Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] [alt-ergo] new public release (version 1.01)

  • Subject: [Frama-c-discuss] [alt-ergo] new public release (version 1.01)
  • From: iguer.pro at gmail.com (Mohamed Iguernlala)
  • Date: Tue, 16 Feb 2016 13:41:35 +0100
Dear Alt-Ergo users,

We are pleased to announce a new public release of Alt-Ergo (version
1.01). The tarball is available on Alt-Ergo's website at:
https://alt-ergo.ocamlpro.com/

OPAM packages and pre-compiled binaries will be available soon.

Please, don't hesitate to report bugs, to ask questions, or to give
your feedback.

CHANGES:
--------

This version is based on private release 1.00 (see its CHANGES
below). The main difference is the new option "-backward-compat" that
allows to output Alt-Ergo's answers in an older syntax (<= 0.99.1). It
is intended to be used with tools that do not support the new
'slightly different' output format (e.g. option
-wp-alt-ergo-opt="-backward-compat" should be used with current
versions of Frama-C).

Best regards,
Mohamed Iguernlala.

---
Senior R&D Engineer, OCamlPro SAS
Research Associate, VALS team, LRI
Webpage: http://www.iguer.info
LinkedIn: https://fr.linkedin.com/in/mohamed-iguernlala-71515979
---


Changes of private release 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 simpler and enables new optimizations and
       factorizations

    ** 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
       avoiding some redundant 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 to the default
        SAT-solver and to the SatML plugin. In particular, the decision
        procedure part now receives facts (literals) in bulk from the
        solvers, rather than individually, trimming the costs of
        intermediate calls to theories reasoners, 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 set) 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 'n'
     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. In practice, the new algorithm
     scales better on linear integer arithmetic problems containing
     lots 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 used

   -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 <delay>: makes the profiling module prints its information
    every <delay> seconds

   -no-tcp: deactivate constraints propagation modulo theories


* Removed Capabilities:

   ** the pruning module used in the frontend is not available anymore

   ** the SMT and SMT2 front-ends have been removed. We plan to implement a
      new front-end for SMT2 in upcoming releases