diff options
Diffstat (limited to 'src/opt')
-rw-r--r-- | src/opt/mfs/mfsCore.c | 4 | ||||
-rw-r--r-- | src/opt/mfs/mfsInt.h | 12 | ||||
-rw-r--r-- | src/opt/mfs/mfsMan.c | 5 | ||||
-rw-r--r-- | src/opt/mfs/mfsResub.c | 8 | ||||
-rw-r--r-- | src/opt/mfs/module.make | 1 |
5 files changed, 28 insertions, 2 deletions
diff --git a/src/opt/mfs/mfsCore.c b/src/opt/mfs/mfsCore.c index 20d3799c..78d45b14 100644 --- a/src/opt/mfs/mfsCore.c +++ b/src/opt/mfs/mfsCore.c @@ -265,6 +265,9 @@ clk = clock(); p->nNodesBad++; return 1; } +clk = clock(); + Abc_NtkMfsConstructGia( p ); +p->timeGia += clock() - clk; // solve the SAT problem if ( p->pPars->fPower ) Abc_NtkMfsEdgePower( p, pNode ); @@ -277,6 +280,7 @@ clk = clock(); Abc_NtkMfsResubNode2( p, pNode ); } p->timeSat += clock() - clk; + Abc_NtkMfsDeconstructGia( p ); return 1; } diff --git a/src/opt/mfs/mfsInt.h b/src/opt/mfs/mfsInt.h index 13f0bce2..6a1d9688 100644 --- a/src/opt/mfs/mfsInt.h +++ b/src/opt/mfs/mfsInt.h @@ -32,6 +32,7 @@ #include "satSolver.h" #include "satStore.h" #include "bdc.h" +#include "gia.h" //////////////////////////////////////////////////////////////////////// /// PARAMETERS /// @@ -65,6 +66,12 @@ struct Mfs_Man_t_ int nCexes; // the numbe rof current counter-examples int nSatCalls; int nSatCexes; + // intermediate AIG data + Gia_Man_t * pGia; // replica of the AIG in the new package + Gia_Obj_t ** pSat2Gia; // mapping of PO SAT var into internal GIA nodes + Tas_Man_t * pTas; // the SAT solver + Vec_Int_t * vCex; // the counter-example + Vec_Ptr_t * vGiaLits; // literals given as assumptions // used for bidecomposition Vec_Int_t * vTruth; Bdc_Man_t * pManDec; @@ -110,6 +117,7 @@ struct Mfs_Man_t_ int timeWin; int timeDiv; int timeAig; + int timeGia; int timeCnf; int timeSat; int timeInt; @@ -155,6 +163,10 @@ extern double Abc_NtkConstraintRatio( Mfs_Man_t * p, Abc_Obj_t * pNode /*=== mfsWin.c ==========================================================*/ extern Vec_Ptr_t * Abc_MfsComputeRoots( Abc_Obj_t * pNode, int nWinTfoMax, int nFanoutLimit ); +/*=== mfsGia.c ==========================================================*/ +extern void Abc_NtkMfsConstructGia( Mfs_Man_t * p ); +extern void Abc_NtkMfsDeconstructGia( Mfs_Man_t * p ); +extern int Abc_NtkMfsTryResubOnceGia( Mfs_Man_t * p, int * pCands, int nCands ); #ifdef __cplusplus } diff --git a/src/opt/mfs/mfsMan.c b/src/opt/mfs/mfsMan.c index e947bd52..71595f6c 100644 --- a/src/opt/mfs/mfsMan.c +++ b/src/opt/mfs/mfsMan.c @@ -157,15 +157,16 @@ void Mfs_ManPrint( Mfs_Man_t * p ) printf( "Nodes resyn = %d. Ratio = %5.2f. Total AIG node gain = %d. Timeouts = %d.\n", p->nNodesDec, 1.0 * p->nNodesDec / p->nNodesTried, p->nNodesGained, p->nTimeOuts ); } -/* + ABC_PRTP( "Win", p->timeWin , p->timeTotal ); ABC_PRTP( "Div", p->timeDiv , p->timeTotal ); ABC_PRTP( "Aig", p->timeAig , p->timeTotal ); + ABC_PRTP( "Gia", p->timeGia , p->timeTotal ); ABC_PRTP( "Cnf", p->timeCnf , p->timeTotal ); ABC_PRTP( "Sat", p->timeSat-p->timeInt , p->timeTotal ); ABC_PRTP( "Int", p->timeInt , p->timeTotal ); ABC_PRTP( "ALL", p->timeTotal , p->timeTotal ); -*/ + } /**Function************************************************************* diff --git a/src/opt/mfs/mfsResub.c b/src/opt/mfs/mfsResub.c index 008b6863..8cd70dbf 100644 --- a/src/opt/mfs/mfsResub.c +++ b/src/opt/mfs/mfsResub.c @@ -99,9 +99,17 @@ int Abc_NtkMfsTryResubOnce( Mfs_Man_t * p, int * pCands, int nCands ) { unsigned * pData; int RetValue, iVar, i; + int clk = clock(), RetValue2 = Abc_NtkMfsTryResubOnceGia( p, pCands, nCands ); +p->timeGia += clock() - clk; + p->nSatCalls++; RetValue = sat_solver_solve( p->pSat, pCands, pCands + nCands, (ABC_INT64_T)p->pPars->nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 ); // assert( RetValue == l_False || RetValue == l_True ); + if ( RetValue != l_Undef && RetValue2 != -1 ) + { + assert( (RetValue == l_False) == (RetValue2 == 1) ); + } + if ( RetValue == l_False ) return 1; if ( RetValue != l_True ) diff --git a/src/opt/mfs/module.make b/src/opt/mfs/module.make index 544accec..bafc1ce5 100644 --- a/src/opt/mfs/module.make +++ b/src/opt/mfs/module.make @@ -1,5 +1,6 @@ SRC += src/opt/mfs/mfsCore.c \ src/opt/mfs/mfsDiv.c \ + src/opt/mfs/mfsGia.c \ src/opt/mfs/mfsInter.c \ src/opt/mfs/mfsMan.c \ src/opt/mfs/mfsResub.c \ |