From d5d526730d11d08c65aa17ea53d0dffb0a72e692 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 23 Mar 2021 15:41:13 -0500 Subject: [PATCH] Passing term registry to ematching utilities (#6190) Model is now nested into term registry. This PR also resolves some complications due to namespaces within quantifiers. --- .../ematching/candidate_generator.cpp | 83 +++++++++++-------- .../ematching/candidate_generator.h | 36 ++++---- .../quantifiers/ematching/ho_trigger.cpp | 23 ++--- src/theory/quantifiers/ematching/ho_trigger.h | 15 ++-- .../quantifiers/ematching/im_generator.cpp | 11 +-- .../quantifiers/ematching/im_generator.h | 9 +- .../ematching/inst_match_generator.cpp | 25 +++--- .../ematching/inst_match_generator.h | 2 + .../ematching/inst_match_generator_multi.cpp | 7 +- .../ematching/inst_match_generator_multi.h | 2 + .../inst_match_generator_multi_linear.cpp | 5 +- .../inst_match_generator_multi_linear.h | 2 + .../ematching/inst_match_generator_simple.cpp | 12 +-- .../ematching/inst_match_generator_simple.h | 2 + .../quantifiers/ematching/inst_strategy.cpp | 5 +- .../quantifiers/ematching/inst_strategy.h | 8 +- .../ematching/inst_strategy_e_matching.cpp | 8 +- .../ematching/inst_strategy_e_matching.h | 1 + .../inst_strategy_e_matching_user.cpp | 18 ++-- .../ematching/inst_strategy_e_matching_user.h | 3 +- .../ematching/instantiation_engine.cpp | 11 +-- .../ematching/instantiation_engine.h | 3 +- .../ematching/pattern_term_selector.cpp | 2 + .../ematching/pattern_term_selector.h | 2 + src/theory/quantifiers/ematching/trigger.cpp | 51 +++++++----- src/theory/quantifiers/ematching/trigger.h | 40 +++++---- .../ematching/trigger_term_info.cpp | 2 + .../quantifiers/ematching/trigger_term_info.h | 2 + .../quantifiers/ematching/trigger_trie.cpp | 2 + .../quantifiers/ematching/trigger_trie.h | 3 +- .../ematching/var_match_generator.cpp | 2 + .../ematching/var_match_generator.h | 2 + .../quantifiers/fmf/full_model_check.cpp | 16 ++-- src/theory/quantifiers/fmf/model_engine.cpp | 12 +-- src/theory/quantifiers/inst_match.cpp | 4 +- src/theory/quantifiers/inst_match.h | 10 +-- src/theory/quantifiers/inst_match_trie.cpp | 4 +- src/theory/quantifiers/inst_match_trie.h | 23 ++--- .../quantifiers/inst_strategy_enumerative.cpp | 3 +- src/theory/quantifiers/instantiate.cpp | 39 +++------ src/theory/quantifiers/instantiate.h | 18 +--- .../quantifiers_inference_manager.cpp | 3 +- .../quantifiers_inference_manager.h | 1 - .../quantifiers/quantifiers_modules.cpp | 15 ++-- src/theory/quantifiers/quantifiers_modules.h | 4 +- src/theory/quantifiers/term_database.cpp | 2 - src/theory/quantifiers/term_registry.cpp | 37 +++++++++ src/theory/quantifiers/term_registry.h | 23 +++++ src/theory/quantifiers/term_util.cpp | 3 - src/theory/quantifiers/theory_quantifiers.cpp | 34 ++------ src/theory/quantifiers/theory_quantifiers.h | 5 +- src/theory/quantifiers_engine.cpp | 9 +- src/theory/quantifiers_engine.h | 9 +- 53 files changed, 376 insertions(+), 297 deletions(-) diff --git a/src/theory/quantifiers/ematching/candidate_generator.cpp b/src/theory/quantifiers/ematching/candidate_generator.cpp index 4cc912e45..60350f882 100644 --- a/src/theory/quantifiers/ematching/candidate_generator.cpp +++ b/src/theory/quantifiers/ematching/candidate_generator.cpp @@ -19,30 +19,37 @@ #include "smt/smt_engine.h" #include "smt/smt_engine_scope.h" #include "theory/quantifiers/first_order_model.h" -#include "theory/quantifiers/inst_match.h" -#include "theory/quantifiers/instantiate.h" #include "theory/quantifiers/quantifiers_state.h" #include "theory/quantifiers/term_database.h" +#include "theory/quantifiers/term_registry.h" #include "theory/quantifiers/term_util.h" -#include "theory/quantifiers_engine.h" using namespace CVC4::kind; namespace CVC4 { namespace theory { +namespace quantifiers { namespace inst { +CandidateGenerator::CandidateGenerator(QuantifiersState& qs, TermRegistry& tr) + : d_qs(qs), d_treg(tr) +{ +} + bool CandidateGenerator::isLegalCandidate( Node n ){ - return d_qe->getTermDatabase()->isTermActive( n ) && ( !options::cegqi() || !quantifiers::TermUtil::hasInstConstAttr(n) ); + return d_treg.getTermDatabase()->isTermActive(n) + && (!options::cegqi() || !quantifiers::TermUtil::hasInstConstAttr(n)); } -CandidateGeneratorQE::CandidateGeneratorQE(QuantifiersEngine* qe, Node pat) - : CandidateGenerator(qe), +CandidateGeneratorQE::CandidateGeneratorQE(QuantifiersState& qs, + TermRegistry& tr, + Node pat) + : CandidateGenerator(qs, tr), d_term_iter(-1), d_term_iter_limit(0), d_mode(cand_term_none) { - d_op = qe->getTermDatabase()->getMatchOperator( pat ); + d_op = d_treg.getTermDatabase()->getMatchOperator(pat); Assert(!d_op.isNull()); } @@ -53,16 +60,16 @@ void CandidateGeneratorQE::resetForOperator(Node eqc, Node op) d_term_iter = 0; d_eqc = eqc; d_op = op; - d_term_iter_limit = d_qe->getTermDatabase()->getNumGroundTerms(d_op); + d_term_iter_limit = d_treg.getTermDatabase()->getNumGroundTerms(d_op); if( eqc.isNull() ){ d_mode = cand_term_db; }else{ if( isExcludedEqc( eqc ) ){ d_mode = cand_term_none; }else{ - eq::EqualityEngine* ee = d_qe->getState().getEqualityEngine(); + eq::EqualityEngine* ee = d_qs.getEqualityEngine(); if( ee->hasTerm( eqc ) ){ - TNodeTrie* tat = d_qe->getTermDatabase()->getTermArgTrie(eqc, op); + TNodeTrie* tat = d_treg.getTermDatabase()->getTermArgTrie(eqc, op); if( tat ){ //create an equivalence class iterator in eq class eqc Node rep = ee->getRepresentative( eqc ); @@ -81,7 +88,7 @@ void CandidateGeneratorQE::resetForOperator(Node eqc, Node op) bool CandidateGeneratorQE::isLegalOpCandidate( Node n ) { if( n.hasOperator() ){ if( isLegalCandidate( n ) ){ - return d_qe->getTermDatabase()->getMatchOperator( n )==d_op; + return d_treg.getTermDatabase()->getMatchOperator(n) == d_op; } } return false; @@ -94,18 +101,18 @@ Node CandidateGeneratorQE::getNextCandidate(){ Node CandidateGeneratorQE::getNextCandidateInternal() { if( d_mode==cand_term_db ){ - quantifiers::QuantifiersState& qs = d_qe->getState(); Debug("cand-gen-qe") << "...get next candidate in tbd" << std::endl; //get next candidate term in the uf term database while( d_term_itergetTermDatabase()->getGroundTerm( d_op, d_term_iter ); + Node n = d_treg.getTermDatabase()->getGroundTerm(d_op, d_term_iter); d_term_iter++; if( isLegalCandidate( n ) ){ - if( d_qe->getTermDatabase()->hasTermCurrent( n ) ){ + if (d_treg.getTermDatabase()->hasTermCurrent(n)) + { if( d_exclude_eqc.empty() ){ return n; }else{ - Node r = qs.getRepresentative(n); + Node r = d_qs.getRepresentative(n); if( d_exclude_eqc.find( r )==d_exclude_eqc.end() ){ Debug("cand-gen-qe") << "...returning " << n << std::endl; return n; @@ -138,14 +145,17 @@ Node CandidateGeneratorQE::getNextCandidateInternal() return Node::null(); } -CandidateGeneratorQELitDeq::CandidateGeneratorQELitDeq( QuantifiersEngine* qe, Node mpat ) : -CandidateGenerator( qe ), d_match_pattern( mpat ){ +CandidateGeneratorQELitDeq::CandidateGeneratorQELitDeq(QuantifiersState& qs, + TermRegistry& tr, + Node mpat) + : CandidateGenerator(qs, tr), d_match_pattern(mpat) +{ Assert(d_match_pattern.getKind() == EQUAL); d_match_pattern_type = d_match_pattern[0].getType(); } void CandidateGeneratorQELitDeq::reset( Node eqc ){ - eq::EqualityEngine* ee = d_qe->getState().getEqualityEngine(); + eq::EqualityEngine* ee = d_qs.getEqualityEngine(); Node falset = NodeManager::currentNM()->mkConst(false); d_eqc_false = eq::EqClassIterator(falset, ee); } @@ -169,9 +179,11 @@ Node CandidateGeneratorQELitDeq::getNextCandidate(){ return Node::null(); } - -CandidateGeneratorQEAll::CandidateGeneratorQEAll( QuantifiersEngine* qe, Node mpat ) : - CandidateGenerator( qe ), d_match_pattern( mpat ){ +CandidateGeneratorQEAll::CandidateGeneratorQEAll(QuantifiersState& qs, + TermRegistry& tr, + Node mpat) + : CandidateGenerator(qs, tr), d_match_pattern(mpat) +{ d_match_pattern_type = mpat.getType(); Assert(mpat.getKind() == INST_CONSTANT); d_f = quantifiers::TermUtil::getInstConstAttr( mpat ); @@ -180,12 +192,12 @@ CandidateGeneratorQEAll::CandidateGeneratorQEAll( QuantifiersEngine* qe, Node mp } void CandidateGeneratorQEAll::reset( Node eqc ) { - d_eq = eq::EqClassesIterator(d_qe->getState().getEqualityEngine()); + d_eq = eq::EqClassesIterator(d_qs.getEqualityEngine()); d_firstTime = true; } Node CandidateGeneratorQEAll::getNextCandidate() { - quantifiers::TermDb* tdb = d_qe->getTermDatabase(); + quantifiers::TermDb* tdb = d_treg.getTermDatabase(); while( !d_eq.isFinished() ){ TNode n = (*d_eq); ++d_eq; @@ -194,7 +206,7 @@ Node CandidateGeneratorQEAll::getNextCandidate() { if( !nh.isNull() ){ if (options::instMaxLevel() != -1) { - nh = d_qe->getModel()->getInternalRepresentative(nh, d_f, d_index); + nh = d_treg.getModel()->getInternalRepresentative(nh, d_f, d_index); //don't consider this if already the instantiation is ineligible if (!nh.isNull() && !tdb->isTermEligibleForInstantiation(nh, d_f)) { @@ -212,14 +224,15 @@ Node CandidateGeneratorQEAll::getNextCandidate() { if( d_firstTime ){ //must return something d_firstTime = false; - return d_qe->getInstantiate()->getTermForType(d_match_pattern_type); + return d_treg.getTermForType(d_match_pattern_type); } return Node::null(); } -CandidateGeneratorConsExpand::CandidateGeneratorConsExpand( - QuantifiersEngine* qe, Node mpat) - : CandidateGeneratorQE(qe, mpat) +CandidateGeneratorConsExpand::CandidateGeneratorConsExpand(QuantifiersState& qs, + TermRegistry& tr, + Node mpat) + : CandidateGeneratorQE(qs, tr, mpat) { Assert(mpat.getKind() == APPLY_CONSTRUCTOR); d_mpat_type = mpat.getType(); @@ -268,9 +281,10 @@ bool CandidateGeneratorConsExpand::isLegalOpCandidate(Node n) return isLegalCandidate(n); } -CandidateGeneratorSelector::CandidateGeneratorSelector(QuantifiersEngine* qe, +CandidateGeneratorSelector::CandidateGeneratorSelector(QuantifiersState& qs, + TermRegistry& tr, Node mpat) - : CandidateGeneratorQE(qe, mpat) + : CandidateGeneratorQE(qs, tr, mpat) { Trace("sel-trigger") << "Selector trigger: " << mpat << std::endl; Assert(mpat.getKind() == APPLY_SELECTOR); @@ -280,19 +294,19 @@ CandidateGeneratorSelector::CandidateGeneratorSelector(QuantifiersEngine* qe, { Assert(mpatExp[1].getKind() == APPLY_SELECTOR_TOTAL); Assert(mpatExp[2].getKind() == APPLY_UF); - d_selOp = qe->getTermDatabase()->getMatchOperator(mpatExp[1]); - d_ufOp = qe->getTermDatabase()->getMatchOperator(mpatExp[2]); + d_selOp = d_treg.getTermDatabase()->getMatchOperator(mpatExp[1]); + d_ufOp = d_treg.getTermDatabase()->getMatchOperator(mpatExp[2]); } else if (mpatExp.getKind() == APPLY_SELECTOR_TOTAL) { // corner case of datatype with one constructor - d_selOp = qe->getTermDatabase()->getMatchOperator(mpatExp); + d_selOp = d_treg.getTermDatabase()->getMatchOperator(mpatExp); } else { // corner case of a wrongly applied selector as a trigger Assert(mpatExp.getKind() == APPLY_UF); - d_ufOp = qe->getTermDatabase()->getMatchOperator(mpatExp); + d_ufOp = d_treg.getTermDatabase()->getMatchOperator(mpatExp); } Assert(d_selOp != d_ufOp); } @@ -332,5 +346,6 @@ Node CandidateGeneratorSelector::getNextCandidate() } } // namespace inst +} // namespace quantifiers } // namespace theory } // namespace CVC4 diff --git a/src/theory/quantifiers/ematching/candidate_generator.h b/src/theory/quantifiers/ematching/candidate_generator.h index e0d25eb64..45eec1d4c 100644 --- a/src/theory/quantifiers/ematching/candidate_generator.h +++ b/src/theory/quantifiers/ematching/candidate_generator.h @@ -22,8 +22,10 @@ namespace CVC4 { namespace theory { +namespace quantifiers { -class QuantifiersEngine; +class QuantifiersState; +class TermRegistry; namespace inst { @@ -51,10 +53,8 @@ namespace inst { * */ class CandidateGenerator { -protected: - QuantifiersEngine* d_qe; -public: - CandidateGenerator( QuantifiersEngine* qe ) : d_qe( qe ){} + public: + CandidateGenerator(QuantifiersState& qs, TermRegistry& tr); virtual ~CandidateGenerator(){} /** reset instantiation round * @@ -70,10 +70,15 @@ public: virtual void reset( Node eqc ) = 0; /** get the next candidate */ virtual Node getNextCandidate() = 0; -public: - /** is n a legal candidate? */ - bool isLegalCandidate(Node n); -};/* class CandidateGenerator */ + /** is n a legal candidate? */ + bool isLegalCandidate(Node n); + + protected: + /** Reference to the quantifiers state */ + QuantifiersState& d_qs; + /** Reference to the term registry */ + TermRegistry& d_treg; +}; /* the default candidate generator class * @@ -88,7 +93,7 @@ class CandidateGeneratorQE : public CandidateGenerator friend class CandidateGeneratorQEDisequal; public: - CandidateGeneratorQE(QuantifiersEngine* qe, Node pat); + CandidateGeneratorQE(QuantifiersState& qs, TermRegistry& tr, Node pat); /** reset */ void reset(Node eqc) override; /** get next candidate */ @@ -142,7 +147,7 @@ class CandidateGeneratorQELitDeq : public CandidateGenerator * mpat is an equality that we are matching to equalities in the equivalence * class of false */ - CandidateGeneratorQELitDeq(QuantifiersEngine* qe, Node mpat); + CandidateGeneratorQELitDeq(QuantifiersState& qs, TermRegistry& tr, Node mpat); /** reset */ void reset(Node eqc) override; /** get next candidate */ @@ -178,7 +183,7 @@ class CandidateGeneratorQEAll : public CandidateGenerator bool d_firstTime; public: - CandidateGeneratorQEAll( QuantifiersEngine* qe, Node mpat ); + CandidateGeneratorQEAll(QuantifiersState& qs, TermRegistry& tr, Node mpat); /** reset */ void reset(Node eqc) override; /** get next candidate */ @@ -196,7 +201,9 @@ class CandidateGeneratorQEAll : public CandidateGenerator class CandidateGeneratorConsExpand : public CandidateGeneratorQE { public: - CandidateGeneratorConsExpand(QuantifiersEngine* qe, Node mpat); + CandidateGeneratorConsExpand(QuantifiersState& qs, + TermRegistry& tr, + Node mpat); /** reset */ void reset(Node eqc) override; /** get next candidate */ @@ -216,7 +223,7 @@ class CandidateGeneratorConsExpand : public CandidateGeneratorQE class CandidateGeneratorSelector : public CandidateGeneratorQE { public: - CandidateGeneratorSelector(QuantifiersEngine* qe, Node mpat); + CandidateGeneratorSelector(QuantifiersState& qs, TermRegistry& tr, Node mpat); /** reset */ void reset(Node eqc) override; /** @@ -234,6 +241,7 @@ class CandidateGeneratorSelector : public CandidateGeneratorQE }; }/* CVC4::theory::inst namespace */ +} // namespace quantifiers }/* CVC4::theory namespace */ }/* CVC4 namespace */ diff --git a/src/theory/quantifiers/ematching/ho_trigger.cpp b/src/theory/quantifiers/ematching/ho_trigger.cpp index 17cbba7ea..6206b24a7 100644 --- a/src/theory/quantifiers/ematching/ho_trigger.cpp +++ b/src/theory/quantifiers/ematching/ho_trigger.cpp @@ -29,17 +29,19 @@ using namespace CVC4::kind; namespace CVC4 { namespace theory { +namespace quantifiers { namespace inst { HigherOrderTrigger::HigherOrderTrigger( QuantifiersEngine* qe, - quantifiers::QuantifiersState& qs, - quantifiers::QuantifiersInferenceManager& qim, - quantifiers::QuantifiersRegistry& qr, + QuantifiersState& qs, + QuantifiersInferenceManager& qim, + QuantifiersRegistry& qr, + TermRegistry& tr, Node q, std::vector& nodes, std::map >& ho_apps) - : Trigger(qe, qs, qim, qr, q, nodes), d_ho_var_apps(ho_apps) + : Trigger(qe, qs, qim, qr, tr, q, nodes), d_ho_var_apps(ho_apps) { NodeManager* nm = NodeManager::currentNM(); // process the higher-order variable applications @@ -166,7 +168,7 @@ void HigherOrderTrigger::collectHoVarApplyTerms( { if (op.getKind() == kind::INST_CONSTANT) { - Assert(quantifiers::TermUtil::getInstConstAttr(ret) == q); + Assert(TermUtil::getInstConstAttr(ret) == q); Trace("ho-quant-trigger-debug") << "Ho variable apply term : " << ret << " with head " << op << std::endl; @@ -234,7 +236,7 @@ bool HigherOrderTrigger::sendInstantiation(std::vector& m, InferenceId id) d_lchildren.clear(); d_arg_to_arg_rep.clear(); d_arg_vector.clear(); - quantifiers::QuantifiersState& qs = d_quantEngine->getState(); + QuantifiersState& qs = d_quantEngine->getState(); for (std::pair >& ha : ho_var_apps_subs) { TNode var = ha.first; @@ -474,7 +476,7 @@ uint64_t HigherOrderTrigger::addHoTypeMatchPredicateLemmas() Trace("ho-quant-trigger") << "addHoTypeMatchPredicateLemmas..." << std::endl; uint64_t numLemmas = 0; // this forces expansion of APPLY_UF terms to curried HO_APPLY chains - quantifiers::TermDb* tdb = d_quantEngine->getTermDatabase(); + TermDb* tdb = d_quantEngine->getTermDatabase(); unsigned size = tdb->getNumOperators(); NodeManager* nm = NodeManager::currentNM(); for (unsigned j = 0; j < size; j++) @@ -522,6 +524,7 @@ uint64_t HigherOrderTrigger::addHoTypeMatchPredicateLemmas() return numLemmas; } -} /* CVC4::theory::inst namespace */ -} /* CVC4::theory namespace */ -} /* CVC4 namespace */ +} // namespace inst +} // namespace quantifiers +} // namespace theory +} // namespace CVC4 diff --git a/src/theory/quantifiers/ematching/ho_trigger.h b/src/theory/quantifiers/ematching/ho_trigger.h index fcb3cbfee..87c7adeec 100644 --- a/src/theory/quantifiers/ematching/ho_trigger.h +++ b/src/theory/quantifiers/ematching/ho_trigger.h @@ -27,6 +27,7 @@ namespace CVC4 { namespace theory { +namespace quantifiers { namespace inst { class Trigger; @@ -93,9 +94,10 @@ class HigherOrderTrigger : public Trigger private: HigherOrderTrigger(QuantifiersEngine* qe, - quantifiers::QuantifiersState& qs, - quantifiers::QuantifiersInferenceManager& qim, - quantifiers::QuantifiersRegistry& qr, + QuantifiersState& qs, + QuantifiersInferenceManager& qim, + QuantifiersRegistry& qr, + TermRegistry& tr, Node q, std::vector& nodes, std::map >& ho_apps); @@ -274,8 +276,9 @@ class HigherOrderTrigger : public Trigger bool arg_changed); }; -} /* CVC4::theory::inst namespace */ -} /* CVC4::theory namespace */ -} /* CVC4 namespace */ +} // namespace inst +} // namespace quantifiers +} // namespace theory +} // namespace CVC4 #endif /* CVC4__THEORY__QUANTIFIERS__HO_TRIGGER_H */ diff --git a/src/theory/quantifiers/ematching/im_generator.cpp b/src/theory/quantifiers/ematching/im_generator.cpp index 829ccc8b1..48c07ba4d 100644 --- a/src/theory/quantifiers/ematching/im_generator.cpp +++ b/src/theory/quantifiers/ematching/im_generator.cpp @@ -20,10 +20,11 @@ using namespace CVC4::kind; namespace CVC4 { namespace theory { +namespace quantifiers { namespace inst { IMGenerator::IMGenerator(Trigger* tparent) - : d_tparent(tparent), d_qstate(tparent->d_qstate) + : d_tparent(tparent), d_qstate(tparent->d_qstate), d_treg(tparent->d_treg) { } @@ -37,7 +38,7 @@ QuantifiersEngine* IMGenerator::getQuantifiersEngine() return d_tparent->d_quantEngine; } - -}/* CVC4::theory::inst namespace */ -}/* CVC4::theory namespace */ -}/* CVC4 namespace */ +} // namespace inst +} // namespace quantifiers +} // namespace theory +} // namespace CVC4 diff --git a/src/theory/quantifiers/ematching/im_generator.h b/src/theory/quantifiers/ematching/im_generator.h index 6bf472cb5..0d0f9498d 100644 --- a/src/theory/quantifiers/ematching/im_generator.h +++ b/src/theory/quantifiers/ematching/im_generator.h @@ -29,7 +29,7 @@ class QuantifiersEngine; namespace quantifiers { class QuantifiersState; -} // namespace quantifiers +class TermRegistry; namespace inst { @@ -110,12 +110,15 @@ protected: bool sendInstantiation(InstMatch& m, InferenceId id); /** The parent trigger that owns this */ Trigger* d_tparent; - /** The state of the quantifiers engine */ - quantifiers::QuantifiersState& d_qstate; + /** Reference to the state of the quantifiers engine */ + QuantifiersState& d_qstate; + /** Reference to the term registry */ + TermRegistry& d_treg; // !!!!!!!!! temporarily available (project #15) QuantifiersEngine* getQuantifiersEngine(); };/* class IMGenerator */ +} // namespace inst } } } diff --git a/src/theory/quantifiers/ematching/inst_match_generator.cpp b/src/theory/quantifiers/ematching/inst_match_generator.cpp index 5f47f70c3..ac3e1b9be 100644 --- a/src/theory/quantifiers/ematching/inst_match_generator.cpp +++ b/src/theory/quantifiers/ematching/inst_match_generator.cpp @@ -33,6 +33,7 @@ using namespace CVC4::kind; namespace CVC4 { namespace theory { +namespace quantifiers { namespace inst { InstMatchGenerator::InstMatchGenerator(Trigger* tparent, Node pat) @@ -200,13 +201,13 @@ void InstMatchGenerator::initialize(Node q, } } - QuantifiersEngine* qe = getQuantifiersEngine(); // create candidate generator if (mpk == APPLY_SELECTOR) { // candidates for apply selector are a union of correctly and incorrectly // applied selectors - d_cg = new inst::CandidateGeneratorSelector(qe, d_match_pattern); + d_cg = + new inst::CandidateGeneratorSelector(d_qstate, d_treg, d_match_pattern); } else if (TriggerTermInfo::isAtomicTriggerKind(mpk)) { @@ -217,12 +218,14 @@ void InstMatchGenerator::initialize(Node q, const DType& dt = d_match_pattern.getType().getDType(); if (dt.getNumConstructors() == 1) { - d_cg = new inst::CandidateGeneratorConsExpand(qe, d_match_pattern); + d_cg = new inst::CandidateGeneratorConsExpand( + d_qstate, d_treg, d_match_pattern); } } if (d_cg == nullptr) { - CandidateGeneratorQE* cg = new CandidateGeneratorQE(qe, d_match_pattern); + CandidateGeneratorQE* cg = + new CandidateGeneratorQE(d_qstate, d_treg, d_match_pattern); // we will be scanning lists trying to find ground terms whose operator // is the same as d_match_operator's. d_cg = cg; @@ -247,9 +250,9 @@ void InstMatchGenerator::initialize(Node q, Trace("inst-match-gen") << "Purify dt trigger " << d_pattern << ", will match terms of op " << cOp << std::endl; - d_cg = new inst::CandidateGeneratorQE(qe, cOp); + d_cg = new inst::CandidateGeneratorQE(d_qstate, d_treg, cOp); }else{ - d_cg = new CandidateGeneratorQEAll(qe, d_match_pattern); + d_cg = new CandidateGeneratorQEAll(d_qstate, d_treg, d_match_pattern); } } else if (mpk == EQUAL) @@ -258,7 +261,8 @@ void InstMatchGenerator::initialize(Node q, if (d_pattern.getKind() == NOT) { // candidates will be all disequalities - d_cg = new inst::CandidateGeneratorQELitDeq(qe, d_match_pattern); + d_cg = new inst::CandidateGeneratorQELitDeq( + d_qstate, d_treg, d_match_pattern); } } else @@ -666,6 +670,7 @@ InstMatchGenerator* InstMatchGenerator::getInstMatchGenerator(Trigger* tparent, return new InstMatchGenerator(tparent, n); } -}/* CVC4::theory::inst namespace */ -}/* CVC4::theory namespace */ -}/* CVC4 namespace */ +} // namespace inst +} // namespace quantifiers +} // namespace theory +} // namespace CVC4 diff --git a/src/theory/quantifiers/ematching/inst_match_generator.h b/src/theory/quantifiers/ematching/inst_match_generator.h index 3f6976ca7..375fe73e1 100644 --- a/src/theory/quantifiers/ematching/inst_match_generator.h +++ b/src/theory/quantifiers/ematching/inst_match_generator.h @@ -24,6 +24,7 @@ namespace CVC4 { namespace theory { +namespace quantifiers { namespace inst { class CandidateGenerator; @@ -321,6 +322,7 @@ class InstMatchGenerator : public IMGenerator { Node n); };/* class InstMatchGenerator */ +} // namespace inst } } } diff --git a/src/theory/quantifiers/ematching/inst_match_generator_multi.cpp b/src/theory/quantifiers/ematching/inst_match_generator_multi.cpp index 2920be1a2..c4d5272a4 100644 --- a/src/theory/quantifiers/ematching/inst_match_generator_multi.cpp +++ b/src/theory/quantifiers/ematching/inst_match_generator_multi.cpp @@ -23,6 +23,7 @@ using namespace CVC4::kind; namespace CVC4 { namespace theory { +namespace quantifiers { namespace inst { InstMatchGeneratorMulti::InstMatchGeneratorMulti(Trigger* tparent, @@ -35,8 +36,7 @@ InstMatchGeneratorMulti::InstMatchGeneratorMulti(Trigger* tparent, std::map > var_contains; for (const Node& pat : pats) { - quantifiers::TermUtil::computeInstConstContainsForQuant( - q, pat, var_contains[pat]); + TermUtil::computeInstConstContainsForQuant(q, pat, var_contains[pat]); } // convert to indicies for (std::pair >& vc : var_contains) @@ -269,7 +269,7 @@ void InstMatchGeneratorMulti::processNewInstantiations(InstMatch& m, { return; } - quantifiers::QuantifiersState& qs = d_qstate; + QuantifiersState& qs = d_qstate; // check modulo equality for other possible instantiations if (!qs.hasTerm(n)) { @@ -314,5 +314,6 @@ void InstMatchGeneratorMulti::processNewInstantiations(InstMatch& m, } } // namespace inst +} // namespace quantifiers } // namespace theory } // namespace CVC4 diff --git a/src/theory/quantifiers/ematching/inst_match_generator_multi.h b/src/theory/quantifiers/ematching/inst_match_generator_multi.h index 85cbff7f0..1e25baea4 100644 --- a/src/theory/quantifiers/ematching/inst_match_generator_multi.h +++ b/src/theory/quantifiers/ematching/inst_match_generator_multi.h @@ -25,6 +25,7 @@ namespace CVC4 { namespace theory { +namespace quantifiers { namespace inst { /** InstMatchGeneratorMulti @@ -100,6 +101,7 @@ class InstMatchGeneratorMulti : public IMGenerator }; } // namespace inst +} // namespace quantifiers } // namespace theory } // namespace CVC4 diff --git a/src/theory/quantifiers/ematching/inst_match_generator_multi_linear.cpp b/src/theory/quantifiers/ematching/inst_match_generator_multi_linear.cpp index ac7bb5f3c..e8c08ef1e 100644 --- a/src/theory/quantifiers/ematching/inst_match_generator_multi_linear.cpp +++ b/src/theory/quantifiers/ematching/inst_match_generator_multi_linear.cpp @@ -22,6 +22,7 @@ using namespace CVC4::kind; namespace CVC4 { namespace theory { +namespace quantifiers { namespace inst { InstMatchGeneratorMultiLinear::InstMatchGeneratorMultiLinear( @@ -32,8 +33,7 @@ InstMatchGeneratorMultiLinear::InstMatchGeneratorMultiLinear( std::map > var_contains; for (const Node& pat : pats) { - quantifiers::TermUtil::computeInstConstContainsForQuant( - q, pat, var_contains[pat]); + TermUtil::computeInstConstContainsForQuant(q, pat, var_contains[pat]); } std::map > var_to_node; for (std::pair >& vc : var_contains) @@ -174,5 +174,6 @@ int InstMatchGeneratorMultiLinear::getNextMatch(Node q, InstMatch& m) } } // namespace inst +} // namespace quantifiers } // namespace theory } // namespace CVC4 diff --git a/src/theory/quantifiers/ematching/inst_match_generator_multi_linear.h b/src/theory/quantifiers/ematching/inst_match_generator_multi_linear.h index ce1e79229..b46960400 100644 --- a/src/theory/quantifiers/ematching/inst_match_generator_multi_linear.h +++ b/src/theory/quantifiers/ematching/inst_match_generator_multi_linear.h @@ -24,6 +24,7 @@ namespace CVC4 { namespace theory { +namespace quantifiers { namespace inst { /** InstMatchGeneratorMultiLinear class @@ -82,6 +83,7 @@ class InstMatchGeneratorMultiLinear : public InstMatchGenerator }; } // namespace inst +} // namespace quantifiers } // namespace theory } // namespace CVC4 diff --git a/src/theory/quantifiers/ematching/inst_match_generator_simple.cpp b/src/theory/quantifiers/ematching/inst_match_generator_simple.cpp index eaf917545..c7360d02f 100644 --- a/src/theory/quantifiers/ematching/inst_match_generator_simple.cpp +++ b/src/theory/quantifiers/ematching/inst_match_generator_simple.cpp @@ -26,6 +26,7 @@ using namespace CVC4::kind; namespace CVC4 { namespace theory { +namespace quantifiers { namespace inst { InstMatchGeneratorSimple::InstMatchGeneratorSimple(Trigger* tparent, @@ -46,7 +47,7 @@ InstMatchGeneratorSimple::InstMatchGeneratorSimple(Trigger* tparent, { d_eqc = d_match_pattern[1]; d_match_pattern = d_match_pattern[0]; - Assert(!quantifiers::TermUtil::hasInstConstAttr(d_eqc)); + Assert(!TermUtil::hasInstConstAttr(d_eqc)); } Assert(TriggerTermInfo::isSimpleTrigger(d_match_pattern)); for (size_t i = 0, nchild = d_match_pattern.getNumChildren(); i < nchild; i++) @@ -54,7 +55,7 @@ InstMatchGeneratorSimple::InstMatchGeneratorSimple(Trigger* tparent, if (d_match_pattern[i].getKind() == INST_CONSTANT) { if (!options::cegqi() - || quantifiers::TermUtil::getInstConstAttr(d_match_pattern[i]) == q) + || TermUtil::getInstConstAttr(d_match_pattern[i]) == q) { d_var_num[i] = d_match_pattern[i].getAttribute(InstVarNumAttribute()); } @@ -65,7 +66,7 @@ InstMatchGeneratorSimple::InstMatchGeneratorSimple(Trigger* tparent, } d_match_pattern_arg_types.push_back(d_match_pattern[i].getType()); } - quantifiers::TermDb* tdb = getQuantifiersEngine()->getTermDatabase(); + TermDb* tdb = getQuantifiersEngine()->getTermDatabase(); d_op = tdb->getMatchOperator(d_match_pattern); } @@ -74,7 +75,7 @@ uint64_t InstMatchGeneratorSimple::addInstantiations(Node q) { uint64_t addedLemmas = 0; TNodeTrie* tat; - quantifiers::TermDb* tdb = getQuantifiersEngine()->getTermDatabase(); + TermDb* tdb = getQuantifiersEngine()->getTermDatabase(); if (d_eqc.isNull()) { tat = tdb->getTermArgTrie(d_op); @@ -187,7 +188,7 @@ void InstMatchGeneratorSimple::addInstantiations(InstMatch& m, int InstMatchGeneratorSimple::getActiveScore() { - quantifiers::TermDb* tdb = getQuantifiersEngine()->getTermDatabase(); + TermDb* tdb = getQuantifiersEngine()->getTermDatabase(); Node f = tdb->getMatchOperator(d_match_pattern); size_t ngt = tdb->getNumGroundTerms(f); Trace("trigger-active-sel-debug") << "Number of ground terms for (simple) " @@ -196,5 +197,6 @@ int InstMatchGeneratorSimple::getActiveScore() } } // namespace inst +} // namespace quantifiers } // namespace theory } // namespace CVC4 diff --git a/src/theory/quantifiers/ematching/inst_match_generator_simple.h b/src/theory/quantifiers/ematching/inst_match_generator_simple.h index bfb4b6840..ad48d9c91 100644 --- a/src/theory/quantifiers/ematching/inst_match_generator_simple.h +++ b/src/theory/quantifiers/ematching/inst_match_generator_simple.h @@ -25,6 +25,7 @@ namespace CVC4 { namespace theory { +namespace quantifiers { namespace inst { /** InstMatchGeneratorSimple class @@ -101,6 +102,7 @@ class InstMatchGeneratorSimple : public IMGenerator }; } // namespace inst +} // namespace quantifiers } // namespace theory } // namespace CVC4 diff --git a/src/theory/quantifiers/ematching/inst_strategy.cpp b/src/theory/quantifiers/ematching/inst_strategy.cpp index 2ca7f7af0..083331948 100644 --- a/src/theory/quantifiers/ematching/inst_strategy.cpp +++ b/src/theory/quantifiers/ematching/inst_strategy.cpp @@ -23,8 +23,9 @@ namespace quantifiers { InstStrategy::InstStrategy(QuantifiersEngine* qe, QuantifiersState& qs, QuantifiersInferenceManager& qim, - QuantifiersRegistry& qr) - : d_quantEngine(qe), d_qstate(qs), d_qim(qim), d_qreg(qr) + QuantifiersRegistry& qr, + TermRegistry& tr) + : d_quantEngine(qe), d_qstate(qs), d_qim(qim), d_qreg(qr), d_treg(tr) { } InstStrategy::~InstStrategy() {} diff --git a/src/theory/quantifiers/ematching/inst_strategy.h b/src/theory/quantifiers/ematching/inst_strategy.h index 84b9c4b77..cbe6e341b 100644 --- a/src/theory/quantifiers/ematching/inst_strategy.h +++ b/src/theory/quantifiers/ematching/inst_strategy.h @@ -32,6 +32,7 @@ namespace quantifiers { class QuantifiersState; class QuantifiersInferenceManager; class QuantifiersRegistry; +class TermRegistry; /** A status response to process */ enum class InstStrategyStatus @@ -51,7 +52,8 @@ class InstStrategy InstStrategy(QuantifiersEngine* qe, QuantifiersState& qs, QuantifiersInferenceManager& qim, - QuantifiersRegistry& qr); + QuantifiersRegistry& qr, + TermRegistry& tr); virtual ~InstStrategy(); /** presolve */ virtual void presolve(); @@ -74,8 +76,10 @@ class InstStrategy QuantifiersState& d_qstate; /** The quantifiers inference manager object */ QuantifiersInferenceManager& d_qim; - /** The quantifiers registry */ + /** Reference to the quantifiers registry */ QuantifiersRegistry& d_qreg; + /** Reference to the term registry */ + TermRegistry& d_treg; }; /* class InstStrategy */ } // namespace quantifiers diff --git a/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp b/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp index 4470e5bf4..ba068230d 100644 --- a/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp +++ b/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp @@ -23,7 +23,7 @@ #include "util/random.h" using namespace CVC4::kind; -using namespace CVC4::theory::inst; +using namespace CVC4::theory::quantifiers::inst; namespace CVC4 { namespace theory { @@ -66,8 +66,9 @@ InstStrategyAutoGenTriggers::InstStrategyAutoGenTriggers( QuantifiersState& qs, QuantifiersInferenceManager& qim, QuantifiersRegistry& qr, + TermRegistry& tr, QuantRelevance* qrlv) - : InstStrategy(qe, qs, qim, qr), d_quant_rel(qrlv) + : InstStrategy(qe, qs, qim, qr, tr), d_quant_rel(qrlv) { //how to select trigger terms d_tr_strategy = options::triggerSelMode(); @@ -284,6 +285,7 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f ){ d_qstate, d_qim, d_qreg, + d_treg, f, patTerms[0], false, @@ -323,6 +325,7 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f ){ d_qstate, d_qim, d_qreg, + d_treg, f, patTerms, false, @@ -367,6 +370,7 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f ){ d_qstate, d_qim, d_qreg, + d_treg, f, patTerms[index], false, diff --git a/src/theory/quantifiers/ematching/inst_strategy_e_matching.h b/src/theory/quantifiers/ematching/inst_strategy_e_matching.h index e0999e984..f4c74c43a 100644 --- a/src/theory/quantifiers/ematching/inst_strategy_e_matching.h +++ b/src/theory/quantifiers/ematching/inst_strategy_e_matching.h @@ -89,6 +89,7 @@ class InstStrategyAutoGenTriggers : public InstStrategy QuantifiersState& qs, QuantifiersInferenceManager& qim, QuantifiersRegistry& qr, + TermRegistry& tr, QuantRelevance* qrlv); ~InstStrategyAutoGenTriggers() {} diff --git a/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.cpp b/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.cpp index c9e566b77..412676ad4 100644 --- a/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.cpp +++ b/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.cpp @@ -19,7 +19,7 @@ #include "theory/quantifiers_engine.h" using namespace CVC4::kind; -using namespace CVC4::theory::inst; +using namespace CVC4::theory::quantifiers::inst; namespace CVC4 { namespace theory { @@ -29,15 +29,16 @@ InstStrategyUserPatterns::InstStrategyUserPatterns( QuantifiersEngine* ie, QuantifiersState& qs, QuantifiersInferenceManager& qim, - QuantifiersRegistry& qr) - : InstStrategy(ie, qs, qim, qr) + QuantifiersRegistry& qr, + TermRegistry& tr) + : InstStrategy(ie, qs, qim, qr, tr) { } InstStrategyUserPatterns::~InstStrategyUserPatterns() {} size_t InstStrategyUserPatterns::getNumUserGenerators(Node q) const { - std::map >::const_iterator it = + std::map >::const_iterator it = d_user_gen.find(q); if (it == d_user_gen.end()) { @@ -46,10 +47,9 @@ size_t InstStrategyUserPatterns::getNumUserGenerators(Node q) const return it->second.size(); } -inst::Trigger* InstStrategyUserPatterns::getUserGenerator(Node q, - size_t i) const +Trigger* InstStrategyUserPatterns::getUserGenerator(Node q, size_t i) const { - std::map >::const_iterator it = + std::map >::const_iterator it = d_user_gen.find(q); if (it == d_user_gen.end()) { @@ -111,6 +111,7 @@ InstStrategyStatus InstStrategyUserPatterns::process(Node q, d_qstate, d_qim, d_qreg, + d_treg, q, ugw[i], true, @@ -123,7 +124,7 @@ InstStrategyStatus InstStrategyUserPatterns::process(Node q, ugw.clear(); } - std::vector& ug = d_user_gen[q]; + std::vector& ug = d_user_gen[q]; for (Trigger* t : ug) { if (Trace.isOn("process-trigger")) @@ -171,6 +172,7 @@ void InstStrategyUserPatterns::addUserPattern(Node q, Node pat) d_qstate, d_qim, d_qreg, + d_treg, q, nodes, true, diff --git a/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.h b/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.h index 4da092f70..e63154a60 100644 --- a/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.h +++ b/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.h @@ -37,7 +37,8 @@ class InstStrategyUserPatterns : public InstStrategy InstStrategyUserPatterns(QuantifiersEngine* qe, QuantifiersState& qs, QuantifiersInferenceManager& qim, - QuantifiersRegistry& qr); + QuantifiersRegistry& qr, + TermRegistry& tr); ~InstStrategyUserPatterns(); /** add pattern */ void addUserPattern(Node q, Node pat); diff --git a/src/theory/quantifiers/ematching/instantiation_engine.cpp b/src/theory/quantifiers/ematching/instantiation_engine.cpp index 619c8b9bb..1c301141c 100644 --- a/src/theory/quantifiers/ematching/instantiation_engine.cpp +++ b/src/theory/quantifiers/ematching/instantiation_engine.cpp @@ -24,10 +24,9 @@ #include "theory/quantifiers/term_util.h" #include "theory/quantifiers_engine.h" -using namespace std; using namespace CVC4::kind; using namespace CVC4::context; -using namespace CVC4::theory::inst; +using namespace CVC4::theory::quantifiers::inst; namespace CVC4 { namespace theory { @@ -36,7 +35,8 @@ namespace quantifiers { InstantiationEngine::InstantiationEngine(QuantifiersEngine* qe, QuantifiersState& qs, QuantifiersInferenceManager& qim, - QuantifiersRegistry& qr) + QuantifiersRegistry& qr, + TermRegistry& tr) : QuantifiersModule(qs, qim, qr, qe), d_instStrategies(), d_isup(), @@ -53,13 +53,14 @@ InstantiationEngine::InstantiationEngine(QuantifiersEngine* qe, // user-provided patterns if (options::userPatternsQuant() != options::UserPatMode::IGNORE) { - d_isup.reset(new InstStrategyUserPatterns(d_quantEngine, qs, qim, qr)); + d_isup.reset( + new InstStrategyUserPatterns(d_quantEngine, qs, qim, qr, tr)); d_instStrategies.push_back(d_isup.get()); } // auto-generated patterns d_i_ag.reset(new InstStrategyAutoGenTriggers( - d_quantEngine, qs, qim, qr, d_quant_rel.get())); + d_quantEngine, qs, qim, qr, tr, d_quant_rel.get())); d_instStrategies.push_back(d_i_ag.get()); } } diff --git a/src/theory/quantifiers/ematching/instantiation_engine.h b/src/theory/quantifiers/ematching/instantiation_engine.h index b327fb4a6..4042e3424 100644 --- a/src/theory/quantifiers/ematching/instantiation_engine.h +++ b/src/theory/quantifiers/ematching/instantiation_engine.h @@ -51,7 +51,8 @@ class InstantiationEngine : public QuantifiersModule { InstantiationEngine(QuantifiersEngine* qe, QuantifiersState& qs, QuantifiersInferenceManager& qim, - QuantifiersRegistry& qr); + QuantifiersRegistry& qr, + TermRegistry& tr); ~InstantiationEngine(); void presolve() override; bool needsCheck(Theory::Effort e) override; diff --git a/src/theory/quantifiers/ematching/pattern_term_selector.cpp b/src/theory/quantifiers/ematching/pattern_term_selector.cpp index bdf5499fa..7ab54fcfe 100644 --- a/src/theory/quantifiers/ematching/pattern_term_selector.cpp +++ b/src/theory/quantifiers/ematching/pattern_term_selector.cpp @@ -24,6 +24,7 @@ using namespace CVC4::kind; namespace CVC4 { namespace theory { +namespace quantifiers { namespace inst { PatternTermSelector::PatternTermSelector(Node q, @@ -726,5 +727,6 @@ void PatternTermSelector::getTriggerVariables(Node n, } } // namespace inst +} // namespace quantifiers } // namespace theory } // namespace CVC4 diff --git a/src/theory/quantifiers/ematching/pattern_term_selector.h b/src/theory/quantifiers/ematching/pattern_term_selector.h index a05600095..9cbf4cf5e 100644 --- a/src/theory/quantifiers/ematching/pattern_term_selector.h +++ b/src/theory/quantifiers/ematching/pattern_term_selector.h @@ -25,6 +25,7 @@ namespace CVC4 { namespace theory { +namespace quantifiers { namespace inst { /** @@ -189,6 +190,7 @@ class PatternTermSelector }; } // namespace inst +} // namespace quantifiers } // namespace theory } // namespace CVC4 diff --git a/src/theory/quantifiers/ematching/trigger.cpp b/src/theory/quantifiers/ematching/trigger.cpp index 3940370cf..af0a0bfbc 100644 --- a/src/theory/quantifiers/ematching/trigger.cpp +++ b/src/theory/quantifiers/ematching/trigger.cpp @@ -38,16 +38,23 @@ using namespace CVC4::kind; namespace CVC4 { namespace theory { +namespace quantifiers { namespace inst { /** trigger class constructor */ Trigger::Trigger(QuantifiersEngine* qe, - quantifiers::QuantifiersState& qs, - quantifiers::QuantifiersInferenceManager& qim, - quantifiers::QuantifiersRegistry& qr, + QuantifiersState& qs, + QuantifiersInferenceManager& qim, + QuantifiersRegistry& qr, + TermRegistry& tr, Node q, std::vector& nodes) - : d_quantEngine(qe), d_qstate(qs), d_qim(qim), d_qreg(qr), d_quant(q) + : d_quantEngine(qe), + d_qstate(qs), + d_qim(qim), + d_qreg(qr), + d_treg(tr), + d_quant(q) { // We must ensure that the ground subterms of the trigger have been // preprocessed. @@ -59,7 +66,7 @@ Trigger::Trigger(QuantifiersEngine* qe, } if (Trace.isOn("trigger")) { - quantifiers::QuantAttributes& qa = d_qreg.getQuantAttributes(); + QuantAttributes& qa = d_qreg.getQuantAttributes(); Trace("trigger") << "Trigger for " << qa.quantToString(q) << ": " << std::endl; for (const Node& n : d_nodes) @@ -169,8 +176,7 @@ bool Trigger::mkTriggerTerms(Node q, std::map< Node, std::vector< Node > > varContains; for (const Node& pat : temp) { - quantifiers::TermUtil::computeInstConstContainsForQuant( - q, pat, varContains[pat]); + TermUtil::computeInstConstContainsForQuant(q, pat, varContains[pat]); } for (const Node& t : temp) { @@ -178,7 +184,7 @@ bool Trigger::mkTriggerTerms(Node q, bool foundVar = false; for (const Node& v : vct) { - Assert(quantifiers::TermUtil::getInstConstAttr(v) == q); + Assert(TermUtil::getInstConstAttr(v) == q); if( vars.find( v )==vars.end() ){ varCount++; vars[ v ] = true; @@ -242,9 +248,10 @@ bool Trigger::mkTriggerTerms(Node q, } Trigger* Trigger::mkTrigger(QuantifiersEngine* qe, - quantifiers::QuantifiersState& qs, - quantifiers::QuantifiersInferenceManager& qim, - quantifiers::QuantifiersRegistry& qr, + QuantifiersState& qs, + QuantifiersInferenceManager& qim, + QuantifiersRegistry& qr, + TermRegistry& tr, Node f, std::vector& nodes, bool keepAll, @@ -285,11 +292,11 @@ Trigger* Trigger::mkTrigger(QuantifiersEngine* qe, Trigger* t; if (!ho_apps.empty()) { - t = new HigherOrderTrigger(qe, qs, qim, qr, f, trNodes, ho_apps); + t = new HigherOrderTrigger(qe, qs, qim, qr, tr, f, trNodes, ho_apps); } else { - t = new Trigger(qe, qs, qim, qr, f, trNodes); + t = new Trigger(qe, qs, qim, qr, tr, f, trNodes); } qe->getTriggerDatabase()->addTrigger( trNodes, t ); @@ -297,9 +304,10 @@ Trigger* Trigger::mkTrigger(QuantifiersEngine* qe, } Trigger* Trigger::mkTrigger(QuantifiersEngine* qe, - quantifiers::QuantifiersState& qs, - quantifiers::QuantifiersInferenceManager& qim, - quantifiers::QuantifiersRegistry& qr, + QuantifiersState& qs, + QuantifiersInferenceManager& qim, + QuantifiersRegistry& qr, + TermRegistry& tr, Node f, Node n, bool keepAll, @@ -308,7 +316,7 @@ Trigger* Trigger::mkTrigger(QuantifiersEngine* qe, { std::vector< Node > nodes; nodes.push_back( n ); - return mkTrigger(qe, qs, qim, qr, f, nodes, keepAll, trOption, useNVars); + return mkTrigger(qe, qs, qim, qr, tr, f, nodes, keepAll, trOption, useNVars); } int Trigger::getActiveScore() { return d_mg->getActiveScore(); } @@ -334,7 +342,7 @@ Node Trigger::ensureGroundTermPreprocessed(Valuation& val, { visited[cur] = cur; } - else if (!quantifiers::TermUtil::hasInstConstAttr(cur)) + else if (!TermUtil::hasInstConstAttr(cur)) { // cur has no INST_CONSTANT, thus is ground. Node vcur = val.getPreprocessedTerm(cur); @@ -382,6 +390,7 @@ void Trigger::debugPrint(const char* c) const Trace(c) << "TRIGGER( " << d_nodes << " )" << std::endl; } -}/* CVC4::theory::inst namespace */ -}/* CVC4::theory namespace */ -}/* CVC4 namespace */ +} // namespace inst +} // namespace quantifiers +} // namespace theory +} // namespace CVC4 diff --git a/src/theory/quantifiers/ematching/trigger.h b/src/theory/quantifiers/ematching/trigger.h index b5a271fae..3c218ca7b 100644 --- a/src/theory/quantifiers/ematching/trigger.h +++ b/src/theory/quantifiers/ematching/trigger.h @@ -30,12 +30,12 @@ namespace quantifiers { class QuantifiersState; class QuantifiersInferenceManager; class QuantifiersRegistry; -} +class TermRegistry; +class InstMatch; namespace inst { class IMGenerator; -class InstMatch; class InstMatchGenerator; /** A collection of nodes representing a trigger. * @@ -162,9 +162,10 @@ class Trigger { TR_RETURN_NULL //return null if a duplicate is found }; static Trigger* mkTrigger(QuantifiersEngine* qe, - quantifiers::QuantifiersState& qs, - quantifiers::QuantifiersInferenceManager& qim, - quantifiers::QuantifiersRegistry& qr, + QuantifiersState& qs, + QuantifiersInferenceManager& qim, + QuantifiersRegistry& qr, + TermRegistry& tr, Node q, std::vector& nodes, bool keepAll = true, @@ -172,9 +173,10 @@ class Trigger { size_t useNVars = 0); /** single trigger version that calls the above function */ static Trigger* mkTrigger(QuantifiersEngine* qe, - quantifiers::QuantifiersState& qs, - quantifiers::QuantifiersInferenceManager& qim, - quantifiers::QuantifiersRegistry& qr, + QuantifiersState& qs, + QuantifiersInferenceManager& qim, + QuantifiersRegistry& qr, + TermRegistry& tr, Node q, Node n, bool keepAll = true, @@ -197,9 +199,10 @@ class Trigger { protected: /** trigger constructor, intentionally protected (use Trigger::mkTrigger). */ Trigger(QuantifiersEngine* ie, - quantifiers::QuantifiersState& qs, - quantifiers::QuantifiersInferenceManager& qim, - quantifiers::QuantifiersRegistry& qr, + QuantifiersState& qs, + QuantifiersInferenceManager& qim, + QuantifiersRegistry& qr, + TermRegistry& tr, Node q, std::vector& nodes); /** add an instantiation (called by InstMatchGenerator) @@ -250,11 +253,13 @@ class Trigger { // !!!!!!!!!!!!!!!!!! temporarily available (project #15) QuantifiersEngine* d_quantEngine; /** Reference to the quantifiers state */ - quantifiers::QuantifiersState& d_qstate; + QuantifiersState& d_qstate; /** Reference to the quantifiers inference manager */ - quantifiers::QuantifiersInferenceManager& d_qim; + QuantifiersInferenceManager& d_qim; /** The quantifiers registry */ - quantifiers::QuantifiersRegistry& d_qreg; + QuantifiersRegistry& d_qreg; + /** Reference to the term registry */ + TermRegistry& d_treg; /** The quantified formula this trigger is for. */ Node d_quant; /** match generator @@ -265,8 +270,9 @@ class Trigger { IMGenerator* d_mg; }; /* class Trigger */ -}/* CVC4::theory::inst namespace */ -}/* CVC4::theory namespace */ -}/* CVC4 namespace */ +} // namespace inst +} // namespace quantifiers +} // namespace theory +} // namespace CVC4 #endif /* CVC4__THEORY__QUANTIFIERS__TRIGGER_H */ diff --git a/src/theory/quantifiers/ematching/trigger_term_info.cpp b/src/theory/quantifiers/ematching/trigger_term_info.cpp index c0aa6bcac..4bc74dd96 100644 --- a/src/theory/quantifiers/ematching/trigger_term_info.cpp +++ b/src/theory/quantifiers/ematching/trigger_term_info.cpp @@ -20,6 +20,7 @@ using namespace CVC4::kind; namespace CVC4 { namespace theory { +namespace quantifiers { namespace inst { void TriggerTermInfo::init(Node q, Node n, int reqPol, Node reqPolEq) @@ -111,5 +112,6 @@ int32_t TriggerTermInfo::getTriggerWeight(Node n) } } // namespace inst +} // namespace quantifiers } // namespace theory } // namespace CVC4 diff --git a/src/theory/quantifiers/ematching/trigger_term_info.h b/src/theory/quantifiers/ematching/trigger_term_info.h index bb829b432..5bf7e8099 100644 --- a/src/theory/quantifiers/ematching/trigger_term_info.h +++ b/src/theory/quantifiers/ematching/trigger_term_info.h @@ -23,6 +23,7 @@ namespace CVC4 { namespace theory { +namespace quantifiers { namespace inst { /** Information about a node used in a trigger. @@ -121,6 +122,7 @@ class TriggerTermInfo }; } // namespace inst +} // namespace quantifiers } // namespace theory } // namespace CVC4 diff --git a/src/theory/quantifiers/ematching/trigger_trie.cpp b/src/theory/quantifiers/ematching/trigger_trie.cpp index 2ed2f4fb6..04e9dabb0 100644 --- a/src/theory/quantifiers/ematching/trigger_trie.cpp +++ b/src/theory/quantifiers/ematching/trigger_trie.cpp @@ -16,6 +16,7 @@ namespace CVC4 { namespace theory { +namespace quantifiers { namespace inst { TriggerTrie::TriggerTrie() {} @@ -71,5 +72,6 @@ void TriggerTrie::addTrigger(std::vector& nodes, inst::Trigger* t) } } // namespace inst +} // namespace quantifiers } // namespace theory } // namespace CVC4 diff --git a/src/theory/quantifiers/ematching/trigger_trie.h b/src/theory/quantifiers/ematching/trigger_trie.h index c016031ed..ad221ee21 100644 --- a/src/theory/quantifiers/ematching/trigger_trie.h +++ b/src/theory/quantifiers/ematching/trigger_trie.h @@ -24,7 +24,7 @@ namespace CVC4 { namespace theory { - +namespace quantifiers { namespace inst { /** A trie of triggers. @@ -56,6 +56,7 @@ class TriggerTrie }; /* class inst::Trigger::TriggerTrie */ } // namespace inst +} // namespace quantifiers } // namespace theory } // namespace CVC4 diff --git a/src/theory/quantifiers/ematching/var_match_generator.cpp b/src/theory/quantifiers/ematching/var_match_generator.cpp index c8d907bcf..1f87c88b4 100644 --- a/src/theory/quantifiers/ematching/var_match_generator.cpp +++ b/src/theory/quantifiers/ematching/var_match_generator.cpp @@ -21,6 +21,7 @@ using namespace CVC4::kind; namespace CVC4 { namespace theory { +namespace quantifiers { namespace inst { VarMatchGeneratorTermSubs::VarMatchGeneratorTermSubs(Trigger* tparent, @@ -79,5 +80,6 @@ int VarMatchGeneratorTermSubs::getNextMatch(Node q, InstMatch& m) } } // namespace inst +} // namespace quantifiers } // namespace theory } // namespace CVC4 diff --git a/src/theory/quantifiers/ematching/var_match_generator.h b/src/theory/quantifiers/ematching/var_match_generator.h index 591c47958..d85a20189 100644 --- a/src/theory/quantifiers/ematching/var_match_generator.h +++ b/src/theory/quantifiers/ematching/var_match_generator.h @@ -22,6 +22,7 @@ namespace CVC4 { namespace theory { +namespace quantifiers { namespace inst { /** match generator for purified terms @@ -50,6 +51,7 @@ class VarMatchGeneratorTermSubs : public InstMatchGenerator }; } // namespace inst +} // namespace quantifiers } // namespace theory } // namespace CVC4 diff --git a/src/theory/quantifiers/fmf/full_model_check.cpp b/src/theory/quantifiers/fmf/full_model_check.cpp index be83f3b10..2245e16dd 100644 --- a/src/theory/quantifiers/fmf/full_model_check.cpp +++ b/src/theory/quantifiers/fmf/full_model_check.cpp @@ -28,14 +28,13 @@ #include "theory/quantifiers_engine.h" #include "theory/rewriter.h" -using namespace std; -using namespace CVC4; using namespace CVC4::kind; using namespace CVC4::context; -using namespace CVC4::theory; -using namespace CVC4::theory::quantifiers; -using namespace CVC4::theory::inst; -using namespace CVC4::theory::quantifiers::fmcheck; + +namespace CVC4 { +namespace theory { +namespace quantifiers { +namespace fmcheck { struct ModelBasisArgSort { @@ -1370,3 +1369,8 @@ bool FullModelChecker::isHandled(Node q) const { return d_unhandledQuant.find(q) == d_unhandledQuant.end(); } + +} // namespace fmcheck +} // namespace quantifiers +} // namespace theory +} // namespace CVC4 diff --git a/src/theory/quantifiers/fmf/model_engine.cpp b/src/theory/quantifiers/fmf/model_engine.cpp index 789a7bd7c..eb7398f92 100644 --- a/src/theory/quantifiers/fmf/model_engine.cpp +++ b/src/theory/quantifiers/fmf/model_engine.cpp @@ -23,13 +23,12 @@ #include "theory/quantifiers/term_database.h" #include "theory/quantifiers_engine.h" -using namespace std; -using namespace CVC4; using namespace CVC4::kind; using namespace CVC4::context; -using namespace CVC4::theory; -using namespace CVC4::theory::quantifiers; -using namespace CVC4::theory::inst; + +namespace CVC4 { +namespace theory { +namespace quantifiers { //Model Engine constructor ModelEngine::ModelEngine(QuantifiersEngine* qe, @@ -335,3 +334,6 @@ void ModelEngine::debugPrint( const char* c ){ //d_quantEngine->getModel()->debugPrint( c ); } +} // namespace quantifiers +} // namespace theory +} // namespace CVC4 diff --git a/src/theory/quantifiers/inst_match.cpp b/src/theory/quantifiers/inst_match.cpp index bb92b905e..a51d66278 100644 --- a/src/theory/quantifiers/inst_match.cpp +++ b/src/theory/quantifiers/inst_match.cpp @@ -21,7 +21,7 @@ namespace CVC4 { namespace theory { -namespace inst { +namespace quantifiers { InstMatch::InstMatch(TNode q) { @@ -103,6 +103,6 @@ bool InstMatch::set(quantifiers::QuantifiersState& qs, size_t i, TNode n) return true; } -}/* CVC4::theory::inst namespace */ +} // namespace quantifiers }/* CVC4::theory namespace */ }/* CVC4 namespace */ diff --git a/src/theory/quantifiers/inst_match.h b/src/theory/quantifiers/inst_match.h index 7bab2083e..0c6ddcf77 100644 --- a/src/theory/quantifiers/inst_match.h +++ b/src/theory/quantifiers/inst_match.h @@ -23,12 +23,9 @@ namespace CVC4 { namespace theory { - namespace quantifiers { -class QuantifiersState; -} -namespace inst { +class QuantifiersState; /** Inst match * @@ -90,10 +87,7 @@ inline std::ostream& operator<<(std::ostream& out, const InstMatch& m) { return out; } -}/* CVC4::theory::inst namespace */ - -typedef CVC4::theory::inst::InstMatch InstMatch; - +} // namespace quantifiers }/* CVC4::theory namespace */ }/* CVC4 namespace */ diff --git a/src/theory/quantifiers/inst_match_trie.cpp b/src/theory/quantifiers/inst_match_trie.cpp index 9c3b9af93..96f668c82 100644 --- a/src/theory/quantifiers/inst_match_trie.cpp +++ b/src/theory/quantifiers/inst_match_trie.cpp @@ -25,7 +25,7 @@ using namespace CVC4::context; namespace CVC4 { namespace theory { -namespace inst { +namespace quantifiers { bool InstMatchTrie::existsInstMatch(quantifiers::QuantifiersState& qs, Node q, @@ -368,6 +368,6 @@ bool InstMatchTrieOrdered::existsInstMatch(quantifiers::QuantifiersState& qs, return d_imt.existsInstMatch(qs, q, m, modEq, d_imtio); } -} /* CVC4::theory::inst namespace */ +} // namespace quantifiers } /* CVC4::theory namespace */ } /* CVC4 namespace */ diff --git a/src/theory/quantifiers/inst_match_trie.h b/src/theory/quantifiers/inst_match_trie.h index 6e6dd92bf..5164f1820 100644 --- a/src/theory/quantifiers/inst_match_trie.h +++ b/src/theory/quantifiers/inst_match_trie.h @@ -25,14 +25,9 @@ namespace CVC4 { namespace theory { - -class QuantifiersEngine; - namespace quantifiers { -class QuantifiersState; -} -namespace inst { +class QuantifiersState; /** trie for InstMatch objects * @@ -62,7 +57,7 @@ class InstMatchTrie * If modEq is true, we check for duplication modulo equality the current * equalities in the equality engine of qs. */ - bool existsInstMatch(quantifiers::QuantifiersState& qs, + bool existsInstMatch(QuantifiersState& qs, Node q, const std::vector& m, bool modEq = false, @@ -76,7 +71,7 @@ class InstMatchTrie * If modEq is true, we check for duplication modulo equality the current * equalities in the equality engine of qs. */ - bool addInstMatch(quantifiers::QuantifiersState& qs, + bool addInstMatch(QuantifiersState& qs, Node f, const std::vector& m, bool modEq = false, @@ -135,7 +130,7 @@ class CDInstMatchTrie * equalities in the equality engine of qs. * It additionally takes a context c, for which the entry is valid in. */ - bool existsInstMatch(quantifiers::QuantifiersState& qs, + bool existsInstMatch(QuantifiersState& qs, Node q, const std::vector& m, bool modEq = false, @@ -149,7 +144,7 @@ class CDInstMatchTrie * equalities in the equality engine of qs. * It additionally takes a context c, for which the entry is valid in. */ - bool addInstMatch(quantifiers::QuantifiersState& qs, + bool addInstMatch(QuantifiersState& qs, Node q, const std::vector& m, bool modEq = false, @@ -205,7 +200,7 @@ class InstMatchTrieOrdered * class. If modEq is true, we consider duplicates modulo the current * equalities stored in the equality engine of qs. */ - bool addInstMatch(quantifiers::QuantifiersState& qs, + bool addInstMatch(QuantifiersState& qs, Node q, const std::vector& m, bool modEq = false); @@ -215,7 +210,7 @@ class InstMatchTrieOrdered * class. If modEq is true, we consider duplicates modulo the current * equalities stored in the equality engine of qs. */ - bool existsInstMatch(quantifiers::QuantifiersState& qs, + bool existsInstMatch(QuantifiersState& qs, Node q, const std::vector& m, bool modEq = false); @@ -227,8 +222,8 @@ class InstMatchTrieOrdered InstMatchTrie d_imt; }; -} /* CVC4::theory::inst namespace */ +} // namespace quantifiers } /* CVC4::theory namespace */ } /* CVC4 namespace */ -#endif /* CVC4__THEORY__QUANTIFIERS__INST_MATCH_H */ +#endif /* CVC4__THEORY__QUANTIFIERS__INST_MATCH_TRIE_H */ diff --git a/src/theory/quantifiers/inst_strategy_enumerative.cpp b/src/theory/quantifiers/inst_strategy_enumerative.cpp index 6efcd2adf..c14ce4ad3 100644 --- a/src/theory/quantifiers/inst_strategy_enumerative.cpp +++ b/src/theory/quantifiers/inst_strategy_enumerative.cpp @@ -28,11 +28,10 @@ using namespace kind; using namespace context; namespace theory { +namespace quantifiers { using namespace inst; -namespace quantifiers { - InstStrategyEnum::InstStrategyEnum(QuantifiersEngine* qe, QuantifiersState& qs, QuantifiersInferenceManager& qim, diff --git a/src/theory/quantifiers/instantiate.cpp b/src/theory/quantifiers/instantiate.cpp index fd74e17e8..61c7703ed 100644 --- a/src/theory/quantifiers/instantiate.cpp +++ b/src/theory/quantifiers/instantiate.cpp @@ -45,13 +45,11 @@ Instantiate::Instantiate(QuantifiersState& qs, QuantifiersInferenceManager& qim, QuantifiersRegistry& qr, TermRegistry& tr, - FirstOrderModel* m, ProofNodeManager* pnm) : d_qstate(qs), d_qim(qim), d_qreg(qr), d_treg(tr), - d_model(m), d_pnm(pnm), d_total_inst_debug(qs.getUserContext()), d_c_inst_match_trie_dom(qs.getUserContext()), @@ -61,7 +59,7 @@ Instantiate::Instantiate(QuantifiersState& qs, Instantiate::~Instantiate() { - for (std::pair& t : d_c_inst_match_trie) + for (std::pair& t : d_c_inst_match_trie) { delete t.second; } @@ -121,7 +119,7 @@ bool Instantiate::addInstantiation(Node q, TypeNode tn = q[0][i].getType(); if (terms[i].isNull()) { - terms[i] = getTermForType(tn); + terms[i] = d_treg.getTermForType(tn); } // Ensure the type is correct, this for instance ensures that real terms // are cast to integers for { x -> t } where x has type Int and t has @@ -131,7 +129,7 @@ bool Instantiate::addInstantiation(Node q, { // pick the best possible representative for instantiation, based on past // use and simplicity of term - terms[i] = d_model->getInternalRepresentative(terms[i], q, i); + terms[i] = d_treg.getModel()->getInternalRepresentative(terms[i], q, i); } Trace("inst-add-debug") << " -> " << terms[i] << std::endl; if (terms[i].isNull()) @@ -496,8 +494,7 @@ bool Instantiate::existsInstantiation(Node q, { if (options::incrementalSolving()) { - std::map::iterator it = - d_c_inst_match_trie.find(q); + std::map::iterator it = d_c_inst_match_trie.find(q); if (it != d_c_inst_match_trie.end()) { return it->second->existsInstMatch(d_qstate, q, terms, modEq); @@ -505,8 +502,7 @@ bool Instantiate::existsInstantiation(Node q, } else { - std::map::iterator it = - d_inst_match_trie.find(q); + std::map::iterator it = d_inst_match_trie.find(q); if (it != d_inst_match_trie.end()) { return it->second.existsInstMatch(d_qstate, q, terms, modEq); @@ -579,16 +575,15 @@ bool Instantiate::recordInstantiationInternal(Node q, Trace("inst-add-debug") << "Adding into context-dependent inst trie, modEq = " << modEq << std::endl; - inst::CDInstMatchTrie* imt; - std::map::iterator it = - d_c_inst_match_trie.find(q); + CDInstMatchTrie* imt; + std::map::iterator it = d_c_inst_match_trie.find(q); if (it != d_c_inst_match_trie.end()) { imt = it->second; } else { - imt = new inst::CDInstMatchTrie(d_qstate.getUserContext()); + imt = new CDInstMatchTrie(d_qstate.getUserContext()); d_c_inst_match_trie[q] = imt; } d_c_inst_match_trie_dom.insert(q); @@ -602,8 +597,7 @@ bool Instantiate::removeInstantiationInternal(Node q, std::vector& terms) { if (options::incrementalSolving()) { - std::map::iterator it = - d_c_inst_match_trie.find(q); + std::map::iterator it = d_c_inst_match_trie.find(q); if (it != d_c_inst_match_trie.end()) { return it->second->removeInstMatch(q, terms); @@ -613,15 +607,6 @@ bool Instantiate::removeInstantiationInternal(Node q, std::vector& terms) return d_inst_match_trie[q].removeInstMatch(q, terms); } -Node Instantiate::getTermForType(TypeNode tn) -{ - if (tn.isClosedEnumerable()) - { - return d_treg.getTermEnumeration()->getEnumerateTerm(tn, 0); - } - return d_treg.getTermDatabase()->getOrMakeTypeGroundTerm(tn); -} - void Instantiate::getInstantiatedQuantifiedFormulas(std::vector& qs) { if (options::incrementalSolving()) @@ -636,7 +621,7 @@ void Instantiate::getInstantiatedQuantifiedFormulas(std::vector& qs) } else { - for (std::pair& t : d_inst_match_trie) + for (std::pair& t : d_inst_match_trie) { qs.push_back(t.first); } @@ -649,7 +634,7 @@ void Instantiate::getInstantiationTermVectors( if (options::incrementalSolving()) { - std::map::const_iterator it = + std::map::const_iterator it = d_c_inst_match_trie.find(q); if (it != d_c_inst_match_trie.end()) { @@ -658,7 +643,7 @@ void Instantiate::getInstantiationTermVectors( } else { - std::map::const_iterator it = + std::map::const_iterator it = d_inst_match_trie.find(q); if (it != d_inst_match_trie.end()) { diff --git a/src/theory/quantifiers/instantiate.h b/src/theory/quantifiers/instantiate.h index 8e556b648..be410c2c8 100644 --- a/src/theory/quantifiers/instantiate.h +++ b/src/theory/quantifiers/instantiate.h @@ -97,7 +97,6 @@ class Instantiate : public QuantifiersUtil QuantifiersInferenceManager& qim, QuantifiersRegistry& qr, TermRegistry& tr, - FirstOrderModel* m, ProofNodeManager* pnm = nullptr); ~Instantiate(); @@ -224,17 +223,6 @@ class Instantiate : public QuantifiersUtil * Same as above but with vars equal to the bound variables of q. */ Node getInstantiation(Node q, std::vector& terms, bool doVts = false); - /** get term for type - * - * This returns an arbitrary term for type tn. - * This term is chosen heuristically to be the best - * term for instantiation. Currently, this - * heuristic enumerates the first term of the - * type if the type is closed enumerable, otherwise - * an existing ground term from the term database if - * one exists, or otherwise a fresh variable. - */ - Node getTermForType(TypeNode tn); //--------------------------------------end general utilities /** @@ -318,8 +306,6 @@ class Instantiate : public QuantifiersUtil 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; /** instantiation rewriter classes */ @@ -335,8 +321,8 @@ class Instantiate : public QuantifiersUtil * We store context (dependent, independent) versions. If incremental solving * is disabled, we use d_inst_match_trie for performance reasons. */ - std::map d_inst_match_trie; - std::map d_c_inst_match_trie; + std::map d_inst_match_trie; + std::map d_c_inst_match_trie; /** * The list of quantified formulas for which the domain of d_c_inst_match_trie * is valid. diff --git a/src/theory/quantifiers/quantifiers_inference_manager.cpp b/src/theory/quantifiers/quantifiers_inference_manager.cpp index 9a82265f9..b25c1aed3 100644 --- a/src/theory/quantifiers/quantifiers_inference_manager.cpp +++ b/src/theory/quantifiers/quantifiers_inference_manager.cpp @@ -26,10 +26,9 @@ QuantifiersInferenceManager::QuantifiersInferenceManager( 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_instantiate(new Instantiate(state, *this, qr, tr, pnm)), d_skolemize(new Skolemize(state, pnm)) { } diff --git a/src/theory/quantifiers/quantifiers_inference_manager.h b/src/theory/quantifiers/quantifiers_inference_manager.h index aa7fc1b6a..f16f91f04 100644 --- a/src/theory/quantifiers/quantifiers_inference_manager.h +++ b/src/theory/quantifiers/quantifiers_inference_manager.h @@ -39,7 +39,6 @@ class QuantifiersInferenceManager : public InferenceManagerBuffered QuantifiersState& state, QuantifiersRegistry& qr, TermRegistry& tr, - FirstOrderModel* m, ProofNodeManager* pnm); ~QuantifiersInferenceManager(); /** get instantiate utility */ diff --git a/src/theory/quantifiers/quantifiers_modules.cpp b/src/theory/quantifiers/quantifiers_modules.cpp index 11d9a116c..bb35d6d26 100644 --- a/src/theory/quantifiers/quantifiers_modules.cpp +++ b/src/theory/quantifiers/quantifiers_modules.cpp @@ -15,8 +15,9 @@ #include "theory/quantifiers/quantifiers_modules.h" #include "options/quantifiers_options.h" -#include "theory/quantifiers_engine.h" #include "theory/quantifiers/relevant_domain.h" +#include "theory/quantifiers/term_registry.h" +#include "theory/quantifiers_engine.h" namespace CVC4 { namespace theory { @@ -43,6 +44,7 @@ void QuantifiersModules::initialize(QuantifiersEngine* qe, QuantifiersState& qs, QuantifiersInferenceManager& qim, QuantifiersRegistry& qr, + TermRegistry& tr, DecisionManager* dm, std::vector& modules) { @@ -59,7 +61,7 @@ void QuantifiersModules::initialize(QuantifiersEngine* qe, } if (!options::finiteModelFind() || options::fmfInstEngine()) { - d_inst_engine.reset(new InstantiationEngine(qe, qs, qim, qr)); + d_inst_engine.reset(new InstantiationEngine(qe, qs, qim, qr, tr)); modules.push_back(d_inst_engine.get()); } if (options::cegqi()) @@ -86,7 +88,7 @@ void QuantifiersModules::initialize(QuantifiersEngine* qe, Trace("quant-init-debug") << "Initialize model engine, mbqi : " << options::mbqiMode() << " " << options::fmfBound() << std::endl; - if (useFmcModel()) + if (tr.useFmcModel()) { Trace("quant-init-debug") << "...make fmc builder." << std::endl; d_builder.reset(new fmcheck::FullModelChecker(qs, qr)); @@ -123,13 +125,6 @@ void QuantifiersModules::initialize(QuantifiersEngine* qe, } } -bool QuantifiersModules::useFmcModel() -{ - return options::mbqiMode() == options::MbqiMode::FMC - || options::mbqiMode() == options::MbqiMode::TRUST - || options::fmfBound(); -} - } // namespace quantifiers } // namespace theory } // namespace CVC4 diff --git a/src/theory/quantifiers/quantifiers_modules.h b/src/theory/quantifiers/quantifiers_modules.h index c111eba25..4ecbf7af4 100644 --- a/src/theory/quantifiers/quantifiers_modules.h +++ b/src/theory/quantifiers/quantifiers_modules.h @@ -58,12 +58,10 @@ class QuantifiersModules QuantifiersState& qs, QuantifiersInferenceManager& qim, QuantifiersRegistry& qr, + TermRegistry& tr, DecisionManager* dm, std::vector& modules); - /** Whether we use the full model check builder and corresponding model */ - static bool useFmcModel(); - private: //------------------------------ quantifier utilities /** relevant domain */ diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index ca11d491d..a6d138806 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -28,10 +28,8 @@ #include "theory/quantifiers_engine.h" #include "theory/theory_engine.h" -using namespace std; using namespace CVC4::kind; using namespace CVC4::context; -using namespace CVC4::theory::inst; namespace CVC4 { namespace theory { diff --git a/src/theory/quantifiers/term_registry.cpp b/src/theory/quantifiers/term_registry.cpp index d23ff060a..74dad6cc7 100644 --- a/src/theory/quantifiers/term_registry.cpp +++ b/src/theory/quantifiers/term_registry.cpp @@ -16,6 +16,8 @@ #include "options/quantifiers_options.h" #include "options/smt_options.h" +#include "theory/quantifiers/first_order_model.h" +#include "theory/quantifiers/fmf/first_order_model_fmc.h" #include "theory/quantifiers/quantifiers_state.h" namespace CVC4 { @@ -24,6 +26,7 @@ namespace quantifiers { TermRegistry::TermRegistry(QuantifiersState& qs, QuantifiersRegistry& qr) : d_presolve(qs.getUserContext(), true), + d_useFmcModel(false), d_presolveCache(qs.getUserContext()), d_termEnum(new TermEnumeration), d_termDb(new TermDb(qs, qr)), @@ -34,6 +37,26 @@ TermRegistry::TermRegistry(QuantifiersState& qs, QuantifiersRegistry& qr) // must be constructed here since it is required for datatypes finistInit d_sygusTdb.reset(new TermDbSygus(qs)); } + Trace("quant-engine-debug") << "Initialize quantifiers engine." << std::endl; + Trace("quant-engine-debug") + << "Initialize model, mbqi : " << options::mbqiMode() << std::endl; + // 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()) + && (options::mbqiMode() == options::MbqiMode::FMC + || options::mbqiMode() == options::MbqiMode::TRUST + || options::fmfBound())) + { + d_useFmcModel = true; + d_qmodel.reset(new quantifiers::fmcheck::FirstOrderModelFmc( + qs, qr, *this, "FirstOrderModelFmc")); + } + else + { + d_qmodel.reset( + new quantifiers::FirstOrderModel(qs, qr, *this, "FirstOrderModel")); + } } void TermRegistry::finishInit(QuantifiersInferenceManager* qim) @@ -84,6 +107,15 @@ void TermRegistry::addTerm(Node n, bool withinQuant) } } +Node TermRegistry::getTermForType(TypeNode tn) +{ + if (tn.isClosedEnumerable()) + { + return d_termEnum->getEnumerateTerm(tn, 0); + } + return d_termDb->getOrMakeTypeGroundTerm(tn); +} + TermDb* TermRegistry::getTermDatabase() const { return d_termDb.get(); } TermDbSygus* TermRegistry::getTermDatabaseSygus() const @@ -95,6 +127,11 @@ TermEnumeration* TermRegistry::getTermEnumeration() const { return d_termEnum.get(); } + +FirstOrderModel* TermRegistry::getModel() const { return d_qmodel.get(); } + +bool TermRegistry::useFmcModel() const { return d_useFmcModel; } + } // namespace quantifiers } // namespace theory } // namespace CVC4 diff --git a/src/theory/quantifiers/term_registry.h b/src/theory/quantifiers/term_registry.h index 1d9058603..d70b7acf8 100644 --- a/src/theory/quantifiers/term_registry.h +++ b/src/theory/quantifiers/term_registry.h @@ -29,6 +29,8 @@ namespace CVC4 { namespace theory { namespace quantifiers { +class FirstOrderModel; + /** * Term Registry, which manages notifying modules within quantifiers about * (ground) terms that exist in the current context. @@ -54,16 +56,35 @@ class TermRegistry */ void addTerm(Node n, bool withinQuant = false); + /** get term for type + * + * This returns an arbitrary term for type tn. + * This term is chosen heuristically to be the best + * term for instantiation. Currently, this + * heuristic enumerates the first term of the + * type if the type is closed enumerable, otherwise + * an existing ground term from the term database if + * one exists, or otherwise a fresh variable. + */ + Node getTermForType(TypeNode tn); + + /** Whether we use the full model check builder and corresponding model */ + bool useFmcModel() const; + /** get term database */ TermDb* getTermDatabase() const; /** get term database sygus */ TermDbSygus* getTermDatabaseSygus() const; /** get term enumeration utility */ TermEnumeration* getTermEnumeration() const; + /** get the model utility */ + FirstOrderModel* getModel() const; private: /** has presolve been called */ context::CDO d_presolve; + /** Whether we are using the fmc model */ + bool d_useFmcModel; /** the set of terms we have seen before presolve */ NodeSet d_presolveCache; /** term enumeration utility */ @@ -72,6 +93,8 @@ class TermRegistry std::unique_ptr d_termDb; /** sygus term database */ std::unique_ptr d_sygusTdb; + /** extended model object */ + std::unique_ptr d_qmodel; }; } // namespace quantifiers diff --git a/src/theory/quantifiers/term_util.cpp b/src/theory/quantifiers/term_util.cpp index 069b9b935..d555a85da 100644 --- a/src/theory/quantifiers/term_util.cpp +++ b/src/theory/quantifiers/term_util.cpp @@ -27,10 +27,7 @@ #include "theory/strings/word.h" #include "theory/rewriter.h" -using namespace std; using namespace CVC4::kind; -using namespace CVC4::context; -using namespace CVC4::theory::inst; namespace CVC4 { namespace theory { diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp index 092689b5f..ace7b79ff 100644 --- a/src/theory/quantifiers/theory_quantifiers.cpp +++ b/src/theory/quantifiers/theory_quantifiers.cpp @@ -18,8 +18,6 @@ #include "expr/proof_node_manager.h" #include "options/quantifiers_options.h" -#include "theory/quantifiers/first_order_model.h" -#include "theory/quantifiers/fmf/first_order_model_fmc.h" #include "theory/quantifiers/quantifiers_modules.h" #include "theory/quantifiers/quantifiers_rewriter.h" #include "theory/valuation.h" @@ -41,7 +39,7 @@ TheoryQuantifiers::TheoryQuantifiers(Context* c, d_qstate(c, u, valuation, logicInfo), d_qreg(), d_treg(d_qstate, d_qreg), - d_qim(nullptr), + d_qim(*this, d_qstate, d_qreg, d_treg, pnm), d_qengine(nullptr) { out.handleUserAttribute( "fun-def", this ); @@ -57,45 +55,23 @@ TheoryQuantifiers::TheoryQuantifiers(Context* c, d_qChecker.registerTo(pc); } - Trace("quant-engine-debug") << "Initialize quantifiers engine." << std::endl; - Trace("quant-engine-debug") - << "Initialize model, mbqi : " << options::mbqiMode() << std::endl; - // 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()) - && 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_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()); + d_treg.finishInit(&d_qim); // construct the quantifiers engine - d_qengine.reset(new QuantifiersEngine( - d_qstate, d_qreg, d_treg, *d_qim.get(), d_qmodel.get(), pnm)); + d_qengine.reset(new QuantifiersEngine(d_qstate, d_qreg, d_treg, d_qim, pnm)); //!!!!!!!!!!!!!! temporary (project #15) - d_qmodel->finishInit(d_qengine.get()); + d_treg.getModel()->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(); + d_inferManager = &d_qim; // 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 2371b00ce..91f12c0ed 100644 --- a/src/theory/quantifiers/theory_quantifiers.h +++ b/src/theory/quantifiers/theory_quantifiers.h @@ -20,7 +20,6 @@ #define CVC4__THEORY__QUANTIFIERS__THEORY_QUANTIFIERS_H #include "expr/node.h" -#include "theory/quantifiers/first_order_model.h" #include "theory/quantifiers/proof_checker.h" #include "theory/quantifiers/quantifiers_inference_manager.h" #include "theory/quantifiers/quantifiers_registry.h" @@ -89,12 +88,10 @@ class TheoryQuantifiers : public Theory { QuantifiersState d_qstate; /** The quantifiers registry */ QuantifiersRegistry d_qreg; - /** extended model object */ - std::unique_ptr d_qmodel; /** The term registry */ TermRegistry d_treg; /** The quantifiers inference manager */ - std::unique_ptr d_qim; + QuantifiersInferenceManager 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 9ca8226bc..2cface166 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -51,7 +51,6 @@ QuantifiersEngine::QuantifiersEngine( quantifiers::QuantifiersRegistry& qr, quantifiers::TermRegistry& tr, quantifiers::QuantifiersInferenceManager& qim, - quantifiers::FirstOrderModel* qm, ProofNodeManager* pnm) : d_qstate(qstate), d_qim(qim), @@ -60,8 +59,8 @@ QuantifiersEngine::QuantifiersEngine( d_pnm(pnm), d_qreg(qr), d_treg(tr), - d_tr_trie(new inst::TriggerTrie), - d_model(qm), + d_tr_trie(new quantifiers::inst::TriggerTrie), + d_model(d_treg.getModel()), d_quants_prereg(qstate.getUserContext()), d_quants_red(qstate.getUserContext()) { @@ -81,7 +80,7 @@ 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, dm, d_modules); + d_qmodules->initialize(this, d_qstate, d_qim, d_qreg, d_treg, dm, d_modules); if (d_qmodules->d_rel_dom.get()) { d_util.push_back(d_qmodules->d_rel_dom.get()); @@ -145,7 +144,7 @@ quantifiers::Skolemize* QuantifiersEngine::getSkolemize() const { return d_qim.getSkolemize(); } -inst::TriggerTrie* QuantifiersEngine::getTriggerDatabase() const +quantifiers::inst::TriggerTrie* QuantifiersEngine::getTriggerDatabase() const { return d_tr_trie.get(); } diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index b6562caa7..1f1dcc950 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -36,10 +36,12 @@ class DecisionManager; class QuantifiersModule; class RepSetIterator; +namespace quantifiers { + namespace inst { class TriggerTrie; } -namespace quantifiers { + class FirstOrderModel; class Instantiate; class QModelBuilder; @@ -67,7 +69,6 @@ class QuantifiersEngine { quantifiers::QuantifiersRegistry& qr, quantifiers::TermRegistry& tr, quantifiers::QuantifiersInferenceManager& qim, - quantifiers::FirstOrderModel* qm, ProofNodeManager* pnm); ~QuantifiersEngine(); //---------------------- external interface @@ -96,7 +97,7 @@ class QuantifiersEngine { /** get skolemize utility */ quantifiers::Skolemize* getSkolemize() const; /** get trigger database */ - inst::TriggerTrie* getTriggerDatabase() const; + quantifiers::inst::TriggerTrie* getTriggerDatabase() const; //---------------------- end utilities private: //---------------------- private initialization @@ -234,7 +235,7 @@ public: /** The term registry */ quantifiers::TermRegistry& d_treg; /** all triggers will be stored in this trie */ - std::unique_ptr d_tr_trie; + std::unique_ptr d_tr_trie; /** extended model object */ quantifiers::FirstOrderModel* d_model; //------------- end quantifiers utilities -- 2.30.2