Changelog

Version 1.6.0

Fact database
  • fixed add_flt_lin and add_flt_lin_rev

  • changed some rewriting rules about quotients into rules about LIN

Arithmetic
  • removed support for homogeneous and relative rounding functions

Version 1.5.0

Fact database
  • added predicate LIN: x = y * e

  • used LIN(a, b) for properties of the kind BND(a / b)

  • generalized Sterbenz-like theorems

  • specified x / 0 as being equal to 0, which removes some NZR hypotheses

Syntax
  • added binary operator // to denote LIN properties

Back-ends
  • added a back-end to produce D2 files

Coq script back-end
  • removed the use of Notation as it causes a huge slowdown in the prover

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