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

- aig.mkNotCached gate = { aig := aig, ref := gate.not }

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

- aig.mkAndCached input = aig.mkGateCached input

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

- aig.mkOrCached input = { aig := (aig.mkGateCached (input.invert true true)).aig, ref := (aig.mkGateCached (input.invert true true)).ref.not }

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

- One or more equations did not get rendered due to their size.

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

- One or more equations did not get rendered due to their size.

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

- aig.mkImpCached input = { aig := (aig.mkGateCached (input.invert false true)).aig, ref := (aig.mkGateCached (input.invert false true)).ref.not }

Instances For