Exemplo de uso do SBV (SMT Solver) para resolver desafio de lógica

desafio2.hs

#!/usr/bin/env stack
{-
  stack --resolver lts-17.4 script
    --package sbv
-}
{-# LANGUAGE DeriveAnyClass     #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE FlexibleInstances  #-}
{-# LANGUAGE NamedFieldPuns     #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TemplateHaskell    #-}
{-# OPTIONS_GHC -Wall -Werror   #-}

{-|
  A estrutura deste módulo foi "fortemente inspirada" por
  [este exemplo do SBV](https://hackage.haskell.org/package/sbv-8.10/docs/Documentation-SBV-Examples-Puzzles-Murder.html).

  O desafio em si foi tirado [deste site](https://www.geniol.com.br/logica/desafios/casais-de-ferias/).
-}
module Desafio2 where

import Data.Foldable (traverse_)
import Data.Functor.Identity (Identity(..))
import Data.List (transpose)
import Data.SBV
import Data.SBV.Control


data Hotel = California
           | FlorestaNativa
           | PonteGrande
           | VolteSempre

data Diferencial = ArCondicionado
                 | BelaVista
                 | Janta
                 | VagaGaragem

mkSymbolicEnumeration ''Hotel
mkSymbolicEnumeration ''Diferencial

-- | Parametrizado sobre um funtor para permitir usar este tipo nos
-- contextos simbólico e concreto.
data Casal f = MkCasal { nome :: String
                       , hotel :: f Hotel
                       , diferencial :: f Diferencial
                       , diaria :: f Word16
                       }

instance Show (Casal Identity) where
  show MkCasal{nome, hotel, diferencial, diaria} =
    unwords [ nome
            , show (runIdentity hotel)
            , show (runIdentity diferencial)
            , show (runIdentity diaria)
            ]

newCasal :: String -> Symbolic (Casal SBV)
newCasal n = do
  a <- MkCasal n <$> free_ <*> free_ <*> free_
  constrain $ diaria a `sElem` [100, 200, 300, 400]
  pure a

getCasal :: Casal SBV -> Query (Casal Identity)
getCasal MkCasal{nome, hotel, diferencial, diaria} =
  MkCasal nome <$> (Identity <$> getValue hotel)
               <*> (Identity <$> getValue diferencial)
               <*> (Identity <$> getValue diaria)

puzzle :: IO [Casal Identity]
puzzle = runSMT $ do
  giseleRafael <- newCasal "Gisele e Rafael"
  jenyVitor <- newCasal "Jeny e Vitor"
  julianaLuis <- newCasal "Juliana e Luís"
  luciaEder <- newCasal "Lúcia e Éder"

  let casais = [ giseleRafael
               , jenyVitor
               , julianaLuis
               , luciaEder
               ]
      -- some f = sOr (map f casais)
      every f = sAnd (map f casais)
      ofHotel f a = hotel a .== literal f
      ofDiferencial o a = diferencial a .== literal o

  constrain $ sAnd
    [ distinct (map hotel casais)
    , distinct (map diferencial casais)
    , distinct (map diaria casais)
    ]

  -- dica 1. O casal que ficou no hotel com vaga na garagem pagou R$
  -- 100 a mais na diária do que o casal Juliana e Luis.
  constrain . every $ \g -> ofDiferencial VagaGaragem g .=>
    diaria g .== diaria julianaLuis + 100

  -- dica 2. O casal que se hospedou no hotel Volte Sempre pagou uma
  -- diária mais cara do que o casal Jeny e Victor.
  constrain . every $ \vs -> ofHotel VolteSempre vs .=>
    diaria vs .> diaria jenyVitor

  -- dica 3. O hotel California não tem a diária mais barata.
  constrain . every $ \c -> ofHotel California c .=>
    every (\o -> literal (nome o /= nome c) .=> diaria o .< diaria c)

  -- dica 4. A diária do hotel Floresta Nativa é mais cara do que a
  -- diária do hotel Volte Sempre.
  constrain . every $ \fn -> ofHotel FlorestaNativa fn .=>
    every (\vs -> ofHotel VolteSempre vs .=>
      diaria fn .> diaria vs)

  -- dica 5. O hotel que tem ar condicionado é o Floresta Nativa ou
  -- o hotel com a diária de R$ 100.
  constrain . every $ \ac -> ofDiferencial ArCondicionado ac .=>
    sOr [ hotel ac .== literal FlorestaNativa
        , diaria ac .== 100
        ]

  -- dica 6. Sobre o casal Lucia e Eder e o casal que se hospedou no
  -- hotel Floresta Nativa, um ficou no quarto com bela vista e o
  -- outro pagou R$ 200 de diária, não necessariamente nessa ordem.
  constrain $ hotel luciaEder ./= literal FlorestaNativa
  constrain . every $ \fn -> ofHotel FlorestaNativa fn .=>
    sOr [ diferencial fn .== literal BelaVista
        , diaria fn .== 200
        ]
  constrain $
    sOr [ diferencial luciaEder .== literal BelaVista
        , diaria luciaEder .== 200
        ]

  query $ do
    cs <- checkSat
    case cs of
      Sat ->
        traverse getCasal casais
      _ ->
        pure []

resolver :: IO ()
resolver = do
  casais <- puzzle
  let toRow MkCasal{nome, hotel, diferencial, diaria} =
        nome : [ show . runIdentity $ hotel
               , show . runIdentity $ diferencial
               , show . runIdentity $ diaria
               ]
      rows = map toRow casais
      widths = map ((+ 2) . maximum . map length) (transpose rows)
      align = concat . zipWith (\i x -> take i (' ' : x ++ repeat ' ')) widths
  traverse_ (putStrLn . align) rows