Smt-lib2 counterexample syntax extension
Dear Why3 dev team,
We propose an extension of the smt-lib2 model format that can handle both assertions and declaration of constants. Our proposition is to use the new keywords declare-const and assert to declare fresh constants and to express assertions, respectively.
(declare-const <name> <type>) (assert <expression>)
The main motivation for our request is to adapt the smt-lib2 format to the (richer) counterexamples (CE) produced by our SMT solver Alt-Ergo (AE).
We recently instrumented AE to produce CE in the smt-lib2 format. However, AE can output models implying intervals (like
x in [0;100]) or linear constraints (like
x = y + 1) that cannot be expressed in the (too restricted) format of smt-lib2 . Now, by combining assert, declare-const, AE could produce models for such CE .
For instance, to express that a variable x is in the interval [0;100], AE could output the following model:
(declare-const c_x Int) (assert (and (<= c_x 100) (>= c_x 0))) (define-fun x () Int c_x)
or even simpler:
(declare-const x Int) (assert (and (< x 100) (> x 0)))
Our proposition could also be very useful to output expressive models for other datatypes.
For instance, suppose a CE contains a record x with two labels
b of type Int, and that
x.a in [0;100] and
x.b = 42. Such a model could be expressed as follows:
(declare-datatype t (mk (a Int) (b Int))) (declare-const c_a Int) (assert (and (< c_a 100)(>= c_a 0))) (define-fun x () t (mk c_a 42))
As another example, suppose a CE contains an enumeration datatype
type u = A | B | C | D and a variable i of type u which is known to be only A or B.
Such a model could be expressed as follows:
(declare-datatype u (A B C D)) (declare-const c_i u) (assert (or (= c_i A) (= c_i B))) (define-fun i () u c_i)
Alt-Ergo dev. team