-----------------------------------------------------------------------------
-- |
-- 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 = Int -> [Integer] -> [Integer]
forall a. Int -> [a] -> [a]
take Int
n ([Integer] -> [Integer]) -> IO [Integer] -> IO [Integer]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Symbolic [Integer] -> IO [Integer]
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 fibs <- String -> Symbolic (SList Integer)
forall a. SymVal a => String -> Symbolic (SList a)
sList String
"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 SInteger
i = SBool -> m ()
forall a. QuantifiedBool a => a -> m ()
forall (m :: * -> *) a.
(SolverContext m, QuantifiedBool a) =>
a -> m ()
constrain (SBool -> m ()) -> SBool -> m ()
forall a b. (a -> b) -> a -> b
$ SList Integer
fibs SList Integer -> SInteger -> SInteger
forall a. SymVal a => SList a -> SInteger -> SBV a
!! SInteger
i SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SList Integer
fibs SList Integer -> SInteger -> SInteger
forall a. SymVal a => SList a -> SInteger -> SBV a
!! (SInteger
iSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+SInteger
1) SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SList Integer
fibs SList Integer -> SInteger -> SInteger
forall a. SymVal a => SList a -> SInteger -> SBV a
!! (SInteger
iSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+SInteger
2)

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

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