More uses of EnvObj (#7230)

9 files changed, 43 insertions, 38 deletions

diff --git a/src/smt/model_core_builder.cpp b/src/smt/model_core_builder.cpp
index 9e9eb5f23..9a9c56972 100644
--- a/src/smt/model_core_builder.cpp
+++ b/src/smt/model_core_builder.cpp
@@ -21,6 +21,8 @@ using namespace cvc5::kind;
 
 namespace cvc5 {
 
+ModelCoreBuilder::ModelCoreBuilder(Env& env) : EnvObj(env) {}
+
 bool ModelCoreBuilder::setModelCore(const std::vector<Node>& assertions,
                                     theory::TheoryModel* m,
                                     options::ModelCoresMode mode)
@@ -78,15 +80,14 @@ bool ModelCoreBuilder::setModelCore(const std::vector<Node>& assertions,
   std::vector<Node> coreVars;
   std::vector<Node> impliedVars;
   bool minimized = false;
+  theory::SubstitutionMinimize sm(d_env);
   if (mode == options::ModelCoresMode::NON_IMPLIED)
   {
-    minimized = theory::SubstitutionMinimize::findWithImplied(
-        formula, vars, subs, coreVars, impliedVars);
+    minimized = sm.findWithImplied(formula, vars, subs, coreVars, impliedVars);
   }
   else if (mode == options::ModelCoresMode::SIMPLE)
   {
-    minimized = theory::SubstitutionMinimize::find(
-        formula, truen, vars, subs, coreVars);
+    minimized = sm.find(formula, truen, vars, subs, coreVars);
   }
   else
   {
diff --git a/src/smt/model_core_builder.h b/src/smt/model_core_builder.h
index aab4fab5e..8a0ca5c8a 100644
--- a/src/smt/model_core_builder.h
+++ b/src/smt/model_core_builder.h
@@ -22,6 +22,7 @@
 
 #include "expr/node.h"
 #include "options/smt_options.h"
+#include "smt/env_obj.h"
 #include "theory/theory_model.h"
 
 namespace cvc5 {
@@ -29,9 +30,10 @@ namespace cvc5 {
 /**
  * A utility for building model cores.
  */
-class ModelCoreBuilder
+class ModelCoreBuilder : protected EnvObj
 {
  public:
+  ModelCoreBuilder(Env& env);
   /** set model core
    *
    * This function updates model m so that it has information regarding its
@@ -55,9 +57,9 @@ class ModelCoreBuilder
    * If m is not a model for assertions, this method returns false and m is
    * left unchanged.
    */
-  static bool setModelCore(const std::vector<Node>& assertions,
-                           theory::TheoryModel* m,
-                           options::ModelCoresMode mode);
+  bool setModelCore(const std::vector<Node>& assertions,
+                    theory::TheoryModel* m,
+                    options::ModelCoresMode mode);
 }; /* class TheoryModelCoreBuilder */
 
 }  // namespace cvc5
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 28ad11f46..f447773ad 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1135,7 +1135,8 @@ bool SmtEngine::isModelCoreSymbol(Node n)
     // impact whether we are in "sat" mode
     std::vector<Node> asserts = getAssertionsInternal();
     d_pp->expandDefinitions(asserts);
-    ModelCoreBuilder::setModelCore(asserts, tm, opts.smt.modelCoresMode);
+    ModelCoreBuilder mcb(*d_env.get());
+    mcb.setModelCore(asserts, tm, opts.smt.modelCoresMode);
   }
   return tm->isModelCoreSymbol(n);
 }
diff --git a/src/theory/datatypes/sygus_extension.cpp b/src/theory/datatypes/sygus_extension.cpp
index d666cdac5..78ff93c1a 100644
--- a/src/theory/datatypes/sygus_extension.cpp
+++ b/src/theory/datatypes/sygus_extension.cpp
@@ -602,7 +602,7 @@ Node SygusExtension::getSimpleSymBreakPred(Node e,
     {
       Node szl = nm->mkNode(DT_SIZE, n);
       Node szr = nm->mkNode(DT_SIZE, utils::getInstCons(n, dt, tindex));
-      szr = Rewriter::rewrite(szr);
+      szr = rewrite(szr);
       sbp_conj.push_back(szl.eqNode(szr));
     }
     if (isVarAgnostic)
diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index 427e0251f..feb19b182 100644
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -327,7 +327,7 @@ void TheoryDatatypes::postCheck(Effort level)
                   if( options::dtBinarySplit() && consIndex!=-1 ){
                     Node test = utils::mkTester(n, consIndex, dt);
                     Trace("dt-split") << "*************Split for possible constructor " << dt[consIndex] << " for " << n << endl;
-                    test = Rewriter::rewrite( test );
+                    test = rewrite(test);
                     NodeBuilder nb(kind::OR);
                     nb << test << test.notNode();
                     Node lemma = nb;
@@ -1009,7 +1009,7 @@ void TheoryDatatypes::collapseSelector( Node s, Node c ) {
     }
     else
     {
-      rrs = Rewriter::rewrite(r);
+      rrs = rewrite(r);
     }
     if (s != rrs)
     {
@@ -1424,7 +1424,7 @@ Node TheoryDatatypes::getInstantiateCons(Node n, const DType& dt, int index)
   //add constructor to equivalence class
   Node k = getTermSkolemFor( n );
   Node n_ic = utils::getInstCons(k, dt, index);
-  n_ic = Rewriter::rewrite( n_ic );
+  n_ic = rewrite(n_ic);
   // it may be a new term, so we collect terms and add it to the equality engine
   collectTerms( n_ic );
   d_equalityEngine->addTerm(n_ic);
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index dfce485f2..e0863f953 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -622,7 +622,7 @@ void QuantifiersEngine::assertQuantifier( Node f, bool pol ){
     {
       if (Trace.isOn("quantifiers-sk-debug"))
       {
-        Node slem = Rewriter::rewrite(lem.getNode());
+        Node slem = rewrite(lem.getNode());
         Trace("quantifiers-sk-debug")
             << "Skolemize lemma : " << slem << std::endl;
       }
diff --git a/src/theory/sep/theory_sep.cpp b/src/theory/sep/theory_sep.cpp
index d28bae12a..dc72783c0 100644
--- a/src/theory/sep/theory_sep.cpp
+++ b/src/theory/sep/theory_sep.cpp
@@ -761,7 +761,7 @@ void TheorySep::postCheck(Effort level)
       }
       else
       {
-        inst = Rewriter::rewrite(inst);
+        inst = rewrite(inst);
         if (inst == (polarity ? d_true : d_false))
         {
           inst_success = false;
@@ -1768,7 +1768,7 @@ void TheorySep::mergePto( Node p1, Node p2 ) {
 
 void TheorySep::sendLemma( std::vector< Node >& ant, Node conc, InferenceId id, bool infer ) {
   Trace("sep-lemma-debug") << "Do rewrite on inference : " << conc << std::endl;
-  conc = Rewriter::rewrite( conc );
+  conc = rewrite(conc);
   Trace("sep-lemma-debug") << "Got : " << conc << std::endl;
   if( conc!=d_true ){
     if( infer && conc!=d_false ){
diff --git a/src/theory/subs_minimize.cpp b/src/theory/subs_minimize.cpp
index 2ec945963..56b7a2fed 100644
--- a/src/theory/subs_minimize.cpp
+++ b/src/theory/subs_minimize.cpp
@@ -27,7 +27,7 @@ using namespace cvc5::kind;
 namespace cvc5 {
 namespace theory {
 
-SubstitutionMinimize::SubstitutionMinimize() {}
+SubstitutionMinimize::SubstitutionMinimize(Env& env) : EnvObj(env) {}
 
 bool SubstitutionMinimize::find(Node t,
                                 Node target,
@@ -119,7 +119,7 @@ bool SubstitutionMinimize::findWithImplied(Node t,
       // try the current substitution
       Node tcs = tc.substitute(
           reqVars.begin(), reqVars.end(), reqSubs.begin(), reqSubs.end());
-      Node tcsr = Rewriter::rewrite(tcs);
+      Node tcsr = rewrite(tcs);
       std::vector<Node> tcsrConj;
       getConjuncts(tcsr, tcsrConj);
       for (const Node& tcc : tcsrConj)
@@ -246,7 +246,7 @@ bool SubstitutionMinimize::findInternal(Node n,
           nb << it->second;
         }
         ret = nb.constructNode();
-        ret = Rewriter::rewrite(ret);
+        ret = rewrite(ret);
       }
       value[cur] = ret;
     }
@@ -323,7 +323,7 @@ bool SubstitutionMinimize::findInternal(Node n,
               // i to visit, and update curr below.
               if (scurr != curr)
               {
-                curr = Rewriter::rewrite(scurr);
+                curr = rewrite(scurr);
                 visit.push_back(cur[i]);
               }
             }
diff --git a/src/theory/subs_minimize.h b/src/theory/subs_minimize.h
index c78467508..571f629dd 100644
--- a/src/theory/subs_minimize.h
+++ b/src/theory/subs_minimize.h
@@ -21,6 +21,7 @@
 #include <vector>
 
 #include "expr/node.h"
+#include "smt/env_obj.h"
 
 namespace cvc5 {
 namespace theory {
@@ -30,10 +31,10 @@ namespace theory {
  * This class is used for finding a minimal substitution under which an
  * evaluation holds.
  */
-class SubstitutionMinimize
+class SubstitutionMinimize : protected EnvObj
 {
  public:
-  SubstitutionMinimize();
+  SubstitutionMinimize(Env& env);
   ~SubstitutionMinimize() {}
   /** find
    *
@@ -45,11 +46,11 @@ class SubstitutionMinimize
    * If t { vars -> subs } does not rewrite to target, this method returns
    * false.
    */
-  static bool find(Node t,
-                   Node target,
-                   const std::vector<Node>& vars,
-                   const std::vector<Node>& subs,
-                   std::vector<Node>& reqVars);
+  bool find(Node t,
+            Node target,
+            const std::vector<Node>& vars,
+            const std::vector<Node>& subs,
+            std::vector<Node>& reqVars);
   /** find with implied
    *
    * This method should be called on a formula t.
@@ -73,26 +74,26 @@ class SubstitutionMinimize
    * to appear in reqVars, whereas those later in the vars are more likely to
    * appear in impliedVars.
    */
-  static bool findWithImplied(Node t,
-                              const std::vector<Node>& vars,
-                              const std::vector<Node>& subs,
-                              std::vector<Node>& reqVars,
-                              std::vector<Node>& impliedVars);
+  bool findWithImplied(Node t,
+                       const std::vector<Node>& vars,
+                       const std::vector<Node>& subs,
+                       std::vector<Node>& reqVars,
+                       std::vector<Node>& impliedVars);
 
  private:
   /** Common helper function for the above functions. */
-  static bool findInternal(Node t,
-                           Node target,
-                           const std::vector<Node>& vars,
-                           const std::vector<Node>& subs,
-                           std::vector<Node>& reqVars);
+  bool findInternal(Node t,
+                    Node target,
+                    const std::vector<Node>& vars,
+                    const std::vector<Node>& subs,
+                    std::vector<Node>& reqVars);
   /** is singular arg
    *
    * Returns true if
    *   <k>( ... t_{arg-1}, n, t_{arg+1}...) = c
    * always holds for some constant c.
    */
-  static bool isSingularArg(Node n, Kind k, unsigned arg);
+  bool isSingularArg(Node n, Kind k, unsigned arg);
 };
 
 }  // namespace theory