NuSMV/code/nusmv/core/bmc/bmc.h File Reference

#include "nusmv/core/bmc/bmcBmc.h"
#include "nusmv/core/bmc/bmcPkg.h"
#include "nusmv/core/bmc/bmcGen.h"
#include "nusmv/core/bmc/bmcDump.h"
#include "nusmv/core/bmc/bmcTableau.h"
#include "nusmv/core/bmc/bmcModel.h"
#include "nusmv/core/bmc/bmcConv.h"
#include "nusmv/core/bmc/bmcCheck.h"
#include "nusmv/core/bmc/bmcUtils.h"

Go to the source code of this file.

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)

---

Define Documentation

#define BMC_DIMACS_FILENAME   "bmc_dimacs_filename"

Todo:

Missing synopsis

Todo:

Missing description

#define BMC_FORCE_PLTL_TABLEAU   "bmc_force_pltl_tableau"

Todo:

Missing synopsis

Todo:

Missing description

#define BMC_HAS_TO_SOLVE   true

Todo:

Missing synopsis

Todo:

Missing description

#define BMC_INC_INVAR_ALG_DUAL   "dual"

Todo:

Missing synopsis

Todo:

Missing description

#define BMC_INC_INVAR_ALG_FALSIFICATION   "falsification"

Todo:

Missing synopsis

Todo:

Missing description

#define BMC_INC_INVAR_ALG_INTERP_SEQ   "interp_seq"

Todo:

Missing synopsis

Todo:

Missing description

#define BMC_INC_INVAR_ALG_INTERPOLANTS   "interpolants"

Todo:

Missing synopsis

Todo:

Missing description

#define BMC_INC_INVAR_ALG_ZIGZAG   "zigzag"

Todo:

Missing synopsis

Todo:

Missing description

#define BMC_INVAR_ALG   "bmc_invar_alg"

Todo:

Missing synopsis

Todo:

Missing description

#define BMC_INVAR_ALG_CLASSIC   "classic"

The names for INVAR solving algorithms (incremental and non-incremental).

#define BMC_INVAR_ALG_EEN_SORENSSON   "een-sorensson"

Todo:

Missing synopsis

Todo:

Missing description

#define BMC_INVAR_ALG_FALSIFICATION   "falsification"

Todo:

Missing synopsis

Todo:

Missing description

#define BMC_INVAR_BACKWARD   "backward"

The names for INVAR closure strategies.

Currently this applies to DUAL algorithm only

#define BMC_INVAR_DIMACS_FILENAME   "bmc_invar_dimacs_filename"

Todo:

Missing synopsis

Todo:

Missing description

#define BMC_INVAR_FORWARD   "forward"

Todo:

Missing synopsis

Todo:

Missing description

#define BMC_MODE   "bmc_mode"

Todo:

Missing synopsis

Todo:

Missing description

#define BMC_OPT_INITIALIZED   "__bmc_opt_initialized__"

The header file for the bmc package.

Author:

Roberto Cavada

Todo:

: Missing description

Todo:

Missing synopsis

Todo:

Missing description

#define BMC_OPTIMIZED_TABLEAU   "bmc_optimized_tableau"

Todo:

Missing synopsis

Todo:

Missing description

#define BMC_PB_LENGTH   "bmc_length"

Todo:

Missing synopsis

Todo:

Missing description

#define BMC_PB_LOOP   "bmc_loopback"

Todo:

Missing synopsis

Todo:

Missing description

#define BMC_SBMC_CACHE_OPT   "bmc_sbmc_cache_opt"

Todo:

Missing synopsis

Todo:

Missing description

#define BMC_SBMC_GF_FG_OPT   "bmc_sbmc_gf_fg_opt"

Todo:

Missing synopsis

Todo:

Missing description

#define BMC_SBMC_IL_OPT   "bmc_sbmc_il_opt"

Todo:

Missing synopsis

Todo:

Missing description

#define BMC_WATCHDOG_NAME   "bmc_watchdog"

Name of the watchdog timer used in the bmc algorithm.

Name of the watchdog timer used in the bmc algorithm

---

Enumeration Type Documentation

enum bmc_invar_algorithm

BMC invariant checking algorithms.

optional

See also:

optional

Enumerator:

ALG_UNDEFINED
ALG_CLASSIC
ALG_EEN_SORENSSON
ALG_FALSIFICATION
ALG_DUAL
ALG_ZIGZAG
ALG_INTERP_SEQ
ALG_INTERPOLANTS

---

Function Documentation

char* get_bmc_dimacs_filename

(

OptsHandler_ptr

)

Todo:

Missing synopsis

Todo:

Missing description

const char* get_bmc_invar_alg

(

OptsHandler_ptr

)

Todo:

Missing synopsis

Todo:

Missing description

char* get_bmc_invar_dimacs_filename

(

OptsHandler_ptr

)

Todo:

Missing synopsis

Todo:

Missing description

int get_bmc_pb_length

(

OptsHandler_ptr

)

Todo:

Missing synopsis

Todo:

Missing description

const char* get_bmc_pb_loop

(

OptsHandler_ptr

)

Todo:

Missing synopsis

Todo:

Missing description

boolean opt_bmc_force_pltl_tableau

(

OptsHandler_ptr

)

Todo:

Missing synopsis

Todo:

Missing description

boolean opt_bmc_mode

(

OptsHandler_ptr

)

Todo:

Missing synopsis

Todo:

Missing description

boolean opt_bmc_optimized_tableau

(

OptsHandler_ptr

)

Todo:

Missing synopsis

Todo:

Missing description

boolean opt_bmc_sbmc_cache

(

OptsHandler_ptr

opt

)

Todo:

Missing synopsis

Todo:

Missing description

boolean opt_bmc_sbmc_gf_fg_opt

(

OptsHandler_ptr

opt

)

Todo:

Missing synopsis

Todo:

Missing description

boolean opt_bmc_sbmc_il_opt

(

OptsHandler_ptr

opt

)

Todo:

Missing synopsis

Todo:

Missing description

void set_bmc_dimacs_filename	(	OptsHandler_ptr	,
		char *
	)

Todo:

Missing synopsis

Todo:

Missing description

void set_bmc_force_pltl_tableau

(

OptsHandler_ptr

)

Todo:

Missing synopsis

Todo:

Missing description

void set_bmc_invar_alg	(	OptsHandler_ptr	opt,
		const char *	loop
	)

Todo:

Missing synopsis

Todo:

Missing description

void set_bmc_invar_dimacs_filename	(	OptsHandler_ptr	,
		char *
	)

Todo:

Missing synopsis

Todo:

Missing description

void set_bmc_mode

(

OptsHandler_ptr

)

AutomaticStart

Todo:

Missing synopsis

Todo:

Missing description

void set_bmc_optimized_tableau

(

OptsHandler_ptr

)

Todo:

Missing synopsis

Todo:

Missing description

void set_bmc_pb_length	(	OptsHandler_ptr	opt,
		const int	k
	)

Todo:

Missing synopsis

Todo:

Missing description

void set_bmc_pb_loop	(	OptsHandler_ptr	opt,
		const char *	loop
	)

Todo:

Missing synopsis

Todo:

Missing description

void set_bmc_sbmc_cache

(

OptsHandler_ptr

opt

)

Todo:

Missing synopsis

Todo:

Missing description

void set_bmc_sbmc_gf_fg_opt

(

OptsHandler_ptr

opt

)

Todo:

Missing synopsis

Todo:

Missing description

void set_bmc_sbmc_il_opt

(

OptsHandler_ptr

opt

)

Todo:

Missing synopsis

Todo:

Missing description

void unset_bmc_force_pltl_tableau

(

OptsHandler_ptr

)

Todo:

Missing synopsis

Todo:

Missing description

void unset_bmc_mode

(

OptsHandler_ptr

)

Todo:

Missing synopsis

Todo:

Missing description

void unset_bmc_optimized_tableau

(

OptsHandler_ptr

)

Todo:

Missing synopsis

Todo:

Missing description

void unset_bmc_sbmc_cache

(

OptsHandler_ptr

opt

)

Todo:

Missing synopsis

Todo:

Missing description

void unset_bmc_sbmc_gf_fg_opt

(

OptsHandler_ptr

opt

)

Todo:

Missing synopsis

Todo:

Missing description

void unset_bmc_sbmc_il_opt

(

OptsHandler_ptr

opt

)

Todo:

Missing synopsis

Todo:

Missing description