diff options
| author | Haniel Barbosa <hanielbbarbosa@gmail.com> | 2021-01-26 13:10:33 -0300 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-01-26 13:10:33 -0300 |
| commit | 022dbeb9e2dc925cf0dcffb75ea57aedf09395de (patch) | |
| tree | 433ee1b826bafad9c311e22288e18e28d868e9c8 /src/api/cvc4cpp.h | |
| parent | 909a0aa67266d7659decf56f2e6eb8101a802d45 (diff) | |
Reestablishing support for define-sort (#5810)
Presumable broken since 3ed42d7ab. This extends the API to have a substitute method for Sort that in needed for doing the Sort substitution in the case of define-sort.
This fixes issue #5809.
Diffstat (limited to 'src/api/cvc4cpp.h')
| -rw-r--r-- | src/api/cvc4cpp.h | 15 |
1 files changed, 15 insertions, 0 deletions
diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h index 98752c697..66ba4f23b 100644 --- a/src/api/cvc4cpp.h +++ b/src/api/cvc4cpp.h @@ -477,6 +477,21 @@ class CVC4_PUBLIC Sort Sort instantiate(const std::vector<Sort>& params) const; /** + * Substitution of Sorts. + * @param sort the subsort to be substituted within this sort. + * @param replacement the sort replacing the substituted subsort. + */ + Sort substitute(const Sort& sort, const Sort& replacement) const; + + /** + * Simultaneous substitution of Sorts. + * @param sorts the subsorts to be substituted within this sort. + * @param replacements the sort replacing the substituted subsorts. + */ + Sort substitute(const std::vector<Sort>& sorts, + const std::vector<Sort>& replacements) const; + + /** * Output a string representation of this sort to a given stream. * @param out the output stream */ |