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