Changes to enable decomposition of non-DSD functions.

6 files changed, 179 insertions, 9 deletions

diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index 70fda8d4..5a6148d0 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -1227,6 +1227,7 @@ extern void                Gia_ObjPrint( Gia_Man_t * p, Gia_Obj_t * pObj );
 extern void                Gia_ManPrint( Gia_Man_t * p );
 extern void                Gia_ManPrintCo( Gia_Man_t * p, Gia_Obj_t * pObj );
 extern void                Gia_ManPrintCone( Gia_Man_t * p, Gia_Obj_t * pObj, int * pLeaves, int nLeaves, Vec_Int_t * vNodes );
+extern void                Gia_ManPrintCone2( Gia_Man_t * p, Gia_Obj_t * pObj );
 extern void                Gia_ManInvertConstraints( Gia_Man_t * pAig );
 extern void                Gia_ManInvertPos( Gia_Man_t * pAig );
 extern int                 Gia_ManCompare( Gia_Man_t * p1, Gia_Man_t * p2 );
diff --git a/src/aig/gia/giaUtil.c b/src/aig/gia/giaUtil.c
index cad6f5ad..cf1aa762 100644
--- a/src/aig/gia/giaUtil.c
+++ b/src/aig/gia/giaUtil.c
@@ -1194,6 +1194,7 @@ void Gia_ManPrintCo( Gia_Man_t * p, Gia_Obj_t * pObj )
     Gia_ManPrintCo_rec( p, Gia_ObjFanin0(pObj) );
     Gia_ObjPrint( p, pObj );
 }
+
 void Gia_ManPrintCollect_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vNodes )
 {
     if ( Vec_IntFind(vNodes, Gia_ObjId(p, pObj)) >= 0 )
@@ -1215,6 +1216,28 @@ void Gia_ManPrintCone( Gia_Man_t * p, Gia_Obj_t * pObj, int * pLeaves, int nLeav
         Gia_ObjPrint( p, pObj );
 }
 
+void Gia_ManPrintCollect2_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vNodes )
+{
+    if ( Vec_IntFind(vNodes, Gia_ObjId(p, pObj)) >= 0 )
+        return;
+    if ( Gia_ObjIsCo(pObj) || Gia_ObjIsAnd(pObj) )
+        Gia_ManPrintCollect2_rec( p, Gia_ObjFanin0(pObj), vNodes );
+    if ( Gia_ObjIsAnd(pObj) )
+        Gia_ManPrintCollect2_rec( p, Gia_ObjFanin1(pObj), vNodes );
+    Vec_IntPush( vNodes, Gia_ObjId(p, pObj) );
+}
+void Gia_ManPrintCone2( Gia_Man_t * p, Gia_Obj_t * pObj )
+{
+    Vec_Int_t * vNodes;
+    int i;
+    vNodes = Vec_IntAlloc( 100 );
+    Gia_ManPrintCollect2_rec( p, pObj, vNodes );
+    printf( "GIA logic cone for node %d:\n", Gia_ObjId(p, pObj) );
+    Gia_ManForEachObjVec( vNodes, p, pObj, i )
+        Gia_ObjPrint( p, pObj );
+    Vec_IntFree( vNodes );
+}
+
 /**Function*************************************************************
 
   Synopsis    [Complements the constraint outputs.]
diff --git a/src/base/abci/abcRec3.c b/src/base/abci/abcRec3.c
index cf90a79d..8bf46feb 100644
--- a/src/base/abci/abcRec3.c
+++ b/src/base/abci/abcRec3.c
@@ -1035,7 +1035,15 @@ Hop_Obj_t * Abc_RecToHop3( Hop_Man_t * pMan, If_Man_t * pIfMan, If_Cut_t * pCut,
     If_CutFindBestStruct( pIfMan, pCut, pCanonPerm, &uCanonPhase, &BestPo );
     assert( BestPo >= 0 );
     pGiaPo = Gia_ManCo( pGia, BestPo );
-
+/*
+if ( If_CutLeaveNum(pCut) == 6 )
+{
+printf( "\n" );
+Kit_DsdPrintFromTruth( If_CutTruth(pCut), If_CutLeaveNum(pCut) ); printf( "\n" );
+//Gia_ManPrintCo( pGia, pGiaPo );
+Gia_ManPrintCone2( pGia, pGiaPo );
+}
+*/
     // collect internal nodes into pGia->vTtNodes
     if ( pGia->vTtNodes == NULL )
         pGia->vTtNodes = Vec_IntAlloc( 256 );
diff --git a/src/bool/rsb/rsbDec6.c b/src/bool/rsb/rsbDec6.c
index df30eb1a..88644686 100644
--- a/src/bool/rsb/rsbDec6.c
+++ b/src/bool/rsb/rsbDec6.c
@@ -334,7 +334,7 @@ int Rsb_DecInitCexes( int nVars, word * f, word ** g, int nGs, int nGsAll, word
   SeeAlso     []
 
 ***********************************************************************/
-unsigned Rsb_DecPerformInt( Rsb_Man_t * p, int nVars, word * f, word ** g, int nGs, int nGsAll ) 
+unsigned Rsb_DecPerformInt( Rsb_Man_t * p, int nVars, word * f, word ** g, int nGs, int nGsAll, int fFindAll ) 
 {
     word * pCexes = Vec_WrdArray(p->vCexes);
     unsigned * pPat = (unsigned *)Vec_IntArray(p->vDecPats);
@@ -365,7 +365,17 @@ unsigned Rsb_DecPerformInt( Rsb_Man_t * p, int nVars, word * f, word ** g, int n
         pDivs[0] = g[i];  p->vFanins->pArray[0] = i;
         uTruth = Rsb_DecCheck( nVars, f, pDivs, Vec_IntSize(p->vFanins), pPat, &iCexA, &iCexB );
         if ( uTruth )
-            return uTruth;
+        {
+            if ( fFindAll )
+            {
+                uTruth = (unsigned)Abc_Tt6Stretch( (word)uTruth, 1 );
+                Kit_DsdPrintFromTruth( &uTruth, 1 ); printf( "   " );
+                Vec_IntPrint(p->vFanins);
+                continue;
+            }
+            else
+                return uTruth;
+        }
         if ( nCexes == 64 )
             return 0;
         Rsb_DecVerifyCex( f, pDivs, Vec_IntSize(p->vFanins), iCexA, iCexB );
@@ -388,7 +398,17 @@ unsigned Rsb_DecPerformInt( Rsb_Man_t * p, int nVars, word * f, word ** g, int n
         pDivs[1] = g[k];  p->vFanins->pArray[1] = k;
         uTruth = Rsb_DecCheck( nVars, f, pDivs, Vec_IntSize(p->vFanins), pPat, &iCexA, &iCexB );
         if ( uTruth )
-            return uTruth;
+        {
+            if ( fFindAll )
+            {
+                uTruth = (unsigned)Abc_Tt6Stretch( (word)uTruth, 2 );
+                Kit_DsdPrintFromTruth( &uTruth, 2 ); printf( "   " );
+                Vec_IntPrint(p->vFanins);
+                continue;
+            }
+            else
+                return uTruth;
+        }
         if ( nCexes == 64 )
             return 0;
         Rsb_DecVerifyCex( f, pDivs, Vec_IntSize(p->vFanins), iCexA, iCexB );
@@ -414,7 +434,17 @@ unsigned Rsb_DecPerformInt( Rsb_Man_t * p, int nVars, word * f, word ** g, int n
         pDivs[2] = g[j];  p->vFanins->pArray[2] = j;
         uTruth = Rsb_DecCheck( nVars, f, pDivs, Vec_IntSize(p->vFanins), pPat, &iCexA, &iCexB );
         if ( uTruth )
-            return uTruth;
+        {
+            if ( fFindAll )
+            {
+                uTruth = (unsigned)Abc_Tt6Stretch( (word)uTruth, 3 );
+                Kit_DsdPrintFromTruth( &uTruth, 3 ); printf( "   " );
+                Vec_IntPrint(p->vFanins);
+                continue;
+            }
+            else
+                return uTruth;
+        }
         if ( nCexes == 64 )
             return 0;
         Rsb_DecVerifyCex( f, pDivs, Vec_IntSize(p->vFanins), iCexA, iCexB );
@@ -443,7 +473,17 @@ unsigned Rsb_DecPerformInt( Rsb_Man_t * p, int nVars, word * f, word ** g, int n
         pDivs[3] = g[n];  p->vFanins->pArray[3] = n;
         uTruth = Rsb_DecCheck( nVars, f, pDivs, Vec_IntSize(p->vFanins), pPat, &iCexA, &iCexB );
         if ( uTruth )
-            return uTruth;
+        {
+            if ( fFindAll )
+            {
+                uTruth = (unsigned)Abc_Tt6Stretch( (word)uTruth, 4 );
+                Kit_DsdPrintFromTruth( &uTruth, 4 ); printf( "   " );
+                Vec_IntPrint(p->vFanins);
+                continue;
+            }
+            else
+                return uTruth;
+        }
         if ( nCexes == 64 )
             return 0;
         Rsb_DecVerifyCex( f, pDivs, Vec_IntSize(p->vFanins), iCexA, iCexB );
@@ -611,7 +651,7 @@ unsigned Rsb_ManPerform( Rsb_Man_t * p, int nVars, word * f, word ** g, int nGs,
 if ( fVerbose )
 vTries = Vec_IntAlloc( 100 );
     assert( nGs < nGsAll );
-    uTruth = Rsb_DecPerformInt( p, nVars, f, g, nGs, nGsAll );
+    uTruth = Rsb_DecPerformInt( p, nVars, f, g, nGs, nGsAll, 0 );
 
     if ( uTruth )
     {
@@ -653,12 +693,13 @@ Vec_IntFree( vTries );
 ***********************************************************************/
 int Rsb_ManPerformResub6( Rsb_Man_t * p, int nVarsAll, word uTruth, Vec_Wrd_t * vDivTruths, word * puTruth0, word * puTruth1, int fVerbose )
 {
-    word * pGs[64];
+    word * pGs[200];
     unsigned uTruthRes;
     int i, nVars, nGs = Vec_WrdSize(vDivTruths);
+    assert( nGs < 200 );
     for ( i = 0; i < nGs; i++ )
         pGs[i] = Vec_WrdEntryP(vDivTruths,i);
-    uTruthRes = Rsb_DecPerformInt( p, nVarsAll, &uTruth, pGs, nGs, nGs );
+    uTruthRes = Rsb_DecPerformInt( p, nVarsAll, &uTruth, pGs, nGs, nGs, 0 );
     if ( uTruthRes == 0 )
         return 0;
 
diff --git a/src/misc/extra/extraUtilDsd.c b/src/misc/extra/extraUtilDsd.c
index 657808fd..cf1d3ade 100644
--- a/src/misc/extra/extraUtilDsd.c
+++ b/src/misc/extra/extraUtilDsd.c
@@ -27,6 +27,7 @@
 #include "misc/vec/vec.h"
 #include "misc/vec/vecHsh.h"
 #include "misc/util/utilTruth.h"
+#include "bool/rsb/rsb.h"
 
 ABC_NAMESPACE_IMPL_START
 
@@ -1151,6 +1152,84 @@ void Sdm_ManCompareCnfSizes()
 }
 */
 
+
+/**Function*************************************************************
+
+  Synopsis    [Collect DSD divisors of the function.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Sdm_ManDivCollect_rec( word t, Vec_Wrd_t ** pvDivs )
+{
+    int i, Config, Counter = 0;
+    // check if function is decomposable
+    Config = Sdm_ManCheckDsd6( s_SdmMan, t );
+    if ( Config != -1 && (Config >> 17) < 2 )
+        return;
+    for ( i = 0; i < 6; i++ )
+    {
+        if ( !Abc_Tt6HasVar( t, i ) )
+            continue;
+        Sdm_ManDivCollect_rec( Abc_Tt6Cofactor0(t, i), pvDivs );
+        Sdm_ManDivCollect_rec( Abc_Tt6Cofactor1(t, i), pvDivs );
+        Counter++;
+    }
+    if ( Config != -1 && Counter >= 2 && Counter <= 4 )
+    {
+        Vec_WrdPush( pvDivs[Counter], (t & 1) ? ~t : t );
+//        Kit_DsdPrintFromTruth( (unsigned *)&t, 6 ); printf( "\n" );
+    }
+}
+void Sdm_ManDivTest()
+{
+//    word u, t0, t1, t = ABC_CONST(0xB0F0BBFFB0F0BAFE);
+//    word u, t0, t1, t = ABC_CONST(0x3F1F3F13FFDFFFD3);
+    word u, t0, t1, t = ABC_CONST(0x3F3FFFFF37003700);
+    Rsb_Man_t * pManRsb = Rsb_ManAlloc( 6, 200, 3, 1 );
+    Vec_Wrd_t * pvDivs[7] = { NULL };
+    Vec_Wrd_t * vDivs = Vec_WrdAlloc( 100 );
+    int i, RetValue;
+
+    // collect divisors
+    for ( i = 2; i <= 4; i++ )
+        pvDivs[i] = Vec_WrdAlloc( 100 );
+    Sdm_ManDivCollect_rec( t, pvDivs );
+    for ( i = 2; i <= 4; i++ )
+        Vec_WrdUniqify( pvDivs[i] );
+
+    // prepare the set
+    vDivs = Vec_WrdAlloc( 100 );
+    for ( i = 0; i < 6; i++ )
+        Vec_WrdPush( vDivs, s_Truths6[i] );
+    for ( i = 2; i <= 4; i++ )
+        Vec_WrdAppend( vDivs, pvDivs[i] );
+    for ( i = 2; i <= 4; i++ )
+        Vec_WrdFree( pvDivs[i] );
+
+    Vec_WrdForEachEntry( vDivs, u, i )
+    {
+        printf( "%2d : ", i );
+        Kit_DsdPrintFromTruth( (unsigned *)&u, 6 ); printf( "\n" );
+    }
+
+    RetValue = Rsb_ManPerformResub6( pManRsb, 6, t, vDivs, &t0, &t1, 1 );
+    if ( RetValue )
+    {
+        Kit_DsdPrintFromTruth( (unsigned *)&t0, 6 ); printf( "\n" );
+        Kit_DsdPrintFromTruth( (unsigned *)&t1, 6 ); printf( "\n" );
+        printf( "Decomposition exits.\n" );
+    }
+
+
+    Vec_WrdFree( vDivs );
+    Rsb_ManFree( pManRsb );
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/misc/vec/vecWrd.h b/src/misc/vec/vecWrd.h
index 99aa1acb..a5beeb37 100644
--- a/src/misc/vec/vecWrd.h
+++ b/src/misc/vec/vecWrd.h
@@ -1120,6 +1120,24 @@ static inline void Vec_WrdSortUnsigned( Vec_Wrd_t * p )
 }
 
 
+/**Function*************************************************************
+
+  Synopsis    [Appends the contents of the second vector.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Vec_WrdAppend( Vec_Wrd_t * vVec1, Vec_Wrd_t * vVec2 )
+{
+    word Entry; int i;
+    Vec_WrdForEachEntry( vVec2, Entry, i )
+        Vec_WrdPush( vVec1, Entry );
+}
+
 
 ABC_NAMESPACE_HEADER_END