Tags

Release 0.4

CHANGES:

  * Decision: Fix delayed decisions handling
  * Array: experimental theory
  * Quantifier: Improve eager instanciation heuristic
  * Quantifier: Avoid creating new term
  * Simplex: Fix redundant run
  * Fix compilation in 32bit
  * Fix sign of sqrt

Release 0.3.3

CHANGES:

  * Bump cmdliner version
  * Bump OCaml version
  * Remove some warnings in 4.14
  * Fix OUnit2 dependency
  * Support 32bit by removing large integer constant

Release 0.3.2

CHANGES:

  * Add missing dependencies

Release 0.3.1

CHANGES:

  * Add lower bounds for dependencies
  * Attach tests to corresponding packages

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