From 856a96f29f3c9c2432bc44db5e1b34df412e882b Mon Sep 17 00:00:00 2001 From: Georgy Lukyanov Date: Fri, 1 Nov 2024 01:18:17 +0100 Subject: [PATCH] Assume the rule remainder condition when checking ensures (#4071) When Booster detects an indeterminate `requires`, it adds it to the constraints on the rewritten `Pattern`. However, when we check the `ensures` clause, we only pass the the constraints on the old pattern as known truth. This PR corrects that by adding the uncertain conditions as additional known truth, as the `ensures` check should be performed on the rewritten pattern, not the old one. --- booster/library/Booster/Pattern/Rewrite.hs | 14 ++++++++++---- 1 file changed, 10 insertions(+), 4 deletions(-) diff --git a/booster/library/Booster/Pattern/Rewrite.hs b/booster/library/Booster/Pattern/Rewrite.hs index 0c60754a7e..920c8ea18e 100644 --- a/booster/library/Booster/Pattern/Rewrite.hs +++ b/booster/library/Booster/Pattern/Rewrite.hs @@ -460,7 +460,10 @@ applyRule pat@Pattern{ceilConditions} rule = -- check ensures constraints (new) from rhs: stop and return `Trivial` if -- any are false, remove all that are trivially true, return the rest - ensuredConditions <- checkEnsures ruleSubstitution + -- + -- we need to add unclearRequiresAfterSmt (if any) as additional known truth, + -- as it may allow us to prune a vacuous state + ensuredConditions <- checkEnsures ruleSubstitution unclearRequiresAfterSmt -- if a new constraint is going to be added, the equation cache is invalid unless (null ensuredConditions) $ do @@ -603,12 +606,15 @@ applyRule pat@Pattern{ceilConditions} rule = SMT.IsValid -> pure [] -- can proceed checkEnsures :: - Substitution -> RewriteRuleAppT (RewriteT io) [Predicate] - checkEnsures matchingSubst = do + Substitution -> [Predicate] -> RewriteRuleAppT (RewriteT io) [Predicate] + checkEnsures matchingSubst unclearRequiresAfterSmt = do -- apply substitution to rule ensures let ruleEnsures = concatMap (splitBoolPredicates . coerce . substituteInTerm matchingSubst . coerce) rule.ensures - knownConstraints = pat.constraints <> (Set.fromList . asEquations $ pat.substitution) + knownConstraints = + pat.constraints + <> (Set.fromList . asEquations $ pat.substitution) + <> Set.fromList unclearRequiresAfterSmt newConstraints <- catMaybes <$> mapM