mirror of
https://github.com/Z3Prover/z3
synced 2026-07-15 11:35:42 +00:00
710b4082d1
The reported case showed expensive reasoning for lexicographic string
comparisons under the default sequence solver, and incorrect handling
expectations with `z3str3` (which does not interpret these comparisons).
This change targets the default solver path by short-circuiting
contradictory constant-bound `<` constraints earlier.
- **Theory shortcut for constant lexical bounds**
- In `theory_seq::assign_eh`, detect asserted `str.<` constraints of the
form `c < x` or `x < c` where `c` is a string constant.
- When a complementary bound on the same equivalence class is already
true, check bound consistency immediately.
- If bounds are contradictory (`!(lower < upper)`), emit a direct theory
conflict from the two active literals instead of waiting for deeper
axiom propagation.
- **Preserve existing comparison reasoning**
- Existing `check_lts` transitivity/axiom flow is retained.
- The new logic is a narrow fast path for contradictory constant bounds
and does not alter general string-order semantics.
- **Regression coverage**
- Added a solver-level regression in `src/test/seq_rewriter.cpp` for
contradictory date-like lexical bounds to ensure this class of
constraints is rejected as `unsat`.
```cpp
ctx.assert_expr(su.str.mk_lex_lt(su.str.mk_string("2024-01-01"), x));
ctx.assert_expr(su.str.mk_lex_lt(x, su.str.mk_string("2024-12-31")));
ctx.assert_expr(su.str.mk_lex_lt(x, su.str.mk_string("2023-01-01")));
ENSURE(ctx.check() == l_false);
```
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
|
||
|---|---|---|
| .. | ||
| ackermannization | ||
| api | ||
| ast | ||
| cmd_context | ||
| math | ||
| model | ||
| muz | ||
| nlsat | ||
| opt | ||
| params | ||
| parsers | ||
| qe | ||
| sat | ||
| shell | ||
| smt | ||
| solver | ||
| tactic | ||
| test | ||
| util | ||
| CMakeLists.txt | ||