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);
// 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;
// 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;
// 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;
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<Term> 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);
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<Term> 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);
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<Term>{
- 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;
// 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 "
// 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
// 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
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;
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;
// (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());
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());
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;
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());
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: "
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;
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);
// 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.
// 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();
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);
// 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);
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;
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;
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;
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);
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});
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())
// 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});
// 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())
// (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});
// 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);
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;
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);
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);
/* 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<Term>{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<Term>{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<Term>{child1, child2, child3});
- ////////
- CVC5_API_TRY_CATCH_END;
-}
-
Term Solver::mkTerm(Kind kind, const std::vector<Term>& children) const
{
CVC5_API_TRY_CATCH_BEGIN;
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<Term>{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<Term>{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<Term>{child1, child2, child3});
- ////////
- CVC5_API_TRY_CATCH_END;
-}
-
Term Solver::mkTerm(const Op& op, const std::vector<Term>& children) const
{
CVC5_API_TRY_CATCH_BEGIN;
/* 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<Term>& 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<Term>& children = {}) const;
/**
* Create n-ary term of given kind from a given operator.
* @param children the children of the term
* @return the Term
*/
- Term mkTerm(const Op& op, const std::vector<Term>& children) const;
+ Term mkTerm(const Op& op, const std::vector<Term>& children = {}) const;
/**
* Create a tuple term. Terms are automatically converted if sorts are
Solver* solver = reinterpret_cast<Solver*>(pointer);
Kind kind = (Kind)kindValue;
Term* child = reinterpret_cast<Term*>(childPointer);
- Term* termPointer = new Term(solver->mkTerm(kind, *child));
+ Term* termPointer = new Term(solver->mkTerm(kind, {*child}));
return reinterpret_cast<jlong>(termPointer);
CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
}
Kind kind = (Kind)kindValue;
Term* child1 = reinterpret_cast<Term*>(child1Pointer);
Term* child2 = reinterpret_cast<Term*>(child2Pointer);
- Term* termPointer = new Term(solver->mkTerm(kind, *child1, *child2));
+ Term* termPointer = new Term(solver->mkTerm(kind, {*child1, *child2}));
return reinterpret_cast<jlong>(termPointer);
CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
}
Term* child1 = reinterpret_cast<Term*>(child1Pointer);
Term* child2 = reinterpret_cast<Term*>(child2Pointer);
Term* child3 = reinterpret_cast<Term*>(child3Pointer);
- Term* retPointer = new Term(solver->mkTerm(kind, *child1, *child2, *child3));
+ Term* retPointer =
+ new Term(solver->mkTerm(kind, {*child1, *child2, *child3}));
return reinterpret_cast<jlong>(retPointer);
CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
}
Solver* solver = reinterpret_cast<Solver*>(pointer);
Op* op = reinterpret_cast<Op*>(opPointer);
Term* child = reinterpret_cast<Term*>(childPointer);
- Term* retPointer = new Term(solver->mkTerm(*op, *child));
+ Term* retPointer = new Term(solver->mkTerm(*op, {*child}));
return reinterpret_cast<jlong>(retPointer);
CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
}
Op* op = reinterpret_cast<Op*>(opPointer);
Term* child1 = reinterpret_cast<Term*>(child1Pointer);
Term* child2 = reinterpret_cast<Term*>(child2Pointer);
- Term* retPointer = new Term(solver->mkTerm(*op, *child1, *child2));
+ Term* retPointer = new Term(solver->mkTerm(*op, {*child1, *child2}));
return reinterpret_cast<jlong>(retPointer);
CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
}
Term* child1 = reinterpret_cast<Term*>(child1Pointer);
Term* child2 = reinterpret_cast<Term*>(child2Pointer);
Term* child3 = reinterpret_cast<Term*>(child3Pointer);
- Term* retPointer = new Term(solver->mkTerm(*op, *child1, *child2, *child3));
+ Term* retPointer = new Term(solver->mkTerm(*op, {*child1, *child2, *child3}));
return reinterpret_cast<jlong>(retPointer);
CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
}
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;
}
{
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;
}
#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 */
{
std::vector<uint32_t> 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; }
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;
<< 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;
}
}
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;
#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 */
#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 */
}
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)
{
// 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);
// 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;
}
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:
{
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)
// 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();
std::vector<api::Term> 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&)
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;
}
{
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());
vector<Term> 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);
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<Term> 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;
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});
}
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);
}
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;
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;
}
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);
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);
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);
}
{
// 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);
}
// 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);
}
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. */
{
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)
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)
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()); }
// 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<Term>& 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();
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<Term>& 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)
// (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());
}
// (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());
}
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());
}
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};
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
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);
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);
}
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();
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);
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();
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);
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());
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());
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();
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();
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());
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));
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));
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));
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<Sort> sorts;
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);
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(
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)));
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));
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");
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);
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<Term>{
- 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);
}
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});
}
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);
std::vector<uint32_t> 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<uint32_t> 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];
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);
}
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);
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());
}
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());
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)
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);
}
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));
}
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));
}
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;
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());
}
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));
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);
}
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);
}
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());
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);
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());
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());
}
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);
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);
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);
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);
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);
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);
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);
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);
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);
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);
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);
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);
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);
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);
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);
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);
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));
{
// 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;
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);
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);
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());
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());
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);
// 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<Term> es;
std::vector<Term> rs;
es.push_back(x);
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)
// 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);
}
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
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));
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
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)
projects / cvc5.git / commitdiff