    -----------------------------------------------------------------------------
    -- |
    -- Module    : Documentation.SBV.Examples.Puzzles.Orangutans
    -- Copyright : (c) Levent Erkok
    -- License   : BSD3
    -- Maintainer: erkokl@gmail.com
    -- Stability : experimental
    --
    -- Based on <http://github.com/goldfirere/video-resources/blob/main/2022-08-12-java/Haskell.hs>
    -----------------------------------------------------------------------------

    {-# LANGUAGE DeriveAnyClass      #-}
    {-# LANGUAGE DeriveDataTypeable  #-}
    {-# LANGUAGE DeriveGeneric       #-}
    {-# LANGUAGE FlexibleContexts    #-}
    {-# LANGUAGE TemplateHaskell     #-}
    {-# LANGUAGE StandaloneDeriving  #-}
    {-# LANGUAGE OverloadedRecordDot #-}

    {-# OPTIONS_GHC -Wall -Werror #-}

    module Documentation.SBV.Examples.Puzzles.Orangutans where

    import Data.SBV
    import GHC.Generics (Generic)

    -- $setup
    -- >>> -- For doctest purposes only:
    -- >>> import Data.SBV

    -- | Orangutans in the puzzle.
    data Orangutan = Merah   | Ofallo  | Quirrel  | Shamir   deriving (Int -> Orangutan
    Orangutan -> Int
    Orangutan -> [Orangutan]
    Orangutan -> Orangutan
    Orangutan -> Orangutan -> [Orangutan]
    Orangutan -> Orangutan -> Orangutan -> [Orangutan]
    (Orangutan -> Orangutan)
    -> (Orangutan -> Orangutan)
    -> (Int -> Orangutan)
    -> (Orangutan -> Int)
    -> (Orangutan -> [Orangutan])
    -> (Orangutan -> Orangutan -> [Orangutan])
    -> (Orangutan -> Orangutan -> [Orangutan])
    -> (Orangutan -> Orangutan -> Orangutan -> [Orangutan])
    -> Enum Orangutan
    forall a.
    (a -> a)
    -> (a -> a)
    -> (Int -> a)
    -> (a -> Int)
    -> (a -> [a])
    -> (a -> a -> [a])
    -> (a -> a -> [a])
    -> (a -> a -> a -> [a])
    -> Enum a
    $csucc :: Orangutan -> Orangutan
    succ :: Orangutan -> Orangutan
    $cpred :: Orangutan -> Orangutan
    pred :: Orangutan -> Orangutan
    $ctoEnum :: Int -> Orangutan
    toEnum :: Int -> Orangutan
    $cfromEnum :: Orangutan -> Int
    fromEnum :: Orangutan -> Int
    $cenumFrom :: Orangutan -> [Orangutan]
    enumFrom :: Orangutan -> [Orangutan]
    $cenumFromThen :: Orangutan -> Orangutan -> [Orangutan]
    enumFromThen :: Orangutan -> Orangutan -> [Orangutan]
    $cenumFromTo :: Orangutan -> Orangutan -> [Orangutan]
    enumFromTo :: Orangutan -> Orangutan -> [Orangutan]
    $cenumFromThenTo :: Orangutan -> Orangutan -> Orangutan -> [Orangutan]
    enumFromThenTo :: Orangutan -> Orangutan -> Orangutan -> [Orangutan]
    Enum, Orangutan
    Orangutan -> Orangutan -> Bounded Orangutan
    forall a. a -> a -> Bounded a
    $cminBound :: Orangutan
    minBound :: Orangutan
    $cmaxBound :: Orangutan
    maxBound :: Orangutan
    Bounded)

    -- | Handlers for each orangutan.
    data Handler   = Dolly   | Eva     | Francine | Gracie

    -- | Location for each orangutan.
    data Location  = Ambalat | Basahan | Kendisi  | Tarakan

    mkSymbolicEnumeration ''Orangutan
    mkSymbolicEnumeration ''Handler
    mkSymbolicEnumeration ''Location

    -- | An assignment is solution to the puzzle
    data Assignment = MkAssignment { Assignment -> SBV Orangutan
    orangutan :: SOrangutan
                                   , Assignment -> SHandler
    handler   :: SHandler
                                   , Assignment -> SLocation
    location  :: SLocation
                                   , Assignment -> SInteger
    age       :: SInteger
                                   }
                                   deriving ((forall x. Assignment -> Rep Assignment x)
    -> (forall x. Rep Assignment x -> Assignment) -> Generic Assignment
    forall x. Rep Assignment x -> Assignment
    forall x. Assignment -> Rep Assignment x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    $cfrom :: forall x. Assignment -> Rep Assignment x
    from :: forall x. Assignment -> Rep Assignment x
    $cto :: forall x. Rep Assignment x -> Assignment
    to :: forall x. Rep Assignment x -> Assignment
    Generic, Bool -> SBool -> Assignment -> Assignment -> Assignment
    (Bool -> SBool -> Assignment -> Assignment -> Assignment)
    -> (forall b.
        (Ord b, SymVal b, Num b) =>
        [Assignment] -> Assignment -> SBV b -> Assignment)
    -> Mergeable Assignment
    forall b.
    (Ord b, SymVal b, Num b) =>
    [Assignment] -> Assignment -> SBV b -> Assignment
    forall a.
    (Bool -> SBool -> a -> a -> a)
    -> (forall b. (Ord b, SymVal b, Num b) => [a] -> a -> SBV b -> a)
    -> Mergeable a
    $csymbolicMerge :: Bool -> SBool -> Assignment -> Assignment -> Assignment
    symbolicMerge :: Bool -> SBool -> Assignment -> Assignment -> Assignment
    $cselect :: forall b.
    (Ord b, SymVal b, Num b) =>
    [Assignment] -> Assignment -> SBV b -> Assignment
    select :: forall b.
    (Ord b, SymVal b, Num b) =>
    [Assignment] -> Assignment -> SBV b -> Assignment
    Mergeable)

    -- | Create a symbolic assignment, using symbolic fields.
    mkSym :: Orangutan -> Symbolic Assignment
    mkSym :: Orangutan -> Symbolic Assignment
    mkSym Orangutan
    o = do let h :: String
    h = Orangutan -> String
    forall a. Show a => a -> String
    show Orangutan
    o String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    ".handler"
                     l :: String
    l = Orangutan -> String
    forall a. Show a => a -> String
    show Orangutan
    o String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    ".location"
                     a :: String
    a = Orangutan -> String
    forall a. Show a => a -> String
    show Orangutan
    o String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    ".age"
                 Assignment
    s <- SBV Orangutan -> SHandler -> SLocation -> SInteger -> Assignment
    MkAssignment (Orangutan -> SBV Orangutan
    forall a. SymVal a => a -> SBV a
    literal Orangutan
    o) (SHandler -> SLocation -> SInteger -> Assignment)
    -> SymbolicT IO SHandler
    -> SymbolicT IO (SLocation -> SInteger -> Assignment)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> String -> SymbolicT IO SHandler
    forall a. SymVal a => String -> Symbolic (SBV a)
    free String
    h SymbolicT IO (SLocation -> SInteger -> Assignment)
    -> SymbolicT IO SLocation -> SymbolicT IO (SInteger -> Assignment)
    forall a b.
    SymbolicT IO (a -> b) -> SymbolicT IO a -> SymbolicT IO b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> String -> SymbolicT IO SLocation
    forall a. SymVal a => String -> Symbolic (SBV a)
    free String
    l SymbolicT IO (SInteger -> Assignment)
    -> SymbolicT IO SInteger -> Symbolic Assignment
    forall a b.
    SymbolicT IO (a -> b) -> SymbolicT IO a -> SymbolicT IO b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> String -> SymbolicT IO SInteger
    forall a. SymVal a => String -> Symbolic (SBV a)
    free String
    a
                 SBool -> SymbolicT IO ()
    forall a. QuantifiedBool a => a -> SymbolicT IO ()
    forall (m :: * -> *) a.
    (SolverContext m, QuantifiedBool a) =>
    a -> m ()
    constrain (SBool -> SymbolicT IO ()) -> SBool -> SymbolicT IO ()
    forall a b. (a -> b) -> a -> b
    $ Assignment
    s.age SInteger -> [SInteger] -> SBool
    forall a. EqSymbolic a => a -> [a] -> SBool
    `sElem` [SInteger
    4, SInteger
    7, SInteger
    10, SInteger
    13]
                 Assignment -> Symbolic Assignment
    forall a. a -> SymbolicT IO a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Assignment
    s

    -- | We get:
    --
    -- >>> allSat puzzle
    -- Solution #1:
    --   Merah.handler    =   Gracie :: Handler
    --   Merah.location   =  Tarakan :: Location
    --   Merah.age        =       10 :: Integer
    --   Ofallo.handler   =      Eva :: Handler
    --   Ofallo.location  =  Kendisi :: Location
    --   Ofallo.age       =       13 :: Integer
    --   Quirrel.handler  =    Dolly :: Handler
    --   Quirrel.location =  Basahan :: Location
    --   Quirrel.age      =        4 :: Integer
    --   Shamir.handler   = Francine :: Handler
    --   Shamir.location  =  Ambalat :: Location
    --   Shamir.age       =        7 :: Integer
    -- This is the only solution.
    puzzle :: ConstraintSet
    puzzle :: SymbolicT IO ()
    puzzle = do
       solution :: [Assignment]
    solution@[Assignment
    _merah, Assignment
    ofallo, Assignment
    quirrel, Assignment
    shamir] <- (Orangutan -> Symbolic Assignment)
    -> [Orangutan] -> SymbolicT IO [Assignment]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
    mapM Orangutan -> Symbolic Assignment
    mkSym [Orangutan
    forall a. Bounded a => a
    minBound .. Orangutan
    forall a. Bounded a => a
    maxBound]

       let find :: (Assignment -> SBool) -> Assignment
    find Assignment -> SBool
    f = (Assignment -> Assignment -> Assignment)
    -> [Assignment] -> Assignment
    forall a. (a -> a -> a) -> [a] -> a
    forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
    foldr1 (\Assignment
    a1 Assignment
    a2 -> SBool -> Assignment -> Assignment -> Assignment
    forall a. Mergeable a => SBool -> a -> a -> a
    ite (Assignment -> SBool
    f Assignment
    a1) Assignment
    a1 Assignment
    a2) [Assignment]
    solution

       -- 0. All are different in terms of handlers, locations, and ages
       SBool -> SymbolicT IO ()
    forall a. QuantifiedBool a => a -> SymbolicT IO ()
    forall (m :: * -> *) a.
    (SolverContext m, QuantifiedBool a) =>
    a -> m ()
    constrain (SBool -> SymbolicT IO ()) -> SBool -> SymbolicT IO ()
    forall a b. (a -> b) -> a -> b
    $ [SHandler] -> SBool
    forall a. EqSymbolic a => [a] -> SBool
    distinct ((Assignment -> SHandler) -> [Assignment] -> [SHandler]
    forall a b. (a -> b) -> [a] -> [b]
    map (.handler)  [Assignment]
    solution)
       SBool -> SymbolicT IO ()
    forall a. QuantifiedBool a => a -> SymbolicT IO ()
    forall (m :: * -> *) a.
    (SolverContext m, QuantifiedBool a) =>
    a -> m ()
    constrain (SBool -> SymbolicT IO ()) -> SBool -> SymbolicT IO ()
    forall a b. (a -> b) -> a -> b
    $ [SLocation] -> SBool
    forall a. EqSymbolic a => [a] -> SBool
    distinct ((Assignment -> SLocation) -> [Assignment] -> [SLocation]
    forall a b. (a -> b) -> [a] -> [b]
    map (.location) [Assignment]
    solution)
       SBool -> SymbolicT IO ()
    forall a. QuantifiedBool a => a -> SymbolicT IO ()
    forall (m :: * -> *) a.
    (SolverContext m, QuantifiedBool a) =>
    a -> m ()
    constrain (SBool -> SymbolicT IO ()) -> SBool -> SymbolicT IO ()
    forall a b. (a -> b) -> a -> b
    $ [SInteger] -> SBool
    forall a. EqSymbolic a => [a] -> SBool
    distinct ((Assignment -> SInteger) -> [Assignment] -> [SInteger]
    forall a b. (a -> b) -> [a] -> [b]
    map (.age)      [Assignment]
    solution)

       -- 1. Shamir is 7 years old.
       SBool -> SymbolicT IO ()
    forall a. QuantifiedBool a => a -> SymbolicT IO ()
    forall (m :: * -> *) a.
    (SolverContext m, QuantifiedBool a) =>
    a -> m ()
    constrain (SBool -> SymbolicT IO ()) -> SBool -> SymbolicT IO ()
    forall a b. (a -> b) -> a -> b
    $ Assignment
    shamir.age SInteger -> SInteger -> SBool
    forall a. EqSymbolic a => a -> a -> SBool
    .== SInteger
    7

       -- 2. Shamir came from Ambalat.
       SBool -> SymbolicT IO ()
    forall a. QuantifiedBool a => a -> SymbolicT IO ()
    forall (m :: * -> *) a.
    (SolverContext m, QuantifiedBool a) =>
    a -> m ()
    constrain (SBool -> SymbolicT IO ()) -> SBool -> SymbolicT IO ()
    forall a b. (a -> b) -> a -> b
    $ Assignment
    shamir.location SLocation -> SLocation -> SBool
    forall a. EqSymbolic a => a -> a -> SBool
    .== SLocation
    sAmbalat

       -- 3. Quirrel is younger than the ape that was found in Tarakan.
       let tarakan :: Assignment
    tarakan = (Assignment -> SBool) -> Assignment
    find (\Assignment
    a -> Assignment
    a.location SLocation -> SLocation -> SBool
    forall a. EqSymbolic a => a -> a -> SBool
    .== SLocation
    sTarakan)
       SBool -> SymbolicT IO ()
    forall a. QuantifiedBool a => a -> SymbolicT IO ()
    forall (m :: * -> *) a.
    (SolverContext m, QuantifiedBool a) =>
    a -> m ()
    constrain (SBool -> SymbolicT IO ()) -> SBool -> SymbolicT IO ()
    forall a b. (a -> b) -> a -> b
    $ Assignment
    quirrel.age SInteger -> SInteger -> SBool
    forall a. OrdSymbolic a => a -> a -> SBool
    .< Assignment
    tarakan.age

       -- 4. Of Ofallo and the ape that was found in Tarakan, one is cared for by Gracie and the other is 13 years old.
       let clue4 :: r -> r -> SBool
    clue4 r
    a1 r
    a2 = r
    a1.handler SHandler -> SHandler -> SBool
    forall a. EqSymbolic a => a -> a -> SBool
    .== SHandler
    sGracie SBool -> SBool -> SBool
    .&& r
    a2.age a -> a -> SBool
    forall a. EqSymbolic a => a -> a -> SBool
    .== a
    13
       SBool -> SymbolicT IO ()
    forall a. QuantifiedBool a => a -> SymbolicT IO ()
    forall (m :: * -> *) a.
    (SolverContext m, QuantifiedBool a) =>
    a -> m ()
    constrain (SBool -> SymbolicT IO ()) -> SBool -> SymbolicT IO ()
    forall a b. (a -> b) -> a -> b
    $ Assignment -> Assignment -> SBool
    forall {a} {r} {r}.
    (EqSymbolic a, HasField "handler" r SHandler, HasField "age" r a,
     Num a) =>
    r -> r -> SBool
    clue4 Assignment
    ofallo Assignment
    tarakan SBool -> SBool -> SBool
    .|| Assignment -> Assignment -> SBool
    forall {a} {r} {r}.
    (EqSymbolic a, HasField "handler" r SHandler, HasField "age" r a,
     Num a) =>
    r -> r -> SBool
    clue4 Assignment
    tarakan Assignment
    ofallo
       SBool -> SymbolicT IO ()
    forall a. QuantifiedBool a => a -> SymbolicT IO ()
    forall (m :: * -> *) a.
    (SolverContext m, QuantifiedBool a) =>
    a -> m ()
    constrain (SBool -> SymbolicT IO ()) -> SBool -> SymbolicT IO ()
    forall a b. (a -> b) -> a -> b
    $ SBV Orangutan
    sOfallo SBV Orangutan -> SBV Orangutan -> SBool
    forall a. EqSymbolic a => a -> a -> SBool
    ./= Assignment
    tarakan.orangutan

       -- 5. The animal that was found in Ambalat is either the 10-year-old or the animal Francine works with.
       let ambalat :: Assignment
    ambalat = (Assignment -> SBool) -> Assignment
    find (\Assignment
    a -> Assignment
    a.location SLocation -> SLocation -> SBool
    forall a. EqSymbolic a => a -> a -> SBool
    .== SLocation
    sAmbalat)
       SBool -> SymbolicT IO ()
    forall a. QuantifiedBool a => a -> SymbolicT IO ()
    forall (m :: * -> *) a.
    (SolverContext m, QuantifiedBool a) =>
    a -> m ()
    constrain (SBool -> SymbolicT IO ()) -> SBool -> SymbolicT IO ()
    forall a b. (a -> b) -> a -> b
    $ Assignment
    ambalat.age SInteger -> SInteger -> SBool
    forall a. EqSymbolic a => a -> a -> SBool
    .== SInteger
    10 SBool -> SBool -> SBool
    .|| Assignment
    ambalat.handler SHandler -> SHandler -> SBool
    forall a. EqSymbolic a => a -> a -> SBool
    .== SHandler
    sFrancine

       -- 6. Ofallo isn't 10 years old.
       SBool -> SymbolicT IO ()
    forall a. QuantifiedBool a => a -> SymbolicT IO ()
    forall (m :: * -> *) a.
    (SolverContext m, QuantifiedBool a) =>
    a -> m ()
    constrain (SBool -> SymbolicT IO ()) -> SBool -> SymbolicT IO ()
    forall a b. (a -> b) -> a -> b
    $ Assignment
    ofallo.age SInteger -> SInteger -> SBool
    forall a. EqSymbolic a => a -> a -> SBool
    ./= SInteger
    10

       -- 7. The ape that was found in Kendisi is older than the ape Dolly works with.
       let kendisi :: Assignment
    kendisi = (Assignment -> SBool) -> Assignment
    find (\Assignment
    a -> Assignment
    a.location SLocation -> SLocation -> SBool
    forall a. EqSymbolic a => a -> a -> SBool
    .== SLocation
    sKendisi)
       let dolly :: Assignment
    dolly   = (Assignment -> SBool) -> Assignment
    find (\Assignment
    a -> Assignment
    a.handler  SHandler -> SHandler -> SBool
    forall a. EqSymbolic a => a -> a -> SBool
    .== SHandler
    sDolly)
       SBool -> SymbolicT IO ()
    forall a. QuantifiedBool a => a -> SymbolicT IO ()
    forall (m :: * -> *) a.
    (SolverContext m, QuantifiedBool a) =>
    a -> m ()
    constrain (SBool -> SymbolicT IO ()) -> SBool -> SymbolicT IO ()
    forall a b. (a -> b) -> a -> b
    $ Assignment
    kendisi.age SInteger -> SInteger -> SBool
    forall a. OrdSymbolic a => a -> a -> SBool
    .> Assignment
    dolly.age