|Index||index by Group||index by Distribution||index by Vendor||index by creation date||index by Name||Mirrors||Help||Search|
|Name: alt-ergo||Distribution: Fedora Project|
|Version: 0.93||Vendor: Fedora Project|
|Release: 2.fc15||Build date: Mon Nov 14 21:13:45 2011|
|Group: Applications/Engineering||Build host: x86-10.phx2.fedoraproject.org|
|Size: 1515233||Source RPM: alt-ergo-0.93-2.fc15.src.rpm|
|Packager: Fedora Project|
|Summary: Automated theorem prover including linear arithmetic|
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.
* Mon Nov 14 2011 Jerry James <email@example.com> - 0.93-2 - Build on all arches with ocaml * Thu May 12 2011 Jerry James <firstname.lastname@example.org> - 0.93-1 - Update to version 0.93. This means: - New command-line options -steps, -max-split, and -proof - New polymorphic theory of arrays - Built-in support for enumeration types - Graphical front end - New predicate distinct() - New constructs: let x = <term> in <term>, let x = <term> in <formula> - Partial support for the division operator - Unspecified bug fixes * Mon Feb 07 2011 Fedora Release Engineering <email@example.com> - 0.92.1-2 - Rebuilt for https://fedoraproject.org/wiki/Fedora_15_Mass_Rebuild * Wed Oct 06 2010 David A. Wheeler <firstname.lastname@example.org> 0.92.1-1 - Update to version 0.92.1. This means: - New built-in syntax for the theory of arrays - Fixes a bug in the arithmetic module - Allows folding and unfolding of predicate definitions * Tue Jun 08 2010 David A. Wheeler <email@example.com> 0.91-1 - Update to version 0.91. This means: - partial support for non-linear arithmetics - support case split on integer variables - new support for Euclidean division and modulo operators * Tue Aug 04 2009 Alan Dunn <firstname.lastname@example.org> 0.9-2 - Added ExcludeArch sparc64 due to no OCaml * Fri Jul 24 2009 Alan Dunn <email@example.com> 0.9-1 - New upstream version - Removed code for check for Fedora version (8) that is EOL - Removed comments re: CeCILL-C license as it is ok to have (no rpmlint warnings to explain either). * Wed Jun 17 2009 Karsten Hopp <firstname.lastname@example.org> 0.8-5.1 - ExcludeArch s390x as there's no ocaml available * Mon Feb 23 2009 Fedora Release Engineering <email@example.com> - 0.8-5 - Rebuilt for https://fedoraproject.org/wiki/Fedora_11_Mass_Rebuild * Wed Dec 24 2008 Alan Dunn <firstname.lastname@example.org> 0.8-4 - Rebuild: Source upstream appears to have changed even with same version number (seems like bug fix from examination of changes) - Changed hardcoded version number in source string * Fri Sep 05 2008 Alan Dunn <email@example.com> 0.8-3 - Fixed BuildRequires to add prelink (for execstack). * Tue Aug 26 2008 Alan Dunn <firstname.lastname@example.org> 0.8-2 - Fixed BuildRequires to add ocaml-ocamlgraph-devel instead of ocaml-ocamlgraph, made other minor changes. * Mon Aug 25 2008 Alan Dunn <email@example.com> 0.8-1 - Initial Fedora RPM version.
/usr/bin/alt-ergo /usr/share/alt-ergo /usr/share/alt-ergo/smt_prelude.mlw /usr/share/doc/alt-ergo-0.93 /usr/share/doc/alt-ergo-0.93/CHANGES /usr/share/doc/alt-ergo-0.93/COPYING /usr/share/doc/alt-ergo-0.93/CeCILL-C /usr/share/doc/alt-ergo-0.93/README.alt-ergo /usr/share/man/man1/alt-ergo.1.gz
Generated by rpm2html 1.8.1
Fabrice Bellet, Mon May 20 07:38:10 2013