¶Simplifying a BDD relative to an implication

[Andersen2011] is the canonical BDD introduction that I read during grad school.

https://www.cmi.ac.in/~madhavan/courses/verification-2011/andersen-bdd.pdf

It describes an algorithm called Simplify, which simplifies one BDD relation to another. That is, given two BDDs representing functions d and u, Simplify(d, u) returns another BDD u' where d ∧ u == d ∧ u'.

For constraint sets, d will be an implication describing that two individual constraints simplify relative to each other, c₁ → c₂. (If c₁ is true, then we know that c₂ is true as well.) The simplification will remove parts of the BDD where we make a redundant check on c₂ (that is, where we've already established that c₁ is true, and therefore don't need to check c₂).

Here we specialize the Simplify algorithm where d is fixed to the implication c₁ → c₂.

The text of the algorithm from [Andersen2011] is:

fn Simplify(d, u) {
  if d = 0 then return 0
  else if u ≤ 1 then return u
  else if d = 1 then
    return Mk(var(u), Simplify(d, low(u)), Simplify(d, high(u)))
  else if var(d) = var(u) then
    if low(d) = 0 then return Simplify(high(d), high(u))
    else if high(d) = 0 then return Simplify(low(d), low(u))
    else return Mk(var(u),
                   Simplify(low(d), low(u)),
                   Simplify(high(d), high(u)))
  else if var(d) < var(u) then
    return Mk(var(d), Simplify(low(d), u), Simplify(high(d), u))
  else
    return Mk(var(u), Simplify(d, low(u)), Simplify(d, high(u)))
}

There are two cases to consider: c₁ < c₂ and c₂ < c₁. (That is c₁ appears before or after c₂ in the BDD variable ordering; we're not talking about subtyping between the two constraints or the types they contain.)

d₁ = c₁ → c₂ = ¬c₁ ∨ c₂
var(d₁)  = c₁
low(d₁)  = 1
high(d₁) = d₂
var(d₂)  = c₂
low(d₂)  = 0
high(d₂) = 1

fn Simplify(d₁, u) {
  if u ≤ 1 then return u
  else if var(u) = c₁ then
    return Mk(c₁,
              Simplify(1, low(u)),
              Simplify(d₂, high(u)))
  else if c₁ < var(u) then
    return Mk(c₁, Simplify(1, u), Simplify(d₂, u))
  else
    return Mk(var(u), Simplify(d₁, low(u)), Simplify(d₁, high(u)))
}