This repository provide all the necessary material
for the practical session of SETI Master - AI section.

The main file is a jupyter notebook `code/tutorial.ipynb`, slides for the first
part of the tutorial are under `doc/slides.pdf`.

There are several dependancies to install.

# Getting started
* We suppose python3.9 is installed and pip
* First we can move into code folder
  ```
  cd code
  ```
* We recommend creating a dedicated environment for the tutorial, using for instance virtualenv. If virtualenv is not installed run:
  ```
  python3.9 -m pip install virtualenv
  ```
  Afterwards you can create the virtualenv using:
  ```
  virtualenv ~/.virtualenvs/tuto_seti
  ```
  consider adding `-p /usr/bin/python3.9` pointing to your python version if you have multiple python installed.
  Then activate the environment using 
  ```
  source ~/.virtualenvs/tuto_seti/bin/activate
  ```

* Once in this venv, we can install python dependencies needed for this tutorial with :
  ```
  jupyter notebook tutorial.ipynb
  ```

# Tools installation

* **Z3**: your linux distribution should have a package (named z3):
  ```
  sudo apt install z3
  ```
  Otherwise check [here](https://github.com/Z3Prover/z3) for a detailed installation instruction 


* **ISAIEH** can be found compiled in the `bin` folder.

* **Marabou** can be found compiled in the `bin` folder.

* **PyRAT** comes as a precompiled binary in this repository that requires Python 3.9

When everything is installed, `jupyter notebook tutorial.ipynb` should open the tutorial notebook in your web browser.

## In case compiled version does not work

* **ISAIEH**: The next is to install dependencies for ISAIEH, which we will use:
  * install the ocaml opam build system with:
  ```
  sudo apt install opam
  ```
  * Additional system dependencies with `m4` and `gmp` are needed at minimum.
  Install them using 
  ```
  sudo apt install m4 libgmp3-dev
  ```
  on a Debian-like.
  * Finally we can install ISAIEH with 
  ```
  git clone https://git.frama-c.com/pub/isaieh.git && cd isaieh && opam init --disable-sandboxing && opam install -y . && eval $(opam env) && dune build
  ```

* **Marabou** can be compiled from [source](https://github.com/NeuralNetworkVerification/Marabou) using:
  ```
  sudo apt install cmake libboost-all-dev
  ```
  ```
  git clone https://github.com/NeuralNetworkVerification/Marabou
  cd Marabou
  mkdir build
  cd build
  cmake ..
  cmake --build .
  ```
  If this does not work an older version binary can be downloaded with
  ```
  wget https://aisafety.stanford.edu/marabou/marabou-1.0-x86_64-linux.zip
  ```

### Authors
- Augustin Lemesle
- Julien Girard-Satabin
- Guillaume Charpiat
- Zakaria Chihani
- Marc Schoenauer