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

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

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

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)

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.

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.

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.

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.