Fedora 21 Update: alt-ergo-0.99.1-1.fc21

updates at fedoraproject.org updates at fedoraproject.org
Sat Jan 17 05:47:33 UTC 2015


--------------------------------------------------------------------------------
Fedora Update Notification
FEDORA-2015-0362
2015-01-07 22:55:24
--------------------------------------------------------------------------------

Name        : alt-ergo
Product     : Fedora 21
Version     : 0.99.1
Release     : 1.fc21
URL         : http://alt-ergo.ocamlpro.com/
Summary     : Automated theorem prover including linear arithmetic
Description :
Alt-Ergo is an automated theorem prover implemented in OCaml. It is
based on CC(X) - a congruence closure algorithm parameterized by an
equational theory X. This algorithm is reminiscent of the Shostak
algorithm. Currently CC(X) is instantiated by the theory of linear
arithmetics. Alt-Ergo also contains a home made SAT-solver and an
instantiation mechanism by which it fully supports quantifiers.

--------------------------------------------------------------------------------
Update Information:

Changes in version 0.99.1:
- the "SAT solving" part can now be delegated to an external plugin;
- new experimental SAT solver based on mini-SAT, provided as a plugin. This solver is, in general, more efficient on ground problems;
- heuristics simplification in the default SAT solver and in the matching (instantiation) module;
- re-implementation of internal literals representation;
- improvement of theories combination architecture;
- rewriting some parts of the formulas module;
- bugfixes in records and numbers modules;
- new option "-no-Ematching" to perform matching without equality  reasoning (i.e. without considering "equivalence classes"). This option is very useful for benchmarks coming from Atelier-B;
- two new experimental options: "-save-used-context" and "-replay-used-context". When the goal is proved valid, the first option allows to save the names of useful axioms into a ".used" file. The second one is used to replay the proof using only the axioms listed in the corresponding ".used" file. Note that the replay may fail because of the absence of necessary ground terms generated by useless axioms (that are not included in .used file) during the initial run.
--------------------------------------------------------------------------------
ChangeLog:

* Tue Jan  6 2015 Jerry James <loganjerry at gmail.com> - 0.99.1-1
- Update to version 0.99.1
--------------------------------------------------------------------------------

This update can be installed with the "yum" update program.  Use
su -c 'yum update alt-ergo' at the command line.
For more information, refer to "Managing Software with yum",
available at http://docs.fedoraproject.org/yum/.

All packages are signed with the Fedora Project GPG key.  More details on the
GPG keys used by the Fedora Project can be found at
https://fedoraproject.org/keys
--------------------------------------------------------------------------------


More information about the package-announce mailing list