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