An Encoding for CLP Problems in SMT-LIB
Daneshvar Amrollahi, Hossein Hojjat, Philipp R\"ummer
TL;DR
This paper introduces a new Prolog front-end for the Eldarica CHC solver, translating Prolog into SMT-LIB format to enhance compatibility and effectiveness for CHC and CLP applications.
Contribution
It provides a formal translation of a subset of Prolog into SMT-LIB, enabling Prolog inputs for CHC solvers.
Findings
Initial experiments show promising effectiveness.
Potential benefits for CHC and CLP communities.
Enhanced input flexibility for CHC solvers.
Abstract
The input language for today's CHC solvers are commonly the standard SMT-LIB format, borrowed from SMT solvers, and the Prolog format that stems from Constraint-Logic Programming (CLP). This paper presents a new front-end of the Eldarica CHC solver that allows inputs in the Prolog language. We give a formal translation of a subset of Prolog into the SMT-LIB commands. Our initial experiments show the effectiveness of the approach and the potential benefits to both the CHC solving and CLP communities.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.