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 instantiation_heuristic =
| INormal
(*
Least costly heuristic for instantiation, instantiate on a reduced set of term
*)
| IAuto
(*
Default Heuristic that try to do the normal heuristic and then try a greedier instantiation if no new instance have been made
*)
| IGreedy
(*
Force instantiation to be the greedier as possible, use all available ground terms
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
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 :
First
Before every instantiation
Before every decision and instantiation
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_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
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.