Simplify initialization of quantifiers engine (#1641)

1 files changed, 54 insertions, 55 deletions

diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 60f44c256..be0cf9fc9 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -175,62 +175,7 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c,
   d_ierCounter_lc = 0;
   d_ierCounterLastLc = 0;
   d_inst_when_phase = 1 + ( options::instWhenPhase()<1 ? 1 : options::instWhenPhase() );
-}
 
-QuantifiersEngine::~QuantifiersEngine(){
-  delete d_alpha_equiv;
-  delete d_builder;
-  delete d_qepr;
-  delete d_rr_engine;
-  delete d_bint;
-  delete d_model_engine;
-  delete d_inst_engine;
-  delete d_qcf;
-  delete d_quant_rel;
-  delete d_rel_dom;
-  delete d_bv_invert;
-  delete d_model;
-  delete d_tr_trie;
-  delete d_term_db;
-  delete d_sygus_tdb;
-  delete d_term_util;
-  delete d_eq_inference;
-  delete d_eq_query;
-  delete d_sg_gen;
-  delete d_ceg_inst;
-  delete d_lte_part_inst;
-  delete d_fun_def_engine;
-  delete d_uee;
-  delete d_fs;
-  delete d_i_cbqi;
-  delete d_qsplit;
-  delete d_anti_skolem;
-  delete d_inst_prop;
-}
-
-EqualityQuery* QuantifiersEngine::getEqualityQuery() {
-  return d_eq_query;
-}
-
-context::Context* QuantifiersEngine::getSatContext(){
-  return d_te->theoryOf( THEORY_QUANTIFIERS )->getSatContext();
-}
-
-context::UserContext* QuantifiersEngine::getUserContext(){
-  return d_te->theoryOf( THEORY_QUANTIFIERS )->getUserContext();
-}
-
-OutputChannel& QuantifiersEngine::getOutputChannel(){
-  return d_te->theoryOf( THEORY_QUANTIFIERS )->getOutputChannel();
-}
-/** get default valuation for the quantifiers engine */
-Valuation& QuantifiersEngine::getValuation(){
-  return d_te->theoryOf( THEORY_QUANTIFIERS )->getValuation();
-}
-
-void QuantifiersEngine::finishInit(){
-  context::Context * c = getSatContext();
-  Trace("quant-engine-debug") << "QuantifiersEngine : finishInit " << std::endl;
   bool needsBuilder = false;
   bool needsRelDom = false;
   //add quantifiers modules
@@ -331,6 +276,60 @@ void QuantifiersEngine::finishInit(){
   }
 }
 
+QuantifiersEngine::~QuantifiersEngine()
+{
+  delete d_alpha_equiv;
+  delete d_builder;
+  delete d_qepr;
+  delete d_rr_engine;
+  delete d_bint;
+  delete d_model_engine;
+  delete d_inst_engine;
+  delete d_qcf;
+  delete d_quant_rel;
+  delete d_rel_dom;
+  delete d_bv_invert;
+  delete d_model;
+  delete d_tr_trie;
+  delete d_term_db;
+  delete d_sygus_tdb;
+  delete d_term_util;
+  delete d_eq_inference;
+  delete d_eq_query;
+  delete d_sg_gen;
+  delete d_ceg_inst;
+  delete d_lte_part_inst;
+  delete d_fun_def_engine;
+  delete d_uee;
+  delete d_fs;
+  delete d_i_cbqi;
+  delete d_qsplit;
+  delete d_anti_skolem;
+  delete d_inst_prop;
+}
+
+EqualityQuery* QuantifiersEngine::getEqualityQuery() { return d_eq_query; }
+
+context::Context* QuantifiersEngine::getSatContext()
+{
+  return d_te->theoryOf(THEORY_QUANTIFIERS)->getSatContext();
+}
+
+context::UserContext* QuantifiersEngine::getUserContext()
+{
+  return d_te->theoryOf(THEORY_QUANTIFIERS)->getUserContext();
+}
+
+OutputChannel& QuantifiersEngine::getOutputChannel()
+{
+  return d_te->theoryOf(THEORY_QUANTIFIERS)->getOutputChannel();
+}
+/** get default valuation for the quantifiers engine */
+Valuation& QuantifiersEngine::getValuation()
+{
+  return d_te->theoryOf(THEORY_QUANTIFIERS)->getValuation();
+}
+
 QuantifiersModule * QuantifiersEngine::getOwner( Node q ) {
   std::map< Node, QuantifiersModule * >::iterator it = d_owner.find( q );
   if( it==d_owner.end() ){