mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-04-02 09:58:59 +00:00
Code Activity

seq_nielsen: use arith binary match overloads in get_const_power_diff (#9125)

Browse source 
* 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 <nbjorner@microsoft.com>
This commit is contained in:
Copilot 2026-03-25 06:51:51 -07:00 • committed by GitHub
parent 8eaa9d9e6b
commit 49f2eb0e49
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 10 additions and 22 deletions
Download patch file Download diff file Expand all files Collapse all files

32
src/smt/seq/seq_nielsen.cpp
View file

@ -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;
}