From e490574524df9ab1059cf20438c1ac1fea4100f3 Mon Sep 17 00:00:00 2001 From: Georgy Lukyanov Date: Wed, 30 Oct 2024 14:45:39 +0100 Subject: [PATCH] Break-up new top-level _andBool_ in evaluatePattern' --- booster/library/Booster/Pattern/ApplyEquations.hs | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/booster/library/Booster/Pattern/ApplyEquations.hs b/booster/library/Booster/Pattern/ApplyEquations.hs index 53b801fcc2..6bb043ce73 100644 --- a/booster/library/Booster/Pattern/ApplyEquations.hs +++ b/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