diff options
author | yoni206 <yoni206@users.noreply.github.com> | 2020-11-13 11:23:49 -0800 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-11-13 13:23:49 -0600 |
commit | 91050c4da5d2ed0b22bf935c09c46184f6fde77e (patch) | |
tree | 00a8ae99e9e5fe7e119d3dcce0c38cff65411db6 /src/options | |
parent | 74be116f3956dab6be0b8e3e18f723957a351fbf (diff) |
Model declarations printing options (#5432)
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 is step 2. It allows the user to choose the model printing style in case of uninterpreted elements: either using datatypes, or using declare-sorts and declare-funs or just using declare-funs.
The default option, which is closest to the standard, is just using declare-funs. In step 3, these will be replaced by abstract values using as.
Diffstat (limited to 'src/options')
-rw-r--r-- | src/options/smt_options.toml | 25 |
1 files changed, 18 insertions, 7 deletions
diff --git a/src/options/smt_options.toml b/src/options/smt_options.toml index 54d81eba6..55ba43ce9 100644 --- a/src/options/smt_options.toml +++ b/src/options/smt_options.toml @@ -412,13 +412,24 @@ header = "options/smt_options.h" help = "in models, output arrays (and in future, maybe others) using abstract values, as required by the SMT-LIB standard" [[option]] - name = "modelUninterpDtEnum" - category = "regular" - long = "model-u-dt-enum" - type = "bool" - default = "false" - read_only = true - help = "in models, output uninterpreted sorts as datatype enumerations" + name = "modelUninterpPrint" + smt_name = "model-uninterp-print" + category = "regular" + long = "model-u-print=MODE" + type = "ModelUninterpPrintMode" + default = "DeclFun" + read_only = true + help = "determines how to print uninterpreted elements in models" + help_mode = "uninterpreted elements in models printing modes." +[[option.mode.DtEnum]] + name = "dtenum" + help = "print uninterpreted elements as datatype enumerations, where the sort is the datatype" +[[option.mode.DeclSortAndFun]] + name = "decl-sort-and-fun" + 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" [[option]] name = "modelWitnessValue" |