Makes both signed and unsigned operations, which have
slightly different pre-conditions.
Further improvement needed: overflow checks are still
using functions `to_int` or `to_uint`, which are not
suitable for SMT solvers with bit-vector support.
* declare range types and float types,
* use integer (resp. real) literals for those types through casting,
* specify how to print them in drivers.
Change in syntax
* use
type t = < range 1 2 > (* integers from 1 to 2 *)
type t' = < float 4 12 > (* float with 4 bits in exponent and 12 in mantissa *)
the two projections :
t'int
t''real
and the predicate :
t''isFinite
* Restrict the use of "'" in whyml:
Users are not allowed to introduce names where a quote symbol
is followed by a letter. Thus, the following identifiers are
valid:
t'
toto'0''
toto'_phi
whereas toto'phi is not.
Note: we do not yet support negative numbers in range declaration
and casting of a literal.
+ size -> size_bv
+ size_int -> size
+ change two_power_size and max_int definitions
+ add axioms to BVConverter
+ new axiom relating nth and nth_bv
+ some reorganisation
- update coq realisation
- modify in consequence the relevant examples and pull the completed ones out of in_progress
