This module contains functions to construct AIG nodes while making use of the sub-circuit cache if possible. For performance reasons these functions should usually be preferred over the naive AIG node creation ones.

def Std.Sat.AIG.mkAtomCached {α : Type} [Hashable α] [DecidableEq α] (aig : AIG α) (n : α) : Entrypoint α

Add a new input node to aig.

Equations

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

@[inline]

def Std.Sat.AIG.mkConstCached {α : Type} [Hashable α] [DecidableEq α] (aig : AIG α) (val : Bool) : aig.Ref

Add a new constant node to aig.

Equations

• aig.mkConstCached val = { gate := 0, invert := val, hgate := ⋯ }

def Std.Sat.AIG.mkGateCached {α : Type} [Hashable α] [DecidableEq α] (aig : AIG α) (input : aig.BinaryInput) : Entrypoint α

Add a new and inverter gate to the AIG in aig.

Beyond caching this function also implements a subset of the optimizations presented in: "Local Two-Level And-Inverter Graph Minimization without Blowu" (https://cca.informatik.uni-freiburg.de/papers/BrummayerBiere-MEMICS06.pdf)

Equations

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

def Std.Sat.AIG.mkGateCached.go {α : Type} [Hashable α] [DecidableEq α] (aig : AIG α) (input : aig.BinaryInput) : Entrypoint α

Equations

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