Decompose Global (cpmpy.transformations.decompose_global)

Functions to decompose global constraints and global functions not supported by the solver.

This transformation is necessary for all non-CP solvers, and also used to decompose global constraints and global functions not implemented in a CP-solver.

While a solver may natively support a global constraint, it may not support it natively in a reified context. In this case, we will als also decompose the global constraint.

For numerical global functions, we will only decompose them if they are not supported in non-reified context. Even if the solver does not explicitely support them in a subexpression, we can rewrite them using func:cpmpy.transformations.reification.reify_rewrite to a non-reified version when the function is total. E.g., bv <-> max(a,b,c) >= 4 can be rewritten as [bv <-> IV0 >= 4, IV0 == max(a,b,c)]

Unsupported global constraints and global functions are decomposed in-place and the resulting set of constraints is wrapped in a conjunction. E.g., x + ~AllDifferent(a,b,c) >= 2 is decomposed into x + ~((a) != (b) & (a) != (c) & (b) != (c)) >= 2 This allows to post the decomposed expression tree to the solver if it supports it (e.g., SMT-solvers, MiniZinc, CPO)

cpmpy.transformations.decompose_global.decompose_in_tree(lst_of_expr: Sequence[Expression], supported: Set[str] = {}, supported_reified: Set[str] = {}, _toplevel=None, nested=False, csemap: CSEMap | None = None, decompose_custom: Dict[str, Callable] | None = None) → List[Expression][source]

Decomposes global constraint or global function not supported by the solver.

Accepts a list of CPMpy expressions as input and returns a (new) list of CPMpy expressions.

Parameters:

  • lst_of_expr – list of CPMpy expressions that may contain global constraints or global functions.

  • supported – a set of names of supported global constraints and global functions (will not be decomposed).

  • supported_reified – a set of names of supported reified global constraints (those with Boolean return type only).

  • _toplevel – DEPRECATED

  • nested – DEPRECATED

  • csemap – a dictionary of ‘expr: expr’ mappings, for Common Subexpression Elimination

Supported numerical global functions remain in the expression tree as is. They can be rewritten using cpmpy.transformations.reification.reify_rewrite() E.g. bv -> NumExpr <comp> Var/Const will then be rewritten as [bv -> IV0 <comp> Var/Const, NumExpr == IV0].

cpmpy.transformations.decompose_global.decompose_objective(expr: Expression, supported: Set[str] = {}, supported_reified: Set[str] = {}, csemap: CSEMap | None = None, decompose_custom: Dict[str, Callable] | None = None) → Tuple[Expression, List[Expression]][source]

Decompose any global constraint or global function not supported by the solver in the objective function expression (numeric or global).

Accepts a single objective expression and returns the decomposed expression plus a list of auxiliary constraints to add as model constraints.

Parameters:

  • expr – objective expression (e.g. min(x), sum(arr)).

  • supported – a set of names of supported global constraints and global functions (will not be decomposed).

  • supported_reified – a set of names of supported reified global constraints (those with Boolean return type only).

  • csemap – a dictionary of ‘expr: expr’ mappings, for Common Subexpression Elimination

Returns:

(decomp_expr, toplevel) where decomp_expr is the decomposed objective and toplevel is the list of auxiliary constraints.

Warning

The returned toplevel list may itself contain global constraints or functions. When adding these to the solver, the solver should still decompose them.