Decompose Global (cpmpy.transformations.decompose_global)

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 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 gobal constraints and global functions are decomposed in-place 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: list[Expression], supported: set[str] = {}, supported_reified: set[str] = {}, csemap: dict[Expression, Expression] | None = None, _nested=False, decompose_custom: dict[str, Callable] = {}) → list[Expression][source]

Decomposes any global constraint not supported by the solver. Accepts a list of CPMpy expressions as input and returns a list of CPMpy expressions.

Parameters:

  • supported – a set of supported global constraints or global functions

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

  • csemap – a dictionary of CSE-mapped expressions, used to re-use expressions that have already been decomposed

  • _nested – whether to treat the root-level as nested, false by default. For internal use only.

Special care is taken for unsupported global constraints in reified (nested) contexts

Supported numerical global functions remain in the expression tree as is. They can be rewritten using cpmpy.transformations.reification.reify_rewrite() The following bv -> NumExpr <comp> Var/Const can be rewritten as [bv -> IV0 <comp> Var/Const, NumExpr == IV0]. So even if numerical constraints are not supported in reified context, we can rewrite them to non-reified versions if they are total.

cpmpy.transformations.decompose_global.decompose_objective(expr, supported={}, supported_reified={}, csemap=None)[source]