Documentation

Std.Sat.AIG.CachedGates

This module contains functions to construct basic logic gates while making use of the sub-circuit cache if possible.

source
@[inline]
def Std.Sat.AIG.mkNotCached {α : Type} [Hashable α] [DecidableEq α] (aig : AIG α) (gate : aig.Ref) :
Entrypoint α

Create a not gate in the input AIG. This uses the builtin cache to enable automated subterm sharing.

Equations
    Instances For
      source
      @[inline]
      def Std.Sat.AIG.mkAndCached {α : Type} [Hashable α] [DecidableEq α] (aig : AIG α) (input : aig.BinaryInput) :
      Entrypoint α

      Create an and gate in the input AIG. This uses the builtin cache to enable automated subterm sharing.

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

          Create an or gate in the input AIG. This uses the builtin cache to enable automated subterm sharing.

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

              Create an xor gate in the input AIG. This uses the builtin cache to enable automated subterm sharing.

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

                  Create an equality gate in the input AIG. This uses the builtin cache to enable automated subterm sharing.

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

                      Create an implication gate in the input AIG. This uses the builtin cache to enable automated subterm sharing.

                      Equations
                        Instances For