Make cegqi subsolvers EnvObj (#7205)

Makes a few places do multiplication for Rational directly instead of invoking the rewriter.

diff --git a/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp
index 77b1d42a9f15827d871b15b226642e03b0ca295c..85e91fee30a892d8673c42ff2549daa6c67637dd 100644 (file)
--- a/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp
+++ b/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp
@@ -33,8 +33,8 @@ namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
-ArithInstantiator::ArithInstantiator(TypeNode tn, VtsTermCache* vtc)
-    : Instantiator(tn), d_vtc(vtc)
+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));
@@ -86,17 +86,15 @@ bool ArithInstantiator::processEquality(CegInstantiator* ci,
     {
       Trace("cegqi-arith-debug") << "...mult lhs by " << rhs_coeff << std::endl;
       eq_lhs = nm->mkNode(MULT, rhs_coeff, eq_lhs);
-      eq_lhs = Rewriter::rewrite(eq_lhs);
     }
     if (!lhs_coeff.isNull())
     {
       Trace("cegqi-arith-debug") << "...mult rhs by " << lhs_coeff << std::endl;
       eq_rhs = nm->mkNode(MULT, lhs_coeff, eq_rhs);
-      eq_rhs = Rewriter::rewrite(eq_rhs);
     }
   }
   Node eq = eq_lhs.eqNode(eq_rhs);
-  eq = Rewriter::rewrite(eq);
+  eq = rewrite(eq);
   Node val;
   TermProperties pv_prop;
   Node vts_coeff_inf;
@@ -188,7 +186,7 @@ bool ArithInstantiator::processAssertion(CegInstantiator* ci,
               PLUS,
               val,
               nm->mkConst(Rational(isUpperBoundCTT(uires) ? 1 : -1)));
-          uval = Rewriter::rewrite(uval);
+          uval = rewrite(uval);
         }
         else
         {
@@ -227,7 +225,7 @@ bool ArithInstantiator::processAssertion(CegInstantiator* ci,
           if (!pv_prop.isBasic())
           {
             lhs_value = pv_prop.getModifiedTerm(pv_value);
-            lhs_value = Rewriter::rewrite(lhs_value);
+            lhs_value = rewrite(lhs_value);
           }
           Trace("cegqi-arith-debug")
               << "Disequality : check model values " << lhs_value << " "
@@ -241,7 +239,7 @@ bool ArithInstantiator::processAssertion(CegInstantiator* ci,
           // where lhs or rhs contains a transcendental function. We consider
           // the bound to be an upper bound in this case.
           Node cmp = nm->mkNode(GEQ, lhs_value, rhs_value);
-          cmp = Rewriter::rewrite(cmp);
+          cmp = rewrite(cmp);
           is_upper = !cmp.isConst() || !cmp.getConst<bool>();
         }
       }
@@ -256,7 +254,7 @@ bool ArithInstantiator::processAssertion(CegInstantiator* ci,
         uires = is_upper ? CEG_TT_LOWER : CEG_TT_UPPER;
         uval = nm->mkNode(
             PLUS, val, nm->mkConst(Rational(isUpperBoundCTT(uires) ? 1 : -1)));
-        uval = Rewriter::rewrite(uval);
+        uval = rewrite(uval);
       }
       else
       {
@@ -285,7 +283,7 @@ bool ArithInstantiator::processAssertion(CegInstantiator* ci,
         else
         {
           vts_coeff_delta = nm->mkNode(PLUS, vts_coeff_delta, delta_coeff);
-          vts_coeff_delta = Rewriter::rewrite(vts_coeff_delta);
+          vts_coeff_delta = rewrite(vts_coeff_delta);
         }
       }
       else
@@ -293,7 +291,7 @@ bool ArithInstantiator::processAssertion(CegInstantiator* ci,
         Node delta = d_vtc->getVtsDelta();
         uval = nm->mkNode(
             uires == CEG_TT_UPPER_STRICT ? PLUS : MINUS, uval, delta);
-        uval = Rewriter::rewrite(uval);
+        uval = rewrite(uval);
       }
     }
     if (options::cegqiModel())
@@ -364,7 +362,7 @@ bool ArithInstantiator::processAssertions(CegInstantiator* ci,
         if (rr == 0)
         {
           val = nm->mkNode(UMINUS, val);
-          val = Rewriter::rewrite(val);
+          val = rewrite(val);
         }
         TermProperties pv_prop_no_bound;
         if (ci->constructInstantiationInc(pv, val, pv_prop_no_bound, sf))
@@ -456,7 +454,7 @@ bool ArithInstantiator::processAssertions(CegInstantiator* ci,
                 nm->mkConst(Rational(1)
                             / d_mbp_coeff[rr][j].getConst<Rational>()),
                 value[t]);
-            value[t] = Rewriter::rewrite(value[t]);
+            value[t] = rewrite(value[t]);
           }
           // check if new best, if we have not already set it.
           if (best != -1 && !new_best_set)
@@ -466,7 +464,7 @@ bool ArithInstantiator::processAssertions(CegInstantiator* ci,
             {
               Kind k = rr == 0 ? GEQ : LEQ;
               Node cmp_bound = nm->mkNode(k, value[t], best_bound_value[t]);
-              cmp_bound = Rewriter::rewrite(cmp_bound);
+              cmp_bound = rewrite(cmp_bound);
               // Should be comparing two constant values which should rewrite
               // to a constant. If a step failed, we assume that this is not
               // the new best bound. We might not be comparing constant
@@ -611,7 +609,7 @@ bool ArithInstantiator::processAssertions(CegInstantiator* ci,
         val = nm->mkNode(MULT,
                          nm->mkNode(PLUS, vals[0], vals[1]),
                          nm->mkConst(Rational(1) / Rational(2)));
-        val = Rewriter::rewrite(val);
+        val = rewrite(val);
       }
     }
     else
@@ -619,12 +617,12 @@ bool ArithInstantiator::processAssertions(CegInstantiator* ci,
       if (!vals[0].isNull())
       {
         val = nm->mkNode(PLUS, vals[0], d_one);
-        val = Rewriter::rewrite(val);
+        val = rewrite(val);
       }
       else if (!vals[1].isNull())
       {
         val = nm->mkNode(MINUS, vals[1], d_one);
-        val = Rewriter::rewrite(val);
+        val = rewrite(val);
       }
     }
     Trace("cegqi-arith-bound") << "Midpoint value : " << val << std::endl;
@@ -718,7 +716,7 @@ bool ArithInstantiator::postProcessInstantiationForVariable(
   // then we are successful
   Node eq_rhs = sf.d_subs[index];
   Node eq = eq_lhs.eqNode(eq_rhs);
-  eq = Rewriter::rewrite(eq);
+  eq = rewrite(eq);
   Trace("cegqi-arith-debug") << "...equality is " << eq << std::endl;
   std::map<Node, Node> msum;
   if (!ArithMSum::getMonomialSumLit(eq, msum))
@@ -823,7 +821,7 @@ CegTermType ArithInstantiator::solve_arith(CegInstantiator* ci,
                   MULT,
                   nm->mkConst(Rational(-1) / itv->second.getConst<Rational>()),
                   vts_coeff[t]);
-              vts_coeff[t] = Rewriter::rewrite(vts_coeff[t]);
+              vts_coeff[t] = rewrite(vts_coeff[t]);
             }
             else if (itv->second.getConst<Rational>().sgn() == 1)
             {
@@ -894,8 +892,7 @@ CegTermType ArithInstantiator::solve_arith(CegInstantiator* ci,
         }
         else
         {
-          msum[it->first] =
-              Rewriter::rewrite(nm->mkNode(MULT, it->second, rcoeff));
+          msum[it->first] = rewrite(nm->mkNode(MULT, it->second, rcoeff));
         }
       }
       if (!it->first.isNull() && !it->first.getType().isInteger())
@@ -910,7 +907,7 @@ CegTermType ArithInstantiator::solve_arith(CegInstantiator* ci,
     // multiply inf
     if (!vts_coeff[0].isNull())
     {
-      vts_coeff[0] = Rewriter::rewrite(nm->mkNode(MULT, rcoeff, vts_coeff[0]));
+      vts_coeff[0] = rewrite(nm->mkNode(MULT, rcoeff, vts_coeff[0]));
     }
     Node realPart = real_part.empty()
                         ? d_zero
@@ -931,7 +928,7 @@ CegTermType ArithInstantiator::solve_arith(CegInstantiator* ci,
       int ires_use =
           (msum[pv].isNull() || msum[pv].getConst<Rational>().sgn() == 1) ? 1
                                                                           : -1;
-      val = Rewriter::rewrite(
+      val = rewrite(
           nm->mkNode(ires_use == -1 ? PLUS : MINUS,
                      nm->mkNode(ires_use == -1 ? MINUS : PLUS, val, realPart),
                      nm->mkNode(TO_INTEGER, realPart)));
@@ -982,7 +979,7 @@ Node ArithInstantiator::getModelBasedProjectionValue(CegInstantiator* ci,
   {
     Assert(c.getType().isInteger());
     ceValue = nm->mkNode(MULT, ceValue, c);
-    ceValue = Rewriter::rewrite(ceValue);
+    ceValue = rewrite(ceValue);
     if (new_theta.isNull())
     {
       new_theta = c;
@@ -990,7 +987,7 @@ Node ArithInstantiator::getModelBasedProjectionValue(CegInstantiator* ci,
     else
     {
       new_theta = nm->mkNode(MULT, new_theta, c);
-      new_theta = Rewriter::rewrite(new_theta);
+      new_theta = rewrite(new_theta);
     }
     Trace("cegqi-arith-bound2") << "...c*e = " << ceValue << std::endl;
     Trace("cegqi-arith-bound2") << "...theta = " << new_theta << std::endl;
@@ -1006,31 +1003,31 @@ Node ArithInstantiator::getModelBasedProjectionValue(CegInstantiator* ci,
     {
       rho = nm->mkNode(MINUS, mt, ceValue);
     }
-    rho = Rewriter::rewrite(rho);
+    rho = rewrite(rho);
     Trace("cegqi-arith-bound2")
         << "...rho = " << me << " - " << mt << " = " << rho << std::endl;
     Trace("cegqi-arith-bound2")
         << "..." << rho << " mod " << new_theta << " = ";
     rho = nm->mkNode(INTS_MODULUS_TOTAL, rho, new_theta);
-    rho = Rewriter::rewrite(rho);
+    rho = rewrite(rho);
     Trace("cegqi-arith-bound2") << rho << std::endl;
     Kind rk = isLower ? PLUS : MINUS;
     val = nm->mkNode(rk, val, rho);
-    val = Rewriter::rewrite(val);
+    val = rewrite(val);
     Trace("cegqi-arith-bound2") << "(after rho) : " << val << std::endl;
   }
   if (!inf_coeff.isNull())
   {
     Assert(!d_vts_sym[0].isNull());
     val = nm->mkNode(PLUS, val, nm->mkNode(MULT, inf_coeff, d_vts_sym[0]));
-    val = Rewriter::rewrite(val);
+    val = rewrite(val);
   }
   if (!delta_coeff.isNull())
   {
     // create delta here if necessary
     val = nm->mkNode(
         PLUS, val, nm->mkNode(MULT, delta_coeff, d_vtc->getVtsDelta()));
-    val = Rewriter::rewrite(val);
+    val = rewrite(val);
   }
   return val;
 }

diff --git a/src/theory/quantifiers/cegqi/ceg_arith_instantiator.h b/src/theory/quantifiers/cegqi/ceg_arith_instantiator.h
index 6d65ae16c12584174205c647fd8b07a6e10509e2..e102b834e2904ddbcee964e204818cc9b39e1763 100644 (file)
--- a/src/theory/quantifiers/cegqi/ceg_arith_instantiator.h
+++ b/src/theory/quantifiers/cegqi/ceg_arith_instantiator.h
@@ -44,7 +44,7 @@ namespace quantifiers {
 class ArithInstantiator : public Instantiator
 {
  public:
-  ArithInstantiator(TypeNode tn, VtsTermCache* vtc);
+  ArithInstantiator(Env& env, TypeNode tn, VtsTermCache* vtc);
   virtual ~ArithInstantiator() {}
   /** reset */
   void reset(CegInstantiator* ci,

diff --git a/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp
index 9ffb31df3a2ef8b777e746c7e555b2a0b6d55527..5b5c1cc8622e74dab8bd0118bedccda8a9f8e1d8 100644 (file)
--- a/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp
+++ b/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp
@@ -54,8 +54,8 @@ class CegInstantiatorBvInverterQuery : public BvInverterQuery
   CegInstantiator* d_ci;
 };
 
-BvInstantiator::BvInstantiator(TypeNode tn, BvInverter* inv)
-    : Instantiator(tn), d_inverter(inv), d_inst_id_counter(0)
+BvInstantiator::BvInstantiator(Env& env, TypeNode tn, BvInverter* inv)
+    : Instantiator(env, tn), d_inverter(inv), d_inst_id_counter(0)
 {
   // The inverter utility d_inverter is global to all BvInstantiator classes.
   // This must be global since we need to:

diff --git a/src/theory/quantifiers/cegqi/ceg_bv_instantiator.h b/src/theory/quantifiers/cegqi/ceg_bv_instantiator.h
index cbc73dc2c8ac6ec9886c92f5229fe98e682d1d5e..0c2cb05df95b81149f1ee118636ee46c3e8ca802 100644 (file)
--- a/src/theory/quantifiers/cegqi/ceg_bv_instantiator.h
+++ b/src/theory/quantifiers/cegqi/ceg_bv_instantiator.h
@@ -39,7 +39,7 @@ namespace quantifiers {
 class BvInstantiator : public Instantiator
 {
  public:
-  BvInstantiator(TypeNode tn, BvInverter* inv);
+  BvInstantiator(Env& env, TypeNode tn, BvInverter* inv);
   ~BvInstantiator() override;
   /** reset */
   void reset(CegInstantiator* ci,

diff --git a/src/theory/quantifiers/cegqi/ceg_dt_instantiator.h b/src/theory/quantifiers/cegqi/ceg_dt_instantiator.h
index 72746a39b91e96230f4cff893beb963ddd3c95b5..9a99c47431adee7dbcc46a9be7579f1fc4c9f67c 100644 (file)
--- a/src/theory/quantifiers/cegqi/ceg_dt_instantiator.h
+++ b/src/theory/quantifiers/cegqi/ceg_dt_instantiator.h
@@ -33,7 +33,7 @@ namespace quantifiers {
 class DtInstantiator : public Instantiator
 {
  public:
-  DtInstantiator(TypeNode tn) : Instantiator(tn) {}
+  DtInstantiator(Env& env, TypeNode tn) : Instantiator(env, tn) {}
   virtual ~DtInstantiator() {}
   /** reset */
   void reset(CegInstantiator* ci,

diff --git a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
index 4b06589b300303302910a4ff9445313183c373c0..d61dd2bd2aea01772ef88909de0df5f31398d1ee 100644 (file)
--- a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
+++ b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
@@ -137,8 +137,9 @@ void TermProperties::composeProperty(TermProperties& p)
   }
   else
   {
-    d_coeff = NodeManager::currentNM()->mkNode(MULT, d_coeff, p.d_coeff);
-    d_coeff = Rewriter::rewrite(d_coeff);
+    NodeManager* nm = NodeManager::currentNM();
+    d_coeff = nm->mkConst(Rational(d_coeff.getConst<Rational>()
+                                   * p.d_coeff.getConst<Rational>()));
   }
 }
 
@@ -161,9 +162,11 @@ void SolvedForm::push_back(Node pv, Node n, TermProperties& pv_prop)
   }
   else
   {
-    new_theta =
-        NodeManager::currentNM()->mkNode(MULT, new_theta, pv_prop.d_coeff);
-    new_theta = Rewriter::rewrite(new_theta);
+    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>()
+                                     * pv_prop.d_coeff.getConst<Rational>()));
   }
   d_theta.push_back(new_theta);
 }
@@ -182,11 +185,13 @@ void SolvedForm::pop_back(Node pv, Node n, TermProperties& pv_prop)
   d_theta.pop_back();
 }
 
-CegInstantiator::CegInstantiator(Node q,
+CegInstantiator::CegInstantiator(Env& env,
+                                 Node q,
                                  QuantifiersState& qs,
                                  TermRegistry& tr,
                                  InstStrategyCegqi* parent)
-    : d_quant(q),
+    : EnvObj(env),
+      d_quant(q),
       d_qstate(qs),
       d_treg(tr),
       d_parent(parent),
@@ -476,16 +481,16 @@ void CegInstantiator::activateInstantiationVariable(Node v, unsigned index)
     TypeNode tn = v.getType();
     Instantiator * vinst;
     if( tn.isReal() ){
-      vinst = new ArithInstantiator(tn, d_parent->getVtsTermCache());
+      vinst = new ArithInstantiator(d_env, tn, d_parent->getVtsTermCache());
     }else if( tn.isDatatype() ){
-      vinst = new DtInstantiator(tn);
+      vinst = new DtInstantiator(d_env, tn);
     }else if( tn.isBitVector() ){
-      vinst = new BvInstantiator(tn, d_parent->getBvInverter());
+      vinst = new BvInstantiator(d_env, tn, d_parent->getBvInverter());
     }else if( tn.isBoolean() ){
-      vinst = new ModelValueInstantiator(tn);
+      vinst = new ModelValueInstantiator(d_env, tn);
     }else{
       //default
-      vinst = new Instantiator(tn);
+      vinst = new Instantiator(d_env, tn);
     }
     d_instantiator[v] = vinst;
   }
@@ -1120,7 +1125,7 @@ bool CegInstantiator::canApplyBasicSubstitution( Node n, std::vector< Node >& no
 
 Node CegInstantiator::applySubstitution( TypeNode tn, Node n, std::vector< Node >& vars, std::vector< Node >& subs, std::vector< TermProperties >& prop, 
                                          std::vector< Node >& non_basic, TermProperties& pv_prop, bool try_coeff ) {
-  n = Rewriter::rewrite(n);
+  n = rewrite(n);
   computeProgVars( n );
   bool is_basic = canApplyBasicSubstitution( n, non_basic );
   if( Trace.isOn("sygus-si-apply-subs-debug") ){
@@ -1144,7 +1149,7 @@ Node CegInstantiator::applySubstitution( TypeNode tn, Node n, std::vector< Node
           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>() ) );
           nn = NodeManager::currentNM()->mkNode( kind::TO_INTEGER, nn );
-          nn =  Rewriter::rewrite( nn );
+          nn = rewrite(nn);
           nsubs.push_back( nn );
         }else{
           nsubs.push_back( subs[i] );
@@ -1183,13 +1188,15 @@ Node CegInstantiator::applySubstitution( TypeNode tn, Node n, std::vector< Node
         }
         //make sum with normalized coefficient
         if( !pv_prop.d_coeff.isNull() ){
-          pv_prop.d_coeff = Rewriter::rewrite( pv_prop.d_coeff );
+          pv_prop.d_coeff = rewrite(pv_prop.d_coeff);
           Trace("sygus-si-apply-subs-debug") << "Combined coeff : " << pv_prop.d_coeff << std::endl;
           std::vector< Node > children;
           for( std::map< Node, Node >::iterator it = msum.begin(); it != msum.end(); ++it ){
             Node c_coeff;
             if( !msum_coeff[it->first].isNull() ){
-              c_coeff = Rewriter::rewrite( NodeManager::currentNM()->mkConst( pv_prop.d_coeff.getConst<Rational>() / msum_coeff[it->first].getConst<Rational>() ) );
+              c_coeff = rewrite(NodeManager::currentNM()->mkConst(
+                  pv_prop.d_coeff.getConst<Rational>()
+                  / msum_coeff[it->first].getConst<Rational>()));
             }else{
               c_coeff = pv_prop.d_coeff;
             }
@@ -1207,7 +1214,7 @@ Node CegInstantiator::applySubstitution( TypeNode tn, Node n, std::vector< Node
             Trace("sygus-si-apply-subs-debug") << "Add child : " << c << std::endl;
           }
           Node nretc = children.size()==1 ? children[0] : NodeManager::currentNM()->mkNode( PLUS, children );
-          nretc = Rewriter::rewrite( nretc );
+          nretc = rewrite(nretc);
           //ensure that nret does not contain vars
           if (!expr::hasSubterm(nretc, vars))
           {
@@ -1226,7 +1233,7 @@ Node CegInstantiator::applySubstitution( TypeNode tn, Node n, std::vector< Node
     }
   }
   if( n!=nret && !nret.isNull() ){
-    nret = Rewriter::rewrite( nret );
+    nret = rewrite(nret);
   }
   return nret;
 }
@@ -1252,7 +1259,7 @@ Node CegInstantiator::applySubstitutionToLiteral( Node lit, std::vector< Node >&
         atom_rhs = atom[1];
       }else{
         atom_lhs = nm->mkNode(MINUS, atom[0], atom[1]);
-        atom_lhs = Rewriter::rewrite( atom_lhs );
+        atom_lhs = rewrite(atom_lhs);
         atom_rhs = nm->mkConst(Rational(0));
       }
       //must be an eligible term
@@ -1269,7 +1276,7 @@ Node CegInstantiator::applySubstitutionToLiteral( Node lit, std::vector< Node >&
         if( !atom_lhs.isNull() ){
           if( !atom_lhs_prop.d_coeff.isNull() ){
             atom_rhs = nm->mkNode(MULT, atom_lhs_prop.d_coeff, atom_rhs);
-            atom_rhs = Rewriter::rewrite(atom_rhs);
+            atom_rhs = rewrite(atom_rhs);
           }
           lret = nm->mkNode(atom.getKind(), atom_lhs, atom_rhs);
           if( !pol ){
@@ -1282,7 +1289,7 @@ Node CegInstantiator::applySubstitutionToLiteral( Node lit, std::vector< Node >&
     }
   }
   if( lit!=lret && !lret.isNull() ){
-    lret = Rewriter::rewrite( lret );
+    lret = rewrite(lret);
   }
   return lret;
 }
@@ -1621,7 +1628,7 @@ void CegInstantiator::registerCounterexampleLemma(Node lem,
   }
 }
 
-Instantiator::Instantiator(TypeNode tn) : d_type(tn)
+Instantiator::Instantiator(Env& env, TypeNode tn) : EnvObj(env), d_type(tn)
 {
   d_closed_enum_type = tn.isClosedEnumerable();
 }

diff --git a/src/theory/quantifiers/cegqi/ceg_instantiator.h b/src/theory/quantifiers/cegqi/ceg_instantiator.h
index 2c228777d23266c7dd3d3f80ed5a88c351c6a636..600f50f42fd7710d16e4363e85467b8864e2bd66 100644 (file)
--- a/src/theory/quantifiers/cegqi/ceg_instantiator.h
+++ b/src/theory/quantifiers/cegqi/ceg_instantiator.h
@@ -21,6 +21,7 @@
 #include <vector>
 
 #include "expr/node.h"
+#include "smt/env_obj.h"
 #include "theory/inference_id.h"
 #include "util/statistics_stats.h"
 
@@ -86,11 +87,12 @@ class TermProperties {
   // get cache node
   // we consider terms + TermProperties that are unique up to their cache node
   // (see constructInstantiationInc)
-  virtual Node getCacheNode() const { return d_coeff; }
-  // is non-basic 
-  virtual bool isBasic() const { return d_coeff.isNull(); }
-  // get modified term 
-  virtual Node getModifiedTerm( Node pv ) const {
+  Node getCacheNode() const { return d_coeff; }
+  // is non-basic
+  bool isBasic() const { return d_coeff.isNull(); }
+  // get modified term
+  Node getModifiedTerm(Node pv) const
+  {
     if( !d_coeff.isNull() ){
       return NodeManager::currentNM()->mkNode( kind::MULT, d_coeff, pv );
     }else{
@@ -99,7 +101,7 @@ class TermProperties {
   }
   // compose property, should be such that: 
   //   p.getModifiedTerm( this.getModifiedTerm( x ) ) = this_updated.getModifiedTerm( x )
-  virtual void composeProperty(TermProperties& p);
+  void composeProperty(TermProperties& p);
 };
 
 /** Solved form
@@ -203,13 +205,15 @@ std::ostream& operator<<(std::ostream& os, CegHandledStatus status);
  * For details on counterexample-guided quantifier instantiation
  * (for linear arithmetic), see Reynolds/King/Kuncak FMSD 2017.
  */
-class CegInstantiator {
+class CegInstantiator : protected EnvObj
+{
  public:
   /**
    * The instantiator will be constructing instantiations for quantified formula
    * q, parent is the owner of this object.
    */
-  CegInstantiator(Node q,
+  CegInstantiator(Env& env,
+                  Node q,
                   QuantifiersState& qs,
                   TermRegistry& tr,
                   InstStrategyCegqi* parent);
@@ -575,21 +579,22 @@ class CegInstantiator {
  * In these calls, the Instantiator in turn makes calls to methods in
  * CegInstanatior (primarily constructInstantiationInc).
  */
-class Instantiator {
-public:
- Instantiator(TypeNode tn);
- virtual ~Instantiator() {}
- /** reset
-  * This is called once, prior to any of the below methods are called.
-  * This function sets up any initial information necessary for constructing
-  * instantiations for pv based on the current context.
-  */
- virtual void reset(CegInstantiator* ci,
-                    SolvedForm& sf,
-                    Node pv,
-                    CegInstEffort effort)
- {
- }
+class Instantiator : protected EnvObj
+{
+ public:
+  Instantiator(Env& env, TypeNode tn);
+  virtual ~Instantiator() {}
+  /** reset
+   * This is called once, prior to any of the below methods are called.
+   * This function sets up any initial information necessary for constructing
+   * instantiations for pv based on the current context.
+   */
+  virtual void reset(CegInstantiator* ci,
+                     SolvedForm& sf,
+                     Node pv,
+                     CegInstEffort effort)
+  {
+  }
 
   /** has process equal term
    *
@@ -782,7 +787,7 @@ public:
 
 class ModelValueInstantiator : public Instantiator {
 public:
- ModelValueInstantiator(TypeNode tn) : Instantiator(tn) {}
+ ModelValueInstantiator(Env& env, TypeNode tn) : Instantiator(env, tn) {}
  virtual ~ModelValueInstantiator() {}
  bool useModelValue(CegInstantiator* ci,
                     SolvedForm& sf,

diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
index 04fa1d2fe1b947b1afe5574bf5f7b6249796938c..e4a75cebb6141a1d950d8bf3cba9db2bf2c3c3b3 100644 (file)
--- a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
+++ b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
@@ -506,7 +506,7 @@ CegInstantiator * InstStrategyCegqi::getInstantiator( Node q ) {
   std::map<Node, std::unique_ptr<CegInstantiator>>::iterator it =
       d_cinst.find(q);
   if( it==d_cinst.end() ){
-    d_cinst[q].reset(new CegInstantiator(q, d_qstate, d_treg, this));
+    d_cinst[q].reset(new CegInstantiator(d_env, q, d_qstate, d_treg, this));
     return d_cinst[q].get();
   }
   return it->second.get();