Skip to content

feat: Make Literal wrapper of Predicate#398

Draft
ImkoMarijnissen wants to merge 13 commits intomainfrom
feat/literal-atomic
Draft

feat: Make Literal wrapper of Predicate#398
ImkoMarijnissen wants to merge 13 commits intomainfrom
feat/literal-atomic

Conversation

@ImkoMarijnissen
Copy link
Copy Markdown
Contributor

@ImkoMarijnissen ImkoMarijnissen commented Mar 26, 2026

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

@ImkoMarijnissen ImkoMarijnissen changed the title feat: Make Literal wrapped of Predicate feat: Make Literal wrapper of Predicate Mar 26, 2026
@EmirDe
Copy link
Copy Markdown
Contributor

EmirDe commented Mar 26, 2026

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
Copy link
Copy Markdown
Contributor

A few thoughts on this:

  1. 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.
  2. 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

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants