Add instantiation pool feature to the API (#6358)

This adds the command declare-pool to the public API. It also adds parsing support for this feature, lifts the internal kinds to public kinds, adds an example regression, and a unit test for the new declare-pool solver method.

5 files changed, 74 insertions, 0 deletions

diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp
index a32ff4caa..aafc5331a 100644
--- a/src/api/cpp/cvc5.cpp
+++ b/src/api/cpp/cvc5.cpp
@@ -350,6 +350,9 @@ const static std::unordered_map<Kind, cvc5::Kind, KindHashFunction> s_kinds{
     {BOUND_VAR_LIST, cvc5::Kind::BOUND_VAR_LIST},
     {INST_PATTERN, cvc5::Kind::INST_PATTERN},
     {INST_NO_PATTERN, cvc5::Kind::INST_NO_PATTERN},
+    {INST_POOL, cvc5::Kind::INST_POOL},
+    {INST_ADD_TO_POOL, cvc5::Kind::INST_ADD_TO_POOL},
+    {SKOLEM_ADD_TO_POOL, cvc5::Kind::SKOLEM_ADD_TO_POOL},
     {INST_ATTRIBUTE, cvc5::Kind::INST_ATTRIBUTE},
     {INST_PATTERN_LIST, cvc5::Kind::INST_PATTERN_LIST},
     {LAST_KIND, cvc5::Kind::LAST_KIND},
@@ -644,6 +647,9 @@ const static std::unordered_map<cvc5::Kind, Kind, cvc5::kind::KindHashFunction>
         {cvc5::Kind::BOUND_VAR_LIST, BOUND_VAR_LIST},
         {cvc5::Kind::INST_PATTERN, INST_PATTERN},
         {cvc5::Kind::INST_NO_PATTERN, INST_NO_PATTERN},
+        {cvc5::Kind::INST_POOL, INST_POOL},
+        {cvc5::Kind::INST_ADD_TO_POOL, INST_ADD_TO_POOL},
+        {cvc5::Kind::SKOLEM_ADD_TO_POOL, SKOLEM_ADD_TO_POOL},
         {cvc5::Kind::INST_ATTRIBUTE, INST_ATTRIBUTE},
         {cvc5::Kind::INST_PATTERN_LIST, INST_PATTERN_LIST},
         /* ----------------------------------------------------------------- */
@@ -6596,6 +6602,24 @@ Term Solver::getSeparationNilTerm() const
   CVC5_API_TRY_CATCH_END;
 }
 
+Term Solver::declarePool(const std::string& symbol,
+                         const Sort& sort,
+                         const std::vector<Term>& initValue) const
+{
+  NodeManagerScope scope(getNodeManager());
+  CVC5_API_TRY_CATCH_BEGIN;
+  CVC5_API_SOLVER_CHECK_SORT(sort);
+  CVC5_API_SOLVER_CHECK_TERMS(initValue);
+  //////// all checks before this line
+  TypeNode setType = getNodeManager()->mkSetType(*sort.d_type);
+  Node pool = getNodeManager()->mkBoundVar(symbol, setType);
+  std::vector<Node> initv = Term::termVectorToNodes(initValue);
+  d_smtEngine->declarePool(pool, initv);
+  return Term(this, pool);
+  ////////
+  CVC5_API_TRY_CATCH_END;
+}
+
 void Solver::pop(uint32_t nscopes) const
 {
   NodeManagerScope scope(getNodeManager());
diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h
index dc834d8b5..aaf19c30b 100644
--- a/src/api/cpp/cvc5.h
+++ b/src/api/cpp/cvc5.h
@@ -3567,6 +3567,19 @@ class CVC4_EXPORT Solver
   Term getSeparationNilTerm() const;
 
   /**
+   * Declare a symbolic pool of terms with the given initial value.
+   * SMT-LIB:
+   * \verbatim
+   * ( declare-pool <symbol> <sort> ( <term>* ) )
+   * \endverbatim
+   * @param symbol The name of the pool
+   * @param sort The sort of the elements of the pool.
+   * @param initValue The initial value of the pool
+   */
+  Term declarePool(const std::string& symbol,
+                   const Sort& sort,
+                   const std::vector<Term>& initValue) const;
+  /**
    * Pop (a) level(s) from the assertion stack.
    * SMT-LIB:
    * \verbatim
diff --git a/src/api/cpp/cvc5_kind.h b/src/api/cpp/cvc5_kind.h
index 6cb4be3c8..86e6d676d 100644
--- a/src/api/cpp/cvc5_kind.h
+++ b/src/api/cpp/cvc5_kind.h
@@ -3331,6 +3331,34 @@ enum CVC4_EXPORT Kind : int32_t
    *   - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
    */
   INST_NO_PATTERN,
+  /*
+   * An instantiation pool.
+   * Specifies an annotation for pool based instantiation.
+   * Parameters: n > 1
+   *   - 1..n: Terms that comprise the pools, which are one-to-one with
+   * the variables of the quantified formula to be instantiated.
+   * Create with:
+   *   - `mkTerm(Kind kind, Term child1, Term child2)
+   *   - `mkTerm(Kind kind, Term child1, Term child2, Term child3)
+   *   - `mkTerm(Kind kind, const std::vector<Term>& children)
+   */
+  INST_POOL,
+  /*
+   * A instantantiation-add-to-pool annotation.
+   * Parameters: n = 1
+   *   - 1: The pool to add to.
+   * Create with:
+   *   - `mkTerm(Kind kind, Term child)
+   */
+  INST_ADD_TO_POOL,
+  /*
+   * A skolemization-add-to-pool annotation.
+   * Parameters: n = 1
+   *   - 1: The pool to add to.
+   * Create with:
+   *   - `mkTerm(Kind kind, Term child)
+   */
+  SKOLEM_ADD_TO_POOL,
   /**
    * An instantiation attribute
    * Specifies a custom property for a quantified formula given by a
diff --git a/src/api/python/cvc4.pxd b/src/api/python/cvc4.pxd
index abc23ea4b..336def3dc 100644
--- a/src/api/python/cvc4.pxd
+++ b/src/api/python/cvc4.pxd
@@ -240,6 +240,7 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5::api":
         void declareSeparationHeap(Sort locSort, Sort dataSort) except +
         Term getSeparationHeap() except +
         Term getSeparationNilTerm() except +
+        Term declarePool(const string& name, Sort sort, vector[Term]& initValue) except +
         void pop(uint32_t nscopes) except +
         void push(uint32_t nscopes) except +
         void reset() except +
diff --git a/src/api/python/cvc4.pxi b/src/api/python/cvc4.pxi
index 3156b0882..48921dc87 100644
--- a/src/api/python/cvc4.pxi
+++ b/src/api/python/cvc4.pxi
@@ -1136,6 +1136,14 @@ cdef class Solver:
         term.cterm = self.csolver.getSeparationNilTerm()
         return term
 
+    def declarePool(self, str symbol, Sort sort, initValue):
+        cdef Term term = Term(self)
+        cdef vector[c_Term] niv
+        for v in initValue:
+            niv.push_back((<Term?> v).cterm)
+        term.cterm = self.csolver.declarePool(symbol.encode(), sort.csort, niv)
+        return term
+
     def pop(self, nscopes=1):
         self.csolver.pop(nscopes)