projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 909a0aa) | patch
Reestablishing support for define-sort (#5810)
authorHaniel Barbosa <hanielbbarbosa@gmail.com>
Tue, 26 Jan 2021 16:10:33 +0000 (13:10 -0300)
committerGitHub <noreply@github.com>
Tue, 26 Jan 2021 16:10:33 +0000 (13:10 -0300)
commit022dbeb9e2dc925cf0dcffb75ea57aedf09395de
tree433ee1b826bafad9c311e22288e18e28d868e9c8tree
parent909a0aa67266d7659decf56f2e6eb8101a802d45commit | 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.
src/api/cvc4cpp.cpp diff | blob | history
src/api/cvc4cpp.h diff | blob | history
src/expr/symbol_table.cpp diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress0/parser/define_sort.smt2 [new file with mode: 0644] blob
test/unit/api/solver_black.cpp diff | blob | history