structure BDD : Type

Abstract BDD type.

• nvars : ℕ

  BDD input size (number of variables).

• nheap : ℕ
• obdd : OBdd self.nvars (BDD.nheap✝ self)
• hred : (BDD.obdd✝ self).Reduced

def BDD.lift {n : ℕ} (B : BDD) (h : B.nvars ≤ n) : BDD

Raise the input size (BDD.nvars) of a BDD to n, given a proof that the current input size is at most n.

Equations

• B.lift h = { nvars := n, nheap := BDD.nheap✝ B, obdd := Lift.olift h (BDD.obdd✝ B), hred := ⋯ }

@[simp]

theorem BDD.lift_nvars {n : ℕ} {B : BDD} {h : B.nvars ≤ n} : (B.lift h).nvars = n

Lifting a BDD to n yields a BDD with input size (BDD.nvars) of n.

@[simp]

theorem BDD.lift_refl {B : BDD} : B.lift ⋯ = B

Lifting a BDD B to its current input size (BDD.nvars) yields back B.

def BDD.denotation {n : ℕ} (B : BDD) (h : B.nvars ≤ n) : Vector Bool n → Bool

The denotation of a BDD is the Boolean function that it represents.

Equations

• B.denotation h = BDD.evaluate✝ (B.lift h)

@[simp]

theorem BDD.lift_denotation {n m : ℕ} {B : BDD} {h1 : B.nvars ≤ n} {h2 : n ≤ m} : (B.lift h1).denotation h2 = B.denotation ⋯

BDD.lift does not affect BDD.denotation.

@[simp]

theorem BDD.denotation_cast {n m : ℕ} {I : Vector Bool n} {B : BDD} {hn : B.nvars ≤ n} {hm : B.nvars ≤ m} (h : n = m) : B.denotation hm (Vector.cast h I) = B.denotation hn I

BDD.denotation absorbs Vector.cast.

theorem BDD.denotation_independentOf_of_geq_nvars {n : ℕ} {i : Fin n} {B : BDD} {h1 : B.nvars ≤ n} {h2 : B.nvars ≤ ↑i} : Nary.IndependentOf (B.denotation h1) i

The denotation of a BDD is independent of indices that exceed its input size.

def BDD.SemanticEquiv : BDD → BDD → Prop

BDDs are semantically equivalent when their denotations coincide.

Equations

• B.SemanticEquiv C = (B.denotation ⋯ = C.denotation ⋯)

instance BDD.instDecidableSemacticEquiv : DecidableRel SemanticEquiv

Equations

• x✝¹.instDecidableSemacticEquiv x✝ = decidable_of_iff' (BDD.SyntacticEquiv✝ x✝¹ x✝) ⋯

def BDD.size : BDD → ℕ

Equations

• x✝.size = Size.size (BDD.obdd✝ x✝)

def BDD.const : Bool → BDD

Equations

• BDD.const x✝ = { nvars := 0, nheap := 0, obdd := ⟨{ heap := Vector.emptyWithCapacity 0, root := Pointer.terminal x✝ }, ⋯⟩, hred := ⋯ }

def BDD.var : ℕ → BDD

Equations

• BDD.var x✝ = { nvars := x✝ + 1, nheap := 1, obdd := ⟨BDD.var_raw✝ x✝, ⋯⟩, hred := ⋯ }

def BDD.apply : (Bool → Bool → Bool) → BDD → BDD → BDD

Equations

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

@[simp]

theorem BDD.apply_nvars {B C : BDD} {o : Bool → Bool → Bool} : (apply o B C).nvars = max B.nvars C.nvars

def BDD.and : BDD → BDD → BDD

Equations

• BDD.and = BDD.apply and

def BDD.or : BDD → BDD → BDD

Equations

• BDD.or = BDD.apply or

def BDD.xor : BDD → BDD → BDD

Equations

• BDD.xor = BDD.apply xor

def BDD.imp : BDD → BDD → BDD

Equations

• BDD.imp = BDD.apply fun (x1 x2 : Bool) => !x1 || x2

def BDD.not : BDD → BDD

Equations

• B.not = B.imp (BDD.const false)

@[simp]

theorem BDD.const_nvars {b : Bool} : (const b).nvars = 0

@[simp]

theorem BDD.const_denotation {b : Bool} {a✝ : ℕ} {h : (const b).nvars ≤ a✝} : (const b).denotation h = Function.const (Vector Bool a✝) b

@[simp]

theorem BDD.var_nvars {i : ℕ} : (var i).nvars = i + 1

@[simp]

theorem BDD.var_denotation {i a✝ : ℕ} {h : (var i).nvars ≤ a✝} {I : Vector Bool a✝} : (var i).denotation h I = I[i]

@[reducible, inline]

abbrev BDD.denotation' (O : BDD) : Vector Bool O.nvars → Bool

Equations

• O.denotation' = O.denotation ⋯

theorem BDD.denotation_take {n m : ℕ} {I : Vector Bool n} {B : BDD} {hn : B.nvars ≤ n} {hm1 : B.nvars ≤ m} {hm2 : m ≤ n} : B.denotation hn I = B.denotation ⋯ (I.take m)

theorem BDD.denotation_take' {n : ℕ} {I : Vector Bool n} {B : BDD} {hn : B.nvars ≤ n} : B.denotation hn I = B.denotation ⋯ (Vector.cast ⋯ (I.take B.nvars))

@[simp]

theorem BDD.apply_denotation {n : ℕ} {B C : BDD} {op : Bool → Bool → Bool} {I : Vector Bool n} {h : (apply op B C).nvars ≤ n} : (apply op B C).denotation h I = op (B.denotation ⋯ I) (C.denotation ⋯ I)

@[simp]

theorem BDD.and_nvars {B C : BDD} : (B.and C).nvars = max B.nvars C.nvars

@[simp]

theorem BDD.and_denotation {n : ℕ} {B C : BDD} {I : Vector Bool n} {h : (B.and C).nvars ≤ n} : (B.and C).denotation h I = (B.denotation ⋯ I && C.denotation ⋯ I)

@[simp]

theorem BDD.or_nvars {B C : BDD} : (B.or C).nvars = max B.nvars C.nvars

@[simp]

theorem BDD.or_denotation {n : ℕ} {B C : BDD} {I : Vector Bool n} {h : (B.or C).nvars ≤ n} : (B.or C).denotation h I = (B.denotation ⋯ I || C.denotation ⋯ I)

@[simp]

theorem BDD.xor_nvars {B C : BDD} : (B.xor C).nvars = max B.nvars C.nvars

@[simp]

theorem BDD.xor_denotation {n : ℕ} {B C : BDD} {I : Vector Bool n} {h : (B.xor C).nvars ≤ n} : (B.xor C).denotation h I = (B.denotation ⋯ I ^^ C.denotation ⋯ I)

@[simp]

theorem BDD.imp_nvars {B C : BDD} : (B.imp C).nvars = max B.nvars C.nvars

@[simp]

theorem BDD.imp_denotation {n : ℕ} {B C : BDD} {I : Vector Bool n} {h : (B.imp C).nvars ≤ n} : (B.imp C).denotation h I = (!B.denotation ⋯ I || C.denotation ⋯ I)

@[simp]

theorem BDD.not_nvars {B : BDD} : B.not.nvars = B.nvars

@[simp]

theorem BDD.not_denotation {n : ℕ} {B : BDD} {I : Vector Bool n} {h : B.not.nvars ≤ n} : B.not.denotation h I = !B.denotation ⋯ I

def BDD.relabel {n : ℕ} (B : BDD) (f : Fin B.nvars → Fin n) (h : ∀ (i i' : Nary.Dependency B.denotation'), ↑i < ↑i' → f ↑i < f ↑i') : BDD

Equations

• B.relabel f h = BDD.relabel''✝ B (BDD.relabel_helper✝ B.nvars n f) ⋯ ⋯

@[simp]

theorem BDD.relabel_nvars {n : ℕ} {B : BDD} {f : Fin B.nvars → Fin n} {h : ∀ (i i' : Nary.Dependency B.denotation'), ↑i < ↑i' → f ↑i < f ↑i'} : (B.relabel f h).nvars = n

@[simp]

theorem BDD.relabel_denotation {n : ℕ} {B : BDD} {f : Fin B.nvars → Fin n} {hf : ∀ (i i' : Nary.Dependency B.denotation'), ↑i < ↑i' → f ↑i < f ↑i'} {I : Vector Bool n} {h : (B.relabel f hf).nvars ≤ n} : (B.relabel f hf).denotation h I = B.denotation' (Vector.ofFn fun (i : Fin B.nvars) => I[f i])

def BDD.choice {B : BDD} (s : ∃ (I : Vector Bool B.nvars), B.denotation' I = true) : Vector Bool B.nvars

Equations

• BDD.choice s = Choice.choice (BDD.obdd✝ B) ⋯

@[simp]

theorem BDD.choice_denotation {B : BDD} {s : ∃ (I : Vector Bool B.nvars), B.denotation' I = true} : B.denotation' (choice s) = true

def BDD.find {B : BDD} : Option (Vector Bool B.nvars)

Equations

• BDD.find = if h : B.SemanticEquiv (BDD.const false) then none else some (BDD.choice ⋯)

theorem BDD.find_none {B : BDD} : find.isNone = true → B.denotation' = Function.const (Vector Bool B.nvars) false

theorem BDD.find_some {B : BDD} {I : Vector Bool B.nvars} : find = some I → B.denotation' I = true

def BDD.restrict (B : BDD) (b : Bool) (i : ℕ) : BDD

Equations

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

theorem BDD.restrict_geq_eq_self {i : ℕ} {b : Bool} {B : BDD} : i ≥ B.nvars → B.restrict b i = B

@[simp]

theorem BDD.restrict_nvars {b : Bool} {B : BDD} {i : ℕ} : (B.restrict b i).nvars = B.nvars

@[simp]

theorem BDD.restrict_denotation {n : ℕ} {b : Bool} {B : BDD} {I : Vector Bool n} {i : ℕ} {hi : i < n} {h : (B.restrict b i).nvars ≤ n} : (B.restrict b i).denotation h I = Nary.restrict (B.denotation ⋯) b ⟨i, hi⟩ I

instance BDD.instDecidableDependsOn (B : BDD) : DecidablePred (Nary.DependsOn B.denotation')

Equations

• B.instDecidableDependsOn = ⋯.mpr inferInstance

def BDD.bforall (B : BDD) (i : ℕ) : BDD

Equations

• B.bforall i = (B.restrict false i).and (B.restrict true i)

def BDD.bforalls (B : BDD) (l : List ℕ) : BDD

Equations

• B.bforalls l = List.foldl BDD.bforall B l

@[simp]

theorem BDD.bforall_nvars {B : BDD} {i : ℕ} : (B.bforall i).nvars = B.nvars

@[simp]

theorem BDD.bforall_denotation {n : ℕ} {B : BDD} {i : ℕ} {hi : i < n} {I : Vector Bool n} {h : (B.bforall i).nvars ≤ n} : (B.bforall i).denotation h I = decide (∀ (b : Bool), B.denotation ⋯ (I.set i b hi) = true)

@[simp]

theorem BDD.bforall_idem {n : ℕ} {B : BDD} {i : ℕ} {hi : i < n} {I : Vector Bool n} {h : ((B.bforall i).bforall i).nvars ≤ n} : ((B.bforall i).bforall i).denotation h I = (B.bforall i).denotation ⋯ I

theorem BDD.bforall_comm {n : ℕ} {B : BDD} {i j : Fin B.nvars} {I : Vector Bool n} {h : ((B.bforall ↑i).bforall ↑j).nvars ≤ n} : ((B.bforall ↑i).bforall ↑j).denotation h I = ((B.bforall ↑j).bforall ↑i).denotation ⋯ I

def BDD.bexists (B : BDD) (i : ℕ) : BDD

Equations

• B.bexists i = (B.restrict false i).or (B.restrict true i)

def BDD.bexistss (B : BDD) (l : List ℕ) : BDD

Equations

• B.bexistss l = List.foldl BDD.bexists B l

@[simp]

theorem BDD.bexists_nvars {B : BDD} {i : ℕ} : (B.bexists i).nvars = B.nvars

@[simp]

theorem BDD.bexists_denotation {n : ℕ} {B : BDD} {i : ℕ} {hi : i < n} {I : Vector Bool n} {h : (B.bexists i).nvars ≤ n} : (B.bexists i).denotation h I = decide (∃ (b : Bool), B.denotation ⋯ (I.set i b hi) = true)

@[simp]

theorem BDD.bexists_idem {n : ℕ} {B : BDD} {i : ℕ} {hi : i < n} {I : Vector Bool n} {h : ((B.bexists i).bexists i).nvars ≤ n} : ((B.bexists i).bexists i).denotation h I = (B.bexists i).denotation ⋯ I

theorem BDD.bexists_comm {n : ℕ} {B : BDD} {i j : Fin B.nvars} {I : Vector Bool n} {h : ((B.bexists ↑i).bexists ↑j).nvars ≤ n} : ((B.bexists ↑i).bexists ↑j).denotation h I = ((B.bexists ↑j).bexists ↑i).denotation ⋯ I