Introduce quantifiers term registry (#5983)

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

6 files changed, 177 insertions, 20 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 */