diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-09-15 16:10:20 -0500 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-09-15 16:10:20 -0500 |
commit | 1cb5f852ba17c13cc39a9c75e5bc0019c80223e8 (patch) | |
tree | 087879d07b352dd644009ecef24fe0392a90f3d7 /src/theory/quantifiers/trigger.cpp | |
parent | 60687e672ea8f485b4071e485b7b0cabc034fd00 (diff) |
Begin refactoring of cbqi, remove a few dead options. Pre-skolemize by default in EPR mode.
Diffstat (limited to 'src/theory/quantifiers/trigger.cpp')
-rw-r--r-- | src/theory/quantifiers/trigger.cpp | 10 |
1 files changed, 0 insertions, 10 deletions
diff --git a/src/theory/quantifiers/trigger.cpp b/src/theory/quantifiers/trigger.cpp index d0bcd3a69..3017238ca 100644 --- a/src/theory/quantifiers/trigger.cpp +++ b/src/theory/quantifiers/trigger.cpp @@ -76,12 +76,6 @@ Trigger::Trigger( QuantifiersEngine* qe, Node f, std::vector< Node >& nodes ) ++(qe->d_statistics.d_multi_triggers); } //Notice() << "Trigger : " << (*this) << " for " << f << std::endl; - if( options::eagerInstQuant() ){ - for( int i=0; i<(int)d_nodes.size(); i++ ){ - Node op = qe->getTermDatabase()->getMatchOperator( d_nodes[i] ); - qe->getTermDatabase()->registerTrigger( this, op ); - } - } Trace("trigger-debug") << "Finished making trigger." << std::endl; } @@ -107,10 +101,6 @@ bool Trigger::getMatch( Node f, Node t, InstMatch& m ){ return ((InstMatchGenerator*)d_mg)->getMatch( f, t, m, d_quantEngine ); } -int Trigger::addTerm( Node t ){ - return d_mg->addTerm( d_f, t, d_quantEngine ); -} - Node Trigger::getInstPattern(){ return NodeManager::currentNM()->mkNode( INST_PATTERN, d_nodes ); } |