Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Assume the rule remainder condition when checking ensures #4071

Merged
merged 1 commit into from
Nov 1, 2024
Merged

Assume the rule remainder condition when checking ensures #4071

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
14 changes: 10 additions & 4 deletions booster/library/Booster/Pattern/Rewrite.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Just stumbled over this line here. What if ensuredConditions is nil but we have unclearRequiresAfterSmt?
We should probably also clear the equation cache in that case. We are most likely going to return a Branching result immediately, but maybe we find one of the branches simplifies to bottom and proceed.

Expand Down Expand Up @@ -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
Expand Down
Loading