mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-06-20 23:50:25 +00:00
Code Activity
z3/src/ast
History
Margus Veanes 8c8e0d5673 Treat each transition-regex leaf as a single bisimulation state (#9871) 
## Summary

egex_bisim::collect_leaves used to descend through `re.union` and
`re.antimirov_union` at the top of each leaf of the transition regex,
splitting a single bisimulation state into multiple states before they
were merged into the union-find. This contradicts the bisimulation
invariant: **each leaf of a t-regex represents one state, regardless of
its top-level shape**. The fix descends into `ite` only (which is the
actual structural splitter of guarded transitions).

## Why it matters

The split happens to be *sound* for the current algorithm when the goal
is asserting `L(union(A, B)) = empty` (since `L(A) = empty AND L(B) =
empty` is equivalent), but it:

1. Adds spurious merges to the union-find that distort state-class
identities.
2. Slows convergence on hard equivalence queries (and causes early
timeouts in practice).
3. Creates latent unsoundness risk for any extension that interprets
leaves more semantically (XOR pair handling, classical-flag propagation,
future antimirov re-enable, etc.).

## Empirical validation

Run on the 1523-file regex-equivalence corpus, 5s/file timeout, 8
workers:

| metric | pre-fix master | post-fix |
|---|---|---|
| sat | 1008 | 1014 |
| unsat | 368 | 368 |
| timeout | 145 | 139 |
| unknown | 2 | 2 |
| SAT↔UNSAT verdict flips | — | **0** |
| timeout→sat flips | — | 6 |
| commonly-solved wall ratio | 1.000x | **0.902x** |

The 6 `timeout` → `sat` cases all return the *same* `sat` under
pre-fix master if given 60s; they are previously-slow cases not
previously-wrong ones.

Z3 unit tests: 89/89 pass (`test-z3 /a`).

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
2026-06-19 17:36:13 -07:00
..
converters Remove redundant explicit default constructors (#8470) 2026-02-18 20:58:01 -08:00
euf Remove redundant min_gen_match search (#9696) 2026-06-03 13:36:51 -07:00
fpa Fix soundness bug in fpa2bv mk_to_real: wrong exponent power for negative exponents (#9513) 2026-05-13 06:11:36 -04:00
macros Add std::initializer_list overloads for update_quantifier and update call sites 2026-02-18 21:02:26 -08:00
normal_forms disable test in tptp, move to native lambdas 2026-06-02 10:38:51 -07:00
pattern disable test in tptp, move to native lambdas 2026-06-02 10:38:51 -07:00
proofs Refactor mk_and/mk_or call sites to use vector overloads (#8286) 2026-02-18 20:57:52 -08:00
rewriter Treat each transition-regex leaf as a single bisimulation state (#9871) 2026-06-19 17:36:13 -07:00
simplifiers disable test in tptp, move to native lambdas 2026-06-02 10:38:51 -07:00
sls Add OP_RE_XOR and union-find bisimulation for ground regex equivalence (#9804) 2026-06-10 14:58:20 -07:00
substitution replace some copies with moves 2026-02-18 21:02:17 -08:00
act_cache.cpp Fix static analysis findings: uninitialized vars, bitwise shift UB, garbage values 2026-03-02 00:13:55 +00:00
act_cache.h
arith_decl_plugin.cpp Standardize for-loop increments to prefix form (++i) (#8199) 2026-02-18 20:57:29 -08:00
arith_decl_plugin.h Fix build warnings: cast size_t to unsigned in arith_decl_plugin.h and bv_decl_plugin.h 2026-02-18 20:58:07 -08:00
array_decl_plugin.cpp Add SMT-LIB choice support via array OP_CHOICE and instantiate choice axioms in array solvers (#9649) 2026-05-27 10:05:06 -07:00
array_decl_plugin.h [code-simplifier] Align choice axiom naming in theory_array_full (#9660) 2026-06-01 16:03:42 -07:00
array_peq.cpp code simplification 2025-02-18 19:07:58 -08:00
array_peq.h code simplification 2025-02-18 19:07:58 -08:00
ast.cpp disable test in tptp, move to native lambdas 2026-06-02 10:38:51 -07:00
ast.h disable test in tptp, move to native lambdas 2026-06-02 10:38:51 -07:00
ast_ll_pp.cpp Fix quoting in low-level pretty printer (#9716) 2026-06-04 15:48:27 -07:00
ast_ll_pp.h
ast_lt.cpp Fix static analysis issues: null dereferences, unsafe casts, branch clones, uninitialized members (#9424) 2026-04-29 13:37:11 -07:00
ast_lt.h
ast_pp.h Reapply PR #8190: Replace std::ostringstream with C++20 std::format (#8204) 2026-02-18 20:57:30 -08:00
ast_pp_dot.cpp Fix static analysis issues: null dereferences, unsafe casts, branch clones, uninitialized members (#9424) 2026-04-29 13:37:11 -07:00
ast_pp_dot.h
ast_pp_util.cpp fixes to mbqi in the new core based on #6575 2023-02-10 16:56:06 -08:00
ast_pp_util.h wip - proof hints 2022-10-08 20:12:57 +02:00
ast_printer.cpp
ast_printer.h Use = default for virtual constructors. 2022-08-05 18:11:46 +03:00
ast_smt2_pp.cpp Standardize for-loop increments to prefix form (++i) (#8199) 2026-02-18 20:57:29 -08:00
ast_smt2_pp.h patch definitions, add pretty print support 2025-10-13 22:39:32 +02:00
ast_smt_pp.cpp Handle choice_k in SMT pretty-printer switch to remove macOS -Wswitch warning (#9734) 2026-06-06 11:37:56 -07:00
ast_smt_pp.h
ast_trail.h remove default destructors 2024-10-02 22:20:12 +01:00
ast_translation.cpp disable test in tptp, move to native lambdas 2026-06-02 10:38:51 -07:00
ast_translation.h
ast_util.cpp Fix static analysis issues: null dereferences, unsafe casts, branch clones, uninitialized members (#9424) 2026-04-29 13:37:11 -07:00
ast_util.h Standardize for-loop increments to prefix form (++i) (#8199) 2026-02-18 20:57:29 -08:00
bv_decl_plugin.cpp recognize ubv_to_int as part of BV logic 2026-05-27 13:08:54 -07:00
bv_decl_plugin.h delete dead code 2026-02-18 21:02:30 -08:00
char_decl_plugin.cpp Typo Fixes (#6803) 2023-07-09 11:56:10 -07:00
char_decl_plugin.h Typo Fixes (#6803) 2023-07-09 11:56:10 -07:00
CMakeLists.txt v1 of term enumeration 2026-06-11 14:24:08 -07:00
cost_evaluator.cpp
cost_evaluator.h
datatype_decl_plugin.cpp address #8376 2026-02-18 20:57:58 -08:00
datatype_decl_plugin.h Subterms Theory (#8115) 2026-02-18 20:57:12 -08:00
decl_collector.cpp Standardize for-loop increments to prefix form (++i) (#8199) 2026-02-18 20:57:29 -08:00
decl_collector.h fixes to mbqi in the new core based on #6575 2023-02-10 16:56:06 -08:00
display_dimacs.cpp Standardize for-loop increments to prefix form (++i) (#8199) 2026-02-18 20:57:29 -08:00
display_dimacs.h
dl_decl_plugin.cpp Adopt std::optional for try_get_value and try_get_size functions (#8268) 2026-02-18 20:57:50 -08:00
dl_decl_plugin.h Adopt std::optional for try_get_value and try_get_size functions (#8268) 2026-02-18 20:57:50 -08:00
expr2polynomial.cpp Standardize for-loop increments to prefix form (++i) (#8199) 2026-02-18 20:57:29 -08:00
expr2polynomial.h remove default destructors 2024-10-02 22:20:12 +01:00
expr2var.cpp Centralize and document TRACE tags using X-macros (#7657) 2025-05-28 14:31:25 +01:00
expr2var.h
expr_abstract.cpp Centralize and document TRACE tags using X-macros (#7657) 2025-05-28 14:31:25 +01:00
expr_abstract.h wip - throttle AC completion, enable congruences over bound bodies 2025-07-11 12:48:27 +02:00
expr_delta_pair.h Remove redundant default constructors when they're the only constructor (#8461) 2026-02-18 20:58:01 -08:00
expr_functors.cpp
expr_functors.h Use = default for virtual constructors. 2022-08-05 18:11:46 +03:00
expr_map.cpp
expr_map.h
expr_stat.cpp Refactor expr_stat to use structured bindings for traversal pairs (#8441) 2026-02-18 20:58:00 -08:00
expr_stat.h Remove redundant default constructors when they're the only constructor (#8461) 2026-02-18 20:58:01 -08:00
expr_substitution.cpp bugfix to elim_uncnstr to ensure nodes are created. Prepare smt_internalizer to replay unit literals 2024-12-04 15:32:15 -08:00
expr_substitution.h wip - testing solve-eqs2, added as tactic 2022-11-05 22:42:59 -07:00
finite_set_decl_plugin.cpp Code simplifications for finite set plugin 2026-02-21 02:08:04 +00:00
finite_set_decl_plugin.h Code simplifications for finite set plugin 2026-02-21 02:08:04 +00:00
for_each_ast.cpp Standardize for-loop increments to prefix form (++i) (#8199) 2026-02-18 20:57:29 -08:00
for_each_ast.h Standardize for-loop increments to prefix form (++i) (#8199) 2026-02-18 20:57:29 -08:00
for_each_expr.cpp remove unneeded iterator functions 2024-09-23 12:59:04 +01:00
for_each_expr.h Standardize for-loop increments to prefix form (++i) (#8199) 2026-02-18 20:57:29 -08:00
format.cpp fix #6530 2023-01-10 13:43:17 -08:00
format.h
fpa_decl_plugin.cpp Standardize for-loop increments to prefix form (++i) (#8199) 2026-02-18 20:57:29 -08:00
fpa_decl_plugin.h remove default destructors 2024-10-02 22:20:12 +01:00
func_decl_dependencies.cpp
func_decl_dependencies.h
has_free_vars.cpp fixup std-order / inv-order 2024-10-03 19:35:16 -07:00
has_free_vars.h
is_variable_test.h
justified_expr.h move from justified_expr to dependent_expr by aligning datatypes 2025-01-22 11:46:10 -08:00
macro_substitution.cpp
macro_substitution.h
num_occurs.cpp Standardize for-loop increments to prefix form (++i) (#8199) 2026-02-18 20:57:29 -08:00
num_occurs.h
occurs.cpp AIX compat (#8113) 2026-02-18 20:57:04 -08:00
occurs.h #6805 2023-07-11 09:41:29 -07:00
pb_decl_plugin.cpp
pb_decl_plugin.h
polymorphism_inst.cpp Remove copies (#8583) 2026-02-18 21:02:22 -08:00
polymorphism_inst.h wip - alpha support for polymorphism 2023-07-12 18:09:02 -07:00
polymorphism_util.cpp Implement finite_set_decl_plugin with complete operator support and polymorphism infrastructure (#7961) 2025-10-13 10:58:53 +02:00
polymorphism_util.h Implement finite_set_decl_plugin with complete operator support and polymorphism infrastructure (#7961) 2025-10-13 10:58:53 +02:00
pp.cpp Standardize for-loop increments to prefix form (++i) (#8199) 2026-02-18 20:57:29 -08:00
pp.h
pp_params.pyg print lemmas2console faster 2023-03-20 17:07:04 +01:00
quantifier_stat.cpp
quantifier_stat.h
recfun_decl_plugin.cpp fix #9234 2026-04-23 13:54:09 -07:00
recfun_decl_plugin.h remove default destructors 2024-10-02 22:20:12 +01:00
recurse_expr.h
recurse_expr_def.h Standardize for-loop increments to prefix form (++i) (#8199) 2026-02-18 20:57:29 -08:00
reg_decl_plugins.cpp Implement finite_set_decl_plugin with complete operator support and polymorphism infrastructure (#7961) 2025-10-13 10:58:53 +02:00
reg_decl_plugins.h
scoped_proof.h overhaul of proof format for new solver 2022-08-28 17:44:33 -07:00
seq_decl_plugin.cpp Add OP_RE_XOR and union-find bisimulation for ground regex equivalence (#9804) 2026-06-10 14:58:20 -07:00
seq_decl_plugin.h Add OP_RE_XOR and union-find bisimulation for ground regex equivalence (#9804) 2026-06-10 14:58:20 -07:00
shared_occs.cpp
shared_occs.h cleanup 2022-11-24 22:46:35 +07:00
special_relations_decl_plugin.cpp add EUF plugin framework. 2023-11-30 13:58:30 -08:00
special_relations_decl_plugin.h add EUF plugin framework. 2023-11-30 13:58:30 -08:00
static_features.cpp Standardize for-loop increments to prefix form (++i) (#8199) 2026-02-18 20:57:29 -08:00
static_features.h disable new code until pre-condition gets fixed 2022-11-30 22:29:59 -08:00
term_enumeration.cpp na 2026-06-19 16:24:08 -07:00
term_enumeration.h updated term enumerator 2026-06-19 16:18:07 -07:00
used_symbols.h Standardize for-loop increments to prefix form (++i) (#8199) 2026-02-18 20:57:29 -08:00
used_vars.cpp Standardize for-loop increments to prefix form (++i) (#8199) 2026-02-18 20:57:29 -08:00
used_vars.h
value_generator.cpp
value_generator.h Use = default for virtual constructors. 2022-08-05 18:11:46 +03:00
well_sorted.cpp Standardize for-loop increments to prefix form (++i) (#8199) 2026-02-18 20:57:29 -08:00
well_sorted.h