diff options
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<Term> assertions = new ArrayList<Term>(); - for (int i = 1; i < k; ++i) - { - index = slv.mkBitVector(index_size, i); - Term new_current = slv.mkTerm(Kind.BITVECTOR_MULT, two, old_current); - // current[i] = 2 * current[i-1] - current_array = 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<Term> assertions = new ArrayList<Term>(); + for (int i = 1; i < k; ++i) + { + index = slv.mkBitVector(index_size, i); + Term new_current = slv.mkTerm(Kind.BITVECTOR_MULT, two, old_current); + // current[i] = 2 * current[i-1] + current_array = 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<Term> it1 = assertions.iterator(); - while (it1.hasNext()) + try (Solver slv = new Solver()) { - Term t = it1.next(); - System.out.println("term: " + t); - Iterator<Term> 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<Term> it1 = assertions.iterator(); + while (it1.hasNext()) { - System.out.println(" + child: " + it2.next()); + Term t = it1.next(); + System.out.println("term: " + t); + Iterator<Term> it2 = t.iterator(); + while (it2.hasNext()) + { + System.out.println(" + child: " + it2.next()); + } } - } - System.out.println(); - System.out.println("Alternatively, you can also use for-each loops."); - for (Term t : assertions) - { - System.out.println("term: " + t); - for (Term c : t) + System.out.println(); + 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<BigInteger, BigInteger> xRational = xVal.getRealValue(); - Pair<BigInteger, BigInteger> yRational = yVal.getRealValue(); - System.out.println("value for x: " + xRational.first + "/" + xRational.second); - System.out.println("value for y: " + yRational.first + "/" + yRational.second); - - // Next, we will check satisfiability of the same formula, - // only this time over integer variables a and b. - - // We start by resetting assertions added to the solver. - solver.resetAssertions(); - - // Next, we assert the same assertions above with integers. - // This time, we inline the construction of terms - // to the assertion command. - solver.assertFormula(solver.mkTerm(Kind.LT, solver.mkInteger(0), a)); - solver.assertFormula(solver.mkTerm(Kind.LT, solver.mkInteger(0), b)); - solver.assertFormula( - solver.mkTerm(Kind.LT, solver.mkTerm(Kind.PLUS, a, b), solver.mkInteger(1))); - solver.assertFormula(solver.mkTerm(Kind.LEQ, a, b)); - - // We check whether the revised assertion is satisfiable. - Result r2 = solver.checkSat(); - - // This time the formula is unsatisfiable - System.out.println("expected: unsat"); - System.out.println("result: " + r2); - - // We can query the solver for an unsatisfiable core, i.e., a subset - // of the assertions that is already unsatisfiable. - List<Term> unsatCore = Arrays.asList(solver.getUnsatCore()); - System.out.println("unsat core size: " + unsatCore.size()); - System.out.println("unsat core: "); - for (Term t : unsatCore) + 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<BigInteger, BigInteger> xRational = xVal.getRealValue(); + Pair<BigInteger, BigInteger> yRational = yVal.getRealValue(); + System.out.println("value for x: " + xRational.first + "/" + xRational.second); + System.out.println("value for y: " + yRational.first + "/" + yRational.second); + + // Next, we will check satisfiability of the same formula, + // only this time over integer variables a and b. + + // We start by resetting assertions added to the solver. + solver.resetAssertions(); + + // Next, we assert the same assertions above with integers. + // This time, we inline the construction of terms + // to the assertion command. + solver.assertFormula(solver.mkTerm(Kind.LT, solver.mkInteger(0), a)); + solver.assertFormula(solver.mkTerm(Kind.LT, solver.mkInteger(0), b)); + solver.assertFormula( + solver.mkTerm(Kind.LT, solver.mkTerm(Kind.PLUS, a, b), solver.mkInteger(1))); + solver.assertFormula(solver.mkTerm(Kind.LEQ, a, b)); + + // We check whether the revised assertion is satisfiable. + Result r2 = solver.checkSat(); + + // This time the formula is unsatisfiable + System.out.println("expected: unsat"); + System.out.println("result: " + r2); + + // We can query the solver for an unsatisfiable core, i.e., a subset + // of the assertions that is already unsatisfiable. + List<Term> unsatCore = Arrays.asList(solver.getUnsatCore()); + System.out.println("unsat core size: " + unsatCore.size()); + System.out.println("unsat core: "); + for (Term t : unsatCore) + { + System.out.println(t); + } } } }
\ No newline at end of file diff --git a/examples/api/java/Relations.java b/examples/api/java/Relations.java index 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<Pair<String, Stat>>` 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<Pair<String, Stat>>` 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<String, Stat> pair : stats) - { - Stat stat = pair.second; - if (stat.isInt()) - { - System.out.println(pair.first + " = " + stat.getInt()); - } - else if (stat.isDouble()) - { - System.out.println(pair.first + " = " + stat.getDouble()); - } - else if (stat.isString()) - { - System.out.println(pair.first + " = " + stat.getString()); - } - else if (stat.isHistogram()) + // long version + for (Pair<String, Stat> pair : stats) { - System.out.println("-------------------------------------------------------"); - System.out.println(pair.first + " : Map"); - for (Map.Entry<String, Long> 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<String, Long> 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<DatatypeConstr 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/DatatypeConstructor.java b/src/api/java/io/github/cvc5/api/DatatypeConstructor.java index f41acee85..5fd9d8407 100644 --- a/src/api/java/io/github/cvc5/api/DatatypeConstructor.java +++ b/src/api/java/io/github/cvc5/api/DatatypeConstructor.java @@ -26,18 +26,13 @@ public class DatatypeConstructor extends AbstractPointer implements Iterable<Dat 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 /** @return the name of this Datatype constructor. */ diff --git a/src/api/java/io/github/cvc5/api/DatatypeConstructorDecl.java b/src/api/java/io/github/cvc5/api/DatatypeConstructorDecl.java index da3fa3582..e1f5ca746 100644 --- a/src/api/java/io/github/cvc5/api/DatatypeConstructorDecl.java +++ b/src/api/java/io/github/cvc5/api/DatatypeConstructorDecl.java @@ -23,18 +23,13 @@ public class DatatypeConstructorDecl 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/DatatypeDecl.java b/src/api/java/io/github/cvc5/api/DatatypeDecl.java index ad90c0987..fb8da9abd 100644 --- a/src/api/java/io/github/cvc5/api/DatatypeDecl.java +++ b/src/api/java/io/github/cvc5/api/DatatypeDecl.java @@ -23,18 +23,13 @@ public class DatatypeDecl 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 /** * Add datatype constructor declaration. diff --git a/src/api/java/io/github/cvc5/api/DatatypeSelector.java b/src/api/java/io/github/cvc5/api/DatatypeSelector.java index 7a0907c9d..d388e7f2b 100644 --- a/src/api/java/io/github/cvc5/api/DatatypeSelector.java +++ b/src/api/java/io/github/cvc5/api/DatatypeSelector.java @@ -23,18 +23,13 @@ public class DatatypeSelector 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 /** @return the name of this Datatype selector. */ diff --git a/src/api/java/io/github/cvc5/api/Grammar.java b/src/api/java/io/github/cvc5/api/Grammar.java index 860bb8302..49a29670d 100644 --- a/src/api/java/io/github/cvc5/api/Grammar.java +++ b/src/api/java/io/github/cvc5/api/Grammar.java @@ -30,18 +30,13 @@ public class Grammar extends AbstractPointer private static native long copyGrammar(long 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/Op.java b/src/api/java/io/github/cvc5/api/Op.java index 86d893785..096fd559d 100644 --- a/src/api/java/io/github/cvc5/api/Op.java +++ b/src/api/java/io/github/cvc5/api/Op.java @@ -23,18 +23,13 @@ public class Op 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/OptionInfo.java b/src/api/java/io/github/cvc5/api/OptionInfo.java index 76633a8a6..6f6024420 100644 --- a/src/api/java/io/github/cvc5/api/OptionInfo.java +++ b/src/api/java/io/github/cvc5/api/OptionInfo.java @@ -46,18 +46,13 @@ public class OptionInfo extends AbstractPointer this.baseInfo = getBaseInfo(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); - } - /** * @return a string representation of this optionInfo. */ diff --git a/src/api/java/io/github/cvc5/api/Result.java b/src/api/java/io/github/cvc5/api/Result.java index 500ec7f16..3a34fbda6 100644 --- a/src/api/java/io/github/cvc5/api/Result.java +++ b/src/api/java/io/github/cvc5/api/Result.java @@ -26,18 +26,13 @@ public class Result 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 public enum UnknownExplanation { diff --git a/src/api/java/io/github/cvc5/api/Solver.java b/src/api/java/io/github/cvc5/api/Solver.java index c57ba48b8..6c1399d9c 100644 --- a/src/api/java/io/github/cvc5/api/Solver.java +++ b/src/api/java/io/github/cvc5/api/Solver.java @@ -18,9 +18,9 @@ package io.github.cvc5.api; import java.io.IOException; import java.util.*; -public class Solver implements IPointer +public class Solver implements IPointer, AutoCloseable { - private final long pointer; + private long pointer; public long getPointer() { @@ -31,14 +31,32 @@ public class Solver implements IPointer public void deletePointer() { - deletePointer(pointer); + if (pointer != 0) + { + deletePointer(pointer); + } + pointer = 0; } private static native void deletePointer(long pointer); - @Override public void finalize() + // store pointers for terms, sorts, etc + List<AbstractPointer> 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<Sort> 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<Sort> } 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<Pair<String, 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/Term.java b/src/api/java/io/github/cvc5/api/Term.java index 7a1798b65..bbed609f7 100644 --- a/src/api/java/io/github/cvc5/api/Term.java +++ b/src/api/java/io/github/cvc5/api/Term.java @@ -31,18 +31,13 @@ public class Term extends AbstractPointer implements Comparable<Term>, 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<Grammar*>(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<Op*>(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<OptionInfo*>(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<Solver*>(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<Sort*>(pointer); @@ -655,7 +655,7 @@ Java_io_github_cvc5_api_Sort_getConstructorDomainSorts(JNIEnv* env, std::vector<jlong> sortPointers(sorts.size()); for (size_t i = 0; i < sorts.size(); i++) { - sortPointers[i] = reinterpret_cast<jlong> (new Sort(sorts[i])); + sortPointers[i] = reinterpret_cast<jlong>(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<Stat*>(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<Statistics*>(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<Term*>(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"); |