diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-04-07 09:38:41 -0500 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-04-07 09:38:41 -0500 |
commit | 59b935c1af18ec51efacf87b0e45d9134d3aaa1e (patch) | |
tree | 57cee5cddf68999e20553ee9746f4a83183e8b99 | |
parent | 576d50ac7c13233a589771401537b587eb36361e (diff) |
Refactor trigger selection, revisions to --relational-trigger. Properly process non-standard user-provided triggers. Avoid entailed instantiations based on equality earlier. Refactor core addInstantiation method, add notification mechanism. Add optional argument to entailment checks. Fix bug for duplicate triggers.
-rw-r--r-- | src/theory/quantifiers/inst_match_generator.cpp | 4 | ||||
-rw-r--r-- | src/theory/quantifiers/inst_strategy_e_matching.cpp | 104 | ||||
-rw-r--r-- | src/theory/quantifiers/inst_strategy_e_matching.h | 1 | ||||
-rw-r--r-- | src/theory/quantifiers/macros.cpp | 2 | ||||
-rw-r--r-- | src/theory/quantifiers/quant_util.h | 2 | ||||
-rw-r--r-- | src/theory/quantifiers/quantifiers_rewriter.cpp | 26 | ||||
-rw-r--r-- | src/theory/quantifiers/term_database.cpp | 90 | ||||
-rw-r--r-- | src/theory/quantifiers/term_database.h | 13 | ||||
-rw-r--r-- | src/theory/quantifiers/trigger.cpp | 261 | ||||
-rw-r--r-- | src/theory/quantifiers/trigger.h | 33 | ||||
-rw-r--r-- | src/theory/quantifiers_engine.cpp | 170 | ||||
-rw-r--r-- | src/theory/quantifiers_engine.h | 14 | ||||
-rw-r--r-- | test/regress/regress0/quantifiers/Makefile.am | 3 | ||||
-rw-r--r-- | test/regress/regress0/quantifiers/double-pattern.smt2 | 6 |
14 files changed, 442 insertions, 287 deletions
diff --git a/src/theory/quantifiers/inst_match_generator.cpp b/src/theory/quantifiers/inst_match_generator.cpp index 34c7949d6..cfa4190e4 100644 --- a/src/theory/quantifiers/inst_match_generator.cpp +++ b/src/theory/quantifiers/inst_match_generator.cpp @@ -139,8 +139,8 @@ 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.getKind()==IFF ){ - Assert( d_match_pattern[0].getKind()==INST_CONSTANT && d_match_pattern[1].getKind()==INST_CONSTANT ); + }else if( ( d_match_pattern.getKind()==EQUAL || d_match_pattern.getKind()==IFF ) && + 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 diff --git a/src/theory/quantifiers/inst_strategy_e_matching.cpp b/src/theory/quantifiers/inst_strategy_e_matching.cpp index 491da7116..8c3154c1c 100644 --- a/src/theory/quantifiers/inst_strategy_e_matching.cpp +++ b/src/theory/quantifiers/inst_strategy_e_matching.cpp @@ -60,6 +60,7 @@ struct sortTriggers { }; void InstStrategyUserPatterns::processResetInstantiationRound( Theory::Effort effort ){ + Trace("inst-alg-debug") << "reset user triggers" << std::endl; //reset triggers for( std::map< Node, std::vector< Trigger* > >::iterator it = d_user_gen.begin(); it != d_user_gen.end(); ++it ){ for( unsigned i=0; i<it->second.size(); i++ ){ @@ -67,6 +68,7 @@ void InstStrategyUserPatterns::processResetInstantiationRound( Theory::Effort ef it->second[i]->reset( Node::null() ); } } + Trace("inst-alg-debug") << "done reset user triggers" << std::endl; } int InstStrategyUserPatterns::process( Node f, Theory::Effort effort, int e ){ @@ -118,11 +120,13 @@ void InstStrategyUserPatterns::addUserPattern( Node q, Node pat ){ bool usable = true; std::vector< Node > nodes; for( unsigned i=0; i<pat.getNumChildren(); i++ ){ - nodes.push_back( pat[i] ); - if( pat[i].getKind()!=INST_CONSTANT && !Trigger::isUsableTrigger( pat[i], q ) ){ + Node pat_use = Trigger::getIsUsableTrigger( pat[i], q ); + if( pat_use.isNull() ){ Trace("trigger-warn") << "User-provided trigger is not usable : " << pat << " because of " << pat[i] << std::endl; usable = false; break; + }else{ + nodes.push_back( pat_use ); } } if( usable ){ @@ -132,7 +136,12 @@ void InstStrategyUserPatterns::addUserPattern( Node q, Node pat ){ if( d_quantEngine->getInstUserPatMode()==USER_PAT_MODE_RESORT ){ d_user_gen_wait[q].push_back( nodes ); }else{ - d_user_gen[q].push_back( Trigger::mkTrigger( d_quantEngine, q, nodes, matchOption, true, Trigger::TR_MAKE_NEW ) ); + Trigger * t = Trigger::mkTrigger( d_quantEngine, q, nodes, matchOption, true, Trigger::TR_MAKE_NEW ); + if( t ){ + d_user_gen[q].push_back( t ); + }else{ + Trace("trigger-warn") << "Failed to construct trigger : " << pat << " due to variable mismatch" << std::endl; + } } } } @@ -154,6 +163,7 @@ InstStrategyAutoGenTriggers::InstStrategyAutoGenTriggers( QuantifiersEngine* qe } void InstStrategyAutoGenTriggers::processResetInstantiationRound( Theory::Effort effort ){ + Trace("inst-alg-debug") << "reset auto-gen triggers" << std::endl; //reset triggers for( unsigned r=0; r<2; r++ ){ for( std::map< Node, std::map< Trigger*, bool > >::iterator it = d_auto_gen_trigger[r].begin(); it != d_auto_gen_trigger[r].end(); ++it ){ @@ -164,6 +174,7 @@ void InstStrategyAutoGenTriggers::processResetInstantiationRound( Theory::Effort } } d_processed_trigger.clear(); + Trace("inst-alg-debug") << "done reset auto-gen triggers" << std::endl; } int InstStrategyAutoGenTriggers::process( Node f, Theory::Effort effort, int e ){ @@ -235,49 +246,51 @@ int InstStrategyAutoGenTriggers::process( Node f, Theory::Effort effort, int e ) } void InstStrategyAutoGenTriggers::generateTriggers( Node f ){ - Trace("auto-gen-trigger-debug") << "Generate triggers for " << f << std::endl; + Trace("auto-gen-trigger-debug") << "Generate triggers for " << f << ", #var=" << f[0].getNumChildren() << "..." << std::endl; if( d_patTerms[0].find( f )==d_patTerms[0].end() ){ //determine all possible pattern terms based on trigger term selection strategy d_tr_strategy d_patTerms[0][f].clear(); d_patTerms[1][f].clear(); bool ntrivTriggers = options::relationalTriggers(); std::vector< Node > patTermsF; - std::map< Node, int > reqPol; + std::map< Node, inst::TriggerTermInfo > tinfo; //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; + tinfo[hd].init( f, hd ); } } //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], reqPol, true ); - Trace("auto-gen-trigger-debug") << "Collected pat terms for " << bd << ", no-patterns : " << d_user_no_gen[f].size() << std::endl; + Trigger::collectPatTerms( f, bd, patTermsF, d_tr_strategy, d_user_no_gen[f], tinfo, true ); if( ntrivTriggers ){ sortTriggers st; std::sort( patTermsF.begin(), patTermsF.end(), st ); } - for( unsigned i=0; i<patTermsF.size(); i++ ){ - Assert( reqPol.find( patTermsF[i] )!=reqPol.end() ); - Trace("auto-gen-trigger-debug") << " " << patTermsF[i] << " " << reqPol[patTermsF[i]] << std::endl; + if( Trace.isOn("auto-gen-trigger-debug") ){ + Trace("auto-gen-trigger-debug") << "Collected pat terms for " << bd << ", no-patterns : " << d_user_no_gen[f].size() << std::endl; + for( unsigned i=0; i<patTermsF.size(); i++ ){ + Assert( tinfo.find( patTermsF[i] )!=tinfo.end() ); + Trace("auto-gen-trigger-debug") << " " << patTermsF[i]; + Trace("auto-gen-trigger-debug") << " info[" << tinfo[patTermsF[i]].d_reqPol << ", " << tinfo[patTermsF[i]].d_reqPolEq << ", " << tinfo[patTermsF[i]].d_fv.size() << "]" << std::endl; + } + Trace("auto-gen-trigger-debug") << std::endl; } - Trace("auto-gen-trigger-debug") << std::endl; } //sort into single/multi triggers, calculate which terms should not be considered - std::map< Node, std::vector< Node > > varContains; std::map< Node, bool > vcMap; std::map< Node, bool > rmPatTermsF; int last_weight = -1; for( unsigned i=0; i<patTermsF.size(); i++ ){ - d_quantEngine->getTermDatabase()->getVarContainsNode( f, patTermsF[i], varContains[ patTermsF[i] ] ); + Assert( patTermsF[i].getKind()!=NOT ); bool newVar = false; - for( unsigned j=0; j<varContains[ patTermsF[i] ].size(); j++ ){ - if( vcMap.find( varContains[ patTermsF[i] ][j] )==vcMap.end() ){ - vcMap[varContains[ patTermsF[i] ][j]] = true; + for( unsigned j=0; j<tinfo[ patTermsF[i] ].d_fv.size(); j++ ){ + if( vcMap.find( tinfo[ patTermsF[i] ].d_fv[j] )==vcMap.end() ){ + vcMap[tinfo[ patTermsF[i] ].d_fv[j]] = true; newVar = true; } } @@ -289,33 +302,46 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f ){ last_weight = curr_w; } } - for( std::map< Node, std::vector< Node > >::iterator it = varContains.begin(); it != varContains.end(); ++it ){ - Node pat = it->first; - Trace("auto-gen-trigger-debug") << "...processing pattern " << pat << std::endl; + for( unsigned i=0; i<patTermsF.size(); i++ ){ + Node pat = patTermsF[i]; if( rmPatTermsF.find( pat )==rmPatTermsF.end() ){ + Trace("auto-gen-trigger-debug") << "...processing pattern " << pat << std::endl; //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 ){ + Assert( tinfo.find( pat )!=tinfo.end() ); + int rpol = tinfo[pat].d_reqPol; + Node rpoleq = tinfo[pat].d_reqPolEq; + unsigned num_fv = tinfo[pat].d_fv.size(); + Trace("auto-gen-trigger-debug") << "...required polarity for " << pat << " is " << rpol << ", eq=" << rpoleq << std::endl; + if( rpol!=0 ){ + if( Trigger::isRelationalTrigger( pat ) ){ + pat = rpol==-1 ? pat.negate() : pat; + }else{ + Assert( Trigger::isAtomicTrigger( pat ) ); + if( pat.getType().isBoolean() && rpoleq.isNull() ){ pat = NodeManager::currentNM()->mkNode( IFF, pat, NodeManager::currentNM()->mkConst( rpol==-1 ) ).negate(); + }else{ + Assert( !rpoleq.isNull() ); + if( rpol==-1 ){ + //all equivalence classes except rpoleq + pat = NodeManager::currentNM()->mkNode( EQUAL, pat, rpoleq ).negate(); + }else if( rpol==1 ){ + //all equivalence classes that are not disequal to rpoleq TODO + } } } - } - 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; + Trace("auto-gen-trigger-debug") << "...got : " << pat << std::endl; }else{ - d_patTerms[1][f].push_back( pat ); - d_is_single_trigger[ pat ] = false; + if( Trigger::isRelationalTrigger( pat ) ){ + //consider both polarities + addPatternToPool( f, pat.negate(), num_fv ); + } } + addPatternToPool( f, pat, num_fv ); } } + //tinfo not used below this point d_made_multi_trigger[f] = false; - Trace("auto-gen-trigger") << "Single triggers for " << f << " : " << std::endl; + Trace("auto-gen-trigger") << "Single trigger pool for " << f << " : " << std::endl; for( unsigned i=0; i<d_patTerms[0][f].size(); i++ ){ Trace("auto-gen-trigger") << " " << d_patTerms[0][f][i] << std::endl; } @@ -427,6 +453,16 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f ){ } } +void InstStrategyAutoGenTriggers::addPatternToPool( Node q, Node pat, unsigned num_fv ) { + if( num_fv==q[0].getNumChildren() && ( options::pureThTriggers() || !Trigger::isPureTheoryTrigger( pat ) ) ){ + d_patTerms[0][q].push_back( pat ); + d_is_single_trigger[ pat ] = true; + }else{ + d_patTerms[1][q].push_back( pat ); + d_is_single_trigger[ pat ] = false; + } +} + bool InstStrategyAutoGenTriggers::hasUserPatterns( Node q ) { if( q.getNumChildren()==3 ){ std::map< Node, bool >::iterator it = d_hasUserPatterns.find( q ); diff --git a/src/theory/quantifiers/inst_strategy_e_matching.h b/src/theory/quantifiers/inst_strategy_e_matching.h index d48084514..028f24b27 100644 --- a/src/theory/quantifiers/inst_strategy_e_matching.h +++ b/src/theory/quantifiers/inst_strategy_e_matching.h @@ -89,6 +89,7 @@ private: int process( Node q, Theory::Effort effort, int e ); /** generate triggers */ void generateTriggers( Node q ); + void addPatternToPool( Node q, Node pat, unsigned num_fv ); //bool addTrigger( inst::Trigger * tr, Node f, unsigned r ); /** has user patterns */ bool hasUserPatterns( Node q ); diff --git a/src/theory/quantifiers/macros.cpp b/src/theory/quantifiers/macros.cpp index 90d01ac28..582599680 100644 --- a/src/theory/quantifiers/macros.cpp +++ b/src/theory/quantifiers/macros.cpp @@ -153,7 +153,7 @@ bool QuantifierMacros::isGroundUfTerm( Node f, Node n ) { d_qe->getTermDatabase()->getVarContainsNode( f, icn, var ); Trace("macros-debug2") << "Get trigger variables for " << icn << std::endl; std::vector< Node > trigger_var; - inst::Trigger::getTriggerVariables( d_qe, icn, f, trigger_var ); + inst::Trigger::getTriggerVariables( icn, f, trigger_var ); Trace("macros-debug2") << "Done." << std::endl; //only if all variables are also trigger variables return trigger_var.size()>=var.size(); diff --git a/src/theory/quantifiers/quant_util.h b/src/theory/quantifiers/quant_util.h index 2558dcbee..8db79db9c 100644 --- a/src/theory/quantifiers/quant_util.h +++ b/src/theory/quantifiers/quant_util.h @@ -101,6 +101,8 @@ class EqualityQuery { public: EqualityQuery(){} virtual ~EqualityQuery(){}; + /** extends engine */ + virtual bool extendsEngine() { return false; } /** contains term */ virtual bool hasTerm( Node a ) = 0; /** get the representative of the equivalence class of a */ diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp index 79c300401..5aae4d640 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.cpp +++ b/src/theory/quantifiers/quantifiers_rewriter.cpp @@ -244,17 +244,21 @@ RewriteResponse QuantifiersRewriter::postRewrite(TNode in) { ret = ret.negate(); status = REWRITE_AGAIN_FULL; }else if( in.getKind()==FORALL ){ - //compute attributes - QAttributes qa; - TermDb::computeQuantAttributes( in, qa ); - if( !qa.isRewriteRule() ){ - for( int op=0; op<COMPUTE_LAST; op++ ){ - if( doOperation( in, op, qa ) ){ - ret = computeOperation( in, op, qa ); - if( ret!=in ){ - rew_op = op; - status = REWRITE_AGAIN_FULL; - break; + if( in[1].isConst() ){ + return RewriteResponse( status, in[1] ); + }else{ + //compute attributes + QAttributes qa; + TermDb::computeQuantAttributes( in, qa ); + if( !qa.isRewriteRule() ){ + for( int op=0; op<COMPUTE_LAST; op++ ){ + if( doOperation( in, op, qa ) ){ + ret = computeOperation( in, op, qa ); + if( ret!=in ){ + rew_op = op; + status = REWRITE_AGAIN_FULL; + break; + } } } } diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index 5d20a7048..763a80af3 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -208,27 +208,26 @@ void TermDb::computeUfEqcTerms( TNode f ) { //returns a term n' equivalent to n // - if hasSubs = true, then n is consider under substitution subs // - if mkNewTerms = true, then n' is either null, or a term in the master equality engine -Node TermDb::evaluateTerm2( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool hasSubs, std::map< TNode, Node >& visited ) { +Node TermDb::evaluateTerm2( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool hasSubs, std::map< TNode, Node >& visited, EqualityQuery * qy ) { std::map< TNode, Node >::iterator itv = visited.find( n ); if( itv != visited.end() ){ return itv->second; } Node ret; Trace("term-db-eval") << "evaluate term : " << n << std::endl; - eq::EqualityEngine * ee = d_quantEngine->getTheoryEngine()->getMasterEqualityEngine(); - if( ee->hasTerm( n ) ){ + if( qy->hasTerm( n ) ){ Trace("term-db-eval") << "...exists in ee, return rep " << std::endl; - ret = ee->getRepresentative( n ); + ret = qy->getRepresentative( n ); }else if( n.getKind()==BOUND_VARIABLE ){ if( hasSubs ){ Assert( subs.find( n )!=subs.end() ); Trace("term-db-eval") << "...substitution is : " << subs[n] << std::endl; if( subsRep ){ - Assert( ee->hasTerm( subs[n] ) ); - Assert( ee->getRepresentative( subs[n] )==subs[n] ); + Assert( qy->hasTerm( subs[n] ) ); + Assert( qy->getRepresentative( subs[n] )==subs[n] ); ret = subs[n]; }else{ - ret = evaluateTerm2( subs[n], subs, subsRep, hasSubs, visited ); + ret = evaluateTerm2( subs[n], subs, subsRep, hasSubs, visited, qy ); } } }else if( n.getKind()==FORALL ){ @@ -239,7 +238,7 @@ Node TermDb::evaluateTerm2( TNode n, std::map< TNode, TNode >& subs, bool subsRe std::vector< TNode > args; bool ret_set = false; for( unsigned i=0; i<n.getNumChildren(); i++ ){ - TNode c = evaluateTerm2( n[i], subs, subsRep, hasSubs, visited ); + TNode c = evaluateTerm2( n[i], subs, subsRep, hasSubs, visited, qy ); if( c.isNull() ){ ret = TNode::null(); ret_set = true; @@ -260,9 +259,9 @@ Node TermDb::evaluateTerm2( TNode n, std::map< TNode, TNode >& subs, bool subsRe Trace("term-db-eval") << "Get term from DB" << std::endl; TNode nn = d_func_map_trie[f].existsTerm( args ); Trace("term-db-eval") << "Got term " << nn << std::endl; - if( !nn.isNull() && ee->hasTerm( nn ) ){ + if( !nn.isNull() && qy->hasTerm( nn ) ){ Trace("term-db-eval") << "return rep " << std::endl; - ret = ee->getRepresentative( nn ); + ret = qy->getRepresentative( nn ); ret_set = true; } } @@ -283,10 +282,10 @@ Node TermDb::evaluateTerm2( TNode n, std::map< TNode, TNode >& subs, bool subsRe } -TNode TermDb::evaluateTerm2( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool hasSubs ) { +TNode TermDb::evaluateTerm2( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool hasSubs, EqualityQuery * qy ) { + Assert( !qy->extendsEngine() ); Trace("term-db-eval") << "evaluate term : " << n << std::endl; - eq::EqualityEngine * ee = d_quantEngine->getTheoryEngine()->getMasterEqualityEngine(); - if( ee->hasTerm( n ) ){ + if( qy->getEngine()->hasTerm( n ) ){ Trace("term-db-eval") << "...exists in ee, return rep " << std::endl; return n; }else if( n.getKind()==BOUND_VARIABLE ){ @@ -294,11 +293,11 @@ TNode TermDb::evaluateTerm2( TNode n, std::map< TNode, TNode >& subs, bool subsR Assert( subs.find( n )!=subs.end() ); Trace("term-db-eval") << "...substitution is : " << subs[n] << std::endl; if( subsRep ){ - Assert( ee->hasTerm( subs[n] ) ); - Assert( ee->getRepresentative( subs[n] )==subs[n] ); + Assert( qy->getEngine()->hasTerm( subs[n] ) ); + Assert( qy->getEngine()->getRepresentative( subs[n] )==subs[n] ); return subs[n]; }else{ - return evaluateTerm2( subs[n], subs, subsRep, hasSubs ); + return evaluateTerm2( subs[n], subs, subsRep, hasSubs, qy ); } } }else{ @@ -307,11 +306,11 @@ TNode TermDb::evaluateTerm2( TNode n, std::map< TNode, TNode >& subs, bool subsR if( !f.isNull() ){ std::vector< TNode > args; for( unsigned i=0; i<n.getNumChildren(); i++ ){ - TNode c = evaluateTerm2( n[i], subs, subsRep, hasSubs ); + TNode c = evaluateTerm2( n[i], subs, subsRep, hasSubs, qy ); if( c.isNull() ){ return TNode::null(); } - c = ee->getRepresentative( c ); + c = qy->getEngine()->getRepresentative( c ); Trace("term-db-eval") << "Got child : " << c << std::endl; args.push_back( c ); } @@ -325,53 +324,59 @@ TNode TermDb::evaluateTerm2( TNode n, std::map< TNode, TNode >& subs, bool subsR return TNode::null(); } -Node TermDb::evaluateTerm( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool mkNewTerms ) { +Node TermDb::evaluateTerm( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool mkNewTerms, EqualityQuery * qy ) { + if( qy==NULL ){ + qy = d_quantEngine->getEqualityQuery(); + } if( mkNewTerms ){ std::map< TNode, Node > visited; - return evaluateTerm2( n, subs, subsRep, true, visited ); + return evaluateTerm2( n, subs, subsRep, true, visited, qy ); }else{ - return evaluateTerm2( n, subs, subsRep, true ); + return evaluateTerm2( n, subs, subsRep, true, qy ); } } -Node TermDb::evaluateTerm( TNode n, bool mkNewTerms ) { +Node TermDb::evaluateTerm( TNode n, bool mkNewTerms, EqualityQuery * qy ) { + if( qy==NULL ){ + qy = d_quantEngine->getEqualityQuery(); + } std::map< TNode, TNode > subs; if( mkNewTerms ){ std::map< TNode, Node > visited; - return evaluateTerm2( n, subs, false, false, visited ); + return evaluateTerm2( n, subs, false, false, visited, qy ); }else{ - return evaluateTerm2( n, subs, false, false ); + return evaluateTerm2( n, subs, false, false, qy ); } } -bool TermDb::isEntailed( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool hasSubs, bool pol ) { +bool TermDb::isEntailed( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool hasSubs, bool pol, EqualityQuery * qy ) { + Assert( !qy->extendsEngine() ); Trace("term-db-eval") << "Check entailed : " << n << ", pol = " << pol << std::endl; Assert( n.getType().isBoolean() ); if( n.getKind()==EQUAL ){ - TNode n1 = evaluateTerm2( n[0], subs, subsRep, hasSubs ); + TNode n1 = evaluateTerm2( n[0], subs, subsRep, hasSubs, qy ); if( !n1.isNull() ){ - TNode n2 = evaluateTerm2( n[1], subs, subsRep, hasSubs ); + TNode n2 = evaluateTerm2( n[1], subs, subsRep, hasSubs, qy ); if( !n2.isNull() ){ if( n1==n2 ){ return pol; }else{ - eq::EqualityEngine * ee = d_quantEngine->getTheoryEngine()->getMasterEqualityEngine(); - Assert( ee->hasTerm( n1 ) ); - Assert( ee->hasTerm( n2 ) ); + Assert( qy->getEngine()->hasTerm( n1 ) ); + Assert( qy->getEngine()->hasTerm( n2 ) ); if( pol ){ - return ee->areEqual( n1, n2 ); + return qy->getEngine()->areEqual( n1, n2 ); }else{ - return ee->areDisequal( n1, n2, false ); + return qy->getEngine()->areDisequal( n1, n2, false ); } } } } }else if( n.getKind()==NOT ){ - return isEntailed( n[0], subs, subsRep, hasSubs, !pol ); + return isEntailed( n[0], subs, subsRep, hasSubs, !pol, qy ); }else if( n.getKind()==OR || n.getKind()==AND ){ bool simPol = ( pol && n.getKind()==OR ) || ( !pol && n.getKind()==AND ); for( unsigned i=0; i<n.getNumChildren(); i++ ){ - if( isEntailed( n[i], subs, subsRep, hasSubs, pol ) ){ + if( isEntailed( n[i], subs, subsRep, hasSubs, pol, qy ) ){ if( simPol ){ return true; } @@ -384,31 +389,34 @@ bool TermDb::isEntailed( TNode n, std::map< TNode, TNode >& subs, bool subsRep, return !simPol; }else if( n.getKind()==IFF || n.getKind()==ITE ){ for( unsigned i=0; i<2; i++ ){ - if( isEntailed( n[0], subs, subsRep, hasSubs, i==0 ) ){ + if( isEntailed( n[0], subs, subsRep, hasSubs, i==0, qy ) ){ unsigned ch = ( n.getKind()==IFF || i==0 ) ? 1 : 2; bool reqPol = ( n.getKind()==ITE || i==0 ) ? pol : !pol; - return isEntailed( n[ch], subs, subsRep, hasSubs, reqPol ); + return isEntailed( n[ch], subs, subsRep, hasSubs, reqPol, qy ); } } }else if( n.getKind()==APPLY_UF ){ - TNode n1 = evaluateTerm2( n, subs, subsRep, hasSubs ); + TNode n1 = evaluateTerm2( n, subs, subsRep, hasSubs, qy ); if( !n1.isNull() ){ + Assert( qy->hasTerm( n1 ) ); if( n1==d_true ){ return pol; }else if( n1==d_false ){ return !pol; }else{ - eq::EqualityEngine * ee = d_quantEngine->getTheoryEngine()->getMasterEqualityEngine(); - return ee->getRepresentative( n1 ) == ( pol ? d_true : d_false ); + return qy->getEngine()->getRepresentative( n1 ) == ( pol ? d_true : d_false ); } } } return false; } -bool TermDb::isEntailed( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool pol ) { +bool TermDb::isEntailed( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool pol, EqualityQuery * qy ) { + if( qy==NULL ){ + qy = d_quantEngine->getEqualityQuery(); + } if( d_consistent_ee ){ - return isEntailed( n, subs, subsRep, true, pol ); + return isEntailed( n, subs, subsRep, true, pol, qy ); }else{ //don't check entailment wrt an inconsistent ee return false; diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h index 4cba619a8..9177d3a1a 100644 --- a/src/theory/quantifiers/term_database.h +++ b/src/theory/quantifiers/term_database.h @@ -20,6 +20,7 @@ #include "expr/attribute.h" #include "theory/theory.h" #include "theory/type_enumerator.h" +#include "theory/quantifiers/quant_util.h" #include <map> @@ -182,9 +183,9 @@ private: /** set has term */ void setHasTerm( Node n ); /** evaluate term */ - TNode evaluateTerm2( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool hasSubs ); - Node evaluateTerm2( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool hasSubs, std::map< TNode, Node >& visited ); - bool isEntailed( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool hasSubs, bool pol ); + TNode evaluateTerm2( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool hasSubs, EqualityQuery * qy ); + Node evaluateTerm2( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool hasSubs, std::map< TNode, Node >& visited, EqualityQuery * qy ); + bool isEntailed( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool hasSubs, bool pol, EqualityQuery * qy ); public: TermDb( context::Context* c, context::UserContext* u, QuantifiersEngine* qe ); ~TermDb(){} @@ -237,11 +238,11 @@ public: /** evaluate a term under a substitution. Return representative in EE if possible. * subsRep is whether subs contains only representatives */ - Node evaluateTerm( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool mkNewTerms = false ); + Node evaluateTerm( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool mkNewTerms = false, EqualityQuery * qy = NULL ); /** same as above, but without substitution */ - Node evaluateTerm( TNode n, bool mkNewTerms = false ); + Node evaluateTerm( TNode n, bool mkNewTerms = false, EqualityQuery * qy = NULL ); /** is entailed (incomplete check) */ - bool isEntailed( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool pol ); + bool isEntailed( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool pol, EqualityQuery * qy = NULL ); /** has term */ bool hasTermCurrent( Node n, bool useMode = true ); /** is term eligble for instantiation? */ diff --git a/src/theory/quantifiers/trigger.cpp b/src/theory/quantifiers/trigger.cpp index b4e00386a..38635b37b 100644 --- a/src/theory/quantifiers/trigger.cpp +++ b/src/theory/quantifiers/trigger.cpp @@ -30,6 +30,18 @@ namespace CVC4 { namespace theory { namespace inst { +void TriggerTermInfo::init( Node q, Node n, int reqPol, Node reqPolEq ){ + if( d_fv.empty() ){ + quantifiers::TermDb::getVarContainsNode( q, n, d_fv ); + } + if( d_reqPol==0 ){ + d_reqPol = reqPol; + d_reqPolEq = reqPolEq; + }else{ + //determined a ground (dis)equality must hold or else q is a tautology? + } +} + /** trigger class constructor */ Trigger::Trigger( QuantifiersEngine* qe, Node f, std::vector< Node >& nodes, int matchOption ) : d_quantEngine( qe ), d_f( f ) @@ -122,7 +134,7 @@ Trigger* Trigger::mkTrigger( QuantifiersEngine* qe, Node f, std::vector< Node >& std::map< Node, std::vector< Node > > patterns; size_t varCount = 0; std::map< Node, std::vector< Node > > varContains; - qe->getTermDatabase()->getVarContains( f, temp, varContains ); + quantifiers::TermDb::getVarContains( f, temp, varContains ); for( unsigned i=0; i<temp.size(); i++ ){ bool foundVar = false; for( unsigned j=0; j<varContains[ temp[i] ].size(); j++ ){ @@ -213,7 +225,7 @@ Trigger* Trigger::mkTrigger( QuantifiersEngine* qe, Node f, Node n, int matchOpt bool Trigger::isUsable( Node n, Node q ){ if( quantifiers::TermDb::getInstConstAttr(n)==q ){ if( isAtomicTrigger( n ) ){ - for( int i=0; i<(int)n.getNumChildren(); i++ ){ + for( unsigned i=0; i<n.getNumChildren(); i++ ){ if( !isUsable( n[i], q ) ){ return false; } @@ -238,68 +250,91 @@ bool Trigger::isUsable( Node n, Node q ){ } } -Node Trigger::getIsUsableTrigger( Node n, Node f, bool pol, bool hasPol ) { - Trace("trigger-debug") << "Is " << n << " a usable trigger? pol/hasPol=" << pol << "/" << hasPol << std::endl; +Node Trigger::getIsUsableEq( Node q, Node n ) { + Assert( isRelationalTrigger( n ) ); + for( unsigned i=0; i<2; i++) { + if( isUsableEqTerms( q, n[i], n[1-i] ) ){ + if( i==1 && ( n.getKind()==EQUAL || n.getKind()==IFF ) && !quantifiers::TermDb::hasInstConstAttr(n[0]) ){ + return NodeManager::currentNM()->mkNode( n.getKind(), n[1], n[0] ); + }else{ + return n; + } + } + } + return Node::null(); +} + +bool Trigger::isUsableEqTerms( Node q, Node n1, Node n2 ) { + if( n1.getKind()==INST_CONSTANT ){ + if( options::relationalTriggers() ){ + if( !quantifiers::TermDb::hasInstConstAttr(n2) ){ + return true; + }else if( n2.getKind()==INST_CONSTANT ){ + return true; + } + } + }else if( isAtomicTrigger( n1 ) && isUsable( n1, q ) ){ + if( options::relationalTriggers() && n2.getKind()==INST_CONSTANT && !quantifiers::TermDb::containsTerm( n1, n2 ) ){ + return true; + }else if( !quantifiers::TermDb::hasInstConstAttr(n2) ){ + return true; + } + } + return false; +} + +Node Trigger::getIsUsableTrigger( Node n, Node q ) { + bool pol = true; + Trace("trigger-debug") << "Is " << n << " a usable trigger?" << std::endl; if( n.getKind()==NOT ){ pol = !pol; n = n[0]; } - if( options::relationalTriggers() ){ - if( n.getKind()==EQUAL || n.getKind()==IFF || n.getKind()==GEQ ){ - Node rtr; - bool do_negate = hasPol && pol; - bool is_arith = n[0].getType().isReal(); - for( unsigned i=0; i<2; i++) { - if( n[1-i].getKind()==INST_CONSTANT ){ - if( ( ( isUsableTrigger( n[i], f ) && !quantifiers::TermDb::containsTerm( n[i], n[1-i] ) ) || !quantifiers::TermDb::hasInstConstAttr(n[i]) ) && - ( !do_negate || is_arith ) ){ - rtr = n; - break; - } - if( n[i].getKind()==INST_CONSTANT && ( !hasPol || pol ) ){ - do_negate = true; - rtr = n; - break; + if( n.getKind()==INST_CONSTANT ){ + return pol ? n : NodeManager::currentNM()->mkNode( IFF, n, NodeManager::currentNM()->mkConst( true ) ).notNode(); + }else if( isRelationalTrigger( n ) ){ + Node rtr = getIsUsableEq( q, n ); + if( rtr.isNull() && n[0].getType().isReal() ){ + //try to solve relation + std::map< Node, Node > m; + if( QuantArith::getMonomialSumLit(n, m) ){ + for( std::map< Node, Node >::iterator it = m.begin(); it!=m.end(); ++it ){ + bool trySolve = false; + if( !it->first.isNull() ){ + if( it->first.getKind()==INST_CONSTANT ){ + trySolve = options::relationalTriggers(); + }else if( isUsableTrigger( it->first, q ) ){ + trySolve = true; + } } - } - } - if( is_arith ){ - //try to rearrange? - std::map< Node, Node > m; - if( QuantArith::getMonomialSumLit(n, m) ){ - for( std::map< Node, Node >::iterator it = m.begin(); it!=m.end(); ++it ){ - if( !it->first.isNull() && it->first.getKind()==INST_CONSTANT ){ - Node veq; - if( QuantArith::isolate( it->first, m, veq, n.getKind() )!=0 ){ - int vti = veq[0]==it->first ? 1 : 0; - if( ( isUsableTrigger( veq[vti], f ) && !quantifiers::TermDb::containsTerm( veq[vti], veq[1-vti] ) ) || !quantifiers::TermDb::hasInstConstAttr(veq[vti]) ){ - rtr = veq; - } - } + if( trySolve ){ + Trace("trigger-debug") << "Try to solve for " << it->first << std::endl; + Node veq; + if( QuantArith::isolate( it->first, m, veq, n.getKind() )!=0 ){ + rtr = getIsUsableEq( q, veq ); } + //either all solves will succeed or all solves will fail + break; } } } - if( !rtr.isNull() ){ - Trace("relational-trigger") << "Relational trigger : " << std::endl; - Trace("relational-trigger") << " " << rtr << " (from " << n << ")" << std::endl; - Trace("relational-trigger") << " in quantifier " << f << std::endl; - if( hasPol ){ - Trace("relational-trigger") << " polarity : " << pol << std::endl; - } - Node rtr2 = do_negate ? rtr.negate() : rtr; - Trace("relational-trigger") << " return : " << rtr2 << std::endl; - return rtr2; - } } - } - bool usable = quantifiers::TermDb::getInstConstAttr(n)==f && isAtomicTrigger( n ) && isUsable( n, f ); - Trace("trigger-debug") << n << " usable : " << (quantifiers::TermDb::getInstConstAttr(n)==f) << " " << isAtomicTrigger( n ) << " " << isUsable( n, f ) << std::endl; - if( usable ){ - return n; + if( !rtr.isNull() ){ + Trace("relational-trigger") << "Relational trigger : " << std::endl; + Trace("relational-trigger") << " " << rtr << " (from " << n << ")" << std::endl; + Trace("relational-trigger") << " in quantifier " << q << std::endl; + Node rtr2 = pol ? rtr : rtr.negate(); + Trace("relational-trigger") << " return : " << rtr2 << std::endl; + return rtr2; + } }else{ - return Node::null(); + bool usable = quantifiers::TermDb::getInstConstAttr(n)==q && isAtomicTrigger( n ) && isUsable( n, q ); + Trace("trigger-debug") << n << " usable : " << (quantifiers::TermDb::getInstConstAttr(n)==q) << " " << isAtomicTrigger( n ) << " " << isUsable( n, q ) << std::endl; + if( usable ){ + return pol ? n : NodeManager::currentNM()->mkNode( IFF, n, NodeManager::currentNM()->mkConst( true ) ).notNode(); + } } + return Node::null(); } bool Trigger::isUsableTrigger( Node n, Node q ){ @@ -319,6 +354,14 @@ bool Trigger::isAtomicTriggerKind( Kind k ) { k==UNION || k==INTERSECTION || k==SUBSET || k==SETMINUS || k==MEMBER || k==SINGLETON; } +bool Trigger::isRelationalTrigger( Node n ) { + return isRelationalTriggerKind( n.getKind() ); +} + +bool Trigger::isRelationalTriggerKind( Kind k ) { + return k==EQUAL || k==IFF || k==GEQ; +} + bool Trigger::isCbqiKind( Kind k ) { return quantifiers::TermDb::isBoolConnective( k ) || k==PLUS || k==GEQ || k==EQUAL || k==MULT || k==APPLY_CONSTRUCTOR || k==APPLY_SELECTOR_TOTAL || k==APPLY_TESTER; @@ -347,40 +390,63 @@ bool Trigger::isSimpleTrigger( Node n ){ } //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, Node >& visited, std::map< Node, std::vector< Node > >& visited_fv, - quantifiers::TriggerSelMode tstrt, std::vector< Node >& exclude, - std::map< Node, int >& reqPol, std::vector< Node >& added, +bool Trigger::collectPatTerms2( Node q, Node n, std::map< Node, Node >& visited, std::map< Node, TriggerTermInfo >& tinfo, + quantifiers::TriggerSelMode tstrt, std::vector< Node >& exclude, std::vector< Node >& added, bool pol, bool hasPol, bool epol, bool hasEPol ){ std::map< Node, Node >::iterator itv = visited.find( n ); if( itv==visited.end() ){ visited[ n ] = Node::null(); Trace("auto-gen-trigger-debug2") << "Collect pat terms " << n << " " << pol << " " << hasPol << " " << epol << " " << hasEPol << std::endl; bool retVal = false; - if( n.getKind()!=FORALL ){ + if( n.getKind()!=FORALL && n.getKind()!=INST_CONSTANT ){ bool rec = true; Node nu; bool nu_single = false; if( n.getKind()!=NOT && std::find( exclude.begin(), exclude.end(), n )==exclude.end() ){ - nu = getIsUsableTrigger( n, f, pol, hasPol ); + nu = getIsUsableTrigger( n, q ); if( !nu.isNull() ){ - reqPol[ nu ] = hasEPol ? ( epol ? 1 : -1 ) : 0; - visited[ nu ] = nu; - quantifiers::TermDb::computeVarContains( nu, visited_fv[ nu ] ); - nu_single = visited_fv[nu].size()==f[0].getNumChildren(); - retVal = true; - if( tstrt==quantifiers::TRIGGER_SEL_MAX || ( tstrt==quantifiers::TRIGGER_SEL_MIN_SINGLE_MAX && !nu_single ) ){ - rec = false; + Assert( nu.getKind()!=NOT ); + Trace("auto-gen-trigger-debug2") << "...found usable trigger : " << nu << std::endl; + Node reqEq; + if( nu.getKind()==IFF || nu.getKind()==EQUAL ){ + if( isAtomicTrigger( nu[0] ) && !quantifiers::TermDb::hasInstConstAttr(nu[1]) ){ + if( hasPol ){ + reqEq = nu[1]; + } + nu = nu[0]; + } + } + Assert( reqEq.isNull() || !quantifiers::TermDb::hasInstConstAttr( reqEq ) ); + Assert( isUsableTrigger( nu, q ) ); + //do not add if already excluded + bool add = true; + if( n!=nu ){ + std::map< Node, Node >::iterator itvu = visited.find( nu ); + if( itvu!=visited.end() && itvu->second.isNull() ){ + add = false; + } + } + if( add ){ + Trace("auto-gen-trigger-debug2") << "...add usable trigger : " << nu << std::endl; + visited[ nu ] = nu; + tinfo[ nu ].init( q, nu, hasEPol ? ( epol ? 1 : -1 ) : 0, reqEq ); + nu_single = tinfo[ nu ].d_fv.size()==q[0].getNumChildren(); + retVal = true; + if( tstrt==quantifiers::TRIGGER_SEL_MAX || ( tstrt==quantifiers::TRIGGER_SEL_MIN_SINGLE_MAX && !nu_single ) ){ + rec = false; + } } } } if( rec ){ + Node nrec = nu.isNull() ? n : nu; std::vector< Node > added2; - for( unsigned i=0; i<n.getNumChildren(); i++ ){ + for( unsigned i=0; i<nrec.getNumChildren(); i++ ){ bool newHasPol, newPol; bool newHasEPol, newEPol; - QuantPhaseReq::getPolarity( n, i, hasPol, pol, newHasPol, newPol ); - QuantPhaseReq::getEntailPolarity( n, i, hasEPol, epol, newHasEPol, newEPol ); - if( collectPatTerms2( f, n[i], visited, visited_fv, tstrt, exclude, reqPol, added2, newPol, newHasPol, newEPol, newHasEPol ) ){ + QuantPhaseReq::getPolarity( nrec, i, hasPol, pol, newHasPol, newPol ); + QuantPhaseReq::getEntailPolarity( nrec, i, hasEPol, epol, newHasEPol, newEPol ); + if( collectPatTerms2( q, nrec[i], visited, tinfo, tstrt, exclude, added2, newPol, newHasPol, newEPol, newHasEPol ) ){ retVal = true; } } @@ -388,15 +454,19 @@ bool Trigger::collectPatTerms2( Node f, Node n, std::map< Node, Node >& visited, bool rm_nu = false; //discard if we added a subterm as a trigger with all variables that nu has for( unsigned i=0; i<added2.size(); i++ ){ - Assert( visited_fv.find( added2[i] )!=visited_fv.end() ); - if( visited_fv[ nu ].size()==visited_fv[added2[i]].size() ){ - rm_nu = true; + Assert( tinfo.find( added2[i] )!=tinfo.end() ); + if( added2[i]!=nu ){ + if( tinfo[ nu ].d_fv.size()==tinfo[ added2[i] ].d_fv.size() ){ + rm_nu = true; + } + added.push_back( added2[i] ); + }else{ + Assert( false ); } - added.push_back( added2[i] ); } if( rm_nu && ( tstrt==quantifiers::TRIGGER_SEL_MIN || ( tstrt==quantifiers::TRIGGER_SEL_MIN_SINGLE_ALL && nu_single ) ) ){ visited[nu] = Node::null(); - reqPol.erase( nu ); + tinfo.erase( nu ); }else{ added.push_back( nu ); } @@ -448,7 +518,7 @@ int Trigger::getTriggerWeight( Node n ) { return 0; }else{ if( options::relationalTriggers() ){ - if( n.getKind()==EQUAL || n.getKind()==IFF || n.getKind()==GEQ ){ + if( isRelationalTrigger( n ) ){ for( unsigned i=0; i<2; i++ ){ if( n[i].getKind()==INST_CONSTANT && !quantifiers::TermDb::hasInstConstAttr( n[1-i] ) ){ return 0; @@ -492,17 +562,17 @@ 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, quantifiers::TriggerSelMode tstrt, std::vector< Node >& exclude, - std::map< Node, int >& reqPol, bool filterInst ){ +void Trigger::collectPatTerms( Node q, Node n, std::vector< Node >& patTerms, quantifiers::TriggerSelMode tstrt, std::vector< Node >& exclude, + std::map< Node, TriggerTermInfo >& tinfo, bool filterInst ){ std::map< Node, Node > visited; if( filterInst ){ //immediately do not consider any term t for which another term is an instance of t std::vector< Node > patTerms2; - std::map< Node, int > reqPol2; - collectPatTerms( qe, f, n, patTerms2, quantifiers::TRIGGER_SEL_ALL, exclude, reqPol2, false ); + std::map< Node, TriggerTermInfo > tinfo2; + collectPatTerms( q, n, patTerms2, quantifiers::TRIGGER_SEL_ALL, exclude, tinfo2, false ); std::vector< Node > temp; temp.insert( temp.begin(), patTerms2.begin(), patTerms2.end() ); - qe->getTermDatabase()->filterInstances( temp ); + quantifiers::TermDb::filterInstances( temp ); if( temp.size()!=patTerms2.size() ){ Trace("trigger-filter-instance") << "Filtered an instance: " << std::endl; Trace("trigger-filter-instance") << "Old: "; @@ -517,7 +587,10 @@ void Trigger::collectPatTerms( QuantifiersEngine* qe, Node f, Node n, std::vecto } if( tstrt==quantifiers::TRIGGER_SEL_ALL ){ for( unsigned i=0; i<temp.size(); i++ ){ - reqPol[temp[i]] = reqPol2[temp[i]]; + //copy information + tinfo[temp[i]].d_fv.insert( tinfo[temp[i]].d_fv.end(), tinfo2[temp[i]].d_fv.begin(), tinfo2[temp[i]].d_fv.end() ); + tinfo[temp[i]].d_reqPol = tinfo2[temp[i]].d_reqPol; + tinfo[temp[i]].d_reqPolEq = tinfo2[temp[i]].d_reqPolEq; patTerms.push_back( temp[i] ); } return; @@ -530,10 +603,9 @@ void Trigger::collectPatTerms( QuantifiersEngine* qe, Node f, Node n, std::vecto } } } - std::map< Node, std::vector< Node > > visited_fv; std::vector< Node > added; - collectPatTerms2( f, n, visited, visited_fv, tstrt, exclude, reqPol, added, true, true, false, true ); - for( std::map< Node, int >::iterator it = reqPol.begin(); it != reqPol.end(); ++it ){ + collectPatTerms2( q, n, visited, tinfo, tstrt, exclude, added, true, true, false, true ); + for( std::map< Node, TriggerTermInfo >::iterator it = tinfo.begin(); it != tinfo.end(); ++it ){ if( !visited[it->first].isNull() ){ patTerms.push_back( it->first ); } @@ -615,15 +687,15 @@ Node Trigger::getInversion( Node n, Node x ) { return Node::null(); } -void Trigger::getTriggerVariables( QuantifiersEngine* qe, Node icn, Node f, std::vector< Node >& t_vars ) { +void Trigger::getTriggerVariables( Node icn, Node q, std::vector< Node >& t_vars ) { std::vector< Node > patTerms; - std::map< Node, int > reqPol; + std::map< Node, TriggerTermInfo > tinfo; //collect all patterns from icn std::vector< Node > exclude; - collectPatTerms( qe, f, icn, patTerms, quantifiers::TRIGGER_SEL_ALL, exclude, reqPol ); + collectPatTerms( q, icn, patTerms, quantifiers::TRIGGER_SEL_ALL, exclude, tinfo ); //collect all variables from all patterns in patTerms, add to t_vars for( unsigned i=0; i<patTerms.size(); i++ ){ - qe->getTermDatabase()->getVarContainsNode( f, patTerms[i], t_vars ); + quantifiers::TermDb::getVarContainsNode( q, patTerms[i], t_vars ); } } @@ -655,7 +727,7 @@ InstMatchGenerator* Trigger::getInstMatchGenerator( Node q, Node n ) { Trigger* TriggerTrie::getTrigger2( std::vector< Node >& nodes ){ if( nodes.empty() ){ - return d_tr; + return d_tr.empty() ? NULL : d_tr[0]; }else{ Node n = nodes.back(); nodes.pop_back(); @@ -669,13 +741,7 @@ Trigger* TriggerTrie::getTrigger2( std::vector< Node >& nodes ){ void TriggerTrie::addTrigger2( std::vector< Node >& nodes, Trigger* t ){ if( nodes.empty() ){ - if(d_tr != NULL){ - // TODO: Andy can you look at fmf/QEpres-uf.855035.smt? - delete d_tr; - d_tr = NULL; - } - Assert(d_tr == NULL); - d_tr = t; + d_tr.push_back( t ); }else{ Node n = nodes.back(); nodes.pop_back(); @@ -688,7 +754,6 @@ void TriggerTrie::addTrigger2( std::vector< Node >& nodes, Trigger* t ){ TriggerTrie::TriggerTrie() - : d_tr( NULL ) {} TriggerTrie::~TriggerTrie() { @@ -699,7 +764,9 @@ TriggerTrie::~TriggerTrie() { } d_children.clear(); - if(d_tr != NULL) { delete d_tr; } + for( unsigned i=0; i<d_tr.size(); i++ ){ + delete d_tr[i]; + } } }/* CVC4::theory::inst namespace */ diff --git a/src/theory/quantifiers/trigger.h b/src/theory/quantifiers/trigger.h index 06e9011c7..41f2a1c38 100644 --- a/src/theory/quantifiers/trigger.h +++ b/src/theory/quantifiers/trigger.h @@ -42,6 +42,16 @@ namespace CVC4 { namespace theory { namespace inst { +class TriggerTermInfo { +public: + TriggerTermInfo() : d_reqPol(0){} + ~TriggerTermInfo(){} + std::vector< Node > d_fv; + int d_reqPol; + Node d_reqPolEq; + void init( Node q, Node n, int reqPol = 0, Node reqPolEq = Node::null() ); +}; + /** A collect of nodes representing a trigger. */ class Trigger { public: @@ -91,14 +101,16 @@ class Trigger { static Trigger* mkTrigger( QuantifiersEngine* qe, Node f, Node n, int matchOption = 0, bool keepAll = true, int trOption = TR_MAKE_NEW ); - static void collectPatTerms( QuantifiersEngine* qe, Node f, Node n, - std::vector< Node >& patTerms, quantifiers::TriggerSelMode tstrt, - std::vector< Node >& exclude, std::map< Node, int >& reqPol, + static void collectPatTerms( Node q, Node n, std::vector< Node >& patTerms, quantifiers::TriggerSelMode tstrt, + std::vector< Node >& exclude, std::map< Node, TriggerTermInfo >& tinfo, bool filterInst = false ); /** is usable trigger */ static bool isUsableTrigger( Node n, Node q ); + static Node getIsUsableTrigger( Node n, Node q ); static bool isAtomicTrigger( Node n ); static bool isAtomicTriggerKind( Kind k ); + static bool isRelationalTrigger( Node n ); + static bool isRelationalTriggerKind( Kind k ); static bool isCbqiKind( Kind k ); static bool isSimpleTrigger( Node n ); static bool isBooleanTermTrigger( Node n ); @@ -111,8 +123,7 @@ class Trigger { static Node getInversionVariable( Node n ); static Node getInversion( Node n, Node x ); /** get all variables that E-matching can possibly handle */ - static void getTriggerVariables( QuantifiersEngine* qe, Node icn, Node f, - std::vector< Node >& t_vars ); + static void getTriggerVariables( Node icn, Node f, std::vector< Node >& t_vars ); void debugPrint( const char * c ) { Trace(c) << "TRIGGER( "; @@ -122,19 +133,17 @@ class Trigger { } Trace(c) << " )"; } - private: /** trigger constructor */ Trigger( QuantifiersEngine* ie, Node f, std::vector< Node >& nodes, int matchOption = 0 ); /** is subterm of trigger usable */ static bool isUsable( Node n, Node q ); - static Node getIsUsableTrigger( Node n, Node f, bool pol = true, - bool hasPol = false ); + static Node getIsUsableEq( Node q, Node eq ); + static bool isUsableEqTerms( Node q, Node n1, Node n2 ); /** collect all APPLY_UF pattern terms for f in n */ - static bool collectPatTerms2( Node f, Node n, std::map< Node, Node >& visited, std::map< Node, std::vector< Node > >& visited_fv, - quantifiers::TriggerSelMode tstrt, std::vector< Node >& exclude, - std::map< Node, int >& reqPol, std::vector< Node >& added, + static bool collectPatTerms2( Node q, Node n, std::map< Node, Node >& visited, std::map< Node, TriggerTermInfo >& tinfo, + quantifiers::TriggerSelMode tstrt, std::vector< Node >& exclude, std::vector< Node >& added, bool pol, bool hasPol, bool epol, bool hasEPol ); std::vector< Node > d_nodes; @@ -169,7 +178,7 @@ private: inst::Trigger* getTrigger2( std::vector< Node >& nodes ); void addTrigger2( std::vector< Node >& nodes, inst::Trigger* t ); - inst::Trigger* d_tr; + std::vector< inst::Trigger* > d_tr; std::map< TNode, TriggerTrie* > d_children; };/* class inst::Trigger::TriggerTrie */ diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 1a2762409..d31865f35 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -142,6 +142,7 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c, context::UserContext* d_rel_dom = NULL; d_builder = NULL; + d_curr_effort_level = QEFFORT_NONE; d_total_inst_count_debug = 0; //allow theory combination to go first, once initially d_ierCounter = options::instWhenTcFirst() ? 0 : 1; @@ -463,6 +464,7 @@ void QuantifiersEngine::check( Theory::Effort e ){ } Trace("quant-engine-debug") << "Check modules that needed check..." << std::endl; for( unsigned quant_e = QEFFORT_CONFLICT; quant_e<=QEFFORT_LAST_CALL; quant_e++ ){ + d_curr_effort_level = quant_e; bool success = true; //build the model if any module requested it if( needsModelE==quant_e ){ @@ -522,6 +524,7 @@ void QuantifiersEngine::check( Theory::Effort e ){ } } } + d_curr_effort_level = QEFFORT_NONE; Trace("quant-engine-debug") << "Done check modules that needed check." << std::endl; if( d_hasAddedLemma ){ //debug information @@ -756,67 +759,6 @@ void QuantifiersEngine::computeTermVector( Node f, InstMatch& m, std::vector< No } } -bool QuantifiersEngine::addInstantiationInternal( Node f, std::vector< Node >& vars, std::vector< Node >& terms, bool doVts ){ - Assert( f.getKind()==FORALL ); - Assert( vars.size()==terms.size() ); - Node body = getInstantiation( f, vars, terms, doVts ); //do virtual term substitution - body = quantifiers::QuantifiersRewriter::preprocess( body, true ); - Trace("inst-debug") << "...preprocess to " << body << std::endl; - Trace("inst-assert") << "(assert " << body << ")" << std::endl; - //make the lemma - Node lem = NodeManager::currentNM()->mkNode( kind::OR, f.negate(), body ); - //check for duplication - if( addLemma( lem ) ){ - d_total_inst_debug[f]++; - d_temp_inst_debug[f]++; - d_total_inst_count_debug++; - Trace("inst") << "*** Instantiate " << f << " with " << std::endl; - for( unsigned i=0; i<terms.size(); i++ ){ - if( Trace.isOn("inst") ){ - Trace("inst") << " " << terms[i]; - if( Trace.isOn("inst-debug") ){ - Trace("inst-debug") << ", type=" << terms[i].getType() << ", var_type=" << f[0][i].getType(); - } - Trace("inst") << std::endl; - } - if( options::cbqi() ){ - Node icf = quantifiers::TermDb::getInstConstAttr(terms[i]); - bool bad_inst = false; - if( !icf.isNull() ){ - if( icf==f ){ - bad_inst = true; - }else{ - bad_inst = quantifiers::TermDb::containsTerms( terms[i], d_term_db->d_inst_constants[f] ); - } - } - if( bad_inst ){ - Trace("inst")<< "***& Bad Instantiate " << f << " with " << std::endl; - for( unsigned i=0; i<terms.size(); i++ ){ - Trace("inst") << " " << terms[i] << std::endl; - } - Unreachable("Bad instantiation"); - } - } - Assert( terms[i].getType().isSubtypeOf( f[0][i].getType() ) ); - } - if( options::instMaxLevel()!=-1 ){ - uint64_t maxInstLevel = 0; - for( unsigned i=0; i<terms.size(); i++ ){ - if( terms[i].hasAttribute(InstLevelAttribute()) ){ - if( terms[i].getAttribute(InstLevelAttribute())>maxInstLevel ){ - maxInstLevel = terms[i].getAttribute(InstLevelAttribute()); - } - } - } - setInstantiationLevelAttr( body, f[1], maxInstLevel+1 ); - } - ++(d_statistics.d_instantiations); - return true; - }else{ - ++(d_statistics.d_inst_duplicate); - return false; - } -} bool QuantifiersEngine::recordInstantiationInternal( Node q, std::vector< Node >& terms, bool modEq, bool modInst ) { if( options::incrementalSolving() ){ @@ -847,7 +789,7 @@ void QuantifiersEngine::setInstantiationLevelAttr( Node n, Node qn, uint64_t lev Trace("inst-level-debug") << "Set instantiation level " << n << " to " << level << std::endl; } Assert( n.getNumChildren()==qn.getNumChildren() ); - for( int i=0; i<(int)n.getNumChildren(); i++ ){ + for( unsigned i=0; i<n.getNumChildren(); i++ ){ setInstantiationLevelAttr( n[i], qn[i], level ); } } @@ -859,7 +801,7 @@ void QuantifiersEngine::setInstantiationLevelAttr( Node n, uint64_t level ){ n.setAttribute(ila,level); Trace("inst-level-debug") << "Set instantiation level " << n << " to " << level << std::endl; } - for( int i=0; i<(int)n.getNumChildren(); i++ ){ + for( unsigned i=0; i<n.getNumChildren(); i++ ){ setInstantiationLevelAttr( n[i], level ); } } @@ -970,9 +912,11 @@ bool QuantifiersEngine::existsInstantiation( Node f, InstMatch& m, bool modEq, b } */ -bool QuantifiersEngine::addLemma( Node lem, bool doCache ){ +bool QuantifiersEngine::addLemma( Node lem, bool doCache, bool doRewrite ){ if( doCache ){ - lem = Rewriter::rewrite(lem); + if( doRewrite ){ + lem = Rewriter::rewrite(lem); + } Trace("inst-add-debug") << "Adding lemma : " << lem << std::endl; if( d_lemmas_produced_c.find( lem )==d_lemmas_produced_c.end() ){ //d_curr_out->lemma( lem, false, true ); @@ -985,6 +929,7 @@ bool QuantifiersEngine::addLemma( Node lem, bool doCache ){ return false; } }else{ + //do not need to rewrite, will be rewritten after sending d_lemmas_waiting.push_back( lem ); return true; } @@ -1012,7 +957,6 @@ bool QuantifiersEngine::addInstantiation( Node q, std::vector< Node >& terms, bo if( terms[i].isNull() ){ terms[i] = d_term_db->getModelBasisTerm( q[0][i].getType() ); } - //make it representative, this is helpful for recognizing duplication if( mkRep ){ //pick the best possible representative for instantiation, based on past use and simplicity of term terms[i] = d_eq_query->getInternalRepresentative( terms[i], q, i ); @@ -1026,7 +970,29 @@ bool QuantifiersEngine::addInstantiation( Node q, std::vector< Node >& terms, bo return false; } #ifdef CVC4_ASSERTIONS - Assert( !quantifiers::TermDb::containsUninterpretedConstant( terms[i] ) ); + bool bad_inst = false; + if( quantifiers::TermDb::containsUninterpretedConstant( terms[i] ) ){ + bad_inst = true; + }else if( !terms[i].getType().isSubtypeOf( q[0][i].getType() ) ){ + bad_inst = true; + }else if( options::cbqi() ){ + Node icf = quantifiers::TermDb::getInstConstAttr(terms[i]); + if( !icf.isNull() ){ + if( icf==q ){ + bad_inst = true; + }else{ + bad_inst = quantifiers::TermDb::containsTerms( terms[i], d_term_db->d_inst_constants[q] ); + } + } + } + //this assertion is critical to soundness + if( bad_inst ){ + Trace("inst")<< "***& Bad Instantiate " << q << " with " << std::endl; + for( unsigned j=0; j<terms.size(); j++ ){ + Trace("inst") << " " << terms[j] << std::endl; + } + Assert( false ); + } #endif } @@ -1038,7 +1004,8 @@ bool QuantifiersEngine::addInstantiation( Node q, std::vector< Node >& terms, bo } } } - //check for entailment + + //check for positive entailment if( options::instNoEntail() ){ std::map< TNode, TNode > subs; for( unsigned i=0; i<terms.size(); i++ ){ @@ -1053,7 +1020,7 @@ bool QuantifiersEngine::addInstantiation( Node q, std::vector< Node >& terms, bo //Trace("ajr-temp") << " " << eval << std::endl; } - //check for duplication + //check for term vector duplication bool alreadyExists = !recordInstantiationInternal( q, terms, modEq, modInst ); if( alreadyExists ){ Trace("inst-add-debug") << " -> Already exists." << std::endl; @@ -1061,16 +1028,57 @@ bool QuantifiersEngine::addInstantiation( Node q, std::vector< Node >& terms, bo return false; } - - //add the instantiation + //construct the instantiation Trace("inst-add-debug") << "Constructing instantiation..." << std::endl; - bool addedInst = addInstantiationInternal( q, d_term_db->d_vars[q], terms, doVts ); - //report the result - if( addedInst ){ + Assert( d_term_db->d_vars[q].size()==terms.size() ); + Node body = getInstantiation( q, d_term_db->d_vars[q], terms, doVts ); //do virtual term substitution + body = quantifiers::QuantifiersRewriter::preprocess( body, true ); + Trace("inst-debug") << "...preprocess to " << body << std::endl; + + //construct the lemma + Trace("inst-assert") << "(assert " << body << ")" << std::endl; + body = Rewriter::rewrite(body); + Node lem = NodeManager::currentNM()->mkNode( kind::OR, q.negate(), body ); + lem = Rewriter::rewrite(lem); + + //check for lemma duplication + if( addLemma( lem, true, false ) ){ + d_total_inst_debug[q]++; + d_temp_inst_debug[q]++; + d_total_inst_count_debug++; + if( Trace.isOn("inst") ){ + Trace("inst") << "*** Instantiate " << q << " with " << std::endl; + for( unsigned i=0; i<terms.size(); i++ ){ + if( Trace.isOn("inst") ){ + Trace("inst") << " " << terms[i]; + if( Trace.isOn("inst-debug") ){ + Trace("inst-debug") << ", type=" << terms[i].getType() << ", var_type=" << q[0][i].getType(); + } + Trace("inst") << std::endl; + } + } + } + if( options::instMaxLevel()!=-1 ){ + uint64_t maxInstLevel = 0; + for( unsigned i=0; i<terms.size(); i++ ){ + if( terms[i].hasAttribute(InstLevelAttribute()) ){ + if( terms[i].getAttribute(InstLevelAttribute())>maxInstLevel ){ + maxInstLevel = terms[i].getAttribute(InstLevelAttribute()); + } + } + } + setInstantiationLevelAttr( body, q[1], maxInstLevel+1 ); + } + //notify listeners + for( unsigned j=0; j<d_inst_notify.size(); j++ ){ + d_inst_notify[j]->notifyInstantiation( q, lem, terms, body ); + } Trace("inst-add-debug") << " -> Success." << std::endl; + ++(d_statistics.d_instantiations); return true; }else{ Trace("inst-add-debug") << " -> Lemma already exists." << std::endl; + ++(d_statistics.d_inst_duplicate); return false; } } @@ -1380,13 +1388,17 @@ bool EqualityQueryQuantifiersEngine::areEqual( Node a, Node b ){ } bool EqualityQueryQuantifiersEngine::areDisequal( Node a, Node b ){ - eq::EqualityEngine* ee = getEngine(); - if( ee->hasTerm( a ) && ee->hasTerm( b ) ){ - if( ee->areDisequal( a, b, false ) ){ - return true; + if( a==b ){ + return false; + }else{ + eq::EqualityEngine* ee = getEngine(); + if( ee->hasTerm( a ) && ee->hasTerm( b ) ){ + if( ee->areDisequal( a, b, false ) ){ + return true; + } } + return false; } - return false; } Node EqualityQueryQuantifiersEngine::getInternalRepresentative( Node a, Node f, int index ){ diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index 641c7624e..cdf7c3b89 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -81,6 +81,12 @@ public: quantifiers::TermDb * getTermDatabase(); };/* class QuantifiersModule */ +class InstantiationNotify { +public: + InstantiationNotify(){} + virtual void notifyInstantiation( Node q, Node lem, std::vector< Node >& terms, Node body ) = 0; +}; + namespace quantifiers { class FirstOrderModel; //modules @@ -128,6 +134,8 @@ private: TheoryEngine* d_te; /** vector of modules for quantifiers */ std::vector< QuantifiersModule* > d_modules; + /** instantiation notify */ + std::vector< InstantiationNotify* > d_inst_notify; /** equality query class */ EqualityQueryQuantifiersEngine* d_eq_query; /** for computing relevance of quantifiers */ @@ -176,6 +184,8 @@ public: //effort levels QEFFORT_NONE, }; private: + /** current effort level */ + unsigned d_curr_effort_level; /** list of all quantifiers seen */ std::map< Node, bool > d_quants; /** quantifiers reduced */ @@ -303,8 +313,6 @@ private: bool reduceQuantifier( Node q ); /** compute term vector */ void computeTermVector( Node f, InstMatch& m, std::vector< Node >& vars, std::vector< Node >& terms ); - /** instantiate f with arguments terms */ - bool addInstantiationInternal( Node f, std::vector< Node >& vars, std::vector< Node >& terms, bool doVts = false ); /** record instantiation, return true if it was non-duplicate */ bool recordInstantiationInternal( Node q, std::vector< Node >& terms, bool modEq = false, bool modInst = false ); /** set instantiation level attr */ @@ -321,7 +329,7 @@ public: /** do substitution */ Node getSubstitute( Node n, std::vector< Node >& terms ); /** add lemma lem */ - bool addLemma( Node lem, bool doCache = true ); + bool addLemma( Node lem, bool doCache = true, bool doRewrite = true ); /** add require phase */ void addRequirePhase( Node lit, bool req ); /** do instantiation specified by m */ diff --git a/test/regress/regress0/quantifiers/Makefile.am b/test/regress/regress0/quantifiers/Makefile.am index f0c9b5a33..784eaf677 100644 --- a/test/regress/regress0/quantifiers/Makefile.am +++ b/test/regress/regress0/quantifiers/Makefile.am @@ -76,7 +76,8 @@ TESTS = \ subtype-param.smt2 \ anti-sk-simp.smt2 \ pure_dt_cbqi.smt2 \ - florian-case-ax.smt2 + florian-case-ax.smt2 \ + double-pattern.smt2 # regression can be solved with --finite-model-find --fmf-inst-engine diff --git a/test/regress/regress0/quantifiers/double-pattern.smt2 b/test/regress/regress0/quantifiers/double-pattern.smt2 new file mode 100644 index 000000000..4ce21d446 --- /dev/null +++ b/test/regress/regress0/quantifiers/double-pattern.smt2 @@ -0,0 +1,6 @@ +(set-logic UFLIA) +(set-info :status unsat) +(declare-fun P (Int) Bool) +(assert (forall ((x Int)) (! (! (P x) :pattern ((P x))) :pattern ((P x))))) +(assert (not (P 0))) +(check-sat) |