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 a
and 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)
Best regards,
Alt-Ergo dev. team