mirror of
https://github.com/Z3Prover/z3
synced 2026-06-19 15:16:29 +00:00
dc8179212e
Introduce exclusion intervals alongside the existing path-based condition tracking in simplify_ite_rec. The intervals track which character values are still possible at each point in the ITE tree, enabling simplification of nested range conditions that the per-entry path approach cannot handle. Key additions: - intervals_t type and push_intervals() to maintain live character ranges - eval_range_cond() checks AND-of-char_le conditions against intervals - intersect_intervals/exclude_interval utilities from seq_rewriter pattern - Negated AND handling: ¬(lo<=x ∧ x<=hi) excludes [lo,hi] from intervals The interval check runs before the existing eval_path_cond logic, catching cases like: if(0<=x<=10, t, if(1<=x<=8, t2, e2)) → if(0<=x<=10, t, e2) where the inner range [1,8] is fully contained in the excluded outer range. Fixes remaining regression timeouts on 5728 P2 and 5731 P4. Co-authored-by: Copilot <223556219+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 | ||