nValues: an exception without message when the limit makes the constraint unsatisfiable (k < 1, or k > |X|) #28

ACE fails, with an exception without message, on a constraint nValues whose limit can never be reached (for example (eq,0), or (eq,k) with k > |X|), instead of saying that the instance is unsatisfiable:

<instance format="XCSP3" type="CSP">
  <variables>
    <array id="x" size="[3]"> 0..2 </array>
  </variables>
  <constraints>
    <nValues>
      <list> x[] </list>
      <condition> (eq,0) </condition>
    </nValues>
  </constraints>
</instance>

Observed: ! ERROR: (java.lang.Exception without message; with -ev: at utility.Kit.control(Kit.java:183), at constraints.global.NValues$NValuesCst.<init>(NValues.java:188)).

Expected: s UNSATISFIABLE (3 variables always take between 1 and 3 distinct values).

Results of the three solvers

with ACE built from the master branch of this repository (83e8b60, embedded in PyCSP3 since xcsp3team/pycsp3#201), CHOCO (choco-parsers-4.10.15-beta, embedded in PyCSP3, and choco-parsers 6.0.2, the latest release, with the same results) and cosoco 2.6.1 (from pip):

• ACE: java -jar ACE-2.6.jar model.xml -s=all -xe -xc=false
• CHOCO: java -cp choco-parsers-4.10.15-beta.jar org.chocosolver.parser.xcsp.ChocoXCSP model.xml -a -f -flt (6.0.2: -a true)
• cosoco: cosoco model.xml -model=2 -nbsols=0

The limits that make the constraint always true ((le,4), (lt,5), (ge,0), (ne,0)) are handled correctly (27 solutions).

Cause

NValuesCst.buildFrom() builds NValuesCstEQ for (eq,k), NValuesCstLE with k - 1 for (lt,k) and NValuesCstGE with k + 1 for (gt,k), whose constructor requires control(1 <= k && k <= list.length) (NValues.java, line 188), without message. The instance is valid: the constraint is just unsatisfiable.

PyCSP3 will evaluate such constraints when compiling (their result being known from the number of terms), so that it will no longer generate them, but the instances are valid and other tools may generate them.

Tests

Found while writing the unit tests of PyCSP3: test_nvalues_with_an_unreachable_condition (NValues(x) == 0, == 5, == -1, > 4, < 1 on 4 variables), test_nvalues_in_groups ([NValues(m[i]) == i for i in range(3)]), test_nvalues_on_integers_only (NValues(1, 2, 1) == 3) and test_nvalues_on_a_single_term in pycsp3/tests/test_constraints_global_nvalues.py: 8 tests.

This issue was found by the unit tests of PyCSP3: xcsp3team/pycsp3#213