diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2012-11-30 20:38:45 +0000 |
|---|---|---|
| committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2012-11-30 20:38:45 +0000 |
| commit | f28bab562105548413cfca93de5c9b047157a076 (patch) | |
| tree | bfbe95b9aed35f91b6bd9e3af50fad03ab86f23b /src/theory/quantifiers/trigger.cpp | |
| parent | 6369830eec077ef112e6cc806cd910c7209eb2db (diff) | |
quantifiers now uses master equality engine, preparation work to cleanup code
Diffstat (limited to 'src/theory/quantifiers/trigger.cpp')
| -rw-r--r-- | src/theory/quantifiers/trigger.cpp | 10 |
1 files changed, 6 insertions, 4 deletions
diff --git a/src/theory/quantifiers/trigger.cpp b/src/theory/quantifiers/trigger.cpp index a9c5e8b96..4d5efcd8d 100644 --- a/src/theory/quantifiers/trigger.cpp +++ b/src/theory/quantifiers/trigger.cpp @@ -48,11 +48,11 @@ d_quantEngine( qe ), d_f( f ){ }else{ d_mg = new InstMatchGenerator( d_nodes, qe, matchOption ); } - Debug("trigger") << "Trigger for " << f << ": " << std::endl; + Trace("trigger") << "Trigger for " << f << ": " << std::endl; for( int i=0; i<(int)d_nodes.size(); i++ ){ - Debug("trigger") << " " << d_nodes[i] << std::endl; + Trace("trigger") << " " << d_nodes[i] << std::endl; } - Debug("trigger") << std::endl; + Trace("trigger") << std::endl; if( d_nodes.size()==1 ){ if( isSimpleTrigger( d_nodes[0] ) ){ ++(qe->d_statistics.d_triggers); @@ -230,7 +230,9 @@ bool Trigger::isUsable( Node n, Node f ){ bool Trigger::isUsableTrigger( Node n, Node f ){ //return n.getAttribute(InstConstantAttribute())==f && n.getKind()==APPLY_UF; - return n.getAttribute(InstConstantAttribute())==f && isAtomicTrigger( n ) && isUsable( n, f ); + bool usable = n.getAttribute(InstConstantAttribute())==f && isAtomicTrigger( n ) && isUsable( n, f ); + Trace("usable") << n << " usable : " << usable << std::endl; + return usable; } bool Trigger::isAtomicTrigger( Node n ){ |