Quickstart Guide

First, create a cvc5 Solver instance using try with resources:

try (Solver solver = new Solver())
{
  /** write your code here */
}

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.

// Further, we can convert the 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-2022 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 import io.github.cvc5.*;
 18 import java.math.BigInteger;
 19 import java.util.ArrayList;
 20 import java.util.Arrays;
 21 import java.util.List;
 22 
 23 public class QuickStart
 24 {
 25   public static void main(String args[]) throws CVC5ApiException
 26   {
 27     // Create a solver
 28     try (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       solver.setOption("produce-models", "true");
 33       solver.setOption("produce-unsat-cores", "true");
 34 
 35       // The simplest way to set a logic for the solver is to choose "ALL".
 36       // This enables all logics in the solver.
 37       // Alternatively, "QF_ALL" enables all logics without quantifiers.
 38       // To optimize the solver's behavior for a more specific logic,
 39       // use the logic name, e.g. "QF_BV" or "QF_AUFBV".
 40 
 41       // Set the logic
 42       solver.setLogic("ALL");
 43 
 44       // In this example, we will define constraints over reals and integers.
 45       // Hence, we first obtain the corresponding sorts.
 46       Sort realSort = solver.getRealSort();
 47       Sort intSort = solver.getIntegerSort();
 48 
 49       // x and y will be real variables, while a and b will be integer variables.
 50       // Formally, their cpp type is Term,
 51       // and they are called "constants" in SMT jargon:
 52       Term x = solver.mkConst(realSort, "x");
 53       Term y = solver.mkConst(realSort, "y");
 54       Term a = solver.mkConst(intSort, "a");
 55       Term b = solver.mkConst(intSort, "b");
 56 
 57       // Our constraints regarding x and y will be:
 58       //
 59       //   (1)  0 < x
 60       //   (2)  0 < y
 61       //   (3)  x + y < 1
 62       //   (4)  x <= y
 63       //
 64 
 65       // Formally, constraints are also terms. Their sort is Boolean.
 66       // We will construct these constraints gradually,
 67       // by defining each of their components.
 68       // We start with the constant numerals 0 and 1:
 69       Term zero = solver.mkReal(0);
 70       Term one = solver.mkReal(1);
 71 
 72       // Next, we construct the term x + y
 73       Term xPlusY = solver.mkTerm(Kind.ADD, x, y);
 74 
 75       // Now we can define the constraints.
 76       // They use the operators +, <=, and <.
 77       // In the API, these are denoted by ADD, LEQ, and LT.
 78       // A list of available operators is available in:
 79       // src/api/cpp/cvc5_kind.h
 80       Term constraint1 = solver.mkTerm(Kind.LT, zero, x);
 81       Term constraint2 = solver.mkTerm(Kind.LT, zero, y);
 82       Term constraint3 = solver.mkTerm(Kind.LT, xPlusY, one);
 83       Term constraint4 = solver.mkTerm(Kind.LEQ, x, y);
 84 
 85       // Now we assert the constraints to the solver.
 86       solver.assertFormula(constraint1);
 87       solver.assertFormula(constraint2);
 88       solver.assertFormula(constraint3);
 89       solver.assertFormula(constraint4);
 90 
 91       // Check if the formula is satisfiable, that is,
 92       // are there real values for x and y that satisfy all the constraints?
 93       Result r1 = solver.checkSat();
 94 
 95       // The result is either SAT, UNSAT, or UNKNOWN.
 96       // In this case, it is SAT.
 97       System.out.println("expected: sat");
 98       System.out.println("result: " + r1);
 99 
100       // We can get the values for x and y that satisfy the constraints.
101       Term xVal = solver.getValue(x);
102       Term yVal = solver.getValue(y);
103 
104       // It is also possible to get values for compound terms,
105       // even if those did not appear in the original formula.
106       Term xMinusY = solver.mkTerm(Kind.SUB, x, y);
107       Term xMinusYVal = solver.getValue(xMinusY);
108 
109       // Further, we can convert the values to java types
110       Pair<BigInteger, BigInteger> xPair = xVal.getRealValue();
111       Pair<BigInteger, BigInteger> yPair = yVal.getRealValue();
112       Pair<BigInteger, BigInteger> xMinusYPair = xMinusYVal.getRealValue();
113 
114       System.out.println("value for x: " + xPair.first + "/" + xPair.second);
115       System.out.println("value for y: " + yPair.first + "/" + yPair.second);
116       System.out.println("value for x - y: " + xMinusYPair.first + "/" + xMinusYPair.second);
117 
118       // Another way to independently compute the value of x - y would be
119       // to perform the (rational) arithmetic manually.
120       // However, for more complex terms,
121       // it is easier to let the solver do the evaluation.
122       Pair<BigInteger, BigInteger> xMinusYComputed =
123           new Pair(xPair.first.multiply(yPair.second).subtract(xPair.second.multiply(yPair.first)),
124               xPair.second.multiply(yPair.second));
125       BigInteger g = xMinusYComputed.first.gcd(xMinusYComputed.second);
126       xMinusYComputed = new Pair(xMinusYComputed.first.divide(g), xMinusYComputed.second.divide(g));
127       if (xMinusYComputed.equals(xMinusYPair))
128       {
129         System.out.println("computed correctly");
130       }
131       else
132       {
133         System.out.println("computed incorrectly");
134       }
135 
136       // Next, we will check satisfiability of the same formula,
137       // only this time over integer variables a and b.
138 
139       // We start by resetting assertions added to the solver.
140       solver.resetAssertions();
141 
142       // Next, we assert the same assertions above with integers.
143       // This time, we inline the construction of terms
144       // to the assertion command.
145       solver.assertFormula(solver.mkTerm(Kind.LT, solver.mkInteger(0), a));
146       solver.assertFormula(solver.mkTerm(Kind.LT, solver.mkInteger(0), b));
147       solver.assertFormula(
148           solver.mkTerm(Kind.LT, solver.mkTerm(Kind.ADD, a, b), solver.mkInteger(1)));
149       solver.assertFormula(solver.mkTerm(Kind.LEQ, a, b));
150 
151       // We check whether the revised assertion is satisfiable.
152       Result r2 = solver.checkSat();
153 
154       // This time the formula is unsatisfiable
155       System.out.println("expected: unsat");
156       System.out.println("result: " + r2);
157 
158       // We can query the solver for an unsatisfiable core, i.e., a subset
159       // of the assertions that is already unsatisfiable.
160       List<Term> unsatCore = Arrays.asList(solver.getUnsatCore());
161       System.out.println("unsat core size: " + unsatCore.size());
162       System.out.println("unsat core: ");
163       for (Term t : unsatCore)
164       {
165         System.out.println(t);
166       }
167     }
168   }
169 }