ToZ3 is a tool that produces Z3 expressions from P4-16 programs.

ToZ3 is written as an extension to P4C. It has no other dependencies. First P4C must be installed. Instructions can be found here.

Once P4C has been installed, ToZ3 can be installed as an extension. The following commands provide an example:

cd ~/p4c/
mkdir extensions
cd extensions
git clone https://github.com/p4gauntlet/toz3
cd ~/p4c/build
make

Afterwards, the ToZ3 executables can be found in the p4c/buildfolder. ToZ3 can be installed globally by running sudo make install.

Generating Z3 from P4-16 with ToZ3 is straightforward. The tool currently supports three different modes.

[TODO]