package alt-ergo-lib

  1. Overview
  2. Docs

Module AltErgoLib.OptionsSource

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

Sourceval set_debug : bool -> unit

setters for debug flags

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_max_split : Numbers.Q.t -> unit
Sourceval set_fm_cross_limit : Numbers.Q.t -> 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_default_input_lang : string -> 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

getters for debug flags

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

additional getters

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 max_split : unit -> Numbers.Q.t
Sourceval fm_cross_limit : unit -> Numbers.Q.t
Sourceval rewriting : unit -> bool
Sourceval unsat_core : unit -> bool
Sourceval rules : unit -> int
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 case_split_policy : unit -> Util.case_split_policy
Sourceval preludes : unit -> string list
Sourceval instantiate_after_backjump : unit -> bool
Sourceval disable_weaks : unit -> bool
Sourceval default_input_lang : unit -> string
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 sat_solver : unit -> Util.sat_solver
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 disable_flat_formulas_simplification : 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
Sourceval tool_req : int -> string -> unit
Sourcemodule Time : sig ... end

Simple Timer module *

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

extra *

Sourceval get_is_gui : unit -> bool
Sourceval parse_cmdline_arguments : unit -> unit