Documentation

Std.Sat.AIG.Cached

This module contains functions to construct AIG nodes while making use of the sub-circuit cache if possible. For performance reasons these functions should usually be preferred over the naive AIG node creation ones.

def Std.Sat.AIG.mkAtomCached {α : Type} [Hashable α] [DecidableEq α] (aig : AIG α) (n : α) :

A version of AIG.mkAtom that uses the subterm cache in AIG. This version is meant for programming, for proving purposes use AIG.mkAtom and equality theorems to this one.

Equations
    Instances For
      @[inline]
      def Std.Sat.AIG.mkConstCached {α : Type} [Hashable α] [DecidableEq α] (aig : AIG α) (val : Bool) :

      A version of AIG.mkConst that uses the subterm cache in AIG. This version is meant for programming, for proving purposes use AIG.mkGate and equality theorems to this one.

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

          A version of AIG.mkGate that uses the subterm cache in AIG. This version is meant for programming, for proving purposes use AIG.mkGate and equality theorems to this one.

          Beyond caching this function also implements a subset of the optimizations presented in:

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