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 (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 (nvars) of n.

@[simp]

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

Lifting a BDD B to its current input size (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 ⋯

lift does not affect 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

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 greater or equal to 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 ⋯)

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

theorem BDD.denotation_eq_of_denotation_eq {n m : ℕ} {B C : BDD} (hn : max B.nvars C.nvars ≤ n) (hm : max B.nvars C.nvars ≤ m) : B.denotation ⋯ = C.denotation ⋯ → B.denotation ⋯ = C.denotation ⋯

If two BDD have the same denotation with respect to some input size n, then they have the same denotation with respect to any other input size m as well.

theorem BDD.SemanticEquiv.equivalence : Equivalence SemanticEquiv

SemanticEquiv is an equivalence relation on BDD.

instance BDD.instDecidableSemanticEquiv : DecidableRel SemanticEquiv

SemanticEquiv is Decidable.

Use this instance to decide whether two BDDs are equivalent.

Equations

• x✝¹.instDecidableSemanticEquiv x✝ = decidable_of_iff' (BDD.Similar✝ x✝¹ x✝) ⋯

def BDD.size : BDD → ℕ

Equations

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

def BDD.const (b : Bool) : BDD

Return a BDD denoting the constantly-b function.

See also const_denotation.

Equations

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

def BDD.var (n : ℕ) : BDD

Return a BDD denoting the nth projection function.

See also var_denotation.

Equations

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

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

Apply a binary Boolean operator to two BDDs.

See also apply_denotation.

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

Return a BDD denoting the conjuction of the denotations of two given BDDs.

See also and_denotation.

Equations

• BDD.and = BDD.apply and

def BDD.or : BDD → BDD → BDD

Return a BDD denoting the disjunction of the denotations of two given BDDs.

See also or_denotation.

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

Return a BDD denoting the negation of the denotation of a given BDD.

See also not_denotation.

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.apply_denotation' {B C : BDD} {op : Bool → Bool → Bool} (I : Vector Bool (apply op B C).nvars) : (apply op B C).denotation ⋯ I = op (B.denotation ⋯ I) (C.denotation ⋯ I)

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

Relabel the variables in a BDD according to a relabeling function f.

See also relabel_denotation.

Equations

• B.relabel f h = BDD.relabel''✝ B (BDD.relabel_wrap✝ 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

Return an input vector that satisfies the denotation of a given BDD, under the assumption that its denotation is satisfiable.

See also choice_denotation.

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)

Return some input vector that satisfies the denotation of a given BDD, or none if none exists.

See also choice, find_none and find_some.

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 : Bool) (i : ℕ) (B : BDD) : BDD

Return a BDD denoting the restriction of a given BDD at an index i to a Boolean b.

See also restrict_denotation.

Equations

• BDD.restrict b i B = if h : i < B.nvars then BDD.restrict'✝ B b ⟨i, h⟩ else B

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

@[simp]

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

@[simp]

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

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

Equations

• B.instDecidableDependsOn i = ⋯ ▸ decidable_of_iff ((↑(BDD.obdd✝ B)).usesVar i) ⋯

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

Universal quantification over input at index i.

See also bforall_denotation.

Equations

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

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

Universal quantification over a list of input indices l.

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

Existential quantification over input at index i.

See also bexists_denotation.

Equations

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

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

Existential quantification over a list of input indices l.

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