Simplifying a BDD relative to an implication

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

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

Case 1: `c₁ < c₂`

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