Overview

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.

Download

How to compile

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
	make
The solver's compilation will require the presence of GNU Multiprecision Library (GMP). It is usually shipped with the distribution of Linux that you use.

In order to enable simplex parallelization, the configuration step above should be adjusted in the following way: 
	./configure --enable-hybrid-int-values --enable-parallel-simplex
In order to enable parallel portfolio, the configuration step above should be adjusted in the following way: 
	./configure --enable-hybrid-int-values --enable-parallel-portfolio
Finally, 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-portfolio
IMPORTANT: 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).

How to use

To use the (sequential) solver, it is best to run it in the following way: 

	./src/argosmt input_file.smt2
The solver accepts inputs in SMT-LIB 2.0 format (for supported theories, only).

In order to use the simplex parallelization described in the above paper, run the solver in the following way: 
	./src/argosmt -c config.cfg  input_file.smt2
where config.cfg is a configuration file with the following content: 
       number_of_threads = 4
(4 can be replaced with any other positive number).

In order to use the parallel portfolio, adjust the configuration file in the following way (example with 4 solvers): 
	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 = 25
Here, 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.

If you want to use the hybrid approach, just give more threads to the solver, as in the following example: 
	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 = 25
Now the total number of available threads is 32, giving each solver 8 threads on average for the simplex parallelization.

Option '-h' provides you with more information about the supported options.