diff options
| author | mudathirmahgoub <mudathirmahgoub@gmail.com> | 2021-10-01 18:21:02 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-10-01 23:21:02 +0000 |
| commit | 98e884a740e8e2d1c32c8b60f3197fbae656e619 (patch) | |
| tree | 3fb1b24141ec833240eb71aebd93f383e897b592 | |
| parent | 6405f082a85e2a2ce7e25ff1f8b058f3f42fd58b (diff) | |
Update java examples using the new Java API (#7225)
This PRs updates java examples using the new Java API, by converting C++ examples to Java.
Examples CVC4Streams.java and PipedInput.java are removed since they are not longer supported by the API.
All examples are not included in the build which would be added in a future PR.
36 files changed, 1743 insertions, 692 deletions
diff --git a/docs/examples/extract.rst b/docs/examples/extract.rst index 61eaa6462..1f6d9b9bf 100644 --- a/docs/examples/extract.rst +++ b/docs/examples/extract.rst @@ -4,5 +4,6 @@ Theory of Bit-Vectors: :code:`extract` .. api-examples:: ../../examples/api/cpp/extract.cpp + ../../examples/api/java/Extract.java ../../examples/api/python/extract.py ../../examples/api/smtlib/extract.smt2 diff --git a/docs/examples/quickstart.rst b/docs/examples/quickstart.rst index bd2c3450a..330cc7065 100644 --- a/docs/examples/quickstart.rst +++ b/docs/examples/quickstart.rst @@ -4,5 +4,6 @@ Quickstart Example .. api-examples:: ../../examples/api/cpp/quickstart.cpp + ../../examples/api/java/QuickStart.java ../../examples/api/python/quickstart.py ../../examples/api/smtlib/quickstart.smt2 diff --git a/docs/examples/relations.rst b/docs/examples/relations.rst index d94fa0aa7..d81eb8fee 100644 --- a/docs/examples/relations.rst +++ b/docs/examples/relations.rst @@ -3,5 +3,6 @@ Theory of Relations .. api-examples:: + ../../examples/api/java/Relations.java ../../examples/api/smtlib/relations.smt2 diff --git a/docs/examples/sequences.rst b/docs/examples/sequences.rst index 569fdfc04..b0a9ab1f1 100644 --- a/docs/examples/sequences.rst +++ b/docs/examples/sequences.rst @@ -4,5 +4,6 @@ Theory of Sequences .. api-examples:: ../../examples/api/cpp/sequences.cpp + ../../examples/api/java/Sequences.java ../../examples/api/python/sequences.py ../../examples/api/smtlib/sequences.smt2 diff --git a/docs/examples/sets.rst b/docs/examples/sets.rst index b0f1fc1da..09cad0cce 100644 --- a/docs/examples/sets.rst +++ b/docs/examples/sets.rst @@ -4,5 +4,6 @@ Theory of Sets .. api-examples:: ../../examples/api/cpp/sets.cpp + ../../examples/api/java/Sets.java ../../examples/api/python/sets.py ../../examples/api/smtlib/sets.smt2 diff --git a/docs/examples/sygus-fun.rst b/docs/examples/sygus-fun.rst index 3d5bddff1..5b22ae833 100644 --- a/docs/examples/sygus-fun.rst +++ b/docs/examples/sygus-fun.rst @@ -4,4 +4,5 @@ SyGuS: Functions .. api-examples:: ../../examples/api/cpp/sygus-fun.cpp + ../../examples/api/java/SygusFun.java ../../examples/api/python/sygus-fun.py diff --git a/docs/examples/sygus-grammar.rst b/docs/examples/sygus-grammar.rst index 3733fe2c3..6c627e22f 100644 --- a/docs/examples/sygus-grammar.rst +++ b/docs/examples/sygus-grammar.rst @@ -4,4 +4,5 @@ SyGuS: Grammars .. api-examples:: ../../examples/api/cpp/sygus-grammar.cpp + ../../examples/api/java/SygusGrammar.java ../../examples/api/python/sygus-grammar.py diff --git a/docs/examples/sygus-inv.rst b/docs/examples/sygus-inv.rst index f9698a720..2fac909ef 100644 --- a/docs/examples/sygus-inv.rst +++ b/docs/examples/sygus-inv.rst @@ -4,4 +4,5 @@ SyGuS: Invariants .. api-examples:: ../../examples/api/cpp/sygus-inv.cpp + ../../examples/api/java/SygusInv.java ../../examples/api/python/sygus-inv.py diff --git a/examples/api/cpp/CMakeLists.txt b/examples/api/cpp/CMakeLists.txt index b33dd3e13..5f3298d19 100644 --- a/examples/api/cpp/CMakeLists.txt +++ b/examples/api/cpp/CMakeLists.txt @@ -19,6 +19,7 @@ set(CVC5_EXAMPLES_API combination datatypes extract + floating_point_arith helloworld linear_arith quickstart diff --git a/examples/api/cpp/floating_point_arith.cpp b/examples/api/cpp/floating_point_arith.cpp new file mode 100644 index 000000000..5c6c5a8a3 --- /dev/null +++ b/examples/api/cpp/floating_point_arith.cpp @@ -0,0 +1,103 @@ +/****************************************************************************** + * Top contributors (to current version): + * Andres Noetzli + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * An example of solving floating-point problems with cvc5's cpp API + * + * This example shows to create floating-point types, variables and expressions, + * and how to create rounding mode constants by solving toy problems. The + * example also shows making special values (such as NaN and +oo) and converting + * an IEEE 754-2008 bit-vector to a floating-point number. + */ + +#include <cvc5/cvc5.h> + +#include <iostream> +#include <cassert> + +using namespace std; +using namespace cvc5::api; + +int main() +{ + Solver solver; + solver.setOption("produce-models", "true"); + + // Make single precision floating-point variables + Sort fpt32 = solver.mkFloatingPointSort(8, 24); + Term a = solver.mkConst(fpt32, "a"); + Term b = solver.mkConst(fpt32, "b"); + Term c = solver.mkConst(fpt32, "c"); + Term d = solver.mkConst(fpt32, "d"); + Term e = solver.mkConst(fpt32, "e"); + + // Assert that floating-point addition is not associative: + // (a + (b + c)) != ((a + b) + c) + Term rm = solver.mkRoundingMode(ROUND_NEAREST_TIES_TO_EVEN); + Term lhs = solver.mkTerm( + FLOATINGPOINT_ADD, rm, a, solver.mkTerm(FLOATINGPOINT_ADD, rm, b, c)); + Term rhs = solver.mkTerm( + FLOATINGPOINT_ADD, rm, solver.mkTerm(FLOATINGPOINT_ADD, rm, a, b), c); + solver.assertFormula(solver.mkTerm(NOT, solver.mkTerm(EQUAL, a, b))); + + Result r = solver.checkSat(); // result is sat + assert (r.isSat()); + + cout << "a = " << solver.getValue(a) << endl; + cout << "b = " << solver.getValue(b) << endl; + cout << "c = " << solver.getValue(c) << endl; + + // Now, let's restrict `a` to be either NaN or positive infinity + Term nan = solver.mkNaN(8, 24); + Term inf = solver.mkPosInf(8, 24); + solver.assertFormula(solver.mkTerm( + OR, solver.mkTerm(EQUAL, a, inf), solver.mkTerm(EQUAL, a, nan))); + + r = solver.checkSat(); // result is sat + assert (r.isSat()); + + cout << "a = " << solver.getValue(a) << endl; + cout << "b = " << solver.getValue(b) << endl; + cout << "c = " << solver.getValue(c) << endl; + + // And now for something completely different. Let's try to find a (normal) + // floating-point number that rounds to different integer values for + // different rounding modes. + Term rtp = solver.mkRoundingMode(ROUND_TOWARD_POSITIVE); + Term rtn = solver.mkRoundingMode(ROUND_TOWARD_NEGATIVE); + Op op = solver.mkOp(FLOATINGPOINT_TO_SBV, 16); // (_ fp.to_sbv 16) + lhs = solver.mkTerm(op, rtp, d); + rhs = solver.mkTerm(op, rtn, d); + solver.assertFormula(solver.mkTerm(FLOATINGPOINT_ISN, d)); + solver.assertFormula(solver.mkTerm(NOT, solver.mkTerm(EQUAL, lhs, rhs))); + + r = solver.checkSat(); // result is sat + assert (r.isSat()); + + // Convert the result to a rational and print it + Term val = solver.getValue(d); + Term realVal = solver.getValue(solver.mkTerm(FLOATINGPOINT_TO_REAL, val)); + cout << "d = " << val << " = " << realVal << endl; + cout << "((_ fp.to_sbv 16) RTP d) = " << solver.getValue(lhs) << endl; + cout << "((_ fp.to_sbv 16) RTN d) = " << solver.getValue(rhs) << endl; + + // For our final trick, let's try to find a floating-point number between + // positive zero and the smallest positive floating-point number + Term zero = solver.mkPosZero(8, 24); + Term smallest = solver.mkFloatingPoint(8, 24, solver.mkBitVector(32, 0b001)); + solver.assertFormula( + solver.mkTerm(AND, + solver.mkTerm(FLOATINGPOINT_LT, zero, e), + solver.mkTerm(FLOATINGPOINT_LT, e, smallest))); + + r = solver.checkSat(); // result is unsat + assert (!r.isSat()); +} diff --git a/examples/api/java/BitVectors.java b/examples/api/java/BitVectors.java index 6d97b93fa..181c16614 100644 --- a/examples/api/java/BitVectors.java +++ b/examples/api/java/BitVectors.java @@ -1,6 +1,6 @@ /****************************************************************************** * Top contributors (to current version): - * Morgan Deters, Liana Hadarean, Aina Niemetz + * Aina Niemetz, Liana Hadarean, Makai Mann * * This file is part of the cvc5 project. * @@ -10,21 +10,20 @@ * directory for licensing information. * **************************************************************************** * - * A simple demonstration of the solving capabilities of the cvc5 bit-vector - * solver. + * A simple demonstration of the solving capabilities of the cvc5 + * bit-vector solver. * */ -import edu.stanford.CVC4.*; +import cvc5.*; +import java.util.*; -public class BitVectors { - public static void main(String[] args) { - System.loadLibrary("cvc4jni"); - - ExprManager em = new ExprManager(); - SmtEngine smt = new SmtEngine(em); - - smt.setLogic("QF_BV"); // Set the logic +public class BitVectors +{ + public static void main(String args[]) throws CVC5ApiException + { + Solver slv = new Solver(); + slv.setLogic("QF_BV"); // Set the logic // The following example has been adapted from the book A Hacker's Delight by // Henry S. Warren. @@ -42,68 +41,85 @@ public class BitVectors { // //(2) x = a + b - x; // - // We will use CVC4 to prove that the three pieces of code above are all + // We will use cvc5 to prove that the three pieces of code above are all // equivalent by encoding the problem in the bit-vector theory. // Creating a bit-vector type of width 32 - Type bitvector32 = em.mkBitVectorType(32); + Sort bitvector32 = slv.mkBitVectorSort(32); // Variables - Expr x = em.mkVar("x", bitvector32); - Expr a = em.mkVar("a", bitvector32); - Expr b = em.mkVar("b", bitvector32); + Term x = slv.mkConst(bitvector32, "x"); + Term a = slv.mkConst(bitvector32, "a"); + Term b = slv.mkConst(bitvector32, "b"); - // First encode the assumption that x must be equal to a or b - Expr x_eq_a = em.mkExpr(Kind.EQUAL, x, a); - Expr x_eq_b = em.mkExpr(Kind.EQUAL, x, b); - Expr assumption = em.mkExpr(Kind.OR, x_eq_a, x_eq_b); + // First encode the assumption that x must be Kind.EQUAL to a or b + Term x_eq_a = slv.mkTerm(Kind.EQUAL, x, a); + Term x_eq_b = slv.mkTerm(Kind.EQUAL, x, b); + Term assumption = slv.mkTerm(Kind.OR, x_eq_a, x_eq_b); // Assert the assumption - smt.assertFormula(assumption); + slv.assertFormula(assumption); // Introduce a new variable for the new value of x after assignment. - Expr new_x = em.mkVar("new_x", bitvector32); // x after executing code (0) - Expr new_x_ = em.mkVar("new_x_", bitvector32); // x after executing code (1) or (2) + Term new_x = slv.mkConst(bitvector32, "new_x"); // x after executing code (0) + Term new_x_ = slv.mkConst(bitvector32, "new_x_"); // x after executing code (1) or (2) // Encoding code (0) // new_x = x == a ? b : a; - Expr ite = em.mkExpr(Kind.ITE, x_eq_a, b, a); - Expr assignment0 = em.mkExpr(Kind.EQUAL, new_x, ite); + Term ite = slv.mkTerm(Kind.ITE, x_eq_a, b, a); + Term assignment0 = slv.mkTerm(Kind.EQUAL, new_x, ite); // Assert the encoding of code (0) - System.out.println("Asserting " + assignment0 + " to CVC4 "); - smt.assertFormula(assignment0); + System.out.println("Asserting " + assignment0 + " to cvc5 "); + slv.assertFormula(assignment0); System.out.println("Pushing a new context."); - smt.push(); + slv.push(); // Encoding code (1) // new_x_ = a xor b xor x - Expr a_xor_b_xor_x = em.mkExpr(Kind.BITVECTOR_XOR, a, b, x); - Expr assignment1 = em.mkExpr(Kind.EQUAL, new_x_, a_xor_b_xor_x); + Term a_xor_b_xor_x = slv.mkTerm(Kind.BITVECTOR_XOR, a, b, x); + Term assignment1 = slv.mkTerm(Kind.EQUAL, new_x_, a_xor_b_xor_x); - // Assert encoding to CVC4 in current context; - System.out.println("Asserting " + assignment1 + " to CVC4 "); - smt.assertFormula(assignment1); - Expr new_x_eq_new_x_ = em.mkExpr(Kind.EQUAL, new_x, new_x_); + // Assert encoding to cvc5 in current context; + System.out.println("Asserting " + assignment1 + " to cvc5 "); + slv.assertFormula(assignment1); + Term new_x_eq_new_x_ = slv.mkTerm(Kind.EQUAL, new_x, new_x_); - System.out.println(" Querying: " + new_x_eq_new_x_); - System.out.println(" Expect entailed. "); - System.out.println(" CVC4: " + smt.checkEntailed(new_x_eq_new_x_)); + System.out.println(" Check entailment assuming: " + new_x_eq_new_x_); + System.out.println(" Expect ENTAILED. "); + System.out.println(" cvc5: " + slv.checkEntailed(new_x_eq_new_x_)); System.out.println(" Popping context. "); - smt.pop(); + slv.pop(); // Encoding code (2) // new_x_ = a + b - x - Expr a_plus_b = em.mkExpr(Kind.BITVECTOR_ADD, a, b); - Expr a_plus_b_minus_x = em.mkExpr(Kind.BITVECTOR_SUB, a_plus_b, x); - Expr assignment2 = em.mkExpr(Kind.EQUAL, new_x_, a_plus_b_minus_x); - - // Assert encoding to CVC4 in current context; - System.out.println("Asserting " + assignment2 + " to CVC4 "); - smt.assertFormula(assignment2); - - System.out.println(" Querying: " + new_x_eq_new_x_); - System.out.println(" Expect entailed. "); - System.out.println(" CVC4: " + smt.checkEntailed(new_x_eq_new_x_)); + Term a_plus_b = slv.mkTerm(Kind.BITVECTOR_ADD, a, b); + Term a_plus_b_minus_x = slv.mkTerm(Kind.BITVECTOR_SUB, a_plus_b, x); + Term assignment2 = slv.mkTerm(Kind.EQUAL, new_x_, a_plus_b_minus_x); + + // Assert encoding to cvc5 in current context; + System.out.println("Asserting " + assignment2 + " to cvc5 "); + slv.assertFormula(assignment2); + + System.out.println(" Check entailment assuming: " + new_x_eq_new_x_); + System.out.println(" Expect ENTAILED. "); + System.out.println(" cvc5: " + slv.checkEntailed(new_x_eq_new_x_)); + + Term x_neq_x = slv.mkTerm(Kind.EQUAL, x, x).notTerm(); + Term[] v = new Term[] {new_x_eq_new_x_, x_neq_x}; + System.out.println(" Check entailment assuming: " + v); + System.out.println(" Expect NOT_ENTAILED. "); + System.out.println(" cvc5: " + slv.checkEntailed(v)); + + // Assert that a is odd + Op extract_op = slv.mkOp(Kind.BITVECTOR_EXTRACT, 0, 0); + Term lsb_of_a = slv.mkTerm(extract_op, a); + System.out.println("Sort of " + lsb_of_a + " is " + lsb_of_a.getSort()); + Term a_odd = slv.mkTerm(Kind.EQUAL, lsb_of_a, slv.mkBitVector(1, 1)); + System.out.println("Assert " + a_odd); + System.out.println("Check satisfiability."); + slv.assertFormula(a_odd); + System.out.println(" Expect sat. "); + System.out.println(" cvc5: " + slv.checkSat()); } -} +}
\ No newline at end of file diff --git a/examples/api/java/BitVectorsAndArrays.java b/examples/api/java/BitVectorsAndArrays.java index 526ee8d99..3e22604dd 100644 --- a/examples/api/java/BitVectorsAndArrays.java +++ b/examples/api/java/BitVectorsAndArrays.java @@ -1,6 +1,6 @@ /****************************************************************************** * Top contributors (to current version): - * Morgan Deters, Liana Hadarean, Andres Noetzli + * Aina Niemetz, Liana Hadarean, Makai Mann * * This file is part of the cvc5 project. * @@ -10,27 +10,27 @@ * directory for licensing information. * **************************************************************************** * - * A simple demonstration of the solving capabilities of the cvc5 bit-vector - * and array solvers. + * A simple demonstration of the solving capabilities of the cvc5 + * bit-vector solver. * */ -import edu.stanford.CVC4.*; +import cvc5.*; import java.util.*; -public class BitVectorsAndArrays { - private static int log2(int n) { +public class BitVectorsAndArrays +{ + private static int log2(int n) + { return (int) Math.round(Math.log(n) / Math.log(2)); } - public static void main(String[] args) { - System.loadLibrary("cvc4jni"); - - ExprManager em = new ExprManager(); - SmtEngine smt = new SmtEngine(em); - smt.setOption("produce-models", new SExpr(true)); // Produce Models - smt.setOption("output-language", new SExpr("smtlib")); // output-language - smt.setLogic("QF_AUFBV"); // Set the logic + public static void main(String[] args) throws CVC5ApiException + { + Solver slv = new Solver(); + slv.setOption("produce-models", "true"); // Produce Models + slv.setOption("output-language", "smtlib"); // output-language + slv.setLogic("QF_AUFBV"); // Set the logic // Consider the following code (where size is some previously defined constant): // @@ -45,54 +45,55 @@ public class BitVectorsAndArrays { // throughout the loop. // Setting up the problem parameters - int k = 4; // number of unrollings (should be a power of 2) + int k = 4; // number of unrollings (should be a power of 2) int index_size = log2(k); // size of the index - - // Types - Type elementType = em.mkBitVectorType(32); - Type indexType = em.mkBitVectorType(index_size); - Type arrayType = em.mkArrayType(indexType, elementType); + // Sorts + Sort elementSort = slv.mkBitVectorSort(32); + Sort indexSort = slv.mkBitVectorSort(index_size); + Sort arraySort = slv.mkArraySort(indexSort, elementSort); // Variables - Expr current_array = em.mkVar("current_array", arrayType); + Term current_array = slv.mkConst(arraySort, "current_array"); // Making a bit-vector constant - Expr zero = em.mkConst(new BitVector(index_size, 0)); + Term zero = slv.mkBitVector(index_size, 0); // Asserting that current_array[0] > 0 - Expr current_array0 = em.mkExpr(Kind.SELECT, current_array, zero); - Expr current_array0_gt_0 = em.mkExpr(Kind.BITVECTOR_SGT, current_array0, em.mkConst(new BitVector(32, 0))); - smt.assertFormula(current_array0_gt_0); + Term current_array0 = slv.mkTerm(Kind.SELECT, current_array, zero); + Term current_array0_gt_0 = + slv.mkTerm(Kind.BITVECTOR_SGT, current_array0, slv.mkBitVector(32, 0)); + slv.assertFormula(current_array0_gt_0); // Building the assertions in the loop unrolling - Expr index = em.mkConst(new BitVector(index_size, 0)); - Expr old_current = em.mkExpr(Kind.SELECT, current_array, index); - Expr two = em.mkConst(new BitVector(32, 2)); - - vectorExpr assertions = new vectorExpr(em); - for (int i = 1; i < k; ++i) { - index = em.mkConst(new BitVector(index_size, new edu.stanford.CVC4.Integer(i))); - Expr new_current = em.mkExpr(Kind.BITVECTOR_MULT, two, old_current); + Term index = slv.mkBitVector(index_size, 0); + Term old_current = slv.mkTerm(Kind.SELECT, current_array, index); + Term two = slv.mkBitVector(32, 2); + + List<Term> assertions = new ArrayList<Term>(); + for (int i = 1; i < k; ++i) + { + index = slv.mkBitVector(index_size, i); + Term new_current = slv.mkTerm(Kind.BITVECTOR_MULT, two, old_current); // current[i] = 2 * current[i-1] - current_array = em.mkExpr(Kind.STORE, current_array, index, new_current); + current_array = slv.mkTerm(Kind.STORE, current_array, index, new_current); // current[i-1] < current [i] - Expr current_slt_new_current = em.mkExpr(Kind.BITVECTOR_SLT, old_current, new_current); + Term current_slt_new_current = slv.mkTerm(Kind.BITVECTOR_SLT, old_current, new_current); assertions.add(current_slt_new_current); - old_current = em.mkExpr(Kind.SELECT, current_array, index); + old_current = slv.mkTerm(Kind.SELECT, current_array, index); } - Expr query = em.mkExpr(Kind.NOT, em.mkExpr(Kind.AND, assertions)); + Term query = slv.mkTerm(Kind.NOT, slv.mkTerm(Kind.AND, assertions.toArray(new Term[0]))); - System.out.println("Asserting " + query + " to CVC4 "); - smt.assertFormula(query); + System.out.println("Asserting " + query + " to cvc5 "); + slv.assertFormula(query); System.out.println("Expect sat. "); - System.out.println("CVC4: " + smt.checkSat(em.mkConst(true))); + System.out.println("cvc5: " + slv.checkSatAssuming(slv.mkTrue())); // Getting the model System.out.println("The satisfying model is: "); - System.out.println(" current_array = " + smt.getValue(current_array)); - System.out.println(" current_array[0] = " + smt.getValue(current_array0)); + System.out.println(" current_array = " + slv.getValue(current_array)); + System.out.println(" current_array[0] = " + slv.getValue(current_array0)); } } diff --git a/examples/api/java/CVC4Streams.java b/examples/api/java/CVC4Streams.java deleted file mode 100644 index 7330b235d..000000000 --- a/examples/api/java/CVC4Streams.java +++ /dev/null @@ -1,59 +0,0 @@ -/****************************************************************************** - * Top contributors (to current version): - * Morgan Deters, Andres Noetzli - * - * This file is part of the cvc5 project. - * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - * in the top-level source directory and their institutional affiliations. - * All rights reserved. See the file COPYING in the top-level source - * directory for licensing information. - * **************************************************************************** - * - * Example of driving CVC4 parsing from Java streams - * - * This example shows how CVC4 can be driven from Java streams. - */ - -import java.io.*; -import edu.stanford.CVC4.*; - -public class CVC4Streams { - public static void main(String[] args) throws IOException { - System.loadLibrary("cvc4jni"); - ExprManager exprMgr = new ExprManager(); - SmtEngine smt = new SmtEngine(exprMgr); - smt.setOption("output-language", new SExpr("smt2")); - - PipedOutputStream solverPipe = new PipedOutputStream(); - PrintWriter toSolver = new PrintWriter(solverPipe); - PipedInputStream stream = new PipedInputStream(solverPipe); - - toSolver.println("(set-logic QF_LIA)"); - toSolver.println("(declare-fun x () Int)"); - toSolver.println("(assert (= x 5))"); - toSolver.println("(check-sat)"); - toSolver.flush(); - - ParserBuilder pbuilder = - new ParserBuilder(exprMgr, "<string 1>") - .withInputLanguage(InputLanguage.INPUT_LANG_SMTLIB_V2) - .withLineBufferedStreamInput((java.io.InputStream)stream); - Parser parser = pbuilder.build(); - - Command cmd; - while((cmd = parser.nextCommand()) != null) { - System.out.println(cmd); - cmd.invoke(smt, System.out); - } - - toSolver.println("(assert (= x 10))"); - toSolver.println("(check-sat)"); - toSolver.flush(); - - while((cmd = parser.nextCommand()) != null) { - System.out.println(cmd); - cmd.invoke(smt, System.out); - } - } -} diff --git a/examples/api/java/Combination.java b/examples/api/java/Combination.java index 0960b7ff3..d25ea849e 100644 --- a/examples/api/java/Combination.java +++ b/examples/api/java/Combination.java @@ -1,6 +1,6 @@ /****************************************************************************** * Top contributors (to current version): - * Morgan Deters, Tim King, Aina Niemetz + * Aina Niemetz, Tim King, Mudathir Mohamed * * This file is part of the cvc5 project. * @@ -10,90 +10,119 @@ * directory for licensing information. * **************************************************************************** * - * A simple demonstration of the capabilities of CVC4 + * A simple demonstration of the capabilities of cvc5 * * A simple demonstration of how to use uninterpreted functions, combining this * with arithmetic, and extracting a model at the end of a satisfiable query. * The model is displayed using getValue(). */ -import edu.stanford.CVC4.*; +import cvc5.*; +import java.util.Iterator; -public class Combination { - private static void prefixPrintGetValue(SmtEngine smt, Expr e, int level) { - for(int i = 0; i < level; ++i) { System.out.print('-'); } - System.out.println("smt.getValue(" + e + ") -> " + smt.getValue(e)); +public class Combination +{ + private static void prefixPrintGetValue(Solver slv, Term t) + { + prefixPrintGetValue(slv, t, 0); + } - if(e.hasOperator()) { - prefixPrintGetValue(smt, e.getOperator(), level + 1); - } + private static void prefixPrintGetValue(Solver slv, Term t, int level) + { + System.out.println("slv.getValue(" + t + "): " + slv.getValue(t)); - for(int i = 0; i < e.getNumChildren(); ++i) { - Expr curr = e.getChild(i); - prefixPrintGetValue(smt, curr, level + 1); + for (Term c : t) + { + prefixPrintGetValue(slv, c, level + 1); } } - public static void main(String[] args) { - System.loadLibrary("cvc4jni"); - - ExprManager em = new ExprManager(); - SmtEngine smt = new SmtEngine(em); - - smt.setOption("tlimit", new SExpr(100)); - smt.setOption("produce-models", new SExpr(true)); // Produce Models - smt.setOption("output-language", new SExpr("cvc4")); // output-language - smt.setOption("dag-thresh", new SExpr(0)); //Disable dagifying the output - smt.setLogic("QF_UFLIRA"); + public static void main(String[] args) throws CVC5ApiException + { + Solver slv = new Solver(); + slv.setOption("produce-models", "true"); // Produce Models + slv.setOption("dag-thresh", "0"); // Disable dagifying the output + slv.setOption("output-language", "smt2"); // use smt-lib v2 as output language + slv.setLogic("QF_UFLIRA"); // Sorts - SortType u = em.mkSort("u"); - Type integer = em.integerType(); - Type booleanType = em.booleanType(); - Type uToInt = em.mkFunctionType(u, integer); - Type intPred = em.mkFunctionType(integer, booleanType); + Sort u = slv.mkUninterpretedSort("u"); + Sort integer = slv.getIntegerSort(); + Sort bool = slv.getBooleanSort(); + Sort uToInt = slv.mkFunctionSort(u, integer); + Sort intPred = slv.mkFunctionSort(integer, bool); // Variables - Expr x = em.mkVar("x", u); - Expr y = em.mkVar("y", u); + Term x = slv.mkConst(u, "x"); + Term y = slv.mkConst(u, "y"); // Functions - Expr f = em.mkVar("f", uToInt); - Expr p = em.mkVar("p", intPred); + Term f = slv.mkConst(uToInt, "f"); + Term p = slv.mkConst(intPred, "p"); // Constants - Expr zero = em.mkConst(new Rational(0)); - Expr one = em.mkConst(new Rational(1)); + Term zero = slv.mkInteger(0); + Term one = slv.mkInteger(1); // Terms - Expr f_x = em.mkExpr(Kind.APPLY_UF, f, x); - Expr f_y = em.mkExpr(Kind.APPLY_UF, f, y); - Expr sum = em.mkExpr(Kind.PLUS, f_x, f_y); - Expr p_0 = em.mkExpr(Kind.APPLY_UF, p, zero); - Expr p_f_y = em.mkExpr(Kind.APPLY_UF, p, f_y); - - // Construct the assumptions - Expr assumptions = - em.mkExpr(Kind.AND, - em.mkExpr(Kind.LEQ, zero, f_x), // 0 <= f(x) - em.mkExpr(Kind.LEQ, zero, f_y), // 0 <= f(y) - em.mkExpr(Kind.LEQ, sum, one), // f(x) + f(y) <= 1 - p_0.notExpr(), // not p(0) - p_f_y); // p(f(y)) - smt.assertFormula(assumptions); - - System.out.println("Given the following assumptions:"); - System.out.println(assumptions); - System.out.println("Prove x /= y is entailed. " - + "CVC4 says: " + smt.checkEntailed(em.mkExpr(Kind.DISTINCT, x, y)) - + "."); - - System.out.println("Now we call checksat on a trivial query to show that"); - System.out.println("the assumptions are satisfiable: " + - smt.checkSat(em.mkConst(true)) + "."); - - System.out.println("Finally, after a SAT call, we recursively call smt.getValue(...) on " + - "all of the assumptions to see what the satisfying model looks like."); - prefixPrintGetValue(smt, assumptions, 0); + Term f_x = slv.mkTerm(Kind.APPLY_UF, f, x); + Term f_y = slv.mkTerm(Kind.APPLY_UF, f, y); + Term sum = slv.mkTerm(Kind.PLUS, f_x, f_y); + Term p_0 = slv.mkTerm(Kind.APPLY_UF, p, zero); + Term p_f_y = slv.mkTerm(Kind.APPLY_UF, p, f_y); + + // Construct the assertions + Term assertions = slv.mkTerm(Kind.AND, + new Term[] { + slv.mkTerm(Kind.LEQ, zero, f_x), // 0 <= f(x) + slv.mkTerm(Kind.LEQ, zero, f_y), // 0 <= f(y) + slv.mkTerm(Kind.LEQ, sum, one), // f(x) + f(y) <= 1 + p_0.notTerm(), // not p(0) + p_f_y // p(f(y)) + }); + slv.assertFormula(assertions); + + System.out.println("Given the following assertions:\n" + assertions + "\n"); + + System.out.println("Prove x /= y is entailed. \n" + + "cvc5: " + slv.checkEntailed(slv.mkTerm(Kind.DISTINCT, x, y)) + ".\n"); + + System.out.println("Call checkSat to show that the assertions are satisfiable. \n" + + "cvc5: " + slv.checkSat() + ".\n"); + + System.out.println("Call slv.getValue(...) on terms of interest."); + System.out.println("slv.getValue(" + f_x + "): " + slv.getValue(f_x)); + System.out.println("slv.getValue(" + f_y + "): " + slv.getValue(f_y)); + System.out.println("slv.getValue(" + sum + "): " + slv.getValue(sum)); + System.out.println("slv.getValue(" + p_0 + "): " + slv.getValue(p_0)); + System.out.println("slv.getValue(" + p_f_y + "): " + slv.getValue(p_f_y) + "\n"); + + System.out.println("Alternatively, iterate over assertions and call slv.getValue(...) " + + "on all terms."); + prefixPrintGetValue(slv, assertions); + + System.out.println(); + System.out.println("You can also use nested loops to iterate over terms."); + Iterator<Term> it1 = assertions.iterator(); + while (it1.hasNext()) + { + Term t = it1.next(); + System.out.println("term: " + t); + Iterator<Term> it2 = t.iterator(); + while (it2.hasNext()) + { + System.out.println(" + child: " + it2.next()); + } + } + System.out.println(); + System.out.println("Alternatively, you can also use for-each loops."); + for (Term t : assertions) + { + System.out.println("term: " + t); + for (Term c : t) + { + System.out.println(" + child: " + c); + } + } } } diff --git a/examples/api/java/Datatypes.java b/examples/api/java/Datatypes.java index d4dd85d2b..b230affd5 100644 --- a/examples/api/java/Datatypes.java +++ b/examples/api/java/Datatypes.java @@ -1,6 +1,6 @@ /****************************************************************************** * Top contributors (to current version): - * Morgan Deters, Andres Noetzli, Andrew Reynolds + * Aina Niemetz, Morgan Deters, Andrew Reynolds * * This file is part of the cvc5 project. * @@ -10,93 +10,159 @@ * directory for licensing information. * **************************************************************************** * - * An example of using inductive datatypes in CVC4 (Java version). + * An example of using inductive datatypes in cvc5. */ -import edu.stanford.CVC4.*; +import cvc5.*; import java.util.Iterator; -public class Datatypes { - public static void main(String[] args) { - System.loadLibrary("cvc4jni"); - - ExprManager em = new ExprManager(); - SmtEngine smt = new SmtEngine(em); - - // This example builds a simple "cons list" of integers, with - // two constructors, "cons" and "nil." - - // Building a datatype consists of two steps. First, the datatype - // is specified. Second, it is "resolved"---at which point function - // symbols are assigned to its constructors, selectors, and testers. - - Datatype consListSpec = new Datatype(em, "list"); // give a name - DatatypeConstructor cons = new DatatypeConstructor(em, "cons"); - cons.addArg("head", em.integerType()); - cons.addArg("tail", new DatatypeSelfType()); // a list - consListSpec.addConstructor(cons); - DatatypeConstructor nil = new DatatypeConstructor(em, "nil"); - consListSpec.addConstructor(nil); - - System.out.println("spec is:"); - System.out.println(consListSpec); - - // Keep in mind that "Datatype" is the specification class for - // datatypes---"Datatype" is not itself a CVC4 Type. Now that - // our Datatype is fully specified, we can get a Type for it. - // This step resolves the "SelfType" reference and creates - // symbols for all the constructors, etc. - - DatatypeType consListType = em.mkDatatypeType(consListSpec); - +public class Datatypes +{ + private static void test(Solver slv, Sort consListSort) throws CVC5ApiException + { // Now our old "consListSpec" is useless--the relevant information // has been copied out, so we can throw that spec away. We can get - // the complete spec for the datatype from the DatatypeType, and + // the complete spec for the datatype from the DatatypeSort, and // this Datatype object has constructor symbols (and others) filled in. - Datatype consList = consListType.getDatatype(); + Datatype consList = consListSort.getDatatype(); - // e = cons 0 nil + // t = cons 0 nil // - // Here, consList.get("cons") gives you the DatatypeConstructor - // (just as consList["cons"] does in C++). To get the constructor - // symbol for application, use .getConstructor("cons"), which is - // equivalent to consList.get("cons").getConstructor(). Note that + // Here, consList["cons"] gives you the DatatypeConstructor. To get + // the constructor symbol for application, use .getConstructor("cons"), + // which is equivalent to consList["cons"].getConstructor(). Note that // "nil" is a constructor too, so it needs to be applied with // APPLY_CONSTRUCTOR, even though it has no arguments. - Expr e = em.mkExpr(Kind.APPLY_CONSTRUCTOR, - consList.getConstructor("cons"), - em.mkConst(new Rational(0)), - em.mkExpr(Kind.APPLY_CONSTRUCTOR, - consList.getConstructor("nil"))); - - System.out.println("e is " + e); - System.out.println("type of cons is " + - consList.getConstructor("cons").getType()); - System.out.println("type of nil is " + - consList.getConstructor("nil").getType()); - - // e2 = head(cons 0 nil), and of course this can be evaluated + Term t = slv.mkTerm(Kind.APPLY_CONSTRUCTOR, + consList.getConstructorTerm("cons"), + slv.mkInteger(0), + slv.mkTerm(Kind.APPLY_CONSTRUCTOR, consList.getConstructorTerm("nil"))); + + System.out.println("t is " + t + "\n" + + "sort of cons is " + consList.getConstructorTerm("cons").getSort() + "\n" + + "sort of nil is " + consList.getConstructorTerm("nil").getSort()); + + // t2 = head(cons 0 nil), and of course this can be evaluated // // Here we first get the DatatypeConstructor for cons (with - // consList.get("cons") in order to get the "head" selector - // symbol to apply. - Expr e2 = em.mkExpr(Kind.APPLY_SELECTOR, - consList.get("cons").getSelector("head"), - e); - - System.out.println("e2 is " + e2); - System.out.println("simplify(e2) is " + smt.simplify(e2)); - System.out.println(); + // consList["cons"]) in order to get the "head" selector symbol + // to apply. + Term t2 = + slv.mkTerm(Kind.APPLY_SELECTOR, consList.getConstructor("cons").getSelectorTerm("head"), t); + + System.out.println("t2 is " + t2 + "\n" + + "simplify(t2) is " + slv.simplify(t2) + "\n"); // You can also iterate over a Datatype to get all its constructors, // and over a DatatypeConstructor to get all its "args" (selectors) - for(Iterator<DatatypeConstructor> i = consList.iterator(); i.hasNext();) { - DatatypeConstructor ctor = i.next(); - System.out.println("ctor: " + ctor); - for(Iterator j = ctor.iterator(); j.hasNext();) { + + for (Iterator<DatatypeConstructor> i = consList.iterator(); i.hasNext();) + { + DatatypeConstructor constructor = i.next(); + System.out.println("ctor: " + constructor); + for (Iterator<DatatypeSelector> j = constructor.iterator(); j.hasNext();) + { System.out.println(" + arg: " + j.next()); } } + System.out.println("\n"); + + // Alternatively, you can use for each loops. + for (DatatypeConstructor c : consList) + { + System.out.println("ctor: " + c); + for (DatatypeSelector s : c) + { + System.out.println(" + arg: " + s); + } + } + System.out.println(); + + // You can also define parameterized datatypes. + // This example builds a simple parameterized list of sort T, with one + // constructor "cons". + Sort sort = slv.mkParamSort("T"); + DatatypeDecl paramConsListSpec = slv.mkDatatypeDecl("paramlist", + sort); // give the datatype a name + DatatypeConstructorDecl paramCons = slv.mkDatatypeConstructorDecl("cons"); + DatatypeConstructorDecl paramNil = slv.mkDatatypeConstructorDecl("nil"); + paramCons.addSelector("head", sort); + paramCons.addSelectorSelf("tail"); + paramConsListSpec.addConstructor(paramCons); + paramConsListSpec.addConstructor(paramNil); + + Sort paramConsListSort = slv.mkDatatypeSort(paramConsListSpec); + Sort paramConsIntListSort = paramConsListSort.instantiate(new Sort[] {slv.getIntegerSort()}); + + Datatype paramConsList = paramConsListSort.getDatatype(); + + System.out.println("parameterized datatype sort is "); + for (DatatypeConstructor ctor : paramConsList) + { + System.out.println("ctor: " + ctor); + for (DatatypeSelector stor : ctor) + { + System.out.println(" + arg: " + stor); + } + } + + Term a = slv.mkConst(paramConsIntListSort, "a"); + System.out.println("term " + a + " is of sort " + a.getSort()); + + Term head_a = slv.mkTerm( + Kind.APPLY_SELECTOR, paramConsList.getConstructor("cons").getSelectorTerm("head"), a); + System.out.println("head_a is " + head_a + " of sort " + head_a.getSort() + "\n" + + "sort of cons is " + paramConsList.getConstructorTerm("cons").getSort() + "\n"); + Term assertion = slv.mkTerm(Kind.GT, head_a, slv.mkInteger(50)); + System.out.println("Assert " + assertion); + slv.assertFormula(assertion); + System.out.println("Expect sat."); + System.out.println("cvc5: " + slv.checkSat()); + } + + public static void main(String[] args) throws CVC5ApiException + { + Solver slv = new Solver(); + // This example builds a simple "cons list" of integers, with + // two constructors, "cons" and "nil." + + // Building a datatype consists of two steps. + // First, the datatype is specified. + // Second, it is "resolved" to an actual sort, at which point function + // symbols are assigned to its constructors, selectors, and testers. + + DatatypeDecl consListSpec = slv.mkDatatypeDecl("list"); // give the datatype a name + DatatypeConstructorDecl cons = slv.mkDatatypeConstructorDecl("cons"); + cons.addSelector("head", slv.getIntegerSort()); + cons.addSelectorSelf("tail"); + consListSpec.addConstructor(cons); + DatatypeConstructorDecl nil = slv.mkDatatypeConstructorDecl("nil"); + consListSpec.addConstructor(nil); + + System.out.println("spec is:" + + "\n" + consListSpec); + + // Keep in mind that "DatatypeDecl" is the specification class for + // datatypes---"DatatypeDecl" is not itself a cvc5 Sort. + // Now that our Datatype is fully specified, we can get a Sort for it. + // This step resolves the "SelfSort" reference and creates + // symbols for all the constructors, etc. + + Sort consListSort = slv.mkDatatypeSort(consListSpec); + + test(slv, consListSort); + + System.out.println("\n" + + ">>> Alternatively, use declareDatatype"); + System.out.println("\n"); + + DatatypeConstructorDecl cons2 = slv.mkDatatypeConstructorDecl("cons"); + cons2.addSelector("head", slv.getIntegerSort()); + cons2.addSelectorSelf("tail"); + DatatypeConstructorDecl nil2 = slv.mkDatatypeConstructorDecl("nil"); + DatatypeConstructorDecl[] ctors = new DatatypeConstructorDecl[] {cons2, nil2}; + Sort consListSort2 = slv.declareDatatype("list2", ctors); + test(slv, consListSort2); } } diff --git a/examples/api/java/Exceptions.java b/examples/api/java/Exceptions.java index c8aa678c6..bf87fc6be 100644 --- a/examples/api/java/Exceptions.java +++ b/examples/api/java/Exceptions.java @@ -15,42 +15,50 @@ * A simple demonstration of catching CVC4 execptions via the Java API. */ -import edu.stanford.CVC4.*; +import cvc5.*; -public class Exceptions { - public static void main(String[] args) { - System.loadLibrary("cvc4jni"); +public class Exceptions +{ + public static void main(String[] args) + { + Solver solver = new Solver(); - ExprManager em = new ExprManager(); - SmtEngine smt = new SmtEngine(em); - - smt.setOption("produce-models", new SExpr(true)); + solver.setOption("produce-models", "true"); // Setting an invalid option - try { - smt.setOption("non-existing", new SExpr(true)); + try + { + solver.setOption("non-existing", "true"); System.exit(1); - } catch (edu.stanford.CVC4.Exception e) { + } + catch (Exception e) + { System.out.println(e.toString()); } // Creating a term with an invalid type - try { - Type integer = em.integerType(); - Expr x = em.mkVar("x", integer); - Expr invalidExpr = em.mkExpr(Kind.AND, x, x); - smt.checkSat(invalidExpr); + try + { + Sort integer = solver.getIntegerSort(); + Term x = solver.mkVar(integer, "x"); + Term invalidTerm = solver.mkTerm(Kind.AND, x, x); + solver.checkSatAssuming(invalidTerm); System.exit(1); - } catch (edu.stanford.CVC4.Exception e) { + } + catch (Exception e) + { System.out.println(e.toString()); } // Asking for a model after unsat result - try { - smt.checkSat(em.mkConst(false)); - smt.getModel(); + try + { + solver.checkSatAssuming(solver.mkBoolean(false)); + solver.getModel(new Sort[] {}, new Term[] {}); System.exit(1); - } catch (edu.stanford.CVC4.Exception e) { + } + catch (Exception e) + { System.out.println(e.toString()); } } diff --git a/examples/api/java/Extract.java b/examples/api/java/Extract.java new file mode 100644 index 000000000..d86b7b1ef --- /dev/null +++ b/examples/api/java/Extract.java @@ -0,0 +1,52 @@ +/****************************************************************************** + * Top contributors (to current version): + * Aina Niemetz, Makai Mann, Clark Barrett + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * A simple demonstration of the solving capabilities of the cvc5 + * bit-vector solver. + * + */ + +import cvc5.*; + +public class Extract +{ + public static void main(String args[]) throws CVC5ApiException + { + Solver slv = new Solver(); + slv.setLogic("QF_BV"); // Set the logic + + Sort bitvector32 = slv.mkBitVectorSort(32); + + Term x = slv.mkConst(bitvector32, "a"); + + Op ext_31_1 = slv.mkOp(Kind.BITVECTOR_EXTRACT, 31, 1); + Term x_31_1 = slv.mkTerm(ext_31_1, x); + + Op ext_30_0 = slv.mkOp(Kind.BITVECTOR_EXTRACT, 30, 0); + Term x_30_0 = slv.mkTerm(ext_30_0, x); + + Op ext_31_31 = slv.mkOp(Kind.BITVECTOR_EXTRACT, 31, 31); + Term x_31_31 = slv.mkTerm(ext_31_31, x); + + Op ext_0_0 = slv.mkOp(Kind.BITVECTOR_EXTRACT, 0, 0); + Term x_0_0 = slv.mkTerm(ext_0_0, x); + + Term eq = slv.mkTerm(Kind.EQUAL, x_31_1, x_30_0); + System.out.println(" Asserting: " + eq); + slv.assertFormula(eq); + + Term eq2 = slv.mkTerm(Kind.EQUAL, x_31_31, x_0_0); + System.out.println(" Check entailment assuming: " + eq2); + System.out.println(" Expect ENTAILED. "); + System.out.println(" cvc5: " + slv.checkEntailed(eq2)); + } +}
\ No newline at end of file diff --git a/examples/api/java/FloatingPointArith.java b/examples/api/java/FloatingPointArith.java index 46f8b8330..dda5bbcd0 100644 --- a/examples/api/java/FloatingPointArith.java +++ b/examples/api/java/FloatingPointArith.java @@ -10,103 +10,92 @@ * directory for licensing information. * **************************************************************************** * - * An example of solving floating-point problems with CVC4's Java API + * An example of solving floating-point problems with cvc5's Java API * - * This example shows how to check whether CVC4 was built with floating-point - * support, how to create floating-point types, variables and expressions, and - * how to create rounding mode constants by solving toy problems. The example - * also shows making special values (such as NaN and +oo) and converting an - * IEEE 754-2008 bit-vector to a floating-point number. + * This example shows to create floating-point types, variables and expressions, + * and how to create rounding mode constants by solving toy problems. The + * example also shows making special values (such as NaN and +oo) and converting + * an IEEE 754-2008 bit-vector to a floating-point number. */ -import edu.stanford.CVC4.*; -import java.util.Iterator; +import static cvc5.Kind.*; -public class FloatingPointArith { - public static void main(String[] args) { - System.loadLibrary("cvc4jni"); +import cvc5.*; - // Test whether CVC4 was built with floating-point support - ExprManager em = new ExprManager(); - SmtEngine smt = new SmtEngine(em); - - // Enable the model production - smt.setOption("produce-models", new SExpr(true)); +public class FloatingPointArith +{ + public static void main(String[] args) throws CVC5ApiException + { + Solver solver = new Solver(); + solver.setOption("produce-models", "true"); // Make single precision floating-point variables - FloatingPointType fpt32 = em.mkFloatingPointType(8, 24); - Expr a = em.mkVar("a", fpt32); - Expr b = em.mkVar("b", fpt32); - Expr c = em.mkVar("c", fpt32); - Expr d = em.mkVar("d", fpt32); - Expr e = em.mkVar("e", fpt32); + Sort fpt32 = solver.mkFloatingPointSort(8, 24); + Term a = solver.mkConst(fpt32, "a"); + Term b = solver.mkConst(fpt32, "b"); + Term c = solver.mkConst(fpt32, "c"); + Term d = solver.mkConst(fpt32, "d"); + Term e = solver.mkConst(fpt32, "e"); // Assert that floating-point addition is not associative: // (a + (b + c)) != ((a + b) + c) - Expr rm = em.mkConst(RoundingMode.roundNearestTiesToEven); - Expr lhs = em.mkExpr(Kind.FLOATINGPOINT_ADD, - rm, - a, - em.mkExpr(Kind.FLOATINGPOINT_ADD, rm, b, c)); - Expr rhs = em.mkExpr(Kind.FLOATINGPOINT_ADD, - rm, - em.mkExpr(Kind.FLOATINGPOINT_ADD, rm, a, b), - c); - smt.assertFormula(em.mkExpr(Kind.NOT, em.mkExpr(Kind.EQUAL, a, b))); + Term rm = solver.mkRoundingMode(RoundingMode.ROUND_NEAREST_TIES_TO_EVEN); + Term lhs = solver.mkTerm( + Kind.FLOATINGPOINT_ADD, rm, a, solver.mkTerm(Kind.FLOATINGPOINT_ADD, rm, b, c)); + Term rhs = solver.mkTerm( + Kind.FLOATINGPOINT_ADD, rm, solver.mkTerm(Kind.FLOATINGPOINT_ADD, rm, a, b), c); + solver.assertFormula(solver.mkTerm(Kind.NOT, solver.mkTerm(Kind.EQUAL, a, b))); - Result r = smt.checkSat(); // result is sat - assert r.isSat() == Result.Sat.SAT; + Result r = solver.checkSat(); // result is sat + assert r.isSat(); - System.out.println("a = " + smt.getValue(a)); - System.out.println("b = " + smt.getValue(b)); - System.out.println("c = " + smt.getValue(c)); + System.out.println("a = " + solver.getValue(a)); + System.out.println("b = " + solver.getValue(b)); + System.out.println("c = " + solver.getValue(c)); // Now, let's restrict `a` to be either NaN or positive infinity - FloatingPointSize fps32 = new FloatingPointSize(8, 24); - Expr nan = em.mkConst(FloatingPoint.makeNaN(fps32)); - Expr inf = em.mkConst(FloatingPoint.makeInf(fps32, /* sign */ true)); - smt.assertFormula(em.mkExpr( - Kind.OR, em.mkExpr(Kind.EQUAL, a, inf), em.mkExpr(Kind.EQUAL, a, nan))); + Term nan = solver.mkNaN(8, 24); + Term inf = solver.mkPosInf(8, 24); + solver.assertFormula(solver.mkTerm( + Kind.OR, solver.mkTerm(Kind.EQUAL, a, inf), solver.mkTerm(Kind.EQUAL, a, nan))); - r = smt.checkSat(); // result is sat - assert r.isSat() == Result.Sat.SAT; + r = solver.checkSat(); // result is sat + assert r.isSat(); - System.out.println("a = " + smt.getValue(a)); - System.out.println("b = " + smt.getValue(b)); - System.out.println("c = " + smt.getValue(c)); + System.out.println("a = " + solver.getValue(a)); + System.out.println("b = " + solver.getValue(b)); + System.out.println("c = " + solver.getValue(c)); // And now for something completely different. Let's try to find a (normal) // floating-point number that rounds to different integer values for // different rounding modes. - Expr rtp = em.mkConst(RoundingMode.roundTowardPositive); - Expr rtn = em.mkConst(RoundingMode.roundTowardNegative); - Expr op = em.mkConst(new FloatingPointToSBV(16)); // (_ fp.to_sbv 16) - lhs = em.mkExpr(op, rtp, d); - rhs = em.mkExpr(op, rtn, d); - smt.assertFormula(em.mkExpr(Kind.FLOATINGPOINT_ISN, d)); - smt.assertFormula(em.mkExpr(Kind.NOT, em.mkExpr(Kind.EQUAL, lhs, rhs))); + Term rtp = solver.mkRoundingMode(RoundingMode.ROUND_TOWARD_POSITIVE); + Term rtn = solver.mkRoundingMode(RoundingMode.ROUND_TOWARD_NEGATIVE); + Op op = solver.mkOp(Kind.FLOATINGPOINT_TO_SBV, 16); // (_ fp.to_sbv 16) + lhs = solver.mkTerm(op, rtp, d); + rhs = solver.mkTerm(op, rtn, d); + solver.assertFormula(solver.mkTerm(Kind.FLOATINGPOINT_ISN, d)); + solver.assertFormula(solver.mkTerm(Kind.NOT, solver.mkTerm(Kind.EQUAL, lhs, rhs))); - r = smt.checkSat(); // result is sat - assert r.isSat() == Result.Sat.SAT; + r = solver.checkSat(); // result is sat + assert r.isSat(); // Convert the result to a rational and print it - Expr val = smt.getValue(d); - Rational realVal = - val.getConstFloatingPoint().convertToRationalTotal(new Rational(0)); + Term val = solver.getValue(d); + Term realVal = solver.getValue(solver.mkTerm(FLOATINGPOINT_TO_REAL, val)); System.out.println("d = " + val + " = " + realVal); - System.out.println("((_ fp.to_sbv 16) RTP d) = " + smt.getValue(lhs)); - System.out.println("((_ fp.to_sbv 16) RTN d) = " + smt.getValue(rhs)); + System.out.println("((_ fp.to_sbv 16) RTP d) = " + solver.getValue(lhs)); + System.out.println("((_ fp.to_sbv 16) RTN d) = " + solver.getValue(rhs)); // For our final trick, let's try to find a floating-point number between // positive zero and the smallest positive floating-point number - Expr zero = em.mkConst(FloatingPoint.makeZero(fps32, /* sign */ true)); - Expr smallest = - em.mkConst(new FloatingPoint(8, 24, new BitVector(32, 0b001))); - smt.assertFormula(em.mkExpr(Kind.AND, - em.mkExpr(Kind.FLOATINGPOINT_LT, zero, e), - em.mkExpr(Kind.FLOATINGPOINT_LT, e, smallest))); - - r = smt.checkSat(); // result is unsat - assert r.isSat() == Result.Sat.UNSAT; + Term zero = solver.mkPosZero(8, 24); + Term smallest = solver.mkFloatingPoint(8, 24, solver.mkBitVector(32, 0b001)); + solver.assertFormula(solver.mkTerm(Kind.AND, + solver.mkTerm(Kind.FLOATINGPOINT_LT, zero, e), + solver.mkTerm(Kind.FLOATINGPOINT_LT, e, smallest))); + + r = solver.checkSat(); // result is unsat + assert !r.isSat(); } } diff --git a/examples/api/java/HelloWorld.java b/examples/api/java/HelloWorld.java index 4cd4fae6a..1013c0a9e 100644 --- a/examples/api/java/HelloWorld.java +++ b/examples/api/java/HelloWorld.java @@ -10,19 +10,18 @@ * directory for licensing information. * **************************************************************************** * - * A very simple CVC4 tutorial example. + * A very simple CVC5 tutorial example. */ -import edu.stanford.CVC4.*; +import cvc5.*; -public class HelloWorld { - public static void main(String[] args) { - System.loadLibrary("cvc4jni"); +public class HelloWorld +{ + public static void main(String[] args) + { + Solver slv = new Solver(); + Term helloworld = slv.mkVar(slv.getBooleanSort(), "Hello World!"); - ExprManager em = new ExprManager(); - Expr helloworld = em.mkVar("Hello World!", em.booleanType()); - SmtEngine smt = new SmtEngine(em); - - System.out.println(helloworld + " is " + smt.checkEntailed(helloworld)); + System.out.println(helloworld + " is " + slv.checkEntailed(helloworld)); } } diff --git a/examples/api/java/LinearArith.java b/examples/api/java/LinearArith.java index 08f3792d6..0c728894a 100644 --- a/examples/api/java/LinearArith.java +++ b/examples/api/java/LinearArith.java @@ -1,6 +1,6 @@ /****************************************************************************** * Top contributors (to current version): - * Morgan Deters, Tim King, Aina Niemetz + * Aina Niemetz, Tim King, Mudathir Mohamed * * This file is part of the cvc5 project. * @@ -11,71 +11,65 @@ * **************************************************************************** * * A simple demonstration of the linear arithmetic solving capabilities and - * the push pop of CVC4. This also gives an example option. + * the push pop of cvc5. This also gives an example option. */ -import edu.stanford.CVC4.*; - -public class LinearArith { - public static void main(String[] args) { - System.loadLibrary("cvc4jni"); - - ExprManager em = new ExprManager(); - SmtEngine smt = new SmtEngine(em); - - smt.setLogic("QF_LIRA"); // Set the logic +import cvc5.*; +public class LinearArith +{ + public static void main(String args[]) throws CVC5ApiException + { + Solver slv = new Solver(); + slv.setLogic("QF_LIRA"); // Set the logic // Prove that if given x (Integer) and y (Real) then // the maximum value of y - x is 2/3 - // Types - Type real = em.realType(); - Type integer = em.integerType(); + // Sorts + Sort real = slv.getRealSort(); + Sort integer = slv.getIntegerSort(); // Variables - Expr x = em.mkVar("x", integer); - Expr y = em.mkVar("y", real); + Term x = slv.mkConst(integer, "x"); + Term y = slv.mkConst(real, "y"); // Constants - Expr three = em.mkConst(new Rational(3)); - Expr neg2 = em.mkConst(new Rational(-2)); - Expr two_thirds = em.mkConst(new Rational(2,3)); + Term three = slv.mkInteger(3); + Term neg2 = slv.mkInteger(-2); + Term two_thirds = slv.mkReal(2, 3); // Terms - Expr three_y = em.mkExpr(Kind.MULT, three, y); - Expr diff = em.mkExpr(Kind.MINUS, y, x); + Term three_y = slv.mkTerm(Kind.MULT, three, y); + Term diff = slv.mkTerm(Kind.MINUS, y, x); // Formulas - Expr x_geq_3y = em.mkExpr(Kind.GEQ, x, three_y); - Expr x_leq_y = em.mkExpr(Kind.LEQ, x, y); - Expr neg2_lt_x = em.mkExpr(Kind.LT, neg2, x); - - Expr assumptions = - em.mkExpr(Kind.AND, x_geq_3y, x_leq_y, neg2_lt_x); + Term x_geq_3y = slv.mkTerm(Kind.GEQ, x, three_y); + Term x_leq_y = slv.mkTerm(Kind.LEQ, x, y); + Term neg2_lt_x = slv.mkTerm(Kind.LT, neg2, x); - System.out.println("Given the assumptions " + assumptions); - smt.assertFormula(assumptions); + Term assertions = slv.mkTerm(Kind.AND, x_geq_3y, x_leq_y, neg2_lt_x); + System.out.println("Given the assertions " + assertions); + slv.assertFormula(assertions); - smt.push(); - Expr diff_leq_two_thirds = em.mkExpr(Kind.LEQ, diff, two_thirds); - System.out.println("Prove that " + diff_leq_two_thirds + " with CVC4."); - System.out.println("CVC4 should report ENTAILED."); - System.out.println( - "Result from CVC4 is: " + smt.checkEntailed(diff_leq_two_thirds)); - smt.pop(); + slv.push(); + Term diff_leq_two_thirds = slv.mkTerm(Kind.LEQ, diff, two_thirds); + System.out.println("Prove that " + diff_leq_two_thirds + " with cvc5."); + System.out.println("cvc5 should report ENTAILED."); + System.out.println("Result from cvc5 is: " + slv.checkEntailed(diff_leq_two_thirds)); + slv.pop(); System.out.println(); - smt.push(); - Expr diff_is_two_thirds = em.mkExpr(Kind.EQUAL, diff, two_thirds); - smt.assertFormula(diff_is_two_thirds); - System.out.println("Show that the asserts are consistent with "); - System.out.println(diff_is_two_thirds + " with CVC4."); - System.out.println("CVC4 should report SAT."); - System.out.println("Result from CVC4 is: " + smt.checkSat(em.mkConst(true))); - smt.pop(); + slv.push(); + Term diff_is_two_thirds = slv.mkTerm(Kind.EQUAL, diff, two_thirds); + slv.assertFormula(diff_is_two_thirds); + System.out.println("Show that the assertions are consistent with "); + System.out.println(diff_is_two_thirds + " with cvc5."); + System.out.println("cvc5 should report SAT."); + System.out.println("Result from cvc5 is: " + slv.checkSat()); + slv.pop(); System.out.println("Thus the maximum value of (y - x) is 2/3."); } -} +}
\ No newline at end of file diff --git a/examples/api/java/PipedInput.java b/examples/api/java/PipedInput.java deleted file mode 100644 index db6c1f902..000000000 --- a/examples/api/java/PipedInput.java +++ /dev/null @@ -1,66 +0,0 @@ -/****************************************************************************** - * Top contributors (to current version): - * Morgan Deters, Andres Noetzli - * - * This file is part of the cvc5 project. - * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - * in the top-level source directory and their institutional affiliations. - * All rights reserved. See the file COPYING in the top-level source - * directory for licensing information. - * **************************************************************************** - * - * A simple demonstration of the input parsing capabilities of CVC4 when - * used from Java. - */ - -import edu.stanford.CVC4.*; -import java.io.*; - -public class PipedInput { - public static void main(String[] args) throws IOException { - System.loadLibrary("cvc4jni"); - - // Boilerplate setup for CVC4 - ExprManager exprMgr = new ExprManager(); - SmtEngine smt = new SmtEngine(exprMgr); - smt.setOption("output-language", new SExpr("smt2")); - - // Set up a pair of connected Java streams - PipedOutputStream solverPipe = new PipedOutputStream(); - PrintWriter toSolver = new PrintWriter(solverPipe); - PipedInputStream stream = new PipedInputStream(solverPipe); - - // Write some things to CVC4's input stream, making sure to flush() - toSolver.println("(set-logic QF_LIA)"); - toSolver.println("(declare-fun x () Int)"); - toSolver.println("(assert (= x 5))"); - toSolver.println("(check-sat)"); - toSolver.flush(); - - // Set up the CVC4 parser - ParserBuilder pbuilder = - new ParserBuilder(exprMgr, "<string 1>") - .withInputLanguage(InputLanguage.INPUT_LANG_SMTLIB_V2) - .withLineBufferedStreamInput((java.io.InputStream)stream); - Parser parser = pbuilder.build(); - - // Read all the commands thus far - Command cmd; - while((cmd = parser.nextCommand()) != null) { - System.out.println(cmd); - cmd.invoke(smt, System.out); - } - - // Write some more things to CVC4's input stream, making sure to flush() - toSolver.println("(assert (= x 10))"); - toSolver.println("(check-sat)"); - toSolver.flush(); - - // Read all the commands thus far - while((cmd = parser.nextCommand()) != null) { - System.out.println(cmd); - cmd.invoke(smt, System.out); - } - } -} diff --git a/examples/api/java/QuickStart.java b/examples/api/java/QuickStart.java new file mode 100644 index 000000000..4e1798d39 --- /dev/null +++ b/examples/api/java/QuickStart.java @@ -0,0 +1,147 @@ +/****************************************************************************** + * Top contributors (to current version): + * Yoni Zohar + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * A simple demonstration of the api capabilities of cvc5. + * + */ + +import cvc5.*; +import java.math.BigInteger; +import java.util.ArrayList; +import java.util.Arrays; +import java.util.List; + +public class QuickStart +{ + public static void main(String args[]) throws CVC5ApiException + { + // Create a solver + Solver solver = new Solver(); + + // We will ask the solver to produce models and unsat cores, + // hence these options should be turned on. + solver.setOption("produce-models", "true"); + solver.setOption("produce-unsat-cores", "true"); + + // 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". + + // Set the logic + solver.setLogic("ALL"); + + // In this example, we will define constraints over reals and integers. + // Hence, we first obtain the corresponding sorts. + Sort realSort = solver.getRealSort(); + Sort intSort = solver.getIntegerSort(); + + // x and y will be real variables, while a and b will be integer variables. + // Formally, their cpp type is Term, + // and they are called "constants" in SMT jargon: + Term x = solver.mkConst(realSort, "x"); + Term y = solver.mkConst(realSort, "y"); + Term a = solver.mkConst(intSort, "a"); + Term b = solver.mkConst(intSort, "b"); + + // Our constraints regarding x and y will be: + // + // (1) 0 < x + // (2) 0 < y + // (3) x + y < 1 + // (4) x <= y + // + + // 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.PLUS, x, y); + + // Now we can define the constraints. + // They use the operators +, <=, and <. + // In the API, these are denoted by PLUS, 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); + + // Check if the formula is satisfiable, that is, + // are there real values for x and y that satisfy all the constraints? + Result r1 = solver.checkSat(); + + // The result is either SAT, UNSAT, or UNKNOWN. + // In this case, it is SAT. + System.out.println("expected: sat"); + System.out.println("result: " + r1); + + // We can get 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 compound terms, + // even if those did not appear in the original formula. + Term xMinusY = solver.mkTerm(Kind.MINUS, x, y); + Term xMinusYVal = solver.getValue(xMinusY); + + // Further, we can convert the values to java types, + Pair<BigInteger, BigInteger> xRational = xVal.getRealValue(); + Pair<BigInteger, BigInteger> yRational = yVal.getRealValue(); + System.out.println("value for x: " + xRational.first + "/" + xRational.second); + System.out.println("value for y: " + yRational.first + "/" + yRational.second); + + // Next, we will check satisfiability of the same formula, + // only this time over integer variables a and b. + + // We start by resetting assertions added to the solver. + solver.resetAssertions(); + + // Next, we assert the same assertions above with integers. + // This time, we inline the construction of terms + // to 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.PLUS, a, b), solver.mkInteger(1))); + solver.assertFormula(solver.mkTerm(Kind.LEQ, a, b)); + + // 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); + + // We can query the solver for an unsatisfiable core, i.e., 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); + } + } +}
\ No newline at end of file diff --git a/examples/api/java/Relations.java b/examples/api/java/Relations.java index 9a6beb6cc..cfcbb3b8e 100644 --- a/examples/api/java/Relations.java +++ b/examples/api/java/Relations.java @@ -13,7 +13,9 @@ * A simple demonstration of reasoning about relations with CVC4 via Java API. */ -import edu.stanford.CVC4.*; +import static cvc5.Kind.*; + +import cvc5.*; /* This file uses the API to make a sat call equivalent to the following benchmark: @@ -63,155 +65,133 @@ This file uses the API to make a sat call equivalent to the following benchmark: (get-model) */ -public class Relations { - public static void main(String[] args) { - System.loadLibrary("cvc4jni"); - - ExprManager manager = new ExprManager(); - SmtEngine smtEngine = new SmtEngine(manager); +public class Relations +{ + public static void main(String[] args) throws CVC5ApiException + { + Solver solver = new Solver(); // Set the logic - smtEngine.setLogic("ALL"); + solver.setLogic("ALL"); // options - smtEngine.setOption("produce-models", new SExpr(true)); - smtEngine.setOption("finite-model-find", new SExpr(true)); - smtEngine.setOption("sets-ext", new SExpr(true)); - smtEngine.setOption("output-language", new SExpr("smt2")); + solver.setOption("produce-models", "true"); + solver.setOption("finite-model-find", "true"); + solver.setOption("sets-ext", "true"); + solver.setOption("output-language", "smt2"); // (declare-sort Person 0) - Type personType = manager.mkSort("Person", 0); - vectorType vector1 = new vectorType(manager); - vector1.add(personType); + Sort personSort = solver.mkUninterpretedSort("Person"); // (Tuple Person) - Type tupleArity1 = manager.mkTupleType(vector1); + Sort tupleArity1 = solver.mkTupleSort(new Sort[] {personSort}); // (Set (Tuple Person)) - SetType relationArity1 = manager.mkSetType(tupleArity1); + Sort relationArity1 = solver.mkSetSort(tupleArity1); - vectorType vector2 = new vectorType(manager); - vector2.add(personType); - vector2.add(personType); // (Tuple Person Person) - DatatypeType tupleArity2 = manager.mkTupleType(vector2); + Sort tupleArity2 = solver.mkTupleSort(new Sort[] {personSort, personSort}); // (Set (Tuple Person Person)) - SetType relationArity2 = manager.mkSetType(tupleArity2); + Sort relationArity2 = solver.mkSetSort(tupleArity2); // empty set - EmptySet emptySet = new EmptySet(manager, relationArity1); - Expr emptySetExpr = manager.mkConst(emptySet); + Term emptySetTerm = solver.mkEmptySet(relationArity1); // empty relation - EmptySet emptyRelation = new EmptySet(manager, relationArity2); - Expr emptyRelationExpr = manager.mkConst(emptyRelation); + Term emptyRelationTerm = solver.mkEmptySet(relationArity2); // universe set - Expr universeSet = - manager.mkNullaryOperator(relationArity1, Kind.UNIVERSE_SET); + Term universeSet = solver.mkUniverseSet(relationArity1); // variables - Expr people = manager.mkVar("people", relationArity1); - Expr males = manager.mkVar("males", relationArity1); - Expr females = manager.mkVar("females", relationArity1); - Expr father = manager.mkVar("father", relationArity2); - Expr mother = manager.mkVar("mother", relationArity2); - Expr parent = manager.mkVar("parent", relationArity2); - Expr ancestor = manager.mkVar("ancestor", relationArity2); - Expr descendant = manager.mkVar("descendant", relationArity2); - - Expr isEmpty1 = manager.mkExpr(Kind.EQUAL, males, emptySetExpr); - Expr isEmpty2 = manager.mkExpr(Kind.EQUAL, females, emptySetExpr); + Term people = solver.mkConst(relationArity1, "people"); + Term males = solver.mkConst(relationArity1, "males"); + Term females = solver.mkConst(relationArity1, "females"); + Term father = solver.mkConst(relationArity2, "father"); + Term mother = solver.mkConst(relationArity2, "mother"); + Term parent = solver.mkConst(relationArity2, "parent"); + Term ancestor = solver.mkConst(relationArity2, "ancestor"); + Term descendant = solver.mkConst(relationArity2, "descendant"); + + Term isEmpty1 = solver.mkTerm(EQUAL, males, emptySetTerm); + Term isEmpty2 = solver.mkTerm(EQUAL, females, emptySetTerm); // (assert (= people (as univset (Set (Tuple Person))))) - Expr peopleAreTheUniverse = manager.mkExpr(Kind.EQUAL, people, universeSet); + Term peopleAreTheUniverse = solver.mkTerm(EQUAL, people, universeSet); // (assert (not (= males (as emptyset (Set (Tuple Person)))))) - Expr maleSetIsNotEmpty = manager.mkExpr(Kind.NOT, isEmpty1); + Term maleSetIsNotEmpty = solver.mkTerm(NOT, isEmpty1); // (assert (not (= females (as emptyset (Set (Tuple Person)))))) - Expr femaleSetIsNotEmpty = manager.mkExpr(Kind.NOT, isEmpty2); + Term femaleSetIsNotEmpty = solver.mkTerm(NOT, isEmpty2); // (assert (= (intersection males females) (as emptyset (Set (Tuple // Person))))) - Expr malesFemalesIntersection = - manager.mkExpr(Kind.INTERSECTION, males, females); - Expr malesAndFemalesAreDisjoint = - manager.mkExpr(Kind.EQUAL, malesFemalesIntersection, emptySetExpr); + Term malesFemalesIntersection = solver.mkTerm(INTERSECTION, males, females); + Term malesAndFemalesAreDisjoint = solver.mkTerm(EQUAL, malesFemalesIntersection, emptySetTerm); // (assert (not (= father (as emptyset (Set (Tuple Person Person)))))) // (assert (not (= mother (as emptyset (Set (Tuple Person Person)))))) - Expr isEmpty3 = manager.mkExpr(Kind.EQUAL, father, emptyRelationExpr); - Expr isEmpty4 = manager.mkExpr(Kind.EQUAL, mother, emptyRelationExpr); - Expr fatherIsNotEmpty = manager.mkExpr(Kind.NOT, isEmpty3); - Expr motherIsNotEmpty = manager.mkExpr(Kind.NOT, isEmpty4); + Term isEmpty3 = solver.mkTerm(EQUAL, father, emptyRelationTerm); + Term isEmpty4 = solver.mkTerm(EQUAL, mother, emptyRelationTerm); + Term fatherIsNotEmpty = solver.mkTerm(NOT, isEmpty3); + Term motherIsNotEmpty = solver.mkTerm(NOT, isEmpty4); // fathers are males // (assert (subset (join father people) males)) - Expr fathers = manager.mkExpr(Kind.JOIN, father, people); - Expr fathersAreMales = manager.mkExpr(Kind.SUBSET, fathers, males); + Term fathers = solver.mkTerm(JOIN, father, people); + Term fathersAreMales = solver.mkTerm(SUBSET, fathers, males); // mothers are females // (assert (subset (join mother people) females)) - Expr mothers = manager.mkExpr(Kind.JOIN, mother, people); - Expr mothersAreFemales = manager.mkExpr(Kind.SUBSET, mothers, females); + Term mothers = solver.mkTerm(JOIN, mother, people); + Term mothersAreFemales = solver.mkTerm(SUBSET, mothers, females); // (assert (= parent (union father mother))) - Expr unionFatherMother = manager.mkExpr(Kind.UNION, father, mother); - Expr parentIsFatherOrMother = - manager.mkExpr(Kind.EQUAL, parent, unionFatherMother); + Term unionFatherMother = solver.mkTerm(UNION, father, mother); + Term parentIsFatherOrMother = solver.mkTerm(EQUAL, parent, unionFatherMother); // (assert (= parent (union father mother))) - Expr transitiveClosure = manager.mkExpr(Kind.TCLOSURE, parent); - Expr descendantFormula = - manager.mkExpr(Kind.EQUAL, descendant, transitiveClosure); + Term transitiveClosure = solver.mkTerm(TCLOSURE, parent); + Term descendantFormula = solver.mkTerm(EQUAL, descendant, transitiveClosure); // (assert (= parent (union father mother))) - Expr transpose = manager.mkExpr(Kind.TRANSPOSE, descendant); - Expr ancestorFormula = manager.mkExpr(Kind.EQUAL, ancestor, transpose); + Term transpose = solver.mkTerm(TRANSPOSE, descendant); + Term ancestorFormula = solver.mkTerm(EQUAL, ancestor, transpose); // (assert (forall ((x Person)) (not (member (mkTuple x x) ancestor)))) - Expr x = manager.mkBoundVar("x", personType); - Expr constructor = tupleArity2.getDatatype().get(0).getConstructor(); - Expr xxTuple = manager.mkExpr(Kind.APPLY_CONSTRUCTOR, constructor, x, x); - Expr member = manager.mkExpr(Kind.MEMBER, xxTuple, ancestor); - Expr notMember = manager.mkExpr(Kind.NOT, member); - vectorExpr vectorExpr = new vectorExpr(manager); - vectorExpr.add(x); - Expr quantifiedVariables = manager.mkExpr(Kind.BOUND_VAR_LIST, x); - Expr noSelfAncestor = - manager.mkExpr(Kind.FORALL, quantifiedVariables, notMember); + Term x = solver.mkVar(personSort, "x"); + DatatypeConstructor constructor = tupleArity2.getDatatype().getConstructor(0); + Term xxTuple = solver.mkTerm(APPLY_CONSTRUCTOR, constructor.getConstructorTerm(), x, x); + Term member = solver.mkTerm(MEMBER, xxTuple, ancestor); + Term notMember = solver.mkTerm(NOT, member); + + Term quantifiedVariables = solver.mkTerm(BOUND_VAR_LIST, x); + Term noSelfAncestor = solver.mkTerm(FORALL, quantifiedVariables, notMember); // formulas - Expr formula1 = manager.mkExpr(Kind.AND, - peopleAreTheUniverse, - maleSetIsNotEmpty, - femaleSetIsNotEmpty, - malesAndFemalesAreDisjoint); - - Expr formula2 = manager.mkExpr(Kind.AND, - formula1, - fatherIsNotEmpty, - motherIsNotEmpty, - fathersAreMales, - mothersAreFemales); - - Expr formula3 = manager.mkExpr(Kind.AND, - formula2, - parentIsFatherOrMother, - descendantFormula, - ancestorFormula, - noSelfAncestor); + solver.assertFormula(peopleAreTheUniverse); + solver.assertFormula(maleSetIsNotEmpty); + solver.assertFormula(femaleSetIsNotEmpty); + solver.assertFormula(malesAndFemalesAreDisjoint); + solver.assertFormula(fatherIsNotEmpty); + solver.assertFormula(motherIsNotEmpty); + solver.assertFormula(fathersAreMales); + solver.assertFormula(mothersAreFemales); + solver.assertFormula(parentIsFatherOrMother); + solver.assertFormula(descendantFormula); + solver.assertFormula(ancestorFormula); + solver.assertFormula(noSelfAncestor); // check sat - Result result = smtEngine.checkSat(formula3); + Result result = solver.checkSat(); // output - System.out.println("CVC4 reports: " + formula3 + " is " + result + "."); - System.out.println("people = " + smtEngine.getValue(people)); - System.out.println("males = " + smtEngine.getValue(males)); - System.out.println("females = " + smtEngine.getValue(females)); - System.out.println("father = " + smtEngine.getValue(father)); - System.out.println("mother = " + smtEngine.getValue(mother)); - System.out.println("parent = " + smtEngine.getValue(parent)); - System.out.println("descendant = " + smtEngine.getValue(descendant)); - System.out.println("ancestor = " + smtEngine.getValue(ancestor)); + System.out.println("Result = " + result); + System.out.println("people = " + solver.getValue(people)); + System.out.println("males = " + solver.getValue(males)); + System.out.println("females = " + solver.getValue(females)); + System.out.println("father = " + solver.getValue(father)); + System.out.println("mother = " + solver.getValue(mother)); + System.out.println("parent = " + solver.getValue(parent)); + System.out.println("descendant = " + solver.getValue(descendant)); + System.out.println("ancestor = " + solver.getValue(ancestor)); } } diff --git a/examples/api/java/Sequences.java b/examples/api/java/Sequences.java new file mode 100644 index 000000000..8d327fb2b --- /dev/null +++ b/examples/api/java/Sequences.java @@ -0,0 +1,68 @@ +/****************************************************************************** + * Top contributors (to current version): + * Andres Noetzli, Aina Niemetz, Tianyi Liang + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * A simple demonstration of reasoning about sequences with cvc5 via C++ API. + */ + +import static cvc5.Kind.*; + +import cvc5.*; + +public class Sequences +{ + public static void main(String args[]) throws CVC5ApiException + { + Solver slv = new Solver(); + + // Set the logic + slv.setLogic("QF_SLIA"); + // Produce models + slv.setOption("produce-models", "true"); + // The option strings-exp is needed + slv.setOption("strings-exp", "true"); + // Set output language to SMTLIB2 + slv.setOption("output-language", "smt2"); + + // Sequence sort + Sort intSeq = slv.mkSequenceSort(slv.getIntegerSort()); + + // Sequence variables + Term x = slv.mkConst(intSeq, "x"); + Term y = slv.mkConst(intSeq, "y"); + + // Empty sequence + Term empty = slv.mkEmptySequence(slv.getIntegerSort()); + // Sequence concatenation: x.y.empty + Term concat = slv.mkTerm(SEQ_CONCAT, x, y, empty); + // Sequence length: |x.y.empty| + Term concat_len = slv.mkTerm(SEQ_LENGTH, concat); + // |x.y.empty| > 1 + Term formula1 = slv.mkTerm(GT, concat_len, slv.mkInteger(1)); + // Sequence unit: seq(1) + Term unit = slv.mkTerm(SEQ_UNIT, slv.mkInteger(1)); + // x = seq(1) + Term formula2 = slv.mkTerm(EQUAL, x, unit); + + // Make a query + Term q = slv.mkTerm(AND, formula1, formula2); + + // check sat + Result result = slv.checkSatAssuming(q); + System.out.println("cvc5 reports: " + q + " is " + result + "."); + + if (result.isSat()) + { + System.out.println(" x = " + slv.getValue(x)); + System.out.println(" y = " + slv.getValue(y)); + } + } +}
\ No newline at end of file diff --git a/examples/api/java/Sets.java b/examples/api/java/Sets.java new file mode 100644 index 000000000..38f7d194d --- /dev/null +++ b/examples/api/java/Sets.java @@ -0,0 +1,92 @@ +/****************************************************************************** + * Top contributors (to current version): + * Aina Niemetz, Kshitij Bansal, Mudathir Mohamed + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * A simple demonstration of reasoning about sets with cvc5. + */ + +import static cvc5.Kind.*; + +import cvc5.*; + +public class Sets +{ + public static void main(String args[]) throws CVC5ApiException + { + Solver slv = new Solver(); + + // Optionally, set the logic. We need at least UF for equality predicate, + // integers (LIA) and sets (FS). + slv.setLogic("QF_UFLIAFS"); + + // Produce models + slv.setOption("produce-models", "true"); + slv.setOption("output-language", "smt2"); + + Sort integer = slv.getIntegerSort(); + Sort set = slv.mkSetSort(integer); + + // Verify union distributions over intersection + // (A union B) intersection C = (A intersection C) union (B intersection C) + { + Term A = slv.mkConst(set, "A"); + Term B = slv.mkConst(set, "B"); + Term C = slv.mkConst(set, "C"); + + Term unionAB = slv.mkTerm(UNION, A, B); + Term lhs = slv.mkTerm(INTERSECTION, unionAB, C); + + Term intersectionAC = slv.mkTerm(INTERSECTION, A, C); + Term intersectionBC = slv.mkTerm(INTERSECTION, B, C); + Term rhs = slv.mkTerm(UNION, intersectionAC, intersectionBC); + + Term theorem = slv.mkTerm(EQUAL, lhs, rhs); + + System.out.println("cvc5 reports: " + theorem + " is " + slv.checkEntailed(theorem) + "."); + } + + // Verify emptset is a subset of any set + { + Term A = slv.mkConst(set, "A"); + Term emptyset = slv.mkEmptySet(set); + + Term theorem = slv.mkTerm(SUBSET, emptyset, A); + + System.out.println("cvc5 reports: " + theorem + " is " + slv.checkEntailed(theorem) + "."); + } + + // Find me an element in {1, 2} intersection {2, 3}, if there is one. + { + Term one = slv.mkInteger(1); + Term two = slv.mkInteger(2); + Term three = slv.mkInteger(3); + + Term singleton_one = slv.mkTerm(SINGLETON, one); + Term singleton_two = slv.mkTerm(SINGLETON, two); + Term singleton_three = slv.mkTerm(SINGLETON, three); + Term one_two = slv.mkTerm(UNION, singleton_one, singleton_two); + Term two_three = slv.mkTerm(UNION, singleton_two, singleton_three); + Term intersection = slv.mkTerm(INTERSECTION, one_two, two_three); + + Term x = slv.mkConst(integer, "x"); + + Term e = slv.mkTerm(MEMBER, x, intersection); + + Result result = slv.checkSatAssuming(e); + System.out.println("cvc5 reports: " + e + " is " + result + "."); + + if (result.isSat()) + { + System.out.println("For instance, " + slv.getValue(x) + " is a member."); + } + } + } +}
\ No newline at end of file diff --git a/examples/api/java/Statistics.java b/examples/api/java/Statistics.java index 0637f66de..c5aad0558 100644 --- a/examples/api/java/Statistics.java +++ b/examples/api/java/Statistics.java @@ -13,32 +13,217 @@ * An example of accessing CVC4's statistics using the Java API. */ -import edu.stanford.CVC4.*; -import java.util.Iterator; +import static cvc5.Kind.*; -public class Statistics { - public static void main(String[] args) { - System.loadLibrary("cvc4jni"); +import cvc5.*; +import java.util.List; +import java.util.Map; - ExprManager em = new ExprManager(); - SmtEngine smt = new SmtEngine(em); +public class Statistics +{ + public static void main(String[] args) + { + Solver solver = getSolver(); + // Get the statistics from the `Solver` and iterate over them. The + // `Statistics` class implements the `Iterable<Pair<String, Stat>>` interface. + cvc5.Statistics stats = solver.getStatistics(); + // short version + System.out.println("Short version:"); + System.out.println(stats); - Type boolType = em.booleanType(); - Expr a = em.mkVar("A", boolType); - Expr b = em.mkVar("B", boolType); + System.out.println("-------------------------------------------------------"); - // A ^ B - smt.assertFormula(em.mkExpr(Kind.AND, a, b)); + System.out.println("Long version:"); - Result res = smt.checkSat(); - - // Get the statistics from the `SmtEngine` and iterate over them. The - // `Statistics` class implements the `Iterable<Statistic>` interface. A - // `Statistic` is a pair that consists of a name and an `SExpr` that stores - // the value of the statistic. - edu.stanford.CVC4.Statistics stats = smt.getStatistics(); - for (Statistic stat : stats) { - System.out.println(stat.getFirst() + " = " + stat.getSecond()); + // long version + for (Pair<String, Stat> pair : stats) + { + Stat stat = pair.second; + if (stat.isInt()) + { + System.out.println(pair.first + " = " + stat.getInt()); + } + else if (stat.isDouble()) + { + System.out.println(pair.first + " = " + stat.getDouble()); + } + else if (stat.isString()) + { + System.out.println(pair.first + " = " + stat.getString()); + } + else if (stat.isHistogram()) + { + System.out.println("-------------------------------------------------------"); + System.out.println(pair.first + " : Map"); + for (Map.Entry<String, Long> entry : stat.getHistogram().entrySet()) + { + System.out.println(entry.getKey() + " = " + entry.getValue()); + } + System.out.println("-------------------------------------------------------"); + } } } + + private static Solver getSolver() + { + Solver solver = new Solver(); + + // String type + Sort string = solver.getStringSort(); + + // std::string + String str_ab = "ab"; + // String constants + Term ab = solver.mkString(str_ab); + Term abc = solver.mkString("abc"); + // String variables + Term x = solver.mkConst(string, "x"); + Term y = solver.mkConst(string, "y"); + Term z = solver.mkConst(string, "z"); + + // String concatenation: x.ab.y + Term lhs = solver.mkTerm(STRING_CONCAT, x, ab, y); + // String concatenation: abc.z + Term rhs = solver.mkTerm(STRING_CONCAT, abc, z); + // x.ab.y = abc.z + Term formula1 = solver.mkTerm(EQUAL, lhs, rhs); + + // Length of y: |y| + Term leny = solver.mkTerm(STRING_LENGTH, y); + // |y| >= 0 + Term formula2 = solver.mkTerm(GEQ, leny, solver.mkInteger(0)); + + // Regular expression: (ab[c-e]*f)|g|h + Term r = solver.mkTerm(REGEXP_UNION, + solver.mkTerm(REGEXP_CONCAT, + solver.mkTerm(STRING_TO_REGEXP, solver.mkString("ab")), + solver.mkTerm(REGEXP_STAR, + solver.mkTerm(REGEXP_RANGE, solver.mkString("c"), solver.mkString("e"))), + solver.mkTerm(STRING_TO_REGEXP, solver.mkString("f"))), + solver.mkTerm(STRING_TO_REGEXP, solver.mkString("g")), + solver.mkTerm(STRING_TO_REGEXP, solver.mkString("h"))); + + // String variables + Term s1 = solver.mkConst(string, "s1"); + Term s2 = solver.mkConst(string, "s2"); + // String concatenation: s1.s2 + Term s = solver.mkTerm(STRING_CONCAT, s1, s2); + + // s1.s2 in (ab[c-e]*f)|g|h + Term formula3 = solver.mkTerm(STRING_IN_REGEXP, s, r); + + // Make a query + Term q = solver.mkTerm(AND, formula1, formula2, formula3); + + // options + solver.setOption("produce-models", "true"); + solver.setOption("finite-model-find", "true"); + solver.setOption("sets-ext", "true"); + solver.setOption("output-language", "smt2"); + + // (declare-sort Person 0) + Sort personSort = solver.mkUninterpretedSort("Person"); + + // (Tuple Person) + Sort tupleArity1 = solver.mkTupleSort(new Sort[] {personSort}); + // (Set (Tuple Person)) + Sort relationArity1 = solver.mkSetSort(tupleArity1); + + // (Tuple Person Person) + Sort tupleArity2 = solver.mkTupleSort(new Sort[] {personSort, personSort}); + // (Set (Tuple Person Person)) + Sort relationArity2 = solver.mkSetSort(tupleArity2); + + // empty set + Term emptySetTerm = solver.mkEmptySet(relationArity1); + + // empty relation + Term emptyRelationTerm = solver.mkEmptySet(relationArity2); + + // universe set + Term universeSet = solver.mkUniverseSet(relationArity1); + + // variables + Term people = solver.mkConst(relationArity1, "people"); + Term males = solver.mkConst(relationArity1, "males"); + Term females = solver.mkConst(relationArity1, "females"); + Term father = solver.mkConst(relationArity2, "father"); + Term mother = solver.mkConst(relationArity2, "mother"); + Term parent = solver.mkConst(relationArity2, "parent"); + Term ancestor = solver.mkConst(relationArity2, "ancestor"); + Term descendant = solver.mkConst(relationArity2, "descendant"); + + Term isEmpty1 = solver.mkTerm(EQUAL, males, emptySetTerm); + Term isEmpty2 = solver.mkTerm(EQUAL, females, emptySetTerm); + + // (assert (= people (as univset (Set (Tuple Person))))) + Term peopleAreTheUniverse = solver.mkTerm(EQUAL, people, universeSet); + // (assert (not (= males (as emptyset (Set (Tuple Person)))))) + Term maleSetIsNotEmpty = solver.mkTerm(NOT, isEmpty1); + // (assert (not (= females (as emptyset (Set (Tuple Person)))))) + Term femaleSetIsNotEmpty = solver.mkTerm(NOT, isEmpty2); + + // (assert (= (intersection males females) (as emptyset (Set (Tuple + // Person))))) + Term malesFemalesIntersection = solver.mkTerm(INTERSECTION, males, females); + Term malesAndFemalesAreDisjoint = solver.mkTerm(EQUAL, malesFemalesIntersection, emptySetTerm); + + // (assert (not (= father (as emptyset (Set (Tuple Person Person)))))) + // (assert (not (= mother (as emptyset (Set (Tuple Person Person)))))) + Term isEmpty3 = solver.mkTerm(EQUAL, father, emptyRelationTerm); + Term isEmpty4 = solver.mkTerm(EQUAL, mother, emptyRelationTerm); + Term fatherIsNotEmpty = solver.mkTerm(NOT, isEmpty3); + Term motherIsNotEmpty = solver.mkTerm(NOT, isEmpty4); + + // fathers are males + // (assert (subset (join father people) males)) + Term fathers = solver.mkTerm(JOIN, father, people); + Term fathersAreMales = solver.mkTerm(SUBSET, fathers, males); + + // mothers are females + // (assert (subset (join mother people) females)) + Term mothers = solver.mkTerm(JOIN, mother, people); + Term mothersAreFemales = solver.mkTerm(SUBSET, mothers, females); + + // (assert (= parent (union father mother))) + Term unionFatherMother = solver.mkTerm(UNION, father, mother); + Term parentIsFatherOrMother = solver.mkTerm(EQUAL, parent, unionFatherMother); + + // (assert (= parent (union father mother))) + Term transitiveClosure = solver.mkTerm(TCLOSURE, parent); + Term descendantFormula = solver.mkTerm(EQUAL, descendant, transitiveClosure); + + // (assert (= parent (union father mother))) + Term transpose = solver.mkTerm(TRANSPOSE, descendant); + Term ancestorFormula = solver.mkTerm(EQUAL, ancestor, transpose); + + // (assert (forall ((x Person)) (not (member (mkTuple x x) ancestor)))) + Term var = solver.mkVar(personSort, "x"); + DatatypeConstructor constructor = tupleArity2.getDatatype().getConstructor(0); + Term xxTuple = solver.mkTerm(APPLY_CONSTRUCTOR, constructor.getConstructorTerm(), var, var); + Term member = solver.mkTerm(MEMBER, xxTuple, ancestor); + Term notMember = solver.mkTerm(NOT, member); + + Term quantifiedVariables = solver.mkTerm(BOUND_VAR_LIST, var); + Term noSelfAncestor = solver.mkTerm(FORALL, quantifiedVariables, notMember); + + // formulas + solver.assertFormula(peopleAreTheUniverse); + solver.assertFormula(maleSetIsNotEmpty); + solver.assertFormula(femaleSetIsNotEmpty); + solver.assertFormula(malesAndFemalesAreDisjoint); + solver.assertFormula(fatherIsNotEmpty); + solver.assertFormula(motherIsNotEmpty); + solver.assertFormula(fathersAreMales); + solver.assertFormula(mothersAreFemales); + solver.assertFormula(parentIsFatherOrMother); + solver.assertFormula(descendantFormula); + solver.assertFormula(ancestorFormula); + solver.assertFormula(noSelfAncestor); + + // check sat + solver.checkSatAssuming(q); + + return solver; + } } diff --git a/examples/api/java/Strings.java b/examples/api/java/Strings.java index e5947abcc..e023459fa 100644 --- a/examples/api/java/Strings.java +++ b/examples/api/java/Strings.java @@ -1,6 +1,6 @@ /****************************************************************************** * Top contributors (to current version): - * Tianyi Liang, Andres Noetzli + * Aina Niemetz, Tianyi Liang, Mudathir Mohamed * * This file is part of the cvc5 project. * @@ -10,81 +10,82 @@ * directory for licensing information. * **************************************************************************** * - * A simple demonstration of reasoning about strings with CVC4 via Java API. + * A simple demonstration of reasoning about strings with cvc5 via C++ API. */ -import edu.stanford.CVC4.*; +import static cvc5.Kind.*; -public class Strings { - public static void main(String[] args) { - System.loadLibrary("cvc4jni"); +import cvc5.*; - ExprManager em = new ExprManager(); - SmtEngine smt = new SmtEngine(em); +public class Strings +{ + public static void main(String args[]) throws CVC5ApiException + { + Solver slv = new Solver(); // Set the logic - smt.setLogic("S"); - + slv.setLogic("QF_SLIA"); // Produce models - smt.setOption("produce-models", new SExpr(true)); + slv.setOption("produce-models", "true"); // The option strings-exp is needed - smt.setOption("strings-exp", new SExpr(true)); - // output-language - smt.setOption("output-language", new SExpr("smt2")); + slv.setOption("strings-exp", "true"); + // Set output language to SMTLIB2 + slv.setOption("output-language", "smt2"); // String type - Type string = em.stringType(); + Sort string = slv.getStringSort(); + // std::string + String str_ab = "ab"; // String constants - Expr ab = em.mkConst(new CVC4String("ab")); - Expr abc = em.mkConst(new CVC4String("abc")); - // Variables - Expr x = em.mkVar("x", string); - Expr y = em.mkVar("y", string); - Expr z = em.mkVar("z", string); + Term ab = slv.mkString(str_ab); + Term abc = slv.mkString("abc"); + // String variables + Term x = slv.mkConst(string, "x"); + Term y = slv.mkConst(string, "y"); + Term z = slv.mkConst(string, "z"); // String concatenation: x.ab.y - Expr lhs = em.mkExpr(Kind.STRING_CONCAT, x, ab, y); + Term lhs = slv.mkTerm(STRING_CONCAT, x, ab, y); // String concatenation: abc.z - Expr rhs = em.mkExpr(Kind.STRING_CONCAT, abc, z);; + Term rhs = slv.mkTerm(STRING_CONCAT, abc, z); // x.ab.y = abc.z - Expr formula1 = em.mkExpr(Kind.EQUAL, lhs, rhs); + Term formula1 = slv.mkTerm(EQUAL, lhs, rhs); // Length of y: |y| - Expr leny = em.mkExpr(Kind.STRING_LENGTH, y); + Term leny = slv.mkTerm(STRING_LENGTH, y); // |y| >= 0 - Expr formula2 = em.mkExpr(Kind.GEQ, leny, em.mkConst(new Rational(0))); + Term formula2 = slv.mkTerm(GEQ, leny, slv.mkInteger(0)); // Regular expression: (ab[c-e]*f)|g|h - Expr r = em.mkExpr(Kind.REGEXP_UNION, - em.mkExpr(Kind.REGEXP_CONCAT, - em.mkExpr(Kind.STRING_TO_REGEXP, em.mkConst(new CVC4String("ab"))), - em.mkExpr(Kind.REGEXP_STAR, - em.mkExpr(Kind.REGEXP_RANGE, em.mkConst(new CVC4String("c")), em.mkConst(new CVC4String("e")))), - em.mkExpr(Kind.STRING_TO_REGEXP, em.mkConst(new CVC4String("f")))), - em.mkExpr(Kind.STRING_TO_REGEXP, em.mkConst(new CVC4String("g"))), - em.mkExpr(Kind.STRING_TO_REGEXP, em.mkConst(new CVC4String("h")))); + Term r = slv.mkTerm(REGEXP_UNION, + slv.mkTerm(REGEXP_CONCAT, + slv.mkTerm(STRING_TO_REGEXP, slv.mkString("ab")), + slv.mkTerm(REGEXP_STAR, slv.mkTerm(REGEXP_RANGE, slv.mkString("c"), slv.mkString("e"))), + slv.mkTerm(STRING_TO_REGEXP, slv.mkString("f"))), + slv.mkTerm(STRING_TO_REGEXP, slv.mkString("g")), + slv.mkTerm(STRING_TO_REGEXP, slv.mkString("h"))); // String variables - Expr s1 = em.mkVar("s1", string); - Expr s2 = em.mkVar("s2", string); + Term s1 = slv.mkConst(string, "s1"); + Term s2 = slv.mkConst(string, "s2"); // String concatenation: s1.s2 - Expr s = em.mkExpr(Kind.STRING_CONCAT, s1, s2); + Term s = slv.mkTerm(STRING_CONCAT, s1, s2); // s1.s2 in (ab[c-e]*f)|g|h - Expr formula3 = em.mkExpr(Kind.STRING_IN_REGEXP, s, r); + Term formula3 = slv.mkTerm(STRING_IN_REGEXP, s, r); - // Make a query - Expr q = em.mkExpr(Kind.AND, - formula1, - formula2, - formula3); + // Make a query + Term q = slv.mkTerm(AND, formula1, formula2, formula3); - // check sat - Result result = smt.checkSat(q); - System.out.println("CVC4 reports: " + q + " is " + result + "."); + // check sat + Result result = slv.checkSatAssuming(q); + System.out.println("cvc5 reports: " + q + " is " + result + "."); - System.out.println(" x = " + smt.getValue(x)); - System.out.println(" s1.s2 = " + smt.getValue(s)); + if (result.isSat()) + { + System.out.println(" x = " + slv.getValue(x)); + System.out.println(" s1.s2 = " + slv.getValue(s)); + } } -} +}
\ No newline at end of file diff --git a/examples/api/java/SygusFun.java b/examples/api/java/SygusFun.java new file mode 100644 index 000000000..1a53a0dd1 --- /dev/null +++ b/examples/api/java/SygusFun.java @@ -0,0 +1,139 @@ +/****************************************************************************** + * Top contributors (to current version): + * Abdalrhman Mohamed, Mudathir Mohamed, Aina Niemetz + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * A simple demonstration of the Sygus API. + * + * A simple demonstration of how to use the Sygus API to synthesize max and min + * functions. Here is the same problem written in Sygus V2 format: + * + * (set-logic LIA) + * + * (synth-fun max ((x Int) (y Int)) Int + * ((Start Int) (StartBool Bool)) + * ((Start Int (0 1 x y + * (+ Start Start) + * (- Start Start) + * (ite StartBool Start Start))) + * (StartBool Bool ((and StartBool StartBool) + * (not StartBool) + * (<= Start Start))))) + * + * (synth-fun min ((x Int) (y Int)) Int) + * + * (declare-var x Int) + * (declare-var y Int) + * + * (constraint (>= (max x y) x)) + * (constraint (>= (max x y) y)) + * (constraint (or (= x (max x y)) + * (= y (max x y)))) + * (constraint (= (+ (max x y) (min x y)) + * (+ x y))) + * + * (check-synth) + * + * The printed output for this example should be equivalent to: + * ( + * (define-fun max ((x Int) (y Int)) Int (ite (<= x y) y x)) + * (define-fun min ((x Int) (y Int)) Int (ite (<= x y) x y)) + * ) + */ + +import static cvc5.Kind.*; + +import cvc5.*; + +public class SygusFun +{ + public static void main(String args[]) throws CVC5ApiException + { + Solver slv = new Solver(); + + // required options + slv.setOption("lang", "sygus2"); + slv.setOption("incremental", "false"); + + // set the logic + slv.setLogic("LIA"); + + Sort integer = slv.getIntegerSort(); + Sort bool = slv.getBooleanSort(); + + // declare input variables for the functions-to-synthesize + Term x = slv.mkVar(integer, "x"); + Term y = slv.mkVar(integer, "y"); + + // declare the grammar non-terminals + Term start = slv.mkVar(integer, "Start"); + Term start_bool = slv.mkVar(bool, "StartBool"); + + // define the rules + Term zero = slv.mkInteger(0); + Term one = slv.mkInteger(1); + + Term plus = slv.mkTerm(PLUS, start, start); + Term minus = slv.mkTerm(MINUS, start, start); + Term ite = slv.mkTerm(ITE, start_bool, start, start); + + Term And = slv.mkTerm(AND, start_bool, start_bool); + Term Not = slv.mkTerm(NOT, start_bool); + Term leq = slv.mkTerm(LEQ, start, start); + + // create the grammar object + Grammar g = slv.mkSygusGrammar(new Term[] {x, y}, new Term[] {start, start_bool}); + + // bind each non-terminal to its rules + g.addRules(start, new Term[] {zero, one, x, y, plus, minus, ite}); + g.addRules(start_bool, new Term[] {And, Not, leq}); + + // declare the functions-to-synthesize. Optionally, provide the grammar + // constraints + Term max = slv.synthFun("max", new Term[] {x, y}, integer, g); + Term min = slv.synthFun("min", new Term[] {x, y}, integer); + + // declare universal variables. + Term varX = slv.mkSygusVar(integer, "x"); + Term varY = slv.mkSygusVar(integer, "y"); + + Term max_x_y = slv.mkTerm(APPLY_UF, max, varX, varY); + Term min_x_y = slv.mkTerm(APPLY_UF, min, varX, varY); + + // add semantic constraints + // (constraint (>= (max x y) x)) + slv.addSygusConstraint(slv.mkTerm(GEQ, max_x_y, varX)); + + // (constraint (>= (max x y) y)) + slv.addSygusConstraint(slv.mkTerm(GEQ, max_x_y, varY)); + + // (constraint (or (= x (max x y)) + // (= y (max x y)))) + slv.addSygusConstraint( + slv.mkTerm(OR, slv.mkTerm(EQUAL, max_x_y, varX), slv.mkTerm(EQUAL, max_x_y, varY))); + + // (constraint (= (+ (max x y) (min x y)) + // (+ x y))) + slv.addSygusConstraint( + slv.mkTerm(EQUAL, slv.mkTerm(PLUS, max_x_y, min_x_y), slv.mkTerm(PLUS, varX, varY))); + + // print solutions if available + if (slv.checkSynth().isUnsat()) + { + // Output should be equivalent to: + // ( + // (define-fun max ((x Int) (y Int)) Int (ite (<= x y) y x)) + // (define-fun min ((x Int) (y Int)) Int (ite (<= x y) x y)) + // ) + Term[] terms = new Term[] {max, min}; + Utils.printSynthSolutions(terms, slv.getSynthSolutions(terms)); + } + } +}
\ No newline at end of file diff --git a/examples/api/java/SygusGrammar.java b/examples/api/java/SygusGrammar.java new file mode 100644 index 000000000..b39094ae5 --- /dev/null +++ b/examples/api/java/SygusGrammar.java @@ -0,0 +1,129 @@ +/****************************************************************************** + * Top contributors (to current version): + * Abdalrhman Mohamed, Mudathir Mohamed, Aina Niemetz + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * A simple demonstration of the Sygus API. + * + * A simple demonstration of how to use Grammar to add syntax constraints to + * the Sygus solution for the identity function. Here is the same problem + * written in Sygus V2 format: + * + * (set-logic LIA) + * + * (synth-fun id1 ((x Int)) Int + * ((Start Int)) ((Start Int ((- x) (+ x Start))))) + * + * (synth-fun id2 ((x Int)) Int + * ((Start Int)) ((Start Int ((Variable Int) (- x) (+ x Start))))) + * + * (synth-fun id3 ((x Int)) Int + * ((Start Int)) ((Start Int (0 (- x) (+ x Start))))) + * + * (synth-fun id4 ((x Int)) Int + * ((Start Int)) ((Start Int ((- x) (+ x Start))))) + * + * (declare-var x Int) + * + * (constraint (= (id1 x) (id2 x) (id3 x) (id4 x) x)) + * + * (check-synth) + * + * The printed output for this example should look like: + * ( + * (define-fun id1 ((x Int)) Int (+ x (+ x (- x)))) + * (define-fun id2 ((x Int)) Int x) + * (define-fun id3 ((x Int)) Int (+ x 0)) + * (define-fun id4 ((x Int)) Int (+ x (+ x (- x)))) + * ) + */ + +import static cvc5.Kind.*; + +import cvc5.*; + +public class SygusGrammar +{ + public static void main(String args[]) throws CVC5ApiException + { + Solver slv = new Solver(); + + // required options + slv.setOption("lang", "sygus2"); + slv.setOption("incremental", "false"); + + // set the logic + slv.setLogic("LIA"); + + Sort integer = slv.getIntegerSort(); + Sort bool = slv.getBooleanSort(); + + // declare input variable for the function-to-synthesize + Term x = slv.mkVar(integer, "x"); + + // declare the grammar non-terminal + Term start = slv.mkVar(integer, "Start"); + + // define the rules + Term zero = slv.mkInteger(0); + Term neg_x = slv.mkTerm(UMINUS, x); + Term plus = slv.mkTerm(PLUS, x, start); + + // create the grammar object + Grammar g1 = slv.mkSygusGrammar(new Term[] {x}, new Term[] {start}); + + // bind each non-terminal to its rules + g1.addRules(start, new Term[] {neg_x, plus}); + + // copy the first grammar with all of its non-terminals and their rules + Grammar g2 = new Grammar(g1); + Grammar g3 = new Grammar(g1); + + // add parameters as rules for the start symbol. Similar to "(Variable Int)" + g2.addAnyVariable(start); + + // declare the functions-to-synthesize + Term id1 = slv.synthFun("id1", new Term[] {x}, integer, g1); + Term id2 = slv.synthFun("id2", new Term[] {x}, integer, g2); + + g3.addRule(start, zero); + + Term id3 = slv.synthFun("id3", new Term[] {x}, integer, g3); + + // g1 is reusable as long as it remains unmodified after first use + Term id4 = slv.synthFun("id4", new Term[] {x}, integer, g1); + + // declare universal variables. + Term varX = slv.mkSygusVar(integer, "x"); + + Term id1_x = slv.mkTerm(APPLY_UF, id1, varX); + Term id2_x = slv.mkTerm(APPLY_UF, id2, varX); + Term id3_x = slv.mkTerm(APPLY_UF, id3, varX); + Term id4_x = slv.mkTerm(APPLY_UF, id4, varX); + + // add semantic constraints + // (constraint (= (id1 x) (id2 x) (id3 x) (id4 x) x)) + slv.addSygusConstraint(slv.mkTerm(EQUAL, new Term[] {id1_x, id2_x, id3_x, id4_x, varX})); + + // print solutions if available + if (slv.checkSynth().isUnsat()) + { + // Output should be equivalent to: + // ( + // (define-fun id1 ((x Int)) Int (+ x (+ x (- x)))) + // (define-fun id2 ((x Int)) Int x) + // (define-fun id3 ((x Int)) Int (+ x 0)) + // (define-fun id4 ((x Int)) Int (+ x (+ x (- x)))) + // ) + Term[] terms = new Term[] {id1, id2, id3, id4}; + Utils.printSynthSolutions(terms, slv.getSynthSolutions(terms)); + } + } +}
\ No newline at end of file diff --git a/examples/api/java/SygusInv.java b/examples/api/java/SygusInv.java new file mode 100644 index 000000000..47d6797ba --- /dev/null +++ b/examples/api/java/SygusInv.java @@ -0,0 +1,94 @@ +/****************************************************************************** + * Top contributors (to current version): + * Abdalrhman Mohamed, Mudathir Mohamed, Aina Niemetz + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * A simple demonstration of the Sygus API. + * + * A simple demonstration of how to use the Sygus API to synthesize a simple + * invariant. Here is the same problem written in Sygus V2 format: + * + * (set-logic LIA) + * + * (synth-inv inv-f ((x Int))) + * + * (define-fun pre-f ((x Int)) Bool + * (= x 0)) + * (define-fun trans-f ((x Int) (xp Int)) Bool + * (ite (< x 10) (= xp (+ x 1)) (= xp x))) + * (define-fun post-f ((x Int)) Bool + * (<= x 10)) + * + * (inv-constraint inv-f pre-f trans-f post-f) + * + * (check-synth) + * + * The printed output for this example should be equivalent to: + * ( + * (define-fun inv-f ((x Int)) Bool (not (>= x 11))) + * ) + */ + +import static cvc5.Kind.*; + +import cvc5.*; + +public class SygusInv +{ + public static void main(String args[]) throws CVC5ApiException + { + Solver slv = new Solver(); + + // required options + slv.setOption("lang", "sygus2"); + slv.setOption("incremental", "false"); + + // set the logic + slv.setLogic("LIA"); + + Sort integer = slv.getIntegerSort(); + Sort bool = slv.getBooleanSort(); + + Term zero = slv.mkInteger(0); + Term one = slv.mkInteger(1); + Term ten = slv.mkInteger(10); + + // declare input variables for functions + Term x = slv.mkVar(integer, "x"); + Term xp = slv.mkVar(integer, "xp"); + + // (ite (< x 10) (= xp (+ x 1)) (= xp x)) + Term ite = slv.mkTerm(ITE, + slv.mkTerm(LT, x, ten), + slv.mkTerm(EQUAL, xp, slv.mkTerm(PLUS, x, one)), + slv.mkTerm(EQUAL, xp, x)); + + // define the pre-conditions, transition relations, and post-conditions + Term pre_f = slv.defineFun("pre-f", new Term[] {x}, bool, slv.mkTerm(EQUAL, x, zero)); + Term trans_f = slv.defineFun("trans-f", new Term[] {x, xp}, bool, ite); + Term post_f = slv.defineFun("post-f", new Term[] {x}, bool, slv.mkTerm(LEQ, x, ten)); + + // declare the invariant-to-synthesize + Term inv_f = slv.synthInv("inv-f", new Term[] {x}); + + slv.addSygusInvConstraint(inv_f, pre_f, trans_f, post_f); + + // print solutions if available + if (slv.checkSynth().isUnsat()) + { + // Output should be equivalent to: + // ( + // (define-fun inv-f ((x Int)) Bool (not (>= x 11))) + // ) + Term[] terms = new Term[] {inv_f}; + Utils.printSynthSolutions(terms, slv.getSynthSolutions(terms)); + } + } +}
\ No newline at end of file diff --git a/examples/api/java/Transcendentals.java b/examples/api/java/Transcendentals.java new file mode 100644 index 000000000..5e8c26820 --- /dev/null +++ b/examples/api/java/Transcendentals.java @@ -0,0 +1,52 @@ +/****************************************************************************** + * Top contributors (to current version): + * Aina Niemetz, Tim King, Mudathir Mohamed + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * A simple demonstration of the transcendental extension. + */ + +import static cvc5.Kind.*; + +import cvc5.*; + +public class Transcendentals +{ + public static void main(String args[]) throws CVC5ApiException + { + Solver slv = new Solver(); + slv.setLogic("QF_NRAT"); + + Sort real = slv.getRealSort(); + + // Variables + Term x = slv.mkConst(real, "x"); + Term y = slv.mkConst(real, "y"); + + // Helper terms + Term two = slv.mkReal(2); + Term pi = slv.mkPi(); + Term twopi = slv.mkTerm(MULT, two, pi); + Term ysq = slv.mkTerm(MULT, y, y); + Term sinx = slv.mkTerm(SINE, x); + + // Formulas + Term x_gt_pi = slv.mkTerm(GT, x, pi); + Term x_lt_tpi = slv.mkTerm(LT, x, twopi); + Term ysq_lt_sinx = slv.mkTerm(LT, ysq, sinx); + + slv.assertFormula(x_gt_pi); + slv.assertFormula(x_lt_tpi); + slv.assertFormula(ysq_lt_sinx); + + System.out.println("cvc5 should report UNSAT."); + System.out.println("Result from cvc5 is: " + slv.checkSat()); + } +}
\ No newline at end of file diff --git a/examples/api/java/UnsatCores.java b/examples/api/java/UnsatCores.java index 42633e803..2f83ddc9c 100644 --- a/examples/api/java/UnsatCores.java +++ b/examples/api/java/UnsatCores.java @@ -13,40 +13,39 @@ * An example of interacting with unsat cores using CVC4's Java API. */ -import edu.stanford.CVC4.*; -import java.util.Iterator; +import cvc5.*; +import java.util.Arrays; -public class UnsatCores { - public static void main(String[] args) { - System.loadLibrary("cvc4jni"); - - ExprManager em = new ExprManager(); - SmtEngine smt = new SmtEngine(em); +public class UnsatCores +{ + public static void main(String[] args) throws CVC5ApiException + { + Solver solver = new Solver(); // Enable the production of unsat cores - smt.setOption("produce-unsat-cores", new SExpr(true)); + solver.setOption("produce-unsat-cores", "true"); - Type boolType = em.booleanType(); - Expr a = em.mkVar("A", boolType); - Expr b = em.mkVar("B", boolType); + Sort boolSort = solver.getBooleanSort(); + Term a = solver.mkConst(boolSort, "A"); + Term b = solver.mkConst(boolSort, "B"); // A ^ B - smt.assertFormula(em.mkExpr(Kind.AND, a, b)); + solver.assertFormula(solver.mkTerm(Kind.AND, a, b)); // ~(A v B) - smt.assertFormula(em.mkExpr(Kind.NOT, em.mkExpr(Kind.OR, a, b))); + solver.assertFormula(solver.mkTerm(Kind.NOT, solver.mkTerm(Kind.OR, a, b))); - Result res = smt.checkSat(); // result is unsat + Result res = solver.checkSat(); // result is unsat // Retrieve the unsat core - UnsatCore unsatCore = smt.getUnsatCore(); - + Term[] unsatCore = solver.getUnsatCore(); + // Print the unsat core - System.out.println("Unsat Core: " + unsatCore); + System.out.println("Unsat Core: " + Arrays.asList(unsatCore)); - // Iterate over expressions in the unsat core. The `UnsatCore` class - // implements the `Iterable<Expr>` interface. + // Iterate over expressions in the unsat core. System.out.println("--- Unsat Core ---"); - for (Expr e : unsatCore) { + for (Term e : unsatCore) + { System.out.println(e); } } diff --git a/src/api/java/cvc5/Grammar.java b/src/api/java/cvc5/Grammar.java index 72558d15b..b9240a621 100644 --- a/src/api/java/cvc5/Grammar.java +++ b/src/api/java/cvc5/Grammar.java @@ -23,6 +23,13 @@ public class Grammar extends AbstractPointer super(solver, pointer); } + public Grammar(Grammar grammar) + { + super(grammar.solver, copyGrammar(grammar.pointer)); + } + + private static native long copyGrammar(long pointer); + protected static native void deletePointer(long pointer); public long getPointer() diff --git a/src/api/java/cvc5/Term.java b/src/api/java/cvc5/Term.java index ebf55116b..a935e453f 100644 --- a/src/api/java/cvc5/Term.java +++ b/src/api/java/cvc5/Term.java @@ -19,6 +19,7 @@ import java.math.BigInteger; import java.util.Iterator; import java.util.List; import java.util.NoSuchElementException; +import java.math.BigInteger; public class Term extends AbstractPointer implements Comparable<Term>, Iterable<Term> { diff --git a/src/api/java/jni/cvc5_Grammar.cpp b/src/api/java/jni/cvc5_Grammar.cpp index 95af2108f..1ca9ea701 100644 --- a/src/api/java/jni/cvc5_Grammar.cpp +++ b/src/api/java/jni/cvc5_Grammar.cpp @@ -22,6 +22,22 @@ using namespace cvc5::api; /* * Class: cvc5_Grammar + * Method: copyGrammar + * Signature: (J)J + */ +JNIEXPORT jlong JNICALL Java_cvc5_Grammar_copyGrammar(JNIEnv* env, + jclass, + jlong pointer) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Grammar* current = reinterpret_cast<Grammar*>(pointer); + Grammar* retPointer = new Grammar(*current); + return reinterpret_cast<jlong>(retPointer); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); +} + +/* + * Class: cvc5_Grammar * Method: deletePointer * Signature: (J)V */ diff --git a/test/unit/api/java/cvc5/SolverTest.java b/test/unit/api/java/cvc5/SolverTest.java index 18560f2dc..d153b8a91 100644 --- a/test/unit/api/java/cvc5/SolverTest.java +++ b/test/unit/api/java/cvc5/SolverTest.java @@ -2338,7 +2338,7 @@ class SolverTest assertEquals(elements[indices[i]], simplifiedTerm); } - assertEquals("((_ tuple_project 0 3 2 0 1 2) (mkTuple true 3 \"C\" (singleton " + assertEquals("((_ tuple_project 0 3 2 0 1 2) (tuple true 3 \"C\" (singleton " + "\"Z\")))", projection.toString()); } |