colibrics tags
https://git.frama-c.com/pub/colibrics/-/tags
2023-02-06T12:13:13Z
https://git.frama-c.com/pub/colibrics/-/tags/0.4
0.4
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
<h2 data-sourcepos="1:1-1:14" dir="auto">
<a id="user-content-release-04" class="anchor" href="#release-04" aria-hidden="true"></a>Release 0.4</h2>
<ul data-sourcepos="2:3-9:0" dir="auto">
<li data-sourcepos="2:3-2:44">Decision: Fix delayed decisions handling</li>
<li data-sourcepos="3:3-3:30">Array: experimental theory</li>
<li data-sourcepos="4:3-4:53">Quantifier: Improve eager instanciation heuristic</li>
<li data-sourcepos="5:3-5:39">Quantifier: Avoid creating new term</li>
<li data-sourcepos="6:3-6:30">Simplex: Fix redundant run</li>
<li data-sourcepos="7:3-7:28">Fix compilation in 32bit</li>
<li data-sourcepos="8:3-9:0">Fix sign of sqrt</li>
</ul>
2023-02-06T12:13:13Z
François Bobot
https://git.frama-c.com/pub/colibrics/-/tags/0.3.3
0.3.3
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
<h2 data-sourcepos="1:1-1:16" dir="auto">
<a id="user-content-release-033" class="anchor" href="#release-033" aria-hidden="true"></a>Release 0.3.3</h2>
<ul data-sourcepos="2:3-7:0" dir="auto">
<li data-sourcepos="2:3-2:25">Bump cmdliner version</li>
<li data-sourcepos="3:3-3:22">Bump OCaml version</li>
<li data-sourcepos="4:3-4:32">Remove some warnings in 4.14</li>
<li data-sourcepos="5:3-5:25">Fix OUnit2 dependency</li>
<li data-sourcepos="6:3-7:0">Support 32bit by removing large integer constant</li>
</ul>
2022-06-19T17:22:21Z
François Bobot
https://git.frama-c.com/pub/colibrics/-/tags/0.3.2
0.3.2
Release 0.3.2
CHANGES:
* Add missing dependencies
<p data-sourcepos="1:1-1:13" dir="auto">Release 0.3.2</p>
<p data-sourcepos="3:1-3:8" dir="auto">CHANGES:</p>
<ul data-sourcepos="5:3-7:0" dir="auto">
<li data-sourcepos="5:3-7:0">Add missing dependencies
Fix missing dependencies</li>
</ul>
2022-06-19T09:50:04Z
François Bobot
https://git.frama-c.com/pub/colibrics/-/tags/0.3.1
0.3.1
Release 0.3.1
CHANGES:
* Add lower bounds for dependencies
* Attach tests to corresponding packages
François Bobot
https://git.frama-c.com/pub/colibrics/-/tags/0.3
0.3
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
<p data-sourcepos="1:1-1:15" dir="auto">Initial release</p>
<h3 data-sourcepos="3:1-3:12" dir="auto">
<a id="user-content-colibri2" class="anchor" href="#colibri2" aria-hidden="true"></a>Colibri2</h3>
<ul data-sourcepos="4:3-14:0" dir="auto">
<li data-sourcepos="4:3-4:39">polymorphism, recursive definitions</li>
<li data-sourcepos="5:3-5:39">quantifiers (eager, multi-triggers)</li>
<li data-sourcepos="6:3-6:48">algebraic datatypes (except cycle detection)</li>
<li data-sourcepos="7:3-7:68">Reals: union of interval domain (proved in why3 with Colibrilib)</li>
<li data-sourcepos="8:3-9:14">Reals: normalization sum, product, some factorization, Fourier-Motskin
or Simplex</li>
<li data-sourcepos="10:3-10:14">Reals: abs</li>
<li data-sourcepos="11:3-11:39">Int: floor, ceil, abs, Real <-> Int</li>
<li data-sourcepos="12:3-12:77">Floating point: evaluation and some simple propagation (Arthur Correnson)</li>
<li data-sourcepos="13:3-14:0">Bitvectors: only evaluation</li>
</ul>
<h3 data-sourcepos="15:1-15:13" dir="auto">
<a id="user-content-colibrics" class="anchor" href="#colibrics" aria-hidden="true"></a>Colibrics</h3>
<ul data-sourcepos="16:3-18:0" dir="auto">
<li data-sourcepos="16:3-16:10">engine</li>
<li data-sourcepos="17:3-18:0">simple constraints</li>
</ul>
<h3 data-sourcepos="19:1-19:14" dir="auto">
<a id="user-content-colibrilib" class="anchor" href="#colibrilib" aria-hidden="true"></a>Colibrilib</h3>
<ul data-sourcepos="20:3-22:14" dir="auto">
<li data-sourcepos="20:3-20:12">interval</li>
<li data-sourcepos="21:3-21:21">union of interval</li>
<li data-sourcepos="22:3-22:14">congruence</li>
</ul>
2022-06-18T21:26:38Z
François Bobot