Eliminate more static calls to Rewriter::rewrite (#7755)

diff --git a/src/theory/quantifiers/sygus/sygus_process_conj.cpp b/src/theory/quantifiers/sygus/sygus_process_conj.cpp
index f5cadc6076b94d2519639e41c919ec8e79e6c89b..d51cd9ab11083c73a45a03922cf1e9927cd21728 100644 (file)
--- a/src/theory/quantifiers/sygus/sygus_process_conj.cpp
+++ b/src/theory/quantifiers/sygus/sygus_process_conj.cpp
@@ -30,6 +30,8 @@ namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
+SynthConjectureProcessFun::SynthConjectureProcessFun(Env& env) : EnvObj(env) {}
+
 void SynthConjectureProcessFun::init(Node f)
 {
   d_synth_fun = f;
@@ -511,7 +513,7 @@ void SynthConjectureProcessFun::getIrrelevantArgs(
   }
 }
 
-SynthConjectureProcess::SynthConjectureProcess() {}
+SynthConjectureProcess::SynthConjectureProcess(Env& env) : EnvObj(env) {}
 SynthConjectureProcess::~SynthConjectureProcess() {}
 Node SynthConjectureProcess::preSimplify(Node q)
 {
@@ -532,7 +534,9 @@ Node SynthConjectureProcess::postSimplify(Node q)
       Node f = q[0][i];
       if (f.getType().isFunction())
       {
-        d_sf_info[f].init(f);
+        std::pair<std::map<Node, SynthConjectureProcessFun>::iterator, bool>
+            it = d_sf_info.emplace(f, d_env);
+        it.first->second.init(f);
       }
     }
 

diff --git a/src/theory/quantifiers/sygus/sygus_process_conj.h b/src/theory/quantifiers/sygus/sygus_process_conj.h
index d751e4c9c5570189a939422babe606582f98fb4f..b0b87c65b29f5a58edfd73ee3641e609deeceac2 100644 (file)
--- a/src/theory/quantifiers/sygus/sygus_process_conj.h
+++ b/src/theory/quantifiers/sygus/sygus_process_conj.h
@@ -25,6 +25,7 @@
 
 #include "expr/node.h"
 #include "expr/type_node.h"
+#include "smt/env_obj.h"
 
 namespace cvc5 {
 namespace theory {
@@ -119,10 +120,10 @@ class SynthConjectureProcessArg
 * It maintains information about each of the function to
 * synthesize's arguments.
 */
-struct SynthConjectureProcessFun
+struct SynthConjectureProcessFun : protected EnvObj
 {
  public:
-  SynthConjectureProcessFun() {}
+  SynthConjectureProcessFun(Env& env);
   ~SynthConjectureProcessFun() {}
   /** initialize this class for function f */
   void init(Node f);
@@ -266,10 +267,10 @@ struct SynthConjectureProcessFun
  * sygus to SynthConjectureProcess::getSymmetryBreakingPredicate(...), which are
  * used for pruning search space based on conjecture-specific analysis.
  */
-class SynthConjectureProcess
+class SynthConjectureProcess : protected EnvObj
 {
  public:
-  SynthConjectureProcess();
+  SynthConjectureProcess(Env& env);
   ~SynthConjectureProcess();
   /** simplify the synthesis conjecture q
    * Returns a formula that is equivalent to q.

diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp
index e7d0ef58be1894fff226ce535b13f855a03b91ff..a90551a0fb9ac4920866d3d72fc330940fd546cd 100644 (file)
--- a/src/theory/quantifiers/sygus/synth_conjecture.cpp
+++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp
@@ -61,7 +61,7 @@ SynthConjecture::SynthConjecture(Env& env,
       d_hasSolution(false),
       d_ceg_si(new CegSingleInv(env, tr, s)),
       d_templInfer(new SygusTemplateInfer(env)),
-      d_ceg_proc(new SynthConjectureProcess),
+      d_ceg_proc(new SynthConjectureProcess(env)),
       d_ceg_gc(new CegGrammarConstructor(env, d_tds, this)),
       d_sygus_rconst(new SygusRepairConst(env, d_tds)),
       d_exampleInfer(new ExampleInfer(d_tds)),

diff --git a/src/theory/theory_model_builder.cpp b/src/theory/theory_model_builder.cpp
index bc63aef97d3d64329ec234b96bf157c8064d0d20..1e56bd6ba031c6892d2717f09f617e80a4232c01 100644 (file)
--- a/src/theory/theory_model_builder.cpp
+++ b/src/theory/theory_model_builder.cpp
@@ -1278,7 +1278,8 @@ void TheoryEngineModelBuilder::assignFunction(TheoryModel* m, Node f)
   }
   std::stringstream ss;
   ss << "_arg_";
-  Node val = ufmt.getFunctionValue(ss.str().c_str(), condenseFuncValues);
+  Rewriter* r = condenseFuncValues ? d_env.getRewriter() : nullptr;
+  Node val = ufmt.getFunctionValue(ss.str(), r);
   m->assignFunctionDefinition(f, val);
   // ufmt.debugPrint( std::cout, m );
 }

diff --git a/src/theory/uf/cardinality_extension.cpp b/src/theory/uf/cardinality_extension.cpp
index f5f6ff565c19bdda87bdbcbfcbba6c0d98fff95a..6dcc0f72f70d325cbc1f878814110768a35d8c7a 100644 (file)
--- a/src/theory/uf/cardinality_extension.cpp
+++ b/src/theory/uf/cardinality_extension.cpp
@@ -465,11 +465,13 @@ std::string SortModel::CardinalityDecisionStrategy::identify() const
   return std::string("uf_card");
 }
 
-SortModel::SortModel(TypeNode tn,
+SortModel::SortModel(Env& env,
+                     TypeNode tn,
                      TheoryState& state,
                      TheoryInferenceManager& im,
                      CardinalityExtension* thss)
-    : d_type(tn),
+    : EnvObj(env),
+      d_type(tn),
       d_state(state),
       d_im(im),
       d_thss(thss),
@@ -1011,7 +1013,7 @@ int SortModel::addSplit(Region* r)
   if (!s.isNull() ){
     //add lemma to output channel
     Assert(s.getKind() == EQUAL);
-    Node ss = Rewriter::rewrite( s );
+    Node ss = rewrite(s);
     if( ss.getKind()!=EQUAL ){
       Node b_t = NodeManager::currentNM()->mkConst( true );
       Node b_f = NodeManager::currentNM()->mkConst( false );
@@ -1620,7 +1622,7 @@ void CardinalityExtension::preRegisterTerm(TNode n)
     if (tn.isSort())
     {
       Trace("uf-ss-register") << "Create sort model " << tn << "." << std::endl;
-      rm = new SortModel(tn, d_state, d_im, this);
+      rm = new SortModel(d_env, tn, d_state, d_im, this);
     }
     if (rm)
     {

diff --git a/src/theory/uf/cardinality_extension.h b/src/theory/uf/cardinality_extension.h
index 7a6d44ee99a3e31a58a2fffa56bef9c577848f04..822f13f2365f72efb95e76cb8ad72157bbf5c405 100644 (file)
--- a/src/theory/uf/cardinality_extension.h
+++ b/src/theory/uf/cardinality_extension.h
@@ -48,7 +48,7 @@ class CardinalityExtension : protected EnvObj
    * Information for incremental conflict/clique finding for a
    * particular sort.
    */
-  class SortModel
+  class SortModel : protected EnvObj
   {
    private:
     std::map< Node, std::vector< int > > d_totality_lems;
@@ -281,7 +281,8 @@ class CardinalityExtension : protected EnvObj
     void simpleCheckCardinality();
 
    public:
-    SortModel(TypeNode tn,
+    SortModel(Env& env,
+              TypeNode tn,
               TheoryState& state,
               TheoryInferenceManager& im,
               CardinalityExtension* thss);

diff --git a/src/theory/uf/proof_equality_engine.cpp b/src/theory/uf/proof_equality_engine.cpp
index 71688fc15da9b9937ba720ba2093a9fe5200b341..856dce011c82c42c44c627c4830a5fd2bb1bb5e8 100644 (file)
--- a/src/theory/uf/proof_equality_engine.cpp
+++ b/src/theory/uf/proof_equality_engine.cpp
@@ -31,7 +31,8 @@ namespace theory {
 namespace eq {
 
 ProofEqEngine::ProofEqEngine(Env& env, EqualityEngine& ee)
-    : EagerProofGenerator(env.getProofNodeManager(),
+    : EnvObj(env),
+      EagerProofGenerator(env.getProofNodeManager(),
                           env.getUserContext(),
                           "pfee::" + ee.identify()),
       d_ee(ee),
@@ -180,7 +181,7 @@ TrustNode ProofEqEngine::assertConflict(Node lit)
   // lit may not be equivalent to false, but should rewrite to false
   if (lit != d_false)
   {
-    Assert(Rewriter::rewrite(lit) == d_false)
+    Assert(rewrite(lit) == d_false)
         << "pfee::assertConflict: conflict literal is not rewritable to "
            "false";
     std::vector<Node> exp;

diff --git a/src/theory/uf/proof_equality_engine.h b/src/theory/uf/proof_equality_engine.h
index fc8520dd153156c3fb4e2ee65537dec2af89f92f..47bb2fe0da6df560e29e7715328d3915bdfe623b 100644 (file)
--- a/src/theory/uf/proof_equality_engine.h
+++ b/src/theory/uf/proof_equality_engine.h
@@ -27,6 +27,7 @@
 #include "proof/buffered_proof_generator.h"
 #include "proof/eager_proof_generator.h"
 #include "proof/lazy_proof.h"
+#include "smt/env_obj.h"
 
 namespace cvc5 {
 
@@ -80,7 +81,7 @@ class EqualityEngine;
  * - explain, for explaining why a literal is true in the current state.
  * Details on these methods can be found below.
  */
-class ProofEqEngine : public EagerProofGenerator
+class ProofEqEngine : protected EnvObj, public EagerProofGenerator
 {
   typedef context::CDHashSet<Node> NodeSet;
   typedef context::CDHashMap<Node, std::shared_ptr<ProofNode>> NodeProofMap;

diff --git a/src/theory/uf/theory_uf_model.cpp b/src/theory/uf/theory_uf_model.cpp
index 861f12d648bad1a0f3a00b030feb7740f488d7c2..6d8d421bac47e7bf3fd0385ce1dd9c02399a263c 100644 (file)
--- a/src/theory/uf/theory_uf_model.cpp
+++ b/src/theory/uf/theory_uf_model.cpp
@@ -57,7 +57,11 @@ void UfModelTreeNode::setValue( TheoryModel* m, Node n, Node v, std::vector< int
   }
 }
 
-Node UfModelTreeNode::getFunctionValue(std::vector<Node>& args, int index, Node argDefaultValue, bool simplify) {
+Node UfModelTreeNode::getFunctionValue(const std::vector<Node>& args,
+                                       int index,
+                                       Node argDefaultValue,
+                                       bool simplify)
+{
   if(!d_data.empty()) {
     Node defaultValue = argDefaultValue;
     if(d_data.find(Node::null()) != d_data.end()) {
@@ -222,16 +226,19 @@ void UfModelTreeNode::debugPrint( std::ostream& out, TheoryModel* m, std::vector
   }
 }
 
-Node UfModelTree::getFunctionValue( std::vector< Node >& args, bool simplify ){
-  Node body = d_tree.getFunctionValue( args, 0, Node::null(), simplify );
-  if(simplify) {
-    body = Rewriter::rewrite( body );
+Node UfModelTree::getFunctionValue(const std::vector<Node>& args, Rewriter* r)
+{
+  Node body = d_tree.getFunctionValue(args, 0, Node::null(), r != nullptr);
+  if (r != nullptr)
+  {
+    body = r->rewrite(body);
   }
   Node boundVarList = NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, args);
   return NodeManager::currentNM()->mkNode(kind::LAMBDA, boundVarList, body);
 }
 
-Node UfModelTree::getFunctionValue( const char* argPrefix, bool simplify ){
+Node UfModelTree::getFunctionValue(const std::string& argPrefix, Rewriter* r)
+{
   TypeNode type = d_op.getType();
   std::vector< Node > vars;
   for( size_t i=0; i<type.getNumChildren()-1; i++ ){
@@ -239,7 +246,7 @@ Node UfModelTree::getFunctionValue( const char* argPrefix, bool simplify ){
     ss << argPrefix << (i+1);
     vars.push_back( NodeManager::currentNM()->mkBoundVar( ss.str(), type[i] ) );
   }
-  return getFunctionValue( vars, simplify );
+  return getFunctionValue(vars, r);
 }
 
 }  // namespace uf

diff --git a/src/theory/uf/theory_uf_model.h b/src/theory/uf/theory_uf_model.h
index f386c2f99a81e670eacebddf35cbd2fef9a789ae..e4235623e68649418faefa4a39998ad24f7ca260 100644 (file)
--- a/src/theory/uf/theory_uf_model.h
+++ b/src/theory/uf/theory_uf_model.h
@@ -26,6 +26,7 @@ namespace cvc5 {
 namespace theory {
 
 class TheoryModel;
+class Rewriter;
 
 namespace uf {
 
@@ -45,7 +46,10 @@ public:
   /** setValue function */
   void setValue( TheoryModel* m, Node n, Node v, std::vector< int >& indexOrder, bool ground, int argIndex );
   /** getFunctionValue */
-  Node getFunctionValue( std::vector< Node >& args, int index, Node argDefaultValue, bool simplify = true );
+  Node getFunctionValue(const std::vector<Node>& args,
+                        int index,
+                        Node argDefaultValue,
+                        bool simplify = true);
   /** update function */
   void update( TheoryModel* m );
   /** simplify function */
@@ -92,11 +96,12 @@ public:
     d_tree.setValue( m, Node::null(), v, d_index_order, false, 0 );
   }
   /** getFunctionValue
-    *   Returns a representation of this function.
-    */
-  Node getFunctionValue( std::vector< Node >& args, bool simplify = true );
+   * Returns a representation of this function. The body of the function is
+   * rewritten if r is non-null.
+   */
+  Node getFunctionValue(const std::vector<Node>& args, Rewriter* r);
   /** getFunctionValue for args with set prefix */
-  Node getFunctionValue( const char* argPrefix, bool simplify = true );
+  Node getFunctionValue(const std::string& argPrefix, Rewriter* r);
   /** update
     *   This will update all values in the tree to be representatives in m.
     */