Added handling runtime limit inside And and AndExist.

7 files changed, 521 insertions, 19 deletions

diff --git a/src/aig/llb/llb2Bad.c b/src/aig/llb/llb2Bad.c
index 4099805b..88ff4c75 100644
--- a/src/aig/llb/llb2Bad.c
+++ b/src/aig/llb/llb2Bad.c
@@ -63,15 +63,16 @@ DdNode * Llb_BddComputeBad( Aig_Man_t * pInit, DdManager * dd, int TimeOut )
             continue;
         bBdd0 = Cudd_NotCond( (DdNode *)Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0(pObj) );
         bBdd1 = Cudd_NotCond( (DdNode *)Aig_ObjFanin1(pObj)->pData, Aig_ObjFaninC1(pObj) );
-        pObj->pData = Cudd_bddAnd( dd, bBdd0, bBdd1 );          Cudd_Ref( (DdNode *)pObj->pData );
-
-        if ( i % 10 == 0 && TimeOut && clock() >= TimeOut )
+        pObj->pData = Extra_bddAndTime( dd, bBdd0, bBdd1, TimeOut );
+        if ( pObj->pData == NULL )
         {
-            Vec_PtrForEachEntryStop( Aig_Obj_t *, vNodes, pObj, k, i+1 )
-                Cudd_RecursiveDeref( dd, (DdNode *)pObj->pData );
+            Vec_PtrForEachEntryStop( Aig_Obj_t *, vNodes, pObj, k, i )
+                if ( pObj->pData )
+                    Cudd_RecursiveDeref( dd, (DdNode *)pObj->pData );
             Vec_PtrFree( vNodes );
             return NULL;
         }
+        Cudd_Ref( (DdNode *)pObj->pData );
     }
     // quantify PIs of each PO
     bResult = Cudd_ReadLogicZero( dd );  Cudd_Ref( bResult );
@@ -112,8 +113,7 @@ DdNode * Llb_BddQuantifyPis( Aig_Man_t * pInit, DdManager * dd, DdNode * bFunc )
     assert( Cudd_ReadSize(dd) == Aig_ManPiNum(pInit) );
     // create PI cube
     bCube = Cudd_ReadOne( dd );  Cudd_Ref( bCube );
-    Saig_ManForEachPi( pInit, pObj, i )
-    {
+    Saig_ManForEachPi( pInit, pObj, i )    {
         bVar  = Cudd_bddIthVar( dd, Aig_ManRegNum(pInit) + i );
         bCube = Cudd_bddAnd( dd, bTemp = bCube, bVar );  Cudd_Ref( bCube );
         Cudd_RecursiveDeref( dd, bTemp );
diff --git a/src/aig/llb/llb3Image.c b/src/aig/llb/llb3Image.c
index 87e09c46..9bb01195 100644
--- a/src/aig/llb/llb3Image.c
+++ b/src/aig/llb/llb3Image.c
@@ -334,7 +334,7 @@ int Llb_NonlinQuantify1( Llb_Mgr_t * p, Llb_Prt_t * pPart, int fSubset )
   SeeAlso     []
 
 ***********************************************************************/
-int Llb_NonlinQuantify2( Llb_Mgr_t * p, Llb_Prt_t * pPart1, Llb_Prt_t * pPart2, int Limit )
+int Llb_NonlinQuantify2( Llb_Mgr_t * p, Llb_Prt_t * pPart1, Llb_Prt_t * pPart2, int Limit, int TimeOut )
 {
     int fVerbose = 0;
     Llb_Var_t * pVar;
@@ -358,10 +358,10 @@ Extra_bddPrintSupport( p->dd, bCube );  printf( "\n" );
  
     // derive new function
 //    bFunc = Cudd_bddAndAbstract( p->dd, pPart1->bFunc, pPart2->bFunc, bCube );  Cudd_Ref( bFunc );
+/*
     bFunc = Cudd_bddAndAbstractLimit( p->dd, pPart1->bFunc, pPart2->bFunc, bCube, Limit );  
     if ( bFunc == NULL )
     {
-/*
         int RetValue;
         Cudd_RecursiveDeref( p->dd, bCube );
         if ( pPart1->nSize < pPart2->nSize )
@@ -370,12 +370,21 @@ Extra_bddPrintSupport( p->dd, bCube );  printf( "\n" );
             RetValue = Llb_NonlinQuantify1( p, pPart2, 1 );
         if ( RetValue )
             Limit = Limit + 1000;
-        Llb_NonlinQuantify2( p, pPart1, pPart2, Limit );
+        Llb_NonlinQuantify2( p, pPart1, pPart2, Limit, TimeOut );
+        return 0;
+    }
+    Cudd_Ref( bFunc );
 */
-        return 1;
+
+    bFunc = Extra_bddAndAbstractTime( p->dd, pPart1->bFunc, pPart2->bFunc, bCube, TimeOut );  
+    if ( bFunc == NULL )
+    {
+        Cudd_RecursiveDeref( p->dd, bCube );
+        return 0;
     }
     Cudd_Ref( bFunc );
     Cudd_RecursiveDeref( p->dd, bCube );
+
     // create new partition
     pTemp = p->pParts[p->iPartFree] = ABC_CALLOC( Llb_Prt_t, 1 );
     pTemp->iPart = p->iPartFree++;
@@ -454,7 +463,7 @@ printf( "Updating partitiong %d with singlton vars.\n", pTemp->iPart );
 if ( fVerbose )
 Llb_NonlinPrint( p );
     Vec_PtrFree( vSingles );
-    return 0;
+    return 1;
 }
 
 /**Function*************************************************************
@@ -529,7 +538,7 @@ Vec_Ptr_t * Llb_NonlinBuildBdds( Aig_Man_t * p, Vec_Ptr_t * vLower, Vec_Ptr_t *
     Vec_Ptr_t * vNodes, * vResult;
     Aig_Obj_t * pObj;
     DdNode * bBdd0, * bBdd1, * bProd;
-    int i;
+    int i, k;
 
     Aig_ManConst1(p)->pData = Cudd_ReadOne( dd );
     Vec_PtrForEachEntry( Aig_Obj_t *, vLower, pObj, i )
@@ -540,16 +549,16 @@ Vec_Ptr_t * Llb_NonlinBuildBdds( Aig_Man_t * p, Vec_Ptr_t * vLower, Vec_Ptr_t *
     {
         bBdd0 = Cudd_NotCond( (DdNode *)Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0(pObj) );
         bBdd1 = Cudd_NotCond( (DdNode *)Aig_ObjFanin1(pObj)->pData, Aig_ObjFaninC1(pObj) );
-        pObj->pData = Cudd_bddAnd( dd, bBdd0, bBdd1 );   Cudd_Ref( (DdNode *)pObj->pData );
-
-        if ( i % 10 == 0 && TimeOut && clock() >= TimeOut )
+        pObj->pData = Extra_bddAndTime( dd, bBdd0, bBdd1, TimeOut );
+        if ( pObj->pData == NULL )
         {
-            Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
+            Vec_PtrForEachEntryStop( Aig_Obj_t *, vNodes, pObj, k, i )
                 if ( pObj->pData )
                     Cudd_RecursiveDeref( dd, (DdNode *)pObj->pData );
             Vec_PtrFree( vNodes );
             return NULL;
         }
+        Cudd_Ref( (DdNode *)pObj->pData );
     }
 
     vResult = Vec_PtrAlloc( 100 );
@@ -882,7 +891,7 @@ DdNode * Llb_NonlinImage( Aig_Man_t * pAig, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vRo
     {
         clk2 = clock();
         nReorders = Cudd_ReadReorderings(dd);
-        if ( Llb_NonlinQuantify2( p, pPart1, pPart2, Limit ) )
+        if ( !Llb_NonlinQuantify2( p, pPart1, pPart2, Limit, TimeOut ) )
         {
             Llb_NonlinFree( p );
             return NULL;
diff --git a/src/aig/llb/llbInt.h b/src/aig/llb/llbInt.h
index 36d3796c..1294438e 100644
--- a/src/aig/llb/llbInt.h
+++ b/src/aig/llb/llbInt.h
@@ -168,7 +168,7 @@ extern DdNode *        Llb_ImgComputeImage( Aig_Man_t * pAig, Vec_Ptr_t * vDdMan
 
 /*=== llb3Image.c ======================================================*/
 extern DdNode *        Llb_NonlinImage( Aig_Man_t * pAig, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vRoots, int * pVars2Q, 
-                           DdManager * dd, DdNode * bCurrent, int fReorder, int fVerbose, int * pOrder, int Limit, int TimeLimit );
+                           DdManager * dd, DdNode * bCurrent, int fReorder, int fVerbose, int * pOrder, int Limit, int TimeTarget );
 
 ABC_NAMESPACE_HEADER_END
 
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 32618e76..7ee6769e 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -27590,6 +27590,11 @@ int Abc_CommandAbc9ReachM( Abc_Frame_t * pAbc, int argc, char ** argv )
         Abc_Print( -1, "Abc_CommandAbc9ReachM(): The current AIG has no latches.\n" );
         return 0;
     } 
+    if ( Gia_ManObjNum(pAbc->pGia) >= (1<<16) )
+    {
+        Abc_Print( -1, "Abc_CommandAbc9ReachM(): Currently cannot handle AIGs with more than %d objects.\n", (1<<16) );
+        return 0;
+    }
     pAbc->Status  = Llb_ManModelCheckGia( pAbc->pGia, pPars );
     pAbc->nFrames = pPars->iFrame;
     Abc_FrameReplaceCex( pAbc, &pAbc->pGia->pCexSeq );
@@ -27737,6 +27742,11 @@ int Abc_CommandAbc9ReachP( Abc_Frame_t * pAbc, int argc, char ** argv )
         Abc_Print( -1, "Abc_CommandAbc9ReachP(): The current AIG has no latches.\n" );
         return 0;
     }
+    if ( Gia_ManObjNum(pAbc->pGia) >= (1<<16) )
+    {
+        Abc_Print( -1, "Abc_CommandAbc9ReachP(): Currently cannot handle AIGs with more than %d objects.\n", (1<<16) );
+        return 0;
+    }
     pMan          = Gia_ManToAigSimple( pAbc->pGia );
     pAbc->Status  = Llb_ManReachMinCut( pMan, pPars );
     pAbc->nFrames = pPars->iFrame;
@@ -27865,6 +27875,11 @@ int Abc_CommandAbc9ReachN( Abc_Frame_t * pAbc, int argc, char ** argv )
         Abc_Print( -1, "Abc_CommandAbc9ReachN(): The current AIG has no latches.\n" );
         return 0;
     }
+    if ( Gia_ManObjNum(pAbc->pGia) >= (1<<16) )
+    {
+        Abc_Print( -1, "Abc_CommandAbc9ReachN(): Currently cannot handle AIGs with more than %d objects.\n", (1<<16) );
+        return 0;
+    }
     pMan          = Gia_ManToAigSimple( pAbc->pGia );
     pAbc->Status  = Llb_NonlinCoreReach( pMan, pPars );
     pAbc->nFrames = pPars->iFrame;
diff --git a/src/misc/extra/extra.h b/src/misc/extra/extra.h
index 33303fac..3f65e43a 100644
--- a/src/misc/extra/extra.h
+++ b/src/misc/extra/extra.h
@@ -263,6 +263,11 @@ extern DdNode *     extraZddSelectOneSubset( DdManager * dd, DdNode * zS );
 
 /*=== extraBddUnate.c =================================================================*/
 
+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 );
+
+/*=== extraBddUnate.c =================================================================*/
+
 typedef struct Extra_UnateVar_t_  Extra_UnateVar_t;
 struct Extra_UnateVar_t_ {
     unsigned    iVar : 30;  // index of the variable
diff --git a/src/misc/extra/extraBddTime.c b/src/misc/extra/extraBddTime.c
new file mode 100644
index 00000000..6a3b725a
--- /dev/null
+++ b/src/misc/extra/extraBddTime.c
@@ -0,0 +1,472 @@
+/**CFile****************************************************************
+
+  FileName    [extraBddTime.c]
+
+  PackageName [extra]
+
+  Synopsis    [Procedures to control runtime in BDD operators.]
+
+  Author      [Alan Mishchenko]
+
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 2.0. Started - September 1, 2003.]
+
+  Revision    [$Id: extraBddTime.c,v 1.0 2003/05/21 18:03:50 alanmi Exp $]
+
+***********************************************************************/
+
+#include "extra.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+/*---------------------------------------------------------------------------*/
+/* Constant declarations                                                     */
+/*---------------------------------------------------------------------------*/
+
+/*---------------------------------------------------------------------------*/
+/* Stucture declarations                                                     */
+/*---------------------------------------------------------------------------*/
+
+/*---------------------------------------------------------------------------*/
+/* Type declarations                                                         */
+/*---------------------------------------------------------------------------*/
+
+
+/*---------------------------------------------------------------------------*/
+/* Variable declarations                                                     */
+/*---------------------------------------------------------------------------*/
+
+
+
+/*---------------------------------------------------------------------------*/
+/* Macro declarations                                                        */
+/*---------------------------------------------------------------------------*/
+
+
+/**AutomaticStart*************************************************************/
+
+/*---------------------------------------------------------------------------*/
+/* Static function prototypes                                                */
+/*---------------------------------------------------------------------------*/
+
+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 );
+
+/**AutomaticEnd***************************************************************/
+
+
+/*---------------------------------------------------------------------------*/
+/* Definition of exported functions                                          */
+/*---------------------------------------------------------------------------*/
+
+/**Function********************************************************************
+
+  Synopsis    [Computes the conjunction of two BDDs f and g.]
+
+  Description [Computes the conjunction of two BDDs f and g. Returns a
+  pointer to the resulting BDD if successful; NULL if the intermediate
+  result blows up.]
+
+  SideEffects [None]
+
+  SeeAlso     [Cudd_bddIte Cudd_addApply Cudd_bddAndAbstract Cudd_bddIntersect
+  Cudd_bddOr Cudd_bddNand Cudd_bddNor Cudd_bddXor Cudd_bddXnor]
+
+******************************************************************************/
+DdNode *
+Extra_bddAndTime(
+  DdManager * dd,
+  DdNode * f,
+  DdNode * g,
+  int TimeOut)
+{
+    DdNode *res;
+    int Counter = 0;
+
+    do {
+    dd->reordered = 0;
+    res = cuddBddAndRecurTime(dd,f,g, &Counter, TimeOut);
+    } while (dd->reordered == 1);
+    return(res);
+
+} /* end of Cudd_bddAnd */
+
+/**Function********************************************************************
+
+  Synopsis [Takes the AND of two BDDs and simultaneously abstracts the
+  variables in cube.]
+
+  Description [Takes the AND of two BDDs and simultaneously abstracts
+  the variables in cube. The variables are existentially abstracted.
+  Returns a pointer to the result is successful; NULL otherwise.
+  Cudd_bddAndAbstract implements the semiring matrix multiplication
+  algorithm for the boolean semiring.]
+
+  SideEffects [None]
+
+  SeeAlso     [Cudd_addMatrixMultiply Cudd_addTriangle Cudd_bddAnd]
+
+******************************************************************************/
+DdNode *
+Extra_bddAndAbstractTime(
+  DdManager * manager,
+  DdNode * f,
+  DdNode * g,
+  DdNode * cube,
+  int TimeOut)
+{
+    DdNode *res;
+    int Counter = 0;
+
+    do {
+    manager->reordered = 0;
+    res = cuddBddAndAbstractRecurTime(manager, f, g, cube, &Counter, TimeOut);
+    } while (manager->reordered == 1);
+    return(res);
+
+} /* end of Cudd_bddAndAbstract */
+
+
+
+/*---------------------------------------------------------------------------*/
+/* Definition of internal functions                                          */
+/*---------------------------------------------------------------------------*/
+
+/**Function********************************************************************
+
+  Synopsis [Implements the recursive step of Cudd_bddAnd.]
+
+  Description [Implements the recursive step of Cudd_bddAnd by taking
+  the conjunction of two BDDs.  Returns a pointer to the result is
+  successful; NULL otherwise.]
+
+  SideEffects [None]
+
+  SeeAlso     [Cudd_bddAnd]
+
+******************************************************************************/
+DdNode *
+cuddBddAndRecurTime(
+  DdManager * manager,
+  DdNode * f,
+  DdNode * g,
+  int * pRecCalls,
+  int TimeOut)
+{
+    DdNode *F, *fv, *fnv, *G, *gv, *gnv;
+    DdNode *one, *r, *t, *e;
+    unsigned int topf, topg, index;
+
+    statLine(manager);
+    one = DD_ONE(manager);
+
+    /* Terminal cases. */
+    F = Cudd_Regular(f);
+    G = Cudd_Regular(g);
+    if (F == G) {
+    if (f == g) return(f);
+    else return(Cudd_Not(one));
+    }
+    if (F == one) {
+    if (f == one) return(g);
+    else return(f);
+    }
+    if (G == one) {
+    if (g == one) return(f);
+    else return(g);
+    }
+
+    /* At this point f and g are not constant. */
+    if (f > g) { /* Try to increase cache efficiency. */
+    DdNode *tmp = f;
+    f = g;
+    g = tmp;
+    F = Cudd_Regular(f);
+    G = Cudd_Regular(g);
+    }
+
+    /* Check cache. */
+    if (F->ref != 1 || G->ref != 1) {
+    r = cuddCacheLookup2(manager, Cudd_bddAnd, f, g);
+    if (r != NULL) return(r);
+    }
+
+    if ( TimeOut && ((*pRecCalls)++ % 10) == 0 && TimeOut < clock() )
+        return NULL;
+
+    /* Here we can skip the use of cuddI, because the operands are known
+    ** to be non-constant.
+    */
+    topf = manager->perm[F->index];
+    topg = manager->perm[G->index];
+
+    /* Compute cofactors. */
+    if (topf <= topg) {
+    index = F->index;
+    fv = cuddT(F);
+    fnv = cuddE(F);
+    if (Cudd_IsComplement(f)) {
+        fv = Cudd_Not(fv);
+        fnv = Cudd_Not(fnv);
+    }
+    } else {
+    index = G->index;
+    fv = fnv = f;
+    }
+
+    if (topg <= topf) {
+    gv = cuddT(G);
+    gnv = cuddE(G);
+    if (Cudd_IsComplement(g)) {
+        gv = Cudd_Not(gv);
+        gnv = Cudd_Not(gnv);
+    }
+    } else {
+    gv = gnv = g;
+    }
+
+    t = cuddBddAndRecurTime(manager, fv, gv, pRecCalls, TimeOut);
+    if (t == NULL) return(NULL);
+    cuddRef(t);
+
+    e = cuddBddAndRecurTime(manager, fnv, gnv, pRecCalls, TimeOut);
+    if (e == NULL) {
+    Cudd_IterDerefBdd(manager, t);
+    return(NULL);
+    }
+    cuddRef(e);
+
+    if (t == e) {
+    r = t;
+    } else {
+    if (Cudd_IsComplement(t)) {
+        r = cuddUniqueInter(manager,(int)index,Cudd_Not(t),Cudd_Not(e));
+        if (r == NULL) {
+        Cudd_IterDerefBdd(manager, t);
+        Cudd_IterDerefBdd(manager, e);
+        return(NULL);
+        }
+        r = Cudd_Not(r);
+    } else {
+        r = cuddUniqueInter(manager,(int)index,t,e);
+        if (r == NULL) {
+        Cudd_IterDerefBdd(manager, t);
+        Cudd_IterDerefBdd(manager, e);
+        return(NULL);
+        }
+    }
+    }
+    cuddDeref(e);
+    cuddDeref(t);
+    if (F->ref != 1 || G->ref != 1)
+    cuddCacheInsert2(manager, Cudd_bddAnd, f, g, r);
+    return(r);
+
+} /* end of cuddBddAndRecur */
+
+
+/**Function********************************************************************
+
+  Synopsis [Takes the AND of two BDDs and simultaneously abstracts the
+  variables in cube.]
+
+  Description [Takes the AND of two BDDs and simultaneously abstracts
+  the variables in cube. The variables are existentially abstracted.
+  Returns a pointer to the result is successful; NULL otherwise.]
+
+  SideEffects [None]
+
+  SeeAlso     [Cudd_bddAndAbstract]
+
+******************************************************************************/
+DdNode *
+cuddBddAndAbstractRecurTime(
+  DdManager * manager,
+  DdNode * f,
+  DdNode * g,
+  DdNode * cube,
+  int * pRecCalls,
+  int TimeOut)
+{
+    DdNode *F, *ft, *fe, *G, *gt, *ge;
+    DdNode *one, *zero, *r, *t, *e;
+    unsigned int topf, topg, topcube, top, index;
+
+    statLine(manager);
+    one = DD_ONE(manager);
+    zero = Cudd_Not(one);
+
+    /* Terminal cases. */
+    if (f == zero || g == zero || f == Cudd_Not(g)) return(zero);
+    if (f == one && g == one)    return(one);
+
+    if (cube == one) {
+    return(cuddBddAndRecurTime(manager, f, g, pRecCalls, TimeOut));
+    }
+    if (f == one || f == g) {
+    return(cuddBddExistAbstractRecur(manager, g, cube));
+    }
+    if (g == one) {
+    return(cuddBddExistAbstractRecur(manager, f, cube));
+    }
+    /* At this point f, g, and cube are not constant. */
+
+    if (f > g) { /* Try to increase cache efficiency. */
+    DdNode *tmp = f;
+    f = g;
+    g = tmp;
+    }
+
+    /* Here we can skip the use of cuddI, because the operands are known
+    ** to be non-constant.
+    */
+    F = Cudd_Regular(f);
+    G = Cudd_Regular(g);
+    topf = manager->perm[F->index];
+    topg = manager->perm[G->index];
+    top = ddMin(topf, topg);
+    topcube = manager->perm[cube->index];
+
+    while (topcube < top) {
+    cube = cuddT(cube);
+    if (cube == one) {
+        return(cuddBddAndRecurTime(manager, f, g, pRecCalls, TimeOut));
+    }
+    topcube = manager->perm[cube->index];
+    }
+    /* Now, topcube >= top. */
+
+    /* Check cache. */
+    if (F->ref != 1 || G->ref != 1) {
+    r = cuddCacheLookup(manager, DD_BDD_AND_ABSTRACT_TAG, f, g, cube);
+    if (r != NULL) {
+        return(r);
+    }
+    }
+
+    if ( TimeOut && ((*pRecCalls)++ % 10) == 0 && TimeOut < clock() )
+        return NULL;
+
+    if (topf == top) {
+    index = F->index;
+    ft = cuddT(F);
+    fe = cuddE(F);
+    if (Cudd_IsComplement(f)) {
+        ft = Cudd_Not(ft);
+        fe = Cudd_Not(fe);
+    }
+    } else {
+    index = G->index;
+    ft = fe = f;
+    }
+
+    if (topg == top) {
+    gt = cuddT(G);
+    ge = cuddE(G);
+    if (Cudd_IsComplement(g)) {
+        gt = Cudd_Not(gt);
+        ge = Cudd_Not(ge);
+    }
+    } else {
+    gt = ge = g;
+    }
+
+    if (topcube == top) {    /* quantify */
+    DdNode *Cube = cuddT(cube);
+    t = cuddBddAndAbstractRecurTime(manager, ft, gt, Cube, pRecCalls, TimeOut);
+    if (t == NULL) return(NULL);
+    /* Special case: 1 OR anything = 1. Hence, no need to compute
+    ** the else branch if t is 1. Likewise t + t * anything == t.
+    ** Notice that t == fe implies that fe does not depend on the
+    ** variables in Cube. Likewise for t == ge.
+    */
+    if (t == one || t == fe || t == ge) {
+        if (F->ref != 1 || G->ref != 1)
+        cuddCacheInsert(manager, DD_BDD_AND_ABSTRACT_TAG,
+                f, g, cube, t);
+        return(t);
+    }
+    cuddRef(t);
+    /* Special case: t + !t * anything == t + anything. */
+    if (t == Cudd_Not(fe)) {
+        e = cuddBddExistAbstractRecur(manager, ge, Cube);
+    } else if (t == Cudd_Not(ge)) {
+        e = cuddBddExistAbstractRecur(manager, fe, Cube);
+    } else {
+        e = cuddBddAndAbstractRecurTime(manager, fe, ge, Cube, pRecCalls, TimeOut);
+    }
+    if (e == NULL) {
+        Cudd_IterDerefBdd(manager, t);
+        return(NULL);
+    }
+    if (t == e) {
+        r = t;
+        cuddDeref(t);
+    } else {
+        cuddRef(e);
+        r = cuddBddAndRecurTime(manager, Cudd_Not(t), Cudd_Not(e), pRecCalls, TimeOut);
+        if (r == NULL) {
+        Cudd_IterDerefBdd(manager, t);
+        Cudd_IterDerefBdd(manager, e);
+        return(NULL);
+        }
+        r = Cudd_Not(r);
+        cuddRef(r);
+        Cudd_DelayedDerefBdd(manager, t);
+        Cudd_DelayedDerefBdd(manager, e);
+        cuddDeref(r);
+    }
+    } else {
+    t = cuddBddAndAbstractRecurTime(manager, ft, gt, cube, pRecCalls, TimeOut);
+    if (t == NULL) return(NULL);
+    cuddRef(t);
+    e = cuddBddAndAbstractRecurTime(manager, fe, ge, cube, pRecCalls, TimeOut);
+    if (e == NULL) {
+        Cudd_IterDerefBdd(manager, t);
+        return(NULL);
+    }
+    if (t == e) {
+        r = t;
+        cuddDeref(t);
+    } else {
+        cuddRef(e);
+        if (Cudd_IsComplement(t)) {
+        r = cuddUniqueInter(manager, (int) index,
+                    Cudd_Not(t), Cudd_Not(e));
+        if (r == NULL) {
+            Cudd_IterDerefBdd(manager, t);
+            Cudd_IterDerefBdd(manager, e);
+            return(NULL);
+        }
+        r = Cudd_Not(r);
+        } else {
+        r = cuddUniqueInter(manager,(int)index,t,e);
+        if (r == NULL) {
+            Cudd_IterDerefBdd(manager, t);
+            Cudd_IterDerefBdd(manager, e);
+            return(NULL);
+        }
+        }
+        cuddDeref(e);
+        cuddDeref(t);
+    }
+    }
+
+    if (F->ref != 1 || G->ref != 1)
+    cuddCacheInsert(manager, DD_BDD_AND_ABSTRACT_TAG, f, g, cube, r);
+    return (r);
+
+} /* end of cuddBddAndAbstractRecur */
+
+/*---------------------------------------------------------------------------*/
+/* Definition of static functions                                            */
+/*---------------------------------------------------------------------------*/
+
+
+////////////////////////////////////////////////////////////////////////
+///                           END OF FILE                            ///
+////////////////////////////////////////////////////////////////////////
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/misc/extra/module.make b/src/misc/extra/module.make
index c7c9be4e..7e4b5e30 100644
--- a/src/misc/extra/module.make
+++ b/src/misc/extra/module.make
@@ -4,6 +4,7 @@ SRC +=    src/misc/extra/extraBddAuto.c \
     src/misc/extra/extraBddKmap.c \
     src/misc/extra/extraBddMisc.c \
     src/misc/extra/extraBddSymm.c \
+    src/misc/extra/extraBddTime.c \
     src/misc/extra/extraBddUnate.c \
     src/misc/extra/extraUtilBitMatrix.c \
     src/misc/extra/extraUtilCanon.c \