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.

6 files changed, 93 insertions, 60 deletions

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