diff --git a/src/Init/Data/Array/Lemmas.lean b/src/Init/Data/Array/Lemmas.lean index 5f2ca41701..133f15bce6 100644 --- a/src/Init/Data/Array/Lemmas.lean +++ b/src/Init/Data/Array/Lemmas.lean @@ -335,6 +335,13 @@ theorem mem_data {a : α} {l : Array α} : a ∈ l.data ↔ a ∈ l := (mem_def theorem not_mem_nil (a : α) : ¬ a ∈ #[] := nofun +theorem getElem_of_mem {a : α} {as : Array α} : + a ∈ as → (∃ (n : Nat) (h : n < as.size), as[n]'h = a) := by + intro ha + rcases List.getElem_of_mem ha.val with ⟨i, hbound, hi⟩ + exists i + exists hbound + /-- # get lemmas -/ theorem lt_of_getElem {x : α} {a : Array α} {idx : Nat} {hidx : idx < a.size} (_ : a[idx] = x) : diff --git a/src/Std/Sat.lean b/src/Std/Sat.lean index 0009cdfd42..e7119caa12 100644 --- a/src/Std/Sat.lean +++ b/src/Std/Sat.lean @@ -4,4 +4,5 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Henrik Böving -/ prelude +import Std.Sat.AIG import Std.Sat.CNF diff --git a/src/Std/Sat/AIG.lean b/src/Std/Sat/AIG.lean new file mode 100644 index 0000000000..f835d56631 --- /dev/null +++ b/src/Std/Sat/AIG.lean @@ -0,0 +1,19 @@ +/- +Copyright (c) 2024 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Henrik Böving +-/ +import Std.Sat.AIG.Basic +import Std.Sat.AIG.LawfulOperator +import Std.Sat.AIG.Lemmas +import Std.Sat.AIG.Cached +import Std.Sat.AIG.CachedLemmas +import Std.Sat.AIG.CachedGates +import Std.Sat.AIG.CachedGatesLemmas +import Std.Sat.AIG.CNF +import Std.Sat.AIG.Relabel +import Std.Sat.AIG.RelabelNat +import Std.Sat.AIG.RefVec +import Std.Sat.AIG.RefVecOperator +import Std.Sat.AIG.LawfulVecOperator +import Std.Sat.AIG.If diff --git a/src/Std/Sat/AIG/Basic.lean b/src/Std/Sat/AIG/Basic.lean new file mode 100644 index 0000000000..2a94ee87e4 --- /dev/null +++ b/src/Std/Sat/AIG/Basic.lean @@ -0,0 +1,510 @@ +/- +Copyright (c) 2024 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Henrik Böving +-/ +import Std.Data.HashMap +import Std.Data.HashSet + +namespace Std +namespace Sat + +/-! +This module contains the basic definitions for an AIG (And Inverter Graph) in the style of AIGNET, +as described in https://arxiv.org/pdf/1304.7861.pdf section 3. It consists of an AIG definition, +a description of its semantics and basic operations to construct nodes in the AIG. +-/ + +variable {α : Type} [Hashable α] [DecidableEq α] + +namespace AIG + +/-- +A circuit node. These are not recursive but instead contain indices into an `AIG`, with inputs indexed by `α`. +-/ +inductive Decl (α : Type) where + /-- + A node with a constant output value. + -/ + | const (b : Bool) + /-- + An input node to the circuit. + -/ + | atom (idx : α) + /-- + An AIG gate with configurable input nodes and polarity. `l` and `r` are the + input node indices while `linv` and `rinv` say whether there is an inverter on + the left and right inputs, respectively. + -/ + | gate (l r : Nat) (linv rinv : Bool) + deriving Hashable, Repr, DecidableEq, Inhabited + + +/-- +`Cache.WF xs` is a predicate asserting that a `cache : HashMap (Decl α) Nat` is a valid lookup +cache for `xs : Array (Decl α)`, that is, whenever `cache.find? decl` returns an index into +`xs : Array Decl`, `xs[index] = decl`. Note that this predicate does not force the cache to be +complete, if there is no entry in the cache for some node, it can still exist in the AIG. +-/ +inductive Cache.WF : Array (Decl α) → HashMap (Decl α) Nat → Prop where + /-- + An empty `Cache` is valid for any `Array Decl` as it never has a hit. + -/ + | empty : WF decls {} + /-- + Given a `cache`, valid with respect to some `decls`, we can extend the `decls` without + extending the cache and remain valid. + -/ + | push_id (h : WF decls cache) : WF (decls.push decl) cache + /-- + Given a `cache`, valid with respect to some `decls`, we can extend the `decls` + and the `cache` at the same time with the same values and remain valid. + -/ + | push_cache (h : WF decls cache) : WF (decls.push decl) (cache.insert decl decls.size) + +/-- +A cache for reusing elements from `decls` if they are available. +-/ +def Cache (α : Type) [DecidableEq α] [Hashable α] (decls : Array (Decl α)) := + { map : HashMap (Decl α) Nat // Cache.WF decls map } + +/-- +Create an empty `Cache`, valid with respect to any `Array Decl`. +-/ +@[irreducible] +def Cache.empty (decls : Array (Decl α)) : Cache α decls := ⟨{}, WF.empty⟩ + +@[inherit_doc Cache.WF.push_id, irreducible] +def Cache.noUpdate (cache : Cache α decls) : Cache α (decls.push decl) := + ⟨cache.val, Cache.WF.push_id cache.property⟩ + +/- +We require the `decls` as an explicit argument because we use `decls.size` so accidentally mutating +`decls` before calling `Cache.insert` will destroy `decl` linearity. +-/ +@[inherit_doc Cache.WF.push_cache, irreducible] +def Cache.insert (decls : Array (Decl α)) (cache : Cache α decls) (decl : Decl α) : + Cache α (decls.push decl) := + ⟨cache.val.insert decl decls.size, Cache.WF.push_cache cache.property⟩ + +/-- +Contains the index of `decl` in `decls` along with a proof that the index is indeed correct. +-/ +structure CacheHit (decls : Array (Decl α)) (decl : Decl α) where + idx : Nat + hbound : idx < decls.size + hvalid : decls[idx]'hbound = decl + +/-- +For a `c : Cache α decls`, any index `idx` that is a cache hit for some `decl` is within bounds of `decls` (i.e. `idx < decls.size`). +-/ +theorem Cache.get?_bounds {decls : Array (Decl α)} {idx : Nat} (c : Cache α decls) (decl : Decl α) + (hfound : c.val[decl]? = some idx) : + idx < decls.size := by + rcases c with ⟨cache, hcache⟩ + induction hcache with + | empty => simp at hfound + | push_id wf ih => + specialize ih hfound + simp + omega + | @push_cache _ _ decl' wf ih => + simp only [HashMap.getElem?_insert, beq_iff_eq] at hfound + split at hfound <;> rename_i h + · subst h + simp_all + · specialize ih hfound + simp + omega + +/-- +If `Cache.get? decl` returns `some i` then `decls[i] = decl` holds. +-/ +theorem Cache.get?_property {decls : Array (Decl α)} {idx : Nat} (c : Cache α decls) (decl : Decl α) + (hfound : c.val[decl]? = some idx) : + decls[idx]'(Cache.get?_bounds c decl hfound) = decl := by + rcases c with ⟨cache, hcache⟩ + induction hcache generalizing decl with + | empty => simp at hfound + | push_id wf ih => + rw [Array.get_push] + split + . apply ih + simp [hfound] + . next hbounds => + exfalso + apply hbounds + specialize ih _ hfound + apply Array.lt_of_getElem + assumption + | push_cache wf ih => + rename_i decl' + rw [Array.get_push] + split + . simp only [HashMap.getElem?_insert] at hfound + match heq : decl == decl' with + | true => + simp only [beq_iff_eq] at heq + simp [heq] at hfound + omega + | false => + apply ih + simpa [BEq.symm_false heq] using hfound + . next hbounds => + simp only [HashMap.getElem?_insert] at hfound + match heq : decl == decl' with + | true => + apply Eq.symm + simpa using heq + | false => + exfalso + apply hbounds + simp only [BEq.symm_false heq, cond_false] at hfound + specialize ih _ hfound + apply Array.lt_of_getElem + assumption + +/-- +Lookup a `Decl` in a `Cache`. +-/ +opaque Cache.get? (cache : Cache α decls) (decl : Decl α) : Option (CacheHit decls decl) := + /- + This function is marked as `opaque` to make sure it never, ever gets unfolded anywhere. + Unfolding it will often cause `HashMap.find?` to be symbolically evaluated by reducing + it either in `whnf` or in the kernel. This causes *huge* performance issues in practice. + The function can still be fully verified as all the proofs we need are in `CacheHit`. + -/ + match hfound : cache.val[decl]? with + | some hit => + some ⟨hit, Cache.get?_bounds _ _ hfound, Cache.get?_property _ _ hfound⟩ + | none => none + +/-- +An `Array Decl` is a Direct Acyclic Graph (DAG) if a gate at index `i` only points to nodes with index lower than `i`. +-/ +def IsDAG (α : Type) (decls : Array (Decl α)) : Prop := + ∀ {i lhs rhs linv rinv} (h : i < decls.size), + decls[i] = .gate lhs rhs linv rinv → lhs < i ∧ rhs < i + +/-- +The empty array is a DAG. +-/ +theorem IsDAG.empty {α : Type} : IsDAG α #[] := by + intro i lhs rhs linv rinv h + simp only [Array.size_toArray, List.length_nil] at h + omega + +end AIG + +/-- +An And Inverter Graph together with a cache for subterm sharing. +-/ +structure AIG (α : Type) [DecidableEq α] [Hashable α] where + /-- + The circuit itself as an `Array Decl` whose members have indices into said array. + -/ + decls : Array (AIG.Decl α) + /-- + The `Decl` cache, valid with respect to `decls`. + -/ + cache : AIG.Cache α decls + /-- + In order to be a valid AIG, `decls` must form a DAG. + -/ + invariant : AIG.IsDAG α decls + +namespace AIG + +/-- +An `AIG` with an empty AIG and cache. +-/ +def empty : AIG α := { decls := #[], cache := Cache.empty #[], invariant := IsDAG.empty } + +/-- +The atom `a` occurs in `aig`. +-/ +def Mem (a : α) (aig : AIG α) : Prop := (.atom a) ∈ aig.decls + +instance : Membership α (AIG α) where + mem := Mem + +/-- +A reference to a node within an AIG. This is the `AIG` analog of `Bool`. +-/ +structure Ref (aig : AIG α) where + gate : Nat + 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) : + Ref aig2 := + { ref with hgate := by have := ref.hgate; omega } + +/-- +A pair of `Ref`s, useful for `LawfulOperator`s that act on two `Ref`s at a time. +-/ +structure BinaryInput (aig : AIG α) where + lhs : Ref aig + rhs : Ref aig + +/-- +The `Ref.cast` equivalent for `BinaryInput`. +-/ +@[inline] +def BinaryInput.cast {aig1 aig2 : AIG α} (input : BinaryInput aig1) + (h : aig1.decls.size ≤ aig2.decls.size) : + BinaryInput aig2 := + { input with lhs := input.lhs.cast h, rhs := input.rhs.cast h } + +/-- +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. +-/ +structure TernaryInput (aig : AIG α) where + discr : Ref aig + lhs : Ref aig + rhs : Ref aig + +/-- +The `Ref.cast` equivalent for `TernaryInput`. +-/ +@[inline] +def TernaryInput.cast {aig1 aig2 : AIG α} (input : TernaryInput aig1) + (h : aig1.decls.size ≤ aig2.decls.size) : + TernaryInput aig2 := + { input with discr := input.discr.cast h, lhs := input.lhs.cast h, rhs := input.rhs.cast h } + +/-- +An entrypoint into an `AIG`. This can be used to evaluate a circuit, starting at a certain node, +with `AIG.denote` or to construct bigger circuits on top of this specific node. +-/ +structure Entrypoint (α : Type) [DecidableEq α] [Hashable α] where + /-- + The AIG that we are in. + -/ + aig : AIG α + /-- + The reference to the node in `aig` that this `Entrypoint` targets. + -/ + ref : Ref aig + +/-- +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 (dag, s) := go "" decls hinv idx h |>.run .empty + 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 + let fidx : Fin decls.size := Fin.mk idx hidx + if (← get).contains fidx then + return acc + modify (fun s ↦ s.insert fidx) + match elem : decls[idx] with + | Decl.const _ => return acc + | Decl.atom _ => return acc + | Decl.gate lidx ridx linv rinv => + let curr := s!"{idx} -> {lidx}{invEdgeStyle linv}; {idx} -> {ridx}{invEdgeStyle rinv};" + let hlr := hinv hidx elem + let laig ← go (acc ++ curr) decls hinv lidx (by omega) + go laig decls hinv ridx (by omega) + invEdgeStyle (isInv : Bool) : String := + if isInv then " [color=red]" else " [color=blue]" + toGraphvizString {α : Type} [DecidableEq α] [ToString α] [Hashable α] (decls : Array (Decl α)) + (idx : Fin decls.size) : String := + match decls[idx] with + | Decl.const b => s!"{idx} [label=\"{b}\", shape=box];" + | Decl.atom i => s!"{idx} [label=\"{i}\", shape=doublecircle];" + | Decl.gate _ _ _ _ => s!"{idx} [label=\"{idx} ∧\",shape=trapezium];" + +/-- +A vector of references into `aig`. This is the `AIG` analog of `BitVec`. +-/ +structure RefVec (aig : AIG α) (w : Nat) where + refs : Array Nat + hlen : refs.size = w + hrefs : ∀ (h : i < w), refs[i] < aig.decls.size + +/-- +A sequence of references bundled with their AIG. +-/ +structure RefVecEntry (α : Type) [DecidableEq α] [Hashable α] [DecidableEq α] (w : Nat) where + aig : AIG α + vec : RefVec aig w + +/-- +A `RefVec` bundled with constant distance to be shifted by. +-/ +structure ShiftTarget (aig : AIG α) (w : Nat) where + vec : AIG.RefVec aig w + distance : Nat + +/-- +A `RefVec` bundled with a `RefVec` as distance to be shifted by. +-/ +structure ArbitraryShiftTarget (aig : AIG α) (m : Nat) where + n : Nat + target : AIG.RefVec aig m + distance : AIG.RefVec aig n + +/-- +A `RefVec` to be extended to `newWidth`. +-/ +structure ExtendTarget (aig : AIG α) (newWidth : Nat) where + w : Nat + vec : AIG.RefVec aig w + +/-- +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 +where + go (x : Nat) (decls : Array (Decl α)) (assign : α → Bool) (h1 : x < decls.size) + (h2 : IsDAG α decls) : + Bool := + match h3 : decls[x] with + | .const b => b + | .atom v => assign v + | .gate lhs rhs linv rinv => + have := h2 h1 h3 + let lval := go lhs decls assign (by omega) h2 + let rval := go rhs decls assign (by omega) h2 + xor lval linv && xor rval rinv + +/-- +Denotation of an `AIG` at a specific `Entrypoint`. +-/ +scoped syntax "⟦" term ", " term "⟧" : term + +/-- +Denotation of an `AIG` at a specific `Entrypoint` with the `Entrypoint` being constructed on the fly. +-/ +scoped syntax "⟦" term ", " term ", " term "⟧" : term + +macro_rules +| `(⟦$entry, $assign⟧) => `(denote $assign $entry) +| `(⟦$aig, $ref, $assign⟧) => `(denote $assign (Entrypoint.mk $aig $ref)) + +@[app_unexpander AIG.denote] +def unexpandDenote : Lean.PrettyPrinter.Unexpander + | `($(_) {aig := $aig, start := $start, inv := $hbound} $assign) => + `(⟦$aig, ⟨$start, $hbound⟩, $assign⟧) + | `($(_) $entry $assign) => `(⟦$entry, $assign⟧) + | _ => throw () + +/-- +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 + +/-- +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 } + +/-- +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 α := + 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 + let cache := aig.cache.noUpdate + have invariant := by + intro i lhs' rhs' linv' rinv' h1 h2 + simp only [Array.get_push] at h2 + split at h2 + . apply aig.invariant <;> assumption + . injections + have := input.lhs.ref.hgate + have := input.rhs.ref.hgate + omega + ⟨{ aig with decls, invariant, cache }, ⟨g, by simp [decls]⟩⟩ + +/-- +Add a new input node to the AIG in `aig`. Note that this version is only meant for proving, +for production purposes use `AIG.mkAtomCached` and equality theorems to this one. +-/ +def mkAtom (aig : AIG α) (n : α) : Entrypoint α := + let g := aig.decls.size + let decls := aig.decls.push (.atom n) + let cache := aig.cache.noUpdate + have invariant := by + intro i lhs rhs linv rinv h1 h2 + simp only [Array.get_push] at h2 + split at h2 + . apply aig.invariant <;> assumption + . contradiction + ⟨{ decls, invariant, cache }, ⟨g, by simp [decls]⟩⟩ + +/-- +Add a new constant node to `aig`. Note that this version is only meant for proving, +for production purposes use `AIG.mkConstCached` and equality theorems to this one. +-/ +def mkConst (aig : AIG α) (val : Bool) : Entrypoint α := + let g := aig.decls.size + let decls := aig.decls.push (.const val) + let cache := aig.cache.noUpdate + have invariant := by + intro i lhs rhs linv rinv h1 h2 + simp only [Array.get_push] at h2 + split at h2 + . apply aig.invariant <;> assumption + . contradiction + ⟨{ decls, invariant, cache }, ⟨g, by simp [decls]⟩⟩ + +end AIG + +end Sat +end Std diff --git a/src/Std/Sat/AIG/CNF.lean b/src/Std/Sat/AIG/CNF.lean new file mode 100644 index 0000000000..42986c17de --- /dev/null +++ b/src/Std/Sat/AIG/CNF.lean @@ -0,0 +1,725 @@ +/- +Copyright (c) 2024 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Henrik Böving +-/ +import Std.Sat.CNF +import Std.Sat.AIG.Basic +import Std.Sat.AIG.Lemmas + + +/-! +This module contains an implementation of a verified Tseitin transformation on AIGs. The key results +are the `toCNF` function and the `toCNF_equisat` correctness statement. The implementation is +done in the style of section 3.4 of the AIGNET paper. +-/ + +namespace Std +namespace Sat + +namespace AIG + +namespace Decl + +/-- +Produce a Tseitin style CNF for a `Decl.const`, using `output` as the tree node variable. +-/ +def constToCNF (output : α) (const : Bool) : CNF α := + [[(output, const)]] + +/-- +Produce a Tseitin style CNF for a `Decl.atom`, using `output` as the tree node variable. +-/ +def atomToCNF (output : α) (atom : α) : CNF α := + [[(output, true), (atom, false)], [(output, false), (atom, true)]] + +/-- +Produce a Tseitin style CNF for a `Decl.gate`, using `output` as the tree node variable. +-/ +def gateToCNF (output : α) (lhs rhs : α) (linv rinv : Bool) : CNF α := + -- a ↔ (b and c) as CNF: (¬a ∨ b) ∧ (¬a ∨ c) ∧ (a ∨ ¬b ∨ ¬c) + -- a ↔ (b and ¬c) as CNF: (¬a ∨ b) ∧ (¬a ∨ ¬c) ∧ (a ∨ ¬b ∨ c) + -- a ↔ (¬b and c) as CNF: (¬a ∨ ¬b) ∧ (¬a ∨ c) ∧ (a ∨ b ∨ ¬c) + -- a ↔ (¬b and ¬c) as CNF: (¬a ∨ ¬b) ∧ (¬a ∨ ¬c) ∧ (a ∨ b ∨ c) + [ + [(output, false), (lhs, !linv)], + [(output, false), (rhs, !rinv)], + [(output, true), (lhs, linv), (rhs, rinv)] + ] + +@[simp] +theorem constToCNF_eval : + (constToCNF output b).eval assign + = + (assign output == b) := by + simp [constToCNF, CNF.eval, CNF.Clause.eval] + +@[simp] +theorem atomToCNF_eval : + (atomToCNF output a).eval assign + = + (assign output == assign a) := by + simp only [atomToCNF, CNF.eval_cons, CNF.Clause.eval_cons, beq_true, beq_false, + CNF.Clause.eval_nil, Bool.or_false, CNF.eval_nil, Bool.and_true] + cases assign output <;> cases assign a <;> decide + +@[simp] +theorem gateToCNF_eval : + (gateToCNF output lhs rhs linv rinv).eval assign + = + (assign output == ((xor (assign lhs) linv) && (xor (assign rhs) rinv))) := by + simp only [CNF.eval, gateToCNF, CNF.Clause.eval, List.all_cons, List.any_cons, beq_false, + List.any_nil, Bool.or_false, beq_true, List.all_nil, Bool.and_true] + cases assign output + <;> cases assign lhs + <;> cases assign rhs + <;> cases linv + <;> cases rinv + <;> decide + +end Decl + +abbrev CNFVar (aig : AIG Nat) := Nat ⊕ (Fin aig.decls.size) + +namespace toCNF + +/-- +Mix: +1. An assignment for AIG atoms +2. An assignment for auxiliary Tseitin variables +into an assignment that can be used by a CNF produced by our Tseitin transformation. +-/ +def mixAssigns {aig : AIG Nat} (assign1 : Nat → Bool) (assign2 : Fin aig.decls.size → Bool) : + CNFVar aig → Bool + | .inl var => assign1 var + | .inr var => assign2 var + +/-- +Project the atom assignment out of a CNF assignment +-/ +def projectLeftAssign (assign : CNFVar aig → Bool) : Nat → Bool := (assign <| .inl ·) + +/-- +Project the auxiliary variable assignment out of a CNF assignment +-/ +def projectRightAssign (assign : CNFVar aig → Bool) : (idx : Nat) → (idx < aig.decls.size) → Bool := + fun idx h => assign (.inr ⟨idx, h⟩) + +@[simp] +theorem projectLeftAssign_property : (projectLeftAssign assign) x = (assign <| .inl x) := by + simp [projectLeftAssign] + +@[simp] +theorem projectRightAssign_property : + (projectRightAssign assign) x hx = (assign <| .inr ⟨x, hx⟩) := by + simp [projectRightAssign] + +/-- +Given an atom assignment, produce an assignment that will always satisfy the CNF generated by our +Tseitin transformation. This is done by combining the atom assignment with an assignment for the +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⟧) + +@[simp] +theorem satAssignment_inl : (cnfSatAssignment aig assign1) (.inl x) = assign1 x := by + simp [cnfSatAssignment, mixAssigns] + +@[simp] +theorem satAssignment_inr : + (cnfSatAssignment aig assign1) (.inr x) = ⟦aig, ⟨x.val, x.isLt⟩, assign1⟧ := by + simp [cnfSatAssignment, mixAssigns] + +/-- +The central invariants for the `Cache`. +-/ +structure Cache.Inv (cnf : CNF (CNFVar aig)) (marks : Array Bool) (hmarks : marks.size = aig.decls.size) : Prop where + /-- + If there exists an AIG node that is marked, its children are also guaranteed to be marked already. + This allows us to conclude that if a gate node is marked, all of its (transitive) children are + also marked. + -/ + hmark : ∀ (lhs rhs : Nat) (linv rinv : Bool) (idx : Nat) (hbound : idx < aig.decls.size) + (_hmarked : marks[idx] = true) (heq : aig.decls[idx] = .gate lhs rhs linv rinv), + marks[lhs]'(by have := aig.invariant hbound heq; omega) = true + ∧ + marks[rhs]'(by have := aig.invariant hbound heq; omega) = true + /-- + Relate satisfiability results about our produced CNF to satisfiability results about the AIG that + we are processing. The intuition for this is: if a node is marked, its CNF (and all required + children CNFs according to `hmark`) are already part of the current CNF. Thus the current CNF is + already mirroring the semantics of the marked node. This means that if the CNF is satisfiable at + some assignment, we can evaluate the marked node under the atom part of that assignment and will + get the value that was assigned to the corresponding auxiliary variable as a result. + -/ + 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 + + +/-- +The `Cache` invariant always holds for an empty CNF when all nodes are unmarked. +-/ +theorem Cache.Inv_init : Inv ([] : CNF (CNFVar aig)) (mkArray aig.decls.size false) (by simp) where + hmark := by + intro lhs rhs linv rinv idx hbound hmarked heq + simp at hmarked + heval := by + intro assign _ idx hbound hmark + simp at hmark + +/-- +The CNF cache. It keeps track of AIG nodes that we already turned into CNF to avoid adding the same +CNF twice. +-/ +structure Cache (aig : AIG Nat) (cnf : CNF (CNFVar aig)) where + /-- + Keeps track of AIG nodes that we already turned into CNF. + -/ + marks : Array Bool + /-- + There are always as many marks as AIG nodes. + -/ + hmarks : marks.size = aig.decls.size + /-- + The invariant to make sure that `marks` is well formed with respect to the `cnf` + -/ + inv : Cache.Inv cnf marks hmarks + +/-- +We say that a cache extends another by an index when it doesn't invalidate any entry and has an +entry for that index. +-/ +structure Cache.IsExtensionBy (cache1 : Cache aig cnf1) (cache2 : Cache aig cnf2) (new : Nat) + (hnew : new < aig.decls.size) : Prop where + /-- + No entry is invalidated. + -/ + extension : ∀ (idx : Nat) (hidx : idx < aig.decls.size), + cache1.marks[idx]'(by have := cache1.hmarks; omega) = true + → + cache2.marks[idx]'(by have := cache2.hmarks; omega) = true + /-- + The second cache is true at the new index. + -/ + trueAt : cache2.marks[new]'(by have := cache2.hmarks; omega) = true + +theorem Cache.IsExtensionBy_trans_left (cache1 : Cache aig cnf1) (cache2 : Cache aig cnf2) + (cache3 : Cache aig cnf3) (h12 : IsExtensionBy cache1 cache2 new1 hnew1) + (h23 : IsExtensionBy cache2 cache3 new2 hnew2) : IsExtensionBy cache1 cache3 new1 hnew1 := by + apply IsExtensionBy.mk + . intro idx hidx hmarked + apply h23.extension + . apply h12.extension + . exact hmarked + . omega + . omega + . apply h23.extension + . exact h12.trueAt + . omega + +theorem Cache.IsExtensionBy_trans_right (cache1 : Cache aig cnf1) (cache2 : Cache aig cnf2) + (cache3 : Cache aig cnf3) (h12 : IsExtensionBy cache1 cache2 new1 hnew1) + (h23 : IsExtensionBy cache2 cache3 new2 hnew2) : IsExtensionBy cache1 cache3 new2 hnew2 := by + apply IsExtensionBy.mk + . intro idx hidx hmarked + apply h23.extension + . apply h12.extension + . exact hmarked + . omega + . omega + . exact h23.trueAt + +/-- +Cache extension is a reflexive relation. +-/ +theorem Cache.IsExtensionBy_rfl (cache : Cache aig cnf) {h} (hmarked : cache.marks[idx]'h = true) : + Cache.IsExtensionBy cache cache idx (have := cache.hmarks; omega) := by + apply IsExtensionBy.mk + . intros + assumption + . exact hmarked + +theorem Cache.IsExtensionBy_set (cache1 : Cache aig cnf1) (cache2 : Cache aig cnf2) (idx : Nat) + (hbound : idx < cache1.marks.size) (h : cache2.marks = cache1.marks.set ⟨idx, hbound⟩ true) : + IsExtensionBy cache1 cache2 idx (by have := cache1.hmarks; omega) := by + apply IsExtensionBy.mk + . intro idx hidx hmark + simp [Array.getElem_set, hmark, h] + . simp [h] + +/-- +A cache with no entries is valid for an empty CNF. +-/ +def Cache.init (aig : AIG Nat) : Cache aig [] where + marks := mkArray aig.decls.size false + hmarks := by simp + inv := Inv_init + +/-- +Add a `Decl.const` to a `Cache`. +-/ +def Cache.addConst (cache : Cache aig cnf) (idx : Nat) (h : idx < aig.decls.size) + (htip : aig.decls[idx]'h = .const b) : + { + out : Cache aig (Decl.constToCNF (.inr ⟨idx, h⟩) b ++ cnf) + // + Cache.IsExtensionBy cache out idx h + } := + have hmarkbound : idx < cache.marks.size := by have := cache.hmarks; omega + let out := + { cache with + marks := cache.marks.set ⟨idx, hmarkbound⟩ true + hmarks := by simp [cache.hmarks] + inv := by + constructor + . intro lhs rhs linv rinv idx hbound hmarked heq + rw [Array.getElem_set] at hmarked + split at hmarked + . simp_all + . have := cache.inv.hmark lhs rhs linv rinv idx hbound hmarked heq + simp [Array.getElem_set, this] + . intro assign heval idx hbound hmarked + rw [Array.getElem_set] at hmarked + split at hmarked + . next heq => + dsimp only at 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] + . 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 + rw [this] + } + ⟨out, IsExtensionBy_set cache out idx hmarkbound (by simp [out])⟩ + +/-- +Add a `Decl.atom` to a cache. +-/ +def Cache.addAtom (cache : Cache aig cnf) (idx : Nat) (h : idx < aig.decls.size) + (htip : aig.decls[idx]'h = .atom a) : + { + out : Cache aig ((Decl.atomToCNF (.inr ⟨idx, h⟩) (.inl a)) ++ cnf) + // + Cache.IsExtensionBy cache out idx h + } := + have hmarkbound : idx < cache.marks.size := by have := cache.hmarks; omega + let out := + { cache with + marks := cache.marks.set ⟨idx, hmarkbound⟩ true + hmarks := by simp [cache.hmarks] + inv := by + constructor + . intro lhs rhs linv rinv idx hbound hmarked heq + rw [Array.getElem_set] at hmarked + split at hmarked + . simp_all + . have := cache.inv.hmark lhs rhs linv rinv idx hbound hmarked heq + simp [Array.getElem_set, this] + . intro assign heval idx hbound hmarked + rw [Array.getElem_set] at hmarked + split at hmarked + . next heq => + dsimp only at heq + simp only [heq, CNF.eval_append, Decl.atomToCNF_eval, Bool.and_eq_true, beq_iff_eq] at htip heval + simp [heval, denote_idx_atom htip] + . next heq => + simp only [CNF.eval_append, Decl.atomToCNF_eval, Bool.and_eq_true, beq_iff_eq] at heval + have := cache.inv.heval assign heval.right idx hbound hmarked + rw [this] + } + ⟨out, IsExtensionBy_set cache out idx hmarkbound (by simp [out])⟩ + +/-- +Add a `Decl.gate` to a cache. +-/ +def Cache.addGate (cache : Cache aig cnf) {hlb} {hrb} (idx : Nat) (h : idx < aig.decls.size) + (htip : aig.decls[idx]'h = .gate lhs rhs linv rinv) (hl : cache.marks[lhs]'hlb = true) + (hr : cache.marks[rhs]'hrb = true) : + { + out : Cache + aig + (Decl.gateToCNF + (.inr ⟨idx, h⟩) + (.inr ⟨lhs, by have := aig.invariant h htip; omega⟩) + (.inr ⟨rhs, by have := aig.invariant h htip; omega⟩) + linv + rinv + ++ cnf) + // + Cache.IsExtensionBy cache out idx h + } := + have := aig.invariant h htip + have hmarkbound : idx < cache.marks.size := by have := cache.hmarks; omega + let out := + { cache with + marks := cache.marks.set ⟨idx, hmarkbound⟩ true + hmarks := by simp [cache.hmarks] + inv := by + constructor + . intro lhs rhs linv rinv idx hbound hmarked heq + rw [Array.getElem_set] at hmarked + split at hmarked + . next heq2 => + simp only at heq2 + simp only [heq2] at htip + rw [htip] at heq + cases heq + simp [Array.getElem_set, hl, hr] + . have := cache.inv.hmark lhs rhs linv rinv idx hbound hmarked heq + simp [Array.getElem_set, this] + . intro assign heval idx hbound hmarked + rw [Array.getElem_set] at hmarked + split at hmarked + . next heq => + dsimp only at heq + simp only [heq, CNF.eval_append, Decl.gateToCNF_eval, Bool.and_eq_true, beq_iff_eq] + 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] + . 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 + rw [this] + } + ⟨out, IsExtensionBy_set cache out idx hmarkbound (by simp [out])⟩ + +/-- +The key invariant about the `State` itself (without cache): The CNF we produce is always satisfiable +at `cnfSatAssignment`. +-/ +def State.Inv (cnf : CNF (CNFVar aig)) : Prop := + ∀ (assign1 : Nat → Bool), cnf.Sat (cnfSatAssignment aig assign1) + +/-- +The `State` invariant always holds when we have an empty CNF. +-/ +theorem State.Inv_nil : State.Inv ([] : CNF (CNFVar aig)) := by + simp [State.Inv] + +/-- +Combining two CNFs for which `State.Inv` holds preserves `State.Inv`. +-/ +theorem State.Inv_append (h1 : State.Inv cnf1) (h2 : State.Inv cnf2) : + State.Inv (cnf1 ++ cnf2) := by + intro assign1 + specialize h1 assign1 + specialize h2 assign1 + simp [CNF.sat_def] at h1 h2 ⊢ + constructor <;> assumption + +/-- +`State.Inv` holds for the CNF that we produce for a `Decl.const`. +-/ +theorem State.Inv_constToCNF (heq : aig.decls[upper] = .const b) : + State.Inv (aig := aig) (Decl.constToCNF (.inr ⟨upper, h⟩) b) := by + intro assign1 + simp [CNF.sat_def, denote_idx_const heq] + +/-- +`State.Inv` holds for the CNF that we produce for a `Decl.atom` +-/ +theorem State.Inv_atomToCNF (heq : aig.decls[upper] = .atom a) : + State.Inv (aig := aig) (Decl.atomToCNF (.inr ⟨upper, h⟩) (.inl a)) := by + intro assign1 + simp [CNF.sat_def, denote_idx_atom heq] + +/-- +`State.Inv` holds for the CNF that we produce for a `Decl.gate` +-/ +theorem State.Inv_gateToCNF {aig : AIG Nat} {h} + (heq : aig.decls[upper]'h = .gate lhs rhs linv rinv) : + State.Inv + (aig := aig) + (Decl.gateToCNF + (.inr ⟨upper, h⟩) + (.inr ⟨lhs, by have := aig.invariant h heq; omega⟩) + (.inr ⟨rhs, by have := aig.invariant h heq; omega⟩) + linv + rinv) + := by + intro assign1 + simp [CNF.sat_def, denote_idx_gate heq] + +/-- +The state to accumulate CNF clauses as we run our Tseitin transformation on the AIG. +-/ +structure State (aig : AIG Nat) where + /-- + The CNF clauses so far. + -/ + cnf : CNF (CNFVar aig) + /-- + A cache so that we don't generate CNF for an AIG node more than once. + -/ + cache : Cache aig cnf + /-- + The invariant that `cnf` has to maintain as we build it up. + -/ + inv : State.Inv cnf + +/-- +An initial state with no CNF clauses and an empty cache. +-/ +def State.empty (aig : AIG Nat) : State aig where + cnf := [] + cache := Cache.init aig + inv := State.Inv_nil + +/-- +State extension are `Cache.IsExtensionBy` for now. +-/ +abbrev State.IsExtensionBy (state1 : State aig) (state2 : State aig) (new : Nat) + (hnew : new < aig.decls.size) : Prop := + Cache.IsExtensionBy state1.cache state2.cache new hnew + +theorem State.IsExtensionBy_trans_left (state1 : State aig) (state2 : State aig) + (state3 : State aig) (h12 : IsExtensionBy state1 state2 new1 hnew1) + (h23 : IsExtensionBy state2 state3 new2 hnew2) : IsExtensionBy state1 state3 new1 hnew1 := by + apply Cache.IsExtensionBy_trans_left + . exact h12 + . exact h23 + +theorem State.IsExtensionBy_trans_right (state1 : State aig) (state2 : State aig) + (state3 : State aig) (h12 : IsExtensionBy state1 state2 new1 hnew1) + (h23 : IsExtensionBy state2 state3 new2 hnew2) : IsExtensionBy state1 state3 new2 hnew2 := by + apply Cache.IsExtensionBy_trans_right + . exact h12 + . exact h23 + +/-- +State extension is a reflexive relation. +-/ +theorem State.IsExtensionBy_rfl (state : State aig) {h} + (hmarked : state.cache.marks[idx]'h = true) : + State.IsExtensionBy state state idx (have := state.cache.hmarks; omega) := by + apply Cache.IsExtensionBy_rfl <;> assumption + +/-- +Add the CNF for a `Decl.const` to the state. +-/ +def State.addConst (state : State aig) (idx : Nat) (h : idx < aig.decls.size) + (htip : aig.decls[idx]'h = .const b) : + { out : State aig // State.IsExtensionBy state out idx h } := + let ⟨cnf, cache, inv⟩ := state + let newCnf := Decl.constToCNF (.inr ⟨idx, h⟩) b + have hinv := toCNF.State.Inv_constToCNF htip + let ⟨cache, hcache⟩ := cache.addConst idx h htip + ⟨⟨newCnf ++ cnf, cache, State.Inv_append hinv inv⟩, by simp [hcache]⟩ + +/-- +Add the CNF for a `Decl.atom` to the state. +-/ +def State.addAtom (state : State aig) (idx : Nat) (h : idx < aig.decls.size) + (htip : aig.decls[idx]'h = .atom a) : + { out : State aig // State.IsExtensionBy state out idx h } := + let ⟨cnf, cache, inv⟩ := state + let newCnf := Decl.atomToCNF (.inr ⟨idx, h⟩) (.inl a) + have hinv := toCNF.State.Inv_atomToCNF htip + let ⟨cache, hcache⟩ := cache.addAtom idx h htip + ⟨⟨newCnf ++ cnf, cache, State.Inv_append hinv inv⟩, by simp [hcache]⟩ + +/-- +Add the CNF for a `Decl.gate` to the state. +-/ +def State.addGate (state : State aig) {hlb} {hrb} (idx : Nat) (h : idx < aig.decls.size) + (htip : aig.decls[idx]'h = .gate lhs rhs linv rinv) (hl : state.cache.marks[lhs]'hlb = true) + (hr : state.cache.marks[rhs]'hrb = true) : + { out : State aig // State.IsExtensionBy state out idx h } := + have := aig.invariant h htip + let ⟨cnf, cache, inv⟩ := state + let newCnf := + Decl.gateToCNF + (.inr ⟨idx, h⟩) + (.inr ⟨lhs, by omega⟩) + (.inr ⟨rhs, by omega⟩) + linv + rinv + have hinv := toCNF.State.Inv_gateToCNF htip + let ⟨cache, hcache⟩ := cache.addGate idx h htip hl hr + ⟨⟨newCnf ++ cnf, cache, State.Inv_append hinv inv⟩, by simp [hcache]⟩ + +/-- +Evaluate the CNF contained within the state. +-/ +def State.eval (assign : CNFVar aig → Bool) (state : State aig) : Bool := + state.cnf.eval assign + +/-- +The CNF within the state is sat. +-/ +def State.Sat (assign : CNFVar aig → Bool) (state : State aig) : Prop := + state.cnf.Sat assign + +/-- +The CNF within the state is unsat. +-/ +def State.Unsat (state : State aig) : Prop := + state.cnf.Unsat + +theorem State.sat_def (assign : CNFVar aig → Bool) (state : State aig) : + state.Sat assign ↔ state.cnf.Sat assign := by + rfl + +theorem State.unsat_def (state : State aig) : + state.Unsat ↔ state.cnf.Unsat := by + rfl + +@[simp] +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] + +@[simp] +theorem State.unsat_iff : State.Unsat state ↔ state.cnf.Unsat := by simp [State.unsat_def] + +end toCNF + +/-- +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 + cnf.relabel inj +where + inj {aig : AIG Nat} (var : CNFVar aig) : Nat := + match var with + | .inl var => aig.decls.size + var + | .inr var => var.val + go (aig : AIG Nat) (upper : Nat) (h : upper < aig.decls.size) (state : toCNF.State aig) : + { out : toCNF.State aig // toCNF.State.IsExtensionBy state out upper h } := + if hmarked : state.cache.marks[upper]'(by have := state.cache.hmarks; omega) then + ⟨state, by apply toCNF.State.IsExtensionBy_rfl <;> assumption⟩ + else + let decl := aig.decls[upper] + match heq : decl with + | .const b => state.addConst upper h heq + | .atom a => state.addAtom upper h heq + | .gate lhs rhs linv rinv => + have := aig.invariant h heq + let ⟨lstate, hlstate⟩ := go aig lhs (by omega) state + let ⟨rstate, hrstate⟩ := go aig rhs (by omega) lstate + + have : toCNF.State.IsExtensionBy state rstate lhs (by omega) := by + apply toCNF.State.IsExtensionBy_trans_left + . exact hlstate + . exact hrstate + + let ⟨ret, hretstate⟩ := rstate.addGate upper h heq this.trueAt hrstate.trueAt + ⟨ + ret, + by + apply toCNF.State.IsExtensionBy_trans_right + . exact hlstate + . apply toCNF.State.IsExtensionBy_trans_right + . exact hrstate + . exact hretstate + ⟩ + +/-- +The function we use to convert from CNF with explicit auxiliary variables to just `Nat` variables +in `toCNF` is an injection. +-/ +theorem toCNF.inj_is_injection {aig : AIG Nat} (a b : CNFVar aig) : + toCNF.inj a = toCNF.inj b → a = b := by + intro h + cases a with + | inl => + cases b with + | inl => + dsimp only [inj] at h + congr + omega + | inr rhs => + exfalso + dsimp only [inj] at h + have := rhs.isLt + omega + | inr lhs => + cases b with + | inl => + dsimp only [inj] at h + omega + | inr => + dsimp only [inj] at h + congr + omega + +/-- +The node that we started CNF conversion at will always be marked as visited in the CNF cache. +-/ +theorem toCNF.go_marks : + (go aig start h state).val.cache.marks[start]'(by have := (go aig start h state).val.cache.hmarks; omega) = true := + (go aig start h state).property.trueAt + +/-- +The CNF returned by `go` will always be SAT at `cnfSatAssignment`. +-/ +theorem toCNF.go_sat (aig : AIG Nat) (start : Nat) (h1 : start < aig.decls.size) (assign1 : Nat → Bool) + (state : toCNF.State aig) : + (go aig start h1 state).val.Sat (cnfSatAssignment aig assign1) := by + have := (go aig start h1 state).val.inv assign1 + 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 + have := go_sat aig start h1 assign1 (.empty aig) + simp only [State.Sat, CNF.sat_def] at this + simp [this] + +/-- +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, h1⟩, assign1⟧ = sat?) := by + have := go_as_denote' aig start 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) + → + CNF.eval assign (([(.inr ⟨start, h1⟩, true)] :: (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] + | false => + simp [heval1] + +/-- +An AIG is unsat iff its CNF is unsat. +-/ +theorem toCNF_equisat (entry : Entrypoint Nat) : (toCNF entry).Unsat ↔ entry.Unsat := by + dsimp only [toCNF] + rw [CNF.unsat_relabel_iff] + . constructor + . intro h assign1 + apply toCNF.go_as_denote + specialize h (toCNF.cnfSatAssignment entry.aig assign1) + simpa using h + . intro h assign + apply toCNF.denote_as_go + specialize h (toCNF.projectLeftAssign assign) + assumption + . intro a b _ _ hinj + apply toCNF.inj_is_injection + assumption + +end AIG + +end Sat +end Std diff --git a/src/Std/Sat/AIG/Cached.lean b/src/Std/Sat/AIG/Cached.lean new file mode 100644 index 0000000000..ef9f778efa --- /dev/null +++ b/src/Std/Sat/AIG/Cached.lean @@ -0,0 +1,132 @@ +/- +Copyright (c) 2024 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Henrik Böving +-/ +import Std.Sat.AIG.Basic +import Std.Sat.AIG.Lemmas + +/-! +This module contains functions to construct AIG nodes while making use of the sub-circuit cache +if possible. For performance reasons these functions should usually be preferred over the naive +AIG node creation ones. +-/ + +namespace Std +namespace Sat + +namespace AIG + +variable {α : Type} [Hashable α] [DecidableEq α] + +/-- +A version of `AIG.mkAtom` that uses the subterm cache in `AIG`. This version is meant for +programmming, for proving purposes use `AIG.mkAtom` and equality theorems to this one. +-/ +def mkAtomCached (aig : AIG α) (n : α) : Entrypoint α := + let ⟨decls, cache, inv⟩ := aig + let decl := .atom n + match cache.get? decl with + | some hit => + ⟨⟨decls, cache, inv⟩ , hit.idx, hit.hbound⟩ + | none => + let g := decls.size + let cache := cache.insert decls decl + let decls := decls.push decl + have inv := by + intro i lhs rhs linv rinv h1 h2 + simp only [Array.get_push] at h2 + split at h2 + . apply inv <;> assumption + . contradiction + ⟨⟨decls, cache, inv⟩, ⟨g, by simp [g, decls]⟩⟩ + +/-- +A version of `AIG.mkConst` that uses the subterm cache in `AIG`. This version is meant for +programmming, for proving purposes use `AIG.mkGate` and equality theorems to this one. +-/ +def mkConstCached (aig : AIG α) (val : Bool) : Entrypoint α := + let ⟨decls, cache, inv⟩ := aig + let decl := .const val + match cache.get? decl with + | some hit => + ⟨⟨decls, cache, inv⟩, hit.idx, hit.hbound⟩ + | none => + let g := decls.size + let cache := cache.insert decls decl + let decls := decls.push decl + have inv := by + intro i lhs rhs linv rinv h1 h2 + simp only [Array.get_push] at h2 + split at h2 + . apply inv <;> assumption + . contradiction + ⟨⟨decls, cache, inv⟩, ⟨g, by simp [g, decls]⟩⟩ + +/-- +A version of `AIG.mkGate` that uses the subterm cache in `AIG`. This version is meant for +programmming, for proving purposes use `AIG.mkGate` and equality theorems to this one. + +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 + 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 α := + 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 decl := .gate lhs rhs linv rinv + match cache.get? decl with + | some hit => + ⟨⟨decls, cache, inv⟩, ⟨hit.idx, hit.hbound⟩⟩ + | none => + /- + Here we implement the constant propagating subset of: + https://fmv.jku.at/papers/BrummayerBiere-MEMICS06.pdf + TODO: rest of the table + -/ + match decls[lhs], decls[rhs], linv, rinv with + -- Boundedness + | .const true, _, true, _ | .const false, _, false, _ + | _, .const true, _, true | _, .const false, _, false => + mkConstCached ⟨decls, cache, inv⟩ false + -- Left Neutrality + | .const true, _, false, false | .const false, _, true, false => + ⟨⟨decls, cache, inv⟩, rhs, (by assumption)⟩ + -- Right Neutrality + | _, .const true, false, false | _, .const false, false, true => + ⟨⟨decls, cache, inv⟩, lhs, (by assumption)⟩ + | _, _, _, _ => + if lhs == rhs && linv == false && rinv == false then + -- Idempotency rule + ⟨⟨decls, cache, inv⟩, lhs, (by assumption)⟩ + else if lhs == rhs && linv == !rinv then + -- Contradiction rule + mkConstCached ⟨decls, cache, inv⟩ false + else + let g := decls.size + let cache := cache.insert decls decl + let decls := decls.push decl + have inv := by + intro i lhs rhs linv rinv h1 h2 + simp only [decls] at * + simp only [Array.get_push] at h2 + split at h2 + . apply inv <;> assumption + . injections; omega + ⟨⟨decls, cache, inv⟩, ⟨g, by simp [g, decls]⟩⟩ + +end AIG + +end Sat +end Std diff --git a/src/Std/Sat/AIG/CachedGates.lean b/src/Std/Sat/AIG/CachedGates.lean new file mode 100644 index 0000000000..b81c0f1e1f --- /dev/null +++ b/src/Std/Sat/AIG/CachedGates.lean @@ -0,0 +1,175 @@ +/- +Copyright (c) 2024 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Henrik Böving +-/ +import Std.Sat.AIG.Cached +import Std.Sat.AIG.CachedLemmas + +/-! +This module contains functions to construct basic logic gates while making use of the sub-circuit +cache if possible. +-/ + +namespace Std +namespace Sat + +namespace AIG + +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 } } + +/-- +Create an and gate in the input AIG. This uses the builtin cache to enable automated subterm +sharing. +-/ +def mkAndCached (aig : AIG α) (input : BinaryInput aig) : Entrypoint α := + aig.mkGateCached <| input.asGateInput false false + +/-- +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 + 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 (config := { zetaDelta := true }) only + apply LawfulOperator.le_size_of_le_aig_size (f := mkConstCached) + omega + inv := true + } + } + +/-- +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 + 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 aig := res.aig + let aux2Ref := res.ref + aig.mkGateCached { + lhs := { + ref := aux1Ref.cast <| by + simp (config := { zetaDelta := true }) only + apply LawfulOperator.le_size_of_le_aig_size (f := mkGateCached) + omega + inv := true + }, + rhs := { + ref := aux2Ref + inv := true + } + } + +/-- +Create an equality gate in the input AIG. This uses the builtin cache to enable automated subterm +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 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 aig := res.aig + let aux2Ref := res.ref + aig.mkGateCached { + lhs := { + ref := aux1Ref.cast <| by + simp (config := { zetaDelta := true }) only + apply LawfulOperator.le_size_of_le_aig_size (f := mkGateCached) + omega + inv := true + }, + rhs := { + ref := aux2Ref + inv := true + } + } + +/-- +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 + 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 (config := { zetaDelta := true }) only + apply LawfulOperator.le_size_of_le_aig_size (f := mkConstCached) + omega + inv := true + } + } + +end AIG + +end Sat +end Std diff --git a/src/Std/Sat/AIG/CachedGatesLemmas.lean b/src/Std/Sat/AIG/CachedGatesLemmas.lean new file mode 100644 index 0000000000..e6e9255b45 --- /dev/null +++ b/src/Std/Sat/AIG/CachedGatesLemmas.lean @@ -0,0 +1,268 @@ +/- +Copyright (c) 2024 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Henrik Böving +-/ +import Std.Sat.AIG.CachedGates +import Std.Sat.AIG.LawfulOperator + +/-! +This module contains the theory of the cached gate creation functions, mostly enabled by the +`LawfulOperator` framework. It is mainly concerned with proving lemmas about the denotational +semantics of the gate functions in different scenarios. +-/ + +namespace Std +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. +-/ +private theorem or_as_aig : ∀ (a b : Bool), (!(!a && !b)) = (a || b) := by + decide + +/-- +Encoding of XOR as boolean expression in AIG form. +-/ +private theorem xor_as_aig : ∀ (a b : Bool), (!(a && b) && !(!a && !b)) = (xor a b) := by + decide + +/-- +Encoding of BEq as boolean expression in AIG form. +-/ +private theorem beq_as_aig : ∀ (a b : Bool), (!(a && !b) && !(!a && b)) = (a == b) := by + decide + +/-- +Encoding of implication as boolean expression in AIG form. +-/ +private theorem imp_as_aig : ∀ (a b : Bool), (!(a && !b)) = (!a || b) := by + decide + +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 + +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 + +instance : LawfulOperator α Ref mkNotCached where + le_size := mkNotCached_le_size + decl_eq := by + intros + apply mkNotCached_decl_eq + +@[simp] +theorem denote_mkNotCached {aig : AIG α} {gate : Ref aig} : + ⟦aig.mkNotCached gate, assign⟧ + = + !⟦aig, ⟨gate.gate, gate.hgate⟩, assign⟧ := by + rw [← not_as_aig] + simp [mkNotCached, LawfulOperator.denote_mem_prefix (f := mkConstCached) gate.hgate] + +theorem mkAndCached_le_size (aig : AIG α) (input : BinaryInput aig) : + aig.decls.size ≤ (aig.mkAndCached input).aig.decls.size := by + simp only [mkAndCached] + apply LawfulOperator.le_size_of_le_aig_size + omega + +theorem mkAndCached_decl_eq idx (aig : AIG α) (input : BinaryInput aig) {h : idx < aig.decls.size} + {h2} : + (aig.mkAndCached input).aig.decls[idx]'h2 = aig.decls[idx] := by + simp only [mkAndCached] + rw [AIG.LawfulOperator.decl_eq (f := mkGateCached)] + +instance : LawfulOperator α BinaryInput mkAndCached where + le_size := mkAndCached_le_size + decl_eq := by intros; apply mkAndCached_decl_eq + +@[simp] +theorem denote_mkAndCached {aig : AIG α} {input : BinaryInput aig} : + ⟦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 + +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 + decl_eq := by intros; apply mkOrCached_decl_eq + +@[simp] +theorem denote_mkOrCached {aig : AIG α} {input : BinaryInput aig} : + ⟦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)] + + +theorem mkXorCached_le_size (aig : AIG α) {input : BinaryInput aig} : + aig.decls.size ≤ (aig.mkXorCached input).aig.decls.size := by + simp only [mkXorCached] + apply LawfulOperator.le_size_of_le_aig_size + apply LawfulOperator.le_size_of_le_aig_size + apply LawfulOperator.le_size_of_le_aig_size + omega + +theorem mkXorCached_decl_eq idx (aig : AIG α) (input : BinaryInput aig) {h : idx < aig.decls.size} + {h2} : + (aig.mkXorCached input).aig.decls[idx]'h2 = aig.decls[idx] := by + simp only [mkXorCached] + rw [AIG.LawfulOperator.decl_eq (f := mkGateCached)] + rw [AIG.LawfulOperator.decl_eq (f := mkGateCached)] + . rw [AIG.LawfulOperator.decl_eq (f := mkGateCached)] + apply LawfulOperator.lt_size_of_lt_aig_size + assumption + . apply LawfulOperator.lt_size_of_lt_aig_size + apply LawfulOperator.lt_size_of_lt_aig_size + assumption + +instance : LawfulOperator α BinaryInput mkXorCached where + le_size := mkXorCached_le_size + decl_eq := by intros; apply mkXorCached_decl_eq + +@[simp] +theorem denote_mkXorCached {aig : AIG α} {input : BinaryInput aig} : + ⟦aig.mkXorCached input, assign⟧ + = + xor + ⟦aig, input.lhs, assign⟧ + ⟦aig, input.rhs, assign⟧ + := by + rw [← xor_as_aig] + simp [ + mkXorCached, + LawfulOperator.denote_mem_prefix (f := mkGateCached) input.lhs.hgate, + LawfulOperator.denote_mem_prefix (f := mkGateCached) input.rhs.hgate + ] + +theorem mkBEqCached_le_size (aig : AIG α) {input : BinaryInput aig} : + aig.decls.size ≤ (aig.mkBEqCached input).aig.decls.size := by + simp only [mkBEqCached] + apply LawfulOperator.le_size_of_le_aig_size + apply LawfulOperator.le_size_of_le_aig_size + apply LawfulOperator.le_size_of_le_aig_size + omega + +theorem mkBEqCached_decl_eq idx (aig : AIG α) (input : BinaryInput aig) {h : idx < aig.decls.size} + {h2} : + (aig.mkBEqCached input).aig.decls[idx]'h2 = aig.decls[idx] := by + simp only [mkBEqCached] + rw [AIG.LawfulOperator.decl_eq (f := mkGateCached)] + rw [AIG.LawfulOperator.decl_eq (f := mkGateCached)] + . rw [AIG.LawfulOperator.decl_eq (f := mkGateCached)] + apply LawfulOperator.lt_size_of_lt_aig_size + assumption + . apply LawfulOperator.lt_size_of_lt_aig_size + apply LawfulOperator.lt_size_of_lt_aig_size + assumption + +instance : LawfulOperator α BinaryInput mkBEqCached where + le_size := mkBEqCached_le_size + decl_eq := by intros; apply mkBEqCached_decl_eq + +@[simp] +theorem denote_mkBEqCached {aig : AIG α} {input : BinaryInput aig} : + ⟦aig.mkBEqCached input, assign⟧ + = + (⟦aig, input.lhs, assign⟧ + == + ⟦aig, input.rhs, assign⟧) := by + rw [← beq_as_aig] + simp [ + mkBEqCached, + LawfulOperator.denote_mem_prefix (f := mkGateCached) input.lhs.hgate, + LawfulOperator.denote_mem_prefix (f := mkGateCached) input.rhs.hgate + ] + +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 + +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 + decl_eq := by intros; apply mkImpCached_decl_eq + +@[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 + rw [← imp_as_aig] + simp [mkImpCached, LawfulOperator.denote_input_entry (f := mkConstCached)] + +end AIG + +end Sat +end Std diff --git a/src/Std/Sat/AIG/CachedLemmas.lean b/src/Std/Sat/AIG/CachedLemmas.lean new file mode 100644 index 0000000000..fd75ec2bf4 --- /dev/null +++ b/src/Std/Sat/AIG/CachedLemmas.lean @@ -0,0 +1,340 @@ +/- +Copyright (c) 2024 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Henrik Böving +-/ +import Std.Sat.AIG.Cached + +/-! +This module contains the theory of the cached AIG node creation functions. +It is mainly concerned with proving lemmas about the denotational semantics of the gate functions +in different scenarios, in particular reductions to the semantics of the non cached versions. +-/ + +namespace Std +namespace Sat + +namespace AIG + +variable {α : Type} [Hashable α] [DecidableEq α] + +/-- +If we find a cached atom declaration in the AIG, denoting it is equivalent to denoting `AIG.mkAtom`. +-/ +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 + have := hit.hvalid + simp only [denote_mkAtom] + unfold denote denote.go + split <;> simp_all + +/-- +`mkAtomCached` does not modify the input AIG upon a cache hit. +-/ +theorem mkAtomCached_hit_aig (aig : AIG α) {hit} (hcache : aig.cache.get? (.atom var) = some hit) : + (aig.mkAtomCached var).aig = aig := by + simp only [mkAtomCached] + split <;> simp_all + +/-- +`mkAtomCached` pushes to the input AIG upon a cache miss. +-/ +theorem mkAtomCached_miss_aig (aig : AIG α) (hcache : aig.cache.get? (.atom var) = none) : + (aig.mkAtomCached var).aig.decls = aig.decls.push (.atom var) := by + simp only [mkAtomCached] + split <;> simp_all + +/-- +The AIG produced by `AIG.mkAtomCached` agrees with the input AIG on all indices that are valid for +both. +-/ +theorem mkAtomCached_decl_eq (aig : AIG α) (var : α) (idx : Nat) {h : idx < aig.decls.size} + {hbound} : + (aig.mkAtomCached var).aig.decls[idx]'hbound = aig.decls[idx] := by + match hcache : aig.cache.get? (.atom var) with + | some gate => + have := mkAtomCached_hit_aig aig hcache + simp [this] + | none => + have := mkAtomCached_miss_aig aig hcache + simp only [this, Array.get_push] + split + . rfl + . contradiction + +/-- +`AIG.mkAtomCached` never shrinks the underlying AIG. +-/ +theorem mkAtomCached_le_size (aig : AIG α) (var : α) : + aig.decls.size ≤ (aig.mkAtomCached var).aig.decls.size := by + dsimp only [mkAtomCached] + split + . simp + . simp_arith + +instance : LawfulOperator α (fun _ => α) mkAtomCached where + le_size := mkAtomCached_le_size + decl_eq := mkAtomCached_decl_eq + +/-- +The central equality theorem between `mkAtomCached` and `mkAtom`. +-/ +@[simp] +theorem mkAtomCached_eval_eq_mkAtom_eval {aig : AIG α} : + ⟦aig.mkAtomCached var, assign⟧ = ⟦aig.mkAtom var, assign⟧ := by + simp only [mkAtomCached] + split + . next heq1 => + rw [denote_mkAtom_cached heq1] + . simp [mkAtom, denote] + +/-- +If we find a cached const declaration in the AIG, denoting it is equivalent to denoting +`AIG.mkConst`. +-/ +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 + have := hit.hvalid + simp only [denote_mkConst] + unfold denote denote.go + split <;> simp_all + +/-- +`mkConstCached` does not modify the input AIG upon a cache hit. +-/ +theorem mkConstCached_hit_aig (aig : AIG α) {hit} + (hcache : aig.cache.get? (.const val) = some hit) : + (aig.mkConstCached val).aig = aig := by + simp only [mkConstCached] + split <;> simp_all + +/-- +`mkConstCached` pushes to the input AIG upon a cache miss. +-/ +theorem mkConstCached_miss_aig (aig : AIG α) (hcache : aig.cache.get? (.const val) = none) : + (aig.mkConstCached val).aig.decls = aig.decls.push (.const val) := by + simp only [mkConstCached] + split <;> simp_all + +/-- +The AIG produced by `AIG.mkConstCached` agrees with the input AIG on all indices that are valid for +both. +-/ +theorem mkConstCached_decl_eq (aig : AIG α) (val : Bool) (idx : Nat) {h : idx < aig.decls.size} + {hbound} : + (aig.mkConstCached val).aig.decls[idx]'hbound = aig.decls[idx] := by + match hcache : aig.cache.get? (.const val) with + | some gate => + have := mkConstCached_hit_aig aig hcache + simp [this] + | none => + have := mkConstCached_miss_aig aig hcache + simp only [this, Array.get_push] + split + . rfl + . contradiction + +/-- +`AIG.mkConstCached` never shrinks the underlying AIG. +-/ +theorem mkConstCached_le_size (aig : AIG α) (val : Bool) : + aig.decls.size ≤ (aig.mkConstCached val).aig.decls.size := by + dsimp only [mkConstCached] + split + . simp + . simp_arith + +instance : LawfulOperator α (fun _ => Bool) mkConstCached where + le_size := mkConstCached_le_size + decl_eq := by + intros + apply mkConstCached_decl_eq + +/-- +The central equality theorem between `mkConstCached` and `mkConst`. +-/ +@[simp] +theorem mkConstCached_eval_eq_mkConst_eval {aig : AIG α} : + ⟦aig.mkConstCached val, assign⟧ = ⟦aig.mkConst val, assign⟧ := by + simp only [mkConstCached] + split + . next heq1 => + rw [denote_mkConst_cached heq1] + . simp [mkConst, denote] + +/-- +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, hit.idx, hit.hbound⟩, assign⟧ + = + ⟦aig.mkGate input, assign⟧ := by + intros + have := hit.hvalid + simp only [denote_mkGate] + conv => + lhs + unfold denote denote.go + split <;> simp_all[denote] + +theorem mkGateCached.go_le_size (aig : AIG α) (input : GateInput aig) : + aig.decls.size ≤ (go aig input).aig.decls.size := by + dsimp only [go] + split + . simp + . split + . simp_arith [mkConstCached_le_size] + . simp_arith [mkConstCached_le_size] + . simp_arith [mkConstCached_le_size] + . simp_arith [mkConstCached_le_size] + . simp_arith + . simp_arith + . simp_arith + . simp_arith + . split + . simp_arith + . split <;> simp_arith [mkConstCached_le_size] + +/-- +`AIG.mkGateCached` never shrinks the underlying AIG. +-/ +theorem mkGateCached_le_size (aig : AIG α) (input : GateInput 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) : + ∀ (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 + dsimp only at hres + split at hres + . rw [← hres] + intros + simp + . split at hres + . rw [← hres] + intros + rw [LawfulOperator.decl_eq (f := AIG.mkConstCached)] + . rw [← hres] + intros + rw [LawfulOperator.decl_eq (f := AIG.mkConstCached)] + . rw [← hres] + intros + rw [LawfulOperator.decl_eq (f := AIG.mkConstCached)] + . rw [← hres] + intros + rw [LawfulOperator.decl_eq (f := AIG.mkConstCached)] + . rw [← hres] + intros + simp + . rw [← hres] + intros + simp + . rw [← hres] + intros + simp + . rw [← hres] + intros + simp + . split at hres + . rw [← hres] + intros + simp + . split at hres + . rw [← hres] + intros + rw [AIG.LawfulOperator.decl_eq (f := AIG.mkConstCached)] + . rw [← hres] + dsimp only + intro idx h1 h2 + rw [Array.get_push] + simp [h2] + +/-- +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) : + ∀ (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 + dsimp only at hres + split at hres + all_goals + rw [← hres] + intros + rw [mkGateCached.go_decl_eq] + +instance : LawfulOperator α GateInput 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} : + ⟦go aig input, assign⟧ = ⟦aig.mkGate input, assign⟧ := by + simp only [go] + split + . next heq1 => + rw [denote_mkGate_cached heq1] + . split + . next heq _ => + simp_all [denote_idx_const heq] + . next heq _ => + simp_all [denote_idx_const heq] + . next heq _ _ _ => + simp_all [denote_idx_const heq] + . next heq _ _ _ => + simp_all [denote_idx_const heq] + . next heq _ _ _ => + simp_all [denote_idx_const heq] + . next heq _ _ _ => + simp_all [denote_idx_const heq] + . next heq _ _ _ _ => + simp_all [denote_idx_const heq] + . next heq _ _ _ => + simp_all [denote_idx_const heq] + . 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] + +/-- +The central equality theorem between `mkGateCached` and `mkGate`. +-/ +@[simp] +theorem mkGateCached_eval_eq_mkGate_eval {aig : AIG α} {input : GateInput aig} : + ⟦aig.mkGateCached input, assign⟧ = ⟦aig.mkGate input, assign⟧ := by + simp only [mkGateCached] + split + . rw [mkGateCached.go_eval_eq_mkGate_eval] + . rw [mkGateCached.go_eval_eq_mkGate_eval] + simp only [denote_mkGate] + rw [Bool.and_comm] + +end AIG + +end Sat +end Std diff --git a/src/Std/Sat/AIG/If.lean b/src/Std/Sat/AIG/If.lean new file mode 100644 index 0000000000..ff3ab22736 --- /dev/null +++ b/src/Std/Sat/AIG/If.lean @@ -0,0 +1,300 @@ +/- +Copyright (c) 2024 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Henrik Böving +-/ +import Std.Sat.AIG.CachedGatesLemmas +import Std.Sat.AIG.LawfulVecOperator + +/-! +Besides introducing a way to construct an if statement in an `AIG`, this module also demonstrates +a style of writing Lean code that minimizes the risk of linearity issues on the `AIG`. + +The idea is to always keep one `aig` variable around that contains the `AIG` and continously +shadow it. However, applying multiple operations to the `AIG` does often require `Ref.cast` to use +other inputs or `Ref`s created by previous operations in later ones. Applying a `Ref.cast` would +usually require keeping around the old `AIG` to state the theorem statement. Luckily in this +situation Lean is usually always able to infer the theorem statement on it's own. For this +reason the style goes as follows: +``` +let res := someLawfulOperator aig input +let aig := res.aig +let ref := res.ref +have := LawfulOperator.le_size (f := mkIfCached) .. +let input1 := input1.cast this +let input2 := input2.cast this +-- ... +-- Next `LawfulOperator` application +``` +This style also generalizes to applications of `LawfulVecOperator`s. +-/ + +namespace Std +namespace Sat + +namespace AIG + +variable {α : Type} [Hashable α] [DecidableEq α] + +open AIG + +def mkIfCached (aig : AIG α) (input : TernaryInput aig) : Entrypoint α := + -- if d then l else r = ((d && l) || (!d && r)) + let res := aig.mkAndCached ⟨input.discr, input.lhs⟩ + let aig := res.aig + let lhsRef := res.ref + let input := input.cast <| by apply AIG.LawfulOperator.le_size (f := mkAndCached) + let res := aig.mkNotCached input.discr + let aig := res.aig + let notDiscr := res.ref + let input := input.cast <| by apply AIG.LawfulOperator.le_size (f := mkNotCached) + let res := aig.mkAndCached ⟨notDiscr, input.rhs⟩ + let aig := res.aig + let rhsRef := res.ref + let lhsRef := lhsRef.cast <| by + apply AIG.LawfulOperator.le_size_of_le_aig_size (f := mkAndCached) + apply AIG.LawfulOperator.le_size (f := mkNotCached) + aig.mkOrCached ⟨lhsRef, rhsRef⟩ + +instance : LawfulOperator α TernaryInput mkIfCached where + le_size := by + intros + unfold mkIfCached + dsimp only + apply LawfulOperator.le_size_of_le_aig_size (f := mkOrCached) + apply LawfulOperator.le_size_of_le_aig_size (f := mkAndCached) + apply LawfulOperator.le_size_of_le_aig_size (f := mkNotCached) + apply LawfulOperator.le_size (f := mkAndCached) + decl_eq := by + intros + unfold mkIfCached + dsimp only + rw [LawfulOperator.decl_eq (f := mkOrCached)] + rw [LawfulOperator.decl_eq (f := mkAndCached)] + rw [LawfulOperator.decl_eq (f := mkNotCached)] + rw [LawfulOperator.decl_eq (f := mkAndCached)] + . apply LawfulOperator.lt_size_of_lt_aig_size (f := mkAndCached) + omega + . apply LawfulOperator.lt_size_of_lt_aig_size (f := mkNotCached) + apply LawfulOperator.lt_size_of_lt_aig_size (f := mkAndCached) + omega + . apply LawfulOperator.lt_size_of_lt_aig_size (f := mkAndCached) + apply LawfulOperator.lt_size_of_lt_aig_size (f := mkNotCached) + apply LawfulOperator.lt_size_of_lt_aig_size (f := mkAndCached) + omega + +theorem if_as_bool (d l r : Bool) : (if d then l else r) = ((d && l) || (!d && r)) := by + revert d l r + decide + +@[simp] +theorem denote_mkIfCached {aig : AIG α} {input : TernaryInput aig} : + ⟦aig.mkIfCached input, assign⟧ + = + if ⟦aig, input.discr, assign⟧ then ⟦aig, input.lhs, assign⟧ else ⟦aig, input.rhs, assign⟧ := by + rw [if_as_bool] + unfold mkIfCached + dsimp only + simp only [TernaryInput.cast, Ref_cast', id_eq, Int.reduceNeg, denote_mkOrCached, + denote_projected_entry, denote_mkAndCached, denote_mkNotCached] + congr 2 + . rw [LawfulOperator.denote_mem_prefix] + rw [LawfulOperator.denote_mem_prefix] + . simp + . simp [Ref.hgate] + . rw [LawfulOperator.denote_mem_prefix] + . rw [LawfulOperator.denote_mem_prefix] + rw [LawfulOperator.denote_mem_prefix] + +namespace RefVec + +structure IfInput (aig : AIG α) (w : Nat) where + discr : Ref aig + lhs : RefVec aig w + rhs : RefVec aig w + +def ite (aig : AIG α) (input : IfInput aig w) : RefVecEntry α w := + let ⟨discr, lhs, rhs⟩ := input + go aig 0 (by omega) discr lhs rhs .empty +where + go {w : Nat} (aig : AIG α) (curr : Nat) (hcurr : curr ≤ w) (discr : Ref aig) + (lhs rhs : RefVec aig w) (s : RefVec aig curr) : RefVecEntry α w := + if hcurr : curr < w then + let input := ⟨discr, lhs.get curr hcurr, rhs.get curr hcurr⟩ + let res := mkIfCached aig input + let aig := res.aig + let ref := res.ref + have := LawfulOperator.le_size (f := mkIfCached) .. + let discr := discr.cast this + let lhs := lhs.cast this + let rhs := rhs.cast this + let s := s.cast this + let s := s.push ref + go aig (curr + 1) (by omega) discr lhs rhs s + else + have : curr = w := by omega + ⟨aig, this ▸ s⟩ +termination_by w - curr + +namespace ite + +theorem go_le_size (aig : AIG α) (curr : Nat) (hcurr : curr ≤ w) (discr : Ref aig) + (lhs rhs : RefVec aig w) (s : RefVec aig curr) : + aig.decls.size ≤ (go aig curr hcurr discr lhs rhs s).aig.decls.size := by + unfold go + dsimp only + split + . refine Nat.le_trans ?_ (by apply go_le_size) + apply LawfulOperator.le_size (f := mkIfCached) + . simp +termination_by w - curr + +theorem go_decl_eq (aig : AIG α) (curr : Nat) (hcurr : curr ≤ w) (discr : Ref aig) + (lhs rhs : RefVec aig w) (s : RefVec aig curr) : + ∀ (idx : Nat) (h1) (h2), + (go aig curr hcurr discr lhs rhs s).aig.decls[idx]'h2 = aig.decls[idx]'h1 := by + generalize hgo : go aig curr hcurr discr lhs rhs s = res + unfold go at hgo + dsimp only at hgo + split at hgo + . rw [← hgo] + intro idx h1 h2 + rw [go_decl_eq] + rw [AIG.LawfulOperator.decl_eq (f := AIG.mkIfCached)] + apply AIG.LawfulOperator.lt_size_of_lt_aig_size (f := AIG.mkIfCached) + assumption + . simp [← hgo] +termination_by w - curr + +end ite + +instance : LawfulVecOperator α IfInput ite where + le_size := by + intros + unfold ite + apply ite.go_le_size + decl_eq := by + intros + unfold ite + rw [ite.go_decl_eq] + +namespace ite + +theorem go_get_aux {w : Nat} (aig : AIG α) (curr : Nat) (hcurr : curr ≤ w) (discr : Ref aig) + (lhs rhs : RefVec aig w) (s : RefVec aig curr) : + ∀ (idx : Nat) (hidx : idx < curr) (hfoo), + (go aig curr hcurr discr lhs rhs s).vec.get idx (by omega) + = + (s.get idx hidx).cast hfoo := by + intro idx hidx + generalize hgo : go aig curr hcurr discr lhs rhs s = res + unfold go at hgo + dsimp only at hgo + split at hgo + . rw [← hgo] + intros + rw [go_get_aux] + rw [AIG.RefVec.get_push_ref_lt] + . simp only [Ref.cast, Ref.mk.injEq] + rw [AIG.RefVec.get_cast] + . simp + . assumption + . apply go_le_size + . rw [← hgo] + simp only [Nat.le_refl, get, Ref_cast', Ref.mk.injEq, true_implies] + have : curr = w := by omega + subst this + simp +termination_by w - curr + +theorem go_get {w : Nat} (aig : AIG α) (curr : Nat) (hcurr : curr ≤ w) (discr : Ref aig) + (lhs rhs : RefVec aig w) (s : RefVec aig curr) : + ∀ (idx : Nat) (hidx : idx < curr), + (go aig curr hcurr discr lhs rhs s).vec.get idx (by omega) + = + (s.get idx hidx).cast (by apply go_le_size) := by + intro idx hidx + apply go_get_aux + +theorem go_denote_mem_prefix {w : Nat} (aig : AIG α) (curr : Nat) (hcurr : curr ≤ w) + (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⟩, + assign + ⟧ + = + ⟦aig, ⟨start, hstart⟩, assign⟧ := by + apply denote.eq_of_isPrefix (entry := ⟨aig, start,hstart⟩) + apply IsPrefix.of + . intros + apply go_decl_eq + . intros + apply go_le_size + +theorem denote_go {w : Nat} (aig : AIG α) (curr : Nat) (hcurr : curr ≤ w) (discr : Ref aig) + (lhs rhs : RefVec aig w) (s : RefVec aig curr) : + ∀ (idx : Nat) (hidx1 : idx < w), + curr ≤ idx + → + ⟦ + (go aig curr hcurr discr lhs rhs s).aig, + (go aig curr hcurr discr lhs rhs s).vec.get idx hidx1, + assign + ⟧ + = + if ⟦aig, discr, assign⟧ then + ⟦aig, lhs.get idx hidx1, assign⟧ + else + ⟦aig, rhs.get idx hidx1, assign⟧ := by + intro idx hidx1 hidx2 + generalize hgo : go aig curr hcurr discr lhs rhs s = res + unfold go at hgo + dsimp only at hgo + split at hgo + . cases Nat.eq_or_lt_of_le hidx2 with + | inl heq => + subst heq + rw [← hgo] + rw [go_get] + rw [AIG.RefVec.get_push_ref_eq'] + . rw [go_denote_mem_prefix] + . simp + . simp [Ref.hgate] + . omega + | inr heq => + rw [← hgo] + rw [denote_go] + . rw [LawfulOperator.denote_mem_prefix (f := mkIfCached)] + rw [LawfulOperator.denote_mem_prefix (f := mkIfCached)] + rw [LawfulOperator.denote_mem_prefix (f := mkIfCached)] + . simp + . simp [Ref.hgate] + . simp [Ref.hgate] + . simp [Ref.hgate] + . omega + . omega +termination_by w - curr + +end ite + +@[simp] +theorem denote_ite {aig : AIG α} {input : IfInput aig w} : + ∀ (idx : Nat) (hidx : idx < w), + ⟦(ite aig input).aig, (ite aig input).vec.get idx hidx, assign⟧ + = + if ⟦aig, input.discr, assign⟧ then + ⟦aig, input.lhs.get idx hidx, assign⟧ + else + ⟦aig, input.rhs.get idx hidx, assign⟧ := by + intro idx hidx + unfold ite + dsimp only + rw [ite.denote_go] + omega +end RefVec + +end AIG + +end Sat +end Std diff --git a/src/Std/Sat/AIG/LawfulOperator.lean b/src/Std/Sat/AIG/LawfulOperator.lean new file mode 100644 index 0000000000..a2338aa6c8 --- /dev/null +++ b/src/Std/Sat/AIG/LawfulOperator.lean @@ -0,0 +1,155 @@ +/- +Copyright (c) 2024 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Henrik Böving +-/ +import Std.Sat.AIG.Basic + +/-! +The lawful operator framework provides free theorems around the typeclass `LawfulOperator`. +Its definition is based on section 3.3 of the AIGNET paper. +-/ + +namespace Std +namespace Sat + +namespace AIG + +/-- +`decls1` is a prefix of `decls2` +-/ +structure IsPrefix (decls1 decls2 : Array (Decl α)) : Prop where + of :: + /-- + The prefix may never be longer than the other array. + -/ + size_le : decls1.size ≤ decls2.size + /-- + The prefix and the other array must agree on all elements up until the bound of the prefix + -/ + idx_eq : ∀ idx (h : idx < decls1.size), decls2[idx]'(by omega) = decls1[idx]'h + +/-- +If `decls1` is a prefix of `decls2` and we start evaluating `decls2` at an +index in bounds of `decls1` we can evaluate at `decls1`. +-/ +theorem denote.go_eq_of_isPrefix (decls1 decls2 : Array (Decl α)) (start : Nat) {hdag1} {hdag2} + {hbounds1} {hbounds2} (hprefix : IsPrefix decls1 decls2) : + denote.go start decls2 assign hbounds2 hdag2 + = + denote.go start decls1 assign hbounds1 hdag1 := by + unfold denote.go + have hidx1 := hprefix.idx_eq start hbounds1 + split + . next heq => + rw [hidx1] at heq + split <;> simp_all + . next heq => + rw [hidx1] at heq + split <;> simp_all + . next lhs rhs linv rinv heq => + rw [hidx1] at heq + have := hdag1 hbounds1 heq + have hidx2 := hprefix.idx_eq lhs (by omega) + have hidx3 := hprefix.idx_eq rhs (by omega) + split + . simp_all + . simp_all + . simp_all + congr 2 + . apply denote.go_eq_of_isPrefix + assumption + . apply denote.go_eq_of_isPrefix + assumption +termination_by start + +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⟧ + = + ⟦entry, assign⟧ + := by + unfold denote + apply denote.go_eq_of_isPrefix + assumption + +abbrev ExtendingEntrypoint (aig : AIG α) : Type := + { entry : Entrypoint α // aig.decls.size ≤ entry.aig.decls.size } + +abbrev ExtendingRefVecEntry (aig : AIG α) (len : Nat) : Type := + { ref : RefVecEntry α len // aig.decls.size ≤ ref.aig.decls.size } + +/-- +A function `f` that takes some `aig : AIG α` and an argument of type `β aig` is called a lawful +AIG operator if it only extends the `AIG` but never modifies already existing nodes. + +This guarantees that applying such a function will not change the semantics of any existing parts +of the circuit, allowing us to perform local reasoning on the AIG. +-/ +class LawfulOperator (α : Type) [Hashable α] [DecidableEq α] + (β : AIG α → Type) (f : (aig : AIG α) → β aig → Entrypoint α) where + le_size : ∀ (aig : AIG α) (input : β aig), aig.decls.size ≤ (f aig input).aig.decls.size + decl_eq : ∀ (aig : AIG α) (input : β aig) (idx : Nat) (h1 : idx < aig.decls.size) (h2), + (f aig input).aig.decls[idx]'h2 = aig.decls[idx]'h1 + +namespace LawfulOperator + +variable {β : AIG α → Type} +variable {f : (aig : AIG α) → β aig → Entrypoint α} [LawfulOperator α β f] + +theorem isPrefix_aig (aig : AIG α) (input : β aig) : + IsPrefix aig.decls (f aig input).aig.decls := by + apply IsPrefix.of + . intro idx h + apply decl_eq + . apply le_size + +theorem lt_size (entry : Entrypoint α) (input : β entry.aig) : + entry.ref.gate < (f entry.aig input).aig.decls.size := by + have h1 := entry.ref.hgate + have h2 : entry.aig.decls.size ≤ (f entry.aig input).aig.decls.size := by + apply le_size + omega + +theorem lt_size_of_lt_aig_size (aig : AIG α) (input : β aig) (h : x < aig.decls.size) : + x < (f aig input).aig.decls.size := by + apply Nat.lt_of_lt_of_le + . exact h + . exact le_size aig input + +theorem le_size_of_le_aig_size (aig : AIG α) (input : β aig) (h : x ≤ aig.decls.size) : + x ≤ (f aig input).aig.decls.size := by + apply Nat.le_trans + . exact h + . exact le_size aig input + +@[simp] +theorem denote_input_entry (entry : Entrypoint α) {input} {h} : + ⟦(f entry.aig input).aig, ⟨entry.ref.gate, h⟩, assign⟧ + = + ⟦entry, assign⟧ := by + apply denote.eq_of_isPrefix + apply isPrefix_aig + +@[simp] +theorem denote_cast_entry (entry : Entrypoint α) {input} {h} : + ⟦(f entry.aig input).aig, entry.ref.cast h, assign⟧ + = + ⟦entry, assign⟧ := by + 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⟧ + = + ⟦aig, ⟨start, h⟩, assign⟧ := by + rw [denote_input_entry ⟨aig, start, h⟩] + +end LawfulOperator + +end AIG + +end Sat +end Std diff --git a/src/Std/Sat/AIG/LawfulVecOperator.lean b/src/Std/Sat/AIG/LawfulVecOperator.lean new file mode 100644 index 0000000000..8432c2fbdf --- /dev/null +++ b/src/Std/Sat/AIG/LawfulVecOperator.lean @@ -0,0 +1,87 @@ +/- +Copyright (c) 2024 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Henrik Böving +-/ +import Std.Sat.AIG.LawfulOperator +import Std.Sat.AIG.RefVec + +namespace Std +namespace Sat + +namespace AIG + +variable {α : Type} [Hashable α] [DecidableEq α] + +class LawfulVecOperator (α : Type) [Hashable α] [DecidableEq α] + (β : AIG α → Nat → Type) (f : {len : Nat} → (aig : AIG α) → β aig len → RefVecEntry α len) where + le_size : ∀ (aig : AIG α) (input : β aig len), aig.decls.size ≤ (f aig input).aig.decls.size + decl_eq : ∀ (aig : AIG α) (input : β aig len) (idx : Nat) (h1 : idx < aig.decls.size) (h2), + (f aig input).aig.decls[idx]'h2 = aig.decls[idx]'h1 + +namespace LawfulVecOperator + +variable {β : AIG α → Nat → Type} +variable {f : {len : Nat} → (aig : AIG α) → β aig len → RefVecEntry α len} +variable [LawfulVecOperator α β f] + +theorem isPrefix_aig (aig : AIG α) (input : β aig len) : + IsPrefix aig.decls (f aig input).aig.decls := by + apply IsPrefix.of + . intro idx h + apply decl_eq + . apply le_size + +theorem lt_size (entry : Entrypoint α) (input : β entry.aig len) : + entry.ref.gate < (f entry.aig input).aig.decls.size := by + have h1 := entry.ref.hgate + have h2 : entry.aig.decls.size ≤ (f entry.aig input).aig.decls.size := by + apply le_size + omega + +theorem lt_size_of_lt_aig_size (aig : AIG α) (input : β aig len) (h : x < aig.decls.size) : + x < (f aig input).aig.decls.size := by + apply Nat.lt_of_lt_of_le + . exact h + . exact le_size aig input + +theorem le_size_of_le_aig_size (aig : AIG α) (input : β aig len) (h : x ≤ aig.decls.size) : + x ≤ (f aig input).aig.decls.size := by + apply Nat.le_trans + . exact h + . exact le_size aig input + +@[simp] +theorem denote_input_entry (entry : Entrypoint α) {input : β entry.aig len} {h} : + ⟦(f entry.aig input).aig, ⟨entry.ref.gate, h⟩, assign ⟧ + = + ⟦entry, assign⟧ := by + apply denote.eq_of_isPrefix + apply isPrefix_aig + +@[simp] +theorem denote_cast_entry (entry : Entrypoint α) {input : β entry.aig len} {h} : + ⟦(f entry.aig input).aig, entry.ref.cast h, assign⟧ + = + ⟦entry, assign⟧ := by + 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⟧ + = + ⟦aig, ⟨start, h⟩, assign⟧ := by + rw [denote_input_entry ⟨aig, start, h⟩] + +@[simp] +theorem denote_input_vec (s : RefVecEntry α len) {input : β s.aig len} {hcast} : + ⟦(f s.aig input).aig, (s.vec.get idx hidx).cast hcast, assign⟧ + = + ⟦s.aig, s.vec.get idx hidx, assign⟧ := by + rw [denote_mem_prefix] + rfl + +end LawfulVecOperator +end AIG + +end Sat +end Std diff --git a/src/Std/Sat/AIG/Lemmas.lean b/src/Std/Sat/AIG/Lemmas.lean new file mode 100644 index 0000000000..c14108f301 --- /dev/null +++ b/src/Std/Sat/AIG/Lemmas.lean @@ -0,0 +1,290 @@ +/- +Copyright (c) 2024 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Henrik Böving +-/ +import Std.Sat.AIG.Basic +import Std.Sat.AIG.LawfulOperator + +/-! +This module provides a basic theory around the naive AIG node creation functions. It is mostly +fundamental work for the cached versions later on. +-/ + +namespace Std +namespace Sat + +namespace AIG + +variable {α : Type} [Hashable α] [DecidableEq α] + +@[simp] +theorem Ref_cast {aig1 aig2 : AIG α} (ref : Ref aig1) + (h : aig1.decls.size ≤ aig2.decls.size) : + (ref.cast h).gate = ref.gate := rfl + +@[simp] +theorem Ref_cast' {aig1 aig2 : AIG α} (ref : Ref aig1) + (h : aig1.decls.size ≤ aig2.decls.size) : + (ref.cast h) = ⟨ref.gate, by have := ref.hgate; omega⟩ := rfl + +@[simp] +theorem Fanin_cast_ref {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_cast_inv {aig1 aig2 : AIG α} (fanin : Fanin aig1) + (h : aig1.decls.size ≤ aig2.decls.size) : + (fanin.cast h).inv = fanin.inv := rfl + +@[simp] +theorem GateInput_cast_lhs {aig1 aig2 : AIG α} (input : GateInput aig1) + (h : aig1.decls.size ≤ aig2.decls.size) : + (input.cast h).lhs = input.lhs.cast h := rfl + +@[simp] +theorem GateInput_cast_rhs {aig1 aig2 : AIG α} (input : GateInput aig1) + (h : aig1.decls.size ≤ aig2.decls.size) : + (input.cast h).rhs = input.rhs.cast h := rfl + +@[simp] +theorem BinaryInput.cast_each {aig1 aig2 : AIG α} (lhs rhs : Ref aig1) + (h1 h2 : aig1.decls.size ≤ aig2.decls.size) : + BinaryInput.mk (lhs.cast h1) (rhs.cast h2) = (BinaryInput.mk lhs rhs).cast h2 := by + simp [BinaryInput.cast] + +@[simp] +theorem denote_projected_entry {entry : Entrypoint α} : + ⟦entry.aig, entry.ref, assign⟧ = ⟦entry, assign⟧ := by + cases entry; simp + +@[simp] +theorem denote_projected_entry' {entry : Entrypoint α} : + ⟦entry.aig, ⟨entry.ref.gate, entry.ref.hgate⟩, assign⟧ = ⟦entry, assign⟧ := by + cases entry; simp + +/-- +`AIG.mkGate` never shrinks the underlying AIG. +-/ +theorem mkGate_le_size (aig : AIG α) (input : GateInput aig) : + aig.decls.size ≤ (aig.mkGate input).aig.decls.size := by + simp_arith [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} : + have := mkGate_le_size aig input + (aig.mkGate input).aig.decls[idx]'(by omega) = aig.decls[idx] := by + simp only [mkGate, Array.get_push] + split + . rfl + . contradiction + +instance : LawfulOperator α GateInput mkGate where + le_size := mkGate_le_size + decl_eq := by + intros + apply mkGate_decl_eq + +@[simp] +theorem denote_mkGate {aig : AIG α} {input : GateInput aig} : + ⟦aig.mkGate input, assign⟧ + = + ( + (xor ⟦aig, input.lhs.ref, assign⟧ input.lhs.inv) + && + (xor ⟦aig, input.rhs.ref, assign⟧ input.rhs.inv) + ) := by + conv => + lhs + unfold denote denote.go + split + . next heq => + rw [mkGate, Array.get_push_eq] at heq + contradiction + . next heq => + rw [mkGate, Array.get_push_eq] at heq + contradiction + . next heq => + rw [mkGate, Array.get_push_eq] at heq + injection heq with heq1 heq2 heq3 heq4 + dsimp only + 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] + +/-- +`AIG.mkAtom` never shrinks the underlying AIG. +-/ +theorem mkAtom_le_size (aig : AIG α) (var : α) : + aig.decls.size ≤ (aig.mkAtom var).aig.decls.size := by + simp_arith [mkAtom] + +/-- +The AIG produced by `AIG.mkAtom` agrees with the input AIG on all indices that are valid for both. +-/ +theorem mkAtom_decl_eq (aig : AIG α) (var : α) (idx : Nat) {h : idx < aig.decls.size} {hbound} : + (aig.mkAtom var).aig.decls[idx]'hbound = aig.decls[idx] := by + simp only [mkAtom, Array.get_push] + split + . rfl + . contradiction + +instance : LawfulOperator α (fun _ => α) mkAtom where + le_size := mkAtom_le_size + decl_eq := by + intros + apply mkAtom_decl_eq + +@[simp] +theorem denote_mkAtom {aig : AIG α} : + ⟦(aig.mkAtom var), assign⟧ = assign var := by + unfold denote denote.go + split + . next heq => + rw [mkAtom, Array.get_push_eq] at heq + contradiction + . next heq => + rw [mkAtom, Array.get_push_eq] at heq + injection heq with heq + rw [heq] + . next heq => + rw [mkAtom, Array.get_push_eq] at heq + contradiction + +/-- +`AIG.mkConst` never shrinks the underlying AIG. +-/ +theorem mkConst_le_size (aig : AIG α) (val : Bool) : + aig.decls.size ≤ (aig.mkConst val).aig.decls.size := by + simp_arith [mkConst] + +/-- +The AIG produced by `AIG.mkConst` agrees with the input AIG on all indices that are valid for both. +-/ +theorem mkConst_decl_eq (aig : AIG α) (val : Bool) (idx : Nat) {h : idx < aig.decls.size} : + have := mkConst_le_size aig val + (aig.mkConst val).aig.decls[idx]'(by omega) = aig.decls[idx] := by + simp only [mkConst, Array.get_push] + split + . rfl + . contradiction + +instance : LawfulOperator α (fun _ => Bool) mkConst where + le_size := mkConst_le_size + decl_eq := by + intros + apply mkConst_decl_eq + +@[simp] +theorem denote_mkConst {aig : AIG α} : ⟦(aig.mkConst val), assign⟧ = val := by + unfold denote denote.go + split + . next heq => + rw [mkConst, Array.get_push_eq] at heq + injection heq with heq + rw [heq] + . next heq => + rw [mkConst, Array.get_push_eq] at heq + contradiction + . next heq => + rw [mkConst, Array.get_push_eq] at heq + contradiction + +/-- +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 + unfold denote denote.go + split <;> simp_all + +/-- +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 + unfold denote denote.go + split <;> simp_all + +/-- +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⟧ + = + ( + (xor ⟦aig, ⟨lhs, by have := aig.invariant hstart h; omega⟩, assign⟧ linv) + && + (xor ⟦aig, ⟨rhs, by have := aig.invariant hstart h; omega⟩, assign⟧ rinv) + ) := by + unfold denote + conv => + lhs + unfold denote.go + split + . simp_all + . simp_all + . next heq => + rw [h] at heq + simp_all + +theorem idx_trichotomy (aig : AIG α) (hstart : start < aig.decls.size) {prop : Prop} + (hconst : ∀ b, aig.decls[start]'hstart = .const b → prop) + (hatom : ∀ a, aig.decls[start]'hstart = .atom a → prop) + (hgate : ∀ lhs rhs linv rinv, aig.decls[start]'hstart = .gate lhs rhs linv rinv → prop) + : prop := by + match h : aig.decls[start]'hstart with + | .const b => apply hconst; assumption + | .atom a => apply hatom; assumption + | .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) + (hgate : + ∀ lhs rhs linv rinv, + aig.decls[start]'hstart = .gate lhs rhs linv rinv + → + ⟦aig, ⟨start, hstart⟩, assign⟧ = res + ) : + ⟦aig, ⟨start, hstart⟩, assign⟧ = res := by + apply idx_trichotomy aig hstart + . exact hconst + . exact hatom + . exact hgate + +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) + (hidx : idx < aig.decls.size) (h : ∀ a, a ∈ aig → assign1 a = assign2 a) : + ⟦aig, ⟨idx, hidx⟩, assign1⟧ = ⟦aig, ⟨idx, hidx⟩, assign2⟧ := by + apply denote_idx_trichotomy + . intro b heq + simp [denote_idx_const heq] + . intro a heq + simp only [denote_idx_atom heq] + apply h + rw [mem_def, ← heq, Array.mem_def] + apply Array.getElem_mem_data + . 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] + +end AIG + +end Sat +end Std diff --git a/src/Std/Sat/AIG/RefVec.lean b/src/Std/Sat/AIG/RefVec.lean new file mode 100644 index 0000000000..9bfe96382c --- /dev/null +++ b/src/Std/Sat/AIG/RefVec.lean @@ -0,0 +1,188 @@ +/- +Copyright (c) 2024 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Henrik Böving +-/ +import Std.Sat.AIG.LawfulOperator +import Std.Sat.AIG.CachedGatesLemmas + +namespace Std +namespace Sat + +namespace AIG + +variable {α : Type} [Hashable α] [DecidableEq α] {aig : AIG α} + +namespace RefVec + +def empty : RefVec aig 0 where + refs := #[] + hlen := by simp + hrefs := by intros; contradiction + +@[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) : + RefVec aig2 len := + { s with + hrefs := by + intros + apply h + · intros + apply s.hrefs + assumption + · assumption + } + +@[inline] +def cast {aig1 aig2 : AIG α} (s : RefVec aig1 len) (h : aig1.decls.size ≤ aig2.decls.size) : + RefVec aig2 len := + s.cast' <| by + intro hall i hi + specialize hall hi + omega + +@[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, 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, + by simp [hlen], + by + intro i hi + simp only [Array.get_push] + split + . apply hrefs + omega + . apply AIG.Ref.hgate + ⟩ + +@[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] + +-- 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] + +theorem get_push_ref_lt (s : RefVec aig len) (ref : AIG.Ref aig) (idx : Nat) + (hidx : idx < len) : + (s.push ref).get idx (by omega) = s.get idx hidx := by + simp only [get, push, Ref.mk.injEq] + cases ref + simp only [Ref.mk.injEq] + rw [Array.get_push_lt] + +@[simp] +theorem get_cast {aig1 aig2 : AIG α} (s : RefVec aig1 len) (idx : Nat) (hidx : idx < len) + (hcast : aig1.decls.size ≤ aig2.decls.size) : + (s.cast hcast).get idx hidx + = + (s.get idx hidx).cast hcast := by + simp [cast, cast', get] + +@[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 + ⟨ + lrefs ++ rrefs, + by simp [Array.size_append, hl1, hr1], + by + intro i h + by_cases hsplit : i < lrefs.size + . rw [Array.get_append_left] + apply hl2 + omega + . rw [Array.get_append_right] + . apply hr2 + omega + . omega + ⟩ + +theorem get_append (lhs : RefVec aig lw) (rhs : RefVec aig rw) (idx : Nat) + (hidx : idx < lw + rw) : + (lhs.append rhs).get idx hidx + = + if h : idx < lw then + lhs.get idx h + else + rhs.get (idx - lw) (by omega) := by + simp only [get, append] + split + . simp [Ref.mk.injEq] + rw [Array.get_append_left] + . simp only [Ref.mk.injEq] + rw [Array.get_append_right] + . simp [lhs.hlen] + . rw [lhs.hlen] + omega + +@[inline] +def getD (s : RefVec aig len) (idx : Nat) (alt : Ref aig) : Ref aig := + if hidx : idx < len then + s.get idx hidx + else + alt + +theorem get_in_bound (s : RefVec aig len) (idx : Nat) (alt : Ref aig) (hidx : idx < len) : + s.getD idx alt = s.get idx hidx := by + unfold getD + simp [hidx] + +theorem get_out_bound (s : RefVec aig len) (idx : Nat) (alt : Ref aig) (hidx : len ≤ idx) : + s.getD idx alt = alt := by + unfold getD + split + . omega + . rfl + +end RefVec + +structure BinaryRefVec (aig : AIG α) (len : Nat) where + lhs : RefVec aig len + rhs : RefVec aig len + +namespace BinaryRefVec + +@[inline] +def cast {aig1 aig2 : AIG α} (s : BinaryRefVec aig1 len) + (h : aig1.decls.size ≤ aig2.decls.size) : + BinaryRefVec aig2 len := + let ⟨lhs, rhs⟩ := s + ⟨lhs.cast h, rhs.cast h⟩ + +@[simp] +theorem lhs_get_cast {aig1 aig2 : AIG α} (s : BinaryRefVec aig1 len) (idx : Nat) + (hidx : idx < len) (hcast : aig1.decls.size ≤ aig2.decls.size) : + (s.cast hcast).lhs.get idx hidx + = + (s.lhs.get idx hidx).cast hcast := by + simp [cast] + +@[simp] +theorem rhs_get_cast {aig1 aig2 : AIG α} (s : BinaryRefVec aig1 len) (idx : Nat) + (hidx : idx < len) (hcast : aig1.decls.size ≤ aig2.decls.size) : + (s.cast hcast).rhs.get idx hidx + = + (s.rhs.get idx hidx).cast hcast := by + simp [cast] + +end BinaryRefVec +end AIG + +end Sat +end Std diff --git a/src/Std/Sat/AIG/RefVecOperator.lean b/src/Std/Sat/AIG/RefVecOperator.lean new file mode 100644 index 0000000000..611f5c6a0e --- /dev/null +++ b/src/Std/Sat/AIG/RefVecOperator.lean @@ -0,0 +1,8 @@ +/- +Copyright (c) 2024 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Henrik Böving +-/ +import Std.Sat.AIG.RefVecOperator.Map +import Std.Sat.AIG.RefVecOperator.Zip +import Std.Sat.AIG.RefVecOperator.Fold diff --git a/src/Std/Sat/AIG/RefVecOperator/Fold.lean b/src/Std/Sat/AIG/RefVecOperator/Fold.lean new file mode 100644 index 0000000000..61648766cf --- /dev/null +++ b/src/Std/Sat/AIG/RefVecOperator/Fold.lean @@ -0,0 +1,195 @@ +/- +Copyright (c) 2024 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Henrik Böving +-/ +import Std.Sat.AIG.RefVec +import Std.Sat.AIG.LawfulVecOperator + +namespace Std +namespace Sat + +namespace AIG +namespace RefVec + +variable {α : Type} [Hashable α] [DecidableEq α] {aig : AIG α} + +structure FoldTarget (aig : AIG α) where + {len : Nat} + vec : RefVec aig len + func : (aig : AIG α) → BinaryInput aig → Entrypoint α + [lawful : LawfulOperator α BinaryInput func] + +attribute [instance] FoldTarget.lawful + +@[inline] +def FoldTarget.mkAnd {aig : AIG α} (vec : RefVec aig w) : FoldTarget aig where + vec := vec + func := mkAndCached + +@[specialize] +def fold (aig : AIG α) (target : FoldTarget aig) : Entrypoint α := + let res := aig.mkConstCached true + let aig := res.aig + let acc := res.ref + let input := target.vec.cast <| by + intros + apply LawfulOperator.le_size_of_le_aig_size (f := mkConstCached) + omega + go aig acc 0 target.len input target.func +where + @[specialize] + go (aig : AIG α) (acc : Ref aig) (idx : Nat) (len : Nat) (input : RefVec aig len) + (f : (aig : AIG α) → BinaryInput aig → Entrypoint α) [LawfulOperator α BinaryInput f] : + Entrypoint α := + if hidx : idx < len then + let res := f aig ⟨acc, input.get idx hidx⟩ + let aig := res.aig + let newAcc := res.ref + let input := input.cast <| by + intros + apply LawfulOperator.le_size_of_le_aig_size (f := f) + omega + go aig newAcc (idx + 1) len input f + else + ⟨aig, acc⟩ + termination_by len - idx + +theorem fold.go_le_size {aig : AIG α} (acc : Ref aig) (idx : Nat) (s : RefVec aig len) + (f : (aig : AIG α) → BinaryInput aig → Entrypoint α) [LawfulOperator α BinaryInput f] : + aig.decls.size ≤ (go aig acc idx len s f).1.decls.size := by + unfold go + split + . next h => + dsimp only + refine Nat.le_trans ?_ (by apply fold.go_le_size) + apply LawfulOperator.le_size + . simp + termination_by len - idx + +theorem fold_le_size {aig : AIG α} (target : FoldTarget aig) : + aig.decls.size ≤ (fold aig target).1.decls.size := by + unfold fold + dsimp only + refine Nat.le_trans ?_ (by apply fold.go_le_size) + apply LawfulOperator.le_size (f := mkConstCached) + +theorem fold.go_decl_eq {aig : AIG α} (acc : Ref aig) (i : Nat) (s : RefVec aig len) + (f : (aig : AIG α) → BinaryInput aig → Entrypoint α) [LawfulOperator α BinaryInput f] : + ∀ (idx : Nat) (h1) (h2), + (go aig acc i len s f).1.decls[idx]'h2 = aig.decls[idx]'h1 := by + generalize hgo : go aig acc i len s f = res + unfold go at hgo + split at hgo + . dsimp only at hgo + rw [← hgo] + intros + rw [go_decl_eq] + rw [LawfulOperator.decl_eq] + apply LawfulOperator.lt_size_of_lt_aig_size + assumption + . rw [← hgo] + intros + simp +termination_by len - i + +theorem fold_decl_eq {aig : AIG α} (target : FoldTarget aig) : + ∀ idx (h1 : idx < aig.decls.size) (h2), + (fold aig target).1.decls[idx]'h2 + = + aig.decls[idx]'h1 := by + intros + unfold fold + dsimp only + rw [fold.go_decl_eq] + rw [LawfulOperator.decl_eq (f := mkConstCached)] + apply LawfulOperator.lt_size_of_lt_aig_size (f := mkConstCached) + assumption + +instance : LawfulOperator α FoldTarget fold where + le_size := by intros; apply fold_le_size + decl_eq := by intros; apply fold_decl_eq + +namespace fold + +theorem denote_go_and {aig : AIG α} (acc : AIG.Ref aig) (curr : Nat) (hcurr : curr ≤ len) + (input : RefVec aig len) : + ⟦ + (go aig acc curr len input mkAndCached).aig, + (go aig acc curr len input mkAndCached).ref, + assign + ⟧ + = + ( + ⟦aig, acc, assign⟧ + ∧ + (∀ (idx : Nat) (hidx1 : idx < len), curr ≤ idx → ⟦aig, input.get idx hidx1, assign⟧) + ) := by + generalize hgo : go aig acc curr len input mkAndCached = res + unfold go at hgo + split at hgo + . dsimp only at hgo + rw [← hgo] + rw [denote_go_and] + . simp only [denote_projected_entry, denote_mkAndCached, Bool.and_eq_true, get_cast, + eq_iff_iff] + constructor + . intro h + rcases h with ⟨⟨h1, h2⟩, h3⟩ + constructor + . assumption + . intro idx hidx1 hidx2 + cases Nat.eq_or_lt_of_le hidx2 with + | inl heq => simpa [heq] using h2 + | inr hlt => + specialize h3 idx hidx1 (by omega) + rw [← h3] + rw [AIG.LawfulOperator.denote_mem_prefix (f := AIG.mkAndCached)] + . simp + . simp [Ref.hgate] + . simp only [and_imp] + intro hacc hrest + constructor + . simp [hacc, hrest] + . intro idx hidx1 hidx2 + specialize hrest idx hidx1 (by omega) + rw [← hrest] + rw [AIG.LawfulOperator.denote_mem_prefix (f := AIG.mkAndCached)] + . simp + . simp [Ref.hgate] + . omega + . rw [← hgo] + simp only [eq_iff_iff, iff_self_and] + omega +termination_by len - curr + +end fold + +@[simp] +theorem denote_fold_and {aig : AIG α} (s : RefVec aig len) : + ⟦(fold aig (FoldTarget.mkAnd s)), assign⟧ + ↔ + (∀ (idx : Nat) (hidx : idx < len), ⟦aig, s.get idx hidx, assign⟧) := by + unfold fold + simp only [FoldTarget.mkAnd] + rw [fold.denote_go_and] + . simp only [denote_projected_entry, mkConstCached_eval_eq_mkConst_eval, denote_mkConst, + Nat.zero_le, get_cast, Ref_cast', true_implies, true_and] + constructor + . intro h idx hidx + specialize h idx hidx + rw [AIG.LawfulOperator.denote_mem_prefix (f := mkConstCached)] at h + rw [← h] + . intro h idx hidx + specialize h idx hidx + rw [AIG.LawfulOperator.denote_mem_prefix (f := mkConstCached)] + . simp only [← h] + . apply RefVec.hrefs + simp [FoldTarget.mkAnd, hidx] + . omega + +end RefVec +end AIG + +end Sat +end Std diff --git a/src/Std/Sat/AIG/RefVecOperator/Map.lean b/src/Std/Sat/AIG/RefVecOperator/Map.lean new file mode 100644 index 0000000000..7a705eab85 --- /dev/null +++ b/src/Std/Sat/AIG/RefVecOperator/Map.lean @@ -0,0 +1,239 @@ +/- +Copyright (c) 2024 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Henrik Böving +-/ +import Std.Sat.AIG.RefVec +import Std.Sat.AIG.LawfulVecOperator + +namespace Std +namespace Sat + +namespace AIG +namespace RefVec + +variable {α : Type} [Hashable α] [DecidableEq α] {aig : AIG α} + +class LawfulMapOperator (α : Type) [Hashable α] [DecidableEq α] + (f : (aig : AIG α) → Ref aig → Entrypoint α) [LawfulOperator α Ref f] : Prop + where + chainable : ∀ (aig : AIG α) (input1 input2 : Ref aig) (h) (assign), + ⟦f (f aig input1).aig (input2.cast h), assign⟧ + = + ⟦f aig input2, assign⟧ + +namespace LawfulMapOperator + +@[simp] +theorem denote_prefix_cast_ref {aig : AIG α} {input1 input2 : Ref aig} + {f : (aig : AIG α) → Ref aig → Entrypoint α} [LawfulOperator α Ref f] [LawfulMapOperator α f] + {h} : + ⟦f (f aig input1).aig (input2.cast h), assign⟧ + = + ⟦f aig input2, assign⟧ := by + rw [LawfulMapOperator.chainable] + +instance : LawfulMapOperator α mkNotCached where + chainable := by + intros + simp only [Ref_cast', denote_mkNotCached] + rw [LawfulOperator.denote_mem_prefix (f := mkNotCached)] + +end LawfulMapOperator + +structure MapTarget (aig : AIG α) (len : Nat) where + vec : RefVec aig len + func : (aig : AIG α) → Ref aig → Entrypoint α + [lawful : LawfulOperator α Ref func] + [chainable : LawfulMapOperator α func] + +attribute [instance] MapTarget.lawful +attribute [instance] MapTarget.chainable + +@[specialize] +def map (aig : AIG α) (target : MapTarget aig len) : RefVecEntry α len := + go aig 0 (by omega) .empty target.vec target.func +where + @[specialize] + go {len : Nat} (aig : AIG α) (idx : Nat) (hidx : idx ≤ len) (s : RefVec aig idx) + (input : RefVec aig len) (f : (aig : AIG α) → Ref aig → Entrypoint α) + [LawfulOperator α Ref f] [LawfulMapOperator α f] : + RefVecEntry α len := + if hidx : idx < len then + let res := f aig (input.get idx hidx) + let aig := res.aig + let newRef := res.ref + have := by + intros + apply LawfulOperator.le_size_of_le_aig_size + omega + let input := input.cast this + let s := s.cast this + let s := s.push newRef + go aig (idx + 1) (by omega) s input f + else + have : idx = len := by omega + ⟨aig, this ▸ s⟩ + termination_by len - idx + +theorem map.go_le_size {aig : AIG α} (idx : Nat) (hidx) (s : RefVec aig idx) + (input : RefVec aig len) (f : (aig : AIG α) → Ref aig → Entrypoint α) + [LawfulOperator α Ref f] [LawfulMapOperator α f] : + aig.decls.size ≤ (go aig idx hidx s input f).aig.decls.size := by + unfold go + split + . next h => + dsimp only + refine Nat.le_trans ?_ (by apply map.go_le_size) + apply LawfulOperator.le_size + . simp + termination_by len - idx + +theorem map_le_size {aig : AIG α} (target : MapTarget aig len) : + aig.decls.size ≤ (map aig target).aig.decls.size := by + unfold map + apply map.go_le_size + +theorem map.go_decl_eq {aig : AIG α} (i) (hi) + (s : RefVec aig i) (input : RefVec aig len) (f : (aig : AIG α) → Ref aig → Entrypoint α) + [LawfulOperator α Ref f] [LawfulMapOperator α f] : + ∀ (idx : Nat) (h1) (h2), (go aig i hi s input f).1.decls[idx]'h2 = aig.decls[idx]'h1 := by + generalize hgo : go aig i hi s input f = res + unfold go at hgo + split at hgo + . dsimp only at hgo + rw [← hgo] + intros + rw [go_decl_eq] + rw [LawfulOperator.decl_eq] + apply LawfulOperator.lt_size_of_lt_aig_size + assumption + . dsimp only at hgo + rw [← hgo] + intros + simp +termination_by len - i + +theorem map_decl_eq {aig : AIG α} (target : MapTarget aig len) : + ∀ idx (h1 : idx < aig.decls.size) (h2), + (map aig target).1.decls[idx]'h2 + = + aig.decls[idx]'h1 := by + intros + unfold map + apply map.go_decl_eq + +instance : LawfulVecOperator α MapTarget map where + le_size := by intros; apply map_le_size + decl_eq := by intros; apply map_decl_eq + +namespace map + +theorem go_get_aux {aig : AIG α} (curr : Nat) (hcurr : curr ≤ len) (s : RefVec aig curr) + (input : RefVec aig len) (f : (aig : AIG α) → Ref aig → Entrypoint α) + [LawfulOperator α Ref f] [LawfulMapOperator α f] : + -- The hfoo here is a trick to make the dependent type gods happy. + ∀ (idx : Nat) (hidx : idx < curr) (hfoo), + (go aig curr hcurr s input f).vec.get idx (by omega) + = + (s.get idx hidx).cast hfoo := by + intro idx hidx + generalize hgo : go aig curr hcurr s input f = res + unfold go at hgo + split at hgo + . dsimp only at hgo + rw [← hgo] + intro hfoo + rw [go_get_aux] + rw [AIG.RefVec.get_push_ref_lt] + . simp only [Ref.cast, Ref.mk.injEq] + rw [AIG.RefVec.get_cast] + . simp + . assumption + . apply go_le_size + . dsimp only at hgo + rw [← hgo] + simp only [Nat.le_refl, get, Ref_cast', Ref.mk.injEq, true_implies] + have : curr = len := by omega + subst this + rfl +termination_by len - curr + +theorem go_get {aig : AIG α} (curr : Nat) (hcurr : curr ≤ len) (s : RefVec aig curr) + (input : RefVec aig len) (f : (aig : AIG α) → Ref aig → Entrypoint α) + [LawfulOperator α Ref f] [LawfulMapOperator α f] : + ∀ (idx : Nat) (hidx : idx < curr), + (go aig curr hcurr s input f).vec.get idx (by omega) + = + (s.get idx hidx).cast (by apply go_le_size) := by + intros + apply go_get_aux + +theorem go_denote_mem_prefix {aig : AIG α} (curr : Nat) (hcurr : curr ≤ len) + (s : RefVec aig curr) (input : RefVec aig len) + (f : (aig : AIG α) → Ref aig → Entrypoint α) [LawfulOperator α Ref f] [LawfulMapOperator α f] + (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⟩, + assign + ⟧ + = + ⟦aig, ⟨start, hstart⟩, assign⟧ := by + apply denote.eq_of_isPrefix (entry := ⟨aig, start,hstart⟩) + apply IsPrefix.of + . intros + apply go_decl_eq + . intros + apply go_le_size + +theorem denote_go {aig : AIG α} (curr : Nat) (hcurr : curr ≤ len) (s : RefVec aig curr) + (input : RefVec aig len) (f : (aig : AIG α) → Ref aig → Entrypoint α) + [LawfulOperator α Ref f] [LawfulMapOperator α f] : + ∀ (idx : Nat) (hidx1 : idx < len), + curr ≤ idx + → + ⟦(go aig curr hcurr s input f).aig, (go aig curr hcurr s input f).vec.get idx hidx1, assign⟧ + = + ⟦f aig (input.get idx hidx1), assign⟧ := by + intro idx hidx1 hidx2 + generalize hgo : go aig curr hcurr s input f = res + unfold go at hgo + split at hgo + . dsimp only at hgo + cases Nat.eq_or_lt_of_le hidx2 with + | inl heq => + rw [← hgo] + rw [go_get] + rw [AIG.RefVec.get_push_ref_eq'] + . simp only [← heq] + rw [go_denote_mem_prefix] + . simp + . simp [Ref.hgate] + . rw [heq] + | inr hlt => + rw [← hgo] + rw [denote_go] + . simp [get_cast, -Ref_cast'] + . omega + . omega +termination_by len - curr + +end map + +@[simp] +theorem denote_map {aig : AIG α} (target : MapTarget aig len) : + ∀ (idx : Nat) (hidx : idx < len), + ⟦(map aig target).aig, (map aig target).vec.get idx hidx, assign⟧ + = + ⟦target.func aig (target.vec.get idx hidx), assign⟧ := by + intro idx hidx + unfold map + apply map.denote_go + omega + +end RefVec +end AIG + +end Sat +end Std diff --git a/src/Std/Sat/AIG/RefVecOperator/Zip.lean b/src/Std/Sat/AIG/RefVecOperator/Zip.lean new file mode 100644 index 0000000000..e15a72a3ed --- /dev/null +++ b/src/Std/Sat/AIG/RefVecOperator/Zip.lean @@ -0,0 +1,269 @@ +/- +Copyright (c) 2024 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Henrik Böving +-/ +import Std.Sat.AIG.RefVec +import Std.Sat.AIG.LawfulVecOperator + +namespace Std +namespace Sat + +namespace AIG +namespace RefVec + +variable {α : Type} [Hashable α] [DecidableEq α] {aig : AIG α} + +class LawfulZipOperator (α : Type) [Hashable α] [DecidableEq α] + (f : (aig : AIG α) → BinaryInput aig → Entrypoint α) [LawfulOperator α BinaryInput f] : Prop + where + chainable : ∀ (aig : AIG α) (input1 input2 : BinaryInput aig) (h) (assign), + ⟦f (f aig input1).aig (input2.cast h), assign⟧ + = + ⟦f aig input2, assign⟧ + +namespace LawfulZipOperator + +@[simp] +theorem denote_prefix_cast_ref {aig : AIG α} {input1 input2 : BinaryInput aig} + {f : (aig : AIG α) → BinaryInput aig → Entrypoint α} [LawfulOperator α BinaryInput f] + [LawfulZipOperator α f] {h} : + ⟦f (f aig input1).aig (input2.cast h), assign⟧ + = + ⟦f aig input2, assign⟧ := by + rw [LawfulZipOperator.chainable] + +instance : LawfulZipOperator α mkAndCached where + chainable := by + intros + simp only [BinaryInput.cast, Ref_cast', denote_mkAndCached] + rw [LawfulOperator.denote_mem_prefix (f := mkAndCached)] + rw [LawfulOperator.denote_mem_prefix (f := mkAndCached)] + +instance : LawfulZipOperator α mkOrCached where + chainable := by + intros + simp only [BinaryInput.cast, Ref_cast', denote_mkOrCached] + rw [LawfulOperator.denote_mem_prefix (f := mkOrCached)] + rw [LawfulOperator.denote_mem_prefix (f := mkOrCached)] + +instance : LawfulZipOperator α mkXorCached where + chainable := by + intros + simp only [BinaryInput.cast, Ref_cast', denote_mkXorCached] + rw [LawfulOperator.denote_mem_prefix (f := mkXorCached)] + rw [LawfulOperator.denote_mem_prefix (f := mkXorCached)] + +instance : LawfulZipOperator α mkBEqCached where + chainable := by + intros + simp only [BinaryInput.cast, Ref_cast', denote_mkBEqCached] + rw [LawfulOperator.denote_mem_prefix (f := mkBEqCached)] + rw [LawfulOperator.denote_mem_prefix (f := mkBEqCached)] + +instance : LawfulZipOperator α mkImpCached where + chainable := by + intros + simp only [BinaryInput.cast, Ref_cast', denote_mkImpCached] + rw [LawfulOperator.denote_mem_prefix (f := mkImpCached)] + rw [LawfulOperator.denote_mem_prefix (f := mkImpCached)] + +end LawfulZipOperator + +structure ZipTarget (aig : AIG α) (len : Nat) where + input : BinaryRefVec aig len + func : (aig : AIG α) → BinaryInput aig → Entrypoint α + [lawful : LawfulOperator α BinaryInput func] + [chainable : LawfulZipOperator α func] + +attribute [instance] ZipTarget.lawful +attribute [instance] ZipTarget.chainable + +@[specialize] +def zip (aig : AIG α) (target : ZipTarget aig len) : RefVecEntry α len := + go aig 0 .empty (by omega) target.input.lhs target.input.rhs target.func +where + @[specialize] + go (aig : AIG α) (idx : Nat) (s : RefVec aig idx) (hidx : idx ≤ len) + (lhs rhs : RefVec aig len) (f : (aig : AIG α) → BinaryInput aig → Entrypoint α) + [LawfulOperator α BinaryInput f] [chainable : LawfulZipOperator α f] : + RefVecEntry α len := + if hidx : idx < len then + let res := f aig ⟨lhs.get idx hidx, rhs.get idx hidx⟩ + let aig := res.aig + let newRef := res.ref + have := by + intros + apply LawfulOperator.le_size_of_le_aig_size + omega + let s := s.cast this + let s := s.push newRef + go aig (idx + 1) s (by omega) (lhs.cast this) (rhs.cast this) f + else + have : idx = len := by omega + ⟨aig, this ▸ s⟩ + termination_by len - idx + +theorem zip.go_le_size {aig : AIG α} (idx : Nat) (hidx) (s : RefVec aig idx) + (lhs rhs : RefVec aig len) + (f : (aig : AIG α) → BinaryInput aig → Entrypoint α) [LawfulOperator α BinaryInput f] + [chainable : LawfulZipOperator α f] : + aig.decls.size ≤ (go aig idx s hidx lhs rhs f).1.decls.size := by + unfold go + split + . dsimp only + refine Nat.le_trans ?_ (by apply zip.go_le_size) + apply LawfulOperator.le_size + . simp + termination_by len - idx + +theorem zip_le_size {aig : AIG α} (target : ZipTarget aig len) : + aig.decls.size ≤ (zip aig target).1.decls.size := by + unfold zip + apply zip.go_le_size + +theorem zip.go_decl_eq {aig : AIG α} (i) (hi) (lhs rhs : RefVec aig len) + (s : RefVec aig i) (f : (aig : AIG α) → BinaryInput aig → Entrypoint α) + [LawfulOperator α BinaryInput f] [chainable : LawfulZipOperator α f] : + ∀ (idx : Nat) (h1) (h2), (go aig i s hi lhs rhs f).1.decls[idx]'h2 = aig.decls[idx]'h1 := by + generalize hgo : go aig i s hi lhs rhs f = res + unfold go at hgo + split at hgo + . dsimp only at hgo + rw [← hgo] + intros + intros + rw [go_decl_eq] + rw [LawfulOperator.decl_eq] + apply LawfulOperator.lt_size_of_lt_aig_size + assumption + . dsimp only at hgo + rw [← hgo] + intros + simp +termination_by len - i + +theorem zip_decl_eq {aig : AIG α} (target : ZipTarget aig len) : + ∀ idx (h1 : idx < aig.decls.size) (h2), + (zip aig target).1.decls[idx]'h2 = aig.decls[idx]'h1 := by + intros + unfold zip + apply zip.go_decl_eq + +instance : LawfulVecOperator α ZipTarget zip where + le_size := by intros; apply zip_le_size + decl_eq := by intros; apply zip_decl_eq + +namespace zip + +theorem go_get_aux {aig : AIG α} (curr : Nat) (hcurr : curr ≤ len) (s : RefVec aig curr) + (lhs rhs : RefVec aig len) (f : (aig : AIG α) → BinaryInput aig → Entrypoint α) + [LawfulOperator α BinaryInput f] [chainable : LawfulZipOperator α f] : + -- The hfoo here is a trick to make the dependent type gods happy + ∀ (idx : Nat) (hidx : idx < curr) (hfoo), + (go aig curr s hcurr lhs rhs f).vec.get idx (by omega) + = + (s.get idx hidx).cast hfoo := by + intro idx hidx + generalize hgo : go aig curr s hcurr lhs rhs f = res + unfold go at hgo + split at hgo + . dsimp only at hgo + rw [← hgo] + intro hfoo + rw [go_get_aux] + rw [AIG.RefVec.get_push_ref_lt] + . simp only [Ref.cast, Ref.mk.injEq] + rw [AIG.RefVec.get_cast] + . simp + . assumption + . apply go_le_size + . dsimp only at hgo + rw [← hgo] + simp only [Nat.le_refl, get, Ref_cast', Ref.mk.injEq, true_implies] + have : curr = len := by omega + subst this + simp +termination_by len - curr + +theorem go_get {aig : AIG α} (curr : Nat) (hcurr : curr ≤ len) (s : RefVec aig curr) + (lhs rhs : RefVec aig len) (f : (aig : AIG α) → BinaryInput aig → Entrypoint α) + [LawfulOperator α BinaryInput f] [chainable : LawfulZipOperator α f] : + ∀ (idx : Nat) (hidx : idx < curr), + (go aig curr s hcurr lhs rhs f).vec.get idx (by omega) + = + (s.get idx hidx).cast (by apply go_le_size) := by + intros + apply go_get_aux + +theorem go_denote_mem_prefix {aig : AIG α} (curr : Nat) (hcurr : curr ≤ len) + (s : RefVec aig curr) (lhs rhs : RefVec aig len) + (f : (aig : AIG α) → BinaryInput aig → Entrypoint α) [LawfulOperator α BinaryInput f] + [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⟩, + assign + ⟧ + = + ⟦aig, ⟨start, hstart⟩, assign⟧ := by + apply denote.eq_of_isPrefix (entry := ⟨aig, start,hstart⟩) + apply IsPrefix.of + . intros + apply go_decl_eq + . intros + apply go_le_size + +theorem denote_go {aig : AIG α} (curr : Nat) (hcurr : curr ≤ len) (s : RefVec aig curr) + (lhs rhs : RefVec aig len) (f : (aig : AIG α) → BinaryInput aig → Entrypoint α) + [LawfulOperator α BinaryInput f] [chainable : LawfulZipOperator α f] : + ∀ (idx : Nat) (hidx1 : idx < len), + curr ≤ idx + → + ⟦ + (go aig curr s hcurr lhs rhs f).aig, + (go aig curr s hcurr lhs rhs f).vec.get idx hidx1, + assign + ⟧ + = + ⟦f aig ⟨lhs.get idx hidx1, rhs.get idx hidx1⟩, assign⟧ := by + intro idx hidx1 hidx2 + generalize hgo : go aig curr s hcurr lhs rhs f = res + unfold go at hgo + split at hgo + . dsimp only at hgo + cases Nat.eq_or_lt_of_le hidx2 with + | inl heq => + rw [← hgo] + rw [go_get] + rw [AIG.RefVec.get_push_ref_eq'] + . simp only [← heq] + rw [go_denote_mem_prefix] + . simp + . simp [Ref.hgate] + . rw [heq] + | inr hlt => + rw [← hgo] + rw [denote_go] + . simp [-Ref_cast'] + . omega + . omega +termination_by len - curr + +end zip + +@[simp] +theorem denote_zip {aig : AIG α} (target : ZipTarget aig len) : + ∀ (idx : Nat) (hidx : idx < len), + ⟦(zip aig target).aig, (zip aig target).vec.get idx hidx, assign⟧ + = + ⟦target.func aig ⟨target.input.lhs.get idx hidx, target.input.rhs.get idx hidx⟩, assign⟧ := by + intros + apply zip.denote_go + omega + +end RefVec +end AIG + +end Sat +end Std diff --git a/src/Std/Sat/AIG/Relabel.lean b/src/Std/Sat/AIG/Relabel.lean new file mode 100644 index 0000000000..bb8c6c243a --- /dev/null +++ b/src/Std/Sat/AIG/Relabel.lean @@ -0,0 +1,175 @@ +/- +Copyright (c) 2024 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Henrik Böving +-/ +import Std.Sat.AIG.Basic +import Std.Sat.AIG.Lemmas + +namespace Std +namespace Sat + +namespace AIG + +namespace Decl + +def relabel (r : α → β) (decl : Decl α) : Decl β := + match decl with + | .const b => .const b + | .atom a => .atom (r a) + | .gate lhs rhs linv rinv => .gate lhs rhs linv rinv + +theorem relabel_id_map (decl : Decl α) : relabel id decl = decl := by + simp only [relabel, id_eq] + cases decl <;> rfl + +theorem relabel_comp (decl : Decl α) (g : α → β) (h : β → γ) : + relabel (h ∘ g) decl = relabel h (relabel g decl) := by + cases decl <;> rfl + +theorem relabel_const {decls : Array (Decl α)} {r : α → β} {hidx : idx < decls.size} + (h : relabel r decls[idx] = .const b) : + decls[idx] = (.const b) := by + unfold relabel at h + split at h <;> simp_all + +theorem relabel_atom {decls : Array (Decl α)} {r : α → β} {hidx : idx < decls.size} + (h : relabel r decls[idx] = .atom a) : + ∃ x, decls[idx] = .atom x ∧ a = r x := by + unfold relabel at h + split at h + . contradiction + . next x heq => + injection h with h + exists x + simp [heq, h] + . contradiction + +theorem relabel_gate {decls : Array (Decl α)} {r : α → β} {hidx : idx < decls.size} + (h : relabel r decls[idx] = .gate lhs rhs linv rinv) : + decls[idx] = (.gate lhs rhs linv rinv : Decl α) := by + unfold relabel at h + split at h <;> simp_all + +end Decl + +variable {α : Type} [Hashable α] [DecidableEq α] +variable {β : Type} [Hashable β] [DecidableEq β] + +def relabel (r : α → β) (aig : AIG α) : AIG β := + let decls := aig.decls.map (Decl.relabel r) + let cache := Cache.empty decls + { + decls, + cache, + invariant := by + intro idx lhs rhs linv rinv hbound hgate + simp [decls] at hgate + have := Decl.relabel_gate hgate + apply aig.invariant + assumption + } + +@[simp] +theorem relabel_size_eq_size {aig : AIG α} {r : α → β} : + (aig.relabel r).decls.size = aig.decls.size := by + simp [relabel] + +theorem relabel_const {aig : AIG α} {r : α → β} {hidx : idx < (relabel r aig).decls.size} + (h : (relabel r aig).decls[idx]'hidx = .const b) : + aig.decls[idx]'(by rw [← relabel_size_eq_size (r := r)]; omega) = .const b := by + apply Decl.relabel_const + simpa [relabel] using h + + +theorem relabel_atom {aig : AIG α} {r : α → β} {hidx : idx < (relabel r aig).decls.size} + (h : (relabel r aig).decls[idx]'hidx = .atom a) : + ∃ x, aig.decls[idx]'(by rw [← relabel_size_eq_size (r := r)]; omega) = .atom x ∧ a = r x := by + apply Decl.relabel_atom + simpa [relabel] using h + +theorem relabel_gate {aig : AIG α} {r : α → β} {hidx : idx < (relabel r aig).decls.size} + (h : (relabel r aig).decls[idx]'hidx = .gate lhs rhs linv rinv) : + aig.decls[idx]'(by rw [← relabel_size_eq_size (r := r)]; omega) = .gate lhs rhs linv rinv := by + apply Decl.relabel_gate + simpa [relabel] using h + +@[simp] +theorem denote_relabel (aig : AIG α) (r : α → β) (start : Nat) {hidx} + (assign : β → Bool) : + ⟦aig.relabel r, ⟨start, hidx⟩, assign⟧ + = + ⟦aig, ⟨start, by rw [← relabel_size_eq_size (r := r)]; omega⟩, (assign ∘ r)⟧ := by + apply denote_idx_trichotomy + . intro b heq1 + have heq2 := relabel_const heq1 + rw [denote_idx_const heq1] + rw [denote_idx_const heq2] + . intro a heq1 + rw [denote_idx_atom heq1] + rcases relabel_atom heq1 with ⟨x, ⟨hlx, hrx⟩⟩ + rw [hrx] at heq1 + rw [denote_idx_atom hlx] + simp [hrx] + . intro lhs rhs linv rinv heq1 + have heq2 := relabel_gate heq1 + rw [denote_idx_gate heq1] + rw [denote_idx_gate heq2] + have := aig.invariant (by rw [← relabel_size_eq_size (r := r)]; omega) heq2 + rw [denote_relabel aig r lhs assign] + 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 + 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 + constructor + . intro h assign + let g : β → α := fun b => + have em := Classical.propDecidable + if h : ∃ a, a ∈ aig ∧ r a = b then h.choose else Classical.choice inferInstance + have h' := unsat_relabel g h + specialize h' assign + simp only [denote_relabel] at h' + rw [← h'] + apply denote_congr + . intro a hmem + simp only [Function.comp_apply, g] + split + . next h => + rcases Exists.choose_spec h with ⟨_, heq⟩ + specialize hinj _ _ (by assumption) (by assumption) heq + simp [hinj] + . next h => + simp only [not_exists, not_and] at h + specialize h a hmem + contradiction + . apply unsat_relabel + +namespace Entrypoint + +def relabel (r : α → β) (entry : Entrypoint α) : Entrypoint β := + { entry with + aig := entry.aig.relabel r + ref.hgate := by simp [entry.ref.hgate] + } + +@[simp] +theorem relabel_size_eq {entry : Entrypoint α} {r : α → β} : + (entry.relabel r).aig.decls.size = entry.aig.decls.size := by + simp [relabel] + +theorem relabel_unsat_iff [Nonempty α] {entry : Entrypoint α} {r : α → β} + (hinj : ∀ x y, x ∈ entry.aig → y ∈ entry.aig → r x = r y → x = y) : + (entry.relabel r).Unsat ↔ entry.Unsat := by + simp [relabel, Unsat] + rw [AIG.relabel_unsat_iff] + assumption + +end Entrypoint +end AIG diff --git a/src/Std/Sat/AIG/RelabelNat.lean b/src/Std/Sat/AIG/RelabelNat.lean new file mode 100644 index 0000000000..88e1d07287 --- /dev/null +++ b/src/Std/Sat/AIG/RelabelNat.lean @@ -0,0 +1,386 @@ +/- +Copyright (c) 2024 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Henrik Böving +-/ +import Std.Sat.AIG.Relabel + + +namespace Std +namespace Sat + +variable {α : Type} [DecidableEq α] [Hashable α] + +namespace AIG +namespace RelabelNat +namespace State + +/-- +This invariant ensures that we only insert an atom at most once and with a monotonically increasing +index. +-/ +inductive Inv1 : Nat → HashMap α Nat → Prop where +| empty : Inv1 0 {} +| insert (hinv : Inv1 n map) (hfind : map[x]? = none) : Inv1 (n + 1) (map.insert x n) + +theorem Inv1.lt_of_get?_eq_some [EquivBEq α] {n m : Nat} (map : HashMap α Nat) (x : α) + (hinv : Inv1 n map) : + map[x]? = some m → m < n := by + induction hinv with + | empty => simp + | insert ih1 ih2 ih3 => + rename_i y + rw [Std.HashMap.getElem?_insert] + match hx : x == y with + | true => + simp only [beq_iff_eq] at hx + simp only [hx, beq_self_eq_true, ↓reduceIte, Option.some.injEq] + omega + | false => + simp only [BEq.symm_false hx, Bool.false_eq_true, ↓reduceIte] + intro h + specialize ih3 h + omega + +/-- +If a HashMap fulfills `Inv1` it is in an injection. +-/ +theorem Inv1.property [EquivBEq α] {n m : Nat} (x y : α) (map : HashMap α Nat) (hinv : Inv1 n map) + (hfound1 : map[x]? = some m) (hfound2 : map[y]? = some m) : x = y := by + induction hinv with + | empty => simp at hfound1 + | insert ih1 _ih2 ih3 => + rename_i z + rw [HashMap.getElem?_insert] at hfound1 + rw [HashMap.getElem?_insert] at hfound2 + match hx : z == x with + | false => + simp only [beq_eq_false_iff_ne, ne_eq] at hx + simp only [beq_iff_eq, hx, ↓reduceIte] at hfound1 + match hy : z == y with + | false => + simp only [beq_eq_false_iff_ne, ne_eq] at hy + simp only [beq_iff_eq, hy, ↓reduceIte] at hfound2 + exact ih3 hfound1 hfound2 + | true => + simp only [hy, ↓reduceIte, Option.some.injEq] at hfound2 + have := Inv1.lt_of_get?_eq_some _ _ ih1 hfound1 + omega + | true => + simp only [hx, ↓reduceIte, Option.some.injEq] at hfound1 + rcases hfound1 with ⟨rfl⟩ + match hy : z == y with + | false => + simp only [beq_eq_false_iff_ne, ne_eq] at hy + simp only [beq_iff_eq, hy, ↓reduceIte] at hfound2 + have := Inv1.lt_of_get?_eq_some _ _ ih1 hfound2 + omega + | true => + simp only [beq_iff_eq] at hx hy + simp only [←hx, hy] + +/-- +This invariant says that we have already visited and inserted all nodes up to a certain index. +-/ +inductive Inv2 (decls : Array (Decl α)) : Nat → HashMap α Nat → Prop where +| empty : Inv2 decls 0 {} +| newAtom (hinv : Inv2 decls idx map) (hlt : idx < decls.size) (hatom : decls[idx] = .atom a) + (hmap : map[a]? = none) : Inv2 decls (idx + 1) (map.insert a val) +| oldAtom (hinv : Inv2 decls idx map) (hlt : idx < decls.size) (hatom : decls[idx] = .atom a) + (hmap : map[a]? = some n) : Inv2 decls (idx + 1) map +| const (hinv : Inv2 decls idx map) (hlt : idx < decls.size) (hatom : decls[idx] = .const b) : + Inv2 decls (idx + 1) map +| gate (hinv : Inv2 decls idx map) (hlt : idx < decls.size) (hatom : decls[idx] = .gate l r li ri) : + Inv2 decls (idx + 1) map + +theorem Inv2.upper_lt_size {decls : Array (Decl α)} (hinv : Inv2 decls upper map) : + upper ≤ decls.size := by + cases hinv <;> omega + +/-- +The key property provided by `Inv2`, if we have `Inv2` at a certain index, then all atoms below +that index have been inserted into the `HashMap`. +-/ +theorem Inv2.property (decls : Array (Decl α)) (idx upper : Nat) (map : HashMap α Nat) + (hidx : idx < upper) (a : α) (hinv : Inv2 decls upper map) + (heq : decls[idx]'(by have := upper_lt_size hinv; omega) = .atom a) : + ∃ n, map[a]? = some n := by + induction hinv with + | empty => omega + | newAtom ih1 ih2 ih3 ih4 ih5 => + next idx' _ a' _ => + replace hidx : idx ≤ idx' := by omega + rw [HashMap.getElem?_insert] + match heq2 : a' == a with + | false => + simp only [Bool.false_eq_true, ↓reduceIte] + cases Nat.eq_or_lt_of_le hidx with + | inl hidxeq => + subst hidxeq + simp_all only [beq_eq_false_iff_ne, Decl.atom.injEq] + | inr hlt => + exact ih5 hlt heq + | true => + exact Option.isSome_iff_exists.mp rfl + | oldAtom ih1 ih2 ih3 ih4 ih5 => + simp_all only [true_implies] + next idx' _ _ _ => + replace hidx : idx ≤ idx' := by omega + cases Nat.eq_or_lt_of_le hidx with + | inl hidxeq => + simp only [hidxeq, ih3, Decl.atom.injEq] at heq + rw [← heq] + apply Exists.intro + assumption + | inr hlt => apply ih5 <;> assumption + | const ih1 ih2 ih3 ih4 => + next idx' _ _ => + replace hidx : idx ≤ idx' := by omega + cases Nat.eq_or_lt_of_le hidx with + | inl hidxeq => simp only [hidxeq, ih3] at heq + | inr hlt => apply ih4 <;> assumption + | gate ih1 ih2 ih3 ih4 => + next idx' _ _ _ _ _ => + replace hidx : idx ≤ idx' := by omega + cases Nat.eq_or_lt_of_le hidx with + | inl hidxeq => simp [hidxeq, ih3] at heq + | inr hlt => apply ih4 <;> assumption + +end State + +/-- +The invariant carrying state structure for building the `HashMap` that translates from arbitrary +atom identifiers to `Nat`. +-/ +structure State (α : Type) [DecidableEq α] [Hashable α] (decls : Array (Decl α)) (idx : Nat) where + /-- + The next number to use for identifying an atom. + -/ + max : Nat + /-- + The translation `HashMap` + -/ + map : HashMap α Nat + /-- + Proof that we never reuse a number. + -/ + inv1 : State.Inv1 max map + /-- + Proof that we inserted all atoms until `idx`. + -/ + inv2 : State.Inv2 decls idx map + +namespace State + +/-- +The basic initial state. +-/ +def empty {decls : Array (Decl α)} : State α decls 0 := + { max := 0, map := {}, inv1 := Inv1.empty, inv2 := Inv2.empty } + +/-- +Insert a `Decl.atom` into the `State` structure. +-/ +def addAtom {decls : Array (Decl α)} {hidx} (state : State α decls idx) (a : α) + (h : decls[idx]'hidx = .atom a) : + State α decls (idx + 1) := + match hmap : state.map[a]? with + | some _ => + { state with + inv2 := by + apply Inv2.oldAtom + . exact state.inv2 + . assumption + . assumption + } + | none => + { + max := state.max + 1 + map := state.map.insert a state.max + inv1 := by + apply State.Inv1.insert + . exact state.inv1 + . assumption + inv2 := by + apply Inv2.newAtom + . exact state.inv2 + . assumption + . assumption + } + +/-- +Insert a `Decl.const` into the `State` structure. +-/ +def addConst {decls : Array (Decl α)} {hidx} (state : State α decls idx) (b : Bool) + (h : decls[idx]'hidx = .const b) : + State α decls (idx + 1) := + { state with + inv2 := by + apply Inv2.const + . exact state.inv2 + . assumption + } + +/-- +Insert a `Decl.gate` into the `State` structure. +-/ +def addGate {decls : Array (Decl α)} {hidx} (state : State α decls idx) (lhs rhs : Nat) + (linv rinv : Bool) (h : decls[idx]'hidx = .gate lhs rhs linv rinv) : + State α decls (idx + 1) := + { state with + inv2 := by + apply Inv2.gate + . exact state.inv2 + . assumption + } + +/-- +Build up a `State` that has all atoms of an `AIG` inserted. +-/ +def ofAIGAux (aig : AIG α) : State α aig.decls aig.decls.size := + go aig.decls 0 .empty +where + go (decls : Array (Decl α)) (idx : Nat) (state : State α decls idx) : State α decls decls.size := + if hidx : idx < decls.size then + let decl := decls[idx] + match hdecl : decl with + | .atom a => go decls (idx + 1) (state.addAtom a hdecl) + | .const b => go decls (idx + 1) (state.addConst b hdecl) + | .gate lhs rhs linv rinv => go decls (idx + 1) (state.addGate lhs rhs linv rinv hdecl) + else + have : idx = decls.size := by + have := state.inv2.upper_lt_size + omega + this ▸ state + termination_by decls.size - idx + +/-- +Obtain the atom mapping from α to `Nat` for a given `AIG`. +-/ +def ofAIG (aig : AIG α) : HashMap α Nat := + ofAIGAux aig |>.map + +/-- +The map returned by `ofAIG` fulfills the `Inv1` property. +-/ +theorem ofAIG.Inv1 (aig : AIG α) : ∃ n, Inv1 n (ofAIG aig) := by + exists (ofAIGAux aig).max + dsimp only [ofAIG] + exact (ofAIGAux aig).inv1 + +/-- +The map returned by `ofAIG` fulfills the `Inv2` property. +-/ +theorem ofAIG.Inv2 (aig : AIG α) : Inv2 aig.decls aig.decls.size (ofAIG aig) := by + have := (ofAIGAux aig).inv2 + simp [ofAIG, this] + +/-- +Assuming that we find a `Nat` for an atom in the `ofAIG` map, that `Nat` is unique in the map. +-/ +theorem ofAIG_find_unique {aig : AIG α} (a : α) (ha : (ofAIG aig)[a]? = some n) : + ∀ a', (ofAIG aig)[a']? = some n → a = a' := by + intro a' ha' + rcases ofAIG.Inv1 aig with ⟨n, hn⟩ + apply Inv1.property <;> assumption + +/-- +We will find a `Nat` for every atom in the `AIG` that the `ofAIG` map was built from. +-/ +theorem ofAIG_find_some {aig : AIG α} : ∀ a ∈ aig, ∃ n, (ofAIG aig)[a]? = some n := by + intro a ha + simp only [mem_def] at ha + rcases Array.getElem_of_mem ha with ⟨i, isLt, hi⟩ + apply Inv2.property + . assumption + . exact aig.decls.size + . omega + · apply ofAIG.Inv2 + +end State +end RelabelNat + +def relabelNat' (aig : AIG α) : (AIG Nat × HashMap α Nat) := + let map := RelabelNat.State.ofAIG aig + let aig := aig.relabel fun x => + -- The none branch never gets hit, we prove this below. + match map[x]? with + | some var => var + | none => 0 + (aig, map) + +/-- +Map an `AIG` with arbitrary atom identifiers to one that uses `Nat` as atom identifiers. This is +useful for preparing an `AIG` for CNF translation if it doesn't already use `Nat` identifiers. +-/ +def relabelNat (aig : AIG α) : AIG Nat := + relabelNat' aig |>.fst + +@[simp] +theorem relabelNat'_fst_eq_relabelNat {aig : AIG α} : aig.relabelNat'.fst = aig.relabelNat := by + rfl + +@[simp] +theorem relabelNat_size_eq_size {aig : AIG α} : aig.relabelNat.decls.size = aig.decls.size := by + simp [relabelNat, relabelNat'] + +/-- +`relabelNat` preserves unsatisfiablility. +-/ +theorem relabelNat_unsat_iff [Nonempty α] {aig : AIG α} {hidx1} {hidx2} : + (aig.relabelNat).UnsatAt idx hidx1 ↔ aig.UnsatAt idx hidx2 := by + dsimp only [relabelNat, relabelNat'] + rw [relabel_unsat_iff] + intro x y hx hy heq + split at heq + . next hcase1 => + split at heq + . next hcase2 => + apply RelabelNat.State.ofAIG_find_unique + . assumption + . rw [heq] + assumption + . next hcase2 => + exfalso + rcases RelabelNat.State.ofAIG_find_some y hy with ⟨n, hn⟩ + simp [hcase2] at hn + . next hcase => + exfalso + rcases RelabelNat.State.ofAIG_find_some x hx with ⟨n, hn⟩ + simp [hcase] at hn + +namespace Entrypoint + +def relabelNat' (entry : Entrypoint α) : (Entrypoint Nat × HashMap α Nat) := + let res := entry.aig.relabelNat' + let entry := + { entry with + aig := res.fst, + ref.hgate := by simp [entry.ref.hgate, res] + } + (entry, res.snd) + +/-- +Map an `Entrypoint` with arbitrary atom identifiers to one that uses `Nat` as atom identifiers. +This is useful for preparing an `AIG` for CNF translation if it doesn't already use `Nat` +identifiers. +-/ +def relabelNat (entry : Entrypoint α) : Entrypoint Nat := + { entry with + aig := entry.aig.relabelNat + ref.hgate := by simp [entry.ref.hgate] + } + +/-- +`relabelNat` preserves unsatisfiablility. +-/ +theorem relabelNat_unsat_iff {entry : Entrypoint α} [Nonempty α] : + (entry.relabelNat).Unsat ↔ entry.Unsat:= by + simp only [Unsat, relabelNat] + rw [AIG.relabelNat_unsat_iff] + +end Entrypoint +end AIG + +end Sat +end Std