package colibrics

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

Install

Dune Dependency

Authors

Maintainers

Sources

colibri2-0.4.tbz
sha256=fe298191f4ae6af7046c6dee617da0100eba1738b11f868290d905cd0055ae27
sha512=75aa7969bdbca6bef396e35d9660381c06ef21332730ecfb0a4dcc72596ef8575d5905ddd5341e0287e8e18a20db8df9d9894b698f98e11dfc6d26a183fc16f7

CHANGES.html

CHANGES

## Release 0.4
  * 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
  * 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
OCaml

Innovation. Community. Security.