From: Andrew Reynolds Date: Sat, 9 Jul 2022 03:42:48 +0000 (-0500) Subject: Eliminate static options access in proof utilities (#8927) X-Git-Tag: cvc5-1.0.1~11 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=2812687446f7f967b62f3e8410012a96e2a87068;p=cvc5.git Eliminate static options access in proof utilities (#8927) This requires changing many of the proof interfaces to pass Env instead of ProofNodeManager. This is also work towards simplifying the initialization of our proof infrastructure. --- diff --git a/src/preprocessing/passes/miplib_trick.cpp b/src/preprocessing/passes/miplib_trick.cpp index 372f70a21..fcfce0875 100644 --- a/src/preprocessing/passes/miplib_trick.cpp +++ b/src/preprocessing/passes/miplib_trick.cpp @@ -537,7 +537,7 @@ PreprocessingPassResult MipLibTrick::applyInternal( Node n = rewrite(geq.andNode(leq)); assertionsToPreprocess->push_back(n); - TrustSubstitutionMap tnullMap(&fakeContext, nullptr); + TrustSubstitutionMap tnullMap(d_env, &fakeContext); CVC5_UNUSED SubstitutionMap& nullMap = tnullMap.get(); Theory::PPAssertStatus status CVC5_UNUSED; // just for assertions status = te->solve(tgeq, tnullMap); diff --git a/src/preprocessing/passes/non_clausal_simp.cpp b/src/preprocessing/passes/non_clausal_simp.cpp index cca0f72b9..70f47641e 100644 --- a/src/preprocessing/passes/non_clausal_simp.cpp +++ b/src/preprocessing/passes/non_clausal_simp.cpp @@ -52,13 +52,12 @@ NonClausalSimp::Statistics::Statistics(StatisticsRegistry& reg) NonClausalSimp::NonClausalSimp(PreprocessingPassContext* preprocContext) : PreprocessingPass(preprocContext, "non-clausal-simp"), d_statistics(statisticsRegistry()), - d_pnm(d_env.getProofNodeManager()), - d_llpg(d_pnm ? new smt::PreprocessProofGenerator( + d_llpg(options().smt.produceProofs ? new smt::PreprocessProofGenerator( d_env, userContext(), "NonClausalSimp::llpg") - : nullptr), - d_llra(d_pnm ? new LazyCDProof( - d_pnm, nullptr, userContext(), "NonClausalSimp::llra") - : nullptr), + : nullptr), + d_llra(options().smt.produceProofs ? new LazyCDProof( + d_env, nullptr, userContext(), "NonClausalSimp::llra") + : nullptr), d_tsubsList(userContext()) { } @@ -124,12 +123,12 @@ PreprocessingPassResult NonClausalSimp::applyInternal( // constant propagations std::shared_ptr constantPropagations = std::make_shared( - u, d_pnm, "NonClausalSimp::cprop", PfRule::PREPROCESS_LEMMA); + d_env, u, "NonClausalSimp::cprop", PfRule::PREPROCESS_LEMMA); SubstitutionMap& cps = constantPropagations->get(); // new substitutions std::shared_ptr newSubstitutions = std::make_shared( - u, d_pnm, "NonClausalSimp::newSubs", PfRule::PREPROCESS_LEMMA); + d_env, u, "NonClausalSimp::newSubs", PfRule::PREPROCESS_LEMMA); SubstitutionMap& nss = newSubstitutions->get(); size_t j = 0; @@ -451,7 +450,10 @@ PreprocessingPassResult NonClausalSimp::applyInternal( return PreprocessingPassResult::NO_CONFLICT; } -bool NonClausalSimp::isProofEnabled() const { return d_pnm != nullptr; } +bool NonClausalSimp::isProofEnabled() const +{ + return options().smt.produceProofs; +} Node NonClausalSimp::processLearnedLit(Node lit, theory::TrustSubstitutionMap* subs, diff --git a/src/preprocessing/passes/non_clausal_simp.h b/src/preprocessing/passes/non_clausal_simp.h index 5d988ec56..e643c1364 100644 --- a/src/preprocessing/passes/non_clausal_simp.h +++ b/src/preprocessing/passes/non_clausal_simp.h @@ -79,8 +79,6 @@ class NonClausalSimp : public PreprocessingPass Node processRewrittenLearnedLit(TrustNode trn); /** Is proof enabled? */ bool isProofEnabled() const; - /** The proof node manager */ - ProofNodeManager* d_pnm; /** the learned literal preprocess proof generator */ std::unique_ptr d_llpg; /** diff --git a/src/proof/alethe/alethe_post_processor.cpp b/src/proof/alethe/alethe_post_processor.cpp index 86c2ef115..db6cb7c1b 100644 --- a/src/proof/alethe/alethe_post_processor.cpp +++ b/src/proof/alethe/alethe_post_processor.cpp @@ -21,6 +21,7 @@ #include "proof/proof_checker.h" #include "proof/proof_node_algorithm.h" #include "proof/proof_node_manager.h" +#include "smt/env.h" #include "theory/builtin/proof_checker.h" #include "util/rational.h" @@ -31,8 +32,8 @@ namespace cvc5::internal { namespace proof { AletheProofPostprocessCallback::AletheProofPostprocessCallback( - ProofNodeManager* pnm, AletheNodeConverter& anc, bool resPivots) - : d_pnm(pnm), d_anc(anc), d_resPivots(resPivots) + Env& env, AletheNodeConverter& anc, bool resPivots) + : EnvObj(env), d_anc(anc), d_resPivots(resPivots) { NodeManager* nm = NodeManager::currentNM(); d_cl = nm->mkBoundVar("cl", nm->sExprType()); @@ -1819,10 +1820,10 @@ bool AletheProofPostprocessCallback::addAletheStepFromOr( return addAletheStep(rule, res, conclusion, children, args, cdp); } -AletheProofPostprocess::AletheProofPostprocess(ProofNodeManager* pnm, +AletheProofPostprocess::AletheProofPostprocess(Env& env, AletheNodeConverter& anc, bool resPivots) - : d_pnm(pnm), d_cb(d_pnm, anc, resPivots) + : EnvObj(env), d_cb(env, anc, resPivots) { } @@ -1831,7 +1832,7 @@ AletheProofPostprocess::~AletheProofPostprocess() {} void AletheProofPostprocess::process(std::shared_ptr pf) { // Translate proof node - ProofNodeUpdater updater(d_pnm, d_cb, false, false); + ProofNodeUpdater updater(d_env, d_cb, false, false); updater.process(pf->getChildren()[0]); // In the Alethe proof format the final step has to be (cl). However, after @@ -1839,7 +1840,7 @@ void AletheProofPostprocess::process(std::shared_ptr pf) // required. // The function has the additional purpose of sanitizing the attributes of the // first SCOPE - CDProof cpf(d_pnm, nullptr, "ProofNodeUpdater::CDProof", true); + CDProof cpf(d_env, nullptr, "ProofNodeUpdater::CDProof", true); const std::vector>& cc = pf->getChildren(); std::vector ccn; for (const std::shared_ptr& cp : cc) @@ -1856,7 +1857,7 @@ void AletheProofPostprocess::process(std::shared_ptr pf) // then, update the original proof node based on this one Trace("pf-process-debug") << "Update node..." << std::endl; - d_pnm->updateNode(pf.get(), npn.get()); + d_env.getProofNodeManager()->updateNode(pf.get(), npn.get()); Trace("pf-process-debug") << "...update node finished." << std::endl; } } diff --git a/src/proof/alethe/alethe_post_processor.h b/src/proof/alethe/alethe_post_processor.h index 620846120..638d9c3ac 100644 --- a/src/proof/alethe/alethe_post_processor.h +++ b/src/proof/alethe/alethe_post_processor.h @@ -28,10 +28,11 @@ namespace proof { * A callback class used by the Alethe converter for post-processing proof nodes * by replacing internal rules by the rules in the Alethe calculus. */ -class AletheProofPostprocessCallback : public ProofNodeUpdaterCallback +class AletheProofPostprocessCallback : protected EnvObj, + public ProofNodeUpdaterCallback { public: - AletheProofPostprocessCallback(ProofNodeManager* pnm, + AletheProofPostprocessCallback(Env& env, AletheNodeConverter& anc, bool resPivots); ~AletheProofPostprocessCallback() {} @@ -88,8 +89,6 @@ class AletheProofPostprocessCallback : public ProofNodeUpdaterCallback CDProof* cdp); private: - /** The proof node manager */ - ProofNodeManager* d_pnm; /** The Alethe node converter */ AletheNodeConverter& d_anc; /** Whether to keep the pivots in the alguments of the resolution rule */ @@ -145,19 +144,15 @@ class AletheProofPostprocessCallback : public ProofNodeUpdaterCallback * The proof postprocessor module. This postprocesses a proof node into one * using the rules from the Alethe calculus. */ -class AletheProofPostprocess +class AletheProofPostprocess : protected EnvObj { public: - AletheProofPostprocess(ProofNodeManager* pnm, - AletheNodeConverter& anc, - bool resPivots); + AletheProofPostprocess(Env& env, AletheNodeConverter& anc, bool resPivots); ~AletheProofPostprocess(); /** post-process */ void process(std::shared_ptr pf); private: - /** The proof node manager */ - ProofNodeManager* d_pnm; /** The post process callback */ AletheProofPostprocessCallback d_cb; }; diff --git a/src/proof/buffered_proof_generator.cpp b/src/proof/buffered_proof_generator.cpp index 0a7e63404..7fa49f089 100644 --- a/src/proof/buffered_proof_generator.cpp +++ b/src/proof/buffered_proof_generator.cpp @@ -20,9 +20,8 @@ namespace cvc5::internal { -BufferedProofGenerator::BufferedProofGenerator(context::Context* c, - ProofNodeManager* pnm) - : ProofGenerator(), d_facts(c), d_pnm(pnm) +BufferedProofGenerator::BufferedProofGenerator(Env& env, context::Context* c) + : EnvObj(env), ProofGenerator(), d_facts(c) { } @@ -76,7 +75,7 @@ std::shared_ptr BufferedProofGenerator::getProofFor(Node fact) } } Trace("pfee-fact-gen") << "...return via step " << *(*it).second << std::endl; - CDProof cdp(d_pnm); + CDProof cdp(d_env); cdp.addStep(fact, *(*it).second); return cdp.getProofFor(fact); } diff --git a/src/proof/buffered_proof_generator.h b/src/proof/buffered_proof_generator.h index 418f130a3..7c72547f7 100644 --- a/src/proof/buffered_proof_generator.h +++ b/src/proof/buffered_proof_generator.h @@ -20,6 +20,7 @@ #include "context/cdhashmap.h" #include "proof/proof_generator.h" +#include "smt/env_obj.h" namespace cvc5::internal { @@ -31,12 +32,12 @@ class ProofStep; * mapping from formulas to proof steps. It does not generate ProofNodes until * it is asked to provide a proof for a given fact. */ -class BufferedProofGenerator : public ProofGenerator +class BufferedProofGenerator : protected EnvObj, public ProofGenerator { typedef context::CDHashMap> NodeProofStepMap; public: - BufferedProofGenerator(context::Context* c, ProofNodeManager* pnm); + BufferedProofGenerator(Env& env, context::Context* c); ~BufferedProofGenerator() {} /** add step * Unless the overwrite policy is ALWAYS it does not replace previously @@ -55,8 +56,6 @@ class BufferedProofGenerator : public ProofGenerator private: /** maps expected to ProofStep */ NodeProofStepMap d_facts; - /** the proof node manager */ - ProofNodeManager* d_pnm; }; } // namespace cvc5::internal diff --git a/src/proof/conv_proof_generator.cpp b/src/proof/conv_proof_generator.cpp index a4bd399bf..790cd4a4b 100644 --- a/src/proof/conv_proof_generator.cpp +++ b/src/proof/conv_proof_generator.cpp @@ -50,14 +50,15 @@ std::ostream& operator<<(std::ostream& out, TConvCachePolicy tcpol) return out; } -TConvProofGenerator::TConvProofGenerator(ProofNodeManager* pnm, +TConvProofGenerator::TConvProofGenerator(Env& env, context::Context* c, TConvPolicy pol, TConvCachePolicy cpol, std::string name, TermContext* tccb, bool rewriteOps) - : d_proof(pnm, nullptr, c, name + "::LazyCDProof"), + : EnvObj(env), + d_proof(env, nullptr, c, name + "::LazyCDProof"), d_preRewriteMap(c ? c : &d_context), d_postRewriteMap(c ? c : &d_context), d_policy(pol), @@ -183,8 +184,7 @@ std::shared_ptr TConvProofGenerator::getProofFor(Node f) return nullptr; } // we use the existing proofs - LazyCDProof lpf( - d_proof.getManager(), &d_proof, nullptr, d_name + "::LazyCDProof"); + LazyCDProof lpf(d_env, &d_proof, nullptr, d_name + "::LazyCDProof"); if (f[0] == f[1]) { // assertion failure in debug @@ -239,8 +239,7 @@ std::shared_ptr TConvProofGenerator::getProofFor(Node f) std::shared_ptr TConvProofGenerator::getProofForRewriting(Node n) { - LazyCDProof lpf( - d_proof.getManager(), &d_proof, nullptr, d_name + "::LazyCDProofRew"); + LazyCDProof lpf(d_env, &d_proof, nullptr, d_name + "::LazyCDProofRew"); Node conc = getProofForRewriting(n, lpf, d_tcontext); if (conc[1] == n) { diff --git a/src/proof/conv_proof_generator.h b/src/proof/conv_proof_generator.h index 60aa4333a..ee4429384 100644 --- a/src/proof/conv_proof_generator.h +++ b/src/proof/conv_proof_generator.h @@ -114,14 +114,14 @@ std::ostream& operator<<(std::ostream& out, TConvCachePolicy tcpol); * replayed in the expected way, e.g. the occurrence of (and A B) that is not * in term position is not rewritten. */ -class TConvProofGenerator : public ProofGenerator +class TConvProofGenerator : protected EnvObj, public ProofGenerator { public: /** * Constructor, which notice does fixpoint rewriting (since this is the * most common use case) and never caches. * - * @param pnm The proof node manager for constructing ProofNode objects. + * @param env Reference to the environment. * @param c The context that this class depends on. If none is provided, * this class is context-independent. * @param tpol The policy for applying rewrite steps of this class. For @@ -132,7 +132,7 @@ class TConvProofGenerator : public ProofGenerator * is non-null, then this class stores a term-context-sensitive rewrite * system. The rewrite steps should be given term context identifiers. */ - TConvProofGenerator(ProofNodeManager* pnm, + TConvProofGenerator(Env& env, context::Context* c = nullptr, TConvPolicy pol = TConvPolicy::FIXPOINT, TConvCachePolicy cpol = TConvCachePolicy::NEVER, diff --git a/src/proof/eager_proof_generator.cpp b/src/proof/eager_proof_generator.cpp index 52432fb02..289daf620 100644 --- a/src/proof/eager_proof_generator.cpp +++ b/src/proof/eager_proof_generator.cpp @@ -18,13 +18,14 @@ #include "proof/proof.h" #include "proof/proof_node.h" #include "proof/proof_node_manager.h" +#include "smt/env.h" namespace cvc5::internal { -EagerProofGenerator::EagerProofGenerator(ProofNodeManager* pnm, +EagerProofGenerator::EagerProofGenerator(Env& env, context::Context* c, std::string name) - : d_pnm(pnm), d_name(name), d_proofs(c == nullptr ? &d_context : c) + : EnvObj(env), d_name(name), d_proofs(c == nullptr ? &d_context : c) { } @@ -104,20 +105,21 @@ TrustNode EagerProofGenerator::mkTrustNode(Node conc, const std::vector& args, bool isConflict) { + ProofNodeManager* pnm = d_env.getProofNodeManager(); // if no children, its easy if (exp.empty()) { - std::shared_ptr pf = d_pnm->mkNode(id, {}, args, conc); + std::shared_ptr pf = pnm->mkNode(id, {}, args, conc); return mkTrustNode(conc, pf, isConflict); } // otherwise, we use CDProof + SCOPE - CDProof cdp(d_pnm); + CDProof cdp(d_env); cdp.addStep(conc, id, exp, args); std::shared_ptr pf = cdp.getProofFor(conc); // We use mkNode instead of mkScope, since there is no reason to check // whether the free assumptions of pf are in exp, since they are by the // construction above. - std::shared_ptr pfs = d_pnm->mkNode(PfRule::SCOPE, {pf}, exp); + std::shared_ptr pfs = pnm->mkNode(PfRule::SCOPE, {pf}, exp); return mkTrustNode(pfs->getResult(), pfs, isConflict); } @@ -140,7 +142,7 @@ TrustNode EagerProofGenerator::mkTrustedRewrite(Node a, const std::vector& args) { Node eq = a.eqNode(b); - CDProof cdp(d_pnm); + CDProof cdp(d_env); cdp.addStep(eq, id, {}, args); std::shared_ptr pf = cdp.getProofFor(eq); return mkTrustedRewrite(a, b, pf); diff --git a/src/proof/eager_proof_generator.h b/src/proof/eager_proof_generator.h index aba4ec11e..a0c0db257 100644 --- a/src/proof/eager_proof_generator.h +++ b/src/proof/eager_proof_generator.h @@ -23,6 +23,7 @@ #include "proof/proof_generator.h" #include "proof/proof_rule.h" #include "proof/trust_node.h" +#include "smt/env_obj.h" namespace cvc5::internal { @@ -83,12 +84,12 @@ class ProofNodeManager; * storing the proof internally, and the proof output channel is responsible for * maintaining the map that epg is who to ask for the proof of the conflict. */ -class EagerProofGenerator : public ProofGenerator +class EagerProofGenerator : protected EnvObj, public ProofGenerator { typedef context::CDHashMap> NodeProofNodeMap; public: - EagerProofGenerator(ProofNodeManager* pnm, + EagerProofGenerator(Env& env, context::Context* c = nullptr, std::string name = "EagerProofGenerator"); ~EagerProofGenerator() {} @@ -191,8 +192,6 @@ class EagerProofGenerator : public ProofGenerator void setProofForLemma(Node lem, std::shared_ptr pf); /** Set that pf is the proof for explained propagation */ void setProofForPropExp(TNode lit, Node exp, std::shared_ptr pf); - /** The proof node manager */ - ProofNodeManager* d_pnm; /** Name identifier */ std::string d_name; /** A dummy context used by this class if none is provided */ diff --git a/src/proof/lazy_proof.cpp b/src/proof/lazy_proof.cpp index 01cd56452..ec4a80c56 100644 --- a/src/proof/lazy_proof.cpp +++ b/src/proof/lazy_proof.cpp @@ -23,13 +23,13 @@ using namespace cvc5::internal::kind; namespace cvc5::internal { -LazyCDProof::LazyCDProof(ProofNodeManager* pnm, +LazyCDProof::LazyCDProof(Env& env, ProofGenerator* dpg, context::Context* c, const std::string& name, bool autoSym, bool doCache) - : CDProof(pnm, c, name, autoSym), + : CDProof(env, c, name, autoSym), d_gens(c ? c : &d_context), d_defaultGen(dpg), d_doCache(doCache), @@ -122,16 +122,16 @@ std::shared_ptr LazyCDProof::getProofFor(Node fact) { if (pgc->getRule() == PfRule::SYMM) { - d_manager->updateNode(cur, pgc->getChildren()[0].get()); + getManager()->updateNode(cur, pgc->getChildren()[0].get()); } else { - d_manager->updateNode(cur, PfRule::SYMM, {pgc}, {}); + getManager()->updateNode(cur, PfRule::SYMM, {pgc}, {}); } } else { - d_manager->updateNode(cur, pgc.get()); + getManager()->updateNode(cur, pgc.get()); } Trace("lazy-cdproof") << "LazyCDProof: Successfully added fact for " << cfactGen << std::endl; @@ -201,7 +201,7 @@ void LazyCDProof::addLazyStep(Node expected, if (isClosed) { Trace("lazy-cdproof-debug") << "Checking closed..." << std::endl; - pfgEnsureClosed(expected, pg, "lazy-cdproof-debug", ctx); + pfgEnsureClosed(options(), expected, pg, "lazy-cdproof-debug", ctx); } } diff --git a/src/proof/lazy_proof.h b/src/proof/lazy_proof.h index 027f90c50..877cc1494 100644 --- a/src/proof/lazy_proof.h +++ b/src/proof/lazy_proof.h @@ -51,7 +51,7 @@ class LazyCDProof : public CDProof * to getProofFor, even if new steps are provided to this class in the * meantime. */ - LazyCDProof(ProofNodeManager* pnm, + LazyCDProof(Env& env, ProofGenerator* dpg = nullptr, context::Context* c = nullptr, const std::string& name = "LazyCDProof", diff --git a/src/proof/lazy_proof_chain.cpp b/src/proof/lazy_proof_chain.cpp index c8dc842e2..46a071e9c 100644 --- a/src/proof/lazy_proof_chain.cpp +++ b/src/proof/lazy_proof_chain.cpp @@ -24,14 +24,13 @@ namespace cvc5::internal { -LazyCDProofChain::LazyCDProofChain(ProofNodeManager* pnm, +LazyCDProofChain::LazyCDProofChain(Env& env, bool cyclic, context::Context* c, ProofGenerator* defGen, bool defRec, const std::string& name) - : CDProof(pnm, c, name, false), - d_manager(pnm), + : CDProof(env, c, name, false), d_cyclic(cyclic), d_defRec(defRec), d_context(), @@ -255,6 +254,7 @@ std::shared_ptr LazyCDProofChain::getProofFor(Node fact) << "\n"; } } while (!visit.empty()); + ProofNodeManager* pnm = getManager(); // expand all assumptions marked to be connected for (const std::pair>& npfn : toConnect) @@ -275,7 +275,7 @@ std::shared_ptr LazyCDProofChain::getProofFor(Node fact) // update each assumption proof node for (std::shared_ptr pfn : it->second) { - d_manager->updateNode(pfn.get(), npfn.second.get()); + pnm->updateNode(pfn.get(), npfn.second.get()); } } Trace("lazy-cdproofchain") << "===========\n"; @@ -328,7 +328,8 @@ void LazyCDProofChain::addLazyStep(Node expected, } Trace("lazy-cdproofchain") << "\n"; } - pfnEnsureClosedWrt(pfn.get(), allowedLeaves, "lazy-cdproofchain", ctx); + pfnEnsureClosedWrt( + options(), pfn.get(), allowedLeaves, "lazy-cdproofchain", ctx); } } diff --git a/src/proof/lazy_proof_chain.h b/src/proof/lazy_proof_chain.h index 88d51c94a..fe3011157 100644 --- a/src/proof/lazy_proof_chain.h +++ b/src/proof/lazy_proof_chain.h @@ -40,7 +40,7 @@ class LazyCDProofChain : public CDProof public: /** Constructor * - * @param pnm The proof node manager for constructing ProofNode objects. + * @param env Reference to the environment * @param cyclic Whether this instance is robust to cycles in the chain. * @param c The context that this class depends on. If none is provided, * this class is context-independent. @@ -48,7 +48,7 @@ class LazyCDProofChain : public CDProof * for a step. * @param defRec Whether this instance expands proofs from defGen recursively. */ - LazyCDProofChain(ProofNodeManager* pnm, + LazyCDProofChain(Env& env, bool cyclic = true, context::Context* c = nullptr, ProofGenerator* defGen = nullptr, @@ -147,9 +147,6 @@ class LazyCDProofChain : public CDProof * Returns a nullptr when no internal proof stored. */ std::shared_ptr getProofForInternal(Node fact, bool& rec); - - /** The proof manager, used for allocating new ProofNode objects */ - ProofNodeManager* d_manager; /** Whether this instance is robust to cycles in the chain. */ bool d_cyclic; /** Whether we expand recursively (for the default generator) */ diff --git a/src/proof/lazy_tree_proof_generator.cpp b/src/proof/lazy_tree_proof_generator.cpp index f231cd5b0..591e6ae16 100644 --- a/src/proof/lazy_tree_proof_generator.cpp +++ b/src/proof/lazy_tree_proof_generator.cpp @@ -22,12 +22,13 @@ #include "proof/proof_generator.h" #include "proof/proof_node.h" #include "proof/proof_node_manager.h" +#include "smt/env.h" namespace cvc5::internal { -LazyTreeProofGenerator::LazyTreeProofGenerator(ProofNodeManager* pnm, +LazyTreeProofGenerator::LazyTreeProofGenerator(Env& env, const std::string& name) - : d_pnm(pnm), d_name(name) + : EnvObj(env), d_name(name) { d_stack.emplace_back(&d_proof); } @@ -90,6 +91,7 @@ std::shared_ptr LazyTreeProofGenerator::getProof( std::vector>& scope, const detail::TreeProofNode& pn) const { + ProofNodeManager* pnm = d_env.getProofNodeManager(); // Store scope size to reset scope afterwards std::size_t before = scope.size(); std::vector> children; @@ -100,7 +102,7 @@ std::shared_ptr LazyTreeProofGenerator::getProof( { for (const auto& a : pn.d_args) { - scope.emplace_back(d_pnm->mkAssume(a)); + scope.emplace_back(pnm->mkAssume(a)); } } } @@ -117,11 +119,11 @@ std::shared_ptr LazyTreeProofGenerator::getProof( for (const auto& p : pn.d_premise) { // Add premises as assumptions - children.emplace_back(d_pnm->mkAssume(p)); + children.emplace_back(pnm->mkAssume(p)); } // Reset scope scope.resize(before); - return d_pnm->mkNode(pn.d_rule, children, pn.d_args); + return pnm->mkNode(pn.d_rule, children, pn.d_args); } void LazyTreeProofGenerator::print(std::ostream& os, diff --git a/src/proof/lazy_tree_proof_generator.h b/src/proof/lazy_tree_proof_generator.h index 3e90c2c67..0e84c5c15 100644 --- a/src/proof/lazy_tree_proof_generator.h +++ b/src/proof/lazy_tree_proof_generator.h @@ -23,6 +23,7 @@ #include "expr/node.h" #include "proof/proof_generator.h" #include "proof/proof_node_manager.h" +#include "smt/env_obj.h" namespace cvc5::internal { namespace detail { @@ -124,13 +125,13 @@ struct TreeProofNode * To explicitly finish proof construction, we need to call closeChild() one * additional time. */ -class LazyTreeProofGenerator : public ProofGenerator +class LazyTreeProofGenerator : protected EnvObj, public ProofGenerator { public: friend std::ostream& operator<<(std::ostream& os, const LazyTreeProofGenerator& ltpg); - LazyTreeProofGenerator(ProofNodeManager* pnm, + LazyTreeProofGenerator(Env& env, const std::string& name = "LazyTreeProofGenerator"); std::string identify() const override { return d_name; } @@ -192,8 +193,6 @@ class LazyTreeProofGenerator : public ProofGenerator const std::string& prefix, const detail::TreeProofNode& pn) const; - /** The ProofNodeManager used for constructing ProofNodes */ - ProofNodeManager* d_pnm; /** The trace to the current node */ std::vector d_stack; /** The root node of the proof tree */ diff --git a/src/proof/lfsc/lfsc_post_processor.cpp b/src/proof/lfsc/lfsc_post_processor.cpp index 9fe578230..a24db91d5 100644 --- a/src/proof/lfsc/lfsc_post_processor.cpp +++ b/src/proof/lfsc/lfsc_post_processor.cpp @@ -22,6 +22,7 @@ #include "proof/proof_node_algorithm.h" #include "proof/proof_node_manager.h" #include "proof/proof_node_updater.h" +#include "smt/env.h" #include "theory/strings/theory_strings_utils.h" using namespace cvc5::internal::kind; @@ -30,8 +31,11 @@ namespace cvc5::internal { namespace proof { LfscProofPostprocessCallback::LfscProofPostprocessCallback( - LfscNodeConverter& ltp, ProofNodeManager* pnm) - : d_pnm(pnm), d_pc(pnm->getChecker()), d_tproc(ltp), d_firstTime(false) + Env& env, LfscNodeConverter& ltp) + : EnvObj(env), + d_pc(env.getProofNodeManager()->getChecker()), + d_tproc(ltp), + d_firstTime(false) { } @@ -427,9 +431,8 @@ Node LfscProofPostprocessCallback::mkDummyPredicate() return nm->mkBoundVar(nm->booleanType()); } -LfscProofPostprocess::LfscProofPostprocess(LfscNodeConverter& ltp, - ProofNodeManager* pnm) - : d_cb(new proof::LfscProofPostprocessCallback(ltp, pnm)), d_pnm(pnm) +LfscProofPostprocess::LfscProofPostprocess(Env& env, LfscNodeConverter& ltp) + : EnvObj(env), d_cb(new proof::LfscProofPostprocessCallback(env, ltp)) { } @@ -438,7 +441,7 @@ void LfscProofPostprocess::process(std::shared_ptr pf) d_cb->initializeUpdate(); // do not automatically add symmetry steps, since this leads to // non-termination for example on policy_variable.smt2 - ProofNodeUpdater updater(d_pnm, *(d_cb.get()), false, false); + ProofNodeUpdater updater(d_env, *(d_cb.get()), false, false); updater.process(pf); } diff --git a/src/proof/lfsc/lfsc_post_processor.h b/src/proof/lfsc/lfsc_post_processor.h index 72cdca8c3..b1e8f5103 100644 --- a/src/proof/lfsc/lfsc_post_processor.h +++ b/src/proof/lfsc/lfsc_post_processor.h @@ -24,6 +24,7 @@ #include "proof/lfsc/lfsc_node_converter.h" #include "proof/lfsc/lfsc_util.h" #include "proof/proof_node_updater.h" +#include "smt/env_obj.h" namespace cvc5::internal { @@ -35,10 +36,11 @@ namespace proof { * A callback class used by the Lfsc convereter for post-processing proof nodes * by replacing internal rules by the rules in the Lfsc calculus. */ -class LfscProofPostprocessCallback : public ProofNodeUpdaterCallback +class LfscProofPostprocessCallback : protected EnvObj, + public ProofNodeUpdaterCallback { public: - LfscProofPostprocessCallback(LfscNodeConverter& ltp, ProofNodeManager* pnm); + LfscProofPostprocessCallback(Env& env, LfscNodeConverter& ltp); /** * Initialize, called once for each new ProofNode to process. This initializes * static information to be used by successive calls to update. @@ -57,8 +59,6 @@ class LfscProofPostprocessCallback : public ProofNodeUpdaterCallback bool& continueUpdate) override; private: - /** The proof node manager */ - ProofNodeManager* d_pnm; /** The proof checker of d_pnm **/ ProofChecker* d_pc; /** The term processor */ @@ -84,18 +84,16 @@ class LfscProofPostprocessCallback : public ProofNodeUpdaterCallback * The proof postprocessor module. This postprocesses a proof node into one * using the rules from the Lfsc calculus. */ -class LfscProofPostprocess +class LfscProofPostprocess : protected EnvObj { public: - LfscProofPostprocess(LfscNodeConverter& ltp, ProofNodeManager* pnm); + LfscProofPostprocess(Env& env, LfscNodeConverter& ltp); /** post-process */ void process(std::shared_ptr pf); private: /** The post process callback */ std::unique_ptr d_cb; - /** The proof node manager */ - ProofNodeManager* d_pnm; }; } // namespace proof diff --git a/src/proof/proof.cpp b/src/proof/proof.cpp index 4b2107bae..97d448a8a 100644 --- a/src/proof/proof.cpp +++ b/src/proof/proof.cpp @@ -18,16 +18,17 @@ #include "proof/proof_checker.h" #include "proof/proof_node.h" #include "proof/proof_node_manager.h" +#include "smt/env.h" using namespace cvc5::internal::kind; namespace cvc5::internal { -CDProof::CDProof(ProofNodeManager* pnm, +CDProof::CDProof(Env& env, context::Context* c, const std::string& name, bool autoSymm) - : d_manager(pnm), + : EnvObj(env), d_context(), d_nodes(c ? c : &d_context), d_name(name), @@ -47,8 +48,9 @@ std::shared_ptr CDProof::getProofFor(Node fact) // add as assumption std::vector pargs = {fact}; std::vector> passume; + ProofNodeManager* pnm = getManager(); std::shared_ptr pfa = - d_manager->mkNode(PfRule::ASSUME, passume, pargs, fact); + pnm->mkNode(PfRule::ASSUME, passume, pargs, fact); d_nodes.insert(fact, pfa); return pfa; } @@ -94,10 +96,11 @@ std::shared_ptr CDProof::getProofSymm(Node fact) std::vector> pschild; pschild.push_back(pfs); std::vector args; + ProofNodeManager* pnm = getManager(); if (pf == nullptr) { Trace("cdproof") << "...fresh make symm" << std::endl; - std::shared_ptr psym = d_manager->mkSymm(pfs, fact); + std::shared_ptr psym = pnm->mkSymm(pfs, fact); Assert(psym != nullptr); d_nodes.insert(fact, psym); return psym; @@ -107,7 +110,7 @@ std::shared_ptr CDProof::getProofSymm(Node fact) // if its not an assumption, make the connection Trace("cdproof") << "...update symm" << std::endl; // update pf - bool sret = d_manager->updateNode(pf.get(), PfRule::SYMM, pschild, args); + bool sret = pnm->updateNode(pf.get(), PfRule::SYMM, pschild, args); AlwaysAssert(sret); } } @@ -151,6 +154,7 @@ bool CDProof::addStep(Node expected, // we will overwrite the existing proof node by updating its contents below } // collect the child proofs, for each premise + ProofNodeManager* pnm = getManager(); std::vector> pchildren; for (const Node& c : children) { @@ -168,7 +172,7 @@ bool CDProof::addStep(Node expected, // otherwise, we initialize it as an assumption std::vector pcargs = {c}; std::vector> pcassume; - pc = d_manager->mkNode(PfRule::ASSUME, pcassume, pcargs, c); + pc = pnm->mkNode(PfRule::ASSUME, pcassume, pcargs, c); // assumptions never fail to check Assert(pc != nullptr); d_nodes.insert(c, pc); @@ -194,7 +198,7 @@ bool CDProof::addStep(Node expected, if (pprev == nullptr) { Trace("cdproof") << " new node " << expected << "..." << std::endl; - pthis = d_manager->mkNode(id, pchildren, args, expected); + pthis = pnm->mkNode(id, pchildren, args, expected); if (pthis == nullptr) { // failed to construct the node, perhaps due to a proof checking failure @@ -211,7 +215,7 @@ bool CDProof::addStep(Node expected, // We return the value of updateNode here. This means this method may return // false if this call failed, regardless of whether we already have a proof // step for expected. - ret = d_manager->updateNode(pthis.get(), id, pchildren, args); + ret = pnm->updateNode(pthis.get(), id, pchildren, args); } if (ret) { @@ -316,8 +320,9 @@ bool CDProof::addProof(std::shared_ptr pn, // checker than the one of the manager in this class, then it is double // checked here, so that this class maintains the invariant that all of // its nodes in d_nodes have been checked by the underlying checker. - Assert(d_manager->getChecker() == nullptr - || d_manager->getChecker()->check(pn.get(), curFact) == curFact); + Assert(getManager()->getChecker() == nullptr + || getManager()->getChecker()->check(pn.get(), curFact) + == curFact); // just store the proof for fact d_nodes.insert(curFact, pn); } @@ -326,7 +331,7 @@ bool CDProof::addProof(std::shared_ptr pn, // We update cur to have the structure of the top node of pn. Notice that // the interface to update this node will ensure that the proof apf is a // proof of the assumption. If it does not, then pn was wrong. - if (!d_manager->updateNode( + if (!getManager()->updateNode( cur.get(), pn->getRule(), pn->getChildren(), pn->getArguments())) { return false; @@ -410,7 +415,12 @@ bool CDProof::hasStep(Node fact) size_t CDProof::getNumProofNodes() const { return d_nodes.size(); } -ProofNodeManager* CDProof::getManager() const { return d_manager; } +ProofNodeManager* CDProof::getManager() const +{ + ProofNodeManager* pnm = d_env.getProofNodeManager(); + Assert(pnm != nullptr); + return pnm; +} bool CDProof::shouldOverwrite(ProofNode* pn, PfRule newId, CDPOverwrite opol) { diff --git a/src/proof/proof.h b/src/proof/proof.h index 4335858ba..72de97c87 100644 --- a/src/proof/proof.h +++ b/src/proof/proof.h @@ -24,6 +24,7 @@ #include "expr/node.h" #include "proof/proof_generator.h" #include "proof/proof_step_buffer.h" +#include "smt/env_obj.h" namespace cvc5::internal { @@ -132,7 +133,7 @@ class ProofNodeManager; * of ID_2. More generally, CDProof::isSame(F,G) returns true if F and G are * essentially the same formula according to this class. */ -class CDProof : public ProofGenerator +class CDProof : protected EnvObj, public ProofGenerator { public: /** @@ -142,7 +143,7 @@ class CDProof : public ProofGenerator * @param autoSymm Whether this proof automatically adds symmetry steps based * on policy documented above. */ - CDProof(ProofNodeManager* pnm, + CDProof(Env& env, context::Context* c = nullptr, const std::string& name = "CDProof", bool autoSymm = true); @@ -249,8 +250,6 @@ class CDProof : public ProofGenerator protected: typedef context::CDHashMap> NodeProofNodeMap; - /** The proof manager, used for allocating new ProofNode objects */ - ProofNodeManager* d_manager; /** A dummy context used by this class if none is provided */ context::Context d_context; /** The nodes of the proof */ diff --git a/src/proof/proof_ensure_closed.cpp b/src/proof/proof_ensure_closed.cpp index 329bbb402..398b115b0 100644 --- a/src/proof/proof_ensure_closed.cpp +++ b/src/proof/proof_ensure_closed.cpp @@ -29,7 +29,8 @@ namespace cvc5::internal { * Ensure closed with respect to assumptions, internal version, which * generalizes the check for a proof generator or a proof node. */ -void ensureClosedWrtInternal(Node proven, +void ensureClosedWrtInternal(const Options& opts, + Node proven, ProofGenerator* pg, ProofNode* pnp, const std::vector& assumps, @@ -37,13 +38,13 @@ void ensureClosedWrtInternal(Node proven, const char* ctx, bool reqGen) { - if (!options::produceProofs()) + if (!opts.smt.produceProofs) { // proofs not enabled, do not do check return; } bool isTraceDebug = TraceIsOn(c); - if (options::proofCheck() != options::ProofCheckMode::EAGER && !isTraceDebug) + if (opts.proof.proofCheck != options::ProofCheckMode::EAGER && !isTraceDebug) { // trace is off and proof new eager checking is off, do not do check return; @@ -143,7 +144,8 @@ void ensureClosedWrtInternal(Node proven, Trace(c) << "====" << std::endl; } -void pfgEnsureClosed(Node proven, +void pfgEnsureClosed(const Options& opts, + Node proven, ProofGenerator* pg, const char* c, const char* ctx, @@ -152,10 +154,11 @@ void pfgEnsureClosed(Node proven, Assert(!proven.isNull()); // proof generator may be null std::vector assumps; - ensureClosedWrtInternal(proven, pg, nullptr, assumps, c, ctx, reqGen); + ensureClosedWrtInternal(opts, proven, pg, nullptr, assumps, c, ctx, reqGen); } -void pfgEnsureClosedWrt(Node proven, +void pfgEnsureClosedWrt(const Options& opts, + Node proven, ProofGenerator* pg, const std::vector& assumps, const char* c, @@ -164,20 +167,25 @@ void pfgEnsureClosedWrt(Node proven, { Assert(!proven.isNull()); // proof generator may be null - ensureClosedWrtInternal(proven, pg, nullptr, assumps, c, ctx, reqGen); + ensureClosedWrtInternal(opts, proven, pg, nullptr, assumps, c, ctx, reqGen); } -void pfnEnsureClosed(ProofNode* pn, const char* c, const char* ctx) +void pfnEnsureClosed(const Options& opts, + ProofNode* pn, + const char* c, + const char* ctx) { - ensureClosedWrtInternal(Node::null(), nullptr, pn, {}, c, ctx, false); + ensureClosedWrtInternal(opts, Node::null(), nullptr, pn, {}, c, ctx, false); } -void pfnEnsureClosedWrt(ProofNode* pn, +void pfnEnsureClosedWrt(const Options& opts, + ProofNode* pn, const std::vector& assumps, const char* c, const char* ctx) { - ensureClosedWrtInternal(Node::null(), nullptr, pn, assumps, c, ctx, false); + ensureClosedWrtInternal( + opts, Node::null(), nullptr, pn, assumps, c, ctx, false); } } // namespace cvc5::internal diff --git a/src/proof/proof_ensure_closed.h b/src/proof/proof_ensure_closed.h index 84b230872..0e683660b 100644 --- a/src/proof/proof_ensure_closed.h +++ b/src/proof/proof_ensure_closed.h @@ -22,6 +22,7 @@ namespace cvc5::internal { +class Options; class ProofGenerator; class ProofNode; @@ -33,7 +34,8 @@ class ProofNode; * * @param reqGen Whether we consider a null generator to be a failure. */ -void pfgEnsureClosed(Node proven, +void pfgEnsureClosed(const Options& opts, + Node proven, ProofGenerator* pg, const char* c, const char* ctx, @@ -47,7 +49,8 @@ void pfgEnsureClosed(Node proven, * * @param reqGen Whether we consider a null generator to be a failure. */ -void pfgEnsureClosedWrt(Node proven, +void pfgEnsureClosedWrt(const Options& opts, + Node proven, ProofGenerator* pg, const std::vector& assumps, const char* c, @@ -59,12 +62,16 @@ void pfgEnsureClosedWrt(Node proven, * assertion failure if pn is not closed. Detailed information is printed * on trace c. Context ctx is a string used for debugging. */ -void pfnEnsureClosed(ProofNode* pn, const char* c, const char* ctx); +void pfnEnsureClosed(const Options& opts, + ProofNode* pn, + const char* c, + const char* ctx); /** * Same as above, but throws an assertion failure only if the free assumptions * of pn are not contained in assumps. */ -void pfnEnsureClosedWrt(ProofNode* pn, +void pfnEnsureClosedWrt(const Options& opts, + ProofNode* pn, const std::vector& assumps, const char* c, const char* ctx); diff --git a/src/proof/proof_node_updater.cpp b/src/proof/proof_node_updater.cpp index 464b3030a..e9c4fa82f 100644 --- a/src/proof/proof_node_updater.cpp +++ b/src/proof/proof_node_updater.cpp @@ -19,6 +19,7 @@ #include "proof/proof_ensure_closed.h" #include "proof/proof_node_algorithm.h" #include "proof/proof_node_manager.h" +#include "smt/env.h" namespace cvc5::internal { @@ -50,11 +51,11 @@ bool ProofNodeUpdaterCallback::updatePost(Node res, return false; } -ProofNodeUpdater::ProofNodeUpdater(ProofNodeManager* pnm, +ProofNodeUpdater::ProofNodeUpdater(Env& env, ProofNodeUpdaterCallback& cb, bool mergeSubproofs, bool autoSym) - : d_pnm(pnm), + : EnvObj(env), d_cb(cb), d_debugFreeAssumps(false), d_mergeSubproofs(mergeSubproofs), @@ -111,6 +112,8 @@ void ProofNodeUpdater::processInternal(std::shared_ptr pf, visit.push_back(pf); std::map>::iterator itc; Node res; + ProofNodeManager* pnm = d_env.getProofNodeManager(); + Assert(pnm != nullptr); do { cur = visit.back(); @@ -126,7 +129,7 @@ void ProofNodeUpdater::processInternal(std::shared_ptr pf, { // already have a proof, merge it into this one visited[cur] = true; - d_pnm->updateNode(cur.get(), itc->second.get()); + pnm->updateNode(cur.get(), itc->second.get()); // does not contain free assumptions since the range of resCache does // not contain free assumptions cfaMap[cur.get()] = false; @@ -200,7 +203,7 @@ bool ProofNodeUpdater::updateProofNode(std::shared_ptr cur, { PfRule id = cur->getRule(); // use CDProof to open a scope for which the callback updates - CDProof cpf(d_pnm, nullptr, "ProofNodeUpdater::CDProof", d_autoSym); + CDProof cpf(d_env, nullptr, "ProofNodeUpdater::CDProof", d_autoSym); const std::vector>& cc = cur->getChildren(); std::vector ccn; for (const std::shared_ptr& cp : cc) @@ -227,7 +230,7 @@ bool ProofNodeUpdater::updateProofNode(std::shared_ptr cur, } // then, update the original proof node based on this one Trace("pf-process-debug") << "Update node..." << std::endl; - d_pnm->updateNode(cur.get(), npn.get()); + d_env.getProofNodeManager()->updateNode(cur.get(), npn.get()); Trace("pf-process-debug") << "...update node finished." << std::endl; if (d_debugFreeAssumps) { @@ -236,8 +239,11 @@ bool ProofNodeUpdater::updateProofNode(std::shared_ptr cur, // the proof. We can now debug based on the expected set of free // assumptions. Trace("pfnu-debug") << "Ensure updated closed..." << std::endl; - pfnEnsureClosedWrt( - npn.get(), fullFa, "pfnu-debug", "ProofNodeUpdater:postupdate"); + pfnEnsureClosedWrt(options(), + npn.get(), + fullFa, + "pfnu-debug", + "ProofNodeUpdater:postupdate"); } Trace("pf-process-debug") << "..finished" << std::endl; return true; @@ -286,9 +292,10 @@ void ProofNodeUpdater::runFinalize( resCacheNcWaiting.find(res); if (itnw != resCacheNcWaiting.end()) { + ProofNodeManager* pnm = d_env.getProofNodeManager(); for (std::shared_ptr& ncp : itnw->second) { - d_pnm->updateNode(ncp.get(), cur.get()); + pnm->updateNode(ncp.get(), cur.get()); } resCacheNcWaiting.erase(res); } @@ -305,7 +312,7 @@ void ProofNodeUpdater::runFinalize( // assumptions. Trace("pfnu-debug") << "Ensure update closed..." << std::endl; pfnEnsureClosedWrt( - cur.get(), fa, "pfnu-debug", "ProofNodeUpdater:finalize"); + options(), cur.get(), fa, "pfnu-debug", "ProofNodeUpdater:finalize"); } } diff --git a/src/proof/proof_node_updater.h b/src/proof/proof_node_updater.h index 690ccabfa..2724bcb29 100644 --- a/src/proof/proof_node_updater.h +++ b/src/proof/proof_node_updater.h @@ -23,6 +23,7 @@ #include "expr/node.h" #include "proof/proof_node.h" +#include "smt/env_obj.h" namespace cvc5::internal { @@ -94,18 +95,18 @@ class ProofNodeUpdaterCallback * should be filled in the callback for each ProofNode to update. This update * process is applied in a *pre-order* traversal. */ -class ProofNodeUpdater +class ProofNodeUpdater : protected EnvObj { public: /** - * @param pnm The proof node manager we are using + * @param env Reference to the environment * @param cb The callback to apply to each node * @param mergeSubproofs Whether to automatically merge subproofs within * the same SCOPE that prove the same fact. * @param autoSym Whether intermediate CDProof objects passed to updater * callbacks automatically introduce SYMM steps. */ - ProofNodeUpdater(ProofNodeManager* pnm, + ProofNodeUpdater(Env& env, ProofNodeUpdaterCallback& cb, bool mergeSubproofs = false, bool autoSym = true); @@ -125,8 +126,6 @@ class ProofNodeUpdater void setDebugFreeAssumptions(const std::vector& freeAssumps); private: - /** The proof node manager */ - ProofNodeManager* d_pnm; /** The callback */ ProofNodeUpdaterCallback& d_cb; /** diff --git a/src/proof/proof_set.h b/src/proof/proof_set.h index b54e82eb1..3a4796bfa 100644 --- a/src/proof/proof_set.h +++ b/src/proof/proof_set.h @@ -22,10 +22,11 @@ #include "context/cdlist.h" #include "context/context.h" -#include "proof/proof_node_manager.h" namespace cvc5::internal { +class Env; + /** * A (context-dependent) set of proofs, which is used for memory * management purposes. @@ -34,10 +35,8 @@ template class CDProofSet { public: - CDProofSet(ProofNodeManager* pnm, - context::Context* c, - std::string namePrefix = "Proof") - : d_pnm(pnm), d_proofs(c), d_namePrefix(namePrefix) + CDProofSet(Env& env, context::Context* c, std::string namePrefix = "Proof") + : d_env(env), d_proofs(c), d_namePrefix(namePrefix) { } /** @@ -56,15 +55,15 @@ class CDProofSet T* allocateProof(Args&&... args) { d_proofs.push_back(std::make_shared( - d_pnm, + d_env, std::forward(args)..., d_namePrefix + "_" + std::to_string(d_proofs.size()))); return d_proofs.back().get(); } protected: - /** The proof node manager */ - ProofNodeManager* d_pnm; + /** Reference to env */ + Env& d_env; /** A context-dependent list of lazy proofs. */ context::CDList> d_proofs; /** The name prefix of the lazy proofs */ diff --git a/src/proof/trust_node.cpp b/src/proof/trust_node.cpp index d32ce1107..56cab5ce5 100644 --- a/src/proof/trust_node.cpp +++ b/src/proof/trust_node.cpp @@ -128,11 +128,12 @@ Node TrustNode::getPropExpProven(TNode lit, Node exp) Node TrustNode::getRewriteProven(TNode n, Node nr) { return n.eqNode(nr); } -void TrustNode::debugCheckClosed(const char* c, +void TrustNode::debugCheckClosed(const Options& opts, + const char* c, const char* ctx, bool reqNullGen) { - pfgEnsureClosed(d_proven, d_gen, c, ctx, reqNullGen); + pfgEnsureClosed(opts, d_proven, d_gen, c, ctx, reqNullGen); } std::string TrustNode::identifyGenerator() const diff --git a/src/proof/trust_node.h b/src/proof/trust_node.h index 86c69832b..0a72cb8e7 100644 --- a/src/proof/trust_node.h +++ b/src/proof/trust_node.h @@ -22,6 +22,7 @@ namespace cvc5::internal { +class Options; class ProofGenerator; class ProofNode; @@ -152,7 +153,10 @@ class TrustNode * * @param reqNullGen Whether we consider a null generator to be a failure. */ - void debugCheckClosed(const char* c, const char* ctx, bool reqNullGen = true); + void debugCheckClosed(const Options& opts, + const char* c, + const char* ctx, + bool reqNullGen = true); private: TrustNode(TrustNodeKind tnk, Node p, ProofGenerator* g = nullptr); diff --git a/src/prop/proof_cnf_stream.cpp b/src/prop/proof_cnf_stream.cpp index 939e78f34..3457ca9cc 100644 --- a/src/prop/proof_cnf_stream.cpp +++ b/src/prop/proof_cnf_stream.cpp @@ -29,10 +29,7 @@ ProofCnfStream::ProofCnfStream(Env& env, : EnvObj(env), d_cnfStream(cnfStream), d_satPM(satPM), - d_proof(env.getProofNodeManager(), - nullptr, - userContext(), - "ProofCnfStream::LazyCDProof"), + d_proof(env, nullptr, userContext(), "ProofCnfStream::LazyCDProof"), d_blocked(userContext()), d_optClausesManager(userContext(), &d_proof, d_optClausesPfs) { diff --git a/src/prop/proof_post_processor.cpp b/src/prop/proof_post_processor.cpp index 4d3def85d..d6a2b1894 100644 --- a/src/prop/proof_post_processor.cpp +++ b/src/prop/proof_post_processor.cpp @@ -21,8 +21,8 @@ namespace cvc5::internal { namespace prop { ProofPostprocessCallback::ProofPostprocessCallback( - ProofNodeManager* pnm, ProofCnfStream* proofCnfStream) - : d_pnm(pnm), d_proofCnfStream(proofCnfStream) + Env& env, ProofCnfStream* proofCnfStream) + : EnvObj(env), d_proofCnfStream(proofCnfStream) { } @@ -94,9 +94,8 @@ bool ProofPostprocessCallback::update(Node res, return true; } -ProofPostproccess::ProofPostproccess(ProofNodeManager* pnm, - ProofCnfStream* proofCnfStream) - : d_cb(pnm, proofCnfStream), d_pnm(pnm) +ProofPostproccess::ProofPostproccess(Env& env, ProofCnfStream* proofCnfStream) + : EnvObj(env), d_cb(env, proofCnfStream) { } @@ -108,7 +107,7 @@ void ProofPostproccess::process(std::shared_ptr pf) // how to process, including how to process assumptions in pf. d_cb.initializeUpdate(); // now, process - ProofNodeUpdater updater(d_pnm, d_cb); + ProofNodeUpdater updater(d_env, d_cb); updater.process(pf); } diff --git a/src/prop/proof_post_processor.h b/src/prop/proof_post_processor.h index a649ec256..ee0858376 100644 --- a/src/prop/proof_post_processor.h +++ b/src/prop/proof_post_processor.h @@ -23,6 +23,7 @@ #include "proof/proof_node_updater.h" #include "prop/proof_cnf_stream.h" +#include "smt/env_obj.h" namespace cvc5::internal { @@ -34,11 +35,11 @@ namespace prop { * assertions and lemmas, with the CNF transformation of these formulas, while * expanding the generators of lemmas. */ -class ProofPostprocessCallback : public ProofNodeUpdaterCallback +class ProofPostprocessCallback : protected EnvObj, + public ProofNodeUpdaterCallback { public: - ProofPostprocessCallback(ProofNodeManager* pnm, - ProofCnfStream* proofCnfStream); + ProofPostprocessCallback(Env& env, ProofCnfStream* proofCnfStream); ~ProofPostprocessCallback() {} /** * Initialize, called once for each new ProofNode to process. This initializes @@ -74,8 +75,6 @@ class ProofPostprocessCallback : public ProofNodeUpdaterCallback bool& continueUpdate) override; private: - /** The proof node manager */ - ProofNodeManager* d_pnm; /** The cnf stream proof generator */ ProofCnfStream* d_proofCnfStream; //---------------------------------reset at the begining of each update @@ -89,10 +88,10 @@ class ProofPostprocessCallback : public ProofNodeUpdaterCallback * produced by the SAT solver. Its main task is to connect the refutation's * assumptions to the CNF transformation proof in ProofCnfStream. */ -class ProofPostproccess +class ProofPostproccess : protected EnvObj { public: - ProofPostproccess(ProofNodeManager* pnm, ProofCnfStream* proofCnfStream); + ProofPostproccess(Env& env, ProofCnfStream* proofCnfStream); ~ProofPostproccess(); /** post-process * @@ -104,8 +103,6 @@ class ProofPostproccess private: /** The post process callback */ ProofPostprocessCallback d_cb; - /** The proof node manager */ - ProofNodeManager* d_pnm; }; } // namespace prop diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index 74e78d14d..c0cfe866c 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -74,9 +74,7 @@ PropEngine::PropEngine(Env& env, TheoryEngine* te) d_satSolver(nullptr), d_cnfStream(nullptr), d_pfCnfStream(nullptr), - d_theoryLemmaPg(d_env.getProofNodeManager(), - d_env.getUserContext(), - "PropEngine::ThLemmaPg"), + d_theoryLemmaPg(d_env, d_env.getUserContext(), "PropEngine::ThLemmaPg"), d_ppm(nullptr), d_interrupted(false), d_assumptions(d_env.getUserContext()) @@ -127,7 +125,7 @@ PropEngine::PropEngine(Env& env, TheoryEngine* te) *d_cnfStream, static_cast(d_satSolver)->getProofManager())); d_ppm.reset( - new PropPfManager(userContext, pnm, d_satSolver, d_pfCnfStream.get())); + new PropPfManager(env, userContext, d_satSolver, d_pfCnfStream.get())); } } @@ -207,11 +205,13 @@ void PropEngine::assertLemma(TrustNode tlemma, theory::LemmaProperty p) { Assert(tplemma.getGenerator() != nullptr); // ensure closed, make the proof node eagerly here to debug - tplemma.debugCheckClosed("te-proof-debug", "TheoryEngine::lemma"); + tplemma.debugCheckClosed( + options(), "te-proof-debug", "TheoryEngine::lemma"); for (theory::SkolemLemma& lem : ppLemmas) { Assert(lem.d_lemma.getGenerator() != nullptr); - lem.d_lemma.debugCheckClosed("te-proof-debug", "TheoryEngine::lemma_new"); + lem.d_lemma.debugCheckClosed( + options(), "te-proof-debug", "TheoryEngine::lemma_new"); } } @@ -726,7 +726,7 @@ std::shared_ptr PropEngine::getRefutation() Assert(options().smt.unsatCoresMode == options::UnsatCoresMode::ASSUMPTIONS); std::vector core; getUnsatCore(core); - CDProof cdp(d_env.getProofNodeManager()); + CDProof cdp(d_env); Node fnode = NodeManager::currentNM()->mkConst(false); cdp.addStep(fnode, PfRule::SAT_REFUTATION, core, {}); return cdp.getProofFor(fnode); diff --git a/src/prop/prop_proof_manager.cpp b/src/prop/prop_proof_manager.cpp index 1ec69f784..1d4ef7724 100644 --- a/src/prop/prop_proof_manager.cpp +++ b/src/prop/prop_proof_manager.cpp @@ -19,16 +19,17 @@ #include "proof/proof_node_algorithm.h" #include "prop/prop_proof_manager.h" #include "prop/sat_solver.h" +#include "smt/env.h" namespace cvc5::internal { namespace prop { -PropPfManager::PropPfManager(context::UserContext* userContext, - ProofNodeManager* pnm, +PropPfManager::PropPfManager(Env& env, + context::UserContext* userContext, CDCLTSatSolverInterface* satSolver, ProofCnfStream* cnfProof) - : d_pnm(pnm), - d_pfpp(new ProofPostproccess(pnm, cnfProof)), + : EnvObj(env), + d_pfpp(new ProofPostproccess(env, cnfProof)), d_satSolver(satSolver), d_assertions(userContext) { @@ -60,8 +61,11 @@ void PropPfManager::checkProof(const context::CDList& assertions) d_assertions.push_back(assertion); } std::vector avec{d_assertions.begin(), d_assertions.end()}; - pfnEnsureClosedWrt( - conflictProof.get(), avec, "sat-proof", "PropPfManager::checkProof"); + pfnEnsureClosedWrt(options(), + conflictProof.get(), + avec, + "sat-proof", + "PropPfManager::checkProof"); } std::shared_ptr PropPfManager::getProof() diff --git a/src/prop/prop_proof_manager.h b/src/prop/prop_proof_manager.h index dfde1d00e..b51a4f53b 100644 --- a/src/prop/prop_proof_manager.h +++ b/src/prop/prop_proof_manager.h @@ -23,6 +23,7 @@ #include "proof/proof_node_manager.h" #include "prop/proof_post_processor.h" #include "prop/sat_proof_manager.h" +#include "smt/env_obj.h" namespace cvc5::internal { @@ -37,11 +38,11 @@ class CDCLTSatSolverInterface; * The expected proof to be built is a refutation proof with preprocessed * assertions as free assumptions. */ -class PropPfManager +class PropPfManager : protected EnvObj { public: - PropPfManager(context::UserContext* userContext, - ProofNodeManager* pnm, + PropPfManager(Env& env, + context::UserContext* userContext, CDCLTSatSolverInterface* satSolver, ProofCnfStream* cnfProof); @@ -76,8 +77,6 @@ class PropPfManager void checkProof(const context::CDList& assertions); private: - /** A node manager */ - ProofNodeManager* d_pnm; /** The proof post-processor */ std::unique_ptr d_pfpp; /** diff --git a/src/prop/sat_proof_manager.cpp b/src/prop/sat_proof_manager.cpp index c567c3190..9d3e89fb5 100644 --- a/src/prop/sat_proof_manager.cpp +++ b/src/prop/sat_proof_manager.cpp @@ -30,8 +30,8 @@ SatProofManager::SatProofManager(Env& env, : EnvObj(env), d_solver(solver), d_cnfStream(cnfStream), - d_resChains(d_env.getProofNodeManager(), true, userContext()), - d_resChainPg(userContext(), d_env.getProofNodeManager()), + d_resChains(d_env, true, userContext()), + d_resChainPg(d_env, userContext()), d_assumptions(userContext()), d_conflictLit(undefSatVariable), d_optResLevels(userContext()), diff --git a/src/prop/zero_level_learner.cpp b/src/prop/zero_level_learner.cpp index 9f2d79b63..13d60b672 100644 --- a/src/prop/zero_level_learner.cpp +++ b/src/prop/zero_level_learner.cpp @@ -351,7 +351,7 @@ bool ZeroLevelLearner::isLearnable(modes::LearnedLitType ltype) const bool ZeroLevelLearner::getSolved(const Node& lit, Subs& subs) { context::Context dummyContext; - theory::TrustSubstitutionMap subsOut(&dummyContext); + theory::TrustSubstitutionMap subsOut(d_env, &dummyContext); TrustNode tlit = TrustNode::mkTrustLemma(lit); theory::Theory::PPAssertStatus status = d_theoryEngine->solve(tlit, subsOut); if (status == theory::Theory::PP_ASSERT_STATUS_SOLVED) diff --git a/src/smt/env.cpp b/src/smt/env.cpp index 00a7a959c..1586d8ad5 100644 --- a/src/smt/env.cpp +++ b/src/smt/env.cpp @@ -45,7 +45,7 @@ Env::Env(NodeManager* nm, const Options* opts) d_rewriter(new theory::Rewriter()), d_evalRew(nullptr), d_eval(nullptr), - d_topLevelSubs(new theory::TrustSubstitutionMap(d_userContext.get())), + d_topLevelSubs(nullptr), d_logic(), d_statisticsRegistry(std::make_unique(*this)), d_options(), @@ -69,13 +69,16 @@ Env::Env(NodeManager* nm, const Options* opts) Env::~Env() {} -void Env::setProofNodeManager(ProofNodeManager* pnm) +void Env::finishInit(ProofNodeManager* pnm) { - Assert(pnm != nullptr); - Assert(d_proofNodeManager == nullptr); - d_proofNodeManager = pnm; - d_rewriter->setProofNodeManager(pnm); - d_topLevelSubs->setProofNodeManager(pnm); + if (pnm != nullptr) + { + Assert(d_proofNodeManager == nullptr); + d_proofNodeManager = pnm; + d_rewriter->finishInit(*this); + } + d_topLevelSubs.reset( + new theory::TrustSubstitutionMap(*this, d_userContext.get())); } void Env::shutdown() diff --git a/src/smt/env.h b/src/smt/env.h index 260407161..a42ad0341 100644 --- a/src/smt/env.h +++ b/src/smt/env.h @@ -267,7 +267,7 @@ class Env /* Private initialization ------------------------------------------------- */ /** Set proof node manager if it exists */ - void setProofNodeManager(ProofNodeManager* pnm); + void finishInit(ProofNodeManager* pnm); /* Private shutdown ------------------------------------------------------- */ /** diff --git a/src/smt/expand_definitions.cpp b/src/smt/expand_definitions.cpp index d9a61b73f..dcd390601 100644 --- a/src/smt/expand_definitions.cpp +++ b/src/smt/expand_definitions.cpp @@ -169,8 +169,7 @@ void ExpandDefs::enableProofs() // initialize if not done already if (d_tpg == nullptr) { - Assert(d_env.getProofNodeManager() != nullptr); - d_tpg.reset(new TConvProofGenerator(d_env.getProofNodeManager(), + d_tpg.reset(new TConvProofGenerator(d_env, d_env.getUserContext(), TConvPolicy::FIXPOINT, TConvCachePolicy::NEVER, diff --git a/src/smt/preprocess_proof_generator.cpp b/src/smt/preprocess_proof_generator.cpp index 2893ccb23..062c6a9dd 100644 --- a/src/smt/preprocess_proof_generator.cpp +++ b/src/smt/preprocess_proof_generator.cpp @@ -23,6 +23,7 @@ #include "proof/proof.h" #include "proof/proof_checker.h" #include "proof/proof_node.h" +#include "proof/proof_node_manager.h" #include "smt/env.h" #include "theory/quantifiers/extended_rewrite.h" @@ -34,8 +35,8 @@ PreprocessProofGenerator::PreprocessProofGenerator( : EnvObj(env), d_ctx(c ? c : &d_context), d_src(d_ctx), - d_helperProofs(env.getProofNodeManager(), d_ctx), - d_inputPf(env.getProofNodeManager(), c, "InputProof"), + d_helperProofs(env, d_ctx), + d_inputPf(env, c, "InputProof"), d_name(name), d_ra(ra), d_rpp(rpp) @@ -128,7 +129,7 @@ std::shared_ptr PreprocessProofGenerator::getProofFor(Node f) return nullptr; } // make CDProof to construct the proof below - CDProof cdp(d_env.getProofNodeManager()); + CDProof cdp(d_env); Node curr = f; std::vector transChildren; diff --git a/src/smt/proof_manager.cpp b/src/smt/proof_manager.cpp index 4099df771..482239a4d 100644 --- a/src/smt/proof_manager.cpp +++ b/src/smt/proof_manager.cpp @@ -48,8 +48,6 @@ PfManager::PfManager(Env& env) d_pfpp(nullptr), d_finalProof(nullptr) { - // enable proof support in the environment/rewriter - d_env.setProofNodeManager(d_pnm.get()); // now construct preprocess proof generator d_pppg = std::make_unique( env, env.getUserContext(), "smt::PreprocessProofGenerator"); @@ -185,7 +183,7 @@ void PfManager::printProof(std::ostream& out, { proof::AletheNodeConverter anc; proof::AletheProofPostprocess vpfpp( - d_pnm.get(), anc, options().proof.proofAletheResPivots); + d_env, anc, options().proof.proofAletheResPivots); vpfpp.process(fp); proof::AletheProofPrinter vpp; vpp.print(out, fp); @@ -195,7 +193,7 @@ void PfManager::printProof(std::ostream& out, std::vector assertions; getAssertions(as, assertions); proof::LfscNodeConverter ltp; - proof::LfscProofPostprocess lpp(ltp, d_pnm.get()); + proof::LfscProofPostprocess lpp(d_env, ltp); lpp.process(fp); proof::LfscPrinter lp(ltp); lp.print(out, assertions, fp.get()); @@ -250,7 +248,7 @@ void PfManager::translateDifficultyMap(std::map& dmap, Trace("difficulty-proc") << "Make SAT refutation" << std::endl; // assume a SAT refutation from all input assertions that were marked // as having a difficulty - CDProof cdp(d_pnm.get()); + CDProof cdp(d_env); Node fnode = NodeManager::currentNM()->mkConst(false); cdp.addStep(fnode, PfRule::SAT_REFUTATION, ppAsserts, {}); std::shared_ptr pf = cdp.getProofFor(fnode); @@ -263,7 +261,7 @@ void PfManager::translateDifficultyMap(std::map& dmap, Assert(fpf->getRule() == PfRule::SAT_REFUTATION); const std::vector>& children = fpf->getChildren(); DifficultyPostprocessCallback dpc; - ProofNodeUpdater dpnu(d_pnm.get(), dpc); + ProofNodeUpdater dpnu(d_env, dpc); Trace("difficulty-proc") << "Compute accumulated difficulty" << std::endl; // For each child of SAT_REFUTATION, we increment the difficulty on all // "source" free assumptions (see DifficultyPostprocessCallback) by the diff --git a/src/smt/proof_post_processor.cpp b/src/smt/proof_post_processor.cpp index 029bfdfcd..ca5cd2277 100644 --- a/src/smt/proof_post_processor.cpp +++ b/src/smt/proof_post_processor.cpp @@ -41,7 +41,6 @@ ProofPostprocessCallback::ProofPostprocessCallback(Env& env, rewriter::RewriteDb* rdb, bool updateScopedAssumptions) : EnvObj(env), - d_pnm(env.getProofNodeManager()), d_pppg(pppg), d_wfpm(env), d_updateScopedAssumptions(updateScopedAssumptions) @@ -316,6 +315,7 @@ Node ProofPostprocessCallback::eliminateCrowdingLits( std::vector childrenResArgs; Node resPlaceHolder; size_t nextGuardedElimPos = eliminators[0]; + ProofNodeManager* pnm = d_env.getProofNodeManager(); do { size_t start = lastElim + 1; @@ -333,11 +333,11 @@ Node ProofPostprocessCallback::eliminateCrowdingLits( args.begin() + (2 * end) + 1); Trace("smt-proof-pp-debug2") << "\tres children: " << childrenRes << "\n"; Trace("smt-proof-pp-debug2") << "\tres args: " << childrenResArgs << "\n"; - resPlaceHolder = d_pnm->getChecker()->checkDebug(PfRule::CHAIN_RESOLUTION, - childrenRes, - childrenResArgs, - Node::null(), - ""); + resPlaceHolder = pnm->getChecker()->checkDebug(PfRule::CHAIN_RESOLUTION, + childrenRes, + childrenResArgs, + Node::null(), + ""); Trace("smt-proof-pp-debug2") << "resPlaceHorder: " << resPlaceHolder << "\n"; Trace("smt-proof-pp-debug2") << "-------\n"; @@ -347,7 +347,7 @@ Node ProofPostprocessCallback::eliminateCrowdingLits( // to be handled by the caller if (end < children.size() - 1) { - lastClause = d_pnm->getChecker()->checkDebug( + lastClause = pnm->getChecker()->checkDebug( PfRule::FACTORING, {resPlaceHolder}, {}, Node::null(), ""); if (!lastClause.isNull()) { @@ -666,9 +666,10 @@ Node ProofPostprocessCallback::expandMacros(PfRule id, else if (id == PfRule::MACRO_RESOLUTION || id == PfRule::MACRO_RESOLUTION_TRUST) { + ProofNodeManager* pnm = d_env.getProofNodeManager(); // first generate the naive chain_resolution std::vector chainResArgs{args.begin() + 1, args.end()}; - Node chainConclusion = d_pnm->getChecker()->checkDebug( + Node chainConclusion = pnm->getChecker()->checkDebug( PfRule::CHAIN_RESOLUTION, children, chainResArgs, Node::null(), ""); Trace("smt-proof-pp-debug") << "Original conclusion: " << args[0] << "\n"; Trace("smt-proof-pp-debug") @@ -886,10 +887,10 @@ Node ProofPostprocessCallback::expandMacros(PfRule id, << "......updated to " << var << " -> " << ss << " based on previous substitution" << std::endl; // make the proof for the tranitivity step - std::shared_ptr pf = std::make_shared(d_pnm); + std::shared_ptr pf = std::make_shared(d_env); pfs.push_back(pf); // prove the updated substitution - TConvProofGenerator tcg(d_pnm, + TConvProofGenerator tcg(d_env, nullptr, TConvPolicy::ONCE, TConvCachePolicy::NEVER, @@ -934,7 +935,7 @@ Node ProofPostprocessCallback::expandMacros(PfRule id, // should be implied by the substitution now TConvPolicy tcpolicy = ida == MethodId::SBA_FIXPOINT ? TConvPolicy::FIXPOINT : TConvPolicy::ONCE; - TConvProofGenerator tcpg(d_pnm, + TConvProofGenerator tcpg(d_env, nullptr, tcpolicy, TConvCachePolicy::NEVER, @@ -1082,9 +1083,10 @@ Node ProofPostprocessCallback::expandMacros(PfRule id, Assert(!args.empty()); Node eq = args[0]; Assert(eq.getKind() == EQUAL); + ProofNodeManager* pnm = d_env.getProofNodeManager(); // try to replay theory rewrite // first, check that maybe its just an evaluation step - ProofChecker* pc = d_pnm->getChecker(); + ProofChecker* pc = pnm->getChecker(); Node ceval = pc->checkDebug(PfRule::EVALUATE, {}, {eq[0]}, eq, "smt-proof-pp-debug"); if (!ceval.isNull() && ceval == eq) @@ -1107,8 +1109,9 @@ Node ProofPostprocessCallback::expandMacros(PfRule id, Trace("macro::arith") << " args: " << args << std::endl; } Assert(args.size() == children.size()); + ProofNodeManager* pnm = d_env.getProofNodeManager(); NodeManager* nm = NodeManager::currentNM(); - ProofStepBuffer steps{d_pnm->getChecker()}; + ProofStepBuffer steps{pnm->getChecker()}; // Scale all children, accumulating std::vector scaledRels; @@ -1164,7 +1167,7 @@ Node ProofPostprocessCallback::expandMacros(PfRule id, } else if (id == PfRule::BV_BITBLAST) { - bv::BBProof bb(d_env, nullptr, d_pnm, true); + bv::BBProof bb(d_env, nullptr, true); Node eq = args[0]; Assert(eq.getKind() == EQUAL); bb.bbAtom(eq[0]); @@ -1267,9 +1270,9 @@ ProofPostproccess::ProofPostproccess(Env& env, : EnvObj(env), d_cb(env, pppg, rdb, updateScopedAssumptions), // the update merges subproofs - d_updater(env.getProofNodeManager(), d_cb, options().proof.proofPpMerge), + d_updater(env, d_cb, options().proof.proofPpMerge), d_finalCb(env), - d_finalizer(env.getProofNodeManager(), d_finalCb) + d_finalizer(env, d_finalCb) { } diff --git a/src/smt/proof_post_processor.h b/src/smt/proof_post_processor.h index 0ee7c31fa..4337b377e 100644 --- a/src/smt/proof_post_processor.h +++ b/src/smt/proof_post_processor.h @@ -76,8 +76,6 @@ class ProofPostprocessCallback : public ProofNodeUpdaterCallback, protected EnvO private: /** Common constants */ Node d_true; - /** Pointer to the proof node manager */ - ProofNodeManager* d_pnm; /** The preprocessing proof generator */ ProofGenerator* d_pppg; /** The witness form proof generator */ diff --git a/src/smt/solver_engine.cpp b/src/smt/solver_engine.cpp index 876f475ff..e6a804653 100644 --- a/src/smt/solver_engine.cpp +++ b/src/smt/solver_engine.cpp @@ -188,6 +188,7 @@ void SolverEngine::finishInit() SetDefaults sdefaults(*d_env, d_isInternalSubsolver); sdefaults.setDefaults(d_env->d_logic, getOptions()); + ProofNodeManager* pnm = nullptr; if (d_env->getOptions().smt.produceProofs) { // ensure bound variable uses canonical bound variables @@ -201,7 +202,10 @@ void SolverEngine::finishInit() d_asserts->enableProofs(pppg); // enabled proofs in the preprocessor d_smtSolver->getPreprocessor()->enableProofs(pppg); + pnm = d_pfManager->getProofNodeManager(); } + // enable proof support in the environment/rewriter + d_env->finishInit(pnm); Trace("smt-debug") << "SolverEngine::finishInit" << std::endl; d_smtSolver->finishInit(); diff --git a/src/smt/term_formula_removal.cpp b/src/smt/term_formula_removal.cpp index 967c1fcf9..f4f15f8e3 100644 --- a/src/smt/term_formula_removal.cpp +++ b/src/smt/term_formula_removal.cpp @@ -42,20 +42,20 @@ RemoveTermFormulas::RemoveTermFormulas(Env& env) if (pnm != nullptr) { d_tpg.reset( - new TConvProofGenerator(pnm, + new TConvProofGenerator(env, nullptr, TConvPolicy::FIXPOINT, TConvCachePolicy::NEVER, "RemoveTermFormulas::TConvProofGenerator", &d_rtfc)); d_tpgi.reset( - new TConvProofGenerator(pnm, + new TConvProofGenerator(env, nullptr, TConvPolicy::ONCE, TConvCachePolicy::NEVER, "RemoveTermFormulas::TConvProofGenerator")); d_lp.reset(new LazyCDProof( - pnm, nullptr, nullptr, "RemoveTermFormulas::LazyCDProof")); + env, nullptr, nullptr, "RemoveTermFormulas::LazyCDProof")); } } @@ -475,8 +475,8 @@ Node RemoveTermFormulas::runCurrentInternal(TNode node, newLem = TrustNode::mkTrustLemma(newAssertion, d_lp.get()); Trace("rtf-proof-debug") << "Checking closed..." << std::endl; - newLem.debugCheckClosed("rtf-proof-debug", - "RemoveTermFormulas::run:new_assert"); + newLem.debugCheckClosed( + options(), "rtf-proof-debug", "RemoveTermFormulas::run:new_assert"); } // The representation is now the skolem diff --git a/src/smt/witness_form.cpp b/src/smt/witness_form.cpp index 36dc798cf..172a9d8ef 100644 --- a/src/smt/witness_form.cpp +++ b/src/smt/witness_form.cpp @@ -24,19 +24,15 @@ namespace smt { WitnessFormGenerator::WitnessFormGenerator(Env& env) : d_rewriter(env.getRewriter()), - d_tcpg(env.getProofNodeManager(), + d_tcpg(env, nullptr, TConvPolicy::FIXPOINT, TConvCachePolicy::NEVER, "WfGenerator::TConvProofGenerator", nullptr, true), - d_wintroPf(env.getProofNodeManager(), - nullptr, - nullptr, - "WfGenerator::LazyCDProof"), - d_pskPf( - env.getProofNodeManager(), nullptr, "WfGenerator::PurifySkolemProof") + d_wintroPf(env, nullptr, nullptr, "WfGenerator::LazyCDProof"), + d_pskPf(env, nullptr, "WfGenerator::PurifySkolemProof") { } diff --git a/src/theory/arith/branch_and_bound.cpp b/src/theory/arith/branch_and_bound.cpp index d51652e8f..77bb2a958 100644 --- a/src/theory/arith/branch_and_bound.cpp +++ b/src/theory/arith/branch_and_bound.cpp @@ -31,14 +31,12 @@ namespace arith { BranchAndBound::BranchAndBound(Env& env, ArithState& s, InferenceManager& im, - PreprocessRewriteEq& ppre, - ProofNodeManager* pnm) + PreprocessRewriteEq& ppre) : EnvObj(env), d_astate(s), d_im(im), d_ppre(ppre), - d_pfGen(new EagerProofGenerator(pnm, userContext())), - d_pnm(pnm) + d_pfGen(new EagerProofGenerator(env, userContext())) { } @@ -78,6 +76,7 @@ TrustNode BranchAndBound::branchIntegerVariable(TNode var, Rational value) Trace("integers") << "l: " << l << std::endl; if (proofsEnabled()) { + ProofNodeManager* pnm = d_env.getProofNodeManager(); Node less = nm->mkNode(LT, var, nm->mkConstInt(nearest)); Node greater = nm->mkNode(GT, var, nm->mkConstInt(nearest)); // TODO (project #37): justify. Thread proofs through *ensureLiteral*. @@ -86,30 +85,29 @@ TrustNode BranchAndBound::branchIntegerVariable(TNode var, Rational value) Trace("integers::pf") << "literal: " << literal << std::endl; Trace("integers::pf") << "eq: " << eq << std::endl; Trace("integers::pf") << "rawEq: " << rawEq << std::endl; - Pf pfNotLit = d_pnm->mkAssume(literal.negate()); + Pf pfNotLit = pnm->mkAssume(literal.negate()); // rewrite notLiteral to notRawEq, using teq. Pf pfNotRawEq = literal == rawEq ? pfNotLit - : d_pnm->mkNode( - PfRule::MACRO_SR_PRED_TRANSFORM, - {pfNotLit, - teq.getGenerator()->getProofFor(teq.getProven())}, - {rawEq.negate()}); - Pf pfBot = d_pnm->mkNode( - PfRule::CONTRA, - {d_pnm->mkNode(PfRule::ARITH_TRICHOTOMY, - {d_pnm->mkAssume(less.negate()), pfNotRawEq}, - {greater}), - d_pnm->mkAssume(greater.negate())}, - {}); + : pnm->mkNode( + PfRule::MACRO_SR_PRED_TRANSFORM, + {pfNotLit, teq.getGenerator()->getProofFor(teq.getProven())}, + {rawEq.negate()}); + Pf pfBot = + pnm->mkNode(PfRule::CONTRA, + {pnm->mkNode(PfRule::ARITH_TRICHOTOMY, + {pnm->mkAssume(less.negate()), pfNotRawEq}, + {greater}), + pnm->mkAssume(greater.negate())}, + {}); std::vector assumptions = { literal.negate(), less.negate(), greater.negate()}; // Proof of (not (and (not (= v i)) (not (< v i)) (not (> v i)))) - Pf pfNotAnd = d_pnm->mkScope(pfBot, assumptions); - Pf pfL = d_pnm->mkNode(PfRule::MACRO_SR_PRED_TRANSFORM, - {d_pnm->mkNode(PfRule::NOT_AND, {pfNotAnd}, {})}, - {l}); + Pf pfNotAnd = pnm->mkScope(pfBot, assumptions); + Pf pfL = pnm->mkNode(PfRule::MACRO_SR_PRED_TRANSFORM, + {pnm->mkNode(PfRule::NOT_AND, {pfNotAnd}, {})}, + {l}); lem = d_pfGen->mkTrustNode(l, pfL); } else @@ -136,7 +134,10 @@ TrustNode BranchAndBound::branchIntegerVariable(TNode var, Rational value) return lem; } -bool BranchAndBound::proofsEnabled() const { return d_pnm != nullptr; } +bool BranchAndBound::proofsEnabled() const +{ + return d_env.isTheoryProofProducing(); +} } // namespace arith } // namespace theory diff --git a/src/theory/arith/branch_and_bound.h b/src/theory/arith/branch_and_bound.h index bb7e2140a..8c7859d93 100644 --- a/src/theory/arith/branch_and_bound.h +++ b/src/theory/arith/branch_and_bound.h @@ -44,8 +44,7 @@ class BranchAndBound : protected EnvObj BranchAndBound(Env& env, ArithState& s, InferenceManager& im, - PreprocessRewriteEq& ppre, - ProofNodeManager* pnm); + PreprocessRewriteEq& ppre); ~BranchAndBound() {} /** * Branch variable, called when integer var has given value @@ -64,8 +63,6 @@ class BranchAndBound : protected EnvObj PreprocessRewriteEq& d_ppre; /** Proof generator. */ std::unique_ptr d_pfGen; - /** Proof node manager */ - ProofNodeManager* d_pnm; }; } // namespace arith diff --git a/src/theory/arith/linear/congruence_manager.cpp b/src/theory/arith/linear/congruence_manager.cpp index bcceb37d0..a360485c4 100644 --- a/src/theory/arith/linear/congruence_manager.cpp +++ b/src/theory/arith/linear/congruence_manager.cpp @@ -59,10 +59,10 @@ ArithCongruenceManager::ArithCongruenceManager( // Construct d_pfGenEe with the SAT context, since its proof include // unclosed assumptions of theory literals. d_pfGenEe(new EagerProofGenerator( - d_pnm, context(), "ArithCongruenceManager::pfGenEe")), + d_env, context(), "ArithCongruenceManager::pfGenEe")), // Construct d_pfGenEe with the USER context, since its proofs are closed. d_pfGenExplain(new EagerProofGenerator( - d_pnm, userContext(), "ArithCongruenceManager::pfGenExplain")), + d_env, userContext(), "ArithCongruenceManager::pfGenExplain")), d_pfee(nullptr) { } diff --git a/src/theory/arith/linear/theory_arith_private.cpp b/src/theory/arith/linear/theory_arith_private.cpp index 697267f7a..8412eda19 100644 --- a/src/theory/arith/linear/theory_arith_private.cpp +++ b/src/theory/arith/linear/theory_arith_private.cpp @@ -95,7 +95,7 @@ TheoryArithPrivate::TheoryArithPrivate(TheoryArith& containing, d_pnm(d_env.isTheoryProofProducing() ? d_env.getProofNodeManager() : nullptr), d_checker(), - d_pfGen(new EagerProofGenerator(d_pnm, userContext())), + d_pfGen(new EagerProofGenerator(env, userContext())), d_constraintDatabase(d_env, d_partialModel, d_congruenceManager, diff --git a/src/theory/arith/nl/coverings/cdcac.cpp b/src/theory/arith/nl/coverings/cdcac.cpp index 24171c8a3..14fbe2f76 100644 --- a/src/theory/arith/nl/coverings/cdcac.cpp +++ b/src/theory/arith/nl/coverings/cdcac.cpp @@ -49,8 +49,7 @@ CDCAC::CDCAC(Env& env, const std::vector& ordering) { if (d_env.isTheoryProofProducing()) { - d_proof.reset( - new CoveringsProofGenerator(userContext(), d_env.getProofNodeManager())); + d_proof.reset(new CoveringsProofGenerator(env, userContext())); } } diff --git a/src/theory/arith/nl/coverings/proof_generator.cpp b/src/theory/arith/nl/coverings/proof_generator.cpp index 53a9f0c91..9931e71fc 100644 --- a/src/theory/arith/nl/coverings/proof_generator.cpp +++ b/src/theory/arith/nl/coverings/proof_generator.cpp @@ -92,9 +92,9 @@ Node mkIRP(const Node& var, } // namespace -CoveringsProofGenerator::CoveringsProofGenerator(context::Context* ctx, - ProofNodeManager* pnm) - : d_pnm(pnm), d_proofs(pnm, ctx), d_current(nullptr) +CoveringsProofGenerator::CoveringsProofGenerator(Env& env, + context::Context* ctx) + : EnvObj(env), d_proofs(env, ctx), d_current(nullptr) { d_false = NodeManager::currentNM()->mkConst(false); d_zero = NodeManager::currentNM()->mkConstReal(Rational(0)); diff --git a/src/theory/arith/nl/coverings/proof_generator.h b/src/theory/arith/nl/coverings/proof_generator.h index f40136b14..35c2c9828 100644 --- a/src/theory/arith/nl/coverings/proof_generator.h +++ b/src/theory/arith/nl/coverings/proof_generator.h @@ -27,6 +27,7 @@ #include "expr/node.h" #include "proof/lazy_tree_proof_generator.h" #include "proof/proof_set.h" +#include "smt/env_obj.h" #include "theory/arith/nl/coverings/cdcac_utils.h" namespace cvc5::internal { @@ -50,12 +51,12 @@ namespace coverings { * It uses a LazyTreeProofGenerator internally to manage the tree-based proof * construction. */ -class CoveringsProofGenerator +class CoveringsProofGenerator : protected EnvObj { public: friend std::ostream& operator<<(std::ostream& os, const CoveringsProofGenerator& proof); - CoveringsProofGenerator(context::Context* ctx, ProofNodeManager* pnm); + CoveringsProofGenerator(Env& env, context::Context* ctx); /** Start a new proof in this proof generator */ void startNewProof(); @@ -130,8 +131,6 @@ class CoveringsProofGenerator VariableMapper& vm); private: - /** The proof node manager used for the proofs */ - ProofNodeManager* d_pnm; /** The list of generated proofs */ CDProofSet d_proofs; /** The current proof */ diff --git a/src/theory/arith/nl/ext/ext_state.cpp b/src/theory/arith/nl/ext/ext_state.cpp index 1ef35b66a..5cb837de6 100644 --- a/src/theory/arith/nl/ext/ext_state.cpp +++ b/src/theory/arith/nl/ext/ext_state.cpp @@ -32,18 +32,17 @@ namespace theory { namespace arith { namespace nl { -ExtState::ExtState(InferenceManager& im, NlModel& model, Env& env) - : d_im(im), d_model(model), d_env(env) +ExtState::ExtState(Env& env, InferenceManager& im, NlModel& model) + : EnvObj(env), d_im(im), d_model(model) { d_false = NodeManager::currentNM()->mkConst(false); d_true = NodeManager::currentNM()->mkConst(true); d_zero = NodeManager::currentNM()->mkConstInt(Rational(0)); d_one = NodeManager::currentNM()->mkConstInt(Rational(1)); d_neg_one = NodeManager::currentNM()->mkConstInt(Rational(-1)); - if (d_env.isTheoryProofProducing()) + if (env.isTheoryProofProducing()) { - d_proof.reset(new CDProofSet( - d_env.getProofNodeManager(), d_env.getUserContext(), "nl-ext")); + d_proof.reset(new CDProofSet(env, env.getUserContext(), "nl-ext")); } } diff --git a/src/theory/arith/nl/ext/ext_state.h b/src/theory/arith/nl/ext/ext_state.h index 7014aa3e4..1e438a9d5 100644 --- a/src/theory/arith/nl/ext/ext_state.h +++ b/src/theory/arith/nl/ext/ext_state.h @@ -36,9 +36,10 @@ namespace nl { class NlModel; -struct ExtState +class ExtState : protected EnvObj { - ExtState(InferenceManager& im, NlModel& model, Env& env); + public: + ExtState(Env& env, InferenceManager& im, NlModel& model); void init(const std::vector& xts); @@ -61,8 +62,6 @@ struct ExtState InferenceManager& d_im; /** Reference to the non-linear model object */ NlModel& d_model; - /** Reference to the environment */ - Env& d_env; /** * A CDProofSet that hands out CDProof objects for lemmas. */ diff --git a/src/theory/arith/nl/ext/factoring_check.h b/src/theory/arith/nl/ext/factoring_check.h index 1220010e4..63e30bf99 100644 --- a/src/theory/arith/nl/ext/factoring_check.h +++ b/src/theory/arith/nl/ext/factoring_check.h @@ -29,7 +29,7 @@ namespace theory { namespace arith { namespace nl { -struct ExtState; +class ExtState; class FactoringCheck : protected EnvObj { diff --git a/src/theory/arith/nl/ext/monomial_bounds_check.cpp b/src/theory/arith/nl/ext/monomial_bounds_check.cpp index 352f1e884..311119953 100644 --- a/src/theory/arith/nl/ext/monomial_bounds_check.cpp +++ b/src/theory/arith/nl/ext/monomial_bounds_check.cpp @@ -209,7 +209,7 @@ void MonomialBoundsCheck::checkBounds(const std::vector& asserts, } // compute if bound is not satisfied, and store what is required // for a possible refinement - if (d_data->d_env.getOptions().arith.nlExtTangentPlanes) + if (options().arith.nlExtTangentPlanes) { if (is_false_lit) { @@ -346,9 +346,7 @@ void MonomialBoundsCheck::checkBounds(const std::vector& asserts, : PfRule::ARITH_MULT_NEG, {}, {mult, simpleeq}); - theory::Rewriter* rew = d_data->d_env.getRewriter(); - if (type == Kind::EQUAL - && (rew->rewrite(simpleeq) != rew->rewrite(exp[1]))) + if (type == Kind::EQUAL && (rewrite(simpleeq) != rewrite(exp[1]))) { // it is not identical under rewriting and we need to do some work here // The proof looks like this: @@ -379,7 +377,7 @@ void MonomialBoundsCheck::checkBounds(const std::vector& asserts, {nm->mkConstInt(Rational(1))}); Node lb = nm->mkNode(Kind::GEQ, simpleeq[0], simpleeq[1]); Node rb = nm->mkNode(Kind::LEQ, simpleeq[0], simpleeq[1]); - if (rew->rewrite(lb) == rew->rewrite(exp[1][0])) + if (rewrite(lb) == rewrite(exp[1][0])) { proof->addStep( lb, PfRule::MACRO_SR_PRED_TRANSFORM, {exp[1][0]}, {lb}); diff --git a/src/theory/arith/nl/ext/monomial_bounds_check.h b/src/theory/arith/nl/ext/monomial_bounds_check.h index 6e9f3456e..ed2ab732c 100644 --- a/src/theory/arith/nl/ext/monomial_bounds_check.h +++ b/src/theory/arith/nl/ext/monomial_bounds_check.h @@ -25,7 +25,7 @@ namespace theory { namespace arith { namespace nl { -struct ExtState; +class ExtState; class MonomialBoundsCheck : protected EnvObj { diff --git a/src/theory/arith/nl/ext/monomial_check.h b/src/theory/arith/nl/ext/monomial_check.h index 9929a8d36..6bf4f72ad 100644 --- a/src/theory/arith/nl/ext/monomial_check.h +++ b/src/theory/arith/nl/ext/monomial_check.h @@ -26,7 +26,7 @@ namespace theory { namespace arith { namespace nl { -struct ExtState; +class ExtState; class MonomialCheck : protected EnvObj { diff --git a/src/theory/arith/nl/ext/split_zero_check.h b/src/theory/arith/nl/ext/split_zero_check.h index 398c322bf..e8e0fb7a1 100644 --- a/src/theory/arith/nl/ext/split_zero_check.h +++ b/src/theory/arith/nl/ext/split_zero_check.h @@ -25,7 +25,7 @@ namespace theory { namespace arith { namespace nl { -struct ExtState; +class ExtState; class SplitZeroCheck : protected EnvObj { diff --git a/src/theory/arith/nl/ext/tangent_plane_check.h b/src/theory/arith/nl/ext/tangent_plane_check.h index 6c77e21ad..a256658b7 100644 --- a/src/theory/arith/nl/ext/tangent_plane_check.h +++ b/src/theory/arith/nl/ext/tangent_plane_check.h @@ -26,7 +26,7 @@ namespace theory { namespace arith { namespace nl { -struct ExtState; +class ExtState; class TangentPlaneCheck : protected EnvObj { diff --git a/src/theory/arith/nl/nonlinear_extension.cpp b/src/theory/arith/nl/nonlinear_extension.cpp index 611cb6e81..0855f5a3b 100644 --- a/src/theory/arith/nl/nonlinear_extension.cpp +++ b/src/theory/arith/nl/nonlinear_extension.cpp @@ -51,7 +51,7 @@ NonlinearExtension::NonlinearExtension(Env& env, d_extTheory(env, d_extTheoryCb, d_im), d_model(env), d_trSlv(d_env, d_astate, d_im, d_model), - d_extState(d_im, d_model, d_env), + d_extState(d_env, d_im, d_model), d_factoringSlv(d_env, &d_extState), d_monomialBoundsSlv(d_env, &d_extState), d_monomialSlv(d_env, &d_extState), diff --git a/src/theory/arith/nl/transcendental/transcendental_state.cpp b/src/theory/arith/nl/transcendental/transcendental_state.cpp index dfb011c4b..67f0366ea 100644 --- a/src/theory/arith/nl/transcendental/transcendental_state.cpp +++ b/src/theory/arith/nl/transcendental/transcendental_state.cpp @@ -17,6 +17,7 @@ #include "expr/skolem_manager.h" #include "proof/proof.h" +#include "proof/proof_node_manager.h" #include "theory/arith/arith_utilities.h" #include "theory/arith/inference_manager.h" #include "theory/arith/nl/nl_model.h" @@ -48,8 +49,8 @@ TranscendentalState::TranscendentalState(Env& env, d_neg_one = NodeManager::currentNM()->mkConstInt(Rational(-1)); if (d_env.isTheoryProofProducing()) { - d_proof.reset(new CDProofSet( - d_env.getProofNodeManager(), d_env.getUserContext(), "nl-trans")); + d_proof.reset( + new CDProofSet(d_env, d_env.getUserContext(), "nl-trans")); d_proofChecker.reset(new TranscendentalProofRuleChecker()); d_proofChecker->registerTo(d_env.getProofNodeManager()->getChecker()); } diff --git a/src/theory/arith/operator_elim.cpp b/src/theory/arith/operator_elim.cpp index 7981c4fba..65caeb3d3 100644 --- a/src/theory/arith/operator_elim.cpp +++ b/src/theory/arith/operator_elim.cpp @@ -33,10 +33,7 @@ namespace cvc5::internal { namespace theory { namespace arith { -OperatorElim::OperatorElim(Env& env) - : EnvObj(env), EagerProofGenerator(d_env.getProofNodeManager()) -{ -} +OperatorElim::OperatorElim(Env& env) : EagerProofGenerator(env) {} void OperatorElim::checkNonLinearLogic(Node term) { @@ -462,7 +459,7 @@ bool OperatorElim::usePartialFunction(SkolemFunId id) const SkolemLemma OperatorElim::mkSkolemLemma(Node lem, Node k) { TrustNode tlem; - if (d_pnm != nullptr) + if (d_env.isTheoryProofProducing()) { tlem = mkTrustNode(lem, PfRule::THEORY_PREPROCESS_LEMMA, {}, {lem}); } diff --git a/src/theory/arith/operator_elim.h b/src/theory/arith/operator_elim.h index 45bc899c2..e91e8d1a9 100644 --- a/src/theory/arith/operator_elim.h +++ b/src/theory/arith/operator_elim.h @@ -31,7 +31,7 @@ class TConvProofGenerator; namespace theory { namespace arith { -class OperatorElim : protected EnvObj, public EagerProofGenerator +class OperatorElim : public EagerProofGenerator { public: OperatorElim(Env& env); diff --git a/src/theory/arith/pp_rewrite_eq.cpp b/src/theory/arith/pp_rewrite_eq.cpp index 6bb4b180d..0e0d10a16 100644 --- a/src/theory/arith/pp_rewrite_eq.cpp +++ b/src/theory/arith/pp_rewrite_eq.cpp @@ -25,8 +25,7 @@ namespace theory { namespace arith { PreprocessRewriteEq::PreprocessRewriteEq(Env& env) - : EnvObj(env), - d_ppPfGen(d_env.getProofNodeManager(), context(), "Arith::ppRewrite") + : EnvObj(env), d_ppPfGen(env, context(), "Arith::ppRewrite") { } diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index e47abdac7..b20632238 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -44,7 +44,7 @@ TheoryArith::TheoryArith(Env& env, OutputChannel& out, Valuation valuation) d_astate(env, valuation), d_im(env, *this, d_astate), d_ppre(d_env), - d_bab(env, d_astate, d_im, d_ppre, d_pnm), + d_bab(env, d_astate, d_im, d_ppre), d_eqSolver(nullptr), d_internal(new linear::TheoryArithPrivate(*this, env, d_bab)), d_nonlinearExtension(nullptr), diff --git a/src/theory/arrays/inference_manager.cpp b/src/theory/arrays/inference_manager.cpp index 2e44598c7..8901832b8 100644 --- a/src/theory/arrays/inference_manager.cpp +++ b/src/theory/arrays/inference_manager.cpp @@ -29,11 +29,9 @@ namespace arrays { InferenceManager::InferenceManager(Env& env, Theory& t, TheoryState& state) : TheoryInferenceManager(env, t, state, "theory::arrays::", false), - d_lemmaPg(isProofEnabled() - ? new EagerProofGenerator(env.getProofNodeManager(), - userContext(), - "ArrayLemmaProofGenerator") - : nullptr) + d_lemmaPg(isProofEnabled() ? new EagerProofGenerator( + env, userContext(), "ArrayLemmaProofGenerator") + : nullptr) { } diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index bed9031c7..02f375a07 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -79,7 +79,7 @@ TheoryArrays::TheoryArrays(Env& env, name + "number of setModelVal conflicts")), d_ppEqualityEngine(d_env, userContext(), name + "pp", true), d_ppFacts(userContext()), - d_rewriter(env.getRewriter(), d_pnm), + d_rewriter(env), d_state(env, valuation), d_im(env, *this, d_state), d_literalsToPropagate(context()), diff --git a/src/theory/arrays/theory_arrays_rewriter.cpp b/src/theory/arrays/theory_arrays_rewriter.cpp index 4aad2bf9a..7af0af62d 100644 --- a/src/theory/arrays/theory_arrays_rewriter.cpp +++ b/src/theory/arrays/theory_arrays_rewriter.cpp @@ -22,6 +22,7 @@ #include "expr/attribute.h" #include "proof/conv_proof_generator.h" #include "proof/eager_proof_generator.h" +#include "smt/env.h" #include "theory/arrays/skolem_cache.h" #include "theory/type_enumerator.h" #include "util/cardinality.h" @@ -58,9 +59,10 @@ void setMostFrequentValueCount(TNode store, uint64_t count) { return store.setAttribute(ArrayConstantMostFrequentValueCountAttr(), count); } -TheoryArraysRewriter::TheoryArraysRewriter(Rewriter* rewriter, - ProofNodeManager* pnm) - : d_rewriter(rewriter), d_epg(pnm ? new EagerProofGenerator(pnm) : nullptr) +TheoryArraysRewriter::TheoryArraysRewriter(Env& env) + : d_rewriter(env.getRewriter()), + d_epg(env.isTheoryProofProducing() ? new EagerProofGenerator(env) + : nullptr) { } diff --git a/src/theory/arrays/theory_arrays_rewriter.h b/src/theory/arrays/theory_arrays_rewriter.h index 9c179eca9..48a4319f7 100644 --- a/src/theory/arrays/theory_arrays_rewriter.h +++ b/src/theory/arrays/theory_arrays_rewriter.h @@ -30,11 +30,10 @@ namespace cvc5::internal { class EagerProofGenerator; +class Env; namespace theory { -class Rewriter; - namespace arrays { Node getMostFrequentValue(TNode store); @@ -49,7 +48,7 @@ static inline Node mkEqNode(Node a, Node b) { class TheoryArraysRewriter : public TheoryRewriter { public: - TheoryArraysRewriter(Rewriter* rewriter, ProofNodeManager* pnm); + TheoryArraysRewriter(Env& env); /** Normalize a constant whose index type has cardinality indexCard */ static Node normalizeConstant(TNode node, Cardinality indexCard); diff --git a/src/theory/booleans/circuit_propagator.cpp b/src/theory/booleans/circuit_propagator.cpp index df3e63d24..22dd3da8b 100644 --- a/src/theory/booleans/circuit_propagator.cpp +++ b/src/theory/booleans/circuit_propagator.cpp @@ -49,7 +49,6 @@ CircuitPropagator::CircuitPropagator(Env& env, bool enableForward, bool enableBa d_forwardPropagation(enableForward), d_backwardPropagation(enableBackward), d_needsFinish(false), - d_pnm(nullptr), d_epg(nullptr), d_proofInternal(nullptr), d_proofExternal(nullptr) @@ -75,7 +74,8 @@ void CircuitPropagator::assertTrue(TNode assertion) } else if (assertion.getKind() == kind::AND) { - ProofCircuitPropagatorBackward prover{d_pnm, assertion, true}; + ProofCircuitPropagatorBackward prover{ + d_env.getProofNodeManager(), assertion, true}; if (isProofEnabled()) { addProof(assertion, prover.assume(assertion)); @@ -93,7 +93,9 @@ void CircuitPropagator::assertTrue(TNode assertion) // Assign the given assertion to true assignAndEnqueue(assertion, true, - isProofEnabled() ? d_pnm->mkAssume(assertion) : nullptr); + isProofEnabled() + ? d_env.getProofNodeManager()->mkAssume(assertion) + : nullptr); } } @@ -165,7 +167,7 @@ void CircuitPropagator::makeConflict(Node n) { return; } - ProofCircuitPropagator pcp(d_pnm); + ProofCircuitPropagator pcp(d_env.getProofNodeManager()); if (n == bfalse) { d_epg->setProofFor(bfalse, pcp.assume(bfalse)); @@ -237,7 +239,8 @@ void CircuitPropagator::propagateBackward(TNode parent, bool parentAssignment) { Trace("circuit-prop") << "CircuitPropagator::propagateBackward(" << parent << ", " << parentAssignment << ")" << endl; - ProofCircuitPropagatorBackward prover{d_pnm, parent, parentAssignment}; + ProofCircuitPropagatorBackward prover{ + d_env.getProofNodeManager(), parent, parentAssignment}; // backward rules switch (parent.getKind()) @@ -449,7 +452,8 @@ void CircuitPropagator::propagateForward(TNode child, bool childAssignment) Trace("circuit-prop") << "Parent: " << parent << endl; Assert(expr::hasSubterm(parent, child)); - ProofCircuitPropagatorForward prover{d_pnm, child, childAssignment, parent}; + ProofCircuitPropagatorForward prover{ + d_env.getProofNodeManager(), child, childAssignment, parent}; // Forward rules switch (parent.getKind()) @@ -774,18 +778,16 @@ TrustNode CircuitPropagator::propagate() void CircuitPropagator::enableProofs(context::Context* ctx, ProofGenerator* defParent) { - d_pnm = d_env.getProofNodeManager(); - Assert(d_pnm != nullptr); - d_epg.reset(new EagerProofGenerator(d_pnm, ctx)); + d_epg.reset(new EagerProofGenerator(d_env, ctx)); d_proofInternal.reset(new LazyCDProofChain( - d_pnm, true, ctx, d_epg.get(), true, "CircuitPropInternalLazyChain")); + d_env, true, ctx, d_epg.get(), true, "CircuitPropInternalLazyChain")); if (defParent != nullptr) { // If we provide a parent proof generator (defParent), we want the ASSUME // leafs of proofs provided by this class to call the getProofFor method on // the parent. To do this, we use a LazyCDProofChain. d_proofExternal.reset(new LazyCDProofChain( - d_pnm, true, ctx, defParent, false, "CircuitPropExternalLazyChain")); + d_env, true, ctx, defParent, false, "CircuitPropExternalLazyChain")); } } diff --git a/src/theory/booleans/circuit_propagator.h b/src/theory/booleans/circuit_propagator.h index 4c872955c..5a93fd651 100644 --- a/src/theory/booleans/circuit_propagator.h +++ b/src/theory/booleans/circuit_propagator.h @@ -249,8 +249,6 @@ class CircuitPropagator : protected EnvObj /** Adds a new proof for f, or drops it if we already have a proof */ void addProof(TNode f, std::shared_ptr pf); - /** A pointer to the proof manager */ - ProofNodeManager* d_pnm; /** Eager proof generator that actually stores the proofs */ std::unique_ptr d_epg; /** Connects the proofs to subproofs internally */ diff --git a/src/theory/bv/bitblast/bitblast_proof_generator.cpp b/src/theory/bv/bitblast/bitblast_proof_generator.cpp index 08fac0fc5..dc4119f96 100644 --- a/src/theory/bv/bitblast/bitblast_proof_generator.cpp +++ b/src/theory/bv/bitblast/bitblast_proof_generator.cpp @@ -22,9 +22,8 @@ namespace theory { namespace bv { BitblastProofGenerator::BitblastProofGenerator(Env& env, - ProofNodeManager* pnm, TConvProofGenerator* tcpg) - : EnvObj(env), d_pnm(pnm), d_tcpg(tcpg) + : EnvObj(env), d_tcpg(tcpg) { } @@ -32,7 +31,7 @@ std::shared_ptr BitblastProofGenerator::getProofFor(Node eq) { const auto& [t, bbt] = d_cache.at(eq); - CDProof cdp(d_pnm); + CDProof cdp(d_env); /* Coarse-grained bit-blast step. */ if (t.isNull()) { diff --git a/src/theory/bv/bitblast/bitblast_proof_generator.h b/src/theory/bv/bitblast/bitblast_proof_generator.h index 3a73210f7..b042697c2 100644 --- a/src/theory/bv/bitblast/bitblast_proof_generator.h +++ b/src/theory/bv/bitblast/bitblast_proof_generator.h @@ -33,7 +33,6 @@ class BitblastProofGenerator : public ProofGenerator, protected EnvObj { public: BitblastProofGenerator(Env& env, - ProofNodeManager* pnm, TConvProofGenerator* tcpg); ~BitblastProofGenerator(){}; @@ -57,8 +56,6 @@ class BitblastProofGenerator : public ProofGenerator, protected EnvObj void addBitblastStep(TNode t, TNode bbt, TNode eq); private: - /** The associated proof node manager. */ - ProofNodeManager* d_pnm; /** * The associated term conversion proof generator, which tracks the * individual bit-blast steps. diff --git a/src/theory/bv/bitblast/proof_bitblaster.cpp b/src/theory/bv/bitblast/proof_bitblaster.cpp index c300a757b..5e5972bc0 100644 --- a/src/theory/bv/bitblast/proof_bitblaster.cpp +++ b/src/theory/bv/bitblast/proof_bitblaster.cpp @@ -24,29 +24,23 @@ namespace cvc5::internal { namespace theory { namespace bv { -BBProof::BBProof(Env& env, - TheoryState* state, - ProofNodeManager* pnm, - bool fineGrained) +BBProof::BBProof(Env& env, TheoryState* state, bool fineGrained) : EnvObj(env), d_bb(new NodeBitblaster(env, state)), - d_pnm(pnm), d_tcontext(new TheoryLeafTermContext(theory::THEORY_BV)), - d_tcpg(pnm ? new TConvProofGenerator( - pnm, - nullptr, - /* ONCE to visit each term only once, post-order. FIXPOINT - * could lead to infinite loops due to terms being rewritten - * to terms that contain themselves */ - TConvPolicy::ONCE, - /* STATIC to get the same ProofNode for a shared subterm. */ - TConvCachePolicy::STATIC, - "BBProof::TConvProofGenerator", - d_tcontext.get(), - false) - : nullptr), - d_bbpg(pnm ? new BitblastProofGenerator(env, pnm, d_tcpg.get()) - : nullptr), + d_tcpg(new TConvProofGenerator( + env, + nullptr, + /* ONCE to visit each term only once, post-order. FIXPOINT + * could lead to infinite loops due to terms being rewritten + * to terms that contain themselves */ + TConvPolicy::ONCE, + /* STATIC to get the same ProofNode for a shared subterm. */ + TConvCachePolicy::STATIC, + "BBProof::TConvProofGenerator", + d_tcontext.get(), + false)), + d_bbpg(new BitblastProofGenerator(env, d_tcpg.get())), d_recordFineGrainedProofs(fineGrained) { } @@ -210,7 +204,7 @@ bool BBProof::collectModelValues(TheoryModel* m, BitblastProofGenerator* BBProof::getProofGenerator() { return d_bbpg.get(); } -bool BBProof::isProofsEnabled() const { return d_pnm != nullptr; } +bool BBProof::isProofsEnabled() const { return d_env.isTheoryProofProducing(); } } // namespace bv } // namespace theory diff --git a/src/theory/bv/bitblast/proof_bitblaster.h b/src/theory/bv/bitblast/proof_bitblaster.h index fc80f1e99..60191a137 100644 --- a/src/theory/bv/bitblast/proof_bitblaster.h +++ b/src/theory/bv/bitblast/proof_bitblaster.h @@ -36,7 +36,6 @@ class BBProof : protected EnvObj public: BBProof(Env& env, TheoryState* state, - ProofNodeManager* pnm, bool fineGrained); ~BBProof(); @@ -64,8 +63,6 @@ class BBProof : protected EnvObj /** The associated simple bit-blaster. */ std::unique_ptr d_bb; - /** The associated proof node manager. */ - ProofNodeManager* d_pnm; /** Term context for d_tcpg to not rewrite below BV leafs. */ std::unique_ptr d_tcontext; /** Term conversion proof generator for bit-blast steps. */ diff --git a/src/theory/bv/bv_solver_bitblast.cpp b/src/theory/bv/bv_solver_bitblast.cpp index a95dfce9b..5049558b7 100644 --- a/src/theory/bv/bv_solver_bitblast.cpp +++ b/src/theory/bv/bv_solver_bitblast.cpp @@ -110,8 +110,7 @@ class BBRegistrar : public prop::Registrar BVSolverBitblast::BVSolverBitblast(Env& env, TheoryState* s, - TheoryInferenceManager& inferMgr, - ProofNodeManager* pnm) + TheoryInferenceManager& inferMgr) : BVSolver(env, *s, inferMgr), d_bitblaster(new NodeBitblaster(env, s)), d_bbRegistrar(new BBRegistrar(d_bitblaster.get())), @@ -120,15 +119,17 @@ BVSolverBitblast::BVSolverBitblast(Env& env, d_bbInputFacts(context()), d_assumptions(context()), d_assertions(context()), - d_epg(pnm ? new EagerProofGenerator(pnm, userContext(), "") : nullptr), + d_epg(env.isTheoryProofProducing() + ? new EagerProofGenerator(env, userContext(), "") + : nullptr), d_factLiteralCache(context()), d_literalFactCache(context()), d_propagate(options().bv.bitvectorPropagate), d_resetNotify(new NotifyResetAssertions(userContext())) { - if (pnm != nullptr) + if (env.isTheoryProofProducing()) { - d_bvProofChecker.registerTo(pnm->getChecker()); + d_bvProofChecker.registerTo(env.getProofNodeManager()->getChecker()); } initSatSolver(); diff --git a/src/theory/bv/bv_solver_bitblast.h b/src/theory/bv/bv_solver_bitblast.h index 401b9a312..519b5693f 100644 --- a/src/theory/bv/bv_solver_bitblast.h +++ b/src/theory/bv/bv_solver_bitblast.h @@ -45,8 +45,7 @@ class BVSolverBitblast : public BVSolver public: BVSolverBitblast(Env& env, TheoryState* state, - TheoryInferenceManager& inferMgr, - ProofNodeManager* pnm); + TheoryInferenceManager& inferMgr); ~BVSolverBitblast() = default; bool needsEqualityEngine(EeSetupInfo& esi) override { return true; } diff --git a/src/theory/bv/bv_solver_bitblast_internal.cpp b/src/theory/bv/bv_solver_bitblast_internal.cpp index a00019ead..eb8ce16e5 100644 --- a/src/theory/bv/bv_solver_bitblast_internal.cpp +++ b/src/theory/bv/bv_solver_bitblast_internal.cpp @@ -70,14 +70,10 @@ void collectBVAtoms(TNode n, std::unordered_set& atoms) } // namespace BVSolverBitblastInternal::BVSolverBitblastInternal( - Env& env, - TheoryState* s, - TheoryInferenceManager& inferMgr, - ProofNodeManager* pnm) + Env& env, TheoryState* s, TheoryInferenceManager& inferMgr) : BVSolver(env, *s, inferMgr), - d_pnm(pnm), - d_bitblaster(new BBProof(env, s, pnm, false)), - d_epg(pnm ? new EagerProofGenerator(pnm) : nullptr) + d_bitblaster(new BBProof(env, s, false)), + d_epg(new EagerProofGenerator(d_env)) { } @@ -92,7 +88,7 @@ void BVSolverBitblastInternal::addBBLemma(TNode fact) Node atom_bb = d_bitblaster->getStoredBBAtom(fact); Node lemma = nm->mkNode(kind::EQUAL, fact, atom_bb); - if (d_pnm == nullptr) + if (!d_env.isTheoryProofProducing()) { d_im.lemma(lemma, InferenceId::BV_BITBLAST_INTERNAL_BITBLAST_LEMMA); } @@ -129,7 +125,7 @@ bool BVSolverBitblastInternal::preNotifyFact( NodeManager* nm = NodeManager::currentNM(); Node lemma = nm->mkNode(kind::EQUAL, fact, n); - if (d_pnm == nullptr) + if (!d_env.isTheoryProofProducing()) { d_im.lemma(lemma, InferenceId::BV_BITBLAST_INTERNAL_EAGER_LEMMA); } diff --git a/src/theory/bv/bv_solver_bitblast_internal.h b/src/theory/bv/bv_solver_bitblast_internal.h index 8ac9fb757..5694324ff 100644 --- a/src/theory/bv/bv_solver_bitblast_internal.h +++ b/src/theory/bv/bv_solver_bitblast_internal.h @@ -40,8 +40,7 @@ class BVSolverBitblastInternal : public BVSolver public: BVSolverBitblastInternal(Env& env, TheoryState* state, - TheoryInferenceManager& inferMgr, - ProofNodeManager* pnm); + TheoryInferenceManager& inferMgr); ~BVSolverBitblastInternal() = default; bool needsEqualityEngine(EeSetupInfo& esi) override; @@ -73,8 +72,6 @@ class BVSolverBitblastInternal : public BVSolver */ void addBBLemma(TNode fact); - /** Proof node manager. */ - ProofNodeManager* d_pnm; /** Bit-blaster used to bit-blast atoms/terms. */ std::unique_ptr d_bitblaster; /** Proof rule checker */ diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index ab87b7fdb..9e3d262ca 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -48,13 +48,12 @@ TheoryBV::TheoryBV(Env& env, switch (options().bv.bvSolver) { case options::BVSolver::BITBLAST: - d_internal.reset(new BVSolverBitblast(env, &d_state, d_im, d_pnm)); + d_internal.reset(new BVSolverBitblast(env, &d_state, d_im)); break; default: AlwaysAssert(options().bv.bvSolver == options::BVSolver::BITBLAST_INTERNAL); - d_internal.reset( - new BVSolverBitblastInternal(d_env, &d_state, d_im, d_pnm)); + d_internal.reset(new BVSolverBitblastInternal(d_env, &d_state, d_im)); } d_theoryState = &d_state; d_inferManager = &d_im; diff --git a/src/theory/combination_engine.cpp b/src/theory/combination_engine.cpp index 07755344f..a23bd7a90 100644 --- a/src/theory/combination_engine.cpp +++ b/src/theory/combination_engine.cpp @@ -34,14 +34,14 @@ CombinationEngine::CombinationEngine(Env& env, : EnvObj(env), d_te(te), d_valuation(&te), - d_pnm(env.isTheoryProofProducing() ? env.getProofNodeManager() : nullptr), d_logicInfo(env.getLogicInfo()), d_paraTheories(paraTheories), d_eemanager(nullptr), d_mmanager(nullptr), d_sharedSolver(nullptr), - d_cmbsPg(d_pnm ? new EagerProofGenerator(d_pnm, env.getUserContext()) - : nullptr) + d_cmbsPg(env.isTheoryProofProducing() + ? new EagerProofGenerator(env, env.getUserContext()) + : nullptr) { // create the equality engine, model manager, and shared solver if (options().theory.eeMode == options::EqEngineMode::DISTRIBUTED) diff --git a/src/theory/combination_engine.h b/src/theory/combination_engine.h index 0e1c3ef92..ab10c48bd 100644 --- a/src/theory/combination_engine.h +++ b/src/theory/combination_engine.h @@ -109,8 +109,6 @@ class CombinationEngine : protected EnvObj TheoryEngine& d_te; /** Valuation for the engine */ Valuation d_valuation; - /** The proof node manager */ - ProofNodeManager* d_pnm; /** Logic info of theory engine (cached) */ const LogicInfo& d_logicInfo; /** List of parametric theories of theory engine */ diff --git a/src/theory/datatypes/infer_proof_cons.cpp b/src/theory/datatypes/infer_proof_cons.cpp index 7ff1c7033..ab12ba6d7 100644 --- a/src/theory/datatypes/infer_proof_cons.cpp +++ b/src/theory/datatypes/infer_proof_cons.cpp @@ -29,10 +29,9 @@ namespace cvc5::internal { namespace theory { namespace datatypes { -InferProofCons::InferProofCons(context::Context* c, ProofNodeManager* pnm) - : d_pnm(pnm), d_lazyFactMap(c == nullptr ? &d_context : c) +InferProofCons::InferProofCons(Env& env, context::Context* c) + : EnvObj(env), d_lazyFactMap(c == nullptr ? &d_context : c) { - Assert(d_pnm != nullptr); } void InferProofCons::notifyFact(const std::shared_ptr& di) @@ -267,7 +266,7 @@ std::shared_ptr InferProofCons::getProofFor(Node fact) { Trace("dt-ipc") << "dt-ipc: Ask proof for " << fact << std::endl; // temporary proof - CDProof pf(d_pnm); + CDProof pf(d_env); // get the inference NodeDatatypesInferenceMap::iterator it = d_lazyFactMap.find(fact); if (it == d_lazyFactMap.end()) diff --git a/src/theory/datatypes/infer_proof_cons.h b/src/theory/datatypes/infer_proof_cons.h index 66f2ba628..109ed71e2 100644 --- a/src/theory/datatypes/infer_proof_cons.h +++ b/src/theory/datatypes/infer_proof_cons.h @@ -21,12 +21,10 @@ #include "context/cdhashmap.h" #include "expr/node.h" #include "proof/proof_generator.h" +#include "smt/env_obj.h" #include "theory/datatypes/inference.h" namespace cvc5::internal { - -class ProofNodeManager; - namespace theory { namespace datatypes { @@ -40,13 +38,13 @@ namespace datatypes { * The main (private) method of this class is convert below, which is * called when we need to construct a proof node from an InferInfo. */ -class InferProofCons : public ProofGenerator +class InferProofCons : protected EnvObj, public ProofGenerator { typedef context::CDHashMap> NodeDatatypesInferenceMap; public: - InferProofCons(context::Context* c, ProofNodeManager* pnm); + InferProofCons(Env& env, context::Context* c); ~InferProofCons() {} /** * This is called to notify that di is an inference that may need a proof @@ -87,8 +85,6 @@ class InferProofCons : public ProofGenerator void convert(InferenceId infer, TNode conc, TNode exp, CDProof* cdp); /** A dummy context used by this class if none is provided */ context::Context d_context; - /** the proof node manager */ - ProofNodeManager* d_pnm; /** The lazy fact map */ NodeDatatypesInferenceMap d_lazyFactMap; }; diff --git a/src/theory/datatypes/inference_manager.cpp b/src/theory/datatypes/inference_manager.cpp index 755c545f0..0ebd85bc1 100644 --- a/src/theory/datatypes/inference_manager.cpp +++ b/src/theory/datatypes/inference_manager.cpp @@ -32,14 +32,10 @@ namespace datatypes { InferenceManager::InferenceManager(Env& env, Theory& t, TheoryState& state) : InferenceManagerBuffered(env, t, state, "theory::datatypes::"), - d_ipc(isProofEnabled() - ? new InferProofCons(context(), env.getProofNodeManager()) - : nullptr), - d_lemPg(isProofEnabled() - ? new EagerProofGenerator(env.getProofNodeManager(), - userContext(), - "datatypes::lemPg") - : nullptr) + d_ipc(isProofEnabled() ? new InferProofCons(env, context()) : nullptr), + d_lemPg(isProofEnabled() ? new EagerProofGenerator( + env, userContext(), "datatypes::lemPg") + : nullptr) { d_false = NodeManager::currentNM()->mkConst(false); } @@ -110,8 +106,7 @@ TrustNode InferenceManager::processDtLemma(Node conc, Node exp, InferenceId id) std::shared_ptr ipcl; if (isProofEnabled()) { - ipcl = - std::make_shared(nullptr, d_env.getProofNodeManager()); + ipcl = std::make_shared(d_env, nullptr); } conc = prepareDtInference(conc, exp, id, ipcl.get()); // send it as a lemma diff --git a/src/theory/quantifiers/alpha_equivalence.cpp b/src/theory/quantifiers/alpha_equivalence.cpp index 422c163d4..8e71239d4 100644 --- a/src/theory/quantifiers/alpha_equivalence.cpp +++ b/src/theory/quantifiers/alpha_equivalence.cpp @@ -166,8 +166,8 @@ AlphaEquivalence::AlphaEquivalence(Env& env) : EnvObj(env), d_termCanon(), d_aedb(userContext(), &d_termCanon, true), - d_pnm(env.getProofNodeManager()), - d_pfAlpha(d_pnm ? new EagerProofGenerator(d_pnm) : nullptr) + d_pfAlpha(env.isTheoryProofProducing() ? new EagerProofGenerator(env) + : nullptr) { } @@ -215,7 +215,7 @@ TrustNode AlphaEquivalence::reduceQuantifier(Node q) Trace("alpha-eq") << "subs: " << vars[i] << " -> " << subs[i] << std::endl; } - CDProof cdp(d_pnm); + CDProof cdp(d_env); Node sret = ret.substitute(vars.begin(), vars.end(), subs.begin(), subs.end()); std::vector transEq; diff --git a/src/theory/quantifiers/alpha_equivalence.h b/src/theory/quantifiers/alpha_equivalence.h index 3d6fdd43e..a78aa98b2 100644 --- a/src/theory/quantifiers/alpha_equivalence.h +++ b/src/theory/quantifiers/alpha_equivalence.h @@ -131,8 +131,6 @@ class AlphaEquivalence : protected EnvObj expr::TermCanonize d_termCanon; /** the database of quantified formulas registered to this class */ AlphaEquivalenceDb d_aedb; - /** Pointer to the proof node manager */ - ProofNodeManager* d_pnm; /** An eager proof generator storing alpha equivalence proofs.*/ std::unique_ptr d_pfAlpha; /** Are proofs enabled for this object? */ diff --git a/src/theory/quantifiers/instantiate.cpp b/src/theory/quantifiers/instantiate.cpp index d7beb12c8..5602f64ad 100644 --- a/src/theory/quantifiers/instantiate.cpp +++ b/src/theory/quantifiers/instantiate.cpp @@ -53,10 +53,9 @@ Instantiate::Instantiate(Env& env, d_treg(tr), d_insts(userContext()), d_c_inst_match_trie_dom(userContext()), - d_pfInst(isProofEnabled() ? new CDProof(env.getProofNodeManager(), - userContext(), - "Instantiate::pfInst") - : nullptr) + d_pfInst(isProofEnabled() + ? new CDProof(env, userContext(), "Instantiate::pfInst") + : nullptr) { } @@ -248,10 +247,8 @@ bool Instantiate::addInstantiation(Node q, std::shared_ptr pfTmp; if (isProofEnabled()) { - pfTmp.reset(new LazyCDProof(d_env.getProofNodeManager(), - nullptr, - nullptr, - "Instantiate::LazyCDProof::tmp")); + pfTmp.reset(new LazyCDProof( + d_env, nullptr, nullptr, "Instantiate::LazyCDProof::tmp")); } // construct the instantiation diff --git a/src/theory/quantifiers/skolemize.cpp b/src/theory/quantifiers/skolemize.cpp index 8de208513..2af247e51 100644 --- a/src/theory/quantifiers/skolemize.cpp +++ b/src/theory/quantifiers/skolemize.cpp @@ -43,9 +43,7 @@ Skolemize::Skolemize(Env& env, QuantifiersState& qs, TermRegistry& tr) d_skolemized(userContext()), d_epg(!isProofEnabled() ? nullptr - : new EagerProofGenerator(env.getProofNodeManager(), - userContext(), - "Skolemize::epg")) + : new EagerProofGenerator(env, userContext(), "Skolemize::epg")) { } @@ -72,7 +70,7 @@ TrustNode Skolemize::process(Node q) Node existsq = nm->mkNode(EXISTS, echildren); Node res = skm->mkSkolemize(existsq, d_skolem_constants[q], "skv"); Node qnot = q.notNode(); - CDProof cdp(pnm); + CDProof cdp(d_env); cdp.addStep(res, PfRule::SKOLEMIZE, {qnot}, {}); std::shared_ptr pf = cdp.getProofFor(res); std::vector assumps; diff --git a/src/theory/rewriter.cpp b/src/theory/rewriter.cpp index af9869dd6..fbba1386c 100644 --- a/src/theory/rewriter.cpp +++ b/src/theory/rewriter.cpp @@ -118,15 +118,15 @@ TrustNode Rewriter::rewriteWithProof(TNode node, return TrustNode::mkTrustRewrite(node, ret, d_tpg.get()); } -void Rewriter::setProofNodeManager(ProofNodeManager* pnm) +void Rewriter::finishInit(Env& env) { // if not already initialized with proof support if (d_tpg == nullptr) { - Trace("rewriter") << "Rewriter::setProofNodeManager" << std::endl; + Trace("rewriter") << "Rewriter::finishInit" << std::endl; // the rewriter is staticly determinstic, thus use static cache policy // for the term conversion proof generator - d_tpg.reset(new TConvProofGenerator(pnm, + d_tpg.reset(new TConvProofGenerator(env, nullptr, TConvPolicy::FIXPOINT, TConvCachePolicy::STATIC, diff --git a/src/theory/rewriter.h b/src/theory/rewriter.h index 0fc50e640..695dbf3b4 100644 --- a/src/theory/rewriter.h +++ b/src/theory/rewriter.h @@ -84,8 +84,8 @@ class Rewriter { TrustNode rewriteWithProof(TNode node, bool isExtEq = false); - /** Set proof node manager */ - void setProofNodeManager(ProofNodeManager* pnm); + /** Finish init, which sets up the proof manager if applicable */ + void finishInit(Env& env); /** * Registers a theory rewriter with this rewriter. The rewriter does not own diff --git a/src/theory/sets/term_registry.cpp b/src/theory/sets/term_registry.cpp index 3f5bc414d..5f91fc97e 100644 --- a/src/theory/sets/term_registry.cpp +++ b/src/theory/sets/term_registry.cpp @@ -28,16 +28,15 @@ namespace sets { TermRegistry::TermRegistry(Env& env, SolverState& state, InferenceManager& im, - SkolemCache& skc, - ProofNodeManager* pnm) + SkolemCache& skc) : EnvObj(env), d_im(im), d_skCache(skc), d_proxy(userContext()), d_proxy_to_term(userContext()), - d_epg( - pnm ? new EagerProofGenerator(pnm, nullptr, "sets::TermRegistry::epg") - : nullptr) + d_epg(env.isTheoryProofProducing() ? new EagerProofGenerator( + env, nullptr, "sets::TermRegistry::epg") + : nullptr) { } diff --git a/src/theory/sets/term_registry.h b/src/theory/sets/term_registry.h index d15ae401d..1a9e3a639 100644 --- a/src/theory/sets/term_registry.h +++ b/src/theory/sets/term_registry.h @@ -44,8 +44,7 @@ class TermRegistry : protected EnvObj TermRegistry(Env& env, SolverState& state, InferenceManager& im, - SkolemCache& skc, - ProofNodeManager* pnm); + SkolemCache& skc); /** get the proxy variable for set n * * Proxy variables are used to communicate information that otherwise would diff --git a/src/theory/sets/theory_sets.cpp b/src/theory/sets/theory_sets.cpp index b1ae7a8eb..5841dd92a 100644 --- a/src/theory/sets/theory_sets.cpp +++ b/src/theory/sets/theory_sets.cpp @@ -34,8 +34,8 @@ TheorySets::TheorySets(Env& env, OutputChannel& out, Valuation valuation) d_state(env, valuation, d_skCache), d_im(env, *this, d_state), d_cpacb(*this), - d_internal(new TheorySetsPrivate( - env, *this, d_state, d_im, d_skCache, d_pnm, d_cpacb)), + d_internal( + new TheorySetsPrivate(env, *this, d_state, d_im, d_skCache, d_cpacb)), d_notify(*d_internal.get(), d_im) { // use the official theory state and inference manager objects diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp index 5794f8a90..485ccb5d0 100644 --- a/src/theory/sets/theory_sets_private.cpp +++ b/src/theory/sets/theory_sets_private.cpp @@ -44,7 +44,6 @@ TheorySetsPrivate::TheorySetsPrivate(Env& env, SolverState& state, InferenceManager& im, SkolemCache& skc, - ProofNodeManager* pnm, CarePairArgumentCallback& cpacb) : EnvObj(env), d_deq(context()), @@ -55,7 +54,7 @@ TheorySetsPrivate::TheorySetsPrivate(Env& env, d_state(state), d_im(im), d_skCache(skc), - d_treg(d_env, state, im, skc, pnm), + d_treg(d_env, state, im, skc), d_rels(new TheorySetsRels(d_env, state, im, skc, d_treg)), d_cardSolver(new CardinalityExtension(d_env, state, im, d_treg)), d_rels_enabled(false), diff --git a/src/theory/sets/theory_sets_private.h b/src/theory/sets/theory_sets_private.h index e80aa7012..281ae7750 100644 --- a/src/theory/sets/theory_sets_private.h +++ b/src/theory/sets/theory_sets_private.h @@ -328,7 +328,6 @@ class TheorySetsPrivate : protected EnvObj SolverState& state, InferenceManager& im, SkolemCache& skc, - ProofNodeManager* pnm, CarePairArgumentCallback& cpacb); ~TheorySetsPrivate(); diff --git a/src/theory/strings/infer_proof_cons.cpp b/src/theory/strings/infer_proof_cons.cpp index 567f61f26..791944d9b 100644 --- a/src/theory/strings/infer_proof_cons.cpp +++ b/src/theory/strings/infer_proof_cons.cpp @@ -31,12 +31,11 @@ namespace cvc5::internal { namespace theory { namespace strings { -InferProofCons::InferProofCons(context::Context* c, - ProofNodeManager* pnm, +InferProofCons::InferProofCons(Env& env, + context::Context* c, SequencesStatistics& statistics) - : d_pnm(pnm), d_lazyFactMap(c), d_statistics(statistics) + : EnvObj(env), d_lazyFactMap(c), d_statistics(statistics) { - Assert(d_pnm != nullptr); } void InferProofCons::notifyFact(const InferInfo& ii) @@ -1170,7 +1169,7 @@ std::shared_ptr InferProofCons::getProofFor(Node fact) Assert(ii->d_conc == fact); // make a placeholder proof using STRINGS_INFERENCE, which is reconstructed // during post-process - CDProof pf(d_pnm); + CDProof pf(d_env); std::vector args; packArgs(ii->d_conc, ii->getId(), ii->d_idRev, ii->d_premises, args); // must flatten diff --git a/src/theory/strings/infer_proof_cons.h b/src/theory/strings/infer_proof_cons.h index 3210308dc..f603d9d15 100644 --- a/src/theory/strings/infer_proof_cons.h +++ b/src/theory/strings/infer_proof_cons.h @@ -24,6 +24,7 @@ #include "proof/proof_checker.h" #include "proof/proof_rule.h" #include "proof/theory_proof_step_buffer.h" +#include "smt/env_obj.h" #include "theory/builtin/proof_checker.h" #include "theory/strings/infer_info.h" #include "theory/strings/sequences_stats.h" @@ -47,13 +48,13 @@ namespace strings { * returns applications of the rule STRING_INFERENCE, which store the arguments * to the proof conversion routine "convert" below. */ -class InferProofCons : public ProofGenerator +class InferProofCons : protected EnvObj, public ProofGenerator { typedef context::CDHashMap> NodeInferInfoMap; public: - InferProofCons(context::Context* c, - ProofNodeManager* pnm, + InferProofCons(Env& env, + context::Context* c, SequencesStatistics& statistics); ~InferProofCons() {} /** @@ -269,8 +270,6 @@ class InferProofCons : public ProofGenerator * in termsToPurify. */ static Node maybePurifyTerm(Node n, std::unordered_set& termsToPurify); - /** the proof node manager */ - ProofNodeManager* d_pnm; /** The lazy fact map */ NodeInferInfoMap d_lazyFactMap; /** Reference to the statistics for the theory of strings/sequences. */ diff --git a/src/theory/strings/inference_manager.cpp b/src/theory/strings/inference_manager.cpp index b4eada12f..ceb27ef4d 100644 --- a/src/theory/strings/inference_manager.cpp +++ b/src/theory/strings/inference_manager.cpp @@ -41,14 +41,10 @@ InferenceManager::InferenceManager(Env& env, d_termReg(tr), d_extt(e), d_statistics(statistics), - d_ipc(isProofEnabled() - ? new InferProofCons( - context(), env.getProofNodeManager(), d_statistics) - : nullptr), - d_ipcl(isProofEnabled() - ? new InferProofCons( - context(), env.getProofNodeManager(), d_statistics) - : nullptr) + d_ipc(isProofEnabled() ? new InferProofCons(env, context(), d_statistics) + : nullptr), + d_ipcl(isProofEnabled() ? new InferProofCons(env, context(), d_statistics) + : nullptr) { NodeManager* nm = NodeManager::currentNM(); d_zero = nm->mkConstInt(Rational(0)); diff --git a/src/theory/strings/regexp_elim.cpp b/src/theory/strings/regexp_elim.cpp index 7ba65bebd..4915dfa57 100644 --- a/src/theory/strings/regexp_elim.cpp +++ b/src/theory/strings/regexp_elim.cpp @@ -18,6 +18,7 @@ #include "expr/bound_var_manager.h" #include "options/strings_options.h" #include "proof/proof_node_manager.h" +#include "smt/env.h" #include "theory/rewriter.h" #include "theory/strings/regexp_entail.h" #include "theory/strings/theory_strings_utils.h" @@ -47,14 +48,12 @@ struct ReElimStarIndexAttributeId typedef expr::Attribute ReElimStarIndexAttribute; -RegExpElimination::RegExpElimination(bool isAgg, - ProofNodeManager* pnm, - context::Context* c) - : d_isAggressive(isAgg), - d_pnm(pnm), - d_epg(pnm == nullptr +RegExpElimination::RegExpElimination(Env& env, bool isAgg, context::Context* c) + : EnvObj(env), + d_isAggressive(isAgg), + d_epg(!env.isTheoryProofProducing() ? nullptr - : new EagerProofGenerator(pnm, c, "RegExpElimination::epg")) + : new EagerProofGenerator(env, c, "RegExpElimination::epg")) { } @@ -80,10 +79,11 @@ TrustNode RegExpElimination::eliminateTrusted(Node atom) // Currently aggressive doesnt work due to fresh bound variables if (isProofEnabled() && !d_isAggressive) { + ProofNodeManager* pnm = d_env.getProofNodeManager(); Node eq = atom.eqNode(eatom); Node aggn = NodeManager::currentNM()->mkConst(d_isAggressive); std::shared_ptr pn = - d_pnm->mkNode(PfRule::RE_ELIM, {}, {atom, aggn}, eq); + pnm->mkNode(PfRule::RE_ELIM, {}, {atom, aggn}, eq); d_epg->setProofFor(eq, pn); return TrustNode::mkTrustRewrite(atom, eatom, d_epg.get()); } @@ -647,7 +647,10 @@ Node RegExpElimination::returnElim(Node atom, Node atomElim, const char* id) << "." << std::endl; return atomElim; } -bool RegExpElimination::isProofEnabled() const { return d_pnm != nullptr; } +bool RegExpElimination::isProofEnabled() const +{ + return d_env.isTheoryProofProducing(); +} } // namespace strings } // namespace theory diff --git a/src/theory/strings/regexp_elim.h b/src/theory/strings/regexp_elim.h index 466c4f882..a3b294668 100644 --- a/src/theory/strings/regexp_elim.h +++ b/src/theory/strings/regexp_elim.h @@ -20,6 +20,7 @@ #include "expr/node.h" #include "proof/eager_proof_generator.h" #include "proof/trust_node.h" +#include "smt/env_obj.h" namespace cvc5::internal { namespace theory { @@ -32,7 +33,7 @@ namespace strings { * * It is used by TheoryStrings during ppRewrite. */ -class RegExpElimination +class RegExpElimination : protected EnvObj { public: /** @@ -40,8 +41,8 @@ class RegExpElimination * @param pnm The proof node manager to use (for proofs) * @param c The context to use (for proofs) */ - RegExpElimination(bool isAgg = false, - ProofNodeManager* pnm = nullptr, + RegExpElimination(Env& env, + bool isAgg = false, context::Context* c = nullptr); /** eliminate membership * @@ -77,8 +78,6 @@ class RegExpElimination bool isProofEnabled() const; /** Are aggressive eliminations enabled? */ bool d_isAggressive; - /** Pointer to the proof node manager */ - ProofNodeManager* d_pnm; /** An eager proof generator for storing proofs in eliminate trusted above */ std::unique_ptr d_epg; }; /* class RegExpElimination */ diff --git a/src/theory/strings/term_registry.cpp b/src/theory/strings/term_registry.cpp index 4ca2ac5f7..0fed748dc 100644 --- a/src/theory/strings/term_registry.cpp +++ b/src/theory/strings/term_registry.cpp @@ -38,8 +38,7 @@ namespace strings { TermRegistry::TermRegistry(Env& env, Theory& t, SolverState& s, - SequencesStatistics& statistics, - ProofNodeManager* pnm) + SequencesStatistics& statistics) : EnvObj(env), d_theory(t), d_state(s), @@ -57,11 +56,10 @@ TermRegistry::TermRegistry(Env& env, d_proxyVar(userContext()), d_proxyVarToLength(userContext()), d_lengthLemmaTermsCache(userContext()), - d_epg(pnm ? new EagerProofGenerator( - pnm, - userContext(), - "strings::TermRegistry::EagerProofGenerator") - : nullptr) + d_epg( + env.isTheoryProofProducing() ? new EagerProofGenerator( + env, userContext(), "strings::TermRegistry::EagerProofGenerator") + : nullptr) { NodeManager* nm = NodeManager::currentNM(); d_zero = nm->mkConstInt(Rational(0)); diff --git a/src/theory/strings/term_registry.h b/src/theory/strings/term_registry.h index 8092b1b0a..210621113 100644 --- a/src/theory/strings/term_registry.h +++ b/src/theory/strings/term_registry.h @@ -59,8 +59,7 @@ class TermRegistry : protected EnvObj TermRegistry(Env& env, Theory& t, SolverState& s, - SequencesStatistics& statistics, - ProofNodeManager* pnm); + SequencesStatistics& statistics); ~TermRegistry(); /** get the cardinality of the alphabet used, based on the options */ uint32_t getAlphabetCardinality() const; diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index e015e1084..a2ff8181e 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -55,7 +55,7 @@ TheoryStrings::TheoryStrings(Env& env, OutputChannel& out, Valuation valuation) d_notify(*this), d_statistics(), d_state(env, d_valuation), - d_termReg(env, *this, d_state, d_statistics, d_pnm), + d_termReg(env, *this, d_state, d_statistics), d_rewriter(env.getRewriter(), &d_statistics.d_rewrites, d_termReg.getAlphabetCardinality()), @@ -83,8 +83,8 @@ TheoryStrings::TheoryStrings(Env& env, OutputChannel& out, Valuation valuation) d_rsolver( env, d_state, d_im, d_termReg, d_csolver, d_esolver, d_statistics), d_regexp_elim( + env, options().strings.regExpElim == options::RegExpElimMode::AGG, - d_pnm, userContext()), d_stringsFmf(env, valuation, d_termReg), d_strat(d_env), diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index a99f07d06..b554a377c 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -215,13 +215,10 @@ void TheoryEngine::finishInit() TheoryEngine::TheoryEngine(Env& env) : EnvObj(env), d_propEngine(nullptr), - d_pnm(d_env.isTheoryProofProducing() ? d_env.getProofNodeManager() - : nullptr), - d_lazyProof( - d_pnm != nullptr ? new LazyCDProof( - d_pnm, nullptr, userContext(), "TheoryEngine::LazyCDProof") - : nullptr), - d_tepg(new TheoryEngineProofGenerator(d_pnm, userContext())), + d_lazyProof(env.isTheoryProofProducing() ? new LazyCDProof( + env, nullptr, userContext(), "TheoryEngine::LazyCDProof") + : nullptr), + d_tepg(new TheoryEngineProofGenerator(env, userContext())), d_tc(nullptr), d_sharedSolver(nullptr), d_quantEngine(nullptr), @@ -1145,7 +1142,7 @@ TrustNode TheoryEngine::getExplanation(TNode node) if (isProofEnabled()) { texplanation.debugCheckClosed( - "te-proof-exp", "texplanation no share", false); + options(), "te-proof-exp", "texplanation no share", false); // check if no generator, if so, add THEORY_LEMMA if (texplanation.getGenerator() == nullptr) { @@ -1321,7 +1318,8 @@ void TheoryEngine::lemma(TrustNode tlemma, tlemma = TrustNode::mkTrustLemma(lemma, d_lazyProof.get()); } // ensure closed - tlemma.debugCheckClosed("te-proof-debug", "TheoryEngine::lemma_initial"); + tlemma.debugCheckClosed( + options(), "te-proof-debug", "TheoryEngine::lemma_initial"); } // assert the lemma @@ -1369,7 +1367,7 @@ void TheoryEngine::conflict(TrustNode tconflict, TheoryId theoryId) Trace("te-proof-debug") << "Check closed conflict" << std::endl; // doesn't require proof generator, yet, since THEORY_LEMMA is added below tconflict.debugCheckClosed( - "te-proof-debug", "TheoryEngine::conflict_initial", false); + options(), "te-proof-debug", "TheoryEngine::conflict_initial", false); Trace("dtview::conflict") << ":THEORY-CONFLICT: " << conflict << std::endl; @@ -1392,7 +1390,8 @@ void TheoryEngine::conflict(TrustNode tconflict, TheoryId theoryId) { Trace("te-proof-debug") << "Check closed conflict explained with sharing" << std::endl; - tncExp.debugCheckClosed("te-proof-debug", + tncExp.debugCheckClosed(options(), + "te-proof-debug", "TheoryEngine::conflict_explained_sharing"); Trace("te-proof-debug") << "Process conflict: " << conflict << std::endl; Trace("te-proof-debug") << "Conflict " << tconflict << " from " @@ -1419,7 +1418,8 @@ void TheoryEngine::conflict(TrustNode tconflict, TheoryId theoryId) Trace("te-proof-debug") << "add lazy step " << tncExp.identifyGenerator() << " for " << proven << std::endl; d_lazyProof->addLazyStep(proven, tncExp.getGenerator()); - pfgEnsureClosed(proven, + pfgEnsureClosed(options(), + proven, d_lazyProof.get(), "te-proof-debug", "TheoryEngine::conflict_during"); @@ -1458,7 +1458,8 @@ void TheoryEngine::conflict(TrustNode tconflict, TheoryId theoryId) << "Check closed conflict with sharing" << std::endl; if (isProofEnabled()) { - tconf.debugCheckClosed("te-proof-debug", "TheoryEngine::conflict:sharing"); + tconf.debugCheckClosed( + options(), "te-proof-debug", "TheoryEngine::conflict:sharing"); } lemma(tconf, LemmaProperty::REMOVABLE); } @@ -1508,7 +1509,7 @@ TrustNode TheoryEngine::getExplanation( // communicating arrangements between shared terms, and the rewriter // for arithmetic equalities does not preserve terms, e.g. x=y may become // x+-1*y=0. - lcp.reset(new LazyCDProof(d_pnm, + lcp.reset(new LazyCDProof(d_env, nullptr, nullptr, "TheoryEngine::LazyCDProof::getExplanation", @@ -1640,7 +1641,8 @@ TrustNode TheoryEngine::getExplanation( d_sharedSolver->explain(toExplain.d_node, toExplain.d_theory); if (lcp != nullptr) { - texplanation.debugCheckClosed("te-proof-exp", "texplanation", false); + texplanation.debugCheckClosed( + options(), "te-proof-exp", "texplanation", false); Trace("te-proof-exp") << "- t-explained[" << toExplain.d_theory << "]: " << toExplain.d_node << " by " << texplanation.getNode() << std::endl; diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 13e378585..545356312 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -498,9 +498,7 @@ class TheoryEngine : protected EnvObj */ theory::Theory* d_theoryTable[theory::THEORY_LAST]; - //--------------------------------- new proofs - /** Proof node manager used by this theory engine, if proofs are enabled */ - ProofNodeManager* d_pnm; + //--------------------------------- proofs /** The lazy proof object * * This stores instructions for how to construct proofs for all theory lemmas. @@ -508,7 +506,7 @@ class TheoryEngine : protected EnvObj std::shared_ptr d_lazyProof; /** The proof generator */ std::shared_ptr d_tepg; - //--------------------------------- end new proofs + //--------------------------------- end proofs /** The combination manager we are using */ std::unique_ptr d_tc; /** The shared solver of the above combination engine. */ diff --git a/src/theory/theory_engine_proof_generator.cpp b/src/theory/theory_engine_proof_generator.cpp index fa28f3f1b..868413bf8 100644 --- a/src/theory/theory_engine_proof_generator.cpp +++ b/src/theory/theory_engine_proof_generator.cpp @@ -18,14 +18,15 @@ #include #include "proof/proof_node.h" +#include "smt/env.h" using namespace cvc5::internal::kind; namespace cvc5::internal { -TheoryEngineProofGenerator::TheoryEngineProofGenerator(ProofNodeManager* pnm, +TheoryEngineProofGenerator::TheoryEngineProofGenerator(Env& env, context::Context* c) - : d_pnm(pnm), d_proofs(c) + : EnvObj(env), d_proofs(c) { d_false = NodeManager::currentNM()->mkConst(false); } @@ -107,7 +108,8 @@ std::shared_ptr TheoryEngineProofGenerator::getProofFor(Node f) std::shared_ptr pfb = lcp->getProofFor(conclusion); Trace("tepg-debug") << "...mkScope" << std::endl; // call the scope method of proof node manager - std::shared_ptr pf = d_pnm->mkScope(pfb, scopeAssumps); + ProofNodeManager* pnm = d_env.getProofNodeManager(); + std::shared_ptr pf = pnm->mkScope(pfb, scopeAssumps); if (pf->getResult() != f) { diff --git a/src/theory/theory_engine_proof_generator.h b/src/theory/theory_engine_proof_generator.h index 7ef10b6de..5ba1f17f4 100644 --- a/src/theory/theory_engine_proof_generator.h +++ b/src/theory/theory_engine_proof_generator.h @@ -26,6 +26,7 @@ #include "proof/proof_generator.h" #include "proof/proof_node_manager.h" #include "proof/trust_node.h" +#include "smt/env_obj.h" namespace cvc5::internal { @@ -36,13 +37,13 @@ namespace cvc5::internal { * Notice that this class could be made general purpose. Its main feature is * storing lazy proofs for facts in a context-dependent manner. */ -class TheoryEngineProofGenerator : public ProofGenerator +class TheoryEngineProofGenerator : protected EnvObj, public ProofGenerator { typedef context::CDHashMap> NodeLazyCDProofMap; public: - TheoryEngineProofGenerator(ProofNodeManager* pnm, context::Context* c); + TheoryEngineProofGenerator(Env& env, context::Context* c); ~TheoryEngineProofGenerator() {} /** * Make trust explanation. Called when lpf has a proof of lit from free @@ -67,8 +68,6 @@ class TheoryEngineProofGenerator : public ProofGenerator std::string identify() const override; private: - /** The proof manager, used for allocating new ProofNode objects */ - ProofNodeManager* d_pnm; /** Map from formulas to lazy CD proofs */ NodeLazyCDProofMap d_proofs; /** The false node */ diff --git a/src/theory/theory_inference_manager.cpp b/src/theory/theory_inference_manager.cpp index ce532bbb0..e9df32f9c 100644 --- a/src/theory/theory_inference_manager.cpp +++ b/src/theory/theory_inference_manager.cpp @@ -68,7 +68,7 @@ TheoryInferenceManager::TheoryInferenceManager(Env& env, context::UserContext* u = userContext(); ProofNodeManager* pnm = env.getProofNodeManager(); d_defaultPg.reset( - new EagerProofGenerator(pnm, u, statsName + "EagerProofGenerator")); + new EagerProofGenerator(env, u, statsName + "EagerProofGenerator")); if (options().proof.proofAnnotate) { d_iipa.reset(new InferenceIdProofAnnotator(pnm, u)); diff --git a/src/theory/theory_preprocessor.cpp b/src/theory/theory_preprocessor.cpp index 0f099239c..81a226b2e 100644 --- a/src/theory/theory_preprocessor.cpp +++ b/src/theory/theory_preprocessor.cpp @@ -44,19 +44,19 @@ TheoryPreprocessor::TheoryPreprocessor(Env& env, TheoryEngine& engine) { context::Context* u = userContext(); d_tpg.reset( - new TConvProofGenerator(pnm, + new TConvProofGenerator(env, u, TConvPolicy::FIXPOINT, TConvCachePolicy::NEVER, "TheoryPreprocessor::preprocess_rewrite", &d_rtfc)); - d_tpgRew.reset(new TConvProofGenerator(pnm, + d_tpgRew.reset(new TConvProofGenerator(env, u, TConvPolicy::ONCE, TConvCachePolicy::NEVER, "TheoryPreprocessor::pprew")); d_lp.reset( - new LazyCDProof(pnm, nullptr, u, "TheoryPreprocessor::LazyCDProof")); + new LazyCDProof(env, nullptr, u, "TheoryPreprocessor::LazyCDProof")); // Make the main term conversion sequence generator, which tracks up to // three conversions made in succession: // (1) rewriting @@ -147,7 +147,8 @@ TrustNode TheoryPreprocessor::preprocessInternal( // node -> irNode via rewriting // irNode -> ppNode via theory-preprocessing + rewriting + tf removal tret = d_tspg->mkTrustRewriteSequence(cterms); - tret.debugCheckClosed("tpp-debug", "TheoryPreprocessor::lemma_ret"); + tret.debugCheckClosed( + options(), "tpp-debug", "TheoryPreprocessor::lemma_ret"); } else { @@ -479,8 +480,8 @@ void TheoryPreprocessor::registerTrustedRewrite(TrustNode trn, { Trace("tpp-debug") << "TheoryPreprocessor: addRewriteStep (generator) " << term << " -> " << termr << std::endl; - trn.debugCheckClosed("tpp-debug", - "TheoryPreprocessor::preprocessWithProof"); + trn.debugCheckClosed( + options(), "tpp-debug", "TheoryPreprocessor::preprocessWithProof"); // always use term context hash 0 (default) pg->addRewriteStep( term, termr, trn.getGenerator(), isPre, PfRule::ASSUME, true, tctx); diff --git a/src/theory/trust_substitutions.cpp b/src/theory/trust_substitutions.cpp index f46e6399e..68cf05de7 100644 --- a/src/theory/trust_substitutions.cpp +++ b/src/theory/trust_substitutions.cpp @@ -15,17 +15,19 @@ #include "theory/trust_substitutions.h" +#include "smt/env.h" #include "theory/rewriter.h" namespace cvc5::internal { namespace theory { -TrustSubstitutionMap::TrustSubstitutionMap(context::Context* c, - ProofNodeManager* pnm, +TrustSubstitutionMap::TrustSubstitutionMap(Env& env, + context::Context* c, std::string name, PfRule trustId, MethodId ids) - : d_ctx(c), + : EnvObj(env), + d_ctx(c), d_subs(c), d_tsubs(c), d_tspb(nullptr), @@ -37,21 +39,15 @@ TrustSubstitutionMap::TrustSubstitutionMap(context::Context* c, d_ids(ids), d_eqtIndex(c) { - setProofNodeManager(pnm); -} - -void TrustSubstitutionMap::setProofNodeManager(ProofNodeManager* pnm) -{ + ProofNodeManager* pnm = d_env.getProofNodeManager(); if (pnm != nullptr) { - // should not set the proof node manager more than once - Assert(d_tspb == nullptr); - d_tspb.reset(new TheoryProofStepBuffer(pnm->getChecker())), - d_subsPg.reset(new LazyCDProof( - pnm, nullptr, d_ctx, "TrustSubstitutionMap::subsPg")); + d_tspb.reset(new TheoryProofStepBuffer(pnm->getChecker())); + d_subsPg.reset( + new LazyCDProof(env, nullptr, d_ctx, "TrustSubstitutionMap::subsPg")); d_applyPg.reset( - new LazyCDProof(pnm, nullptr, d_ctx, "TrustSubstitutionMap::applyPg")); - d_helperPf.reset(new CDProofSet(pnm, d_ctx)); + new LazyCDProof(env, nullptr, d_ctx, "TrustSubstitutionMap::applyPg")); + d_helperPf.reset(new CDProofSet(env, d_ctx)); } } diff --git a/src/theory/trust_substitutions.h b/src/theory/trust_substitutions.h index 1428b9391..98b28df39 100644 --- a/src/theory/trust_substitutions.h +++ b/src/theory/trust_substitutions.h @@ -36,18 +36,16 @@ namespace theory { /** * A layer on top of SubstitutionMap that tracks proofs. */ -class TrustSubstitutionMap : public ProofGenerator +class TrustSubstitutionMap : protected EnvObj, public ProofGenerator { using NodeUIntMap = context::CDHashMap; public: - TrustSubstitutionMap(context::Context* c, - ProofNodeManager* pnm = nullptr, + TrustSubstitutionMap(Env& env, + context::Context* c, std::string name = "TrustSubstitutionMap", PfRule trustId = PfRule::PREPROCESS_LEMMA, MethodId ids = MethodId::SB_DEFAULT); - /** Set proof node manager */ - void setProofNodeManager(ProofNodeManager* pnm); /** Gets a reference to the underlying substitution map */ SubstitutionMap& get(); /** diff --git a/src/theory/uf/lambda_lift.cpp b/src/theory/uf/lambda_lift.cpp index 7e1823dfc..3188e3e83 100644 --- a/src/theory/uf/lambda_lift.cpp +++ b/src/theory/uf/lambda_lift.cpp @@ -31,9 +31,9 @@ LambdaLift::LambdaLift(Env& env) : EnvObj(env), d_lifted(userContext()), d_lambdaMap(userContext()), - d_epg(env.isTheoryProofProducing() ? new EagerProofGenerator( - env.getProofNodeManager(), userContext(), "LambdaLift::epg") - : nullptr) + d_epg(env.isTheoryProofProducing() + ? new EagerProofGenerator(env, userContext(), "LambdaLift::epg") + : nullptr) { } diff --git a/src/theory/uf/proof_equality_engine.cpp b/src/theory/uf/proof_equality_engine.cpp index b7d265a8a..6993bc242 100644 --- a/src/theory/uf/proof_equality_engine.cpp +++ b/src/theory/uf/proof_equality_engine.cpp @@ -31,15 +31,11 @@ namespace theory { namespace eq { ProofEqEngine::ProofEqEngine(Env& env, EqualityEngine& ee) - : EnvObj(env), - EagerProofGenerator(env.getProofNodeManager(), - env.getUserContext(), - "pfee::" + ee.identify()), + : EagerProofGenerator(env, env.getUserContext(), "pfee::" + ee.identify()), d_ee(ee), - d_factPg(env.getContext(), env.getProofNodeManager()), + d_factPg(env, env.getContext()), d_assumpPg(env.getProofNodeManager()), - d_pnm(env.getProofNodeManager()), - d_proof(env.getProofNodeManager(), + d_proof(env, nullptr, env.getContext(), "pfee::LazyCDProof::" + ee.identify()), @@ -226,7 +222,7 @@ TrustNode ProofEqEngine::assertLemma(Node conc, << ", exp = " << exp << ", noExplain = " << noExplain << ", args = " << args << std::endl; Assert(conc != d_true); - LazyCDProof tmpProof(d_pnm, &d_proof); + LazyCDProof tmpProof(d_env, &d_proof); LazyCDProof* curr; TrustNodeKind tnk; // same policy as above: for conflicts, use existing lazy proof @@ -245,7 +241,7 @@ TrustNode ProofEqEngine::assertLemma(Node conc, explainVecWithProof(tnk, assumps, exp, noExplain, curr); // Register the proof step. We use a separate lazy CDProof which will make // calls to curr above for the proofs of the literals in exp. - LazyCDProof outer(d_pnm, curr); + LazyCDProof outer(d_env, curr); if (!outer.addStep(conc, id, exp, args)) { // a step went wrong, e.g. during checking @@ -265,7 +261,7 @@ TrustNode ProofEqEngine::assertLemma(Node conc, Trace("pfee") << "pfee::assertLemma " << conc << ", exp = " << exp << ", noExplain = " << noExplain << " via generator" << std::endl; - LazyCDProof tmpProof(d_pnm, &d_proof); + LazyCDProof tmpProof(d_env, &d_proof); LazyCDProof* curr; TrustNodeKind tnk; // same policy as above: for conflicts, use existing lazy proof @@ -286,7 +282,7 @@ TrustNode ProofEqEngine::assertLemma(Node conc, // "skeleton" that is the base of the proof we are constructing. The call to // LazyCDProofChain::getProofFor will expand the leaves of this proof via // calls to curr. - LazyCDProofChain outer(d_pnm, true, nullptr, curr, false); + LazyCDProofChain outer(d_env, true, nullptr, curr, false); outer.addLazyStep(conc, pg); return ensureProofForFact(conc, assumps, tnk, &outer); } @@ -294,7 +290,7 @@ TrustNode ProofEqEngine::assertLemma(Node conc, TrustNode ProofEqEngine::explain(Node conc) { Trace("pfee") << "pfee::explain " << conc << std::endl; - LazyCDProof tmpProof(d_pnm, &d_proof); + LazyCDProof tmpProof(d_env, &d_proof); std::vector assumps; explainWithProof(conc, assumps, &tmpProof); return ensureProofForFact(conc, assumps, TrustNodeKind::PROP_EXP, &tmpProof); @@ -357,7 +353,8 @@ TrustNode ProofEqEngine::ensureProofForFact(Node conc, return TrustNode::null(); } // clone it so that we have a fresh copy - pfBody = d_pnm->clone(pfBody); + ProofNodeManager* pnm = d_env.getProofNodeManager(); + pfBody = pnm->clone(pfBody); Trace("pfee-proof") << "pfee::ensureProofForFact: add scope" << std::endl; // The free assumptions must be closed by assumps, which should be passed // as arguments of SCOPE. However, some of the free assumptions may not @@ -381,7 +378,7 @@ TrustNode ProofEqEngine::ensureProofForFact(Node conc, } // Scope the proof constructed above, and connect the formula with the proof // minimize the assumptions. - pf = d_pnm->mkScope(pfBody, scopeAssumps, true, true); + pf = pnm->mkScope(pfBody, scopeAssumps, true, true); // If we have no assumptions, and are proving an explanation for propagation if (scopeAssumps.empty() && tnk == TrustNodeKind::PROP_EXP) { @@ -391,7 +388,7 @@ TrustNode ProofEqEngine::ensureProofForFact(Node conc, // minimize here, since we already ensured the proof was closed above, and // we do not want to minimize, or else "true" would be omitted. scopeAssumps.push_back(nm->mkConst(true)); - pf = d_pnm->mkScope(pf, scopeAssumps, false); + pf = pnm->mkScope(pf, scopeAssumps, false); } exp = nm->mkAnd(scopeAssumps); // Make the lemma or conflict node. This must exactly match the conclusion diff --git a/src/theory/uf/proof_equality_engine.h b/src/theory/uf/proof_equality_engine.h index 52e9c18e8..78f23ee22 100644 --- a/src/theory/uf/proof_equality_engine.h +++ b/src/theory/uf/proof_equality_engine.h @@ -81,7 +81,7 @@ class EqualityEngine; * - explain, for explaining why a literal is true in the current state. * Details on these methods can be found below. */ -class ProofEqEngine : protected EnvObj, public EagerProofGenerator +class ProofEqEngine : public EagerProofGenerator { typedef context::CDHashSet NodeSet; typedef context::CDHashMap> NodeProofMap; @@ -287,8 +287,6 @@ class ProofEqEngine : protected EnvObj, public EagerProofGenerator /** common nodes */ Node d_true; Node d_false; - /** the proof node manager */ - ProofNodeManager* d_pnm; /** The SAT-context-dependent proof object */ LazyCDProof d_proof; /** diff --git a/test/unit/theory/theory_arith_coverings_white.cpp b/test/unit/theory/theory_arith_coverings_white.cpp index 7349aff5c..e0a591472 100644 --- a/test/unit/theory/theory_arith_coverings_white.cpp +++ b/test/unit/theory/theory_arith_coverings_white.cpp @@ -387,6 +387,7 @@ TEST_F(TestTheoryWhiteArithCoverings, test_cdcac_proof_1) opts.writeSmt().produceProofs = true; Env env(NodeManager::currentNM(), &opts); smt::PfManager pfm(env); + env.finishInit(pfm.getProofNodeManager()); EXPECT_TRUE(env.isTheoryProofProducing()); // register checkers that we need builtin::BuiltinProofRuleChecker btchecker(env);