From df8d23960eda51b796bc82cfcbc3319f135a1b34 Mon Sep 17 00:00:00 2001 From: Copilot <198982749+Copilot@users.noreply.github.com> Date: Wed, 22 Jul 2026 18:11:00 -0700 Subject: [PATCH] qe2: fix nonlinear term introduced by term_graph representative selection in MBP (#10186) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit `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 --- src/qe/mbp/mbp_term_graph.cpp | 17 +++++++++++++++++ 1 file changed, 17 insertions(+) diff --git a/src/qe/mbp/mbp_term_graph.cpp b/src/qe/mbp/mbp_term_graph.cpp index 04985c2ffe..3d02cd7f85 100644 --- a/src/qe/mbp/mbp_term_graph.cpp +++ b/src/qe/mbp/mbp_term_graph.cpp @@ -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();