projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: a19e20c) | patch
Models standard (#5415)
authoryoni206 <yoni206@users.noreply.github.com>
Thu, 12 Nov 2020 22:00:14 +0000 (14:00 -0800)
committerGitHub <noreply@github.com>
Thu, 12 Nov 2020 22:00:14 +0000 (16:00 -0600)
commit3db60fa3fba4787cc33a61c1a357c43ba1cc9d6d
tree5d28086747e689cb3499873bf23c1c8fe3178785tree
parenta19e20cd3049134b15dbdcf7854a8854a77ccc43commit | diff
Models standard (#5415)

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

delete the model keyword
avoid printing extra declarations by default
wrap UF values with as expressions.
This PR does step 1, and fixes regressions accordingly.
NEWS diff | blob | history
src/printer/smt2/smt2_printer.cpp diff | blob | history
test/regress/regress0/datatypes/dt-param-2.6-print.smt2 diff | blob | history
test/regress/regress0/parser/strings20.smt2 diff | blob | history
test/regress/regress0/parser/strings25.smt2 diff | blob | history
test/regress/regress0/simple-dump-model.smt2 diff | blob | history
test/regress/regress0/smt2output.smt2 diff | blob | history