Skip to content

Commit

Permalink
Break-up new top-level _andBool_ in evaluatePattern'
Browse files Browse the repository at this point in the history
  • Loading branch information
geo2a committed Oct 30, 2024
1 parent 328cd2c commit e490574
Showing 1 changed file with 5 additions and 1 deletion.
6 changes: 5 additions & 1 deletion booster/library/Booster/Pattern/ApplyEquations.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down

0 comments on commit e490574

Please sign in to comment.