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)
• License text
• 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.