thinkapart_20160120.hs

#!/usr/bin/env stack
-- stack --install-ghc runghc --package sbv

import Data.SBV

main =
  print =<<
    (sat $
      \lo m2 m1 hi ->
        ((lo :: SInt8) + m2 + m1 + hi .== 31)
        &&& (lo `sMod` 2 + m2 `sMod` 2 + m1 `sMod` 2 + hi `sMod` 2 .== 1)
        &&& allDifferent [lo, m2, m1, hi]
        &&& lo .< m2
        &&& m2 .< m1
        &&& m1 .< hi
        &&& (hi - lo .== 7)
        &&& (m1 - m2 .== 2))