feat: Std.Sat.AIG (#4953)
Step 2/~7 in upstreaming LeanSAT. --------- Co-authored-by: Tobias Grosser <tobias@grosser.es> Co-authored-by: Siddharth <siddu.druid@gmail.com> Co-authored-by: Markus Himmel <markus@lean-fro.org> Co-authored-by: Kim Morrison <scott.morrison@gmail.com>
This commit is contained in:
Henrik Böving
GitHub
parent
c237c1f9fb
commit
dc3eccdf26
20 changed files with 4469 additions and 0 deletions
|
|
@ -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) :
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
19
src/Std/Sat/AIG.lean
Normal file
19
src/Std/Sat/AIG.lean
Normal file
|
|
@ -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
|
||||
510
src/Std/Sat/AIG/Basic.lean
Normal file
510
src/Std/Sat/AIG/Basic.lean
Normal file
|
|
@ -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
|
||||
725
src/Std/Sat/AIG/CNF.lean
Normal file
725
src/Std/Sat/AIG/CNF.lean
Normal file
|
|
@ -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
|
||||
132
src/Std/Sat/AIG/Cached.lean
Normal file
132
src/Std/Sat/AIG/Cached.lean
Normal file
|
|
@ -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
|
||||
175
src/Std/Sat/AIG/CachedGates.lean
Normal file
175
src/Std/Sat/AIG/CachedGates.lean
Normal file
|
|
@ -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
|
||||
268
src/Std/Sat/AIG/CachedGatesLemmas.lean
Normal file
268
src/Std/Sat/AIG/CachedGatesLemmas.lean
Normal file
|
|
@ -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
|
||||
340
src/Std/Sat/AIG/CachedLemmas.lean
Normal file
340
src/Std/Sat/AIG/CachedLemmas.lean
Normal file
|
|
@ -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
|
||||
300
src/Std/Sat/AIG/If.lean
Normal file
300
src/Std/Sat/AIG/If.lean
Normal file
|
|
@ -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
|
||||
155
src/Std/Sat/AIG/LawfulOperator.lean
Normal file
155
src/Std/Sat/AIG/LawfulOperator.lean
Normal file
|
|
@ -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
|
||||
87
src/Std/Sat/AIG/LawfulVecOperator.lean
Normal file
87
src/Std/Sat/AIG/LawfulVecOperator.lean
Normal file
|
|
@ -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
|
||||
290
src/Std/Sat/AIG/Lemmas.lean
Normal file
290
src/Std/Sat/AIG/Lemmas.lean
Normal file
|
|
@ -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
|
||||
188
src/Std/Sat/AIG/RefVec.lean
Normal file
188
src/Std/Sat/AIG/RefVec.lean
Normal file
|
|
@ -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
|
||||
8
src/Std/Sat/AIG/RefVecOperator.lean
Normal file
8
src/Std/Sat/AIG/RefVecOperator.lean
Normal file
|
|
@ -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
|
||||
195
src/Std/Sat/AIG/RefVecOperator/Fold.lean
Normal file
195
src/Std/Sat/AIG/RefVecOperator/Fold.lean
Normal file
|
|
@ -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
|
||||
239
src/Std/Sat/AIG/RefVecOperator/Map.lean
Normal file
239
src/Std/Sat/AIG/RefVecOperator/Map.lean
Normal file
|
|
@ -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
|
||||
269
src/Std/Sat/AIG/RefVecOperator/Zip.lean
Normal file
269
src/Std/Sat/AIG/RefVecOperator/Zip.lean
Normal file
|
|
@ -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
|
||||
175
src/Std/Sat/AIG/Relabel.lean
Normal file
175
src/Std/Sat/AIG/Relabel.lean
Normal file
|
|
@ -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
|
||||
386
src/Std/Sat/AIG/RelabelNat.lean
Normal file
386
src/Std/Sat/AIG/RelabelNat.lean
Normal file
|
|
@ -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
|
||||
Loading…
Add table
Reference in a new issue