Documentation.SBV.Examples.Misc.ProgramPaths

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?

Documentation

d1 :: SInteger -> SInteger -> SInteger

Symbolic version of d1 x y = if y < x - 2 then 7 else 2

d2 :: SInteger -> SInteger

Symbolic version of d2 x y = if y > 3 then 10 else 50

d3 :: SInteger -> SInteger -> SInteger

Symbolic version of d3 x y = if y < -x + 3 then 100 else 200

d4 :: SInteger -> SInteger -> SInteger

Symbolic version of d4 x y = d1 x y + d2 x y + d3 x y

paths :: IO AllSatResult

Compute all possible program paths. Note the call to partition, 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.