From 4a58ed7daf86dd0b9cd1dabc9d83458da1fb23ae Mon Sep 17 00:00:00 2001 From: Mathias Preiner Date: Mon, 21 Mar 2022 17:22:41 -0700 Subject: [PATCH] api: Unify mkTerm variants. (#8357) --- examples/api/cpp/bitvectors.cpp | 30 +- examples/api/cpp/bitvectors_and_arrays.cpp | 19 +- examples/api/cpp/combination.cpp | 29 +- examples/api/cpp/datatypes.cpp | 25 +- examples/api/cpp/extract.cpp | 12 +- examples/api/cpp/floating_point_arith.cpp | 22 +- examples/api/cpp/linear_arith.cpp | 17 +- examples/api/cpp/quickstart.cpp | 20 +- examples/api/cpp/relations.cpp | 51 ++- examples/api/cpp/sequences.cpp | 12 +- examples/api/cpp/sets.cpp | 28 +- examples/api/cpp/strings.cpp | 39 +- examples/api/cpp/sygus-fun.cpp | 28 +- examples/api/cpp/sygus-grammar.cpp | 15 +- examples/api/cpp/sygus-inv.cpp | 12 +- examples/api/cpp/transcendentals.cpp | 12 +- examples/simple_vc_cxx.cpp | 14 +- examples/simple_vc_quant_cxx.cpp | 20 +- src/api/cpp/cvc5.cpp | 108 ----- src/api/cpp/cvc5.h | 85 +--- src/api/java/jni/solver.cpp | 13 +- src/parser/parser.cpp | 4 +- src/parser/smt2/Smt2.g | 4 +- src/parser/smt2/smt2.cpp | 12 +- src/parser/tptp/Tptp.g | 6 +- src/parser/tptp/tptp.cpp | 12 +- src/smt/command.cpp | 8 +- test/api/cpp/issue4889.cpp | 6 +- test/api/cpp/issue5074.cpp | 4 +- test/api/cpp/issue6111.cpp | 6 +- test/api/cpp/proj-issue306.cpp | 6 +- test/api/cpp/proj-issue334.cpp | 6 +- test/api/cpp/reset_assertions.cpp | 6 +- test/api/cpp/sep_log_api.cpp | 14 +- test/unit/api/cpp/solver_black.cpp | 428 +++++++++--------- test/unit/api/cpp/solver_white.cpp | 8 +- test/unit/api/cpp/term_black.cpp | 142 +++--- test/unit/api/cpp/term_white.cpp | 16 +- test/unit/api/cpp/theory_uf_ho_black.cpp | 8 +- .../theory/theory_sets_type_rules_white.cpp | 8 +- 40 files changed, 571 insertions(+), 744 deletions(-) diff --git a/examples/api/cpp/bitvectors.cpp b/examples/api/cpp/bitvectors.cpp index 3aa9ca8ad..999d89d7f 100644 --- a/examples/api/cpp/bitvectors.cpp +++ b/examples/api/cpp/bitvectors.cpp @@ -55,9 +55,9 @@ int main() Term b = slv.mkConst(bitvector32, "b"); // First encode the assumption that x must be equal to a or b - Term x_eq_a = slv.mkTerm(EQUAL, x, a); - Term x_eq_b = slv.mkTerm(EQUAL, x, b); - Term assumption = slv.mkTerm(OR, x_eq_a, x_eq_b); + Term x_eq_a = slv.mkTerm(EQUAL, {x, a}); + Term x_eq_b = slv.mkTerm(EQUAL, {x, b}); + Term assumption = slv.mkTerm(OR, {x_eq_a, x_eq_b}); // Assert the assumption slv.assertFormula(assumption); @@ -69,8 +69,8 @@ int main() // Encoding code (0) // new_x = x == a ? b : a; - Term ite = slv.mkTerm(ITE, x_eq_a, b, a); - Term assignment0 = slv.mkTerm(EQUAL, new_x, ite); + Term ite = slv.mkTerm(ITE, {x_eq_a, b, a}); + Term assignment0 = slv.mkTerm(EQUAL, {new_x, ite}); // Assert the encoding of code (0) cout << "Asserting " << assignment0 << " to cvc5 " << endl; @@ -80,13 +80,13 @@ int main() // Encoding code (1) // new_x_ = a xor b xor x - Term a_xor_b_xor_x = slv.mkTerm(BITVECTOR_XOR, a, b, x); - Term assignment1 = slv.mkTerm(EQUAL, new_x_, a_xor_b_xor_x); + Term a_xor_b_xor_x = slv.mkTerm(BITVECTOR_XOR, {a, b, x}); + Term assignment1 = slv.mkTerm(EQUAL, {new_x_, a_xor_b_xor_x}); // Assert encoding to cvc5 in current context; cout << "Asserting " << assignment1 << " to cvc5 " << endl; slv.assertFormula(assignment1); - Term new_x_eq_new_x_ = slv.mkTerm(EQUAL, new_x, new_x_); + Term new_x_eq_new_x_ = slv.mkTerm(EQUAL, {new_x, new_x_}); cout << " Check sat assuming: " << new_x_eq_new_x_.notTerm() << endl; cout << " Expect UNSAT. " << endl; @@ -96,9 +96,9 @@ int main() // Encoding code (2) // new_x_ = a + b - x - Term a_plus_b = slv.mkTerm(BITVECTOR_ADD, a, b); - Term a_plus_b_minus_x = slv.mkTerm(BITVECTOR_SUB, a_plus_b, x); - Term assignment2 = slv.mkTerm(EQUAL, new_x_, a_plus_b_minus_x); + Term a_plus_b = slv.mkTerm(BITVECTOR_ADD, {a, b}); + Term a_plus_b_minus_x = slv.mkTerm(BITVECTOR_SUB, {a_plus_b, x}); + Term assignment2 = slv.mkTerm(EQUAL, {new_x_, a_plus_b_minus_x}); // Assert encoding to cvc5 in current context; cout << "Asserting " << assignment2 << " to cvc5 " << endl; @@ -108,18 +108,18 @@ int main() cout << " Expect UNSAT. " << endl; cout << " cvc5: " << slv.checkSatAssuming(new_x_eq_new_x_.notTerm()) << endl; - Term x_neq_x = slv.mkTerm(EQUAL, x, x).notTerm(); + Term x_neq_x = slv.mkTerm(EQUAL, {x, x}).notTerm(); std::vector v{new_x_eq_new_x_, x_neq_x}; - Term query = slv.mkTerm(AND, v); + Term query = slv.mkTerm(AND, {v}); cout << " Check sat assuming: " << query.notTerm() << endl; cout << " Expect SAT. " << endl; cout << " cvc5: " << slv.checkSatAssuming(query.notTerm()) << endl; // Assert that a is odd Op extract_op = slv.mkOp(BITVECTOR_EXTRACT, 0, 0); - Term lsb_of_a = slv.mkTerm(extract_op, a); + Term lsb_of_a = slv.mkTerm(extract_op, {a}); cout << "Sort of " << lsb_of_a << " is " << lsb_of_a.getSort() << endl; - Term a_odd = slv.mkTerm(EQUAL, lsb_of_a, slv.mkBitVector(1u, 1u)); + Term a_odd = slv.mkTerm(EQUAL, {lsb_of_a, slv.mkBitVector(1u, 1u)}); cout << "Assert " << a_odd << endl; cout << "Check satisfiability." << endl; slv.assertFormula(a_odd); diff --git a/examples/api/cpp/bitvectors_and_arrays.cpp b/examples/api/cpp/bitvectors_and_arrays.cpp index 6b58daf1b..5e8d589c0 100644 --- a/examples/api/cpp/bitvectors_and_arrays.cpp +++ b/examples/api/cpp/bitvectors_and_arrays.cpp @@ -59,30 +59,31 @@ int main() Term zero = slv.mkBitVector(index_size, 0u); // Asserting that current_array[0] > 0 - Term current_array0 = slv.mkTerm(SELECT, current_array, zero); - Term current_array0_gt_0 = slv.mkTerm( - BITVECTOR_SGT, current_array0, slv.mkBitVector(32, 0u)); + Term current_array0 = slv.mkTerm(SELECT, {current_array, zero}); + Term current_array0_gt_0 = + slv.mkTerm(BITVECTOR_SGT, {current_array0, slv.mkBitVector(32, 0u)}); slv.assertFormula(current_array0_gt_0); // Building the assertions in the loop unrolling Term index = slv.mkBitVector(index_size, 0u); - Term old_current = slv.mkTerm(SELECT, current_array, index); + Term old_current = slv.mkTerm(SELECT, {current_array, index}); Term two = slv.mkBitVector(32, 2u); std::vector assertions; for (unsigned i = 1; i < k; ++i) { index = slv.mkBitVector(index_size, i); - Term new_current = slv.mkTerm(BITVECTOR_MULT, two, old_current); + Term new_current = slv.mkTerm(BITVECTOR_MULT, {two, old_current}); // current[i] = 2 * current[i-1] - current_array = slv.mkTerm(STORE, current_array, index, new_current); + current_array = slv.mkTerm(STORE, {current_array, index, new_current}); // current[i-1] < current [i] - Term current_slt_new_current = slv.mkTerm(BITVECTOR_SLT, old_current, new_current); + Term current_slt_new_current = + slv.mkTerm(BITVECTOR_SLT, {old_current, new_current}); assertions.push_back(current_slt_new_current); - old_current = slv.mkTerm(SELECT, current_array, index); + old_current = slv.mkTerm(SELECT, {current_array, index}); } - Term query = slv.mkTerm(NOT, slv.mkTerm(AND, assertions)); + Term query = slv.mkTerm(NOT, {slv.mkTerm(AND, assertions)}); cout << "Asserting " << query << " to cvc5 " << endl; slv.assertFormula(query); diff --git a/examples/api/cpp/combination.cpp b/examples/api/cpp/combination.cpp index c3847e51e..d5d031f5c 100644 --- a/examples/api/cpp/combination.cpp +++ b/examples/api/cpp/combination.cpp @@ -62,28 +62,29 @@ int main() Term one = slv.mkInteger(1); // Terms - Term f_x = slv.mkTerm(APPLY_UF, f, x); - Term f_y = slv.mkTerm(APPLY_UF, f, y); - Term sum = slv.mkTerm(ADD, f_x, f_y); - Term p_0 = slv.mkTerm(APPLY_UF, p, zero); - Term p_f_y = slv.mkTerm(APPLY_UF, p, f_y); + Term f_x = slv.mkTerm(APPLY_UF, {f, x}); + Term f_y = slv.mkTerm(APPLY_UF, {f, y}); + Term sum = slv.mkTerm(ADD, {f_x, f_y}); + Term p_0 = slv.mkTerm(APPLY_UF, {p, zero}); + Term p_f_y = slv.mkTerm(APPLY_UF, {p, f_y}); // Construct the assertions - Term assertions = slv.mkTerm(AND, - vector{ - slv.mkTerm(LEQ, zero, f_x), // 0 <= f(x) - slv.mkTerm(LEQ, zero, f_y), // 0 <= f(y) - slv.mkTerm(LEQ, sum, one), // f(x) + f(y) <= 1 - p_0.notTerm(), // not p(0) - p_f_y // p(f(y)) - }); + Term assertions = + slv.mkTerm(AND, + { + slv.mkTerm(LEQ, {zero, f_x}), // 0 <= f(x) + slv.mkTerm(LEQ, {zero, f_y}), // 0 <= f(y) + slv.mkTerm(LEQ, {sum, one}), // f(x) + f(y) <= 1 + p_0.notTerm(), // not p(0) + p_f_y // p(f(y)) + }); slv.assertFormula(assertions); cout << "Given the following assertions:" << endl << assertions << endl << endl; cout << "Prove x /= y is entailed. " << endl - << "cvc5: " << slv.checkSatAssuming(slv.mkTerm(EQUAL, x, y)) << "." + << "cvc5: " << slv.checkSatAssuming(slv.mkTerm(EQUAL, {x, y})) << "." << endl << endl; diff --git a/examples/api/cpp/datatypes.cpp b/examples/api/cpp/datatypes.cpp index 7c0b03b05..2e2bb842e 100644 --- a/examples/api/cpp/datatypes.cpp +++ b/examples/api/cpp/datatypes.cpp @@ -37,9 +37,9 @@ void test(Solver& slv, Sort& consListSort) // APPLY_CONSTRUCTOR, even though it has no arguments. Term t = slv.mkTerm( APPLY_CONSTRUCTOR, - consList.getConstructorTerm("cons"), - slv.mkInteger(0), - slv.mkTerm(APPLY_CONSTRUCTOR, consList.getConstructorTerm("nil"))); + {consList.getConstructorTerm("cons"), + slv.mkInteger(0), + slv.mkTerm(APPLY_CONSTRUCTOR, {consList.getConstructorTerm("nil")})}); std::cout << "t is " << t << std::endl << "sort of cons is " @@ -53,7 +53,7 @@ void test(Solver& slv, Sort& consListSort) // consList["cons"]) in order to get the "head" selector symbol // to apply. Term t2 = - slv.mkTerm(APPLY_SELECTOR, consList["cons"].getSelectorTerm("head"), t); + slv.mkTerm(APPLY_SELECTOR, {consList["cons"].getSelectorTerm("head"), t}); std::cout << "t2 is " << t2 << std::endl << "simplify(t2) is " << slv.simplify(t2) << std::endl @@ -85,16 +85,15 @@ void test(Solver& slv, Sort& consListSort) // You can also define a tester term for constructor 'cons': (_ is cons) Term t_is_cons = - slv.mkTerm(APPLY_TESTER, consList["cons"].getTesterTerm(), t); + slv.mkTerm(APPLY_TESTER, {consList["cons"].getTesterTerm(), t}); std::cout << "t_is_cons is " << t_is_cons << std::endl << std::endl; slv.assertFormula(t_is_cons); // Updating t at 'head' with value 1 is defined as follows: - Term t_updated = slv.mkTerm(APPLY_UPDATER, - consList["cons"]["head"].getUpdaterTerm(), - t, - slv.mkInteger(1)); + Term t_updated = slv.mkTerm( + APPLY_UPDATER, + {consList["cons"]["head"].getUpdaterTerm(), t, slv.mkInteger(1)}); std::cout << "t_updated is " << t_updated << std::endl << std::endl; - slv.assertFormula(slv.mkTerm(DISTINCT, t, t_updated)); + slv.assertFormula(slv.mkTerm(DISTINCT, {t, t_updated})); // You can also define parameterized datatypes. // This example builds a simple parameterized list of sort T, with one @@ -129,15 +128,15 @@ void test(Solver& slv, Sort& consListSort) Term a = slv.mkConst(paramConsIntListSort, "a"); std::cout << "term " << a << " is of sort " << a.getSort() << std::endl; - Term head_a = slv.mkTerm( - APPLY_SELECTOR, paramConsList["cons"].getSelectorTerm("head"), a); + Term head_a = slv.mkTerm(APPLY_SELECTOR, + {paramConsList["cons"].getSelectorTerm("head"), a}); std::cout << "head_a is " << head_a << " of sort " << head_a.getSort() << std::endl << "sort of cons is " << paramConsList.getConstructorTerm("cons").getSort() << std::endl << std::endl; - Term assertion = slv.mkTerm(GT, head_a, slv.mkInteger(50)); + Term assertion = slv.mkTerm(GT, {head_a, slv.mkInteger(50)}); std::cout << "Assert " << assertion << std::endl; slv.assertFormula(assertion); std::cout << "Expect sat." << std::endl; diff --git a/examples/api/cpp/extract.cpp b/examples/api/cpp/extract.cpp index 9b036caa4..87e91e0b5 100644 --- a/examples/api/cpp/extract.cpp +++ b/examples/api/cpp/extract.cpp @@ -32,22 +32,22 @@ int main() Term x = slv.mkConst(bitvector32, "a"); Op ext_31_1 = slv.mkOp(BITVECTOR_EXTRACT, 31, 1); - Term x_31_1 = slv.mkTerm(ext_31_1, x); + Term x_31_1 = slv.mkTerm(ext_31_1, {x}); Op ext_30_0 = slv.mkOp(BITVECTOR_EXTRACT, 30, 0); - Term x_30_0 = slv.mkTerm(ext_30_0, x); + Term x_30_0 = slv.mkTerm(ext_30_0, {x}); Op ext_31_31 = slv.mkOp(BITVECTOR_EXTRACT, 31, 31); - Term x_31_31 = slv.mkTerm(ext_31_31, x); + Term x_31_31 = slv.mkTerm(ext_31_31, {x}); Op ext_0_0 = slv.mkOp(BITVECTOR_EXTRACT, 0, 0); - Term x_0_0 = slv.mkTerm(ext_0_0, x); + Term x_0_0 = slv.mkTerm(ext_0_0, {x}); - Term eq = slv.mkTerm(EQUAL, x_31_1, x_30_0); + Term eq = slv.mkTerm(EQUAL, {x_31_1, x_30_0}); cout << " Asserting: " << eq << endl; slv.assertFormula(eq); - Term eq2 = slv.mkTerm(EQUAL, x_31_31, x_0_0); + Term eq2 = slv.mkTerm(EQUAL, {x_31_31, x_0_0}); cout << " Check sat assuming: " << eq2.notTerm() << endl; cout << " Expect UNSAT. " << endl; cout << " cvc5: " << slv.checkSatAssuming(eq2.notTerm()) << endl; diff --git a/examples/api/cpp/floating_point_arith.cpp b/examples/api/cpp/floating_point_arith.cpp index 4e44965d1..6233102cb 100644 --- a/examples/api/cpp/floating_point_arith.cpp +++ b/examples/api/cpp/floating_point_arith.cpp @@ -43,10 +43,10 @@ int main() // (a + (b + c)) != ((a + b) + c) Term rm = solver.mkRoundingMode(ROUND_NEAREST_TIES_TO_EVEN); Term lhs = solver.mkTerm( - FLOATINGPOINT_ADD, rm, a, solver.mkTerm(FLOATINGPOINT_ADD, rm, b, c)); + FLOATINGPOINT_ADD, {rm, a, solver.mkTerm(FLOATINGPOINT_ADD, {rm, b, c})}); Term rhs = solver.mkTerm( - FLOATINGPOINT_ADD, rm, solver.mkTerm(FLOATINGPOINT_ADD, rm, a, b), c); - solver.assertFormula(solver.mkTerm(NOT, solver.mkTerm(EQUAL, a, b))); + FLOATINGPOINT_ADD, {rm, solver.mkTerm(FLOATINGPOINT_ADD, {rm, a, b}), c}); + solver.assertFormula(solver.mkTerm(NOT, {solver.mkTerm(EQUAL, {a, b})})); Result r = solver.checkSat(); // result is sat assert (r.isSat()); @@ -59,7 +59,7 @@ int main() Term nan = solver.mkFloatingPointNaN(8, 24); Term inf = solver.mkFloatingPointPosInf(8, 24); solver.assertFormula(solver.mkTerm( - OR, solver.mkTerm(EQUAL, a, inf), solver.mkTerm(EQUAL, a, nan))); + OR, {solver.mkTerm(EQUAL, {a, inf}), solver.mkTerm(EQUAL, {a, nan})})); r = solver.checkSat(); // result is sat assert (r.isSat()); @@ -74,17 +74,17 @@ int main() Term rtp = solver.mkRoundingMode(ROUND_TOWARD_POSITIVE); Term rtn = solver.mkRoundingMode(ROUND_TOWARD_NEGATIVE); Op op = solver.mkOp(FLOATINGPOINT_TO_SBV, 16); // (_ fp.to_sbv 16) - lhs = solver.mkTerm(op, rtp, d); - rhs = solver.mkTerm(op, rtn, d); - solver.assertFormula(solver.mkTerm(FLOATINGPOINT_IS_NORMAL, d)); - solver.assertFormula(solver.mkTerm(NOT, solver.mkTerm(EQUAL, lhs, rhs))); + lhs = solver.mkTerm(op, {rtp, d}); + rhs = solver.mkTerm(op, {rtn, d}); + solver.assertFormula(solver.mkTerm(FLOATINGPOINT_IS_NORMAL, {d})); + solver.assertFormula(solver.mkTerm(NOT, {solver.mkTerm(EQUAL, {lhs, rhs})})); r = solver.checkSat(); // result is sat assert (r.isSat()); // Convert the result to a rational and print it Term val = solver.getValue(d); - Term realVal = solver.getValue(solver.mkTerm(FLOATINGPOINT_TO_REAL, val)); + Term realVal = solver.getValue(solver.mkTerm(FLOATINGPOINT_TO_REAL, {val})); cout << "d = " << val << " = " << realVal << endl; cout << "((_ fp.to_sbv 16) RTP d) = " << solver.getValue(lhs) << endl; cout << "((_ fp.to_sbv 16) RTN d) = " << solver.getValue(rhs) << endl; @@ -95,8 +95,8 @@ int main() Term smallest = solver.mkFloatingPoint(8, 24, solver.mkBitVector(32, 0b001)); solver.assertFormula( solver.mkTerm(AND, - solver.mkTerm(FLOATINGPOINT_LT, zero, e), - solver.mkTerm(FLOATINGPOINT_LT, e, smallest))); + {solver.mkTerm(FLOATINGPOINT_LT, {zero, e}), + solver.mkTerm(FLOATINGPOINT_LT, {e, smallest})})); r = solver.checkSat(); // result is unsat assert (!r.isSat()); diff --git a/examples/api/cpp/linear_arith.cpp b/examples/api/cpp/linear_arith.cpp index 3a8879813..a02484534 100644 --- a/examples/api/cpp/linear_arith.cpp +++ b/examples/api/cpp/linear_arith.cpp @@ -43,23 +43,22 @@ int main() Term two_thirds = slv.mkReal(2, 3); // Terms - Term three_y = slv.mkTerm(MULT, three, y); - Term diff = slv.mkTerm(SUB, y, x); + Term three_y = slv.mkTerm(MULT, {three, y}); + Term diff = slv.mkTerm(SUB, {y, x}); // Formulas - Term x_geq_3y = slv.mkTerm(GEQ, x, three_y); - Term x_leq_y = slv.mkTerm(LEQ, x, y); - Term neg2_lt_x = slv.mkTerm(LT, neg2, x); + Term x_geq_3y = slv.mkTerm(GEQ, {x, three_y}); + Term x_leq_y = slv.mkTerm(LEQ, {x, y}); + Term neg2_lt_x = slv.mkTerm(LT, {neg2, x}); - Term assertions = - slv.mkTerm(AND, x_geq_3y, x_leq_y, neg2_lt_x); + Term assertions = slv.mkTerm(AND, {x_geq_3y, x_leq_y, neg2_lt_x}); cout << "Given the assertions " << assertions << endl; slv.assertFormula(assertions); slv.push(); - Term diff_leq_two_thirds = slv.mkTerm(LEQ, diff, two_thirds); + Term diff_leq_two_thirds = slv.mkTerm(LEQ, {diff, two_thirds}); cout << "Prove that " << diff_leq_two_thirds << " with cvc5." << endl; cout << "cvc5 should report UNSAT." << endl; cout << "Result from cvc5 is: " @@ -69,7 +68,7 @@ int main() cout << endl; slv.push(); - Term diff_is_two_thirds = slv.mkTerm(EQUAL, diff, two_thirds); + Term diff_is_two_thirds = slv.mkTerm(EQUAL, {diff, two_thirds}); slv.assertFormula(diff_is_two_thirds); cout << "Show that the assertions are consistent with " << endl; cout << diff_is_two_thirds << " with cvc5." << endl; diff --git a/examples/api/cpp/quickstart.cpp b/examples/api/cpp/quickstart.cpp index 35d9971cf..309459f73 100644 --- a/examples/api/cpp/quickstart.cpp +++ b/examples/api/cpp/quickstart.cpp @@ -69,17 +69,17 @@ int main() Term one = solver.mkReal(1); // Next, we construct the term x + y - Term xPlusY = solver.mkTerm(ADD, x, y); + Term xPlusY = solver.mkTerm(ADD, {x, y}); // Now we can define the constraints. // They use the operators +, <=, and <. // In the API, these are denoted by ADD, LEQ, and LT. // A list of available operators is available in: // src/api/cpp/cvc5_kind.h - Term constraint1 = solver.mkTerm(LT, zero, x); - Term constraint2 = solver.mkTerm(LT, zero, y); - Term constraint3 = solver.mkTerm(LT, xPlusY, one); - Term constraint4 = solver.mkTerm(LEQ, x, y); + Term constraint1 = solver.mkTerm(LT, {zero, x}); + Term constraint2 = solver.mkTerm(LT, {zero, y}); + Term constraint3 = solver.mkTerm(LT, {xPlusY, one}); + Term constraint4 = solver.mkTerm(LEQ, {x, y}); // Now we assert the constraints to the solver. solver.assertFormula(constraint1); @@ -102,7 +102,7 @@ int main() // It is also possible to get values for compound terms, // even if those did not appear in the original formula. - Term xMinusY = solver.mkTerm(SUB, x, y); + Term xMinusY = solver.mkTerm(SUB, {x, y}); Term xMinusYVal = solver.getValue(xMinusY); // We can now obtain the string representations of the values. @@ -151,11 +151,11 @@ int main() // 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(LT, solver.mkInteger(0), a)); - solver.assertFormula(solver.mkTerm(LT, solver.mkInteger(0), b)); + solver.assertFormula(solver.mkTerm(LT, {solver.mkInteger(0), a})); + solver.assertFormula(solver.mkTerm(LT, {solver.mkInteger(0), b})); solver.assertFormula( - solver.mkTerm(LT, solver.mkTerm(ADD, a, b), solver.mkInteger(1))); - solver.assertFormula(solver.mkTerm(LEQ, a, b)); + solver.mkTerm(LT, {solver.mkTerm(ADD, {a, b}), solver.mkInteger(1)})); + solver.assertFormula(solver.mkTerm(LEQ, {a, b})); // We check whether the revised assertion is satisfiable. Result r2 = solver.checkSat(); diff --git a/examples/api/cpp/relations.cpp b/examples/api/cpp/relations.cpp index cf462bd4a..d19e91cea 100644 --- a/examples/api/cpp/relations.cpp +++ b/examples/api/cpp/relations.cpp @@ -66,59 +66,60 @@ int main() 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); + Term isEmpty1 = solver.mkTerm(EQUAL, {males, emptySetTerm}); + Term isEmpty2 = solver.mkTerm(EQUAL, {females, emptySetTerm}); // (assert (= people (as set.universe (Set (Tuple Person))))) - Term peopleAreTheUniverse = solver.mkTerm(EQUAL, people, universeSet); + Term peopleAreTheUniverse = solver.mkTerm(EQUAL, {people, universeSet}); // (assert (not (= males (as set.empty (Set (Tuple Person)))))) - Term maleSetIsNotEmpty = solver.mkTerm(NOT, isEmpty1); + Term maleSetIsNotEmpty = solver.mkTerm(NOT, {isEmpty1}); // (assert (not (= females (as set.empty (Set (Tuple Person)))))) - Term femaleSetIsNotEmpty = solver.mkTerm(NOT, isEmpty2); + Term femaleSetIsNotEmpty = solver.mkTerm(NOT, {isEmpty2}); // (assert (= (set.inter males females) // (as set.empty (Set (Tuple Person))))) - Term malesFemalesIntersection = solver.mkTerm(SET_INTER, males, females); + Term malesFemalesIntersection = solver.mkTerm(SET_INTER, {males, females}); Term malesAndFemalesAreDisjoint = - solver.mkTerm(EQUAL, malesFemalesIntersection, emptySetTerm); + solver.mkTerm(EQUAL, {malesFemalesIntersection, emptySetTerm}); // (assert (not (= father (as set.empty (Set (Tuple Person Person)))))) // (assert (not (= mother (as set.empty (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); + 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 (set.subset (rel.join father people) males)) - Term fathers = solver.mkTerm(RELATION_JOIN, father, people); - Term fathersAreMales = solver.mkTerm(SET_SUBSET, fathers, males); + Term fathers = solver.mkTerm(RELATION_JOIN, {father, people}); + Term fathersAreMales = solver.mkTerm(SET_SUBSET, {fathers, males}); // mothers are females // (assert (set.subset (rel.join mother people) females)) - Term mothers = solver.mkTerm(RELATION_JOIN, mother, people); - Term mothersAreFemales = solver.mkTerm(SET_SUBSET, mothers, females); + Term mothers = solver.mkTerm(RELATION_JOIN, {mother, people}); + Term mothersAreFemales = solver.mkTerm(SET_SUBSET, {mothers, females}); // (assert (= parent (set.union father mother))) - Term unionFatherMother = solver.mkTerm(SET_UNION, father, mother); - Term parentIsFatherOrMother = solver.mkTerm(EQUAL, parent, unionFatherMother); + Term unionFatherMother = solver.mkTerm(SET_UNION, {father, mother}); + Term parentIsFatherOrMother = + solver.mkTerm(EQUAL, {parent, unionFatherMother}); // (assert (= ancestor (rel.tclosure parent))) - Term transitiveClosure = solver.mkTerm(RELATION_TCLOSURE, parent); - Term ancestorFormula = solver.mkTerm(EQUAL, ancestor, transitiveClosure); + Term transitiveClosure = solver.mkTerm(RELATION_TCLOSURE, {parent}); + Term ancestorFormula = solver.mkTerm(EQUAL, {ancestor, transitiveClosure}); // (assert (= descendant (rel.transpose descendant))) - Term transpose = solver.mkTerm(RELATION_TRANSPOSE, ancestor); - Term descendantFormula = solver.mkTerm(EQUAL, descendant, transpose); + Term transpose = solver.mkTerm(RELATION_TRANSPOSE, {ancestor}); + Term descendantFormula = solver.mkTerm(EQUAL, {descendant, transpose}); // (assert (forall ((x Person)) (not (set.member (tuple x x) ancestor)))) Term x = solver.mkVar(personSort, "x"); Term xxTuple = solver.mkTuple({personSort, personSort}, {x, x}); - Term member = solver.mkTerm(SET_MEMBER, xxTuple, ancestor); - Term notMember = solver.mkTerm(NOT, member); + Term member = solver.mkTerm(SET_MEMBER, {xxTuple, ancestor}); + Term notMember = solver.mkTerm(NOT, {member}); - Term quantifiedVariables = solver.mkTerm(VARIABLE_LIST, x); - Term noSelfAncestor = solver.mkTerm(FORALL, quantifiedVariables, notMember); + Term quantifiedVariables = solver.mkTerm(VARIABLE_LIST, {x}); + Term noSelfAncestor = solver.mkTerm(FORALL, {quantifiedVariables, notMember}); // formulas solver.assertFormula(peopleAreTheUniverse); diff --git a/examples/api/cpp/sequences.cpp b/examples/api/cpp/sequences.cpp index 40cacf5c7..d9ba3c7b1 100644 --- a/examples/api/cpp/sequences.cpp +++ b/examples/api/cpp/sequences.cpp @@ -42,18 +42,18 @@ int main() // Empty sequence Term empty = slv.mkEmptySequence(slv.getIntegerSort()); // Sequence concatenation: x.y.empty - Term concat = slv.mkTerm(SEQ_CONCAT, 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); + Term concat_len = slv.mkTerm(SEQ_LENGTH, {concat}); // |x.y.empty| > 1 - Term formula1 = slv.mkTerm(GT, concat_len, slv.mkInteger(1)); + Term formula1 = slv.mkTerm(GT, {concat_len, slv.mkInteger(1)}); // Sequence unit: seq(1) - Term unit = slv.mkTerm(SEQ_UNIT, slv.mkInteger(1)); + Term unit = slv.mkTerm(SEQ_UNIT, {slv.mkInteger(1)}); // x = seq(1) - Term formula2 = slv.mkTerm(EQUAL, x, unit); + Term formula2 = slv.mkTerm(EQUAL, {x, unit}); // Make a query - Term q = slv.mkTerm(AND, formula1, formula2); + Term q = slv.mkTerm(AND, {formula1, formula2}); // check sat Result result = slv.checkSatAssuming(q); diff --git a/examples/api/cpp/sets.cpp b/examples/api/cpp/sets.cpp index 8cd643908..a517ba2e2 100644 --- a/examples/api/cpp/sets.cpp +++ b/examples/api/cpp/sets.cpp @@ -42,14 +42,14 @@ int main() Term B = slv.mkConst(set, "B"); Term C = slv.mkConst(set, "C"); - Term unionAB = slv.mkTerm(SET_UNION, A, B); - Term lhs = slv.mkTerm(SET_INTER, unionAB, C); + Term unionAB = slv.mkTerm(SET_UNION, {A, B}); + Term lhs = slv.mkTerm(SET_INTER, {unionAB, C}); - Term intersectionAC = slv.mkTerm(SET_INTER, A, C); - Term intersectionBC = slv.mkTerm(SET_INTER, B, C); - Term rhs = slv.mkTerm(SET_UNION, intersectionAC, intersectionBC); + Term intersectionAC = slv.mkTerm(SET_INTER, {A, C}); + Term intersectionBC = slv.mkTerm(SET_INTER, {B, C}); + Term rhs = slv.mkTerm(SET_UNION, {intersectionAC, intersectionBC}); - Term theorem = slv.mkTerm(EQUAL, lhs, rhs); + Term theorem = slv.mkTerm(EQUAL, {lhs, rhs}); cout << "cvc5 reports: " << theorem << " is " << slv.checkSatAssuming(theorem.notTerm()) << "." << endl; @@ -60,7 +60,7 @@ int main() Term A = slv.mkConst(set, "A"); Term emptyset = slv.mkEmptySet(set); - Term theorem = slv.mkTerm(SET_SUBSET, emptyset, A); + Term theorem = slv.mkTerm(SET_SUBSET, {emptyset, A}); cout << "cvc5 reports: " << theorem << " is " << slv.checkSatAssuming(theorem.notTerm()) << "." << endl; @@ -72,16 +72,16 @@ int main() Term two = slv.mkInteger(2); Term three = slv.mkInteger(3); - Term singleton_one = slv.mkTerm(SET_SINGLETON, one); - Term singleton_two = slv.mkTerm(SET_SINGLETON, two); - Term singleton_three = slv.mkTerm(SET_SINGLETON, three); - Term one_two = slv.mkTerm(SET_UNION, singleton_one, singleton_two); - Term two_three = slv.mkTerm(SET_UNION, singleton_two, singleton_three); - Term intersection = slv.mkTerm(SET_INTER, one_two, two_three); + Term singleton_one = slv.mkTerm(SET_SINGLETON, {one}); + Term singleton_two = slv.mkTerm(SET_SINGLETON, {two}); + Term singleton_three = slv.mkTerm(SET_SINGLETON, {three}); + Term one_two = slv.mkTerm(SET_UNION, {singleton_one, singleton_two}); + Term two_three = slv.mkTerm(SET_UNION, {singleton_two, singleton_three}); + Term intersection = slv.mkTerm(SET_INTER, {one_two, two_three}); Term x = slv.mkConst(integer, "x"); - Term e = slv.mkTerm(SET_MEMBER, x, intersection); + Term e = slv.mkTerm(SET_MEMBER, {x, intersection}); Result result = slv.checkSatAssuming(e); cout << "cvc5 reports: " << e << " is " << result << "." << endl; diff --git a/examples/api/cpp/strings.cpp b/examples/api/cpp/strings.cpp index 01e384ee7..7b374cebd 100644 --- a/examples/api/cpp/strings.cpp +++ b/examples/api/cpp/strings.cpp @@ -46,41 +46,42 @@ int main() Term z = slv.mkConst(string, "z"); // String concatenation: x.ab.y - Term lhs = slv.mkTerm(STRING_CONCAT, x, ab, y); + Term lhs = slv.mkTerm(STRING_CONCAT, {x, ab, y}); // String concatenation: abc.z - Term rhs = slv.mkTerm(STRING_CONCAT, abc, z); + Term rhs = slv.mkTerm(STRING_CONCAT, {abc, z}); // x.ab.y = abc.z - Term formula1 = slv.mkTerm(EQUAL, lhs, rhs); + Term formula1 = slv.mkTerm(EQUAL, {lhs, rhs}); // Length of y: |y| - Term leny = slv.mkTerm(STRING_LENGTH, y); + Term leny = slv.mkTerm(STRING_LENGTH, {y}); // |y| >= 0 - Term formula2 = slv.mkTerm(GEQ, leny, slv.mkInteger(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"))); + 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); + 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); + Term formula3 = slv.mkTerm(STRING_IN_REGEXP, {s, r}); // Make a query - Term q = slv.mkTerm(AND, - formula1, - formula2, - formula3); + Term q = slv.mkTerm(AND, {formula1, formula2, formula3}); // check sat Result result = slv.checkSatAssuming(q); diff --git a/examples/api/cpp/sygus-fun.cpp b/examples/api/cpp/sygus-fun.cpp index f778af95b..37a69fbdb 100644 --- a/examples/api/cpp/sygus-fun.cpp +++ b/examples/api/cpp/sygus-fun.cpp @@ -82,13 +82,13 @@ int main() Term zero = slv.mkInteger(0); Term one = slv.mkInteger(1); - Term plus = slv.mkTerm(ADD, start, start); - Term minus = slv.mkTerm(SUB, start, start); - Term ite = slv.mkTerm(ITE, start_bool, start, start); + Term plus = slv.mkTerm(ADD, {start, start}); + Term minus = slv.mkTerm(SUB, {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); + 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({x, y}, {start, start_bool}); @@ -106,25 +106,27 @@ int main() 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); + 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)); + slv.addSygusConstraint(slv.mkTerm(GEQ, {max_x_y, varX})); // (constraint (>= (max x y) y)) - slv.addSygusConstraint(slv.mkTerm(GEQ, max_x_y, varY)); + 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))); + 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(ADD, max_x_y, min_x_y), slv.mkTerm(ADD, varX, varY))); + EQUAL, + {slv.mkTerm(ADD, {max_x_y, min_x_y}), slv.mkTerm(ADD, {varX, varY})})); // print solutions if available if (slv.checkSynth().isUnsat()) diff --git a/examples/api/cpp/sygus-grammar.cpp b/examples/api/cpp/sygus-grammar.cpp index ed0282bb9..fc31a6a32 100644 --- a/examples/api/cpp/sygus-grammar.cpp +++ b/examples/api/cpp/sygus-grammar.cpp @@ -75,8 +75,8 @@ int main() // define the rules Term zero = slv.mkInteger(0); - Term neg_x = slv.mkTerm(NEG, x); - Term plus = slv.mkTerm(ADD, x, start); + Term neg_x = slv.mkTerm(NEG, {x}); + Term plus = slv.mkTerm(ADD, {x, start}); // create the grammar object Grammar g1 = slv.mkSygusGrammar({x}, {start}); @@ -105,14 +105,15 @@ int main() // 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, {id1_x, id2_x, id3_x, id4_x, varX})); + slv.addSygusConstraint( + slv.mkTerm(EQUAL, {{id1_x, id2_x, id3_x, id4_x, varX}})); // print solutions if available if (slv.checkSynth().isUnsat()) diff --git a/examples/api/cpp/sygus-inv.cpp b/examples/api/cpp/sygus-inv.cpp index 9c976beef..aaff3e695 100644 --- a/examples/api/cpp/sygus-inv.cpp +++ b/examples/api/cpp/sygus-inv.cpp @@ -68,14 +68,16 @@ int main() // (ite (< x 10) (= xp (+ x 1)) (= xp x)) Term ite = slv.mkTerm(ITE, - slv.mkTerm(LT, x, ten), - slv.mkTerm(EQUAL, xp, slv.mkTerm(ADD, x, one)), - slv.mkTerm(EQUAL, xp, x)); + {slv.mkTerm(LT, {x, ten}), + slv.mkTerm(EQUAL, {xp, slv.mkTerm(ADD, {x, one})}), + slv.mkTerm(EQUAL, {xp, x})}); // define the pre-conditions, transition relations, and post-conditions - Term pre_f = slv.defineFun("pre-f", {x}, boolean, slv.mkTerm(EQUAL, x, zero)); + Term pre_f = + slv.defineFun("pre-f", {x}, boolean, slv.mkTerm(EQUAL, {x, zero})); Term trans_f = slv.defineFun("trans-f", {x, xp}, boolean, ite); - Term post_f = slv.defineFun("post-f", {x}, boolean, slv.mkTerm(LEQ, x, ten)); + Term post_f = + slv.defineFun("post-f", {x}, boolean, slv.mkTerm(LEQ, {x, ten})); // declare the invariant-to-synthesize Term inv_f = slv.synthInv("inv-f", {x}); diff --git a/examples/api/cpp/transcendentals.cpp b/examples/api/cpp/transcendentals.cpp index a9a3ce681..2b530ae70 100644 --- a/examples/api/cpp/transcendentals.cpp +++ b/examples/api/cpp/transcendentals.cpp @@ -34,14 +34,14 @@ int main() // 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); + 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); + 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); diff --git a/examples/simple_vc_cxx.cpp b/examples/simple_vc_cxx.cpp index e440c09a0..ad2ad3690 100644 --- a/examples/simple_vc_cxx.cpp +++ b/examples/simple_vc_cxx.cpp @@ -34,18 +34,18 @@ int main() { Term y = slv.mkConst(integer, "y"); Term zero = slv.mkInteger(0); - Term x_positive = slv.mkTerm(Kind::GT, x, zero); - Term y_positive = slv.mkTerm(Kind::GT, y, zero); + Term x_positive = slv.mkTerm(Kind::GT, {x, zero}); + Term y_positive = slv.mkTerm(Kind::GT, {y, zero}); Term two = slv.mkInteger(2); - Term twox = slv.mkTerm(Kind::MULT, two, x); - Term twox_plus_y = slv.mkTerm(Kind::ADD, twox, y); + Term twox = slv.mkTerm(Kind::MULT, {two, x}); + Term twox_plus_y = slv.mkTerm(Kind::ADD, {twox, y}); Term three = slv.mkInteger(3); - Term twox_plus_y_geq_3 = slv.mkTerm(Kind::GEQ, twox_plus_y, three); + Term twox_plus_y_geq_3 = slv.mkTerm(Kind::GEQ, {twox_plus_y, three}); - Term formula = - slv.mkTerm(Kind::AND, x_positive, y_positive).impTerm(twox_plus_y_geq_3); + Term formula = slv.mkTerm(Kind::AND, {x_positive, y_positive}) + .impTerm(twox_plus_y_geq_3); std::cout << "Checking entailment of formula " << formula << " with cvc5." << std::endl; diff --git a/examples/simple_vc_quant_cxx.cpp b/examples/simple_vc_quant_cxx.cpp index ea8aa10a4..1b50a141f 100644 --- a/examples/simple_vc_quant_cxx.cpp +++ b/examples/simple_vc_quant_cxx.cpp @@ -33,18 +33,18 @@ int main() { Term x = slv.mkVar(integer, "x"); // make forall x. P( x ) - Term var_list = slv.mkTerm(Kind::VARIABLE_LIST, x); - Term px = slv.mkTerm(Kind::APPLY_UF, p, x); - Term quantpospx = slv.mkTerm(Kind::FORALL, var_list, px); + Term var_list = slv.mkTerm(Kind::VARIABLE_LIST, {x}); + Term px = slv.mkTerm(Kind::APPLY_UF, {p, x}); + Term quantpospx = slv.mkTerm(Kind::FORALL, {var_list, px}); std::cout << "Made expression : " << quantpospx << std::endl; //make ~P( 5 ) Term five = slv.mkInteger(5); - Term pfive = slv.mkTerm(Kind::APPLY_UF, p, five); - Term negpfive = slv.mkTerm(Kind::NOT, pfive); + Term pfive = slv.mkTerm(Kind::APPLY_UF, {p, five}); + Term negpfive = slv.mkTerm(Kind::NOT, {pfive}); std::cout << "Made expression : " << negpfive << std::endl; - Term formula = slv.mkTerm(Kind::AND, quantpospx, negpfive); + Term formula = slv.mkTerm(Kind::AND, {quantpospx, negpfive}); slv.assertFormula(formula); @@ -56,13 +56,13 @@ int main() { slv.resetAssertions(); // this version has a pattern e.g. in smt2 syntax (forall ((x Int)) (! (P x ) :pattern ((P x)))) - Term pattern = slv.mkTerm(Kind::INST_PATTERN, px); - Term pattern_list = slv.mkTerm(Kind::INST_PATTERN_LIST, pattern); + Term pattern = slv.mkTerm(Kind::INST_PATTERN, {px}); + Term pattern_list = slv.mkTerm(Kind::INST_PATTERN_LIST, {pattern}); Term quantpospx_pattern = - slv.mkTerm(Kind::FORALL, var_list, px, pattern_list); + slv.mkTerm(Kind::FORALL, {var_list, px, pattern_list}); std::cout << "Made expression : " << quantpospx_pattern << std::endl; - Term formula_pattern = slv.mkTerm(Kind::AND, quantpospx_pattern, negpfive); + Term formula_pattern = slv.mkTerm(Kind::AND, {quantpospx_pattern, negpfive}); slv.assertFormula(formula_pattern); diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp index 37cdd5619..b6e4ef187 100644 --- a/src/api/cpp/cvc5.cpp +++ b/src/api/cpp/cvc5.cpp @@ -6066,56 +6066,6 @@ DatatypeDecl Solver::mkDatatypeDecl(const std::string& name, /* Create terms */ /* -------------------------------------------------------------------------- */ -Term Solver::mkTerm(Kind kind) const -{ - CVC5_API_TRY_CATCH_BEGIN; - CVC5_API_KIND_CHECK(kind); - //////// all checks before this line - return mkTermFromKind(kind); - //////// - CVC5_API_TRY_CATCH_END; -} - -Term Solver::mkTerm(Kind kind, const Term& child) const -{ - CVC5_API_TRY_CATCH_BEGIN; - CVC5_API_KIND_CHECK(kind); - CVC5_API_SOLVER_CHECK_TERM(child); - //////// all checks before this line - return mkTermHelper(kind, std::vector{child}); - //////// - CVC5_API_TRY_CATCH_END; -} - -Term Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const -{ - CVC5_API_TRY_CATCH_BEGIN; - CVC5_API_KIND_CHECK(kind); - CVC5_API_SOLVER_CHECK_TERM(child1); - CVC5_API_SOLVER_CHECK_TERM(child2); - //////// all checks before this line - return mkTermHelper(kind, std::vector{child1, child2}); - //////// - CVC5_API_TRY_CATCH_END; -} - -Term Solver::mkTerm(Kind kind, - const Term& child1, - const Term& child2, - const Term& child3) const -{ - CVC5_API_TRY_CATCH_BEGIN; - CVC5_API_KIND_CHECK(kind); - CVC5_API_SOLVER_CHECK_TERM(child1); - CVC5_API_SOLVER_CHECK_TERM(child2); - CVC5_API_SOLVER_CHECK_TERM(child3); - //////// all checks before this line - // need to use internal term call to check e.g. associative construction - return mkTermHelper(kind, std::vector{child1, child2, child3}); - //////// - CVC5_API_TRY_CATCH_END; -} - Term Solver::mkTerm(Kind kind, const std::vector& children) const { CVC5_API_TRY_CATCH_BEGIN; @@ -6127,64 +6077,6 @@ Term Solver::mkTerm(Kind kind, const std::vector& children) const CVC5_API_TRY_CATCH_END; } -Term Solver::mkTerm(const Op& op) const -{ - CVC5_API_TRY_CATCH_BEGIN; - CVC5_API_SOLVER_CHECK_OP(op); - if (!op.isIndexedHelper()) - { - return mkTermFromKind(op.d_kind); - } - checkMkTerm(op.d_kind, 0); - //////// all checks before this line - const cvc5::Kind int_kind = extToIntKind(op.d_kind); - Term res = Term(this, getNodeManager()->mkNode(int_kind, *op.d_node)); - - (void)res.d_node->getType(true); /* kick off type checking */ - return res; - //////// - CVC5_API_TRY_CATCH_END; -} - -Term Solver::mkTerm(const Op& op, const Term& child) const -{ - CVC5_API_TRY_CATCH_BEGIN; - CVC5_API_SOLVER_CHECK_OP(op); - CVC5_API_SOLVER_CHECK_TERM(child); - //////// all checks before this line - return mkTermHelper(op, std::vector{child}); - //////// - CVC5_API_TRY_CATCH_END; -} - -Term Solver::mkTerm(const Op& op, const Term& child1, const Term& child2) const -{ - CVC5_API_TRY_CATCH_BEGIN; - CVC5_API_SOLVER_CHECK_OP(op); - CVC5_API_SOLVER_CHECK_TERM(child1); - CVC5_API_SOLVER_CHECK_TERM(child2); - //////// all checks before this line - return mkTermHelper(op, std::vector{child1, child2}); - //////// - CVC5_API_TRY_CATCH_END; -} - -Term Solver::mkTerm(const Op& op, - const Term& child1, - const Term& child2, - const Term& child3) const -{ - CVC5_API_TRY_CATCH_BEGIN; - CVC5_API_SOLVER_CHECK_OP(op); - CVC5_API_SOLVER_CHECK_TERM(child1); - CVC5_API_SOLVER_CHECK_TERM(child2); - CVC5_API_SOLVER_CHECK_TERM(child3); - //////// all checks before this line - return mkTermHelper(op, std::vector{child1, child2, child3}); - //////// - CVC5_API_TRY_CATCH_END; -} - Term Solver::mkTerm(const Op& op, const std::vector& children) const { CVC5_API_TRY_CATCH_BEGIN; diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h index d0419bf1e..83187a1b0 100644 --- a/src/api/cpp/cvc5.h +++ b/src/api/cpp/cvc5.h @@ -3230,91 +3230,12 @@ class CVC5_EXPORT Solver /* Create Terms */ /* .................................................................... */ - /** - * Create 0-ary term of given kind. - * @param kind the kind of the term - * @return the Term - */ - Term mkTerm(Kind kind) const; - - /** - * Create a unary term of given kind. - * @param kind the kind of the term - * @param child the child of the term - * @return the Term - */ - Term mkTerm(Kind kind, const Term& child) const; - - /** - * Create binary term of given kind. - * @param kind the kind of the term - * @param child1 the first child of the term - * @param child2 the second child of the term - * @return the Term - */ - Term mkTerm(Kind kind, const Term& child1, const Term& child2) const; - - /** - * Create ternary term of given kind. - * @param kind the kind of the term - * @param child1 the first child of the term - * @param child2 the second child of the term - * @param child3 the third child of the term - * @return the Term - */ - Term mkTerm(Kind kind, - const Term& child1, - const Term& child2, - const Term& child3) const; - /** * Create n-ary term of given kind. * @param kind the kind of the term * @param children the children of the term - * @return the Term - */ - Term mkTerm(Kind kind, const std::vector& children) const; - - /** - * Create nullary term of given kind from a given operator. - * Create operators with mkOp(). - * @param op the operator - * @return the Term - */ - Term mkTerm(const Op& op) const; - - /** - * Create unary term of given kind from a given operator. - * Create operators with mkOp(). - * @param op the operator - * @param child the child of the term - * @return the Term - */ - Term mkTerm(const Op& op, const Term& child) const; - - /** - * Create binary term of given kind from a given operator. - * Create operators with mkOp(). - * @param op the operator - * @param child1 the first child of the term - * @param child2 the second child of the term - * @return the Term - */ - Term mkTerm(const Op& op, const Term& child1, const Term& child2) const; - - /** - * Create ternary term of given kind from a given operator. - * Create operators with mkOp(). - * @param op the operator - * @param child1 the first child of the term - * @param child2 the second child of the term - * @param child3 the third child of the term - * @return the Term - */ - Term mkTerm(const Op& op, - const Term& child1, - const Term& child2, - const Term& child3) const; + * @return the Term */ + Term mkTerm(Kind kind, const std::vector& children = {}) const; /** * Create n-ary term of given kind from a given operator. @@ -3323,7 +3244,7 @@ class CVC5_EXPORT Solver * @param children the children of the term * @return the Term */ - Term mkTerm(const Op& op, const std::vector& children) const; + Term mkTerm(const Op& op, const std::vector& children = {}) const; /** * Create a tuple term. Terms are automatically converted if sorts are diff --git a/src/api/java/jni/solver.cpp b/src/api/java/jni/solver.cpp index 4544ca2a7..fae1b44eb 100644 --- a/src/api/java/jni/solver.cpp +++ b/src/api/java/jni/solver.cpp @@ -545,7 +545,7 @@ JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_mkTerm__JIJ( Solver* solver = reinterpret_cast(pointer); Kind kind = (Kind)kindValue; Term* child = reinterpret_cast(childPointer); - Term* termPointer = new Term(solver->mkTerm(kind, *child)); + Term* termPointer = new Term(solver->mkTerm(kind, {*child})); return reinterpret_cast(termPointer); CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); } @@ -568,7 +568,7 @@ Java_io_github_cvc5_api_Solver_mkTerm__JIJJ(JNIEnv* env, Kind kind = (Kind)kindValue; Term* child1 = reinterpret_cast(child1Pointer); Term* child2 = reinterpret_cast(child2Pointer); - Term* termPointer = new Term(solver->mkTerm(kind, *child1, *child2)); + Term* termPointer = new Term(solver->mkTerm(kind, {*child1, *child2})); return reinterpret_cast(termPointer); CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); } @@ -593,7 +593,8 @@ Java_io_github_cvc5_api_Solver_mkTerm__JIJJJ(JNIEnv* env, Term* child1 = reinterpret_cast(child1Pointer); Term* child2 = reinterpret_cast(child2Pointer); Term* child3 = reinterpret_cast(child3Pointer); - Term* retPointer = new Term(solver->mkTerm(kind, *child1, *child2, *child3)); + Term* retPointer = + new Term(solver->mkTerm(kind, {*child1, *child2, *child3})); return reinterpret_cast(retPointer); CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); } @@ -648,7 +649,7 @@ JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_mkTerm__JJJ( Solver* solver = reinterpret_cast(pointer); Op* op = reinterpret_cast(opPointer); Term* child = reinterpret_cast(childPointer); - Term* retPointer = new Term(solver->mkTerm(*op, *child)); + Term* retPointer = new Term(solver->mkTerm(*op, {*child})); return reinterpret_cast(retPointer); CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); } @@ -671,7 +672,7 @@ Java_io_github_cvc5_api_Solver_mkTerm__JJJJ(JNIEnv* env, Op* op = reinterpret_cast(opPointer); Term* child1 = reinterpret_cast(child1Pointer); Term* child2 = reinterpret_cast(child2Pointer); - Term* retPointer = new Term(solver->mkTerm(*op, *child1, *child2)); + Term* retPointer = new Term(solver->mkTerm(*op, {*child1, *child2})); return reinterpret_cast(retPointer); CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); } @@ -696,7 +697,7 @@ Java_io_github_cvc5_api_Solver_mkTerm__JJJJJ(JNIEnv* env, Term* child1 = reinterpret_cast(child1Pointer); Term* child2 = reinterpret_cast(child2Pointer); Term* child3 = reinterpret_cast(child3Pointer); - Term* retPointer = new Term(solver->mkTerm(*op, *child1, *child2, *child3)); + Term* retPointer = new Term(solver->mkTerm(*op, {*child1, *child2, *child3})); return reinterpret_cast(retPointer); CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); } diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp index 9969602c4..acb8b78a5 100644 --- a/src/parser/parser.cpp +++ b/src/parser/parser.cpp @@ -122,7 +122,7 @@ api::Term Parser::getExpressionForNameAndType(const std::string& name, if (te.isConstructor() && te.getConstructorArity() == 0) { // nullary constructors have APPLY_CONSTRUCTOR kind with no children - expr = d_solver->mkTerm(api::APPLY_CONSTRUCTOR, expr); + expr = d_solver->mkTerm(api::APPLY_CONSTRUCTOR, {expr}); } return expr; } @@ -513,7 +513,7 @@ api::Term Parser::mkHoApply(api::Term expr, const std::vector& args) { for (unsigned i = 0; i < args.size(); i++) { - expr = d_solver->mkTerm(api::HO_APPLY, expr, args[i]); + expr = d_solver->mkTerm(api::HO_APPLY, {expr, args[i]}); } return expr; } diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 40446874d..5985d4f8f 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -121,7 +121,7 @@ using namespace cvc5::parser; #undef SYM_MAN #define SYM_MAN PARSER_STATE->getSymbolManager() #undef MK_TERM -#define MK_TERM SOLVER->mkTerm +#define MK_TERM(KIND, ...) SOLVER->mkTerm(KIND, {__VA_ARGS__}) #define UNSUPPORTED PARSER_STATE->unimplementedFeature }/* parser::postinclude */ @@ -1504,7 +1504,7 @@ termNonVariable[cvc5::api::Term& expr, cvc5::api::Term& expr2] { std::vector indices; api::Op op = SOLVER->mkOp(api::TUPLE_PROJECT, indices); - expr = SOLVER->mkTerm(op, expr); + expr = SOLVER->mkTerm(op, {expr}); } | /* an atomic term (a term with no subterms) */ termAtomic[atomTerm] { expr = atomTerm; } diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index 74e045b4c..cb979d463 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -1024,13 +1024,13 @@ api::Term Smt2::applyParseOp(ParseOp& p, std::vector& args) api::Term ret; if (p.d_kind == api::APPLY_SELECTOR) { - ret = d_solver->mkTerm( - api::APPLY_SELECTOR, dt[0][n].getSelectorTerm(), args[0]); + ret = d_solver->mkTerm(api::APPLY_SELECTOR, + {dt[0][n].getSelectorTerm(), args[0]}); } else { - ret = d_solver->mkTerm( - api::APPLY_UPDATER, dt[0][n].getUpdaterTerm(), args[0], args[1]); + ret = d_solver->mkTerm(api::APPLY_UPDATER, + {dt[0][n].getUpdaterTerm(), args[0], args[1]}); } Trace("parser") << "applyParseOp: return selector " << ret << std::endl; return ret; @@ -1088,7 +1088,7 @@ api::Term Smt2::applyParseOp(ParseOp& p, std::vector& args) << std::endl; return ret; } - api::Term ret = d_solver->mkTerm(api::NEG, args[0]); + api::Term ret = d_solver->mkTerm(api::NEG, {args[0]}); Trace("parser") << "applyParseOp: return uminus " << ret << std::endl; return ret; } @@ -1105,7 +1105,7 @@ api::Term Smt2::applyParseOp(ParseOp& p, std::vector& args) } if (kind == api::SET_SINGLETON && args.size() == 1) { - api::Term ret = d_solver->mkTerm(api::SET_SINGLETON, args[0]); + api::Term ret = d_solver->mkTerm(api::SET_SINGLETON, {args[0]}); Trace("parser") << "applyParseOp: return set.singleton " << ret << std::endl; return ret; diff --git a/src/parser/tptp/Tptp.g b/src/parser/tptp/Tptp.g index c78494e2c..518b72ac5 100644 --- a/src/parser/tptp/Tptp.g +++ b/src/parser/tptp/Tptp.g @@ -75,9 +75,7 @@ using namespace cvc5::parser; #undef SOLVER #define SOLVER PARSER_STATE->getSolver() #undef MK_TERM -#define MK_TERM SOLVER->mkTerm -#undef MK_TERM -#define MK_TERM SOLVER->mkTerm +#define MK_TERM(KIND, ...) SOLVER->mkTerm(KIND, {__VA_ARGS__}) #define UNSUPPORTED PARSER_STATE->unimplementedFeature }/* @lexer::postinclude */ @@ -117,7 +115,7 @@ using namespace cvc5::parser; #undef SYM_MAN #define SYM_MAN PARSER_STATE->getSymbolManager() #undef MK_TERM -#define MK_TERM SOLVER->mkTerm +#define MK_TERM(KIND, ...) SOLVER->mkTerm(KIND, {__VA_ARGS__}) #define UNSUPPORTED PARSER_STATE->unimplementedFeature }/* parser::postinclude */ diff --git a/src/parser/tptp/tptp.cpp b/src/parser/tptp/tptp.cpp index d971c4f24..8681b623a 100644 --- a/src/parser/tptp/tptp.cpp +++ b/src/parser/tptp/tptp.cpp @@ -350,7 +350,7 @@ api::Term Tptp::applyParseOp(ParseOp& p, std::vector& args) } if (kind == api::SUB && args.size() == 1) { - return d_solver->mkTerm(api::NEG, args[0]); + return d_solver->mkTerm(api::NEG, {args[0]}); } if (kind == api::TO_REAL) { @@ -498,11 +498,11 @@ api::Term Tptp::convertRatToUnsorted(api::Term expr) // Add the inverse in order to show that over the elements that // appear in the problem there is a bijection between unsorted and // rational - api::Term ret = d_solver->mkTerm(api::APPLY_UF, d_rtu_op, expr); + api::Term ret = d_solver->mkTerm(api::APPLY_UF, {d_rtu_op, expr}); if (d_r_converted.find(expr) == d_r_converted.end()) { d_r_converted.insert(expr); api::Term eq = d_solver->mkTerm( - api::EQUAL, expr, d_solver->mkTerm(api::APPLY_UF, d_utr_op, ret)); + api::EQUAL, {expr, d_solver->mkTerm(api::APPLY_UF, {d_utr_op, ret})}); preemptCommand(new AssertCommand(eq)); } return api::Term(ret); @@ -535,8 +535,8 @@ api::Term Tptp::mkLambdaWrapper(api::Kind k, api::Sort argType) // apply body of lambda to variables api::Term wrapper = d_solver->mkTerm(api::LAMBDA, - d_solver->mkTerm(api::VARIABLE_LIST, lvars), - d_solver->mkTerm(k, lvars)); + {d_solver->mkTerm(api::VARIABLE_LIST, lvars), + d_solver->mkTerm(k, lvars)}); return wrapper; } @@ -556,7 +556,7 @@ api::Term Tptp::getAssertionExpr(FormulaRole fr, api::Term expr) return expr; case FR_CONJECTURE: // it should be negated when asserted - return d_solver->mkTerm(api::NOT, expr); + return d_solver->mkTerm(api::NOT, {expr}); case FR_UNKNOWN: case FR_FI_DOMAIN: case FR_FI_FUNCTORS: diff --git a/src/smt/command.cpp b/src/smt/command.cpp index 5535cd0c2..59e79c28c 100644 --- a/src/smt/command.cpp +++ b/src/smt/command.cpp @@ -1512,9 +1512,9 @@ void GetValueCommand::invoke(api::Solver* solver, SymbolManager* sm) { api::Term request = d_terms[i]; api::Term value = result[i]; - result[i] = solver->mkTerm(api::SEXPR, request, value); + result[i] = solver->mkTerm(api::SEXPR, {request, value}); } - d_result = solver->mkTerm(api::SEXPR, result); + d_result = solver->mkTerm(api::SEXPR, {result}); d_commandStatus = CommandSuccess::instance(); } catch (api::CVC5ApiRecoverableException& e) @@ -1587,7 +1587,7 @@ void GetAssignmentCommand::invoke(api::Solver* solver, SymbolManager* sm) // Treat the expression name as a variable name as opposed to a string // constant to avoid printing double quotes around the name. api::Term name = solver->mkVar(solver->getBooleanSort(), names[i]); - sexprs.push_back(solver->mkTerm(api::SEXPR, name, values[i])); + sexprs.push_back(solver->mkTerm(api::SEXPR, {name, values[i]})); } d_result = solver->mkTerm(api::SEXPR, sexprs); d_commandStatus = CommandSuccess::instance(); @@ -2713,7 +2713,7 @@ void GetInfoCommand::invoke(api::Solver* solver, SymbolManager* sm) std::vector v; v.push_back(solver->mkString(":" + d_flag)); v.push_back(solver->mkString(solver->getInfo(d_flag))); - d_result = sexprToString(solver->mkTerm(api::SEXPR, v)); + d_result = sexprToString(solver->mkTerm(api::SEXPR, {v})); d_commandStatus = CommandSuccess::instance(); } catch (api::CVC5ApiUnsupportedException&) diff --git a/test/api/cpp/issue4889.cpp b/test/api/cpp/issue4889.cpp index 373aa6d00..404255c4a 100644 --- a/test/api/cpp/issue4889.cpp +++ b/test/api/cpp/issue4889.cpp @@ -28,9 +28,9 @@ int main() Term const0 = slv.mkConst(sort_fp32, "_c0"); Term const1 = slv.mkConst(sort_fp32, "_c2"); Term const2 = slv.mkConst(sort_bool, "_c4"); - Term ite = slv.mkTerm(ITE, const2, const1, const0); - Term rem = slv.mkTerm(FLOATINGPOINT_REM, ite, const1); - Term isnan = slv.mkTerm(FLOATINGPOINT_IS_NAN, rem); + Term ite = slv.mkTerm(ITE, {const2, const1, const0}); + Term rem = slv.mkTerm(FLOATINGPOINT_REM, {ite, const1}); + Term isnan = slv.mkTerm(FLOATINGPOINT_IS_NAN, {rem}); slv.checkSatAssuming(isnan); return 0; } diff --git a/test/api/cpp/issue5074.cpp b/test/api/cpp/issue5074.cpp index a8e91c27a..b744ea824 100644 --- a/test/api/cpp/issue5074.cpp +++ b/test/api/cpp/issue5074.cpp @@ -21,8 +21,8 @@ int main() { Solver slv; Term c1 = slv.mkConst(slv.getIntegerSort()); - Term t6 = slv.mkTerm(Kind::STRING_FROM_CODE, c1); - Term t12 = slv.mkTerm(Kind::STRING_TO_REGEXP, t6); + Term t6 = slv.mkTerm(Kind::STRING_FROM_CODE, {c1}); + Term t12 = slv.mkTerm(Kind::STRING_TO_REGEXP, {t6}); Term t14 = slv.mkTerm(Kind::STRING_REPLACE_RE, {t6, t12, t6}); Term t16 = slv.mkTerm(Kind::STRING_CONTAINS, {t14, t14}); slv.checkSatAssuming(t16.notTerm()); diff --git a/test/api/cpp/issue6111.cpp b/test/api/cpp/issue6111.cpp index c0366ce23..8d458ad8f 100644 --- a/test/api/cpp/issue6111.cpp +++ b/test/api/cpp/issue6111.cpp @@ -32,7 +32,7 @@ int main() vector args1; args1.push_back(zero); args1.push_back(input2_1); - Term bvult_res = solver.mkTerm(BITVECTOR_ULT, args1); + Term bvult_res = solver.mkTerm(BITVECTOR_ULT, {args1}); solver.assertFormula(bvult_res); Sort bvsort4 = solver.mkBitVectorSort(4); @@ -44,13 +44,13 @@ int main() args2.push_back(concat_result_42); args2.push_back( solver.mkTerm(solver.mkOp(BITVECTOR_EXTRACT, 7, 4), {concat_result_43})); - solver.assertFormula(solver.mkTerm(EQUAL, args2)); + solver.assertFormula(solver.mkTerm(EQUAL, {args2})); vector args3; args3.push_back(concat_result_42); args3.push_back( solver.mkTerm(solver.mkOp(BITVECTOR_EXTRACT, 3, 0), {concat_result_43})); - solver.assertFormula(solver.mkTerm(EQUAL, args3)); + solver.assertFormula(solver.mkTerm(EQUAL, {args3})); cout << solver.checkSat() << endl; diff --git a/test/api/cpp/proj-issue306.cpp b/test/api/cpp/proj-issue306.cpp index 35ecda567..8aa857e66 100644 --- a/test/api/cpp/proj-issue306.cpp +++ b/test/api/cpp/proj-issue306.cpp @@ -29,9 +29,9 @@ int main(void) Term t3 = slv.mkConst(s1, "_x2"); Term t11 = slv.mkString(""); Term t14 = slv.mkConst(s3, "_x11"); - Term t42 = slv.mkTerm(Kind::ITE, t3, t14, t1); - Term t58 = slv.mkTerm(Kind::STRING_LEQ, t14, t11); - Term t95 = slv.mkTerm(Kind::EQUAL, t14, t42); + Term t42 = slv.mkTerm(Kind::ITE, {t3, t14, t1}); + Term t58 = slv.mkTerm(Kind::STRING_LEQ, {t14, t11}); + Term t95 = slv.mkTerm(Kind::EQUAL, {t14, t42}); slv.assertFormula(t95); slv.checkSatAssuming({t58}); } diff --git a/test/api/cpp/proj-issue334.cpp b/test/api/cpp/proj-issue334.cpp index bbb7f1a46..6598bba2e 100644 --- a/test/api/cpp/proj-issue334.cpp +++ b/test/api/cpp/proj-issue334.cpp @@ -27,10 +27,10 @@ int main(void) Term val = slv.mkBitVector(32, "10000000110010111010111011000101", 2); Term t1 = slv.mkFloatingPoint(8, 24, val); Term t2 = slv.mkConst(s1); - Term t4 = slv.mkTerm(Kind::BITVECTOR_TO_NAT, t2); - Term t5 = slv.mkTerm(Kind::STRING_FROM_CODE, t4); + Term t4 = slv.mkTerm(Kind::BITVECTOR_TO_NAT, {t2}); + Term t5 = slv.mkTerm(Kind::STRING_FROM_CODE, {t4}); Term t6 = slv.simplify(t5); - Term t7 = slv.mkTerm(Kind::STRING_LEQ, t5, t6); + Term t7 = slv.mkTerm(Kind::STRING_LEQ, {t5, t6}); slv.assertFormula(t7); slv.simplify(t1); } diff --git a/test/api/cpp/reset_assertions.cpp b/test/api/cpp/reset_assertions.cpp index 68e22f7dc..3edea1a01 100644 --- a/test/api/cpp/reset_assertions.cpp +++ b/test/api/cpp/reset_assertions.cpp @@ -33,7 +33,7 @@ int main() Sort real = slv.getRealSort(); Term x = slv.mkConst(real, "x"); Term four = slv.mkInteger(4); - Term xEqFour = slv.mkTerm(Kind::EQUAL, x, four); + Term xEqFour = slv.mkTerm(Kind::EQUAL, {x, four}); slv.assertFormula(xEqFour); std::cout << slv.checkSat() << std::endl; @@ -43,9 +43,9 @@ int main() Sort indexType = slv.getIntegerSort(); Sort arrayType = slv.mkArraySort(indexType, elementType); Term array = slv.mkConst(arrayType, "array"); - Term arrayAtFour = slv.mkTerm(Kind::SELECT, array, four); + Term arrayAtFour = slv.mkTerm(Kind::SELECT, {array, four}); Term ten = slv.mkInteger(10); - Term arrayAtFour_eq_ten = slv.mkTerm(Kind::EQUAL, arrayAtFour, ten); + Term arrayAtFour_eq_ten = slv.mkTerm(Kind::EQUAL, {arrayAtFour, ten}); slv.assertFormula(arrayAtFour_eq_ten); std::cout << slv.checkSat() << std::endl; } diff --git a/test/api/cpp/sep_log_api.cpp b/test/api/cpp/sep_log_api.cpp index 6a2fc9740..84aac0424 100644 --- a/test/api/cpp/sep_log_api.cpp +++ b/test/api/cpp/sep_log_api.cpp @@ -54,7 +54,7 @@ int validate_exception(void) Term y = slv.mkConst(integer, "y"); /* y > x */ - Term y_gt_x(slv.mkTerm(Kind::GT, y, x)); + Term y_gt_x(slv.mkTerm(Kind::GT, {y, x})); /* assert it */ slv.assertFormula(y_gt_x); @@ -156,18 +156,18 @@ int validate_getters(void) Term p2 = slv.mkConst(integer, "p2"); /* Constraints on x and y */ - Term x_equal_const = slv.mkTerm(Kind::EQUAL, x, random_constant); - Term y_gt_x = slv.mkTerm(Kind::GT, y, x); + Term x_equal_const = slv.mkTerm(Kind::EQUAL, {x, random_constant}); + Term y_gt_x = slv.mkTerm(Kind::GT, {y, x}); /* Points-to expressions */ - Term p1_to_x = slv.mkTerm(Kind::SEP_PTO, p1, x); - Term p2_to_y = slv.mkTerm(Kind::SEP_PTO, p2, y); + Term p1_to_x = slv.mkTerm(Kind::SEP_PTO, {p1, x}); + Term p2_to_y = slv.mkTerm(Kind::SEP_PTO, {p2, y}); /* Heap -- the points-to have to be "starred"! */ - Term heap = slv.mkTerm(Kind::SEP_STAR, p1_to_x, p2_to_y); + Term heap = slv.mkTerm(Kind::SEP_STAR, {p1_to_x, p2_to_y}); /* Constain "nil" to be something random */ - Term fix_nil = slv.mkTerm(Kind::EQUAL, nil, expr_nil_val); + Term fix_nil = slv.mkTerm(Kind::EQUAL, {nil, expr_nil_val}); /* Add it all to the solver! */ slv.assertFormula(x_equal_const); diff --git a/test/unit/api/cpp/solver_black.cpp b/test/unit/api/cpp/solver_black.cpp index 3acdecbb8..7c28fde12 100644 --- a/test/unit/api/cpp/solver_black.cpp +++ b/test/unit/api/cpp/solver_black.cpp @@ -46,8 +46,8 @@ TEST_F(TestApiBlackSolver, pow2Large1) ctors.back().addSelector("_x112", s7); Sort s11 = d_solver.declareDatatype("_x107", ctors); Term t82 = d_solver.mkConst(s11, "_x114"); - Term t180 = d_solver.mkTerm(POW2, t10); - Term t258 = d_solver.mkTerm(GEQ, t74, t180); + Term t180 = d_solver.mkTerm(POW2, {t10}); + Term t258 = d_solver.mkTerm(GEQ, {t74, t180}); d_solver.assertFormula(t258); ASSERT_THROW(d_solver.simplify(t82), CVC5ApiException); } @@ -56,9 +56,9 @@ TEST_F(TestApiBlackSolver, pow2Large2) { // Based on https://github.com/cvc5/cvc5-projects/issues/333 Term t1 = d_solver.mkBitVector(63, ~(((uint64_t)1) << 62)); - Term t2 = d_solver.mkTerm(Kind::BITVECTOR_TO_NAT, t1); - Term t3 = d_solver.mkTerm(Kind::POW2, t2); - Term t4 = d_solver.mkTerm(Kind::DISTINCT, t3, t2); + Term t2 = d_solver.mkTerm(Kind::BITVECTOR_TO_NAT, {t1}); + Term t3 = d_solver.mkTerm(Kind::POW2, {t2}); + Term t4 = d_solver.mkTerm(Kind::DISTINCT, {t3, t2}); ASSERT_THROW(d_solver.checkSatAssuming({t4}), CVC5ApiException); } @@ -67,8 +67,8 @@ TEST_F(TestApiBlackSolver, pow2Large3) // Based on https://github.com/cvc5/cvc5-projects/issues/339 Sort s4 = d_solver.getIntegerSort(); Term t203 = d_solver.mkInteger("6135470354240554220207"); - Term t262 = d_solver.mkTerm(POW2, t203); - Term t536 = d_solver.mkTerm(d_solver.mkOp(INT_TO_BITVECTOR, 49), t262); + Term t262 = d_solver.mkTerm(POW2, {t203}); + Term t536 = d_solver.mkTerm(d_solver.mkOp(INT_TO_BITVECTOR, 49), {t262}); ASSERT_THROW(d_solver.simplify(t536), CVC5ApiException); } @@ -230,8 +230,7 @@ TEST_F(TestApiBlackSolver, mkDatatypeSorts) Term t1 = d_solver.mkConst(isort1, "t"); Term t0 = d_solver.mkTerm( APPLY_SELECTOR, - t1.getSort().getDatatype().getSelector("s1").getSelectorTerm(), - t1); + {t1.getSort().getDatatype().getSelector("s1").getSelectorTerm(), t1}); ASSERT_EQ(dt_sorts[0].instantiate({d_solver.getBooleanSort()}), t0.getSort()); /* Note: More tests are in datatype_api_black. */ @@ -664,7 +663,8 @@ TEST_F(TestApiBlackSolver, mkRegexpAll) { Sort strSort = d_solver.getStringSort(); Term s = d_solver.mkConst(strSort, "s"); - ASSERT_NO_THROW(d_solver.mkTerm(STRING_IN_REGEXP, s, d_solver.mkRegexpAll())); + ASSERT_NO_THROW( + d_solver.mkTerm(STRING_IN_REGEXP, {s, d_solver.mkRegexpAll()})); } TEST_F(TestApiBlackSolver, mkRegexpAllchar) @@ -672,7 +672,7 @@ TEST_F(TestApiBlackSolver, mkRegexpAllchar) Sort strSort = d_solver.getStringSort(); Term s = d_solver.mkConst(strSort, "s"); ASSERT_NO_THROW( - d_solver.mkTerm(STRING_IN_REGEXP, s, d_solver.mkRegexpAllchar())); + d_solver.mkTerm(STRING_IN_REGEXP, {s, d_solver.mkRegexpAllchar()})); } TEST_F(TestApiBlackSolver, mkRegexpNone) @@ -680,7 +680,7 @@ TEST_F(TestApiBlackSolver, mkRegexpNone) Sort strSort = d_solver.getStringSort(); Term s = d_solver.mkConst(strSort, "s"); ASSERT_NO_THROW( - d_solver.mkTerm(STRING_IN_REGEXP, s, d_solver.mkRegexpNone())); + d_solver.mkTerm(STRING_IN_REGEXP, {s, d_solver.mkRegexpNone()})); } TEST_F(TestApiBlackSolver, mkSepEmp) { ASSERT_NO_THROW(d_solver.mkSepEmp()); } @@ -718,61 +718,63 @@ TEST_F(TestApiBlackSolver, mkTerm) // mkTerm(Kind kind) const ASSERT_NO_THROW(d_solver.mkTerm(PI)); - ASSERT_NO_THROW(d_solver.mkTerm(PI, v6)); + ASSERT_NO_THROW(d_solver.mkTerm(PI, {v6})); ASSERT_NO_THROW(d_solver.mkTerm(d_solver.mkOp(PI))); - ASSERT_NO_THROW(d_solver.mkTerm(d_solver.mkOp(PI), v6)); + ASSERT_NO_THROW(d_solver.mkTerm(d_solver.mkOp(PI), {v6})); ASSERT_NO_THROW(d_solver.mkTerm(REGEXP_NONE)); - ASSERT_NO_THROW(d_solver.mkTerm(REGEXP_NONE, v6)); + ASSERT_NO_THROW(d_solver.mkTerm(REGEXP_NONE, {v6})); ASSERT_NO_THROW(d_solver.mkTerm(d_solver.mkOp(REGEXP_NONE))); - ASSERT_NO_THROW(d_solver.mkTerm(d_solver.mkOp(REGEXP_NONE), v6)); + ASSERT_NO_THROW(d_solver.mkTerm(d_solver.mkOp(REGEXP_NONE), {v6})); ASSERT_NO_THROW(d_solver.mkTerm(REGEXP_ALLCHAR)); - ASSERT_NO_THROW(d_solver.mkTerm(REGEXP_ALLCHAR, v6)); + ASSERT_NO_THROW(d_solver.mkTerm(REGEXP_ALLCHAR, {v6})); ASSERT_NO_THROW(d_solver.mkTerm(d_solver.mkOp(REGEXP_ALLCHAR))); - ASSERT_NO_THROW(d_solver.mkTerm(d_solver.mkOp(REGEXP_ALLCHAR), v6)); + ASSERT_NO_THROW(d_solver.mkTerm(d_solver.mkOp(REGEXP_ALLCHAR), {v6})); ASSERT_NO_THROW(d_solver.mkTerm(SEP_EMP)); - ASSERT_NO_THROW(d_solver.mkTerm(SEP_EMP, v6)); + ASSERT_NO_THROW(d_solver.mkTerm(SEP_EMP, {v6})); ASSERT_NO_THROW(d_solver.mkTerm(d_solver.mkOp(SEP_EMP))); - ASSERT_NO_THROW(d_solver.mkTerm(d_solver.mkOp(SEP_EMP), v6)); + ASSERT_NO_THROW(d_solver.mkTerm(d_solver.mkOp(SEP_EMP), {v6})); ASSERT_THROW(d_solver.mkTerm(CONST_BITVECTOR), CVC5ApiException); // mkTerm(Kind kind, Term child) const - ASSERT_NO_THROW(d_solver.mkTerm(NOT, d_solver.mkTrue())); + ASSERT_NO_THROW(d_solver.mkTerm(NOT, {d_solver.mkTrue()})); ASSERT_NO_THROW( - d_solver.mkTerm(BAG_MAKE, d_solver.mkTrue(), d_solver.mkInteger(1))); - ASSERT_THROW(d_solver.mkTerm(NOT, Term()), CVC5ApiException); - ASSERT_THROW(d_solver.mkTerm(NOT, a), CVC5ApiException); - ASSERT_THROW(slv.mkTerm(NOT, d_solver.mkTrue()), CVC5ApiException); + d_solver.mkTerm(BAG_MAKE, {d_solver.mkTrue(), d_solver.mkInteger(1)})); + ASSERT_THROW(d_solver.mkTerm(NOT, {Term()}), CVC5ApiException); + ASSERT_THROW(d_solver.mkTerm(NOT, {a}), CVC5ApiException); + ASSERT_THROW(slv.mkTerm(NOT, {d_solver.mkTrue()}), CVC5ApiException); // mkTerm(Kind kind, Term child1, Term child2) const - ASSERT_NO_THROW(d_solver.mkTerm(EQUAL, a, b)); - ASSERT_THROW(d_solver.mkTerm(EQUAL, Term(), b), CVC5ApiException); - ASSERT_THROW(d_solver.mkTerm(EQUAL, a, Term()), CVC5ApiException); - ASSERT_THROW(d_solver.mkTerm(EQUAL, a, d_solver.mkTrue()), CVC5ApiException); - ASSERT_THROW(slv.mkTerm(EQUAL, a, b), CVC5ApiException); + ASSERT_NO_THROW(d_solver.mkTerm(EQUAL, {a, b})); + ASSERT_THROW(d_solver.mkTerm(EQUAL, {Term(), b}), CVC5ApiException); + ASSERT_THROW(d_solver.mkTerm(EQUAL, {a, Term()}), CVC5ApiException); + ASSERT_THROW(d_solver.mkTerm(EQUAL, {a, d_solver.mkTrue()}), + CVC5ApiException); + ASSERT_THROW(slv.mkTerm(EQUAL, {a, b}), CVC5ApiException); // mkTerm(Kind kind, Term child1, Term child2, Term child3) const ASSERT_NO_THROW(d_solver.mkTerm( - ITE, d_solver.mkTrue(), d_solver.mkTrue(), d_solver.mkTrue())); + ITE, {d_solver.mkTrue(), d_solver.mkTrue(), d_solver.mkTrue()})); ASSERT_THROW( - d_solver.mkTerm(ITE, Term(), d_solver.mkTrue(), d_solver.mkTrue()), + d_solver.mkTerm(ITE, {Term(), d_solver.mkTrue(), d_solver.mkTrue()}), CVC5ApiException); ASSERT_THROW( - d_solver.mkTerm(ITE, d_solver.mkTrue(), Term(), d_solver.mkTrue()), + d_solver.mkTerm(ITE, {d_solver.mkTrue(), Term(), d_solver.mkTrue()}), CVC5ApiException); ASSERT_THROW( - d_solver.mkTerm(ITE, d_solver.mkTrue(), d_solver.mkTrue(), Term()), + d_solver.mkTerm(ITE, {d_solver.mkTrue(), d_solver.mkTrue(), Term()}), CVC5ApiException); - ASSERT_THROW(d_solver.mkTerm(ITE, d_solver.mkTrue(), d_solver.mkTrue(), b), + ASSERT_THROW(d_solver.mkTerm(ITE, {d_solver.mkTrue(), d_solver.mkTrue(), b}), CVC5ApiException); ASSERT_THROW( - slv.mkTerm(ITE, d_solver.mkTrue(), d_solver.mkTrue(), d_solver.mkTrue()), + slv.mkTerm(ITE, + {d_solver.mkTrue(), d_solver.mkTrue(), d_solver.mkTrue()}), CVC5ApiException); // mkTerm(Kind kind, const std::vector& children) const - ASSERT_NO_THROW(d_solver.mkTerm(EQUAL, v1)); - ASSERT_THROW(d_solver.mkTerm(EQUAL, v2), CVC5ApiException); - ASSERT_THROW(d_solver.mkTerm(EQUAL, v3), CVC5ApiException); - ASSERT_THROW(d_solver.mkTerm(DISTINCT, v6), CVC5ApiException); + ASSERT_NO_THROW(d_solver.mkTerm(EQUAL, {v1})); + ASSERT_THROW(d_solver.mkTerm(EQUAL, {v2}), CVC5ApiException); + ASSERT_THROW(d_solver.mkTerm(EQUAL, {v3}), CVC5ApiException); + ASSERT_THROW(d_solver.mkTerm(DISTINCT, {v6}), CVC5ApiException); // Test cases that are nary via the API but have arity = 2 internally Sort s_bool = d_solver.getBooleanSort(); @@ -854,61 +856,62 @@ TEST_F(TestApiBlackSolver, mkTermFromOp) Term tailTerm2 = list["cons"]["tail"].getSelectorTerm(); // mkTerm(Op op, Term term) const - ASSERT_NO_THROW(d_solver.mkTerm(APPLY_CONSTRUCTOR, nilTerm1)); - ASSERT_NO_THROW(d_solver.mkTerm(APPLY_CONSTRUCTOR, nilTerm2)); - ASSERT_THROW(d_solver.mkTerm(APPLY_SELECTOR, nilTerm1), CVC5ApiException); - ASSERT_THROW(d_solver.mkTerm(APPLY_SELECTOR, consTerm1), CVC5ApiException); - ASSERT_THROW(d_solver.mkTerm(APPLY_CONSTRUCTOR, consTerm2), CVC5ApiException); + ASSERT_NO_THROW(d_solver.mkTerm(APPLY_CONSTRUCTOR, {nilTerm1})); + ASSERT_NO_THROW(d_solver.mkTerm(APPLY_CONSTRUCTOR, {nilTerm2})); + ASSERT_THROW(d_solver.mkTerm(APPLY_SELECTOR, {nilTerm1}), CVC5ApiException); + ASSERT_THROW(d_solver.mkTerm(APPLY_SELECTOR, {consTerm1}), CVC5ApiException); + ASSERT_THROW(d_solver.mkTerm(APPLY_CONSTRUCTOR, {consTerm2}), + CVC5ApiException); ASSERT_THROW(d_solver.mkTerm(opterm1), CVC5ApiException); - ASSERT_THROW(d_solver.mkTerm(APPLY_SELECTOR, headTerm1), CVC5ApiException); + ASSERT_THROW(d_solver.mkTerm(APPLY_SELECTOR, {headTerm1}), CVC5ApiException); ASSERT_THROW(d_solver.mkTerm(opterm1), CVC5ApiException); - ASSERT_THROW(slv.mkTerm(APPLY_CONSTRUCTOR, nilTerm1), CVC5ApiException); + ASSERT_THROW(slv.mkTerm(APPLY_CONSTRUCTOR, {nilTerm1}), CVC5ApiException); // mkTerm(Op op, Term child) const - ASSERT_NO_THROW(d_solver.mkTerm(opterm1, a)); - ASSERT_NO_THROW(d_solver.mkTerm(opterm2, d_solver.mkInteger(1))); - ASSERT_NO_THROW(d_solver.mkTerm(APPLY_SELECTOR, headTerm1, c)); - ASSERT_NO_THROW(d_solver.mkTerm(APPLY_SELECTOR, tailTerm2, c)); - ASSERT_THROW(d_solver.mkTerm(opterm2, a), CVC5ApiException); - ASSERT_THROW(d_solver.mkTerm(opterm1, Term()), CVC5ApiException); + ASSERT_NO_THROW(d_solver.mkTerm(opterm1, {a})); + ASSERT_NO_THROW(d_solver.mkTerm(opterm2, {d_solver.mkInteger(1)})); + ASSERT_NO_THROW(d_solver.mkTerm(APPLY_SELECTOR, {headTerm1, c})); + ASSERT_NO_THROW(d_solver.mkTerm(APPLY_SELECTOR, {tailTerm2, c})); + ASSERT_THROW(d_solver.mkTerm(opterm2, {a}), CVC5ApiException); + ASSERT_THROW(d_solver.mkTerm(opterm1, {Term()}), CVC5ApiException); ASSERT_THROW( - d_solver.mkTerm(APPLY_CONSTRUCTOR, consTerm1, d_solver.mkInteger(0)), + d_solver.mkTerm(APPLY_CONSTRUCTOR, {consTerm1, d_solver.mkInteger(0)}), CVC5ApiException); - ASSERT_THROW(slv.mkTerm(opterm1, a), CVC5ApiException); + ASSERT_THROW(slv.mkTerm(opterm1, {a}), CVC5ApiException); // mkTerm(Op op, Term child1, Term child2) const ASSERT_NO_THROW( d_solver.mkTerm(APPLY_CONSTRUCTOR, - consTerm1, - d_solver.mkInteger(0), - d_solver.mkTerm(APPLY_CONSTRUCTOR, nilTerm1))); + {consTerm1, + d_solver.mkInteger(0), + d_solver.mkTerm(APPLY_CONSTRUCTOR, {nilTerm1})})); ASSERT_THROW( - d_solver.mkTerm(opterm2, d_solver.mkInteger(1), d_solver.mkInteger(2)), + d_solver.mkTerm(opterm2, {d_solver.mkInteger(1), d_solver.mkInteger(2)}), CVC5ApiException); - ASSERT_THROW(d_solver.mkTerm(opterm1, a, b), CVC5ApiException); - ASSERT_THROW(d_solver.mkTerm(opterm2, d_solver.mkInteger(1), Term()), + ASSERT_THROW(d_solver.mkTerm(opterm1, {a, b}), CVC5ApiException); + ASSERT_THROW(d_solver.mkTerm(opterm2, {d_solver.mkInteger(1), Term()}), CVC5ApiException); - ASSERT_THROW(d_solver.mkTerm(opterm2, Term(), d_solver.mkInteger(1)), + ASSERT_THROW(d_solver.mkTerm(opterm2, {Term(), d_solver.mkInteger(1)}), CVC5ApiException); ASSERT_THROW(slv.mkTerm(APPLY_CONSTRUCTOR, - consTerm1, - d_solver.mkInteger(0), - d_solver.mkTerm(APPLY_CONSTRUCTOR, nilTerm1)), + {consTerm1, + d_solver.mkInteger(0), + d_solver.mkTerm(APPLY_CONSTRUCTOR, {nilTerm1})}), CVC5ApiException); // mkTerm(Op op, Term child1, Term child2, Term child3) const - ASSERT_THROW(d_solver.mkTerm(opterm1, a, b, a), CVC5ApiException); + ASSERT_THROW(d_solver.mkTerm(opterm1, {a, b, a}), CVC5ApiException); ASSERT_THROW( - d_solver.mkTerm( - opterm2, d_solver.mkInteger(1), d_solver.mkInteger(1), Term()), + d_solver.mkTerm(opterm2, + {d_solver.mkInteger(1), d_solver.mkInteger(1), Term()}), CVC5ApiException); // mkTerm(Op op, const std::vector& children) const - ASSERT_NO_THROW(d_solver.mkTerm(opterm2, v4)); - ASSERT_THROW(d_solver.mkTerm(opterm2, v1), CVC5ApiException); - ASSERT_THROW(d_solver.mkTerm(opterm2, v2), CVC5ApiException); - ASSERT_THROW(d_solver.mkTerm(opterm2, v3), CVC5ApiException); - ASSERT_THROW(slv.mkTerm(opterm2, v4), CVC5ApiException); + ASSERT_NO_THROW(d_solver.mkTerm(opterm2, {v4})); + ASSERT_THROW(d_solver.mkTerm(opterm2, {v1}), CVC5ApiException); + ASSERT_THROW(d_solver.mkTerm(opterm2, {v2}), CVC5ApiException); + ASSERT_THROW(d_solver.mkTerm(opterm2, {v3}), CVC5ApiException); + ASSERT_THROW(slv.mkTerm(opterm2, {v4}), CVC5ApiException); } TEST_F(TestApiBlackSolver, mkTrue) @@ -1105,12 +1108,12 @@ TEST_F(TestApiBlackSolver, defineFunGlobal) // (assert (or (not f) (not (g true)))) d_solver.assertFormula(d_solver.mkTerm( - OR, f.notTerm(), d_solver.mkTerm(APPLY_UF, g, bTrue).notTerm())); + OR, {f.notTerm(), d_solver.mkTerm(APPLY_UF, {g, bTrue}).notTerm()})); ASSERT_TRUE(d_solver.checkSat().isUnsat()); d_solver.resetAssertions(); // (assert (or (not f) (not (g true)))) d_solver.assertFormula(d_solver.mkTerm( - OR, f.notTerm(), d_solver.mkTerm(APPLY_UF, g, bTrue).notTerm())); + OR, {f.notTerm(), d_solver.mkTerm(APPLY_UF, {g, bTrue}).notTerm()})); ASSERT_TRUE(d_solver.checkSat().isUnsat()); } @@ -1194,12 +1197,12 @@ TEST_F(TestApiBlackSolver, defineFunRecGlobal) // (assert (or (not f) (not (g true)))) d_solver.assertFormula(d_solver.mkTerm( - OR, f.notTerm(), d_solver.mkTerm(APPLY_UF, g, bTrue).notTerm())); + OR, {f.notTerm(), d_solver.mkTerm(APPLY_UF, {g, bTrue}).notTerm()})); ASSERT_TRUE(d_solver.checkSat().isUnsat()); d_solver.pop(); // (assert (or (not f) (not (g true)))) d_solver.assertFormula(d_solver.mkTerm( - OR, f.notTerm(), d_solver.mkTerm(APPLY_UF, g, bTrue).notTerm())); + OR, {f.notTerm(), d_solver.mkTerm(APPLY_UF, {g, bTrue}).notTerm()})); ASSERT_TRUE(d_solver.checkSat().isUnsat()); } @@ -1294,11 +1297,11 @@ TEST_F(TestApiBlackSolver, defineFunsRecGlobal) d_solver.defineFunsRec({gSym}, {{b}}, {b}, true); // (assert (not (g true))) - d_solver.assertFormula(d_solver.mkTerm(APPLY_UF, gSym, bTrue).notTerm()); + d_solver.assertFormula(d_solver.mkTerm(APPLY_UF, {gSym, bTrue}).notTerm()); ASSERT_TRUE(d_solver.checkSat().isUnsat()); d_solver.pop(); // (assert (not (g true))) - d_solver.assertFormula(d_solver.mkTerm(APPLY_UF, gSym, bTrue).notTerm()); + d_solver.assertFormula(d_solver.mkTerm(APPLY_UF, {gSym, bTrue}).notTerm()); ASSERT_TRUE(d_solver.checkSat().isUnsat()); } @@ -1309,7 +1312,7 @@ TEST_F(TestApiBlackSolver, uFIteration) Term x = d_solver.mkConst(intSort, "x"); Term y = d_solver.mkConst(intSort, "y"); Term f = d_solver.mkConst(funSort, "f"); - Term fxy = d_solver.mkTerm(APPLY_UF, f, x, y); + Term fxy = d_solver.mkTerm(APPLY_UF, {f, x, y}); // Expecting the uninterpreted function to be one of the children Term expected_children[3] = {f, x, y}; @@ -1340,9 +1343,9 @@ TEST_F(TestApiBlackSolver, getAbduct) Term y = d_solver.mkConst(intSort, "y"); // Assumptions for abduction: x > 0 - d_solver.assertFormula(d_solver.mkTerm(GT, x, zero)); + d_solver.assertFormula(d_solver.mkTerm(GT, {x, zero})); // Conjecture for abduction: y > 0 - Term conj = d_solver.mkTerm(GT, y, zero); + Term conj = d_solver.mkTerm(GT, {y, zero}); // Call the abduction api, while the resulting abduct is the output Term output = d_solver.getAbduct(conj); // We expect the resulting output to be a boolean formula @@ -1354,7 +1357,7 @@ TEST_F(TestApiBlackSolver, getAbduct) Term start = d_solver.mkVar(boolean); Term output2; Grammar g = d_solver.mkSygusGrammar({}, {start}); - Term conj2 = d_solver.mkTerm(GT, x, zero); + Term conj2 = d_solver.mkTerm(GT, {x, zero}); ASSERT_NO_THROW(g.addRule(start, truen)); // Call the abduction api, while the resulting abduct is the output output2 = d_solver.getAbduct(conj2, g); @@ -1371,9 +1374,9 @@ TEST_F(TestApiBlackSolver, getAbduct2) Term x = d_solver.mkConst(intSort, "x"); Term y = d_solver.mkConst(intSort, "y"); // Assumptions for abduction: x > 0 - d_solver.assertFormula(d_solver.mkTerm(GT, x, zero)); + d_solver.assertFormula(d_solver.mkTerm(GT, {x, zero})); // Conjecture for abduction: y > 0 - Term conj = d_solver.mkTerm(GT, y, zero); + Term conj = d_solver.mkTerm(GT, {y, zero}); // Fails due to option not set ASSERT_THROW(d_solver.getAbduct(conj), CVC5ApiException); } @@ -1390,9 +1393,9 @@ TEST_F(TestApiBlackSolver, getAbductNext) Term y = d_solver.mkConst(intSort, "y"); // Assumptions for abduction: x > 0 - d_solver.assertFormula(d_solver.mkTerm(GT, x, zero)); + d_solver.assertFormula(d_solver.mkTerm(GT, {x, zero})); // Conjecture for abduction: y > 0 - Term conj = d_solver.mkTerm(GT, y, zero); + Term conj = d_solver.mkTerm(GT, {y, zero}); // Call the abduction api, while the resulting abduct is the output Term output = d_solver.getAbduct(conj); Term output2 = d_solver.getAbductNext(); @@ -1413,13 +1416,14 @@ TEST_F(TestApiBlackSolver, getInterpolant) Term z = d_solver.mkConst(intSort, "z"); // Assumptions for interpolation: x + y > 0 /\ x < 0 - d_solver.assertFormula(d_solver.mkTerm(GT, d_solver.mkTerm(ADD, x, y), zero)); - d_solver.assertFormula(d_solver.mkTerm(LT, x, zero)); + d_solver.assertFormula( + d_solver.mkTerm(GT, {d_solver.mkTerm(ADD, {x, y}), zero})); + d_solver.assertFormula(d_solver.mkTerm(LT, {x, zero})); // Conjecture for interpolation: y + z > 0 \/ z < 0 - Term conj = - d_solver.mkTerm(OR, - d_solver.mkTerm(GT, d_solver.mkTerm(ADD, y, z), zero), - d_solver.mkTerm(LT, z, zero)); + Term conj = d_solver.mkTerm( + OR, + {d_solver.mkTerm(GT, {d_solver.mkTerm(ADD, {y, z}), zero}), + d_solver.mkTerm(LT, {z, zero})}); // Call the interpolation api, while the resulting interpolant is the output Term output = d_solver.getInterpolant(conj); @@ -1439,13 +1443,14 @@ TEST_F(TestApiBlackSolver, getInterpolantNext) Term y = d_solver.mkConst(intSort, "y"); Term z = d_solver.mkConst(intSort, "z"); // Assumptions for interpolation: x + y > 0 /\ x < 0 - d_solver.assertFormula(d_solver.mkTerm(GT, d_solver.mkTerm(ADD, x, y), zero)); - d_solver.assertFormula(d_solver.mkTerm(LT, x, zero)); + d_solver.assertFormula( + d_solver.mkTerm(GT, {d_solver.mkTerm(ADD, {x, y}), zero})); + d_solver.assertFormula(d_solver.mkTerm(LT, {x, zero})); // Conjecture for interpolation: y + z > 0 \/ z < 0 - Term conj = - d_solver.mkTerm(OR, - d_solver.mkTerm(GT, d_solver.mkTerm(ADD, y, z), zero), - d_solver.mkTerm(LT, z, zero)); + Term conj = d_solver.mkTerm( + OR, + {d_solver.mkTerm(GT, {d_solver.mkTerm(ADD, {y, z}), zero}), + d_solver.mkTerm(LT, {z, zero})}); Term output = d_solver.getInterpolant(conj); Term output2 = d_solver.getInterpolantNext(); @@ -1474,7 +1479,7 @@ TEST_F(TestApiBlackSolver, getOp) Sort bv32 = d_solver.mkBitVectorSort(32); Term a = d_solver.mkConst(bv32, "a"); Op ext = d_solver.mkOp(BITVECTOR_EXTRACT, 2, 1); - Term exta = d_solver.mkTerm(ext, a); + Term exta = d_solver.mkTerm(ext, {a}); ASSERT_FALSE(a.hasOp()); ASSERT_THROW(a.getOp(), CVC5ApiException); @@ -1496,10 +1501,10 @@ TEST_F(TestApiBlackSolver, getOp) Term nilTerm = consList.getConstructorTerm("nil"); Term headTerm = consList["cons"].getSelectorTerm("head"); - Term listnil = d_solver.mkTerm(APPLY_CONSTRUCTOR, nilTerm); - Term listcons1 = d_solver.mkTerm( - APPLY_CONSTRUCTOR, consTerm, d_solver.mkInteger(1), listnil); - Term listhead = d_solver.mkTerm(APPLY_SELECTOR, headTerm, listcons1); + Term listnil = d_solver.mkTerm(APPLY_CONSTRUCTOR, {nilTerm}); + Term listcons1 = d_solver.mkTerm(APPLY_CONSTRUCTOR, + {consTerm, d_solver.mkInteger(1), listnil}); + Term listhead = d_solver.mkTerm(APPLY_SELECTOR, {headTerm, listcons1}); ASSERT_TRUE(listnil.hasOp()); ASSERT_TRUE(listcons1.hasOp()); @@ -1636,14 +1641,14 @@ TEST_F(TestApiBlackSolver, getUnsatCoreAndProof) Term p = d_solver.mkConst(intPredSort, "p"); Term zero = d_solver.mkInteger(0); Term one = d_solver.mkInteger(1); - Term f_x = d_solver.mkTerm(APPLY_UF, f, x); - Term f_y = d_solver.mkTerm(APPLY_UF, f, y); - Term sum = d_solver.mkTerm(ADD, f_x, f_y); - Term p_0 = d_solver.mkTerm(APPLY_UF, p, zero); - Term p_f_y = d_solver.mkTerm(APPLY_UF, p, f_y); - d_solver.assertFormula(d_solver.mkTerm(GT, zero, f_x)); - d_solver.assertFormula(d_solver.mkTerm(GT, zero, f_y)); - d_solver.assertFormula(d_solver.mkTerm(GT, sum, one)); + Term f_x = d_solver.mkTerm(APPLY_UF, {f, x}); + Term f_y = d_solver.mkTerm(APPLY_UF, {f, y}); + Term sum = d_solver.mkTerm(ADD, {f_x, f_y}); + Term p_0 = d_solver.mkTerm(APPLY_UF, {p, zero}); + Term p_f_y = d_solver.mkTerm(APPLY_UF, {p, f_y}); + d_solver.assertFormula(d_solver.mkTerm(GT, {zero, f_x})); + d_solver.assertFormula(d_solver.mkTerm(GT, {zero, f_y})); + d_solver.assertFormula(d_solver.mkTerm(GT, {sum, one})); d_solver.assertFormula(p_0); d_solver.assertFormula(p_f_y.notTerm()); ASSERT_TRUE(d_solver.checkSat().isUnsat()); @@ -1686,8 +1691,8 @@ TEST_F(TestApiBlackSolver, getDifficulty3) Term x = d_solver.mkConst(intSort, "x"); Term zero = d_solver.mkInteger(0); Term ten = d_solver.mkInteger(10); - Term f0 = d_solver.mkTerm(GEQ, x, ten); - Term f1 = d_solver.mkTerm(GEQ, zero, x); + Term f0 = d_solver.mkTerm(GEQ, {x, ten}); + Term f1 = d_solver.mkTerm(GEQ, {zero, x}); d_solver.assertFormula(f0); d_solver.assertFormula(f1); d_solver.checkSat(); @@ -1718,9 +1723,9 @@ TEST_F(TestApiBlackSolver, getLearnedLiterals2) Term y = d_solver.mkConst(intSort, "y"); Term zero = d_solver.mkInteger(0); Term ten = d_solver.mkInteger(10); - Term f0 = d_solver.mkTerm(GEQ, x, ten); + Term f0 = d_solver.mkTerm(GEQ, {x, ten}); Term f1 = d_solver.mkTerm( - OR, d_solver.mkTerm(GEQ, zero, x), d_solver.mkTerm(GEQ, y, zero)); + OR, {d_solver.mkTerm(GEQ, {zero, x}), d_solver.mkTerm(GEQ, {y, zero})}); d_solver.assertFormula(f0); d_solver.assertFormula(f1); d_solver.checkSat(); @@ -1762,15 +1767,15 @@ TEST_F(TestApiBlackSolver, getValue3) Term p = d_solver.mkConst(intPredSort, "p"); Term zero = d_solver.mkInteger(0); Term one = d_solver.mkInteger(1); - Term f_x = d_solver.mkTerm(APPLY_UF, f, x); - Term f_y = d_solver.mkTerm(APPLY_UF, f, y); - Term sum = d_solver.mkTerm(ADD, f_x, f_y); - Term p_0 = d_solver.mkTerm(APPLY_UF, p, zero); - Term p_f_y = d_solver.mkTerm(APPLY_UF, p, f_y); - - d_solver.assertFormula(d_solver.mkTerm(LEQ, zero, f_x)); - d_solver.assertFormula(d_solver.mkTerm(LEQ, zero, f_y)); - d_solver.assertFormula(d_solver.mkTerm(LEQ, sum, one)); + Term f_x = d_solver.mkTerm(APPLY_UF, {f, x}); + Term f_y = d_solver.mkTerm(APPLY_UF, {f, y}); + Term sum = d_solver.mkTerm(ADD, {f_x, f_y}); + Term p_0 = d_solver.mkTerm(APPLY_UF, {p, zero}); + Term p_f_y = d_solver.mkTerm(APPLY_UF, {p, f_y}); + + d_solver.assertFormula(d_solver.mkTerm(LEQ, {zero, f_x})); + d_solver.assertFormula(d_solver.mkTerm(LEQ, {zero, f_y})); + d_solver.assertFormula(d_solver.mkTerm(LEQ, {sum, one})); d_solver.assertFormula(p_0.notTerm()); d_solver.assertFormula(p_f_y); ASSERT_TRUE(d_solver.checkSat().isSat()); @@ -1792,7 +1797,7 @@ TEST_F(TestApiBlackSolver, getModelDomainElements) Term x = d_solver.mkConst(uSort, "x"); Term y = d_solver.mkConst(uSort, "y"); Term z = d_solver.mkConst(uSort, "z"); - Term f = d_solver.mkTerm(DISTINCT, x, y, z); + Term f = d_solver.mkTerm(DISTINCT, {x, y, z}); d_solver.assertFormula(f); d_solver.checkSat(); ASSERT_NO_THROW(d_solver.getModelDomainElements(uSort)); @@ -1807,9 +1812,9 @@ TEST_F(TestApiBlackSolver, getModelDomainElements2) Sort uSort = d_solver.mkUninterpretedSort("u"); Term x = d_solver.mkVar(uSort, "x"); Term y = d_solver.mkVar(uSort, "y"); - Term eq = d_solver.mkTerm(EQUAL, x, y); - Term bvl = d_solver.mkTerm(VARIABLE_LIST, x, y); - Term f = d_solver.mkTerm(FORALL, bvl, eq); + Term eq = d_solver.mkTerm(EQUAL, {x, y}); + Term bvl = d_solver.mkTerm(VARIABLE_LIST, {x, y}); + Term f = d_solver.mkTerm(FORALL, {bvl, eq}); d_solver.assertFormula(f); d_solver.checkSat(); ASSERT_NO_THROW(d_solver.getModelDomainElements(uSort)); @@ -1826,7 +1831,7 @@ TEST_F(TestApiBlackSolver, isModelCoreSymbol) Term y = d_solver.mkConst(uSort, "y"); Term z = d_solver.mkConst(uSort, "z"); Term zero = d_solver.mkInteger(0); - Term f = d_solver.mkTerm(NOT, d_solver.mkTerm(EQUAL, x, y)); + Term f = d_solver.mkTerm(NOT, {d_solver.mkTerm(EQUAL, {x, y})}); d_solver.assertFormula(f); d_solver.checkSat(); ASSERT_TRUE(d_solver.isModelCoreSymbol(x)); @@ -1842,7 +1847,7 @@ TEST_F(TestApiBlackSolver, getModel) Term x = d_solver.mkConst(uSort, "x"); Term y = d_solver.mkConst(uSort, "y"); Term z = d_solver.mkConst(uSort, "z"); - Term f = d_solver.mkTerm(NOT, d_solver.mkTerm(EQUAL, x, y)); + Term f = d_solver.mkTerm(NOT, {d_solver.mkTerm(EQUAL, {x, y})}); d_solver.assertFormula(f); d_solver.checkSat(); std::vector sorts; @@ -1881,8 +1886,8 @@ TEST_F(TestApiBlackSolver, getQuantifierElimination) Term x = d_solver.mkVar(d_solver.getBooleanSort(), "x"); Term forall = d_solver.mkTerm(FORALL, - d_solver.mkTerm(VARIABLE_LIST, x), - d_solver.mkTerm(OR, x, d_solver.mkTerm(NOT, x))); + {d_solver.mkTerm(VARIABLE_LIST, {x}), + d_solver.mkTerm(OR, {x, d_solver.mkTerm(NOT, {x})})}); ASSERT_THROW(d_solver.getQuantifierElimination(Term()), CVC5ApiException); ASSERT_THROW(d_solver.getQuantifierElimination(Solver().mkBoolean(false)), CVC5ApiException); @@ -1894,8 +1899,8 @@ TEST_F(TestApiBlackSolver, getQuantifierEliminationDisjunct) Term x = d_solver.mkVar(d_solver.getBooleanSort(), "x"); Term forall = d_solver.mkTerm(FORALL, - d_solver.mkTerm(VARIABLE_LIST, x), - d_solver.mkTerm(OR, x, d_solver.mkTerm(NOT, x))); + {d_solver.mkTerm(VARIABLE_LIST, {x}), + d_solver.mkTerm(OR, {x, d_solver.mkTerm(NOT, {x})})}); ASSERT_THROW(d_solver.getQuantifierEliminationDisjunct(Term()), CVC5ApiException); ASSERT_THROW( @@ -1926,7 +1931,7 @@ void checkSimpleSeparationConstraints(Solver* solver) solver->declareSepHeap(integer, integer); Term x = solver->mkConst(integer, "x"); Term p = solver->mkConst(integer, "p"); - Term heap = solver->mkTerm(cvc5::api::Kind::SEP_PTO, p, x); + Term heap = solver->mkTerm(cvc5::api::Kind::SEP_PTO, {p, x}); solver->assertFormula(heap); Term nil = solver->mkSepNil(integer); solver->assertFormula(nil.eqTerm(solver->mkReal(5))); @@ -2204,11 +2209,11 @@ TEST_F(TestApiBlackSolver, simplify) ASSERT_NO_THROW(d_solver.simplify(a)); Term b = d_solver.mkConst(bvSort, "b"); ASSERT_NO_THROW(d_solver.simplify(b)); - Term x_eq_x = d_solver.mkTerm(EQUAL, x, x); + Term x_eq_x = d_solver.mkTerm(EQUAL, {x, x}); ASSERT_NO_THROW(d_solver.simplify(x_eq_x)); ASSERT_NE(d_solver.mkTrue(), x_eq_x); ASSERT_EQ(d_solver.mkTrue(), d_solver.simplify(x_eq_x)); - Term x_eq_b = d_solver.mkTerm(EQUAL, x, b); + Term x_eq_b = d_solver.mkTerm(EQUAL, {x, b}); ASSERT_NO_THROW(d_solver.simplify(x_eq_b)); ASSERT_NE(d_solver.mkTrue(), x_eq_b); ASSERT_NE(d_solver.mkTrue(), d_solver.simplify(x_eq_b)); @@ -2217,24 +2222,25 @@ TEST_F(TestApiBlackSolver, simplify) Term i1 = d_solver.mkConst(d_solver.getIntegerSort(), "i1"); ASSERT_NO_THROW(d_solver.simplify(i1)); - Term i2 = d_solver.mkTerm(MULT, i1, d_solver.mkInteger("23")); + Term i2 = d_solver.mkTerm(MULT, {i1, d_solver.mkInteger("23")}); ASSERT_NO_THROW(d_solver.simplify(i2)); ASSERT_NE(i1, i2); ASSERT_NE(i1, d_solver.simplify(i2)); - Term i3 = d_solver.mkTerm(ADD, i1, d_solver.mkInteger(0)); + Term i3 = d_solver.mkTerm(ADD, {i1, d_solver.mkInteger(0)}); ASSERT_NO_THROW(d_solver.simplify(i3)); ASSERT_NE(i1, i3); ASSERT_EQ(i1, d_solver.simplify(i3)); Datatype consList = consListSort.getDatatype(); - Term dt1 = d_solver.mkTerm( - APPLY_CONSTRUCTOR, - consList.getConstructorTerm("cons"), - d_solver.mkInteger(0), - d_solver.mkTerm(APPLY_CONSTRUCTOR, consList.getConstructorTerm("nil"))); + Term dt1 = + d_solver.mkTerm(APPLY_CONSTRUCTOR, + {consList.getConstructorTerm("cons"), + d_solver.mkInteger(0), + d_solver.mkTerm(APPLY_CONSTRUCTOR, + {consList.getConstructorTerm("nil")})}); ASSERT_NO_THROW(d_solver.simplify(dt1)); - Term dt2 = d_solver.mkTerm( - APPLY_SELECTOR, consList["cons"].getSelectorTerm("head"), dt1); + Term dt2 = d_solver.mkTerm(APPLY_SELECTOR, + {consList["cons"].getSelectorTerm("head"), dt1}); ASSERT_NO_THROW(d_solver.simplify(dt2)); Term b1 = d_solver.mkVar(bvSort, "b1"); @@ -2285,7 +2291,7 @@ TEST_F(TestApiBlackSolver, checkSatAssuming1) Sort boolSort = d_solver.getBooleanSort(); Term x = d_solver.mkConst(boolSort, "x"); Term y = d_solver.mkConst(boolSort, "y"); - Term z = d_solver.mkTerm(AND, x, y); + Term z = d_solver.mkTerm(AND, {x, y}); d_solver.setOption("incremental", "true"); ASSERT_NO_THROW(d_solver.checkSatAssuming(d_solver.mkTrue())); ASSERT_THROW(d_solver.checkSatAssuming(Term()), CVC5ApiException); @@ -2316,30 +2322,31 @@ TEST_F(TestApiBlackSolver, checkSatAssuming2) Term zero = d_solver.mkInteger(0); Term one = d_solver.mkInteger(1); // Terms - Term f_x = d_solver.mkTerm(APPLY_UF, f, x); - Term f_y = d_solver.mkTerm(APPLY_UF, f, y); - Term sum = d_solver.mkTerm(ADD, f_x, f_y); - Term p_0 = d_solver.mkTerm(APPLY_UF, p, zero); - Term p_f_y = d_solver.mkTerm(APPLY_UF, p, f_y); + Term f_x = d_solver.mkTerm(APPLY_UF, {f, x}); + Term f_y = d_solver.mkTerm(APPLY_UF, {f, y}); + Term sum = d_solver.mkTerm(ADD, {f_x, f_y}); + Term p_0 = d_solver.mkTerm(APPLY_UF, {p, zero}); + Term p_f_y = d_solver.mkTerm(APPLY_UF, {p, f_y}); // Assertions Term assertions = d_solver.mkTerm(AND, - std::vector{ - d_solver.mkTerm(LEQ, zero, f_x), // 0 <= f(x) - d_solver.mkTerm(LEQ, zero, f_y), // 0 <= f(y) - d_solver.mkTerm(LEQ, sum, one), // f(x) + f(y) <= 1 - p_0.notTerm(), // not p(0) - p_f_y // p(f(y)) + { + d_solver.mkTerm(LEQ, {zero, f_x}), // 0 <= f(x) + d_solver.mkTerm(LEQ, {zero, f_y}), // 0 <= f(y) + d_solver.mkTerm(LEQ, {sum, one}), // f(x) + f(y) <= 1 + p_0.notTerm(), // not p(0) + p_f_y // p(f(y)) }); ASSERT_NO_THROW(d_solver.checkSatAssuming(d_solver.mkTrue())); d_solver.assertFormula(assertions); - ASSERT_NO_THROW(d_solver.checkSatAssuming(d_solver.mkTerm(DISTINCT, x, y))); + ASSERT_NO_THROW(d_solver.checkSatAssuming(d_solver.mkTerm(DISTINCT, {x, y}))); ASSERT_NO_THROW(d_solver.checkSatAssuming( - {d_solver.mkFalse(), d_solver.mkTerm(DISTINCT, x, y)})); + {d_solver.mkFalse(), d_solver.mkTerm(DISTINCT, {x, y})})); ASSERT_THROW(d_solver.checkSatAssuming(n), CVC5ApiException); - ASSERT_THROW(d_solver.checkSatAssuming({n, d_solver.mkTerm(DISTINCT, x, y)}), - CVC5ApiException); + ASSERT_THROW( + d_solver.checkSatAssuming({n, d_solver.mkTerm(DISTINCT, {x, y})}), + CVC5ApiException); Solver slv; ASSERT_THROW(slv.checkSatAssuming(d_solver.mkTrue()), CVC5ApiException); } @@ -2368,10 +2375,10 @@ TEST_F(TestApiBlackSolver, resetAssertions) Sort bvSort = d_solver.mkBitVectorSort(4); Term one = d_solver.mkBitVector(4, 1); Term x = d_solver.mkConst(bvSort, "x"); - Term ule = d_solver.mkTerm(BITVECTOR_ULE, x, one); - Term srem = d_solver.mkTerm(BITVECTOR_SREM, one, x); + Term ule = d_solver.mkTerm(BITVECTOR_ULE, {x, one}); + Term srem = d_solver.mkTerm(BITVECTOR_SREM, {one, x}); d_solver.push(4); - Term slt = d_solver.mkTerm(BITVECTOR_SLT, srem, one); + Term slt = d_solver.mkTerm(BITVECTOR_SLT, {srem, one}); d_solver.resetAssertions(); d_solver.checkSatAssuming({slt, ule}); } @@ -2660,7 +2667,7 @@ TEST_F(TestApiBlackSolver, tupleProject) d_solver.mkBoolean(true), d_solver.mkInteger(3), d_solver.mkString("C"), - d_solver.mkTerm(SET_SINGLETON, d_solver.mkString("Z"))}; + d_solver.mkTerm(SET_SINGLETON, {d_solver.mkString("Z")})}; Term tuple = d_solver.mkTuple(sorts, elements); @@ -2672,23 +2679,23 @@ TEST_F(TestApiBlackSolver, tupleProject) std::vector indices6 = {0, 4}; ASSERT_NO_THROW( - d_solver.mkTerm(d_solver.mkOp(TUPLE_PROJECT, indices1), tuple)); + d_solver.mkTerm(d_solver.mkOp(TUPLE_PROJECT, indices1), {tuple})); ASSERT_NO_THROW( - d_solver.mkTerm(d_solver.mkOp(TUPLE_PROJECT, indices2), tuple)); + d_solver.mkTerm(d_solver.mkOp(TUPLE_PROJECT, indices2), {tuple})); ASSERT_NO_THROW( - d_solver.mkTerm(d_solver.mkOp(TUPLE_PROJECT, indices3), tuple)); + d_solver.mkTerm(d_solver.mkOp(TUPLE_PROJECT, indices3), {tuple})); ASSERT_NO_THROW( - d_solver.mkTerm(d_solver.mkOp(TUPLE_PROJECT, indices4), tuple)); + d_solver.mkTerm(d_solver.mkOp(TUPLE_PROJECT, indices4), {tuple})); - ASSERT_THROW(d_solver.mkTerm(d_solver.mkOp(TUPLE_PROJECT, indices5), tuple), + ASSERT_THROW(d_solver.mkTerm(d_solver.mkOp(TUPLE_PROJECT, indices5), {tuple}), CVC5ApiException); - ASSERT_THROW(d_solver.mkTerm(d_solver.mkOp(TUPLE_PROJECT, indices6), tuple), + ASSERT_THROW(d_solver.mkTerm(d_solver.mkOp(TUPLE_PROJECT, indices6), {tuple}), CVC5ApiException); std::vector indices = {0, 3, 2, 0, 1, 2}; Op op = d_solver.mkOp(TUPLE_PROJECT, indices); - Term projection = d_solver.mkTerm(op, tuple); + Term projection = d_solver.mkTerm(op, {tuple}); Datatype datatype = tuple.getSort().getDatatype(); DatatypeConstructor constructor = datatype[0]; @@ -2696,7 +2703,7 @@ TEST_F(TestApiBlackSolver, tupleProject) for (size_t i = 0; i < indices.size(); i++) { Term selectorTerm = constructor[indices[i]].getSelectorTerm(); - Term selectedTerm = d_solver.mkTerm(APPLY_SELECTOR, selectorTerm, tuple); + Term selectedTerm = d_solver.mkTerm(APPLY_SELECTOR, {selectorTerm, tuple}); Term simplifiedTerm = d_solver.simplify(selectedTerm); ASSERT_EQ(elements[indices[i]], simplifiedTerm); } @@ -2727,8 +2734,8 @@ TEST_F(TestApiBlackSolver, issue7000) Term t7 = d_solver.mkConst(s3, "_x5"); Term t37 = d_solver.mkConst(s2, "_x32"); Term t59 = d_solver.mkConst(s2, "_x51"); - Term t72 = d_solver.mkTerm(EQUAL, t37, t59); - Term t74 = d_solver.mkTerm(GT, t4, t7); + Term t72 = d_solver.mkTerm(EQUAL, {t37, t59}); + Term t74 = d_solver.mkTerm(GT, {t4, t7}); Term query = d_solver.mkTerm(AND, {t72, t74, t72, t72}); // throws logic exception since logic is not higher order by default ASSERT_THROW(d_solver.checkSatAssuming(query.notTerm()), CVC5ApiException); @@ -2743,8 +2750,8 @@ TEST_F(TestApiBlackSolver, issue5893) Term arr = d_solver.mkConst(arrsort, "arr"); Term idx = d_solver.mkConst(bvsort4, "idx"); Term ten = d_solver.mkBitVector(8, "10", 10); - Term sel = d_solver.mkTerm(SELECT, arr, idx); - Term distinct = d_solver.mkTerm(DISTINCT, sel, ten); + Term sel = d_solver.mkTerm(SELECT, {arr, idx}); + Term distinct = d_solver.mkTerm(DISTINCT, {sel, ten}); ASSERT_NO_FATAL_FAILURE(distinct.getOp()); } @@ -2754,7 +2761,7 @@ TEST_F(TestApiBlackSolver, proj_issue308) slv.setOption("check-proofs", "true"); Sort s1 = slv.getBooleanSort(); Term t1 = slv.mkConst(s1, "_x0"); - Term t2 = slv.mkTerm(Kind::XOR, t1, t1); + Term t2 = slv.mkTerm(Kind::XOR, {t1, t1}); slv.checkSatAssuming({t2}); auto unsat_core = slv.getUnsatCore(); ASSERT_FALSE(unsat_core.empty()); @@ -2813,12 +2820,12 @@ TEST_F(TestApiBlackSolver, proj_issue378) Sort s7 = d_solver.mkDatatypeSort(dtdecl); Sort s9 = s7.instantiate({s2}); Term t1507 = d_solver.mkTerm( - APPLY_CONSTRUCTOR, s9.getDatatype().getConstructorTerm("_x184"), t7); + APPLY_CONSTRUCTOR, {s9.getDatatype().getConstructorTerm("_x184"), t7}); ASSERT_NO_THROW(d_solver.mkTerm( APPLY_UPDATER, - s9.getDatatype().getConstructor("_x186").getSelectorTerm("_x185"), - t1507, - t7)); + {s9.getDatatype().getConstructor("_x186").getSelectorTerm("_x185"), + t1507, + t7})); } TEST_F(TestApiBlackSolver, proj_issue379) @@ -2840,13 +2847,13 @@ TEST_F(TestApiBlackSolver, proj_issue379) Term t317 = d_solver.mkConst(bsort, "_x345"); Term t843 = d_solver.mkConst(s6, "_x346"); Term t879 = d_solver.mkTerm(APPLY_UPDATER, - t843.getSort() - .getDatatype() - .getConstructor("_x8") - .getSelector("_x7") - .getUpdaterTerm(), - t843, - t317); + {t843.getSort() + .getDatatype() + .getConstructor("_x8") + .getSelector("_x7") + .getUpdaterTerm(), + t843, + t317}); ASSERT_EQ(t879.getSort(), s6); } @@ -2872,13 +2879,13 @@ TEST_F(TestApiBlackSolver, proj_issue381) Term t26 = d_solver.mkConst(s6, "_x63"); Term t5 = d_solver.mkTrue(); Term t187 = d_solver.mkTerm(APPLY_UPDATER, - t26.getSort() - .getDatatype() - .getConstructor("_x22") - .getSelector("_x19") - .getUpdaterTerm(), - t26, - t5); + {t26.getSort() + .getDatatype() + .getConstructor("_x22") + .getSelector("_x19") + .getUpdaterTerm(), + t26, + t5}); ASSERT_NO_THROW(d_solver.simplify(t187)); } @@ -2896,23 +2903,22 @@ TEST_F(TestApiBlackSolver, proj_issue382) Term t13 = d_solver.mkVar(s6, "_x58"); Term t18 = d_solver.mkConst(s6, "_x63"); Term t52 = d_solver.mkVar(s6, "_x70"); - Term t53 = d_solver.mkTerm( - MATCH_BIND_CASE, d_solver.mkTerm(VARIABLE_LIST, t52), t52, t18); + Term t53 = d_solver.mkTerm(MATCH_BIND_CASE, + {d_solver.mkTerm(VARIABLE_LIST, {t52}), t52, t18}); Term t73 = d_solver.mkVar(s1, "_x78"); Term t81 = d_solver.mkTerm(MATCH_BIND_CASE, - d_solver.mkTerm(VARIABLE_LIST, t73), - d_solver.mkTerm(APPLY_CONSTRUCTOR, - s6.getDatatype() - .getConstructor("_x20") - .getInstantiatedConstructorTerm(s6), - t73), - t18); + {d_solver.mkTerm(VARIABLE_LIST, {t73}), + d_solver.mkTerm(APPLY_CONSTRUCTOR, + {s6.getDatatype() + .getConstructor("_x20") + .getInstantiatedConstructorTerm(s6), + t73}), + t18}); Term t82 = d_solver.mkTerm(MATCH, {t13, t53, t53, t53, t81}); Term t325 = d_solver.mkTerm( APPLY_SELECTOR, - t82.getSort().getDatatype().getSelector("_x19").getSelectorTerm(), - t82); + {t82.getSort().getDatatype().getSelector("_x19").getSelectorTerm(), t82}); ASSERT_NO_THROW(d_solver.simplify(t325)); } @@ -3185,7 +3191,7 @@ TEST_F(TestApiBlackSolver, projIssue431) Term sel = t47.getSort().getDatatype().getConstructor("_cons64").getSelectorTerm( "_sel62"); - Term t274 = slv.mkTerm(APPLY_SELECTOR, sel, t47); + Term t274 = slv.mkTerm(APPLY_SELECTOR, {sel, t47}); Term t488 = slv.mkTerm(Kind::APPLY_UF, {t31, t274}); slv.assertFormula({t488}); Term abduct; @@ -3195,7 +3201,7 @@ TEST_F(TestApiBlackSolver, projIssue431) TEST_F(TestApiBlackSolver, projIssue337) { Term t = - d_solver.mkTerm(SEQ_UNIT, d_solver.mkReal("3416574625719121610379268")); + d_solver.mkTerm(SEQ_UNIT, {d_solver.mkReal("3416574625719121610379268")}); Term tt = d_solver.simplify(t); ASSERT_EQ(t.getSort(), tt.getSort()); } diff --git a/test/unit/api/cpp/solver_white.cpp b/test/unit/api/cpp/solver_white.cpp index 5d7b9eacf..bab2bcee0 100644 --- a/test/unit/api/cpp/solver_white.cpp +++ b/test/unit/api/cpp/solver_white.cpp @@ -42,10 +42,10 @@ TEST_F(TestApiWhiteSolver, getOp) Term consTerm = consList.getConstructorTerm("cons"); Term headTerm = consList["cons"].getSelectorTerm("head"); - Term listnil = d_solver.mkTerm(APPLY_CONSTRUCTOR, nilTerm); - Term listcons1 = d_solver.mkTerm( - APPLY_CONSTRUCTOR, consTerm, d_solver.mkInteger(1), listnil); - Term listhead = d_solver.mkTerm(APPLY_SELECTOR, headTerm, listcons1); + Term listnil = d_solver.mkTerm(APPLY_CONSTRUCTOR, {nilTerm}); + Term listcons1 = d_solver.mkTerm(APPLY_CONSTRUCTOR, + {consTerm, d_solver.mkInteger(1), listnil}); + Term listhead = d_solver.mkTerm(APPLY_SELECTOR, {headTerm, listcons1}); ASSERT_EQ(listnil.getOp(), Op(&d_solver, APPLY_CONSTRUCTOR)); ASSERT_EQ(listcons1.getOp(), Op(&d_solver, APPLY_CONSTRUCTOR)); diff --git a/test/unit/api/cpp/term_black.cpp b/test/unit/api/cpp/term_black.cpp index a4dad3718..965a935c5 100644 --- a/test/unit/api/cpp/term_black.cpp +++ b/test/unit/api/cpp/term_black.cpp @@ -76,22 +76,22 @@ TEST_F(TestApiBlackTerm, getKind) Term zero = d_solver.mkInteger(0); ASSERT_NO_THROW(zero.getKind()); - Term f_x = d_solver.mkTerm(APPLY_UF, f, x); + Term f_x = d_solver.mkTerm(APPLY_UF, {f, x}); ASSERT_NO_THROW(f_x.getKind()); - Term f_y = d_solver.mkTerm(APPLY_UF, f, y); + Term f_y = d_solver.mkTerm(APPLY_UF, {f, y}); ASSERT_NO_THROW(f_y.getKind()); - Term sum = d_solver.mkTerm(ADD, f_x, f_y); + Term sum = d_solver.mkTerm(ADD, {f_x, f_y}); ASSERT_NO_THROW(sum.getKind()); - Term p_0 = d_solver.mkTerm(APPLY_UF, p, zero); + Term p_0 = d_solver.mkTerm(APPLY_UF, {p, zero}); ASSERT_NO_THROW(p_0.getKind()); - Term p_f_y = d_solver.mkTerm(APPLY_UF, p, f_y); + Term p_f_y = d_solver.mkTerm(APPLY_UF, {p, f_y}); ASSERT_NO_THROW(p_f_y.getKind()); // Sequence kinds do not exist internally, test that the API properly // converts them back. Sort seqSort = d_solver.mkSequenceSort(intSort); Term s = d_solver.mkConst(seqSort, "s"); - Term ss = d_solver.mkTerm(SEQ_CONCAT, s, s); + Term ss = d_solver.mkTerm(SEQ_CONCAT, {s, s}); ASSERT_EQ(ss.getKind(), SEQ_CONCAT); } @@ -123,19 +123,19 @@ TEST_F(TestApiBlackTerm, getSort) ASSERT_NO_THROW(zero.getSort()); ASSERT_EQ(zero.getSort(), intSort); - Term f_x = d_solver.mkTerm(APPLY_UF, f, x); + Term f_x = d_solver.mkTerm(APPLY_UF, {f, x}); ASSERT_NO_THROW(f_x.getSort()); ASSERT_EQ(f_x.getSort(), intSort); - Term f_y = d_solver.mkTerm(APPLY_UF, f, y); + Term f_y = d_solver.mkTerm(APPLY_UF, {f, y}); ASSERT_NO_THROW(f_y.getSort()); ASSERT_EQ(f_y.getSort(), intSort); - Term sum = d_solver.mkTerm(ADD, f_x, f_y); + Term sum = d_solver.mkTerm(ADD, {f_x, f_y}); ASSERT_NO_THROW(sum.getSort()); ASSERT_EQ(sum.getSort(), intSort); - Term p_0 = d_solver.mkTerm(APPLY_UF, p, zero); + Term p_0 = d_solver.mkTerm(APPLY_UF, {p, zero}); ASSERT_NO_THROW(p_0.getSort()); ASSERT_EQ(p_0.getSort(), boolSort); - Term p_f_y = d_solver.mkTerm(APPLY_UF, p, f_y); + Term p_f_y = d_solver.mkTerm(APPLY_UF, {p, f_y}); ASSERT_NO_THROW(p_f_y.getSort()); ASSERT_EQ(p_f_y.getSort(), boolSort); } @@ -154,9 +154,9 @@ TEST_F(TestApiBlackTerm, getOp) ASSERT_FALSE(x.hasOp()); ASSERT_THROW(x.getOp(), CVC5ApiException); - Term ab = d_solver.mkTerm(SELECT, a, b); + Term ab = d_solver.mkTerm(SELECT, {a, b}); Op ext = d_solver.mkOp(BITVECTOR_EXTRACT, 4, 0); - Term extb = d_solver.mkTerm(ext, b); + Term extb = d_solver.mkTerm(ext, {b}); ASSERT_TRUE(ab.hasOp()); ASSERT_FALSE(ab.getOp().isIndexed()); @@ -166,7 +166,7 @@ TEST_F(TestApiBlackTerm, getOp) ASSERT_EQ(extb.getOp(), ext); Term f = d_solver.mkConst(funsort, "f"); - Term fx = d_solver.mkTerm(APPLY_UF, f, x); + Term fx = d_solver.mkTerm(APPLY_UF, {f, x}); ASSERT_FALSE(f.hasOp()); ASSERT_THROW(f.getOp(), CVC5ApiException); @@ -195,11 +195,11 @@ TEST_F(TestApiBlackTerm, getOp) Term headOpTerm = list["cons"].getSelectorTerm("head"); Term tailOpTerm = list["cons"].getSelectorTerm("tail"); - Term nilTerm = d_solver.mkTerm(APPLY_CONSTRUCTOR, nilOpTerm); - Term consTerm = d_solver.mkTerm( - APPLY_CONSTRUCTOR, consOpTerm, d_solver.mkInteger(0), nilTerm); - Term headTerm = d_solver.mkTerm(APPLY_SELECTOR, headOpTerm, consTerm); - Term tailTerm = d_solver.mkTerm(APPLY_SELECTOR, tailOpTerm, consTerm); + Term nilTerm = d_solver.mkTerm(APPLY_CONSTRUCTOR, {nilOpTerm}); + Term consTerm = d_solver.mkTerm(APPLY_CONSTRUCTOR, + {consOpTerm, d_solver.mkInteger(0), nilTerm}); + Term headTerm = d_solver.mkTerm(APPLY_SELECTOR, {headOpTerm, consTerm}); + Term tailTerm = d_solver.mkTerm(APPLY_SELECTOR, {tailOpTerm, consTerm}); ASSERT_TRUE(nilTerm.hasOp()); ASSERT_TRUE(consTerm.hasOp()); @@ -254,13 +254,13 @@ TEST_F(TestApiBlackTerm, notTerm) ASSERT_THROW(p.notTerm(), CVC5ApiException); Term zero = d_solver.mkInteger(0); ASSERT_THROW(zero.notTerm(), CVC5ApiException); - Term f_x = d_solver.mkTerm(APPLY_UF, f, x); + Term f_x = d_solver.mkTerm(APPLY_UF, {f, x}); ASSERT_THROW(f_x.notTerm(), CVC5ApiException); - Term sum = d_solver.mkTerm(ADD, f_x, f_x); + Term sum = d_solver.mkTerm(ADD, {f_x, f_x}); ASSERT_THROW(sum.notTerm(), CVC5ApiException); - Term p_0 = d_solver.mkTerm(APPLY_UF, p, zero); + Term p_0 = d_solver.mkTerm(APPLY_UF, {p, zero}); ASSERT_NO_THROW(p_0.notTerm()); - Term p_f_x = d_solver.mkTerm(APPLY_UF, p, f_x); + Term p_f_x = d_solver.mkTerm(APPLY_UF, {p, f_x}); ASSERT_NO_THROW(p_f_x.notTerm()); } @@ -294,14 +294,14 @@ TEST_F(TestApiBlackTerm, andTerm) ASSERT_THROW(zero.andTerm(f), CVC5ApiException); ASSERT_THROW(zero.andTerm(p), CVC5ApiException); ASSERT_THROW(zero.andTerm(zero), CVC5ApiException); - Term f_x = d_solver.mkTerm(APPLY_UF, f, x); + Term f_x = d_solver.mkTerm(APPLY_UF, {f, x}); ASSERT_THROW(f_x.andTerm(b), CVC5ApiException); ASSERT_THROW(f_x.andTerm(x), CVC5ApiException); ASSERT_THROW(f_x.andTerm(f), CVC5ApiException); ASSERT_THROW(f_x.andTerm(p), CVC5ApiException); ASSERT_THROW(f_x.andTerm(zero), CVC5ApiException); ASSERT_THROW(f_x.andTerm(f_x), CVC5ApiException); - Term sum = d_solver.mkTerm(ADD, f_x, f_x); + Term sum = d_solver.mkTerm(ADD, {f_x, f_x}); ASSERT_THROW(sum.andTerm(b), CVC5ApiException); ASSERT_THROW(sum.andTerm(x), CVC5ApiException); ASSERT_THROW(sum.andTerm(f), CVC5ApiException); @@ -309,7 +309,7 @@ TEST_F(TestApiBlackTerm, andTerm) ASSERT_THROW(sum.andTerm(zero), CVC5ApiException); ASSERT_THROW(sum.andTerm(f_x), CVC5ApiException); ASSERT_THROW(sum.andTerm(sum), CVC5ApiException); - Term p_0 = d_solver.mkTerm(APPLY_UF, p, zero); + Term p_0 = d_solver.mkTerm(APPLY_UF, {p, zero}); ASSERT_NO_THROW(p_0.andTerm(b)); ASSERT_THROW(p_0.andTerm(x), CVC5ApiException); ASSERT_THROW(p_0.andTerm(f), CVC5ApiException); @@ -318,7 +318,7 @@ TEST_F(TestApiBlackTerm, andTerm) ASSERT_THROW(p_0.andTerm(f_x), CVC5ApiException); ASSERT_THROW(p_0.andTerm(sum), CVC5ApiException); ASSERT_NO_THROW(p_0.andTerm(p_0)); - Term p_f_x = d_solver.mkTerm(APPLY_UF, p, f_x); + Term p_f_x = d_solver.mkTerm(APPLY_UF, {p, f_x}); ASSERT_NO_THROW(p_f_x.andTerm(b)); ASSERT_THROW(p_f_x.andTerm(x), CVC5ApiException); ASSERT_THROW(p_f_x.andTerm(f), CVC5ApiException); @@ -360,14 +360,14 @@ TEST_F(TestApiBlackTerm, orTerm) ASSERT_THROW(zero.orTerm(f), CVC5ApiException); ASSERT_THROW(zero.orTerm(p), CVC5ApiException); ASSERT_THROW(zero.orTerm(zero), CVC5ApiException); - Term f_x = d_solver.mkTerm(APPLY_UF, f, x); + Term f_x = d_solver.mkTerm(APPLY_UF, {f, x}); ASSERT_THROW(f_x.orTerm(b), CVC5ApiException); ASSERT_THROW(f_x.orTerm(x), CVC5ApiException); ASSERT_THROW(f_x.orTerm(f), CVC5ApiException); ASSERT_THROW(f_x.orTerm(p), CVC5ApiException); ASSERT_THROW(f_x.orTerm(zero), CVC5ApiException); ASSERT_THROW(f_x.orTerm(f_x), CVC5ApiException); - Term sum = d_solver.mkTerm(ADD, f_x, f_x); + Term sum = d_solver.mkTerm(ADD, {f_x, f_x}); ASSERT_THROW(sum.orTerm(b), CVC5ApiException); ASSERT_THROW(sum.orTerm(x), CVC5ApiException); ASSERT_THROW(sum.orTerm(f), CVC5ApiException); @@ -375,7 +375,7 @@ TEST_F(TestApiBlackTerm, orTerm) ASSERT_THROW(sum.orTerm(zero), CVC5ApiException); ASSERT_THROW(sum.orTerm(f_x), CVC5ApiException); ASSERT_THROW(sum.orTerm(sum), CVC5ApiException); - Term p_0 = d_solver.mkTerm(APPLY_UF, p, zero); + Term p_0 = d_solver.mkTerm(APPLY_UF, {p, zero}); ASSERT_NO_THROW(p_0.orTerm(b)); ASSERT_THROW(p_0.orTerm(x), CVC5ApiException); ASSERT_THROW(p_0.orTerm(f), CVC5ApiException); @@ -384,7 +384,7 @@ TEST_F(TestApiBlackTerm, orTerm) ASSERT_THROW(p_0.orTerm(f_x), CVC5ApiException); ASSERT_THROW(p_0.orTerm(sum), CVC5ApiException); ASSERT_NO_THROW(p_0.orTerm(p_0)); - Term p_f_x = d_solver.mkTerm(APPLY_UF, p, f_x); + Term p_f_x = d_solver.mkTerm(APPLY_UF, {p, f_x}); ASSERT_NO_THROW(p_f_x.orTerm(b)); ASSERT_THROW(p_f_x.orTerm(x), CVC5ApiException); ASSERT_THROW(p_f_x.orTerm(f), CVC5ApiException); @@ -426,14 +426,14 @@ TEST_F(TestApiBlackTerm, xorTerm) ASSERT_THROW(zero.xorTerm(f), CVC5ApiException); ASSERT_THROW(zero.xorTerm(p), CVC5ApiException); ASSERT_THROW(zero.xorTerm(zero), CVC5ApiException); - Term f_x = d_solver.mkTerm(APPLY_UF, f, x); + Term f_x = d_solver.mkTerm(APPLY_UF, {f, x}); ASSERT_THROW(f_x.xorTerm(b), CVC5ApiException); ASSERT_THROW(f_x.xorTerm(x), CVC5ApiException); ASSERT_THROW(f_x.xorTerm(f), CVC5ApiException); ASSERT_THROW(f_x.xorTerm(p), CVC5ApiException); ASSERT_THROW(f_x.xorTerm(zero), CVC5ApiException); ASSERT_THROW(f_x.xorTerm(f_x), CVC5ApiException); - Term sum = d_solver.mkTerm(ADD, f_x, f_x); + Term sum = d_solver.mkTerm(ADD, {f_x, f_x}); ASSERT_THROW(sum.xorTerm(b), CVC5ApiException); ASSERT_THROW(sum.xorTerm(x), CVC5ApiException); ASSERT_THROW(sum.xorTerm(f), CVC5ApiException); @@ -441,7 +441,7 @@ TEST_F(TestApiBlackTerm, xorTerm) ASSERT_THROW(sum.xorTerm(zero), CVC5ApiException); ASSERT_THROW(sum.xorTerm(f_x), CVC5ApiException); ASSERT_THROW(sum.xorTerm(sum), CVC5ApiException); - Term p_0 = d_solver.mkTerm(APPLY_UF, p, zero); + Term p_0 = d_solver.mkTerm(APPLY_UF, {p, zero}); ASSERT_NO_THROW(p_0.xorTerm(b)); ASSERT_THROW(p_0.xorTerm(x), CVC5ApiException); ASSERT_THROW(p_0.xorTerm(f), CVC5ApiException); @@ -450,7 +450,7 @@ TEST_F(TestApiBlackTerm, xorTerm) ASSERT_THROW(p_0.xorTerm(f_x), CVC5ApiException); ASSERT_THROW(p_0.xorTerm(sum), CVC5ApiException); ASSERT_NO_THROW(p_0.xorTerm(p_0)); - Term p_f_x = d_solver.mkTerm(APPLY_UF, p, f_x); + Term p_f_x = d_solver.mkTerm(APPLY_UF, {p, f_x}); ASSERT_NO_THROW(p_f_x.xorTerm(b)); ASSERT_THROW(p_f_x.xorTerm(x), CVC5ApiException); ASSERT_THROW(p_f_x.xorTerm(f), CVC5ApiException); @@ -492,14 +492,14 @@ TEST_F(TestApiBlackTerm, eqTerm) ASSERT_THROW(zero.eqTerm(f), CVC5ApiException); ASSERT_THROW(zero.eqTerm(p), CVC5ApiException); ASSERT_NO_THROW(zero.eqTerm(zero)); - Term f_x = d_solver.mkTerm(APPLY_UF, f, x); + Term f_x = d_solver.mkTerm(APPLY_UF, {f, x}); ASSERT_THROW(f_x.eqTerm(b), CVC5ApiException); ASSERT_THROW(f_x.eqTerm(x), CVC5ApiException); ASSERT_THROW(f_x.eqTerm(f), CVC5ApiException); ASSERT_THROW(f_x.eqTerm(p), CVC5ApiException); ASSERT_NO_THROW(f_x.eqTerm(zero)); ASSERT_NO_THROW(f_x.eqTerm(f_x)); - Term sum = d_solver.mkTerm(ADD, f_x, f_x); + Term sum = d_solver.mkTerm(ADD, {f_x, f_x}); ASSERT_THROW(sum.eqTerm(b), CVC5ApiException); ASSERT_THROW(sum.eqTerm(x), CVC5ApiException); ASSERT_THROW(sum.eqTerm(f), CVC5ApiException); @@ -507,7 +507,7 @@ TEST_F(TestApiBlackTerm, eqTerm) ASSERT_NO_THROW(sum.eqTerm(zero)); ASSERT_NO_THROW(sum.eqTerm(f_x)); ASSERT_NO_THROW(sum.eqTerm(sum)); - Term p_0 = d_solver.mkTerm(APPLY_UF, p, zero); + Term p_0 = d_solver.mkTerm(APPLY_UF, {p, zero}); ASSERT_NO_THROW(p_0.eqTerm(b)); ASSERT_THROW(p_0.eqTerm(x), CVC5ApiException); ASSERT_THROW(p_0.eqTerm(f), CVC5ApiException); @@ -516,7 +516,7 @@ TEST_F(TestApiBlackTerm, eqTerm) ASSERT_THROW(p_0.eqTerm(f_x), CVC5ApiException); ASSERT_THROW(p_0.eqTerm(sum), CVC5ApiException); ASSERT_NO_THROW(p_0.eqTerm(p_0)); - Term p_f_x = d_solver.mkTerm(APPLY_UF, p, f_x); + Term p_f_x = d_solver.mkTerm(APPLY_UF, {p, f_x}); ASSERT_NO_THROW(p_f_x.eqTerm(b)); ASSERT_THROW(p_f_x.eqTerm(x), CVC5ApiException); ASSERT_THROW(p_f_x.eqTerm(f), CVC5ApiException); @@ -558,14 +558,14 @@ TEST_F(TestApiBlackTerm, impTerm) ASSERT_THROW(zero.impTerm(f), CVC5ApiException); ASSERT_THROW(zero.impTerm(p), CVC5ApiException); ASSERT_THROW(zero.impTerm(zero), CVC5ApiException); - Term f_x = d_solver.mkTerm(APPLY_UF, f, x); + Term f_x = d_solver.mkTerm(APPLY_UF, {f, x}); ASSERT_THROW(f_x.impTerm(b), CVC5ApiException); ASSERT_THROW(f_x.impTerm(x), CVC5ApiException); ASSERT_THROW(f_x.impTerm(f), CVC5ApiException); ASSERT_THROW(f_x.impTerm(p), CVC5ApiException); ASSERT_THROW(f_x.impTerm(zero), CVC5ApiException); ASSERT_THROW(f_x.impTerm(f_x), CVC5ApiException); - Term sum = d_solver.mkTerm(ADD, f_x, f_x); + Term sum = d_solver.mkTerm(ADD, {f_x, f_x}); ASSERT_THROW(sum.impTerm(b), CVC5ApiException); ASSERT_THROW(sum.impTerm(x), CVC5ApiException); ASSERT_THROW(sum.impTerm(f), CVC5ApiException); @@ -573,7 +573,7 @@ TEST_F(TestApiBlackTerm, impTerm) ASSERT_THROW(sum.impTerm(zero), CVC5ApiException); ASSERT_THROW(sum.impTerm(f_x), CVC5ApiException); ASSERT_THROW(sum.impTerm(sum), CVC5ApiException); - Term p_0 = d_solver.mkTerm(APPLY_UF, p, zero); + Term p_0 = d_solver.mkTerm(APPLY_UF, {p, zero}); ASSERT_NO_THROW(p_0.impTerm(b)); ASSERT_THROW(p_0.impTerm(x), CVC5ApiException); ASSERT_THROW(p_0.impTerm(f), CVC5ApiException); @@ -582,7 +582,7 @@ TEST_F(TestApiBlackTerm, impTerm) ASSERT_THROW(p_0.impTerm(f_x), CVC5ApiException); ASSERT_THROW(p_0.impTerm(sum), CVC5ApiException); ASSERT_NO_THROW(p_0.impTerm(p_0)); - Term p_f_x = d_solver.mkTerm(APPLY_UF, p, f_x); + Term p_f_x = d_solver.mkTerm(APPLY_UF, {p, f_x}); ASSERT_NO_THROW(p_f_x.impTerm(b)); ASSERT_THROW(p_f_x.impTerm(x), CVC5ApiException); ASSERT_THROW(p_f_x.impTerm(f), CVC5ApiException); @@ -622,17 +622,17 @@ TEST_F(TestApiBlackTerm, iteTerm) Term zero = d_solver.mkInteger(0); ASSERT_THROW(zero.iteTerm(x, x), CVC5ApiException); ASSERT_THROW(zero.iteTerm(x, b), CVC5ApiException); - Term f_x = d_solver.mkTerm(APPLY_UF, f, x); + Term f_x = d_solver.mkTerm(APPLY_UF, {f, x}); ASSERT_THROW(f_x.iteTerm(b, b), CVC5ApiException); ASSERT_THROW(f_x.iteTerm(b, x), CVC5ApiException); - Term sum = d_solver.mkTerm(ADD, f_x, f_x); + Term sum = d_solver.mkTerm(ADD, {f_x, f_x}); ASSERT_THROW(sum.iteTerm(x, x), CVC5ApiException); ASSERT_THROW(sum.iteTerm(b, x), CVC5ApiException); - Term p_0 = d_solver.mkTerm(APPLY_UF, p, zero); + Term p_0 = d_solver.mkTerm(APPLY_UF, {p, zero}); ASSERT_NO_THROW(p_0.iteTerm(b, b)); ASSERT_NO_THROW(p_0.iteTerm(x, x)); ASSERT_THROW(p_0.iteTerm(x, b), CVC5ApiException); - Term p_f_x = d_solver.mkTerm(APPLY_UF, p, f_x); + Term p_f_x = d_solver.mkTerm(APPLY_UF, {p, f_x}); ASSERT_NO_THROW(p_f_x.iteTerm(b, b)); ASSERT_NO_THROW(p_f_x.iteTerm(x, x)); ASSERT_THROW(p_f_x.iteTerm(x, b), CVC5ApiException); @@ -649,8 +649,10 @@ TEST_F(TestApiBlackTerm, termAssignment) TEST_F(TestApiBlackTerm, termCompare) { Term t1 = d_solver.mkInteger(1); - Term t2 = d_solver.mkTerm(ADD, d_solver.mkInteger(2), d_solver.mkInteger(2)); - Term t3 = d_solver.mkTerm(ADD, d_solver.mkInteger(2), d_solver.mkInteger(2)); + Term t2 = + d_solver.mkTerm(ADD, {d_solver.mkInteger(2), d_solver.mkInteger(2)}); + Term t3 = + d_solver.mkTerm(ADD, {d_solver.mkInteger(2), d_solver.mkInteger(2)}); ASSERT_TRUE(t2 >= t3); ASSERT_TRUE(t2 <= t3); ASSERT_TRUE((t1 > t2) != (t1 < t2)); @@ -661,7 +663,7 @@ TEST_F(TestApiBlackTerm, termChildren) { // simple term 2+3 Term two = d_solver.mkInteger(2); - Term t1 = d_solver.mkTerm(ADD, two, d_solver.mkInteger(3)); + Term t1 = d_solver.mkTerm(ADD, {two, d_solver.mkInteger(3)}); ASSERT_EQ(t1[0], two); ASSERT_EQ(t1.getNumChildren(), 2); Term tnull; @@ -671,7 +673,7 @@ TEST_F(TestApiBlackTerm, termChildren) Sort intSort = d_solver.getIntegerSort(); Sort fsort = d_solver.mkFunctionSort(intSort, intSort); Term f = d_solver.mkConst(fsort, "f"); - Term t2 = d_solver.mkTerm(APPLY_UF, f, two); + Term t2 = d_solver.mkTerm(APPLY_UF, {f, two}); // due to our higher-order view of terms, we treat f as a child of APPLY_UF ASSERT_EQ(t2.getNumChildren(), 2); ASSERT_EQ(t2[0], f); @@ -909,7 +911,7 @@ TEST_F(TestApiBlackTerm, getUninterpretedSortValue) Sort uSort = d_solver.mkUninterpretedSort("u"); Term x = d_solver.mkConst(uSort, "x"); Term y = d_solver.mkConst(uSort, "y"); - d_solver.assertFormula(d_solver.mkTerm(EQUAL, x, y)); + d_solver.assertFormula(d_solver.mkTerm(EQUAL, {x, y})); ASSERT_TRUE(d_solver.checkSat().isSat()); Term vx = d_solver.getValue(x); Term vy = d_solver.getValue(y); @@ -962,11 +964,11 @@ TEST_F(TestApiBlackTerm, getSet) Term i2 = d_solver.mkInteger(7); Term s1 = d_solver.mkEmptySet(s); - Term s2 = d_solver.mkTerm(Kind::SET_SINGLETON, i1); - Term s3 = d_solver.mkTerm(Kind::SET_SINGLETON, i1); - Term s4 = d_solver.mkTerm(Kind::SET_SINGLETON, i2); - Term s5 = d_solver.mkTerm( - Kind::SET_UNION, s2, d_solver.mkTerm(Kind::SET_UNION, s3, s4)); + Term s2 = d_solver.mkTerm(Kind::SET_SINGLETON, {i1}); + Term s3 = d_solver.mkTerm(Kind::SET_SINGLETON, {i1}); + Term s4 = d_solver.mkTerm(Kind::SET_SINGLETON, {i2}); + Term s5 = d_solver.mkTerm(Kind::SET_UNION, + {s2, d_solver.mkTerm(Kind::SET_UNION, {s3, s4})}); ASSERT_TRUE(s1.isSetValue()); ASSERT_TRUE(s2.isSetValue()); @@ -991,11 +993,11 @@ TEST_F(TestApiBlackTerm, getSequence) Term i2 = d_solver.mkInteger(7); Term s1 = d_solver.mkEmptySequence(s); - Term s2 = d_solver.mkTerm(Kind::SEQ_UNIT, i1); - Term s3 = d_solver.mkTerm(Kind::SEQ_UNIT, i1); - Term s4 = d_solver.mkTerm(Kind::SEQ_UNIT, i2); - Term s5 = d_solver.mkTerm( - Kind::SEQ_CONCAT, s2, d_solver.mkTerm(Kind::SEQ_CONCAT, s3, s4)); + Term s2 = d_solver.mkTerm(Kind::SEQ_UNIT, {i1}); + Term s3 = d_solver.mkTerm(Kind::SEQ_UNIT, {i1}); + Term s4 = d_solver.mkTerm(Kind::SEQ_UNIT, {i2}); + Term s5 = d_solver.mkTerm(Kind::SEQ_CONCAT, + {s2, d_solver.mkTerm(Kind::SEQ_CONCAT, {s3, s4})}); ASSERT_TRUE(s1.isSequenceValue()); ASSERT_TRUE(!s2.isSequenceValue()); @@ -1020,8 +1022,8 @@ TEST_F(TestApiBlackTerm, substitute) Term x = d_solver.mkConst(d_solver.getIntegerSort(), "x"); Term one = d_solver.mkInteger(1); Term ttrue = d_solver.mkTrue(); - Term xpx = d_solver.mkTerm(ADD, x, x); - Term onepone = d_solver.mkTerm(ADD, one, one); + Term xpx = d_solver.mkTerm(ADD, {x, x}); + Term onepone = d_solver.mkTerm(ADD, {one, one}); ASSERT_EQ(xpx.substitute(x, one), onepone); ASSERT_EQ(onepone.substitute(one, x), xpx); @@ -1030,8 +1032,8 @@ TEST_F(TestApiBlackTerm, substitute) // simultaneous substitution Term y = d_solver.mkConst(d_solver.getIntegerSort(), "y"); - Term xpy = d_solver.mkTerm(ADD, x, y); - Term xpone = d_solver.mkTerm(ADD, y, one); + Term xpy = d_solver.mkTerm(ADD, {x, y}); + Term xpone = d_solver.mkTerm(ADD, {y, one}); std::vector es; std::vector rs; es.push_back(x); @@ -1082,11 +1084,11 @@ TEST_F(TestApiBlackTerm, constArray) d_solver.mkArraySort(d_solver.getRealSort(), d_solver.getRealSort()); Term zero_array = d_solver.mkConstArray(arrsort, d_solver.mkReal(0)); Term stores = d_solver.mkTerm( - STORE, zero_array, d_solver.mkReal(1), d_solver.mkReal(2)); + STORE, {zero_array, d_solver.mkReal(1), d_solver.mkReal(2)}); stores = - d_solver.mkTerm(STORE, stores, d_solver.mkReal(2), d_solver.mkReal(3)); + d_solver.mkTerm(STORE, {stores, d_solver.mkReal(2), d_solver.mkReal(3)}); stores = - d_solver.mkTerm(STORE, stores, d_solver.mkReal(4), d_solver.mkReal(5)); + d_solver.mkTerm(STORE, {stores, d_solver.mkReal(4), d_solver.mkReal(5)}); } TEST_F(TestApiBlackTerm, getSequenceValue) @@ -1102,7 +1104,7 @@ TEST_F(TestApiBlackTerm, getSequenceValue) // A seq.unit app is not a constant sequence (regardless of whether it is // applied to a constant). - Term su = d_solver.mkTerm(SEQ_UNIT, d_solver.mkReal(1)); + Term su = d_solver.mkTerm(SEQ_UNIT, {d_solver.mkReal(1)}); ASSERT_THROW(su.getSequenceValue(), CVC5ApiException); } diff --git a/test/unit/api/cpp/term_white.cpp b/test/unit/api/cpp/term_white.cpp index ace5645dc..be8e7cf08 100644 --- a/test/unit/api/cpp/term_white.cpp +++ b/test/unit/api/cpp/term_white.cpp @@ -36,16 +36,16 @@ TEST_F(TestApiWhiteTerm, getOp) Term a = d_solver.mkConst(arrsort, "a"); Term b = d_solver.mkConst(bvsort, "b"); - Term ab = d_solver.mkTerm(SELECT, a, b); + Term ab = d_solver.mkTerm(SELECT, {a, b}); Op ext = d_solver.mkOp(BITVECTOR_EXTRACT, 4, 0); - Term extb = d_solver.mkTerm(ext, b); + Term extb = d_solver.mkTerm(ext, {b}); ASSERT_EQ(ab.getOp(), Op(&d_solver, SELECT)); // can compare directly to a Kind (will invoke Op constructor) ASSERT_EQ(ab.getOp(), Op(&d_solver, SELECT)); Term f = d_solver.mkConst(funsort, "f"); - Term fx = d_solver.mkTerm(APPLY_UF, f, x); + Term fx = d_solver.mkTerm(APPLY_UF, {f, x}); ASSERT_EQ(fx.getOp(), Op(&d_solver, APPLY_UF)); // testing rebuild from op and children @@ -70,11 +70,11 @@ TEST_F(TestApiWhiteTerm, getOp) Term headOpTerm = list["cons"].getSelectorTerm("head"); Term tailOpTerm = list["cons"].getSelectorTerm("tail"); - Term nilTerm = d_solver.mkTerm(APPLY_CONSTRUCTOR, nilOpTerm); - Term consTerm = d_solver.mkTerm( - APPLY_CONSTRUCTOR, consOpTerm, d_solver.mkInteger(0), nilTerm); - Term headTerm = d_solver.mkTerm(APPLY_SELECTOR, headOpTerm, consTerm); - Term tailTerm = d_solver.mkTerm(APPLY_SELECTOR, tailOpTerm, consTerm); + Term nilTerm = d_solver.mkTerm(APPLY_CONSTRUCTOR, {nilOpTerm}); + Term consTerm = d_solver.mkTerm(APPLY_CONSTRUCTOR, + {consOpTerm, d_solver.mkInteger(0), nilTerm}); + Term headTerm = d_solver.mkTerm(APPLY_SELECTOR, {headOpTerm, consTerm}); + Term tailTerm = d_solver.mkTerm(APPLY_SELECTOR, {tailOpTerm, consTerm}); ASSERT_EQ(nilTerm.getOp(), Op(&d_solver, APPLY_CONSTRUCTOR)); ASSERT_EQ(consTerm.getOp(), Op(&d_solver, APPLY_CONSTRUCTOR)); diff --git a/test/unit/api/cpp/theory_uf_ho_black.cpp b/test/unit/api/cpp/theory_uf_ho_black.cpp index c672b12aa..ac252a27a 100644 --- a/test/unit/api/cpp/theory_uf_ho_black.cpp +++ b/test/unit/api/cpp/theory_uf_ho_black.cpp @@ -32,18 +32,18 @@ TEST_F(TestTheoryBlackUfHo, proj_issue361) d_solver.setOption("produce-models", "true"); Sort s1 = d_solver.getBooleanSort(); Term t1 = d_solver.mkConst(s1, "_x0"); - Term t145 = d_solver.mkTerm(NOT, t1); - Term t169 = d_solver.mkTerm(AND, t145, t1); + Term t145 = d_solver.mkTerm(NOT, {t1}); + Term t169 = d_solver.mkTerm(AND, {t145, t1}); Sort s4 = d_solver.mkFunctionSort({s1, s1, s1}, s1); Sort s6 = d_solver.mkBagSort(s1); Term t189 = d_solver.mkConst(s4, "_x32"); Term t200 = d_solver.mkConst(s6, "_x43"); - Term t250 = d_solver.mkTerm(BAG_COUNT, t145, t200); + Term t250 = d_solver.mkTerm(BAG_COUNT, {t145, t200}); Term t367 = d_solver.mkTerm(APPLY_UF, {t189, t1, t169, t1}); d_solver.checkSatAssuming({t145, t367, t145, t145, t145}); Term v = d_solver.getValue(t250); ASSERT_TRUE( - d_solver.checkSatAssuming(d_solver.mkTerm(EQUAL, t250, v)).isSat()); + d_solver.checkSatAssuming(d_solver.mkTerm(EQUAL, {t250, v})).isSat()); } } // namespace test diff --git a/test/unit/theory/theory_sets_type_rules_white.cpp b/test/unit/theory/theory_sets_type_rules_white.cpp index f5ca53451..de668b3a3 100644 --- a/test/unit/theory/theory_sets_type_rules_white.cpp +++ b/test/unit/theory/theory_sets_type_rules_white.cpp @@ -48,17 +48,17 @@ TEST_F(TestTheoryWhiteSetsTypeRuleApi, singleton_term) Term emptyReal = d_solver.mkEmptySet(d_solver.mkSetSort(realSort)); Term integerOne = d_solver.mkInteger(1); Term realOne = d_solver.mkReal(1); - Term singletonInt = d_solver.mkTerm(api::SET_SINGLETON, integerOne); - Term singletonReal = d_solver.mkTerm(api::SET_SINGLETON, realOne); + Term singletonInt = d_solver.mkTerm(api::SET_SINGLETON, {integerOne}); + Term singletonReal = d_solver.mkTerm(api::SET_SINGLETON, {realOne}); // (union // (singleton (singleton_op Int) 1) // (as emptyset (Set Real))) - ASSERT_THROW(d_solver.mkTerm(SET_UNION, singletonInt, emptyReal), + ASSERT_THROW(d_solver.mkTerm(SET_UNION, {singletonInt, emptyReal}), CVC5ApiException); // (union // (singleton (singleton_op Real) 1) // (as emptyset (Set Real))) - ASSERT_NO_THROW(d_solver.mkTerm(SET_UNION, singletonReal, emptyReal)); + ASSERT_NO_THROW(d_solver.mkTerm(SET_UNION, {singletonReal, emptyReal})); } TEST_F(TestTheoryWhiteSetsTypeRuleInternal, singleton_node) -- 2.30.2