Module AltErgoLib.Options

val fmt : Stdlib.Format.formatter

setter functions *********************************************************

val set_debug : bool -> unit

setters for debug flags

val set_debug_cc : bool -> unit
val set_debug_gc : bool -> unit
val set_debug_use : bool -> unit
val set_debug_uf : bool -> unit
val set_debug_fm : bool -> unit
val set_debug_sum : bool -> unit
val set_debug_adt : bool -> unit
val set_debug_arith : bool -> unit
val set_debug_bitv : bool -> unit
val set_debug_ac : bool -> unit
val set_debug_sat : bool -> unit
val set_debug_sat_simple : bool -> unit
val set_debug_typing : bool -> unit
val set_debug_constr : bool -> unit
val set_debug_arrays : bool -> unit
val set_debug_ite : bool -> unit
val set_debug_types : bool -> unit
val set_debug_combine : bool -> unit
val set_debug_unsat_core : bool -> unit
val set_debug_split : bool -> unit
val set_debug_matching : int -> unit
val set_debug_explanations : bool -> unit
val set_timers : bool -> unit
val set_profiling : float -> bool -> unit

additional setters

val set_type_only : bool -> unit
val set_type_smt2 : bool -> unit
val set_parse_only : bool -> unit
val set_frontend : string -> unit
val set_verbose : bool -> unit
val set_steps_bound : int -> unit
val set_age_bound : int -> unit
val set_no_user_triggers : bool -> unit
val set_triggers_var : bool -> unit
val set_nb_triggers : int -> unit
val set_greedy : bool -> unit
val set_no_Ematching : bool -> unit
val set_no_NLA : bool -> unit
val set_no_ac : bool -> unit
val set_normalize_instances : bool -> unit
val set_nocontracongru : bool -> unit
val set_term_like_pp : bool -> unit
val set_all_models : bool -> unit
val set_model : bool -> unit
val set_complete_model : bool -> unit
val set_interpretation : int -> unit
val set_max_split : Numbers.Q.t -> unit
val set_fm_cross_limit : Numbers.Q.t -> unit
val set_rewriting : bool -> unit
val set_unsat_core : bool -> unit
val set_rules : int -> unit
val set_restricted : bool -> unit
val set_bottom_classes : bool -> unit
val set_timelimit : float -> unit
val set_thread_yield : ( unit -> unit ) -> unit
val set_timeout : ( unit -> unit ) -> unit
val set_save_used_context : bool -> unit
val set_default_input_lang : string -> unit
val set_unsat_mode : bool -> unit
val set_inline_lets : bool -> unit
val set_file_for_js : string -> unit

getter functions *********************************************************

val debug : unit -> bool

getters for debug flags

val debug_warnings : unit -> bool
val debug_cc : unit -> bool
val debug_gc : unit -> bool
val debug_use : unit -> bool
val debug_uf : unit -> bool
val debug_fm : unit -> bool
val debug_fpa : unit -> int
val debug_sum : unit -> bool
val debug_adt : unit -> bool
val debug_arith : unit -> bool
val debug_bitv : unit -> bool
val debug_ac : unit -> bool
val debug_sat : unit -> bool
val debug_sat_simple : unit -> bool
val debug_typing : unit -> bool
val debug_constr : unit -> bool
val debug_arrays : unit -> bool
val debug_ite : unit -> bool
val debug_types : unit -> bool
val debug_combine : unit -> bool
val debug_unsat_core : unit -> bool
val debug_split : unit -> bool
val debug_matching : unit -> int
val debug_explanations : unit -> bool
val debug_triggers : unit -> bool
val enable_assertions : unit -> bool

additional getters

val disable_ites : unit -> bool
val disable_adts : unit -> bool
val enable_adts_cs : unit -> bool
val type_only : unit -> bool
val type_smt2 : unit -> bool
val parse_only : unit -> bool
val frontend : unit -> string
val steps_bound : unit -> int
val no_tcp : unit -> bool
val no_decisions : unit -> bool
val no_fm : unit -> bool
val no_theory : unit -> bool
val tighten_vars : unit -> bool
val age_bound : unit -> int
val no_user_triggers : unit -> bool
val triggers_var : unit -> bool
val nb_triggers : unit -> int
val max_multi_triggers_size : unit -> int
val verbose : unit -> bool
val greedy : unit -> bool
val no_Ematching : unit -> bool
val arith_matching : unit -> bool
val no_backjumping : unit -> bool
val no_NLA : unit -> bool
val no_ac : unit -> bool
val no_backward : unit -> bool
val no_sat_learning : unit -> bool
val sat_learning : unit -> bool
val nocontracongru : unit -> bool
val term_like_pp : unit -> bool
val all_models : unit -> bool
val model : unit -> bool
val interpretation : unit -> int
val debug_interpretation : unit -> bool
val complete_model : unit -> bool
val max_split : unit -> Numbers.Q.t
val fm_cross_limit : unit -> Numbers.Q.t
val rewriting : unit -> bool
val unsat_core : unit -> bool
val rules : unit -> int
val restricted : unit -> bool
val bottom_classes : unit -> bool
val timelimit : unit -> float
val timelimit_per_goal : unit -> bool
val interpretation_timelimit : unit -> float
val profiling : unit -> bool
val cumulative_time_profiling : unit -> bool
val profiling_period : unit -> float
val js_mode : unit -> bool
val case_split_policy : unit -> Util.case_split_policy
val preludes : unit -> string list
val instantiate_after_backjump : unit -> bool
val disable_weaks : unit -> bool
val default_input_lang : unit -> string
val answers_with_locs : unit -> bool
val unsat_mode : unit -> bool
val inline_lets : unit -> bool
val timers : unit -> bool

this option also yields true if profiling is set to true *

val replay : unit -> bool
val replay_used_context : unit -> bool
val replay_all_used_context : unit -> bool
val save_used_context : unit -> bool
val get_file : unit -> string
val get_session_file : unit -> string
val get_used_context_file : unit -> string
val sat_plugin : unit -> string
val parsers : unit -> string list
val inequalities_plugin : unit -> string
val profiling_plugin : unit -> string
val normalize_instances : unit -> bool
val sat_solver : unit -> Util.sat_solver
val cdcl_tableaux_inst : unit -> bool
val cdcl_tableaux_th : unit -> bool
val cdcl_tableaux : unit -> bool
val tableaux_cdcl : unit -> bool
val minimal_bj : unit -> bool
val enable_restarts : unit -> bool
val disable_flat_formulas_simplification : unit -> bool
val use_fpa : unit -> bool
val exec_thread_yield : unit -> unit

particular getters : functions that are immediately executed *************

val exec_timeout : unit -> unit
val tool_req : int -> string -> unit
module Time : sig ... end

Simple Timer module *

globals *

val cs_steps : unit -> int
val incr_cs_steps : unit -> unit
val (<>) : int -> int -> bool

open Options in every module to hide polymorphic versions of Pervasives *

val (=) : int -> int -> bool
val (<) : int -> int -> bool
val (>) : int -> int -> bool
val (<=) : int -> int -> bool
val (>=) : int -> int -> bool
val compare : int -> int -> int
val can_decide_on : string -> bool
val no_decisions_on__is_empty : unit -> bool
val set_is_gui : bool -> unit

extra *

val get_is_gui : unit -> bool
val parse_cmdline_arguments : unit -> unit