From f9e109b0ac12ffbfd167a19dcd60f16241a0542c Mon Sep 17 00:00:00 2001
From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Wed, 4 Nov 2015 10:41:49 +0100
Subject: Better combination of UF with cbqi, refactor quantifiers
 intialization.

---
 src/theory/quantifiers/instantiation_engine.cpp | 20 ++++++++++----------
 1 file changed, 10 insertions(+), 10 deletions(-)

(limited to 'src/theory/quantifiers/instantiation_engine.cpp')

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();
-- 
cgit v1.2.3