The solver supports:
- Boolean
- Linear arithmetic (using Fourier-Mostkin)
- Uninterpreted symbols
- Quantifiers
- Polymorphism
In a limited way:
- Floating Point numbers
- Function ceil and floor
2021: Colibri2 0.1
The solver supports:
In a limited way:
2020: Colibri2
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:
2019: Colibrics
Colibrics started as an experiment on the possibility to prove a simple CP solver in Why3
2016: Popop
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.
2014: SOPRANO
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.
2000: First COLIBRI
COLIBRI started as a COnstraint solving LIBrary in Eclipse Prolog