diff options
-rw-r--r-- | src/theory/quantifiers/instantiate.cpp | 30 | ||||
-rw-r--r-- | src/theory/quantifiers/instantiate.h | 19 | ||||
-rw-r--r-- | src/theory/quantifiers/quantifiers_inference_manager.cpp | 24 | ||||
-rw-r--r-- | src/theory/quantifiers/quantifiers_inference_manager.h | 18 | ||||
-rw-r--r-- | src/theory/quantifiers/theory_quantifiers.cpp | 45 | ||||
-rw-r--r-- | src/theory/quantifiers/theory_quantifiers.h | 2 | ||||
-rw-r--r-- | src/theory/quantifiers_engine.cpp | 27 | ||||
-rw-r--r-- | 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<Node>& 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<Node>& qs) @@ -704,7 +706,7 @@ void Instantiate::debugPrint(std::ostream& out) for (std::pair<const Node, uint32_t>& 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<Node, uint32_t, NodeHashFunction> 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<InstantiationRewriter*> 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<Instantiate> d_instantiate; + /** skolemize utility */ + std::unique_ptr<Skolemize> 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<QuantifiersInferenceManager> d_qim; /** The quantifiers engine, which lives here */ std::unique_ptr<QuantifiersEngine> 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<Node>& qs) { - d_instantiate->getInstantiatedQuantifiedFormulas(qs); + d_qim.getInstantiate()->getInstantiatedQuantifiedFormulas(qs); } void QuantifiersEngine::getSkolemTermVectors( std::map<Node, std::vector<Node> >& 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<inst::TriggerTrie> d_tr_trie; /** extended model object */ quantifiers::FirstOrderModel* d_model; - /** instantiate utility */ - std::unique_ptr<quantifiers::Instantiate> d_instantiate; - /** skolemize utility */ - std::unique_ptr<quantifiers::Skolemize> d_skolemize; //------------- end quantifiers utilities /** * The modules utility, which contains all of the quantifiers modules. |