# Changelog¶

## 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`

- changed precedence of unary minus,
e.g.,
- 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

- added option

## Version 1.2.2¶

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

- fixed incorrect error computation for negative inputs of

## 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

- improved handling of powers of two in
- 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

- added option

## Version 1.0.0¶

- Syntax
- recognized
`e <> 0`

for inputting`NZR`

properties

- recognized
- Fact database
- added some new theorems for
`NZR`

- added some new theorems for
- 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

- removed option

## Version 0.18.0¶

- Main interface
- removed option
`-Mexpensive`

- added more details to
`-Mstatistics`

- removed option
- 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`

- switched to
- 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`

- fixed crash when dichotomy fails to prove properties other than

## Version 0.16.3¶

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

- fixed crash when performing dichotomy while there are properties other than

## 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`

- fixed signature of theorem

## 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`

- fixed broken simplification of

## 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

- added
- 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

- added

## 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

- removed option
- Documentation
- switched from
`jade`

to`dblatex`

- switched from

## 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

- fixed output of underspecified

## 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

- added option
- 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`

- removed error code on options

## 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

- added
- 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

- added

## Version 0.9.0¶

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

- added constraints on user rewriting, e.g.,
- Whole engine
- added detection of assumed facts in
`-Munconstrained mode`

- added detection of assumed facts in
- 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

- added option
- 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

- added predicate

## 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`

- added
- Arithmetic
- added
`fma_rel`

- added
- Main interface
- added
`-Ereverted-fma`

option to change the meaning of`fma(a,b,c)`

to`c+a*b`

- added

## 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`

- enabled test to zero with relative rounding; it can still be disabled
by
- 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

- added

## 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

- tightened intervals for

## 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