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
def Std.Sat.AIG.mkNotCached {α : Type} [Hashable α] [DecidableEq α] (aig : Std.Sat.AIG α) (gate : aig.Ref) :
Std.Sat.AIG.Entrypoint α

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

Equations
  • aig.mkNotCached gate = (aig.mkConstCached true).aig.mkGateCached { lhs := { ref := (aig.mkConstCached true).ref, inv := false }, rhs := { ref := gate.cast ⋯, inv := true } }
Instances For
source
@[inline]
def Std.Sat.AIG.BinaryInput.asGateInput {α : Type} [Hashable α] [DecidableEq α] {aig : Std.Sat.AIG α} (input : aig.BinaryInput) (linv : Bool) (rinv : Bool) :
aig.GateInput
Equations
  • input.asGateInput linv rinv = { lhs := { ref := input.lhs, inv := linv }, rhs := { ref := input.rhs, inv := rinv } }
source
def Std.Sat.AIG.mkAndCached {α : Type} [Hashable α] [DecidableEq α] (aig : Std.Sat.AIG α) (input : aig.BinaryInput) :
Std.Sat.AIG.Entrypoint α

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

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

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

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

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

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

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

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

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

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