Hybrid unique abstraction

unique.c

DdNode* uniqueAbstractRec(DdManager* home, DdNode* f, DdNode* cube) {
  // satLine(home)
  uniqueStats.recursiveCalls++;

  DdNode* one = Cudd_ReadOne(home);
  DdNode* zero = Cudd_Not(one);
  DdNode* 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 is not constant
  int topf = var2level(home, f);
  int topc = var2level(home, cube);

  if (topc < topf) { // Variable in cube is a don't care in f
    uniqueStats.varAbstracted++;
    return zero;
  }

  // Check the cache
  if (F->ref != 1) {
    DdNode* result = cuddCacheLookup2(home, uniqueAbstract, f, cube);
    if (result != NULL) {
      uniqueStats.cacheHits++;
      return result;
    }
  }

  DdNode* T = Cudd_T(F);
  DdNode* E = Cudd_E(F);
  if (f != F) {
    T = Cudd_Not(T);
    E = Cudd_Not(E);
  }

  if (topf == topc) {
    uniqueStats.abstract++;

    if (E == zero) {
      uniqueStats.abstractSimple++;
      DdNode* res = uniqueAbstractRec(home, T, Cudd_T(cube));
      if (res == NULL)
        return NULL;
      if (F->ref != 1)
        cuddCacheInsert2(home, uniqueAbstract, f, cube, res);
      return res;
    } else if (T == zero) {
      uniqueStats.abstractSimple++;
      DdNode* res = uniqueAbstractRec(home, E, Cudd_T(cube));
      if (res == NULL)
        return NULL;
      if (F->ref != 1)
        cuddCacheInsert2(home, uniqueAbstract, f, cube, res);
      return res;
    } else {
      uniqueStats.abstractComplex++;
      DdNode* EX = cuddBddExistAbstractRecur(home, E, Cudd_T(cube));
      if (EX == NULL) {
        return NULL;
      }
      Cudd_Ref(EX);
      uniqueStats.existAbstract++;
      DdNode* TX = cuddBddExistAbstractRecur(home, T, Cudd_T(cube));
      if (TX == NULL) {
        Cudd_IterDerefBdd(home, EX);
        return NULL;
      }
      Cudd_Ref(TX);
      uniqueStats.existAbstract++;
      if (EX == TX) {
        Cudd_IterDerefBdd(home, EX);
        Cudd_IterDerefBdd(home, TX);
        if (F->ref != 1)
          cuddCacheInsert2(home, uniqueAbstract, f, cube, zero);
        return zero;
      }
      // This is the really complex case

      DdNode* resultThen; // resultThen = uniqueThen /\ ~EX
      {
        DdNode* uniqueThen = uniqueAbstractRec(home, T, Cudd_T(cube));
        if (uniqueThen == NULL)
          return NULL;
        Cudd_Ref(uniqueThen);

        resultThen = cuddBddAndRecur(home, uniqueThen, Cudd_Not(EX));
        if (resultThen == NULL) {
          Cudd_IterDerefBdd(home, uniqueThen);
          return NULL;
        }
        Cudd_Ref(resultThen);
        Cudd_IterDerefBdd(home, uniqueThen);
        Cudd_IterDerefBdd(home, EX);
      }

      DdNode* resultElse; // resultElse = uniqueElse /\ ~TX
      {
        DdNode* uniqueElse = uniqueAbstractRec(home, E, Cudd_T(cube));
        if (uniqueElse == NULL) {
          Cudd_IterDerefBdd(home, resultThen);
          Cudd_IterDerefBdd(home, TX);
          return NULL;
        }
        Cudd_Ref(uniqueElse);

        resultElse = cuddBddAndRecur(home, uniqueElse, Cudd_Not(TX));
        if (resultElse == NULL) {
          Cudd_IterDerefBdd(home, resultThen);
          Cudd_IterDerefBdd(home, TX);
          Cudd_IterDerefBdd(home, uniqueElse);
          return NULL;
        }
        Cudd_Ref(resultElse);
        Cudd_IterDerefBdd(home, TX);
        Cudd_IterDerefBdd(home, uniqueElse);
      }

      DdNode* result =
          cuddBddAndRecur(home, Cudd_Not(resultThen), Cudd_Not(resultElse));
      if (result == NULL) {
        Cudd_IterDerefBdd(home, resultThen);
        Cudd_IterDerefBdd(home, resultElse);
        return NULL;
      }
      result = Cudd_Not(result); // result = resultThen \/ resultElse
      Cudd_Ref(result);
      Cudd_IterDerefBdd(home, resultThen);
      Cudd_IterDerefBdd(home, resultElse);

      if (F->ref != 1) {
        cuddCacheInsert2(home, uniqueAbstract, f, cube, result);
      }
      Cudd_Deref(result);
      return result;
    }
  } else {
    uniqueStats.nonAbstract++;
    DdNode* uniqueThen = uniqueAbstractRec(home, T, cube);
    if (uniqueThen == NULL)
      return NULL;
    Cudd_Ref(uniqueThen);

    DdNode* uniqueElse = uniqueAbstractRec(home, E, cube);
    if (uniqueElse == NULL) {
      Cudd_IterDerefBdd(home, uniqueThen);
      return NULL;
    }
    Cudd_Ref(uniqueElse);

    DdNode* result =
        cuddBddIteRecur(home, topVar(home, F), uniqueThen, uniqueElse);
    if (result == NULL) {
      Cudd_IterDerefBdd(home, uniqueThen);
      Cudd_IterDerefBdd(home, uniqueElse);
      return NULL;
    }
    Cudd_Deref(uniqueThen);
    Cudd_Deref(uniqueElse);

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

    return result;
  }
}