SMTSampler: Efficient Stimulus Generation from Complex SMT Constraints
You may also want to also check out our new project GuidedSampler, which is an extension of SMTSampler for coverage-guided sampling of solutions.
Install dependencies
sudo apt install git g++ make python-minimal
Clone repos
git clone https://github.com/RafaelTupynamba/SMTSampler.git
git clone https://github.com/Z3Prover/z3.git
Build z3 (with a patch to compute the coverage of a formula)
cd z3
git checkout bb7ad4e938ec3ade23282142119e77c838b1f7d1
cp ../SMTSampler/z3-patch/mk_util.py scripts/mk_util.py
cp ../SMTSampler/z3-patch/rewriter_def.h src/ast/rewriter/rewriter_def.h
cp ../SMTSampler/z3-patch/model.cpp src/model/model.cpp
cp ../SMTSampler/z3-patch/permutation_matrix.h src/util/lp/permutation_matrix.h
python scripts/mk_make.py
cd build
make
sudo make install
cd ../..
Build SMTSampler
cd SMTSampler
make
Simply run with
./smtsampler -n 1000000 -t 3600.0 --smtbit formula.smt2
SMTSampler will create a file formula.smt2.samples with the samples generated and print statistics to standard output. The file formula.smt2.samples has one line for each produced sample. The first number represents the number of atomic mutations which were used to generate this sample. Then, the sample is displayed in a compact format.
The option -n can be used to specify the maximum number of samples produced and the option -t can be used to specify the maximum time allowed for sampling.
Three different strategies can be used for sampling, as described in the paper. With option --smtbit, we add one soft constraint for each bit inside a bit-vector. With option --smtbv, only one soft constraint is added for each bit-vector. Finally, option --sat encodes the SMT formula into SAT and performs the sampling over the converted SAT formula.
All the samples that SMTSampler outputs are valid solutions to the formula.
The benchmarks used come from SMT-LIB. They can be obtained from the following repositories.
SMTSampler: Efficient Stimulus Generation from Complex SMT Constraints
Rafael Dutra, Jonathan Bachrach, Koushik Sen