Parallel OpenSMT2

Overview

Parallel OpenSMT2 consists of a client-server architecture based on TCP/IP with the aim of solving SMT instances harnessing parallel computing.

The clients consist of OpenSMT2 processes called "workers". The workers are connected to a server that provides a problem to solve for each worker. The server takes several SMT instances as input and using various approaches, each instance is solved by spreading the solving task through the workers.

How to use

The server consist of a Python/2.7 program and each worker is an OpenSMT2 instance. Given that, the requirements are:

  • Python 2.7
  • C++ compiler capable of -std=gnu++11
  • automake 1.14

 

First, Download the OpenSMT2 development version and unzip it:

~$ unzip opensmt2parallel.zip
~$ cd opensmt2parallel/

Then run ./configure

~/opensmt2parallel$ ./configure

Then make

~/opensmt2parallel$ make

At this point, the opensmt2parallel folder will have, among others:

~/opensmt2parallel
    |- opensmt
    |- sample/
      |- README
      |- sample.sh
    |- test/
    |- wserver/
      |- command.py
      |- sserver.py

 

  • ./opensmt is the OpenSMT2 executable
  • ./sample/ is a folder containing a sample script that runs all the environment in a simple way, please read ./sample/README first, it contains all the instructions!
  • ./test/ is a folder containing some SMT-LIB test files
  • ./wserver is the server folder. It contains sserver.py (server) and command.py (command)