How to compile SMTS

 

SMTS: a framework for distributed SMT and PDR, supporting lemma sharing and partitioning

$ git clone https://scm.ti-edu.ch/repogit/smts.git

 

HOW TO GET STARTED

1) Download and install the dependencies

  • PDR: Z3-Spacer supporting lemma sharing

$ git clone -b p3 https://bitbucket.org/maresm/spacer
$ mkdir build; cd build; cmake ..; make -j8 install
  • SMT: OpenSMT2

$ git clone https://scm.ti-edu.ch/repogit/opensmt2.git
$ autoreconf --force --install
$ ./configure --enable-library
$ make -j8 install

 

2) Compile SMTS

$ cd smts
$ mkdir build; cd build; cmake ..; make -j8

Note 1: you can disable either SMT or PDR support by commenting the respective lines in: ./src/client/CMakeLists.txt

Note 2: If SMTS cmake script can't find lib or headers (e.g. you installed in non-standard folders), then use:

$ cmake -DOPENSMT2_DIR=<install_dir> -DZ3SPACER_DIR=<install_dir> ..

 

3) Configure SMTS

Copy the default "read-only" configuration file:

$ cp ./server/config/default.py ./server/config/config.py

Note 3: If SMTS is not compiled in ./build then change ./server/config/config.py variable build_path accordingly

Note 4: SMTS loads ./server/config/config.py automatically. However using -c, you can specify other configuration files that (partially) override options. 

 

4) Try SMTS locally

These might help:

$ ./smts.py --help
$ ./client.py --help

Examples:

The following command executes 4 OpenSMT processes with lemma sharing and enables the GUI:

$ ./smts.py -g -d test.db -o4 -l

The following command executes 4 Z3-Spacer processes with lemma sharing + storage and enables the GUI:

$ ./smts.py -g -d test.db -z4 -l -D

In both cases benchmarks are provided using:

$ ./client.py 3000 <benchmark-path>

To analyze a given database use:

$ ./utils.py -g <db-path>

To see the GUI open the browser at http://127.0.0.1:8080

 

Other links:

SMTS

P3 full experimental results from FMCAD 2017