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
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
|
-----------------------------------------------------------------------------
-- |
-- Module : Documentation.SBV.Examples.Misc.Definitions
-- Copyright : (c) Levent Erkok
-- License : BSD3
-- Maintainer: erkokl@gmail.com
-- Stability : experimental
--
-- Demonstrates how we can add actual SMT-definitions for functions
-- that cannot otherwise be defined in SBV. Typically, these are used
-- for recursive definitions.
-----------------------------------------------------------------------------
{-# LANGUAGE OverloadedLists #-}
{-# OPTIONS_GHC -Wall -Werror #-}
module Documentation.SBV.Examples.Misc.Definitions where
import Data.SBV
import Data.SBV.Tuple
import qualified Data.SBV.List as L
-------------------------------------------------------------------------
-- * Simple functions
-------------------------------------------------------------------------
-- | Add one to an argument
add1 :: SInteger -> SInteger
add1 = smtFunction "add1" (+1)
-- | Reverse run the add1 function. Note that the generated SMTLib will have the function
-- add1 itself defined. You can verify this by running the below in verbose mode.
--
-- >>> add1Example
-- Satisfiable. Model:
-- x = 4 :: Integer
add1Example :: IO SatResult
add1Example = sat $ do
x <- sInteger "x"
pure $ 5 .== add1 x
-------------------------------------------------------------------------
-- * Basic recursive functions
-------------------------------------------------------------------------
-- | Sum of numbers from 0 to the given number. Since this is a recursive
-- definition, we cannot simply symbolically simulate it as it wouldn't
-- terminat. So, we use the function generation facilities to define it
-- directly in SMTLib. Note how the function itself takes a "recursive version"
-- of itself, and all recursive calls are made with this name.
sumToN :: SInteger -> SInteger
sumToN = smtFunction "sumToN" $ \x -> ite (x .<= 0) 0 (x + sumToN (x - 1))
-- | Prove that sumToN works as expected.
--
-- We have:
--
-- >>> sumToNExample
-- Satisfiable. Model:
-- s0 = 5 :: Integer
-- s1 = 15 :: Integer
sumToNExample :: IO SatResult
sumToNExample = sat $ \a r -> a .== 5 .&& r .== sumToN a
-- | Coding list-length recursively. Again, we map directly to an SMTLib function.
len :: SList Integer -> SInteger
len = smtFunction "list_length" $ \xs -> ite (L.null xs) 0 (1 + len (L.tail xs))
-- | Calculate the length of a list, using recursive functions.
--
-- We have:
--
-- >>> lenExample
-- Satisfiable. Model:
-- s0 = [1,2,3] :: [Integer]
-- s1 = 3 :: Integer
lenExample :: IO SatResult
lenExample = sat $ \a r -> a .== [1,2,3::Integer] .&& r .== len a
-------------------------------------------------------------------------
-- * Mutual recursion
-------------------------------------------------------------------------
-- | A simple mutual-recursion example, from the z3 documentation. We have:
--
-- >>> pingPong
-- Satisfiable. Model:
-- s0 = 1 :: Integer
pingPong :: IO SatResult
pingPong = sat $ \x -> x .> 0 .&& ping x sTrue .> x
where ping :: SInteger -> SBool -> SInteger
ping = smtFunction "ping" $ \x y -> ite y (pong (x+1) (sNot y)) (x - 1)
pong :: SInteger -> SBool -> SInteger
pong = smtFunction "pong" $ \a b -> ite b (ping (a-1) (sNot b)) a
-- | Usual way to define even-odd mutually recursively. Unfortunately, while this goes through,
-- the backend solver does not terminate on this example. See 'evenOdd2' for an alternative
-- technique to handle such definitions, which seems to be more solver friendly.
evenOdd :: IO SatResult
evenOdd = satWith z3{verbose=True} $ \a r -> a .== 20 .&& r .== isE a
where isE, isO :: SInteger -> SBool
isE = smtFunction "isE" $ \x -> ite (x .< 0) (isE (-x)) (x .== 0 .|| isO (x - 1))
isO = smtFunction "isO" $ \x -> ite (x .< 0) (isO (-x)) (x .== 0 .|| isE (x - 1))
-- | Another technique to handle mutually definitions is to define the functions together, and pull the results out individually.
-- This usually works better than defining the functions separately, from a solver perspective.
isEvenOdd :: SInteger -> STuple Bool Bool
isEvenOdd = smtFunction "isEvenOdd" $ \x -> ite (x .< 0) (isEvenOdd (-x))
$ ite (x .== 0) (tuple (sTrue, sFalse))
(swap (isEvenOdd (x - 1)))
-- | Extract the isEven function for easier use.
isEven :: SInteger -> SBool
isEven x = isEvenOdd x ^._1
-- | Extract the isOdd function for easier use.
isOdd :: SInteger -> SBool
isOdd x = isEvenOdd x ^._2
-- | We can prove 20 is even and definitely not odd, thusly:
--
-- >>> evenOdd2
-- Satisfiable. Model:
-- s0 = 20 :: Integer
-- s1 = True :: Bool
-- s2 = False :: Bool
evenOdd2 :: IO SatResult
evenOdd2 = sat $ \a r1 r2 -> a .== 20 .&& r1 .== isEven a .&& r2 .== isOdd a
-------------------------------------------------------------------------
-- * Nested recursion
-------------------------------------------------------------------------
-- | Ackermann function, demonstrating nested recursion.
ack :: SInteger -> SInteger -> SInteger
ack = smtFunction "ack" $ \x y -> ite (x .== 0) (y + 1)
$ ite (y .== 0) (ack (x - 1) 1)
(ack (x - 1) (ack x (y - 1)))
-- | We can prove constant-folding instances of the equality @ack 1 y == y + 2@:
--
-- >>> ack1y
-- Satisfiable. Model:
-- s0 = 5 :: Integer
-- s1 = 7 :: Integer
--
-- Expecting the prover to handle the general case for arbitrary @y@ is beyond the current
-- scope of what SMT solvers do out-of-the-box for the time being.
ack1y :: IO SatResult
ack1y = sat $ \y r -> y .== 5 .&& r .== ack 1 y
|
