package colibrics

  1. Overview
  2. Docs
A CP solver proved in Why3

Install

Dune Dependency

Authors

Maintainers

Sources

colibri2-0.3.3.tbz
sha256=db4c79c00e02a9bd437844ca49b328938a4b774e7a7bd24a8d9e1eaba04f5abc
sha512=1fd0eca1aac1cda92828f8691765eca02a00e90c7758d33347436f4ae580776877121102d505ee72c4b68a55d1d6b591a29258616971ca80fba4d17e2c507d2e

CHANGES.html

CHANGES

## Release 0.3.3
  * 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
  * Add missing dependencies

## Release 0.3.1
  * Add lower bounds for dependencies
  * Attach tests to corresponding packages

## Release 0.3

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