diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-04-20 16:40:12 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-04-20 21:40:12 +0000 |
commit | cc8ce1bcdf8d6a4b508723063879e891a6cbd8c3 (patch) | |
tree | fef63c0628404e673eca56947d19411198ba3ce2 /src/api | |
parent | 18ce14653647a93319cc53eec9bc310d3a4c6f57 (diff) |
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.
Diffstat (limited to 'src/api')
-rw-r--r-- | src/api/cpp/cvc5.cpp | 24 | ||||
-rw-r--r-- | src/api/cpp/cvc5.h | 13 | ||||
-rw-r--r-- | src/api/cpp/cvc5_kind.h | 28 | ||||
-rw-r--r-- | src/api/python/cvc4.pxd | 1 | ||||
-rw-r--r-- | src/api/python/cvc4.pxi | 8 |
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) |