Add Alt-Ergo

[hra687261]

This PR adds support for the Alt-Ergo SMT solver, it was tested on collections-c (results below) with a 2s timeout.

It currently depends on my branch of Alt-Ergo, so maybe we should wait for OCamlPro/alt-ergo#1259 to be merged so it can depend on the official Alt-Ergo repository? (Or I'll just do another PR when that is case)

I am a bit surprised with the results, since the tests seemed pretty simple, it shouldn't take so much time. I'll investigate at a later time why it isn't better, if it's just the solver or something I did wrong in the mapping.

STAT:
provers      │smtml-colibri2│smtml-alt-ergo
─────────────┼──────────────┼──────────────
sat          │2774          │2820
─────────────┼──────────────┼──────────────
unsat        │1216          │1387
─────────────┼──────────────┼──────────────
sat+unsat    │3990          │4207
─────────────┼──────────────┼──────────────
errors       │0             │0
─────────────┼──────────────┼──────────────
valid_proof  │0             │0
─────────────┼──────────────┼──────────────
invalid_proof│0             │0
─────────────┼──────────────┼──────────────
unknown      │558           │0
─────────────┼──────────────┼──────────────
timeout      │0             │341
─────────────┼──────────────┼──────────────
memory       │0             │0
─────────────┼──────────────┼──────────────
total        │4548          │4548
─────────────┼──────────────┼──────────────
total_time   │2m59.5s       │9m37s
ANALYSIS:
provers      │smtml-colibri2│smtml-alt-ergo
─────────────┼──────────────┼──────────────
improved     │3990          │4207
─────────────┼──────────────┼──────────────
ok           │558           │0
─────────────┼──────────────┼──────────────
disappoint   │0             │0
─────────────┼──────────────┼──────────────
bad          │0             │0
─────────────┼──────────────┼──────────────
valid proof  │0             │0
─────────────┼──────────────┼──────────────
invalid proof│0             │0
─────────────┼──────────────┼──────────────
errors       │0             │0
─────────────┼──────────────┼──────────────
total        │4548          │4548

[filipeom]

Thank you so much for this @hra687261! Unfortunately, we probably won't have time to include it in the paper as we're trying to close the evaluation today 😞

It currently depends on my branch of Alt-Ergo, so maybe we should wait for OCamlPro/alt-ergo#1259 to be merged so it can depend on the official Alt-Ergo repository? (Or I'll just do another PR when that is case)

However you prefer, we can merge as soon as CI is happy. Or, we can wait for the Alt-Ergo PR to be merged. Please, let me know what you prefer.

I am a bit surprised with the results, since the tests seemed pretty simple, it shouldn't take so much time. I'll investigate at a later time why it isn't better, if it's just the solver or something I did wrong in the mapping.

Yes, I'm also a bit surprised. I was expecting the results to be in line with Colibri’s. There's probably something that was overlooked. I can try installing Alt-Ergo on my machine and compare the execution times with this PR, but I'm okay with merging this as is.

On another note, I’m not sure if you’ve seen this already, but we now have a more simplified way of creating mappings. Essentially, the solver mappings only need to comply with this interface:

smtml/src/mappings_intf.ml

Line 25 in 3ce9451

module type M = sig

They just need to provide the mappings to the logic's operators and then compose it with the Mappings.Make functor:

smtml/src/z3_mappings.default.ml

Line 563 in 3ce9451

include Mappings.Make (M)

For example, see z3_mappings.default.ml.

Do you think it would be a lot of work to apply this to Colibri2 and Alt-Ergo? I could probably give it a shot in a future PR and ask you to review it, if you don’t mind?

[hra687261]

Unfortunately, we probably won't have time to include it in the paper as we're trying to close the evaluation today 😞

No problem! Leo asked for this a long time ago anyway haha

However you prefer, we can merge as soon as CI is happy. Or, we can wait for the Alt-Ergo PR to be merged. Please, let me know what you prefer.

I think we can merge when the CI passes, I'll open a new PR as soon as that other one is merged.

On another note, I’m not sure if you’ve seen this already, but we now have a more simplified way of creating mappings. Essentially, the solver mappings only need to comply with this interface:

smtml/src/mappings_intf.ml

Line 25 in 3ce9451

module type M = sig

They just need to provide the mappings to the logic's operators and then compose it with the Mappings.Make functor:

smtml/src/z3_mappings.default.ml

Line 563 in 3ce9451

include Mappings.Make (M)

For example, see z3_mappings.default.ml.

Do you think it would be a lot of work to apply this to Colibri2 and Alt-Ergo? I could probably give it a shot in a future PR and ask you to review it, if you don’t mind?

At first sight I think it should be doable, but I am not 100% sure. Of course, I'd be happy to :)

[filipeom]

I think we can merge when the CI passes, I'll open a new PR as soon as that other one is merged.

Ok perfect thanks! I'll queue it up :)

At first sight I think it should be doable, but I am not 100% sure. Of course, I'd be happy to :)

Nice, thanks! If I find some courage in the next few weeks I'll ping you 😄

[hra687261]

OCamlPro/alt-ergo#1259 was merged.

And with some luck, the CI should be fixed after this...

[bclement-ocp]

Happy to finally see Alt-Ergo included here! Thanks @hra687261 :)

I assume the total time is not computed on timeouts, since there are 341 timeouts for Alt-Ergo and 341 * 2s = 11min22s. If some of the slow tests turn out to be Alt-Ergo problems (my intuition is that it might be bit-vector comparisons as there are known inefficiencies there, especially with signed comparisons -- this is on my todo list) please send issues our way and we'd be happy to look into it!

[zapashcanon]

Thanks a lot @hra687261! Can't wait to spam the alt-ergo team with performance-related questions! :D