SAT/SMT Summer School 2014

Tutorial Assignments

[School home page] [Home directories] [General information] [Tools] [Backup Policy] [Forgot Your Password?]

Personal Home Directories

A personal home directory will be automatically created for all students registered for the course. The directory is accessible using an URL of the form

https://puzzle.ics.hut.fi/SATSMT-2014/students/id/

where id is your account of the form guestXYZ. In addition to the URL above, you have to know your password that is given to you at the school. If you have not received them, please contact the staff.

Back to menu.

General Information

Back to menu.

Tools and Tutorials

See the school home page for the school program and locations.

As our SAT/SMT solver in tutorials, we will use Z3 developed at Microsoft through its Python interface.

Installing and using Python

You should have the Python programming language version 2.7.X (not 3.X.X) installed in your machine. If not, please follow these instructions and be sure to download the correct version (currently 2.7.6, not any 3.X.X). For writing Python code you can use any text editor, and then use shell commands to run the code. If you prefer to use your favorite IDE with Python support instead, you are free to do so.

If you are unfamiliar with Python, you can have a look at for example the official Python tutorial. Particularly list comprehensions are useful with Z3.

Installing and using Z3

The easiest way to start using Z3 is to install the precompiled nightly build version by following the instructions found here (see the section on supported platforms). If this does not work, e.g., due to versions of libraries, it is also quite straightforward to compile Z3 from the respective source package. Note that for a 64-bit Z3 installation you should have the 64-bit Python interpreter, and similarly for 32-bit.

What remains is to ensure that the Python interpreter can find Z3 by setting path variables appropriately:

After installing Python and Z3, test your installation with this small Z3 "Hello world" example. Have a look at the Python Z3 tutorial. This is a non-interactive version of the temporarily unavailable tutorial in http://rise4fun.com/z3py.

Python support for Eclipse IDE (optional)

Eclipse users can use the PyDev plugin. For system requirements and more detailed instructions, see the download page. Basically, you just select "Help -> Install new software ..." in Eclipse, enter http://pydev.org/updates in the "Work with:" field, and then mark and install "PyDev".

After this, follow the instructions in PyDev's manual page to configure the Python interpreter. Basically, select window -> Preferences -> PyDev in left side menu -> Interpreter - Python, click New and enter the path for your Python interpreter, typically /usr/bin/python in Linux. If you have multiple versions of Python in your machine, make sure that language version 2.7 is supported.

When creating new projects for the assignments, use "PyDev project". Then right click the project, choose "Properties", PyDev - PYTHONPATH in the left side menu, "External libraries", "Add source folder" and include the "bin" or "build" directory in the Z3 installation directory.

To import source files from the assignments, use "Import" -> "General" -> "File system" and then include the assignment directory and mark the source files there.

To run Python code, select the source file, right mouse click, and "Run as" with "Python Run"

Back to menu.

Backup Policy

You are responsible for maintaining backups of your answers.

Back to menu.