Skip to content

Commit 67c2241

Browse files
maartenflippomaartenflippo
authored
feature: lazy explanation context (#123)
When using lazy explanations, the propagator receives the internal `Assignments` structure. However, we want them to access more than just the assignments. So we introduce a dedicated context to expose a wider API. Since it is likely undesirable that propagators can access the `Assignments` directly, the accessor is marked deprecated. The only spot where we use this is now explicitly allowed but may need to be refactored.
1 parent 247fcd9 commit 67c2241

23 files changed

+276
-97
lines changed

‎pumpkin-solver/src/basic_types/propagation_status_cp.rs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -8,7 +8,7 @@ use crate::predicates::Predicate;
88
pub(crate) type PropagationStatusCP = Result<(), Inconsistency>;
99

1010
#[derive(Debug, PartialEq, Eq)]
11-
pub enum Inconsistency {
11+
pub(crate) enum Inconsistency {
1212
EmptyDomain,
1313
Conflict(PropositionalConjunction),
1414
}

‎pumpkin-solver/src/containers/key_value_heap.rs

Lines changed: 21 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -18,7 +18,7 @@ use crate::pumpkin_assert_moderate;
1818
/// which allows for generalised `Key`s (required to implement [StorageKey]) and `Value`s (which are
1919
/// required to be ordered, divisible and addable).
2020
#[derive(Debug, Clone)]
21-
pub struct KeyValueHeap<Key: StorageKey, Value> {
21+
pub struct KeyValueHeap<Key, Value> {
2222
/// Contains the values stored as a heap; the value of key `i` is at index
2323
/// [`KeyValueHeap::map_key_to_position\[i\]`][KeyValueHeap::map_key_to_position]
2424
values: Vec<Value>,
@@ -43,11 +43,31 @@ impl<Key: StorageKey, Value> Default for KeyValueHeap<Key, Value> {
4343
}
4444
}
4545

46+
impl<Key, Value> KeyValueHeap<Key, Value> {
47+
pub(crate) const fn new() -> Self {
48+
Self {
49+
values: Vec::new(),
50+
map_key_to_position: KeyedVec::new(),
51+
map_position_to_key: Vec::new(),
52+
end_position: 0,
53+
}
54+
}
55+
}
56+
4657
impl<Key, Value> KeyValueHeap<Key, Value>
4758
where
4859
Key: StorageKey + Copy,
4960
Value: AddAssign<Value> + DivAssign<Value> + PartialOrd + Default + Copy,
5061
{
62+
/// Get the keys in the heap.
63+
///
64+
/// The order in which the keys are yielded is unspecified.
65+
pub(crate) fn keys(&self) -> impl Iterator<Item = Key> + '_ {
66+
self.map_position_to_key[..self.end_position]
67+
.iter()
68+
.copied()
69+
}
70+
5171
/// Return the key with maximum value from the heap, or None if the heap is empty. Note that
5272
/// this does not delete the key (see [`KeyValueHeap::pop_max`] to get and delete).
5373
///

‎pumpkin-solver/src/containers/keyed_vec.rs

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -32,6 +32,15 @@ impl<Key, Value> Default for KeyedVec<Key, Value> {
3232
}
3333
}
3434

35+
impl<Key, Value> KeyedVec<Key, Value> {
36+
pub(crate) const fn new() -> Self {
37+
Self {
38+
key: PhantomData,
39+
elements: Vec::new(),
40+
}
41+
}
42+
}
43+
3544
impl<Key: StorageKey, Value> KeyedVec<Key, Value> {
3645
pub(crate) fn len(&self) -> usize {
3746
self.elements.len()

‎pumpkin-solver/src/engine/conflict_analysis/conflict_analysis_context.rs

Lines changed: 7 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -9,6 +9,8 @@ use crate::branching::Brancher;
99
use crate::engine::constraint_satisfaction_solver::CSPSolverState;
1010
use crate::engine::predicates::predicate::Predicate;
1111
use crate::engine::propagation::store::PropagatorStore;
12+
use crate::engine::propagation::CurrentNogood;
13+
use crate::engine::propagation::ExplanationContext;
1214
use crate::engine::reason::ReasonRef;
1315
use crate::engine::reason::ReasonStore;
1416
use crate::engine::solver_statistics::SolverStatistics;
@@ -130,6 +132,7 @@ impl<'a> ConflictAnalysisContext<'a> {
130132
pub(crate) fn get_propagation_reason(
131133
predicate: Predicate,
132134
assignments: &Assignments,
135+
current_nogood: CurrentNogood<'_>,
133136
reason_store: &'a mut ReasonStore,
134137
propagators: &'a mut PropagatorStore,
135138
proof_log: &'a mut ProofLog,
@@ -170,8 +173,11 @@ impl<'a> ConflictAnalysisContext<'a> {
170173

171174
let propagator_id = reason_store.get_propagator(reason_ref);
172175
let constraint_tag = propagators.get_tag(propagator_id);
176+
177+
let explanation_context = ExplanationContext::new(assignments, current_nogood);
178+
173179
let reason = reason_store
174-
.get_or_compute(reason_ref, assignments, propagators)
180+
.get_or_compute(reason_ref, explanation_context, propagators)
175181
.expect("reason reference should not be stale");
176182
if propagator_id == ConstraintSatisfactionSolver::get_nogood_propagator_id()
177183
&& reason.is_empty()

‎pumpkin-solver/src/engine/conflict_analysis/minimisers/recursive_minimiser.rs

Lines changed: 15 additions & 18 deletions
Original file line numberDiff line numberDiff line change
@@ -2,6 +2,7 @@ use crate::basic_types::moving_averages::MovingAverage;
22
use crate::basic_types::HashMap;
33
use crate::basic_types::HashSet;
44
use crate::engine::conflict_analysis::ConflictAnalysisContext;
5+
use crate::engine::propagation::CurrentNogood;
56
use crate::engine::Assignments;
67
use crate::predicates::Predicate;
78
use crate::pumpkin_assert_moderate;
@@ -45,7 +46,7 @@ impl RecursiveMinimiser {
4546
for i in 0..initial_nogood_size {
4647
let learned_predicate = nogood[i];
4748

48-
self.compute_label(learned_predicate, context);
49+
self.compute_label(learned_predicate, context, nogood);
4950

5051
let label = self.get_predicate_label(learned_predicate);
5152
// Keep the predicate in case it was not deemed deemed redundant.
@@ -69,7 +70,12 @@ impl RecursiveMinimiser {
6970
.add_term(num_predicates_removed as u64);
7071
}
7172

72-
fn compute_label(&mut self, input_predicate: Predicate, context: &mut ConflictAnalysisContext) {
73+
fn compute_label(
74+
&mut self,
75+
input_predicate: Predicate,
76+
context: &mut ConflictAnalysisContext,
77+
current_nogood: &[Predicate],
78+
) {
7379
pumpkin_assert_moderate!(context.assignments.is_predicate_satisfied(input_predicate));
7480

7581
self.current_depth += 1;
@@ -109,29 +115,20 @@ impl RecursiveMinimiser {
109115
return;
110116
}
111117

112-
// Due to ownership rules, we retrieve the reason each time we need it, and then drop it.
113-
// Here we retrieve the reason and just record the length, dropping the ownership of the
114-
// reason.
115-
let reason_size = ConflictAnalysisContext::get_propagation_reason(
118+
// Due to ownership rules, we have to take ownership of the reason.
119+
// TODO: Reuse the allocation if it becomes a bottleneck.
120+
let reason = ConflictAnalysisContext::get_propagation_reason(
116121
input_predicate,
117122
context.assignments,
123+
CurrentNogood::from(current_nogood),
118124
context.reason_store,
119125
context.propagators,
120126
context.proof_log,
121127
context.unit_nogood_step_ids,
122128
)
123-
.len();
124-
125-
for i in 0..reason_size {
126-
let antecedent_predicate = ConflictAnalysisContext::get_propagation_reason(
127-
input_predicate,
128-
context.assignments,
129-
context.reason_store,
130-
context.propagators,
131-
context.proof_log,
132-
context.unit_nogood_step_ids,
133-
)[i];
129+
.to_vec();
134130

131+
for antecedent_predicate in reason {
135132
// Root assignments can be safely ignored.
136133
if context
137134
.assignments
@@ -143,7 +140,7 @@ impl RecursiveMinimiser {
143140
}
144141

145142
// Compute the label of the antecedent predicate.
146-
self.compute_label(antecedent_predicate, context);
143+
self.compute_label(antecedent_predicate, context, current_nogood);
147144

148145
// In case one of the antecedents is Poison,
149146
// the input predicate is not deemed redundant.

‎pumpkin-solver/src/engine/conflict_analysis/minimisers/semantic_minimiser.rs

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -9,7 +9,7 @@ use crate::predicates::Predicate;
99
use crate::variables::DomainId;
1010

1111
#[derive(Clone, Debug)]
12-
pub struct SemanticMinimiser {
12+
pub(crate) struct SemanticMinimiser {
1313
original_domains: KeyedVec<DomainId, SimpleIntegerDomain>,
1414
domains: KeyedVec<DomainId, SimpleIntegerDomain>,
1515
present_ids: SparseSet<DomainId>,
@@ -29,13 +29,13 @@ impl Default for SemanticMinimiser {
2929
}
3030

3131
#[derive(Clone, Copy, Debug)]
32-
pub enum Mode {
32+
pub(crate) enum Mode {
3333
EnableEqualityMerging,
3434
DisableEqualityMerging,
3535
}
3636

3737
impl SemanticMinimiser {
38-
pub fn minimise(
38+
pub(crate) fn minimise(
3939
&mut self,
4040
nogood: &Vec<Predicate>,
4141
assignments: &Assignments,
@@ -128,7 +128,7 @@ impl SemanticMinimiser {
128128
let _ = self.domains.push(initial_domain);
129129
}
130130

131-
pub fn clean_up(&mut self) {
131+
pub(crate) fn clean_up(&mut self) {
132132
// Remove the domain ids from the present domain ids.
133133
let vals: Vec<DomainId> = self.present_ids.iter().copied().collect();
134134
for domain_id in vals {

‎pumpkin-solver/src/engine/conflict_analysis/resolvers/resolution_resolver.rs

Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -9,6 +9,7 @@ use crate::engine::conflict_analysis::minimisers::Mode;
99
use crate::engine::conflict_analysis::minimisers::RecursiveMinimiser;
1010
use crate::engine::conflict_analysis::ConflictAnalysisContext;
1111
use crate::engine::conflict_analysis::LearnedNogood;
12+
use crate::engine::propagation::CurrentNogood;
1213
use crate::engine::Assignments;
1314
use crate::predicates::Predicate;
1415
use crate::pumpkin_assert_advanced;
@@ -140,6 +141,11 @@ impl ConflictResolver for ResolutionResolver {
140141
let reason = ConflictAnalysisContext::get_propagation_reason(
141142
predicate,
142143
context.assignments,
144+
CurrentNogood::new(
145+
&self.to_process_heap,
146+
&self.processed_nogood_predicates,
147+
&self.predicate_id_generator,
148+
),
143149
context.reason_store,
144150
context.propagators,
145151
context.proof_log,
@@ -196,6 +202,11 @@ impl ConflictResolver for ResolutionResolver {
196202
let reason = ConflictAnalysisContext::get_propagation_reason(
197203
predicate,
198204
context.assignments,
205+
CurrentNogood::new(
206+
&self.to_process_heap,
207+
&self.processed_nogood_predicates,
208+
&self.predicate_id_generator,
209+
),
199210
context.reason_store,
200211
context.propagators,
201212
context.proof_log,
@@ -218,6 +229,11 @@ impl ConflictResolver for ResolutionResolver {
218229
let reason = ConflictAnalysisContext::get_propagation_reason(
219230
next_predicate,
220231
context.assignments,
232+
CurrentNogood::new(
233+
&self.to_process_heap,
234+
&self.processed_nogood_predicates,
235+
&self.predicate_id_generator,
236+
),
221237
context.reason_store,
222238
context.propagators,
223239
context.proof_log,

‎pumpkin-solver/src/engine/constraint_satisfaction_solver.rs

Lines changed: 13 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -38,7 +38,9 @@ use crate::engine::conflict_analysis::ConflictResolver as Resolver;
3838
use crate::engine::cp::PropagatorQueue;
3939
use crate::engine::cp::WatchListCP;
4040
use crate::engine::predicates::predicate::Predicate;
41+
use crate::engine::propagation::CurrentNogood;
4142
use crate::engine::propagation::EnqueueDecision;
43+
use crate::engine::propagation::ExplanationContext;
4244
use crate::engine::propagation::LocalId;
4345
use crate::engine::propagation::PropagationContext;
4446
use crate::engine::propagation::PropagationContextMut;
@@ -1114,7 +1116,11 @@ impl ConstraintSatisfactionSolver {
11141116
// Look up the reason for the bound that changed.
11151117
// The reason for changing the bound cannot be a decision, so we can safely unwrap.
11161118
let reason_changing_bound = reason_store
1117-
.get_or_compute(entry.reason.unwrap(), assignments, propagators)
1119+
.get_or_compute(
1120+
entry.reason.unwrap(),
1121+
ExplanationContext::from(&*assignments),
1122+
propagators,
1123+
)
11181124
.unwrap();
11191125

11201126
let mut empty_domain_reason: Vec<Predicate> = vec![
@@ -1241,7 +1247,11 @@ impl ConstraintSatisfactionSolver {
12411247
// Get the conjunction of predicates explaining the propagation.
12421248
let reason = self
12431249
.reason_store
1244-
.get_or_compute(reason, &self.assignments, &mut self.propagators)
1250+
.get_or_compute(
1251+
reason,
1252+
ExplanationContext::new(&self.assignments, CurrentNogood::empty()),
1253+
&mut self.propagators,
1254+
)
12451255
.expect("Reason ref is valid");
12461256

12471257
let propagated = entry.predicate;
@@ -1317,7 +1327,7 @@ impl ConstraintSatisfactionSolver {
13171327
/// If the solver is already in a conflicting state, i.e. a previous call to this method
13181328
/// already returned `false`, calling this again will not alter the solver in any way, and
13191329
/// `false` will be returned again.
1320-
pub fn add_propagator(
1330+
pub(crate) fn add_propagator(
13211331
&mut self,
13221332
propagator_to_add: impl Propagator + 'static,
13231333
tag: Option<NonZero<u32>>,

‎pumpkin-solver/src/engine/cp/domain_events.rs

Lines changed: 11 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -3,36 +3,37 @@ use enumset::EnumSet;
33

44
use crate::engine::IntDomainEvent;
55

6+
#[derive(Debug, Copy, Clone)]
7+
pub(crate) struct DomainEvents {
8+
int_events: Option<EnumSet<IntDomainEvent>>,
9+
}
10+
611
impl DomainEvents {
712
/// DomainEvents with both lower and upper bound tightening (but not other value removal).
8-
pub const BOUNDS: DomainEvents = DomainEvents::create_with_int_events(enum_set!(
13+
pub(crate) const BOUNDS: DomainEvents = DomainEvents::create_with_int_events(enum_set!(
914
IntDomainEvent::LowerBound | IntDomainEvent::UpperBound
1015
));
1116
// this is all options right now, but won't be once we add variables of other types
1217
/// DomainEvents with lower and upper bound tightening, assigning to a single value, and
1318
/// single value removal.
14-
pub const ANY_INT: DomainEvents = DomainEvents::create_with_int_events(enum_set!(
19+
pub(crate) const ANY_INT: DomainEvents = DomainEvents::create_with_int_events(enum_set!(
1520
IntDomainEvent::Assign
1621
| IntDomainEvent::LowerBound
1722
| IntDomainEvent::UpperBound
1823
| IntDomainEvent::Removal
1924
));
2025
/// DomainEvents with only lower bound tightening.
21-
pub const LOWER_BOUND: DomainEvents =
26+
pub(crate) const LOWER_BOUND: DomainEvents =
2227
DomainEvents::create_with_int_events(enum_set!(IntDomainEvent::LowerBound));
2328
/// DomainEvents with only upper bound tightening.
24-
pub const UPPER_BOUND: DomainEvents =
29+
#[allow(unused, reason = "will be part of public API at some point")]
30+
pub(crate) const UPPER_BOUND: DomainEvents =
2531
DomainEvents::create_with_int_events(enum_set!(IntDomainEvent::UpperBound));
2632
/// DomainEvents with only assigning to a single value.
27-
pub const ASSIGN: DomainEvents =
33+
pub(crate) const ASSIGN: DomainEvents =
2834
DomainEvents::create_with_int_events(enum_set!(IntDomainEvent::Assign));
2935
}
3036

31-
#[derive(Debug, Copy, Clone)]
32-
pub struct DomainEvents {
33-
int_events: Option<EnumSet<IntDomainEvent>>,
34-
}
35-
3637
impl DomainEvents {
3738
pub(crate) const fn create_with_int_events(
3839
int_events: EnumSet<IntDomainEvent>,

0 commit comments

Comments
 (0)