Blase: Add a tactic to genralize the widths of bitvectors #1756
Conversation
|
bv_decide solved 0 theorems. |
ineol
force-pushed
the
push-tnpkrqksnkvx
branch
from
d003a14 to
9feffb1
Compare
|
bv_decide solved 0 theorems. |
ineol
force-pushed
the
push-tnpkrqksnkvx
branch
2 times, most recently
from
e6f5a3d to
0cbe25c
Compare
|
@bollu it seems to be working now |
|
bv_decide solved 0 theorems. |
1 similar comment
|
bv_decide solved 0 theorems. |
There was a problem hiding this comment.
While I agree that this is a viable approach, I had a different algorithm in mind:
At each function application f x1 ... xn, infer the type of the function as f : T1 -> T2 .. -> Tn -> O. Inspect the (xi, ti), and if the type ti is a BitVec K, we perform the generalization as you did. This avoids the need for a table, but I guess I'm now not sure about the tradeoffs between having a table and not having one.
Anyway, LGTM to me! I wrote down some comments, but none of them are blockers to merging.
Thanks muchly ^_^
Blase/Blase/MultiWidth/Tactic.lean
Outdated
| for (e', x) in s.mapping do | ||
| if ← isDefEq e e' then | ||
| return x |
There was a problem hiding this comment.
| for (e', x) in s.mapping do | |
| if ← isDefEq e e' then | |
| return x | |
| /-- TODO: Instead of using a HashMap, consider using a DiscrTree. -/ | |
| for (e', x) in s.mapping do | |
| if ← isDefEq e e' then | |
| return x |
There was a problem hiding this comment.
Hmm is there a good way to recover the original expression from the keys of the tree?
| let arg ← if bv? i then State.add? arg else visit arg | ||
| pure <| .app res arg | ||
| | .forallE n e₁ e₂ info => | ||
| pure <| .forallE n (← visit e₁) (← visit e₂) info |
There was a problem hiding this comment.
Why don't you use the combinators forallTelescoping and instead work with raw BVars? I guess in this case it's OK, but I do wonder why you prefer the approach :)
There was a problem hiding this comment.
Hmm we want to recurse in e1 so we'd need to first change the types in the telescope and then use forallTelescope right?
| def genTable : Std.HashMap Name (Array Bool) := Id.run do | ||
| let mut table := .emptyWithCapacity 16 | ||
| table := table.insert ``BitVec #[true] | ||
| table := table.insert ``BitVec.zeroExtend #[true, true, false] | ||
| table := table.insert ``BitVec.signExtend #[true, true, false] | ||
| table := table.insert ``BitVec.instAdd #[true] | ||
| table := table.insert ``BitVec.instSub #[true] | ||
| table := table.insert ``BitVec.instMul #[true] | ||
| table := table.insert ``BitVec.instDiv #[true] | ||
| table |
There was a problem hiding this comment.
Don't we want to always generalize a BV variable? My intuition is that instead of having a table, we check if a value has type BitVec w, and if it is, we generalize it, with a possible exception for BitVec 1?
There was a problem hiding this comment.
The problem is that we want to generalize 10 in x.signExtend 10 but it's only because we know that the first parameter of signExtend is a width and not a random Nat.
A more rigorous approach would be to analyze at the type of signExtend and see that the variable appears as a paramter of BitVec and recover the information in the table like that, but it seems complicated.
There was a problem hiding this comment.
I just read your comment above, so we agree on the method :)
I think we can try this simple approach and see if it's sufficient for the evaluation.
ineol
force-pushed
the
push-tnpkrqksnkvx
branch
from
0cbe25c to
867a36c
Compare
|
bv_decide solved 0 theorems. |
2 participants
It seems to be working on a small example.
It needs to special case functions such as
zeroExtendto recognize that some parameters are "width" parameters.