From c956118d285deea24c3389e851deda0d83cf9e5f Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 22 Dec 2021 11:17:52 -0600 Subject: [PATCH] Remove most uses of mkRationalNode (#7854) Towards eliminating arithmetic subtyping. --- src/theory/arith/approx_simplex.cpp | 17 ------- src/theory/arith/arith_ite_utils.cpp | 30 ++++++++----- src/theory/arith/arith_rewriter.cpp | 8 ++-- src/theory/arith/arith_static_learner.cpp | 26 +++++------ src/theory/arith/arith_utilities.h | 44 +++++++++--------- src/theory/arith/congruence_manager.cpp | 18 +++++--- src/theory/arith/constraint.cpp | 14 +++--- src/theory/arith/nl/ext/monomial.cpp | 8 ++-- src/theory/arith/normal_form.h | 1 - src/theory/arith/theory_arith_private.cpp | 55 ++++++++++------------- 10 files changed, 102 insertions(+), 119 deletions(-) diff --git a/src/theory/arith/approx_simplex.cpp b/src/theory/arith/approx_simplex.cpp index 5b225ef30..5ec46b00c 100644 --- a/src/theory/arith/approx_simplex.cpp +++ b/src/theory/arith/approx_simplex.cpp @@ -1703,23 +1703,6 @@ MipResult ApproxGLPK::solveMIP(bool activelyLog){ } } -// Node explainSet(const set& inp){ -// Assert(!inp.empty()); -// NodeBuilder nb(kind::AND); -// set::const_iterator iter, end; -// for(iter = inp.begin(), end = inp.end(); iter != end; ++iter){ -// const ConstraintP c = *iter; -// Assert(c != NullConstraint); -// c->explainForConflict(nb); -// } -// Node ret = safeConstructNary(nb); -// Node rew = rewrite(ret); -// if(rew.getNumChildren() < ret.getNumChildren()){ -// //Debug("approx::") << "explainSet " << ret << " " << rew << endl; -// } -// return rew; -// } - DeltaRational sumConstraints(const DenseMap& xs, const DenseMap& cs, bool* anyinf){ if(anyinf != NULL){ *anyinf = false; diff --git a/src/theory/arith/arith_ite_utils.cpp b/src/theory/arith/arith_ite_utils.cpp index d986dd74b..36cd18aa1 100644 --- a/src/theory/arith/arith_ite_utils.cpp +++ b/src/theory/arith/arith_ite_utils.cpp @@ -59,7 +59,8 @@ Node ArithIteUtils::reduceVariablesInItes(Node n){ switch(n.getKind()){ case ITE:{ Node c = n[0], t = n[1], e = n[2]; - if (n.getType().isRealOrInt()) + TypeNode tn = n.getType(); + if (tn.isRealOrInt()) { Node rc = reduceVariablesInItes(c); Node rt = reduceVariablesInItes(t); @@ -69,15 +70,15 @@ Node ArithIteUtils::reduceVariablesInItes(Node n){ Node ve = d_varParts[e]; Node vpite = (vt == ve) ? vt : Node::null(); + NodeManager* nm = NodeManager::currentNM(); if(vpite.isNull()){ Node rite = rc.iteNode(rt, re); // do not apply d_reduceVar[n] = rite; - d_constants[n] = mkRationalNode(Rational(0)); + d_constants[n] = nm->mkConstRealOrInt(tn, Rational(0)); d_varParts[n] = rite; // treat the ite as a variable return rite; }else{ - NodeManager* nm = NodeManager::currentNM(); Node constantite = rc.iteNode(d_constants[t], d_constants[e]); Node sum = nm->mkNode(kind::PLUS, vpite, constantite); d_reduceVar[n] = sum; @@ -99,7 +100,9 @@ Node ArithIteUtils::reduceVariablesInItes(Node n){ } }break; default: - if (n.getType().isRealOrInt() && Polynomial::isMember(n)) + { + TypeNode tn = n.getType(); + if (tn.isRealOrInt() && Polynomial::isMember(n)) { Node newn = Node::null(); if(!d_contains.containsTermITE(n)){ @@ -111,15 +114,15 @@ Node ArithIteUtils::reduceVariablesInItes(Node n){ }else{ newn = n; } - + NodeManager* nm = NodeManager::currentNM(); Polynomial p = Polynomial::parsePolynomial(newn); if(p.isConstant()){ d_constants[n] = newn; - d_varParts[n] = mkRationalNode(Rational(0)); + d_varParts[n] = nm->mkConstRealOrInt(tn, Rational(0)); // don't bother adding to d_reduceVar return newn; }else if(!p.containsConstant()){ - d_constants[n] = mkRationalNode(Rational(0)); + d_constants[n] = nm->mkConstRealOrInt(tn, Rational(0)); d_varParts[n] = newn; d_reduceVar[n] = p.getNode(); return p.getNode(); @@ -144,6 +147,7 @@ Node ArithIteUtils::reduceVariablesInItes(Node n){ return n; } } + } break; } Unreachable(); @@ -204,8 +208,9 @@ const Integer& ArithIteUtils::gcdIte(Node n){ Node ArithIteUtils::reduceIteConstantIteByGCD_rec(Node n, const Rational& q){ if(n.isConst()){ - Assert(n.getKind() == kind::CONST_RATIONAL); - return mkRationalNode(n.getConst() * q); + Assert(n.getType().isRealOrInt()); + return NodeManager::currentNM()->mkConstRealOrInt( + n.getType(), n.getConst() * q); }else{ Assert(n.getKind() == kind::ITE); Assert(n.getType().isInteger()); @@ -220,19 +225,20 @@ Node ArithIteUtils::reduceIteConstantIteByGCD(Node n){ Assert(n.getKind() == kind::ITE); Assert(n.getType().isRealOrInt()); const Integer& gcd = gcdIte(n); + NodeManager* nm = NodeManager::currentNM(); if(gcd.isOne()){ Node newIte = reduceConstantIteByGCD(n[0]).iteNode(n[1],n[2]); d_reduceGcd[n] = newIte; return newIte; }else if(gcd.isZero()){ - Node zeroNode = mkRationalNode(Rational(0)); + Node zeroNode = nm->mkConstRealOrInt(n.getType(), Rational(0)); d_reduceGcd[n] = zeroNode; return zeroNode; }else{ Rational divBy(Integer(1), gcd); Node redite = reduceIteConstantIteByGCD_rec(n, divBy); - Node gcdNode = mkRationalNode(Rational(gcd)); - Node multIte = NodeManager::currentNM()->mkNode(kind::MULT, gcdNode, redite); + Node gcdNode = nm->mkConstRealOrInt(n.getType(), Rational(gcd)); + Node multIte = nm->mkNode(kind::MULT, gcdNode, redite); d_reduceGcd[n] = multIte; return multIte; } diff --git a/src/theory/arith/arith_rewriter.cpp b/src/theory/arith/arith_rewriter.cpp index f7d2a2a11..4e79515bd 100644 --- a/src/theory/arith/arith_rewriter.cpp +++ b/src/theory/arith/arith_rewriter.cpp @@ -226,7 +226,9 @@ RewriteResponse ArithRewriter::postRewriteTerm(TNode t){ const Rational& exp = t[1].getConst(); TNode base = t[0]; if(exp.sgn() == 0){ - return RewriteResponse(REWRITE_DONE, mkRationalNode(Rational(1))); + return RewriteResponse(REWRITE_DONE, + NodeManager::currentNM()->mkConstRealOrInt( + t.getType(), Rational(1))); }else if(exp.sgn() > 0 && exp.isIntegral()){ cvc5::Rational r(expr::NodeValue::MAX_CHILDREN); if (exp <= r) @@ -536,7 +538,7 @@ RewriteResponse ArithRewriter::postRewriteTranscendental(TNode t) { Rational r = pi_factor.getConst(); Rational r_abs = r.abs(); Rational rone = Rational(1); - Node ntwo = mkRationalNode(Rational(2)); + Node ntwo = nm->mkConstInt(Rational(2)); if (r_abs > rone) { //add/substract 2*pi beyond scope @@ -880,7 +882,7 @@ RewriteResponse ArithRewriter::rewriteIntsDivModTotal(TNode t, bool pre) if (k == kind::INTS_MODULUS_TOTAL) { // (mod x 1) --> 0 - return returnRewrite(t, mkRationalNode(0), Rewrite::MOD_BY_ONE); + return returnRewrite(t, nm->mkConstInt(0), Rewrite::MOD_BY_ONE); } Assert(k == kind::INTS_DIVISION_TOTAL); // (div x 1) --> x diff --git a/src/theory/arith/arith_static_learner.cpp b/src/theory/arith/arith_static_learner.cpp index 07582f222..7a10d23bc 100644 --- a/src/theory/arith/arith_static_learner.cpp +++ b/src/theory/arith/arith_static_learner.cpp @@ -200,14 +200,11 @@ void ArithStaticLearner::iteConstant(TNode n, NodeBuilder& learned) CDNodeToMinMaxMap::const_iterator minFind = d_minMap.find(n); if (minFind == d_minMap.end() || (*minFind).second < min) { d_minMap.insert(n, min); - Node nGeqMin; - if (min.getInfinitesimalPart() == 0) { - nGeqMin = NodeBuilder(kind::GEQ) - << n << mkRationalNode(min.getNoninfinitesimalPart()); - } else { - nGeqMin = NodeBuilder(kind::GT) - << n << mkRationalNode(min.getNoninfinitesimalPart()); - } + NodeManager* nm = NodeManager::currentNM(); + Node nGeqMin = nm->mkNode( + min.getInfinitesimalPart() == 0 ? kind::GEQ : kind::GT, + n, + nm->mkConstRealOrInt(n.getType(), min.getNoninfinitesimalPart())); learned << nGeqMin; Debug("arith::static") << n << " iteConstant" << nGeqMin << endl; ++(d_statistics.d_iteConstantApplications); @@ -221,14 +218,11 @@ void ArithStaticLearner::iteConstant(TNode n, NodeBuilder& learned) CDNodeToMinMaxMap::const_iterator maxFind = d_maxMap.find(n); if (maxFind == d_maxMap.end() || (*maxFind).second > max) { d_maxMap.insert(n, max); - Node nLeqMax; - if (max.getInfinitesimalPart() == 0) { - nLeqMax = NodeBuilder(kind::LEQ) - << n << mkRationalNode(max.getNoninfinitesimalPart()); - } else { - nLeqMax = NodeBuilder(kind::LT) - << n << mkRationalNode(max.getNoninfinitesimalPart()); - } + NodeManager* nm = NodeManager::currentNM(); + Node nLeqMax = nm->mkNode( + max.getInfinitesimalPart() == 0 ? kind::LEQ : kind::LT, + n, + nm->mkConstRealOrInt(n.getType(), max.getNoninfinitesimalPart())); learned << nLeqMax; Debug("arith::static") << n << " iteConstant" << nLeqMax << endl; ++(d_statistics.d_iteConstantApplications); diff --git a/src/theory/arith/arith_utilities.h b/src/theory/arith/arith_utilities.h index 027f7a65a..1e844f829 100644 --- a/src/theory/arith/arith_utilities.h +++ b/src/theory/arith/arith_utilities.h @@ -223,24 +223,23 @@ inline Node flattenAnd(Node n){ } // Returns an node that is the identity of a select few kinds. -inline Node getIdentity(Kind k){ - switch(k){ - case kind::AND: - return mkBoolNode(true); - case kind::PLUS: - return mkRationalNode(0); - case kind::MULT: - case kind::NONLINEAR_MULT: - return mkRationalNode(1); - default: Unreachable(); return Node::null(); // silence warning +inline Node getIdentityType(const TypeNode& tn, Kind k) +{ + switch (k) + { + case kind::PLUS: return NodeManager::currentNM()->mkConstRealOrInt(tn, 0); + case kind::MULT: + case kind::NONLINEAR_MULT: + return NodeManager::currentNM()->mkConstRealOrInt(tn, 1); + default: Unreachable(); return Node::null(); // silence warning } } -inline Node safeConstructNary(NodeBuilder& nb) +inline Node mkAndFromBuilder(NodeBuilder& nb) { + Assert(nb.getKind() == kind::AND); switch (nb.getNumChildren()) { - case 0: - return getIdentity(nb.getKind()); + case 0: return mkBoolNode(true); case 1: return nb[0]; default: @@ -248,14 +247,15 @@ inline Node safeConstructNary(NodeBuilder& nb) } } -inline Node safeConstructNary(Kind k, const std::vector& children) { - switch (children.size()) { - case 0: - return getIdentity(k); - case 1: - return children[0]; - default: - return NodeManager::currentNM()->mkNode(k, children); +inline Node safeConstructNaryType(const TypeNode& tn, + Kind k, + const std::vector& children) +{ + switch (children.size()) + { + case 0: return getIdentityType(tn, k); + case 1: return children[0]; + default: return NodeManager::currentNM()->mkNode(k, children); } } @@ -277,7 +277,7 @@ inline Node mkInRange(Node term, Node start, Node end) { // when n is 0 or not. Useful for division by 0 logic. // (ite (= n 0) (= q if_zero) (= q not_zero)) inline Node mkOnZeroIte(Node n, Node q, Node if_zero, Node not_zero) { - Node zero = mkRationalNode(0); + Node zero = NodeManager::currentNM()->mkConstRealOrInt(n.getType(), 0); return n.eqNode(zero).iteNode(q.eqNode(if_zero), q.eqNode(not_zero)); } diff --git a/src/theory/arith/congruence_manager.cpp b/src/theory/arith/congruence_manager.cpp index de68a4987..6dc501c96 100644 --- a/src/theory/arith/congruence_manager.cpp +++ b/src/theory/arith/congruence_manager.cpp @@ -238,7 +238,7 @@ void ArithCongruenceManager::watchedVariableIsZero(ConstraintCP lb, ConstraintCP NodeBuilder reasonBuilder(Kind::AND); auto pfLb = lb->externalExplainByAssertions(reasonBuilder); auto pfUb = ub->externalExplainByAssertions(reasonBuilder); - Node reason = safeConstructNary(reasonBuilder); + Node reason = mkAndFromBuilder(reasonBuilder); std::shared_ptr pf{}; if (isProofEnabled()) { @@ -280,7 +280,7 @@ void ArithCongruenceManager::watchedVariableIsZero(ConstraintCP eq){ pf = d_pnm->mkNode( PfRule::MACRO_SR_PRED_TRANSFORM, {pf}, {d_watchedEqualities[s]}); } - Node reason = safeConstructNary(nb); + Node reason = mkAndFromBuilder(nb); d_keepAlive.push_back(reason); assertionToEqualityEngine(true, s, reason, pf); @@ -305,7 +305,7 @@ void ArithCongruenceManager::watchedVariableCannotBeZero(ConstraintCP c){ pf->printDebug(Debug("arith::cong::notzero")); Debug("arith::cong::notzero") << std::endl; } - Node reason = safeConstructNary(nb); + Node reason = mkAndFromBuilder(nb); if (isProofEnabled()) { if (c->getType() == ConstraintType::Disequality) @@ -636,7 +636,9 @@ void ArithCongruenceManager::equalsConstant(ConstraintCP c){ ArithVar x = c->getVariable(); Node xAsNode = d_avariables.asNode(x); - Node asRational = mkRationalNode(c->getValue().getNoninfinitesimalPart()); + NodeManager* nm = NodeManager::currentNM(); + Node asRational = nm->mkConstRealOrInt( + xAsNode.getType(), c->getValue().getNoninfinitesimalPart()); // No guarentee this is in normal form! // Note though, that it happens to be in proof normal form! @@ -645,7 +647,7 @@ void ArithCongruenceManager::equalsConstant(ConstraintCP c){ NodeBuilder nb(Kind::AND); auto pf = c->externalExplainByAssertions(nb); - Node reason = safeConstructNary(nb); + Node reason = mkAndFromBuilder(nb); d_keepAlive.push_back(reason); Trace("arith-ee") << "Assert equalsConstant " << eq << ", reason " << reason << std::endl; @@ -665,10 +667,12 @@ void ArithCongruenceManager::equalsConstant(ConstraintCP lb, ConstraintCP ub){ NodeBuilder nb(Kind::AND); auto pfLb = lb->externalExplainByAssertions(nb); auto pfUb = ub->externalExplainByAssertions(nb); - Node reason = safeConstructNary(nb); + Node reason = mkAndFromBuilder(nb); Node xAsNode = d_avariables.asNode(x); - Node asRational = mkRationalNode(lb->getValue().getNoninfinitesimalPart()); + NodeManager* nm = NodeManager::currentNM(); + Node asRational = nm->mkConstRealOrInt( + xAsNode.getType(), lb->getValue().getNoninfinitesimalPart()); // No guarentee this is in normal form! // Note though, that it happens to be in proof normal form! diff --git a/src/theory/arith/constraint.cpp b/src/theory/arith/constraint.cpp index a9576e0cc..806079f62 100644 --- a/src/theory/arith/constraint.cpp +++ b/src/theory/arith/constraint.cpp @@ -519,7 +519,7 @@ TrustNode Constraint::externalExplainByAssertions() const { NodeBuilder nb(kind::AND); auto pfFromAssumptions = externalExplain(nb, AssertionOrderSentinel); - Node exp = safeConstructNary(nb); + Node exp = mkAndFromBuilder(nb); if (d_database->isProofEnabled()) { std::vector assumptions; @@ -533,7 +533,7 @@ TrustNode Constraint::externalExplainByAssertions() const } auto pf = d_database->d_pnm->mkScope(pfFromAssumptions, assumptions); return d_database->d_pfGen->mkTrustedPropagation( - getLiteral(), safeConstructNary(Kind::AND, assumptions), pf); + getLiteral(), NodeManager::currentNM()->mkAnd(assumptions), pf); } return TrustNode::mkTrustPropExp(getLiteral(), exp); } @@ -1548,7 +1548,7 @@ TrustNode Constraint::externalExplainForPropagation(TNode lit) const Assert(!isInternalAssumption()); NodeBuilder nb(Kind::AND); auto pfFromAssumptions = externalExplain(nb, d_assertionOrder); - Node n = safeConstructNary(nb); + Node n = mkAndFromBuilder(nb); if (d_database->isProofEnabled()) { std::vector assumptions; @@ -1567,7 +1567,7 @@ TrustNode Constraint::externalExplainForPropagation(TNode lit) const } auto pf = d_database->d_pnm->mkScope(pfFromAssumptions, assumptions); return d_database->d_pfGen->mkTrustedPropagation( - lit, safeConstructNary(Kind::AND, assumptions), pf); + lit, NodeManager::currentNM()->mkAnd(assumptions), pf); } else { @@ -1583,7 +1583,7 @@ TrustNode Constraint::externalExplainConflict() const auto pf1 = externalExplainByAssertions(nb); auto not2 = getNegation()->getProofLiteral().negate(); auto pf2 = getNegation()->externalExplainByAssertions(nb); - Node n = safeConstructNary(nb); + Node n = mkAndFromBuilder(nb); if (d_database->isProofEnabled()) { auto pfNot2 = d_database->d_pnm->mkNode( @@ -1621,7 +1621,7 @@ TrustNode Constraint::externalExplainConflict() const } auto confPf = d_database->d_pnm->mkScope(bot, lits); return d_database->d_pfGen->mkTrustNode( - safeConstructNary(Kind::AND, lits), confPf, true); + NodeManager::currentNM()->mkAnd(lits), confPf, true); } else { @@ -1682,7 +1682,7 @@ Node Constraint::externalExplain(const ConstraintCPVec& v, AssertionOrder order) ConstraintCP v_i = *i; v_i->externalExplain(nb, order); } - return safeConstructNary(nb); + return mkAndFromBuilder(nb); } std::shared_ptr Constraint::externalExplain( diff --git a/src/theory/arith/nl/ext/monomial.cpp b/src/theory/arith/nl/ext/monomial.cpp index 47beb6959..d71b41da6 100644 --- a/src/theory/arith/nl/ext/monomial.cpp +++ b/src/theory/arith/nl/ext/monomial.cpp @@ -182,8 +182,10 @@ void MonomialDb::registerMonomialSubset(Node a, Node b) d_m_contain_parent[a].push_back(b); d_m_contain_children[b].push_back(a); - Node mult_term = safeConstructNary(MULT, diff_children); - Node nlmult_term = safeConstructNary(NONLINEAR_MULT, diff_children); + // currently use real type here + TypeNode tn = NodeManager::currentNM()->realType(); + Node mult_term = safeConstructNaryType(tn, MULT, diff_children); + Node nlmult_term = safeConstructNaryType(tn, NONLINEAR_MULT, diff_children); d_m_contain_mult[a][b] = mult_term; d_m_contain_umult[a][b] = nlmult_term; Trace("nl-ext-mindex") << "..." << a << " is a subset of " << b @@ -325,7 +327,7 @@ Node MonomialDb::mkMonomialRemFactor(Node n, << "......rem, now " << inc << " factors of " << v << std::endl; children.insert(children.end(), inc, v); } - Node ret = safeConstructNary(MULT, children); + Node ret = safeConstructNaryType(n.getType(), MULT, children); Trace("nl-ext-mono-factor") << "...return : " << ret << std::endl; return ret; } diff --git a/src/theory/arith/normal_form.h b/src/theory/arith/normal_form.h index 4084ed11c..577bd052d 100644 --- a/src/theory/arith/normal_form.h +++ b/src/theory/arith/normal_form.h @@ -335,7 +335,6 @@ public: size_t getComplexity() const; };/* class Variable */ - class Constant : public NodeWrapper { public: Constant(Node n) : NodeWrapper(n) { Assert(isMember(getNode())); } diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp index 9b4623d37..4efdfc2bf 100644 --- a/src/theory/arith/theory_arith_private.cpp +++ b/src/theory/arith/theory_arith_private.cpp @@ -235,17 +235,6 @@ static void resolve(ConstraintCPVec& buf, ConstraintP c, const ConstraintCPVec& } } Assert(negPos < neg.size()); - - // Assert(dnconf.getKind() == kind::AND); - // Assert(upconf.getKind() == kind::AND); - // Assert(dnpos < dnconf.getNumChildren()); - // Assert(uppos < upconf.getNumChildren()); - // Assert(equalUpToNegation(dnconf[dnpos], upconf[uppos])); - - // NodeBuilder nb(kind::AND); - // dropPosition(nb, dnconf, dnpos); - // dropPosition(nb, upconf, uppos); - // return safeConstructNary(nb); } TheoryArithPrivate::ModelException::ModelException(TNode n, const char* msg) @@ -959,7 +948,7 @@ Node TheoryArithPrivate::getModelValue(TNode term) { const DeltaRational drv = getDeltaValue(term); const Rational& delta = d_partialModel.getDelta(); const Rational qmodel = drv.substituteDelta( delta ); - return mkRationalNode( qmodel ); + return NodeManager::currentNM()->mkConstRealOrInt(term.getType(), qmodel); } catch (DeltaRationalException& dr) { return Node::null(); } catch (ModelException& me) { @@ -1960,7 +1949,9 @@ std::pair TheoryArithPrivate::replayGetConstraint(const D Assert(k == kind::LEQ || k == kind::GEQ); - Node comparison = NodeManager::currentNM()->mkNode(k, sum, mkRationalNode(rhs)); + NodeManager* nm = NodeManager::currentNM(); + Node comparison = + nm->mkNode(k, sum, nm->mkConstRealOrInt(sum.getType(), rhs)); Node rewritten = rewrite(comparison); if(!(Comparison::isNormalAtom(rewritten))){ return make_pair(NullConstraint, added); @@ -2060,21 +2051,12 @@ std::pair TheoryArithPrivate::replayGetConstraint(const C return replayGetConstraint(lhs, k, rhs, ci.getKlass() == BranchCutKlass); } -// Node denseVectorToLiteral(const ArithVariables& vars, const DenseVector& dv, -// Kind k){ -// NodeManager* nm = NodeManager::currentNM(); -// Node sumLhs = toSumNode(vars, dv.lhs); -// Node ineq = nm->mkNode(k, sumLhs, mkRationalNode(dv.rhs) ); -// Node lit = rewrite(ineq); -// return lit; -// } - Node toSumNode(const ArithVariables& vars, const DenseMap& sum){ Debug("arith::toSumNode") << "toSumNode() begin" << endl; - NodeBuilder nb(kind::PLUS); NodeManager* nm = NodeManager::currentNM(); DenseMap::const_iterator iter, end; iter = sum.begin(), end = sum.end(); + std::vector children; for(; iter != end; ++iter){ ArithVar x = *iter; if(!vars.hasNode(x)){ return Node::null(); } @@ -2082,10 +2064,19 @@ Node toSumNode(const ArithVariables& vars, const DenseMap& sum){ const Rational& q = sum[x]; Node mult = nm->mkNode(kind::MULT, mkRationalNode(q), xNode); Debug("arith::toSumNode") << "toSumNode() " << x << " " << mult << endl; - nb << mult; + children.push_back(mult); } Debug("arith::toSumNode") << "toSumNode() end" << endl; - return safeConstructNary(nb); + if (children.empty()) + { + // NOTE: real type assumed here + return nm->mkConstReal(Rational(0)); + } + else if (children.size() == 1) + { + return children[0]; + } + return nm->mkNode(kind::PLUS, children); } ConstraintCP TheoryArithPrivate::vectorToIntHoleConflict(const ConstraintCPVec& conflict){ @@ -2586,7 +2577,8 @@ Node TheoryArithPrivate::branchToNode(ApproximateSimplex* approx, } Rational fl(maybe_value.value().floor()); NodeManager* nm = NodeManager::currentNM(); - Node leq = nm->mkNode(kind::LEQ, n, mkRationalNode(fl)); + Node leq = + nm->mkNode(kind::LEQ, n, nm->mkConstRealOrInt(n.getType(), fl)); Node norm = rewrite(leq); return norm; } @@ -2600,11 +2592,10 @@ Node TheoryArithPrivate::cutToLiteral(ApproximateSimplex* approx, const CutInfo& const DenseMap& lhs = ci.getReconstruction().lhs; Node sum = toSumNode(d_partialModel, lhs); if(!sum.isNull()){ + NodeManager* nm = NodeManager::currentNM(); Kind k = ci.getKind(); Assert(k == kind::LEQ || k == kind::GEQ); - Node rhs = mkRationalNode(ci.getReconstruction().rhs); - - NodeManager* nm = NodeManager::currentNM(); + Node rhs = nm->mkConstRealOrInt(sum.getType(), ci.getReconstruction().rhs); Node ineq = nm->mkNode(k, sum, rhs); return rewrite(ineq); } @@ -3687,6 +3678,7 @@ void TheoryArithPrivate::propagate(Theory::Effort e) { } } + NodeManager* nm = NodeManager::currentNM(); while(d_congruenceManager.hasMorePropagations()){ TNode toProp = d_congruenceManager.getNextPropagation(); @@ -3706,7 +3698,7 @@ void TheoryArithPrivate::propagate(Theory::Effort e) { Node notNormalized = normalized.negate(); std::vector ants(exp.getNode().begin(), exp.getNode().end()); ants.push_back(notNormalized); - Node lp = safeConstructNary(kind::AND, ants); + Node lp = nm->mkAnd(ants); Debug("arith::prop") << "propagate conflict" << lp << endl; if (proofsEnabled()) { @@ -3901,6 +3893,7 @@ void TheoryArithPrivate::collectModelValues(const std::set& termSet, // TODO: // This is not very good for user push/pop.... // Revisit when implementing push/pop + NodeManager* nm = NodeManager::currentNM(); for(var_iterator vi = var_begin(), vend = var_end(); vi != vend; ++vi){ ArithVar v = *vi; @@ -3913,7 +3906,7 @@ void TheoryArithPrivate::collectModelValues(const std::set& termSet, const DeltaRational& mod = d_partialModel.getAssignment(v); Rational qmodel = mod.substituteDelta(delta); - Node qNode = mkRationalNode(qmodel); + Node qNode = nm->mkConstRealOrInt(term.getType(), qmodel); Debug("arith::collectModelInfo") << "m->assertEquality(" << term << ", " << qmodel << ", true)" << endl; // Add to the map arithModel[term] = qNode; -- 2.30.2