Three implementations of unique abstraction

uniques.c

#include "unique.h"
#include <assert.h>
#include <cuddInt.h>

/*
  This is a copy of the function with the same name at the end of
  cuddBddAbs.c. the reason it is here is because that function is
  not in the public interface.
*/
static int bddCheckPositiveCube(DdManager *manager, DdNode *cube) {
  if (Cudd_IsComplement(cube))
    return (0);
  if (cube == DD_ONE(manager))
    return (1);
  if (cuddIsConstant(cube))
    return (0);
  if (cuddE(cube) == Cudd_Not(DD_ONE(manager))) {
    return (bddCheckPositiveCube(manager, cuddT(cube)));
  }
  return (0);
}

DdNode *cuddBddExistAbstractRecur(DdManager *manager, DdNode *f, DdNode *cube);

// Returns the level of the top variable in @a f
int var2level(DdManager *home, DdNode *f) {
  return Cudd_ReadPerm(home, Cudd_NodeReadIndex(f));
}

// Returns the variable at a given level
DdNode *topVar(DdManager *home, DdNode *f) {
  return Cudd_ReadVars(home, Cudd_NodeReadIndex(f));
}

void printUniqueAbstractionStats(DdManager *manager) {
  printf("Unique abstraction statistics:\n");
  printf("\tTotal calls: %f\n", manager->unique_abstraction_total_calls);
  printf("\tOptimized calls: %f\n",
         manager->unique_abstraction_optimized_calls);
  printf("\tTotal exist abstract calls: %f\n",
         manager->exist_abstract_total_calls);
  printf("\tUnique abstract calls to exist abstract: %f\n",
         manager->exist_abstract_calls);
  printf("\tTotal ite calls: %f\n", manager->ite_calls);
}

/**
 * @brief Unique abstraction implementation.
 *
 * Proposed by Robert Meolic:
 * http://stackoverflow.com/questions/26375035/extended-find-of-unique-tuples-in-a-relation-represented-by-a-bdd
 *
 */
DdNode *uniqueAbstractSERec(DdManager *manager, DdNode *f, DdNode *cube) {
  DdNode *F, *T, *E, *res, *res1, *res2, *EX, *TX, *one, *zero;
  int topf, topc;

  manager->unique_abstraction_total_calls++;

  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);
      manager->unique_abstraction_optimized_calls++;
      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);
      manager->unique_abstraction_optimized_calls++;
      return res;
    } else {
      EX = cuddBddExistAbstractRecur(manager, E, Cudd_T(cube));
      manager->exist_abstract_calls++;
      if (EX == NULL)
        return NULL;
      Cudd_Ref(EX);
      TX = cuddBddExistAbstractRecur(manager, T, Cudd_T(cube));
      manager->exist_abstract_calls++;
      if (TX == NULL) {
        Cudd_IterDerefBdd(manager, EX);
        return NULL;
      }
      Cudd_Ref(TX);
      if (EX == TX) {
        Cudd_IterDerefBdd(manager, EX);
        Cudd_IterDerefBdd(manager, TX);
        if (F->ref != 1)
          cuddCacheInsert2(manager, uniqueAbstract, f, cube, zero);
        return zero;
      }

      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, 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;
    }
  }
}

/**
 * @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)
  home->unique_abstraction_total_calls++;

  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
    return zero;
  }

  // Check the cache
  if (F->ref != 1) {
    DdNode *result = cuddCacheLookup2(home, uniqueAbstract, f, cube);
    if (result != NULL) {
      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) {
    if (E == zero) {
      DdNode *res = uniqueAbstractRec(home, T, Cudd_T(cube));
      if (res == NULL)
        return NULL;
      if (F->ref != 1)
        cuddCacheInsert2(home, uniqueAbstract, f, cube, res);
      home->unique_abstraction_optimized_calls++;
      return res;
    } else if (T == zero) {
      DdNode *res = uniqueAbstractRec(home, E, Cudd_T(cube));
      if (res == NULL)
        return NULL;
      if (F->ref != 1)
        cuddCacheInsert2(home, uniqueAbstract, f, cube, res);
      home->unique_abstraction_optimized_calls++;
      return res;
    } else {
      DdNode *EX = cuddBddExistAbstractRecur(home, E, Cudd_T(cube));
      home->exist_abstract_calls++;
      if (EX == NULL) {
        return NULL;
      }
      Cudd_Ref(EX);
      DdNode *TX = cuddBddExistAbstractRecur(home, T, Cudd_T(cube));
      home->exist_abstract_calls++;
      if (TX == NULL) {
        Cudd_IterDerefBdd(home, EX);
        return NULL;
      }
      Cudd_Ref(TX);
      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 =
            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 =
            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
      if (result == NULL) {
        Cudd_IterDerefBdd(home, resultThen);
        Cudd_IterDerefBdd(home, resultElse);
        return NULL;
      }
      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 {
    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;
  }
}

/**
 * @brief Unique abstraction implementation.
 *
 * Reference implementation with no optimization.
 */
DdNode *uniqueAbstractRecRef(DdManager *home, DdNode *f, DdNode *cube) {
  home->unique_abstraction_total_calls++;

  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
    return zero;

  // Check the cache
  if (F->ref != 1) {
    DdNode *result = cuddCacheLookup2(home, uniqueAbstract, f, cube);
    if (result != NULL) {
      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) {
    // resultThen = uniqueThen /\ ~EX
    DdNode *resultThen;
    {
      DdNode *uniqueThen = uniqueAbstractRecRef(home, T, Cudd_T(cube));
      if (uniqueThen == NULL)
        return NULL;
      Cudd_Ref(uniqueThen);

      DdNode *EX = cuddBddExistAbstractRecur(home, E, Cudd_T(cube));
      home->exist_abstract_calls++;
      if (EX == NULL) {
        Cudd_IterDerefBdd(home, uniqueThen);
        return NULL;
      }
      Cudd_Ref(EX);

      resultThen =
          cuddBddIteRecur(home, EX, zero, uniqueThen); // ITE(F,0,H) = !F * H
      if (resultThen == NULL) {
        Cudd_IterDerefBdd(home, uniqueThen);
        Cudd_IterDerefBdd(home, EX);
        return NULL;
      }
      Cudd_Ref(resultThen);
      Cudd_IterDerefBdd(home, uniqueThen);
      Cudd_IterDerefBdd(home, EX);
    }

    // resultElse = uniqueElse /\ ~TX
    DdNode *resultElse;
    {
      DdNode *TX = cuddBddExistAbstractRecur(home, T, Cudd_T(cube));
      home->exist_abstract_calls++;
      if (TX == NULL) {
        Cudd_IterDerefBdd(home, resultThen);
        return NULL;
      }
      Cudd_Ref(TX);

      DdNode *uniqueElse = uniqueAbstractRecRef(home, E, Cudd_T(cube));
      home->exist_abstract_calls++;
      if (uniqueElse == NULL) {
        Cudd_IterDerefBdd(home, resultThen);
        Cudd_IterDerefBdd(home, TX);
        return NULL;
      }
      Cudd_Ref(uniqueElse);

      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
    if (result == NULL) {
      Cudd_IterDerefBdd(home, resultThen);
      Cudd_IterDerefBdd(home, resultElse);
      return NULL;
    }
    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 {
    DdNode *uniqueThen = uniqueAbstractRecRef(home, T, cube);
    if (uniqueThen == NULL)
      return NULL;
    Cudd_Ref(uniqueThen);

    DdNode *uniqueElse = uniqueAbstractRecRef(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;
  }
}

DdNode *uniqueAbstract(DdManager *home, DdNode *f, DdNode *cube) {
  if (bddCheckPositiveCube(home, cube) == 0) {
    printf("The provided cube is not a cube\n");
    return NULL;
  }

  DdNode *res;
  do {
    home->reordered = 0;
    //    res = uniqueAbstractRecRef(home, f, cube);
    res = uniqueAbstractRec(home, f, cube);
    //    res = uniqueAbstractSERec(home, f, cube);
  } while (home->reordered == 1);

  return res;
}

DdNode *uniqueAbstractSE(DdManager *home, DdNode *f, DdNode *cube) {
  if (bddCheckPositiveCube(home, cube) == 0) {
    printf("The provided cube is not a cube\n");
    return NULL;
  }

  DdNode *res;
  do {
    home->reordered = 0;
    res = uniqueAbstractSERec(home, f, cube);
  } while (home->reordered == 1);

  return res;
}