A few more miscellaneous uses of EnvObj (#7325)

diff --git a/src/preprocessing/learned_literal_manager.cpp b/src/preprocessing/learned_literal_manager.cpp
index fa6a017910833b99c4b4d9b6d4524aabdaaf25e5..c40414bacb31471368667dcf4e44f19ef6ed6494 100644 (file)
--- a/src/preprocessing/learned_literal_manager.cpp
+++ b/src/preprocessing/learned_literal_manager.cpp
@@ -15,15 +15,15 @@
 
 #include "preprocessing/learned_literal_manager.h"
 
+#include "smt/env.h"
 #include "theory/rewriter.h"
+#include "theory/trust_substitutions.h"
 
 namespace cvc5 {
 namespace preprocessing {
 
-LearnedLiteralManager::LearnedLiteralManager(theory::TrustSubstitutionMap& tls,
-                                             context::UserContext* u,
-                                             ProofNodeManager* pnm)
-    : d_topLevelSubs(tls), d_learnedLits(u)
+LearnedLiteralManager::LearnedLiteralManager(Env& env)
+    : EnvObj(env), d_learnedLits(userContext())
 {
 }
 
@@ -35,12 +35,13 @@ void LearnedLiteralManager::notifyLearnedLiteral(TNode lit)
 
 std::vector<Node> LearnedLiteralManager::getLearnedLiterals() const
 {
+  theory::TrustSubstitutionMap& tls = d_env.getTopLevelSubstitutions();
   std::vector<Node> currLearnedLits;
   for (const auto& lit: d_learnedLits)
   {
     // update based on substitutions
-    Node tlsNode = d_topLevelSubs.get().apply(lit);
-    tlsNode = theory::Rewriter::rewrite(tlsNode);
+    Node tlsNode = tls.get().apply(lit);
+    tlsNode = rewrite(tlsNode);
     currLearnedLits.push_back(tlsNode);
     Trace("pp-llm") << "Learned literal : " << tlsNode << " from " << lit
                     << std::endl;

diff --git a/src/preprocessing/learned_literal_manager.h b/src/preprocessing/learned_literal_manager.h
index 2b02736286884079863725caf11484b8bd8f46fb..5e7898da40ea708e9de168142bea82aa5c2b50b0 100644 (file)
--- a/src/preprocessing/learned_literal_manager.h
+++ b/src/preprocessing/learned_literal_manager.h
@@ -20,7 +20,7 @@
 
 #include "context/cdhashset.h"
 #include "expr/node.h"
-#include "theory/trust_substitutions.h"
+#include "smt/env_obj.h"
 
 namespace cvc5 {
 namespace preprocessing {
@@ -35,12 +35,10 @@ namespace preprocessing {
  * a literal like (> x t) is learned at top-level, it may be useful to remember
  * this information. This class is concerned with the latter kind of literals.
  */
-class LearnedLiteralManager
+class LearnedLiteralManager : protected EnvObj
 {
  public:
-  LearnedLiteralManager(theory::TrustSubstitutionMap& tls,
-                        context::UserContext* u,
-                        ProofNodeManager* pnm);
+  LearnedLiteralManager(Env& env);
   /**
    * Notify learned literal. This method is called when a literal is
    * entailed by the current set of assertions.
@@ -59,8 +57,6 @@ class LearnedLiteralManager
  private:
   /** Learned literal map */
   typedef context::CDHashSet<Node> NodeSet;
-  /* The top level substitutions */
-  theory::TrustSubstitutionMap& d_topLevelSubs;
   /** Learned literals */
   NodeSet d_learnedLits;
 };

diff --git a/src/preprocessing/passes/non_clausal_simp.cpp b/src/preprocessing/passes/non_clausal_simp.cpp
index e380a107396c3b993e2fa00aae3567ffee50d6f5..4bf29157efbe8a247045215ed7dd344aeeec301b 100644 (file)
--- a/src/preprocessing/passes/non_clausal_simp.cpp
+++ b/src/preprocessing/passes/non_clausal_simp.cpp
@@ -52,12 +52,12 @@ NonClausalSimp::Statistics::Statistics(StatisticsRegistry& reg)
 NonClausalSimp::NonClausalSimp(PreprocessingPassContext* preprocContext)
     : PreprocessingPass(preprocContext, "non-clausal-simp"),
       d_statistics(statisticsRegistry()),
-      d_pnm(preprocContext->getProofNodeManager()),
+      d_pnm(d_env.getProofNodeManager()),
       d_llpg(d_pnm ? new smt::PreprocessProofGenerator(
-                 d_pnm, userContext(), "NonClausalSimp::llpg")
+                         d_pnm, userContext(), "NonClausalSimp::llpg")
                    : nullptr),
       d_llra(d_pnm ? new LazyCDProof(
-                 d_pnm, nullptr, userContext(), "NonClausalSimp::llra")
+                         d_pnm, nullptr, userContext(), "NonClausalSimp::llra")
                    : nullptr),
       d_tsubsList(userContext())
 {

diff --git a/src/preprocessing/preprocessing_pass_context.cpp b/src/preprocessing/preprocessing_pass_context.cpp
index 91f83c56e16299ea10b109ac5b47f7bf01210815..e316c2f811a7df273a1adf2e9c234712d3c912bc 100644 (file)
--- a/src/preprocessing/preprocessing_pass_context.cpp
+++ b/src/preprocessing/preprocessing_pass_context.cpp
@@ -32,8 +32,7 @@ PreprocessingPassContext::PreprocessingPassContext(
       d_theoryEngine(te),
       d_propEngine(pe),
       d_circuitPropagator(circuitPropagator),
-      d_llm(
-          env.getTopLevelSubstitutions(), userContext(), getProofNodeManager()),
+      d_llm(env),
       d_symsInAssertions(userContext())
 {
 }
@@ -97,10 +96,5 @@ void PreprocessingPassContext::addSubstitution(const Node& lhs,
   getTopLevelSubstitutions().addSubstitution(lhs, rhs, id, {}, args);
 }
 
-ProofNodeManager* PreprocessingPassContext::getProofNodeManager() const
-{
-  return d_env.getProofNodeManager();
-}
-
 }  // namespace preprocessing
 }  // namespace cvc5

diff --git a/src/preprocessing/preprocessing_pass_context.h b/src/preprocessing/preprocessing_pass_context.h
index fc3faa7abada04a455e841cfebe0a3e065be444c..d452e23ff5b3947d80868d61a4e703bc0f57c4ea 100644 (file)
--- a/src/preprocessing/preprocessing_pass_context.h
+++ b/src/preprocessing/preprocessing_pass_context.h
@@ -26,6 +26,7 @@
 #include "preprocessing/learned_literal_manager.h"
 #include "smt/env_obj.h"
 #include "theory/logic_info.h"
+#include "theory/trust_substitutions.h"
 #include "util/resource_manager.h"
 
 namespace cvc5 {
@@ -116,8 +117,6 @@ class PreprocessingPassContext : protected EnvObj
                        PfRule id,
                        const std::vector<Node>& args);
 
-  /** The the proof node manager associated with this context, if it exists */
-  ProofNodeManager* getProofNodeManager() const;
 
  private:
   /** Pointer to the theory engine associated with this context. */

diff --git a/src/smt/smt_engine_state.cpp b/src/smt/smt_engine_state.cpp
index 37b057048424229b620a6b5c2fabfabdf8669f95..9452081c9b81491b96b98f0206c58c7beb1b72d7 100644 (file)
--- a/src/smt/smt_engine_state.cpp
+++ b/src/smt/smt_engine_state.cpp
@@ -27,8 +27,8 @@ namespace cvc5 {
 namespace smt {
 
 SmtEngineState::SmtEngineState(Env& env, SolverEngine& slv)
-    : d_slv(slv),
-      d_env(env),
+    : EnvObj(env),
+      d_slv(slv),
       d_pendingPops(0),
       d_fullyInited(false),
       d_queryMade(false),
@@ -44,7 +44,7 @@ void SmtEngineState::notifyExpectedStatus(const std::string& status)
   Assert(status == "sat" || status == "unsat" || status == "unknown")
       << "SmtEngineState::notifyExpectedStatus: unexpected status string "
       << status;
-  d_expectedStatus = Result(status, d_env.getOptions().driver.filename);
+  d_expectedStatus = Result(status, options().driver.filename);
 }
 
 void SmtEngineState::notifyResetAssertions()
@@ -56,7 +56,7 @@ void SmtEngineState::notifyResetAssertions()
   }
   // Remember the global push/pop around everything when beyond Start mode
   // (see solver execution modes in the SMT-LIB standard)
-  Assert(d_userLevels.size() == 0 && getUserContext()->getLevel() == 1);
+  Assert(d_userLevels.size() == 0 && userContext()->getLevel() == 1);
   popto(0);
 }
 
@@ -157,7 +157,7 @@ void SmtEngineState::shutdown()
 {
   doPendingPops();
 
-  while (options::incrementalSolving() && getUserContext()->getLevel() > 1)
+  while (options::incrementalSolving() && userContext()->getLevel() > 1)
   {
     internalPop(true);
   }
@@ -181,10 +181,10 @@ void SmtEngineState::userPush()
   // staying symmetric with pop.
   d_smtMode = SmtMode::ASSERT;
 
-  d_userLevels.push_back(getUserContext()->getLevel());
+  d_userLevels.push_back(userContext()->getLevel());
   internalPush();
   Trace("userpushpop") << "SmtEngineState: pushed to level "
-                       << getUserContext()->getLevel() << std::endl;
+                       << userContext()->getLevel() << std::endl;
 }
 
 void SmtEngineState::userPop()
@@ -206,35 +206,30 @@ void SmtEngineState::userPop()
   // is no longer in scope!).
   d_smtMode = SmtMode::ASSERT;
 
-  AlwaysAssert(getUserContext()->getLevel() > 0);
-  AlwaysAssert(d_userLevels.back() < getUserContext()->getLevel());
-  while (d_userLevels.back() < getUserContext()->getLevel())
+  AlwaysAssert(userContext()->getLevel() > 0);
+  AlwaysAssert(d_userLevels.back() < userContext()->getLevel());
+  while (d_userLevels.back() < userContext()->getLevel())
   {
     internalPop(true);
   }
   d_userLevels.pop_back();
 }
-context::Context* SmtEngineState::getContext() { return d_env.getContext(); }
-context::UserContext* SmtEngineState::getUserContext()
-{
-  return d_env.getUserContext();
-}
 void SmtEngineState::push()
 {
-  getUserContext()->push();
-  getContext()->push();
+  userContext()->push();
+  context()->push();
 }
 
 void SmtEngineState::pop()
 {
-  getUserContext()->pop();
-  getContext()->pop();
+  userContext()->pop();
+  context()->pop();
 }
 
 void SmtEngineState::popto(int toLevel)
 {
-  getContext()->popto(toLevel);
-  getUserContext()->popto(toLevel);
+  context()->popto(toLevel);
+  userContext()->popto(toLevel);
 }
 
 Result SmtEngineState::getStatus() const { return d_status; }
@@ -258,7 +253,7 @@ void SmtEngineState::internalPush()
   {
     // notifies the SolverEngine to process the assertions immediately
     d_slv.notifyPushPre();
-    getUserContext()->push();
+    userContext()->push();
     // the context push is done inside of the SAT solver
     d_slv.notifyPushPost();
   }
@@ -292,7 +287,7 @@ void SmtEngineState::doPendingPops()
     // the context pop is done inside of the SAT solver
     d_slv.notifyPopPre();
     // pop the context
-    getUserContext()->pop();
+    userContext()->pop();
     --d_pendingPops;
     // no need for pop post (for now)
   }

diff --git a/src/smt/smt_engine_state.h b/src/smt/smt_engine_state.h
index 535be2092798a12bcd413e28567b44ac4b7fd827..d7a0e2290bc73649b1c89c38baea4180330ad1b8 100644 (file)
--- a/src/smt/smt_engine_state.h
+++ b/src/smt/smt_engine_state.h
@@ -21,13 +21,13 @@
 #include <string>
 
 #include "context/context.h"
+#include "smt/env_obj.h"
 #include "smt/smt_mode.h"
 #include "util/result.h"
 
 namespace cvc5 {
 
 class SolverEngine;
-class Env;
 
 namespace smt {
 
@@ -48,7 +48,7 @@ namespace smt {
  * It maintains a reference to the SolverEngine for the sake of making
  * callbacks.
  */
-class SmtEngineState
+class SmtEngineState : protected EnvObj
 {
  public:
   SmtEngineState(Env& env, SolverEngine& smt);
@@ -176,10 +176,6 @@ class SmtEngineState
   //---------------------------- end queries
 
  private:
-  /** get the sat context we are using */
-  context::Context* getContext();
-  /** get the user context we are using */
-  context::UserContext* getUserContext();
   /** Pushes the user and SAT contexts */
   void push();
   /** Pops the user and SAT contexts */
@@ -199,8 +195,6 @@ class SmtEngineState
   void internalPop(bool immediate = false);
   /** Reference to the SolverEngine */
   SolverEngine& d_slv;
-  /** Reference to the env of the parent SolverEngine */
-  Env& d_env;
   /** The context levels of user pushes */
   std::vector<int> d_userLevels;