Add term pools utility (#6243)

This utility will be used to track pools for pool-based instantiation.

5 files changed, 301 insertions, 0 deletions

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 04ad27b5c..2bcda537c 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -786,6 +786,8 @@ libcvc4_add_sources(
   theory/quantifiers/skolemize.h
   theory/quantifiers/solution_filter.cpp
   theory/quantifiers/solution_filter.h
+  theory/quantifiers/term_pools.cpp
+  theory/quantifiers/term_pools.h
   theory/quantifiers/term_tuple_enumerator.cpp
   theory/quantifiers/term_tuple_enumerator.h
   theory/quantifiers/sygus/ce_guided_single_inv.cpp
diff --git a/src/theory/quantifiers/term_pools.cpp b/src/theory/quantifiers/term_pools.cpp
new file mode 100644
index 000000000..e90fd69b3
--- /dev/null
+++ b/src/theory/quantifiers/term_pools.cpp
@@ -0,0 +1,158 @@
+/*********************                                                        */
+/*! \file term_pools.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2021 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 utilities for term enumeration
+ **/
+
+#include "theory/quantifiers/term_pools.h"
+
+#include "theory/quantifiers/quantifiers_state.h"
+
+namespace cvc5 {
+namespace theory {
+namespace quantifiers {
+
+void TermPoolDomain::initialize() { d_terms.clear(); }
+void TermPoolDomain::add(Node n)
+{
+  if (std::find(d_terms.begin(), d_terms.end(), n) == d_terms.end())
+  {
+    d_terms.push_back(n);
+  }
+}
+
+void TermPoolQuantInfo::initialize()
+{
+  d_instAddToPool.clear();
+  d_skolemAddToPool.clear();
+}
+
+TermPools::TermPools(QuantifiersState& qs) : d_qs(qs) {}
+
+bool TermPools::reset(Theory::Effort e)
+{
+  for (std::pair<const Node, TermPoolDomain>& p : d_pools)
+  {
+    p.second.d_currTerms.clear();
+  }
+  return true;
+}
+
+void TermPools::registerQuantifier(Node q)
+{
+  if (q.getNumChildren() < 3)
+  {
+    return;
+  }
+  TermPoolQuantInfo& qi = d_qinfo[q];
+  qi.initialize();
+  for (const Node& p : q[2])
+  {
+    Kind pk = p.getKind();
+    if (pk == kind::INST_ADD_TO_POOL)
+    {
+      qi.d_instAddToPool.push_back(p);
+    }
+    else if (pk == kind::SKOLEM_ADD_TO_POOL)
+    {
+      qi.d_skolemAddToPool.push_back(p);
+    }
+  }
+  if (qi.d_instAddToPool.empty() && qi.d_skolemAddToPool.empty())
+  {
+    d_qinfo.erase(q);
+  }
+}
+
+std::string TermPools::identify() const { return "TermPools"; }
+
+void TermPools::registerPool(Node p, const std::vector<Node>& initValue)
+{
+  TermPoolDomain& d = d_pools[p];
+  d.initialize();
+  for (const Node& i : initValue)
+  {
+    d.add(i);
+  }
+}
+
+void TermPools::getTermsForPool(Node p, std::vector<Node>& terms)
+{
+  // for now, we assume p is a variable
+  Assert(p.isVar());
+  TermPoolDomain& dom = d_pools[p];
+  if (dom.d_terms.empty())
+  {
+    return;
+  }
+  // if we have yet to compute terms on this round
+  if (dom.d_currTerms.empty())
+  {
+    std::unordered_set<Node, NodeHashFunction> reps;
+    // eliminate modulo equality
+    for (const Node& t : dom.d_terms)
+    {
+      Node r = d_qs.getRepresentative(t);
+      if (reps.find(r) == reps.end())
+      {
+        reps.insert(r);
+        dom.d_currTerms.push_back(t);
+      }
+    }
+    Trace("pool-terms") << "* Domain for pool " << p << " is "
+                        << dom.d_currTerms << std::endl;
+  }
+  terms.insert(terms.end(), dom.d_currTerms.begin(), dom.d_currTerms.end());
+}
+
+void TermPools::processInstantiation(Node q, const std::vector<Node>& terms)
+{
+  processInternal(q, terms, true);
+}
+
+void TermPools::processSkolemization(Node q, const std::vector<Node>& skolems)
+{
+  processInternal(q, skolems, false);
+}
+
+void TermPools::processInternal(Node q,
+                                const std::vector<Node>& ts,
+                                bool isInst)
+{
+  Assert(q.getKind() == kind::FORALL);
+  std::map<Node, TermPoolQuantInfo>::iterator it = d_qinfo.find(q);
+  if (it == d_qinfo.end())
+  {
+    // does not impact
+    return;
+  }
+  std::vector<Node> vars(q[0].begin(), q[0].end());
+  Assert(vars.size() == ts.size());
+  std::vector<Node>& cmds =
+      isInst ? it->second.d_instAddToPool : it->second.d_skolemAddToPool;
+  for (const Node& c : cmds)
+  {
+    Assert(c.getNumChildren() == 2);
+    Node t = c[0];
+    // substitute the term
+    Node st = t.substitute(vars.begin(), vars.end(), ts.begin(), ts.end());
+    // add to pool
+    Trace("pool-terms") << "Due to "
+                        << (isInst ? "instantiation" : "skolemization")
+                        << ", add " << st << " to pool " << c[1] << std::endl;
+    TermPoolDomain& dom = d_pools[c[1]];
+    dom.d_terms.push_back(st);
+  }
+}
+
+}  // namespace quantifiers
+}  // namespace theory
+}  // namespace CVC4
diff --git a/src/theory/quantifiers/term_pools.h b/src/theory/quantifiers/term_pools.h
new file mode 100644
index 000000000..117cffc42
--- /dev/null
+++ b/src/theory/quantifiers/term_pools.h
@@ -0,0 +1,107 @@
+/*********************                                                        */
+/*! \file term_pools.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2021 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 utilities for term enumeration
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__THEORY__QUANTIFIERS__TERM_POOLS_H
+#define CVC4__THEORY__QUANTIFIERS__TERM_POOLS_H
+
+#include <unordered_set>
+#include <vector>
+
+#include "expr/node.h"
+#include "theory/quantifiers/quant_util.h"
+
+namespace cvc5 {
+namespace theory {
+namespace quantifiers {
+
+class QuantifiersState;
+
+/**
+ * Information concerning a pool variable.
+ */
+class TermPoolDomain
+{
+ public:
+  /** initialize, which clears the data below */
+  void initialize();
+  /** add node to this pool */
+  void add(Node n);
+  /** The list in this pool */
+  std::vector<Node> d_terms;
+  /**
+   * The list of terms on this round. This is cleared at the beginning of an
+   * instantiation round. The members are unique modulo equality.
+   */
+  std::vector<Node> d_currTerms;
+};
+
+/**
+ * Contains all annotations that pertain to pools for a given quantified
+ * formula.
+ */
+class TermPoolQuantInfo
+{
+ public:
+  /** initialize, which clears the data below */
+  void initialize();
+  /** Annotations of kind INST_ADD_TO_POOL */
+  std::vector<Node> d_instAddToPool;
+  /** Annotations of kind SKOLEM_ADD_TO_POOL */
+  std::vector<Node> d_skolemAddToPool;
+};
+
+/**
+ * Term pools, which tracks the values of "pools", which are used for
+ * pool-based instantiation.
+ */
+class TermPools : public QuantifiersUtil
+{
+ public:
+  TermPools(QuantifiersState& qs);
+  ~TermPools() {}
+  /** reset, which resets the current values of pools */
+  bool reset(Theory::Effort e) override;
+  /** Called for new quantifiers, which computes TermPoolQuantInfo above */
+  void registerQuantifier(Node q) override;
+  /** Identify this module (for debugging, dynamic configuration, etc..) */
+  std::string identify() const override;
+  /** Register pool p with initial value initValue. */
+  void registerPool(Node p, const std::vector<Node>& initValue);
+  /** Get terms for pool p, adds them to the vector terms. */
+  void getTermsForPool(Node p, std::vector<Node>& terms);
+  /**
+   * Process instantiation, called at the moment we successfully instantiate
+   * q with terms. This adds terms to pools based on INST_ADD_TO_POOL
+   * annotations.
+   */
+  void processInstantiation(Node q, const std::vector<Node>& terms);
+  /** Same as above, for SKOLEM_ADD_TO_POOL. */
+  void processSkolemization(Node q, const std::vector<Node>& skolems);
+ private:
+  void processInternal(Node q, const std::vector<Node>& ts, bool isInst);
+  /** reference to the quantifiers state */
+  QuantifiersState& d_qs;
+  /** Maps pools to a domain */
+  std::map<Node, TermPoolDomain> d_pools;
+  /** Maps quantifiers to info */
+  std::map<Node, TermPoolQuantInfo> d_qinfo;
+};
+
+}  // namespace quantifiers
+}  // namespace theory
+}  // namespace CVC5
+
+#endif /* CVC4__THEORY__QUANTIFIERS__TERM_POOLS_H */
diff --git a/src/theory/quantifiers/term_registry.cpp b/src/theory/quantifiers/term_registry.cpp
index 8317271f9..96bde733a 100644
--- a/src/theory/quantifiers/term_registry.cpp
+++ b/src/theory/quantifiers/term_registry.cpp
@@ -18,7 +18,9 @@
 #include "options/smt_options.h"
 #include "theory/quantifiers/first_order_model.h"
 #include "theory/quantifiers/fmf/first_order_model_fmc.h"
+#include "theory/quantifiers/quantifiers_attributes.h"
 #include "theory/quantifiers/quantifiers_state.h"
+#include "theory/quantifiers/term_util.h"
 
 namespace cvc5 {
 namespace theory {
@@ -29,6 +31,7 @@ TermRegistry::TermRegistry(QuantifiersState& qs, QuantifiersRegistry& qr)
       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)
 {
@@ -116,6 +119,21 @@ Node TermRegistry::getTermForType(TypeNode tn)
   return d_termDb->getOrMakeTypeGroundTerm(tn);
 }
 
+void TermRegistry::declarePool(Node p, const std::vector<Node>& initValue)
+{
+  d_termPools->registerPool(p, initValue);
+}
+
+void TermRegistry::processInstantiation(Node q, const std::vector<Node>& terms)
+{
+  d_termPools->processInstantiation(q, terms);
+}
+void TermRegistry::processSkolemization(Node q,
+                                        const std::vector<Node>& skolems)
+{
+  d_termPools->processSkolemization(q, skolems);
+}
+
 TermDb* TermRegistry::getTermDatabase() const { return d_termDb.get(); }
 
 TermDbSygus* TermRegistry::getTermDatabaseSygus() const
@@ -128,6 +146,8 @@ TermEnumeration* TermRegistry::getTermEnumeration() const
   return d_termEnum.get();
 }
 
+TermPools* TermRegistry::getTermPools() const { return d_termPools.get(); }
+
 FirstOrderModel* TermRegistry::getModel() const { return d_qmodel.get(); }
 
 bool TermRegistry::useFmcModel() const { return d_useFmcModel; }
diff --git a/src/theory/quantifiers/term_registry.h b/src/theory/quantifiers/term_registry.h
index 79070fae8..e6b577f4e 100644
--- a/src/theory/quantifiers/term_registry.h
+++ b/src/theory/quantifiers/term_registry.h
@@ -24,6 +24,7 @@
 #include "theory/quantifiers/sygus/term_database_sygus.h"
 #include "theory/quantifiers/term_database.h"
 #include "theory/quantifiers/term_enumeration.h"
+#include "theory/quantifiers/term_pools.h"
 
 namespace cvc5 {
 namespace theory {
@@ -67,6 +68,15 @@ class TermRegistry
    * one exists, or otherwise a fresh variable.
    */
   Node getTermForType(TypeNode tn);
+  /**
+   * Declare pool p with initial value initValue.
+   */
+  void declarePool(Node p, const std::vector<Node>& initValue);
+  /**
+   * Process instantiation
+   */
+  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;
@@ -77,6 +87,8 @@ class TermRegistry
   TermDbSygus* getTermDatabaseSygus() const;
   /** get term enumeration utility */
   TermEnumeration* getTermEnumeration() const;
+  /** get the term pools utility */
+  TermPools* getTermPools() const;
   /** get the model utility */
   FirstOrderModel* getModel() const;
 
@@ -89,6 +101,8 @@ class TermRegistry
   NodeSet d_presolveCache;
   /** term enumeration utility */
   std::unique_ptr<TermEnumeration> d_termEnum;
+  /** term enumeration utility */
+  std::unique_ptr<TermPools> d_termPools;
   /** term database */
   std::unique_ptr<TermDb> d_termDb;
   /** sygus term database */