diff options
Diffstat (limited to 'src/bdd')
-rw-r--r-- | src/bdd/cudd/cuddGroup.c | 25 | ||||
-rw-r--r-- | src/bdd/cudd/cuddInt.h | 15 | ||||
-rw-r--r-- | src/bdd/cudd/cuddReorder.c | 5 | ||||
-rw-r--r-- | src/bdd/cudd/cuddSymmetry.c | 5 |
4 files changed, 29 insertions, 21 deletions
diff --git a/src/bdd/cudd/cuddGroup.c b/src/bdd/cudd/cuddGroup.c index e38eee72..8e637603 100644 --- a/src/bdd/cudd/cuddGroup.c +++ b/src/bdd/cudd/cuddGroup.c @@ -110,11 +110,11 @@ static int originalLevel; /* Static function prototypes */ /*---------------------------------------------------------------------------*/ -static int ddTreeSiftingAux ARGS((DdManager *table, MtrNode *treenode, Cudd_ReorderingType method)); +static int ddTreeSiftingAux ARGS((DdManager *table, MtrNode *treenode, Cudd_ReorderingType method, int TimeStop)); #ifdef DD_STATS static int ddCountInternalMtrNodes ARGS((DdManager *table, MtrNode *treenode)); #endif -static int ddReorderChildren ARGS((DdManager *table, MtrNode *treenode, Cudd_ReorderingType method)); +static int ddReorderChildren ARGS((DdManager *table, MtrNode *treenode, Cudd_ReorderingType method, int TimeStop)); static void ddFindNodeHiLo ARGS((DdManager *table, MtrNode *treenode, int *lower, int *upper)); static int ddUniqueCompareGroup ARGS((int *ptrX, int *ptrY)); static int ddGroupSifting ARGS((DdManager *table, int lower, int upper, int (*checkFunction)(DdManager *, int, int), int lazyFlag)); @@ -231,7 +231,8 @@ Cudd_MakeTreeNode( int cuddTreeSifting( DdManager * table /* DD table */, - Cudd_ReorderingType method /* reordering method for the groups of leaves */) + Cudd_ReorderingType method /* reordering method for the groups of leaves */, + int TimeStop) { int i; int nvars; @@ -276,7 +277,7 @@ cuddTreeSifting( /* Reorder. */ - result = ddTreeSiftingAux(table, table->tree, method); + result = ddTreeSiftingAux(table, table->tree, method, TimeStop); #ifdef DD_STATS /* print stats */ if (!tempTree && method == CUDD_REORDER_GROUP_SIFT && @@ -319,7 +320,8 @@ static int ddTreeSiftingAux( DdManager * table, MtrNode * treenode, - Cudd_ReorderingType method) + Cudd_ReorderingType method, + int TimeStop) { MtrNode *auxnode; int res; @@ -332,20 +334,20 @@ ddTreeSiftingAux( auxnode = treenode; while (auxnode != NULL) { if (auxnode->child != NULL) { - if (!ddTreeSiftingAux(table, auxnode->child, method)) + if (!ddTreeSiftingAux(table, auxnode->child, method, TimeStop)) return(0); saveCheck = table->groupcheck; table->groupcheck = CUDD_NO_CHECK; if (method != CUDD_REORDER_LAZY_SIFT) - res = ddReorderChildren(table, auxnode, CUDD_REORDER_GROUP_SIFT); + res = ddReorderChildren(table, auxnode, CUDD_REORDER_GROUP_SIFT, TimeStop); else - res = ddReorderChildren(table, auxnode, CUDD_REORDER_LAZY_SIFT); + res = ddReorderChildren(table, auxnode, CUDD_REORDER_LAZY_SIFT, TimeStop); table->groupcheck = saveCheck; if (res == 0) return(0); } else if (auxnode->size > 1) { - if (!ddReorderChildren(table, auxnode, method)) + if (!ddReorderChildren(table, auxnode, method, TimeStop)) return(0); } auxnode = auxnode->younger; @@ -411,7 +413,8 @@ static int ddReorderChildren( DdManager * table, MtrNode * treenode, - Cudd_ReorderingType method) + Cudd_ReorderingType method, + int TimeStop) { int lower; int upper; @@ -450,7 +453,7 @@ ddReorderChildren( } while (result != 0); break; case CUDD_REORDER_SYMM_SIFT: - result = cuddSymmSifting(table,lower,upper); + result = cuddSymmSifting(table,lower,upper,TimeStop); break; case CUDD_REORDER_SYMM_SIFT_CONV: result = cuddSymmSiftingConv(table,lower,upper); diff --git a/src/bdd/cudd/cuddInt.h b/src/bdd/cudd/cuddInt.h index f5becf84..ca24a8aa 100644 --- a/src/bdd/cudd/cuddInt.h +++ b/src/bdd/cudd/cuddInt.h @@ -431,16 +431,17 @@ struct DdManager { /* specialized DD symbol table */ #endif #ifdef DD_MIS /* mis/verif compatibility fields */ - array_t *iton; /* maps ids in ddNode to node_t */ - array_t *order; /* copy of order_list */ + array_t *iton; /* maps ids in ddNode to node_t */ + array_t *order; /* copy of order_list */ lsHandle handle; /* where it is in network BDD list */ network_t *network; - st_table *local_order; /* for local BDDs */ - int nvars; /* variables used so far */ - int threshold; /* for pseudo var threshold value*/ + st_table *local_order; /* for local BDDs */ + int nvars; /* variables used so far */ + int threshold; /* for pseudo var threshold value*/ #endif DdNode * bFunc; DdNode * bFunc2; + int TimeStop; /* timeout for reordering */ }; typedef struct Move { @@ -1016,7 +1017,7 @@ EXTERN DdNode * cuddAddConstrainRecur ARGS((DdManager *dd, DdNode *f, DdNode *c) EXTERN DdNode * cuddAddRestrictRecur ARGS((DdManager *dd, DdNode *f, DdNode *c)); EXTERN DdNode * cuddBddLICompaction ARGS((DdManager *dd, DdNode *f, DdNode *c)); EXTERN int cuddGa ARGS((DdManager *table, int lower, int upper)); -EXTERN int cuddTreeSifting ARGS((DdManager *table, Cudd_ReorderingType method)); +EXTERN int cuddTreeSifting ARGS((DdManager *table, Cudd_ReorderingType method, int TimeStop)); EXTERN int cuddZddInitUniv ARGS((DdManager *zdd)); EXTERN void cuddZddFreeUniv ARGS((DdManager *zdd)); EXTERN void cuddSetInteract ARGS((DdManager *table, int x, int y)); @@ -1071,7 +1072,7 @@ EXTERN DdNode* cuddSplitSetRecur ARGS((DdManager *manager, st_table *mtable, int EXTERN DdNode * cuddSubsetHeavyBranch ARGS((DdManager *dd, DdNode *f, int numVars, int threshold)); EXTERN DdNode * cuddSubsetShortPaths ARGS((DdManager *dd, DdNode *f, int numVars, int threshold, int hardlimit)); EXTERN int cuddSymmCheck ARGS((DdManager *table, int x, int y)); -EXTERN int cuddSymmSifting ARGS((DdManager *table, int lower, int upper)); +EXTERN int cuddSymmSifting ARGS((DdManager *table, int lower, int upper, int TimeStop)); EXTERN int cuddSymmSiftingConv ARGS((DdManager *table, int lower, int upper)); EXTERN DdNode * cuddAllocNode ARGS((DdManager *unique)); EXTERN DdManager * cuddInitTable ARGS((unsigned int numVars, unsigned int numVarsZ, unsigned int numSlots, unsigned int looseUpTo)); diff --git a/src/bdd/cudd/cuddReorder.c b/src/bdd/cudd/cuddReorder.c index 93bbb10b..020a1b5e 100644 --- a/src/bdd/cudd/cuddReorder.c +++ b/src/bdd/cudd/cuddReorder.c @@ -158,6 +158,7 @@ Cudd_ReduceHeap( unsigned int finalSize; #endif long localTime; + int TimeStop = table->TimeStop; /* Don't reorder if there are too many dead nodes. */ if (table->keys - table->dead < (unsigned) minsize) @@ -239,10 +240,10 @@ Cudd_ReduceHeap( if (table->reordCycle && table->reorderings % table->reordCycle == 0) { double saveGrowth = table->maxGrowth; table->maxGrowth = table->maxGrowthAlt; - result = cuddTreeSifting(table,heuristic); + result = cuddTreeSifting(table,heuristic,TimeStop); table->maxGrowth = saveGrowth; } else { - result = cuddTreeSifting(table,heuristic); + result = cuddTreeSifting(table,heuristic,TimeStop); } #ifdef DD_STATS diff --git a/src/bdd/cudd/cuddSymmetry.c b/src/bdd/cudd/cuddSymmetry.c index 88e607e5..535ba978 100644 --- a/src/bdd/cudd/cuddSymmetry.c +++ b/src/bdd/cudd/cuddSymmetry.c @@ -294,7 +294,8 @@ int cuddSymmSifting( DdManager * table, int lower, - int upper) + int upper, + int TimeStop) { int i; int *var; @@ -338,6 +339,8 @@ cuddSymmSifting( for (i = 0; i < ddMin(table->siftMaxVar,size); i++) { if (ddTotalNumberSwapping >= table->siftMaxSwap) break; + if ( TimeStop && TimeStop < clock() ) + break; x = table->perm[var[i]]; #ifdef DD_STATS previousSize = table->keys - table->isolated; |