Skip to main content

Setup

Platforms

Make sure you can access our course platforms. If any of these links do not work, email the course staff and we will resync the roster. Enrollment changes can take up to a day to be reflected across these systems.

Python + Z3

CARS uses Python with the Z3 solver library. This page walks you through a quick verification that your environment works. Each assignment will come with its own setup instructions and dependencies.

You will need:

Step 1: Install Python

macOS: Install via Homebrew (brew install python3) or download from python.org.

Windows: Download from python.org and run the installer. Check "Add Python to PATH" during installation.

Linux (Ubuntu/Debian): sudo apt install python3 python3-pip python3-venv

Verify your version:

python3 --version    # macOS/Linux
python --version     # Windows

You need 3.12 or later.

Step 2: Install Z3

Create a temporary directory and set up a virtual environment:

macOS / Linux:

mkdir cars-test
cd cars-test
python3 -m venv venv
source venv/bin/activate
pip install z3-solver

Windows (PowerShell):

mkdir cars-test
cd cars-test
python -m venv venv
venv\Scripts\Activate
pip install z3-solver

Your terminal prompt should show (venv) when the environment is active. Now verify Z3 is installed:

python -c "from z3 import *; print(f'Z3 version: {get_version_string()}')"

If you see a version number, Z3 is installed correctly.

Note: the package is called z3-solver, not z3. They are different packages.

Step 3: Your first solver problem

Create a file called hello.py with this content:

from z3 import *

x = Int('x')
y = Int('y')

s = Solver()
s.add(x + y == 10)
s.add(x - y == 4)

# does this set of constraints have a solution?
print(s.check())

# if so, what are x and y?
print(s.model())

Before you run it, think about what you expect. What values of x and y satisfy both equations? Now run it:

python hello.py

Now try a harder one. Create hello2.py:

from z3 import *

a = Int('a')
b = Int('b')
c = Int('c')

s = Solver()
s.add(a + b + c == 100)
s.add(a == 2 * b)
s.add(c == a + 10)

# can Z3 find values for a, b, and c?
print(s.check())
print(s.model())

Again, try to work it out in your head first. Then run it and see if Z3 agrees. You can delete the cars-test directory when you are done.

About virtual environments

Each assignment will have you create a virtual environment in the assignment directory. A virtual environment keeps each project's dependencies separate and avoids conflicts with your system Python. The pattern is always the same:

python3 -m venv venv        # create (once)
source venv/bin/activate    # activate (each new terminal)
pip install -r requirements.txt  # install dependencies (once)

You need to activate the environment each time you open a new terminal to work on an assignment.

Editor

We officially support VS Code. Install the Python extension, then select your virtual environment's Python interpreter. Open the Command Palette (Cmd+Shift+P on macOS, Ctrl+Shift+P on Windows/Linux) and run "Python: Select Interpreter", then choose the interpreter from your venv directory. You can also click the Python version in the bottom status bar.

Troubleshooting

If you run into problems during setup, here are the most common issues and fixes.

Z3 import fails

"ModuleNotFoundError: No module named 'z3'"

Make sure your virtual environment is activated (your prompt should show (venv)) and that you installed z3-solver, not z3. These are different packages. To fix:

source venv/bin/activate    # or venv\Scripts\Activate on Windows
pip install z3-solver

Cannot create virtual environment

"No module named venv"

On Ubuntu/Debian, the venv module needs to be installed separately:

sudo apt install python3-venv

pip blocked by system Python

"error: externally-managed-environment"

This means you are trying to install packages into your system Python. Modern Python requires a virtual environment. Create and activate one first (see Step 2 above).

pip not found

"pip: command not found"

Try using Python's built-in pip module instead:

python3 -m pip install z3-solver    # macOS/Linux
py -m pip install z3-solver         # Windows

Apple Silicon

pip install z3-solver works natively on M1/M2/M3/M4 Macs. No special steps needed.

Still stuck?

Post on Ed with your error message and OS, or come to office hours. As a temporary fallback while debugging your local setup, you can run Z3 in the browser via the Z3 online playground (SMT-LIB syntax only, not Python).