# CLP-Prover

• 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 arithmetic constraints.
• Download CLP-Prover for Linux/x86: clp-prover (Oct 03, 2007)
• News:
• Oct 03, 2007: added experimental support for unary monotonic functions.
• Example interpolant generation > ≥ < ≤ queries:
• `interpolate([f(x) > 0, x = y], [f(y) =< 0]).`
• `interpolate([f(a) = b+5, f(f(a)) >= b+1], [f(c) = d+4, d = b+1, f(f(c)) < b+1]).`
• `interpolate([f(x, z) >= 1, x = y+1, z =< a, z >= b], [f(y+1, z) =< 0, a =< z, b >= z]).`
• `interpolate([f(a) = b+5, f(f(a)) >= b+1], [f(c) = d+4, d = b+1, f(f(c)) < b+1]).`
• `interpolate([a =< b, a >= c, f(a) =< 1], [b =< d, c >= d, f(d) >= 2]).`
• `interpolate([f(x) >= 1], [f(y) =< -1, x =< y, x >= y]).`
• `interpolate([f(x, z) >= 1, x = y+1, z =< a, z >= b], [f(y+1, z) =< 0, a =< z, b >= z]).`
• `interpolate([x = y], [f(x) = 0, f(y) = 1]).`
• `interpolate([f(x) = 0, f(y) = 1], [x = y]).`
• `interpolate([x = y, z = 0], [f(x+a) = p, f(y+b) = q, a = b, p-q+z = 1]).`
• `interpolate([f(x+a)=p, f(y+b) = q, a = b, p-q+z = 1], [x = y, z = 0]).`
• `interpolate([x = y, z = 0], [f(x+a) = p, f(y+b) = q, a = b, f(p+c) = s, f(q+d) = t, c = d, s-t+z = 1]).`
• `interpolate([f(x+a) = p, f(y+b) = q, a = b, f(p+c) = s, f(q+d) = t, c = d, s-t+z = 1], [x = y, z = 0]).`
• `interpolate([x = y], [f(x) = 1, f(a) = 0, y = a]).`
• `interpolate([x =< p, x >= q, f(x) = 0], [p =< y, q >= y, f(y) = 1]).`
• `add_monotonic(symbol(m,1)).interpolate([x =< y], [m(x) >= m(y)+1]).`
• `add_monotonic(symbol(f,1)).interpolate([x =< t, f(x) >= 1], [t =< y, f(y) =< 0]).`
• 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.` switches off.
• Use `add_monotonic(symbol(Name, Arity)).` to declare monotonic function symbols. Here, `del_monotonic(symbol(Name, Arity)).` reverts the declaration.
• Example un/satisfiability checking queries:
• ``` sat([f(x)>0, x=y, f(y)=<0]). ```
• ``` unsat([f(a)=b+5, f(f(a)) >=b+1, f(c)=d+4, d=b+1, f(f(c))< b+1]). ```
• Use `exit.` to leave the read-eval loop.
• 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 prover.
• solving LI-part applying axioms separating terms total solving total  example #queries CLP-Prover time, s FOCI time, s solving LI-part applying axioms separating terms total solving total `ntdrivers/kbfiltr.i` 139 0.13 0.02 0.00 0.15 0.46 0.55 `ntdrivers/diskperf.i` 747 0.38 0.21 0.00 0.59 2.68 3.72 `ntdrivers/floppy.i` 1082 0.61 0.36 0.00 0.97 3.97 4.91
• Interpretation of the timings: We should compare CLP-Prover total solving time with FOCI time.
• solving LI-part
solving the system of constraints that defines an interpolant in linear arithmetic
• applying axioms
testing entailment of premises of functionality axiom instances
• separating terms
computation of separating terms for premises of applied axiom instances
• total solving
total time spent on constraint solving
• total
total time spent in CLP-Prover, which includes parsing, computation of constraint systems, etc.

Back to homepage