    -----------------------------------------------------------------------------
    -- |
    -- 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.
    -----------------------------------------------------------------------------

    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 n = take n <$> runSMT genFibs

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

                 -- constrain the length
                 constrain $ L.length fibs .== 200

                 -- Constrain first two elements
                 constrain $ fibs .!! 0 .== 1
                 constrain $ fibs .!! 1 .== 1

                 -- Constrain an arbitrary element at index `i`
                 let constr i = constrain $ fibs .!! i + fibs .!! (i+1) .== fibs .!! (i+2)

                 -- Constrain the remaining elts
                 mapM_ (constr . fromIntegral) [(0::Int) .. 197]

                 query $ do cs <- checkSat
                            case cs of
                              Unk   -> error "Solver returned unknown!"
                              Unsat -> error "Solver couldn't generate the fibonacci sequence!"
                              Sat   -> getValue fibs