ggutierrez

int main() {
  return 0
}

ggutierrez

#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) {

ggutierrez

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

ggutierrez

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;

ggutierrez

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;

ggutierrez

/**Function********************************************************************

  Synopsis    [Performs the recursive steps of Cudd_bddExistAbstract.]

  Description [Performs the recursive steps of Cudd_bddExistAbstract.
  Returns the BDD obtained by abstracting the variables
  of cube from f if successful; NULL otherwise. It is also used by
  Cudd_bddUnivAbstract.]

  SideEffects [None]

ggutierrez

DdNode* uniqueAbstractSERec(DdManager* home, DdNode* f, DdNode* cube) {
  // Constants
  DdNode* one = Cudd_ReadOne(home);
  DdNode* zero = Cudd_Not(one);

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

  if (f == zero || f == one) // Base case 2: f is a terminal
    return zero;

ggutierrez

BDD uniqueAbstractImplSE(const Cudd& home, BDD f, BDD cube) {
  BDD one = home.bddOne();
  BDD zero = home.bddZero();

  if (cube.IsOne())
    return f;
  if (f.IsZero() || f.IsOne())
    return zero;

  int topf = level(home, f);