Skip to content

A
abc
Commit ac037cbb by Alan Mishchenko
Options

New MFS package.

parent 78d60d98
Showing with 349 additions and 125 deletions
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 )
......
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;
}
......
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 );
......
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 )
{
......
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 ///
////////////////////////////////////////////////////////////////////////
......
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 );
}
////////////////////////////////////////////////////////////////////////
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment