diff options
| author | yoni206 <yoni206@users.noreply.github.com> | 2020-12-03 12:18:10 -0800 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-12-03 14:18:10 -0600 |
| commit | 8994bc9fd49a255286f8a6bac6c14407e8add41f (patch) | |
| tree | 145ea96fcb9381be1aa2f298ca66165d12864682 /src/options/smt_options.toml | |
| parent | 8e1dc557383f754e33399b6b0f783e7048732df0 (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.
Diffstat (limited to 'src/options/smt_options.toml')
| -rw-r--r-- | src/options/smt_options.toml | 8 |
1 files changed, 6 insertions, 2 deletions
diff --git a/src/options/smt_options.toml b/src/options/smt_options.toml index 405abfc4f..08d53855c 100644 --- a/src/options/smt_options.toml +++ b/src/options/smt_options.toml @@ -417,7 +417,7 @@ header = "options/smt_options.h" category = "regular" long = "model-u-print=MODE" type = "ModelUninterpPrintMode" - default = "DeclFun" + default = "None" read_only = true help = "determines how to print uninterpreted elements in models" help_mode = "uninterpreted elements in models printing modes." @@ -429,7 +429,11 @@ header = "options/smt_options.h" help = "print uninterpreted elements declare-fun, and also include a declare-sort for the sort" [[option.mode.DeclFun]] name = "decl-fun" - help = "(default) print uninterpreted elements declare-fun, but don't include a declare-sort for the sort" + help = "print uninterpreted elements declare-fun, but don't include a declare-sort for the sort" +[[option.mode.None]] + name = "none" + help = "(default) do not print declarations of uninterpreted elements in models." + [[option]] name = "modelWitnessValue" |