ToZ3 produces intermediate Python code that can be used to generate Z3 expressions from P4 programs. The code does not work without the parent repository Gauntlet. Please see more details there.
ToZ3 is written as an extension to P4C. It has no other dependencies. First P4C must be installed. Instructions can be found here.
| Option | Description |
|---|---|
--ouput |
File name of the output Python Z3 formula |
--emit_p4 |
If set, will generate a --output.p4 P4 program |
--prune |
If set, will randomly prune the input P4 program and output to --output Z3 formula |