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
- Std.Sat.AIG.instLawfulOperatorGateInputMkGate = { le_size := ⋯, decl_eq := ⋯ }
@[simp]
theorem
Std.Sat.AIG.denote_mkGate
{α : Type}
[Hashable α]
[DecidableEq α]
{assign : α → Bool}
{aig : Std.Sat.AIG α}
{input : aig.GateInput}
:
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
- Std.Sat.AIG.instLawfulOperatorMkAtom = { le_size := ⋯, decl_eq := ⋯ }
@[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
- Std.Sat.AIG.instLawfulOperatorBoolMkConst = { le_size := ⋯, decl_eq := ⋯ }
@[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)
:
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 b → prop)
(hatom : ∀ (a : α), aig.decls[start] = Std.Sat.AIG.Decl.atom a → prop)
(hgate : ∀ (lhs rhs : Nat) (linv rinv : Bool), aig.decls[start] = Std.Sat.AIG.Decl.gate lhs rhs linv rinv → prop)
:
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 b →
⟦assign, { aig := aig, ref := { gate := start, hgate := hstart } }⟧ = res)
(hatom : ∀ (a : α),
aig.decls[start] = Std.Sat.AIG.Decl.atom a → ⟦assign, { 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 rinv →
⟦assign, { 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 ∈ aig → assign1 a = assign2 a)
:
⟦assign1, { aig := aig, ref := { gate := idx, hgate := hidx } }⟧ = ⟦assign2, { aig := aig, ref := { gate := idx, hgate := hidx } }⟧