From 61b9dadc88de3bf7d52538f9e914cfb61cbb7bb6 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 22 Mar 2021 20:32:32 -0500 Subject: [PATCH] Moving instantiate and skolemize into quantifiers inference manager (#6188) After this PR, utilities for instantiation are available from the quantifiers inference manager instead of quantifiers engine. This means that the majority of the dependencies on quantifiers engine will (finally) start being cleaned up after this PR. --- src/theory/quantifiers/instantiate.cpp | 30 +++++++------ src/theory/quantifiers/instantiate.h | 19 ++++---- .../quantifiers_inference_manager.cpp | 24 +++++++++- .../quantifiers_inference_manager.h | 18 ++++++++ src/theory/quantifiers/theory_quantifiers.cpp | 45 +++++++++---------- src/theory/quantifiers/theory_quantifiers.h | 2 +- src/theory/quantifiers_engine.cpp | 27 +++++------ src/theory/quantifiers_engine.h | 4 -- 8 files changed, 101 insertions(+), 68 deletions(-) diff --git a/src/theory/quantifiers/instantiate.cpp b/src/theory/quantifiers/instantiate.cpp index be6101b81..fd74e17e8 100644 --- a/src/theory/quantifiers/instantiate.cpp +++ b/src/theory/quantifiers/instantiate.cpp @@ -29,6 +29,7 @@ #include "theory/quantifiers/quantifiers_rewriter.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/quantifiers_engine.h" #include "theory/rewriter.h" @@ -40,17 +41,18 @@ namespace CVC4 { namespace theory { namespace quantifiers { -Instantiate::Instantiate(QuantifiersEngine* qe, - QuantifiersState& qs, +Instantiate::Instantiate(QuantifiersState& qs, QuantifiersInferenceManager& qim, QuantifiersRegistry& qr, + TermRegistry& tr, + FirstOrderModel* m, ProofNodeManager* pnm) - : d_qe(qe), - d_qstate(qs), + : d_qstate(qs), d_qim(qim), d_qreg(qr), + d_treg(tr), + d_model(m), d_pnm(pnm), - d_term_db(nullptr), d_total_inst_debug(qs.getUserContext()), d_c_inst_match_trie_dom(qs.getUserContext()), d_pfInst(pnm ? new CDProof(pnm) : nullptr) @@ -79,7 +81,6 @@ bool Instantiate::reset(Theory::Effort e) } d_recorded_inst.clear(); } - d_term_db = d_qe->getTermDatabase(); return true; } @@ -111,7 +112,6 @@ bool Instantiate::addInstantiation(Node q, d_qim.safePoint(ResourceManager::Resource::QuantifierStep); Assert(!d_qstate.isInConflict()); Assert(terms.size() == q[0].getNumChildren()); - Assert(d_term_db != nullptr); Trace("inst-add-debug") << "For quantified formula " << q << ", add instantiation: " << std::endl; for (unsigned i = 0, size = terms.size(); i < size; i++) @@ -131,7 +131,7 @@ bool Instantiate::addInstantiation(Node q, { // pick the best possible representative for instantiation, based on past // use and simplicity of term - terms[i] = d_qe->getModel()->getInternalRepresentative(terms[i], q, i); + terms[i] = d_model->getInternalRepresentative(terms[i], q, i); } Trace("inst-add-debug") << " -> " << terms[i] << std::endl; if (terms[i].isNull()) @@ -188,6 +188,7 @@ bool Instantiate::addInstantiation(Node q, #endif } + TermDb* tdb = d_treg.getTermDatabase(); // Note we check for entailment before checking for term vector duplication. // Although checking for term vector duplication is a faster check, it is // included automatically with recordInstantiationInternal, hence we prefer @@ -210,7 +211,7 @@ bool Instantiate::addInstantiation(Node q, { subs[q[0][i]] = terms[i]; } - if (d_term_db->isEntailed(q[1], subs, false, true)) + if (tdb->isEntailed(q[1], subs, false, true)) { Trace("inst-add-debug") << " --> Currently entailed." << std::endl; ++(d_statistics.d_inst_duplicate_ent); @@ -223,7 +224,7 @@ bool Instantiate::addInstantiation(Node q, { for (Node& t : terms) { - if (!d_term_db->isTermEligibleForInstantiation(t, q)) + if (!tdb->isTermEligibleForInstantiation(t, q)) { return false; } @@ -408,6 +409,7 @@ bool Instantiate::addInstantiationExpFail(Node q, // will never succeed with 1 variable return false; } + TermDb* tdb = d_treg.getTermDatabase(); Trace("inst-exp-fail") << "Explain inst failure..." << terms << std::endl; // set up information for below std::vector& vars = d_qreg.d_vars[q]; @@ -441,7 +443,7 @@ bool Instantiate::addInstantiationExpFail(Node q, if (options::instNoEntail()) { Trace("inst-exp-fail") << " check entailment" << std::endl; - success = d_term_db->isEntailed(q[1], subs, false, true); + success = tdb->isEntailed(q[1], subs, false, true); Trace("inst-exp-fail") << " entailed: " << success << std::endl; } // check whether the instantiation rewrites to the same thing @@ -615,9 +617,9 @@ Node Instantiate::getTermForType(TypeNode tn) { if (tn.isClosedEnumerable()) { - return d_qe->getTermEnumeration()->getEnumerateTerm(tn, 0); + return d_treg.getTermEnumeration()->getEnumerateTerm(tn, 0); } - return d_qe->getTermDatabase()->getOrMakeTypeGroundTerm(tn); + return d_treg.getTermDatabase()->getOrMakeTypeGroundTerm(tn); } void Instantiate::getInstantiatedQuantifiedFormulas(std::vector& qs) @@ -704,7 +706,7 @@ void Instantiate::debugPrint(std::ostream& out) for (std::pair& i : d_temp_inst_debug) { Node name; - if (!d_qe->getNameForQuant(i.first, name, req)) + if (!d_qreg.getNameForQuant(i.first, name, req)) { continue; } diff --git a/src/theory/quantifiers/instantiate.h b/src/theory/quantifiers/instantiate.h index abdee69ef..8e556b648 100644 --- a/src/theory/quantifiers/instantiate.h +++ b/src/theory/quantifiers/instantiate.h @@ -32,15 +32,13 @@ namespace CVC4 { class LazyCDProof; namespace theory { - -class QuantifiersEngine; - namespace quantifiers { -class TermDb; +class TermRegistry; class QuantifiersState; class QuantifiersInferenceManager; class QuantifiersRegistry; +class FirstOrderModel; /** Instantiation rewriter * @@ -95,10 +93,11 @@ class Instantiate : public QuantifiersUtil typedef context::CDHashMap NodeUIntMap; public: - Instantiate(QuantifiersEngine* qe, - QuantifiersState& qs, + Instantiate(QuantifiersState& qs, QuantifiersInferenceManager& qim, QuantifiersRegistry& qr, + TermRegistry& tr, + FirstOrderModel* m, ProofNodeManager* pnm = nullptr); ~Instantiate(); @@ -311,18 +310,18 @@ class Instantiate : public QuantifiersUtil */ static Node ensureType(Node n, TypeNode tn); - /** pointer to the quantifiers engine */ - QuantifiersEngine* d_qe; /** Reference to the quantifiers state */ QuantifiersState& d_qstate; /** Reference to the quantifiers inference manager */ QuantifiersInferenceManager& d_qim; /** The quantifiers registry */ QuantifiersRegistry& d_qreg; + /** Reference to the term registry */ + TermRegistry& d_treg; + /** Pointer to the model */ + FirstOrderModel* d_model; /** pointer to the proof node manager */ ProofNodeManager* d_pnm; - /** cache of term database for quantifiers engine */ - TermDb* d_term_db; /** 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 8469720c4..9a82265f9 100644 --- a/src/theory/quantifiers/quantifiers_inference_manager.cpp +++ b/src/theory/quantifiers/quantifiers_inference_manager.cpp @@ -14,18 +14,38 @@ #include "theory/quantifiers/quantifiers_inference_manager.h" +#include "theory/quantifiers/instantiate.h" +#include "theory/quantifiers/skolemize.h" + namespace CVC4 { namespace theory { namespace quantifiers { QuantifiersInferenceManager::QuantifiersInferenceManager( - Theory& t, QuantifiersState& state, ProofNodeManager* pnm) - : InferenceManagerBuffered(t, state, pnm, "theory::quantifiers") + Theory& t, + QuantifiersState& state, + QuantifiersRegistry& qr, + TermRegistry& tr, + FirstOrderModel* m, + ProofNodeManager* pnm) + : InferenceManagerBuffered(t, state, pnm, "theory::quantifiers"), + d_instantiate(new Instantiate(state, *this, qr, tr, m, pnm)), + d_skolemize(new Skolemize(state, pnm)) { } QuantifiersInferenceManager::~QuantifiersInferenceManager() {} +Instantiate* QuantifiersInferenceManager::getInstantiate() +{ + return d_instantiate.get(); +} + +Skolemize* QuantifiersInferenceManager::getSkolemize() +{ + return d_skolemize.get(); +} + void QuantifiersInferenceManager::doPending() { doPendingLemmas(); diff --git a/src/theory/quantifiers/quantifiers_inference_manager.h b/src/theory/quantifiers/quantifiers_inference_manager.h index 76b7d0982..aa7fc1b6a 100644 --- a/src/theory/quantifiers/quantifiers_inference_manager.h +++ b/src/theory/quantifiers/quantifiers_inference_manager.h @@ -24,6 +24,11 @@ namespace CVC4 { namespace theory { namespace quantifiers { +class Instantiate; +class Skolemize; +class QuantifiersRegistry; +class TermRegistry; +class FirstOrderModel; /** * The quantifiers inference manager. */ @@ -32,12 +37,25 @@ class QuantifiersInferenceManager : public InferenceManagerBuffered public: QuantifiersInferenceManager(Theory& t, QuantifiersState& state, + QuantifiersRegistry& qr, + TermRegistry& tr, + FirstOrderModel* m, ProofNodeManager* pnm); ~QuantifiersInferenceManager(); + /** get instantiate utility */ + Instantiate* getInstantiate(); + /** get skolemize utility */ + Skolemize* getSkolemize(); /** * Do all pending lemmas, then do all pending phase requirements. */ void doPending(); + + private: + /** instantiate utility */ + std::unique_ptr d_instantiate; + /** skolemize utility */ + std::unique_ptr d_skolemize; }; } // namespace quantifiers diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp index 5bcc80eb0..092689b5f 100644 --- a/src/theory/quantifiers/theory_quantifiers.cpp +++ b/src/theory/quantifiers/theory_quantifiers.cpp @@ -41,15 +41,9 @@ TheoryQuantifiers::TheoryQuantifiers(Context* c, d_qstate(c, u, valuation, logicInfo), d_qreg(), d_treg(d_qstate, d_qreg), - d_qim(*this, d_qstate, pnm) + d_qim(nullptr), + d_qengine(nullptr) { - // 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 ); @@ -62,10 +56,6 @@ TheoryQuantifiers::TheoryQuantifiers(Context* c, // add the proof rules d_qChecker.registerTo(pc); } - // indicate we are using the quantifiers theory state object - d_theoryState = &d_qstate; - // use the inference manager as the official inference manager - d_inferManager = &d_qim; Trace("quant-engine-debug") << "Initialize quantifiers engine." << std::endl; Trace("quant-engine-debug") @@ -73,18 +63,11 @@ TheoryQuantifiers::TheoryQuantifiers(Context* c, // Finite model finding requires specialized ways of building the model. // We require constructing the model here, since it is required for // initializing the CombinationEngine and the rest of quantifiers engine. - if (options::finiteModelFind() || options::fmfBound()) + if ((options::finiteModelFind() || options::fmfBound()) + && QuantifiersModules::useFmcModel()) { - if (QuantifiersModules::useFmcModel()) - { - d_qmodel.reset(new quantifiers::fmcheck::FirstOrderModelFmc( - d_qstate, d_qreg, d_treg, "FirstOrderModelFmc")); - } - else - { - d_qmodel.reset(new quantifiers::FirstOrderModel( - d_qstate, d_qreg, d_treg, "FirstOrderModel")); - } + d_qmodel.reset(new quantifiers::fmcheck::FirstOrderModelFmc( + d_qstate, d_qreg, d_treg, "FirstOrderModelFmc")); } else { @@ -92,13 +75,27 @@ TheoryQuantifiers::TheoryQuantifiers(Context* c, d_qstate, d_qreg, d_treg, "FirstOrderModel")); } + d_qim.reset(new QuantifiersInferenceManager( + *this, d_qstate, d_qreg, d_treg, d_qmodel.get(), 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.get()); + // construct the quantifiers engine d_qengine.reset(new QuantifiersEngine( - d_qstate, d_qreg, d_treg, d_qim, d_qmodel.get(), pnm)); + d_qstate, d_qreg, d_treg, *d_qim.get(), d_qmodel.get(), pnm)); //!!!!!!!!!!!!!! temporary (project #15) d_qmodel->finishInit(d_qengine.get()); + // indicate we are using the quantifiers theory state object + d_theoryState = &d_qstate; + // use the inference manager as the official inference manager + d_inferManager = d_qim.get(); // Set the pointer to the quantifiers engine, which this theory owns. This // pointer will be retreived by TheoryEngine and set to all theories // post-construction. diff --git a/src/theory/quantifiers/theory_quantifiers.h b/src/theory/quantifiers/theory_quantifiers.h index 9714ec718..2371b00ce 100644 --- a/src/theory/quantifiers/theory_quantifiers.h +++ b/src/theory/quantifiers/theory_quantifiers.h @@ -94,7 +94,7 @@ class TheoryQuantifiers : public Theory { /** The term registry */ TermRegistry d_treg; /** The quantifiers inference manager */ - QuantifiersInferenceManager d_qim; + std::unique_ptr d_qim; /** The quantifiers engine, which lives here */ std::unique_ptr d_qengine; };/* class TheoryQuantifiers */ diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 68962de72..9ca8226bc 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -62,9 +62,6 @@ QuantifiersEngine::QuantifiersEngine( d_treg(tr), d_tr_trie(new inst::TriggerTrie), d_model(qm), - d_instantiate( - new quantifiers::Instantiate(this, qstate, qim, d_qreg, pnm)), - d_skolemize(new quantifiers::Skolemize(d_qstate, d_pnm)), d_quants_prereg(qstate.getUserContext()), d_quants_red(qstate.getUserContext()) { @@ -73,7 +70,7 @@ QuantifiersEngine::QuantifiersEngine( // quantifiers registry must come before the remaining utilities d_util.push_back(&d_qreg); d_util.push_back(tr.getTermDatabase()); - d_util.push_back(d_instantiate.get()); + d_util.push_back(qim.getInstantiate()); } QuantifiersEngine::~QuantifiersEngine() {} @@ -125,6 +122,9 @@ quantifiers::FirstOrderModel* QuantifiersEngine::getModel() const { return d_model; } + +/// !!!!!!!!!!!!!! temporary (project #15) + quantifiers::TermDb* QuantifiersEngine::getTermDatabase() const { return d_treg.getTermDatabase(); @@ -139,16 +139,17 @@ quantifiers::TermEnumeration* QuantifiersEngine::getTermEnumeration() const } quantifiers::Instantiate* QuantifiersEngine::getInstantiate() const { - return d_instantiate.get(); + return d_qim.getInstantiate(); } quantifiers::Skolemize* QuantifiersEngine::getSkolemize() const { - return d_skolemize.get(); + return d_qim.getSkolemize(); } inst::TriggerTrie* QuantifiersEngine::getTriggerDatabase() const { return d_tr_trie.get(); } +/// !!!!!!!!!!!!!! void QuantifiersEngine::presolve() { Trace("quant-engine-proc") << "QuantifiersEngine : presolve " << std::endl; @@ -468,7 +469,7 @@ void QuantifiersEngine::check( Theory::Effort e ){ { Options& sopts = smt::currentSmtEngine()->getOptions(); std::ostream& out = *sopts.getOut(); - d_instantiate->debugPrint(out); + d_qim.getInstantiate()->debugPrint(out); } } if( Trace.isOn("quant-engine") ){ @@ -491,7 +492,7 @@ void QuantifiersEngine::check( Theory::Effort e ){ d_qim.setIncomplete(); } //output debug stats - d_instantiate->debugPrintModel(); + d_qim.getInstantiate()->debugPrintModel(); } } @@ -611,7 +612,7 @@ void QuantifiersEngine::assertQuantifier( Node f, bool pol ){ } if( !pol ){ // do skolemization - TrustNode lem = d_skolemize->process(f); + TrustNode lem = d_qim.getSkolemize()->process(f); if (!lem.isNull()) { if (Trace.isOn("quantifiers-sk-debug")) @@ -645,11 +646,11 @@ void QuantifiersEngine::markRelevant( Node q ) { } void QuantifiersEngine::getInstantiationTermVectors( Node q, std::vector< std::vector< Node > >& tvecs ) { - d_instantiate->getInstantiationTermVectors(q, tvecs); + d_qim.getInstantiate()->getInstantiationTermVectors(q, tvecs); } void QuantifiersEngine::getInstantiationTermVectors( std::map< Node, std::vector< std::vector< Node > > >& insts ) { - d_instantiate->getInstantiationTermVectors(insts); + d_qim.getInstantiate()->getInstantiationTermVectors(insts); } void QuantifiersEngine::printSynthSolution( std::ostream& out ) { @@ -663,13 +664,13 @@ void QuantifiersEngine::printSynthSolution( std::ostream& out ) { void QuantifiersEngine::getInstantiatedQuantifiedFormulas(std::vector& qs) { - d_instantiate->getInstantiatedQuantifiedFormulas(qs); + d_qim.getInstantiate()->getInstantiatedQuantifiedFormulas(qs); } void QuantifiersEngine::getSkolemTermVectors( std::map >& sks) const { - d_skolemize->getSkolemTermVectors(sks); + d_qim.getSkolemize()->getSkolemTermVectors(sks); } QuantifiersEngine::Statistics::Statistics() diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index 4d3029ca9..b6562caa7 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -237,10 +237,6 @@ public: std::unique_ptr d_tr_trie; /** extended model object */ quantifiers::FirstOrderModel* d_model; - /** instantiate utility */ - std::unique_ptr d_instantiate; - /** skolemize utility */ - std::unique_ptr d_skolemize; //------------- end quantifiers utilities /** * The modules utility, which contains all of the quantifiers modules. -- 2.30.2