feat(pumpkin-core): Introduce runtime consistency verification of propagators#374
feat(pumpkin-core): Introduce runtime consistency verification of propagators#374maartenflippo wants to merge 16 commits intomainfrom
Conversation
|
|
||
| fn assign(&self, value: i32) -> SingleVariableAssignment { | ||
| assert_eq!((value - self.offset) % self.scale, 0); | ||
| let inner_assignment = (value - self.offset) / self.scale; |
There was a problem hiding this comment.
Why not use the invert method here?
There was a problem hiding this comment.
I want to explicitly maintain that no rounding happens.
| #[cfg(feature = "check-propagations")] | ||
| { | ||
| use crate::propagation::checkers::ConsistencyChecker; | ||
|
|
||
| #[allow(trivial_casts, reason = "removing it causes a compiler error")] | ||
| let previous_checker = self.consistency_checkers.insert( | ||
| handle.propagator_id(), | ||
| BoxedConsistencyChecker::from( | ||
| Box::new(consistency_checker) as Box<dyn ConsistencyChecker> | ||
| ), | ||
| ); | ||
| assert!( | ||
| previous_checker.is_none(), | ||
| "somehow adding multiple consistency checkers to the same propagator" | ||
| ); | ||
| } |
There was a problem hiding this comment.
Why not add this directly in constructor.add_inference? It seems like this is doing the same thing as for the InferenceChecker
There was a problem hiding this comment.
I think this does not work due to our strong/weak consistency difference. We should discuss on Zoom at some point
There was a problem hiding this comment.
In my mind, it would be good to explicitly differentiate between InferenceChecker and ConsistencyChecker; naming the module checkers makes this ambiguous
| Domain, | ||
| } | ||
|
|
||
| fn assert_consistency<PropagationChecker>( |
There was a problem hiding this comment.
As per usual, documentation please
| } | ||
| } | ||
|
|
||
| fn support_value<PropagationChecker>( |
| #[derive(Clone, Debug, Default)] | ||
| pub struct ScopeBuilder(Vec<(LocalId, DomainId)>); | ||
|
|
||
| impl ScopeBuilder { | ||
| pub fn add(&mut self, local_id: LocalId, domain_id: DomainId) { | ||
| self.0.push((local_id, domain_id)); | ||
| } | ||
|
|
||
| pub fn build(self) -> Scope { | ||
| Scope(self.0) | ||
| } | ||
| } |
There was a problem hiding this comment.
What is the purpose of the ScopeBuilder? This seems to be a pass-along struct at the moment?
There was a problem hiding this comment.
Indeed. Removed
| let last_idx = hypercube_predicates.len() - 1; | ||
| [ | ||
| context.register_predicate(hypercube_predicates[0.min(last_idx)]), | ||
| context.register_predicate(hypercube_predicates[0]), |
There was a problem hiding this comment.
This is a new nightly clippy warning, so its fixed to get the code style action to pass
Witness generators now immediately provide all witnesses
maartenflippo
force-pushed
the
feat/propagation-checkers
branch
from
04d580a to
9a528c3
Compare
2 participants
To increase the trust in propagator implementations, we complement the existing inference checkers with consistency checkers. A consistency checker verifies that a propagator is at its intended consistency level.
The function
PropagatorConstructor::add_inference_checkersnow returns aConsistencyCheckerimplementation. This means there is one ConsistencyChecker per propagator. The interface forces propagator implementations to return a consistency checker if they want to run any checkers at all.Since the
add_inference_checkershad a default implementation, that now returns a consistency checker that always indicates the desired consistency level is achieved. For any new propagators, we do not want to expose that, so the implementation is marked deprecated and is hidden from the documentation. However, it reduces the size of this already significant PR as we don't have to implement consistency checkers for every propagator as well.In this PR, we also implement reusable checkers for:
TODO
Witness generators for bound consistent propagators
Witness generators for domain consistent propagators
Migrate
propagate_from_scratchto custom consistency checkers where bounds or domain consistency is not applicableWitness generators for non-bound consistent propagators
Division (Not bound-consistent since it only propagates when the denominator spans 0)
Multiplication (Only propagates in certain situations)