[Why3-club] Release of Alt-Ergo 2.3.0

Mohamed Iguernlala iguer.auto at gmail.com
Tue Feb 12 11:58:56 CET 2019


Yes, we will probably write a more detailed paper about this, and
it should part of Albin Coquereau's Thesis.

Roughly speaking, we (dynamically) filter the model constructed
by the CDCL SAT solver to only keep the facts which satisfy a
branch that would be constructed by the Tableaux method. This
reduced model is then used to check satisfiabily modulo theories
and to generate new instances by E-matching.

This is somehow similar to what is described in this Z3 tech. report:
https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/tr-2007-140.pdf

- Mohamed.


On 12/02/2019 11:50, Gabriel Scherer wrote:
> Thanks for the very nice blog post, and interesting work.
>
> I looked at the System Description paper, but there are not a lot of 
> details about how you tweak CDCL to better match the previous Tableaux 
> prover.
> Do you plan to write a more detailed article about this?
>
> On Tue, Feb 12, 2019 at 11:21 AM Mohamed Iguernlala 
> <iguer.auto at gmail.com <mailto:iguer.auto at gmail.com>> wrote:
>
>     Release of Alt-Ergo 2.3.0
>
>     Dear Alt-Ergo users,
>
>     We are happy to announce the release of Alt-Ergo 2.3.0. You can
>     get the sources from the website: https://alt-ergo.ocamlpro.com.
>     OPAM packages will be available soon.
>
>     The main novelties of this version are given in this blog post:
>     http://www.ocamlpro.com/2019/02/11/whats-new-for-alt-ergo-in-2018-here-is-a-recap/
>
>     and a more exhaustive list of CHANGES is available here:
>     https://github.com/OCamlPro/alt-ergo/blob/2.3.0/sources/CHANGES
>
>     Also, we are happy to inform you that an Alt-Ergo Users Club is
>     born. The first meeting is scheduled for this week. Don't
>     hesitate to contact us if you want to join the Club and to support
>     Alt-Ergo development.
>
>     As usual, you can report bugs, ask questions, or give your
>     feedback regarding this version, or Alt-Ergo in general:
>     https://github.com/OCamlPro/alt-ergo/issues
>
>     Best regards,
>     Mohamed Iguernlala
>
>     -- 
>     Senior R&D Engineer, OCamlPro SAS
>     Research Associate, VALS team, LRI
>     Webpage: http://www.iguer.xyz
>     LinkedIn: https://fr.linkedin.com/in/mohamed-iguernlala-71515979
>
>     _______________________________________________
>     Why3-club mailing list
>     Why3-club at lists.gforge.inria.fr
>     <mailto:Why3-club at lists.gforge.inria.fr>
>     https://lists.gforge.inria.fr/mailman/listinfo/why3-club
>
-------------- section suivante --------------
Une pièce jointe HTML a été nettoyée...
URL: <http://lists.gforge.inria.fr/pipermail/why3-club/attachments/20190212/36d114ca/attachment-0001.html>


More information about the Why3-club mailing list