Eliminate calls to currentResourceManager (#7350)

The remaining calls to smt::currentResourceManager are in the bitblasters, which should probably update to Env. FYI @mpreiner .

diff --git a/src/smt/env.cpp b/src/smt/env.cpp
index 9334732fe10ed639a92271e5b890d91b9d077922..fd44c274c6f35ce62de9f892cbff7185cafc8b7c 100644 (file)
--- a/src/smt/env.cpp
+++ b/src/smt/env.cpp
@@ -63,6 +63,7 @@ Env::Env(NodeManager* nm, const Options* opts)
       new theory::Evaluator(nullptr, d_options.strings.stringsAlphaCard));
   d_statisticsRegistry->registerTimer("global::totalTime").start();
   d_resourceManager = std::make_unique<ResourceManager>(*d_statisticsRegistry, d_options);
+  d_rewriter->d_resourceManager = d_resourceManager.get();
 }
 
 Env::~Env() {}

diff --git a/src/theory/bv/bv_solver_bitblast.cpp b/src/theory/bv/bv_solver_bitblast.cpp
index a8ae3b117224d14e7c25420e241efeff867f33b4..0a9fc78873fc40a04dd4f378cb0852eaa7eab62e 100644 (file)
--- a/src/theory/bv/bv_solver_bitblast.cpp
+++ b/src/theory/bv/bv_solver_bitblast.cpp
@@ -342,7 +342,7 @@ void BVSolverBitblast::initSatSolver()
                                         d_bbRegistrar.get(),
                                         d_nullContext.get(),
                                         nullptr,
-                                        smt::currentResourceManager(),
+                                        d_env.getResourceManager(),
                                         prop::FormulaLitPolicy::INTERNAL,
                                         "theory::bv::BVSolverBitblast"));
 }

diff --git a/src/theory/rewriter.cpp b/src/theory/rewriter.cpp
index 234b3d142c186e1478c37ee529dcf01d01be5723..6cb3bf3ff2668b7b89707c8e0212eaaab12c2e3f 100644 (file)
--- a/src/theory/rewriter.cpp
+++ b/src/theory/rewriter.cpp
@@ -196,17 +196,11 @@ Node Rewriter::rewriteTo(theory::TheoryId theoryId,
   vector<RewriteStackElement> rewriteStack;
   rewriteStack.push_back(RewriteStackElement(node, theoryId));
 
-  ResourceManager* rm = NULL;
-  bool hasSlvEngine = smt::solverEngineInScope();
-  if (hasSlvEngine)
-  {
-    rm = smt::currentResourceManager();
-  }
   // Rewrite until the stack is empty
   for (;;){
-    if (hasSlvEngine)
+    if (d_resourceManager != nullptr)
     {
-      rm->spendResource(Resource::RewriteStep);
+      d_resourceManager->spendResource(Resource::RewriteStep);
     }
 
     // Get the top of the recursion stack

diff --git a/src/theory/rewriter.h b/src/theory/rewriter.h
index be11ff5de8939db0321175a7a44d38a72e6e78e4..f96062b6154057b3a28297130aaf3001332c905c 100644 (file)
--- a/src/theory/rewriter.h
+++ b/src/theory/rewriter.h
@@ -35,7 +35,7 @@ class Evaluator;
  * The main rewriter class.
  */
 class Rewriter {
-  friend class cvc5::Env;  // to initialize the evaluators of this class
+  friend class cvc5::Env;  // to set the resource manager
  public:
   Rewriter();
 
@@ -159,6 +159,9 @@ class Rewriter {
 
   void clearCachesInternal();
 
+  /** The resource manager, for tracking resource usage */
+  ResourceManager* d_resourceManager;
+
   /** Theory rewriters used by this rewriter instance */
   TheoryRewriter* d_theoryRewriters[theory::THEORY_LAST];
 

diff --git a/src/theory/rewriter_tables_template.h b/src/theory/rewriter_tables_template.h
index e86d748fd2d689ad7796752789a771f98429fef6..fd99b962536f0cee635c7022f20414132067a434 100644 (file)
--- a/src/theory/rewriter_tables_template.h
+++ b/src/theory/rewriter_tables_template.h
@@ -80,7 +80,7 @@ ${post_rewrite_set_cache}
   }
 }
 
-Rewriter::Rewriter() : d_tpg(nullptr) {}
+Rewriter::Rewriter() : d_resourceManager(nullptr), d_tpg(nullptr) {}
 
 void Rewriter::clearCachesInternal()
 {

diff --git a/src/theory/theory_inference_manager.cpp b/src/theory/theory_inference_manager.cpp
index 5fc94614779eae6d446dc1217a70a950720dd93c..1699e91ad3f21936795d71b78da7f8ab543af979 100644 (file)
--- a/src/theory/theory_inference_manager.cpp
+++ b/src/theory/theory_inference_manager.cpp
@@ -16,7 +16,6 @@
 #include "theory/theory_inference_manager.h"
 
 #include "smt/smt_statistics_registry.h"
-#include "smt/solver_engine_scope.h"
 #include "theory/output_channel.h"
 #include "theory/rewriter.h"
 #include "theory/theory.h"
@@ -125,7 +124,7 @@ void TheoryInferenceManager::conflict(TNode conf, InferenceId id)
 void TheoryInferenceManager::trustedConflict(TrustNode tconf, InferenceId id)
 {
   d_conflictIdStats << id;
-  smt::currentResourceManager()->spendResource(id);
+  resourceManager()->spendResource(id);
   Trace("im") << "(conflict " << id << " " << tconf.getProven() << ")"
               << std::endl;
   d_out.trustedConflict(tconf);
@@ -257,7 +256,7 @@ bool TheoryInferenceManager::trustedLemma(const TrustNode& tlem,
     }
   }
   d_lemmaIdStats << id;
-  smt::currentResourceManager()->spendResource(id);
+  resourceManager()->spendResource(id);
   Trace("im") << "(lemma " << id << " " << tlem.getProven() << ")" << std::endl;
   // shouldn't send trivially true or false lemmas
   Assert(!Rewriter::rewrite(tlem.getProven()).isConst());
@@ -380,7 +379,7 @@ bool TheoryInferenceManager::processInternalFact(TNode atom,
                                                  ProofGenerator* pg)
 {
   d_factIdStats << iid;
-  smt::currentResourceManager()->spendResource(iid);
+  resourceManager()->spendResource(iid);
   // make the node corresponding to the explanation
   Node expn = NodeManager::currentNM()->mkAnd(exp);
   Trace("im") << "(fact " << iid << " " << (pol ? Node(atom) : atom.notNode())