refactor(pumpkin-solver): Force checkers to be registered in propagator constructor

[maartenflippo]

Updates the interface of PropagatorConstructor::create to explicitly require a bag of checkers to be provided. This makes it harder to forget and requires explicit opt-out of registering checkers.

Based on discussions for #449.

Changes

• Introduce ConstructedPropagator as the return type of PropagatorConstructor::create
• Remove PropagatorConstructorContext::add_inference_checker
• Remove PropagatorConstructor::add_inference_checkers

TODO

• Depends on refactor(pumpkin-solver): PropagatorConstructor::create now returns event registrations #456

[EmirDe]

An incomplete review from my side to keep things from being blocked (I am guessing that perhaps not too detailed reviews are ok for now, and once everything is in place, we do a detailed review?):

Overall looks like nice design.

ConstructedPropagator -> I like the idea of having a struct as a return type. I am not sure about the name, since it holds the propagator plus additional info. Some potential alternative names: PropagatorDefinition/Spec/Description? In some sense, it is a specification of the propagator.

About the name "RuntimeCheckers". I like this name. But we previously used "ConsistencyCheckers", which is more descriptive in what it does, but RuntimeChecker is more descriptive of when it does checking. What is better, should we also use this name in our paper? I am slightly in favour of RuntimeCheckers, but not sure.

Is there a world in which we want to have empty runtime checkers? We have support for it in the code with the builder, just to check!

pub trait StoresCheckers -> why is this a trait? I am not too opposed to this so that we keep things going but just wondering.

any_checker_accepts_inference -> conceptually, it feels a bit awkward; it feels like we should handle these cases more elegantly, e.g., some notion of "decomposition checker" and appropriate logic around it. We could ignore this for now and still go with it. If you also think it is a bit awkward, then we could make an issue.

[ImkoMarijnissen]

Looks good overall, I left some small comments for now!

[maartenflippo]

ConstructedPropagator -> I like the idea of having a struct as a return type. I am not sure about the name, since it holds the propagator plus additional info. Some potential alternative names: PropagatorDefinition/Spec/Description? In some sense, it is a specification of the propagator.

I like PropagatorSpec as well. Will make the change.

About the name "RuntimeCheckers". I like this name. But we previously used "ConsistencyCheckers", which is more descriptive in what it does, but RuntimeChecker is more descriptive of when it does checking. What is better, should we also use this name in our paper? I am slightly in favour of RuntimeCheckers, but not sure.

For me the term RuntimeCheckers is more natural. I am struggling to remember that ConsistencyChecker = Inference + Propagation checkers, which signals the name may not be the most convenient? Note this PR does not yet add retention checkers.

Is there a world in which we want to have empty runtime checkers? We have support for it in the code with the builder, just to check!

Yes! The nogood propagator only posts checkers when nogoods are added. So at construction the checkers are empty.

pub trait StoresCheckers -> why is this a trait? I am not too opposed to this so that we keep things going but just wondering.

To decouple this module from the rest of the solver details. Allows for easier testing in isolation.

any_checker_accepts_inference -> conceptually, it feels a bit awkward; it feels like we should handle these cases more elegantly, e.g., some notion of "decomposition checker" and appropriate logic around it. We could ignore this for now and still go with it. If you also think it is a bit awkward, then we could make an issue.

Actually, I think this a natural consequence of the fact that our checkers are sound but not complete. If any checker accepts an inference it is (should be) sound.

Review re-requested

[EmirDe]

For me the term RuntimeCheckers is more natural. I am struggling to remember that ConsistencyChecker = Inference + Propagation checkers, which signals the name may not be the most convenient? Note this PR does not yet add retention checkers.

It would be useful if you could elaborate on this, so that we can also make the change in the paper, in particular the part of what is so confusing about the consistency checking term. In my mind, 'checking consistency' means we want to be sure the propagator is at its advertised level of consistency. To do that, we need to check every removal from the domain (propagator checker, which is composed on inference checking plus checking the applicability of the explanation given the trail) and we need to check for every value we kept in the domain (retention checkers). Then Consistency Checkers for both of these makes sense. But maybe runtime checking sounds nice because it shows when these checkers are used, and it is perhaps clearer that these are not 'conventional' checkers used in proof systems.

Yes! The nogood propagator only posts checkers when nogoods are added. So at construction the checkers are empty.

Ah yes, so probably also in the hypercube propagator, or any compound propagator that is not a constraint on its own but a collection of constraints.

pub trait StoresCheckers -> why is this a trait? I am not too opposed to this so that we keep things going but just wondering.

To decouple this module from the rest of the solver details. Allows for easier testing in isolation.

Great, like in the other PR, small traits -> good!

any_checker_accepts_inference -> conceptually, it feels a bit awkward; it feels like we should handle these cases more elegantly, e.g., some notion of "decomposition checker" and appropriate logic around it. We could ignore this for now and still go with it. If you also think it is a bit awkward, then we could make an issue.

Actually, I think this a natural consequence of the fact that our checkers are sound but not complete. If any checker accepts an inference it is (should be) sound.

Technically, our checkers are not complete. However, the way we use checkers is quite deliberate. For all other uses of checkers, if a checker fails, we know we have a problem and we know exactly where the problem is, e.g., a propagation cannot be justified even though we expect that it should, despite the checkers not being complete. In fact, we might not even want complete checkers, since we want to know that our components are working exactly as they should, and not be right for reasons we did not foresee!

When it comes to 'any_checker_accepts_inference', it is very different from the above cases, since we do not know what to check; we use all these checkers and expect one of them to trigger. It would be more natural if we could pinpoint exactly which one, which would make more sense given how we do things.

We do not need to make changes to this now because it is not critical for this PR, but I do feel that it sticks out a bit!

[EmirDe]

I like PropagatorSpec as well. Will make the change.
Assuming we make this change, looks ok to merge. See also comments.