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 continuously 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.

source
def Std.Sat.AIG.mkIfCached {α : Type} [Hashable α] [DecidableEq α] (aig : AIG α) (input : aig.TernaryInput) :
Entrypoint α
Equations

- One or more equations did not get rendered due to their size.

Instances For

source
instance Std.Sat.AIG.instLawfulOperatorTernaryInputMkIfCached {α : Type} [Hashable α] [DecidableEq α] :
LawfulOperator α TernaryInput mkIfCached
source
theorem Std.Sat.AIG.if_as_bool (d l r : Bool) :
(if d = true then l else r) = (d && l || !d && r)
source
@[simp]
theorem Std.Sat.AIG.denote_mkIfCached {α : Type} [Hashable α] [DecidableEq α] {assign : α → Bool} {aig : AIG α} {input : aig.TernaryInput} :
⟦assign, aig.mkIfCached input⟧ = if ⟦assign, { aig := aig, ref := input.discr }⟧ = true then ⟦assign, { aig := aig, ref := input.lhs }⟧ else ⟦assign, { aig := aig, ref := input.rhs }⟧
source
structure Std.Sat.AIG.RefVec.IfInput {α : Type} [Hashable α] [DecidableEq α] (aig : AIG α) (w : Nat) :
Type

- discr : aig.Ref
- lhs : aig.RefVec w
- rhs : aig.RefVec w

Instances For

source
def Std.Sat.AIG.RefVec.ite {α : Type} [Hashable α] [DecidableEq α] {w : Nat} (aig : AIG α) (input : IfInput aig w) :
RefVecEntry α w
Equations

- Std.Sat.AIG.RefVec.ite aig { discr := discr, lhs := lhs, rhs := rhs } = Std.Sat.AIG.RefVec.ite.go aig 0 ⋯ discr lhs rhs (Std.Sat.AIG.RefVec.emptyWithCapacity w)

Instances For

source
@[irreducible]
def Std.Sat.AIG.RefVec.ite.go {α : Type} [Hashable α] [DecidableEq α] {w : Nat} (aig : AIG α) (curr : Nat) (hcurr : curr ≤ w) (discr : aig.Ref) (lhs rhs : aig.RefVec w) (s : aig.RefVec curr) :
RefVecEntry α w
Equations

- One or more equations did not get rendered due to their size.

Instances For

source
@[irreducible]
theorem Std.Sat.AIG.RefVec.ite.go_le_size {α : Type} [Hashable α] [DecidableEq α] {w : Nat} (aig : AIG α) (curr : Nat) (hcurr : curr ≤ w) (discr : aig.Ref) (lhs rhs : aig.RefVec w) (s : aig.RefVec curr) :
aig.decls.size ≤ (go aig curr hcurr discr lhs rhs s).aig.decls.size
source
@[irreducible]
theorem Std.Sat.AIG.RefVec.ite.go_decl_eq {α : Type} [Hashable α] [DecidableEq α] {w : Nat} (aig : AIG α) (curr : Nat) (hcurr : curr ≤ w) (discr : aig.Ref) (lhs rhs : aig.RefVec w) (s : aig.RefVec curr) (idx : Nat) (h1 : idx < aig.decls.size) (h2 : idx < (go aig curr hcurr discr lhs rhs s).aig.decls.size) :
(go aig curr hcurr discr lhs rhs s).aig.decls[idx] = aig.decls[idx]
source
instance Std.Sat.AIG.RefVec.instLawfulVecOperatorIfInputIte {α : Type} [Hashable α] [DecidableEq α] :
LawfulVecOperator α IfInput fun {len : Nat} => ite
source
@[irreducible]
theorem Std.Sat.AIG.RefVec.ite.go_get_aux {α : Type} [Hashable α] [DecidableEq α] {w : Nat} (aig : AIG α) (curr : Nat) (hcurr : curr ≤ w) (discr : aig.Ref) (lhs rhs : aig.RefVec w) (s : aig.RefVec curr) (idx : Nat) (hidx : idx < curr) (hfoo : aig.decls.size ≤ (go aig curr hcurr discr lhs rhs s).aig.decls.size) :
(go aig curr hcurr discr lhs rhs s).vec.get idx ⋯ = (s.get idx hidx).cast hfoo
source
theorem Std.Sat.AIG.RefVec.ite.go_get {α : Type} [Hashable α] [DecidableEq α] {w : Nat} (aig : AIG α) (curr : Nat) (hcurr : curr ≤ w) (discr : aig.Ref) (lhs rhs : aig.RefVec w) (s : aig.RefVec curr) (idx : Nat) (hidx : idx < curr) :
(go aig curr hcurr discr lhs rhs s).vec.get idx ⋯ = (s.get idx hidx).cast ⋯
source
theorem Std.Sat.AIG.RefVec.ite.go_denote_mem_prefix {α : Type} [Hashable α] [DecidableEq α] {assign : α → Bool} {inv : Bool} {w : Nat} (aig : AIG α) (curr : Nat) (hcurr : curr ≤ w) (discr : aig.Ref) (lhs rhs : aig.RefVec w) (s : aig.RefVec curr) (start : Nat) (hstart : start < aig.decls.size) :
⟦assign, { aig := (go aig curr hcurr discr lhs rhs s).aig, ref := { gate := start, invert := inv, hgate := ⋯ } }⟧ = ⟦assign, { aig := aig, ref := { gate := start, invert := inv, hgate := hstart } }⟧
source
@[irreducible]
theorem Std.Sat.AIG.RefVec.ite.denote_go {α : Type} [Hashable α] [DecidableEq α] {assign : α → Bool} {w : Nat} (aig : AIG α) (curr : Nat) (hcurr : curr ≤ w) (discr : aig.Ref) (lhs rhs : aig.RefVec w) (s : aig.RefVec curr) (idx : Nat) (hidx1 : idx < w) :
curr ≤ idx → ⟦assign, { aig := (go aig curr hcurr discr lhs rhs s).aig, ref := (go aig curr hcurr discr lhs rhs s).vec.get idx hidx1 }⟧ = if ⟦assign, { aig := aig, ref := discr }⟧ = true then ⟦assign, { aig := aig, ref := lhs.get idx hidx1 }⟧ else ⟦assign, { aig := aig, ref := rhs.get idx hidx1 }⟧
source
@[simp]
theorem Std.Sat.AIG.RefVec.denote_ite {α : Type} [Hashable α] [DecidableEq α] {w : Nat} {assign : α → Bool} {aig : AIG α} {input : IfInput aig w} (idx : Nat) (hidx : idx < w) :
⟦assign, { aig := (ite aig input).aig, ref := (ite aig input).vec.get idx hidx }⟧ = if ⟦assign, { aig := aig, ref := input.discr }⟧ = true then ⟦assign, { aig := aig, ref := input.lhs.get idx hidx }⟧ else ⟦assign, { aig := aig, ref := input.rhs.get idx hidx }⟧