s2s is an SMT solver for the quantifier-free theory of strings combined with linear integer arithmetic (QF_SLIA).
It encodes the problem into propositional logic and calls a SAT solver to check satisfiability.
It currently supports a limited fragment of the SMT-LIB Theory of Strings. More precisely, it supports:
- String terms that are variables, constant string, and concatenations thereof.
- All grounded regular expression that do not contain complements over anything but
re.range,str.to_re - Word equations: Atoms of the form
(= l r)wherelandrare string terms - Regular constraints: Atoms of the form
(str.in_re l R)wherelis a string term andRa regular expression - Linear arithmetic constraints: Atoms of the from
(<op> l r)wherelandrare linear integer terms over integer variables and string lengths, and<op>is one of<, <=,=, >=, >
The solver makes a best-effort to solve formulas containing unsupport constructs but can fail, in which case it returns unknown.
- Ensure that the Rust toolchain is installed.
- Install dependencies:
- On Ubuntu:
sudo apt-get install libssl-dev pkg-config libclang-dev - On MacOs:
brew install pkgconf openssl - Windows is currently not supported
- On Ubuntu:
- Clone the repository and build the project using
cargo build --release
The compiled binary will be located at target/release/s2s.
s2s [OPTIONS] <FILE><FILE>is the path to an SMT-LIB file (QF_SLIA).[OPTIONS]is a list of options. Available options can be obtained by runnings2s --help.
To run the solver on an SMT file, use
$ s2s res/tests_sat/regex_simp.smt2
satIn order to obtain a model (on SAT), use the --model option
$ s2s res/tests_sat/regex_simp.smt2
sat
(
(define-fun X () String "xeeeex")
)If the problem is unsat, then --model will print an error
$ s2s res/tests_unsat/levis_simp.smt2 --model
unsat
error: no model to getMore example problems are in res/tests_sat/ and rest/tests_unsat/.
Licensed under either of:
at your option.