From cc8ce1bcdf8d6a4b508723063879e891a6cbd8c3 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 20 Apr 2021 16:40:12 -0500 Subject: 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. --- src/api/cpp/cvc5.cpp | 24 ++++++++++++++++++++++++ src/api/cpp/cvc5.h | 13 +++++++++++++ src/api/cpp/cvc5_kind.h | 28 ++++++++++++++++++++++++++++ src/api/python/cvc4.pxd | 1 + src/api/python/cvc4.pxi | 8 ++++++++ 5 files changed, 74 insertions(+) (limited to 'src/api') 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 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::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& 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 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 @@ -3566,6 +3566,19 @@ class CVC4_EXPORT Solver */ Term getSeparationNilTerm() const; + /** + * Declare a symbolic pool of terms with the given initial value. + * SMT-LIB: + * \verbatim + * ( declare-pool ( * ) ) + * \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& initValue) const; /** * Pop (a) level(s) from the assertion stack. * SMT-LIB: 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& 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& 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(( v).cterm) + term.cterm = self.csolver.declarePool(symbol.encode(), sort.csort, niv) + return term + def pop(self, nscopes=1): self.csolver.pop(nscopes) -- cgit v1.2.3