A simple Java library for generating z3 / SMT-LIB code.
The library contains only a small portion of z3's features, and is not fully documented.
Created for the course Applied Logic, 2ITX0.
- Download the z3-gen.jar file from the latest release.
- Add the z3-gen.jar file to your IDE.
- For VSCode: open a folder in your IDE
- Open the File Explorer tab on the left
- Expand 'Java Projects'
- Expand the project to add it to (there's probably only one)
- Click the + next to Referenced Libraries
- Select the z3-gen.jar file
- Take a look at the examples below, and try them out and play around with them to see how this library works.
Check out a few examples, I recommend going over them in this order, in increasing difficulty: