After the public release of AltErgo 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 AltErgo’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 AltErgo’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 AltErgo 1.00
General Improvements
 theories data structures: semantic values (internal theories representation of terms) are now hashconsed. This enables the use of hashbased 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 reimplemented. The new code is much more simpler and enables some optimizations and factorizations that could not be made before
 casesplit analysis: we made several improvements in the heuristics of the casesplit 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 backjumping in the SAT solver part
 linear integer arithmetic: we reimplemented several parts of linear arithmetic and introduced important improvements in the FourierMotzkin algorithm to make it run on smaller subproblems and avoid some useless executions. These optimizations allowed a significant speed up on our internal benchmarks
 data structures: we optimized hashconsing and some functions in the “formula” and “literal” modules
 SAT solving: we made a lot of improvements in the default SATsolver 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 FourierMotzkin
 Matching: we extended the Ematching algorithm to also perform matching modulo the theory of records. In addition, we simplified matching heuristics and optimized the Ematching process to avoid computing the same instances several times
 Memory management: thanks to the ocpmemprof tool (http://memprof.typerex.org/), we identified some parts of AltErgo 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 ‘saveusedcontext’ 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 frontend” module that interacts with the SAT solvers
 1 in the “congruence closure” algorithm
 1 in “existential quantifiers elimination” module
 1 in the “typechecker”
 1 in the “AC theory” of associative and commutative function symbols
 1 in the “unionfind” module
New OCamlPro Plugins
 profiling plugin: when activated, this plugin records and prints some information about the current execution of AltErgo 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 casesplits, of boolean/theory conflicts, of assumptions in the decision procedure, of generated instances per axiom, ….
 fmsimplex plugin: when activated, this plugin is used instead of the FourierMotzkin method to infer bounds for linear integer arithmetic affine forms (which are used in the casesplit analysis process). This module uses the Simplex algorithm to simulate particular runs of FourierMotzkin, which makes it scale better on linear integer arithmetic problems containing a lot of inequalities
New Options
versioninfo: prints some information about this version of AltErgo (release and compilation dates, release commit ID)
notheory: deactivate theory reasoning. In this case, only the SATsolver and the matching parts are working
inequalitiesplugin: specify a plugin to use, instead of the “default” FourierMotzkin algorithm, to handle inequalities of linear arithmetic
tightenvars: when this option is set, the FmSimplex plugin will try to infer bounds for integer variables as well. Note that this option may be very expensive
profilingplugin: specify a profiling plugin to use to monitor an execution of AltErgo
profiling <freq>: makes the profiling module prints its information every <freq> seconds
notcp: deactivate constraints propagation modulo theories
Removed Capabilities
 the pruning module used in the frontend is now removed
 the SMT and SMT2 frontends are removed. We plan to implement a new frontend for SMT2 in upcoming releases