Skip to content

Commit

Permalink
chore: delete unused code (#5493)
Browse files Browse the repository at this point in the history
  • Loading branch information
@hargoniX
hargoniX authored Sep 27, 2024
1 parent f22998e commit 2221296
Show file tree
Hide file tree
Showing 6 changed files with 18 additions and 49 deletions.
2 changes: 0 additions & 2 deletions src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/Reflect.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -75,9 +75,7 @@ instance : ToExpr Gate where
toExpr x :=
match x with
| .and => mkConst ``Gate.and
| .or => mkConst ``Gate.or
| .xor => mkConst ``Gate.xor
| .imp => mkConst ``Gate.imp
| .beq => mkConst ``Gate.beq
toTypeExpr := mkConst ``Gate

Expand Down
1 change: 0 additions & 1 deletion src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/ReifiedBVLogical.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -65,7 +65,6 @@ partial def of (t : Expr) : M (Option ReifiedBVLogical) := do
let subProof ← sub.evalsAtAtoms
return mkApp3 (mkConst ``Std.Tactic.BVDecide.Reflect.Bool.not_congr) subExpr subEvalExpr subProof
return some ⟨boolExpr, proof, expr⟩
| Bool.or lhsExpr rhsExpr => gateReflection lhsExpr rhsExpr .or ``Std.Tactic.BVDecide.Reflect.Bool.or_congr
| Bool.and lhsExpr rhsExpr => gateReflection lhsExpr rhsExpr .and ``Std.Tactic.BVDecide.Reflect.Bool.and_congr
| Bool.xor lhsExpr rhsExpr => gateReflection lhsExpr rhsExpr .xor ``Std.Tactic.BVDecide.Reflect.Bool.xor_congr
| BEq.beq α _ lhsExpr rhsExpr =>
Expand Down
6 changes: 0 additions & 6 deletions src/Std/Tactic/BVDecide/Bitblast/BoolExpr/Basic.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -16,26 +16,20 @@ namespace Std.Tactic.BVDecide

inductive Gate
| and
| or
| xor
| beq
| imp

namespace Gate

def toString : Gate → String
| and => "&&"
| or => "||"
| xor => "^^"
| beq => "=="
| imp => "→"

def eval : Gate → Bool → Bool → Bool
| and => (· && ·)
| or => (· || ·)
| xor => (· ^^ ·)
| beq => (· == ·)
| imp => (!· || ·)

end Gate

Expand Down
15 changes: 0 additions & 15 deletions src/Std/Tactic/BVDecide/Bitblast/BoolExpr/Circuit.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -51,10 +51,6 @@ where
let ret := aig.mkAndCached input
have := LawfulOperator.le_size (f := mkAndCached) aig input
⟨ret, by dsimp only [ret] at lextend rextend ⊢; omega⟩
| .or =>
let ret := aig.mkOrCached input
have := LawfulOperator.le_size (f := mkOrCached) aig input
⟨ret, by dsimp only [ret] at lextend rextend ⊢; omega⟩
| .xor =>
let ret := aig.mkXorCached input
have := LawfulOperator.le_size (f := mkXorCached) aig input
Expand All @@ -63,11 +59,6 @@ where
let ret := aig.mkBEqCached input
have := LawfulOperator.le_size (f := mkBEqCached) aig input
⟨ret, by dsimp only [ret] at lextend rextend ⊢; omega⟩
| .imp =>
let ret := aig.mkImpCached input
have := LawfulOperator.le_size (f := mkImpCached) aig input
⟨ret, by dsimp only [ret] at lextend rextend ⊢; omega⟩


variable (atomHandler : AIG β → α → Entrypoint β) [LawfulOperator β (fun _ => α) atomHandler]

Expand Down Expand Up @@ -99,18 +90,12 @@ theorem ofBoolExprCached.go_decl_eq (idx) (aig : AIG β) (h : idx < aig.decls.si
| and =>
simp only [go]
rw [AIG.LawfulOperator.decl_eq (f := mkAndCached), rih, lih]
| or =>
simp only [go]
rw [AIG.LawfulOperator.decl_eq (f := mkOrCached), rih, lih]
| xor =>
simp only [go]
rw [AIG.LawfulOperator.decl_eq (f := mkXorCached), rih, lih]
| beq =>
simp only [go]
rw [AIG.LawfulOperator.decl_eq (f := mkBEqCached), rih, lih]
| imp =>
simp only [go]
rw [AIG.LawfulOperator.decl_eq (f := mkImpCached), rih, lih]

theorem ofBoolExprCached.go_isPrefix_aig {aig : AIG β} :
IsPrefix aig.decls (go aig expr atomHandler).val.aig.decls := by
Expand Down
4 changes: 0 additions & 4 deletions src/Std/Tactic/BVDecide/Reflect.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -121,10 +121,6 @@ theorem and_congr (lhs rhs lhs' rhs' : Bool) (h1 : lhs' = lhs) (h2 : rhs' = rhs)
(lhs' && rhs') = (lhs && rhs) := by
simp[*]

theorem or_congr (lhs rhs lhs' rhs' : Bool) (h1 : lhs' = lhs) (h2 : rhs' = rhs) :
(lhs' || rhs') = (lhs || rhs) := by
simp[*]

theorem xor_congr (lhs rhs lhs' rhs' : Bool) (h1 : lhs' = lhs) (h2 : rhs' = rhs) :
(lhs' ^^ rhs') = (lhs ^^ rhs) := by
simp[*]
Expand Down
39 changes: 18 additions & 21 deletions tests/lean/run/aig_shared.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -8,44 +8,41 @@ def mkSharedTree (n : Nat) : BoolExpr Nat :=
| 0 => .literal 0
| n + 1 =>
let tree := mkSharedTree n
.gate .or tree tree
.gate .xor tree tree

/--
info: #[Std.Sat.AIG.Decl.atom 0, Std.Sat.AIG.Decl.gate 0 0 true true, Std.Sat.AIG.Decl.const true,
Std.Sat.AIG.Decl.gate 1 2 true false]
info: #[Std.Sat.AIG.Decl.atom 0, Std.Sat.AIG.Decl.gate 0 0 true true, Std.Sat.AIG.Decl.gate 0 1 true true]
-/
#guard_msgs in
#eval ofBoolExprCached (mkSharedTree 1) AIG.mkAtomCached |>.aig.decls

/--
info: #[Std.Sat.AIG.Decl.atom 0, Std.Sat.AIG.Decl.gate 0 0 true true, Std.Sat.AIG.Decl.const true,
Std.Sat.AIG.Decl.gate 1 2 true false, Std.Sat.AIG.Decl.gate 3 3 true true, Std.Sat.AIG.Decl.gate 2 4 false true]
info: #[Std.Sat.AIG.Decl.atom 0, Std.Sat.AIG.Decl.gate 0 0 true true, Std.Sat.AIG.Decl.gate 0 1 true true,
Std.Sat.AIG.Decl.gate 2 2 true true, Std.Sat.AIG.Decl.gate 2 3 true true]
-/
#guard_msgs in
#eval ofBoolExprCached (mkSharedTree 2) AIG.mkAtomCached |>.aig.decls

/--
info: #[Std.Sat.AIG.Decl.atom 0, Std.Sat.AIG.Decl.gate 0 0 true true, Std.Sat.AIG.Decl.const true,
Std.Sat.AIG.Decl.gate 1 2 true false, Std.Sat.AIG.Decl.gate 3 3 true true, Std.Sat.AIG.Decl.gate 2 4 false true,
Std.Sat.AIG.Decl.gate 5 5 true true, Std.Sat.AIG.Decl.gate 2 6 false true, Std.Sat.AIG.Decl.gate 7 7 true true,
Std.Sat.AIG.Decl.gate 2 8 false true]
info: #[Std.Sat.AIG.Decl.atom 0, Std.Sat.AIG.Decl.gate 0 0 true true, Std.Sat.AIG.Decl.gate 0 1 true true,
Std.Sat.AIG.Decl.gate 2 2 true true, Std.Sat.AIG.Decl.gate 2 3 true true, Std.Sat.AIG.Decl.gate 4 4 true true,
Std.Sat.AIG.Decl.gate 4 5 true true, Std.Sat.AIG.Decl.gate 6 6 true true, Std.Sat.AIG.Decl.gate 6 7 true true]
-/
#guard_msgs in
#eval ofBoolExprCached (mkSharedTree 4) AIG.mkAtomCached |>.aig.decls

/--
info: #[Std.Sat.AIG.Decl.atom 0, Std.Sat.AIG.Decl.gate 0 0 true true, Std.Sat.AIG.Decl.const true,
Std.Sat.AIG.Decl.gate 1 2 true false, Std.Sat.AIG.Decl.gate 3 3 true true, Std.Sat.AIG.Decl.gate 2 4 false true,
Std.Sat.AIG.Decl.gate 5 5 true true, Std.Sat.AIG.Decl.gate 2 6 false true, Std.Sat.AIG.Decl.gate 7 7 true true,
Std.Sat.AIG.Decl.gate 2 8 false true, Std.Sat.AIG.Decl.gate 9 9 true true, Std.Sat.AIG.Decl.gate 2 10 false true,
Std.Sat.AIG.Decl.gate 11 11 true true, Std.Sat.AIG.Decl.gate 2 12 false true, Std.Sat.AIG.Decl.gate 13 13 true true,
Std.Sat.AIG.Decl.gate 2 14 false true, Std.Sat.AIG.Decl.gate 15 15 true true, Std.Sat.AIG.Decl.gate 2 16 false true,
Std.Sat.AIG.Decl.gate 17 17 true true, Std.Sat.AIG.Decl.gate 2 18 false true, Std.Sat.AIG.Decl.gate 19 19 true true,
Std.Sat.AIG.Decl.gate 2 20 false true, Std.Sat.AIG.Decl.gate 21 21 true true, Std.Sat.AIG.Decl.gate 2 22 false true,
Std.Sat.AIG.Decl.gate 23 23 true true, Std.Sat.AIG.Decl.gate 2 24 false true, Std.Sat.AIG.Decl.gate 25 25 true true,
Std.Sat.AIG.Decl.gate 2 26 false true, Std.Sat.AIG.Decl.gate 27 27 true true, Std.Sat.AIG.Decl.gate 2 28 false true,
Std.Sat.AIG.Decl.gate 29 29 true true, Std.Sat.AIG.Decl.gate 2 30 false true, Std.Sat.AIG.Decl.gate 31 31 true true,
Std.Sat.AIG.Decl.gate 2 32 false true]
info: #[Std.Sat.AIG.Decl.atom 0, Std.Sat.AIG.Decl.gate 0 0 true true, Std.Sat.AIG.Decl.gate 0 1 true true,
Std.Sat.AIG.Decl.gate 2 2 true true, Std.Sat.AIG.Decl.gate 2 3 true true, Std.Sat.AIG.Decl.gate 4 4 true true,
Std.Sat.AIG.Decl.gate 4 5 true true, Std.Sat.AIG.Decl.gate 6 6 true true, Std.Sat.AIG.Decl.gate 6 7 true true,
Std.Sat.AIG.Decl.gate 8 8 true true, Std.Sat.AIG.Decl.gate 8 9 true true, Std.Sat.AIG.Decl.gate 10 10 true true,
Std.Sat.AIG.Decl.gate 10 11 true true, Std.Sat.AIG.Decl.gate 12 12 true true, Std.Sat.AIG.Decl.gate 12 13 true true,
Std.Sat.AIG.Decl.gate 14 14 true true, Std.Sat.AIG.Decl.gate 14 15 true true, Std.Sat.AIG.Decl.gate 16 16 true true,
Std.Sat.AIG.Decl.gate 16 17 true true, Std.Sat.AIG.Decl.gate 18 18 true true, Std.Sat.AIG.Decl.gate 18 19 true true,
Std.Sat.AIG.Decl.gate 20 20 true true, Std.Sat.AIG.Decl.gate 20 21 true true, Std.Sat.AIG.Decl.gate 22 22 true true,
Std.Sat.AIG.Decl.gate 22 23 true true, Std.Sat.AIG.Decl.gate 24 24 true true, Std.Sat.AIG.Decl.gate 24 25 true true,
Std.Sat.AIG.Decl.gate 26 26 true true, Std.Sat.AIG.Decl.gate 26 27 true true, Std.Sat.AIG.Decl.gate 28 28 true true,
Std.Sat.AIG.Decl.gate 28 29 true true, Std.Sat.AIG.Decl.gate 30 30 true true, Std.Sat.AIG.Decl.gate 30 31 true true]
-/
#guard_msgs in
#eval ofBoolExprCached (mkSharedTree 16) AIG.mkAtomCached |>.aig.decls

0 comments on commit 2221296

Please sign in to comment.