    -----------------------------------------------------------------------------
    -- |
    -- Module    : Documentation.SBV.Examples.Lists.Fibonacci
    -- Copyright : (c) Joel Burget
    -- License   : BSD3
    -- Maintainer: erkokl@gmail.com
    -- Stability : experimental
    --
    -- Define the fibonacci sequence as an SBV symbolic list.
    -----------------------------------------------------------------------------

    {-# OPTIONS_GHC -Wall -Werror #-}

    module Documentation.SBV.Examples.Lists.Fibonacci where

    import Data.SBV

    import           Data.SBV.List ((.!!))
    import qualified Data.SBV.List as L

    import Data.SBV.Control

    -- | Compute a prefix of the fibonacci numbers. We have:
    --
    -- >>> mkFibs 10
    -- [1,1,2,3,5,8,13,21,34,55]
    mkFibs :: Int -> IO [Integer]
    mkFibs :: Int -> IO [Integer]
    mkFibs n :: Int
    n = Int -> [Integer] -> [Integer]
    forall a. Int -> [a] -> [a]
    take Int
    n ([Integer] -> [Integer]) -> IO [Integer] -> IO [Integer]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Symbolic [Integer] -> IO [Integer]
    forall a. Symbolic a -> IO a
    runSMT Symbolic [Integer]
    genFibs

    -- | Generate fibonacci numbers as a sequence. Note that we constrain only
    -- the first 200 entries.
    genFibs :: Symbolic [Integer]
    genFibs :: Symbolic [Integer]
    genFibs = do SList Integer
    fibs <- String -> Symbolic (SList Integer)
    forall a. SymVal a => String -> Symbolic (SList a)
    sList "fibs"

                 -- constrain the length
                 SBool -> SymbolicT IO ()
    forall (m :: * -> *). SolverContext m => SBool -> m ()
    constrain (SBool -> SymbolicT IO ()) -> SBool -> SymbolicT IO ()
    forall a b. (a -> b) -> a -> b
    $ SList Integer -> SInteger
    forall a. SymVal a => SList a -> SInteger
    L.length SList Integer
    fibs SInteger -> SInteger -> SBool
    forall a. EqSymbolic a => a -> a -> SBool
    .== 200

                 -- Constrain first two elements
                 SBool -> SymbolicT IO ()
    forall (m :: * -> *). SolverContext m => SBool -> m ()
    constrain (SBool -> SymbolicT IO ()) -> SBool -> SymbolicT IO ()
    forall a b. (a -> b) -> a -> b
    $ SList Integer
    fibs SList Integer -> SInteger -> SInteger
    forall a. SymVal a => SList a -> SInteger -> SBV a
    .!! 0 SInteger -> SInteger -> SBool
    forall a. EqSymbolic a => a -> a -> SBool
    .== 1
                 SBool -> SymbolicT IO ()
    forall (m :: * -> *). SolverContext m => SBool -> m ()
    constrain (SBool -> SymbolicT IO ()) -> SBool -> SymbolicT IO ()
    forall a b. (a -> b) -> a -> b
    $ SList Integer
    fibs SList Integer -> SInteger -> SInteger
    forall a. SymVal a => SList a -> SInteger -> SBV a
    .!! 1 SInteger -> SInteger -> SBool
    forall a. EqSymbolic a => a -> a -> SBool
    .== 1

                 -- Constrain an arbitrary element at index `i`
                 let constr :: SInteger -> m ()
    constr i :: SInteger
    i = SBool -> m ()
    forall (m :: * -> *). SolverContext m => SBool -> m ()
    constrain (SBool -> m ()) -> SBool -> m ()
    forall a b. (a -> b) -> a -> b
    $ SList Integer
    fibs SList Integer -> SInteger -> SInteger
    forall a. SymVal a => SList a -> SInteger -> SBV a
    .!! SInteger
    i SInteger -> SInteger -> SInteger
    forall a. Num a => a -> a -> a
    + SList Integer
    fibs SList Integer -> SInteger -> SInteger
    forall a. SymVal a => SList a -> SInteger -> SBV a
    .!! (SInteger
    iSInteger -> SInteger -> SInteger
    forall a. Num a => a -> a -> a
    +1) SInteger -> SInteger -> SBool
    forall a. EqSymbolic a => a -> a -> SBool
    .== SList Integer
    fibs SList Integer -> SInteger -> SInteger
    forall a. SymVal a => SList a -> SInteger -> SBV a
    .!! (SInteger
    iSInteger -> SInteger -> SInteger
    forall a. Num a => a -> a -> a
    +2)

                 -- Constrain the remaining elts
                 (Int -> SymbolicT IO ()) -> [Int] -> SymbolicT IO ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    (a -> m b) -> t a -> m ()
    mapM_ (SInteger -> SymbolicT IO ()
    forall (m :: * -> *). SolverContext m => SInteger -> m ()
    constr (SInteger -> SymbolicT IO ())
    -> (Int -> SInteger) -> Int -> SymbolicT IO ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Int -> SInteger
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral) [(0::Int) .. 197]

                 Query [Integer] -> Symbolic [Integer]
    forall a. Query a -> Symbolic a
    query (Query [Integer] -> Symbolic [Integer])
    -> Query [Integer] -> Symbolic [Integer]
    forall a b. (a -> b) -> a -> b
    $ do CheckSatResult
    cs <- Query CheckSatResult
    checkSat
                            case CheckSatResult
    cs of
                              Unk   -> String -> Query [Integer]
    forall a. HasCallStack => String -> a
    error "Solver returned unknown!"
                              Unsat -> String -> Query [Integer]
    forall a. HasCallStack => String -> a
    error "Solver couldn't generate the fibonacci sequence!"
                              Sat   -> SList Integer -> Query [Integer]
    forall a. SymVal a => SBV a -> Query a
    getValue SList Integer
    fibs