Documentation

Std.Sat.AIG.Basic

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

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

const {α : Type} (b : Bool) : Decl α
A node with a constant output value.
atom {α : Type} (idx : α) : Decl α
An input node to the circuit.
gate {α : Type} (l r : Nat) (linv rinv : Bool) : 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

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.const default }

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

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 decls = ⟨∅, ⋯⟩

@[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 α) :

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

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} :

The empty array is a DAG.

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

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.
invariant : IsDAG α self.decls
In order to be a valid AIG, decls must form a DAG.

Instances For

Std.Sat.AIG.instMembership

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

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 : AIG α) (a : α) :

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

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

@[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, hgate := ⋯ }

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

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

lhs : aig.Ref
rhs : aig.Ref

Instances For

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

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

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 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 α] :

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

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

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

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

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

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

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

A RefVec bundled with constant distance to be shifted by.

vec : aig.RefVec w
distance : Nat

Instances For

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

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

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

A RefVec to be extended to newWidth.

w : Nat
vec : aig.RefVec self.w

Instances For

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

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 (Decl α)) (assign : α → Bool) (h1 : x < decls.size) (h2 : IsDAG α decls) :

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) (h : start < aig.decls.size) :

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

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

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 aig2 : 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 : AIG α) :

The input type for creating AIG and gates.

lhs : aig.Fanin
rhs : aig.Fanin

Instances For

@[inline]

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

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 : AIG α) (input : aig.GateInput) :

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 : AIG α) (n : α) :

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 : AIG α) (val : Bool) :

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

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

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

Equations

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