An Encoding for CLP Problems in SMT-LIB
read the original 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.
This paper has not been read by Pith yet.
Forward citations
Cited by 1 Pith paper
-
FuzzPilot: Plateau-Triggered Recipe Validation for Structured Text Fuzzing
FuzzPilot implements plateau-triggered recipe validation for AFL++ but reports no statistically significant coverage gains and zero promotions of model-proposed recipes on the saturated cJSON target.
discussion (0)
Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.