From 36419fa92f087b976990388063f92cf10b4e1f30 Mon Sep 17 00:00:00 2001 From: Georgy Lukyanov Date: Fri, 25 Oct 2024 15:04:37 +0200 Subject: [PATCH] Tweak comments --- booster/library/Booster/Pattern/Rewrite.hs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/booster/library/Booster/Pattern/Rewrite.hs b/booster/library/Booster/Pattern/Rewrite.hs index ae439054dd..f58fb5b9e4 100644 --- a/booster/library/Booster/Pattern/Rewrite.hs +++ b/booster/library/Booster/Pattern/Rewrite.hs @@ -227,13 +227,13 @@ rewriteStep cutLabels terminalLabels pat = do pure $ mkBranch pat ruleApplicationData satRes@(SMT.IsSat{}) -> do -- the remainder condition is satisfiable. - -- TODO construct the remainder branch and consider it. -- To construct the "remainder pattern", -- we add the remainder condition to the predicates of pat + -- TODO: construct the remainder branch and consider it. throwRemainder (map fst ruleApplicationData) satRes groupRemainderPredicate satRes@SMT.IsUnknown{} -> do -- solver cannot solve the remainder - -- TODO descend into the remainder branch anyway + -- TODO: descend into the remainder branch anyway, same as in the satisfiable case throwRemainder (map fst ruleApplicationData) satRes groupRemainderPredicate labelOf = fromMaybe "" . (.ruleLabel) . (.attributes)