Introduce quantifiers term registry (#5983)

This groups utilities related to ground terms into TermRegistry which will be passed to quantifier modules.

8 files changed, 202 insertions, 101 deletions

diff --git a/src/theory/quantifiers/equality_query.cpp b/src/theory/quantifiers/equality_query.cpp
index def27fe5a..60cc08bdc 100644
--- a/src/theory/quantifiers/equality_query.cpp
+++ b/src/theory/quantifiers/equality_query.cpp
@@ -17,7 +17,6 @@
 #include "options/quantifiers_options.h"
 #include "theory/quantifiers/first_order_model.h"
 #include "theory/quantifiers/quantifiers_attributes.h"
-#include "theory/quantifiers/term_database.h"
 #include "theory/quantifiers/term_util.h"
 
 using namespace std;
@@ -29,9 +28,8 @@ namespace theory {
 namespace quantifiers {
 
 EqualityQueryQuantifiersEngine::EqualityQueryQuantifiersEngine(
-    QuantifiersState& qs, TermDb* tdb, FirstOrderModel* m)
+    QuantifiersState& qs, FirstOrderModel* m)
     : d_qstate(qs),
-      d_tdb(tdb),
       d_model(m),
       d_eqi_counter(qs.getSatContext()),
       d_reset_count(0)
diff --git a/src/theory/quantifiers/equality_query.h b/src/theory/quantifiers/equality_query.h
index 9944bf703..86b07a643 100644
--- a/src/theory/quantifiers/equality_query.h
+++ b/src/theory/quantifiers/equality_query.h
@@ -27,7 +27,6 @@ namespace CVC4 {
 namespace theory {
 namespace quantifiers {
 
-class TermDb;
 class FirstOrderModel;
 
 /** EqualityQueryQuantifiersEngine class
@@ -44,7 +43,6 @@ class EqualityQueryQuantifiersEngine : public QuantifiersUtil
 {
  public:
   EqualityQueryQuantifiersEngine(QuantifiersState& qs,
-                                 TermDb* tdb,
                                  FirstOrderModel* m);
   virtual ~EqualityQueryQuantifiersEngine();
   /** reset */
@@ -72,8 +70,6 @@ class EqualityQueryQuantifiersEngine : public QuantifiersUtil
  private:
   /** the quantifiers state */
   QuantifiersState& d_qstate;
-  /** Pointer to the term database */
-  TermDb* d_tdb;
   /** Pointer to the model */
   FirstOrderModel* d_model;
   /** quantifiers equality inference */
diff --git a/src/theory/quantifiers/sygus/term_database_sygus.cpp b/src/theory/quantifiers/sygus/term_database_sygus.cpp
index f393601ad..275e9a27f 100644
--- a/src/theory/quantifiers/sygus/term_database_sygus.cpp
+++ b/src/theory/quantifiers/sygus/term_database_sygus.cpp
@@ -21,14 +21,11 @@
 #include "options/datatypes_options.h"
 #include "options/quantifiers_options.h"
 #include "printer/printer.h"
-#include "theory/arith/arith_msum.h"
 #include "theory/datatypes/sygus_datatype_utils.h"
 #include "theory/quantifiers/quantifiers_attributes.h"
 #include "theory/quantifiers/quantifiers_inference_manager.h"
 #include "theory/quantifiers/quantifiers_state.h"
-#include "theory/quantifiers/term_database.h"
 #include "theory/quantifiers/term_util.h"
-#include "theory/quantifiers_engine.h"
 
 using namespace CVC4::kind;
 
@@ -49,11 +46,8 @@ std::ostream& operator<<(std::ostream& os, EnumeratorRole r)
   return os;
 }
 
-TermDbSygus::TermDbSygus(QuantifiersEngine* qe,
-                         QuantifiersState& qs,
-                         QuantifiersInferenceManager& qim)
-    : d_quantEngine(qe),
-      d_qstate(qs),
+TermDbSygus::TermDbSygus(QuantifiersState& qs, QuantifiersInferenceManager& qim)
+    : d_qstate(qs),
       d_qim(qim),
       d_syexp(new SygusExplain(this)),
       d_ext_rw(new ExtendedRewriter(true)),
diff --git a/src/theory/quantifiers/sygus/term_database_sygus.h b/src/theory/quantifiers/sygus/term_database_sygus.h
index ba09c723f..013922c94 100644
--- a/src/theory/quantifiers/sygus/term_database_sygus.h
+++ b/src/theory/quantifiers/sygus/term_database_sygus.h
@@ -54,9 +54,7 @@ std::ostream& operator<<(std::ostream& os, EnumeratorRole r);
 // TODO :issue #1235 split and document this class
 class TermDbSygus {
  public:
-  TermDbSygus(QuantifiersEngine* qe,
-              QuantifiersState& qs,
-              QuantifiersInferenceManager& qim);
+  TermDbSygus(QuantifiersState& qs, QuantifiersInferenceManager& qim);
   ~TermDbSygus() {}
   /** Reset this utility */
   bool reset(Theory::Effort e);
@@ -316,8 +314,6 @@ class TermDbSygus {
   static void toStreamSygus(std::ostream& out, Node n);
   
  private:
-  /** reference to the quantifiers engine */
-  QuantifiersEngine* d_quantEngine;
   /** Reference to the quantifiers state */
   QuantifiersState& d_qstate;
   /** The quantifiers inference manager */
diff --git a/src/theory/quantifiers/term_registry.cpp b/src/theory/quantifiers/term_registry.cpp
new file mode 100644
index 000000000..40e45ae35
--- /dev/null
+++ b/src/theory/quantifiers/term_registry.cpp
@@ -0,0 +1,93 @@
+/*********************                                                        */
+/*! \file term_registry.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** in the top-level source directory and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief term registry class
+ **/
+
+#include "theory/quantifiers/term_registry.h"
+
+#include "options/quantifiers_options.h"
+#include "options/smt_options.h"
+#include "theory/quantifiers/quantifiers_state.h"
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+TermRegistry::TermRegistry(QuantifiersState& qs,
+                           QuantifiersInferenceManager& qim,
+                           QuantifiersRegistry& qr)
+    : d_presolve(qs.getUserContext(), true),
+      d_presolveCache(qs.getUserContext()),
+      d_termEnum(new TermEnumeration),
+      d_termDb(new TermDb(qs, qim, qr)),
+      d_sygusTdb(nullptr)
+{
+  if (options::sygus() || options::sygusInst())
+  {
+    // must be constructed here since it is required for datatypes finistInit
+    d_sygusTdb.reset(new TermDbSygus(qs, qim));
+  }
+}
+
+void TermRegistry::presolve()
+{
+  d_termDb->presolve();
+  d_presolve = false;
+  // add all terms to database
+  if (options::incrementalSolving() && !options::termDbCd())
+  {
+    Trace("quant-engine-proc")
+        << "Add presolve cache " << d_presolveCache.size() << std::endl;
+    for (const Node& t : d_presolveCache)
+    {
+      addTerm(t);
+    }
+    Trace("quant-engine-proc") << "Done add presolve cache " << std::endl;
+  }
+}
+
+void TermRegistry::addTerm(Node n, bool withinQuant)
+{
+  // don't add terms in quantifier bodies
+  if (withinQuant && !options::registerQuantBodyTerms())
+  {
+    return;
+  }
+  if (options::incrementalSolving() && !options::termDbCd())
+  {
+    d_presolveCache.insert(n);
+  }
+  // only wait if we are doing incremental solving
+  if (!d_presolve || !options::incrementalSolving() || options::termDbCd())
+  {
+    d_termDb->addTerm(n);
+    if (d_sygusTdb.get() && options::sygusEvalUnfold())
+    {
+      d_sygusTdb->getEvalUnfold()->registerEvalTerm(n);
+    }
+  }
+}
+
+TermDb* TermRegistry::getTermDatabase() const { return d_termDb.get(); }
+
+TermDbSygus* TermRegistry::getTermDatabaseSygus() const
+{
+  return d_sygusTdb.get();
+}
+
+TermEnumeration* TermRegistry::getTermEnumeration() const
+{
+  return d_termEnum.get();
+}
+}  // namespace quantifiers
+}  // namespace theory
+}  // namespace CVC4
diff --git a/src/theory/quantifiers/term_registry.h b/src/theory/quantifiers/term_registry.h
new file mode 100644
index 000000000..83c89f5e7
--- /dev/null
+++ b/src/theory/quantifiers/term_registry.h
@@ -0,0 +1,80 @@
+/*********************                                                        */
+/*! \file term_registry.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** in the top-level source directory and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief term registry class
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__THEORY__QUANTIFIERS__TERM_REGISTRY_H
+#define CVC4__THEORY__QUANTIFIERS__TERM_REGISTRY_H
+
+#include <map>
+#include <unordered_set>
+
+#include "context/cdhashset.h"
+#include "theory/quantifiers/sygus/term_database_sygus.h"
+#include "theory/quantifiers/term_database.h"
+#include "theory/quantifiers/term_enumeration.h"
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+/**
+ * Term Registry, which manages notifying modules within quantifiers about
+ * (ground) terms that exist in the current context.
+ */
+class TermRegistry
+{
+  using NodeSet = context::CDHashSet<Node, NodeHashFunction>;
+
+ public:
+  TermRegistry(QuantifiersState& qs,
+               QuantifiersInferenceManager& qim,
+               QuantifiersRegistry& qr);
+  /** Presolve */
+  void presolve();
+
+  /**
+   * Add term n, which notifies the term database that the ground term n
+   * exists in the current context.
+   *
+   * @param n the term to add
+   * @param withinQuant whether n occurs within a quantified formula body
+   */
+  void addTerm(Node n, bool withinQuant = false);
+
+  /** get term database */
+  TermDb* getTermDatabase() const;
+  /** get term database sygus */
+  TermDbSygus* getTermDatabaseSygus() const;
+  /** get term enumeration utility */
+  TermEnumeration* getTermEnumeration() const;
+
+ private:
+  /** has presolve been called */
+  context::CDO<bool> d_presolve;
+  /** the set of terms we have seen before presolve */
+  NodeSet d_presolveCache;
+  /** term enumeration utility */
+  std::unique_ptr<TermEnumeration> d_termEnum;
+  /** term database */
+  std::unique_ptr<TermDb> d_termDb;
+  /** sygus term database */
+  std::unique_ptr<TermDbSygus> d_sygusTdb;
+};
+
+}  // namespace quantifiers
+}  // namespace theory
+}  // namespace CVC4
+
+#endif /* CVC4__THEORY__QUANTIFIERS__TERM_REGISTRY_H */
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 79422b418..f9982b536 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -55,32 +55,21 @@ QuantifiersEngine::QuantifiersEngine(
       d_decManager(nullptr),
       d_pnm(pnm),
       d_qreg(),
+      d_treg(qstate, qim, d_qreg),
       d_tr_trie(new inst::TriggerTrie),
       d_model(nullptr),
       d_builder(nullptr),
-      d_term_db(new quantifiers::TermDb(qstate, qim, d_qreg)),
       d_eq_query(nullptr),
-      d_sygus_tdb(nullptr),
       d_instantiate(
           new quantifiers::Instantiate(this, qstate, qim, d_qreg, pnm)),
       d_skolemize(new quantifiers::Skolemize(d_qstate, d_pnm)),
-      d_term_enum(new quantifiers::TermEnumeration),
       d_quants_prereg(qstate.getUserContext()),
-      d_quants_red(qstate.getUserContext()),
-      d_presolve(qstate.getUserContext(), true),
-      d_presolve_in(qstate.getUserContext()),
-      d_presolve_cache(qstate.getUserContext())
+      d_quants_red(qstate.getUserContext())
 {
   //---- utilities
   // quantifiers registry must come before the other utilities
   d_util.push_back(&d_qreg);
-  d_util.push_back(d_term_db.get());
-
-  if (options::sygus() || options::sygusInst())
-  {
-    // must be constructed here since it is required for datatypes finistInit
-    d_sygus_tdb.reset(new quantifiers::TermDbSygus(this, qstate, qim));
-  }
+  d_util.push_back(d_treg.getTermDatabase());
 
   d_util.push_back(d_instantiate.get());
 
@@ -113,8 +102,8 @@ QuantifiersEngine::QuantifiersEngine(
     d_model.reset(new quantifiers::FirstOrderModel(
         this, qstate, d_qreg, "FirstOrderModel"));
   }
-  d_eq_query.reset(new quantifiers::EqualityQueryQuantifiersEngine(
-      qstate, d_term_db.get(), d_model.get()));
+  d_eq_query.reset(
+      new quantifiers::EqualityQueryQuantifiersEngine(qstate, d_model.get()));
   d_util.insert(d_util.begin(), d_eq_query.get());
 }
 
@@ -163,11 +152,15 @@ quantifiers::FirstOrderModel* QuantifiersEngine::getModel() const
 }
 quantifiers::TermDb* QuantifiersEngine::getTermDatabase() const
 {
-  return d_term_db.get();
+  return d_treg.getTermDatabase();
 }
 quantifiers::TermDbSygus* QuantifiersEngine::getTermDatabaseSygus() const
 {
-  return d_sygus_tdb.get();
+  return d_treg.getTermDatabaseSygus();
+}
+quantifiers::TermEnumeration* QuantifiersEngine::getTermEnumeration() const
+{
+  return d_treg.getTermEnumeration();
 }
 quantifiers::Instantiate* QuantifiersEngine::getInstantiate() const
 {
@@ -177,10 +170,6 @@ 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();
@@ -198,7 +187,7 @@ bool QuantifiersEngine::isFiniteBound(Node q, Node v) const
   {
     return true;
   }
-  else if (d_term_enum->mayComplete(tn))
+  else if (d_treg.getTermEnumeration()->mayComplete(tn))
   {
     return true;
   }
@@ -255,18 +244,9 @@ void QuantifiersEngine::presolve() {
   for( unsigned i=0; i<d_modules.size(); i++ ){
     d_modules[i]->presolve();
   }
-  d_term_db->presolve();
-  d_presolve = false;
-  //add all terms to database
-  if (options::incrementalSolving() && !options::termDbCd())
-  {
-    Trace("quant-engine-proc") << "Add presolve cache " << d_presolve_cache.size() << std::endl;
-    for (const Node& t : d_presolve_cache)
-    {
-      addTermToDatabase(t);
-    }
-    Trace("quant-engine-proc") << "Done add presolve cache " << std::endl;
-  }
+  // presolve with term registry, which populates the term database based on
+  // terms registered before presolve when in incremental mode
+  d_treg.presolve();
 }
 
 void QuantifiersEngine::ppNotifyAssertions(
@@ -742,37 +722,11 @@ void QuantifiersEngine::assertQuantifier( Node f, bool pol ){
   {
     mdl->assertNode(f);
   }
-  addTermToDatabase(d_qreg.getInstConstantBody(f), true);
+  // add term to the registry
+  d_treg.addTerm(d_qreg.getInstConstantBody(f), true);
 }
 
-void QuantifiersEngine::addTermToDatabase(Node n, bool withinQuant)
-{
-  // don't add terms in quantifier bodies
-  if (withinQuant && !options::registerQuantBodyTerms())
-  {
-    return;
-  }
-  if (options::incrementalSolving() && !options::termDbCd())
-  {
-    if( d_presolve_in.find( n )==d_presolve_in.end() ){
-      d_presolve_in.insert( n );
-      d_presolve_cache.push_back( n );
-    }
-  }
-  //only wait if we are doing incremental solving
-  if (!d_presolve || !options::incrementalSolving() || options::termDbCd())
-  {
-    d_term_db->addTerm(n);
-    if (d_sygus_tdb && options::sygusEvalUnfold())
-    {
-      d_sygus_tdb->getEvalUnfold()->registerEvalTerm(n);
-    }
-  }
-}
-
-void QuantifiersEngine::eqNotifyNewClass(TNode t) {
-  addTermToDatabase( t );
-}
+void QuantifiersEngine::eqNotifyNewClass(TNode t) { d_treg.addTerm(t); }
 
 void QuantifiersEngine::markRelevant( Node q ) {
   d_model->markRelevant( q );
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index d08e32f6e..23f3d1203 100644
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -25,6 +25,7 @@
 #include "context/cdlist.h"
 #include "theory/quantifiers/quant_util.h"
 #include "theory/quantifiers/quantifiers_registry.h"
+#include "theory/quantifiers/term_registry.h"
 #include "util/statistics_registry.h"
 
 namespace CVC4 {
@@ -86,12 +87,12 @@ class QuantifiersEngine {
   quantifiers::TermDb* getTermDatabase() const;
   /** get term database sygus */
   quantifiers::TermDbSygus* getTermDatabaseSygus() const;
+  /** get term enumeration utility */
+  quantifiers::TermEnumeration* getTermEnumeration() 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
@@ -170,13 +171,11 @@ private:
  bool reduceQuantifier(Node q);
 
 public:
+ /** notification when master equality engine is updated */
+ void eqNotifyNewClass(TNode t);
  /** mark relevant quantified formula, this will indicate it should be checked
   * before the others */
  void markRelevant(Node q);
- /** add term to database */
- void addTermToDatabase(Node n, bool withinQuant = false);
- /** notification when master equality engine is updated */
- void eqNotifyNewClass(TNode t);
  /** get internal representative
   *
   * Choose a term that is equivalent to a in the current context that is the
@@ -282,24 +281,20 @@ public:
   //------------- quantifiers utilities
   /** The quantifiers registry */
   quantifiers::QuantifiersRegistry d_qreg;
+  /** The term registry */
+  quantifiers::TermRegistry d_treg;
   /** 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;
   /** model builder */
   std::unique_ptr<quantifiers::QModelBuilder> d_builder;
-  /** term database */
-  std::unique_ptr<quantifiers::TermDb> d_term_db;
   /** equality query class */
   std::unique_ptr<quantifiers::EqualityQueryQuantifiersEngine> d_eq_query;
-  /** sygus term database */
-  std::unique_ptr<quantifiers::TermDbSygus> d_sygus_tdb;
   /** 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
   /**
    * The modules utility, which contains all of the quantifiers modules.
@@ -314,11 +309,6 @@ public:
   /** quantifiers reduced */
   BoolMap d_quants_red;
   std::map<Node, Node> d_quants_red_lem;
-  /** has presolve been called */
-  context::CDO<bool> d_presolve;
-  /** presolve cache */
-  NodeSet d_presolve_in;
-  NodeList d_presolve_cache;
 };/* class QuantifiersEngine */
 
 }/* CVC4::theory namespace */