From ff6f0943362c30176fd1f961bcbd19e188cee520 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Fri, 14 Mar 2008 08:01:00 -0700 Subject: Version abc80314 --- src/opt/mfs/mfsInt.h | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) (limited to 'src/opt/mfs/mfsInt.h') 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 -- cgit v1.2.3