fix resolve

Author: Julien Moutinho

holmes.cabal

@@ -38,15 +38,15 @@ library
                , Data.JoinSemilattice.Class.Zipping
                , Data.CDCL
 
-  build-depends: base >= 4.12 && < 4.16
-               , containers >= 0.6 && < 0.7
-               , hashable >= 1.3 && < 1.4
-               , hedgehog >= 1.0 && < 1.1
-               , logict >= 0.7 && < 0.8
-               , mtl >= 2.2 && < 2.3
-               , primitive >= 0.7 && < 0.8
-               , transformers >= 0.5 && < 0.6
-               , unordered-containers >= 0.2 && < 0.3
+  build-depends: base >= 4.12
+               , containers >= 0.6
+               , hashable >= 1.3
+               , hedgehog >= 1.0
+               , logict >= 0.7
+               , mtl >= 2.2
+               , primitive >= 0.7
+               , transformers >= 0.5
+               , unordered-containers >= 0.2
 
   ghc-options: -Wall -Wextra
   hs-source-dirs: src
@@ -60,23 +60,24 @@ test-suite examples
   main-is:  Main.hs
 
   build-depends: base
-               , hashable >= 1.3 && < 1.4
+               , hashable >= 1.3
                , holmes
-               , hspec >= 2.7 && < 2.9
-               , split >= 0.2 && < 0.3
-               , unordered-containers >= 0.2 && < 0.3
-               , relude >= 0.6 && < 1.1
-               , tasty >= 1.2 && < 1.5
+               , hspec >= 2.7
+               , split >= 0.2
+               , unordered-containers >= 0.2
+               , relude >= 0.6
+               , tasty >= 1.2
                , tasty-discover
                , tasty-hspec
 
-  other-modules: Futoshiki
+  other-modules:
+               Futoshiki
                , Issue14
                , WaveFunctionCollapse
 
   ghc-options: -Wall -Wextra -threaded
   hs-source-dirs: examples
-  build-tool-depends: tasty-discover:tasty-discover
+--  build-tool-depends: tasty-discover:tasty-discover
   default-language: Haskell2010
 
 --------------------------------------------------
@@ -87,13 +88,13 @@ test-suite test
   main-is:  Main.hs
 
   build-depends: base
-               , containers >= 0.6 && < 0.7
-               , hashable >= 1.3 && < 1.4
-               , hedgehog >= 1.0 && < 1.1
+               , containers >= 0.6
+               , hashable >= 1.3
+               , hedgehog >= 1.0
                , holmes
-               , primitive >= 0.7 && < 0.8
-               , transformers >= 0.5 && < 0.6
-               , tasty >= 1.2 && < 1.5
+               , primitive >= 0.7
+               , transformers >= 0.5
+               , tasty >= 1.2
                , tasty-discover
                , tasty-hedgehog
                , tasty-hspec
@@ -115,20 +116,20 @@ test-suite test
 
   ghc-options: -Wall -Wextra -threaded
   hs-source-dirs: test
-  build-tool-depends: markdown-unlit:markdown-unlit
-                    , tasty-discover:tasty-discover
+--  build-tool-depends: markdown-unlit:markdown-unlit
+--                    , tasty-discover:tasty-discover
   default-language: Haskell2010
 
 --------------------------------------------------
 -- LITERATE HASKELL README / HSPEC RUNNER
 
-test-suite readme
-  build-depends: base
-               , hashable >= 1.3 && < 1.4
-               , holmes
-               , hspec >= 2.7 && < 2.9
-  main-is:             README.lhs
-  type:                exitcode-stdio-1.0
-  default-language:    Haskell2010
-  ghc-options:         -pgmL markdown-unlit -Wall
-  build-tool-depends:  markdown-unlit:markdown-unlit
+--test-suite readme
+--  build-depends: base
+--               , hashable >= 1.3
+--               , holmes
+--               , hspec >= 2.7
+--  main-is:             README.lhs
+--  type:                exitcode-stdio-1.0
+--  default-language:    Haskell2010
+--  ghc-options:         -pgmL markdown-unlit -Wall
+--  build-tool-depends:  markdown-unlit:markdown-unlit

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