sbv-14.0: Documentation/SBV/Examples/Misc/Definitions.hs
-----------------------------------------------------------------------------
-- |
-- 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 #-}
{-# LANGUAGE QuasiQuotes #-}
{-# OPTIONS_GHC -Wall -Werror #-}
module Documentation.SBV.Examples.Misc.Definitions where
import Data.SBV
import Data.SBV.Tuple
-------------------------------------------------------------------------
-- * 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
-- terminate. So, we use the function generation facilities to define it
-- directly in SMTLib.
sumToN :: SInteger -> SInteger
sumToN = smtFunction "sumToN" $ \x -> [sCase| x of
_ | 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 -> [sCase| xs of
[] -> 0
_:ts -> 1 + len ts
|]
-- | 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] .&& 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 = smtFunctionWithMeasure "ping" (\_ y -> ite y 1 (0 :: SInteger), [])
$ \x y -> [sCase| y of
True -> pong (x+1) (sNot y)
False -> x - 1
|]
pong :: SInteger -> SBool -> SInteger
pong = smtFunctionWithMeasure "pong" (\_ b -> ite b 1 (0 :: SInteger), [])
$ \a b -> [sCase| b of
True -> ping (a-1) (sNot b)
False -> a
|]
-- | Usual way to define even-odd mutually recursively. While the termination measure
-- is verified, current SMT solvers do not terminate when evaluating mutually recursive
-- @define-funs-rec@ definitions. See 'isEvenOdd' for a single-function alternative
-- that is more solver-friendly.
--
-- >>> evenOdd
-- Unknown.
-- Reason: timeout
evenOdd :: IO SatResult
evenOdd = sat $ do setTimeOut 5000
a <- sInteger "a"
r <- sBool "r"
constrain $ a .== 20 .&& r .== isE a
where isE, isO :: SInteger -> SBool
isE = smtFunctionWithMeasure "isE" (\x -> tuple (abs x, ite (x .< 0) (1 :: SInteger) 0), [])
$ \x -> [sCase| x of
_ | x .< 0 -> isE (-x)
_ -> x .== 0 .|| isO (x - 1)
|]
isO = smtFunctionWithMeasure "isO" (\x -> tuple (abs x, ite (x .< 0) (1 :: SInteger) 0), [])
$ \x -> [sCase| x of
_ | 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.
--
-- The measure @(abs x, ite (x < 0) 1 0)@ ensures termination: when @x < 0@, the call @isEvenOdd(-x)@
-- keeps @abs x@ the same but drops the second component from 1 to 0. When @x > 0@, the call
-- @isEvenOdd(x-1)@ decreases @abs x@.
isEvenOdd :: SInteger -> STuple Bool Bool
isEvenOdd = smtFunctionWithMeasure "isEvenOdd" (\x -> tuple (abs x, ite (x .< 0) (1 :: SInteger) 0), [])
$ \x -> [sCase| x of
_ | x .< 0 -> isEvenOdd (-x)
_ | 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 -> [sCase| x of
_ | x .<= 0 -> y + 1
_ | 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