New MFS package.

4 files changed, 145 insertions, 8 deletions

diff --git a/src/opt/sfm/sfm.h b/src/opt/sfm/sfm.h
index fd25a6a1..42f8156a 100644
--- a/src/opt/sfm/sfm.h
+++ b/src/opt/sfm/sfm.h
@@ -75,7 +75,7 @@ extern int          Sfm_ManPerform( Sfm_Ntk_t * p, Sfm_Par_t * pPars );
 extern Sfm_Man_t *  Sfm_ManAlloc( Sfm_Ntk_t * p );
 extern void         Sfm_ManFree( Sfm_Man_t * p );
 /*=== sfmNtk.c ==========================================================*/
-extern Sfm_Ntk_t *  Sfm_NtkAlloc( int nPis, int nPos, int nNodes, int nEdges );
+extern Sfm_Ntk_t *  Sfm_NtkAlloc( int nPis, int nPos, int nNodes, Vec_Int_t * vFanins, Vec_Int_t * vFanouts, Vec_Int_t * vEdges, Vec_Int_t * vOpts );
 extern void         Sfm_NtkFree( Sfm_Ntk_t * p );
 /*=== sfmSat.c ==========================================================*/
 
diff --git a/src/opt/sfm/sfmCnf.c b/src/opt/sfm/sfmCnf.c
index 9518c37a..77260b9d 100644
--- a/src/opt/sfm/sfmCnf.c
+++ b/src/opt/sfm/sfmCnf.c
@@ -19,6 +19,7 @@
 ***********************************************************************/
 
 #include "sfmInt.h"
+#include "bool/kit/kit.h"
 
 ABC_NAMESPACE_IMPL_START
 
@@ -42,11 +43,80 @@ ABC_NAMESPACE_IMPL_START
   SeeAlso     []
 
 ***********************************************************************/
-Vec_Int_t * Sfm_TruthToCnf( word Truth )
+int Sfm_TruthToCnf( word Truth, int nVars, Vec_Int_t * vCover, Vec_Str_t * vCnf )
 {
-    return NULL;
+    int nCubes = 0;
+    Vec_StrClear( vCnf );
+    if ( Truth == 0 || ~Truth == 0 )
+    {
+        Vec_StrPush( vCnf, (char)(Truth == 0) );
+        Vec_StrPush( vCnf, -1 );
+        return 1;
+    }
+    else 
+    {
+        int i, k, c, RetValue, Literal, Cube, nCubes = 0;
+        for ( c = 0; c < 2; c ++ )
+        {
+            Truth = c ? ~Truth : Truth;
+            RetValue = Kit_TruthIsop( (unsigned *)&Truth, nVars, vCover, 0 );
+            assert( RetValue == 0 );
+            nCubes += Vec_IntSize( vCover );
+            Vec_IntForEachEntry( vCover, Cube, i )
+            {
+                for ( k = 0; k < nVars; k++ )
+                {
+                    Literal = 3 & (Cube >> (k << 1));
+                    if ( Literal == 1 )      // '0'  -> pos lit
+                        Vec_StrPush( vCnf, (char)Abc_Var2Lit(k, 0) );
+                    else if ( Literal == 2 ) // '1'  -> neg lit
+                        Vec_StrPush( vCnf, (char)Abc_Var2Lit(k, 1) );
+                    else if ( Literal != 0 )
+                        assert( 0 );
+                }
+                Vec_StrPush( vCnf, (char)Abc_Var2Lit(nVars, c) );
+                Vec_StrPush( vCnf, -1 );
+            }
+        }
+        return nCubes;
+    }
 }
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Sfm_DeriveCnfs( Vec_Wrd_t * vTruths, Vec_Int_t * vFanins, Vec_Str_t ** pvCnfs, Vec_Int_t ** pvOffsets )
+{
+    Vec_Str_t * vCnfs, * vCnf;
+    Vec_Int_t * vOffsets, * vCover;
+    int i, k, nFanins, nClauses = 0;
+    vCnf     = Vec_StrAlloc( 1000 );
+    vCnfs    = Vec_StrAlloc( 1000 );
+    vOffsets = Vec_IntAlloc( Vec_IntSize(vFanins) );
+    vCover   = Vec_IntAlloc( 1 << 16 );
+    assert( Vec_WrdSize(vTruths) == Vec_IntSize(vFanins) );
+    Vec_IntForEachEntry( vFanins, nFanins, i )
+    {
+        nClauses += Sfm_TruthToCnf( Vec_WrdEntry(vTruths, i), nFanins, vCover, vCnf );
+        Vec_IntPush( vOffsets, Vec_StrSize(vCnfs) );
+        for ( k = 0; k < Vec_StrSize(vCnf); k++ )
+            Vec_StrPush( vCnfs, Vec_StrEntry(vCnf, k) );
+    }
+    Vec_IntPush( vOffsets, Vec_StrSize(vCnfs) );
+    Vec_StrFree( vCnf );
+    Vec_IntFree( vCover );
+    return nClauses;
+}
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/opt/sfm/sfmInt.h b/src/opt/sfm/sfmInt.h
index 66f1c216..9dad053f 100644
--- a/src/opt/sfm/sfmInt.h
+++ b/src/opt/sfm/sfmInt.h
@@ -65,7 +65,7 @@ struct Sfm_Obj_t_
 {
     unsigned          Type   :  2;
     unsigned          Id     : 30;
-    unsigned          fFixed :  1;
+    unsigned          fOpt   :  1;
     unsigned          fTfo   :  1;
     unsigned          nFanis :  4;
     unsigned          nFanos : 26;
@@ -88,12 +88,21 @@ struct Sfm_Man_t_
 ///                      MACRO DEFINITIONS                           ///
 ////////////////////////////////////////////////////////////////////////
 
+static inline Sfm_Obj_t * Sfm_ManObj( Sfm_Ntk_t * p, int Id ) { return (Sfm_Obj_t *)Vec_IntEntryP( &p->vObjs, Id ); }
+
+#define Sfm_ManForEachObj( p, pObj, i )                                \
+    for ( i = 0; (i < Vec_IntSize(&p->vObjs) && ((pObj) = Sfm_ManObj(p, i))); i++ )
+#define Sfm_ManForEachPi( p, pObj, i )                                 \
+    for ( i = 0; (i < Vec_IntSize(&p->vPis) && ((pObj) = Sfm_ManObj(p, Vec_IntEntry(&p->vPis, i)))); i++ )
+#define Sfm_ManForEachPo( p, pObj, i )                                 \
+    for ( i = 0; (i < Vec_IntSize(&p->vPos) && ((pObj) = Sfm_ManObj(p, Vec_IntEntry(&p->vPos, i)))); i++ )
+
 ////////////////////////////////////////////////////////////////////////
 ///                    FUNCTION DECLARATIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
 /*=== sfmCnf.c ==========================================================*/
-extern Vec_Int_t *  Sfm_TruthToCnf( word Truth );
+extern int          Sfm_DeriveCnfs( Vec_Wrd_t * vTruths, Vec_Int_t * vFanins, Vec_Str_t ** pvCnfs, Vec_Int_t ** pvOffsets );
 /*=== sfmCore.c ==========================================================*/
 /*=== sfmMan.c ==========================================================*/
 /*=== sfmNtk.c ==========================================================*/
diff --git a/src/opt/sfm/sfmNtk.c b/src/opt/sfm/sfmNtk.c
index 24ca514d..07a2e4ff 100644
--- a/src/opt/sfm/sfmNtk.c
+++ b/src/opt/sfm/sfmNtk.c
@@ -42,13 +42,71 @@ ABC_NAMESPACE_IMPL_START
   SeeAlso     []
 
 ***********************************************************************/
-Sfm_Ntk_t * Sfm_NtkAlloc( int nPis, int nPos, int nNodes, int nEdges )
+Sfm_Ntk_t * Sfm_NtkAlloc( int nPis, int nPos, int nNodes, Vec_Int_t * vFanins, Vec_Int_t * vFanouts, Vec_Int_t * vEdges, Vec_Int_t * vOpts )
 {
     Sfm_Ntk_t * p;
-    int AddOn = 2;
-    int nSize = (nPis + nPos + nNodes) * (sizeof(Sfm_Obj_t) / sizeof(int) + AddOn) + 2 * nEdges;
+    Sfm_Obj_t * pObj, * pFan;
+    int i, k, nObjSize, AddOn = 2;
+    int nStructSize = sizeof(Sfm_Obj_t) / sizeof(int);
+    int iFanin, iOffset = 2, iFanOffset = 0;
+    int nEdges = Vec_IntSize(vEdges);
+    int nObjs  = nPis + nPos + nNodes;
+    int nSize  = 2 + nObjs + nObjs * nStructSize + 2 * nEdges + AddOn * (nObjs - Vec_IntSum(vOpts));
+    assert( sizeof(Sfm_Obj_t) % sizeof(int) == 0 );
+    assert( nEdges == Vec_IntSum(vFanins) );
+    assert( nEdges == Vec_IntSum(vFanouts) );
     p = ABC_CALLOC( Sfm_Ntk_t, 1 );
     p->pMem = ABC_CALLOC( int, nSize );
+    for ( i = 0; i < nObjs; i++ )
+    {
+        Vec_IntPush( &p->vObjs, iOffset );
+        pObj = Sfm_ManObj( p, i );
+        pObj->Id  = i;
+        if ( i < nPis )
+        {
+            pObj->Type = 1;
+            assert( Vec_IntEntry(vFanins, i) == 0 );
+            assert( Vec_IntEntry(vOpts, i) == 0 );
+            Vec_IntPush( &p->vPis, iOffset );
+        }
+        else 
+        {
+            pObj->Type = 2;
+            pObj->fOpt = Vec_IntEntry(vOpts, i);
+            if ( i >= nPis + nNodes ) // PO
+            {
+                pObj->Type = 3;
+                assert( Vec_IntEntry(vFanins, i) == 1 );
+                assert( Vec_IntEntry(vFanouts, i) == 0 );
+                assert( Vec_IntEntry(vOpts, i) == 0 );
+                Vec_IntPush( &p->vPos, iOffset );
+            }
+            for ( k = 0; k < Vec_IntEntry(vFanins, i); k++ )
+            {
+                iFanin = Vec_IntEntry( vEdges, iFanOffset++ );
+                pFan = Sfm_ManObj( p, iFanin );
+                assert( iFanin < i );
+                pObj->Fanio[ pObj->nFanis++ ] = iFanin;
+                pFan->Fanio[ pFan->nFanis + pFan->nFanos++ ] = i;
+            }
+        }
+        // add node size
+        nObjSize  = nStructSize + Vec_IntEntry(vFanins, i) + Vec_IntEntry(vFanouts, i) + AddOn * pObj->fOpt;
+        nObjSize += (int)( nObjSize & 1 );
+        assert( (nObjSize & 1) == 0 );
+        iOffset  += nObjSize;
+    }
+    assert( iOffSet <= nSize );
+    assert( iFanOffset == Vec_IntSize(vEdges) );
+    iFanOffset = 0;
+    Sfm_ManForEachObj( p, pObj, i )
+    {
+        assert( Vec_IntEntry(vFanins, i) == pObj->nFanis );
+        assert( Vec_IntEntry(vFanouts, i) == pObj->nFanos );
+        for ( k = 0; k < (int)pObj->nFanis; k++ )
+            assert( pObj->Fanio[k] == Vec_IntEntry(vEdges, iFanOffset++) );
+    }
+    assert( iFanOffset == Vec_IntSize(vEdges) );
     return p;
 }
 void Sfm_NtkFree( Sfm_Ntk_t * p )