setter functions *********************************************************
Sourceval set_debug : bool -> unit Sourceval set_debug_cc : bool -> unit Sourceval set_debug_gc : bool -> unit Sourceval set_debug_use : bool -> unit Sourceval set_debug_uf : bool -> unit Sourceval set_debug_fm : bool -> unit Sourceval set_debug_sum : bool -> unit Sourceval set_debug_adt : bool -> unit Sourceval set_debug_arith : bool -> unit Sourceval set_debug_bitv : bool -> unit Sourceval set_debug_ac : bool -> unit Sourceval set_debug_sat : bool -> unit Sourceval set_debug_sat_simple : bool -> unit Sourceval set_debug_typing : bool -> unit Sourceval set_debug_constr : bool -> unit Sourceval set_debug_arrays : bool -> unit Sourceval set_debug_ite : bool -> unit Sourceval set_debug_types : bool -> unit Sourceval set_debug_combine : bool -> unit Sourceval set_debug_unsat_core : bool -> unit Sourceval set_debug_split : bool -> unit Sourceval set_debug_matching : int -> unit Sourceval set_debug_explanations : bool -> unit Sourceval set_timers : bool -> unit Sourceval set_profiling : float -> bool -> unit additional setters
Sourceval set_type_only : bool -> unit Sourceval set_type_smt2 : bool -> unit Sourceval set_parse_only : bool -> unit Sourceval set_frontend : string -> unit Sourceval set_verbose : bool -> unit Sourceval set_steps_bound : int -> unit Sourceval set_age_bound : int -> unit Sourceval set_no_user_triggers : bool -> unit Sourceval set_triggers_var : bool -> unit Sourceval set_nb_triggers : int -> unit Sourceval set_greedy : bool -> unit Sourceval set_no_Ematching : bool -> unit Sourceval set_no_NLA : bool -> unit Sourceval set_no_ac : bool -> unit Sourceval set_normalize_instances : bool -> unit Sourceval set_nocontracongru : bool -> unit Sourceval set_term_like_pp : bool -> unit Sourceval set_all_models : bool -> unit Sourceval set_model : bool -> unit Sourceval set_complete_model : bool -> unit Sourceval set_interpretation : int -> unit Sourceval set_rewriting : bool -> unit Sourceval set_unsat_core : bool -> unit Sourceval set_rules : int -> unit Sourceval set_restricted : bool -> unit Sourceval set_bottom_classes : bool -> unit Sourceval set_timelimit : float -> unit Sourceval set_thread_yield : (unit -> unit) -> unit Sourceval set_timeout : (unit -> unit) -> unit Sourceval set_save_used_context : bool -> unit Sourceval set_unsat_mode : bool -> unit Sourceval set_inline_lets : bool -> unit Sourceval set_file_for_js : string -> unit getter functions *********************************************************
Sourceval debug : unit -> bool Sourceval debug_warnings : unit -> bool Sourceval debug_cc : unit -> bool Sourceval debug_gc : unit -> bool Sourceval debug_use : unit -> bool Sourceval debug_uf : unit -> bool Sourceval debug_fm : unit -> bool Sourceval debug_fpa : unit -> int Sourceval debug_sum : unit -> bool Sourceval debug_adt : unit -> bool Sourceval debug_arith : unit -> bool Sourceval debug_bitv : unit -> bool Sourceval debug_ac : unit -> bool Sourceval debug_sat : unit -> bool Sourceval debug_sat_simple : unit -> bool Sourceval debug_typing : unit -> bool Sourceval debug_constr : unit -> bool Sourceval debug_arrays : unit -> bool Sourceval debug_ite : unit -> bool Sourceval debug_types : unit -> bool Sourceval debug_combine : unit -> bool Sourceval debug_unsat_core : unit -> bool Sourceval debug_split : unit -> bool Sourceval debug_matching : unit -> int Sourceval debug_explanations : unit -> bool Sourceval debug_triggers : unit -> bool Sourceval enable_assertions : unit -> bool Sourceval disable_ites : unit -> bool Sourceval disable_adts : unit -> bool Sourceval enable_adts_cs : unit -> bool Sourceval type_only : unit -> bool Sourceval type_smt2 : unit -> bool Sourceval parse_only : unit -> bool Sourceval frontend : unit -> string Sourceval steps_bound : unit -> int Sourceval no_tcp : unit -> bool Sourceval no_decisions : unit -> bool Sourceval no_fm : unit -> bool Sourceval no_theory : unit -> bool Sourceval tighten_vars : unit -> bool Sourceval age_bound : unit -> int Sourceval no_user_triggers : unit -> bool Sourceval triggers_var : unit -> bool Sourceval nb_triggers : unit -> int Sourceval max_multi_triggers_size : unit -> int Sourceval verbose : unit -> bool Sourceval greedy : unit -> bool Sourceval no_Ematching : unit -> bool Sourceval arith_matching : unit -> bool Sourceval no_backjumping : unit -> bool Sourceval no_NLA : unit -> bool Sourceval no_ac : unit -> bool Sourceval no_backward : unit -> bool Sourceval no_sat_learning : unit -> bool Sourceval sat_learning : unit -> bool Sourceval nocontracongru : unit -> bool Sourceval term_like_pp : unit -> bool Sourceval all_models : unit -> bool Sourceval model : unit -> bool Sourceval interpretation : unit -> int Sourceval debug_interpretation : unit -> bool Sourceval complete_model : unit -> bool Sourceval rewriting : unit -> bool Sourceval unsat_core : unit -> bool Sourceval restricted : unit -> bool Sourceval bottom_classes : unit -> bool Sourceval timelimit : unit -> float Sourceval timelimit_per_goal : unit -> bool Sourceval interpretation_timelimit : unit -> float Sourceval profiling : unit -> bool Sourceval cumulative_time_profiling : unit -> bool Sourceval profiling_period : unit -> float Sourceval js_mode : unit -> bool Sourceval preludes : unit -> string list Sourceval instantiate_after_backjump : unit -> bool Sourceval disable_weaks : unit -> bool Sourceval answers_with_locs : unit -> bool Sourceval unsat_mode : unit -> bool Sourceval inline_lets : unit -> bool Sourceval timers : unit -> bool this option also yields true if profiling is set to true *
Sourceval replay : unit -> bool Sourceval replay_used_context : unit -> bool Sourceval replay_all_used_context : unit -> bool Sourceval save_used_context : unit -> bool Sourceval get_file : unit -> string Sourceval get_session_file : unit -> string Sourceval get_used_context_file : unit -> string Sourceval sat_plugin : unit -> string Sourceval parsers : unit -> string list Sourceval inequalities_plugin : unit -> string Sourceval profiling_plugin : unit -> string Sourceval normalize_instances : unit -> bool Sourceval cdcl_tableaux_inst : unit -> bool Sourceval cdcl_tableaux_th : unit -> bool Sourceval cdcl_tableaux : unit -> bool Sourceval tableaux_cdcl : unit -> bool Sourceval minimal_bj : unit -> bool Sourceval enable_restarts : unit -> bool Sourceval use_fpa : unit -> bool Sourceval exec_thread_yield : unit -> unit particular getters : functions that are immediately executed *************
Sourceval exec_timeout : unit -> unit globals *
Sourceval cs_steps : unit -> int Sourceval incr_cs_steps : unit -> unit Sourceval (<>) : int -> int -> bool open Options in every module to hide polymorphic versions of Pervasives *
Sourceval (=) : int -> int -> bool Sourceval (<) : int -> int -> bool Sourceval (>) : int -> int -> bool Sourceval (<=) : int -> int -> bool Sourceval (>=) : int -> int -> bool Sourceval compare : int -> int -> int Sourceval can_decide_on : string -> bool Sourceval no_decisions_on__is_empty : unit -> bool Sourceval set_is_gui : bool -> unit Sourceval get_is_gui : unit -> bool Sourceval parse_cmdline_arguments : unit -> unit