feat(CDCL): Add ability to decide on semantic literals

[bclement-ocp]

This patch introduces the ability for the CDCL solver to deal with semantic literals. This is part of work towards #901 although it does not (yet) achieves the goals of #901.

More precisely:

• We add a new Literal module in structures to represent literals that are either syntaxic (represented by expressions) or semantic (represented using the Xliteral module).

• The new Literal module is used to represent the literals associated with the Atoms in the CDCL solver [1]

• The CDCL solver has a special handling of these semantic literals, which are treated as "local" literals: they are not added in the variable ordering, and will not be decided upon by the solver. Instead, a new mechanism inspired by mSAT (and, transitively, mcSAT) is provided, where the theory is able to mark certain literals as "immediate decisions". When literals are marked this way, the solver will decide on one of the marked literals the next time a decision must be made. Literals marked as immediate decisions are part of a transient solver state, and are forgotten upon backtracking.

• The theory uses this marking mechanism to communicate case splits (and a similar mechanism for optimization objectives, which is separate because the value of the objective is sent back to the theory once the decision is made) to the solver.

This mechanism allows to introduce splits that are, in a way, "local", and do not pollute other branches of the solver. It can be seen as an intermediate step towards a mcSAT approach, but where we are still deciding on boolean literals and hence try to avoid adding a large number of splits globally into the solver -- although it does mean that the splits are not incorporated into the activity heuristic.

The functionality is currently gated behind a new flag --enable-sat-cs.

Note that with --enable-sat-cs this change is +46-13 on ae-format (and +8-7 on benchtop-tests) or a net positive of +33 on ae-format, so we might want to enable it by default.

[1] : It could also be used for the Bjs in the Tableaux solver, if we
wanted to suport similar features in the Tableaux solver.

[bclement-ocp]

I forgot to mention but: the --enable-sat-cs flag currently only applies to the Arrays theory, because for some theories (e.g. integers) it leads to regressions, probably due to polluting the main environment too much with irrelevant decisions. Further work towards #901 should investigate strategies to gradually move the other theories to this mechanism without introducing regressions (the enum and bit-vector theories should be prime candidates).

[bclement-ocp]

So it turns out that I forgot to reset the number of choices when backtracking, which means that we reply "sat" from satML too early, which in turns means we are more aggressive with instantiation, and that seems to be beneficial somehow, since we get an improvement… but doing what should be the right thing (i.e. actually counting semantic decisions properly) causes large regressions (+69-137). I will investigate next week.

[bclement-ocp]

So it turns out that I forgot to reset the number of choices when backtracking, which means that we reply "sat" from satML too early, which in turns means we are more aggressive with instantiation, and that seems to be beneficial somehow, since we get an improvement… but doing what should be the right thing (i.e. actually counting semantic decisions properly) causes large regressions (+69-137). I will investigate next week.

Turns out I made a typo while rebasing: d708f33

Rerunning the benches.

[bclement-ocp]

The benches now say +49-14 with the correct code rebased on e18c2d1

[Halbaroth]

I'm not very fond of this name. We may call it add_sem_atom?

[bclement-ocp]

I don't like it either, but I do not have a better solution. add_sem_atom would be confusing IMO because Shostak.Literal.t can contain either "syntaxic" literals (LTerm) or "semantic" literals (LSem).

Maybe renaming this one to add_atom and the current add_atom to add_expr_atom?

[bclement-ocp]

Should be ready for round 2.

(Note: the changes are fairly involved and so I want to re-run the benches with the exact code that will get merged prior to merging; please don't merge when approving)

[bclement-ocp]

I don't like it either, but I do not have a better solution. add_sem_atom would be confusing IMO because Shostak.Literal.t can contain either "syntaxic" literals (LTerm) or "semantic" literals (LSem).

Maybe renaming this one to add_atom and the current add_atom to add_expr_atom?

[Halbaroth]

Looks good to me, you can merge the PR.

[bclement-ocp]

There is an additional bit of code that I believe is needed in try_to_backjump_further (we could end up taking a semantic decision from the "fake" lazy_cnf that we shouldn't have taken); I will fix this and rerun benchmarks before merging.

[bclement-ocp]

There is an additional bit of code that I believe is needed in try_to_backjump_further (we could end up taking a semantic decision from the "fake" lazy_cnf that we shouldn't have taken); I will fix this and rerun benchmarks before merging.

Pushed the aforementioned change as well as separation of next_decisions into next_decisions (mandatory, keep all) and next_split (optional, keep only one). This is because otherwise in the initial processing phase (before actually solving) we will add the same split over and over again to next_decisions. I have kept next_decisions even though it is no longer used; I'm not too sure about this — it can be useful in the near future but also could be re-introduced at that point.

Re-running benchmarks before merging; although we still need to decide if --enable-sat-cs should be on by default (I'd say yes, but I'm also OK waiting until we can enable it for all theories w/o regressions).

[bclement-ocp]

The current version is +50-8 on AE-format.

[bclement-ocp]

I will go ahead and merge this now with the flag disabled — I think it is acceptable to have it as an experimental flag (and this simplifies the optimization code somewhat) but we should have a comprehensive story for all theories before enabling the flag by default.