cleanup(CP): Simplify constraint handling

[bclement-ocp]

This patch rewrites the Constraints_make module in order to make it more flexible (this is preparatory step for dealing with arithmetic bit-vector constraints, see #903).

More precisely:

• Constraints no longer need to keep track of their own explanations, this is now entirely done by the Constraints_make functor. This makes it simpler to write Constraint modules, and avoid repeating boilerplate code to deal with explanation storage. Instead, the explanations are provided to the Constraint module in its propagate function.

• The Constraints_make functor no longer need to know about constraint propagation. Instead, it simply keeps track of constraints that need to be propagated (pending constraints), and provides an API to iterate (and remove) the set of constraints to be propagated, letting the user take care of propagation proper.

• The Constraints_make functor now tracks separately the constraint arguments and the leaves of said arguments. The leaves are used to know which constraints need to be updated during a substitution, and the arguments are used to mark as pending all constraints that apply to a given representative when its domain is updated (note that, for the bit-list domains, we actually store the domains at the leaves, so the arguments mapping is not used -- but this still makes the module more flexible in general, and in particular will allow to introduce arithmetic domains that need to be stored for all values, not only leaves, for the purpose of Improving reasoning for the BV theory #903 in a future PR)

The new design should make it easier to write Constraint modules. It also fixes a bug in the contract between the Constraint and Domain modules regarding substitution: the Domain modules was written under the assumption that constraints applying to changed domains would always be marked as pending upon substitution, but that is not true because we use functional representations where such updates are delayed, and hence the changed flag needs to be propagated after substitution (if appropriate).

[bclement-ocp]

I have pushed a small modification to a comment stating a restriction on constraint substitutions that was true in an early implementation of this PR, but is no longer a restriction.

For more details, the restriction was about preventing constraint substitution from preventing simplifications, which was intended to avoid having to mark the new constraint as pending after substitution as an optimization. However, it turned out to be too tricky to do this properly, and so I have removed the optimization — and hence the restriction — but forgot to update that comment.

[bclement-ocp]

it turned out to be too tricky to do this properly

Actually just realized that this is because in the current version the bvxor constraint does perform simplifications and it was never going to work (unlike the context where the PR was originally written, with a version of bvxor that does not perform simplifications) (:

[Halbaroth]

I believe the flag pending is useless here. Indeed, the constraint c is removed in remove c t (as the comparison function of the module CS ignores the explanation, even if the underlying explanation of c changed during this function iteration, we remove the only copy of c in the map), thus the function CS.find will always raise Not_found in the function add.

[bclement-ocp]

The result of Constraint.subst rr nrr c.value is not identical to c. It is possible that the resulting constraint was already there for another reason (e.g. suppose we have C1(x, y) that was pending and C1(x, x) that was already present but not pending, then we apply the substitution y → x and C1(x, y) becomes C1(x, x) but we want to preserve the fact that it was pending and needs to be propagated.

Although if this is the case and C1(x, x) was not pending then presumably it has already been propagated? This is probably a relic that was necessary for the optimization I mentioned in another comment but is no longer required without that optimization; I think we can indeed remove the flag here.

[Halbaroth]

I don't know if it was like this before but the fact we ignore explanations here means we cannot store several times the same constraint with not comparable explanations (by not comparable explanations, I mean there is no one of them which is subsumed by the other one).

We should document this point.

[bclement-ocp]

This was already the case before, it was explained in the documentation of Constraint.compare. This is now enforced by Constraints_make rather than Constraint, so I removed it from the documentation of Constraint.compare; I will mention it in the documentation of Constraints_make.

[Halbaroth]

We can remove the flag pending as we don't use it anymore.

[Halbaroth]

Can you explain why is it correct to look up in t.leaves_map instead of t.args_map?
I guess it's because we perform substitution on leaves?

[bclement-ocp]

By definition, substitutions apply on leaves (terms and AC applications). It would be incorrect to look in t.args_map: for instance, if C is the constraint r = x & (y ++ z) (where ++ is BV concatenation) then the args_map is r → C; x → C; (y ++ z) → C but substitutions can only apply to r, x, y and z.

[bclement-ocp]

I will clarify this because it's not strictly correct: Alt-Ergo does propagate Subst rewritings for superterms; for instance, if we substitute z → z' then the UF module will generate the substitution y ++ z → y ++ z'. However, the Shostak modules only supports substituting leaves, and we ultimately call X.subst here.

Now that I think about it more, I believe this was an error in the design of the original Constraint module — it should not call X.subst but rather simply perform a comparison on the result of congruence closure (i.e. the thing that gets substituted). This is probably also true of the Domains module.

[bclement-ocp]

After some more investigation: using comparison instead of X.subst here doesn't work for a reason related to #474: when class representatives change from rr to nrr, we only get the substitution rr → nrr if rr was a semantic value for a term of the initial problem (iow, if it is in repr). So for instance if we have substitutions x → 0 @ .k0 (where .k0 is a fresh constant) then .k0 → 0 @ .k1, the relations will only see x → 00 @ .k1 and .k0 → 0 @ .k1 — but not 0 @ .k0 → 00 @ .k1.

[Halbaroth]

My connection is terrible, I will try again to comment...
So, as you changed the design of these modules in recent PR, I believe we can merge this one now?

[bclement-ocp]

So, as you changed the design of these modules in recent PR, I believe we can merge this one now?

The PR is still marked as "Changes requested" so I was waiting for your 2nd round of review & the green checkmark :) I will merge taking this message as approval.