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

Equations

• Std.Sat.AIG.instHashableFanin.hash { val := a } = mixHash 0 (hash a)

@[instance_reducible]

instance Std.Sat.AIG.instHashableFanin : Hashable Fanin

Equations

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

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

Equations

• Std.Sat.AIG.instReprFanin.repr x✝ prec✝ = Std.Format.bracket "{ " (Std.Format.nil ++ Std.Format.text "val" ++ Std.Format.text " := " ++ (Std.Format.nest 7 (repr x✝.val)).group) " }"

@[instance_reducible]

instance Std.Sat.AIG.instReprFanin : Repr Fanin

Equations

• Std.Sat.AIG.instReprFanin = { reprPrec := Std.Sat.AIG.instReprFanin.repr }

@[instance_reducible]

instance Std.Sat.AIG.instDecidableEqFanin : DecidableEq Fanin

Equations

• Std.Sat.AIG.instDecidableEqFanin = Std.Sat.AIG.instDecidableEqFanin.decEq

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

Equations

• Std.Sat.AIG.instDecidableEqFanin.decEq { val := a } { val := b } = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Std.Sat.AIG.instInhabitedFanin : Inhabited Fanin

Equations

• Std.Sat.AIG.instInhabitedFanin = { default := Std.Sat.AIG.instInhabitedFanin.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 = f.val / 2

@[inline]

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

Get the inverter bit.

Equations

• f.invert = (1 &&& f.val != 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 := f.val ^^^ 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) : (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

Equations

• Std.Sat.AIG.instHashableDecl.hash Std.Sat.AIG.Decl.false = 0
• Std.Sat.AIG.instHashableDecl.hash (Std.Sat.AIG.Decl.atom a) = mixHash 1 (hash a)
• Std.Sat.AIG.instHashableDecl.hash (Std.Sat.AIG.Decl.gate a a_1) = mixHash (mixHash 2 (hash a)) (hash a_1)

@[instance_reducible]

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

Equations

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

@[instance_reducible]

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

Equations

• Std.Sat.AIG.instReprDecl = { reprPrec := Std.Sat.AIG.instReprDecl.repr }

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

Equations

• One or more equations did not get rendered due to their size.
• Std.Sat.AIG.instReprDecl.repr Std.Sat.AIG.Decl.false prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Std.Sat.AIG.Decl.false")).group prec✝

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

Equations

• Std.Sat.AIG.instDecidableEqDecl.decEq Std.Sat.AIG.Decl.false Std.Sat.AIG.Decl.false = isTrue ⋯
• Std.Sat.AIG.instDecidableEqDecl.decEq Std.Sat.AIG.Decl.false (Std.Sat.AIG.Decl.atom idx) = isFalse ⋯
• Std.Sat.AIG.instDecidableEqDecl.decEq Std.Sat.AIG.Decl.false (Std.Sat.AIG.Decl.gate l r) = isFalse ⋯
• Std.Sat.AIG.instDecidableEqDecl.decEq (Std.Sat.AIG.Decl.atom idx) Std.Sat.AIG.Decl.false = isFalse ⋯
• Std.Sat.AIG.instDecidableEqDecl.decEq (Std.Sat.AIG.Decl.atom a) (Std.Sat.AIG.Decl.atom b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Std.Sat.AIG.instDecidableEqDecl.decEq (Std.Sat.AIG.Decl.atom idx) (Std.Sat.AIG.Decl.gate l r) = isFalse ⋯
• Std.Sat.AIG.instDecidableEqDecl.decEq (Std.Sat.AIG.Decl.gate l r) Std.Sat.AIG.Decl.false = isFalse ⋯
• Std.Sat.AIG.instDecidableEqDecl.decEq (Std.Sat.AIG.Decl.gate l r) (Std.Sat.AIG.Decl.atom idx) = isFalse ⋯
• Std.Sat.AIG.instDecidableEqDecl.decEq (Std.Sat.AIG.Decl.gate a a_1) (Std.Sat.AIG.Decl.gate b b_1) = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

@[instance_reducible]

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

Equations

• Std.Sat.AIG.instDecidableEqDecl = Std.Sat.AIG.instDecidableEqDecl.decEq

@[instance_reducible]

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

Equations

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

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.

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 α)} (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.

Equations

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

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

Equations

• Std.Sat.AIG.Cache.insert decls cache decl hmiss = ⟨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.

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

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.

Equations

• Std.Sat.AIG.Cache.ofAtoms decls huniq = Std.Sat.AIG.Cache.ofAtoms.go decls huniq 0 ∅ ⋯ ⋯

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

Equations

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

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

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.

Equations

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

@[instance_reducible]

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

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

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