How to compile SMTS?


A framework for distributed SMT and PDR, supporting lemma sharing and partitioning

$ git clone https://github.com/usi-verification-and-security/SMTS.git --branch cube-and-conquer

 

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

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 -DCMAKE_INSTALL_PREFIX=${OPENSMT2_DIR} ..

cmake -DCMAKE_INSTALL_PREFIX=${Z3SPACER_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>

 

Other links: