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

examples/api/c/quickstart.c

  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}