projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 8e1dc55) | patch
Models as (#5581)
authoryoni206 <yoni206@users.noreply.github.com>
Thu, 3 Dec 2020 20:18:10 +0000 (12:18 -0800)
committerGitHub <noreply@github.com>
Thu, 3 Dec 2020 20:18:10 +0000 (14:18 -0600)
commit8994bc9fd49a255286f8a6bac6c14407e8add41f
tree145ea96fcb9381be1aa2f298ca66165d12864682tree
parent8e1dc557383f754e33399b6b0f783e7048732df0commit | diff
Models as (#5581)

This PR relates to #4987 .
Our plan is to:

delete the model keyword (done in #5415 )
avoid printing extra declarations by default (done in #5432 )
wrap UF values with as expressions.
This PR does step 3, fixes a regression accordingly, and adds the formula from #4987 and a variant of it to the regressions.
src/options/smt_options.toml diff | blob | history
src/printer/smt2/smt2_printer.cpp diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress0/models-print-1.smt2 [new file with mode: 0644] blob
test/regress/regress0/models-print-2.smt2 [new file with mode: 0644] blob
test/regress/regress0/printer/empty_sort.smt2 diff | blob | history