Simplify initialization of quantifiers engine (#1641)

diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 60f44c256ff3b40eed6d660aa47637b25eced81d..be0cf9fc9388a9262617314807501c2c9b34fed2 100644 (file)
--- 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() ){

diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index 3716fc49770fdb49136def91fd9a1c46b9434b59..3fb250d4addc37ba9ce2d76115925ca992a23cce 100644 (file)
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -277,8 +277,6 @@ public:
   /** is finite bound */
   bool isFiniteBound( Node q, Node v );
 public:
-  /** initialize */
-  void finishInit();
   /** presolve */
   void presolve();
   /** notify preprocessed assertion */

diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 0c2857b11a268e8e30ce4eda2b3966c0496c2d8d..a6c42f5848e3f829c100d0d6c73c6fe276f63e3a 100644 (file)
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -214,12 +214,11 @@ void TheoryEngine::EngineOutputChannel::conflict(TNode conflictNode,
 }
 
 void TheoryEngine::finishInit() {
-  // initialize the quantifiers engine
-  d_quantEngine = new QuantifiersEngine(d_context, d_userContext, this);
 
   //initialize the quantifiers engine, master equality engine, model, model builder
   if( d_logicInfo.isQuantified() ) {
-    d_quantEngine->finishInit();
+    // initialize the quantifiers engine
+    d_quantEngine = new QuantifiersEngine(d_context, d_userContext, this);
     Assert(d_masterEqualityEngine == 0);
     d_masterEqualityEngine = new eq::EqualityEngine(d_masterEENotify,getSatContext(), "theory::master", false);
 
@@ -904,7 +903,14 @@ TheoryModel* TheoryEngine::getModel() {
 
 void TheoryEngine::getSynthSolutions(std::map<Node, Node>& sol_map)
 {
-  d_quantEngine->getSynthSolutions(sol_map);
+  if (d_quantEngine)
+  {
+    d_quantEngine->getSynthSolutions(sol_map);
+  }
+  else
+  {
+    Assert(false);
+  }
 }
 
 bool TheoryEngine::presolve() {
@@ -1480,6 +1486,7 @@ void TheoryEngine::printInstantiations( std::ostream& out ) {
     d_quantEngine->printInstantiations( out );
   }else{
     out << "Internal error : instantiations not available when quantifiers are not present." << std::endl;
+    Assert(false);
   }
 }
 
@@ -1488,6 +1495,7 @@ void TheoryEngine::printSynthSolution( std::ostream& out ) {
     d_quantEngine->printSynthSolution( out );
   }else{
     out << "Internal error : synth solution not available when quantifiers are not present." << std::endl;
+    Assert(false);
   }
 }