This module provides a basic theory around the naive AIG node creation functions. It is mostly fundamental work for the cached versions later on.

source
@[simp]
theorem Std.Sat.AIG.Ref.gate_cast {α : Type} [Hashable α] [DecidableEq α] {aig1 aig2 : AIG α} (ref : aig1.Ref) (h : aig1.decls.size ≤ aig2.decls.size) :
(ref.cast h).gate = ref.gate
source
@[simp]
theorem Std.Sat.AIG.Ref.cast_eq {α : Type} [Hashable α] [DecidableEq α] {aig1 aig2 : AIG α} (ref : aig1.Ref) (h : aig1.decls.size ≤ aig2.decls.size) :
ref.cast h = { gate := ref.gate, invert := ref.invert, hgate := ⋯ }
source
@[simp]
theorem Std.Sat.AIG.BinaryInput.lhs_cast {α : Type} [Hashable α] [DecidableEq α] {aig1 aig2 : AIG α} (input : aig1.BinaryInput) (h : aig1.decls.size ≤ aig2.decls.size) :
(input.cast h).lhs = input.lhs.cast h
source
@[simp]
theorem Std.Sat.AIG.BinaryInput.rhs_cast {α : Type} [Hashable α] [DecidableEq α] {aig1 aig2 : AIG α} (input : aig1.BinaryInput) (h : aig1.decls.size ≤ aig2.decls.size) :
(input.cast h).rhs = input.rhs.cast h
source
@[simp]
theorem Std.Sat.AIG.BinaryInput.each_cast {α : Type} [Hashable α] [DecidableEq α] {aig1 aig2 : AIG α} (lhs rhs : aig1.Ref) (h1 h2 : aig1.decls.size ≤ aig2.decls.size) :
{ lhs := lhs.cast h1, rhs := rhs.cast h2 } = { lhs := lhs, rhs := rhs }.cast h2
source
@[simp]
theorem Std.Sat.AIG.BinaryInput_invert_lhs {α : Type} [Hashable α] [DecidableEq α] {aig : AIG α} (input : aig.BinaryInput) (linv rinv : Bool) :
(input.invert linv rinv).lhs = { gate := input.lhs.gate, invert := linv ^^ input.lhs.invert, hgate := ⋯ }
source
@[simp]
theorem Std.Sat.AIG.BinaryInput_invert_rhs {α : Type} [Hashable α] [DecidableEq α] {aig : AIG α} (input : aig.BinaryInput) (linv rinv : Bool) :
(input.invert linv rinv).rhs = { gate := input.rhs.gate, invert := rinv ^^ input.rhs.invert, hgate := ⋯ }
source
@[simp]
theorem Std.Sat.AIG.denote_projected_entry {α : Type} [Hashable α] [DecidableEq α] {assign : α → Bool} {entry : Entrypoint α} :
⟦assign, { aig := entry.aig, ref := entry.ref }⟧ = ⟦assign, entry⟧
source
@[simp]
theorem Std.Sat.AIG.denote_projected_entry' {α : Type} [Hashable α] [DecidableEq α] {assign : α → Bool} {entry : Entrypoint α} :
⟦assign, { aig := entry.aig, ref := { gate := entry.ref.gate, invert := entry.ref.invert, hgate := ⋯ } }⟧ = ⟦assign, entry⟧
source
@[simp]
theorem Std.Sat.AIG.Ref.denote_flip {α : Type} [Hashable α] [DecidableEq α] {assign : α → Bool} {aig : AIG α} {ref : aig.Ref} {inv : Bool} :
⟦assign, { aig := aig, ref := ref.flip inv }⟧ = (⟦assign, { aig := aig, ref := ref }⟧ ^^ inv)
source
@[simp]
theorem Std.Sat.AIG.Ref.denote_not {α : Type} [Hashable α] [DecidableEq α] {assign : α → Bool} {aig : AIG α} {ref : aig.Ref} :
⟦assign, { aig := aig, ref := ref.not }⟧ = !⟦assign, { aig := aig, ref := ref }⟧
source
@[simp]
theorem Std.Sat.AIG.denote_not_invert {α : Type} [Hashable α] [DecidableEq α] {assign : α → Bool} {aig : AIG α} {gate : Nat} {inv : Bool} {hgate : gate < aig.decls.size} :
⟦assign, { aig := aig, ref := { gate := gate, invert := !inv, hgate := hgate } }⟧ = !⟦assign, { aig := aig, ref := { gate := gate, invert := inv, hgate := hgate } }⟧
source
@[simp]
theorem Std.Sat.AIG.denote_invert_true {α : Type} [Hashable α] [DecidableEq α] {assign : α → Bool} {aig : AIG α} {gate : Nat} {hgate : gate < aig.decls.size} :
⟦assign, { aig := aig, ref := { gate := gate, invert := true, hgate := hgate } }⟧ = !⟦assign, { aig := aig, ref := { gate := gate, invert := false, hgate := hgate } }⟧
source
theorem Std.Sat.AIG.mkGate_le_size {α : Type} [Hashable α] [DecidableEq α] (aig : AIG α) (input : aig.BinaryInput) :
aig.decls.size ≤ (aig.mkGate input).aig.decls.size

`AIG.mkGate` never shrinks the underlying AIG.

source
theorem Std.Sat.AIG.mkGate_decl_eq {α : Type} [Hashable α] [DecidableEq α] (idx : Nat) (aig : AIG α) (input : aig.BinaryInput) {h : idx < aig.decls.size} :
have this := ⋯; (aig.mkGate input).aig.decls[idx] = aig.decls[idx]

The AIG produced by `AIG.mkGate` agrees with the input AIG on all indices that are valid for both.

source
instance Std.Sat.AIG.instLawfulOperatorBinaryInputMkGate {α : Type} [Hashable α] [DecidableEq α] :
LawfulOperator α BinaryInput mkGate
source
@[simp]
theorem Std.Sat.AIG.denote_mkGate {α : Type} [Hashable α] [DecidableEq α] {assign : α → Bool} {aig : AIG α} {input : aig.BinaryInput} :
⟦assign, aig.mkGate input⟧ = (⟦assign, { aig := aig, ref := input.lhs }⟧ && ⟦assign, { aig := aig, ref := input.rhs }⟧)
source
theorem Std.Sat.AIG.mkAtom_le_size {α : Type} [Hashable α] [DecidableEq α] (aig : AIG α) (var : α) :
aig.decls.size ≤ (aig.mkAtom var).aig.decls.size

`AIG.mkAtom` never shrinks the underlying AIG.

source
theorem Std.Sat.AIG.mkAtom_decl_eq {α : Type} [Hashable α] [DecidableEq α] (aig : AIG α) (var : α) (idx : Nat) {h : idx < aig.decls.size} {hbound : idx < (aig.mkAtom var).aig.decls.size} :
(aig.mkAtom var).aig.decls[idx] = aig.decls[idx]

The AIG produced by `AIG.mkAtom` agrees with the input AIG on all indices that are valid for both.

source
instance Std.Sat.AIG.instLawfulOperatorMkAtom {α : Type} [Hashable α] [DecidableEq α] :
LawfulOperator α (fun (x : AIG α) => α) mkAtom
source
@[simp]
theorem Std.Sat.AIG.denote_mkAtom {α : Type} [Hashable α] [DecidableEq α] {assign : α → Bool} {var : α} {aig : AIG α} :
⟦assign, aig.mkAtom var⟧ = assign var
source
theorem Std.Sat.AIG.mkConst_le_size {α : Type} [Hashable α] [DecidableEq α] (aig : AIG α) (val : Bool) :
aig.decls.size ≤ (aig.mkConst val).aig.decls.size

`AIG.mkConst` never shrinks the underlying AIG.

source
theorem Std.Sat.AIG.mkConst_decl_eq {α : Type} [Hashable α] [DecidableEq α] (aig : AIG α) (val : Bool) (idx : Nat) {h : idx < aig.decls.size} :
have this := ⋯; (aig.mkConst val).aig.decls[idx] = aig.decls[idx]

The AIG produced by `AIG.mkConst` agrees with the input AIG on all indices that are valid for both.

source
instance Std.Sat.AIG.instLawfulOperatorBoolMkConst {α : Type} [Hashable α] [DecidableEq α] :
LawfulOperator α (fun (x : AIG α) => Bool) mkConst
source
@[simp]
theorem Std.Sat.AIG.denote_mkConst {α : Type} [Hashable α] [DecidableEq α] {assign : α → Bool} {val : Bool} {aig : AIG α} :
⟦assign, aig.mkConst val⟧ = val
source
theorem Std.Sat.AIG.denote_idx_false {α : Type} [Hashable α] [DecidableEq α] {start : Nat} {assign : α → Bool} {invert : Bool} {aig : AIG α} {hstart : start < aig.decls.size} (h : aig.decls[start] = Decl.false) :
⟦assign, { aig := aig, ref := { gate := start, invert := invert, hgate := hstart } }⟧ = invert

If an index contains a `Decl.false` we know how to denote it.

source
theorem Std.Sat.AIG.denote_idx_atom {α : Type} [Hashable α] [DecidableEq α] {start : Nat} {assign : α → Bool} {invert : Bool} {a : α} {aig : AIG α} {hstart : start < aig.decls.size} (h : aig.decls[start] = Decl.atom a) :
⟦assign, { aig := aig, ref := { gate := start, invert := invert, hgate := hstart } }⟧ = (assign a ^^ invert)

If an index contains a `Decl.atom` we know how to denote it.

source
theorem Std.Sat.AIG.denote_idx_gate {α : Type} [Hashable α] [DecidableEq α] {start : Nat} {assign : α → Bool} {invert : Bool} {lhs rhs : Fanin} {aig : AIG α} {hstart : start < aig.decls.size} (h : aig.decls[start] = Decl.gate lhs rhs) :
⟦assign, { aig := aig, ref := { gate := start, invert := invert, hgate := hstart } }⟧ = (⟦assign, { aig := aig, ref := { gate := lhs.gate, invert := lhs.invert, hgate := ⋯ } }⟧ && ⟦assign, { aig := aig, ref := { gate := rhs.gate, invert := rhs.invert, hgate := ⋯ } }⟧ ^^ invert)

If an index contains a `Decl.gate` we know how to denote it.

source
theorem Std.Sat.AIG.idx_trichotomy {α : Type} [Hashable α] [DecidableEq α] {start : Nat} (aig : AIG α) (hstart : start < aig.decls.size) {prop : Prop} (hfalse : aig.decls[start] = Decl.false → prop) (hatom : ∀ (a : α), aig.decls[start] = Decl.atom a → prop) (hgate : ∀ (lhs rhs : Fanin), aig.decls[start] = Decl.gate lhs rhs → prop) :
prop
source
theorem Std.Sat.AIG.denote_idx_trichotomy {α : Type} [Hashable α] [DecidableEq α] {start : Nat} {assign : α → Bool} {invert res : Bool} {aig : AIG α} {hstart : start < aig.decls.size} (hfalse : aig.decls[start] = Decl.false → ⟦assign, { aig := aig, ref := { gate := start, invert := invert, hgate := hstart } }⟧ = res) (hatom : ∀ (a : α), aig.decls[start] = Decl.atom a → ⟦assign, { aig := aig, ref := { gate := start, invert := invert, hgate := hstart } }⟧ = res) (hgate : ∀ (lhs rhs : Fanin), aig.decls[start] = Decl.gate lhs rhs → ⟦assign, { aig := aig, ref := { gate := start, invert := invert, hgate := hstart } }⟧ = res) :
⟦assign, { aig := aig, ref := { gate := start, invert := invert, hgate := hstart } }⟧ = res
source
theorem Std.Sat.AIG.mem_def {α : Type} [Hashable α] [DecidableEq α] {aig : AIG α} {a : α} :
a ∈ aig ↔ Decl.atom a ∈ aig.decls
source
@[irreducible]
theorem Std.Sat.AIG.denote_congr {α : Type} [Hashable α] [DecidableEq α] (assign1 assign2 : α → Bool) (aig : AIG α) (idx : Nat) (invert : Bool) (hidx : idx < aig.decls.size) (h : ∀ (a : α), a ∈ aig → assign1 a = assign2 a) :
⟦assign1, { aig := aig, ref := { gate := idx, invert := invert, hgate := hidx } }⟧ = ⟦assign2, { aig := aig, ref := { gate := idx, invert := invert, hgate := hidx } }⟧
source
theorem Std.Sat.AIG.of_isConstant {α : Type} [Hashable α] [DecidableEq α] {aig : AIG α} {assign : α → Bool} {ref : aig.Ref} {b : Bool} :
aig.isConstant ref b = true → ⟦assign, { aig := aig, ref := ref }⟧ = b
source
theorem Std.Sat.AIG.denote_getConstant {α : Type} [Hashable α] [DecidableEq α] {aig : AIG α} {assign : α → Bool} {ref : aig.Ref} {b : Bool} :
aig.getConstant ref = some b → ⟦assign, { aig := aig, ref := ref }⟧ = b