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.

Getting Started

CARS uses Python with the Z3 solver library, and distributes course code through a Git repository. This page walks you through the initial setup.

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: Clone the course repo

All course code lives in one repository. Clone it and move into the directory:

git clone https://gitlab.cs.washington.edu/cars-26sp/cars-26sp-public.git
cd cars-26sp-public

You will run git pull at the start of each week to get new lecture code and assignments as they are released.

Step 3: Set up your environment

Create a virtual environment and install dependencies:

macOS / Linux:

python3 -m venv venv
source venv/bin/activate
pip install -r requirements.txt

Windows (PowerShell):

python -m venv venv
venv\Scripts\Activate
pip install -r requirements.txt

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 working. Now run the setup test:

python setup/hello.py

You should see:

sat
[y = 3, x = 7]

If you do, your environment is ready.

About virtual environments

A virtual environment keeps your course dependencies separate from your system Python. You created one in Step 3. You need to activate it each time you open a new terminal to work on course code:

source venv/bin/activate    # macOS/Linux
venv\Scripts\Activate       # Windows

See the Python venv documentation for more details.

Editor

We officially support VS Code. Install the Python extension.

Open the course repo folder in VS Code (File > Open Folder) and 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. Make sure you activated the virtual environment first (see Step 3 above).

pip not found

"pip: command not found"

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

python3 -m pip install -r requirements.txt    # macOS/Linux
py -m pip install -r requirements.txt         # Windows

VS Code does not find the virtual environment

Make sure you opened the course repo folder in VS Code (File > Open Folder), not an individual file. VS Code needs the folder open to detect the venv directory. After opening the folder, run "Python: Select Interpreter" from the Command Palette and choose the interpreter from venv.

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).