diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-05-23 15:44:50 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-05-23 15:44:50 -0500 |
| commit | a96fbfe33c05bea0b94d5387dda65c2ae343f66b (patch) | |
| tree | a3b1e28dc45f05ef218331217ed072e842d6dfd3 /src/options/theory_options.toml | |
| parent | 4c2138a14c4abba2431bc8ba51359d3a565baf05 (diff) | |
Add notions of evaluated kinds in TheoryModel (#1947)
Diffstat (limited to 'src/options/theory_options.toml')
| -rw-r--r-- | src/options/theory_options.toml | 17 |
1 files changed, 17 insertions, 0 deletions
diff --git a/src/options/theory_options.toml b/src/options/theory_options.toml index 2b1f75072..3509f408d 100644 --- a/src/options/theory_options.toml +++ b/src/options/theory_options.toml @@ -23,3 +23,20 @@ header = "options/theory_options.h" notifies = ["notifyUseTheoryList"] read_only = true help = "use alternate theory implementation NAME (--use-theory=help for a list). This option may be repeated or a comma separated list." + +[[option]] + name = "assignFunctionValues" + category = "regular" + long = "assign-function-values" + type = "bool" + default = "true" + help = "assign values for uninterpreted functions in models" + +[[option]] + name = "condenseFunctionValues" + category = "regular" + long = "condense-function-values" + type = "bool" + default = "true" + read_only = true + help = "condense values for functions in models rather than explicitly representing them" |