diff options
| author | yoni206 <yoni206@users.noreply.github.com> | 2020-07-11 04:39:56 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-07-11 06:39:56 -0500 |
| commit | c481454a4b05a78ea99e835ec7427a719a2d5c77 (patch) | |
| tree | 9e1b3d680f2ffe418317c014fd4e733ff68cc0a5 /src/options/smt_options.toml | |
| parent | 9aab4da2460b62273ac937ad96b7b6695b904e0d (diff) | |
Changing bv_to_int options (#4721)
This PR changes --solve-bv-as-int from a numerical option (specifying the granularity) to an enum (specifying the approach). Currently we support only two modes: OFF and SUM. Future PRs will add more modes.
The numerical value of the granularity is now captured by the new option --bvand-integer-granularity.
Tests are updated accordingly.
Diffstat (limited to 'src/options/smt_options.toml')
| -rw-r--r-- | src/options/smt_options.toml | 21 |
1 files changed, 18 insertions, 3 deletions
diff --git a/src/options/smt_options.toml b/src/options/smt_options.toml index 13791bfd6..80183b71f 100644 --- a/src/options/smt_options.toml +++ b/src/options/smt_options.toml @@ -639,11 +639,26 @@ header = "options/smt_options.h" [[option]] name = "solveBVAsInt" category = "undocumented" - long = "solve-bv-as-int=N" + long = "solve-bv-as-int=MODE" + type = "SolveBVAsIntMode" + default = "OFF" + help = "mode for translating BVAnd to integer" + help_mode = "solve-bv-as-int modes." +[[option.mode.OFF]] + name = "off" + help = "Do not translate bit-vectors to integers" +[[option.mode.SUM]] + name = "sum" + help = "Generate a sum expression for each bvand instance, based on the value in --solbv-bv-as-int-granularity" + +[[option]] + name = "BVAndIntegerGranularity" + category = "undocumented" + long = "bvand-integer-granularity=N" type = "uint32_t" - default = "0" + default = "1" read_only = true - help = "attempt to solve BV formulas by translation to integer arithmetic (experimental)" + help = "granularity to use in --solve-bv-as-int mode and for iand operator (experimental)" [[option]] name = "iandMode" |