{MULT, cvc5::Kind::MULT},
{IAND, cvc5::Kind::IAND},
{POW2, cvc5::Kind::POW2},
- {MINUS, cvc5::Kind::MINUS},
- {UMINUS, cvc5::Kind::UMINUS},
+ {MINUS, cvc5::Kind::SUB},
+ {UMINUS, cvc5::Kind::NEG},
{DIVISION, cvc5::Kind::DIVISION},
{INTS_DIVISION, cvc5::Kind::INTS_DIVISION},
{INTS_MODULUS, cvc5::Kind::INTS_MODULUS},
{cvc5::Kind::MULT, MULT},
{cvc5::Kind::IAND, IAND},
{cvc5::Kind::POW2, POW2},
- {cvc5::Kind::MINUS, MINUS},
- {cvc5::Kind::UMINUS, UMINUS},
+ {cvc5::Kind::SUB, MINUS},
+ {cvc5::Kind::NEG, UMINUS},
{cvc5::Kind::DIVISION, DIVISION},
{cvc5::Kind::DIVISION_TOTAL, INTERNAL_KIND},
{cvc5::Kind::INTS_DIVISION, INTS_DIVISION},
newKind = kind::BITVECTOR_MULT;
max = max * 2;
break;
- case kind::MINUS:
+ case kind::SUB:
Assert(children.size() == 2);
newKind = kind::BITVECTOR_SUB;
max = max + 1;
break;
- case kind::UMINUS:
+ case kind::NEG:
Assert(children.size() == 1);
newKind = kind::BITVECTOR_NEG;
max = max + 1;
Node bv2int = nm->mkNode(
kind::ITE,
nm->mkNode(kind::BITVECTOR_SLT, result, nm->mkConst(bvzero)),
- nm->mkNode(kind::UMINUS, negResult),
+ nm->mkNode(kind::NEG, negResult),
nm->mkNode(kind::BITVECTOR_TO_NAT, result));
d_preprocContext->addSubstitution(current, bv2int);
}
Node ret = n;
if (n.getNumChildren() > 0)
{
- if (beneathMult
- && (n.getKind() == kind::PLUS || n.getKind() == kind::MINUS))
+ if (beneathMult && (n.getKind() == kind::PLUS || n.getKind() == kind::SUB))
{
// don't do it if it rewrites to a constant
Node nr = rewrite(n);
case kind::NOT:
case kind::BITVECTOR_NOT:
case kind::BITVECTOR_NEG:
- case kind::UMINUS:
+ case kind::NEG:
++d_numUnconstrainedElim;
Assert(parent[0] == current);
if (currentSub.isNull())
// N-ary operators returning same type requiring at least one child to
// be unconstrained
case kind::PLUS:
- case kind::MINUS:
+ case kind::SUB:
if (current.getType().isInteger() && !parent.getType().isInteger())
{
break;
case kind::ARCCOTANGENT: return "arccot";
case kind::PI: return "real.pi";
case kind::SQRT: return "sqrt";
- case kind::MINUS: return "-";
- case kind::UMINUS: return "-";
+ case kind::SUB: return "-";
+ case kind::NEG: return "-";
case kind::LT: return "<";
case kind::LEQ: return "<=";
case kind::GT: return ">";
vrule = AletheRule::PROD_SIMPLIFY;
break;
}
- case kind::MINUS:
+ case kind::SUB:
{
vrule = AletheRule::MINUS_SIMPLIFY;
break;
}
- case kind::UMINUS:
+ case kind::NEG:
{
vrule = AletheRule::UNARY_MINUS_SIMPLIFY;
break;
ArrayStoreAll storeAll = n.getConst<ArrayStoreAll>();
return nm->mkNode(APPLY_UF, f, convert(storeAll.getValue()));
}
- else if (k == GEQ || k == GT || k == LEQ || k == LT || k == MINUS
+ else if (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 == UMINUS || k == POW
+ || k == INTS_MODULUS_TOTAL || k == NEG || k == POW
|| isIndexedOperatorKind(k))
{
// must give special names to SMT-LIB operators with arithmetic subtyping
- // note that MINUS is not n-ary
+ // note that SUB is not n-ary
// get the macro-apply version of the operator
Node opc = getOperatorOfTerm(n, true);
std::vector<Node> children;
}
// all arithmetic kinds must explicitly deal with real vs int subtyping
if (k == PLUS || k == MULT || k == NONLINEAR_MULT || k == GEQ || k == GT
- || k == LEQ || k == LT || k == MINUS || k == DIVISION
- || k == DIVISION_TOTAL || k == INTS_DIVISION || k == INTS_DIVISION_TOTAL
- || k == INTS_MODULUS || k == INTS_MODULUS_TOTAL || k == UMINUS
- || k == POW)
+ || 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)
{
// currently allow subtyping
opName << "a.";
}
- if (k == UMINUS)
+ if (k == NEG)
{
opName << "u";
}
visited[cur].addMonomial(null, r);
}
}
- else if (k == PLUS || k == MINUS || k == UMINUS || k == MULT
+ else if (k == PLUS || k == SUB || k == NEG || k == MULT
|| k == NONLINEAR_MULT)
{
visited[cur] = PolyNorm();
switch (k)
{
case PLUS:
- case MINUS:
- case UMINUS:
+ case SUB:
+ case NEG:
case MULT:
case NONLINEAR_MULT:
for (size_t i = 0, nchild = cur.getNumChildren(); i < nchild; i++)
{
it = visited.find(cur[i]);
Assert(it != visited.end());
- if ((k == MINUS && i == 1) || k == UMINUS)
+ if ((k == SUB && i == 1) || k == NEG)
{
ret.subtract(it->second);
}
bool isEqual(const PolyNorm& p) const;
/**
* Make polynomial from real term n. This method normalizes applications
- * of operators PLUS, MINUS, UMINUS, MULT, and NONLINEAR_MULT only.
+ * of operators PLUS, 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, t);
}
-RewriteResponse ArithRewriter::rewriteMinus(TNode t)
+RewriteResponse ArithRewriter::rewriteSub(TNode t)
{
- Assert(t.getKind() == kind::MINUS);
+ Assert(t.getKind() == kind::SUB);
Assert(t.getNumChildren() == 2);
auto* nm = NodeManager::currentNM();
nm->mkNode(Kind::PLUS, t[0], makeUnaryMinusNode(t[1])));
}
-RewriteResponse ArithRewriter::rewriteUMinus(TNode t, bool pre){
- Assert(t.getKind() == kind::UMINUS);
+RewriteResponse ArithRewriter::rewriteNeg(TNode t, bool pre)
+{
+ Assert(t.getKind() == kind::NEG);
if (t[0].isConst())
{
}else{
switch(Kind k = t.getKind()){
case kind::REAL_ALGEBRAIC_NUMBER: return rewriteRAN(t);
- case kind::MINUS: return rewriteMinus(t);
- case kind::UMINUS: return rewriteUMinus(t, true);
+ case kind::SUB: return rewriteSub(t);
+ case kind::NEG: return rewriteNeg(t, true);
case kind::DIVISION:
case kind::DIVISION_TOTAL: return rewriteDiv(t, true);
case kind::PLUS: return preRewritePlus(t);
Trace("arith-rewriter") << "postRewriteTerm: " << t << std::endl;
switch(t.getKind()){
case kind::REAL_ALGEBRAIC_NUMBER: return rewriteRAN(t);
- case kind::MINUS: return rewriteMinus(t);
- case kind::UMINUS: return rewriteUMinus(t, false);
+ case kind::SUB: return rewriteSub(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);
}
else if (rat.sgn() == -1)
{
- Node ret = nm->mkNode(kind::UMINUS,
+ Node ret = nm->mkNode(kind::NEG,
nm->mkNode(kind::SINE, nm->mkConstReal(-rat)));
return RewriteResponse(REWRITE_AGAIN_FULL, ret);
}
kind::INTS_DIVISION, mkRationalNode(r_abs + rone), ntwo);
Node new_pi_factor;
if( r.sgn()==1 ){
- new_pi_factor =
- nm->mkNode(kind::MINUS,
- pi_factor,
- nm->mkNode(kind::MULT, ntwo, ra_div_two));
+ new_pi_factor = nm->mkNode(
+ kind::SUB, pi_factor, nm->mkNode(kind::MULT, ntwo, ra_div_two));
}else{
Assert(r.sgn() == -1);
new_pi_factor =
{
return RewriteResponse(
REWRITE_AGAIN_FULL,
- nm->mkNode(kind::UMINUS, nm->mkNode(kind::SINE, rem)));
+ nm->mkNode(kind::NEG, nm->mkNode(kind::SINE, rem)));
}
}
else if (rem.isNull())
REWRITE_AGAIN_FULL,
nm->mkNode(
kind::SINE,
- nm->mkNode(kind::MINUS,
+ nm->mkNode(kind::SUB,
nm->mkNode(kind::MULT,
nm->mkConstReal(Rational(1) / Rational(2)),
mkPi()),
// (mod x (- c)) ---> (mod x c)
Node nn = nm->mkNode(k, t[0], nm->mkConstInt(-t[1].getConst<Rational>()));
Node ret = (k == kind::INTS_DIVISION || k == kind::INTS_DIVISION_TOTAL)
- ? nm->mkNode(kind::UMINUS, nn)
+ ? nm->mkNode(kind::NEG, nn)
: nn;
return returnRewrite(t, ret, Rewrite::DIV_MOD_PULL_NEG_DEN);
}
static RewriteResponse rewriteRAN(TNode t);
static RewriteResponse rewriteVariable(TNode t);
- static RewriteResponse rewriteMinus(TNode t);
- static RewriteResponse rewriteUMinus(TNode t, bool pre);
+ static RewriteResponse rewriteSub(TNode t);
+ static RewriteResponse rewriteNeg(TNode t, bool pre);
static RewriteResponse rewriteDiv(TNode t, bool pre);
static RewriteResponse rewriteAbs(TNode t);
static RewriteResponse rewriteIntsDivMod(TNode t, bool pre);
operator PLUS 2: "arithmetic addition (N-ary)"
operator MULT 2: "arithmetic multiplication (N-ary)"
operator NONLINEAR_MULT 2: "synonym for MULT"
-operator MINUS 2 "arithmetic binary subtraction operator"
-operator UMINUS 1 "arithmetic unary negation"
+operator SUB 2 "arithmetic binary subtraction operator"
+operator NEG 1 "arithmetic unary negation"
operator DIVISION 2 "real division, division by 0 undefined (user symbol)"
operator DIVISION_TOTAL 2 "real division with interpreted division by 0 (internal symbol)"
operator INTS_DIVISION 2 "integer division, division by 0 undefined (user symbol)"
typerule PLUS ::cvc5::theory::arith::ArithOperatorTypeRule
typerule MULT ::cvc5::theory::arith::ArithOperatorTypeRule
typerule NONLINEAR_MULT ::cvc5::theory::arith::ArithOperatorTypeRule
-typerule MINUS ::cvc5::theory::arith::ArithOperatorTypeRule
-typerule UMINUS ::cvc5::theory::arith::ArithOperatorTypeRule
+typerule SUB ::cvc5::theory::arith::ArithOperatorTypeRule
+typerule NEG ::cvc5::theory::arith::ArithOperatorTypeRule
typerule DIVISION ::cvc5::theory::arith::ArithOperatorTypeRule
typerule POW ::cvc5::theory::arith::ArithOperatorTypeRule
{
return a_eq_b;
}
- Node negate_b = NodeManager::currentNM()->mkNode(Kind::UMINUS, b);
+ Node negate_b = NodeManager::currentNM()->mkNode(Kind::NEG, b);
return a_eq_b.orNode(a.eqNode(negate_b));
}
else if (status < 0)
// return nm->mkNode( greater_op, mkAbs( a ), mkAbs( b ) );
Node a_is_nonnegative = nm->mkNode(Kind::GEQ, a, d_data->d_zero);
Node b_is_nonnegative = nm->mkNode(Kind::GEQ, b, d_data->d_zero);
- Node negate_a = nm->mkNode(Kind::UMINUS, a);
- Node negate_b = nm->mkNode(Kind::UMINUS, b);
+ Node negate_a = nm->mkNode(Kind::NEG, a);
+ Node negate_b = nm->mkNode(Kind::NEG, b);
return a_is_nonnegative.iteNode(
b_is_nonnegative.iteNode(nm->mkNode(greater_op, a, b),
nm->mkNode(greater_op, a, negate_b)),
Node b = args[4];
int sgn = args[5].getConst<Rational>().getNumerator().sgn();
Assert(sgn == -1 || sgn == 1);
- Node tplane = nm->mkNode(Kind::MINUS,
+ Node tplane = nm->mkNode(Kind::SUB,
nm->mkNode(Kind::PLUS,
nm->mkNode(Kind::MULT, b, x),
nm->mkNode(Kind::MULT, a, y)),
Node b_v = pts[1][p];
// tangent plane
- Node tplane = nm->mkNode(Kind::MINUS,
+ Node tplane = nm->mkNode(Kind::SUB,
nm->mkNode(Kind::PLUS,
nm->mkNode(Kind::MULT, b_v, a),
nm->mkNode(Kind::MULT, a_v, b)),
Node IAndSolver::mkINot(unsigned k, Node x) const
{
NodeManager* nm = NodeManager::currentNM();
- Node ret = nm->mkNode(MINUS, d_iandUtils.twoToKMinusOne(k), x);
+ Node ret = nm->mkNode(SUB, d_iandUtils.twoToKMinusOne(k), x);
ret = rewrite(ret);
return ret;
}
{
// could be faster
NodeManager* nm = NodeManager::currentNM();
- return nm->mkNode(kind::MINUS, twoToK(k), d_one);
+ return nm->mkNode(kind::SUB, twoToK(k), d_one);
}
} // namespace nl
Trace("nl-ext-cms-debug") << " b = " << b << std::endl;
// find maximal/minimal value on the interval
Node apex = nm->mkNode(
- DIVISION, nm->mkNode(UMINUS, b), nm->mkNode(MULT, d_two, a));
+ DIVISION, nm->mkNode(NEG, b), nm->mkNode(MULT, d_two, a));
apex = rewrite(apex);
Assert(apex.isConst());
// for lower, upper, whether we are greater than the apex
{
// pick c-1
bounds.first = rewrite(
- NodeManager::currentNM()->mkNode(Kind::MINUS, center, d_data->d_one));
+ NodeManager::currentNM()->mkNode(Kind::SUB, center, d_data->d_one));
}
if (bounds.second.isNull())
{
evall,
nm->mkNode(Kind::MULT,
nm->mkNode(Kind::DIVISION,
- nm->mkNode(Kind::MINUS, evall, evalu),
- nm->mkNode(Kind::MINUS, l, u)),
- nm->mkNode(Kind::MINUS, t, l)));
+ nm->mkNode(Kind::SUB, evall, evalu),
+ nm->mkNode(Kind::SUB, l, u)),
+ nm->mkNode(Kind::SUB, t, l)));
}
} // namespace
AND,
nm->mkNode(IMPLIES,
nm->mkNode(GT, args[0], mpi),
- nm->mkNode(GT, s, nm->mkNode(MINUS, mpi, args[0]))),
+ nm->mkNode(GT, s, nm->mkNode(SUB, mpi, args[0]))),
nm->mkNode(IMPLIES,
nm->mkNode(LT, args[0], pi),
- nm->mkNode(LT, s, nm->mkNode(MINUS, pi, args[0]))));
+ nm->mkNode(LT, s, nm->mkNode(SUB, pi, args[0]))));
}
else if (id == PfRule::ARITH_TRANS_SINE_APPROX_ABOVE_NEG)
{
nm->mkNode(Kind::GT, t[0], d_data->d_pi_neg),
nm->mkNode(Kind::GT,
t,
- nm->mkNode(Kind::MINUS, d_data->d_pi_neg, t[0]))),
+ nm->mkNode(Kind::SUB, d_data->d_pi_neg, t[0]))),
nm->mkNode(
Kind::IMPLIES,
nm->mkNode(Kind::LT, t[0], d_data->d_pi),
- nm->mkNode(Kind::LT,
- t,
- nm->mkNode(Kind::MINUS, d_data->d_pi, t[0]))));
+ nm->mkNode(
+ Kind::LT, t, nm->mkNode(Kind::SUB, d_data->d_pi, t[0]))));
CDProof* proof = nullptr;
if (d_data->isProofEnabled())
{
else
{
Assert(k == Kind::SINE);
- Node l = nm->mkNode(Kind::MINUS, taylor_sum, ru);
+ Node l = nm->mkNode(Kind::SUB, taylor_sum, ru);
Node u = nm->mkNode(Kind::PLUS, taylor_sum, ru);
pbounds.d_lower = l;
pbounds.d_upperNeg = u;
{
NodeManager* nm = NodeManager::currentNM();
// Figure 3: S_l( x ), S_u( x ) for s = 0,1
- Node rcoeff_n = rewrite(nm->mkNode(Kind::MINUS, lower, upper));
+ Node rcoeff_n = rewrite(nm->mkNode(Kind::SUB, lower, upper));
Assert(rcoeff_n.isConst());
Rational rcoeff = rcoeff_n.getConst<Rational>();
Assert(rcoeff.sgn() != 0);
lval,
nm->mkNode(Kind::MULT,
nm->mkNode(Kind::DIVISION,
- nm->mkNode(Kind::MINUS, lval, uval),
- nm->mkNode(Kind::MINUS, lower, upper)),
- nm->mkNode(Kind::MINUS, arg, lower)));
+ nm->mkNode(Kind::SUB, lval, uval),
+ nm->mkNode(Kind::SUB, lower, upper)),
+ nm->mkNode(Kind::SUB, arg, lower)));
Trace("nl-trans") << "Creating secant plane for transcendental function of "
<< arg << std::endl;
Trace("nl-trans") << "\tfrom ( " << lower << " ; " << lval << " ) to ( "
bvm->mkBoundVar<ToIntWitnessVarAttribute>(node[0], nm->integerType());
Node one = nm->mkConstReal(Rational(1));
Node zero = nm->mkConstReal(Rational(0));
- Node diff = nm->mkNode(MINUS, node[0], v);
+ Node diff = nm->mkNode(SUB, node[0], v);
Node lem = mkInRange(diff, zero, one);
Node toIntSkolem =
mkWitnessTerm(v,
v, lem, "linearIntDiv", "the result of an intdiv-by-k term", lems);
if (k == INTS_MODULUS_TOTAL)
{
- Node nn = nm->mkNode(MINUS, num, nm->mkNode(MULT, den, intVar));
+ Node nn = nm->mkNode(SUB, num, nm->mkNode(MULT, den, intVar));
return nn;
}
else
nm->mkNode(LT,
node[0],
nm->mkConstRealOrInt(node[0].getType(), Rational(0))),
- nm->mkNode(UMINUS, node[0]),
+ nm->mkNode(NEG, node[0]),
node[0]);
break;
}
{
return d_internal->getEqualityStatus(a,b);
}
- Node diff = d_env.getNodeManager()->mkNode(Kind::MINUS, a, b);
+ Node diff = d_env.getNodeManager()->mkNode(Kind::SUB, a, b);
std::optional<bool> isZero = isExpressionZero(d_env, diff, d_arithModelCache);
if (isZero)
{
}
return value;
}
- case kind::MINUS: { // 2 args
+ case kind::SUB:
+ { // 2 args
return getDeltaValue(term[0]) - getDeltaValue(term[1]);
}
- case kind::UMINUS: { // 1 arg
+ case kind::NEG:
+ { // 1 arg
return (-getDeltaValue(term[0]));
}
success = decomposeTerm(rewrite(right), rm, rp, rc);
if(!success){ return false; }
- Node diff =
- rewrite(NodeManager::currentNM()->mkNode(kind::MINUS, left, right));
+ Node diff = rewrite(NodeManager::currentNM()->mkNode(kind::SUB, left, right));
Rational dc;
success = decomposeTerm(diff, dm, dp, dc);
Assert(success);
Node i =
bvm->mkBoundVar<FirstIndexVarAttribute>(node, "i", nm->integerType());
Node iList = nm->mkNode(BOUND_VAR_LIST, i);
- Node iMinusOne = nm->mkNode(MINUS, i, one);
+ Node iMinusOne = nm->mkNode(SUB, i, one);
Node uf_i = nm->mkNode(APPLY_UF, uf, i);
Node combine_0 = nm->mkNode(APPLY_UF, combine, zero);
Node combine_iMinusOne = nm->mkNode(APPLY_UF, combine, iMinusOne);
bvm->mkBoundVar<SecondIndexVarAttribute>(node, "j", nm->integerType());
Node iList = nm->mkNode(BOUND_VAR_LIST, i);
Node jList = nm->mkNode(BOUND_VAR_LIST, j);
- Node iMinusOne = nm->mkNode(MINUS, i, one);
+ Node iMinusOne = nm->mkNode(SUB, i, one);
Node uf_i = nm->mkNode(APPLY_UF, uf, i);
Node uf_j = nm->mkNode(APPLY_UF, uf, j);
Node cardinality_0 = nm->mkNode(APPLY_UF, cardinality, zero);
Node skolem = getSkolem(n, inferInfo);
Node count = getMultiplicityTerm(e, skolem);
- Node subtract = d_nm->mkNode(MINUS, countA, countB);
+ Node subtract = d_nm->mkNode(SUB, countA, countB);
Node gte = d_nm->mkNode(GEQ, countA, countB);
Node difference = d_nm->mkNode(ITE, gte, subtract, d_zero);
Node equal = count.eqNode(difference);
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 iMinusOne = d_nm->mkNode(MINUS, 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 f_uf_i = d_nm->mkNode(APPLY_UF, f, uf_i);
returnNode = d_nm->mkNode(
kind::ITE,
d_nm->mkNode(kind::EQUAL, translated_children[1], d_zero),
- d_nm->mkNode(kind::MINUS, pow2BvSize, d_one),
+ d_nm->mkNode(kind::SUB, pow2BvSize, d_one),
divNode);
break;
}
Node modNode = d_nm->mkNode(kind::INTS_MODULUS_TOTAL, x, powNode);
Node two = d_nm->mkConstInt(Rational(2));
Node twoTimesNode = d_nm->mkNode(kind::MULT, two, modNode);
- return d_nm->mkNode(kind::MINUS, twoTimesNode, x);
+ return d_nm->mkNode(kind::SUB, twoTimesNode, x);
}
Node IntBlaster::createSignExtendNode(Node x, uint64_t bvsize, uint64_t amount)
Node IntBlaster::createBVSubNode(Node x, Node y, uint64_t bvsize)
{
- Node minus = d_nm->mkNode(kind::MINUS, x, y);
+ Node minus = d_nm->mkNode(kind::SUB, x, y);
Node p2 = pow2(bvsize);
return d_nm->mkNode(kind::INTS_MODULUS_TOTAL, minus, p2);
}
// Based on Hacker's Delight section 2-2 equation a:
// -x = ~x+1
Node p2 = pow2(bvsize);
- return d_nm->mkNode(kind::MINUS, p2, n);
+ return d_nm->mkNode(kind::SUB, p2, n);
}
Node IntBlaster::createBVNotNode(Node n, uint64_t bvsize)
{
- return d_nm->mkNode(kind::MINUS, maxInt(bvsize), n);
+ return d_nm->mkNode(kind::SUB, maxInt(bvsize), n);
}
} // namespace cvc5
if (doSymBreak)
{
// direct solving for children
- // for instance, we may want to insist that the LHS of MINUS is 0
+ // for instance, we may want to insist that the LHS of SUB is 0
Trace("sygus-sb-simple-debug") << " Solve children..." << std::endl;
std::map<unsigned, unsigned> children_solved;
for (unsigned j = 0; j < dt_index_nargs; j++)
{
// other cases of rewriting x k x -> x'
Node req_const;
- if (nk == GT || nk == LT || nk == XOR || nk == MINUS
+ if (nk == GT || nk == LT || nk == XOR || nk == SUB
|| nk == BITVECTOR_SUB || nk == BITVECTOR_XOR
|| nk == BITVECTOR_UREM)
{
Assert(rt.empty());
// construct rt by cases
- if (pk == NOT || pk == BITVECTOR_NOT || pk == UMINUS || pk == BITVECTOR_NEG)
+ if (pk == NOT || pk == BITVECTOR_NOT || pk == NEG || pk == BITVECTOR_NEG)
{
// negation normal form
if (pk == k)
rt.d_req_kind = BITVECTOR_XNOR;
}
}
- else if (pk == UMINUS)
+ else if (pk == NEG)
{
if (k == PLUS)
{
rt.d_req_kind = PLUS;
- reqk = UMINUS;
+ reqk = NEG;
}
}
else if (pk == BITVECTOR_NEG)
}
}
}
- else if (k == MINUS || k == BITVECTOR_SUB)
+ else if (k == SUB || k == BITVECTOR_SUB)
{
- if (pk == EQUAL || pk == MINUS || pk == BITVECTOR_SUB || pk == LEQ
- || pk == LT || pk == GEQ || pk == GT)
+ if (pk == EQUAL || pk == SUB || pk == BITVECTOR_SUB || pk == LEQ || pk == LT
+ || pk == GEQ || pk == GT)
{
int oarg = arg == 0 ? 1 : 0;
// (~ x (- y z)) ----> (~ (+ x z) y)
// (~ (- 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 == MINUS ? PLUS : BITVECTOR_ADD;
+ rt.d_children[oarg].d_req_kind = k == SUB ? PLUS : 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);
}
{
// (+ x (- y z)) -----> (- (+ x y) z)
// (+ (- y z) x) -----> (- (+ x y) z)
- rt.d_req_kind = pk == PLUS ? MINUS : BITVECTOR_SUB;
+ rt.d_req_kind = pk == PLUS ? 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);
break;
}
- case kind::MINUS:
+ case kind::SUB:
{
const Rational& x = results[currNode[0]].d_rat;
const Rational& y = results[currNode[1]].d_rat;
break;
}
- case kind::UMINUS:
+ case kind::NEG:
{
const Rational& x = results[currNode[0]].d_rat;
results[currNode] = EvalResult(-x);
else
{
Node delta = d_vtc->getVtsDelta();
- uval = nm->mkNode(
- uires == CEG_TT_UPPER_STRICT ? PLUS : MINUS, uval, delta);
+ uval =
+ nm->mkNode(uires == CEG_TT_UPPER_STRICT ? PLUS : SUB, uval, delta);
uval = rewrite(uval);
}
}
// could get rho value for infinity here
if (rr == 0)
{
- val = nm->mkNode(UMINUS, val);
+ val = nm->mkNode(NEG, val);
val = rewrite(val);
}
TermProperties pv_prop_no_bound;
}
else if (!vals[1].isNull())
{
- val = nm->mkNode(MINUS, vals[1], d_one);
+ val = nm->mkNode(SUB, vals[1], d_one);
val = rewrite(val);
}
}
(msum[pv].isNull() || msum[pv].getConst<Rational>().sgn() == 1) ? 1
: -1;
val = rewrite(
- nm->mkNode(ires_use == -1 ? PLUS : MINUS,
- nm->mkNode(ires_use == -1 ? MINUS : PLUS, val, realPart),
+ nm->mkNode(ires_use == -1 ? PLUS : SUB,
+ nm->mkNode(ires_use == -1 ? SUB : PLUS, val, realPart),
nm->mkNode(TO_INTEGER, realPart)));
// could round up for upper bounds here
Trace("cegqi-arith-debug") << "result : " << val << std::endl;
Node rho;
if (isLower)
{
- rho = nm->mkNode(MINUS, ceValue, mt);
+ rho = nm->mkNode(SUB, ceValue, mt);
}
else
{
- rho = nm->mkNode(MINUS, mt, ceValue);
+ rho = nm->mkNode(SUB, mt, ceValue);
}
rho = rewrite(rho);
Trace("cegqi-arith-bound2")
rho = nm->mkNode(INTS_MODULUS_TOTAL, rho, new_theta);
rho = rewrite(rho);
Trace("cegqi-arith-bound2") << rho << std::endl;
- Kind rk = isLower ? PLUS : MINUS;
+ Kind rk = isLower ? PLUS : SUB;
val = nm->mkNode(rk, val, rho);
val = rewrite(val);
Trace("cegqi-arith-bound2") << "(after rho) : " << val << std::endl;
atom_lhs = atom[0];
atom_rhs = atom[1];
}else{
- atom_lhs = nm->mkNode(MINUS, atom[0], atom[1]);
+ atom_lhs = nm->mkNode(SUB, atom[0], atom[1]);
atom_lhs = rewrite(atom_lhs);
atom_rhs = nm->mkConstRealOrInt(atom_lhs.getType(), Rational(0));
}
{
if (pat.getKind() == GT)
{
- t_match = nm->mkNode(
- MINUS, t, nm->mkConstRealOrInt(t.getType(), Rational(1)));
+ t_match =
+ nm->mkNode(SUB, t, nm->mkConstRealOrInt(t.getType(), Rational(1)));
}else{
t_match = t;
}
{
if (nk == PLUS)
{
- x = nm->mkNode(MINUS, x, nc);
+ x = nm->mkNode(SUB, x, nc);
}
else if (nk == MULT)
{
}
if (nc.getConst<Rational>().sgn() < 0)
{
- x = nm->mkNode(UMINUS, x);
+ x = nm->mkNode(NEG, x);
}
}
else
!= bound_int_range_term[b].end());
d_bounds[b][f][v] = bound_int_range_term[b][v];
}
- Node r = nm->mkNode(MINUS, d_bounds[1][f][v], d_bounds[0][f][v]);
+ Node r = nm->mkNode(SUB, d_bounds[1][f][v], d_bounds[0][f][v]);
d_range[f][v] = rewrite(r);
Trace("bound-int") << "Variable " << v << " is bound because of int range literals " << bound_lit_map[0][v] << " and " << bound_lit_map[1][v] << std::endl;
}
}else{
NodeManager* nm = NodeManager::currentNM();
Trace("bound-int-rsi") << "Can limit bounds of " << v << " to " << l << "..." << u << std::endl;
- Node range = rewrite(nm->mkNode(MINUS, u, l));
+ Node range = rewrite(nm->mkNode(SUB, u, l));
// 9999 is an arbitrary range past which we do not do exhaustive
// bounded instantation, based on the check below.
Node ra =
{
Kind kn = k;
if( d_vars[index].getKind()==PLUS ){
- kn = MINUS;
+ kn = SUB;
}
if( kn!=k ){
sum = NodeManager::currentNM()->mkNode( kn, v, lhs );
STRING_SUBSTR,
slv,
tpreL,
- nm->mkNode(MINUS, slvL, nm->mkNode(PLUS, tpreL, tpostL)));
+ nm->mkNode(SUB, slvL, nm->mkNode(PLUS, tpreL, tpostL)));
// forall x. r ++ x ++ t = s => P( x )
// is equivalent to
// r ++ s' ++ t = s => P( s' ) where
Node icond = nm->mkNode(GEQ, k, nm->mkConstInt(Rational(0)));
Node iret =
ret.substitute(ind_vars[0],
- nm->mkNode(MINUS, k, nm->mkConstInt(Rational(1))))
+ nm->mkNode(SUB, k, nm->mkConstInt(Rational(1))))
.negate();
n_str_ind = nm->mkNode(OR, icond.negate(), iret);
n_str_ind = nm->mkNode(AND, icond, n_str_ind);
if (types[i].isRealOrInt())
{
- // Add PLUS, MINUS
- Kind kinds[2] = {PLUS, MINUS};
+ // Add PLUS, SUB
+ Kind kinds[2] = {PLUS, SUB};
for (const Kind kind : kinds)
{
Trace("sygus-grammar-def") << "...add for " << kind << std::endl;
if (Random::getRandom().pickWithProb(0.5))
{
// negative
- ret = nm->mkNode(kind::UMINUS, ret);
+ ret = nm->mkNode(kind::NEG, ret);
}
ret = d_env.getRewriter()->rewrite(ret);
Assert(ret.isConst());
bool TermUtil::isNegate(Kind k)
{
- return k == NOT || k == BITVECTOR_NOT || k == BITVECTOR_NEG || k == UMINUS;
+ return k == NOT || k == BITVECTOR_NOT || k == BITVECTOR_NEG || k == NEG;
}
bool TermUtil::isAssoc(Kind k, bool reqNAry)
{
return true;
}
- else if (ik == MINUS || ik == BITVECTOR_SHL || ik == BITVECTOR_LSHR
+ else if (ik == SUB || ik == BITVECTOR_SHL || ik == BITVECTOR_LSHR
|| ik == BITVECTOR_ASHR || ik == BITVECTOR_SUB
|| ik == BITVECTOR_UREM)
{
else if (node[0].getKind() == kind::SET_UNION)
{
Node ret = NodeManager::currentNM()->mkNode(
- kind::MINUS,
+ kind::SUB,
NodeManager::currentNM()->mkNode(
kind::PLUS,
NodeManager::currentNM()->mkNode(kind::SET_CARD, node[0][0]),
else if (node[0].getKind() == kind::SET_MINUS)
{
Node ret = NodeManager::currentNM()->mkNode(
- kind::MINUS,
+ kind::SUB,
NodeManager::currentNM()->mkNode(kind::SET_CARD, node[0][0]),
NodeManager::currentNM()->mkNode(
kind::SET_CARD,
{
return !strict;
}
- Node diff = NodeManager::currentNM()->mkNode(kind::MINUS, a, b);
+ Node diff = NodeManager::currentNM()->mkNode(kind::SUB, a, b);
return check(diff, strict);
}
return a.getConst<Rational>().sgn() >= (strict ? 1 : 0);
}
- Node ar =
- strict ? NodeManager::currentNM()->mkNode(
- kind::MINUS, a, NodeManager::currentNM()->mkConstInt(Rational(1)))
- : a;
+ Node ar = strict ? NodeManager::currentNM()->mkNode(
+ kind::SUB, a, NodeManager::currentNM()->mkConstInt(Rational(1)))
+ : a;
ar = d_rr->rewrite(ar);
if (ar.getAttribute(StrCheckEntailArithComputedAttr()))
{
// n <= len( x ) implies
// len( x ) - n >= len( substr( x, n, m ) )
- approx.push_back(nm->mkNode(MINUS, lenx, a[0][1]));
+ approx.push_back(nm->mkNode(SUB, lenx, a[0][1]));
}
else
{
// len(x)-n <= len( substr( x, n, m ) )
if (check(a[0][1]) && check(npm, lenx))
{
- approx.push_back(nm->mkNode(MINUS, lenx, a[0][1]));
+ approx.push_back(nm->mkNode(SUB, lenx, a[0][1]));
}
}
}
else
{
// len( x ) - len( y ) <= len( replace( x, y, z ) )
- approx.push_back(nm->mkNode(MINUS, lenx, leny));
+ approx.push_back(nm->mkNode(SUB, lenx, leny));
}
}
}
{
// len( x ) >= len( y ) implies
// len( x ) - len( y ) >= indexof( x, y, n )
- approx.push_back(nm->mkNode(MINUS, lenx, leny));
+ approx.push_back(nm->mkNode(SUB, lenx, leny));
}
else
{
toVisit.pop_back();
if (curr.getKind() == kind::PLUS || curr.getKind() == kind::MULT
- || curr.getKind() == kind::MINUS || curr.getKind() == kind::EQUAL)
+ || curr.getKind() == kind::SUB || curr.getKind() == kind::EQUAL)
{
for (const auto& currChild : curr)
{
// (not (>= s t)) --> (>= (t - 1) s)
Assert(assumption.getKind() == kind::NOT
&& assumption[0].getKind() == kind::GEQ);
- x = nm->mkNode(
- kind::MINUS, assumption[0][1], nm->mkConstInt(Rational(1)));
+ x = nm->mkNode(kind::SUB, assumption[0][1], nm->mkConstInt(Rational(1)));
y = assumption[0][0];
}
nm->mkNode(kind::EQUAL, x, nm->mkNode(kind::PLUS, y, slen)));
}
- Node diff = nm->mkNode(kind::MINUS, a, b);
+ Node diff = nm->mkNode(kind::SUB, a, b);
bool res = false;
if (assumption.isConst())
{
Node i = n[1];
Node sLen = nm->mkNode(STRING_LENGTH, s);
Node iRev = nm->mkNode(
- MINUS, sLen, nm->mkNode(PLUS, i, nm->mkConstInt(Rational(1))));
+ SUB, sLen, nm->mkNode(PLUS, i, nm->mkConstInt(Rational(1))));
std::vector<Node> nexp;
nexp.push_back(nm->mkNode(LEQ, nm->mkConstInt(Rational(0)), i));
if (!lacc.empty())
{
currSum = lacc.size() == 1 ? lacc[0] : nm->mkNode(PLUS, lacc);
- currIndex = nm->mkNode(MINUS, currIndex, currSum);
+ currIndex = nm->mkNode(SUB, currIndex, currSum);
}
Node cc;
if (k == STRING_UPDATE && checkInv)
{
Assert(l.getType().isInteger());
NodeManager* nm = NodeManager::currentNM();
- Node n = isRev ? nm->mkNode(MINUS, nm->mkNode(STRING_LENGTH, x), l) : l;
+ Node n = isRev ? nm->mkNode(SUB, nm->mkNode(STRING_LENGTH, x), l) : l;
Node sk1 = skc->mkSkolemCached(x, n, SkolemCache::SK_PREFIX, "dc_spt1");
newSkolems.push_back(sk1);
Node sk2 = skc->mkSkolemCached(x, n, SkolemCache::SK_SUFFIX_REM, "dc_spt2");
Node ppSum = childLengthsPostPivot.size() == 1
? childLengthsPostPivot[0]
: nm->mkNode(PLUS, childLengthsPostPivot);
- currEnd = nm->mkNode(MINUS, lenx, ppSum);
+ currEnd = nm->mkNode(SUB, lenx, ppSum);
}
else
{
// ... ^ "B" = substr( x, len( x ) - 3, 1 ) ^ ...
Node sc = sep_children.back();
Node lenSc = nm->mkNode(STRING_LENGTH, sc);
- Node loc = nm->mkNode(MINUS, lenx, nm->mkNode(PLUS, lenSc, cEnd));
+ Node loc = nm->mkNode(SUB, lenx, nm->mkNode(PLUS, 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:
Assert(children[index + (r == 0 ? 1 : -1)].getKind() != STRING_TO_REGEXP);
Node s = c[0];
Node lens = nm->mkNode(STRING_LENGTH, s);
- Node sss = r == 0 ? zero : nm->mkNode(MINUS, lenx, lens);
+ Node sss = r == 0 ? zero : nm->mkNode(SUB, lenx, lens);
Node ss = nm->mkNode(STRING_SUBSTR, x, sss, lens);
sConstraints.push_back(ss.eqNode(s));
if (r == 0)
Node bound = nm->mkNode(GEQ, sss, sStartIndex);
sConstraints.push_back(bound);
}
- sLength = nm->mkNode(MINUS, sLength, lens);
+ sLength = nm->mkNode(SUB, sLength, lens);
}
if (r == 1 && !sConstraints.empty())
{
}
else if (i + 1 == nchildren)
{
- k = nm->mkNode(MINUS, lenx, lens);
+ k = nm->mkNode(SUB, lenx, lens);
}
else
{
Node bound =
nm->mkNode(AND,
nm->mkNode(LEQ, zero, k),
- nm->mkNode(LEQ, k, nm->mkNode(MINUS, lenx, lens)));
+ nm->mkNode(LEQ, k, nm->mkNode(SUB, lenx, lens)));
echildren.push_back(bound);
}
Node substrEq = nm->mkNode(STRING_SUBSTR, x, k, lens).eqNode(s);
Node ks = nm->mkNode(PLUS, k, lens);
Node substrSuffix = nm->mkNode(
STRING_IN_REGEXP,
- nm->mkNode(STRING_SUBSTR, x, ks, nm->mkNode(MINUS, lenx, ks)),
+ nm->mkNode(STRING_SUBSTR, x, ks, nm->mkNode(SUB, lenx, ks)),
rps);
echildren.push_back(substrSuffix);
}
nm->mkNode(AND, nm->mkNode(GT, b1, zero), nm->mkNode(GEQ, lens, b1));
// internal
Node s1 = nm->mkNode(STRING_SUBSTR, s, zero, b1);
- Node s2 = nm->mkNode(STRING_SUBSTR, s, b1, nm->mkNode(MINUS, lens, b1));
+ Node s2 = nm->mkNode(STRING_SUBSTR, s, b1, nm->mkNode(SUB, lens, b1));
Node s1r1 = nm->mkNode(STRING_IN_REGEXP, s1, r[0]).negate();
Node s2r2 = nm->mkNode(STRING_IN_REGEXP, s2, r).negate();
if (index == 0)
{
s1 = nm->mkNode(STRING_SUBSTR, s, zero, b1);
- s2 = nm->mkNode(STRING_SUBSTR, s, b1, nm->mkNode(MINUS, lens, b1));
+ s2 = nm->mkNode(STRING_SUBSTR, s, b1, nm->mkNode(SUB, lens, b1));
}
else
{
- s1 = nm->mkNode(STRING_SUBSTR, s, nm->mkNode(MINUS, lens, b1), b1);
- s2 = nm->mkNode(STRING_SUBSTR, s, zero, nm->mkNode(MINUS, lens, b1));
+ s1 = nm->mkNode(STRING_SUBSTR, s, nm->mkNode(SUB, lens, b1), b1);
+ s2 = nm->mkNode(STRING_SUBSTR, s, zero, nm->mkNode(SUB, lens, b1));
}
Node s1r1 = nm->mkNode(STRING_IN_REGEXP, s1, r[index]).negate();
std::vector<Node> nvec;
else
{
// strip up to ( str.len(node[0]) - end_pt ) off the end of the string
- curr =
- d_arithEntail.rewrite(nm->mkNode(kind::MINUS, tot_len, end_pt));
+ curr = d_arithEntail.rewrite(nm->mkNode(kind::SUB, tot_len, end_pt));
}
}
}
// the length of a string from the inner substr subtracts the start point
// of the outer substr
- Node len_from_inner = d_arithEntail.rewrite(
- nm->mkNode(kind::MINUS, node[0][2], start_outer));
+ Node len_from_inner =
+ d_arithEntail.rewrite(nm->mkNode(kind::SUB, node[0][2], start_outer));
Node len_from_outer = node[2];
Node new_len;
// take quantity that is for sure smaller than the other
{
// str.update(str.rev(s), n, t) --->
// str.rev(str.update(s, len(s) - (n + 1), t))
- Node idx = nm->mkNode(MINUS,
+ Node idx = nm->mkNode(SUB,
nm->mkNode(STRING_LENGTH, s),
nm->mkNode(PLUS, i, nm->mkConstInt(Rational(1))));
Node ret = nm->mkNode(STRING_REV, nm->mkNode(STRING_UPDATE, s[0], idx, x));
Node len0 = nm->mkNode(STRING_LENGTH, node[0]);
Node len1 = nm->mkNode(STRING_LENGTH, node[1]);
- Node len0m2 = nm->mkNode(MINUS, len0, node[2]);
+ Node len0m2 = nm->mkNode(SUB, len0, node[2]);
if (node[1].isConst())
{
Node nn = utils::mkConcat(children0, stype);
Node ret =
nm->mkNode(PLUS,
- nm->mkNode(MINUS, node[2], new_len),
+ 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);
}
kind::STRING_SUBSTR,
lastChild1[0],
lastChild1[1],
- nm->mkNode(
- kind::PLUS, len0, one, nm->mkNode(kind::UMINUS, partLen1))));
+ nm->mkNode(kind::PLUS, len0, one, nm->mkNode(kind::NEG, partLen1))));
Node res = nm->mkNode(kind::STRING_REPLACE,
node[0],
utils::mkConcat(children1, stype),
}
else
{
- val = NodeManager::currentNM()->mkNode(kind::MINUS, lent, lens);
+ val = NodeManager::currentNM()->mkNode(kind::SUB, lent, lens);
}
// Check if we can turn the prefix/suffix into equalities by showing that the
// SK_ID_*_SPT_REV(x, y) ---> SK_PREFIX(x, (- (str.len x) (str.len y)))
id = SK_PREFIX;
b = nm->mkNode(
- MINUS, nm->mkNode(STRING_LENGTH, a), nm->mkNode(STRING_LENGTH, b));
+ SUB, nm->mkNode(STRING_LENGTH, a), nm->mkNode(STRING_LENGTH, b));
}
else if (id == SK_ID_VC_SPT)
{
// SK_ID_VC_SPT_REV(x, y) ---> SK_PREFIX(x, (- (str.len x) 1))
id = SK_PREFIX;
b = nm->mkNode(
- MINUS, nm->mkNode(STRING_LENGTH, a), nm->mkConstInt(Rational(1)));
+ SUB, nm->mkNode(STRING_LENGTH, a), nm->mkConstInt(Rational(1)));
}
else if (id == SK_ID_DC_SPT)
{
bool isRev = (id == SK_ID_V_UNIFIED_SPT_REV);
Node la = nm->mkNode(STRING_LENGTH, a);
Node lb = nm->mkNode(STRING_LENGTH, b);
- Node ta = isRev ? utils::mkPrefix(a, nm->mkNode(MINUS, la, lb))
+ Node ta = isRev ? utils::mkPrefix(a, nm->mkNode(SUB, la, lb))
: utils::mkSuffix(a, lb);
- Node tb = isRev ? utils::mkPrefix(b, nm->mkNode(MINUS, lb, la))
+ Node tb = isRev ? utils::mkPrefix(b, nm->mkNode(SUB, lb, la))
: utils::mkSuffix(b, la);
id = SK_PURIFY;
// SK_ID_V_UNIFIED_SPT(x,y) --->
Node s = n1[sindex_use];
size_t slen = Word::getLength(s);
Node ncl = nm->mkConstInt(cvc5::Rational(slen));
- Node next_s = nm->mkNode(MINUS, lowerBound, ncl);
+ Node next_s = nm->mkNode(SUB, lowerBound, ncl);
next_s = d_rr->rewrite(next_s);
Assert(next_s.isConst());
// we can remove the entire constant
if (next_s.getConst<Rational>().sgn() >= 0)
{
- curr = d_rr->rewrite(nm->mkNode(MINUS, curr, ncl));
+ curr = d_rr->rewrite(nm->mkNode(SUB, curr, ncl));
success = true;
sindex++;
}
// lower bound minus the length of a concrete string is negative,
// hence lowerBound cannot be larger than long max
Assert(lbr < Rational(String::maxSize()));
- curr = d_rr->rewrite(nm->mkNode(MINUS, curr, lowerBound));
+ curr = d_rr->rewrite(nm->mkNode(SUB, curr, lowerBound));
uint32_t lbsize = lbr.getNumerator().toUnsignedInt();
Assert(lbsize < slen);
if (dir == 1)
else
{
Node next_s = NodeManager::currentNM()->mkNode(
- MINUS,
+ SUB,
curr,
NodeManager::currentNM()->mkNode(STRING_LENGTH, n1[sindex_use]));
next_s = d_rr->rewrite(next_s);
// len(s) - n -m
Node b13 = nm->mkNode(
OR,
- nm->mkNode(EQUAL, lsk2, nm->mkNode(MINUS, lt0, nm->mkNode(PLUS, n, m))),
+ nm->mkNode(EQUAL, lsk2, nm->mkNode(SUB, lt0, nm->mkNode(PLUS, 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);
}
else
{
- rs = nm->mkNode(STRING_SUBSTR, r, zero, nm->mkNode(MINUS, lens, n));
+ 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 negone = nm->mkConstInt(Rational(-1));
// substr( x, n, len( x ) - n )
- Node st = nm->mkNode(STRING_SUBSTR,
- x,
- n,
- nm->mkNode(MINUS, nm->mkNode(STRING_LENGTH, x), n));
+ Node st = nm->mkNode(
+ STRING_SUBSTR, x, n, nm->mkNode(SUB, nm->mkNode(STRING_LENGTH, x), n));
Node io2 =
sc->mkSkolemCached(st, y, SkolemCache::SK_FIRST_CTN_PRE, "iopre");
Node io4 =
Node c31 = st.eqNode(nm->mkNode(STRING_CONCAT, io2, y, io4));
// ~contains( str.++( io2, substr( y, 0, len( y ) - 1) ), y )
Node c32 =
- nm->mkNode(
- STRING_CONTAINS,
- nm->mkNode(
- STRING_CONCAT,
- io2,
- nm->mkNode(
- STRING_SUBSTR,
- y,
- zero,
- nm->mkNode(MINUS, nm->mkNode(STRING_LENGTH, y), one))),
- y)
+ nm->mkNode(STRING_CONTAINS,
+ nm->mkNode(
+ STRING_CONCAT,
+ io2,
+ nm->mkNode(
+ STRING_SUBSTR,
+ y,
+ zero,
+ nm->mkNode(SUB, nm->mkNode(STRING_LENGTH, y), one))),
+ y)
.negate();
// skk = n + len( io2 )
Node c33 = skk.eqNode(nm->mkNode(PLUS, n, nm->mkNode(STRING_LENGTH, io2)));
nm->mkNode(GEQ, i, n),
nm->mkNode(LT, i, nm->mkNode(ITE, retNegOne, sLen, skk)),
nm->mkNode(GT, l, zero),
- nm->mkNode(LEQ, l, nm->mkNode(MINUS, sLen, i)),
+ nm->mkNode(LEQ, l, nm->mkNode(SUB, sLen, i)),
});
Node body = nm->mkNode(
OR,
// ~in_re(substr(s, i, l), r)
Node firstMatch = utils::mkForallInternal(bvl, body);
Node bvll = nm->mkNode(BOUND_VAR_LIST, l);
- Node validLen =
- nm->mkNode(AND,
- nm->mkNode(GEQ, l, zero),
- nm->mkNode(LEQ, l, nm->mkNode(MINUS, sLen, skk)));
+ Node validLen = nm->mkNode(AND,
+ nm->mkNode(GEQ, l, zero),
+ nm->mkNode(LEQ, l, nm->mkNode(SUB, sLen, skk)));
Node matchBody = nm->mkNode(
AND,
validLen,
Node ux = nm->mkNode(APPLY_UF, u, x);
Node ux1 = nm->mkNode(APPLY_UF, u, xPlusOne);
Node c0 = nm->mkNode(STRING_TO_CODE, nm->mkConst(String("0")));
- Node c = nm->mkNode(MINUS, nm->mkNode(STRING_TO_CODE, sx), c0);
+ 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 kc2 = nm->mkNode(LT, k, lens);
Node c0 = nm->mkNode(STRING_TO_CODE, nm->mkConst(String("0")));
Node codeSk = nm->mkNode(
- MINUS,
+ SUB,
nm->mkNode(STRING_TO_CODE, nm->mkNode(STRING_SUBSTR, s, k, one)),
c0);
Node ten = nm->mkConstInt(Rational(10));
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 c = nm->mkNode(MINUS, nm->mkNode(STRING_TO_CODE, sx), c0);
+ 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 cb = nm->mkNode(AND, nm->mkNode(GEQ, c, zero), nm->mkNode(LT, c, ten));
// length of first skolem is second argument
Node b12 = nm->mkNode(STRING_LENGTH, sk1).eqNode(n);
Node lsk2 = nm->mkNode(STRING_LENGTH, sk2);
- Node b13 = nm->mkNode(EQUAL, lsk2, nm->mkNode(MINUS, lt0, t12));
+ Node b13 = nm->mkNode(EQUAL, lsk2, nm->mkNode(SUB, lt0, t12));
Node b1 = nm->mkNode(AND, b11, b12, b13);
// nodes for the case where `seq.nth` is undefined.
nm->mkNode(kind::STRING_SUBSTR,
y,
zero,
- nm->mkNode(kind::MINUS,
+ nm->mkNode(kind::SUB,
nm->mkNode(kind::STRING_LENGTH, y),
one))),
y)
Node ufi = nm->mkNode(APPLY_UF, uf, i);
Node ufip1 = nm->mkNode(APPLY_UF, uf, nm->mkNode(PLUS, 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(MINUS, ii, ufi)),
- z,
- nm->mkNode(APPLY_UF, us, nm->mkNode(PLUS, i, one)));
+ 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)));
std::vector<Node> flem;
flem.push_back(ii.eqNode(negOne).negate());
Node ufip1 = nm->mkNode(APPLY_UF, uf, ip1);
Node ulip1 = nm->mkNode(APPLY_UF, ul, ip1);
// ii = Uf(i + 1) - Ul(i + 1)
- Node ii = nm->mkNode(MINUS, ufip1, ulip1);
+ Node ii = nm->mkNode(SUB, ufip1, ulip1);
std::vector<Node> flem;
// Ul(i + 1) > 0
// forall l. 0 < l < Ul(i + 1) =>
// ~in_re(substr(x, Uf(i + 1) - Ul(i + 1), l), y')
flem.push_back(utils::mkForallInternal(bvll, shortestMatchBody));
- Node pfxMatch =
- nm->mkNode(STRING_SUBSTR, x, ufi, nm->mkNode(MINUS, ii, ufi));
+ Node pfxMatch = nm->mkNode(STRING_SUBSTR, x, ufi, nm->mkNode(SUB, ii, ufi));
// Us(i) = substr(x, Uf(i), ii - Uf(i)) ++ z ++ Us(i + 1)
flem.push_back(
nm->mkNode(APPLY_UF, us, i)
Node i = SkolemCache::mkIndexVar(t);
Node bvi = nm->mkNode(BOUND_VAR_LIST, i);
- Node revi = nm->mkNode(
- MINUS, nm->mkNode(STRING_LENGTH, x), nm->mkNode(PLUS, i, one));
+ Node revi =
+ nm->mkNode(SUB, nm->mkNode(STRING_LENGTH, x), nm->mkNode(PLUS, i, one));
Node ssr = nm->mkNode(STRING_SUBSTR, r, i, one);
Node ssx = nm->mkNode(STRING_SUBSTR, x, revi, one);
NodeManager::currentNM()->mkNode(
kind::LEQ,
b1,
- NodeManager::currentNM()->mkNode(kind::MINUS, lenx, lens)),
+ NodeManager::currentNM()->mkNode(kind::SUB, lenx, lens)),
NodeManager::currentNM()->mkNode(
kind::EQUAL,
NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR, x, b1, lens),
{
NodeManager* nm = NodeManager::currentNM();
return nm->mkNode(
- STRING_SUBSTR, t, n, nm->mkNode(MINUS, nm->mkNode(STRING_LENGTH, t), n));
+ STRING_SUBSTR, t, n, nm->mkNode(SUB, nm->mkNode(STRING_LENGTH, t), n));
}
Node getConstantComponent(Node t)
n = d_nodeManager->mkNode(PLUS, x, y);
ASSERT_EQ(PLUS, n.getKind());
- n = d_nodeManager->mkNode(UMINUS, x);
- ASSERT_EQ(UMINUS, n.getKind());
+ n = d_nodeManager->mkNode(NEG, x);
+ ASSERT_EQ(NEG, n.getKind());
}
TEST_F(TestNodeBlackNode, getOperator)
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 x_minus_y = d_nodeManager->mkNode(kind::MINUS, x, y);
+ Node x_minus_y = d_nodeManager->mkNode(kind::SUB, x, y);
{ // iterator
Node::kinded_iterator i = plus_x_y_z.begin(PLUS);
Node p = d_nodeManager->mkNode(
EQUAL,
d_nodeManager->mkConst<Rational>(CONST_RATIONAL, 0),
- d_nodeManager->mkNode(PLUS, r, d_nodeManager->mkNode(UMINUS, s), t));
+ d_nodeManager->mkNode(PLUS, r, d_nodeManager->mkNode(NEG, s), t));
Node q = d_nodeManager->mkNode(AND, x, z, d_nodeManager->mkNode(NOT, y));
#ifdef CVC5_ASSERTIONS
t2 = d_nodeManager->mkNode(PLUS, {w, y, y, z, x});
ASSERT_TRUE(PolyNorm::isArithPolyNorm(t1, t2));
- t1 = d_nodeManager->mkNode(MINUS, t1, t2);
+ t1 = d_nodeManager->mkNode(SUB, t1, t2);
t2 = zero;
ASSERT_TRUE(PolyNorm::isArithPolyNorm(t1, t2));
- t1 = d_nodeManager->mkNode(UMINUS, d_nodeManager->mkNode(PLUS, x, y));
- t2 = d_nodeManager->mkNode(MINUS, zero, d_nodeManager->mkNode(PLUS, y, x));
+ t1 = d_nodeManager->mkNode(NEG, d_nodeManager->mkNode(PLUS, x, y));
+ t2 = d_nodeManager->mkNode(SUB, zero, d_nodeManager->mkNode(PLUS, y, x));
ASSERT_TRUE(PolyNorm::isArithPolyNorm(t1, t2));
- t1 = d_nodeManager->mkNode(MULT, d_nodeManager->mkNode(UMINUS, x), y);
- t2 = d_nodeManager->mkNode(MULT, d_nodeManager->mkNode(UMINUS, y), x);
+ 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));
// x + 5 < 6 |= 0 > x --> false
ASSERT_TRUE(!ae.checkWithAssumption(x_plus_five_lt_six, zero, x, true));
- Node neg_x = d_nodeManager->mkNode(kind::UMINUS, x);
+ Node neg_x = d_nodeManager->mkNode(kind::NEG, x);
Node x_plus_five_lt_five =
d_rewriter->rewrite(d_nodeManager->mkNode(kind::LT, x_plus_five, five));
{
RealAlgebraicNumber sqrt2({-2, 0, 1}, 1, 3);
Node n = d_nodeManager->mkRealAlgebraicNumber(sqrt2);
- n = d_nodeManager->mkNode(Kind::MINUS, n, n);
+ n = d_nodeManager->mkNode(Kind::SUB, n, n);
n = d_slvEngine->getRewriter()->rewrite(n);
EXPECT_EQ(n.getKind(), Kind::CONST_RATIONAL);
EXPECT_EQ(n.getConst<Rational>(), Rational(0));
RealAlgebraicNumber sqrt2({-2, 0, 1}, 1, 2);
Node m = d_nodeManager->mkRealAlgebraicNumber(msqrt2);
Node n = d_nodeManager->mkRealAlgebraicNumber(sqrt2);
- Node mm = d_nodeManager->mkNode(Kind::UMINUS, m);
- Node mn = d_nodeManager->mkNode(Kind::UMINUS, n);
+ Node mm = d_nodeManager->mkNode(Kind::NEG, m);
+ Node mn = d_nodeManager->mkNode(Kind::NEG, n);
mm = d_slvEngine->getRewriter()->rewrite(mm);
mn = d_slvEngine->getRewriter()->rewrite(mn);
EXPECT_EQ(-msqrt2, sqrt2);
projects / cvc5.git / commitdiff