src/abs/absCatalog.c

Go to the documentation of this file.

#include "absInt.h" 

static char rcsid[] UNUSED = "$Id: absCatalog.c,v 1.8 2005/04/16 04:22:21 fabio Exp $";


/*---------------------------------------------------------------------------*/
/* Structure declarations                                                    */
/*---------------------------------------------------------------------------*/

struct AbsVertexCatalog {
  lsList fixedPoints;
  lsList booleanOps;
  lsList negations;
  lsList preImages;
  lsList identifiers;
  lsList variables;
};

/*---------------------------------------------------------------------------*/
/* Macro declarations                                                        */
/*---------------------------------------------------------------------------*/

#define AbsVertexCatalogReadFixedPoints(\
  /* AbsVertexCatalog_t * */ cPtr      \
)                                      \
    (cPtr->fixedPoints)

#define AbsVertexCatalogReadBooleanOps(\
  /* AbsVertexCatalog_t * */ cPtr      \
)                                      \
    (cPtr->booleanOps)

#define AbsVertexCatalogReadNegations(\
  /* AbsVertexCatalog_t * */ cPtr      \
)                                      \
    (cPtr->negations)

#define AbsVertexCatalogReadPreImages(\
  /* AbsVertexCatalog_t * */ cPtr      \
)                                      \
    (cPtr->preImages)

#define AbsVertexCatalogReadIdentifiers(\
  /* AbsVertexCatalog_t * */ cPtr      \
)                                      \
    (cPtr->identifiers)

#define AbsVertexCatalogReadVariables(\
  /* AbsVertexCatalog_t * */ cPtr     \
)                                     \
    (cPtr->variables)

#define AbsVertexCatalogSetFixedPoints(\
  /* AbsVertexCatalog_t * */ cPtr,    \
  /* lsList */ data                   \
)                                     \
    (cPtr->fixedPoints) = (data)

#define AbsVertexCatalogSetBooleanOps(\
  /* AbsVertexCatalog_t * */ cPtr,    \
  /* lsList */ data                   \
)                                     \
    (cPtr->booleanOps) = (data)

#define AbsVertexCatalogSetNegations(\
  /* AbsVertexCatalog_t * */ cPtr,   \
  /* lsList */ data                  \
)                                    \
    (cPtr->negations) = (data)

#define AbsVertexCatalogSetPreImages(\
  /* AbsVertexCatalog_t * */ cPtr,  \
  /* lsList */ data                 \
)                                   \
    (cPtr->preImages) = (data)

#define AbsVertexCatalogSetIdentifiers(\
  /* AbsVertexCatalog_t * */ cPtr,     \
  /* lsList */ data                    \
)                                      \
    (cPtr->identifiers) = (data)

#define AbsVertexCatalogSetVariables(\
  /* AbsVertexCatalog_t * */ cPtr,   \
  /* lsList */ data                  \
)                                    \
    (cPtr->variables) = (data)

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

static AbsVertexInfo_t * LookUpBooleanOp(lsList vertexList, AbsVertex_t type, boolean polarity, AbsVertexInfo_t *leftKid, AbsVertexInfo_t *rightKid);
static AbsVertexInfo_t * LookUpFixedPoint(lsList vertexList, boolean polarity, AbsVertexInfo_t *leftKid, int localId);
static AbsVertexInfo_t * LookUpIdentifier(lsList vertexList, boolean polarity, char *name, char *value);
static AbsVertexInfo_t * LookUpPreImage(lsList vertexList, boolean polarity, AbsVertexInfo_t *leftKid);
static AbsVertexInfo_t * LookUpVariable(lsList vertexList, boolean polarity, int localId);

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

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

AbsVertexCatalog_t *
AbsVertexCatalogInitialize(void)
{
  AbsVertexCatalog_t *result;

  result = ALLOC(AbsVertexCatalog_t, 1);

  AbsVertexCatalogSetFixedPoints(result, lsCreate());
  AbsVertexCatalogSetBooleanOps(result, lsCreate());
  AbsVertexCatalogSetNegations(result, lsCreate());
  AbsVertexCatalogSetPreImages(result, lsCreate());
  AbsVertexCatalogSetIdentifiers(result, lsCreate());
  AbsVertexCatalogSetVariables(result, lsCreate());

  return result;
} /* End of AbsVertexCatalogInitialize */

void
AbsVertexCatalogFree(
  AbsVertexCatalog_t *c)
{
  lsDestroy(AbsVertexCatalogReadFixedPoints(c), (void (*)(lsGeneric))0);
  lsDestroy(AbsVertexCatalogReadBooleanOps(c), (void (*)(lsGeneric))0);
  lsDestroy(AbsVertexCatalogReadNegations(c), (void (*)(lsGeneric))0);
  lsDestroy(AbsVertexCatalogReadPreImages(c), (void (*)(lsGeneric))0);
  lsDestroy(AbsVertexCatalogReadIdentifiers(c), (void (*)(lsGeneric))0);
  lsDestroy(AbsVertexCatalogReadVariables(c), (void (*)(lsGeneric))0);

  FREE(c);

  return;
} /* End of AbsVertexCatalogFree */

AbsVertexInfo_t *
AbsVertexCatalogFindOrAdd(
  AbsVertexCatalog_t *catalog,
  AbsVertex_t type,
  boolean polarity,
  AbsVertexInfo_t *leftKid,
  AbsVertexInfo_t *rightKid,
  int localId,
  char *idName,
  char *idValue
)
{
  if (type == fixedPoint_c) {
    return LookUpFixedPoint(AbsVertexCatalogReadFixedPoints(catalog),
                            polarity, leftKid, localId);
  }

  if (type == and_c || type == xor_c || type == xnor_c) {
    return LookUpBooleanOp(AbsVertexCatalogReadBooleanOps(catalog),
                           type, polarity, leftKid, rightKid);
  }

  if (type == not_c) {
    return LookUpPreImage(AbsVertexCatalogReadNegations(catalog),
                          polarity, leftKid);
  }

  if (type == preImage_c) {
    return LookUpPreImage(AbsVertexCatalogReadPreImages(catalog),
                          polarity, leftKid);
  }

  if (type == identifier_c) {
    return LookUpIdentifier(AbsVertexCatalogReadIdentifiers(catalog),
                            polarity, idName, idValue);
  }

  if (type == variable_c) {
    return LookUpVariable(AbsVertexCatalogReadVariables(catalog),
                          polarity, localId);
  }

  (void) fprintf(vis_stderr, "** abs error: Unknown vertex type in function ");
  (void) fprintf(vis_stderr, "AbsVertexCatalogFindOrAdd.\n");

  return NIL(AbsVertexInfo_t);

} /* End of AbsVertexCatalogFindOrAdd */

void
AbsCatalogDelete(
  AbsVertexCatalog_t *catalog,
  AbsVertexInfo_t *vertex)
{
  AbsVertex_t type;
  AbsVertexInfo_t *result;
  lsList vertexList;
  lsGen listGen;
  lsHandle item;
  lsGeneric userData;

  vertexList = 0;
  type = AbsVertexReadType(vertex);

  /* Select the proper list from the catalog */
  if (type == fixedPoint_c) {
    vertexList = AbsVertexCatalogReadFixedPoints(catalog);
  }

  if (type == and_c || type == xor_c || type == xnor_c) {
    vertexList = AbsVertexCatalogReadBooleanOps(catalog);
  }

  if (type == not_c) {
    vertexList = AbsVertexCatalogReadNegations(catalog);
  }

  if (type == preImage_c) {
    vertexList = AbsVertexCatalogReadPreImages(catalog);
  }

  if (type == identifier_c) {
    vertexList = AbsVertexCatalogReadIdentifiers(catalog);
  }

  if (type == variable_c) {
    vertexList = AbsVertexCatalogReadVariables(catalog);
  }
  
  listGen = lsStart(vertexList);
  while(lsNext(listGen, &result, &item) == LS_OK) {
    if (result == vertex) {
      lsRemoveItem(item, &userData);
      assert(vertex == (AbsVertexInfo_t *)userData);
      lsFinish(listGen);
      return;
    }
  }

  (void) fprintf(vis_stderr, "** abs error: Removing non-existent vertex from");
  (void) fprintf(vis_stderr, " catalog\n");

  return;
} /* End of AbsCatalogDelete */

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

static AbsVertexInfo_t *
LookUpBooleanOp(
  lsList vertexList,
  AbsVertex_t type,
  boolean polarity,
  AbsVertexInfo_t *leftKid,
  AbsVertexInfo_t *rightKid)
{
  lsGen listGen;
  AbsVertexInfo_t *result;

  /* Start the generator and traverse the list */
  listGen = lsStart(vertexList);
  while(lsNext(listGen, &result, NIL(lsHandle)) == LS_OK) {
    if (AbsVertexReadType(result) == type &&
        AbsVertexReadLeftKid(result) == leftKid &&
        AbsVertexReadRightKid(result) == rightKid &&
        AbsVertexReadPolarity(result) == polarity) {
      AbsVertexReadRefs(result)++;
      lsFinish(listGen);
      return result;
    }
  }

  /* Item has not been found */
  lsFinish(listGen);
  result = AbsVertexInitialize();
  lsNewBegin(vertexList, (lsGeneric)result, NIL(lsHandle));

  return result;
} /* End of LookUpBooleanOp */

static AbsVertexInfo_t *
LookUpFixedPoint(
  lsList vertexList,
  boolean polarity,
  AbsVertexInfo_t *leftKid,
  int localId)
{
  lsGen listGen;
  AbsVertexInfo_t *result;

  /* Start the generator and traverse the list */
  listGen = lsStart(vertexList);
  while(lsNext(listGen, &result, NIL(lsHandle)) == LS_OK) {
    if (AbsVertexReadLeftKid(result) == leftKid &&
        AbsVertexReadPolarity(result) == polarity &&
        AbsVertexReadVarId(AbsVertexReadFpVar(result)) == localId) {
      AbsVertexReadRefs(result)++;
      lsFinish(listGen);
      return result;
    }
  }

  /* Item has not been found */
  lsFinish(listGen);
  result = AbsVertexInitialize();
  lsNewBegin(vertexList, (lsGeneric)result, NIL(lsHandle));

  return result;
} /* End of LookUpFixedPoint */

static AbsVertexInfo_t *
LookUpIdentifier(
  lsList vertexList,
  boolean polarity,
  char *name,
  char *value)
{
  lsGen listGen;
  AbsVertexInfo_t *result;

  /* Start the generator and traverse the list */
  listGen = lsStart(vertexList);
  while(lsNext(listGen, &result, NIL(lsHandle)) == LS_OK) {
    if (AbsVertexReadPolarity(result) == polarity &&
        strcmp(AbsVertexReadName(result), name) == 0 && 
        strcmp(AbsVertexReadValue(result), value) == 0) {
      AbsVertexReadRefs(result)++;
      lsFinish(listGen);
      return result;
    }
  }

  /* Item has not been found */
  lsFinish(listGen);
  result = AbsVertexInitialize();
  lsNewBegin(vertexList, (lsGeneric)result, NIL(lsHandle));

  return result;
} /* End of LookUpIdentifier */

static AbsVertexInfo_t *
LookUpPreImage(
  lsList vertexList,
  boolean polarity,
  AbsVertexInfo_t *leftKid)
{
  lsGen listGen;
  AbsVertexInfo_t *result;

  /* Start the generator and traverse the list */
  listGen = lsStart(vertexList);
  while(lsNext(listGen, &result, NIL(lsHandle)) == LS_OK) {
    if (AbsVertexReadLeftKid(result) == leftKid &&
        AbsVertexReadPolarity(result) == polarity) {
      AbsVertexReadRefs(result)++;
      lsFinish(listGen);
      return result;
    }
  }

  /* Item has not been found */
  lsFinish(listGen);
  result = AbsVertexInitialize();
  lsNewBegin(vertexList, (lsGeneric)result, NIL(lsHandle));

  return result;
} /* End of LookUpPreImage */

static AbsVertexInfo_t *
LookUpVariable(
  lsList vertexList,
  boolean polarity,
  int localId)
{
  lsGen listGen;
  AbsVertexInfo_t *result;

  /* Start the generator and traverse the list */
  listGen = lsStart(vertexList);
  while(lsNext(listGen, &result, NIL(lsHandle)) == LS_OK) {
    if (AbsVertexReadPolarity(result) == polarity &&
        AbsVertexReadVarId(result) == localId) {
      AbsVertexReadRefs(result)++;
      lsFinish(listGen);
      return result;
    }
  }

  /* Item has not been found */
  lsFinish(listGen);
  result = AbsVertexInitialize();
  lsNewBegin(vertexList, (lsGeneric)result, NIL(lsHandle));

  return result;
} /* End of LookUpVariable */