Quickstart Guide ¶
First, create a cvc5 Solver instance using try with resources:
try (Solver solver = new Solver())
{
/** write your code here */
}
To produce models and unsat cores, we have to enable the following options.
solver.setOption("produce-models", "true");
solver.setOption("produce-unsat-cores", "true");
Next 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"
.
solver.setLogic("ALL");
In the following, we will define real and integer constraints. For this, we first query the solver for the corresponding sorts.
Sort realSort = solver.getRealSort();
Sort intSort = solver.getIntegerSort();
Now, we create two constants
x
and
y
of sort
Real
,
and two constants
a
and
b
of sort
Integer
.
Notice that these are
symbolic
constants, not actual values.
Term x = solver.mkConst(realSort, "x");
Term y = solver.mkConst(realSort, "y");
Term a = solver.mkConst(intSort, "a");
Term b = solver.mkConst(intSort, "b");
We define the following constraints regarding
x
and
y
:
\[(0 < x) \wedge (0 < y) \wedge (x + y < 1) \wedge (x \leq y)\]
We construct the required terms and assert them as follows:
// Formally, constraints are also terms. Their sort is Boolean.
// We will construct these constraints gradually,
// by defining each of their components.
// We start with the constant numerals 0 and 1:
Term zero = solver.mkReal(0);
Term one = solver.mkReal(1);
// Next, we construct the term x + y
Term xPlusY = solver.mkTerm(Kind.ADD, x, y);
// Now we can define the constraints.
// They use the operators +, <=, and <.
// In the API, these are denoted by ADD, LEQ, and LT.
// A list of available operators is available in:
// src/api/cpp/cvc5_kind.h
Term constraint1 = solver.mkTerm(Kind.LT, zero, x);
Term constraint2 = solver.mkTerm(Kind.LT, zero, y);
Term constraint3 = solver.mkTerm(Kind.LT, xPlusY, one);
Term constraint4 = solver.mkTerm(Kind.LEQ, x, y);
// Now we assert the constraints to the solver.
solver.assertFormula(constraint1);
solver.assertFormula(constraint2);
solver.assertFormula(constraint3);
solver.assertFormula(constraint4);
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.
Result r1 = solver.checkSat();
The result we get from this satisfiability check is either
sat
,
unsat
or
unknown
.
It’s status can be queried via
Result.isSat
,
Result.isUnsat
and
Result.isSatUnknown
.
Alternatively, it can also be printed.
System.out.println("expected: sat");
System.out.println("result: " + r1);
This will print:
expected: sat
result: sat
Now, we query the solver for the values for
x
and
y
that satisfy
the constraints.
Term xVal = solver.getValue(x);
Term yVal = solver.getValue(y);
It is also possible to get values for terms that do not appear in the original formula.
Term xMinusY = solver.mkTerm(Kind.SUB, x, y);
Term xMinusYVal = solver.getValue(xMinusY);
We can convert these values to Java types.
Pair<BigInteger, BigInteger> xPair = xVal.getRealValue();
Pair<BigInteger, BigInteger> yPair = yVal.getRealValue();
Pair<BigInteger, BigInteger> xMinusYPair = xMinusYVal.getRealValue();
System.out.println("value for x: " + xPair.first + "/" + xPair.second);
System.out.println("value for y: " + yPair.first + "/" + yPair.second);
System.out.println("value for x - y: " + xMinusYPair.first + "/" + xMinusYPair.second);
Another way to independently compute the value of
x
-
y
would be to
perform the (rational) arithmetic manually.
However, for more complex terms, it is easier to let the solver do the
evaluation.
Pair<BigInteger, BigInteger> xMinusYComputed =
new Pair(xPair.first.multiply(yPair.second).subtract(xPair.second.multiply(yPair.first)),
xPair.second.multiply(yPair.second));
BigInteger g = xMinusYComputed.first.gcd(xMinusYComputed.second);
xMinusYComputed = new Pair(xMinusYComputed.first.divide(g), xMinusYComputed.second.divide(g));
if (xMinusYComputed.equals(xMinusYPair))
{
System.out.println("computed correctly");
}
else
{
System.out.println("computed incorrectly");
}
This will print:
computed correctly
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.
solver.resetAssertions();
Next, we assert the same assertions as above, but with integers. This time, we inline the construction of terms in the assertion command.
solver.assertFormula(solver.mkTerm(Kind.LT, solver.mkInteger(0), a));
solver.assertFormula(solver.mkTerm(Kind.LT, solver.mkInteger(0), b));
solver.assertFormula(
solver.mkTerm(Kind.LT, solver.mkTerm(Kind.ADD, a, b), solver.mkInteger(1)));
solver.assertFormula(solver.mkTerm(Kind.LEQ, a, b));
Now, we check whether the revised assertion is satisfiable.
Result r2 = solver.checkSat();
// This time the formula is unsatisfiable
System.out.println("expected: unsat");
System.out.println("result: " + r2);
This time the asserted formula is unsatisfiable:
expected: unsat
result: unsat
We can query the solver for an unsatisfiable core, that is, a subset of the assertions that is already unsatisfiable.
List<Term> unsatCore = Arrays.asList(solver.getUnsatCore());
System.out.println("unsat core size: " + unsatCore.size());
System.out.println("unsat core: ");
for (Term t : unsatCore)
{
System.out.println(t);
}
This will print:
unsat core size: 3
unsat core:
(< 0 a)
(< 0 b)
(< (+ a b) 1)
Example ¶
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 }
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 }
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]
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]