Illustrates the use of
sBranch, as a means of dealing with certain cases
of the symbolic-termination problem.
A fast implementation of population-count. Note that SBV already provides
this functionality via
sbvPopCount, using simple expansion and counting
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
ite would never symbolically terminate: Recursion is done
on the input argument: In each recursive call, we reduce the value
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.
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
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
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.