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