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 freely provide a JavaScript version on Alt-Ergo's website
• we provide a private access to our internal repositories for academia users and our clients.

Quick Evaluation

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.

	public release 0.95.2	public release 0.99.1	private release 1.00
Proved Valid	15980	16334	17638
Proved Valid (%)	84,01 %	85,77 %	92,62 %
Required time (seconds)	10831	10504	9767
Average speed (valid formulas per second)	1,47	1,55	1,81

Main Novelties of Alt-Ergo 1.00

General Improvements

• 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

Bug Fixes

• 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

New Options

• 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

• profiling : makes the profiling module prints its information every seconds

• no-tcp: deactivate constraints propagation modulo theories

Removed Capabilities

• 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

---

About Alt-Ergo

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 Why3 platform. Its development started in 2006 at the Laboratoire de Recherche en Informatique (LRI - CNRS/Inria) of the Université Paris-Saclay and is maintained, developed and distributed since 2013 by the Formal Methods team at OCamlPro.

This work is made possible through research projects like Décysif, Soprano, BWare, Vocal and LCHIP, as well as support from our Alt-Ergo Users' Club members. If Alt-Ergo has been valuable to you, consider joining the Alt-Ergo Users' Club.