Make decision engine use env (#7300)

diff --git a/src/decision/decision_engine.cpp b/src/decision/decision_engine.cpp
index 5b65951a671d0ad2500376af8bd95220c3722c8f..3011ad6ec4ebf3f4e1703b60712cd87b1e22c253 100644 (file)
--- a/src/decision/decision_engine.cpp
+++ b/src/decision/decision_engine.cpp
@@ -17,16 +17,14 @@
 #include "decision/decision_engine_old.h"
 #include "options/decision_options.h"
 #include "prop/sat_solver.h"
+#include "smt/env.h"
 #include "util/resource_manager.h"
 
 namespace cvc5 {
 namespace decision {
 
-DecisionEngine::DecisionEngine(context::Context* c, ResourceManager* rm)
-    : d_context(c),
-      d_resourceManager(rm),
-      d_cnfStream(nullptr),
-      d_satSolver(nullptr)
+DecisionEngine::DecisionEngine(Env& env)
+    : EnvObj(env), d_cnfStream(nullptr), d_satSolver(nullptr)
 {
 }
 
@@ -38,15 +36,11 @@ void DecisionEngine::finishInit(CDCLTSatSolverInterface* ss, CnfStream* cs)
 
 prop::SatLiteral DecisionEngine::getNext(bool& stopSearch)
 {
-  d_resourceManager->spendResource(Resource::DecisionStep);
+  resourceManager()->spendResource(Resource::DecisionStep);
   return getNextInternal(stopSearch);
 }
 
-DecisionEngineEmpty::DecisionEngineEmpty(context::Context* sc,
-                                         ResourceManager* rm)
-    : DecisionEngine(sc, rm)
-{
-}
+DecisionEngineEmpty::DecisionEngineEmpty(Env& env) : DecisionEngine(env) {}
 bool DecisionEngineEmpty::isDone() { return false; }
 void DecisionEngineEmpty::addAssertion(TNode assertion) {}
 void DecisionEngineEmpty::addSkolemDefinition(TNode lem, TNode skolem) {}

diff --git a/src/decision/decision_engine.h b/src/decision/decision_engine.h
index aa4c43e892695e532a3b1e3696b9dab52568fbfb..331d6eacaa2142627e9a0de5e1cbad9defd3ebce 100644 (file)
--- a/src/decision/decision_engine.h
+++ b/src/decision/decision_engine.h
@@ -22,16 +22,16 @@
 #include "prop/cnf_stream.h"
 #include "prop/sat_solver.h"
 #include "prop/sat_solver_types.h"
+#include "smt/env_obj.h"
 
 namespace cvc5 {
 namespace decision {
 
-class DecisionEngine
+class DecisionEngine : protected EnvObj
 {
  public:
   /** Constructor */
-  DecisionEngine(context::Context* sc,
-                 ResourceManager* rm);
+  DecisionEngine(Env& env);
   virtual ~DecisionEngine() {}
 
   /** Finish initialize */
@@ -86,7 +86,7 @@ class DecisionEngine
 class DecisionEngineEmpty : public DecisionEngine
 {
  public:
-  DecisionEngineEmpty(context::Context* sc, ResourceManager* rm);
+  DecisionEngineEmpty(Env& env);
   bool isDone() override;
   void addAssertion(TNode assertion) override;
   void addSkolemDefinition(TNode lem, TNode skolem) override;

diff --git a/src/decision/decision_engine_old.cpp b/src/decision/decision_engine_old.cpp
index 6bfba35ee64831931445d9e739e0e583b261f797..c61069cae494d7f97b1c349229be7f66fec17f8f 100644 (file)
--- a/src/decision/decision_engine_old.cpp
+++ b/src/decision/decision_engine_old.cpp
@@ -25,11 +25,9 @@ using namespace std;
 
 namespace cvc5 {
 
-DecisionEngineOld::DecisionEngineOld(context::Context* sc,
-                                     context::UserContext* uc,
-                                     ResourceManager* rm)
-    : DecisionEngine(sc, rm),
-      d_result(sc, SAT_VALUE_UNKNOWN),
+DecisionEngineOld::DecisionEngineOld(Env& env)
+    : DecisionEngine(env),
+      d_result(context(), SAT_VALUE_UNKNOWN),
       d_engineState(0),
       d_enabledITEStrategy(nullptr),
       d_decisionStopOnly(options::decisionMode()
@@ -47,8 +45,7 @@ DecisionEngineOld::DecisionEngineOld(context::Context* sc,
 
   if (options::decisionMode() == options::DecisionMode::JUSTIFICATION)
   {
-    d_enabledITEStrategy.reset(
-        new decision::JustificationHeuristic(this, uc, sc));
+    d_enabledITEStrategy.reset(new decision::JustificationHeuristic(env, this));
   }
 }
 

diff --git a/src/decision/decision_engine_old.h b/src/decision/decision_engine_old.h
index 93f58114340cd9f0fba58b2e8100c39c44a376ce..f1a340ca07949d6e5e01f5b1e6ed152d06fd5975 100644 (file)
--- a/src/decision/decision_engine_old.h
+++ b/src/decision/decision_engine_old.h
@@ -39,9 +39,7 @@ class DecisionEngineOld : public decision::DecisionEngine
   // Necessary functions
 
   /** Constructor */
-  DecisionEngineOld(context::Context* sc,
-                    context::UserContext* uc,
-                    ResourceManager* rm);
+  DecisionEngineOld(Env& env);
 
   /** Destructor, currently does nothing */
   ~DecisionEngineOld()

diff --git a/src/decision/decision_strategy.h b/src/decision/decision_strategy.h
index 87c463c29877d0902758c2c469f858eb7b4fb8da..e8f7683fd1dc9f4fbd565b9bc858a8bc2338c1b8 100644 (file)
--- a/src/decision/decision_strategy.h
+++ b/src/decision/decision_strategy.h
@@ -22,39 +22,35 @@
 
 #include "expr/node.h"
 #include "prop/sat_solver_types.h"
+#include "smt/env_obj.h"
 #include "smt/term_formula_removal.h"
 
 namespace cvc5 {
 
 class DecisionEngineOld;
 
-namespace context {
-  class Context;
-  }  // namespace context
-
 namespace decision {
-  
-class DecisionEngine;
-
-class DecisionStrategy {
-protected:
- DecisionEngineOld* d_decisionEngine;
 
-public:
- DecisionStrategy(DecisionEngineOld* de, context::Context* c)
-     : d_decisionEngine(de)
- {
+class DecisionStrategy : protected EnvObj
+{
+ public:
+  DecisionStrategy(Env& env, DecisionEngineOld* de)
+      : EnvObj(env), d_decisionEngine(de)
+  {
   }
 
   virtual ~DecisionStrategy() { }
 
   virtual prop::SatLiteral getNext(bool&) = 0;
+
+ protected:
+  DecisionEngineOld* d_decisionEngine;
 };/* class DecisionStrategy */
 
 class ITEDecisionStrategy : public DecisionStrategy {
 public:
- ITEDecisionStrategy(DecisionEngineOld* de, context::Context* c)
-     : DecisionStrategy(de, c)
+ ITEDecisionStrategy(Env& env, DecisionEngineOld* de)
+     : DecisionStrategy(env, de)
  {
   }
   /**

diff --git a/src/decision/justification_heuristic.cpp b/src/decision/justification_heuristic.cpp
index dcf8975bb3c39dd88dc416da29808f02e0a25ade..e04de9ce1c9b33d96b33112b258d5426f02d4ae3 100644 (file)
--- a/src/decision/justification_heuristic.cpp
+++ b/src/decision/justification_heuristic.cpp
@@ -34,28 +34,26 @@ using namespace cvc5::prop;
 namespace cvc5 {
 namespace decision {
 
-JustificationHeuristic::JustificationHeuristic(DecisionEngineOld* de,
-                                               context::UserContext* uc,
-                                               context::Context* c)
-    : ITEDecisionStrategy(de, c),
-      d_justified(c),
-      d_exploredThreshold(c),
-      d_prvsIndex(c, 0),
-      d_threshPrvsIndex(c, 0),
+JustificationHeuristic::JustificationHeuristic(Env& env, DecisionEngineOld* de)
+    : ITEDecisionStrategy(env, de),
+      d_justified(context()),
+      d_exploredThreshold(context()),
+      d_prvsIndex(context(), 0),
+      d_threshPrvsIndex(context(), 0),
       d_helpfulness(
           smtStatisticsRegistry().registerInt("decision::jh::helpfulness")),
       d_giveup(smtStatisticsRegistry().registerInt("decision::jh::giveup")),
       d_timestat(smtStatisticsRegistry().registerTimer("decision::jh::time")),
-      d_assertions(uc),
-      d_skolemAssertions(uc),
-      d_skolemCache(uc),
+      d_assertions(userContext()),
+      d_skolemAssertions(userContext()),
+      d_skolemCache(userContext()),
       d_visited(),
       d_visitedComputeSkolems(),
       d_curDecision(),
       d_curThreshold(0),
-      d_childCache(uc),
-      d_weightCache(uc),
-      d_startIndexCache(c)
+      d_childCache(userContext()),
+      d_weightCache(userContext()),
+      d_startIndexCache(context())
 {
   Trace("decision") << "Justification heuristic enabled" << std::endl;
 }

diff --git a/src/decision/justification_heuristic.h b/src/decision/justification_heuristic.h
index 8c713ab06abd96f456468e87fc8b0a6ce090f82f..303f1a63bca9180b7fb841b8a9b1a2fdbd3a3256 100644 (file)
--- a/src/decision/justification_heuristic.h
+++ b/src/decision/justification_heuristic.h
@@ -113,9 +113,7 @@ class JustificationHeuristic : public ITEDecisionStrategy {
   };
 
 public:
- JustificationHeuristic(DecisionEngineOld* de,
-                        context::UserContext* uc,
-                        context::Context* c);
+ JustificationHeuristic(Env& env, DecisionEngineOld* de);
 
  ~JustificationHeuristic();
 

diff --git a/src/decision/justification_strategy.cpp b/src/decision/justification_strategy.cpp
index 56d96b32f1b610adf37b1a282bfe52eac43c0978..d9e6b43e9d44be395190400cd2199fe0daf4dbd5 100644 (file)
--- a/src/decision/justification_strategy.cpp
+++ b/src/decision/justification_strategy.cpp
@@ -23,20 +23,19 @@ using namespace cvc5::prop;
 namespace cvc5 {
 namespace decision {
 
-JustificationStrategy::JustificationStrategy(context::Context* c,
-                                             context::UserContext* u,
-                                             prop::SkolemDefManager* skdm,
-                                             ResourceManager* rm)
-    : DecisionEngine(c, rm),
+JustificationStrategy::JustificationStrategy(Env& env,
+                                             prop::SkolemDefManager* skdm)
+    : DecisionEngine(env),
       d_skdm(skdm),
       d_assertions(
-          u,
-          c,
+          userContext(),
+          context(),
           options::jhRlvOrder()),  // assertions are user-context dependent
-      d_skolemAssertions(c, c),  // skolem assertions are SAT-context dependent
-      d_justified(c),
-      d_stack(c),
-      d_lastDecisionLit(c),
+      d_skolemAssertions(
+          context(), context()),  // skolem assertions are SAT-context dependent
+      d_justified(context()),
+      d_stack(context()),
+      d_lastDecisionLit(context()),
       d_currStatusDec(false),
       d_useRlvOrder(options::jhRlvOrder()),
       d_decisionStopOnly(options::decisionMode()

diff --git a/src/decision/justification_strategy.h b/src/decision/justification_strategy.h
index fc31805dd4c86ada61020c00253f47b29cd54a9b..26b456cf18dbc1ae375271285e736d71f7af4b9b 100644 (file)
--- a/src/decision/justification_strategy.h
+++ b/src/decision/justification_strategy.h
@@ -122,10 +122,7 @@ class JustificationStrategy : public DecisionEngine
 {
  public:
   /** Constructor */
-  JustificationStrategy(context::Context* c,
-                        context::UserContext* u,
-                        prop::SkolemDefManager* skdm,
-                        ResourceManager* rm);
+  JustificationStrategy(Env& env, prop::SkolemDefManager* skdm);
 
   /** Presolve, called at the beginning of each check-sat call */
   void presolve() override;

diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index 9060c318cb50edcecac74037ac296abe9bf45257..34dff2ba8815c6fee48397f4c4383314f6cc1b29 100644 (file)
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -79,7 +79,6 @@ PropEngine::PropEngine(TheoryEngine* te, Env& env)
       d_assumptions(d_env.getUserContext())
 {
   Debug("prop") << "Constructing the PropEngine" << std::endl;
-  context::Context* satContext = d_env.getContext();
   context::UserContext* userContext = d_env.getUserContext();
   ProofNodeManager* pnm = d_env.getProofNodeManager();
   ResourceManager* rm = d_env.getResourceManager();
@@ -88,17 +87,17 @@ PropEngine::PropEngine(TheoryEngine* te, Env& env)
   if (dmode == options::DecisionMode::JUSTIFICATION
       || dmode == options::DecisionMode::STOPONLY)
   {
-    d_decisionEngine.reset(new decision::JustificationStrategy(
-        satContext, userContext, d_skdm.get(), rm));
+    d_decisionEngine.reset(
+        new decision::JustificationStrategy(env, d_skdm.get()));
   }
   else if (dmode == options::DecisionMode::JUSTIFICATION_OLD
            || dmode == options::DecisionMode::STOPONLY_OLD)
   {
-    d_decisionEngine.reset(new DecisionEngineOld(satContext, userContext, rm));
+    d_decisionEngine.reset(new DecisionEngineOld(env));
   }
   else
   {
-    d_decisionEngine.reset(new decision::DecisionEngineEmpty(satContext, rm));
+    d_decisionEngine.reset(new decision::DecisionEngineEmpty(env));
   }
 
   d_satSolver = SatSolverFactory::createCDCLTMinisat(smtStatisticsRegistry());

diff --git a/src/smt/env.cpp b/src/smt/env.cpp
index 5c7836fb72de4c646a8826f761b09cd3d2c4f1db..3267702fb0a9778b835840b02decb02d3ca1429d 100644 (file)
--- a/src/smt/env.cpp
+++ b/src/smt/env.cpp
@@ -77,10 +77,10 @@ void Env::shutdown()
   d_resourceManager.reset(nullptr);
 }
 
-context::UserContext* Env::getUserContext() { return d_userContext.get(); }
-
 context::Context* Env::getContext() { return d_context.get(); }
 
+context::UserContext* Env::getUserContext() { return d_userContext.get(); }
+
 NodeManager* Env::getNodeManager() const { return d_nodeManager; }
 
 ProofNodeManager* Env::getProofNodeManager() { return d_proofNodeManager; }

diff --git a/src/smt/env_obj.cpp b/src/smt/env_obj.cpp
index b9aebbe830931439180896fc9d4a20da4319ca01..926bf61ff555c1584f917504df562350b8bc905b 100644 (file)
--- a/src/smt/env_obj.cpp
+++ b/src/smt/env_obj.cpp
@@ -49,8 +49,6 @@ Node EnvObj::evaluate(TNode n,
   return d_env.evaluate(n, args, vals, visited, useRewriter);
 }
 
-const LogicInfo& EnvObj::logicInfo() const { return d_env.getLogicInfo(); }
-
 const Options& EnvObj::options() const { return d_env.getOptions(); }
 
 context::Context* EnvObj::context() const { return d_env.getContext(); }
@@ -60,6 +58,13 @@ context::UserContext* EnvObj::userContext() const
   return d_env.getUserContext();
 }
 
+const LogicInfo& EnvObj::logicInfo() const { return d_env.getLogicInfo(); }
+
+ResourceManager* EnvObj::resourceManager() const
+{
+  return d_env.getResourceManager();
+}
+
 StatisticsRegistry& EnvObj::statisticsRegistry() const
 {
   return d_env.getStatisticsRegistry();

diff --git a/src/smt/env_obj.h b/src/smt/env_obj.h
index 75b97fda9aea78eeeed60d268073ca69cb16bd49..b240b48525c0316a2f80ba35ff81c54e65718f2d 100644 (file)
--- a/src/smt/env_obj.h
+++ b/src/smt/env_obj.h
@@ -70,9 +70,6 @@ class EnvObj
                 const std::unordered_map<Node, Node>& visited,
                 bool useRewriter = true) const;
 
-  /** Get the current logic information. */
-  const LogicInfo& logicInfo() const;
-
   /** Get the options object (const version only) via Env. */
   const Options& options() const;
 
@@ -82,6 +79,12 @@ class EnvObj
   /** Get a pointer to the UserContext via Env. */
   context::UserContext* userContext() const;
 
+  /** Get the resource manager owned by this Env. */
+  ResourceManager* resourceManager() const;
+
+  /** Get the current logic information. */
+  const LogicInfo& logicInfo() const;
+
   /** Get the statistics registry via Env. */
   StatisticsRegistry& statisticsRegistry() const;