{-# 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
mkFibs :: Int -> IO [Integer]
mkFibs n = take n <$> runSMT genFibs
genFibs :: Symbolic [Integer]
genFibs = do fibs <- sList "fibs"
constrain $ L.length fibs .== 200
constrain $ fibs .!! 0 .== 1
constrain $ fibs .!! 1 .== 1
let constr i = constrain $ fibs .!! i + fibs .!! (i+1) .== fibs .!! (i+2)
mapM_ (constr . fromIntegral) [(0::Int) .. 197]
query $ do cs <- checkSat
case cs of
Unk -> error "Solver returned unknown!"
DSat{} -> error "Unexpected dsat result!"
Unsat -> error "Solver couldn't generate the fibonacci sequence!"
Sat -> getValue fibs