Eliminate dependency on quantifiers engine in quantifiers model (#6165)

diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp
index 44c42b305ffc778ae1fa3a938687dcf97e957f09..001c2f62a55af2422da1c91a808bcd467a184889 100644 (file)
--- a/src/theory/quantifiers/first_order_model.cpp
+++ b/src/theory/quantifiers/first_order_model.cpp
@@ -20,8 +20,8 @@
 #include "theory/quantifiers/quantifiers_attributes.h"
 #include "theory/quantifiers/term_database.h"
 #include "theory/quantifiers/term_enumeration.h"
+#include "theory/quantifiers/term_registry.h"
 #include "theory/quantifiers/term_util.h"
-#include "theory/quantifiers_engine.h"
 
 using namespace std;
 using namespace CVC4::kind;
@@ -32,18 +32,33 @@ namespace CVC4 {
 namespace theory {
 namespace quantifiers {
 
-FirstOrderModel::FirstOrderModel(QuantifiersEngine* qe,
-                                 QuantifiersState& qs,
+struct ModelBasisAttributeId
+{
+};
+using ModelBasisAttribute = expr::Attribute<ModelBasisAttributeId, bool>;
+// for APPLY_UF terms, 1 : term has direct child with model basis attribute,
+//                     0 : term has no direct child with model basis attribute.
+struct ModelBasisArgAttributeId
+{
+};
+using ModelBasisArgAttribute = expr::Attribute<ModelBasisArgAttributeId, uint64_t>;
+
+FirstOrderModel::FirstOrderModel(QuantifiersState& qs,
                                  QuantifiersRegistry& qr,
+                                 TermRegistry& tr,
                                  std::string name)
     : TheoryModel(qs.getSatContext(), name, true),
-      d_qe(qe),
+      d_qe(nullptr),
       d_qreg(qr),
+      d_treg(tr),
       d_forall_asserts(qs.getSatContext()),
       d_forallRlvComputed(false)
 {
 }
 
+//!!!!!!!!!!!!!!!!!!!!! temporary (project #15)
+void FirstOrderModel::finishInit(QuantifiersEngine* qe) { d_qe = qe; }
+
 void FirstOrderModel::assertQuantifier( Node n ){
   if( n.getKind()==FORALL ){
     d_forall_asserts.push_back( n );
@@ -143,6 +158,11 @@ bool FirstOrderModel::initializeRepresentativesForType(TypeNode tn)
   }
 }
 
+bool FirstOrderModel::isModelBasis(TNode n)
+{
+  return n.getAttribute(ModelBasisAttribute());
+}
+
 /** needs check */
 bool FirstOrderModel::checkNeeded() {
   return d_forall_asserts.size()>0;
@@ -237,13 +257,13 @@ Node FirstOrderModel::getModelBasisTerm(TypeNode tn)
     Node mbt;
     if (tn.isClosedEnumerable())
     {
-      mbt = d_qe->getTermEnumeration()->getEnumerateTerm(tn, 0);
+      mbt = d_treg.getTermEnumeration()->getEnumerateTerm(tn, 0);
     }
     else
     {
       if (options::fmfFreshDistConst())
       {
-        mbt = d_qe->getTermDatabase()->getOrMakeTypeFreshVariable(tn);
+        mbt = d_treg.getTermDatabase()->getOrMakeTypeFreshVariable(tn);
       }
       else
       {
@@ -251,7 +271,7 @@ Node FirstOrderModel::getModelBasisTerm(TypeNode tn)
         // may produce an inconsistent model by choosing an arbitrary
         // equivalence class for it. Hence, we require that it be an existing or
         // fresh variable.
-        mbt = d_qe->getTermDatabase()->getOrMakeTypeGroundTerm(tn, true);
+        mbt = d_treg.getTermDatabase()->getOrMakeTypeGroundTerm(tn, true);
       }
     }
     ModelBasisAttribute mba;

diff --git a/src/theory/quantifiers/first_order_model.h b/src/theory/quantifiers/first_order_model.h
index 484d7738ae3a922bcdfc61aed946e0e3df7d5398..c2660d9335d9dde4313bfc6ca16a23ebf0c021b2 100644 (file)
--- a/src/theory/quantifiers/first_order_model.h
+++ b/src/theory/quantifiers/first_order_model.h
@@ -27,22 +27,10 @@ namespace theory {
 
 class QuantifiersEngine;
 
-struct ModelBasisAttributeId
-{
-};
-typedef expr::Attribute<ModelBasisAttributeId, bool> ModelBasisAttribute;
-// for APPLY_UF terms, 1 : term has direct child with model basis attribute,
-//                     0 : term has no direct child with model basis attribute.
-struct ModelBasisArgAttributeId
-{
-};
-typedef expr::Attribute<ModelBasisArgAttributeId, uint64_t>
-    ModelBasisArgAttribute;
-
 namespace quantifiers {
 
-class TermDb;
 class QuantifiersState;
+class TermRegistry;
 class QuantifiersRegistry;
 
 namespace fmcheck {
@@ -56,12 +44,15 @@ typedef expr::Attribute<IsStarAttributeId, bool> IsStarAttribute;
 class FirstOrderModel : public TheoryModel
 {
  public:
-  FirstOrderModel(QuantifiersEngine* qe,
-                  QuantifiersState& qs,
+  FirstOrderModel(QuantifiersState& qs,
                   QuantifiersRegistry& qr,
+                  TermRegistry& tr,
                   std::string name);
 
-  virtual fmcheck::FirstOrderModelFmc* asFirstOrderModelFmc() { return nullptr; }
+  //!!!!!!!!!!!!!!!!!!!!! temporary (project #15)
+  /** finish initialize */
+  void finishInit(QuantifiersEngine* qe);
+
   /** assert quantifier */
   void assertQuantifier( Node n );
   /** get number of asserted quantifiers */
@@ -132,12 +123,18 @@ class FirstOrderModel : public TheoryModel
    * has all representatives of type tn.
    */
   bool initializeRepresentativesForType(TypeNode tn);
+  /**
+   * Has the term been marked as a model basis term?
+   */
+  static bool isModelBasis(TNode n);
 
  protected:
-  /** quant engine */
+  //!!!!!!!!!!!!!!!!!!!!!!! TODO (project #15): temporarily available
   QuantifiersEngine* d_qe;
   /** The quantifiers registry */
   QuantifiersRegistry& d_qreg;
+  /** Reference to the term registry */
+  TermRegistry& d_treg;
   /** list of quantifiers asserted in the current context */
   context::CDList<Node> d_forall_asserts;
   /** 

diff --git a/src/theory/quantifiers/fmf/first_order_model_fmc.cpp b/src/theory/quantifiers/fmf/first_order_model_fmc.cpp
index 5ce5eecfc77314ca42296d10503bedb745bfd82b..252261b9cc8b08bdee01a46e5a4d3071f790c43f 100644 (file)
--- a/src/theory/quantifiers/fmf/first_order_model_fmc.cpp
+++ b/src/theory/quantifiers/fmf/first_order_model_fmc.cpp
@@ -24,11 +24,11 @@ namespace theory {
 namespace quantifiers {
 namespace fmcheck {
 
-FirstOrderModelFmc::FirstOrderModelFmc(QuantifiersEngine* qe,
-                                       QuantifiersState& qs,
+FirstOrderModelFmc::FirstOrderModelFmc(QuantifiersState& qs,
                                        QuantifiersRegistry& qr,
+                                       TermRegistry& tr,
                                        std::string name)
-    : FirstOrderModel(qe, qs, qr, name)
+    : FirstOrderModel(qs, qr, tr, name)
 {
 }
 

diff --git a/src/theory/quantifiers/fmf/first_order_model_fmc.h b/src/theory/quantifiers/fmf/first_order_model_fmc.h
index 8f371a96b2a334c610279e63c4f23b735fb0e3a5..d8ae054ad68a90affa21cd32b7162d301b123d50 100644 (file)
--- a/src/theory/quantifiers/fmf/first_order_model_fmc.h
+++ b/src/theory/quantifiers/fmf/first_order_model_fmc.h
@@ -38,17 +38,16 @@ class FirstOrderModelFmc : public FirstOrderModel
   void processInitializeModelForTerm(Node n) override;
 
  public:
-  FirstOrderModelFmc(QuantifiersEngine* qe,
-                     QuantifiersState& qs,
+  FirstOrderModelFmc(QuantifiersState& qs,
                      QuantifiersRegistry& qr,
+                     TermRegistry& tr,
                      std::string name);
   ~FirstOrderModelFmc() override;
-  FirstOrderModelFmc* asFirstOrderModelFmc() override { return this; }
   // initialize the model
   void processInitialize(bool ispre) override;
   Node getFunctionValue(Node op, const char* argPrefix);
 
-  bool isStar(Node n);
+  static bool isStar(Node n);
   Node getStar(TypeNode tn);
 }; /* class FirstOrderModelFmc */
 

diff --git a/src/theory/quantifiers/fmf/full_model_check.cpp b/src/theory/quantifiers/fmf/full_model_check.cpp
index abcd5a7944ba29d71b58a415f2558dc6f2fa4f96..be83f3b10966f4022bd92be3f5ad39317d656f70 100644 (file)
--- a/src/theory/quantifiers/fmf/full_model_check.cpp
+++ b/src/theory/quantifiers/fmf/full_model_check.cpp
@@ -284,10 +284,9 @@ void Def::debugPrint(const char * tr, Node op, FullModelChecker * m) {
   }
 }
 
-FullModelChecker::FullModelChecker(QuantifiersEngine* qe,
-                                   QuantifiersState& qs,
+FullModelChecker::FullModelChecker(QuantifiersState& qs,
                                    QuantifiersRegistry& qr)
-    : QModelBuilder(qe, qs, qr)
+    : QModelBuilder(qs, qr)
 {
   d_true = NodeManager::currentNM()->mkConst(true);
   d_false = NodeManager::currentNM()->mkConst(false);
@@ -298,8 +297,8 @@ bool FullModelChecker::preProcessBuildModel(TheoryModel* m) {
   if( !preProcessBuildModelStd( m ) ){
     return false;
   }
-  
-  FirstOrderModelFmc * fm = ((FirstOrderModelFmc*)m)->asFirstOrderModelFmc();
+
+  FirstOrderModelFmc* fm = (FirstOrderModelFmc*)m;
   Trace("fmc") << "---Full Model Check preprocess() " << std::endl;
   d_preinitialized_eqc.clear();
   d_preinitialized_types.clear();
@@ -346,7 +345,7 @@ bool FullModelChecker::processBuildModel(TheoryModel* m){
     // nothing to do if no functions
     return true;
   }
-  FirstOrderModelFmc * fm = ((FirstOrderModelFmc*)m)->asFirstOrderModelFmc();
+  FirstOrderModelFmc* fm = (FirstOrderModelFmc*)m;
   Trace("fmc") << "---Full Model Check reset() " << std::endl;
   d_quant_models.clear();
   d_rep_ids.clear();
@@ -573,11 +572,11 @@ void FullModelChecker::debugPrintCond(const char * tr, Node n, bool dispStar) {
 }
 
 void FullModelChecker::debugPrint(const char * tr, Node n, bool dispStar) {
-  FirstOrderModelFmc * fm = (FirstOrderModelFmc *)d_qe->getModel();
   if( n.isNull() ){
     Trace(tr) << "null";
   }
-  else if(fm->isStar(n) && dispStar) {
+  else if (FirstOrderModelFmc::isStar(n) && dispStar)
+  {
     Trace(tr) << "*";
   }
   else
@@ -607,7 +606,7 @@ int FullModelChecker::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, i
   {
     return 0;
   }
-  FirstOrderModelFmc* fmfmc = fm->asFirstOrderModelFmc();
+  FirstOrderModelFmc* fmfmc = static_cast<FirstOrderModelFmc*>(fm);
   if (effort == 0)
   {
     if (options::mbqiMode() == options::MbqiMode::NONE)

diff --git a/src/theory/quantifiers/fmf/full_model_check.h b/src/theory/quantifiers/fmf/full_model_check.h
index b3c55ee7ac3426af552ce562c2bb6dd5855e062a..904a1b9a088d7b06d6159e9ddce3bcca30c0c1e1 100644 (file)
--- a/src/theory/quantifiers/fmf/full_model_check.h
+++ b/src/theory/quantifiers/fmf/full_model_check.h
@@ -154,9 +154,7 @@ protected:
   Node getSomeDomainElement( FirstOrderModelFmc * fm, TypeNode tn );
 
  public:
-  FullModelChecker(QuantifiersEngine* qe,
-                   QuantifiersState& qs,
-                   QuantifiersRegistry& qr);
+  FullModelChecker(QuantifiersState& qs, QuantifiersRegistry& qr);
 
   void debugPrintCond(const char * tr, Node n, bool dispStar = false);
   void debugPrint(const char * tr, Node n, bool dispStar = false);

diff --git a/src/theory/quantifiers/fmf/model_builder.cpp b/src/theory/quantifiers/fmf/model_builder.cpp
index 89e4fa29d958fcf3a3a2ee0c755b01a30e6ccba6..9aa687fbd6ec129f6b5fa35b37e2ea1689f76c7d 100644 (file)
--- a/src/theory/quantifiers/fmf/model_builder.cpp
+++ b/src/theory/quantifiers/fmf/model_builder.cpp
@@ -30,13 +30,11 @@ using namespace CVC4::context;
 using namespace CVC4::theory;
 using namespace CVC4::theory::quantifiers;
 
-QModelBuilder::QModelBuilder(QuantifiersEngine* qe,
-                             QuantifiersState& qs,
-                             QuantifiersRegistry& qr)
+QModelBuilder::QModelBuilder(QuantifiersState& qs, QuantifiersRegistry& qr)
     : TheoryEngineModelBuilder(),
-      d_qe(qe),
       d_addedLemmas(0),
       d_triedLemmas(0),
+      d_qe(nullptr),
       d_qstate(qs),
       d_qreg(qr)
 {

diff --git a/src/theory/quantifiers/fmf/model_builder.h b/src/theory/quantifiers/fmf/model_builder.h
index 534226a7c037b4e9314bbefa85fdbae8ee47cbd8..7ba7a66e2c1bee63b960e856c74f5077c6cf77ac 100644 (file)
--- a/src/theory/quantifiers/fmf/model_builder.h
+++ b/src/theory/quantifiers/fmf/model_builder.h
@@ -32,8 +32,6 @@ class QuantifiersRegistry;
 class QModelBuilder : public TheoryEngineModelBuilder
 {
  protected:
-  //quantifiers engine
-  QuantifiersEngine* d_qe;
   // must call preProcessBuildModelStd
   bool preProcessBuildModel(TheoryModel* m) override;
   bool preProcessBuildModelStd(TheoryModel* m);
@@ -42,9 +40,9 @@ class QModelBuilder : public TheoryEngineModelBuilder
   unsigned d_triedLemmas;
 
  public:
-  QModelBuilder(QuantifiersEngine* qe,
-                QuantifiersState& qs,
-                QuantifiersRegistry& qr);
+  QModelBuilder(QuantifiersState& qs, QuantifiersRegistry& qr);
+  //!!!!!!!!!!!!!!!!!!!!! temporary (project #15)
+  void finishInit(QuantifiersEngine* qe) { d_qe = qe; }
 
   //do exhaustive instantiation  
   // 0 :  failed, but resorting to true exhaustive instantiation may work
@@ -62,6 +60,8 @@ class QModelBuilder : public TheoryEngineModelBuilder
   unsigned getNumTriedLemmas() { return d_triedLemmas; }
 
  protected:
+  /** Pointer to quantifiers engine */
+  QuantifiersEngine* d_qe;
   /** The quantifiers state object */
   QuantifiersState& d_qstate;
   /** Reference to the quantifiers registry */

diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 1784b976ed1568814c988e818fe8b1d113ad482b..d6aaeed3f414edfc9a4e99c9ae153c9694e8d10f 100644 (file)
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -72,7 +72,7 @@ QuantifiersEngine::QuantifiersEngine(
   //---- utilities
   // quantifiers registry must come before the other utilities
   d_util.push_back(&d_qreg);
-  d_util.push_back(d_treg.getTermDatabase());
+  d_util.push_back(tr.getTermDatabase());
 
   d_util.push_back(d_instantiate.get());
 
@@ -93,19 +93,22 @@ QuantifiersEngine::QuantifiersEngine(
     {
       Trace("quant-engine-debug") << "...make fmc builder." << std::endl;
       d_model.reset(new quantifiers::fmcheck::FirstOrderModelFmc(
-          this, qstate, qr, "FirstOrderModelFmc"));
-      d_builder.reset(
-          new quantifiers::fmcheck::FullModelChecker(this, qstate, qr));
+          qstate, qr, tr, "FirstOrderModelFmc"));
+      d_builder.reset(new quantifiers::fmcheck::FullModelChecker(qstate, qr));
     }else{
       Trace("quant-engine-debug") << "...make default model builder." << std::endl;
-      d_model.reset(new quantifiers::FirstOrderModel(
-          this, qstate, qr, "FirstOrderModel"));
-      d_builder.reset(new quantifiers::QModelBuilder(this, qstate, qr));
+      d_model.reset(
+          new quantifiers::FirstOrderModel(qstate, qr, tr, "FirstOrderModel"));
+      d_builder.reset(new quantifiers::QModelBuilder(qstate, qr));
     }
+    d_builder->finishInit(this);
   }else{
-    d_model.reset(new quantifiers::FirstOrderModel(
-        this, qstate, d_qreg, "FirstOrderModel"));
+    d_model.reset(
+        new quantifiers::FirstOrderModel(qstate, qr, tr, "FirstOrderModel"));
   }
+  //!!!!!!!!!!!!!!!!!!!!! temporary (project #15)
+  d_model->finishInit(this);
+  // initialize the equality query
   d_eq_query.reset(
       new quantifiers::EqualityQueryQuantifiersEngine(qstate, d_model.get()));
   d_util.insert(d_util.begin(), d_eq_query.get());

diff --git a/src/theory/uf/theory_uf_model.cpp b/src/theory/uf/theory_uf_model.cpp
index 393f1f705b9311bce5ccc51e292242d5a1d37eac..abb0c2e6c862907dcb8e07ad99bdbc11db55b3da 100644 (file)
--- a/src/theory/uf/theory_uf_model.cpp
+++ b/src/theory/uf/theory_uf_model.cpp
@@ -45,7 +45,11 @@ void UfModelTreeNode::setValue( TheoryModel* m, Node n, Node v, std::vector< int
   if( argIndex<(int)indexOrder.size() ){
     //take r = null when argument is the model basis
     Node r;
-    if( ground || ( !n.isNull() && !n[ indexOrder[argIndex] ].getAttribute(ModelBasisAttribute()) ) ){
+    if (ground
+        || (!n.isNull()
+            && !quantifiers::FirstOrderModel::isModelBasis(
+                   n[indexOrder[argIndex]])))
+    {
       r = m->getRepresentative( n[ indexOrder[argIndex] ] );
     }
     d_data[ r ].setValue( m, n, v, indexOrder, ground, argIndex+1 );