Documentation

Std.Sat.AIG.Basic

This module contains the basic definitions for an AIG (And Inverter Graph) in the style of AIGNET, as described in https://arxiv.org/pdf/1304.7861.pdf section 3. It consists of an AIG definition, a description of its semantics and basic operations to construct nodes in the AIG.

This datatype is isomorphic to a pair of a Nat and a Bool, however the Bool is stored in the lowest bit of the Nat in order to save memory. It is used to describe an input to an AIG circuit node which consists of a Nat describing the input node and a Bool saying whether there is an inverter on the input.

  • ofRaw :: (
  • )
Instances For
    def Std.Sat.AIG.instDecidableEqFanin.decEq (x✝ x✝¹ : Fanin) :
    Decidable (x✝ = x✝¹)
    Equations
    Instances For
      @[inline]
      def Std.Sat.AIG.Fanin.mk (gate : Nat) (invert : Bool) :

      The public constructor of Fanin.

      Equations
      Instances For
        @[inline]

        Get the gate.

        Equations
        Instances For
          @[inline]

          Get the inverter bit.

          Equations
          Instances For
            @[inline]

            Flip the inverter bit according to val.

            Equations
            Instances For
              @[simp]
              theorem Std.Sat.AIG.Fanin.gate_mk {g : Nat} {i : Bool} :
              (mk g i).gate = g
              @[simp]
              theorem Std.Sat.AIG.Fanin.invert_mk {g : Nat} {i : Bool} :
              (mk g i).invert = i
              @[simp]
              theorem Std.Sat.AIG.Fanin.gate_flip {v : Bool} (f : Fanin) :
              (f.flip v).gate = f.gate
              @[simp]
              inductive Std.Sat.AIG.Decl (α : Type) :

              A circuit node. These are not recursive but instead contain indices into an AIG, with inputs indexed by α.

              • false {α : Type} : Decl α

                A node with the constant value false. The constant true can be represented with a Ref to false with invert set true

              • atom {α : Type} (idx : α) : Decl α

                An input node to the circuit.

              • gate {α : Type} (l r : Fanin) : Decl α

                An AIG gate with configurable input nodes and polarity. l and r are the input nodes together with their inverter bit.

              Instances For
                def Std.Sat.AIG.instReprDecl.repr {α✝ : Type} [Repr α✝] :
                Decl α✝NatFormat
                Equations
                Instances For
                  inductive Std.Sat.AIG.Cache.WF {α : Type} [Hashable α] [DecidableEq α] :
                  Array (Decl α)HashMap (Decl α) NatProp

                  Cache.WF xs is a predicate asserting that a cache : HashMap (Decl α) Nat is a valid lookup cache for xs : Array (Decl α), that is, whenever cache.find? decl returns an index into xs : Array Decl, xs[index] = decl. Note that this predicate does not force the cache to be complete, if there is no entry in the cache for some node, it can still exist in the AIG.

                  Instances For
                    def Std.Sat.AIG.Cache (α : Type) [DecidableEq α] [Hashable α] (decls : Array (Decl α)) :

                    A cache for reusing elements from decls if they are available.

                    Equations
                    Instances For
                      @[irreducible, inline]
                      def Std.Sat.AIG.Cache.empty {α : Type} [Hashable α] [DecidableEq α] {decls : Array (Decl α)} :
                      Cache α decls

                      Create an empty Cache, valid with respect to any Array Decl.

                      Equations
                      Instances For
                        @[irreducible, inline]
                        def Std.Sat.AIG.Cache.noUpdate {α : Type} [Hashable α] [DecidableEq α] {decls : Array (Decl α)} {decl : Decl α} (cache : Cache α decls) :
                        Cache α (decls.push decl)

                        Given a cache, valid with respect to some decls, we can extend the decls without extending the cache and remain valid.

                        Equations
                        Instances For
                          @[irreducible, inline]
                          def Std.Sat.AIG.Cache.insert {α : Type} [Hashable α] [DecidableEq α] (decls : Array (Decl α)) (cache : Cache α decls) (decl : Decl α) :
                          Cache α (decls.push decl)

                          Given a cache, valid with respect to some decls, we can extend the decls and the cache at the same time with the same values and remain valid.

                          Equations
                          Instances For
                            structure Std.Sat.AIG.CacheHit {α : Type} (decls : Array (Decl α)) (decl : Decl α) :

                            Contains the index of decl in decls along with a proof that the index is indeed correct.

                            Instances For
                              theorem Std.Sat.AIG.Cache.get?_bounds {α : Type} [Hashable α] [DecidableEq α] {decls : Array (Decl α)} {idx : Nat} (c : Cache α decls) (decl : Decl α) (hfound : c.val[decl]? = some idx) :
                              idx < decls.size

                              For a c : Cache α decls, any index idx that is a cache hit for some decl is within bounds of decls (i.e. idx < decls.size).

                              theorem Std.Sat.AIG.Cache.get?_property {α : Type} [Hashable α] [DecidableEq α] {decls : Array (Decl α)} {idx : Nat} (c : Cache α decls) (decl : Decl α) (hfound : c.val[decl]? = some idx) :
                              decls[idx] = decl

                              If Cache.get? decl returns some i then decls[i] = decl holds.

                              @[irreducible, inline]
                              def Std.Sat.AIG.Cache.get? {α : Type} [Hashable α] [DecidableEq α] {decls : Array (Decl α)} (cache : Cache α decls) (decl : Decl α) :
                              Option (CacheHit decls decl)

                              Lookup a Decl in a Cache.

                              Equations
                              Instances For
                                def Std.Sat.AIG.IsDAG (α : Type) (decls : Array (Decl α)) :

                                An Array Decl is a Direct Acyclic Graph (DAG) if a gate at index i only points to nodes with index lower than i.

                                Equations
                                Instances For

                                  The empty AIG is a DAG.

                                  structure Std.Sat.AIG (α : Type) [DecidableEq α] [Hashable α] :

                                  An And Inverter Graph together with a cache for subterm sharing.

                                  Instances For
                                    def Std.Sat.AIG.empty {α : Type} [Hashable α] [DecidableEq α] :
                                    AIG α

                                    An AIG with an empty AIG and cache.

                                    Equations
                                    Instances For
                                      def Std.Sat.AIG.Mem {α : Type} [Hashable α] [DecidableEq α] (aig : AIG α) (a : α) :

                                      The atom a occurs in aig.

                                      Equations
                                      Instances For
                                        structure Std.Sat.AIG.Ref {α : Type} [Hashable α] [DecidableEq α] (aig : AIG α) :

                                        A reference to a node within an AIG.

                                        Instances For
                                          @[inline]
                                          def Std.Sat.AIG.Ref.cast {α : Type} [Hashable α] [DecidableEq α] {aig1 aig2 : AIG α} (ref : aig1.Ref) (h : aig1.decls.size aig2.decls.size) :
                                          aig2.Ref

                                          A Ref into aig1 is also valid for aig2 if aig1 is smaller than aig2.

                                          Equations
                                          Instances For
                                            @[inline]
                                            def Std.Sat.AIG.Ref.flip {α : Type} [Hashable α] [DecidableEq α] {aig : AIG α} (ref : aig.Ref) (inv : Bool) :
                                            aig.Ref

                                            Flip the polarity of Ref if inv is set.

                                            Equations
                                            Instances For
                                              @[inline]
                                              def Std.Sat.AIG.Ref.not {α : Type} [Hashable α] [DecidableEq α] {aig : AIG α} (ref : aig.Ref) :
                                              aig.Ref

                                              Flip the polarity of Ref.

                                              Equations
                                              Instances For
                                                structure Std.Sat.AIG.BinaryInput {α : Type} [Hashable α] [DecidableEq α] (aig : AIG α) :

                                                A pair of Refs, useful for LawfulOperators that act on two Refs at a time.

                                                Instances For
                                                  @[inline]
                                                  def Std.Sat.AIG.BinaryInput.cast {α : Type} [Hashable α] [DecidableEq α] {aig1 aig2 : AIG α} (input : aig1.BinaryInput) (h : aig1.decls.size aig2.decls.size) :

                                                  The Ref.cast equivalent for BinaryInput.

                                                  Equations
                                                  Instances For
                                                    @[inline]
                                                    def Std.Sat.AIG.BinaryInput.invert {α : Type} [Hashable α] [DecidableEq α] {aig : AIG α} (input : aig.BinaryInput) (linv rinv : Bool) :

                                                    Flip the current inverter settings of the BinaryInput if linv or rinv is set respectively.

                                                    Equations
                                                    Instances For
                                                      structure Std.Sat.AIG.TernaryInput {α : Type} [Hashable α] [DecidableEq α] (aig : AIG α) :

                                                      A collection of 3 of Refs, useful for LawfulOperators that act on three Refs at a time, in particular multiplexer style functions.

                                                      Instances For
                                                        @[inline]
                                                        def Std.Sat.AIG.TernaryInput.cast {α : Type} [Hashable α] [DecidableEq α] {aig1 aig2 : AIG α} (input : aig1.TernaryInput) (h : aig1.decls.size aig2.decls.size) :

                                                        The Ref.cast equivalent for TernaryInput.

                                                        Equations
                                                        Instances For

                                                          An entrypoint into an AIG. This can be used to evaluate a circuit, starting at a certain node, with AIG.denote or to construct bigger circuits on top of this specific node.

                                                          • aig : AIG α

                                                            The AIG that we are in.

                                                          • ref : self.aig.Ref

                                                            The reference to the node in aig that this Entrypoint targets.

                                                          Instances For
                                                            def Std.Sat.AIG.toGraphviz {α : Type} [DecidableEq α] [ToString α] [Hashable α] (entry : Entrypoint α) :

                                                            Transform an Entrypoint into a graphviz string. Useful for debugging purposes.

                                                            Equations
                                                            • One or more equations did not get rendered due to their size.
                                                            Instances For
                                                              @[irreducible]
                                                              def Std.Sat.AIG.toGraphviz.go {α : Type} [DecidableEq α] [ToString α] [Hashable α] (acc : String) (decls : Array (Decl α)) (hinv : IsDAG α decls) (idx : Nat) (hidx : idx < decls.size) :
                                                              Equations
                                                              • One or more equations did not get rendered due to their size.
                                                              Instances For
                                                                Equations
                                                                Instances For
                                                                  def Std.Sat.AIG.toGraphviz.toGraphvizString {α : Type} [DecidableEq α] [ToString α] [Hashable α] (decls : Array (Decl α)) (idx : Fin decls.size) :
                                                                  Equations
                                                                  • One or more equations did not get rendered due to their size.
                                                                  Instances For
                                                                    structure Std.Sat.AIG.RefVec {α : Type} [Hashable α] [DecidableEq α] (aig : AIG α) (w : Nat) :

                                                                    A vector of references into aig. This is the AIG analog of BitVec.

                                                                    Instances For
                                                                      structure Std.Sat.AIG.RefVecEntry (α : Type) [DecidableEq α] [Hashable α] [DecidableEq α] (w : Nat) :

                                                                      A sequence of references bundled with their AIG.

                                                                      Instances For
                                                                        structure Std.Sat.AIG.ShiftTarget {α : Type} [Hashable α] [DecidableEq α] (aig : AIG α) (w : Nat) :

                                                                        A RefVec bundled with constant distance to be shifted by.

                                                                        Instances For
                                                                          structure Std.Sat.AIG.ArbitraryShiftTarget {α : Type} [Hashable α] [DecidableEq α] (aig : AIG α) (m : Nat) :

                                                                          A RefVec bundled with a RefVec as distance to be shifted by.

                                                                          Instances For
                                                                            structure Std.Sat.AIG.ExtendTarget {α : Type} [Hashable α] [DecidableEq α] (aig : AIG α) (newWidth : Nat) :

                                                                            A RefVec to be extended to newWidth.

                                                                            Instances For
                                                                              def Std.Sat.AIG.denote {α : Type} [Hashable α] [DecidableEq α] (assign : αBool) (entry : Entrypoint α) :

                                                                              Evaluate an AIG.Entrypoint using some assignment for atoms.

                                                                              Equations
                                                                              Instances For
                                                                                @[irreducible]
                                                                                def Std.Sat.AIG.denote.go {α : Type} (x : Nat) (decls : Array (Decl α)) (assign : αBool) (h1 : x < decls.size) (h2 : IsDAG α decls) :
                                                                                Equations
                                                                                • One or more equations did not get rendered due to their size.
                                                                                Instances For

                                                                                  Denotation of an AIG at a specific Entrypoint.

                                                                                  Equations
                                                                                  • One or more equations did not get rendered due to their size.
                                                                                  Instances For

                                                                                    Denotation of an AIG at a specific Entrypoint with the Entrypoint being constructed on the fly.

                                                                                    Equations
                                                                                    • One or more equations did not get rendered due to their size.
                                                                                    Instances For
                                                                                      Equations
                                                                                      • One or more equations did not get rendered due to their size.
                                                                                      Instances For
                                                                                        def Std.Sat.AIG.UnsatAt {α : Type} [Hashable α] [DecidableEq α] (aig : AIG α) (start : Nat) (invert : Bool) (h : start < aig.decls.size) :

                                                                                        The denotation of the sub-DAG in the aig at node start is false for all assignments.

                                                                                        Equations
                                                                                        • aig.UnsatAt start invert h = ∀ (assign : αBool), assign, { aig := aig, ref := { gate := start, invert := invert, hgate := h } } = false
                                                                                        Instances For

                                                                                          The denotation of the Entrypoint is false for all assignments.

                                                                                          Equations
                                                                                          Instances For
                                                                                            def Std.Sat.AIG.mkGate {α : Type} [Hashable α] [DecidableEq α] (aig : AIG α) (input : aig.BinaryInput) :

                                                                                            Add a new and inverter gate to the AIG in aig. Note that this version is only meant for proving, for production purposes use AIG.mkGateCached and equality theorems to this one.

                                                                                            Equations
                                                                                            • One or more equations did not get rendered due to their size.
                                                                                            Instances For
                                                                                              def Std.Sat.AIG.mkAtom {α : Type} [Hashable α] [DecidableEq α] (aig : AIG α) (n : α) :

                                                                                              Add a new input node to the AIG in aig. Note that this version is only meant for proving, for production purposes use AIG.mkAtomCached and equality theorems to this one.

                                                                                              Equations
                                                                                              • One or more equations did not get rendered due to their size.
                                                                                              Instances For
                                                                                                def Std.Sat.AIG.mkConst {α : Type} [Hashable α] [DecidableEq α] (aig : AIG α) (val : Bool) :

                                                                                                Add a new constant node to aig. Note that this version is only meant for proving, for production purposes use AIG.mkConstCached and equality theorems to this one.

                                                                                                Equations
                                                                                                • One or more equations did not get rendered due to their size.
                                                                                                Instances For
                                                                                                  def Std.Sat.AIG.isConstant {α : Type} [Hashable α] [DecidableEq α] (aig : AIG α) (ref : aig.Ref) (b : Bool) :

                                                                                                  Determine whether ref is a Decl.const with value b.

                                                                                                  Equations
                                                                                                  Instances For
                                                                                                    def Std.Sat.AIG.getConstant {α : Type} [Hashable α] [DecidableEq α] (aig : AIG α) (ref : aig.Ref) :

                                                                                                    Get the value of ref if it is constant.

                                                                                                    Equations
                                                                                                    Instances For