Improvements to 'satclp'.

5 files changed, 356 insertions, 25 deletions

diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index 6b801b9e..4ad3e39a 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -1452,6 +1452,7 @@ extern int                 Gia_ObjRecognizeExor( Gia_Obj_t * pObj, Gia_Obj_t **
 extern Gia_Obj_t *         Gia_ObjRecognizeMux( Gia_Obj_t * pNode, Gia_Obj_t ** ppNodeT, Gia_Obj_t ** ppNodeE );
 extern int                 Gia_ObjRecognizeMuxLits( Gia_Man_t * p, Gia_Obj_t * pNode, int * iLitT, int * iLitE );
 extern int                 Gia_NodeMffcSize( Gia_Man_t * p, Gia_Obj_t * pNode );
+extern int                 Gia_NodeMffcSizeSupp( Gia_Man_t * p, Gia_Obj_t * pNode, Vec_Int_t * vSupp );
 extern int                 Gia_ManHasDangling( Gia_Man_t * p );
 extern int                 Gia_ManMarkDangling( Gia_Man_t * p );
 extern Vec_Int_t *         Gia_ManGetDangling( Gia_Man_t * p );
diff --git a/src/aig/gia/giaUtil.c b/src/aig/gia/giaUtil.c
index ae32b91e..ff44eecf 100644
--- a/src/aig/gia/giaUtil.c
+++ b/src/aig/gia/giaUtil.c
@@ -1143,6 +1143,47 @@ int Gia_NodeMffcSize( Gia_Man_t * p, Gia_Obj_t * pNode )
 
 /**Function*************************************************************
 
+  Synopsis    [Returns the number of internal nodes in the MFFC.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Gia_NodeCollect_rec( Gia_Man_t * p, Gia_Obj_t * pNode, Vec_Int_t * vSupp )
+{
+    if ( Gia_ObjIsTravIdCurrent(p, pNode) )
+        return;
+    Gia_ObjSetTravIdCurrent(p, pNode);
+    if ( Gia_ObjRefNum(p, pNode) || Gia_ObjIsCi(pNode) )
+    {
+        Vec_IntPush( vSupp, Gia_ObjId(p, pNode) );
+        return;
+    }
+    assert( Gia_ObjIsAnd(pNode) );
+    Gia_NodeCollect_rec( p, Gia_ObjFanin0(pNode), vSupp );
+    Gia_NodeCollect_rec( p, Gia_ObjFanin1(pNode), vSupp );
+}
+int Gia_NodeMffcSizeSupp( Gia_Man_t * p, Gia_Obj_t * pNode, Vec_Int_t * vSupp )
+{
+    int ConeSize1, ConeSize2;
+    assert( !Gia_IsComplement(pNode) );
+    assert( Gia_ObjIsAnd(pNode) );
+    Vec_IntClear( vSupp );
+    Gia_ManIncrementTravId( p );
+    ConeSize1 = Gia_NodeDeref_rec( p, pNode );
+    Gia_NodeCollect_rec( p, Gia_ObjFanin0(pNode), vSupp );
+    Gia_NodeCollect_rec( p, Gia_ObjFanin1(pNode), vSupp );
+    ConeSize2 = Gia_NodeRef_rec( p, pNode );
+    assert( ConeSize1 == ConeSize2 );
+    assert( ConeSize1 >= 0 );
+    return ConeSize1;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Returns 1 if AIG has dangling nodes.]
 
   Description []
diff --git a/src/base/abci/abcCollapse.c b/src/base/abci/abcCollapse.c
index d1e6be2f..ac7bcdc5 100644
--- a/src/base/abci/abcCollapse.c
+++ b/src/base/abci/abcCollapse.c
@@ -583,6 +583,51 @@ Gia_Man_t * Abc_NtkClpGia( Abc_Ntk_t * pNtk )
 
 /**Function*************************************************************
 
+  Synopsis    [Minimize SOP by removing redundant variables.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+#define Abc_NtkSopForEachCube( pSop, nVars, pCube )  for ( pCube = (pSop); *pCube; pCube += (nVars) + 3 )
+
+int Abc_NtkCollapseCountVars( Vec_Str_t * vSop, Vec_Int_t * vSupp )
+{
+    int j = 0, k, iVar, nVars = Vec_IntSize(vSupp);
+    char * pCube, * pSop = Vec_StrArray(vSop);
+    Vec_Int_t * vPres = Vec_IntStart( nVars );
+    Abc_NtkSopForEachCube( pSop, nVars, pCube )
+        for ( k = 0; k < nVars; k++ )
+            if ( pCube[k] != '-' )
+                Vec_IntWriteEntry( vPres, k, 1 );
+    if ( Vec_IntCountZero(vPres) == 0 )
+    {
+        Vec_IntFree( vPres );
+        return 0;
+    }
+    // reduce cubes
+    Abc_NtkSopForEachCube( pSop, nVars, pCube )
+        for ( k = 0; k < nVars + 3; k++ )
+            if ( k >= nVars || Vec_IntEntry(vPres, k) )
+                Vec_StrWriteEntry( vSop, j++, pCube[k] );
+    Vec_StrWriteEntry( vSop, j++, '\0' );
+    Vec_StrShrink( vSop, j );
+    // reduce support
+    j = 0;
+    Vec_IntForEachEntry( vSupp, iVar, k )
+        if ( Vec_IntEntry(vPres, k) )
+            Vec_IntWriteEntry( vSupp, j++, iVar );
+    Vec_IntShrink( vSupp, j );
+    Vec_IntFree( vPres );
+    return 1;
+}
+
+
+/**Function*************************************************************
+
   Synopsis    [Computes SOPs for each output.]
 
   Description []
@@ -606,6 +651,10 @@ Vec_Str_t * Abc_NtkClpGiaOne( Gia_Man_t * p, int iCo, int nCubeLim, int nBTLimit
         return NULL;
     if ( Vec_StrSize(vSop) == 4 ) // constant
         Vec_IntClear(vSupp);
+    else
+        Abc_NtkCollapseCountVars( vSop, vSupp );
+    if ( fVerbose )
+        printf( "Supp new = %4d. Sop = %4d.  ", Vec_IntSize(vSupp), Vec_StrSize(vSop)/(Vec_IntSize(vSupp) +3) );
     if ( fVerbose )
         Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
     return vSop; 
@@ -613,27 +662,18 @@ Vec_Str_t * Abc_NtkClpGiaOne( Gia_Man_t * p, int iCo, int nCubeLim, int nBTLimit
 Vec_Ptr_t * Abc_GiaDeriveSops( Abc_Ntk_t * pNtkNew, Gia_Man_t * p, Vec_Wec_t * vSupps, int nCubeLim, int nBTLimit, int nCostMax, int fCanon, int fReverse, int fVerbose )
 {
     ProgressBar * pProgress;
+    abctime clk = Abc_Clock();
     Vec_Ptr_t * vSops = NULL, * vSopsRepr;
     Vec_Int_t * vReprs, * vClass, * vReprSuppSizes;
     int i, k, Entry, iCo, * pOrder;
     Vec_Wec_t * vClasses;
-    // check the largest output
-    if ( nCubeLim > 0 && nCostMax > 0 )
-    {
-        int iCoMax   = Gia_ManCoLargestSupp( p, vSupps );
-        int iObjMax  = Gia_ObjId( p, Gia_ManCo(p, iCoMax) );
-        int nSuppMax = Vec_IntSize( Vec_WecEntry(vSupps, iCoMax) );
-        int nNodeMax = Gia_ManConeSize( p, &iObjMax, 1 );
-        word Cost = (word)nNodeMax * (word)nSuppMax * (word)nCubeLim;
-        if ( Cost > (word)nCostMax )
-        {
-            printf( "Cost of the largest output cone exceeded the limit (%d * %d * %d  >  %d).\n", 
-                nNodeMax, nSuppMax, nCubeLim, nCostMax );
-            return NULL;
-        }
-    }
     // derive classes of outputs
     vClasses = Gia_ManIsoStrashReduceInt( p, vSupps, 0 );
+    if ( fVerbose )
+    {
+        printf( "Considering %d (out of %d) outputs. ", Vec_WecSize(vClasses), Gia_ManCoNum(p) );
+        Abc_PrintTime( 1, "Reduction time", Abc_Clock() - clk );
+    }
     // derive representatives
     vReprs = Vec_WecCollectFirsts( vClasses );
     vReprSuppSizes = Vec_IntAlloc( Vec_IntSize(vReprs) );
@@ -693,6 +733,23 @@ Abc_Ntk_t * Abc_NtkFromSopsInt( Abc_Ntk_t * pNtk, int nCubeLim, int nBTLimit, in
     int i, k, iCi; 
     pGia    = Abc_NtkClpGia( pNtk );
     vSupps  = Gia_ManCreateCoSupps( pGia, fVerbose );
+    // check the largest output
+    if ( nCubeLim > 0 && nCostMax > 0 )
+    {
+        int iCoMax   = Gia_ManCoLargestSupp( pGia, vSupps );
+        int iObjMax  = Gia_ObjId( pGia, Gia_ManCo(pGia, iCoMax) );
+        int nSuppMax = Vec_IntSize( Vec_WecEntry(vSupps, iCoMax) );
+        int nNodeMax = Gia_ManConeSize( pGia, &iObjMax, 1 );
+        word Cost = (word)nNodeMax * (word)nSuppMax * (word)nCubeLim;
+        if ( Cost > (word)nCostMax )
+        {
+            printf( "Cost of the largest output cone exceeded the limit (%d * %d * %d  >  %d).\n", 
+                nNodeMax, nSuppMax, nCubeLim, nCostMax );
+            Gia_ManStop( pGia );
+            Vec_WecFree( vSupps );
+            return NULL;
+        }
+    }
     pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC, ABC_FUNC_SOP );
     vSops   = Abc_GiaDeriveSops( pNtkNew, pGia, vSupps, nCubeLim, nBTLimit, nCostMax, fCanon, fReverse, fVerbose );
     Gia_ManStop( pGia );
diff --git a/src/proof/abs/absRpm.c b/src/proof/abs/absRpm.c
index ef5747c1..edcbe7ed 100644
--- a/src/proof/abs/absRpm.c
+++ b/src/proof/abs/absRpm.c
@@ -19,6 +19,7 @@
 ***********************************************************************/
  
 #include "abs.h"
+#include "misc/vec/vecWec.h"
 
 ABC_NAMESPACE_IMPL_START 
 
@@ -106,6 +107,86 @@ void Gia_ManComputeDoms( Gia_Man_t * p )
         Gia_ManAddDom( p, Gia_ObjFanin1(pObj), i );
     }
 }
+
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Wec_t * Gia_ManCreateSupps( Gia_Man_t * p, int fVerbose )
+{
+    abctime clk = Abc_Clock();
+    Gia_Obj_t * pObj; int i, Id;
+    Vec_Wec_t * vSupps = Vec_WecStart( Gia_ManObjNum(p) );
+    Gia_ManForEachCiId( p, Id, i )
+        Vec_IntPush( Vec_WecEntry(vSupps, Id), i );
+    Gia_ManForEachAnd( p, pObj, Id )
+        Vec_IntTwoMerge2( Vec_WecEntry(vSupps, Gia_ObjFaninId0(pObj, Id)), 
+                          Vec_WecEntry(vSupps, Gia_ObjFaninId1(pObj, Id)), 
+                          Vec_WecEntry(vSupps, Id) ); 
+//    Gia_ManForEachCo( p, pObj, i )
+//        Vec_IntAppend( Vec_WecEntry(vSupps, Gia_ObjId(p, pObj)), Vec_WecEntry(vSupps, Gia_ObjFaninId0p(p, pObj)) );
+    if ( fVerbose )
+        Abc_PrintTime( 1, "Support computation", Abc_Clock() - clk );
+    return vSupps;
+}
+void Gia_ManDomTest( Gia_Man_t * p )
+{
+    Vec_Int_t * vDoms = Vec_IntAlloc( 100 );
+    Vec_Int_t * vSupp = Vec_IntAlloc( 100 );
+    Vec_Wec_t * vSupps = Gia_ManCreateSupps( p, 1 );
+    Vec_Wec_t * vDomeds = Vec_WecStart( Gia_ManObjNum(p) );
+    Gia_Obj_t * pObj, * pDom; int i, Id, nMffcSize;
+    Gia_ManCreateRefs( p );
+    Gia_ManComputeDoms( p );
+    Gia_ManForEachCi( p, pObj, i )
+    {
+        if ( Gia_ObjDom(p, pObj) == -1 )
+            continue;
+        for ( pDom = Gia_ManObj(p, Gia_ObjDom(p, pObj)); Gia_ObjIsAnd(pDom); pDom = Gia_ManObj(p, Gia_ObjDom(p, pDom)) )
+            Vec_IntPush( Vec_WecEntry(vDomeds, Gia_ObjId(p, pDom)), i );
+    }
+    Gia_ManForEachAnd( p, pObj, i )
+        if ( Vec_IntEqual(Vec_WecEntry(vSupps, i), Vec_WecEntry(vDomeds, i)) )
+            Vec_IntPush( vDoms, i );
+    Vec_WecFree( vSupps );
+    Vec_WecFree( vDomeds );
+
+    // check MFFC sizes
+    Vec_IntForEachEntry( vDoms, Id, i )
+        Gia_ObjRefInc( p, Gia_ManObj(p, Id) );
+    Vec_IntForEachEntry( vDoms, Id, i )
+    {
+        nMffcSize = Gia_NodeMffcSizeSupp( p, Gia_ManObj(p, Id), vSupp );
+        printf( "%d(%d:%d) ", Id, Vec_IntSize(vSupp), nMffcSize );
+    }
+    printf( "\n" );
+    Vec_IntForEachEntry( vDoms, Id, i )
+        Gia_ObjRefDec( p, Gia_ManObj(p, Id) );
+
+//    Vec_IntPrint( vDoms );
+    Vec_IntFree( vDoms );
+    Vec_IntFree( vSupp );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 void Gia_ManTestDoms2( Gia_Man_t * p )
 {
     Vec_Int_t * vNodes;
diff --git a/src/sat/bmc/bmcClp.c b/src/sat/bmc/bmcClp.c
index 81f81063..826c0a32 100644
--- a/src/sat/bmc/bmcClp.c
+++ b/src/sat/bmc/bmcClp.c
@@ -36,14 +36,158 @@ extern Cnf_Dat_t * Mf_ManGenerateCnf( Gia_Man_t * pGia, int nLutSize, int fCnfOb
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
+/**Function*************************************************************
+
+  Synopsis    [For a given random pattern, compute output change.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Bmc_ComputeSimDiff( Gia_Man_t * p, Vec_Int_t * vPat, Vec_Int_t * vPat2 )
+{
+    Gia_Obj_t * pObj;
+    int i, Id; word Sim, Sim0, Sim1;
+    Gia_ManForEachCiId( p, Id, i )
+    {
+        Sim = Vec_IntEntry(vPat, i) ? ~(word)0 : 0;
+        Sim ^= (word)1 << (i + 1);
+        Vec_WrdWriteEntry( p->vSims, Id, Sim );
+    }
+    Gia_ManForEachAnd( p, pObj, i )
+    {
+        Sim0 = Vec_WrdEntry( p->vSims, Gia_ObjFaninId0(pObj, i) );
+        Sim1 = Vec_WrdEntry( p->vSims, Gia_ObjFaninId1(pObj, i) );
+        Sim0 = Gia_ObjFaninC0(pObj) ? ~Sim0 : Sim0;
+        Sim1 = Gia_ObjFaninC1(pObj) ? ~Sim1 : Sim1;
+        Vec_WrdWriteEntry( p->vSims, i, Sim0 & Sim1 );
+    }
+    Gia_ManForEachCo( p, pObj, i )
+    {
+        Id = Gia_ObjId( p, pObj );
+        Sim0 = Vec_WrdEntry( p->vSims, Gia_ObjFaninId0(pObj, Id) );
+        Sim0 = Gia_ObjFaninC0(pObj) ? ~Sim0 : Sim0;
+        Vec_WrdWriteEntry( p->vSims, Id, Sim0 );
+    }
+    pObj = Gia_ManCo( p, 0 );
+    Sim = Vec_WrdEntry( p->vSims, Gia_ObjId(p, pObj) );
+    Vec_IntClear( vPat2 );
+    for ( i = 1; i <= Gia_ManCiNum(p); i++ )
+        Vec_IntPush( vPat2, (int)((Sim & 1) ^ ((Sim >> i) & 1)) );
+    return (int)(Sim & 1);
+}
+void Bmc_ComputeSimTest( Gia_Man_t * p )
+{
+    int i, v, w, Res, Bit, Bit2, nPats = 256;
+    int Count[2][64][64] = {{{0}}};
+    int PatCount[64][2][2] = {{{0}}};
+    int DiffCount[64] = {0};
+    Vec_Int_t * vPat = Vec_IntAlloc( Gia_ManCiNum(p) );
+    Vec_Int_t * vPat2 = Vec_IntAlloc( Gia_ManCiNum(p) );
+    Vec_WrdFreeP( &p->vSims );
+    p->vSims = Vec_WrdStart( Gia_ManObjNum(p) );
+    printf( "Number of patterns = %d.\n", nPats );
+    for ( i = 0; i < nPats; i++ )
+    {
+        Vec_IntClear( vPat );
+        for ( v = 0; v < Gia_ManCiNum(p); v++ )
+            Vec_IntPush( vPat, rand() & 1 );
+
+//        Vec_IntForEachEntry( vPat, Bit, v )
+//            printf( "%d", Bit );
+//        printf( "    " );
+
+        Res = Bmc_ComputeSimDiff( p, vPat, vPat2 );
+//        printf( "%d ", Res );
+
+//        Vec_IntForEachEntry( vPat2, Bit, v )
+//            printf( "%d", Bit );
+//        printf( "\n" );
+
+        Vec_IntForEachEntry( vPat, Bit, v )
+            PatCount[v][Res][Bit]++;
+
+        Vec_IntForEachEntry( vPat2, Bit, v )
+        {
+            if ( Bit )
+                DiffCount[v]++;
+            Vec_IntForEachEntryStart( vPat2, Bit2, w, v + 1 )
+                if ( Bit && Bit2 )
+                    Count[Res][v][w]++;
+        }
+    }
+    Vec_IntFree( vPat );
+    Vec_IntFree( vPat2 );
+    Vec_WrdFreeP( &p->vSims );
+
+
+    printf( "\n" );
+    printf( "      " );
+    for ( v = 0; v < Gia_ManCiNum(p); v++ )
+        printf( "%3c ", 'a'+v );
+    printf( "\n" );
+
+    printf( "Off0  " );
+    for ( v = 0; v < Gia_ManCiNum(p); v++ )
+        printf( "%3d ", PatCount[v][0][0] );
+    printf( "\n" );
+
+    printf( "Off1  " );
+    for ( v = 0; v < Gia_ManCiNum(p); v++ )
+        printf( "%3d ", PatCount[v][0][1] );
+    printf( "\n" );
+
+    printf( "On0   " );
+    for ( v = 0; v < Gia_ManCiNum(p); v++ )
+        printf( "%3d ", PatCount[v][1][0] );
+    printf( "\n" );
+
+    printf( "On1   " );
+    for ( v = 0; v < Gia_ManCiNum(p); v++ )
+        printf( "%3d ", PatCount[v][1][1] );
+    printf( "\n" );
+    printf( "\n" );
+
+    printf( "Diff  " );
+    for ( v = 0; v < Gia_ManCiNum(p); v++ )
+        printf( "%3d ", DiffCount[v] );
+    printf( "\n" );
+    printf( "\n" );
+
+    for ( i = 0; i < 2; i++ )
+    {
+        printf( "      " );
+        for ( v = 0; v < Gia_ManCiNum(p); v++ )
+            printf( "%3c ", 'a'+v );
+        printf( "\n" );
+
+        for ( v = 0; v < Gia_ManCiNum(p); v++ )
+        {
+            printf( " %c    ", 'a'+v );
+            for ( w = 0; w < Gia_ManCiNum(p); w++ )
+            {
+                if ( Count[i][v][w] )
+                    printf( "%3d ", Count[i][v][w] );
+                else
+                    printf( "  . " );
+            }
+            printf( "\n" );
+        }
+        printf( "\n" );
+    }
+}
+
+
 static abctime clkCheck1 = 0;
 static abctime clkCheck2 = 0;
 static abctime clkCheckS = 0;
 static abctime clkCheckU = 0;
 
-// enumerate cubes and literals
-#define Bmc_SopForEachCube( pSop, nVars, pCube )                        \
-    for ( pCube = (pSop); *pCube; pCube += (nVars) + 3 )
+// iterator thought the cubes
+#define Bmc_SopForEachCube( pSop, nVars, pCube )  for ( pCube = (pSop); *pCube; pCube += (nVars) + 3 )
 
 /**Function*************************************************************
 
@@ -270,11 +414,6 @@ int Bmc_CollapseExpandRound( sat_solver * pSat, sat_solver * pSatOn, Vec_Int_t *
     }
 //    if ( pSatOn )
 //    printf( "\n" );
-    // put into new array
-    Vec_IntClear( vNums );
-    Vec_IntForEachEntry( vLits, iLit, n )
-        if ( iLit != -1 )
-            Vec_IntPush( vNums, n );
     return 0;
 }
 
@@ -311,9 +450,21 @@ int Bmc_CollapseExpand( sat_solver * pSat, sat_solver * pSatOn, Vec_Int_t * vLit
             if ( k == nFinal )
                 Vec_IntWriteEntry( vLits, i, -1 );
         }
+        Bmc_CollapseExpandRound( pSat, NULL,   vLits, vNums, vTemp, nBTLimit, fCanon );
+    }
+    else
+    {
+        Bmc_CollapseExpandRound( pSat, pSatOn, vLits, vNums, vTemp, nBTLimit, fCanon );
+        Bmc_CollapseExpandRound( pSat, NULL,   vLits, vNums, vTemp, nBTLimit, fCanon );
+    }
+    {
+        // put into new array
+        int i, iLit;
+        Vec_IntClear( vNums );
+        Vec_IntForEachEntry( vLits, iLit, i )
+            if ( iLit != -1 )
+                Vec_IntPush( vNums, i );
     }
-    Bmc_CollapseExpandRound( pSat, pSatOn, vLits, vNums, vTemp, nBTLimit, fCanon );
-    Bmc_CollapseExpandRound( pSat, NULL,   vLits, vNums, vTemp, nBTLimit, fCanon );
     return 0;
 }