Module AltErgoLib.Options

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 instantiation_heuristic =
  1. | INormal
    (*

    Least costly heuristic for instantiation, instantiate on a reduced set of term

    *)
  2. | IAuto
    (*

    Default Heuristic that try to do the normal heuristic and then try a greedier instantiation if no new instance have been made

    *)
  3. | IGreedy
    (*

    Force instantiation to be the greedier as possible, use all available ground terms

    *)

Type used to describe the type of heuristic for instantiation wanted by set_instantiation_heuristic

type interpretation =
  1. | INone
    (*

    Default, No interpretation computed

    *)
  2. | IFirst
    (*

    Compute an interpretation after the first instantiation and output it at the end of the executionn

    *)
  3. | IEvery
    (*

    Compute an interpretation before every instantiation and return the last one computed

    *)
  4. | ILast
    (*

    Compute only the last interpretation just before returning SAT/Unknown

    *)

Type used to describe the type of interpretation wanted by set_interpretation

type smtlib2_version = [
  1. | `Latest
    (*

    Latest version of the SMT-LIB standard.

    *)
  2. | `V2_6
    (*

    The SMT-LIB standard: Version 2.6

    *)
  3. | `Poly
    (*

    Polymorphic extension of the SMT-LIB standard.

    See the tool paper

    *)
]

Version of the SMT-LIB standard used.

type input_format =
  1. | Native
    (*

    Native Alt-Ergo format

    *)
  2. | Smtlib2 of smtlib2_version
    (*

    SMT-LIB 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 model_type =
  1. | Value
  2. | Constraints
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_intervals : bool -> unit

Set debug_intervals accessible with get_debug_intervals

val set_debug_fpa : int -> unit

Set debug_fpa accessible with get_debug_fpa

Possible values are

  1. Disabled
  2. Light
  3. Full
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_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_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_debug_commands : bool -> unit

Set debug_commands accessible with get_debug_commands

val set_debug_optimize : bool -> unit

Set debug_optimize accessible with get_debug_optimize

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_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 option -> unit

Set input_format accessible with get_input_format

val set_interpretation : interpretation -> unit

Set interpretation accessible with get_interpretation

Possible values are :

  1. First
  2. Before every instantiation
  3. Before every decision and instantiation
  4. Before end
val set_strict_mode : bool -> unit

Set strict_mode accessible with get_strict_mode.

val set_dump_models : bool -> unit

dump_models accessible with get_dump_models.

val set_interpretation_use_underscore : bool -> unit

Set interpretation_use_underscore accessible with get_interpretation_use_underscore

val set_objectives_in_interpretation : bool -> unit

Set objectives_in_interpretation accessible with get_objectives_in_interpretation

val set_max_split : Numbers.Q.t -> unit

Set max_split accessible with get_max_split

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_model_type : model_type -> unit

Set model_type accessible with get_model_type

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

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_enable_sat_cs : bool -> unit

Set enable_sat_cs accessible with get_enable_sat_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_output_format : bool -> unit

Set infer_output_format accessible with get_infer_output_format

val set_preludes : string list -> unit

Set preludes accessible with get_preludes

val set_theory_preludes : Theories.prelude list -> unit

Set theory_preludes accessible with get_theory_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_exit_on_error : bool -> unit

Set exit_on_error accessible with get_exit_on_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 : AltErgoLib.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_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_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_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_commands : unit -> bool

Get the debugging flag of commands. If enabled, Alt-Ergo will display all the commands that are sent to the solver.

val get_debug_optimize : unit -> bool

Get the debugging flag of optimize. If enabled, Alt-Ergo will output debugging messages about the optimization of values in models.

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_intervals : unit -> bool

Get the debugging flag of intervals.

val get_debug_fpa : unit -> int

Get the debugging value of floating-point.

Default to 0.

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_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_enable_sat_cs : unit -> bool

true if case-split are performed in the SAT solver rather than the theory solver (only for CDCL solver and for select theories).

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_input_format : unit -> input_format option

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

If None, Alt-Ergo will automatically infer the input format according to the file extension.

Default to None

val get_parse_only : unit -> bool

true if the program shall stop after parsing.

Default to false

val get_preludes : unit -> string list

List of files that have be loaded as preludes.

Default to []

val get_theory_preludes : unit -> Theories.prelude list

List of theory preludes to load.

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

val get_exit_on_error : unit -> bool

true if alt-ergo exits on all errors.

Default to true

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_interpretation : unit -> bool

Experimental support for counter-example generation.

Possible values are :

  1. First
  2. Before every instantiation
  3. Before every decision and instantiation
  4. Before end

Which are used in the four getters below. This option answers true if the interpretation is set to First, Before_end, Before_dec or Before_inst.

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

Default to false

val get_strict_mode : unit -> bool

true if strict mode is enabled.

val get_dump_models : unit -> bool

true if the interpretation for each goal or check-sat is printed.

Default to false.

val get_first_interpretation : unit -> bool

true if the interpretation is set to first interpretation

Default to false

val get_every_interpretation : unit -> bool

true if the interpretation is set to compute interpretation before every instantiation

Default to false

val get_last_interpretation : unit -> bool

true if the interpretation is set to compute interpretation before the solver return unknown

Default to false

val get_interpretation_use_underscore : unit -> bool

true if the interpretation_use_underscore is set to output _ instead of fresh values

Default to false

val get_objectives_in_interpretation : unit -> bool

true if the objectives_in_interpretation is set to inline pretty-printing of optimized expressions in the model instead of a dedicated section '(objectives ...)'. Be aware that the model may be shrunk or not accurate if some expressions to optimize are unbounded.

Default to false

val get_output_format : unit -> output_format

Value specifying the default output format. possible values are

  • native
  • smtlib2
  • why3

.

Default to Native

val get_output_smtlib : unit -> bool

true if the output format is set to smtlib2 or why3

Default to false

val get_model_type : unit -> model_type

Value specifying the default model type. possible values are

  • value
  • constraints

.

Default to Value

val get_model_type_constraints : unit -> bool

true if the model kind is set to constraints .

Default to false

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_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_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_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
val with_timelimit_if : bool -> (unit -> 'a) -> 'a

with_timelimit_if cond f is:

  • Time.with_timeout (get_timeout ()) f when cond is true
  • f () otherwise
  • raises Util.Timeout

    if the cond is true and the timeout is reached before the calls to f () completes.

Globals

Global functions used throughout the whole program

val tool_req : int -> string -> unit

Displays the used rule

val get_can_decide_on : string -> bool
val get_no_decisions_on_is_empty : unit -> bool
val match_extension : string -> input_format

Extra

Printer and formatter

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

module Output : sig ... end

Output channels manager.

module Sources : sig ... end
val pp_comment : Stdlib.Format.formatter -> string -> unit

Print message as comment in the corresponding output format

val heavy_assert : (unit -> bool) -> unit

heavy_assert p checks if the suspended boolean p evaluates to true. No-op if the Options.get_enable_assertions () is false.

  • raises Assert_failure

    if p evaluates to false.