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 Refs 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 LawfulVecOperators.

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

Equations

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

instance Std.Sat.AIG.instLawfulOperatorTernaryInputMkIfCached {α : Type} [Hashable α] [DecidableEq α] : Std.Sat.AIG.LawfulOperator α Std.Sat.AIG.TernaryInput Std.Sat.AIG.mkIfCached

Equations

• ⋯ = ⋯

theorem Std.Sat.AIG.if_as_bool (d l r : Bool) : (if d = true then l else r) = (d && l || !d && r)

@[simp]

theorem Std.Sat.AIG.denote_mkIfCached {α : Type} [Hashable α] [DecidableEq α] {assign : α → Bool} {aig : Std.Sat.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 }⟧

structure Std.Sat.AIG.RefVec.IfInput {α : Type} [Hashable α] [DecidableEq α] (aig : Std.Sat.AIG α) (w : Nat) : Type

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

def Std.Sat.AIG.RefVec.ite {α : Type} [Hashable α] [DecidableEq α] {w : Nat} (aig : Std.Sat.AIG α) (input : Std.Sat.AIG.RefVec.IfInput aig w) : Std.Sat.AIG.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.empty

@[irreducible]

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

Equations

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

@[irreducible]

theorem Std.Sat.AIG.RefVec.ite.go_le_size {α : Type} [Hashable α] [DecidableEq α] {w : Nat} (aig : Std.Sat.AIG α) (curr : Nat) (hcurr : curr ≤ w) (discr : aig.Ref) (lhs rhs : aig.RefVec w) (s : aig.RefVec curr) : aig.decls.size ≤ (Std.Sat.AIG.RefVec.ite.go aig curr hcurr discr lhs rhs s).aig.decls.size

@[irreducible]

theorem Std.Sat.AIG.RefVec.ite.go_decl_eq {α : Type} [Hashable α] [DecidableEq α] {w : Nat} (aig : Std.Sat.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 < (Std.Sat.AIG.RefVec.ite.go aig curr hcurr discr lhs rhs s).aig.decls.size) : (Std.Sat.AIG.RefVec.ite.go aig curr hcurr discr lhs rhs s).aig.decls[idx] = aig.decls[idx]

instance Std.Sat.AIG.RefVec.instLawfulVecOperatorIfInputIte {α : Type} [Hashable α] [DecidableEq α] : Std.Sat.AIG.LawfulVecOperator α Std.Sat.AIG.RefVec.IfInput fun {len : Nat} => Std.Sat.AIG.RefVec.ite

Equations

• ⋯ = ⋯

@[irreducible]

theorem Std.Sat.AIG.RefVec.ite.go_get_aux {α : Type} [Hashable α] [DecidableEq α] {w : Nat} (aig : Std.Sat.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 ≤ (Std.Sat.AIG.RefVec.ite.go aig curr hcurr discr lhs rhs s).aig.decls.size) : (Std.Sat.AIG.RefVec.ite.go aig curr hcurr discr lhs rhs s).vec.get idx ⋯ = (s.get idx hidx).cast hfoo

theorem Std.Sat.AIG.RefVec.ite.go_get {α : Type} [Hashable α] [DecidableEq α] {w : Nat} (aig : Std.Sat.AIG α) (curr : Nat) (hcurr : curr ≤ w) (discr : aig.Ref) (lhs rhs : aig.RefVec w) (s : aig.RefVec curr) (idx : Nat) (hidx : idx < curr) : (Std.Sat.AIG.RefVec.ite.go aig curr hcurr discr lhs rhs s).vec.get idx ⋯ = (s.get idx hidx).cast ⋯

theorem Std.Sat.AIG.RefVec.ite.go_denote_mem_prefix {α : Type} [Hashable α] [DecidableEq α] {assign : α → Bool} {w : Nat} (aig : Std.Sat.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 := (Std.Sat.AIG.RefVec.ite.go aig curr hcurr discr lhs rhs s).aig, ref := { gate := start, hgate := ⋯ } }⟧ = ⟦assign, { aig := aig, ref := { gate := start, hgate := hstart } }⟧

@[irreducible]

theorem Std.Sat.AIG.RefVec.ite.denote_go {α : Type} [Hashable α] [DecidableEq α] {assign : α → Bool} {w : Nat} (aig : Std.Sat.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 := (Std.Sat.AIG.RefVec.ite.go aig curr hcurr discr lhs rhs s).aig, ref := (Std.Sat.AIG.RefVec.ite.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 }⟧

@[simp]

theorem Std.Sat.AIG.RefVec.denote_ite {α : Type} [Hashable α] [DecidableEq α] {w : Nat} {assign : α → Bool} {aig : Std.Sat.AIG α} {input : Std.Sat.AIG.RefVec.IfInput aig w} (idx : Nat) (hidx : idx < w) : ⟦assign, { aig := (Std.Sat.AIG.RefVec.ite aig input).aig, ref := (Std.Sat.AIG.RefVec.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 }⟧