From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Tue, 12 Oct 2021 21:09:12 +0000 (-0500)
Subject: Eliminate calls to currentResourceManager (#7350)
X-Git-Tag: cvc5-1.0.0~1074
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=afd08bf3024c1f4c0d2fa8bcfc3a2cccab6f44ad;p=cvc5.git

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 9334732fe..fd44c274c 100644
--- 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 a8ae3b117..0a9fc7887 100644
--- 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 234b3d142..6cb3bf3ff 100644
--- 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 be11ff5de..f96062b61 100644
--- 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 e86d748fd..fd99b9625 100644
--- 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 5fc946147..1699e91ad 100644
--- 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())