diff options
| author | Andres Noetzli <andres.noetzli@gmail.com> | 2020-09-02 14:02:26 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-09-02 16:02:26 -0500 |
| commit | 0f9fb31069d51e003a39b0e93f506324dec2bdac (patch) | |
| tree | e59f8a6d5a6290ad7e4d83abc2c721c5efd6757f /src/api/cvc4cpp.h | |
| parent | f845c04a147021937f1b0a942ee2080df950cda3 (diff) | |
[Python API] Add missing methods to Datatype/Term (#4998)
Fixes #4942. The Python API was missing some methods related to
datatypes. Most importantly, it was missing mkDatatypeSorts, which
meant that datatypes with unresolved placeholders could not be resolved.
This commit adds missing methods and ports the corresponding tests of
datatype_api_black.h to Python. The commit also adds support for
__getitem__ in Term.
Diffstat (limited to 'src/api/cvc4cpp.h')
| -rw-r--r-- | src/api/cvc4cpp.h | 9 |
1 files changed, 5 insertions, 4 deletions
diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h index d92660920..acf34abf9 100644 --- a/src/api/cvc4cpp.h +++ b/src/api/cvc4cpp.h @@ -2254,8 +2254,9 @@ class CVC4_PUBLIC Solver * @param unresolvedSorts the list of unresolved sorts * @return the datatype sorts */ - std::vector<Sort> mkDatatypeSorts(std::vector<DatatypeDecl>& dtypedecls, - std::set<Sort>& unresolvedSorts) const; + std::vector<Sort> mkDatatypeSorts( + const std::vector<DatatypeDecl>& dtypedecls, + const std::set<Sort>& unresolvedSorts) const; /** * Create function sort. @@ -3353,8 +3354,8 @@ class CVC4_PUBLIC Solver * @return the datatype sorts */ std::vector<Sort> mkDatatypeSortsInternal( - std::vector<DatatypeDecl>& dtypedecls, - std::set<Sort>& unresolvedSorts) const; + const std::vector<DatatypeDecl>& dtypedecls, + const std::set<Sort>& unresolvedSorts) const; /** * Synthesize n-ary function following specified syntactic constraints. |