feat: add all bitwuzla level 1 if rewrites to bv_decide (#7275)
This PR adds all level 1 rewrites from Bitwuzla to the preprocessor of bv_decide.
This commit is contained in:
Henrik Böving
GitHub
parent
75df4c0b52
commit
84da113355
2 changed files with 297 additions and 0 deletions
|
|
@ -6,6 +6,7 @@ Authors: Henrik Böving
|
|||
prelude
|
||||
import Init.SimpLemmas
|
||||
import Init.Data.Bool
|
||||
import Init.Data.BitVec.Lemmas
|
||||
|
||||
/-!
|
||||
This module contains the `Bool` simplifying part of the `bv_normalize` simp set.
|
||||
|
|
@ -54,6 +55,153 @@ theorem Bool.not_xor : ∀ (a b : Bool), !(a ^^ b) = (a == b) := by decide
|
|||
@[bv_normalize]
|
||||
theorem Bool.or_elim : ∀ (a b : Bool), (a || b) = !(!a && !b) := by decide
|
||||
|
||||
@[bv_normalize]
|
||||
theorem Bool.not_beq_one : ∀ (a : BitVec 1), (!(a == 1#1)) = (a == 0#1) := by
|
||||
decide
|
||||
|
||||
@[bv_normalize]
|
||||
theorem Bool.not_beq_zero : ∀ (a : BitVec 1), (!(a == 0#1)) = (a == 1#1) := by
|
||||
decide
|
||||
|
||||
@[bv_normalize]
|
||||
theorem Bool.not_one_beq : ∀ (a : BitVec 1), (!(1#1 == a)) = (a == 0#1) := by
|
||||
decide
|
||||
|
||||
@[bv_normalize]
|
||||
theorem Bool.not_zero_beq : ∀ (a : BitVec 1), (!(0#1 == a)) = (a == 1#1) := by
|
||||
decide
|
||||
|
||||
@[bv_normalize]
|
||||
theorem Bool.ite_same_then : ∀ (c t e : Bool), ((bif c then t else e) == t) = (c || (t == e)) := by
|
||||
decide
|
||||
|
||||
@[bv_normalize]
|
||||
theorem Bool.ite_same_then' : ∀ (c t e : Bool), (t == (bif c then t else e)) = (c || (t == e)) := by
|
||||
decide
|
||||
|
||||
@[bv_normalize]
|
||||
theorem Bool.ite_same_else : ∀ (c t e : Bool), ((bif c then t else e) == e) = (!c || (t == e)) := by
|
||||
decide
|
||||
|
||||
@[bv_normalize]
|
||||
theorem Bool.ite_same_else' :
|
||||
∀ (c t e : Bool), (e == (bif c then t else e)) = (!c || (t == e)) := by
|
||||
decide
|
||||
|
||||
@[bv_normalize]
|
||||
theorem BitVec.ite_same_then :
|
||||
∀ (c : Bool) (t e : BitVec w), ((bif c then t else e) == t) = (c || (t == e)) := by
|
||||
intro c t e
|
||||
cases c <;> simp [BEq.comm (a := t) (b := e)]
|
||||
|
||||
@[bv_normalize]
|
||||
theorem BitVec.ite_same_then' :
|
||||
∀ (c : Bool) (t e : BitVec w), (t == (bif c then t else e)) = (c || (t == e)) := by
|
||||
intro c t e
|
||||
cases c <;> simp
|
||||
|
||||
@[bv_normalize]
|
||||
theorem BitVec.ite_same_else :
|
||||
∀ (c : Bool) (t e : BitVec w), ((bif c then t else e) == e) = (!c || (t == e)) := by
|
||||
intro c t e
|
||||
cases c <;> simp
|
||||
|
||||
@[bv_normalize]
|
||||
theorem BitVec.ite_same_else' :
|
||||
∀ (c : Bool) (t e : BitVec w), (e == (bif c then t else e)) = (!c || (t == e)) := by
|
||||
intro c t e
|
||||
cases c <;> simp [BEq.comm (a := t) (b := e)]
|
||||
|
||||
@[bv_normalize]
|
||||
theorem Bool.ite_then_ite (cond : Bool) {a b c : α} :
|
||||
(bif cond then (bif cond then a else b) else c) = (bif cond then a else c) := by
|
||||
cases cond <;> simp
|
||||
|
||||
@[bv_normalize]
|
||||
theorem Bool.ite_then_not_ite (cond : Bool) {a b c : Bool} :
|
||||
(bif cond then !(bif cond then a else b) else c) = (bif cond then !a else c) := by
|
||||
cases cond <;> simp
|
||||
|
||||
@[bv_normalize]
|
||||
theorem BitVec.ite_then_not_ite (cond : Bool) {a b c : BitVec w} :
|
||||
(bif cond then ~~~(bif cond then a else b) else c) = (bif cond then ~~~a else c) := by
|
||||
cases cond <;> simp
|
||||
|
||||
@[bv_normalize]
|
||||
theorem Bool.ite_else_ite (cond : Bool) {a b c : α} :
|
||||
(bif cond then a else (bif cond then b else c)) = (bif cond then a else c) := by
|
||||
cases cond <;> simp
|
||||
|
||||
@[bv_normalize]
|
||||
theorem Bool.ite_else_not_ite (cond : Bool) {a b c : Bool} :
|
||||
(bif cond then a else !(bif cond then b else c)) = (bif cond then a else !c) := by
|
||||
cases cond <;> simp
|
||||
|
||||
@[bv_normalize]
|
||||
theorem BitVec.ite_else_not_ite (cond : Bool) {a b c : BitVec w} :
|
||||
(bif cond then a else ~~~(bif cond then b else c)) = (bif cond then a else ~~~c) := by
|
||||
cases cond <;> simp
|
||||
|
||||
@[bv_normalize]
|
||||
theorem Bool.ite_then_ite' (c0 c1 : Bool) {a b : α} :
|
||||
(bif c0 then (bif c1 then a else b) else a) = (bif c0 && !c1 then b else a) := by
|
||||
cases c0 <;> cases c1 <;> simp
|
||||
|
||||
@[bv_normalize]
|
||||
theorem Bool.ite_then_not_ite' (c0 c1 : Bool) {a b : Bool} :
|
||||
(bif c0 then !(bif c1 then !a else b) else a) = (bif c0 && !c1 then !b else a) := by
|
||||
cases c0 <;> cases c1 <;> simp
|
||||
|
||||
@[bv_normalize]
|
||||
theorem BitVec.ite_then_not_ite' (c0 c1 : Bool) {a b : BitVec w} :
|
||||
(bif c0 then ~~~(bif c1 then ~~~a else b) else a) = (bif c0 && !c1 then ~~~b else a) := by
|
||||
cases c0 <;> cases c1 <;> simp
|
||||
|
||||
@[bv_normalize]
|
||||
theorem Bool.ite_else_ite' (c0 c1 : Bool) {a b : α} :
|
||||
(bif c0 then a else (bif c1 then a else b)) = (bif !c0 && !c1 then b else a) := by
|
||||
cases c0 <;> cases c1 <;> simp
|
||||
|
||||
@[bv_normalize]
|
||||
theorem Bool.ite_else_not_ite' (c0 c1 : Bool) {a b : Bool} :
|
||||
(bif c0 then a else !(bif c1 then !a else b)) = (bif !c0 && !c1 then !b else a) := by
|
||||
cases c0 <;> cases c1 <;> simp
|
||||
|
||||
@[bv_normalize]
|
||||
theorem BitVec.ite_else_not_ite' (c0 c1 : Bool) {a b : BitVec w} :
|
||||
(bif c0 then a else ~~~(bif c1 then ~~~a else b)) = (bif !c0 && !c1 then ~~~b else a) := by
|
||||
cases c0 <;> cases c1 <;> simp
|
||||
|
||||
@[bv_normalize]
|
||||
theorem Bool.ite_then_ite'' (c0 c1 : Bool) {a b : α} :
|
||||
(bif c0 then (bif c1 then b else a) else a) = (bif c0 && c1 then b else a) := by
|
||||
cases c0 <;> cases c1 <;> simp
|
||||
|
||||
@[bv_normalize]
|
||||
theorem Bool.ite_then_not_ite'' (c0 c1 : Bool) {a b : Bool} :
|
||||
(bif c0 then !(bif c1 then b else !a) else a) = (bif c0 && c1 then !b else a) := by
|
||||
cases c0 <;> cases c1 <;> simp
|
||||
|
||||
@[bv_normalize]
|
||||
theorem BitVec.ite_then_not_ite'' (c0 c1 : Bool) {a b : BitVec w} :
|
||||
(bif c0 then ~~~(bif c1 then b else ~~~a) else a) = (bif c0 && c1 then ~~~b else a) := by
|
||||
cases c0 <;> cases c1 <;> simp
|
||||
|
||||
@[bv_normalize]
|
||||
theorem Bool.ite_else_ite'' (c0 c1 : Bool) {a b : α} :
|
||||
(bif c0 then a else (bif c1 then b else a)) = (bif !c0 && c1 then b else a) := by
|
||||
cases c0 <;> cases c1 <;> simp
|
||||
|
||||
@[bv_normalize]
|
||||
theorem Bool.ite_else_not_ite'' (c0 c1 : Bool) {a b : Bool} :
|
||||
(bif c0 then a else !(bif c1 then b else !a)) = (bif !c0 && c1 then !b else a) := by
|
||||
cases c0 <;> cases c1 <;> simp
|
||||
|
||||
@[bv_normalize]
|
||||
theorem BitVec.ite_else_not_ite'' (c0 c1 : Bool) {a b : BitVec w} :
|
||||
(bif c0 then a else ~~~(bif c1 then b else ~~~a )) = (bif !c0 && c1 then ~~~b else a) := by
|
||||
cases c0 <;> cases c1 <;> simp
|
||||
|
||||
theorem Bool.and_left (lhs rhs : Bool) (h : (lhs && rhs) = true) : lhs = true := by
|
||||
revert lhs rhs
|
||||
decide
|
||||
|
|
|
|||
|
|
@ -282,6 +282,155 @@ example (a : BitVec 16) : a * 8#16 = a <<< 3 := by
|
|||
example (a : BitVec 16) : a + a = a <<< 1 := by
|
||||
bv_normalize
|
||||
|
||||
-- NOT_EQUAL_BV1_BOOL
|
||||
example : ∀ (a : Bool), (!(a == true)) = (a == false) := by
|
||||
bv_normalize
|
||||
|
||||
example : ∀ (a : Bool), (!(a == false)) = (a == true) := by
|
||||
bv_normalize
|
||||
|
||||
example : ∀ (a : Bool), (!(true == a)) = (a == false) := by
|
||||
bv_normalize
|
||||
|
||||
example : ∀ (a : Bool), (!(false == a)) = (a == true) := by
|
||||
bv_normalize
|
||||
|
||||
example : ∀ (a : BitVec 1), (!(a == 1#1)) = (a == 0#1) := by
|
||||
bv_normalize
|
||||
|
||||
example : ∀ (a : BitVec 1), (!(a == 0#1)) = (a == 1#1) := by
|
||||
bv_normalize
|
||||
|
||||
example : ∀ (a : BitVec 1), (!(1#1 == a)) = (a == 0#1) := by
|
||||
bv_normalize
|
||||
|
||||
example : ∀ (a : BitVec 1), (!(0#1 == a)) = (a == 1#1) := by
|
||||
bv_normalize
|
||||
|
||||
-- ITE_SAME
|
||||
example : ∀ (c t e : Bool), ((bif c then t else e) == t) = (c || (t == e)) := by
|
||||
bv_normalize
|
||||
|
||||
example : ∀ (c t e : Bool), (t == (bif c then t else e)) = (c || (t == e)) := by
|
||||
bv_normalize
|
||||
|
||||
example : ∀ (c t e : Bool), ((bif c then t else e) == e) = (!c || (t == e)) := by
|
||||
bv_normalize
|
||||
|
||||
example : ∀ (c t e : Bool), (e == (bif c then t else e)) = (!c || (t == e)) := by
|
||||
bv_normalize
|
||||
|
||||
example : ∀ (c : Bool) (t e : BitVec 8), ((bif c then t else e) == t) = (c || (t == e)) := by
|
||||
bv_normalize
|
||||
|
||||
example : ∀ (c : Bool) (t e : BitVec 8), (t == (bif c then t else e)) = (c || (t == e)) := by
|
||||
bv_normalize
|
||||
|
||||
example : ∀ (c : Bool) (t e : BitVec 8), ((bif c then t else e) == e) = (!c || (t == e)) := by
|
||||
bv_normalize
|
||||
|
||||
example : ∀ (c : Bool) (t e : BitVec 8), (e == (bif c then t else e)) = (!c || (t == e)) := by
|
||||
bv_normalize
|
||||
|
||||
example (c : Bool) : ((if c then 1#1 else 0#1) == 1#1) ↔ c := by
|
||||
bv_normalize
|
||||
|
||||
-- ITE_THEN_ITE_1
|
||||
example (cond : Bool) {a b c d : Bool}
|
||||
(h : (bif cond then (bif cond then a else b) else c) = d) :
|
||||
(bif cond then a else c) = d := by
|
||||
bv_normalize
|
||||
|
||||
example (cond : Bool) {a b c d : Bool}
|
||||
(h : (bif cond then !(bif cond then a else b) else c) = d) :
|
||||
(bif cond then !a else c) = d := by
|
||||
bv_normalize
|
||||
|
||||
example (cond : Bool) {a b c d : BitVec 8}
|
||||
(h : (bif cond then ~~~(bif cond then a else b) else c) = d) :
|
||||
(bif cond then ~~~a else c) = d := by
|
||||
bv_normalize
|
||||
|
||||
-- ITE_ELSE_ITE_1
|
||||
example (cond : Bool) {a b c d : Bool}
|
||||
(h : (bif cond then a else (bif cond then b else c)) = d) :
|
||||
(bif cond then a else c) = d := by
|
||||
bv_normalize
|
||||
|
||||
example (cond : Bool) {a b c d : Bool}
|
||||
(h : (bif cond then a else !(bif cond then b else c)) = d) :
|
||||
(bif cond then a else !c) = d := by
|
||||
bv_normalize
|
||||
|
||||
example (cond : Bool) {a b c d : BitVec 8}
|
||||
(h : (bif cond then a else ~~~(bif cond then b else c)) = d) :
|
||||
(bif cond then a else ~~~c) = d := by
|
||||
bv_normalize
|
||||
|
||||
-- ITE_THEN_ITE_2
|
||||
example (c0 c1 : Bool) {a b d : Bool}
|
||||
(h : (bif c0 then (bif c1 then a else b) else a) = d) :
|
||||
(bif c0 && !c1 then b else a) = d := by
|
||||
bv_normalize
|
||||
|
||||
example (c0 c1 : Bool) {a b d : Bool}
|
||||
(h : (bif c0 then !(bif c1 then !a else b) else a) = d) :
|
||||
(bif c0 && !c1 then !b else a) = d := by
|
||||
bv_normalize
|
||||
|
||||
example (c0 c1 : Bool) {a b d : BitVec 8}
|
||||
(h : (bif c0 then ~~~(bif c1 then ~~~a else b) else a) = d) :
|
||||
(bif c0 && !c1 then ~~~b else a) = d := by
|
||||
bv_normalize
|
||||
|
||||
-- ITE_ELSE_ITE_2
|
||||
example (c0 c1 : Bool) {a b d : Bool}
|
||||
(h : (bif c0 then a else (bif c1 then a else b)) = d) :
|
||||
(bif !c0 && !c1 then b else a) = d := by
|
||||
bv_normalize
|
||||
|
||||
example (c0 c1 : Bool) {a b d : Bool}
|
||||
(h : (bif c0 then a else !(bif c1 then !a else b)) = d) :
|
||||
(bif !c0 && !c1 then !b else a) = d := by
|
||||
bv_normalize
|
||||
|
||||
example (c0 c1 : Bool) {a b d : BitVec 8}
|
||||
(h : (bif c0 then a else ~~~(bif c1 then ~~~a else b)) = d) :
|
||||
(bif !c0 && !c1 then ~~~b else a) = d := by
|
||||
bv_normalize
|
||||
|
||||
-- ITE_THEN_ITE_3
|
||||
example (c0 c1 : Bool) {a b d : Bool}
|
||||
(h : (bif c0 then (bif c1 then b else a) else a) = d) :
|
||||
(bif c0 && c1 then b else a) = d := by
|
||||
bv_normalize
|
||||
|
||||
example (c0 c1 : Bool) {a b d : Bool}
|
||||
(h : (bif c0 then !(bif c1 then b else !a) else a) = d) :
|
||||
(bif c0 && c1 then !b else a) = d := by
|
||||
bv_normalize
|
||||
|
||||
example (c0 c1 : Bool) {a b d : BitVec 8}
|
||||
(h : (bif c0 then ~~~(bif c1 then b else ~~~a) else a) = d) :
|
||||
(bif c0 && c1 then ~~~b else a) = d := by
|
||||
bv_normalize
|
||||
|
||||
-- ITE_ELSE_ITE_3
|
||||
example (c0 c1 : Bool) {a b d : Bool}
|
||||
(h : (bif c0 then a else (bif c1 then b else a)) = d) :
|
||||
(bif !c0 && c1 then b else a) = d := by
|
||||
bv_normalize
|
||||
|
||||
example (c0 c1 : Bool) {a b d : Bool}
|
||||
(h : (bif c0 then a else !(bif c1 then b else !a)) = d) :
|
||||
(bif !c0 && c1 then !b else a) = d := by
|
||||
bv_normalize
|
||||
|
||||
example (c0 c1 : Bool) {a b d : BitVec 8}
|
||||
(h : (bif c0 then a else ~~~(bif c1 then b else ~~~a)) = d) :
|
||||
(bif !c0 && c1 then ~~~b else a) = d := by
|
||||
bv_normalize
|
||||
|
||||
section
|
||||
|
||||
example (x y : BitVec 256) : x * y = y * x := by
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue