Break-up new top-level _andBool_ in evaluatePattern' (#4070)

This PR breaks-up new symbolic conjuncts when simplifying a pattern.

It is useful in conjunction K rule:
```
 rule [notBool-or]:  notBool ( A  orBool B ) => ( notBool A ) andBool ( notBool B ) [simplification]
```

Author: geo2a

booster/library/Booster/Pattern/ApplyEquations.hs

@@ -479,12 +479,16 @@ evaluatePattern' pat@Pattern{term, ceilConditions} = withPatternContext pat $ do
     traverse_ simplifyAssumedPredicate . predicates =<< getState
     -- this may yield additional new constraints, left unevaluated
     evaluatedConstraints <- predicates <$> getState
+    -- break-up introduced symbolic _andBool_, filter-out trivial truth, de-duplicate
+    let flattenedEvaluatedConstraints =
+            Set.unions . Set.map (Set.fromList . filter (/= Predicate TrueBool) . splitBoolPredicates) $
+                evaluatedConstraints
     -- The interface-level evaluatePattern puts pat.substitution together with pat.constraints
     -- into the simplifier state as known truth. Here the substitution will bubble-up as part of
     -- evaluatedConstraints. To avoid duplicating constraints (i.e. having equivalent entities
     -- in pat.predicate and pat.substitution), we discard the old substitution here
     -- and extract a possible simplified one from evaluatedConstraints.
-    let (simplifiedSubsitution, simplifiedConstraints) = extractSubstitution (Set.toList evaluatedConstraints)
+    let (simplifiedSubsitution, simplifiedConstraints) = extractSubstitution . Set.toList $ flattenedEvaluatedConstraints
 
     pure
         Pattern