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

#include "nusmv/core/utils/utils.h"
#include "nusmv/core/sat/sat.h"
#include "nusmv/core/trans/trans.h"
#include "nusmv/core/enc/enc.h"
#include "nusmv/core/fsm/bdd/bdd.h"
#include "nusmv/core/be/be.h"
#include "nusmv/core/opt/OptsHandler.h"
#include "nusmv/core/cinit/NuSMVEnv.h"

Go to the source code of this file.

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)

Define Documentation

#define A_SAT_SOLVER   "sat_solver"
Todo:
Missing synopsis
Todo:
Missing description
#define AFFINITY_CLUSTERING   "affinity"
Todo:
Missing synopsis
Todo:
Missing description
#define AG_ONLY_SEARCH   "ag_only_search"
Todo:
Missing synopsis
Todo:
Missing description
#define APPEND_CLUSTERS   "append_clusters"
Todo:
Missing synopsis
Todo:
Missing description
#define APPEND_CLUSTERS_VISIBLE   0
Todo:
Missing synopsis
Todo:
Missing description
#define BACKWARD_COMPATIBILITY   "backward_compatibility"
Todo:
Missing synopsis
Todo:
Missing description
#define BATCH   "batch"
Todo:
Missing synopsis
Todo:
Missing description
#define BDD_ENCODE_WORD_BITS   "bdd_encode_word_bits"
Todo:
Missing synopsis
Todo:
Missing description
#define BDD_STATIC_ORDER_HEURISTICS   "bdd_static_order_heuristics"
Todo:
Missing synopsis
Todo:
Missing description
#define BOOLEAN_CONVERSION_USES_PREDICATE_NORMALIZATION   "boolean_conversion_uses_predicate_normalization"
Todo:
Missing synopsis
Todo:
Missing description
#define CHECK_INVAR_BDDBMC_HEURISTIC   "check_invar_bddbmc_heuristic"
Todo:
Missing synopsis
Todo:
Missing description
#define CHECK_INVAR_BDDBMC_HEURISTIC_THRESHOLD   "check_invar_bddbmc_threshold"
Todo:
Missing synopsis
Todo:
Missing description
#define CHECK_INVAR_FB_HEURISTIC   "check_invar_forward_backward_heuristic"
Todo:
Missing synopsis
Todo:
Missing description
#define CONE_OF_INFLUENCE   "cone_of_influence"
Todo:
Missing synopsis
Todo:
Missing description
#define CONJ_PART_THRESHOLD   "conj_part_threshold"
Todo:
Missing synopsis
Todo:
Missing description
#define COUNTER_EXAMPLES   "counter_examples"
Todo:
Missing synopsis
Todo:
Missing description
#define DAGGIFIER_COUNTER_THRESHOLD   "daggifier_counter_threshold"
Todo:
Missing synopsis
Todo:
Missing description
#define DAGGIFIER_DEPTH_THRESHOLD   "daggifier_depth_threshold"
Todo:
Missing synopsis
Todo:
Missing description
#define DAGGIFIER_ENABLED   "daggifier_enabled"
Todo:
Missing synopsis
Todo:
Missing description
#define DAGGIFIER_STATISTICS   "daggifier_statistics"
Todo:
Missing synopsis
Todo:
Missing description
#define DEFAULT_BACKWARD_COMPATIBILITY   false
Todo:
Missing synopsis
Todo:
Missing description
#define DEFAULT_BDD2BMC_HEURISTIC   STEPS_HEURISTIC
Todo:
Missing synopsis
Todo:
Missing description
#define DEFAULT_BDD2BMC_HEURISTIC_THRESHOLD   10
Todo:
Missing synopsis
Todo:
Missing description
#define DEFAULT_BDD_ENCODE_WORD_BITS   true
Todo:
Missing synopsis
Todo:
Missing description
#define DEFAULT_BOOLEAN_CONVERSION_USES_PREDICATE_NORMALIZATION   false
Todo:
Missing synopsis
Todo:
Missing description
#define DEFAULT_CONJ_PART_THRESHOLD   1000
Todo:
Missing synopsis
Todo:
Missing description
#define DEFAULT_DAGGIFIER_COUNTER_THS   3
Todo:
Missing synopsis
Todo:
Missing description
#define DEFAULT_DAGGIFIER_DEPTH_THS   2
Todo:
Missing synopsis
Todo:
Missing description
#define DEFAULT_DAGGIFIER_ENABLED   true
Todo:
Missing synopsis
Todo:
Missing description
#define DEFAULT_FORWARD_BACKWARD_ANALYSIS_HEURISTIC   ZIGZAG_HEURISTIC
Todo:
Missing synopsis
Todo:
Missing description
#define DEFAULT_IMAGE_CLUSTER_SIZE   1000
Todo:
Missing synopsis
Todo:
Missing description
#define DEFAULT_INPUT_FILE   (char *)NULL
Todo:
Missing synopsis
Todo:
Missing description
#define DEFAULT_INPUT_ORDER_FILE   (char *)NULL
Todo:
Missing synopsis
Todo:
Missing description
#define DEFAULT_INVAR_CHECK_STRATEGY   FORWARD
Todo:
Missing synopsis
Todo:
Missing description
#define DEFAULT_LTL2SMV_SINGLE_JUSTICE   false
Todo:
Missing synopsis
Todo:
Missing description
#define DEFAULT_OREG_JUSTICE_EMPTINESS_BDD_ALGORITHM   BDD_OREG_JUSTICE_EMPTINESS_BDD_ALGORITHM_EL_BWD
Todo:
Missing synopsis
Todo:
Missing description
#define DEFAULT_OUTPUT_ORDER_FILE   "temp.ord"
Todo:
Missing synopsis
Todo:
Missing description
#define DEFAULT_PGM_NAME   NUSMV_PACKAGE_NAME

The option header file.

Author:
Marco Roveri This file conatins a data structure to manage all the command line options of the NuSMV system.
Todo:
Missing synopsis
Todo:
Missing description
#define DEFAULT_PGM_PATH   (char *)NULL
Todo:
Missing synopsis
Todo:
Missing description
#define DEFAULT_PP_CPP_PATH   (char *)NULL
Todo:
Missing synopsis
Todo:
Missing description
#define DEFAULT_PP_M4_PATH   (char *)NULL
Todo:
Missing synopsis
Todo:
Missing description
#define DEFAULT_SAT_SOLVER   (char*)NULL
#define DEFAULT_SHOW_DEFINES_IN_TRACES   true
Todo:
Missing synopsis
Todo:
Missing description
#define DEFAULT_SHOW_DEFINES_WITH_NEXT   true
Todo:
Missing synopsis
Todo:
Missing description
#define DEFAULT_SHOWN_STATES   25
Todo:
Missing synopsis
Todo:
Missing description
#define DEFAULT_SIMULATION_STEPS   "default_simulation_steps"
Todo:
Missing synopsis
Todo:
Missing description
#define DEFAULT_TRACE_PLUGIN   "default_trace_plugin"
Todo:
Missing synopsis
Todo:
Missing description
#define DEFAULT_TRACES_HIDING_PREFIX   "__"
Todo:
Missing synopsis
Todo:
Missing description
#define DEFAULT_TRANS_ORDER_FILE   (char *)NULL
Todo:
Missing synopsis
Todo:
Missing description
#define DEFAULT_TYPE_CHECKING_WARNING_ON   true
Todo:
Missing synopsis
Todo:
Missing description
#define DEFAULT_USE_COI_SIZE_SORTING   true
Todo:
Missing synopsis
Todo:
Missing description
#define DISABLE_SYNTACTIC_CHECKS   "disable_syntactic_checks"
Todo:
Missing synopsis
Todo:
Missing description
#define DYNAMIC_REORDER   "dynamic_reorder"
Todo:
Missing synopsis
Todo:
Missing description
#define ENABLE_REORDER   "enable_reorder"
Todo:
Missing synopsis
Todo:
Missing description
#define ENABLE_SEXP2BDD_CACHING   "enable_sexp2bdd_caching"
Todo:
Missing synopsis
Todo:
Missing description
#define FORWARD_SEARCH   "forward_search"
Todo:
Missing synopsis
Todo:
Missing description
#define IGNORE_COMPUTE   "ignore_compute"
Todo:
Missing synopsis
Todo:
Missing description
#define IGNORE_INIT_FILE   "ignore_init_file"
Todo:
Missing synopsis
Todo:
Missing description
#define IGNORE_INVAR   "ignore_invar"
Todo:
Missing synopsis
Todo:
Missing description
#define IGNORE_LTLSPEC   "ignore_ltlspec"
Todo:
Missing synopsis
Todo:
Missing description
#define IGNORE_PSLSPEC   "ignore_pslspec"
Todo:
Missing synopsis
Todo:
Missing description
#define IGNORE_SPEC   "ignore_spec"
Todo:
Missing synopsis
Todo:
Missing description
#define IMAGE_CLUSTER_SIZE   "image_cluster_size"
Todo:
Missing synopsis
Todo:
Missing description
#define INPUT_FILE   "input_file"
Todo:
Missing synopsis
Todo:
Missing description
#define INPUT_ORDER_FILE   "input_order_file"
Todo:
Missing synopsis
Todo:
Missing description
#define INVAR_CHECK_STRATEGY   "check_invar_strategy"
Todo:
Missing synopsis
Todo:
Missing description
#define IWLS95_PREORDER   "iwls95preorder"
Todo:
Missing synopsis
Todo:
Missing description
#define KEEP_SINGLE_VALUE_VARS   "keep_single_value_vars"
Todo:
Missing synopsis
Todo:
Missing description
#define LIST_PROPERTIES   "list_properties"
Todo:
Missing synopsis
Todo:
Missing description
#define LTL2SMV_SINGLE_JUSTICE   "ltl2smv_single_justice"
Todo:
Missing synopsis
Todo:
Missing description
#define LTL_TABLEAU_FORWARD_SEARCH   "ltl_tableau_forward_search"
Todo:
Missing synopsis
Todo:
Missing description
#define MAX_SHOWN_STATES   65535
Todo:
Missing synopsis
Todo:
Missing description
#define ON_FAILURE_SCRIPT_QUITS   "on_failure_script_quits"
Todo:
Missing synopsis
Todo:
Missing description
#define OPT_CHECK_FSM   "check_fsm"
Todo:
Missing synopsis
Todo:
Missing description
#define OPT_USER_POV_NULL_STRING   ""
Todo:
Missing synopsis
Todo:
Missing description
#define OREG_JUSTICE_EMPTINESS_BDD_ALGORITHM   "oreg_justice_emptiness_bdd_algorithm"
Todo:
Missing synopsis
Todo:
Missing description
#define OUTPUT_BOOLEAN_MODEL_FILE   "output_boolean_model_file"
Todo:
Missing synopsis
Todo:
Missing description
#define OUTPUT_FLATTEN_MODEL_FILE   "output_flatten_model_file"
Todo:
Missing synopsis
Todo:
Missing description
#define OUTPUT_ORDER_FILE   "output_order_file"
Todo:
Missing synopsis
Todo:
Missing description
#define OUTPUT_WORD_FORMAT   "output_word_format"
Todo:
Missing synopsis
Todo:
Missing description
#define PARTITION_METHOD   "partition_method"
Todo:
Missing synopsis
Todo:
Missing description
#define PP_CPP_PATH   "pp_cpp_path"
Todo:
Missing synopsis
Todo:
Missing description
#define PP_LIST   "pp_list"
Todo:
Missing synopsis
Todo:
Missing description
#define PP_M4_PATH   "pp_m4_path"
Todo:
Missing synopsis
Todo:
Missing description
#define PRINT_REACHABLE   "print_reachable"
Todo:
Missing synopsis
Todo:
Missing description
#define PROGRAM_NAME   "program_name"
Todo:
Missing synopsis
Todo:
Missing description
#define PROGRAM_PATH   "program_path"
Todo:
Missing synopsis
Todo:
Missing description
#define PROP_NO   "prop_no"
Todo:
Missing synopsis
Todo:
Missing description
#define PROP_PRINT_METHOD   "prop_print_method"
Todo:
Missing synopsis
Todo:
Missing description
#define QUIET_MODE   "quiet_mode"
Todo:
Missing synopsis
Todo:
Missing description
#define RBC_CNF_ALGORITHM   "rbc_rbc2cnf_algorithm"
Todo:
Missing synopsis
Todo:
Missing description
#define RBC_INLINING   "rbc_inlining"
Todo:
Missing synopsis
Todo:
Missing description
#define RBC_INLINING_LAZY   "rbc_inlining_lazy"
Todo:
Missing synopsis
Todo:
Missing description
#define REORDER_METHOD   "reorder_method"
Todo:
Missing synopsis
Todo:
Missing description
#define RUN_CPP   "run_cpp"
Todo:
Missing synopsis
Todo:
Missing description
#define SCRIPT_FILE   "script_file"
Todo:
Missing synopsis
Todo:
Missing description
#define SHOW_DEFINES_IN_TRACES   "traces_show_defines"
Todo:
Missing synopsis
Todo:
Missing description
#define SHOW_DEFINES_WITH_NEXT   "traces_show_defines_with_next"
Todo:
Missing synopsis
Todo:
Missing description
#define SHOWN_STATES   "shown_states"
Todo:
Missing synopsis
Todo:
Missing description
#define SYMB_INLINING   "sexp_inlining"
Todo:
Missing synopsis
Todo:
Missing description
#define TRACES_HIDING_PREFIX   "traces_hiding_prefix"
Todo:
Missing synopsis
Todo:
Missing description
#define TRANS_ORDER_FILE   "trans_order_file"
Todo:
Missing synopsis
Todo:
Missing description
#define TYPE_CHECKING_WARNING_ON   "type_checking_warning_on"
Todo:
Missing synopsis
Todo:
Missing description
#define USE_ANSI_C_DIV_OP   "use_ansi_c_div_op"
Todo:
Missing synopsis
Todo:
Missing description
#define USE_COI_SIZE_SORTING   "use_coi_size_sorting"
Todo:
Missing synopsis
Todo:
Missing description
#define USE_FAIR_STATES   "use_fair_states"
Todo:
Missing synopsis
Todo:
Missing description
#define USE_REACHABLE_STATES   "use_reachable_states"
Todo:
Missing synopsis
Todo:
Missing description
#define VARS_ORD_TYPE   "vars_order_type"
Todo:
Missing synopsis
Todo:
Missing description
#define VERBOSE_LEVEL   "verbose_level"
Todo:
Missing synopsis
Todo:
Missing description
#define WRITE_ORDER_DUMPS_BITS   "write_order_dumps_bits"
Todo:
Missing synopsis
Todo:
Missing description

Typedef Documentation

typedef struct options_TAG* options_ptr

Enumeration Type Documentation

Todo:
Missing synopsis
Todo:
Missing description
Enumerator:
STEPS_HEURISTIC 
SIZE_HEURISTIC 
Todo:
Missing synopsis
Todo:
Missing description
Enumerator:
FORWARD 
BACKWARD 
FORWARD_BACKWARD 
BDD_BMC 
Todo:
Missing synopsis
Todo:
Missing description
Enumerator:
ZIGZAG_HEURISTIC 
SMALLEST_BDD_HEURISTIC 

Function Documentation

BddSohEnum get_bdd_static_order_heuristics ( OptsHandler_ptr   ) 
Todo:
Missing synopsis
Todo:
Missing description
int get_conj_part_threshold ( OptsHandler_ptr   ) 
Todo:
Missing synopsis
Todo:
Missing description
int get_default_simulation_steps ( OptsHandler_ptr   ) 
Todo:
Missing synopsis
Todo:
Missing description
int get_default_trace_plugin ( OptsHandler_ptr  opt  ) 
Todo:
Missing synopsis
Todo:
Missing description
int get_image_cluster_size ( OptsHandler_ptr   ) 
Todo:
Missing synopsis
Todo:
Missing description
char* get_input_file ( OptsHandler_ptr   ) 
Todo:
Missing synopsis
Todo:
Missing description
char* get_input_order_file ( OptsHandler_ptr   ) 
Todo:
Missing synopsis
Todo:
Missing description
BddOregJusticeEmptinessBddAlgorithmType get_oreg_justice_emptiness_bdd_algorithm ( OptsHandler_ptr  opt  ) 
char* get_output_boolean_model_file ( OptsHandler_ptr   ) 
Todo:
Missing synopsis
Todo:
Missing description
char* get_output_flatten_model_file ( OptsHandler_ptr   ) 
Todo:
Missing synopsis
Todo:
Missing description
char* get_output_order_file ( OptsHandler_ptr   ) 
Todo:
Missing synopsis
Todo:
Missing description
int get_output_word_format ( OptsHandler_ptr   ) 
Todo:
Missing synopsis
Todo:
Missing description
TransType get_partition_method ( OptsHandler_ptr  opt  ) 
Todo:
Missing synopsis
Todo:
Missing description
char* get_pgm_name ( OptsHandler_ptr   ) 
Todo:
Missing synopsis
Todo:
Missing description
char* get_pgm_path ( OptsHandler_ptr   ) 
Todo:
Missing synopsis
Todo:
Missing description
char* get_pp_cpp_path ( OptsHandler_ptr   ) 
Todo:
Missing synopsis
Todo:
Missing description
char* get_pp_list ( OptsHandler_ptr   ) 
Todo:
Missing synopsis
Todo:
Missing description
char* get_pp_m4_path ( OptsHandler_ptr   ) 
Todo:
Missing synopsis
Todo:
Missing description
int get_prop_no ( OptsHandler_ptr   ) 
Todo:
Missing synopsis
Todo:
Missing description
int get_prop_print_method ( OptsHandler_ptr  opt  ) 
Todo:
Missing synopsis
Todo:
Missing description
Be_CnfAlgorithm get_rbc2cnf_algorithm ( OptsHandler_ptr  opt  ) 
Todo:
Missing synopsis
Todo:
Missing description
unsigned int get_reorder_method ( OptsHandler_ptr   ) 
Todo:
Missing synopsis
Todo:
Missing description
const char* get_sat_solver ( OptsHandler_ptr   ) 
Todo:
Missing synopsis
Todo:
Missing description
char* get_script_file ( OptsHandler_ptr   ) 
Todo:
Missing synopsis
Todo:
Missing description
char* get_trans_order_file ( OptsHandler_ptr   ) 
Todo:
Missing synopsis
Todo:
Missing description
VarsOrdType get_vars_order_type ( OptsHandler_ptr   ) 
Todo:
Missing synopsis
Todo:
Missing description
int get_verbose_level ( OptsHandler_ptr   ) 
Todo:
Missing synopsis
Todo:
Missing description
boolean is_default_order_file ( OptsHandler_ptr  opt  ) 
Todo:
Missing synopsis
Todo:
Missing description
boolean opt_affinity ( OptsHandler_ptr   ) 
Todo:
Missing synopsis
Todo:
Missing description
boolean opt_ag_only ( OptsHandler_ptr   ) 
Todo:
Missing synopsis
Todo:
Missing description
boolean opt_append_clusters ( OptsHandler_ptr   ) 
Todo:
Missing synopsis
Todo:
Missing description
boolean opt_backward_comp ( OptsHandler_ptr   ) 
Todo:
Missing synopsis
Todo:
Missing description
boolean opt_batch ( OptsHandler_ptr   ) 
Todo:
Missing synopsis
Todo:
Missing description
boolean opt_bdd_encoding_word_bits ( OptsHandler_ptr  opt  ) 
Todo:
Missing synopsis
Todo:
Missing description
boolean opt_boolconv_uses_prednorm ( OptsHandler_ptr  opt  ) 
Todo:
Missing synopsis
Todo:
Missing description
boolean opt_check_fsm ( OptsHandler_ptr   ) 
Todo:
Missing synopsis
Todo:
Missing description
Bdd2bmc_Heuristic opt_check_invar_bddbmc_heuristic ( OptsHandler_ptr  opt  ) 
Todo:
Missing synopsis
Todo:
Missing description
const char* opt_check_invar_bddbmc_heuristic_as_string ( OptsHandler_ptr  opt  ) 
Todo:
Missing synopsis
Todo:
Missing description
int opt_check_invar_bddbmc_heuristic_threshold ( OptsHandler_ptr  opt  ) 
Todo:
Missing synopsis
Todo:
Missing description
FB_Heuristic opt_check_invar_fb_heuristic ( OptsHandler_ptr  opt  ) 
Todo:
Missing synopsis
Todo:
Missing description
const char* opt_check_invar_fb_heuristic_as_string ( OptsHandler_ptr  opt  ) 
Todo:
Missing synopsis
Todo:
Missing description
Check_Strategy opt_check_invar_strategy ( OptsHandler_ptr  opt  ) 
Todo:
Missing synopsis
Todo:
Missing description
const char* opt_check_invar_strategy_as_string ( OptsHandler_ptr  opt  ) 
Todo:
Missing synopsis
Todo:
Missing description
boolean opt_cone_of_influence ( OptsHandler_ptr   ) 
Todo:
Missing synopsis
Todo:
Missing description
boolean opt_conj_partitioning ( OptsHandler_ptr   ) 
Todo:
Missing synopsis
Todo:
Missing description
boolean opt_counter_examples ( OptsHandler_ptr   ) 
Todo:
Missing synopsis
Todo:
Missing description
void opt_disable_daggifier ( OptsHandler_ptr  opt  ) 
Todo:
Missing synopsis
Todo:
Missing description
void opt_disable_syntactic_checks ( OptsHandler_ptr  opt  ) 
Todo:
Missing synopsis
Todo:
Missing description
boolean opt_dynamic_reorder ( OptsHandler_ptr   ) 
Todo:
Missing synopsis
Todo:
Missing description
void opt_enable_daggifier ( OptsHandler_ptr  opt  ) 
Todo:
Missing synopsis
Todo:
Missing description
boolean opt_enable_sexp2bdd_caching ( OptsHandler_ptr   ) 
Todo:
Missing synopsis
Todo:
Missing description
void opt_enable_syntactic_checks ( OptsHandler_ptr  opt  ) 
Todo:
Missing synopsis
Todo:
Missing description
boolean opt_forward_search ( OptsHandler_ptr   ) 
Todo:
Missing synopsis
Todo:
Missing description
int opt_get_daggifier_counter_threshold ( OptsHandler_ptr  opt  ) 
Todo:
Missing synopsis
Todo:
Missing description
int opt_get_daggifier_depth_threshold ( OptsHandler_ptr  opt  ) 
Todo:
Missing synopsis
Todo:
Missing description
boolean opt_get_daggifier_statistics ( OptsHandler_ptr  opt  ) 
Todo:
Missing synopsis
Todo:
Missing description
boolean opt_get_quiet_mode ( OptsHandler_ptr  opt  ) 
Todo:
Missing synopsis
Todo:
Missing description
boolean opt_ignore_compute ( OptsHandler_ptr   ) 
Todo:
Missing synopsis
Todo:
Missing description
boolean opt_ignore_init_file ( OptsHandler_ptr   ) 
Todo:
Missing synopsis
Todo:
Missing description
boolean opt_ignore_invar ( OptsHandler_ptr   ) 
Todo:
Missing synopsis
Todo:
Missing description
boolean opt_ignore_ltlspec ( OptsHandler_ptr   ) 
Todo:
Missing synopsis
Todo:
Missing description
boolean opt_ignore_pslspec ( OptsHandler_ptr   ) 
Todo:
Missing synopsis
Todo:
Missing description
boolean opt_ignore_spec ( OptsHandler_ptr   ) 
Todo:
Missing synopsis
Todo:
Missing description
boolean opt_is_daggifier_enabled ( OptsHandler_ptr  opt  ) 
Todo:
Missing synopsis
Todo:
Missing description
boolean opt_iwls95_preorder ( OptsHandler_ptr  opt  ) 
Todo:
Missing synopsis
Todo:
Missing description
boolean opt_iwls95cp_partitioning ( OptsHandler_ptr   ) 
Todo:
Missing synopsis
Todo:
Missing description
boolean opt_keep_single_value_vars ( OptsHandler_ptr  opt  ) 
Todo:
Missing synopsis
Todo:
Missing description
boolean opt_list_properties ( OptsHandler_ptr   ) 
Todo:
Missing synopsis
Todo:
Missing description
boolean opt_ltl2smv_single_justice ( OptsHandler_ptr  opt  ) 
Todo:
Missing synopsis
Todo:
Missing description
boolean opt_ltl_tableau_forward_search ( OptsHandler_ptr  opt  ) 
Todo:
Missing synopsis
Todo:
Missing description
boolean opt_monolithic ( OptsHandler_ptr   ) 
Todo:
Missing synopsis
Todo:
Missing description
boolean opt_on_failure_script_quits ( OptsHandler_ptr   ) 
Todo:
Missing synopsis
Todo:
Missing description
boolean opt_print_reachable ( OptsHandler_ptr   ) 
Todo:
Missing synopsis
Todo:
Missing description
boolean opt_rbc_inlining ( OptsHandler_ptr  opt  ) 
Todo:
Missing synopsis
Todo:
Missing description
boolean opt_rbc_inlining_lazy ( OptsHandler_ptr  opt  ) 
Todo:
Missing synopsis
Todo:
Missing description
boolean opt_reorder ( OptsHandler_ptr   ) 
Todo:
Missing synopsis
Todo:
Missing description
void opt_set_daggifier_counter_threshold ( OptsHandler_ptr  opt,
int  x 
)
Todo:
Missing synopsis
Todo:
Missing description
void opt_set_daggifier_depth_threshold ( OptsHandler_ptr  opt,
int  x 
)
Todo:
Missing synopsis
Todo:
Missing description
boolean opt_show_defines_in_traces ( OptsHandler_ptr  opt  ) 
Todo:
Missing synopsis
Todo:
Missing description
boolean opt_show_defines_with_next ( OptsHandler_ptr  opt  ) 
Todo:
Missing synopsis
Todo:
Missing description
int opt_shown_states_level ( OptsHandler_ptr   ) 
Todo:
Missing synopsis
Todo:
Missing description
boolean opt_symb_inlining ( OptsHandler_ptr  opt  ) 
Todo:
Missing synopsis
Todo:
Missing description
boolean opt_syntactic_checks_disabled ( OptsHandler_ptr  opt  ) 
Todo:
Missing synopsis
Todo:
Missing description
const char* opt_traces_hiding_prefix ( OptsHandler_ptr   ) 
Todo:
Missing synopsis
Todo:
Missing description
boolean opt_trans_order_file ( OptsHandler_ptr   ) 
Todo:
Missing synopsis
Todo:
Missing description
boolean opt_type_checking_warning_on ( OptsHandler_ptr   ) 
Todo:
Missing synopsis
Todo:
Missing description
boolean opt_use_ansi_c_div_op ( OptsHandler_ptr  opt  ) 
Todo:
Missing synopsis
Todo:
Missing description
boolean opt_use_coi_size_sorting ( OptsHandler_ptr  opt  ) 
Todo:
Missing synopsis
Todo:
Missing description
boolean opt_use_fair_states ( OptsHandler_ptr   ) 
Todo:
Missing synopsis
Todo:
Missing description
boolean opt_use_reachable_states ( OptsHandler_ptr   ) 
Todo:
Missing synopsis
Todo:
Missing description
boolean opt_verbose_level_eq ( OptsHandler_ptr  ,
int   
)
Todo:
Missing synopsis
Todo:
Missing description
boolean opt_verbose_level_ge ( OptsHandler_ptr  ,
int   
)
Todo:
Missing synopsis
Todo:
Missing description
boolean opt_verbose_level_gt ( OptsHandler_ptr  ,
int   
)
Todo:
Missing synopsis
Todo:
Missing description
boolean opt_verbose_level_le ( OptsHandler_ptr  ,
int   
)
Todo:
Missing synopsis
Todo:
Missing description
boolean opt_verbose_level_lt ( OptsHandler_ptr  ,
int   
)
Todo:
Missing synopsis
Todo:
Missing description
boolean opt_write_order_dumps_bits ( OptsHandler_ptr   ) 
Todo:
Missing synopsis
Todo:
Missing description
void print_partition_method ( FILE *   ) 
Todo:
Missing synopsis
Todo:
Missing description
void reset_bdd_encoding_word_bits ( OptsHandler_ptr  opt  ) 
Todo:
Missing synopsis
Todo:
Missing description
void reset_conj_part_threshold ( OptsHandler_ptr   ) 
Todo:
Missing synopsis
Todo:
Missing description
void reset_default_simulation_steps ( OptsHandler_ptr   ) 
Todo:
Missing synopsis
Todo:
Missing description
void reset_image_cluster_size ( OptsHandler_ptr   ) 
Todo:
Missing synopsis
Todo:
Missing description
void reset_input_file ( OptsHandler_ptr   ) 
Todo:
Missing synopsis
Todo:
Missing description
void reset_input_order_file ( OptsHandler_ptr   ) 
Todo:
Missing synopsis
Todo:
Missing description
void reset_oreg_justice_emptiness_bdd_algorithm ( OptsHandler_ptr  opt  ) 
void reset_output_boolean_model_file ( OptsHandler_ptr   ) 
Todo:
Missing synopsis
Todo:
Missing description
void reset_output_flatten_model_file ( OptsHandler_ptr   ) 
Todo:
Missing synopsis
Todo:
Missing description
void reset_output_order_file ( OptsHandler_ptr   ) 
Todo:
Missing synopsis
Todo:
Missing description
void reset_partitioning_method ( OptsHandler_ptr   ) 
Todo:
Missing synopsis
Todo:
Missing description
void reset_pgm_name ( OptsHandler_ptr   ) 
Todo:
Missing synopsis
Todo:
Missing description
void reset_pgm_path ( OptsHandler_ptr   ) 
Todo:
Missing synopsis
Todo:
Missing description
void reset_pp_cpp_path ( OptsHandler_ptr   ) 
Todo:
Missing synopsis
Todo:
Missing description
void reset_pp_m4_path ( OptsHandler_ptr   ) 
Todo:
Missing synopsis
Todo:
Missing description
void reset_prop_print_method ( OptsHandler_ptr  opt  ) 
Todo:
Missing synopsis
Todo:
Missing description
void reset_script_file ( OptsHandler_ptr   ) 
Todo:
Missing synopsis
Todo:
Missing description
void reset_trans_order_file ( OptsHandler_ptr   ) 
Todo:
Missing synopsis
Todo:
Missing description
void set_affinity ( OptsHandler_ptr   ) 
Todo:
Missing synopsis
Todo:
Missing description
void set_ag_only ( OptsHandler_ptr   ) 
Todo:
Missing synopsis
Todo:
Missing description
void set_append_clusters ( OptsHandler_ptr   ) 
Todo:
Missing synopsis
Todo:
Missing description
void set_backward_comp ( OptsHandler_ptr   ) 
Todo:
Missing synopsis
Todo:
Missing description
void set_batch ( OptsHandler_ptr   ) 
Todo:
Missing synopsis
Todo:
Missing description
void set_bdd_encoding_word_bits ( OptsHandler_ptr  opt  ) 
Todo:
Missing synopsis
Todo:
Missing description
void set_bdd_static_order_heuristics ( OptsHandler_ptr  ,
BddSohEnum  value 
)
Todo:
Missing synopsis
Todo:
Missing description
void set_boolconv_uses_prednorm ( OptsHandler_ptr  opt  ) 
Todo:
Missing synopsis
Todo:
Missing description
void set_check_fsm ( OptsHandler_ptr   ) 
Todo:
Missing synopsis
Todo:
Missing description
void set_check_invar_bddbmc_heuristic ( OptsHandler_ptr  opt,
Bdd2bmc_Heuristic  strategy 
)
Todo:
Missing synopsis
Todo:
Missing description
void set_check_invar_bddbmc_heuristic_threshold ( OptsHandler_ptr  opt,
int  t 
)
Todo:
Missing synopsis
Todo:
Missing description
void set_check_invar_fb_heuristic ( OptsHandler_ptr  opt,
FB_Heuristic  strategy 
)
Todo:
Missing synopsis
Todo:
Missing description
void set_check_invar_strategy ( OptsHandler_ptr  opt,
Check_Strategy  strategy 
)
Todo:
Missing synopsis
Todo:
Missing description
void set_cone_of_influence ( OptsHandler_ptr   ) 
Todo:
Missing synopsis
Todo:
Missing description
void set_conj_part_threshold ( OptsHandler_ptr  ,
int   
)
Todo:
Missing synopsis
Todo:
Missing description
void set_conj_partitioning ( OptsHandler_ptr   ) 
Todo:
Missing synopsis
Todo:
Missing description
void set_counter_examples ( OptsHandler_ptr   ) 
Todo:
Missing synopsis
Todo:
Missing description
void set_daggifier_statistics ( OptsHandler_ptr  opt  ) 
Todo:
Missing synopsis
Todo:
Missing description
void set_default_simulation_steps ( OptsHandler_ptr  ,
int   
)
Todo:
Missing synopsis
Todo:
Missing description
boolean set_default_trace_plugin ( OptsHandler_ptr  opt,
int  plugin 
)
Todo:
Missing synopsis
Todo:
Missing description
void set_dynamic_reorder ( OptsHandler_ptr   ) 
Todo:
Missing synopsis
Todo:
Missing description
void set_enable_sexp2bdd_caching ( OptsHandler_ptr   ) 
Todo:
Missing synopsis
Todo:
Missing description
void set_forward_search ( OptsHandler_ptr   ) 
Todo:
Missing synopsis
Todo:
Missing description
void set_ignore_compute ( OptsHandler_ptr   ) 
Todo:
Missing synopsis
Todo:
Missing description
void set_ignore_init_file ( OptsHandler_ptr   ) 
Todo:
Missing synopsis
Todo:
Missing description
void set_ignore_invar ( OptsHandler_ptr   ) 
Todo:
Missing synopsis
Todo:
Missing description
void set_ignore_ltlspec ( OptsHandler_ptr   ) 
Todo:
Missing synopsis
Todo:
Missing description
void set_ignore_pslspec ( OptsHandler_ptr   ) 
Todo:
Missing synopsis
Todo:
Missing description
void set_ignore_spec ( OptsHandler_ptr   ) 
Todo:
Missing synopsis
Todo:
Missing description
void set_image_cluster_size ( OptsHandler_ptr  ,
int   
)
Todo:
Missing synopsis
Todo:
Missing description
void set_input_file ( OptsHandler_ptr  ,
const char *   
)
Todo:
Missing synopsis
Todo:
Missing description
void set_input_order_file ( OptsHandler_ptr  ,
char *   
)
Todo:
Missing synopsis
Todo:
Missing description
void set_iwls95_preorder ( OptsHandler_ptr  opt  ) 
Todo:
Missing synopsis
Todo:
Missing description
void set_iwls95cp_partitioning ( OptsHandler_ptr   ) 
Todo:
Missing synopsis
Todo:
Missing description
void set_keep_single_value_vars ( OptsHandler_ptr  opt  ) 
Todo:
Missing synopsis
Todo:
Missing description
void set_list_properties ( OptsHandler_ptr   ) 
Todo:
Missing synopsis
Todo:
Missing description
void set_ltl2smv_single_justice ( OptsHandler_ptr  opt  ) 
Todo:
Missing synopsis
Todo:
Missing description
void set_ltl_tableau_forward_search ( OptsHandler_ptr  opt  ) 
Todo:
Missing synopsis
Todo:
Missing description
void set_monolithic ( OptsHandler_ptr   ) 
Todo:
Missing synopsis
Todo:
Missing description
void set_on_failure_script_quits ( OptsHandler_ptr   ) 
Todo:
Missing synopsis
Todo:
Missing description
void set_oreg_justice_emptiness_bdd_algorithm ( OptsHandler_ptr  opt,
BddOregJusticeEmptinessBddAlgorithmType  alg 
)
void set_output_boolean_model_file ( OptsHandler_ptr  ,
char *   
)
Todo:
Missing synopsis
Todo:
Missing description
void set_output_flatten_model_file ( OptsHandler_ptr  ,
char *   
)
Todo:
Missing synopsis
Todo:
Missing description
void set_output_order_file ( OptsHandler_ptr  ,
char *   
)
Todo:
Missing synopsis
Todo:
Missing description
void set_output_word_format ( OptsHandler_ptr  ,
int  i 
)
Todo:
Missing synopsis
Todo:
Missing description
void set_partition_method ( OptsHandler_ptr  ,
const   TransType 
)
Todo:
Missing synopsis
Todo:
Missing description
void set_pgm_name ( OptsHandler_ptr  ,
char *   
)
Todo:
Missing synopsis
Todo:
Missing description
void set_pgm_path ( OptsHandler_ptr  ,
char *   
)
Todo:
Missing synopsis
Todo:
Missing description
void set_pp_cpp_path ( OptsHandler_ptr  ,
const char *   
)
Todo:
Missing synopsis
Todo:
Missing description
void set_pp_list ( OptsHandler_ptr  ,
char *  ,
const NuSMVEnv_ptr  env 
)
Todo:
Missing synopsis
Todo:
Missing description
void set_pp_m4_path ( OptsHandler_ptr  ,
const char *   
)
Todo:
Missing synopsis
Todo:
Missing description
void set_print_reachable ( OptsHandler_ptr   ) 
Todo:
Missing synopsis
Todo:
Missing description
void set_prop_no ( OptsHandler_ptr  ,
int  n 
)
Todo:
Missing synopsis
Todo:
Missing description
void set_prop_print_method ( OptsHandler_ptr  opt,
const char *  string 
)
Todo:
Missing synopsis
Todo:
Missing description
void set_quiet_mode ( OptsHandler_ptr  opt  ) 
Todo:
Missing synopsis
Todo:
Missing description
void set_rbc2cnf_algorithm ( OptsHandler_ptr  opt,
Be_CnfAlgorithm  alg 
)
Todo:
Missing synopsis
Todo:
Missing description
void set_rbc_inlining ( OptsHandler_ptr  opt  ) 
Todo:
Missing synopsis
Todo:
Missing description
void set_rbc_inlining_lazy ( OptsHandler_ptr  opt  ) 
Todo:
Missing synopsis
Todo:
Missing description
void set_reorder ( OptsHandler_ptr   ) 
Todo:
Missing synopsis
Todo:
Missing description
void set_reorder_method ( OptsHandler_ptr  ,
unsigned  int 
)
Todo:
Missing synopsis
Todo:
Missing description
void set_sat_solver ( OptsHandler_ptr  ,
const char *   
)
Todo:
Missing synopsis
Todo:
Missing description
void set_script_file ( OptsHandler_ptr  ,
char *   
)
Todo:
Missing synopsis
Todo:
Missing description
void set_show_defines_in_traces ( OptsHandler_ptr  opt  ) 
Todo:
Missing synopsis
Todo:
Missing description
void set_show_defines_with_next ( OptsHandler_ptr  opt  ) 
Todo:
Missing synopsis
Todo:
Missing description
void set_shown_states_level ( OptsHandler_ptr  ,
int   
)
Todo:
Missing synopsis
Todo:
Missing description
void set_symb_inlining ( OptsHandler_ptr  opt  ) 
Todo:
Missing synopsis
Todo:
Missing description
void set_traces_hiding_prefix ( OptsHandler_ptr  ,
const char *   
)
Todo:
Missing synopsis
Todo:
Missing description
void set_trans_order_file ( OptsHandler_ptr  ,
char *   
)
Todo:
Missing synopsis
Todo:
Missing description
void set_type_checking_warning_on ( OptsHandler_ptr   ) 
Todo:
Missing synopsis
Todo:
Missing description
void set_use_coi_size_sorting ( OptsHandler_ptr  opt  ) 
Todo:
Missing synopsis
Todo:
Missing description
void set_use_fair_states ( OptsHandler_ptr   ) 
Todo:
Missing synopsis
Todo:
Missing description
void set_use_reachable_states ( OptsHandler_ptr   ) 
Todo:
Missing synopsis
Todo:
Missing description
void set_vars_order_type ( OptsHandler_ptr  ,
VarsOrdType   
)
Todo:
Missing synopsis
Todo:
Missing description
void set_verbose_level ( OptsHandler_ptr  ,
int   
)
Todo:
Missing synopsis
Todo:
Missing description
void set_write_order_dumps_bits ( OptsHandler_ptr   ) 
Todo:
Missing synopsis
Todo:
Missing description
void unset_affinity ( OptsHandler_ptr   ) 
Todo:
Missing synopsis
Todo:
Missing description
void unset_ag_only ( OptsHandler_ptr   ) 
Todo:
Missing synopsis
Todo:
Missing description
void unset_append_clusters ( OptsHandler_ptr   ) 
Todo:
Missing synopsis
Todo:
Missing description
void unset_backward_comp ( OptsHandler_ptr   ) 
Todo:
Missing synopsis
Todo:
Missing description
void unset_batch ( OptsHandler_ptr   ) 
Todo:
Missing synopsis
Todo:
Missing description
void unset_bdd_encoding_word_bits ( OptsHandler_ptr  opt  ) 
Todo:
Missing synopsis
Todo:
Missing description
void unset_boolconv_uses_prednorm ( OptsHandler_ptr  opt  ) 
Todo:
Missing synopsis
Todo:
Missing description
void unset_check_fsm ( OptsHandler_ptr   ) 
Todo:
Missing synopsis
Todo:
Missing description
void unset_cone_of_influence ( OptsHandler_ptr   ) 
Todo:
Missing synopsis
Todo:
Missing description
void unset_counter_examples ( OptsHandler_ptr   ) 
Todo:
Missing synopsis
Todo:
Missing description
void unset_daggifier_statistics ( OptsHandler_ptr  opt  ) 
Todo:
Missing synopsis
Todo:
Missing description
void unset_dynamic_reorder ( OptsHandler_ptr   ) 
Todo:
Missing synopsis
Todo:
Missing description
void unset_enable_sexp2bdd_caching ( OptsHandler_ptr   ) 
Todo:
Missing synopsis
Todo:
Missing description
void unset_forward_search ( OptsHandler_ptr   ) 
Todo:
Missing synopsis
Todo:
Missing description
void unset_ignore_compute ( OptsHandler_ptr   ) 
Todo:
Missing synopsis
Todo:
Missing description
void unset_ignore_init_file ( OptsHandler_ptr   ) 
Todo:
Missing synopsis
Todo:
Missing description
void unset_ignore_invar ( OptsHandler_ptr   ) 
Todo:
Missing synopsis
Todo:
Missing description
void unset_ignore_ltlspec ( OptsHandler_ptr   ) 
Todo:
Missing synopsis
Todo:
Missing description
void unset_ignore_pslspec ( OptsHandler_ptr   ) 
Todo:
Missing synopsis
Todo:
Missing description
void unset_ignore_spec ( OptsHandler_ptr   ) 
Todo:
Missing synopsis
Todo:
Missing description
void unset_iwls95_preorder ( OptsHandler_ptr  opt  ) 
Todo:
Missing synopsis
Todo:
Missing description
void unset_keep_single_value_vars ( OptsHandler_ptr  opt  ) 
Todo:
Missing synopsis
Todo:
Missing description
void unset_list_properties ( OptsHandler_ptr   ) 
Todo:
Missing synopsis
Todo:
Missing description
void unset_ltl2smv_single_justice ( OptsHandler_ptr  opt  ) 
Todo:
Missing synopsis
Todo:
Missing description
void unset_ltl_tableau_forward_search ( OptsHandler_ptr  opt  ) 
Todo:
Missing synopsis
Todo:
Missing description
void unset_on_failure_script_quits ( OptsHandler_ptr   ) 
Todo:
Missing synopsis
Todo:
Missing description
void unset_print_reachable ( OptsHandler_ptr   ) 
Todo:
Missing synopsis
Todo:
Missing description
void unset_quiet_mode ( OptsHandler_ptr  opt  ) 
Todo:
Missing synopsis
Todo:
Missing description
void unset_rbc2cnf_algorithm ( OptsHandler_ptr  opt  ) 
Todo:
Missing synopsis
Todo:
Missing description
void unset_rbc_inlining ( OptsHandler_ptr  opt  ) 
Todo:
Missing synopsis
Todo:
Missing description
void unset_rbc_inlining_lazy ( OptsHandler_ptr  opt  ) 
Todo:
Missing synopsis
Todo:
Missing description
void unset_reorder ( OptsHandler_ptr   ) 
Todo:
Missing synopsis
Todo:
Missing description
void unset_show_defines_in_traces ( OptsHandler_ptr  opt  ) 
Todo:
Missing synopsis
Todo:
Missing description
void unset_show_defines_with_next ( OptsHandler_ptr  opt  ) 
Todo:
Missing synopsis
Todo:
Missing description
void unset_symb_inlining ( OptsHandler_ptr  opt  ) 
Todo:
Missing synopsis
Todo:
Missing description
void unset_type_checking_warning_on ( OptsHandler_ptr   ) 
Todo:
Missing synopsis
Todo:
Missing description
void unset_use_ansi_c_div_op ( OptsHandler_ptr  opt  ) 
Todo:
Missing synopsis
Todo:
Missing description
void unset_use_coi_size_sorting ( OptsHandler_ptr  opt  ) 
Todo:
Missing synopsis
Todo:
Missing description
void unset_use_fair_states ( OptsHandler_ptr   ) 
Todo:
Missing synopsis
Todo:
Missing description
void unset_use_reachable_states ( OptsHandler_ptr   ) 
Todo:
Missing synopsis
Todo:
Missing description
void unset_write_order_dumps_bits ( OptsHandler_ptr   ) 
Todo:
Missing synopsis
Todo:
Missing description
 All Data Structures Files Functions Variables Typedefs Enumerations Enumerator Defines

Generated on 14 Oct 2015 for NuSMV Developers Manual by  doxygen 1.6.1