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