From c66cb00c0fbdc28636a0ebe7c0ac264e68ecd15b Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Thu, 20 Mar 2025 17:57:04 +0100 Subject: [PATCH] refactor: turn the AIG framework's RefVec from Array to Vector (#7603) This PR uses the new `Vector` API inside of the AIG framework's `RefVec` datatype. --- src/Std/Sat/AIG/Basic.lean | 4 +- src/Std/Sat/AIG/RefVec.lean | 69 ++++++++----------- src/Std/Sat/AIG/RefVecOperator/Fold.lean | 1 - .../Circuit/Lemmas/Operations/Extract.lean | 3 +- .../BVExpr/Circuit/Lemmas/Operations/Ult.lean | 1 - 5 files changed, 32 insertions(+), 46 deletions(-) diff --git a/src/Std/Sat/AIG/Basic.lean b/src/Std/Sat/AIG/Basic.lean index 5fed87fcf2..f426ca4a45 100644 --- a/src/Std/Sat/AIG/Basic.lean +++ b/src/Std/Sat/AIG/Basic.lean @@ -5,6 +5,7 @@ Authors: Henrik Böving -/ prelude import Std.Data.HashSet +import Init.Data.Vector.Basic namespace Std namespace Sat @@ -348,8 +349,7 @@ where A vector of references into `aig`. This is the `AIG` analog of `BitVec`. -/ structure RefVec (aig : AIG α) (w : Nat) where - refs : Array (Nat × Bool) - hlen : refs.size = w + refs : Vector (Nat × Bool) w hrefs : ∀ (h : i < w), refs[i].1 < aig.decls.size /-- diff --git a/src/Std/Sat/AIG/RefVec.lean b/src/Std/Sat/AIG/RefVec.lean index 3ff1f769a4..52f42c6cc3 100644 --- a/src/Std/Sat/AIG/RefVec.lean +++ b/src/Std/Sat/AIG/RefVec.lean @@ -6,6 +6,7 @@ Authors: Henrik Böving prelude import Std.Sat.AIG.LawfulOperator import Std.Sat.AIG.CachedGatesLemmas +import Init.Data.Vector.Lemmas namespace Std namespace Sat @@ -17,13 +18,11 @@ variable {α : Type} [Hashable α] [DecidableEq α] {aig : AIG α} namespace RefVec def empty : RefVec aig 0 where - refs := #[] - hlen := by simp + refs := #v[] hrefs := by intros; contradiction def emptyWithCapacity (c : Nat) : RefVec aig 0 where - refs := Array.emptyWithCapacity c - hlen := by simp + refs := Vector.emptyWithCapacity c hrefs := by intros; contradiction @[simp] @@ -33,17 +32,15 @@ theorem emptyWithCapacity_eq : emptyWithCapacity (aig := aig) c = empty := by @[inline] def cast' {aig1 aig2 : AIG α} (s : RefVec aig1 len) (h : - (∀ {i : Nat} (h : i < len), (s.refs[i]'(by have := s.hlen; omega)).1 < aig1.decls.size) - → ∀ {i : Nat} (h : i < len), (s.refs[i]'(by have := s.hlen; omega)).1 < aig2.decls.size) : + (∀ {i : Nat} (h : i < len), s.refs[i].1 < aig1.decls.size) + → ∀ {i : Nat} (h : i < len), s.refs[i].1 < aig2.decls.size) : RefVec aig2 len := { s with hrefs := by intros apply h - · intros - apply s.hrefs - assumption - · assumption + intros + apply s.hrefs } @[inline] @@ -56,22 +53,20 @@ def cast {aig1 aig2 : AIG α} (s : RefVec aig1 len) (h : aig1.decls.size ≤ aig @[inline] def get (s : RefVec aig len) (idx : Nat) (hidx : idx < len) : Ref aig := - let ⟨refs, hlen, hrefs⟩ := s - let ref := refs[idx]'(by rw [hlen]; assumption) - ⟨ref.1, ref.2, by apply hrefs; assumption⟩ + let ⟨refs, hrefs⟩ := s + let ref := refs[idx] + ⟨ref.1, ref.2, hrefs ..⟩ @[inline] def push (s : RefVec aig len) (ref : AIG.Ref aig) : RefVec aig (len + 1) := - let ⟨refs, hlen, hrefs⟩ := s + let ⟨refs, hrefs⟩ := s ⟨ refs.push (ref.gate, ref.invert), - by simp [hlen], by intro i hi - simp only [Array.getElem_push] + simp only [Vector.getElem_push hi] split · apply hrefs - omega · apply AIG.Ref.hgate ⟩ @@ -83,15 +78,13 @@ theorem cast_cast {aig1 aig2 aig3 : AIG α} (s : RefVec aig1 len) @[simp] theorem get_push_ref_eq (s : RefVec aig len) (ref : AIG.Ref aig) : (s.push ref).get len (by omega) = ref := by - have := s.hlen - simp [get, push, ← this] + simp [get, push] -- This variant exists because it is sometimes hard to rewrite properly with DTT. theorem get_push_ref_eq' (s : RefVec aig len) (ref : AIG.Ref aig) (idx : Nat) (hidx : idx = len) : (s.push ref).get idx (by omega) = ref := by - have := s.hlen - simp [get, push, ← this, hidx] + simp [get, push, hidx] theorem get_push_ref_lt (s : RefVec aig len) (ref : AIG.Ref aig) (idx : Nat) (hidx : idx < len) : @@ -99,9 +92,9 @@ theorem get_push_ref_lt (s : RefVec aig len) (ref : AIG.Ref aig) (idx : Nat) simp only [get, push, Ref.mk.injEq] cases ref simp only [Ref.mk.injEq] - rw [Array.getElem_push_lt] + rw [Vector.getElem_push_lt] · simp - · simp [hlen, hidx] + · simp [hidx] @[simp] theorem get_cast {aig1 aig2 : AIG α} (s : RefVec aig1 len) (idx : Nat) (hidx : idx < len) @@ -113,20 +106,18 @@ theorem get_cast {aig1 aig2 : AIG α} (s : RefVec aig1 len) (idx : Nat) (hidx : @[inline] def append (lhs : RefVec aig lw) (rhs : RefVec aig rw) : RefVec aig (lw + rw) := - let ⟨lrefs, hl1, hl2⟩ := lhs - let ⟨rrefs, hr1, hr2⟩ := rhs + let ⟨lrefs, hl⟩ := lhs + let ⟨rrefs, hr⟩ := rhs ⟨ lrefs ++ rrefs, - by simp [Array.size_append, hl1, hr1], by intro i h - by_cases hsplit : i < lrefs.size - · rw [Array.getElem_append_left] - apply hl2 + by_cases hsplit : i < lw + · rw [Vector.getElem_append_left] + apply hl omega - · rw [Array.getElem_append_right] - · apply hr2 - omega + · rw [Vector.getElem_append_right] + · apply hr · omega ⟩ @@ -141,15 +132,13 @@ theorem get_append (lhs : RefVec aig lw) (rhs : RefVec aig rw) (idx : Nat) simp only [get, append] split · simp [Ref.mk.injEq] - rw [Array.getElem_append_left] + rw [Vector.getElem_append_left] · simp - · rw [lhs.hlen] - assumption + · assumption · simp only [Ref.mk.injEq] - rw [Array.getElem_append_right] - · simp [lhs.hlen] - · rw [lhs.hlen] - omega + rw [Vector.getElem_append_right] + · simp + · omega @[inline] def getD (s : RefVec aig len) (idx : Nat) (alt : Ref aig) : Ref aig := @@ -176,7 +165,7 @@ def countKnown [Inhabited α] (aig : AIG α) (s : RefVec aig len) : Nat := Id.ru match decl with | .const .. => acc + 1 | _ => acc - return s.refs.foldl (init := 0) folder + return s.refs.foldl (b := 0) folder end RefVec diff --git a/src/Std/Sat/AIG/RefVecOperator/Fold.lean b/src/Std/Sat/AIG/RefVecOperator/Fold.lean index 19206d208c..dd88c1d755 100644 --- a/src/Std/Sat/AIG/RefVecOperator/Fold.lean +++ b/src/Std/Sat/AIG/RefVecOperator/Fold.lean @@ -186,7 +186,6 @@ theorem denote_fold_and {aig : AIG α} (s : RefVec aig len) : rw [AIG.LawfulOperator.denote_mem_prefix (f := mkConstCached)] · simp only [← h] · apply RefVec.hrefs - simp [FoldTarget.mkAnd, hidx] · omega end RefVec diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Extract.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Extract.lean index 9becb98fea..e650eedc4e 100644 --- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Extract.lean +++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Extract.lean @@ -91,8 +91,7 @@ theorem denote_blastExtract (aig : AIG α) (target : ExtractTarget aig newWidth) split · rw [RefVec.get_in_bound] rw [LawfulOperator.denote_mem_prefix (f := mkConstCached)] - · congr 1 - · assumption + congr 1 · rw [RefVec.get_out_bound] · simp · omega diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Ult.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Ult.lean index 8fdafbee0f..1591d5016a 100644 --- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Ult.lean +++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Ult.lean @@ -38,7 +38,6 @@ theorem mkUlt_denote_eq (aig : AIG α) (lhs rhs : BitVec w) (input : BinaryRefVe rw [AIG.LawfulOperator.denote_mem_prefix (f := AIG.mkConstCached)] rw [AIG.LawfulVecOperator.denote_mem_prefix (f := BVExpr.bitblast.blastNot)] apply hleft - assumption · dsimp only intro idx hidx rw [AIG.LawfulOperator.denote_mem_prefix (f := AIG.mkConstCached)]