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 :dump-unsat-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 :dump-unsat-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]
examples/api/cpp/quickstart.cpp
1 /******************************************************************************
2 * Top contributors (to current version):
3 * Yoni Zohar, Gereon Kremer, Mathias Preiner
4 *
5 * This file is part of the cvc5 project.
6 *
7 * Copyright (c) 2009-2022 by the authors listed in the file AUTHORS
8 * in the top-level source directory and their institutional affiliations.
9 * All rights reserved. See the file COPYING in the top-level source
10 * directory for licensing information.
11 * ****************************************************************************
12 *
13 * A simple demonstration of the api capabilities of cvc5.
14 *
15 */
16
17 #include <cvc5/cvc5.h>
18
19 #include <iostream>
20 #include <numeric>
21
22 using namespace cvc5;
23
24 int main()
25 {
26 // Create a solver
27 //! [docs-cpp-quickstart-1 start]
28 Solver solver;
29 //! [docs-cpp-quickstart-1 end]
30
31 // We will ask the solver to produce models and unsat cores,
32 // hence these options should be turned on.
33 //! [docs-cpp-quickstart-2 start]
34 solver.setOption("produce-models", "true");
35 solver.setOption("produce-unsat-cores", "true");
36 //! [docs-cpp-quickstart-2 end]
37
38 // The simplest way to set a logic for the solver is to choose "ALL".
39 // This enables all logics in the solver.
40 // Alternatively, "QF_ALL" enables all logics without quantifiers.
41 // To optimize the solver's behavior for a more specific logic,
42 // use the logic name, e.g. "QF_BV" or "QF_AUFBV".
43
44 // Set the logic
45 //! [docs-cpp-quickstart-3 start]
46 solver.setLogic("ALL");
47 //! [docs-cpp-quickstart-3 end]
48
49 // In this example, we will define constraints over reals and integers.
50 // Hence, we first obtain the corresponding sorts.
51 //! [docs-cpp-quickstart-4 start]
52 Sort realSort = solver.getRealSort();
53 Sort intSort = solver.getIntegerSort();
54 //! [docs-cpp-quickstart-4 end]
55
56 // x and y will be real variables, while a and b will be integer variables.
57 // Formally, their cpp type is Term,
58 // and they are called "constants" in SMT jargon:
59 //! [docs-cpp-quickstart-5 start]
60 Term x = solver.mkConst(realSort, "x");
61 Term y = solver.mkConst(realSort, "y");
62 Term a = solver.mkConst(intSort, "a");
63 Term b = solver.mkConst(intSort, "b");
64 //! [docs-cpp-quickstart-5 end]
65
66 // Our constraints regarding x and y will be:
67 //
68 // (1) 0 < x
69 // (2) 0 < y
70 // (3) x + y < 1
71 // (4) x <= y
72 //
73
74 //! [docs-cpp-quickstart-6 start]
75 // Formally, constraints are also terms. Their sort is Boolean.
76 // We will construct these constraints gradually,
77 // by defining each of their components.
78 // We start with the constant numerals 0 and 1:
79 Term zero = solver.mkReal(0);
80 Term one = solver.mkReal(1);
81
82 // Next, we construct the term x + y
83 Term xPlusY = solver.mkTerm(ADD, {x, y});
84
85 // Now we can define the constraints.
86 // They use the operators +, <=, and <.
87 // In the API, these are denoted by ADD, LEQ, and LT.
88 // A list of available operators is available in:
89 // src/api/cpp/cvc5_kind.h
90 Term constraint1 = solver.mkTerm(LT, {zero, x});
91 Term constraint2 = solver.mkTerm(LT, {zero, y});
92 Term constraint3 = solver.mkTerm(LT, {xPlusY, one});
93 Term constraint4 = solver.mkTerm(LEQ, {x, y});
94
95 // Now we assert the constraints to the solver.
96 solver.assertFormula(constraint1);
97 solver.assertFormula(constraint2);
98 solver.assertFormula(constraint3);
99 solver.assertFormula(constraint4);
100 //! [docs-cpp-quickstart-6 end]
101
102 // Check if the formula is satisfiable, that is,
103 // are there real values for x and y that satisfy all the constraints?
104 //! [docs-cpp-quickstart-7 start]
105 Result r1 = solver.checkSat();
106 //! [docs-cpp-quickstart-7 end]
107
108 // The result is either SAT, UNSAT, or UNKNOWN.
109 // In this case, it is SAT.
110 //! [docs-cpp-quickstart-8 start]
111 std::cout << "expected: sat" << std::endl;
112 std::cout << "result: " << r1 << std::endl;
113 //! [docs-cpp-quickstart-8 end]
114
115 // We can get the values for x and y that satisfy the constraints.
116 //! [docs-cpp-quickstart-9 start]
117 Term xVal = solver.getValue(x);
118 Term yVal = solver.getValue(y);
119 //! [docs-cpp-quickstart-9 end]
120
121 // It is also possible to get values for compound terms,
122 // even if those did not appear in the original formula.
123 //! [docs-cpp-quickstart-10 start]
124 Term xMinusY = solver.mkTerm(SUB, {x, y});
125 Term xMinusYVal = solver.getValue(xMinusY);
126 //! [docs-cpp-quickstart-10 end]
127
128 // We can now obtain the string representations of the values.
129 //! [docs-cpp-quickstart-11 start]
130 std::string xStr = xVal.getRealValue();
131 std::string yStr = yVal.getRealValue();
132 std::string xMinusYStr = xMinusYVal.getRealValue();
133
134 std::cout << "value for x: " << xStr << std::endl;
135 std::cout << "value for y: " << yStr << std::endl;
136 std::cout << "value for x - y: " << xMinusYStr << std::endl;
137 //! [docs-cpp-quickstart-11 end]
138
139 //! [docs-cpp-quickstart-12 start]
140 // Further, we can convert the values to cpp types
141 std::pair<int64_t, uint64_t> xPair = xVal.getReal64Value();
142 std::pair<int64_t, uint64_t> yPair = yVal.getReal64Value();
143 std::pair<int64_t, uint64_t> xMinusYPair = xMinusYVal.getReal64Value();
144
145 std::cout << "value for x: " << xPair.first << "/" << xPair.second
146 << std::endl;
147 std::cout << "value for y: " << yPair.first << "/" << yPair.second
148 << std::endl;
149 std::cout << "value for x - y: " << xMinusYPair.first << "/"
150 << xMinusYPair.second << std::endl;
151 //! [docs-cpp-quickstart-12 end]
152
153 // Another way to independently compute the value of x - y would be
154 // to perform the (rational) arithmetic manually.
155 // However, for more complex terms,
156 // it is easier to let the solver do the evaluation.
157 //! [docs-cpp-quickstart-13 start]
158 std::pair<int64_t, uint64_t> xMinusYComputed = {
159 xPair.first * yPair.second - xPair.second * yPair.first,
160 xPair.second * yPair.second
161 };
162 uint64_t g = std::gcd(xMinusYComputed.first, xMinusYComputed.second);
163 xMinusYComputed = { xMinusYComputed.first / g, xMinusYComputed.second / g };
164 if (xMinusYComputed == xMinusYPair)
165 {
166 std::cout << "computed correctly" << std::endl;
167 }
168 else
169 {
170 std::cout << "computed incorrectly" << std::endl;
171 }
172 //! [docs-cpp-quickstart-13 end]
173
174 // Next, we will check satisfiability of the same formula,
175 // only this time over integer variables a and b.
176
177 // We start by resetting assertions added to the solver.
178 //! [docs-cpp-quickstart-14 start]
179 solver.resetAssertions();
180 //! [docs-cpp-quickstart-14 end]
181
182 // Next, we assert the same assertions above with integers.
183 // This time, we inline the construction of terms
184 // to the assertion command.
185 //! [docs-cpp-quickstart-15 start]
186 solver.assertFormula(solver.mkTerm(LT, {solver.mkInteger(0), a}));
187 solver.assertFormula(solver.mkTerm(LT, {solver.mkInteger(0), b}));
188 solver.assertFormula(
189 solver.mkTerm(LT, {solver.mkTerm(ADD, {a, b}), solver.mkInteger(1)}));
190 solver.assertFormula(solver.mkTerm(LEQ, {a, b}));
191 //! [docs-cpp-quickstart-15 end]
192
193 // We check whether the revised assertion is satisfiable.
194 //! [docs-cpp-quickstart-16 start]
195 Result r2 = solver.checkSat();
196 //! [docs-cpp-quickstart-16 end]
197
198 // This time the formula is unsatisfiable
199 //! [docs-cpp-quickstart-17 start]
200 std::cout << "expected: unsat" << std::endl;
201 std::cout << "result: " << r2 << std::endl;
202 //! [docs-cpp-quickstart-17 end]
203
204 // We can query the solver for an unsatisfiable core, i.e., a subset
205 // of the assertions that is already unsatisfiable.
206 //! [docs-cpp-quickstart-18 start]
207 std::vector<Term> unsatCore = solver.getUnsatCore();
208 std::cout << "unsat core size: " << unsatCore.size() << std::endl;
209 std::cout << "unsat core: " << std::endl;
210 for (const Term& t : unsatCore)
211 {
212 std::cout << t << std::endl;
213 }
214 //! [docs-cpp-quickstart-18 end]
215
216 return 0;
217 }
examples/api/java/QuickStart.java
1 /******************************************************************************
2 * Top contributors (to current version):
3 * Mudathir Mohamed, Aina Niemetz, Andres Noetzli
4 *
5 * This file is part of the cvc5 project.
6 *
7 * Copyright (c) 2009-2022 by the authors listed in the file AUTHORS
8 * in the top-level source directory and their institutional affiliations.
9 * All rights reserved. See the file COPYING in the top-level source
10 * directory for licensing information.
11 * ****************************************************************************
12 *
13 * A simple demonstration of the api capabilities of cvc5.
14 *
15 */
16
17 import io.github.cvc5.*;
18 import java.math.BigInteger;
19 import java.util.ArrayList;
20 import java.util.Arrays;
21 import java.util.List;
22
23 public class QuickStart
24 {
25 public static void main(String args[]) throws CVC5ApiException
26 {
27 // Create a solver
28 try (Solver solver = new Solver())
29 {
30 // We will ask the solver to produce models and unsat cores,
31 // hence these options should be turned on.
32 //! [docs-java-quickstart-1 start]
33 solver.setOption("produce-models", "true");
34 solver.setOption("produce-unsat-cores", "true");
35 //! [docs-java-quickstart-1 end]
36
37 // The simplest way to set a logic for the solver is to choose "ALL".
38 // This enables all logics in the solver.
39 // Alternatively, "QF_ALL" enables all logics without quantifiers.
40 // To optimize the solver's behavior for a more specific logic,
41 // use the logic name, e.g. "QF_BV" or "QF_AUFBV".
42
43 // Set the logic
44 //! [docs-java-quickstart-2 start]
45 solver.setLogic("ALL");
46 //! [docs-java-quickstart-2 end]
47
48 // In this example, we will define constraints over reals and integers.
49 // Hence, we first obtain the corresponding sorts.
50 //! [docs-java-quickstart-3 start]
51 Sort realSort = solver.getRealSort();
52 Sort intSort = solver.getIntegerSort();
53 //! [docs-java-quickstart-3 end]
54
55 // x and y will be real variables, while a and b will be integer variables.
56 // Formally, their cpp type is Term,
57 // and they are called "constants" in SMT jargon:
58 //! [docs-java-quickstart-4 start]
59 Term x = solver.mkConst(realSort, "x");
60 Term y = solver.mkConst(realSort, "y");
61 Term a = solver.mkConst(intSort, "a");
62 Term b = solver.mkConst(intSort, "b");
63 //! [docs-java-quickstart-4 end]
64
65 // Our constraints regarding x and y will be:
66 //
67 // (1) 0 < x
68 // (2) 0 < y
69 // (3) x + y < 1
70 // (4) x <= y
71 //
72
73 //! [docs-java-quickstart-5 start]
74 // Formally, constraints are also terms. Their sort is Boolean.
75 // We will construct these constraints gradually,
76 // by defining each of their components.
77 // We start with the constant numerals 0 and 1:
78 Term zero = solver.mkReal(0);
79 Term one = solver.mkReal(1);
80
81 // Next, we construct the term x + y
82 Term xPlusY = solver.mkTerm(Kind.ADD, x, y);
83
84 // Now we can define the constraints.
85 // They use the operators +, <=, and <.
86 // In the API, these are denoted by ADD, LEQ, and LT.
87 // A list of available operators is available in:
88 // src/api/cpp/cvc5_kind.h
89 Term constraint1 = solver.mkTerm(Kind.LT, zero, x);
90 Term constraint2 = solver.mkTerm(Kind.LT, zero, y);
91 Term constraint3 = solver.mkTerm(Kind.LT, xPlusY, one);
92 Term constraint4 = solver.mkTerm(Kind.LEQ, x, y);
93
94 // Now we assert the constraints to the solver.
95 solver.assertFormula(constraint1);
96 solver.assertFormula(constraint2);
97 solver.assertFormula(constraint3);
98 solver.assertFormula(constraint4);
99 //! [docs-java-quickstart-5 end]
100
101 // Check if the formula is satisfiable, that is,
102 // are there real values for x and y that satisfy all the constraints?
103 //! [docs-java-quickstart-6 start]
104 Result r1 = solver.checkSat();
105 //! [docs-java-quickstart-6 end]
106
107 // The result is either SAT, UNSAT, or UNKNOWN.
108 // In this case, it is SAT.
109 //! [docs-java-quickstart-7 start]
110 System.out.println("expected: sat");
111 System.out.println("result: " + r1);
112 //! [docs-java-quickstart-7 end]
113
114 // We can get the values for x and y that satisfy the constraints.
115 //! [docs-java-quickstart-8 start]
116 Term xVal = solver.getValue(x);
117 Term yVal = solver.getValue(y);
118 //! [docs-java-quickstart-8 end]
119
120 // It is also possible to get values for compound terms,
121 // even if those did not appear in the original formula.
122 //! [docs-java-quickstart-9 start]
123 Term xMinusY = solver.mkTerm(Kind.SUB, x, y);
124 Term xMinusYVal = solver.getValue(xMinusY);
125 //! [docs-java-quickstart-9 end]
126
127 // Further, we can convert the values to java types
128 //! [docs-java-quickstart-10 start]
129 Pair<BigInteger, BigInteger> xPair = xVal.getRealValue();
130 Pair<BigInteger, BigInteger> yPair = yVal.getRealValue();
131 Pair<BigInteger, BigInteger> xMinusYPair = xMinusYVal.getRealValue();
132
133 System.out.println("value for x: " + xPair.first + "/" + xPair.second);
134 System.out.println("value for y: " + yPair.first + "/" + yPair.second);
135 System.out.println("value for x - y: " + xMinusYPair.first + "/" + xMinusYPair.second);
136 //! [docs-java-quickstart-10 end]
137
138 // Another way to independently compute the value of x - y would be
139 // to perform the (rational) arithmetic manually.
140 // However, for more complex terms,
141 // it is easier to let the solver do the evaluation.
142 //! [docs-java-quickstart-11 start]
143 Pair<BigInteger, BigInteger> xMinusYComputed =
144 new Pair(xPair.first.multiply(yPair.second).subtract(xPair.second.multiply(yPair.first)),
145 xPair.second.multiply(yPair.second));
146 BigInteger g = xMinusYComputed.first.gcd(xMinusYComputed.second);
147 xMinusYComputed = new Pair(xMinusYComputed.first.divide(g), xMinusYComputed.second.divide(g));
148 if (xMinusYComputed.equals(xMinusYPair))
149 {
150 System.out.println("computed correctly");
151 }
152 else
153 {
154 System.out.println("computed incorrectly");
155 }
156 //! [docs-java-quickstart-11 end]
157
158 // Next, we will check satisfiability of the same formula,
159 // only this time over integer variables a and b.
160
161 // We start by resetting assertions added to the solver.
162 //! [docs-java-quickstart-12 start]
163 solver.resetAssertions();
164 //! [docs-java-quickstart-12 end]
165
166 // Next, we assert the same assertions above with integers.
167 // This time, we inline the construction of terms
168 // to the assertion command.
169 //! [docs-java-quickstart-13 start]
170 solver.assertFormula(solver.mkTerm(Kind.LT, solver.mkInteger(0), a));
171 solver.assertFormula(solver.mkTerm(Kind.LT, solver.mkInteger(0), b));
172 solver.assertFormula(
173 solver.mkTerm(Kind.LT, solver.mkTerm(Kind.ADD, a, b), solver.mkInteger(1)));
174 solver.assertFormula(solver.mkTerm(Kind.LEQ, a, b));
175 //! [docs-java-quickstart-13 end]
176
177 // We check whether the revised assertion is satisfiable.
178 //! [docs-java-quickstart-14 start]
179 Result r2 = solver.checkSat();
180
181 // This time the formula is unsatisfiable
182 System.out.println("expected: unsat");
183 System.out.println("result: " + r2);
184 //! [docs-java-quickstart-14 end]
185
186 // We can query the solver for an unsatisfiable core, i.e., a subset
187 // of the assertions that is already unsatisfiable.
188 //! [docs-java-quickstart-15 start]
189 List<Term> unsatCore = Arrays.asList(solver.getUnsatCore());
190 System.out.println("unsat core size: " + unsatCore.size());
191 System.out.println("unsat core: ");
192 for (Term t : unsatCore)
193 {
194 System.out.println(t);
195 }
196 //! [docs-java-quickstart-15 end]
197 }
198 }
199 }
cvc5_pythonic_api:/test/pgms/example_quickstart.py
1 from cvc5_pythonic_api import *
2
3 if __name__ == '__main__':
4
5 # Let's introduce some variables
6 x, y = Reals('x y')
7 a, b = Ints('a b')
8
9 # We will confirm that
10 # * 0 < x
11 # * 0 < y
12 # * x + y < 1
13 # * x <= y
14 # are satisfiable
15 solve(0 < x, 0 < y, x + y < 1, x <= y)
16
17 # If we get the model (the satisfying assignment) explicitly, we can
18 # evaluate terms under it.
19 s = Solver()
20 s.add(0 < x, 0 < y, x + y < 1, x <= y)
21 assert sat == s.check()
22 m = s.model()
23
24 print('x:', m[x])
25 print('y:', m[y])
26 print('x - y:', m[x - y])
27
28 # We can also get these values in other forms:
29 print('string x:', str(m[x]))
30 print('decimal x:', m[x].as_decimal(4))
31 print('fraction x:', m[x].as_fraction())
32 print('float x:', float(m[x].as_fraction()))
33
34 # The above constraints are *UNSAT* for integer variables.
35 # This reports "no solution"
36 solve(0 < a, 0 < b, a + b < 1, a <= b)
37
38
39
examples/api/python/quickstart.py
1 #!/usr/bin/env python
2 ###############################################################################
3 # Top contributors (to current version):
4 # Yoni Zohar, Aina Niemetz, Alex Ozdemir
5 #
6 # This file is part of the cvc5 project.
7 #
8 # Copyright (c) 2009-2022 by the authors listed in the file AUTHORS
9 # in the top-level source directory and their institutional affiliations.
10 # All rights reserved. See the file COPYING in the top-level source
11 # directory for licensing information.
12 # #############################################################################
13 #
14 # A simple demonstration of the api capabilities of cvc5, adapted from quickstart.cpp
15 ##
16
17 import cvc5
18 from cvc5 import Kind
19
20 if __name__ == "__main__":
21 # Create a solver
22 #! [docs-python-quickstart-1 start]
23 solver = cvc5.Solver()
24 #! [docs-python-quickstart-1 end]
25
26 # We will ask the solver to produce models and unsat cores,
27 # hence these options should be turned on.
28 #! [docs-python-quickstart-2 start]
29 solver.setOption("produce-models", "true");
30 solver.setOption("produce-unsat-cores", "true");
31 #! [docs-python-quickstart-2 end]
32
33 # The simplest way to set a logic for the solver is to choose "ALL".
34 # This enables all logics in the solver.
35 # Alternatively, "QF_ALL" enables all logics without quantifiers.
36 # To optimize the solver's behavior for a more specific logic,
37 # use the logic name, e.g. "QF_BV" or "QF_AUFBV".
38
39 # Set the logic
40 #! [docs-python-quickstart-3 start]
41 solver.setLogic("ALL");
42 #! [docs-python-quickstart-3 end]
43
44 # In this example, we will define constraints over reals and integers.
45 # Hence, we first obtain the corresponding sorts.
46 #! [docs-python-quickstart-4 start]
47 realSort = solver.getRealSort();
48 intSort = solver.getIntegerSort();
49 #! [docs-python-quickstart-4 end]
50
51 # x and y will be real variables, while a and b will be integer variables.
52 # Formally, their python type is Term,
53 # and they are called "constants" in SMT jargon:
54 #! [docs-python-quickstart-5 start]
55 x = solver.mkConst(realSort, "x");
56 y = solver.mkConst(realSort, "y");
57 a = solver.mkConst(intSort, "a");
58 b = solver.mkConst(intSort, "b");
59 #! [docs-python-quickstart-5 end]
60
61 # Our constraints regarding x and y will be:
62 #
63 # (1) 0 < x
64 # (2) 0 < y
65 # (3) x + y < 1
66 # (4) x <= y
67 #
68
69 #! [docs-python-quickstart-6 start]
70 # Formally, constraints are also terms. Their sort is Boolean.
71 # We will construct these constraints gradually,
72 # by defining each of their components.
73 # We start with the constant numerals 0 and 1:
74 zero = solver.mkReal(0);
75 one = solver.mkReal(1);
76
77 # Next, we construct the term x + y
78 xPlusY = solver.mkTerm(Kind.ADD, x, y);
79
80 # Now we can define the constraints.
81 # They use the operators +, <=, and <.
82 # In the API, these are denoted by Plus, Leq, and Lt.
83 constraint1 = solver.mkTerm(Kind.LT, zero, x);
84 constraint2 = solver.mkTerm(Kind.LT, zero, y);
85 constraint3 = solver.mkTerm(Kind.LT, xPlusY, one);
86 constraint4 = solver.mkTerm(Kind.LEQ, x, y);
87
88 # Now we assert the constraints to the solver.
89 solver.assertFormula(constraint1);
90 solver.assertFormula(constraint2);
91 solver.assertFormula(constraint3);
92 solver.assertFormula(constraint4);
93 #! [docs-python-quickstart-6 end]
94
95 # Check if the formula is satisfiable, that is,
96 # are there real values for x and y that satisfy all the constraints?
97 #! [docs-python-quickstart-7 start]
98 r1 = solver.checkSat();
99 #! [docs-python-quickstart-7 end]
100
101 # The result is either SAT, UNSAT, or UNKNOWN.
102 # In this case, it is SAT.
103 #! [docs-python-quickstart-8 start]
104 print("expected: sat")
105 print("result: ", r1)
106 #! [docs-python-quickstart-8 end]
107
108 # We can get the values for x and y that satisfy the constraints.
109 #! [docs-python-quickstart-9 start]
110 xVal = solver.getValue(x);
111 yVal = solver.getValue(y);
112 #! [docs-python-quickstart-9 end]
113
114 # It is also possible to get values for compound terms,
115 # even if those did not appear in the original formula.
116 #! [docs-python-quickstart-10 start]
117 xMinusY = solver.mkTerm(Kind.SUB, x, y);
118 xMinusYVal = solver.getValue(xMinusY);
119 #! [docs-python-quickstart-10 end]
120
121 # We can now obtain the values as python values
122 #! [docs-python-quickstart-11 start]
123 xPy = xVal.getRealValue();
124 yPy = yVal.getRealValue();
125 xMinusYPy = xMinusYVal.getRealValue();
126
127 print("value for x: ", xPy)
128 print("value for y: ", yPy)
129 print("value for x - y: ", xMinusYPy)
130 #! [docs-python-quickstart-11 end]
131
132 # Another way to independently compute the value of x - y would be
133 # to use the python minus operator instead of asking the solver.
134 # However, for more complex terms,
135 # it is easier to let the solver do the evaluation.
136 #! [docs-python-quickstart-12 start]
137 xMinusYComputed = xPy - yPy;
138 if xMinusYComputed == xMinusYPy:
139 print("computed correctly")
140 else:
141 print("computed incorrectly")
142 #! [docs-python-quickstart-12 end]
143
144 # Further, we can convert the values to strings
145 #! [docs-python-quickstart-13 start]
146 xStr = str(xPy);
147 yStr = str(yPy);
148 xMinusYStr = str(xMinusYPy);
149 #! [docs-python-quickstart-13 end]
150
151 # Next, we will check satisfiability of the same formula,
152 # only this time over integer variables a and b.
153
154 # We start by resetting assertions added to the solver.
155 #! [docs-python-quickstart-14 start]
156 solver.resetAssertions();
157 #! [docs-python-quickstart-14 end]
158
159 # Next, we assert the same assertions above with integers.
160 # This time, we inline the construction of terms
161 # to the assertion command.
162 #! [docs-python-quickstart-15 start]
163 solver.assertFormula(solver.mkTerm(Kind.LT, solver.mkInteger(0), a));
164 solver.assertFormula(solver.mkTerm(Kind.LT, solver.mkInteger(0), b));
165 solver.assertFormula(
166 solver.mkTerm(
167 Kind.LT, solver.mkTerm(Kind.ADD, a, b), solver.mkInteger(1)));
168 solver.assertFormula(solver.mkTerm(Kind.LEQ, a, b));
169 #! [docs-python-quickstart-15 end]
170
171 # We check whether the revised assertion is satisfiable.
172 #! [docs-python-quickstart-16 start]
173 r2 = solver.checkSat();
174 #! [docs-python-quickstart-16 end]
175
176 # This time the formula is unsatisfiable
177 #! [docs-python-quickstart-17 start]
178 print("expected: unsat")
179 print("result:", r2)
180 #! [docs-python-quickstart-17 end]
181
182 # We can query the solver for an unsatisfiable core, i.e., a subset
183 # of the assertions that is already unsatisfiable.
184 #! [docs-python-quickstart-18 start]
185 unsatCore = solver.getUnsatCore();
186 print("unsat core size:", len(unsatCore))
187 print("unsat core:", unsatCore)
188 #! [docs-python-quickstart-18 end]