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>
