COLIBRI handles the elements at an higher level than many other solvers. For example for each floating point number (IEEE) it keeps its possible values in an interval, and other flags such as if it is integral. It propagates this information through the formula.
For example for the 64bit floating-point addition:
COLIBRI good for because
Example: x-y=0.1 => x \in [..;..] /\ y \in [..,..]
Colibrics proved in why3
COLIBRI started as a COnstraint solving LIBrary in Eclipse Prolog
The ANR SOPRANO project allowed to gather researchers working on SMT (OcamlPro, Université Paris-Saclay) and CP (CEA, INRIA) and industrials partner (Adacore) in the domain of software verification. The goal was to merge the powerful learning of SMT and the powerful propagations of CP.
Popop, developped during the SOPRANO project, is a framework that combined the learning of SMT and the propagation of CP. However the learning framework was to cumbersome to allow the developpement of more complicated theories than booleans and linear arithmetic.
Colibrics started as an experiment on the possibility to prove a simple CP solver in Why3
The learning developed in Popop is removed to keep only the propagation part as in COLIBRI. So the solver is named Colibri2. The first features to be available are:
The solver supports:
In a limited way: