Unique abstraction implementation as close to cuddBddExistAbstractRecur as possible.

uniqueAbstract.c

DdNode* uniqueAbstractSERec(DdManager* manager, DdNode* f, DdNode* cube) {
  DdNode* F, *T, *E, *res, *res1, *res2, *EX, *TX, *one, *zero;
  int topf, topc;

  one = DD_ONE(manager);
  zero = Cudd_Not(one);
  F = Cudd_Regular(f);

  if (cube == one) // Base case 1: Cube is exhausted
    return f;

  if (Cudd_IsConstant(f)) // Base case 2: f is a terminal
    return zero;

  /* From now on, f and cube are non-constant. */

  topf = var2level(manager, f);
  topc = var2level(manager, cube);

  if (topc < topf) // Variable in cube is a don't care in f
    return zero;

  /* Check the cache. */
  if (F->ref != 1 &&
      (res = cuddCacheLookup2(manager, uniqueAbstract, f, cube)) != NULL)
    return res;

  /* Compute the cofactors of f. */
  T = Cudd_T(F);
  E = Cudd_E(F);
  if (f != F) {
    T = Cudd_Not(T);
    E = Cudd_Not(E);
  }

  if (topf < topc) { // Current top of f does not need abstraction
    res1 = uniqueAbstractSERec(manager, T, cube);
    if (res1 == NULL)
      return NULL;
    Cudd_Ref(res1);

    res2 = uniqueAbstractSERec(manager, E, cube);
    if (res2 == NULL) {
      Cudd_IterDerefBdd(manager, res1);
      return NULL;
    }
    Cudd_Ref(res2);

    res = cuddBddIteRecur(manager, topVar(manager, F), res1, res2);
    if (res == NULL) {
      Cudd_IterDerefBdd(manager, res1);
      Cudd_IterDerefBdd(manager, res2);
      return NULL;
    }
    Cudd_Deref(res1);
    Cudd_Deref(res2);

    if (F->ref != 1)
      cuddCacheInsert2(manager, uniqueAbstract, f, cube, res);

    return res;

  } else { /* Abstarct the current top. */
    assert(topc == topf);
    if (E == zero) {
      res = uniqueAbstractSERec(manager, T, Cudd_T(cube));
      if (res == NULL)
        return NULL;
      if (F->ref != 1)
        cuddCacheInsert2(manager, uniqueAbstract, f, cube, res);
      return res;
    } else if (T == zero) {
      res = uniqueAbstractSERec(manager, E, Cudd_T(cube));
      if (res == NULL)
        return NULL;
      if (F->ref != 1)
        cuddCacheInsert2(manager, uniqueAbstract, f, cube, res);
      return res;
    } else {
      EX = cuddBddExistAbstractRecur(manager, E, Cudd_T(cube));
      if (EX == NULL)
        return NULL;
      TX = cuddBddExistAbstractRecur(manager, T, Cudd_T(cube));
      if (TX == NULL)
        return NULL;
      if (EX == TX) {
        if (F->ref != 1)
          cuddCacheInsert2(manager, uniqueAbstract, f, cube, zero);
        return zero;
      }
      Cudd_Ref(EX);
      Cudd_Ref(TX);

      DdNode* iteExFalseThen = cuddBddIteRecur(manager, EX, zero, T);
      if (iteExFalseThen == NULL) {
        Cudd_IterDerefBdd(manager, EX);
        Cudd_IterDerefBdd(manager, TX);
        return NULL;
      }
      Cudd_Ref(iteExFalseThen);
      Cudd_IterDerefBdd(manager, EX);

      DdNode* iteTxFalseElse = cuddBddIteRecur(manager, TX, zero, E);
      if (iteTxFalseElse == NULL) {
        Cudd_IterDerefBdd(manager, EX);
        Cudd_IterDerefBdd(manager, TX);
        Cudd_IterDerefBdd(manager, iteExFalseThen);
        return NULL;
      }
      Cudd_Ref(iteTxFalseElse);
      Cudd_IterDerefBdd(manager, TX);

      res1 = cuddBddIteRecur(manager, iteExFalseThen, one, iteTxFalseElse);
      if (res1 == NULL) {
        Cudd_IterDerefBdd(manager, iteExFalseThen);
        Cudd_IterDerefBdd(manager, iteTxFalseElse);
        return NULL;
      }
      Cudd_Ref(res1);
      Cudd_IterDerefBdd(manager, iteExFalseThen);
      Cudd_IterDerefBdd(manager, iteTxFalseElse);

      res = uniqueAbstractSERec(manager, res1, Cudd_T(cube));
      if (res == NULL) {
        Cudd_IterDerefBdd(manager, res1);
        return NULL;
      }
      Cudd_Ref(res);
      Cudd_IterDerefBdd(manager, res1);

      // Store the result in the cache
      if (F->ref != 1)
        cuddCacheInsert2(manager, uniqueAbstract, f, cube, res);

      Cudd_Deref(res);
      return res;
    }
  }
}