mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-07-29 02:03:49 +00:00
Code Activity

[nra_solver] Simplify COI guard logic using early-continue pattern (#10245)

Browse source 
Refactors the constraint/monic verification loops in `nra_solver.cpp`
introduced by #10230 to reduce nesting and improve readability. No
functional change.

### Changes

- **Early-continue guards**: Replace `if (!check_X(ci)) { if
(coi.contains(ci)) { ... } return l_undef; }` with `if (check_X(ci))
continue;` so the failure path reads linearly
- **Explicit braces**: Add braces to the constraint loop (monic loop
already had them), making both loops consistent
- **Condensed comment**: Collapse 6-line COI explanation to one line

```cpp
// Before
for (lp::constraint_index ci : lra.constraints().indices())
    if (!check_constraint(ci)) {
        // nlsat only solves over the cone-of-influence (COI) subset
        // of constraints, so constraints outside the COI may be
        // legitimately violated by the nlsat model. Only a violation
        // of a COI constraint indicates a genuine nlsat bug; a
        // non-COI violation is benign, so fall back to l_undef
        // quietly without emitting diagnostics.
        if (m_coi.constraints().contains(ci)) { ...; UNREACHABLE(); }
        return l_undef;
    }

// After
for (lp::constraint_index ci : lra.constraints().indices()) {
    if (check_constraint(ci)) continue;
    // Non-COI constraint violations are benign; only COI violations indicate a bug.
    if (m_coi.constraints().contains(ci)) { ...; UNREACHABLE(); }
    return l_undef;
}
```

<!-- START COPILOT CODING AGENT SUFFIX -->

- Fixes #10235

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
This commit is contained in:
Copilot 2026-07-27 07:18:30 -07:00 • committed by GitHub
parent 2d48fd119c
commit 7ef68c3ae1
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 15 additions and 21 deletions
Download patch file Download diff file Expand all files Collapse all files

36
src/math/lp/nra_solver.cpp
View file

@ -238,30 +238,24 @@ struct solver::imp {
m_nlsat->restore_order();
m_nla_core.set_use_nra_model(true);
lra.init_model();
for (lp::constraint_index ci : lra.constraints().indices())
if (!check_constraint(ci)) {
// nlsat only solves over the cone-of-influence (COI) subset
// of constraints, so constraints outside the COI may be
// legitimately violated by the nlsat model. Only a violation
// of a COI constraint indicates a genuine nlsat bug; a
// non-COI violation is benign, so fall back to l_undef
// quietly without emitting diagnostics.
if (m_coi.constraints().contains(ci)) {
IF_VERBOSE(0, verbose_stream() << "constraint " << ci << " violated\n";
lra.constraints().display(verbose_stream()));
UNREACHABLE();
}
return l_undef;
for (lp::constraint_index ci : lra.constraints().indices()) {
if (check_constraint(ci)) continue;
// Non-COI constraint violations are benign; only COI violations indicate a bug.
if (m_coi.constraints().contains(ci)) {
IF_VERBOSE(0, verbose_stream() << "constraint " << ci << " violated\n";
lra.constraints().display(verbose_stream()));
UNREACHABLE();
}
return l_undef;
}
for (auto const &m : m_nla_core.emons()) {
if (!check_monic(m)) {
if (m_coi.mons().contains(m.var())) {
IF_VERBOSE(0, verbose_stream() << "monic " << m << " violated\n";
lra.constraints().display(verbose_stream()));
UNREACHABLE();
}
return l_undef;
if (check_monic(m)) continue;
if (m_coi.mons().contains(m.var())) {
IF_VERBOSE(0, verbose_stream() << "monic " << m << " violated\n";
lra.constraints().display(verbose_stream()));
UNREACHABLE();
}
return l_undef;
}
break;
case l_false: {