next up previous
Next: Formula Straightening Up: Formula Processor Details Previous: The ``Nothing Inside'' Test

Parser Implementation

The graph rewriting parser uses two main data structures: a labelled directed graph and a priority queue. A graph is represented within the system using:

The priority queue is implemented as a doubly linked list, the items in the list ordered by their score. Each item in the queue holds a copy of the formula graph, along with additional information about the state of the formula processing at that point.

Steve Smithies