From 5a5e83c26c2c74948e32e103e155fb57079e8e6c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Mon, 17 Mar 2025 18:33:49 +0100 Subject: [PATCH] refactor: the AIG framework to track negations in a more efficient way (#7381) This PR refactors the AIG datastructures that underly bv_decide in order to allow a better tracking of negations in the circuit. This refactor has two effects, for one adding full constant folding to the AIG framework and secondly enabling us to add further simplifications from the Brummayer Biere paper in the future which was previously architecturally impossible. --- .../BVDecide/Frontend/Normalize/Simproc.lean | 20 +-- src/Std/Sat/AIG/Basic.lean | 103 ++++++--------- src/Std/Sat/AIG/CNF.lean | 41 +++--- src/Std/Sat/AIG/Cached.lean | 42 +++--- src/Std/Sat/AIG/CachedGates.lean | 125 +++--------------- src/Std/Sat/AIG/CachedGatesLemmas.lean | 88 ++---------- src/Std/Sat/AIG/CachedLemmas.lean | 47 +++---- src/Std/Sat/AIG/If.lean | 6 +- src/Std/Sat/AIG/LawfulOperator.lean | 18 ++- src/Std/Sat/AIG/LawfulVecOperator.lean | 8 +- src/Std/Sat/AIG/Lemmas.lean | 125 ++++++++++-------- src/Std/Sat/AIG/RefVec.lean | 20 ++- src/Std/Sat/AIG/RefVecOperator/Map.lean | 10 +- src/Std/Sat/AIG/RefVecOperator/Zip.lean | 6 +- src/Std/Sat/AIG/Relabel.lean | 8 +- src/Std/Sat/AIG/RelabelNat.lean | 2 +- .../BVExpr/Circuit/Impl/Operations/Add.lean | 2 + .../Bitblast/BVExpr/Circuit/Lemmas/Const.lean | 6 +- .../Bitblast/BVExpr/Circuit/Lemmas/Expr.lean | 6 +- .../BVExpr/Circuit/Lemmas/Operations/Add.lean | 10 +- .../BVExpr/Circuit/Lemmas/Operations/Neg.lean | 5 +- .../Circuit/Lemmas/Operations/ShiftLeft.lean | 6 +- .../Circuit/Lemmas/Operations/ShiftRight.lean | 6 +- .../Circuit/Lemmas/Operations/Udiv.lean | 100 +++++++------- .../BVExpr/Circuit/Lemmas/Operations/Ult.lean | 9 +- .../Circuit/Lemmas/Operations/ZeroExtend.lean | 6 +- .../Bitblast/BVExpr/Circuit/Lemmas/Var.lean | 6 +- .../BVDecide/Bitblast/BoolExpr/Circuit.lean | 10 +- tests/lean/run/bv_counterexample.lean | 2 +- 29 files changed, 359 insertions(+), 484 deletions(-) diff --git a/src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/Simproc.lean b/src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/Simproc.lean index d6f048d0f3..be3864b098 100644 --- a/src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/Simproc.lean +++ b/src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/Simproc.lean @@ -111,10 +111,10 @@ builtin_simproc [bv_normalize] bv_udiv_of_two_pow (((_ : BitVec _) / (BitVec.ofN } builtin_simproc [bv_normalize] bv_equal_const_not (~~~(_ : BitVec _) == (BitVec.ofNat _ _)) := fun e => do - let_expr BEq.beq α inst outerLhs rhs := e | return .continue + let_expr BEq.beq _ _ outerLhs rhs := e | return .continue let some ⟨w, rhsVal⟩ ← getBitVecValue? rhs | return .continue let_expr Complement.complement _ _ lhs := outerLhs | return .continue - let expr := mkApp4 (mkConst ``BEq.beq [0]) α inst lhs (toExpr (~~~rhsVal)) + let expr ← mkAppM ``BEq.beq #[lhs, toExpr (~~~rhsVal)] let proof := mkApp3 (mkConst ``Std.Tactic.BVDecide.Frontend.Normalize.BitVec.not_eq_comm) (toExpr w) @@ -123,10 +123,10 @@ builtin_simproc [bv_normalize] bv_equal_const_not (~~~(_ : BitVec _) == (BitVec. return .visit { expr := expr, proof? := some proof } builtin_simproc [bv_normalize] bv_equal_const_not' ((BitVec.ofNat _ _) == ~~~(_ : BitVec _)) := fun e => do - let_expr BEq.beq α inst lhs outerRhs := e | return .continue + let_expr BEq.beq _ _ lhs outerRhs := e | return .continue let some ⟨w, lhsVal⟩ ← getBitVecValue? lhs | return .continue let_expr Complement.complement _ _ rhs := outerRhs | return .continue - let expr := mkApp4 (mkConst ``BEq.beq [0]) α inst rhs (toExpr (~~~lhsVal)) + let expr ← mkAppM ``BEq.beq #[rhs, toExpr (~~~lhsVal)] let proof := mkApp3 (mkConst ``Std.Tactic.BVDecide.Frontend.Normalize.BitVec.not_eq_comm') (toExpr w) @@ -135,12 +135,12 @@ builtin_simproc [bv_normalize] bv_equal_const_not' ((BitVec.ofNat _ _) == ~~~(_ return .visit { expr := expr, proof? := some proof } builtin_simproc [bv_normalize] bv_and_eq_allOnes ((_ : BitVec _) &&& (_ : BitVec _) == (BitVec.ofNat _ _)) := fun e => do - let_expr BEq.beq α instBEq outerLhs rhs := e | return .continue + let_expr BEq.beq _ _ outerLhs rhs := e | return .continue let some ⟨w, rhsVal⟩ ← getBitVecValue? rhs | return .continue if -1#w != rhsVal then return .continue let_expr HAnd.hAnd _ _ _ _ llhs lrhs := outerLhs | return .continue - let newLhs := mkApp4 (mkConst ``BEq.beq [0]) α instBEq llhs rhs - let newRhs := mkApp4 (mkConst ``BEq.beq [0]) α instBEq lrhs rhs + let newLhs ← mkAppM ``BEq.beq #[llhs, rhs] + let newRhs ← mkAppM ``BEq.beq #[lrhs, rhs] let expr := mkApp2 (mkConst ``Bool.and) newLhs newRhs let proof := mkApp3 (mkConst ``Std.Tactic.BVDecide.Frontend.Normalize.BitVec.and_eq_allOnes) @@ -150,12 +150,12 @@ builtin_simproc [bv_normalize] bv_and_eq_allOnes ((_ : BitVec _) &&& (_ : BitVec return .visit { expr := expr, proof? := some proof } builtin_simproc [bv_normalize] bv_allOnes_eq_and ((BitVec.ofNat _ _) == (_ : BitVec _) &&& (_ : BitVec _)) := fun e => do - let_expr BEq.beq α instBEq lhs outerRhs := e | return .continue + let_expr BEq.beq _ _ lhs outerRhs := e | return .continue let some ⟨w, lhsVal⟩ ← getBitVecValue? lhs | return .continue if -1#w != lhsVal then return .continue let_expr HAnd.hAnd _ _ _ _ rlhs rrhs := outerRhs | return .continue - let newLhs := mkApp4 (mkConst ``BEq.beq [0]) α instBEq rlhs lhs - let newRhs := mkApp4 (mkConst ``BEq.beq [0]) α instBEq rrhs lhs + let newLhs ← mkAppM ``BEq.beq #[rlhs, lhs] + let newRhs ← mkAppM ``BEq.beq #[rrhs, lhs] let expr := mkApp2 (mkConst ``Bool.and) newLhs newRhs let proof := mkApp3 (mkConst ``Std.Tactic.BVDecide.Frontend.Normalize.BitVec.allOnes_eq_and) diff --git a/src/Std/Sat/AIG/Basic.lean b/src/Std/Sat/AIG/Basic.lean index b7e47b7e06..5fed87fcf2 100644 --- a/src/Std/Sat/AIG/Basic.lean +++ b/src/Std/Sat/AIG/Basic.lean @@ -224,21 +224,36 @@ instance : Membership α (AIG α) where mem := Mem /-- -A reference to a node within an AIG. This is the `AIG` analog of `Bool`. +A reference to a node within an AIG. -/ structure Ref (aig : AIG α) where gate : Nat + invert : Bool hgate : gate < aig.decls.size /-- A `Ref` into `aig1` is also valid for `aig2` if `aig1` is smaller than `aig2`. -/ @[inline] -def Ref.cast {aig1 aig2 : AIG α} (ref : Ref aig1) - (h : aig1.decls.size ≤ aig2.decls.size) : +def Ref.cast {aig1 aig2 : AIG α} (ref : Ref aig1) (h : aig1.decls.size ≤ aig2.decls.size) : Ref aig2 := { ref with hgate := by have := ref.hgate; omega } + +/-- +Flip the polarity of `Ref` if `inv` is set. +-/ +@[inline] +def Ref.flip {aig : AIG α} (ref : Ref aig) (inv : Bool) : Ref aig := + { ref with invert := inv ^^ ref.invert } + +/-- +Flip the polarity of `Ref`. +-/ +@[inline] +def Ref.not {aig : AIG α} (ref : Ref aig) : Ref aig := + ref.flip true + /-- A pair of `Ref`s, useful for `LawfulOperator`s that act on two `Ref`s at a time. -/ @@ -255,6 +270,14 @@ def BinaryInput.cast {aig1 aig2 : AIG α} (input : BinaryInput aig1) BinaryInput aig2 := { input with lhs := input.lhs.cast h, rhs := input.rhs.cast h } +/-- +Flip the current inverter settings of the `BinaryInput` if `linv` or `rinv` is set respectively. +-/ +@[inline] +def BinaryInput.invert {aig : AIG α} (input : BinaryInput aig) (linv rinv : Bool) : + BinaryInput aig := + { input with lhs := input.lhs.flip linv, rhs := input.rhs.flip rinv } + /-- A collection of 3 of `Ref`s, useful for `LawfulOperator`s that act on three `Ref`s at a time, in particular multiplexer style functions. @@ -292,14 +315,14 @@ Transform an `Entrypoint` into a graphviz string. Useful for debugging purposes. -/ def toGraphviz {α : Type} [DecidableEq α] [ToString α] [Hashable α] (entry : Entrypoint α) : String := - let ⟨⟨decls, _, hinv⟩, ⟨idx, h⟩⟩ := entry + let ⟨⟨decls, _, hinv⟩, ⟨idx, invert, h⟩⟩ := entry let (dag, s) := go "" decls hinv idx h |>.run ∅ let nodes := s.fold (fun x y ↦ x ++ toGraphvizString decls y) "" "Digraph AIG {" ++ nodes ++ dag ++ "}" where go {α : Type} [DecidableEq α] [ToString α] [Hashable α] (acc : String) (decls : Array (Decl α)) - (hinv : IsDAG α decls) (idx : Nat) (hidx : idx < decls.size) - : StateM (HashSet (Fin decls.size)) String := do + (hinv : IsDAG α decls) (idx : Nat) (hidx : idx < decls.size) : + StateM (HashSet (Fin decls.size)) String := do let fidx : Fin decls.size := Fin.mk idx hidx if (← get).contains fidx then return acc @@ -325,9 +348,9 @@ where A vector of references into `aig`. This is the `AIG` analog of `BitVec`. -/ structure RefVec (aig : AIG α) (w : Nat) where - refs : Array Nat + refs : Array (Nat × Bool) hlen : refs.size = w - hrefs : ∀ (h : i < w), refs[i] < aig.decls.size + hrefs : ∀ (h : i < w), refs[i].1 < aig.decls.size /-- A sequence of references bundled with their AIG. @@ -362,7 +385,7 @@ structure ExtendTarget (aig : AIG α) (newWidth : Nat) where Evaluate an `AIG.Entrypoint` using some assignment for atoms. -/ def denote (assign : α → Bool) (entry : Entrypoint α) : Bool := - go entry.ref.gate entry.aig.decls assign entry.ref.hgate entry.aig.invariant + go entry.ref.gate entry.aig.decls assign entry.ref.hgate entry.aig.invariant ^^ entry.ref.invert where go (x : Nat) (decls : Array (Decl α)) (assign : α → Bool) (h1 : x < decls.size) (h2 : IsDAG α decls) : @@ -400,61 +423,23 @@ def unexpandDenote : Lean.PrettyPrinter.Unexpander /-- The denotation of the sub-DAG in the `aig` at node `start` is false for all assignments. -/ -def UnsatAt (aig : AIG α) (start : Nat) (h : start < aig.decls.size) : Prop := - ∀ assign, ⟦aig, ⟨start, h⟩, assign⟧ = false +def UnsatAt (aig : AIG α) (start : Nat) (invert : Bool) (h : start < aig.decls.size) : Prop := + ∀ assign, ⟦aig, ⟨start, invert, h⟩, assign⟧ = false /-- The denotation of the `Entrypoint` is false for all assignments. -/ def Entrypoint.Unsat (entry : Entrypoint α) : Prop := - entry.aig.UnsatAt entry.ref.gate entry.ref.hgate - -/-- -An input to an AIG gate. --/ -structure Fanin (aig : AIG α) where - /-- - The node we are referring to. - -/ - ref : Ref aig - /-- - Whether the node is inverted - -/ - inv : Bool - -/-- -The `Ref.cast` equivalent for `Fanin`. --/ -@[inline] -def Fanin.cast {aig1 aig2 : AIG α} (fanin : Fanin aig1) - (h : aig1.decls.size ≤ aig2.decls.size) : - Fanin aig2 := - { fanin with ref := fanin.ref.cast h } - -/-- -The input type for creating AIG and gates. --/ -structure GateInput (aig : AIG α) where - lhs : Fanin aig - rhs : Fanin aig - -/-- -The `Ref.cast` equivalent for `GateInput`. --/ -@[inline] -def GateInput.cast {aig1 aig2 : AIG α} (input : GateInput aig1) - (h : aig1.decls.size ≤ aig2.decls.size) : - GateInput aig2 := - { input with lhs := input.lhs.cast h, rhs := input.rhs.cast h } + entry.aig.UnsatAt entry.ref.gate entry.ref.invert entry.ref.hgate /-- Add a new and inverter gate to the AIG in `aig`. Note that this version is only meant for proving, for production purposes use `AIG.mkGateCached` and equality theorems to this one. -/ -def mkGate (aig : AIG α) (input : GateInput aig) : Entrypoint α := +def mkGate (aig : AIG α) (input : BinaryInput aig) : Entrypoint α := let g := aig.decls.size let decls := - aig.decls.push <| .gate input.lhs.ref.gate input.rhs.ref.gate input.lhs.inv input.rhs.inv + aig.decls.push <| .gate input.lhs.gate input.rhs.gate input.lhs.invert input.rhs.invert let cache := aig.cache.noUpdate have invariant := by intro i lhs' rhs' linv' rinv' h1 h2 @@ -462,10 +447,10 @@ def mkGate (aig : AIG α) (input : GateInput aig) : Entrypoint α := split at h2 · apply aig.invariant <;> assumption · injections - have := input.lhs.ref.hgate - have := input.rhs.ref.hgate + have := input.lhs.hgate + have := input.rhs.hgate omega - ⟨{ aig with decls, invariant, cache }, ⟨g, by simp [g, decls]⟩⟩ + ⟨{ aig with decls, invariant, cache }, ⟨g, false, by simp [g, decls]⟩⟩ /-- Add a new input node to the AIG in `aig`. Note that this version is only meant for proving, @@ -481,7 +466,7 @@ def mkAtom (aig : AIG α) (n : α) : Entrypoint α := split at h2 · apply aig.invariant <;> assumption · contradiction - ⟨{ decls, invariant, cache }, ⟨g, by simp [g, decls]⟩⟩ + ⟨{ decls, invariant, cache }, ⟨g, false, by simp [g, decls]⟩⟩ /-- Add a new constant node to `aig`. Note that this version is only meant for proving, @@ -497,17 +482,17 @@ def mkConst (aig : AIG α) (val : Bool) : Entrypoint α := split at h2 · apply aig.invariant <;> assumption · contradiction - ⟨{ decls, invariant, cache }, ⟨g, by simp [g, decls]⟩⟩ + ⟨{ decls, invariant, cache }, ⟨g, false, by simp [g, decls]⟩⟩ /-- Determine whether `ref` is a `Decl.const` with value `b`. -/ def isConstant (aig : AIG α) (ref : Ref aig) (b : Bool) : Bool := - let ⟨gate, hgate⟩ := ref + let ⟨gate, invert, hgate⟩ := ref let decl := aig.decls[gate]'hgate match decl with - | .const val => b = val + | .const val => (invert ^^ b) = val | _ => false end AIG diff --git a/src/Std/Sat/AIG/CNF.lean b/src/Std/Sat/AIG/CNF.lean index b43ced351d..d1810717e2 100644 --- a/src/Std/Sat/AIG/CNF.lean +++ b/src/Std/Sat/AIG/CNF.lean @@ -121,7 +121,7 @@ Tseitin transformation. This is done by combining the atom assignment with an as auxiliary variables, that just evaluates the AIG at the corresponding node. -/ def cnfSatAssignment (aig : AIG Nat) (assign1 : Nat → Bool) : CNFVar aig → Bool := - mixAssigns assign1 (fun idx => ⟦aig, ⟨idx.val, idx.isLt⟩, assign1⟧) + mixAssigns assign1 (fun idx => ⟦aig, ⟨idx.val, false, idx.isLt⟩, assign1⟧) @[simp] theorem satAssignment_inl : (cnfSatAssignment aig assign1) (.inl x) = assign1 x := by @@ -129,7 +129,7 @@ theorem satAssignment_inl : (cnfSatAssignment aig assign1) (.inl x) = assign1 x @[simp] theorem satAssignment_inr : - (cnfSatAssignment aig assign1) (.inr x) = ⟦aig, ⟨x.val, x.isLt⟩, assign1⟧ := by + (cnfSatAssignment aig assign1) (.inr x) = ⟦aig, ⟨x.val, false, x.isLt⟩, assign1⟧ := by simp [cnfSatAssignment, mixAssigns] /-- @@ -156,7 +156,7 @@ structure Cache.Inv (cnf : CNF (CNFVar aig)) (marks : Array Bool) (hmarks : mark -/ heval : ∀ (assign : CNFVar aig → Bool) (_heval : cnf.eval assign = true) (idx : Nat) (hbound : idx < aig.decls.size) (_hmark : marks[idx]'(by omega) = true), - ⟦aig, ⟨idx, hbound⟩, projectLeftAssign assign⟧ = (projectRightAssign assign) idx hbound + ⟦aig, ⟨idx, false, hbound⟩, projectLeftAssign assign⟧ = (projectRightAssign assign) idx hbound /-- @@ -287,7 +287,7 @@ def Cache.addConst (cache : Cache aig cnf) (idx : Nat) (h : idx < aig.decls.size · next heq => simp only [heq, CNF.eval_append, Decl.constToCNF_eval, Bool.and_eq_true, beq_iff_eq] at htip heval - simp only [denote_idx_const htip, projectRightAssign_property, heval] + simp [denote_idx_const htip, projectRightAssign_property, heval] · next heq => simp only [CNF.eval_append, Decl.constToCNF_eval, Bool.and_eq_true, beq_iff_eq] at heval have := cache.inv.heval assign heval.right idx hbound hmarked @@ -376,7 +376,7 @@ def Cache.addGate (cache : Cache aig cnf) {hlb} {hrb} (idx : Nat) (h : idx < aig at htip heval have hleval := cache.inv.heval assign heval.right lhs (by omega) hl have hreval := cache.inv.heval assign heval.right rhs (by omega) hr - simp only [denote_idx_gate htip, hleval, projectRightAssign_property, hreval, heval] + cases linv <;> cases rinv <;> simp [denote_idx_gate htip, hleval, projectRightAssign_property, hreval, heval] · next heq => simp only [CNF.eval_append, Decl.gateToCNF_eval, Bool.and_eq_true, beq_iff_eq] at heval have := cache.inv.heval assign heval.right idx hbound hmarked @@ -439,7 +439,7 @@ theorem State.Inv_gateToCNF {aig : AIG Nat} {h} rinv) := by intro assign1 - simp [CNF.sat_def, denote_idx_gate heq] + cases linv <;> cases rinv <;> simp [CNF.sat_def, denote_idx_gate heq] /-- The state to accumulate CNF clauses as we run our Tseitin transformation on the AIG. @@ -566,10 +566,12 @@ theorem State.unsat_def (state : State aig) : rfl @[simp] -theorem State.eval_eq : State.eval assign state = state.cnf.eval assign := by simp [State.eval] +theorem State.eval_eq : State.eval assign state = state.cnf.eval assign := by + simp [State.eval] @[simp] -theorem State.sat_iff : State.Sat assign state ↔ state.cnf.Sat assign := by simp [State.sat_def] +theorem State.sat_iff : State.Sat assign state ↔ state.cnf.Sat assign := by + simp [State.sat_def] @[simp] theorem State.unsat_iff : State.Unsat state ↔ state.cnf.Unsat := by simp [State.unsat_def] @@ -581,7 +583,7 @@ Convert an AIG into CNF, starting at some entry node. -/ def toCNF (entry : Entrypoint Nat) : CNF Nat := let ⟨state, _⟩ := go entry.aig entry.ref.gate entry.ref.hgate (toCNF.State.empty entry.aig) - let cnf : CNF (CNFVar entry.aig) := [(.inr ⟨entry.ref.gate, entry.ref.hgate⟩, true)] :: state.cnf + let cnf : CNF (CNFVar entry.aig) := [(.inr ⟨entry.ref.gate, entry.ref.hgate⟩, !entry.ref.invert)] :: state.cnf cnf.relabel inj where inj {aig : AIG Nat} (var : CNFVar aig) : Nat := @@ -664,8 +666,8 @@ theorem toCNF.go_sat (aig : AIG Nat) (start : Nat) (h1 : start < aig.decls.size) rw [State.sat_iff] simp [this] -theorem toCNF.go_as_denote' (aig : AIG Nat) (start) (h1) (assign1) : - ⟦aig, ⟨start, h1⟩, assign1⟧ → (go aig start h1 (.empty aig)).val.eval (cnfSatAssignment aig assign1) := by +theorem toCNF.go_as_denote' (aig : AIG Nat) (start) (inv) (h1) (assign1) : + ⟦aig, ⟨start, inv, h1⟩, assign1⟧ → (go aig start h1 (.empty aig)).val.eval (cnfSatAssignment aig assign1) := by have := go_sat aig start h1 assign1 (.empty aig) simp only [State.Sat, CNF.sat_def] at this simp [this] @@ -674,26 +676,25 @@ theorem toCNF.go_as_denote' (aig : AIG Nat) (start) (h1) (assign1) : Connect SAT results about the CNF to SAT results about the AIG. -/ theorem toCNF.go_as_denote (aig : AIG Nat) (start) (h1) (assign1) : - ((⟦aig, ⟨start, h1⟩, assign1⟧ && (go aig start h1 (.empty aig)).val.eval (cnfSatAssignment aig assign1)) = sat?) + ((⟦aig, ⟨start, inv, h1⟩, assign1⟧ && (go aig start h1 (.empty aig)).val.eval (cnfSatAssignment aig assign1)) = sat?) → - (⟦aig, ⟨start, h1⟩, assign1⟧ = sat?) := by - have := go_as_denote' aig start h1 assign1 + (⟦aig, ⟨start, inv, h1⟩, assign1⟧ = sat?) := by + have := go_as_denote' aig start inv h1 assign1 by_cases CNF.eval (cnfSatAssignment aig assign1) (go aig start h1 (State.empty aig)).val.cnf <;> simp_all /-- Connect SAT results about the AIG to SAT results about the CNF. -/ -theorem toCNF.denote_as_go {assign : AIG.CNFVar aig → Bool}: - (⟦aig, ⟨start, h1⟩, projectLeftAssign assign⟧ = false) +theorem toCNF.denote_as_go {assign : AIG.CNFVar aig → Bool} : + (⟦aig, ⟨start, inv, h1⟩, projectLeftAssign assign⟧ = false) → - CNF.eval assign (([(.inr ⟨start, h1⟩, true)] :: (go aig start h1 (.empty aig)).val.cnf)) = false := by + CNF.eval assign (([(.inr ⟨start, h1⟩, !inv)] :: (go aig start h1 (.empty aig)).val.cnf)) = false := by intro h match heval1:(go aig start h1 (State.empty aig)).val.cnf.eval assign with | true => have heval2 := (go aig start h1 (.empty aig)).val.cache.inv.heval specialize heval2 assign heval1 start h1 go_marks - simp only [h, projectRightAssign_property, Bool.false_eq] at heval2 - simp [heval2] + cases inv <;> simp_all | false => simp [heval1] @@ -707,7 +708,7 @@ theorem toCNF_equisat (entry : Entrypoint Nat) : (toCNF entry).Unsat ↔ entry.U · intro h assign1 apply toCNF.go_as_denote specialize h (toCNF.cnfSatAssignment entry.aig assign1) - simpa using h + rcases entry with ⟨_, ⟨_, _ | _, _⟩⟩ <;> simpa using h · intro h assign apply toCNF.denote_as_go specialize h (toCNF.projectLeftAssign assign) diff --git a/src/Std/Sat/AIG/Cached.lean b/src/Std/Sat/AIG/Cached.lean index 8537c6f07c..0627ba521c 100644 --- a/src/Std/Sat/AIG/Cached.lean +++ b/src/Std/Sat/AIG/Cached.lean @@ -29,7 +29,7 @@ def mkAtomCached (aig : AIG α) (n : α) : Entrypoint α := let decl := .atom n match cache.get? decl with | some hit => - ⟨⟨decls, cache, inv⟩ , hit.idx, hit.hbound⟩ + ⟨⟨decls, cache, inv⟩ , hit.idx, false, hit.hbound⟩ | none => let g := decls.size let cache := cache.insert decls decl @@ -40,7 +40,7 @@ def mkAtomCached (aig : AIG α) (n : α) : Entrypoint α := split at h2 · apply inv <;> assumption · contradiction - ⟨⟨decls, cache, inv⟩, ⟨g, by simp [g, decls]⟩⟩ + ⟨⟨decls, cache, inv⟩, ⟨g, false, by simp [g, decls]⟩⟩ /-- A version of `AIG.mkConst` that uses the subterm cache in `AIG`. This version is meant for @@ -51,7 +51,7 @@ def mkConstCached (aig : AIG α) (val : Bool) : Entrypoint α := let decl := .const val match cache.get? decl with | some hit => - ⟨⟨decls, cache, inv⟩, hit.idx, hit.hbound⟩ + ⟨⟨decls, cache, inv⟩, hit.idx, false, hit.hbound⟩ | none => let g := decls.size let cache := cache.insert decls decl @@ -62,7 +62,7 @@ def mkConstCached (aig : AIG α) (val : Bool) : Entrypoint α := split at h2 · apply inv <;> assumption · contradiction - ⟨⟨decls, cache, inv⟩, ⟨g, by simp [g, decls]⟩⟩ + ⟨⟨decls, cache, inv⟩, ⟨g, false, by simp [g, decls]⟩⟩ /-- A version of `AIG.mkGate` that uses the subterm cache in `AIG`. This version is meant for @@ -70,26 +70,26 @@ programming, for proving purposes use `AIG.mkGate` and equality theorems to this Beyond caching this function also implements a subset of the optimizations presented in: -/ -def mkGateCached (aig : AIG α) (input : GateInput aig) : Entrypoint α := - let lhs := input.lhs.ref.gate - let rhs := input.rhs.ref.gate +def mkGateCached (aig : AIG α) (input : BinaryInput aig) : Entrypoint α := + let lhs := input.lhs.gate + let rhs := input.rhs.gate if lhs < rhs then go aig ⟨input.lhs, input.rhs⟩ else go aig ⟨input.rhs, input.lhs⟩ where - go (aig : AIG α) (input : GateInput aig) : Entrypoint α := + go (aig : AIG α) (input : BinaryInput aig) : Entrypoint α := let ⟨decls, cache, inv⟩ := aig - let lhs := input.lhs.ref.gate - 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 + let lhs := input.lhs.gate + let rhs := input.rhs.gate + let linv := input.lhs.invert + let rinv := input.rhs.invert + have := input.lhs.hgate + have := input.rhs.hgate let decl := .gate lhs rhs linv rinv match cache.get? decl with | some hit => - ⟨⟨decls, cache, inv⟩, ⟨hit.idx, hit.hbound⟩⟩ + ⟨⟨decls, cache, inv⟩, ⟨hit.idx, false, hit.hbound⟩⟩ | none => /- Here we implement the constant propagating subset of: @@ -102,15 +102,15 @@ where | _, .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)⟩ + | .const true, _, false, _ | .const false, _, true, _ => + ⟨⟨decls, cache, inv⟩, rhs, rinv, by assumption⟩ -- Right Neutrality - | _, .const true, false, false | _, .const false, false, true => - ⟨⟨decls, cache, inv⟩, lhs, (by assumption)⟩ + | _, .const true, _, false | _, .const false, _, true => + ⟨⟨decls, cache, inv⟩, lhs, linv, by assumption⟩ | _, _, _, _ => if lhs == rhs && linv == false && rinv == false then -- Idempotency rule - ⟨⟨decls, cache, inv⟩, lhs, (by assumption)⟩ + ⟨⟨decls, cache, inv⟩, lhs, false, by assumption⟩ else if lhs == rhs && linv == !rinv then -- Contradiction rule mkConstCached ⟨decls, cache, inv⟩ false @@ -125,7 +125,7 @@ where split at h2 · apply inv <;> assumption · injections; omega - ⟨⟨decls, cache, inv⟩, ⟨g, by simp [g, decls]⟩⟩ + ⟨⟨decls, cache, inv⟩, ⟨g, false, by simp [g, decls]⟩⟩ end AIG diff --git a/src/Std/Sat/AIG/CachedGates.lean b/src/Std/Sat/AIG/CachedGates.lean index 5c4ed37724..40ceef0562 100644 --- a/src/Std/Sat/AIG/CachedGates.lean +++ b/src/Std/Sat/AIG/CachedGates.lean @@ -22,94 +22,43 @@ variable {α : Type} [Hashable α] [DecidableEq α] /-- Create a not gate in the input AIG. This uses the builtin cache to enable automated subterm sharing. -/ -def mkNotCached (aig : AIG α) (gate : Ref aig) : Entrypoint α := - -- ¬x = true && invert x - let res := aig.mkConstCached true - let aig := res.aig - let constRef := res.ref - aig.mkGateCached { - lhs := { - ref := constRef - inv := false - } - rhs := { - ref := gate.cast <| by - intros - apply LawfulOperator.le_size_of_le_aig_size (f := mkConstCached) - omega - inv := true - } - } - @[inline] -def BinaryInput.asGateInput {aig : AIG α} (input : BinaryInput aig) (linv rinv : Bool) : - GateInput aig := - { lhs := { ref := input.lhs, inv := linv }, rhs := { ref := input.rhs, inv := rinv } } +def mkNotCached (aig : AIG α) (gate : Ref aig) : Entrypoint α := + ⟨aig, gate.not⟩ /-- Create an and gate in the input AIG. This uses the builtin cache to enable automated subterm sharing. -/ +@[inline] def mkAndCached (aig : AIG α) (input : BinaryInput aig) : Entrypoint α := - aig.mkGateCached <| input.asGateInput false false + aig.mkGateCached input /-- Create an or gate in the input AIG. This uses the builtin cache to enable automated subterm sharing. -/ def mkOrCached (aig : AIG α) (input : BinaryInput aig) : Entrypoint α := - -- x or y = true && (invert (invert x && invert y)) - let res := aig.mkGateCached <| input.asGateInput true true + -- x or y = invert (invert x && invert y) + let res := aig.mkGateCached <| input.invert true true let aig := res.aig let auxRef := res.ref - let res := aig.mkConstCached true - let aig := res.aig - let constRef := res.ref - aig.mkGateCached { - lhs := { - ref := constRef - inv := false - }, - rhs := { - ref := auxRef.cast <| by - intros - simp +zetaDelta only - apply LawfulOperator.le_size_of_le_aig_size (f := mkConstCached) - omega - inv := true - } - } + ⟨aig, auxRef.not⟩ /-- Create an xor gate in the input AIG. This uses the builtin cache to enable automated subterm sharing. -/ def mkXorCached (aig : AIG α) (input : BinaryInput aig) : Entrypoint α := - -- x xor y = (invert (invert (x && y))) && (invert ((invert x) && (invert y))) - let res := aig.mkGateCached <| input.asGateInput false false + -- x xor y = (invert (x && y)) && (invert ((invert x) && (invert y))) + let res := aig.mkGateCached input let aig := res.aig let aux1Ref := res.ref - let rinput := - (input.asGateInput true true).cast - (by - intros - apply LawfulOperator.le_size_of_le_aig_size (f := mkGateCached) - omega) - let res := aig.mkGateCached rinput + let input := input.cast <| by apply LawfulOperator.le_size (f := mkGateCached) + let res := aig.mkGateCached (input.invert true true) let aig := res.aig let aux2Ref := res.ref - aig.mkGateCached { - lhs := { - ref := aux1Ref.cast <| by - simp +zetaDelta only - apply LawfulOperator.le_size_of_le_aig_size (f := mkGateCached) - omega - inv := true - }, - rhs := { - ref := aux2Ref - inv := true - } - } + let aux1Ref := aux1Ref.cast <| by apply LawfulOperator.le_size (f := mkGateCached) + aig.mkGateCached ⟨aux1Ref.not, aux2Ref.not⟩ /-- Create an equality gate in the input AIG. This uses the builtin cache to enable automated subterm @@ -117,58 +66,26 @@ sharing. -/ def mkBEqCached (aig : AIG α) (input : BinaryInput aig) : Entrypoint α := -- a == b = (invert (a && (invert b))) && (invert ((invert a) && b)) - let res := aig.mkGateCached <| input.asGateInput false true + let res := aig.mkGateCached <| input.invert false true let aig := res.aig let aux1Ref := res.ref - let rinput := - (input.asGateInput true false).cast - (by - intros - apply LawfulOperator.le_size_of_le_aig_size (f := mkGateCached) - omega) - let res := aig.mkGateCached rinput + let input := input.cast <| by apply LawfulOperator.le_size (f := mkGateCached) + let res := aig.mkGateCached (input.invert true false) let aig := res.aig let aux2Ref := res.ref - aig.mkGateCached { - lhs := { - ref := aux1Ref.cast <| by - simp +zetaDelta only - apply LawfulOperator.le_size_of_le_aig_size (f := mkGateCached) - omega - inv := true - }, - rhs := { - ref := aux2Ref - inv := true - } - } + let aux1Ref := aux1Ref.cast <| by apply LawfulOperator.le_size (f := mkGateCached) + aig.mkGateCached ⟨aux1Ref.not, aux2Ref.not⟩ /-- 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))) - let res := aig.mkGateCached <| input.asGateInput false true + -- a -> b = (invert (a and (invert b))) + let res := aig.mkGateCached <| input.invert false true let aig := res.aig let auxRef := res.ref - let res := aig.mkConstCached true - let aig := res.aig - let constRef := res.ref - aig.mkGateCached { - lhs := { - ref := constRef - inv := false - }, - rhs := { - ref := auxRef.cast <| by - intros - simp +zetaDelta only - apply LawfulOperator.le_size_of_le_aig_size (f := mkConstCached) - omega - inv := true - } - } + ⟨aig, auxRef.not⟩ end AIG diff --git a/src/Std/Sat/AIG/CachedGatesLemmas.lean b/src/Std/Sat/AIG/CachedGatesLemmas.lean index f17df1aa34..4f1b9afbd9 100644 --- a/src/Std/Sat/AIG/CachedGatesLemmas.lean +++ b/src/Std/Sat/AIG/CachedGatesLemmas.lean @@ -18,12 +18,6 @@ namespace Sat namespace AIG -/-- -Encoding of not as boolean expression in AIG form. --/ -private theorem not_as_aig : ∀ (b : Bool), (true && !b) = !b := by - decide - /-- Encoding of or as boolean expression in AIG form. -/ @@ -50,27 +44,13 @@ private theorem imp_as_aig : ∀ (a b : Bool), (!(a && !b)) = (!a || b) := by variable {α : Type} [Hashable α] [DecidableEq α] -@[simp] -theorem BinaryInput_asGateInput_lhs {aig : AIG α} (input : BinaryInput aig) (linv rinv : Bool) : - (input.asGateInput linv rinv).lhs = ⟨input.lhs, linv⟩ := rfl - -@[simp] -theorem BinaryInput_asGateInput_rhs {aig : AIG α} (input : BinaryInput aig) (linv rinv : Bool) : - (input.asGateInput linv rinv).rhs = ⟨input.rhs, rinv⟩ := rfl - theorem mkNotCached_le_size (aig : AIG α) (gate : Ref aig) : aig.decls.size ≤ (aig.mkNotCached gate).aig.decls.size := by - simp only [mkNotCached] - apply LawfulOperator.le_size_of_le_aig_size - apply mkConstCached_le_size + simp [mkNotCached] theorem mkNotCached_decl_eq idx (aig : AIG α) (gate : Ref aig) {h : idx < aig.decls.size} {h2} : - (aig.mkNotCached gate).aig.decls[idx]'h2 = aig.decls[idx] := by - simp only [mkNotCached] - rw [AIG.LawfulOperator.decl_eq (f := mkGateCached)] - rw [AIG.LawfulOperator.decl_eq (f := mkConstCached)] - apply LawfulOperator.lt_size_of_lt_aig_size (f := mkConstCached) - assumption + (aig.mkNotCached gate).aig.decls[idx]'h2 = aig.decls[idx]'h := by + simp [mkNotCached] instance : LawfulOperator α Ref mkNotCached where le_size := mkNotCached_le_size @@ -80,10 +60,7 @@ instance : LawfulOperator α Ref mkNotCached where @[simp] theorem denote_mkNotCached {aig : AIG α} {gate : Ref aig} : - ⟦aig.mkNotCached gate, assign⟧ - = - !⟦aig, ⟨gate.gate, gate.hgate⟩, assign⟧ := by - rw [← not_as_aig] + ⟦aig.mkNotCached gate, assign⟧ = !⟦aig, gate, assign⟧ := by simp [mkNotCached, LawfulOperator.denote_mem_prefix (f := mkConstCached) gate.hgate] theorem mkAndCached_le_size (aig : AIG α) (input : BinaryInput aig) : @@ -104,33 +81,19 @@ instance : LawfulOperator α BinaryInput mkAndCached where @[simp] theorem denote_mkAndCached {aig : AIG α} {input : BinaryInput aig} : - ⟦aig.mkAndCached input, assign⟧ - = - (⟦aig, input.lhs, assign⟧ - && - ⟦aig, input.rhs, assign⟧) := by + ⟦aig.mkAndCached input, assign⟧ = (⟦aig, input.lhs, assign⟧ && ⟦aig, input.rhs, assign⟧) := by simp [mkAndCached] theorem mkOrCached_le_size (aig : AIG α) (input : BinaryInput aig) : aig.decls.size ≤ (aig.mkOrCached input).aig.decls.size := by simp only [mkOrCached] - apply LawfulOperator.le_size_of_le_aig_size - apply LawfulOperator.le_size_of_le_aig_size (f := mkConstCached) - apply LawfulOperator.le_size_of_le_aig_size - omega + apply LawfulOperator.le_size theorem mkOrCached_decl_eq idx (aig : AIG α) (input : BinaryInput aig) {h : idx < aig.decls.size} {h2} : (aig.mkOrCached input).aig.decls[idx]'h2 = aig.decls[idx] := by simp only [mkOrCached] rw [AIG.LawfulOperator.decl_eq (f := mkGateCached)] - rw [AIG.LawfulOperator.decl_eq (f := mkConstCached)] - · rw [AIG.LawfulOperator.decl_eq (f := mkGateCached)] - apply LawfulOperator.lt_size_of_lt_aig_size - assumption - · apply LawfulOperator.lt_size_of_lt_aig_size (f := mkConstCached) - apply LawfulOperator.lt_size_of_lt_aig_size - assumption instance : LawfulOperator α BinaryInput mkOrCached where le_size := mkOrCached_le_size @@ -138,11 +101,7 @@ instance : LawfulOperator α BinaryInput mkOrCached where @[simp] theorem denote_mkOrCached {aig : AIG α} {input : BinaryInput aig} : - ⟦aig.mkOrCached input, assign⟧ - = - (⟦aig, input.lhs, assign⟧ - || - ⟦aig, input.rhs, assign⟧) := by + ⟦aig.mkOrCached input, assign⟧ = (⟦aig, input.lhs, assign⟧ || ⟦aig, input.rhs, assign⟧) := by rw [← or_as_aig] simp [mkOrCached, LawfulOperator.denote_input_entry (f := mkConstCached)] @@ -174,12 +133,7 @@ instance : LawfulOperator α BinaryInput mkXorCached where @[simp] theorem denote_mkXorCached {aig : AIG α} {input : BinaryInput aig} : - ⟦aig.mkXorCached input, assign⟧ - = - xor - ⟦aig, input.lhs, assign⟧ - ⟦aig, input.rhs, assign⟧ - := by + ⟦aig.mkXorCached input, assign⟧ = (⟦aig, input.lhs, assign⟧ ^^ ⟦aig, input.rhs, assign⟧) := by rw [← xor_as_aig] simp [ mkXorCached, @@ -214,11 +168,7 @@ instance : LawfulOperator α BinaryInput mkBEqCached where @[simp] theorem denote_mkBEqCached {aig : AIG α} {input : BinaryInput aig} : - ⟦aig.mkBEqCached input, assign⟧ - = - (⟦aig, input.lhs, assign⟧ - == - ⟦aig, input.rhs, assign⟧) := by + ⟦aig.mkBEqCached input, assign⟧ = (⟦aig, input.lhs, assign⟧ == ⟦aig, input.rhs, assign⟧) := by rw [← beq_as_aig] simp [ mkBEqCached, @@ -229,23 +179,13 @@ theorem denote_mkBEqCached {aig : AIG α} {input : BinaryInput aig} : theorem mkImpCached_le_size (aig : AIG α) (input : BinaryInput aig) : aig.decls.size ≤ (aig.mkImpCached input).aig.decls.size := by simp only [mkImpCached] - apply LawfulOperator.le_size_of_le_aig_size - apply LawfulOperator.le_size_of_le_aig_size (f := mkConstCached) - apply LawfulOperator.le_size_of_le_aig_size - omega + apply LawfulOperator.le_size theorem mkImpCached_decl_eq idx (aig : AIG α) (input : BinaryInput aig) {h : idx < aig.decls.size} {h2} : (aig.mkImpCached input).aig.decls[idx]'h2 = aig.decls[idx] := by simp only [mkImpCached] rw [AIG.LawfulOperator.decl_eq (f := mkGateCached)] - rw [AIG.LawfulOperator.decl_eq (f := mkConstCached)] - · rw [AIG.LawfulOperator.decl_eq (f := mkGateCached)] - apply LawfulOperator.lt_size_of_lt_aig_size - assumption - · apply LawfulOperator.lt_size_of_lt_aig_size (f := mkConstCached) - apply LawfulOperator.lt_size_of_lt_aig_size - assumption instance : LawfulOperator α BinaryInput mkImpCached where le_size := mkImpCached_le_size @@ -253,13 +193,7 @@ instance : LawfulOperator α BinaryInput mkImpCached where @[simp] theorem denote_mkImpCached {aig : AIG α} {input : BinaryInput aig} : - ⟦aig.mkImpCached input, assign⟧ - = - ( - !⟦aig, ⟨input.lhs.gate, input.lhs.hgate⟩, assign⟧ - || - ⟦aig, ⟨input.rhs.gate, input.rhs.hgate⟩, assign⟧ - ) := by + ⟦aig.mkImpCached input, assign⟧ = ( !⟦aig, input.lhs, assign⟧ || ⟦aig, input.rhs, assign⟧) := by rw [← imp_as_aig] simp [mkImpCached, LawfulOperator.denote_input_entry (f := mkConstCached)] diff --git a/src/Std/Sat/AIG/CachedLemmas.lean b/src/Std/Sat/AIG/CachedLemmas.lean index 311ad2a982..3254cbeaa6 100644 --- a/src/Std/Sat/AIG/CachedLemmas.lean +++ b/src/Std/Sat/AIG/CachedLemmas.lean @@ -25,7 +25,7 @@ If we find a cached atom declaration in the AIG, denoting it is equivalent to de theorem denote_mkAtom_cached {aig : AIG α} {hit} : aig.cache.get? (.atom v) = some hit → - ⟦aig, ⟨hit.idx, hit.hbound⟩, assign⟧ = ⟦aig.mkAtom v, assign⟧ := by + ⟦aig, ⟨hit.idx, false, hit.hbound⟩, assign⟧ = ⟦aig.mkAtom v, assign⟧ := by have := hit.hvalid simp only [denote_mkAtom] unfold denote denote.go @@ -98,7 +98,7 @@ If we find a cached const declaration in the AIG, denoting it is equivalent to d theorem denote_mkConst_cached {aig : AIG α} {hit} : aig.cache.get? (.const b) = some hit → - ⟦aig, ⟨hit.idx, hit.hbound⟩, assign⟧ = ⟦aig.mkConst b, assign⟧ := by + ⟦aig, ⟨hit.idx, false, hit.hbound⟩, assign⟧ = ⟦aig.mkConst b, assign⟧ := by have := hit.hvalid simp only [denote_mkConst] unfold denote denote.go @@ -171,9 +171,9 @@ theorem mkConstCached_eval_eq_mkConst_eval {aig : AIG α} : If we find a cached gate declaration in the AIG, denoting it is equivalent to denoting `AIG.mkGate`. -/ theorem denote_mkGate_cached {aig : AIG α} {input} {hit} : - aig.cache.get? (.gate input.lhs.ref.gate input.rhs.ref.gate input.lhs.inv input.rhs.inv) = some hit + aig.cache.get? (.gate input.lhs.gate input.rhs.gate input.lhs.invert input.rhs.invert) = some hit → - ⟦⟨aig, hit.idx, hit.hbound⟩, assign⟧ + ⟦⟨aig, hit.idx, false, hit.hbound⟩, assign⟧ = ⟦aig.mkGate input, assign⟧ := by intros @@ -184,27 +184,29 @@ theorem denote_mkGate_cached {aig : AIG α} {input} {hit} : unfold denote denote.go split <;> simp_all[denote] -theorem mkGateCached.go_le_size (aig : AIG α) (input : GateInput aig) : +theorem mkGateCached.go_le_size (aig : AIG α) (input : BinaryInput aig) : aig.decls.size ≤ (go aig input).aig.decls.size := by dsimp only [go] split · simp - · split <;> try simp +arith [mkConstCached_le_size] + · split <;> try simp [mkConstCached_le_size] split - · simp +arith - · split <;> simp +arith [mkConstCached_le_size] + · simp + · split + · simp [mkConstCached_le_size] + · simp /-- `AIG.mkGateCached` never shrinks the underlying AIG. -/ -theorem mkGateCached_le_size (aig : AIG α) (input : GateInput aig) +theorem mkGateCached_le_size (aig : AIG α) (input : BinaryInput aig) : aig.decls.size ≤ (aig.mkGateCached input).aig.decls.size := by dsimp only [mkGateCached] split · apply mkGateCached.go_le_size · apply mkGateCached.go_le_size -theorem mkGateCached.go_decl_eq (aig : AIG α) (input : GateInput aig) : +theorem mkGateCached.go_decl_eq (aig : AIG α) (input : BinaryInput aig) : ∀ (idx : Nat) (h1) (h2), (go aig input).aig.decls[idx]'h1 = aig.decls[idx]'h2 := by generalize hres : go aig input = res unfold go at hres @@ -256,7 +258,7 @@ theorem mkGateCached.go_decl_eq (aig : AIG α) (input : GateInput aig) : 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) : +theorem mkGateCached_decl_eq (aig : AIG α) (input : BinaryInput aig) : ∀ (idx : Nat) (h1) (h2), (aig.mkGateCached input).aig.decls[idx]'h1 = aig.decls[idx]'h2 := by generalize hres : mkGateCached aig input = res unfold mkGateCached at hres @@ -267,13 +269,13 @@ theorem mkGateCached_decl_eq (aig : AIG α) (input : GateInput aig) : intros rw [mkGateCached.go_decl_eq] -instance : LawfulOperator α GateInput mkGateCached where +instance : LawfulOperator α BinaryInput mkGateCached where le_size := mkGateCached_le_size decl_eq := by intros apply mkGateCached_decl_eq -theorem mkGateCached.go_eval_eq_mkGate_eval {aig : AIG α} {input : GateInput aig} : +theorem mkGateCached.go_eval_eq_mkGate_eval {aig : AIG α} {input : BinaryInput aig} : ⟦go aig input, assign⟧ = ⟦aig.mkGate input, assign⟧ := by simp only [go] split @@ -289,28 +291,27 @@ theorem mkGateCached.go_eval_eq_mkGate_eval {aig : AIG α} {input : GateInput ai · next heq _ _ _ => simp_all [denote_idx_const heq] · next heq _ _ _ => + rcases input with ⟨_, ⟨rhs, rinv, hrgate⟩⟩ simp_all [denote_idx_const heq] · next heq _ _ _ => + rcases input with ⟨_, ⟨rhs, rinv, hrgate⟩⟩ simp_all [denote_idx_const heq] - · next heq _ _ _ _ => + · next heq _ _ _ _ _ => + rcases input with ⟨⟨lhs, linv, hlgate⟩, _⟩ simp_all [denote_idx_const heq] - · next heq _ _ _ => + · next heq _ _ _ _ _ => + rcases input with ⟨⟨lhs, linv, hlgate⟩, _⟩ simp_all [denote_idx_const heq] - · split + · rcases input with ⟨⟨lhs, linv, hlgate⟩, ⟨rhs, rinv, hrgate⟩⟩ + split · next hif => simp only [beq_false, Bool.and_eq_true, beq_iff_eq, Bool.not_eq_true'] at hif rcases hif with ⟨⟨hifeq, hlinv⟩, hrinv⟩ - replace hifeq : input.lhs.ref = input.rhs.ref := by - rcases input with ⟨⟨⟨_, _⟩, _⟩, ⟨⟨_, _⟩, _⟩⟩ - simpa using hifeq simp [hlinv, hrinv, hifeq] · split · next hif => simp only [Bool.and_eq_true, beq_iff_eq] at hif rcases hif with ⟨hifeq, hinv⟩ - replace hifeq : input.lhs.ref = input.rhs.ref := by - rcases input with ⟨⟨⟨_, _⟩, _⟩, ⟨⟨_, _⟩, _⟩⟩ - simpa using hifeq simp [hifeq, hinv] · simp [mkGate, denote] @@ -318,7 +319,7 @@ theorem mkGateCached.go_eval_eq_mkGate_eval {aig : AIG α} {input : GateInput ai The central equality theorem between `mkGateCached` and `mkGate`. -/ @[simp] -theorem mkGateCached_eval_eq_mkGate_eval {aig : AIG α} {input : GateInput aig} : +theorem mkGateCached_eval_eq_mkGate_eval {aig : AIG α} {input : BinaryInput aig} : ⟦aig.mkGateCached input, assign⟧ = ⟦aig.mkGate input, assign⟧ := by simp only [mkGateCached] split diff --git a/src/Std/Sat/AIG/If.lean b/src/Std/Sat/AIG/If.lean index 649a7dde04..d37781ecc6 100644 --- a/src/Std/Sat/AIG/If.lean +++ b/src/Std/Sat/AIG/If.lean @@ -221,12 +221,12 @@ theorem go_denote_mem_prefix {w : Nat} (aig : AIG α) (curr : Nat) (hcurr : curr (discr : Ref aig) (lhs rhs : RefVec aig w) (s : RefVec 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⟩, + ⟨start, inv, by apply Nat.lt_of_lt_of_le; exact hstart; apply go_le_size⟩, assign ⟧ = - ⟦aig, ⟨start, hstart⟩, assign⟧ := by - apply denote.eq_of_isPrefix (entry := ⟨aig, start,hstart⟩) + ⟦aig, ⟨start, inv, hstart⟩, assign⟧ := by + apply denote.eq_of_isPrefix (entry := ⟨aig, start, inv, hstart⟩) apply IsPrefix.of · intros apply go_decl_eq diff --git a/src/Std/Sat/AIG/LawfulOperator.lean b/src/Std/Sat/AIG/LawfulOperator.lean index f7bd85297e..a26a40ba87 100644 --- a/src/Std/Sat/AIG/LawfulOperator.lean +++ b/src/Std/Sat/AIG/LawfulOperator.lean @@ -30,6 +30,13 @@ structure IsPrefix (decls1 decls2 : Array (Decl α)) : Prop where -/ idx_eq : ∀ idx (h : idx < decls1.size), decls2[idx]'(by omega) = decls1[idx]'h +@[simp] +theorem IsPrefix_push {decls : Array (Decl α)} : IsPrefix decls (decls.push decl) := by + apply IsPrefix.of + · intro idx hidx + simp [hidx, Array.getElem_push] + · simp + /-- If `decls1` is a prefix of `decls2` and we start evaluating `decls2` at an index in bounds of `decls1` we can evaluate at `decls1`. @@ -69,11 +76,12 @@ variable {α : Type} [Hashable α] [DecidableEq α] @[inherit_doc denote.go_eq_of_isPrefix] theorem denote.eq_of_isPrefix (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⟧ + ⟦newAIG, ⟨entry.ref.gate, entry.ref.invert, (by have := entry.ref.hgate; have := hprefix.size_le; omega)⟩, assign⟧ = ⟦entry, assign⟧ := by unfold denote + rw [Bool.bne_left_inj] apply denote.go_eq_of_isPrefix assumption @@ -129,7 +137,7 @@ theorem le_size_of_le_aig_size (aig : AIG α) (input : β aig) (h : x ≤ aig.de @[simp] theorem denote_input_entry (entry : Entrypoint α) {input} {h} : - ⟦(f entry.aig input).aig, ⟨entry.ref.gate, h⟩, assign⟧ + ⟦(f entry.aig input).aig, ⟨entry.ref.gate, entry.ref.invert, h⟩, assign⟧ = ⟦entry, assign⟧ := by apply denote.eq_of_isPrefix @@ -143,10 +151,10 @@ theorem denote_cast_entry (entry : Entrypoint α) {input} {h} : simp [Ref.cast] theorem denote_mem_prefix {aig : AIG α} {input} (h) : - ⟦(f aig input).aig, ⟨start, by apply lt_size_of_lt_aig_size; omega⟩, assign⟧ + ⟦(f aig input).aig, ⟨start, invert, by apply lt_size_of_lt_aig_size; omega⟩, assign⟧ = - ⟦aig, ⟨start, h⟩, assign⟧ := by - rw [denote_input_entry ⟨aig, start, h⟩] + ⟦aig, ⟨start, invert, h⟩, assign⟧ := by + rw [denote_input_entry ⟨aig, start, invert, h⟩] end LawfulOperator diff --git a/src/Std/Sat/AIG/LawfulVecOperator.lean b/src/Std/Sat/AIG/LawfulVecOperator.lean index f0f02301dc..29bc7d0549 100644 --- a/src/Std/Sat/AIG/LawfulVecOperator.lean +++ b/src/Std/Sat/AIG/LawfulVecOperator.lean @@ -54,7 +54,7 @@ theorem le_size_of_le_aig_size (aig : AIG α) (input : β aig len) (h : x ≤ ai @[simp] theorem denote_input_entry (entry : Entrypoint α) {input : β entry.aig len} {h} : - ⟦(f entry.aig input).aig, ⟨entry.ref.gate, h⟩, assign ⟧ + ⟦(f entry.aig input).aig, ⟨entry.ref.gate, entry.ref.invert, h⟩, assign ⟧ = ⟦entry, assign⟧ := by apply denote.eq_of_isPrefix @@ -68,10 +68,10 @@ theorem denote_cast_entry (entry : Entrypoint α) {input : β entry.aig len} {h} simp [Ref.cast] theorem denote_mem_prefix {aig : AIG α} {input : β aig len} (h) : - ⟦(f aig input).aig, ⟨start, by apply lt_size_of_lt_aig_size; omega⟩, assign⟧ + ⟦(f aig input).aig, ⟨start, inv, by apply lt_size_of_lt_aig_size; omega⟩, assign⟧ = - ⟦aig, ⟨start, h⟩, assign⟧ := by - rw [denote_input_entry ⟨aig, start, h⟩] + ⟦aig, ⟨start, inv, h⟩, assign⟧ := by + rw [denote_input_entry ⟨aig, start, inv, h⟩] @[simp] theorem denote_input_vec (s : RefVecEntry α len) {input : β s.aig len} {hcast} : diff --git a/src/Std/Sat/AIG/Lemmas.lean b/src/Std/Sat/AIG/Lemmas.lean index 81d6ac58d2..f50b22c5a7 100644 --- a/src/Std/Sat/AIG/Lemmas.lean +++ b/src/Std/Sat/AIG/Lemmas.lean @@ -27,25 +27,15 @@ theorem Ref.gate_cast {aig1 aig2 : AIG α} (ref : Ref aig1) @[simp] theorem Ref.cast_eq {aig1 aig2 : AIG α} (ref : Ref aig1) (h : aig1.decls.size ≤ aig2.decls.size) : - (ref.cast h) = ⟨ref.gate, by have := ref.hgate; omega⟩ := rfl + (ref.cast h) = ⟨ref.gate, ref.invert, by have := ref.hgate; omega⟩ := rfl @[simp] -theorem Fanin.ref_cast {aig1 aig2 : AIG α} (fanin : Fanin aig1) - (h : aig1.decls.size ≤ aig2.decls.size) : - (fanin.cast h).ref = fanin.ref.cast h := rfl - -@[simp] -theorem Fanin.inv_cast {aig1 aig2 : AIG α} (fanin : Fanin aig1) - (h : aig1.decls.size ≤ aig2.decls.size) : - (fanin.cast h).inv = fanin.inv := rfl - -@[simp] -theorem GateInput.lhs_cast {aig1 aig2 : AIG α} (input : GateInput aig1) +theorem BinaryInput.lhs_cast {aig1 aig2 : AIG α} (input : BinaryInput aig1) (h : aig1.decls.size ≤ aig2.decls.size) : (input.cast h).lhs = input.lhs.cast h := rfl @[simp] -theorem GateInput.rhs_cast {aig1 aig2 : AIG α} (input : GateInput aig1) +theorem BinaryInput.rhs_cast {aig1 aig2 : AIG α} (input : BinaryInput aig1) (h : aig1.decls.size ≤ aig2.decls.size) : (input.cast h).rhs = input.rhs.cast h := rfl @@ -55,6 +45,16 @@ theorem BinaryInput.each_cast {aig1 aig2 : AIG α} (lhs rhs : Ref aig1) BinaryInput.mk (lhs.cast h1) (rhs.cast h2) = (BinaryInput.mk lhs rhs).cast h2 := by simp [BinaryInput.cast] +@[simp] +theorem BinaryInput_invert_lhs {aig : AIG α} (input : BinaryInput aig) (linv rinv : Bool) : + (input.invert linv rinv).lhs = ⟨input.lhs.gate, linv ^^ input.lhs.invert, input.lhs.hgate⟩ := by + simp [BinaryInput.invert, Ref.flip] + +@[simp] +theorem BinaryInput_invert_rhs {aig : AIG α} (input : BinaryInput aig) (linv rinv : Bool) : + (input.invert linv rinv).rhs = ⟨input.rhs.gate, rinv ^^ input.rhs.invert, input.rhs.hgate⟩ := by + simp [BinaryInput.invert, Ref.flip] + @[simp] theorem denote_projected_entry {entry : Entrypoint α} : ⟦entry.aig, entry.ref, assign⟧ = ⟦entry, assign⟧ := by @@ -62,20 +62,43 @@ theorem denote_projected_entry {entry : Entrypoint α} : @[simp] theorem denote_projected_entry' {entry : Entrypoint α} : - ⟦entry.aig, ⟨entry.ref.gate, entry.ref.hgate⟩, assign⟧ = ⟦entry, assign⟧ := by + ⟦entry.aig, ⟨entry.ref.gate, entry.ref.invert, entry.ref.hgate⟩, assign⟧ = ⟦entry, assign⟧ := by cases entry; simp +@[simp] +theorem Ref.denote_flip {aig : AIG α} {ref : Ref aig} {inv : Bool} : + ⟦aig, ref.flip inv, assign⟧ = (⟦aig, ref, assign⟧ ^^ inv) := by + unfold denote + cases ref <;> cases inv <;> simp [Ref.flip] + +@[simp] +theorem Ref.denote_not {aig : AIG α} {ref : Ref aig} : + ⟦aig, ref.not, assign⟧ = !⟦aig, ref, assign⟧ := by + simp [Ref.not] + +@[simp] +theorem denote_not_invert {aig : AIG α} {gate} {inv} {hgate} : + ⟦aig, ⟨gate, !inv, hgate⟩, assign⟧ = !⟦aig, ⟨gate, inv, hgate⟩, assign⟧ := by + unfold denote + simp + +@[simp] +theorem denote_invert_true {aig : AIG α} {gate} {hgate} : + ⟦aig, ⟨gate, true, hgate⟩, assign⟧ = !⟦aig, ⟨gate, false, hgate⟩, assign⟧ := by + unfold denote + simp + /-- `AIG.mkGate` never shrinks the underlying AIG. -/ -theorem mkGate_le_size (aig : AIG α) (input : GateInput aig) : +theorem mkGate_le_size (aig : AIG α) (input : BinaryInput aig) : aig.decls.size ≤ (aig.mkGate input).aig.decls.size := by - simp +arith [mkGate] + simp [mkGate] /-- The AIG produced by `AIG.mkGate` agrees with the input AIG on all indices that are valid for both. -/ -theorem mkGate_decl_eq idx (aig : AIG α) (input : GateInput aig) {h : idx < aig.decls.size} : +theorem mkGate_decl_eq idx (aig : AIG α) (input : BinaryInput aig) {h : idx < aig.decls.size} : have := mkGate_le_size aig input (aig.mkGate input).aig.decls[idx]'(by omega) = aig.decls[idx] := by simp only [mkGate, Array.getElem_push] @@ -83,17 +106,17 @@ theorem mkGate_decl_eq idx (aig : AIG α) (input : GateInput aig) {h : idx < aig · rfl · contradiction -instance : LawfulOperator α GateInput mkGate where +instance : LawfulOperator α BinaryInput mkGate where le_size := mkGate_le_size decl_eq := by intros apply mkGate_decl_eq @[simp] -theorem denote_mkGate {aig : AIG α} {input : GateInput aig} : +theorem denote_mkGate {aig : AIG α} {input : BinaryInput aig} : ⟦aig.mkGate input, assign⟧ = - ((⟦aig, input.lhs.ref, assign⟧ ^^ input.lhs.inv) && (⟦aig, input.rhs.ref, assign⟧ ^^ input.rhs.inv)) := by + (⟦aig, input.lhs, assign⟧ && ⟦aig, input.rhs, assign⟧) := by conv => lhs unfold denote denote.go @@ -107,18 +130,12 @@ theorem denote_mkGate {aig : AIG α} {input : GateInput aig} : · next heq => rw [mkGate, Array.getElem_push_eq] at heq injection heq with heq1 heq2 heq3 heq4 - dsimp only + simp only [← heq1, mkGate, ← heq3, ← heq2, ← heq4, Bool.bne_false, denote] congr 2 - · unfold denote - simp only [heq1] - apply denote.go_eq_of_isPrefix - apply LawfulOperator.isPrefix_aig - · simp [heq3] - · unfold denote - simp only [heq2] - apply denote.go_eq_of_isPrefix - apply LawfulOperator.isPrefix_aig - · simp [heq4] + · apply denote.go_eq_of_isPrefix + simp + · apply denote.go_eq_of_isPrefix + simp /-- `AIG.mkAtom` never shrinks the underlying AIG. @@ -154,7 +171,7 @@ theorem denote_mkAtom {aig : AIG α} : · next heq => rw [mkAtom, Array.getElem_push_eq] at heq injection heq with heq - rw [heq] + simp [heq, mkAtom] · next heq => rw [mkAtom, Array.getElem_push_eq] at heq contradiction @@ -190,7 +207,7 @@ theorem denote_mkConst {aig : AIG α} : ⟦(aig.mkConst val), assign⟧ = val := · next heq => rw [mkConst, Array.getElem_push_eq] at heq injection heq with heq - rw [heq] + simp [heq, mkConst] · next heq => rw [mkConst, Array.getElem_push_eq] at heq contradiction @@ -202,7 +219,7 @@ theorem denote_mkConst {aig : AIG α} : ⟦(aig.mkConst val), assign⟧ = val := If an index contains a `Decl.const` we know how to denote it. -/ theorem denote_idx_const {aig : AIG α} {hstart} (h : aig.decls[start]'hstart = .const b) : - ⟦aig, ⟨start, hstart⟩, assign⟧ = b := by + ⟦aig, ⟨start, invert, hstart⟩, assign⟧ = (b ^^ invert) := by unfold denote denote.go split <;> simp_all @@ -210,7 +227,7 @@ theorem denote_idx_const {aig : AIG α} {hstart} (h : aig.decls[start]'hstart = If an index contains a `Decl.atom` we know how to denote it. -/ theorem denote_idx_atom {aig : AIG α} {hstart} (h : aig.decls[start] = .atom a) : - ⟦aig, ⟨start, hstart⟩, assign⟧ = assign a := by + ⟦aig, ⟨start, invert, hstart⟩, assign⟧ = (assign a ^^ invert) := by unfold denote denote.go split <;> simp_all @@ -218,13 +235,13 @@ theorem denote_idx_atom {aig : AIG α} {hstart} (h : aig.decls[start] = .atom a) If an index contains a `Decl.gate` we know how to denote it. -/ theorem denote_idx_gate {aig : AIG α} {hstart} (h : aig.decls[start] = .gate lhs rhs linv rinv) : - ⟦aig, ⟨start, hstart⟩, assign⟧ + ⟦aig, ⟨start, invert, hstart⟩, assign⟧ = - ( - (⟦aig, ⟨lhs, by have := aig.invariant hstart h; omega⟩, assign⟧ ^^ linv) + (( + (⟦aig, ⟨lhs, linv, by have := aig.invariant hstart h; omega⟩, assign⟧) && - (⟦aig, ⟨rhs, by have := aig.invariant hstart h; omega⟩, assign⟧ ^^ rinv) - ) := by + (⟦aig, ⟨rhs, rinv, by have := aig.invariant hstart h; omega⟩, assign⟧) + ) ^^ invert) := by unfold denote conv => lhs @@ -247,15 +264,15 @@ theorem idx_trichotomy (aig : AIG α) (hstart : start < aig.decls.size) {prop : | .gate lhs rhs linv rinv => apply hgate; assumption theorem denote_idx_trichotomy {aig : AIG α} {hstart : start < aig.decls.size} - (hconst : ∀ b, aig.decls[start]'hstart = .const b → ⟦aig, ⟨start, hstart⟩, assign⟧ = res) - (hatom : ∀ a, aig.decls[start]'hstart = .atom a → ⟦aig, ⟨start, hstart⟩, assign⟧ = res) + (hconst : ∀ b, aig.decls[start]'hstart = .const b → ⟦aig, ⟨start, invert, hstart⟩, assign⟧ = res) + (hatom : ∀ a, aig.decls[start]'hstart = .atom a → ⟦aig, ⟨start, invert, hstart⟩, assign⟧ = res) (hgate : ∀ lhs rhs linv rinv, aig.decls[start]'hstart = .gate lhs rhs linv rinv → - ⟦aig, ⟨start, hstart⟩, assign⟧ = res + ⟦aig, ⟨start, invert, hstart⟩, assign⟧ = res ) : - ⟦aig, ⟨start, hstart⟩, assign⟧ = res := by + ⟦aig, ⟨start, invert, hstart⟩, assign⟧ = res := by apply idx_trichotomy aig hstart · exact hconst · exact hatom @@ -264,32 +281,32 @@ theorem denote_idx_trichotomy {aig : AIG α} {hstart : start < aig.decls.size} theorem mem_def {aig : AIG α} {a : α} : (a ∈ aig) ↔ ((.atom a) ∈ aig.decls) := by simp [Membership.mem, Mem] -theorem denote_congr (assign1 assign2 : α → Bool) (aig : AIG α) (idx : Nat) +theorem denote_congr (assign1 assign2 : α → Bool) (aig : AIG α) (idx : Nat) (invert : Bool) (hidx : idx < aig.decls.size) (h : ∀ a, a ∈ aig → assign1 a = assign2 a) : - ⟦aig, ⟨idx, hidx⟩, assign1⟧ = ⟦aig, ⟨idx, hidx⟩, assign2⟧ := by + ⟦aig, ⟨idx, invert, hidx⟩, assign1⟧ = ⟦aig, ⟨idx, invert, hidx⟩, assign2⟧ := by apply denote_idx_trichotomy · intro b heq simp [denote_idx_const heq] · intro a heq - simp only [denote_idx_atom heq] + simp only [denote_idx_atom heq, Bool.bne_left_inj] apply h - rw [mem_def, ← heq, Array.mem_def] - apply Array.getElem_mem_toList + simp [mem_def, ← heq] · intro lhs rhs linv rinv heq simp only [denote_idx_gate heq] have := aig.invariant hidx heq - rw [denote_congr assign1 assign2 aig lhs (by omega) h] - rw [denote_congr assign1 assign2 aig rhs (by omega) h] + rw [denote_congr assign1 assign2 aig lhs _ (by omega) h] + rw [denote_congr assign1 assign2 aig rhs _ (by omega) h] theorem of_isConstant {aig : AIG α} {assign : α → Bool} {ref : Ref aig} {b : Bool} : aig.isConstant ref b → ⟦aig, ref, assign⟧ = b := by - rcases ref with ⟨gate, hgate⟩ + rcases ref with ⟨gate, invert, hgate⟩ intro h unfold isConstant at h dsimp only at h split at h - · rw [denote_idx_const] - simp_all + · next heq => + rw [denote_idx_const (h := heq)] + cases invert <;> simp_all · contradiction end AIG diff --git a/src/Std/Sat/AIG/RefVec.lean b/src/Std/Sat/AIG/RefVec.lean index ca3b2b907a..3ff1f769a4 100644 --- a/src/Std/Sat/AIG/RefVec.lean +++ b/src/Std/Sat/AIG/RefVec.lean @@ -33,8 +33,8 @@ 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) < aig1.decls.size) - → ∀ {i : Nat} (h : i < len), s.refs[i]'(by have := s.hlen; omega) < aig2.decls.size) : + (∀ {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) : RefVec aig2 len := { s with hrefs := by @@ -58,13 +58,13 @@ def cast {aig1 aig2 : AIG α} (s : RefVec aig1 len) (h : aig1.decls.size ≤ aig 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, by apply hrefs; assumption⟩ + ⟨ref.1, ref.2, by apply hrefs; assumption⟩ @[inline] def push (s : RefVec aig len) (ref : AIG.Ref aig) : RefVec aig (len + 1) := let ⟨refs, hlen, hrefs⟩ := s ⟨ - refs.push ref.gate, + refs.push (ref.gate, ref.invert), by simp [hlen], by intro i hi @@ -75,6 +75,11 @@ def push (s : RefVec aig len) (ref : AIG.Ref aig) : RefVec aig (len + 1) := · apply AIG.Ref.hgate ⟩ +@[simp] +theorem cast_cast {aig1 aig2 aig3 : AIG α} (s : RefVec aig1 len) + (h1 : aig1.decls.size ≤ aig2.decls.size) (h2 : aig2.decls.size ≤ aig3.decls.size) : + (s.cast h1).cast h2 = s.cast (Nat.le_trans h1 h2) := by rfl + @[simp] theorem get_push_ref_eq (s : RefVec aig len) (ref : AIG.Ref aig) : (s.push ref).get len (by omega) = ref := by @@ -95,6 +100,8 @@ theorem get_push_ref_lt (s : RefVec aig len) (ref : AIG.Ref aig) (idx : Nat) cases ref simp only [Ref.mk.injEq] rw [Array.getElem_push_lt] + · simp + · simp [hlen, hidx] @[simp] theorem get_cast {aig1 aig2 : AIG α} (s : RefVec aig1 len) (idx : Nat) (hidx : idx < len) @@ -135,6 +142,9 @@ theorem get_append (lhs : RefVec aig lw) (rhs : RefVec aig rw) (idx : Nat) split · simp [Ref.mk.injEq] rw [Array.getElem_append_left] + · simp + · rw [lhs.hlen] + assumption · simp only [Ref.mk.injEq] rw [Array.getElem_append_right] · simp [lhs.hlen] @@ -162,7 +172,7 @@ theorem get_out_bound (s : RefVec aig len) (idx : Nat) (alt : Ref aig) (hidx : l def countKnown [Inhabited α] (aig : AIG α) (s : RefVec aig len) : Nat := Id.run do let folder acc ref := - let decl := aig.decls[ref]! + let decl := aig.decls[ref.1]! match decl with | .const .. => acc + 1 | _ => acc diff --git a/src/Std/Sat/AIG/RefVecOperator/Map.lean b/src/Std/Sat/AIG/RefVecOperator/Map.lean index 0f60aa90ad..fd7922be31 100644 --- a/src/Std/Sat/AIG/RefVecOperator/Map.lean +++ b/src/Std/Sat/AIG/RefVecOperator/Map.lean @@ -36,7 +36,7 @@ theorem denote_prefix_cast_ref {aig : AIG α} {input1 input2 : Ref aig} instance : LawfulMapOperator α mkNotCached where chainable := by intros - simp only [Ref.gate_cast, denote_mkNotCached] + simp only [Ref.cast_eq, denote_mkNotCached, Bool.not_eq_eq_eq_not, Bool.not_not] rw [LawfulOperator.denote_mem_prefix (f := mkNotCached)] end LawfulMapOperator @@ -156,7 +156,7 @@ theorem go_get_aux {aig : AIG α} (curr : Nat) (hcurr : curr ≤ len) (s : RefVe simp only [Nat.le_refl, get, Ref.cast_eq, Ref.mk.injEq, true_implies] have : curr = len := by omega subst this - rfl + simp termination_by len - curr theorem go_get {aig : AIG α} (curr : Nat) (hcurr : curr ≤ len) (s : RefVec aig curr) @@ -175,12 +175,12 @@ theorem go_denote_mem_prefix {aig : AIG α} (curr : Nat) (hcurr : curr ≤ len) (start : Nat) (hstart) : ⟦ (go aig curr hcurr s input f).aig, - ⟨start, by apply Nat.lt_of_lt_of_le; exact hstart; apply go_le_size⟩, + ⟨start, inv, by apply Nat.lt_of_lt_of_le; exact hstart; apply go_le_size⟩, assign ⟧ = - ⟦aig, ⟨start, hstart⟩, assign⟧ := by - apply denote.eq_of_isPrefix (entry := ⟨aig, start,hstart⟩) + ⟦aig, ⟨start, inv, hstart⟩, assign⟧ := by + apply denote.eq_of_isPrefix (entry := ⟨aig, start, inv, hstart⟩) apply IsPrefix.of · intros apply go_decl_eq diff --git a/src/Std/Sat/AIG/RefVecOperator/Zip.lean b/src/Std/Sat/AIG/RefVecOperator/Zip.lean index a8dd69ae91..d9f4f36d7a 100644 --- a/src/Std/Sat/AIG/RefVecOperator/Zip.lean +++ b/src/Std/Sat/AIG/RefVecOperator/Zip.lean @@ -202,12 +202,12 @@ theorem go_denote_mem_prefix {aig : AIG α} (curr : Nat) (hcurr : curr ≤ len) [chainable : LawfulZipOperator α f] (start : Nat) (hstart) : ⟦ (go aig curr s hcurr lhs rhs f).aig, - ⟨start, by apply Nat.lt_of_lt_of_le; exact hstart; apply go_le_size⟩, + ⟨start, inv, by apply Nat.lt_of_lt_of_le; exact hstart; apply go_le_size⟩, assign ⟧ = - ⟦aig, ⟨start, hstart⟩, assign⟧ := by - apply denote.eq_of_isPrefix (entry := ⟨aig, start,hstart⟩) + ⟦aig, ⟨start, inv, hstart⟩, assign⟧ := by + apply denote.eq_of_isPrefix (entry := ⟨aig, start, inv, hstart⟩) apply IsPrefix.of · intros apply go_decl_eq diff --git a/src/Std/Sat/AIG/Relabel.lean b/src/Std/Sat/AIG/Relabel.lean index ae33a83460..8c082ac585 100644 --- a/src/Std/Sat/AIG/Relabel.lean +++ b/src/Std/Sat/AIG/Relabel.lean @@ -98,9 +98,9 @@ theorem relabel_gate {aig : AIG α} {r : α → β} {hidx : idx < (relabel r aig @[simp] theorem denote_relabel (aig : AIG α) (r : α → β) (start : Nat) {hidx} (assign : β → Bool) : - ⟦aig.relabel r, ⟨start, hidx⟩, assign⟧ + ⟦aig.relabel r, ⟨start, invert, hidx⟩, assign⟧ = - ⟦aig, ⟨start, by rw [← relabel_size_eq_size (r := r)]; omega⟩, (assign ∘ r)⟧ := by + ⟦aig, ⟨start, invert, by rw [← relabel_size_eq_size (r := r)]; omega⟩, (assign ∘ r)⟧ := by apply denote_idx_trichotomy · intro b heq1 have heq2 := relabel_const heq1 @@ -121,14 +121,14 @@ theorem denote_relabel (aig : AIG α) (r : α → β) (start : Nat) {hidx} rw [denote_relabel aig r rhs assign] theorem unsat_relabel {aig : AIG α} (r : α → β) {hidx} : - aig.UnsatAt idx hidx → (aig.relabel r).UnsatAt idx (by simp [hidx]) := by + aig.UnsatAt idx invert hidx → (aig.relabel r).UnsatAt idx invert (by simp [hidx]) := by intro h assign specialize h (assign ∘ r) simp [h] theorem relabel_unsat_iff [Nonempty α] {aig : AIG α} {r : α → β} {hidx1} {hidx2} (hinj : ∀ x y, x ∈ aig → y ∈ aig → r x = r y → x = y) : - (aig.relabel r).UnsatAt idx hidx1 ↔ aig.UnsatAt idx hidx2 := by + (aig.relabel r).UnsatAt idx invert hidx1 ↔ aig.UnsatAt idx invert hidx2 := by constructor · intro h assign let g : β → α := fun b => diff --git a/src/Std/Sat/AIG/RelabelNat.lean b/src/Std/Sat/AIG/RelabelNat.lean index bc78f4cc57..8d66f738e4 100644 --- a/src/Std/Sat/AIG/RelabelNat.lean +++ b/src/Std/Sat/AIG/RelabelNat.lean @@ -329,7 +329,7 @@ theorem relabelNat_size_eq_size {aig : AIG α} : aig.relabelNat.decls.size = aig `relabelNat` preserves unsatisfiablility. -/ theorem relabelNat_unsat_iff [Nonempty α] {aig : AIG α} {hidx1} {hidx2} : - (aig.relabelNat).UnsatAt idx hidx1 ↔ aig.UnsatAt idx hidx2 := by + (aig.relabelNat).UnsatAt idx invert hidx1 ↔ aig.UnsatAt idx invert hidx2 := by dsimp only [relabelNat, relabelNat'] rw [relabel_unsat_iff] intro x y hx hy heq diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Add.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Add.lean index 429c30a85c..6032ccd160 100644 --- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Add.lean +++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Add.lean @@ -197,6 +197,8 @@ theorem go_le_size (aig : AIG α) (curr : Nat) (hcurr : curr ≤ w) (cin : AIG.R dsimp only split · refine Nat.le_trans ?_ (by apply go_le_size) + unfold mkFullAdder + dsimp only apply AIG.LawfulOperator.le_size_of_le_aig_size (f := mkFullAdderCarry) apply AIG.LawfulOperator.le_size (f := mkFullAdderOut) · simp diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Const.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Const.lean index bbff7b66ad..4ffd685bdf 100644 --- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Const.lean +++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Const.lean @@ -64,12 +64,12 @@ theorem go_denote_mem_prefix (aig : AIG α) (idx : Nat) (hidx) (s : AIG.RefVec aig idx) (c : BitVec w) (start : Nat) (hstart) : ⟦ (go aig c idx s hidx).aig, - ⟨start, by apply Nat.lt_of_lt_of_le; exact hstart; apply go_le_size⟩, + ⟨start, inv, by apply Nat.lt_of_lt_of_le; exact hstart; apply go_le_size⟩, assign ⟧ = - ⟦aig, ⟨start, hstart⟩, assign⟧ := by - apply denote.eq_of_isPrefix (entry := ⟨aig, start,hstart⟩) + ⟦aig, ⟨start, inv, hstart⟩, assign⟧ := by + apply denote.eq_of_isPrefix (entry := ⟨aig, start, inv, hstart⟩) apply IsPrefix.of · intros apply go_decl_eq diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Expr.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Expr.lean index 099483892a..8a960a50ef 100644 --- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Expr.lean +++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Expr.lean @@ -42,12 +42,12 @@ theorem go_denote_mem_prefix (aig : AIG BVBit) (expr : BVExpr w) (assign : Assig (hstart) : ⟦ (go aig expr).val.aig, - ⟨start, by apply Nat.lt_of_lt_of_le; exact hstart; apply (go aig expr).property⟩, + ⟨start, inv, by apply Nat.lt_of_lt_of_le; exact hstart; apply (go aig expr).property⟩, assign.toAIGAssignment ⟧ = - ⟦aig, ⟨start, hstart⟩, assign.toAIGAssignment⟧ := by - apply denote.eq_of_isPrefix (entry := ⟨aig, start,hstart⟩) + ⟦aig, ⟨start, inv, hstart⟩, assign.toAIGAssignment⟧ := by + apply denote.eq_of_isPrefix (entry := ⟨aig, start, inv, hstart⟩) apply IsPrefix.of · intros apply go_decl_eq diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Add.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Add.lean index 77b1485094..3998f3a2b3 100644 --- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Add.lean +++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Add.lean @@ -63,11 +63,11 @@ theorem mkFullAdder_denote_mem_prefix (aig : AIG α) (input : FullAdderInput aig (hstart) : ⟦ (mkFullAdder aig input).aig, - ⟨start, Nat.lt_of_lt_of_le hstart (FullAdderOutput.hle _)⟩, + ⟨start, inv, Nat.lt_of_lt_of_le hstart (FullAdderOutput.hle _)⟩, assign ⟧ = - ⟦aig, ⟨start, hstart⟩, assign⟧ := by + ⟦aig, ⟨start, inv, hstart⟩, assign⟧ := by unfold mkFullAdder dsimp only rw [AIG.LawfulOperator.denote_mem_prefix (f := mkFullAdderCarry)] @@ -77,12 +77,12 @@ theorem go_denote_mem_prefix (aig : AIG α) (curr : Nat) (hcurr : curr ≤ w) (c (s : AIG.RefVec aig curr) (lhs rhs : AIG.RefVec aig w) (start : Nat) (hstart) : ⟦ (go aig lhs rhs curr hcurr cin s).aig, - ⟨start, by apply Nat.lt_of_lt_of_le; exact hstart; apply go_le_size⟩, + ⟨start, inv, by apply Nat.lt_of_lt_of_le; exact hstart; apply go_le_size⟩, assign ⟧ = - ⟦aig, ⟨start, hstart⟩, assign⟧ := by - apply denote.eq_of_isPrefix (entry := ⟨aig, start,hstart⟩) + ⟦aig, ⟨start, inv, hstart⟩, assign⟧ := by + apply denote.eq_of_isPrefix (entry := ⟨aig, start, inv, hstart⟩) apply IsPrefix.of · intros apply go_decl_eq diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Neg.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Neg.lean index e05ec1ac91..fc445e2d5c 100644 --- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Neg.lean +++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Neg.lean @@ -39,9 +39,8 @@ theorem denote_blastNeg (aig : AIG α) (value : BitVec w) (target : RefVec aig w rw [denote_blastAdd] · intro idx hidx rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastConst)] - · simp only [RefVec.get_cast, Ref.gate_cast, BitVec.getLsbD_not, hidx, decide_true, - Bool.true_and] - rw [denote_blastNot, htarget] + · simp only [RefVec.get_cast, Ref.cast_eq, hidx, BitVec.getLsbD_eq_getElem, BitVec.getElem_not] + rw [denote_blastNot, htarget, BitVec.getLsbD_eq_getElem] · simp [Ref.hgate] · simp diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/ShiftLeft.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/ShiftLeft.lean index e7145d2efa..dceb5be1a6 100644 --- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/ShiftLeft.lean +++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/ShiftLeft.lean @@ -69,12 +69,12 @@ theorem go_denote_mem_prefix (aig : AIG α) (distance : Nat) (input : AIG.RefVec (curr : Nat) (hcurr : curr ≤ w) (s : AIG.RefVec aig curr) (start : Nat) (hstart) : ⟦ (go aig input distance curr hcurr s).aig, - ⟨start, by apply Nat.lt_of_lt_of_le; exact hstart; apply go_le_size⟩, + ⟨start, inv, by apply Nat.lt_of_lt_of_le; exact hstart; apply go_le_size⟩, assign ⟧ = - ⟦aig, ⟨start, hstart⟩, assign⟧ := by - apply denote.eq_of_isPrefix (entry := ⟨aig, start,hstart⟩) + ⟦aig, ⟨start, inv, hstart⟩, assign⟧ := by + apply denote.eq_of_isPrefix (entry := ⟨aig, start, inv, hstart⟩) apply IsPrefix.of · intros apply go_decl_eq diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/ShiftRight.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/ShiftRight.lean index 807103acf0..8b6202681b 100644 --- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/ShiftRight.lean +++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/ShiftRight.lean @@ -69,12 +69,12 @@ theorem go_denote_mem_prefix (aig : AIG α) (distance : Nat) (input : AIG.RefVec (curr : Nat) (hcurr : curr ≤ w) (s : AIG.RefVec aig curr) (start : Nat) (hstart) : ⟦ (go aig input distance curr hcurr s).aig, - ⟨start, by apply Nat.lt_of_lt_of_le; exact hstart; apply go_le_size⟩, + ⟨start, inv, by apply Nat.lt_of_lt_of_le; exact hstart; apply go_le_size⟩, assign ⟧ = - ⟦aig, ⟨start, hstart⟩, assign⟧ := by - apply denote.eq_of_isPrefix (entry := ⟨aig, start,hstart⟩) + ⟦aig, ⟨start, inv, hstart⟩, assign⟧ := by + apply denote.eq_of_isPrefix (entry := ⟨aig, start, inv, hstart⟩) apply IsPrefix.of · intros apply go_decl_eq diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Udiv.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Udiv.lean index d939f530c3..983792eff1 100644 --- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Udiv.lean +++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Udiv.lean @@ -61,12 +61,12 @@ theorem blastDivSubtractShift_denote_mem_prefix (aig : AIG α) (falseRef trueRef (n d q r : AIG.RefVec aig w) (wn wr : Nat) (start : Nat) (hstart) : ⟦ (blastDivSubtractShift aig falseRef trueRef n d wn wr q r).aig, - ⟨start, by apply Nat.lt_of_lt_of_le; exact hstart; apply blastDivSubtractShift_le_size⟩, + ⟨start, inv, by apply Nat.lt_of_lt_of_le; exact hstart; apply blastDivSubtractShift_le_size⟩, assign ⟧ = - ⟦aig, ⟨start, hstart⟩, assign⟧ := by - apply denote.eq_of_isPrefix (entry := ⟨aig, start,hstart⟩) + ⟦aig, ⟨start, inv, hstart⟩, assign⟧ := by + apply denote.eq_of_isPrefix (entry := ⟨aig, start, inv, hstart⟩) apply IsPrefix.of · intros apply blastDivSubtractShift_decl_eq @@ -95,58 +95,60 @@ theorem denote_blastDivSubtractShift_q (aig : AIG α) (assign : α → Bool) (lh unfold blastDivSubtractShift BitVec.divSubtractShift dsimp only rw [AIG.LawfulVecOperator.denote_mem_prefix (f := AIG.RefVec.ite)] - . simp only [RefVec.get_cast, Ref.gate_cast] + . simp only [Ref.cast_eq, RefVec.cast_cast, RefVec.get_cast] rw [AIG.RefVec.denote_ite] - rw [BVPred.mkUlt_denote_eq (lhs := rbv.shiftConcat (lhs.getLsbD (wn - 1))) (rhs := rhs)] - · split - · next hdiscr => - rw [← Normalize.BitVec.lt_ult] at hdiscr - simp only [Ref.cast_eq, id_eq, Int.reduceNeg, RefVec.get_cast, hdiscr, ↓reduceIte] - rw [AIG.LawfulOperator.denote_mem_prefix (f := BVPred.mkUlt)] + conv => + rhs + rw [apply_ite (f := BitVec.DivModState.q)] + rw [apply_ite (f := (BitVec.getLsbD · idx))] + apply ite_congr + · rw [BVPred.mkUlt_denote_eq (assign := assign) (lhs := rbv.shiftConcat (lhs.getLsbD (wn - 1))) (rhs := rhs)] + · simp [Std.Tactic.BVDecide.Normalize.BitVec.lt_ult] + · intro idx hidx + simp only [RefVec.get_cast, Ref.cast_eq] rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastSub)] rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftConcat)] + rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftConcat)] rw [denote_blastShiftConcat_eq_shiftConcat] - · intro idx hidx - rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftConcat)] - · simp [hq] - · simp [Ref.hgate] - · rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftConcat)] + · simp [hr] + · rw [BVPred.denote_getD_eq_getLsbD] + · simp [hleft] · simp [hfalse] - · simp [Ref.hgate] - · next hdiscr => - rw [← Normalize.BitVec.lt_ult] at hdiscr - simp only [Ref.cast_eq, id_eq, Int.reduceNeg, RefVec.get_cast, hdiscr, ↓reduceIte] - rw [AIG.LawfulOperator.denote_mem_prefix (f := BVPred.mkUlt)] + · intro idx hidx + simp only [RefVec.get_cast, Ref.cast_eq] rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastSub)] - rw [denote_blastShiftConcat_eq_shiftConcat] - · intro idx hidx - rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftConcat)] - rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftConcat)] - · simp [hq] - · simp [Ref.hgate] - · rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftConcat)] - rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftConcat)] - · simp [htrue] - · simp [Ref.hgate] - · intro idx hidx + rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftConcat)] + rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftConcat)] + rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftConcat)] + · simp [hright] + · simp [Ref.hgate] + · intro h + simp only [RefVec.get_cast, Ref.cast_eq] + rw [AIG.LawfulOperator.denote_mem_prefix (f := BVPred.mkUlt)] rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastSub)] rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftConcat)] - rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftConcat)] - . simp only [Ref.cast_eq, id_eq, Int.reduceNeg, RefVec.get_cast] - rw [denote_blastShiftConcat_eq_shiftConcat] - . simp [hr] - . dsimp only - rw [BVPred.denote_getD_eq_getLsbD] - · exact hleft - · exact hfalse - . simp [Ref.hgate] - · intro idx hidx + rw [denote_blastShiftConcat_eq_shiftConcat] + · intro idx hidx + rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftConcat)] + · simp [hq] + · simp [Ref.hgate] + · rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftConcat)] + · simp [hfalse] + · simp [Ref.hgate] + · intro h + simp only [RefVec.get_cast, Ref.cast_eq] + rw [AIG.LawfulOperator.denote_mem_prefix (f := BVPred.mkUlt)] rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastSub)] - rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftConcat)] - rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftConcat)] - rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftConcat)] - . simp [hright] - . simp [Ref.hgate] + rw [denote_blastShiftConcat_eq_shiftConcat] + · intro idx hidx + rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftConcat)] + rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftConcat)] + · simp [hq] + · simp [Ref.hgate] + · rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftConcat)] + rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftConcat)] + · simp [htrue] + · simp [Ref.hgate] . simp [Ref.hgate] theorem denote_blastDivSubtractShift_r (aig : AIG α) (assign : α → Bool) (lhs rhs : BitVec w) @@ -378,12 +380,12 @@ theorem go_denote_mem_prefix (aig : AIG α) (curr : Nat) (falseRef trueRef : AIG (n d q r : AIG.RefVec aig w) (wn wr : Nat) (start : Nat) (hstart) : ⟦ (go aig curr falseRef trueRef n d wn wr q r).aig, - ⟨start, by apply Nat.lt_of_lt_of_le; exact hstart; apply go_le_size⟩, + ⟨start, inv, by apply Nat.lt_of_lt_of_le; exact hstart; apply go_le_size⟩, assign ⟧ = - ⟦aig, ⟨start, hstart⟩, assign⟧ := by - apply denote.eq_of_isPrefix (entry := ⟨aig, start,hstart⟩) + ⟦aig, ⟨start, inv, hstart⟩, assign⟧ := by + apply denote.eq_of_isPrefix (entry := ⟨aig, start, inv, hstart⟩) apply IsPrefix.of · intros apply go_decl_eq 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 8ea81d4847..8fdafbee0f 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 @@ -26,7 +26,7 @@ theorem mkUlt_denote_eq (aig : AIG α) (lhs rhs : BitVec w) (input : BinaryRefVe (assign : α → Bool) (hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, input.lhs.get idx hidx, assign⟧ = lhs.getLsbD idx) (hright : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, input.rhs.get idx hidx, assign⟧ = rhs.getLsbD idx) : - ⟦(mkUlt aig input).aig, (mkUlt aig input).ref, assign⟧ = BitVec.ult lhs rhs := by + ⟦mkUlt aig input, assign⟧ = BitVec.ult lhs rhs := by rw [BitVec.ult_eq_not_carry] unfold mkUlt simp only [denote_projected_entry, denote_mkNotCached, denote_projected_entry'] @@ -42,11 +42,8 @@ theorem mkUlt_denote_eq (aig : AIG α) (lhs rhs : BitVec w) (input : BinaryRefVe · dsimp only intro idx hidx rw [AIG.LawfulOperator.denote_mem_prefix (f := AIG.mkConstCached)] - · simp only [RefVec.get_cast, Ref.gate_cast, BitVec.getLsbD_not, hidx, decide_true, - Bool.true_and] - rw [BVExpr.bitblast.denote_blastNot] - congr 1 - apply hright + · simp only [RefVec.get_cast, Ref.cast_eq, hidx, BitVec.getLsbD_eq_getElem, BitVec.getElem_not] + rw [BVExpr.bitblast.denote_blastNot, hright, BitVec.getLsbD_eq_getElem] · simp [Ref.hgate] end BVPred diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/ZeroExtend.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/ZeroExtend.lean index 1e38916934..c148dd8a20 100644 --- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/ZeroExtend.lean +++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/ZeroExtend.lean @@ -69,12 +69,12 @@ theorem go_denote_mem_prefix (aig : AIG α) (w : Nat) (input : AIG.RefVec aig w) (hcurr : curr ≤ newWidth) (s : AIG.RefVec aig curr) (start : Nat) (hstart) : ⟦ (go aig w input newWidth curr hcurr s).aig, - ⟨start, by apply Nat.lt_of_lt_of_le; exact hstart; apply go_le_size⟩, + ⟨start, inv, by apply Nat.lt_of_lt_of_le; exact hstart; apply go_le_size⟩, assign ⟧ = - ⟦aig, ⟨start, hstart⟩, assign⟧ := by - apply denote.eq_of_isPrefix (entry := ⟨aig, start,hstart⟩) + ⟦aig, ⟨start, inv, hstart⟩, assign⟧ := by + apply denote.eq_of_isPrefix (entry := ⟨aig, start, inv, hstart⟩) apply IsPrefix.of · intros apply go_decl_eq diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Var.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Var.lean index 66cdb77688..dc8bd5e0b0 100644 --- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Var.lean +++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Var.lean @@ -62,12 +62,12 @@ theorem go_denote_mem_prefix (aig : AIG BVBit) (idx : Nat) (hidx) (s : AIG.RefVe (a : Nat) (start : Nat) (hstart) : ⟦ (go aig w a idx s hidx).aig, - ⟨start, by apply Nat.lt_of_lt_of_le; exact hstart; apply go_le_size⟩, + ⟨start, inv, by apply Nat.lt_of_lt_of_le; exact hstart; apply go_le_size⟩, assign ⟧ = - ⟦aig, ⟨start, hstart⟩, assign⟧ := by - apply denote.eq_of_isPrefix (entry := ⟨aig, start,hstart⟩) + ⟦aig, ⟨start, inv, hstart⟩, assign⟧ := by + apply denote.eq_of_isPrefix (entry := ⟨aig, start, inv, hstart⟩) apply IsPrefix.of · intros apply go_decl_eq diff --git a/src/Std/Tactic/BVDecide/Bitblast/BoolExpr/Circuit.lean b/src/Std/Tactic/BVDecide/Bitblast/BoolExpr/Circuit.lean index 6edda27913..6dce59215f 100644 --- a/src/Std/Tactic/BVDecide/Bitblast/BoolExpr/Circuit.lean +++ b/src/Std/Tactic/BVDecide/Bitblast/BoolExpr/Circuit.lean @@ -141,17 +141,19 @@ theorem go_isPrefix_aig {aig : AIG β} : theorem go_denote_mem_prefix : ⟦ (go aig expr atomHandler).val.aig, - ⟨start, by apply Nat.lt_of_lt_of_le; exact hstart; apply go_le_size⟩, + ⟨start, inv, by apply Nat.lt_of_lt_of_le; exact hstart; apply go_le_size⟩, assign ⟧ = - ⟦aig, ⟨start, hstart⟩, assign⟧ := by - apply denote.eq_of_isPrefix (entry := ⟨aig, start,hstart⟩) + ⟦aig, ⟨start, inv, hstart⟩, assign⟧ := by + apply denote.eq_of_isPrefix (entry := ⟨aig, start, inv, hstart⟩) apply go_isPrefix_aig @[simp] theorem go_denote_entry (entry : Entrypoint β) {h} : - ⟦(go entry.aig expr atomHandler).val.aig, ⟨entry.ref.gate, h⟩, assign⟧ = ⟦entry, assign⟧ := by + ⟦(go entry.aig expr atomHandler).val.aig, ⟨entry.ref.gate, entry.ref.invert, h⟩, assign⟧ + = + ⟦entry, assign⟧ := by apply denote.eq_of_isPrefix apply ofBoolExprCached.go_isPrefix_aig diff --git a/tests/lean/run/bv_counterexample.lean b/tests/lean/run/bv_counterexample.lean index 445235db68..c3081bd7ea 100644 --- a/tests/lean/run/bv_counterexample.lean +++ b/tests/lean/run/bv_counterexample.lean @@ -12,7 +12,7 @@ example (x : BitVec 64) : x < x + 1 := by /-- error: The prover found a counterexample, consider the following assignment: -x = 511#64 +x = 0#64 -/ #guard_msgs in example (x : BitVec 64) (h : x < 512) : x ^^^ x ≠ 0 := by