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.

• ofRaw :: (
• val : Nat
• )

def Std.Sat.AIG.instHashableFanin.hash : Fanin → UInt64

@[instance_reducible]

instance Std.Sat.AIG.instHashableFanin : Hashable Fanin

def Std.Sat.AIG.instReprFanin.repr : Fanin → Nat → Format

@[instance_reducible]

instance Std.Sat.AIG.instReprFanin : Repr Fanin

@[instance_reducible]

instance Std.Sat.AIG.instDecidableEqFanin : DecidableEq Fanin

def Std.Sat.AIG.instDecidableEqFanin.decEq (x✝ x✝¹ : Fanin) : Decidable (x✝ = x✝¹)

@[instance_reducible]

instance Std.Sat.AIG.instInhabitedFanin : Inhabited Fanin

@[inline]

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

The public constructor of Fanin.

@[inline]

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

Get the gate.

@[inline]

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

Get the inverter bit.

@[inline]

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

Flip the inverter bit according to val.

@[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) : (f.flip v).invert = (f.invert ^^ v)

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.

def Std.Sat.AIG.instHashableDecl.hash {α✝ : Type} [Hashable α✝] : Decl α✝ → UInt64

@[instance_reducible]

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

@[instance_reducible]

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

def Std.Sat.AIG.instReprDecl.repr {α✝ : Type} [Repr α✝] : Decl α✝ → Nat → Format

def Std.Sat.AIG.instDecidableEqDecl.decEq {α✝ : Type} [DecidableEq α✝] (x✝ x✝¹ : Decl α✝) : Decidable (x✝ = x✝¹)

@[instance_reducible]

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

@[instance_reducible]

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

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

• sound (decl : Decl α) (idx : Nat) : cache[decl]? = some idx → ∃ (h : idx < decls.size), decls[idx] = decl

  Whenever cache[decl]? returns an index into decls, decls[index] = decl. Note that this does not force the cache to be complete for gates, if there is no entry in the cache for some gate, it can still exist in decls.

• atoms (i : Nat) (h : i < decls.size) (a : α) : decls[i] = Decl.atom a → cache[Decl.atom a]? = some i

  The cache knows about every atom in decls. This is crucial to enforce that all atoms occur at most once in the AIG.

theorem Std.Sat.AIG.Cache.WF.empty {α : Type} [Hashable α] [DecidableEq α] {decls : Array (Decl α)} (hatoms : ∀ (i : Nat) (h : i < decls.size) (a : α), decls[i] ≠ Decl.atom a) : WF decls ∅

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

theorem Std.Sat.AIG.Cache.WF.push_cache {α : Type} [Hashable α] [DecidableEq α] {decls : Array (Decl α)} {cache : HashMap (Decl α) Nat} {decl : Decl α} (h : WF decls cache) (hmiss : cache[decl]? = none) : 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 a decl that is not yet in the cache 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.

@[irreducible, inline]

def Std.Sat.AIG.Cache.empty {α : Type} [Hashable α] [DecidableEq α] {decls : Array (Decl α)} (hatoms : ∀ (i : Nat) (h : i < decls.size) (a : α), decls[i] ≠ Decl.atom a := by simp) : Cache α decls

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

@[irreducible, inline]

def Std.Sat.AIG.Cache.insert {α : Type} [Hashable α] [DecidableEq α] (decls : Array (Decl α)) (cache : Cache α decls) (decl : Decl α) (hmiss : cache.val[decl]? = none) : 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 a decl that is not yet in the cache and remain valid.

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.

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

theorem Std.Sat.AIG.Cache.get?_eq_none_iff {α : Type} [Hashable α] [DecidableEq α] {decls : Array (Decl α)} {cache : Cache α decls} {decl : Decl α} : cache.get? decl = none ↔ cache.val[decl]? = none

theorem Std.Sat.AIG.Cache.get?_eq_some_iff {α : Type} [Hashable α] [DecidableEq α] {decls : Array (Decl α)} {cache : Cache α decls} {decl : Decl α} {hit : CacheHit decls decl} : cache.get? decl = some hit ↔ cache.val[decl]? = some hit.idx

theorem Std.Sat.AIG.Cache.get?_atom {α : Type} [Hashable α] [DecidableEq α] {decls : Array (Decl α)} (cache : Cache α decls) {i : Nat} {hi : i < decls.size} {a : α} (h : decls[i] = Decl.atom a) : cache.get? (Decl.atom a) = some { idx := i, hbound := hi, hvalid := h }

theorem Std.Sat.AIG.Cache.ofAtoms.complete_succ {α : Type} [Hashable α] [DecidableEq α] {decls : Array (Decl α)} {map : HashMap (Decl α) Nat} {idx : Nat} (hcomp : ∀ (i : Nat) (h : i < decls.size), i < idx → ∀ (a : α), decls[i] = Decl.atom a → map[Decl.atom a]? = some i) (hnot : ∀ (h : idx < decls.size) (a : α), decls[idx] ≠ Decl.atom a) (i : Nat) (h : i < decls.size) : i < idx + 1 → ∀ (a : α), decls[i] = Decl.atom a → map[Decl.atom a]? = some i

def Std.Sat.AIG.Cache.ofAtoms {α : Type} [Hashable α] [DecidableEq α] (decls : Array (Decl α)) (huniq : ∀ (i j : Nat) (hi : i < decls.size) (hj : j < decls.size) (a : α), decls[i] = Decl.atom a → decls[j] = Decl.atom a → i = j) : Cache α decls

Build a cache for decls that contains exactly the atoms of decls. This requires that every atom occurs at most once in decls.

@[irreducible]

def Std.Sat.AIG.Cache.ofAtoms.go {α : Type} [Hashable α] [DecidableEq α] (decls : Array (Decl α)) (huniq : ∀ (i j : Nat) (hi : i < decls.size) (hj : j < decls.size) (a : α), decls[i] = Decl.atom a → decls[j] = Decl.atom a → i = j) (idx : Nat) (map : HashMap (Decl α) Nat) (hsound : ∀ (decl : Decl α) (i : Nat), map[decl]? = some i → ∃ (h : i < decls.size), decls[i] = decl) (hcomp : ∀ (i : Nat) (h : i < decls.size), i < idx → ∀ (a : α), decls[i] = Decl.atom a → map[Decl.atom a]? = some i) : Cache α decls

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.

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.

theorem Std.Sat.AIG.atom_unique {α : Type} [Hashable α] [DecidableEq α] (aig : AIG α) {i j : Nat} {hi : i < aig.decls.size} {hj : j < aig.decls.size} {a : α} (h1 : aig.decls[i] = Decl.atom a) (h2 : aig.decls[j] = Decl.atom a) : i = j

Every atom occurs at most once in an AIG.

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

The atom a occurs in aig.

@[instance_reducible]

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

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

@[implicit_reducible, 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.

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

@[inline]

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

Flip the polarity of Ref.

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.

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

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.

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.

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

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

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

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.

@[irreducible]

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

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

Denotation of an AIG at a specific Entrypoint.

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

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

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

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.

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

The denotation of the Entrypoint is false for all assignments.

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.

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

Get the value of ref if it is constant.