From 94a75fe6d8f8709603dbf9e5bf959174dc3342ac Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sat, 25 May 2013 18:10:45 -0700 Subject: New MFS package. --- src/base/abci/abc.c | 4 +-- src/base/abci/abcMfs.c | 11 ++++++- src/opt/mfs/mfsCore.c | 4 +-- src/opt/mfs/mfsDiv.c | 4 +-- src/opt/mfs/mfsMan.c | 4 +-- src/opt/mfs/mfsResub.c | 8 +++--- src/opt/sfm/sfm.h | 25 ++++++++-------- src/opt/sfm/sfmCore.c | 27 ++++++++--------- src/opt/sfm/sfmInt.h | 11 +++---- src/opt/sfm/sfmNtk.c | 17 +++++------ src/opt/sfm/sfmSat.c | 78 +++++++++++++++++++------------------------------- src/opt/sfm/sfmWin.c | 27 ++++++++++++----- 12 files changed, 111 insertions(+), 109 deletions(-) diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 5f100fb0..cb3e1f1e 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -4327,7 +4327,7 @@ int Abc_CommandMfs( Abc_Frame_t * pAbc, int argc, char ** argv ) } pPars->nFanoutsMax = atoi(argv[globalUtilOptind]); globalUtilOptind++; - if ( pPars->nFanoutsMax < 1 ) + if ( pPars->nFanoutsMax < 0 ) goto usage; break; case 'D': @@ -4496,7 +4496,7 @@ int Abc_CommandMfs2( Abc_Frame_t * pAbc, int argc, char ** argv ) } pPars->nFanoutMax = atoi(argv[globalUtilOptind]); globalUtilOptind++; - if ( pPars->nFanoutMax < 1 ) + if ( pPars->nFanoutMax < 0 ) goto usage; break; case 'D': diff --git a/src/base/abci/abcMfs.c b/src/base/abci/abcMfs.c index 9c0513de..7953be15 100644 --- a/src/base/abci/abcMfs.c +++ b/src/base/abci/abcMfs.c @@ -19,6 +19,7 @@ ***********************************************************************/ #include "base/abc/abc.h" +#include "bool/kit/kit.h" #include "opt/sfm/sfm.h" ABC_NAMESPACE_IMPL_START @@ -120,6 +121,7 @@ Sfm_Ntk_t * Abc_NtkExtractMfs( Abc_Ntk_t * pNtk ) ***********************************************************************/ void Abc_NtkInsertMfs( Abc_Ntk_t * pNtk, Sfm_Ntk_t * p ) { + Vec_Int_t * vCover = Sfm_NodeReadCover(p); Vec_Int_t * vMap, * vArray; Abc_Obj_t * pNode; int i, k, Fanin; @@ -155,7 +157,14 @@ void Abc_NtkInsertMfs( Abc_Ntk_t * pNtk, Sfm_Ntk_t * p ) else if ( ~pTruth[0] == 0 ) pNode->pData = Abc_SopRegister( (Mem_Flex_t *)pNtk->pManFunc, " 1\n" ); else - pNode->pData = Abc_SopCreateFromTruth( (Mem_Flex_t *)pNtk->pManFunc, Vec_IntSize(vArray), (unsigned *)pTruth ); + { +// pNode->pData = Abc_SopCreateFromTruth( (Mem_Flex_t *)pNtk->pManFunc, Vec_IntSize(vArray), (unsigned *)pTruth ); + int RetValue = Kit_TruthIsop( (unsigned *)pTruth, Vec_IntSize(vArray), vCover, 1 ); + assert( RetValue == 0 || RetValue == 1 ); + pNode->pData = Abc_SopCreateFromIsop( (Mem_Flex_t *)pNtk->pManFunc, Vec_IntSize(vArray), vCover ); + if ( RetValue ) + Abc_SopComplement( (char *)pNode->pData ); + } } Vec_IntFree( vMap ); } diff --git a/src/opt/mfs/mfsCore.c b/src/opt/mfs/mfsCore.c index 22a28e22..d652d8cd 100644 --- a/src/opt/mfs/mfsCore.c +++ b/src/opt/mfs/mfsCore.c @@ -48,7 +48,7 @@ void Abc_NtkMfsParsDefault( Mfs_Par_t * pPars ) { memset( pPars, 0, sizeof(Mfs_Par_t) ); pPars->nWinTfoLevs = 2; - pPars->nFanoutsMax = 10; + pPars->nFanoutsMax = 30; pPars->nDepthMax = 20; pPars->nDivMax = 250; pPars->nWinSizeMax = 300; @@ -406,7 +406,7 @@ int Abc_NtkMfs( Abc_Ntk_t * pNtk, Mfs_Par_t * pPars ) } } // perform the network sweep - Abc_NtkSweep( pNtk, 0 ); +// Abc_NtkSweep( pNtk, 0 ); // convert into the AIG if ( !Abc_NtkToAig(pNtk) ) { diff --git a/src/opt/mfs/mfsDiv.c b/src/opt/mfs/mfsDiv.c index 1473580e..0b29673e 100644 --- a/src/opt/mfs/mfsDiv.c +++ b/src/opt/mfs/mfsDiv.c @@ -214,7 +214,7 @@ Vec_Ptr_t * Abc_MfsComputeDivisors( Mfs_Man_t * p, Abc_Obj_t * pNode, int nLevDi // (3) the node's fanins (these are treated as a special case) Abc_NtkIncrementTravId( pNode->pNtk ); Abc_MfsWinSweepLeafTfo_rec( pNode, nLevDivMax ); - Abc_MfsWinVisitMffc( pNode ); +// Abc_MfsWinVisitMffc( pNode ); Abc_ObjForEachFanin( pNode, pObj, k ) Abc_NodeSetTravIdCurrent( pObj ); @@ -244,7 +244,7 @@ Vec_Ptr_t * Abc_MfsComputeDivisors( Mfs_Man_t * p, Abc_Obj_t * pNode, int nLevDi Abc_ObjForEachFanout( pObj, pFanout, f ) { // stop if there are too many fanouts - if ( f > 20 ) + if ( p->pPars->nFanoutsMax && f > p->pPars->nFanoutsMax ) break; // skip nodes that are already added if ( Abc_NodeIsTravIdPrevious(pFanout) ) diff --git a/src/opt/mfs/mfsMan.c b/src/opt/mfs/mfsMan.c index 3ed6436f..401c6edd 100644 --- a/src/opt/mfs/mfsMan.c +++ b/src/opt/mfs/mfsMan.c @@ -113,7 +113,7 @@ void Mfs_ManPrint( Mfs_Man_t * p ) if ( p->pPars->fResub ) { printf( "Nodes = %d. Try = %d. Resub = %d. Div = %d. SAT calls = %d. Timeouts = %d.\n", - Abc_NtkNodeNum(p->pNtk), p->nNodesTried, p->nNodesResub, p->nTotalDivs, p->nSatCalls, p->nTimeOuts ); + p->nTotalNodesBeg, p->nNodesTried, p->nNodesResub, p->nTotalDivs, p->nSatCalls, p->nTimeOuts ); printf( "Attempts : " ); printf( "Remove %6d out of %6d (%6.2f %%) ", p->nRemoves, p->nTryRemoves, 100.0*p->nRemoves/Abc_MaxInt(1, p->nTryRemoves) ); @@ -137,7 +137,7 @@ void Mfs_ManPrint( Mfs_Man_t * p ) else { printf( "Nodes = %d. Try = %d. Total mints = %d. Local DC mints = %d. Ratio = %5.2f.\n", - Abc_NtkNodeNum(p->pNtk), p->nNodesTried, p->nMintsTotal, p->nMintsTotal-p->nMintsCare, + p->nTotalNodesBeg, p->nNodesTried, p->nMintsTotal, p->nMintsTotal-p->nMintsCare, 1.0 * (p->nMintsTotal-p->nMintsCare) / p->nMintsTotal ); // printf( "Average ratio of sequential DCs in the global space = %5.2f.\n", // 1.0-(p->dTotalRatios/p->nNodesTried) ); diff --git a/src/opt/mfs/mfsResub.c b/src/opt/mfs/mfsResub.c index 0ecd0f67..85eb8140 100644 --- a/src/opt/mfs/mfsResub.c +++ b/src/opt/mfs/mfsResub.c @@ -164,7 +164,7 @@ p->timeGia += clock() - clk; ***********************************************************************/ int Abc_NtkMfsSolveSatResub( Mfs_Man_t * p, Abc_Obj_t * pNode, int iFanin, int fOnlyRemove, int fSkipUpdate ) { - int fVeryVerbose = p->pPars->fVeryVerbose && Vec_PtrSize(p->vDivs) < 200;// || pNode->Id == 556; + int fVeryVerbose = 0;//p->pPars->fVeryVerbose && Vec_PtrSize(p->vDivs) < 200;// || pNode->Id == 556; unsigned * pData; int pCands[MFS_FANIN_MAX]; int RetValue, iVar, i, nCands, nWords, w; @@ -180,9 +180,9 @@ int Abc_NtkMfsSolveSatResub( Mfs_Man_t * p, Abc_Obj_t * pNode, int iFanin, int f if ( p->pPars->fVeryVerbose ) { // printf( "\n" ); - printf( "Node %5d : Level = %2d. Divs = %3d. Fanin = %d (out of %d). MFFC = %d\n", - pNode->Id, pNode->Level, Vec_PtrSize(p->vDivs)-Abc_ObjFaninNum(pNode), - iFanin, Abc_ObjFaninNum(pNode), + printf( "%5d : Lev =%3d. Leaf =%3d. Node =%3d. Divs =%3d. Fanin = %4d (%d/%d), MFFC = %d\n", + pNode->Id, pNode->Level, Vec_PtrSize(p->vSupp), Vec_PtrSize(p->vNodes), Vec_PtrSize(p->vDivs)-Abc_ObjFaninNum(pNode), + Abc_ObjFaninId(pNode, iFanin), iFanin, Abc_ObjFaninNum(pNode), Abc_ObjFanoutNum(Abc_ObjFanin(pNode, iFanin)) == 1 ? Abc_NodeMffcLabel(Abc_ObjFanin(pNode, iFanin)) : 0 ); } diff --git a/src/opt/sfm/sfm.h b/src/opt/sfm/sfm.h index c34ae859..31519c8e 100644 --- a/src/opt/sfm/sfm.h +++ b/src/opt/sfm/sfm.h @@ -42,18 +42,18 @@ typedef struct Sfm_Ntk_t_ Sfm_Ntk_t; typedef struct Sfm_Par_t_ Sfm_Par_t; struct Sfm_Par_t_ { - int nTfoLevMax; // the maximum fanout levels - int nFanoutMax; // the maximum number of fanouts - int nDepthMax; // the maximum depth to try - int nWinSizeMax; // the maximum window size - int nDivNumMax; // the maximum number of divisors - int nBTLimit; // the maximum number of conflicts in one SAT run - int fFixLevel; // does not allow level to increase - int fRrOnly; // perform redundance removal - int fArea; // performs optimization for area - int fMoreEffort; // performs high-affort minimization - int fVerbose; // enable basic stats - int fVeryVerbose; // enable detailed stats + int nTfoLevMax; // the maximum fanout levels + int nFanoutMax; // the maximum number of fanouts + int nDepthMax; // the maximum depth to try + int nWinSizeMax; // the maximum window size + int nDivNumMax; // the maximum number of divisors + int nBTLimit; // the maximum number of conflicts in one SAT run + int fFixLevel; // does not allow level to increase + int fRrOnly; // perform redundance removal + int fArea; // performs optimization for area + int fMoreEffort; // performs high-affort minimization + int fVerbose; // enable basic stats + int fVeryVerbose; // enable detailed stats }; //////////////////////////////////////////////////////////////////////// @@ -75,6 +75,7 @@ extern Vec_Int_t * Sfm_NodeReadFanins( 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 ); extern int Sfm_NodeReadUsed( Sfm_Ntk_t * p, int i ); +extern Vec_Int_t * Sfm_NodeReadCover( Sfm_Ntk_t * p ); /*=== sfmSat.c ==========================================================*/ diff --git a/src/opt/sfm/sfmCore.c b/src/opt/sfm/sfmCore.c index 9d96a1ac..67cbaa3a 100644 --- a/src/opt/sfm/sfmCore.c +++ b/src/opt/sfm/sfmCore.c @@ -33,7 +33,7 @@ ABC_NAMESPACE_IMPL_START /**Function************************************************************* - Synopsis [] + Synopsis [Setup parameter structure.] Description [] @@ -46,7 +46,7 @@ void Sfm_ParSetDefault( Sfm_Par_t * pPars ) { memset( pPars, 0, sizeof(Sfm_Par_t) ); pPars->nTfoLevMax = 2; // the maximum fanout levels - pPars->nFanoutMax = 10; // the maximum number of fanouts + pPars->nFanoutMax = 30; // the maximum number of fanouts pPars->nDepthMax = 20; // the maximum depth to try pPars->nWinSizeMax = 300; // the maximum window size pPars->nDivNumMax = 300; // the maximum number of divisors @@ -61,7 +61,7 @@ void Sfm_ParSetDefault( Sfm_Par_t * pPars ) /**Function************************************************************* - Synopsis [] + Synopsis [Prints statistics.] Description [] @@ -73,12 +73,12 @@ void Sfm_ParSetDefault( Sfm_Par_t * pPars ) void Sfm_NtkPrintStats( Sfm_Ntk_t * p ) { p->timeOther = p->timeTotal - p->timeWin - p->timeDiv - p->timeCnf - p->timeSat; - 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( "Nodes = %d. Try = %d. Resub = %d. Div = %d. SAT calls = %d. Timeouts = %d. MaxDivs = %d.\n", + Sfm_NtkNodeNum(p), p->nNodesTried, p->nRemoves + p->nResubs, p->nTotalDivs, p->nSatCalls, p->nTimeOuts, p->nMaxDivs ); printf( "Attempts : " ); - printf( "Remove %6d out of %6d (%6.2f %%) ", p->nRemoves, p->nTryRemoves, p->nRemoves, 100.0*p->nRemoves/Abc_MaxInt(1, p->nTryRemoves) ); - printf( "Resub %6d out of %6d (%6.2f %%) ", p->nResubs, p->nTryResubs, p->nResubs, 100.0*p->nResubs /Abc_MaxInt(1, p->nTryResubs) ); + printf( "Remove %6d out of %6d (%6.2f %%) ", p->nRemoves, p->nTryRemoves, 100.0*p->nRemoves/Abc_MaxInt(1, p->nTryRemoves) ); + printf( "Resub %6d out of %6d (%6.2f %%) ", p->nResubs, p->nTryResubs, 100.0*p->nResubs /Abc_MaxInt(1, p->nTryResubs) ); printf( "\n" ); printf( "Reduction: " ); @@ -92,6 +92,7 @@ void Sfm_NtkPrintStats( Sfm_Ntk_t * p ) ABC_PRTP( "Sat", p->timeSat , p->timeTotal ); ABC_PRTP( "Oth", p->timeOther, p->timeTotal ); ABC_PRTP( "ALL", p->timeTotal, p->timeTotal ); +// ABC_PRTP( " ", p->time1 , p->timeTotal ); } /**Function************************************************************* @@ -108,22 +109,18 @@ void Sfm_NtkPrintStats( Sfm_Ntk_t * p ) int Sfm_NodeResubSolve( Sfm_Ntk_t * p, int iNode, int f, int fRemoveOnly ) { int fSkipUpdate = 0; - int fVeryVerbose = p->pPars->fVeryVerbose && Vec_IntSize(p->vDivs) < 200;// || pNode->Id == 556; + int fVeryVerbose = 0;//p->pPars->fVeryVerbose && Vec_IntSize(p->vDivs) < 200;// || pNode->Id == 556; int i, iFanin, iVar = -1; word uTruth, uSign, uMask; clock_t clk; assert( Sfm_ObjIsNode(p, iNode) ); assert( f >= 0 && f < Sfm_ObjFaninNum(p, iNode) ); - if ( iNode == 211 ) - { - int i = 0; - } p->nTryRemoves++; // report init stats if ( p->pPars->fVeryVerbose ) - printf( "%5d : Lev =%3d. Leaf =%3d. Node =%3d. Div=%3d. Fanin = %d/%d. MFFC = %d\n", - iNode, Sfm_ObjLevel(p, iNode), Vec_IntSize(p->vLeaves), Vec_IntSize(p->vNodes), Vec_IntSize(p->vDivs), f, Sfm_ObjFaninNum(p, iNode), - Sfm_ObjFanoutNum(p, Sfm_ObjFanin(p, iNode, f)) == 1 ? Sfm_ObjMffcSize(p, iNode) : 0 ); + printf( "%5d : Lev =%3d. Leaf =%3d. Node =%3d. Div=%3d. Fanin =%4d (%d/%d). MFFC = %d\n", + iNode, Sfm_ObjLevel(p, iNode), Vec_IntSize(p->vLeaves), Vec_IntSize(p->vNodes), Vec_IntSize(p->vDivs), + Sfm_ObjFanin(p, iNode, f), f, Sfm_ObjFaninNum(p, iNode), Sfm_ObjMffcSize(p, Sfm_ObjFanin(p, iNode, f)) ); // clean simulation info p->nCexes = 0; Vec_WrdFill( p->vDivCexes, Vec_IntSize(p->vDivs), 0 ); diff --git a/src/opt/sfm/sfmInt.h b/src/opt/sfm/sfmInt.h index bdb1c600..8b0072f1 100644 --- a/src/opt/sfm/sfmInt.h +++ b/src/opt/sfm/sfmInt.h @@ -84,8 +84,7 @@ struct Sfm_Ntk_t_ 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 + sat_solver * pSat; // SAT solver int nSatVars; // the number of variables int nTryRemoves; // number of fanin removals int nTryResubs; // number of resubstitutions @@ -95,11 +94,11 @@ 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 * vOrder; // object order Vec_Int_t * vDivVars; // divisor SAT variables Vec_Int_t * vDivIds; // divisors indexes Vec_Int_t * vLits; // literals + Vec_Int_t * vValues; // SAT variable values Vec_Wec_t * vClauses; // CNF clauses for the node Vec_Int_t * vFaninMap; // mapping fanins into their SAT vars // nodes @@ -111,6 +110,7 @@ struct Sfm_Ntk_t_ int nTotalDivs; int nSatCalls; int nTimeOuts; + int nMaxDivs; // runtime clock_t timeWin; clock_t timeDiv; @@ -118,6 +118,7 @@ struct Sfm_Ntk_t_ clock_t timeSat; clock_t timeOther; clock_t timeTotal; +// clock_t time1; }; static inline int Sfm_NtkPiNum( Sfm_Ntk_t * p ) { return p->nPis; } @@ -135,8 +136,8 @@ static inline Vec_Int_t * Sfm_ObjFoArray( Sfm_Ntk_t * p, int i ) { return 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_ObjRefIncrement( Sfm_Ntk_t * p, int iObj ) { return ++Sfm_ObjFiArray(p, iObj)->nSize; } -static inline int Sfm_ObjRefDecrement( Sfm_Ntk_t * p, int iObj ) { return --Sfm_ObjFiArray(p, iObj)->nSize; } +static inline int Sfm_ObjRefIncrement( Sfm_Ntk_t * p, int iObj ) { return ++Sfm_ObjFoArray(p, iObj)->nSize; } +static inline int Sfm_ObjRefDecrement( Sfm_Ntk_t * p, int iObj ) { return --Sfm_ObjFoArray(p, iObj)->nSize; } 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); } diff --git a/src/opt/sfm/sfmNtk.c b/src/opt/sfm/sfmNtk.c index 53ec4153..3783e368 100644 --- a/src/opt/sfm/sfmNtk.c +++ b/src/opt/sfm/sfmNtk.c @@ -169,13 +169,14 @@ void Sfm_NtkPrepare( Sfm_Ntk_t * p ) p->vRoots = Vec_IntAlloc( 1000 ); p->vTfo = Vec_IntAlloc( 1000 ); p->vDivCexes = Vec_WrdStart( p->pPars->nDivNumMax ); -// p->vFans = Vec_IntAlloc( 100 ); p->vOrder = Vec_IntAlloc( 100 ); p->vDivVars = Vec_IntAlloc( 100 ); p->vDivIds = Vec_IntAlloc( 1000 ); p->vLits = Vec_IntAlloc( 100 ); + p->vValues = Vec_IntAlloc( 100 ); p->vClauses = Vec_WecAlloc( 100 ); p->vFaninMap = Vec_IntAlloc( 10 ); + p->pSat = sat_solver_new(); } void Sfm_NtkFree( Sfm_Ntk_t * p ) { @@ -200,15 +201,14 @@ void Sfm_NtkFree( Sfm_Ntk_t * p ) Vec_IntFreeP( &p->vRoots ); Vec_IntFreeP( &p->vTfo ); Vec_WrdFreeP( &p->vDivCexes ); -// Vec_IntFreeP( &p->vFans ); Vec_IntFreeP( &p->vOrder ); Vec_IntFreeP( &p->vDivVars ); Vec_IntFreeP( &p->vDivIds ); Vec_IntFreeP( &p->vLits ); + Vec_IntFreeP( &p->vValues ); Vec_WecFreeP( &p->vClauses ); Vec_IntFreeP( &p->vFaninMap ); - if ( p->pSat0 ) sat_solver_delete( p->pSat0 ); - if ( p->pSat1 ) sat_solver_delete( p->pSat1 ); + if ( p->pSat ) sat_solver_delete( p->pSat ); ABC_FREE( p ); } @@ -243,10 +243,6 @@ 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 ( iNode == 202 ) - { - int s = 0; - } if ( Sfm_ObjFanoutNum(p, iNode) > 0 || Sfm_ObjIsPi(p, iNode) ) return; assert( Sfm_ObjIsNode(p, iNode) ); @@ -272,6 +268,7 @@ void Sfm_NtkUpdateLevel_rec( Sfm_Ntk_t * p, int iNode ) void Sfm_NtkUpdate( Sfm_Ntk_t * p, int iNode, int f, int iFaninNew, word uTruth ) { int iFanin = Sfm_ObjFanin( p, iNode, f ); + assert( iFanin != iFaninNew ); // replace old fanin by new fanin assert( Sfm_ObjIsNode(p, iNode) ); Sfm_NtkRemoveFanin( p, iNode, iFanin ); @@ -312,6 +309,10 @@ int Sfm_NodeReadUsed( Sfm_Ntk_t * p, int i ) { return (Sfm_ObjFaninNum(p, i) > 0) || (Sfm_ObjFanoutNum(p, i) > 0); } +Vec_Int_t * Sfm_NodeReadCover( Sfm_Ntk_t * p ) +{ + return p->vCover; +} //////////////////////////////////////////////////////////////////////// /// END OF FILE /// diff --git a/src/opt/sfm/sfmSat.c b/src/opt/sfm/sfmSat.c index 228a5fd8..bf6a06b0 100644 --- a/src/opt/sfm/sfmSat.c +++ b/src/opt/sfm/sfmSat.c @@ -54,18 +54,18 @@ static word s_Truths6[6] = { void Sfm_NtkWindowToSolver( Sfm_Ntk_t * p ) { Vec_Int_t * vClause; - int RetValue, Lit, iNode = -1, iFanin, i, k; + int RetValue, iNode = -1, iFanin, i, k; clock_t clk = clock(); - sat_solver * pSat0 = sat_solver_new(); - sat_solver * pSat1 = sat_solver_new(); - 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 ); +// if ( p->pSat ) +// printf( "%d ", p->pSat->stats.learnts ); + sat_solver_restart( p->pSat ); + sat_solver_setnvars( p->pSat, 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_IntForEachEntry( p->vOrder, iNode, i ) Sfm_ObjSetSatVar( p, iNode, p->nSatVars++ ); - // create divisor variables + // collect divisor variables Vec_IntClear( p->vDivVars ); Vec_IntForEachEntry( p->vDivs, iNode, i ) Vec_IntPush( p->vDivVars, Sfm_ObjSatVar(p, iNode) ); @@ -86,39 +86,15 @@ void Sfm_NtkWindowToSolver( Sfm_Ntk_t * p ) { 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) ); + RetValue = sat_solver_addclause( p->pSat, Vec_IntArray(vClause), Vec_IntArray(vClause) + Vec_IntSize(vClause) ); assert( RetValue ); } } -// Sat_SolverWriteDimacs( pSat0, "test.cnf", NULL, NULL, 0 ); - // 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 - RetValue = sat_solver_simplify( pSat0 ); + RetValue = sat_solver_simplify( p->pSat ); assert( RetValue ); - RetValue = sat_solver_simplify( pSat1 ); - if ( RetValue == 0 ) - { - Sat_SolverWriteDimacs( pSat1, "test.cnf", NULL, NULL, 0 ); - } - assert( RetValue ); - // return the result - 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; -} +} /**Function************************************************************* @@ -135,55 +111,59 @@ word Sfm_ComputeInterpolant( Sfm_Ntk_t * p ) { word * pSign, uCube, uTruth = 0; 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 ); + int pLits[2], nVars = sat_solver_nvars( p->pSat ); + sat_solver_setnvars( p->pSat, nVars + 1 ); + pLits[0] = Abc_Var2Lit( Sfm_ObjSatVar(p, Vec_IntEntryLast(p->vNodes)), 0 ); // F = 1 + pLits[1] = Abc_Var2Lit( nVars, 0 ); // iNewLit while ( 1 ) { // find onset minterm p->nSatCalls++; - status = sat_solver_solve( p->pSat1, &iNewLit, &iNewLit + 1, p->pPars->nBTLimit, 0, 0, 0 ); + status = sat_solver_solve( p->pSat, pLits, pLits + 2, 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 ); + // remember variable values + Vec_IntClear( p->vValues ); + Vec_IntForEachEntry( p->vDivVars, iVar, i ) + Vec_IntPush( p->vValues, sat_solver_var_value(p->pSat, iVar) ); // collect divisor literals Vec_IntClear( p->vLits ); + Vec_IntPush( p->vLits, Abc_LitNot(pLits[0]) ); // F = 0 Vec_IntForEachEntry( p->vDivIds, Div, i ) - Vec_IntPush( p->vLits, sat_solver_var_literal(p->pSat1, Div) ); + Vec_IntPush( p->vLits, sat_solver_var_literal(p->pSat, 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 ); + status = sat_solver_solve( p->pSat, 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; if ( status == l_True ) break; assert( status == l_False ); // compute cube and add clause - nFinal = sat_solver_final( p->pSat0, &pFinal ); + nFinal = sat_solver_final( p->pSat, &pFinal ); uCube = ~(word)0; Vec_IntClear( p->vLits ); - Vec_IntPush( p->vLits, Abc_LitNot(iNewLit) ); + Vec_IntPush( p->vLits, Abc_LitNot(pLits[1]) ); // NOT(iNewLit) for ( i = 0; i < nFinal; i++ ) { + if ( pFinal[i] == pLits[0] ) + continue; Vec_IntPush( p->vLits, pFinal[i] ); iVar = Vec_IntFind( p->vDivIds, Abc_Lit2Var(pFinal[i]) ); assert( iVar >= 0 ); uCube &= Abc_LitIsCompl(pFinal[i]) ? s_Truths6[iVar] : ~s_Truths6[iVar]; } uTruth |= uCube; - status = sat_solver_addclause( p->pSat1, Vec_IntArray(p->vLits), Vec_IntArray(p->vLits) + Vec_IntSize(p->vLits) ); + status = sat_solver_addclause( p->pSat, 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 ) - if ( sat_solver_var_value(p->pSat1, iVar) ^ sat_solver_var_value(p->pSat0, iVar) ) // insert 1 + if ( Vec_IntEntry(p->vValues, i) ^ sat_solver_var_value(p->pSat, iVar) ) // insert 1 { pSign = Vec_WrdEntryP( p->vDivCexes, i ); assert( !Abc_InfoHasBit( (unsigned *)pSign, p->nCexes) ); @@ -207,8 +187,8 @@ word Sfm_ComputeInterpolant( Sfm_Ntk_t * p ) void Sfm_ComputeInterpolantCheck( Sfm_Ntk_t * p ) { int iNode = 3; - int iDiv0 = 5; - int iDiv1 = 4; + int iDiv0 = 6; + int iDiv1 = 7; word uTruth; // int i; // Sfm_NtkForEachNode( p, i ) diff --git a/src/opt/sfm/sfmWin.c b/src/opt/sfm/sfmWin.c index f96221c0..1d2919f9 100644 --- a/src/opt/sfm/sfmWin.c +++ b/src/opt/sfm/sfmWin.c @@ -89,6 +89,10 @@ int Sfm_ObjDeref( Sfm_Ntk_t * p, int iObj ) int Sfm_ObjMffcSize( Sfm_Ntk_t * p, int iObj ) { int Count1, Count2; + if ( Sfm_ObjIsPi(p, iObj) ) + return 0; + if ( Sfm_ObjFanoutNum(p, iObj) != 1 ) + return 0; assert( Sfm_ObjIsNode( p, iObj ) ); Count1 = Sfm_ObjDeref( p, iObj ); Count2 = Sfm_ObjRef( p, iObj ); @@ -182,10 +186,11 @@ int Sfm_NtkCheckFanouts( Sfm_Ntk_t * p, int iNode ) void Sfm_NtkAddDivisors( Sfm_Ntk_t * p, int iNode, int nLevelMax ) { int i, iFanout; - if ( Sfm_ObjFanoutNum(p, iNode) > p->pPars->nFanoutMax ) - return; Sfm_ObjForEachFanout( p, iNode, iFanout, i ) { + // skip some of the fanouts if the number is large + if ( p->pPars->nFanoutMax && i > p->pPars->nFanoutMax ) + break; // skip TFI nodes, PO nodes, or nodes with high logic level if ( Sfm_ObjIsTravIdCurrent(p, iFanout) || Sfm_ObjIsPo(p, iFanout) || (p->pPars->fFixLevel && Sfm_ObjLevel(p, iFanout) >= nLevelMax) ) @@ -252,7 +257,8 @@ int Sfm_NtkCreateWindow( Sfm_Ntk_t * p, int iNode, int fVerbose ) return 0; } // collect TFO (currently use only one level of TFO) - if ( Sfm_NtkCheckFanouts(p, iNode) ) +// if ( Sfm_NtkCheckFanouts(p, iNode) ) + if ( 0 ) { Sfm_ObjForEachFanout( p, iNode, iTemp, i ) { @@ -268,10 +274,10 @@ int Sfm_NtkCreateWindow( Sfm_Ntk_t * p, int iNode, int fVerbose ) clk = clock(); // create ordering of the nodes Vec_IntClear( p->vOrder ); - Vec_IntForEachEntryReverse( p->vNodes, iNode, i ) - Vec_IntPush( p->vOrder, iNode ); - Vec_IntForEachEntry( p->vLeaves, iNode, i ) - Vec_IntPush( p->vOrder, iNode ); + Vec_IntForEachEntryReverse( p->vNodes, iTemp, i ) + Vec_IntPush( p->vOrder, iTemp ); + Vec_IntForEachEntry( p->vLeaves, iTemp, i ) + Vec_IntPush( p->vOrder, iTemp ); // mark fanins Sfm_NtkIncrementTravId2( p ); Sfm_ObjSetTravIdCurrent2( p, iNode ); @@ -294,11 +300,17 @@ int Sfm_NtkCreateWindow( Sfm_Ntk_t * p, int iNode, int fVerbose ) Vec_IntShrink( p->vDivs, k ); assert( Vec_IntSize(p->vDivs) == p->pPars->nDivNumMax ); } +//Vec_IntPrint( p->vLeaves ); +//Vec_IntPrint( p->vNodes ); +//Vec_IntPrint( p->vDivs ); // collect additional divisors of the TFI nodes if ( Vec_IntSize(p->vDivs) < p->pPars->nDivNumMax ) { int nStartNew = Vec_IntSize(p->vDivs); Sfm_NtkIncrementTravId2( p ); + Sfm_ObjForEachFanin( p, iNode, iTemp, i ) + if ( Vec_IntSize(p->vDivs) < p->pPars->nDivNumMax ) + Sfm_NtkAddDivisors( p, iTemp, Sfm_ObjLevel(p, iNode) ); Vec_IntForEachEntry( p->vDivs, iTemp, i ) if ( Vec_IntSize(p->vDivs) < p->pPars->nDivNumMax ) Sfm_NtkAddDivisors( p, iTemp, Sfm_ObjLevel(p, iNode) ); @@ -309,6 +321,7 @@ int Sfm_NtkCreateWindow( Sfm_Ntk_t * p, int iNode, int fVerbose ) Vec_IntPush( p->vOrder, iTemp ); } assert( Vec_IntSize(p->vDivs) <= p->pPars->nDivNumMax ); + p->nMaxDivs += (Vec_IntSize(p->vDivs) == p->pPars->nDivNumMax); // statistics p->nTotalDivs += Vec_IntSize(p->vDivs); p->timeDiv += clock() - clk; -- cgit v1.2.3