Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

An Encoding for CLP Problems in SMT-LIB

Daneshvar Amrollahi, Hossein Hojjat, Philipp Rümmer

TL;DR

The paper addresses bridging Prolog/CLP with CHC solving by introducing a Prolog front-end for the Eldarica CHC solver and a formal translation of Prolog fragments into SMT-LIB. It develops a universal algebraic data-type $U$ and accompanying data-types (e.g., $L$ for lists) to encode Prolog terms, facts, and rules, including CLP($\mathbb{Z}$) arithmetic, as CHC-friendly SMT-LIB constructs. Translation rules are provided for facts, rules, lists, and integers, with typing side-conditions to preserve Prolog semantics. A concrete SMT-LIB encoding of a motivating routing example demonstrates how CHC solvers can derive satisfiability/unsatisfiability and potentially reveal paths under constraints, signaling a foundation for integrated CLP-CHC tooling and potential performance benefits.

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.

An Encoding for CLP Problems in SMT-LIB

TL;DR

The paper addresses bridging Prolog/CLP with CHC solving by introducing a Prolog front-end for the Eldarica CHC solver and a formal translation of Prolog fragments into SMT-LIB. It develops a universal algebraic data-type and accompanying data-types (e.g., for lists) to encode Prolog terms, facts, and rules, including CLP() arithmetic, as CHC-friendly SMT-LIB constructs. Translation rules are provided for facts, rules, lists, and integers, with typing side-conditions to preserve Prolog semantics. A concrete SMT-LIB encoding of a motivating routing example demonstrates how CHC solvers can derive satisfiability/unsatisfiability and potentially reveal paths under constraints, signaling a foundation for integrated CLP-CHC tooling and potential performance benefits.

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.
Paper Structure (14 sections, 4 equations, 16 figures)

This paper contains 14 sections, 4 equations, 16 figures.

Table of Contents

  1. Introduction
  2. Example
  3. Preliminaries
  4. Constraint Logic Programming (CLP)
  5. SMT-LIB
  6. Translating CLP to SMT-LIB
  7. A Motivating Example
  8. Algebraic Data Types (ADTs)
  9. Translation of Facts
  10. Translation of Rules
  11. Translation of Lists
  12. Integer Arithmetic
  13. An SMT-LIB Encoding of the Motivating Example
  14. Conclusion

Figures (16)

  • Figure 1: Prolog Program for distance between cities in CLP($\mathbb{Z}$)
  • Figure 2: A simplified grammar for describing the syntax of Prolog programs.
  • Figure 3: SMT-LIB equivalent of man(father(claire))
  • Figure 4: Function $\mathit{collectFunctions}$ collecting functions in the terms
  • Figure 5: Definition of the universal type U for functions $\{ (f_1, a_1), \ldots, (f_n, a_n) \}$
  • ...and 11 more figures