Quickstart Guide

The primary input language for cvc5 is SMT-LIB v2. We give a short explanation of the SMT-LIB v2 quickstart example here.

First, we set the logic. The simplest way to set a logic for the solver is to choose “ALL”. This enables all logics in the solver. Alternatively, "QF_ALL" enables all logics without quantifiers. To optimize the solver’s behavior for a more specific logic, use the logic name, e.g. "QF_BV" or "QF_AUFBV".

(set-logic ALL)

We will ask the solver to produce models and unsat cores in the following, and for this we have to enable the following options. Furthermore, we enable incremental solving so that we can use the (reset-assertions) command later on.

(set-option :produce-models true)
(set-option :incremental true)
; print unsat cores, include assertions in the unsat core that have not been named
(set-option :produce-unsat-cores true)
(set-option :print-cores-full true)

Now, we create two constants x and y of sort Real. Notice that these are symbolic constants, but not actual values.

; Declare real constants x,y
(declare-const x Real)
(declare-const y Real)

We define the following constraints regarding x and y:

\[(0 < x) \wedge (0 < y) \wedge (x + y < 1) \wedge (x \leq y)\]

We assert them as follows. Notice that in SMT-LIB v2, terms are written in prefix notation, e.g., we write (+ x y) instead of (x + y).

; Our constraints regarding x and y will be:
;
;   (1)  0 < x
;   (2)  0 < y
;   (3)  x + y < 1
;   (4)  x <= y

(assert (< 0 x))
(assert (< 0 y))
(assert (< (+ x y) 1))
(assert (<= x y))

Now we check if the asserted formula is satisfiable, that is, we check if there exist values of sort Real for x and y that satisfy all the constraints.

(check-sat)

The result we get from this satisfiability check is either sat, unsat or unknown, and it is printed to standard output. In this case, it will print sat.

Now, we query the solver for the values for x and y that satisfy the constraints. It is also possible to get values for terms that do not appear in the original formula.

(echo "Values of declared real constants and of compound terms built with them.")
(get-value (x y (- x y)))

This will print the values of x, y, and x-y, in a key-value format (<term> <value>) one after the other:

((x (/ 1 6)) (y (/ 1 6)) ((- x y) 0.0))

Next, we will check satisfiability of the same formula, only this time over integer variables a and b. For this, we first reset the assertions added to the solver and declare fresh integer variables a and b.

(echo "We will reset the solver with the (reset-assertions) command and check satisfiability of the same assertions but with the integers constants rather than with the real ones.")
(reset-assertions)
; Declare integer constants a,b
(declare-const a Int)
(declare-const b Int)

Next, we assert the same assertions as above, but with integers.

(assert (< 0 a))
(assert (< 0 b))
(assert (< (+ a b) 1))
(assert (<= a b))

Now, we check whether the revised query is satisfiable.

(check-sat)

This time the asserted formula is unsatisfiable and unsat is printed.

We can query the solver for an unsatisfiable core, that is, a subset of the assertions that is already unsatisfiable.

(get-unsat-core)

This will print:

(
(< 0 a)
(< 0 b)
(< (+ a b) 1)
)

Example

examples/api/smtlib/quickstart.smt2

 1;! [docs-smt2-quickstart-1 start]
 2(set-logic ALL)
 3;! [docs-smt2-quickstart-1 end]
 4;! [docs-smt2-quickstart-2 start]
 5(set-option :produce-models true)
 6(set-option :incremental true)
 7; print unsat cores, include assertions in the unsat core that have not been named
 8(set-option :produce-unsat-cores true)
 9(set-option :print-cores-full true)
10;! [docs-smt2-quickstart-2 end]
11
12;! [docs-smt2-quickstart-3 start]
13; Declare real constants x,y
14(declare-const x Real)
15(declare-const y Real)
16;! [docs-smt2-quickstart-3 end]
17
18;! [docs-smt2-quickstart-4 start]
19; Our constraints regarding x and y will be:
20;
21;   (1)  0 < x
22;   (2)  0 < y
23;   (3)  x + y < 1
24;   (4)  x <= y
25
26(assert (< 0 x))
27(assert (< 0 y))
28(assert (< (+ x y) 1))
29(assert (<= x y))
30;! [docs-smt2-quickstart-4 end]
31
32;! [docs-smt2-quickstart-5 start]
33(check-sat)
34;! [docs-smt2-quickstart-5 end]
35;! [docs-smt2-quickstart-6 start]
36(echo "Values of declared real constants and of compound terms built with them.")
37(get-value (x y (- x y)))
38;! [docs-smt2-quickstart-6 end]
39
40;! [docs-smt2-quickstart-7 start]
41(echo "We will reset the solver with the (reset-assertions) command and check satisfiability of the same assertions but with the integers constants rather than with the real ones.")
42(reset-assertions)
43; Declare integer constants a,b
44(declare-const a Int)
45(declare-const b Int)
46;! [docs-smt2-quickstart-7 end]
47;! [docs-smt2-quickstart-8 start]
48(assert (< 0 a))
49(assert (< 0 b))
50(assert (< (+ a b) 1))
51(assert (<= a b))
52;! [docs-smt2-quickstart-8 end]
53
54;! [docs-smt2-quickstart-9 start]
55(check-sat)
56;! [docs-smt2-quickstart-9 end]
57;! [docs-smt2-quickstart-10 start]
58(get-unsat-core)
59;! [docs-smt2-quickstart-10 end]