Yet another update to the runtime control in BDD operations.

src/aig/llb/llb3Nonlin.c

@@ -427,7 +427,7 @@ int Llb_NonlinReachability( Llb_Mnn_t * p )
         if ( p->pPars->TimeLimit && clock() >= p->pPars->TimeTarget )
         {
             if ( !p->pPars->fSilent )
-                printf( "Reached timeout during image computation (%d seconds).\n",  p->pPars->TimeLimit );
+                printf( "Reached timeout (%d seconds) during image computation.\n",  p->pPars->TimeLimit );
             p->pPars->iFrame = nIters - 1;
             Cudd_RecursiveDeref( p->dd,  bCurrent );  bCurrent = NULL;
             return -1;
@@ -484,7 +484,7 @@ int Llb_NonlinReachability( Llb_Mnn_t * p )
         if ( bNext == NULL )
         {
             if ( !p->pPars->fSilent )
-                printf( "Reached timeout during image computation (%d seconds).\n",  p->pPars->TimeLimit );
+                printf( "Reached timeout (%d seconds) during image computation in quantification.\n",  p->pPars->TimeLimit );
             p->pPars->iFrame = nIters - 1;
             Cudd_RecursiveDeref( p->dd,  bCurrent );  bCurrent = NULL;
             return -1;
@@ -530,7 +530,16 @@ int Llb_NonlinReachability( Llb_Mnn_t * p )
         // transfer to the state manager
         clk3 = clock();
         Cudd_RecursiveDeref( p->ddG, p->ddG->bFunc2 );
-        p->ddG->bFunc2 = Extra_TransferPermute( p->dd, p->ddG, bNext, Vec_IntArray(p->vNs2Glo) );    Cudd_Ref( p->ddG->bFunc2 );
+        p->ddG->bFunc2 = Extra_TransferPermuteTime( p->dd, p->ddG, bNext, Vec_IntArray(p->vNs2Glo), p->pPars->TimeTarget );    
+        if ( p->ddG->bFunc2 == NULL )
+        {
+            if ( !p->pPars->fSilent )
+                printf( "Reached timeout (%d seconds) during image computation in transfer 1.\n",  p->pPars->TimeLimit );
+            p->pPars->iFrame = nIters - 1;
+            Cudd_RecursiveDeref( p->dd,  bNext );  
+            return -1;
+        }
+        Cudd_Ref( p->ddG->bFunc2 );
         Cudd_RecursiveDeref( p->dd, bNext );
         p->timeTran1 += clock() - clk3;
 
@@ -552,7 +561,15 @@ int Llb_NonlinReachability( Llb_Mnn_t * p )
 
         // move new states to the working manager
         clk3 = clock();
-        bCurrent = Extra_TransferPermute( p->ddG, p->dd, p->ddG->bFunc2, Vec_IntArray(p->vGlo2Cs) ); Cudd_Ref( bCurrent );
+        bCurrent = Extra_TransferPermuteTime( p->ddG, p->dd, p->ddG->bFunc2, Vec_IntArray(p->vGlo2Cs), p->pPars->TimeTarget ); 
+        if ( bCurrent == NULL )
+        {
+            if ( !p->pPars->fSilent )
+                printf( "Reached timeout (%d seconds) during image computation in transfer 2.\n",  p->pPars->TimeLimit );
+            p->pPars->iFrame = nIters - 1;
+            return -1;
+        }
+        Cudd_Ref( bCurrent );
         p->timeTran2 += clock() - clk3;
 
         // report the results

src/misc/extra/extra.h

@@ -265,6 +265,7 @@ extern DdNode *     extraZddSelectOneSubset( DdManager * dd, DdNode * zS );
 
 extern DdNode *    Extra_bddAndTime( DdManager * dd, DdNode * f, DdNode * g, int TimeOut );
 extern DdNode *    Extra_bddAndAbstractTime( DdManager * manager, DdNode * f, DdNode * g, DdNode * cube, int TimeOut );
+extern DdNode *    Extra_TransferPermuteTime( DdManager * ddSource, DdManager * ddDestination, DdNode * f, int * Permute, int TimeOut );
 
 /*=== extraBddUnate.c =================================================================*/
 

src/misc/extra/extraBddTime.c

@@ -25,6 +25,8 @@ ABC_NAMESPACE_IMPL_START
 /* Constant declarations                                                     */
 /*---------------------------------------------------------------------------*/
 
+#define CHECK_FACTOR 10
+
 /*---------------------------------------------------------------------------*/
 /* Stucture declarations                                                     */
 /*---------------------------------------------------------------------------*/
@@ -53,6 +55,8 @@ ABC_NAMESPACE_IMPL_START
 
 static DdNode * cuddBddAndRecurTime( DdManager * manager, DdNode * f, DdNode * g, int * pRecCalls, int TimeOut );
 static DdNode * cuddBddAndAbstractRecurTime( DdManager * manager, DdNode * f, DdNode * g, DdNode * cube, int * pRecCalls, int TimeOut );
+static DdNode * extraTransferPermuteTime( DdManager * ddS, DdManager * ddD, DdNode * f, int * Permute, int TimeOut );
+static DdNode * extraTransferPermuteRecurTime( DdManager * ddS, DdManager * ddD, DdNode * f, st_table * table, int * Permute, int TimeOut );
 
 /**AutomaticEnd***************************************************************/
 
@@ -91,7 +95,7 @@ Extra_bddAndTime(
     } while (dd->reordered == 1);
     return(res);
 
-} /* end of Cudd_bddAnd */
+} /* end of Extra_bddAndTime */
 
 /**Function********************************************************************
 
@@ -126,8 +130,35 @@ Extra_bddAndAbstractTime(
     } while (manager->reordered == 1);
     return(res);
 
-} /* end of Cudd_bddAndAbstract */
+} /* end of Extra_bddAndAbstractTime */
+
+/**Function********************************************************************
+
+  Synopsis    [Convert a {A,B}DD from a manager to another with variable remapping.]
+
+  Description [Convert a {A,B}DD from a manager to another one. The orders of the
+  variables in the two managers may be different. Returns a
+  pointer to the {A,B}DD in the destination manager if successful; NULL
+  otherwise. The i-th entry in the array Permute tells what is the index
+  of the i-th variable from the old manager in the new manager.]
+
+  SideEffects [None]
+
+  SeeAlso     []
 
+******************************************************************************/
+DdNode * Extra_TransferPermuteTime( DdManager * ddSource, DdManager * ddDestination, DdNode * f, int * Permute, int TimeOut )
+{
+    DdNode * bRes;
+    do
+    {
+        ddDestination->reordered = 0;
+        bRes = extraTransferPermuteTime( ddSource, ddDestination, f, Permute, TimeOut );
+    }
+    while ( ddDestination->reordered == 1 );
+    return ( bRes );
+
+} /* end of Extra_TransferPermuteTime */
 
 
 /*---------------------------------------------------------------------------*/
@@ -193,7 +224,8 @@ cuddBddAndRecurTime(
     if (r != NULL) return(r);
     }
 
-    if ( TimeOut && ((*pRecCalls)++ % 10) == 0 && TimeOut < clock() )
+//    if ( TimeOut && ((*pRecCalls)++ % CHECK_FACTOR) == 0 && TimeOut < clock() )
+    if ( TimeOut && TimeOut < clock() )
         return NULL;
 
     /* Here we can skip the use of cuddI, because the operands are known
@@ -346,7 +378,8 @@ cuddBddAndAbstractRecurTime(
     }
     }
 
-    if ( TimeOut && ((*pRecCalls)++ % 10) == 0 && TimeOut < clock() )
+//    if ( TimeOut && ((*pRecCalls)++ % CHECK_FACTOR) == 0 && TimeOut < clock() )
+    if ( TimeOut && TimeOut < clock() )
         return NULL;
 
     if (topf == top) {
@@ -464,6 +497,161 @@ cuddBddAndAbstractRecurTime(
 /* Definition of static functions                                            */
 /*---------------------------------------------------------------------------*/
 
+/**Function********************************************************************
+
+  Synopsis    [Convert a BDD from a manager to another one.]
+
+  Description [Convert a BDD from a manager to another one. Returns a
+  pointer to the BDD in the destination manager if successful; NULL
+  otherwise.]
+
+  SideEffects [None]
+
+  SeeAlso     [Extra_TransferPermute]
+
+******************************************************************************/
+DdNode * extraTransferPermuteTime( DdManager * ddS, DdManager * ddD, DdNode * f, int * Permute, int TimeOut )
+{
+    DdNode *res;
+    st_table *table = NULL;
+    st_generator *gen = NULL;
+    DdNode *key, *value;
+
+    table = st_init_table( st_ptrcmp, st_ptrhash );
+    if ( table == NULL )
+        goto failure;
+    res = extraTransferPermuteRecurTime( ddS, ddD, f, table, Permute, TimeOut );
+    if ( res != NULL )
+        cuddRef( res );
+
+    /* Dereference all elements in the table and dispose of the table.
+       ** This must be done also if res is NULL to avoid leaks in case of
+       ** reordering. */
+    gen = st_init_gen( table );
+    if ( gen == NULL )
+        goto failure;
+    while ( st_gen( gen, ( const char ** ) &key, ( char ** ) &value ) )
+    {
+        Cudd_RecursiveDeref( ddD, value );
+    }
+    st_free_gen( gen );
+    gen = NULL;
+    st_free_table( table );
+    table = NULL;
+
+    if ( res != NULL )
+        cuddDeref( res );
+    return ( res );
+
+  failure:
+    if ( table != NULL )
+        st_free_table( table );
+    if ( gen != NULL )
+        st_free_gen( gen );
+    return ( NULL );
+
+} /* end of extraTransferPermuteTime */
+
+
+/**Function********************************************************************
+
+  Synopsis    [Performs the recursive step of Extra_TransferPermute.]
+
+  Description [Performs the recursive step of Extra_TransferPermute.
+  Returns a pointer to the result if successful; NULL otherwise.]
+
+  SideEffects [None]
+
+  SeeAlso     [extraTransferPermuteTime]
+
+******************************************************************************/
+static DdNode * 
+extraTransferPermuteRecurTime( 
+  DdManager * ddS, 
+  DdManager * ddD, 
+  DdNode * f, 
+  st_table * table, 
+  int * Permute,
+  int TimeOut )
+{
+    DdNode *ft, *fe, *t, *e, *var, *res;
+    DdNode *one, *zero;
+    int index;
+    int comple = 0;
+
+    statLine( ddD );
+    one = DD_ONE( ddD );
+    comple = Cudd_IsComplement( f );
+
+    /* Trivial cases. */
+    if ( Cudd_IsConstant( f ) )
+        return ( Cudd_NotCond( one, comple ) );
+
+
+    /* Make canonical to increase the utilization of the cache. */
+    f = Cudd_NotCond( f, comple );
+    /* Now f is a regular pointer to a non-constant node. */
+
+    /* Check the cache. */
+    if ( st_lookup( table, ( char * ) f, ( char ** ) &res ) )
+        return ( Cudd_NotCond( res, comple ) );
+
+    if ( TimeOut && TimeOut < clock() )
+        return NULL;
+
+    /* Recursive step. */
+    if ( Permute )
+        index = Permute[f->index];
+    else
+        index = f->index;
+
+    ft = cuddT( f );
+    fe = cuddE( f );
+
+    t = extraTransferPermuteRecurTime( ddS, ddD, ft, table, Permute, TimeOut );
+    if ( t == NULL )
+    {
+        return ( NULL );
+    }
+    cuddRef( t );
+
+    e = extraTransferPermuteRecurTime( ddS, ddD, fe, table, Permute, TimeOut );
+    if ( e == NULL )
+    {
+        Cudd_RecursiveDeref( ddD, t );
+        return ( NULL );
+    }
+    cuddRef( e );
+
+    zero = Cudd_Not(ddD->one);
+    var = cuddUniqueInter( ddD, index, one, zero );
+    if ( var == NULL )
+    {
+        Cudd_RecursiveDeref( ddD, t );
+        Cudd_RecursiveDeref( ddD, e );
+        return ( NULL );
+    }
+    res = cuddBddIteRecur( ddD, var, t, e );
+
+    if ( res == NULL )
+    {
+        Cudd_RecursiveDeref( ddD, t );
+        Cudd_RecursiveDeref( ddD, e );
+        return ( NULL );
+    }
+    cuddRef( res );
+    Cudd_RecursiveDeref( ddD, t );
+    Cudd_RecursiveDeref( ddD, e );
+
+    if ( st_add_direct( table, ( char * ) f, ( char * ) res ) ==
+         ST_OUT_OF_MEM )
+    {
+        Cudd_RecursiveDeref( ddD, res );
+        return ( NULL );
+    }
+    return ( Cudd_NotCond( res, comple ) );
+
+}  /* end of extraTransferPermuteRecurTime */
 
 ////////////////////////////////////////////////////////////////////////
 ///                           END OF FILE                            ///