Github repository: https://github.com/mgritter/soffit
Previous entry: "My #Procjam Project: Soffit"
I was supposed to go out and have fun this weekend; instead I both got sick and handled two customer escalations. But I made a little progress on the next task for my graph rewrite engine: I implemented pattern matching!
The code below pretty closely follows the example from my prototype using or-tools and I'm happy at how it came out. The right-hand rule will require some additional constraints in the model, to avoid leaving dangling edges or simultaneously deleting and not deleting a vertex or edge.
A design choice to explore once I have actual users: do they expect that a rule A--B matches any edge, even one with a tag? As implemented, it only matches edges without a tag. I was thinking of putting in a wildcard match whose syntax would be something like A--B [$x], as shown in my design exploration document.
def leftSide( self, leftGraph ):
"""Specify the left side of a rule; that is, a graph to match."""
self.checkCompatible( leftGraph )
self.left = leftGraph
maxVertex = max( self.graph.nodes )
# Build a variable for each vertex that must be matched.
# The convention is to allow non-injective matches, so
# two variables could match to the same vertex.
for n in leftGraph.nodes:
# FIXME: how permissive is this on what may be in a string?
v = self.model.NewIntVar( 0, maxVertex, n )
self.variables[n] = v
# Add a contraint to only assign to nodes with identical tag.
# FIXME: no tag is *not* a wildcard, does that match expectations?
tag = leftGraph.nodes[n].get( 'tag', None )
matchingTag = [ i for i in self.graph.nodes
if self.graph.nodes[i].get( 'tag', None ) == tag ]
if self.verbose:
print( "node", n, "matchingTag", matchingTag )
if len( matchingTag ) == 0:
self.impossible = True
return
# If node choice is unconstrained, don't bother adding it as
# a constraint!
if len( matchingTag ) != len( self.graph.nodes ):
self.model.AddAllowedAssignments(
[v],
[ (x,) for x in matchingTag ] )
# Add an allowed assignment for each edge that must be matched,
# again limiting to just exact matching tags.
for (a,b) in leftGraph.edges:
tag = leftGraph.edges[a,b].get( 'tag', None )
matchingTag = [ i for i in self.graph.edges
if self.graph.edges[i].get( 'tag', None ) == tag ]
if self.verbose:
print( "edge", (a,b), "matchingTag", matchingTag )
if len( matchingTag ) == 0:
self.impossible = True
return
# Allow reverse matches if the graph is undirected
if not nx.is_directed( leftGraph ):
revEdges = [ (b,a) for (a,b) in matchingTag ]
matchingTag += revEdges
self.model.AddAllowedAssignments( [self.variables[a], self.variables[b]],
matchingTag )
Unfortunately, I found two bugs in or-tools:
The solver returned the same solution multiple times. I didn't file an issue because I didn't know if this was expected, though some of the examples suggested it was not. But a maintainer confirmed it's a bug. This one I can easily work around by putting the matches found into a set to deduplicate them.
I also crashed the C++ library with an unsatisfiable instance. This will be harder to work around. If the library was pure Python I could just catch the error, but the C++ assert kills the process. It looks like the non-callback function Solve doesn't crash, so maybe I can try calling that first.
I also found bugs in my own code, of course, and reworked the parser to create a canonical version of a graph after merging has been done. The previous version had some nodes that were aliases as separate objects in the networkx graph, and I found myself writing a separate "make it canonical" step which made no sense (and would have made tag handling a lot more complicated.)
Next steps:
- Workaround or-tools bug, or fix it in the original sources
- Write the additional constraints imposed by the right-hand side rule
- Perform the graph rewriting!