From 9e26baaaa717a5075984c63878e8bc1aa4e78b16 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 9 May 2019 09:33:22 -0500 Subject: Fixes for relational triggers (#2967) --- src/options/quantifiers_options.toml | 2 +- .../quantifiers/ematching/candidate_generator.cpp | 6 +- .../quantifiers/ematching/inst_match_generator.cpp | 100 ++++++++++++++------- .../ematching/inst_strategy_e_matching.cpp | 5 +- src/theory/quantifiers/ematching/trigger.cpp | 31 +++---- src/theory/quantifiers/ematching/trigger.h | 9 +- src/theory/quantifiers/instantiate.cpp | 2 +- src/theory/quantifiers/term_database.cpp | 14 ++- src/theory/quantifiers/term_database.h | 2 +- 9 files changed, 106 insertions(+), 65 deletions(-) (limited to 'src') diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml index 0a69178b3..66bd265d8 100644 --- a/src/options/quantifiers_options.toml +++ b/src/options/quantifiers_options.toml @@ -247,7 +247,7 @@ header = "options/quantifiers_options.h" category = "regular" long = "relational-triggers" type = "bool" - default = "false" + default = "true" read_only = true help = "choose relational triggers such as x = f(y), x >= f(y)" 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/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(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_strategy_e_matching.cpp b/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp index 8f671fb55..ce328df2e 100644 --- a/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp +++ b/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp @@ -325,7 +325,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{ 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 > 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 f276585d6..d47ea72ee 100644 --- a/src/theory/quantifiers/ematching/trigger.h +++ b/src/theory/quantifiers/ematching/trigger.h @@ -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 diff --git a/src/theory/quantifiers/instantiate.cpp b/src/theory/quantifiers/instantiate.cpp index 623db032a..8bd39c241 100644 --- a/src/theory/quantifiers/instantiate.cpp +++ b/src/theory/quantifiers/instantiate.cpp @@ -221,7 +221,7 @@ bool Instantiate::addInstantiation( { for (Node& t : terms) { - if (!d_term_db->isTermEligibleForInstantiation(t, q, true)) + if (!d_term_db->isTermEligibleForInstantiation(t, q)) { return false; } diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index abb84ccd7..c4b10eb6f 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -907,7 +907,8 @@ bool TermDb::hasTermCurrent( Node n, bool useMode ) { } } -bool TermDb::isTermEligibleForInstantiation( TNode n, TNode f, bool print ) { +bool TermDb::isTermEligibleForInstantiation(TNode n, TNode f) +{ if( options::lteRestrictInstClosure() ){ //has to be both in inst closure and in ground assertions if( !isInstClosure( n ) ){ @@ -937,7 +938,9 @@ bool TermDb::isTermEligibleForInstantiation( TNode n, TNode f, bool print ) { } } } - return true; + // it cannot have instantiation constants, which originate from + // counterexample-guided instantiation strategies. + return !TermUtil::hasInstConstAttr(n); } Node TermDb::getEligibleTermInEqc( TNode r ) { @@ -949,11 +952,14 @@ Node TermDb::getEligibleTermInEqc( TNode r ) { Node h; eq::EqualityEngine* ee = d_quantEngine->getActiveEqualityEngine(); eq::EqClassIterator eqc_i = eq::EqClassIterator( r, ee ); - while( h.isNull() && !eqc_i.isFinished() ){ + while (!eqc_i.isFinished()) + { TNode n = (*eqc_i); ++eqc_i; - if( hasTermCurrent( n ) ){ + if (isTermEligibleForInstantiation(n, TNode::null())) + { h = n; + break; } } d_term_elig_eqc[r] = h; diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h index 148a18958..cd5c27f0d 100644 --- a/src/theory/quantifiers/term_database.h +++ b/src/theory/quantifiers/term_database.h @@ -277,7 +277,7 @@ class TermDb : public QuantifiersUtil { */ bool hasTermCurrent(Node n, bool useMode = true); /** is term eligble for instantiation? */ - bool isTermEligibleForInstantiation(TNode n, TNode f, bool print = false); + bool isTermEligibleForInstantiation(TNode n, TNode f); /** get eligible term in equivalence class of r */ Node getEligibleTermInEqc(TNode r); /** is r a inst closure node? -- cgit v1.2.3