Skip to content

A
abc
Commit d5234332 by Alan Mishchenko
Options

New MFS package.

parent 283abd47
Showing with 102 additions and 73 deletions
src/base/abci/abcMfs.c
......@@ -134,6 +134,11 @@ void Abc_NtkInsertMfs( Abc_Ntk_t * pNtk, Sfm_Ntk_t * p )
if ( pNode->iTemp > 0 && !Sfm_NodeReadFixed(p, pNode->iTemp) )
{
vArray = Sfm_NodeReadFanins( p, pNode->iTemp );
if ( Vec_IntSize(vArray) == 0 )
{
Abc_NtkDeleteObj( pNode );
continue;
}
Vec_IntForEachEntry( vArray, Fanin, k )
Abc_ObjAddFanin( pNode, Abc_NtkObj(pNtk, Vec_IntEntry(vMap, Fanin)) );
pNode->pData = Abc_SopCreateFromTruth( (Mem_Flex_t *)pNtk->pManFunc, Vec_IntSize(vArray), (unsigned *)Sfm_NodeReadTruth(p, pNode->iTemp) );
......@@ -170,11 +175,11 @@ int Abc_NtkPerformMfs( Abc_Ntk_t * pNtk, Sfm_Par_t * pPars )
nNodes = Sfm_NtkPerform( p, pPars );
// call the fast extract procedure
if ( nNodes == 0 )
Abc_Print( 1, "The networks is not changed by \"mfs\".\n" );
Abc_Print( 1, "The network is not changed by \"mfs\".\n" );
else
{
Abc_NtkInsertMfs( pNtk, p );
Abc_Print( 1, "The networks has %d nodes changed by \"mfs\".\n", nNodes );
Abc_Print( 1, "The network has %d nodes changed by \"mfs\".\n", nNodes );
}
Sfm_NtkFree( p );
return 1;
......
src/base/io/io.c
......@@ -2663,22 +2663,22 @@ int IoCommandWriteTruth( Abc_Frame_t * pAbc, int argc, char **argv )
}
if ( pAbc->pNtkCur == NULL )
{
printf( "Current networks is not available.\n" );
printf( "Current network is not available.\n" );
return 0;
}
if ( !Abc_NtkIsLogic(pNtk) )
{
printf( "Current networks should not an AIG. Run \"logic\".\n" );
printf( "Current network should not an AIG. Run \"logic\".\n" );
return 0;
}
if ( Abc_NtkPoNum(pNtk) != 1 )
{
printf( "Current networks should have exactly one primary output.\n" );
printf( "Current network should have exactly one primary output.\n" );
return 0;
}
if ( Abc_NtkNodeNum(pNtk) != 1 )
{
printf( "Current networks should have exactly one node.\n" );
printf( "Current network should have exactly one node.\n" );
return 0;
}
pNode = Abc_ObjFanin0( Abc_NtkPo(pNtk, 0) );
......
src/map/scl/scl.c
......@@ -339,7 +339,7 @@ int Scl_CommandStime( Abc_Frame_t * pAbc, int argc, char **argv )
}
if ( !Abc_SclCheckNtk(Abc_FrameReadNtk(pAbc), 0) )
{
fprintf( pAbc->Err, "The current networks is not in a topo order (run \"topo\").\n" );
fprintf( pAbc->Err, "The current network is not in a topo order (run \"topo\").\n" );
return 1;
}
if ( pAbc->pLibScl == NULL )
......@@ -541,7 +541,7 @@ int Scl_CommandMinsize( Abc_Frame_t * pAbc, int argc, char **argv )
}
if ( !Abc_SclCheckNtk(Abc_FrameReadNtk(pAbc), 0) )
{
fprintf( pAbc->Err, "The current networks is not in a topo order (run \"topo\").\n" );
fprintf( pAbc->Err, "The current network is not in a topo order (run \"topo\").\n" );
return 1;
}
if ( pAbc->pLibScl == NULL )
......@@ -670,7 +670,7 @@ int Scl_CommandGsize( Abc_Frame_t * pAbc, int argc, char **argv )
}
if ( !Abc_SclCheckNtk(Abc_FrameReadNtk(pAbc), 0) )
{
fprintf( pAbc->Err, "The current networks is not in a topo order (run \"topo\").\n" );
fprintf( pAbc->Err, "The current network is not in a topo order (run \"topo\").\n" );
return 1;
}
if ( pAbc->pLibScl == NULL )
......@@ -827,7 +827,7 @@ int Scl_CommandUpsize( Abc_Frame_t * pAbc, int argc, char **argv )
}
if ( !Abc_SclCheckNtk(Abc_FrameReadNtk(pAbc), 0) )
{
fprintf( pAbc->Err, "The current networks is not in a topo order (run \"topo\").\n" );
fprintf( pAbc->Err, "The current network is not in a topo order (run \"topo\").\n" );
return 1;
}
if ( pAbc->pLibScl == NULL )
......
src/opt/sfm/sfm.h
......@@ -71,7 +71,7 @@ extern int Sfm_NtkPerform( Sfm_Ntk_t * p, Sfm_Par_t * pPars );
extern Sfm_Ntk_t * Sfm_NtkConstruct( Vec_Wec_t * vFanins, int nPis, int nPos, Vec_Str_t * vFixed, Vec_Wrd_t * vTruths );
extern void Sfm_NtkFree( Sfm_Ntk_t * p );
extern Vec_Int_t * Sfm_NodeReadFanins( Sfm_Ntk_t * p, int i );
extern word Sfm_NodeReadTruth( Sfm_Ntk_t * p, int i );
extern word * Sfm_NodeReadTruth( Sfm_Ntk_t * p, int i );
extern int Sfm_NodeReadFixed( Sfm_Ntk_t * p, int i );
/*=== sfmSat.c ==========================================================*/
......
src/opt/sfm/sfmCnf.c
......@@ -151,8 +151,8 @@ Vec_Wec_t * Sfm_CreateCnf( Sfm_Ntk_t * p )
void Sfm_TranslateCnf( Vec_Wec_t * vRes, Vec_Str_t * vCnf, Vec_Int_t * vFaninMap )
{
Vec_Int_t * vClause;
int i, Lit;
char Entry;
int i, Lit;
Vec_WecClear( vRes );
vClause = Vec_WecPushLevel( vRes );
Vec_StrForEachEntry( vCnf, Entry, i )
......
src/opt/sfm/sfmCore.c
......@@ -51,7 +51,7 @@ void Sfm_ParSetDefault( Sfm_Par_t * pPars )
pPars->nDivNumMax = 200; // the maximum number of divisors
pPars->nWinSizeMax = 500; // the maximum window size
pPars->nBTLimit = 0; // the maximum number of conflicts in one SAT run
pPars->fFixLevel = 0; // does not allow level to increase
pPars->fFixLevel = 1; // does not allow level to increase
pPars->fArea = 0; // performs optimization for area
pPars->fMoreEffort = 0; // performs high-affort minimization
pPars->fVerbose = 0; // enable basic stats
......@@ -71,14 +71,17 @@ void Sfm_ParSetDefault( Sfm_Par_t * pPars )
***********************************************************************/
void Sfm_NtkPrintStats( Sfm_Ntk_t * p )
{
printf( "Attempts : " );
printf( "Remove %5d (%6.2f%%) ", p->nRemoves, 100.0*p->nRemoves/p->nTryRemoves );
printf( "Resub %5d (%6.2f%%) ", p->nResubs, 100.0*p->nResubs /p->nTryResubs );
printf( "Nodes = %d. Try = %d. Resub = %d. Div = %d. SAT calls = %d. Timeouts = %d.\n",
Sfm_NtkNodeNum(p), p->nNodesTried, p->nRemoves + p->nResubs, p->nTotalDivs, p->nSatCalls, p->nTimeOuts );
printf( "Attempts : " );
printf( "Remove %6d -> %6d (%6.2f %%) ", p->nTryRemoves, p->nRemoves, 100.0*p->nRemoves/Abc_MaxInt(1, p->nTryRemoves) );
printf( "Resub %6d -> %6d (%6.2f %%) ", p->nTryResubs, p->nResubs, 100.0*p->nResubs /Abc_MaxInt(1, p->nTryResubs) );
printf( "\n" );
printf( "Reduction: " );
printf( "Nodes %5d (%6.2f%%) ", p->nTotalNodesBeg-p->nTotalNodesEnd, 100.0*(p->nTotalNodesBeg-p->nTotalNodesEnd)/p->nTotalNodesBeg );
printf( "Edges %5d (%6.2f%%) ", p->nTotalEdgesBeg-p->nTotalEdgesEnd, 100.0*(p->nTotalEdgesBeg-p->nTotalEdgesEnd)/p->nTotalEdgesBeg );
printf( "Reduction: " );
printf( "Nodes %6d -> %6d (%6.2f %%) ", p->nTotalNodesBeg, p->nTotalNodesEnd, 100.0*(p->nTotalNodesBeg-p->nTotalNodesEnd)/Abc_MaxInt(1, p->nTotalNodesBeg) );
printf( "Edges %6d -> %6d (%6.2f %%) ", p->nTotalEdgesBeg, p->nTotalEdgesEnd, 100.0*(p->nTotalEdgesBeg-p->nTotalEdgesEnd)/Abc_MaxInt(1, p->nTotalEdgesBeg) );
printf( "\n" );
ABC_PRTP( "Win", p->timeWin , p->timeTotal );
......@@ -101,7 +104,7 @@ void Sfm_NtkPrintStats( Sfm_Ntk_t * p )
***********************************************************************/
int Sfm_NodeResubSolve( Sfm_Ntk_t * p, int iNode, int f, int fRemoveOnly )
{
int fSkipUpdate = 1;
int fSkipUpdate = 0;
int fVeryVerbose = p->pPars->fVeryVerbose && Vec_IntSize(p->vDivs) < 200;// || pNode->Id == 556;
int i, iFanin, iVar = -1;
word uTruth, uSign, uMask;
......@@ -121,19 +124,22 @@ int Sfm_NodeResubSolve( Sfm_Ntk_t * p, int iNode, int f, int fRemoveOnly )
p->nCexes = 0;
Vec_WrdFill( p->vDivCexes, Vec_IntSize(p->vDivs), 0 );
// try removing the critical fanin
clk = clock();
Vec_IntClear( p->vDivIds );
Sfm_ObjForEachFanin( p, iNode, iFanin, i )
if ( i != f )
Vec_IntPush( p->vDivIds, Sfm_ObjSatVar(p, iFanin) );
clk = clock();
uTruth = Sfm_ComputeInterpolant( p );
p->timeSat += clock() - clk;
// analyze outcomes
if ( uTruth == SFM_SAT_UNDEC )
{
p->nTimeOuts++;
return 0;
if ( uTruth == SFM_SAT_SAT )
}
if ( uTruth != SFM_SAT_SAT )
goto finish;
if ( fRemoveOnly )
if ( fRemoveOnly || Vec_IntSize(p->vDivs) == 0 )
return 0;
if ( fVeryVerbose )
{
......@@ -160,14 +166,17 @@ p->timeSat += clock() - clk;
if ( iVar == Vec_IntSize(p->vDivs) )
return 0;
// try replacing the critical fanin
clk = clock();
Vec_IntPush( p->vDivIds, Sfm_ObjSatVar(p, Vec_IntEntry(p->vDivs, iVar)) );
clk = clock();
uTruth = Sfm_ComputeInterpolant( p );
p->timeSat += clock() - clk;
// analyze outcomes
if ( uTruth == SFM_SAT_UNDEC )
{
p->nTimeOuts++;
return 0;
if ( uTruth == SFM_SAT_SAT )
}
if ( uTruth != SFM_SAT_SAT )
goto finish;
if ( p->nCexes == 64 )
return 0;
......@@ -188,7 +197,7 @@ finish:
else
p->nResubs++;
if ( fSkipUpdate )
return 1;
return 0;
// update the network
Sfm_NtkUpdate( p, iNode, f, (iVar == -1 ? iVar : Vec_IntEntry(p->vDivs, iVar)), uTruth );
return 1;
......@@ -196,6 +205,7 @@ finish:
int Sfm_NodeResub( Sfm_Ntk_t * p, int iNode )
{
int i, iFanin;
p->nNodesTried++;
// prepare SAT solver
Sfm_NtkCreateWindow( p, iNode, p->pPars->fVeryVerbose );
Sfm_NtkWindowToSolver( p );
......@@ -240,26 +250,30 @@ int Sfm_NodeResub( Sfm_Ntk_t * p, int iNode )
***********************************************************************/
int Sfm_NtkPerform( Sfm_Ntk_t * p, Sfm_Par_t * pPars )
{
int i;
int i, Counter = 0;
p->timeTotal = clock();
p->pPars = pPars;
Sfm_NtkPrepare( p );
// Sfm_ComputeInterpolantCheck( p );
// return 0;
p->nTotalNodesBeg = Vec_WecSizeUsed(&p->vFanins) - Sfm_NtkPoNum(p);
p->nTotalEdgesBeg = Vec_WecSizeSize(&p->vFanins);
Sfm_NtkForEachNode( p, i )
{
if ( Sfm_ObjIsFixed( p, i ) )
continue;
if ( p->pPars->nDepthMax && Sfm_ObjLevel(p, i) > p->pPars->nDepthMax )
continue;
if ( Sfm_ObjFaninNum(p, i) < 2 || Sfm_ObjFaninNum(p, i) > 6 )
continue;
Sfm_NodeResub( p, i );
Counter += Sfm_NodeResub( p, i );
}
p->nTotalNodesEnd = Vec_WecSizeUsed(&p->vFanins) - Sfm_NtkPoNum(p);
p->nTotalEdgesEnd = Vec_WecSizeSize(&p->vFanins);
p->timeTotal = clock() - p->timeTotal;
if ( pPars->fVerbose )
Sfm_NtkPrintStats( p );
return 0;
return Counter;
}
////////////////////////////////////////////////////////////////////////
......
src/opt/sfm/sfmInt.h
......@@ -43,6 +43,9 @@ ABC_NAMESPACE_HEADER_START
#define SFM_FANIN_MAX 6
#define SFM_SAT_UNDEC 0x1234567812345678
#define SFM_SAT_SAT 0x8765432187654321
////////////////////////////////////////////////////////////////////////
/// BASIC TYPES ///
////////////////////////////////////////////////////////////////////////
......@@ -76,10 +79,10 @@ struct Sfm_Ntk_t_
// 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
Vec_Int_t * vRoots; // roots
Vec_Int_t * vTfo; // TFO (excluding iNode)
// SAT solving
sat_solver * pSat0; // SAT solver for the off-set
sat_solver * pSat1; // SAT solver for the on-set
......@@ -92,7 +95,7 @@ struct Sfm_Ntk_t_
int nCexes; // number of CEXes
Vec_Wrd_t * vDivCexes; // counter-examples
// intermediate data
Vec_Int_t * vFans; // current fanins
// Vec_Int_t * vFans; // current fanins
Vec_Int_t * vOrder; // object order
Vec_Int_t * vDivVars; // divisor SAT variables
Vec_Int_t * vDivIds; // divisors indexes
......@@ -104,6 +107,10 @@ struct Sfm_Ntk_t_
int nTotalEdgesBeg;
int nTotalNodesEnd;
int nTotalEdgesEnd;
int nNodesTried;
int nTotalDivs;
int nSatCalls;
int nTimeOuts;
// runtime
clock_t timeWin;
clock_t timeDiv;
......@@ -112,10 +119,6 @@ struct Sfm_Ntk_t_
clock_t timeTotal;
};
#define SFM_SAT_UNDEC 0x1234567812345678
#define SFM_SAT_SAT 0x8765432187654321
static inline int Sfm_NtkPiNum( Sfm_Ntk_t * p ) { return p->nPis; }
static inline int Sfm_NtkPoNum( Sfm_Ntk_t * p ) { return p->nPos; }
static inline int Sfm_NtkNodeNum( Sfm_Ntk_t * p ) { return p->nObjs - p->nPis - p->nPos; }
......@@ -123,6 +126,7 @@ static inline int Sfm_NtkNodeNum( Sfm_Ntk_t * p ) { return
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_ObjIsFixed( Sfm_Ntk_t * p, int i ) { return Vec_StrEntry(p->vFixed, i); }
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); }
......@@ -136,10 +140,10 @@ static inline int Sfm_ObjRefDecrement( Sfm_Ntk_t * p, int iObj ) { return
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 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_ObjSatVar( Sfm_Ntk_t * p, int iObj ) { assert(Vec_IntEntry(&p->vId2Var, iObj) > 0); return Vec_IntEntry(&p->vId2Var, iObj); }
static inline void Sfm_ObjSetSatVar( Sfm_Ntk_t * p, int iObj, int Num ) { assert(Vec_IntEntry(&p->vId2Var, 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 ) { int iObj = Vec_IntEntry(&p->vVar2Id, Num); assert(Vec_IntEntry(&p->vId2Var, iObj) > 0); Vec_IntWriteEntry(&p->vId2Var, iObj, -1); Vec_IntWriteEntry(&p->vVar2Id, Num, -1); }
static inline void Sfm_NtkCleanVars( Sfm_Ntk_t * p ) { int i; for ( i = 1; i < p->nSatVars; i++ ) Sfm_ObjCleanSatVar( p, i ); }
static inline int Sfm_ObjLevel( Sfm_Ntk_t * p, int iObj ) { return Vec_IntEntry( &p->vLevels, iObj ); }
static inline void Sfm_ObjSetLevel( Sfm_Ntk_t * p, int iObj, int Lev ) { Vec_IntWriteEntry( &p->vLevels, iObj, Lev ); }
......
src/opt/sfm/sfmNtk.c
......@@ -163,15 +163,15 @@ Sfm_Ntk_t * Sfm_NtkConstruct( Vec_Wec_t * vFanins, int nPis, int nPos, Vec_Str_t
}
void Sfm_NtkPrepare( Sfm_Ntk_t * p )
{
p->vDivCexes = Vec_WrdStart( p->pPars->nDivNumMax );
p->vLeaves = Vec_IntAlloc( 1000 );
p->vRoots = Vec_IntAlloc( 1000 );
p->vNodes = Vec_IntAlloc( 1000 );
p->vDivs = Vec_IntAlloc( 100 );
p->vRoots = Vec_IntAlloc( 1000 );
p->vTfo = Vec_IntAlloc( 1000 );
p->vFans = Vec_IntAlloc( 100 );
p->vDivCexes = Vec_WrdStart( p->pPars->nDivNumMax );
// p->vFans = Vec_IntAlloc( 100 );
p->vOrder = Vec_IntAlloc( 100 );
p->vDivVars = Vec_IntAlloc( 100 );
p->vDivs = Vec_IntAlloc( 100 );
p->vDivIds = Vec_IntAlloc( 1000 );
p->vLits = Vec_IntAlloc( 100 );
p->vClauses = Vec_WecAlloc( 100 );
......@@ -194,15 +194,15 @@ void Sfm_NtkFree( Sfm_Ntk_t * p )
Vec_WecFree( p->vCnfs );
Vec_IntFree( p->vCover );
// other data
Vec_WrdFreeP( &p->vDivCexes );
Vec_IntFreeP( &p->vLeaves );
Vec_IntFreeP( &p->vRoots );
Vec_IntFreeP( &p->vNodes );
Vec_IntFreeP( &p->vDivs );
Vec_IntFreeP( &p->vRoots );
Vec_IntFreeP( &p->vTfo );
Vec_IntFreeP( &p->vFans );
Vec_WrdFreeP( &p->vDivCexes );
// Vec_IntFreeP( &p->vFans );
Vec_IntFreeP( &p->vOrder );
Vec_IntFreeP( &p->vDivVars );
Vec_IntFreeP( &p->vDivs );
Vec_IntFreeP( &p->vDivIds );
Vec_IntFreeP( &p->vLits );
Vec_WecFreeP( &p->vClauses );
......@@ -243,8 +243,9 @@ void Sfm_NtkAddFanin( Sfm_Ntk_t * p, int iNode, int iFanin )
void Sfm_NtkDeleteObj_rec( Sfm_Ntk_t * p, int iNode )
{
int i, iFanin;
if ( Sfm_ObjFanoutNum(p, iNode) > 0 )
if ( Sfm_ObjFanoutNum(p, iNode) > 0 || Sfm_ObjIsPi(p, iNode) )
return;
assert( Sfm_ObjIsNode(p, iNode) );
Sfm_ObjForEachFanin( p, iNode, iFanin, i )
{
int RetValue = Vec_IntRemove( Sfm_ObjFoArray(p, iFanin), iNode ); assert( RetValue );
......@@ -260,13 +261,15 @@ void Sfm_NtkUpdateLevel_rec( Sfm_Ntk_t * p, int iNode )
if ( LevelNew == Sfm_ObjLevel(p, iNode) )
return;
Sfm_ObjSetLevel( p, iNode, LevelNew );
Sfm_ObjForEachFanout( p, iNode, iFanout, i )
Sfm_NtkUpdateLevel_rec( p, iFanout );
if ( Sfm_ObjIsNode(p, iNode) )
Sfm_ObjForEachFanout( p, iNode, iFanout, i )
Sfm_NtkUpdateLevel_rec( p, iFanout );
}
void Sfm_NtkUpdate( Sfm_Ntk_t * p, int iNode, int f, int iFaninNew, word uTruth )
{
int iFanin = Sfm_ObjFanin( p, iNode, f );
// replace old fanin by new fanin
assert( Sfm_ObjIsNode(p, iNode) );
Sfm_NtkRemoveFanin( p, iNode, iFanin );
Sfm_NtkAddFanin( p, iNode, iFaninNew );
// recursively remove MFFC
......@@ -293,9 +296,9 @@ Vec_Int_t * Sfm_NodeReadFanins( Sfm_Ntk_t * p, int i )
{
return Vec_WecEntry( &p->vFanins, i );
}
word Sfm_NodeReadTruth( Sfm_Ntk_t * p, int i )
word * Sfm_NodeReadTruth( Sfm_Ntk_t * p, int i )
{
return Vec_WrdEntry( p->vTruths, i );
return Vec_WrdEntryP( p->vTruths, i );
}
int Sfm_NodeReadFixed( Sfm_Ntk_t * p, int i )
{
......
src/opt/sfm/sfmSat.c
......@@ -54,7 +54,7 @@ static word s_Truths6[6] = {
void Sfm_NtkOrderObjects( Sfm_Ntk_t * p )
{
int i, iNode;
assert( Vec_IntEntryLast(p->vNodes) == Vec_IntEntry(p->vDivs, Vec_IntSize(p->vLeaves) + Vec_IntSize(p->vNodes)) );
assert( Vec_IntEntryLast(p->vNodes) == Vec_IntEntry(p->vDivs, Vec_IntSize(p->vLeaves) + Vec_IntSize(p->vNodes) - 1) );
Vec_IntClear( p->vOrder );
Vec_IntForEachEntryReverse( p->vNodes, iNode, i )
Vec_IntPush( p->vOrder, iNode );
......@@ -83,15 +83,14 @@ void Sfm_NtkWindowToSolver( Sfm_Ntk_t * p )
sat_solver_setnvars( pSat0, 1 + Vec_IntSize(p->vDivs) + 2 * Vec_IntSize(p->vTfo) + Vec_IntSize(p->vRoots) + 100 );
sat_solver_setnvars( pSat1, 1 + Vec_IntSize(p->vDivs) + 2 * Vec_IntSize(p->vTfo) + Vec_IntSize(p->vRoots) + 100 );
// create SAT variables
Sfm_NtkCleanVars( p );
p->nSatVars = 1;
Vec_IntForEachEntryReverse( p->vNodes, iNode, i )
Sfm_ObjSetSatVar( p, iNode, p->nSatVars++ );
Vec_IntForEachEntryReverse( p->vLeaves, iNode, i )
Sfm_NtkOrderObjects( p );
Vec_IntForEachEntry( p->vOrder, iNode, i )
Sfm_ObjSetSatVar( p, iNode, p->nSatVars++ );
Vec_IntForEachEntryReverse( p->vDivs, iNode, i )
Vec_IntForEachEntry( p->vLeaves, iNode, i )
Sfm_ObjSetSatVar( p, iNode, p->nSatVars++ );
// add CNF clauses for the TFI
Sfm_NtkOrderObjects( p );
Vec_IntForEachEntry( p->vOrder, iNode, i )
{
// collect fanin variables
......@@ -112,6 +111,7 @@ void Sfm_NtkWindowToSolver( Sfm_Ntk_t * p )
assert( RetValue );
}
}
// Sat_SolverWriteDimacs( pSat0, "test.cnf", NULL, NULL, 0 );
// get the last node
iNode = Vec_IntEntryLast( p->vNodes );
// add unit clause
......@@ -126,8 +126,8 @@ void Sfm_NtkWindowToSolver( Sfm_Ntk_t * p )
sat_solver_compress( pSat0 );
sat_solver_compress( pSat1 );
// return the result
assert( p->pSat0 == NULL );
assert( p->pSat1 == NULL );
if ( p->pSat0 ) sat_solver_delete( p->pSat0 );
if ( p->pSat1 ) sat_solver_delete( p->pSat1 );
p->pSat0 = pSat0;
p->pSat1 = pSat1;
p->timeCnf += clock() - clk;
......@@ -147,24 +147,29 @@ void Sfm_NtkWindowToSolver( Sfm_Ntk_t * p )
word Sfm_ComputeInterpolant( Sfm_Ntk_t * p )
{
word * pSign, uCube, uTruth = 0;
int status, i, Div, iVar, nFinal, * pFinal;
int status, i, Div, iVar, nFinal, * pFinal, nIter = 0;
int nVars = sat_solver_nvars( p->pSat1 );
int iNewLit = Abc_Var2Lit( nVars, 0 );
sat_solver_setnvars( p->pSat1, nVars + 1 );
while ( 1 )
{
// find onset minterm
p->nSatCalls++;
status = sat_solver_solve( p->pSat1, &iNewLit, &iNewLit + 1, p->pPars->nBTLimit, 0, 0, 0 );
if ( status == l_Undef )
return SFM_SAT_UNDEC;
if ( status == l_False )
{
// printf( "+%d ", nIter );
return uTruth;
}
assert( status == l_True );
// collect divisor literals
Vec_IntClear( p->vLits );
Vec_IntForEachEntry( p->vDivIds, Div, i )
Vec_IntPush( p->vLits, sat_solver_var_literal(p->pSat1, Div) );
// check against offset
p->nSatCalls++;
status = sat_solver_solve( p->pSat0, Vec_IntArray(p->vLits), Vec_IntArray(p->vLits) + Vec_IntSize(p->vLits), p->pPars->nBTLimit, 0, 0, 0 );
if ( status == l_Undef )
return SFM_SAT_UNDEC;
......@@ -185,7 +190,9 @@ word Sfm_ComputeInterpolant( Sfm_Ntk_t * p )
uTruth |= uCube;
status = sat_solver_addclause( p->pSat1, Vec_IntArray(p->vLits), Vec_IntArray(p->vLits) + Vec_IntSize(p->vLits) );
assert( status );
nIter++;
}
// printf( "-%d ", nIter );
assert( status == l_True );
// store the counter-example
Vec_IntForEachEntry( p->vDivVars, iVar, i )
......@@ -210,12 +217,11 @@ word Sfm_ComputeInterpolant( Sfm_Ntk_t * p )
SeeAlso []
***********************************************************************/
/*
void Sfm_ComputeInterpolantCheck( Sfm_Ntk_t * p )
{
int iNode = 3;
int iDiv0 = 6;
int iDiv1 = 7;
int iDiv0 = 5;
int iDiv1 = 4;
word uTruth;
// int i;
// Sfm_NtkForEachNode( p, i )
......@@ -228,7 +234,7 @@ void Sfm_ComputeInterpolantCheck( Sfm_Ntk_t * p )
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 );
uTruth = Sfm_ComputeInterpolant( p );
if ( uTruth == SFM_SAT_SAT )
printf( "The problem is SAT.\n" );
......@@ -236,13 +242,8 @@ void Sfm_ComputeInterpolantCheck( Sfm_Ntk_t * p )
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
......@@ -245,6 +245,7 @@ int Sfm_NtkCreateWindow( Sfm_Ntk_t * p, int iNode, int fVerbose )
assert( Sfm_ObjIsNode( p, iNode ) );
Vec_IntClear( p->vLeaves ); // leaves
Vec_IntClear( p->vNodes ); // internal
Vec_IntClear( p->vDivs ); // divisors
// collect transitive fanin
Sfm_NtkIncrementTravId( p );
Sfm_NtkCollectTfi_rec( p, iNode );
......@@ -266,12 +267,13 @@ int Sfm_NtkCreateWindow( Sfm_Ntk_t * p, int iNode, int fVerbose )
p->timeWin += clock() - clk;
// collect divisors of the TFI nodes
clk = clock();
Vec_IntClear( p->vDivs );
Vec_IntAppend( p->vDivs, p->vLeaves );
Vec_IntAppend( p->vDivs, p->vNodes );
Sfm_NtkIncrementTravId2( p );
Vec_IntForEachEntry( p->vDivs, iTemp, i )
Sfm_NtkAddDivisors( p, iTemp );
if ( Vec_IntSize(p->vDivs) < p->pPars->nDivNumMax )
Sfm_NtkAddDivisors( p, iTemp );
p->nTotalDivs += Vec_IntSize(p->vDivs);
p->timeDiv += clock() - clk;
if ( !fVerbose )
return 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