Skip to content

chore(pumpkin-core): Update cached predicate when known to not be satisfied #601

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
ImkoMarijnissen wants to merge 1 commit into
base: main
Choose a base branch
from
Open

chore(pumpkin-core): Update cached predicate when known to not be satisfied #601

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
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
30 changes: 30 additions & 0 deletions Cargo.lock
View file
Open in desktop

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

13 changes: 13 additions & 0 deletions pumpkin-crates/core/src/propagation/contexts/propagation_context.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -136,6 +136,19 @@ impl<'a> PropagationContext<'a> {
)
}

/// Register the propagator to be enqueued when the predicate with the provided [`PredicateId`]
/// becomes true.
///
/// Avoids looking up the [`PredicateId`] when it is already known.
pub(crate) fn register_predicate_id(&mut self, predicate_id: PredicateId) {
self.notification_engine.watch_predicate_id(
predicate_id,
self.propagator_id,
self.trailed_values,
self.assignments,
)
}

/// Stop being enqueued for the given predicate.
pub fn unregister_predicate(&mut self, predicate_id: PredicateId) {
self.notification_engine
Expand Down
29 changes: 17 additions & 12 deletions pumpkin-crates/core/src/propagators/nogoods/nogood_propagator.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -43,7 +43,6 @@ use crate::propagators::nogoods::WatcherProcessingStatus;
use crate::propagators::nogoods::arena_allocator::ArenaAllocator;
use crate::propagators::nogoods::arena_allocator::NogoodIndex;
use crate::propagators::nogoods::semantic_minimiser::SemanticMinimiser;
use crate::pumpkin_assert_eq_simple;
use crate::pumpkin_assert_extreme;
use crate::pumpkin_assert_moderate;
use crate::pumpkin_assert_simple;
Expand Down Expand Up @@ -418,9 +417,16 @@ impl Propagator for NogoodPropagator {
// Found another predicate that can be the watcher.
found_new_watch = true;

// The old cached predicate is known to not be falsified (otherwise no
// new watcher would be searched for), so we set it to the other
// watcher.
let new_watcher = Watcher {
cached_predicate: nogood_predicates[0],
..watcher
};
Self::replace_watcher(
&mut context,
watcher,
new_watcher,
nogood_predicates,
i,
1,
Expand Down Expand Up @@ -1107,23 +1113,24 @@ impl NogoodPropagator {
.push(NogoodInfo::new_learned_nogood_info(lbd));
let _ = self.inference_codes.push(inference_code);

let watcher = Watcher {
nogood_id,
cached_predicate: self.nogood_predicates.get_nogood(nogood_id)[0],
};

// Now we add two watchers to the first two predicates in the nogood; we are
// guaranteed that these are different predicates
NogoodPropagator::add_watcher(
context,
self.nogood_predicates.get_nogood(nogood_id)[0],
watcher,
Watcher {
nogood_id,
cached_predicate: self.nogood_predicates.get_nogood(nogood_id)[1],
},
&mut self.watch_lists,
);
NogoodPropagator::add_watcher(
context,
self.nogood_predicates.get_nogood(nogood_id)[1],
watcher,
Watcher {
nogood_id,
cached_predicate: self.nogood_predicates.get_nogood(nogood_id)[0],
},
&mut self.watch_lists,
);

Expand Down Expand Up @@ -1380,9 +1387,7 @@ impl NogoodPropagator {
}

if watch_lists[predicate].is_empty() {
let actual_predicate = context.get_predicate(predicate);
let other_id = context.register_predicate(actual_predicate);
pumpkin_assert_eq_simple!(predicate, other_id);
context.register_predicate_id(predicate);
}

watch_lists[predicate].push(watcher);
Expand Down
30 changes: 16 additions & 14 deletions pumpkin-crates/core/src/propagators/nogoods/propagation_mode.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -362,22 +362,23 @@ impl PropagationMode {
let _ = nogood_info.push(NogoodInfo::new_permanent_nogood_info());
let _ = inference_codes.push(inference_code);

let watcher = Watcher {
nogood_id,
cached_predicate: nogood_predicates.get_nogood(nogood_id)[0],
};

NogoodPropagator::add_watcher(
context,
nogood_predicates.get_nogood(nogood_id)[0],
watcher,
Watcher {
nogood_id,
cached_predicate: nogood_predicates.get_nogood(nogood_id)[1],
},
watch_lists,
);

NogoodPropagator::add_watcher(
context,
nogood_predicates.get_nogood(nogood_id)[1],
watcher,
Watcher {
nogood_id,
cached_predicate: nogood_predicates.get_nogood(nogood_id)[0],
},
watch_lists,
);
} else {
Expand All @@ -394,21 +395,22 @@ impl PropagationMode {
let _ = nogood_info.push(NogoodInfo::new_permanent_nogood_info());
let _ = inference_codes.push(inference_code);

let watcher = Watcher {
nogood_id,
cached_predicate: nogood_predicates.get_nogood(nogood_id)[0],
};

NogoodPropagator::add_watcher(
context,
nogood_predicates.get_nogood(nogood_id)[0],
watcher,
Watcher {
nogood_id,
cached_predicate: nogood_predicates.get_nogood(nogood_id)[1],
},
watch_lists,
);
NogoodPropagator::add_watcher(
context,
nogood_predicates.get_nogood(nogood_id)[1],
watcher,
Watcher {
nogood_id,
cached_predicate: nogood_predicates.get_nogood(nogood_id)[0],
},
watch_lists,
);
}
Expand Down
Loading
Loading