Overhaul predicate simplifier

[ttuegel]

This issue is the first part of addressing the issues raised in #2400. See also: #2566.

We will move Condition.simplifyPredicate to its own module and implement a Predicate.simplify similar to TermLike.simplify. It must not call simplifyCondition or simplifyTermLike. Predicate.simplify will simplify a Predicate from the bottom up; at each level, it will iterate until the predicate does not change.

Questions:

• What should be the return type of Predicate.simplify? Two reasonable-seeming options are a disjunction of Conditions, or a disjunction of MultiAnd (Predicate _). In the former case, the Condition will not be simplified. What does the condition simplifier expect?

[ttuegel]

@ana-pantilie I would appreciate your thoughts on this.

[ttuegel]

As for the return type of Predicate.simplify, I'm inclined to return the disjunction of MultiAnd (Predicate _) for these reasons:

• I can't think of any reason the Predicate simplifier shouldn't return something that isn't basically a predicate.
• The implementation will be simpler.
• The Condition simplifier that calls Predicate.simplify can easily break down a MultiAnd (Predicate _) into a Condition _.

[ana-pantilie]

I think that from the point of view of the Condition simplifier, a disjunction of MultiAnd (Predicate ..) would be fine. We already go back and forth between Condition and MultiAnd there.

One thing is that the ML pattern simplifiers return disjunctions of Patterns or of Conditions, so we'd still have to turn that into a MultiAnd (Predicate _) at the end, unless there's something nicer we could do.