Safening (cpmpy.transformations.safening)

Transforms partial functions into total functions.

cpmpy.transformations.safening.no_partial_functions(lst_of_expr, _toplevel=None, _nbc=None, safen_toplevel=frozenset({}))[source]

A partial function is a function whose output is not defined for all possible inputs.

In CPMpy, this is the case for the following 3 numeric functions:

  • (Integer) division x // y: undefined when y=0

  • Modulo x mod y: undefined when y=0

  • Element Arr[idx]: undefined when idx is not in the range of Arr

A toplevel constraint must always be true, so constraint solvers simply propagate the ‘unsafe’ value(s) away. However, CPMpy allows arbitrary nesting and reification of constraints, so an expression like b <-> (Arr[idx] == 5) is allowed, even when variable idx goes outside the bounds of Arr. Should idx be restricted to be in-bounds? and what value should ‘b’ take if it is out-of-bounds?

This transformation will transform a partial function (e.g. Arr[idx]) into a total function following the relational semantics as discussed in:

Frisch, Alan M., and Peter J. Stuckey. “The proper treatment of undefinedness in constraint languages.” International Conference on Principles and Practice of Constraint Programming. Berlin, Heidelberg: Springer Berlin Heidelberg, 2009.

Under the relational semantic, an ‘undefined’ output for a (numerical) expression should propagate to False in the nearest Boolean parent expression. In the above example: idx should be allowed to take a value outside the bounds of Arr, and b should be False in that case.

To enable this, we want to rewrite an expression like b <-> (partial == 5) to something like b <-> (is_defined & (total == 5)). The key idea is to create a copy of the potentially unsafe argument, that can only take ‘safe’ values. Using this new argument in the original expression results in a total function. We now have the original argument variable, which is decoupled from the expression, and a new ‘safe’ argument variable which is used in the expression. The is_defined flag serves two purposes: it represents whether the original argument has a safe value; and if it is true the new argument must equal the original argument so the two are coupled again. If is_defined is false, the new argument remains decoupled (can take any value, as will the function’s output).

Warning

Under the relational semantics, b <-> ~(partial==5) and b <-> (partial!=5) mean different things! The second is b <-> (is_defined & (total!=5)) the first is b <-> (~is_defined | (total!=5)).

A clever observation of the implementation below is that for the above 3 expressions, the ‘safe’ domain of a potentially unsafe argument (y or idx) is either one ‘trimmed’ continuous domain (for idx and in case y = [0..n] or [-n..0]), or two ‘trimmed’ continuous domains (for y=[-n..m]). Furthermore, the reformulation for these two cases can be done generically, without needing to know the specifics of the partial function being made total.

Parameters:

  • list_of_expr – list of CPMpy expressions

  • _toplevel – list of new expressions to put toplevel (used internally)

  • _nbc – list of new expressions to put in nearest Boolean context (used internally)

  • toplevel (safen) – list of expression types that need to be safened, even when toplevel. Used when a solver does not support unsafe values in it’s API (e.g., OR-Tools for div).