diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2008-03-14 08:01:00 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2008-03-14 08:01:00 -0700 |
| commit | ff6f0943362c30176fd1f961bcbd19e188cee520 (patch) | |
| tree | fc2b888c8403ee04fb7d473433c1eb3bcc5ef8c5 /src/opt/mfs/mfsInt.h | |
| parent | 6205eaaee3a840dd076f9baaac67720d85d6a680 (diff) | |
| download | abc-ff6f0943362c30176fd1f961bcbd19e188cee520.tar.gz abc-ff6f0943362c30176fd1f961bcbd19e188cee520.tar.bz2 abc-ff6f0943362c30176fd1f961bcbd19e188cee520.zip | |
Version abc80314
Diffstat (limited to 'src/opt/mfs/mfsInt.h')
| -rw-r--r-- | src/opt/mfs/mfsInt.h | 8 |
1 files changed, 7 insertions, 1 deletions
diff --git a/src/opt/mfs/mfsInt.h b/src/opt/mfs/mfsInt.h index 91395d03..f4da45ef 100644 --- a/src/opt/mfs/mfsInt.h +++ b/src/opt/mfs/mfsInt.h @@ -35,12 +35,13 @@ extern "C" { #include "cnf.h" #include "satSolver.h" #include "satStore.h" +#include "bdc.h" //////////////////////////////////////////////////////////////////////// /// PARAMETERS /// //////////////////////////////////////////////////////////////////////// -#define MFS_FANIN_MAX 10 +#define MFS_FANIN_MAX 12 typedef struct Mfs_Man_t_ Mfs_Man_t; struct Mfs_Man_t_ @@ -64,6 +65,11 @@ struct Mfs_Man_t_ int nCexes; // the numbe rof current counter-examples int nSatCalls; int nSatCexes; + // used for bidecomposition + Vec_Int_t * vTruth; + Bdc_Man_t * pManDec; + int nNodesDec; + int nNodesGained; // solving data Aig_Man_t * pAigWin; // window AIG with constraints Cnf_Dat_t * pCnf; // the CNF for the window |