diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2013-06-17 15:31:28 -0500 |
|---|---|---|
| committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2013-06-17 15:31:38 -0500 |
| commit | 66ee6c6472264be842f4e80a7106399d7f51d28a (patch) | |
| tree | 55c6adcdcadc41c7b34d46eea7081d8bdc2eb7a0 /src/theory/quantifiers/trigger.cpp | |
| parent | 8936ca3ab2a1b9e3612e08a73542f7a288ee1df8 (diff) | |
Make --var-elim-quant true by default. Add rewrite engine to quantifiers module.
Diffstat (limited to 'src/theory/quantifiers/trigger.cpp')
| -rw-r--r-- | src/theory/quantifiers/trigger.cpp | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/src/theory/quantifiers/trigger.cpp b/src/theory/quantifiers/trigger.cpp index fea8ab6d5..b71a1486c 100644 --- a/src/theory/quantifiers/trigger.cpp +++ b/src/theory/quantifiers/trigger.cpp @@ -44,7 +44,7 @@ d_quantEngine( qe ), d_f( f ){ d_mg = new InstMatchGeneratorSimple( f, d_nodes[0] ); }else{ d_mg = InstMatchGenerator::mkInstMatchGenerator( d_nodes[0], qe ); - d_mg->setActiveAdd(); + d_mg->setActiveAdd(true); } }else{ d_mg = new InstMatchGeneratorMulti( f, d_nodes, qe, matchOption ); @@ -53,7 +53,7 @@ d_quantEngine( qe ), d_f( f ){ } }else{ d_mg = InstMatchGenerator::mkInstMatchGenerator( d_nodes, qe ); - d_mg->setActiveAdd(); + d_mg->setActiveAdd(true); } if( d_nodes.size()==1 ){ if( isSimpleTrigger( d_nodes[0] ) ){ @@ -301,7 +301,7 @@ Node Trigger::getIsUsableTrigger( Node n, Node f, bool pol, bool hasPol ) { } } bool usable = quantifiers::TermDb::getInstConstAttr(n)==f && isAtomicTrigger( n ) && isUsable( n, f ); - Trace("usable") << n << " usable : " << usable << std::endl; + Trace("usable") << n << " usable : " << (quantifiers::TermDb::getInstConstAttr(n)==f) << " " << isAtomicTrigger( n ) << " " << isUsable( n, f ) << std::endl; if( usable ){ return n; }else{ |