Term two = slv.mkInteger(2);
Term twox = slv.mkTerm(Kind.MULT, two, x);
- Term twox_plus_y = slv.mkTerm(Kind.PLUS, twox, y);
+ 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);
// Terms
Term f_x = slv.mkTerm(APPLY_UF, f, x);
Term f_y = slv.mkTerm(APPLY_UF, f, y);
- Term sum = slv.mkTerm(PLUS, f_x, 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 one = solver.mkReal(1);
// Next, we construct the term x + y
- Term xPlusY = solver.mkTerm(PLUS, 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 PLUS, LEQ, and LT.
+ // 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);
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(PLUS, a, b), solver.mkInteger(1)));
+ 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.
Term zero = slv.mkInteger(0);
Term one = slv.mkInteger(1);
- Term plus = slv.mkTerm(PLUS, 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);
// (constraint (= (+ (max x y) (min x y))
// (+ x y)))
slv.addSygusConstraint(slv.mkTerm(
- EQUAL, slv.mkTerm(PLUS, max_x_y, min_x_y), slv.mkTerm(PLUS, varX, varY)));
+ 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(PLUS, x, start);
+ Term plus = slv.mkTerm(ADD, x, start);
// create the grammar object
Grammar g1 = slv.mkSygusGrammar({x}, {start});
// (ite (< x 10) (= xp (+ x 1)) (= xp x))
Term ite = slv.mkTerm(ITE,
slv.mkTerm(LT, x, ten),
- slv.mkTerm(EQUAL, xp, slv.mkTerm(PLUS, x, one)),
+ slv.mkTerm(EQUAL, xp, slv.mkTerm(ADD, x, one)),
slv.mkTerm(EQUAL, xp, x));
// define the pre-conditions, transition relations, and post-conditions
// Terms
Term f_x = slv.mkTerm(Kind.APPLY_UF, f, x);
Term f_y = slv.mkTerm(Kind.APPLY_UF, f, y);
- Term sum = slv.mkTerm(Kind.PLUS, f_x, f_y);
+ Term sum = slv.mkTerm(Kind.ADD, f_x, f_y);
Term p_0 = slv.mkTerm(Kind.APPLY_UF, p, zero);
Term p_f_y = slv.mkTerm(Kind.APPLY_UF, p, f_y);
Term one = solver.mkReal(1);
// Next, we construct the term x + y
- Term xPlusY = solver.mkTerm(Kind.PLUS, x, y);
+ Term xPlusY = solver.mkTerm(Kind.ADD, x, y);
// Now we can define the constraints.
// They use the operators +, <=, and <.
- // In the API, these are denoted by PLUS, LEQ, and LT.
+ // 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(Kind.LT, zero, x);
solver.assertFormula(solver.mkTerm(Kind.LT, solver.mkInteger(0), a));
solver.assertFormula(solver.mkTerm(Kind.LT, solver.mkInteger(0), b));
solver.assertFormula(
- solver.mkTerm(Kind.LT, solver.mkTerm(Kind.PLUS, a, b), solver.mkInteger(1)));
+ solver.mkTerm(Kind.LT, solver.mkTerm(Kind.ADD, a, b), solver.mkInteger(1)));
solver.assertFormula(solver.mkTerm(Kind.LEQ, a, b));
// We check whether the revised assertion is satisfiable.
Term zero = slv.mkInteger(0);
Term one = slv.mkInteger(1);
- Term plus = slv.mkTerm(PLUS, 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);
// (constraint (= (+ (max x y) (min x y))
// (+ x y)))
slv.addSygusConstraint(
- slv.mkTerm(EQUAL, slv.mkTerm(PLUS, max_x_y, min_x_y), slv.mkTerm(PLUS, varX, varY)));
+ slv.mkTerm(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(PLUS, x, start);
+ Term plus = slv.mkTerm(ADD, x, start);
// create the grammar object
Grammar g1 = slv.mkSygusGrammar(new Term[] {x}, new Term[] {start});
// (ite (< x 10) (= xp (+ x 1)) (= xp x))
Term ite = slv.mkTerm(ITE,
slv.mkTerm(LT, x, ten),
- slv.mkTerm(EQUAL, xp, slv.mkTerm(PLUS, x, one)),
+ slv.mkTerm(EQUAL, xp, slv.mkTerm(ADD, x, one)),
slv.mkTerm(EQUAL, xp, x));
// define the pre-conditions, transition relations, and post-conditions
# Terms
f_x = slv.mkTerm(Kind.ApplyUf, f, x)
f_y = slv.mkTerm(Kind.ApplyUf, f, y)
- sum_ = slv.mkTerm(Kind.Plus, f_x, f_y)
+ sum_ = slv.mkTerm(Kind.Add, f_x, f_y)
p_0 = slv.mkTerm(Kind.ApplyUf, p, zero)
p_f_y = slv.mkTerm(Kind.ApplyUf, p, f_y)
one = solver.mkReal(1);
# Next, we construct the term x + y
- xPlusY = solver.mkTerm(Kind.Plus, x, y);
+ xPlusY = solver.mkTerm(Kind.Add, x, y);
# Now we can define the constraints.
# They use the operators +, <=, and <.
solver.assertFormula(solver.mkTerm(Kind.Lt, solver.mkInteger(0), a));
solver.assertFormula(solver.mkTerm(Kind.Lt, solver.mkInteger(0), b));
solver.assertFormula(
- solver.mkTerm(Kind.Lt, solver.mkTerm(Kind.Plus, a, b), solver.mkInteger(1)));
+ solver.mkTerm(Kind.Lt, solver.mkTerm(Kind.Add, a, b), solver.mkInteger(1)));
solver.assertFormula(solver.mkTerm(Kind.Leq, a, b));
# We check whether the revised assertion is satisfiable.
zero = slv.mkInteger(0)
one = slv.mkInteger(1)
- plus = slv.mkTerm(Kind.Plus, start, start)
+ plus = slv.mkTerm(Kind.Add, start, start)
minus = slv.mkTerm(Kind.Sub, start, start)
ite = slv.mkTerm(Kind.Ite, start_bool, start, start)
# (constraint (= (+ (max x y) (min x y))
# (+ x y)))
slv.addSygusConstraint(slv.mkTerm(
- Kind.Equal, slv.mkTerm(Kind.Plus, max_x_y, min_x_y), slv.mkTerm(Kind.Plus, varX, varY)))
+ Kind.Equal, slv.mkTerm(Kind.Add, max_x_y, min_x_y), slv.mkTerm(Kind.Add, varX, varY)))
# print solutions if available
if (slv.checkSynth().isUnsat()):
# define the rules
zero = slv.mkInteger(0)
neg_x = slv.mkTerm(Kind.Neg, x)
- plus = slv.mkTerm(Kind.Plus, x, start)
+ plus = slv.mkTerm(Kind.Add, x, start)
# create the grammar object
g1 = slv.mkSygusGrammar({x}, {start})
# (ite (< x 10) (= xp (+ x 1)) (= xp x))
ite = slv.mkTerm(Kind.Ite,
slv.mkTerm(Kind.Lt, x, ten),
- slv.mkTerm(Kind.Equal, xp, slv.mkTerm(Kind.Plus, x, one)),
+ slv.mkTerm(Kind.Equal, xp, slv.mkTerm(Kind.Add, x, one)),
slv.mkTerm(Kind.Equal, xp, x))
# define the pre-conditions, transition relations, and post-conditions
} else {
switch (term.getKind()) {
- case kind::PLUS:
+ case kind::ADD:
cout << "(";
first = true;
for (unsigned i = 0; i < n; ++ i) {
} else {
switch (term.getKind()) {
- case kind::PLUS:
+ case kind::ADD:
cout << "(";
first = true;
for (unsigned i = 0; i < n; ++ i) {
} else {
switch (term.getKind()) {
- case kind::PLUS:
+ case kind::ADD:
cout << "(";
first = true;
for (unsigned i = 0; i < n; ++ i) {
} else {
switch (term.getKind()) {
- case kind::PLUS:
+ case kind::ADD:
cout << "(";
first = true;
for (unsigned i = 0; i < n; ++ i) {
Term two = slv.mkInteger(2);
Term twox = slv.mkTerm(Kind::MULT, two, x);
- Term twox_plus_y = slv.mkTerm(Kind::PLUS, twox, y);
+ 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);
{CARDINALITY_CONSTRAINT, cvc5::Kind::CARDINALITY_CONSTRAINT},
{HO_APPLY, cvc5::Kind::HO_APPLY},
/* Arithmetic ---------------------------------------------------------- */
- {PLUS, cvc5::Kind::PLUS},
+ {ADD, cvc5::Kind::ADD},
{MULT, cvc5::Kind::MULT},
{IAND, cvc5::Kind::IAND},
{POW2, cvc5::Kind::POW2},
{cvc5::Kind::CARDINALITY_CONSTRAINT, CARDINALITY_CONSTRAINT},
{cvc5::Kind::HO_APPLY, HO_APPLY},
/* Arithmetic ------------------------------------------------------ */
- {cvc5::Kind::PLUS, PLUS},
+ {cvc5::Kind::ADD, ADD},
{cvc5::Kind::MULT, MULT},
{cvc5::Kind::IAND, IAND},
{cvc5::Kind::POW2, POW2},
* - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const`
* - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
*/
- PLUS,
+ ADD,
/**
* Arithmetic multiplication.
*
* @param cargs the arguments of the constructor.
* It should be the case that cargs are sygus datatypes that
* encode the arguments of op. For example, a sygus constructor
- * with op = PLUS should be such that cargs.size()>=2 and
+ * with op = ADD should be such that cargs.size()>=2 and
* the sygus type of cargs[i] is Real/Int for each i.
* @param weight denotes the value added by the constructor when computing the
* size of datatype terms. Passing a value < 0 denotes the default weight for
case kind::AND:
case kind::OR:
case kind::MULT:
- case kind::PLUS:
- return true;
+ case kind::ADD: return true;
default:
return false;
case OR: nullTerm = nm->mkConst(false); break;
case AND:
case SEP_STAR: nullTerm = nm->mkConst(true); break;
- case PLUS: nullTerm = nm->mkConstRealOrInt(tn, Rational(0)); break;
+ case ADD: nullTerm = nm->mkConstRealOrInt(tn, Rational(0)); break;
case MULT:
case NONLINEAR_MULT:
nullTerm = nm->mkConstRealOrInt(tn, Rational(1));
* Returns the iterator pointing to the first child, if the node's
* kind is the same as the parameter, otherwise returns the iterator
* pointing to the node itself. This is useful if you want to
- * pretend to iterate over a "unary" PLUS, for instance, since unary
- * PLUSes don't exist---begin(PLUS) will give an iterator over the
- * children if the node's a PLUS node, otherwise give an iterator
- * over the node itself, as if it were a unary PLUS.
+ * pretend to iterate over a "unary" ADD, for instance, since unary
+ * PLUSes don't exist---begin(ADD) will give an iterator over the
+ * children if the node's an ADD node, otherwise give an iterator
+ * over the node itself, as if it were a unary ADD.
* @param kind the kind to match
* @return the kinded_iterator iterating over this Node (if its kind
* is not the passed kind) or its children
* beyond the last one), if the node's kind is the same as the
* parameter, otherwise returns the iterator pointing to the
* one-of-the-node-itself. This is useful if you want to pretend to
- * iterate over a "unary" PLUS, for instance, since unary PLUSes
- * don't exist---begin(PLUS) will give an iterator over the children
- * if the node's a PLUS node, otherwise give an iterator over the
- * node itself, as if it were a unary PLUS.
+ * iterate over a "unary" ADD, for instance, since unary PLUSes
+ * don't exist---begin(ADD) will give an iterator over the children
+ * if the node's an ADD node, otherwise give an iterator over the
+ * node itself, as if it were a unary ADD.
* @param kind the kind to match
* @return the kinded_iterator pointing off-the-end of this Node (if
* its kind is not the passed kind) or off-the-end of its children
* Returns the iterator pointing to the first child, if the node's
* kind is the same as the parameter, otherwise returns the iterator
* pointing to the node itself. This is useful if you want to
- * pretend to iterate over a "unary" PLUS, for instance, since unary
- * PLUSes don't exist---begin(PLUS) will give an iterator over the
- * children if the node's a PLUS node, otherwise give an iterator
- * over the node itself, as if it were a unary PLUS.
+ * pretend to iterate over a "unary" ADD, for instance, since unary
+ * PLUSes don't exist---begin(ADD) will give an iterator over the
+ * children if the node's an ADD node, otherwise give an iterator
+ * over the node itself, as if it were a unary ADD.
* @param kind the kind to match
* @return the kinded_iterator iterating over this Node (if its kind
* is not the passed kind) or its children
* beyond the last one), if the node's kind is the same as the
* parameter, otherwise returns the iterator pointing to the
* one-of-the-node-itself. This is useful if you want to pretend to
- * iterate over a "unary" PLUS, for instance, since unary PLUSes
- * don't exist---begin(PLUS) will give an iterator over the children
- * if the node's a PLUS node, otherwise give an iterator over the
- * node itself, as if it were a unary PLUS.
+ * iterate over a "unary" ADD, for instance, since unary PLUSes
+ * don't exist---begin(ADD) will give an iterator over the children
+ * if the node's an ADD node, otherwise give an iterator over the
+ * node itself, as if it were a unary ADD.
* @param kind the kind to match
* @return the kinded_iterator pointing off-the-end of this Node (if
* its kind is not the passed kind) or off-the-end of its children
// equal
// we compare operators instead of kinds because different terms may have
// the same kind (both `(id x)` and `(square x)` have kind APPLY_UF)
- // since many builtin operators like `PLUS` allow arbitrary number of
+ // since many builtin operators like `ADD` allow arbitrary number of
// arguments, we also need to check if the two subterms have the same
// number of children
if (curr.first.getNumChildren() != curr.second.getNumChildren()
/**
* A set of operator singletons (w.r.t. to this NodeManager
* instance) for operators. Conceptually, Nodes with kind, say,
- * PLUS, are APPLYs of a PLUS operator to arguments. This array
- * holds the set of operators for these things. A PLUS operator is
+ * ADD, are APPLYs of a ADD operator to arguments. This array
+ * holds the set of operators for these things. A ADD operator is
* a Node with kind "BUILTIN", and if you call
- * plusOperator->getConst<cvc5::Kind>(), you get kind::PLUS back.
+ * plusOperator->getConst<cvc5::Kind>(), you get kind::ADD back.
*/
Node d_operators[kind::LAST_KIND];
{
Kind k = n.getKind();
bool convertToRealChildren = false;
- if (k == PLUS || k == MULT || k == NONLINEAR_MULT)
+ if (k == ADD || k == MULT || k == NONLINEAR_MULT)
{
convertToRealChildren = isRealTypeStrict(n.getType());
}
*
* It should be the case that argTypes are sygus datatype types (possibly
* unresolved) that encode the arguments of the builtin operator. That is,
- * if op is the builtin PLUS operator, then argTypes could contain 2+
+ * if op is the builtin ADD operator, then argTypes could contain 2+
* sygus datatype types that encode integer.
*/
void addConstructor(Node op,
// ANTLR defines these, which is really bad!
#undef true
#undef false
+// ANTLR pulls in arpa/nameser_compat.h which defines this (again, bad!)
+#undef ADD
namespace cvc5 {
namespace parser {
Smt2::~Smt2() {}
void Smt2::addArithmeticOperators() {
- addOperator(api::PLUS, "+");
+ addOperator(api::ADD, "+");
addOperator(api::SUB, "-");
// api::SUB is converted to api::NEG if there is only a single operand
Parser::addOperator(api::NEG);
}
| '$sum'
{
- p.d_kind = api::PLUS;
+ p.d_kind = api::ADD;
}
| '$difference'
{
MK_TERM(api::GT, decPart, SOLVER->mkReal(1, 2)),
// if decPart > 0.5, round up
MK_TERM(api::TO_INTEGER,
- MK_TERM(api::PLUS, n, SOLVER->mkReal(1))),
+ MK_TERM(api::ADD, n, SOLVER->mkReal(1))),
// if decPart == 0.5, round to nearest even integer:
// result is: to_int(n/2 + .5) * 2
MK_TERM(api::MULT,
MK_TERM(api::TO_INTEGER,
- MK_TERM(api::PLUS,
+ MK_TERM(api::ADD,
MK_TERM(api::DIVISION,
n,
SOLVER->mkReal(2)),
result = current;
}
else if (current.getNumChildren() > 2
- && (current.getKind() == kind::PLUS
+ && (current.getKind() == kind::ADD
|| current.getKind() == kind::MULT
|| current.getKind() == kind::NONLINEAR_MULT))
{
{
switch (newKind)
{
- case kind::PLUS:
+ case kind::ADD:
Assert(children.size() == 2);
newKind = kind::BITVECTOR_ADD;
max = max + 1;
Node sum;
if (pos.getKind() == kind::AND)
{
- NodeBuilder sumb(kind::PLUS);
+ NodeBuilder sumb(kind::ADD);
for (size_t jj = 0; jj < pos.getNumChildren(); ++jj)
{
sumb << nm->mkNode(
Node ret = n;
if (n.getNumChildren() > 0)
{
- if (beneathMult && (n.getKind() == kind::PLUS || n.getKind() == kind::SUB))
+ if (beneathMult && (n.getKind() == kind::ADD || n.getKind() == kind::SUB))
{
// don't do it if it rewrites to a constant
Node nr = rewrite(n);
return false;
}
// don't bother matching on anything other than + on the left hand side
- if (l.getKind() != kind::PLUS)
+ if (l.getKind() != kind::ADD)
{
Debug("pbs::rewrites") << "not plus" << assertion << std::endl;
return false;
Node sumt =
sum.empty()
? nm->mkConstInt(Rational(0))
- : (sum.size() == 1 ? sum[0] : nm->mkNode(kind::PLUS, sum));
+ : (sum.size() == 1 ? sum[0] : nm->mkNode(kind::ADD, sum));
ret = nm->mkNode(
ret_lit.getKind(), sumt, nm->mkConstInt(Rational(0)));
if (!ret_pol)
// N-ary operators returning same type requiring at least one child to
// be unconstrained
- case kind::PLUS:
+ case kind::ADD:
case kind::SUB:
if (current.getType().isInteger() && !parent.getType().isInteger())
{
case kind::WITNESS: return "witness";
// arith theory
- case kind::PLUS: return "+";
+ case kind::ADD: return "+";
case kind::MULT:
case kind::NONLINEAR_MULT: return "*";
case kind::IAND: return "iand";
vrule = AletheRule::UNARY_MINUS_SIMPLIFY;
break;
}
- case kind::PLUS:
+ case kind::ADD:
{
vrule = AletheRule::SUM_SIMPLIFY;
break;
// check whether we are also changing the operator name, in which case
// we build a binary uninterpreted function opc
Node opc;
- if (k == PLUS || k == MULT || k == NONLINEAR_MULT)
+ if (k == ADD || k == MULT || k == NONLINEAR_MULT)
{
std::stringstream opName;
// currently allow subtyping
opName << "f_";
}
// all arithmetic kinds must explicitly deal with real vs int subtyping
- if (k == PLUS || k == MULT || k == NONLINEAR_MULT || k == GEQ || k == GT
+ if (k == ADD || k == MULT || k == NONLINEAR_MULT || k == GEQ || k == GT
|| k == LEQ || k == LT || k == SUB || k == DIVISION || k == DIVISION_TOTAL
|| k == INTS_DIVISION || k == INTS_DIVISION_TOTAL || k == INTS_MODULUS
|| k == INTS_MODULUS_TOTAL || k == NEG || k == POW)
case PfRule::ARITH_SUM_UB:
{
// proof of null terminator base 0 = 0
- Node zero = d_tproc.getNullTerminator(PLUS);
+ Node zero = d_tproc.getNullTerminator(ADD);
Node cur = zero.eqNode(zero);
cdp->addStep(cur, PfRule::REFL, {}, {zero});
for (size_t i = 0, size = children.size(); i < size; i++)
return rite;
}else{
Node constantite = rc.iteNode(d_constants[t], d_constants[e]);
- Node sum = nm->mkNode(kind::PLUS, vpite, constantite);
+ Node sum = nm->mkNode(kind::ADD, vpite, constantite);
d_reduceVar[n] = sum;
d_constants[n] = constantite;
d_varParts[n] = vpite;
bool ArithMSum::getMonomialSum(Node n, std::map<Node, Node>& msum)
{
- if (n.getKind() == PLUS)
+ if (n.getKind() == ADD)
{
for (Node nc : n)
{
children.push_back(m);
}
return children.size() > 1
- ? nm->mkNode(PLUS, children)
+ ? nm->mkNode(ADD, children)
: (children.size() == 1 ? children[0]
: nm->mkConstRealOrInt(tn, Rational(0)));
}
}
val =
children.size() > 1
- ? nm->mkNode(PLUS, children)
+ ? nm->mkNode(ADD, children)
: (children.size() == 1 ? children[0]
: nm->mkConstRealOrInt(vtn, Rational(0)));
if (!r.isOne() && !r.isNegativeOne())
visited[cur].addMonomial(null, r);
}
}
- else if (k == PLUS || k == SUB || k == NEG || k == MULT
+ else if (k == ADD || k == SUB || k == NEG || k == MULT
|| k == NONLINEAR_MULT)
{
visited[cur] = PolyNorm();
PolyNorm& ret = visited[cur];
switch (k)
{
- case PLUS:
+ case ADD:
case SUB:
case NEG:
case MULT:
bool isEqual(const PolyNorm& p) const;
/**
* Make polynomial from real term n. This method normalizes applications
- * of operators PLUS, SUB, NEG, MULT, and NONLINEAR_MULT only.
+ * of operators ADD, SUB, NEG, MULT, and NONLINEAR_MULT only.
*/
static PolyNorm mkPolyNorm(TNode n);
/** Do a and b normalize to the same polynomial? */
return RewriteResponse(REWRITE_DONE,
nm->mkConstRealOrInt(t.getType(), Rational(0)));
}
- return RewriteResponse(
- REWRITE_AGAIN_FULL,
- nm->mkNode(Kind::PLUS, t[0], makeUnaryMinusNode(t[1])));
+ return RewriteResponse(REWRITE_AGAIN_FULL,
+ nm->mkNode(Kind::ADD, t[0], makeUnaryMinusNode(t[1])));
}
RewriteResponse ArithRewriter::rewriteNeg(TNode t, bool pre)
case kind::NEG: return rewriteNeg(t, true);
case kind::DIVISION:
case kind::DIVISION_TOTAL: return rewriteDiv(t, true);
- case kind::PLUS: return preRewritePlus(t);
+ case kind::ADD: return preRewritePlus(t);
case kind::MULT:
case kind::NONLINEAR_MULT: return preRewriteMult(t);
case kind::IAND: return RewriteResponse(REWRITE_DONE, t);
case kind::NEG: return rewriteNeg(t, false);
case kind::DIVISION:
case kind::DIVISION_TOTAL: return rewriteDiv(t, false);
- case kind::PLUS: return postRewritePlus(t);
+ case kind::ADD: return postRewritePlus(t);
case kind::MULT:
case kind::NONLINEAR_MULT: return postRewriteMult(t);
case kind::IAND: return postRewriteIAnd(t);
RewriteResponse ArithRewriter::preRewritePlus(TNode t){
- Assert(t.getKind() == kind::PLUS);
+ Assert(t.getKind() == kind::ADD);
return RewriteResponse(REWRITE_DONE, expr::algorithm::flatten(t));
}
RewriteResponse ArithRewriter::postRewritePlus(TNode t){
- Assert(t.getKind() == kind::PLUS);
+ Assert(t.getKind() == kind::ADD);
Assert(t.getNumChildren() > 1);
{
}
return RewriteResponse(
REWRITE_DONE,
- nm->mkNode(Kind::PLUS, nm->mkRealAlgebraicNumber(ran), poly.getNode()));
+ nm->mkNode(Kind::ADD, nm->mkRealAlgebraicNumber(ran), poly.getNode()));
}
RewriteResponse ArithRewriter::preRewriteMult(TNode node)
return RewriteResponse(REWRITE_DONE, t);
}
}
- else if (t[0].getKind() == kind::PLUS)
+ else if (t[0].getKind() == kind::ADD)
{
std::vector<Node> product;
for (const Node tc : t[0])
//add/substract 2*pi beyond scope
Rational ra_div_two = (r_abs + rone) / rtwo;
Node new_pi_factor;
- if( r.sgn()==1 ){
+ if (r.sgn() == 1)
+ {
new_pi_factor = nm->mkConstReal(r - rtwo * ra_div_two.floor());
- }else{
+ }
+ else
+ {
Assert(r.sgn() == -1);
new_pi_factor = nm->mkConstReal(r + rtwo * ra_div_two.floor());
}
Node new_arg = nm->mkNode(kind::MULT, new_pi_factor, pi);
if (!rem.isNull())
{
- new_arg = nm->mkNode(kind::PLUS, new_arg, rem);
+ new_arg = nm->mkNode(kind::ADD, new_arg, rem);
}
// sin( 2*n*PI + x ) = sin( x )
return RewriteResponse(REWRITE_AGAIN_FULL,
// (mod (mod x c) c) --> (mod x c)
return returnRewrite(t, t[0], Rewrite::MOD_OVER_MOD);
}
- else if (k0 == kind::NONLINEAR_MULT || k0 == kind::MULT || k0 == kind::PLUS)
+ else if (k0 == kind::NONLINEAR_MULT || k0 == kind::MULT || k0 == kind::ADD)
{
// can drop all
std::vector<Node> newChildren;
if (childChanged)
{
// (mod (op ... (mod x c) ...) c) ---> (mod (op ... x ...) c) where
- // op is one of { NONLINEAR_MULT, MULT, PLUS }.
+ // op is one of { NONLINEAR_MULT, MULT, ADD }.
Node ret = nm->mkNode(k0, newChildren);
ret = nm->mkNode(kind::INTS_MODULUS_TOTAL, ret, t[1]);
return returnRewrite(t, ret, Rewrite::MOD_CHILD_MOD);
inline Node maybeUnaryConvert(NodeBuilder& builder)
{
Assert(builder.getKind() == kind::OR || builder.getKind() == kind::AND
- || builder.getKind() == kind::PLUS || builder.getKind() == kind::MULT);
+ || builder.getKind() == kind::ADD || builder.getKind() == kind::MULT);
Assert(builder.getNumChildren() >= 1);
if(builder.getNumChildren() == 1){
return builder[0];
{
switch (k)
{
- case kind::PLUS: return NodeManager::currentNM()->mkConstRealOrInt(tn, 0);
+ case kind::ADD: return NodeManager::currentNM()->mkConstRealOrInt(tn, 0);
case kind::MULT:
case kind::NONLINEAR_MULT:
return NodeManager::currentNM()->mkConstRealOrInt(tn, 1);
//We need to handle both cases seperately to ensure termination.
Node qr = SumPair::computeQR(si, a.getValue().getNumerator());
- Assert(qr.getKind() == kind::PLUS);
+ Assert(qr.getKind() == kind::ADD);
Assert(qr.getNumChildren() == 2);
SumPair q = SumPair::parseSumPair(qr[0]);
SumPair r = SumPair::parseSumPair(qr[1]);
rewriter ::cvc5::theory::arith::ArithRewriter "theory/arith/arith_rewriter.h"
-operator PLUS 2: "arithmetic addition (N-ary)"
+operator ADD 2: "arithmetic addition (N-ary)"
operator MULT 2: "arithmetic multiplication (N-ary)"
operator NONLINEAR_MULT 2: "synonym for MULT"
operator SUB 2 "arithmetic binary subtraction operator"
# This way, we avoid having 2 nested TO_REAL nodess as a result of Solver::mkTerm(TO_REAL, Solver::mkReal(int val))
operator CAST_TO_REAL 1 "cast term to real same as TO_REAL, but it is used internally, whereas TO_REAL is accessible in the API"
-typerule PLUS ::cvc5::theory::arith::ArithOperatorTypeRule
+typerule ADD ::cvc5::theory::arith::ArithOperatorTypeRule
typerule MULT ::cvc5::theory::arith::ArithOperatorTypeRule
typerule NONLINEAR_MULT ::cvc5::theory::arith::ArithOperatorTypeRule
typerule SUB ::cvc5::theory::arith::ArithOperatorTypeRule
{
continue;
}
- Node sum = nm->mkNode(Kind::PLUS, itf->second);
+ Node sum = nm->mkNode(Kind::ADD, itf->second);
sum = rewrite(sum);
Trace("nl-ext-factor")
<< "* Factored sum for " << x << " : " << sum << std::endl;
itm->second, itm->first.isNull() ? d_one : itm->first));
}
}
- Node polyn =
- poly.size() == 1 ? poly[0] : nm->mkNode(Kind::PLUS, poly);
+ Node polyn = poly.size() == 1 ? poly[0] : nm->mkNode(Kind::ADD, poly);
Trace("nl-ext-factor")
<< "...factored polynomial : " << polyn << std::endl;
Node zero = nm->mkConstRealOrInt(polyn.getType(), Rational(0));
}
else
{
- Assert(k != PLUS && k != MULT);
+ Assert(k != ADD && k != MULT);
d_m_exp[n][n] = 1;
d_m_vlist[n].push_back(n);
d_m_degree[n] = 1;
int sgn = args[5].getConst<Rational>().getNumerator().sgn();
Assert(sgn == -1 || sgn == 1);
Node tplane = nm->mkNode(Kind::SUB,
- nm->mkNode(Kind::PLUS,
+ nm->mkNode(Kind::ADD,
nm->mkNode(Kind::MULT, b, x),
nm->mkNode(Kind::MULT, a, y)),
nm->mkNode(Kind::MULT, a, b));
// tangent plane
Node tplane = nm->mkNode(Kind::SUB,
- nm->mkNode(Kind::PLUS,
+ nm->mkNode(Kind::ADD,
nm->mkNode(Kind::MULT, b_v, a),
nm->mkNode(Kind::MULT, a_v, b)),
nm->mkNode(Kind::MULT, a_v, b_v));
Node sumPart = createITEFromTable(xExtract, yExtract, granularity, table);
// append the current block to the sum
sumNode =
- nm->mkNode(kind::PLUS,
+ nm->mkNode(kind::ADD,
sumNode,
nm->mkNode(kind::MULT, pow2(i * granularity), sumPart));
}
if (cur.getType().isRealOrInt() && !cur.isConst())
{
Kind k = cur.getKind();
- if (k != MULT && k != PLUS && k != NONLINEAR_MULT
+ if (k != MULT && k != ADD && k != NONLINEAR_MULT
&& !isTranscendentalKind(k))
{
// if we have not set an approximate bound for it
Node invalid_vsum = vs_invalid.empty() ? d_zero
: (vs_invalid.size() == 1
? vs_invalid[0]
- : nm->mkNode(PLUS, vs_invalid));
+ : nm->mkNode(ADD, vs_invalid));
// substitution to try
Subs qsub;
for (const Node& v : vs)
if (it != v_b.end())
{
b = it->second;
- t = nm->mkNode(PLUS, t, nm->mkNode(MULT, b, v));
+ t = nm->mkNode(ADD, t, nm->mkNode(MULT, b, v));
}
t = rewrite(t);
Trace("nl-ext-cms-debug") << "Trying to find min/max for quadratic "
Node bound;
if (sum_bound.size() > 1)
{
- bound = nm->mkNode(kind::PLUS, sum_bound);
+ bound = nm->mkNode(kind::ADD, sum_bound);
}
else if (sum_bound.size() == 1)
{
// witness is the midpoint
witness = nm->mkNode(MULT,
nm->mkConst(CONST_RATIONAL, Rational(1, 2)),
- nm->mkNode(PLUS, l, u));
+ nm->mkNode(ADD, l, u));
witness = rewrite(witness);
Trace("nl-model") << v << " witness is " << witness << std::endl;
}
Node coeff =
nm->mkConst(CONST_RATIONAL, poly_utils::toRational(coeffs[i]));
Node term = nm->mkNode(Kind::MULT, coeff, monomial);
- res = nm->mkNode(Kind::PLUS, res, term);
+ res = nm->mkNode(Kind::ADD, res, term);
}
monomial = nm->mkNode(Kind::NONLINEAR_MULT, monomial, var);
}
denominator = poly_utils::toInteger(r.getDenominator());
return poly::UPolynomial(poly_utils::toInteger(r.getNumerator()));
}
- case Kind::PLUS:
+ case Kind::ADD:
{
poly::UPolynomial res;
poly::Integer denom;
denominator = poly_utils::toInteger(r.getDenominator());
return poly::Polynomial(poly_utils::toInteger(r.getNumerator()));
}
- case Kind::PLUS:
+ case Kind::ADD:
{
poly::Polynomial res;
poly::Integer denom;
{
return cmd.d_terms.front();
}
- return cmd.d_nm->mkNode(Kind::PLUS, cmd.d_terms);
+ return cmd.d_nm->mkNode(Kind::ADD, cmd.d_terms);
}
poly::SignCondition normalize_kind(cvc5::Kind kind,
Kind::OR,
nm->mkNode(Kind::LEQ, t[0], d_data->d_zero),
nm->mkNode(
- Kind::GT, t, nm->mkNode(Kind::PLUS, t[0], d_data->d_one)));
+ Kind::GT, t, nm->mkNode(Kind::ADD, t[0], d_data->d_one)));
CDProof* proof = nullptr;
if (d_data->isProofEnabled())
{
{
// pick c+1
bounds.second = rewrite(
- NodeManager::currentNM()->mkNode(Kind::PLUS, center, d_data->d_one));
+ NodeManager::currentNM()->mkNode(Kind::ADD, center, d_data->d_one));
}
return bounds;
}
Node mkSecant(TNode t, TNode l, TNode u, TNode evall, TNode evalu)
{
NodeManager* nm = NodeManager::currentNM();
- return nm->mkNode(Kind::PLUS,
+ return nm->mkNode(Kind::ADD,
evall,
nm->mkNode(Kind::MULT,
nm->mkNode(Kind::DIVISION,
Node e = nm->mkNode(Kind::EXPONENTIAL, args[0]);
return nm->mkNode(OR,
nm->mkNode(LEQ, args[0], zero),
- nm->mkNode(GT, e, nm->mkNode(PLUS, args[0], one)));
+ nm->mkNode(GT, e, nm->mkNode(ADD, args[0], one)));
}
else if (id == PfRule::ARITH_TRANS_EXP_ZERO)
{
nm->mkNode(Kind::LEQ, x, pi),
}),
x.eqNode(y),
- x.eqNode(
- nm->mkNode(Kind::PLUS,
- y,
- nm->mkNode(Kind::MULT, nm->mkConstReal(2), s, pi)))),
+ x.eqNode(nm->mkNode(
+ Kind::ADD,
+ y,
+ nm->mkNode(Kind::MULT, nm->mkConstReal(2), s, pi)))),
nm->mkNode(Kind::SINE, y).eqNode(nm->mkNode(Kind::SINE, x))});
}
else if (id == PfRule::ARITH_TRANS_SINE_SYMMETRY)
Assert(args[0].getType().isReal());
Node s1 = nm->mkNode(Kind::SINE, args[0]);
Node s2 = nm->mkNode(Kind::SINE, nm->mkNode(Kind::MULT, mone, args[0]));
- return nm->mkNode(PLUS, s1, s2).eqNode(zero);
+ return nm->mkNode(ADD, s1, s2).eqNode(zero);
}
else if (id == PfRule::ARITH_TRANS_SINE_TANGENT_ZERO)
{
nm->mkNode(Kind::ITE,
mkValidPhase(a[0], d_data->d_pi),
a[0].eqNode(y),
- a[0].eqNode(nm->mkNode(Kind::PLUS,
+ a[0].eqNode(nm->mkNode(Kind::ADD,
y,
nm->mkNode(Kind::MULT,
nm->mkConstReal(Rational(2)),
}
{
// sine symmetry: sin(t) - sin(-t) = 0
- Node lem = nm->mkNode(Kind::PLUS, t, symn).eqNode(d_data->d_zero);
+ Node lem = nm->mkNode(Kind::ADD, t, symn).eqNode(d_data->d_zero);
CDProof* proof = nullptr;
if (d_data->isProofEnabled())
{
proof = d_data->getProof();
Node tmplem =
- nm->mkNode(Kind::PLUS,
+ nm->mkNode(Kind::ADD,
t,
nm->mkNode(
Kind::SINE,
factorial *= counter;
varpow = nm->mkNode(Kind::MULT, d_taylor_real_fv, varpow);
}
- Node taylor_sum = (sum.size() == 1 ? sum[0] : nm->mkNode(Kind::PLUS, sum));
+ Node taylor_sum = (sum.size() == 1 ? sum[0] : nm->mkNode(Kind::ADD, sum));
Node taylor_rem =
nm->mkNode(Kind::DIVISION, varpow, nm->mkConstReal(factorial));
if (k == Kind::EXPONENTIAL)
{
pbounds.d_lower = taylor_sum;
- pbounds.d_upperNeg = nm->mkNode(Kind::PLUS, taylor_sum, ru);
+ pbounds.d_upperNeg = nm->mkNode(Kind::ADD, taylor_sum, ru);
pbounds.d_upperPos =
nm->mkNode(Kind::MULT,
taylor_sum,
- nm->mkNode(Kind::PLUS, nm->mkConstReal(Rational(1)), ru));
+ nm->mkNode(Kind::ADD, nm->mkConstReal(Rational(1)), ru));
}
else
{
Assert(k == Kind::SINE);
Node l = nm->mkNode(Kind::SUB, taylor_sum, ru);
- Node u = nm->mkNode(Kind::PLUS, taylor_sum, ru);
+ Node u = nm->mkNode(Kind::ADD, taylor_sum, ru);
pbounds.d_lower = l;
pbounds.d_upperNeg = u;
pbounds.d_upperPos = u;
Rational rcoeff = rcoeff_n.getConst<Rational>();
Assert(rcoeff.sgn() != 0);
Node res =
- nm->mkNode(Kind::PLUS,
+ nm->mkNode(Kind::ADD,
lval,
nm->mkNode(Kind::MULT,
nm->mkNode(Kind::DIVISION,
Polynomial p_q = Polynomial::mkPolynomial(q_vec);
Polynomial p_r = Polynomial::mkPolynomial(r_vec);
- return NodeManager::currentNM()->mkNode(kind::PLUS, p_q.getNode(), p_r.getNode());
+ return NodeManager::currentNM()->mkNode(
+ kind::ADD, p_q.getNode(), p_r.getNode());
}
bool Polynomial::isMember(TNode n) {
if(Monomial::isMember(n)){
return true;
- }else if(n.getKind() == kind::PLUS){
+ }
+ else if (n.getKind() == kind::ADD)
+ {
Assert(n.getNumChildren() >= 2);
Node::iterator currIter = n.begin(), end = n.end();
Node prev = *currIter;
mprev = mcurr;
}
return true;
- } else {
+ }
+ else
+ {
return false;
}
}
Integer::floorQR(constant_q, constant_r, constant, div);
Node p_qr = Polynomial::computeQR(sp.getPolynomial(), div);
- Assert(p_qr.getKind() == kind::PLUS);
+ Assert(p_qr.getKind() == kind::ADD);
Assert(p_qr.getNumChildren() == 2);
Polynomial p_q = Polynomial::parsePolynomial(p_qr[0]);
SumPair sp_q(p_q, Constant::mkConstant(constant_q));
SumPair sp_r(p_r, Constant::mkConstant(constant_r));
- return NodeManager::currentNM()->mkNode(kind::PLUS, sp_q.getNode(), sp_r.getNode());
+ return NodeManager::currentNM()->mkNode(
+ kind::ADD, sp_q.getNode(), sp_r.getNode());
}
SumPair SumPair::mkSumPair(const Polynomial& p){
static Node makePlusNode(const std::vector<Monomial>& m) {
Assert(m.size() >= 2);
- return makeNode(kind::PLUS, m.begin(), m.end());
+ return makeNode(kind::ADD, m.begin(), m.end());
}
typedef expr::NodeSelfIterator internal_iterator;
if(singleton()){
return 1;
}else{
- Assert(getNode().getKind() == kind::PLUS);
+ Assert(getNode().getKind() == kind::ADD);
return getNode().getNumChildren();
}
}
}
uint32_t numMonomials() const {
- if( getNode().getKind() == kind::PLUS ){
+ if (getNode().getKind() == kind::ADD)
+ {
return getNode().getNumChildren();
- }else if(isZero()){
+ }
+ else if (isZero())
+ {
return 0;
- }else{
+ }
+ else
+ {
return 1;
}
}
class SumPair : public NodeWrapper {
private:
static Node toNode(const Polynomial& p, const Constant& c){
- return NodeManager::currentNM()->mkNode(kind::PLUS, p.getNode(), c.getNode());
+ return NodeManager::currentNM()->mkNode(
+ kind::ADD, p.getNode(), c.getNode());
}
SumPair(TNode n) : NodeWrapper(n) { Assert(isNormalForm()); }
}
static bool isMember(TNode n) {
- if(n.getKind() == kind::PLUS && n.getNumChildren() == 2){
+ if (n.getKind() == kind::ADD && n.getNumChildren() == 2)
+ {
if(Constant::isMember(n[1])){
if(Polynomial::isMember(n[0])){
Polynomial p = Polynomial::parsePolynomial(n[0]);
}else{
return false;
}
- }else{
+ }
+ else
+ {
return false;
}
}
nm->mkNode(
LT,
num,
- nm->mkNode(
- MULT,
- den,
- nm->mkNode(PLUS, v, nm->mkConstInt(Rational(1))))));
+ nm->mkNode(MULT,
+ den,
+ nm->mkNode(ADD, v, nm->mkConstInt(Rational(1))))));
}
else
{
nm->mkNode(
MULT,
den,
- nm->mkNode(PLUS, v, nm->mkConstInt(Rational(-1))))));
+ nm->mkNode(ADD, v, nm->mkConstInt(Rational(-1))))));
}
}
else
nm->mkNode(
MULT,
den,
- nm->mkNode(
- PLUS, v, nm->mkConstInt(Rational(1))))))),
+ nm->mkNode(ADD, v, nm->mkConstInt(Rational(1))))))),
nm->mkNode(
IMPLIES,
nm->mkNode(LT, den, nm->mkConstInt(Rational(0))),
MULT,
den,
nm->mkNode(
- PLUS, v, nm->mkConstInt(Rational(-1))))))));
+ ADD, v, nm->mkConstInt(Rational(-1))))))));
}
Node intVar = mkWitnessTerm(
v, lem, "linearIntDiv", "the result of an intdiv-by-k term", lems);
// Whether a strict inequality is in the sum.
bool strict = false;
- NodeBuilder leftSum(Kind::PLUS);
- NodeBuilder rightSum(Kind::PLUS);
+ NodeBuilder leftSum(Kind::ADD);
+ NodeBuilder rightSum(Kind::ADD);
for (size_t i = 0; i < children.size(); ++i)
{
// Adjust strictness
// Whether a strict inequality is in the sum.
bool strict = false;
- NodeBuilder leftSum(Kind::PLUS);
- NodeBuilder rightSum(Kind::PLUS);
+ NodeBuilder leftSum(Kind::ADD);
+ NodeBuilder rightSum(Kind::ADD);
for (size_t i = 0; i < children.size(); ++i)
{
Rational scalar = args[i].getConst<Rational>();
// (mod (mod x c) c) --> (mod x c)
MOD_OVER_MOD,
// (mod (op ... (mod x c) ...) c) ---> (mod (op ... x ...) c) where
- // op is one of { NONLINEAR_MULT, MULT, PLUS }.
+ // op is one of { NONLINEAR_MULT, MULT, ADD }.
MOD_CHILD_MOD,
// (div (mod x c) c) --> 0
DIV_OVER_MOD,
}
}
- if(polyNode.getKind() == PLUS){
+ if (polyNode.getKind() == ADD)
+ {
d_tableauSizeHasBeenModified = true;
vector<ArithVar> variables;
/* Note:
* It is worth documenting that polyNode should only be marked as
- * being setup by this function if it has kind PLUS.
+ * being setup by this function if it has kind ADD.
* Other kinds will be marked as being setup by lower levels of setup
* specifically setupVariableList.
*/
ArithVar TheoryArithPrivate::requestArithVar(TNode x, bool aux, bool internal){
//TODO : The VarList trick is good enough?
- Assert(isLeaf(x) || VarList::isMember(x) || x.getKind() == PLUS || internal);
+ Assert(isLeaf(x) || VarList::isMember(x) || x.getKind() == ADD || internal);
if (logicInfo().isLinear() && Variable::isDivMember(x))
{
stringstream ss;
switch(k){
case kind::OR:
case kind::AND:
- case kind::PLUS:
+ case kind::ADD:
case kind::MULT:
break;
default:
{
return children[0];
}
- return nm->mkNode(kind::PLUS, children);
+ return nm->mkNode(kind::ADD, children);
}
ConstraintCP TheoryArithPrivate::vectorToIntHoleConflict(const ConstraintCPVec& conflict){
case kind::CONST_RATIONAL:
return term.getConst<Rational>();
- case kind::PLUS: { // 2+ args
+ case kind::ADD:
+ { // 2+ args
DeltaRational value(0);
for (TNode::iterator i = term.begin(), iend = term.end(); i != iend;
++i) {
void TheoryArithPrivate::entailmentCheckRowSum(std::pair<Node, DeltaRational>& tmp, int sgn, TNode tp) const {
tmp.first = Node::null();
if(sgn == 0){ return; }
- if(tp.getKind() != PLUS){ return; }
+ if (tp.getKind() != ADD)
+ {
+ return;
+ }
Assert(Polynomial::isMember(tp));
tmp.second = DeltaRational(0);
Node cardinality_0_equal = cardinality_0.eqNode(zero);
Node uf_i_multiplicity = nm->mkNode(BAG_COUNT, uf_i, A);
Node cardinality_i_equal = cardinality_i.eqNode(
- nm->mkNode(PLUS, uf_i_multiplicity, cardinality_iMinusOne));
+ nm->mkNode(ADD, uf_i_multiplicity, cardinality_iMinusOne));
Node unionDisjoint_0_equal =
unionDisjoint_0.eqNode(nm->mkConst(EmptyBag(bagType)));
Node bag = nm->mkBag(elementType, uf_i, uf_i_multiplicity);
// (bag.card (bag.union-disjoint A B)) = (+ (bag.card A) (bag.card B))
Node A = d_nm->mkNode(BAG_CARD, n[0][0]);
Node B = d_nm->mkNode(BAG_CARD, n[0][1]);
- Node plus = d_nm->mkNode(PLUS, A, B);
+ Node plus = d_nm->mkNode(ADD, A, B);
return BagsRewriteResponse(plus, Rewrite::CARD_DISJOINT);
}
return BagsRewriteResponse(n, Rewrite::NONE);
counts.push_back(pairs[k].second);
}
counts.push_back(pairs[j].second);
- Node sum = d_nm->mkNode(PLUS, counts);
+ Node sum = d_nm->mkNode(ADD, counts);
Node premise;
if (distinct.size() == 1)
{
Node skolem = getSkolem(n, inferInfo);
Node count = getMultiplicityTerm(e, skolem);
- Node sum = d_nm->mkNode(PLUS, countA, countB);
+ Node sum = d_nm->mkNode(ADD, countA, countB);
Node equal = count.eqNode(sum);
inferInfo.d_conclusion = equal;
lemmas.push_back(d_state->registerCardinalityTerm(card));
d_state->getCardinalitySkolem(card);
Node skolem = d_state->getCardinalitySkolem(card);
- sum = d_nm->mkNode(PLUS, sum, skolem);
+ sum = d_nm->mkNode(ADD, sum, skolem);
++it;
}
Node parentCard = d_nm->mkNode(BAG_CARD, parent);
bvm->mkBoundVar<SecondIndexVarAttribute>(n, "j", d_nm->integerType());
Node iList = d_nm->mkNode(BOUND_VAR_LIST, i);
Node jList = d_nm->mkNode(BOUND_VAR_LIST, j);
- Node iPlusOne = d_nm->mkNode(PLUS, i, d_one);
+ Node iPlusOne = d_nm->mkNode(ADD, i, d_one);
Node iMinusOne = d_nm->mkNode(SUB, i, d_one);
Node uf_i = d_nm->mkNode(APPLY_UF, uf, i);
Node uf_j = d_nm->mkNode(APPLY_UF, uf, j);
Node count_iMinusOne = d_nm->mkNode(BAG_COUNT, uf_iMinusOne, A);
Node count_uf_i = d_nm->mkNode(BAG_COUNT, uf_i, A);
Node inductiveCase =
- d_nm->mkNode(EQUAL, sum_i, d_nm->mkNode(PLUS, sum_iMinusOne, count_uf_i));
+ d_nm->mkNode(EQUAL, sum_i, d_nm->mkNode(ADD, sum_iMinusOne, count_uf_i));
Node f_iEqualE = d_nm->mkNode(EQUAL, f_uf_i, e);
Node geqOne = d_nm->mkNode(GEQ, count_uf_i, d_one);
# upper bound, leave the colon after LB, but omit UB. For example,
# an N-ary operator might be defined as:
#
-# operator PLUS 2: "addition on two or more arguments"
+# operator ADD 2: "addition on two or more arguments"
#
# parameterized K1 K2 #children ["comment"]
#
Node a =
d_nm->mkNode(kind::MULT, translated_children[0], pow2BvSizeRight);
Node b = translated_children[1];
- returnNode = d_nm->mkNode(kind::PLUS, a, b);
+ returnNode = d_nm->mkNode(kind::ADD, a, b);
break;
}
case kind::BITVECTOR_EXTRACT:
Node thenResult = x;
Node left = maxInt(amount);
Node mul = d_nm->mkNode(kind::MULT, left, pow2(bvsize));
- Node sum = d_nm->mkNode(kind::PLUS, mul, x);
+ Node sum = d_nm->mkNode(kind::ADD, mul, x);
Node elseResult = sum;
Node ite = d_nm->mkNode(kind::ITE, condition, thenResult, elseResult);
returnNode = ite;
Node IntBlaster::createBVAddNode(Node x, Node y, uint64_t bvsize)
{
- Node plus = d_nm->mkNode(kind::PLUS, x, y);
+ Node plus = d_nm->mkNode(kind::ADD, x, y);
Node p2 = pow2(bvsize);
return d_nm->mkNode(kind::INTS_MODULUS_TOTAL, plus, p2);
}
nm->mkNode(kind::ITE, cond, nm->mkConstInt(Rational(i)), z));
}
// avoid plus with one child
- return children.size() == 1 ? children[0] : nm->mkNode(kind::PLUS, children);
+ return children.size() == 1 ? children[0] : nm->mkNode(kind::ADD, children);
}
Node eliminateInt2Bv(TNode node)
unsigned weight = c.getWeight();
children.push_back(nm->mkConstInt(Rational(weight)));
Node res =
- children.size() == 1 ? children[0] : nm->mkNode(kind::PLUS, children);
+ children.size() == 1 ? children[0] : nm->mkNode(kind::ADD, children);
Trace("datatypes-rewrite")
<< "DatatypesRewriter::postRewrite: rewrite size " << in << " to "
<< res << std::endl;
Node mt = d_szinfo[m]->getOrMkActiveMeasureValue();
Node newMt = d_szinfo[m]->getOrMkActiveMeasureValue(true);
Node ds = nm->mkNode(DT_SIZE, e);
- slem = mt.eqNode(nm->mkNode(PLUS, newMt, ds));
+ slem = mt.eqNode(nm->mkNode(ADD, newMt, ds));
}
Trace("sygus-sb") << "...size lemma : " << slem << std::endl;
d_im.lemma(slem, InferenceId::DATATYPES_SYGUS_MT_BOUND);
*
* As a simple example, consider the trie:
* root:
- * d_req_kind = PLUS
+ * d_req_kind = ADD
* d_children[0]:
* d_req_type = A
* d_children[1]:
* d_req_type = A
* This trie is satisfied by sygus types that have a constructor whose builtin
- * kind is PLUS and whose argument types are both A.
+ * kind is ADD and whose argument types are both A.
*/
class ReqTrie
{
{
// (not (~ x y)) -----> (~ (+ y 1) x)
rt.d_req_kind = k;
- rt.d_children[0].d_req_kind = PLUS;
+ rt.d_children[0].d_req_kind = ADD;
rt.d_children[0].d_children[0].d_req_type = dt[c].getArgType(1);
rt.d_children[0].d_children[1].d_req_const =
NodeManager::currentNM()->mkConstInt(Rational(1));
// (not (~ x y)) -----> (~ y (+ x 1))
rt.d_req_kind = k;
rt.d_children[0].d_req_type = dt[c].getArgType(1);
- rt.d_children[1].d_req_kind = PLUS;
+ rt.d_children[1].d_req_kind = ADD;
rt.d_children[1].d_children[0].d_req_type = dt[c].getArgType(0);
rt.d_children[1].d_children[1].d_req_const =
NodeManager::currentNM()->mkConstInt(Rational(1));
}
else if (pk == NEG)
{
- if (k == PLUS)
+ if (k == ADD)
{
- rt.d_req_kind = PLUS;
+ rt.d_req_kind = ADD;
reqk = NEG;
}
}
else if (pk == BITVECTOR_NEG)
{
- if (k == PLUS)
+ if (k == ADD)
{
- rt.d_req_kind = PLUS;
+ rt.d_req_kind = ADD;
reqk = BITVECTOR_NEG;
}
}
// (~ (- y z) x) ----> (~ y (+ x z))
rt.d_req_kind = pk;
rt.d_children[arg].d_req_type = dt[c].getArgType(0);
- rt.d_children[oarg].d_req_kind = k == SUB ? PLUS : BITVECTOR_ADD;
+ rt.d_children[oarg].d_req_kind = k == SUB ? ADD : BITVECTOR_ADD;
rt.d_children[oarg].d_children[0].d_req_type = pdt[pc].getArgType(oarg);
rt.d_children[oarg].d_children[1].d_req_type = dt[c].getArgType(1);
}
- else if (pk == PLUS || pk == BITVECTOR_ADD)
+ else if (pk == ADD || pk == BITVECTOR_ADD)
{
// (+ x (- y z)) -----> (- (+ x y) z)
// (+ (- y z) x) -----> (- (+ x y) z)
- rt.d_req_kind = pk == PLUS ? SUB : BITVECTOR_SUB;
+ rt.d_req_kind = pk == ADD ? SUB : BITVECTOR_SUB;
int oarg = arg == 0 ? 1 : 0;
rt.d_children[0].d_req_kind = pk;
rt.d_children[0].d_children[0].d_req_type = pdt[pc].getArgType(oarg);
results[currNode] = EvalResult(av);
break;
}
- case kind::PLUS:
+ case kind::ADD:
{
Rational res = results[currNode[0]].d_rat;
for (size_t i = 1, end = currNode.getNumChildren(); i < end; i++)
k = sv_t.getKind();
/* Note: All n-ary kinds except for CONCAT (i.e., BITVECTOR_AND,
- * BITVECTOR_OR, MULT, PLUS) are commutative (no case split
+ * BITVECTOR_OR, MULT, ADD) are commutative (no case split
* based on index). */
Node s = dropChild(sv_t, index);
Assert((nchildren == 1 && s.isNull()) || (nchildren > 1 && !s.isNull()));
if (d_type.isInteger())
{
uval = nm->mkNode(
- PLUS,
+ ADD,
val,
nm->mkConstInt(Rational(isUpperBoundCTT(uires) ? 1 : -1)));
uval = rewrite(uval);
{
uires = is_upper ? CEG_TT_LOWER : CEG_TT_UPPER;
uval = nm->mkNode(
- PLUS,
+ ADD,
val,
nm->mkConstInt(Rational(isUpperBoundCTT(uires) ? 1 : -1)));
uval = rewrite(uval);
}
else
{
- vts_coeff_delta = nm->mkNode(PLUS, vts_coeff_delta, delta_coeff);
+ vts_coeff_delta = nm->mkNode(ADD, vts_coeff_delta, delta_coeff);
vts_coeff_delta = rewrite(vts_coeff_delta);
}
}
{
Node delta = d_vtc->getVtsDelta();
uval =
- nm->mkNode(uires == CEG_TT_UPPER_STRICT ? PLUS : SUB, uval, delta);
+ nm->mkNode(uires == CEG_TT_UPPER_STRICT ? ADD : SUB, uval, delta);
uval = rewrite(uval);
}
}
else
{
val = nm->mkNode(MULT,
- nm->mkNode(PLUS, vals[0], vals[1]),
+ nm->mkNode(ADD, vals[0], vals[1]),
nm->mkConstReal(Rational(1) / Rational(2)));
val = rewrite(val);
}
{
if (!vals[0].isNull())
{
- val = nm->mkNode(PLUS, vals[0], d_one);
+ val = nm->mkNode(ADD, vals[0], d_one);
val = rewrite(val);
}
else if (!vals[1].isNull())
&& options().quantifiers.cegqiRoundUpLowerLia)
{
sf.d_subs[index] = nm->mkNode(
- PLUS,
+ ADD,
sf.d_subs[index],
nm->mkNode(
ITE,
Node realPart = real_part.empty()
? d_zero
: (real_part.size() == 1 ? real_part[0]
- : nm->mkNode(PLUS, real_part));
+ : nm->mkNode(ADD, real_part));
Assert(ci->isEligibleForInstantiation(realPart));
// re-isolate
Trace("cegqi-arith-debug") << "Re-isolate..." << std::endl;
(msum[pv].isNull() || msum[pv].getConst<Rational>().sgn() == 1) ? 1
: -1;
val = rewrite(
- nm->mkNode(ires_use == -1 ? PLUS : SUB,
- nm->mkNode(ires_use == -1 ? SUB : PLUS, val, realPart),
+ nm->mkNode(ires_use == -1 ? ADD : SUB,
+ nm->mkNode(ires_use == -1 ? SUB : ADD, val, realPart),
nm->mkNode(TO_INTEGER, realPart)));
// could round up for upper bounds here
Trace("cegqi-arith-debug") << "result : " << val << std::endl;
rho = nm->mkNode(INTS_MODULUS_TOTAL, rho, new_theta);
rho = rewrite(rho);
Trace("cegqi-arith-bound2") << rho << std::endl;
- Kind rk = isLower ? PLUS : SUB;
+ Kind rk = isLower ? ADD : SUB;
val = nm->mkNode(rk, val, rho);
val = rewrite(val);
Trace("cegqi-arith-bound2") << "(after rho) : " << val << std::endl;
if (!inf_coeff.isNull())
{
Assert(!d_vts_sym[0].isNull());
- val = nm->mkNode(PLUS, val, nm->mkNode(MULT, inf_coeff, d_vts_sym[0]));
+ val = nm->mkNode(ADD, val, nm->mkNode(MULT, inf_coeff, d_vts_sym[0]));
val = rewrite(val);
}
if (!delta_coeff.isNull())
{
// create delta here if necessary
val = nm->mkNode(
- PLUS, val, nm->mkNode(MULT, delta_coeff, d_vtc->getVtsDelta()));
+ ADD, val, nm->mkNode(MULT, delta_coeff, d_vtc->getVtsDelta()));
val = rewrite(val);
}
return val;
CegHandledStatus CegInstantiator::isCbqiKind(Kind k)
{
- if (quantifiers::TermUtil::isBoolConnective(k) || k == PLUS || k == GEQ
+ if (quantifiers::TermUtil::isBoolConnective(k) || k == ADD || k == GEQ
|| k == EQUAL || k == MULT || k == NONLINEAR_MULT || k == DIVISION
|| k == DIVISION_TOTAL || k == INTS_DIVISION || k == INTS_DIVISION_TOTAL
|| k == INTS_MODULUS || k == INTS_MODULUS_TOTAL || k == TO_INTEGER
children.push_back( c );
Trace("sygus-si-apply-subs-debug") << "Add child : " << c << std::endl;
}
- Node nretc = children.size()==1 ? children[0] : NodeManager::currentNM()->mkNode( PLUS, children );
+ Node nretc = children.size() == 1
+ ? children[0]
+ : NodeManager::currentNM()->mkNode(ADD, children);
nretc = rewrite(nretc);
//ensure that nret does not contain vars
if (!expr::hasSubterm(nretc, vars))
else
{
Assert(tn.isRealOrInt());
- t_match = nm->mkNode(PLUS, t, nm->mkConstRealOrInt(tn, Rational(1)));
+ t_match = nm->mkNode(ADD, t, nm->mkConstRealOrInt(tn, Rational(1)));
}
}
else if (pat.getKind() == GEQ)
{
t_match =
- nm->mkNode(PLUS, t, nm->mkConstRealOrInt(t.getType(), Rational(1)));
+ nm->mkNode(ADD, t, nm->mkConstRealOrInt(t.getType(), Rational(1)));
}
else if (pat.getKind() == GT)
{
{
return n;
}
- else if (nk == PLUS || nk == MULT)
+ else if (nk == ADD || nk == MULT)
{
Node ret;
for (const Node& nc : n)
{
return x;
}
- else if (nk == PLUS || nk == MULT)
+ else if (nk == ADD || nk == MULT)
{
NodeManager* nm = NodeManager::currentNM();
int cindex = -1;
Node nc = n[i];
if (!quantifiers::TermUtil::hasInstConstAttr(nc))
{
- if (nk == PLUS)
+ if (nk == ADD)
{
x = nm->mkNode(SUB, x, nc);
}
if (!checkPol)
{
s = nm->mkNode(
- PLUS,
+ ADD,
s,
nm->mkConstRealOrInt(s.getType(), Rational(d_rel == GEQ ? -1 : 1)));
}
n1 = veq[1];
n2 = veq[0];
if( n1.getKind()==BOUND_VARIABLE ){
- n2 = nm->mkNode(PLUS, n2, nm->mkConstInt(Rational(1)));
+ n2 = nm->mkNode(ADD, n2, nm->mkConstInt(Rational(1)));
}else{
- n1 = nm->mkNode(PLUS, n1, nm->mkConstInt(Rational(-1)));
+ n1 = nm->mkNode(ADD, n1, nm->mkConstInt(Rational(-1)));
}
veq = nm->mkNode(GEQ, n1, n2);
}
Trace("bound-int-rsi") << "Actual bound range is " << rr << std::endl;
for (long k = 0; k < rr; k++)
{
- Node t = nm->mkNode(PLUS, tl, nm->mkConstInt(Rational(k)));
+ Node t = nm->mkNode(ADD, tl, nm->mkConstInt(Rational(k)));
t = rewrite(t);
elements.push_back( t );
}
slv_v = index;
}
Trace("qcf-tconstraint-debug") << "Solve " << d_vars[index] << " = " << v << " " << d_vars[index].getKind() << std::endl;
- if( d_vars[index].getKind()==PLUS || d_vars[index].getKind()==MULT ){
+ if (d_vars[index].getKind() == ADD || d_vars[index].getKind() == MULT)
+ {
Kind k = d_vars[index].getKind();
std::vector< TNode > children;
for (const Node& vi : d_vars[index]){
if (d_parent->atConflictEffort())
{
Kind kn = k;
- if( d_vars[index].getKind()==PLUS ){
+ if (d_vars[index].getKind() == ADD)
+ {
kn = SUB;
}
if( kn!=k ){
if (it == d_zero.end())
{
Node nn;
- if( k==PLUS ){
+ if (k == ADD)
+ {
nn = NodeManager::currentNM()->mkConstRealOrInt(tn, Rational(0));
}
d_zero[key] = nn;
candidates.push_back(n);
}
}
- else if (n.getKind() == PLUS)
+ else if (n.getKind() == ADD)
{
for (size_t i = 0; i < n.getNumChildren(); i++)
{
Node slvL = nm->mkNode(STRING_LENGTH, slv);
Node tpreL = nm->mkNode(STRING_LENGTH, tpre);
Node tpostL = nm->mkNode(STRING_LENGTH, tpost);
- slv = nm->mkNode(
- STRING_SUBSTR,
- slv,
- tpreL,
- nm->mkNode(SUB, slvL, nm->mkNode(PLUS, tpreL, tpostL)));
+ slv =
+ nm->mkNode(STRING_SUBSTR,
+ slv,
+ tpreL,
+ nm->mkNode(SUB, slvL, nm->mkNode(ADD, tpreL, tpostL)));
// forall x. r ++ x ++ t = s => P( x )
// is equivalent to
// r ++ s' ++ t = s => P( s' ) where
if( n.getKind()==EQUAL ){
for( unsigned i=0; i<2; i++ ){
Node roff = nm->mkNode(
- PLUS, r_add, nm->mkConstInt(Rational(i == 0 ? 1 : -1)));
+ ADD, r_add, nm->mkConstInt(Rational(i == 0 ? 1 : -1)));
rdl.d_val.push_back(roff);
}
}else if( n.getKind()==GEQ ){
- Node roff = nm->mkNode(
- PLUS, r_add, nm->mkConstInt(Rational(varLhs ? 1 : -1)));
+ Node roff =
+ nm->mkNode(ADD, r_add, nm->mkConstInt(Rational(varLhs ? 1 : -1)));
rdl.d_val.push_back(roff);
}
}
std::vector<TypeNode> cargsPlus;
cargsPlus.push_back(u);
cargsPlus.push_back(u);
- sdt.addConstructor(PLUS, cargsPlus);
+ sdt.addConstructor(ADD, cargsPlus);
sdt.initializeDatatype(nm->integerType(), bvl, false, false);
std::vector<DType> datatypes;
datatypes.push_back(sdt.getDatatype());
if (types[i].isRealOrInt())
{
- // Add PLUS, SUB
- Kind kinds[2] = {PLUS, SUB};
+ // Add ADD, SUB
+ Kind kinds[2] = {ADD, SUB};
for (const Kind kind : kinds)
{
Trace("sygus-grammar-def") << "...add for " << kind << std::endl;
std::vector<TypeNode> cargsEmpty;
sdts.back().addConstructor(
nm->mkConstInt(Rational(1)), "1", cargsEmpty);
- /* Add operator PLUS */
- Kind kind = PLUS;
- Trace("sygus-grammar-def") << "\t...add for PLUS to Pos_Int\n";
+ /* Add operator ADD */
+ Kind kind = ADD;
+ Trace("sygus-grammar-def") << "\t...add for ADD to Pos_Int\n";
std::vector<TypeNode> cargsPlus;
cargsPlus.push_back(unresPosInt);
cargsPlus.push_back(unresPosInt);
cargsAnyTerm.push_back(unresAnyConst);
// make the sygus operator lambda X. c1*t1 + ... + cn*tn + c
Assert(sumChildren.size() > 1);
- Node ops = nm->mkNode(PLUS, sumChildren);
+ Node ops = nm->mkNode(ADD, sumChildren);
Node op = nm->mkNode(LAMBDA, nm->mkNode(BOUND_VAR_LIST, lambdaVars), ops);
Trace("sygus-grammar-def") << "any term operator is " << op << std::endl;
// make the any term datatype, add to back
std::vector<TypeNode> cargsPlus;
cargsPlus.push_back(unres_types[iat]);
cargsPlus.push_back(unres_types[iat]);
- sdts[iat].d_sdt.addConstructor(PLUS, cargsPlus);
+ sdts[iat].d_sdt.addConstructor(ADD, cargsPlus);
}
// add the ITE, regardless of sum-of-monomials vs polynomial
std::vector<TypeNode> cargsIte;
bool SygusGrammarNorm::TransfChain::isChainable(TypeNode tn, Node op)
{
/* Checks whether operator occurs chainable for its type */
- if (tn.isInteger() && NodeManager::currentNM()->operatorToKind(op) == PLUS)
+ if (tn.isInteger() && NodeManager::currentNM()->operatorToKind(op) == ADD)
{
return true;
}
function should realize that it is chainable for integers */
bool SygusGrammarNorm::TransfChain::isId(TypeNode tn, Node op, Node n)
{
- if (tn.isInteger() && NodeManager::currentNM()->operatorToKind(op) == PLUS
+ if (tn.isInteger() && NodeManager::currentNM()->operatorToKind(op) == ADD
&& n == TermUtil::mkTypeValue(tn, 0))
{
return true;
std::vector<TypeNode> ctypesp;
ctypesp.push_back(t);
ctypesp.push_back(to.d_unres_tn);
- to.d_sdt.addConstructor(nm->operatorOf(PLUS), kindToString(PLUS), ctypesp);
+ to.d_sdt.addConstructor(nm->operatorOf(ADD), kindToString(ADD), ctypesp);
Trace("sygus-grammar-normalize-chain")
- << "\tAdding PLUS to " << to.d_unres_tn << " with arg types "
+ << "\tAdding ADD to " << to.d_unres_tn << " with arg types "
<< to.d_unres_tn << " and " << t << "\n";
}
/* In the initial case if not all operators claimed always creates a next */
{
Assert(op_pos[i] < dt.getNumConstructors());
Node sop = dt[op_pos[i]].getSygusOp();
- /* Collects a chainable operator such as PLUS */
+ /* Collects a chainable operator such as ADD */
if (sop.getKind() == BUILTIN && TransfChain::isChainable(sygus_tn, sop))
{
- Assert(nm->operatorToKind(sop) == PLUS);
+ Assert(nm->operatorToKind(sop) == ADD);
/* TODO #1304: be robust for this case */
/* For now only transforms applications whose arguments have the same type
* as the root */
if (!same_type_plus)
{
Trace("sygus-grammar-normalize-infer")
- << "\tFor OP " << PLUS << " did not collecting sop " << sop
+ << "\tFor OP " << ADD << " did not collecting sop " << sop
<< " in position " << op_pos[i] << "\n";
continue;
}
continue;
}
/* TODO #1304: check this for each operator */
- /* Collects elements that are not the identity (e.g. 0 is the id of PLUS) */
- if (!TransfChain::isId(sygus_tn, nm->operatorOf(PLUS), sop))
+ /* Collects elements that are not the identity (e.g. 0 is the id of ADD) */
+ if (!TransfChain::isId(sygus_tn, nm->operatorOf(ADD), sop))
{
Trace("sygus-grammar-normalize-infer")
<< "\tCollecting for NON_ID_ELEMS the sop " << sop
* neutral element.
*
* TODO: #1304:
- * - define this transformation for more than just PLUS for Int.
+ * - define this transformation for more than just ADD for Int.
* - improve the building such that elements that should not be entitled a
* "link in the chain" (such as 5 in opposition to variables and 1) do not get
* one
const DType& dt,
std::vector<unsigned>& op_pos) override;
- /** Whether operator is chainable for the type (e.g. PLUS for Int)
+ /** Whether operator is chainable for the type (e.g. ADD for Int)
*
* Since the map this function depends on cannot be built statically, this
* function first build maps the first time a type is checked. As a
*/
static bool isChainable(TypeNode tn, Node op);
/* Whether n is the identity for the chain operator of the type (e.g. 1 is
- * not the identity 0 for PLUS for Int)
+ * not the identity 0 for ADD for Int)
*
* TODO: #1304: Cover more types, make this robust to more complex grammars
*/
static std::map<TypeNode, std::vector<Kind>> d_chain_ops;
/** Specifies for each type node and chainable operator its identity
*
- * For example, for Int and PLUS the map is {Int -> {+ -> 0}}
+ * For example, for Int and ADD the map is {Int -> {+ -> 0}}
*
* TODO #1304: consider more operators
*/
Trace("sygus-db") << std::endl;
// We must properly catch type errors in sygus grammars for arguments of
// builtin operators. The challenge is that we easily ask for expected
- // argument types of builtin operators e.g. PLUS. Hence we use a call to
+ // argument types of builtin operators e.g. ADD. Hence we use a call to
// mkGeneric below. This ensures that terms that this constructor encodes
// are of the type specified in the datatype. This will fail if
// e.g. bitvector-and is a constructor of an integer grammar. Our (version
}
else
{
- ret = nm->mkNode(kind::PLUS, sum);
+ ret = nm->mkNode(kind::ADD, sum);
}
if (Random::getRandom().pickWithProb(0.5))
/** Get the currently added ground terms for the given operator */
DbList* getOrMkDbListForOp(TNode op);
/** get match operator for term n
- *
- * If n has a kind that we index, this function will
- * typically return n.getOperator().
- *
- * However, for parametric operators f, the match operator is an arbitrary
- * chosen f-application. For example, consider array select:
- * A : (Array Int Int)
- * B : (Array Bool Int)
- * We require that terms like (select A 1) and (select B 2) are indexed in
- * separate
- * data structures despite the fact that
- * (select A 1).getOperator()==(select B 2).getOperator().
- * Hence, for the above terms, we may return:
- * getMatchOperator( (select A 1) ) = (select A 1), and
- * getMatchOperator( (select B 2) ) = (select B 2).
- * The match operator is the first instance of an application of the parametric
- * operator of its type.
- *
- * If n has a kind that we do not index (like PLUS),
- * then this function returns Node::null().
- */
+ *
+ * If n has a kind that we index, this function will
+ * typically return n.getOperator().
+ *
+ * However, for parametric operators f, the match operator is an arbitrary
+ * chosen f-application. For example, consider array select:
+ * A : (Array Int Int)
+ * B : (Array Bool Int)
+ * We require that terms like (select A 1) and (select B 2) are indexed in
+ * separate
+ * data structures despite the fact that
+ * (select A 1).getOperator()==(select B 2).getOperator().
+ * Hence, for the above terms, we may return:
+ * getMatchOperator( (select A 1) ) = (select A 1), and
+ * getMatchOperator( (select B 2) ) = (select B 2).
+ * The match operator is the first instance of an application of the
+ * parametric operator of its type.
+ *
+ * If n has a kind that we do not index (like ADD),
+ * then this function returns Node::null().
+ */
Node getMatchOperator(Node n);
/** get term arg index for all f-applications in the current context */
TNodeTrie* getTermArgTrie(Node f);
return false;
}
}
- return k == PLUS || k == MULT || k == NONLINEAR_MULT || k == AND || k == OR
+ return k == ADD || k == MULT || k == NONLINEAR_MULT || k == AND || k == OR
|| k == XOR || k == BITVECTOR_ADD || k == BITVECTOR_MULT
|| k == BITVECTOR_AND || k == BITVECTOR_OR || k == BITVECTOR_XOR
|| k == BITVECTOR_XNOR || k == BITVECTOR_CONCAT || k == STRING_CONCAT
return false;
}
}
- return k == EQUAL || k == PLUS || k == MULT || k == NONLINEAR_MULT || k == AND
+ return k == EQUAL || k == ADD || k == MULT || k == NONLINEAR_MULT || k == AND
|| k == OR || k == XOR || k == BITVECTOR_ADD || k == BITVECTOR_MULT
|| k == BITVECTOR_AND || k == BITVECTOR_OR || k == BITVECTOR_XOR
|| k == BITVECTOR_XNOR || k == SET_UNION || k == SET_INTER
TypeNode tn = n.getType();
if (n == mkTypeValue(tn, 0))
{
- if (ik == PLUS || ik == OR || ik == XOR || ik == BITVECTOR_ADD
+ if (ik == ADD || ik == OR || ik == XOR || ik == BITVECTOR_ADD
|| ik == BITVECTOR_OR || ik == BITVECTOR_XOR || ik == STRING_CONCAT)
{
return true;
Node ret = NodeManager::currentNM()->mkNode(
kind::SUB,
NodeManager::currentNM()->mkNode(
- kind::PLUS,
+ kind::ADD,
NodeManager::currentNM()->mkNode(kind::SET_CARD, node[0][0]),
NodeManager::currentNM()->mkNode(kind::SET_CARD, node[0][1])),
NodeManager::currentNM()->mkNode(
// get the current "fixed" sum for the abstraction of ar
Node aar = aarSum.empty()
? d_zero
- : (aarSum.size() == 1 ? aarSum[0] : nm->mkNode(PLUS, aarSum));
+ : (aarSum.size() == 1 ? aarSum[0] : nm->mkNode(ADD, aarSum));
aar = d_rr->rewrite(aar);
Trace("strings-ent-approx-debug")
<< "...processed fixed sum " << aar << " with " << mApprox.size()
Assert(!v.isNull() && !vapprox.isNull());
Assert(msum.find(v) != msum.end());
Node mn = ArithMSum::mkCoeffTerm(msum[v], vapprox);
- aar = nm->mkNode(PLUS, aar, mn);
+ aar = nm->mkNode(ADD, aar, mn);
// update the msumAar map
aar = d_rr->rewrite(aar);
msumAar.clear();
bool isOverApprox)
{
NodeManager* nm = NodeManager::currentNM();
- // We do not handle PLUS here since this leads to exponential behavior.
+ // We do not handle ADD here since this leads to exponential behavior.
// Instead, this is managed, e.g. during checkApprox, where
- // PLUS terms are expanded "on-demand" during the reasoning.
+ // ADD terms are expanded "on-demand" during the reasoning.
Trace("strings-ent-approx-debug")
<< "Get arith approximations " << a << std::endl;
Kind ak = a.getKind();
{
// 0 <= n and n+m <= len( x ) implies
// m <= len( substr( x, n, m ) )
- Node npm = nm->mkNode(PLUS, a[0][1], a[0][2]);
+ Node npm = nm->mkNode(ADD, a[0][1], a[0][2]);
if (check(a[0][1]) && check(lenx, npm))
{
approx.push_back(a[0][2]);
else
{
// len( x ) + len( z ) >= len( replace( x, y, z ) )
- approx.push_back(nm->mkNode(PLUS, lenx, lenz));
+ approx.push_back(nm->mkNode(ADD, lenx, lenz));
}
}
else
// x >= 0 implies
// x+1 >= len( int.to.str( x ) )
approx.push_back(
- nm->mkNode(PLUS, nm->mkConstInt(Rational(1)), a[0][0]));
+ nm->mkNode(ADD, nm->mkConstInt(Rational(1)), a[0][0]));
}
}
}
Node curr = toVisit.back();
toVisit.pop_back();
- if (curr.getKind() == kind::PLUS || curr.getKind() == kind::MULT
+ if (curr.getKind() == kind::ADD || curr.getKind() == kind::MULT
|| curr.getKind() == kind::SUB || curr.getKind() == kind::EQUAL)
{
for (const auto& currChild : curr)
Node s = nm->mkBoundVar("slackVal", nm->stringType());
Node slen = nm->mkNode(kind::STRING_LENGTH, s);
assumption = d_rr->rewrite(
- nm->mkNode(kind::EQUAL, x, nm->mkNode(kind::PLUS, y, slen)));
+ nm->mkNode(kind::EQUAL, x, nm->mkNode(kind::ADD, y, slen)));
}
Node diff = nm->mkNode(kind::SUB, a, b);
ret = d_zero;
}
}
- else if (a.getKind() == kind::PLUS || a.getKind() == kind::MULT)
+ else if (a.getKind() == kind::ADD || a.getKind() == kind::MULT)
{
std::vector<Node> children;
bool success = true;
// str.len( t ) >= 0
return true;
}
- else if (a.getKind() == kind::PLUS || a.getKind() == kind::MULT)
+ else if (a.getKind() == kind::ADD || a.getKind() == kind::MULT)
{
for (unsigned i = 0; i < a.getNumChildren(); i++)
{
NodeManager* nm = NodeManager::currentNM();
// Check if we can show that y1 + ... + yn >= x
- Node sum = (ys.size() > 1) ? nm->mkNode(PLUS, ys) : ys[0];
+ Node sum = (ys.size() > 1) ? nm->mkNode(ADD, ys) : ys[0];
if (!check(sum, x))
{
return false;
std::vector<Node>::iterator pos = ys.erase(ys.begin() + i);
if (ys.size() > 1)
{
- sum = nm->mkNode(PLUS, ys);
+ sum = nm->mkNode(ADD, ys);
}
else
{
Node i = n[1];
Node sLen = nm->mkNode(STRING_LENGTH, s);
Node iRev = nm->mkNode(
- SUB, sLen, nm->mkNode(PLUS, i, nm->mkConstInt(Rational(1))));
+ SUB, sLen, nm->mkNode(ADD, i, nm->mkConstInt(Rational(1))));
std::vector<Node> nexp;
nexp.push_back(nm->mkNode(LEQ, nm->mkConstInt(Rational(0)), i));
Node currSum = d_zero;
if (!lacc.empty())
{
- currSum = lacc.size() == 1 ? lacc[0] : nm->mkNode(PLUS, lacc);
+ currSum = lacc.size() == 1 ? lacc[0] : nm->mkNode(ADD, lacc);
currIndex = nm->mkNode(SUB, currIndex, currSum);
}
Node cc;
lacc.push_back(clen);
if (k == SEQ_NTH)
{
- Node currSumPost = lacc.size() == 1 ? lacc[0] : nm->mkNode(PLUS, lacc);
+ Node currSumPost = lacc.size() == 1 ? lacc[0] : nm->mkNode(ADD, lacc);
Node cf = nm->mkNode(LT, t[1], currSumPost);
Trace("seq-array-debug") << "......condition " << cf << std::endl;
cond.push_back(cf);
}
}
Node lenSum = childLengths.size() > 1
- ? nm->mkNode(PLUS, childLengths)
+ ? nm->mkNode(ADD, childLengths)
: (childLengths.empty() ? zero : childLengths[0]);
// if we have a fixed length
if (hasFixedLength)
{
Node ppSum = childLengthsPostPivot.size() == 1
? childLengthsPostPivot[0]
- : nm->mkNode(PLUS, childLengthsPostPivot);
+ : nm->mkNode(ADD, childLengthsPostPivot);
currEnd = nm->mkNode(SUB, lenx, ppSum);
}
else
Node currMem = nm->mkNode(STRING_IN_REGEXP, curr, re[i]);
conc.push_back(currMem);
}
- currEnd = nm->mkNode(PLUS, currEnd, childLengths[i]);
+ currEnd = nm->mkNode(ADD, currEnd, childLengths[i]);
}
}
Node res = nm->mkNode(AND, conc);
if (gap_minsize[i] > 0)
{
// the gap to this child is at least gap_minsize[i]
- prev_end = nm->mkNode(
- PLUS, prev_end, nm->mkConstInt(Rational(gap_minsize[i])));
+ prev_end =
+ nm->mkNode(ADD, prev_end, nm->mkConstInt(Rational(gap_minsize[i])));
}
prev_ends.push_back(prev_end);
Node sc = sep_children[i];
Node curr = prev_end;
Node ss = nm->mkNode(STRING_SUBSTR, x, curr, lensc);
conj.push_back(ss.eqNode(sc));
- prev_end = nm->mkNode(PLUS, curr, lensc);
+ prev_end = nm->mkNode(ADD, curr, lensc);
}
else
{
Node k =
bvm->mkBoundVar<ReElimConcatIndexAttribute>(cacheVal, intType);
non_greedy_find_vars.push_back(k);
- prev_end = nm->mkNode(PLUS, prev_end, k);
+ prev_end = nm->mkNode(ADD, prev_end, k);
}
Node curr = nm->mkNode(STRING_INDEXOF, x, sc, prev_end);
Node idofFind = curr.eqNode(nm->mkConstInt(Rational(-1))).negate();
conj.push_back(idofFind);
- prev_end = nm->mkNode(PLUS, curr, lensc);
+ prev_end = nm->mkNode(ADD, curr, lensc);
}
}
// ... ^ "B" = substr( x, len( x ) - 3, 1 ) ^ ...
Node sc = sep_children.back();
Node lenSc = nm->mkNode(STRING_LENGTH, sc);
- Node loc = nm->mkNode(SUB, lenx, nm->mkNode(PLUS, lenSc, cEnd));
+ Node loc = nm->mkNode(SUB, lenx, nm->mkNode(ADD, lenSc, cEnd));
Node scc = sc.eqNode(nm->mkNode(STRING_SUBSTR, x, loc, lenSc));
// We also must ensure that we fit. This constraint is necessary in
// addition to the constraint above. Take this example:
// For example:
// x in (re.++ "A" (re.* _) "B" _ _ (re.* _)) --->
// ... ^ indexof( x, "B", 1 ) + 2 <= len( x )
- Node fit = nm->mkNode(LEQ, nm->mkNode(PLUS, prev_end, cEnd), lenx);
+ Node fit = nm->mkNode(LEQ, nm->mkNode(ADD, prev_end, cEnd), lenx);
conj.push_back(fit);
}
Node res = nm->mkAnd(conj);
std::vector<Node> rsuffix;
rsuffix.insert(rsuffix.end(), children.begin() + i + 1, children.end());
Node rps = utils::mkConcat(rsuffix, nm->regExpType());
- Node ks = nm->mkNode(PLUS, k, lens);
+ Node ks = nm->mkNode(ADD, k, lens);
Node substrSuffix = nm->mkNode(
STRING_IN_REGEXP,
nm->mkNode(STRING_SUBSTR, x, ks, nm->mkNode(SUB, lenx, ks)),
kind::STRING_LENGTH, tmpNode[i]));
}
}
- Node retNode = NodeManager::currentNM()->mkNode(kind::PLUS, node_vec);
+ Node retNode = NodeManager::currentNM()->mkNode(kind::ADD, node_vec);
return returnRewrite(node, retNode, Rewrite::LEN_CONCAT);
}
}
Node tot_len =
d_arithEntail.rewrite(nm->mkNode(kind::STRING_LENGTH, node[0]));
Node end_pt =
- d_arithEntail.rewrite(nm->mkNode(kind::PLUS, node[1], node[2]));
+ d_arithEntail.rewrite(nm->mkNode(kind::ADD, node[1], node[2]));
if (node[2] != tot_len)
{
if (d_arithEntail.check(node[2], tot_len))
}
if (!new_len.isNull())
{
- Node new_start = nm->mkNode(kind::PLUS, start_inner, start_outer);
+ Node new_start = nm->mkNode(kind::ADD, start_inner, start_outer);
Node ret =
nm->mkNode(kind::STRING_SUBSTR, node[0][0], new_start, new_len);
return returnRewrite(node, ret, Rewrite::SS_COMBINE);
// str.rev(str.update(s, len(s) - (n + 1), t))
Node idx = nm->mkNode(SUB,
nm->mkNode(STRING_LENGTH, s),
- nm->mkNode(PLUS, i, nm->mkConstInt(Rational(1))));
+ nm->mkNode(ADD, i, nm->mkConstInt(Rational(1))));
Node ret = nm->mkNode(STRING_REV, nm->mkNode(STRING_UPDATE, s[0], idx, x));
return returnRewrite(node, ret, Rewrite::UPD_REV);
}
// str.indexof(str.++("AB", x, "C"), "C", 0) --->
// 2 + str.indexof(str.++(x, "C"), "C", 0)
Node ret = nm->mkNode(
- kind::PLUS,
+ kind::ADD,
nm->mkNode(kind::STRING_LENGTH, utils::mkConcat(nb, stype)),
nm->mkNode(kind::STRING_INDEXOF,
utils::mkConcat(children0, stype),
// str.len( x1 ) + str.indexof( x2, y, z-str.len(x1) )
Node nn = utils::mkConcat(children0, stype);
Node ret =
- nm->mkNode(PLUS,
+ nm->mkNode(ADD,
nm->mkNode(SUB, node[2], new_len),
nm->mkNode(STRING_INDEXOF, nn, node[1], new_len));
return returnRewrite(node, ret, Rewrite::IDOF_STRIP_SYM_LEN);
// Length of the non-substr components in the second argument
Node partLen1 =
nm->mkNode(kind::STRING_LENGTH, utils::mkConcat(children1, stype));
- Node maxLen1 = nm->mkNode(kind::PLUS, partLen1, lastChild1[2]);
+ Node maxLen1 = nm->mkNode(kind::ADD, partLen1, lastChild1[2]);
Node zero = nm->mkConstInt(Rational(0));
Node one = nm->mkConstInt(Rational(1));
Node len0 = nm->mkNode(kind::STRING_LENGTH, node[0]);
- Node len0_1 = nm->mkNode(kind::PLUS, len0, one);
+ Node len0_1 = nm->mkNode(kind::ADD, len0, one);
// Check len(t) + j > len(x) + 1
if (d_arithEntail.check(maxLen1, len0_1, true))
{
kind::STRING_SUBSTR,
lastChild1[0],
lastChild1[1],
- nm->mkNode(kind::PLUS, len0, one, nm->mkNode(kind::NEG, partLen1))));
+ nm->mkNode(kind::ADD, len0, one, nm->mkNode(kind::NEG, partLen1))));
Node res = nm->mkNode(kind::STRING_REPLACE,
node[0],
utils::mkConcat(children1, stype),
// sorts do not permit values that the solver can handle (e.g. uninterpreted
// sorts and arrays).
}
- else if (len.getKind() == PLUS)
+ else if (len.getKind() == ADD)
{
// x + y -> norm(x) + norm(y)
NodeBuilder concatBuilder(STRING_CONCAT);
id = SK_SUFFIX_REM;
Node pre = mkSkolemCached(a, b, SK_FIRST_CTN_PRE, "pre");
b = nm->mkNode(
- PLUS, nm->mkNode(STRING_LENGTH, pre), nm->mkNode(STRING_LENGTH, b));
+ ADD, nm->mkNode(STRING_LENGTH, pre), nm->mkNode(STRING_LENGTH, b));
}
else if (id == SK_ID_V_SPT || id == SK_ID_C_SPT)
{
{
bool success = true;
Node start_pos = n2[1];
- Node end_pos = nm->mkNode(PLUS, n2[1], n2[2]);
+ Node end_pos = nm->mkNode(ADD, n2[1], n2[2]);
Node len_n2s = nm->mkNode(STRING_LENGTH, n2[0]);
if (dir == 1)
{
{
sum.push_back(nm->mkNode(STRING_LENGTH, v));
}
- Node sumn = sum.size() == 1 ? sum[0] : nm->mkNode(PLUS, sum);
+ Node sumn = sum.size() == 1 ? sum[0] : nm->mkNode(ADD, sum);
d_inputVarLsum.set(sumn);
}
}
nodeVec.push_back(lni);
}
}
- lsum = nm->mkNode(PLUS, nodeVec);
+ lsum = nm->mkNode(ADD, nodeVec);
lsum = rewrite(lsum);
}
else if (n.isConst())
Node n = t[1];
Node m = t[2];
Node skt = sc->mkSkolemCached(t, SkolemCache::SK_PURIFY, "sst");
- Node t12 = nm->mkNode(PLUS, n, m);
+ Node t12 = nm->mkNode(ADD, n, m);
Node lt0 = nm->mkNode(STRING_LENGTH, s);
//start point is greater than or equal zero
Node c1 = nm->mkNode(GEQ, n, zero);
// len(s) - n -m
Node b13 = nm->mkNode(
OR,
- nm->mkNode(EQUAL, lsk2, nm->mkNode(SUB, lt0, nm->mkNode(PLUS, n, m))),
+ nm->mkNode(EQUAL, lsk2, nm->mkNode(SUB, lt0, nm->mkNode(ADD, n, m))),
nm->mkNode(EQUAL, lsk2, zero));
// Length of the result is at most m
Node b14 = nm->mkNode(LEQ, nm->mkNode(STRING_LENGTH, skt), m);
rs = nm->mkNode(STRING_SUBSTR, r, zero, nm->mkNode(SUB, lens, n));
}
Node rslen = nm->mkNode(STRING_LENGTH, rs);
- Node nsuf = nm->mkNode(PLUS, n, rslen);
+ Node nsuf = nm->mkNode(ADD, n, rslen);
// substr(s, n, len(substr(r,0,|s|-n))), which is used for formalizing the
// purification variable sk3 below.
Node ssubstr = nm->mkNode(STRING_SUBSTR, s, n, rslen);
y)
.negate();
// skk = n + len( io2 )
- Node c33 = skk.eqNode(nm->mkNode(PLUS, n, nm->mkNode(STRING_LENGTH, io2)));
+ Node c33 = skk.eqNode(nm->mkNode(ADD, n, nm->mkNode(STRING_LENGTH, io2)));
Node cc3 = nm->mkNode(AND, c31, c32, c33);
// assert:
conc.push_back(lem);
Node x = SkolemCache::mkIndexVar(t);
- Node xPlusOne = nm->mkNode(PLUS, x, one);
+ Node xPlusOne = nm->mkNode(ADD, x, one);
Node xbv = nm->mkNode(BOUND_VAR_LIST, x);
Node g = nm->mkNode(AND, nm->mkNode(GEQ, x, zero), nm->mkNode(LT, x, leni));
Node sx = nm->mkNode(STRING_SUBSTR, itost, x, one);
Node c = nm->mkNode(SUB, nm->mkNode(STRING_TO_CODE, sx), c0);
Node ten = nm->mkConstInt(Rational(10));
- Node eq = ux1.eqNode(nm->mkNode(PLUS, c, nm->mkNode(MULT, ten, ux)));
+ Node eq = ux1.eqNode(nm->mkNode(ADD, c, nm->mkNode(MULT, ten, ux)));
Node leadingZeroPos =
nm->mkNode(AND, x.eqNode(zero), nm->mkNode(GT, leni, one));
Node cb = nm->mkNode(
Node g = nm->mkNode(AND, nm->mkNode(GEQ, x, zero), nm->mkNode(LT, x, lens));
Node sx = nm->mkNode(STRING_SUBSTR, s, x, one);
Node ux = nm->mkNode(APPLY_UF, u, x);
- Node ux1 = nm->mkNode(APPLY_UF, u, nm->mkNode(PLUS, x, one));
+ Node ux1 = nm->mkNode(APPLY_UF, u, nm->mkNode(ADD, x, one));
Node c = nm->mkNode(SUB, nm->mkNode(STRING_TO_CODE, sx), c0);
- Node eq = ux1.eqNode(nm->mkNode(PLUS, c, nm->mkNode(MULT, ten, ux)));
+ Node eq = ux1.eqNode(nm->mkNode(ADD, c, nm->mkNode(MULT, ten, ux)));
Node cb = nm->mkNode(AND, nm->mkNode(GEQ, c, zero), nm->mkNode(LT, c, ten));
Node ux1lem = nm->mkNode(GEQ, stoit, ux1);
Node s = t[0];
Node n = t[1];
Node skt = sc->mkSkolemCached(t, SkolemCache::SK_PURIFY, "sst");
- Node t12 = nm->mkNode(PLUS, n, one);
+ Node t12 = nm->mkNode(ADD, n, one);
Node lt0 = nm->mkNode(STRING_LENGTH, s);
// start point is greater than or equal zero
Node c1 = nm->mkNode(GEQ, n, zero);
Node bound =
nm->mkNode(AND, nm->mkNode(GEQ, i, zero), nm->mkNode(LT, i, numOcc));
Node ufi = nm->mkNode(APPLY_UF, uf, i);
- Node ufip1 = nm->mkNode(APPLY_UF, uf, nm->mkNode(PLUS, i, one));
+ Node ufip1 = nm->mkNode(APPLY_UF, uf, nm->mkNode(ADD, i, one));
Node ii = nm->mkNode(STRING_INDEXOF, x, y, ufi);
Node cc =
nm->mkNode(STRING_CONCAT,
nm->mkNode(STRING_SUBSTR, x, ufi, nm->mkNode(SUB, ii, ufi)),
z,
- nm->mkNode(APPLY_UF, us, nm->mkNode(PLUS, i, one)));
+ nm->mkNode(APPLY_UF, us, nm->mkNode(ADD, i, one)));
std::vector<Node> flem;
flem.push_back(ii.eqNode(negOne).negate());
flem.push_back(nm->mkNode(APPLY_UF, us, i).eqNode(cc));
flem.push_back(
- ufip1.eqNode(nm->mkNode(PLUS, ii, nm->mkNode(STRING_LENGTH, y))));
+ ufip1.eqNode(nm->mkNode(ADD, ii, nm->mkNode(STRING_LENGTH, y))));
Node body = nm->mkNode(OR, bound.negate(), nm->mkNode(AND, flem));
Node q = utils::mkForallInternal(bvli, body);
Node bvli = nm->mkNode(BOUND_VAR_LIST, i);
Node bound =
nm->mkNode(AND, nm->mkNode(GEQ, i, zero), nm->mkNode(LT, i, numOcc));
- Node ip1 = nm->mkNode(PLUS, i, one);
+ Node ip1 = nm->mkNode(ADD, i, one);
Node ufi = nm->mkNode(APPLY_UF, uf, i);
Node ufip1 = nm->mkNode(APPLY_UF, uf, ip1);
Node ulip1 = nm->mkNode(APPLY_UF, ul, ip1);
flem.push_back(nm->mkNode(GT, ulip1, zero));
// Uf(i + 1) = indexof_re(x, yp, Uf(i)) + Ul(i + 1)
flem.push_back(ufip1.eqNode(
- nm->mkNode(PLUS, nm->mkNode(STRING_INDEXOF_RE, x, yp, ufi), ulip1)));
+ nm->mkNode(ADD, nm->mkNode(STRING_INDEXOF_RE, x, yp, ufi), ulip1)));
// in_re(substr(x, ii, Ul(i + 1)), y')
flem.push_back(nm->mkNode(
STRING_IN_REGEXP, nm->mkNode(STRING_SUBSTR, x, ii, ulip1), yp));
Node res = nm->mkNode(
ITE,
nm->mkNode(AND, nm->mkNode(LEQ, lb, ci), nm->mkNode(LEQ, ci, ub)),
- nm->mkNode(PLUS, ci, offset),
+ nm->mkNode(ADD, ci, offset),
ci);
Node bound =
Node bvi = nm->mkNode(BOUND_VAR_LIST, i);
Node revi =
- nm->mkNode(SUB, nm->mkNode(STRING_LENGTH, x), nm->mkNode(PLUS, i, one));
+ nm->mkNode(SUB, nm->mkNode(STRING_LENGTH, x), nm->mkNode(ADD, i, one));
Node ssr = nm->mkNode(STRING_SUBSTR, r, i, one);
Node ssx = nm->mkNode(STRING_SUBSTR, x, revi, one);
* kind k in getModelValue. We distinguish four categories of kinds:
*
* [1] "Evaluated"
- * This includes (standard) interpreted symbols like NOT, PLUS, SET_UNION,
+ * This includes (standard) interpreted symbols like NOT, ADD, SET_UNION,
* etc. These operators can be characterized by the invariant that they are
* "evaluatable". That is, if they are applied to only constants, the rewriter
* is guaranteed to rewrite the application to a constant. When getting
* an `std::ostream`.
* New values are added by
* HistogramStat<Kind> stat;
- * stat << Kind::PLUS << Kind::AND;
+ * stat << Kind::ADD << Kind::AND;
*/
template <typename Integral>
class HistogramStat
TEST_F(TestApiBlackOp, opFromKind)
{
- ASSERT_NO_THROW(d_solver.mkOp(PLUS));
+ ASSERT_NO_THROW(d_solver.mkOp(ADD));
ASSERT_THROW(d_solver.mkOp(BITVECTOR_EXTRACT), CVC5ApiException);
}
TEST_F(TestApiBlackOp, getNumIndices)
{
- Op plus = d_solver.mkOp(PLUS);
+ Op plus = d_solver.mkOp(ADD);
Op divisible = d_solver.mkOp(DIVISIBLE, 4);
Op bitvector_repeat = d_solver.mkOp(BITVECTOR_REPEAT, 5);
Op bitvector_zero_extend = d_solver.mkOp(BITVECTOR_ZERO_EXTEND, 6);
TEST_F(TestApiBlackOp, subscriptOperator)
{
- Op plus = d_solver.mkOp(PLUS);
+ Op plus = d_solver.mkOp(ADD);
Op divisible = d_solver.mkOp(DIVISIBLE, 4);
Op bitvector_repeat = d_solver.mkOp(BITVECTOR_REPEAT, 4);
Op bitvector_zero_extend = d_solver.mkOp(BITVECTOR_ZERO_EXTEND, 4);
TEST_F(TestApiWhiteOp, opFromKind)
{
- Op plus(&d_solver, PLUS);
+ Op plus(&d_solver, ADD);
ASSERT_FALSE(plus.isIndexed());
ASSERT_THROW(plus.getIndices<uint32_t>(), CVC5ApiException);
- ASSERT_EQ(plus, d_solver.mkOp(PLUS));
+ ASSERT_EQ(plus, d_solver.mkOp(ADD));
}
} // namespace test
} // namespace cvc5
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(PLUS, x, y), 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(PLUS, y, z), zero),
+ d_solver.mkTerm(GT, d_solver.mkTerm(ADD, y, z), zero),
d_solver.mkTerm(LT, z, zero));
Term output;
// Call the interpolation api, while the resulting interpolant is the output
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(PLUS, x, y), 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(PLUS, y, z), zero),
+ d_solver.mkTerm(GT, d_solver.mkTerm(ADD, y, z), zero),
d_solver.mkTerm(LT, z, zero));
Term output;
d_solver.getInterpolant(conj, output);
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(PLUS, f_x, 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));
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(PLUS, f_x, 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);
ASSERT_NO_THROW(d_solver.simplify(i2));
ASSERT_NE(i1, i2);
ASSERT_NE(i1, d_solver.simplify(i2));
- Term i3 = d_solver.mkTerm(PLUS, 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));
// 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(PLUS, f_x, 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
// 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(PLUS, f_x, 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
ASSERT_NO_THROW(f_x.getKind());
Term f_y = d_solver.mkTerm(APPLY_UF, f, y);
ASSERT_NO_THROW(f_y.getKind());
- Term sum = d_solver.mkTerm(PLUS, 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);
ASSERT_NO_THROW(p_0.getKind());
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(PLUS, 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);
ASSERT_THROW(zero.notTerm(), CVC5ApiException);
Term f_x = d_solver.mkTerm(APPLY_UF, f, x);
ASSERT_THROW(f_x.notTerm(), CVC5ApiException);
- Term sum = d_solver.mkTerm(PLUS, 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);
ASSERT_NO_THROW(p_0.notTerm());
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(PLUS, 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(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(PLUS, 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(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(PLUS, 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(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(PLUS, 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_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(PLUS, 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);
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(PLUS, 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);
TEST_F(TestApiBlackTerm, termCompare)
{
Term t1 = d_solver.mkInteger(1);
- Term t2 = d_solver.mkTerm(PLUS, d_solver.mkInteger(2), d_solver.mkInteger(2));
- Term t3 = d_solver.mkTerm(PLUS, 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(PLUS, 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;
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(PLUS, x, x);
- Term onepone = d_solver.mkTerm(PLUS, 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(PLUS, x, y);
- Term xpone = d_solver.mkTerm(PLUS, 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);
@Test void opFromKind()
{
- assertDoesNotThrow(() -> d_solver.mkOp(PLUS));
+ assertDoesNotThrow(() -> d_solver.mkOp(ADD));
assertThrows(CVC5ApiException.class, () -> d_solver.mkOp(BITVECTOR_EXTRACT));
}
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(PLUS, x, y), 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(PLUS, y, z), zero), d_solver.mkTerm(LT, z, zero));
+ OR, d_solver.mkTerm(GT, d_solver.mkTerm(ADD, y, z), zero), d_solver.mkTerm(LT, z, zero));
Term output = d_solver.getNullTerm();
// Call the interpolation api, while the resulting interpolant is the output
d_solver.getInterpolant(conj, output);
Term y = d_solver.mkConst(intSort, "y");
Term z = d_solver.mkConst(intSort, "z");
- d_solver.assertFormula(d_solver.mkTerm(GT, d_solver.mkTerm(PLUS, x, y), zero));
+ d_solver.assertFormula(d_solver.mkTerm(GT, d_solver.mkTerm(ADD, x, y), zero));
d_solver.assertFormula(d_solver.mkTerm(LT, x, zero));
Term conj = d_solver.mkTerm(
- OR, d_solver.mkTerm(GT, d_solver.mkTerm(PLUS, y, z), zero), d_solver.mkTerm(LT, z, zero));
+ OR, d_solver.mkTerm(GT, d_solver.mkTerm(ADD, y, z), zero), d_solver.mkTerm(LT, z, zero));
Term output = d_solver.getNullTerm();
d_solver.getInterpolant(conj, output);
Term output2 = d_solver.getNullTerm();
Term one = d_solver.mkInteger(1);
Term f_x = d_solver.mkTerm(Kind.APPLY_UF, f, x);
Term f_y = d_solver.mkTerm(Kind.APPLY_UF, f, y);
- Term sum = d_solver.mkTerm(Kind.PLUS, f_x, f_y);
+ Term sum = d_solver.mkTerm(Kind.ADD, f_x, f_y);
Term p_0 = d_solver.mkTerm(Kind.APPLY_UF, p, zero);
Term p_f_y = d_solver.mkTerm(APPLY_UF, p, f_y);
d_solver.assertFormula(d_solver.mkTerm(Kind.GT, zero, f_x));
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(PLUS, f_x, 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);
assertDoesNotThrow(() -> d_solver.simplify(i2));
assertNotEquals(i1, i2);
assertNotEquals(i1, d_solver.simplify(i2));
- Term i3 = d_solver.mkTerm(PLUS, i1, d_solver.mkInteger(0));
+ Term i3 = d_solver.mkTerm(ADD, i1, d_solver.mkInteger(0));
assertDoesNotThrow(() -> d_solver.simplify(i3));
assertNotEquals(i1, i3);
assertEquals(i1, d_solver.simplify(i3));
// 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(PLUS, f_x, 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
// 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(PLUS, f_x, 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
assertDoesNotThrow(() -> f_x.getKind());
Term f_y = d_solver.mkTerm(APPLY_UF, f, y);
assertDoesNotThrow(() -> f_y.getKind());
- Term sum = d_solver.mkTerm(PLUS, f_x, f_y);
+ Term sum = d_solver.mkTerm(ADD, f_x, f_y);
assertDoesNotThrow(() -> sum.getKind());
Term p_0 = d_solver.mkTerm(APPLY_UF, p, zero);
assertDoesNotThrow(() -> p_0.getKind());
Term f_y = d_solver.mkTerm(APPLY_UF, f, y);
assertDoesNotThrow(() -> f_y.getSort());
assertEquals(f_y.getSort(), intSort);
- Term sum = d_solver.mkTerm(PLUS, f_x, f_y);
+ Term sum = d_solver.mkTerm(ADD, f_x, f_y);
assertDoesNotThrow(() -> sum.getSort());
assertEquals(sum.getSort(), intSort);
Term p_0 = d_solver.mkTerm(APPLY_UF, p, zero);
assertThrows(CVC5ApiException.class, () -> zero.notTerm());
Term f_x = d_solver.mkTerm(APPLY_UF, f, x);
assertThrows(CVC5ApiException.class, () -> f_x.notTerm());
- Term sum = d_solver.mkTerm(PLUS, f_x, f_x);
+ Term sum = d_solver.mkTerm(ADD, f_x, f_x);
assertThrows(CVC5ApiException.class, () -> sum.notTerm());
Term p_0 = d_solver.mkTerm(APPLY_UF, p, zero);
assertDoesNotThrow(() -> p_0.notTerm());
assertThrows(CVC5ApiException.class, () -> f_x.andTerm(p));
assertThrows(CVC5ApiException.class, () -> f_x.andTerm(zero));
assertThrows(CVC5ApiException.class, () -> f_x.andTerm(f_x));
- Term sum = d_solver.mkTerm(PLUS, f_x, f_x);
+ Term sum = d_solver.mkTerm(ADD, f_x, f_x);
assertThrows(CVC5ApiException.class, () -> sum.andTerm(b));
assertThrows(CVC5ApiException.class, () -> sum.andTerm(x));
assertThrows(CVC5ApiException.class, () -> sum.andTerm(f));
assertThrows(CVC5ApiException.class, () -> f_x.orTerm(p));
assertThrows(CVC5ApiException.class, () -> f_x.orTerm(zero));
assertThrows(CVC5ApiException.class, () -> f_x.orTerm(f_x));
- Term sum = d_solver.mkTerm(PLUS, f_x, f_x);
+ Term sum = d_solver.mkTerm(ADD, f_x, f_x);
assertThrows(CVC5ApiException.class, () -> sum.orTerm(b));
assertThrows(CVC5ApiException.class, () -> sum.orTerm(x));
assertThrows(CVC5ApiException.class, () -> sum.orTerm(f));
assertThrows(CVC5ApiException.class, () -> f_x.xorTerm(p));
assertThrows(CVC5ApiException.class, () -> f_x.xorTerm(zero));
assertThrows(CVC5ApiException.class, () -> f_x.xorTerm(f_x));
- Term sum = d_solver.mkTerm(PLUS, f_x, f_x);
+ Term sum = d_solver.mkTerm(ADD, f_x, f_x);
assertThrows(CVC5ApiException.class, () -> sum.xorTerm(b));
assertThrows(CVC5ApiException.class, () -> sum.xorTerm(x));
assertThrows(CVC5ApiException.class, () -> sum.xorTerm(f));
assertThrows(CVC5ApiException.class, () -> f_x.eqTerm(p));
assertDoesNotThrow(() -> f_x.eqTerm(zero));
assertDoesNotThrow(() -> f_x.eqTerm(f_x));
- Term sum = d_solver.mkTerm(PLUS, f_x, f_x);
+ Term sum = d_solver.mkTerm(ADD, f_x, f_x);
assertThrows(CVC5ApiException.class, () -> sum.eqTerm(b));
assertThrows(CVC5ApiException.class, () -> sum.eqTerm(x));
assertThrows(CVC5ApiException.class, () -> sum.eqTerm(f));
assertThrows(CVC5ApiException.class, () -> f_x.impTerm(p));
assertThrows(CVC5ApiException.class, () -> f_x.impTerm(zero));
assertThrows(CVC5ApiException.class, () -> f_x.impTerm(f_x));
- Term sum = d_solver.mkTerm(PLUS, f_x, f_x);
+ Term sum = d_solver.mkTerm(ADD, f_x, f_x);
assertThrows(CVC5ApiException.class, () -> sum.impTerm(b));
assertThrows(CVC5ApiException.class, () -> sum.impTerm(x));
assertThrows(CVC5ApiException.class, () -> sum.impTerm(f));
Term f_x = d_solver.mkTerm(APPLY_UF, f, x);
assertThrows(CVC5ApiException.class, () -> f_x.iteTerm(b, b));
assertThrows(CVC5ApiException.class, () -> f_x.iteTerm(b, x));
- Term sum = d_solver.mkTerm(PLUS, f_x, f_x);
+ Term sum = d_solver.mkTerm(ADD, f_x, f_x);
assertThrows(CVC5ApiException.class, () -> sum.iteTerm(x, x));
assertThrows(CVC5ApiException.class, () -> sum.iteTerm(b, x));
Term p_0 = d_solver.mkTerm(APPLY_UF, p, zero);
@Test void termCompare()
{
Term t1 = d_solver.mkInteger(1);
- Term t2 = d_solver.mkTerm(PLUS, d_solver.mkInteger(2), d_solver.mkInteger(2));
- Term t3 = d_solver.mkTerm(PLUS, 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));
assertTrue(t2.compareTo(t3) >= 0);
assertTrue(t2.compareTo(t3) <= 0);
assertTrue((t1.compareTo(t2) > 0) != (t1.compareTo(t2) < 0));
{
// simple term 2+3
Term two = d_solver.mkInteger(2);
- Term t1 = d_solver.mkTerm(PLUS, two, d_solver.mkInteger(3));
+ Term t1 = d_solver.mkTerm(ADD, two, d_solver.mkInteger(3));
assertEquals(t1.getChild(0), two);
assertEquals(t1.getNumChildren(), 2);
Term tnull = d_solver.getNullTerm();
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(PLUS, x, x);
- Term onepone = d_solver.mkTerm(PLUS, one, one);
+ Term xpx = d_solver.mkTerm(ADD, x, x);
+ Term onepone = d_solver.mkTerm(ADD, one, one);
assertEquals(xpx.substitute(x, one), onepone);
assertEquals(onepone.substitute(one, x), xpx);
// simultaneous substitution
Term y = d_solver.mkConst(d_solver.getIntegerSort(), "y");
- Term xpy = d_solver.mkTerm(PLUS, x, y);
- Term xpone = d_solver.mkTerm(PLUS, y, one);
+ Term xpy = d_solver.mkTerm(ADD, x, y);
+ Term xpone = d_solver.mkTerm(ADD, y, one);
List<Term> es = new ArrayList<>();
List<Term> rs = new ArrayList<>();
es.add(x);
def test_op_from_kind(solver):
- solver.mkOp(Kind.Plus)
+ solver.mkOp(Kind.Add)
with pytest.raises(RuntimeError):
solver.mkOp(Kind.BVExtract)
def test_get_num_indices(solver):
- plus = solver.mkOp(Kind.Plus)
+ plus = solver.mkOp(Kind.Add)
divisible = solver.mkOp(Kind.Divisible, 4)
bitvector_repeat = solver.mkOp(Kind.BVRepeat, 5)
bitvector_zero_extend = solver.mkOp(Kind.BVZeroExtend, 6)
one = solver.mkInteger(1)
f_x = solver.mkTerm(Kind.ApplyUf, f, x)
f_y = solver.mkTerm(Kind.ApplyUf, f, y)
- summ = solver.mkTerm(Kind.Plus, f_x, f_y)
+ summ = solver.mkTerm(Kind.Add, f_x, f_y)
p_0 = solver.mkTerm(Kind.ApplyUf, p, zero)
p_f_y = solver.mkTerm(Kind.ApplyUf, p, f_y)
solver.assertFormula(solver.mkTerm(Kind.Gt, zero, f_x))
one = solver.mkInteger(1)
f_x = solver.mkTerm(Kind.ApplyUf, f, x)
f_y = solver.mkTerm(Kind.ApplyUf, f, y)
- summ = solver.mkTerm(Kind.Plus, f_x, f_y)
+ summ = solver.mkTerm(Kind.Add, f_x, f_y)
p_0 = solver.mkTerm(Kind.ApplyUf, p, zero)
p_f_y = solver.mkTerm(Kind.ApplyUf, p, f_y)
solver.simplify(i2)
assert i1 != i2
assert i1 != solver.simplify(i2)
- i3 = solver.mkTerm(Kind.Plus, i1, solver.mkInteger(0))
+ i3 = solver.mkTerm(Kind.Add, i1, solver.mkInteger(0))
solver.simplify(i3)
assert i1 != i3
assert i1 == solver.simplify(i3)
# Terms
f_x = solver.mkTerm(Kind.ApplyUf, f, x)
f_y = solver.mkTerm(Kind.ApplyUf, f, y)
- summ = solver.mkTerm(Kind.Plus, f_x, f_y)
+ summ = solver.mkTerm(Kind.Add, f_x, f_y)
p_0 = solver.mkTerm(Kind.ApplyUf, p, zero)
p_f_y = solver.mkTerm(Kind.ApplyUf, p, f_y)
# Assertions
# Terms
f_x = solver.mkTerm(Kind.ApplyUf, f, x)
f_y = solver.mkTerm(Kind.ApplyUf, f, y)
- summ = solver.mkTerm(Kind.Plus, f_x, f_y)
+ summ = solver.mkTerm(Kind.Add, f_x, f_y)
p_0 = solver.mkTerm(Kind.ApplyUf, p, zero)
p_f_y = solver.mkTerm(Kind.ApplyUf, p, f_y)
# Assertions
y = solver.mkConst(intSort, "y")
z = solver.mkConst(intSort, "z")
- solver.assertFormula(solver.mkTerm(Kind.Gt, solver.mkTerm(Kind.Plus, x, y), zero))
+ solver.assertFormula(solver.mkTerm(
+ Kind.Gt, solver.mkTerm(Kind.Add, x, y), zero))
solver.assertFormula(solver.mkTerm(Kind.Lt, x, zero))
- conj = solver.mkTerm(Kind.Or, solver.mkTerm(Kind.Gt, solver.mkTerm(Kind.Plus, y, z), zero), solver.mkTerm(Kind.Lt, z, zero))
+ conj = solver.mkTerm(
+ Kind.Or,
+ solver.mkTerm(Kind.Gt, solver.mkTerm(Kind.Add, y, z), zero),
+ solver.mkTerm(Kind.Lt, z, zero))
output = cvc5.Term(solver)
solver.getInterpolant(conj, output)
assert output.getSort().isBoolean()
y = solver.mkConst(intSort, "y")
z = solver.mkConst(intSort, "z")
- solver.assertFormula(solver.mkTerm(Kind.Gt, solver.mkTerm(Kind.Plus, x, y), zero))
+ solver.assertFormula(solver.mkTerm(
+ Kind.Gt, solver.mkTerm(Kind.Add, x, y), zero))
solver.assertFormula(solver.mkTerm(Kind.Lt, x, zero))
- conj = solver.mkTerm(Kind.Or, solver.mkTerm(Kind.Gt, solver.mkTerm(Kind.Plus, y, z), zero), solver.mkTerm(Kind.Lt, z, zero))
+ conj = solver.mkTerm(
+ Kind.Or,
+ solver.mkTerm(Kind.Gt, solver.mkTerm(Kind.Add, y, z), zero),
+ solver.mkTerm(Kind.Lt, z, zero))
output = cvc5.Term(solver)
solver.getInterpolant(conj, output)
output2 = cvc5.Term(solver)
f_x.getKind()
f_y = solver.mkTerm(Kind.ApplyUf, f, y)
f_y.getKind()
- sum = solver.mkTerm(Kind.Plus, f_x, f_y)
+ sum = solver.mkTerm(Kind.Add, f_x, f_y)
sum.getKind()
p_0 = solver.mkTerm(Kind.ApplyUf, p, zero)
p_0.getKind()
f_y = solver.mkTerm(Kind.ApplyUf, f, y)
f_y.getSort()
assert f_y.getSort() == intSort
- sum = solver.mkTerm(Kind.Plus, f_x, f_y)
+ sum = solver.mkTerm(Kind.Add, f_x, f_y)
sum.getSort()
assert sum.getSort() == intSort
p_0 = solver.mkTerm(Kind.ApplyUf, p, zero)
f_x = solver.mkTerm(Kind.ApplyUf, f, x)
with pytest.raises(RuntimeError):
f_x.notTerm()
- sum = solver.mkTerm(Kind.Plus, f_x, f_x)
+ sum = solver.mkTerm(Kind.Add, f_x, f_x)
with pytest.raises(RuntimeError):
sum.notTerm()
p_0 = solver.mkTerm(Kind.ApplyUf, p, zero)
f_x.andTerm(zero)
with pytest.raises(RuntimeError):
f_x.andTerm(f_x)
- sum = solver.mkTerm(Kind.Plus, f_x, f_x)
+ sum = solver.mkTerm(Kind.Add, f_x, f_x)
with pytest.raises(RuntimeError):
sum.andTerm(b)
with pytest.raises(RuntimeError):
f_x.orTerm(zero)
with pytest.raises(RuntimeError):
f_x.orTerm(f_x)
- sum = solver.mkTerm(Kind.Plus, f_x, f_x)
+ sum = solver.mkTerm(Kind.Add, f_x, f_x)
with pytest.raises(RuntimeError):
sum.orTerm(b)
with pytest.raises(RuntimeError):
f_x.xorTerm(zero)
with pytest.raises(RuntimeError):
f_x.xorTerm(f_x)
- sum = solver.mkTerm(Kind.Plus, f_x, f_x)
+ sum = solver.mkTerm(Kind.Add, f_x, f_x)
with pytest.raises(RuntimeError):
sum.xorTerm(b)
with pytest.raises(RuntimeError):
f_x.eqTerm(p)
f_x.eqTerm(zero)
f_x.eqTerm(f_x)
- sum = solver.mkTerm(Kind.Plus, f_x, f_x)
+ sum = solver.mkTerm(Kind.Add, f_x, f_x)
with pytest.raises(RuntimeError):
sum.eqTerm(b)
with pytest.raises(RuntimeError):
f_x.impTerm(zero)
with pytest.raises(RuntimeError):
f_x.impTerm(f_x)
- sum = solver.mkTerm(Kind.Plus, f_x, f_x)
+ sum = solver.mkTerm(Kind.Add, f_x, f_x)
with pytest.raises(RuntimeError):
sum.impTerm(b)
with pytest.raises(RuntimeError):
f_x.iteTerm(b, b)
with pytest.raises(RuntimeError):
f_x.iteTerm(b, x)
- sum = solver.mkTerm(Kind.Plus, f_x, f_x)
+ sum = solver.mkTerm(Kind.Add, f_x, f_x)
with pytest.raises(RuntimeError):
sum.iteTerm(x, x)
with pytest.raises(RuntimeError):
x = solver.mkConst(solver.getIntegerSort(), "x")
one = solver.mkInteger(1)
ttrue = solver.mkTrue()
- xpx = solver.mkTerm(Kind.Plus, x, x)
- onepone = solver.mkTerm(Kind.Plus, one, one)
+ xpx = solver.mkTerm(Kind.Add, x, x)
+ onepone = solver.mkTerm(Kind.Add, one, one)
assert xpx.substitute(x, one) == onepone
assert onepone.substitute(one, x) == xpx
# simultaneous substitution
y = solver.mkConst(solver.getIntegerSort(), "y")
- xpy = solver.mkTerm(Kind.Plus, x, y)
- xpone = solver.mkTerm(Kind.Plus, y, one)
+ xpy = solver.mkTerm(Kind.Add, x, y)
+ xpone = solver.mkTerm(Kind.Add, y, one)
es = []
rs = []
es.append(x)
def test_term_compare(solver):
t1 = solver.mkInteger(1)
- t2 = solver.mkTerm(Kind.Plus, solver.mkInteger(2), solver.mkInteger(2))
- t3 = solver.mkTerm(Kind.Plus, solver.mkInteger(2), solver.mkInteger(2))
+ t2 = solver.mkTerm(Kind.Add, solver.mkInteger(2), solver.mkInteger(2))
+ t3 = solver.mkTerm(Kind.Add, solver.mkInteger(2), solver.mkInteger(2))
assert t2 >= t3
assert t2 <= t3
assert (t1 > t2) != (t1 < t2)
def test_term_children(solver):
# simple term 2+3
two = solver.mkInteger(2)
- t1 = solver.mkTerm(Kind.Plus, two, solver.mkInteger(3))
+ t1 = solver.mkTerm(Kind.Add, two, solver.mkInteger(3))
assert t1[0] == two
assert t1.getNumChildren() == 2
tnull = Term(solver)
Node var = d_nodeManager->mkBoundVar(*d_intTypeNode);
std::vector<Node> vars;
vars.push_back(var);
- Node sum = d_nodeManager->mkNode(PLUS, var, var);
+ Node sum = d_nodeManager->mkNode(ADD, var, var);
Node qeq = d_nodeManager->mkNode(EQUAL, x, sum);
Node bvl = d_nodeManager->mkNode(BOUND_VAR_LIST, vars);
Node right = d_nodeManager->mkNode(EXISTS, bvl, qeq);
// create test formula
Node x = d_skolemManager->mkDummySkolem("x", d_nodeManager->integerType());
- Node plus = d_nodeManager->mkNode(PLUS, x, x);
+ Node plus = d_nodeManager->mkNode(ADD, x, x);
Node mul = d_nodeManager->mkNode(MULT, x, x);
Node eq1 = d_nodeManager->mkNode(EQUAL, plus, mul);
// in integers, we should only have plus and mult as operators
ASSERT_EQ(result[*d_intTypeNode].size(), 2);
- ASSERT_NE(result[*d_intTypeNode].find(d_nodeManager->operatorOf(PLUS)),
+ ASSERT_NE(result[*d_intTypeNode].find(d_nodeManager->operatorOf(ADD)),
result[*d_intTypeNode].end());
ASSERT_NE(result[*d_intTypeNode].find(d_nodeManager->operatorOf(MULT)),
result[*d_intTypeNode].end());
{
{
Node x = d_nodeManager->mkBoundVar(*d_realTypeNode);
- Node n = d_nodeManager->mkNode(Kind::PLUS, x, x);
+ Node n = d_nodeManager->mkNode(Kind::ADD, x, x);
EXPECT_FALSE(expr::algorithm::canFlatten(n));
- EXPECT_FALSE(expr::algorithm::canFlatten(n, Kind::PLUS));
+ EXPECT_FALSE(expr::algorithm::canFlatten(n, Kind::ADD));
EXPECT_FALSE(expr::algorithm::canFlatten(n, Kind::MULT));
- EXPECT_FALSE(expr::algorithm::canFlatten(n, Kind::PLUS, Kind::MULT));
+ EXPECT_FALSE(expr::algorithm::canFlatten(n, Kind::ADD, Kind::MULT));
EXPECT_EQ(expr::algorithm::flatten(n), n);
- EXPECT_EQ(expr::algorithm::flatten(n, Kind::PLUS), n);
+ EXPECT_EQ(expr::algorithm::flatten(n, Kind::ADD), n);
EXPECT_EQ(expr::algorithm::flatten(n, Kind::MULT), n);
- EXPECT_EQ(expr::algorithm::flatten(n, Kind::PLUS, Kind::MULT), n);
+ EXPECT_EQ(expr::algorithm::flatten(n, Kind::ADD, Kind::MULT), n);
{
std::vector<TNode> children;
}
{
std::vector<TNode> children;
- expr::algorithm::flatten(n, children, Kind::PLUS);
+ expr::algorithm::flatten(n, children, Kind::ADD);
EXPECT_EQ(children.size(), 2);
EXPECT_EQ(children[0], x);
EXPECT_EQ(children[1], x);
}
{
std::vector<TNode> children;
- expr::algorithm::flatten(n, children, Kind::PLUS, Kind::MULT);
+ expr::algorithm::flatten(n, children, Kind::ADD, Kind::MULT);
EXPECT_EQ(children.size(), 2);
EXPECT_EQ(children[0], x);
EXPECT_EQ(children[1], x);
{
Node x = d_nodeManager->mkBoundVar(*d_realTypeNode);
Node n = d_nodeManager->mkNode(
- Kind::PLUS, x, d_nodeManager->mkNode(Kind::PLUS, x, x));
+ Kind::ADD, x, d_nodeManager->mkNode(Kind::ADD, x, x));
EXPECT_TRUE(expr::algorithm::canFlatten(n));
- EXPECT_TRUE(expr::algorithm::canFlatten(n, Kind::PLUS));
+ EXPECT_TRUE(expr::algorithm::canFlatten(n, Kind::ADD));
EXPECT_FALSE(expr::algorithm::canFlatten(n, Kind::MULT));
- EXPECT_TRUE(expr::algorithm::canFlatten(n, Kind::PLUS, Kind::MULT));
+ EXPECT_TRUE(expr::algorithm::canFlatten(n, Kind::ADD, Kind::MULT));
EXPECT_NE(expr::algorithm::flatten(n), n);
- EXPECT_NE(expr::algorithm::flatten(n, Kind::PLUS), n);
+ EXPECT_NE(expr::algorithm::flatten(n, Kind::ADD), n);
EXPECT_EQ(expr::algorithm::flatten(n, Kind::MULT), n);
- EXPECT_NE(expr::algorithm::flatten(n, Kind::PLUS, Kind::MULT), n);
+ EXPECT_NE(expr::algorithm::flatten(n, Kind::ADD, Kind::MULT), n);
{
std::vector<TNode> children;
}
{
std::vector<TNode> children;
- expr::algorithm::flatten(n, children, Kind::PLUS);
+ expr::algorithm::flatten(n, children, Kind::ADD);
EXPECT_EQ(children.size(), 3);
EXPECT_EQ(children[0], x);
EXPECT_EQ(children[1], x);
}
{
std::vector<TNode> children;
- expr::algorithm::flatten(n, children, Kind::PLUS, Kind::MULT);
+ expr::algorithm::flatten(n, children, Kind::ADD, Kind::MULT);
EXPECT_EQ(children.size(), 3);
EXPECT_EQ(children[0], x);
EXPECT_EQ(children[1], x);
{
Node x = d_nodeManager->mkBoundVar(*d_realTypeNode);
Node n = d_nodeManager->mkNode(
- Kind::PLUS, x, d_nodeManager->mkNode(Kind::MULT, x, x));
+ Kind::ADD, x, d_nodeManager->mkNode(Kind::MULT, x, x));
EXPECT_FALSE(expr::algorithm::canFlatten(n));
- EXPECT_FALSE(expr::algorithm::canFlatten(n, Kind::PLUS));
+ EXPECT_FALSE(expr::algorithm::canFlatten(n, Kind::ADD));
EXPECT_FALSE(expr::algorithm::canFlatten(n, Kind::MULT));
- EXPECT_TRUE(expr::algorithm::canFlatten(n, Kind::PLUS, Kind::MULT));
+ EXPECT_TRUE(expr::algorithm::canFlatten(n, Kind::ADD, Kind::MULT));
EXPECT_EQ(expr::algorithm::flatten(n), n);
- EXPECT_EQ(expr::algorithm::flatten(n, Kind::PLUS), n);
+ EXPECT_EQ(expr::algorithm::flatten(n, Kind::ADD), n);
EXPECT_EQ(expr::algorithm::flatten(n, Kind::MULT), n);
- EXPECT_NE(expr::algorithm::flatten(n, Kind::PLUS, Kind::MULT), n);
+ EXPECT_NE(expr::algorithm::flatten(n, Kind::ADD, Kind::MULT), n);
{
std::vector<TNode> children;
}
{
std::vector<TNode> children;
- expr::algorithm::flatten(n, children, Kind::PLUS);
+ expr::algorithm::flatten(n, children, Kind::ADD);
EXPECT_EQ(children.size(), 2);
EXPECT_EQ(children[0], x);
EXPECT_EQ(children[1], n[1]);
}
{
std::vector<TNode> children;
- expr::algorithm::flatten(n, children, Kind::PLUS, Kind::MULT);
+ expr::algorithm::flatten(n, children, Kind::ADD, Kind::MULT);
EXPECT_EQ(children.size(), 3);
EXPECT_EQ(children[0], x);
EXPECT_EQ(children[1], x);
Node x = d_skolemManager->mkDummySkolem("x", d_nodeManager->realType());
Node y = d_skolemManager->mkDummySkolem("y", d_nodeManager->realType());
- n = d_nodeManager->mkNode(PLUS, x, y);
- ASSERT_EQ(PLUS, n.getKind());
+ n = d_nodeManager->mkNode(ADD, x, y);
+ ASSERT_EQ(ADD, n.getKind());
n = d_nodeManager->mkNode(NEG, x);
ASSERT_EQ(NEG, n.getKind());
Node x = d_skolemManager->mkDummySkolem("x", integerType);
Node y = d_skolemManager->mkDummySkolem("y", integerType);
Node z = d_skolemManager->mkDummySkolem("z", integerType);
- Node plus_x_y_z = d_nodeManager->mkNode(kind::PLUS, x, y, z);
+ Node plus_x_y_z = d_nodeManager->mkNode(kind::ADD, x, y, z);
Node x_minus_y = d_nodeManager->mkNode(kind::SUB, x, y);
{ // iterator
- Node::kinded_iterator i = plus_x_y_z.begin(PLUS);
+ Node::kinded_iterator i = plus_x_y_z.begin(ADD);
ASSERT_EQ(*i++, x);
ASSERT_EQ(*i++, y);
ASSERT_EQ(*i++, z);
- ASSERT_TRUE(i == plus_x_y_z.end(PLUS));
+ ASSERT_TRUE(i == plus_x_y_z.end(ADD));
- i = x.begin(PLUS);
+ i = x.begin(ADD);
ASSERT_EQ(*i++, x);
- ASSERT_TRUE(i == x.end(PLUS));
+ ASSERT_TRUE(i == x.end(ADD));
}
}
{
const std::vector<Node> skolems =
makeNSkolemNodes(d_nodeManager, 3, d_nodeManager->integerType());
- Node add = d_nodeManager->mkNode(kind::PLUS, skolems);
+ Node add = d_nodeManager->mkNode(kind::ADD, skolems);
std::vector<Node> children;
for (Node child : add)
{
{
const std::vector<Node> skolems =
makeNSkolemNodes(d_nodeManager, 3, d_nodeManager->integerType());
- Node add = d_nodeManager->mkNode(kind::PLUS, skolems);
+ Node add = d_nodeManager->mkNode(kind::ADD, skolems);
std::vector<TNode> children;
for (TNode child : add)
{
{
const std::vector<Node> skolems =
makeNSkolemNodes(d_nodeManager, 3, d_nodeManager->integerType());
- Node add_node = d_nodeManager->mkNode(kind::PLUS, skolems);
+ Node add_node = d_nodeManager->mkNode(kind::ADD, skolems);
TNode add_tnode = add_node;
std::vector<Node> children;
for (Node child : add_tnode)
{
const std::vector<Node> skolems =
makeNSkolemNodes(d_nodeManager, 3, d_nodeManager->integerType());
- Node add_node = d_nodeManager->mkNode(kind::PLUS, skolems);
+ Node add_node = d_nodeManager->mkNode(kind::ADD, skolems);
TNode add_tnode = add_node;
std::vector<TNode> children;
for (TNode child : add_tnode)
noKind << x << x;
ASSERT_EQ(noKind.getKind(), UNDEFINED_KIND);
- noKind << PLUS;
- ASSERT_EQ(noKind.getKind(), PLUS);
+ noKind << ADD;
+ ASSERT_EQ(noKind.getKind(), ADD);
Node n = noKind;
#ifdef CVC5_ASSERTIONS
ASSERT_DEATH(noKind.getKind(), "!isUsed\\(\\)");
#endif
- NodeBuilder spec(PLUS);
- ASSERT_EQ(spec.getKind(), PLUS);
+ NodeBuilder spec(ADD);
+ ASSERT_EQ(spec.getKind(), ADD);
spec << x << x;
- ASSERT_EQ(spec.getKind(), PLUS);
+ ASSERT_EQ(spec.getKind(), ADD);
}
TEST_F(TestNodeBlackNodeBuilder, getNumChildren)
ASSERT_DEATH(nb.getNumChildren(), "getKind\\(\\) != kind::UNDEFINED_KIND");
#endif
- nb << PLUS << x << x;
+ nb << ADD << x << x;
ASSERT_EQ(nb.getNumChildren(), 2u);
nb << x << x;
ASSERT_DEATH(nb.getNumChildren(), "getKind\\(\\) != kind::UNDEFINED_KIND");
#endif
- nb.clear(PLUS);
+ nb.clear(ADD);
ASSERT_EQ(nb.getNumChildren(), 0u);
nb << x << x << x;
ASSERT_EQ(nb.getNumChildren(), 6u);
#ifdef CVC5_ASSERTIONS
- ASSERT_DEATH(nb << PLUS, "getKind\\(\\) == kind::UNDEFINED_KIND");
+ ASSERT_DEATH(nb << ADD, "getKind\\(\\) == kind::UNDEFINED_KIND");
Node n = nb;
ASSERT_DEATH(nb.getNumChildren(), "!isUsed\\(\\)");
#endif
{
#ifdef CVC5_ASSERTIONS
NodeBuilder spec(d_specKind);
- ASSERT_DEATH(spec << PLUS, "can't redefine the Kind of a NodeBuilder");
+ ASSERT_DEATH(spec << ADD, "can't redefine the Kind of a NodeBuilder");
#endif
NodeBuilder noSpec;
NodeBuilder nb(d_specKind);
nb << d_nodeManager->mkConst(true) << d_nodeManager->mkConst(false);
- nb.clear(PLUS);
+ nb.clear(ADD);
#ifdef CVC5_ASSERTIONS
Node n;
- ASSERT_DEATH(n = nb, "Nodes with kind PLUS must have at least 2 children");
- nb.clear(PLUS);
+ ASSERT_DEATH(n = nb, "Nodes with kind ADD must have at least 2 children");
+ nb.clear(ADD);
#endif
#ifdef CVC5_ASSERTIONS
- ASSERT_DEATH(nb << PLUS, "can't redefine the Kind of a NodeBuilder");
+ ASSERT_DEATH(nb << ADD, "can't redefine the Kind of a NodeBuilder");
#endif
NodeBuilder testRef;
#ifdef CVC5_ASSERTIONS
NodeBuilder testTwo;
- ASSERT_DEATH(testTwo << d_specKind << PLUS,
+ ASSERT_DEATH(testTwo << d_specKind << ADD,
"can't redefine the Kind of a NodeBuilder");
#endif
Node p = d_nodeManager->mkNode(
EQUAL,
d_nodeManager->mkConst<Rational>(CONST_RATIONAL, 0),
- d_nodeManager->mkNode(PLUS, r, d_nodeManager->mkNode(NEG, s), t));
+ d_nodeManager->mkNode(ADD, r, d_nodeManager->mkNode(NEG, s), t));
Node q = d_nodeManager->mkNode(AND, x, z, d_nodeManager->mkNode(NOT, y));
#ifdef CVC5_ASSERTIONS
{
Node x = d_nodeManager->mkVar("x", d_nodeManager->integerType());
Node y = d_nodeManager->mkVar("y", d_nodeManager->integerType());
- Node x_plus_y = d_nodeManager->mkNode(PLUS, x, y);
+ Node x_plus_y = d_nodeManager->mkNode(ADD, x, y);
Node two = d_nodeManager->mkConst(CONST_RATIONAL, Rational(2));
Node x_times_2 = d_nodeManager->mkNode(MULT, x, two);
- Node n = d_nodeManager->mkNode(PLUS, x_times_2, x_plus_y, y);
+ Node n = d_nodeManager->mkNode(ADD, x_times_2, x_plus_y, y);
Node::iterator i;
t2 = one;
ASSERT_FALSE(PolyNorm::isArithPolyNorm(t1, t2));
- t1 = d_nodeManager->mkNode(PLUS, x, y);
- t2 = d_nodeManager->mkNode(PLUS, y, d_nodeManager->mkNode(MULT, one, x));
+ t1 = d_nodeManager->mkNode(ADD, x, y);
+ t2 = d_nodeManager->mkNode(ADD, y, d_nodeManager->mkNode(MULT, one, x));
ASSERT_TRUE(PolyNorm::isArithPolyNorm(t1, t2));
- t2 = d_nodeManager->mkNode(PLUS, x, x, y);
+ t2 = d_nodeManager->mkNode(ADD, x, x, y);
ASSERT_FALSE(PolyNorm::isArithPolyNorm(t1, t2));
- t1 = d_nodeManager->mkNode(PLUS, x, d_nodeManager->mkNode(MULT, y, zero));
+ t1 = d_nodeManager->mkNode(ADD, x, d_nodeManager->mkNode(MULT, y, zero));
t2 = x;
ASSERT_TRUE(PolyNorm::isArithPolyNorm(t1, t2));
- t1 = d_nodeManager->mkNode(MULT, y, d_nodeManager->mkNode(PLUS, one, one));
- t2 = d_nodeManager->mkNode(PLUS, y, y);
+ t1 = d_nodeManager->mkNode(MULT, y, d_nodeManager->mkNode(ADD, one, one));
+ t2 = d_nodeManager->mkNode(ADD, y, y);
ASSERT_TRUE(PolyNorm::isArithPolyNorm(t1, t2));
t1 = d_nodeManager->mkNode(MULT,
- d_nodeManager->mkNode(PLUS, one, zero),
- d_nodeManager->mkNode(PLUS, x, y));
- t2 = d_nodeManager->mkNode(PLUS, x, y);
+ d_nodeManager->mkNode(ADD, one, zero),
+ d_nodeManager->mkNode(ADD, x, y));
+ t2 = d_nodeManager->mkNode(ADD, x, y);
ASSERT_TRUE(PolyNorm::isArithPolyNorm(t1, t2));
- t1 = d_nodeManager->mkNode(PLUS, {x, y, z, w, y});
- t2 = d_nodeManager->mkNode(PLUS, {w, y, y, z, x});
+ t1 = d_nodeManager->mkNode(ADD, {x, y, z, w, y});
+ t2 = d_nodeManager->mkNode(ADD, {w, y, y, z, x});
ASSERT_TRUE(PolyNorm::isArithPolyNorm(t1, t2));
t1 = d_nodeManager->mkNode(SUB, t1, t2);
t2 = zero;
ASSERT_TRUE(PolyNorm::isArithPolyNorm(t1, t2));
- t1 = d_nodeManager->mkNode(NEG, d_nodeManager->mkNode(PLUS, x, y));
- t2 = d_nodeManager->mkNode(SUB, zero, d_nodeManager->mkNode(PLUS, y, x));
+ t1 = d_nodeManager->mkNode(NEG, d_nodeManager->mkNode(ADD, x, y));
+ t2 = d_nodeManager->mkNode(SUB, zero, d_nodeManager->mkNode(ADD, y, x));
ASSERT_TRUE(PolyNorm::isArithPolyNorm(t1, t2));
t1 = d_nodeManager->mkNode(MULT, d_nodeManager->mkNode(NEG, x), y);
t2 = d_nodeManager->mkNode(MULT, d_nodeManager->mkNode(NEG, y), x);
ASSERT_TRUE(PolyNorm::isArithPolyNorm(t1, t2));
- t1 = d_nodeManager->mkNode(MULT, x, d_nodeManager->mkNode(PLUS, y, z));
- t2 = d_nodeManager->mkNode(PLUS,
+ t1 = d_nodeManager->mkNode(MULT, x, d_nodeManager->mkNode(ADD, y, z));
+ t2 = d_nodeManager->mkNode(ADD,
d_nodeManager->mkNode(MULT, x, y),
d_nodeManager->mkNode(MULT, z, x));
ASSERT_TRUE(PolyNorm::isArithPolyNorm(t1, t2));
Node t1, t2;
- t1 = d_nodeManager->mkNode(PLUS, x, y, y);
- t2 = d_nodeManager->mkNode(PLUS, y, x, y);
+ t1 = d_nodeManager->mkNode(ADD, x, y, y);
+ t2 = d_nodeManager->mkNode(ADD, y, x, y);
ASSERT_TRUE(PolyNorm::isArithPolyNorm(t1, t2));
t1 = one;
t2 = d_nodeManager->mkNode(MULT, two, half);
ASSERT_TRUE(PolyNorm::isArithPolyNorm(t1, t2));
- t1 = d_nodeManager->mkNode(PLUS, y, x);
+ t1 = d_nodeManager->mkNode(ADD, y, x);
t2 = d_nodeManager->mkNode(
MULT,
- d_nodeManager->mkNode(PLUS,
+ d_nodeManager->mkNode(ADD,
d_nodeManager->mkNode(MULT, half, x),
d_nodeManager->mkNode(MULT, half, y)),
two);
Node a = d_nodeManager->mkConst(::cvc5::String("A"));
Node slen_y = d_nodeManager->mkNode(kind::STRING_LENGTH, y);
- Node x_plus_slen_y = d_nodeManager->mkNode(kind::PLUS, x, slen_y);
+ Node x_plus_slen_y = d_nodeManager->mkNode(kind::ADD, x, slen_y);
Node x_plus_slen_y_eq_zero = d_rewriter->rewrite(
d_nodeManager->mkNode(kind::EQUAL, x_plus_slen_y, zero));
ASSERT_FALSE(ae.checkWithAssumption(x_plus_slen_y_eq_zero, zero, x, true));
Node x_plus_slen_y_plus_z_eq_zero = d_rewriter->rewrite(d_nodeManager->mkNode(
- kind::EQUAL, d_nodeManager->mkNode(kind::PLUS, x_plus_slen_y, z), zero));
+ kind::EQUAL, d_nodeManager->mkNode(kind::ADD, x_plus_slen_y, z), zero));
// x + (str.len y) + z = 0 |= 0 > x --> false
ASSERT_FALSE(
Node x_plus_slen_y_plus_slen_y_eq_zero =
d_rewriter->rewrite(d_nodeManager->mkNode(
kind::EQUAL,
- d_nodeManager->mkNode(kind::PLUS, x_plus_slen_y, slen_y),
+ d_nodeManager->mkNode(kind::ADD, x_plus_slen_y, slen_y),
zero));
// x + (str.len y) + (str.len y) = 0 |= 0 >= x --> true
Node five = d_nodeManager->mkConst(CONST_RATIONAL, Rational(5));
Node six = d_nodeManager->mkConst(CONST_RATIONAL, Rational(6));
- Node x_plus_five = d_nodeManager->mkNode(kind::PLUS, x, five);
+ Node x_plus_five = d_nodeManager->mkNode(kind::ADD, x, five);
Node x_plus_five_lt_six =
d_rewriter->rewrite(d_nodeManager->mkNode(kind::LT, x_plus_five, six));
kind::STRING_SUBSTR,
a,
d_nodeManager->mkNode(
- kind::PLUS, x, d_nodeManager->mkConst(CONST_RATIONAL, Rational(1))),
+ kind::ADD, x, d_nodeManager->mkConst(CONST_RATIONAL, Rational(1))),
x);
sameNormalForm(n, empty);
kind::STRING_SUBSTR,
a,
d_nodeManager->mkNode(
- kind::PLUS, x, d_nodeManager->mkNode(kind::STRING_LENGTH, s)),
+ kind::ADD, x, d_nodeManager->mkNode(kind::STRING_LENGTH, s)),
x);
sameNormalForm(n, empty);
ASSERT_EQ(res, n);
// (str.substr "ABCD" (+ x 3) x) -> ""
- n = d_nodeManager->mkNode(kind::STRING_SUBSTR,
- abcd,
- d_nodeManager->mkNode(kind::PLUS, x, three),
- x);
+ n = d_nodeManager->mkNode(
+ kind::STRING_SUBSTR, abcd, d_nodeManager->mkNode(kind::ADD, x, three), x);
sameNormalForm(n, empty);
// (str.substr "ABCD" (+ x 2) x) -> (str.substr "ABCD" (+ x 2) x)
n = d_nodeManager->mkNode(
- kind::STRING_SUBSTR, abcd, d_nodeManager->mkNode(kind::PLUS, x, two), x);
+ kind::STRING_SUBSTR, abcd, d_nodeManager->mkNode(kind::ADD, x, two), x);
res = sr.rewriteSubstr(n);
sameNormalForm(res, n);
a,
zero);
Node rhs = d_nodeManager->mkNode(
- kind::PLUS,
+ kind::ADD,
two,
d_nodeManager->mkNode(
kind::STRING_INDEXOF,
}
Node operator+(const Node& a, const Node& b)
{
- return nodeManager->mkNode(Kind::PLUS, a, b);
+ return nodeManager->mkNode(Kind::ADD, a, b);
}
Node operator*(const Node& a, const Node& b)
{
d_nodeManager->mkNode(
Kind::EQUAL,
d_nodeManager->mkNode(
- Kind::PLUS,
+ Kind::ADD,
d_nodeManager->mkNode(Kind::NONLINEAR_MULT, a, c),
d_nodeManager->mkConst(CONST_RATIONAL, d_one)),
d_nodeManager->mkConst(CONST_RATIONAL, d_zero))});
RealAlgebraicNumber twosqrt2({-8, 0, 1}, 2, 3);
RealAlgebraicNumber sqrt2({-2, 0, 1}, 1, 3);
Node n = d_nodeManager->mkRealAlgebraicNumber(sqrt2);
- n = d_nodeManager->mkNode(Kind::PLUS, n, n);
+ n = d_nodeManager->mkNode(Kind::ADD, n, n);
n = d_slvEngine->getRewriter()->rewrite(n);
EXPECT_EQ(n.getKind(), Kind::REAL_ALGEBRAIC_NUMBER);
EXPECT_EQ(n.getOperator().getConst<RealAlgebraicNumber>(), twosqrt2);
// (exp (+ 2 + x)) --> (* (exp x) (exp 1) (exp 1))
Node t =
- d_nodeManager->mkNode(EXPONENTIAL, d_nodeManager->mkNode(PLUS, c2, xr))
+ d_nodeManager->mkNode(EXPONENTIAL, d_nodeManager->mkNode(ADD, c2, xr))
.eqNode(c0);
ASSERT_EQ(Rewriter::rewrite(Rewriter::rewrite(t)), Rewriter::rewrite(t));
}
Node n3 = d_nodeManager->mkNode(BAG_CARD, unionDisjointAB);
Node cardA = d_nodeManager->mkNode(BAG_CARD, A);
Node cardB = d_nodeManager->mkNode(BAG_CARD, B);
- Node plus = d_nodeManager->mkNode(PLUS, cardA, cardB);
+ Node plus = d_nodeManager->mkNode(ADD, cardA, cardB);
RewriteResponse response3 = d_rewriter->postRewrite(n3);
ASSERT_TRUE(response3.d_node == plus
&& response3.d_status == REWRITE_AGAIN_FULL);
Node x = d_nodeManager->mkBoundVar("x", d_nodeManager->integerType());
Node y = d_nodeManager->mkBoundVar("y", d_nodeManager->integerType());
Node xy = d_nodeManager->mkNode(BOUND_VAR_LIST, x, y);
- Node sum = d_nodeManager->mkNode(PLUS, x, y);
+ Node sum = d_nodeManager->mkNode(ADD, x, y);
// f(x,y) = 0 for all x, y
Node f = d_nodeManager->mkNode(LAMBDA, xy, zero);
Node y = d_nodeManager->mkVar("y", d_nodeManager->integerType());
Node z = d_nodeManager->mkVar("z", d_nodeManager->integerType());
- // make the expression (PLUS x y (MULT z 0))
+ // make the expression (ADD x y (MULT z 0))
Node zero = d_nodeManager->mkConst(CONST_RATIONAL, Rational("0"));
Node zTimesZero = d_nodeManager->mkNode(MULT, z, zero);
- Node n = d_nodeManager->mkNode(PLUS, x, y, zTimesZero);
+ Node n = d_nodeManager->mkNode(ADD, x, y, zTimesZero);
Node nExpected = n;
Node nOut;
/* Optimization objective:
cost1 + cost2
*/
- Node cost3 = d_nodeManager->mkNode(kind::PLUS, cost1, cost2);
+ Node cost3 = d_nodeManager->mkNode(kind::ADD, cost1, cost2);
d_optslv->addObjective(cost3, OptimizationObjective::MINIMIZE);
ASSERT_THROW(
ArrayStoreAll(d_nodeManager->integerType(),
d_nodeManager->mkNode(
- kind::PLUS,
+ kind::ADD,
d_nodeManager->mkConst(CONST_RATIONAL, Rational(1)),
d_nodeManager->mkConst(CONST_RATIONAL, Rational(0)))),
IllegalArgumentException);
projects / cvc5.git / commitdiff