source
class Std.Sat.AIG.RefVec.LawfulZipOperator (α : Type) [Hashable α] [DecidableEq α] (f : (aig : AIG α) → aig.BinaryInput → Entrypoint α) [LawfulOperator α BinaryInput f] :
Prop

- chainable (aig : AIG α) (input1 input2 : aig.BinaryInput) (h : aig.decls.size ≤ (f aig input1).aig.decls.size) (assign : α → Bool) : ⟦assign, f (f aig input1).aig (input2.cast h)⟧ = ⟦assign, f aig input2⟧

Instances

source
theorem Std.Sat.AIG.RefVec.LawfulZipOperator.denote_prefix_cast_ref {α : Type} [Hashable α] [DecidableEq α] {assign : α → Bool} {aig : AIG α} {input1 input2 : aig.BinaryInput} {f : (aig : AIG α) → aig.BinaryInput → Entrypoint α} [LawfulOperator α BinaryInput f] [LawfulZipOperator α f] {h : aig.decls.size ≤ (f aig input1).aig.decls.size} :
⟦assign, f (f aig input1).aig (input2.cast h)⟧ = ⟦assign, f aig input2⟧
source
instance Std.Sat.AIG.RefVec.LawfulZipOperator.instMkAndCached {α : Type} [Hashable α] [DecidableEq α] :
LawfulZipOperator α mkAndCached
source
instance Std.Sat.AIG.RefVec.LawfulZipOperator.instMkOrCached {α : Type} [Hashable α] [DecidableEq α] :
LawfulZipOperator α mkOrCached
source
instance Std.Sat.AIG.RefVec.LawfulZipOperator.instMkXorCached {α : Type} [Hashable α] [DecidableEq α] :
LawfulZipOperator α mkXorCached
source
instance Std.Sat.AIG.RefVec.LawfulZipOperator.instMkBEqCached {α : Type} [Hashable α] [DecidableEq α] :
LawfulZipOperator α mkBEqCached
source
instance Std.Sat.AIG.RefVec.LawfulZipOperator.instMkImpCached {α : Type} [Hashable α] [DecidableEq α] :
LawfulZipOperator α mkImpCached
source
@[specialize #[]]
def Std.Sat.AIG.RefVec.zip {α : Type} [Hashable α] [DecidableEq α] {len : Nat} (aig : AIG α) (input : aig.BinaryRefVec len) (func : (aig : AIG α) → aig.BinaryInput → Entrypoint α) [LawfulOperator α BinaryInput func] [LawfulZipOperator α func] :
RefVecEntry α len
Equations

- Std.Sat.AIG.RefVec.zip aig input func = Std.Sat.AIG.RefVec.zip.go aig 0 (Std.Sat.AIG.RefVec.emptyWithCapacity len) ⋯ input.lhs input.rhs func

Instances For

source
@[irreducible, specialize #[]]
def Std.Sat.AIG.RefVec.zip.go {α : Type} [Hashable α] [DecidableEq α] {len : Nat} (aig : AIG α) (idx : Nat) (s : aig.RefVec idx) (hidx : idx ≤ len) (lhs rhs : aig.RefVec len) (f : (aig : AIG α) → aig.BinaryInput → Entrypoint α) [LawfulOperator α BinaryInput f] [LawfulZipOperator α f] :
RefVecEntry α len
Equations

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

Instances For

source
@[irreducible]
theorem Std.Sat.AIG.RefVec.zip.go_le_size {α : Type} [Hashable α] [DecidableEq α] {len : Nat} {aig : AIG α} (idx : Nat) (hidx : idx ≤ len) (s : aig.RefVec idx) (lhs rhs : aig.RefVec len) (f : (aig : AIG α) → aig.BinaryInput → Entrypoint α) [LawfulOperator α BinaryInput f] [LawfulZipOperator α f] :
aig.decls.size ≤ (go aig idx s hidx lhs rhs f).aig.decls.size
source
theorem Std.Sat.AIG.RefVec.zip_le_size {α : Type} [Hashable α] [DecidableEq α] {len : Nat} (aig : AIG α) (input : aig.BinaryRefVec len) (func : (aig : AIG α) → aig.BinaryInput → Entrypoint α) [LawfulOperator α BinaryInput func] [LawfulZipOperator α func] :
aig.decls.size ≤ (zip aig input func).aig.decls.size
source
@[irreducible]
theorem Std.Sat.AIG.RefVec.zip.go_decl_eq {α : Type} [Hashable α] [DecidableEq α] {len : Nat} {aig : AIG α} (i : Nat) (hi : i ≤ len) (lhs rhs : aig.RefVec len) (s : aig.RefVec i) (f : (aig : AIG α) → aig.BinaryInput → Entrypoint α) [LawfulOperator α BinaryInput f] [LawfulZipOperator α f] (idx : Nat) (h1 : idx < aig.decls.size) (h2 : idx < (go aig i s hi lhs rhs f).aig.decls.size) :
(go aig i s hi lhs rhs f).aig.decls[idx] = aig.decls[idx]
source
theorem Std.Sat.AIG.RefVec.zip_decl_eq {α : Type} [Hashable α] [DecidableEq α] {len : Nat} {aig : AIG α} (input : aig.BinaryRefVec len) (func : (aig : AIG α) → aig.BinaryInput → Entrypoint α) [LawfulOperator α BinaryInput func] [LawfulZipOperator α func] (idx : Nat) (h1 : idx < aig.decls.size) (h2 : idx < (zip aig input func).aig.decls.size) :
(zip aig input func).aig.decls[idx] = aig.decls[idx]
source
theorem Std.Sat.AIG.RefVec.zip_lt_size_of_lt_aig_size {α : Type} [Hashable α] [DecidableEq α] {len x : Nat} (aig : AIG α) (input : aig.BinaryRefVec len) (func : (aig : AIG α) → aig.BinaryInput → Entrypoint α) [LawfulOperator α BinaryInput func] [LawfulZipOperator α func] (h : x < aig.decls.size) :
x < (zip aig input func).aig.decls.size
source
theorem Std.Sat.AIG.RefVec.zip_le_size_of_le_aig_size {α : Type} [Hashable α] [DecidableEq α] {len x : Nat} (aig : AIG α) (input : aig.BinaryRefVec len) (func : (aig : AIG α) → aig.BinaryInput → Entrypoint α) [LawfulOperator α BinaryInput func] [LawfulZipOperator α func] (h : x ≤ aig.decls.size) :
x ≤ (zip aig input func).aig.decls.size
source
theorem Std.Sat.AIG.RefVec.IsPrefix_zip {α : Type} [Hashable α] [DecidableEq α] {len : Nat} {aig : AIG α} (input : aig.BinaryRefVec len) (func : (aig : AIG α) → aig.BinaryInput → Entrypoint α) [LawfulOperator α BinaryInput func] [LawfulZipOperator α func] :
IsPrefix aig.decls (zip aig input func).aig.decls
source
@[irreducible]
theorem Std.Sat.AIG.RefVec.zip.go_get_aux {α : Type} [Hashable α] [DecidableEq α] {len : Nat} {aig : AIG α} (curr : Nat) (hcurr : curr ≤ len) (s : aig.RefVec curr) (lhs rhs : aig.RefVec len) (f : (aig : AIG α) → aig.BinaryInput → Entrypoint α) [LawfulOperator α BinaryInput f] [LawfulZipOperator α f] (idx : Nat) (hidx : idx < curr) (hfoo : aig.decls.size ≤ (go aig curr s hcurr lhs rhs f).aig.decls.size) :
(go aig curr s hcurr lhs rhs f).vec.get idx ⋯ = (s.get idx hidx).cast hfoo
source
theorem Std.Sat.AIG.RefVec.zip.go_get {α : Type} [Hashable α] [DecidableEq α] {len : Nat} {aig : AIG α} (curr : Nat) (hcurr : curr ≤ len) (s : aig.RefVec curr) (lhs rhs : aig.RefVec len) (f : (aig : AIG α) → aig.BinaryInput → Entrypoint α) [LawfulOperator α BinaryInput f] [LawfulZipOperator α f] (idx : Nat) (hidx : idx < curr) :
(go aig curr s hcurr lhs rhs f).vec.get idx ⋯ = (s.get idx hidx).cast ⋯
source
theorem Std.Sat.AIG.RefVec.zip.go_denote_mem_prefix {α : Type} [Hashable α] [DecidableEq α] {len : Nat} {assign : α → Bool} {inv : Bool} {aig : AIG α} (curr : Nat) (hcurr : curr ≤ len) (s : aig.RefVec curr) (lhs rhs : aig.RefVec len) (f : (aig : AIG α) → aig.BinaryInput → Entrypoint α) [LawfulOperator α BinaryInput f] [LawfulZipOperator α f] (start : Nat) (hstart : start < aig.decls.size) :
⟦assign, { aig := (go aig curr s hcurr lhs rhs f).aig, ref := { gate := start, invert := inv, hgate := ⋯ } }⟧ = ⟦assign, { aig := aig, ref := { gate := start, invert := inv, hgate := hstart } }⟧
source
@[irreducible]
theorem Std.Sat.AIG.RefVec.zip.denote_go {α : Type} [Hashable α] [DecidableEq α] {len : Nat} {assign : α → Bool} {aig : AIG α} (curr : Nat) (hcurr : curr ≤ len) (s : aig.RefVec curr) (lhs rhs : aig.RefVec len) (f : (aig : AIG α) → aig.BinaryInput → Entrypoint α) [LawfulOperator α BinaryInput f] [LawfulZipOperator α f] (idx : Nat) (hidx1 : idx < len) :
curr ≤ idx → ⟦assign, { aig := (go aig curr s hcurr lhs rhs f).aig, ref := (go aig curr s hcurr lhs rhs f).vec.get idx hidx1 }⟧ = ⟦assign, f aig { lhs := lhs.get idx hidx1, rhs := rhs.get idx hidx1 }⟧
source
@[simp]
theorem Std.Sat.AIG.RefVec.denote_zip {α : Type} [Hashable α] [DecidableEq α] {len : Nat} {assign : α → Bool} {aig : AIG α} (input : aig.BinaryRefVec len) (func : (aig : AIG α) → aig.BinaryInput → Entrypoint α) [LawfulOperator α BinaryInput func] [LawfulZipOperator α func] (idx : Nat) (hidx : idx < len) :
⟦assign, { aig := (zip aig input func).aig, ref := (zip aig input func).vec.get idx hidx }⟧ = ⟦assign, func aig { lhs := input.lhs.get idx hidx, rhs := input.rhs.get idx hidx }⟧