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 α

A version of AIG.mkAtom that uses the subterm cache in AIG. This version is meant for programming, for proving purposes use AIG.mkAtom and equality theorems to this one.

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) : Entrypoint α

A version of AIG.mkConst that uses the subterm cache in AIG. This version is meant for programming, for proving purposes use AIG.mkGate and equality theorems to this one.

Equations

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

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

A version of AIG.mkGate that uses the subterm cache in AIG. This version is meant for programming, for proving purposes use AIG.mkGate and equality theorems to this one.

Beyond caching this function also implements a subset of the optimizations presented in:

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.