WIP - Implement Generalizer #1022
Conversation
| import SSA.Experimental.Bits.Fast.Defs | ||
| import SSA.Experimental.Bits.Fast.FiniteStateMachine | ||
| import SSA.Experimental.Bits.Fast.Attr | ||
| import SSA.Experimental.Bits.Fast.Decide |
There was a problem hiding this comment.
This tactic should not depend on Mathlib or SSA, no?
| (fun ix => inputs.map ⟨fun input => Inputs.mk ix input, by intros a b; simp⟩) | ||
| ⟨out, by | ||
| ⟨out, by |
There was a problem hiding this comment.
These changes seem unrelated, no?
There was a problem hiding this comment.
They are unrelated. My editor keeps removing these trailing whitespaces, which seems to be according to the setting here, but I'm not sure why they were present before.
There was a problem hiding this comment.
It might be worth to commit these whitespace separately, so this diff is clean and our codebase is also cleaner.
| BVExpr.shiftRight (substituteBVExpr lhs) (substituteBVExpr rhs) | ||
| | .arithShiftRight lhs rhs => | ||
| BVExpr.arithShiftRight (substituteBVExpr lhs) (substituteBVExpr rhs) | ||
| | _ => bvExpr --TODO: handle other constructors? |
There was a problem hiding this comment.
Yeah, you need to handle all constructors which contain expressions
oluwatimilehin
force-pushed
the
exists-forall
branch
from
a972112 to
47493ff
Compare
…ins; constraint constants when bitshifts are involved; cleanup, etc
oluwatimilehin
force-pushed
the
exists-forall
branch
from
a20dc4d to
0f7b444
Compare
|
|
||
| -- x + c1 == c1 | ||
| let lhs := BVExpr.bin x BVBinOp.add c1 | ||
| BoolExpr.literal (BVPred.bin lhs BVBinPred.eq x) |
|
I'd suggest the following course of action:
|
|
@oluwatimilehin could you please merge |
|
@oluwatimilehin It seems the CI fails, and I conjecture it's because it's not setup to work well with forks. Could you close this PR, and reopen it as a branch against |
|
Created #1153 |
No description provided.