From 690a3926569a29217df5000cfb673cc407ada356 Mon Sep 17 00:00:00 2001 From: mudathirmahgoub Date: Wed, 3 Nov 2021 16:32:10 -0500 Subject: [PATCH] Enable CI for Junit tests (#7436) This PR enables CI for java tests by adding --java-bindings to ci.yml. It also replaces the unreliable finalize method and instead uses AutoCloseable and explicit close method to clean up dynamic memory allocated by java native interface. The PR fixes compile errors for SolverTest.java and runtime errors for Solver.defineFun. --- .github/workflows/ci.yml | 2 +- examples/api/java/BitVectors.java | 202 +++++++------- examples/api/java/BitVectorsAndArrays.java | 114 ++++---- examples/api/java/Combination.java | 160 +++++------ examples/api/java/Datatypes.java | 84 +++--- examples/api/java/Exceptions.java | 73 ++--- examples/api/java/Extract.java | 42 +-- examples/api/java/FloatingPointArith.java | 120 ++++----- examples/api/java/HelloWorld.java | 8 +- examples/api/java/LinearArith.java | 82 +++--- examples/api/java/QuickStart.java | 233 ++++++++-------- examples/api/java/Relations.java | 250 +++++++++--------- examples/api/java/Sequences.java | 73 ++--- examples/api/java/Sets.java | 101 +++---- examples/api/java/Statistics.java | 64 ++--- examples/api/java/Strings.java | 114 ++++---- examples/api/java/SygusFun.java | 157 +++++------ examples/api/java/SygusGrammar.java | 111 ++++---- examples/api/java/SygusInv.java | 75 +++--- examples/api/java/Transcendentals.java | 58 ++-- examples/api/java/UnsatCores.java | 43 +-- .../io/github/cvc5/api/AbstractPointer.java | 14 +- src/api/java/io/github/cvc5/api/Datatype.java | 7 +- .../github/cvc5/api/DatatypeConstructor.java | 7 +- .../cvc5/api/DatatypeConstructorDecl.java | 7 +- .../java/io/github/cvc5/api/DatatypeDecl.java | 7 +- .../io/github/cvc5/api/DatatypeSelector.java | 7 +- src/api/java/io/github/cvc5/api/Grammar.java | 7 +- src/api/java/io/github/cvc5/api/Op.java | 7 +- .../java/io/github/cvc5/api/OptionInfo.java | 7 +- src/api/java/io/github/cvc5/api/Result.java | 7 +- src/api/java/io/github/cvc5/api/Solver.java | 28 +- src/api/java/io/github/cvc5/api/Sort.java | 9 +- src/api/java/io/github/cvc5/api/Stat.java | 7 +- .../java/io/github/cvc5/api/Statistics.java | 7 +- src/api/java/io/github/cvc5/api/Term.java | 7 +- src/api/java/jni/datatype.cpp | 2 +- src/api/java/jni/datatype_constructor.cpp | 2 +- .../java/jni/datatype_constructor_decl.cpp | 2 +- src/api/java/jni/datatype_decl.cpp | 2 +- src/api/java/jni/datatype_selector.cpp | 2 +- src/api/java/jni/grammar.cpp | 2 +- src/api/java/jni/op.cpp | 2 +- src/api/java/jni/option_info.cpp | 4 +- src/api/java/jni/result.cpp | 2 +- src/api/java/jni/solver.cpp | 17 +- src/api/java/jni/sort.cpp | 4 +- src/api/java/jni/stat.cpp | 2 +- src/api/java/jni/statistics.cpp | 4 +- src/api/java/jni/term.cpp | 2 +- test/unit/api/java/DatatypeTest.java | 5 + test/unit/api/java/GrammarTest.java | 5 + test/unit/api/java/OpTest.java | 5 + test/unit/api/java/ResultTest.java | 5 + test/unit/api/java/SolverTest.java | 77 +++++- test/unit/api/java/SortTest.java | 5 + test/unit/api/java/TermTest.java | 5 + 57 files changed, 1268 insertions(+), 1189 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 1acc26c5a..fedcb9bb4 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -38,7 +38,7 @@ jobs: - name: ubuntu:production-dbg os: ubuntu-18.04 - config: production --auto-download --assertions --tracing --unit-testing --editline + config: production --auto-download --assertions --tracing --unit-testing --java-bindings --editline cache-key: dbg check-units: true exclude_regress: 3-4 diff --git a/examples/api/java/BitVectors.java b/examples/api/java/BitVectors.java index 6209cf9dd..4d1d9e169 100644 --- a/examples/api/java/BitVectors.java +++ b/examples/api/java/BitVectors.java @@ -22,104 +22,106 @@ 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. - // - // Given a variable x that can only have two values, a or b. We want to - // assign to x a value other than the current one. The straightforward code - // to do that is: - // - //(0) if (x == a ) x = b; - // else x = a; - // - // Two more efficient yet equivalent methods are: - // - //(1) x = a ⊕ b ⊕ x; - // - //(2) x = a + b - x; - // - // 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 - Sort bitvector32 = slv.mkBitVectorSort(32); - - // Variables - 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 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 - slv.assertFormula(assumption); - - // Introduce a new variable for the new value of x after assignment. - 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; - 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 cvc5 "); - slv.assertFormula(assignment0); - System.out.println("Pushing a new context."); - slv.push(); - - // Encoding code (1) - // 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 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(" 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. "); - slv.pop(); - - // Encoding code (2) - // new_x_ = a + b - 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()); + try (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. + // + // Given a variable x that can only have two values, a or b. We want to + // assign to x a value other than the current one. The straightforward code + // to do that is: + // + //(0) if (x == a ) x = b; + // else x = a; + // + // Two more efficient yet equivalent methods are: + // + //(1) x = a ⊕ b ⊕ x; + // + //(2) x = a + b - x; + // + // 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 + Sort bitvector32 = slv.mkBitVectorSort(32); + + // Variables + 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 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 + slv.assertFormula(assumption); + + // Introduce a new variable for the new value of x after assignment. + 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; + 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 cvc5 "); + slv.assertFormula(assignment0); + System.out.println("Pushing a new context."); + slv.push(); + + // Encoding code (1) + // 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 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(" 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. "); + slv.pop(); + + // Encoding code (2) + // new_x_ = a + b - 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 07b9781d2..c72106082 100644 --- a/examples/api/java/BitVectorsAndArrays.java +++ b/examples/api/java/BitVectorsAndArrays.java @@ -27,73 +27,75 @@ public class BitVectorsAndArrays 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 + try (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): - // - // - // Assert (current_array[0] > 0); - // for (unsigned i = 1; i < k; ++i) { - // current_array[i] = 2 * current_array[i - 1]; - // Assert (current_array[i-1] < current_array[i]); - // } - // - // We want to check whether the assertion in the body of the for loop holds - // throughout the loop. + // Consider the following code (where size is some previously defined constant): + // + // + // Assert (current_array[0] > 0); + // for (unsigned i = 1; i < k; ++i) { + // current_array[i] = 2 * current_array[i - 1]; + // Assert (current_array[i-1] < current_array[i]); + // } + // + // We want to check whether the assertion in the body of the for loop holds + // throughout the loop. - // Setting up the problem parameters - int k = 4; // number of unrollings (should be a power of 2) - int index_size = log2(k); // size of the index + // Setting up the problem parameters + int k = 4; // number of unrollings (should be a power of 2) + int index_size = log2(k); // size of the index - // Sorts - Sort elementSort = slv.mkBitVectorSort(32); - Sort indexSort = slv.mkBitVectorSort(index_size); - Sort arraySort = slv.mkArraySort(indexSort, elementSort); + // Sorts + Sort elementSort = slv.mkBitVectorSort(32); + Sort indexSort = slv.mkBitVectorSort(index_size); + Sort arraySort = slv.mkArraySort(indexSort, elementSort); - // Variables - Term current_array = slv.mkConst(arraySort, "current_array"); + // Variables + Term current_array = slv.mkConst(arraySort, "current_array"); - // Making a bit-vector constant - Term zero = slv.mkBitVector(index_size, 0); + // Making a bit-vector constant + Term zero = slv.mkBitVector(index_size, 0); - // Asserting that current_array[0] > 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); + // Asserting that current_array[0] > 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 - Term index = slv.mkBitVector(index_size, 0); - Term old_current = slv.mkTerm(Kind.SELECT, current_array, index); - Term two = slv.mkBitVector(32, 2); + // Building the assertions in the loop unrolling + Term index = slv.mkBitVector(index_size, 0); + Term old_current = slv.mkTerm(Kind.SELECT, current_array, index); + Term two = slv.mkBitVector(32, 2); - List assertions = new ArrayList(); - 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 = slv.mkTerm(Kind.STORE, current_array, index, new_current); - // current[i-1] < current [i] - Term current_slt_new_current = slv.mkTerm(Kind.BITVECTOR_SLT, old_current, new_current); - assertions.add(current_slt_new_current); + List assertions = new ArrayList(); + 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 = slv.mkTerm(Kind.STORE, current_array, index, new_current); + // current[i-1] < current [i] + Term current_slt_new_current = slv.mkTerm(Kind.BITVECTOR_SLT, old_current, new_current); + assertions.add(current_slt_new_current); - old_current = slv.mkTerm(Kind.SELECT, current_array, index); - } + old_current = slv.mkTerm(Kind.SELECT, current_array, index); + } - Term query = slv.mkTerm(Kind.NOT, slv.mkTerm(Kind.AND, assertions.toArray(new Term[0]))); + Term query = slv.mkTerm(Kind.NOT, slv.mkTerm(Kind.AND, assertions.toArray(new Term[0]))); - System.out.println("Asserting " + query + " to cvc5 "); - slv.assertFormula(query); - System.out.println("Expect sat. "); - System.out.println("cvc5: " + slv.checkSatAssuming(slv.mkTrue())); + System.out.println("Asserting " + query + " to cvc5 "); + slv.assertFormula(query); + System.out.println("Expect sat. "); + System.out.println("cvc5: " + slv.checkSatAssuming(slv.mkTrue())); - // Getting the model - System.out.println("The satisfying model is: "); - System.out.println(" current_array = " + slv.getValue(current_array)); - System.out.println(" current_array[0] = " + slv.getValue(current_array0)); + // Getting the model + System.out.println("The satisfying model is: "); + 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/Combination.java b/examples/api/java/Combination.java index 66cd30b2b..03c43521a 100644 --- a/examples/api/java/Combination.java +++ b/examples/api/java/Combination.java @@ -39,89 +39,91 @@ public class Combination 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 - 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 - Term x = slv.mkConst(u, "x"); - Term y = slv.mkConst(u, "y"); - - // Functions - Term f = slv.mkConst(uToInt, "f"); - Term p = slv.mkConst(intPred, "p"); - - // Constants - Term zero = slv.mkInteger(0); - Term one = slv.mkInteger(1); - - // Terms - 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 it1 = assertions.iterator(); - while (it1.hasNext()) + try (Solver slv = new Solver()) { - Term t = it1.next(); - System.out.println("term: " + t); - Iterator it2 = t.iterator(); - while (it2.hasNext()) + 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 + 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 + Term x = slv.mkConst(u, "x"); + Term y = slv.mkConst(u, "y"); + + // Functions + Term f = slv.mkConst(uToInt, "f"); + Term p = slv.mkConst(intPred, "p"); + + // Constants + Term zero = slv.mkInteger(0); + Term one = slv.mkInteger(1); + + // Terms + 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 it1 = assertions.iterator(); + while (it1.hasNext()) { - System.out.println(" + child: " + it2.next()); + Term t = it1.next(); + System.out.println("term: " + t); + Iterator 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(); + System.out.println("Alternatively, you can also use for-each loops."); + for (Term t : assertions) { - System.out.println(" + child: " + c); + 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 85f878098..b29419165 100644 --- a/examples/api/java/Datatypes.java +++ b/examples/api/java/Datatypes.java @@ -123,46 +123,48 @@ public class Datatypes 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); + try (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 2d62a7570..bc142571d 100644 --- a/examples/api/java/Exceptions.java +++ b/examples/api/java/Exceptions.java @@ -21,45 +21,46 @@ public class Exceptions { public static void main(String[] args) { - Solver solver = new Solver(); - - solver.setOption("produce-models", "true"); - - // Setting an invalid option - try - { - solver.setOption("non-existing", "true"); - System.exit(1); - } - catch (Exception e) + try (Solver solver = new Solver()) { - System.out.println(e.toString()); - } + solver.setOption("produce-models", "true"); - // Creating a term with an invalid type - 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 (Exception e) - { - System.out.println(e.toString()); - } + // Setting an invalid option + try + { + solver.setOption("non-existing", "true"); + System.exit(1); + } + catch (Exception e) + { + System.out.println(e.toString()); + } - // Asking for a model after unsat result - try - { - solver.checkSatAssuming(solver.mkBoolean(false)); - solver.getModel(new Sort[] {}, new Term[] {}); - System.exit(1); - } - catch (Exception e) - { - System.out.println(e.toString()); + // Creating a term with an invalid type + 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 (Exception e) + { + System.out.println(e.toString()); + } + + // Asking for a model after unsat result + try + { + solver.checkSatAssuming(solver.mkBoolean(false)); + solver.getModel(new Sort[] {}, new Term[] {}); + System.exit(1); + } + catch (Exception e) + { + System.out.println(e.toString()); + } } } } diff --git a/examples/api/java/Extract.java b/examples/api/java/Extract.java index 0d8d6c2b2..4ec0c100f 100644 --- a/examples/api/java/Extract.java +++ b/examples/api/java/Extract.java @@ -21,32 +21,34 @@ public class Extract { public static void main(String args[]) throws CVC5ApiException { - Solver slv = new Solver(); - slv.setLogic("QF_BV"); // Set the logic + try (Solver slv = new Solver()) + { + slv.setLogic("QF_BV"); // Set the logic - Sort bitvector32 = slv.mkBitVectorSort(32); + Sort bitvector32 = slv.mkBitVectorSort(32); - Term x = slv.mkConst(bitvector32, "a"); + 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_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_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_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); + 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 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)); + 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 88e24cbab..d8ed384d0 100644 --- a/examples/api/java/FloatingPointArith.java +++ b/examples/api/java/FloatingPointArith.java @@ -26,76 +26,78 @@ public class FloatingPointArith { public static void main(String[] args) throws CVC5ApiException { - Solver solver = new Solver(); - solver.setOption("produce-models", "true"); + try (Solver solver = new 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"); + // 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(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))); + // Assert that floating-point addition is not associative: + // (a + (b + c)) != ((a + b) + c) + 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 = solver.checkSat(); // result is sat - assert r.isSat(); + Result r = solver.checkSat(); // result is sat + assert r.isSat(); - System.out.println("a = " + solver.getValue(a)); - System.out.println("b = " + solver.getValue(b)); - System.out.println("c = " + solver.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 - 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))); + // 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( + Kind.OR, solver.mkTerm(Kind.EQUAL, a, inf), solver.mkTerm(Kind.EQUAL, a, nan))); - r = solver.checkSat(); // result is sat - assert r.isSat(); + r = solver.checkSat(); // result is sat + assert r.isSat(); - System.out.println("a = " + solver.getValue(a)); - System.out.println("b = " + solver.getValue(b)); - System.out.println("c = " + solver.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. - 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))); + // 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(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 = solver.checkSat(); // result is sat - assert r.isSat(); + 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)); - System.out.println("d = " + val + " = " + realVal); - System.out.println("((_ fp.to_sbv 16) RTP d) = " + solver.getValue(lhs)); - System.out.println("((_ fp.to_sbv 16) RTN d) = " + solver.getValue(rhs)); + // Convert the result to a rational and print it + 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) = " + 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 - 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))); + // 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(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(); + r = solver.checkSat(); // result is unsat + assert !r.isSat(); + } } } diff --git a/examples/api/java/HelloWorld.java b/examples/api/java/HelloWorld.java index 966bfb329..7535430e3 100644 --- a/examples/api/java/HelloWorld.java +++ b/examples/api/java/HelloWorld.java @@ -19,9 +19,11 @@ public class HelloWorld { public static void main(String[] args) { - Solver slv = new Solver(); - Term helloworld = slv.mkVar(slv.getBooleanSort(), "Hello World!"); + try (Solver slv = new Solver()) + { + Term helloworld = slv.mkVar(slv.getBooleanSort(), "Hello World!"); - System.out.println(helloworld + " is " + slv.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 2e67d526f..1f8153e44 100644 --- a/examples/api/java/LinearArith.java +++ b/examples/api/java/LinearArith.java @@ -19,57 +19,59 @@ public class LinearArith { public static void main(String args[]) throws CVC5ApiException { - Solver slv = new Solver(); - slv.setLogic("QF_LIRA"); // Set the logic + try (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 + // Prove that if given x (Integer) and y (Real) then + // the maximum value of y - x is 2/3 - // Sorts - Sort real = slv.getRealSort(); - Sort integer = slv.getIntegerSort(); + // Sorts + Sort real = slv.getRealSort(); + Sort integer = slv.getIntegerSort(); - // Variables - Term x = slv.mkConst(integer, "x"); - Term y = slv.mkConst(real, "y"); + // Variables + Term x = slv.mkConst(integer, "x"); + Term y = slv.mkConst(real, "y"); - // Constants - Term three = slv.mkInteger(3); - Term neg2 = slv.mkInteger(-2); - Term two_thirds = slv.mkReal(2, 3); + // Constants + Term three = slv.mkInteger(3); + Term neg2 = slv.mkInteger(-2); + Term two_thirds = slv.mkReal(2, 3); - // Terms - Term three_y = slv.mkTerm(Kind.MULT, three, y); - Term diff = slv.mkTerm(Kind.MINUS, y, x); + // Terms + Term three_y = slv.mkTerm(Kind.MULT, three, y); + Term diff = slv.mkTerm(Kind.MINUS, y, x); - // Formulas - 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); + // Formulas + 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); - Term assertions = slv.mkTerm(Kind.AND, x_geq_3y, x_leq_y, neg2_lt_x); + 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); + System.out.println("Given the assertions " + assertions); + slv.assertFormula(assertions); - 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(); + 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(); + System.out.println(); - 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(); + 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."); + 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/QuickStart.java b/examples/api/java/QuickStart.java index 73bddb083..a79263cbf 100644 --- a/examples/api/java/QuickStart.java +++ b/examples/api/java/QuickStart.java @@ -25,123 +25,124 @@ 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 xRational = xVal.getRealValue(); - Pair 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 unsatCore = Arrays.asList(solver.getUnsatCore()); - System.out.println("unsat core size: " + unsatCore.size()); - System.out.println("unsat core: "); - for (Term t : unsatCore) + try (Solver solver = new Solver()) { - System.out.println(t); + // 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 xRational = xVal.getRealValue(); + Pair 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 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 f6454c812..0d78562bb 100644 --- a/examples/api/java/Relations.java +++ b/examples/api/java/Relations.java @@ -69,129 +69,131 @@ public class Relations { public static void main(String[] args) throws CVC5ApiException { - Solver solver = new Solver(); - - // Set the logic - solver.setLogic("ALL"); - - // 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 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 - 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 = solver.checkSat(); - - // output - 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)); + try (Solver solver = new Solver()) + { + // Set the logic + solver.setLogic("ALL"); + + // 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 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 + 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 = solver.checkSat(); + + // output + 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 index d1bb0440d..0fd578984 100644 --- a/examples/api/java/Sequences.java +++ b/examples/api/java/Sequences.java @@ -21,48 +21,49 @@ 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"); + try (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 sort + Sort intSeq = slv.mkSequenceSort(slv.getIntegerSort()); - // Sequence variables - Term x = slv.mkConst(intSeq, "x"); - Term y = slv.mkConst(intSeq, "y"); + // 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); + // 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); + // 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 + "."); + // 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)); + 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 index 602014c96..3edc49ae6 100644 --- a/examples/api/java/Sets.java +++ b/examples/api/java/Sets.java @@ -21,72 +21,73 @@ 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"); + try (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"); + // Produce models + slv.setOption("produce-models", "true"); + slv.setOption("output-language", "smt2"); - Sort integer = slv.getIntegerSort(); - Sort set = slv.mkSetSort(integer); + 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"); + // 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 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 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); + Term theorem = slv.mkTerm(EQUAL, lhs, rhs); - System.out.println("cvc5 reports: " + theorem + " is " + slv.checkEntailed(theorem) + "."); - } + 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); + // 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); + Term theorem = slv.mkTerm(SUBSET, emptyset, A); - System.out.println("cvc5 reports: " + theorem + " is " + slv.checkEntailed(theorem) + "."); - } + 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); + // 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 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 x = slv.mkConst(integer, "x"); - Term e = slv.mkTerm(MEMBER, x, intersection); + Term e = slv.mkTerm(MEMBER, x, intersection); - Result result = slv.checkSatAssuming(e); - System.out.println("cvc5 reports: " + e + " is " + result + "."); + 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."); + 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 e524eb3e3..751dda947 100644 --- a/examples/api/java/Statistics.java +++ b/examples/api/java/Statistics.java @@ -23,43 +23,45 @@ 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>` interface. - io.github.cvc5.api.Statistics stats = solver.getStatistics(); - // short version - System.out.println("Short version:"); - System.out.println(stats); + try (Solver solver = new Solver()) + { + // Get the statistics from the `Solver` and iterate over them. The + // `Statistics` class implements the `Iterable>` interface. + io.github.cvc5.api.Statistics stats = solver.getStatistics(); + // short version + System.out.println("Short version:"); + System.out.println(stats); - System.out.println("-------------------------------------------------------"); + System.out.println("-------------------------------------------------------"); - System.out.println("Long version:"); + System.out.println("Long version:"); - // long version - for (Pair 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()) + // long version + for (Pair pair : stats) { - System.out.println("-------------------------------------------------------"); - System.out.println(pair.first + " : Map"); - for (Map.Entry entry : stat.getHistogram().entrySet()) + 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(entry.getKey() + " = " + entry.getValue()); + System.out.println("-------------------------------------------------------"); + System.out.println(pair.first + " : Map"); + for (Map.Entry entry : stat.getHistogram().entrySet()) + { + System.out.println(entry.getKey() + " = " + entry.getValue()); + } + System.out.println("-------------------------------------------------------"); } - System.out.println("-------------------------------------------------------"); } } } diff --git a/examples/api/java/Strings.java b/examples/api/java/Strings.java index 6cc152159..28487b852 100644 --- a/examples/api/java/Strings.java +++ b/examples/api/java/Strings.java @@ -21,71 +21,73 @@ public class Strings { 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"); + try (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"); - // String type - Sort string = slv.getStringSort(); + // String type + Sort string = slv.getStringSort(); - // std::string - String str_ab = "ab"; - // String constants - 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"); + // std::string + String str_ab = "ab"; + // String constants + 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 - Term lhs = slv.mkTerm(STRING_CONCAT, x, ab, y); - // String concatenation: abc.z - Term rhs = slv.mkTerm(STRING_CONCAT, abc, z); - // x.ab.y = abc.z - Term formula1 = slv.mkTerm(EQUAL, lhs, rhs); + // String concatenation: x.ab.y + Term lhs = slv.mkTerm(STRING_CONCAT, x, ab, y); + // String concatenation: abc.z + Term rhs = slv.mkTerm(STRING_CONCAT, abc, z); + // x.ab.y = abc.z + Term formula1 = slv.mkTerm(EQUAL, lhs, rhs); - // Length of y: |y| - Term leny = slv.mkTerm(STRING_LENGTH, y); - // |y| >= 0 - Term formula2 = slv.mkTerm(GEQ, leny, slv.mkInteger(0)); + // Length of y: |y| + Term leny = slv.mkTerm(STRING_LENGTH, y); + // |y| >= 0 + Term formula2 = slv.mkTerm(GEQ, leny, slv.mkInteger(0)); - // Regular expression: (ab[c-e]*f)|g|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"))); + // Regular expression: (ab[c-e]*f)|g|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 - Term s1 = slv.mkConst(string, "s1"); - Term s2 = slv.mkConst(string, "s2"); - // String concatenation: s1.s2 - Term s = slv.mkTerm(STRING_CONCAT, s1, s2); + // String variables + Term s1 = slv.mkConst(string, "s1"); + Term s2 = slv.mkConst(string, "s2"); + // String concatenation: s1.s2 + Term s = slv.mkTerm(STRING_CONCAT, s1, s2); - // s1.s2 in (ab[c-e]*f)|g|h - Term formula3 = slv.mkTerm(STRING_IN_REGEXP, s, r); + // s1.s2 in (ab[c-e]*f)|g|h + Term formula3 = slv.mkTerm(STRING_IN_REGEXP, s, r); - // Make a query - Term q = slv.mkTerm(AND, formula1, formula2, formula3); + // Make a query + Term q = slv.mkTerm(AND, formula1, formula2, formula3); - // check sat - Result result = slv.checkSatAssuming(q); - System.out.println("cvc5 reports: " + q + " is " + result + "."); + // 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(" s1.s2 = " + slv.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 index 8b96dff50..bc1d7e6b1 100644 --- a/examples/api/java/SygusFun.java +++ b/examples/api/java/SygusFun.java @@ -56,84 +56,85 @@ 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()) + try (Solver slv = new Solver()) { - // 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)); + // 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 index fb079d49f..230229fdd 100644 --- a/examples/api/java/SygusGrammar.java +++ b/examples/api/java/SygusGrammar.java @@ -53,77 +53,78 @@ 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"); + try (Solver slv = new Solver()) + { + // required options + slv.setOption("lang", "sygus2"); + slv.setOption("incremental", "false"); - // set the logic - slv.setLogic("LIA"); + // set the logic + slv.setLogic("LIA"); - Sort integer = slv.getIntegerSort(); - Sort bool = slv.getBooleanSort(); + Sort integer = slv.getIntegerSort(); + Sort bool = slv.getBooleanSort(); - // declare input variable for the function-to-synthesize - Term x = slv.mkVar(integer, "x"); + // 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"); + // 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); + // 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}); + // 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}); + // 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); + // 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); + // 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); + // 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); + g3.addRule(start, zero); - Term id3 = slv.synthFun("id3", new Term[] {x}, integer, g3); + 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); + // 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"); + // 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); + 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})); + // 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)); + // 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 index 6c66c910b..be1311318 100644 --- a/examples/api/java/SygusInv.java +++ b/examples/api/java/SygusInv.java @@ -44,51 +44,52 @@ 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"); + try (Solver slv = new Solver()) + { + // required options + slv.setOption("lang", "sygus2"); + slv.setOption("incremental", "false"); - // set the logic - slv.setLogic("LIA"); + // set the logic + slv.setLogic("LIA"); - Sort integer = slv.getIntegerSort(); - Sort bool = slv.getBooleanSort(); + Sort integer = slv.getIntegerSort(); + Sort bool = slv.getBooleanSort(); - Term zero = slv.mkInteger(0); - Term one = slv.mkInteger(1); - Term ten = slv.mkInteger(10); + 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"); + // 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)); + // (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)); + // 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}); + // 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); + 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)); + // 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 index 026f9b826..a44a1e4c0 100644 --- a/examples/api/java/Transcendentals.java +++ b/examples/api/java/Transcendentals.java @@ -21,32 +21,34 @@ 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()); + try (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 cefa90290..feec35dbd 100644 --- a/examples/api/java/UnsatCores.java +++ b/examples/api/java/UnsatCores.java @@ -20,33 +20,34 @@ public class UnsatCores { public static void main(String[] args) throws CVC5ApiException { - Solver solver = new Solver(); - - // Enable the production of unsat cores - solver.setOption("produce-unsat-cores", "true"); + try (Solver solver = new Solver()) + { + // Enable the production of unsat cores + solver.setOption("produce-unsat-cores", "true"); - Sort boolSort = solver.getBooleanSort(); - Term a = solver.mkConst(boolSort, "A"); - Term b = solver.mkConst(boolSort, "B"); + Sort boolSort = solver.getBooleanSort(); + Term a = solver.mkConst(boolSort, "A"); + Term b = solver.mkConst(boolSort, "B"); - // A ^ B - solver.assertFormula(solver.mkTerm(Kind.AND, a, b)); - // ~(A v B) - solver.assertFormula(solver.mkTerm(Kind.NOT, solver.mkTerm(Kind.OR, a, b))); + // A ^ B + solver.assertFormula(solver.mkTerm(Kind.AND, a, b)); + // ~(A v B) + solver.assertFormula(solver.mkTerm(Kind.NOT, solver.mkTerm(Kind.OR, a, b))); - Result res = solver.checkSat(); // result is unsat + Result res = solver.checkSat(); // result is unsat - // Retrieve the unsat core - Term[] unsatCore = solver.getUnsatCore(); + // Retrieve the unsat core + Term[] unsatCore = solver.getUnsatCore(); - // Print the unsat core - System.out.println("Unsat Core: " + Arrays.asList(unsatCore)); + // Print the unsat core + System.out.println("Unsat Core: " + Arrays.asList(unsatCore)); - // Iterate over expressions in the unsat core. - System.out.println("--- Unsat Core ---"); - for (Term e : unsatCore) - { - System.out.println(e); + // Iterate over expressions in the unsat core. + System.out.println("--- Unsat Core ---"); + for (Term e : unsatCore) + { + System.out.println(e); + } } } } diff --git a/src/api/java/io/github/cvc5/api/AbstractPointer.java b/src/api/java/io/github/cvc5/api/AbstractPointer.java index 092e33d43..c627dcf84 100644 --- a/src/api/java/io/github/cvc5/api/AbstractPointer.java +++ b/src/api/java/io/github/cvc5/api/AbstractPointer.java @@ -18,13 +18,24 @@ package io.github.cvc5.api; abstract class AbstractPointer implements IPointer { protected final Solver solver; - protected final long pointer; + protected long pointer; public long getPointer() { return pointer; } + protected abstract void deletePointer(long pointer); + + void deletePointer() + { + if (pointer != 0) + { + deletePointer(pointer); + } + pointer = 0; + } + public Solver getSolver() { return solver; @@ -41,5 +52,6 @@ abstract class AbstractPointer implements IPointer { this.solver = solver; this.pointer = pointer; + solver.addAbstractPointer(this); } } diff --git a/src/api/java/io/github/cvc5/api/Datatype.java b/src/api/java/io/github/cvc5/api/Datatype.java index c5422c215..bc33ba10b 100644 --- a/src/api/java/io/github/cvc5/api/Datatype.java +++ b/src/api/java/io/github/cvc5/api/Datatype.java @@ -26,18 +26,13 @@ public class Datatype extends AbstractPointer implements Iterable abstractPointers = new ArrayList<>(); + + @Override public void close() + { + // delete heap memory for terms, sorts, etc + for (int i = abstractPointers.size() - 1; i >= 0; i--) + { + abstractPointers.get(i).deletePointer(); + } + // delete the heap memory for this solver + deletePointer(); + } + + void addAbstractPointer(AbstractPointer abstractPointer) { - deletePointer(pointer); + abstractPointers.add(abstractPointer); } static diff --git a/src/api/java/io/github/cvc5/api/Sort.java b/src/api/java/io/github/cvc5/api/Sort.java index ec7091e5c..440b1ba59 100644 --- a/src/api/java/io/github/cvc5/api/Sort.java +++ b/src/api/java/io/github/cvc5/api/Sort.java @@ -25,18 +25,13 @@ public class Sort extends AbstractPointer implements Comparable super(solver, pointer); } - protected static native void deletePointer(long pointer); + protected native void deletePointer(long pointer); public long getPointer() { return pointer; } - @Override public void finalize() - { - deletePointer(pointer); - } - // endregion /** @@ -799,4 +794,4 @@ public class Sort extends AbstractPointer implements Comparable } private native long[] getTupleSorts(long pointer); -} \ No newline at end of file +} diff --git a/src/api/java/io/github/cvc5/api/Stat.java b/src/api/java/io/github/cvc5/api/Stat.java index c0c81c472..6bcae5322 100644 --- a/src/api/java/io/github/cvc5/api/Stat.java +++ b/src/api/java/io/github/cvc5/api/Stat.java @@ -34,18 +34,13 @@ public class Stat extends AbstractPointer super(solver, pointer); } - protected static native void deletePointer(long pointer); + protected native void deletePointer(long pointer); public long getPointer() { return pointer; } - @Override public void finalize() - { - deletePointer(pointer); - } - // endregion /** diff --git a/src/api/java/io/github/cvc5/api/Statistics.java b/src/api/java/io/github/cvc5/api/Statistics.java index c874e483a..ad904aa1f 100644 --- a/src/api/java/io/github/cvc5/api/Statistics.java +++ b/src/api/java/io/github/cvc5/api/Statistics.java @@ -26,18 +26,13 @@ public class Statistics extends AbstractPointer implements Iterable, Iterable< super(solver, pointer); } - protected static native void deletePointer(long pointer); + protected native void deletePointer(long pointer); public long getPointer() { return pointer; } - @Override public void finalize() - { - deletePointer(pointer); - } - // endregion /** diff --git a/src/api/java/jni/datatype.cpp b/src/api/java/jni/datatype.cpp index 5efff9f2c..3f340c93c 100644 --- a/src/api/java/jni/datatype.cpp +++ b/src/api/java/jni/datatype.cpp @@ -25,7 +25,7 @@ using namespace cvc5::api; * Signature: (J)V */ JNIEXPORT void JNICALL Java_io_github_cvc5_api_Datatype_deletePointer( - JNIEnv* env, jclass, jlong pointer) + JNIEnv* env, jobject, jlong pointer) { delete ((Datatype*)pointer); } diff --git a/src/api/java/jni/datatype_constructor.cpp b/src/api/java/jni/datatype_constructor.cpp index 853766c3c..7fe5f21c6 100644 --- a/src/api/java/jni/datatype_constructor.cpp +++ b/src/api/java/jni/datatype_constructor.cpp @@ -26,7 +26,7 @@ using namespace cvc5::api; */ JNIEXPORT void JNICALL Java_io_github_cvc5_api_DatatypeConstructor_deletePointer(JNIEnv*, - jclass, + jobject, jlong pointer) { delete ((DatatypeConstructor*)pointer); diff --git a/src/api/java/jni/datatype_constructor_decl.cpp b/src/api/java/jni/datatype_constructor_decl.cpp index b13b75e45..75cdb7aca 100644 --- a/src/api/java/jni/datatype_constructor_decl.cpp +++ b/src/api/java/jni/datatype_constructor_decl.cpp @@ -26,7 +26,7 @@ using namespace cvc5::api; */ JNIEXPORT void JNICALL Java_io_github_cvc5_api_DatatypeConstructorDecl_deletePointer(JNIEnv*, - jclass, + jobject, jlong pointer) { delete ((DatatypeConstructorDecl*)pointer); diff --git a/src/api/java/jni/datatype_decl.cpp b/src/api/java/jni/datatype_decl.cpp index 845afac9d..1940c37e1 100644 --- a/src/api/java/jni/datatype_decl.cpp +++ b/src/api/java/jni/datatype_decl.cpp @@ -25,7 +25,7 @@ using namespace cvc5::api; * Signature: (J)V */ JNIEXPORT void JNICALL Java_io_github_cvc5_api_DatatypeDecl_deletePointer( - JNIEnv*, jclass, jlong pointer) + JNIEnv*, jobject, jlong pointer) { delete ((DatatypeDecl*)pointer); } diff --git a/src/api/java/jni/datatype_selector.cpp b/src/api/java/jni/datatype_selector.cpp index 964eb24f5..4a3358513 100644 --- a/src/api/java/jni/datatype_selector.cpp +++ b/src/api/java/jni/datatype_selector.cpp @@ -25,7 +25,7 @@ using namespace cvc5::api; * Signature: (J)V */ JNIEXPORT void JNICALL Java_io_github_cvc5_api_DatatypeSelector_deletePointer( - JNIEnv*, jclass, jlong pointer) + JNIEnv*, jobject, jlong pointer) { delete ((DatatypeSelector*)pointer); } diff --git a/src/api/java/jni/grammar.cpp b/src/api/java/jni/grammar.cpp index 4bafd54d6..751e5ffdd 100644 --- a/src/api/java/jni/grammar.cpp +++ b/src/api/java/jni/grammar.cpp @@ -40,7 +40,7 @@ Java_io_github_cvc5_api_Grammar_copyGrammar(JNIEnv* env, jclass, jlong pointer) * Signature: (J)V */ JNIEXPORT void JNICALL -Java_io_github_cvc5_api_Grammar_deletePointer(JNIEnv*, jclass, jlong pointer) +Java_io_github_cvc5_api_Grammar_deletePointer(JNIEnv*, jobject, jlong pointer) { delete reinterpret_cast(pointer); } diff --git a/src/api/java/jni/op.cpp b/src/api/java/jni/op.cpp index cb6a7a728..f34444001 100644 --- a/src/api/java/jni/op.cpp +++ b/src/api/java/jni/op.cpp @@ -25,7 +25,7 @@ using namespace cvc5::api; * Signature: (J)V */ JNIEXPORT void JNICALL Java_io_github_cvc5_api_Op_deletePointer(JNIEnv*, - jclass, + jobject, jlong pointer) { delete reinterpret_cast(pointer); diff --git a/src/api/java/jni/option_info.cpp b/src/api/java/jni/option_info.cpp index 031b1bae9..da2a485e3 100644 --- a/src/api/java/jni/option_info.cpp +++ b/src/api/java/jni/option_info.cpp @@ -24,8 +24,8 @@ using namespace cvc5::api; * Method: deletePointer * Signature: (J)V */ -JNIEXPORT void JNICALL -Java_io_github_cvc5_api_OptionInfo_deletePointer(JNIEnv*, jclass, jlong pointer) +JNIEXPORT void JNICALL Java_io_github_cvc5_api_OptionInfo_deletePointer( + JNIEnv*, jobject, jlong pointer) { delete reinterpret_cast(pointer); } diff --git a/src/api/java/jni/result.cpp b/src/api/java/jni/result.cpp index 34b3262ca..0534f240e 100644 --- a/src/api/java/jni/result.cpp +++ b/src/api/java/jni/result.cpp @@ -25,7 +25,7 @@ using namespace cvc5::api; * Signature: (J)V */ JNIEXPORT void JNICALL -Java_io_github_cvc5_api_Result_deletePointer(JNIEnv*, jclass, jlong pointer) +Java_io_github_cvc5_api_Result_deletePointer(JNIEnv*, jobject, jlong pointer) { delete ((Result*)pointer); } diff --git a/src/api/java/jni/solver.cpp b/src/api/java/jni/solver.cpp index bc4d7ff43..2d775c545 100644 --- a/src/api/java/jni/solver.cpp +++ b/src/api/java/jni/solver.cpp @@ -1679,15 +1679,14 @@ JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_declareSort( * Signature: (JLjava/lang/String;[JJJZ)J */ JNIEXPORT jlong JNICALL -Java_io_github_cvc5_api_Solver_defineFun__JLjava_lang_String_2_3JJJZ( - JNIEnv* env, - jobject, - jlong pointer, - jstring jSymbol, - jlongArray jVars, - jlong sortPointer, - jlong termPointer, - jboolean global) +Java_io_github_cvc5_api_Solver_defineFun(JNIEnv* env, + jobject, + jlong pointer, + jstring jSymbol, + jlongArray jVars, + jlong sortPointer, + jlong termPointer, + jboolean global) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Solver* solver = reinterpret_cast(pointer); diff --git a/src/api/java/jni/sort.cpp b/src/api/java/jni/sort.cpp index e5b4f06fe..2c7ee4fd0 100644 --- a/src/api/java/jni/sort.cpp +++ b/src/api/java/jni/sort.cpp @@ -25,7 +25,7 @@ using namespace cvc5::api; * Signature: (J)V */ JNIEXPORT void JNICALL Java_io_github_cvc5_api_Sort_deletePointer(JNIEnv*, - jclass, + jobject, jlong pointer) { delete reinterpret_cast(pointer); @@ -655,7 +655,7 @@ Java_io_github_cvc5_api_Sort_getConstructorDomainSorts(JNIEnv* env, std::vector sortPointers(sorts.size()); for (size_t i = 0; i < sorts.size(); i++) { - sortPointers[i] = reinterpret_cast (new Sort(sorts[i])); + sortPointers[i] = reinterpret_cast(new Sort(sorts[i])); } jlongArray ret = env->NewLongArray(sorts.size()); env->SetLongArrayRegion(ret, 0, sorts.size(), sortPointers.data()); diff --git a/src/api/java/jni/stat.cpp b/src/api/java/jni/stat.cpp index 5db362ce2..8b9efbd3f 100644 --- a/src/api/java/jni/stat.cpp +++ b/src/api/java/jni/stat.cpp @@ -25,7 +25,7 @@ using namespace cvc5::api; * Signature: (J)V */ JNIEXPORT void JNICALL Java_io_github_cvc5_api_Stat_deletePointer(JNIEnv*, - jclass, + jobject, jlong pointer) { delete reinterpret_cast(pointer); diff --git a/src/api/java/jni/statistics.cpp b/src/api/java/jni/statistics.cpp index 827c3184a..dfea8bf9d 100644 --- a/src/api/java/jni/statistics.cpp +++ b/src/api/java/jni/statistics.cpp @@ -26,8 +26,8 @@ using namespace cvc5::api; * Method: deletePointer * Signature: (J)V */ -JNIEXPORT void JNICALL -Java_io_github_cvc5_api_Statistics_deletePointer(JNIEnv*, jclass, jlong pointer) +JNIEXPORT void JNICALL Java_io_github_cvc5_api_Statistics_deletePointer( + JNIEnv*, jobject, jlong pointer) { delete reinterpret_cast(pointer); } diff --git a/src/api/java/jni/term.cpp b/src/api/java/jni/term.cpp index 5c8300e17..d54b0a2b5 100644 --- a/src/api/java/jni/term.cpp +++ b/src/api/java/jni/term.cpp @@ -25,7 +25,7 @@ using namespace cvc5::api; * Signature: (J)V */ JNIEXPORT void JNICALL Java_io_github_cvc5_api_Term_deletePointer(JNIEnv* env, - jclass, + jobject, jlong pointer) { delete reinterpret_cast(pointer); diff --git a/test/unit/api/java/DatatypeTest.java b/test/unit/api/java/DatatypeTest.java index cd9d7ee73..fb23ea515 100644 --- a/test/unit/api/java/DatatypeTest.java +++ b/test/unit/api/java/DatatypeTest.java @@ -33,6 +33,11 @@ class DatatypeTest d_solver = new Solver(); } + @AfterEach void tearDown() + { + d_solver.close(); + } + @Test void mkDatatypeSort() throws CVC5ApiException { DatatypeDecl dtypeSpec = d_solver.mkDatatypeDecl("list"); diff --git a/test/unit/api/java/GrammarTest.java b/test/unit/api/java/GrammarTest.java index e9b0d730c..37e1b5206 100644 --- a/test/unit/api/java/GrammarTest.java +++ b/test/unit/api/java/GrammarTest.java @@ -32,6 +32,11 @@ class GrammarTest d_solver = new Solver(); } + @AfterEach void tearDown() + { + d_solver.close(); + } + @Test void addRule() { Sort bool = d_solver.getBooleanSort(); diff --git a/test/unit/api/java/OpTest.java b/test/unit/api/java/OpTest.java index c63157155..9b4999211 100644 --- a/test/unit/api/java/OpTest.java +++ b/test/unit/api/java/OpTest.java @@ -32,6 +32,11 @@ class OpTest d_solver = new Solver(); } + @AfterEach void tearDown() + { + d_solver.close(); + } + @Test void getKind() throws CVC5ApiException { Op x; diff --git a/test/unit/api/java/ResultTest.java b/test/unit/api/java/ResultTest.java index 38e981888..59bd752ca 100644 --- a/test/unit/api/java/ResultTest.java +++ b/test/unit/api/java/ResultTest.java @@ -31,6 +31,11 @@ class ResultTest d_solver = new Solver(); } + @AfterEach void tearDown() + { + d_solver.close(); + } + @Test void isNull() { Result res_null = d_solver.getNullResult(); diff --git a/test/unit/api/java/SolverTest.java b/test/unit/api/java/SolverTest.java index 58b8d03aa..e61022e99 100644 --- a/test/unit/api/java/SolverTest.java +++ b/test/unit/api/java/SolverTest.java @@ -35,6 +35,11 @@ class SolverTest d_solver = new Solver(); } + @AfterEach void tearDown() + { + d_solver.close(); + } + @Test void recoverableException() throws CVC5ApiException { d_solver.setOption("produce-models", "true"); @@ -102,6 +107,7 @@ class SolverTest Solver slv = new Solver(); assertThrows(CVC5ApiException.class, () -> slv.mkArraySort(boolSort, boolSort)); + slv.close(); } @Test void mkBitVectorSort() throws CVC5ApiException @@ -132,6 +138,7 @@ class SolverTest DatatypeDecl throwsDtypeSpec = d_solver.mkDatatypeDecl("list"); assertThrows(CVC5ApiException.class, () -> d_solver.mkDatatypeSort(throwsDtypeSpec)); + slv.close(); } @Test void mkDatatypeSorts() throws CVC5ApiException @@ -175,6 +182,7 @@ class SolverTest assertThrows( CVC5ApiException.class, () -> slv.mkDatatypeSorts(Arrays.asList(udecls), unresSorts)); + slv.close(); /* Note: More tests are in datatype_api_black. */ } @@ -227,6 +235,7 @@ class SolverTest assertThrows(CVC5ApiException.class, () -> slv.mkFunctionSort(sorts1, slv.getIntegerSort())); assertThrows( CVC5ApiException.class, () -> slv.mkFunctionSort(sorts2, d_solver.getIntegerSort())); + slv.close(); } @Test void mkParamSort() throws CVC5ApiException @@ -248,6 +257,7 @@ class SolverTest Solver slv = new Solver(); assertThrows( CVC5ApiException.class, () -> slv.mkPredicateSort(new Sort[] {d_solver.getIntegerSort()})); + slv.close(); } @Test void mkRecordSort() throws CVC5ApiException @@ -263,6 +273,7 @@ class SolverTest Solver slv = new Solver(); assertThrows(CVC5ApiException.class, () -> slv.mkRecordSort(fields)); + slv.close(); } @Test void mkSetSort() throws CVC5ApiException @@ -272,6 +283,7 @@ class SolverTest assertDoesNotThrow(() -> d_solver.mkSetSort(d_solver.mkBitVectorSort(4))); Solver slv = new Solver(); assertThrows(CVC5ApiException.class, () -> slv.mkSetSort(d_solver.mkBitVectorSort(4))); + slv.close(); } @Test void mkBagSort() throws CVC5ApiException @@ -281,6 +293,7 @@ class SolverTest assertDoesNotThrow(() -> d_solver.mkBagSort(d_solver.mkBitVectorSort(4))); Solver slv = new Solver(); assertThrows(CVC5ApiException.class, () -> slv.mkBagSort(d_solver.mkBitVectorSort(4))); + slv.close(); } @Test void mkSequenceSort() throws CVC5ApiException @@ -290,6 +303,7 @@ class SolverTest () -> d_solver.mkSequenceSort(d_solver.mkSequenceSort(d_solver.getIntegerSort()))); Solver slv = new Solver(); assertThrows(CVC5ApiException.class, () -> slv.mkSequenceSort(d_solver.getIntegerSort())); + slv.close(); } @Test void mkUninterpretedSort() throws CVC5ApiException @@ -316,6 +330,7 @@ class SolverTest Solver slv = new Solver(); assertThrows( CVC5ApiException.class, () -> slv.mkTupleSort(new Sort[] {d_solver.getIntegerSort()})); + slv.close(); } @Test void mkBitVector() throws CVC5ApiException @@ -374,6 +389,7 @@ class SolverTest assertThrows(CVC5ApiException.class, () -> d_solver.mkVar(d_solver.getNullSort(), "a")); Solver slv = new Solver(); assertThrows(CVC5ApiException.class, () -> slv.mkVar(boolSort, "x")); + slv.close(); } @Test void mkBoolean() throws CVC5ApiException @@ -422,6 +438,7 @@ class SolverTest Solver slv = new Solver(); assertThrows(CVC5ApiException.class, () -> slv.mkFloatingPoint(3, 5, t1)); + slv.close(); } @Test void mkCardinalityConstraint() throws CVC5ApiException @@ -429,13 +446,11 @@ class SolverTest Sort su = d_solver.mkUninterpretedSort("u"); Sort si = d_solver.getIntegerSort(); assertDoesNotThrow(() -> d_solver.mkCardinalityConstraint(su, 3)); - assertThrows( - CVC5ApiException.class, () -> d_solver.mkCardinalityConstraint(si, 3)); - assertThrows( - CVC5ApiException.class, () -> d_solver.mkCardinalityConstraint(su, 0)); + assertThrows(CVC5ApiException.class, () -> d_solver.mkCardinalityConstraint(si, 3)); + assertThrows(CVC5ApiException.class, () -> d_solver.mkCardinalityConstraint(su, 0)); Solver slv = new Solver(); - assertThrows( - CVC5ApiException.class, () -> slv.mkCardinalityConstraint(su, 3)); + assertThrows(CVC5ApiException.class, () -> slv.mkCardinalityConstraint(su, 3)); + slv.close(); } @Test void mkEmptySet() throws CVC5ApiException @@ -446,6 +461,7 @@ class SolverTest assertDoesNotThrow(() -> d_solver.mkEmptySet(s)); assertThrows(CVC5ApiException.class, () -> d_solver.mkEmptySet(d_solver.getBooleanSort())); assertThrows(CVC5ApiException.class, () -> slv.mkEmptySet(s)); + slv.close(); } @Test void mkEmptyBag() throws CVC5ApiException @@ -457,6 +473,7 @@ class SolverTest assertThrows(CVC5ApiException.class, () -> d_solver.mkEmptyBag(d_solver.getBooleanSort())); assertThrows(CVC5ApiException.class, () -> slv.mkEmptyBag(s)); + slv.close(); } @Test void mkEmptySequence() throws CVC5ApiException @@ -466,6 +483,7 @@ class SolverTest assertDoesNotThrow(() -> d_solver.mkEmptySequence(s)); assertDoesNotThrow(() -> d_solver.mkEmptySequence(d_solver.getBooleanSort())); assertThrows(CVC5ApiException.class, () -> slv.mkEmptySequence(s)); + slv.close(); } @Test void mkFalse() throws CVC5ApiException @@ -639,6 +657,7 @@ class SolverTest assertThrows(CVC5ApiException.class, () -> d_solver.mkSepNil(d_solver.getNullSort())); Solver slv = new Solver(); assertThrows(CVC5ApiException.class, () -> slv.mkSepNil(d_solver.getIntegerSort())); + slv.close(); } @Test void mkString() @@ -704,6 +723,7 @@ class SolverTest assertThrows(CVC5ApiException.class, () -> d_solver.mkTerm(EQUAL, v2)); assertThrows(CVC5ApiException.class, () -> d_solver.mkTerm(EQUAL, v3)); assertThrows(CVC5ApiException.class, () -> d_solver.mkTerm(DISTINCT, v6)); + slv.close(); } @Test void mkTermFromOp() throws CVC5ApiException @@ -804,6 +824,7 @@ class SolverTest assertThrows(CVC5ApiException.class, () -> d_solver.mkTerm(opterm2, v2)); assertThrows(CVC5ApiException.class, () -> d_solver.mkTerm(opterm2, v3)); assertThrows(CVC5ApiException.class, () -> slv.mkTerm(opterm2, v4)); + slv.close(); } @Test void mkTrue() @@ -844,6 +865,7 @@ class SolverTest () -> slv.mkTuple(new Sort[] {slv.mkBitVectorSort(3)}, new Term[] {d_solver.mkBitVector(3, "101", 2)})); + slv.close(); } @Test void mkUniverseSet() @@ -852,6 +874,7 @@ class SolverTest assertThrows(CVC5ApiException.class, () -> d_solver.mkUniverseSet(d_solver.getNullSort())); Solver slv = new Solver(); assertThrows(CVC5ApiException.class, () -> slv.mkUniverseSet(d_solver.getBooleanSort())); + slv.close(); } @Test void mkConst() @@ -870,6 +893,7 @@ class SolverTest Solver slv = new Solver(); assertThrows(CVC5ApiException.class, () -> slv.mkConst(boolSort)); + slv.close(); } @Test void mkConstArray() @@ -892,6 +916,7 @@ class SolverTest Sort arrSort2 = slv.mkArraySort(slv.getIntegerSort(), slv.getIntegerSort()); assertThrows(CVC5ApiException.class, () -> slv.mkConstArray(arrSort2, zero)); assertThrows(CVC5ApiException.class, () -> slv.mkConstArray(arrSort, zero2)); + slv.close(); } @Test void declareDatatype() @@ -914,6 +939,7 @@ class SolverTest Solver slv = new Solver(); assertThrows(CVC5ApiException.class, () -> slv.declareDatatype(("a"), ctors1)); + slv.close(); } @Test void declareFun() throws CVC5ApiException @@ -932,6 +958,7 @@ class SolverTest Solver slv = new Solver(); assertThrows(CVC5ApiException.class, () -> slv.declareFun("f1", new Sort[] {}, bvSort)); + slv.close(); } @Test void declareSort() @@ -974,7 +1001,7 @@ class SolverTest assertThrows( CVC5ApiException.class, () -> d_solver.defineFun("fff", new Term[] {b1}, bvSort, v2)); assertThrows( - CVC5ApiException.class, () -> d_solver.defineFun("ffff", new Term[] {b1}, funSort2, v2)); + CVC5ApiException.class, () -> d_solver.defineFun("ffff", new Term[] {b1}, funSort, v2)); // b3 has function sort, which is allowed as an argument assertDoesNotThrow(() -> d_solver.defineFun("fffff", new Term[] {b1, b3}, bvSort, v1)); @@ -994,6 +1021,7 @@ class SolverTest CVC5ApiException.class, () -> slv.defineFun("ff", new Term[] {b12, b22}, bvSort, v12)); assertThrows( CVC5ApiException.class, () -> slv.defineFun("ff", new Term[] {b12, b22}, bvSort2, v1)); + slv.close(); } @Test void defineFunGlobal() @@ -1074,6 +1102,7 @@ class SolverTest assertThrows( CVC5ApiException.class, () -> slv.defineFunRec("ff", new Term[] {b12, b22}, bvSort2, v1)); + slv.close(); } @Test void defineFunRecWrongLogic() throws CVC5ApiException @@ -1201,6 +1230,7 @@ class SolverTest () -> slv.defineFunsRec( new Term[] {f12, f22}, new Term[][] {{b12, b112}, {b42}}, new Term[] {v12, v2})); + slv.close(); } @Test void defineFunsRecWrongLogic() throws CVC5ApiException @@ -1581,6 +1611,7 @@ class SolverTest Solver slv = new Solver(); assertThrows(CVC5ApiException.class, () -> slv.getValue(x)); + slv.close(); } @Test void getModelDomainElements() @@ -1680,10 +1711,12 @@ class SolverTest d_solver.mkTerm(OR, x, d_solver.mkTerm(NOT, x))); assertThrows( CVC5ApiException.class, () -> d_solver.getQuantifierElimination(d_solver.getNullTerm())); - assertThrows(CVC5ApiException.class, - () -> d_solver.getQuantifierElimination(new Solver().mkBoolean(false))); + Solver slv = new Solver(); + assertThrows( + CVC5ApiException.class, () -> d_solver.getQuantifierElimination(slv.mkBoolean(false))); assertDoesNotThrow(() -> d_solver.getQuantifierElimination(forall)); + slv.close(); } @Test void getQuantifierEliminationDisjunct() @@ -1695,10 +1728,12 @@ class SolverTest assertThrows(CVC5ApiException.class, () -> d_solver.getQuantifierEliminationDisjunct(d_solver.getNullTerm())); + Solver slv = new Solver(); assertThrows(CVC5ApiException.class, - () -> d_solver.getQuantifierEliminationDisjunct(new Solver().mkBoolean(false))); + () -> d_solver.getQuantifierEliminationDisjunct(slv.mkBoolean(false))); assertDoesNotThrow(() -> d_solver.getQuantifierEliminationDisjunct(forall)); + slv.close(); } @Test void declareSeparationHeap() throws CVC5ApiException @@ -1910,8 +1945,10 @@ class SolverTest assertThrows(CVC5ApiException.class, () -> d_solver.blockModelValues(new Term[] {})); assertThrows(CVC5ApiException.class, () -> d_solver.blockModelValues(new Term[] {d_solver.getNullTerm()})); - assertThrows(CVC5ApiException.class, - () -> d_solver.blockModelValues(new Term[] {new Solver().mkBoolean(false)})); + Solver slv = new Solver(); + assertThrows( + CVC5ApiException.class, () -> d_solver.blockModelValues(new Term[] {slv.mkBoolean(false)})); + slv.close(); } @Test void blockModelValues2() throws CVC5ApiException @@ -2049,6 +2086,7 @@ class SolverTest d_solver.defineFunsRec(new Term[] {f1, f2}, new Term[][] {{b1, b2}, {b3}}, new Term[] {v1, v2}); assertDoesNotThrow(() -> d_solver.simplify(f1)); assertDoesNotThrow(() -> d_solver.simplify(f2)); + slv.close(); } @Test void assertFormula() @@ -2057,6 +2095,7 @@ class SolverTest assertThrows(CVC5ApiException.class, () -> d_solver.assertFormula(d_solver.getNullTerm())); Solver slv = new Solver(); assertThrows(CVC5ApiException.class, () -> slv.assertFormula(d_solver.mkTrue())); + slv.close(); } @Test void checkEntailed() @@ -2066,6 +2105,7 @@ class SolverTest assertThrows(CVC5ApiException.class, () -> d_solver.checkEntailed(d_solver.mkTrue())); Solver slv = new Solver(); assertThrows(CVC5ApiException.class, () -> slv.checkEntailed(d_solver.mkTrue())); + slv.close(); } @Test void checkEntailed1() @@ -2081,6 +2121,7 @@ class SolverTest assertDoesNotThrow(() -> d_solver.checkEntailed(z)); Solver slv = new Solver(); assertThrows(CVC5ApiException.class, () -> slv.checkEntailed(d_solver.mkTrue())); + slv.close(); } @Test void checkEntailed2() @@ -2131,6 +2172,7 @@ class SolverTest Solver slv = new Solver(); assertThrows(CVC5ApiException.class, () -> slv.checkEntailed(d_solver.mkTrue())); + slv.close(); } @Test void checkSat() throws CVC5ApiException @@ -2147,6 +2189,7 @@ class SolverTest assertThrows(CVC5ApiException.class, () -> d_solver.checkSatAssuming(d_solver.mkTrue())); Solver slv = new Solver(); assertThrows(CVC5ApiException.class, () -> slv.checkSatAssuming(d_solver.mkTrue())); + slv.close(); } @Test void checkSatAssuming1() throws CVC5ApiException @@ -2162,6 +2205,7 @@ class SolverTest assertDoesNotThrow(() -> d_solver.checkSatAssuming(z)); Solver slv = new Solver(); assertThrows(CVC5ApiException.class, () -> slv.checkSatAssuming(d_solver.mkTrue())); + slv.close(); } @Test void checkSatAssuming2() throws CVC5ApiException @@ -2212,6 +2256,7 @@ class SolverTest Solver slv = new Solver(); assertThrows(CVC5ApiException.class, () -> slv.checkSatAssuming(d_solver.mkTrue())); + slv.close(); } @Test void setLogic() throws CVC5ApiException @@ -2261,6 +2306,7 @@ class SolverTest Solver slv = new Solver(); assertThrows(CVC5ApiException.class, () -> slv.mkSygusVar(boolSort)); + slv.close(); } @Test void mkSygusGrammar() throws CVC5ApiException @@ -2291,6 +2337,7 @@ class SolverTest () -> slv.mkSygusGrammar(new Term[] {boolVar}, new Term[] {intVar2})); assertThrows(CVC5ApiException.class, () -> slv.mkSygusGrammar(new Term[] {boolVar2}, new Term[] {intVar})); + slv.close(); } @Test void synthFun() throws CVC5ApiException @@ -2328,6 +2375,7 @@ class SolverTest CVC5ApiException.class, () -> slv.synthFun("", new Term[] {}, d_solver.getBooleanSort())); assertThrows(CVC5ApiException.class, () -> slv.synthFun("f1", new Term[] {x}, d_solver.getBooleanSort())); + slv.close(); } @Test void synthInv() throws CVC5ApiException @@ -2367,6 +2415,7 @@ class SolverTest Solver slv = new Solver(); assertThrows(CVC5ApiException.class, () -> slv.addSygusConstraint(boolTerm)); + slv.close(); } @Test void addSygusAssume() @@ -2381,6 +2430,7 @@ class SolverTest Solver slv = new Solver(); assertThrows(CVC5ApiException.class, () -> slv.addSygusAssume(boolTerm)); + slv.close(); } @Test void addSygusInvConstraint() throws CVC5ApiException @@ -2445,6 +2495,7 @@ class SolverTest CVC5ApiException.class, () -> slv.addSygusInvConstraint(inv22, pre22, trans, post22)); assertThrows( CVC5ApiException.class, () -> slv.addSygusInvConstraint(inv22, pre22, trans22, post)); + slv.close(); } @Test void getSynthSolution() throws CVC5ApiException @@ -2468,6 +2519,7 @@ class SolverTest Solver slv = new Solver(); assertThrows(CVC5ApiException.class, () -> slv.getSynthSolution(f)); + slv.close(); } @Test void getSynthSolutions() throws CVC5ApiException @@ -2493,6 +2545,7 @@ class SolverTest Solver slv = new Solver(); assertThrows(CVC5ApiException.class, () -> slv.getSynthSolutions(new Term[] {x})); + slv.close(); } @Test void tupleProject() throws CVC5ApiException diff --git a/test/unit/api/java/SortTest.java b/test/unit/api/java/SortTest.java index 6649e5de0..977ba483e 100644 --- a/test/unit/api/java/SortTest.java +++ b/test/unit/api/java/SortTest.java @@ -36,6 +36,11 @@ class SortTest d_solver = new Solver(); } + @AfterEach void tearDown() + { + d_solver.close(); + } + Sort create_datatype_sort() throws CVC5ApiException { DatatypeDecl dtypeSpec = d_solver.mkDatatypeDecl("list"); diff --git a/test/unit/api/java/TermTest.java b/test/unit/api/java/TermTest.java index cb59849e0..94f35e97f 100644 --- a/test/unit/api/java/TermTest.java +++ b/test/unit/api/java/TermTest.java @@ -39,6 +39,11 @@ class TermTest d_solver = new Solver(); } + @AfterEach void tearDown() + { + d_solver.close(); + } + @Test void eq() { Sort uSort = d_solver.mkUninterpretedSort("u"); -- 2.30.2