feat: Make Literal wrapper of Predicate by ImkoMarijnissen · Pull Request #398 · ConSol-Lab/Pumpkin

ImkoMarijnissen · 2026-03-26T13:38:42Z

Related to #375.

This PR aims to move away from having to create a fresh variable for each Literal by making it a wrapper around a Predicate.

Any feedback on this PR is welcome!

TODOs

Figure out how to post bool2int and the boolean equals constraint since it has a list of Literals as input, which sum up to a DomainId, which means that the scaling trick does not work.
I have created a system for tracking when a literal is tracked, in which case the event should use notify instead of notify_predicate.
As discussed in Preprocessing variables #375, backtracking is somewhat tricky; the problem currently is that for a literal, you might now be updated multiple times (since it could occur that the predicate notification notifies of the same Predicate multiple times). This breaks some of the invariants that we have for certain propagators, so these should be double-checked.
Fix issues in the python interface from to_integer_variable being removed.
Use trail for keeping track of the backtrack notification events for literals

EmirDe · 2026-03-26T15:53:10Z

It might be a good idea to briefly describe what has been done, the main idea, and the main change. It would make reviewing easier.

maartenflippo · 2026-03-26T23:06:37Z

A few thoughts on this:

bool2int at the moment is only posted when doing logging a proof with inferences. Otherwise, we use the domain underlying the 0-1 literal as the integer domain. See merge_equivalences.rs for this logic.
Now we have a watchlist for predicates with a local ID (i.e. those that emulate an integer variable) and a watchlist for predicate IDs without a local ID. Perhaps we can merge those? That would mean every predicate receives a local ID. But then the notifier does not have two watch lists for predicates

… finding watchers for literals when negated

maartenflippo

As far as I can tell, this feature is not extensively tested. The test cases with bool2int are not sufficient, since they always have the literal be over a 0-1 variable.

maartenflippo · 2026-04-09T05:31:45Z

+#[derive(Clone, Copy, Debug, PartialEq, Eq, Hash)]
+pub enum IntegerVariableEnum {
+    DomainId(AffineView<DomainId>),
+    Literal(AffineView<Literal>),
+}


Can we move this to pumpkin-solver instead? I don't think we need to pollute the core with this?

Keep in core, but move to different file

maartenflippo · 2026-04-09T05:33:10Z

+#[derive(Clone, Copy, Debug, PartialEq, Eq, Hash)]
+pub enum IntegerVariableEnum {
+    DomainId(AffineView<DomainId>),
+    Literal(AffineView<Literal>),
+}


Can we rename this? We never suffix the type with what kind of type it is. I guess this is done to avoid name clashes with the trait. Perhaps we can call it AnyInteger?

maartenflippo · 2026-04-09T05:33:38Z

+#[derive(Clone, Copy, Debug, PartialEq, Eq, Hash)]
+pub enum IntegerVariableEnum {
+    DomainId(AffineView<DomainId>),
+    Literal(AffineView<Literal>),
+}


Why put the affine view inside the variants? We could unwrap that and let any user wrap the enum with an affine view

maartenflippo · 2026-04-09T05:35:15Z

At this point, what is the reason for keeping Literal? We can do without it I think? We can simply implement IntegerVariable for Predicate?

maartenflippo · 2026-04-09T05:39:04Z

+#[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>)>>,


Conceptually, why would we have predicates with and without a local ID? Can they be watched as both? Would it not be cleaner to say that a notification happens to a LocalId, removing the need for notify_predicate?

After a discussion we decided to keep this distinction for now. It may make sense to simplify this in the future to always associate any registration with a local ID, but it is not clear that goes without problems

Review re-requested

maartenflippo · 2026-04-30T01:19:25Z

-    //!   trait [`TransformableVariable`]) to create an [`AffineView`].
-    //! - Literals ([`Literal`]) - These specify booleans that can be used when interacting with the
-    //!   [`Solver`]. A [`Literal`] can be created using [`Solver::new_literal`].
+    //! We define the following type of variable:


'type' = 'types'
'variable' = 'variables'

maartenflippo · 2026-04-30T01:21:09Z

+    //!  - Represented by [`Predicate`]s when interacting with the [`Solver`]. These can be created
+    //!    [`DomainId`]s using the [`crate::predicate`] macro and are also treated as integer
+    //!    variables by the [`Solver`].


This does not read right, although I am not entirely sure what you want to have written

maartenflippo · 2026-04-30T01:23:22Z

+            .unwatch_predicate(predicate_id, propagator_to_unwatch)
+    }
+
+    pub(crate) fn watch_literal(


Should this be called 'watch_predicate'?

maartenflippo · 2026-04-30T01:30:10Z

+        predicate_notifier.track_predicate(predicate_id, trailed_values, assignments);
+    }
+
+    pub(crate) fn watch_literal(


watch_predicate?

maartenflippo · 2026-04-30T01:31:00Z

    }

-    pub(crate) fn unwatch_predicate(
+    pub(crate) fn watch_literal_backtrack(


watch_predicate_backtrack?

maartenflippo · 2026-04-30T01:32:31Z

+        for (literal, propagator_id) in self
+            .backtrack_events_literals
+            .synchronise(new_checkpoint)
+            .collect::<Vec<_>>()


Is the collect really necessary?

maartenflippo · 2026-04-30T01:33:39Z

+        for predicate_id in self
+            .predicate_notifier
+            .drain_satisfied_predicates()
+            .collect::<Vec<_>>()


Is the collect necessary?

maartenflippo · 2026-04-30T01:34:14Z

+                                predicate_watcher.propagator_id,
+                                propagator.priority(),
+                            );
+                        }


Could we reverse some of the if statements here to reduce the level of indentation?

maartenflippo · 2026-04-30T01:35:03Z

+pub enum AnyInteger {
+    DomainId(DomainId),
+    Predicate(Predicate),
+}


maartenflippo · 2026-04-30T01:39:18Z

+    pub fn as_expression(&self) -> IntExpression {
+        (*self).into()
+    }


can we name this as_integer, like it was before?

Review re-requested

ImkoMarijnissen added 3 commits March 24, 2026 15:41

feat: initial setup for making literal wrapper around atomic

ce4da57

chore: cleanup

2363a7e

chore: place todo in bool2int

5224ac3

ImkoMarijnissen requested review from EmirDe and maartenflippo March 26, 2026 13:38

ImkoMarijnissen changed the title ~~feat: Make Literal wrapped of Predicate~~ feat: Make Literal wrapper of Predicate Mar 26, 2026

ImkoMarijnissen added 3 commits March 26, 2026 15:24

refactor: avoid duplicate notification + properly notifying or removal

856e025

fix: bug in notifications not working properly

ff21389

chore: remove check for duplicate notifications in system

233f391

ImkoMarijnissen added 8 commits March 27, 2026 12:29

refactor: create structure for watch list literals and predicate ids

22561ac

Merge branch 'main' into feat/literal-atomic

e9b25e1

fix: add enum for integer variable to be able to post elements

0657c57

fix: introduce enum for boolean + fixing backtrack events + correctly…

1e32139

… finding watchers for literals when negated

fix: initial attempt at fix for python interface

b8c8b9b

refactor: moving everything to IntExpression

0812291

fix: issues with python interface

63b8a11

refactor: merge watch lists

08bd014

maartenflippo previously requested changes Apr 9, 2026

View reviewed changes

maartenflippo reviewed Apr 9, 2026

View reviewed changes

Comment thread pumpkin-solver-py/src/variables.rs

ImkoMarijnissen added 6 commits April 10, 2026 15:28

refactor: WIP - remove literal in its entirety and move to predicate

137ca1e

fix: test cases + update docs

f7743a2

Merge branch 'main' into feat/literal-atomic

90647bb

refactor: rename to AnyInteger and move to new file

1232285

refactor: do not store affineview in AnyInteger

895b8e3

fix: affine view

c3e2b63

ImkoMarijnissen requested a review from maartenflippo April 29, 2026 14:33

maartenflippo previously requested changes Apr 30, 2026

View reviewed changes

ImkoMarijnissen added 3 commits April 30, 2026 12:09

chore: apply comments

35a4b22

Merge branch 'main' into feat/literal-atomic

6d3ffa6

fix: as_expression to as_integer

1339241

ImkoMarijnissen requested a review from maartenflippo April 30, 2026 10:21

Conversation

ImkoMarijnissen commented Mar 26, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

TODOs

Uh oh!

EmirDe commented Mar 26, 2026

Uh oh!

maartenflippo commented Mar 26, 2026

Uh oh!

maartenflippo left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

maartenflippo Apr 9, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

ImkoMarijnissen commented Mar 26, 2026 •

edited

Loading

maartenflippo Apr 9, 2026 •

edited

Loading