diff options
| author | Baruch Sterin <baruchs@gmail.com> | 2011-01-13 22:42:54 +0200 |
|---|---|---|
| committer | Baruch Sterin <baruchs@gmail.com> | 2011-01-13 22:42:54 +0200 |
| commit | ab80b015a4efdf196334aafc19d589d48778f0bb (patch) | |
| tree | 0a4af678193d4d84de98d0ecb0e141c17fa8ae87 /src/opt/mfs/mfsInt.h | |
| parent | 811f5631a812968ccdbe157549f2445747053d50 (diff) | |
| parent | ae4b51351c93983a1285ce1028e3bbd90a6d5721 (diff) | |
| download | abc-ab80b015a4efdf196334aafc19d589d48778f0bb.tar.gz abc-ab80b015a4efdf196334aafc19d589d48778f0bb.tar.bz2 abc-ab80b015a4efdf196334aafc19d589d48778f0bb.zip | |
merge changes from main branch
Diffstat (limited to 'src/opt/mfs/mfsInt.h')
| -rw-r--r-- | src/opt/mfs/mfsInt.h | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/src/opt/mfs/mfsInt.h b/src/opt/mfs/mfsInt.h index 5611afa0..28a68bd8 100644 --- a/src/opt/mfs/mfsInt.h +++ b/src/opt/mfs/mfsInt.h @@ -61,19 +61,22 @@ struct Mfs_Man_t_ Vec_Ptr_t * vNodes; // the internal nodes of the window Vec_Ptr_t * vDivs; // the divisors of the node Vec_Int_t * vDivLits; // the SAT literals of divisor nodes - Vec_Int_t * vProjVars; // the projection variables + Vec_Int_t * vProjVarsCnf; // the projection variables + Vec_Int_t * vProjVarsSat; // the projection variables // intermediate simulation data Vec_Ptr_t * vDivCexes; // the counter-example for dividors int nDivWords; // the number of words 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; @@ -87,7 +90,7 @@ struct Mfs_Man_t_ Int_Man_t * pMan; // interpolation manager; Vec_Int_t * vMem; // memory for intermediate SOPs Vec_Vec_t * vLevels; // levelized structure for updating - Vec_Ptr_t * vFanins; // the new set of fanins + Vec_Ptr_t * vMfsFanins; // the new set of fanins int nTotConfLim; // total conflict limit int nTotConfLevel; // total conflicts on this level // switching activity |