summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/opt/sfm/sfm.h2
-rw-r--r--src/opt/sfm/sfmCnf.c74
-rw-r--r--src/opt/sfm/sfmInt.h13
-rw-r--r--src/opt/sfm/sfmNtk.c64
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 )
generated by cgit v1.2.3 (git 2.25.1) at 2025-10-31 23:46:17 +0000