1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
|
-----------------------------------------------------------------------------
-- |
-- 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 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!"
DSat{} -> error "Unexpected dsat result!"
Unsat -> error "Solver couldn't generate the fibonacci sequence!"
Sat -> getValue fibs
|
