You will need to have Z3 installed; see Homework 0.
To double check, run z3 --version, you should get something like:
Z3 version 4.15.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 Gradescope. You can find the Gradescope link through Canvas. Please see this Piazza post for further important instructions on submitting your files.
Like HW1, there are three parts to the assignment:
- Part 1 is a series of mini exercises.
- Part 2 is a solver for a "four numbers" guessing game: guess two numbers given a list of their sum, difference, product, and quotient.
- Part 3 explores some of the limitations of Z3.
Part 1 contains a small extra credit question.
We have provided 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!