Documentation

Std.Sat.AIG.CNF

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.

def Std.Sat.AIG.Decl.constToCNF {α : Type u_1} (output : α) (const : Bool) :

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

Equations
Instances For
    def Std.Sat.AIG.Decl.atomToCNF {α : Type u_1} (output : α) (atom : α) :

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

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

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

      Equations
      Instances For
        @[simp]
        theorem Std.Sat.AIG.Decl.constToCNF_eval :
        ∀ {α : Type u_1} {output : α} {b : Bool} {assign : αBool}, Std.Sat.CNF.eval assign (Std.Sat.AIG.Decl.constToCNF output b) = (assign output == b)
        @[simp]
        theorem Std.Sat.AIG.Decl.atomToCNF_eval :
        ∀ {α : Type u_1} {output a : α} {assign : αBool}, Std.Sat.CNF.eval assign (Std.Sat.AIG.Decl.atomToCNF output a) = (assign output == assign a)
        @[simp]
        theorem Std.Sat.AIG.Decl.gateToCNF_eval :
        ∀ {α : Type u_1} {output lhs rhs : α} {linv rinv : Bool} {assign : αBool}, Std.Sat.CNF.eval assign (Std.Sat.AIG.Decl.gateToCNF output lhs rhs linv rinv) = (assign output == ((assign lhs ^^ linv) && (assign rhs ^^ rinv)))
        @[reducible, inline]
        Equations
        Instances For
          def Std.Sat.AIG.toCNF.mixAssigns {aig : Std.Sat.AIG Nat} (assign1 : NatBool) (assign2 : Fin aig.decls.sizeBool) :
          aig.CNFVarBool

          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
          Instances For
            def Std.Sat.AIG.toCNF.projectLeftAssign {aig : Std.Sat.AIG Nat} (assign : aig.CNFVarBool) :
            NatBool

            Project the atom assignment out of a CNF assignment

            Equations
            Instances For
              def Std.Sat.AIG.toCNF.projectRightAssign {aig : Std.Sat.AIG Nat} (assign : aig.CNFVarBool) (idx : Nat) :
              idx < aig.decls.sizeBool

              Project the auxiliary variable assignment out of a CNF assignment

              Equations
              Instances For
                @[simp]
                theorem Std.Sat.AIG.toCNF.projectLeftAssign_property :
                ∀ {aig : Std.Sat.AIG Nat} {assign : aig.CNFVarBool} {x : Nat}, Std.Sat.AIG.toCNF.projectLeftAssign assign x = assign (Sum.inl x)
                @[simp]
                theorem Std.Sat.AIG.toCNF.projectRightAssign_property :
                ∀ {aig : Std.Sat.AIG Nat} {assign : aig.CNFVarBool} {x : Nat} {hx : x < aig.decls.size}, Std.Sat.AIG.toCNF.projectRightAssign assign x hx = assign (Sum.inr x, hx)
                def Std.Sat.AIG.toCNF.cnfSatAssignment (aig : Std.Sat.AIG Nat) (assign1 : NatBool) :
                aig.CNFVarBool

                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
                Instances For
                  @[simp]
                  theorem Std.Sat.AIG.toCNF.satAssignment_inl {aig : Std.Sat.AIG Nat} {assign1 : NatBool} {x : Nat} :
                  Std.Sat.AIG.toCNF.cnfSatAssignment aig assign1 (Sum.inl x) = assign1 x
                  @[simp]
                  theorem Std.Sat.AIG.toCNF.satAssignment_inr {aig : Std.Sat.AIG Nat} {assign1 : NatBool} {x : Fin aig.decls.size} :
                  Std.Sat.AIG.toCNF.cnfSatAssignment aig assign1 (Sum.inr x) = assign1, { aig := aig, ref := { gate := x, hgate := } }
                  structure Std.Sat.AIG.toCNF.Cache.Inv {aig : Std.Sat.AIG Nat} (cnf : Std.Sat.CNF aig.CNFVar) (marks : Array Bool) (hmarks : marks.size = aig.decls.size) :

                  The central invariants for the Cache.

                  • hmark : ∀ (lhs rhs : Nat) (linv rinv : Bool) (idx : Nat) (hbound : idx < aig.decls.size), marks[idx] = true∀ (heq : aig.decls[idx] = Std.Sat.AIG.Decl.gate lhs rhs linv rinv), marks[lhs] = true marks[rhs] = true

                    If there exists an AIG node that is marked, its children are also guaranteed to be marked already. This allows us to conclude that if a gate node is marked, all of its (transitive) children are also marked.

                  • heval : ∀ (assign : aig.CNFVarBool), Std.Sat.CNF.eval assign cnf = true∀ (idx : Nat) (hbound : idx < aig.decls.size), marks[idx] = trueStd.Sat.AIG.toCNF.projectLeftAssign assign, { aig := aig, ref := { gate := idx, hgate := hbound } } = Std.Sat.AIG.toCNF.projectRightAssign assign idx hbound

                    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 (and all required children CNFs according to hmark) are 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.

                  Instances For
                    theorem Std.Sat.AIG.toCNF.Cache.Inv.hmark {aig : Std.Sat.AIG Nat} {cnf : Std.Sat.CNF aig.CNFVar} {marks : Array Bool} {hmarks : marks.size = aig.decls.size} (self : Std.Sat.AIG.toCNF.Cache.Inv cnf marks hmarks) (lhs : Nat) (rhs : Nat) (linv : Bool) (rinv : Bool) (idx : Nat) (hbound : idx < aig.decls.size) (_hmarked : marks[idx] = true) (heq : aig.decls[idx] = Std.Sat.AIG.Decl.gate lhs rhs linv rinv) :
                    marks[lhs] = true marks[rhs] = true

                    If there exists an AIG node that is marked, its children are also guaranteed to be marked already. This allows us to conclude that if a gate node is marked, all of its (transitive) children are also marked.

                    theorem Std.Sat.AIG.toCNF.Cache.Inv.heval {aig : Std.Sat.AIG Nat} {cnf : Std.Sat.CNF aig.CNFVar} {marks : Array Bool} {hmarks : marks.size = aig.decls.size} (self : Std.Sat.AIG.toCNF.Cache.Inv cnf marks hmarks) (assign : aig.CNFVarBool) (_heval : Std.Sat.CNF.eval assign cnf = true) (idx : Nat) (hbound : idx < aig.decls.size) (_hmark : marks[idx] = true) :
                    Std.Sat.AIG.toCNF.projectLeftAssign assign, { aig := aig, ref := { gate := idx, hgate := hbound } } = Std.Sat.AIG.toCNF.projectRightAssign assign idx hbound

                    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 (and all required children CNFs according to hmark) are 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.

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

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

                    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 : Std.Sat.AIG.toCNF.Cache.Inv cnf self.marks

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

                    Instances For
                      theorem Std.Sat.AIG.toCNF.Cache.hmarks {aig : Std.Sat.AIG Nat} {cnf : Std.Sat.CNF aig.CNFVar} (self : Std.Sat.AIG.toCNF.Cache aig cnf) :
                      self.marks.size = aig.decls.size

                      There are always as many marks as AIG nodes.

                      theorem Std.Sat.AIG.toCNF.Cache.inv {aig : Std.Sat.AIG Nat} {cnf : Std.Sat.CNF aig.CNFVar} (self : Std.Sat.AIG.toCNF.Cache aig cnf) :
                      Std.Sat.AIG.toCNF.Cache.Inv cnf self.marks

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

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

                      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] = truecache2.marks[idx] = true

                        No entry is invalidated.

                      • trueAt : cache2.marks[new] = true

                        The second cache is true at the new index.

                      Instances For
                        theorem Std.Sat.AIG.toCNF.Cache.IsExtensionBy.extension {aig : Std.Sat.AIG Nat} {cnf1 : Std.Sat.CNF aig.CNFVar} {cnf2 : Std.Sat.CNF aig.CNFVar} {cache1 : Std.Sat.AIG.toCNF.Cache aig cnf1} {cache2 : Std.Sat.AIG.toCNF.Cache aig cnf2} {new : Nat} {hnew : new < aig.decls.size} (self : cache1.IsExtensionBy cache2 new hnew) (idx : Nat) (hidx : idx < aig.decls.size) :
                        cache1.marks[idx] = truecache2.marks[idx] = true

                        No entry is invalidated.

                        theorem Std.Sat.AIG.toCNF.Cache.IsExtensionBy.trueAt {aig : Std.Sat.AIG Nat} {cnf1 : Std.Sat.CNF aig.CNFVar} {cnf2 : Std.Sat.CNF aig.CNFVar} {cache1 : Std.Sat.AIG.toCNF.Cache aig cnf1} {cache2 : Std.Sat.AIG.toCNF.Cache aig cnf2} {new : Nat} {hnew : new < aig.decls.size} (self : cache1.IsExtensionBy cache2 new hnew) :
                        cache2.marks[new] = true

                        The second cache is true at the new index.

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

                        Cache extension is a reflexive relation.

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

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

                        Equations
                        Instances For
                          def Std.Sat.AIG.toCNF.Cache.addConst {aig : Std.Sat.AIG Nat} {cnf : Std.Sat.CNF aig.CNFVar} {b : Bool} (cache : Std.Sat.AIG.toCNF.Cache aig cnf) (idx : Nat) (h : idx < aig.decls.size) (htip : aig.decls[idx] = Std.Sat.AIG.Decl.const b) :
                          { out : Std.Sat.AIG.toCNF.Cache aig (Std.Sat.AIG.Decl.constToCNF (Sum.inr idx, h) b ++ cnf) // cache.IsExtensionBy out idx h }

                          Add a Decl.const to a Cache.

                          Equations
                          • cache.addConst idx h htip = { marks := cache.marks.set idx, true, hmarks := , inv := },
                          Instances For
                            def Std.Sat.AIG.toCNF.Cache.addAtom {aig : Std.Sat.AIG Nat} {cnf : Std.Sat.CNF aig.CNFVar} {a : Nat} (cache : Std.Sat.AIG.toCNF.Cache aig cnf) (idx : Nat) (h : idx < aig.decls.size) (htip : aig.decls[idx] = Std.Sat.AIG.Decl.atom a) :
                            { out : Std.Sat.AIG.toCNF.Cache aig (Std.Sat.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
                              def Std.Sat.AIG.toCNF.Cache.addGate {aig : Std.Sat.AIG Nat} {cnf : Std.Sat.CNF aig.CNFVar} {lhs : Nat} {rhs : Nat} {linv : Bool} {rinv : Bool} (cache : Std.Sat.AIG.toCNF.Cache aig cnf) {hlb : lhs < cache.marks.size} {hrb : rhs < cache.marks.size} (idx : Nat) (h : idx < aig.decls.size) (htip : aig.decls[idx] = Std.Sat.AIG.Decl.gate lhs rhs linv rinv) (hl : cache.marks[lhs] = true) (hr : cache.marks[rhs] = true) :
                              { out : Std.Sat.AIG.toCNF.Cache aig (Std.Sat.AIG.Decl.gateToCNF (Sum.inr idx, h) (Sum.inr lhs, ) (Sum.inr rhs, ) linv rinv ++ 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

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

                                Equations
                                Instances For

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

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

                                  theorem Std.Sat.AIG.toCNF.State.Inv_constToCNF {upper : Nat} {aig : Std.Sat.AIG Nat} {h : upper < aig.decls.size} {b : Bool} (heq : aig.decls[upper] = Std.Sat.AIG.Decl.const b) :

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

                                  theorem Std.Sat.AIG.toCNF.State.Inv_atomToCNF {upper : Nat} {aig : Std.Sat.AIG Nat} {h : upper < aig.decls.size} {a : Nat} (heq : aig.decls[upper] = Std.Sat.AIG.Decl.atom a) :

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

                                  theorem Std.Sat.AIG.toCNF.State.Inv_gateToCNF {upper : Nat} {lhs : Nat} {rhs : Nat} {linv : Bool} {rinv : Bool} {aig : Std.Sat.AIG Nat} {h : upper < aig.decls.size} (heq : aig.decls[upper] = Std.Sat.AIG.Decl.gate lhs rhs linv rinv) :
                                  Std.Sat.AIG.toCNF.State.Inv (Std.Sat.AIG.Decl.gateToCNF (Sum.inr upper, h) (Sum.inr lhs, ) (Sum.inr rhs, ) linv rinv)

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

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

                                  Instances For

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

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

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

                                      State extension are Cache.IsExtensionBy for now.

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

                                        State extension is a reflexive relation.

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

                                        Add the CNF for a Decl.const to the state.

                                        Equations
                                        • One or more equations did not get rendered due to their size.
                                        Instances For
                                          def Std.Sat.AIG.toCNF.State.addAtom {aig : Std.Sat.AIG Nat} {a : Nat} (state : Std.Sat.AIG.toCNF.State aig) (idx : Nat) (h : idx < aig.decls.size) (htip : aig.decls[idx] = Std.Sat.AIG.Decl.atom a) :
                                          { out : Std.Sat.AIG.toCNF.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
                                            def Std.Sat.AIG.toCNF.State.addGate {aig : Std.Sat.AIG Nat} {lhs : Nat} {rhs : Nat} {linv : Bool} {rinv : Bool} (state : Std.Sat.AIG.toCNF.State aig) {hlb : lhs < state.cache.marks.size} {hrb : rhs < state.cache.marks.size} (idx : Nat) (h : idx < aig.decls.size) (htip : aig.decls[idx] = Std.Sat.AIG.Decl.gate lhs rhs linv rinv) (hl : state.cache.marks[lhs] = true) (hr : state.cache.marks[rhs] = true) :
                                            { out : Std.Sat.AIG.toCNF.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
                                              def Std.Sat.AIG.toCNF.State.eval {aig : Std.Sat.AIG Nat} (assign : aig.CNFVarBool) (state : Std.Sat.AIG.toCNF.State aig) :

                                              Evaluate the CNF contained within the state.

                                              Equations
                                              Instances For
                                                def Std.Sat.AIG.toCNF.State.Sat {aig : Std.Sat.AIG Nat} (assign : aig.CNFVarBool) (state : Std.Sat.AIG.toCNF.State aig) :

                                                The CNF within the state is sat.

                                                Equations
                                                Instances For

                                                  The CNF within the state is unsat.

                                                  Equations
                                                  • state.Unsat = state.cnf.Unsat
                                                  Instances For
                                                    theorem Std.Sat.AIG.toCNF.State.sat_def {aig : Std.Sat.AIG Nat} (assign : aig.CNFVarBool) (state : Std.Sat.AIG.toCNF.State aig) :
                                                    Std.Sat.AIG.toCNF.State.Sat assign state Std.Sat.CNF.Sat assign state.cnf
                                                    theorem Std.Sat.AIG.toCNF.State.unsat_def {aig : Std.Sat.AIG Nat} (state : Std.Sat.AIG.toCNF.State aig) :
                                                    state.Unsat state.cnf.Unsat
                                                    @[simp]
                                                    theorem Std.Sat.AIG.toCNF.State.eval_eq :
                                                    ∀ {aig : Std.Sat.AIG Nat} {assign : aig.CNFVarBool} {state : Std.Sat.AIG.toCNF.State aig}, Std.Sat.AIG.toCNF.State.eval assign state = Std.Sat.CNF.eval assign state.cnf
                                                    @[simp]
                                                    theorem Std.Sat.AIG.toCNF.State.sat_iff :
                                                    ∀ {aig : Std.Sat.AIG Nat} {assign : aig.CNFVarBool} {state : Std.Sat.AIG.toCNF.State aig}, Std.Sat.AIG.toCNF.State.Sat assign state Std.Sat.CNF.Sat assign state.cnf
                                                    @[simp]
                                                    theorem Std.Sat.AIG.toCNF.State.unsat_iff :
                                                    ∀ {aig : Std.Sat.AIG Nat} {state : Std.Sat.AIG.toCNF.State aig}, state.Unsat state.cnf.Unsat

                                                    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
                                                      def Std.Sat.AIG.toCNF.inj {aig : Std.Sat.AIG Nat} (var : aig.CNFVar) :
                                                      Equations
                                                      Instances For
                                                        @[irreducible]
                                                        def Std.Sat.AIG.toCNF.go (aig : Std.Sat.AIG Nat) (upper : Nat) (h : upper < aig.decls.size) (state : Std.Sat.AIG.toCNF.State aig) :
                                                        { out : Std.Sat.AIG.toCNF.State aig // state.IsExtensionBy out upper h }
                                                        Equations
                                                        • One or more equations did not get rendered due to their size.
                                                        Instances For
                                                          theorem Std.Sat.AIG.toCNF.inj_is_injection {aig : Std.Sat.AIG Nat} (a : aig.CNFVar) (b : aig.CNFVar) :

                                                          The function we use to convert from CNF with explicit auxiliary variables to just Nat variables in toCNF is an injection.

                                                          theorem Std.Sat.AIG.toCNF.go_marks {aig : Std.Sat.AIG Nat} {start : Nat} {h : start < aig.decls.size} {state : Std.Sat.AIG.toCNF.State aig} :
                                                          (Std.Sat.AIG.toCNF.go aig start h state).val.cache.marks[start] = true

                                                          The node that we started CNF conversion at will always be marked as visited in the CNF cache.

                                                          theorem Std.Sat.AIG.toCNF.go_sat (aig : Std.Sat.AIG Nat) (start : Nat) (h1 : start < aig.decls.size) (assign1 : NatBool) (state : Std.Sat.AIG.toCNF.State aig) :

                                                          The CNF returned by go will always be SAT at cnfSatAssignment.

                                                          theorem Std.Sat.AIG.toCNF.go_as_denote' (aig : Std.Sat.AIG Nat) (start : Nat) (h1 : start < aig.decls.size) (assign1 : NatBool) :
                                                          assign1, { aig := aig, ref := { gate := start, hgate := h1 } } = trueStd.Sat.AIG.toCNF.State.eval (Std.Sat.AIG.toCNF.cnfSatAssignment aig assign1) (Std.Sat.AIG.toCNF.go aig start h1 (Std.Sat.AIG.toCNF.State.empty aig)).val = true
                                                          theorem Std.Sat.AIG.toCNF.go_as_denote {sat? : Bool} (aig : Std.Sat.AIG Nat) (start : Nat) (h1 : start < aig.decls.size) (assign1 : NatBool) :
                                                          (assign1, { aig := aig, ref := { gate := start, hgate := h1 } } && Std.Sat.AIG.toCNF.State.eval (Std.Sat.AIG.toCNF.cnfSatAssignment aig assign1) (Std.Sat.AIG.toCNF.go aig start h1 (Std.Sat.AIG.toCNF.State.empty aig)).val) = sat?assign1, { aig := aig, ref := { gate := start, hgate := h1 } } = sat?

                                                          Connect SAT results about the CNF to SAT results about the AIG.

                                                          theorem Std.Sat.AIG.toCNF.denote_as_go {aig : Std.Sat.AIG Nat} {start : Nat} {h1 : start < aig.decls.size} {assign : aig.CNFVarBool} :
                                                          Std.Sat.AIG.toCNF.projectLeftAssign assign, { aig := aig, ref := { gate := start, hgate := h1 } } = falseStd.Sat.CNF.eval assign ([(Sum.inr start, h1, true)] :: (Std.Sat.AIG.toCNF.go aig start h1 (Std.Sat.AIG.toCNF.State.empty aig)).val.cnf) = false

                                                          Connect SAT results about the AIG to SAT results about the CNF.

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

                                                          An AIG is unsat iff its CNF is unsat.