Changelog
=========
Version 1.4.2
-------------

Build system
  * regenerated using a recent version of Autoconf

Version 1.4.1
-------------

Coq back-end
  * registered a few more theorems

Whole engine
  * fixed crash on negative literals in rewriting rules

Version 1.4.0
-------------

Syntax
  * changed precedence of unary minus,
    e.g., ``- 1`` is parsed as ``-(1)``, ``-1*x`` as ``(-1)*x``,
    ``- 1*x`` as ``-(1*x)``, ``-x*1`` as ``-(x*1)``
  * allowed ``;`` as a separator for interval bounds, e.g., ``[1;2]``
  * allowed ``p`` as exponent after a decimal integer, e.g., ``1p2``

Proof paths
  * decreased amount of pointless lemmas

Documentation
  * moved to reST

Build system
  * added support for DESTDIR during installation

Licensing
  * updated CeCILL from 2.0 to 2.1 and GPL from 2 to 3

Version 1.3.5
-------------

Whole engine
  * fixed crash on Windows 64-bit builds

Version 1.3.4
-------------

Build system
  * fixed compilation of a MinGW binary using a Cygwin toolchain

Version 1.3.3
-------------

Coq back-end
  * prepared for Flocq 3.0

Build system
  * fixed some STL debug failures

Version 1.3.2
-------------

Proof graph
  * fixed loss of information on some complicated hypotheses

Version 1.3.1
-------------

Fact database
  * improved handling of division

Proof graph
  * fixed loss of information for some case splits

Version 1.3.0
-------------

Arithmetic
  * added support for floating-point formats without minimal exponent

Proof graph
  * allowed dichotomy on variables without any known range
  * improved handling of half-bounded intervals

Proof paths
  * added heuristic for automatically selecting one variable for dichotomy

Main interface
  * added option ``-Eno-auto-dichotomy`` to disable the heuristic above
  * reduced amount of warnings in case of dichotomy failures
  * improved validity checking of rewriting rules

Version 1.2.2
-------------

Arithmetic
  * fixed incorrect error computation for negative inputs of ``float<zr>``

Version 1.2.1
-------------

Proof graph
  * sped up simplification of large proofs

Coq back-end
  * fixed garbled generation of some theorem calls

Version 1.2.0
-------------

Fact database
  * improved handling of powers of two in ``mul_flt``
  * fixed incorrect computation of the order-3 term of the relative error for division
  * added rewriting rules for emulating reverse propagation

Proof graph
  * improved proof simplification

Proof paths
  * improved performances by avoiding some absolute values
  * improved detection of approximate/exact pairs of expressions

Version 1.1.2
-------------

Back-ends
  * fixed missing proof parts with the LaTeX back-end

Main interface
  * fixed confusing message in case of failure

Version 1.1.1
-------------

Arithmetic
  * fixed incorrect error computation for some uncommon bound values

Back-ends
  * fixed crash on useless leaves with undefined properties

Version 1.1.0
-------------

Proof graph
  * added detection and avoidance of slow convergence

Main interface
  * added option ``-Echange-threshold`` to control detection of slow convergence

Version 1.0.0
-------------

Syntax
  * recognized ``e <> 0`` for inputting ``NZR`` properties

Fact database
  * added some new theorems for ``NZR``

Back-ends
  * added a back-end producing LaTeX files
  * disabled HOL Light back-end as it was not used
  * enabled automatic dichotomy and formula reduction

Proof graph
  * allowed arbitrary formulas as output of nodes

Main interface
  * removed option ``-Msequent`` as formulas are handled as a whole now

Version 0.18.0
--------------

Main interface
  * removed option ``-Mexpensive``
  * added more details to ``-Mstatistics``

Proof graph
  * improved performances
  * improved proof simplification

Coq back-end
  * fixed incorrect theorem name for square root

Version 0.17.1
--------------

Build system
  * fixed issues with MacOSX, BSD, and compilation flags

Version 0.17.0
--------------

Build system
  * switched to ``remake``

Fact database
  * added theorems relating the ranges of two expressions, given the relative error between them
  * simplified squaring

Proof graph
  * allowed logic simplifications, even in case of indeterminate intervals

Documentation
  * added list of theorems

Version 0.16.6
--------------

Coq lambda back-end
  * fixed crash on goals that are trivial implications

Version 0.16.5
--------------

Arithmetic
  * fixed incorrect round-off error for values close to zero

Version 0.16.4
--------------

Proof graph
  * fixed crash when dichotomy fails to prove properties other than ``BND``

Version 0.16.3
--------------

Proof graph
  * fixed crash when performing dichotomy while there are properties other than ``BND``

Version 0.16.2
--------------

Coq lambda back-end
  * fixed incorrect certificate for intersection lemmas

Version 0.16.1
--------------

Proof graph
  * fixed segfault when splitting cases on a degenerate goal
  * reenabled logic reasoning for ``ABS`` and ``REL`` predicates

Coq lambda back-end
  * fixed signature of theorem ``mul_firs``

Version 0.16.0
--------------

Coq lambda back-end
  * fixed syntax of proofs containing no variables
  * fixed typing of some floating-point constants
  * fixed signature of theorems ``rel_refl``, ``div_fil``, ``div_fir``

Coq script back-end
  * fixed typing of some floating-point constants
  * fixed syntax for Coq support library 0.17

Fact database
  * added support for proving equalities between constants
  * changed ``fixed_of_fix`` so that it produces an ``EQL`` property

Version 0.15.1
--------------

Fact database
  * fixed broken simplification of ``a*b -/ c*b``

Version 0.15.0
--------------

Fact database
  * added ``EQL`` predicate: ``e1 = e2``
  * changed user rewriting to use the ``EQL`` predicate
  * improved rewriting rules to handle ``ABS``, ``FIX``, ``FLT``, ``NZR``, ``REL``
    in addition to ``BND`` predicate

Syntax
  * added ``@FLT(e,k)`` and ``@FIX(e,k)`` for inputting ``FLT`` and ``FIX`` properties
  * added ``e1 = e2`` for inputting ``EQL`` properties
  * allowed arbitrary logical propositions as termination condition for bisection

Version 0.14.1
--------------

Build system
  * fixed some platform-specific issues

Version 0.14.0
--------------

Coq back-end
  * added support for Coq support library 0.14

Version 0.13.0
--------------

Coq lambda back-end
  * simplified generated proofs

Proof graph
  * disabled sequent generation
  * disabled proof tracking for the null back-end
  * improved handling of deep logic negations
  * handled disjunctions by dichotomies (null back-end only)

Main interface
  * removed option ``-Monly-failure`` since there is only one proposition

Documentation
  * switched from ``jade`` to ``dblatex``

Version 0.12.3
--------------

Coq lambda back-end
  * fixed incorrect invocation of some theorems

Arithmetic
  * fixed incorrect proofs for floating-point error near powers of two

Version 0.12.2
--------------

Back-ends
  * fixed output of underspecified ``REL`` goals

Version 0.12.1
--------------

Proof graph
  * fixed sequents with empty goals not being recognized as proved

Main interface
  * added option ``-Msequent`` to display goals as Gappa scripts
  * added option ``-Monly-failure`` to limit output to failing goals
  * improved display of extremely small/big bounds
  * improved display of rounding operators

Proof paths
  * fixed inequalities (lower bound) on absolute values being ignored

Arithmetic
  * improved relative operators handling when exponents are not constrained

Version 0.12.0
--------------

Back-ends
  * added back-end for producing Coq lambda terms
    (support is limited to what the Coq tactic can handle)

Proof graph
  * fixed handling of complicated goals

Main interface
  * added output of failed subgoals

Version 0.11.3
--------------

Coq back-end
  * applied correct theorems for intervals with infinite bounds

Version 0.11.2
--------------

Parser
  * fixed handling of CRLF end of line

Version 0.11.1
--------------

Main interface
  * removed error code on options ``--help`` and ``--version``

Version 0.11.0
--------------

Proof graph
  * avoided splitting provably-singleton intervals
  * added score system for favoring successful schemes

Arithmetic
  * tightened rounding error when applied to short values

Proof paths
  * recognized lhs of user rewriting as potential user approximate

Syntax
  * added ``x -/ y in ...`` and ``|x -/ y| <= ...`` for ``REL`` properties

Build system
  * fixed compilation on Cygwin

Version 0.10.0
--------------

Proof graph
  * avoided infinite dichotomy on some unprovable propositions

Back-ends
  * fixed generation of subset facts

Fact database
  * reduced cycles in theorems

Main interface
  * added ``-Mschemes`` option for generating ``.dot`` scheme graphs
  * allowed input filename on command line

Version 0.9.0
-------------

Syntax
  * added constraints on user rewriting, e.g., ``x -> 1/(1/x) { x <> 0 }``

Whole engine
  * added detection of assumed facts in ``-Munconstrained mode``

Fact database
  * added relative error propagation through division

Back-ends
  * fixed cache collisions between theorems

Proof graph
  * fixed intersection of relative errors
  * enabled bound simplification through rewriting rules
  * fixed handling of half-bounded goals

Version 0.8.0
-------------

HOL Light back-end
  * added new back-end

Proof graph
  * added option ``-Mexpensive`` to select best paths on length

Fact database
  * added predicate ``REL``: ``x = y * (1 + e)``
  * replaced rewriting rules on relative error by computations on REL
  * enhanced path finder to fill holes in theorems
  * put back rewriting rules to theorem level
  * fixed incorrect equality of variables
  * added predicate ``NZR``: ``x <> 0``
  * added propagation of ``FIX`` and ``FLT`` through rounding operators

Version 0.7.3
-------------

Fact database
  * generalized rounding theorems to any combination of errors and predicates

Whole engine
  * removed dependencies between sequents

Parser
  * removed automatic rounding of negated expressions
  * equated numbers with exponent zero but different radices
  * fixed grammar for multiple splits

Proof graph
  * improved quality of fixed split

Version 0.7.2
-------------

Parser
  * fixed incorrectly rounded intervals on input

Fact database
  * restricted domain of some rewriting rules

Version 0.7.1
-------------

Fact database
  * added error propagation through opposite, division, and square root

Coq back-end
  * fixed confusion between nodes from different proof graphs
  * optimized away trivial goal nodes

Version 0.7.0
-------------

Coq back-end
  * updated to support Gappa library version 0.1

Proof graph
  * added optimization pass for bound precision

Whole engine
  * simplified back-end handling

Version 0.6.5
-------------

Coq back-end
  * fixed square root generation

Fact database
  * disabled square root of negative numbers

Syntax
  * added ``fma(a,b,c)`` as a synonym for ``a*b+c``

Arithmetic
  * added ``fma_rel``

Main interface
  * added ``-Ereverted-fma`` option to change the meaning of ``fma(a,b,c)`` to ``c+a*b``

Version 0.6.4
-------------

Arithmetic
  * fixed influence zone again for floating-point absolute error

Version 0.6.3
-------------

Proof graph
  * fixed failure when an inequality leads to a contradiction
  * added support for intersecting ``ABS`` predicates

Hint parser
  * added detection of useless hints

Parser
  * normalized numbers with fractional part ending by zero

Version 0.6.2
-------------

Fact database
  * fixed dependencies of rewriting rules relying on non-zero values;
    a race could lead to failed theorems
  * added formulas to compute the relative error of a sum

Arithmetic
  * added new directed rounding: to odd, away from zero
  * added new rounding to nearest with tie breaking: to odd, to zero, away from zero, up, down
  * fixed influence zone for floating-point absolute error

Version 0.6.1
-------------

Proof paths
  * improved detection of dead paths

Fact database
  * fixed patterns for generalized rounding operators
  * improved rewriting rules for approx/accurate pairs
  * renamed rewriting rules

Version 0.6.0
-------------

Syntax
  * added ways of specifying how interval splitting is done
  * added detection of badly-formed intervals in propositions
  * removed limitation on multiple hypotheses about the same expression
  * improved heuristic for detecting approx/accurate pairs
  * removed limitation on number of accurate expressions for a given approximate
  * removed hack for accurate expressions of rounded expressions (potentially disruptive)

Whole engine
  * added inequalities; as hypotheses, they cannot imply theorems but they
    can restrict computed ranges

Proof paths
  * put rewriting schemes to a higher level to remove constraints on approx/accurate pairs
  * added rewriting rules for replacing an accurate expression by an approximate and an error

Version 0.5.6
-------------

Fact database
  * cleaned theorems and removed redundant ones

Arithmetic
  * enabled test to zero with relative rounding; it can still be disabled
    by ``-Munconstrained``

Coq back-end
  * improved script generation

Proof graph
  * fixed premature halt when a case split was a failure
  * fixed case split not noticing newly discovered bounds

Main interface
  * simplified display of hypotheses and sorted display of goals

Version 0.5.5
-------------

Whole engine
  * added square root (no rule checking though)
  * modified rewriting rules to apply to approximates instead of just rounded values
  * added ``ABS`` predicate to workaround abuse of absolute values in theorems

Syntax
  * added syntax to define user approximates

Fact database
  * added option to disable constraint checking around zero

Arithmetic
  * generalized fixed-point range enforcing to any expression

Proof paths
  * enhanced the detection of dead paths that contain cycles

Version 0.5.4
-------------

Syntax
  * reduced the number of false-positive for unbound identifiers
  * merged variables and functions anew in order to correctly detect define-after-uses errors

Proof graph
  * added fifo processing of proof schemes
  * handled case splitting on empty goals
  * added more general schemes for case splitting

Hint parser
  * shut up warning messages about trivial integers as denominator

Version 0.5.3
-------------

Proof graph
  * fixed goal removal: undefined goals require "optimal" solutions

Version 0.5.2
-------------

Proof graph
  * simplified node memory handling
  * simplified graph handling
  * put dichotomy at a higher level, outside of proof schemes
  * replaced hypothesis property vectors by bit vectors, stored in-place if possible

Syntax
  * added detection of unbound identifiers

Whole engine
  * added support for complex logical properties

Version 0.5.1
-------------

Whole engine
  * added ``FIX`` and ``FLT`` predicates in addition to the original ``BND`` predicate

Version 0.5.0
-------------

Whole engine
  * generalized rounding modes as functions
  * generalized functions with rounding theorems
  * removed default rounding theorems

Syntax
  * split variables and functions
  * simplified rounding and function syntax: purely C++-template-like syntax
  * added NOT and OR logical operators

Arithmetic
  * replaced relative rounding by functions
  * factored number rounding handling
  * added fixed-point arithmetic
  * generalized floating-point rounding modes to any triplet (precision,
    subnormal smallest exponent, direction)

Proof graph
  * reduced the number of node types by demoting theorem and axiom nodes to internal facts

Version 0.4.12
--------------

Syntax
  * added a way to define new names for rounding operators
  * simplified the handling of negative numbers

Coq back-end
  * fixed representation of relative rounding

Version 0.4.11
--------------

Proof graph
  * fixed a missing dependency cleanup for an owned union node

Main interface
  * added parsing of embedded options

Version 0.4.10
--------------

Proof graph
  * changed the node hypotheses to be graph hypotheses

Fact database
  * switched some other facts to the absolute value of the denominators
  * added an explicit exclusion pattern for the rewriting rules
    (e.g., ``x * x`` is no more excluded)

Main interface
  * added basic command-line parsing for warnings and parameters

Version 0.4.9
-------------

Numbers and arithmetic
  * separated number handling from special arithmetic
  * added ``relative``, a format for handling varying precision rounding

Formulas
  * implemented absolute value

Fact database
  * made relative error depends on absolute value of the range

Proof graph
  * fixed a bug related to the clean-up of the last graph of a dichotomy
  * strengthened the role of modus nodes

Version 0.4.8
-------------

Fact database
  * tightened intervals for ``a + b + a * b``
  * discarded multiple occurrences of the same term in the rewriting rules
  * cleaned up rewriting rules

Version 0.4.7
-------------

Hint parser
  * sped up verification

Version 0.4.6
-------------

Floating-point numbers
  * disabled relative error for subnormal numbers (potentially disruptive)

Homogen numbers
  * cleaned up
  * added non-homogen double rounded format

Hint parser
  * added pseudo-support for quotient in hint

Parser
  * added support for C99 hexadecimal floating-point format

Proof graph
  * replaced useless empty intersections by contradiction proofs

Version 0.4.5
-------------

Proof graph
  * reworked modus ponens creation to fix an assertion failure in lemma invocation

Fact database
  * added conditional rules (potentially disruptive)

Homogen numbers
  * split roundings between initialization and computation

Coq back-end
  * implemented union