README

To report problems

If there is something that is not working or if you have questions on
RMT, please contact me at:

stefan.ciobaca@gmail.com.

Prerequisites

* A modern C++ compiler (a recent version of g++, clang or MSVC will do)
* git
* CMake
* Z3
	
Compilation

We list the exact steps for an Ubuntu machine.
Please adapt for use on Mac or Windows.

* Step 1: Install build-essential (g++) and cmake:

sudo apt install build-essential cmake

* Step 2: Clone the Z3 repository in ~/z3:

git clone https://github.com/Z3Prover/z3.git

* Step 3: Compile Z3 in ~/z3/build (4 parallel compilation processes):

cd z3
mkdir build
cd build
cmake ..
make -j 4
cd ../..

This step might take around 10 minutes, depending on your exact machine.
		
* Step 4: Clone the RMT repository in ~/rmt:

git clone https://github.com/ciobaca/rmt.git

* Step 5: Build RMT (links against Z3, previously compiled)

cd rmt
mkdir build
cd build
cmake .. -DZ3_DIR=~/z3/build
make -j 4
cd ../..

Step 6: running RMT:

cd rmt/examples/
~/rmt/build/rmt -v 0 example1.rmt

This will will rmt with verbosity 0 (lowest) on the given example.