diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2013-03-06 10:46:07 -0600 |
---|---|---|
committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2013-03-06 10:46:19 -0600 |
commit | 44d9a7c29f565dbba0baea3f9df23d6d3e5bd74f (patch) | |
tree | f9a0b47038e393553a2d6a315138ae8b128915a1 /src/theory/quantifiers/trigger.cpp | |
parent | 66b99ac64a6920787905948315e74ca1c5b3e90b (diff) |
fixed two bugs for the new E-matching implementation, added aggressive miniscoping option --ag-miniscope-quant, minor cleanup
Diffstat (limited to 'src/theory/quantifiers/trigger.cpp')
-rw-r--r-- | src/theory/quantifiers/trigger.cpp | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/src/theory/quantifiers/trigger.cpp b/src/theory/quantifiers/trigger.cpp index c4bc248d3..cff28f243 100644 --- a/src/theory/quantifiers/trigger.cpp +++ b/src/theory/quantifiers/trigger.cpp @@ -38,7 +38,8 @@ d_quantEngine( qe ), d_f( f ){ for( int i=0; i<(int)d_nodes.size(); i++ ){ Trace("trigger") << " " << d_nodes[i] << std::endl; } - Trace("trigger") << ", smart triggers = " << smartTriggers << std::endl; + Trace("trigger-debug") << ", smart triggers = " << smartTriggers; + Trace("trigger") << std::endl; if( smartTriggers ){ if( d_nodes.size()==1 ){ if( isSimpleTrigger( d_nodes[0] ) ){ @@ -49,6 +50,8 @@ d_quantEngine( qe ), d_f( f ){ } }else{ d_mg = new InstMatchGeneratorMulti( f, d_nodes, qe, matchOption ); + //d_mg = InstMatchGenerator::mkInstMatchGenerator( d_nodes, qe ); + //d_mg->setActiveAdd(); } }else{ d_mg = InstMatchGenerator::mkInstMatchGenerator( d_nodes, qe ); |