Remove most uses of mkRationalNode (#7854)

Towards eliminating arithmetic subtyping.

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<ConstraintP>& inp){
-//   Assert(!inp.empty());
-//   NodeBuilder nb(kind::AND);
-//   set<ConstraintP>::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<Rational>& xs, const DenseMap<ConstraintP>& 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<Rational>() * q);
+    Assert(n.getType().isRealOrInt());
+    return NodeManager::currentNM()->mkConstRealOrInt(
+        n.getType(), n.getConst<Rational>() * 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<Rational>();
           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>();
         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<Node>& 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<Node>& 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<ProofNode> 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<Node> 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<Node> 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<ProofNode> 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<ConstraintP, ArithVar> 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<ConstraintP, ArithVar> 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<Rational>& sum){
   Debug("arith::toSumNode") << "toSumNode() begin" << endl;
-  NodeBuilder nb(kind::PLUS);
   NodeManager* nm = NodeManager::currentNM();
   DenseMap<Rational>::const_iterator iter, end;
   iter = sum.begin(), end = sum.end();
+  std::vector<Node> 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<Rational>& 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<Rational>& 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<Node> 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<Node>& 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<Node>& 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;