Quickstart Guide
First, create a cvc5 Cvc5TermManager instance:
Cvc5TermManager* tm = cvc5_term_manager_new();
Then, create a Cvc5 solver instance:
Cvc5* slv = cvc5_new(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.
cvc5_set_option(slv, "produce-models", "true");
cvc5_set_option(slv, "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".
cvc5_set_logic(slv, "ALL");
In the following, we will define constraints of reals and integers. For this, we first query the solver for the corresponding sorts.
Cvc5Sort real_sort = cvc5_get_real_sort(tm);
Cvc5Sort int_sort = cvc5_get_integer_sort(tm);
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.
Cvc5Term x = cvc5_mk_const(tm, real_sort, "x");
Cvc5Term y = cvc5_mk_const(tm, real_sort, "y");
Cvc5Term a = cvc5_mk_const(tm, int_sort, "a");
Cvc5Term b = cvc5_mk_const(tm, int_sort, "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:
Cvc5Term zero = cvc5_mk_real_int64(tm, 0);
Cvc5Term one = cvc5_mk_real_int64(tm, 1);
// Next, we construct the term x + y
Cvc5Term args2[2] = {x, y};
Cvc5Term x_plus_y = cvc5_mk_term(tm, CVC5_KIND_ADD, 2, args2);
// 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
args2[0] = zero;
args2[1] = x;
Cvc5Term constraint1 = cvc5_mk_term(tm, CVC5_KIND_LT, 2, args2);
args2[1] = y;
Cvc5Term constraint2 = cvc5_mk_term(tm, CVC5_KIND_LT, 2, args2);
args2[0] = x_plus_y;
args2[1] = one;
Cvc5Term constraint3 = cvc5_mk_term(tm, CVC5_KIND_LT, 2, args2);
args2[0] = x;
args2[1] = y;
Cvc5Term constraint4 = cvc5_mk_term(tm, CVC5_KIND_LEQ, 2, args2);
// Now we assert the constraints to the solver.
cvc5_assert_formula(slv, constraint1);
cvc5_assert_formula(slv, constraint2);
cvc5_assert_formula(slv, constraint3);
cvc5_assert_formula(slv, 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.
Cvc5Result r = cvc5_check_sat(slv);
The result we get from this satisfiability check is either sat, unsat
or unknown.
It’s status can be queried via
cvc5_result_is_sat(),
cvc5_result_is_unsat() and
cvc5_result_is_unknown().
Alternatively, it can also be printed.
printf("expected: sat\n");
printf("result: %s\n", cvc5_result_to_string(r));
This will print:
expected: sat
result: sat
Now, we query the solver for the values for x and y that satisfy
the constraints.
Cvc5Term x_val = cvc5_get_value(slv, x);
Cvc5Term y_val = cvc5_get_value(slv, y);
It is also possible to get values for terms that do not appear in the original formula.
args2[0] = x;
args2[1] = y;
Cvc5Term x_minus_y = cvc5_mk_term(tm, CVC5_KIND_SUB, 2, args2);
Cvc5Term x_minus_y_val = cvc5_get_value(slv, x_minus_y);
We can retrieve the string representation of these values as follows.
// Note: The const char* returned by cvc5_term_get_real_value is only valid
// until the next call to this function.
char* x_str = strdup(cvc5_term_get_real_value(x_val));
char* y_str = strdup(cvc5_term_get_real_value(y_val));
char* x_minus_y_str = strdup(cvc5_term_get_real_value(x_minus_y_val));
printf("value for x: %s\n", x_str);
printf("value for y: %s\n", y_str);
printf("value for x - y: %s\n", x_minus_y_str);
free(y_str);
free(x_str);
free(x_minus_y_str);
// Alternatively, you can directly print the value strings without
// copying them first:
printf("value for x: %s\n", cvc5_term_get_real_value(x_val));
printf("value for y: %s\n", cvc5_term_get_real_value(y_val));
printf("value for x - y: %s\n", cvc5_term_get_real_value(x_minus_y_val));
This will print the following:
value for x: 1/6
value for y: 1/6
value for x - y: 0.0
We can convert these values to C++ types.
// Further, we can convert the values to cpp types
int64_t x_num;
uint64_t x_den;
cvc5_term_get_real64_value(x_val, &x_num, &x_den);
int64_t y_num;
uint64_t y_den;
cvc5_term_get_real64_value(y_val, &y_num, &y_den);
int64_t x_minus_y_num;
uint64_t x_minus_y_den;
cvc5_term_get_real64_value(x_minus_y_val, &x_minus_y_num, &x_minus_y_den);
printf("value for x: %" PRId64 "/%" PRIu64 "\n", x_num, x_den);
printf("value for y: %" PRId64 "/%" PRIu64 "\n", y_num, y_den);
printf("value for x - y: %" PRId64 "/%" PRIu64 "\n", x_minus_y_num, x_minus_y_den);
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.
int64_t x_minus_y_num_computed = x_num * y_den - x_den * y_num;
uint64_t x_minus_y_den_computed = x_den * y_den;
uint64_t g = gcd(x_minus_y_num_computed, x_minus_y_den_computed);
x_minus_y_num_computed = x_minus_y_num_computed / g;
x_minus_y_den_computed = x_minus_y_den_computed / g;
if (x_minus_y_num_computed == x_minus_y_num
&& x_minus_y_den_computed == x_minus_y_den)
{
printf("computed correctly\n");
}
else
{
printf("computed incorrectly\n");
}
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.
cvc5_reset_assertions(slv);
Next, we assert the same assertions as above, but with integers. This time, we inline the construction of terms to the assertion command.
args2[0] = cvc5_mk_integer_int64(tm, 0);
args2[1] = a;
cvc5_assert_formula(slv, cvc5_mk_term(tm, CVC5_KIND_LT, 2, args2));
args2[1] = b;
cvc5_assert_formula(slv, cvc5_mk_term(tm, CVC5_KIND_LT, 2, args2));
args2[0] = a;
args2[1] = b;
Cvc5Term add = cvc5_mk_term(tm, CVC5_KIND_ADD, 2, args2);
args2[0] = add;
args2[1] = cvc5_mk_integer_int64(tm, 1);
cvc5_assert_formula(slv, cvc5_mk_term(tm, CVC5_KIND_LT, 2, args2));
args2[0] = a;
args2[1] = b;
cvc5_assert_formula(slv, cvc5_mk_term(tm, CVC5_KIND_LEQ, 2, args2));
Now, we check whether the revised assertion is satisfiable.
cvc5_result_release(r); // optional, not needed anymore so we can release
r = cvc5_check_sat(slv);
printf("expected: unsat\n");
printf("result: %s\n", cvc5_result_to_string(r));
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.
size_t size;
const Cvc5Term* unsat_core = cvc5_get_unsat_core(slv, &size);
printf("unsat core size: %zu\n", size);
printf("unsat core: \n");
for (size_t i = 0; i < size; i++)
{
printf("%s\n", cvc5_term_to_string(unsat_core[i]));
}
This will print:
unsat core size: 3
unsat core:
(< 0 a)
(< 0 b)
(< (+ a b) 1)
Example
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/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}
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/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/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]