diff options
Diffstat (limited to 'src/theory/quantifiers/ematching')
12 files changed, 200 insertions, 125 deletions
diff --git a/src/theory/quantifiers/ematching/candidate_generator.cpp b/src/theory/quantifiers/ematching/candidate_generator.cpp index cb0fcaf50..3be1d4a4b 100644 --- a/src/theory/quantifiers/ematching/candidate_generator.cpp +++ b/src/theory/quantifiers/ematching/candidate_generator.cpp @@ -173,16 +173,18 @@ void CandidateGeneratorQEAll::reset( Node eqc ) { } Node CandidateGeneratorQEAll::getNextCandidate() { + quantifiers::TermDb* tdb = d_qe->getTermDatabase(); while( !d_eq.isFinished() ){ TNode n = (*d_eq); ++d_eq; if( n.getType().isComparableTo( d_match_pattern_type ) ){ - TNode nh = d_qe->getTermDatabase()->getEligibleTermInEqc( n ); + TNode nh = tdb->getEligibleTermInEqc(n); if( !nh.isNull() ){ if( options::instMaxLevel()!=-1 || options::lteRestrictInstClosure() ){ nh = d_qe->getInternalRepresentative( nh, d_f, d_index ); //don't consider this if already the instantiation is ineligible - if( !d_qe->getTermDatabase()->isTermEligibleForInstantiation( nh, d_f, false ) ){ + if (!tdb->isTermEligibleForInstantiation(nh, d_f)) + { nh = Node::null(); } } diff --git a/src/theory/quantifiers/ematching/candidate_generator.h b/src/theory/quantifiers/ematching/candidate_generator.h index d2718fa1f..8cff12477 100644 --- a/src/theory/quantifiers/ematching/candidate_generator.h +++ b/src/theory/quantifiers/ematching/candidate_generator.h @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__THEORY__QUANTIFIERS__CANDIDATE_GENERATOR_H -#define __CVC4__THEORY__QUANTIFIERS__CANDIDATE_GENERATOR_H +#ifndef CVC4__THEORY__QUANTIFIERS__CANDIDATE_GENERATOR_H +#define CVC4__THEORY__QUANTIFIERS__CANDIDATE_GENERATOR_H #include "theory/theory.h" #include "theory/uf/equality_engine.h" @@ -212,4 +212,4 @@ class CandidateGeneratorConsExpand : public CandidateGeneratorQE }/* CVC4::theory namespace */ }/* CVC4 namespace */ -#endif /* __CVC4__THEORY__QUANTIFIERS__CANDIDATE_GENERATOR_H */ +#endif /* CVC4__THEORY__QUANTIFIERS__CANDIDATE_GENERATOR_H */ diff --git a/src/theory/quantifiers/ematching/ho_trigger.cpp b/src/theory/quantifiers/ematching/ho_trigger.cpp index 7598e6fdc..b01d5e1df 100644 --- a/src/theory/quantifiers/ematching/ho_trigger.cpp +++ b/src/theory/quantifiers/ematching/ho_trigger.cpp @@ -469,12 +469,12 @@ int HigherOrderTrigger::addHoTypeMatchPredicateLemmas() Trace("ho-quant-trigger") << "addHoTypeMatchPredicateLemmas..." << std::endl; unsigned numLemmas = 0; // this forces expansion of APPLY_UF terms to curried HO_APPLY chains - unsigned size = d_quantEngine->getTermDatabase()->getNumOperators(); - quantifiers::TermUtil* tutil = d_quantEngine->getTermUtil(); + quantifiers::TermDb* tdb = d_quantEngine->getTermDatabase(); + unsigned size = tdb->getNumOperators(); NodeManager* nm = NodeManager::currentNM(); for (unsigned j = 0; j < size; j++) { - Node f = d_quantEngine->getTermDatabase()->getOperator(j); + Node f = tdb->getOperator(j); if (f.isVar()) { TypeNode tn = f.getType(); @@ -497,7 +497,7 @@ int HigherOrderTrigger::addHoTypeMatchPredicateLemmas() // if a variable of this type occurs in this trigger if (d_ho_var_types.find(stn) != d_ho_var_types.end()) { - Node u = tutil->getHoTypeMatchPredicate(tn); + Node u = tdb->getHoTypeMatchPredicate(tn); Node au = nm->mkNode(kind::APPLY_UF, u, f); if (d_quantEngine->addLemma(au)) { diff --git a/src/theory/quantifiers/ematching/ho_trigger.h b/src/theory/quantifiers/ematching/ho_trigger.h index b57db5799..6f0ff0635 100644 --- a/src/theory/quantifiers/ematching/ho_trigger.h +++ b/src/theory/quantifiers/ematching/ho_trigger.h @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__THEORY__QUANTIFIERS__HO_TRIGGER_H -#define __CVC4__THEORY__QUANTIFIERS__HO_TRIGGER_H +#ifndef CVC4__THEORY__QUANTIFIERS__HO_TRIGGER_H +#define CVC4__THEORY__QUANTIFIERS__HO_TRIGGER_H #include <map> #include <unordered_set> @@ -275,4 +275,4 @@ class HigherOrderTrigger : public Trigger } /* CVC4::theory namespace */ } /* CVC4 namespace */ -#endif /* __CVC4__THEORY__QUANTIFIERS__HO_TRIGGER_H */ +#endif /* CVC4__THEORY__QUANTIFIERS__HO_TRIGGER_H */ diff --git a/src/theory/quantifiers/ematching/inst_match_generator.cpp b/src/theory/quantifiers/ematching/inst_match_generator.cpp index 0a4386db9..9e76a6a31 100644 --- a/src/theory/quantifiers/ematching/inst_match_generator.cpp +++ b/src/theory/quantifiers/ematching/inst_match_generator.cpp @@ -98,28 +98,53 @@ void InstMatchGenerator::initialize( Node q, QuantifiersEngine* qe, std::vector< if( !d_pattern.isNull() ){ Trace("inst-match-gen") << "Initialize, pattern term is " << d_pattern << std::endl; if( d_match_pattern.getKind()==NOT ){ + Assert(d_pattern.getKind() == NOT); //we want to add the children of the NOT - d_match_pattern = d_pattern[0]; + d_match_pattern = d_match_pattern[0]; + } + + if (d_pattern.getKind() == NOT && d_match_pattern.getKind() == EQUAL + && d_match_pattern[0].getKind() == INST_CONSTANT + && d_match_pattern[1].getKind() == INST_CONSTANT) + { + // special case: disequalities between variables x != y will match ground + // disequalities. } - if( d_match_pattern.getKind()==EQUAL || d_match_pattern.getKind()==GEQ ){ - //make sure the matching portion of the equality is on the LHS of d_pattern - // and record what d_match_pattern is + else if (d_match_pattern.getKind() == EQUAL + || d_match_pattern.getKind() == GEQ) + { + // We are one of the following cases: + // f(x)~a, f(x)~y, x~a, x~y + // If we are the first or third case, we ensure that f(x)/x is on the left + // hand side of the relation d_pattern, d_match_pattern is f(x)/x and + // d_eq_class_rel (indicating the equivalence class that we are related + // to) is set to a. for( unsigned i=0; i<2; i++ ){ - if( !quantifiers::TermUtil::hasInstConstAttr(d_match_pattern[i]) || d_match_pattern[i].getKind()==INST_CONSTANT ){ - Node mp = d_match_pattern[1-i]; - Node mpo = d_match_pattern[i]; - if( mp.getKind()!=INST_CONSTANT ){ - if( i==0 ){ - if( d_match_pattern.getKind()==GEQ ){ - d_pattern = NodeManager::currentNM()->mkNode( kind::GT, mp, mpo ); - d_pattern = d_pattern.negate(); - }else{ - d_pattern = NodeManager::currentNM()->mkNode( d_match_pattern.getKind(), mp, mpo ); - } + Node mp = d_match_pattern[i]; + Node mpo = d_match_pattern[1 - i]; + // If this side has free variables, and the other side does not or + // it is a free variable, then we will match on this side of the + // relation. + if (quantifiers::TermUtil::hasInstConstAttr(mp) + && (!quantifiers::TermUtil::hasInstConstAttr(mpo) + || mpo.getKind() == INST_CONSTANT)) + { + if (i == 1) + { + if (d_match_pattern.getKind() == GEQ) + { + d_pattern = NodeManager::currentNM()->mkNode(kind::GT, mp, mpo); + d_pattern = d_pattern.negate(); + } + else + { + d_pattern = NodeManager::currentNM()->mkNode( + d_match_pattern.getKind(), mp, mpo); } - d_eq_class_rel = mpo; - d_match_pattern = mp; } + d_eq_class_rel = mpo; + d_match_pattern = mp; + // we won't find a term in the other direction break; } } @@ -178,9 +203,7 @@ void InstMatchGenerator::initialize( Node q, QuantifiersEngine* qe, std::vector< { // 1-constructors have a trivial way of generating candidates in a // given equivalence class - const Datatype& dt = - static_cast<DatatypeType>(d_match_pattern.getType().toType()) - .getDatatype(); + const Datatype& dt = d_match_pattern.getType().getDatatype(); if (dt.getNumConstructors() == 1) { d_cg = new inst::CandidateGeneratorConsExpand(qe, d_match_pattern); @@ -188,14 +211,18 @@ void InstMatchGenerator::initialize( Node q, QuantifiersEngine* qe, std::vector< } if (d_cg == nullptr) { - // we will be scanning lists trying to find - // d_match_pattern.getOperator() - d_cg = new inst::CandidateGeneratorQE(qe, d_match_pattern); - } - //if matching on disequality, inform the candidate generator not to match on eqc - if( d_pattern.getKind()==NOT && d_pattern[0].getKind()==EQUAL ){ - ((inst::CandidateGeneratorQE*)d_cg)->excludeEqc( d_eq_class_rel ); - d_eq_class_rel = Node::null(); + CandidateGeneratorQE* cg = + new CandidateGeneratorQE(qe, 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; + // if matching on disequality, inform the candidate generator not to + // match on eqc + if (d_pattern.getKind() == NOT && d_pattern[0].getKind() == EQUAL) + { + cg->excludeEqc(d_eq_class_rel); + d_eq_class_rel = Node::null(); + } } }else if( d_match_pattern.getKind()==INST_CONSTANT ){ if( d_pattern.getKind()==APPLY_SELECTOR_TOTAL ){ @@ -209,12 +236,15 @@ void InstMatchGenerator::initialize( Node q, QuantifiersEngine* qe, std::vector< }else{ d_cg = new CandidateGeneratorQEAll( qe, d_match_pattern ); } - }else if( d_match_pattern.getKind()==EQUAL && - d_match_pattern[0].getKind()==INST_CONSTANT && d_match_pattern[1].getKind()==INST_CONSTANT ){ + } + else if (d_match_pattern.getKind() == EQUAL) + { //we will be producing candidates via literal matching heuristics - Assert(d_pattern.getKind() == NOT); - // candidates will be all disequalities - d_cg = new inst::CandidateGeneratorQELitDeq(qe, d_match_pattern); + if (d_pattern.getKind() == NOT) + { + // candidates will be all disequalities + d_cg = new inst::CandidateGeneratorQELitDeq(qe, d_match_pattern); + } }else{ Trace("inst-match-gen-warn") << "(?) Unknown matching pattern is " << d_match_pattern << std::endl; } @@ -288,8 +318,10 @@ int InstMatchGenerator::getMatch( prev.push_back(d_children_types[0]); } } + } //for relational matching - }else if( !d_eq_class_rel.isNull() && d_eq_class_rel.getKind()==INST_CONSTANT ){ + if (!d_eq_class_rel.isNull() && d_eq_class_rel.getKind() == INST_CONSTANT) + { int v = d_eq_class_rel.getAttribute(InstVarNumAttribute()); //also must fit match to equivalence class bool pol = d_pattern.getKind()!=NOT; diff --git a/src/theory/quantifiers/ematching/inst_match_generator.h b/src/theory/quantifiers/ematching/inst_match_generator.h index f9fd2be25..3995c67b4 100644 --- a/src/theory/quantifiers/ematching/inst_match_generator.h +++ b/src/theory/quantifiers/ematching/inst_match_generator.h @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__THEORY__QUANTIFIERS__INST_MATCH_GENERATOR_H -#define __CVC4__THEORY__QUANTIFIERS__INST_MATCH_GENERATOR_H +#ifndef CVC4__THEORY__QUANTIFIERS__INST_MATCH_GENERATOR_H +#define CVC4__THEORY__QUANTIFIERS__INST_MATCH_GENERATOR_H #include <map> #include "expr/node_trie.h" diff --git a/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp b/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp index 8f671fb55..876e4e369 100644 --- a/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp +++ b/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp @@ -18,6 +18,7 @@ #include "theory/quantifiers/quantifiers_attributes.h" #include "theory/quantifiers/term_database.h" #include "theory/quantifiers/term_util.h" +#include "theory/quantifiers_engine.h" #include "theory/theory_engine.h" #include "util/random.h" @@ -41,11 +42,11 @@ namespace quantifiers { // user-pat=interleave alternates between use and resort struct sortQuantifiersForSymbol { - QuantifiersEngine* d_qe; + QuantRelevance* d_quant_rel; std::map< Node, Node > d_op_map; bool operator() (Node i, Node j) { - int nqfsi = d_qe->getQuantifierRelevance()->getNumQuantifiersForSymbol( d_op_map[i] ); - int nqfsj = d_qe->getQuantifierRelevance()->getNumQuantifiersForSymbol( d_op_map[j] ); + int nqfsi = d_quant_rel->getNumQuantifiersForSymbol(d_op_map[i]); + int nqfsj = d_quant_rel->getNumQuantifiersForSymbol(d_op_map[j]); if( nqfsi<nqfsj ){ return true; }else if( nqfsi>nqfsj ){ @@ -154,7 +155,10 @@ void InstStrategyUserPatterns::addUserPattern( Node q, Node pat ){ } } -InstStrategyAutoGenTriggers::InstStrategyAutoGenTriggers( QuantifiersEngine* qe ) : InstStrategy( qe ){ +InstStrategyAutoGenTriggers::InstStrategyAutoGenTriggers(QuantifiersEngine* qe, + QuantRelevance* qr) + : InstStrategy(qe), d_quant_rel(qr) +{ //how to select trigger terms d_tr_strategy = options::triggerSelMode(); //whether to select new triggers during the search @@ -325,7 +329,10 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f ){ } } int curr_w = Trigger::getTriggerWeight( patTermsF[i] ); - if( ntrivTriggers && !newVar && last_weight!=-1 && curr_w>last_weight ){ + // triggers whose value is maximum (2) are considered expendable. + if (ntrivTriggers && !newVar && last_weight != -1 && curr_w > last_weight + && curr_w >= 2) + { Trace("auto-gen-trigger-debug") << "...exclude expendible non-trivial trigger : " << patTermsF[i] << std::endl; rmPatTermsF[patTermsF[i]] = true; }else{ @@ -425,8 +432,9 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f ){ Trace("auto-gen-trigger") << "Generate trigger for " << f << std::endl; //sort terms based on relevance if( options::relevantTriggers() ){ + Assert(d_quant_rel); sortQuantifiersForSymbol sqfs; - sqfs.d_qe = d_quantEngine; + sqfs.d_quant_rel = d_quant_rel; for( unsigned i=0; i<patTerms.size(); i++ ){ Assert( d_pat_to_mpat.find( patTerms[i] )!=d_pat_to_mpat.end() ); Assert( d_pat_to_mpat[patTerms[i]].hasOperator() ); @@ -434,10 +442,19 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f ){ } //sort based on # occurrences (this will cause Trigger to select rarer symbols) std::sort( patTerms.begin(), patTerms.end(), sqfs ); - Debug("relevant-trigger") << "Terms based on relevance: " << std::endl; - for( unsigned i=0; i<patTerms.size(); i++ ){ - Debug("relevant-trigger") << " " << patTerms[i] << " from " << d_pat_to_mpat[patTerms[i]] << " ("; - Debug("relevant-trigger") << d_quantEngine->getQuantifierRelevance()->getNumQuantifiersForSymbol( d_pat_to_mpat[patTerms[i]].getOperator() ) << ")" << std::endl; + if (Debug.isOn("relevant-trigger")) + { + Debug("relevant-trigger") + << "Terms based on relevance: " << std::endl; + for (const Node& p : patTerms) + { + Debug("relevant-trigger") + << " " << p << " from " << d_pat_to_mpat[p] << " ("; + Debug("relevant-trigger") + << d_quant_rel->getNumQuantifiersForSymbol( + d_pat_to_mpat[p].getOperator()) + << ")" << std::endl; + } } } //now, generate the trigger... @@ -478,14 +495,18 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f ){ //check if similar patterns exist, and if so, add them additionally unsigned nqfs_curr = 0; if( options::relevantTriggers() ){ - nqfs_curr = d_quantEngine->getQuantifierRelevance()->getNumQuantifiersForSymbol( patTerms[0].getOperator() ); + nqfs_curr = d_quant_rel->getNumQuantifiersForSymbol( + patTerms[0].getOperator()); } index++; bool success = true; while( success && index<patTerms.size() && d_is_single_trigger[ patTerms[index] ] ){ success = false; - if( !options::relevantTriggers() || - d_quantEngine->getQuantifierRelevance()->getNumQuantifiersForSymbol( patTerms[index].getOperator() )<=nqfs_curr ){ + if (!options::relevantTriggers() + || d_quant_rel->getNumQuantifiersForSymbol( + patTerms[index].getOperator()) + <= nqfs_curr) + { d_single_trigger_gen[ patTerms[index] ] = true; Trigger* tr2 = Trigger::mkTrigger( d_quantEngine, f, patTerms[index], false, Trigger::TR_RETURN_NULL, d_num_trigger_vars[f] ); addTrigger( tr2, f ); diff --git a/src/theory/quantifiers/ematching/inst_strategy_e_matching.h b/src/theory/quantifiers/ematching/inst_strategy_e_matching.h index d715d7f7a..1a014939f 100644 --- a/src/theory/quantifiers/ematching/inst_strategy_e_matching.h +++ b/src/theory/quantifiers/ematching/inst_strategy_e_matching.h @@ -14,16 +14,12 @@ #include "cvc4_private.h" -#ifndef __CVC4__INST_STRATEGY_E_MATCHING_H -#define __CVC4__INST_STRATEGY_E_MATCHING_H +#ifndef CVC4__INST_STRATEGY_E_MATCHING_H +#define CVC4__INST_STRATEGY_E_MATCHING_H -#include "context/context.h" -#include "context/context_mm.h" #include "theory/quantifiers/ematching/instantiation_engine.h" #include "theory/quantifiers/ematching/trigger.h" -#include "theory/quantifiers_engine.h" -#include "util/statistics_registry.h" -#include "options/quantifiers_options.h" +#include "theory/quantifiers/quant_relevance.h" namespace CVC4 { namespace theory { @@ -100,9 +96,11 @@ private: bool hasUserPatterns(Node q); /** has user patterns */ std::map<Node, bool> d_hasUserPatterns; + public: - InstStrategyAutoGenTriggers( QuantifiersEngine* qe ); - ~InstStrategyAutoGenTriggers(){} + InstStrategyAutoGenTriggers(QuantifiersEngine* qe, QuantRelevance* qr); + ~InstStrategyAutoGenTriggers() {} + public: /** get auto-generated trigger */ inst::Trigger* getAutoGenTrigger( Node q ); @@ -113,6 +111,13 @@ public: } /** add pattern */ void addUserNoPattern( Node q, Node pat ); + + private: + /** + * Pointer to the module that computes relevance of quantifiers, which is + * owned by the instantiation engine that owns this class. + */ + QuantRelevance* d_quant_rel; };/* class InstStrategyAutoGenTriggers */ diff --git a/src/theory/quantifiers/ematching/instantiation_engine.cpp b/src/theory/quantifiers/ematching/instantiation_engine.cpp index d2650f01f..2fe28fc61 100644 --- a/src/theory/quantifiers/ematching/instantiation_engine.cpp +++ b/src/theory/quantifiers/ematching/instantiation_engine.cpp @@ -15,11 +15,12 @@ #include "theory/quantifiers/ematching/instantiation_engine.h" #include "options/quantifiers_options.h" -#include "theory/quantifiers/first_order_model.h" #include "theory/quantifiers/ematching/inst_strategy_e_matching.h" +#include "theory/quantifiers/ematching/trigger.h" +#include "theory/quantifiers/first_order_model.h" #include "theory/quantifiers/term_database.h" #include "theory/quantifiers/term_util.h" -#include "theory/quantifiers/ematching/trigger.h" +#include "theory/quantifiers_engine.h" #include "theory/theory_engine.h" using namespace std; @@ -35,7 +36,13 @@ InstantiationEngine::InstantiationEngine(QuantifiersEngine* qe) d_instStrategies(), d_isup(), d_i_ag(), - d_quants() { + d_quants(), + d_quant_rel(nullptr) +{ + if (options::relevantTriggers()) + { + d_quant_rel.reset(new quantifiers::QuantRelevance); + } if (options::eMatching()) { // these are the instantiation strategies for E-matching // user-provided patterns @@ -45,7 +52,8 @@ InstantiationEngine::InstantiationEngine(QuantifiersEngine* qe) } // auto-generated patterns - d_i_ag.reset(new InstStrategyAutoGenTriggers(d_quantEngine)); + d_i_ag.reset( + new InstStrategyAutoGenTriggers(d_quantEngine, d_quant_rel.get())); d_instStrategies.push_back(d_i_ag.get()); } } @@ -174,24 +182,32 @@ void InstantiationEngine::checkOwnership(Node q) } } -void InstantiationEngine::registerQuantifier( Node f ){ - if( d_quantEngine->hasOwnership( f, this ) ){ - //for( unsigned i=0; i<d_instStrategies.size(); ++i ){ - // d_instStrategies[i]->registerQuantifier( f ); - //} - //take into account user patterns - if( f.getNumChildren()==3 ){ - Node subsPat = - d_quantEngine->getTermUtil()->substituteBoundVariablesToInstConstants( - f[2], f); - //add patterns - for( int i=0; i<(int)subsPat.getNumChildren(); i++ ){ - //Notice() << "Add pattern " << subsPat[i] << " for " << f << std::endl; - if( subsPat[i].getKind()==INST_PATTERN ){ - addUserPattern( f, subsPat[i] ); - }else if( subsPat[i].getKind()==INST_NO_PATTERN ){ - addUserNoPattern( f, subsPat[i] ); - } +void InstantiationEngine::registerQuantifier(Node q) +{ + if (!d_quantEngine->hasOwnership(q, this)) + { + return; + } + if (d_quant_rel) + { + d_quant_rel->registerQuantifier(q); + } + // take into account user patterns + if (q.getNumChildren() == 3) + { + Node subsPat = + d_quantEngine->getTermUtil()->substituteBoundVariablesToInstConstants( + q[2], q); + // add patterns + for (const Node& p : subsPat) + { + if (p.getKind() == INST_PATTERN) + { + addUserPattern(q, p); + } + else if (p.getKind() == INST_NO_PATTERN) + { + addUserNoPattern(q, p); } } } diff --git a/src/theory/quantifiers/ematching/instantiation_engine.h b/src/theory/quantifiers/ematching/instantiation_engine.h index cd82e67a3..26fc3767b 100644 --- a/src/theory/quantifiers/ematching/instantiation_engine.h +++ b/src/theory/quantifiers/ematching/instantiation_engine.h @@ -14,13 +14,13 @@ #include "cvc4_private.h" -#ifndef __CVC4__THEORY__QUANTIFIERS__INSTANTIATION_ENGINE_H -#define __CVC4__THEORY__QUANTIFIERS__INSTANTIATION_ENGINE_H +#ifndef CVC4__THEORY__QUANTIFIERS__INSTANTIATION_ENGINE_H +#define CVC4__THEORY__QUANTIFIERS__INSTANTIATION_ENGINE_H -#include <memory> +#include <vector> -#include "theory/quantifiers_engine.h" -#include "theory/quantifiers/theory_quantifiers.h" +#include "theory/quantifiers/quant_relevance.h" +#include "theory/quantifiers/quant_util.h" namespace CVC4 { namespace theory { @@ -51,8 +51,6 @@ public: virtual int process( Node f, Theory::Effort effort, int e ) = 0; /** identify */ virtual std::string identify() const { return std::string("Unknown"); } - /** register quantifier */ - //virtual void registerQuantifier( Node q ) {} };/* class InstStrategy */ class InstantiationEngine : public QuantifiersModule { @@ -64,7 +62,6 @@ class InstantiationEngine : public QuantifiersModule { /** auto gen triggers; only kept for destructor cleanup */ std::unique_ptr<InstStrategyAutoGenTriggers> d_i_ag; - typedef context::CDHashMap<Node, bool, NodeHashFunction> BoolMap; /** current processing quantified formulas */ std::vector<Node> d_quants; @@ -89,10 +86,14 @@ class InstantiationEngine : public QuantifiersModule { void addUserNoPattern(Node q, Node pat); /** Identify this module */ std::string identify() const override { return "InstEngine"; } + + private: + /** for computing relevance of quantifiers */ + std::unique_ptr<QuantRelevance> d_quant_rel; }; /* class InstantiationEngine */ }/* CVC4::theory::quantifiers namespace */ }/* CVC4::theory namespace */ }/* CVC4 namespace */ -#endif /* __CVC4__THEORY__QUANTIFIERS__INSTANTIATION_ENGINE_H */ +#endif /* CVC4__THEORY__QUANTIFIERS__INSTANTIATION_ENGINE_H */ diff --git a/src/theory/quantifiers/ematching/trigger.cpp b/src/theory/quantifiers/ematching/trigger.cpp index 31bd1aa96..201aad3a0 100644 --- a/src/theory/quantifiers/ematching/trigger.cpp +++ b/src/theory/quantifiers/ematching/trigger.cpp @@ -232,8 +232,8 @@ Trigger* Trigger::mkTrigger( QuantifiersEngine* qe, Node f, std::vector< Node >& << std::endl; std::map<Node, std::vector<Node> > ho_apps; HigherOrderTrigger::collectHoVarApplyTerms(f, trNodes, ho_apps); - Trace("trigger") << "...got " << ho_apps.size() - << " higher-order applications." << std::endl; + Trace("trigger-debug") << "...got " << ho_apps.size() + << " higher-order applications." << std::endl; Trigger* t; if (!ho_apps.empty()) { @@ -488,10 +488,15 @@ void Trigger::collectPatTerms2( Node q, Node n, std::map< Node, std::vector< Nod // if child was not already removed if( tinfo.find( added2[i] )!=tinfo.end() ){ if( tstrt==quantifiers::TRIGGER_SEL_MAX || ( tstrt==quantifiers::TRIGGER_SEL_MIN_SINGLE_MAX && !nu_single ) ){ - //discard all subterms - Trace("auto-gen-trigger-debug2") << "......remove it." << std::endl; - visited[ added2[i] ].clear(); - tinfo.erase( added2[i] ); + // discard all subterms + // do not remove if it has smaller weight + if (tinfo[nu].d_weight <= tinfo[added2[i]].d_weight) + { + Trace("auto-gen-trigger-debug2") + << "......remove it." << std::endl; + visited[added2[i]].clear(); + tinfo.erase(added2[i]); + } }else{ if( tinfo[ nu ].d_fv.size()==tinfo[ added2[i] ].d_fv.size() ){ if (tinfo[nu].d_weight >= tinfo[added2[i]].d_weight) @@ -548,21 +553,11 @@ int Trigger::getTriggerWeight( Node n ) { { return 0; } - else if (isAtomicTrigger(n)) + if (isAtomicTrigger(n)) { return 1; - }else{ - if( options::relationalTriggers() ){ - if( isRelationalTrigger( n ) ){ - for( unsigned i=0; i<2; i++ ){ - if( n[i].getKind()==INST_CONSTANT && !quantifiers::TermUtil::hasInstConstAttr( n[1-i] ) ){ - return 0; - } - } - } - } - return 2; } + return 2; } bool Trigger::isLocalTheoryExt( Node n, std::vector< Node >& vars, std::vector< Node >& patTerms ) { diff --git a/src/theory/quantifiers/ematching/trigger.h b/src/theory/quantifiers/ematching/trigger.h index 9a65f0c02..d47ea72ee 100644 --- a/src/theory/quantifiers/ematching/trigger.h +++ b/src/theory/quantifiers/ematching/trigger.h @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__THEORY__QUANTIFIERS__TRIGGER_H -#define __CVC4__THEORY__QUANTIFIERS__TRIGGER_H +#ifndef CVC4__THEORY__QUANTIFIERS__TRIGGER_H +#define CVC4__THEORY__QUANTIFIERS__TRIGGER_H #include <map> @@ -319,9 +319,12 @@ class Trigger { static bool isPureTheoryTrigger( Node n ); /** get trigger weight * - * Returns 0 for triggers that are easy to process and 1 otherwise. - * A trigger is easy to process if it is an atomic trigger, or a relational - * trigger of the form x ~ g for ~ \in { =, >=, > }. + * Intutively, this function classifies how difficult it is to handle the + * trigger term n, where the smaller the value, the easier. + * + * Returns 0 for triggers that are APPLY_UF terms. + * Returns 1 for other triggers whose kind is atomic. + * Returns 2 otherwise. */ static int getTriggerWeight( Node n ); /** Returns whether n is a trigger term with a local theory extension @@ -464,4 +467,4 @@ public: }/* CVC4::theory namespace */ }/* CVC4 namespace */ -#endif /* __CVC4__THEORY__QUANTIFIERS__TRIGGER_H */ +#endif /* CVC4__THEORY__QUANTIFIERS__TRIGGER_H */ |