diff options
Diffstat (limited to 'src/theory/quantifiers/instantiation_engine.cpp')
-rw-r--r-- | src/theory/quantifiers/instantiation_engine.cpp | 9 |
1 files changed, 1 insertions, 8 deletions
diff --git a/src/theory/quantifiers/instantiation_engine.cpp b/src/theory/quantifiers/instantiation_engine.cpp index e867aae1e..4fbf298f4 100644 --- a/src/theory/quantifiers/instantiation_engine.cpp +++ b/src/theory/quantifiers/instantiation_engine.cpp @@ -31,14 +31,13 @@ using namespace CVC4::theory::quantifiers; using namespace CVC4::theory::inst; InstantiationEngine::InstantiationEngine( QuantifiersEngine* qe ) : -QuantifiersModule( qe ), d_isup(NULL), d_i_ag(NULL), d_i_lte(NULL), d_i_fs(NULL), d_i_splx(NULL), d_i_cegqi( NULL ){ +QuantifiersModule( qe ), d_isup(NULL), d_i_ag(NULL), d_i_fs(NULL), d_i_splx(NULL), d_i_cegqi( NULL ){ } InstantiationEngine::~InstantiationEngine() { delete d_i_ag; delete d_isup; - delete d_i_lte; delete d_i_fs; delete d_i_splx; delete d_i_cegqi; @@ -59,12 +58,6 @@ void InstantiationEngine::finishInit(){ d_instStrategies.push_back( d_i_ag ); } - //local theory extensions TODO? - //if( options::localTheoryExt() ){ - // d_i_lte = new InstStrategyLocalTheoryExt( d_quantEngine ); - // d_instStrategies.push_back( d_i_lte ); - //} - //full saturation : instantiate from relevant domain, then arbitrary terms if( options::fullSaturateQuant() ){ d_i_fs = new InstStrategyFreeVariable( d_quantEngine ); |