From e4cf178041c482b32482b85fdf9badcd020947c3 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Wed, 3 Apr 2013 12:39:24 -0700 Subject: New MFS package. --- src/opt/sfm/sfm.h | 2 +- src/opt/sfm/sfmCnf.c | 74 ++++++++++++++++++++++++++++++++++++++++++++++++++-- src/opt/sfm/sfmInt.h | 13 +++++++-- src/opt/sfm/sfmNtk.c | 64 ++++++++++++++++++++++++++++++++++++++++++--- 4 files changed, 145 insertions(+), 8 deletions(-) (limited to 'src/opt') 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 ) -- cgit v1.2.3