refactor: remove AIG optimizations

LeanSAT/AIG/Cached.lean

@@ -74,40 +74,29 @@ def mkGateCached (aig : AIG α) (input : GateInput aig) : Entrypoint α :=
   let rhs := input.rhs.ref.gate
   let linv := input.lhs.inv
   let rinv := input.rhs.inv
-  have := input.lhs.ref.hgate
-  have := input.rhs.ref.hgate
+  have lhgate := input.lhs.ref.hgate
+  have rhgate := input.rhs.ref.hgate
   let decl := .gate lhs rhs linv rinv
   match cache.find? decl with
   | some hit =>
     ⟨⟨decls, cache, inv⟩, ⟨hit.idx, hit.hbound⟩⟩
   | none =>
     /-
-    Here we implement the constant propagating subset of:
+    We looked into implementing AIG optimization according to:
     https://fmv.jku.at/papers/BrummayerBiere-MEMICS06.pdf
-    TODO: rest of the table
+    However the constant folding subset of this seemed to *decrease* SAT solver performance noticeably.
+    We thus decided to just do the naive approach.
     -/
-    match decls[lhs], decls[rhs], linv, rinv with
-    -- Boundedness
-    | .const true, _, true, _ | .const false, _, false, _
-    | _, .const true, _, true | _, .const false, _, false =>
-      mkConstCached ⟨decls, cache, inv⟩ false
-    -- Left Neutrality
-    | .const true, _, false, false | .const false, _, true, false =>
-      ⟨⟨decls, cache, inv⟩, rhs, (by assumption)⟩
-    -- Right Neutrality
-    | _, .const true, false, false | _, .const false, false, true =>
-      ⟨⟨decls, cache, inv⟩, lhs, (by assumption)⟩
-    | _, _, _, _ =>
-      let g := decls.size
-      let cache := cache.insert decls decl
-      let decls := decls.push decl
-      have inv := by
-        intro lhs rhs linv rinv i h1 h2
-        simp only [decls] at *
-        simp only [Array.get_push] at h2
-        split at h2
-        . apply inv <;> assumption
-        . injections; omega
-      ⟨⟨decls, cache, inv⟩, ⟨g, by simp [g, decls]⟩⟩
+    let g := decls.size
+    let cache := cache.insert decls decl
+    let decls := decls.push decl
+    have inv := by
+      intro lhs rhs linv rinv i h1 h2
+      simp only [decls] at *
+      simp only [Array.get_push] at h2
+      split at h2
+      . apply inv <;> assumption
+      . injections; omega
+    ⟨⟨decls, cache, inv⟩, ⟨g, by simp [g, decls]⟩⟩
 
 end AIG

LeanSAT/AIG/CachedLemmas.lean

@@ -183,7 +183,7 @@ theorem mkGateCached_le_size (aig : AIG α) (input : GateInput aig)
   dsimp [mkGateCached]
   split
   . simp
-  . split <;> simp_arith [mkConstCached_le_size]
+  . simp_arith
 
 /--
 The AIG produced by `AIG.mkGateCached` agrees with the input AIG on all indices that are valid for both.
@@ -198,36 +198,11 @@ theorem mkGateCached_decl_eq (aig : AIG α) (input : GateInput aig) :
     . rw [← hres]
       intros
       simp
-    . split at hres
-      . rw [← hres]
-        intros
-        rw [LawfulOperator.decl_eq (f := AIG.mkConstCached)]
-      . rw [← hres]
-        intros
-        rw [LawfulOperator.decl_eq (f := AIG.mkConstCached)]
-      . rw [← hres]
-        intros
-        rw [LawfulOperator.decl_eq (f := AIG.mkConstCached)]
-      . rw [← hres]
-        intros
-        rw [LawfulOperator.decl_eq (f := AIG.mkConstCached)]
-      . rw [← hres]
-        intros
-        simp
-      . rw [← hres]
-        intros
-        simp
-      . rw [← hres]
-        intros
-        simp
-      . rw [← hres]
-        intros
-        simp
-      . rw [← hres]
-        dsimp
-        intro idx h1 h2
-        rw [Array.get_push]
-        simp [h2]
+    . rw [← hres]
+      dsimp
+      intro idx h1 h2
+      rw [Array.get_push]
+      simp [h2]
 
 instance : LawfulOperator α GateInput mkGateCached where
   le_size := mkGateCached_le_size
@@ -243,25 +218,8 @@ theorem mkGateCached_eval_eq_mkGate_eval {aig : AIG α} {input : GateInput aig}
     ⟦aig.mkGateCached input, assign⟧ = ⟦aig.mkGate input, assign⟧ := by
   simp only [mkGateCached]
   split
-  . next heq1 =>
-    rw [denote_mkGate_cached heq1]
-  . split
-    . next heq _ =>
-      simp_all [denote_idx_const heq]
-    . next heq _ =>
-      simp_all [denote_idx_const heq]
-    . next heq _ _ _ =>
-      simp_all [denote_idx_const heq]
-    . next heq _ _ _ =>
-      simp_all [denote_idx_const heq]
-    . next heq _ _ _ =>
-      simp_all [denote_idx_const heq]
-    . next heq _ _ _ =>
-      simp_all [denote_idx_const heq]
-    . next heq _ _ _ _ =>
-      simp_all [denote_idx_const heq]
-    . next heq _ _ _ =>
-      simp_all [denote_idx_const heq]
-    . simp [mkGate, denote]
+  . rw [denote_mkGate_cached]
+    assumption
+  . simp [mkGate, denote]
 
 end AIG

Test/AIG.lean

@@ -1,3 +1,2 @@
-import Test.AIG.Opt
 import Test.AIG.Shared
 import Test.AIG.Stress

Test/Sat.lean-test-7-47.lrat

@@ -1,12 +1,27 @@
-18 4 0 1 2 0
-18 d 2 0
-19 6 0 1 3 0
-19 d 3 4 0
-20 -3 0 19 5 0
-20 d 5 0
-21 -5 0 19 6 0
-21 d 6 7 8 9 0
-22 -1 2 0 21 10 0
-22 d 10 0
-23 2 0 11 22 0
-24 0 18 23 12 0
+33 7 0 1 2 0
+33 d 2 0
+34 11 0 1 3 0
+34 d 3 4 0
+35 -9 0 34 5 0
+35 d 5 0
+36 -10 0 34 6 0
+36 d 6 7 8 9 0
+37 3 -8 0 36 10 0
+37 d 10 11 12 0
+38 -3 8 0 35 13 0
+38 d 13 0
+39 1 0 33 17 0
+39 d 17 0
+40 6 0 33 18 0
+40 d 18 19 0
+41 -4 0 40 20 0
+41 d 20 0
+42 -5 0 40 21 0
+42 d 21 22 23 24 0
+43 2 -3 0 42 25 0
+43 d 25 26 27 0
+44 -2 3 0 41 28 0
+44 d 28 0
+45 -8 0 29 37 0
+46 -2 0 29 44 0
+47 0 45 46 39 16 0

Test/sat_check.lrat

@@ -1,12 +1,27 @@
-18 4 0 1 2 0
-18 d 2 0
-19 6 0 1 3 0
-19 d 3 4 0
-20 -3 0 19 5 0
-20 d 5 0
-21 -5 0 19 6 0
-21 d 6 7 8 9 0
-22 -1 2 0 21 10 0
-22 d 10 0
-23 2 0 11 22 0
-24 0 18 23 12 0
+33 7 0 1 2 0
+33 d 2 0
+34 11 0 1 3 0
+34 d 3 4 0
+35 -9 0 34 5 0
+35 d 5 0
+36 -10 0 34 6 0
+36 d 6 7 8 9 0
+37 3 -8 0 36 10 0
+37 d 10 11 12 0
+38 -3 8 0 35 13 0
+38 d 13 0
+39 1 0 33 17 0
+39 d 17 0
+40 6 0 33 18 0
+40 d 18 19 0
+41 -4 0 40 20 0
+41 d 20 0
+42 -5 0 40 21 0
+42 d 21 22 23 24 0
+43 2 -3 0 42 25 0
+43 d 25 26 27 0
+44 -2 3 0 41 28 0
+44 d 28 0
+45 -8 0 29 37 0
+46 -2 0 29 44 0
+47 0 45 46 39 16 0