rafaeltupynamba / smtsampler

SMTSampler: Efficient Stimulus Generation from Complex SMT Constraints

SMTSampler

SMTSampler: Efficient Stimulus Generation from Complex SMT Constraints

Paper

Update

You may also want to also check out our new project GuidedSampler, which is an extension of SMTSampler for coverage-guided sampling of solutions.

Building

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

Running

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.

Benchmarks

The benchmarks used come from SMT-LIB. They can be obtained from the following repositories.

QF_AUFBV QF_ABV QF_BV

Paper

ICCAD 2018 paper

SMTSampler: Efficient Stimulus Generation from Complex SMT Constraints

Rafael Dutra, Jonathan Bachrach, Koushik Sen

smtsampler's Issues

why an older version of z3 is asked?

I wonder why an older version of z3 is asked?
Is any change in new version disturb any part of sampling?
Thanks

Can't run make for SMTSampler

When I try to run make in the SMTSampler directory I get this error:

I have followed all the steps in the readme, what could the problem be?

Thank you!

Sample Interpretation.

Thanks for the sampler tool.
I had one query regarding the sample produced.
How do I interpret the sample? I wanted to know the value of each bit vector entry corresponding to the variables I have.

; benchmark generated from python API
(set-info :smt-lib-version 2.6)
(set-logic QF_AUFBV)

(declare-fun x1 () (_ BitVec 32))
(declare-fun x2 () (_ BitVec 32))
(declare-fun a1 () (_ BitVec 32))
(declare-fun y1 () (_ BitVec 32))
(declare-fun y2 () (_ BitVec 32))
(declare-fun n2 () (_ BitVec 32))
(declare-fun n1 () (_ BitVec 32))
(declare-fun a2 () (_ BitVec 32))
;; Loop body operations
(assert
 (= x2 (bvadd x1 (_ bv1 32))))
(assert
 (= y2 (bvadd y1 a1)))
;; Transfer across the loop body.
(assert
 (= n1 n2))
(assert
 (= a1 a2))
 ;; Inv(x1, y1, n1, a1) && (x1 <= n1) => Inv(x2, y2, n2, a2)
(assert
 (let (($x49 (and (= y2 (bvmul x2 a2)) (bvsle x2 n2))))
 (let (($x45 (and (and (= y1 (bvmul x1 a1)) (bvsle x1 n1)) (bvslt x1 n1))))
 (=> $x45 $x49))))
 ;; DataSet Constraints
 ;; n > 0, y != 0, x != 0, a > 0
(assert
 (bvsgt n1 (_ bv0 32)))
(assert
 (bvsgt a1 (_ bv0 32)))
(assert
 (and (distinct y1 (_ bv0 32)) true))
(assert
 (and (distinct x1 (_ bv0 32)) true))

(check-sat)
(exit)

This is the file and samples are

999ea4ca�999ea4c9�6c1f10c2�40466e40�2bd8a282�4e44df19�4e44df19�2bd8a282�
999ea4c9�999ea4c8�6c1f10c2�40466e40�2bd8a282�4e44df19�4e44df19�2bd8a282�
999ea4ce�999ea4cd�6c1f10c2�40466e40�2bd8a282�4e44df19�4e44df19�2bd8a282�
999ea4c2�999ea4c1�6c1f10c2�40466e40�2bd8a282�4e44df19�4e44df19�2bd8a282�
999ea4da�999ea4d9�6c1f10c2�40466e40�2bd8a282�4e44df19�4e44df19�2bd8a282�
999ea4ea�999ea4e9�6c1f10c2�40466e40�2bd8a282�4e44df19�4e44df19�2bd8a282�
999ea48a�999ea489�6c1f10c2�40466e40�2bd8a282�4e44df19�4e44df19�2bd8a282�
999ea44a�999ea449�6c1f10c2�40466e40�2bd8a282�4e44df19�4e44df19�2bd8a282�
999ea5ca�999ea5c9�6c1f10c2�40466e40�2bd8a282�4e44df19�4e44df19�2bd8a282�
999ea6ca�999ea6c9�6c1f10c2�40466e40�2bd8a282�4e44df19�4e44df19�2bd8a282�
999ea0ca�999ea0c9�6c1f10c2�40466e40�2bd8a282�4e44df19�4e44df19�2bd8a282�
999eacca�999eacc9�6c1f10c2�40466e40�2bd8a282�4e44df19�4e44df19�2bd8a282�
999eb4ca�999eb4c9�6c1f10c2�40466e40�2bd8a282�4e44df19�4e44df19�2bd8a282�
999e84ca�999e84c9�6c1f10c2�40466e40�2bd8a282�4e44df19�4e44df19�2bd8a282�
999ee4ca�999ee4c9�6c1f10c2�40466e40�2bd8a282�4e44df19�4e44df19�2bd8a282�
999e24ca�999e24c9�6c1f10c2�40466e40�2bd8a282�4e44df19�4e44df19�2bd8a282�
999fa4ca�999fa4c9�6c1f10c2�40466e40�2bd8a282�4e44df19�4e44df19�2bd8a282�
999ca4ca�999ca4c9�6c1f10c2�40466e40�2bd8a282�4e44df19�4e44df19�2bd8a282�
999aa4ca�999aa4c9�6c1f10c2�40466e40�2bd8a282�4e44df19�4e44df19�2bd8a282�
9996a4ca�9996a4c9�6c1f10c2�40466e40�2bd8a282�4e44df19�4e44df19�2bd8a282�
998ea4ca�998ea4c9�6c1f10c2�40466e40�2bd8a282�4e44df19�4e44df19�2bd8a282�
99bea4ca�99bea4c9�6c1f10c2�40466e40�2bd8a282�4e44df19�4e44df19�2bd8a282�
99dea4ca�99dea4c9�6c1f10c2�40466e40�2bd8a282�4e44df19�4e44df19�2bd8a282�
991ea4ca�991ea4c9�6c1f10c2�40466e40�2bd8a282�4e44df19�4e44df19�2bd8a282�
989ea4ca�989ea4c9�6c1f10c2�40466e40�2bd8a282�4e44df19�4e44df19�2bd8a282�
9b9ea4ca�9b9ea4c9�6c1f10c2�40466e40�2bd8a282�4e44df19�4e44df19�2bd8a282�
9d9ea4ca�9d9ea4c9�6c1f10c2�40466e40�2bd8a282�4e44df19�4e44df19�2bd8a282�
919ea4ca�919ea4c9�6c1f10c2�40466e40�2bd8a282�4e44df19�4e44df19�2bd8a282�
899ea4ca�899ea4c9�6c1f10c2�40466e40�2bd8a282�4e44df19�4e44df19�2bd8a282�
b99ea4ca�b99ea4c9�6c1f10c2�40466e40�2bd8a282�4e44df19�4e44df19�2bd8a282�
d99ea4ca�d99ea4c9�6c1f10c2�40466e40�2bd8a282�4e44df19�4e44df19�2bd8a282�
199ea4ca�199ea4c9�6c1f10c2�40466e40�2bd8a282�4e44df19�4e44df19�2bd8a282�
999ea4cc�999ea4cb�6c1f10c2�40466e40�2bd8a282�4e44df19�4e44df19�2bd8a282�
999ea4ca�999ea4c9�6c1f10c3�40466e41�2bd8a282�4e44df19�4e44df19�2bd8a282�
999ea4ca�999ea4c9�6c1f10c0�40466e40�2bd8a280�4e44df19�4e44df19�2bd8a280�
999ea4ca�999ea4c9�6c1f10c6�40466e44�2bd8a282�4e44df19�4e44df19�2bd8a282�
999ea4ca�999ea4c9�6c1f10ca�40466e48�2bd8a282�4e44df19�4e44df19�2bd8a282�
999ea4ca�999ea4c9�6c1f10d2�40466e50�2bd8a282�4e44df19�4e44df19�2bd8a282�
999ea4ca�999ea4c9�6c1f10e2�40466e60�2bd8a282�4e44df19�4e44df19�2bd8a282�
999ea4ca�999ea4c9�6c1f1082�40466e00�2bd8a282�4e44df19�4e44df19�2bd8a282�
999ea4ca�999ea4c9�6c1f1142�40466ec0�2bd8a282�4e44df19�4e44df19�2bd8a282�
999ea4ca�999ea4c9�6c1f11c2�40466f40�2bd8a282�4e44df19�4e44df19�2bd8a282�
999ea4ca�999ea4c9�6c1f12c2�40466c40�2bd8a682�4e44df19�4e44df19�2bd8a682�
999ea4ca�999ea4c9�6c1f14c2�40466e40�2bd8a682�4e44df19�4e44df19�2bd8a682�
999ea4ca�999ea4c9�6c1f08c2�40466640�2bd8a282�4e44df19�4e44df19�2bd8a282�
999ea4ca�999ea4c9�6c1f20c2�40467e40�2bd8a282�4e44df19�4e44df19�2bd8a282�
999ea4ca�999ea4c9�6c1f50c2�4046ae40�2bd8a282�4e44df19�4e44df19�2bd8a282�
999ea4ca�999ea4c9�6c1f90c2�4046ee40�2bd8a282�4e44df19�4e44df19�2bd8a282�
999ea4ca�999ea4c9�6c1e10c2�40456e40�2bd8a282�4e44df19�4e44df19�2bd8a282�
999ea4ca�999ea4c9�6c1d10c2�40446e40�2bd8a282�4e44df19�4e44df19�2bd8a282�

Error in Build SMTSampler

I followed all the steps of installation.

During Build SMTSampler
while running make I got this error.

g++ -g -std=c++11 -O3 -o smtsampler smtsampler.cpp -lz3
smtsampler.cpp:2:10: fatal error: z3++.h: No such file or directory
#include <z3++.h>
^~~~~~~~
compilation terminated.
Makefile:2: recipe for target 'all' failed
make: *** [all] Error 1

Do I need to include any Library Paths ?

Paper can not be found

When clicking on the link to the paper, one is redirected to the site https://people.eecs.berkeley.edu/~rtd/papers/SMTSampler.pdf which says "The server has encountered a problem because the resource was not found."

Question about formula.smt2

Thank you for this great work!
I notice this repository didn't provide a formula.smt2 presented in readme
If I wanna generate random x y in such constraints:

(set-info :status unknown)
(set-logic QF_LIA)
(declare-fun max () Int)
(declare-fun min () Int)
(declare-fun typ () Int)
(assert
 (let (($x21 (>= max 64)))
 (let (($x10 (= min 16)))
 (let (($x20 (and (< typ max) (> typ min) (< max 128))))
 (and $x20 $x10 $x21)))))
(check-sat)
(get-model)

What formula.smt2 is supposed to be?
I tried this file but it failed in
https://github.com/RafaelTupynamba/SMTSampler/blob/master/smtsampler.cpp#L226
I think my smt2 file is not correct for this usage.

Query while running the file

Hello,

Whenever I am running the file,
it is showing that could not read the input format.$ ./smtsampler -6 1000000 -10 3600.0 --smtbv formula.smt2.samples
null
Could not read input formula.
it is saying that the ast is null.
How do I have to give input to the file.

z3 error

Hi,
I was trying to use your tool and got this error when compling z3
Traceback (most recent call last):
File "scripts/mk_make.py", line 21, in
mk_makefile()
File "z3/scripts/mk_util.py", line 2674, in mk_makefile
c.mk_makefile(out)
File "z3/scripts/mk_util.py", line 1103, in mk_makefile
Component.mk_makefile(self, out)
File "z3/scripts/mk_util.py", line 1050, in mk_makefile
self.add_cpp_rules(out, include_defs, cppfile)
File "z3/scripts/mk_util.py", line 1007, in add_cpp_rules
self.add_rule_for_each_include(out, cppfile)
File "z3/scripts/mk_util.py", line 986, in add_rule_for_each_include
owner = self.find_file(include, fullname)
File "z3/scripts/mk_util.py", line 970, in find_file
raise MKException("Failed to find include file '%s' for '%s' when processing '%s'." % (fname, ownerfile, self.name))
mk_exception.MKException: "Failed to find include file 'api_context.h' for 'src/model/model.cpp' when processing 'model'."