Bind the known constraints expressin

runtimeverification · Oct 23, 2024 · 9bcdc52 · 9bcdc52
1 parent c974346
commit 9bcdc52
Showing 1 changed file with 6 additions and 4 deletions.
diff --git a/booster/library/Booster/Pattern/Rewrite.hs b/booster/library/Booster/Pattern/Rewrite.hs
@@ -435,12 +435,13 @@ applyRule pat@Pattern{ceilConditions} rule =
         -- apply substitution to rule requires
         let ruleRequires =
                 concatMap (splitBoolPredicates . coerce . substituteInTerm matchingSubst . coerce) rule.requires
+            knownConstraints = pat.constraints <> (Set.fromList . asEquations $ pat.substitution)
 
         -- filter out any predicates known to be _syntactically_ present in the known prior
         toCheck <-
             lift $
                 filterOutKnownConstraints
-                    (pat.constraints <> (Set.fromList . asEquations $ pat.substitution))
+                    knownConstraints
                     ruleRequires
 
         -- simplify the constraints (one by one in isolation). Stop if false, abort rewrite if indeterminate.
@@ -450,7 +451,7 @@ applyRule pat@Pattern{ceilConditions} rule =
                     ( checkConstraint
                         id
                         notAppliedIfBottom
-                        (pat.constraints <> (Set.fromList . asEquations $ pat.substitution))
+                        knownConstraints
                     )
                     toCheck
 
@@ -459,7 +460,7 @@ applyRule pat@Pattern{ceilConditions} rule =
         stillUnclear <-
             lift $
                 filterOutKnownConstraints
-                    (pat.constraints <> (Set.fromList . asEquations $ pat.substitution))
+                    knownConstraints
                     unclearRequires
 
         -- check unclear requires-clauses in the context of known constraints (priorKnowledge)
@@ -481,13 +482,14 @@ applyRule pat@Pattern{ceilConditions} rule =
         -- apply substitution to rule ensures
         let ruleEnsures =
                 concatMap (splitBoolPredicates . coerce . substituteInTerm matchingSubst . coerce) rule.ensures
+            knownConstraints = pat.constraints <> (Set.fromList . asEquations $ pat.substitution)
         newConstraints <-
             catMaybes
                 <$> mapM
                     ( checkConstraint
                         id
                         trivialIfBottom
-                        (pat.constraints <> (Set.fromList . asEquations $ pat.substitution))
+                        knownConstraints
                     )
                     ruleEnsures