CLP-Prover is a constraint logic programming-based tool for
satisfiability checking and interpolant generation. It is implemented
in SICStus Prolog and applies the clp(q,r) library for solving linear
Download CLP-Prover for Linux/x86: clp-prover
(Oct 03, 2007)
Use print_interpolant_ast. to switch on printing of the
abstract syntax tree of the computed interpolant (useful for parsing
CLP-Prover output in an external application). You can switch it off
using no_print_interpolant_ast. command.
Use print_instances. to print instances of functionality
axioms applied on the A-side. no_print_instances.
Use add_monotonic(symbol(Name, Arity)). to declare monotonic
function symbols. Here, del_monotonic(symbol(Name, Arity)).
reverts the declaration.
The expression language description can be found at on
this page. Note that it is extended with applications of function
symbols. We use constants (nullary function symbols) to represent
variables, and not the Prolog variables!
Preliminary experimental evaluation on examples from Blast
distribution. We used a Linux PC with 3 GHz CPU. Memory consumption
was not an issue. We integrated CLP-Prover into Blast 2.0 and applied
it on queries that are passed to the FOCI interpolating theorem
CLP-Prover time, s
FOCI time, s
solving LI-part applying axioms separating terms total solving total
Interpretation of the timings: We should compare CLP-Prover total solving time
with FOCI time.
solving the system of constraints that defines an interpolant in linear arithmetic
testing entailment of premises of functionality axiom instances
computation of separating terms for premises of applied axiom instances
total time spent on constraint solving
total time spent in CLP-Prover, which includes parsing, computation of constraint systems, etc.