diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2015-06-22 23:04:59 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2015-06-22 23:04:59 -0700 |
| commit | da65e88e3b346bcd70198b980e918ea9f1e11b4e (patch) | |
| tree | ce660cd8d798ddd41787322db32e6ae21b2ceb11 /src/opt/mfs/mfsInt.h | |
| parent | 270f6db24625e4838dcafe7d45e69cc9522d703e (diff) | |
| download | abc-da65e88e3b346bcd70198b980e918ea9f1e11b4e.tar.gz abc-da65e88e3b346bcd70198b980e918ea9f1e11b4e.tar.bz2 abc-da65e88e3b346bcd70198b980e918ea9f1e11b4e.zip | |
Version abc90804
committer: Baruch Sterin <baruchs@gmail.com>
Diffstat (limited to 'src/opt/mfs/mfsInt.h')
| -rw-r--r-- | src/opt/mfs/mfsInt.h | 12 |
1 files changed, 12 insertions, 0 deletions
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 } |