Safening (cpmpy.transformations.safening)

Transforms partial functions into total functions.

cpmpy.transformations.safening.no_partial_functions(lst_of_expr: list[Expression], _toplevel: Any | None = None, _nbc: Any | None = None, safen_toplevel: AbstractSet[str] | None = None) → list[Expression]

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:

• lst_of_expr (list[Expression]) – list of CPMpy expressions

• _toplevel (None) – DEPRECATED

• _nbc (None) – DEPRECATED

• safen_toplevel (set[str]) – 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), or when the solver does not support the global function, and it needs to be decomposed.

cpmpy.transformations.safening.safen_objective(expr: Expression) → tuple[Expression | int | integer | bool, list[Expression]]

Safen any partial functions in the objective function expression.

Parameters:

expr (Expression) – objective expression (e.g. x // y, arr[x] + arr[y]).

Returns:

tuple[Expression, list[Expression]] safe_expr (Expression): the safened objective expression toplevel (list[Expression]): the list of auxiliary constraints to post at top level.