From 2abcda1cfcb0c6388c00d65f8a6b3e63de9d96df Mon Sep 17 00:00:00 2001 From: ajreynol Date: Wed, 30 Mar 2016 14:06:27 -0500 Subject: [PATCH] Updates to E-matching to avoid entailed instantiations earlier. Minor updates to datatypes lemmas, other minor changes. --- src/options/quantifiers_options | 5 - src/smt/smt_engine.cpp | 10 ++ src/theory/datatypes/theory_datatypes.cpp | 37 +++--- .../quantifiers/candidate_generator.cpp | 37 ++++-- src/theory/quantifiers/candidate_generator.h | 4 + .../quantifiers/inst_match_generator.cpp | 108 ++++++++-------- src/theory/quantifiers/inst_match_generator.h | 4 +- .../quantifiers/inst_strategy_e_matching.cpp | 39 ++++-- .../quantifiers/inst_strategy_e_matching.h | 2 + src/theory/quantifiers/quant_util.cpp | 17 +++ src/theory/quantifiers/quant_util.h | 1 + .../quantifiers/quantifiers_rewriter.cpp | 4 +- src/theory/quantifiers/trigger.cpp | 122 ++++++++++-------- src/theory/quantifiers/trigger.h | 8 +- 14 files changed, 231 insertions(+), 167 deletions(-) diff --git a/src/options/quantifiers_options b/src/options/quantifiers_options index d001684a0..04b6e6813 100644 --- a/src/options/quantifiers_options +++ b/src/options/quantifiers_options @@ -37,11 +37,6 @@ option condVarSplitQuantAgg --cond-var-split-agg-quant bool :default false aggressive split quantified formulas that lead to variable eliminations option iteDtTesterSplitQuant --ite-dtt-split-quant bool :read-write :default false split ites with dt testers as conditions -# Whether to CNF quantifier bodies -# option cnfQuant --cnf-quant bool :default false -# apply CNF conversion to quantified formulas -option nnfQuant --nnf-quant bool :default true - apply NNF conversion to quantified formulas # Whether to pre-skolemize quantifier bodies. # For example, forall x. ( P( x ) => (exists y. f( y ) = x) ) will be rewritten to # forall x. P( x ) => f( S( x ) ) = x diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 98ed9c4fd..784d82228 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -552,6 +552,11 @@ class SmtEnginePrivate : public NodeManagerListener { */ unsigned d_simplifyAssertionsDepth; + /** whether certain preprocess steps are necessary */ + bool d_needsExpandDefs; + bool d_needsRewriteBoolTerms; + bool d_needsConstrainSubTypes; + public: /** * Map from skolem variables to index in d_assertions containing @@ -679,6 +684,9 @@ public: d_abstractValueMap(&d_fakeContext), d_abstractValues(), d_simplifyAssertionsDepth(0), + d_needsExpandDefs(true), + d_needsRewriteBoolTerms(true), + d_needsConstrainSubTypes(true), //TODO d_iteSkolemMap(), d_iteRemover(smt.d_userContext), d_pbsProcessor(smt.d_userContext), @@ -3860,6 +3868,7 @@ void SmtEnginePrivate::processAssertions() { Debug("smt") << " d_assertions : " << d_assertions.size() << endl; + dumpAssertions("pre-constrain-subtypes", d_assertions); { // Any variables of subtype types need to be constrained properly. @@ -4194,6 +4203,7 @@ void SmtEnginePrivate::processAssertions() { Trace("smt-proc") << "SmtEnginePrivate::processAssertions() end" << endl; dumpAssertions("post-everything", d_assertions); + //set instantiation level of everything to zero if( options::instLevelInputOnly() && options::instMaxLevel()!=-1 ){ diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index 8123fe39c..f044ff401 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -375,15 +375,23 @@ void TheoryDatatypes::flushPendingFacts(){ Trace("dt-lemma-debug") << "Trivial explanation." << std::endl; }else{ Trace("dt-lemma-debug") << "Get explanation..." << std::endl; - Node ee_exp; + std::vector< TNode > assumptions; //if( options::dtRExplainLemmas() ){ - ee_exp = explain( exp ); + explain( exp, assumptions ); //}else{ // ee_exp = exp; //} - Trace("dt-lemma-debug") << "Explanation : " << ee_exp << std::endl; - lem = NodeManager::currentNM()->mkNode( OR, ee_exp.negate(), fact ); - lem = Rewriter::rewrite( lem ); + //Trace("dt-lemma-debug") << "Explanation : " << ee_exp << std::endl; + if( assumptions.empty() ){ + lem = fact; + }else{ + std::vector< Node > children; + for( unsigned i=0; imkNode( OR, children ); + } } Trace("dt-lemma") << "Datatypes lemma : " << lem << std::endl; if( doSendLemma( lem ) ){ @@ -1941,14 +1949,7 @@ bool TheoryDatatypes::mustCommunicateFact( Node n, Node exp ){ bool addLemma = false; if( options::dtInferAsLemmas() && exp!=d_true ){ addLemma = true; - }else if( n.getKind()==EQUAL || n.getKind()==IFF ){ - /* - for( unsigned i=0; i<2; i++ ){ - if( !n[i].isVar() && n[i].getKind()!=APPLY_SELECTOR_TOTAL && n[i].getKind()!=APPLY_CONSTRUCTOR ){ - addLemma = true; - } - } - */ + }else if( n.getKind()==EQUAL ){ TypeNode tn = n[0].getType(); if( !DatatypesRewriter::isTypeDatatype( tn ) ){ addLemma = true; @@ -1956,15 +1957,7 @@ bool TheoryDatatypes::mustCommunicateFact( Node n, Node exp ){ const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype(); addLemma = dt.involvesExternalType(); } - //for( int j=0; j<(int)n[1].getNumChildren(); j++ ){ - // if( !DatatypesRewriter::isTermDatatype( n[1][j] ) ){ - // addLemma = true; - // break; - // } - //} - }else if( n.getKind()==LEQ ){ - addLemma = true; - }else if( n.getKind()==OR ){ + }else if( n.getKind()==LEQ || n.getKind()==IFF || n.getKind()==OR ){ addLemma = true; } if( addLemma ){ diff --git a/src/theory/quantifiers/candidate_generator.cpp b/src/theory/quantifiers/candidate_generator.cpp index 1f68884b6..e5cc34f7e 100644 --- a/src/theory/quantifiers/candidate_generator.cpp +++ b/src/theory/quantifiers/candidate_generator.cpp @@ -62,6 +62,7 @@ CandidateGeneratorQE::CandidateGeneratorQE( QuantifiersEngine* qe, Node op ) : d_op( op ), d_qe( qe ), d_term_iter( -1 ){ Assert( !d_op.isNull() ); } + void CandidateGeneratorQE::resetInstantiationRound(){ d_term_iter_limit = d_qe->getTermDatabase()->getNumGroundTerms( d_op ); } @@ -71,20 +72,20 @@ void CandidateGeneratorQE::reset( Node eqc ){ if( eqc.isNull() ){ d_mode = cand_term_db; }else{ - //create an equivalence class iterator in eq class eqc - //d_qe->getEqualityQuery()->getEquivalenceClass( eqc, d_eqc ); - - eq::EqualityEngine* ee = d_qe->getEqualityQuery()->getEngine(); - if( ee->hasTerm( eqc ) ){ - Node rep = ee->getRepresentative( eqc ); - d_eqc_iter = eq::EqClassIterator( rep, ee ); - d_mode = cand_term_eqc; + if( isExcludedEqc( eqc ) ){ + d_mode = cand_term_none; }else{ - d_n = eqc; - d_mode = cand_term_ident; + eq::EqualityEngine* ee = d_qe->getEqualityQuery()->getEngine(); + if( ee->hasTerm( eqc ) ){ + //create an equivalence class iterator in eq class eqc + Node rep = ee->getRepresentative( eqc ); + d_eqc_iter = eq::EqClassIterator( rep, ee ); + d_mode = cand_term_eqc; + }else{ + d_n = eqc; + d_mode = cand_term_ident; + } } - //a should be in its equivalence class - //Assert( std::find( eqc.begin(), eqc.end(), a )!=eqc.end() ); } } bool CandidateGeneratorQE::isLegalOpCandidate( Node n ) { @@ -98,17 +99,26 @@ bool CandidateGeneratorQE::isLegalOpCandidate( Node n ) { Node CandidateGeneratorQE::getNextCandidate(){ if( d_mode==cand_term_db ){ + 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 ); d_term_iter++; if( isLegalCandidate( n ) ){ if( d_qe->getTermDatabase()->hasTermCurrent( n ) ){ - return n; + if( d_exclude_eqc.empty() ){ + return n; + }else{ + Node r = d_qe->getEqualityQuery()->getRepresentative( n ); + if( d_exclude_eqc.find( r )==d_exclude_eqc.end() ){ + return n; + } + } } } } }else if( d_mode==cand_term_eqc ){ + Debug("cand-gen-qe") << "...get next candidate in eqc" << std::endl; while( !d_eqc_iter.isFinished() ){ Node n = *d_eqc_iter; ++d_eqc_iter; @@ -117,6 +127,7 @@ Node CandidateGeneratorQE::getNextCandidate(){ } } }else if( d_mode==cand_term_ident ){ + Debug("cand-gen-qe") << "...get next candidate identity" << std::endl; if( !d_n.isNull() ){ Node n = d_n; d_n = Node::null(); diff --git a/src/theory/quantifiers/candidate_generator.h b/src/theory/quantifiers/candidate_generator.h index d86891de7..9d8e318aa 100644 --- a/src/theory/quantifiers/candidate_generator.h +++ b/src/theory/quantifiers/candidate_generator.h @@ -88,10 +88,12 @@ private: cand_term_db, cand_term_ident, cand_term_eqc, + cand_term_none, }; short d_mode; bool isLegalOpCandidate( Node n ); Node d_n; + std::map< Node, bool > d_exclude_eqc; public: CandidateGeneratorQE( QuantifiersEngine* qe, Node op ); ~CandidateGeneratorQE() throw() {} @@ -99,6 +101,8 @@ public: void resetInstantiationRound(); void reset( Node eqc ); Node getNextCandidate(); + void excludeEqc( Node r ) { d_exclude_eqc[r] = true; } + bool isExcludedEqc( Node r ) { return d_exclude_eqc.find( r )!=d_exclude_eqc.end(); } }; class CandidateGeneratorQELitEq : public CandidateGenerator diff --git a/src/theory/quantifiers/inst_match_generator.cpp b/src/theory/quantifiers/inst_match_generator.cpp index 41c62192f..7d732ab8a 100644 --- a/src/theory/quantifiers/inst_match_generator.cpp +++ b/src/theory/quantifiers/inst_match_generator.cpp @@ -40,7 +40,6 @@ InstMatchGenerator::InstMatchGenerator( Node pat ){ d_match_pattern_type = pat.getType(); d_next = NULL; d_matchPolicy = MATCH_GEN_DEFAULT; - d_eq_class_rel = false; } InstMatchGenerator::InstMatchGenerator() { @@ -59,7 +58,7 @@ void InstMatchGenerator::setActiveAdd(bool val){ void InstMatchGenerator::initialize( Node q, QuantifiersEngine* qe, std::vector< InstMatchGenerator * > & gens ){ if( !d_pattern.isNull() ){ - Debug("inst-match-gen") << "Pattern term is " << d_pattern << std::endl; + Trace("inst-match-gen") << "Initialize, pattern term is " << d_pattern << std::endl; if( d_match_pattern.getKind()==NOT ){ //we want to add the children of the NOT d_match_pattern = d_pattern[0]; @@ -67,29 +66,23 @@ void InstMatchGenerator::initialize( Node q, QuantifiersEngine* qe, std::vector< if( d_match_pattern.getKind()==IFF || 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 - if( !quantifiers::TermDb::hasInstConstAttr(d_match_pattern[0]) || d_match_pattern[0].getKind()==INST_CONSTANT ){ - if( d_match_pattern[1].getKind()!=INST_CONSTANT ){ - Assert( quantifiers::TermDb::hasInstConstAttr(d_match_pattern[1]) ); - Node mp = d_match_pattern[1]; - //swap sides - Node pat = d_pattern; - if(d_match_pattern.getKind()==GEQ){ - d_pattern = NodeManager::currentNM()->mkNode( kind::GT, d_match_pattern[1], d_match_pattern[0] ); - d_pattern = d_pattern.negate(); - }else{ - d_pattern = NodeManager::currentNM()->mkNode( d_match_pattern.getKind(), d_match_pattern[1], d_match_pattern[0] ); - } - d_pattern = pat.getKind()==NOT ? d_pattern.negate() : d_pattern; - d_match_pattern = mp; - } - }else if( !quantifiers::TermDb::hasInstConstAttr(d_match_pattern[1]) || d_match_pattern[1].getKind()==INST_CONSTANT ){ - if( d_match_pattern[0].getKind()!=INST_CONSTANT ){ - Assert( quantifiers::TermDb::hasInstConstAttr(d_match_pattern[0]) ); - if( d_pattern.getKind()!=NOT ){ //TEMPORARY until we do better implementation of disequality matching - d_match_pattern = d_match_pattern[0]; - }else if( d_match_pattern[1].getKind()==INST_CONSTANT ){ - d_match_pattern = d_match_pattern[0]; + for( unsigned i=0; i<2; i++ ){ + if( !quantifiers::TermDb::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 ); + } + } + d_eq_class_rel = mpo; + d_match_pattern = mp; } + break; } } }else if( d_match_pattern.getKind()==APPLY_SELECTOR_TOTAL && d_match_pattern[0].getKind()==INST_CONSTANT && options::purifyDtTriggers() ){ @@ -100,7 +93,6 @@ void InstMatchGenerator::initialize( Node q, QuantifiersEngine* qe, std::vector< d_match_pattern_op = qe->getTermDatabase()->getMatchOperator( d_match_pattern ); //now, collect children of d_match_pattern - //int childMatchPolicy = MATCH_GEN_DEFAULT; for( unsigned i=0; iexcludeEqc( 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 ){ Expr selectorExpr = qe->getTermDatabase()->getMatchOperator( d_pattern ).toExpr(); size_t selectorIndex = Datatype::cindexOf(selectorExpr); @@ -140,6 +140,7 @@ void InstMatchGenerator::initialize( Node q, QuantifiersEngine* qe, std::vector< d_cg = new CandidateGeneratorQEAll( qe, d_match_pattern ); } }else if( d_match_pattern.getKind()==EQUAL || d_match_pattern.getKind()==IFF ){ + Assert( d_match_pattern[0].getKind()==INST_CONSTANT && d_match_pattern[1].getKind()==INST_CONSTANT ); //we will be producing candidates via literal matching heuristics if( d_pattern.getKind()!=NOT ){ //candidates will be all equalities @@ -148,26 +149,6 @@ void InstMatchGenerator::initialize( Node q, QuantifiersEngine* qe, std::vector< //candidates will be all disequalities d_cg = new inst::CandidateGeneratorQELitDeq( qe, d_match_pattern ); } - }else if( d_pattern.getKind()==EQUAL || d_pattern.getKind()==IFF || - d_pattern.getKind()==GEQ || d_pattern.getKind()==GT || d_pattern.getKind()==NOT ){ - Assert( d_matchPolicy==MATCH_GEN_DEFAULT ); - if( d_pattern.getKind()==NOT ){ - if (d_pattern[0][1].getKind()!=INST_CONSTANT) { - Unimplemented("Disequal generator unimplemented"); - }else{ - d_eq_class = d_pattern[0][1]; - } - }else{ - //store the equivalence class that we will call d_cg->reset( ... ) on - d_eq_class = d_pattern[1]; - } - d_eq_class_rel = true; - Assert( Trigger::isAtomicTrigger( d_match_pattern ) ); - //we are matching only in a particular equivalence class - d_cg = new inst::CandidateGeneratorQE( qe, d_match_pattern_op ); - }else if( Trigger::isAtomicTrigger( d_match_pattern ) ){ - //we will be scanning lists trying to find d_match_pattern.getOperator() - d_cg = new inst::CandidateGeneratorQE( qe, d_match_pattern_op ); }else{ d_cg = new CandidateGeneratorQueue; Trace("inst-match-gen-warn") << "(?) Unknown matching pattern is " << d_match_pattern << std::endl; @@ -231,8 +212,8 @@ bool InstMatchGenerator::getMatch( Node f, Node t, InstMatch& m, QuantifiersEngi } } //for relational matching - }else if( d_eq_class_rel && d_eq_class.getKind()==INST_CONSTANT ){ - int v = d_eq_class.getAttribute(InstVarNumAttribute()); + }else 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; Node pat = d_pattern.getKind()==NOT ? d_pattern[0] : d_pattern; @@ -313,20 +294,22 @@ void InstMatchGenerator::resetInstantiationRound( QuantifiersEngine* qe ){ void InstMatchGenerator::reset( Node eqc, QuantifiersEngine* qe ){ eqc = qe->getEqualityQuery()->getRepresentative( eqc ); Trace("matching-debug2") << this << " reset " << eqc << "." << std::endl; - if( !eqc.isNull() ){ + if( !d_eq_class_rel.isNull() && d_eq_class_rel.getKind()!=INST_CONSTANT ){ + d_eq_class = d_eq_class_rel; + }else if( !eqc.isNull() ){ d_eq_class = eqc; } //we have a specific equivalence class in mind //we are producing matches for f(E) ~ t, where E is a non-ground vector of terms, and t is a ground term //just look in equivalence class of the RHS - d_cg->reset( d_eq_class_rel ? Node::null() : d_eq_class ); + d_cg->reset( d_eq_class ); d_needsReset = false; } bool InstMatchGenerator::getNextMatch( Node f, InstMatch& m, QuantifiersEngine* qe ){ if( d_needsReset ){ Trace("matching") << "Reset not done yet, must do the reset..." << std::endl; - reset( d_eq_class_rel ? Node::null() : d_eq_class, qe ); + reset( d_eq_class, qe ); } m.d_matched = Node::null(); Trace("matching") << this << " " << d_match_pattern << " get next match " << m << " in eq class " << d_eq_class << std::endl; @@ -346,7 +329,7 @@ bool InstMatchGenerator::getNextMatch( Node f, InstMatch& m, QuantifiersEngine* if( !success ){ Trace("matching") << this << " failed, reset " << d_eq_class << std::endl; //we failed, must reset - reset( d_eq_class_rel ? Node::null() : d_eq_class, qe ); + reset( d_eq_class, qe ); } return success; } @@ -696,6 +679,12 @@ int InstMatchGeneratorMulti::addTerm( Node q, Node t, QuantifiersEngine* qe ){ } InstMatchGeneratorSimple::InstMatchGeneratorSimple( Node q, Node pat ) : d_f( q ), d_match_pattern( pat ) { + if( d_match_pattern.getKind()==EQUAL || d_match_pattern.getKind()==IFF ){ + d_eqc = d_match_pattern[1]; + d_match_pattern = d_match_pattern[0]; + Assert( !quantifiers::TermDb::hasInstConstAttr( d_eqc ) ); + } + Assert( Trigger::isSimpleTrigger( d_match_pattern ) ); for( unsigned i=0; igetTermDatabase()->d_func_map_trie[ d_op ]) ); - return addedLemmas; + quantifiers::TermArgTrie* tat; + if( d_eqc.isNull() ){ + tat = qe->getTermDatabase()->getTermArgTrie( d_op ); + }else{ + tat = qe->getTermDatabase()->getTermArgTrie( d_eqc, d_op ); + } + if( tat ){ + addInstantiations( m, qe, addedLemmas, 0, tat ); + return addedLemmas; + }else{ + return 0; + } } void InstMatchGeneratorSimple::addInstantiations( InstMatch& m, QuantifiersEngine* qe, int& addedLemmas, int argIndex, quantifiers::TermArgTrie* tat ){ diff --git a/src/theory/quantifiers/inst_match_generator.h b/src/theory/quantifiers/inst_match_generator.h index 75adeb2d8..58531f3e6 100644 --- a/src/theory/quantifiers/inst_match_generator.h +++ b/src/theory/quantifiers/inst_match_generator.h @@ -64,7 +64,7 @@ protected: InstMatchGenerator* d_next; /** eq class */ Node d_eq_class; - bool d_eq_class_rel; + Node d_eq_class_rel; /** variable numbers */ std::map< int, int > d_var_num; /** initialize pattern */ @@ -211,6 +211,8 @@ private: Node d_f; /** match term */ Node d_match_pattern; + /** equivalence class */ + Node d_eqc; /** match pattern arg types */ std::vector< TypeNode > d_match_pattern_arg_types; /** operator */ diff --git a/src/theory/quantifiers/inst_strategy_e_matching.cpp b/src/theory/quantifiers/inst_strategy_e_matching.cpp index 111eab116..fac83ec5c 100644 --- a/src/theory/quantifiers/inst_strategy_e_matching.cpp +++ b/src/theory/quantifiers/inst_strategy_e_matching.cpp @@ -246,29 +246,32 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f ){ d_patTerms[1][f].clear(); bool ntrivTriggers = options::relationalTriggers(); std::vector< Node > patTermsF; + std::map< Node, int > reqPol; //well-defined function: can assume LHS is only trigger if( options::quantFunWellDefined() ){ Node hd = TermDb::getFunDefHead( f ); if( !hd.isNull() ){ hd = d_quantEngine->getTermDatabase()->getInstConstantNode( hd, f ); patTermsF.push_back( hd ); + reqPol[hd] = 0; } } //otherwise, use algorithm for collecting pattern terms if( patTermsF.empty() ){ Node bd = d_quantEngine->getTermDatabase()->getInstConstantBody( f ); - Trigger::collectPatTerms( d_quantEngine, f, bd, patTermsF, d_tr_strategy, d_user_no_gen[f], true ); + Trigger::collectPatTerms( d_quantEngine, f, bd, patTermsF, d_tr_strategy, d_user_no_gen[f], reqPol, true ); Trace("auto-gen-trigger-debug") << "Collected pat terms for " << bd << ", no-patterns : " << d_user_no_gen[f].size() << std::endl; if( ntrivTriggers ){ sortTriggers st; std::sort( patTermsF.begin(), patTermsF.end(), st ); } for( unsigned i=0; i > varContains; std::map< Node, bool > vcMap; std::map< Node, bool > rmPatTermsF; @@ -284,20 +287,34 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f ){ } int curr_w = Trigger::getTriggerWeight( patTermsF[i] ); if( ntrivTriggers && !newVar && last_weight!=-1 && curr_w>last_weight ){ - Trace("auto-gen-trigger-debug") << "Exclude expendible non-trivial trigger : " << patTermsF[i] << std::endl; + Trace("auto-gen-trigger-debug") << "...exclude expendible non-trivial trigger : " << patTermsF[i] << std::endl; rmPatTermsF[patTermsF[i]] = true; }else{ last_weight = curr_w; } } for( std::map< Node, std::vector< Node > >::iterator it = varContains.begin(); it != varContains.end(); ++it ){ - if( rmPatTermsF.find( it->first )==rmPatTermsF.end() ){ - if( it->second.size()==f[0].getNumChildren() && ( options::pureThTriggers() || !Trigger::isPureTheoryTrigger( it->first ) ) ){ - d_patTerms[0][f].push_back( it->first ); - d_is_single_trigger[ it->first ] = true; + Node pat = it->first; + Trace("auto-gen-trigger-debug") << "...processing pattern " << pat << std::endl; + if( rmPatTermsF.find( pat )==rmPatTermsF.end() ){ + //process the pattern: if it has a required polarity, consider it + if( options::instNoEntail() ){ + Assert( reqPol.find( pat )!=reqPol.end() ); + int rpol = reqPol[pat]; + Trace("auto-gen-trigger-debug") << "...required polarity for " << pat << " is " << rpol << std::endl; + if( rpol!=0 ){ + Assert( pat.getType().isBoolean() ); + if( pat.getKind()==APPLY_UF ){ + pat = NodeManager::currentNM()->mkNode( IFF, pat, NodeManager::currentNM()->mkConst( rpol==-1 ) ).negate(); + } + } + } + if( it->second.size()==f[0].getNumChildren() && ( options::pureThTriggers() || !Trigger::isPureTheoryTrigger( pat ) ) ){ + d_patTerms[0][f].push_back( pat ); + d_is_single_trigger[ pat ] = true; }else{ - d_patTerms[1][f].push_back( it->first ); - d_is_single_trigger[ it->first ] = false; + d_patTerms[1][f].push_back( pat ); + d_is_single_trigger[ pat ] = false; } } } @@ -332,7 +349,7 @@ 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( int i=0; i<(int)patTerms.size(); i++ ){ + for( unsigned i=0; igetQuantifierRelevance()->getNumQuantifiersForSymbol( patTerms[i].getOperator() ) << ")" << std::endl; } diff --git a/src/theory/quantifiers/inst_strategy_e_matching.h b/src/theory/quantifiers/inst_strategy_e_matching.h index 4e7afad5d..04f35a3ed 100644 --- a/src/theory/quantifiers/inst_strategy_e_matching.h +++ b/src/theory/quantifiers/inst_strategy_e_matching.h @@ -73,6 +73,8 @@ private: std::map< Node, int > d_counter; /** single, multi triggers for each quantifier */ std::map< Node, std::vector< Node > > d_patTerms[2]; + std::map< Node, std::map< Node, bool > > d_patReqPol; + /** information about triggers */ std::map< Node, bool > d_is_single_trigger; std::map< Node, bool > d_single_trigger_gen; std::map< Node, bool > d_made_multi_trigger; diff --git a/src/theory/quantifiers/quant_util.cpp b/src/theory/quantifiers/quant_util.cpp index 1f1efa2a8..eb92b0f70 100644 --- a/src/theory/quantifiers/quant_util.cpp +++ b/src/theory/quantifiers/quant_util.cpp @@ -377,3 +377,20 @@ void QuantPhaseReq::getPolarity( Node n, int child, bool hasPol, bool pol, bool& newPol = pol; } } + +void QuantPhaseReq::getEntailPolarity( Node n, int child, bool hasPol, bool pol, bool& newHasPol, bool& newPol ) { + if( n.getKind()==AND || n.getKind()==OR ){ + newHasPol = hasPol && pol==( n.getKind()==AND ); + newPol = pol; + }else if( n.getKind()==IMPLIES ){ + newHasPol = hasPol && !pol; + newPol = child==0 ? !pol : pol; + }else if( n.getKind()==NOT ){ + newHasPol = hasPol; + newPol = !pol; + }else{ + newHasPol = false; + newPol = pol; + } +} + diff --git a/src/theory/quantifiers/quant_util.h b/src/theory/quantifiers/quant_util.h index 31743d352..073777014 100644 --- a/src/theory/quantifiers/quant_util.h +++ b/src/theory/quantifiers/quant_util.h @@ -93,6 +93,7 @@ public: std::map< Node, Node > d_phase_reqs_equality_term; static void getPolarity( Node n, int child, bool hasPol, bool pol, bool& newHasPol, bool& newPol ); + static void getEntailPolarity( Node n, int child, bool hasPol, bool pol, bool& newHasPol, bool& newPol ); }; diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp index b0340d630..9e0e40911 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.cpp +++ b/src/theory/quantifiers/quantifiers_rewriter.cpp @@ -324,7 +324,7 @@ Node QuantifiersRewriter::computeNNF( Node body ){ }else if( isLiteral( body[0] ) ){ return body; }else{ - std::vector< Node > children; + std::vector< Node > children; Kind k = body[0].getKind(); if( body[0].getKind()==OR || body[0].getKind()==AND ){ @@ -1546,7 +1546,7 @@ bool QuantifiersRewriter::doOperation( Node f, int computeOption, QAttributes& q }else if( computeOption==COMPUTE_AGGRESSIVE_MINISCOPING ){ return options::aggressiveMiniscopeQuant() && is_std; }else if( computeOption==COMPUTE_NNF ){ - return options::nnfQuant(); + return true; }else if( computeOption==COMPUTE_PROCESS_TERMS ){ return true; //return options::iteLiftQuant()!=ITE_LIFT_QUANT_MODE_NONE || options::iteCondVarSplitQuant(); diff --git a/src/theory/quantifiers/trigger.cpp b/src/theory/quantifiers/trigger.cpp index efffe10bd..79c677f1c 100644 --- a/src/theory/quantifiers/trigger.cpp +++ b/src/theory/quantifiers/trigger.cpp @@ -337,13 +337,19 @@ bool Trigger::isCbqiKind( Kind k ) { } bool Trigger::isSimpleTrigger( Node n ){ - if( isAtomicTrigger( n ) ){ - for( int i=0; i<(int)n.getNumChildren(); i++ ){ - if( n[i].getKind()!=INST_CONSTANT && quantifiers::TermDb::hasInstConstAttr(n[i]) ){ + Node t = n; + if( n.getKind()==IFF || n.getKind()==EQUAL ){ + if( !quantifiers::TermDb::hasInstConstAttr( n[1] ) ){ + t = n[0]; + } + } + if( isAtomicTrigger( t ) ){ + for( unsigned i=0; i& patMap, int tstrt, std::vector< Node >& exclude, bool pol, bool hasPol ){ - if( patMap.find( n )==patMap.end() ){ - patMap[ n ] = false; - if( tstrt==TS_MIN_TRIGGER ){ - if( n.getKind()==FORALL ){ - return false; - }else{ - bool retVal = false; +//store triggers in reqPol, indicating their polarity (if any) they must appear to falsify the quantified formula +bool Trigger::collectPatTerms2( Node f, Node n, std::map< Node, bool >& visited, int tstrt, std::vector< Node >& exclude, + std::map< Node, int >& reqPol, bool pol, bool hasPol, bool epol, bool hasEPol ){ + std::map< Node, bool >::iterator itv = visited.find( n ); + if( itv==visited.end() ){ + visited[ n ] = false; + Trace("auto-gen-trigger-debug2") << "Collect pat terms " << n << " " << pol << " " << hasPol << " " << epol << " " << hasEPol << std::endl; + bool retVal = false; + if( n.getKind()!=FORALL ){ + if( tstrt==TS_MIN_TRIGGER ){ for( unsigned i=0; isecond; } } @@ -493,42 +501,47 @@ bool Trigger::isLocalTheoryExt( Node n, std::vector< Node >& vars, std::vector< return true; } -void Trigger::collectPatTerms( QuantifiersEngine* qe, Node f, Node n, std::vector< Node >& patTerms, int tstrt, std::vector< Node >& exclude, bool filterInst ){ - std::map< Node, bool > patMap; +void Trigger::collectPatTerms( QuantifiersEngine* qe, Node f, Node n, std::vector< Node >& patTerms, int tstrt, std::vector< Node >& exclude, + std::map< Node, int >& reqPol, bool filterInst ){ + std::map< Node, bool > visited; if( filterInst ){ //immediately do not consider any term t for which another term is an instance of t std::vector< Node > patTerms2; - collectPatTerms( qe, f, n, patTerms2, TS_ALL, exclude, false ); + std::map< Node, int > reqPol2; + collectPatTerms( qe, f, n, patTerms2, TS_ALL, exclude, reqPol2, false ); std::vector< Node > temp; temp.insert( temp.begin(), patTerms2.begin(), patTerms2.end() ); qe->getTermDatabase()->filterInstances( temp ); if( temp.size()!=patTerms2.size() ){ Trace("trigger-filter-instance") << "Filtered an instance: " << std::endl; Trace("trigger-filter-instance") << "Old: "; - for( int i=0; i<(int)patTerms2.size(); i++ ){ + for( unsigned i=0; i::iterator it = patMap.begin(); it != patMap.end(); ++it ){ - if( it->second ){ + collectPatTerms2( f, n, visited, tstrt, exclude, reqPol, true, true, false, true ); + for( std::map< Node, int >::iterator it = reqPol.begin(); it != reqPol.end(); ++it ){ + if( visited[it->first] ){ patTerms.push_back( it->first ); } } @@ -611,9 +624,10 @@ Node Trigger::getInversion( Node n, Node x ) { void Trigger::getTriggerVariables( QuantifiersEngine* qe, Node icn, Node f, std::vector< Node >& t_vars ) { std::vector< Node > patTerms; + std::map< Node, int > reqPol; //collect all patterns from icn std::vector< Node > exclude; - collectPatTerms( qe, f, icn, patTerms, TS_ALL, exclude ); + collectPatTerms( qe, f, icn, patTerms, TS_ALL, exclude, reqPol ); //collect all variables from all patterns in patTerms, add to t_vars for( unsigned i=0; igetTermDatabase()->getVarContainsNode( f, patTerms[i], t_vars ); diff --git a/src/theory/quantifiers/trigger.h b/src/theory/quantifiers/trigger.h index 2ca2eb55d..22c4e5905 100644 --- a/src/theory/quantifiers/trigger.h +++ b/src/theory/quantifiers/trigger.h @@ -100,7 +100,7 @@ class Trigger { }; static void collectPatTerms( QuantifiersEngine* qe, Node f, Node n, std::vector< Node >& patTerms, int tstrt, - std::vector< Node >& exclude, + std::vector< Node >& exclude, std::map< Node, int >& reqPol, bool filterInst = false ); /** is usable trigger */ static bool isUsableTrigger( Node n, Node q ); @@ -140,9 +140,9 @@ private: static Node getIsUsableTrigger( Node n, Node f, bool pol = true, bool hasPol = false ); /** collect all APPLY_UF pattern terms for f in n */ - static bool collectPatTerms2( Node f, Node n, std::map< Node, bool >& patMap, - int tstrt, std::vector< Node >& exclude, - bool pol, bool hasPol ); + static bool collectPatTerms2( Node f, Node n, std::map< Node, bool >& visited, + int tstrt, std::vector< Node >& exclude, std::map< Node, int >& reqPol, + bool pol, bool hasPol, bool epol, bool hasEPol ); std::vector< Node > d_nodes; -- 2.30.2