Modificationd to CUDD to enable runtime-limit in variable reordering.

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 );

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);

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));

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

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;