Private Release of Alt-Ergo 1.00
After the public release of Alt-Ergo 0.99.1 last December, it's time to announce a new major private version (1.00) of our SMT solver. As usual:
- we provide a private access to our internal repositories for academia users and our clients.
A quick comparison between this new version and the previous releases is given below. Timeout is set to 60 seconds. The benchmark is made of 19044 formulas: (a) some of these formulas are known to be invalid, and (b) some of them are out of scope of current SMT solvers. The results are obtained with Alt-Ergo's native input language.
|Proved Valid (%)||84,01 %||85,77 %||92,62 %|
|Required time (seconds)||10831||10504||9767|
(valid formulas per second)
Main Novelties of Alt-Ergo 1.00
- theories data structures: semantic values (internal theories representation of terms) are now hash-consed. This enables the use of hash-based comparison (instead of structural comparison) when possible
- theories combination: the dispatcher component, that sends literals assumed by the SAT solver to different theories depending on whether these literals are equalities, disequalities or inequalities, has been re-implemented. The new code is much more simpler and enables some optimizations and factorizations that could not be made before
- case-split analysis: we made several improvements in the heuristics of the case-split analysis mechanism over finite domains
- explanations propagation: we improved explanations propagation in congruence closure and linear arithmetic algorithms. This makes the proofs faster thanks to a better back-jumping in the SAT solver part
- linear integer arithmetic: we re-implemented several parts of linear arithmetic and introduced important improvements in the Fourier-Motzkin algorithm to make it run on smaller sub-problems and avoid some useless executions. These optimizations allowed a significant speed up on our internal benchmarks
- data structures: we optimized hash-consing and some functions in the "formula" and "literal" modules
- SAT solving: we made a lot of improvements in the default SAT-solver and in the SatML plugin. In particular, the solvers now send lists of facts (literals) to "the decision procedure part" instead of sending them one by one. This avoids intermediate calls to some "expensive" algorithms, such as Fourier-Motzkin
- Matching: we extended the E-matching algorithm to also perform matching modulo the theory of records. In addition, we simplified matching heuristics and optimized the E-matching process to avoid computing the same instances several times
- Memory management: thanks to the ocp-memprof tool (http://memprof.typerex.org/), we identified some parts of Alt-Ergo that needed some improvements in order to avoid useless memory allocations, and thus unburden the OCaml garbage collector
- the function that retrieves the used axioms and predicates (when option 'save-used-context' is activated) has been improved
- 6 in the "inequalities" module of linear arithmetic
- 4 in the "formula" module
- 3 in the "ty" module used for types representation and manipulation
- 2 in the "theories front-end" module that interacts with the SAT solvers
- 1 in the "congruence closure" algorithm
- 1 in "existential quantifiers elimination" module
- 1 in the "type-checker"
- 1 in the "AC theory" of associative and commutative function symbols
- 1 in the "union-find" module
New OCamlPro Plugins
- profiling plugin: when activated, this plugin records and prints some information about the current execution of Alt-Ergo every 'x' seconds: In particular, one can observe a module being activated, a function being called, the amount of time spent in every module/function, the current decision/instantiation level, the number of decisions/instantiations that have been made so far, the number of case-splits, of boolean/theory conflicts, of assumptions in the decision procedure, of generated instances per axiom, ….
- fm-simplex plugin: when activated, this plugin is used instead of the Fourier-Motzkin method to infer bounds for linear integer arithmetic affine forms (which are used in the case-split analysis process). This module uses the Simplex algorithm to simulate particular runs of Fourier-Motzkin, which makes it scale better on linear integer arithmetic problems containing a lot of inequalities
version-info: prints some information about this version of Alt-Ergo (release and compilation dates, release commit ID)
no-theory: deactivate theory reasoning. In this case, only the SAT-solver and the matching parts are working
inequalities-plugin: specify a plugin to use, instead of the "default" Fourier-Motzkin algorithm, to handle inequalities of linear arithmetic
tighten-vars: when this option is set, the Fm-Simplex plugin will try to infer bounds for integer variables as well. Note that this option may be very expensive
profiling-plugin: specify a profiling plugin to use to monitor an execution of Alt-Ergo
: makes the profiling module prints its information every seconds
no-tcp: deactivate constraints propagation modulo theories
- the pruning module used in the frontend is now removed
- the SMT and SMT2 front-ends are removed. We plan to implement a new front-end for SMT2 in upcoming releases
Alt-Ergo is an open-source automatic solver of mathematical formulas designed for program verification. Alt-Ergo is very successful for proving formulas generated in the context of deductive program verification. It was originally designed and tuned to be used by the Why playform. Its development started in 2006 at the Laboratoire de Recherche en Informatique (LRI) of the Université Paris Sud and is maintained, developed and distributed since 2013 by the company OCamlPro.
Alt-Ergo is part of the formal method team here at OCamlPro. This work is partially funded by the research projects Soprano, BWare, Vocal and LCHIP. If you like Alt-Ergo, consider joining the Alt-Ergo user’s Club