    -----------------------------------------------------------------------------
    -- |
    -- Module    : Documentation.SBV.Examples.Misc.Tuple
    -- Copyright : (c) Joel Burget
    --                 Levent Erkok
    -- License   : BSD3
    -- Maintainer: erkokl@gmail.com
    -- Stability : experimental
    --
    -- A basic tuple use case, also demonstrating regular expressions,
    -- strings, etc. This is a basic template for getting SBV to produce
    -- valid data for applications that require inputs that satisfy
    -- arbitrary criteria.
    -----------------------------------------------------------------------------

    {-# LANGUAGE OverloadedStrings   #-}
    {-# LANGUAGE ScopedTypeVariables #-}

    {-# OPTIONS_GHC -Wall -Werror #-}

    module Documentation.SBV.Examples.Misc.Tuple where

    import Data.SBV
    import Data.SBV.Tuple
    import Data.SBV.Control

    import Data.SBV.List   ((.!!))
    import Data.SBV.RegExp

    import qualified Data.SBV.String as S
    import qualified Data.SBV.List   as L

    -- | A dictionary is a list of lookup values. Note that we
    -- store the type @[(a, b)]@ as a symbolic value here, mixing
    -- sequences and tuples.
    type Dict a b = SBV [(a, b)]

    -- | Create a dictionary of length 5, such that each element
    -- has an string key and each value is the length of the key.
    -- We impose a few more constraints to make the output interesting.
    -- For instance, you might get:
    --
    -- @ ghci> example
    -- [("nt_",3),("dHAk",4),("kzkk0",5),("mZxs9s",6),("c32'dPM",7)]
    -- @
    --
    -- Depending on your version of z3, a different answer might be provided.
    -- Here, we check that it satisfies our length conditions:
    --
    -- >>> import Data.List (genericLength)
    -- >>> example >>= \ex -> return (length ex == 5 && all (\(l, i) -> genericLength l == i) ex)
    -- True
    example :: IO [(String, Integer)]
    example :: IO [(String, Integer)]
    example = Symbolic [(String, Integer)] -> IO [(String, Integer)]
    forall a. Symbolic a -> IO a
    runSMT (Symbolic [(String, Integer)] -> IO [(String, Integer)])
    -> Symbolic [(String, Integer)] -> IO [(String, Integer)]
    forall a b. (a -> b) -> a -> b
    $ do Dict String Integer
    dict :: Dict String Integer <- String -> Symbolic (Dict String Integer)
    forall a. SymVal a => String -> Symbolic (SBV a)
    free "dict"

                          -- require precisely 5 elements
                          let len :: Int
    len   = 5 :: Int
                              range :: [Int]
    range = [0 .. Int
    len Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - 1]

                          SBool -> SymbolicT IO ()
    forall (m :: * -> *). SolverContext m => SBool -> m ()
    constrain (SBool -> SymbolicT IO ()) -> SBool -> SymbolicT IO ()
    forall a b. (a -> b) -> a -> b
    $ Dict String Integer -> SInteger
    forall a. SymVal a => SList a -> SInteger
    L.length Dict String Integer
    dict SInteger -> SInteger -> SBool
    forall a. EqSymbolic a => a -> a -> SBool
    .== Int -> SInteger
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral Int
    len

                          -- require each key to be at of length 3 more than the index it occupies
                          -- and look like an identifier
                          let goodKey :: a -> SBV String -> SBool
    goodKey i :: a
    i s :: SBV String
    s = let l :: SInteger
    l = SBV String -> SInteger
    S.length SBV String
    s
                                                r :: RegExp
    r = RegExp
    asciiLower RegExp -> RegExp -> RegExp
    forall a. Num a => a -> a -> a
    * RegExp -> RegExp
    KStar (RegExp
    asciiLetter RegExp -> RegExp -> RegExp
    forall a. Num a => a -> a -> a
    + RegExp
    digit RegExp -> RegExp -> RegExp
    forall a. Num a => a -> a -> a
    + "_" RegExp -> RegExp -> RegExp
    forall a. Num a => a -> a -> a
    + "'")
                                          in SInteger
    l SInteger -> SInteger -> SBool
    forall a. EqSymbolic a => a -> a -> SBool
    .== a -> SInteger
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral a
    iSInteger -> SInteger -> SInteger
    forall a. Num a => a -> a -> a
    +3 SBool -> SBool -> SBool
    .&& SBV String
    s SBV String -> RegExp -> SBool
    forall a. RegExpMatchable a => a -> RegExp -> SBool
    `match` RegExp
    r

                              restrict :: a -> m ()
    restrict i :: a
    i = case SBV (String, Integer) -> (SBV String, SInteger)
    forall tup a. Tuple tup a => SBV tup -> a
    untuple (Dict String Integer
    dict Dict String Integer -> SInteger -> SBV (String, Integer)
    forall a. SymVal a => SList a -> SInteger -> SBV a
    .!! a -> SInteger
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral a
    i) of
                                             (k :: SBV String
    k, v :: SInteger
    v) -> SBool -> m ()
    forall (m :: * -> *). SolverContext m => SBool -> m ()
    constrain (SBool -> m ()) -> SBool -> m ()
    forall a b. (a -> b) -> a -> b
    $ a -> SBV String -> SBool
    forall a. Integral a => a -> SBV String -> SBool
    goodKey a
    i SBV String
    k SBool -> SBool -> SBool
    .&& SInteger
    v SInteger -> SInteger -> SBool
    forall a. EqSymbolic a => a -> a -> SBool
    .== SBV String -> SInteger
    S.length SBV String
    k

                          (Int -> SymbolicT IO ()) -> [Int] -> SymbolicT IO ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    (a -> m b) -> t a -> m ()
    mapM_ Int -> SymbolicT IO ()
    forall a (m :: * -> *). (Integral a, SolverContext m) => a -> m ()
    restrict [Int]
    range

                          -- require distinct keys:
                          let keys :: [SBV String]
    keys = [(Dict String Integer
    dict Dict String Integer -> SInteger -> SBV (String, Integer)
    forall a. SymVal a => SList a -> SInteger -> SBV a
    .!! Int -> SInteger
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral Int
    i)SBV (String, Integer)
    -> (SBV (String, Integer) -> SBV String) -> SBV String
    forall a b. a -> (a -> b) -> b
    ^.SBV (String, Integer) -> SBV String
    forall b a. HasField "_1" b a => SBV a -> SBV b
    _1 | Int
    i <- [Int]
    range]
                          SBool -> SymbolicT IO ()
    forall (m :: * -> *). SolverContext m => SBool -> m ()
    constrain (SBool -> SymbolicT IO ()) -> SBool -> SymbolicT IO ()
    forall a b. (a -> b) -> a -> b
    $ [SBV String] -> SBool
    forall a. EqSymbolic a => [a] -> SBool
    distinct [SBV String]
    keys

                          Query [(String, Integer)] -> Symbolic [(String, Integer)]
    forall a. Query a -> Symbolic a
    query (Query [(String, Integer)] -> Symbolic [(String, Integer)])
    -> Query [(String, Integer)] -> Symbolic [(String, Integer)]
    forall a b. (a -> b) -> a -> b
    $ do Query ()
    ensureSat
                                     Dict String Integer -> Query [(String, Integer)]
    forall a. SymVal a => SBV a -> Query a
    getValue Dict String Integer
    dict