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