From: Andrew Reynolds Date: Fri, 1 Oct 2021 21:47:02 +0000 (-0500) Subject: Update theory preprocessor to use Env (#7288) X-Git-Tag: cvc5-1.0.0~1134 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=6405f082a85e2a2ce7e25ff1f8b058f3f42fd58b;p=cvc5.git 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 c18fe2dd4..5b283635d 100644 --- 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 692b7c889..6a2f6fbd4 100644 --- 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 6f27b9462..a47bcfbb0 100644 --- 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& 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 53c90c88a..4b100a12f 100644 --- 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 6015f2b07..d34bd5c45 100644 --- 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 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.