diff options
Diffstat (limited to 'src/theory/quantifiers')
-rw-r--r-- | src/theory/quantifiers/candidate_generator.cpp | 32 | ||||
-rw-r--r-- | src/theory/quantifiers/candidate_generator.h | 2 | ||||
-rw-r--r-- | src/theory/quantifiers/inst_strategy_e_matching.cpp | 22 | ||||
-rw-r--r-- | src/theory/quantifiers/trigger.cpp | 24 | ||||
-rw-r--r-- | src/theory/quantifiers/trigger.h | 1 |
5 files changed, 62 insertions, 19 deletions
diff --git a/src/theory/quantifiers/candidate_generator.cpp b/src/theory/quantifiers/candidate_generator.cpp index 680be77da..1f68884b6 100644 --- a/src/theory/quantifiers/candidate_generator.cpp +++ b/src/theory/quantifiers/candidate_generator.cpp @@ -130,21 +130,37 @@ Node CandidateGeneratorQE::getNextCandidate(){ CandidateGeneratorQELitEq::CandidateGeneratorQELitEq( QuantifiersEngine* qe, Node mpat ) : d_match_pattern( mpat ), d_qe( qe ){ - + Assert( mpat.getKind()==EQUAL ); + for( unsigned i=0; i<2; i++ ){ + if( !quantifiers::TermDb::hasInstConstAttr(mpat[i]) ){ + d_match_gterm = mpat[i]; + } + } } void CandidateGeneratorQELitEq::resetInstantiationRound(){ } void CandidateGeneratorQELitEq::reset( Node eqc ){ - d_eq = eq::EqClassesIterator( d_qe->getEqualityQuery()->getEngine() ); + if( d_match_gterm.isNull() ){ + d_eq = eq::EqClassesIterator( d_qe->getEqualityQuery()->getEngine() ); + }else{ + d_do_mgt = true; + } } Node CandidateGeneratorQELitEq::getNextCandidate(){ - while( !d_eq.isFinished() ){ - Node n = (*d_eq); - ++d_eq; - if( n.getType().isComparableTo( d_match_pattern[0].getType() ) ){ - //an equivalence class with the same type as the pattern, return reflexive equality - return NodeManager::currentNM()->mkNode( d_match_pattern.getKind(), n, n ); + if( d_match_gterm.isNull() ){ + while( !d_eq.isFinished() ){ + Node n = (*d_eq); + ++d_eq; + if( n.getType().isComparableTo( d_match_pattern[0].getType() ) ){ + //an equivalence class with the same type as the pattern, return reflexive equality + return NodeManager::currentNM()->mkNode( d_match_pattern.getKind(), n, n ); + } + } + }else{ + if( d_do_mgt ){ + d_do_mgt = false; + return NodeManager::currentNM()->mkNode( d_match_pattern.getKind(), d_match_gterm, d_match_gterm ); } } return Node::null(); diff --git a/src/theory/quantifiers/candidate_generator.h b/src/theory/quantifiers/candidate_generator.h index fb120dd08..d86891de7 100644 --- a/src/theory/quantifiers/candidate_generator.h +++ b/src/theory/quantifiers/candidate_generator.h @@ -108,6 +108,8 @@ private: eq::EqClassesIterator d_eq; //equality you are trying to match equalities for Node d_match_pattern; + Node d_match_gterm; + bool d_do_mgt; //einstantiator pointer QuantifiersEngine* d_qe; public: diff --git a/src/theory/quantifiers/inst_strategy_e_matching.cpp b/src/theory/quantifiers/inst_strategy_e_matching.cpp index 621327c0b..111eab116 100644 --- a/src/theory/quantifiers/inst_strategy_e_matching.cpp +++ b/src/theory/quantifiers/inst_strategy_e_matching.cpp @@ -51,10 +51,12 @@ struct sortQuantifiersForSymbol { struct sortTriggers { bool operator() (Node i, Node j) { - if( Trigger::isAtomicTrigger( i ) ){ - return i<j || !Trigger::isAtomicTrigger( j ); + int wi = Trigger::getTriggerWeight( i ); + int wj = Trigger::getTriggerWeight( j ); + if( wi==wj ){ + return i<j; }else{ - return i<j && !Trigger::isAtomicTrigger( j ); + return wi<wj; } } }; @@ -257,19 +259,20 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f ){ Node bd = d_quantEngine->getTermDatabase()->getInstConstantBody( f ); Trigger::collectPatTerms( d_quantEngine, f, bd, patTermsF, d_tr_strategy, d_user_no_gen[f], true ); Trace("auto-gen-trigger-debug") << "Collected pat terms for " << bd << ", no-patterns : " << d_user_no_gen[f].size() << std::endl; - for( int i=0; i<(int)patTermsF.size(); i++ ){ - Trace("auto-gen-trigger-debug") << " " << patTermsF[i] << std::endl; - } - Trace("auto-gen-trigger-debug") << std::endl; if( ntrivTriggers ){ sortTriggers st; std::sort( patTermsF.begin(), patTermsF.end(), st ); } + for( unsigned i=0; i<patTermsF.size(); i++ ){ + Trace("auto-gen-trigger-debug") << " " << patTermsF[i] << std::endl; + } + Trace("auto-gen-trigger-debug") << std::endl; } //sort into single/multi triggers 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] ] ); bool newVar = false; @@ -279,9 +282,12 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f ){ newVar = true; } } - if( ntrivTriggers && !newVar && !Trigger::isAtomicTrigger( patTermsF[i] ) ){ + 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; rmPatTermsF[patTermsF[i]] = true; + }else{ + last_weight = curr_w; } } for( std::map< Node, std::vector< Node > >::iterator it = varContains.begin(); it != varContains.end(); ++it ){ diff --git a/src/theory/quantifiers/trigger.cpp b/src/theory/quantifiers/trigger.cpp index 0628b7fbc..48385e28b 100644 --- a/src/theory/quantifiers/trigger.cpp +++ b/src/theory/quantifiers/trigger.cpp @@ -242,7 +242,7 @@ 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?" << std::endl; + Trace("trigger-debug") << "Is " << n << " a usable trigger? pol/hasPol=" << pol << "/" << hasPol << std::endl; if( n.getKind()==NOT ){ pol = !pol; n = n[0]; @@ -254,7 +254,8 @@ Node Trigger::getIsUsableTrigger( Node n, Node f, bool pol, bool hasPol ) { 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] ) && ( !do_negate || is_arith ) ){ + 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; } @@ -274,7 +275,7 @@ Node Trigger::getIsUsableTrigger( Node n, Node f, bool pol, bool hasPol ) { 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] ) ){ + if( ( isUsableTrigger( veq[vti], f ) && !quantifiers::TermDb::containsTerm( veq[vti], veq[1-vti] ) ) || !quantifiers::TermDb::hasInstConstAttr(veq[vti]) ){ rtr = veq; } } @@ -434,6 +435,23 @@ bool Trigger::isPureTheoryTrigger( Node n ) { } } +int Trigger::getTriggerWeight( Node n ) { + if( isAtomicTrigger( n ) ){ + return 0; + }else{ + if( options::relationalTriggers() ){ + if( n.getKind()==EQUAL || n.getKind()==IFF || n.getKind()==GEQ ){ + for( unsigned i=0; i<2; i++ ){ + if( n[i].getKind()==INST_CONSTANT && !quantifiers::TermDb::hasInstConstAttr( n[1-i] ) ){ + return 0; + } + } + } + } + return 1; + } +} + bool Trigger::isLocalTheoryExt( Node n, std::vector< Node >& vars, std::vector< Node >& patTerms ) { if( !n.getType().isBoolean() && n.getKind()==APPLY_UF ){ if( std::find( patTerms.begin(), patTerms.end(), n )==patTerms.end() ){ diff --git a/src/theory/quantifiers/trigger.h b/src/theory/quantifiers/trigger.h index 11962008e..bbbf9495f 100644 --- a/src/theory/quantifiers/trigger.h +++ b/src/theory/quantifiers/trigger.h @@ -112,6 +112,7 @@ public: static bool isSimpleTrigger( Node n ); static bool isBooleanTermTrigger( Node n ); static bool isPureTheoryTrigger( Node n ); + static int getTriggerWeight( Node n ); static bool isLocalTheoryExt( Node n, std::vector< Node >& vars, std::vector< Node >& patTerms ); /** return data structure for producing matches for this trigger. */ static InstMatchGenerator* getInstMatchGenerator( Node q, Node n ); |