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.15.1, 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.
-
The Mata library for efficient handling of finite automata. Minimum required version of
mataisv1.26.1.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 examplexcode-select --install, as per a suggestion from StackOverflow.
git clone 'https://github.com/VeriFIT/z3-noodler.git'
mkdir z3-noodler/build
cd z3-noodler/build
cmake -DCMAKE_BUILD_TYPE=Release ..
makeSee 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-noodlerTo 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-noodlerOther than the constraints defined in the SMT-LIB theory of strings, Z3-Noodler can handle the following functions:
(str.to_real String Real)
Converts a string representation of a (positive) real number to the corresponding number. The string representation can either be a positive integer with leading zeros (similarly as in str.to_int) or it can contain one decimal separator .. It evaluates to -1.0 otherwise.
Examples:
(str.to_real "4562")evaluates to4562.0(str.to_real "-4562")evaluates to-1.0(str.to_real "45.62")evaluates to45.62(str.to_real "00045.620000")evaluates to45.62(str.to_real "")evaluates to-1.0(str.to_real ".456")evaluates to0.456(str.to_real "8494.")evaluates to8494.0(str.to_real ".")evaluates to-1.0(str.to_real "4564a")evaluates to-1.0(str.to_real "4564e3")evaluates to-1.0
(str.from_real Real Int String)
Transforms a positive real number r to a string s with a corresponding number of decimal places n. If either n or r is negative, it evaluates to the empty string.
Examples:
(str.from_real 4.56 5)evaluates to"4.56000"(str.from_real 4.56 0)evaluates to"4"(str.from_real 4.56 1)evaluates to"4.5"(str.from_real -4.56 -5)evaluates to""(str.from_real -4.56 5)evaluates to""(str.from_real 4.56 -5)evaluates to""
- Y. Chen, V. Havlena, M.Hečko, L.Holík, and O. Lengál. A Uniform Framework for Handling Position Constraints in String Solving. In Proc. of PLDI'25, volume 9, pages 550-575, 2025. ACM.
- D. Chocholatý, V. Havlena, L. Holík, J. Hranička, O. Lengál, and J. Síč. Z3-Noodler 1.3: Shepherding Decision Procedures for Strings with Model Generation. In Proc. of TACAS'25, volume 15697 of LNCS, pages 23-44, 2025. Springer.
- 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.
The string solver of Z3-Noodler is implemented in src/smt/theory_str_noodler.
Tests for Z3-Noodler are located in src/test/noodler.
Z3-Noodler is licensed under the MIT License for general use (see LICENSE.md). However, use of this software, or any derivative work, as a participant in the SMT-COMP competition requires a separate Competition Use License from the copyright holder. For competitor licensing requests, contact the authors.
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.
For the original Z3 README, see README-Z3.md.