From 854ab7e1adce90ebd822cc29ffabf5546d13f5cc Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 23 Feb 2021 19:12:32 -0600 Subject: [PATCH] Add interface to TheoryState for sort inference and facts (#5967) This eliminates the need for direct references to TheoryEngine from quantifiers and UF+cardinality. This PR also eliminates an unnecessary reference to TheoryEngine in TheoryModelBuilder and breaks a few more dependencies in quantifiers modules. --- src/preprocessing/passes/sort_infer.cpp | 3 +- src/theory/model_manager.cpp | 2 +- .../quantifiers/cegqi/ceg_instantiator.cpp | 52 +++++++++++++------ .../quantifiers/cegqi/ceg_instantiator.h | 5 +- .../quantifiers/cegqi/inst_strategy_cegqi.cpp | 2 +- .../quantifiers/fmf/bounded_integers.cpp | 9 ++-- src/theory/quantifiers/fmf/bounded_integers.h | 6 ++- src/theory/quantifiers/fmf/model_builder.cpp | 2 +- .../quantifiers/quantifiers_modules.cpp | 3 +- src/theory/quantifiers/quantifiers_modules.h | 2 + src/theory/quantifiers/quantifiers_state.cpp | 7 ++- src/theory/quantifiers/quantifiers_state.h | 9 +++- src/theory/quantifiers/skolemize.cpp | 15 +++--- src/theory/quantifiers/skolemize.h | 8 +-- src/theory/quantifiers/term_database.cpp | 15 ++---- src/theory/quantifiers/term_database.h | 5 +- src/theory/quantifiers/theory_quantifiers.cpp | 2 +- src/theory/quantifiers_engine.cpp | 11 ++-- src/theory/quantifiers_engine.h | 4 +- src/theory/sort_inference.cpp | 4 +- src/theory/sort_inference.h | 2 + src/theory/theory_engine.cpp | 5 ++ src/theory/theory_engine.h | 9 ++-- src/theory/theory_model_builder.cpp | 6 +-- src/theory/theory_model_builder.h | 4 +- src/theory/theory_state.cpp | 14 +++++ src/theory/theory_state.h | 16 ++++++ src/theory/uf/cardinality_extension.cpp | 34 +++++------- src/theory/uf/cardinality_extension.h | 5 -- src/theory/valuation.cpp | 22 ++++++++ src/theory/valuation.h | 19 +++++++ 31 files changed, 195 insertions(+), 107 deletions(-) diff --git a/src/preprocessing/passes/sort_infer.cpp b/src/preprocessing/passes/sort_infer.cpp index 79f387aa6..918b13140 100644 --- a/src/preprocessing/passes/sort_infer.cpp +++ b/src/preprocessing/passes/sort_infer.cpp @@ -34,7 +34,8 @@ SortInferencePass::SortInferencePass(PreprocessingPassContext* preprocContext) PreprocessingPassResult SortInferencePass::applyInternal( AssertionPipeline* assertionsToPreprocess) { - SortInference* si = d_preprocContext->getTheoryEngine()->getSortInference(); + theory::SortInference* si = + d_preprocContext->getTheoryEngine()->getSortInference(); if (options::sortInference()) { diff --git a/src/theory/model_manager.cpp b/src/theory/model_manager.cpp index 295b7309e..bb2bf937a 100644 --- a/src/theory/model_manager.cpp +++ b/src/theory/model_manager.cpp @@ -62,7 +62,7 @@ void ModelManager::finishInit(eq::EqualityEngineNotify* notify) // not have a model builder if (d_modelBuilder == nullptr) { - d_alocModelBuilder.reset(new TheoryEngineModelBuilder(&d_te)); + d_alocModelBuilder.reset(new TheoryEngineModelBuilder); d_modelBuilder = d_alocModelBuilder.get(); } // notice that the equality engine of the model has yet to be assigned. diff --git a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp index 8b60152a8..0d1a51a30 100644 --- a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp +++ b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp @@ -181,8 +181,11 @@ void SolvedForm::pop_back(Node pv, Node n, TermProperties& pv_prop) d_theta.pop_back(); } -CegInstantiator::CegInstantiator(Node q, InstStrategyCegqi* parent) +CegInstantiator::CegInstantiator(Node q, + QuantifiersState& qs, + InstStrategyCegqi* parent) : d_quant(q), + d_qstate(qs), d_parent(parent), d_qe(parent->getQuantifiersEngine()), d_is_nested_quant(false), @@ -1337,22 +1340,37 @@ void CegInstantiator::processAssertions() { } } //collect assertions for relevant theories - for( unsigned i=0; igetTheoryEngine()->theoryOf( tid ); - if( theory && d_qe->getTheoryEngine()->isTheoryEnabled(tid) ){ - Trace("cegqi-proc") << "Collect assertions from theory " << tid << std::endl; - d_curr_asserts[tid].clear(); - //collect all assertions from theory - for( context::CDList::const_iterator it = theory->facts_begin(); it != theory->facts_end(); ++ it) { - Node lit = (*it).d_assertion; - Node atom = lit.getKind()==NOT ? lit[0] : lit; - if( d_is_nested_quant || std::find( d_ce_atoms.begin(), d_ce_atoms.end(), atom )!=d_ce_atoms.end() ){ - d_curr_asserts[tid].push_back( lit ); - Trace("cegqi-proc-debug") << "...add : " << lit << std::endl; - }else{ - Trace("cegqi-proc") << "...do not consider literal " << tid << " : " << lit << " since it is not part of CE body." << std::endl; - } + const LogicInfo& logicInfo = d_qstate.getLogicInfo(); + for (TheoryId tid : d_tids) + { + if (!logicInfo.isTheoryEnabled(tid)) + { + continue; + } + Trace("cegqi-proc") << "Collect assertions from theory " << tid + << std::endl; + d_curr_asserts[tid].clear(); + // collect all assertions from theory + for (context::CDList::const_iterator + it = d_qstate.factsBegin(tid), + itEnd = d_qstate.factsEnd(tid); + it != itEnd; + ++it) + { + Node lit = (*it).d_assertion; + Node atom = lit.getKind() == NOT ? lit[0] : lit; + if (d_is_nested_quant + || std::find(d_ce_atoms.begin(), d_ce_atoms.end(), atom) + != d_ce_atoms.end()) + { + d_curr_asserts[tid].push_back(lit); + Trace("cegqi-proc-debug") << "...add : " << lit << std::endl; + } + else + { + Trace("cegqi-proc") + << "...do not consider literal " << tid << " : " << lit + << " since it is not part of CE body." << std::endl; } } } diff --git a/src/theory/quantifiers/cegqi/ceg_instantiator.h b/src/theory/quantifiers/cegqi/ceg_instantiator.h index b8a337cdb..85e14d579 100644 --- a/src/theory/quantifiers/cegqi/ceg_instantiator.h +++ b/src/theory/quantifiers/cegqi/ceg_instantiator.h @@ -33,6 +33,7 @@ namespace quantifiers { class Instantiator; class InstantiatorPreprocess; class InstStrategyCegqi; +class QuantifiersState; /** * Descriptions of the types of constraints that a term was solved for in. @@ -209,7 +210,7 @@ class CegInstantiator { * The instantiator will be constructing instantiations for quantified formula * q, parent is the owner of this object. */ - CegInstantiator(Node q, InstStrategyCegqi* parent); + CegInstantiator(Node q, QuantifiersState& qs, InstStrategyCegqi* parent); virtual ~CegInstantiator(); /** check * This adds instantiations based on the state of d_vars in current context @@ -353,6 +354,8 @@ class CegInstantiator { private: /** The quantified formula of this instantiator */ Node d_quant; + /** Reference to the quantifiers state */ + QuantifiersState& d_qstate; /** The parent of this instantiator */ InstStrategyCegqi* d_parent; /** quantified formula associated with this instantiator */ diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp index a79fbb9b6..dff10ddf1 100644 --- a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp +++ b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp @@ -503,7 +503,7 @@ CegInstantiator * InstStrategyCegqi::getInstantiator( Node q ) { std::map>::iterator it = d_cinst.find(q); if( it==d_cinst.end() ){ - d_cinst[q].reset(new CegInstantiator(q, this)); + d_cinst[q].reset(new CegInstantiator(q, d_qstate, this)); return d_cinst[q].get(); } return it->second.get(); diff --git a/src/theory/quantifiers/fmf/bounded_integers.cpp b/src/theory/quantifiers/fmf/bounded_integers.cpp index b9a3e1f34..700ae2c64 100644 --- a/src/theory/quantifiers/fmf/bounded_integers.cpp +++ b/src/theory/quantifiers/fmf/bounded_integers.cpp @@ -87,8 +87,9 @@ Node BoundedIntegers::IntRangeDecisionHeuristic::proxyCurrentRangeLemma() BoundedIntegers::BoundedIntegers(QuantifiersEngine* qe, QuantifiersState& qs, QuantifiersInferenceManager& qim, - QuantifiersRegistry& qr) - : QuantifiersModule(qs, qim, qr, qe) + QuantifiersRegistry& qr, + DecisionManager* dm) + : QuantifiersModule(qs, qim, qr, qe), d_dm(dm) { } @@ -500,9 +501,7 @@ void BoundedIntegers::checkOwnership(Node f) d_qstate.getUserContext(), d_qstate.getValuation(), isProxy)); - d_quantEngine->getTheoryEngine() - ->getDecisionManager() - ->registerStrategy(DecisionManager::STRAT_QUANT_BOUND_INT_SIZE, + d_dm->registerStrategy(DecisionManager::STRAT_QUANT_BOUND_INT_SIZE, d_rms[r].get()); } } diff --git a/src/theory/quantifiers/fmf/bounded_integers.h b/src/theory/quantifiers/fmf/bounded_integers.h index dce515d0d..9d4a414e9 100644 --- a/src/theory/quantifiers/fmf/bounded_integers.h +++ b/src/theory/quantifiers/fmf/bounded_integers.h @@ -28,6 +28,7 @@ namespace CVC4 { namespace theory { class RepSetIterator; +class DecisionManager; /** * Attribute set to 1 for literals that comprise the bounds of a quantified @@ -164,7 +165,8 @@ private: BoundedIntegers(QuantifiersEngine* qe, QuantifiersState& qs, QuantifiersInferenceManager& qim, - QuantifiersRegistry& qr); + QuantifiersRegistry& qr, + DecisionManager* dm); virtual ~BoundedIntegers(); void presolve() override; @@ -231,6 +233,8 @@ private: Node matchBoundVar( Node v, Node t, Node e ); bool getRsiSubsitution( Node q, Node v, std::vector< Node >& vars, std::vector< Node >& subs, RepSetIterator * rsi ); + /** Pointer to the decision manager */ + DecisionManager* d_dm; }; } diff --git a/src/theory/quantifiers/fmf/model_builder.cpp b/src/theory/quantifiers/fmf/model_builder.cpp index cdb65f2b2..13bdcf963 100644 --- a/src/theory/quantifiers/fmf/model_builder.cpp +++ b/src/theory/quantifiers/fmf/model_builder.cpp @@ -30,7 +30,7 @@ using namespace CVC4::theory; using namespace CVC4::theory::quantifiers; QModelBuilder::QModelBuilder(QuantifiersEngine* qe, QuantifiersState& qs) - : TheoryEngineModelBuilder(qe->getTheoryEngine()), + : TheoryEngineModelBuilder(), d_qe(qe), d_addedLemmas(0), d_triedLemmas(0), diff --git a/src/theory/quantifiers/quantifiers_modules.cpp b/src/theory/quantifiers/quantifiers_modules.cpp index 74f553800..8142165aa 100644 --- a/src/theory/quantifiers/quantifiers_modules.cpp +++ b/src/theory/quantifiers/quantifiers_modules.cpp @@ -41,6 +41,7 @@ void QuantifiersModules::initialize(QuantifiersEngine* qe, QuantifiersState& qs, QuantifiersInferenceManager& qim, QuantifiersRegistry& qr, + DecisionManager* dm, std::vector& modules) { // add quantifiers modules @@ -73,7 +74,7 @@ void QuantifiersModules::initialize(QuantifiersEngine* qe, // finite model finding if (options::fmfBound()) { - d_bint.reset(new BoundedIntegers(qe, qs, qim, qr)); + d_bint.reset(new BoundedIntegers(qe, qs, qim, qr, dm)); modules.push_back(d_bint.get()); } if (options::finiteModelFind() || options::fmfBound()) diff --git a/src/theory/quantifiers/quantifiers_modules.h b/src/theory/quantifiers/quantifiers_modules.h index 08266c8fe..c9960a1bc 100644 --- a/src/theory/quantifiers/quantifiers_modules.h +++ b/src/theory/quantifiers/quantifiers_modules.h @@ -32,6 +32,7 @@ namespace CVC4 { namespace theory { class QuantifiersEngine; +class DecisionManager; namespace quantifiers { @@ -55,6 +56,7 @@ class QuantifiersModules QuantifiersState& qs, QuantifiersInferenceManager& qim, QuantifiersRegistry& qr, + DecisionManager* dm, std::vector& modules); private: diff --git a/src/theory/quantifiers/quantifiers_state.cpp b/src/theory/quantifiers/quantifiers_state.cpp index 07bd97918..0bcca266e 100644 --- a/src/theory/quantifiers/quantifiers_state.cpp +++ b/src/theory/quantifiers/quantifiers_state.cpp @@ -22,8 +22,9 @@ namespace quantifiers { QuantifiersState::QuantifiersState(context::Context* c, context::UserContext* u, - Valuation val) - : TheoryState(c, u, val), d_ierCounterc(c) + Valuation val, + const LogicInfo& logicInfo) + : TheoryState(c, u, val), d_ierCounterc(c), d_logicInfo(logicInfo) { // allow theory combination to go first, once initially d_ierCounter = options::instWhenTcFirst() ? 0 : 1; @@ -152,6 +153,8 @@ void QuantifiersState::debugPrintEqualityEngine(const char* c) const } } +const LogicInfo& QuantifiersState::getLogicInfo() const { return d_logicInfo; } + } // namespace quantifiers } // namespace theory } // namespace CVC4 diff --git a/src/theory/quantifiers/quantifiers_state.h b/src/theory/quantifiers/quantifiers_state.h index d45938f98..edebec156 100644 --- a/src/theory/quantifiers/quantifiers_state.h +++ b/src/theory/quantifiers/quantifiers_state.h @@ -30,7 +30,10 @@ namespace quantifiers { class QuantifiersState : public TheoryState { public: - QuantifiersState(context::Context* c, context::UserContext* u, Valuation val); + QuantifiersState(context::Context* c, + context::UserContext* u, + Valuation val, + const LogicInfo& logicInfo); ~QuantifiersState() {} /** * Increment the instantiation counters, called once at the beginning of when @@ -51,6 +54,8 @@ class QuantifiersState : public TheoryState uint64_t getInstRounds() const; /** debug print equality engine on trace c */ void debugPrintEqualityEngine(const char* c) const; + /** get the logic info */ + const LogicInfo& getLogicInfo() const; private: /** The number of instantiation rounds in this SAT context */ @@ -70,6 +75,8 @@ class QuantifiersState : public TheoryState * combination. */ uint64_t d_instWhenPhase; + /** Information about the logic we're operating within. */ + const LogicInfo& d_logicInfo; }; } // namespace quantifiers diff --git a/src/theory/quantifiers/skolemize.cpp b/src/theory/quantifiers/skolemize.cpp index 4f9a0ee91..2e9093b82 100644 --- a/src/theory/quantifiers/skolemize.cpp +++ b/src/theory/quantifiers/skolemize.cpp @@ -14,12 +14,13 @@ #include "theory/quantifiers/skolemize.h" +#include "expr/dtype.h" #include "expr/skolem_manager.h" #include "options/quantifiers_options.h" #include "options/smt_options.h" #include "theory/quantifiers/quantifiers_attributes.h" +#include "theory/quantifiers/quantifiers_state.h" #include "theory/quantifiers/term_util.h" -#include "theory/quantifiers_engine.h" #include "theory/sort_inference.h" #include "theory/theory_engine.h" @@ -29,10 +30,8 @@ namespace CVC4 { namespace theory { namespace quantifiers { -Skolemize::Skolemize(QuantifiersEngine* qe, - QuantifiersState& qs, - ProofNodeManager* pnm) - : d_quantEngine(qe), +Skolemize::Skolemize(QuantifiersState& qs, ProofNodeManager* pnm) + : d_qstate(qs), d_skolemized(qs.getUserContext()), d_pnm(pnm), d_epg(pnm == nullptr ? nullptr @@ -350,13 +349,13 @@ Node Skolemize::getSkolemizedBody(Node f) } } Assert(d_skolem_constants[f].size() == f[0].getNumChildren()); - if (options::sortInference()) + SortInference* si = d_qstate.getSortInference(); + if (si != nullptr) { for (unsigned i = 0; i < d_skolem_constants[f].size(); i++) { // carry information for sort inference - d_quantEngine->getTheoryEngine()->getSortInference()->setSkolemVar( - f, f[0][i], d_skolem_constants[f][i]); + si->setSkolemVar(f, f[0][i], d_skolem_constants[f][i]); } } return ret; diff --git a/src/theory/quantifiers/skolemize.h b/src/theory/quantifiers/skolemize.h index c959758a0..4f92b2eda 100644 --- a/src/theory/quantifiers/skolemize.h +++ b/src/theory/quantifiers/skolemize.h @@ -32,7 +32,7 @@ class DTypeConstructor; namespace theory { -class QuantifiersEngine; +class SortInference; namespace quantifiers { @@ -69,7 +69,7 @@ class Skolemize typedef context::CDHashMap NodeNodeMap; public: - Skolemize(QuantifiersEngine* qe, QuantifiersState& qs, ProofNodeManager* pnm); + Skolemize(QuantifiersState& qs, ProofNodeManager* pnm); ~Skolemize() {} /** skolemize quantified formula q * If the return value ret of this function is non-null, then ret is a trust @@ -140,8 +140,8 @@ class Skolemize Node n, TypeNode ntn, std::vector& selfSel); - /** quantifiers engine that owns this module */ - QuantifiersEngine* d_quantEngine; + /** Reference to the quantifiers state */ + QuantifiersState& d_qstate; /** quantified formulas that have been skolemized */ NodeNodeMap d_skolemized; /** map from quantified formulas to the list of skolem constants */ diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index f111b23ce..cb5c7dfec 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -36,10 +36,8 @@ namespace quantifiers { TermDb::TermDb(QuantifiersState& qs, QuantifiersInferenceManager& qim, - QuantifiersRegistry& qr, - QuantifiersEngine* qe) - : d_quantEngine(qe), - d_qstate(qs), + QuantifiersRegistry& qr) + : d_qstate(qs), d_qim(qim), d_qreg(qr), d_termsContext(), @@ -1083,19 +1081,16 @@ bool TermDb::reset( Theory::Effort effort ){ } ++eqcs_i; } - TheoryEngine* te = d_quantEngine->getTheoryEngine(); - const LogicInfo& logicInfo = te->getLogicInfo(); + const LogicInfo& logicInfo = d_qstate.getLogicInfo(); for (TheoryId theoryId = THEORY_FIRST; theoryId < THEORY_LAST; ++theoryId) { if (!logicInfo.isTheoryEnabled(theoryId)) { continue; } - Theory* theory = te->theoryOf(theoryId); - Assert(theory != nullptr); for (context::CDList::const_iterator - it = theory->facts_begin(), - it_end = theory->facts_end(); + it = d_qstate.factsBegin(theoryId), + it_end = d_qstate.factsEnd(theoryId); it != it_end; ++it) { diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h index 89d77e169..9a031f99c 100644 --- a/src/theory/quantifiers/term_database.h +++ b/src/theory/quantifiers/term_database.h @@ -77,8 +77,7 @@ class TermDb : public QuantifiersUtil { public: TermDb(QuantifiersState& qs, QuantifiersInferenceManager& qim, - QuantifiersRegistry& qr, - QuantifiersEngine* qe); + QuantifiersRegistry& qr); ~TermDb(); /** presolve (called once per user check-sat) */ void presolve(); @@ -291,8 +290,6 @@ class TermDb : public QuantifiersUtil { Node getHoTypeMatchPredicate(TypeNode tn); private: - /** reference to the quantifiers engine */ - QuantifiersEngine* d_quantEngine; /** The quantifiers state object */ QuantifiersState& d_qstate; /** The quantifiers inference manager */ diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp index 7c2bbb019..0f1f5f7de 100644 --- a/src/theory/quantifiers/theory_quantifiers.cpp +++ b/src/theory/quantifiers/theory_quantifiers.cpp @@ -43,7 +43,7 @@ TheoryQuantifiers::TheoryQuantifiers(Context* c, const LogicInfo& logicInfo, ProofNodeManager* pnm) : Theory(THEORY_QUANTIFIERS, c, u, out, valuation, logicInfo, pnm), - d_qstate(c, u, valuation), + d_qstate(c, u, valuation, logicInfo), d_qim(*this, d_qstate, pnm), d_qengine(d_qstate, d_qim, pnm) { diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index ec4cb7905..7046a8ef0 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -41,16 +41,17 @@ QuantifiersEngine::QuantifiersEngine( d_qim(qim), d_te(nullptr), d_decManager(nullptr), + d_pnm(pnm), d_qreg(), d_tr_trie(new inst::TriggerTrie), d_model(nullptr), d_builder(nullptr), - d_term_db(new quantifiers::TermDb(qstate, qim, d_qreg, this)), + d_term_db(new quantifiers::TermDb(qstate, qim, d_qreg)), d_eq_query(nullptr), d_sygus_tdb(nullptr), d_instantiate( new quantifiers::Instantiate(this, qstate, qim, d_qreg, pnm)), - d_skolemize(new quantifiers::Skolemize(this, qstate, pnm)), + d_skolemize(new quantifiers::Skolemize(d_qstate, d_pnm)), d_term_enum(new quantifiers::TermEnumeration), d_quants_prereg(qstate.getUserContext()), d_quants_red(qstate.getUserContext()), @@ -113,15 +114,13 @@ void QuantifiersEngine::finishInit(TheoryEngine* te, DecisionManager* dm) d_decManager = dm; // Initialize the modules and the utilities here. d_qmodules.reset(new quantifiers::QuantifiersModules); - d_qmodules->initialize(this, d_qstate, d_qim, d_qreg, d_modules); + d_qmodules->initialize(this, d_qstate, d_qim, d_qreg, dm, d_modules); if (d_qmodules->d_rel_dom.get()) { d_util.push_back(d_qmodules->d_rel_dom.get()); } } -TheoryEngine* QuantifiersEngine::getTheoryEngine() const { return d_te; } - DecisionManager* QuantifiersEngine::getDecisionManager() { return d_decManager; @@ -387,7 +386,7 @@ void QuantifiersEngine::check( Theory::Effort e ){ } if( Trace.isOn("quant-engine-assert") ){ Trace("quant-engine-assert") << "Assertions : " << std::endl; - getTheoryEngine()->printAssertions("quant-engine-assert"); + d_te->printAssertions("quant-engine-assert"); } //reset utilities diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index c8f9cd6ad..f464b24d4 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -65,8 +65,6 @@ class QuantifiersEngine { ProofNodeManager* pnm); ~QuantifiersEngine(); //---------------------- external interface - /** get theory engine */ - TheoryEngine* getTheoryEngine() const; /** Get the decision manager */ DecisionManager* getDecisionManager(); /** The quantifiers state object */ @@ -272,6 +270,8 @@ public: TheoryEngine* d_te; /** Reference to the decision manager of the theory engine */ DecisionManager* d_decManager; + /** Pointer to the proof node manager */ + ProofNodeManager* d_pnm; /** vector of utilities for quantifiers */ std::vector d_util; /** vector of modules for quantifiers */ diff --git a/src/theory/sort_inference.cpp b/src/theory/sort_inference.cpp index 9fa216e67..63e3359ab 100644 --- a/src/theory/sort_inference.cpp +++ b/src/theory/sort_inference.cpp @@ -32,6 +32,7 @@ using namespace CVC4::kind; using namespace std; namespace CVC4 { +namespace theory { void SortInference::UnionFind::print(const char * c){ for( std::map< int, int >::iterator it = d_eqc.begin(); it != d_eqc.end(); ++it ){ @@ -864,4 +865,5 @@ bool SortInference::isHandledApplyUf(Kind k) const return k == APPLY_UF && !options::ufHo(); } -}/* CVC4 namespace */ +} // namespace theory +} // namespace CVC4 diff --git a/src/theory/sort_inference.h b/src/theory/sort_inference.h index 059dc5582..46497c494 100644 --- a/src/theory/sort_inference.h +++ b/src/theory/sort_inference.h @@ -25,6 +25,7 @@ #include "expr/type_node.h" namespace CVC4 { +namespace theory { /** sort inference * @@ -165,6 +166,7 @@ private: bool isHandledApplyUf(Kind k) const; }; +} // namespace theory } #endif diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index a2e608b9f..e49ca8b05 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -250,6 +250,11 @@ TheoryEngine::TheoryEngine(context::Context* context, d_theoryOut[theoryId] = NULL; } + if (options::sortInference()) + { + d_sortInfer.reset(new SortInference); + } + smtStatisticsRegistry()->registerStat(&d_combineTheoriesTime); d_true = NodeManager::currentNM()->mkConst(true); d_false = NodeManager::currentNM()->mkConst(false); diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 224d84664..d10e498a8 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -274,7 +274,7 @@ class TheoryEngine { void ensureLemmaAtoms(const std::vector& atoms, theory::TheoryId theory); /** sort inference module */ - SortInference d_sortInfer; + std::unique_ptr d_sortInfer; /** Time spent in theory combination */ TimerStat d_combineTheoriesTime; @@ -634,11 +634,10 @@ class TheoryEngine { /** For preprocessing pass lifting bit-vectors of size 1 to booleans */ public: + theory::SortInference* getSortInference() { return d_sortInfer.get(); } - SortInference* getSortInference() { return &d_sortInfer; } - - /** Prints the assertions to the debug stream */ - void printAssertions(const char* tag); + /** Prints the assertions to the debug stream */ + void printAssertions(const char* tag); private: diff --git a/src/theory/theory_model_builder.cpp b/src/theory/theory_model_builder.cpp index 53b8f25a4..9604dc72b 100644 --- a/src/theory/theory_model_builder.cpp +++ b/src/theory/theory_model_builder.cpp @@ -16,8 +16,8 @@ #include "expr/dtype.h" #include "options/quantifiers_options.h" #include "options/smt_options.h" +#include "options/theory_options.h" #include "options/uf_options.h" -#include "theory/theory_engine.h" #include "theory/uf/theory_uf_model.h" using namespace std; @@ -60,9 +60,7 @@ Node TheoryEngineModelBuilder::Assigner::getNextAssignment() return n; } -TheoryEngineModelBuilder::TheoryEngineModelBuilder(TheoryEngine* te) : d_te(te) -{ -} +TheoryEngineModelBuilder::TheoryEngineModelBuilder() {} Node TheoryEngineModelBuilder::evaluateEqc(TheoryModel* m, TNode r) { diff --git a/src/theory/theory_model_builder.h b/src/theory/theory_model_builder.h index 4ffcbeee7..fde74a05f 100644 --- a/src/theory/theory_model_builder.h +++ b/src/theory/theory_model_builder.h @@ -47,7 +47,7 @@ class TheoryEngineModelBuilder typedef std::unordered_set NodeSet; public: - TheoryEngineModelBuilder(TheoryEngine* te); + TheoryEngineModelBuilder(); virtual ~TheoryEngineModelBuilder() {} /** * Should be called only on models m after they have been prepared @@ -84,8 +84,6 @@ class TheoryEngineModelBuilder void postProcessModel(bool incomplete, TheoryModel* m); protected: - /** pointer to theory engine */ - TheoryEngine* d_te; //-----------------------------------virtual functions /** pre-process build model diff --git a/src/theory/theory_state.cpp b/src/theory/theory_state.cpp index e145baa6a..2d6c713de 100644 --- a/src/theory/theory_state.cpp +++ b/src/theory/theory_state.cpp @@ -152,11 +152,25 @@ bool TheoryState::isSatLiteral(TNode lit) const TheoryModel* TheoryState::getModel() { return d_valuation.getModel(); } +SortInference* TheoryState::getSortInference() +{ + return d_valuation.getSortInference(); +} + bool TheoryState::hasSatValue(TNode n, bool& value) const { return d_valuation.hasSatValue(n, value); } +context::CDList::const_iterator TheoryState::factsBegin(TheoryId tid) +{ + return d_valuation.factsBegin(tid); +} +context::CDList::const_iterator TheoryState::factsEnd(TheoryId tid) +{ + return d_valuation.factsEnd(tid); +} + Valuation& TheoryState::getValuation() { return d_valuation; } } // namespace theory diff --git a/src/theory/theory_state.h b/src/theory/theory_state.h index 891016f0a..60b45878f 100644 --- a/src/theory/theory_state.h +++ b/src/theory/theory_state.h @@ -81,10 +81,26 @@ class TheoryState * check. */ TheoryModel* getModel(); + /** + * Returns a pointer to the sort inference module, which lives in TheoryEngine + * and is non-null when options::sortInference is true. + */ + SortInference* getSortInference(); /** Returns true if n has a current SAT assignment and stores it in value. */ virtual bool hasSatValue(TNode n, bool& value) const; + //------------------------------------------- access methods for assertions + /** + * The following methods are intended only to be used in limited use cases, + * for cases where a theory (e.g. quantifiers) requires knowing about the + * assertions from other theories. + */ + /** The beginning iterator of facts for theory tid.*/ + context::CDList::const_iterator factsBegin(TheoryId tid); + /** The beginning iterator of facts for theory tid.*/ + context::CDList::const_iterator factsEnd(TheoryId tid); + /** Get the underlying valuation class */ Valuation& getValuation(); diff --git a/src/theory/uf/cardinality_extension.cpp b/src/theory/uf/cardinality_extension.cpp index aa73e3419..94402e2d9 100644 --- a/src/theory/uf/cardinality_extension.cpp +++ b/src/theory/uf/cardinality_extension.cpp @@ -740,7 +740,7 @@ void SortModel::check(Theory::Effort level) Trace("uf-ss-debug") << "No splits added. " << d_cardinality << std::endl; Trace("uf-ss-si") << "Must combine region" << std::endl; bool recheck = false; - SortInference* si = d_thss->getSortInference(); + SortInference* si = d_state.getSortInference(); if (si != nullptr) { // If sort inference is enabled, search for regions with same sort. @@ -1021,14 +1021,18 @@ int SortModel::addSplit(Region* r) AlwaysAssert(false); } } - SortInference* si = d_thss->getSortInference(); - if (si != nullptr) + if (Trace.isOn("uf-ss-split-si")) { - for( int i=0; i<2; i++ ){ - int sid = si->getSortId(ss[i]); - Trace("uf-ss-split-si") << sid << " "; + SortInference* si = d_state.getSortInference(); + if (si != nullptr) + { + for (size_t i = 0; i < 2; i++) + { + int sid = si->getSortId(ss[i]); + Trace("uf-ss-split-si") << sid << " "; + } + Trace("uf-ss-split-si") << std::endl; } - Trace("uf-ss-split-si") << std::endl; } //Trace("uf-ss-lemma") << d_th->getEqualityEngine()->areEqual( s[0], s[1] ) << " "; //Trace("uf-ss-lemma") << d_th->getEqualityEngine()->areDisequal( s[0], s[1] ) << std::endl; @@ -1247,20 +1251,6 @@ CardinalityExtension::~CardinalityExtension() } } -SortInference* CardinalityExtension::getSortInference() -{ - if (!options::sortInference()) - { - return nullptr; - } - QuantifiersEngine* qe = d_th->getQuantifiersEngine(); - if (qe != nullptr) - { - return qe->getTheoryEngine()->getSortInference(); - } - return nullptr; -} - /** ensure eqc */ void CardinalityExtension::ensureEqc(SortModel* c, Node a) { @@ -1351,12 +1341,12 @@ void CardinalityExtension::assertNode(Node n, bool isDecision) Trace("uf-ss-debug") << "...check cardinality terms : " << lit[0] << " " << ct << std::endl; if( lit[0]==ct ){ if( options::ufssFairnessMonotone() ){ + SortInference* si = d_state.getSortInference(); Trace("uf-ss-com-card-debug") << "...set master/slave" << std::endl; if( tn!=d_tn_mono_master ){ std::map< TypeNode, bool >::iterator it = d_tn_mono_slave.find( tn ); if( it==d_tn_mono_slave.end() ){ bool isMonotonic; - SortInference* si = getSortInference(); if (si != nullptr) { isMonotonic = si->isMonotonic(tn); diff --git a/src/theory/uf/cardinality_extension.h b/src/theory/uf/cardinality_extension.h index 6b5349ce7..4f1566424 100644 --- a/src/theory/uf/cardinality_extension.h +++ b/src/theory/uf/cardinality_extension.h @@ -25,9 +25,6 @@ #include "theory/decision_manager.h" namespace CVC4 { - -class SortInference; - namespace theory { namespace uf { @@ -366,8 +363,6 @@ class CardinalityExtension ~CardinalityExtension(); /** get theory */ TheoryUF* getTheory() { return d_th; } - /** get sort inference module */ - SortInference* getSortInference(); /** new node */ void newEqClass( Node n ); /** merge */ diff --git a/src/theory/valuation.cpp b/src/theory/valuation.cpp index 1926c836e..0dd576a04 100644 --- a/src/theory/valuation.cpp +++ b/src/theory/valuation.cpp @@ -124,6 +124,15 @@ TheoryModel* Valuation::getModel() { } return d_engine->getModel(); } +SortInference* Valuation::getSortInference() +{ + if (d_engine == nullptr) + { + // no theory engine, thus we don't have a sort inference object + return nullptr; + } + return d_engine->getSortInference(); +} void Valuation::setUnevaluatedKind(Kind k) { @@ -198,5 +207,18 @@ bool Valuation::needCheck() const{ bool Valuation::isRelevant(Node lit) const { return d_engine->isRelevant(lit); } +context::CDList::const_iterator Valuation::factsBegin(TheoryId tid) +{ + Theory* theory = d_engine->theoryOf(tid); + Assert(theory != nullptr); + return theory->facts_begin(); +} +context::CDList::const_iterator Valuation::factsEnd(TheoryId tid) +{ + Theory* theory = d_engine->theoryOf(tid); + Assert(theory != nullptr); + return theory->facts_end(); +} + }/* CVC4::theory namespace */ }/* CVC4 namespace */ diff --git a/src/theory/valuation.h b/src/theory/valuation.h index 9759309fa..305795881 100644 --- a/src/theory/valuation.h +++ b/src/theory/valuation.h @@ -21,8 +21,10 @@ #ifndef CVC4__THEORY__VALUATION_H #define CVC4__THEORY__VALUATION_H +#include "context/cdlist.h" #include "expr/node.h" #include "options/theory_options.h" +#include "theory/assertion.h" namespace CVC4 { @@ -31,6 +33,7 @@ class TheoryEngine; namespace theory { class TheoryModel; +class SortInference; /** * The status of an equality in the current context. @@ -111,6 +114,11 @@ public: * check. */ TheoryModel* getModel(); + /** + * Returns a pointer to the sort inference module, which lives in TheoryEngine + * and is non-null when options::sortInference is true. + */ + SortInference* getSortInference(); //-------------------------------------- static configuration of the model /** @@ -195,6 +203,17 @@ public: * or during LAST_CALL effort. */ bool isRelevant(Node lit) const; + + //------------------------------------------- access methods for assertions + /** + * The following methods are intended only to be used in limited use cases, + * for cases where a theory (e.g. quantifiers) requires knowing about the + * assertions from other theories. + */ + /** The beginning iterator of facts for theory tid.*/ + context::CDList::const_iterator factsBegin(TheoryId tid); + /** The beginning iterator of facts for theory tid.*/ + context::CDList::const_iterator factsEnd(TheoryId tid); };/* class Valuation */ }/* CVC4::theory namespace */ -- 2.30.2