summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/quantifiers')
-rw-r--r--src/theory/quantifiers/candidate_generator.cpp32
-rw-r--r--src/theory/quantifiers/candidate_generator.h2
-rw-r--r--src/theory/quantifiers/inst_strategy_e_matching.cpp22
-rw-r--r--src/theory/quantifiers/trigger.cpp24
-rw-r--r--src/theory/quantifiers/trigger.h1
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 );
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback