transformations: better document the reification transformation
@@ -81,6 +81,9 @@ def reify_rewrite(constraints, supported=frozenset(['sum', 'wsum'])):
Output will also be in Flat Normal Form
argument 'supported' is a list (or set) of expression names that support reification in the solver
+ including supported 'Left Hand Side' expressions in reified comparisons, e.g. BV -> (LHS == V)
+ Boolean expressions 'and', 'or', and '->' are assumed to support reification
+ (you MUST give an empty supported set if no others are supported...)
"""
if not is_any_list(constraints):
# assume list, so make list
@@ -117,6 +120,9 @@ def reify_rewrite(constraints, supported=frozenset(['sum', 'wsum'])):
elif isinstance(boolexpr, GlobalConstraint):
# Case 2, BE is a GlobalConstraint
# replace BE by its decomposition, then flatten
+ if boolexpr.name in supported:
+ newcons.append(cpm_expr)
+ else:
reifexpr = copy.copy(cpm_expr)
reifexpr.args[boolexpr_index] = all(boolexpr.decompose()) # decomp() returns list
newcons += flatten_constraint(reifexpr)
