diff --git a/src/Data/CDCL.hs b/src/Data/CDCL.hs index 1f09d94..31050ad 100644 --- a/src/Data/CDCL.hs +++ b/src/Data/CDCL.hs @@ -116,8 +116,8 @@ implies (Group group) candidate = any (`subsumes` candidate) group -- __subset__ of the switches in @y@. In other words, the @x@ 'Rule' will match -- /everything/ that @y@ will. subsumes :: Rule -> Rule -> Bool -subsumes (Rule these) (Rule those) = HashMap.foldrWithKey check True these - where check key value acc = HashMap.lookup key those == Just value && acc +subsumes (Rule x) (Rule y) = HashMap.foldrWithKey check True x + where check key v acc = HashMap.lookup key y == Just v && acc -- | Add a new 'Rule' to a 'Group'. Attempt to calculate any 'refinements' of -- the rule, and generalise the 'Group' as far as possible. @@ -126,11 +126,17 @@ resolve rule group | group `implies` rule = group resolve rule@(Rule config) group@(Group rules) = case refinements rule group of [] -> Group case HashMap.toList config of - [ (key, value) ] -> do -- Unit propagation + [ (key, x) ] -> do -- Unit propagation HashSet.insert rule $ rules & HashSet.map \(Rule current) -> do - if HashMap.lookup key current /= Just value - then Rule (HashMap.delete key current) - else rule + Rule $ case HashMap.lookup key current of + -- The unit does not appear in the current rule : keep the current rule. + Nothing -> current + -- The unit subsumes the current rule : delete the current rule. + Just y | y == x -> config + -- If the unit matches, the current rule is useless for that group to match. + -- Otherwise the unit does not match, but then the current rule + -- does not need to recheck that : delete the unit from the current rule. + | otherwise {- y == not x -} -> HashMap.delete key current _ -> rules & HashSet.filter (not . (rule `subsumes`)) & HashSet.insert rule