Georgy/refactor check requires #4035
Merged
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
geo2a
force-pushed
the
georgy/refactor-check-requires
branch
from
ab8bd3e
to
c78d8bb
Compare
geo2a
requested review from
goodlyrottenapple and
jberthold
and removed request for
goodlyrottenapple
| -- can proceed | ||
| pure () | ||
| -- check required constraints from lhs. | ||
| -- Reaction on false/indeterminate is varies depending on the equation's type (function/simplification), |
There was a problem hiding this comment.
Suggested change
| -- Reaction on false/indeterminate is varies depending on the equation's type (function/simplification), | |
| -- Reaction on false/indeterminate varies depending on the equation's type (function/simplification), |
Comment on lines
+420
to
+485
| checkRequires :: | ||
| Substitution -> RewriteRuleAppT (RewriteT io) () | ||
| checkRequires matchingSubst = do | ||
| ModifiersRep (_ :: FromModifiersT mods => Proxy mods) <- getPrettyModifiers | ||
| -- apply substitution to rule requires | ||
| let ruleRequires = | ||
| concatMap (splitBoolPredicates . coerce . substituteInTerm matchingSubst . coerce) rule.requires | ||
|
|
||
| -- filter out any predicates known to be _syntactically_ present in the known prior | ||
| toCheck <- lift $ filterOutKnownConstraints pat.constraints ruleRequires | ||
|
|
||
| -- simplify the constraints (one by one in isolation). Stop if false, abort rewrite if indeterminate. | ||
| unclearRequires <- | ||
| catMaybes <$> mapM (checkConstraint id notAppliedIfBottom pat.constraints) toCheck | ||
|
|
||
| -- unclear conditions may have been simplified and | ||
| -- could now be syntactically present in the path constraints, filter again | ||
| stillUnclear <- lift $ filterOutKnownConstraints pat.constraints unclearRequires | ||
|
|
||
| -- check unclear requires-clauses in the context of known constraints (priorKnowledge) | ||
| solver <- lift $ RewriteT $ (.smtSolver) <$> ask | ||
| let smtUnclear = do | ||
| withContext CtxConstraint . withContext CtxAbort . logMessage $ | ||
| WithJsonMessage (object ["conditions" .= (externaliseTerm . coerce <$> stillUnclear)]) $ | ||
| renderOneLineText $ | ||
| "Uncertain about condition(s) in a rule:" | ||
| <+> (hsep . punctuate comma . map (pretty' @mods) $ stillUnclear) | ||
| failRewrite $ | ||
| RuleConditionUnclear rule . coerce . foldl1 AndTerm $ | ||
| map coerce stillUnclear | ||
| SMT.checkPredicates solver pat.constraints mempty (Set.fromList stillUnclear) >>= \case | ||
| SMT.IsUnknown{} -> | ||
| smtUnclear -- abort rewrite if a solver result was Unknown | ||
| SMT.IsInvalid -> do | ||
| -- requires is actually false given the prior | ||
| withContext CtxFailure $ logMessage ("Required clauses evaluated to #Bottom." :: Text) | ||
| RewriteRuleAppT $ pure NotApplied | ||
| SMT.IsValid -> | ||
| pure () -- can proceed | ||
| checkEnsures :: | ||
| Substitution -> RewriteRuleAppT (RewriteT io) [Predicate] | ||
| checkEnsures matchingSubst = do | ||
| -- apply substitution to rule requires | ||
| let ruleEnsures = | ||
| concatMap (splitBoolPredicates . coerce . substituteInTerm matchingSubst . coerce) $ | ||
| Set.toList rule.ensures | ||
| newConstraints <- | ||
| catMaybes <$> mapM (checkConstraint id trivialIfBottom pat.constraints) ruleEnsures | ||
|
|
||
| -- check all new constraints together with the known side constraints | ||
| solver <- lift $ RewriteT $ (.smtSolver) <$> ask | ||
| (lift $ SMT.checkPredicates solver pat.constraints mempty (Set.fromList newConstraints)) >>= \case | ||
| SMT.IsInvalid -> do | ||
| withContext CtxSuccess $ logMessage ("New constraints evaluated to #Bottom." :: Text) | ||
| RewriteRuleAppT $ pure Trivial | ||
| _other -> | ||
| pure () | ||
|
|
||
| -- if a new constraint is going to be added, the equation cache is invalid | ||
| unless (null newConstraints) $ do | ||
| withContextFor Equations . logMessage $ | ||
| ("New path condition ensured, invalidating cache" :: Text) | ||
|
|
||
| lift . RewriteT . lift . modify $ \s -> s{equations = mempty} | ||
| pure newConstraints | ||
|
|
There was a problem hiding this comment.
can this be subsumed by the ApplyEquations version?
There was a problem hiding this comment.
We may find the common denominator, but I'm reluctant to do it as #4022 will change checkRequires in ApplyEquations significantly, and I do not think we want to allow rewrite rules with syntactic requires clauses.
goodlyrottenapple
approved these changes
Aug 15, 2024
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Refactor
applyRuleandapplyEquationto checkrequires/ensuresin separate functions.This will make reviewing #4022 easier.