Quickstart Guide

First, create a cvc5 Solver instance:

Solver solver = new Solver();

To produce models and unsat cores, we have to enable the following options.

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

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

solver.setLogic("ALL");

In the following, we will define real and integer constraints. For this, we first query the solver for the corresponding sorts.

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

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

Term x = solver.mkConst(realSort, "x");
Term y = solver.mkConst(realSort, "y");
Term a = solver.mkConst(intSort, "a");
Term b = solver.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 = solver.mkReal(0);
Term one = solver.mkReal(1);

// Next, we construct the term x + y
Term xPlusY = solver.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 = solver.mkTerm(Kind.LT, zero, x);
Term constraint2 = solver.mkTerm(Kind.LT, zero, y);
Term constraint3 = solver.mkTerm(Kind.LT, xPlusY, one);
Term constraint4 = solver.mkTerm(Kind.LEQ, x, y);

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

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

Result r1 = solver.checkSat();

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

System.out.println("expected: sat");
System.out.println("result: " + r1);

This will print:

expected: sat
result: sat

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

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

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

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

We can convert these values to Java types.

Pair<BigInteger, BigInteger> xPair = xVal.getRealValue();
Pair<BigInteger, BigInteger> yPair = yVal.getRealValue();
Pair<BigInteger, BigInteger> xMinusYPair = xMinusYVal.getRealValue();

System.out.println("value for x: " + xPair.first + "/" + xPair.second);
System.out.println("value for y: " + yPair.first + "/" + yPair.second);
System.out.println("value for x - y: " + xMinusYPair.first + "/" + xMinusYPair.second);

Another way to independently compute the value of x - y would be to perform the (rational) arithmetic manually. However, for more complex terms, it is easier to let the solver do the evaluation.

Pair<BigInteger, BigInteger> xMinusYComputed =
    new Pair(xPair.first.multiply(yPair.second).subtract(xPair.second.multiply(yPair.first)),
        xPair.second.multiply(yPair.second));
BigInteger g = xMinusYComputed.first.gcd(xMinusYComputed.second);
xMinusYComputed = new Pair(xMinusYComputed.first.divide(g), xMinusYComputed.second.divide(g));
if (xMinusYComputed.equals(xMinusYPair))
{
  System.out.println("computed correctly");
}
else
{
  System.out.println("computed incorrectly");
}

This will print:

computed correctly

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

solver.resetAssertions();

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

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

Now, we check whether the revised assertion is satisfiable.

Result r2 = solver.checkSat();

// This time the formula is unsatisfiable
System.out.println("expected: unsat");
System.out.println("result: " + r2);

This time the asserted formula is unsatisfiable:

expected: unsat
result: unsat

We can query the solver for an unsatisfiable core, that is, a subset of the assertions that is already unsatisfiable.

List<Term> unsatCore = Arrays.asList(solver.getUnsatCore());
System.out.println("unsat core size: " + unsatCore.size());
System.out.println("unsat core: ");
for (Term t : unsatCore)
{
  System.out.println(t);
}

This will print:

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

Example

examples/api/java/QuickStart.java

  1/******************************************************************************
  2 * Top contributors (to current version):
  3 *   Mudathir Mohamed, Aina Niemetz, 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}