An Encoding for CLP Problems in SMT-LIB
<|reference_start|>An Encoding for CLP Problems in SMT-LIB: 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.<|reference_end|>
@article{amrollahi2024an,
    title={An Encoding for CLP Problems in SMT-LIB},
    author={Daneshvar Amrollahi, Hossein Hojjat, Philipp R"ummer},
    journal={EPTCS 402, 2024, pp. 118-130},
    year={2024},
    doi={10.4204/EPTCS.402.12},
    archivePrefix={arXiv},
    eprint={2404.14924},
    primaryClass={cs.LO cs.PL}
}