Merge branch 'master' into refactorEagerSolverrefactorEagerSolver

4 files changed, 44 insertions, 24 deletions

diff --git a/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp
index 163a49b8c..425ab0484 100644
--- a/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp
+++ b/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp
@@ -36,8 +36,8 @@ namespace quantifiers {
 ArithInstantiator::ArithInstantiator(Env& env, TypeNode tn, VtsTermCache* vtc)
     : Instantiator(env, tn), d_vtc(vtc)
 {
-  d_zero = NodeManager::currentNM()->mkConst(Rational(0));
-  d_one = NodeManager::currentNM()->mkConst(Rational(1));
+  d_zero = NodeManager::currentNM()->mkConst(CONST_RATIONAL, Rational(0));
+  d_one = NodeManager::currentNM()->mkConst(CONST_RATIONAL, Rational(1));
 }
 
 void ArithInstantiator::reset(CegInstantiator* ci,
@@ -185,7 +185,8 @@ bool ArithInstantiator::processAssertion(CegInstantiator* ci,
           uval = nm->mkNode(
               PLUS,
               val,
-              nm->mkConst(Rational(isUpperBoundCTT(uires) ? 1 : -1)));
+              nm->mkConst(CONST_RATIONAL,
+                          Rational(isUpperBoundCTT(uires) ? 1 : -1)));
           uval = rewrite(uval);
         }
         else
@@ -252,8 +253,11 @@ bool ArithInstantiator::processAssertion(CegInstantiator* ci,
       if (d_type.isInteger())
       {
         uires = is_upper ? CEG_TT_LOWER : CEG_TT_UPPER;
-        uval = nm->mkNode(
-            PLUS, val, nm->mkConst(Rational(isUpperBoundCTT(uires) ? 1 : -1)));
+        uval =
+            nm->mkNode(PLUS,
+                       val,
+                       nm->mkConst(CONST_RATIONAL,
+                                   Rational(isUpperBoundCTT(uires) ? 1 : -1)));
         uval = rewrite(uval);
       }
       else
@@ -274,8 +278,8 @@ bool ArithInstantiator::processAssertion(CegInstantiator* ci,
     {
       if (options().quantifiers.cegqiModel)
       {
-        Node delta_coeff =
-            nm->mkConst(Rational(isUpperBoundCTT(uires) ? 1 : -1));
+        Node delta_coeff = nm->mkConst(
+            CONST_RATIONAL, Rational(isUpperBoundCTT(uires) ? 1 : -1));
         if (vts_coeff_delta.isNull())
         {
           vts_coeff_delta = delta_coeff;
@@ -451,8 +455,9 @@ bool ArithInstantiator::processAssertions(CegInstantiator* ci,
             Assert(d_mbp_coeff[rr][j].isConst());
             value[t] = nm->mkNode(
                 MULT,
-                nm->mkConst(Rational(1)
-                            / d_mbp_coeff[rr][j].getConst<Rational>()),
+                nm->mkConst(
+                    CONST_RATIONAL,
+                    Rational(1) / d_mbp_coeff[rr][j].getConst<Rational>()),
                 value[t]);
             value[t] = rewrite(value[t]);
           }
@@ -606,9 +611,10 @@ bool ArithInstantiator::processAssertions(CegInstantiator* ci,
       }
       else
       {
-        val = nm->mkNode(MULT,
-                         nm->mkNode(PLUS, vals[0], vals[1]),
-                         nm->mkConst(Rational(1) / Rational(2)));
+        val =
+            nm->mkNode(MULT,
+                       nm->mkNode(PLUS, vals[0], vals[1]),
+                       nm->mkConst(CONST_RATIONAL, Rational(1) / Rational(2)));
         val = rewrite(val);
       }
     }
@@ -803,7 +809,7 @@ CegTermType ArithInstantiator::solve_arith(CegInstantiator* ci,
         vts_coeff[t] = itminf->second;
         if (vts_coeff[t].isNull())
         {
-          vts_coeff[t] = nm->mkConst(Rational(1));
+          vts_coeff[t] = nm->mkConst(CONST_RATIONAL, Rational(1));
         }
         // negate if coefficient on variable is positive
         std::map<Node, Node>::iterator itv = msum.find(pv);
@@ -820,7 +826,8 @@ CegTermType ArithInstantiator::solve_arith(CegInstantiator* ci,
             {
               vts_coeff[t] = nm->mkNode(
                   MULT,
-                  nm->mkConst(Rational(-1) / itv->second.getConst<Rational>()),
+                  nm->mkConst(CONST_RATIONAL,
+                              Rational(-1) / itv->second.getConst<Rational>()),
                   vts_coeff[t]);
               vts_coeff[t] = rewrite(vts_coeff[t]);
             }
@@ -880,7 +887,7 @@ CegTermType ArithInstantiator::solve_arith(CegInstantiator* ci,
       }
     }
     // multiply everything by this coefficient
-    Node rcoeff = nm->mkConst(Rational(coeff));
+    Node rcoeff = nm->mkConst(CONST_RATIONAL, Rational(coeff));
     std::vector<Node> real_part;
     for (std::map<Node, Node>::iterator it = msum.begin(); it != msum.end();
          ++it)
diff --git a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
index 9dc11955b..494ac8e53 100644
--- a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
+++ b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
@@ -138,7 +138,8 @@ void TermProperties::composeProperty(TermProperties& p)
   else
   {
     NodeManager* nm = NodeManager::currentNM();
-    d_coeff = nm->mkConst(Rational(d_coeff.getConst<Rational>()
+    d_coeff = nm->mkConst(CONST_RATIONAL,
+                          Rational(d_coeff.getConst<Rational>()
                                    * p.d_coeff.getConst<Rational>()));
   }
 }
@@ -165,7 +166,8 @@ void SolvedForm::push_back(Node pv, Node n, TermProperties& pv_prop)
     Assert(new_theta.getKind() == CONST_RATIONAL);
     Assert(pv_prop.d_coeff.getKind() == CONST_RATIONAL);
     NodeManager* nm = NodeManager::currentNM();
-    new_theta = nm->mkConst(Rational(new_theta.getConst<Rational>()
+    new_theta = nm->mkConst(CONST_RATIONAL,
+                            Rational(new_theta.getConst<Rational>()
                                      * pv_prop.d_coeff.getConst<Rational>()));
   }
   d_theta.push_back(new_theta);
@@ -1151,7 +1153,12 @@ Node CegInstantiator::applySubstitution( TypeNode tn, Node n, std::vector< Node
         if( !prop[i].d_coeff.isNull() ){
           Assert(vars[i].getType().isInteger());
           Assert(prop[i].d_coeff.isConst());
-          Node nn = NodeManager::currentNM()->mkNode( MULT, subs[i], NodeManager::currentNM()->mkConst( Rational(1)/prop[i].d_coeff.getConst<Rational>() ) );
+          Node nn = NodeManager::currentNM()->mkNode(
+              MULT,
+              subs[i],
+              NodeManager::currentNM()->mkConst(
+                  CONST_RATIONAL,
+                  Rational(1) / prop[i].d_coeff.getConst<Rational>()));
           nn = NodeManager::currentNM()->mkNode( kind::TO_INTEGER, nn );
           nn = rewrite(nn);
           nsubs.push_back( nn );
@@ -1199,8 +1206,9 @@ Node CegInstantiator::applySubstitution( TypeNode tn, Node n, std::vector< Node
             Node c_coeff;
             if( !msum_coeff[it->first].isNull() ){
               c_coeff = rewrite(NodeManager::currentNM()->mkConst(
+                  CONST_RATIONAL,
                   pv_prop.d_coeff.getConst<Rational>()
-                  / msum_coeff[it->first].getConst<Rational>()));
+                      / msum_coeff[it->first].getConst<Rational>()));
             }else{
               c_coeff = pv_prop.d_coeff;
             }
@@ -1264,7 +1272,7 @@ Node CegInstantiator::applySubstitutionToLiteral( Node lit, std::vector< Node >&
       }else{
         atom_lhs = nm->mkNode(MINUS, atom[0], atom[1]);
         atom_lhs = rewrite(atom_lhs);
-        atom_rhs = nm->mkConst(Rational(0));
+        atom_rhs = nm->mkConst(CONST_RATIONAL, Rational(0));
       }
       //must be an eligible term
       if( isEligible( atom_lhs ) ){
diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
index 6340e2a2a..65ad79e29 100644
--- a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
+++ b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
@@ -58,8 +58,8 @@ InstStrategyCegqi::InstStrategyCegqi(Env& env,
       d_added_cbqi_lemma(userContext()),
       d_vtsCache(new VtsTermCache(qim)),
       d_bv_invert(nullptr),
-      d_small_const_multiplier(
-          NodeManager::currentNM()->mkConst(Rational(1) / Rational(1000000))),
+      d_small_const_multiplier(NodeManager::currentNM()->mkConst(
+          CONST_RATIONAL, Rational(1) / Rational(1000000))),
       d_small_const(d_small_const_multiplier)
 {
   d_check_vts_lemma_lc = false;
@@ -453,7 +453,12 @@ void InstStrategyCegqi::process( Node q, Theory::Effort effort, int e ) {
       d_vtsCache->getVtsTerms(inf, true, false, false);
       for( unsigned i=0; i<inf.size(); i++ ){
         Trace("quant-vts-debug") << "Infinity lemma for " << inf[i] << " " << d_small_const << std::endl;
-        Node inf_lem_lb = NodeManager::currentNM()->mkNode( GT, inf[i], NodeManager::currentNM()->mkConst( Rational(1)/d_small_const.getConst<Rational>() ) );
+        Node inf_lem_lb = NodeManager::currentNM()->mkNode(
+            GT,
+            inf[i],
+            NodeManager::currentNM()->mkConst(
+                CONST_RATIONAL,
+                Rational(1) / d_small_const.getConst<Rational>()));
         d_qim.lemma(inf_lem_lb, InferenceId::QUANTIFIERS_CEGQI_VTS_LB_INF);
       }
     }
diff --git a/src/theory/quantifiers/cegqi/vts_term_cache.cpp b/src/theory/quantifiers/cegqi/vts_term_cache.cpp
index fe47f1dd1..37ded9b7f 100644
--- a/src/theory/quantifiers/cegqi/vts_term_cache.cpp
+++ b/src/theory/quantifiers/cegqi/vts_term_cache.cpp
@@ -30,7 +30,7 @@ namespace quantifiers {
 
 VtsTermCache::VtsTermCache(QuantifiersInferenceManager& qim) : d_qim(qim)
 {
-  d_zero = NodeManager::currentNM()->mkConst(Rational(0));
+  d_zero = NodeManager::currentNM()->mkConst(CONST_RATIONAL, Rational(0));
 }
 
 void VtsTermCache::getVtsTerms(std::vector<Node>& t,