Quickstart Guide
First, create a cvc5 term manager instance:
tm = cvc5.TermManager()
Then, create a cvc5 solver instance:
solver = cvc5.Solver(tm)
We will ask the solver to produce models and unsat cores in the following, and for this 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 constraints of reals and integers. For this, we first query the solver for the corresponding sorts.
realSort = tm.getRealSort()
intSort = tm.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, but not actual values.
x = tm.mkConst(realSort, "x")
y = tm.mkConst(realSort, "y")
a = tm.mkConst(intSort, "a")
b = tm.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:
zero = tm.mkReal(0)
one = tm.mkReal(1)
# Next, we construct the term x + y
xPlusY = tm.mkTerm(Kind.ADD, x, y)
# Now we can define the constraints.
# They use the operators +, <=, and <.
# In the API, these are denoted by Plus, Leq, and Lt.
constraint1 = tm.mkTerm(Kind.LT, zero, x)
constraint2 = tm.mkTerm(Kind.LT, zero, y)
constraint3 = tm.mkTerm(Kind.LT, xPlusY, one)
constraint4 = tm.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.
r1 = solver.checkSat()
The result we get from this satisfiability check is either sat, unsat
or unknown.
It’s status can be queried via isSat, isUnsat and isSatUnknown functions.
Alternatively, it can also be printed.
print("expected: sat")
print("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.
xVal = solver.getValue(x)
yVal = solver.getValue(y)
It is also possible to get values for terms that do not appear in the original formula.
xMinusY = tm.mkTerm(Kind.SUB, x, y)
xMinusYVal = solver.getValue(xMinusY)
We can retrieve the Python representation of these values as follows.
xPy = xVal.getRealValue()
yPy = yVal.getRealValue()
xMinusYPy = xMinusYVal.getRealValue()
print("value for x: ", xPy)
print("value for y: ", yPy)
print("value for x - y: ", xMinusYPy)
This will print the following:
value for x: 1/6
value for y: 1/6
value for x - y: 0
Another way to independently compute the value of x - y would be to
use the Python minus operator instead of asking the solver.
However, for more complex terms, it is easier to let the solver do the
evaluation.
xMinusYComputed = xPy - yPy
if xMinusYComputed == xMinusYPy:
print("computed correctly")
else:
print("computed incorrectly")
This will print:
computed correctly
Further, we can convert these values to strings:
xStr = str(xPy)
yStr = str(yPy)
xMinusYStr = str(xMinusYPy)
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 to the assertion command.
solver.assertFormula(tm.mkTerm(Kind.LT, tm.mkInteger(0), a))
solver.assertFormula(tm.mkTerm(Kind.LT, tm.mkInteger(0), b))
solver.assertFormula(
tm.mkTerm(
Kind.LT, tm.mkTerm(Kind.ADD, a, b), tm.mkInteger(1)))
solver.assertFormula(tm.mkTerm(Kind.LEQ, a, b))
Now, we check whether the revised assertion is satisfiable.
r2 = solver.checkSat()
print("expected: unsat")
print("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.
unsatCore = solver.getUnsatCore()
print("unsat core size:", len(unsatCore))
print("unsat core:", unsatCore)
This will print:
unsat core size: 3
unsat core: [(< 0 a), (< 0 b), (< (+ a b) 1)]
Example
examples/api/python/quickstart.py
1#!/usr/bin/env python
2###############################################################################
3# This file is part of the cvc5 project.
4#
5# Copyright (c) 2009-2026 by the authors listed in the file AUTHORS
6# in the top-level source directory and their institutional affiliations.
7# All rights reserved. See the file COPYING in the top-level source
8# directory for licensing information.
9# #############################################################################
10#
11# A simple demonstration of the api capabilities of cvc5, adapted from quickstart.cpp
12##
13
14import cvc5
15from cvc5 import Kind
16
17if __name__ == "__main__":
18 # Create a term manager
19 #! [docs-python-quickstart-0 start]
20 tm = cvc5.TermManager()
21 #! [docs-python-quickstart-0 end]
22 # Create a solver
23 #! [docs-python-quickstart-1 start]
24 solver = cvc5.Solver(tm)
25 #! [docs-python-quickstart-1 end]
26
27 # We will ask the solver to produce models and unsat cores,
28 # hence these options should be turned on.
29 #! [docs-python-quickstart-2 start]
30 solver.setOption("produce-models", "true")
31 solver.setOption("produce-unsat-cores", "true")
32 #! [docs-python-quickstart-2 end]
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 #! [docs-python-quickstart-3 start]
42 solver.setLogic("ALL")
43 #! [docs-python-quickstart-3 end]
44
45 # In this example, we will define constraints over reals and integers.
46 # Hence, we first obtain the corresponding sorts.
47 #! [docs-python-quickstart-4 start]
48 realSort = tm.getRealSort()
49 intSort = tm.getIntegerSort()
50 #! [docs-python-quickstart-4 end]
51
52 # x and y will be real variables, while a and b will be integer variables.
53 # Formally, their python type is Term,
54 # and they are called "constants" in SMT jargon:
55 #! [docs-python-quickstart-5 start]
56 x = tm.mkConst(realSort, "x")
57 y = tm.mkConst(realSort, "y")
58 a = tm.mkConst(intSort, "a")
59 b = tm.mkConst(intSort, "b")
60 #! [docs-python-quickstart-5 end]
61
62 # Our constraints regarding x and y will be:
63 #
64 # (1) 0 < x
65 # (2) 0 < y
66 # (3) x + y < 1
67 # (4) x <= y
68 #
69
70 #! [docs-python-quickstart-6 start]
71 # Formally, constraints are also terms. Their sort is Boolean.
72 # We will construct these constraints gradually,
73 # by defining each of their components.
74 # We start with the constant numerals 0 and 1:
75 zero = tm.mkReal(0)
76 one = tm.mkReal(1)
77
78 # Next, we construct the term x + y
79 xPlusY = tm.mkTerm(Kind.ADD, x, y)
80
81 # Now we can define the constraints.
82 # They use the operators +, <=, and <.
83 # In the API, these are denoted by Plus, Leq, and Lt.
84 constraint1 = tm.mkTerm(Kind.LT, zero, x)
85 constraint2 = tm.mkTerm(Kind.LT, zero, y)
86 constraint3 = tm.mkTerm(Kind.LT, xPlusY, one)
87 constraint4 = tm.mkTerm(Kind.LEQ, x, y)
88
89 # Now we assert the constraints to the solver.
90 solver.assertFormula(constraint1)
91 solver.assertFormula(constraint2)
92 solver.assertFormula(constraint3)
93 solver.assertFormula(constraint4)
94 #! [docs-python-quickstart-6 end]
95
96 # Check if the formula is satisfiable, that is,
97 # are there real values for x and y that satisfy all the constraints?
98 #! [docs-python-quickstart-7 start]
99 r1 = solver.checkSat()
100 #! [docs-python-quickstart-7 end]
101
102 # The result is either SAT, UNSAT, or UNKNOWN.
103 # In this case, it is SAT.
104 #! [docs-python-quickstart-8 start]
105 print("expected: sat")
106 print("result: ", r1)
107 #! [docs-python-quickstart-8 end]
108
109 # We can get the values for x and y that satisfy the constraints.
110 #! [docs-python-quickstart-9 start]
111 xVal = solver.getValue(x)
112 yVal = solver.getValue(y)
113 #! [docs-python-quickstart-9 end]
114
115 # It is also possible to get values for compound terms,
116 # even if those did not appear in the original formula.
117 #! [docs-python-quickstart-10 start]
118 xMinusY = tm.mkTerm(Kind.SUB, x, y)
119 xMinusYVal = solver.getValue(xMinusY)
120 #! [docs-python-quickstart-10 end]
121
122 # We can now obtain the values as python values
123 #! [docs-python-quickstart-11 start]
124 xPy = xVal.getRealValue()
125 yPy = yVal.getRealValue()
126 xMinusYPy = xMinusYVal.getRealValue()
127
128 print("value for x: ", xPy)
129 print("value for y: ", yPy)
130 print("value for x - y: ", xMinusYPy)
131 #! [docs-python-quickstart-11 end]
132
133 # Another way to independently compute the value of x - y would be
134 # to use the python minus operator instead of asking the solver.
135 # However, for more complex terms,
136 # it is easier to let the solver do the evaluation.
137 #! [docs-python-quickstart-12 start]
138 xMinusYComputed = xPy - yPy
139 if xMinusYComputed == xMinusYPy:
140 print("computed correctly")
141 else:
142 print("computed incorrectly")
143 #! [docs-python-quickstart-12 end]
144
145 # Further, we can convert the values to strings
146 #! [docs-python-quickstart-13 start]
147 xStr = str(xPy)
148 yStr = str(yPy)
149 xMinusYStr = str(xMinusYPy)
150 #! [docs-python-quickstart-13 end]
151
152 # Next, we will check satisfiability of the same formula,
153 # only this time over integer variables a and b.
154
155 # We start by resetting assertions added to the solver.
156 #! [docs-python-quickstart-14 start]
157 solver.resetAssertions()
158 #! [docs-python-quickstart-14 end]
159
160 # Next, we assert the same assertions above with integers.
161 # This time, we inline the construction of terms
162 # to the assertion command.
163 #! [docs-python-quickstart-15 start]
164 solver.assertFormula(tm.mkTerm(Kind.LT, tm.mkInteger(0), a))
165 solver.assertFormula(tm.mkTerm(Kind.LT, tm.mkInteger(0), b))
166 solver.assertFormula(
167 tm.mkTerm(
168 Kind.LT, tm.mkTerm(Kind.ADD, a, b), tm.mkInteger(1)))
169 solver.assertFormula(tm.mkTerm(Kind.LEQ, a, b))
170 #! [docs-python-quickstart-15 end]
171
172 # We check whether the revised assertion is satisfiable.
173 #! [docs-python-quickstart-16 start]
174 r2 = solver.checkSat()
175 #! [docs-python-quickstart-16 end]
176
177 # This time the formula is unsatisfiable
178 #! [docs-python-quickstart-17 start]
179 print("expected: unsat")
180 print("result:", r2)
181 #! [docs-python-quickstart-17 end]
182
183 # We can query the solver for an unsatisfiable core, i.e., a subset
184 # of the assertions that is already unsatisfiable.
185 #! [docs-python-quickstart-18 start]
186 unsatCore = solver.getUnsatCore()
187 print("unsat core size:", len(unsatCore))
188 print("unsat core:", unsatCore)
189 #! [docs-python-quickstart-18 end]
examples/api/cpp/quickstart.cpp
1/******************************************************************************
2 * This file is part of the cvc5 project.
3 *
4 * Copyright (c) 2009-2026 by the authors listed in the file AUTHORS
5 * in the top-level source directory and their institutional affiliations.
6 * All rights reserved. See the file COPYING in the top-level source
7 * directory for licensing information.
8 * ****************************************************************************
9 *
10 * A simple demonstration of the API capabilities of cvc5.
11 *
12 */
13
14#include <cvc5/cvc5.h>
15
16#include <iostream>
17#include <numeric>
18
19using namespace cvc5;
20
21int main()
22{
23 // Create a term manager
24 //! [docs-cpp-quickstart-0 start]
25 TermManager tm;
26 //! [docs-cpp-quickstart-0 end]
27 // Create a solver
28 //! [docs-cpp-quickstart-1 start]
29 Solver solver(tm);
30 //! [docs-cpp-quickstart-1 end]
31
32 // We will ask the solver to produce models and unsat cores,
33 // hence these options should be turned on.
34 //! [docs-cpp-quickstart-2 start]
35 solver.setOption("produce-models", "true");
36 solver.setOption("produce-unsat-cores", "true");
37 //! [docs-cpp-quickstart-2 end]
38
39 // The simplest way to set a logic for the solver is to choose "ALL".
40 // This enables all logics in the solver.
41 // Alternatively, "QF_ALL" enables all logics without quantifiers.
42 // To optimize the solver's behavior for a more specific logic,
43 // use the logic name, e.g. "QF_BV" or "QF_AUFBV".
44
45 // Set the logic
46 //! [docs-cpp-quickstart-3 start]
47 solver.setLogic("ALL");
48 //! [docs-cpp-quickstart-3 end]
49
50 // In this example, we will define constraints over reals and integers.
51 // Hence, we first obtain the corresponding sorts.
52 //! [docs-cpp-quickstart-4 start]
53 Sort realSort = tm.getRealSort();
54 Sort intSort = tm.getIntegerSort();
55 //! [docs-cpp-quickstart-4 end]
56
57 // x and y will be real variables, while a and b will be integer variables.
58 // Formally, their cpp type is Term,
59 // and they are called "constants" in SMT jargon:
60 //! [docs-cpp-quickstart-5 start]
61 Term x = tm.mkConst(realSort, "x");
62 Term y = tm.mkConst(realSort, "y");
63 Term a = tm.mkConst(intSort, "a");
64 Term b = tm.mkConst(intSort, "b");
65 //! [docs-cpp-quickstart-5 end]
66
67 // Our constraints regarding x and y will be:
68 //
69 // (1) 0 < x
70 // (2) 0 < y
71 // (3) x + y < 1
72 // (4) x <= y
73 //
74
75 //! [docs-cpp-quickstart-6 start]
76 // Formally, constraints are also terms. Their sort is Boolean.
77 // We will construct these constraints gradually,
78 // by defining each of their components.
79 // We start with the constant numerals 0 and 1:
80 Term zero = tm.mkReal(0);
81 Term one = tm.mkReal(1);
82
83 // Next, we construct the term x + y
84 Term xPlusY = tm.mkTerm(Kind::ADD, {x, y});
85
86 // Now we can define the constraints.
87 // They use the operators +, <=, and <.
88 // In the API, these are denoted by ADD, LEQ, and LT.
89 // A list of available operators is available in:
90 // src/api/cpp/cvc5_kind.h
91 Term constraint1 = tm.mkTerm(Kind::LT, {zero, x});
92 Term constraint2 = tm.mkTerm(Kind::LT, {zero, y});
93 Term constraint3 = tm.mkTerm(Kind::LT, {xPlusY, one});
94 Term constraint4 = tm.mkTerm(Kind::LEQ, {x, y});
95
96 // Now we assert the constraints to the solver.
97 solver.assertFormula(constraint1);
98 solver.assertFormula(constraint2);
99 solver.assertFormula(constraint3);
100 solver.assertFormula(constraint4);
101 //! [docs-cpp-quickstart-6 end]
102
103 // Check if the formula is satisfiable, that is,
104 // are there real values for x and y that satisfy all the constraints?
105 //! [docs-cpp-quickstart-7 start]
106 Result r1 = solver.checkSat();
107 //! [docs-cpp-quickstart-7 end]
108
109 // The result is either SAT, UNSAT, or UNKNOWN.
110 // In this case, it is SAT.
111 //! [docs-cpp-quickstart-8 start]
112 std::cout << "expected: sat" << std::endl;
113 std::cout << "result: " << r1 << std::endl;
114 //! [docs-cpp-quickstart-8 end]
115
116 // We can get the values for x and y that satisfy the constraints.
117 //! [docs-cpp-quickstart-9 start]
118 Term xVal = solver.getValue(x);
119 Term yVal = solver.getValue(y);
120 //! [docs-cpp-quickstart-9 end]
121
122 // It is also possible to get values for compound terms,
123 // even if those did not appear in the original formula.
124 //! [docs-cpp-quickstart-10 start]
125 Term xMinusY = tm.mkTerm(Kind::SUB, {x, y});
126 Term xMinusYVal = solver.getValue(xMinusY);
127 //! [docs-cpp-quickstart-10 end]
128
129 // We can now obtain the string representations of the values.
130 //! [docs-cpp-quickstart-11 start]
131 std::string xStr = xVal.getRealValue();
132 std::string yStr = yVal.getRealValue();
133 std::string xMinusYStr = xMinusYVal.getRealValue();
134
135 std::cout << "value for x: " << xStr << std::endl;
136 std::cout << "value for y: " << yStr << std::endl;
137 std::cout << "value for x - y: " << xMinusYStr << std::endl;
138 //! [docs-cpp-quickstart-11 end]
139
140 //! [docs-cpp-quickstart-12 start]
141 // Further, we can convert the values to cpp types
142 std::pair<int64_t, uint64_t> xPair = xVal.getReal64Value();
143 std::pair<int64_t, uint64_t> yPair = yVal.getReal64Value();
144 std::pair<int64_t, uint64_t> xMinusYPair = xMinusYVal.getReal64Value();
145
146 std::cout << "value for x: " << xPair.first << "/" << xPair.second
147 << std::endl;
148 std::cout << "value for y: " << yPair.first << "/" << yPair.second
149 << std::endl;
150 std::cout << "value for x - y: " << xMinusYPair.first << "/"
151 << xMinusYPair.second << std::endl;
152 //! [docs-cpp-quickstart-12 end]
153
154 // Another way to independently compute the value of x - y would be
155 // to perform the (rational) arithmetic manually.
156 // However, for more complex terms,
157 // it is easier to let the solver do the evaluation.
158 //! [docs-cpp-quickstart-13 start]
159 std::pair<int64_t, uint64_t> xMinusYComputed = {
160 xPair.first * yPair.second - xPair.second * yPair.first,
161 xPair.second * yPair.second
162 };
163 uint64_t g = std::gcd(xMinusYComputed.first, xMinusYComputed.second);
164 xMinusYComputed = { xMinusYComputed.first / g, xMinusYComputed.second / g };
165 if (xMinusYComputed == xMinusYPair)
166 {
167 std::cout << "computed correctly" << std::endl;
168 }
169 else
170 {
171 std::cout << "computed incorrectly" << std::endl;
172 }
173 //! [docs-cpp-quickstart-13 end]
174
175 // Next, we will check satisfiability of the same formula,
176 // only this time over integer variables a and b.
177
178 // We start by resetting assertions added to the solver.
179 //! [docs-cpp-quickstart-14 start]
180 solver.resetAssertions();
181 //! [docs-cpp-quickstart-14 end]
182
183 // Next, we assert the same assertions above with integers.
184 // This time, we inline the construction of terms
185 // to the assertion command.
186 //! [docs-cpp-quickstart-15 start]
187 solver.assertFormula(tm.mkTerm(Kind::LT, {tm.mkInteger(0), a}));
188 solver.assertFormula(tm.mkTerm(Kind::LT, {tm.mkInteger(0), b}));
189 solver.assertFormula(
190 tm.mkTerm(Kind::LT, {tm.mkTerm(Kind::ADD, {a, b}), tm.mkInteger(1)}));
191 solver.assertFormula(tm.mkTerm(Kind::LEQ, {a, b}));
192 //! [docs-cpp-quickstart-15 end]
193
194 // We check whether the revised assertion is satisfiable.
195 //! [docs-cpp-quickstart-16 start]
196 Result r2 = solver.checkSat();
197 //! [docs-cpp-quickstart-16 end]
198
199 // This time the formula is unsatisfiable
200 //! [docs-cpp-quickstart-17 start]
201 std::cout << "expected: unsat" << std::endl;
202 std::cout << "result: " << r2 << std::endl;
203 //! [docs-cpp-quickstart-17 end]
204
205 // We can query the solver for an unsatisfiable core, i.e., a subset
206 // of the assertions that is already unsatisfiable.
207 //! [docs-cpp-quickstart-18 start]
208 std::vector<Term> unsatCore = solver.getUnsatCore();
209 std::cout << "unsat core size: " << unsatCore.size() << std::endl;
210 std::cout << "unsat core: " << std::endl;
211 for (const Term& t : unsatCore)
212 {
213 std::cout << t << std::endl;
214 }
215 //! [docs-cpp-quickstart-18 end]
216
217 return 0;
218}
1/******************************************************************************
2 * This file is part of the cvc5 project.
3 *
4 * Copyright (c) 2009-2026 by the authors listed in the file AUTHORS
5 * in the top-level source directory and their institutional affiliations.
6 * All rights reserved. See the file COPYING in the top-level source
7 * directory for licensing information.
8 * ****************************************************************************
9 *
10 * A simple demonstration of the API capabilities of cvc5.
11 *
12 */
13
14#include <cvc5/c/cvc5.h>
15#include <stdio.h>
16#include <stdlib.h>
17#include <string.h>
18#include <inttypes.h>
19
20int32_t gcd(int32_t a, int32_t b)
21{
22 int32_t remainder = a % b;
23
24 if (remainder == 0)
25 {
26 return b;
27 }
28
29 return gcd(b, remainder);
30}
31
32int main()
33{
34 // Create a term manager
35 //! [docs-c-quickstart-0 start]
36 Cvc5TermManager* tm = cvc5_term_manager_new();
37 //! [docs-c-quickstart-0 end]
38 // Create a solver
39 //! [docs-c-quickstart-1 start]
40 Cvc5* slv = cvc5_new(tm);
41 //! [docs-c-quickstart-1 end]
42
43 // We will ask the solver to produce models and unsat cores,
44 // hence these options should be turned on.
45 //! [docs-c-quickstart-2 start]
46 cvc5_set_option(slv, "produce-models", "true");
47 cvc5_set_option(slv, "produce-unsat-cores", "true");
48 //! [docs-c-quickstart-2 end]
49
50 // The simplest way to set a logic for the solver is to choose "ALL".
51 // This enables all logics in the solver.
52 // Alternatively, "QF_ALL" enables all logics without quantifiers.
53 // To optimize the solver's behavior for a more specific logic,
54 // use the logic name, e.g. "QF_BV" or "QF_AUFBV".
55
56 // Set the logic
57 //! [docs-c-quickstart-3 start]
58 cvc5_set_logic(slv, "ALL");
59 //! [docs-c-quickstart-3 end]
60
61 // In this example, we will define constraints over reals and integers.
62 // Hence, we first obtain the corresponding sorts.
63 //! [docs-c-quickstart-4 start]
64 Cvc5Sort real_sort = cvc5_get_real_sort(tm);
65 Cvc5Sort int_sort = cvc5_get_integer_sort(tm);
66 //! [docs-c-quickstart-4 end]
67
68 // x and y will be real variables, while a and b will be integer variables.
69 // Formally, their cpp type is Term,
70 // and they are called "constants" in SMT jargon:
71 //! [docs-c-quickstart-5 start]
72 Cvc5Term x = cvc5_mk_const(tm, real_sort, "x");
73 Cvc5Term y = cvc5_mk_const(tm, real_sort, "y");
74 Cvc5Term a = cvc5_mk_const(tm, int_sort, "a");
75 Cvc5Term b = cvc5_mk_const(tm, int_sort, "b");
76 //! [docs-c-quickstart-5 end]
77
78 // Our constraints regarding x and y will be:
79 //
80 // (1) 0 < x
81 // (2) 0 < y
82 // (3) x + y < 1
83 // (4) x <= y
84 //
85
86 //! [docs-c-quickstart-6 start]
87 // Formally, constraints are also terms. Their sort is Boolean.
88 // We will construct these constraints gradually,
89 // by defining each of their components.
90 // We start with the constant numerals 0 and 1:
91 Cvc5Term zero = cvc5_mk_real_int64(tm, 0);
92 Cvc5Term one = cvc5_mk_real_int64(tm, 1);
93
94 // Next, we construct the term x + y
95 Cvc5Term args2[2] = {x, y};
96 Cvc5Term x_plus_y = cvc5_mk_term(tm, CVC5_KIND_ADD, 2, args2);
97
98 // Now we can define the constraints.
99 // They use the operators +, <=, and <.
100 // In the API, these are denoted by ADD, LEQ, and LT.
101 // A list of available operators is available in:
102 // src/api/cpp/cvc5_kind.h
103 args2[0] = zero;
104 args2[1] = x;
105 Cvc5Term constraint1 = cvc5_mk_term(tm, CVC5_KIND_LT, 2, args2);
106 args2[1] = y;
107 Cvc5Term constraint2 = cvc5_mk_term(tm, CVC5_KIND_LT, 2, args2);
108 args2[0] = x_plus_y;
109 args2[1] = one;
110 Cvc5Term constraint3 = cvc5_mk_term(tm, CVC5_KIND_LT, 2, args2);
111 args2[0] = x;
112 args2[1] = y;
113 Cvc5Term constraint4 = cvc5_mk_term(tm, CVC5_KIND_LEQ, 2, args2);
114
115 // Now we assert the constraints to the solver.
116 cvc5_assert_formula(slv, constraint1);
117 cvc5_assert_formula(slv, constraint2);
118 cvc5_assert_formula(slv, constraint3);
119 cvc5_assert_formula(slv, constraint4);
120 //! [docs-c-quickstart-6 end]
121
122 // Check if the formula is satisfiable, that is,
123 // are there real values for x and y that satisfy all the constraints?
124 //! [docs-c-quickstart-7 start]
125 Cvc5Result r = cvc5_check_sat(slv);
126 //! [docs-c-quickstart-7 end]
127
128 // The result is either SAT, UNSAT, or UNKNOWN.
129 // In this case, it is SAT.
130 //! [docs-c-quickstart-8 start]
131 printf("expected: sat\n");
132 printf("result: %s\n", cvc5_result_to_string(r));
133 //! [docs-c-quickstart-8 end]
134
135 // We can get the values for x and y that satisfy the constraints.
136 //! [docs-c-quickstart-9 start]
137 Cvc5Term x_val = cvc5_get_value(slv, x);
138 Cvc5Term y_val = cvc5_get_value(slv, y);
139 //! [docs-c-quickstart-9 end]
140
141 // It is also possible to get values for compound terms,
142 // even if those did not appear in the original formula.
143 //! [docs-c-quickstart-10 start]
144 args2[0] = x;
145 args2[1] = y;
146 Cvc5Term x_minus_y = cvc5_mk_term(tm, CVC5_KIND_SUB, 2, args2);
147 Cvc5Term x_minus_y_val = cvc5_get_value(slv, x_minus_y);
148 //! [docs-c-quickstart-10 end]
149
150 // We can now obtain the string representations of the values.
151 //! [docs-c-quickstart-11 start]
152 // Note: The const char* returned by cvc5_term_get_real_value is only valid
153 // until the next call to this function.
154 char* x_str = strdup(cvc5_term_get_real_value(x_val));
155 char* y_str = strdup(cvc5_term_get_real_value(y_val));
156 char* x_minus_y_str = strdup(cvc5_term_get_real_value(x_minus_y_val));
157
158 printf("value for x: %s\n", x_str);
159 printf("value for y: %s\n", y_str);
160 printf("value for x - y: %s\n", x_minus_y_str);
161
162 free(y_str);
163 free(x_str);
164 free(x_minus_y_str);
165
166 // Alternatively, you can directly print the value strings without
167 // copying them first:
168 printf("value for x: %s\n", cvc5_term_get_real_value(x_val));
169 printf("value for y: %s\n", cvc5_term_get_real_value(y_val));
170 printf("value for x - y: %s\n", cvc5_term_get_real_value(x_minus_y_val));
171 //! [docs-c-quickstart-11 end]
172
173 //! [docs-c-quickstart-12 start]
174 // Further, we can convert the values to cpp types
175 int64_t x_num;
176 uint64_t x_den;
177 cvc5_term_get_real64_value(x_val, &x_num, &x_den);
178 int64_t y_num;
179 uint64_t y_den;
180 cvc5_term_get_real64_value(y_val, &y_num, &y_den);
181 int64_t x_minus_y_num;
182 uint64_t x_minus_y_den;
183 cvc5_term_get_real64_value(x_minus_y_val, &x_minus_y_num, &x_minus_y_den);
184
185 printf("value for x: %" PRId64 "/%" PRIu64 "\n", x_num, x_den);
186 printf("value for y: %" PRId64 "/%" PRIu64 "\n", y_num, y_den);
187 printf("value for x - y: %" PRId64 "/%" PRIu64 "\n", x_minus_y_num, x_minus_y_den);
188 //! [docs-c-quickstart-12 end]
189
190 // Another way to independently compute the value of x - y would be
191 // to perform the (rational) arithmetic manually.
192 // However, for more complex terms,
193 // it is easier to let the solver do the evaluation.
194 //! [docs-c-quickstart-13 start]
195 int64_t x_minus_y_num_computed = x_num * y_den - x_den * y_num;
196 uint64_t x_minus_y_den_computed = x_den * y_den;
197 uint64_t g = gcd(x_minus_y_num_computed, x_minus_y_den_computed);
198 x_minus_y_num_computed = x_minus_y_num_computed / g;
199 x_minus_y_den_computed = x_minus_y_den_computed / g;
200 if (x_minus_y_num_computed == x_minus_y_num
201 && x_minus_y_den_computed == x_minus_y_den)
202 {
203 printf("computed correctly\n");
204 }
205 else
206 {
207 printf("computed incorrectly\n");
208 }
209 //! [docs-c-quickstart-13 end]
210
211 // Next, we will check satisfiability of the same formula,
212 // only this time over integer variables a and b.
213
214 // We start by resetting assertions added to the solver.
215 //! [docs-c-quickstart-14 start]
216 cvc5_reset_assertions(slv);
217 //! [docs-c-quickstart-14 end]
218
219 // Next, we assert the same assertions above with integers.
220 // This time, we inline the construction of terms
221 // to the assertion command.
222 //! [docs-c-quickstart-15 start]
223 args2[0] = cvc5_mk_integer_int64(tm, 0);
224 args2[1] = a;
225 cvc5_assert_formula(slv, cvc5_mk_term(tm, CVC5_KIND_LT, 2, args2));
226 args2[1] = b;
227 cvc5_assert_formula(slv, cvc5_mk_term(tm, CVC5_KIND_LT, 2, args2));
228 args2[0] = a;
229 args2[1] = b;
230 Cvc5Term add = cvc5_mk_term(tm, CVC5_KIND_ADD, 2, args2);
231 args2[0] = add;
232 args2[1] = cvc5_mk_integer_int64(tm, 1);
233 cvc5_assert_formula(slv, cvc5_mk_term(tm, CVC5_KIND_LT, 2, args2));
234 args2[0] = a;
235 args2[1] = b;
236 cvc5_assert_formula(slv, cvc5_mk_term(tm, CVC5_KIND_LEQ, 2, args2));
237 //! [docs-c-quickstart-15 end]
238
239 // We check whether the revised assertion is satisfiable.
240 //! [docs-c-quickstart-16 start]
241 cvc5_result_release(r); // optional, not needed anymore so we can release
242 r = cvc5_check_sat(slv);
243 //! [docs-c-quickstart-16 end]
244
245 // This time the formula is unsatisfiable
246 //! [docs-c-quickstart-17 start]
247 printf("expected: unsat\n");
248 printf("result: %s\n", cvc5_result_to_string(r));
249 //! [docs-c-quickstart-17 end]
250
251 // We can query the solver for an unsatisfiable core, i.e., a subset
252 // of the assertions that is already unsatisfiable.
253 //! [docs-c-quickstart-18 start]
254 size_t size;
255 const Cvc5Term* unsat_core = cvc5_get_unsat_core(slv, &size);
256 printf("unsat core size: %zu\n", size);
257 printf("unsat core: \n");
258 for (size_t i = 0; i < size; i++)
259 {
260 printf("%s\n", cvc5_term_to_string(unsat_core[i]));
261 }
262 //! [docs-c-quickstart-18 end]
263
264 // Delete solver instance.
265 //! [docs-c-quickstart-19 start]
266 cvc5_delete(slv);
267 //! [docs-c-quickstart-19 end]
268
269 // Delete term manager instance.
270 //! [docs-c-quickstart-20 start]
271 cvc5_term_manager_delete(tm);
272 //! [docs-c-quickstart-20 end]
273 return 0;
274}
examples/api/java/QuickStart.java
1/******************************************************************************
2 * This file is part of the cvc5 project.
3 *
4 * Copyright (c) 2009-2026 by the authors listed in the file AUTHORS
5 * in the top-level source directory and their institutional affiliations.
6 * All rights reserved. See the file COPYING in the top-level source
7 * directory for licensing information.
8 * ****************************************************************************
9 *
10 * A simple demonstration of the api capabilities of cvc5.
11 *
12 */
13
14import io.github.cvc5.*;
15import java.math.BigInteger;
16import java.util.ArrayList;
17import java.util.Arrays;
18import java.util.List;
19
20public class QuickStart
21{
22 public static void main(String args[]) throws CVC5ApiException
23 {
24 // Create a term manager
25 //! [docs-java-quickstart-0 start]
26 TermManager tm = new TermManager();
27 //! [docs-java-quickstart-0 end]
28 // Create a solver
29 //! [docs-java-quickstart-1 start]
30 Solver solver = new Solver(tm);
31 //! [docs-java-quickstart-1 end]
32 {
33 // We will ask the solver to produce models and unsat cores,
34 // hence these options should be turned on.
35 //! [docs-java-quickstart-2 start]
36 solver.setOption("produce-models", "true");
37 solver.setOption("produce-unsat-cores", "true");
38 //! [docs-java-quickstart-2 end]
39
40 // The simplest way to set a logic for the solver is to choose "ALL".
41 // This enables all logics in the solver.
42 // Alternatively, "QF_ALL" enables all logics without quantifiers.
43 // To optimize the solver's behavior for a more specific logic,
44 // use the logic name, e.g. "QF_BV" or "QF_AUFBV".
45
46 // Set the logic
47 //! [docs-java-quickstart-3 start]
48 solver.setLogic("ALL");
49 //! [docs-java-quickstart-3 end]
50
51 // In this example, we will define constraints over reals and integers.
52 // Hence, we first obtain the corresponding sorts.
53 //! [docs-java-quickstart-4 start]
54 Sort realSort = tm.getRealSort();
55 Sort intSort = tm.getIntegerSort();
56 //! [docs-java-quickstart-4 end]
57
58 // x and y will be real variables, while a and b will be integer variables.
59 // Formally, their cpp type is Term,
60 // and they are called "constants" in SMT jargon:
61 //! [docs-java-quickstart-5 start]
62 Term x = tm.mkConst(realSort, "x");
63 Term y = tm.mkConst(realSort, "y");
64 Term a = tm.mkConst(intSort, "a");
65 Term b = tm.mkConst(intSort, "b");
66 //! [docs-java-quickstart-5 end]
67
68 // Our constraints regarding x and y will be:
69 //
70 // (1) 0 < x
71 // (2) 0 < y
72 // (3) x + y < 1
73 // (4) x <= y
74 //
75
76 //! [docs-java-quickstart-6 start]
77 // Formally, constraints are also terms. Their sort is Boolean.
78 // We will construct these constraints gradually,
79 // by defining each of their components.
80 // We start with the constant numerals 0 and 1:
81 Term zero = tm.mkReal(0);
82 Term one = tm.mkReal(1);
83
84 // Next, we construct the term x + y
85 Term xPlusY = tm.mkTerm(Kind.ADD, x, y);
86
87 // Now we can define the constraints.
88 // They use the operators +, <=, and <.
89 // In the API, these are denoted by ADD, LEQ, and LT.
90 // A list of available operators is available in:
91 // src/api/cpp/cvc5_kind.h
92 Term constraint1 = tm.mkTerm(Kind.LT, zero, x);
93 Term constraint2 = tm.mkTerm(Kind.LT, zero, y);
94 Term constraint3 = tm.mkTerm(Kind.LT, xPlusY, one);
95 Term constraint4 = tm.mkTerm(Kind.LEQ, x, y);
96
97 // Now we assert the constraints to the solver.
98 solver.assertFormula(constraint1);
99 solver.assertFormula(constraint2);
100 solver.assertFormula(constraint3);
101 solver.assertFormula(constraint4);
102 //! [docs-java-quickstart-6 end]
103
104 // Check if the formula is satisfiable, that is,
105 // are there real values for x and y that satisfy all the constraints?
106 //! [docs-java-quickstart-7 start]
107 Result r1 = solver.checkSat();
108 //! [docs-java-quickstart-7 end]
109
110 // The result is either SAT, UNSAT, or UNKNOWN.
111 // In this case, it is SAT.
112 //! [docs-java-quickstart-8 start]
113 System.out.println("expected: sat");
114 System.out.println("result: " + r1);
115 //! [docs-java-quickstart-8 end]
116
117 // We can get the values for x and y that satisfy the constraints.
118 //! [docs-java-quickstart-9 start]
119 Term xVal = solver.getValue(x);
120 Term yVal = solver.getValue(y);
121 //! [docs-java-quickstart-9 end]
122
123 // It is also possible to get values for compound terms,
124 // even if those did not appear in the original formula.
125 //! [docs-java-quickstart-10 start]
126 Term xMinusY = tm.mkTerm(Kind.SUB, x, y);
127 Term xMinusYVal = solver.getValue(xMinusY);
128 //! [docs-java-quickstart-10 end]
129
130 // Further, we can convert the values to java types
131 //! [docs-java-quickstart-11 start]
132 Pair<BigInteger, BigInteger> xPair = xVal.getRealValue();
133 Pair<BigInteger, BigInteger> yPair = yVal.getRealValue();
134 Pair<BigInteger, BigInteger> xMinusYPair = xMinusYVal.getRealValue();
135
136 System.out.println("value for x: " + xPair.first + "/" + xPair.second);
137 System.out.println("value for y: " + yPair.first + "/" + yPair.second);
138 System.out.println("value for x - y: " + xMinusYPair.first + "/" + xMinusYPair.second);
139 //! [docs-java-quickstart-11 end]
140
141 // Another way to independently compute the value of x - y would be
142 // to perform the (rational) arithmetic manually.
143 // However, for more complex terms,
144 // it is easier to let the solver do the evaluation.
145 //! [docs-java-quickstart-12 start]
146 Pair<BigInteger, BigInteger> xMinusYComputed =
147 new Pair<>(xPair.first.multiply(yPair.second).subtract(xPair.second.multiply(yPair.first)),
148 xPair.second.multiply(yPair.second));
149 BigInteger g = xMinusYComputed.first.gcd(xMinusYComputed.second);
150 xMinusYComputed = new Pair<>(xMinusYComputed.first.divide(g), xMinusYComputed.second.divide(g));
151 if (xMinusYComputed.equals(xMinusYPair))
152 {
153 System.out.println("computed correctly");
154 }
155 else
156 {
157 System.out.println("computed incorrectly");
158 }
159 //! [docs-java-quickstart-12 end]
160
161 // Next, we will check satisfiability of the same formula,
162 // only this time over integer variables a and b.
163
164 // We start by resetting assertions added to the solver.
165 //! [docs-java-quickstart-13 start]
166 solver.resetAssertions();
167 //! [docs-java-quickstart-13 end]
168
169 // Next, we assert the same assertions above with integers.
170 // This time, we inline the construction of terms
171 // to the assertion command.
172 //! [docs-java-quickstart-14 start]
173 solver.assertFormula(tm.mkTerm(Kind.LT, tm.mkInteger(0), a));
174 solver.assertFormula(tm.mkTerm(Kind.LT, tm.mkInteger(0), b));
175 solver.assertFormula(
176 tm.mkTerm(Kind.LT, tm.mkTerm(Kind.ADD, a, b), tm.mkInteger(1)));
177 solver.assertFormula(tm.mkTerm(Kind.LEQ, a, b));
178 //! [docs-java-quickstart-14 end]
179
180 // We check whether the revised assertion is satisfiable.
181 //! [docs-java-quickstart-15 start]
182 Result r2 = solver.checkSat();
183
184 // This time the formula is unsatisfiable
185 System.out.println("expected: unsat");
186 System.out.println("result: " + r2);
187 //! [docs-java-quickstart-15 end]
188
189 // We can query the solver for an unsatisfiable core, i.e., a subset
190 // of the assertions that is already unsatisfiable.
191 //! [docs-java-quickstart-16 start]
192 List<Term> unsatCore = Arrays.asList(solver.getUnsatCore());
193 System.out.println("unsat core size: " + unsatCore.size());
194 System.out.println("unsat core: ");
195 for (Term t : unsatCore)
196 {
197 System.out.println(t);
198 }
199 //! [docs-java-quickstart-16 end]
200 }
201 Context.deletePointers();
202 }
203}
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/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]