Copyright | (c) Levent Erkok |
---|---|

License | BSD3 |

Maintainer | erkokl@gmail.com |

Stability | experimental |

Safe Haskell | None |

Language | Haskell2010 |

Illustrates the use of `sBranch`

, as a means of dealing with certain cases
of the symbolic-termination problem.

# Documentation

bitCount :: SWord32 -> SWord8 Source

A fast implementation of population-count. Note that SBV already provides
this functionality via `sbvPopCount`

, using simple expansion and counting
algorithm. `sbvPopCount`

is linear in the size of the input, i.e., a 32-bit
word would take 32 additions. This implementation here is *faster* in the
sense that it takes as many additions as there are set-bits in the given word.

Of course, the issue is that this definition is recursive, and the usual
definition via `ite`

would never symbolically terminate: Recursion is done
on the input argument: In each recursive call, we *reduce* the value `n`

to `n .&. (n-1)`

. This eliminates one set-bit in the input. However, this
claim is far from obvious. By the use of `sBranch`

we tell SBV to call
the SMT solver in each test to ensure we only evaluate the branches we need,
thus avoiding the symbolic-termination issue. In a sense, the SMT solvers
proves that the implementation terminates for all valid inputs.

Note that replacing `sBranch`

in this implementation with `ite`

would cause
symbolic-termination to loop forever. Of course, this does *not* mean that
`sBranch`

is fast: It is costly to make external calls to the solver for
each branch, so use with care.

Prove that the `bitCount`

function implemented here is equivalent to
the internal "slower" implementation. We have:

`>>>`

Q.E.D.`prop`

path :: SWord8 -> SWord8 Source

Illustrates the use of path-conditions in avoiding infeasible paths in symbolic
simulation. If we used `ite`

instead of `sBranch`

in the else-branch of the
implementation of `path`

symbolic simulation would have encountered the `error`

call, and
hence would have failed. But `sBranch`

keeps track of the path condition, and can
successfully determine that this path will never be taken, and hence avoids the problem.
Note that we can freely mix/match `ite`

and `sBranch`

calls; path conditions will be
tracked in both cases. In fact, use of `ite`

is advisable if we know for a fact that
both branches are feasible, as it avoids the external call. `sBranch`

will have the
same result, albeit it'll cost more.