Convert reification constraints (cpmpy.transformations.reification)
- cpmpy.transformations.reification.only_implies(constraints)[source]
Transforms all reifications to BV -> BE form
- More specifically:
- BV0 -> BV2 == BV3 :: BV0 -> (BV2->BV3 & BV3->BV2)
:: BV0 -> (BV2->BV3) & BV0 -> (BV3->BV2) :: BV0 -> (~BV2|BV3) & BV0 -> (~BV3|BV2)
BV == BE :: ~BV -> ~BE, BV -> BE
Assumes all constraints are in ‘flat normal form’ and all reifications have a variable in lhs. Hence, only apply AFTER flatten() and ‘only_bv_reifies()’.
- cpmpy.transformations.reification.reify_rewrite(constraints, supported=frozenset({}))[source]
Rewrites reified constraints not natively supported by a solver, to a version that uses standard constraints and reification over equalities between variables.
Input is expected to be in Flat Normal Form without unsupported globals present. (so after flatten_constraint() and ‘decompose_global()’) Output will also be in Flat Normal Form
Boolean expressions ‘and’, ‘or’, and ‘->’ and comparison expression ‘IV1==IV2’ are assumed to support reification (actually currently all comparisons <op> in {‘==’, ‘!=’, ‘<=’, ‘<’, ‘>=’, ‘>’},
IV1 <op> IV2 are assumed to support reification BV -> (IV1 <op> IV2))
- :param supported a (frozen)set of expression names that support reification in the solver, including
supported ‘Left Hand Side (LHS)’ expressions in reified comparisons, e.g. BV -> (LHS == V)