This PR enables CI for java tests by adding --java-bindings to ci.yml.
It also replaces the unreliable finalize method and instead uses AutoCloseable and explicit close method to clean up dynamic memory allocated by java native interface.
The PR fixes compile errors for SolverTest.java and runtime errors for Solver.defineFun.
- 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
{
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
+}
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));
+ }
}
}
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);
+ }
}
}
}
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);
+ }
}
}
{
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());
+ }
}
}
}
{
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
+}
{
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();
+ }
}
}
{
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));
+ }
}
}
{
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
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
{
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));
+ }
}
}
{
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
{
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
+}
{
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("-------------------------------------------------------");
}
}
}
{
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
+}
{
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
+}
{
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
+}
{
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
+}
{
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
+}
{
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);
+ }
}
}
}
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;
{
this.solver = solver;
this.pointer = pointer;
+ solver.addAbstractPointer(this);
}
}
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
/**
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. */
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
/**
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.
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. */
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
/**
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
/**
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.
*/
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 {
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()
{
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
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
/**
}
private native long[] getTupleSorts(long pointer);
-}
\ No newline at end of file
+}
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
/**
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
/**
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
/**
* 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);
}
*/
JNIEXPORT void JNICALL
Java_io_github_cvc5_api_DatatypeConstructor_deletePointer(JNIEnv*,
- jclass,
+ jobject,
jlong pointer)
{
delete ((DatatypeConstructor*)pointer);
*/
JNIEXPORT void JNICALL
Java_io_github_cvc5_api_DatatypeConstructorDecl_deletePointer(JNIEnv*,
- jclass,
+ jobject,
jlong pointer)
{
delete ((DatatypeConstructorDecl*)pointer);
* Signature: (J)V
*/
JNIEXPORT void JNICALL Java_io_github_cvc5_api_DatatypeDecl_deletePointer(
- JNIEnv*, jclass, jlong pointer)
+ JNIEnv*, jobject, jlong pointer)
{
delete ((DatatypeDecl*)pointer);
}
* Signature: (J)V
*/
JNIEXPORT void JNICALL Java_io_github_cvc5_api_DatatypeSelector_deletePointer(
- JNIEnv*, jclass, jlong pointer)
+ JNIEnv*, jobject, jlong pointer)
{
delete ((DatatypeSelector*)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);
}
* Signature: (J)V
*/
JNIEXPORT void JNICALL Java_io_github_cvc5_api_Op_deletePointer(JNIEnv*,
- jclass,
+ jobject,
jlong pointer)
{
delete reinterpret_cast<Op*>(pointer);
* 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);
}
* 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);
}
* 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);
* Signature: (J)V
*/
JNIEXPORT void JNICALL Java_io_github_cvc5_api_Sort_deletePointer(JNIEnv*,
- jclass,
+ jobject,
jlong pointer)
{
delete reinterpret_cast<Sort*>(pointer);
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());
* Signature: (J)V
*/
JNIEXPORT void JNICALL Java_io_github_cvc5_api_Stat_deletePointer(JNIEnv*,
- jclass,
+ jobject,
jlong pointer)
{
delete reinterpret_cast<Stat*>(pointer);
* 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);
}
* Signature: (J)V
*/
JNIEXPORT void JNICALL Java_io_github_cvc5_api_Term_deletePointer(JNIEnv* env,
- jclass,
+ jobject,
jlong pointer)
{
delete reinterpret_cast<Term*>(pointer);
d_solver = new Solver();
}
+ @AfterEach void tearDown()
+ {
+ d_solver.close();
+ }
+
@Test void mkDatatypeSort() throws CVC5ApiException
{
DatatypeDecl dtypeSpec = d_solver.mkDatatypeDecl("list");
d_solver = new Solver();
}
+ @AfterEach void tearDown()
+ {
+ d_solver.close();
+ }
+
@Test void addRule()
{
Sort bool = d_solver.getBooleanSort();
d_solver = new Solver();
}
+ @AfterEach void tearDown()
+ {
+ d_solver.close();
+ }
+
@Test void getKind() throws CVC5ApiException
{
Op x;
d_solver = new Solver();
}
+ @AfterEach void tearDown()
+ {
+ d_solver.close();
+ }
+
@Test void isNull()
{
Result res_null = d_solver.getNullResult();
d_solver = new Solver();
}
+ @AfterEach void tearDown()
+ {
+ d_solver.close();
+ }
+
@Test void recoverableException() throws CVC5ApiException
{
d_solver.setOption("produce-models", "true");
Solver slv = new Solver();
assertThrows(CVC5ApiException.class, () -> slv.mkArraySort(boolSort, boolSort));
+ slv.close();
}
@Test void mkBitVectorSort() throws CVC5ApiException
DatatypeDecl throwsDtypeSpec = d_solver.mkDatatypeDecl("list");
assertThrows(CVC5ApiException.class, () -> d_solver.mkDatatypeSort(throwsDtypeSpec));
+ slv.close();
}
@Test void mkDatatypeSorts() throws CVC5ApiException
assertThrows(
CVC5ApiException.class, () -> slv.mkDatatypeSorts(Arrays.asList(udecls), unresSorts));
+ slv.close();
/* Note: More tests are in datatype_api_black. */
}
assertThrows(CVC5ApiException.class, () -> slv.mkFunctionSort(sorts1, slv.getIntegerSort()));
assertThrows(
CVC5ApiException.class, () -> slv.mkFunctionSort(sorts2, d_solver.getIntegerSort()));
+ slv.close();
}
@Test void mkParamSort() throws CVC5ApiException
Solver slv = new Solver();
assertThrows(
CVC5ApiException.class, () -> slv.mkPredicateSort(new Sort[] {d_solver.getIntegerSort()}));
+ slv.close();
}
@Test void mkRecordSort() throws CVC5ApiException
Solver slv = new Solver();
assertThrows(CVC5ApiException.class, () -> slv.mkRecordSort(fields));
+ slv.close();
}
@Test void mkSetSort() throws CVC5ApiException
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
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
() -> 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
Solver slv = new Solver();
assertThrows(
CVC5ApiException.class, () -> slv.mkTupleSort(new Sort[] {d_solver.getIntegerSort()}));
+ slv.close();
}
@Test void mkBitVector() throws CVC5ApiException
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
Solver slv = new Solver();
assertThrows(CVC5ApiException.class, () -> slv.mkFloatingPoint(3, 5, t1));
+ slv.close();
}
@Test void mkCardinalityConstraint() throws CVC5ApiException
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
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
assertThrows(CVC5ApiException.class, () -> d_solver.mkEmptyBag(d_solver.getBooleanSort()));
assertThrows(CVC5ApiException.class, () -> slv.mkEmptyBag(s));
+ slv.close();
}
@Test void mkEmptySequence() throws CVC5ApiException
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
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()
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
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()
()
-> slv.mkTuple(new Sort[] {slv.mkBitVectorSort(3)},
new Term[] {d_solver.mkBitVector(3, "101", 2)}));
+ slv.close();
}
@Test void mkUniverseSet()
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()
Solver slv = new Solver();
assertThrows(CVC5ApiException.class, () -> slv.mkConst(boolSort));
+ slv.close();
}
@Test void mkConstArray()
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()
Solver slv = new Solver();
assertThrows(CVC5ApiException.class, () -> slv.declareDatatype(("a"), ctors1));
+ slv.close();
}
@Test void declareFun() throws CVC5ApiException
Solver slv = new Solver();
assertThrows(CVC5ApiException.class, () -> slv.declareFun("f1", new Sort[] {}, bvSort));
+ slv.close();
}
@Test void declareSort()
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));
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()
assertThrows(
CVC5ApiException.class, () -> slv.defineFunRec("ff", new Term[] {b12, b22}, bvSort2, v1));
+ slv.close();
}
@Test void defineFunRecWrongLogic() throws CVC5ApiException
()
-> slv.defineFunsRec(
new Term[] {f12, f22}, new Term[][] {{b12, b112}, {b42}}, new Term[] {v12, v2}));
+ slv.close();
}
@Test void defineFunsRecWrongLogic() throws CVC5ApiException
Solver slv = new Solver();
assertThrows(CVC5ApiException.class, () -> slv.getValue(x));
+ slv.close();
}
@Test void getModelDomainElements()
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()
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
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
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()
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()
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()
assertDoesNotThrow(() -> d_solver.checkEntailed(z));
Solver slv = new Solver();
assertThrows(CVC5ApiException.class, () -> slv.checkEntailed(d_solver.mkTrue()));
+ slv.close();
}
@Test void checkEntailed2()
Solver slv = new Solver();
assertThrows(CVC5ApiException.class, () -> slv.checkEntailed(d_solver.mkTrue()));
+ slv.close();
}
@Test void checkSat() throws CVC5ApiException
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
assertDoesNotThrow(() -> d_solver.checkSatAssuming(z));
Solver slv = new Solver();
assertThrows(CVC5ApiException.class, () -> slv.checkSatAssuming(d_solver.mkTrue()));
+ slv.close();
}
@Test void checkSatAssuming2() throws CVC5ApiException
Solver slv = new Solver();
assertThrows(CVC5ApiException.class, () -> slv.checkSatAssuming(d_solver.mkTrue()));
+ slv.close();
}
@Test void setLogic() throws CVC5ApiException
Solver slv = new Solver();
assertThrows(CVC5ApiException.class, () -> slv.mkSygusVar(boolSort));
+ slv.close();
}
@Test void mkSygusGrammar() throws CVC5ApiException
() -> 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
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
Solver slv = new Solver();
assertThrows(CVC5ApiException.class, () -> slv.addSygusConstraint(boolTerm));
+ slv.close();
}
@Test void addSygusAssume()
Solver slv = new Solver();
assertThrows(CVC5ApiException.class, () -> slv.addSygusAssume(boolTerm));
+ slv.close();
}
@Test void addSygusInvConstraint() throws CVC5ApiException
CVC5ApiException.class, () -> slv.addSygusInvConstraint(inv22, pre22, trans, post22));
assertThrows(
CVC5ApiException.class, () -> slv.addSygusInvConstraint(inv22, pre22, trans22, post));
+ slv.close();
}
@Test void getSynthSolution() throws CVC5ApiException
Solver slv = new Solver();
assertThrows(CVC5ApiException.class, () -> slv.getSynthSolution(f));
+ slv.close();
}
@Test void getSynthSolutions() throws CVC5ApiException
Solver slv = new Solver();
assertThrows(CVC5ApiException.class, () -> slv.getSynthSolutions(new Term[] {x}));
+ slv.close();
}
@Test void tupleProject() throws CVC5ApiException
d_solver = new Solver();
}
+ @AfterEach void tearDown()
+ {
+ d_solver.close();
+ }
+
Sort create_datatype_sort() throws CVC5ApiException
{
DatatypeDecl dtypeSpec = d_solver.mkDatatypeDecl("list");
d_solver = new Solver();
}
+ @AfterEach void tearDown()
+ {
+ d_solver.close();
+ }
+
@Test void eq()
{
Sort uSort = d_solver.mkUninterpretedSort("u");
projects / cvc5.git / commitdiff