mirror of
https://github.com/Z3Prover/z3
synced 2026-08-09 23:42:21 +00:00
a7762346d2
Decide monadic memberships over their atomic terms first and canonize through theory_seq's word equations lazily, inside final_check's refinement loop, only when a proposed model violates a term's defining equation. This mirrors the existing lazy length-bound enforcement. Eagerly canonizing at add time baked every word equation into every unsat core, producing weak, non-generalizing conflicts. With lazy canonization an unsatisfiable regex is refuted over the atomic term with no length/canonization dependency attached (strong conflicts); a canonization equality enters a core only when it was actually needed. Unit tests (test-z3 seq_monadic) pass; a 120-instance slog+automatark sweep with model_validate=true reports 0 invalid models and no regressions. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> Copilot-Session: 57b9b87e-950a-49ea-bbb3-ed585646a5a9 |
||
|---|---|---|
| .. | ||
| ackermannization | ||
| api | ||
| ast | ||
| cmd_context | ||
| math | ||
| model | ||
| muz | ||
| nlsat | ||
| opt | ||
| params | ||
| parsers | ||
| qe | ||
| sat | ||
| shell | ||
| smt | ||
| solver | ||
| tactic | ||
| test | ||
| util | ||
| CMakeLists.txt | ||