simplification
type: Property
domain: Formula
range: Formula
comment: simplification replaces constraints by simpler constraints while preserving logical equivalence

propagation
type: Property
domain: Formula
range: Formula
comment: propagation adds new constraints which are logically redundant but may cause further simplification

commit
type: Property
domain: Formula
range: Formula
comment: the LHS builtin constraints are a precondition on the applicability of the rule

rewrite
type: Property
domain: Formula
range: Formula
comment: only rewrite RHS user constraints in a simplification rule