cleanup(CDCL): Get rid of repush list

[bclement-ocp]

When cancelling decisions, we collect literals at a higher decision level than the one we are cancelling to (when the --minimal-bj option is enabled) into a list, then replay them at the new decision level (using enqueue_assigned).

This method introduces linear space overhead for the intermediate list that gets created to store the literals to repush, aptly named repush.

This patch uses a more efficient implementation with no additional memory usage by directly moving the literal towards the start of the vector in a single pass, and removes the enqueue_assigned function and repush list.

[Halbaroth]

Actually, I don't know too. I'm still trying to understand the real meaning of this field ;)

[bclement-ocp]

Actually I understood this and forgot: the timp field is set to 1 when the atom is learned using theory propagation (through th_entailed), and we then set it to -1 when we backtrack at a lower level so that we can check whether it is still implied at an earlier level or we need to propagate it back to the theory (see theory_propagate). I will update the comment.

We should probably replace this with a tri-state field :)

[Halbaroth]

Looks correct because this code is already present in enqueue but we don't and we can't call enqueue to push again the literal on the trail in cancel_until, which means the new implementation of cancel_until doesn't raise anymore the Unsat exception. I check this code is never called in a non-regression test. As we don't catch the unsat exception for push or pop statements, I guess this code was never called here. First, I thought this code was never called at all, even in enqueue because the the field is_guard is always false on the negation of a guard and the only place we enqueue explicitly the negation a = g.neg of a guard g (and so a.neg.is_guard = g.is_guard could be true), is in the pop function but both a.is_guard and a.neg.is_guard are set to false just before.

In fact, the negation of guard g.is_guard can be enqueued in the following scenario (and it does with the test testfile-bvnot.dolmen.smt2):
Let's imagine we add in our clause database an implication of the form g => c where c is a clause asserted at the level of assertion of the guard g and image that c is obviously wrong, the clause ~g \/ c is unit and the function add_clause won't produce a new clause at all. Instead, we enqueue immediately the atom ~g.

Another possibility (which doesn't occur in our non-regression tests, but we use few pop/push statements in them) is during the BCP: if we discover that c (same notation as above) is false in the current trail, the clause ~g \/ c becomes unit and we'll propagate the atom ~g but the clause c is a part of our problem (at some assertion level), thus our problem is unsat at this level and we have to stop.

[bclement-ocp]

This code is here to ensure we never propagate the negation of a guard (you give scenarios where this can happen), but in enqueue_assigned it was useless because enqueue_assigned is only called on literals that were already propagated, and thus would have hit the corresponding path in enqueue at the moment they were initially propagated.

[Halbaroth]

It seems this PR breaks an invariant in the assume of Theory.ml:

      assert (not ordered || is_ordered_list t.assumed);

This occurs only with the option --no-tableaux-cdcl-in-theories.
For instance:

dune exec -- alt-ergo --sat-solver CDCL-Tableaux tests/everything/improvement\#1bis.ae --no-tableaux-cdcl-in-theories 

[Halbaroth]

Another difference between this implementation and the previous comes the fact you unassign the atoms in the order of the trail instead of the reverse order. It means you call insert_var_order in reverse order. I'm not sure it's a big issue but I guess the order in which we insert variables in the heap can affect the heuristic algorithm we use to select the next decision.

[bclement-ocp]

It seems this PR breaks an invariant in the assume of Theory.ml:

Good thing we have tests :) Since we repush earlier we can't use Vec.size env.trail to compute the propagation level anymore, thanks for investigating.

Another difference between this implementation and the previous comes the fact you unassign the atoms in the order of the trail instead of the reverse order. It means you call insert_var_order in reverse order. I'm not sure it's a big issue but I guess the order in which we insert variables in the heap can affect the heuristic algorithm we use to select the next decision.

Since this is not the first time we add the variables, most of the time they will probably have different activities, in which case the order we insert them should not matter.

[bclement-ocp]

This code is here to ensure we never propagate the negation of a guard (you give scenarios where this can happen), but in enqueue_assigned it was useless because enqueue_assigned is only called on literals that were already propagated, and thus would have hit the corresponding path in enqueue at the moment they were initially propagated.

[bclement-ocp]

Actually I understood this and forgot: the timp field is set to 1 when the atom is learned using theory propagation (through th_entailed), and we then set it to -1 when we backtrack at a lower level so that we can check whether it is still implied at an earlier level or we need to propagate it back to the theory (see theory_propagate). I will update the comment.

We should probably replace this with a tri-state field :)

[bclement-ocp]

Marking as draft until we look at bench results

[bclement-ocp]

Since this is not the first time we add the variables, most of the time they will probably have different activities, in which case the order we insert them should not matter.

Turns out that this intuition was only partially correct — this order kind of matters for variables which never took part in a conflict, of which there are many for the first few conflicts, and this impacts the search afterwards!

This causes regressions on internal data sets, let's scratch it for now.