Skip to content
Draft
Show file tree
Hide file tree
Changes from 13 commits
Commits
Show all changes
25 commits
Select commit Hold shift + click to select a range
ce4da57
feat: initial setup for making literal wrapper around atomic
ImkoMarijnissen Mar 24, 2026
2363a7e
chore: cleanup
ImkoMarijnissen Mar 26, 2026
5224ac3
chore: place todo in bool2int
ImkoMarijnissen Mar 26, 2026
856e025
refactor: avoid duplicate notification + properly notifying or removal
ImkoMarijnissen Mar 26, 2026
ff21389
fix: bug in notifications not working properly
ImkoMarijnissen Mar 26, 2026
233f391
chore: remove check for duplicate notifications in system
ImkoMarijnissen Mar 26, 2026
22561ac
refactor: create structure for watch list literals and predicate ids
ImkoMarijnissen Mar 27, 2026
e9b25e1
Merge branch 'main' into feat/literal-atomic
ImkoMarijnissen Apr 1, 2026
0657c57
fix: add enum for integer variable to be able to post elements
ImkoMarijnissen Apr 1, 2026
1e32139
fix: introduce enum for boolean + fixing backtrack events + correctly…
ImkoMarijnissen Apr 1, 2026
b8c8b9b
fix: initial attempt at fix for python interface
ImkoMarijnissen Apr 1, 2026
0812291
refactor: moving everything to IntExpression
ImkoMarijnissen Apr 2, 2026
63b8a11
fix: issues with python interface
ImkoMarijnissen Apr 2, 2026
08bd014
refactor: merge watch lists
ImkoMarijnissen Apr 2, 2026
137ca1e
refactor: WIP - remove literal in its entirety and move to predicate
ImkoMarijnissen Apr 10, 2026
f7743a2
fix: test cases + update docs
ImkoMarijnissen Apr 29, 2026
90647bb
Merge branch 'main' into feat/literal-atomic
ImkoMarijnissen Apr 29, 2026
1232285
refactor: rename to AnyInteger and move to new file
ImkoMarijnissen Apr 29, 2026
895b8e3
refactor: do not store affineview in AnyInteger
ImkoMarijnissen Apr 29, 2026
c3e2b63
fix: affine view
ImkoMarijnissen Apr 29, 2026
35a4b22
chore: apply comments
ImkoMarijnissen Apr 30, 2026
6d3ffa6
Merge branch 'main' into feat/literal-atomic
ImkoMarijnissen Apr 30, 2026
1339241
fix: as_expression to as_integer
ImkoMarijnissen Apr 30, 2026
e587c93
test: use bitset for tracking whether predicateid has already been no…
ImkoMarijnissen May 1, 2026
ae1c0c4
fix: properly check whether predicate id notification has occurred
ImkoMarijnissen May 1, 2026
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
13 changes: 7 additions & 6 deletions pumpkin-crates/constraints/src/constraints/boolean.rs
Original file line number Diff line number Diff line change
Expand Up @@ -4,11 +4,12 @@ use pumpkin_core::constraints::Constraint;
use pumpkin_core::proof::ConstraintTag;
use pumpkin_core::variables::AffineView;
use pumpkin_core::variables::DomainId;
use pumpkin_core::variables::IntegerVariableEnum;
use pumpkin_core::variables::Literal;
use pumpkin_core::variables::TransformableVariable;

use super::equals;
use super::less_than_or_equals;
use crate::equals;

/// Creates the [`Constraint`] `∑ weights_i * bools_i <= rhs`.
pub fn boolean_less_than_or_equals(
Expand Down Expand Up @@ -67,11 +68,11 @@ impl Constraint for BooleanLessThanOrEqual {
}

impl BooleanLessThanOrEqual {
fn create_domains(&self) -> Vec<AffineView<DomainId>> {
fn create_domains(&self) -> Vec<AffineView<Literal>> {
self.bools
.iter()
.enumerate()
.map(|(index, bool)| bool.get_integer_variable().scaled(self.weights[index]))
.map(|(index, bool)| bool.scaled(self.weights[index]))
.collect()
}
}
Expand Down Expand Up @@ -102,12 +103,12 @@ impl Constraint for BooleanEqual {
}

impl BooleanEqual {
fn create_domains(&self) -> Vec<AffineView<DomainId>> {
fn create_domains(&self) -> Vec<IntegerVariableEnum> {
self.bools
.iter()
.enumerate()
.map(|(index, bool)| bool.get_integer_variable().scaled(self.weights[index]))
.chain(std::iter::once(self.rhs.scaled(-1)))
.map(|(index, bool)| bool.scaled(self.weights[index]).into())
.chain(std::iter::once(self.rhs.scaled(-1).into()))
.collect()
}
}
1 change: 1 addition & 0 deletions pumpkin-crates/core/src/api/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -52,6 +52,7 @@ pub mod variables {
pub use crate::engine::variables::AffineView;
pub use crate::engine::variables::DomainId;
pub use crate::engine::variables::IntegerVariable;
pub use crate::engine::variables::IntegerVariableEnum;
pub use crate::engine::variables::Literal;
pub use crate::engine::variables::TransformableVariable;
}
Expand Down
4 changes: 2 additions & 2 deletions pumpkin-crates/core/src/api/solver.rs
Original file line number Diff line number Diff line change
Expand Up @@ -102,7 +102,7 @@ pub struct Solver {
impl Default for Solver {
fn default() -> Self {
let satisfaction_solver = ConstraintSatisfactionSolver::default();
let true_literal = Literal::new(Predicate::trivially_true().get_domain());
let true_literal = Literal::new(Predicate::trivially_true());
Self {
satisfaction_solver,
true_literal,
Expand All @@ -114,7 +114,7 @@ impl Solver {
/// Creates a solver with the provided [`SolverOptions`].
pub fn with_options(solver_options: SolverOptions) -> Self {
let satisfaction_solver = ConstraintSatisfactionSolver::new(solver_options);
let true_literal = Literal::new(Predicate::trivially_true().get_domain());
let true_literal = Literal::new(Predicate::trivially_true());
Self {
satisfaction_solver,
true_literal,
Expand Down
87 changes: 87 additions & 0 deletions pumpkin-crates/core/src/engine/cp/assignments.rs
Original file line number Diff line number Diff line change
Expand Up @@ -288,6 +288,15 @@ impl Assignments {
self.is_domain_assigned(var).then(|| var.lower_bound(self))
}

pub(crate) fn get_assigned_value_at_trail_position<Var: IntegerVariable>(
&self,
var: &Var,
trail_position: usize,
) -> Option<i32> {
self.is_domain_assigned_at_trail_position(var, trail_position)
.then(|| var.lower_bound(self))
}

pub(crate) fn is_decision_predicate(&self, predicate: &Predicate) -> bool {
let domain = predicate.get_domain();
if let Some(trail_position) = self.get_trail_position(predicate)
Expand Down Expand Up @@ -368,6 +377,15 @@ impl Assignments {
var.lower_bound(self) == var.upper_bound(self)
}

pub(crate) fn is_domain_assigned_at_trail_position<Var: IntegerVariable>(
&self,
var: &Var,
trail_position: usize,
) -> bool {
var.lower_bound_at_trail_position(self, trail_position)
== var.upper_bound_at_trail_position(self, trail_position)
}

/// Returns the index of the trail entry at which point the given predicate became true.
/// In case the predicate is not true, then the function returns None.
/// Note that it is not necessary for the predicate to be explicitly present on the trail,
Expand Down Expand Up @@ -617,6 +635,66 @@ impl Assignments {
Ok(update_took_place)
}

/// Determines whether the provided [`Predicate`] holds at the provided trail position. In case
/// the predicate is not assigned yet (neither true nor false), returns None.
pub(crate) fn evaluate_predicate_at_trail_position(
&self,
predicate: Predicate,
trail_position: usize,
) -> Option<bool> {
let domain_id = predicate.get_domain();
let value = predicate.get_right_hand_side();

match predicate.get_predicate_type() {
PredicateType::LowerBound => {
if self.get_lower_bound_at_trail_position(domain_id, trail_position) >= value {
Some(true)
} else if self.get_upper_bound_at_trail_position(domain_id, trail_position) < value
{
Some(false)
} else {
None
}
}
PredicateType::UpperBound => {
if self.get_upper_bound_at_trail_position(domain_id, trail_position) <= value {
Some(true)
} else if self.get_lower_bound_at_trail_position(domain_id, trail_position) > value
{
Some(false)
} else {
None
}
}
PredicateType::NotEqual => {
if !self.is_value_in_domain_at_trail_position(domain_id, value, trail_position) {
Some(true)
} else if let Some(assigned_value) =
self.get_assigned_value_at_trail_position(&domain_id, trail_position)
{
// Previous branch concluded the value is not in the domain, so if the variable
// is assigned, then it is assigned to the not equals value.
pumpkin_assert_simple!(assigned_value == value);
Some(false)
} else {
None
}
}
PredicateType::Equal => {
if !self.is_value_in_domain_at_trail_position(domain_id, value, trail_position) {
Some(false)
} else if let Some(assigned_value) =
self.get_assigned_value_at_trail_position(&domain_id, trail_position)
{
pumpkin_assert_moderate!(assigned_value == value);
Some(true)
} else {
None
}
}
}
}

/// Determines whether the provided [`Predicate`] holds in the current state of the
/// [`Assignments`]. In case the predicate is not assigned yet (neither true nor false),
/// returns None.
Expand Down Expand Up @@ -673,6 +751,15 @@ impl Assignments {
.is_some_and(|truth_value| truth_value)
}

pub(crate) fn is_predicate_satisfied_at_trail_position(
&self,
predicate: Predicate,
trail_position: usize,
) -> bool {
self.evaluate_predicate_at_trail_position(predicate, trail_position)
.is_some_and(|truth_value| truth_value)
}

#[allow(unused, reason = "makes sense to have in this API")]
pub(crate) fn is_predicate_falsified(&self, predicate: Predicate) -> bool {
self.evaluate_predicate(predicate)
Expand Down
2 changes: 1 addition & 1 deletion pumpkin-crates/core/src/engine/cp/test_solver.rs
Original file line number Diff line number Diff line change
Expand Up @@ -86,7 +86,7 @@ impl TestSolver {

pub fn new_literal(&mut self) -> Literal {
let domain_id = self.new_variable(0, 1);
Literal::new(domain_id)
Literal::new(predicate!(domain_id >= 1))
}

pub fn new_propagator<Constructor>(
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -4,9 +4,13 @@ use enumset::EnumSet;
use enumset::EnumSetType;

use crate::containers::KeyedVec;
use crate::engine::Assignments;
use crate::engine::TrailedValues;
use crate::engine::notifications::NotificationEngine;
use crate::engine::variables::DomainId;
use crate::predicates::Predicate;
use crate::propagation::PropagatorVarId;
use crate::variables::Literal;

#[derive(Default, Debug, Clone)]
pub(crate) struct WatchListDomainEvents {
Expand All @@ -22,6 +26,40 @@ pub(crate) struct WatchListDomainEvents {
pub struct Watchers<'a> {
propagator_var: PropagatorVarId,
notification_engine: &'a mut NotificationEngine,
trailed_values: &'a mut TrailedValues,
assignments: &'a Assignments,
}

impl<'a> Watchers<'a> {
pub(crate) fn watch_literal(&mut self, literal: Literal, events: EnumSet<DomainEvent>) {
self.notification_engine.watch_literal(
literal,
events,
self.propagator_var,
self.trailed_values,
self.assignments,
)
}

pub(crate) fn watch_literal_backtrack(
&mut self,
literal: Literal,
events: EnumSet<DomainEvent>,
) {
self.notification_engine.watch_literal_backtrack(
literal,
events,
self.propagator_var,
self.trailed_values,
self.assignments,
)
}

pub(crate) fn unwatch_predicate(&mut self, predicate: Predicate) {
let predicate_id = self.notification_engine.get_id(predicate);
self.notification_engine
.unwatch_predicate(predicate_id, self.propagator_var.propagator);
}
}

/// A description of the kinds of events that can happen on a domain variable.
Expand Down Expand Up @@ -95,10 +133,14 @@ impl<'a> Watchers<'a> {
pub(crate) fn new(
propagator_var: PropagatorVarId,
notification_engine: &'a mut NotificationEngine,
trailed_values: &'a mut TrailedValues,
assignments: &'a Assignments,
) -> Self {
Watchers {
propagator_var,
notification_engine,
trailed_values,
assignments,
}
}

Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -6,3 +6,5 @@ pub use domain_event_watch_list::DomainEvent;
pub(crate) use domain_event_watch_list::WatchListDomainEvents;
pub(crate) use domain_event_watch_list::Watchers;
pub(crate) use event_sink::*;
pub(crate) use watch_list_predicate_id::PredicateWatchList;
mod watch_list_predicate_id;
Original file line number Diff line number Diff line change
@@ -0,0 +1,92 @@
use enumset::EnumSet;

use crate::basic_types::PredicateId;
use crate::containers::HashMap;
use crate::containers::KeyedVec;
use crate::propagation::DomainEvent;
use crate::propagation::LocalId;
use crate::propagation::PropagatorVarId;
use crate::state::PropagatorId;
use crate::variables::Literal;

#[derive(Debug, Default, Clone)]
pub(crate) struct PredicateWatchList {
/// The watch list from predicates to propagators.
pub(crate) watch_list_predicate_id: KeyedVec<PredicateId, Vec<PropagatorId>>,
// TODO: Should use direct hashing
pub(crate) literal_watch_list:
HashMap<Literal, HashMap<PropagatorId, (LocalId, EnumSet<DomainEvent>)>>,
pub(crate) literal_watch_list_backtrack:
HashMap<Literal, HashMap<PropagatorId, (LocalId, EnumSet<DomainEvent>)>>,
Comment thread
maartenflippo marked this conversation as resolved.
Outdated
}

impl PredicateWatchList {
pub(crate) fn watch_predicate_id(
&mut self,
predicate_id: PredicateId,
propagator_id: PropagatorId,
) {
self.watch_list_predicate_id
.accomodate(predicate_id, vec![]);
self.watch_list_predicate_id[predicate_id].push(propagator_id);
}

pub(crate) fn watchers_predicate_id_mut(
&mut self,
predicate_id: PredicateId,
) -> Option<&mut Vec<PropagatorId>> {
self.watch_list_predicate_id.get_mut(predicate_id)
}

pub(crate) fn watchers_predicate_id(
&self,
predicate_id: PredicateId,
) -> Option<&Vec<PropagatorId>> {
self.watch_list_predicate_id.get(predicate_id)
}

pub(crate) fn insert_literal_watcher(
&mut self,
literal: Literal,
propagator_var: PropagatorVarId,
events: EnumSet<DomainEvent>,
) {
let entry = self
.literal_watch_list
.entry(literal)
.or_default()
.entry(propagator_var.propagator)
.or_insert((propagator_var.variable, events));
entry.1 |= events;
}

pub(crate) fn insert_literal_watcher_backtrack(
&mut self,
literal: Literal,
propagator_var: PropagatorVarId,
events: EnumSet<DomainEvent>,
) {
let entry = self
.literal_watch_list_backtrack
.entry(literal)
.or_default()
.entry(propagator_var.propagator)
.or_insert((propagator_var.variable, events));
entry.1 |= events;
}

pub(crate) fn watchers_literal_propagator(
&self,
literal: Literal,
propagator_id: PropagatorId,
) -> Option<&(LocalId, EnumSet<DomainEvent>)> {
self.literal_watch_list
.get(&literal)
.and_then(|inner| inner.get(&propagator_id))
.or_else(|| {
self.literal_watch_list
.get(&(!literal))
.and_then(|inner| inner.get(&propagator_id))
})
}
}
Loading
Loading