bv_decide - kernel deterministic timeout + ofBool normalization #6043
Comments
|
The error is correct but the diagnosis around |
AFAIU there are two issues in this test case. One is the fundamental issue with 'deterministic timeout'. The second is that bv_normalize should normalize this better. In particular, we currently get: theorem extracted_1 (x : BitVec 32) :
BitVec.ofBool (x != 51#32) &&& BitVec.ofBool (x != 50#32) =
BitVec.ofBool (4294967294#32 > x + 4294967244#32) := by
/-
case h
x : BitVec 32
a✝ : (!((if (!x == 51#32) = true then 1#1 else 0#1) &&& if (!x == 50#32) = true then 1#1 else 0#1) ==
if (x + 4294967244#32).ult 4294967294#32 = true then 1#1 else 0#1) =
true
⊢ False
-/
bv_normalizebut should get theorem extracted_1 (x : BitVec 32) :
BitVec.ofBool (x != 51#32) &&& BitVec.ofBool (x != 50#32) =
BitVec.ofBool (4294967294#32 > x + 4294967244#32) := by
simp [BitVec.ofBool_and_ofBool, BitVec.ofBool_eq_iff_eq]
/-
case h
x : BitVec 32
a✝ : (!(!x == 51#32 && !x == 50#32) == (x + 4294967244#32).ult 4294967294#32) = true
⊢ False
-/
bv_normalize
bv_decideThis improved Or is there a reason we would want to bit-blast an if-statement if there is a way to eliminate it? |
|
There is almost no difference between the bitblasted versions of these two, they get solved in basically the same time. The way to rewrite this would be with rewrite rules on the |
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
Prerequisites
Please put an X between the brackets as you perform the following steps:
https://github.com/leanprover/lean4/issues
Avoid dependencies to Mathlib or Batteries.
https://live.lean-lang.org/#project=lean-nightly
(You can also use the settings there to switch to “Lean nightly”)
Description
The following test case fails with 'kernel deterministic timeout)
import Lean.Elab.Tactic.BVDecide
Steps to Reproduce
Expected behavior: bv_decide should solve this goal quickly. In case it fails, it should not be a kernel timeout
Actual behavior: A kernel timeout
Versions
Lean 4.15.0-nightly-2024-11-11
Target: arm64-apple-darwin23.6.0 macOS
Additional Information
This bug goes away if I simplify with the relevant
ofBool_*theorems. Adding them tobv_normalizedoes not help, though.Impact
Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.
The text was updated successfully, but these errors were encountered: