Defines |
#define | A_SAT_SOLVER "sat_solver" |
#define | AFFINITY_CLUSTERING "affinity" |
#define | AG_ONLY_SEARCH "ag_only_search" |
#define | APPEND_CLUSTERS "append_clusters" |
#define | APPEND_CLUSTERS_VISIBLE 0 |
#define | BACKWARD_COMPATIBILITY "backward_compatibility" |
#define | BATCH "batch" |
#define | BDD_ENCODE_WORD_BITS "bdd_encode_word_bits" |
#define | BDD_STATIC_ORDER_HEURISTICS "bdd_static_order_heuristics" |
#define | BOOLEAN_CONVERSION_USES_PREDICATE_NORMALIZATION "boolean_conversion_uses_predicate_normalization" |
#define | CHECK_INVAR_BDDBMC_HEURISTIC "check_invar_bddbmc_heuristic" |
#define | CHECK_INVAR_BDDBMC_HEURISTIC_THRESHOLD "check_invar_bddbmc_threshold" |
#define | CHECK_INVAR_FB_HEURISTIC "check_invar_forward_backward_heuristic" |
#define | CONE_OF_INFLUENCE "cone_of_influence" |
#define | CONJ_PART_THRESHOLD "conj_part_threshold" |
#define | COUNTER_EXAMPLES "counter_examples" |
#define | DAGGIFIER_COUNTER_THRESHOLD "daggifier_counter_threshold" |
#define | DAGGIFIER_DEPTH_THRESHOLD "daggifier_depth_threshold" |
#define | DAGGIFIER_ENABLED "daggifier_enabled" |
#define | DAGGIFIER_STATISTICS "daggifier_statistics" |
#define | DEFAULT_BACKWARD_COMPATIBILITY false |
#define | DEFAULT_BDD2BMC_HEURISTIC STEPS_HEURISTIC |
#define | DEFAULT_BDD2BMC_HEURISTIC_THRESHOLD 10 |
#define | DEFAULT_BDD_ENCODE_WORD_BITS true |
#define | DEFAULT_BOOLEAN_CONVERSION_USES_PREDICATE_NORMALIZATION false |
#define | DEFAULT_CONJ_PART_THRESHOLD 1000 |
#define | DEFAULT_DAGGIFIER_COUNTER_THS 3 |
#define | DEFAULT_DAGGIFIER_DEPTH_THS 2 |
#define | DEFAULT_DAGGIFIER_ENABLED true |
#define | DEFAULT_FORWARD_BACKWARD_ANALYSIS_HEURISTIC ZIGZAG_HEURISTIC |
#define | DEFAULT_IMAGE_CLUSTER_SIZE 1000 |
#define | DEFAULT_INPUT_FILE (char *)NULL |
#define | DEFAULT_INPUT_ORDER_FILE (char *)NULL |
#define | DEFAULT_INVAR_CHECK_STRATEGY FORWARD |
#define | DEFAULT_LTL2SMV_SINGLE_JUSTICE false |
#define | DEFAULT_OREG_JUSTICE_EMPTINESS_BDD_ALGORITHM BDD_OREG_JUSTICE_EMPTINESS_BDD_ALGORITHM_EL_BWD |
#define | DEFAULT_OUTPUT_ORDER_FILE "temp.ord" |
#define | DEFAULT_PGM_NAME NUSMV_PACKAGE_NAME |
| The option header file.
|
#define | DEFAULT_PGM_PATH (char *)NULL |
#define | DEFAULT_PP_CPP_PATH (char *)NULL |
#define | DEFAULT_PP_M4_PATH (char *)NULL |
#define | DEFAULT_SAT_SOLVER (char*)NULL |
#define | DEFAULT_SHOW_DEFINES_IN_TRACES true |
#define | DEFAULT_SHOW_DEFINES_WITH_NEXT true |
#define | DEFAULT_SHOWN_STATES 25 |
#define | DEFAULT_SIMULATION_STEPS "default_simulation_steps" |
#define | DEFAULT_TRACE_PLUGIN "default_trace_plugin" |
#define | DEFAULT_TRACES_HIDING_PREFIX "__" |
#define | DEFAULT_TRANS_ORDER_FILE (char *)NULL |
#define | DEFAULT_TYPE_CHECKING_WARNING_ON true |
#define | DEFAULT_USE_COI_SIZE_SORTING true |
#define | DISABLE_SYNTACTIC_CHECKS "disable_syntactic_checks" |
#define | DYNAMIC_REORDER "dynamic_reorder" |
#define | ENABLE_REORDER "enable_reorder" |
#define | ENABLE_SEXP2BDD_CACHING "enable_sexp2bdd_caching" |
#define | FORWARD_SEARCH "forward_search" |
#define | IGNORE_COMPUTE "ignore_compute" |
#define | IGNORE_INIT_FILE "ignore_init_file" |
#define | IGNORE_INVAR "ignore_invar" |
#define | IGNORE_LTLSPEC "ignore_ltlspec" |
#define | IGNORE_PSLSPEC "ignore_pslspec" |
#define | IGNORE_SPEC "ignore_spec" |
#define | IMAGE_CLUSTER_SIZE "image_cluster_size" |
#define | INPUT_FILE "input_file" |
#define | INPUT_ORDER_FILE "input_order_file" |
#define | INVAR_CHECK_STRATEGY "check_invar_strategy" |
#define | IWLS95_PREORDER "iwls95preorder" |
#define | KEEP_SINGLE_VALUE_VARS "keep_single_value_vars" |
#define | LIST_PROPERTIES "list_properties" |
#define | LTL2SMV_SINGLE_JUSTICE "ltl2smv_single_justice" |
#define | LTL_TABLEAU_FORWARD_SEARCH "ltl_tableau_forward_search" |
#define | MAX_SHOWN_STATES 65535 |
#define | ON_FAILURE_SCRIPT_QUITS "on_failure_script_quits" |
#define | OPT_CHECK_FSM "check_fsm" |
#define | OPT_USER_POV_NULL_STRING "" |
#define | OREG_JUSTICE_EMPTINESS_BDD_ALGORITHM "oreg_justice_emptiness_bdd_algorithm" |
#define | OUTPUT_BOOLEAN_MODEL_FILE "output_boolean_model_file" |
#define | OUTPUT_FLATTEN_MODEL_FILE "output_flatten_model_file" |
#define | OUTPUT_ORDER_FILE "output_order_file" |
#define | OUTPUT_WORD_FORMAT "output_word_format" |
#define | PARTITION_METHOD "partition_method" |
#define | PP_CPP_PATH "pp_cpp_path" |
#define | PP_LIST "pp_list" |
#define | PP_M4_PATH "pp_m4_path" |
#define | PRINT_REACHABLE "print_reachable" |
#define | PROGRAM_NAME "program_name" |
#define | PROGRAM_PATH "program_path" |
#define | PROP_NO "prop_no" |
#define | PROP_PRINT_METHOD "prop_print_method" |
#define | QUIET_MODE "quiet_mode" |
#define | RBC_CNF_ALGORITHM "rbc_rbc2cnf_algorithm" |
#define | RBC_INLINING "rbc_inlining" |
#define | RBC_INLINING_LAZY "rbc_inlining_lazy" |
#define | REORDER_METHOD "reorder_method" |
#define | RUN_CPP "run_cpp" |
#define | SCRIPT_FILE "script_file" |
#define | SHOW_DEFINES_IN_TRACES "traces_show_defines" |
#define | SHOW_DEFINES_WITH_NEXT "traces_show_defines_with_next" |
#define | SHOWN_STATES "shown_states" |
#define | SYMB_INLINING "sexp_inlining" |
#define | TRACES_HIDING_PREFIX "traces_hiding_prefix" |
#define | TRANS_ORDER_FILE "trans_order_file" |
#define | TYPE_CHECKING_WARNING_ON "type_checking_warning_on" |
#define | USE_ANSI_C_DIV_OP "use_ansi_c_div_op" |
#define | USE_COI_SIZE_SORTING "use_coi_size_sorting" |
#define | USE_FAIR_STATES "use_fair_states" |
#define | USE_REACHABLE_STATES "use_reachable_states" |
#define | VARS_ORD_TYPE "vars_order_type" |
#define | VERBOSE_LEVEL "verbose_level" |
#define | WRITE_ORDER_DUMPS_BITS "write_order_dumps_bits" |
Typedefs |
typedef struct options_TAG * | options_ptr |
Enumerations |
enum | Bdd2bmc_Heuristic { STEPS_HEURISTIC,
SIZE_HEURISTIC
} |
enum | Check_Strategy { FORWARD,
BACKWARD,
FORWARD_BACKWARD,
BDD_BMC
} |
enum | FB_Heuristic { ZIGZAG_HEURISTIC,
SMALLEST_BDD_HEURISTIC
} |
Functions |
BddSohEnum | get_bdd_static_order_heuristics (OptsHandler_ptr) |
int | get_conj_part_threshold (OptsHandler_ptr) |
int | get_default_simulation_steps (OptsHandler_ptr) |
int | get_default_trace_plugin (OptsHandler_ptr opt) |
int | get_image_cluster_size (OptsHandler_ptr) |
char * | get_input_file (OptsHandler_ptr) |
char * | get_input_order_file (OptsHandler_ptr) |
BddOregJusticeEmptinessBddAlgorithmType | get_oreg_justice_emptiness_bdd_algorithm (OptsHandler_ptr opt) |
char * | get_output_boolean_model_file (OptsHandler_ptr) |
char * | get_output_flatten_model_file (OptsHandler_ptr) |
char * | get_output_order_file (OptsHandler_ptr) |
int | get_output_word_format (OptsHandler_ptr) |
TransType | get_partition_method (OptsHandler_ptr opt) |
char * | get_pgm_name (OptsHandler_ptr) |
char * | get_pgm_path (OptsHandler_ptr) |
char * | get_pp_cpp_path (OptsHandler_ptr) |
char * | get_pp_list (OptsHandler_ptr) |
char * | get_pp_m4_path (OptsHandler_ptr) |
int | get_prop_no (OptsHandler_ptr) |
int | get_prop_print_method (OptsHandler_ptr opt) |
Be_CnfAlgorithm | get_rbc2cnf_algorithm (OptsHandler_ptr opt) |
unsigned int | get_reorder_method (OptsHandler_ptr) |
const char * | get_sat_solver (OptsHandler_ptr) |
char * | get_script_file (OptsHandler_ptr) |
char * | get_trans_order_file (OptsHandler_ptr) |
VarsOrdType | get_vars_order_type (OptsHandler_ptr) |
int | get_verbose_level (OptsHandler_ptr) |
boolean | is_default_order_file (OptsHandler_ptr opt) |
boolean | opt_affinity (OptsHandler_ptr) |
boolean | opt_ag_only (OptsHandler_ptr) |
boolean | opt_append_clusters (OptsHandler_ptr) |
boolean | opt_backward_comp (OptsHandler_ptr) |
boolean | opt_batch (OptsHandler_ptr) |
boolean | opt_bdd_encoding_word_bits (OptsHandler_ptr opt) |
boolean | opt_boolconv_uses_prednorm (OptsHandler_ptr opt) |
boolean | opt_check_fsm (OptsHandler_ptr) |
Bdd2bmc_Heuristic | opt_check_invar_bddbmc_heuristic (OptsHandler_ptr opt) |
const char * | opt_check_invar_bddbmc_heuristic_as_string (OptsHandler_ptr opt) |
int | opt_check_invar_bddbmc_heuristic_threshold (OptsHandler_ptr opt) |
FB_Heuristic | opt_check_invar_fb_heuristic (OptsHandler_ptr opt) |
const char * | opt_check_invar_fb_heuristic_as_string (OptsHandler_ptr opt) |
Check_Strategy | opt_check_invar_strategy (OptsHandler_ptr opt) |
const char * | opt_check_invar_strategy_as_string (OptsHandler_ptr opt) |
boolean | opt_cone_of_influence (OptsHandler_ptr) |
boolean | opt_conj_partitioning (OptsHandler_ptr) |
boolean | opt_counter_examples (OptsHandler_ptr) |
void | opt_disable_daggifier (OptsHandler_ptr opt) |
void | opt_disable_syntactic_checks (OptsHandler_ptr opt) |
boolean | opt_dynamic_reorder (OptsHandler_ptr) |
void | opt_enable_daggifier (OptsHandler_ptr opt) |
boolean | opt_enable_sexp2bdd_caching (OptsHandler_ptr) |
void | opt_enable_syntactic_checks (OptsHandler_ptr opt) |
boolean | opt_forward_search (OptsHandler_ptr) |
int | opt_get_daggifier_counter_threshold (OptsHandler_ptr opt) |
int | opt_get_daggifier_depth_threshold (OptsHandler_ptr opt) |
boolean | opt_get_daggifier_statistics (OptsHandler_ptr opt) |
boolean | opt_get_quiet_mode (OptsHandler_ptr opt) |
boolean | opt_ignore_compute (OptsHandler_ptr) |
boolean | opt_ignore_init_file (OptsHandler_ptr) |
boolean | opt_ignore_invar (OptsHandler_ptr) |
boolean | opt_ignore_ltlspec (OptsHandler_ptr) |
boolean | opt_ignore_pslspec (OptsHandler_ptr) |
boolean | opt_ignore_spec (OptsHandler_ptr) |
boolean | opt_is_daggifier_enabled (OptsHandler_ptr opt) |
boolean | opt_iwls95_preorder (OptsHandler_ptr opt) |
boolean | opt_iwls95cp_partitioning (OptsHandler_ptr) |
boolean | opt_keep_single_value_vars (OptsHandler_ptr opt) |
boolean | opt_list_properties (OptsHandler_ptr) |
boolean | opt_ltl2smv_single_justice (OptsHandler_ptr opt) |
boolean | opt_ltl_tableau_forward_search (OptsHandler_ptr opt) |
boolean | opt_monolithic (OptsHandler_ptr) |
boolean | opt_on_failure_script_quits (OptsHandler_ptr) |
boolean | opt_print_reachable (OptsHandler_ptr) |
boolean | opt_rbc_inlining (OptsHandler_ptr opt) |
boolean | opt_rbc_inlining_lazy (OptsHandler_ptr opt) |
boolean | opt_reorder (OptsHandler_ptr) |
void | opt_set_daggifier_counter_threshold (OptsHandler_ptr opt, int x) |
void | opt_set_daggifier_depth_threshold (OptsHandler_ptr opt, int x) |
boolean | opt_show_defines_in_traces (OptsHandler_ptr opt) |
boolean | opt_show_defines_with_next (OptsHandler_ptr opt) |
int | opt_shown_states_level (OptsHandler_ptr) |
boolean | opt_symb_inlining (OptsHandler_ptr opt) |
boolean | opt_syntactic_checks_disabled (OptsHandler_ptr opt) |
const char * | opt_traces_hiding_prefix (OptsHandler_ptr) |
boolean | opt_trans_order_file (OptsHandler_ptr) |
boolean | opt_type_checking_warning_on (OptsHandler_ptr) |
boolean | opt_use_ansi_c_div_op (OptsHandler_ptr opt) |
boolean | opt_use_coi_size_sorting (OptsHandler_ptr opt) |
boolean | opt_use_fair_states (OptsHandler_ptr) |
boolean | opt_use_reachable_states (OptsHandler_ptr) |
boolean | opt_verbose_level_eq (OptsHandler_ptr, int) |
boolean | opt_verbose_level_ge (OptsHandler_ptr, int) |
boolean | opt_verbose_level_gt (OptsHandler_ptr, int) |
boolean | opt_verbose_level_le (OptsHandler_ptr, int) |
boolean | opt_verbose_level_lt (OptsHandler_ptr, int) |
boolean | opt_write_order_dumps_bits (OptsHandler_ptr) |
void | print_partition_method (FILE *) |
void | reset_bdd_encoding_word_bits (OptsHandler_ptr opt) |
void | reset_conj_part_threshold (OptsHandler_ptr) |
void | reset_default_simulation_steps (OptsHandler_ptr) |
void | reset_image_cluster_size (OptsHandler_ptr) |
void | reset_input_file (OptsHandler_ptr) |
void | reset_input_order_file (OptsHandler_ptr) |
void | reset_oreg_justice_emptiness_bdd_algorithm (OptsHandler_ptr opt) |
void | reset_output_boolean_model_file (OptsHandler_ptr) |
void | reset_output_flatten_model_file (OptsHandler_ptr) |
void | reset_output_order_file (OptsHandler_ptr) |
void | reset_partitioning_method (OptsHandler_ptr) |
void | reset_pgm_name (OptsHandler_ptr) |
void | reset_pgm_path (OptsHandler_ptr) |
void | reset_pp_cpp_path (OptsHandler_ptr) |
void | reset_pp_m4_path (OptsHandler_ptr) |
void | reset_prop_print_method (OptsHandler_ptr opt) |
void | reset_script_file (OptsHandler_ptr) |
void | reset_trans_order_file (OptsHandler_ptr) |
void | set_affinity (OptsHandler_ptr) |
void | set_ag_only (OptsHandler_ptr) |
void | set_append_clusters (OptsHandler_ptr) |
void | set_backward_comp (OptsHandler_ptr) |
void | set_batch (OptsHandler_ptr) |
void | set_bdd_encoding_word_bits (OptsHandler_ptr opt) |
void | set_bdd_static_order_heuristics (OptsHandler_ptr, BddSohEnum value) |
void | set_boolconv_uses_prednorm (OptsHandler_ptr opt) |
void | set_check_fsm (OptsHandler_ptr) |
void | set_check_invar_bddbmc_heuristic (OptsHandler_ptr opt, Bdd2bmc_Heuristic strategy) |
void | set_check_invar_bddbmc_heuristic_threshold (OptsHandler_ptr opt, int t) |
void | set_check_invar_fb_heuristic (OptsHandler_ptr opt, FB_Heuristic strategy) |
void | set_check_invar_strategy (OptsHandler_ptr opt, Check_Strategy strategy) |
void | set_cone_of_influence (OptsHandler_ptr) |
void | set_conj_part_threshold (OptsHandler_ptr, int) |
void | set_conj_partitioning (OptsHandler_ptr) |
void | set_counter_examples (OptsHandler_ptr) |
void | set_daggifier_statistics (OptsHandler_ptr opt) |
void | set_default_simulation_steps (OptsHandler_ptr, int) |
boolean | set_default_trace_plugin (OptsHandler_ptr opt, int plugin) |
void | set_dynamic_reorder (OptsHandler_ptr) |
void | set_enable_sexp2bdd_caching (OptsHandler_ptr) |
void | set_forward_search (OptsHandler_ptr) |
void | set_ignore_compute (OptsHandler_ptr) |
void | set_ignore_init_file (OptsHandler_ptr) |
void | set_ignore_invar (OptsHandler_ptr) |
void | set_ignore_ltlspec (OptsHandler_ptr) |
void | set_ignore_pslspec (OptsHandler_ptr) |
void | set_ignore_spec (OptsHandler_ptr) |
void | set_image_cluster_size (OptsHandler_ptr, int) |
void | set_input_file (OptsHandler_ptr, const char *) |
void | set_input_order_file (OptsHandler_ptr, char *) |
void | set_iwls95_preorder (OptsHandler_ptr opt) |
void | set_iwls95cp_partitioning (OptsHandler_ptr) |
void | set_keep_single_value_vars (OptsHandler_ptr opt) |
void | set_list_properties (OptsHandler_ptr) |
void | set_ltl2smv_single_justice (OptsHandler_ptr opt) |
void | set_ltl_tableau_forward_search (OptsHandler_ptr opt) |
void | set_monolithic (OptsHandler_ptr) |
void | set_on_failure_script_quits (OptsHandler_ptr) |
void | set_oreg_justice_emptiness_bdd_algorithm (OptsHandler_ptr opt, BddOregJusticeEmptinessBddAlgorithmType alg) |
void | set_output_boolean_model_file (OptsHandler_ptr, char *) |
void | set_output_flatten_model_file (OptsHandler_ptr, char *) |
void | set_output_order_file (OptsHandler_ptr, char *) |
void | set_output_word_format (OptsHandler_ptr, int i) |
void | set_partition_method (OptsHandler_ptr, const TransType) |
void | set_pgm_name (OptsHandler_ptr, char *) |
void | set_pgm_path (OptsHandler_ptr, char *) |
void | set_pp_cpp_path (OptsHandler_ptr, const char *) |
void | set_pp_list (OptsHandler_ptr, char *, const NuSMVEnv_ptr env) |
void | set_pp_m4_path (OptsHandler_ptr, const char *) |
void | set_print_reachable (OptsHandler_ptr) |
void | set_prop_no (OptsHandler_ptr, int n) |
void | set_prop_print_method (OptsHandler_ptr opt, const char *string) |
void | set_quiet_mode (OptsHandler_ptr opt) |
void | set_rbc2cnf_algorithm (OptsHandler_ptr opt, Be_CnfAlgorithm alg) |
void | set_rbc_inlining (OptsHandler_ptr opt) |
void | set_rbc_inlining_lazy (OptsHandler_ptr opt) |
void | set_reorder (OptsHandler_ptr) |
void | set_reorder_method (OptsHandler_ptr, unsigned int) |
void | set_sat_solver (OptsHandler_ptr, const char *) |
void | set_script_file (OptsHandler_ptr, char *) |
void | set_show_defines_in_traces (OptsHandler_ptr opt) |
void | set_show_defines_with_next (OptsHandler_ptr opt) |
void | set_shown_states_level (OptsHandler_ptr, int) |
void | set_symb_inlining (OptsHandler_ptr opt) |
void | set_traces_hiding_prefix (OptsHandler_ptr, const char *) |
void | set_trans_order_file (OptsHandler_ptr, char *) |
void | set_type_checking_warning_on (OptsHandler_ptr) |
void | set_use_coi_size_sorting (OptsHandler_ptr opt) |
void | set_use_fair_states (OptsHandler_ptr) |
void | set_use_reachable_states (OptsHandler_ptr) |
void | set_vars_order_type (OptsHandler_ptr, VarsOrdType) |
void | set_verbose_level (OptsHandler_ptr, int) |
void | set_write_order_dumps_bits (OptsHandler_ptr) |
void | unset_affinity (OptsHandler_ptr) |
void | unset_ag_only (OptsHandler_ptr) |
void | unset_append_clusters (OptsHandler_ptr) |
void | unset_backward_comp (OptsHandler_ptr) |
void | unset_batch (OptsHandler_ptr) |
void | unset_bdd_encoding_word_bits (OptsHandler_ptr opt) |
void | unset_boolconv_uses_prednorm (OptsHandler_ptr opt) |
void | unset_check_fsm (OptsHandler_ptr) |
void | unset_cone_of_influence (OptsHandler_ptr) |
void | unset_counter_examples (OptsHandler_ptr) |
void | unset_daggifier_statistics (OptsHandler_ptr opt) |
void | unset_dynamic_reorder (OptsHandler_ptr) |
void | unset_enable_sexp2bdd_caching (OptsHandler_ptr) |
void | unset_forward_search (OptsHandler_ptr) |
void | unset_ignore_compute (OptsHandler_ptr) |
void | unset_ignore_init_file (OptsHandler_ptr) |
void | unset_ignore_invar (OptsHandler_ptr) |
void | unset_ignore_ltlspec (OptsHandler_ptr) |
void | unset_ignore_pslspec (OptsHandler_ptr) |
void | unset_ignore_spec (OptsHandler_ptr) |
void | unset_iwls95_preorder (OptsHandler_ptr opt) |
void | unset_keep_single_value_vars (OptsHandler_ptr opt) |
void | unset_list_properties (OptsHandler_ptr) |
void | unset_ltl2smv_single_justice (OptsHandler_ptr opt) |
void | unset_ltl_tableau_forward_search (OptsHandler_ptr opt) |
void | unset_on_failure_script_quits (OptsHandler_ptr) |
void | unset_print_reachable (OptsHandler_ptr) |
void | unset_quiet_mode (OptsHandler_ptr opt) |
void | unset_rbc2cnf_algorithm (OptsHandler_ptr opt) |
void | unset_rbc_inlining (OptsHandler_ptr opt) |
void | unset_rbc_inlining_lazy (OptsHandler_ptr opt) |
void | unset_reorder (OptsHandler_ptr) |
void | unset_show_defines_in_traces (OptsHandler_ptr opt) |
void | unset_show_defines_with_next (OptsHandler_ptr opt) |
void | unset_symb_inlining (OptsHandler_ptr opt) |
void | unset_type_checking_warning_on (OptsHandler_ptr) |
void | unset_use_ansi_c_div_op (OptsHandler_ptr opt) |
void | unset_use_coi_size_sorting (OptsHandler_ptr opt) |
void | unset_use_fair_states (OptsHandler_ptr) |
void | unset_use_reachable_states (OptsHandler_ptr) |
void | unset_write_order_dumps_bits (OptsHandler_ptr) |