Unique abstraction reference

unique.c

/**
 * @brief Unique abstraction implementation.
 *
 * This implementation includes some optimizations from Meolic's proposal.
 * However, it does make the recursive calls before combining the results
 * with the ITE operator.
 */
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));
        resultThen =
            cuddBddIteRecur(home, EX, zero, uniqueThen); // ITE(F,0,H) = !F * H
        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));
        resultElse =
            cuddBddIteRecur(home, TX, zero, uniqueElse); // ITE(F,0,H) = !F * H
        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 = cuddBddIteRecur(home, resultThen, one,
                                       resultElse); // ITE(F,1,H) = F + H
      // DdNode* result =
      //    cuddBddAndRecur(home, Cudd_Not(resultThen), Cudd_Not(resultElse));

      if (result == NULL) {
        Cudd_IterDerefBdd(home, resultThen);
        Cudd_IterDerefBdd(home, resultElse);
        return NULL;
      }
      // The folowing is required if cuddBddAndRecur is used to compute the or.
      // 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;
  }
}