This module contains the basic definitions for an AIG (And Inverter Graph) in the style of AIGNET, as described in https://arxiv.org/pdf/1304.7861.pdf section 3. It consists of an AIG definition, a description of its semantics and basic operations to construct nodes in the AIG.

structure Std.Sat.AIG.Fanin : Type

This datatype is isomorphic to a pair of a Nat and a Bool, however the Bool is stored in the lowest bit of the Nat in order to save memory. It is used to describe an input to an AIG circuit node which consists of a Nat describing the input node and a Bool saying whether there is an inverter on the input.

• of :: (
• val : Nat
• )

instance Std.Sat.AIG.instHashableFanin : Hashable Fanin

Equations

• Std.Sat.AIG.instHashableFanin = { hash := Std.Sat.AIG.hashFanin✝ }

instance Std.Sat.AIG.instReprFanin : Repr Fanin

Equations

• Std.Sat.AIG.instReprFanin = { reprPrec := Std.Sat.AIG.reprFanin✝ }

instance Std.Sat.AIG.instDecidableEqFanin : DecidableEq Fanin

Equations

• Std.Sat.AIG.instDecidableEqFanin = Std.Sat.AIG.decEqFanin✝

instance Std.Sat.AIG.instInhabitedFanin : Inhabited Fanin

Equations

• Std.Sat.AIG.instInhabitedFanin = { default := { val := default } }

@[inline]

def Std.Sat.AIG.Fanin.mk (gate : Nat) (invert : Bool) : Fanin

The public constructor of Fanin.

Equations

• Std.Sat.AIG.Fanin.mk gate invert = { val := gate * 2 ||| invert.toNat }

@[inline]

def Std.Sat.AIG.Fanin.gate (f : Fanin) : Nat

Get the gate.

Equations

• f.gate = Std.Sat.AIG.Fanin.val✝ f / 2

@[inline]

def Std.Sat.AIG.Fanin.invert (f : Fanin) : Bool

Get the inverter bit.

Equations

• f.invert = (1 &&& Std.Sat.AIG.Fanin.val✝ f != 0)

@[inline]

def Std.Sat.AIG.Fanin.flip (f : Fanin) (val : Bool) : Fanin

Flip the inverter bit according to val.

Equations

• f.flip val = { val := Std.Sat.AIG.Fanin.val✝ f ^^^ val.toNat }

@[simp]

theorem Std.Sat.AIG.Fanin.gate_mk {g : Nat} {i : Bool} : (mk g i).gate = g

@[simp]

theorem Std.Sat.AIG.Fanin.invert_mk {g : Nat} {i : Bool} : (mk g i).invert = i

@[simp]

theorem Std.Sat.AIG.Fanin.gate_flip {v : Bool} (f : Fanin) : (f.flip v).gate = f.gate

@[simp]

theorem Std.Sat.AIG.Fanin.invert_flip {v : Bool} (f : Fanin) : (decide ((f.flip v).invert = f.invert) ^^ v) = true

inductive Std.Sat.AIG.Decl (α : Type) : Type

A circuit node. These are not recursive but instead contain indices into an AIG, with inputs indexed by α.

• false {α : Type} : Decl α

  A node with the constant value false. The constant true can be represented with a Ref to false with invert set true

• atom {α : Type} (idx : α) : Decl α

  An input node to the circuit.

• gate {α : Type} (l r : Fanin) : Decl α

  An AIG gate with configurable input nodes and polarity. l and r are the input nodes together with their inverter bit.

instance Std.Sat.AIG.instHashableDecl {α✝ : Type} [Hashable α✝] : Hashable (Decl α✝)

Equations

• Std.Sat.AIG.instHashableDecl = { hash := Std.Sat.AIG.hashDecl✝ }

instance Std.Sat.AIG.instReprDecl {α✝ : Type} [Repr α✝] : Repr (Decl α✝)

Equations

• Std.Sat.AIG.instReprDecl = { reprPrec := Std.Sat.AIG.reprDecl✝ }

instance Std.Sat.AIG.instDecidableEqDecl {α✝ : Type} [DecidableEq α✝] : DecidableEq (Decl α✝)

Equations

• Std.Sat.AIG.instDecidableEqDecl = Std.Sat.AIG.decEqDecl✝

instance Std.Sat.AIG.instInhabitedDecl {a✝ : Type} : Inhabited (Decl a✝)

Equations

• Std.Sat.AIG.instInhabitedDecl = { default := Std.Sat.AIG.Decl.false }

inductive Std.Sat.AIG.Cache.WF {α : Type} [Hashable α] [DecidableEq α] : Array (Decl α) → HashMap (Decl α) Nat → Prop

Cache.WF xs is a predicate asserting that a cache : HashMap (Decl α) Nat is a valid lookup cache for xs : Array (Decl α), that is, whenever cache.find? decl returns an index into xs : Array Decl, xs[index] = decl. Note that this predicate does not force the cache to be complete, if there is no entry in the cache for some node, it can still exist in the AIG.

• empty {α : Type} [Hashable α] [DecidableEq α] {decls : Array (Decl α)} : WF decls ∅

  An empty Cache is valid for any Array Decl as it never has a hit.

• push_id {α : Type} [Hashable α] [DecidableEq α] {decls : Array (Decl α)} {cache : HashMap (Decl α) Nat} {decl : Decl α} (h : WF decls cache) : WF (decls.push decl) cache

  Given a cache, valid with respect to some decls, we can extend the decls without extending the cache and remain valid.

• push_cache {α : Type} [Hashable α] [DecidableEq α] {decls : Array (Decl α)} {cache : HashMap (Decl α) Nat} {decl : Decl α} (h : WF decls cache) : WF (decls.push decl) (cache.insert decl decls.size)

  Given a cache, valid with respect to some decls, we can extend the decls and the cache at the same time with the same values and remain valid.

def Std.Sat.AIG.Cache (α : Type) [DecidableEq α] [Hashable α] (decls : Array (Decl α)) : Type

A cache for reusing elements from decls if they are available.

Equations

• Std.Sat.AIG.Cache α decls = { map : Std.HashMap (Std.Sat.AIG.Decl α) Nat // Std.Sat.AIG.Cache.WF decls map }

@[irreducible, inline]

def Std.Sat.AIG.Cache.empty {α : Type} [Hashable α] [DecidableEq α] {decls : Array (Decl α)} : Cache α decls

Create an empty Cache, valid with respect to any Array Decl.

Equations

• Std.Sat.AIG.Cache.empty = ⟨∅, ⋯⟩

@[irreducible, inline]

def Std.Sat.AIG.Cache.noUpdate {α : Type} [Hashable α] [DecidableEq α] {decls : Array (Decl α)} {decl : Decl α} (cache : Cache α decls) : Cache α (decls.push decl)

Given a cache, valid with respect to some decls, we can extend the decls without extending the cache and remain valid.

Equations

• cache.noUpdate = ⟨cache.val, ⋯⟩

@[irreducible, inline]

def Std.Sat.AIG.Cache.insert {α : Type} [Hashable α] [DecidableEq α] (decls : Array (Decl α)) (cache : Cache α decls) (decl : Decl α) : Cache α (decls.push decl)

Given a cache, valid with respect to some decls, we can extend the decls and the cache at the same time with the same values and remain valid.

Equations

• Std.Sat.AIG.Cache.insert decls cache decl = ⟨cache.val.insert decl decls.size, ⋯⟩

structure Std.Sat.AIG.CacheHit {α : Type} (decls : Array (Decl α)) (decl : Decl α) : Type

Contains the index of decl in decls along with a proof that the index is indeed correct.

• idx : Nat
• hbound : self.idx < decls.size
• hvalid : decls[self.idx] = decl

theorem Std.Sat.AIG.Cache.get?_bounds {α : Type} [Hashable α] [DecidableEq α] {decls : Array (Decl α)} {idx : Nat} (c : Cache α decls) (decl : Decl α) (hfound : c.val[decl]? = some idx) : idx < decls.size

For a c : Cache α decls, any index idx that is a cache hit for some decl is within bounds of decls (i.e. idx < decls.size).

theorem Std.Sat.AIG.Cache.get?_property {α : Type} [Hashable α] [DecidableEq α] {decls : Array (Decl α)} {idx : Nat} (c : Cache α decls) (decl : Decl α) (hfound : c.val[decl]? = some idx) : decls[idx] = decl

If Cache.get? decl returns some i then decls[i] = decl holds.

@[irreducible, inline]

def Std.Sat.AIG.Cache.get? {α : Type} [Hashable α] [DecidableEq α] {decls : Array (Decl α)} (cache : Cache α decls) (decl : Decl α) : Option (CacheHit decls decl)

Lookup a Decl in a Cache.

Equations

• cache.get? decl = match hfound : cache.val[decl]? with | some hit => some { idx := hit, hbound := ⋯, hvalid := ⋯ } | none => none

def Std.Sat.AIG.IsDAG (α : Type) (decls : Array (Decl α)) : Prop

An Array Decl is a Direct Acyclic Graph (DAG) if a gate at index i only points to nodes with index lower than i.

Equations

• Std.Sat.AIG.IsDAG α decls = ∀ {i : Nat} {lhs rhs : Std.Sat.AIG.Fanin} (h : i < decls.size), decls[i] = Std.Sat.AIG.Decl.gate lhs rhs → lhs.gate < i ∧ rhs.gate < i

theorem Std.Sat.AIG.IsDAG.empty {α : Type} : IsDAG α #[Decl.false]

The empty AIG is a DAG.

structure Std.Sat.AIG (α : Type) [DecidableEq α] [Hashable α] : Type

An And Inverter Graph together with a cache for subterm sharing.

• decls : Array (Decl α)

  The circuit itself as an Array Decl whose members have indices into said array.

• cache : Cache α self.decls

  The Decl cache, valid with respect to decls.

• hdag : IsDAG α self.decls

  In order to be a valid AIG, decls must form a DAG.

• hzero : 0 < self.decls.size

  The decls Array can never be empty, see hconst.

• hconst : self.decls[0] = Decl.false

  We always store .false at the first position. This allows us to avoid cache lookups

def Std.Sat.AIG.empty {α : Type} [Hashable α] [DecidableEq α] : AIG α

An AIG with an empty AIG and cache.

Equations

• Std.Sat.AIG.empty = { decls := #[Std.Sat.AIG.Decl.false], cache := Std.Sat.AIG.Cache.empty, hdag := ⋯, hzero := ⋯, hconst := ⋯ }

def Std.Sat.AIG.Mem {α : Type} [Hashable α] [DecidableEq α] (aig : AIG α) (a : α) : Prop

The atom a occurs in aig.

Equations

• aig.Mem a = (Std.Sat.AIG.Decl.atom a ∈ aig.decls)

instance Std.Sat.AIG.instMembership {α : Type} [Hashable α] [DecidableEq α] : Membership α (AIG α)

Equations

• Std.Sat.AIG.instMembership = { mem := Std.Sat.AIG.Mem }

structure Std.Sat.AIG.Ref {α : Type} [Hashable α] [DecidableEq α] (aig : AIG α) : Type

A reference to a node within an AIG.

• gate : Nat
• invert : Bool
• hgate : self.gate < aig.decls.size

@[inline]

def Std.Sat.AIG.Ref.cast {α : Type} [Hashable α] [DecidableEq α] {aig1 aig2 : AIG α} (ref : aig1.Ref) (h : aig1.decls.size ≤ aig2.decls.size) : aig2.Ref

A Ref into aig1 is also valid for aig2 if aig1 is smaller than aig2.

Equations

• ref.cast h = { gate := ref.gate, invert := ref.invert, hgate := ⋯ }

@[inline]

def Std.Sat.AIG.Ref.flip {α : Type} [Hashable α] [DecidableEq α] {aig : AIG α} (ref : aig.Ref) (inv : Bool) : aig.Ref

Flip the polarity of Ref if inv is set.

Equations

• ref.flip inv = { gate := ref.gate, invert := inv ^^ ref.invert, hgate := ⋯ }

@[inline]

def Std.Sat.AIG.Ref.not {α : Type} [Hashable α] [DecidableEq α] {aig : AIG α} (ref : aig.Ref) : aig.Ref

Flip the polarity of Ref.

Equations

• ref.not = ref.flip true

structure Std.Sat.AIG.BinaryInput {α : Type} [Hashable α] [DecidableEq α] (aig : AIG α) : Type

A pair of Refs, useful for LawfulOperators that act on two Refs at a time.

• lhs : aig.Ref
• rhs : aig.Ref

@[inline]

def Std.Sat.AIG.BinaryInput.cast {α : Type} [Hashable α] [DecidableEq α] {aig1 aig2 : AIG α} (input : aig1.BinaryInput) (h : aig1.decls.size ≤ aig2.decls.size) : aig2.BinaryInput

The Ref.cast equivalent for BinaryInput.

Equations

• input.cast h = { lhs := input.lhs.cast h, rhs := input.rhs.cast h }

@[inline]

def Std.Sat.AIG.BinaryInput.invert {α : Type} [Hashable α] [DecidableEq α] {aig : AIG α} (input : aig.BinaryInput) (linv rinv : Bool) : aig.BinaryInput

Flip the current inverter settings of the BinaryInput if linv or rinv is set respectively.

Equations

• input.invert linv rinv = { lhs := input.lhs.flip linv, rhs := input.rhs.flip rinv }

structure Std.Sat.AIG.TernaryInput {α : Type} [Hashable α] [DecidableEq α] (aig : AIG α) : Type

A collection of 3 of Refs, useful for LawfulOperators that act on three Refs at a time, in particular multiplexer style functions.

• discr : aig.Ref
• lhs : aig.Ref
• rhs : aig.Ref

@[inline]

def Std.Sat.AIG.TernaryInput.cast {α : Type} [Hashable α] [DecidableEq α] {aig1 aig2 : AIG α} (input : aig1.TernaryInput) (h : aig1.decls.size ≤ aig2.decls.size) : aig2.TernaryInput

The Ref.cast equivalent for TernaryInput.

Equations

• input.cast h = { discr := input.discr.cast h, lhs := input.lhs.cast h, rhs := input.rhs.cast h }

structure Std.Sat.AIG.Entrypoint (α : Type) [DecidableEq α] [Hashable α] : Type

An entrypoint into an AIG. This can be used to evaluate a circuit, starting at a certain node, with AIG.denote or to construct bigger circuits on top of this specific node.

• aig : AIG α

  The AIG that we are in.

• ref : self.aig.Ref

  The reference to the node in aig that this Entrypoint targets.

def Std.Sat.AIG.toGraphviz {α : Type} [DecidableEq α] [ToString α] [Hashable α] (entry : Entrypoint α) : String

Transform an Entrypoint into a graphviz string. Useful for debugging purposes.

Equations

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

@[irreducible]

def Std.Sat.AIG.toGraphviz.go {α : Type} [DecidableEq α] [ToString α] [Hashable α] (acc : String) (decls : Array (Decl α)) (hinv : IsDAG α decls) (idx : Nat) (hidx : idx < decls.size) : StateM (HashSet (Fin decls.size)) String

Equations

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

def Std.Sat.AIG.toGraphviz.invEdgeStyle (isInv : Bool) : String

Equations

• Std.Sat.AIG.toGraphviz.invEdgeStyle isInv = if isInv = true then " [color=red]" else " [color=blue]"

def Std.Sat.AIG.toGraphviz.toGraphvizString {α : Type} [DecidableEq α] [ToString α] [Hashable α] (decls : Array (Decl α)) (idx : Fin decls.size) : String

Equations

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

structure Std.Sat.AIG.RefVec {α : Type} [Hashable α] [DecidableEq α] (aig : AIG α) (w : Nat) : Type

A vector of references into aig. This is the AIG analog of BitVec.

• refs : Vector Fanin w
• hrefs {i : Nat} (h : i < w) : self.refs[i].gate < aig.decls.size

structure Std.Sat.AIG.RefVecEntry (α : Type) [DecidableEq α] [Hashable α] [DecidableEq α] (w : Nat) : Type

A sequence of references bundled with their AIG.

• aig : AIG α
• vec : self.aig.RefVec w

structure Std.Sat.AIG.ShiftTarget {α : Type} [Hashable α] [DecidableEq α] (aig : AIG α) (w : Nat) : Type

A RefVec bundled with constant distance to be shifted by.

• vec : aig.RefVec w
• distance : Nat

structure Std.Sat.AIG.ArbitraryShiftTarget {α : Type} [Hashable α] [DecidableEq α] (aig : AIG α) (m : Nat) : Type

A RefVec bundled with a RefVec as distance to be shifted by.

• n : Nat
• target : aig.RefVec m
• distance : aig.RefVec self.n

structure Std.Sat.AIG.ExtendTarget {α : Type} [Hashable α] [DecidableEq α] (aig : AIG α) (newWidth : Nat) : Type

A RefVec to be extended to newWidth.

• w : Nat
• vec : aig.RefVec self.w

def Std.Sat.AIG.denote {α : Type} [Hashable α] [DecidableEq α] (assign : α → Bool) (entry : Entrypoint α) : Bool

Evaluate an AIG.Entrypoint using some assignment for atoms.

Equations

• ⟦assign, entry⟧ = (Std.Sat.AIG.denote.go entry.ref.gate entry.aig.decls assign ⋯ ⋯ ^^ entry.ref.invert)

@[irreducible]

def Std.Sat.AIG.denote.go {α : Type} (x : Nat) (decls : Array (Decl α)) (assign : α → Bool) (h1 : x < decls.size) (h2 : IsDAG α decls) : Bool

Equations

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

def Std.Sat.AIG.«term⟦_,_⟧» : Lean.ParserDescr

Denotation of an AIG at a specific Entrypoint.

Equations

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

def Std.Sat.AIG.«term⟦_,_,_⟧» : Lean.ParserDescr

Denotation of an AIG at a specific Entrypoint with the Entrypoint being constructed on the fly.

Equations

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

def Std.Sat.AIG.unexpandDenote : Lean.PrettyPrinter.Unexpander

Equations

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

def Std.Sat.AIG.UnsatAt {α : Type} [Hashable α] [DecidableEq α] (aig : AIG α) (start : Nat) (invert : Bool) (h : start < aig.decls.size) : Prop

The denotation of the sub-DAG in the aig at node start is false for all assignments.

Equations

• aig.UnsatAt start invert h = ∀ (assign : α → Bool), ⟦assign, { aig := aig, ref := { gate := start, invert := invert, hgate := h } }⟧ = false

def Std.Sat.AIG.Entrypoint.Unsat {α : Type} [Hashable α] [DecidableEq α] (entry : Entrypoint α) : Prop

The denotation of the Entrypoint is false for all assignments.

Equations

• entry.Unsat = entry.aig.UnsatAt entry.ref.gate entry.ref.invert ⋯

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

Add a new and inverter gate to the AIG in aig. Note that this version is only meant for proving, for production purposes use AIG.mkGateCached and equality theorems to this one.

Equations

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

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

Add a new input node to the AIG in aig. Note that this version is only meant for proving, for production purposes use AIG.mkAtomCached and equality theorems to this one.

Equations

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

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

Add a new constant node to aig. Note that this version is only meant for proving, for production purposes use AIG.mkConstCached and equality theorems to this one.

Equations

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

def Std.Sat.AIG.isConstant {α : Type} [Hashable α] [DecidableEq α] (aig : AIG α) (ref : aig.Ref) (b : Bool) : Bool

Determine whether ref is a Decl.const with value b.

Equations

• aig.isConstant { gate := gate, invert := invert, hgate := hgate } b = match aig.decls[gate] with | Std.Sat.AIG.Decl.false => decide (invert = b) | x => false

def Std.Sat.AIG.getConstant {α : Type} [Hashable α] [DecidableEq α] (aig : AIG α) (ref : aig.Ref) : Option Bool

Get the value of ref if it is constant.

Equations

• aig.getConstant { gate := gate, invert := invert, hgate := hgate } = match aig.decls[gate] with | Std.Sat.AIG.Decl.false => some invert | x => none