Z3-Noodler

Z3-Noodler is an SMT solver for string constraints such as those that occur in symbolic execution and analysis of programs, reasoning about configuration files of cloud services and smart contracts, etc. Z3-Noodler is based on the SMT solver Z3 v4.13.0, in which it replaces the solver for the theory of strings. The core of the string solver implements several decision procedures, but mainly it relies on the equation stabilization algorithm (see Publications).

Z3-Noodler utilizes the automata library Mata for efficient representation of automata and their processing.

For a brief overview of the architecture, see SMT-COMP'24 Z3-Noodler description.

Building and running

Dependencies

1. The Mata library for efficient handling of finite automata. Minimum required version of mata is v1.6.10.

   git clone 'https://github.com/VeriFIT/mata.git'
   cd mata
   make release
   sudo make install

   Make sure your system looks for libraries in /usr/local/include (where Mata will be installed). For example, MacOS might skip looking for libraries there, so you might need to add these paths by running, for example xcode-select --install, as per a suggestion from StackOverflow.

Building Z3-Noodler

git clone 'https://github.com/VeriFIT/z3-noodler.git'
mkdir z3-noodler/build
cd z3-noodler/build
cmake -DCMAKE_BUILD_TYPE=Release ..
make

See instructions for building Z3 for more details.

To build tests for Z3-Noodler (assuming you have Catch2 version 3 installed), run the following command.

make test-noodler

Running Z3-Noodler

To run Z3-Noodler, use:

cd build/
./z3 <instance_file.smt2> 

If you want to get a model for sat instances (using get-model or get-value), you need to enable model generation:

cd build/
./z3 model=true <instance_file.smt2> 

To run tests for Z3-Noodler, execute

cd build/
./test-noodler

Limitations

The following functions/predicates of the SMTLIB Strings theory are not supported at the moment:

str.replace_all
str.replace_re_all

Furthermore, we do not support string variables as arguments of str.to_re and re.range.

Publications

• V. Havlena, L. Holík, O. Lengál, and J. Síč. Cooking String-Integer Conversions with Noodles. In Proc. of SAT'24, LIPIcs, Volume 305, pp. 14:1-14:19, 2024. Schloss Dagstuhl – Leibniz-Zentrum für Informatik.
• Y. Chen, D. Chocholatý, V. Havlena, L. Holík, O. Lengál, and J. Síč. Z3-Noodler: An Automata-based String Solver. In Proc. of TACAS'24, volume 14570 of LNCS, pages 24-33, 2024. Springer.
• Y. Chen, D. Chocholatý, V. Havlena, L. Holík, O. Lengál, and J. Síč. Solving String Constraints with Lengths by Stabilization. In Proc. of OOPSLA'23, Volume 7, Issue OOPSLA2, pages 2112–2141, 2023. ACM.
• F. Blahoudek, Y. Chen, D. Chocholatý, V. Havlena, L. Holík, O. Lengál, and J. Síč. Word Equations in Synergy with Regular Constraints. In Proc. of FM’23, volume 14000 of LNCS, pages 403–423, 2023. Springer.

Z3-Noodler source files

The string solver of Z3-Noodler is implemented in src/smt/theory_str_noodler.

Tests for Z3-Noodler are located in src/test/noodler.

Licensing

Z3-Noodler is licensed under the MIT License. See LICENSE.md.

Z3-Noodler is a derivative work of the SMT solver Z3. The original SMT solver Z3 from the Z3 repository is licensed under the MIT License. See LICENSE_Z3.txt.

Original Z3 README

For the original Z3 README, see README-Z3.md.

Authors

• ✉️ Vojtěch Havlena,
• ✉️ Juraj Síč,
• Yu-Fang Chen,
• David Chocholatý,
• Lukáš Holík,
• Ondřej Lengál.