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.

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 α.

• const: {α : Type} → Bool → Std.Sat.AIG.Decl α

  A node with a constant output value.

• atom: {α : Type} → α → Std.Sat.AIG.Decl α

  An input node to the circuit.

• gate: {α : Type} → Nat → Nat → Bool → Bool → Std.Sat.AIG.Decl α

  An AIG gate with configurable input nodes and polarity. l and r are the input node indices while linv and rinv say whether there is an inverter on the left and right inputs, respectively.

Instances For

• Std.Sat.AIG.instHashableDecl
• Std.Sat.AIG.instInhabitedDecl
• Std.Sat.AIG.instReprDecl

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

inductive Std.Sat.AIG.Cache.WF {α : Type} [Hashable α] [DecidableEq α] : Array (Std.Sat.AIG.Decl α) → Std.HashMap (Std.Sat.AIG.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} [inst : Hashable α] [inst_1 : DecidableEq α] {decls : Array (Std.Sat.AIG.Decl α)}, Std.Sat.AIG.Cache.WF decls ∅

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

• push_id: ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {decls : Array (Std.Sat.AIG.Decl α)} {cache : Std.HashMap (Std.Sat.AIG.Decl α) Nat} {decl : Std.Sat.AIG.Decl α}, Std.Sat.AIG.Cache.WF decls cache → Std.Sat.AIG.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} [inst : Hashable α] [inst_1 : DecidableEq α] {decls : Array (Std.Sat.AIG.Decl α)} {cache : Std.HashMap (Std.Sat.AIG.Decl α) Nat} {decl : Std.Sat.AIG.Decl α}, Std.Sat.AIG.Cache.WF decls cache → Std.Sat.AIG.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 (Std.Sat.AIG.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]

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

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

Equations

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

@[irreducible]

def Std.Sat.AIG.Cache.noUpdate {α : Type} [Hashable α] [DecidableEq α] {decls : Array (Std.Sat.AIG.Decl α)} {decl : Std.Sat.AIG.Decl α} (cache : Std.Sat.AIG.Cache α decls) : Std.Sat.AIG.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]

def Std.Sat.AIG.Cache.insert {α : Type} [Hashable α] [DecidableEq α] (decls : Array (Std.Sat.AIG.Decl α)) (cache : Std.Sat.AIG.Cache α decls) (decl : Std.Sat.AIG.Decl α) : Std.Sat.AIG.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 (Std.Sat.AIG.Decl α)) (decl : Std.Sat.AIG.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.CacheHit.hbound {α : Type} {decls : Array (Std.Sat.AIG.Decl α)} {decl : Std.Sat.AIG.Decl α} (self : Std.Sat.AIG.CacheHit decls decl) : self.idx < decls.size

theorem Std.Sat.AIG.CacheHit.hvalid {α : Type} {decls : Array (Std.Sat.AIG.Decl α)} {decl : Std.Sat.AIG.Decl α} (self : Std.Sat.AIG.CacheHit decls decl) : decls[self.idx] = decl

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

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

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

Lookup a Decl in a Cache.

def Std.Sat.AIG.IsDAG (α : Type) (decls : Array (Std.Sat.AIG.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 lhs rhs : Nat} {linv rinv : Bool} (h : i < decls.size), decls[i] = Std.Sat.AIG.Decl.gate lhs rhs linv rinv → lhs < i ∧ rhs < i

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

The empty array is a DAG.

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

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

• decls : Array (Std.Sat.AIG.Decl α)

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

• cache : Std.Sat.AIG.Cache α self.decls

  The Decl cache, valid with respect to decls.

• invariant : Std.Sat.AIG.IsDAG α self.decls

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

Instances For

• Std.Sat.AIG.instMembership

theorem Std.Sat.AIG.invariant {α : Type} [DecidableEq α] [Hashable α] (self : Std.Sat.AIG α) : Std.Sat.AIG.IsDAG α self.decls

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

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

An AIG with an empty AIG and cache.

Equations

• Std.Sat.AIG.empty = { decls := #[], cache := Std.Sat.AIG.Cache.empty #[], invariant := ⋯ }

def Std.Sat.AIG.Mem {α : Type} [Hashable α] [DecidableEq α] (aig : Std.Sat.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 α (Std.Sat.AIG α)

Equations

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

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

A reference to a node within an AIG. This is the AIG analog of Bool.

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

Instances For

• Std.Sat.AIG.instLawfulOperatorRefMkNotCached

theorem Std.Sat.AIG.Ref.hgate {α : Type} [Hashable α] [DecidableEq α] {aig : Std.Sat.AIG α} (self : aig.Ref) : self.gate < aig.decls.size

@[inline]

def Std.Sat.AIG.Ref.cast {α : Type} [Hashable α] [DecidableEq α] {aig1 : Std.Sat.AIG α} {aig2 : Std.Sat.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, hgate := ⋯ }

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

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

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

Instances For

• Std.Sat.AIG.instLawfulOperatorBinaryInputMkAndCached
• Std.Sat.AIG.instLawfulOperatorBinaryInputMkBEqCached
• Std.Sat.AIG.instLawfulOperatorBinaryInputMkImpCached
• Std.Sat.AIG.instLawfulOperatorBinaryInputMkOrCached
• Std.Sat.AIG.instLawfulOperatorBinaryInputMkXorCached

@[inline]

def Std.Sat.AIG.BinaryInput.cast {α : Type} [Hashable α] [DecidableEq α] {aig1 : Std.Sat.AIG α} {aig2 : Std.Sat.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 }

structure Std.Sat.AIG.TernaryInput {α : Type} [Hashable α] [DecidableEq α] (aig : Std.Sat.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

Instances For

• Std.Sat.AIG.instLawfulOperatorTernaryInputMkIfCached

@[inline]

def Std.Sat.AIG.TernaryInput.cast {α : Type} [Hashable α] [DecidableEq α] {aig1 : Std.Sat.AIG α} {aig2 : Std.Sat.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 : Std.Sat.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 : Std.Sat.AIG.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 (Std.Sat.AIG.Decl α)) (hinv : Std.Sat.AIG.IsDAG α decls) (idx : Nat) (hidx : idx < decls.size) : StateM (Std.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 (Std.Sat.AIG.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 : Std.Sat.AIG α) (w : Nat) : Type

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

• refs : Array Nat
• hlen : self.refs.size = w
• hrefs : ∀ {i : Nat} (h : i < w), self.refs[i] < aig.decls.size

Instances For

• Std.Tactic.BVDecide.BVExpr.bitblast.instLawfulVecOperatorRefVecBlastNot

theorem Std.Sat.AIG.RefVec.hlen {α : Type} [Hashable α] [DecidableEq α] {aig : Std.Sat.AIG α} {w : Nat} (self : aig.RefVec w) : self.refs.size = w

theorem Std.Sat.AIG.RefVec.hrefs {α : Type} [Hashable α] [DecidableEq α] {aig : Std.Sat.AIG α} {w : Nat} (self : aig.RefVec w) {i : Nat} (h : i < w) : self.refs[i] < aig.decls.size

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

A sequence of references bundled with their AIG.

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

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

A RefVec bundled with constant distance to be shifted by.

• vec : aig.RefVec w
• distance : Nat

Instances For

• Std.Tactic.BVDecide.BVExpr.bitblast.instLawfulVecOperatorShiftTargetBlastArithShiftRightConst
• Std.Tactic.BVDecide.BVExpr.bitblast.instLawfulVecOperatorShiftTargetBlastRotateLeft
• Std.Tactic.BVDecide.BVExpr.bitblast.instLawfulVecOperatorShiftTargetBlastRotateRight
• Std.Tactic.BVDecide.BVExpr.bitblast.instLawfulVecOperatorShiftTargetBlastShiftLeftConst
• Std.Tactic.BVDecide.BVExpr.bitblast.instLawfulVecOperatorShiftTargetBlastShiftRightConst

structure Std.Sat.AIG.ArbitraryShiftTarget {α : Type} [Hashable α] [DecidableEq α] (aig : Std.Sat.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

Instances For

• Std.Tactic.BVDecide.BVExpr.bitblast.instLawfulVecOperatorArbitraryShiftTargetBlastShiftLeft
• Std.Tactic.BVDecide.BVExpr.bitblast.instLawfulVecOperatorArbitraryShiftTargetBlastShiftRight

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

A RefVec to be extended to newWidth.

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

Instances For

• Std.Tactic.BVDecide.BVExpr.bitblast.instLawfulVecOperatorExtendTargetBlastSignExtend
• Std.Tactic.BVDecide.BVExpr.bitblast.instLawfulVecOperatorExtendTargetBlastZeroExtend

def Std.Sat.AIG.denote {α : Type} [Hashable α] [DecidableEq α] (assign : α → Bool) (entry : Std.Sat.AIG.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 ⋯ ⋯

@[irreducible]

def Std.Sat.AIG.denote.go {α : Type} (x : Nat) (decls : Array (Std.Sat.AIG.Decl α)) (assign : α → Bool) (h1 : x < decls.size) (h2 : Std.Sat.AIG.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 : Std.Sat.AIG α) (start : Nat) (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 h = ∀ (assign : α → Bool), ⟦assign, { aig := aig, ref := { gate := start, hgate := h } }⟧ = false

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

The denotation of the Entrypoint is false for all assignments.

Equations

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

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

An input to an AIG gate.

• ref : aig.Ref

  The node we are referring to.

• inv : Bool

  Whether the node is inverted

@[inline]

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

The Ref.cast equivalent for Fanin.

Equations

• fanin.cast h = { ref := fanin.ref.cast h, inv := fanin.inv }

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

The input type for creating AIG and gates.

• lhs : aig.Fanin
• rhs : aig.Fanin

Instances For

• Std.Sat.AIG.instLawfulOperatorGateInputMkGate
• Std.Sat.AIG.instLawfulOperatorGateInputMkGateCached

@[inline]

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

The Ref.cast equivalent for GateInput.

Equations

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

def Std.Sat.AIG.mkGate {α : Type} [Hashable α] [DecidableEq α] (aig : Std.Sat.AIG α) (input : aig.GateInput) : Std.Sat.AIG.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.

Instances For

• Std.Sat.AIG.instLawfulOperatorGateInputMkGate

def Std.Sat.AIG.mkAtom {α : Type} [Hashable α] [DecidableEq α] (aig : Std.Sat.AIG α) (n : α) : Std.Sat.AIG.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

• aig.mkAtom n = { aig := { decls := aig.decls.push (Std.Sat.AIG.Decl.atom n), cache := aig.cache.noUpdate, invariant := ⋯ }, ref := { gate := aig.decls.size, hgate := ⋯ } }

Instances For

• Std.Sat.AIG.instLawfulOperatorMkAtom

def Std.Sat.AIG.mkConst {α : Type} [Hashable α] [DecidableEq α] (aig : Std.Sat.AIG α) (val : Bool) : Std.Sat.AIG.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

• aig.mkConst val = { aig := { decls := aig.decls.push (Std.Sat.AIG.Decl.const val), cache := aig.cache.noUpdate, invariant := ⋯ }, ref := { gate := aig.decls.size, hgate := ⋯ } }

Instances For

• Std.Sat.AIG.instLawfulOperatorBoolMkConst