File tree 1 file changed +2
-2
lines changed
booster/library/Booster/Pattern
1 file changed +2
-2
lines changed Original file line number Diff line number Diff line change @@ -227,13 +227,13 @@ rewriteStep cutLabels terminalLabels pat = do
227
227
pure $ mkBranch pat ruleApplicationData
228
228
satRes@ (SMT. IsSat {}) -> do
229
229
-- the remainder condition is satisfiable.
230
- -- TODO construct the remainder branch and consider it.
231
230
-- To construct the "remainder pattern",
232
231
-- we add the remainder condition to the predicates of pat
232
+ -- TODO: construct the remainder branch and consider it.
233
233
throwRemainder (map fst ruleApplicationData) satRes groupRemainderPredicate
234
234
satRes@ SMT. IsUnknown {} -> do
235
235
-- solver cannot solve the remainder
236
- -- TODO descend into the remainder branch anyway
236
+ -- TODO: descend into the remainder branch anyway, same as in the satisfiable case
237
237
throwRemainder (map fst ruleApplicationData) satRes groupRemainderPredicate
238
238
239
239
labelOf = fromMaybe " " . (. ruleLabel) . (. attributes)
You can’t perform that action at this time.
0 commit comments