From: Andrew Reynolds Date: Fri, 22 Oct 2021 16:56:05 +0000 (-0500) Subject: Refactor theory inference manager constructor (#7457) X-Git-Tag: cvc5-1.0.0~1005 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=5d0bc27685611a9ee738507a45f5b68b6da42d8a;p=cvc5.git Refactor theory inference manager constructor (#7457) Eliminates a style where proof node manager was passed as an argument to indicate proofs enabled if non-null. All theory inference managers now check Env::isTheoryProofProducing instead. Since BV did not pass a proof node manager to its inference manager, this PR also incidentally enables equality engine proofs for BV. --- diff --git a/src/theory/arith/inference_manager.cpp b/src/theory/arith/inference_manager.cpp index 0c6b18893..670f38c40 100644 --- a/src/theory/arith/inference_manager.cpp +++ b/src/theory/arith/inference_manager.cpp @@ -26,9 +26,8 @@ namespace arith { InferenceManager::InferenceManager(Env& env, TheoryArith& ta, - ArithState& astate, - ProofNodeManager* pnm) - : InferenceManagerBuffered(env, ta, astate, pnm, "theory::arith::"), + ArithState& astate) + : InferenceManagerBuffered(env, ta, astate, "theory::arith::"), // currently must track propagated literals if using the equality solver d_trackPropLits(options().arith.arithEqSolver), d_propLits(context()) diff --git a/src/theory/arith/inference_manager.h b/src/theory/arith/inference_manager.h index d327106d7..11532fd72 100644 --- a/src/theory/arith/inference_manager.h +++ b/src/theory/arith/inference_manager.h @@ -46,10 +46,7 @@ class InferenceManager : public InferenceManagerBuffered using NodeSet = context::CDHashSet; public: - InferenceManager(Env& env, - TheoryArith& ta, - ArithState& astate, - ProofNodeManager* pnm); + InferenceManager(Env& env, TheoryArith& ta, ArithState& astate); /** * Add a lemma as pending lemma to this inference manager. diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index cf2373b9f..583b53d5e 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -40,7 +40,7 @@ TheoryArith::TheoryArith(Env& env, OutputChannel& out, Valuation valuation) d_ppRewriteTimer( statisticsRegistry().registerTimer("theory::arith::ppRewriteTimer")), d_astate(env, valuation), - d_im(env, *this, d_astate, d_pnm), + d_im(env, *this, d_astate), d_ppre(d_env), d_bab(env, d_astate, d_im, d_ppre, d_pnm), d_eqSolver(nullptr), diff --git a/src/theory/arrays/inference_manager.cpp b/src/theory/arrays/inference_manager.cpp index 4eef9a018..caef4502b 100644 --- a/src/theory/arrays/inference_manager.cpp +++ b/src/theory/arrays/inference_manager.cpp @@ -27,13 +27,12 @@ namespace cvc5 { namespace theory { namespace arrays { -InferenceManager::InferenceManager(Env& env, - Theory& t, - TheoryState& state, - ProofNodeManager* pnm) - : TheoryInferenceManager(env, t, state, pnm, "theory::arrays::", false), - d_lemmaPg(pnm ? new EagerProofGenerator( - pnm, userContext(), "ArrayLemmaProofGenerator") +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) { } diff --git a/src/theory/arrays/inference_manager.h b/src/theory/arrays/inference_manager.h index 899df0a6b..f0e3bfe90 100644 --- a/src/theory/arrays/inference_manager.h +++ b/src/theory/arrays/inference_manager.h @@ -33,10 +33,7 @@ namespace arrays { class InferenceManager : public TheoryInferenceManager { public: - InferenceManager(Env& env, - Theory& t, - TheoryState& state, - ProofNodeManager* pnm); + InferenceManager(Env& env, Theory& t, TheoryState& state); ~InferenceManager() {} /** diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index 93eadde43..97cbec1d5 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -81,7 +81,7 @@ TheoryArrays::TheoryArrays(Env& env, d_ppFacts(userContext()), d_rewriter(env.getRewriter(), d_pnm), d_state(env, valuation), - d_im(env, *this, d_state, d_pnm), + d_im(env, *this, d_state), d_literalsToPropagate(context()), d_literalsToPropagateIndex(context(), 0), d_isPreRegistered(context()), diff --git a/src/theory/bags/inference_manager.cpp b/src/theory/bags/inference_manager.cpp index ee25861be..92f5dfd82 100644 --- a/src/theory/bags/inference_manager.cpp +++ b/src/theory/bags/inference_manager.cpp @@ -24,11 +24,8 @@ namespace cvc5 { namespace theory { namespace bags { -InferenceManager::InferenceManager(Env& env, - Theory& t, - SolverState& s, - ProofNodeManager* pnm) - : InferenceManagerBuffered(env, t, s, pnm, "theory::bags::"), d_state(s) +InferenceManager::InferenceManager(Env& env, Theory& t, SolverState& s) + : InferenceManagerBuffered(env, t, s, "theory::bags::"), d_state(s) { d_true = NodeManager::currentNM()->mkConst(true); d_false = NodeManager::currentNM()->mkConst(false); diff --git a/src/theory/bags/inference_manager.h b/src/theory/bags/inference_manager.h index a9e8d9121..45827f27b 100644 --- a/src/theory/bags/inference_manager.h +++ b/src/theory/bags/inference_manager.h @@ -38,7 +38,7 @@ class InferenceManager : public InferenceManagerBuffered typedef context::CDHashSet NodeSet; public: - InferenceManager(Env& env, Theory& t, SolverState& s, ProofNodeManager* pnm); + InferenceManager(Env& env, Theory& t, SolverState& s); /** * Do pending method. This processes all pending facts, lemmas and pending diff --git a/src/theory/bags/theory_bags.cpp b/src/theory/bags/theory_bags.cpp index 004766d83..4a6d345e9 100644 --- a/src/theory/bags/theory_bags.cpp +++ b/src/theory/bags/theory_bags.cpp @@ -30,7 +30,7 @@ namespace bags { TheoryBags::TheoryBags(Env& env, OutputChannel& out, Valuation valuation) : Theory(THEORY_BAGS, env, out, valuation), d_state(env, valuation), - d_im(env, *this, d_state, d_pnm), + d_im(env, *this, d_state), d_ig(&d_state, &d_im), d_notify(*this, d_im), d_statistics(), diff --git a/src/theory/builtin/theory_builtin.cpp b/src/theory/builtin/theory_builtin.cpp index cd3b27b6e..e519cbed7 100644 --- a/src/theory/builtin/theory_builtin.cpp +++ b/src/theory/builtin/theory_builtin.cpp @@ -29,7 +29,7 @@ TheoryBuiltin::TheoryBuiltin(Env& env, OutputChannel& out, Valuation valuation) : Theory(THEORY_BUILTIN, env, out, valuation), d_checker(env), d_state(env, valuation), - d_im(env, *this, d_state, d_pnm, "theory::builtin::") + d_im(env, *this, d_state, "theory::builtin::") { // indicate we are using the default theory state and inference managers d_theoryState = &d_state; diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index f027b56fe..8e9c2da5b 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -40,7 +40,7 @@ TheoryBV::TheoryBV(Env& env, d_internal(nullptr), d_rewriter(), d_state(env, valuation), - d_im(env, *this, d_state, nullptr, "theory::bv::"), + d_im(env, *this, d_state, "theory::bv::"), d_notify(d_im), d_invalidateModelCache(context(), true), d_stats(statisticsRegistry(), "theory::bv::") diff --git a/src/theory/datatypes/inference_manager.cpp b/src/theory/datatypes/inference_manager.cpp index 16a621012..fef85f4c6 100644 --- a/src/theory/datatypes/inference_manager.cpp +++ b/src/theory/datatypes/inference_manager.cpp @@ -30,16 +30,16 @@ namespace cvc5 { namespace theory { namespace datatypes { -InferenceManager::InferenceManager(Env& env, - Theory& t, - TheoryState& state, - ProofNodeManager* pnm) - : InferenceManagerBuffered(env, t, state, pnm, "theory::datatypes::"), - d_pnm(pnm), - d_ipc(pnm == nullptr ? nullptr : new InferProofCons(context(), pnm)), - d_lemPg(pnm == nullptr ? nullptr - : new EagerProofGenerator( - pnm, userContext(), "datatypes::lemPg")) +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_false = NodeManager::currentNM()->mkConst(false); } @@ -103,15 +103,14 @@ void InferenceManager::sendDtConflict(const std::vector& conf, InferenceId conflictExp(id, conf, d_ipc.get()); } -bool InferenceManager::isProofEnabled() const { return d_ipc != nullptr; } - TrustNode InferenceManager::processDtLemma(Node conc, Node exp, InferenceId id) { // set up a proof constructor std::shared_ptr ipcl; if (isProofEnabled()) { - ipcl = std::make_shared(nullptr, d_pnm); + ipcl = + std::make_shared(nullptr, d_env.getProofNodeManager()); } conc = prepareDtInference(conc, exp, id, ipcl.get()); // send it as a lemma @@ -133,7 +132,7 @@ TrustNode InferenceManager::processDtLemma(Node conc, Node exp, InferenceId id) { std::vector expv; expv.push_back(exp); - pn = d_pnm->mkScope(pbody, expv); + pn = d_env.getProofNodeManager()->mkScope(pbody, expv); } d_lemPg->setProofFor(lem, pn); } diff --git a/src/theory/datatypes/inference_manager.h b/src/theory/datatypes/inference_manager.h index 27e0e90b6..2616eb40a 100644 --- a/src/theory/datatypes/inference_manager.h +++ b/src/theory/datatypes/inference_manager.h @@ -38,10 +38,7 @@ class InferenceManager : public InferenceManagerBuffered friend class DatatypesInference; public: - InferenceManager(Env& env, - Theory& t, - TheoryState& state, - ProofNodeManager* pnm); + InferenceManager(Env& env, Theory& t, TheoryState& state); ~InferenceManager(); /** * Add pending inference, which may be processed as either a fact or @@ -78,8 +75,6 @@ class InferenceManager : public InferenceManagerBuffered void sendDtConflict(const std::vector& conf, InferenceId id); private: - /** Are proofs enabled? */ - bool isProofEnabled() const; /** * Process datatype inference as a lemma */ @@ -103,8 +98,6 @@ class InferenceManager : public InferenceManagerBuffered Node prepareDtInference(Node conc, Node exp, InferenceId id, InferProofCons* ipc); /** The false node */ Node d_false; - /** Pointer to the proof node manager */ - ProofNodeManager* d_pnm; /** The inference to proof converter */ std::unique_ptr d_ipc; /** An eager proof generator for lemmas */ diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index 0cbeaa515..fe48aa59d 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -63,7 +63,7 @@ TheoryDatatypes::TheoryDatatypes(Env& env, d_sygusExtension(nullptr), d_rewriter(env.getEvaluator()), d_state(env, valuation), - d_im(env, *this, d_state, d_pnm), + d_im(env, *this, d_state), d_notify(d_im, *this) { diff --git a/src/theory/fp/theory_fp.cpp b/src/theory/fp/theory_fp.cpp index d38b6d0fa..8364aa81b 100644 --- a/src/theory/fp/theory_fp.cpp +++ b/src/theory/fp/theory_fp.cpp @@ -68,7 +68,7 @@ TheoryFp::TheoryFp(Env& env, OutputChannel& out, Valuation valuation) d_abstractionMap(userContext()), d_rewriter(userContext()), d_state(env, valuation), - d_im(env, *this, d_state, d_pnm, "theory::fp::", true), + d_im(env, *this, d_state, "theory::fp::", true), d_wbFactsCache(userContext()), d_true(d_env.getNodeManager()->mkConst(true)) { diff --git a/src/theory/inference_manager_buffered.cpp b/src/theory/inference_manager_buffered.cpp index 5b0dac776..d38fcf3e3 100644 --- a/src/theory/inference_manager_buffered.cpp +++ b/src/theory/inference_manager_buffered.cpp @@ -27,10 +27,9 @@ namespace theory { InferenceManagerBuffered::InferenceManagerBuffered(Env& env, Theory& t, TheoryState& state, - ProofNodeManager* pnm, const std::string& statsName, bool cacheLemmas) - : TheoryInferenceManager(env, t, state, pnm, statsName, cacheLemmas), + : TheoryInferenceManager(env, t, state, statsName, cacheLemmas), d_processingPendingLemmas(false) { } diff --git a/src/theory/inference_manager_buffered.h b/src/theory/inference_manager_buffered.h index 202948d26..e93152f72 100644 --- a/src/theory/inference_manager_buffered.h +++ b/src/theory/inference_manager_buffered.h @@ -35,7 +35,6 @@ class InferenceManagerBuffered : public TheoryInferenceManager InferenceManagerBuffered(Env& env, Theory& t, TheoryState& state, - ProofNodeManager* pnm, const std::string& statsName, bool cacheLemmas = true); virtual ~InferenceManagerBuffered() {} diff --git a/src/theory/quantifiers/instantiate.cpp b/src/theory/quantifiers/instantiate.cpp index be04f9404..f47a71926 100644 --- a/src/theory/quantifiers/instantiate.cpp +++ b/src/theory/quantifiers/instantiate.cpp @@ -46,18 +46,18 @@ Instantiate::Instantiate(Env& env, QuantifiersState& qs, QuantifiersInferenceManager& qim, QuantifiersRegistry& qr, - TermRegistry& tr, - ProofNodeManager* pnm) + TermRegistry& tr) : QuantifiersUtil(env), d_qstate(qs), d_qim(qim), d_qreg(qr), d_treg(tr), - d_pnm(pnm), d_insts(userContext()), d_c_inst_match_trie_dom(userContext()), - d_pfInst(pnm ? new CDProof(pnm, userContext(), "Instantiate::pfInst") - : nullptr) + d_pfInst(isProofEnabled() ? new CDProof(env.getProofNodeManager(), + userContext(), + "Instantiate::pfInst") + : nullptr) { } @@ -242,8 +242,10 @@ bool Instantiate::addInstantiation(Node q, std::shared_ptr pfTmp; if (isProofEnabled()) { - pfTmp.reset(new LazyCDProof( - d_pnm, nullptr, nullptr, "Instantiate::LazyCDProof::tmp")); + pfTmp.reset(new LazyCDProof(d_env.getProofNodeManager(), + nullptr, + nullptr, + "Instantiate::LazyCDProof::tmp")); } // construct the instantiation @@ -300,7 +302,8 @@ bool Instantiate::addInstantiation(Node q, // make the scope proof to get (=> q body) std::vector assumps; assumps.push_back(q); - std::shared_ptr pfns = d_pnm->mkScope({pfn}, assumps); + std::shared_ptr pfns = + d_env.getProofNodeManager()->mkScope({pfn}, assumps); Assert(assumps.size() == 1 && assumps[0] == q); // store in the main proof d_pfInst->addProof(pfns); @@ -688,7 +691,10 @@ void Instantiate::getInstantiations(Node q, std::vector& insts) } } -bool Instantiate::isProofEnabled() const { return d_pfInst != nullptr; } +bool Instantiate::isProofEnabled() const +{ + return d_env.isTheoryProofProducing(); +} void Instantiate::notifyEndRound() { diff --git a/src/theory/quantifiers/instantiate.h b/src/theory/quantifiers/instantiate.h index b4972a7b6..2e5bd1e2f 100644 --- a/src/theory/quantifiers/instantiate.h +++ b/src/theory/quantifiers/instantiate.h @@ -108,8 +108,7 @@ class Instantiate : public QuantifiersUtil QuantifiersState& qs, QuantifiersInferenceManager& qim, QuantifiersRegistry& qr, - TermRegistry& tr, - ProofNodeManager* pnm = nullptr); + TermRegistry& tr); ~Instantiate(); /** reset */ bool reset(Theory::Effort e) override; @@ -318,8 +317,6 @@ class Instantiate : public QuantifiersUtil QuantifiersRegistry& d_qreg; /** Reference to the term registry */ TermRegistry& d_treg; - /** pointer to the proof node manager */ - ProofNodeManager* d_pnm; /** instantiation rewriter classes */ std::vector d_instRewrite; diff --git a/src/theory/quantifiers/quantifiers_inference_manager.cpp b/src/theory/quantifiers/quantifiers_inference_manager.cpp index 20987b02e..f282b8d11 100644 --- a/src/theory/quantifiers/quantifiers_inference_manager.cpp +++ b/src/theory/quantifiers/quantifiers_inference_manager.cpp @@ -27,11 +27,10 @@ QuantifiersInferenceManager::QuantifiersInferenceManager( Theory& t, QuantifiersState& state, QuantifiersRegistry& qr, - TermRegistry& tr, - ProofNodeManager* pnm) - : InferenceManagerBuffered(env, t, state, pnm, "theory::quantifiers::"), - d_instantiate(new Instantiate(env, state, *this, qr, tr, pnm)), - d_skolemize(new Skolemize(env, state, tr, pnm)) + TermRegistry& tr) + : InferenceManagerBuffered(env, t, state, "theory::quantifiers::"), + d_instantiate(new Instantiate(env, state, *this, qr, tr)), + d_skolemize(new Skolemize(env, state, tr)) { } diff --git a/src/theory/quantifiers/quantifiers_inference_manager.h b/src/theory/quantifiers/quantifiers_inference_manager.h index 20981a795..abd8d0761 100644 --- a/src/theory/quantifiers/quantifiers_inference_manager.h +++ b/src/theory/quantifiers/quantifiers_inference_manager.h @@ -40,8 +40,7 @@ class QuantifiersInferenceManager : public InferenceManagerBuffered Theory& t, QuantifiersState& state, QuantifiersRegistry& qr, - TermRegistry& tr, - ProofNodeManager* pnm); + TermRegistry& tr); ~QuantifiersInferenceManager(); /** get instantiate utility */ Instantiate* getInstantiate(); diff --git a/src/theory/quantifiers/skolemize.cpp b/src/theory/quantifiers/skolemize.cpp index a34547f45..830847b74 100644 --- a/src/theory/quantifiers/skolemize.cpp +++ b/src/theory/quantifiers/skolemize.cpp @@ -36,18 +36,16 @@ namespace cvc5 { namespace theory { namespace quantifiers { -Skolemize::Skolemize(Env& env, - QuantifiersState& qs, - TermRegistry& tr, - ProofNodeManager* pnm) +Skolemize::Skolemize(Env& env, QuantifiersState& qs, TermRegistry& tr) : EnvObj(env), d_qstate(qs), d_treg(tr), d_skolemized(userContext()), - d_pnm(pnm), - d_epg(pnm == nullptr + d_epg(!isProofEnabled() ? nullptr - : new EagerProofGenerator(pnm, userContext(), "Skolemize::epg")) + : new EagerProofGenerator(env.getProofNodeManager(), + userContext(), + "Skolemize::epg")) { } @@ -397,7 +395,10 @@ void Skolemize::getSkolemTermVectors( } } -bool Skolemize::isProofEnabled() const { return d_epg != nullptr; } +bool Skolemize::isProofEnabled() const +{ + return d_env.isTheoryProofProducing(); +} } // namespace quantifiers } // namespace theory diff --git a/src/theory/quantifiers/skolemize.h b/src/theory/quantifiers/skolemize.h index 294ad0084..604bc60e4 100644 --- a/src/theory/quantifiers/skolemize.h +++ b/src/theory/quantifiers/skolemize.h @@ -69,10 +69,7 @@ class Skolemize : protected EnvObj typedef context::CDHashMap NodeNodeMap; public: - Skolemize(Env& env, - QuantifiersState& qs, - TermRegistry& tr, - ProofNodeManager* pnm); + Skolemize(Env& env, QuantifiersState& qs, TermRegistry& tr); ~Skolemize() {} /** skolemize quantified formula q * If the return value ret of this function is non-null, then ret is a trust diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp index 7e20c3a4a..bce827bbd 100644 --- a/src/theory/quantifiers/theory_quantifiers.cpp +++ b/src/theory/quantifiers/theory_quantifiers.cpp @@ -38,7 +38,7 @@ TheoryQuantifiers::TheoryQuantifiers(Env& env, d_qstate(env, valuation, logicInfo()), d_qreg(env), d_treg(env, d_qstate, d_qreg), - d_qim(env, *this, d_qstate, d_qreg, d_treg, d_pnm), + d_qim(env, *this, d_qstate, d_qreg, d_treg), d_qengine(nullptr) { // construct the quantifiers engine diff --git a/src/theory/sep/theory_sep.cpp b/src/theory/sep/theory_sep.cpp index 88851e407..ad41d8327 100644 --- a/src/theory/sep/theory_sep.cpp +++ b/src/theory/sep/theory_sep.cpp @@ -47,7 +47,7 @@ TheorySep::TheorySep(Env& env, OutputChannel& out, Valuation valuation) d_lemmas_produced_c(userContext()), d_bounds_init(false), d_state(env, valuation), - d_im(env, *this, d_state, d_pnm, "theory::sep::"), + d_im(env, *this, d_state, "theory::sep::"), d_notify(*this), d_reduce(userContext()), d_spatial_assertions(context()) diff --git a/src/theory/sets/inference_manager.cpp b/src/theory/sets/inference_manager.cpp index 58fcbdae9..15c4fd405 100644 --- a/src/theory/sets/inference_manager.cpp +++ b/src/theory/sets/inference_manager.cpp @@ -25,11 +25,8 @@ namespace cvc5 { namespace theory { namespace sets { -InferenceManager::InferenceManager(Env& env, - Theory& t, - SolverState& s, - ProofNodeManager* pnm) - : InferenceManagerBuffered(env, t, s, pnm, "theory::sets::"), d_state(s) +InferenceManager::InferenceManager(Env& env, Theory& t, SolverState& s) + : InferenceManagerBuffered(env, t, s, "theory::sets::"), d_state(s) { d_true = NodeManager::currentNM()->mkConst(true); d_false = NodeManager::currentNM()->mkConst(false); diff --git a/src/theory/sets/inference_manager.h b/src/theory/sets/inference_manager.h index a9016ac3d..36eec2cd3 100644 --- a/src/theory/sets/inference_manager.h +++ b/src/theory/sets/inference_manager.h @@ -39,7 +39,7 @@ class InferenceManager : public InferenceManagerBuffered typedef context::CDHashSet NodeSet; public: - InferenceManager(Env& env, Theory& t, SolverState& s, ProofNodeManager* pnm); + InferenceManager(Env& env, Theory& t, SolverState& s); /** * Add facts corresponding to ( exp => fact ) via calls to the assertFact * method of TheorySetsPrivate. diff --git a/src/theory/sets/theory_sets.cpp b/src/theory/sets/theory_sets.cpp index 833f4b22d..2901703dd 100644 --- a/src/theory/sets/theory_sets.cpp +++ b/src/theory/sets/theory_sets.cpp @@ -31,7 +31,7 @@ TheorySets::TheorySets(Env& env, OutputChannel& out, Valuation valuation) : Theory(THEORY_SETS, env, out, valuation), d_skCache(), d_state(env, valuation, d_skCache), - d_im(env, *this, d_state, d_pnm), + d_im(env, *this, d_state), d_internal( new TheorySetsPrivate(env, *this, d_state, d_im, d_skCache, d_pnm)), d_notify(*d_internal.get(), d_im) diff --git a/src/theory/strings/inference_manager.cpp b/src/theory/strings/inference_manager.cpp index 1f531a97c..a4f100c19 100644 --- a/src/theory/strings/inference_manager.cpp +++ b/src/theory/strings/inference_manager.cpp @@ -35,15 +35,20 @@ InferenceManager::InferenceManager(Env& env, SolverState& s, TermRegistry& tr, ExtTheory& e, - SequencesStatistics& statistics, - ProofNodeManager* pnm) - : InferenceManagerBuffered(env, t, s, pnm, "theory::strings::", false), + SequencesStatistics& statistics) + : InferenceManagerBuffered(env, t, s, "theory::strings::", false), d_state(s), d_termReg(tr), d_extt(e), d_statistics(statistics), - d_ipc(pnm ? new InferProofCons(context(), pnm, d_statistics) : nullptr), - d_ipcl(pnm ? new InferProofCons(context(), pnm, d_statistics) : nullptr) + d_ipc(isProofEnabled() + ? new InferProofCons( + context(), env.getProofNodeManager(), d_statistics) + : nullptr), + d_ipcl(isProofEnabled() + ? new InferProofCons( + context(), env.getProofNodeManager(), d_statistics) + : nullptr) { NodeManager* nm = NodeManager::currentNM(); d_zero = nm->mkConst(Rational(0)); diff --git a/src/theory/strings/inference_manager.h b/src/theory/strings/inference_manager.h index 9f4cd1986..3ef83189b 100644 --- a/src/theory/strings/inference_manager.h +++ b/src/theory/strings/inference_manager.h @@ -82,8 +82,7 @@ class InferenceManager : public InferenceManagerBuffered SolverState& s, TermRegistry& tr, ExtTheory& e, - SequencesStatistics& statistics, - ProofNodeManager* pnm); + SequencesStatistics& statistics); ~InferenceManager() {} /** diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 88698d9d8..25d0e7336 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -58,7 +58,7 @@ TheoryStrings::TheoryStrings(Env& env, OutputChannel& out, Valuation valuation) d_eagerSolver(d_state), d_termReg(env, d_state, d_statistics, d_pnm), d_extTheoryCb(), - d_im(env, *this, d_state, d_termReg, d_extTheory, d_statistics, d_pnm), + d_im(env, *this, d_state, d_termReg, d_extTheory, d_statistics), d_extTheory(env, d_extTheoryCb, d_im), d_rewriter(env.getRewriter(), &d_statistics.d_rewrites, diff --git a/src/theory/theory_inference_manager.cpp b/src/theory/theory_inference_manager.cpp index 22b5e9c44..fdd1d07c8 100644 --- a/src/theory/theory_inference_manager.cpp +++ b/src/theory/theory_inference_manager.cpp @@ -31,7 +31,6 @@ namespace theory { TheoryInferenceManager::TheoryInferenceManager(Env& env, Theory& t, TheoryState& state, - ProofNodeManager* pnm, const std::string& statsName, bool cacheLemmas) : EnvObj(env), @@ -41,7 +40,6 @@ TheoryInferenceManager::TheoryInferenceManager(Env& env, d_ee(nullptr), d_decManager(nullptr), d_pfee(nullptr), - d_pnm(pnm), d_cacheLemmas(cacheLemmas), d_keep(context()), d_lemmasSent(userContext()), @@ -71,7 +69,7 @@ void TheoryInferenceManager::setEqualityEngine(eq::EqualityEngine* ee) // if it is non-null. If its proof equality engine has already been assigned, // use it. This is to ensure that all theories use the same proof equality // engine when in ee-mode=central. - if (d_pnm != nullptr && d_ee != nullptr) + if (isProofEnabled() && d_ee != nullptr) { d_pfee = d_ee->getProofEqualityEngine(); if (d_pfee == nullptr) @@ -88,7 +86,10 @@ void TheoryInferenceManager::setDecisionManager(DecisionManager* dm) d_decManager = dm; } -bool TheoryInferenceManager::isProofEnabled() const { return d_pnm != nullptr; } +bool TheoryInferenceManager::isProofEnabled() const +{ + return d_env.isTheoryProofProducing(); +} void TheoryInferenceManager::reset() { diff --git a/src/theory/theory_inference_manager.h b/src/theory/theory_inference_manager.h index 221d25fae..d7334d0e6 100644 --- a/src/theory/theory_inference_manager.h +++ b/src/theory/theory_inference_manager.h @@ -89,7 +89,6 @@ class TheoryInferenceManager : protected EnvObj TheoryInferenceManager(Env& env, Theory& t, TheoryState& state, - ProofNodeManager* pnm, const std::string& statsName, bool cacheLemmas = true); virtual ~TheoryInferenceManager(); @@ -441,8 +440,6 @@ class TheoryInferenceManager : protected EnvObj eq::ProofEqEngine* d_pfee; /** The proof equality engine we allocated */ std::unique_ptr d_pfeeAlloc; - /** The proof node manager of the theory */ - ProofNodeManager* d_pnm; /** Whether this manager caches lemmas */ bool d_cacheLemmas; /** diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp index a76591b6e..498fe765e 100644 --- a/src/theory/uf/theory_uf.cpp +++ b/src/theory/uf/theory_uf.cpp @@ -51,7 +51,7 @@ TheoryUF::TheoryUF(Env& env, d_symb(userContext(), instanceName), d_rewriter(logicInfo().isHigherOrder()), d_state(env, valuation), - d_im(env, *this, d_state, d_pnm, "theory::uf::" + instanceName, false), + d_im(env, *this, d_state, "theory::uf::" + instanceName, false), d_notify(d_im, *this) { d_true = NodeManager::currentNM()->mkConst( true );