ArgoSMT is an experimental SMT solver with integrated techniques for parallelization (the simplex algorithm parallelization and the parallel portfolio, as well as the hybridization of the two approaches). The author of the solver is Milan Banković, a member of the ARGO Group. The solver is released under the GNU GPL licence and, therefore, is a free software.
The solver currently supports EUF, LRA and LIA theories, as well as their combinations. Other theory solvers are also planned to be included in the future.
To compile the sequential solver (under Linux), you should run the following commands:
tar xzvf argosmt-5.21.tar.gz cd argosmt-5.21/ ./configure --enable-hybrid-int-values makeThe solver's compilation will require the presence of GNU Multiprecision Library (GMP). It is usually shipped with the distribution of Linux that you use.
./configure --enable-hybrid-int-values --enable-parallel-simplexIn order to enable parallel portfolio, the configuration step above should be adjusted in the following way:
./configure --enable-hybrid-int-values --enable-parallel-portfolioFinally, in order to enable the combination of both parallel simplex and parallel portfolio, configure the solver in the following way:
./configure --enable-hybrid-int-values --enable-parallel-simplex --enable-parallel-portfolioIMPORTANT: In order to compile the solver with the parallelization capabilities included, you must have TBB library installed on your system (you can download it from here).
To use the (sequential) solver, it is best to run it in the following way:
./src/argosmt input_file.smt2The solver accepts inputs in SMT-LIB 2.0 format (for supported theories, only).
./src/argosmt -c config.cfg input_file.smt2where config.cfg is a configuration file with the following content:
number_of_threads = 4(4 can be replaced with any other positive number).
number_of_solvers = 4 number_of_threads = 4 randomize_decide = yes random_decides_percent = 0.05 random_seed[0] = 1 random_seed[1] = 2 random_seed[2] = 3 random_seed[3] = 4 share_size_limit = 25Here, share_size_limit is the maximal length of learnt clauses to be shared between the solvers (the value 0 means "no cooperation"). random_seed[i] is the seed used by ith solver (solvers are indexed from 0 to n-1, where n is the number of solvers). Other options are self-explaining.
number_of_solvers = 4 number_of_threads = 32 randomize_decide = yes random_decides_percent = 0.05 random_seed[0] = 1 random_seed[1] = 2 random_seed[2] = 3 random_seed[3] = 4 share_size_limit = 25Now the total number of available threads is 32, giving each solver 8 threads on average for the simplex parallelization.