From 6f16a535f83838cc6ff196abb33b70799482aa0a Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Sun, 16 Mar 2025 15:29:33 +0100 Subject: [PATCH] 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 --- src/Std/Sat/CNF/Literal.lean | 1 + .../BVDecide/LRAT/Internal/Actions.lean | 50 ++-- .../BVDecide/LRAT/Internal/Assignment.lean | 6 + .../Tactic/BVDecide/LRAT/Internal/Clause.lean | 270 ++++++++---------- .../BVDecide/LRAT/Internal/Convert.lean | 41 +-- .../LRAT/Internal/Formula/Implementation.lean | 15 +- .../Tactic/BVDecide/LRAT/Internal/PosFin.lean | 4 + 7 files changed, 174 insertions(+), 213 deletions(-) diff --git a/src/Std/Sat/CNF/Literal.lean b/src/Std/Sat/CNF/Literal.lean index 36a19340e0..724bf667eb 100644 --- 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 diff --git a/src/Std/Tactic/BVDecide/LRAT/Internal/Actions.lean b/src/Std/Tactic/BVDecide/LRAT/Internal/Actions.lean index 557c74fce0..324ce7728f 100644 --- 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 diff --git a/src/Std/Tactic/BVDecide/LRAT/Internal/Assignment.lean b/src/Std/Tactic/BVDecide/LRAT/Internal/Assignment.lean index ef953113a0..927bf3c27f 100644 --- 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 diff --git a/src/Std/Tactic/BVDecide/LRAT/Internal/Clause.lean b/src/Std/Tactic/BVDecide/LRAT/Internal/Clause.lean index c1a4764a1d..568f844757 100644 --- 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 diff --git a/src/Std/Tactic/BVDecide/LRAT/Internal/Convert.lean b/src/Std/Tactic/BVDecide/LRAT/Internal/Convert.lean index d2fa295845..332dac0fe2 100644 --- 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) : diff --git a/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/Implementation.lean b/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/Implementation.lean index 108fc7114e..d3f3c7b828 100644 --- 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⟩ /-- diff --git a/src/Std/Tactic/BVDecide/LRAT/Internal/PosFin.lean b/src/Std/Tactic/BVDecide/LRAT/Internal/PosFin.lean index 036e496986..d535987445 100644 --- 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