Introduce sBranch

[LeventErkok]

It's useful at times to do a branch only if the condition is satisfiable. This cannot be done outside the SBV machinary currently, since cross-definitions would be missed. (This is realted to issue #71.) So, it needs to be supported primitively. The idea is to introduce a new kind of "ite", that only takes the branches that are reachable; pruning of either the true or false branch if we can show that they are not reachable from the current condition. This should be tied to a time-out; since we wouldn't want to spend way too much time doing this analysis: If timeout happens, then we assume both branches are reachable.

One idea is to add a new configuration to the SBV solver type. Just like you say now:

proveWith z3{verbose=True}

you'll be allowed to say:

proveWith z3{branchCheck=True, branchCheckTimeOut=Just 5}

which will change the "semantics" of "ite"; so it'll only evaluate a branch if it's on a satisfiable path.

Of course, this'll impact all the "ite"'s in your program. So, an alternative idea is to introduce a new kind of ite, let's call it sBranch; with the following signature:

sBranch :: Mergeable a => Maybe Int -> SBool -> SBV a -> SBV a -> SBV a
sBranch mbTimeOut cond trueBranch falseBranch = ...

With this design, you can selectively introduce "smarter" branching as you need.

[LeventErkok]

New design:

 sBranch :: Mergeable a => SBool -> a -> a -> a

And the time-out can be controlled via sBranchTimeOut parameter, which defaults to Nothing.