From 49f2eb0e49010761cbbede2af408ddf0aa66c465 Mon Sep 17 00:00:00 2001 From: Copilot <198982749+Copilot@users.noreply.github.com> Date: Wed, 25 Mar 2026 06:51:51 -0700 Subject: [PATCH] seq_nielsen: use arith binary match overloads in get_const_power_diff (#9125) * refactor get_const_power_diff to use is_add/is_sub binary overloads Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> Agent-Logs-Url: https://github.com/Z3Prover/z3/sessions/1d71a642-bb8f-43ca-88fd-9dc48f5aab24 * fix build: remove unnecessary arith_solver.h include from seq_nielsen.cpp Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> Agent-Logs-Url: https://github.com/Z3Prover/z3/sessions/bb09a786-4445-4645-9930-e80494d96dbf --------- Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com> Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> Co-authored-by: Nikolaj Bjorner --- src/smt/seq/seq_nielsen.cpp | 32 ++++++++++---------------------- 1 file changed, 10 insertions(+), 22 deletions(-) diff --git a/src/smt/seq/seq_nielsen.cpp b/src/smt/seq/seq_nielsen.cpp index 106d161a6..d3ce54984 100644 --- a/src/smt/seq/seq_nielsen.cpp +++ b/src/smt/seq/seq_nielsen.cpp @@ -692,34 +692,22 @@ namespace seq { // static bool get_const_power_diff(expr* b, expr* a, arith_util& arith, rational& diff) { if (a == b) { diff = rational(0); return true; } + expr* x = nullptr, *y = nullptr; + rational val; // b = (+ a k) ? - if (arith.is_add(b) && to_app(b)->get_num_args() == 2) { - rational val; - if (to_app(b)->get_arg(0) == a && arith.is_numeral(to_app(b)->get_arg(1), val)) - { diff = val; return true; } - if (to_app(b)->get_arg(1) == a && arith.is_numeral(to_app(b)->get_arg(0), val)) - { diff = val; return true; } + if (arith.is_add(b, x, y)) { + if (x == a && arith.is_numeral(y, val)) { diff = val; return true; } + if (y == a && arith.is_numeral(x, val)) { diff = val; return true; } } // a = (+ b k) → diff = -k - if (arith.is_add(a) && to_app(a)->get_num_args() == 2) { - rational val; - if (to_app(a)->get_arg(0) == b && arith.is_numeral(to_app(a)->get_arg(1), val)) - { diff = -val; return true; } - if (to_app(a)->get_arg(1) == b && arith.is_numeral(to_app(a)->get_arg(0), val)) - { diff = -val; return true; } + if (arith.is_add(a, x, y)) { + if (x == b && arith.is_numeral(y, val)) { diff = -val; return true; } + if (y == b && arith.is_numeral(x, val)) { diff = -val; return true; } } // b = (- a k) → diff = -k - if (arith.is_sub(b) && to_app(b)->get_num_args() == 2) { - rational val; - if (to_app(b)->get_arg(0) == a && arith.is_numeral(to_app(b)->get_arg(1), val)) - { diff = -val; return true; } - } + if (arith.is_sub(b, x, y) && x == a && arith.is_numeral(y, val)) { diff = -val; return true; } // a = (- b k) → diff = k - if (arith.is_sub(a) && to_app(a)->get_num_args() == 2) { - rational val; - if (to_app(a)->get_arg(0) == b && arith.is_numeral(to_app(a)->get_arg(1), val)) - { diff = val; return true; } - } + if (arith.is_sub(a, x, y) && x == b && arith.is_numeral(y, val)) { diff = val; return true; } return false; }