mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-07-15 11:35:42 +00:00
Code Activity
z3/src/api
History
Copilot b1aa1e6ddc
Add z3regex Python module to translate Python regex syntax into Z3 regular expressions (#10095) 
This PR adds a first-class Python API helper for expressing regex
constraints in familiar Python regex syntax and translating them into Z3
regex terms. The translator is implemented as a separate module
(`z3regex.py`) as requested, keeping regex conversion logic isolated
from core API files.

- **New Python regex translator module**
  - Adds `src/api/python/z3/z3regex.py`.
- Introduces `regex_to_re(pattern, flags=0, ctx=None)` to convert parsed
Python regex constructs into Z3 regex expressions.
- Supports core regular constructs (literals, classes/ranges,
alternation, grouping, quantifiers, categories, wildcard).
- Raises `NotImplementedError` for unsupported non-regular constructs
(e.g., features outside regular languages).

- **API/package integration**
  - Exposes the module via `src/api/python/z3/__init__.py`.
- Includes `z3/z3regex.py` in Python binding file copy/install flow in
`src/api/python/CMakeLists.txt`.

- **Doctest entrypoint support**
- Extends `src/api/python/z3test.py` with `z3regex` mode so translator
doctests can be run consistently with existing Python API doctest flows.

```python
from z3 import *
from z3.z3regex import regex_to_re

x = String("x")
r = regex_to_re(r"(ab|cd)+\d{2}")

s = Solver()
s.add(InRe(x, r))
```

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
2026-07-12 18:26:59 -07:00
..
c++ Fixes necessary to compile z3 included in clang-tidy via FetchContents. (#9768) 2026-06-08 19:44:01 -07:00
dll
dotnet Fix .NET API memory leak: NativeContext finalizer, delegate lifetime, GC memory pressure (#10090) 2026-07-11 21:15:36 -07:00
go Go bindings: enable concurrent dec_ref for GC-driven finalizers (#10002) 2026-06-29 13:14:41 -06:00
java fix build warnings 2026-06-22 18:20:23 -07:00
js Bump markdown-it from 14.1.0 to 14.2.0 in /src/api/js (#9881) 2026-06-16 11:34:20 -06:00
julia fix issues 1-10: add missing API bindings across Go, Julia, TypeScript, OCaml, and Java (#9432) 2026-05-04 09:29:47 -07:00
mcp remove non-working ts mcp server, settle with python variant 2025-04-18 10:10:12 -07:00
ml Expose Seq.mk_re_diff in ocaml bindings (#9584) 2026-05-21 10:29:08 -07:00
python Add z3regex Python module to translate Python regex syntax into Z3 regular expressions (#10095) 2026-07-12 18:26:59 -07:00
api_algebraic.cpp Remove unnecessary semicolons (Attempt 2) (#10020) 2026-07-02 12:47:29 -07:00
api_arith.cpp Remove unnecessary semicolons (Attempt 2) (#10020) 2026-07-02 12:47:29 -07:00
api_array.cpp Remove unnecessary semicolons (Attempt 2) (#10020) 2026-07-02 12:47:29 -07:00
api_ast.cpp Remove unnecessary semicolons (Attempt 2) (#10020) 2026-07-02 12:47:29 -07:00
api_ast_map.cpp Remove unnecessary semicolons (Attempt 2) (#10020) 2026-07-02 12:47:29 -07:00
api_ast_map.h booyah 2020-07-04 15:56:30 -07:00
api_ast_vector.cpp Remove unnecessary semicolons (Attempt 2) (#10020) 2026-07-02 12:47:29 -07:00
api_ast_vector.h Remove unnecessary semicolons (Attempt 2) (#10020) 2026-07-02 12:47:29 -07:00
api_bv.cpp Remove unnecessary semicolons (Attempt 2) (#10020) 2026-07-02 12:47:29 -07:00
api_config_params.cpp Remove unnecessary semicolons (Attempt 2) (#10020) 2026-07-02 12:47:29 -07:00
api_context.cpp Remove unnecessary semicolons (Attempt 2) (#10020) 2026-07-02 12:47:29 -07:00
api_context.h Remove unnecessary semicolons (Attempt 2) (#10020) 2026-07-02 12:47:29 -07:00
api_datalog.cpp Remove unnecessary semicolons (Attempt 2) (#10020) 2026-07-02 12:47:29 -07:00
api_datalog.h Remove unnecessary semicolons (Attempt 2) (#10020) 2026-07-02 12:47:29 -07:00
api_datatype.cpp Remove unnecessary semicolons (Attempt 2) (#10020) 2026-07-02 12:47:29 -07:00
api_finite_set.cpp Remove unnecessary semicolons (Attempt 2) (#10020) 2026-07-02 12:47:29 -07:00
api_fpa.cpp Remove unnecessary semicolons (Attempt 2) (#10020) 2026-07-02 12:47:29 -07:00
api_goal.cpp Remove unnecessary semicolons (Attempt 2) (#10020) 2026-07-02 12:47:29 -07:00
api_goal.h Remove empty leaf destructors. (#6211) 2022-07-30 10:07:03 +01:00
api_log.cpp api: avoid some string copies when using mk_external_string 2024-12-28 09:42:54 +00:00
api_model.cpp Remove unnecessary semicolons (Attempt 2) (#10020) 2026-07-02 12:47:29 -07:00
api_model.h Remove empty leaf destructors. (#6211) 2022-07-30 10:07:03 +01:00
api_numeral.cpp Remove unnecessary semicolons (Attempt 2) (#10020) 2026-07-02 12:47:29 -07:00
api_opt.cpp Remove unnecessary semicolons (Attempt 2) (#10020) 2026-07-02 12:47:29 -07:00
api_params.cpp Remove unnecessary semicolons (Attempt 2) (#10020) 2026-07-02 12:47:29 -07:00
api_parsers.cpp add py_value to selected classes in python bindings, add mode for input-assertion based lookahead solving 2025-01-04 13:40:49 -08:00
api_pb.cpp Remove unnecessary semicolons (Attempt 2) (#10020) 2026-07-02 12:47:29 -07:00
api_polynomial.cpp Remove unnecessary semicolons (Attempt 2) (#10020) 2026-07-02 12:47:29 -07:00
api_polynomial.h remove a hundred implicit constructors/destructors 2021-05-23 14:25:01 +01:00
api_qe.cpp filter out terms that are not solved 2025-04-30 09:40:45 -07:00
api_quant.cpp Remove unnecessary semicolons (Attempt 2) (#10020) 2026-07-02 12:47:29 -07:00
api_rcf.cpp Remove unnecessary semicolons (Attempt 2) (#10020) 2026-07-02 12:47:29 -07:00
api_seq.cpp Remove unnecessary semicolons (Attempt 2) (#10020) 2026-07-02 12:47:29 -07:00
api_solver.cpp Remove unnecessary semicolons (Attempt 2) (#10020) 2026-07-02 12:47:29 -07:00
api_solver.h add API for creating and attaching simplifiers 2023-01-31 17:06:03 -08:00
api_special_relations.cpp Remove unnecessary semicolons (Attempt 2) (#10020) 2026-07-02 12:47:29 -07:00
api_stats.cpp Remove unnecessary semicolons (Attempt 2) (#10020) 2026-07-02 12:47:29 -07:00
api_stats.h Remove empty leaf destructors. (#6211) 2022-07-30 10:07:03 +01:00
api_tactic.cpp Remove unnecessary semicolons (Attempt 2) (#10020) 2026-07-02 12:47:29 -07:00
api_tactic.h add API for creating and attaching simplifiers 2023-01-31 17:06:03 -08:00
api_util.h Remove unnecessary semicolons (Attempt 2) (#10020) 2026-07-02 12:47:29 -07:00
CMakeLists.txt Fixes necessary to compile z3 included in clang-tidy via FetchContents. (#9768) 2026-06-08 19:44:01 -07:00
z3.h z3.h: Don't include stdio.h (#7014) 2023-11-24 16:46:32 +01:00
z3_algebraic.h fix grouping for latest doxygen (#5626) 2021-10-27 23:46:31 +02:00
z3_api.h Fix documentation for Z3_solver_to_dimacs_string (#9053) 2026-03-20 10:18:13 -07:00
z3_ast_containers.h fix grouping for latest doxygen (#5626) 2021-10-27 23:46:31 +02:00
z3_fixedpoint.h Added function to select the next variable to split on (User-Propagator) (#6096) 2022-06-19 10:49:25 -07:00
z3_fpa.h Return sign from Z3_fpa_get_numeral_sign as bool instead of int (#8047) 2026-02-18 20:56:01 -08:00
z3_logger.h Make sure all headers do #pragma once. (#6188) 2022-07-23 10:41:14 -07:00
z3_macros.h Make sure all headers do #pragma once. (#6188) 2022-07-23 10:41:14 -07:00
z3_optimization.h Implement Z3_optimize_translate for context translation (#8072) 2026-02-18 20:56:58 -08:00
z3_polynomial.h fix grouping for latest doxygen (#5626) 2021-10-27 23:46:31 +02:00
z3_private.h remove '#include <iostream>' from headers and from unneeded places 2022-06-17 14:10:19 +01:00
z3_rcf.h Return bool instead of int from Z3_rcf_interval (#8046) 2026-02-18 20:56:01 -08:00
z3_replayer.cpp Fix clang warnings about casting away const. (#9933) 2026-06-23 19:57:46 -06:00
z3_replayer.h Return sign from Z3_fpa_get_numeral_sign as bool instead of int (#8047) 2026-02-18 20:56:01 -08:00
z3_spacer.h add projection with witnesses 2024-11-27 10:26:34 -08:00
z3_v1.h booyah 2020-07-04 15:56:30 -07:00