diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2012-11-13 21:16:26 +0000 |
|---|---|---|
| committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2012-11-13 21:16:26 +0000 |
| commit | 795e5ba8a1138a371409ac9c8e9da78ce652bb94 (patch) | |
| tree | 5cc0d5bebbccf87b122b9e1690f27e398b4e8cc0 /src/theory/quantifiers/trigger.cpp | |
| parent | 740df5937639738a0238312dfb061643e62ba605 (diff) | |
refactoring of quantifiers rewriter based on code review from yesterday, refactoring code out of instantiators in preparation for quantifiers equality engine
Diffstat (limited to 'src/theory/quantifiers/trigger.cpp')
| -rw-r--r-- | src/theory/quantifiers/trigger.cpp | 4 |
1 files changed, 1 insertions, 3 deletions
diff --git a/src/theory/quantifiers/trigger.cpp b/src/theory/quantifiers/trigger.cpp index ae08fe863..67b2e6bd8 100644 --- a/src/theory/quantifiers/trigger.cpp +++ b/src/theory/quantifiers/trigger.cpp @@ -67,10 +67,8 @@ d_quantEngine( qe ), d_f( f ){ } //Notice() << "Trigger : " << (*this) << " for " << f << std::endl; if( options::eagerInstQuant() ){ - Theory* th_uf = qe->getTheoryEngine()->theoryOf( theory::THEORY_UF ); - uf::InstantiatorTheoryUf* ith = (uf::InstantiatorTheoryUf*)th_uf->getInstantiator(); for( int i=0; i<(int)d_nodes.size(); i++ ){ - ith->registerTrigger( this, d_nodes[i].getOperator() ); + qe->getTermDatabase()->registerTrigger( this, d_nodes[i].getOperator() ); } } } |