This PR fixes `bv_decide`'s embedded constraint substitution to generate
correct counter examples in the corner case where duplicate theorems are
in the local context.
This PR introduces the and flattening pre processing pass from Bitwuzla
to `bv_decide`. It splits hypotheses of the form `(a && b) = true` into
`a = true` and `b = true` which has synergy potential with the already
existing embedded constraint substitution pass.
Beyond this I also added some profiling infra structure for the passes.
This PR adds a normalization rule to `bv_normalize` (which is used by
`bv_decide`) that converts `x / 2^k` into `x >>> k` under suitable
conditions. This allows us to simplify the expensive division circuits
that are used for bitblasting into much cheaper shifting circuits.
Concretely, it allows for the following canonicalization:
```lean
example {x : BitVec 16} : x / (BitVec.twoPow 16 2) = x >>> 2 := by bv_normalize
example {x : BitVec 16} : x / (BitVec.ofNat 16 8) = x >>> 3 := by bv_normalize
```
This PR changes `bv_decide`'s configuration from lots of `set_option` to
an elaborated config like `simp` or `omega`. The notable exception is
`sat.solver` which is still a `set_option` such that users can configure
a custom SAT solver globally for an entire project or file. Additionally
it introduces the ability to set `maxSteps` for the simp preprocessing
run through the new config.
The latter feature was requested by people using `bv_decide` on SMTLIB
which has ginormous terms that exceed the default.
Using the same strategy as #5852 this provides `bv_decide` support for
`Bool` and `BitVec` ifs
this in turn instantly enables support for:
- `sdiv`
- `smod`
- `abs`
and thus closes our last discrepancies to QF_BV!
This is the first step towards fixing the issue of not having mutual
recursion between the `Bool` and `BitVec` fragment of `QF_BV` in
`bv_decide`. This PR adds support for `BitVec.ofBool` by doing the
following:
1. Introduce a new mechanism into the reification engine that allows us
to add additional lemmas to the top level on the fly as we are
traversing the expression tree.
2. If we encounter an expression `BitVec.ofBool boolExpr` we reify
`boolExpr` and then abstract `BitVec.ofBool boolExpr` as some atom `a`
3. We add two lemmas `boolExpr = true -> a = 1#1` and `boolExpr = false
-> a = 0#1`. This mirrors the full behavior of `BitVec.ofBool` and thus
makes our atom `a` correctly interpreted again.
In order to do the reification in step 2 mutual recursion in the
reification engine is required. For this reason I started pulling out
logic from the, now rather large, mutual block into other files and
document the invariants that they assume explicitly.
We trust that the users read the error messages or tactic docs to
discover the option.
AWS problems have shown that this can be too eager of an operation to
do.
Given that we have the luxury of interactivity let's go for an approach
where the users
can optionally enable it.
... while at it also call `trivial` to close goals that can be trivially
closed.
---------
Co-authored-by: Siddharth <siddu.druid@gmail.com>
Co-authored-by: Henrik Böving <hargonix@gmail.com>
