Revisiting branch handling in pyk

[PetarMax]

With the merging of runtimeverification/pyk#942, the branching responses from the backend now come with rule identifiers and branching conditions. This information should allow us to minimize the use of the heuristic branch extraction and branching patterns and simply rely on the provided information instead.

A draft PR runtimeverification/pyk#1072 has been opened showing promising results. I would like to use this issue to discuss options with @ehildenb, @tothtamas28, @jberthold, @goodlyrottenapple, @geo2a, and others. In particular, I would like to understand:

1. How would it be possible for a branching to happen and the rule_predicate field not to have some sort of branching condition (i.e., equal None)? Would that be a pure non-deterministic transition and if so, would the rule_predicate effectively be #Top? Are there other possibilities?
2. Does the rule_id field of each next state in a branching response have the identifier of the rule that was used to create that branch? Is it possible for this field to be None?
3. Do we actually care if there is branch overlapping/non-determinism happening if we have got all the branching conditions right?