Blockpc

This patch addresses issue #81 by implementing blockpc based on Peter's
suggestion. blockpc has the same semantics as pc, except that pc only applies
when the given predecessor of the given block is chosen.

blockpc(s) are collected in a way similar to what we currently do for pc(s),
and are encoded with a similar technique for encoding UB constraints.

The parser is also updated to parse blockpc(s).

I am sorry the path is a bit big...

This doesn't look right. If a given blockpc and pc are in an equivalence class that does not overlap with `Cand`'s equivalence class, that should not cause us to add the blockpc to the set of relevant blockpcs, as it should not be able to influence the validity of the overall expression.