chore: delete unused code (#5493)
This commit is contained in:
Henrik Böving
GitHub
parent
f22998edfe
commit
2221296d3c
6 changed files with 18 additions and 49 deletions
|
|
@ -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
|
||||
|
||||
|
|
|
|||
|
|
@ -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 =>
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
@ -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]
|
||||
|
||||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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[*]
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue