package alt-ergo-lib

  1. Overview
  2. Docs
package alt-ergo-lib
Legend:
Library
Module
Module type
Parameter
Class
Class type

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
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct