This PR adds SMT-LIB operators to detect overflow
`BitVec.(uadd_overflow, sadd_overflow)`, according to the definitions
[here](https://github.com/SMT-LIB/SMT-LIB-2/blob/2.7/Theories/FixedSizeBitVectors.smt2),
and the theorems proving equivalence of such definitions with the
`BitVec` library functions (`uaddOverflow_eq`, `saddOverflow_eq`).
Support theorems for these proofs are `BitVec.toNat_mod_cancel_of_lt,
BitVec.toInt_lt, BitVec.le_toInt, Int.bmod_neg_iff`. The PR also
includes a set of tests.
---------
Co-authored-by: Tobias Grosser <github@grosser.es>
Co-authored-by: Alex Keizer <alex@keizer.dev>
Co-authored-by: Tobias Grosser <tobias@grosser.es>
Co-authored-by: Siddharth Bhat <siddu.druid@gmail.com>
This PR implements two rules for bv_decide's preprocessor, lowering
`|||` to `&&&` in order to enable more term sharing + application of
rules about `&&&` as well as rewrites of the form `(a &&& b == -1#w) =
(a == -1#w && b == -1#w)` in order to preserve rewriting behavior that
already existed before this lowering.
This PR teaches bv_normalize to replace subtractions on one side of an
equality with an addition on the other side, this re-write eliminates a
not + addition in the normalized form so it is easier on the solver.
Note that I also make a point to normalize (1 + ~~~x) to (~~~x + 1) to
limit the amount of boilerplate symmetry theorems we require.
This PR adds BitVec lemmas required to cancel multiplicative negatives,
and plumb support through to bv_normalize to make use of this result in
the normalized twos-complement form.
I include some bmod lemmas I found useful to prove this result, the two
helper lemmas I add use the same naming/proofs as their emod
equivalents.
This PR makes `bv_normalize` rewrite shifts by `BitVec` constants to
shifts by `Nat` constants. This is part of the greater effort in
providing good support for constant shift simplification in
`bv_normalize`.
This PR adds add/sub injectivity lemmas for BitVec, and then adds
specialized forms with additional symmetries for the `bv_normalize`
normal form.
Since I need `neg_inj`, I add `not_inj`/`neg_inj` at once, and use it in
`BitVec.not_beq_not` instead of re-proving it.
This PR adds a BitVec lemma that `(x >> x) = 0` and plumbs it through to
bv_normalize. I also move some theorems I found useful to the top of the
ushiftRight section.
This PR adds a number of simple comparison lemmas to the top/bottom
element for BitVec. Then they are applied to teach bv_normalize that
`(a<1) = (a==0)` and to remove an intermediate proof that is no longer
necessary along the way.
This PR adds a fast path for bitblasting multiplication with constants
in `bv_decide`.
While the circuit generated is the same (as the AIG already performs
constant folding) this avoids calling out to the shift and addition
bitblaster unless required. Thus the overall time to generate the
circuit is reduced. Inspired by
[bitwuzla](25d77f819c/src/lib/bitblast/bitblaster.h (L454)).
This PR adds support for `bv_decide` to automatically split up
non-recursive structures that contain information about supported types.
It can be controlled using the new `structures` field in the `bv_decide`
config.
This PR puts the `bv_normalize` simp set into simp_nf and splits up the
bv_normalize implementation across multiple files in preparation for
upcoming changes.
This PR fixes a slight bug that was created in the reflection of `bif`
in `bv_decide`.
Tagged as changelog-no as the code in question isn't in an RC yet.
This PR improves bv_decide's performance in the presence of large
literals.
The core change of this PR is the reformulation of the reflection code
for literals to:
```diff
def eval (assign : Assignment) : BVExpr w → BitVec w
| .var idx =>
- let ⟨bv⟩ := assign.get idx
- bv.truncate w
+ let packedBv := assign.get idx
+ /-
+ This formulation improves performance, as in a well formed expression the condition always holds
+ so there is no need for the more involved `BitVec.truncate` logic.
+ -/
+ if h : packedBv.w = w then
+ h ▸ packedBv.bv
+ else
+ packedBv.bv.truncate w
```
The remainder is merely further simplifications that make the terms
smaller and easier to deal with in general. This change is motivated by
applying the following diff to the kernel:
```diff
diff --git a/src/kernel/type_checker.cpp b/src/kernel/type_checker.cpp
index b0e6844dca..f13bb96bd4 100644
--- a/src/kernel/type_checker.cpp
+++ b/src/kernel/type_checker.cpp
@@ -518,6 +518,7 @@ optional<constant_info> type_checker::is_delta(expr const & e) const {
optional<expr> type_checker::unfold_definition_core(expr const & e) {
if (is_constant(e)) {
if (auto d = is_delta(e)) {
+// std::cout << "Working on unfolding: " << d->get_name() << std::endl;
if (length(const_levels(e)) == d->get_num_lparams()) {
if (m_diag) {
m_diag->record_unfold(d->get_name());
```
and observing that in the test case from #6043 we see a long series of
```
Working on unfolding: Bool.decEq
Working on unfolding: Bool.decEq.match_1
Working on unfolding: Bool.casesOn
Working on unfolding: Nat.ble
Working on unfolding: Nat.brecOn
Working on unfolding: Nat.beq.match_1
Working on unfolding: Nat.casesOn
Working on unfolding: Nat.casesOn
Working on unfolding: Nat.beq.match_1
Working on unfolding: Nat.casesOn
Working on unfolding: Nat.casesOn
```
the chain begins with `BitVec.truncate`, works through a few
abstractions and then continues like above forever, so I avoid the call
to truncate like this. It is not quite clear to me why removing `ofBool`
helps so much here, maybe some other kernel heuristic kicks in to rescue
us.
Either way this diff is a general improvement for reflection of `BitVec`
constants as we should never have to run `BitVec.truncate` again!
Fixes: #6043
This PR ensures that the configuration in `Simp.Config` is used when
reducing terms and checking definitional equality in `simp`.
closes#5455
---------
Co-authored-by: Kim Morrison <kim@tqft.net>
This PR adds `BitVec.[toFin|getMsbD]_setWidth` and
`[getMsb|msb]_signExtend` as well as `ofInt_toInt`.
Also correct renamed the misnamed theorem for
`signExtend_eq_setWidth_of_msb_false`.
---------
Co-authored-by: Siddharth <siddu.druid@gmail.com>
This PR uses Lean.RArray in bv_decide's reflection proofs. Giving
speedups on problems with lots of variables.
Implement like #6068, speedup:
```
# before
λ hyperfine "lean +nightly-2024-12-02 tests/lean/run/bv_reflection_stress.lean"
Benchmark 1: lean +nightly-2024-12-02 tests/lean/run/bv_reflection_stress.lean
Time (mean ± σ): 1.939 s ± 0.007 s [User: 1.549 s, System: 0.104 s]
Range (min … max): 1.928 s … 1.947 s 10 runs
# after
λ hyperfine "lean tests/lean/run/bv_reflection_stress.lean"
Benchmark 1: lean tests/lean/run/bv_reflection_stress.lean
Time (mean ± σ): 1.409 s ± 0.006 s [User: 1.058 s, System: 0.073 s]
Range (min … max): 1.401 s … 1.419 s 10 runs
```
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.
Following up #5928, updates the syntax for `omega` and `solve_by_elim`
and restores the syntax quotations in their implementations.
Following up #5898, uses the new tactic syntax in the library, replacing
all uses of `(config := ...)`.
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.
