summaryrefslogtreecommitdiffstats
path: root/src/sat/bmc
diff options
context:
space:
mode:
Diffstat (limited to 'src/sat/bmc')
-rw-r--r--src/sat/bmc/bmc.h14
-rw-r--r--src/sat/bmc/module.make1
2 files changed, 15 insertions, 0 deletions
diff --git a/src/sat/bmc/bmc.h b/src/sat/bmc/bmc.h
index 6e1fd62a..f1407936 100644
--- a/src/sat/bmc/bmc.h
+++ b/src/sat/bmc/bmc.h
@@ -68,6 +68,20 @@ struct Saig_ParBmc_t_
int(*pFuncOnFail)(int,Abc_Cex_t*); // called for a failed output in MO mode
};
+
+typedef struct Bmc_LadPar_t_ Bmc_LadPar_t;
+struct Bmc_LadPar_t_
+{
+ int nStart; // starting timeframe
+ int nFramesMax; // maximum number of timeframes
+ int nConfLimit; // maximum number of conflicts at a node
+ int fLoadCnf; // dynamic CNF loading
+ int fVerbose; // verbose
+ int fNotVerbose; // skip line-by-line print-out
+ int iFrame; // explored up to this frame
+ int nFailOuts; // the number of failed outputs
+ int nDropOuts; // the number of dropped outputs
+};
////////////////////////////////////////////////////////////////////////
/// MACRO DEFINITIONS ///
diff --git a/src/sat/bmc/module.make b/src/sat/bmc/module.make
index 1ac04203..cde439b4 100644
--- a/src/sat/bmc/module.make
+++ b/src/sat/bmc/module.make
@@ -6,4 +6,5 @@ SRC += src/sat/bmc/bmcBmc.c \
src/sat/bmc/bmcCexMin1.c \
src/sat/bmc/bmcCexMin2.c \
src/sat/bmc/bmcCexTools.c \
+ src/sat/bmc/bmcLoad.c \
src/sat/bmc/bmcUnroll.c