summaryrefslogtreecommitdiffstats
path: root/src/sat/bmc/bmc.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/sat/bmc/bmc.h')
-rw-r--r--src/sat/bmc/bmc.h14
1 files changed, 14 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 ///