package alt-ergo-lib

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

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
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