diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-03-23 15:41:13 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-03-23 20:41:13 +0000 |
commit | d5d526730d11d08c65aa17ea53d0dffb0a72e692 (patch) | |
tree | 13ce2001785e168ea82cbd0bce0c1750f987a338 /src/theory/quantifiers/ematching | |
parent | 8fc8793f4337663f7250846dd6acae167a7f27ec (diff) |
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.
Diffstat (limited to 'src/theory/quantifiers/ematching')
32 files changed, 247 insertions, 152 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_iter<d_term_iter_limit ){ - Node n = d_qe->getTermDatabase()->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<Node>& nodes, std::map<Node, std::vector<Node> >& 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<Node>& 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<const TNode, std::vector<Node> >& 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<Node>& nodes, std::map<Node, std::vector<Node> >& 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<Node, std::vector<Node> > 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<const Node, std::vector<Node> >& 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<Node, std::vector<Node> > var_contains; for (const Node& pat : pats) { - quantifiers::TermUtil::computeInstConstContainsForQuant( - q, pat, var_contains[pat]); + TermUtil::computeInstConstContainsForQuant(q, pat, var_contains[pat]); } std::map<Node, std::vector<Node> > var_to_node; for (std::pair<const Node, std::vector<Node> >& 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<Node, std::vector<inst::Trigger*> >::const_iterator it = + std::map<Node, std::vector<Trigger*> >::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<Node, std::vector<inst::Trigger*> >::const_iterator it = + std::map<Node, std::vector<Trigger*> >::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<inst::Trigger*>& ug = d_user_gen[q]; + std::vector<Trigger*>& 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<Node>& 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<Node>& 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<Node>& 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<Node>& 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<Node>& 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 |