From 67c43a7294442a7c660a26faf230cd983b21117d Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Tue, 4 May 2021 18:22:49 -0500
Subject: Move env into smt solver, theory engine, prop engine (#6486)

This is work towards eliminating singletons.

Also, TheoryModel should use the same substitution map as the preprocessor. This is work towards unifying these things, which will be done in a future PR.
---
 src/prop/prop_engine.cpp | 32 ++++++++++++++++++--------------
 src/prop/prop_engine.h   | 15 ++++++---------
 2 files changed, 24 insertions(+), 23 deletions(-)

(limited to 'src/prop')

diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index 5903c1606..dfd4c4528 100644
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -35,6 +35,7 @@
 #include "prop/sat_solver.h"
 #include "prop/sat_solver_factory.h"
 #include "prop/theory_proxy.h"
+#include "smt/env.h"
 #include "smt/smt_statistics_registry.h"
 #include "theory/output_channel.h"
 #include "theory/theory_engine.h"
@@ -65,15 +66,13 @@ public:
 };
 
 PropEngine::PropEngine(TheoryEngine* te,
-                       context::Context* satContext,
-                       context::UserContext* userContext,
-                       ResourceManager* rm,
+                       Env& env,
                        OutputManager& outMgr,
                        ProofNodeManager* pnm)
     : d_inCheckSat(false),
       d_theoryEngine(te),
-      d_context(satContext),
-      d_skdm(new SkolemDefManager(satContext, userContext)),
+      d_env(env),
+      d_skdm(new SkolemDefManager(d_env.getContext(), d_env.getUserContext())),
       d_theoryProxy(nullptr),
       d_satSolver(nullptr),
       d_pnm(pnm),
@@ -81,11 +80,13 @@ PropEngine::PropEngine(TheoryEngine* te,
       d_pfCnfStream(nullptr),
       d_ppm(nullptr),
       d_interrupted(false),
-      d_resourceManager(rm),
       d_outMgr(outMgr),
-      d_assumptions(userContext)
+      d_assumptions(d_env.getUserContext())
 {
   Debug("prop") << "Constructing the PropEngine" << std::endl;
+  context::Context* satContext = d_env.getContext();
+  context::UserContext* userContext = d_env.getUserContext();
+  ResourceManager* rm = d_env.getResourceManager();
 
   d_decisionEngine.reset(new DecisionEngine(satContext, userContext, rm));
   d_decisionEngine->init();  // enable appropriate strategies
@@ -112,9 +113,9 @@ PropEngine::PropEngine(TheoryEngine* te,
   d_theoryProxy->finishInit(d_cnfStream);
   // connect SAT solver
   d_satSolver->initialize(
-      d_context,
+      d_env.getContext(),
       d_theoryProxy,
-      userContext,
+      d_env.getUserContext(),
       options::unsatCoresMode() != options::UnsatCoresMode::ASSUMPTIONS
           ? pnm
           : nullptr);
@@ -395,13 +396,16 @@ Result PropEngine::checkSat() {
   }
 
   if( result == SAT_VALUE_UNKNOWN ) {
-
+    ResourceManager* rm = d_env.getResourceManager();
     Result::UnknownExplanation why = Result::INTERRUPTED;
-    if (d_resourceManager->outOfTime())
+    if (rm->outOfTime())
+    {
       why = Result::TIMEOUT;
-    if (d_resourceManager->outOfResources())
+    }
+    if (rm->outOfResources())
+    {
       why = Result::RESOURCEOUT;
-
+    }
     return Result(Result::SAT_UNKNOWN, why);
   }
 
@@ -576,7 +580,7 @@ void PropEngine::interrupt()
 
 void PropEngine::spendResource(Resource r)
 {
-  d_resourceManager->spendResource(r);
+  d_env.getResourceManager()->spendResource(r);
 }
 
 bool PropEngine::properExplanation(TNode node, TNode expl) const
diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h
index 6812a6549..631317c2d 100644
--- a/src/prop/prop_engine.h
+++ b/src/prop/prop_engine.h
@@ -29,6 +29,7 @@
 
 namespace cvc5 {
 
+class Env;
 class ResourceManager;
 class OutputManager;
 class ProofNodeManager;
@@ -56,10 +57,8 @@ class PropEngine
   /**
    * Create a PropEngine with a particular decision and theory engine.
    */
-  PropEngine(TheoryEngine*,
-             context::Context* satContext,
-             context::UserContext* userContext,
-             ResourceManager* rm,
+  PropEngine(TheoryEngine* te,
+             Env& env,
              OutputManager& outMgr,
              ProofNodeManager* pnm);
 
@@ -341,12 +340,12 @@ class PropEngine
   /** The theory engine we will be using */
   TheoryEngine* d_theoryEngine;
 
+  /** Reference to the environment */
+  Env& d_env;
+
   /** The decision engine we will be using */
   std::unique_ptr<decision::DecisionEngine> d_decisionEngine;
 
-  /** The context */
-  context::Context* d_context;
-
   /** The skolem definition manager */
   std::unique_ptr<SkolemDefManager> d_skdm;
 
@@ -372,8 +371,6 @@ class PropEngine
 
   /** Whether we were just interrupted (or not) */
   bool d_interrupted;
-  /** Pointer to resource manager for associated SmtEngine */
-  ResourceManager* d_resourceManager;
 
   /** Reference to the output manager of the smt engine */
   OutputManager& d_outMgr;
-- 
cgit v1.2.3