Skip to content

Commit 024e5fd

Browse files
geo2ageo2a
committed
Build existential substitution together with the matching one
1 parent 053ed88 commit 024e5fd

File tree

1 file changed

+67
-40
lines changed

1 file changed

+67
-40
lines changed

‎booster/library/Booster/Pattern/Rewrite.hs

Lines changed: 67 additions & 40 deletions
Original file line numberDiff line numberDiff line change
@@ -304,23 +304,38 @@ applyRule pat@Pattern{ceilConditions} rule =
304304
NE.toList remainder
305305
)
306306
failRewrite $ RuleApplicationUnclear rule pat.term remainder
307-
MatchSuccess substitution -> do
307+
MatchSuccess matchingSubstitution -> do
308+
-- existential variables may be present in rule.rhs and rule.ensures,
309+
-- need to strip prefixes and freshen their names with respect to variables already
310+
-- present in the input pattern and in the unification substitution
311+
varsFromInput <- lift . RewriteT $ asks (.varsToAvoid)
312+
let varsFromPattern = freeVariables pat.term <> (Set.unions $ Set.map (freeVariables . coerce) pat.constraints)
313+
varsFromSubst = Set.unions . map freeVariables . Map.elems $ matchingSubstitution
314+
forbiddenVars = varsFromInput <> varsFromPattern <> varsFromSubst
315+
existentialSubst =
316+
Map.fromSet
317+
(\v -> Var $ freshenVar v{variableName = stripMarker v.variableName} forbiddenVars)
318+
rule.existentials
319+
combinedSubstitution = matchingSubstitution <> existentialSubst
320+
308321
withContext CtxSuccess $ do
309322
logMessage rule
310323
withContext CtxSubstitution
311324
$ logMessage
312325
$ WithJsonMessage
313326
( object
314-
["substitution" .= (bimap (externaliseTerm . Var) externaliseTerm <$> Map.toList substitution)]
327+
[ "substitution"
328+
.= (bimap (externaliseTerm . Var) externaliseTerm <$> Map.toList combinedSubstitution)
329+
]
315330
)
316331
$ renderOneLineText
317332
$ "Substitution:"
318333
<+> ( hsep $
319334
intersperse "," $
320335
map (\(k, v) -> pretty' @mods k <+> "->" <+> pretty' @mods v) $
321-
Map.toList substitution
336+
Map.toList combinedSubstitution
322337
)
323-
pure substitution
338+
pure combinedSubstitution
324339

325340
-- Also fail the whole rewrite if a rule applies but may introduce
326341
-- an undefined term.
@@ -349,37 +364,29 @@ applyRule pat@Pattern{ceilConditions} rule =
349364
("New path condition ensured, invalidating cache" :: Text)
350365
lift . RewriteT . lift . modify $ \s -> s{equations = mempty}
351366

367+
-- partition ensured constrains into substitution and predicates
352368
let (newSubsitution, newConstraints) = partitionPredicates ensuredConditions
353369

354-
-- existential variables may be present in rule.rhs and rule.ensures,
355-
-- need to strip prefixes and freshen their names with respect to variables already
356-
-- present in the input pattern and in the unification substitution
357-
varsFromInput <- lift . RewriteT $ asks (.varsToAvoid)
358-
let varsFromPattern = freeVariables pat.term <> (Set.unions $ Set.map (freeVariables . coerce) pat.constraints)
359-
varsFromSubst = Set.unions . map freeVariables . Map.elems $ subst
360-
forbiddenVars = varsFromInput <> varsFromPattern <> varsFromSubst
361-
existentialSubst =
362-
Map.fromSet
363-
(\v -> Var $ freshenVar v{variableName = stripMarker v.variableName} forbiddenVars)
364-
rule.existentials
365-
370+
-- merge existing substitution and newly acquired one, applying the latter to the former
366371
normalisedPatternSubst <-
367-
lift $ normaliseSubstitution pat.constraints pat.substitution newSubsitution
368-
369-
-- modify the substitution to include the existentials
370-
let substWithExistentials = subst <> existentialSubst
371-
372+
lift $
373+
normaliseSubstitution
374+
pat.constraints
375+
pat.substitution
376+
newSubsitution
377+
-- NOTE it is necessary to first apply the rule substitution and then the pattern/ensures substitution, but it is suboptimal to traverse the term twice.
378+
-- TODO a substitution composition operator
379+
let rewrittenTerm = substituteInTerm normalisedPatternSubst . substituteInTerm subst $ rule.rhs
380+
substitutedNewConstraints =
381+
Set.fromList $
382+
map
383+
(coerce . substituteInTerm normalisedPatternSubst . substituteInTerm subst . coerce)
384+
newConstraints
372385
let rewritten =
373386
Pattern
374-
(substituteInTerm normalisedPatternSubst . substituteInTerm substWithExistentials $ rule.rhs)
387+
rewrittenTerm
375388
-- adding new constraints that have not been trivially `Top`, substituting the Ex# variables
376-
( pat.constraints
377-
<> ( Set.fromList $
378-
map
379-
(coerce . substituteInTerm normalisedPatternSubst . substituteInTerm substWithExistentials . coerce)
380-
newConstraints
381-
)
382-
)
389+
(pat.constraints <> substitutedNewConstraints)
383390
normalisedPatternSubst
384391
ceilConditions
385392
withContext CtxSuccess $
@@ -396,7 +403,7 @@ applyRule pat@Pattern{ceilConditions} rule =
396403
-- - apply the new substitution to the old substitution
397404
-- - simplify the substituted old substitution, assuming known truth
398405
-- - TODO check for loops?
399-
-- - filter out possible trivial items
406+
-- - TODO filter out possible trivial items?
400407
-- - finally, merge with the new substitution items and return
401408
normaliseSubstitution ::
402409
Set.Set Predicate -> Substitution -> Substitution -> RewriteT io Substitution
@@ -470,23 +477,36 @@ applyRule pat@Pattern{ceilConditions} rule =
470477
concatMap (splitBoolPredicates . coerce . substituteInTerm matchingSubst . coerce) rule.requires
471478

472479
-- filter out any predicates known to be _syntactically_ present in the known prior
473-
toCheck <- lift $ filterOutKnownConstraints pat.constraints ruleRequires
480+
toCheck <-
481+
lift $
482+
filterOutKnownConstraints
483+
(pat.constraints <> (Set.fromList . asEquations $ pat.substitution))
484+
ruleRequires
474485

475486
-- simplify the constraints (one by one in isolation). Stop if false, abort rewrite if indeterminate.
476487
unclearRequires <-
477-
catMaybes <$> mapM (checkConstraint id notAppliedIfBottom pat.constraints) toCheck
488+
catMaybes
489+
<$> mapM
490+
( checkConstraint
491+
id
492+
notAppliedIfBottom
493+
(pat.constraints <> (Set.fromList . asEquations $ pat.substitution))
494+
)
495+
toCheck
478496

479497
-- unclear conditions may have been simplified and
480498
-- could now be syntactically present in the path constraints, filter again
481-
stillUnclear <- lift $ filterOutKnownConstraints pat.constraints unclearRequires
499+
stillUnclear <-
500+
lift $
501+
filterOutKnownConstraints
502+
(pat.constraints <> (Set.fromList . asEquations $ pat.substitution))
503+
unclearRequires
482504

483505
-- check unclear requires-clauses in the context of known constraints (priorKnowledge)
484506
solver <- lift $ RewriteT $ (.smtSolver) <$> ask
485-
SMT.checkPredicates solver pat.constraints mempty (Set.fromList stillUnclear) >>= \case
486-
SMT.IsUnknown reason -> do
487-
-- abort rewrite if a solver result was Unknown
488-
withContext CtxAbort $ logMessage reason
489-
smtUnclear stillUnclear
507+
SMT.checkPredicates solver pat.constraints pat.substitution (Set.fromList stillUnclear) >>= \case
508+
SMT.IsUnknown{} ->
509+
smtUnclear stillUnclear -- abort rewrite if a solver result was Unknown
490510
SMT.IsInvalid -> do
491511
-- requires is actually false given the prior
492512
withContext CtxFailure $ logMessage ("Required clauses evaluated to #Bottom." :: Text)
@@ -500,13 +520,20 @@ applyRule pat@Pattern{ceilConditions} rule =
500520
let ruleEnsures =
501521
concatMap (splitBoolPredicates . coerce . substituteInTerm matchingSubst . coerce) rule.ensures
502522
newConstraints <-
503-
catMaybes <$> mapM (checkConstraint id trivialIfBottom pat.constraints) ruleEnsures
523+
catMaybes
524+
<$> mapM
525+
( checkConstraint
526+
id
527+
trivialIfBottom
528+
(pat.constraints <> (Set.fromList . asEquations $ pat.substitution))
529+
)
530+
ruleEnsures
504531

505532
-- check all new constraints together with the known side constraints
506533
solver <- lift $ RewriteT $ (.smtSolver) <$> ask
507534
-- TODO it is probably enough to establish satisfiablity (rather than validity) of the ensured conditions.
508535
-- For now, we check validity to be safe and admit indeterminate result (i.e. (P, not P) is (Sat, Sat)).
509-
(lift $ SMT.checkPredicates solver pat.constraints mempty (Set.fromList newConstraints)) >>= \case
536+
(lift $ SMT.checkPredicates solver pat.constraints pat.substitution (Set.fromList newConstraints)) >>= \case
510537
SMT.IsInvalid -> do
511538
withContext CtxSuccess $ logMessage ("New constraints evaluated to #Bottom." :: Text)
512539
RewriteRuleAppT $ pure Trivial

0 commit comments

Comments
 (0)