Do not have quantifiers model inherit from theory model (#6493)

This is work towards making the initialization of theory engine, theory models, quantifiers engine more flexible.

This makes it so that the specialized quantifiers models classes (FirstOrderModel) do not inherit from TheoryModel. There is no longer any reason for this, since FirstOrderModel does not have any override methods.

As a result of this PR, there is only one kind of TheoryModel and it is constructed immediately when ModelManager is constructed.

This required refactoring the initialization of when FirstOrderModel is constructed in ModelBuilder classes in quantifiers.

This also avoids the need for casting TheoryModel to FirstOrderModel.

21 files changed, 254 insertions, 181 deletions

diff --git a/src/theory/combination_engine.cpp b/src/theory/combination_engine.cpp
index 3a2460959..4b04188f1 100644
--- a/src/theory/combination_engine.cpp
+++ b/src/theory/combination_engine.cpp
@@ -42,12 +42,6 @@ CombinationEngine::CombinationEngine(TheoryEngine& te,
       d_cmbsPg(pnm ? new EagerProofGenerator(pnm, te.getUserContext())
                    : nullptr)
 {
-}
-
-CombinationEngine::~CombinationEngine() {}
-
-void CombinationEngine::finishInit()
-{
   // create the equality engine, model manager, and shared solver
   if (options::eeMode() == options::EqEngineMode::DISTRIBUTED)
   {
@@ -64,7 +58,12 @@ void CombinationEngine::finishInit()
     Unhandled() << "CombinationEngine::finishInit: equality engine mode "
                 << options::eeMode() << " not supported";
   }
+}
+
+CombinationEngine::~CombinationEngine() {}
 
+void CombinationEngine::finishInit()
+{
   Assert(d_eemanager != nullptr);
 
   // initialize equality engines in all theories, including quantifiers engine
diff --git a/src/theory/model_manager.cpp b/src/theory/model_manager.cpp
index 5c2b3b25a..b7499447f 100644
--- a/src/theory/model_manager.cpp
+++ b/src/theory/model_manager.cpp
@@ -32,7 +32,9 @@ ModelManager::ModelManager(TheoryEngine& te, EqEngineManager& eem)
       d_eem(eem),
       d_modelEqualityEngine(nullptr),
       d_modelEqualityEngineAlloc(nullptr),
-      d_model(nullptr),
+      d_model(new TheoryModel(te.getUserContext(),
+                              "DefaultModel",
+                              options::assignFunctionValues())),
       d_modelBuilder(nullptr),
       d_modelBuilt(false),
       d_modelBuiltSuccess(false)
@@ -51,14 +53,6 @@ void ModelManager::finishInit(eq::EqualityEngineNotify* notify)
     QuantifiersEngine* qe = d_te.getQuantifiersEngine();
     Assert(qe != nullptr);
     d_modelBuilder = qe->getModelBuilder();
-    d_model = qe->getModel();
-  }
-  else
-  {
-    context::Context* u = d_te.getUserContext();
-    d_alocModel.reset(
-        new TheoryModel(u, "DefaultModel", options::assignFunctionValues()));
-    d_model = d_alocModel.get();
   }
 
   // make the default builder, e.g. in the case that the quantifiers engine does
@@ -142,13 +136,13 @@ void ModelManager::postProcessModel(bool incomplete)
     }
     Trace("model-builder-debug")
         << "  PostProcessModel on theory: " << theoryId << std::endl;
-    t->postProcessModel(d_model);
+    t->postProcessModel(d_model.get());
   }
   // also call the model builder's post-process model
-  d_modelBuilder->postProcessModel(incomplete, d_model);
+  d_modelBuilder->postProcessModel(incomplete, d_model.get());
 }
 
-theory::TheoryModel* ModelManager::getModel() { return d_model; }
+theory::TheoryModel* ModelManager::getModel() { return d_model.get(); }
 
 bool ModelManager::collectModelBooleanVariables()
 {
diff --git a/src/theory/model_manager.h b/src/theory/model_manager.h
index 50cd6a3d2..41559e7b6 100644
--- a/src/theory/model_manager.h
+++ b/src/theory/model_manager.h
@@ -73,7 +73,7 @@ class ModelManager
    */
   void postProcessModel(bool incomplete);
   /** Get a pointer to model object maintained by this class. */
-  theory::TheoryModel* getModel();
+  TheoryModel* getModel();
   //------------------------ finer grained control over model building
   /**
    * Prepare model, which is the manager-specific method for setting up the
@@ -138,14 +138,12 @@ class ModelManager
   eq::EqualityEngine* d_modelEqualityEngine;
   /** The equality engine of the model, if we allocated it */
   std::unique_ptr<eq::EqualityEngine> d_modelEqualityEngineAlloc;
-  /** The model object we are using */
-  theory::TheoryModel* d_model;
   /** The model object we have allocated (if one exists) */
-  std::unique_ptr<theory::TheoryModel> d_alocModel;
+  std::unique_ptr<TheoryModel> d_model;
   /** The model builder object we are using */
-  theory::TheoryEngineModelBuilder* d_modelBuilder;
+  TheoryEngineModelBuilder* d_modelBuilder;
   /** The model builder object we have allocated (if one exists) */
-  std::unique_ptr<theory::TheoryEngineModelBuilder> d_alocModelBuilder;
+  std::unique_ptr<TheoryEngineModelBuilder> d_alocModelBuilder;
   /** whether we have tried to build this model in the current context */
   bool d_modelBuilt;
   /** whether this model has been built successfully */
diff --git a/src/theory/model_manager_distributed.cpp b/src/theory/model_manager_distributed.cpp
index 6c807c647..f3a501f94 100644
--- a/src/theory/model_manager_distributed.cpp
+++ b/src/theory/model_manager_distributed.cpp
@@ -85,7 +85,7 @@ bool ModelManagerDistributed::prepareModel()
     collectAssertedTerms(theoryId, termSet);
     // also get relevant terms
     t->computeRelevantTerms(termSet);
-    if (!t->collectModelInfo(d_model, termSet))
+    if (!t->collectModelInfo(d_model.get(), termSet))
     {
       Trace("model-builder")
           << "ModelManagerDistributed: fail collect model info" << std::endl;
@@ -106,7 +106,7 @@ bool ModelManagerDistributed::prepareModel()
 bool ModelManagerDistributed::finishBuildModel() const
 {
   // do not use relevant terms
-  if (!d_modelBuilder->buildModel(d_model))
+  if (!d_modelBuilder->buildModel(d_model.get()))
   {
     Trace("model-builder") << "ModelManager: fail build model" << std::endl;
     return false;
diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp
index de71d62a7..d4bc7dfcb 100644
--- a/src/theory/quantifiers/first_order_model.cpp
+++ b/src/theory/quantifiers/first_order_model.cpp
@@ -44,10 +44,8 @@ using ModelBasisArgAttribute = expr::Attribute<ModelBasisArgAttributeId, uint64_
 
 FirstOrderModel::FirstOrderModel(QuantifiersState& qs,
                                  QuantifiersRegistry& qr,
-                                 TermRegistry& tr,
-                                 std::string name)
-    : TheoryModel(qs.getSatContext(), name, true),
-      d_qe(nullptr),
+                                 TermRegistry& tr)
+    : d_model(nullptr),
       d_qreg(qr),
       d_treg(tr),
       d_eq_query(qs, this),
@@ -56,8 +54,32 @@ FirstOrderModel::FirstOrderModel(QuantifiersState& qs,
 {
 }
 
-//!!!!!!!!!!!!!!!!!!!!! temporary (project #15)
-void FirstOrderModel::finishInit(QuantifiersEngine* qe) { d_qe = qe; }
+void FirstOrderModel::finishInit(TheoryModel* m) { d_model = m; }
+
+Node FirstOrderModel::getValue(TNode n) const { return d_model->getValue(n); }
+bool FirstOrderModel::hasTerm(TNode a) { return d_model->hasTerm(a); }
+Node FirstOrderModel::getRepresentative(TNode a)
+{
+  return d_model->getRepresentative(a);
+}
+bool FirstOrderModel::areEqual(TNode a, TNode b)
+{
+  return d_model->areEqual(a, b);
+}
+bool FirstOrderModel::areDisequal(TNode a, TNode b)
+{
+  return d_model->areDisequal(a, b);
+}
+eq::EqualityEngine* FirstOrderModel::getEqualityEngine()
+{
+  return d_model->getEqualityEngine();
+}
+const RepSet* FirstOrderModel::getRepSet() const
+{
+  return d_model->getRepSet();
+}
+RepSet* FirstOrderModel::getRepSetPtr() { return d_model->getRepSetPtr(); }
+TheoryModel* FirstOrderModel::getTheoryModel() { return d_model; }
 
 Node FirstOrderModel::getInternalRepresentative(Node a, Node q, size_t index)
 {
@@ -118,23 +140,25 @@ void FirstOrderModel::initializeModelForTerm( Node n, std::map< Node, bool >& vi
 
 Node FirstOrderModel::getSomeDomainElement(TypeNode tn){
   //check if there is even any domain elements at all
-  if (!d_rep_set.hasType(tn) || d_rep_set.d_type_reps[tn].size() == 0)
+  RepSet* rs = d_model->getRepSetPtr();
+  if (!rs->hasType(tn) || rs->getNumRepresentatives(tn) == 0)
   {
     Trace("fm-debug") << "Must create domain element for " << tn << "..."
                       << std::endl;
     Node mbt = getModelBasisTerm(tn);
     Trace("fm-debug") << "Add to representative set..." << std::endl;
-    d_rep_set.add(tn, mbt);
+    rs->add(tn, mbt);
   }
-  return d_rep_set.d_type_reps[tn][0];
+  return rs->getRepresentative(tn, 0);
 }
 
 bool FirstOrderModel::initializeRepresentativesForType(TypeNode tn)
 {
+  RepSet* rs = d_model->getRepSetPtr();
   if (tn.isSort())
   {
     // must ensure uninterpreted type is non-empty.
-    if (!d_rep_set.hasType(tn))
+    if (!rs->hasType(tn))
     {
       // terms in rep_set are now constants which mapped to terms through
       // TheoryModel. Thus, should introduce a constant and a term.
@@ -142,7 +166,7 @@ bool FirstOrderModel::initializeRepresentativesForType(TypeNode tn)
       Node var = getSomeDomainElement(tn);
       Trace("mkVar") << "RepSetIterator:: Make variable " << var << " : " << tn
                      << std::endl;
-      d_rep_set.add(tn, var);
+      rs->add(tn, var);
     }
     return true;
   }
@@ -153,9 +177,9 @@ bool FirstOrderModel::initializeRepresentativesForType(TypeNode tn)
     {
       Trace("fm-debug") << "  do complete, since cardinality is small ("
                         << tn.getCardinality() << ")..." << std::endl;
-      d_rep_set.complete(tn);
+      rs->complete(tn);
       // must have succeeded
-      Assert(d_rep_set.hasType(tn));
+      Assert(rs->hasType(tn));
       return true;
     }
     Trace("fm-debug") << "  variable cannot be bounded." << std::endl;
diff --git a/src/theory/quantifiers/first_order_model.h b/src/theory/quantifiers/first_order_model.h
index 04b1fdb63..1969fdde7 100644
--- a/src/theory/quantifiers/first_order_model.h
+++ b/src/theory/quantifiers/first_order_model.h
@@ -26,7 +26,8 @@
 namespace cvc5 {
 namespace theory {
 
-class QuantifiersEngine;
+class TheoryModel;
+class RepSet;
 
 namespace quantifiers {
 
@@ -35,17 +36,36 @@ class TermRegistry;
 class QuantifiersRegistry;
 
 // TODO (#1301) : document and refactor this class
-class FirstOrderModel : public TheoryModel
+class FirstOrderModel
 {
  public:
   FirstOrderModel(QuantifiersState& qs,
                   QuantifiersRegistry& qr,
-                  TermRegistry& tr,
-                  std::string name);
+                  TermRegistry& tr);
+  virtual ~FirstOrderModel() {}
 
-  //!!!!!!!!!!!!!!!!!!!!! temporary (project #15)
-  /** finish initialize */
-  void finishInit(QuantifiersEngine* qe);
+  /** finish init */
+  void finishInit(TheoryModel* m);
+  //---------------------------------- access functions for underlying model
+  /** Get value in the underlying theory model */
+  Node getValue(TNode n) const;
+  /** does the equality engine of this model have term a? */
+  bool hasTerm(TNode a);
+  /** get the representative of a in the equality engine of this model */
+  Node getRepresentative(TNode a);
+  /** are a and b equal in the equality engine of this model? */
+  bool areEqual(TNode a, TNode b);
+  /** are a and b disequal in the equality engine of this model? */
+  bool areDisequal(TNode a, TNode b);
+  /** get the equality engine for this model */
+  eq::EqualityEngine* getEqualityEngine();
+  /** get the representative set object */
+  const RepSet* getRepSet() const;
+  /** get the representative set object */
+  RepSet* getRepSetPtr();
+  /** get the entire theory model */
+  TheoryModel* getTheoryModel();
+  //---------------------------------- end access functions for underlying model
   /** get internal representative
    *
    * Choose a term that is equivalent to a in the current context that is the
@@ -136,8 +156,8 @@ class FirstOrderModel : public TheoryModel
   EqualityQuery* getEqualityQuery();
 
  protected:
-  //!!!!!!!!!!!!!!!!!!!!!!! TODO (project #15): temporarily available
-  QuantifiersEngine* d_qe;
+  /** Pointer to the underyling theory model */
+  TheoryModel* d_model;
   /** The quantifiers registry */
   QuantifiersRegistry& d_qreg;
   /** Reference to the term registry */
diff --git a/src/theory/quantifiers/fmf/first_order_model_fmc.cpp b/src/theory/quantifiers/fmf/first_order_model_fmc.cpp
index 852b60521..e17271613 100644
--- a/src/theory/quantifiers/fmf/first_order_model_fmc.cpp
+++ b/src/theory/quantifiers/fmf/first_order_model_fmc.cpp
@@ -38,9 +38,8 @@ using IsStarAttribute = expr::Attribute<IsStarAttributeId, bool>;
 
 FirstOrderModelFmc::FirstOrderModelFmc(QuantifiersState& qs,
                                        QuantifiersRegistry& qr,
-                                       TermRegistry& tr,
-                                       std::string name)
-    : FirstOrderModel(qs, qr, tr, name)
+                                       TermRegistry& tr)
+    : FirstOrderModel(qs, qr, tr)
 {
 }
 
diff --git a/src/theory/quantifiers/fmf/first_order_model_fmc.h b/src/theory/quantifiers/fmf/first_order_model_fmc.h
index 3c35fdbe8..f148a9e19 100644
--- a/src/theory/quantifiers/fmf/first_order_model_fmc.h
+++ b/src/theory/quantifiers/fmf/first_order_model_fmc.h
@@ -41,8 +41,7 @@ class FirstOrderModelFmc : public FirstOrderModel
  public:
   FirstOrderModelFmc(QuantifiersState& qs,
                      QuantifiersRegistry& qr,
-                     TermRegistry& tr,
-                     std::string name);
+                     TermRegistry& tr);
   ~FirstOrderModelFmc() override;
   // initialize the model
   void processInitialize(bool ispre) override;
diff --git a/src/theory/quantifiers/fmf/full_model_check.cpp b/src/theory/quantifiers/fmf/full_model_check.cpp
index da220be18..fd91a94ab 100644
--- a/src/theory/quantifiers/fmf/full_model_check.cpp
+++ b/src/theory/quantifiers/fmf/full_model_check.cpp
@@ -286,26 +286,28 @@ void Def::debugPrint(const char * tr, Node op, FullModelChecker * m) {
 }
 
 FullModelChecker::FullModelChecker(QuantifiersState& qs,
+                                   QuantifiersInferenceManager& qim,
                                    QuantifiersRegistry& qr,
-                                   QuantifiersInferenceManager& qim)
-    : QModelBuilder(qs, qr, qim)
+                                   TermRegistry& tr)
+    : QModelBuilder(qs, qim, qr, tr), d_fm(new FirstOrderModelFmc(qs, qr, tr))
 {
   d_true = NodeManager::currentNM()->mkConst(true);
   d_false = NodeManager::currentNM()->mkConst(false);
 }
 
+void FullModelChecker::finishInit() { d_model = d_fm.get(); }
+
 bool FullModelChecker::preProcessBuildModel(TheoryModel* m) {
   //standard pre-process
   if( !preProcessBuildModelStd( m ) ){
     return false;
   }
 
-  FirstOrderModelFmc* fm = (FirstOrderModelFmc*)m;
   Trace("fmc") << "---Full Model Check preprocess() " << std::endl;
   d_preinitialized_eqc.clear();
   d_preinitialized_types.clear();
   //traverse equality engine
-  eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( fm->d_equalityEngine );
+  eq::EqClassesIterator eqcs_i = eq::EqClassesIterator(m->getEqualityEngine());
   while( !eqcs_i.isFinished() ){
     Node r = *eqcs_i;
     TypeNode tr = r.getType();
@@ -315,23 +317,24 @@ bool FullModelChecker::preProcessBuildModel(TheoryModel* m) {
 
   //must ensure model basis terms exists in model for each relevant type
   Trace("fmc") << "preInitialize types..." << std::endl;
-  fm->initialize();
-  for( std::map<Node, Def * >::iterator it = fm->d_models.begin(); it != fm->d_models.end(); ++it ) {
-    Node op = it->first;
+  d_fm->initialize();
+  for (std::pair<const Node, Def*>& mp : d_fm->d_models)
+  {
+    Node op = mp.first;
     Trace("fmc") << "preInitialize types for " << op << std::endl;
     TypeNode tno = op.getType();
     for( unsigned i=0; i<tno.getNumChildren(); i++) {
       Trace("fmc") << "preInitializeType " << tno[i] << std::endl;
-      preInitializeType( fm, tno[i] );
+      preInitializeType(m, tno[i]);
       Trace("fmc") << "finished preInitializeType " << tno[i] << std::endl;
     }
   }
   Trace("fmc") << "Finish preInitialize types" << std::endl;
   //do not have to introduce terms for sorts of domains of quantified formulas if we are allowed to assume empty sorts
-  for (unsigned i = 0, nquant = fm->getNumAssertedQuantifiers(); i < nquant;
+  for (unsigned i = 0, nquant = d_fm->getNumAssertedQuantifiers(); i < nquant;
        i++)
   {
-    Node q = fm->getAssertedQuantifier(i);
+    Node q = d_fm->getAssertedQuantifier(i);
     registerQuantifiedFormula(q);
     if (!isHandled(q))
     {
@@ -340,7 +343,7 @@ bool FullModelChecker::preProcessBuildModel(TheoryModel* m) {
     // make sure all types are set
     for (const Node& v : q[0])
     {
-      preInitializeType(fm, v.getType());
+      preInitializeType(m, v.getType());
     }
   }
   return true;
@@ -352,13 +355,13 @@ bool FullModelChecker::processBuildModel(TheoryModel* m){
     // nothing to do if no functions
     return true;
   }
-  FirstOrderModelFmc* fm = (FirstOrderModelFmc*)m;
+  FirstOrderModelFmc* fm = d_fm.get();
   Trace("fmc") << "---Full Model Check reset() " << std::endl;
   d_quant_models.clear();
   d_rep_ids.clear();
   d_star_insts.clear();
   //process representatives
-  RepSet* rs = fm->getRepSetPtr();
+  RepSet* rs = m->getRepSetPtr();
   for (std::map<TypeNode, std::vector<Node> >::iterator it =
            rs->d_type_reps.begin();
        it != rs->d_type_reps.end();
@@ -367,7 +370,7 @@ bool FullModelChecker::processBuildModel(TheoryModel* m){
     if( it->first.isSort() ){
       Trace("fmc") << "Cardinality( " << it->first << " )" << " = " << it->second.size() << std::endl;
       for( size_t a=0; a<it->second.size(); a++ ){
-        Node r = fm->getRepresentative( it->second[a] );
+        Node r = m->getRepresentative(it->second[a]);
         if( Trace.isOn("fmc-model-debug") ){
           std::vector< Node > eqc;
           d_qstate.getEquivalenceClass(r, eqc);
@@ -387,25 +390,27 @@ bool FullModelChecker::processBuildModel(TheoryModel* m){
   }
 
   //now, make models
-  for( std::map<Node, Def * >::iterator it = fm->d_models.begin(); it != fm->d_models.end(); ++it ) {
-    Node op = it->first;
+  for (std::pair<const Node, Def*>& fmm : d_fm->d_models)
+  {
+    Node op = fmm.first;
     //reset the model
-    fm->d_models[op]->reset();
+    d_fm->d_models[op]->reset();
 
     std::vector< Node > add_conds;
     std::vector< Node > add_values;      
     bool needsDefault = true;
-    std::map< Node, std::vector< Node > >::iterator itut = fm->d_uf_terms.find( op );
-    if( itut!=fm->d_uf_terms.end() ){
-      Trace("fmc-model-debug") << itut->second.size() << " model values for " << op << " ... " << std::endl;
-      for( size_t i=0; i<itut->second.size(); i++ ){
-        Node n = itut->second[i];
+    if (m->hasUfTerms(op))
+    {
+      const std::vector<Node>& uft = m->getUfTerms(op);
+      Trace("fmc-model-debug")
+          << uft.size() << " model values for " << op << " ... " << std::endl;
+      for (const Node& n : uft)
+      {
         // only consider unique up to congruence (in model equality engine)?
         add_conds.push_back( n );
         add_values.push_back( n );
-        Node r = fm->getRepresentative(n);
+        Node r = m->getRepresentative(n);
         Trace("fmc-model-debug") << n << " -> " << r << std::endl;
-        //AlwaysAssert( fm->areEqual( itut->second[i], r ) );
       }
     }else{
       Trace("fmc-model-debug") << "No model values for " << op << " ... " << std::endl;
@@ -413,17 +418,18 @@ bool FullModelChecker::processBuildModel(TheoryModel* m){
     Trace("fmc-model-debug") << std::endl;
     //possibly get default
     if( needsDefault ){
-      Node nmb = fm->getModelBasisOpTerm(op);
+      Node nmb = d_fm->getModelBasisOpTerm(op);
       //add default value if necessary
-      if( fm->hasTerm( nmb ) ){
+      if (m->hasTerm(nmb))
+      {
         Trace("fmc-model-debug") << "Add default " << nmb << std::endl;
         add_conds.push_back( nmb );
         add_values.push_back( nmb );
       }else{
-        Node vmb = getSomeDomainElement(fm, nmb.getType());
+        Node vmb = getSomeDomainElement(d_fm.get(), nmb.getType());
         Trace("fmc-model-debug") << "Add default to default representative " << nmb << " ";
         Trace("fmc-model-debug")
-            << fm->getRepSet()->getNumRepresentatives(nmb.getType())
+            << m->getRepSet()->getNumRepresentatives(nmb.getType())
             << std::endl;
         add_conds.push_back( nmb );
         add_values.push_back( vmb );
@@ -536,32 +542,33 @@ bool FullModelChecker::processBuildModel(TheoryModel* m){
   return TheoryEngineModelBuilder::processBuildModel( m );
 }
 
-void FullModelChecker::preInitializeType( FirstOrderModelFmc * fm, TypeNode tn ){
+void FullModelChecker::preInitializeType(TheoryModel* m, TypeNode tn)
+{
   if( d_preinitialized_types.find( tn )==d_preinitialized_types.end() ){
     d_preinitialized_types[tn] = true;
     if (tn.isFirstClass())
     {
       Trace("fmc") << "Get model basis term " << tn << "..." << std::endl;
-      Node mb = fm->getModelBasisTerm(tn);
+      Node mb = d_fm->getModelBasisTerm(tn);
       Trace("fmc") << "...return " << mb << std::endl;
       // if the model basis term does not exist in the model,
       // either add it directly to the model's equality engine if no other terms
       // of this type exist, or otherwise assert that it is equal to the first
       // equivalence class of its type.
-      if (!fm->hasTerm(mb) && !mb.isConst())
+      if (!m->hasTerm(mb) && !mb.isConst())
       {
         std::map<TypeNode, Node>::iterator itpe = d_preinitialized_eqc.find(tn);
         if (itpe == d_preinitialized_eqc.end())
         {
           Trace("fmc") << "...add model basis term to EE of model " << mb << " "
                        << tn << std::endl;
-          fm->d_equalityEngine->addTerm(mb);
+          m->getEqualityEngine()->addTerm(mb);
         }
         else
         {
           Trace("fmc") << "...add model basis eqc equality to model " << mb
                        << " == " << itpe->second << " " << tn << std::endl;
-          bool ret = fm->assertEquality(mb, itpe->second, true);
+          bool ret = m->assertEquality(mb, itpe->second, true);
           AlwaysAssert(ret);
         }
       }
@@ -1348,7 +1355,6 @@ Node FullModelChecker::getFunctionValue(FirstOrderModelFmc * fm, Node op, const
 bool FullModelChecker::useSimpleModels() {
   return options::fmfFmcSimple();
 }
-
 void FullModelChecker::registerQuantifiedFormula(Node q)
 {
   if (d_quant_cond.find(q) != d_quant_cond.end())
diff --git a/src/theory/quantifiers/fmf/full_model_check.h b/src/theory/quantifiers/fmf/full_model_check.h
index fd50d632f..fdaf18e81 100644
--- a/src/theory/quantifiers/fmf/full_model_check.h
+++ b/src/theory/quantifiers/fmf/full_model_check.h
@@ -113,7 +113,7 @@ protected:
    * if a bound variable is of type T, or an uninterpreted function has an
    * argument or a return value of type T.
    */
-  void preInitializeType( FirstOrderModelFmc * fm, TypeNode tn );
+  void preInitializeType(TheoryModel* m, TypeNode tn);
   /** for each type, an equivalence class of that type from the model */
   std::map<TypeNode, Node> d_preinitialized_eqc;
   /** map from types to whether we have called the method above */
@@ -156,9 +156,11 @@ protected:
 
  public:
   FullModelChecker(QuantifiersState& qs,
+                   QuantifiersInferenceManager& qim,
                    QuantifiersRegistry& qr,
-                   QuantifiersInferenceManager& qim);
-
+                   TermRegistry& tr);
+  /** finish init, which sets the model object */
+  void finishInit() override;
   void debugPrintCond(const char * tr, Node n, bool dispStar = false);
   void debugPrint(const char * tr, Node n, bool dispStar = false);
 
@@ -173,7 +175,6 @@ protected:
   bool processBuildModel(TheoryModel* m) override;
 
   bool useSimpleModels();
-
  private:
   /**
    * Register quantified formula.
@@ -183,6 +184,11 @@ protected:
   void registerQuantifiedFormula(Node q);
   /** Is quantified formula q handled by model-based instantiation? */
   bool isHandled(Node q) const;
+  /**
+   * The first order model. This is an extended form of the first order model
+   * class that is specialized for this class.
+   */
+  std::unique_ptr<FirstOrderModelFmc> d_fm;
 };/* class FullModelChecker */
 
 }  // namespace fmcheck
diff --git a/src/theory/quantifiers/fmf/model_builder.cpp b/src/theory/quantifiers/fmf/model_builder.cpp
index d012bea8a..ab3dbea95 100644
--- a/src/theory/quantifiers/fmf/model_builder.cpp
+++ b/src/theory/quantifiers/fmf/model_builder.cpp
@@ -30,17 +30,27 @@ using namespace cvc5::theory;
 using namespace cvc5::theory::quantifiers;
 
 QModelBuilder::QModelBuilder(QuantifiersState& qs,
+                             QuantifiersInferenceManager& qim,
                              QuantifiersRegistry& qr,
-                             QuantifiersInferenceManager& qim)
+                             TermRegistry& tr)
     : TheoryEngineModelBuilder(),
       d_addedLemmas(0),
       d_triedLemmas(0),
       d_qstate(qs),
+      d_qim(qim),
       d_qreg(qr),
-      d_qim(qim)
+      d_treg(tr),
+      d_model(nullptr)
 {
 }
 
+void QModelBuilder::finishInit()
+{
+  // allocate the default model
+  d_modelAloc.reset(new FirstOrderModel(d_qstate, d_qreg, d_treg));
+  d_model = d_modelAloc.get();
+}
+
 bool QModelBuilder::optUseModel() {
   return options::mbqiMode() != options::MbqiMode::NONE || options::fmfBound();
 }
@@ -54,20 +64,23 @@ bool QModelBuilder::preProcessBuildModelStd(TheoryModel* m) {
   d_triedLemmas = 0;
   if (options::fmfFunWellDefinedRelevant())
   {
-    FirstOrderModel * fm = (FirstOrderModel*)m;
     //traverse equality engine
     std::map< TypeNode, bool > eqc_usort;
     eq::EqClassesIterator eqcs_i =
-        eq::EqClassesIterator(fm->getEqualityEngine());
+        eq::EqClassesIterator(m->getEqualityEngine());
     while( !eqcs_i.isFinished() ){
       TypeNode tr = (*eqcs_i).getType();
       eqc_usort[tr] = true;
       ++eqcs_i;
     }
     //look at quantified formulas
-    for( unsigned i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
-      Node q = fm->getAssertedQuantifier( i, true );
-      if( fm->isQuantifierActive( q ) ){
+    for (size_t i = 0, nquant = d_model->getNumAssertedQuantifiers();
+         i < nquant;
+         i++)
+    {
+      Node q = d_model->getAssertedQuantifier(i, true);
+      if (d_model->isQuantifierActive(q))
+      {
         //check if any of these quantified formulas can be set inactive
         if (q[0].getNumChildren() == 1)
         {
@@ -79,7 +92,7 @@ bool QModelBuilder::preProcessBuildModelStd(TheoryModel* m) {
             {
               Trace("model-engine-debug")
                   << "Irrelevant function definition : " << q << std::endl;
-              fm->setQuantifierActive( q, false );
+              d_model->setQuantifierActive(q, false);
             }
           }
         }
@@ -92,7 +105,7 @@ bool QModelBuilder::preProcessBuildModelStd(TheoryModel* m) {
 void QModelBuilder::debugModel( TheoryModel* m ){
   //debug the model: cycle through all instantiations for all quantifiers, report ones that are not true
   if( Trace.isOn("quant-check-model") ){
-    FirstOrderModel* fm = (FirstOrderModel*)m;
+    FirstOrderModel* fm = d_model;
     Trace("quant-check-model") << "Testing quantifier instantiations..." << std::endl;
     int tests = 0;
     int bad = 0;
@@ -105,7 +118,7 @@ void QModelBuilder::debugModel( TheoryModel* m ){
         vars.push_back( f[0][j] );
       }
       QRepBoundExt qrbe(qbi, fm);
-      RepSetIterator riter(fm->getRepSet(), &qrbe);
+      RepSetIterator riter(m->getRepSet(), &qrbe);
       if( riter.setQuantifier( f ) ){
         while( !riter.isFinished() ){
           tests++;
@@ -115,7 +128,7 @@ void QModelBuilder::debugModel( TheoryModel* m ){
             terms.push_back( riter.getCurrentTerm( k ) );
           }
           Node n = inst->getInstantiation(f, vars, terms);
-          Node val = fm->getValue( n );
+          Node val = m->getValue(n);
           if (!val.isConst() || !val.getConst<bool>())
           {
             Trace("quant-check-model") << "*******  Instantiation " << n << " for " << std::endl;
@@ -138,3 +151,4 @@ void QModelBuilder::debugModel( TheoryModel* m ){
     }
   }
 }
+FirstOrderModel* QModelBuilder::getModel() { return d_model; }
diff --git a/src/theory/quantifiers/fmf/model_builder.h b/src/theory/quantifiers/fmf/model_builder.h
index df866fbe1..cfccd4d93 100644
--- a/src/theory/quantifiers/fmf/model_builder.h
+++ b/src/theory/quantifiers/fmf/model_builder.h
@@ -30,6 +30,7 @@ class FirstOrderModel;
 class QuantifiersState;
 class QuantifiersRegistry;
 class QuantifiersInferenceManager;
+class TermRegistry;
 
 class QModelBuilder : public TheoryEngineModelBuilder
 {
@@ -43,9 +44,11 @@ class QModelBuilder : public TheoryEngineModelBuilder
 
  public:
   QModelBuilder(QuantifiersState& qs,
+                QuantifiersInferenceManager& qim,
                 QuantifiersRegistry& qr,
-                QuantifiersInferenceManager& qim);
-
+                TermRegistry& tr);
+  /** finish init, which sets the model object */
+  virtual void finishInit();
   //do exhaustive instantiation  
   // 0 :  failed, but resorting to true exhaustive instantiation may work
   // >0 : success
@@ -60,16 +63,22 @@ class QModelBuilder : public TheoryEngineModelBuilder
   //statistics 
   unsigned getNumAddedLemmas() { return d_addedLemmas; }
   unsigned getNumTriedLemmas() { return d_triedLemmas; }
+  /** get the model we are using */
+  FirstOrderModel* getModel();
 
  protected:
-  /** Pointer to quantifiers engine */
-  QuantifiersEngine* d_qe;
   /** The quantifiers state object */
   QuantifiersState& d_qstate;
+  /** The quantifiers inference manager */
+  QuantifiersInferenceManager& d_qim;
   /** Reference to the quantifiers registry */
   QuantifiersRegistry& d_qreg;
-  /** The quantifiers inference manager */
-  quantifiers::QuantifiersInferenceManager& d_qim;
+  /** Term registry */
+  TermRegistry& d_treg;
+  /** Pointer to the model object we are using */
+  FirstOrderModel* d_model;
+  /** The model object we have allocated */
+  std::unique_ptr<FirstOrderModel> d_modelAloc;
 };
 
 }  // namespace quantifiers
diff --git a/src/theory/quantifiers/quantifiers_modules.cpp b/src/theory/quantifiers/quantifiers_modules.cpp
index 704a65bfb..f6b8f30f4 100644
--- a/src/theory/quantifiers/quantifiers_modules.cpp
+++ b/src/theory/quantifiers/quantifiers_modules.cpp
@@ -28,7 +28,6 @@ QuantifiersModules::QuantifiersModules()
       d_alpha_equiv(nullptr),
       d_inst_engine(nullptr),
       d_model_engine(nullptr),
-      d_builder(nullptr),
       d_bint(nullptr),
       d_qcf(nullptr),
       d_sg_gen(nullptr),
@@ -45,6 +44,7 @@ void QuantifiersModules::initialize(QuantifiersState& qs,
                                     QuantifiersInferenceManager& qim,
                                     QuantifiersRegistry& qr,
                                     TermRegistry& tr,
+                                    QModelBuilder* builder,
                                     std::vector<QuantifiersModule*>& modules)
 {
   // add quantifiers modules
@@ -80,23 +80,10 @@ void QuantifiersModules::initialize(QuantifiersState& qs,
     d_bint.reset(new BoundedIntegers(qs, qim, qr, tr));
     modules.push_back(d_bint.get());
   }
+
   if (options::finiteModelFind() || options::fmfBound())
   {
-    Trace("quant-init-debug")
-        << "Initialize model engine, mbqi : " << options::mbqiMode() << " "
-        << options::fmfBound() << std::endl;
-    if (tr.useFmcModel())
-    {
-      Trace("quant-init-debug") << "...make fmc builder." << std::endl;
-      d_builder.reset(new fmcheck::FullModelChecker(qs, qr, qim));
-    }
-    else
-    {
-      Trace("quant-init-debug")
-          << "...make default model builder." << std::endl;
-      d_builder.reset(new QModelBuilder(qs, qr, qim));
-    }
-    d_model_engine.reset(new ModelEngine(qs, qim, qr, tr, d_builder.get()));
+    d_model_engine.reset(new ModelEngine(qs, qim, qr, tr, builder));
     modules.push_back(d_model_engine.get());
   }
   if (options::quantDynamicSplit() != options::QuantDSplitMode::NONE)
diff --git a/src/theory/quantifiers/quantifiers_modules.h b/src/theory/quantifiers/quantifiers_modules.h
index 659be0381..f41e81f34 100644
--- a/src/theory/quantifiers/quantifiers_modules.h
+++ b/src/theory/quantifiers/quantifiers_modules.h
@@ -61,6 +61,7 @@ class QuantifiersModules
                   QuantifiersInferenceManager& qim,
                   QuantifiersRegistry& qr,
                   TermRegistry& tr,
+                  QModelBuilder* builder,
                   std::vector<QuantifiersModule*>& modules);
 
  private:
@@ -74,8 +75,6 @@ class QuantifiersModules
   std::unique_ptr<InstantiationEngine> d_inst_engine;
   /** model engine */
   std::unique_ptr<ModelEngine> d_model_engine;
-  /** model builder */
-  std::unique_ptr<quantifiers::QModelBuilder> d_builder;
   /** bounded integers utility */
   std::unique_ptr<BoundedIntegers> d_bint;
   /** Conflict find mechanism for quantifiers */
diff --git a/src/theory/quantifiers/term_registry.cpp b/src/theory/quantifiers/term_registry.cpp
index 4e1aacbac..5b7bd1552 100644
--- a/src/theory/quantifiers/term_registry.cpp
+++ b/src/theory/quantifiers/term_registry.cpp
@@ -29,12 +29,12 @@ namespace quantifiers {
 
 TermRegistry::TermRegistry(QuantifiersState& qs, QuantifiersRegistry& qr)
     : d_presolve(qs.getUserContext(), true),
-      d_useFmcModel(false),
       d_presolveCache(qs.getUserContext()),
       d_termEnum(new TermEnumeration),
       d_termPools(new TermPools(qs)),
       d_termDb(new TermDb(qs, qr)),
-      d_sygusTdb(nullptr)
+      d_sygusTdb(nullptr),
+      d_qmodel(nullptr)
 {
   if (options::sygus() || options::sygusInst())
   {
@@ -44,27 +44,12 @@ TermRegistry::TermRegistry(QuantifiersState& qs, QuantifiersRegistry& qr)
   Trace("quant-engine-debug") << "Initialize quantifiers engine." << std::endl;
   Trace("quant-engine-debug")
       << "Initialize model, mbqi : " << options::mbqiMode() << std::endl;
-  // Finite model finding requires specialized ways of building the model.
-  // We require constructing the model here, since it is required for
-  // initializing the CombinationEngine and the rest of quantifiers engine.
-  if ((options::finiteModelFind() || options::fmfBound())
-      && (options::mbqiMode() == options::MbqiMode::FMC
-          || options::mbqiMode() == options::MbqiMode::TRUST
-          || options::fmfBound()))
-  {
-    d_useFmcModel = true;
-    d_qmodel.reset(new quantifiers::fmcheck::FirstOrderModelFmc(
-        qs, qr, *this, "FirstOrderModelFmc"));
-  }
-  else
-  {
-    d_qmodel.reset(
-        new quantifiers::FirstOrderModel(qs, qr, *this, "FirstOrderModel"));
-  }
 }
 
-void TermRegistry::finishInit(QuantifiersInferenceManager* qim)
+void TermRegistry::finishInit(FirstOrderModel* fm,
+                              QuantifiersInferenceManager* qim)
 {
+  d_qmodel = fm;
   d_termDb->finishInit(qim);
   if (d_sygusTdb.get())
   {
@@ -149,9 +134,7 @@ TermEnumeration* TermRegistry::getTermEnumeration() const
 
 TermPools* TermRegistry::getTermPools() const { return d_termPools.get(); }
 
-FirstOrderModel* TermRegistry::getModel() const { return d_qmodel.get(); }
-
-bool TermRegistry::useFmcModel() const { return d_useFmcModel; }
+FirstOrderModel* TermRegistry::getModel() const { return d_qmodel; }
 
 }  // namespace quantifiers
 }  // namespace theory
diff --git a/src/theory/quantifiers/term_registry.h b/src/theory/quantifiers/term_registry.h
index 5dfc3f78d..cf2ba7a47 100644
--- a/src/theory/quantifiers/term_registry.h
+++ b/src/theory/quantifiers/term_registry.h
@@ -45,7 +45,7 @@ class TermRegistry
   TermRegistry(QuantifiersState& qs,
                QuantifiersRegistry& qr);
   /** Finish init, which sets the inference manager on modules of this class */
-  void finishInit(QuantifiersInferenceManager* qim);
+  void finishInit(FirstOrderModel* fm, QuantifiersInferenceManager* qim);
   /** Presolve */
   void presolve();
 
@@ -79,9 +79,6 @@ class TermRegistry
   void processInstantiation(Node q, const std::vector<Node>& terms);
   void processSkolemization(Node q, const std::vector<Node>& skolems);
 
-  /** Whether we use the full model check builder and corresponding model */
-  bool useFmcModel() const;
-
   /** get term database */
   TermDb* getTermDatabase() const;
   /** get term database sygus */
@@ -109,7 +106,7 @@ class TermRegistry
   /** sygus term database */
   std::unique_ptr<TermDbSygus> d_sygusTdb;
   /** extended model object */
-  std::unique_ptr<FirstOrderModel> d_qmodel;
+  FirstOrderModel* d_qmodel;
 };
 
 }  // namespace quantifiers
diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp
index 27b16e411..6bfedb0a2 100644
--- a/src/theory/quantifiers/theory_quantifiers.cpp
+++ b/src/theory/quantifiers/theory_quantifiers.cpp
@@ -49,19 +49,9 @@ TheoryQuantifiers::TheoryQuantifiers(Context* c,
   out.handleUserAttribute( "quant-elim", this );
   out.handleUserAttribute( "quant-elim-partial", this );
 
-  // Finish initializing the term registry by hooking it up to the inference
-  // manager. This is required due to a cyclic dependency between the term
-  // database and the instantiate module. Term database needs inference manager
-  // since it sends out lemmas when term indexing is inconsistent, instantiate
-  // needs term database for entailment checks.
-  d_treg.finishInit(&d_qim);
-
   // construct the quantifiers engine
   d_qengine.reset(new QuantifiersEngine(d_qstate, d_qreg, d_treg, d_qim, pnm));
 
-  //!!!!!!!!!!!!!! temporary (project #15)
-  d_treg.getModel()->finishInit(d_qengine.get());
-
   // indicate we are using the quantifiers theory state object
   d_theoryState = &d_qstate;
   // use the inference manager as the official inference manager
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 5916390a6..2d1eeab84 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -44,21 +44,54 @@ namespace cvc5 {
 namespace theory {
 
 QuantifiersEngine::QuantifiersEngine(
-    quantifiers::QuantifiersState& qstate,
+    quantifiers::QuantifiersState& qs,
     quantifiers::QuantifiersRegistry& qr,
     quantifiers::TermRegistry& tr,
     quantifiers::QuantifiersInferenceManager& qim,
     ProofNodeManager* pnm)
-    : d_qstate(qstate),
+    : d_qstate(qs),
       d_qim(qim),
       d_te(nullptr),
       d_pnm(pnm),
       d_qreg(qr),
       d_treg(tr),
-      d_model(d_treg.getModel()),
-      d_quants_prereg(qstate.getUserContext()),
-      d_quants_red(qstate.getUserContext())
+      d_model(nullptr),
+      d_quants_prereg(qs.getUserContext()),
+      d_quants_red(qs.getUserContext())
 {
+  Trace("quant-init-debug")
+      << "Initialize model engine, mbqi : " << options::mbqiMode() << " "
+      << options::fmfBound() << std::endl;
+  // Finite model finding requires specialized ways of building the model.
+  // We require constructing the model here, since it is required for
+  // initializing the CombinationEngine and the rest of quantifiers engine.
+  if (options::fmfBound()
+      || (options::finiteModelFind()
+          && (options::mbqiMode() == options::MbqiMode::FMC
+              || options::mbqiMode() == options::MbqiMode::TRUST)))
+  {
+    Trace("quant-init-debug") << "...make fmc builder." << std::endl;
+    d_builder.reset(
+        new quantifiers::fmcheck::FullModelChecker(qs, qim, qr, tr));
+  }
+  else
+  {
+    Trace("quant-init-debug") << "...make default model builder." << std::endl;
+    d_builder.reset(new quantifiers::QModelBuilder(qs, qim, qr, tr));
+  }
+  // set the model object
+  d_builder->finishInit();
+  d_model = d_builder->getModel();
+
+  // Finish initializing the term registry by hooking it up to the model and the
+  // inference manager. The former is required since theories are not given
+  // access to the model in their constructors currently.
+  // The latter is required due to a cyclic dependency between the term
+  // database and the instantiate module. Term database needs inference manager
+  // since it sends out lemmas when term indexing is inconsistent, instantiate
+  // needs term database for entailment checks.
+  d_treg.finishInit(d_model, &d_qim);
+
   // initialize the utilities
   d_util.push_back(d_model->getEqualityQuery());
   // quantifiers registry must come before the remaining utilities
@@ -72,10 +105,13 @@ QuantifiersEngine::~QuantifiersEngine() {}
 
 void QuantifiersEngine::finishInit(TheoryEngine* te)
 {
+  // connect the quantifiers model to the underlying theory model
+  d_model->finishInit(te->getModel());
   d_te = te;
   // Initialize the modules and the utilities here.
   d_qmodules.reset(new quantifiers::QuantifiersModules);
-  d_qmodules->initialize(d_qstate, d_qim, d_qreg, d_treg, d_modules);
+  d_qmodules->initialize(
+      d_qstate, d_qim, d_qreg, d_treg, d_builder.get(), d_modules);
   if (d_qmodules->d_rel_dom.get())
   {
     d_util.push_back(d_qmodules->d_rel_dom.get());
@@ -95,11 +131,7 @@ quantifiers::QuantifiersRegistry& QuantifiersEngine::getQuantifiersRegistry()
 
 quantifiers::QModelBuilder* QuantifiersEngine::getModelBuilder() const
 {
-  return d_qmodules->d_builder.get();
-}
-quantifiers::FirstOrderModel* QuantifiersEngine::getModel() const
-{
-  return d_model;
+  return d_builder.get();
 }
 
 /// !!!!!!!!!!!!!! temporary (project #15)
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index fd4889154..631f7bec1 100644
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -69,8 +69,6 @@ class QuantifiersEngine {
   //---------------------- utilities
   /** get the model builder */
   quantifiers::QModelBuilder* getModelBuilder() const;
-  /** get model */
-  quantifiers::FirstOrderModel* getModel() const;
   /** get term database sygus */
   quantifiers::TermDbSygus* getTermDatabaseSygus() const;
   //---------------------- end utilities
@@ -194,6 +192,8 @@ public:
   quantifiers::QuantifiersRegistry& d_qreg;
   /** The term registry */
   quantifiers::TermRegistry& d_treg;
+  /** model builder */
+  std::unique_ptr<quantifiers::QModelBuilder> d_builder;
   /** extended model object */
   quantifiers::FirstOrderModel* d_model;
   //------------- end quantifiers utilities
diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp
index 40a64cb35..1543739e0 100644
--- a/src/theory/theory_model.cpp
+++ b/src/theory/theory_model.cpp
@@ -681,6 +681,18 @@ bool TheoryModel::areDisequal(TNode a, TNode b)
   }
 }
 
+bool TheoryModel::hasUfTerms(Node f) const
+{
+  return d_uf_terms.find(f) != d_uf_terms.end();
+}
+
+const std::vector<Node>& TheoryModel::getUfTerms(Node f) const
+{
+  const auto it = d_uf_terms.find(f);
+  Assert(it != d_uf_terms.end());
+  return it->second;
+}
+
 bool TheoryModel::areFunctionValuesEnabled() const
 {
   return d_enableFuncModels;
diff --git a/src/theory/theory_model.h b/src/theory/theory_model.h
index 42392c522..b4a089767 100644
--- a/src/theory/theory_model.h
+++ b/src/theory/theory_model.h
@@ -328,10 +328,10 @@ public:
   Cardinality getCardinality(TypeNode t) const;
 
   //---------------------------- function values
-  /** a map from functions f to a list of all APPLY_UF terms with operator f */
-  std::map< Node, std::vector< Node > > d_uf_terms;
-  /** a map from functions f to a list of all HO_APPLY terms with first argument f */
-  std::map< Node, std::vector< Node > > d_ho_uf_terms;
+  /** Does this model have terms for the given uninterpreted function? */
+  bool hasUfTerms(Node f) const;
+  /** Get the terms for uninterpreted function f */
+  const std::vector<Node>& getUfTerms(Node f) const;
   /** are function values enabled? */
   bool areFunctionValuesEnabled() const;
   /** assign function value f to definition f_def */
@@ -423,6 +423,11 @@ public:
   //---------------------------- end separation logic
 
   //---------------------------- function values
+  /** a map from functions f to a list of all APPLY_UF terms with operator f */
+  std::map<Node, std::vector<Node> > d_uf_terms;
+  /** a map from functions f to a list of all HO_APPLY terms with first argument
+   * f */
+  std::map<Node, std::vector<Node> > d_ho_uf_terms;
   /** whether function models are enabled */
   bool d_enableFuncModels;
   /** map from function terms to the (lambda) definitions