Release 0.3
CHANGES:
initial release
* polymorphism, recursive definitions
* quantifiers (eager, multi-triggers)
* algebraic datatypes (except cycle detection)
* Reals: union of interval domain (proved in why3 with Colibrilib)
* Reals: normalization sum, product, some factorization, Fourier-Motskin
or Simplex
* Reals: abs
* Int: floor, ceil, abs, Real <-> Int
* Floating point: evaluation and some simple propagation (Arthur Correnson)
* Bitvectors: only evaluation
* engine
* simple constraints
* interval
* union of interval
* congruence
Initial release
Colibri2
- polymorphism, recursive definitions
- quantifiers (eager, multi-triggers)
- algebraic datatypes (except cycle detection)
- Reals: union of interval domain (proved in why3 with Colibrilib)
- Reals: normalization sum, product, some factorization, Fourier-Motskin or Simplex
- Reals: abs
- Int: floor, ceil, abs, Real <-> Int
- Floating point: evaluation and some simple propagation (Arthur Correnson)
- Bitvectors: only evaluation
Colibrics
- engine
- simple constraints
Colibrilib
- interval
- union of interval
- congruence