From 6d060743830ab21dc970444688fe1dc2ad34494f Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 15 Mar 2021 13:17:19 -0500 Subject: [PATCH] Reorganizing initialization of term registry in quantifiers (#6127) This is in preparation for moving several utilities into the quantifiers inference manager. This PR moves ownership of TermRegistry and QuantifiersRegistry to TheoryQuantifiers from QuantifiersEngine. --- src/theory/quantifiers/ematching/ho_trigger.cpp | 1 + .../ematching/inst_strategy_e_matching.cpp | 1 + src/theory/quantifiers/ematching/trigger.cpp | 1 + src/theory/quantifiers/relevant_domain.cpp | 2 ++ .../quantifiers/sygus/term_database_sygus.cpp | 9 +++++---- .../quantifiers/sygus/term_database_sygus.h | 8 +++++--- src/theory/quantifiers/term_database.cpp | 13 +++++++------ src/theory/quantifiers/term_database.h | 7 ++++--- src/theory/quantifiers/term_registry.cpp | 17 ++++++++++++----- src/theory/quantifiers/term_registry.h | 3 ++- .../quantifiers/term_tuple_enumerator.cpp | 1 + src/theory/quantifiers/theory_quantifiers.cpp | 11 ++++++++++- src/theory/quantifiers/theory_quantifiers.h | 6 ++++++ src/theory/quantifiers_engine.cpp | 14 ++++++++------ src/theory/quantifiers_engine.h | 10 ++++++---- 15 files changed, 71 insertions(+), 33 deletions(-) diff --git a/src/theory/quantifiers/ematching/ho_trigger.cpp b/src/theory/quantifiers/ematching/ho_trigger.cpp index 953693f59..17cbba7ea 100644 --- a/src/theory/quantifiers/ematching/ho_trigger.cpp +++ b/src/theory/quantifiers/ematching/ho_trigger.cpp @@ -17,6 +17,7 @@ #include "theory/quantifiers/ematching/ho_trigger.h" #include "theory/quantifiers/instantiate.h" #include "theory/quantifiers/quantifiers_inference_manager.h" +#include "theory/quantifiers/quantifiers_registry.h" #include "theory/quantifiers/quantifiers_state.h" #include "theory/quantifiers/term_database.h" #include "theory/quantifiers/term_util.h" diff --git a/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp b/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp index 257684704..4470e5bf4 100644 --- a/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp +++ b/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp @@ -17,6 +17,7 @@ #include "theory/quantifiers/ematching/pattern_term_selector.h" #include "theory/quantifiers/quant_relevance.h" #include "theory/quantifiers/quantifiers_inference_manager.h" +#include "theory/quantifiers/quantifiers_registry.h" #include "theory/quantifiers/quantifiers_state.h" #include "theory/quantifiers_engine.h" #include "util/random.h" diff --git a/src/theory/quantifiers/ematching/trigger.cpp b/src/theory/quantifiers/ematching/trigger.cpp index 62a63a2d5..3940370cf 100644 --- a/src/theory/quantifiers/ematching/trigger.cpp +++ b/src/theory/quantifiers/ematching/trigger.cpp @@ -28,6 +28,7 @@ #include "theory/quantifiers/instantiate.h" #include "theory/quantifiers/quantifiers_attributes.h" #include "theory/quantifiers/quantifiers_inference_manager.h" +#include "theory/quantifiers/quantifiers_registry.h" #include "theory/quantifiers/quantifiers_state.h" #include "theory/quantifiers/term_util.h" #include "theory/quantifiers_engine.h" diff --git a/src/theory/quantifiers/relevant_domain.cpp b/src/theory/quantifiers/relevant_domain.cpp index ac59a852e..456a7a8fc 100644 --- a/src/theory/quantifiers/relevant_domain.cpp +++ b/src/theory/quantifiers/relevant_domain.cpp @@ -13,8 +13,10 @@ **/ #include "theory/quantifiers/relevant_domain.h" + #include "theory/arith/arith_msum.h" #include "theory/quantifiers/first_order_model.h" +#include "theory/quantifiers/quantifiers_registry.h" #include "theory/quantifiers/quantifiers_state.h" #include "theory/quantifiers/term_database.h" #include "theory/quantifiers/term_util.h" diff --git a/src/theory/quantifiers/sygus/term_database_sygus.cpp b/src/theory/quantifiers/sygus/term_database_sygus.cpp index fa90d699a..50c522d95 100644 --- a/src/theory/quantifiers/sygus/term_database_sygus.cpp +++ b/src/theory/quantifiers/sygus/term_database_sygus.cpp @@ -47,9 +47,8 @@ std::ostream& operator<<(std::ostream& os, EnumeratorRole r) return os; } -TermDbSygus::TermDbSygus(QuantifiersState& qs, QuantifiersInferenceManager& qim) +TermDbSygus::TermDbSygus(QuantifiersState& qs) : d_qstate(qs), - d_qim(qim), d_syexp(new SygusExplain(this)), d_ext_rw(new ExtendedRewriter(true)), d_eval(new Evaluator), @@ -60,6 +59,8 @@ TermDbSygus::TermDbSygus(QuantifiersState& qs, QuantifiersInferenceManager& qim) d_false = NodeManager::currentNM()->mkConst( false ); } +void TermDbSygus::finishInit(QuantifiersInferenceManager* qim) { d_qim = qim; } + bool TermDbSygus::reset( Theory::Effort e ) { return true; } @@ -565,8 +566,8 @@ void TermDbSygus::registerEnumerator(Node e, ag = d_qstate.getValuation().ensureLiteral(ag); // must ensure that it is asserted as a literal before we begin solving Node lem = nm->mkNode(OR, ag, ag.negate()); - d_qim.requirePhase(ag, true); - d_qim.lemma(lem, InferenceId::QUANTIFIERS_SYGUS_ENUM_ACTIVE_GUARD_SPLIT); + d_qim->requirePhase(ag, true); + d_qim->lemma(lem, InferenceId::QUANTIFIERS_SYGUS_ENUM_ACTIVE_GUARD_SPLIT); d_enum_to_active_guard[e] = ag; } } diff --git a/src/theory/quantifiers/sygus/term_database_sygus.h b/src/theory/quantifiers/sygus/term_database_sygus.h index b313846b9..f2188469e 100644 --- a/src/theory/quantifiers/sygus/term_database_sygus.h +++ b/src/theory/quantifiers/sygus/term_database_sygus.h @@ -54,8 +54,10 @@ std::ostream& operator<<(std::ostream& os, EnumeratorRole r); // TODO :issue #1235 split and document this class class TermDbSygus { public: - TermDbSygus(QuantifiersState& qs, QuantifiersInferenceManager& qim); + TermDbSygus(QuantifiersState& qs); ~TermDbSygus() {} + /** Finish init, which sets the inference manager */ + void finishInit(QuantifiersInferenceManager* qim); /** Reset this utility */ bool reset(Theory::Effort e); /** Identify this utility */ @@ -316,8 +318,8 @@ class TermDbSygus { private: /** Reference to the quantifiers state */ QuantifiersState& d_qstate; - /** The quantifiers inference manager */ - QuantifiersInferenceManager& d_qim; + /** Pointer to the quantifiers inference manager */ + QuantifiersInferenceManager* d_qim; //------------------------------utilities /** sygus explanation */ diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index 2d896c089..ca11d491d 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -22,6 +22,7 @@ #include "theory/quantifiers/ematching/trigger_term_info.h" #include "theory/quantifiers/quantifiers_attributes.h" #include "theory/quantifiers/quantifiers_inference_manager.h" +#include "theory/quantifiers/quantifiers_registry.h" #include "theory/quantifiers/quantifiers_state.h" #include "theory/quantifiers/term_util.h" #include "theory/quantifiers_engine.h" @@ -36,11 +37,9 @@ namespace CVC4 { namespace theory { namespace quantifiers { -TermDb::TermDb(QuantifiersState& qs, - QuantifiersInferenceManager& qim, - QuantifiersRegistry& qr) +TermDb::TermDb(QuantifiersState& qs, QuantifiersRegistry& qr) : d_qstate(qs), - d_qim(qim), + d_qim(nullptr), d_qreg(qr), d_termsContext(), d_termsContextUse(options::termDbCd() ? qs.getSatContext() @@ -66,6 +65,8 @@ TermDb::~TermDb(){ } +void TermDb::finishInit(QuantifiersInferenceManager* qim) { d_qim = qim; } + void TermDb::registerQuantifier( Node q ) { Assert(q[0].getNumChildren() == d_qreg.getNumInstantiationConstants(q)); for (size_t i = 0, nvars = q[0].getNumChildren(); i < nvars; i++) @@ -437,7 +438,7 @@ void TermDb::computeUfTerms( TNode f ) { } Trace("term-db-lemma") << " add lemma : " << lem << std::endl; } - d_qim.addPendingLemma(lem, InferenceId::UNKNOWN); + d_qim->addPendingLemma(lem, InferenceId::UNKNOWN); d_qstate.notifyInConflict(); d_consistent_ee = false; return; @@ -1047,7 +1048,7 @@ bool TermDb::reset( Theory::Effort effort ){ // equality is sent out as a lemma here. Trace("term-db-lemma") << "Purify equality lemma: " << eq << std::endl; - d_qim.addPendingLemma(eq, InferenceId::UNKNOWN); + d_qim->addPendingLemma(eq, InferenceId::UNKNOWN); d_qstate.notifyInConflict(); d_consistent_ee = false; return false; diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h index 61754ac32..6506a6123 100644 --- a/src/theory/quantifiers/term_database.h +++ b/src/theory/quantifiers/term_database.h @@ -78,9 +78,10 @@ class TermDb : public QuantifiersUtil { public: TermDb(QuantifiersState& qs, - QuantifiersInferenceManager& qim, QuantifiersRegistry& qr); ~TermDb(); + /** Finish init, which sets the inference manager */ + void finishInit(QuantifiersInferenceManager* qim); /** presolve (called once per user check-sat) */ void presolve(); /** reset (calculate which terms are active) */ @@ -294,8 +295,8 @@ class TermDb : public QuantifiersUtil { private: /** The quantifiers state object */ QuantifiersState& d_qstate; - /** The quantifiers inference manager */ - QuantifiersInferenceManager& d_qim; + /** Pointer to the quantifiers inference manager */ + QuantifiersInferenceManager* d_qim; /** The quantifiers registry */ QuantifiersRegistry& d_qreg; /** A context for the data structures below, when not context-dependent */ diff --git a/src/theory/quantifiers/term_registry.cpp b/src/theory/quantifiers/term_registry.cpp index 1377ad23d..d23ff060a 100644 --- a/src/theory/quantifiers/term_registry.cpp +++ b/src/theory/quantifiers/term_registry.cpp @@ -22,19 +22,26 @@ namespace CVC4 { namespace theory { namespace quantifiers { -TermRegistry::TermRegistry(QuantifiersState& qs, - QuantifiersInferenceManager& qim, - QuantifiersRegistry& qr) +TermRegistry::TermRegistry(QuantifiersState& qs, QuantifiersRegistry& qr) : d_presolve(qs.getUserContext(), true), d_presolveCache(qs.getUserContext()), d_termEnum(new TermEnumeration), - d_termDb(new TermDb(qs, qim, qr)), + d_termDb(new TermDb(qs, qr)), d_sygusTdb(nullptr) { if (options::sygus() || options::sygusInst()) { // must be constructed here since it is required for datatypes finistInit - d_sygusTdb.reset(new TermDbSygus(qs, qim)); + d_sygusTdb.reset(new TermDbSygus(qs)); + } +} + +void TermRegistry::finishInit(QuantifiersInferenceManager* qim) +{ + d_termDb->finishInit(qim); + if (d_sygusTdb.get()) + { + d_sygusTdb->finishInit(qim); } } diff --git a/src/theory/quantifiers/term_registry.h b/src/theory/quantifiers/term_registry.h index 624787285..1d9058603 100644 --- a/src/theory/quantifiers/term_registry.h +++ b/src/theory/quantifiers/term_registry.h @@ -39,8 +39,9 @@ class TermRegistry public: TermRegistry(QuantifiersState& qs, - QuantifiersInferenceManager& qim, QuantifiersRegistry& qr); + /** Finish init, which sets the inference manager on modules of this class */ + void finishInit(QuantifiersInferenceManager* qim); /** Presolve */ void presolve(); diff --git a/src/theory/quantifiers/term_tuple_enumerator.cpp b/src/theory/quantifiers/term_tuple_enumerator.cpp index 1466e1026..190e51c54 100644 --- a/src/theory/quantifiers/term_tuple_enumerator.cpp +++ b/src/theory/quantifiers/term_tuple_enumerator.cpp @@ -27,6 +27,7 @@ #include "theory/quantifiers/index_trie.h" #include "theory/quantifiers/quant_module.h" #include "theory/quantifiers/relevant_domain.h" +#include "theory/quantifiers/term_registry.h" #include "theory/quantifiers/term_util.h" #include "theory/quantifiers_engine.h" #include "util/statistics_registry.h" diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp index 5802e1abc..e054fd309 100644 --- a/src/theory/quantifiers/theory_quantifiers.cpp +++ b/src/theory/quantifiers/theory_quantifiers.cpp @@ -44,9 +44,18 @@ TheoryQuantifiers::TheoryQuantifiers(Context* c, ProofNodeManager* pnm) : Theory(THEORY_QUANTIFIERS, c, u, out, valuation, logicInfo, pnm), d_qstate(c, u, valuation, logicInfo), + d_qreg(), + d_treg(d_qstate, d_qreg), d_qim(*this, d_qstate, pnm), - d_qengine(d_qstate, d_qim, pnm) + d_qengine(d_qstate, d_qreg, d_treg, d_qim, pnm) { + // Finish initializing the term registry by hooking it up to the inference + // manager. This is required due to a cyclic dependency between the term + // database and the instantiate module. Term database needs inference manager + // since it sends out lemmas when term indexing is inconsistent, instantiate + // needs term database for entailment checks. + d_treg.finishInit(&d_qim); + out.handleUserAttribute( "fun-def", this ); out.handleUserAttribute("qid", this); out.handleUserAttribute( "quant-inst-max-level", this ); diff --git a/src/theory/quantifiers/theory_quantifiers.h b/src/theory/quantifiers/theory_quantifiers.h index 8b85a1bf6..e9785fcea 100644 --- a/src/theory/quantifiers/theory_quantifiers.h +++ b/src/theory/quantifiers/theory_quantifiers.h @@ -22,8 +22,10 @@ #include "expr/node.h" #include "theory/quantifiers/proof_checker.h" #include "theory/quantifiers/quantifiers_inference_manager.h" +#include "theory/quantifiers/quantifiers_registry.h" #include "theory/quantifiers/quantifiers_rewriter.h" #include "theory/quantifiers/quantifiers_state.h" +#include "theory/quantifiers/term_registry.h" #include "theory/quantifiers_engine.h" #include "theory/theory.h" #include "theory/valuation.h" @@ -84,6 +86,10 @@ class TheoryQuantifiers : public Theory { QuantifiersProofRuleChecker d_qChecker; /** The quantifiers state */ QuantifiersState d_qstate; + /** The quantifiers registry */ + quantifiers::QuantifiersRegistry d_qreg; + /** The term registry */ + quantifiers::TermRegistry d_treg; /** The quantifiers inference manager */ QuantifiersInferenceManager d_qim; /** The quantifiers engine, which lives here */ diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 24919fae0..c41fa36e6 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -26,17 +26,17 @@ #include "theory/quantifiers/fmf/first_order_model_fmc.h" #include "theory/quantifiers/fmf/full_model_check.h" #include "theory/quantifiers/fmf/model_builder.h" +#include "theory/quantifiers/quant_module.h" #include "theory/quantifiers/quantifiers_inference_manager.h" #include "theory/quantifiers/quantifiers_modules.h" +#include "theory/quantifiers/quantifiers_registry.h" #include "theory/quantifiers/quantifiers_rewriter.h" #include "theory/quantifiers/quantifiers_state.h" -#include "theory/quantifiers/quant_module.h" #include "theory/quantifiers/relevant_domain.h" #include "theory/quantifiers/skolemize.h" -#include "theory/quantifiers/sygus/term_database_sygus.h" -#include "theory/quantifiers/term_util.h" -#include "theory/quantifiers/term_database.h" #include "theory/quantifiers/term_enumeration.h" +#include "theory/quantifiers/term_registry.h" +#include "theory/quantifiers/term_util.h" #include "theory/theory_engine.h" #include "theory/uf/equality_engine.h" @@ -48,6 +48,8 @@ namespace theory { QuantifiersEngine::QuantifiersEngine( quantifiers::QuantifiersState& qstate, + quantifiers::QuantifiersRegistry& qr, + quantifiers::TermRegistry& tr, quantifiers::QuantifiersInferenceManager& qim, ProofNodeManager* pnm) : d_qstate(qstate), @@ -55,8 +57,8 @@ QuantifiersEngine::QuantifiersEngine( d_te(nullptr), d_decManager(nullptr), d_pnm(pnm), - d_qreg(), - d_treg(qstate, qim, d_qreg), + d_qreg(qr), + d_treg(tr), d_tr_trie(new inst::TriggerTrie), d_model(nullptr), d_builder(nullptr), diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index 91c21a650..c7c716105 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -24,8 +24,6 @@ #include "context/cdhashset.h" #include "context/cdlist.h" #include "theory/quantifiers/quant_util.h" -#include "theory/quantifiers/quantifiers_registry.h" -#include "theory/quantifiers/term_registry.h" #include "util/statistics_registry.h" namespace CVC4 { @@ -49,10 +47,12 @@ class QModelBuilder; class QuantifiersInferenceManager; class QuantifiersModules; class QuantifiersState; +class QuantifiersRegistry; class Skolemize; class TermDb; class TermDbSygus; class TermEnumeration; +class TermRegistry; } // TODO: organize this more/review this, github issue #1163 @@ -65,6 +65,8 @@ class QuantifiersEngine { public: QuantifiersEngine(quantifiers::QuantifiersState& qstate, + quantifiers::QuantifiersRegistry& qr, + quantifiers::TermRegistry& tr, quantifiers::QuantifiersInferenceManager& qim, ProofNodeManager* pnm); ~QuantifiersEngine(); @@ -270,9 +272,9 @@ public: std::vector d_modules; //------------- quantifiers utilities /** The quantifiers registry */ - quantifiers::QuantifiersRegistry d_qreg; + quantifiers::QuantifiersRegistry& d_qreg; /** The term registry */ - quantifiers::TermRegistry d_treg; + quantifiers::TermRegistry& d_treg; /** all triggers will be stored in this trie */ std::unique_ptr d_tr_trie; /** extended model object */ -- 2.30.2