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.

1 files changed, 28 insertions, 0 deletions

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