NAME¶

alt-ergo - Execute Alt-Ergo on the given file.

SYNOPSIS¶

alt-ergo [OPTION]… [FILE]

ARGUMENTS¶

FILE

Source file. Must be suffixed by .ae, (.mlw and .why are depreciated, .smt2 or .psmt2.

OPTIONS¶

-d, --debug

Set the debugging flag.

-i FMT, --input=FMT

Set the default input format to FMT and must be one of native, altergo, alt-ergo, smtlib2, smt-lib2 or why3. Useful when the extension does not allow to automatically select a parser (eg. JS mode, GUI mode, ...).

-m VAL, --model=VAL (absent=none)

Experimental support for models on labeled terms. VAL must be one of none, default, complete or all. 'complete' shows a complete model and 'all' shows all models.

-o FMT, --output=FMT

Control the output format of the solver, FMT must be either native or smtlib.The alt-ergo native format outputs Valid/Invalid/I don't know.The smtlib format outputs unsat/sat/unknown.If left unspecified, Alt-Ergo will use its heuristics to determine the adequate output format according to the input format.It must be noticed that not specifying an output format will let Alt-Ergo set it according to the input file's extension.

-p, --pretty-output

Print output with formatting rules, headers and colors

-r, --replay-used-context

Replay with axioms and predicates saved in .used file.

-S STEPS, --steps-bound=STEPS (absent=-1)

Set the maximum number of steps.

-s, --save-used-context

Save used axioms and predicates in a .used file. This option implies --unsat-core.

-t VAL, --timelimit=VAL

Set the time limit to VAL seconds (not supported on Windows).

-u, --unsat-core

Experimental support for computing and printing unsat-cores.

-v, --verbose

Set the verbose mode.

EXECUTION OPTIONS¶

--add-parser=VAL

Register a new parser for Alt-Ergo.

--colors-in-output

Print output with colors.

--frontend=FTD (absent=legacy)

Select the parsing and typing frontend.

--no-forced-flush-in-output

Print output without forced flush at the end of each print.

--no-formatting-in-output

Don not use formatting rule in output.

--no-headers-in-output

Print output without headers.

--no-locs-in-answers

Do not show the locations of goals when printing solver's answers.

--parse-only

Stop after parsing.

--prelude=VAL

Add a file that will be loaded as a prelude. The command is cumulative, and the order of successive preludes is preserved.

--type-only

Stop after typing.

--type-smt2

Stop after SMT2 typing.

LIMIT OPTIONS¶

--age-bound=AGE (absent=50)

Set the age limit bound.

--fm-cross-limit=VAL (absent=10000)

Skip Fourier-Motzkin variables elimination steps that may produce a number of inequalities that is greater than the given limit. However, unit eliminations are always done.

--timelimit-interpretation=SEC

Set the time limit to SEC seconds for model generation (not supported on Windows).

--timelimit-per-goal

Set the timelimit given by the --timelimit option to apply 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.

INTERNAL OPTIONS¶

--disable-weaks

Prevent the GC from collecting hashconsed data structrures that are not reachable (useful for more determinism).

--enable-assertions

Enable verification of some heavy invariants.

--gc-policy=PLCY (absent=0)

Set the gc policy allocation. 0 = next-fit policy, 1 = first-fit policy, 2 = best-fit policy. See the Gc module of the OCaml distribution for more informations.

--warning-as-error

Enable warning as error

OUTPUT OPTIONS¶

--interpretation=VAL (absent=0)

Experimental support for counter-example generation. Possible values are 1, 2, or 3 to compute an interpretation before returning Unknown, before instantiation (1), or before every decision (2) or instantiation (3). A negative value (-1, -2, or -3) will disable interpretation display. Note that --max-split limitation will be ignored in model generation phase.

CONTEXT OPTIONS¶

--replay

Replay session saved in file_name.agr.

--replay-all-used-context

Replay with all axioms and predicates saved in .used files of the current directory.

PROFILING OPTIONS¶

--cumulative-time-profiling

Record the time spent in called functions in callers

--profiling=DELAY

Activate the profiling module with the given frequency. Use Ctrl-C to switch between different views and "Ctrl + AltGr + \ " to exit.

--profiling-plugin=PGN

Use the given profiling plugin.

SAT OPTIONS¶

--bottom-classes

Show equivalence classes at each bottom of the sat.

--disable-flat-formulas-simplification

Disable facts simplifications in satML's flat formulas.

--enable-restarts

For satML: enable restarts or not. Default behavior is 'false'.

--no-arith-matching

Disable (the weak form of) matching modulo linear arithmetic.

--no-backjumping

Disable backjumping mechanism in the functional SAT solver.

--no-backward

Disable backward reasoning step (starting from the goal) done in the default SAT solver before deciding.

--no-decisions

Disable decisions at the SAT level.

--no-decisions-on=[INST1; INST2; ...]

Disable decisions at the SAT level for the instances generated from the given axioms. Arguments should be separated with a comma.

--no-minimal-bj

Disable minimal backjumping in satML CDCL solver.

--no-sat-learning

Disable learning/caching of unit facts in the Default SAT. These facts are used to improve bcp.

--no-tableaux-cdcl-in-instantiation

When satML is used, this disables the use of a tableaux-likemethod for instantiations with the CDCL solver.

--no-tableaux-cdcl-in-theories

When satML is used, this disables the use of a tableaux-likemethod for theories with the CDCL solver.

--sat-plugin=VAL

Use the given SAT-solver instead of the default DFS-based SAT solver.

--sat-solver=SAT (absent=CDCL-Tableaux)

Choose the SAT solver to use. Default value is CDCL (i.e. satML solver). Possible options are one of CDCL, satML, CDCL-Tableaux, satML-Tableaux or Tableaux-CDCL.

QUANTIFIERS OPTIONS¶

--inst-after-bj

Make a (normal) instantiation round after every backjump/backtrack.

--instantiation-heuristic=VAL (absent=auto)

Change the instantiation heuristic. VAL must be one of normal, auto or greedy. By default 'auto' is used for both sat solvers. 'normal' does one less phase of instantiation. 'greedy' use all available ground terms in instantiation.

--max-multi-triggers-size=VAL (absent=4)

Maximum size of multi-triggers, i.e. the maximum number of independent patterns in a multi-trigger.

--nb-triggers=VAL (absent=2)

Maximum number of triggers used (including regular and multi triggers).

--no-ematching

Disable matching modulo ground equalities.

--no-user-triggers

Ignore user triggers, except for triggers of theories' axioms

--normalize-instances

Normalize generated substitutions 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.

--triggers-var

Allows variables as triggers.

TERM OPTIONS¶

--disable-ites

Disable handling of ite(s) on terms in the backend.

--inline-lets

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

--rwt, --rewriting

Use rewriting instead of axiomatic approach.

--term-like-pp

Output semantic values as terms.

THEORY OPTIONS¶

--disable-adts

Disable Algebraic Datatypes theory.

--inequalities-plugin=VAL

Use the given module to handle inequalities of linear arithmetic.

--no-ac

Disable the AC theory of Associative and Commutative function symbols.

--no-contracongru

Disable contracongru.

--no-fm

Disable Fourier-Motzkin algorithm.

--no-nla

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

--no-tcp

Deactivate Boolean Constant Propagation (BCP) modulo theories.

--no-theory

Completely deactivate theory reasoning.

--restricted

Restrict set of decision procedures (equality, arithmetic and AC).

--tighten-vars

Compute the best bounds for arithmetic variables.

--use-fpa

Enable support for floating-point arithmetic.

CASE SPLIT OPTIONS¶

--case-split-policy=PLCY (absent=after-theory-assume)

Case-split policy. Set the case-split policy to use. Possible values are one of after-theory-assume, before-matching or after-matching.

--enable-adts-cs

Enable case-split for Algebraic Datatypes theory.

--max-split=VAL (absent=1000000)

Maximum size of case-split.

HALTING OPTIONS¶

--version-info

Print some info about this version (version, date released, date commited) .

--where=DIR

Print the directory of DIR. Possible arguments are one of lib, plugins, preludes, data or man.

FORMATTER OPTIONS¶

--err-formatter=VAL (absent=stderr)

Set the error formatter used by default to output error, debug and warning informations. Possible values are one of stdout, stderr or <filename>.

--std-formatter=VAL (absent=stdout)

Set the standard formatter used by default to output the results, models and unsat cores. Possible values are one of stdout, stderr or <filename>.

DEBUG OPTIONS¶

These options are used to output debug info for the concerned part of the solver.They are not used to check internal consistency.

--dac

Set the debugging flag of ac.

--dadt

Set the debugging flag of ADTs.

--darith

Set the debugging flag of Arith (without fm).

--darrays

Set the debugging flag of arrays.

--dbitv

Set the debugging flag of bitv.

--dcc

Set the debugging flag of cc.

--dcombine

Set the debugging flag of combine.

--dconstr

Set the debugging flag of constructors.

--debug-interpretation

Set debug flag for interpretation generatation.

--debug-unsat-core

Replay unsat-cores produced by --unsat-core. The option implies --unsat-core.

--dexplanations

Set the debugging flag of explanations.

--dfm

Set the debugging flag of inequalities.

--dfpa=VAL (absent=0)

Set the debugging flag of floating-point.

--dgc

Prints some debug info about the GC's activity.

--dite

Set the debugging flag of ite.

--dmatching=FLAG (absent=0)

Set the debugging flag of E-matching (0=disabled, 1=light, 2=full).

--dsat

Set the debugging flag of sat.

--dsplit

Set the debugging flag of case-split analysis.

--dsum

Set the debugging flag of Sum.

--dtriggers

Set the debugging flag of triggers.

--dtypes

Set the debugging flag of types.

--dtyping

Set the debugging flag of typing.

--duf

Set the debugging flag of uf.

--duse

Set the debugging flag of use.

--dwarnings

Set the debugging flag of warnings.

--rule=TR (absent=none)

TR = parsing|typing|sat|cc|arith, output rule used on stderr.

COMMON OPTIONS¶

--help[=FMT] (default=auto)

Show this help in format FMT. The value FMT must be one of auto, pager, groff or plain. With auto, the format is pager or plain whenever the TERM env var is dumb or undefined.

--version

Show version information.

EXIT STATUS¶

alt-ergo exits with the following status:

0

on success.

1

on default errors

123

on indiscriminate errors reported on standard error.

124

on command line parsing errors.

125

on unexpected internal errors (bugs).

142

on timeout errors

BUGS¶

You can open an issue on: https://github.com/OCamlPro/alt-ergo/issues

Or you can write to: 


   alt-ergo@ocamlpro.com

AUTHORS¶

CURRENT AUTHORS


   Sylvain Conchon


   Albin Coquereau


   Guillaume Bury


   Mattias Roux

ORIGINAL AUTHORS


   Sylvain Conchon


   Evelyne Contejean


   Mohamed Iguernlala


   Stephane Lescuyer


   Alain Mebsout