summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/aig/llb/llb3Nonlin.c4
-rw-r--r--src/bdd/cudd/cuddGroup.c25
-rw-r--r--src/bdd/cudd/cuddInt.h15
-rw-r--r--src/bdd/cudd/cuddReorder.c5
-rw-r--r--src/bdd/cudd/cuddSymmetry.c5
5 files changed, 33 insertions, 21 deletions
diff --git a/src/aig/llb/llb3Nonlin.c b/src/aig/llb/llb3Nonlin.c
index 2b4272d9..adab5b0b 100644
--- a/src/aig/llb/llb3Nonlin.c
+++ b/src/aig/llb/llb3Nonlin.c
@@ -401,6 +401,10 @@ int Llb_NonlinReachability( Llb_Mnn_t * p )
p->pPars->TimeTarget = clock() + p->pPars->TimeLimit * CLOCKS_PER_SEC;
else
p->pPars->TimeTarget = 0;
+ // set the stop time parameter
+ p->dd->TimeStop = p->pPars->TimeTarget;
+ p->ddG->TimeStop = p->pPars->TimeTarget;
+ p->ddR->TimeStop = p->pPars->TimeTarget;
// set reordering hooks
assert( p->dd->bFunc == NULL );
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;
generated by cgit v1.2.3 (git 2.25.1) at 2025-04-02 17:28:23 +0000