structure BDD : Type

Abstract BDD type.

• nvars : ℕ

  BDD input size (number of variables).

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

def BDD.lift (B : BDD) {n : ℕ} (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 {B : BDD} {n : ℕ} {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.

@[implicit_reducible]

instance BDD.instGetElemVectorBoolLeNatNvars {n : ℕ} : GetElem BDD (Vector Bool n) Bool fun (B : BDD) (x : Vector Bool n) => B.nvars ≤ n

Evaluate the given BDD on the given variable assignment, assuming that the assignment interprets all variables of the BDD.

The get_elem_tactic_extensible has been extended to simplify all hypothesis using the lemmas marked with bdd_nvars, and hence the validity of the bounds can usually be inferred automatically.

Equations

• BDD.instGetElemVectorBoolLeNatNvars = { getElem := fun (B : BDD) (v : Vector Bool n) (h : B.nvars ≤ n) => Evaluate.evaluate (BDD.obdd✝ (B.lift h)) v }

def BDD.DependsOn (B : BDD) (i : ℕ) : Prop

A BDD B depends on a variable i if there are two variable assignemts I and I' such that I and I' only differ on the variable i and B[I] ≠ B[I'].

Equations

• B.DependsOn i = ∃ (h : i < B.nvars), Nary.DependsOn (Evaluate.evaluate (BDD.obdd✝ B)) ⟨i, h⟩

@[simp]

theorem BDD.not_dependsOn_of_ge {B : BDD} {i : ℕ} (h : i ≥ B.nvars) : ¬B.DependsOn i

A BDD does not depend on variables greater or equal to its input size.

@[simp]

theorem BDD.getElem_cast {m : ℕ} {B : BDD} {n : ℕ} {I : Vector Bool n} {hn : B.nvars ≤ n} (h : n = m) : B[Vector.cast h I] = B[I]

def BDD.SemanticEquiv (B C : BDD) : Prop

Two BDDs are semantically equivalent when they have the same evaluation on all variable assignemts.

Equations

• B.SemanticEquiv C = ∀ (I : Vector Bool (max B.nvars C.nvars)), B[I] = C[I]

theorem BDD.getElem_take {B : BDD} {n : ℕ} {I : Vector Bool n} {m : ℕ} {h1 : B.nvars ≤ m} {h2 : m ≤ n} : B[I.take m] = B[I]

theorem BDD.getElem_take' {B : BDD} {n : ℕ} {I : Vector Bool n} {hn : B.nvars ≤ n} : B[I.take B.nvars] = B[I]

theorem BDD.congrBDD {B C : BDD} {n m : ℕ} (hn : B.nvars ≤ n) (h : C.nvars ≤ n) (hm : max B.nvars C.nvars ≤ m) : (∀ (I : Vector Bool n), B[I] = C[I]) → ∀ (I : Vector Bool m), B[I] = C[I]

theorem BDD.congrInterpretation {n m : ℕ} {B : BDD} {I : Vector Bool n} {J : Vector Bool m} {hn : B.nvars ≤ n} {hm : B.nvars ≤ m} : (∀ (i : Fin B.nvars), B.DependsOn ↑i → I[i] = J[i]) → B[I] = B[J]

theorem BDD.congrInterpretation' {n m : ℕ} {B : BDD} {I : Vector Bool n} {J : Vector Bool m} {hn : B.nvars ≤ n} {hm : B.nvars ≤ m} : (∀ (i : Fin B.nvars), I[i] = J[i]) → B[I] = B[J]

theorem BDD.dependsOn_iff {B : BDD} {i : ℕ} (n : ℕ) (h : B.nvars ≤ n) : B.DependsOn i ↔ ∃ (v1 : Vector Bool n) (v2 : Vector Bool n), (∀ (i' : Fin n), i ≠ ↑i' → v1[i'] = v2[i']) ∧ B[v1] ≠ B[v2]

theorem BDD.dependsOn_getElem_ne_of_ne {n m : ℕ} {B : BDD} {I : Vector Bool n} {J : Vector Bool m} {hn : B.nvars ≤ n} {hm : B.nvars ≤ m} : B[I] ≠ B[J] → ∃ (i : Fin B.nvars), B.DependsOn ↑i ∧ I[i] ≠ J[i]

@[simp]

theorem BDD.getElem_lift {B : BDD} {n : ℕ} {h1 : B.nvars ≤ n} {m : ℕ} {I : Vector Bool m} {h2 : (B.lift h1).nvars ≤ m} : (B.lift h1)[I] = B[I]

theorem BDD.lift_dependsOn {B : BDD} {n : ℕ} {h1 : B.nvars ≤ n} {i : ℕ} : (B.lift h1).DependsOn i ↔ B.DependsOn i

theorem BDD.SemanticEquiv.equivalence : Equivalence SemanticEquiv

SemanticEquiv is an equivalence relation on BDD.

@[implicit_reducible]

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 → ℕ

Return the number of reachable nodes in given BDD.

Equations

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

def BDD.const (b : Bool) : BDD

Return the constant BDD for the boolean value b.

Equations

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

@[simp]

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

@[simp]

theorem BDD.getElem_const {n : ℕ} {b : Bool} (I : Vector Bool n) : (const b)[I] = b

@[simp]

theorem BDD.const_dependsOn {b : Bool} (i : ℕ) : ¬(const b).DependsOn i

def BDD.var (n : ℕ) : BDD

Return the BDD representing the nth projection function.

Equations

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

@[simp]

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

@[simp]

theorem BDD.getElem_var {i n : ℕ} (h1 : (var i).nvars ≤ n := by bdd_bounds) (h2 : i < n := by bdd_bounds) (I : Vector Bool n) : (var i)[I] = I[i]

@[simp]

theorem BDD.var_dependsOn {n i : ℕ} : (var n).DependsOn i ↔ i = n

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

Apply the given binary Boolean operator to the two BDDs.

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

@[simp]

theorem BDD.getElem_apply {n : ℕ} {B C : BDD} {op : Bool → Bool → Bool} {h1 : max B.nvars C.nvars ≤ n} (I : Vector Bool n) : (apply op B C)[I] = op B[I] C[I]

theorem BDD.apply_dependsOn {o : Bool → Bool → Bool} {C B : BDD} {i : ℕ} : (apply o B C).DependsOn i → B.DependsOn i ∨ C.DependsOn i

def BDD.and : BDD → BDD → BDD

Return the conjuction of the two given BDDs.

Equations

• BDD.and = BDD.apply and

@[simp]

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

@[simp]

theorem BDD.getElem_and {n : ℕ} {B C : BDD} {h : (B.and C).nvars ≤ n} (I : Vector Bool n) : (B.and C)[I] = (B[I] && C[I])

theorem BDD.and_dependsOn {B C : BDD} {i : ℕ} : (B.and C).DependsOn i → B.DependsOn i ∨ C.DependsOn i

def BDD.or : BDD → BDD → BDD

Return the disjunction of the two given BDDs.

Equations

• BDD.or = BDD.apply or

@[simp]

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

@[simp]

theorem BDD.getElem_or {B C : BDD} {n : ℕ} {h : (B.or C).nvars ≤ n} (I : Vector Bool n) : (B.or C)[I] = (B[I] || C[I])

theorem BDD.or_dependsOn {B C : BDD} {i : ℕ} : (B.or C).DependsOn i → B.DependsOn i ∨ C.DependsOn i

def BDD.xor : BDD → BDD → BDD

Return the exclusive disjunction of the two given BDDs.

Equations

• BDD.xor = BDD.apply xor

@[simp]

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

@[simp]

theorem BDD.getElem_xor {n : ℕ} {B C : BDD} {h : (B.xor C).nvars ≤ n} (I : Vector Bool n) : (B.xor C)[I] = (B[I] ^^ C[I])

theorem BDD.xor_dependsOn {B C : BDD} {i : ℕ} : (B.xor C).DependsOn i → B.DependsOn i ∨ C.DependsOn i

def BDD.imp : BDD → BDD → BDD

Compute the logical implication a → b of the two given BDDs.

Equations

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

@[simp]

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

@[simp]

theorem BDD.getElem_imp {n : ℕ} {B C : BDD} {h : (B.imp C).nvars ≤ n} (I : Vector Bool n) : (B.imp C)[I] = (!B[I] || C[I])

theorem BDD.imp_dependsOn {B C : BDD} {i : ℕ} : (B.imp C).DependsOn i → B.DependsOn i ∨ C.DependsOn i

def BDD.not : BDD → BDD

Return the negation of the given BDD.

Equations

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

@[simp]

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

@[simp]

theorem BDD.getElem_not {n : ℕ} {B : BDD} {h : B.not.nvars ≤ n} (I : Vector Bool n) : B.not[I] = !B[I]

@[simp]

theorem BDD.not_dependsOn {B : BDD} {i : ℕ} : B.not.DependsOn i ↔ B.DependsOn i

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

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

See also getElem_relabel.

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' : Fin B.nvars), B.DependsOn ↑i → B.DependsOn ↑i' → i < i' → f i < f i'} : (B.relabel f h).nvars = n

@[simp]

theorem BDD.getElem_relabel {B : BDD} {n : ℕ} {f : Fin B.nvars → Fin n} {hf : ∀ (i i' : Fin B.nvars), B.DependsOn ↑i → B.DependsOn ↑i' → i < i' → f i < f i'} {m : ℕ} {I : Vector Bool m} (h1 : n ≤ m) : (B.relabel f hf)[I] = B[Vector.ofFn fun (x : Fin B.nvars) => I[f x]]

theorem BDD.relabel_dependsOn {n : ℕ} {B : BDD} {f : Fin B.nvars → Fin n} {hf : ∀ (i i' : Fin B.nvars), B.DependsOn ↑i → B.DependsOn ↑i' → i < i' → f i < f i'} {i : Fin n} : (B.relabel f hf).DependsOn ↑i ↔ ∃ (j : Fin B.nvars), i = f j ∧ B.DependsOn ↑j

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

Return a satisfying assignment for the given BDD, assuming it is satisfiable.

Equations

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

@[simp]

theorem BDD.getElem_choice {B : BDD} {s : ∃ (I : Vector Bool B.nvars), B[I] = true} : B[choice s] = true

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

Return some input vector that satisfying the given BDD, or none if none exists. See also choice.

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 → ∀ (I : Vector Bool B.nvars), B[I] = false

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

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

Return the BDD obtained by fixing variable i to value b in B.

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.getElem_restrict {n : ℕ} {b : Bool} {B : BDD} {i : ℕ} {hi : i < n} {h : (restrict b i B).nvars ≤ n} (I : Vector Bool n) : (restrict b i B)[I] = B[I.set i b hi]

theorem BDD.restrict_dependsOn {B : BDD} {b : Bool} {i j : ℕ} {hi : i < B.nvars} : (restrict b i B).DependsOn j → B.DependsOn j ∧ i ≠ j

@[implicit_reducible]

instance BDD.instDecidableDependsOn (B : BDD) : DecidablePred B.DependsOn

Equations

• B.instDecidableDependsOn i = if hi : i < B.nvars then decidable_of_iff ((↑(BDD.obdd✝ B)).usesVar ⟨i, hi⟩) ⋯ else isFalse ⋯

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

Eliminate the variable i from the given BDD via universal quantification.

Equations

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

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

Eliminate variables in l from the given BDD via universal quantification.

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.getElem_bforall {n : ℕ} {B : BDD} {i : ℕ} {hi : i < n} {I : Vector Bool n} {h : (B.bforall i).nvars ≤ n} : (B.bforall i)[I] = decide (∀ (b : Bool), B[I.set i b hi] = true)

theorem BDD.bforall_dependsOn {B : BDD} {i j : ℕ} {hi : i < B.nvars} : (B.bforall i).DependsOn j → B.DependsOn j ∧ i ≠ j

@[simp]

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

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

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

Eliminate the variable i from the given BDD via existential quantification.

Equations

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

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

Eliminate variables in l from the given BDD via existential quantification.

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.getElem_bexists {n : ℕ} {B : BDD} {i : ℕ} {hi : i < n} {I : Vector Bool n} {h : (B.bexists i).nvars ≤ n} : (B.bexists i)[I] = decide (∃ (b : Bool), B[I.set i b hi] = true)

theorem BDD.bexists_dependsOn {B : BDD} {i j : ℕ} {hi : i < B.nvars} : (B.bexists i).DependsOn j → B.DependsOn j ∧ i ≠ j

@[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)[I] = (B.bexists i)[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)[I] = ((B.bexists ↑j).bexists ↑i)[I]

def BDD.count (B : BDD) : ℕ

Return the number of satisfying assignments the given BDD.

Equations

• B.count = Count.count (BDD.obdd✝ B)

theorem BDD.count_eq_card {B : BDD} : B.count = Fintype.card { I : Vector Bool B.nvars // B[I] = true }