Type used to describe the type of models wanted

Type used to describe the type of heuristic for instantiation wanted

Type used to describe the type of input wanted by set_input_format

Type used to describe the type of output wanted by set_output_format

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

Set debug accessible with get_debug

Set debug_ac accessible with get_debug_ac

Set debug_adt accessible with get_debug_adt

Set debug_arith accessible with get_debug_arith

Set debug_arrays accessible with get_debug_arrays

Set debug_bitv accessible with get_debug_bitv

Set debug_cc accessible with get_debug_cc

Set debug_combine accessible with get_debug_combine

Set debug_constr accessible with get_debug_constr

Set debug_explanations accessible with get_debug_explanations

Set debug_fm accessible with get_debug_fm

Set debug_fpa accessible with get_debug_fpa

Set debug_gc accessible with get_debug_gc

Set debug_interpretation accessible with get_debug_interpretation

Set debug_ite accessible with get_debug_ite

Set debug_matching accessible with get_debug_matching

Possible values are

1. Disabled
2. Light
3. Full

Set debug_sat accessible with get_debug_sat

Set debug_split accessible with get_debug_split

Set debug_sum accessible with get_debug_sum

Set debug_triggers accessible with get_debug_triggers

Set debug_types accessible with get_debug_types

Set debug_typing accessible with get_debug_typing

Set debug_uf accessible with get_debug_uf

Set debug_unsat_core accessible with get_debug_unsat_core

Set debug_use accessible with get_debug_use

Set debug_warnings accessible with get_debug_warnings

Set profiling accessible with get_profiling

Set timers accessible with get_timers

Set type_only accessible with get_type_only

Set age_bound accessible with get_age_bound

Set bottom_classes accessible with get_bottom_classes

Set fm_cross_limit accessible with get_fm_cross_limit

Set frontend accessible with get_frontend

Set instantiation_heuristic accessible with get_instantiation_heuristic

Set inline_lets accessible with get_inline_lets

Set input_format accessible with get_input_format

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.

Set max_split accessible with get_max_split

Set model accessible with get_model

Possible values are :

• Default
• Complete
• All

Set nb_triggers accessible with get_nb_triggers

Set no_ac accessible with get_no_ac

Set no_contragru accessible with get_no_contragru

Set no_ematching accessible with get_no_ematching

Set no_nla accessible with get_no_nla

Set no_user_triggers accessible with get_no_user_triggers

Set normalize_instances accessible with get_normalize_instances

Set output_format accessible with get_output_format

Set parse_only accessible with get_parse_only

Set restricted accessible with get_restricted

Set rewriting accessible with get_rewriting

Set rule accessible with get_rule

Set save_used_context accessible with get_save_used_context

Set steps_bound accessible with get_steps_bound

Set term_like_pp accessible with get_term_like_pp

Set thread_yield accessible with get_thread_yield

Set timelimit accessible with get_timelimit

Set timeout accessible with get_timeout

Set triggers_var accessible with get_triggers_var

Set type_smt2 accessible with get_type_smt2

Set unsat_core accessible with get_unsat_core

Set verbose accessible with get_verbose

Set status accessible with get_status

Set file accessible with get_file

Updates the filename to be parsed and sets a js_mode flag

Set case_split_policy accessible with get_case_split_policy

Set enable_adts_cs accessible with get_enable_adts_cs

Set replay accessible with get_replay

Set replay_all_used_context accessible with get_replay_all_used_context

Set replay_used_context accessible with get_replay_used_context

Set answers_with_loc accessible with get_answers_with_loc

Set output_with_colors accessible with get_output_with_colors

Set output_with_headers accessible with get_output_with_headers

Set output_with_formatting accessible with get_output_with_formatting

Set infer_input_format accessible with get_infer_input_format

Set infer_output_format accessible with get_infer_output_format

Set parsers accessible with get_parsers

Set preludes accessible with get_preludes

Set disable_weaks accessible with get_disable_weaks

Set enable_assertions accessible with get_enable_assertions

Set warning_as_error accessible with get_warning_as_error

Set timelimit_interpretation accessible with get_timelimit_interpretation

Set timelimit_per_goal accessible with get_timelimit_per_goal

Set cumulative_time_profiling accessible with get_cumulative_time_profiling

Set profiling_period accessible with get_profiling_period

Set profiling_plugin accessible with get_profiling_plugin

Set instantiate_after_backjump accessible with get_instantiate_after_backjump

Set max_multi_triggers_size accessible with get_max_multi_triggers_size

Set arith_matching accessible with get_arith_matching

Set cdcl_tableaux_inst accessible with get_cdcl_tableaux_inst

Set cdcl_tableaux_th accessible with get_cdcl_tableaux_th

Set disable_flat_formulas_simplification accessible with get_disable_flat_formulas_simplification

Set enable_restarts accessible with get_enable_restarts

Set minimal_bj accessible with get_minimal_bj

Set no_backjumping accessible with get_no_backjumping

Set no_backward accessible with get_no_backward

Set no_decisions accessible with get_no_decisions

Set no_decisions_on accessible with get_no_decisions_on

Set no_sat_learning accessible with get_no_sat_learning

Set sat_plugin accessible with get_sat_plugin

Set sat_solver accessible with get_sat_solver

Set tableaux_cdcl accessible with get_tableaux_cdcl

Set disable_ites accessible with get_disable_ites

Set disable_adts accessible with get_disable_adts

Set inequalities_plugin accessible with get_inequalities_plugin

Set no_fm accessible with get_no_fm

Set no_tcp accessible with get_no_tcp

Set no_theory accessible with get_no_theory

Set tighten_vars accessible with get_tighten_vars

Set use_fpa accessible with get_use_fpa

Set session_file accessible with get_session_file

Set used_context_file accessible with get_used_context_file

Get the debugging flag.

Get the debugging flag of warnings.

Get the debugging flag of cc.

Prints some debug info about the GC's activity.

Get the debugging flag of use.

Get the debugging flag of uf.

Get the debugging flag of inequalities.

Get the debugging value of floating-point.

Default to 0.

Get the debugging flag of Sum.

Get the debugging flag of ADTs.

Get the debugging flag of Arith (without fm).

Get the debugging flag of bitv.

Get the debugging flag of ac.

Get the debugging flag of SAT.

Get the debugging flag of typing.

Get the debugging flag of constructors.

Get the debugging flag of arrays.

Get the debugging flag of ite.

Get the debugging flag of types.

Get the debugging flag of combine.

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

Get the debugging flag of case-split analysis.

Get the debugging flag of E-matching

Possible values are

1. Disabled
2. Light
3. Full

Get the debugging flag of explanations.

Get the debugging flag of triggers.

Get the debugging flag for interpretation generatation.

Value specifying the case-split policy.

Possible values are :

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

Default to after-theory-assume

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

Default to false

Valuget_e specifying the maximum size of case-split.

Default to 1_000_000

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

Default to false

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

Default to false

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

Default to false

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

Default to false

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

Default to true

true if the outputs are printed with colors

Default to true

true if the outputs are printed with headers

Default to true

true if the outputs are printed with formatting rules

Default to true

Valuget_e of the currently selected parsing and typing frontend.

Default to legacy

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

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

true if the program shall stop after parsing.

Default to false

List of registered parsers for Alt-Ergo.

Default to false

List of files that have be loaded as preludes.

Default to []

true if the program shall stop after typing.

Default to false

true if the program shall stop after SMT2 typing.

Default to false

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

Default to false

true if verification of some heavy invariants is enabled.

Default to false

true if warning are set as error.

Default to false

Value specifying the age limit bound.

Default to 50

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

Value specifying the maximum number of steps.

Default to -1

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

Default to 0.

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

Default to 1. (not supported on Windows)

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

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

true if the model is set to complete model

Default to false

true if the model is set to all models?

Default to false

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

Value specifying the default output format. possible values are

• native
• smtlib2
• why3

.

Default to Native

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

Default to true

true if experimental support for unsat-cores is on.

Default to false

true if the profiling module is activated.

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

Default to false

Value specifying the profiling module frequency.

Default to 0.

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

Default to false

Value specifying which module is used as a profiling plugin.

Default to false

true if profiling is set to true (automatically enabled)

Default to false

true if the verbose mode is activated.

Default to false

Value specifying the instantiation heuristic. possible values are

• normal
• auto
• greedy

.

Default to IAuto

true is the greedy instantiation heuristic is set

Default to false

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

Default to false

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

Default to 4

true if variables are allowed as triggers.

Default to false

Value specifying the number of (multi)triggers.

Default to 2

true if matching modulo ground equalities is disabled.

Default to false

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

Default to false

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

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

Default to true

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

Default to false

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

Default to false

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

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

Default to true

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

Default to true

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

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

Default to false

true if minimal backjumping in satML CDCL solver is enabled

Default to true

true if restarts are enabled for satML.

Default to false

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

Default to false

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)

Value specifying which SAT-solver is used.

Default to false

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

Default to false

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

true if rewriting is used instead of axiomatic approach.

Default to false

true if semantic values shall be output as terms.

Default to true

true if Algebraic Datatypes theory is disabled

Default to false

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

Default to false

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

Default to false

true if contracongru is disabled.

Default to false

true if Fourier-Motzkin algorithm is disabled.

Default to false

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

true if BCP modulo theories is deactivated.

Default to false

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

Default to false

true if decisions at the SAT level are disabled.

Default to false

true if theory reasoning is completely deactivated.

Default to false

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

Default to false

true if the best bounds for arithmetic variables is computed.

Default to false

true if support for floating-point arithmetic is enabled.

Default to false

Possible values are

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

output rule used on stderr.

Default to -1

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

Default to Status_Unknown

true if the JavaScript mode is activated

Default to false

Value specifying the file given to Alt-Ergo

Default to ""

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

Default to false

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

Default to false

Displays the used rule

Extra

Print message as comment in the corresponding output format

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

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

Value specifying the formatter used to output results

Default to Format.std_formatter

Value specifying the formatter used to output errors

Default to Format.err_formatter

Value specifying the formatter used to output warnings

Default to Format.err_formatter

Value specifying the formatter used to output debug informations

Default to Format.err_formatter

Value specifying the formatter used to output model

Default to Format.std_formatter

Value specifying the formatter used to output unsat core

Default to Format.std_formatter

Set fmt_std accessible with get_fmt_std

Set fmt_err accessible with get_fmt_err

Set fmt_wrn accessible with get_fmt_wrn

Set fmt_dbg accessible with get_fmt_dbg

Set fmt_mdl accessible with get_fmt_mdl

Set fmt_usc accessible with get_fmt_usc