src/mvfaig/mvfaigUtil.c

Go to the documentation of this file.

#include "mvfaigInt.h"

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


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

void
MvfAig_Init(void)
{
}


void
MvfAig_End(void)
{
}


MvfAig_Function_t *
MvfAig_FunctionAlloc(
  int n)
{
  int      i;
  array_t *bAndInvArray = array_alloc(bAigEdge_t, n);

  for (i = 0; i < n; i++) {
    array_insert(bAigEdge_t, bAndInvArray, i, bAig_Zero);
  }
  return ((MvfAig_Function_t *) bAndInvArray);
}

void
MvfAig_FunctionFree(
  MvfAig_Function_t *function)
{
  array_free((array_t *) function);
}

MvfAig_Function_t *
MvfAig_FunctionDuplicate(
  MvfAig_Function_t *function)
{
  return ((MvfAig_Function_t *) array_dup((array_t *) function));
}


void
MvfAig_FunctionArrayFree(
  array_t *functionArray)
{
  int i;

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


int
MvfAig_FunctionReadNumComponents(
  MvfAig_Function_t *function)
{
  return (array_n((array_t *) function));
}


mAigEdge_t
MvfAig_FunctionReadComponent(
  MvfAig_Function_t *function,
  int i)
{
  bAigEdge_t component = array_fetch(bAigEdge_t, (array_t *) function, i);
  return (component);
}


MvfAig_Function_t *
MvfAig_FunctionCreateFromVariable(
  mAig_Manager_t *manager,
  mAigEdge_t mVarId)
{
  int        i;
  array_t   *mVarList    = mAigReadMulVarList(manager);
  mAigMvar_t mVar;
  array_t   *result;

  assert( (mVarId >= 0) && (mVarId <= array_n(mVarList)));
  mVar   = array_fetch(mAigMvar_t, mVarList, mVarId);
  result = array_alloc(bAigEdge_t, mVar.values);  /* array of all possible values of this variable */
  for(i = 0; i < mVar.values; i++) {
    bAigEdge_t literal;

    literal = mAig_EquC(manager, mVarId, i);       /* AndInv graph = 1 if the variable = i*/
    array_insert(bAigEdge_t, result, i, literal);
    {
      /*
        The name of the node in AIG is node name = node value.
       */
      /*
      char *valueStr = util_inttostr(i);
      char *name     = util_strcat3(mVar.name,"=", valueStr);
      char *tmpName;
      int  index;
      
      bAig_NodeSetName(manager, literal, name);
      FREE(valueStr);
      */
    }
  }
  return ((MvfAig_Function_t *) result);
} 


void
MvfAig_FunctionAddMintermsToComponent(
  mAig_Manager_t    *manager,
  MvfAig_Function_t *function,
  int               i,
  mAigEdge_t        g)
{
  mAigEdge_t oldComponent;
  mAigEdge_t newComponent;
  array_t    *mAigArray = (array_t *) function;

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

  oldComponent = array_fetch(mAigEdge_t , mAigArray, i);
  newComponent = mAig_Or(manager, oldComponent, g);
  array_insert(mAigEdge_t , mAigArray, i, newComponent);
}

mAigEdge_t 
MvfAig_FunctionsComputeEquivalentSet(
  mAig_Manager_t *manager, 
  MvfAig_Function_t *function1,
  MvfAig_Function_t *function2)
{
  int          i;
  array_t     *mAigArray1     = (array_t *) function1;
  array_t     *mAigArray2     = (array_t *) function2;
  int          numComponents = array_n(mAigArray1);
  mAigEdge_t   product       = mAig_One;

  assert(numComponents == array_n(mAigArray1));
  assert(numComponents == array_n(mAigArray2));
  
  for (i = 0; i < numComponents; i++) {
    mAigEdge_t mAig1 = array_fetch(mAigEdge_t, mAigArray1, i);
    mAigEdge_t mAig2 = array_fetch(mAigEdge_t, mAigArray2, i);
    mAigEdge_t xnor = mAig_Eq(manager, mAig1, mAig2);
    mAigEdge_t temp = product;

    product = mAig_And(manager, temp, xnor);
  }

  return product;
}

mAigEdge_t 
MvfAig_FunctionComputeDomain(
  mAig_Manager_t *manager,
  MvfAig_Function_t *function)
{
  int          i;
  array_t     *mAigArray     = (array_t *) function;
  int          numComponents = array_n(mAigArray);
  mAigEdge_t   sum           = mAig_Zero;

  for (i = 0; i < numComponents; i++) {
    mAigEdge_t ithComponent = array_fetch(mAigEdge_t , mAigArray, i);
    mAigEdge_t temp = sum;
    
    sum = mAig_Or(manager, temp, ithComponent);
  }
  return sum;
}

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


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