src/mvf/mvfMvf.c

Go to the documentation of this file.

#include "mvfInt.h"

static char rcsid[] UNUSED = "$Id: mvfMvf.c,v 1.6 2002/09/08 21:48:24 fabio Exp $";

/*---------------------------------------------------------------------------*/
/* Static function prototypes                                                */
/*---------------------------------------------------------------------------*/


/*---------------------------------------------------------------------------*/
/* Definition of exported functions                                          */
/*---------------------------------------------------------------------------*/

void
Mvf_Init(void)
{
}


void
Mvf_End(void)
{
}


Mvf_Function_t *
Mvf_FunctionAlloc(
  mdd_manager *mddManager,
  int n)
{
  int      i;
  array_t *mddArray = array_alloc(mdd_t *, n);

  for (i = 0; i < n; i++) {
    array_insert(mdd_t *, mddArray, i, mdd_zero(mddManager));
  }
  return ((Mvf_Function_t *) mddArray);
}


void
Mvf_FunctionAddMintermsToComponent(
  Mvf_Function_t *function,
  int             i,
  mdd_t          *g)
{
  mdd_t   *oldComponent;
  mdd_t   *newComponent;
  array_t *mddArray = (array_t *) function;

  assert((i >= 0) && (i < array_n(mddArray)));

  oldComponent = array_fetch(mdd_t *, mddArray, i);
  newComponent = mdd_or(oldComponent, g, 1, 1);
  mdd_free(oldComponent);
  array_insert(mdd_t *, mddArray, i, newComponent);
}


mdd_t *
Mvf_FunctionBuildRelationWithVariable(
  Mvf_Function_t *function,
  int mddId)
{
  int          i;
  mvar_type    mddVar;
  array_t     *mddArray     = (array_t *) function;
  mdd_manager *mddManager   = Mvf_FunctionReadMddManager(function);
  mdd_t       *sumOfFactors = mdd_zero(mddManager);
  
  mddVar = array_fetch(mvar_type, mdd_ret_mvar_list(mddManager), mddId);
  assert(mddVar.values == Mvf_FunctionReadNumComponents(function));

  for (i = 0; i < array_n(mddArray); i++) {
    mdd_t *varLiteral;
    mdd_t *factor;
    mdd_t *tmp;
    mdd_t *fComponent = array_fetch(mdd_t *, mddArray, i);

    varLiteral = mdd_eq_c(mddManager, mddId, i);
    factor = mdd_and(fComponent, varLiteral, 1, 1);
    mdd_free(varLiteral);

    /* Take the or of the sumOfFactors so far and the new factor */
    tmp = mdd_or(sumOfFactors, factor, 1, 1);
    mdd_free(factor);
    mdd_free(sumOfFactors);
    sumOfFactors = tmp;
  } 

  return sumOfFactors;
} 


int
Mvf_FunctionReadNumComponents(
  Mvf_Function_t *function)
{
  return (array_n((array_t *) function));
}


mdd_manager *
Mvf_FunctionReadMddManager(
  Mvf_Function_t *function)
{
  mdd_t *component = array_fetch(mdd_t *, (array_t *) function, 0);
  
  return (mdd_get_manager(component));
}


Mvf_Function_t *
Mvf_FunctionDuplicate(
  Mvf_Function_t *function)
{
  return ((Mvf_Function_t *) mdd_array_duplicate((array_t *) function));
}


void
Mvf_FunctionFree(
  Mvf_Function_t *function)
{
  mdd_array_free((array_t *) function);
}


void
Mvf_FunctionArrayFree(
  array_t *functionArray)
{
  int i;

  if (functionArray != NIL(array_t)) {
    for (i = 0; i < array_n(functionArray); i++) {
      Mvf_Function_t *function = array_fetch(Mvf_Function_t *, functionArray, i);
      Mvf_FunctionFree(function);
    }
    array_free(functionArray);
  }
}

mdd_t *
Mvf_FunctionObtainComponent(
  Mvf_Function_t *function,
  int i)
{
  mdd_t *component = array_fetch(mdd_t *, (array_t *) function, i);
  return (mdd_dup(component));
}

mdd_t *
Mvf_FunctionReadComponent(
  Mvf_Function_t *function,
  int i)
{
  mdd_t *component = array_fetch(mdd_t *, (array_t *) function, i);
  return (component);
}


Mvf_Function_t *
Mvf_FunctionCreateFromVariable(
  mdd_manager *mddManager,
  int mddId)
{
  int        i;
  array_t   *mvar_list = mdd_ret_mvar_list(mddManager);
  mvar_type  varInfo;
  array_t   *result;

  assert(mddId >= 0);

  varInfo   = array_fetch(mvar_type, mvar_list, mddId);
  result    = array_alloc(mdd_t *, varInfo.values);

  for(i = 0; i < varInfo.values; i++) {
    mdd_t *literal;

    literal = mdd_eq_c(mddManager, mddId, i);
    array_insert(mdd_t *, result, i, literal);
  } 

  return ((Mvf_Function_t *) result);
} 


Mvf_Function_t *
Mvf_FunctionComposeWithFunctionArray(
  Mvf_Function_t *f,
  array_t        *mddIdArray /* of int */,   
  array_t        *functionArray /* of Mvf_Function_t* */)
{
  Mvf_Function_t *result;
  int i;

  assert(array_n(mddIdArray) == array_n(functionArray));

  /* Make an initial copy of the function */
  result = Mvf_FunctionDuplicate(f);

  for(i = 0; i < array_n(mddIdArray); i++) {
    Mvf_Function_t *tmp;
    int             mddId = array_fetch(int, mddIdArray, i);
    Mvf_Function_t *g     = array_fetch(Mvf_Function_t *, functionArray, i);
    
    tmp = Mvf_FunctionComposeWithFunction(result, mddId, g);

    Mvf_FunctionFree(result);
    result = tmp;
  } 

  return result;
}


Mvf_Function_t *
Mvf_FunctionComposeWithFunction(
  Mvf_Function_t *f,
  int             mddId,
  Mvf_Function_t *g)
{
  mdd_t   *sumOfFactors;
  array_t *result;
  array_t *values;
  int      i;
  mdd_manager *mddManager = Mvf_FunctionReadMddManager(f);

  /* Allocate array to hold values for the literal and the result */
  result = array_alloc(mdd_t *, array_n(f));

  /*
   * Create the sum of factors (x==i * gi). This function will verify that the
   * domain of x and the range of g have the same cardinality.
   */
  sumOfFactors = Mvf_FunctionBuildRelationWithVariable(g, mddId);

  /* 
   * Result is an array of mdd_t * , result[i] = Exists(x) (f[i] * sumOfFactors)
   * The array values holds now the index of the variable to smooth out.
   */
  values = array_alloc(int, 1);
  array_insert(int, values, 0, mddId);
  for(i = 0; i < array_n(f); i++) {
    mdd_t *functionUnit = array_fetch(mdd_t *, f, i);
    mdd_t *tmp          = mdd_and_smooth(mddManager, functionUnit, sumOfFactors, values);

    array_insert(mdd_t *, result, i, tmp);
  } 

  /* Clean up */
  array_free(values);
  mdd_free(sumOfFactors);

  return ((Mvf_Function_t *) result);
}


mdd_t *
Mvf_MddComposeWithFunction(
  mdd_t          *f,
  int             mddId,
  Mvf_Function_t *g)
{
  mdd_t       *sumOfFactors;
  mdd_t       *result;
  array_t     *values;
  mdd_manager *mddManager = mdd_get_manager(f);
  
  /*
   * Create the sum of factors (x==i * gi). This function will verify that the
   * domain of x and the range of g have the same cardinality.
   */
  sumOfFactors = Mvf_FunctionBuildRelationWithVariable(g, mddId);

  /* Result is an mdd_t * , result = Exists(x) (f * sumOfFactors) */
  values = array_alloc(int, 1);
  array_insert(int, values, 0, mddId);
  result = mdd_and_smooth(mddManager, f, sumOfFactors, values);

  /* Clean up */
  array_free(values);
  mdd_free(sumOfFactors);

  return result;
} 


boolean
Mvf_FunctionTestIsDeterministic(
  Mvf_Function_t *function)
{
  int      i;
  array_t *mddArray      = (array_t *) function;
  int      numComponents = array_n(mddArray);
  mdd_t   *sum;

  if (numComponents == 0) {
    return TRUE;
  }
  
  sum = mdd_dup(array_fetch(mdd_t *, mddArray, 0));
  
  for (i = 1; i < numComponents; i++) {
    mdd_t *temp         = sum;
    mdd_t *ithComponent = array_fetch(mdd_t *, mddArray, i);
    boolean intersectionIsEmpty = mdd_lequal(ithComponent, sum, 1, 0);
    
    /* If the intersection is not empty, then return FALSE. */
    if (!intersectionIsEmpty) {
      mdd_free(sum);
      return FALSE;
    }

    sum = mdd_or(temp, ithComponent, 1, 1);
    mdd_free(temp);
  }
  mdd_free(sum);
  
  /* The components are pairwise disjoint. */
  return TRUE;
}


boolean
Mvf_FunctionTestIsCompletelySpecified(
  Mvf_Function_t *function)
{
  mdd_t   *sum            = Mvf_FunctionComputeDomain(function);
  boolean  sumIsTautology = mdd_is_tautology(sum, 1);

  mdd_free(sum);
  return sumIsTautology;
}


boolean
Mvf_FunctionTestIsConstant(
  Mvf_Function_t *function,
  int            *constantValue /* return value */ )
{
  int      i;
  array_t *mddArray      = (array_t *) function;
  int      numComponents = array_n(mddArray);
  int      numTautComps  = 0;

  for (i = 0; i < numComponents; i++) {
    mdd_t *ithComponent = array_fetch(mdd_t *, mddArray, i);

    if (mdd_is_tautology(ithComponent, 1)) {
      *constantValue = i;
      numTautComps++;
    }
    else if (!mdd_is_tautology(ithComponent, 0)) {
      /* this component is not 1 nor 0, so function can't be a constant */
      return FALSE;
    }
    /* else, must be the zero function */
  }

  return (numTautComps == 1);
}


boolean
Mvf_FunctionTestIsNonDeterministicConstant(
  Mvf_Function_t *function)
{
  int      i;
  array_t *mddArray      = (array_t *) function;
  int      numComponents = array_n(mddArray);
  int      numTautComps  = 0;

  for (i = 0; i < numComponents; i++) {
    mdd_t *ithComponent = array_fetch(mdd_t *, mddArray, i);

    if (mdd_is_tautology(ithComponent, 1)) {
      numTautComps++;
    }
    else if (!mdd_is_tautology(ithComponent, 0)) {
      /* this component is not 1 nor 0, so function can't be a non-det constant */
      return FALSE;
    }
    /* else, must be the zero function */
  }

  return (numTautComps > 1);
}


mdd_t *
Mvf_FunctionComputeDomain(
  Mvf_Function_t *function)
{
  array_t     *mddArray   = (array_t *) function;
  mdd_manager *mddManager = Mvf_FunctionReadMddManager(function);
  mdd_t       *sum        = mdd_multiway_or(mddManager, mddArray);

  return sum;
}


boolean
Mvf_FunctionTestIsWellFormed(
  Mvf_Function_t *function)
{
  return (Mvf_FunctionTestIsDeterministic(function) 
          && Mvf_FunctionTestIsCompletelySpecified(function));
}


boolean
Mvf_FunctionTestIsEqualToFunction(
  Mvf_Function_t *function1,
  Mvf_Function_t *function2)
{
  int      i;
  array_t *mddArray1     = (array_t *) function1;
  array_t *mddArray2     = (array_t *) function2;
  int      numComponents = array_n(mddArray1);

  if (numComponents != array_n(mddArray2)) {
    return FALSE;
  }

  for (i = 0; i < numComponents; i++) {
    mdd_t *mdd1 = array_fetch(mdd_t *, mddArray1, i);
    mdd_t *mdd2 = array_fetch(mdd_t *, mddArray2, i);
    if (!mdd_equal(mdd1, mdd2)) {
      return FALSE;
    }
  }

  return TRUE;
}


mdd_t *
Mvf_FunctionsComputeEquivalentSet(
  Mvf_Function_t *function1,
  Mvf_Function_t *function2)
{
  int          i;
  array_t     *mddArray1     = (array_t *) function1;
  array_t     *mddArray2     = (array_t *) function2;
  int          numComponents = array_n(mddArray1);
  mdd_manager *mddManager    = Mvf_FunctionReadMddManager(function1);
  mdd_t       *product       = mdd_one(mddManager);

  assert(numComponents == array_n(mddArray2));
  
  for (i = 0; i < numComponents; i++) {
    mdd_t *mdd1 = array_fetch(mdd_t *, mddArray1, i);
    mdd_t *mdd2 = array_fetch(mdd_t *, mddArray2, i);
    mdd_t *xnor = mdd_xnor(mdd1, mdd2);
    mdd_t *temp = product;

    product = mdd_and(temp, xnor, 1, 1);
    mdd_free(temp);
    mdd_free(xnor);
  }

  return product;
}

  
Mvf_Function_t *
Mvf_FunctionCofactor(
  Mvf_Function_t * function,
  mdd_t          * wrtMdd)
{
  int      i;
  array_t *mddArray      = (array_t *) function;
  int      numComponents = array_n(mddArray);
  array_t *newFunction   = array_alloc(mdd_t *, numComponents);
  
  for(i = 0; i < numComponents; i++) {
    mdd_t *component = array_fetch(mdd_t *, mddArray, i);
    mdd_t *cofactor  = bdd_cofactor(component, wrtMdd);

    array_insert(mdd_t *, newFunction, i, cofactor);
  }
  return((Mvf_Function_t *)newFunction);
}


Mvf_Function_t *
Mvf_FunctionMinimize(
  Mvf_Function_t *f,
  mdd_t          *c)
{
  int      i;
  array_t *mddArray      = (array_t *) f;
  int      numComponents = array_n(mddArray);
  array_t *newFunction   = array_alloc(mdd_t *, numComponents);
  
  for(i = 0; i < numComponents; i++) {
    mdd_t *component = array_fetch(mdd_t *, mddArray, i);
    mdd_t *minimize  = bdd_minimize(component, c);

    array_insert(mdd_t *, newFunction, i, minimize);
  }
  return((Mvf_Function_t *)newFunction);
}


long
Mvf_FunctionArrayComputeNumBddNodes(
  array_t * functionArray)
{
  int      i;
  long     numNodes;
  array_t *mddArray = array_alloc(mdd_t *, 0);

  /* Build an array of all MDDs */
  for(i = 0; i < array_n(functionArray); i++) {
    int      j;
    array_t *function = (array_t *)array_fetch(Mvf_Function_t *, functionArray, i);

    for(j = 0; j < array_n(function); j++) {
      mdd_t *component = array_fetch(mdd_t *, function, j);
      array_insert_last(mdd_t *, mddArray, component);
    }
  }
  
  /* Compute the reduced number of bdd nodes */
  numNodes = mdd_size_multiple(mddArray);
  array_free(mddArray);
  
  return(numNodes);
}


long
Mvf_FunctionComputeNumBddNodes(
  Mvf_Function_t * function)
{
  return(mdd_size_multiple((array_t *)function));
}


int
Mvf_FunctionFindFirstTrueComponent(
  Mvf_Function_t * function)
{
  int      i;
  array_t *mddArray = (array_t *) function;
  
  for(i = 0; i < array_n(mddArray); i++) {
    mdd_t *component = array_fetch(mdd_t *, mddArray, i);
    if (mdd_is_tautology(component, 1)) {
      return(i);
    }
  }
  return(-1);
}

int
Mvf_FunctionComputeHashValue(
  Mvf_Function_t * function)
{
  int      i;
  int      result   = 0;
  array_t *mddArray = (array_t *) function;
  
  for(i = 0; i < array_n(mddArray); i++) {
    mdd_t *component = array_fetch(mdd_t *, mddArray, i);
    result += (mdd_top_var_id(component)) * (i + 1);
  }
  return(result);
}



array_t *
Mvf_FunctionComputeSupport(
  Mvf_Function_t *function,
  mdd_manager *mddMgr,
  int *value)
{
  int        i;
  mdd_t     *component;
  array_t   *totalSupportArray;
  var_set_t *totalSupportSet;
  int        numMddVars = array_n(mdd_ret_mvar_list(mddMgr));

  /*
   * Handle the case where function is just a constant.
   */
  if (Mvf_FunctionTestIsConstant(function, value)) {
    return NIL(array_t);
  }
  
  /*
   * Accumulate the union of supports of the function components into a bit
   * array.
   */
  totalSupportArray = array_alloc(int, 0);
  totalSupportSet   = var_set_new(numMddVars);

  Mvf_FunctionForEachComponent(function, i, component) {
    int      j;
    int      mddVarId;
    array_t *support = mdd_get_support(mddMgr, component);

    arrayForEachItem(int, support, j, mddVarId) {
      var_set_set_elt(totalSupportSet, mddVarId);
    }
    array_free(support);
  }
  
  /* Convert the bit array to an array of mdd ids. */
  for (i = 0; i < numMddVars; i++) {
    if (var_set_get_elt(totalSupportSet, i)) {
      array_insert_last(int, totalSupportArray, i);
    }
  }
  var_set_free(totalSupportSet);

  return totalSupportArray;
}

/*---------------------------------------------------------------------------*/
/* Definition of internal functions                                          */
/*---------------------------------------------------------------------------*/


/*---------------------------------------------------------------------------*/
/* Definition of static functions                                            */
/*---------------------------------------------------------------------------*/