Documentation

Std.Sat.AIG.Lemmas

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

@[simp]
theorem Std.Sat.AIG.Ref.gate_cast {α : Type} [Hashable α] [DecidableEq α] {aig1 : Std.Sat.AIG α} {aig2 : Std.Sat.AIG α} (ref : aig1.Ref) (h : aig1.decls.size aig2.decls.size) :
(ref.cast h).gate = ref.gate
@[simp]
theorem Std.Sat.AIG.Ref.cast_eq {α : Type} [Hashable α] [DecidableEq α] {aig1 : Std.Sat.AIG α} {aig2 : Std.Sat.AIG α} (ref : aig1.Ref) (h : aig1.decls.size aig2.decls.size) :
ref.cast h = { gate := ref.gate, hgate := }
@[simp]
theorem Std.Sat.AIG.Fanin.ref_cast {α : Type} [Hashable α] [DecidableEq α] {aig1 : Std.Sat.AIG α} {aig2 : Std.Sat.AIG α} (fanin : aig1.Fanin) (h : aig1.decls.size aig2.decls.size) :
(fanin.cast h).ref = fanin.ref.cast h
@[simp]
theorem Std.Sat.AIG.Fanin.inv_cast {α : Type} [Hashable α] [DecidableEq α] {aig1 : Std.Sat.AIG α} {aig2 : Std.Sat.AIG α} (fanin : aig1.Fanin) (h : aig1.decls.size aig2.decls.size) :
(fanin.cast h).inv = fanin.inv
@[simp]
theorem Std.Sat.AIG.GateInput.lhs_cast {α : Type} [Hashable α] [DecidableEq α] {aig1 : Std.Sat.AIG α} {aig2 : Std.Sat.AIG α} (input : aig1.GateInput) (h : aig1.decls.size aig2.decls.size) :
(input.cast h).lhs = input.lhs.cast h
@[simp]
theorem Std.Sat.AIG.GateInput.rhs_cast {α : Type} [Hashable α] [DecidableEq α] {aig1 : Std.Sat.AIG α} {aig2 : Std.Sat.AIG α} (input : aig1.GateInput) (h : aig1.decls.size aig2.decls.size) :
(input.cast h).rhs = input.rhs.cast h
@[simp]
theorem Std.Sat.AIG.BinaryInput.each_cast {α : Type} [Hashable α] [DecidableEq α] {aig1 : Std.Sat.AIG α} {aig2 : Std.Sat.AIG α} (lhs : aig1.Ref) (rhs : aig1.Ref) (h1 : aig1.decls.size aig2.decls.size) (h2 : aig1.decls.size aig2.decls.size) :
{ lhs := lhs.cast h1, rhs := rhs.cast h2 } = { lhs := lhs, rhs := rhs }.cast h2
@[simp]
theorem Std.Sat.AIG.denote_projected_entry {α : Type} [Hashable α] [DecidableEq α] {assign : αBool} {entry : Std.Sat.AIG.Entrypoint α} :
assign, { aig := entry.aig, ref := entry.ref } = assign, entry
@[simp]
theorem Std.Sat.AIG.denote_projected_entry' {α : Type} [Hashable α] [DecidableEq α] {assign : αBool} {entry : Std.Sat.AIG.Entrypoint α} :
assign, { aig := entry.aig, ref := { gate := entry.ref.gate, hgate := } } = assign, entry
theorem Std.Sat.AIG.mkGate_le_size {α : Type} [Hashable α] [DecidableEq α] (aig : Std.Sat.AIG α) (input : aig.GateInput) :
aig.decls.size (aig.mkGate input).aig.decls.size

AIG.mkGate never shrinks the underlying AIG.

theorem Std.Sat.AIG.mkGate_decl_eq {α : Type} [Hashable α] [DecidableEq α] (idx : Nat) (aig : Std.Sat.AIG α) (input : aig.GateInput) {h : idx < aig.decls.size} :
let_fun 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.

instance Std.Sat.AIG.instLawfulOperatorGateInputMkGate {α : Type} [Hashable α] [DecidableEq α] :
Std.Sat.AIG.LawfulOperator α Std.Sat.AIG.GateInput Std.Sat.AIG.mkGate
Equations
  • =
@[simp]
theorem Std.Sat.AIG.denote_mkGate {α : Type} [Hashable α] [DecidableEq α] {assign : αBool} {aig : Std.Sat.AIG α} {input : aig.GateInput} :
assign, aig.mkGate input = ((assign, { aig := aig, ref := input.lhs.ref } ^^ input.lhs.inv) && (assign, { aig := aig, ref := input.rhs.ref } ^^ input.rhs.inv))
theorem Std.Sat.AIG.mkAtom_le_size {α : Type} [Hashable α] [DecidableEq α] (aig : Std.Sat.AIG α) (var : α) :
aig.decls.size (aig.mkAtom var).aig.decls.size

AIG.mkAtom never shrinks the underlying AIG.

theorem Std.Sat.AIG.mkAtom_decl_eq {α : Type} [Hashable α] [DecidableEq α] (aig : Std.Sat.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.

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

AIG.mkConst never shrinks the underlying AIG.

theorem Std.Sat.AIG.mkConst_decl_eq {α : Type} [Hashable α] [DecidableEq α] (aig : Std.Sat.AIG α) (val : Bool) (idx : Nat) {h : idx < aig.decls.size} :
let_fun 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.

instance Std.Sat.AIG.instLawfulOperatorBoolMkConst {α : Type} [Hashable α] [DecidableEq α] :
Std.Sat.AIG.LawfulOperator α (fun (x : Std.Sat.AIG α) => Bool) Std.Sat.AIG.mkConst
Equations
  • =
@[simp]
theorem Std.Sat.AIG.denote_mkConst {α : Type} [Hashable α] [DecidableEq α] {assign : αBool} {val : Bool} {aig : Std.Sat.AIG α} :
assign, aig.mkConst val = val
theorem Std.Sat.AIG.denote_idx_const {α : Type} [Hashable α] [DecidableEq α] {start : Nat} {assign : αBool} {b : Bool} {aig : Std.Sat.AIG α} {hstart : start < aig.decls.size} (h : aig.decls[start] = Std.Sat.AIG.Decl.const b) :
assign, { aig := aig, ref := { gate := start, hgate := hstart } } = b

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

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

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

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

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

theorem Std.Sat.AIG.idx_trichotomy {α : Type} [Hashable α] [DecidableEq α] {start : Nat} (aig : Std.Sat.AIG α) (hstart : start < aig.decls.size) {prop : Prop} (hconst : ∀ (b : Bool), aig.decls[start] = Std.Sat.AIG.Decl.const bprop) (hatom : ∀ (a : α), aig.decls[start] = Std.Sat.AIG.Decl.atom aprop) (hgate : ∀ (lhs rhs : Nat) (linv rinv : Bool), aig.decls[start] = Std.Sat.AIG.Decl.gate lhs rhs linv rinvprop) :
prop
theorem Std.Sat.AIG.denote_idx_trichotomy {α : Type} [Hashable α] [DecidableEq α] {start : Nat} {assign : αBool} {res : Bool} {aig : Std.Sat.AIG α} {hstart : start < aig.decls.size} (hconst : ∀ (b : Bool), aig.decls[start] = Std.Sat.AIG.Decl.const bassign, { aig := aig, ref := { gate := start, hgate := hstart } } = res) (hatom : ∀ (a : α), aig.decls[start] = Std.Sat.AIG.Decl.atom aassign, { aig := aig, ref := { gate := start, hgate := hstart } } = res) (hgate : ∀ (lhs rhs : Nat) (linv rinv : Bool), aig.decls[start] = Std.Sat.AIG.Decl.gate lhs rhs linv rinvassign, { aig := aig, ref := { gate := start, hgate := hstart } } = res) :
assign, { aig := aig, ref := { gate := start, hgate := hstart } } = res
theorem Std.Sat.AIG.mem_def {α : Type} [Hashable α] [DecidableEq α] {aig : Std.Sat.AIG α} {a : α} :
a aig Std.Sat.AIG.Decl.atom a aig.decls
@[irreducible]
theorem Std.Sat.AIG.denote_congr {α : Type} [Hashable α] [DecidableEq α] (assign1 : αBool) (assign2 : αBool) (aig : Std.Sat.AIG α) (idx : Nat) (hidx : idx < aig.decls.size) (h : ∀ (a : α), a aigassign1 a = assign2 a) :
assign1, { aig := aig, ref := { gate := idx, hgate := hidx } } = assign2, { aig := aig, ref := { gate := idx, hgate := hidx } }