diff options
| author | Mathias Preiner <mathias.preiner@gmail.com> | 2021-05-13 17:29:52 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-05-14 00:29:52 +0000 |
| commit | b59deea057513448d98f54629c78a38a81f99b27 (patch) | |
| tree | 4f4458795bc505173710786a932c3babf9a1b5d4 /src/options | |
| parent | d7b74a33e3722dd123ecfb79603538cc5ac889a0 (diff) | |
bv: Assert input facts on user-level 0. (#6515)
The bitblast solver currently uses solving under assumptions for all facts that are sent to the bit-vector solver. For input facts on user-level 0 we can however assert the fact to the SAT solver, which allows the SAT solver to do more preprocessing. This PR adds the option to assert user-level 0 input facts, which is disabled by default.
Diffstat (limited to 'src/options')
| -rw-r--r-- | src/options/bv_options.toml | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/src/options/bv_options.toml b/src/options/bv_options.toml index 3172f8d5f..34bdfcdaa 100644 --- a/src/options/bv_options.toml +++ b/src/options/bv_options.toml @@ -243,3 +243,11 @@ name = "Bitvector theory" name = "simple" help = "Enables simple bitblasting solver with proof support." +[[option]] + name = "bvAssertInput" + category = "regular" + long = "bv-assert-input" + type = "bool" + default = "false" + help = "assert input assertions on user-level 0 instead of assuming them in the bit-vector SAT solver" + |