From d5234332fb29b7b50220df6a09d913d6832a425c Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Fri, 24 May 2013 22:35:22 -0700 Subject: New MFS package. --- src/base/abci/abcMfs.c | 9 +++++++-- src/base/io/io.c | 8 ++++---- src/map/scl/scl.c | 8 ++++---- src/opt/sfm/sfm.h | 2 +- src/opt/sfm/sfmCnf.c | 2 +- src/opt/sfm/sfmCore.c | 48 +++++++++++++++++++++++++++++++----------------- src/opt/sfm/sfmInt.h | 26 +++++++++++++++----------- src/opt/sfm/sfmNtk.c | 29 ++++++++++++++++------------- src/opt/sfm/sfmSat.c | 37 +++++++++++++++++++------------------ src/opt/sfm/sfmWin.c | 6 ++++-- 10 files changed, 102 insertions(+), 73 deletions(-) diff --git a/src/base/abci/abcMfs.c b/src/base/abci/abcMfs.c index ddc91467..5259ea03 100644 --- a/src/base/abci/abcMfs.c +++ b/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; diff --git a/src/base/io/io.c b/src/base/io/io.c index 9dee37a7..b472dac5 100644 --- a/src/base/io/io.c +++ b/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) ); diff --git a/src/map/scl/scl.c b/src/map/scl/scl.c index 49a7dcc3..4b856321 100644 --- a/src/map/scl/scl.c +++ b/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 ) diff --git a/src/opt/sfm/sfm.h b/src/opt/sfm/sfm.h index 5f266c68..b67fc8df 100644 --- a/src/opt/sfm/sfm.h +++ b/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 ==========================================================*/ diff --git a/src/opt/sfm/sfmCnf.c b/src/opt/sfm/sfmCnf.c index 09dce50c..126b6ca0 100644 --- a/src/opt/sfm/sfmCnf.c +++ b/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 ) diff --git a/src/opt/sfm/sfmCore.c b/src/opt/sfm/sfmCore.c index 7d206fa2..35c092fa 100644 --- a/src/opt/sfm/sfmCore.c +++ b/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; } //////////////////////////////////////////////////////////////////////// diff --git a/src/opt/sfm/sfmInt.h b/src/opt/sfm/sfmInt.h index 57c5e352..03d03111 100644 --- a/src/opt/sfm/sfmInt.h +++ b/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 ); } diff --git a/src/opt/sfm/sfmNtk.c b/src/opt/sfm/sfmNtk.c index 3098d72f..29463de6 100644 --- a/src/opt/sfm/sfmNtk.c +++ b/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 ) { diff --git a/src/opt/sfm/sfmSat.c b/src/opt/sfm/sfmSat.c index 86564744..f5355503 100644 --- a/src/opt/sfm/sfmSat.c +++ b/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 /// diff --git a/src/opt/sfm/sfmWin.c b/src/opt/sfm/sfmWin.c index e0baa96f..893a4592 100644 --- a/src/opt/sfm/sfmWin.c +++ b/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; -- cgit v1.2.3