Allowing nodes and boxes to have more than 6 inputs in mfs2 and &mfs.

6 files changed, 65 insertions, 16 deletions

diff --git a/src/opt/sfm/sfm.h b/src/opt/sfm/sfm.h
index 002778dc..1aa8b7d0 100644
--- a/src/opt/sfm/sfm.h
+++ b/src/opt/sfm/sfm.h
@@ -87,7 +87,7 @@ struct Sfm_Par_t_
 extern void         Sfm_ParSetDefault( Sfm_Par_t * pPars );
 extern int          Sfm_NtkPerform( Sfm_Ntk_t * p, Sfm_Par_t * pPars );
 /*=== sfmNtk.c ==========================================================*/
-extern Sfm_Ntk_t *  Sfm_NtkConstruct( Vec_Wec_t * vFanins, int nPis, int nPos, Vec_Str_t * vFixed, Vec_Str_t * vEmpty, Vec_Wrd_t * vTruths );
+extern Sfm_Ntk_t *  Sfm_NtkConstruct( Vec_Wec_t * vFanins, int nPis, int nPos, Vec_Str_t * vFixed, Vec_Str_t * vEmpty, Vec_Wrd_t * vTruths, Vec_Int_t * vStarts, Vec_Wrd_t * vTruths2 );
 extern void         Sfm_NtkFree( Sfm_Ntk_t * p );
 extern Vec_Int_t *  Sfm_NodeReadFanins( Sfm_Ntk_t * p, int i );
 extern word *       Sfm_NodeReadTruth( Sfm_Ntk_t * p, int i );
diff --git a/src/opt/sfm/sfmCnf.c b/src/opt/sfm/sfmCnf.c
index ce2f34b8..f6d434f8 100644
--- a/src/opt/sfm/sfmCnf.c
+++ b/src/opt/sfm/sfmCnf.c
@@ -68,24 +68,63 @@ void Sfm_PrintCnf( Vec_Str_t * vCnf )
   SeeAlso     []
 
 ***********************************************************************/
-int Sfm_TruthToCnf( word Truth, int nVars, Vec_Int_t * vCover, Vec_Str_t * vCnf )
+int Sfm_TruthToCnf( word Truth, word * pTruth, int nVars, Vec_Int_t * vCover, Vec_Str_t * vCnf )
 {
+    int w, nWords = Abc_Truth6WordNum( nVars );
     Vec_StrClear( vCnf );
-    if ( Truth == 0 || ~Truth == 0 )
+    if ( nVars <= 6 )
     {
-//        assert( nVars == 0 );
-        Vec_StrPush( vCnf, (char)(Truth == 0) );
-        Vec_StrPush( vCnf, (char)-1 );
-        return 1;
+        if ( Truth == 0 || ~Truth == 0 )
+        {
+            //assert( nVars == 0 );
+            Vec_StrPush( vCnf, (char)(Truth == 0) );
+            Vec_StrPush( vCnf, (char)-1 );
+            return 1;
+        }
+    }
+    else
+    {
+        // const0
+        for ( w = 0; w < nWords; w++ )
+            if ( pTruth[w] )
+                break;
+        if ( w == nWords )
+        {
+            Vec_StrPush( vCnf, (char)1 );
+            Vec_StrPush( vCnf, (char)-1 );
+            return 1;
+        }
+        // const1
+        for ( w = 0; w < nWords; w++ )
+            if ( ~pTruth[w] )
+                break;
+        if ( w == nWords )
+        {
+            Vec_StrPush( vCnf, (char)0 );
+            Vec_StrPush( vCnf, (char)-1 );
+            return 1;
+        }
     }
-    else 
     {
         int i, k, c, RetValue, Literal, Cube, nCubes = 0;
         assert( nVars > 0 );
         for ( c = 0; c < 2; c ++ )
         {
-            Truth = c ? ~Truth : Truth;
-            RetValue = Kit_TruthIsop( (unsigned *)&Truth, nVars, vCover, 0 );
+            if ( nVars <= 6 )
+            {
+                Truth = c ? ~Truth : Truth;
+                RetValue = Kit_TruthIsop( (unsigned *)&Truth, nVars, vCover, 0 );
+            }
+            else
+            {
+                if ( c )
+                    for ( k = 0; k < nWords; k++ )
+                        pTruth[k] = ~pTruth[k];
+                RetValue = Kit_TruthIsop( (unsigned *)pTruth, nVars, vCover, 0 );
+                if ( c )
+                    for ( k = 0; k < nWords; k++ )
+                        pTruth[k] = ~pTruth[k];
+            }
             assert( RetValue == 0 );
             nCubes += Vec_IntSize( vCover );
             Vec_IntForEachEntry( vCover, Cube, i )
@@ -129,7 +168,9 @@ Vec_Wec_t * Sfm_CreateCnf( Sfm_Ntk_t * p )
     vCnfs = Vec_WecStart( p->nObjs );
     Vec_WrdForEachEntryStartStop( p->vTruths, uTruth, i, p->nPis, Vec_WrdSize(p->vTruths)-p->nPos )
     {
-        nCubes = Sfm_TruthToCnf( uTruth, Sfm_ObjFaninNum(p, i), p->vCover, vCnf );
+        int Offset  = Vec_IntEntry( p->vStarts, i );
+        word * pRes = Vec_WrdSize(p->vTruths2) ? Vec_WrdEntryP( p->vTruths2, Offset ) : NULL;
+        nCubes = Sfm_TruthToCnf( uTruth, pRes, Sfm_ObjFaninNum(p, i), p->vCover, vCnf );
         vCnfBase = (Vec_Str_t *)Vec_WecEntry( vCnfs, i );
         Vec_StrGrow( vCnfBase, Vec_StrSize(vCnf) );
         memcpy( Vec_StrArray(vCnfBase), Vec_StrArray(vCnf), (size_t)Vec_StrSize(vCnf) );
diff --git a/src/opt/sfm/sfmInt.h b/src/opt/sfm/sfmInt.h
index 2b96d4bd..80edd54d 100644
--- a/src/opt/sfm/sfmInt.h
+++ b/src/opt/sfm/sfmInt.h
@@ -81,6 +81,8 @@ struct Sfm_Ntk_t_
     Vec_Str_t *       vEmpty;      // transparent objects
     Vec_Wrd_t *       vTruths;     // truth tables
     Vec_Wec_t         vFanins;     // fanins
+    Vec_Int_t *       vStarts;     // offsets
+    Vec_Wrd_t *       vTruths2;    // truth tables (large)
     // attributes
     Vec_Wec_t         vFanouts;    // fanouts
     Vec_Int_t         vLevels;     // logic level
@@ -195,7 +197,7 @@ extern void        Kit_DsdPrintFromTruth( unsigned * pTruth, int nVars );
 
 /*=== sfmCnf.c ==========================================================*/
 extern void         Sfm_PrintCnf( Vec_Str_t * vCnf );
-extern int          Sfm_TruthToCnf( word Truth, int nVars, Vec_Int_t * vCover, Vec_Str_t * vCnf );
+extern int          Sfm_TruthToCnf( word Truth, word * pTruth, int nVars, Vec_Int_t * vCover, Vec_Str_t * vCnf );
 extern Vec_Wec_t *  Sfm_CreateCnf( Sfm_Ntk_t * p );
 extern void         Sfm_TranslateCnf( Vec_Wec_t * vRes, Vec_Str_t * vCnf, Vec_Int_t * vFaninMap, int iPivotVar );
 /*=== sfmCore.c ==========================================================*/
diff --git a/src/opt/sfm/sfmLib.c b/src/opt/sfm/sfmLib.c
index afb4a48d..18ba0971 100644
--- a/src/opt/sfm/sfmLib.c
+++ b/src/opt/sfm/sfmLib.c
@@ -107,7 +107,7 @@ void Sfm_DecCreateCnf( Vec_Int_t * vGateSizes, Vec_Wrd_t * vGateFuncs, Vec_Wec_t
     vCover = Vec_IntAlloc( 100 );
     Vec_WrdForEachEntry( vGateFuncs, uTruth, i )
     {
-        nCubes = Sfm_TruthToCnf( uTruth, Vec_IntEntry(vGateSizes, i), vCover, vCnf );
+        nCubes = Sfm_TruthToCnf( uTruth, NULL, Vec_IntEntry(vGateSizes, i), vCover, vCnf );
         vCnfBase = (Vec_Str_t *)Vec_WecEntry( vGateCnfs, i );
         Vec_StrGrow( vCnfBase, Vec_StrSize(vCnf) );
         memcpy( Vec_StrArray(vCnfBase), Vec_StrArray(vCnf), (size_t)Vec_StrSize(vCnf) );
diff --git a/src/opt/sfm/sfmNtk.c b/src/opt/sfm/sfmNtk.c
index 1ded0ede..d410aa0b 100644
--- a/src/opt/sfm/sfmNtk.c
+++ b/src/opt/sfm/sfmNtk.c
@@ -164,7 +164,7 @@ void Sfm_CreateLevelR( Vec_Wec_t * vFanouts, Vec_Int_t * vLevelsR, Vec_Str_t * v
   SeeAlso     []
 
 ***********************************************************************/
-Sfm_Ntk_t * Sfm_NtkConstruct( Vec_Wec_t * vFanins, int nPis, int nPos, Vec_Str_t * vFixed, Vec_Str_t * vEmpty, Vec_Wrd_t * vTruths )
+Sfm_Ntk_t * Sfm_NtkConstruct( Vec_Wec_t * vFanins, int nPis, int nPos, Vec_Str_t * vFixed, Vec_Str_t * vEmpty, Vec_Wrd_t * vTruths, Vec_Int_t * vStarts, Vec_Wrd_t * vTruths2 )
 {
     Sfm_Ntk_t * p;
     Sfm_CheckConsistency( vFanins, nPis, nPos, vFixed );
@@ -178,6 +178,8 @@ Sfm_Ntk_t * Sfm_NtkConstruct( Vec_Wec_t * vFanins, int nPis, int nPos, Vec_Str_t
     p->vEmpty   = vEmpty;
     p->vTruths  = vTruths;
     p->vFanins  = *vFanins;
+    p->vStarts  = vStarts;
+    p->vTruths2 = vTruths2;
     ABC_FREE( vFanins );
     // attributes
     Sfm_CreateFanout( &p->vFanins, &p->vFanouts );
@@ -217,6 +219,8 @@ void Sfm_NtkFree( Sfm_Ntk_t * p )
     Vec_StrFreeP( &p->vEmpty );
     Vec_WrdFree( p->vTruths );
     Vec_WecErase( &p->vFanins );
+    Vec_IntFree( p->vStarts );
+    Vec_WrdFree( p->vTruths2 );
     // attributes
     Vec_WecErase( &p->vFanouts );
     ABC_FREE( p->vLevels.pArray );
@@ -316,6 +320,7 @@ void Sfm_NtkUpdate( Sfm_Ntk_t * p, int iNode, int f, int iFaninNew, word uTruth
     int iFanin = Sfm_ObjFanin( p, iNode, f );
     assert( Sfm_ObjIsNode(p, iNode) );
     assert( iFanin != iFaninNew );
+    assert( Sfm_ObjFaninNum(p, iNode) <= 6 );
     if ( uTruth == 0 || ~uTruth == 0 )
     {
         Sfm_ObjForEachFanin( p, iNode, iFanin, f )
@@ -341,7 +346,7 @@ void Sfm_NtkUpdate( Sfm_Ntk_t * p, int iNode, int f, int iFaninNew, word uTruth
         Sfm_NtkUpdateLevelR_rec( p, iFanin );
     // update truth table
     Vec_WrdWriteEntry( p->vTruths, iNode, uTruth );
-    Sfm_TruthToCnf( uTruth, Sfm_ObjFaninNum(p, iNode), p->vCover, (Vec_Str_t *)Vec_WecEntry(p->vCnfs, iNode) );
+    Sfm_TruthToCnf( uTruth, NULL, Sfm_ObjFaninNum(p, iNode), p->vCover, (Vec_Str_t *)Vec_WecEntry(p->vCnfs, iNode) );
 }
 
 /**Function*************************************************************
@@ -361,7 +366,7 @@ Vec_Int_t *  Sfm_NodeReadFanins( Sfm_Ntk_t * p, int i )
 }
 word * Sfm_NodeReadTruth( Sfm_Ntk_t * p, int i )
 {
-    return Vec_WrdEntryP( p->vTruths, i );
+    return Sfm_ObjFaninNum(p, i) <= 6 ? Vec_WrdEntryP( p->vTruths, i ) : Vec_WrdEntryP( p->vTruths2, Vec_IntEntry(p->vStarts, i) );
 }
 int Sfm_NodeReadFixed( Sfm_Ntk_t * p, int i )
 {
diff --git a/src/opt/sfm/sfmSat.c b/src/opt/sfm/sfmSat.c
index 8bcb7f8a..6ccdd903 100644
--- a/src/opt/sfm/sfmSat.c
+++ b/src/opt/sfm/sfmSat.c
@@ -167,6 +167,7 @@ word Sfm_ComputeInterpolant( Sfm_Ntk_t * p )
     sat_solver_setnvars( p->pSat, nVars + 1 );
     pLits[0] = Abc_Var2Lit( Sfm_ObjSatVar(p, p->iPivotNode), 0 ); // F = 1
     pLits[1] = Abc_Var2Lit( nVars, 0 ); // iNewLit
+    assert( Vec_IntSize(p->vDivIds) <= 6 );
     while ( 1 ) 
     {
         // find onset minterm