diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-08-18 15:13:21 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-08-18 15:13:21 -0500 |
commit | dfd844226c4cc6c6d2af78ef6291b0a9d087f4d4 (patch) | |
tree | 47853884475eefcdad531e6ea6edc274d63abcf1 /src/prop | |
parent | 42b8e0a4fc5b23dfce79cbadc08a8aa8542997e0 (diff) |
Make TheoryProxy use Env, simplify initialization of PropEngine (#7031)
This simplifies our management of how/when proofs are enabled in the PropEngine.
Diffstat (limited to 'src/prop')
-rw-r--r-- | src/prop/prop_engine.cpp | 35 | ||||
-rw-r--r-- | src/prop/prop_engine.h | 7 | ||||
-rw-r--r-- | src/prop/theory_proxy.cpp | 15 | ||||
-rw-r--r-- | src/prop/theory_proxy.h | 11 |
4 files changed, 28 insertions, 40 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<Node>* assertions) { - if (!d_pnm) + if (!d_env.isSatProofProducing()) { return; } @@ -681,7 +672,7 @@ ProofCnfStream* PropEngine::getProofCnfStream() { return d_pfCnfStream.get(); } std::shared_ptr<ProofNode> PropEngine::getProof() { - if (!d_pnm) + if (!d_env.isSatProofProducing()) { return nullptr; } @@ -706,7 +697,7 @@ std::shared_ptr<ProofNode> PropEngine::getRefutation() Assert(options::unsatCoresMode() == options::UnsatCoresMode::ASSUMPTIONS); std::vector<Node> 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<Node> 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 |