Skip to content
Open
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 2 additions & 2 deletions pumpkin-crates/checking/src/inference_checker.rs
Original file line number Diff line number Diff line change
Expand Up @@ -30,8 +30,8 @@ impl<Atomic: AtomicConstraint> Clone for BoxedChecker<Atomic> {
}
}

impl<Atomic: AtomicConstraint> From<Box<dyn InferenceChecker<Atomic>>> for BoxedChecker<Atomic> {
fn from(value: Box<dyn InferenceChecker<Atomic>>) -> Self {
impl<Atomic: AtomicConstraint> BoxedChecker<Atomic> {
pub fn new(value: Box<dyn InferenceChecker<Atomic>>) -> Self {
BoxedChecker(value)
}
}
Expand Down
2 changes: 0 additions & 2 deletions pumpkin-crates/core/src/basic_types/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,6 @@ mod function;
mod predicate_id_generators;
mod propositional_conjunction;
mod random;
mod ref_or_owned;
pub(crate) mod sequence_generators;
mod solution;
mod stored_conflict_info;
Expand All @@ -19,7 +18,6 @@ pub use predicate_id_generators::PredicateId;
pub use predicate_id_generators::PredicateIdGenerator;
pub use propositional_conjunction::PropositionalConjunction;
pub use random::*;
pub(crate) use ref_or_owned::*;
pub use solution::ProblemSolution;
pub use solution::Solution;
pub use solution::SolutionReference;
Expand Down
49 changes: 0 additions & 49 deletions pumpkin-crates/core/src/basic_types/ref_or_owned.rs

This file was deleted.

3 changes: 3 additions & 0 deletions pumpkin-crates/core/src/checkers/mod.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
mod store;

pub use store::*;
40 changes: 40 additions & 0 deletions pumpkin-crates/core/src/checkers/store.rs
Comment thread
ImkoMarijnissen marked this conversation as resolved.
Original file line number Diff line number Diff line change
@@ -0,0 +1,40 @@
//! This module facilitates runtime verification in Pumpkin. It defines common types as well as the
//! [`CheckerStore`] that owns the checkers that are active in the solver.

use pumpkin_checking::BoxedChecker;
#[cfg(doc)]
use pumpkin_checking::InferenceChecker;

use crate::containers::HashMap;
use crate::predicates::Predicate;
use crate::proof::InferenceCode;

/// Owns the runtime checkers present in the solver.
#[derive(Clone, Debug, Default)]
pub struct CheckerStore {
inference_codes: HashMap<InferenceCode, Vec<BoxedChecker<Predicate>>>,
}

impl CheckerStore {
/// Get the [`InferenceChecker`]s for the given inference code.
pub fn for_inference_code(
&self,
inference_code: &InferenceCode,
) -> impl ExactSizeIterator<Item = &BoxedChecker<Predicate>> {
self.inference_codes
.get(inference_code)
.map(|checkers| itertools::Either::Left(checkers.iter()))
.unwrap_or(itertools::Either::Right(std::iter::empty()))
}

pub fn add_inference_checker(
&mut self,
inference_code: InferenceCode,
checker: BoxedChecker<Predicate>,
) {
self.inference_codes
.entry(inference_code.clone())
.or_default()
.push(checker);
}
}
Original file line number Diff line number Diff line change
Expand Up @@ -279,13 +279,13 @@ impl ConflictAnalysisContext<'_> {
let learned_nogood = LearnedNogood::create_from_vec(learned_nogood_predicates, self);

let constraint_tag = self.log_deduction(learned_nogood.predicates.iter().copied());
let inference_code = InferenceCode::new(constraint_tag, NogoodLabel);

self.state.add_inference_checker(
inference_code.clone(),
Box::new(NogoodChecker {
let inference_code = self.state.add_inference_checker(
constraint_tag,
NogoodLabel,
NogoodChecker {
nogood: learned_nogood.predicates.clone().into(),
}),
},
);

self.restore_to(learned_nogood.backtrack_level);
Expand Down
16 changes: 8 additions & 8 deletions pumpkin-crates/core/src/engine/constraint_satisfaction_solver.rs
Original file line number Diff line number Diff line change
Expand Up @@ -891,16 +891,17 @@ impl ConstraintSatisfactionSolver {
fn add_nogood(
&mut self,
nogood: Vec<Predicate>,
inference_code: InferenceCode,
constraint_tag: ConstraintTag,
) -> Result<(), ConstraintOperationError> {
pumpkin_assert_eq_simple!(self.get_checkpoint(), 0);
let num_trail_entries = self.state.trail_len();

self.state.add_inference_checker(
inference_code.clone(),
Box::new(NogoodChecker {
let inference_code = self.state.add_inference_checker(
constraint_tag,
NogoodLabel,
NogoodChecker {
nogood: nogood.clone().into(),
}),
},
);

let (nogood_propagator, mut context) = self
Expand Down Expand Up @@ -983,7 +984,6 @@ impl ConstraintSatisfactionSolver {
return Err(ConstraintOperationError::InfeasibleClause);
}

let inference_code = InferenceCode::new(constraint_tag, NogoodLabel);
if are_all_falsified_at_root {
// Since the propagation is not actually performed, we log the inference
// explicitly here for the proof.
Expand All @@ -992,7 +992,7 @@ impl ConstraintSatisfactionSolver {
.proof_log
.log_inference(
&mut self.state.constraint_tags,
inference_code,
InferenceCode::new(constraint_tag, NogoodLabel),
predicates.iter().copied(),
None,
&self.state.variable_names,
Expand All @@ -1013,7 +1013,7 @@ impl ConstraintSatisfactionSolver {
return Err(ConstraintOperationError::InfeasibleClause);
}

if let Err(constraint_operation_error) = self.add_nogood(predicates, inference_code) {
if let Err(constraint_operation_error) = self.add_nogood(predicates, constraint_tag) {
let _ = self.conclude_proof_unsat();

self.solver_state
Expand Down
9 changes: 7 additions & 2 deletions pumpkin-crates/core/src/engine/cp/test_solver.rs
Original file line number Diff line number Diff line change
Expand Up @@ -17,6 +17,7 @@ use crate::predicate;
use crate::predicates::PropositionalConjunction;
use crate::proof::ConstraintTag;
use crate::proof::InferenceCode;
use crate::proof::InferenceLabel;
use crate::propagation::EnqueueDecision;
use crate::propagation::ExplanationContext;
use crate::propagation::NotificationContext;
Expand Down Expand Up @@ -57,7 +58,11 @@ impl Default for TestSolver {

#[deprecated = "Will be replaced by the state API"]
impl TestSolver {
pub fn accept_inferences_by(&mut self, inference_code: InferenceCode) {
pub fn accept_inferences_by(
&mut self,
constraint_tag: ConstraintTag,
inference_label: impl InferenceLabel,
) -> InferenceCode {
#[derive(Debug, Clone, Copy)]
struct Checker;

Expand All @@ -73,7 +78,7 @@ impl TestSolver {
}

self.state
.add_inference_checker(inference_code, Box::new(Checker));
.add_inference_checker(constraint_tag, inference_label, Checker)
}

pub fn new_variable(&mut self, lb: i32, ub: i32) -> DomainId {
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -102,11 +102,6 @@ impl<'a> Watchers<'a> {
}
}

pub(crate) fn watch_all(&mut self, domain: DomainId, events: EnumSet<DomainEvent>) {
self.notification_engine
.watch_all(domain, events, self.propagator_var);
}

pub(crate) fn unwatch_all(&mut self, domain: DomainId) {
self.notification_engine
.unwatch_all(domain, self.propagator_var);
Expand Down
92 changes: 52 additions & 40 deletions pumpkin-crates/core/src/engine/state.rs
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,7 @@ use pumpkin_checking::InferenceChecker;
#[cfg(feature = "check-propagations")]
use pumpkin_checking::VariableState;

use crate::containers::HashMap;
use crate::checkers::CheckerStore;
use crate::containers::KeyGenerator;
use crate::create_statistics_struct;
use crate::engine::Assignments;
Expand All @@ -25,17 +25,18 @@ use crate::predicates::PredicateType;
use crate::predicates::PropositionalConjunction;
use crate::proof::ConstraintTag;
use crate::proof::InferenceCode;
use crate::proof::InferenceLabel;
use crate::propagation::ConstructedPropagator;
use crate::propagation::CurrentNogood;
use crate::propagation::Domains;
use crate::propagation::ExplanationContext;
#[cfg(feature = "check-propagations")]
use crate::propagation::InferenceCheckers;
use crate::propagation::NotificationContext;
use crate::propagation::PropagationContext;
use crate::propagation::Propagator;
use crate::propagation::PropagatorConstructor;
use crate::propagation::PropagatorConstructorContext;
use crate::propagation::PropagatorId;
use crate::propagation::PropagatorVarId;
use crate::propagation::store::PropagatorStore;
use crate::pumpkin_assert_advanced;
use crate::pumpkin_assert_eq_simple;
Expand Down Expand Up @@ -80,8 +81,8 @@ pub struct State {

statistics: StateStatistics,

/// Inference checkers to run in the propagation loop.
checkers: HashMap<InferenceCode, Vec<BoxedChecker<Predicate>>>,
/// Runtime checkers to run in the propagation loop.
checkers: CheckerStore,
}

create_statistics_struct!(StateStatistics {
Expand Down Expand Up @@ -111,7 +112,7 @@ impl Default for State {
notification_engine: NotificationEngine::default(),
statistics: StateStatistics::default(),
constraint_tags: KeyGenerator::default(),
checkers: HashMap::default(),
checkers: CheckerStore::default(),
};
// As a convention, the assignments contain a dummy domain_id=0, which represents a 0-1
// variable that is assigned to one. We use it to represent predicates that are
Expand Down Expand Up @@ -333,15 +334,31 @@ impl State {
Constructor: PropagatorConstructor,
Constructor::PropagatorImpl: 'static,
{
#[cfg(feature = "check-propagations")]
constructor.add_inference_checkers(InferenceCheckers::new(self));

let original_handle: PropagatorHandle<Constructor::PropagatorImpl> =
self.propagators.new_propagator().key();

let constructor_context =
PropagatorConstructorContext::new(original_handle.propagator_id(), self);
let propagator = constructor.create(constructor_context);

let ConstructedPropagator {
registration,
checkers,
propagator,
} = constructor.create(constructor_context);

for (domain_id, events, local_id) in registration.iter() {
let propagator_var = PropagatorVarId {
propagator: original_handle.propagator_id(),
variable: local_id,
};

self.notification_engine
.watch_all(domain_id, events, propagator_var);
Comment thread
ImkoMarijnissen marked this conversation as resolved.
}

for (inference_code, checker) in checkers.into_iter() {
self.checkers.add_inference_checker(inference_code, checker);
}

pumpkin_assert_simple!(
propagator.priority() as u8 <= 3,
Expand Down Expand Up @@ -370,11 +387,14 @@ impl State {
/// any checker accepts the inference, the inference is accepted.
pub fn add_inference_checker(
&mut self,
inference_code: InferenceCode,
checker: Box<dyn InferenceChecker<Predicate>>,
) {
let checkers = self.checkers.entry(inference_code).or_default();
checkers.push(BoxedChecker::from(checker));
constraint_tag: ConstraintTag,
inference_label: impl InferenceLabel,
Comment thread
ImkoMarijnissen marked this conversation as resolved.
checker: impl InferenceChecker<Predicate> + 'static,
) -> InferenceCode {
let inference_code = InferenceCode::new(constraint_tag, inference_label);
self.checkers
.add_inference_checker(inference_code.clone(), BoxedChecker::new(Box::new(checker)));
inference_code
}
}

Expand Down Expand Up @@ -770,31 +790,23 @@ impl State {
) {
let premises: Vec<_> = premises.into_iter().collect();

let checkers = self
.checkers
.get(inference_code)
.map(|vec| vec.as_slice())
.unwrap_or(&[]);

assert!(
!checkers.is_empty(),
"missing checker for inference code {inference_code:?}"
);

let any_checker_accepts_inference = checkers.iter().any(|checker| {
// Construct the variable state for the conflict check.
let variable_state = VariableState::prepare_for_conflict_check(
premises.clone(),
consequent,
)
.unwrap_or_else(|domain| {
panic!(
"inconsistent atomics over domain {domain:?} in inference by {inference_code:?}"
)
});

checker.check(variable_state, &premises, consequent.as_ref())
});
let any_checker_accepts_inference =
self.checkers
.for_inference_code(inference_code)
.any(|checker| {
// Construct the variable state for the conflict check.
let variable_state = VariableState::prepare_for_conflict_check(
premises.clone(),
consequent,
)
.unwrap_or_else(|domain| {
panic!(
"inconsistent atomics over domain {domain:?} in inference by {inference_code:?}"
)
});

checker.check(variable_state, &premises, consequent.as_ref())
});

assert!(
any_checker_accepts_inference,
Expand Down
Loading
Loading