-----------------------------------------------------------------------------
-- |
-- Module    : Documentation.SBV.Examples.Misc.ProgramPaths
-- Copyright : (c) Levent Erkok
-- License   : BSD3
-- Maintainer: erkokl@gmail.com
-- Stability : experimental
--
-- A simple example of showing how to compute program paths. Consider the simple
-- program:
--
-- @
--   d1 x y = if y < x - 2  then   7 else   2
--   d2   y = if y > 3      then  10 else  50
--   d3 x y = if y < -x + 3 then 100 else 200
--   d4 x y = d1 x y + d2 y + d3 x y
-- @
--
-- What are all the possible values @d4 x y@ can take, and what are the values of
-- @x@ and @y@ to obtain these values?
-----------------------------------------------------------------------------

{-# OPTIONS_GHC -Wall -Werror #-}

module Documentation.SBV.Examples.Misc.ProgramPaths where

import Data.SBV

-- | Symbolic version of @d1 x y = if y < x - 2 then 7 else 2@
d1 :: SInteger -> SInteger -> SInteger
d1 :: SInteger -> SInteger -> SInteger
d1 SInteger
x SInteger
y = SBool -> SInteger -> SInteger -> SInteger
forall a. Mergeable a => SBool -> a -> a -> a
ite (SInteger
y SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.< SInteger
x SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
- SInteger
2) SInteger
7 SInteger
2

-- | Symbolic version of @d2 x y = if y > 3 then  10 else  50@
d2 :: SInteger -> SInteger
d2 :: SInteger -> SInteger
d2 SInteger
y = SBool -> SInteger -> SInteger -> SInteger
forall a. Mergeable a => SBool -> a -> a -> a
ite (SInteger
y SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.> SInteger
3) SInteger
10 SInteger
50

-- | Symbolic version of @d3 x y = if y < -x + 3 then 100 else 200@
d3 :: SInteger -> SInteger -> SInteger
d3 :: SInteger -> SInteger -> SInteger
d3 SInteger
x SInteger
y = SBool -> SInteger -> SInteger -> SInteger
forall a. Mergeable a => SBool -> a -> a -> a
ite (SInteger
y SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.< -SInteger
x SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger
3) SInteger
100 SInteger
200

-- | Symbolic version of @d4 x y = d1 x y + d2 x y + d3 x y@
d4 :: SInteger -> SInteger -> SInteger
d4 :: SInteger -> SInteger -> SInteger
d4 SInteger
x SInteger
y = SInteger -> SInteger -> SInteger
d1 SInteger
x SInteger
y SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger -> SInteger
d2 SInteger
y SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger -> SInteger -> SInteger
d3 SInteger
x SInteger
y

-- | Compute all possible program paths. Note the call to `allSatPartition`, which
-- causes `allSat` to find models that generate differing values for the given
-- expression. We have:
--
-- >>> paths
-- Solution #1:
--   x =  -2 :: Integer
--   y =   4 :: Integer
--   r = 112 :: Integer
-- Solution #2:
--   x =   0 :: Integer
--   y =   3 :: Integer
--   r = 252 :: Integer
-- Solution #3:
--   x =  -1 :: Integer
--   y =   4 :: Integer
--   r = 212 :: Integer
-- Solution #4:
--   x =   3 :: Integer
--   y =   0 :: Integer
--   r = 257 :: Integer
-- Solution #5:
--   x =   2 :: Integer
--   y =  -1 :: Integer
--   r = 157 :: Integer
-- Solution #6:
--   x =   7 :: Integer
--   y =   4 :: Integer
--   r = 217 :: Integer
-- Solution #7:
--   x =   0 :: Integer
--   y =   0 :: Integer
--   r = 152 :: Integer
-- Found 7 different solutions.
paths :: IO AllSatResult
paths :: IO AllSatResult
paths = SymbolicT IO () -> IO AllSatResult
forall a. Satisfiable a => a -> IO AllSatResult
allSat (SymbolicT IO () -> IO AllSatResult)
-> SymbolicT IO () -> IO AllSatResult
forall a b. (a -> b) -> a -> b
$ do
  x <- String -> Symbolic SInteger
sInteger String
"x"
  y <- sInteger "y"
  allSatPartition "r" $ d4 x y