package colibrics
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
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>