examples/api/java/QuickStart.java

   1 /******************************************************************************
   2  * Top contributors (to current version):
   3  *   Yoni Zohar
   4  *
   5  * This file is part of the cvc5 project.
   6  *
   7  * Copyright (c) 2009-2021 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.api.*;
  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.PLUS, x, y);
  74
  75       // Now we can define the constraints.
  76       // They use the operators +, <=, and <.
  77       // In the API, these are denoted by PLUS, 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.MINUS, 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.PLUS, 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 }