    -----------------------------------------------------------------------------
    -- |
    -- Module    : Documentation.SBV.Examples.Puzzles.Fish
    -- Copyright : (c) Levent Erkok
    -- License   : BSD3
    -- Maintainer: erkokl@gmail.com
    -- Stability : experimental
    --
    -- Solves the following logic puzzle, attributed to Albert Einstein:
    --
    --   - The Briton lives in the red house.
    --   - The Swede keeps dogs as pets.
    --   - The Dane drinks tea.
    --   - The green house is left to the white house.
    --   - The owner of the green house drinks coffee.
    --   - The person who plays football rears birds.
    --   - The owner of the yellow house plays baseball.
    --   - The man living in the center house drinks milk.
    --   - The Norwegian lives in the first house.
    --   - The man who plays volleyball lives next to the one who keeps cats.
    --   - The man who keeps the horse lives next to the one who plays baseball.
    --   - The owner who plays tennis drinks beer.
    --   - The German plays hockey.
    --   - The Norwegian lives next to the blue house.
    --   - The man who plays volleyball has a neighbor who drinks water.
    --
    -- Who owns the fish?
    ------------------------------------------------------------------------------

    {-# OPTIONS_GHC -Wall -Werror #-}

    {-# LANGUAGE DeriveAnyClass      #-}
    {-# LANGUAGE DeriveDataTypeable  #-}
    {-# LANGUAGE ScopedTypeVariables #-}
    {-# LANGUAGE StandaloneDeriving  #-}
    {-# LANGUAGE TemplateHaskell     #-}

    module Documentation.SBV.Examples.Puzzles.Fish where

    import Data.SBV

    -- | Colors of houses
    data Color = Red | Green | White | Yellow | Blue

    -- | Make 'Color' a symbolic value.
    mkSymbolicEnumeration ''Color

    -- | Nationalities of the occupants
    data Nationality = Briton | Dane | Swede | Norwegian | German

    -- | Make 'Nationality' a symbolic value.
    mkSymbolicEnumeration ''Nationality

    -- | Beverage choices
    data Beverage = Tea | Coffee | Milk | Beer | Water

    -- | Make 'Beverage' a symbolic value.
    mkSymbolicEnumeration ''Beverage

    -- | Pets they keep
    data Pet = Dog | Horse | Cat | Bird | Fish

    -- | Make 'Pet' a symbolic value.
    mkSymbolicEnumeration ''Pet

    -- | Sports they engage in
    data Sport = Football | Baseball | Volleyball | Hockey | Tennis

    -- | Make 'Sport' a symbolic value.
    mkSymbolicEnumeration ''Sport

    -- | We have:
    --
    -- >>> fishOwner
    -- German
    --
    -- It's not hard to modify this program to grab the values of all the assignments, i.e., the full
    -- solution to the puzzle. We leave that as an exercise to the interested reader!
    -- NB. We use the 'allSatTrackUFs' configuration to indicate that the uninterpreted function
    -- changes do not matter for generating different values. All we care is that the fishOwner changes!
    fishOwner :: IO ()
    fishOwner :: IO ()
    fishOwner = do [Maybe Nationality]
    vs <- String -> AllSatResult -> [Maybe Nationality]
    forall b. SymVal b => String -> AllSatResult -> [Maybe b]
    getModelValues String
    "fishOwner" (AllSatResult -> [Maybe Nationality])
    -> IO AllSatResult -> IO [Maybe Nationality]
    forall a b. (a -> b) -> IO a -> IO b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    `fmap` SMTConfig -> SymbolicT IO () -> IO AllSatResult
    forall a. Satisfiable a => SMTConfig -> a -> IO AllSatResult
    allSatWith SMTConfig
    z3{allSatTrackUFs :: Bool
    allSatTrackUFs = Bool
    False} SymbolicT IO ()
    puzzle
                   case [Maybe Nationality]
    vs of
                     [Just (Nationality
    v::Nationality)] -> Nationality -> IO ()
    forall a. Show a => a -> IO ()
    print Nationality
    v
                     []                      -> String -> IO ()
    forall a. HasCallStack => String -> a
    error String
    "no solution"
                     [Maybe Nationality]
    _                       -> String -> IO ()
    forall a. HasCallStack => String -> a
    error String
    "no unique solution"
     where puzzle :: SymbolicT IO ()
    puzzle = do

              let c :: SBV Integer -> SBV Color
    c = String -> SBV Integer -> SBV Color
    forall a. SMTDefinable a => String -> a
    uninterpret String
    "color"
                  n :: SBV Integer -> SBV Nationality
    n = String -> SBV Integer -> SBV Nationality
    forall a. SMTDefinable a => String -> a
    uninterpret String
    "nationality"
                  b :: SBV Integer -> SBV Beverage
    b = String -> SBV Integer -> SBV Beverage
    forall a. SMTDefinable a => String -> a
    uninterpret String
    "beverage"
                  p :: SBV Integer -> SBV Pet
    p = String -> SBV Integer -> SBV Pet
    forall a. SMTDefinable a => String -> a
    uninterpret String
    "pet"
                  s :: SBV Integer -> SBV Sport
    s = String -> SBV Integer -> SBV Sport
    forall a. SMTDefinable a => String -> a
    uninterpret String
    "sport"

              let a
    i neighbor :: a -> a -> SBool
    `neighbor` a
    j = a
    i a -> a -> SBool
    forall a. EqSymbolic a => a -> a -> SBool
    .== a
    ja -> a -> a
    forall a. Num a => a -> a -> a
    +a
    1 SBool -> SBool -> SBool
    .|| a
    j a -> a -> SBool
    forall a. EqSymbolic a => a -> a -> SBool
    .== a
    ia -> a -> a
    forall a. Num a => a -> a -> a
    +a
    1
                  SBV a
    a is :: SBV a -> a -> SBool
    `is`       a
    v = SBV a
    a SBV a -> SBV a -> SBool
    forall a. EqSymbolic a => a -> a -> SBool
    .== a -> SBV a
    forall a. SymVal a => a -> SBV a
    literal a
    v

              let fact0 :: SBool -> SymbolicT IO ()
    fact0   = SBool -> SymbolicT IO ()
    forall a. QuantifiedBool a => a -> SymbolicT IO ()
    forall (m :: * -> *) a.
    (SolverContext m, QuantifiedBool a) =>
    a -> m ()
    constrain
                  fact1 :: (SBV Integer -> a) -> SymbolicT IO ()
    fact1 SBV Integer -> a
    f = do SBV Integer
    i <- Symbolic (SBV Integer)
    forall a. SymVal a => Symbolic (SBV a)
    free_
                               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 Integer
    1 SBV Integer -> SBV Integer -> SBool
    forall a. OrdSymbolic a => a -> a -> SBool
    .<= SBV Integer
    i SBool -> SBool -> SBool
    .&& SBV Integer
    i SBV Integer -> SBV Integer -> SBool
    forall a. OrdSymbolic a => a -> a -> SBool
    .<= (SBV Integer
    5 :: SInteger)
                               a -> SymbolicT IO ()
    forall a. QuantifiedBool a => a -> SymbolicT IO ()
    forall (m :: * -> *) a.
    (SolverContext m, QuantifiedBool a) =>
    a -> m ()
    constrain (a -> SymbolicT IO ()) -> a -> SymbolicT IO ()
    forall a b. (a -> b) -> a -> b
    $ SBV Integer -> a
    f SBV Integer
    i
                  fact2 :: (SBV Integer -> SBV Integer -> a) -> SymbolicT IO ()
    fact2 SBV Integer -> SBV Integer -> a
    f = do SBV Integer
    i <- Symbolic (SBV Integer)
    forall a. SymVal a => Symbolic (SBV a)
    free_
                               SBV Integer
    j <- Symbolic (SBV Integer)
    forall a. SymVal a => Symbolic (SBV a)
    free_
                               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 Integer
    1 SBV Integer -> SBV Integer -> SBool
    forall a. OrdSymbolic a => a -> a -> SBool
    .<= SBV Integer
    i SBool -> SBool -> SBool
    .&& SBV Integer
    i SBV Integer -> SBV Integer -> SBool
    forall a. OrdSymbolic a => a -> a -> SBool
    .<= (SBV Integer
    5 :: SInteger)
                               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 Integer
    1 SBV Integer -> SBV Integer -> SBool
    forall a. OrdSymbolic a => a -> a -> SBool
    .<= SBV Integer
    j SBool -> SBool -> SBool
    .&& SBV Integer
    j SBV Integer -> SBV Integer -> SBool
    forall a. OrdSymbolic a => a -> a -> SBool
    .<= SBV Integer
    5
                               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 Integer
    i SBV Integer -> SBV Integer -> SBool
    forall a. EqSymbolic a => a -> a -> SBool
    ./= SBV Integer
    j
                               a -> SymbolicT IO ()
    forall a. QuantifiedBool a => a -> SymbolicT IO ()
    forall (m :: * -> *) a.
    (SolverContext m, QuantifiedBool a) =>
    a -> m ()
    constrain (a -> SymbolicT IO ()) -> a -> SymbolicT IO ()
    forall a b. (a -> b) -> a -> b
    $ SBV Integer -> SBV Integer -> a
    f SBV Integer
    i SBV Integer
    j

              (SBV Integer -> SBool) -> SymbolicT IO ()
    forall {a}.
    QuantifiedBool a =>
    (SBV Integer -> a) -> SymbolicT IO ()
    fact1 ((SBV Integer -> SBool) -> SymbolicT IO ())
    -> (SBV Integer -> SBool) -> SymbolicT IO ()
    forall a b. (a -> b) -> a -> b
    $ \SBV Integer
    i   -> SBV Integer -> SBV Nationality
    n SBV Integer
    i SBV Nationality -> Nationality -> SBool
    forall {a}. SymVal a => SBV a -> a -> SBool
    `is` Nationality
    Briton     SBool -> SBool -> SBool
    .&& SBV Integer -> SBV Color
    c SBV Integer
    i SBV Color -> Color -> SBool
    forall {a}. SymVal a => SBV a -> a -> SBool
    `is` Color
    Red
              (SBV Integer -> SBool) -> SymbolicT IO ()
    forall {a}.
    QuantifiedBool a =>
    (SBV Integer -> a) -> SymbolicT IO ()
    fact1 ((SBV Integer -> SBool) -> SymbolicT IO ())
    -> (SBV Integer -> SBool) -> SymbolicT IO ()
    forall a b. (a -> b) -> a -> b
    $ \SBV Integer
    i   -> SBV Integer -> SBV Nationality
    n SBV Integer
    i SBV Nationality -> Nationality -> SBool
    forall {a}. SymVal a => SBV a -> a -> SBool
    `is` Nationality
    Swede      SBool -> SBool -> SBool
    .&& SBV Integer -> SBV Pet
    p SBV Integer
    i SBV Pet -> Pet -> SBool
    forall {a}. SymVal a => SBV a -> a -> SBool
    `is` Pet
    Dog
              (SBV Integer -> SBool) -> SymbolicT IO ()
    forall {a}.
    QuantifiedBool a =>
    (SBV Integer -> a) -> SymbolicT IO ()
    fact1 ((SBV Integer -> SBool) -> SymbolicT IO ())
    -> (SBV Integer -> SBool) -> SymbolicT IO ()
    forall a b. (a -> b) -> a -> b
    $ \SBV Integer
    i   -> SBV Integer -> SBV Nationality
    n SBV Integer
    i SBV Nationality -> Nationality -> SBool
    forall {a}. SymVal a => SBV a -> a -> SBool
    `is` Nationality
    Dane       SBool -> SBool -> SBool
    .&& SBV Integer -> SBV Beverage
    b SBV Integer
    i SBV Beverage -> Beverage -> SBool
    forall {a}. SymVal a => SBV a -> a -> SBool
    `is` Beverage
    Tea
              (SBV Integer -> SBV Integer -> SBool) -> SymbolicT IO ()
    forall {a}.
    QuantifiedBool a =>
    (SBV Integer -> SBV Integer -> a) -> SymbolicT IO ()
    fact2 ((SBV Integer -> SBV Integer -> SBool) -> SymbolicT IO ())
    -> (SBV Integer -> SBV Integer -> SBool) -> SymbolicT IO ()
    forall a b. (a -> b) -> a -> b
    $ \SBV Integer
    i SBV Integer
    j -> SBV Integer -> SBV Color
    c SBV Integer
    i SBV Color -> Color -> SBool
    forall {a}. SymVal a => SBV a -> a -> SBool
    `is` Color
    Green      SBool -> SBool -> SBool
    .&& SBV Integer -> SBV Color
    c SBV Integer
    j SBV Color -> Color -> SBool
    forall {a}. SymVal a => SBV a -> a -> SBool
    `is` Color
    White    SBool -> SBool -> SBool
    .&& SBV Integer
    i SBV Integer -> SBV Integer -> SBool
    forall a. EqSymbolic a => a -> a -> SBool
    .== SBV Integer
    jSBV Integer -> SBV Integer -> SBV Integer
    forall a. Num a => a -> a -> a
    -SBV Integer
    1
              (SBV Integer -> SBool) -> SymbolicT IO ()
    forall {a}.
    QuantifiedBool a =>
    (SBV Integer -> a) -> SymbolicT IO ()
    fact1 ((SBV Integer -> SBool) -> SymbolicT IO ())
    -> (SBV Integer -> SBool) -> SymbolicT IO ()
    forall a b. (a -> b) -> a -> b
    $ \SBV Integer
    i   -> SBV Integer -> SBV Color
    c SBV Integer
    i SBV Color -> Color -> SBool
    forall {a}. SymVal a => SBV a -> a -> SBool
    `is` Color
    Green      SBool -> SBool -> SBool
    .&& SBV Integer -> SBV Beverage
    b SBV Integer
    i SBV Beverage -> Beverage -> SBool
    forall {a}. SymVal a => SBV a -> a -> SBool
    `is` Beverage
    Coffee
              (SBV Integer -> SBool) -> SymbolicT IO ()
    forall {a}.
    QuantifiedBool a =>
    (SBV Integer -> a) -> SymbolicT IO ()
    fact1 ((SBV Integer -> SBool) -> SymbolicT IO ())
    -> (SBV Integer -> SBool) -> SymbolicT IO ()
    forall a b. (a -> b) -> a -> b
    $ \SBV Integer
    i   -> SBV Integer -> SBV Sport
    s SBV Integer
    i SBV Sport -> Sport -> SBool
    forall {a}. SymVal a => SBV a -> a -> SBool
    `is` Sport
    Football   SBool -> SBool -> SBool
    .&& SBV Integer -> SBV Pet
    p SBV Integer
    i SBV Pet -> Pet -> SBool
    forall {a}. SymVal a => SBV a -> a -> SBool
    `is` Pet
    Bird
              (SBV Integer -> SBool) -> SymbolicT IO ()
    forall {a}.
    QuantifiedBool a =>
    (SBV Integer -> a) -> SymbolicT IO ()
    fact1 ((SBV Integer -> SBool) -> SymbolicT IO ())
    -> (SBV Integer -> SBool) -> SymbolicT IO ()
    forall a b. (a -> b) -> a -> b
    $ \SBV Integer
    i   -> SBV Integer -> SBV Color
    c SBV Integer
    i SBV Color -> Color -> SBool
    forall {a}. SymVal a => SBV a -> a -> SBool
    `is` Color
    Yellow     SBool -> SBool -> SBool
    .&& SBV Integer -> SBV Sport
    s SBV Integer
    i SBV Sport -> Sport -> SBool
    forall {a}. SymVal a => SBV a -> a -> SBool
    `is` Sport
    Baseball
              SBool -> SymbolicT IO ()
    fact0 (SBool -> SymbolicT IO ()) -> SBool -> SymbolicT IO ()
    forall a b. (a -> b) -> a -> b
    $         SBV Integer -> SBV Beverage
    b SBV Integer
    3 SBV Beverage -> Beverage -> SBool
    forall {a}. SymVal a => SBV a -> a -> SBool
    `is` Beverage
    Milk
              SBool -> SymbolicT IO ()
    fact0 (SBool -> SymbolicT IO ()) -> SBool -> SymbolicT IO ()
    forall a b. (a -> b) -> a -> b
    $         SBV Integer -> SBV Nationality
    n SBV Integer
    1 SBV Nationality -> Nationality -> SBool
    forall {a}. SymVal a => SBV a -> a -> SBool
    `is` Nationality
    Norwegian
              (SBV Integer -> SBV Integer -> SBool) -> SymbolicT IO ()
    forall {a}.
    QuantifiedBool a =>
    (SBV Integer -> SBV Integer -> a) -> SymbolicT IO ()
    fact2 ((SBV Integer -> SBV Integer -> SBool) -> SymbolicT IO ())
    -> (SBV Integer -> SBV Integer -> SBool) -> SymbolicT IO ()
    forall a b. (a -> b) -> a -> b
    $ \SBV Integer
    i SBV Integer
    j -> SBV Integer -> SBV Sport
    s SBV Integer
    i SBV Sport -> Sport -> SBool
    forall {a}. SymVal a => SBV a -> a -> SBool
    `is` Sport
    Volleyball SBool -> SBool -> SBool
    .&& SBV Integer -> SBV Pet
    p SBV Integer
    j SBV Pet -> Pet -> SBool
    forall {a}. SymVal a => SBV a -> a -> SBool
    `is` Pet
    Cat      SBool -> SBool -> SBool
    .&& SBV Integer
    i SBV Integer -> SBV Integer -> SBool
    forall {a}. (EqSymbolic a, Num a) => a -> a -> SBool
    `neighbor` SBV Integer
    j
              (SBV Integer -> SBV Integer -> SBool) -> SymbolicT IO ()
    forall {a}.
    QuantifiedBool a =>
    (SBV Integer -> SBV Integer -> a) -> SymbolicT IO ()
    fact2 ((SBV Integer -> SBV Integer -> SBool) -> SymbolicT IO ())
    -> (SBV Integer -> SBV Integer -> SBool) -> SymbolicT IO ()
    forall a b. (a -> b) -> a -> b
    $ \SBV Integer
    i SBV Integer
    j -> SBV Integer -> SBV Pet
    p SBV Integer
    i SBV Pet -> Pet -> SBool
    forall {a}. SymVal a => SBV a -> a -> SBool
    `is` Pet
    Horse      SBool -> SBool -> SBool
    .&& SBV Integer -> SBV Sport
    s SBV Integer
    j SBV Sport -> Sport -> SBool
    forall {a}. SymVal a => SBV a -> a -> SBool
    `is` Sport
    Baseball SBool -> SBool -> SBool
    .&& SBV Integer
    i SBV Integer -> SBV Integer -> SBool
    forall {a}. (EqSymbolic a, Num a) => a -> a -> SBool
    `neighbor` SBV Integer
    j
              (SBV Integer -> SBool) -> SymbolicT IO ()
    forall {a}.
    QuantifiedBool a =>
    (SBV Integer -> a) -> SymbolicT IO ()
    fact1 ((SBV Integer -> SBool) -> SymbolicT IO ())
    -> (SBV Integer -> SBool) -> SymbolicT IO ()
    forall a b. (a -> b) -> a -> b
    $ \SBV Integer
    i   -> SBV Integer -> SBV Sport
    s SBV Integer
    i SBV Sport -> Sport -> SBool
    forall {a}. SymVal a => SBV a -> a -> SBool
    `is` Sport
    Tennis     SBool -> SBool -> SBool
    .&& SBV Integer -> SBV Beverage
    b SBV Integer
    i SBV Beverage -> Beverage -> SBool
    forall {a}. SymVal a => SBV a -> a -> SBool
    `is` Beverage
    Beer
              (SBV Integer -> SBool) -> SymbolicT IO ()
    forall {a}.
    QuantifiedBool a =>
    (SBV Integer -> a) -> SymbolicT IO ()
    fact1 ((SBV Integer -> SBool) -> SymbolicT IO ())
    -> (SBV Integer -> SBool) -> SymbolicT IO ()
    forall a b. (a -> b) -> a -> b
    $ \SBV Integer
    i   -> SBV Integer -> SBV Nationality
    n SBV Integer
    i SBV Nationality -> Nationality -> SBool
    forall {a}. SymVal a => SBV a -> a -> SBool
    `is` Nationality
    German     SBool -> SBool -> SBool
    .&& SBV Integer -> SBV Sport
    s SBV Integer
    i SBV Sport -> Sport -> SBool
    forall {a}. SymVal a => SBV a -> a -> SBool
    `is` Sport
    Hockey
              (SBV Integer -> SBV Integer -> SBool) -> SymbolicT IO ()
    forall {a}.
    QuantifiedBool a =>
    (SBV Integer -> SBV Integer -> a) -> SymbolicT IO ()
    fact2 ((SBV Integer -> SBV Integer -> SBool) -> SymbolicT IO ())
    -> (SBV Integer -> SBV Integer -> SBool) -> SymbolicT IO ()
    forall a b. (a -> b) -> a -> b
    $ \SBV Integer
    i SBV Integer
    j -> SBV Integer -> SBV Nationality
    n SBV Integer
    i SBV Nationality -> Nationality -> SBool
    forall {a}. SymVal a => SBV a -> a -> SBool
    `is` Nationality
    Norwegian  SBool -> SBool -> SBool
    .&& SBV Integer -> SBV Color
    c SBV Integer
    j SBV Color -> Color -> SBool
    forall {a}. SymVal a => SBV a -> a -> SBool
    `is` Color
    Blue     SBool -> SBool -> SBool
    .&& SBV Integer
    i SBV Integer -> SBV Integer -> SBool
    forall {a}. (EqSymbolic a, Num a) => a -> a -> SBool
    `neighbor` SBV Integer
    j
              (SBV Integer -> SBV Integer -> SBool) -> SymbolicT IO ()
    forall {a}.
    QuantifiedBool a =>
    (SBV Integer -> SBV Integer -> a) -> SymbolicT IO ()
    fact2 ((SBV Integer -> SBV Integer -> SBool) -> SymbolicT IO ())
    -> (SBV Integer -> SBV Integer -> SBool) -> SymbolicT IO ()
    forall a b. (a -> b) -> a -> b
    $ \SBV Integer
    i SBV Integer
    j -> SBV Integer -> SBV Sport
    s SBV Integer
    i SBV Sport -> Sport -> SBool
    forall {a}. SymVal a => SBV a -> a -> SBool
    `is` Sport
    Volleyball SBool -> SBool -> SBool
    .&& SBV Integer -> SBV Beverage
    b SBV Integer
    j SBV Beverage -> Beverage -> SBool
    forall {a}. SymVal a => SBV a -> a -> SBool
    `is` Beverage
    Water    SBool -> SBool -> SBool
    .&& SBV Integer
    i SBV Integer -> SBV Integer -> SBool
    forall {a}. (EqSymbolic a, Num a) => a -> a -> SBool
    `neighbor` SBV Integer
    j

              SBV Nationality
    ownsFish <- String -> Symbolic (SBV Nationality)
    forall a. SymVal a => String -> Symbolic (SBV a)
    free String
    "fishOwner"
              (SBV Integer -> SBool) -> SymbolicT IO ()
    forall {a}.
    QuantifiedBool a =>
    (SBV Integer -> a) -> SymbolicT IO ()
    fact1 ((SBV Integer -> SBool) -> SymbolicT IO ())
    -> (SBV Integer -> SBool) -> SymbolicT IO ()
    forall a b. (a -> b) -> a -> b
    $ \SBV Integer
    i -> SBV Integer -> SBV Nationality
    n SBV Integer
    i SBV Nationality -> SBV Nationality -> SBool
    forall a. EqSymbolic a => a -> a -> SBool
    .== SBV Nationality
    ownsFish SBool -> SBool -> SBool
    .&& SBV Integer -> SBV Pet
    p SBV Integer
    i SBV Pet -> Pet -> SBool
    forall {a}. SymVal a => SBV a -> a -> SBool
    `is` Pet
    Fish