Update theory preprocessor to use Env (#7288)

In preparation for making the "lemma context" configurable.

diff --git a/src/prop/theory_proxy.cpp b/src/prop/theory_proxy.cpp
index c18fe2dd4474fec678af6e3989fdf3fb18b804b9..5b283635d32fec6ad98c139b584b88d3522d1916 100644 (file)
--- a/src/prop/theory_proxy.cpp
+++ b/src/prop/theory_proxy.cpp
@@ -43,7 +43,7 @@ TheoryProxy::TheoryProxy(PropEngine* propEngine,
       d_decisionEngine(decisionEngine),
       d_theoryEngine(theoryEngine),
       d_queue(env.getContext()),
-      d_tpp(*theoryEngine, env.getUserContext(), env.getProofNodeManager()),
+      d_tpp(env, *theoryEngine),
       d_skdm(skdm),
       d_env(env)
 {

diff --git a/src/smt/term_formula_removal.cpp b/src/smt/term_formula_removal.cpp
index 692b7c88919743dcc561ccb34485fc39e0869ef4..6a2f6fbd467e07484aaf576fc2d48e5ff3a68268 100644 (file)
--- a/src/smt/term_formula_removal.cpp
+++ b/src/smt/term_formula_removal.cpp
@@ -23,31 +23,32 @@
 #include "options/smt_options.h"
 #include "proof/conv_proof_generator.h"
 #include "proof/lazy_proof.h"
+#include "smt/env.h"
 
 using namespace std;
 
 namespace cvc5 {
 
-RemoveTermFormulas::RemoveTermFormulas(context::UserContext* u,
-                                       ProofNodeManager* pnm)
-    : d_tfCache(u),
-      d_skolem_cache(u),
-      d_pnm(pnm),
+RemoveTermFormulas::RemoveTermFormulas(Env& env)
+    : EnvObj(env),
+      d_tfCache(userContext()),
+      d_skolem_cache(userContext()),
       d_tpg(nullptr),
       d_lp(nullptr)
 {
   // enable proofs if necessary
-  if (d_pnm != nullptr)
+  ProofNodeManager* pnm = env.getProofNodeManager();
+  if (pnm != nullptr)
   {
     d_tpg.reset(
-        new TConvProofGenerator(d_pnm,
+        new TConvProofGenerator(pnm,
                                 nullptr,
                                 TConvPolicy::FIXPOINT,
                                 TConvCachePolicy::NEVER,
                                 "RemoveTermFormulas::TConvProofGenerator",
                                 &d_rtfc));
     d_lp.reset(new LazyCDProof(
-        d_pnm, nullptr, nullptr, "RemoveTermFormulas::LazyCDProof"));
+        pnm, nullptr, nullptr, "RemoveTermFormulas::LazyCDProof"));
   }
 }
 
@@ -103,7 +104,7 @@ TrustNode RemoveTermFormulas::runLemma(TrustNode lem,
   }
   Assert(trn.getKind() == TrustNodeKind::REWRITE);
   Node newAssertion = trn.getNode();
-  if (!isProofEnabled())
+  if (!d_env.isTheoryProofProducing())
   {
     // proofs not enabled, just take result
     return TrustNode::mkTrustLemma(newAssertion, nullptr);
@@ -537,6 +538,6 @@ ProofGenerator* RemoveTermFormulas::getTConvProofGenerator()
   return d_tpg.get();
 }
 
-bool RemoveTermFormulas::isProofEnabled() const { return d_pnm != nullptr; }
+bool RemoveTermFormulas::isProofEnabled() const { return d_tpg != nullptr; }
 
 }  // namespace cvc5

diff --git a/src/smt/term_formula_removal.h b/src/smt/term_formula_removal.h
index 6f27b94629a79bf1efcca3666a00a48cd21db6fb..a47bcfbb058abcfacb215d7f9f7f9dadb4a1a9f0 100644 (file)
--- a/src/smt/term_formula_removal.h
+++ b/src/smt/term_formula_removal.h
@@ -25,6 +25,7 @@
 #include "expr/node.h"
 #include "expr/term_context.h"
 #include "proof/trust_node.h"
+#include "smt/env_obj.h"
 #include "util/hash.h"
 
 namespace cvc5 {
@@ -33,9 +34,10 @@ class LazyCDProof;
 class ProofNodeManager;
 class TConvProofGenerator;
 
-class RemoveTermFormulas {
+class RemoveTermFormulas : protected EnvObj
+{
  public:
-  RemoveTermFormulas(context::UserContext* u, ProofNodeManager* pnm = nullptr);
+  RemoveTermFormulas(Env& env);
   ~RemoveTermFormulas();
 
   /**
@@ -164,8 +166,6 @@ class RemoveTermFormulas {
    */
   inline Node getSkolemForNode(Node node) const;
 
-  /** Pointer to a proof node manager */
-  ProofNodeManager* d_pnm;
   /**
    * A proof generator for the term conversion.
    */
@@ -203,9 +203,8 @@ class RemoveTermFormulas {
    * returns the null node.
    */
   Node runCurrent(std::pair<Node, uint32_t>& curr, TrustNode& newLem);
-
-  /** Whether proofs are enabled */
+  /** Is proof enabled? True if proofs are enabled in any mode. */
   bool isProofEnabled() const;
-};/* class RemoveTTE */
+}; /* class RemoveTTE */
 
 }  // namespace cvc5

diff --git a/src/theory/theory_preprocessor.cpp b/src/theory/theory_preprocessor.cpp
index 53c90c88a88ba635a1658d0670c6cea25e520303..4b100a12f77a140ab5030aaabcafbbb5d2c13b65 100644 (file)
--- a/src/theory/theory_preprocessor.cpp
+++ b/src/theory/theory_preprocessor.cpp
@@ -27,44 +27,43 @@ using namespace std;
 namespace cvc5 {
 namespace theory {
 
-TheoryPreprocessor::TheoryPreprocessor(TheoryEngine& engine,
-                                       context::UserContext* userContext,
-                                       ProofNodeManager* pnm)
-    : d_engine(engine),
-      d_logicInfo(engine.getLogicInfo()),
-      d_ppCache(userContext),
-      d_rtfCache(userContext),
-      d_tfr(userContext, pnm),
-      d_tpg(pnm ? new TConvProofGenerator(
-                      pnm,
-                      userContext,
-                      TConvPolicy::FIXPOINT,
-                      TConvCachePolicy::NEVER,
-                      "TheoryPreprocessor::preprocess_rewrite",
-                      &d_iqtc)
-                : nullptr),
-      d_tpgRtf(pnm ? new TConvProofGenerator(pnm,
-                                             userContext,
-                                             TConvPolicy::FIXPOINT,
-                                             TConvCachePolicy::NEVER,
-                                             "TheoryPreprocessor::rtf",
-                                             &d_iqtc)
-                   : nullptr),
-      d_tpgRew(pnm ? new TConvProofGenerator(pnm,
-                                             userContext,
-                                             TConvPolicy::ONCE,
-                                             TConvCachePolicy::NEVER,
-                                             "TheoryPreprocessor::pprew")
-                   : nullptr),
+TheoryPreprocessor::TheoryPreprocessor(Env& env, TheoryEngine& engine)
+    : EnvObj(env),
+      d_engine(engine),
+      d_ppCache(userContext()),
+      d_rtfCache(userContext()),
+      d_tfr(env),
+      d_tpg(nullptr),
+      d_tpgRtf(nullptr),
+      d_tpgRew(nullptr),
       d_tspg(nullptr),
-      d_lp(pnm ? new LazyCDProof(pnm,
-                                 nullptr,
-                                 userContext,
-                                 "TheoryPreprocessor::LazyCDProof")
-               : nullptr)
+      d_lp(nullptr)
 {
-  if (isProofEnabled())
+  // proofs are enabled in the theory preprocessor regardless of the proof mode
+  ProofNodeManager* pnm = env.getProofNodeManager();
+  if (pnm != nullptr)
   {
+    context::Context* u = userContext();
+    d_tpg.reset(
+        new TConvProofGenerator(pnm,
+                                u,
+                                TConvPolicy::FIXPOINT,
+                                TConvCachePolicy::NEVER,
+                                "TheoryPreprocessor::preprocess_rewrite",
+                                &d_iqtc));
+    d_tpgRtf.reset(new TConvProofGenerator(pnm,
+                                           u,
+                                           TConvPolicy::FIXPOINT,
+                                           TConvCachePolicy::NEVER,
+                                           "TheoryPreprocessor::rtf",
+                                           &d_iqtc));
+    d_tpgRew.reset(new TConvProofGenerator(pnm,
+                                           u,
+                                           TConvPolicy::ONCE,
+                                           TConvCachePolicy::NEVER,
+                                           "TheoryPreprocessor::pprew"));
+    d_lp.reset(
+        new LazyCDProof(pnm, nullptr, u, "TheoryPreprocessor::LazyCDProof"));
     // Make the main term conversion sequence generator, which tracks up to
     // three conversions made in succession:
     // (1) rewriting
@@ -74,7 +73,7 @@ TheoryPreprocessor::TheoryPreprocessor(TheoryEngine& engine,
     ts.push_back(d_tpgRew.get());
     ts.push_back(d_tpgRtf.get());
     d_tspg.reset(new TConvSeqProofGenerator(
-        pnm, ts, userContext, "TheoryPreprocessor::sequence"));
+        pnm, ts, userContext(), "TheoryPreprocessor::sequence"));
   }
 }
 
@@ -272,10 +271,10 @@ TrustNode TheoryPreprocessor::theoryPreprocess(
 
     TheoryId tid = Theory::theoryOf(current);
 
-    if (!d_logicInfo.isTheoryEnabled(tid) && tid != THEORY_SAT_SOLVER)
+    if (!logicInfo().isTheoryEnabled(tid) && tid != THEORY_SAT_SOLVER)
     {
       stringstream ss;
-      ss << "The logic was specified as " << d_logicInfo.getLogicString()
+      ss << "The logic was specified as " << logicInfo().getLogicString()
          << ", which doesn't include " << tid
          << ", but got a preprocessing-time fact for that theory." << endl
          << "The fact:" << endl

diff --git a/src/theory/theory_preprocessor.h b/src/theory/theory_preprocessor.h
index 6015f2b07753cefdf122a23c2320a6e6a94c115d..d34bd5c457b02931e0b5dc275be9e0d732c09b5d 100644 (file)
--- a/src/theory/theory_preprocessor.h
+++ b/src/theory/theory_preprocessor.h
@@ -70,15 +70,13 @@ namespace theory {
  * rewrite a theory atom into a formula, e.g. quantifiers miniscoping. This
  * impacts what the inner traversal is applied to.
  */
-class TheoryPreprocessor
+class TheoryPreprocessor : protected EnvObj
 {
   typedef context::CDHashMap<Node, Node> NodeMap;
 
  public:
   /** Constructs a theory preprocessor */
-  TheoryPreprocessor(TheoryEngine& engine,
-                     context::UserContext* userContext,
-                     ProofNodeManager* pnm = nullptr);
+  TheoryPreprocessor(Env& env, TheoryEngine& engine);
   /** Destroys a theory preprocessor */
   ~TheoryPreprocessor();
   /**
@@ -143,8 +141,6 @@ class TheoryPreprocessor
                                     bool procLemmas);
   /** Reference to owning theory engine */
   TheoryEngine& d_engine;
-  /** Logic info of theory engine */
-  const LogicInfo& d_logicInfo;
   /**
    * Cache for theory-preprocessing of theory atoms. The domain of this map
    * are terms that appear within theory atoms given to this class.