Better combination of UF with cbqi, refactor quantifiers intialization.

1 files changed, 10 insertions, 10 deletions

diff --git a/src/theory/quantifiers/instantiation_engine.cpp b/src/theory/quantifiers/instantiation_engine.cpp
index 2785ad128..49f561234 100644
--- a/src/theory/quantifiers/instantiation_engine.cpp
+++ b/src/theory/quantifiers/instantiation_engine.cpp
@@ -30,16 +30,7 @@ using namespace CVC4::theory::quantifiers;
 using namespace CVC4::theory::inst;
 
 InstantiationEngine::InstantiationEngine( QuantifiersEngine* qe ) :
-QuantifiersModule( qe ), d_isup(NULL), d_i_ag(NULL){
-
-}
-
-InstantiationEngine::~InstantiationEngine() {
-  delete d_i_ag;
-  delete d_isup;
-}
-
-void InstantiationEngine::finishInit(){
+QuantifiersModule( qe ){
   if( options::eMatching() ){
     //these are the instantiation strategies for E-matching
     //user-provided patterns
@@ -51,9 +42,18 @@ void InstantiationEngine::finishInit(){
     //auto-generated patterns
     d_i_ag = new InstStrategyAutoGenTriggers( d_quantEngine );
     d_instStrategies.push_back( d_i_ag );
+  }else{
+    d_isup = NULL;
+    d_i_ag = NULL;
   }
 }
 
+InstantiationEngine::~InstantiationEngine() {
+  delete d_i_ag;
+  delete d_isup;
+}
+
+
 void InstantiationEngine::presolve() {
   for( unsigned i=0; i<d_instStrategies.size(); ++i ){
     d_instStrategies[i]->presolve();