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
- Proof paths
- decreased amount of pointless lemmas
- Documentation
-
- 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
-
- 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
-
- 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
-
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
-
- 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
-
- 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
-
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
-