style: format and split up AIG

LeanSAT/AIG/Basic.lean

@@ -91,7 +91,8 @@ structure CacheHit (decls : Array (Decl α)) (decl : Decl α) where
   hvalid : decls[idx]'hbound = decl
 
 /--
-All indices, found in a `Cache` that is valid with respect to some `decls`, are within bounds of `decls`.
+All indices, found in a `Cache` that is valid with respect to some `decls`, are within bounds of
+`decls`.
 -/
 theorem Cache.get?_bounds {decls : Array (Decl α)} {idx : Nat} (c : Cache α decls) (decl : Decl α)
     (hfound : c.val[decl]? = some idx) : idx < decls.size := by

LeanSAT/AIG/CachedGates.lean

@@ -39,7 +39,8 @@ def mkNotCached (aig : AIG α) (gate : Ref aig) : Entrypoint α :=
     }
 
 @[inline]
-def BinaryInput.asGateInput {aig : AIG α} (input : BinaryInput aig) (linv rinv : Bool) : GateInput aig :=
+def BinaryInput.asGateInput {aig : AIG α} (input : BinaryInput aig) (linv rinv : Bool)
+    : GateInput aig :=
   {
     lhs := {
       ref := input.lhs
@@ -117,7 +118,8 @@ def mkXorCached (aig : AIG α) (input : BinaryInput aig) : Entrypoint α :=
     }
 
 /--
-Create an equality gate in the input AIG. This uses the builtin cache to enable automated subterm sharing
+Create an equality gate in the input AIG. This uses the builtin cache to enable automated subterm
+sharing
 -/
 def mkBEqCached (aig : AIG α) (input : BinaryInput aig) : Entrypoint α :=
   -- a == b = (invert (a && (invert b))) && (invert ((invert a) && b))
@@ -149,7 +151,8 @@ def mkBEqCached (aig : AIG α) (input : BinaryInput aig) : Entrypoint α :=
     }
 
 /--
-Create an implication gate in the input AIG. This uses the builtin cache to enable automated subterm sharing
+Create an implication gate in the input AIG. This uses the builtin cache to enable automated subterm
+sharing.
 -/
 def mkImpCached (aig : AIG α) (input : BinaryInput aig) : Entrypoint α :=
   -- a -> b = true && (invert (a and (invert b)))

LeanSAT/AIG/CachedGatesLemmas.lean

@@ -15,27 +15,32 @@ semantics of the gate functions in different scenarios.
 /--
 Encoding not as boolen expression in AIG form.
 -/
-theorem not_as_aig (b : Bool) : (true && !b) = !b := by cases b <;> decide
+theorem not_as_aig (b : Bool) : (true && !b) = !b := by
+  cases b <;> decide
 
 /--
 Encoding or as boolen expression in AIG form.
 -/
-theorem or_as_aig (a b : Bool) : (!(!a && !b)) = (a || b) := by cases a <;> cases b <;> decide
+theorem or_as_aig (a b : Bool) : (!(!a && !b)) = (a || b) := by
+  cases a <;> cases b <;> decide
 
 /--
 Encoding XOR as boolen expression in AIG form.
 -/
-theorem xor_as_aig (a b : Bool) : (!(a && b) && !(!a && !b)) = (xor a b) := by cases a <;> cases b <;> decide
+theorem xor_as_aig (a b : Bool) : (!(a && b) && !(!a && !b)) = (xor a b) := by
+  cases a <;> cases b <;> decide
 
 /--
 Encoding BEq as boolen expression in AIG form.
 -/
-theorem beq_as_aig (a b : Bool) : (!(a && !b) && !(!a && b)) = (a == b) := by cases a <;> cases b <;> decide
+theorem beq_as_aig (a b : Bool) : (!(a && !b) && !(!a && b)) = (a == b) := by
+  cases a <;> cases b <;> decide
 
 /--
 Encoding implication as boolen expression in AIG form.
 -/
-theorem imp_as_aig (a b : Bool) : (!(a && !b)) = (!a || b) := by cases a <;> cases b <;> decide
+theorem imp_as_aig (a b : Bool) : (!(a && !b)) = (!a || b) := by
+  cases a <;> cases b <;> decide
 
 namespace AIG
 

LeanSAT/AIG/CachedLemmas.lean

@@ -44,10 +44,12 @@ theorem mkAtomCached_miss_aig (aig : AIG α) (hcache : aig.cache.get? (.atom var
   split <;> simp_all
 
 /--
-The AIG produced by `AIG.mkAtomCached` agrees with the input AIG on all indices that are valid for both.
+The AIG produced by `AIG.mkAtomCached` agrees with the input AIG on all indices that are valid for
+both.
 -/
-theorem mkAtomCached_decl_eq (aig : AIG α) (var : α) (idx : Nat) {h : idx < aig.decls.size} {hbound} :
-    (aig.mkAtomCached var).aig.decls[idx]'hbound = aig.decls[idx] := by
+theorem mkAtomCached_decl_eq (aig : AIG α) (var : α) (idx : Nat) {h : idx < aig.decls.size}
+    {hbound}
+    : (aig.mkAtomCached var).aig.decls[idx]'hbound = aig.decls[idx] := by
   match hcache:aig.cache.get? (.atom var) with
   | some gate =>
     have := mkAtomCached_hit_aig aig hcache
@@ -86,7 +88,8 @@ theorem mkAtomCached_eval_eq_mkAtom_eval {aig : AIG α}
   . simp [mkAtom, denote]
 
 /--
-If we find a cached const declaration in the AIG, denoting it is equivalent to denoting `AIG.mkConst`.
+If we find a cached const declaration in the AIG, denoting it is equivalent to denoting
+`AIG.mkConst`.
 -/
 theorem denote_mkConst_cached {aig : AIG α} {hit} :
     aig.cache.get? (.const b) = some hit
@@ -100,8 +103,8 @@ theorem denote_mkConst_cached {aig : AIG α} {hit} :
 /--
 `mkConstCached` does not modify the input AIG upon a cache hit.
 -/
-theorem mkConstCached_hit_aig (aig : AIG α) {hit} (hcache : aig.cache.get? (.const val) = some hit) :
-    (aig.mkConstCached val).aig = aig := by
+theorem mkConstCached_hit_aig (aig : AIG α) {hit} (hcache : aig.cache.get? (.const val) = some hit)
+    : (aig.mkConstCached val).aig = aig := by
   simp only [mkConstCached]
   split <;> simp_all
 
@@ -116,8 +119,9 @@ theorem mkConstCached_miss_aig (aig : AIG α) (hcache : aig.cache.get? (.const v
 /--
 The AIG produced by `AIG.mkConstCached` agrees with the input AIG on all indices that are valid for both.
 -/
-theorem mkConstCached_decl_eq (aig : AIG α) (val : Bool) (idx : Nat) {h : idx < aig.decls.size} {hbound} :
-    (aig.mkConstCached val).aig.decls[idx]'hbound = aig.decls[idx] := by
+theorem mkConstCached_decl_eq (aig : AIG α) (val : Bool) (idx : Nat) {h : idx < aig.decls.size}
+    {hbound}
+    : (aig.mkConstCached val).aig.decls[idx]'hbound = aig.decls[idx] := by
   match hcache:aig.cache.get? (.const val) with
   | some gate =>
     have := mkConstCached_hit_aig aig hcache
@@ -253,7 +257,8 @@ theorem mkGateCached.go_decl_eq (aig : AIG α) (input : GateInput aig) :
             simp [h2]
 
 /--
-The AIG produced by `AIG.mkGateCached` agrees with the input AIG on all indices that are valid for both.
+The AIG produced by `AIG.mkGateCached` agrees with the input AIG on all indices that are valid for
+both.
 -/
 theorem mkGateCached_decl_eq (aig : AIG α) (input : GateInput aig) :
     ∀ (idx : Nat) (h1) (h2),

LeanSAT/AIG/If.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Henrik Böving
 -/
 import LeanSAT.AIG.CachedGatesLemmas
-import LeanSAT.AIG.RefStreamOperator
+import LeanSAT.AIG.LawfulStreamOperator
 
 namespace AIG
 
@@ -48,14 +48,14 @@ instance : LawfulOperator α TernaryInput mkIfCached where
     rw [LawfulOperator.decl_eq (f := mkNotCached)]
     rw [LawfulOperator.decl_eq (f := mkAndCached)]
     . apply LawfulOperator.lt_size_of_lt_aig_size (f := mkAndCached)
-      assumption
+      omega
     . apply LawfulOperator.lt_size_of_lt_aig_size (f := mkNotCached)
       apply LawfulOperator.lt_size_of_lt_aig_size (f := mkAndCached)
-      assumption
+      omega
     . apply LawfulOperator.lt_size_of_lt_aig_size (f := mkAndCached)
       apply LawfulOperator.lt_size_of_lt_aig_size (f := mkNotCached)
       apply LawfulOperator.lt_size_of_lt_aig_size (f := mkAndCached)
-      assumption
+      omega
 
 theorem if_as_bool (d l r : Bool) : (if d then l else r) = ((d && l) || (!d && r))  := by
   revert d l r
@@ -91,8 +91,8 @@ def ite (aig : AIG α) (input : IfInput aig w) : RefStreamEntry α w :=
   let ⟨discr, lhs, rhs⟩ := input
   go aig 0 (by omega) discr lhs rhs .empty
 where
-  go {w : Nat} (aig : AIG α) (curr : Nat) (hcurr : curr ≤ w) (discr : Ref aig) (lhs rhs : RefStream aig w)
-      (s : RefStream aig curr) : RefStreamEntry α w :=
+  go {w : Nat} (aig : AIG α) (curr : Nat) (hcurr : curr ≤ w) (discr : Ref aig)
+      (lhs rhs : RefStream aig w) (s : RefStream aig curr) : RefStreamEntry α w :=
     if hcurr:curr < w then
       let input := ⟨discr, lhs.getRef curr hcurr, rhs.getRef curr hcurr⟩
       let res := mkIfCached aig input
@@ -109,6 +109,7 @@ where
     else
       have : curr = w := by omega
       ⟨aig, this ▸ s⟩
+termination_by w - curr
 
 namespace ite
 
@@ -190,8 +191,8 @@ theorem go_getRef {w : Nat} (aig : AIG α) (curr : Nat) (hcurr : curr ≤ w) (di
   intro idx hidx
   apply go_getRef_aux
 
-theorem go_denote_mem_prefix {w : Nat} (aig : AIG α) (curr : Nat) (hcurr : curr ≤ w) (discr : Ref aig)
-      (lhs rhs : RefStream aig w) (s : RefStream aig curr) (start : Nat) (hstart)
+theorem go_denote_mem_prefix {w : Nat} (aig : AIG α) (curr : Nat) (hcurr : curr ≤ w)
+      (discr : Ref aig) (lhs rhs : RefStream aig w) (s : RefStream aig curr) (start : Nat) (hstart)
   : ⟦
       (go aig curr hcurr discr lhs rhs s).aig,
       ⟨start, by apply Nat.lt_of_lt_of_le; exact hstart; apply go_le_size⟩,

LeanSAT/AIG/LawfulOperator.lean

@@ -63,7 +63,8 @@ theorem denote.go_eq_of_aig_eq (decls1 decls2 : Array (Decl α)) (start : Nat) {
 termination_by sizeOf start
 
 @[inherit_doc denote.go_eq_of_aig_eq ]
-theorem denote.eq_of_aig_eq (entry : Entrypoint α) (newAIG : AIG α) (hprefix : IsPrefix entry.aig.decls newAIG.decls) :
+theorem denote.eq_of_aig_eq (entry : Entrypoint α) (newAIG : AIG α)
+      (hprefix : IsPrefix entry.aig.decls newAIG.decls) :
     ⟦newAIG, ⟨entry.ref.gate, (by have := entry.ref.hgate; have := hprefix.size_le; omega)⟩, assign⟧
       =
     ⟦entry, assign⟧

LeanSAT/AIG/Lemmas.lean

@@ -124,7 +124,8 @@ theorem denote_mkGate {aig : AIG α} {input : GateInput aig} :
 /--
 `AIG.mkAtom` never shrinks the underlying AIG.
 -/
-theorem mkAtom_le_size (aig : AIG α) (var : α) : aig.decls.size ≤ (aig.mkAtom var).aig.decls.size := by
+theorem mkAtom_le_size (aig : AIG α) (var : α)
+    : aig.decls.size ≤ (aig.mkAtom var).aig.decls.size := by
   simp_arith [mkAtom]
 
 /--

LeanSAT/AIG/RefStream.lean

@@ -70,12 +70,14 @@ theorem getRef_push_ref_eq (s : RefStream aig len) (ref : AIG.Ref aig)
   simp [getRef, pushRef, ← this]
 
 -- This variant exists because it is sometimes hard to rewrite properly with DTT
-theorem getRef_push_ref_eq' (s : RefStream aig len) (ref : AIG.Ref aig) (idx : Nat) (hidx : idx = len)
+theorem getRef_push_ref_eq' (s : RefStream aig len) (ref : AIG.Ref aig) (idx : Nat)
+    (hidx : idx = len)
     : (s.pushRef ref).getRef idx (by omega) = ref := by
   have := s.hlen
   simp [getRef, pushRef, ← this, hidx]
 
-theorem getRef_push_ref_lt (s : RefStream aig len) (ref : AIG.Ref aig) (idx : Nat) (hidx : idx < len)
+theorem getRef_push_ref_lt (s : RefStream aig len) (ref : AIG.Ref aig) (idx : Nat)
+    (hidx : idx < len)
     : (s.pushRef ref).getRef idx (by omega) = s.getRef idx hidx := by
   simp [getRef, pushRef]
   cases ref
@@ -108,7 +110,8 @@ def append (lhs : RefStream aig lw) (rhs : RefStream aig rw) : RefStream aig (lw
         . omega
   ⟩
 
-theorem getRef_append (lhs : RefStream aig lw) (rhs : RefStream aig rw) (idx : Nat) (hidx : idx < lw + rw)
+theorem getRef_append (lhs : RefStream aig lw) (rhs : RefStream aig rw) (idx : Nat)
+      (hidx : idx < lw + rw)
     : (lhs.append rhs).getRef idx hidx
         =
       if h:idx < lw then
@@ -160,16 +163,16 @@ def cast {aig1 aig2 : AIG α} (s : BinaryRefStream aig1 len)
   ⟨lhs.cast h, rhs.cast h⟩
 
 @[simp]
-theorem lhs_getRef_cast {aig1 aig2 : AIG α} (s : BinaryRefStream aig1 len) (idx : Nat) (hidx : idx < len)
-      (hcast : aig1.decls.size ≤ aig2.decls.size)
+theorem lhs_getRef_cast {aig1 aig2 : AIG α} (s : BinaryRefStream aig1 len) (idx : Nat)
+      (hidx : idx < len) (hcast : aig1.decls.size ≤ aig2.decls.size)
     : (s.cast hcast).lhs.getRef idx hidx
         =
       (s.lhs.getRef idx hidx).cast hcast := by
   simp [cast]
 
 @[simp]
-theorem rhs_getRef_cast {aig1 aig2 : AIG α} (s : BinaryRefStream aig1 len) (idx : Nat) (hidx : idx < len)
-      (hcast : aig1.decls.size ≤ aig2.decls.size)
+theorem rhs_getRef_cast {aig1 aig2 : AIG α} (s : BinaryRefStream aig1 len) (idx : Nat)
+      (hidx : idx < len) (hcast : aig1.decls.size ≤ aig2.decls.size)
     : (s.cast hcast).rhs.getRef idx hidx
         =
       (s.rhs.getRef idx hidx).cast hcast := by