NuSMV Developers Manual: NuSMV/code/nusmv/core/opt/opt.h Source File

00001 /* ---------------------------------------------------------------------------
00002 
00003 
00004   This file is part of the ``opt'' package of NuSMV version 2.
00005   Copyright (C) 1998-2001 by CMU and FBK-irst.
00006 
00007   NuSMV version 2 is free software; you can redistribute it and/or
00008   modify it under the terms of the GNU Lesser General Public
00009   License as published by the Free Software Foundation; either
00010   version 2 of the License, or (at your option) any later version.
00011 
00012   NuSMV version 2 is distributed in the hope that it will be useful,
00013   but WITHOUT ANY WARRANTY; without even the implied warranty of
00014   MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
00015   Lesser General Public License for more details.
00016 
00017   You should have received a copy of the GNU Lesser General Public
00018   License along with this library; if not, write to the Free Software
00019   Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307  USA.
00020 
00021   For more information on NuSMV see <http://nusmv.fbk.eu>
00022   or email to <nusmv-users@fbk.eu>.
00023   Please report bugs to <nusmv-users@fbk.eu>.
00024 
00025   To contact the NuSMV development board, email to <nusmv@fbk.eu>.
00026 
00027 -----------------------------------------------------------------------------*/
00028 
00039 #ifndef __NUSMV_CORE_OPT_OPT_H__
00040 #define __NUSMV_CORE_OPT_OPT_H__
00041 
00042 #if HAVE_CONFIG_H
00043 # include "nusmv-config.h"
00044 #endif
00045 
00046 #if NUSMV_HAVE_REGEX_H
00047 # if NUSMV_HAVE_SYS_TYPES_H
00048 /* posix requires that sys/types.h is included before regex */
00049 #  include <sys/types.h>
00050 # endif
00051 # include <regex.h>
00052 #endif
00053 
00054 #include "nusmv/core/utils/utils.h"
00055 #include "nusmv/core/sat/sat.h" /* for SAT Solver */
00056 #include "nusmv/core/trans/trans.h" /* for TransType */
00057 #include "nusmv/core/enc/enc.h" /* for VarsOrderType and BddSohEnum*/
00058 #include "nusmv/core/fsm/bdd/bdd.h" /* for BddOregJusticeEmptinessBddAlgorithmType */
00059 #include "nusmv/core/be/be.h" /* For RBC2CNF algorithms */
00060 #include "nusmv/core/opt/OptsHandler.h"
00061 #include "nusmv/core/cinit/NuSMVEnv.h"
00062 
00063 /*---------------------------------------------------------------------------*/
00064 /* Constant declarations                                                     */
00065 /*---------------------------------------------------------------------------*/
00066 
00067 /* Opts names */
00068 
00074 #define DEFAULT_PGM_NAME   NUSMV_PACKAGE_NAME
00075 
00081 #define DEFAULT_PGM_PATH   (char *)NULL
00082 
00088 #define DEFAULT_INPUT_FILE (char *)NULL
00089 
00095 #define DEFAULT_INPUT_ORDER_FILE (char *)NULL
00096 
00102 #define DEFAULT_OUTPUT_ORDER_FILE "temp.ord"
00103 
00109 #define DEFAULT_TRANS_ORDER_FILE (char *)NULL
00110 
00116 #define DEFAULT_PP_CPP_PATH (char *)NULL
00117 
00123 #define DEFAULT_PP_M4_PATH (char *)NULL
00124 
00125 /* outputs warning instead of errors in type checking */
00126 
00132 #define DEFAULT_BACKWARD_COMPATIBILITY false
00133 /* allows warning messages to be printed during type checking */
00134 
00140 #define DEFAULT_TYPE_CHECKING_WARNING_ON true
00141 
00147 #define DEFAULT_CONJ_PART_THRESHOLD 1000
00148 
00154 #define DEFAULT_IMAGE_CLUSTER_SIZE 1000
00155 
00161 #define DEFAULT_SHOWN_STATES 25
00162 /* maximum number of states shown during an interactive simulation step*/
00163 
00169 #define MAX_SHOWN_STATES 65535
00170 
00171 #if NUSMV_HAVE_SOLVER_MINISAT
00172 
00178 #define DEFAULT_SAT_SOLVER        "MiniSat"
00179 #else
00180 #if NUSMV_HAVE_SOLVER_ZCHAFF
00181 #define DEFAULT_SAT_SOLVER        "zchaff"
00182 #else
00183 #define DEFAULT_SAT_SOLVER        (char*)NULL
00184 #endif
00185 #endif
00186 
00192 #define OPT_USER_POV_NULL_STRING  "" /* user pov of the null string */
00193 
00199 #define DEFAULT_OREG_JUSTICE_EMPTINESS_BDD_ALGORITHM \
00200   BDD_OREG_JUSTICE_EMPTINESS_BDD_ALGORITHM_EL_BWD
00201 
00207 #define DEFAULT_SHOW_DEFINES_IN_TRACES true
00208 
00214 #define DEFAULT_SHOW_DEFINES_WITH_NEXT true
00215 
00221 #define DEFAULT_USE_COI_SIZE_SORTING true
00222 
00228 #define DEFAULT_BDD_ENCODE_WORD_BITS true
00229 
00235 typedef enum {
00236   FORWARD,
00237   BACKWARD,
00238   FORWARD_BACKWARD,
00239   BDD_BMC
00240 } Check_Strategy;
00241 
00247 #define DEFAULT_INVAR_CHECK_STRATEGY FORWARD
00248 
00254 typedef enum {
00255   ZIGZAG_HEURISTIC,
00256   SMALLEST_BDD_HEURISTIC
00257 } FB_Heuristic;
00258 
00264 #define DEFAULT_FORWARD_BACKWARD_ANALYSIS_HEURISTIC ZIGZAG_HEURISTIC
00265 
00271 typedef enum {
00272   STEPS_HEURISTIC,
00273   SIZE_HEURISTIC
00274 } Bdd2bmc_Heuristic;
00275 
00281 #define DEFAULT_BDD2BMC_HEURISTIC STEPS_HEURISTIC
00282 
00288 #define DEFAULT_DAGGIFIER_ENABLED true
00289 
00295 #define DEFAULT_DAGGIFIER_COUNTER_THS 3
00296 
00302 #define DEFAULT_DAGGIFIER_DEPTH_THS 2
00303 
00309 #define DEFAULT_BDD2BMC_HEURISTIC_THRESHOLD 10
00310 
00316 #define APPEND_CLUSTERS_VISIBLE 0
00317 
00323 #define PROGRAM_NAME      "program_name"
00324 
00330 #define PROGRAM_PATH      "program_path"
00331 
00337 #define INPUT_FILE        "input_file"
00338 
00344 #define SCRIPT_FILE       "script_file"
00345 
00351 #define INPUT_ORDER_FILE  "input_order_file"
00352 
00358 #define OUTPUT_ORDER_FILE "output_order_file"
00359 
00365 #define TRANS_ORDER_FILE  "trans_order_file"
00366 
00372 #define OUTPUT_FLATTEN_MODEL_FILE "output_flatten_model_file"
00373 
00379 #define OUTPUT_BOOLEAN_MODEL_FILE "output_boolean_model_file"
00380 
00386 #define OUTPUT_WORD_FORMAT "output_word_format"
00387 
00393 #define BACKWARD_COMPATIBILITY "backward_compatibility"
00394 
00400 #define TYPE_CHECKING_WARNING_ON "type_checking_warning_on"
00401 
00407 #define VERBOSE_LEVEL     "verbose_level"
00408 
00414 #define RUN_CPP           "run_cpp"
00415 
00421 #define PP_LIST           "pp_list"
00422 
00428 #define SHOWN_STATES      "shown_states"
00429 
00435 #define IGNORE_SPEC       "ignore_spec"
00436 
00442 #define IGNORE_COMPUTE    "ignore_compute"
00443 
00449 #define IGNORE_LTLSPEC    "ignore_ltlspec"
00450 
00456 #define IGNORE_PSLSPEC    "ignore_pslspec"
00457 
00463 #define OPT_CHECK_FSM   "check_fsm"
00464 
00470 #define IGNORE_INVAR      "ignore_invar"
00471 
00477 #define FORWARD_SEARCH    "forward_search"
00478 
00484 #define LTL_TABLEAU_FORWARD_SEARCH "ltl_tableau_forward_search"
00485 
00491 #define PRINT_REACHABLE   "print_reachable"
00492 
00498 #define ENABLE_REORDER    "enable_reorder"
00499 
00505 #define REORDER_METHOD    "reorder_method"
00506 
00512 #define DYNAMIC_REORDER   "dynamic_reorder"
00513 
00519 #define ENABLE_SEXP2BDD_CACHING   "enable_sexp2bdd_caching"
00520 
00526 #define PARTITION_METHOD  "partition_method"
00527 
00533 #define CONJ_PART_THRESHOLD "conj_part_threshold"
00534 
00540 #define IMAGE_CLUSTER_SIZE "image_cluster_size"
00541 
00547 #define IGNORE_INIT_FILE  "ignore_init_file"
00548 
00554 #define AG_ONLY_SEARCH    "ag_only_search"
00555 
00561 #define CONE_OF_INFLUENCE "cone_of_influence"
00562 
00568 #define LIST_PROPERTIES "list_properties"
00569 
00575 #define PROP_PRINT_METHOD "prop_print_method"
00576 
00582 #define PROP_NO         "prop_no"
00583 
00589 #define A_SAT_SOLVER "sat_solver"
00590 
00596 #define IWLS95_PREORDER  "iwls95preorder"
00597 
00603 #define AFFINITY_CLUSTERING  "affinity"
00604 
00610 #define APPEND_CLUSTERS  "append_clusters"
00611 
00617 #define USE_REACHABLE_STATES  "use_reachable_states"
00618 
00624 #define USE_FAIR_STATES  "use_fair_states"
00625 
00631 #define COUNTER_EXAMPLES  "counter_examples"
00632 
00638 #define TRACES_HIDING_PREFIX  "traces_hiding_prefix"
00639 
00645 #define DEFAULT_TRACES_HIDING_PREFIX  "__"
00646 
00652 #define BDD_ENCODE_WORD_BITS "bdd_encode_word_bits"
00653 
00659 #define PP_CPP_PATH "pp_cpp_path"
00660 
00666 #define PP_M4_PATH "pp_m4_path"
00667 
00668 #if NUSMV_HAVE_REGEX_H
00669 
00675 #define TRACES_REGEXP  "traces_regexp"
00676 #endif
00677 
00683 #define DEFAULT_TRACE_PLUGIN  "default_trace_plugin"
00684 
00690 #define ON_FAILURE_SCRIPT_QUITS "on_failure_script_quits"
00691 
00697 #define WRITE_ORDER_DUMPS_BITS "write_order_dumps_bits"
00698 
00704 #define USE_ANSI_C_DIV_OP "use_ansi_c_div_op"
00705 
00711 #define VARS_ORD_TYPE "vars_order_type"
00712 
00718 #define BDD_STATIC_ORDER_HEURISTICS   "bdd_static_order_heuristics"
00719 
00725 #define RBC_CNF_ALGORITHM "rbc_rbc2cnf_algorithm"
00726 
00732 #define SYMB_INLINING "sexp_inlining"
00733 
00739 #define RBC_INLINING "rbc_inlining"
00740 
00746 #define RBC_INLINING_LAZY "rbc_inlining_lazy"
00747 
00753 #define SHOW_DEFINES_IN_TRACES "traces_show_defines"
00754 
00760 #define SHOW_DEFINES_WITH_NEXT "traces_show_defines_with_next"
00761 
00767 #define INVAR_CHECK_STRATEGY "check_invar_strategy"
00768 
00774 #define CHECK_INVAR_FB_HEURISTIC "check_invar_forward_backward_heuristic"
00775 
00781 #define CHECK_INVAR_BDDBMC_HEURISTIC "check_invar_bddbmc_heuristic"
00782 
00788 #define CHECK_INVAR_BDDBMC_HEURISTIC_THRESHOLD "check_invar_bddbmc_threshold"
00789 
00795 #define DAGGIFIER_ENABLED "daggifier_enabled"
00796 
00802 #define DAGGIFIER_COUNTER_THRESHOLD "daggifier_counter_threshold"
00803 
00809 #define DAGGIFIER_DEPTH_THRESHOLD "daggifier_depth_threshold"
00810 
00816 #define DAGGIFIER_STATISTICS "daggifier_statistics"
00817 
00823 #define OREG_JUSTICE_EMPTINESS_BDD_ALGORITHM    \
00824   "oreg_justice_emptiness_bdd_algorithm"
00825 
00831 #define USE_COI_SIZE_SORTING "use_coi_size_sorting"
00832 
00838 #define BATCH "batch"
00839 
00845 #define QUIET_MODE "quiet_mode"
00846 
00852 #define DISABLE_SYNTACTIC_CHECKS "disable_syntactic_checks"
00853 
00859 #define KEEP_SINGLE_VALUE_VARS "keep_single_value_vars"
00860 
00866 #define DEFAULT_SIMULATION_STEPS "default_simulation_steps"
00867 
00868 /* For modifying the behavior of ltl2smv to compact the fairness in
00869    one single justice constraint instead of possibly moer than one. */
00870 
00876 #define LTL2SMV_SINGLE_JUSTICE "ltl2smv_single_justice"
00877 
00883 #define DEFAULT_LTL2SMV_SINGLE_JUSTICE false
00884 
00890 #define BOOLEAN_CONVERSION_USES_PREDICATE_NORMALIZATION "boolean_conversion_uses_predicate_normalization"
00891 
00897 #define DEFAULT_BOOLEAN_CONVERSION_USES_PREDICATE_NORMALIZATION false
00898 
00899 /*---------------------------------------------------------------------------*/
00900 /* Type declarations                                                         */
00901 /*---------------------------------------------------------------------------*/
00902 
00909 typedef struct options_TAG*  options_ptr;
00910 
00916 void set_use_reachable_states(OptsHandler_ptr);
00917 
00923 void unset_use_reachable_states(OptsHandler_ptr);
00924 
00930 boolean opt_use_reachable_states(OptsHandler_ptr);
00931 
00937 void set_use_fair_states(OptsHandler_ptr);
00938 
00944 void unset_use_fair_states(OptsHandler_ptr);
00945 
00951 boolean opt_use_fair_states(OptsHandler_ptr);
00952 
00953 
00954 /*---------------------------------------------------------------------------*/
00955 /* Function prototypes                                                       */
00956 /*---------------------------------------------------------------------------*/
00957 
00963 void    set_pgm_name(OptsHandler_ptr, char *);
00964 
00970 void    reset_pgm_name(OptsHandler_ptr);
00971 
00977 char *  get_pgm_name(OptsHandler_ptr);
00978 
00984 void    set_script_file(OptsHandler_ptr, char *);
00985 
00991 void    reset_script_file(OptsHandler_ptr);
00992 
00998 char *  get_script_file(OptsHandler_ptr);
00999 
01005 void    set_pgm_path(OptsHandler_ptr, char *);
01006 
01012 void    reset_pgm_path(OptsHandler_ptr);
01013 
01019 char *  get_pgm_path(OptsHandler_ptr);
01020 
01026 void    set_input_file(OptsHandler_ptr, const char *);
01027 
01033 void    reset_input_file(OptsHandler_ptr);
01034 
01040 char *  get_input_file(OptsHandler_ptr);
01041 
01047 void    set_input_order_file(OptsHandler_ptr, char *);
01048 
01054 void    reset_input_order_file(OptsHandler_ptr);
01055 
01061 char *  get_input_order_file(OptsHandler_ptr);
01062 
01068 void    set_output_order_file(OptsHandler_ptr, char *);
01069 
01075 void    reset_output_order_file(OptsHandler_ptr);
01076 
01082 char *  get_output_order_file(OptsHandler_ptr);
01083 
01089 boolean is_default_order_file(OptsHandler_ptr opt);
01090 
01096 void    set_trans_order_file(OptsHandler_ptr, char *);
01097 
01103 void    reset_trans_order_file(OptsHandler_ptr);
01104 
01110 char *  get_trans_order_file(OptsHandler_ptr);
01111 
01117 boolean opt_trans_order_file(OptsHandler_ptr);
01118 
01124 void    set_output_flatten_model_file(OptsHandler_ptr, char *);
01125 
01131 void    reset_output_flatten_model_file(OptsHandler_ptr);
01132 
01138 char *  get_output_flatten_model_file(OptsHandler_ptr);
01139 
01145 void    set_output_boolean_model_file(OptsHandler_ptr, char *);
01146 
01152 void    reset_output_boolean_model_file(OptsHandler_ptr);
01153 
01159 char *  get_output_boolean_model_file(OptsHandler_ptr);
01160 
01166 void    set_output_word_format(OptsHandler_ptr, int i);
01167 
01173 int     get_output_word_format(OptsHandler_ptr);
01174 
01180 void    set_backward_comp(OptsHandler_ptr);
01181 
01187 void    unset_backward_comp(OptsHandler_ptr);
01188 
01194 boolean opt_backward_comp(OptsHandler_ptr);
01195 
01201 void    set_type_checking_warning_on(OptsHandler_ptr);
01202 
01208 void    unset_type_checking_warning_on(OptsHandler_ptr);
01209 
01215 boolean opt_type_checking_warning_on(OptsHandler_ptr);
01216 
01222 void    set_verbose_level(OptsHandler_ptr, int);
01223 
01229 int     get_verbose_level(OptsHandler_ptr);
01230 
01236 boolean opt_verbose_level_eq(OptsHandler_ptr, int);
01237 
01243 boolean opt_verbose_level_gt(OptsHandler_ptr, int);
01244 
01250 boolean opt_verbose_level_ge(OptsHandler_ptr, int);
01251 
01257 boolean opt_verbose_level_lt(OptsHandler_ptr, int);
01258 
01264 boolean opt_verbose_level_le(OptsHandler_ptr, int);
01265 
01271 void    set_pp_list(OptsHandler_ptr, char *, const NuSMVEnv_ptr env);
01272 
01278 char *  get_pp_list(OptsHandler_ptr);
01279 
01285 void    set_shown_states_level(OptsHandler_ptr, int);
01286 
01292 int     opt_shown_states_level(OptsHandler_ptr);
01293 
01299 void    set_ignore_spec(OptsHandler_ptr);
01300 
01306 void    unset_ignore_spec(OptsHandler_ptr);
01307 
01313 boolean opt_ignore_spec(OptsHandler_ptr);
01314 
01320 void    set_ignore_compute(OptsHandler_ptr);
01321 
01327 void    unset_ignore_compute(OptsHandler_ptr);
01328 
01334 boolean opt_ignore_compute(OptsHandler_ptr);
01335 
01341 void    set_ignore_ltlspec(OptsHandler_ptr);
01342 
01348 void    unset_ignore_ltlspec(OptsHandler_ptr);
01349 
01355 boolean opt_ignore_ltlspec(OptsHandler_ptr);
01356 
01362 void    set_ignore_pslspec(OptsHandler_ptr);
01363 
01369 void    unset_ignore_pslspec(OptsHandler_ptr);
01370 
01376 boolean opt_ignore_pslspec(OptsHandler_ptr);
01377 
01383 void    set_check_fsm(OptsHandler_ptr);
01384 
01390 void    unset_check_fsm(OptsHandler_ptr);
01391 
01397 boolean opt_check_fsm(OptsHandler_ptr);
01398 
01404 void    set_ignore_invar(OptsHandler_ptr);
01405 
01411 void    unset_ignore_invar(OptsHandler_ptr);
01412 
01418 boolean opt_ignore_invar(OptsHandler_ptr);
01419 
01425 void    set_forward_search(OptsHandler_ptr);
01426 
01432 void    unset_forward_search(OptsHandler_ptr);
01433 
01439 boolean opt_forward_search(OptsHandler_ptr);
01440 
01446 void set_ltl_tableau_forward_search(OptsHandler_ptr opt);
01447 
01453 void unset_ltl_tableau_forward_search(OptsHandler_ptr opt);
01454 
01460 boolean opt_ltl_tableau_forward_search(OptsHandler_ptr opt);
01461 
01467 void    set_print_reachable(OptsHandler_ptr);
01468 
01474 void    unset_print_reachable(OptsHandler_ptr);
01475 
01481 boolean opt_print_reachable(OptsHandler_ptr);
01482 
01488 void    set_reorder(OptsHandler_ptr);
01489 
01495 void    unset_reorder(OptsHandler_ptr);
01496 
01502 boolean opt_reorder(OptsHandler_ptr);
01503 
01509 void    set_reorder_method(OptsHandler_ptr, unsigned int);
01510 
01516 unsigned int get_reorder_method(OptsHandler_ptr);
01517 
01523 void    set_dynamic_reorder(OptsHandler_ptr);
01524 
01530 void    unset_dynamic_reorder(OptsHandler_ptr);
01531 
01537 boolean opt_dynamic_reorder(OptsHandler_ptr);
01538 
01544 void    set_enable_sexp2bdd_caching(OptsHandler_ptr);
01545 
01551 void    unset_enable_sexp2bdd_caching(OptsHandler_ptr);
01552 
01558 boolean opt_enable_sexp2bdd_caching(OptsHandler_ptr);
01559 
01565 void    set_batch(OptsHandler_ptr);
01566 
01572 void    unset_batch(OptsHandler_ptr);
01573 
01579 boolean opt_batch(OptsHandler_ptr);
01580 
01586 void set_partition_method(OptsHandler_ptr, const TransType);
01587 
01593 TransType get_partition_method(OptsHandler_ptr opt);
01594 
01600 void    reset_partitioning_method(OptsHandler_ptr);
01601 
01607 void    set_monolithic(OptsHandler_ptr);
01608 
01614 void    set_conj_partitioning(OptsHandler_ptr);
01615 
01621 void    set_iwls95cp_partitioning(OptsHandler_ptr);
01622 
01628 boolean opt_monolithic(OptsHandler_ptr);
01629 
01635 boolean opt_conj_partitioning(OptsHandler_ptr);
01636 
01642 boolean opt_iwls95cp_partitioning(OptsHandler_ptr);
01643 
01649 void    set_conj_part_threshold(OptsHandler_ptr, int);
01650 
01656 void    reset_conj_part_threshold(OptsHandler_ptr);
01657 
01663 int     get_conj_part_threshold(OptsHandler_ptr);
01664 
01670 void set_image_cluster_size(OptsHandler_ptr, int);
01671 
01677 void reset_image_cluster_size(OptsHandler_ptr);
01678 
01684 int get_image_cluster_size(OptsHandler_ptr);
01685 
01691 void    set_ignore_init_file(OptsHandler_ptr);
01692 
01698 void    unset_ignore_init_file(OptsHandler_ptr);
01699 
01705 boolean opt_ignore_init_file(OptsHandler_ptr);
01706 
01712 void    set_ag_only(OptsHandler_ptr);
01713 
01719 void    unset_ag_only(OptsHandler_ptr);
01720 
01726 boolean opt_ag_only(OptsHandler_ptr);
01727 
01733 void    set_cone_of_influence(OptsHandler_ptr);
01734 
01740 void    unset_cone_of_influence(OptsHandler_ptr);
01741 
01747 boolean opt_cone_of_influence(OptsHandler_ptr);
01748 
01754 void    set_list_properties(OptsHandler_ptr);
01755 
01761 void    unset_list_properties(OptsHandler_ptr);
01762 
01768 boolean opt_list_properties(OptsHandler_ptr);
01769 
01775 void    set_pp_cpp_path(OptsHandler_ptr, const char *);
01776 
01782 void    reset_pp_cpp_path(OptsHandler_ptr);
01783 
01789 char *  get_pp_cpp_path(OptsHandler_ptr);
01790 
01796 void    set_pp_m4_path(OptsHandler_ptr, const char *);
01797 
01803 void    reset_pp_m4_path(OptsHandler_ptr);
01804 
01810 char *  get_pp_m4_path(OptsHandler_ptr);
01811 
01817 void set_prop_print_method(OptsHandler_ptr opt, const char* string);
01818 
01824 void reset_prop_print_method(OptsHandler_ptr opt);
01825 
01831 int get_prop_print_method(OptsHandler_ptr opt);
01832 
01838 void    set_prop_no(OptsHandler_ptr, int n);
01839 
01845 int     get_prop_no(OptsHandler_ptr);
01846 
01852 void print_partition_method(FILE *);
01853 
01859 void set_sat_solver(OptsHandler_ptr, const char*);
01860 
01866 const char* get_sat_solver(OptsHandler_ptr);
01867 
01873 boolean set_default_trace_plugin(OptsHandler_ptr opt, int plugin);
01874 
01880 int get_default_trace_plugin(OptsHandler_ptr opt);
01881 
01887 void set_iwls95_preorder(OptsHandler_ptr opt);
01888 
01894 void unset_iwls95_preorder(OptsHandler_ptr opt);
01895 
01901 boolean opt_iwls95_preorder(OptsHandler_ptr opt);
01902 
01908 void set_affinity(OptsHandler_ptr);
01909 
01915 void unset_affinity(OptsHandler_ptr);
01916 
01922 boolean opt_affinity(OptsHandler_ptr);
01923 
01929 void set_append_clusters(OptsHandler_ptr);
01930 
01936 void unset_append_clusters(OptsHandler_ptr);
01937 
01943 boolean opt_append_clusters(OptsHandler_ptr);
01944 
01945 /* counter examples */
01946 
01952 void set_counter_examples(OptsHandler_ptr);
01953 
01959 void unset_counter_examples(OptsHandler_ptr);
01960 
01966 boolean opt_counter_examples(OptsHandler_ptr);
01967 
01973 void set_traces_hiding_prefix(OptsHandler_ptr, const char*);
01974 
01980 const char* opt_traces_hiding_prefix(OptsHandler_ptr);
01981 
01987 void set_bdd_encoding_word_bits(OptsHandler_ptr opt);
01988 
01994 void unset_bdd_encoding_word_bits(OptsHandler_ptr opt);
01995 
02001 void reset_bdd_encoding_word_bits(OptsHandler_ptr opt);
02002 
02008 boolean opt_bdd_encoding_word_bits(OptsHandler_ptr opt);
02009 
02010 #if NUSMV_HAVE_REGEX_H
02011 
02017 const char* opt_traces_regexp(OptsHandler_ptr);
02018 
02024 boolean set_traces_regexp(OptsHandler_ptr, const char*);
02025 #endif
02026 
02027 /* others */
02028 
02034 void set_on_failure_script_quits(OptsHandler_ptr);
02035 
02041 void unset_on_failure_script_quits(OptsHandler_ptr);
02042 
02048 boolean opt_on_failure_script_quits(OptsHandler_ptr);
02049 
02055 void set_write_order_dumps_bits(OptsHandler_ptr);
02056 
02062 void unset_write_order_dumps_bits(OptsHandler_ptr);
02063 
02069 boolean opt_write_order_dumps_bits(OptsHandler_ptr);
02070 
02076 void unset_use_ansi_c_div_op(OptsHandler_ptr opt);
02077 
02083 boolean opt_use_ansi_c_div_op(OptsHandler_ptr opt);
02084 
02090 void set_vars_order_type(OptsHandler_ptr, VarsOrdType);
02091 
02097 VarsOrdType get_vars_order_type(OptsHandler_ptr);
02098 
02104 void set_bdd_static_order_heuristics(OptsHandler_ptr, BddSohEnum value);
02105 
02111 BddSohEnum get_bdd_static_order_heuristics(OptsHandler_ptr);
02112 
02113 /* inlining */
02114 
02120 void set_symb_inlining(OptsHandler_ptr opt);
02121 
02127 void unset_symb_inlining(OptsHandler_ptr opt);
02128 
02134 boolean opt_symb_inlining(OptsHandler_ptr opt);
02135 
02141 void set_rbc_inlining(OptsHandler_ptr opt);
02142 
02148 void unset_rbc_inlining(OptsHandler_ptr opt);
02149 
02155 boolean opt_rbc_inlining(OptsHandler_ptr opt);
02156 
02162 void set_rbc_inlining_lazy(OptsHandler_ptr opt);
02163 
02169 void unset_rbc_inlining_lazy(OptsHandler_ptr opt);
02170 
02176 boolean opt_rbc_inlining_lazy(OptsHandler_ptr opt);
02177 
02183 void set_use_coi_size_sorting(OptsHandler_ptr opt);
02184 
02190 void unset_use_coi_size_sorting(OptsHandler_ptr opt);
02191 
02197 boolean opt_use_coi_size_sorting(OptsHandler_ptr opt);
02198 
02204 void opt_disable_syntactic_checks(OptsHandler_ptr opt);
02205 
02211 void opt_enable_syntactic_checks(OptsHandler_ptr opt);
02212 
02218 boolean opt_syntactic_checks_disabled(OptsHandler_ptr opt);
02219 
02225 void set_keep_single_value_vars(OptsHandler_ptr opt);
02226 
02232 void unset_keep_single_value_vars(OptsHandler_ptr opt);
02233 
02239 boolean opt_keep_single_value_vars(OptsHandler_ptr opt);
02240 
02246 void set_show_defines_in_traces(OptsHandler_ptr opt);
02247 
02253 void unset_show_defines_in_traces(OptsHandler_ptr opt);
02254 
02260 boolean opt_show_defines_in_traces(OptsHandler_ptr opt);
02261 
02267 void set_show_defines_with_next(OptsHandler_ptr opt);
02268 
02274 void unset_show_defines_with_next(OptsHandler_ptr opt);
02275 
02281 boolean opt_show_defines_with_next(OptsHandler_ptr opt);
02282 
02288 void
02289 set_check_invar_strategy(OptsHandler_ptr opt, Check_Strategy strategy);
02290 
02296 Check_Strategy opt_check_invar_strategy(OptsHandler_ptr opt);
02297 
02303 const char* opt_check_invar_strategy_as_string(OptsHandler_ptr opt);
02304 
02310 void
02311 set_check_invar_fb_heuristic(OptsHandler_ptr opt, FB_Heuristic strategy);
02312 
02318 FB_Heuristic opt_check_invar_fb_heuristic(OptsHandler_ptr opt);
02319 
02325 const char* opt_check_invar_fb_heuristic_as_string(OptsHandler_ptr opt);
02326 
02332 void
02333 set_check_invar_bddbmc_heuristic(OptsHandler_ptr opt,
02334                                  Bdd2bmc_Heuristic strategy);
02335 
02341 Bdd2bmc_Heuristic
02342 opt_check_invar_bddbmc_heuristic(OptsHandler_ptr opt);
02343 
02349 const char*
02350 opt_check_invar_bddbmc_heuristic_as_string(OptsHandler_ptr opt);
02351 
02357 void
02358 set_check_invar_bddbmc_heuristic_threshold(OptsHandler_ptr opt, int t);
02359 
02365 int
02366 opt_check_invar_bddbmc_heuristic_threshold(OptsHandler_ptr opt);
02367 
02368 /* Daggifier on/off */
02369 
02375 boolean opt_is_daggifier_enabled(OptsHandler_ptr opt);
02376 
02382 void opt_enable_daggifier(OptsHandler_ptr opt);
02383 
02389 void opt_disable_daggifier(OptsHandler_ptr opt);
02390 
02396 int opt_get_daggifier_counter_threshold(OptsHandler_ptr opt);
02397 
02403 void opt_set_daggifier_counter_threshold(OptsHandler_ptr opt,
02404                                                 int x);
02405 
02411 int opt_get_daggifier_depth_threshold(OptsHandler_ptr opt);
02412 
02418 void opt_set_daggifier_depth_threshold(OptsHandler_ptr opt,
02419                                               int x);
02420 
02426 boolean opt_get_quiet_mode(OptsHandler_ptr opt);
02427 
02433 void set_quiet_mode(OptsHandler_ptr opt);
02434 
02440 void unset_quiet_mode(OptsHandler_ptr opt);
02441 
02442 /* Daggifier statistics */
02443 
02449 boolean opt_get_daggifier_statistics(OptsHandler_ptr opt);
02450 
02456 void set_daggifier_statistics(OptsHandler_ptr opt);
02457 
02463 void unset_daggifier_statistics(OptsHandler_ptr opt);
02464 
02465 /* different BDD-based algorithms to check language emptiness for
02466    omega-regular properties */
02467 BddOregJusticeEmptinessBddAlgorithmType
02468   get_oreg_justice_emptiness_bdd_algorithm(OptsHandler_ptr opt);
02469 void set_oreg_justice_emptiness_bdd_algorithm
02470 (OptsHandler_ptr opt, BddOregJusticeEmptinessBddAlgorithmType alg);
02471 void reset_oreg_justice_emptiness_bdd_algorithm
02472 (OptsHandler_ptr opt);
02473 
02474 /* RBC2CNF */
02475 
02481 void
02482 set_rbc2cnf_algorithm(OptsHandler_ptr opt, Be_CnfAlgorithm alg);
02483 
02489 void
02490 unset_rbc2cnf_algorithm(OptsHandler_ptr opt);
02491 
02497 Be_CnfAlgorithm
02498 get_rbc2cnf_algorithm(OptsHandler_ptr opt);
02499 
02505 void set_default_simulation_steps(OptsHandler_ptr, int);
02506 
02512 void reset_default_simulation_steps(OptsHandler_ptr);
02513 
02519 int get_default_simulation_steps(OptsHandler_ptr);
02520 
02526 void set_ltl2smv_single_justice(OptsHandler_ptr opt);
02527 
02533 void unset_ltl2smv_single_justice(OptsHandler_ptr opt);
02534 
02540 boolean opt_ltl2smv_single_justice(OptsHandler_ptr opt);
02541 
02547 void set_boolconv_uses_prednorm(OptsHandler_ptr opt);
02548 
02554 void unset_boolconv_uses_prednorm(OptsHandler_ptr opt);
02555 
02561 boolean opt_boolconv_uses_prednorm(OptsHandler_ptr opt);
02562 
02563 #endif /* __NUSMV_CORE_OPT_OPT_H__ */