本文整理汇总了C++中cuddDynamicAllocNode函数的典型用法代码示例。如果您正苦于以下问题:C++ cuddDynamicAllocNode函数的具体用法?C++ cuddDynamicAllocNode怎么用?C++ cuddDynamicAllocNode使用的例子?那么恭喜您, 这里精选的函数代码示例或许可以为您提供帮助。
在下文中一共展示了cuddDynamicAllocNode函数的14个代码示例,这些例子默认根据受欢迎程度排序。您可以为喜欢或者感觉有用的代码点赞,您的评价将有助于我们的系统推荐出更棒的C++代码示例。
示例1: cuddZddUndoMoves
/**Function********************************************************************
Synopsis [Given a set of moves, returns the ZDD heap to the order
in effect before the moves.]
Description [Given a set of moves, returns the ZDD heap to the
order in effect before the moves. Returns 1 in case of success;
0 otherwise.]
SideEffects [None]
******************************************************************************/
static Move*
cuddZddUndoMoves(
DdManager * table,
Move * moves)
{
Move *invmoves = NULL;
Move *move;
Move *invmove;
int size;
for (move = moves; move != NULL; move = move->next) {
invmove = (Move *) cuddDynamicAllocNode(table);
if (invmove == NULL) goto cuddZddUndoMovesOutOfMem;
invmove->x = move->x;
invmove->y = move->y;
invmove->next = invmoves;
invmoves = invmove;
if (move->flags == CUDD_SWAP_MOVE) {
invmove->flags = CUDD_SWAP_MOVE;
size = cuddZddSwapInPlace(table,(int)move->x,(int)move->y);
if (!size) goto cuddZddUndoMovesOutOfMem;
} else if (move->flags == CUDD_LINEAR_TRANSFORM_MOVE) {
invmove->flags = CUDD_INVERSE_TRANSFORM_MOVE;
size = cuddZddLinearInPlace(table,(int)move->x,(int)move->y);
if (!size) goto cuddZddUndoMovesOutOfMem;
size = cuddZddSwapInPlace(table,(int)move->x,(int)move->y);
if (!size) goto cuddZddUndoMovesOutOfMem;
} else { /* must be CUDD_INVERSE_TRANSFORM_MOVE */
#ifdef DD_DEBUG
(void) fprintf(table->err,"Unforseen event in ddUndoMoves!\n");
#endif
invmove->flags = CUDD_LINEAR_TRANSFORM_MOVE;
size = cuddZddSwapInPlace(table,(int)move->x,(int)move->y);
if (!size) goto cuddZddUndoMovesOutOfMem;
size = cuddZddLinearInPlace(table,(int)move->x,(int)move->y);
if (!size) goto cuddZddUndoMovesOutOfMem;
}
invmove->size = size;
}
return(invmoves);
cuddZddUndoMovesOutOfMem:
while (invmoves != NULL) {
move = invmoves->next;
cuddDeallocMove(table, invmoves);
invmoves = move;
}
return((Move *) CUDD_OUT_OF_MEM);
} /* end of cuddZddUndoMoves */
开发者ID:hugopaquet,项目名称:mcmas-sdds,代码行数:63,代码来源:cuddZddLin.c
示例2: bound
/**Function********************************************************************
Synopsis [Sifts a variable down.]
Description [Sifts a variable down. Moves x down until either it
reaches the bound (x_high) or the size of the ZDD heap increases too
much. Returns the set of moves in case of success; NULL if memory is
full.]
SideEffects [None]
SeeAlso []
******************************************************************************/
static Move *
cuddZddSiftingDown(
DdManager * table,
int x,
int x_high,
int initial_size)
{
Move *moves;
Move *move;
int y;
int size;
int limit_size = initial_size;
moves = NULL;
y = cuddZddNextHigh(table, x);
while (y <= x_high) {
size = cuddZddSwapInPlace(table, x, y);
if (size == 0)
goto cuddZddSiftingDownOutOfMem;
move = (Move *)cuddDynamicAllocNode(table);
if (move == NULL)
goto cuddZddSiftingDownOutOfMem;
move->x = x;
move->y = y;
move->size = size;
move->next = moves;
moves = move;
if ((double)size > (double)limit_size * table->maxGrowth)
break;
if (size < limit_size)
limit_size = size;
x = y;
y = cuddZddNextHigh(table, x);
}
return(moves);
cuddZddSiftingDownOutOfMem:
while (moves != NULL) {
move = moves->next;
cuddDeallocNode(table, (DdNode *)moves);
moves = move;
}
return(NULL);
} /* end of cuddZddSiftingDown */
开发者ID:saidalfaraby,项目名称:DTP4TC,代码行数:61,代码来源:cuddZddReord.c
示例3: ddJumpingUp
/**Function********************************************************************
Synopsis [This function is for jumping up.]
Description [This is a simplified version of ddSiftingUp. It does not
use lower bounding. Returns the set of moves in case of success; NULL
if memory is full.]
SideEffects [None]
SeeAlso []
******************************************************************************/
static Move *
ddJumpingUp(
DdManager * table,
int x,
int x_low,
int initial_size)
{
Move *moves;
Move *move;
int y;
int size;
int limit_size = initial_size;
moves = NULL;
y = cuddNextLow(table,x);
while (y >= x_low) {
size = cuddSwapInPlace(table,y,x);
if (size == 0) goto ddJumpingUpOutOfMem;
move = (Move *)cuddDynamicAllocNode(table);
if (move == NULL) goto ddJumpingUpOutOfMem;
move->x = y;
move->y = x;
move->size = size;
move->next = moves;
moves = move;
if ((double) size > table->maxGrowth * (double) limit_size) {
break;
} else if (size < limit_size) {
limit_size = size;
}
x = y;
y = cuddNextLow(table,x);
}
return(moves);
ddJumpingUpOutOfMem:
while (moves != NULL) {
move = moves->next;
cuddDeallocNode(table, (DdNode *) moves);
moves = move;
}
return(NULL);
} /* end of ddJumpingUp */
开发者ID:ansonn,项目名称:esl_systemc,代码行数:57,代码来源:cuddAnneal.c
示例4: zdd_group_move
/**Function********************************************************************
Synopsis [Swaps two groups.]
Description [Swaps two groups. x is assumed to be the bottom variable
of the first group. y is assumed to be the top variable of the second
group. Updates the list of moves. Returns the number of keys in the
table if successful; 0 otherwise.]
SideEffects [None]
SeeAlso []
******************************************************************************/
static int
zdd_group_move(
DdManager * table,
int x,
int y,
Move ** moves)
{
Move *move;
int size;
int i, temp, gxtop, gxbot, gybot, yprev;
int swapx, swapy;
/* NuSMV: add begin */
swapy = 0;
swapx = 0;
/* NuSMV: add end */
#ifdef DD_DEBUG
assert(x < y); /* we assume that x < y */
#endif
/* Find top and bottom for the two groups. */
gxtop = table->subtableZ[x].next;
gxbot = x;
gybot = table->subtableZ[y].next;
while (table->subtableZ[gybot].next != (unsigned) y)
gybot = table->subtableZ[gybot].next;
yprev = gybot;
while (x <= y) {
while (y > gxtop) {
/* Set correct symmetries. */
temp = table->subtableZ[x].next;
if (temp == x)
temp = y;
i = gxtop;
for (;;) {
if (table->subtableZ[i].next == (unsigned) x) {
table->subtableZ[i].next = y;
break;
} else {
i = table->subtableZ[i].next;
}
}
if (table->subtableZ[y].next != (unsigned) y) {
table->subtableZ[x].next = table->subtableZ[y].next;
} else {
table->subtableZ[x].next = x;
}
if (yprev != y) {
table->subtableZ[yprev].next = x;
} else {
yprev = x;
}
table->subtableZ[y].next = temp;
size = cuddZddSwapInPlace(table, x, y);
if (size == 0)
goto zdd_group_moveOutOfMem;
swapx = x;
swapy = y;
y = x;
x--;
} /* while y > gxtop */
/* Trying to find the next y. */
if (table->subtableZ[y].next <= (unsigned) y) {
gybot = y;
} else {
y = table->subtableZ[y].next;
}
yprev = gxtop;
gxtop++;
gxbot++;
x = gxbot;
} /* while x <= y, end of group movement */
move = (Move *)cuddDynamicAllocNode(table);
if (move == NULL)
goto zdd_group_moveOutOfMem;
move->x = swapx;
move->y = swapy;
move->size = table->keysZ;
move->next = *moves;
*moves = move;
//.........这里部分代码省略.........
开发者ID:ancailliau,项目名称:pynusmv,代码行数:101,代码来源:cuddZddSymm.c
示例5: bound
/**Function********************************************************************
Synopsis [Moves x down until either it reaches the bound (x_high) or
the size of the ZDD heap increases too much.]
Description [Moves x down until either it reaches the bound (x_high)
or the size of the ZDD heap increases too much. Assumes that x is the
bottom of a symmetry group. Checks x for symmetry to the adjacent
variables. If symmetry is found, the symmetry group of x is merged
with the symmetry group of the other variable. Returns the set of
moves in case of success; ZDD_MV_OOM if memory is full.]
SideEffects [None]
SeeAlso []
******************************************************************************/
static Move *
cuddZddSymmSifting_down(
DdManager * table,
int x,
int x_high,
int initial_size)
{
Move *moves;
Move *move;
int y;
int size;
int limit_size = initial_size;
int i, gxtop, gybot;
moves = NULL;
y = cuddZddNextHigh(table, x);
while (y <= x_high) {
gybot = table->subtableZ[y].next;
while (table->subtableZ[gybot].next != (unsigned) y)
gybot = table->subtableZ[gybot].next;
if (cuddZddSymmCheck(table, x, y)) {
/* Symmetry found, attach symm groups */
gxtop = table->subtableZ[x].next;
table->subtableZ[x].next = y;
i = table->subtableZ[y].next;
while (table->subtableZ[i].next != (unsigned) y)
i = table->subtableZ[i].next;
table->subtableZ[i].next = gxtop;
}
else if ((table->subtableZ[x].next == (unsigned) x) &&
(table->subtableZ[y].next == (unsigned) y)) {
/* x and y have self symmetry */
size = cuddZddSwapInPlace(table, x, y);
if (size == 0)
goto cuddZddSymmSifting_downOutOfMem;
move = (Move *)cuddDynamicAllocNode(table);
if (move == NULL)
goto cuddZddSymmSifting_downOutOfMem;
move->x = x;
move->y = y;
move->size = size;
move->next = moves;
moves = move;
if ((double)size >
(double)limit_size * table->maxGrowth)
return(moves);
if (size < limit_size)
limit_size = size;
x = y;
y = cuddZddNextHigh(table, x);
}
else { /* Group move */
size = zdd_group_move(table, x, y, &moves);
if ((double)size >
(double)limit_size * table->maxGrowth)
return(moves);
if (size < limit_size)
limit_size = size;
}
x = gybot;
y = cuddZddNextHigh(table, x);
}
return(moves);
cuddZddSymmSifting_downOutOfMem:
while (moves != NULL) {
move = moves->next;
cuddDeallocMove(table, moves);
moves = move;
}
return(ZDD_MV_OOM);
} /* end of cuddZddSymmSifting_down */
开发者ID:ancailliau,项目名称:pynusmv,代码行数:91,代码来源:cuddZddSymm.c
示例6: exp
/**Function********************************************************************
Synopsis [This function is for exchanging two variables, x and y.]
Description [This is the same funcion as ddSwapping except for
comparison expression. Use probability function, exp(-size_change/temp).]
SideEffects [None]
SeeAlso []
******************************************************************************/
static int
ddExchange(
DdManager * table,
int x,
int y,
double temp)
{
Move *move,*moves;
int tmp;
int x_ref,y_ref;
int x_next,y_next;
int size, result;
int initial_size, limit_size;
x_ref = x;
y_ref = y;
x_next = cuddNextHigh(table,x);
y_next = cuddNextLow(table,y);
moves = NULL;
initial_size = limit_size = table->keys - table->isolated;
for (;;) {
if (x_next == y_next) {
size = cuddSwapInPlace(table,x,x_next);
if (size == 0) goto ddExchangeOutOfMem;
move = (Move *)cuddDynamicAllocNode(table);
if (move == NULL) goto ddExchangeOutOfMem;
move->x = x;
move->y = x_next;
move->size = size;
move->next = moves;
moves = move;
size = cuddSwapInPlace(table,y_next,y);
if (size == 0) goto ddExchangeOutOfMem;
move = (Move *)cuddDynamicAllocNode(table);
if (move == NULL) goto ddExchangeOutOfMem;
move->x = y_next;
move->y = y;
move->size = size;
move->next = moves;
moves = move;
size = cuddSwapInPlace(table,x,x_next);
if (size == 0) goto ddExchangeOutOfMem;
move = (Move *)cuddDynamicAllocNode(table);
if (move == NULL) goto ddExchangeOutOfMem;
move->x = x;
move->y = x_next;
move->size = size;
move->next = moves;
moves = move;
tmp = x;
x = y;
y = tmp;
} else if (x == y_next) {
size = cuddSwapInPlace(table,x,x_next);
if (size == 0) goto ddExchangeOutOfMem;
move = (Move *)cuddDynamicAllocNode(table);
if (move == NULL) goto ddExchangeOutOfMem;
move->x = x;
move->y = x_next;
move->size = size;
move->next = moves;
moves = move;
tmp = x;
x = y;
y = tmp;
} else {
size = cuddSwapInPlace(table,x,x_next);
if (size == 0) goto ddExchangeOutOfMem;
move = (Move *)cuddDynamicAllocNode(table);
if (move == NULL) goto ddExchangeOutOfMem;
move->x = x;
move->y = x_next;
move->size = size;
move->next = moves;
moves = move;
size = cuddSwapInPlace(table,y_next,y);
if (size == 0) goto ddExchangeOutOfMem;
move = (Move *)cuddDynamicAllocNode(table);
if (move == NULL) goto ddExchangeOutOfMem;
move->x = y_next;
move->y = y;
move->size = size;
move->next = moves;
moves = move;
x = x_next;
//.........这里部分代码省略.........
开发者ID:ansonn,项目名称:esl_systemc,代码行数:101,代码来源:cuddAnneal.c
示例7: zddSwapAny
/**Function********************************************************************
Synopsis [Swaps any two variables.]
Description [Swaps any two variables. Returns the set of moves.]
SideEffects [None]
SeeAlso []
******************************************************************************/
static Move *
zddSwapAny(
DdManager * table,
int x,
int y)
{
Move *move, *moves;
int tmp, size;
int x_ref, y_ref;
int x_next, y_next;
int limit_size;
if (x > y) { /* make x precede y */
tmp = x; x = y; y = tmp;
}
x_ref = x; y_ref = y;
x_next = cuddZddNextHigh(table, x);
y_next = cuddZddNextLow(table, y);
moves = NULL;
limit_size = table->keysZ;
for (;;) {
if (x_next == y_next) { /* x < x_next = y_next < y */
size = cuddZddSwapInPlace(table, x, x_next);
if (size == 0)
goto zddSwapAnyOutOfMem;
move = (Move *) cuddDynamicAllocNode(table);
if (move == NULL)
goto zddSwapAnyOutOfMem;
move->x = x;
move->y = x_next;
move->size = size;
move->next = moves;
moves = move;
size = cuddZddSwapInPlace(table, y_next, y);
if (size == 0)
goto zddSwapAnyOutOfMem;
move = (Move *)cuddDynamicAllocNode(table);
if (move == NULL)
goto zddSwapAnyOutOfMem;
move->x = y_next;
move->y = y;
move->size = size;
move->next = moves;
moves = move;
size = cuddZddSwapInPlace(table, x, x_next);
if (size == 0)
goto zddSwapAnyOutOfMem;
move = (Move *)cuddDynamicAllocNode(table);
if (move == NULL)
goto zddSwapAnyOutOfMem;
move->x = x;
move->y = x_next;
move->size = size;
move->next = moves;
moves = move;
tmp = x; x = y; y = tmp;
} else if (x == y_next) { /* x = y_next < y = x_next */
size = cuddZddSwapInPlace(table, x, x_next);
if (size == 0)
goto zddSwapAnyOutOfMem;
move = (Move *)cuddDynamicAllocNode(table);
if (move == NULL)
goto zddSwapAnyOutOfMem;
move->x = x;
move->y = x_next;
move->size = size;
move->next = moves;
moves = move;
tmp = x; x = y; y = tmp;
} else {
size = cuddZddSwapInPlace(table, x, x_next);
if (size == 0)
goto zddSwapAnyOutOfMem;
move = (Move *)cuddDynamicAllocNode(table);
if (move == NULL)
goto zddSwapAnyOutOfMem;
move->x = x;
move->y = x_next;
move->size = size;
move->next = moves;
moves = move;
//.........这里部分代码省略.........
开发者ID:saidalfaraby,项目名称:DTP4TC,代码行数:101,代码来源:cuddZddReord.c
示例8: cuddZddSwapInPlace
//.........这里部分代码省略.........
f11 = empty; f10 = f1;
}
f0 = cuddE(f);
if ((int) f0->index == yindex) {
f01 = cuddT(f0); f00 = cuddE(f0);
} else {
f01 = empty; f00 = f0;
}
/* Decrease ref count of f1. */
cuddSatDec(f1->ref);
/* Create the new T child. */
if (f11 == empty) {
if (f01 != empty) {
newf1 = f01;
cuddSatInc(newf1->ref);
}
/* else case was already handled when finding nodes
** with both children below level y
*/
} else {
/* Check xlist for triple (xindex, f11, f01). */
posn = ddHash(f11, f01, xshift);
/* For each element newf1 in collision list xlist[posn]. */
newf1 = xlist[posn];
while (newf1 != NULL) {
if (cuddT(newf1) == f11 && cuddE(newf1) == f01) {
cuddSatInc(newf1->ref);
break; /* match */
}
newf1 = newf1->next;
} /* while newf1 */
if (newf1 == NULL) { /* no match */
newf1 = cuddDynamicAllocNode(table);
if (newf1 == NULL)
goto zddSwapOutOfMem;
newf1->index = xindex; newf1->ref = 1;
cuddT(newf1) = f11;
cuddE(newf1) = f01;
/* Insert newf1 in the collision list xlist[pos];
** increase the ref counts of f11 and f01
*/
newxkeys++;
newf1->next = xlist[posn];
xlist[posn] = newf1;
cuddSatInc(f11->ref);
cuddSatInc(f01->ref);
}
}
cuddT(f) = newf1;
/* Do the same for f0. */
/* Decrease ref count of f0. */
cuddSatDec(f0->ref);
/* Create the new E child. */
if (f10 == empty) {
newf0 = f00;
cuddSatInc(newf0->ref);
} else {
/* Check xlist for triple (xindex, f10, f00). */
posn = ddHash(f10, f00, xshift);
/* For each element newf0 in collision list xlist[posn]. */
newf0 = xlist[posn];
while (newf0 != NULL) {
if (cuddT(newf0) == f10 && cuddE(newf0) == f00) {
cuddSatInc(newf0->ref);
开发者ID:saidalfaraby,项目名称:DTP4TC,代码行数:67,代码来源:cuddZddReord.c
示例9: group
/**Function********************************************************************
Synopsis [Sifts down a variable until it reaches position xHigh.]
Description [Sifts down a variable until it reaches position xHigh.
Assumes that x is the bottom of a group (or a singleton). Records
all the moves. Returns 1 in case of success; 0 otherwise.]
SideEffects [None]
******************************************************************************/
static int
zddGroupSiftingDown(
DdManager * table,
int x,
int xHigh,
Move ** moves)
{
Move *move;
int y;
int size;
int limitSize;
int gxtop,gybot;
int xindex;
/* Initialize R */
xindex = table->invpermZ[x];
gxtop = table->subtableZ[x].next;
limitSize = size = table->keysZ;
y = cuddZddNextHigh(table,x);
while (y <= xHigh) {
/* Find bottom of y group. */
gybot = table->subtableZ[y].next;
while (table->subtableZ[gybot].next != (unsigned) y)
gybot = table->subtableZ[gybot].next;
if (table->subtableZ[x].next == (unsigned) x &&
table->subtableZ[y].next == (unsigned) y) {
/* x and y are self groups */
size = cuddZddSwapInPlace(table,x,y);
#ifdef DD_DEBUG
assert(table->subtableZ[x].next == (unsigned) x);
assert(table->subtableZ[y].next == (unsigned) y);
#endif
if (size == 0) goto zddGroupSiftingDownOutOfMem;
/* Record move. */
move = (Move *) cuddDynamicAllocNode(table);
if (move == NULL) goto zddGroupSiftingDownOutOfMem;
move->x = x;
move->y = y;
move->flags = MTR_DEFAULT;
move->size = size;
move->next = *moves;
*moves = move;
#ifdef DD_DEBUG
if (pr > 0) (void) fprintf(table->out,"zddGroupSiftingDown (2 single groups):\n");
#endif
if ((double) size > (double) limitSize * table->maxGrowth)
return(1);
if (size < limitSize) limitSize = size;
x = y;
y = cuddZddNextHigh(table,x);
} else { /* Group move */
size = zddGroupMove(table,x,y,moves);
if (size == 0) goto zddGroupSiftingDownOutOfMem;
if ((double) size > (double) limitSize * table->maxGrowth)
return(1);
if (size < limitSize) limitSize = size;
}
x = gybot;
y = cuddZddNextHigh(table,x);
}
return(1);
zddGroupSiftingDownOutOfMem:
while (*moves != NULL) {
move = (*moves)->next;
cuddDeallocNode(table, (DdNode *) *moves);
*moves = move;
}
return(0);
} /* end of zddGroupSiftingDown */
开发者ID:ansonn,项目名称:esl_systemc,代码行数:88,代码来源:cuddZddGroup.c
示例10: zddGroupMove
/**Function********************************************************************
Synopsis [Swaps two groups and records the move.]
Description [Swaps two groups and records the move. Returns the
number of keys in the DD table in case of success; 0 otherwise.]
SideEffects [None]
******************************************************************************/
static int
zddGroupMove(
DdManager * table,
int x,
int y,
Move ** moves)
{
Move *move;
int size;
int i,j,xtop,xbot,xsize,ytop,ybot,ysize,newxtop;
int swapx = x, swapy = y;
#if defined(DD_DEBUG) && defined(DD_VERBOSE)
int initialSize,bestSize;
#endif
#if DD_DEBUG
/* We assume that x < y */
assert(x < y);
#endif
/* Find top, bottom, and size for the two groups. */
xbot = x;
xtop = table->subtableZ[x].next;
xsize = xbot - xtop + 1;
ybot = y;
while ((unsigned) ybot < table->subtableZ[ybot].next)
ybot = table->subtableZ[ybot].next;
ytop = y;
ysize = ybot - ytop + 1;
#if defined(DD_DEBUG) && defined(DD_VERBOSE)
initialSize = bestSize = table->keysZ;
#endif
/* Sift the variables of the second group up through the first group */
for (i = 1; i <= ysize; i++) {
for (j = 1; j <= xsize; j++) {
size = cuddZddSwapInPlace(table,x,y);
if (size == 0) goto zddGroupMoveOutOfMem;
#if defined(DD_DEBUG) && defined(DD_VERBOSE)
if (size < bestSize)
bestSize = size;
#endif
swapx = x; swapy = y;
y = x;
x = cuddZddNextLow(table,y);
}
y = ytop + i;
x = cuddZddNextLow(table,y);
}
#if defined(DD_DEBUG) && defined(DD_VERBOSE)
if ((bestSize < initialSize) && (bestSize < size))
(void) fprintf(table->out,"Missed local minimum: initialSize:%d bestSize:%d finalSize:%d\n",initialSize,bestSize,size);
#endif
/* fix groups */
y = xtop; /* ytop is now where xtop used to be */
for (i = 0; i < ysize - 1; i++) {
table->subtableZ[y].next = cuddZddNextHigh(table,y);
y = cuddZddNextHigh(table,y);
}
table->subtableZ[y].next = xtop; /* y is bottom of its group, join */
/* it to top of its group */
x = cuddZddNextHigh(table,y);
newxtop = x;
for (i = 0; i < xsize - 1; i++) {
table->subtableZ[x].next = cuddZddNextHigh(table,x);
x = cuddZddNextHigh(table,x);
}
table->subtableZ[x].next = newxtop; /* x is bottom of its group, join */
/* it to top of its group */
#ifdef DD_DEBUG
if (pr > 0) (void) fprintf(table->out,"zddGroupMove:\n");
#endif
/* Store group move */
move = (Move *) cuddDynamicAllocNode(table);
if (move == NULL) goto zddGroupMoveOutOfMem;
move->x = swapx;
move->y = swapy;
move->flags = MTR_DEFAULT;
move->size = table->keysZ;
move->next = *moves;
*moves = move;
return(table->keysZ);
zddGroupMoveOutOfMem:
while (*moves != NULL) {
move = (*moves)->next;
cuddDeallocNode(table, (DdNode *) *moves);
*moves = move;
//.........这里部分代码省略.........
开发者ID:ansonn,项目名称:esl_systemc,代码行数:101,代码来源:cuddZddGroup.c
示例11: bound
/**Function********************************************************************
Synopsis [Sifts a variable down and applies the XOR transformation.]
Description [Sifts a variable down. Moves x down until either it
reaches the bound (xHigh) or the size of the ZDD heap increases too
much. Returns the set of moves in case of success; NULL if memory is
full.]
SideEffects [None]
SeeAlso []
******************************************************************************/
static Move *
cuddZddLinearDown(
DdManager * table,
int x,
int xHigh,
Move * prevMoves)
{
Move *moves;
Move *move;
int y;
int size, newsize;
int limitSize;
moves = prevMoves;
limitSize = table->keysZ;
y = cuddZddNextHigh(table, x);
while (y <= xHigh) {
size = cuddZddSwapInPlace(table, x, y);
if (size == 0)
goto cuddZddLinearDownOutOfMem;
newsize = cuddZddLinearInPlace(table, x, y);
if (newsize == 0)
goto cuddZddLinearDownOutOfMem;
move = (Move *) cuddDynamicAllocNode(table);
if (move == NULL)
goto cuddZddLinearDownOutOfMem;
move->x = x;
move->y = y;
move->next = moves;
moves = move;
move->flags = CUDD_SWAP_MOVE;
if (newsize > size) {
/* Undo transformation. The transformation we apply is
** its own inverse. Hence, we just apply the transformation
** again.
*/
newsize = cuddZddLinearInPlace(table,x,y);
if (newsize == 0) goto cuddZddLinearDownOutOfMem;
if (newsize != size) {
(void) fprintf(table->err,"Change in size after identity transformation! From %d to %d\n",size,newsize);
}
} else {
size = newsize;
move->flags = CUDD_LINEAR_TRANSFORM_MOVE;
}
move->size = size;
if ((double)size > (double)limitSize * table->maxGrowth)
break;
if (size < limitSize)
limitSize = size;
x = y;
y = cuddZddNextHigh(table, x);
}
return(moves);
cuddZddLinearDownOutOfMem:
while (moves != NULL) {
move = moves->next;
cuddDeallocMove(table, moves);
moves = move;
}
return((Move *) CUDD_OUT_OF_MEM);
} /* end of cuddZddLinearDown */
开发者ID:hugopaquet,项目名称:mcmas-sdds,代码行数:81,代码来源:cuddZddLin.c
示例12: cuddZddLinearInPlace
//.........这里部分代码省略.........
next = f->next;
/* Find f1, f0, f11, f10, f01, f00. */
f1 = cuddT(f);
if ((int) f1->index == yindex || (int) f1->index == xindex) {
f11 = cuddT(f1); f10 = cuddE(f1);
} else {
f11 = empty; f10 = f1;
}
f0 = cuddE(f);
if ((int) f0->index == yindex || (int) f0->index == xindex) {
f01 = cuddT(f0); f00 = cuddE(f0);
} else {
f01 = empty; f00 = f0;
}
/* Create the new T child. */
if (f01 == empty) {
newf1 = f10;
cuddSatInc(newf1->ref);
} else {
/* Check ylist for triple (yindex, f01, f10). */
posn = ddHash(f01, f10, yshift);
/* For each element newf1 in collision list ylist[posn]. */
newf1 = ylist[posn];
/* Search the collision chain skipping the marked nodes. */
while (newf1 != NULL) {
if (cuddT(newf1) == f01 && cuddE(newf1) == f10 &&
(int) newf1->index == yindex) {
cuddSatInc(newf1->ref);
break; /* match */
}
newf1 = newf1->next;
} /* while newf1 */
if (newf1 == NULL) { /* no match */
newf1 = cuddDynamicAllocNode(table);
if (newf1 == NULL)
goto zddSwapOutOfMem;
newf1->index = yindex; newf1->ref = 1;
cuddT(newf1) = f01;
cuddE(newf1) = f10;
/* Insert newf1 in the collision list ylist[pos];
** increase the ref counts of f01 and f10
*/
newykeys++;
newf1->next = ylist[posn];
ylist[posn] = newf1;
cuddSatInc(f01->ref);
cuddSatInc(f10->ref);
}
}
cuddT(f) = newf1;
/* Do the same for f0. */
/* Create the new E child. */
if (f11 == empty) {
newf0 = f00;
cuddSatInc(newf0->ref);
} else {
/* Check ylist for triple (yindex, f11, f00). */
posn = ddHash(f11, f00, yshift);
/* For each element newf0 in collision list ylist[posn]. */
newf0 = ylist[posn];
while (newf0 != NULL) {
if (cuddT(newf0) == f11 && cuddE(newf0) == f00 &&
(int) newf0->index == yindex) {
cuddSatInc(newf0->ref);
break; /* match */
开发者ID:hugopaquet,项目名称:mcmas-sdds,代码行数:67,代码来源:cuddZddLin.c
示例13: ddSymmGroupMove
/**Function********************************************************************
Synopsis [Swaps two groups.]
Description [Swaps two groups. x is assumed to be the bottom variable
of the first group. y is assumed to be the top variable of the second
group. Updates the list of moves. Returns the number of keys in the
table if successful; 0 otherwise.]
SideEffects [None]
******************************************************************************/
static int
ddSymmGroupMove(
DdManager * table,
int x,
int y,
Move ** moves)
{
Move *move;
int size;
int i,j;
int xtop,xbot,xsize,ytop,ybot,ysize,newxtop;
int swapx,swapy;
#ifdef DD_DEBUG
assert(x < y); /* we assume that x < y */
#endif
/* Find top, bottom, and size for the two groups. */
xbot = x;
xtop = table->subtables[x].next;
xsize = xbot - xtop + 1;
ybot = y;
while ((unsigned) ybot < table->subtables[ybot].next)
ybot = table->subtables[ybot].next;
ytop = y;
ysize = ybot - ytop + 1;
/* Sift the variables of the second group up through the first group. */
for (i = 1; i <= ysize; i++) {
for (j = 1; j <= xsize; j++) {
size = cuddSwapInPlace(table,x,y);
if (size == 0) return(0);
swapx = x; swapy = y;
y = x;
x = y - 1;
}
y = ytop + i;
x = y - 1;
}
/* fix symmetries */
y = xtop; /* ytop is now where xtop used to be */
for (i = 0; i < ysize-1 ; i++) {
table->subtables[y].next = y + 1;
y = y + 1;
}
table->subtables[y].next = xtop; /* y is bottom of its group, join */
/* its symmetry to top of its group */
x = y + 1;
newxtop = x;
for (i = 0; i < xsize - 1 ; i++) {
table->subtables[x].next = x + 1;
x = x + 1;
}
table->subtables[x].next = newxtop; /* x is bottom of its group, join */
/* its symmetry to top of its group */
/* Store group move */
move = (Move *) cuddDynamicAllocNode(table);
if (move == NULL) return(0);
move->x = swapx;
move->y = swapy;
move->size = size;
move->next = *moves;
*moves = move;
return(size);
} /* end of ddSymmGroupMove */
开发者ID:AndrewSmart,项目名称:CS5600,代码行数:79,代码来源:cuddSymmetry.c
示例14: bound
/**Function********************************************************************
Synopsis [Moves x down until either it reaches the bound (xHigh) or
the size of the DD heap increases too much.]
Description [Moves x down until either it reaches the bound (xHigh)
or the size of the DD heap increases too much. Assumes that x is the
bottom of a symmetry group. Checks x for symmetry to the adjacent
variables. If symmetry is found, the symmetry group of x is merged
with the symmetry group of the other variable. Returns the set of
moves in case of success; MV_OOM if memory is full.]
SideEffects [None]
******************************************************************************/
static Move *
ddSymmSiftingDown(
DdManager * table,
int x,
int xHigh)
{
Move *moves;
Move *move;
int y;
int size;
int limitSize;
int gxtop,gybot;
int R; /* upper bound on node decrease */
int xindex, yindex;
int isolated;
int z;
int zindex;
#ifdef DD_DEBUG
int checkR;
#endif
moves = NULL;
/* Initialize R */
xindex = table->invperm[x];
gxtop = table->subtables[x].next;
limitSize = size = table->keys - table->isolated;
R = 0;
for (z = xHigh; z > gxtop; z--) {
zindex = table->invperm[z];
if (zindex == xindex || cuddTestInteract(table,xindex,zindex)) {
isolated = table->vars[zindex]->ref == 1;
R += table->subtables[z].keys - isolated;
}
}
y = cuddNextHigh(table,x);
while (y <= xHigh && size - R < limitSize) {
#ifdef DD_DEBUG
gxtop = table->subtables[x].next;
checkR = 0;
for (z = xHigh; z > gxtop; z--) {
zindex = table->invperm[z];
if (zindex == xindex || cuddTestInteract(table,xindex,zindex)) {
isolated = table->vars[zindex]->ref == 1;
checkR += table->subtables[z].keys - isolated;
}
}
assert(R == checkR);
#endif
gybot = table->subtables[y].next;
while (table->subtables[gybot].next != (unsigned) y)
gybot = table->subtables[gybot].next;
if (cuddSymmCheck(table,x,y)) {
/* Symmetry found, attach symm groups */
gxtop = table->subtables[x].next;
table->subtables[x].next = y;
table->subtables[gybot].next = gxtop;
} else if (table->subtables[x].next == (unsigned) x &&
table->subtables[y].next == (unsigned) y) {
/* x and y have self symmetry */
/* Update upper bound on node decrease. */
yindex = table->invperm[y];
if (cuddTestInteract(table,xindex,yindex)) {
isolated = table->vars[yindex]->ref == 1;
R -= table->subtables[y].keys - isolated;
}
size = cuddSwapInPlace(table,x,y);
#ifdef DD_DEBUG
assert(table->subtables[x].next == (unsigned) x);
assert(table->subtables[y].next == (unsigned) y);
#endif
if (size == 0) goto ddSymmSiftingDownOutOfMem;
move = (Move *) cuddDynamicAllocNode(table);
if (move == NULL) goto ddSymmSiftingDownOutOfMem;
move->x = x;
move->y = y;
move->size = size;
move->next = moves;
moves = move;
if ((double) size > (double) limitSize * table->maxGrowth)
return(moves);
if (size < limitSize) limitSize = size;
} else { /* Group move */
/* Update upper bound on node decrease: first phase. */
gxtop = table->subtables[x].next;
//.........这里部分代码省略.........
开发者ID:AndrewSmart,项目名称:CS5600,代码行数:101,代码来源:cuddSymmetry.c
注:本文中的cuddDynamicAllocNode函数示例由纯净天空整理自Github/MSDocs等源码及文档管理平台,相关代码片段筛选自各路编程大神贡献的开源项目,源码版权归原作者所有,传播和使用请参考对应项目的License;未经允许,请勿转载。 |
请发表评论