src/calBdd/calAssociation.c File Reference

#include "calInt.h"

Include dependency graph for calAssociation.c:

Go to the source code of this file.

Functions
static int	AssociationIsEqual (Cal_BddManager_t *bddManager, Cal_Bdd_t *p, Cal_Bdd_t *q)
static int	CheckAssoc (Cal_BddManager_t *bddManager, Cal_Bdd *assocInfo, int pairs)
int	Cal_AssociationInit (Cal_BddManager bddManager, Cal_Bdd *associationInfoUserBdds, int pairs)
void	Cal_AssociationQuit (Cal_BddManager bddManager, int associationId)
int	Cal_AssociationSetCurrent (Cal_BddManager bddManager, int associationId)
void	Cal_TempAssociationAugment (Cal_BddManager bddManager, Cal_Bdd *associationInfoUserBdds, int pairs)
void	Cal_TempAssociationInit (Cal_BddManager bddManager, Cal_Bdd *associationInfoUserBdds, int pairs)
void	Cal_TempAssociationQuit (Cal_BddManager bddManager)
void	CalAssociationListFree (Cal_BddManager_t *bddManager)
void	CalVarAssociationRepackUpdate (Cal_BddManager_t *bddManager, Cal_BddId_t id)
void	CalCheckAssociationValidity (Cal_BddManager_t *bddManager)
void	CalReorderAssociationFix (Cal_BddManager_t *bddManager)

---

Function Documentation

static int AssociationIsEqual	(	Cal_BddManager_t *	bddManager,
		Cal_Bdd_t *	p,
		Cal_Bdd_t *	q
	)			[static]

CFile***********************************************************************

FileName [calAssociation.c]

PackageName [cal]

Synopsis [Contains the routines related to the variable association.]

Description [optional]

SeeAlso [optional]

Author [Rajeev K. Ranjan (rajeev@eecs.berkeley.edu) Jagesh Sanghavi (sanghavi@eecs.berkeley.edu) ]

Copyright [Copyright (c) 1994-1996 The Regents of the Univ. of California. All rights reserved.

Permission is hereby granted, without written agreement and without license or royalty fees, to use, copy, modify, and distribute this software and its documentation for any purpose, provided that the above copyright notice and the following two paragraphs appear in all copies of this software.

IN NO EVENT SHALL THE UNIVERSITY OF CALIFORNIA BE LIABLE TO ANY PARTY FOR DIRECT, INDIRECT, SPECIAL, INCIDENTAL, OR CONSEQUENTIAL DAMAGES ARISING OUT OF THE USE OF THIS SOFTWARE AND ITS DOCUMENTATION, EVEN IF THE UNIVERSITY OF CALIFORNIA HAS BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.

THE UNIVERSITY OF CALIFORNIA SPECIFICALLY DISCLAIMS ANY WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE. THE SOFTWARE PROVIDED HEREUNDER IS ON AN "AS IS" BASIS, AND THE UNIVERSITY OF CALIFORNIA HAS NO OBLIGATION TO PROVIDE MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR MODIFICATIONS.]

Revision [

Id

calAssociation.c,v 1.1.1.3 1998/05/04 00:58:50 hsv Exp

]AutomaticStart

Function********************************************************************

Synopsis [Checks for equality of two associations]

Description [Checks for equality of two associations]

SideEffects [None]

Definition at line 560 of file calAssociation.c.

{
  int i;
  for(i = 1; i <= bddManager->maxNumVars; i++){
    if(CalBddIsEqual(p[i], q[i]) == 0){
      return (0);
    }
  }
  return (1);
}

int Cal_AssociationInit	(	Cal_BddManager	bddManager,
		Cal_Bdd *	associationInfoUserBdds,
		int	pairs
	)

AutomaticEnd Function********************************************************************

Synopsis [Creates or finds a variable association.]

Description [Creates or finds a variable association. The association is specified by associationInfo, which is a an array of BDD with Cal_BddNull(bddManager) as the end marker. If pairs is 0, the array is assumed to be an array of variables. In this case, each variable is paired with constant BDD one. Such an association may viewed as specifying a set of variables for use with routines such as Cal_BddExists. If pair is not 0, then the even numbered array elements should be variables and the odd numbered elements should be the BDDs which they are mapped to. In both cases, the return value is an integer identifier for this association. If the given association is equivalent to one which already exists, the same identifier is used for both, and the reference count of the association is increased by one.]

SideEffects [None]

SeeAlso [Cal_AssociationQuit]

Definition at line 106 of file calAssociation.c.

{
  int i, numAssociations;
  CalAssociation_t *p, **q;
  Cal_Bdd_t f;
  Cal_Bdd_t *varAssociation;
  Cal_BddId_t j;
  long last;
  Cal_Bdd_t *associationInfo;
  
  if (!CheckAssoc(bddManager, associationInfoUserBdds, pairs)){
    return (-1);
  }


/* First count the number of elements */
  for (i=0; associationInfoUserBdds[i]; i++);
  if (pairs)  numAssociations = i/2;
  else numAssociations = i;
  associationInfo = Cal_MemAlloc(Cal_Bdd_t, i+1);
  for (j=0; j < i; j++){
    associationInfo[j] =
        CalBddGetInternalBdd(bddManager,associationInfoUserBdds[j]);
  }
  associationInfo[j] = bddManager->bddNull;

  
  varAssociation = Cal_MemAlloc(Cal_Bdd_t, bddManager->maxNumVars+1);
  for(i = 0; i <= bddManager->maxNumVars; i++){
    varAssociation[i] = bddManager->bddNull;
  }

  
  if(pairs){
    for(i = 0; i < numAssociations; i++){
      f = associationInfo[(i<<1)];
      varAssociation[CalBddGetBddId(f)] = associationInfo[(i<<1)+1];
    }
  }
  else{
    for(i = 0; i < numAssociations; i++){
      f=associationInfo[i];
      varAssociation[CalBddGetBddId(f)] = CalBddOne(bddManager);
    }
  }
  /* Check for existence. */
  for(p = bddManager->associationList; p; p = p->next){
    if(AssociationIsEqual(bddManager, p->varAssociation, varAssociation)){
        Cal_MemFree(varAssociation);
    Cal_MemFree(associationInfo);
        p->refCount++;
        return (p->id);
    }
  }
  /* Find the first unused id. */
  for(q = &bddManager->associationList, p = *q, i = 0;
      p && p->id == i; q = &p->next, p = *q, ++i){
  }
  /*p = Cal_MemAlloc(CalAssociation_t, 1);*/
  /*p = CAL_BDD_NEW_REC(bddManager, CalAssociation_t);*/
  p = Cal_MemAlloc(CalAssociation_t, 1);
  p->id = i;
  p->next = *q;
  *q = p;
  p->varAssociation = varAssociation;
  last = -1;
  if(pairs){
    for(i = 0; i < numAssociations; i++){
      f = associationInfo[(i<<1)];
      j = CalBddGetBddIndex(bddManager, f);
      if((long)j > last){
          last = j;
      }
    }
  }
  else{
    for(i = 0; i < numAssociations; i++){
      f = associationInfo[i];
      j = CalBddGetBddIndex(bddManager, f);
      if((long)j > last){
          last = j;
      }
    }
  }
  p->lastBddIndex = last;
  p->refCount = 1;
  /* Protect BDDs in the association. */
  if(pairs){
    for(i = 0; i < numAssociations; i++){
      f = associationInfo[(i<<1)+1];
      CalBddIcrRefCount(f);
    }
  }
  Cal_MemFree(associationInfo);
  return p->id;
}

void Cal_AssociationQuit	(	Cal_BddManager	bddManager,
		int	associationId
	)

Function********************************************************************

Synopsis [Deletes the variable association given by id]

Description [Decrements the reference count of the variable association with identifier id, and frees it if the reference count becomes zero.]

SideEffects [None]

SeeAlso [Cal_AssociationInit]

Definition at line 219 of file calAssociation.c.

{
  Cal_BddId_t i;
  Cal_Bdd_t f;
  CalAssociation_t *p, **q;

  if(bddManager->currentAssociation->id == associationId){
    bddManager->currentAssociation = bddManager->tempAssociation;
  }
  for(q = &bddManager->associationList, p = *q; p; q = &p->next, p = *q){
    if(p->id == associationId){
      p->refCount--;
      if(!p->refCount){
        /* Unprotect the BDDs in the association. */
        for(i = 1; i <= bddManager->numVars; i++){
          f = p->varAssociation[i];
          if(!CalBddIsBddNull(bddManager, f)){
            CalBddDcrRefCount(f);
          }
        }
        *q = p->next;
        Cal_MemFree(p->varAssociation);
        /*CAL_BDD_FREE_REC(bddManager, p, CalAssociation_t);*/
        Cal_MemFree(p);
        CalCacheTableTwoFlushAssociationId(bddManager, associationId);
      }
      return;
    }
  }
  CalBddWarningMessage("Cal_AssociationQuit: no association with specified ID");
}

int Cal_AssociationSetCurrent	(	Cal_BddManager	bddManager,
		int	associationId
	)

Function********************************************************************

Synopsis [Sets the current variable association to the one given by id and returns the ID of the old association.]

Description [Sets the current variable association to the one given by id and returns the ID of the old association. An id of -1 indicates the temporary association]

SideEffects [None]

Definition at line 264 of file calAssociation.c.

{
  int oldAssociationId;
  CalAssociation_t *p;

  oldAssociationId = bddManager->currentAssociation->id;
  if(associationId != -1){
    for(p = bddManager->associationList; p; p = p->next){
      if(p->id == associationId){
        bddManager->currentAssociation = p;
        return (oldAssociationId);
      }
    }
    CalBddWarningMessage(
        "Cal_AssociationSetCurrent: no variable association with specified ID.\n May have been discarded during dynamic reordering.");
  }
  bddManager->currentAssociation = bddManager->tempAssociation;
  return oldAssociationId;
}

void Cal_TempAssociationAugment	(	Cal_BddManager	bddManager,
		Cal_Bdd *	associationInfoUserBdds,
		int	pairs
	)

Function********************************************************************

Synopsis [Adds to the temporary variable association.]

Description [Pairs is 0 if the information represents only a list of variables rather than a full association.]

SideEffects [None]

Definition at line 296 of file calAssociation.c.

{
  int i, j, numAssociations;
  Cal_Bdd_t f;
  long last;
  Cal_Bdd_t *associationInfo;
  
  if (CheckAssoc(bddManager, associationInfoUserBdds, pairs) == 0) {
    return;
  }

  /*while (associationInfoUserBdds[i++]);*/
  for (i=0; associationInfoUserBdds[i]; i++);
  if (pairs) numAssociations = i/2;
  else numAssociations = i;
  associationInfo = Cal_MemAlloc(Cal_Bdd_t, i+1);
  for (j=0; j < i; j++){
    associationInfo[j] =
        CalBddGetInternalBdd(bddManager,associationInfoUserBdds[j]);
  }
  associationInfo[j] = bddManager->bddNull;
  
  last = bddManager->tempAssociation->lastBddIndex;
  if(pairs){
    for(i = 0; i < numAssociations; i++){
      f = associationInfo[(i<<1)];
      j = CalBddGetBddId(f);
      if(bddManager->idToIndex[j] > last){
        last = bddManager->idToIndex[j];
      }
      f = bddManager->tempAssociation->varAssociation[j];
      if(!CalBddIsBddNull(bddManager, f)){
        CalBddDcrRefCount(f);
      }
      f = associationInfo[(i<<1)+1];
      bddManager->tempAssociation->varAssociation[j] = f;
      /* Protect BDDs in the association. */
      CalBddIcrRefCount(f);
    }
  }
  else{
    for(i = 0; i < numAssociations; i++){
      f = associationInfo[i];
      j = CalBddGetBddId(f);
      if(bddManager->idToIndex[j] > last){
        last = bddManager->idToIndex[j];
      }
      f = bddManager->tempAssociation->varAssociation[j];
      if(!CalBddIsBddNull(bddManager, f)){
        CalBddDcrRefCount(f);
      }
      bddManager->tempAssociation->varAssociation[j] = CalBddOne(bddManager);
    } 
  }
  bddManager->tempAssociation->lastBddIndex = last;
  Cal_MemFree(associationInfo);
}

void Cal_TempAssociationInit	(	Cal_BddManager	bddManager,
		Cal_Bdd *	associationInfoUserBdds,
		int	pairs
	)

Function********************************************************************

Synopsis [Sets the temporary variable association.]

Description [Pairs is 0 if the information represents only a list of variables rather than a full association.]

SideEffects [None]

Definition at line 369 of file calAssociation.c.

{
  long i;
  Cal_Bdd_t f;

  /* Clean up old temporary association. */
  for(i = 1; i <= bddManager->numVars; i++){
    f = bddManager->tempAssociation->varAssociation[i];
    if(!CalBddIsBddNull(bddManager, f)){
      CalBddDcrRefCount(f);
      bddManager->tempAssociation->varAssociation[i] = bddManager->bddNull;
    }
  }
  bddManager->tempAssociation->lastBddIndex = -1;
  Cal_TempAssociationAugment(bddManager, associationInfoUserBdds, pairs);
}

void Cal_TempAssociationQuit

(

Cal_BddManager

bddManager

)

Function********************************************************************

Synopsis [Cleans up temporary association]

Description [Cleans up temporary associationoptional]

SideEffects [None]

Definition at line 398 of file calAssociation.c.

{
  int i;
  Cal_Bdd_t f;

  /* Clean up old temporary association. */
  for(i = 1; i <= bddManager->numVars; i++){
    f = bddManager->tempAssociation->varAssociation[i];
    if(!CalBddIsBddNull(bddManager, f)){
      CalBddDcrRefCount(f);
      bddManager->tempAssociation->varAssociation[i] = bddManager->bddNull;
    }
  }
  bddManager->tempAssociation->lastBddIndex = -1;
}

void CalAssociationListFree

(

Cal_BddManager_t *

bddManager

)

Function********************************************************************

Synopsis [Frees the variable associations]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 431 of file calAssociation.c.

{
  CalAssociation_t *assoc, *nextAssoc;
  
  for(assoc = bddManager->associationList;
      assoc != Cal_Nil(CalAssociation_t); assoc = nextAssoc){
    nextAssoc = assoc->next;
    Cal_MemFree(assoc->varAssociation);
    /*CAL_BDD_FREE_REC(bddManager, assoc, CalAssociation_t);*/
    Cal_MemFree(assoc);
  }
}

void CalCheckAssociationValidity

(

Cal_BddManager_t *

bddManager

)

Function********************************************************************

Synopsis [Checks the validity of association.]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 492 of file calAssociation.c.

{
  CalAssociation_t *assoc, *nextAssoc;
  int i;
  
  for(assoc = bddManager->associationList;
      assoc != Cal_Nil(CalAssociation_t); assoc = nextAssoc){
    nextAssoc = assoc->next;
    for (i=1; i <= bddManager->numVars; i++){
      Cal_Assert(CalBddIsForwarded(assoc->varAssociation[i]) == 0);
    }
  }
  /* temporary association */
  assoc = bddManager->tempAssociation;
  for (i=1; i <= bddManager->numVars; i++){
    Cal_Assert(CalBddIsForwarded(assoc->varAssociation[i]) == 0);
  }
}

void CalReorderAssociationFix

(

Cal_BddManager_t *

bddManager

)

Function********************************************************************

Synopsis [required]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 523 of file calAssociation.c.

{
  CalAssociation_t *assoc, *nextAssoc;
  int i;
  
  for(assoc = bddManager->associationList;
      assoc != Cal_Nil(CalAssociation_t); assoc = nextAssoc){
    nextAssoc = assoc->next;
    for (i=1; i <= bddManager->numVars; i++){
        if (CalBddGetBddId(assoc->varAssociation[i]) != CAL_BDD_NULL_ID){
            CalBddIsForwardedTo(assoc->varAssociation[i]);
        }
    }
  }
  /* fix temporary association */
  assoc = bddManager->tempAssociation;
  for (i=1; i <= bddManager->numVars; i++){
      if (CalBddGetBddId(assoc->varAssociation[i]) != CAL_BDD_NULL_ID){
          CalBddIsForwardedTo(assoc->varAssociation[i]);
      }
  }
}

void CalVarAssociationRepackUpdate	(	Cal_BddManager_t *	bddManager,
		Cal_BddId_t	id
	)

Function********************************************************************

Synopsis [Need to be called after repacking.]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 456 of file calAssociation.c.

{
  CalAssociation_t *assoc, *nextAssoc;
  int i;
  
  for(assoc = bddManager->associationList;
      assoc != Cal_Nil(CalAssociation_t); assoc = nextAssoc){
    nextAssoc = assoc->next;
    for (i=1; i <= bddManager->numVars; i++){
      if (CalBddGetBddId(assoc->varAssociation[i]) == id){
        CalBddForward(assoc->varAssociation[i]);
      }
    }
  }
  /* fix temporary association */
  assoc = bddManager->tempAssociation;
  for (i=1; i <= bddManager->numVars; i++){
    if (CalBddGetBddId(assoc->varAssociation[i]) == id){
      CalBddForward(assoc->varAssociation[i]);
    }
  }
}

static int CheckAssoc	(	Cal_BddManager_t *	bddManager,
		Cal_Bdd *	assocInfo,
		int	pairs
	)			[static]

Function********************************************************************

Synopsis [required]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 585 of file calAssociation.c.

{
  CalBddArrayPreProcessing(bddManager, assocInfo);
  if (pairs){
    while (assocInfo[0] && assocInfo[1]){
      if (CalBddTypeAux(bddManager,
                        CalBddGetInternalBdd(bddManager, assocInfo[0])) !=
          CAL_BDD_TYPE_POSVAR){  
            CalBddWarningMessage("CheckAssoc: first element in pair is not a positive variable"); 
            return (0);
          }
      assocInfo+=2;
    }
  }
  return (1);
}