KCFGStore for managing loading and storage of KCFG data

Start by reading the KCFG class and the related issue 686 to understand the broken replace_node behavior. Trace how nodes and edge types are stored, then review the proposed KCFGStore dictionaries and the optimizer in pull request 872. Done means node updates remain consistent across all KCFG accessors and no code outside KCFG manipulates the underlying data structures directly.

Related: https://github.com/runtimeverification/pyk/issues/686

Currently in the KCFG class, we store a copy of the nodes on each of the edge types in the KCFG, which makes it very easy to select the source/target nodes for an edge without doing a second node lookup in the KCFG. The issue is that routines which modify nodes (such as (i) replace_node, which is broken https://github.com/runtimeverification/pyk/issues/686, or (ii) if we switch to storing attributes directly on the node), don't also modify the given edges which contain the node as a source/target.

Another observation is that for any given node, it may have 0 or 1 successors, and that's it. We enforce this at the code level. So we can take advantage of this in our data-structures, by instead just having a single dictionary of _successors and _predecessors, where the _successors dictionary either has the entry with a single integer pointing at the target successor or nothing, and the precessors has a list of potential predecessors.

We could do one of two things:

• Change the way we store KCFGs in the following way:
  • New class KCFGStore, which has _nodes: dict[int, KCFG.Node], _constraints: dict[int, KInner], _csubsts: dict[int, CSubst]. These are the basic datas that are needed to reconstruct any edge in a KCFG.
  • Change the storage of nodes/edges in the KCFG class to be dictionaries that contain references to the given data components instead. For example, _covers becomes _dict[int, dict[int, int]], then when we are returning a Cover from KCFG.Cover, we lookup the relevant CSubst in KCFGStore._csubsts(...) and construct a KCFG.Cover directly at that moment.
  • Make sure there aren't any places outside of KCFG where the underlying datastructures are manipulated directly.

This would make it so that when we change a given node (adding a constraint, change attributes, simplify it, etc...), all the KCFG accessors will also be correctly updated. This change may also make it so we can more broadly apply things like the optimizer (https://github.com/runtimeverification/pyk/pull/872) across all datastructures in the KCFGStore.