mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-08-08 06:52:26 +00:00
Code Activity

Skip is_string_equality rewrite when monadic regex is enabled

Browse source 
When smt.seq.regex_monadic is on, keep contains-style memberships
(s in .*P.*) as regex memberships routed to the monadic solver instead
of rewriting them into a word equation s = f1 ++ P ++ f2. The word
equation blows up theory_seq on long concatenations before final_check
(hence monadic) is ever reached.

Evaluated on 1476 regex benchmarks (10s timeout): solved 1160 -> 1341
vs legacy, +193 newly solved, 0 sat<->unsat soundness disagreements.

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Copilot-Session: 57b9b87e-950a-49ea-bbb3-ed585646a5a9
This commit is contained in:
Nikolaj Bjorner 2026-08-02 12:23:05 -07:00
parent 11c969d31d
commit 385672ce5d
1 changed files with 6 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

8
src/smt/seq_regex.cpp
View file

@ -275,8 +275,12 @@ namespace smt {
if (coallesce_in_re(lit))
return;
if (is_string_equality(lit))
// With the monadic end-game enabled, keep contains-style memberships (s in .*P.*)
// as regex memberships routed to the monadic solver instead of rewriting them into
// a word equation s = f1 ++ P ++ f2, whose word-equation solving blows up on long
// concatenations before final_check is ever reached.
if (!th.use_monadic_regex() && is_string_equality(lit))
return;
if (th.use_monadic_regex())