1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63
|
version 0.91, May 19th, 2010
===============================
o experimental support for the theory of functional polymorphic
arrays with the -arrays option
o the -pairs option should now be used for the built-in support of
polymorphic pairs
o support the equality part of the omega test with the -omega option
o partial support for non-linear arithmetics
o support case split on integer variables
o new support for Euclidean division and modulo operators
o new environment variable ERGOLIB to specify the library directory
version 0.9, July 17th, 2009
===============================
o support AC symbols
o support for C-like hexadecimal floating-point constants
o handle the division operator
version 0.8, July 21th, 2008
===============================
o pretty output with the -color option
o the SAT solver part is now equipped with a backjumping mechanism
o now handles the flet and let SMT-lib constructs
o goal directed strategy
o pruning strategy (-select option)
o incremental strategy for instantiation of lemmas
o fail if a parameter is bound twice in a definition
o treatment of existential formulas have been slightly improved
o decision procedure for polymorphic pairs
o decision procedure for bit-vectors
o combination scheme for several decision procedures
version 0.7.3, March 5th, 2008
===============================
o renamings in the interfaces
o provides an API for alt-ergo (make api or make api.byte)
o handles the modulo operator (%) as an uninterpreted symbol
o allow labels on any term, not only on predicates
version 0.7, October 11th, 2007
===============================
o trigger construction has been improved
o preliminary implementation of combination scheme (Arithmetic+pairs)
o the SAT loop has been improved
version 0.6, February 1st, 2007
===============================
o new CC(X) architecture (it can know directly handle relation symbols)
o fully handles the polymorphism of the logic
version 0.5, October 12th, 2006
===============================
o first (beta) release
Local Variables:
mode: text
End:
|