Clean up quantifiers engine initialization. (#2371)

2 files changed, 326 insertions, 283 deletions

diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index a5cd95d29..510953035 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -70,10 +70,36 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c,
                                      context::UserContext* u,
                                      TheoryEngine* te)
     : d_te(te),
+      d_eq_query(new quantifiers::EqualityQueryQuantifiersEngine(c, this)),
+      d_eq_inference(nullptr),
+      d_inst_prop(nullptr),
+      d_tr_trie(new inst::TriggerTrie),
+      d_model(nullptr),
+      d_quant_rel(nullptr),
+      d_rel_dom(nullptr),
+      d_bv_invert(nullptr),
+      d_builder(nullptr),
+      d_qepr(nullptr),
+      d_term_util(new quantifiers::TermUtil(this)),
+      d_term_db(new quantifiers::TermDb(c, u, this)),
+      d_sygus_tdb(nullptr),
       d_quant_attr(new quantifiers::QuantAttributes(this)),
       d_instantiate(new quantifiers::Instantiate(this, u)),
       d_skolemize(new quantifiers::Skolemize(this, u)),
       d_term_enum(new quantifiers::TermEnumeration),
+      d_alpha_equiv(nullptr),
+      d_inst_engine(nullptr),
+      d_model_engine(nullptr),
+      d_bint(nullptr),
+      d_qcf(nullptr),
+      d_rr_engine(nullptr),
+      d_sg_gen(nullptr),
+      d_ceg_inst(nullptr),
+      d_lte_part_inst(nullptr),
+      d_fs(nullptr),
+      d_i_cbqi(nullptr),
+      d_qsplit(nullptr),
+      d_anti_skolem(nullptr),
       d_conflict_c(c, false),
       // d_quants(u),
       d_quants_prereg(u),
@@ -89,41 +115,29 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c,
       d_presolve_cache_wq(u),
       d_presolve_cache_wic(u)
 {
-  //utilities
-  d_eq_query = new quantifiers::EqualityQueryQuantifiersEngine( c, this );
-  d_util.push_back( d_eq_query );
+  //---- utilities
+  d_util.push_back(d_eq_query.get());
+  // term util must come before the other utilities
+  d_util.push_back(d_term_util.get());
+  d_util.push_back(d_term_db.get());
 
-  // term util must come first
-  d_term_util = new quantifiers::TermUtil(this);
-  d_util.push_back(d_term_util);
-
-  d_term_db = new quantifiers::TermDb( c, u, this );
-  d_util.push_back( d_term_db );
-  
   if (options::ceGuidedInst()) {
-    d_sygus_tdb = new quantifiers::TermDbSygus(c, this);
-  }else{
-    d_sygus_tdb = NULL;
+    d_sygus_tdb.reset(new quantifiers::TermDbSygus(c, this));
   }
 
   if( options::instPropagate() ){
     // notice that this option is incompatible with options::qcfAllConflict()
-    d_inst_prop = new quantifiers::InstPropagator( this );
-    d_util.push_back( d_inst_prop );
+    d_inst_prop.reset(new quantifiers::InstPropagator(this));
+    d_util.push_back(d_inst_prop.get());
     d_instantiate->addNotify(d_inst_prop->getInstantiationNotify());
-  }else{
-    d_inst_prop = NULL;
   }
   
   if( options::inferArithTriggerEq() ){
-    d_eq_inference = new quantifiers::EqualityInference(c, false);
-  }else{
-    d_eq_inference = NULL;
+    d_eq_inference.reset(new quantifiers::EqualityInference(c, false));
   }
 
   d_util.push_back(d_instantiate.get());
 
-  d_tr_trie = new inst::TriggerTrie;
   d_curr_effort_level = QuantifiersModule::QEFFORT_NONE;
   d_conflict = false;
   d_hasAddedLemma = false;
@@ -135,37 +149,15 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c,
   Trace("quant-engine-debug") << "Initialize model, mbqi : " << options::mbqiMode() << std::endl;
 
   if( options::relevantTriggers() ){
-    d_quant_rel = new quantifiers::QuantRelevance;
-    d_util.push_back(d_quant_rel);
-  }else{
-    d_quant_rel = NULL;
+    d_quant_rel.reset(new quantifiers::QuantRelevance);
+    d_util.push_back(d_quant_rel.get());
   }
 
   if( options::quantEpr() ){
     Assert( !options::incrementalSolving() );
-    d_qepr = new quantifiers::QuantEPR;
-  }else{
-    d_qepr = NULL;
+    d_qepr.reset(new quantifiers::QuantEPR);
   }
-
-
-  d_qcf = NULL;
-  d_sg_gen = NULL;
-  d_inst_engine = NULL;
-  d_i_cbqi = NULL;
-  d_qsplit = NULL;
-  d_anti_skolem = NULL;
-  d_model = NULL;
-  d_model_engine = NULL;
-  d_bint = NULL;
-  d_rr_engine = NULL;
-  d_ceg_inst = NULL;
-  d_lte_part_inst = NULL;
-  d_alpha_equiv = NULL;
-  d_fs = NULL;
-  d_rel_dom = NULL;
-  d_bv_invert = NULL;
-  d_builder = NULL;
+  //---- end utilities
 
   //allow theory combination to go first, once initially
   d_ierCounter = options::instWhenTcFirst() ? 0 : 1;
@@ -178,70 +170,70 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c,
   bool needsRelDom = false;
   //add quantifiers modules
   if( options::quantConflictFind() || options::quantRewriteRules() ){
-    d_qcf = new quantifiers::QuantConflictFind( this, c);
-    d_modules.push_back( d_qcf );
+    d_qcf.reset(new quantifiers::QuantConflictFind(this, c));
+    d_modules.push_back(d_qcf.get());
   }
   if( options::conjectureGen() ){
-    d_sg_gen = new quantifiers::ConjectureGenerator( this, c );
-    d_modules.push_back( d_sg_gen );
+    d_sg_gen.reset(new quantifiers::ConjectureGenerator(this, c));
+    d_modules.push_back(d_sg_gen.get());
   }
   if( !options::finiteModelFind() || options::fmfInstEngine() ){
-    d_inst_engine = new quantifiers::InstantiationEngine( this );
-    d_modules.push_back(  d_inst_engine );
+    d_inst_engine.reset(new quantifiers::InstantiationEngine(this));
+    d_modules.push_back(d_inst_engine.get());
   }
   if( options::cbqi() ){
-    d_i_cbqi = new quantifiers::InstStrategyCegqi( this );
-    d_modules.push_back( d_i_cbqi );
+    d_i_cbqi.reset(new quantifiers::InstStrategyCegqi(this));
+    d_modules.push_back(d_i_cbqi.get());
     if( options::cbqiBv() ){
       // if doing instantiation for BV, need the inverter class
-      d_bv_invert = new quantifiers::BvInverter;
+      d_bv_invert.reset(new quantifiers::BvInverter);
     }
   }
   if( options::ceGuidedInst() ){
-    d_ceg_inst = new quantifiers::CegInstantiation( this, c );
-    d_modules.push_back( d_ceg_inst );
+    d_ceg_inst.reset(new quantifiers::CegInstantiation(this, c));
+    d_modules.push_back(d_ceg_inst.get());
     //needsBuilder = true;
   }  
   //finite model finding
   if( options::finiteModelFind() ){
     if( options::fmfBound() ){
-      d_bint = new quantifiers::BoundedIntegers( c, this );
-      d_modules.push_back( d_bint );
+      d_bint.reset(new quantifiers::BoundedIntegers(c, this));
+      d_modules.push_back(d_bint.get());
     }
-    d_model_engine = new quantifiers::ModelEngine( c, this );
-    d_modules.push_back( d_model_engine );
+    d_model_engine.reset(new quantifiers::ModelEngine(c, this));
+    d_modules.push_back(d_model_engine.get());
     //finite model finder has special ways of building the model
     needsBuilder = true;
   }
   if( options::quantRewriteRules() ){
-    d_rr_engine = new quantifiers::RewriteEngine( c, this );
-    d_modules.push_back(d_rr_engine);
+    d_rr_engine.reset(new quantifiers::RewriteEngine(c, this));
+    d_modules.push_back(d_rr_engine.get());
   }
   if( options::ltePartialInst() ){
-    d_lte_part_inst = new quantifiers::LtePartialInst( this, c );
-    d_modules.push_back( d_lte_part_inst );
+    d_lte_part_inst.reset(new quantifiers::LtePartialInst(this, c));
+    d_modules.push_back(d_lte_part_inst.get());
   }
   if( options::quantDynamicSplit()!=quantifiers::QUANT_DSPLIT_MODE_NONE ){
-    d_qsplit = new quantifiers::QuantDSplit( this, c );
-    d_modules.push_back( d_qsplit );
+    d_qsplit.reset(new quantifiers::QuantDSplit(this, c));
+    d_modules.push_back(d_qsplit.get());
   }
   if( options::quantAntiSkolem() ){
-    d_anti_skolem = new quantifiers::QuantAntiSkolem( this );
-    d_modules.push_back( d_anti_skolem );
+    d_anti_skolem.reset(new quantifiers::QuantAntiSkolem(this));
+    d_modules.push_back(d_anti_skolem.get());
   }
   if( options::quantAlphaEquiv() ){
-    d_alpha_equiv = new quantifiers::AlphaEquivalence( this );
+    d_alpha_equiv.reset(new quantifiers::AlphaEquivalence(this));
   }
   //full saturation : instantiate from relevant domain, then arbitrary terms
   if( options::fullSaturateQuant() || options::fullSaturateInterleave() ){
-    d_fs = new quantifiers::InstStrategyEnum(this);
-    d_modules.push_back( d_fs );
+    d_fs.reset(new quantifiers::InstStrategyEnum(this));
+    d_modules.push_back(d_fs.get());
     needsRelDom = true;
   }
   
   if( needsRelDom ){
-    d_rel_dom = new quantifiers::RelevantDomain( this );
-    d_util.push_back( d_rel_dom );
+    d_rel_dom.reset(new quantifiers::RelevantDomain(this));
+    d_util.push_back(d_rel_dom.get());
   }
   
   // if we require specialized ways of building the model
@@ -252,53 +244,27 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c,
         || options::fmfBound())
     {
       Trace("quant-engine-debug") << "...make fmc builder." << std::endl;
-      d_model = new quantifiers::fmcheck::FirstOrderModelFmc( this, c, "FirstOrderModelFmc" );
-      d_builder = new quantifiers::fmcheck::FullModelChecker( c, this );
+      d_model.reset(new quantifiers::fmcheck::FirstOrderModelFmc(
+          this, c, "FirstOrderModelFmc"));
+      d_builder.reset(new quantifiers::fmcheck::FullModelChecker(c, this));
     }else if( options::mbqiMode()==quantifiers::MBQI_ABS ){
       Trace("quant-engine-debug") << "...make abs mbqi builder." << std::endl;
-      d_model = new quantifiers::FirstOrderModelAbs( this, c, "FirstOrderModelAbs" );
-      d_builder = new quantifiers::AbsMbqiBuilder( c, this );
+      d_model.reset(
+          new quantifiers::FirstOrderModelAbs(this, c, "FirstOrderModelAbs"));
+      d_builder.reset(new quantifiers::AbsMbqiBuilder(c, this));
     }else{
       Trace("quant-engine-debug") << "...make default model builder." << std::endl;
-      d_model = new quantifiers::FirstOrderModelIG( this, c, "FirstOrderModelIG" );
-      d_builder = new quantifiers::QModelBuilderDefault( c, this );
+      d_model.reset(
+          new quantifiers::FirstOrderModelIG(this, c, "FirstOrderModelIG"));
+      d_builder.reset(new quantifiers::QModelBuilderDefault(c, this));
     }
   }else{
-    d_model = new quantifiers::FirstOrderModelIG( this, c, "FirstOrderModelIG" );
+    d_model.reset(
+        new quantifiers::FirstOrderModelIG(this, c, "FirstOrderModelIG"));
   }
 }
 
-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_fs;
-  delete d_i_cbqi;
-  delete d_qsplit;
-  delete d_anti_skolem;
-  delete d_inst_prop;
-}
-
-EqualityQuery* QuantifiersEngine::getEqualityQuery() { return d_eq_query; }
+QuantifiersEngine::~QuantifiersEngine() {}
 
 context::Context* QuantifiersEngine::getSatContext()
 {
@@ -325,6 +291,96 @@ const LogicInfo& QuantifiersEngine::getLogicInfo() const
   return d_te->getLogicInfo();
 }
 
+EqualityQuery* QuantifiersEngine::getEqualityQuery() const
+{
+  return d_eq_query.get();
+}
+quantifiers::EqualityInference* QuantifiersEngine::getEqualityInference() const
+{
+  return d_eq_inference.get();
+}
+quantifiers::RelevantDomain* QuantifiersEngine::getRelevantDomain() const
+{
+  return d_rel_dom.get();
+}
+quantifiers::BvInverter* QuantifiersEngine::getBvInverter() const
+{
+  return d_bv_invert.get();
+}
+quantifiers::QuantRelevance* QuantifiersEngine::getQuantifierRelevance() const
+{
+  return d_quant_rel.get();
+}
+quantifiers::QModelBuilder* QuantifiersEngine::getModelBuilder() const
+{
+  return d_builder.get();
+}
+quantifiers::QuantEPR* QuantifiersEngine::getQuantEPR() const
+{
+  return d_qepr.get();
+}
+quantifiers::FirstOrderModel* QuantifiersEngine::getModel() const
+{
+  return d_model.get();
+}
+quantifiers::TermDb* QuantifiersEngine::getTermDatabase() const
+{
+  return d_term_db.get();
+}
+quantifiers::TermDbSygus* QuantifiersEngine::getTermDatabaseSygus() const
+{
+  return d_sygus_tdb.get();
+}
+quantifiers::TermUtil* QuantifiersEngine::getTermUtil() const
+{
+  return d_term_util.get();
+}
+quantifiers::QuantAttributes* QuantifiersEngine::getQuantAttributes() const
+{
+  return d_quant_attr.get();
+}
+quantifiers::Instantiate* QuantifiersEngine::getInstantiate() const
+{
+  return d_instantiate.get();
+}
+quantifiers::Skolemize* QuantifiersEngine::getSkolemize() const
+{
+  return d_skolemize.get();
+}
+quantifiers::TermEnumeration* QuantifiersEngine::getTermEnumeration() const
+{
+  return d_term_enum.get();
+}
+inst::TriggerTrie* QuantifiersEngine::getTriggerDatabase() const
+{
+  return d_tr_trie.get();
+}
+
+quantifiers::BoundedIntegers* QuantifiersEngine::getBoundedIntegers() const
+{
+  return d_bint.get();
+}
+quantifiers::QuantConflictFind* QuantifiersEngine::getConflictFind() const
+{
+  return d_qcf.get();
+}
+quantifiers::RewriteEngine* QuantifiersEngine::getRewriteEngine() const
+{
+  return d_rr_engine.get();
+}
+quantifiers::CegInstantiation* QuantifiersEngine::getCegInstantiation() const
+{
+  return d_ceg_inst.get();
+}
+quantifiers::InstStrategyEnum* QuantifiersEngine::getInstStrategyEnum() const
+{
+  return d_fs.get();
+}
+quantifiers::InstStrategyCbqi* QuantifiersEngine::getInstStrategyCbqi() const
+{
+  return d_i_cbqi.get();
+}
+
 QuantifiersModule * QuantifiersEngine::getOwner( Node q ) {
   std::map< Node, QuantifiersModule * >::iterator it = d_owner.find( q );
   if( it==d_owner.end() ){
@@ -419,7 +475,8 @@ void QuantifiersEngine::check( Theory::Effort e ){
   // if we want to use the model's equality engine, build the model now
   if( d_useModelEe && !d_model->isBuilt() ){
     Trace("quant-engine-debug") << "Build the model." << std::endl;
-    if( !d_te->getModelBuilder()->buildModel( d_model ) ){
+    if (!d_te->getModelBuilder()->buildModel(d_model.get()))
+    {
       //we are done if model building was unsuccessful
       flushLemmas();
       if( d_hasAddedLemma ){
@@ -582,9 +639,10 @@ void QuantifiersEngine::check( Theory::Effort e ){
         {
           // theory engine's model builder is quantifier engine's builder if it
           // has one
-          Assert(!d_builder || d_builder == d_te->getModelBuilder());
+          Assert(!getModelBuilder()
+                 || getModelBuilder() == d_te->getModelBuilder());
           Trace("quant-engine-debug") << "Build model..." << std::endl;
-          if (!d_te->getModelBuilder()->buildModel(d_model))
+          if (!d_te->getModelBuilder()->buildModel(d_model.get()))
           {
             flushLemmas();
           }
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index 674954023..aabca1640 100644
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -84,134 +84,17 @@ namespace inst {
 
 
 class QuantifiersEngine {
-  // TODO: remove these github issue #1163
-  friend class quantifiers::InstantiationEngine;
-  friend class quantifiers::InstStrategyCbqi;
-  friend class quantifiers::InstStrategyCegqi;
-  friend class quantifiers::ModelEngine;
-  friend class quantifiers::RewriteEngine;
-  friend class quantifiers::QuantConflictFind;
-  friend class inst::InstMatch;
   typedef context::CDHashMap< Node, bool, NodeHashFunction > BoolMap;
   typedef context::CDList<Node> NodeList;
   typedef context::CDList<bool> BoolList;
   typedef context::CDHashSet<Node, NodeHashFunction> NodeSet;
-private:
-  /** reference to theory engine object */
-  TheoryEngine* d_te;
-  /** vector of utilities for quantifiers */
-  std::vector< QuantifiersUtil* > d_util;
-  /** vector of modules for quantifiers */
-  std::vector< QuantifiersModule* > d_modules;
-  /** equality query class */
-  quantifiers::EqualityQueryQuantifiersEngine* d_eq_query;
-  /** equality inference class */
-  quantifiers::EqualityInference* d_eq_inference;
-  /** for computing relevance of quantifiers */
-  quantifiers::QuantRelevance* d_quant_rel;
-  /** relevant domain */
-  quantifiers::RelevantDomain* d_rel_dom;
-  /** inversion utility for BV instantiation */
-  quantifiers::BvInverter * d_bv_invert;
-  /** alpha equivalence */
-  quantifiers::AlphaEquivalence * d_alpha_equiv;
-  /** model builder */
-  quantifiers::QModelBuilder* d_builder;
-  /** utility for effectively propositional logic */
-  quantifiers::QuantEPR* d_qepr;
-  /** term database */
-  quantifiers::TermDb* d_term_db;
-  /** sygus term database */
-  quantifiers::TermDbSygus* d_sygus_tdb;
-  /** term utilities */
-  quantifiers::TermUtil* d_term_util;
-  /** quantifiers attributes */
-  std::unique_ptr<quantifiers::QuantAttributes> d_quant_attr;
-  /** instantiate utility */
-  std::unique_ptr<quantifiers::Instantiate> d_instantiate;
-  /** skolemize utility */
-  std::unique_ptr<quantifiers::Skolemize> d_skolemize;
-  /** term enumeration utility */
-  std::unique_ptr<quantifiers::TermEnumeration> d_term_enum;
-  /** instantiation engine */
-  quantifiers::InstantiationEngine* d_inst_engine;
-  /** model engine */
-  quantifiers::ModelEngine* d_model_engine;
-  /** bounded integers utility */
-  quantifiers::BoundedIntegers * d_bint;
-  /** Conflict find mechanism for quantifiers */
-  quantifiers::QuantConflictFind* d_qcf;
-  /** rewrite rules utility */
-  quantifiers::RewriteEngine * d_rr_engine;
-  /** subgoal generator */
-  quantifiers::ConjectureGenerator * d_sg_gen;
-  /** ceg instantiation */
-  quantifiers::CegInstantiation * d_ceg_inst;
-  /** lte partial instantiation */
-  quantifiers::LtePartialInst * d_lte_part_inst;
-  /** full saturation */
-  quantifiers::InstStrategyEnum* d_fs;
-  /** counterexample-based quantifier instantiation */
-  quantifiers::InstStrategyCbqi * d_i_cbqi;
-  /** quantifiers splitting */
-  quantifiers::QuantDSplit * d_qsplit;
-  /** quantifiers anti-skolemization */
-  quantifiers::QuantAntiSkolem * d_anti_skolem;
-  /** quantifiers instantiation propagtor */
-  quantifiers::InstPropagator * d_inst_prop;
-
- private:  //this information is reset during check
-    /** current effort level */
-  QuantifiersModule::QEffort d_curr_effort_level;
-  /** are we in conflict */
-  bool d_conflict;
-  context::CDO<bool> d_conflict_c;
-  /** has added lemma this round */
-  bool d_hasAddedLemma;
-  /** whether to use model equality engine */
-  bool d_useModelEe;
- private:
-  /** list of all quantifiers seen */
-  std::map< Node, bool > d_quants;
-  /** quantifiers pre-registered */
-  NodeSet d_quants_prereg;
-  /** quantifiers reduced */
-  BoolMap d_quants_red;
-  std::map< Node, Node > d_quants_red_lem;
-  /** list of all lemmas produced */
-  //std::map< Node, bool > d_lemmas_produced;
-  BoolMap d_lemmas_produced_c;
-  /** lemmas waiting */
-  std::vector< Node > d_lemmas_waiting;
-  /** phase requirements waiting */
-  std::map< Node, bool > d_phase_req_waiting;
-  /** all triggers will be stored in this trie */
-  inst::TriggerTrie* d_tr_trie;
-  /** extended model object */
-  quantifiers::FirstOrderModel* d_model;
-  /** inst round counters TODO: make context-dependent? */
-  context::CDO< int > d_ierCounter_c;
-  int d_ierCounter;
-  int d_ierCounter_lc;
-  int d_ierCounterLastLc;
-  int d_inst_when_phase;
-  /** has presolve been called */
-  context::CDO< bool > d_presolve;
-  /** presolve cache */
-  NodeSet d_presolve_in;
-  NodeList d_presolve_cache;
-  BoolList d_presolve_cache_wq;
-  BoolList d_presolve_cache_wic;
 
 public:
   QuantifiersEngine(context::Context* c, context::UserContext* u, TheoryEngine* te);
   ~QuantifiersEngine();
+  //---------------------- external interface
   /** get theory engine */
-  TheoryEngine* getTheoryEngine() { return d_te; }
-  /** get equality query */
-  EqualityQuery* getEqualityQuery();
-  /** get the equality inference */
-  quantifiers::EqualityInference* getEqualityInference() { return d_eq_inference; }
+  TheoryEngine* getTheoryEngine() const { return d_te; }
   /** get default sat context for quantifiers engine */
   context::Context* getSatContext();
   /** get default sat context for quantifiers engine */
@@ -222,42 +105,56 @@ public:
   Valuation& getValuation();
   /** get the logic info for the quantifiers engine */
   const LogicInfo& getLogicInfo() const;
+  //---------------------- end external interface
+  //---------------------- utilities
+  /** get equality query */
+  EqualityQuery* getEqualityQuery() const;
+  /** get the equality inference */
+  quantifiers::EqualityInference* getEqualityInference() const;
   /** get relevant domain */
-  quantifiers::RelevantDomain* getRelevantDomain() { return d_rel_dom; }
+  quantifiers::RelevantDomain* getRelevantDomain() const;
   /** get the BV inverter utility */
-  quantifiers::BvInverter * getBvInverter() { return d_bv_invert; }
+  quantifiers::BvInverter* getBvInverter() const;
   /** get quantifier relevance */
-  quantifiers::QuantRelevance* getQuantifierRelevance() { return d_quant_rel; }
+  quantifiers::QuantRelevance* getQuantifierRelevance() const;
   /** get the model builder */
-  quantifiers::QModelBuilder* getModelBuilder() { return d_builder; }
+  quantifiers::QModelBuilder* getModelBuilder() const;
   /** get utility for EPR */
-  quantifiers::QuantEPR* getQuantEPR() { return d_qepr; }
- public:  // modules
-  /** get instantiation engine */
-  quantifiers::InstantiationEngine* getInstantiationEngine() { return d_inst_engine; }
-  /** get model engine */
-  quantifiers::ModelEngine* getModelEngine() { return d_model_engine; }
+  quantifiers::QuantEPR* getQuantEPR() const;
+  /** get model */
+  quantifiers::FirstOrderModel* getModel() const;
+  /** get term database */
+  quantifiers::TermDb* getTermDatabase() const;
+  /** get term database sygus */
+  quantifiers::TermDbSygus* getTermDatabaseSygus() const;
+  /** get term utilities */
+  quantifiers::TermUtil* getTermUtil() const;
+  /** get quantifiers attributes */
+  quantifiers::QuantAttributes* getQuantAttributes() const;
+  /** get instantiate utility */
+  quantifiers::Instantiate* getInstantiate() const;
+  /** get skolemize utility */
+  quantifiers::Skolemize* getSkolemize() const;
+  /** get term enumeration utility */
+  quantifiers::TermEnumeration* getTermEnumeration() const;
+  /** get trigger database */
+  inst::TriggerTrie* getTriggerDatabase() const;
+  //---------------------- end utilities
+  //---------------------- modules
   /** get bounded integers utility */
-  quantifiers::BoundedIntegers * getBoundedIntegers() { return d_bint; }
+  quantifiers::BoundedIntegers* getBoundedIntegers() const;
   /** Conflict find mechanism for quantifiers */
-  quantifiers::QuantConflictFind* getConflictFind() { return d_qcf; }
+  quantifiers::QuantConflictFind* getConflictFind() const;
   /** rewrite rules utility */
-  quantifiers::RewriteEngine * getRewriteEngine() { return d_rr_engine; }
-  /** subgoal generator */
-  quantifiers::ConjectureGenerator * getConjectureGenerator() { return d_sg_gen; }
+  quantifiers::RewriteEngine* getRewriteEngine() const;
   /** ceg instantiation */
-  quantifiers::CegInstantiation * getCegInstantiation() { return d_ceg_inst; }
-  /** local theory ext partial inst */
-  quantifiers::LtePartialInst * getLtePartialInst() { return d_lte_part_inst; }
+  quantifiers::CegInstantiation* getCegInstantiation() const;
   /** get full saturation */
-  quantifiers::InstStrategyEnum* getInstStrategyEnum() { return d_fs; }
+  quantifiers::InstStrategyEnum* getInstStrategyEnum() const;
   /** get inst strategy cbqi */
-  quantifiers::InstStrategyCbqi * getInstStrategyCbqi() { return d_i_cbqi; }
-  /** get quantifiers splitting */
-  quantifiers::QuantDSplit * getQuantDSplit() { return d_qsplit; }
-  /** get quantifiers anti-skolemization */
-  quantifiers::QuantAntiSkolem * getQuantAntiSkolem() { return d_anti_skolem; }
-private:
+  quantifiers::InstStrategyCbqi* getInstStrategyCbqi() const;
+  //---------------------- end modules
+ private:
   /** owner of quantified formulas */
   std::map< Node, QuantifiersModule * > d_owner;
   std::map< Node, int > d_owner_priority;
@@ -331,29 +228,6 @@ public:
   /** get user pat mode */
   quantifiers::UserPatMode getInstUserPatMode();
 public:
-  /** get model */
-  quantifiers::FirstOrderModel* getModel() { return d_model; }
-  /** get term database */
-  quantifiers::TermDb* getTermDatabase() { return d_term_db; }
-  /** get term database sygus */
-  quantifiers::TermDbSygus * getTermDatabaseSygus() { return d_sygus_tdb; }
-  /** get term utilities */
-  quantifiers::TermUtil* getTermUtil() { return d_term_util; }
-  /** get quantifiers attributes */
-  quantifiers::QuantAttributes* getQuantAttributes() {
-    return d_quant_attr.get();
-  }
-  /** get instantiate utility */
-  quantifiers::Instantiate* getInstantiate() { return d_instantiate.get(); }
-  /** get skolemize utility */
-  quantifiers::Skolemize* getSkolemize() { return d_skolemize.get(); }
-  /** get term enumeration utility */
-  quantifiers::TermEnumeration* getTermEnumeration()
-  {
-    return d_term_enum.get();
-  }
-  /** get trigger database */
-  inst::TriggerTrie* getTriggerDatabase() { return d_tr_trie; }
   /** add term to database */
   void addTermToDatabase( Node n, bool withinQuant = false, bool withinInstClosure = false );
   /** notification when master equality engine is updated */
@@ -439,6 +313,117 @@ public:
     ~Statistics();
   };/* class QuantifiersEngine::Statistics */
   Statistics d_statistics;
+  
+ private:
+  /** reference to theory engine object */
+  TheoryEngine* d_te;
+  /** vector of utilities for quantifiers */
+  std::vector<QuantifiersUtil*> d_util;
+  /** vector of modules for quantifiers */
+  std::vector<QuantifiersModule*> d_modules;
+  //------------- quantifiers utilities
+  /** equality query class */
+  std::unique_ptr<quantifiers::EqualityQueryQuantifiersEngine> d_eq_query;
+  /** equality inference class */
+  std::unique_ptr<quantifiers::EqualityInference> d_eq_inference;
+  /** quantifiers instantiation propagtor */
+  std::unique_ptr<quantifiers::InstPropagator> d_inst_prop;
+  /** all triggers will be stored in this trie */
+  std::unique_ptr<inst::TriggerTrie> d_tr_trie;
+  /** extended model object */
+  std::unique_ptr<quantifiers::FirstOrderModel> d_model;
+  /** for computing relevance of quantifiers */
+  std::unique_ptr<quantifiers::QuantRelevance> d_quant_rel;
+  /** relevant domain */
+  std::unique_ptr<quantifiers::RelevantDomain> d_rel_dom;
+  /** inversion utility for BV instantiation */
+  std::unique_ptr<quantifiers::BvInverter> d_bv_invert;
+  /** model builder */
+  std::unique_ptr<quantifiers::QModelBuilder> d_builder;
+  /** utility for effectively propositional logic */
+  std::unique_ptr<quantifiers::QuantEPR> d_qepr;
+  /** term utilities */
+  std::unique_ptr<quantifiers::TermUtil> d_term_util;
+  /** term database */
+  std::unique_ptr<quantifiers::TermDb> d_term_db;
+  /** sygus term database */
+  std::unique_ptr<quantifiers::TermDbSygus> d_sygus_tdb;
+  /** quantifiers attributes */
+  std::unique_ptr<quantifiers::QuantAttributes> d_quant_attr;
+  /** instantiate utility */
+  std::unique_ptr<quantifiers::Instantiate> d_instantiate;
+  /** skolemize utility */
+  std::unique_ptr<quantifiers::Skolemize> d_skolemize;
+  /** term enumeration utility */
+  std::unique_ptr<quantifiers::TermEnumeration> d_term_enum;
+  //------------- end quantifiers utilities
+  //------------- quantifiers modules
+  /** alpha equivalence */
+  std::unique_ptr<quantifiers::AlphaEquivalence> d_alpha_equiv;
+  /** instantiation engine */
+  std::unique_ptr<quantifiers::InstantiationEngine> d_inst_engine;
+  /** model engine */
+  std::unique_ptr<quantifiers::ModelEngine> d_model_engine;
+  /** bounded integers utility */
+  std::unique_ptr<quantifiers::BoundedIntegers> d_bint;
+  /** Conflict find mechanism for quantifiers */
+  std::unique_ptr<quantifiers::QuantConflictFind> d_qcf;
+  /** rewrite rules utility */
+  std::unique_ptr<quantifiers::RewriteEngine> d_rr_engine;
+  /** subgoal generator */
+  std::unique_ptr<quantifiers::ConjectureGenerator> d_sg_gen;
+  /** ceg instantiation */
+  std::unique_ptr<quantifiers::CegInstantiation> d_ceg_inst;
+  /** lte partial instantiation */
+  std::unique_ptr<quantifiers::LtePartialInst> d_lte_part_inst;
+  /** full saturation */
+  std::unique_ptr<quantifiers::InstStrategyEnum> d_fs;
+  /** counterexample-based quantifier instantiation */
+  std::unique_ptr<quantifiers::InstStrategyCbqi> d_i_cbqi;
+  /** quantifiers splitting */
+  std::unique_ptr<quantifiers::QuantDSplit> d_qsplit;
+  /** quantifiers anti-skolemization */
+  std::unique_ptr<quantifiers::QuantAntiSkolem> d_anti_skolem;
+  //------------- end quantifiers modules
+  //------------- temporary information during check
+  /** current effort level */
+  QuantifiersModule::QEffort d_curr_effort_level;
+  /** are we in conflict */
+  bool d_conflict;
+  context::CDO<bool> d_conflict_c;
+  /** has added lemma this round */
+  bool d_hasAddedLemma;
+  /** whether to use model equality engine */
+  bool d_useModelEe;
+  //------------- end temporary information during check
+ private:
+  /** list of all quantifiers seen */
+  std::map<Node, bool> d_quants;
+  /** quantifiers pre-registered */
+  NodeSet d_quants_prereg;
+  /** quantifiers reduced */
+  BoolMap d_quants_red;
+  std::map<Node, Node> d_quants_red_lem;
+  /** list of all lemmas produced */
+  // std::map< Node, bool > d_lemmas_produced;
+  BoolMap d_lemmas_produced_c;
+  /** lemmas waiting */
+  std::vector<Node> d_lemmas_waiting;
+  /** phase requirements waiting */
+  std::map<Node, bool> d_phase_req_waiting;
+  /** inst round counters TODO: make context-dependent? */
+  context::CDO<int> d_ierCounter_c;
+  int d_ierCounter;
+  int d_ierCounter_lc;
+  int d_ierCounterLastLc;
+  int d_inst_when_phase;
+  /** has presolve been called */
+  context::CDO<bool> d_presolve;
+  /** presolve cache */
+  NodeSet d_presolve_in;
+  NodeList d_presolve_cache;
+  BoolList d_presolve_cache_wq;
+  BoolList d_presolve_cache_wic;
 };/* class QuantifiersEngine */
 
 }/* CVC4::theory namespace */