Add pool instantiation strategy (#6308)

Adds an instantiation strategy based on user-provided pool annotations.

The next PR will connect this to quantifiers engine.

11 files changed, 320 insertions, 2 deletions

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index c33110cc3..ee59d5d31 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -745,6 +745,8 @@ libcvc4_add_sources(
   theory/quantifiers/inst_match_trie.h
   theory/quantifiers/inst_strategy_enumerative.cpp
   theory/quantifiers/inst_strategy_enumerative.h
+  theory/quantifiers/inst_strategy_pool.cpp
+  theory/quantifiers/inst_strategy_pool.h
   theory/quantifiers/instantiate.cpp
   theory/quantifiers/instantiate.h
   theory/quantifiers/instantiation_list.cpp
diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml
index db7100e9c..bbdf030a1 100644
--- a/src/options/quantifiers_options.toml
+++ b/src/options/quantifiers_options.toml
@@ -586,6 +586,14 @@ header = "options/quantifiers_options.h"
   name = "agg"
   help = "Consider the phase requirements aggressively for all triggers."
 
+[[option]]
+  name       = "poolInst"
+  category   = "regular"
+  long       = "pool-inst"
+  type       = "bool"
+  default    = "true"
+  help       = "pool-based instantiation: instantiate with ground terms occurring in user-specified pools"
+
 ### Finite model finding options
 
 [[option]]
diff --git a/src/theory/inference_id.cpp b/src/theory/inference_id.cpp
index c1c751800..ceca32a8d 100644
--- a/src/theory/inference_id.cpp
+++ b/src/theory/inference_id.cpp
@@ -174,6 +174,7 @@ const char* toString(InferenceId i)
     case InferenceId::QUANTIFIERS_INST_CEGQI: return "QUANTIFIERS_INST_CEGQI";
     case InferenceId::QUANTIFIERS_INST_SYQI: return "QUANTIFIERS_INST_SYQI";
     case InferenceId::QUANTIFIERS_INST_ENUM: return "QUANTIFIERS_INST_ENUM";
+    case InferenceId::QUANTIFIERS_INST_POOL: return "QUANTIFIERS_INST_POOL";
     case InferenceId::QUANTIFIERS_BINT_PROXY: return "QUANTIFIERS_BINT_PROXY";
     case InferenceId::QUANTIFIERS_BINT_MIN_NG: return "QUANTIFIERS_BINT_MIN_NG";
     case InferenceId::QUANTIFIERS_CEGQI_CEX: return "QUANTIFIERS_CEGQI_CEX";
diff --git a/src/theory/inference_id.h b/src/theory/inference_id.h
index 985d90738..7730a7d14 100644
--- a/src/theory/inference_id.h
+++ b/src/theory/inference_id.h
@@ -265,6 +265,8 @@ enum class InferenceId
   QUANTIFIERS_INST_SYQI,
   // instantiations from enumerative instantiation
   QUANTIFIERS_INST_ENUM,
+  // instantiations from pool instantiation
+  QUANTIFIERS_INST_POOL,
   //-------------------- bounded integers
   // a proxy lemma from bounded integers, used to control bounds on ground terms
   QUANTIFIERS_BINT_PROXY,
diff --git a/src/theory/quantifiers/inst_strategy_pool.cpp b/src/theory/quantifiers/inst_strategy_pool.cpp
new file mode 100644
index 000000000..0e32c246e
--- /dev/null
+++ b/src/theory/quantifiers/inst_strategy_pool.cpp
@@ -0,0 +1,168 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Andrew Reynolds
+ *
+ * This file is part of the cvc5 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.
+ * ****************************************************************************
+ *
+ * Pool-based instantiation strategy
+ */
+
+#include "theory/quantifiers/inst_strategy_pool.h"
+
+#include "options/quantifiers_options.h"
+#include "theory/quantifiers/first_order_model.h"
+#include "theory/quantifiers/instantiate.h"
+#include "theory/quantifiers/quantifiers_inference_manager.h"
+#include "theory/quantifiers/term_pools.h"
+#include "theory/quantifiers/term_registry.h"
+#include "theory/quantifiers/term_tuple_enumerator.h"
+
+using namespace cvc5::kind;
+using namespace cvc5::context;
+
+namespace cvc5 {
+namespace theory {
+namespace quantifiers {
+
+InstStrategyPool::InstStrategyPool(QuantifiersState& qs,
+                                   QuantifiersInferenceManager& qim,
+                                   QuantifiersRegistry& qr,
+                                   TermRegistry& tr)
+    : QuantifiersModule(qs, qim, qr, tr)
+{
+}
+
+void InstStrategyPool::presolve() {}
+
+bool InstStrategyPool::needsCheck(Theory::Effort e)
+{
+  return d_qstate.getInstWhenNeedsCheck(e);
+}
+
+void InstStrategyPool::reset_round(Theory::Effort e) {}
+
+void InstStrategyPool::registerQuantifier(Node q)
+{
+  // take into account user pools
+  if (q.getNumChildren() == 3)
+  {
+    Node subsPat = d_qreg.substituteBoundVariablesToInstConstants(q[2], q);
+    // add patterns
+    for (const Node& p : subsPat)
+    {
+      if (p.getKind() == INST_POOL)
+      {
+        d_userPools[q].push_back(p);
+      }
+    }
+  }
+}
+
+void InstStrategyPool::check(Theory::Effort e, QEffort quant_e)
+{
+  if (d_userPools.empty())
+  {
+    return;
+  }
+  double clSet = 0;
+  if (Trace.isOn("pool-engine"))
+  {
+    clSet = double(clock()) / double(CLOCKS_PER_SEC);
+    Trace("pool-engine") << "---Pool instantiation, effort = " << e << "---"
+                         << std::endl;
+  }
+  FirstOrderModel* fm = d_treg.getModel();
+  bool inConflict = false;
+  uint64_t addedLemmas = 0;
+  size_t nquant = fm->getNumAssertedQuantifiers();
+  std::map<Node, std::vector<Node> >::iterator uit;
+  for (size_t i = 0; i < nquant; i++)
+  {
+    Node q = fm->getAssertedQuantifier(i, true);
+    uit = d_userPools.find(q);
+    if (uit == d_userPools.end())
+    {
+      // no user pools for this
+      continue;
+    }
+    if (!d_qreg.hasOwnership(q, this) || !fm->isQuantifierActive(q))
+    {
+      // quantified formula is not owned by this or is inactive
+      continue;
+    }
+    // process with each user pool
+    for (const Node& p : uit->second)
+    {
+      inConflict = process(q, p, addedLemmas);
+      if (inConflict)
+      {
+        break;
+      }
+    }
+    if (inConflict)
+    {
+      break;
+    }
+  }
+  if (Trace.isOn("pool-engine"))
+  {
+    Trace("pool-engine") << "Added lemmas = " << addedLemmas << std::endl;
+    double clSet2 = double(clock()) / double(CLOCKS_PER_SEC);
+    Trace("pool-engine") << "Finished pool instantiation, time = "
+                         << (clSet2 - clSet) << std::endl;
+  }
+}
+
+std::string InstStrategyPool::identify() const
+{
+  return std::string("InstStrategyPool");
+}
+
+bool InstStrategyPool::process(Node q, Node p, uint64_t& addedLemmas)
+{
+  TermTupleEnumeratorEnv ttec;
+  ttec.d_fullEffort = true;
+  ttec.d_increaseSum = options::fullSaturateSum();
+  TermPools* tp = d_treg.getTermPools();
+  std::shared_ptr<TermTupleEnumeratorInterface> enumerator(
+      mkTermTupleEnumeratorPool(q, &ttec, tp, p));
+  Instantiate* ie = d_qim.getInstantiate();
+  std::vector<Node> terms;
+  std::vector<bool> failMask;
+  // we instantiate exhaustively
+  enumerator->init();
+  while (enumerator->hasNext())
+  {
+    if (d_qstate.isInConflict())
+    {
+      // could be conflicting for an internal reason
+      return true;
+    }
+    enumerator->next(terms);
+    // try instantiation
+    failMask.clear();
+    if (ie->addInstantiationExpFail(
+            q, terms, failMask, InferenceId::QUANTIFIERS_INST_POOL))
+    {
+      Trace("pool-inst") << "Success with " << terms << std::endl;
+      addedLemmas++;
+    }
+    else
+    {
+      Trace("pool-inst") << "Fail with " << terms << std::endl;
+      // notify the enumerator of the failure
+      enumerator->failureReason(failMask);
+    }
+  }
+  return false;
+}
+
+}  // namespace quantifiers
+}  // namespace theory
+}  // namespace cvc5
diff --git a/src/theory/quantifiers/inst_strategy_pool.h b/src/theory/quantifiers/inst_strategy_pool.h
new file mode 100644
index 000000000..e45f08bc2
--- /dev/null
+++ b/src/theory/quantifiers/inst_strategy_pool.h
@@ -0,0 +1,73 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Andrew Reynolds
+ *
+ * This file is part of the cvc5 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.
+ * ****************************************************************************
+ *
+ * Pool-based instantiation strategy
+ */
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__THEORY__QUANTIFIERS__INST_STRATEGY_POOL_H
+#define CVC4__THEORY__QUANTIFIERS__INST_STRATEGY_POOL_H
+
+#include "theory/quantifiers/quant_module.h"
+
+namespace cvc5 {
+namespace theory {
+namespace quantifiers {
+
+/**
+ * Pool-based instantiation. This implements a strategy for instantiating
+ * quantifiers based on user-provided pool annotations.
+ *
+ * When check is invoked, this strategy considers each
+ * INST_POOL annotation on quantified formulas. For each annotation, it
+ * instantiates the associated quantified formula with the Cartesian
+ * product of terms currently in the pool, using efficient techniques for
+ * enumerating over tuples of terms, as implemented in the term tuple
+ * enumerator utilities (see quantifiers/term_tuple_enumerator.h).
+ */
+class InstStrategyPool : public QuantifiersModule
+{
+ public:
+  InstStrategyPool(QuantifiersState& qs,
+                   QuantifiersInferenceManager& qim,
+                   QuantifiersRegistry& qr,
+                   TermRegistry& tr);
+  ~InstStrategyPool() {}
+  /** Presolve */
+  void presolve() override;
+  /** Needs check. */
+  bool needsCheck(Theory::Effort e) override;
+  /** Reset round. */
+  void reset_round(Theory::Effort e) override;
+  /** Register quantified formula q */
+  void registerQuantifier(Node q) override;
+  /** Check.
+   * Adds instantiations for all currently asserted
+   * quantified formulas via calls to process(...)
+   */
+  void check(Theory::Effort e, QEffort quant_e) override;
+  /** Identify. */
+  std::string identify() const override;
+
+ private:
+  /** Process quantified formula with user pool */
+  bool process(Node q, Node p, uint64_t& addedLemmas);
+  /** Map from quantified formulas to user pools */
+  std::map<Node, std::vector<Node> > d_userPools;
+};
+
+}  // namespace quantifiers
+}  // namespace theory
+}  // namespace cvc5
+
+#endif
diff --git a/src/theory/quantifiers/quant_util.h b/src/theory/quantifiers/quant_util.h
index a70cc2c8e..85c891117 100644
--- a/src/theory/quantifiers/quant_util.h
+++ b/src/theory/quantifiers/quant_util.h
@@ -43,9 +43,9 @@ public:
    * Returns false if the reset failed. When reset fails, the utility should
    * have added a lemma via a call to d_qim.addPendingLemma.
    */
-  virtual bool reset( Theory::Effort e ) = 0;
+  virtual bool reset(Theory::Effort e) { return true; }
   /* Called for new quantifiers */
-  virtual void registerQuantifier(Node q) = 0;
+  virtual void registerQuantifier(Node q) {}
   /** Identify this module (for debugging, dynamic configuration, etc..) */
   virtual std::string identify() const = 0;
   /** Check complete?
diff --git a/src/theory/quantifiers/quantifiers_modules.cpp b/src/theory/quantifiers/quantifiers_modules.cpp
index a9871d643..704a65bfb 100644
--- a/src/theory/quantifiers/quantifiers_modules.cpp
+++ b/src/theory/quantifiers/quantifiers_modules.cpp
@@ -34,6 +34,7 @@ QuantifiersModules::QuantifiersModules()
       d_sg_gen(nullptr),
       d_synth_e(nullptr),
       d_fs(nullptr),
+      d_ipool(nullptr),
       d_i_cbqi(nullptr),
       d_qsplit(nullptr),
       d_sygus_inst(nullptr)
@@ -114,6 +115,11 @@ void QuantifiersModules::initialize(QuantifiersState& qs,
     d_fs.reset(new InstStrategyEnum(qs, qim, qr, tr, d_rel_dom.get()));
     modules.push_back(d_fs.get());
   }
+  if (options::poolInst())
+  {
+    d_ipool.reset(new InstStrategyPool(qs, qim, qr, tr));
+    modules.push_back(d_ipool.get());
+  }
   if (options::sygusInst())
   {
     d_sygus_inst.reset(new SygusInst(qs, qim, qr, tr));
diff --git a/src/theory/quantifiers/quantifiers_modules.h b/src/theory/quantifiers/quantifiers_modules.h
index d42c60c31..dabee00f9 100644
--- a/src/theory/quantifiers/quantifiers_modules.h
+++ b/src/theory/quantifiers/quantifiers_modules.h
@@ -26,6 +26,7 @@
 #include "theory/quantifiers/fmf/model_builder.h"
 #include "theory/quantifiers/fmf/model_engine.h"
 #include "theory/quantifiers/inst_strategy_enumerative.h"
+#include "theory/quantifiers/inst_strategy_pool.h"
 #include "theory/quantifiers/quant_conflict_find.h"
 #include "theory/quantifiers/quant_split.h"
 #include "theory/quantifiers/sygus/synth_engine.h"
@@ -85,6 +86,8 @@ class QuantifiersModules
   std::unique_ptr<SynthEngine> d_synth_e;
   /** full saturation */
   std::unique_ptr<InstStrategyEnum> d_fs;
+  /** pool-based instantiation */
+  std::unique_ptr<InstStrategyPool> d_ipool;
   /** counterexample-based quantifier instantiation */
   std::unique_ptr<InstStrategyCegqi> d_i_cbqi;
   /** quantifiers splitting */
diff --git a/src/theory/quantifiers/term_tuple_enumerator.cpp b/src/theory/quantifiers/term_tuple_enumerator.cpp
index 169d2afea..4b714419f 100644
--- a/src/theory/quantifiers/term_tuple_enumerator.cpp
+++ b/src/theory/quantifiers/term_tuple_enumerator.cpp
@@ -28,6 +28,7 @@
 #include "theory/quantifiers/index_trie.h"
 #include "theory/quantifiers/quant_module.h"
 #include "theory/quantifiers/relevant_domain.h"
+#include "theory/quantifiers/term_pools.h"
 #include "theory/quantifiers/term_registry.h"
 #include "theory/quantifiers/term_util.h"
 #include "util/statistics_registry.h"
@@ -491,6 +492,48 @@ Node TermTupleEnumeratorBasic::getTerm(size_t variableIx, size_t term_index)
   return d_termDbList[type_node][term_index];
 }
 
+/**
+ * Enumerate ground terms as they come from a user-provided term pool
+ */
+class TermTupleEnumeratorPool : public TermTupleEnumeratorBase
+{
+ public:
+  TermTupleEnumeratorPool(Node quantifier,
+                          const TermTupleEnumeratorEnv* env,
+                          TermPools* tp,
+                          Node pool)
+      : TermTupleEnumeratorBase(quantifier, env), d_tp(tp), d_pool(pool)
+  {
+    Assert(d_pool.getKind() == kind::INST_POOL);
+  }
+
+  virtual ~TermTupleEnumeratorPool() = default;
+
+ protected:
+  /** Pointer to the term pool utility */
+  TermPools* d_tp;
+  /** The pool annotation */
+  Node d_pool;
+  /**  a list of terms for each id */
+  std::map<size_t, std::vector<Node> > d_poolList;
+  /** gets the terms from the pool */
+  size_t prepareTerms(size_t variableIx) override
+  {
+    Assert(d_pool.getNumChildren() > variableIx);
+    // prepare terms from pool
+    d_poolList[variableIx].clear();
+    d_tp->getTermsForPool(d_pool[variableIx], d_poolList[variableIx]);
+    Trace("pool-inst") << "Instantiation Terms for child " << variableIx << ": "
+                       << d_poolList[variableIx] << std::endl;
+    return d_poolList[variableIx].size();
+  }
+  Node getTerm(size_t variableIx, size_t term_index) override
+  {
+    Assert(term_index < d_poolList[variableIx].size());
+    return d_poolList[variableIx][term_index];
+  }
+};
+
 TermTupleEnumeratorInterface* mkTermTupleEnumerator(
     Node q, const TermTupleEnumeratorEnv* env, QuantifiersState& qs, TermDb* td)
 {
@@ -504,6 +547,13 @@ TermTupleEnumeratorInterface* mkTermTupleEnumeratorRd(
       new TermTupleEnumeratorRD(q, env, rd));
 }
 
+TermTupleEnumeratorInterface* mkTermTupleEnumeratorPool(
+    Node q, const TermTupleEnumeratorEnv* env, TermPools* tp, Node pool)
+{
+  return static_cast<TermTupleEnumeratorInterface*>(
+      new TermTupleEnumeratorPool(q, env, tp, pool));
+}
+
 }  // namespace quantifiers
 }  // namespace theory
 }  // namespace cvc5
diff --git a/src/theory/quantifiers/term_tuple_enumerator.h b/src/theory/quantifiers/term_tuple_enumerator.h
index c7f71481e..3306ee430 100644
--- a/src/theory/quantifiers/term_tuple_enumerator.h
+++ b/src/theory/quantifiers/term_tuple_enumerator.h
@@ -24,6 +24,7 @@ namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
+class TermPools;
 class QuantifiersState;
 class TermDb;
 class RelevantDomain;
@@ -94,6 +95,10 @@ TermTupleEnumeratorInterface* mkTermTupleEnumerator(
 TermTupleEnumeratorInterface* mkTermTupleEnumeratorRd(
     Node q, const TermTupleEnumeratorEnv* env, RelevantDomain* rd);
 
+/** Make term pool enumerator */
+TermTupleEnumeratorInterface* mkTermTupleEnumeratorPool(
+    Node q, const TermTupleEnumeratorEnv* env, TermPools* tp, Node p);
+
 }  // namespace quantifiers
 }  // namespace theory
 }  // namespace cvc5