Quickstart Guide
First, 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, but not actual values.
x, y = Reals('x y')
a, b = Ints('a b')
We define the following constraints regarding
x
and
y
:
\[(0 < x) \wedge (0 < y) \wedge (x + y < 1) \wedge (x \leq y)\]
We check whether there is a solution to these constraints:
solve(0 < x, 0 < y, x + y < 1, x <= y)
In this case, there is, so we get output:
[x = 1/6, y = 1/6]
We can also get an explicit model (assignment) for the constraints.
s = Solver()
s.add(0 < x, 0 < y, x + y < 1, x <= y)
assert sat == s.check()
m = s.model()
With the model, we can evaluate variables and terms:
print('x:', m[x])
print('y:', m[y])
print('x - y:', m[x - y])
This will print:
x: 1/6
y: 1/6
x - y: 0
We can also get these values in other forms:
print('string x:', str(m[x]))
print('decimal x:', m[x].as_decimal(4))
print('fraction x:', m[x].as_fraction())
print('float x:', float(m[x].as_fraction()))
Next, we assert the same assertions as above, but with integers. This time, there is no solution, so “no solution” is printed.
solve(0 < a, 0 < b, a + b < 1, a <= b)
Example
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 solver = cvc5.Solver()
23
24 # We will ask the solver to produce models and unsat cores,
25 # hence these options should be turned on.
26 solver.setOption("produce-models", "true");
27 solver.setOption("produce-unsat-cores", "true");
28
29 # The simplest way to set a logic for the solver is to choose "ALL".
30 # This enables all logics in the solver.
31 # Alternatively, "QF_ALL" enables all logics without quantifiers.
32 # To optimize the solver's behavior for a more specific logic,
33 # use the logic name, e.g. "QF_BV" or "QF_AUFBV".
34
35 # Set the logic
36 solver.setLogic("ALL");
37
38 # In this example, we will define constraints over reals and integers.
39 # Hence, we first obtain the corresponding sorts.
40 realSort = solver.getRealSort();
41 intSort = solver.getIntegerSort();
42
43 # x and y will be real variables, while a and b will be integer variables.
44 # Formally, their python type is Term,
45 # and they are called "constants" in SMT jargon:
46 x = solver.mkConst(realSort, "x");
47 y = solver.mkConst(realSort, "y");
48 a = solver.mkConst(intSort, "a");
49 b = solver.mkConst(intSort, "b");
50
51 # Our constraints regarding x and y will be:
52 #
53 # (1) 0 < x
54 # (2) 0 < y
55 # (3) x + y < 1
56 # (4) x <= y
57 #
58
59 # Formally, constraints are also terms. Their sort is Boolean.
60 # We will construct these constraints gradually,
61 # by defining each of their components.
62 # We start with the constant numerals 0 and 1:
63 zero = solver.mkReal(0);
64 one = solver.mkReal(1);
65
66 # Next, we construct the term x + y
67 xPlusY = solver.mkTerm(Kind.ADD, x, y);
68
69 # Now we can define the constraints.
70 # They use the operators +, <=, and <.
71 # In the API, these are denoted by Plus, Leq, and Lt.
72 constraint1 = solver.mkTerm(Kind.LT, zero, x);
73 constraint2 = solver.mkTerm(Kind.LT, zero, y);
74 constraint3 = solver.mkTerm(Kind.LT, xPlusY, one);
75 constraint4 = solver.mkTerm(Kind.LEQ, x, y);
76
77 # Now we assert the constraints to the solver.
78 solver.assertFormula(constraint1);
79 solver.assertFormula(constraint2);
80 solver.assertFormula(constraint3);
81 solver.assertFormula(constraint4);
82
83 # Check if the formula is satisfiable, that is,
84 # are there real values for x and y that satisfy all the constraints?
85 r1 = solver.checkSat();
86
87 # The result is either SAT, UNSAT, or UNKNOWN.
88 # In this case, it is SAT.
89 print("expected: sat")
90 print("result: ", r1)
91
92 # We can get the values for x and y that satisfy the constraints.
93 xVal = solver.getValue(x);
94 yVal = solver.getValue(y);
95
96 # It is also possible to get values for compound terms,
97 # even if those did not appear in the original formula.
98 xMinusY = solver.mkTerm(Kind.SUB, x, y);
99 xMinusYVal = solver.getValue(xMinusY);
100
101 # We can now obtain the values as python values
102 xPy = xVal.getRealValue();
103 yPy = yVal.getRealValue();
104 xMinusYPy = xMinusYVal.getRealValue();
105
106 print("value for x: ", xPy)
107 print("value for y: ", yPy)
108 print("value for x - y: ", xMinusYPy)
109
110 # Another way to independently compute the value of x - y would be
111 # to use the python minus operator instead of asking the solver.
112 # However, for more complex terms,
113 # it is easier to let the solver do the evaluation.
114 xMinusYComputed = xPy - yPy;
115 if xMinusYComputed == xMinusYPy:
116 print("computed correctly")
117 else:
118 print("computed incorrectly")
119
120 # Further, we can convert the values to strings
121 xStr = str(xPy);
122 yStr = str(yPy);
123 xMinusYStr = str(xMinusYPy);
124
125
126 # Next, we will check satisfiability of the same formula,
127 # only this time over integer variables a and b.
128
129 # We start by resetting assertions added to the solver.
130 solver.resetAssertions();
131
132 # Next, we assert the same assertions above with integers.
133 # This time, we inline the construction of terms
134 # to the assertion command.
135 solver.assertFormula(solver.mkTerm(Kind.LT, solver.mkInteger(0), a));
136 solver.assertFormula(solver.mkTerm(Kind.LT, solver.mkInteger(0), b));
137 solver.assertFormula(
138 solver.mkTerm(
139 Kind.LT, solver.mkTerm(Kind.ADD, a, b), solver.mkInteger(1)));
140 solver.assertFormula(solver.mkTerm(Kind.LEQ, a, b));
141
142 # We check whether the revised assertion is satisfiable.
143 r2 = solver.checkSat();
144
145 # This time the formula is unsatisfiable
146 print("expected: unsat")
147 print("result:", r2)
148
149 # We can query the solver for an unsatisfiable core, i.e., a subset
150 # of the assertions that is already unsatisfiable.
151 unsatCore = solver.getUnsatCore();
152 print("unsat core size:", len(unsatCore))
153 print("unsat core:", unsatCore)
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 Solver solver;
28
29 // We will ask the solver to produce models and unsat cores,
30 // hence these options should be turned on.
31 solver.setOption("produce-models", "true");
32 solver.setOption("produce-unsat-cores", "true");
33
34 // The simplest way to set a logic for the solver is to choose "ALL".
35 // This enables all logics in the solver.
36 // Alternatively, "QF_ALL" enables all logics without quantifiers.
37 // To optimize the solver's behavior for a more specific logic,
38 // use the logic name, e.g. "QF_BV" or "QF_AUFBV".
39
40 // Set the logic
41 solver.setLogic("ALL");
42
43 // In this example, we will define constraints over reals and integers.
44 // Hence, we first obtain the corresponding sorts.
45 Sort realSort = solver.getRealSort();
46 Sort intSort = solver.getIntegerSort();
47
48 // x and y will be real variables, while a and b will be integer variables.
49 // Formally, their cpp type is Term,
50 // and they are called "constants" in SMT jargon:
51 Term x = solver.mkConst(realSort, "x");
52 Term y = solver.mkConst(realSort, "y");
53 Term a = solver.mkConst(intSort, "a");
54 Term b = solver.mkConst(intSort, "b");
55
56 // Our constraints regarding x and y will be:
57 //
58 // (1) 0 < x
59 // (2) 0 < y
60 // (3) x + y < 1
61 // (4) x <= y
62 //
63
64 // Formally, constraints are also terms. Their sort is Boolean.
65 // We will construct these constraints gradually,
66 // by defining each of their components.
67 // We start with the constant numerals 0 and 1:
68 Term zero = solver.mkReal(0);
69 Term one = solver.mkReal(1);
70
71 // Next, we construct the term x + y
72 Term xPlusY = solver.mkTerm(ADD, {x, y});
73
74 // Now we can define the constraints.
75 // They use the operators +, <=, and <.
76 // In the API, these are denoted by ADD, LEQ, and LT.
77 // A list of available operators is available in:
78 // src/api/cpp/cvc5_kind.h
79 Term constraint1 = solver.mkTerm(LT, {zero, x});
80 Term constraint2 = solver.mkTerm(LT, {zero, y});
81 Term constraint3 = solver.mkTerm(LT, {xPlusY, one});
82 Term constraint4 = solver.mkTerm(LEQ, {x, y});
83
84 // Now we assert the constraints to the solver.
85 solver.assertFormula(constraint1);
86 solver.assertFormula(constraint2);
87 solver.assertFormula(constraint3);
88 solver.assertFormula(constraint4);
89
90 // Check if the formula is satisfiable, that is,
91 // are there real values for x and y that satisfy all the constraints?
92 Result r1 = solver.checkSat();
93
94 // The result is either SAT, UNSAT, or UNKNOWN.
95 // In this case, it is SAT.
96 std::cout << "expected: sat" << std::endl;
97 std::cout << "result: " << r1 << std::endl;
98
99 // We can get the values for x and y that satisfy the constraints.
100 Term xVal = solver.getValue(x);
101 Term yVal = solver.getValue(y);
102
103 // It is also possible to get values for compound terms,
104 // even if those did not appear in the original formula.
105 Term xMinusY = solver.mkTerm(SUB, {x, y});
106 Term xMinusYVal = solver.getValue(xMinusY);
107
108 // We can now obtain the string representations of the values.
109 std::string xStr = xVal.getRealValue();
110 std::string yStr = yVal.getRealValue();
111 std::string xMinusYStr = xMinusYVal.getRealValue();
112
113 std::cout << "value for x: " << xStr << std::endl;
114 std::cout << "value for y: " << yStr << std::endl;
115 std::cout << "value for x - y: " << xMinusYStr << std::endl;
116
117 // Further, we can convert the values to cpp types
118 std::pair<int64_t, uint64_t> xPair = xVal.getReal64Value();
119 std::pair<int64_t, uint64_t> yPair = yVal.getReal64Value();
120 std::pair<int64_t, uint64_t> xMinusYPair = xMinusYVal.getReal64Value();
121
122 std::cout << "value for x: " << xPair.first << "/" << xPair.second << std::endl;
123 std::cout << "value for y: " << yPair.first << "/" << yPair.second << std::endl;
124 std::cout << "value for x - y: " << xMinusYPair.first << "/" << xMinusYPair.second << std::endl;
125
126 // Another way to independently compute the value of x - y would be
127 // to perform the (rational) arithmetic manually.
128 // However, for more complex terms,
129 // it is easier to let the solver do the evaluation.
130 std::pair<int64_t, uint64_t> xMinusYComputed = {
131 xPair.first * yPair.second - xPair.second * yPair.first,
132 xPair.second * yPair.second
133 };
134 uint64_t g = std::gcd(xMinusYComputed.first, xMinusYComputed.second);
135 xMinusYComputed = { xMinusYComputed.first / g, xMinusYComputed.second / g };
136 if (xMinusYComputed == xMinusYPair)
137 {
138 std::cout << "computed correctly" << std::endl;
139 }
140 else
141 {
142 std::cout << "computed incorrectly" << std::endl;
143 }
144
145 // Next, we will check satisfiability of the same formula,
146 // only this time over integer variables a and b.
147
148 // We start by resetting assertions added to the solver.
149 solver.resetAssertions();
150
151 // Next, we assert the same assertions above with integers.
152 // This time, we inline the construction of terms
153 // to the assertion command.
154 solver.assertFormula(solver.mkTerm(LT, {solver.mkInteger(0), a}));
155 solver.assertFormula(solver.mkTerm(LT, {solver.mkInteger(0), b}));
156 solver.assertFormula(
157 solver.mkTerm(LT, {solver.mkTerm(ADD, {a, b}), solver.mkInteger(1)}));
158 solver.assertFormula(solver.mkTerm(LEQ, {a, b}));
159
160 // We check whether the revised assertion is satisfiable.
161 Result r2 = solver.checkSat();
162
163 // This time the formula is unsatisfiable
164 std::cout << "expected: unsat" << std::endl;
165 std::cout << "result: " << r2 << std::endl;
166
167 // We can query the solver for an unsatisfiable core, i.e., a subset
168 // of the assertions that is already unsatisfiable.
169 std::vector<Term> unsatCore = solver.getUnsatCore();
170 std::cout << "unsat core size: " << unsatCore.size() << std::endl;
171 std::cout << "unsat core: " << std::endl;
172 for (const Term& t : unsatCore)
173 {
174 std::cout << t << std::endl;
175 }
176
177 return 0;
178 }
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 solver.setOption("produce-models", "true");
33 solver.setOption("produce-unsat-cores", "true");
34
35 // The simplest way to set a logic for the solver is to choose "ALL".
36 // This enables all logics in the solver.
37 // Alternatively, "QF_ALL" enables all logics without quantifiers.
38 // To optimize the solver's behavior for a more specific logic,
39 // use the logic name, e.g. "QF_BV" or "QF_AUFBV".
40
41 // Set the logic
42 solver.setLogic("ALL");
43
44 // In this example, we will define constraints over reals and integers.
45 // Hence, we first obtain the corresponding sorts.
46 Sort realSort = solver.getRealSort();
47 Sort intSort = solver.getIntegerSort();
48
49 // x and y will be real variables, while a and b will be integer variables.
50 // Formally, their cpp type is Term,
51 // and they are called "constants" in SMT jargon:
52 Term x = solver.mkConst(realSort, "x");
53 Term y = solver.mkConst(realSort, "y");
54 Term a = solver.mkConst(intSort, "a");
55 Term b = solver.mkConst(intSort, "b");
56
57 // Our constraints regarding x and y will be:
58 //
59 // (1) 0 < x
60 // (2) 0 < y
61 // (3) x + y < 1
62 // (4) x <= y
63 //
64
65 // Formally, constraints are also terms. Their sort is Boolean.
66 // We will construct these constraints gradually,
67 // by defining each of their components.
68 // We start with the constant numerals 0 and 1:
69 Term zero = solver.mkReal(0);
70 Term one = solver.mkReal(1);
71
72 // Next, we construct the term x + y
73 Term xPlusY = solver.mkTerm(Kind.ADD, x, y);
74
75 // Now we can define the constraints.
76 // They use the operators +, <=, and <.
77 // In the API, these are denoted by ADD, LEQ, and LT.
78 // A list of available operators is available in:
79 // src/api/cpp/cvc5_kind.h
80 Term constraint1 = solver.mkTerm(Kind.LT, zero, x);
81 Term constraint2 = solver.mkTerm(Kind.LT, zero, y);
82 Term constraint3 = solver.mkTerm(Kind.LT, xPlusY, one);
83 Term constraint4 = solver.mkTerm(Kind.LEQ, x, y);
84
85 // Now we assert the constraints to the solver.
86 solver.assertFormula(constraint1);
87 solver.assertFormula(constraint2);
88 solver.assertFormula(constraint3);
89 solver.assertFormula(constraint4);
90
91 // Check if the formula is satisfiable, that is,
92 // are there real values for x and y that satisfy all the constraints?
93 Result r1 = solver.checkSat();
94
95 // The result is either SAT, UNSAT, or UNKNOWN.
96 // In this case, it is SAT.
97 System.out.println("expected: sat");
98 System.out.println("result: " + r1);
99
100 // We can get the values for x and y that satisfy the constraints.
101 Term xVal = solver.getValue(x);
102 Term yVal = solver.getValue(y);
103
104 // It is also possible to get values for compound terms,
105 // even if those did not appear in the original formula.
106 Term xMinusY = solver.mkTerm(Kind.SUB, x, y);
107 Term xMinusYVal = solver.getValue(xMinusY);
108
109 // Further, we can convert the values to java types
110 Pair<BigInteger, BigInteger> xPair = xVal.getRealValue();
111 Pair<BigInteger, BigInteger> yPair = yVal.getRealValue();
112 Pair<BigInteger, BigInteger> xMinusYPair = xMinusYVal.getRealValue();
113
114 System.out.println("value for x: " + xPair.first + "/" + xPair.second);
115 System.out.println("value for y: " + yPair.first + "/" + yPair.second);
116 System.out.println("value for x - y: " + xMinusYPair.first + "/" + xMinusYPair.second);
117
118 // Another way to independently compute the value of x - y would be
119 // to perform the (rational) arithmetic manually.
120 // However, for more complex terms,
121 // it is easier to let the solver do the evaluation.
122 Pair<BigInteger, BigInteger> xMinusYComputed =
123 new Pair(xPair.first.multiply(yPair.second).subtract(xPair.second.multiply(yPair.first)),
124 xPair.second.multiply(yPair.second));
125 BigInteger g = xMinusYComputed.first.gcd(xMinusYComputed.second);
126 xMinusYComputed = new Pair(xMinusYComputed.first.divide(g), xMinusYComputed.second.divide(g));
127 if (xMinusYComputed.equals(xMinusYPair))
128 {
129 System.out.println("computed correctly");
130 }
131 else
132 {
133 System.out.println("computed incorrectly");
134 }
135
136 // Next, we will check satisfiability of the same formula,
137 // only this time over integer variables a and b.
138
139 // We start by resetting assertions added to the solver.
140 solver.resetAssertions();
141
142 // Next, we assert the same assertions above with integers.
143 // This time, we inline the construction of terms
144 // to the assertion command.
145 solver.assertFormula(solver.mkTerm(Kind.LT, solver.mkInteger(0), a));
146 solver.assertFormula(solver.mkTerm(Kind.LT, solver.mkInteger(0), b));
147 solver.assertFormula(
148 solver.mkTerm(Kind.LT, solver.mkTerm(Kind.ADD, a, b), solver.mkInteger(1)));
149 solver.assertFormula(solver.mkTerm(Kind.LEQ, a, b));
150
151 // We check whether the revised assertion is satisfiable.
152 Result r2 = solver.checkSat();
153
154 // This time the formula is unsatisfiable
155 System.out.println("expected: unsat");
156 System.out.println("result: " + r2);
157
158 // We can query the solver for an unsatisfiable core, i.e., a subset
159 // of the assertions that is already unsatisfiable.
160 List<Term> unsatCore = Arrays.asList(solver.getUnsatCore());
161 System.out.println("unsat core size: " + unsatCore.size());
162 System.out.println("unsat core: ");
163 for (Term t : unsatCore)
164 {
165 System.out.println(t);
166 }
167 }
168 }
169 }
examples/api/python/pythonic/quickstart.py
1 from cvc5.pythonic 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/smtlib/quickstart.smt2
1 (set-logic ALL)
2 (set-option :produce-models true)
3 (set-option :incremental true)
4 ; print unsat cores, include assertions in the unsat core that have not been named
5 (set-option :produce-unsat-cores true)
6 (set-option :dump-unsat-cores-full true)
7
8 ; Declare real constants x,y
9 (declare-const x Real)
10 (declare-const y Real)
11
12 ; Our constraints regarding x and y will be:
13 ;
14 ; (1) 0 < x
15 ; (2) 0 < y
16 ; (3) x + y < 1
17 ; (4) x <= y
18
19 (assert (< 0 x))
20 (assert (< 0 y))
21 (assert (< (+ x y) 1))
22 (assert (<= x y))
23
24 (check-sat)
25 (echo "Values of declared real constants and of compound terms built with them.")
26 (get-value (x y (- x y)))
27
28 (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.")
29 (reset-assertions)
30 ; Declare integer constants a,b
31 (declare-const a Int)
32 (declare-const b Int)
33 (assert (< 0 a))
34 (assert (< 0 b))
35 (assert (< (+ a b) 1))
36 (assert (<= a b))
37
38 (check-sat)
39 (get-unsat-core)