From dfd844226c4cc6c6d2af78ef6291b0a9d087f4d4 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 18 Aug 2021 15:13:21 -0500 Subject: [PATCH] Make TheoryProxy use Env, simplify initialization of PropEngine (#7031) This simplifies our management of how/when proofs are enabled in the PropEngine. --- src/prop/prop_engine.cpp | 35 +++++++++++++---------------------- src/prop/prop_engine.h | 7 +------ src/prop/theory_proxy.cpp | 15 +++++++-------- src/prop/theory_proxy.h | 11 +++++++---- src/smt/env.cpp | 8 ++++++++ src/smt/env.h | 7 +++++++ src/smt/smt_engine.cpp | 2 -- src/smt/smt_solver.cpp | 12 +++++------- src/smt/smt_solver.h | 10 ---------- 9 files changed, 48 insertions(+), 59 deletions(-) diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index 0308715e6..dd22416db 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -65,16 +65,13 @@ public: } }; -PropEngine::PropEngine(TheoryEngine* te, - Env& env, - ProofNodeManager* pnm) +PropEngine::PropEngine(TheoryEngine* te, Env& env) : d_inCheckSat(false), d_theoryEngine(te), d_env(env), d_skdm(new SkolemDefManager(d_env.getContext(), d_env.getUserContext())), d_theoryProxy(nullptr), d_satSolver(nullptr), - d_pnm(pnm), d_cnfStream(nullptr), d_pfCnfStream(nullptr), d_ppm(nullptr), @@ -84,6 +81,7 @@ PropEngine::PropEngine(TheoryEngine* te, Debug("prop") << "Constructing the PropEngine" << std::endl; context::Context* satContext = d_env.getContext(); context::UserContext* userContext = d_env.getUserContext(); + ProofNodeManager* pnm = d_env.getProofNodeManager(); ResourceManager* rm = d_env.getResourceManager(); options::DecisionMode dmode = options::decisionMode(); @@ -107,13 +105,8 @@ PropEngine::PropEngine(TheoryEngine* te, // CNF stream and theory proxy required pointers to each other, make the // theory proxy first - d_theoryProxy = new TheoryProxy(this, - d_theoryEngine, - d_decisionEngine.get(), - d_skdm.get(), - satContext, - userContext, - pnm); + d_theoryProxy = new TheoryProxy( + this, d_theoryEngine, d_decisionEngine.get(), d_skdm.get(), d_env); d_cnfStream = new CnfStream(d_satSolver, d_theoryProxy, userContext, @@ -124,17 +117,15 @@ PropEngine::PropEngine(TheoryEngine* te, // connect theory proxy d_theoryProxy->finishInit(d_cnfStream); + bool satProofs = d_env.isSatProofProducing(); // connect SAT solver - d_satSolver->initialize( - d_env.getContext(), - d_theoryProxy, - d_env.getUserContext(), - options::unsatCoresMode() != options::UnsatCoresMode::ASSUMPTIONS - ? pnm - : nullptr); + d_satSolver->initialize(d_env.getContext(), + d_theoryProxy, + d_env.getUserContext(), + satProofs ? pnm : nullptr); d_decisionEngine->finishInit(d_satSolver, d_cnfStream); - if (pnm && options::unsatCoresMode() != options::UnsatCoresMode::ASSUMPTIONS) + if (satProofs) { d_pfCnfStream.reset(new ProofCnfStream( userContext, @@ -670,7 +661,7 @@ bool PropEngine::properExplanation(TNode node, TNode expl) const void PropEngine::checkProof(context::CDList* assertions) { - if (!d_pnm) + if (!d_env.isSatProofProducing()) { return; } @@ -681,7 +672,7 @@ ProofCnfStream* PropEngine::getProofCnfStream() { return d_pfCnfStream.get(); } std::shared_ptr PropEngine::getProof() { - if (!d_pnm) + if (!d_env.isSatProofProducing()) { return nullptr; } @@ -706,7 +697,7 @@ std::shared_ptr PropEngine::getRefutation() Assert(options::unsatCoresMode() == options::UnsatCoresMode::ASSUMPTIONS); std::vector core; getUnsatCore(core); - CDProof cdp(d_pnm); + CDProof cdp(d_env.getProofNodeManager()); Node fnode = NodeManager::currentNM()->mkConst(false); cdp.addStep(fnode, PfRule::SAT_REFUTATION, core, {}); return cdp.getProofFor(fnode); diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h index 4d06adfba..d26a425c8 100644 --- a/src/prop/prop_engine.h +++ b/src/prop/prop_engine.h @@ -56,9 +56,7 @@ class PropEngine /** * Create a PropEngine with a particular decision and theory engine. */ - PropEngine(TheoryEngine* te, - Env& env, - ProofNodeManager* pnm); + PropEngine(TheoryEngine* te, Env& env); /** * Destructor. @@ -372,9 +370,6 @@ class PropEngine /** List of all of the assertions that need to be made */ std::vector d_assertionList; - /** A pointer to the proof node maneger to be used by this engine. */ - ProofNodeManager* d_pnm; - /** The CNF converter in use */ CnfStream* d_cnfStream; /** Proof-producing CNF converter */ diff --git a/src/prop/theory_proxy.cpp b/src/prop/theory_proxy.cpp index 47263af97..b4bc7fa60 100644 --- a/src/prop/theory_proxy.cpp +++ b/src/prop/theory_proxy.cpp @@ -24,6 +24,7 @@ #include "prop/cnf_stream.h" #include "prop/prop_engine.h" #include "prop/skolem_def_manager.h" +#include "smt/env.h" #include "smt/smt_statistics_registry.h" #include "theory/rewriter.h" #include "theory/theory_engine.h" @@ -36,16 +37,15 @@ TheoryProxy::TheoryProxy(PropEngine* propEngine, TheoryEngine* theoryEngine, decision::DecisionEngine* decisionEngine, SkolemDefManager* skdm, - context::Context* context, - context::UserContext* userContext, - ProofNodeManager* pnm) + Env& env) : d_propEngine(propEngine), d_cnfStream(nullptr), d_decisionEngine(decisionEngine), d_theoryEngine(theoryEngine), - d_queue(context), - d_tpp(*theoryEngine, userContext, pnm), - d_skdm(skdm) + d_queue(env.getContext()), + d_tpp(*theoryEngine, env.getUserContext(), env.getProofNodeManager()), + d_skdm(skdm), + d_env(env) { } @@ -98,8 +98,7 @@ void TheoryProxy::explainPropagation(SatLiteral l, SatClause& explanation) { TrustNode tte = d_theoryEngine->getExplanation(lNode); Node theoryExplanation = tte.getNode(); - if (options::produceProofs() - && options::unsatCoresMode() != options::UnsatCoresMode::ASSUMPTIONS) + if (d_env.isTheoryProofProducing()) { Assert(options::unsatCoresMode() != options::UnsatCoresMode::FULL_PROOF || tte.getGenerator()); diff --git a/src/prop/theory_proxy.h b/src/prop/theory_proxy.h index f988c00e2..0e54ff8c9 100644 --- a/src/prop/theory_proxy.h +++ b/src/prop/theory_proxy.h @@ -35,10 +35,12 @@ namespace cvc5 { +class Env; +class TheoryEngine; + namespace decision { class DecisionEngine; } -class TheoryEngine; namespace prop { @@ -56,9 +58,7 @@ class TheoryProxy : public Registrar TheoryEngine* theoryEngine, decision::DecisionEngine* decisionEngine, SkolemDefManager* skdm, - context::Context* context, - context::UserContext* userContext, - ProofNodeManager* pnm); + Env& env); ~TheoryProxy(); @@ -162,6 +162,9 @@ class TheoryProxy : public Registrar /** The skolem definition manager */ SkolemDefManager* d_skdm; + + /** Reference to the environment */ + Env& d_env; }; /* class TheoryProxy */ } // namespace prop diff --git a/src/smt/env.cpp b/src/smt/env.cpp index 3ec9899ad..d6677c343 100644 --- a/src/smt/env.cpp +++ b/src/smt/env.cpp @@ -85,6 +85,14 @@ ProofNodeManager* Env::getProofNodeManager() { return d_proofNodeManager; } const std::string& Env::getFilename() const { return d_filename; } +bool Env::isSatProofProducing() const +{ + return d_proofNodeManager != nullptr + && (!d_options.smt.unsatCores + || d_options.smt.unsatCoresMode + != options::UnsatCoresMode::ASSUMPTIONS); +} + bool Env::isTheoryProofProducing() const { return d_proofNodeManager != nullptr diff --git a/src/smt/env.h b/src/smt/env.h index 9887aea08..68148ec00 100644 --- a/src/smt/env.h +++ b/src/smt/env.h @@ -85,6 +85,13 @@ class Env /** Return the input name, or the empty string if not set */ const std::string& getFilename() const; + /** + * Check whether the SAT solver should produce proofs. Other than whether + * the proof node manager is set, SAT proofs are only generated when the + * unsat core mode is not ASSUMPTIONS. + */ + bool isSatProofProducing() const; + /** * Check whether theories should produce proofs as well. Other than whether * the proof node manager is set, theory engine proofs are conditioned on the diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 43177a73a..78bb9044a 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -213,8 +213,6 @@ void SmtEngine::finishInit() d_env->setProofNodeManager(pnm); // enable it in the assertions pipeline d_asserts->setProofGenerator(pppg); - // enable it in the SmtSolver - d_smtSolver->setProofNodeManager(pnm); // enabled proofs in the preprocessor d_pp->setProofGenerator(pppg); } diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp index 1014b218d..214193b00 100644 --- a/src/smt/smt_solver.cpp +++ b/src/smt/smt_solver.cpp @@ -40,7 +40,6 @@ SmtSolver::SmtSolver(Env& env, d_state(state), d_pp(pp), d_stats(stats), - d_pnm(nullptr), d_theoryEngine(nullptr), d_propEngine(nullptr) { @@ -61,16 +60,17 @@ void SmtSolver::finishInit(const LogicInfo& logicInfo) theory::TheoryConstructor::addTheory(d_theoryEngine.get(), id); } // Add the proof checkers for each theory - if (d_pnm) + ProofNodeManager* pnm = d_env.getProofNodeManager(); + if (pnm) { - d_theoryEngine->initializeProofChecker(d_pnm->getChecker()); + d_theoryEngine->initializeProofChecker(pnm->getChecker()); } Trace("smt-debug") << "Making prop engine..." << std::endl; /* force destruction of referenced PropEngine to enforce that statistics * are unregistered by the obsolete PropEngine object before registered * again by the new PropEngine object */ d_propEngine.reset(nullptr); - d_propEngine.reset(new prop::PropEngine(d_theoryEngine.get(), d_env, d_pnm)); + d_propEngine.reset(new prop::PropEngine(d_theoryEngine.get(), d_env)); Trace("smt-debug") << "Setting up theory engine..." << std::endl; d_theoryEngine->setPropEngine(getPropEngine()); @@ -86,7 +86,7 @@ void SmtSolver::resetAssertions() * statistics are unregistered by the obsolete PropEngine object before * registered again by the new PropEngine object */ d_propEngine.reset(nullptr); - d_propEngine.reset(new prop::PropEngine(d_theoryEngine.get(), d_env, d_pnm)); + d_propEngine.reset(new prop::PropEngine(d_theoryEngine.get(), d_env)); d_theoryEngine->setPropEngine(getPropEngine()); // Notice that we do not reset TheoryEngine, nor does it require calling // finishInit again. In particular, TheoryEngine::finishInit does not @@ -236,8 +236,6 @@ void SmtSolver::processAssertions(Assertions& as) as.clearCurrent(); } -void SmtSolver::setProofNodeManager(ProofNodeManager* pnm) { d_pnm = pnm; } - TheoryEngine* SmtSolver::getTheoryEngine() { return d_theoryEngine.get(); } prop::PropEngine* SmtSolver::getPropEngine() { return d_propEngine.get(); } diff --git a/src/smt/smt_solver.h b/src/smt/smt_solver.h index cf82d9309..cdc98606c 100644 --- a/src/smt/smt_solver.h +++ b/src/smt/smt_solver.h @@ -114,11 +114,6 @@ class SmtSolver * into the SMT solver, and clears the buffer. */ void processAssertions(Assertions& as); - /** - * Set proof node manager. Enables proofs in this SmtSolver. Should be - * called before finishInit. - */ - void setProofNodeManager(ProofNodeManager* pnm); //------------------------------------------ access methods /** Get a pointer to the TheoryEngine owned by this solver. */ TheoryEngine* getTheoryEngine(); @@ -139,11 +134,6 @@ class SmtSolver Preprocessor& d_pp; /** Reference to the statistics of SmtEngine */ SmtEngineStatistics& d_stats; - /** - * Pointer to the proof node manager used by this SmtSolver. A non-null - * proof node manager indicates that proofs are enabled. - */ - ProofNodeManager* d_pnm; /** The theory engine */ std::unique_ptr d_theoryEngine; /** The propositional engine */ -- 2.30.2