mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-07-26 17:02:38 +00:00
Code Activity

qe2: fix nonlinear term introduced by term_graph representative selection in MBP (#10186)

Browse source 
`qe2` could produce a nonlinear term (e.g. `(* x x1)`) when eliminating
quantifiers from a purely linear LIA formula. The result was logically
equivalent but broke downstream consumers expecting QF_LIA output.

**Root cause**

In `term_graph::term_lt`, numeric values were unconditionally ranked
*lower* than uninterpreted constants when selecting equivalence class
representatives. During model-based projection, ITE processing adds the
model literal `(= x1 2)` to the term graph, merging `x1` and `2` into
one equivalence class with `x1` elected as representative. Any
expression containing the coefficient `2` — e.g. `(* 2 x)` from `x + x`
— then gets rewritten as `(* x1 x)`, a nonlinear product of two free
variables.

**Fix** (`src/qe/mbp/mbp_term_graph.cpp` — `term_lt`)

When both terms are 0-argument and differ in value-ness, prefer the
*value* as class representative **unless** the non-value is a variable
slated for elimination (where `refine_repr_class` will later replace it
with a value anyway). This prevents free variables from displacing
numeric coefficients.

```smt2
; Before fix
(apply qe2)
; => (or (not (= x1 2)) (not (= (+ y (* (- 1) x x1)) 0)) (not (= y 0)))
;                                          ^^^^^^^^^^^ nonlinear

; After fix
; => (or (not (= x1 2)) (not (= x 0)) (not (= y 0)))  ; fully linear
```

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: Nikolaj Bjorner <nikolaj@cs.stanford.edu>
This commit is contained in:
Copilot 2026-07-22 18:11:00 -07:00 • committed by GitHub
parent 35b0b42d2e
commit df8d23960e
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 17 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

17
src/qe/mbp/mbp_term_graph.cpp
View file

@ -818,6 +818,23 @@ bool term_graph::term_lt(term const &t1, term const &t2) {
if (t1.get_num_args() == t2.get_num_args()) {
if (m.is_value(t1.get_expr()) == m.is_value(t2.get_expr()))
return t1.get_id() < t2.get_id();
// Prefer values over non-var uninterpreted constants to avoid
// substituting numeric literals with free variables. This prevents
// non-linear terms like (x * x1) when x1=2 is added as a model
// constraint and 2 appears as a coefficient in (2 * x).
// Exception: if the non-value is a variable to eliminate, keep the
// old preference (non-value wins) so refine_repr can replace it.
auto is_elim_var = [&](term const &t) {
expr *e = t.get_expr();
return is_app(e) && m_is_var.contains(to_app(e)->get_decl());
};
bool t1_is_val = m.is_value(t1.get_expr());
bool t2_is_val = m.is_value(t2.get_expr());
// If the non-value is NOT a variable to eliminate, prefer the value
if (t1_is_val && !t2_is_val && !is_elim_var(t2))
return true; // t1 (value) preferred
if (t2_is_val && !t1_is_val && !is_elim_var(t1))
return false; // t2 (value) preferred
return m.is_value(t2.get_expr());
}
return t1.get_num_args() < t2.get_num_args();