Defines |
#define | BMC_DIMACS_FILENAME "bmc_dimacs_filename" |
#define | BMC_FORCE_PLTL_TABLEAU "bmc_force_pltl_tableau" |
#define | BMC_HAS_TO_SOLVE true |
#define | BMC_INC_INVAR_ALG_DUAL "dual" |
#define | BMC_INC_INVAR_ALG_FALSIFICATION "falsification" |
#define | BMC_INC_INVAR_ALG_INTERP_SEQ "interp_seq" |
#define | BMC_INC_INVAR_ALG_INTERPOLANTS "interpolants" |
#define | BMC_INC_INVAR_ALG_ZIGZAG "zigzag" |
#define | BMC_INVAR_ALG "bmc_invar_alg" |
#define | BMC_INVAR_ALG_CLASSIC "classic" |
| The names for INVAR solving algorithms (incremental and non-incremental).
|
#define | BMC_INVAR_ALG_EEN_SORENSSON "een-sorensson" |
#define | BMC_INVAR_ALG_FALSIFICATION "falsification" |
#define | BMC_INVAR_BACKWARD "backward" |
| The names for INVAR closure strategies.
|
#define | BMC_INVAR_DIMACS_FILENAME "bmc_invar_dimacs_filename" |
#define | BMC_INVAR_FORWARD "forward" |
#define | BMC_MODE "bmc_mode" |
#define | BMC_OPT_INITIALIZED "__bmc_opt_initialized__" |
| The header file for the bmc package.
|
#define | BMC_OPTIMIZED_TABLEAU "bmc_optimized_tableau" |
#define | BMC_PB_LENGTH "bmc_length" |
#define | BMC_PB_LOOP "bmc_loopback" |
#define | BMC_SBMC_CACHE_OPT "bmc_sbmc_cache_opt" |
#define | BMC_SBMC_GF_FG_OPT "bmc_sbmc_gf_fg_opt" |
#define | BMC_SBMC_IL_OPT "bmc_sbmc_il_opt" |
#define | BMC_WATCHDOG_NAME "bmc_watchdog" |
| Name of the watchdog timer used in the bmc algorithm.
|
Enumerations |
enum | bmc_invar_algorithm {
ALG_UNDEFINED,
ALG_CLASSIC,
ALG_EEN_SORENSSON,
ALG_FALSIFICATION,
ALG_DUAL,
ALG_ZIGZAG,
ALG_INTERP_SEQ,
ALG_INTERPOLANTS
} |
| BMC invariant checking algorithms.
More...
|
Functions |
char * | get_bmc_dimacs_filename (OptsHandler_ptr) |
const char * | get_bmc_invar_alg (OptsHandler_ptr) |
char * | get_bmc_invar_dimacs_filename (OptsHandler_ptr) |
int | get_bmc_pb_length (OptsHandler_ptr) |
const char * | get_bmc_pb_loop (OptsHandler_ptr) |
boolean | opt_bmc_force_pltl_tableau (OptsHandler_ptr) |
boolean | opt_bmc_mode (OptsHandler_ptr) |
boolean | opt_bmc_optimized_tableau (OptsHandler_ptr) |
boolean | opt_bmc_sbmc_cache (OptsHandler_ptr opt) |
boolean | opt_bmc_sbmc_gf_fg_opt (OptsHandler_ptr opt) |
boolean | opt_bmc_sbmc_il_opt (OptsHandler_ptr opt) |
void | set_bmc_dimacs_filename (OptsHandler_ptr, char *) |
void | set_bmc_force_pltl_tableau (OptsHandler_ptr) |
void | set_bmc_invar_alg (OptsHandler_ptr opt, const char *loop) |
void | set_bmc_invar_dimacs_filename (OptsHandler_ptr, char *) |
void | set_bmc_mode (OptsHandler_ptr) |
void | set_bmc_optimized_tableau (OptsHandler_ptr) |
void | set_bmc_pb_length (OptsHandler_ptr opt, const int k) |
void | set_bmc_pb_loop (OptsHandler_ptr opt, const char *loop) |
void | set_bmc_sbmc_cache (OptsHandler_ptr opt) |
void | set_bmc_sbmc_gf_fg_opt (OptsHandler_ptr opt) |
void | set_bmc_sbmc_il_opt (OptsHandler_ptr opt) |
void | unset_bmc_force_pltl_tableau (OptsHandler_ptr) |
void | unset_bmc_mode (OptsHandler_ptr) |
void | unset_bmc_optimized_tableau (OptsHandler_ptr) |
void | unset_bmc_sbmc_cache (OptsHandler_ptr opt) |
void | unset_bmc_sbmc_gf_fg_opt (OptsHandler_ptr opt) |
void | unset_bmc_sbmc_il_opt (OptsHandler_ptr opt) |