Preprocessing SOPs given to 'fx' to be D1C-free and SCC-free. Handling the case of non-prime SOPs.

4 files changed, 139 insertions, 79 deletions

diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h
index e408a58f..a2b2fdf5 100644
--- a/src/base/abc/abc.h
+++ b/src/base/abc/abc.h
@@ -503,11 +503,13 @@ static inline void        Abc_ObjSetMvVar( Abc_Obj_t * pObj, void * pV) { Vec_At
 #define Abc_ObjForEachFanout( pObj, pFanout, i )                                                   \
     for ( i = 0; (i < Abc_ObjFanoutNum(pObj)) && (((pFanout) = Abc_ObjFanout(pObj, i)), 1); i++ )
 // cubes and literals
-#define Abc_SopForEachCube( pSop, nFanins, pCube )                                                 \
-    for ( pCube = (pSop); *pCube; pCube += (nFanins) + 3 )
 #define Abc_CubeForEachVar( pCube, Value, i )                                                      \
     for ( i = 0; (pCube[i] != ' ') && (Value = pCube[i]); i++ )           
-
+#define Abc_SopForEachCube( pSop, nFanins, pCube )                                                 \
+    for ( pCube = (pSop); *pCube; pCube += (nFanins) + 3 )
+#define Abc_SopForEachCubePair( pSop, nFanins, pCube, pCube2 )                                     \
+    Abc_SopForEachCube( pSop, nFanins, pCube )                                                     \
+    Abc_SopForEachCube( pCube + (nFanins) + 3, nFanins, pCube2 )
 
 ////////////////////////////////////////////////////////////////////////
 ///                    FUNCTION DECLARATIONS                         ///
diff --git a/src/base/abc/abcFanOrder.c b/src/base/abc/abcFanOrder.c
index dd1cfc79..bdeb6d87 100644
--- a/src/base/abc/abcFanOrder.c
+++ b/src/base/abc/abcFanOrder.c
@@ -233,77 +233,6 @@ void Abc_NtkOrderFaninsByLitCountAndCubeCount( Abc_Ntk_t * pNtk )
 
 /**Function*************************************************************
 
-  Synopsis    [Checks if the network is SCC-free.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline int Abc_CubeContain( char * pCube1, char * pCube2, int nVars )
-{
-    int v, fCont12 = 1, fCont21 = 1;
-    for ( v = 0; v < nVars; v++ )
-    {
-        if ( pCube1[v] == pCube2[v] )
-            continue;
-        if ( pCube1[v] == '-' )
-            fCont21 = 0;
-        else if ( pCube2[v] == '-' )
-            fCont12 = 0;
-        else
-            return 0;
-        if ( !fCont21 && !fCont21 )
-            return 0;
-    }
-    assert( fCont21 || fCont12 );
-    return (fCont21 << 1) | fCont12;
-}
-int Abc_NodeMakeSCCFree( Abc_Obj_t * pNode, Vec_Ptr_t * vCubes )
-{
-    char * pSop = (char *)pNode->pData;
-    char * pCube, * pCube2;
-    int i, k, Status, nCount = 0;
-    int nVars = Abc_ObjFaninNum(pNode);
-    Vec_PtrClear( vCubes );
-    Abc_SopForEachCube( pSop, nVars, pCube )
-        Vec_PtrPush( vCubes, pCube );
-    Vec_PtrForEachEntry( char *, vCubes, pCube, i )
-    if ( pCube != NULL )
-        Vec_PtrForEachEntryStart( char *, vCubes, pCube2, k, i+1 )
-        if ( pCube2 != NULL )
-        {
-            Status = Abc_CubeContain( pCube, pCube2, nVars );
-            nCount += (int)(Status > 0);
-            if ( Status & 1 )
-                Vec_PtrWriteEntry( vCubes, k, NULL );
-            else if ( Status & 2 )
-                Vec_PtrWriteEntry( vCubes, i, NULL );
-        }
-    if ( nCount == 0 )
-        return 0;
-    return 1;
-}
-void Abc_NtkMakeSCCFree( Abc_Ntk_t * pNtk )
-{
-    Vec_Ptr_t * vCubes;
-    Abc_Obj_t * pNode;
-    int i;
-    assert( Abc_NtkHasSop(pNtk) );
-    vCubes = Vec_PtrAlloc( 1000 );
-    Abc_NtkForEachNode( pNtk, pNode, i )
-        if ( Abc_NodeMakeSCCFree( pNode, vCubes ) )
-        {
-            printf( "Node %d is not SCC-free.\n", i );
-            break;
-        }
-    Vec_PtrFree( vCubes );
-}
-
-/**Function*************************************************************
-
   Synopsis    [Split large nodes by dividing their SOPs in half.]
 
   Description []
@@ -424,6 +353,123 @@ void Abc_NtkSortSops( Abc_Ntk_t * pNtk )
     Abc_NtkSortCubes( pNtk );
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Makes cover legitimate for "fast_extract".]
+
+  Description [Iteratively removes distance-1 and contained cubes.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Abc_CubeContain( char * pCube1, char * pCube2, int nVars )
+{
+    int v, fCont12 = 1, fCont21 = 1;
+    for ( v = 0; v < nVars; v++ )
+    {
+        if ( pCube1[v] == pCube2[v] )
+            continue;
+        if ( pCube1[v] == '-' )
+            fCont21 = 0;
+        else if ( pCube2[v] == '-' )
+            fCont12 = 0;
+        else
+            return 0;
+        if ( !fCont21 && !fCont21 )
+            return 0;
+    }
+    assert( fCont21 || fCont12 );
+    return (fCont21 << 1) | fCont12;
+}
+int Abc_NodeMakeSCCFree( Abc_Obj_t * pNode )
+{
+    char * pSop = (char *)pNode->pData;
+    char * pCube, * pCube2, * pSopNew;
+    int nVars = Abc_ObjFaninNum(pNode);
+    int Status, nCount = 0;
+    Abc_SopForEachCubePair( pSop, nVars, pCube, pCube2 )
+    {
+        if ( pCube[0] == 'z' || pCube2[0] == 'z' )
+            continue;
+        Status = Abc_CubeContain( pCube, pCube2, nVars );
+        nCount += (int)(Status > 0);
+        if ( Status & 1 )
+            pCube2[0] = 'z';
+        else if ( Status & 2 )
+            pCube[0] = 'z';
+    }
+    if ( nCount == 0 )
+        return 0;
+    // create new cover
+    pSopNew = (char *)pNode->pData;
+    Abc_SopForEachCube( pSop, nVars, pCube )
+    {
+        if ( pCube[0] == 'z' )
+            continue;
+        memcpy( pSopNew, pCube, nVars + 3 );
+        pSopNew += nVars + 3;
+    }
+    *pSopNew = 0;
+    return 1;
+}
+void Abc_NodeMakeDist1Free( Abc_Obj_t * pNode )
+{
+    char * pSop = (char *)pNode->pData;
+    char * pCube, * pCube2;
+    int i, nVars = Abc_ObjFaninNum(pNode);
+    Abc_SopForEachCube( pSop, nVars, pCube )
+    Abc_SopForEachCube( pCube + nVars + 3, nVars, pCube2 )
+    {
+        int Counter = 0, iDiff = -1;
+        for ( i = 0; i < nVars; i++ )
+            if ( pCube[i] != pCube2[i] )
+                Counter++, iDiff = i;
+        if ( Counter == 1 && ((pCube[iDiff] == '0' && pCube2[iDiff] == '1') || (pCube[iDiff] == '1' && pCube2[iDiff] == '0')) )
+            pCube[iDiff] = pCube2[iDiff] = '-';
+    }
+}
+void Abc_NodeCheckDist1Free( Abc_Obj_t * pNode )
+{
+    char * pSop = (char *)pNode->pData;
+    char * pCube, * pCube2;
+    int i, nVars = Abc_ObjFaninNum(pNode);
+    Abc_SopForEachCube( pSop, nVars, pCube )
+    Abc_SopForEachCube( pSop, nVars, pCube2 )
+    {
+        int Counter = 0;
+        if ( pCube == pCube2 )
+            continue;
+        for ( i = 0; i < nVars; i++ )
+            if ( pCube[i] != pCube2[i] )
+                Counter++;
+        assert( Counter > 1 );
+    }
+}
+int Abc_NodeMakeLegit( Abc_Obj_t * pNode )
+{
+    int i, fChanges = 1;
+    for ( i = 0; fChanges; i++ )
+    {
+        Abc_NodeMakeDist1Free( pNode );
+        fChanges = Abc_NodeMakeSCCFree( pNode );
+    }
+//    Abc_NodeCheckDist1Free( pNode );
+    return i > 1;
+}
+int Abc_NtkMakeLegit( Abc_Ntk_t * pNtk )
+{
+    Abc_Obj_t * pNode;
+    int i, Counter = 0;
+    assert( Abc_NtkHasSop(pNtk) );
+    Abc_NtkForEachNode( pNtk, pNode, i )
+        Counter += Abc_NodeMakeLegit( pNode );
+    if ( Counter )
+        Abc_Print( 1, "%d nodes were made dist1-cube-free and/or single-cube-containment-free.\n", Counter );
+    return 1;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 6de6a637..bd18200c 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -9625,8 +9625,8 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
 */
     if ( pNtk )
     { 
-        extern void Abc_NtkTestTim( Abc_Ntk_t * pNtk, int fVerbose );
-        Abc_NtkTestTim( pNtk, fVerbose ); 
+        extern void Abc_NtkMakeLegit( Abc_Ntk_t * pNtk );
+        Abc_NtkMakeLegit( pNtk ); 
     }
     return 0;
 usage:
diff --git a/src/base/abci/abcFx.c b/src/base/abci/abcFx.c
index c515afb1..953f87f3 100644
--- a/src/base/abci/abcFx.c
+++ b/src/base/abci/abcFx.c
@@ -134,12 +134,14 @@ static inline int Fx_ManGetFirstVarCube( Fx_Man_t * p, Vec_Int_t * vCube ) { ret
 ***********************************************************************/
 Vec_Wec_t * Abc_NtkFxRetrieve( Abc_Ntk_t * pNtk )
 {
+    extern int Abc_NtkMakeLegit( Abc_Ntk_t * pNtk );
     Vec_Wec_t * vCubes;
     Vec_Int_t * vCube;
     Abc_Obj_t * pNode;
     char * pCube, * pSop;
     int nVars, i, v, Lit;
     assert( Abc_NtkIsSopLogic(pNtk) );
+    Abc_NtkMakeLegit( pNtk );
     vCubes = Vec_WecAlloc( 1000 );
     Abc_NtkForEachNode( pNtk, pNode, i )
     {
@@ -597,7 +599,7 @@ int Fx_ManDivFindCubeFree( Vec_Int_t * vArr1, Vec_Int_t * vArr2, Vec_Int_t * vCu
             pBeg1++, pBeg2++, Counter++;
         else if ( *pBeg1 < *pBeg2 )
             Vec_IntPush( vCubeFree, Abc_Var2Lit(*pBeg1++, fAttr0) );
-        else 
+        else  
         {
             if ( Vec_IntSize(vCubeFree) == 0 )
                 fAttr0 = 1, fAttr1 = 0;
@@ -608,7 +610,12 @@ int Fx_ManDivFindCubeFree( Vec_Int_t * vArr1, Vec_Int_t * vArr2, Vec_Int_t * vCu
         Vec_IntPush( vCubeFree, Abc_Var2Lit(*pBeg1++, fAttr0) );
     while ( pBeg2 < pEnd2 )
         Vec_IntPush( vCubeFree, Abc_Var2Lit(*pBeg2++, fAttr1) );
-    assert( Vec_IntSize(vCubeFree) > 1 ); // the cover is not SCC-free
+    if ( Vec_IntSize(vCubeFree) == 0 )
+        printf( "The SOP has duplicated cubes.\n" );
+    else if ( Vec_IntSize(vCubeFree) == 1 )
+        printf( "The SOP has contained cubes.\n" );
+    else if ( Vec_IntSize(vCubeFree) == 2 && Abc_Lit2Var(Abc_Lit2Var(Vec_IntEntry(vCubeFree, 0))) == Abc_Lit2Var(Abc_Lit2Var(Vec_IntEntry(vCubeFree, 1))) )
+        printf( "The SOP has distance-1 cubes or it is not a prime cover.  Please make sure the result verifies.\n" );
     assert( !Abc_LitIsCompl(Vec_IntEntry(vCubeFree, 0)) );
     return Counter;
 }
@@ -807,7 +814,7 @@ void Fx_ManCubeDoubleCubeDivisors( Fx_Man_t * p, int iFirst, Vec_Int_t * vPivot,
             else if ( !fRemove )
                 Vec_QuePush( p->vPrio, iDiv );
         }
-    }
+    } 
 }
 void Fx_ManCreateDivisors( Fx_Man_t * p )
 {
@@ -936,6 +943,11 @@ void Fx_ManUpdate( Fx_Man_t * p, int iDiv )
     Fx_ManDivFindPivots( vDiv, &Lit0, &Lit1 );
     assert( Lit0 >= 0 && Lit1 >= 0 );
 
+    // if the input cover is not prime, it may happen that we are extracting divisor (x + !x)
+    // although it is not strictly correct, it seems to be fine to just skip such divisors
+    if ( Abc_Lit2Var(Lit0) == Abc_Lit2Var(Lit1) )
+        return;
+
     // collect single-cube-divisor cubes
     Vec_IntClear( p->vCubesS );
     if ( Vec_IntSize(vDiv) == 2 )