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