Skip to content

Commit

Permalink
Build existential substitution together with the matching one
Browse files Browse the repository at this point in the history
  • Loading branch information
@geo2a
geo2a committed Oct 16, 2024
1 parent abf0354 commit 9ffac4a
Showing 1 changed file with 65 additions and 36 deletions.
101 changes: 65 additions & 36 deletions booster/library/Booster/Pattern/Rewrite.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -304,23 +304,38 @@ applyRule pat@Pattern{ceilConditions} rule =
NE.toList remainder
)
failRewrite $ RuleApplicationUnclear rule pat.term remainder
MatchSuccess substitution -> do
MatchSuccess matchingSubstitution -> do
-- existential variables may be present in rule.rhs and rule.ensures,
-- need to strip prefixes and freshen their names with respect to variables already
-- present in the input pattern and in the unification substitution
varsFromInput <- lift . RewriteT $ asks (.varsToAvoid)
let varsFromPattern = freeVariables pat.term <> (Set.unions $ Set.map (freeVariables . coerce) pat.constraints)
varsFromSubst = Set.unions . map freeVariables . Map.elems $ matchingSubstitution
forbiddenVars = varsFromInput <> varsFromPattern <> varsFromSubst
existentialSubst =
Map.fromSet
(\v -> Var $ freshenVar v{variableName = stripMarker v.variableName} forbiddenVars)
rule.existentials
combinedSubstitution = matchingSubstitution <> existentialSubst

withContext CtxSuccess $ do
logMessage rule
withContext CtxSubstitution
$ logMessage
$ WithJsonMessage
( object
["substitution" .= (bimap (externaliseTerm . Var) externaliseTerm <$> Map.toList substitution)]
[ "substitution"
.= (bimap (externaliseTerm . Var) externaliseTerm <$> Map.toList combinedSubstitution)
]
)
$ renderOneLineText
$ "Substitution:"
<+> ( hsep $
intersperse "," $
map (\(k, v) -> pretty' @mods k <+> "->" <+> pretty' @mods v) $
Map.toList substitution
Map.toList combinedSubstitution
)
pure substitution
pure combinedSubstitution

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

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

-- existential variables may be present in rule.rhs and rule.ensures,
-- need to strip prefixes and freshen their names with respect to variables already
-- present in the input pattern and in the unification substitution
varsFromInput <- lift . RewriteT $ asks (.varsToAvoid)
let varsFromPattern = freeVariables pat.term <> (Set.unions $ Set.map (freeVariables . coerce) pat.constraints)
varsFromSubst = Set.unions . map freeVariables . Map.elems $ subst
forbiddenVars = varsFromInput <> varsFromPattern <> varsFromSubst
existentialSubst =
Map.fromSet
(\v -> Var $ freshenVar v{variableName = stripMarker v.variableName} forbiddenVars)
rule.existentials

-- merge existing substitution and newly acquired one, applying the latter to the former
normalisedPatternSubst <-
lift $ normaliseSubstitution pat.constraints pat.substitution newSubsitution

-- modify the substitution to include the existentials
let substWithExistentials = subst <> existentialSubst

lift $
normaliseSubstitution
pat.constraints
pat.substitution
newSubsitution
-- 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.
-- TODO a substitution composition operator
let rewrittenTerm = substituteInTerm normalisedPatternSubst . substituteInTerm subst $ rule.rhs
substitutedNewConstraints =
Set.fromList $
map
(coerce . substituteInTerm normalisedPatternSubst . substituteInTerm subst . coerce)
newConstraints
let rewritten =
Pattern
(substituteInTerm normalisedPatternSubst . substituteInTerm substWithExistentials $ rule.rhs)
rewrittenTerm
-- adding new constraints that have not been trivially `Top`, substituting the Ex# variables
( pat.constraints
<> ( Set.fromList $
map
(coerce . substituteInTerm normalisedPatternSubst . substituteInTerm substWithExistentials . coerce)
newConstraints
)
)
(pat.constraints <> substitutedNewConstraints)
normalisedPatternSubst
ceilConditions
withContext CtxSuccess $
Expand All @@ -396,7 +403,7 @@ applyRule pat@Pattern{ceilConditions} rule =
-- - apply the new substitution to the old substitution
-- - simplify the substituted old substitution, assuming known truth
-- - TODO check for loops?
-- - filter out possible trivial items
-- - TODO filter out possible trivial items?
-- - finally, merge with the new substitution items and return
normaliseSubstitution ::
Set.Set Predicate -> Substitution -> Substitution -> RewriteT io Substitution
Expand Down Expand Up @@ -470,15 +477,30 @@ applyRule pat@Pattern{ceilConditions} rule =
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
toCheck <-
lift $
filterOutKnownConstraints
(pat.constraints <> (Set.fromList . asEquations $ pat.substitution))
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
catMaybes
<$> mapM
( checkConstraint
id
notAppliedIfBottom
(pat.constraints <> (Set.fromList . asEquations $ pat.substitution))
)
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
stillUnclear <-
lift $
filterOutKnownConstraints
(pat.constraints <> (Set.fromList . asEquations $ pat.substitution))
unclearRequires

-- check unclear requires-clauses in the context of known constraints (priorKnowledge)
solver <- lift $ RewriteT $ (.smtSolver) <$> ask
Expand All @@ -491,7 +513,7 @@ applyRule pat@Pattern{ceilConditions} rule =
failRewrite $
RuleConditionUnclear rule . coerce . foldl1 AndTerm $
map coerce stillUnclear
SMT.checkPredicates solver pat.constraints mempty (Set.fromList stillUnclear) >>= \case
SMT.checkPredicates solver pat.constraints pat.substitution (Set.fromList stillUnclear) >>= \case
SMT.IsUnknown{} ->
smtUnclear -- abort rewrite if a solver result was Unknown
SMT.IsInvalid -> do
Expand All @@ -507,11 +529,18 @@ applyRule pat@Pattern{ceilConditions} rule =
let ruleEnsures =
concatMap (splitBoolPredicates . coerce . substituteInTerm matchingSubst . coerce) rule.ensures
newConstraints <-
catMaybes <$> mapM (checkConstraint id trivialIfBottom pat.constraints) ruleEnsures
catMaybes
<$> mapM
( checkConstraint
id
trivialIfBottom
(pat.constraints <> (Set.fromList . asEquations $ pat.substitution))
)
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
(lift $ SMT.checkPredicates solver pat.constraints pat.substitution (Set.fromList newConstraints)) >>= \case
SMT.IsInvalid -> do
withContext CtxSuccess $ logMessage ("New constraints evaluated to #Bottom." :: Text)
RewriteRuleAppT $ pure Trivial
Expand Down

0 comments on commit 9ffac4a

Please sign in to comment.