diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-11-12 11:00:44 +0100 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-11-12 11:00:44 +0100 |
| commit | ada1fc44c9b5b8746a2e1e4046032282149768b5 (patch) | |
| tree | efb350f7729004fedb4d7d872d5ff7e8d5d1fdc4 /src/theory/quantifiers/trigger.cpp | |
| parent | 97470da31e14104f807fb33b2b3423e583e10726 (diff) | |
Minor fixes and improvements to purify quant, relational triggers.
Diffstat (limited to 'src/theory/quantifiers/trigger.cpp')
| -rw-r--r-- | src/theory/quantifiers/trigger.cpp | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/src/theory/quantifiers/trigger.cpp b/src/theory/quantifiers/trigger.cpp index 1f332e909..fdfa77b02 100644 --- a/src/theory/quantifiers/trigger.cpp +++ b/src/theory/quantifiers/trigger.cpp @@ -250,9 +250,10 @@ Node Trigger::getIsUsableTrigger( Node n, Node f, bool pol, bool hasPol ) { 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] ) ){ + if( isUsableTrigger( n[i], f ) && !quantifiers::TermDb::containsTerm( n[i], n[1-i] ) && ( !do_negate || is_arith ) ){ rtr = n; break; } @@ -263,7 +264,7 @@ Node Trigger::getIsUsableTrigger( Node n, Node f, bool pol, bool hasPol ) { } } } - if( n[0].getType().isInteger() ){ + if( is_arith ){ //try to rearrange? std::map< Node, Node > m; if( QuantArith::getMonomialSumLit(n, m) ){ |