This module contains an implementation of a verified Tseitin transformation on AIGs. The key results are the `toCNF` function and the `toCNF_equisat` correctness statement. The implementation is done in the style of section 3.4 of the AIGNET paper.

source
def Std.Sat.AIG.Decl.falseToCNF {α : Type u_1} (output : α) :
CNF α

Produce a Tseitin style CNF for a `Decl.false`, using `output` as the tree node variable.

Equations

- Std.Sat.AIG.Decl.falseToCNF output = [[(output, false)]]

Instances For

source
def Std.Sat.AIG.Decl.atomToCNF {α : Type u_1} (output atom : α) :
CNF α

Produce a Tseitin style CNF for a `Decl.atom`, using `output` as the tree node variable.

Equations

- Std.Sat.AIG.Decl.atomToCNF output atom = [[(output, true), (atom, false)], [(output, false), (atom, true)]]

Instances For

source
def Std.Sat.AIG.Decl.gateToCNF {α : Type u_1} (output lhs rhs : α) (linv rinv : Bool) :
CNF α

Produce a Tseitin style CNF for a `Decl.gate`, using `output` as the tree node variable.

Equations

- Std.Sat.AIG.Decl.gateToCNF output lhs rhs linv rinv = [[(output, false), (lhs, !linv)], [(output, false), (rhs, !rinv)], [(output, true), (lhs, linv), (rhs, rinv)]]

Instances For

source
@[simp]
theorem Std.Sat.AIG.Decl.falseToCNF_eval {α✝ : Type u_1} {output : α✝} {assign : α✝ → Bool} :
CNF.eval assign (falseToCNF output) = (assign output == Bool.false)
source
@[simp]
theorem Std.Sat.AIG.Decl.atomToCNF_eval {α✝ : Type u_1} {output a : α✝} {assign : α✝ → Bool} :
CNF.eval assign (atomToCNF output a) = (assign output == assign a)
source
@[simp]
theorem Std.Sat.AIG.Decl.gateToCNF_eval {α✝ : Type u_1} {output lhs rhs : α✝} {linv rinv : Bool} {assign : α✝ → Bool} :
CNF.eval assign (gateToCNF output lhs rhs linv rinv) = (assign output == ((assign lhs ^^ linv) && (assign rhs ^^ rinv)))
source
@[reducible, inline]
abbrev Std.Sat.AIG.CNFVar (aig : AIG Nat) :
Type
Equations

- aig.CNFVar = (Nat ⊕ Fin aig.decls.size)

Instances For

source
def Std.Sat.AIG.toCNF.mixAssigns {aig : AIG Nat} (assign1 : Nat → Bool) (assign2 : Fin aig.decls.size → Bool) :
aig.CNFVar → Bool

Mix:

1. An assignment for AIG atoms
2. An assignment for auxiliary Tseitin variables into an assignment that can be used by a CNF produced by our Tseitin transformation.

Equations

- Std.Sat.AIG.toCNF.mixAssigns assign1 assign2 (Sum.inl var) = assign1 var
- Std.Sat.AIG.toCNF.mixAssigns assign1 assign2 (Sum.inr var) = assign2 var

Instances For

source
def Std.Sat.AIG.toCNF.projectLeftAssign {aig : AIG Nat} (assign : aig.CNFVar → Bool) :
Nat → Bool

Project the atom assignment out of a CNF assignment

Equations

- Std.Sat.AIG.toCNF.projectLeftAssign assign x✝ = assign (Sum.inl x✝)

Instances For

source
def Std.Sat.AIG.toCNF.projectRightAssign {aig : AIG Nat} (assign : aig.CNFVar → Bool) (idx : Nat) :
idx < aig.decls.size → Bool

Project the auxiliary variable assignment out of a CNF assignment

Equations

- Std.Sat.AIG.toCNF.projectRightAssign assign idx h = assign (Sum.inr ⟨idx, h⟩)

Instances For

source
@[simp]
theorem Std.Sat.AIG.toCNF.projectLeftAssign_property {aig✝ : AIG Nat} {assign : aig✝.CNFVar → Bool} {x : Nat} :
projectLeftAssign assign x = assign (Sum.inl x)
source
@[simp]
theorem Std.Sat.AIG.toCNF.projectRightAssign_property {aig✝ : AIG Nat} {assign : aig✝.CNFVar → Bool} {x : Nat} {hx : x < aig✝.decls.size} :
projectRightAssign assign x hx = assign (Sum.inr ⟨x, hx⟩)
source
def Std.Sat.AIG.toCNF.cnfSatAssignment (aig : AIG Nat) (assign1 : Nat → Bool) :
aig.CNFVar → Bool

Given an atom assignment, produce an assignment that will always satisfy the CNF generated by our Tseitin transformation. This is done by combining the atom assignment with an assignment for the auxiliary variables, that just evaluates the AIG at the corresponding node.

Equations

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

Instances For

source
@[simp]
theorem Std.Sat.AIG.toCNF.satAssignment_inl {aig : AIG Nat} {assign1 : Nat → Bool} {x : Nat} :
cnfSatAssignment aig assign1 (Sum.inl x) = assign1 x
source
@[simp]
theorem Std.Sat.AIG.toCNF.satAssignment_inr {aig : AIG Nat} {assign1 : Nat → Bool} {x : Fin aig.decls.size} :
cnfSatAssignment aig assign1 (Sum.inr x) = ⟦assign1, { aig := aig, ref := { gate := ↑x, invert := false, hgate := ⋯ } }⟧
source
def Std.Sat.AIG.toCNF.Cache.Inv {aig : AIG Nat} (cnf : CNF aig.CNFVar) (marks : Array Bool) (hmarks : marks.size = aig.decls.size) :
Prop

The central invariant for the `Cache`.

Relate satisfiability results about our produced CNF to satisfiability results about the AIG that we are processing. The intuition for this is: if a node is marked, its CNF is already part of the current CNF. Thus the current CNF is already mirroring the semantics of the marked node. This means that if the CNF is satisfiable at some assignment, we can evaluate the marked node under the atom part of that assignment and will get the value that was assigned to the corresponding auxiliary variable as a result.

Equations

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

Instances For

source
theorem Std.Sat.AIG.toCNF.Cache.Inv_init {aig : AIG Nat} :
Inv [] (Array.replicate aig.decls.size false) ⋯

The `Cache` invariant always holds for an empty CNF when all nodes are unmarked.

source
structure Std.Sat.AIG.toCNF.Cache (aig : AIG Nat) (cnf : CNF aig.CNFVar) :
Type

The CNF cache. It keeps track of AIG nodes that we already turned into CNF to avoid adding the same CNF twice.

- marks : Array Bool

  Keeps track of AIG nodes that we already turned into CNF.

- hmarks : self.marks.size = aig.decls.size

  There are always as many marks as AIG nodes.

- inv : Inv cnf self.marks ⋯

  The invariant to make sure that `marks` is well formed with respect to the `cnf`

Instances For

source
structure Std.Sat.AIG.toCNF.Cache.IsExtensionBy {aig : AIG Nat} {cnf1 cnf2 : CNF aig.CNFVar} (cache1 : Cache aig cnf1) (cache2 : Cache aig cnf2) (new : Nat) (hnew : new < aig.decls.size) :
Prop

We say that a cache extends another by an index when it doesn't invalidate any entry and has an entry for that index.

- extension (idx : Nat) (hidx : idx < aig.decls.size) : cache1.marks[idx] = true → cache2.marks[idx] = true

  No entry is invalidated.

- trueAt : cache2.marks[new] = true

  The second cache is true at the new index.

Instances For

source
theorem Std.Sat.AIG.toCNF.Cache.IsExtensionBy_trans_left {aig : AIG Nat} {cnf1 cnf2 cnf3 : CNF aig.CNFVar} {new1 : Nat} {hnew1 : new1 < aig.decls.size} {new2 : Nat} {hnew2 : new2 < aig.decls.size} (cache1 : Cache aig cnf1) (cache2 : Cache aig cnf2) (cache3 : Cache aig cnf3) (h12 : cache1.IsExtensionBy cache2 new1 hnew1) (h23 : cache2.IsExtensionBy cache3 new2 hnew2) :
cache1.IsExtensionBy cache3 new1 hnew1
source
theorem Std.Sat.AIG.toCNF.Cache.IsExtensionBy_trans_right {aig : AIG Nat} {cnf1 cnf2 cnf3 : CNF aig.CNFVar} {new1 : Nat} {hnew1 : new1 < aig.decls.size} {new2 : Nat} {hnew2 : new2 < aig.decls.size} (cache1 : Cache aig cnf1) (cache2 : Cache aig cnf2) (cache3 : Cache aig cnf3) (h12 : cache1.IsExtensionBy cache2 new1 hnew1) (h23 : cache2.IsExtensionBy cache3 new2 hnew2) :
cache1.IsExtensionBy cache3 new2 hnew2
source
theorem Std.Sat.AIG.toCNF.Cache.IsExtensionBy_rfl {aig : AIG Nat} {cnf : CNF aig.CNFVar} {idx : Nat} {omega : idx < aig.decls.size} (cache : Cache aig cnf) {h : idx < cache.marks.size} (hmarked : cache.marks[idx] = true) :
cache.IsExtensionBy cache idx ⋯

Cache extension is a reflexive relation.

source
theorem Std.Sat.AIG.toCNF.Cache.IsExtensionBy_set {aig : AIG Nat} {cnf1 cnf2 : CNF aig.CNFVar} (cache1 : Cache aig cnf1) (cache2 : Cache aig cnf2) (idx : Nat) (hbound : idx < cache1.marks.size) (h : cache2.marks = cache1.marks.set idx true hbound) :
cache1.IsExtensionBy cache2 idx ⋯
source
def Std.Sat.AIG.toCNF.Cache.init (aig : AIG Nat) :
Cache aig []

A cache with no entries is valid for an empty CNF.

Equations

- Std.Sat.AIG.toCNF.Cache.init aig = { marks := Array.replicate aig.decls.size false, hmarks := ⋯, inv := ⋯ }

Instances For

source
def Std.Sat.AIG.toCNF.Cache.addFalse {aig : AIG Nat} {cnf : CNF aig.CNFVar} (cache : Cache aig cnf) (idx : Nat) (h : idx < aig.decls.size) (htip : aig.decls[idx] = Decl.false) :
{ out : Cache aig (Decl.falseToCNF (Sum.inr ⟨idx, h⟩) ++ cnf) // cache.IsExtensionBy out idx h }

Add a `Decl.false` to a `Cache`.

Equations

- cache.addFalse idx h htip = ⟨{ marks := cache.marks.set idx true ⋯, hmarks := ⋯, inv := ⋯ }, ⋯⟩

Instances For

source
def Std.Sat.AIG.toCNF.Cache.addAtom {aig : AIG Nat} {cnf : CNF aig.CNFVar} {a : Nat} (cache : Cache aig cnf) (idx : Nat) (h : idx < aig.decls.size) (htip : aig.decls[idx] = Decl.atom a) :
{ out : Cache aig (Decl.atomToCNF (Sum.inr ⟨idx, h⟩) (Sum.inl a) ++ cnf) // cache.IsExtensionBy out idx h }

Add a `Decl.atom` to a cache.

Equations

- cache.addAtom idx h htip = ⟨{ marks := cache.marks.set idx true ⋯, hmarks := ⋯, inv := ⋯ }, ⋯⟩

Instances For

source
def Std.Sat.AIG.toCNF.Cache.addGate {aig : AIG Nat} {cnf : CNF aig.CNFVar} {lhs rhs : Fanin} (cache : Cache aig cnf) {hlb : lhs.gate < cache.marks.size} {hrb : rhs.gate < cache.marks.size} (idx : Nat) (h : idx < aig.decls.size) (htip : aig.decls[idx] = Decl.gate lhs rhs) (hl : cache.marks[lhs.gate] = true) (hr : cache.marks[rhs.gate] = true) :
{ out : Cache aig (Decl.gateToCNF (Sum.inr ⟨idx, h⟩) (Sum.inr ⟨lhs.gate, ⋯⟩) (Sum.inr ⟨rhs.gate, ⋯⟩) lhs.invert rhs.invert ++ cnf) // cache.IsExtensionBy out idx h }

Add a `Decl.gate` to a cache.

Equations

- cache.addGate idx h htip hl hr = ⟨{ marks := cache.marks.set idx true ⋯, hmarks := ⋯, inv := ⋯ }, ⋯⟩

Instances For

source
def Std.Sat.AIG.toCNF.State.Inv {aig : AIG Nat} (cnf : CNF aig.CNFVar) :
Prop

The key invariant about the `State` itself (without cache): The CNF we produce is always satisfiable at `cnfSatAssignment`.

Equations

- Std.Sat.AIG.toCNF.State.Inv cnf = ∀ (assign1 : Nat → Bool), Std.Sat.CNF.Sat (Std.Sat.AIG.toCNF.cnfSatAssignment aig assign1) cnf

Instances For

source
theorem Std.Sat.AIG.toCNF.State.Inv_nil {aig : AIG Nat} :
Inv []

The `State` invariant always holds when we have an empty CNF.

source
theorem Std.Sat.AIG.toCNF.State.Inv_append {aig✝ : AIG Nat} {cnf1 cnf2 : CNF aig✝.CNFVar} (h1 : Inv cnf1) (h2 : Inv cnf2) :
Inv (cnf1 ++ cnf2)

Combining two CNFs for which `State.Inv` holds preserves `State.Inv`.

source
theorem Std.Sat.AIG.toCNF.State.Inv_falseToCNF {upper : Nat} {aig : AIG Nat} {h : upper < aig.decls.size} (heq : aig.decls[upper] = Decl.false) :
Inv (Decl.falseToCNF (Sum.inr ⟨upper, h⟩))

`State.Inv` holds for the CNF that we produce for a `Decl.false`.

source
theorem Std.Sat.AIG.toCNF.State.Inv_atomToCNF {upper : Nat} {aig : AIG Nat} {h : upper < aig.decls.size} {a : Nat} (heq : aig.decls[upper] = Decl.atom a) :
Inv (Decl.atomToCNF (Sum.inr ⟨upper, h⟩) (Sum.inl a))

`State.Inv` holds for the CNF that we produce for a `Decl.atom`

source
theorem Std.Sat.AIG.toCNF.State.Inv_gateToCNF {upper : Nat} {lhs rhs : Fanin} {aig : AIG Nat} {h : upper < aig.decls.size} (heq : aig.decls[upper] = Decl.gate lhs rhs) :
Inv (Decl.gateToCNF (Sum.inr ⟨upper, h⟩) (Sum.inr ⟨lhs.gate, ⋯⟩) (Sum.inr ⟨rhs.gate, ⋯⟩) lhs.invert rhs.invert)

`State.Inv` holds for the CNF that we produce for a `Decl.gate`

source
structure Std.Sat.AIG.toCNF.State (aig : AIG Nat) :
Type

The state to accumulate CNF clauses as we run our Tseitin transformation on the AIG.

- cnf : CNF aig.CNFVar

  The CNF clauses so far.

- cache : Cache aig self.cnf

  A cache so that we don't generate CNF for an AIG node more than once.

- inv : Inv self.cnf

  The invariant that `cnf` has to maintain as we build it up.

Instances For

source
def Std.Sat.AIG.toCNF.State.empty (aig : AIG Nat) :
State aig

An initial state with no CNF clauses and an empty cache.

Equations

- Std.Sat.AIG.toCNF.State.empty aig = { cnf := [], cache := Std.Sat.AIG.toCNF.Cache.init aig, inv := ⋯ }

Instances For

source
@[reducible, inline]
abbrev Std.Sat.AIG.toCNF.State.IsExtensionBy {aig : AIG Nat} (state1 state2 : State aig) (new : Nat) (hnew : new < aig.decls.size) :
Prop

State extension are `Cache.IsExtensionBy` for now.

Equations

- state1.IsExtensionBy state2 new hnew = state1.cache.IsExtensionBy state2.cache new hnew

Instances For

source
theorem Std.Sat.AIG.toCNF.State.IsExtensionBy_trans_left {aig : AIG Nat} {new1 : Nat} {hnew1 : new1 < aig.decls.size} {new2 : Nat} {hnew2 : new2 < aig.decls.size} (state1 state2 state3 : State aig) (h12 : state1.IsExtensionBy state2 new1 hnew1) (h23 : state2.IsExtensionBy state3 new2 hnew2) :
state1.IsExtensionBy state3 new1 hnew1
source
theorem Std.Sat.AIG.toCNF.State.IsExtensionBy_trans_right {aig : AIG Nat} {new1 : Nat} {hnew1 : new1 < aig.decls.size} {new2 : Nat} {hnew2 : new2 < aig.decls.size} (state1 state2 state3 : State aig) (h12 : state1.IsExtensionBy state2 new1 hnew1) (h23 : state2.IsExtensionBy state3 new2 hnew2) :
state1.IsExtensionBy state3 new2 hnew2
source
theorem Std.Sat.AIG.toCNF.State.IsExtensionBy_rfl {aig : AIG Nat} {idx : Nat} {omega : idx < aig.decls.size} (state : State aig) {h : idx < state.cache.marks.size} (hmarked : state.cache.marks[idx] = true) :
state.IsExtensionBy state idx ⋯

State extension is a reflexive relation.

source
def Std.Sat.AIG.toCNF.State.addFalse {aig : AIG Nat} (state : State aig) (idx : Nat) (h : idx < aig.decls.size) (htip : aig.decls[idx] = Decl.false) :
{ out : State aig // state.IsExtensionBy out idx h }

Add the CNF for a `Decl.false` to the state.

Equations

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

Instances For

source
def Std.Sat.AIG.toCNF.State.addAtom {aig : AIG Nat} {a : Nat} (state : State aig) (idx : Nat) (h : idx < aig.decls.size) (htip : aig.decls[idx] = Decl.atom a) :
{ out : State aig // state.IsExtensionBy out idx h }

Add the CNF for a `Decl.atom` to the state.

Equations

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

Instances For

source
def Std.Sat.AIG.toCNF.State.addGate {aig : AIG Nat} {lhs rhs : Fanin} (state : State aig) {hlb : lhs.gate < state.cache.marks.size} {hrb : rhs.gate < state.cache.marks.size} (idx : Nat) (h : idx < aig.decls.size) (htip : aig.decls[idx] = Decl.gate lhs rhs) (hl : state.cache.marks[lhs.gate] = true) (hr : state.cache.marks[rhs.gate] = true) :
{ out : State aig // state.IsExtensionBy out idx h }

Add the CNF for a `Decl.gate` to the state.

Equations

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

Instances For

source
def Std.Sat.AIG.toCNF.State.eval {aig : AIG Nat} (assign : aig.CNFVar → Bool) (state : State aig) :
Bool

Evaluate the CNF contained within the state.

Equations

- Std.Sat.AIG.toCNF.State.eval assign state = Std.Sat.CNF.eval assign state.cnf

Instances For

source
def Std.Sat.AIG.toCNF.State.Sat {aig : AIG Nat} (assign : aig.CNFVar → Bool) (state : State aig) :
Prop

The CNF within the state is sat.

Equations

- Std.Sat.AIG.toCNF.State.Sat assign state = Std.Sat.CNF.Sat assign state.cnf

Instances For

source
def Std.Sat.AIG.toCNF.State.Unsat {aig : AIG Nat} (state : State aig) :
Prop

The CNF within the state is unsat.

Equations

- state.Unsat = state.cnf.Unsat

Instances For

source
theorem Std.Sat.AIG.toCNF.State.sat_def {aig : AIG Nat} (assign : aig.CNFVar → Bool) (state : State aig) :
Sat assign state ↔ CNF.Sat assign state.cnf
source
theorem Std.Sat.AIG.toCNF.State.unsat_def {aig : AIG Nat} (state : State aig) :
state.Unsat ↔ state.cnf.Unsat
source
@[simp]
theorem Std.Sat.AIG.toCNF.State.eval_eq {aig✝ : AIG Nat} {assign : aig✝.CNFVar → Bool} {state : State aig✝} :
eval assign state = CNF.eval assign state.cnf
source
@[simp]
theorem Std.Sat.AIG.toCNF.State.sat_iff {aig✝ : AIG Nat} {assign : aig✝.CNFVar → Bool} {state : State aig✝} :
Sat assign state ↔ CNF.Sat assign state.cnf
source
@[simp]
theorem Std.Sat.AIG.toCNF.State.unsat_iff {aig✝ : AIG Nat} {state : State aig✝} :
state.Unsat ↔ state.cnf.Unsat
source
def Std.Sat.AIG.toCNF (entry : Entrypoint Nat) :
CNF Nat

Convert an AIG into CNF, starting at some entry node.

Equations

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

Instances For

source
theorem Std.Sat.AIG.toCNF_equisat (entry : Entrypoint Nat) :
(toCNF entry).Unsat ↔ entry.Unsat

An AIG is unsat iff its CNF is unsat.