Other improvements to bmc2 and bmc3.

1 files changed, 116 insertions, 73 deletions

diff --git a/src/aig/saig/saigBmc3.c b/src/aig/saig/saigBmc3.c
index 5b36c01a..f97bd5da 100644
--- a/src/aig/saig/saigBmc3.c
+++ b/src/aig/saig/saigBmc3.c
@@ -42,13 +42,19 @@ struct Gia_ManBmc_t_
     Vec_Int_t *       vId2Num;     // number of each node 
     Vec_Ptr_t *       vTerInfo;    // ternary information
     Vec_Ptr_t *       vId2Var;     // SAT vars for each object
+    // hash table
+    unsigned *        pTable;
+    int               nTable;
+    int               nHashHit;
+    int               nHashMiss;
+    int               nHashOver;
+    int               nBufNum;     // the number of simple nodes
+    int               nDupNum;     // the number of simple nodes
     // SAT solver
     sat_solver *      pSat;        // SAT solver
     int               nSatVars;    // SAT variables
     int               nObjNums;    // SAT objects
     int               nWordNum;    // unsigned words for ternary simulation
-    int               nBufNum;     // the number of simple nodes
-    int               nDupNum;     // the number of simple nodes
     char * pSopSizes, ** pSops;    // CNF representation
 };
 
@@ -692,6 +698,9 @@ Gia_ManBmc_t * Saig_Bmc3ManStart( Aig_Man_t * pAig )
     Cnf_ReadMsops( &p->pSopSizes, &p->pSops );
     // terminary simulation 
     p->nWordNum = Abc_BitWordNum( 2 * Aig_ManObjNumMax(pAig) );
+    // hash table
+    p->nTable = 1000003;
+    p->pTable = ABC_CALLOC( unsigned, 6 * p->nTable ); // 2.4 Mb
     return p;
 }
 
@@ -708,6 +717,9 @@ Gia_ManBmc_t * Saig_Bmc3ManStart( Aig_Man_t * pAig )
 ***********************************************************************/
 void Saig_Bmc3ManStop( Gia_ManBmc_t * p )
 {
+    if ( p->pPars->fVerbose )
+    printf( "Buffs = %d. Dups = %d.   Hash hits = %d.  Hash misses = %d.  Hash overs = %d.\n", 
+        p->nBufNum, p->nDupNum, p->nHashHit, p->nHashMiss, p->nHashOver );
 //    Aig_ManCleanMarkA( p->pAig );
     if ( p->vCexes )
     {
@@ -722,10 +734,11 @@ void Saig_Bmc3ManStop( Gia_ManBmc_t * p )
     Vec_VecFree( (Vec_Vec_t *)p->vId2Var );
     Vec_PtrFreeFree( p->vTerInfo );
     sat_solver_delete( p->pSat );
-    free( p->pSopSizes );
-    free( p->pSops[1] );
-    free( p->pSops );
-    free( p );
+    ABC_FREE( p->pTable );
+    ABC_FREE( p->pSopSizes );
+    ABC_FREE( p->pSops[1] );
+    ABC_FREE( p->pSops );
+    ABC_FREE( p );
 }
 
 
@@ -809,23 +822,24 @@ static inline int Saig_ManBmcCof0( int t, int v )
     static int s_Truth[4] = { 0xAAAA, 0xCCCC, 0xF0F0, 0xFF00 };
     return 0xffff & ((t & ~s_Truth[v]) | ((t & ~s_Truth[v]) << (1<<v)));
 }
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
 static inline int Saig_ManBmcCof1( int t, int v )
 {
     static int s_Truth[4] = { 0xAAAA, 0xCCCC, 0xF0F0, 0xFF00 };
     return 0xffff & ((t & s_Truth[v]) | ((t & s_Truth[v]) >> (1<<v)));
 }
+static inline int Saig_ManBmcCofEqual( int t, int v )
+{
+    assert( v >= 0 && v <= 3 );
+    if ( v == 0 )
+        return ((t & 0xAAAA) >> 1) == (t & 0x5555);
+    if ( v == 1 )
+        return ((t & 0xCCCC) >> 2) == (t & 0x3333);
+    if ( v == 2 )
+        return ((t & 0xF0F0) >> 4) == (t & 0x0F0F);
+    if ( v == 3 )
+        return ((t & 0xFF00) >> 8) == (t & 0x00FF);
+    return -1;
+}
 
 /**Function*************************************************************
 
@@ -838,7 +852,7 @@ static inline int Saig_ManBmcCof1( int t, int v )
   SeeAlso     []
 
 ***********************************************************************/
-static inline int Saig_ManBmcDeriveTruth( int uTruth, int Lits[] )
+static inline int Saig_ManBmcReduceTruth( int uTruth, int Lits[] )
 {
     int v;
     for ( v = 0; v < 4; v++ )
@@ -854,7 +868,9 @@ static inline int Saig_ManBmcDeriveTruth( int uTruth, int Lits[] )
         }
     for ( v = 0; v < 4; v++ )
         if ( Lits[v] == -1 )
-            assert( Saig_ManBmcCof0(uTruth, v) == Saig_ManBmcCof1(uTruth, v) );
+            assert( Saig_ManBmcCofEqual(uTruth, v) );
+        else if ( Saig_ManBmcCofEqual(uTruth, v) )
+            Lits[v] = -1;
     return uTruth;
 }
 
@@ -978,6 +994,51 @@ static inline void Saig_ManBmcAddClauses( Gia_ManBmc_t * p, int uTruth, int Lits
     }
 }
 
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline unsigned Saig_ManBmcHashKey( unsigned * pArray )
+{
+    static s_Primes[5] = { 12582917, 25165843, 50331653, 100663319, 201326611 };
+    unsigned i, Key = 0;
+    for ( i = 0; i < 5; i++ )
+        Key += pArray[i] * s_Primes[i];
+    return Key;
+}
+static inline int * Saig_ManBmcLookup( Gia_ManBmc_t * p, unsigned * pArray )
+{
+    unsigned * pTable = p->pTable + 6 * (Saig_ManBmcHashKey(pArray) % p->nTable);
+/*
+int i;
+for ( i = 0; i < 5; i++ )
+printf( "%6d ", pArray[i] );
+printf( "\n" );
+*/
+    if ( memcmp( pTable, pArray, 20 ) )
+    {
+        if ( pTable[0] == 0 )
+            p->nHashMiss++;
+        else
+            p->nHashOver++;
+        memcpy( pTable, pArray, 20 );
+        pTable[5] = 0;
+    }
+    else
+        p->nHashHit++;
+
+    assert( pTable + 5 < pTable + 6 * p->nTable );
+    return (int *)(pTable + 5);
+}
+
 /**Function*************************************************************
 
   Synopsis    [Derives CNF for one node.]
@@ -989,10 +1050,10 @@ static inline void Saig_ManBmcAddClauses( Gia_ManBmc_t * p, int uTruth, int Lits
   SeeAlso     []
 
 ***********************************************************************/
-int Saig_ManBmcCreateCnf_rec( Gia_ManBmc_t * p, Aig_Obj_t * pObj, int iFrame, int fAddClauses )
+int Saig_ManBmcCreateCnf_rec( Gia_ManBmc_t * p, Aig_Obj_t * pObj, int iFrame )
 {
-    int * pMapping, i, iLit, Lits[4], uTruth;
-    assert( fAddClauses );
+    extern unsigned Dar_CutSortVars( unsigned uTruth, int * pVars );
+    int * pMapping, * pLookup, i, iLit, Lits[5], uTruth;
     iLit = Saig_ManBmcLiteral( p, pObj, iFrame );
     if ( iLit != ~0 )
         return iLit; 
@@ -1000,14 +1061,14 @@ int Saig_ManBmcCreateCnf_rec( Gia_ManBmc_t * p, Aig_Obj_t * pObj, int iFrame, in
     if ( Aig_ObjIsCi(pObj) )
     {
         if ( Saig_ObjIsPi(p->pAig, pObj) )
-            iLit = fAddClauses ? toLit( p->nSatVars++ ) : ABC_INFINITY;
+            iLit = toLit( p->nSatVars++ );
         else
-            iLit = Saig_ManBmcCreateCnf_rec( p, Saig_ObjLoToLi(p->pAig, pObj), iFrame-1, fAddClauses );
+            iLit = Saig_ManBmcCreateCnf_rec( p, Saig_ObjLoToLi(p->pAig, pObj), iFrame-1 );
         return Saig_ManBmcSetLiteral( p, pObj, iFrame, iLit );
     }
     if ( Aig_ObjIsCo(pObj) )
     {
-        iLit = Saig_ManBmcCreateCnf_rec( p, Aig_ObjFanin0(pObj), iFrame, fAddClauses );
+        iLit = Saig_ManBmcCreateCnf_rec( p, Aig_ObjFanin0(pObj), iFrame );
         if ( Aig_ObjFaninC0(pObj) )
             iLit = lit_neg(iLit);
         return Saig_ManBmcSetLiteral( p, pObj, iFrame, iLit );
@@ -1018,62 +1079,44 @@ int Saig_ManBmcCreateCnf_rec( Gia_ManBmc_t * p, Aig_Obj_t * pObj, int iFrame, in
         if ( pMapping[i+1] == -1 )
             Lits[i] = -1;
         else
-            Lits[i] = Saig_ManBmcCreateCnf_rec( p, Aig_ManObj(p->pAig, pMapping[i+1]), iFrame, fAddClauses );
-    // derive new truth table
-//uTruth = 0xffff & (unsigned)pMapping[0];
-//printf( "Truth : " );
-//Extra_PrintBinary( stdout, &uTruth, 16 ); printf( "\n" );
-    uTruth = Saig_ManBmcDeriveTruth( 0xffff & (unsigned)pMapping[0], Lits );
+            Lits[i] = Saig_ManBmcCreateCnf_rec( p, Aig_ManObj(p->pAig, pMapping[i+1]), iFrame );
+    uTruth = 0xffff & (unsigned)pMapping[0];
+    // propagate constants
+    uTruth = Saig_ManBmcReduceTruth( uTruth, Lits );
     if ( uTruth == 0 || uTruth == 0xffff )
     {
         iLit = (uTruth == 0xffff);
         return Saig_ManBmcSetLiteral( p, pObj, iFrame, iLit );
     }
-    // create CNF
-    if ( fAddClauses )
+    // canonicize inputs
+    uTruth = Dar_CutSortVars( uTruth, Lits );
+    assert( uTruth != 0 && uTruth != 0xffff );
+    if ( uTruth == 0xAAAA || uTruth == 0x5555 )
     {
-        if ( uTruth == 0xAAAA || (0xffff & ~uTruth) == 0xAAAA ||
-             uTruth == 0xCCCC || (0xffff & ~uTruth) == 0xCCCC ||
-             uTruth == 0xF0F0 || (0xffff & ~uTruth) == 0xF0F0 ||
-             uTruth == 0xFF00 || (0xffff & ~uTruth) == 0xFF00 )
-        {
-            p->nBufNum++;
-
-            if ( uTruth == 0xAAAA )
-                iLit = Lits[0];
-            else if ( uTruth == 0xCCCC )
-                iLit = Lits[1];
-            else if ( uTruth == 0xF0F0 )
-                iLit = Lits[2];
-            else if ( uTruth == 0xFF00 )
-                iLit = Lits[3];
-            else if ( (0xffff & ~uTruth) == 0xAAAA )
-                iLit = Abc_LitNot(Lits[0]);
-            else if ( (0xffff & ~uTruth) == 0xCCCC )
-                iLit = Abc_LitNot(Lits[1]);
-            else if ( (0xffff & ~uTruth) == 0xF0F0 )
-                iLit = Abc_LitNot(Lits[2]);
-            else if ( (0xffff & ~uTruth) == 0xFF00 )
-                iLit = Abc_LitNot(Lits[3]);
-
-        }
-        else
+        iLit = Abc_LitNotCond( Lits[0], uTruth == 0x5555 );
+        p->nBufNum++;
+    }
+    else 
+    {
+        assert( !(uTruth == 0xAAAA || (0xffff & ~uTruth) == 0xAAAA ||
+                  uTruth == 0xCCCC || (0xffff & ~uTruth) == 0xCCCC ||
+                  uTruth == 0xF0F0 || (0xffff & ~uTruth) == 0xF0F0 ||
+                  uTruth == 0xFF00 || (0xffff & ~uTruth) == 0xFF00) );
+
+        Lits[4] = uTruth;
+        pLookup = Saig_ManBmcLookup( p, Lits );
+        if ( *pLookup == 0 )
         {
-            iLit = toLit( p->nSatVars++ );
-            Saig_ManBmcAddClauses( p, uTruth, Lits, iLit );
+            *pLookup = toLit( p->nSatVars++ );
+            Saig_ManBmcAddClauses( p, uTruth, Lits, *pLookup );
 
             if ( (Lits[0] > 1 && (Lits[0] == Lits[1] || Lits[0] == Lits[2] || Lits[0] == Lits[3]))   ||
                  (Lits[1] > 1 && (Lits[1] == Lits[2] || Lits[1] == Lits[2]))                         ||
                  (Lits[2] > 1 && (Lits[2] == Lits[3]))    )
                        p->nDupNum++;
         }
-
-    }
-    else
-    {
-        iLit = ABC_INFINITY;
+        iLit = *pLookup;
     }
-//    assert( iLit != ABC_INFINITY );
     return Saig_ManBmcSetLiteral( p, pObj, iFrame, iLit );
 }
 
@@ -1142,7 +1185,7 @@ int Saig_ManBmcCreateCnf( Gia_ManBmc_t * p, Aig_Obj_t * pObj, int iFrame )
     if ( Value != SAIG_TER_UND )
         return (int)(Value == SAIG_TER_ONE);
     // construct CNF if value is ternary
-    return Saig_ManBmcCreateCnf_rec( p, pObj, iFrame, 1 );
+    return Saig_ManBmcCreateCnf_rec( p, pObj, iFrame );
 }
 
 
@@ -1358,8 +1401,8 @@ clkOther += clock() - clk2;
 //                        printf( "\n" );
 //                        ABC_PRMn( "Id2Var", (f+1)*p->nObjNums*4 );
 //                        ABC_PRMn( "SAT", 42 * p->pSat->size + 16 * (int)p->pSat->stats.clauses + 4 * (int)p->pSat->stats.clauses_literals );
-                        printf( "S =%6d. ", p->nBufNum );
-                        printf( "D =%6d. ", p->nDupNum );
+//                        printf( "S =%6d. ", p->nBufNum );
+//                        printf( "D =%6d. ", p->nDupNum );
                         printf( "\n" );
                         fflush( stdout );
                     }
@@ -1422,8 +1465,8 @@ clkOther += clock() - clk2;
 //            printf( "\n" );
 //            ABC_PRMn( "Id2Var", (f+1)*p->nObjNums*4 );
 //            ABC_PRMn( "SAT", 42 * p->pSat->size + 16 * (int)p->pSat->stats.clauses + 4 * (int)p->pSat->stats.clauses_literals );
-            printf( "Simples = %6d. ", p->nBufNum );
-            printf( "Dups = %6d. ", p->nDupNum );
+//            printf( "Simples = %6d. ", p->nBufNum );
+//            printf( "Dups = %6d. ", p->nDupNum );
             printf( "\n" );
             fflush( stdout );
         }