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

> If a predecessor produces zero predicates, then with the current approach, we just don't generate blockpcs for the BB (or should we?). My understanding is that if predicates on a predecessor are missing, then we have incomplete info about the incoming branches and don't want to produce blockpcs in this case. Maybe I am wrong.

It shouldn't mean that we don't want blockpcs at all for that block. For example, with this graph:
```
B1    B2
  \  /
   B3
```
we might normally encode this as:
(B1 pred 0 selected) => (B2's blockpcs) && (B1 pred 1 selected) => (B3's blockpcs)

But if we can't get blockpcs for B2 we could just encode it as:
(B1 pred 1 selected) => (B3's blockpcs)

I don't see any unsoundness there.

> Can you elaborate on the case where a predecessor produces more than one predicate? I am not sure if I understand it.

For example:

```
     B1
    /  \
  B2    B3
       /  \
     B4    B5    ...
             \  /              
              B6
```
we would want to harvest B1->B3 and B3->B5 for B6's first predecessor.