Allow node aliases

[alberdingk-thijm]

It would be great if we could use other values to refer to nodes rather than simply numbers. This could be a simple case where we internally just store all the node labels in a list and use the list indices internally, but print with the labels.

We would need to either add a new node_labels declaration of some kind, or change how a user can write nodes declarations.

Here's a rough idea of what it might look like:

type attribute = int

(* 4 node SRP *)
let nodes = [ 'a, 'b, 'c, 'd, ]

let edges = {
    'a-'b;
    'b-'a;
    'c='d;
    'b='d;
}

let merge n x y = min x y

let trans e x = if e = 'a~'b then 0 else x + 1

let init n = if n = 'd then 0 else 10

[alberdingk-thijm]

Some thoughts on how we can potentially do this:

Change the type of Vertex.t

One natural way to allow node aliases to work would be to change the underlying type of vertices to be some other value, e.g. a string. Code that currently assumes nodes are integers between 0 and n (like the SMT encoding) would then be change to iterate over the vertices of the graph. Pros:

• Easy to understand from a programmer's perspective.
• Easy to refactor again in the future if we want to change the type of vertex, or extend it to let the users define nodes differently.
• SMT query and printing functions can retain node names for easier debugging.
• Partitioning can simply cut nodes from the graph (an O(|V|*ln(|V|)) operation), without needing to re-index any (grows with the size of the AST).

Cons:

• May be slower to use an additional map data structure to look up vertices. For example, refactoring SmtClassicEncoding would mean changing code that iterates over an Array (which has O(1) access time) to iterate over vertices (which are backed in ocamlgraph by a Map, itself implemented using AVL trees). Swapping the Graph.Persistent implementation for a Graph.Imperative may however help address this issue.

Add syntactic sugar to name nodes

Another approach would be to convert a statement like this:

let nodes = ('a, 'b, 'c, 'd)
let edges = {'a-'b; 'b-'a; 'b='c; 'b='d; }

into one like this:

let nodes = 4
let edges = {0-1; 1-0; 1=2; 1=3; }
let 'a = 0
let 'b = 1
let 'c = 2
let 'd = 3

We then can use 'a, 'b, 'c, 'd freely in the rest of the file and they will be inlined by the transformations. Pros:

• Very easy change to make to the code and underlying representation is left untouched.
• Performance penalty is equivalent to one additional step during parsing, and slightly more code to inline once.

Cons:

• Names are lost internally, which means the user may have to determine a name's index themself when debugging an SMT query.
• Partitioning must look up these labels and re-index or delete each one (order O(|V|)?)

Overall, while Option 1 is promising from a design perspective, it may not make sense performance-wise. Hence, a better approach might be to take Option 2.