-----------------------------------------------------------------------------
-- |
-- 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 :: 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 SList Integer
fibs <- String -> Symbolic (SList Integer)
forall a. SymVal a => String -> Symbolic (SList a)
sList String
"fibs"

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

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

             -- Constrain an arbitrary element at index `i`
             let constr :: SInteger -> m ()
constr SInteger
i = SBool -> m ()
forall (m :: * -> *). SolverContext m => SBool -> 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
             (Int -> SymbolicT IO ()) -> [Int] -> SymbolicT IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (SInteger -> SymbolicT IO ()
forall (m :: * -> *). SolverContext m => SInteger -> m ()
constr (SInteger -> SymbolicT IO ())
-> (Int -> SInteger) -> Int -> SymbolicT IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> SInteger
forall a b. (Integral a, Num b) => a -> b
fromIntegral) [(Int
0::Int) .. Int
197]

             Query [Integer] -> Symbolic [Integer]
forall a. Query a -> Symbolic a
query (Query [Integer] -> Symbolic [Integer])
-> Query [Integer] -> Symbolic [Integer]
forall a b. (a -> b) -> a -> b
$ do CheckSatResult
cs <- Query CheckSatResult
checkSat
                        case CheckSatResult
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