-----------------------------------------------------------------------------
-- |
-- 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 Prelude hiding ((!!))

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 Int
n = forall a. Int -> [a] -> [a]
take Int
n forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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 <- forall a. SymVal a => String -> Symbolic (SList a)
sList String
"fibs"

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

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

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

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

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