Quickstart Guide

First, create a cvc5 TermManager instance:

TermManager tm;

Then, create a cvc5 Solver instance:

Solver solver(tm);

We will ask the solver to produce models and unsat cores in the following, and for this we have to enable the following options.

solver.setOption("produce-models", "true");
solver.setOption("produce-unsat-cores", "true");

Next we set the logic. The simplest way to set a logic for the solver is to choose “ALL”. This enables all logics in the solver. Alternatively, "QF_ALL" enables all logics without quantifiers. To optimize the solver’s behavior for a more specific logic, use the logic name, e.g. "QF_BV" or "QF_AUFBV" .

solver.setLogic("ALL");

In the following, we will define constraints of reals and integers. For this, we first query the solver for the corresponding sorts.

Sort realSort = tm.getRealSort();
Sort intSort = tm.getIntegerSort();

Now, we create two constants x and y of sort Real , and two constants a and b of sort Integer . Notice that these are symbolic constants, but not actual values.

Term x = tm.mkConst(realSort, "x");
Term y = tm.mkConst(realSort, "y");
Term a = tm.mkConst(intSort, "a");
Term b = tm.mkConst(intSort, "b");

We define the following constraints regarding x and y :

\[(0 < x) \wedge (0 < y) \wedge (x + y < 1) \wedge (x \leq y)\]

We construct the required terms and assert them as follows:

// Formally, constraints are also terms. Their sort is Boolean.
// We will construct these constraints gradually,
// by defining each of their components.
// We start with the constant numerals 0 and 1:
Term zero = tm.mkReal(0);
Term one = tm.mkReal(1);

// Next, we construct the term x + y
Term xPlusY = tm.mkTerm(Kind::ADD, {x, y});

// Now we can define the constraints.
// They use the operators +, <=, and <.
// In the API, these are denoted by ADD, LEQ, and LT.
// A list of available operators is available in:
// src/api/cpp/cvc5_kind.h
Term constraint1 = tm.mkTerm(Kind::LT, {zero, x});
Term constraint2 = tm.mkTerm(Kind::LT, {zero, y});
Term constraint3 = tm.mkTerm(Kind::LT, {xPlusY, one});
Term constraint4 = tm.mkTerm(Kind::LEQ, {x, y});

// Now we assert the constraints to the solver.
solver.assertFormula(constraint1);
solver.assertFormula(constraint2);
solver.assertFormula(constraint3);
solver.assertFormula(constraint4);

Now we check if the asserted formula is satisfiable, that is, we check if there exist values of sort Real for x and y that satisfy all the constraints.

Result r1 = solver.checkSat();

The result we get from this satisfiability check is either sat , unsat or unknown . It’s status can be queried via cvc5::Result::isSat() , cvc5::Result::isUnsat() and cvc5::Result::isSatUnknown() . Alternatively, it can also be printed.

std::cout << "expected: sat" << std::endl;
std::cout << "result: " << r1 << std::endl;

This will print:

expected: sat
result: sat

Now, we query the solver for the values for x and y that satisfy the constraints.

Term xVal = solver.getValue(x);
Term yVal = solver.getValue(y);

It is also possible to get values for terms that do not appear in the original formula.

Term xMinusY = tm.mkTerm(Kind::SUB, {x, y});
Term xMinusYVal = solver.getValue(xMinusY);

We can retrieve the string representation of these values as follows.

std::string xStr = xVal.getRealValue();
std::string yStr = yVal.getRealValue();
std::string xMinusYStr = xMinusYVal.getRealValue();

std::cout << "value for x: " << xStr << std::endl;
std::cout << "value for y: " << yStr << std::endl;
std::cout << "value for x - y: " << xMinusYStr << std::endl;

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
std::pair<int64_t, uint64_t> xPair = xVal.getReal64Value();
std::pair<int64_t, uint64_t> yPair = yVal.getReal64Value();
std::pair<int64_t, uint64_t> xMinusYPair = xMinusYVal.getReal64Value();

std::cout << "value for x: " << xPair.first << "/" << xPair.second
          << std::endl;
std::cout << "value for y: " << yPair.first << "/" << yPair.second
          << std::endl;
std::cout << "value for x - y: " << xMinusYPair.first << "/"
          << xMinusYPair.second << std::endl;

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.

std::pair<int64_t, uint64_t> xMinusYComputed = {
  xPair.first * yPair.second - xPair.second * yPair.first,
  xPair.second * yPair.second
};
uint64_t g = std::gcd(xMinusYComputed.first, xMinusYComputed.second);
xMinusYComputed = { xMinusYComputed.first / g, xMinusYComputed.second / g };
if (xMinusYComputed == xMinusYPair)
{
  std::cout << "computed correctly" << std::endl;
}
else
{
  std::cout << "computed incorrectly" << std::endl;
}

This will print:

computed correctly

Next, we will check satisfiability of the same formula, only this time over integer variables a and b . For this, we first reset the assertions added to the solver.

solver.resetAssertions();

Next, we assert the same assertions as above, but with integers. This time, we inline the construction of terms to the assertion command.

solver.assertFormula(tm.mkTerm(Kind::LT, {tm.mkInteger(0), a}));
solver.assertFormula(tm.mkTerm(Kind::LT, {tm.mkInteger(0), b}));
solver.assertFormula(
    tm.mkTerm(Kind::LT, {tm.mkTerm(Kind::ADD, {a, b}), tm.mkInteger(1)}));
solver.assertFormula(tm.mkTerm(Kind::LEQ, {a, b}));

Now, we check whether the revised assertion is satisfiable.

Result r2 = solver.checkSat();
std::cout << "expected: unsat" << std::endl;
std::cout << "result: " << r2 << std::endl;

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.

std::vector<Term> unsatCore = solver.getUnsatCore();
std::cout << "unsat core size: " << unsatCore.size() << std::endl;
std::cout << "unsat core: " << std::endl;
for (const Term& t : unsatCore)
{
  std::cout << t << std::endl;
}

This will print:

unsat core size: 3
unsat core:
(< 0 a)
(< 0 b)
(< (+ a b) 1)

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}