summaryrefslogtreecommitdiffstats
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/misc/vec/vecWec.h19
-rw-r--r--src/opt/sfm/sfmCore.c14
-rw-r--r--src/opt/sfm/sfmInt.h56
-rw-r--r--src/opt/sfm/sfmNtk.c37
-rw-r--r--src/opt/sfm/sfmSat.c129
-rw-r--r--src/opt/sfm/sfmWin.c219
6 files changed, 349 insertions, 125 deletions
diff --git a/src/misc/vec/vecWec.h b/src/misc/vec/vecWec.h
index ece7b0a1..a70d92ad 100644
--- a/src/misc/vec/vecWec.h
+++ b/src/misc/vec/vecWec.h
@@ -122,6 +122,11 @@ static inline void Vec_WecGrow( Vec_Wec_t * p, int nCapMin )
memset( p->pArray + p->nCap, 0, sizeof(Vec_Int_t) * (nCapMin - p->nCap) );
p->nCap = nCapMin;
}
+static inline void Vec_WecInit( Vec_Wec_t * p, int nSize )
+{
+ Vec_WecGrow( p, nSize );
+ p->nSize = nSize;
+}
/**Function*************************************************************
@@ -314,12 +319,24 @@ static inline double Vec_WecMemory( Vec_Wec_t * p )
SeeAlso []
***********************************************************************/
-static inline void Vec_WecFree( Vec_Wec_t * p )
+static inline void Vec_WecZero( Vec_Wec_t * p )
+{
+ p->pArray = NULL;
+ p->nSize = 0;
+ p->nCap = 0;
+}
+static inline void Vec_WecErase( Vec_Wec_t * p )
{
int i;
for ( i = 0; i < p->nCap; i++ )
ABC_FREE( p->pArray[i].pArray );
ABC_FREE( p->pArray );
+ p->nSize = 0;
+ p->nCap = 0;
+}
+static inline void Vec_WecFree( Vec_Wec_t * p )
+{
+ Vec_WecErase( p );
ABC_FREE( p );
}
static inline void Vec_WecFreeP( Vec_Wec_t ** p )
diff --git a/src/opt/sfm/sfmCore.c b/src/opt/sfm/sfmCore.c
index a8ff1e21..965d03cc 100644
--- a/src/opt/sfm/sfmCore.c
+++ b/src/opt/sfm/sfmCore.c
@@ -75,6 +75,8 @@ void Sfm_NtkPrepare( Sfm_Ntk_t * p )
p->vNodes = Vec_IntAlloc( 1000 );
p->vTfo = Vec_IntAlloc( 1000 );
p->vDivs = Vec_IntAlloc( 100 );
+ p->vDivIds = Vec_IntAlloc( 1000 );
+ p->vDiffs = Vec_IntAlloc( 1000 );
p->vLits = Vec_IntAlloc( 100 );
p->vClauses = Vec_WecAlloc( 100 );
p->vFaninMap = Vec_IntAlloc( 10 );
@@ -94,15 +96,19 @@ void Sfm_NtkPrepare( Sfm_Ntk_t * p )
***********************************************************************/
int Sfm_NtkPerform( Sfm_Ntk_t * p, Sfm_Par_t * pPars )
{
- int i;
+// int i;
p->pPars = pPars;
Sfm_NtkPrepare( p );
+ Sfm_ComputeInterpolantCheck( p );
+/*
Sfm_NtkForEachNode( p, i )
{
- printf( "Node %d:\n", i );
- Sfm_PrintCnf( (Vec_Str_t *)Vec_WecEntry(p->vCnfs, i) );
- printf( "\n" );
+// printf( "Node %d:\n", i );
+// Sfm_PrintCnf( (Vec_Str_t *)Vec_WecEntry(p->vCnfs, i) );
+// printf( "\n" );
+ Sfm_NtkWindow( p, i, 1 );
}
+*/
return 0;
}
diff --git a/src/opt/sfm/sfmInt.h b/src/opt/sfm/sfmInt.h
index d52b46e4..e2833121 100644
--- a/src/opt/sfm/sfmInt.h
+++ b/src/opt/sfm/sfmInt.h
@@ -55,33 +55,37 @@ struct Sfm_Ntk_t_
int nNodes; // internal nodes
int nObjs; // total objects
// user data
- Vec_Wec_t * vFanins; // fanins
Vec_Str_t * vFixed; // persistent objects
Vec_Wrd_t * vTruths; // truth tables
+ Vec_Wec_t vFanins; // fanins
// attributes
- Vec_Wec_t * vFanouts; // fanouts
- Vec_Int_t * vLevels; // logic level
- Vec_Int_t vTravIds; // traversal IDs
+ Vec_Wec_t vFanouts; // fanouts
+ Vec_Int_t vLevels; // logic level
+ Vec_Int_t vCounts; // fanin counters
Vec_Int_t vId2Var; // ObjId -> SatVar
Vec_Int_t vVar2Id; // SatVar -> ObjId
Vec_Wec_t * vCnfs; // CNFs
Vec_Int_t * vCover; // temporary
+ // traversal IDs
+ Vec_Int_t vTravIds; // traversal IDs
+ Vec_Int_t vTravIds2;// traversal IDs
int nTravIds; // traversal IDs
+ int nTravIds2;// traversal IDs
// window
int iNode;
Vec_Int_t * vLeaves; // leaves
Vec_Int_t * vRoots; // roots
Vec_Int_t * vNodes; // internal
Vec_Int_t * vTfo; // TFO (excluding iNode)
+ Vec_Int_t * vDivs; // divisors
// SAT solving
int nSatVars; // the number of variables
sat_solver * pSat1; // SAT solver for the on-set
sat_solver * pSat0; // SAT solver for the off-set
// intermediate data
- Vec_Int_t * vDivs; // divisors
+ Vec_Int_t * vDivIds; // divisors indexes
Vec_Int_t * vLits; // literals
- Vec_Int_t * vFani; // iterator fanins
- Vec_Int_t * vFano; // iterator fanouts
+ Vec_Int_t * vDiffs; // differences
Vec_Wec_t * vClauses; // CNF clauses for the node
Vec_Int_t * vFaninMap;// mapping fanins into their SAT vars
};
@@ -89,26 +93,38 @@ struct Sfm_Ntk_t_
#define SFM_SAT_UNDEC 0x1234567812345678
#define SFM_SAT_SAT 0x8765432187654321
-////////////////////////////////////////////////////////////////////////
-/// MACRO DEFINITIONS ///
-////////////////////////////////////////////////////////////////////////
-#define Sfm_NtkForEachNode( p, i ) for ( i = p->nPis; i + p->nPos < p->nObjs; i++ )
-#define Sfm_NodeForEachFanin( p, Node, Fan, i ) for ( p->vFani = Vec_WecEntry(p->vFanins, Node), i = 0; i < Vec_IntSize(p->vFani) && ((Fan = Vec_IntEntry(p->vFani, i)), 1); i++ )
-#define Sfm_NodeForEachFanout( p, Node, Fan, i ) for ( p->vFano = Vec_WecEntry(p->vFanouts, Node), i = 0; i < Vec_IntSize(p->vFani) && ((Fan = Vec_IntEntry(p->vFano, i)), 1); i++ )
+static inline int Sfm_ObjIsPi( Sfm_Ntk_t * p, int i ) { return i < p->nPis; }
+static inline int Sfm_ObjIsPo( Sfm_Ntk_t * p, int i ) { return i + p->nPos >= p->nObjs; }
+static inline int Sfm_ObjIsNode( Sfm_Ntk_t * p, int i ) { return i >= p->nPis && i + p->nPos < p->nObjs; }
+
+static inline Vec_Int_t * Sfm_ObjFiArray( Sfm_Ntk_t * p, int i ) { return Vec_WecEntry(&p->vFanins, i); }
+static inline Vec_Int_t * Sfm_ObjFoArray( Sfm_Ntk_t * p, int i ) { return Vec_WecEntry(&p->vFanouts, i); }
-static inline int Sfm_ObjIsPi( Sfm_Ntk_t * p, int i ) { return i < p->nPis; }
-static inline int Sfm_ObjIsPo( Sfm_Ntk_t * p, int i ) { return i + p->nPos < p->nObjs; }
-static inline int Sfm_ObjIsNode( Sfm_Ntk_t * p, int i ) { return i >= p->nPis && i + p->nPos < p->nObjs; }
+static inline int Sfm_ObjFaninNum( Sfm_Ntk_t * p, int i ) { return Vec_IntSize(Sfm_ObjFiArray(p, i)); }
+static inline int Sfm_ObjFanoutNum( Sfm_Ntk_t * p, int i ) { return Vec_IntSize(Sfm_ObjFoArray(p, i)); }
-static inline int Sfm_ObjFaninNum( Sfm_Ntk_t * p, int i ) { return Vec_IntSize(Vec_WecEntry(p->vFanins, i)); }
-static inline int Sfm_ObjFanoutNum( Sfm_Ntk_t * p, int i ) { return Vec_IntSize(Vec_WecEntry(p->vFanouts, i)); }
+static inline int Sfm_ObjFanin( Sfm_Ntk_t * p, int i, int k ) { return Vec_IntEntry(Sfm_ObjFiArray(p, i), k); }
+static inline int Sfm_ObjFanout( Sfm_Ntk_t * p, int i, int k ) { return Vec_IntEntry(Sfm_ObjFoArray(p, i), k); }
-static inline int Sfm_ObjSatVar( Sfm_Ntk_t * p, int iObj ) { return Vec_IntEntry(&p->vId2Var, iObj); }
+static inline int Sfm_ObjSatVar( Sfm_Ntk_t * p, int iObj ) { return Vec_IntEntry(&p->vId2Var, iObj); }
static inline void Sfm_ObjSetSatVar( Sfm_Ntk_t * p, int iObj, int Num ) { assert(Sfm_ObjSatVar(p, iObj) == -1); Vec_IntWriteEntry(&p->vId2Var, iObj, Num); Vec_IntWriteEntry(&p->vVar2Id, Num, iObj); }
static inline void Sfm_ObjCleanSatVar( Sfm_Ntk_t * p, int Num ) { assert(Sfm_ObjSatVar(p, Vec_IntEntry(&p->vVar2Id, Num)) != -1); Vec_IntWriteEntry(&p->vId2Var, Vec_IntEntry(&p->vVar2Id, Num), Num); Vec_IntWriteEntry(&p->vVar2Id, Num, -1); }
static inline void Sfm_NtkCleanVars( Sfm_Ntk_t * p, int nSize ) { int i; for ( i = 1; i < nSize; i++ ) Sfm_ObjCleanSatVar( p, i ); }
+static inline int Sfm_ObjLevel( Sfm_Ntk_t * p, int iObj ) { return Vec_IntEntry(&p->vLevels, iObj); }
+
+static inline int Sfm_ObjUpdateFaninCount( Sfm_Ntk_t * p, int iObj ) { return Vec_IntAddToEntry(&p->vCounts, iObj, -1); }
+static inline void Sfm_ObjResetFaninCount( Sfm_Ntk_t * p, int iObj ) { Vec_IntWriteEntry(&p->vCounts, iObj, Sfm_ObjFaninNum(p, iObj)-1); }
+
+
+////////////////////////////////////////////////////////////////////////
+/// MACRO DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+#define Sfm_NtkForEachNode( p, i ) for ( i = p->nPis; i + p->nPos < p->nObjs; i++ )
+#define Sfm_NodeForEachFanin( p, Node, Fan, i ) for ( i = 0; i < Sfm_ObjFaninNum(p, Node) && ((Fan = Sfm_ObjFanin(p, Node, i)), 1); i++ )
+#define Sfm_NodeForEachFanout( p, Node, Fan, i ) for ( i = 0; i < Sfm_ObjFanoutNum(p, Node) && ((Fan = Sfm_ObjFanout(p, Node, i)), 1); i++ )
////////////////////////////////////////////////////////////////////////
/// FUNCTION DECLARATIONS ///
@@ -124,7 +140,7 @@ extern Sfm_Ntk_t * Sfm_ConstructNetwork( Vec_Wec_t * vFanins, int nPis, int nPo
/*=== sfmSat.c ==========================================================*/
extern word Sfm_ComputeInterpolant( sat_solver * pSatOn, sat_solver * pSatOff, Vec_Int_t * vDivs, Vec_Int_t * vLits, Vec_Int_t * vDiffs, int nBTLimit );
/*=== sfmWin.c ==========================================================*/
-extern int Sfm_NtkWindow( Sfm_Ntk_t * p, int iNode );
+extern int Sfm_NtkWindow( Sfm_Ntk_t * p, int iNode, int fVerbose );
extern void Sfm_NtkWin2Sat( Sfm_Ntk_t * p );
diff --git a/src/opt/sfm/sfmNtk.c b/src/opt/sfm/sfmNtk.c
index 602f6d75..d9b17799 100644
--- a/src/opt/sfm/sfmNtk.c
+++ b/src/opt/sfm/sfmNtk.c
@@ -72,13 +72,12 @@ void Sfm_CheckConsistency( Vec_Wec_t * vFanins, int nPis, int nPos, Vec_Str_t *
SeeAlso []
***********************************************************************/
-Vec_Wec_t * Sfm_CreateFanout( Vec_Wec_t * vFanins )
+void Sfm_CreateFanout( Vec_Wec_t * vFanins, Vec_Wec_t * vFanouts )
{
- Vec_Wec_t * vFanouts;
Vec_Int_t * vArray;
int i, k, Fanin;
// count fanouts
- vFanouts = Vec_WecStart( Vec_WecSize(vFanins) );
+ Vec_WecInit( vFanouts, Vec_WecSize(vFanins) );
Vec_WecForEachLevel( vFanins, vArray, i )
Vec_IntForEachEntry( vArray, Fanin, k )
Vec_WecEntry( vFanouts, Fanin )->nSize++;
@@ -93,9 +92,8 @@ Vec_Wec_t * Sfm_CreateFanout( Vec_Wec_t * vFanins )
Vec_IntForEachEntry( vArray, Fanin, k )
Vec_IntPush( Vec_WecEntry( vFanouts, Fanin ), i );
// verify
- Vec_WecForEachLevel( vFanins, vArray, i )
+ Vec_WecForEachLevel( vFanouts, vArray, i )
assert( Vec_IntSize(vArray) == Vec_IntCap(vArray) );
- return vFanouts;
}
/**Function*************************************************************
@@ -109,17 +107,15 @@ Vec_Wec_t * Sfm_CreateFanout( Vec_Wec_t * vFanins )
SeeAlso []
***********************************************************************/
-Vec_Int_t * Sfm_CreateLevel( Vec_Wec_t * vFanins )
+void Sfm_CreateLevel( Vec_Wec_t * vFanins, Vec_Int_t * vLevels )
{
- Vec_Int_t * vLevels;
Vec_Int_t * vArray;
int i, k, Fanin, * pLevels;
- vLevels = Vec_IntStart( Vec_WecSize(vFanins) );
+ Vec_IntFill( vLevels, Vec_WecSize(vFanins), 0 );
pLevels = Vec_IntArray( vLevels );
Vec_WecForEachLevel( vFanins, vArray, i )
Vec_IntForEachEntry( vArray, Fanin, k )
pLevels[i] = Abc_MaxInt( pLevels[i], pLevels[Fanin] + 1 );
- return vLevels;
}
/**Function*************************************************************
@@ -143,7 +139,7 @@ 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 )
{
- Sfm_TruthToCnf( uTruth, Vec_IntSize(Vec_WecEntry(p->vFanins, i)), p->vCover, vCnf );
+ Sfm_TruthToCnf( uTruth, 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), Vec_StrSize(vCnf) );
@@ -173,14 +169,17 @@ Sfm_Ntk_t * Sfm_NtkConstruct( Vec_Wec_t * vFanins, int nPis, int nPos, Vec_Str_t
p->nPis = nPis;
p->nPos = nPos;
p->nNodes = p->nObjs - p->nPis - p->nPos;
- p->vFanins = vFanins;
// user data
p->vFixed = vFixed;
p->vTruths = vTruths;
+ p->vFanins = *vFanins;
+ ABC_FREE( vFanins );
// attributes
- p->vFanouts = Sfm_CreateFanout( vFanins );
- p->vLevels = Sfm_CreateLevel( vFanins );
+ Sfm_CreateFanout( &p->vFanins, &p->vFanouts );
+ Sfm_CreateLevel( &p->vFanins, &p->vLevels );
+ Vec_IntFill( &p->vCounts, p->nObjs, 0 );
Vec_IntFill( &p->vTravIds, p->nObjs, 0 );
+ Vec_IntFill( &p->vTravIds2, p->nObjs, 0 );
Vec_IntFill( &p->vId2Var, p->nObjs, -1 );
Vec_IntFill( &p->vVar2Id, p->nObjs, -1 );
p->vCover = Vec_IntAlloc( 1 << 16 );
@@ -190,13 +189,15 @@ Sfm_Ntk_t * Sfm_NtkConstruct( Vec_Wec_t * vFanins, int nPis, int nPos, Vec_Str_t
void Sfm_NtkFree( Sfm_Ntk_t * p )
{
// user data
- Vec_WecFree( p->vFanins );
Vec_StrFree( p->vFixed );
Vec_WrdFree( p->vTruths );
+ Vec_WecErase( &p->vFanins );
// attributes
- Vec_WecFree( p->vFanouts );
- Vec_IntFree( p->vLevels );
+ Vec_WecErase( &p->vFanouts );
+ ABC_FREE( p->vLevels.pArray );
+ ABC_FREE( p->vCounts.pArray );
ABC_FREE( p->vTravIds.pArray );
+ ABC_FREE( p->vTravIds2.pArray );
ABC_FREE( p->vId2Var.pArray );
ABC_FREE( p->vVar2Id.pArray );
Vec_WecFree( p->vCnfs );
@@ -207,7 +208,9 @@ void Sfm_NtkFree( Sfm_Ntk_t * p )
Vec_IntFreeP( &p->vNodes );
Vec_IntFreeP( &p->vTfo );
Vec_IntFreeP( &p->vDivs );
+ Vec_IntFreeP( &p->vDivIds );
Vec_IntFreeP( &p->vLits );
+ Vec_IntFreeP( &p->vDiffs );
Vec_WecFreeP( &p->vClauses );
Vec_IntFreeP( &p->vFaninMap );
if ( p->pSat0 ) sat_solver_delete( p->pSat0 );
@@ -228,7 +231,7 @@ void Sfm_NtkFree( Sfm_Ntk_t * p )
***********************************************************************/
Vec_Int_t * Sfm_NodeReadFanins( Sfm_Ntk_t * p, int i )
{
- return Vec_WecEntry( p->vFanins, i );
+ return Vec_WecEntry( &p->vFanins, i );
}
word Sfm_NodeReadTruth( Sfm_Ntk_t * p, int i )
{
diff --git a/src/opt/sfm/sfmSat.c b/src/opt/sfm/sfmSat.c
index 6431cd50..3ad97503 100644
--- a/src/opt/sfm/sfmSat.c
+++ b/src/opt/sfm/sfmSat.c
@@ -42,6 +42,78 @@ static word s_Truths6[6] = {
/**Function*************************************************************
+ Synopsis [Converts a window into a SAT solver.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Sfm_NtkWin2Sat( Sfm_Ntk_t * p )
+{
+ Vec_Int_t * vClause;
+ int RetValue, Lit, iNode = -1, iFanin, i, k, c;
+ sat_solver * pSat0 = sat_solver_new();
+ sat_solver * pSat1 = sat_solver_new();
+ sat_solver_setnvars( pSat0, 1 + Vec_IntSize(p->vLeaves) + Vec_IntSize(p->vNodes) + 2 * Vec_IntSize(p->vTfo) + Vec_IntSize(p->vRoots) );
+ sat_solver_setnvars( pSat1, 1 + Vec_IntSize(p->vLeaves) + Vec_IntSize(p->vNodes) + 2 * Vec_IntSize(p->vTfo) + Vec_IntSize(p->vRoots) );
+ // create SAT variables
+ p->nSatVars = 1;
+ Vec_IntForEachEntryReverse( p->vNodes, iNode, i )
+ Sfm_ObjSetSatVar( p, iNode, p->nSatVars++ );
+ Vec_IntForEachEntryReverse( p->vLeaves, iNode, i )
+ Sfm_ObjSetSatVar( p, iNode, p->nSatVars++ );
+ Vec_IntForEachEntryReverse( p->vDivs, iNode, i )
+ Sfm_ObjSetSatVar( p, iNode, p->nSatVars++ );
+ // add CNF clauses
+ for ( c = 0; c < 2; c++ )
+ {
+ Vec_Int_t * vObjs = c ? p->vDivs : p->vNodes;
+ Vec_IntForEachEntryReverse( vObjs, iNode, i )
+ {
+ // collect fanin variables
+ Vec_IntClear( p->vFaninMap );
+ Sfm_NodeForEachFanin( p, iNode, iFanin, k )
+ Vec_IntPush( p->vFaninMap, Sfm_ObjSatVar(p, iFanin) );
+ Vec_IntPush( p->vFaninMap, Sfm_ObjSatVar(p, iNode) );
+ // generate CNF
+ Sfm_TranslateCnf( p->vClauses, (Vec_Str_t *)Vec_WecEntry(p->vCnfs, iNode), p->vFaninMap );
+ // add clauses
+ Vec_WecForEachLevel( p->vClauses, vClause, k )
+ {
+ if ( Vec_IntSize(vClause) == 0 )
+ break;
+ RetValue = sat_solver_addclause( pSat0, Vec_IntArray(vClause), Vec_IntArray(vClause) + Vec_IntSize(vClause) );
+ assert( RetValue );
+ RetValue = sat_solver_addclause( pSat1, Vec_IntArray(vClause), Vec_IntArray(vClause) + Vec_IntSize(vClause) );
+ assert( RetValue );
+ }
+ }
+ }
+ // get the last node
+ iNode = Vec_IntEntryLast( p->vNodes );
+ // add unit clause
+ Lit = Abc_Var2Lit( Sfm_ObjSatVar(p, iNode), 1 );
+ RetValue = sat_solver_addclause( pSat0, &Lit, &Lit + 1 );
+ assert( RetValue );
+ // add unit clause
+ Lit = Abc_Var2Lit( Sfm_ObjSatVar(p, iNode), 0 );
+ RetValue = sat_solver_addclause( pSat1, &Lit, &Lit + 1 );
+ assert( RetValue );
+ // finalize
+ sat_solver_compress( pSat0 );
+ sat_solver_compress( pSat1 );
+ // return the result
+ assert( p->pSat0 == NULL );
+ assert( p->pSat1 == NULL );
+ p->pSat0 = pSat0;
+ p->pSat1 = pSat1;
+}
+
+/**Function*************************************************************
+
Synopsis [Takes SAT solver and returns interpolant.]
Description [If interpolant does not exist, returns diff SAT variables.]
@@ -51,12 +123,14 @@ static word s_Truths6[6] = {
SeeAlso []
***********************************************************************/
-word Sfm_ComputeInterpolant( sat_solver * pSatOn, sat_solver * pSatOff, Vec_Int_t * vDivs, Vec_Int_t * vLits, Vec_Int_t * vDiffs, int nBTLimit )
+word Sfm_ComputeInterpolant( sat_solver * pSatOn, sat_solver * pSatOff, Vec_Int_t * vDivIds, Vec_Int_t * vLits, Vec_Int_t * vDiffs, int nBTLimit )
{
word uTruth = 0, uCube;
int status, i, Div, iVar, nFinal, * pFinal;
int nVars = sat_solver_nvars(pSatOn);
int iNewLit = Abc_Var2Lit( nVars, 0 );
+ int RetValue;
+ sat_solver_setnvars( pSatOn, nVars + 1 );
while ( 1 )
{
// find onset minterm
@@ -68,8 +142,9 @@ word Sfm_ComputeInterpolant( sat_solver * pSatOn, sat_solver * pSatOff, Vec_Int_
assert( status == l_True );
// collect literals
Vec_IntClear( vLits );
- Vec_IntForEachEntry( vDivs, Div, i )
- Vec_IntPush( vLits, Abc_LitNot(sat_solver_var_literal(pSatOn, Div)) );
+ Vec_IntForEachEntry( vDivIds, Div, i )
+// Vec_IntPush( vLits, Abc_LitNot(sat_solver_var_literal(pSatOn, Div)) );
+ Vec_IntPush( vLits, sat_solver_var_literal(pSatOn, Div) );
// check against offset
status = sat_solver_solve( pSatOff, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits), nBTLimit, 0, 0, 0 );
if ( status == l_Undef )
@@ -90,16 +165,60 @@ word Sfm_ComputeInterpolant( sat_solver * pSatOn, sat_solver * pSatOff, Vec_Int_
for ( i = 0; i < nFinal; i++ )
{
Vec_IntPush( vLits, pFinal[i] );
- iVar = Vec_IntFind( vDivs, Abc_Lit2Var(pFinal[i]) ); assert( iVar >= 0 );
+ iVar = Vec_IntFind( vDivIds, Abc_Lit2Var(pFinal[i]) ); assert( iVar >= 0 );
uCube &= Abc_LitIsCompl(pFinal[i]) ? s_Truths6[iVar] : ~s_Truths6[iVar];
}
uTruth |= uCube;
- sat_solver_addclause( pSatOn, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits) );
+ RetValue = sat_solver_addclause( pSatOn, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits) );
+ assert( RetValue );
}
assert( 0 );
return 0;
}
+/**Function*************************************************************
+
+ Synopsis [Checks resubstitution.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Sfm_ComputeInterpolantCheck( Sfm_Ntk_t * p )
+{
+ int iNode = 3;
+ int iDiv0 = 6;
+ int iDiv1 = 7;
+ word uTruth;
+// int i;
+// Sfm_NtkForEachNode( p, i )
+ {
+ Sfm_NtkWindow( p, iNode, 1 );
+ Sfm_NtkWin2Sat( p );
+
+ // collect SAT variables of divisors
+ Vec_IntClear( p->vDivIds );
+ Vec_IntPush( p->vDivIds, Sfm_ObjSatVar(p, iDiv0) );
+ Vec_IntPush( p->vDivIds, Sfm_ObjSatVar(p, iDiv1) );
+
+ uTruth = Sfm_ComputeInterpolant( p->pSat1, p->pSat0, p->vDivIds, p->vLits, p->vDiffs, 0 );
+
+ if ( uTruth == SFM_SAT_SAT )
+ printf( "The problem is SAT.\n" );
+ else if ( uTruth == SFM_SAT_UNDEC )
+ printf( "The problem is UNDEC.\n" );
+ else
+ Kit_DsdPrintFromTruth( (unsigned *)&uTruth, 2 ); printf( "\n" );
+
+ Sfm_NtkCleanVars( p, p->nSatVars );
+ sat_solver_delete( p->pSat0 ); p->pSat0 = NULL;
+ sat_solver_delete( p->pSat1 ); p->pSat1 = NULL;
+ }
+}
+
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
diff --git a/src/opt/sfm/sfmWin.c b/src/opt/sfm/sfmWin.c
index c8f0af61..078406ba 100644
--- a/src/opt/sfm/sfmWin.c
+++ b/src/opt/sfm/sfmWin.c
@@ -42,9 +42,103 @@ ABC_NAMESPACE_IMPL_START
SeeAlso []
***********************************************************************/
-static inline void Sfm_NtkIncrementTravId( Sfm_Ntk_t * p ) { p->nTravIds++; }
-static inline void Sfm_ObjSetTravIdCurrent( Sfm_Ntk_t * p, int Id ) { Vec_IntWriteEntry( &p->vTravIds, Id, p->nTravIds ); }
-static inline int Sfm_ObjIsTravIdCurrent( Sfm_Ntk_t * p, int Id ) { return (Vec_IntEntry(&p->vTravIds, Id) == p->nTravIds); }
+static inline void Sfm_NtkIncrementTravId( Sfm_Ntk_t * p ) { p->nTravIds++; }
+static inline void Sfm_ObjSetTravIdCurrent( Sfm_Ntk_t * p, int Id ) { Vec_IntWriteEntry( &p->vTravIds, Id, p->nTravIds ); }
+static inline int Sfm_ObjIsTravIdCurrent( Sfm_Ntk_t * p, int Id ) { return (Vec_IntEntry(&p->vTravIds, Id) == p->nTravIds); }
+
+static inline void Sfm_NtkIncrementTravId2( Sfm_Ntk_t * p ) { p->nTravIds2++; }
+static inline void Sfm_ObjSetTravIdCurrent2( Sfm_Ntk_t * p, int Id ) { Vec_IntWriteEntry( &p->vTravIds2, Id, p->nTravIds2 ); }
+static inline int Sfm_ObjIsTravIdCurrent2( Sfm_Ntk_t * p, int Id ) { return (Vec_IntEntry(&p->vTravIds2, Id) == p->nTravIds2); }
+
+
+/**Function*************************************************************
+
+ Synopsis [Check if this fanout overlaps with TFI cone of the node.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Sfm_NtkCheckOverlap_rec( Sfm_Ntk_t * p, int iThis, int iNode )
+{
+ int i, iFanin;
+ if ( Sfm_ObjIsTravIdCurrent2(p, iThis) || iThis == iNode )
+ return 0;
+ if ( Sfm_ObjIsTravIdCurrent(p, iThis) )
+ return 1;
+ Sfm_ObjSetTravIdCurrent2(p, iThis);
+ Sfm_NodeForEachFanin( p, iThis, iFanin, i )
+ if ( Sfm_NtkCheckOverlap_rec(p, iFanin, iNode) )
+ return 1;
+ return 0;
+}
+int Sfm_NtkCheckOverlap( Sfm_Ntk_t * p, int iFan, int iNode )
+{
+ Sfm_NtkIncrementTravId2( p );
+ return Sfm_NtkCheckOverlap_rec( p, iFan, iNode );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Check fanouts of the node.]
+
+ Description [Returns 1 if they can be used instead of the node.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Sfm_NtkCheckFanouts( Sfm_Ntk_t * p, int iNode )
+{
+ int i, iFanout;
+ if ( Sfm_ObjFanoutNum(p, iNode) >= p->pPars->nFanoutMax )
+ return 0;
+ Sfm_NodeForEachFanout( p, iNode, iFanout, i )
+ if ( !Sfm_NtkCheckOverlap( p, iFanout, iNode ) )
+ return 0;
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Collects divisors of the node.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Sfm_NtkAddDivisors( Sfm_Ntk_t * p, int iNode )
+{
+ int i, iFanout;
+ Sfm_NodeForEachFanout( p, iNode, iFanout, i )
+ {
+ // skip TFI nodes, PO nodes, and nodes with high fanout or nodes with high logic level
+ if ( Sfm_ObjIsTravIdCurrent(p, iFanout) || Sfm_ObjIsPo(p, iFanout) ||
+ Sfm_ObjFanoutNum(p, iFanout) >= p->pPars->nFanoutMax ||
+ (p->pPars->fFixLevel && Sfm_ObjLevel(p, iFanout) >= Sfm_ObjLevel(p, iNode)) )
+ continue;
+ // handle single-input nodes
+ if ( Sfm_ObjFaninNum(p, iFanout) == 1 )
+ Vec_IntPush( p->vDivs, iFanout );
+ // visit node for the first time
+ else if ( !Sfm_ObjIsTravIdCurrent2(p, iFanout) )
+ {
+ assert( Sfm_ObjFaninNum(p, iFanout) > 1 );
+ Sfm_ObjSetTravIdCurrent2( p, iFanout );
+ Sfm_ObjResetFaninCount( p, iFanout );
+ }
+ // visit node again
+ else if ( Sfm_ObjUpdateFaninCount(p, iFanout) == 0 )
+ Vec_IntPush( p->vDivs, iFanout );
+ }
+}
/**Function*************************************************************
@@ -72,94 +166,63 @@ void Sfm_NtkCollectTfi_rec( Sfm_Ntk_t * p, int iNode )
Sfm_NtkCollectTfi_rec( p, iFanin );
Vec_IntPush( p->vNodes, iNode );
}
-int Sfm_NtkWindow( Sfm_Ntk_t * p, int iNode )
+int Sfm_NtkWindow( Sfm_Ntk_t * p, int iNode, int fVerbose )
{
-// int i, iRoot;
+ int i, iTemp;
+/*
+ if ( iNode == 7 )
+ {
+ int iLevel = Sfm_ObjLevel(p, iNode);
+ int s = 0;
+ }
+*/
assert( Sfm_ObjIsNode( p, iNode ) );
- Sfm_NtkIncrementTravId( p );
Vec_IntClear( p->vLeaves ); // leaves
Vec_IntClear( p->vNodes ); // internal
// collect transitive fanin
+ Sfm_NtkIncrementTravId( p );
Sfm_NtkCollectTfi_rec( p, iNode );
- // collect TFO
+ // collect TFO (currently use only one level of TFO)
Vec_IntClear( p->vRoots ); // roots
Vec_IntClear( p->vTfo ); // roots
- Vec_IntPush( p->vRoots, iNode );
-/*
- Vec_IntForEachEntry( p->vRoots, iRoot, i )
+ if ( Sfm_NtkCheckFanouts(p, iNode) )
{
- assert( Sfm_ObjIsNode(p, iRoot) );
- if ( Sfm_ObjIsTravIdCurrent(p, iRoot) )
- continue;
- if ( Sfm_ObjFanoutNum(p, iRoot) >= p->pPars->nFanoutMax )
- continue;
+ Sfm_NodeForEachFanout( p, iNode, iTemp, i )
+ {
+ if ( Sfm_ObjIsPo(p, iTemp) )
+ continue;
+ Vec_IntPush( p->vRoots, iTemp );
+ Vec_IntPush( p->vTfo, iTemp );
+ }
}
-*/
+ else
+ Vec_IntPush( p->vRoots, iNode );
+ // collect divisors of the TFI nodes
+ Vec_IntClear( p->vDivs );
+ Sfm_NtkIncrementTravId2( p );
+ Vec_IntForEachEntry( p->vLeaves, iTemp, i )
+ Sfm_NtkAddDivisors( p, iTemp );
+ Vec_IntForEachEntry( p->vNodes, iTemp, i )
+ Sfm_NtkAddDivisors( p, iTemp );
+ Vec_IntForEachEntry( p->vDivs, iTemp, i )
+ Sfm_NtkAddDivisors( p, iTemp );
+ if ( !fVerbose )
+ return 1;
+
+ // print stats about the window
+ printf( "%6d : ", iNode );
+ printf( "Leaves = %5d. ", Vec_IntSize(p->vLeaves) );
+ printf( "Nodes = %5d. ", Vec_IntSize(p->vNodes) );
+ printf( "Roots = %5d. ", Vec_IntSize(p->vRoots) );
+ printf( "Divs = %5d. ", Vec_IntSize(p->vDivs) );
+ printf( "\n" );
return 1;
}
-
-/**Function*************************************************************
-
- Synopsis [Converts a window into a SAT solver.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Sfm_NtkWin2Sat( Sfm_Ntk_t * p )
+void Sfm_NtkWindowTest( Sfm_Ntk_t * p, int iNode )
{
- Vec_Int_t * vClause;
- int RetValue, Lit, iNode = -1, iFanin, i, k;
- sat_solver * pSat0 = sat_solver_new();
- sat_solver * pSat1 = sat_solver_new();
- sat_solver_setnvars( pSat0, 1 + Vec_IntSize(p->vLeaves) + Vec_IntSize(p->vNodes) + 2 * Vec_IntSize(p->vTfo) + Vec_IntSize(p->vRoots) );
- sat_solver_setnvars( pSat1, 1 + Vec_IntSize(p->vLeaves) + Vec_IntSize(p->vNodes) + 2 * Vec_IntSize(p->vTfo) + Vec_IntSize(p->vRoots) );
- // create SAT variables
- p->nSatVars = 1;
- Vec_IntForEachEntryReverse( p->vNodes, iNode, i )
- Sfm_ObjSetSatVar( p, iNode, p->nSatVars++ );
- Vec_IntForEachEntryReverse( p->vLeaves, iNode, i )
- Sfm_ObjSetSatVar( p, iNode, p->nSatVars++ );
- // add CNF clauses
- Vec_IntForEachEntryReverse( p->vNodes, iNode, i )
- {
- // collect fanin variables
- Vec_IntClear( p->vFaninMap );
- Sfm_NodeForEachFanin( p, iNode, iFanin, k )
- Vec_IntPush( p->vFaninMap, Sfm_ObjSatVar(p, iFanin) );
- Vec_IntPush( p->vFaninMap, Sfm_ObjSatVar(p, iNode) );
- // generate CNF
- Sfm_TranslateCnf( p->vClauses, (Vec_Str_t *)Vec_WecEntry(p->vCnfs, iNode), p->vFaninMap );
- // add clauses
- Vec_WecForEachLevel( p->vClauses, vClause, k )
- {
- if ( Vec_IntSize(vClause) == 0 )
- break;
- RetValue = sat_solver_addclause( pSat0, Vec_IntArray(vClause), Vec_IntArray(vClause) + Vec_IntSize(vClause) );
- assert( RetValue );
- RetValue = sat_solver_addclause( pSat1, Vec_IntArray(vClause), Vec_IntArray(vClause) + Vec_IntSize(vClause) );
- assert( RetValue );
- }
- }
- // add unit clause
- Lit = Abc_Var2Lit( Sfm_ObjSatVar(p, iNode), 1 );
- RetValue = sat_solver_addclause( pSat0, &Lit, &Lit + 1 );
- assert( RetValue );
- // add unit clause
- Lit = Abc_Var2Lit( Sfm_ObjSatVar(p, iNode), 0 );
- RetValue = sat_solver_addclause( pSat1, &Lit, &Lit + 1 );
- assert( RetValue );
- // finalize
- sat_solver_compress( p->pSat0 );
- sat_solver_compress( p->pSat1 );
- // return the result
- assert( p->pSat0 == NULL );
- assert( p->pSat1 == NULL );
- p->pSat0 = pSat0;
- p->pSat1 = pSat1;
+ int i;
+ Sfm_NtkForEachNode( p, i )
+ Sfm_NtkWindow( p, i, 1 );
}
////////////////////////////////////////////////////////////////////////
generated by cgit v1.2.3 (git 2.25.1) at 2024-08-19 08:46:18 +0000