Std.Sat.AIG.RefVecOperator.Zip

source

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

Prop

chainable : ∀ (aig : Std.Sat.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.chainable {α : Type} :

∀ {inst : Hashable α} {inst_1 : DecidableEq α} {f : (aig : Std.Sat.AIG α) → aig.BinaryInput → Std.Sat.AIG.Entrypoint α} {inst_2 : Std.Sat.AIG.LawfulOperator α Std.Sat.AIG.BinaryInput f} [self : Std.Sat.AIG.RefVec.LawfulZipOperator α f] (aig : Std.Sat.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⟧

source

theorem Std.Sat.AIG.RefVec.LawfulZipOperator.denote_prefix_cast_ref {α : Type} [Hashable α] [DecidableEq α] {assign : α → Bool} {aig : Std.Sat.AIG α} {input1 : aig.BinaryInput} {input2 : aig.BinaryInput} {f : (aig : Std.Sat.AIG α) → aig.BinaryInput → Std.Sat.AIG.Entrypoint α} [Std.Sat.AIG.LawfulOperator α Std.Sat.AIG.BinaryInput f] [Std.Sat.AIG.RefVec.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 α] :

Std.Sat.AIG.RefVec.LawfulZipOperator α Std.Sat.AIG.mkAndCached

Equations

⋯ = ⋯

source

instance Std.Sat.AIG.RefVec.LawfulZipOperator.instMkOrCached {α : Type} [Hashable α] [DecidableEq α] :

Std.Sat.AIG.RefVec.LawfulZipOperator α Std.Sat.AIG.mkOrCached

Equations

⋯ = ⋯

source

instance Std.Sat.AIG.RefVec.LawfulZipOperator.instMkXorCached {α : Type} [Hashable α] [DecidableEq α] :

Std.Sat.AIG.RefVec.LawfulZipOperator α Std.Sat.AIG.mkXorCached

Equations

⋯ = ⋯

source

instance Std.Sat.AIG.RefVec.LawfulZipOperator.instMkBEqCached {α : Type} [Hashable α] [DecidableEq α] :

Std.Sat.AIG.RefVec.LawfulZipOperator α Std.Sat.AIG.mkBEqCached

Equations

⋯ = ⋯

source

instance Std.Sat.AIG.RefVec.LawfulZipOperator.instMkImpCached {α : Type} [Hashable α] [DecidableEq α] :

Std.Sat.AIG.RefVec.LawfulZipOperator α Std.Sat.AIG.mkImpCached

Equations

⋯ = ⋯

source

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

Type

input : aig.BinaryRefVec len
func : (aig : Std.Sat.AIG α) → aig.BinaryInput → Std.Sat.AIG.Entrypoint α
lawful : Std.Sat.AIG.LawfulOperator α Std.Sat.AIG.BinaryInput self.func
chainable : Std.Sat.AIG.RefVec.LawfulZipOperator α self.func

Instances For

source

theorem Std.Sat.AIG.RefVec.ZipTarget.lawful {α : Type} [Hashable α] [DecidableEq α] {aig : Std.Sat.AIG α} {len : Nat} (self : Std.Sat.AIG.RefVec.ZipTarget aig len) :

Std.Sat.AIG.LawfulOperator α Std.Sat.AIG.BinaryInput self.func

source

theorem Std.Sat.AIG.RefVec.ZipTarget.chainable {α : Type} [Hashable α] [DecidableEq α] {aig : Std.Sat.AIG α} {len : Nat} (self : Std.Sat.AIG.RefVec.ZipTarget aig len) :

Std.Sat.AIG.RefVec.LawfulZipOperator α self.func

source

@[specialize #[]]

def Std.Sat.AIG.RefVec.zip {α : Type} [Hashable α] [DecidableEq α] {len : Nat} (aig : Std.Sat.AIG α) (target : Std.Sat.AIG.RefVec.ZipTarget aig len) :

Std.Sat.AIG.RefVecEntry α len

Equations

Std.Sat.AIG.RefVec.zip aig target = Std.Sat.AIG.RefVec.zip.go aig 0 Std.Sat.AIG.RefVec.empty ⋯ target.input.lhs target.input.rhs target.func

Instances For

source

@[irreducible, specialize #[]]

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

Std.Sat.AIG.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 : Std.Sat.AIG α} (idx : Nat) (hidx : idx ≤ len) (s : aig.RefVec idx) (lhs : aig.RefVec len) (rhs : aig.RefVec len) (f : (aig : Std.Sat.AIG α) → aig.BinaryInput → Std.Sat.AIG.Entrypoint α) [Std.Sat.AIG.LawfulOperator α Std.Sat.AIG.BinaryInput f] [chainable : Std.Sat.AIG.RefVec.LawfulZipOperator α f] :

aig.decls.size ≤ (Std.Sat.AIG.RefVec.zip.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 : Std.Sat.AIG α} (target : Std.Sat.AIG.RefVec.ZipTarget aig len) :

aig.decls.size ≤ (Std.Sat.AIG.RefVec.zip aig target).aig.decls.size

source

@[irreducible]

theorem Std.Sat.AIG.RefVec.zip.go_decl_eq {α : Type} [Hashable α] [DecidableEq α] {len : Nat} {aig : Std.Sat.AIG α} (i : Nat) (hi : i ≤ len) (lhs : aig.RefVec len) (rhs : aig.RefVec len) (s : aig.RefVec i) (f : (aig : Std.Sat.AIG α) → aig.BinaryInput → Std.Sat.AIG.Entrypoint α) [Std.Sat.AIG.LawfulOperator α Std.Sat.AIG.BinaryInput f] [chainable : Std.Sat.AIG.RefVec.LawfulZipOperator α f] (idx : Nat) (h1 : idx < aig.decls.size) (h2 : idx < (Std.Sat.AIG.RefVec.zip.go aig i s hi lhs rhs f).aig.decls.size) :

(Std.Sat.AIG.RefVec.zip.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 : Std.Sat.AIG α} (target : Std.Sat.AIG.RefVec.ZipTarget aig len) (idx : Nat) (h1 : idx < aig.decls.size) (h2 : idx < (Std.Sat.AIG.RefVec.zip aig target).aig.decls.size) :

(Std.Sat.AIG.RefVec.zip aig target).aig.decls[idx] = aig.decls[idx]

source

instance Std.Sat.AIG.RefVec.instLawfulVecOperatorZipTargetZip {α : Type} [Hashable α] [DecidableEq α] :

Std.Sat.AIG.LawfulVecOperator α Std.Sat.AIG.RefVec.ZipTarget fun {len : Nat} => Std.Sat.AIG.RefVec.zip

Equations

⋯ = ⋯

source

@[irreducible]

theorem Std.Sat.AIG.RefVec.zip.go_get_aux {α : Type} [Hashable α] [DecidableEq α] {len : Nat} {aig : Std.Sat.AIG α} (curr : Nat) (hcurr : curr ≤ len) (s : aig.RefVec curr) (lhs : aig.RefVec len) (rhs : aig.RefVec len) (f : (aig : Std.Sat.AIG α) → aig.BinaryInput → Std.Sat.AIG.Entrypoint α) [Std.Sat.AIG.LawfulOperator α Std.Sat.AIG.BinaryInput f] [chainable : Std.Sat.AIG.RefVec.LawfulZipOperator α f] (idx : Nat) (hidx : idx < curr) (hfoo : aig.decls.size ≤ (Std.Sat.AIG.RefVec.zip.go aig curr s hcurr lhs rhs f).aig.decls.size) :

(Std.Sat.AIG.RefVec.zip.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 : Std.Sat.AIG α} (curr : Nat) (hcurr : curr ≤ len) (s : aig.RefVec curr) (lhs : aig.RefVec len) (rhs : aig.RefVec len) (f : (aig : Std.Sat.AIG α) → aig.BinaryInput → Std.Sat.AIG.Entrypoint α) [Std.Sat.AIG.LawfulOperator α Std.Sat.AIG.BinaryInput f] [chainable : Std.Sat.AIG.RefVec.LawfulZipOperator α f] (idx : Nat) (hidx : idx < curr) :

(Std.Sat.AIG.RefVec.zip.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} {aig : Std.Sat.AIG α} (curr : Nat) (hcurr : curr ≤ len) (s : aig.RefVec curr) (lhs : aig.RefVec len) (rhs : aig.RefVec len) (f : (aig : Std.Sat.AIG α) → aig.BinaryInput → Std.Sat.AIG.Entrypoint α) [Std.Sat.AIG.LawfulOperator α Std.Sat.AIG.BinaryInput f] [chainable : Std.Sat.AIG.RefVec.LawfulZipOperator α f] (start : Nat) (hstart : start < aig.decls.size) :

⟦assign, { aig := (Std.Sat.AIG.RefVec.zip.go aig curr s hcurr lhs rhs f).aig, ref := { gate := start, hgate := ⋯ } }⟧ = ⟦assign, { aig := aig, ref := { gate := start, hgate := hstart } }⟧

source

@[irreducible]

theorem Std.Sat.AIG.RefVec.zip.denote_go {α : Type} [Hashable α] [DecidableEq α] {len : Nat} {assign : α → Bool} {aig : Std.Sat.AIG α} (curr : Nat) (hcurr : curr ≤ len) (s : aig.RefVec curr) (lhs : aig.RefVec len) (rhs : aig.RefVec len) (f : (aig : Std.Sat.AIG α) → aig.BinaryInput → Std.Sat.AIG.Entrypoint α) [Std.Sat.AIG.LawfulOperator α Std.Sat.AIG.BinaryInput f] [chainable : Std.Sat.AIG.RefVec.LawfulZipOperator α f] (idx : Nat) (hidx1 : idx < len) :

curr ≤ idx → ⟦assign, { aig := (Std.Sat.AIG.RefVec.zip.go aig curr s hcurr lhs rhs f).aig, ref := (Std.Sat.AIG.RefVec.zip.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 : Std.Sat.AIG α} (target : Std.Sat.AIG.RefVec.ZipTarget aig len) (idx : Nat) (hidx : idx < len) :

⟦assign, { aig := (Std.Sat.AIG.RefVec.zip aig target).aig, ref := (Std.Sat.AIG.RefVec.zip aig target).vec.get idx hidx }⟧ = ⟦assign, target.func aig { lhs := target.input.lhs.get idx hidx, rhs := target.input.rhs.get idx hidx }⟧