Improvements to timeout.

5 files changed, 192 insertions, 56 deletions

diff --git a/abclib.dsp b/abclib.dsp
index d0007d9b..62267cbe 100644
--- a/abclib.dsp
+++ b/abclib.dsp
@@ -2027,6 +2027,10 @@ SOURCE=.\src\map\if\ifCut.c
 # End Source File
 # Begin Source File
 
+SOURCE=.\src\map\if\ifDec.c
+# End Source File
+# Begin Source File
+
 SOURCE=.\src\map\if\ifLib.c
 # End Source File
 # Begin Source File
diff --git a/src/aig/llb/llb4Nonlin.c b/src/aig/llb/llb4Nonlin.c
index c87c13c2..25ef8c96 100644
--- a/src/aig/llb/llb4Nonlin.c
+++ b/src/aig/llb/llb4Nonlin.c
@@ -659,14 +659,6 @@ int Llb_Nonlin4Reachability( Llb_Mnx_t * p )
     int clkTemp, clkIter, clk = clock();
     assert( Aig_ManRegNum(p->pAig) > 0 );
 
-    // compute time to stop
-    if ( p->pPars->TimeLimit )
-        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;
-
     if ( p->pPars->fBackward )
     {
         // create bad state in the ring manager
@@ -935,11 +927,18 @@ Llb_Mnx_t * Llb_MnxStart( Aig_Man_t * pAig, Gia_ParLlb_t * pPars )
     p->pAig    = pAig;
     p->pPars   = pPars;
 
+    // compute time to stop
+    if ( p->pPars->TimeLimit )
+        p->pPars->TimeTarget = clock() + p->pPars->TimeLimit * CLOCKS_PER_SEC;
+    else
+        p->pPars->TimeTarget = 0;
     if ( pPars->fCluster )
     {
 //        Llb_Nonlin4Cluster( p->pAig, &p->dd, &p->vOrder, &p->vRoots, pPars->nBddMax, pPars->fVerbose );
 //        Cudd_AutodynEnable( p->dd,  CUDD_REORDER_SYMM_SIFT );
         Llb4_Nonlin4Sweep( p->pAig, pPars->nBddMax, pPars->nClusterMax, &p->dd, &p->vOrder, &p->vRoots, pPars->fVerbose );
+        // set the stop time parameter
+        p->dd->TimeStop  = p->pPars->TimeTarget;
     }
     else
     {
@@ -948,6 +947,8 @@ Llb_Mnx_t * Llb_MnxStart( Aig_Man_t * pAig, Gia_ParLlb_t * pPars )
         p->dd      = Cudd_Init( Vec_IntSize(p->vOrder), 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
         Cudd_AutodynEnable( p->dd,  CUDD_REORDER_SYMM_SIFT );
         Cudd_SetMaxGrowth( p->dd, 1.05 );
+        // set the stop time parameter
+        p->dd->TimeStop  = p->pPars->TimeTarget;
         p->vRoots  = Llb_Nonlin4DerivePartitions( p->dd, pAig, p->vOrder );
     }
 
@@ -994,13 +995,15 @@ void Llb_MnxStop( Llb_Mnx_t * p )
         Cudd_RecursiveDeref( p->dd, p->bCurrent );
     if ( p->bNext )
         Cudd_RecursiveDeref( p->dd, p->bNext );
+    if ( p->vRings );
     Vec_PtrForEachEntry( DdNode *, p->vRings, bTemp, i )
         Cudd_RecursiveDeref( p->dd, bTemp );
+    if ( p->vRoots )
     Vec_PtrForEachEntry( DdNode *, p->vRoots, bTemp, i )
         Cudd_RecursiveDeref( p->dd, bTemp );
     // remove arrays
-    Vec_PtrFree( p->vRings );
-    Vec_PtrFree( p->vRoots );
+    Vec_PtrFreeP( &p->vRings );
+    Vec_PtrFreeP( &p->vRoots );
 //Cudd_PrintInfo( p->dd, stdout );
     Extra_StopManager( p->dd );
     Vec_IntFreeP( &p->vOrder );
diff --git a/src/base/main/main.c b/src/base/main/main.c
index cf8e855e..16c6e362 100644
--- a/src/base/main/main.c
+++ b/src/base/main/main.c
@@ -64,8 +64,10 @@ int Abc_RealMain( int argc, char * argv[] )
     char * sCommand;
     int  fStatus = 0;
     int c, fBatch, fInitSource, fInitRead, fFinalWrite;
-
-    // added to detect memory leaks:
+ 
+    // added to detect memory leaks
+    // watch for {,,msvcrtd.dll}*__p__crtBreakAlloc()
+    // (http://support.microsoft.com/kb/151585)
 #if defined(_DEBUG) && defined(_MSC_VER) 
     _CrtSetDbgFlag( _CRTDBG_ALLOC_MEM_DF | _CRTDBG_LEAK_CHECK_DF );
 #endif
diff --git a/src/map/if/ifDec.c b/src/map/if/ifDec.c
index e5656d9e..7409c05a 100644
--- a/src/map/if/ifDec.c
+++ b/src/map/if/ifDec.c
@@ -62,15 +62,41 @@ static word Truth7[7][2] = {
     0xFF00FF00FF00FF00,0xFF00FF00FF00FF00,
     0xFFFF0000FFFF0000,0xFFFF0000FFFF0000,
     0xFFFFFFFF00000000,0xFFFFFFFF00000000,
-    0xFFFFFFFFFFFFFFFF,0x0000000000000000
+    0x0000000000000000,0xFFFFFFFFFFFFFFFF
 };
 
 extern void Kit_DsdPrintFromTruth( unsigned * pTruth, int nVars );
+extern void Extra_PrintBinary( FILE * pFile, unsigned Sign[], int nBits );
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
+static void If_DecPrintConfig( word z )
+{
+   unsigned S[1];
+   S[0] = (z & 0xffff) | ((z & 0xffff) << 16);
+   Extra_PrintBinary( stdout, S, 16 ); 
+   printf( " " );
+   Kit_DsdPrintFromTruth( S, 4 );
+   printf( " " );
+   printf( " %d", (z >> 16) & 7 );
+   printf( " %d", (z >> 20) & 7 );
+   printf( " %d", (z >> 24) & 7 );
+   printf( " %d", (z >> 28) & 7 );
+   printf( "   " );
+   S[0] = ((z >> 32) & 0xffff) | (((z >> 32) & 0xffff) << 16);
+   Extra_PrintBinary( stdout, S, 16 );
+   printf( " " );
+   Kit_DsdPrintFromTruth( S, 4 );
+   printf( " " );
+   printf( " %d", (z >> 48) & 7 );
+   printf( " %d", (z >> 52) & 7 );
+   printf( " %d", (z >> 56) & 7 );
+   printf( " %d", (z >> 60) & 7 );
+   printf( "\n" );
+}
+
 // verification for 6-input function
 static word If_Dec6ComposeLut4( int t, word f[4] )
 {
@@ -78,6 +104,8 @@ static word If_Dec6ComposeLut4( int t, word f[4] )
     word c, r = 0;
     for ( m = 0; m < 16; m++ )
     {
+        if ( !((t >> m) & 1) )
+            continue;
         c = ~0;
         for ( v = 0; v < 4; v++ )
             c &= ((m >> v) & 1) ? f[v] : ~f[v];
@@ -87,22 +115,30 @@ static word If_Dec6ComposeLut4( int t, word f[4] )
 }
 static void If_Dec6Verify( word t, word z )
 {
-    word f[4];
+    word r, q, f[4];
     int i, v;
+    assert( z );
     for ( i = 0; i < 4; i++ )
     {
         v = (z >> (16+(i<<2))) & 7;
-        f[i] = (v == 7) ? 0 : Truth6[v];
+        assert( v != 7 );
+        f[i] = Truth6[v];
     }
-    f[0] = If_Dec6ComposeLut4( (int)(z & 0xffff), f );
-    for ( i = 0; i < 3; i++ )
+    q = If_Dec6ComposeLut4( (int)(z & 0xffff), f );
+    for ( i = 0; i < 4; i++ )
     {
         v = (z >> (48+(i<<2))) & 7;
-        f[i+1] = (v == 7) ? 0 : Truth6[v];
+        f[i] = (v == 7) ? q : Truth6[v];
     }
-    f[0] = If_Dec6ComposeLut4( (int)((z >> 32) & 0xffff), f );
-    if ( f[0] != t )
+    r = If_Dec6ComposeLut4( (int)((z >> 32) & 0xffff), f );
+    if ( r != t )
+    {
+        If_DecPrintConfig( z );
+        Kit_DsdPrintFromTruth( (unsigned*)&t, 6 ); printf( "\n" );
+        Kit_DsdPrintFromTruth( (unsigned*)&q, 6 ); printf( "\n" );
+        Kit_DsdPrintFromTruth( (unsigned*)&r, 6 ); printf( "\n" );
         printf( "Verification failed!\n" );
+    }
 }
 // verification for 7-input function
 static void If_Dec7ComposeLut4( int t, word f[4][2], word r[2] )
@@ -112,6 +148,8 @@ static void If_Dec7ComposeLut4( int t, word f[4][2], word r[2] )
     r[0] = r[1] = 0;
     for ( m = 0; m < 16; m++ )
     {
+        if ( !((t >> m) & 1) )
+            continue;
         c[0] = c[1] = ~0;
         for ( v = 0; v < 4; v++ )
         {
@@ -126,6 +164,7 @@ static void If_Dec7Verify( word t[2], word z )
 {
     word f[4][2], r[2];
     int i, v;
+    assert( z );
     for ( i = 0; i < 4; i++ )
     {
         v = (z >> (16+(i<<2))) & 7;
@@ -133,19 +172,25 @@ static void If_Dec7Verify( word t[2], word z )
         f[i][1] = Truth7[v][1];
     }
     If_Dec7ComposeLut4( (int)(z & 0xffff), f, r );
-    f[0][0] = r[0];
-    f[0][1] = r[1];
+    f[3][0] = r[0];
+    f[3][1] = r[1];
     for ( i = 0; i < 3; i++ )
     {
         v = (z >> (48+(i<<2))) & 7;
-        f[i+1][0] = Truth7[v][0];
-        f[i+1][1] = Truth7[v][1];
+        f[i][0] = Truth7[v][0];
+        f[i][1] = Truth7[v][1];
     }
     If_Dec7ComposeLut4( (int)((z >> 32) & 0xffff), f, r );
     if ( r[0] != t[0] || r[1] != t[1] )
+    {
+        If_DecPrintConfig( z );
+        Kit_DsdPrintFromTruth( (unsigned*)t, 7 ); printf( "\n" );
+        Kit_DsdPrintFromTruth( (unsigned*)r, 7 ); printf( "\n" );
         printf( "Verification failed!\n" );
+    }
 }
 
+
 // count the number of unique cofactors
 static inline int If_Dec6CofCount2( word t )
 {
@@ -229,24 +274,106 @@ static inline void If_Dec7MoveTo( word t[2], int v, int p, int Pla2Var[7], int V
     assert( Pla2Var[p] == v );
 }
 
+// derive binary function
+static inline int If_Dec6DeriveCount2( word t, int * pCof0, int * pCof1 )
+{
+    int i, Mask = 0;
+    *pCof0 = (t & 15);
+    *pCof1 = (t & 15);
+    for ( i = 1; i < 16; i++ )
+        if ( *pCof0 != ((t >> (i<<2)) & 15) )
+        {
+            *pCof1 = ((t >> (i<<2)) & 15);
+            Mask |= (1 << i);
+        }
+    return Mask;
+}
+static inline int If_Dec7DeriveCount3( word t[2], int * pCof0, int * pCof1 )
+{
+    unsigned char * pTruth = (unsigned char *)t;
+    int i, Mask = 0;
+    *pCof0 = pTruth[0];
+    *pCof1 = pTruth[0];
+    for ( i = 1; i < 16; i++ )
+        if ( *pCof0 != pTruth[i] )
+        {
+            *pCof1 = pTruth[i];
+            Mask |= (1 << i);
+        }
+    return Mask;
+}
 
 // derives decomposition
+static inline word If_Dec6Cofactor( word t, int iVar, int fCof1 )
+{
+    assert( iVar >= 0 && iVar < 6 );
+    if ( fCof1 )
+        return (t & Truth6[iVar]) | ((t & Truth6[iVar]) >> (1<<iVar));
+    else
+        return (t &~Truth6[iVar]) | ((t &~Truth6[iVar]) << (1<<iVar));
+}
 static word If_Dec6DeriveDisjoint( word t, int Pla2Var[6], int Var2Pla[6] )
 {
-    word z = 1;
-//    If_Dec6Verify( t, z );
+    int i, Cof0, Cof1;
+    word z = If_Dec6DeriveCount2( t, &Cof0, &Cof1 );
+    for ( i = 0; i < 4; i++ )
+        z |= (((word)Pla2Var[i+2]) << (16 + 4*i));
+    z |= ((word)((Cof1 << 4) | Cof0) << 32);
+    z |= ((word)((Cof1 << 4) | Cof0) << 40);
+    for ( i = 0; i < 2; i++ )
+        z |= (((word)Pla2Var[i]) << (48 + 4*i));
+    z |= (((word)7) << (48 + 4*i++));
+    assert( i == 3 );
     return z;
 }
-static word If_Dec6DeriveNonDisjoint( word t, word c0, word c1, int s, int Pla2Var[6], int Var2Pla[6] )
+static word If_Dec6DeriveNonDisjoint( word t, int s, int Pla2Var0[6], int Var2Pla0[6] )
 {
-    word z = 1;
-//    If_Dec6Verify( t, z );
+    word z, c0, c1;
+    int Cof0[2], Cof1[2];
+    int Truth0, Truth1, i;
+    int Pla2Var[6], Var2Pla[6];
+    assert( s >= 2 && s <= 5 );
+    for ( i = 0; i < 6; i++ )
+    {
+        Pla2Var[i] = Pla2Var0[i];
+        Var2Pla[i] = Var2Pla0[i];
+    }
+    for ( i = s; i < 5; i++ )
+    {
+        t = If_Dec6SwapAdjacent( t, i );
+        Var2Pla[Pla2Var[i]]++;
+        Var2Pla[Pla2Var[i+1]]--;
+        Pla2Var[i] ^= Pla2Var[i+1];
+        Pla2Var[i+1] ^= Pla2Var[i];
+        Pla2Var[i] ^= Pla2Var[i+1];
+    }
+    c0 = If_Dec6Cofactor( t, 5, 0 );
+    c1 = If_Dec6Cofactor( t, 5, 1 );
+    assert( 2 >= If_Dec6CofCount2(c0) );
+    assert( 2 >= If_Dec6CofCount2(c1) );
+    Truth0 = If_Dec6DeriveCount2( c0, &Cof0[0], &Cof0[1] );
+    Truth1 = If_Dec6DeriveCount2( c1, &Cof1[0], &Cof1[1] );
+    z = ((Truth1 & 0xFF) << 8) | (Truth0 & 0xFF);
+    for ( i = 0; i < 4; i++ )
+        z |= (((word)Pla2Var[i+2]) << (16 + 4*i));
+    z |= ((word)((Cof0[1] << 4) | Cof0[0]) << 32);
+    z |= ((word)((Cof1[1] << 4) | Cof1[0]) << 40);
+    for ( i = 0; i < 2; i++ )
+        z |= (((word)Pla2Var[i]) << (48 + 4*i));
+    z |= (((word)7) << (48 + 4*i++));
+    z |= (((word)Pla2Var[5]) << (48 + 4*i++));
+    assert( i == 4 );
     return z;
 }
 static word If_Dec7DeriveDisjoint( word t[2], int Pla2Var[7], int Var2Pla[7] )
 {
-    word z = 1;
-//    If_Dec7Verify( t, z );
+    int i, Cof0, Cof1;
+    word z = If_Dec7DeriveCount3( t, &Cof0, &Cof1 );
+    for ( i = 0; i < 4; i++ )
+        z |= (((word)Pla2Var[i+3]) << (16 + 4*i));
+    z |= ((word)((Cof1 << 8) | Cof0) << 32);
+    for ( i = 0; i < 3; i++ )
+        z |= (((word)Pla2Var[i]) << (48 + 4*i));
     return z;
 }
 
@@ -269,21 +396,11 @@ static inline void If_DecVerifyPerm( int Pla2Var[6], int Var2Pla[6] )
     int i;
     for ( i = 0; i < 6; i++ )
         assert( Pla2Var[Var2Pla[i]] == i );
-}
-static inline word If_Dec6Cofactor( word t, int iVar, int fCof1 )
-{
-    assert( iVar >= 0 && iVar < 6 );
-    if ( fCof1 )
-        return (t & Truth6[iVar]) | ((t & Truth6[iVar]) >> (1<<iVar));
-    else
-        return (t &~Truth6[iVar]) | ((t &~Truth6[iVar]) << (1<<iVar));
-}
-static word If_Dec6Perform( word t )
+} 
+static word If_Dec6Perform( word t, int fDerive )
 { 
+    word r = 0;
     int i, v, u, x, Count, Pla2Var[6], Var2Pla[6];
-    int fFound = 0;
-//    if ( If_Dec6CountOnes(t) == 1 )
-//        return 1;
     // start arrays
     for ( i = 0; i < 6; i++ )
     {
@@ -301,27 +418,26 @@ static word If_Dec6Perform( word t )
         Count = If_Dec6CofCount2( t );
         assert( Count > 1 );
         if ( Count == 2 )
-            return If_Dec6DeriveDisjoint( t, Pla2Var, Var2Pla );
+            return !fDerive ? 1 : If_Dec6DeriveDisjoint( t, Pla2Var, Var2Pla );
         // check non-disjoint decomposition
-        if ( !fFound && (Count == 3 || Count == 4) )
+        if ( !r && (Count == 3 || Count == 4) )
         {
             for ( x = 0; x < 4; x++ )
             {
-                word c0 = If_Dec6Cofactor( t, Pla2Var[x+2], 0 );
-                word c1 = If_Dec6Cofactor( t, Pla2Var[x+2], 1 );
+                word c0 = If_Dec6Cofactor( t, x+2, 0 );
+                word c1 = If_Dec6Cofactor( t, x+2, 1 );
                 if ( If_Dec6CofCount2( c0 ) <= 2 && If_Dec6CofCount2( c1 ) <= 2 )
                 {
-                    fFound = 1;
+                    r = !fDerive ? 1 : If_Dec6DeriveNonDisjoint( t, x+2, Pla2Var, Var2Pla );
                     break;
-                 //   return If_Dec6DeriveNonDisjoint( t, c0, c1, x+2, Pla2Var, Var2Pla );
                 }
             }
         }
     }
     assert( i == 15 );
-    return fFound;
+    return r;
 }
-static word If_Dec7Perform( word t0[2] )
+static word If_Dec7Perform( word t0[2], int fDerive )
 {
     word t[2] = {t0[0], t0[1]}; 
     int i, v, u, y, Pla2Var[7], Var2Pla[7];
@@ -344,7 +460,9 @@ static word If_Dec7Perform( word t0[2] )
         If_Dec7MoveTo( t, y, 2, Pla2Var, Var2Pla );
 //        If_DecVerifyPerm( Pla2Var, Var2Pla );
         if ( If_Dec7CofCount3( t ) == 2 )
-            return If_Dec7DeriveDisjoint( t, Pla2Var, Var2Pla );
+        {
+            return !fDerive ? 1 : If_Dec7DeriveDisjoint( t, Pla2Var, Var2Pla );
+        }
     }
     return 0;
 }
@@ -363,19 +481,26 @@ static word If_Dec7Perform( word t0[2] )
 ***********************************************************************/
 int If_CutPerformCheckInt( unsigned * pTruth, int nVars, int nLeaves )
 {
+    int fDerive = 0;
     if ( nLeaves < 6 )
         return 1;
     if ( nLeaves == 6 )
     {
         word t = ((word *)pTruth)[0];
-        return If_Dec6Perform( t ) != 0;
+        word z = If_Dec6Perform( t, fDerive );
+        if ( fDerive && z )
+            If_Dec6Verify( t, z );
+        return z != 0;
     }
     if ( nLeaves == 7 )
     {
-        word t[2];
+        word t[2], z;
         t[0] = ((word *)pTruth)[0];
         t[1] = ((word *)pTruth)[1];
-        return If_Dec7Perform( t ) != 0;
+        z = If_Dec7Perform( t, fDerive );
+        if ( fDerive && z )
+            If_Dec7Verify( t, z );
+        return z != 0;
     }
     assert( 0 );
     return 0;
diff --git a/src/sat/pdr/pdrCnf.c b/src/sat/pdr/pdrCnf.c
index 2c5218d8..4b42262c 100644
--- a/src/sat/pdr/pdrCnf.c
+++ b/src/sat/pdr/pdrCnf.c
@@ -278,6 +278,7 @@ static inline sat_solver * Pdr_ManNewSolver1( Pdr_Man_t * p, int k, int fInit )
             Vec_IntWriteEntry( p->vVar2Reg, Pdr_ObjSatVar(p, k, pObj), i );
     }
     pSat = (sat_solver *)Cnf_DataWriteIntoSolver( p->pCnf1, 1, fInit );
+    sat_solver_set_runtime_limit( pSat, p->timeToStop );
     return pSat;
 }
 
@@ -322,6 +323,7 @@ static inline sat_solver * Pdr_ManNewSolver2( Pdr_Man_t * p, int k, int fInit )
     // start the SAT solver
     pSat = sat_solver_new();
     sat_solver_setnvars( pSat, 500 );
+    sat_solver_set_runtime_limit( pSat, p->timeToStop );
     return pSat;
 }