diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-07-01 14:54:41 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-07-01 14:54:41 -0500 |
| commit | e968ea45fd46ce6837d50b2893568872378171f1 (patch) | |
| tree | 1e9f4e720830562e4bbf77186ca90f85405aea9c /src/options/smt_options.toml | |
| parent | 9ce4c3153d42bc079470b7bd73bf131499b3fcbe (diff) | |
Add solver for integer AND (#4681)
This omits certain inference schemas (sum and bitwise lemmas) which depends on an option that will be added later.
Diffstat (limited to 'src/options/smt_options.toml')
| -rw-r--r-- | src/options/smt_options.toml | 19 |
1 files changed, 19 insertions, 0 deletions
diff --git a/src/options/smt_options.toml b/src/options/smt_options.toml index c104cb3e7..c09f8bbf3 100644 --- a/src/options/smt_options.toml +++ b/src/options/smt_options.toml @@ -651,6 +651,25 @@ header = "options/smt_options.h" help = "attempt to solve BV formulas by translation to integer arithmetic (experimental)" [[option]] + name = "iandMode" + category = "undocumented" + long = "iand-mode=mode" + type = "IandMode" + default = "VALUE" + read_only = true + help = "Set the refinement scheme for integer AND" + help_mode = "Refinement modes for integer AND" + [[option.mode.VALUE]] + name = "value" + help = "value-based refinement" + [[option.mode.SUM]] + name = "sum" + help = "use sum to represent integer AND in refinement" + [[option.mode.BITWISE]] + name = "bitwise" + help = "use bitwise comparisons on binary representation of integer for refinement (experimental)" + +[[option]] name = "solveIntAsBV" category = "undocumented" long = "solve-int-as-bv=N" |