Added handling runtime limit inside And and AndExist.

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

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;

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
 

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;

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

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 \