Add colibri2 support

[hra687261]

With this PR, you'll be able to use Colibri2 instead of Z3 using the command line option -p colibri2
Support for optimization with ocplib_simplex (The simplex library used by both Colibri2 and Alt-Ergo) is incomplete, I'll take a better look at how to properly do it in another time (or someone else can if they're motivated)
Currently it's necessary to pin Colibri2 on the master branch in https://git.frama-c.com/pub/colibrics

[filipeom]

The way I encoded this using Z3 was for the expressions es to not be added to the solver. Because, IIRC Z3's check actually behaves like a check-sat-assuming with the argument es being the assumptions.

Do you think this will be problematic? We should probably add a label to es something like: Val check : solver -> assumptions:expr list to make this more clear

[filipeom]

Btw, you don't need to support the optimization module. I just implemented it here to play with linear programming for an algorithms course project.

But if I find time in the next few weeks, I'd probably like to give it a go. I'm interested in seeing the performance when compared with Z3's optimize (which was horrible for my use cases)

[hra687261]

@filipeom It seems that the CI can't install some of Colibri2's external dependencies on mac-os, so that's problematic :( I'll see what can be done about that

cf: bobot/ocaml-flint#7

[filipeom]

@filipeom It seems that the CI can't install some of Colibri2's external dependencies on mac-os, so that's problematic :( I'll see what can be done about that

cf: bobot/ocaml-flint#7

I also can't install it locally on arch. Not even with the patch you linked 😔

What we can do is make colibri2_mappings an optional library and declare colibri2 as a depopts. This way, we can merge this so you don't have to rebase all the time. I can play with this. What do you think?

[hra687261]

Yes, I agree, that seems like a good solution for now.

[filipeom]

Got it. I'll also rebase my useless commits. Thanks a bunch for your help. I really appreciate it! And sorry again for any disruptions this afternoon. Won't happen again :)

[hra687261]

No worries at all :)