The token file generated by the tokenizer includes the internal representation of a given DATR theory. It contains all necessary information for the inference engine required as input for zdatrinf. Note that the token file code structure is far from trivial, and manipulation can lead to completely unpredictable results -- so DON'T!
The following specification is therefore mentioned for the sake of completeness only and not specified in detail. The file is organized in three sections: the header information, the look-up tables for atoms, variables and nodes and the equation part. The header consists of the `magic string' DATR-Token-file followed by the source name of the theory. The three look-up tables are line-oriented and contain after the number of atoms/vars/nodes an enumeration number, the length of the item in bytes and the item itself. The equation section contains for each node the node key as defined in the look-up table, the number of equations, and the list of left hand sides and right hand sides with each pair separated with a '=='.