These predicates allow users to mark constraints as e.g. symmetry breaking or redundant, so that solvers can choose to implement them differently.
We cannot easily use annotations for this purpose, since annotations are propagated to all constraints in a decomposition, which may be incorrect for redundant or symmetry breaking constraints in the presence of common subexpression elimination (CSE).
Mark b as an implied constraint (synonym for redundant_constraint)
Mark b as a redundant constraint
Mark b as a symmetry breaking constraint