package alt-ergo-lib

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

Options module used at start-up to parse the command line

Some values are defined once and for all in the options module since it will be opened in each module. Even though it's not a good habit to do so this will stay like this until the next PR that's supposed to clean some parts of the program

type model =
  1. | MNone
  2. | MDefault
  3. | MAll
  4. | MComplete

Type used to describe the type of models wanted

type instantiation_heuristic =
  1. | INormal
  2. | IAuto
  3. | IGreedy

Type used to describe the type of heuristic for instantiation wanted

type input_format =
  1. | Native
    (*

    Native Alt-Ergo format

    *)
  2. | Smtlib2
    (*

    Smtlib default format

    *)
  3. | Why3
    (*

    Why3 file format

    *)
  4. | Unknown of string
    (*

    Unknown file format

    *)

Type used to describe the type of input wanted by set_input_format

type output_format = input_format

Type used to describe the type of output wanted by set_output_format

type known_status =
  1. | Status_Sat
  2. | Status_Unsat
  3. | Status_Unknown
  4. | Status_Undefined of string

Type used to register the status, if known, of the input problem

Setter functions

Setters for debug flags

val set_debug : bool -> unit

Set debug accessible with get_debug

val set_debug_ac : bool -> unit

Set debug_ac accessible with get_debug_ac

val set_debug_adt : bool -> unit

Set debug_adt accessible with get_debug_adt

val set_debug_arith : bool -> unit

Set debug_arith accessible with get_debug_arith

val set_debug_arrays : bool -> unit

Set debug_arrays accessible with get_debug_arrays

val set_debug_bitv : bool -> unit

Set debug_bitv accessible with get_debug_bitv

val set_debug_cc : bool -> unit

Set debug_cc accessible with get_debug_cc

val set_debug_combine : bool -> unit

Set debug_combine accessible with get_debug_combine

val set_debug_constr : bool -> unit

Set debug_constr accessible with get_debug_constr

val set_debug_explanations : bool -> unit

Set debug_explanations accessible with get_debug_explanations

val set_debug_fm : bool -> unit

Set debug_fm accessible with get_debug_fm

val set_debug_fpa : int -> unit

Set debug_fpa accessible with get_debug_fpa

val set_debug_gc : bool -> unit

Set debug_gc accessible with get_debug_gc

val set_debug_interpretation : bool -> unit

Set debug_interpretation accessible with get_debug_interpretation

val set_debug_ite : bool -> unit

Set debug_ite accessible with get_debug_ite

val set_debug_matching : int -> unit

Set debug_matching accessible with get_debug_matching

Possible values are

  1. Disabled
  2. Light
  3. Full
val set_debug_sat : bool -> unit

Set debug_sat accessible with get_debug_sat

val set_debug_split : bool -> unit

Set debug_split accessible with get_debug_split

val set_debug_sum : bool -> unit

Set debug_sum accessible with get_debug_sum

val set_debug_triggers : bool -> unit

Set debug_triggers accessible with get_debug_triggers

val set_debug_types : bool -> unit

Set debug_types accessible with get_debug_types

val set_debug_typing : bool -> unit

Set debug_typing accessible with get_debug_typing

val set_debug_uf : bool -> unit

Set debug_uf accessible with get_debug_uf

val set_debug_unsat_core : bool -> unit

Set debug_unsat_core accessible with get_debug_unsat_core

val set_debug_use : bool -> unit

Set debug_use accessible with get_debug_use

val set_debug_warnings : bool -> unit

Set debug_warnings accessible with get_debug_warnings

val set_profiling : bool -> float -> unit

Set profiling accessible with get_profiling

val set_timers : bool -> unit

Set timers accessible with get_timers

Additional setters

val set_type_only : bool -> unit

Set type_only accessible with get_type_only

val set_age_bound : int -> unit

Set age_bound accessible with get_age_bound

val set_bottom_classes : bool -> unit

Set bottom_classes accessible with get_bottom_classes

val set_fm_cross_limit : Numbers.Q.t -> unit

Set fm_cross_limit accessible with get_fm_cross_limit

val set_frontend : string -> unit

Set frontend accessible with get_frontend

val set_instantiation_heuristic : instantiation_heuristic -> unit

Set instantiation_heuristic accessible with get_instantiation_heuristic

val set_inline_lets : bool -> unit

Set inline_lets accessible with get_inline_lets

val set_input_format : input_format -> unit

Set input_format accessible with get_input_format

val set_interpretation : int -> unit

Set interpretation accessible with get_interpretation

Possible values are :

  1. Unknown
  2. Before instantiation
  3. Before every decision or instantiation

A negative value (-1, -2, or -3) will disable interpretation display.

val set_max_split : Numbers.Q.t -> unit

Set max_split accessible with get_max_split

val set_model : model -> unit

Set model accessible with get_model

Possible values are :

  • Default
  • Complete
  • All
val set_nb_triggers : int -> unit

Set nb_triggers accessible with get_nb_triggers

val set_no_ac : bool -> unit

Set no_ac accessible with get_no_ac

val set_no_contracongru : bool -> unit

Set no_contragru accessible with get_no_contragru

val set_no_ematching : bool -> unit

Set no_ematching accessible with get_no_ematching

val set_no_nla : bool -> unit

Set no_nla accessible with get_no_nla

val set_no_user_triggers : bool -> unit

Set no_user_triggers accessible with get_no_user_triggers

val set_normalize_instances : bool -> unit

Set normalize_instances accessible with get_normalize_instances

val set_output_format : output_format -> unit

Set output_format accessible with get_output_format

val set_parse_only : bool -> unit

Set parse_only accessible with get_parse_only

val set_restricted : bool -> unit

Set restricted accessible with get_restricted

val set_rewriting : bool -> unit

Set rewriting accessible with get_rewriting

val set_rule : int -> unit

Set rule accessible with get_rule

val set_save_used_context : bool -> unit

Set save_used_context accessible with get_save_used_context

val set_steps_bound : int -> unit

Set steps_bound accessible with get_steps_bound

val set_term_like_pp : bool -> unit

Set term_like_pp accessible with get_term_like_pp

val set_thread_yield : (unit -> unit) -> unit

Set thread_yield accessible with get_thread_yield

val set_timelimit : float -> unit

Set timelimit accessible with get_timelimit

val set_timeout : (unit -> unit) -> unit

Set timeout accessible with get_timeout

val set_triggers_var : bool -> unit

Set triggers_var accessible with get_triggers_var

val set_type_smt2 : bool -> unit

Set type_smt2 accessible with get_type_smt2

val set_unsat_core : bool -> unit

Set unsat_core accessible with get_unsat_core

val set_verbose : bool -> unit

Set verbose accessible with get_verbose

val set_status : string -> unit

Set status accessible with get_status

val set_file : string -> unit

Set file accessible with get_file

val set_file_for_js : string -> unit

Updates the filename to be parsed and sets a js_mode flag

Setters used by parse_command

val set_case_split_policy : Util.case_split_policy -> unit

Set case_split_policy accessible with get_case_split_policy

val set_enable_adts_cs : bool -> unit

Set enable_adts_cs accessible with get_enable_adts_cs

val set_replay : bool -> unit

Set replay accessible with get_replay

val set_replay_all_used_context : bool -> unit

Set replay_all_used_context accessible with get_replay_all_used_context

val set_replay_used_context : bool -> unit

Set replay_used_context accessible with get_replay_used_context

val set_answers_with_loc : bool -> unit

Set answers_with_loc accessible with get_answers_with_loc

val set_output_with_colors : bool -> unit

Set output_with_colors accessible with get_output_with_colors

val set_output_with_headers : bool -> unit

Set output_with_headers accessible with get_output_with_headers

val set_output_with_formatting : bool -> unit

Set output_with_formatting accessible with get_output_with_formatting

val set_output_with_forced_flush : bool -> unit

Set output_with_forced_flush accessible with get_output_with_forced_flush

val set_infer_input_format : 'a option -> unit

Set infer_input_format accessible with get_infer_input_format

val set_infer_output_format : 'a option -> unit

Set infer_output_format accessible with get_infer_output_format

val set_parsers : string list -> unit

Set parsers accessible with get_parsers

val set_preludes : string list -> unit

Set preludes accessible with get_preludes

val set_disable_weaks : bool -> unit

Set disable_weaks accessible with get_disable_weaks

val set_enable_assertions : bool -> unit

Set enable_assertions accessible with get_enable_assertions

val set_warning_as_error : bool -> unit

Set warning_as_error accessible with get_warning_as_error

val set_timelimit_interpretation : float -> unit

Set timelimit_interpretation accessible with get_timelimit_interpretation

val set_timelimit_per_goal : bool -> unit

Set timelimit_per_goal accessible with get_timelimit_per_goal

val set_cumulative_time_profiling : bool -> unit

Set cumulative_time_profiling accessible with get_cumulative_time_profiling

val set_profiling_period : float -> unit

Set profiling_period accessible with get_profiling_period

val set_profiling_plugin : string -> unit

Set profiling_plugin accessible with get_profiling_plugin

val set_instantiate_after_backjump : bool -> unit

Set instantiate_after_backjump accessible with get_instantiate_after_backjump

val set_max_multi_triggers_size : int -> unit

Set max_multi_triggers_size accessible with get_max_multi_triggers_size

val set_arith_matching : bool -> unit

Set arith_matching accessible with get_arith_matching

val set_cdcl_tableaux_inst : bool -> unit

Set cdcl_tableaux_inst accessible with get_cdcl_tableaux_inst

val set_cdcl_tableaux_th : bool -> unit

Set cdcl_tableaux_th accessible with get_cdcl_tableaux_th

val set_disable_flat_formulas_simplification : bool -> unit

Set disable_flat_formulas_simplification accessible with get_disable_flat_formulas_simplification

val set_enable_restarts : bool -> unit

Set enable_restarts accessible with get_enable_restarts

val set_minimal_bj : bool -> unit

Set minimal_bj accessible with get_minimal_bj

val set_no_backjumping : bool -> unit

Set no_backjumping accessible with get_no_backjumping

val set_no_backward : bool -> unit

Set no_backward accessible with get_no_backward

val set_no_decisions : bool -> unit

Set no_decisions accessible with get_no_decisions

val set_no_decisions_on : Util.SS.t -> unit

Set no_decisions_on accessible with get_no_decisions_on

val set_no_sat_learning : bool -> unit

Set no_sat_learning accessible with get_no_sat_learning

val set_sat_plugin : string -> unit

Set sat_plugin accessible with get_sat_plugin

val set_sat_solver : Util.sat_solver -> unit

Set sat_solver accessible with get_sat_solver

val set_tableaux_cdcl : bool -> unit

Set tableaux_cdcl accessible with get_tableaux_cdcl

val set_disable_ites : bool -> unit

Set disable_ites accessible with get_disable_ites

val set_disable_adts : bool -> unit

Set disable_adts accessible with get_disable_adts

val set_inequalities_plugin : string -> unit

Set inequalities_plugin accessible with get_inequalities_plugin

val set_no_fm : bool -> unit

Set no_fm accessible with get_no_fm

val set_no_tcp : bool -> unit

Set no_tcp accessible with get_no_tcp

val set_no_theory : bool -> unit

Set no_theory accessible with get_no_theory

val set_tighten_vars : bool -> unit

Set tighten_vars accessible with get_tighten_vars

val set_use_fpa : bool -> unit

Set use_fpa accessible with get_use_fpa

val set_session_file : string -> unit

Set session_file accessible with get_session_file

val set_used_context_file : string -> unit

Set used_context_file accessible with get_used_context_file

Getter functions

Getters for debug flags

Default value for all the debug flags is false

val get_debug : unit -> bool

Get the debugging flag.

val get_debug_warnings : unit -> bool

Get the debugging flag of warnings.

val get_debug_cc : unit -> bool

Get the debugging flag of cc.

val get_debug_gc : unit -> bool

Prints some debug info about the GC's activity.

val get_debug_use : unit -> bool

Get the debugging flag of use.

val get_debug_uf : unit -> bool

Get the debugging flag of uf.

val get_debug_fm : unit -> bool

Get the debugging flag of inequalities.

val get_debug_fpa : unit -> int

Get the debugging value of floating-point.

Default to 0.

val get_debug_sum : unit -> bool

Get the debugging flag of Sum.

val get_debug_adt : unit -> bool

Get the debugging flag of ADTs.

val get_debug_arith : unit -> bool

Get the debugging flag of Arith (without fm).

val get_debug_bitv : unit -> bool

Get the debugging flag of bitv.

val get_debug_ac : unit -> bool

Get the debugging flag of ac.

val get_debug_sat : unit -> bool

Get the debugging flag of SAT.

val get_debug_typing : unit -> bool

Get the debugging flag of typing.

val get_debug_constr : unit -> bool

Get the debugging flag of constructors.

val get_debug_arrays : unit -> bool

Get the debugging flag of arrays.

val get_debug_ite : unit -> bool

Get the debugging flag of ite.

val get_debug_types : unit -> bool

Get the debugging flag of types.

val get_debug_combine : unit -> bool

Get the debugging flag of combine.

val get_debug_unsat_core : unit -> bool

Replay unsat-cores produced by get_unsat_core. The option implies get_unsat_core returns true.

val get_debug_split : unit -> bool

Get the debugging flag of case-split analysis.

val get_debug_matching : unit -> int

Get the debugging flag of E-matching

Possible values are

  1. Disabled
  2. Light
  3. Full
val get_debug_explanations : unit -> bool

Get the debugging flag of explanations.

val get_debug_triggers : unit -> bool

Get the debugging flag of triggers.

val get_debug_interpretation : unit -> bool

Get the debugging flag for interpretation generatation.

Additional getters

Case-split options
val get_case_split_policy : unit -> Util.case_split_policy

Value specifying the case-split policy.

Possible values are :

  • after-theory-assume
  • before-matching
  • after-matching

Default to after-theory-assume

val get_enable_adts_cs : unit -> bool

true if case-split for Algebraic Datatypes theory is enabled.

Default to false

val get_max_split : unit -> Numbers.Q.t

Valuget_e specifying the maximum size of case-split.

Default to 1_000_000

Context options
val get_replay : unit -> bool

true if replay session will be saved in file_name.agr.

Default to false

val get_replay_all_used_context : unit -> bool

true if replay with all axioms and predicates saved in .used files of the current directory is enabled.

Default to false

val get_replay_used_context : unit -> bool

true if replay with axioms and predicates saved in .used file is enabled.

Default to false

val get_save_used_context : unit -> bool

true if used axioms and predicates will be saved in a .used file. This option implies get_unsat_core returns true.

Default to false

Execution options
val get_answers_with_locs : unit -> bool

true if the locations of goals is shown when printing solver's answers.

Default to true

val get_output_with_colors : unit -> bool

true if the outputs are printed with colors

Default to true

val get_output_with_headers : unit -> bool

true if the outputs are printed with headers

Default to true

val get_output_with_formatting : unit -> bool

true if the outputs are printed with formatting rules

Default to true

val get_output_with_forced_flush : unit -> bool

true if the outputs are flushed at the end of every print

Default to true

val get_frontend : unit -> string

Valuget_e of the currently selected parsing and typing frontend.

Default to legacy

val get_input_format : unit -> input_format

Value specifying the default input format. Useful when the extension does not allow to automatically select a parser (eg. JS mode, GUI mode, ...). possible values are

  • native
  • smtlib2
  • why3

Default to Native

val get_infer_input_format : unit -> bool

true if Alt-Ergo infers automatically the input format according to the file extension. false if an input format is set with -i option

Default to true

val get_parse_only : unit -> bool

true if the program shall stop after parsing.

Default to false

val get_parsers : unit -> string list

List of registered parsers for Alt-Ergo.

Default to false

val get_preludes : unit -> string list

List of files that have be loaded as preludes.

Default to []

val get_type_only : unit -> bool

true if the program shall stop after typing.

Default to false

val get_type_smt2 : unit -> bool

true if the program shall stop after SMT2 typing.

Default to false

Internal options
val get_disable_weaks : unit -> bool

true if the GC is prevented from collecting hashconsed data structrures that are not reachable (useful for more determinism).

Default to false

val get_enable_assertions : unit -> bool

true if verification of some heavy invariants is enabled.

Default to false

val get_warning_as_error : unit -> bool

true if warning are set as error.

Default to false

Limit options
val get_age_bound : unit -> int

Value specifying the age limit bound.

Default to 50

val get_fm_cross_limit : unit -> Numbers.Q.t

Value specifying the limit above which Fourier-Motzkin variables elimination steps that may produce a number of inequalities that is greater than this limit are skipped. However, unit eliminations are always done.

Default to 10_000

val get_steps_bound : unit -> int

Value specifying the maximum number of steps.

Default to -1

val get_timelimit : unit -> float

Value specifying the time limit (not supported on Windows).

Default to 0.

val get_timelimit_interpretation : unit -> float

Value specifying the time limit for model generation (not supported on Windows).

Default to 1. (not supported on Windows)

val get_timelimit_per_goal : unit -> bool

Value specifying the given timelimit for each goal in case of multiple goals per file. In this case, time spent in preprocessing is separated from resolution time.

$Not relevant for GUI-mode.

Default to false

Output options
val get_model : unit -> bool

Experimental support for models on labeled terms.

Possible values are

  • None
  • Default
  • Complete : shows a complete model
  • All : shows all models

Which are used in the two setters below. This option answers true if the model is set to Default or Complete

Default to false

val get_complete_model : unit -> bool

true if the model is set to complete model

Default to false

val get_all_models : unit -> bool

true if the model is set to all models?

Default to false

val get_interpretation : unit -> int

Experimental support for counter-example generation.

Possible values are :

  1. Unknown
  2. Before instantiation
  3. Before every decision or instantiation

A negative value (-1, -2, or -3) will disable interpretation display.

Note that get_max_split limitation will be ignored in model generation phase.

Default to 0

val get_output_format : unit -> output_format

Value specifying the default output format. possible values are

  • native
  • smtlib2
  • why3

.

Default to Native

val get_infer_output_format : unit -> bool

true if Alt-Ergo infers automatically the output format according to the the file extension or the input format if set.

Default to true

val get_unsat_core : unit -> bool

true if experimental support for unsat-cores is on.

Default to false

Profiling options
val get_profiling : unit -> bool

true if the profiling module is activated.

Use Ctrl-C to switch between different views and Ctrl + AltGr + \ to exit.

Default to false

val get_profiling_period : unit -> float

Value specifying the profiling module frequency.

Default to 0.

val get_cumulative_time_profiling : unit -> bool

true if the time spent in called functions is recorded in callers

Default to false

val get_profiling_plugin : unit -> string

Value specifying which module is used as a profiling plugin.

Default to false

val get_timers : unit -> bool

true if profiling is set to true (automatically enabled)

Default to false

val get_verbose : unit -> bool

true if the verbose mode is activated.

Default to false

Quantifier options
val get_instantiation_heuristic : unit -> instantiation_heuristic

Value specifying the instantiation heuristic. possible values are

  • normal
  • auto
  • greedy

.

Default to IAuto

val get_greedy : unit -> bool

true is the greedy instantiation heuristic is set

Default to false

val get_instantiate_after_backjump : unit -> bool

true if a (normal) instantiation round is made after every backjump/backtrack.

Default to false

val get_max_multi_triggers_size : unit -> int

Value specifying the max number of terms allowed in multi-triggers.

Default to 4

val get_triggers_var : unit -> bool

true if variables are allowed as triggers.

Default to false

val get_nb_triggers : unit -> int

Value specifying the number of (multi)triggers.

Default to 2

val get_no_ematching : unit -> bool

true if matching modulo ground equalities is disabled.

Default to false

val get_no_user_triggers : unit -> bool

true if user triggers are ignored except for triggers of theories axioms

Default to false

val get_normalize_instances : unit -> bool

true if generated substitutions are normalised by matching w.r.t. the state of the theory.

This means that only terms that are greater (w.r.t. depth) than the initial terms of the problem are normalized.

Default to false

SAT options
val get_arith_matching : unit -> bool

true if (the weak form of) matching modulo linear arithmetic is disabled.

Default to true

val get_no_backjumping : unit -> bool

true if backjumping mechanism in the functional SAT solver is disabled.

Default to false

val get_bottom_classes : unit -> bool

true if equivalence classes at each bottom of the SAT are shown.

Default to false

val get_sat_solver : unit -> Util.sat_solver

Value specifying which SAT solver is being used.

Possible values are:

  • CDCL-tableaux : CDCL SAT-solver with formulas filtering based on tableaux method

    • satML-Tableaux
    • satML-tableaux

  • CDCL : CDCL SAT-solver

    • satML

  • Tableaux : SAT-solver based on tableaux method

    • tableaux
    • tableaux-like
    • Tableaux-like

  • Tableaux-CDCL : Tableaux method assisted with a CDCL SAT-solver

    • tableaux-cdcl
    • tableaux-CDCL
    • Tableaux-cdcl

Default to CDCL-tableaux

val get_cdcl_tableaux_inst : unit -> bool

true if the use of a tableaux-like method for instantiations is enabled with the CDCL solver if satML is used.

Default to true

val get_cdcl_tableaux_th : unit -> bool

true if the use of a tableaux-like method for theories is enabled with the CDCL solver if satML is used.

Default to true

val get_cdcl_tableaux : unit -> bool

true if the use of a tableaux-like method for theories or instantiations is enabled with the CDCL solver if satML is used.

Default to true

val get_tableaux_cdcl : unit -> bool

true if the tableaux SAT-solver is used with CDCL assist.

Default to false

val get_minimal_bj : unit -> bool

true if minimal backjumping in satML CDCL solver is enabled

Default to true

val get_enable_restarts : unit -> bool

true if restarts are enabled for satML.

Default to false

val get_disable_flat_formulas_simplification : unit -> bool

true if facts simplification is disabled in satML's flat formulas.

Default to false

val get_no_sat_learning : unit -> bool
val get_sat_learning : unit -> bool

true if learning/caching of unit facts in the Default SAT is disabled. These facts are used to improve bcp.

Default to true (sat_learning is active)

val get_sat_plugin : unit -> string

Value specifying which SAT-solver is used.

Default to false

Term options
val get_disable_ites : unit -> bool

true if handling of ite(s) on terms in the backend is disabled.

Default to false

val get_inline_lets : unit -> bool

true if substitution of variables bounds by Let is enabled. The default behavior is to only substitute variables that are bound to a constant, or that appear at most once.

Default to false

val get_rewriting : unit -> bool

true if rewriting is used instead of axiomatic approach.

Default to false

val get_term_like_pp : unit -> bool

true if semantic values shall be output as terms.

Default to true

Theory options
val get_disable_adts : unit -> bool

true if Algebraic Datatypes theory is disabled

Default to false

val get_inequalities_plugin : unit -> string

Value specifying which module is used to handle inequalities of linear arithmetic.

Default to false

val get_no_ac : unit -> bool

true if the AC (Associative and Commutative) theory is disabled for function symbols.

Default to false

val get_no_contracongru : unit -> bool

true if contracongru is disabled.

Default to false

val get_no_fm : unit -> bool

true if Fourier-Motzkin algorithm is disabled.

Default to false

val get_no_nla : unit -> bool

true if non-linear arithmetic reasoning (i.e. non-linear multplication, division and modulo on integers and rationals) is disabled. Non-linear multiplication remains AC.

Default to false

val get_no_tcp : unit -> bool

true if BCP modulo theories is deactivated.

Default to false

val get_no_backward : unit -> bool

true if backward reasoning step (starting from the goal) done in the default SAT solver before deciding is disabled.

Default to false

val get_no_decisions : unit -> bool

true if decisions at the SAT level are disabled.

Default to false

val get_no_theory : unit -> bool

true if theory reasoning is completely deactivated.

Default to false

val get_restricted : unit -> bool

true if the set of decision procedures (equality, arithmetic and AC) is restricted.

Default to false

val get_tighten_vars : unit -> bool

true if the best bounds for arithmetic variables is computed.

Default to false

val get_use_fpa : unit -> bool

true if support for floating-point arithmetic is enabled.

Default to false

val get_rule : unit -> int

Possible values are

  • 0 : parsing
  • 1 : typing
  • 2 : sat
  • 3 : cc
  • 4 : arith

output rule used on stderr.

Default to -1

Files
val get_status : unit -> known_status

Value specifying the status of the file given to Alt-Ergo

Default to Status_Unknown

val get_js_mode : unit -> bool

true if the JavaScript mode is activated

Default to false

val get_file : unit -> string

Value specifying the file given to Alt-Ergo

Default to ""

val get_session_file : unit -> string

Value specifying the session file (base_name.agr) handled by Alt-Ergo

Default to false

val get_used_context_file : unit -> string

Value specifying the base name of the file (with no extension)

Default to false

Functions that are immediately executed

val exec_thread_yield : unit -> unit
val exec_timeout : unit -> unit

Simple Timer module

module Time : sig ... end

Globals

Global functions used throughout the whole program

val tool_req : int -> string -> unit

Displays the used rule

Monomorphisations

Since Options is opened in every module, definition of binary operators to hide their polymorphic versions Stdlib

val (<>) : int -> int -> bool
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 get_can_decide_on : string -> bool
val get_no_decisions_on_is_empty : unit -> bool
val match_extension : string -> input_format

Extra

val set_is_gui : bool -> unit
val get_is_gui : unit -> bool

Printer and formatter

This functions are use to print or set the formatter used to output results debug or error informations

val print_output_format : Format.formatter -> string -> unit

Print message as comment in the corresponding output format

val set_std_fmt : Format.formatter -> unit

Set the std formatter used by default to output the results fmt_std, model fmt_mdl and unsat core fmt_usc.

Default to Format.std_formatter

val set_err_fmt : Format.formatter -> unit

Set the err formatter used by default to output error fmt_err, debug fmt_dbg and warning fmt_wrn informations.

Default to Format.err_formatter

val get_fmt_std : unit -> Format.formatter

Value specifying the formatter used to output results

Default to Format.std_formatter

val get_fmt_err : unit -> Format.formatter

Value specifying the formatter used to output errors

Default to Format.err_formatter

val get_fmt_wrn : unit -> Format.formatter

Value specifying the formatter used to output warnings

Default to Format.err_formatter

val get_fmt_dbg : unit -> Format.formatter

Value specifying the formatter used to output debug informations

Default to Format.err_formatter

val get_fmt_mdl : unit -> Format.formatter

Value specifying the formatter used to output model

Default to Format.std_formatter

val get_fmt_usc : unit -> Format.formatter

Value specifying the formatter used to output unsat core

Default to Format.std_formatter

val set_fmt_std : Format.formatter -> unit

Set fmt_std accessible with get_fmt_std

val set_fmt_err : Format.formatter -> unit

Set fmt_err accessible with get_fmt_err

val set_fmt_wrn : Format.formatter -> unit

Set fmt_wrn accessible with get_fmt_wrn

val set_fmt_dbg : Format.formatter -> unit

Set fmt_dbg accessible with get_fmt_dbg

val set_fmt_mdl : Format.formatter -> unit

Set fmt_mdl accessible with get_fmt_mdl

val set_fmt_usc : Format.formatter -> unit

Set fmt_usc accessible with get_fmt_usc

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