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.

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
  • One or more equations did not get rendered due to their size.
Instances For

    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
    • One or more equations did not get rendered due to their size.
    Instances For
      def Std.Sat.AIG.mkGateCached {α : Type} [Hashable α] [DecidableEq α] (aig : Std.Sat.AIG α) (input : aig.GateInput) :

      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
      • One or more equations did not get rendered due to their size.
      Instances For
        def Std.Sat.AIG.mkGateCached.go {α : Type} [Hashable α] [DecidableEq α] (aig : Std.Sat.AIG α) (input : aig.GateInput) :
        Equations
        • One or more equations did not get rendered due to their size.
        Instances For