Repository navigation
Conversation
… in XCSP (+ to fzn)
The degree of the XCSP variable should be different from 0 to be really created in the choco model.
…ation" of a failure is too big (=all variables)
… Expression (XCSP3)
…ory footprint when using PropSTR2+
…laration (for RoundRobin mainly)
…ico order for breaking ties
+add model and decision path to AbstractStrategy
+ delete ValueSortedMap.java
Can be used to map double to Identity-based objects
… to MiniSat#doReduceDB(). This is done by storing separately failure clauses and prohibiting-solution ones in MiniSat#learnts
…ents generated by propagateSat() can be lost because of `onPropagatorExecution` not placed correctly + fix typo in IntCircularQueue#toString
…les). See 2025/hitori with 5.1.dzn
…d of CT + add new option 'maxSizeInMBToUseCompactTable' in Settings + STR2+ now manages tuples without ISet (IStateInt + int[] instead)
+ correction of few propagators which were incorrect + correction of false literal declaration (init of MiniSat) + correction of assertion message and showReason
| /** | ||
| * Indicates if all literals but one are false in the clause. | ||
| * By implication, the remaining literal is the asserting literal. | ||
| * By contract, the literal at index 0 is the asserting literal and should not be considered. |
There was a problem hiding this comment.
I find the combination of "literal at index 0 ... should not be considered" and "allFalseButOne" confusing.
My first understanding is that were are checking that all literals but one are false, starting from position 1, whereas the code check that they are all false. If the code is correct, I would rephrase the doc :
"By contract, the literal at index 0 is the asserting literal and always true."
There was a problem hiding this comment.
Your first understanding is correct: we are checking that all literals but one are false, starting from position 1.
The loop starts at 1 (not 0) and if a literal is not false, the loop is broken and false is returned.
Then, the contract is not that the literal at 0 is always true.
In its current usage (for assertion only), it should be undefined, otherwise there is a problem somewhere (indeed, the current cannot explain an event that already occurs).
Note that if this method is called somewhere else in the code, the assertion can be wrong, though, since it must be true only when a literal is satisfied or falsified.
Its easier (from a conception perspective) to keep the method in the Clause class, but I agree that it can be renamed for clarity.
| * @param vars array of integer variables | ||
| * @param except array of values that can be excluded from the allDifferent constraint | ||
| */ | ||
| default void allDifferentExceptDec2(IntVar[] vars, int[] except) { |
There was a problem hiding this comment.
What about "allDifferentExceptDecBasedOnGCC" ? Or "allDifferentExceptDecByGCC" ?
| * If a task is optional, it can be performed with a duration of 0 and the other mandatory tasks can overlap it. | ||
| * Otherwise, the task must be performed and cannot be overlapped by any other task even if it has a duration of 0. |
There was a problem hiding this comment.
This is not clear to me. I don't see, from the code, where the optionality of a task does intervene ? And shouldn't the optional tasks that are performed be considered as mandatory tasks ?
There was a problem hiding this comment.
Following the MiniZinc definition (for which this decomposition has been written) a task with 0-duration is considered as optional, and can be overlapped.
But, if strict is set to true, a 0-duration task cannot be overlapped.
There was a problem hiding this comment.
Ok this is clearer for the definition and I agree on the documentation.
I still would precise that optionality is treated as the possibility of the task to have a null-duration (as it is the only criteria taken into account in the code wrt optionality of tasks)
| int u = Y.getUB(); | ||
| if (l >= 0) { | ||
| absY.updateLowerBound(l, this, lcg() ? Reason.r(Y.getMinLit()) : Reason.undef()); | ||
| absY.updateUpperBound(u, this, lcg() ? Reason.r(Y.getMinLit(), Y.getMaxLit()) : Reason.undef()); |
There was a problem hiding this comment.
Why is there Y.getMinLit() in the explanation ?
There was a problem hiding this comment.
Because l (Y.getLB()) is >=0, which could happen due to filtering of Y lower bound.
Consider the case where Y = [-10, 5], then |Y| = [0,10]
If an event set Y to [2,5], then |Y| = [2,5] and the modification of |Y| upper bound is due to the current upper bound of Y and the fact the lower bound of Y changes (to a value >= 0)
There was a problem hiding this comment.
I would have expected the explanation to therefore be Reason.r(Y.getLELit(-1), Y.getMaxLit()) but it would only work for enumerated-domains' variables. Maybe we could rely on the getNegGeqLit and getNegLeqLit functions I used in PropagatorCumulative (by making them static functions in Reason ?)
+ taking PR comments into account
* copy based reliable iterators for swap and list based sets * fix linkedlist and graph var * fix swap sets + refactoring * add unit test * optimize method * add test group * add tests in ReifiedConnectivityTest
4 participants
These changes include the following: