perf: speedup bv_decide's LRAT checker by improving input validaton (#7491)

This PR achieves a speed up in bv_decide's LRAT checker by improving its input validation. When the LRAT checker works on a clause it needs to know that the clause has no duplicate literals and is not tautological (i.e. doesn't contain the same variable in different polarities). Previously this was done using a naive quadratic algorithm, now we check the property using a HashMap in linear time. Beyond this there is also a few micro optimizations. Together they improve the runtime on the SMTLIB problem `non-incremental/QF_BV/20210312-Bouvier/vlsat3_a15.smt2` from `1:25.31` to `1:01.32` minutes (where 39 seconds of this run time are the SAT solver and thus completely unaffected by the optimization) Co-authored-by: @JOSHCLUNE --------- Co-authored-by: JOSHCLUNE <josh.seth.clune@gmail.com>
2025-03-16 15:29:33 +01:00 · 2025-03-16 15:29:33 +01:00 · 6f16a535f8
commit 6f16a535f8
parent 6cbb8876d6
7 changed files with 174 additions and 213 deletions
--- a/src/Std/Sat/CNF/Literal.lean
+++ b/src/Std/Sat/CNF/Literal.lean
@ -21,6 +21,7 @@ namespace Literal
 /--
 Flip the polarity of `l`.
 -/
+@[inline]
 def negate (l : Literal α) : Literal α := (l.1, !l.2)

 end Literal
--- a/src/Std/Tactic/BVDecide/LRAT/Internal/Actions.lean
+++ b/src/Std/Tactic/BVDecide/LRAT/Internal/Actions.lean
@ -36,18 +36,20 @@ def WellFormedAction [Clause α β] : Action β α → Prop
  | .addRat _ c p _ _ => Limplies α p c
  | _ => True

-def natLiteralToPosFinLiteral {n : Nat} (x : Literal Nat) (x_ne_zero : x.1 ≠ 0) : Option (Literal (PosFin n)) := do
-  if h : x.1 < n then
-    some (⟨x.1, ⟨Nat.zero_lt_of_ne_zero x_ne_zero, h⟩⟩, x.2)
+@[inline]
+def natLiteralToPosFinLiteral {n : Nat} (x : Literal Nat) : Option (Literal (PosFin n)) := do
+  if h : x.1 < n ∧ x.1 ≠ 0 then
+    some (⟨x.1, ⟨Nat.zero_lt_of_ne_zero h.right, h.left⟩⟩, x.2)
  else
    none

-def intToLiteralPure {n : Nat} (x : Int) (x_ne_zero : x ≠ 0) : Option (Literal (PosFin n)) := do
-  if h : x.natAbs < n then
-    if x > 0 then
-      some (⟨x.natAbs, ⟨by omega, h⟩⟩, true)
+@[inline]
+def intToLiteral {n : Nat} (x : Int) : Option (Literal (PosFin n)) := do
+  if h1 : x.natAbs < n ∧ x ≠ 0 then
+    if h2 : x > 0 then
+      some (⟨x.natAbs, ⟨by omega, h1.left⟩⟩, true)
    else
-      some (⟨x.natAbs, ⟨by omega, h⟩⟩, false)
+      some (⟨x.natAbs, ⟨by omega, h1.left⟩⟩, false)
  else
    none

@ -64,31 +66,15 @@ are 0 or ≥ n.
 def intActionToDefaultClauseAction (n : Nat) : IntAction → Option (DefaultClauseAction n)
  | .addEmpty cId rupHints => some <| .addEmpty cId rupHints
  | .addRup cId c rupHints => do
-    let c : Array (Option (Literal (PosFin n))) :=
-      c.map (fun x => if h : x ≠ 0 then intToLiteralPure x h else none)
-    if c.contains none then
-      none
-    else
-      let c := c.filterMap id
-      match Clause.ofArray c with
-      | none => none
-      | some c => some <| .addRup cId c rupHints
+    let c ← c.mapM intToLiteral
+    let c ← Clause.ofArray c
+    return .addRup cId c rupHints
  | .addRat cId c pivot rupHints ratHints => do
-    if h : pivot.1 ≠ 0 then
-      let some pivot := natLiteralToPosFinLiteral pivot h
-        | none
-      let c : Array (Option (Literal (PosFin n))) :=
-        c.map (fun x => if h : x ≠ 0 then intToLiteralPure x h else none)
-      if c.contains none then
-        none
-      else
-        let c := c.filterMap id
-        match Clause.ofArray c with
-        | some c => some <| .addRat cId c pivot rupHints ratHints
-        | none => none
-    else
-      none
-  | .del ids => some <| .del ids
+    let pivot ← natLiteralToPosFinLiteral pivot
+    let c ← c.mapM intToLiteral
+    let c ← Clause.ofArray c
+    return .addRat cId c pivot rupHints ratHints
+  | .del ids => return .del ids


 end Internal
--- a/src/Std/Tactic/BVDecide/LRAT/Internal/Assignment.lean
+++ b/src/Std/Tactic/BVDecide/LRAT/Internal/Assignment.lean
@ -46,6 +46,7 @@ instance : ToString Assignment where
    | both => "both"
    | unassigned => "unassigned"

+@[inline]
 def hasPosAssignment (assignment : Assignment) : Bool :=
  match assignment with
  | pos => true
@ -53,6 +54,7 @@ def hasPosAssignment (assignment : Assignment) : Bool :=
  | both => true
  | unassigned => false

+@[inline]
 def hasNegAssignment (assignment : Assignment) : Bool :=
  match assignment with
  | pos => false
@ -63,6 +65,7 @@ def hasNegAssignment (assignment : Assignment) : Bool :=
 /--
 Updates the old assignment of `l` to reflect the fact that `(l, true)` is now part of the formula.
 -/
+@[inline]
 def addPosAssignment (oldAssignment : Assignment) : Assignment :=
  match oldAssignment with
  | pos => pos
@ -74,6 +77,7 @@ def addPosAssignment (oldAssignment : Assignment) : Assignment :=
 Updates the old assignment of `l` to reflect the fact that `(l, true)` is no longer part of the
 formula.
 -/
+@[inline]
 def removePosAssignment (oldAssignment : Assignment) : Assignment :=
  match oldAssignment with
  | pos => unassigned
@ -84,6 +88,7 @@ def removePosAssignment (oldAssignment : Assignment) : Assignment :=
 /--
 Updates the old assignment of `l` to reflect the fact that `(l, false)` is now part of the formula.
 -/
+@[inline]
 def addNegAssignment (oldAssignment : Assignment) : Assignment :=
  match oldAssignment with
  | pos => both
@ -95,6 +100,7 @@ def addNegAssignment (oldAssignment : Assignment) : Assignment :=
 Updates the old assignment of `l` to reflect the fact that `(l, false)` is no longer part of the
 formula.
 -/
+@[inline]
 def removeNegAssignment (oldAssignment : Assignment) : Assignment :=
  match oldAssignment with
  | pos => pos -- Note: This case should not occur
--- a/src/Std/Tactic/BVDecide/LRAT/Internal/Clause.lean
+++ b/src/Std/Tactic/BVDecide/LRAT/Internal/Clause.lean
@ -6,6 +6,7 @@ Authors: Josh Clune
 prelude
 import Init.Data.List.Erase
 import Init.Data.Array.Lemmas
+import Std.Data.HashMap
 import Std.Sat.CNF.Basic
 import Std.Tactic.BVDecide.LRAT.Internal.PosFin
 import Std.Tactic.BVDecide.LRAT.Internal.Assignment
@ -36,9 +37,6 @@ class Clause (α : outParam (Type u)) (β : Type v) where
  not_tautology : ∀ c : β, ∀ l : Literal α, l ∉ toList c ∨ Literal.negate l ∉ toList c
  /-- Returns none if the given array contains complementary literals -/
  ofArray : Array (Literal α) → Option β
-  ofArray_eq :
-    ∀ arr : Array (Literal α), (∀ i : Fin arr.size, ∀ j : Fin arr.size, i.1 ≠ j.1 → arr[i] ≠ arr[j]) →
-      ∀ c : β, ofArray arr = some c → toList c = arr.toList
  empty : β
  empty_eq : toList empty = []
  unit : Literal α → β
@ -47,8 +45,6 @@ class Clause (α : outParam (Type u)) (β : Type v) where
  isUnit_iff : ∀ c : β, ∀ l : Literal α, isUnit c = some l ↔ toList c = [l]
  negate : β → CNF.Clause α
  negate_eq : ∀ c : β, negate c = (toList c).map Literal.negate
-  /-- Returns none if the result is a tautology. -/
-  insert : β → Literal α → Option β
  delete : β → Literal α → β
  delete_iff : ∀ c : β, ∀ l : Literal α, ∀ l' : Literal α,
    l' ∈ toList (delete c l) ↔ l' ≠ l ∧ l' ∈ toList c
@ -116,6 +112,7 @@ theorem not_tautology (c : DefaultClause n) (l : Literal (PosFin n)) :
    apply Or.symm
    rwa [← hl] at h

+@[inline]
 def empty : DefaultClause n :=
  let clause := []
  have nodupkey := by
@ -126,6 +123,7 @@ def empty : DefaultClause n :=

 theorem empty_eq : toList (empty : DefaultClause n) = [] := rfl

+@[inline]
 def unit (l : Literal (PosFin n)) : DefaultClause n :=
  let clause := [l]
  have nodupkey : ∀ (l : PosFin n), ¬(l, true) ∈ clause ∨ ¬(l, false) ∈ clause := by
@ -142,6 +140,7 @@ def unit (l : Literal (PosFin n)) : DefaultClause n :=

 theorem unit_eq (l : Literal (PosFin n)) : toList (unit l) = [l] := rfl

+@[inline]
 def isUnit (c : DefaultClause n) : Option (Literal (PosFin n)) :=
  match c.clause with
  | [l] => some l
@ -156,151 +155,137 @@ theorem isUnit_iff (c : DefaultClause n) (l : Literal (PosFin n)) :
    simp
    apply hne

+@[inline]
 def negate (c : DefaultClause n) : CNF.Clause (PosFin n) := c.clause.map Literal.negate

 theorem negate_eq (c : DefaultClause n) : negate c = (toList c).map Literal.negate := rfl

-/--
-Attempts to add the literal `(idx, b)` to clause `c`. Returns none if doing so would make `c` a
-tautology.
-/
-def insert (c : DefaultClause n) (l : Literal (PosFin n)) : Option (DefaultClause n) :=
-  if heq1 : c.clause.contains (l.1, !l.2) then
-    none -- Adding l would make c a tautology
-  else if heq2 : c.clause.contains l then
-    some c
-  else
-    let clause := l :: c.clause
-    have nodupkey : ∀ (l : PosFin n), ¬(l, true) ∈ clause ∨ ¬(l, false) ∈ clause := by
-      intro l'
-      simp only [List.contains, Bool.not_eq_true] at heq1
-      simp only [List.find?, List.mem_cons, not_or, clause]
-      by_cases l' = l.1
-      · next l'_eq_l =>
-        by_cases hl : l.2
-        · apply Or.inr
-          constructor
-          · intro heq
-            simp [← heq] at hl
-          · simpa [hl, ← l'_eq_l] using heq1
-        · simp only [Bool.not_eq_true] at hl
-          apply Or.inl
-          constructor
-          · intro heq
-            simp [← heq] at hl
-          · simpa [hl, ← l'_eq_l] using heq1
-      · next l'_ne_l =>
-        have := c.nodupkey l'
-        rcases c.nodupkey l' with h | h
-        · left
-          constructor
-          · intro heq
-            simp [← heq] at l'_ne_l
-          · simp [h]
-        · right
-          constructor
-          · intro heq
-            simp [← heq] at l'_ne_l
-          · simp [h]
-    have nodup : List.Nodup clause := by
-      simp only [List.elem_eq_mem, decide_eq_true_eq] at heq2
-      simp [c.nodup, heq2, clause]
-    some ⟨clause, nodupkey, nodup⟩
-
 def ofArray (ls : Array (Literal (PosFin n))) : Option (DefaultClause n) :=
-  let fold_fn (l : Literal (PosFin n)) (acc : Option (DefaultClause n)) : Option (DefaultClause n) :=
+  let mapOption := ls.foldl folder (some (HashMap.emptyWithCapacity ls.size))
+  match mapOption with
+  | none => none
+  | some map =>
+   have mapnodup := map.distinct_keys
+    have nodupkey : ∀ (l : PosFin n), ¬(l, true) ∈ map.toList ∨ ¬(l, false) ∈ map.toList := by
+      intro l
+      apply Classical.byContradiction
+      simp_all
+    have nodup : map.toList.Nodup := by
+      rw [List.Nodup, List.pairwise_iff_forall_sublist]
+      simp only [ne_eq, Prod.forall, Bool.forall_bool, Prod.mk.injEq, not_and, Bool.not_eq_false,
+        Bool.not_eq_true, Bool.false_eq_true, imp_false, implies_true, and_true, Bool.true_eq_false,
+        true_and]
+      intro l1
+      constructor
+      . intros l2 h hl
+        rw [List.pairwise_iff_forall_sublist] at mapnodup
+        replace h : [l1, l2].Sublist map.keys := by
+          rw [← HashMap.map_fst_toList_eq_keys, List.sublist_map_iff]
+          apply Exists.intro [(l1, false), (l2, false)]
+          simp [h]
+        specialize mapnodup h
+        simp [hl] at mapnodup
+      . intros l2 h hl
+        rw [List.pairwise_iff_forall_sublist] at mapnodup
+        replace h : [l1, l2].Sublist map.keys := by
+          rw [← HashMap.map_fst_toList_eq_keys, List.sublist_map_iff]
+          apply Exists.intro [(l1, true), (l2, true)]
+          simp [h]
+        specialize mapnodup h
+        simp [hl] at mapnodup
+    some ⟨map.toList, nodupkey, nodup⟩
+where
+  folder (acc : Option (Std.HashMap (PosFin n) Bool)) (l : Literal (PosFin n)) :
+      Option (Std.HashMap (PosFin n) Bool) :=
    match acc with
    | none => none
-    | some acc => acc.insert l
-  ls.foldr fold_fn (some empty)
+    | some map =>
+      let (val?, map) := map.getThenInsertIfNew? l.1 l.2
+      if let some val' := val? then
+        if l.2 != val' then
+          none
+        else
+          some map
+      else
+        some map

-theorem ofArray_eq (arr : Array (Literal (PosFin n)))
-    (arrNodup : ∀ i : Fin arr.size, ∀ j : Fin arr.size, i.1 ≠ j.1 → arr[i] ≠ arr[j])
-    (c : DefaultClause n) :
-    ofArray arr = some c → toList c = Array.toList arr := by
-  intro h
-  simp only [ofArray] at h
-  rw [toList]
-  let motive (idx : Nat) (acc : Option (DefaultClause n)) : Prop :=
-    ∃ idx_le_arr_size : idx ≤ arr.size, ∀ c' : DefaultClause n, acc = some c' →
-      ∃ hsize : c'.clause.length = arr.size - idx, ∀ i : Fin c'.clause.length,
-      have idx_in_bounds : idx + i.1 < arr.size := by
-        omega
-      List.get c'.clause i = arr[idx + i]'idx_in_bounds
-  have h_base : motive arr.size (some empty) := by
-    apply Exists.intro <| Nat.le_refl arr.size
-    intro c' heq
-    simp only [Option.some.injEq] at heq
-    have hsize : List.length c'.clause = arr.size - arr.size := by
-      simp [← heq, empty]
-    apply Exists.intro hsize
-    intro i
-    simp only [← heq, empty, List.length_nil] at i
-    exact Fin.elim0 i
-  let fold_fn (l : Literal (PosFin n)) (acc : Option (DefaultClause n)) : Option (DefaultClause n) :=
-    match acc with
-    | none => none
-    | some acc => acc.insert l
-  have h_inductive (idx : Fin arr.size) (acc : Option (DefaultClause n)) (ih : motive (idx.1 + 1) acc) :
-    motive idx.1 (fold_fn arr[idx] acc) := by
-    rcases ih with ⟨idx_add_one_le_arr_size, ih⟩
-    apply Exists.intro <| Nat.le_of_succ_le idx_add_one_le_arr_size
-    intro c' heq
-    simp only [Fin.getElem_fin, fold_fn] at heq
-    split at heq
-    · simp at heq
-    · next acc =>
-      specialize ih acc rfl
-      rcases ih with ⟨hsize, ih⟩
-      simp only at ih
-      simp only [insert] at heq
-      split at heq
-      · simp at heq
-      · split at heq
-        · next h_dup =>
-          exfalso -- h_dup contradicts arrNodup
-          simp only [List.contains] at h_dup
-          rcases List.get_of_mem <| List.mem_of_elem_eq_true h_dup with ⟨j, hj⟩
-          specialize ih j
-          rw [hj] at ih
-          have idx_add_one_add_j_in_bounds : idx.1 + 1 + j.1 < arr.size := by
-            omega
-          have idx_ne_idx_add_one_add_j_in_bounds : idx.1 ≠ idx.1 + 1 + j.1 := by
-            omega
-          exact arrNodup idx ⟨idx.1 + 1 + j.1, idx_add_one_add_j_in_bounds⟩ idx_ne_idx_add_one_add_j_in_bounds ih
-        · simp only [Option.some.injEq] at heq
-          have hsize' : c'.clause.length = arr.size - idx.1 := by
-            simp only [← heq, List.length_cons, hsize]
-            omega
-          apply Exists.intro hsize'
-          intro i
-          simp only
-          have lhs_rw : c'.clause = arr[idx.1] :: acc.clause := by rw [← heq]
-          simp only [List.get_of_eq lhs_rw]
-          by_cases i.1 = 0
-          · next i_eq_zero =>
-            simp only [List.length_cons, i_eq_zero, List.get, Nat.add_zero]
-          · next i_ne_zero =>
-            rcases Nat.exists_eq_succ_of_ne_zero i_ne_zero with ⟨j, hj⟩
-            simp only [List.length_cons, hj, List.get, Nat.succ_eq_add_one]
-            simp only [Nat.add_comm j 1, ← Nat.add_assoc]
-            exact ih ⟨j, by omega⟩
-  rcases (Array.foldr_induction motive h_base h_inductive).2 c h with ⟨hsize, h⟩
-  ext
-  next i l =>
-  by_cases i_in_bounds : i < c.clause.length
-  · specialize h ⟨i, i_in_bounds⟩
-    have i_in_bounds' : i < arr.toList.length := by
-      dsimp; omega
-    rw [List.getElem?_eq_getElem i_in_bounds, List.getElem?_eq_getElem i_in_bounds']
-    simp only [List.get_eq_getElem, Nat.zero_add] at h
-    rw [Array.getElem_toList]
-    simp [h]
-  · have arr_data_length_le_i : arr.toList.length ≤ i := by
-      dsimp; omega
-    simp only [Nat.not_lt, ← List.getElem?_eq_none_iff] at i_in_bounds arr_data_length_le_i
-    rw [i_in_bounds, arr_data_length_le_i]
+@[simp]
+theorem ofArray.foldl_folder_none_eq_none : List.foldl ofArray.folder none ls = none := by
+  apply List.foldlRecOn (motive := (· = none))
+  · simp
+  · intro b hb a ha
+    unfold DefaultClause.ofArray.folder
+    simp [hb]

+theorem ofArray.mem_of_mem_of_foldl_folder_eq_some
+    (h : List.foldl DefaultClause.ofArray.folder (some acc) ls = some acc') :
+    ∀ l ∈ acc.toList, l ∈ acc'.toList := by
+  intro l hl
+  induction ls generalizing acc with
+  | nil => simp_all
+  | cons x xs ih =>
+    rcases l with ⟨var, pol⟩
+    rw [List.foldl_cons, DefaultClause.ofArray.folder.eq_def] at h
+    split at h
+    · contradiction
+    · simp only [HashMap.getThenInsertIfNew?_fst, HashMap.get?_eq_getElem?, bne_iff_ne, ne_eq,
+        HashMap.getThenInsertIfNew?_snd, ite_not] at h
+      split at h
+      · split at h
+        · apply ih
+          · exact h
+          · rw [Std.HashMap.mem_toList_iff_getElem?_eq_some, Std.HashMap.getElem?_insertIfNew]
+            rename_i map _ _ _ _ _
+            have : x.fst ∈ map := by
+              apply Classical.byContradiction
+              intro h2
+              have := Std.HashMap.getElem?_eq_none h2
+              simp_all
+            simp [this]
+            rw [Std.HashMap.mem_toList_iff_getElem?_eq_some] at hl
+            simp_all
+        · simp at h
+      · apply ih
+        · exact h
+        · rw [Std.HashMap.mem_toList_iff_getElem?_eq_some, Std.HashMap.getElem?_insertIfNew]
+          simp_all
+          intros
+          cases pol <;> simp_all
+
+theorem ofArray.folder_foldl_mem_of_mem
+    (h : List.foldl DefaultClause.ofArray.folder acc ls = some map) :
+    ∀ l ∈ ls, l ∈ map.toList := by
+  intro l hl
+  induction ls generalizing acc with
+  | nil => simp at hl
+  | cons x xs ih =>
+    simp at hl h
+    rcases hl with hl | hl
+    · rw [DefaultClause.ofArray.folder.eq_def] at h
+      simp at h
+      split at h
+      · simp at h
+      · split at h
+        · split at h
+          · apply mem_of_mem_of_foldl_folder_eq_some
+            · exact h
+            · rw [Std.HashMap.mem_toList_iff_getElem?_eq_some]
+              rw [Std.HashMap.getElem?_insertIfNew]
+              simp_all
+          · simp at h
+        · apply mem_of_mem_of_foldl_folder_eq_some
+          · exact h
+          · next hfoo =>
+            rw [hl]
+            cases x
+            simp [Std.HashMap.getElem?_insertIfNew]
+            intro hbar
+            exfalso
+            apply hfoo
+            rw [Std.HashMap.getElem?_eq_some_getElem! hbar]
+    · exact ih h hl
+
+@[inline]
 def delete (c : DefaultClause n) (l : Literal (PosFin n)) : DefaultClause n :=
  let clause := c.clause.erase l
  let nodupkey : ∀ (l : PosFin n), ¬(l, true) ∈ clause ∨ ¬(l, false) ∈ clause := by
@ -327,6 +312,7 @@ theorem delete_iff (c : DefaultClause n) (l l' : Literal (PosFin n)) :
  · simp only [hl, not_false_eq_true, true_and]
    exact List.mem_erase_of_ne hl

+@[inline]
 def contains (c : DefaultClause n) (l : Literal (PosFin n)) : Bool := c.clause.contains l

 theorem contains_iff :
@ -393,7 +379,6 @@ instance : Clause (PosFin n) (DefaultClause n) where
  toList := toList
  not_tautology := not_tautology
  ofArray := ofArray
-  ofArray_eq := ofArray_eq
  empty := empty
  empty_eq := empty_eq
  unit := unit
@ -402,7 +387,6 @@ instance : Clause (PosFin n) (DefaultClause n) where
  isUnit_iff := isUnit_iff
  negate := negate
  negate_eq := negate_eq
-  insert := insert
  delete := delete
  delete_iff := delete_iff
  contains := contains
--- a/src/Std/Tactic/BVDecide/LRAT/Internal/Convert.lean
+++ b/src/Std/Tactic/BVDecide/LRAT/Internal/Convert.lean
@ -57,40 +57,13 @@ def CNF.convertLRAT' (clauses : CNF (PosFin n)) : List (Option (DefaultClause n)

 theorem CNF.Clause.mem_lrat_of_mem (clause : CNF.Clause (PosFin n)) (h1 : l ∈ clause)
    (h2 : DefaultClause.ofArray clause.toArray = some lratClause) : l ∈ lratClause.clause := by
-  induction clause generalizing lratClause with
-  | nil => cases h1
-  | cons hd tl ih =>
-    unfold DefaultClause.ofArray at h2
-    rw [← Array.foldr_toList, Array.toArray_toList] at h2
-    dsimp only [List.foldr] at h2
-    split at h2
-    · cases h2
-    · rw [DefaultClause.insert] at h2
-      split at h2
-      · cases h2
-      · split at h2
-        · rename_i h
-          rw [← Option.some.inj h2] at *
-          cases h1
-          · exact List.mem_of_elem_eq_true h
-          · apply ih
-            · assumption
-            · next heq _ _ =>
-              unfold DefaultClause.ofArray
-              rw [← Array.foldr_toList, Array.toArray_toList]
-              exact heq
-        · cases h1
-          · simp only [← Option.some.inj h2]
-            constructor
-          · simp only at h2
-            simp only [← Option.some.inj h2]
-            rename_i heq _ _ _
-            apply List.Mem.tail
-            apply ih
-            assumption
-            unfold DefaultClause.ofArray
-            rw [← Array.foldr_toList, Array.toArray_toList]
-            exact heq
+  unfold DefaultClause.ofArray at h2
+  simp at h2
+  split at h2
+  · contradiction
+  · simp only [Option.some.injEq] at h2
+    rw [← h2]
+    apply DefaultClause.ofArray.folder_foldl_mem_of_mem <;> assumption

 theorem CNF.Clause.convertLRAT_sat_of_sat (clause : CNF.Clause (PosFin n))
    (h : Clause.convertLRAT' clause = some lratClause) :
--- a/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/Implementation.lean
+++ b/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/Implementation.lean
@ -119,15 +119,20 @@ def insertUnit : Array (Literal (PosFin n)) × Array Assignment × Bool →
    Literal (PosFin n) → Array (Literal (PosFin n)) × Array Assignment × Bool :=
  fun (units, assignments, foundContradiction) (l, b) =>
    let curAssignment := assignments[l.1]!
-    if hasAssignment b curAssignment then (units, assignments, foundContradiction)
-    else (units.push (l, b), assignments.modify l (addAssignment b), foundContradiction || curAssignment != unassigned)
+    if hasAssignment b curAssignment then
+      (units, assignments, foundContradiction)
+    else
+      let units := units.push (l, b)
+      let assignments := assignments.modify l (addAssignment b)
+      let foundContradiction := foundContradiction || curAssignment != unassigned
+      (units, assignments, foundContradiction)

 /--
 Returns an updated formula f and a bool which indicates whether a contradiction was found in the
 process of updating f.
 -/
-def insertRupUnits {n : Nat} (f : DefaultFormula n) (ls : CNF.Clause (PosFin n))
-    : DefaultFormula n × Bool :=
+def insertRupUnits {n : Nat} (f : DefaultFormula n) (ls : CNF.Clause (PosFin n)) :
+    DefaultFormula n × Bool :=
  let ⟨clauses, rupUnits, ratUnits, assignments⟩ := f
  let (rupUnits, assignments, foundContradiction) := ls.foldl insertUnit (rupUnits, assignments, false)
  (⟨clauses, rupUnits, ratUnits, assignments⟩, foundContradiction)
@ -147,11 +152,13 @@ def clearUnit : Array Assignment → Literal (PosFin n) → Array Assignment
 def clearRupUnits {n : Nat} (f : DefaultFormula n) : DefaultFormula n :=
  let ⟨clauses, rupUnits, ratUnits, assignments⟩ := f
  let assignments := rupUnits.foldl clearUnit assignments
+  -- TODO: in principle we could cache the memory of rupUnits here if we had Array.clear
  ⟨clauses, #[], ratUnits, assignments⟩

 def clearRatUnits {n : Nat} (f : DefaultFormula n) : DefaultFormula n :=
  let ⟨clauses, rupUnits, ratUnits, assignments⟩ := f
  let assignments := ratUnits.foldl clearUnit assignments
+  -- TODO: in principle we could cache the memory of ratUnits here if we had Array.clear
  ⟨clauses, rupUnits, #[], assignments⟩

 /--
--- a/src/Std/Tactic/BVDecide/LRAT/Internal/PosFin.lean
+++ b/src/Std/Tactic/BVDecide/LRAT/Internal/PosFin.lean
@ -5,6 +5,7 @@ Authors: Josh Clune
 -/
 prelude
 import Init.NotationExtra
+import Init.Data.Hashable

 namespace Std.Tactic.BVDecide
 namespace LRAT
@ -18,6 +19,9 @@ instance : DecidableEq (PosFin n) :=
 instance : CoeOut (PosFin n) Nat where
  coe p := p.val

+instance {n} : Hashable (PosFin n) where
+  hash p := hash p.val
+
 instance : ToString (PosFin n) where
  toString p := toString p.val