diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2013-06-24 12:52:07 -0500 |
---|---|---|
committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2013-06-24 12:52:21 -0500 |
commit | 30d21b25af6ee619e5f53d1ca8821b710fad4cb7 (patch) | |
tree | 409009a6ab55986308cc73d030db53489beef26d /src/theory/quantifiers/trigger.cpp | |
parent | 3eaf02c01e74a2a43b2eff7638d6c16171a11a13 (diff) |
Add options for symmetry breaking in uf+ss totality axiom approach, option for using clique lemmas instead of splitting on demand, option for simplifying models in fmf-fmc, minor fixes for rewrite engine
Diffstat (limited to 'src/theory/quantifiers/trigger.cpp')
-rw-r--r-- | src/theory/quantifiers/trigger.cpp | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/src/theory/quantifiers/trigger.cpp b/src/theory/quantifiers/trigger.cpp index b71a1486c..39063942d 100644 --- a/src/theory/quantifiers/trigger.cpp +++ b/src/theory/quantifiers/trigger.cpp @@ -73,6 +73,7 @@ d_quantEngine( qe ), d_f( f ){ qe->getTermDatabase()->registerTrigger( this, d_nodes[i].getOperator() ); } } + Trace("trigger-debug") << "Finished making trigger." << std::endl; } void Trigger::resetInstantiationRound(){ @@ -144,6 +145,12 @@ Trigger* Trigger::mkTrigger( QuantifiersEngine* qe, Node f, std::vector< Node >& } } if( varCount<f[0].getNumChildren() ){ + Trace("trigger-debug") << "Don't consider trigger since it does not contain all variables in " << f << std::endl; + for( unsigned i=0; i<nodes.size(); i++) { + Trace("trigger-debug") << nodes[i] << " "; + } + Trace("trigger-debug") << std::endl; + //do not generate multi-trigger if it does not contain all variables return NULL; }else{ |