Module substitution_parser 

Parsing functions for VeriPB substitutions.

A substitution in VeriPB format is a list of pairs of variables and literals or truth values. For instance:

x1 1 x12 0 variable x1 another ~x1

maps x1 to true, x12 to false, variable to x1, and another to not x1.

Optionally, it is possible to add the arrow -> inside a pair, so that our example becomes:

x1 -> 1 x12 -> 0 variable -> x1 another -> ~x1

Tokenization is performed by using SubstitutionToken.

Functions

parse_substitution

Parse a substitution in VeriPB format into the Substitution data structure.