Unique Quantification is Broken

[nhusung]

$\exists! x_0. \top$ should be $\top\vert_{x_0 = \bot} \oplus \top\vert_{x_0 = \top} \equiv \top \oplus \top \equiv \bot$, but BuDDy returns $\top$. Here is a test for reproducing the bug:

#include <bdd.h>
#include <stdio.h>

int main(void) {
  bdd_init(1024, 256);
  bdd_setvarnum(3);

  int x[] = {0};
  BDD set = bdd_makeset(x, 1);
  BDD res = bdd_unique(bdd_true(), set);

  if (res == bdd_true()) {
    puts("res is true");
  } else if (res == bdd_false()) {
    puts("res is false");
  }
}

For reference: AFAIK, unique quantification is the same as the Boolean difference or Boolean derivative.

From my side, there is no urge to fix this bug, I just wanted to report it in case someone else stumbles across incorrect results.

[ssoelvsten]

Interesting! The bdd_unique function is implemented as quantification with XOR, i.e. it uses quant_rec with xor_op. Here, every (existing) to-be quantified node in the BDD is resolved with a nested call to apply_rec. That is, it assumes a skipped variable (a Don't Care) does not change the result. This is indeed true for and_op and or_op but not xor_op.

To fix it, one would need to implement another quant_rec which immediately collapses to the false terminal when it skips a variable. In BuDDy, one uses a vartable (created with varset2vartable) to quickly discern whether a variable needs to be quantified. For bdd_unique one would have to check all skipped levels before recursing.

Fixing this is not going to be high on my priority list either. But, now there is a guide on how to get started fixing it.