feat(pumpkin-core): Introduce runtime consistency verification of propagators#374
feat(pumpkin-core): Introduce runtime consistency verification of propagators#374maartenflippo wants to merge 10 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?
| #[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.
In my mind, it would be good to explicitly differentiate between InferenceChecker and ConsistencyChecker; naming the module checkers makes this ambiguous
| ) where | ||
| PropagationChecker: WitnessGenerator + InferenceChecker<Predicate>, | ||
| { | ||
| let mut supported_values: HashMap<DomainId, Vec<i32>> = HashMap::default(); |
There was a problem hiding this comment.
Maybe a hasty optimisation, but I can imagine that this structure might become large for certain propagators; perhaps good to reuse the existing allocation?
Up to you whether you feel like this is necessary at this point, please feel free to resolve this comment
| 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?
| let last_idx = hypercube_predicates.len() - 1; | ||
| [ | ||
| context.register_predicate(hypercube_predicates[0.min(last_idx)]), | ||
| context.register_predicate(hypercube_predicates[0]), |
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)