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

@[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 }

@[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

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 }

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.

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.

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 }