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...

Sorry about that. I should have used the complete notation including the predecessor number. I will update the notation. 

In terms of the second concern, I think my notation is confusing. I refine the graph as:
                 B1              B8
                /    \            /     \
                     B2      B3
                        \      /
                          B4             B9
                         /    \           /      \
                               B5    B6
                                  \    /
                                   B7
Let's say we are dealing with an instruction %i in B7, then correct form should be:
blockpc %B4, 0, s1, r1 // B1->B2
blockpc %B4, 1, s2, r2 // B8->B3
...
blockpc %B7, 0, s3, r3 // B4 -> B5
blockpc %B7, 1, s4, r4 // B9 -> B6
...
cand %i, 1

In fact, in the original call graph, we won't have blockpc for %B7 because we can't harvest predicates for %B6. So, basically the current mechanism is that we harvest blockpc for a BB only if we can collect predicates for all of its predecessors.