projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 9108877) | patch
Remove support for unused `declare-*` commands (#8623)
authorAndres Noetzli <andres.noetzli@gmail.com>
Mon, 18 Apr 2022 13:30:30 +0000 (06:30 -0700)
committerGitHub <noreply@github.com>
Mon, 18 Apr 2022 13:30:30 +0000 (13:30 +0000)
commit8aac04e31310be4fb80fb60df0c88751ee457f6c
tree255ce6387c80b35faa5deaab9415cf4b84cb5a64tree
parent910887748fef32cf57c0bad3b5eac2c44d6f48f8commit | diff
Remove support for unused `declare-*` commands (#8623)

This commit removes support for
declare-sorts/declare-funs/declare-preds. These commands seem to
be a leftover of an earlier SMT-LIB draft [0]. We only had a test for
declare-funs and Z3 doesn't support declare-funs either.

[0] http://homepage.cs.uiowa.edu/~astump/papers/smt-cmd-lang.pdf
NEWS.md diff | blob | history
src/parser/smt2/Smt2.g diff | blob | history
test/regress/cli/CMakeLists.txt diff | blob | history
test/regress/cli/regress0/declare-funs.smt2 [deleted file] blob | history