You will need to have Z3 installed; see Homework 0.
To double check, run z3 --version, you should get something like:
Z3 version 4.13.0 - 64 bit
(a different version is probably OK.)
You may need to pip3 install z3-solver if you are
using codespaces or if you are on a fresh machine.
As with HW1, you will submit your homework through GitHub Classroom. Clone your copy of the repository, then push your changes to GitHub before the deadline. Please see this Piazza post for further instructions.
Like HW1, there are three parts to the assignment and a fourth part that is extra credit:
- Part 1 is a series of mini exercises.
- Part 2 is a solver for the "four numbers" game that we played on the first day of class.
- Part 3 explores some of the limitations of Z3.
- Part 4 (optional) explores an application of Z3 to writing compiler optimizations.
There is also a helper file, helper.py that contains some useful
functions when working with Z3.
To continue, open and edit the files part1.py, part2.py, and part3.py.
If you get stuck, take a look at the file hints.md for some hints.
Please also don't hesitate to ask questions on Piazza or drop by
office hours!