From 9a2867aeb7eaefadce0792a4f54f9387a5f66aa2 Mon Sep 17 00:00:00 2001 From: Nelson Elhage Date: Tue, 21 Oct 2025 12:16:54 -0700 Subject: [PATCH] Add a fast-path to _coerce_exprs. (#7995) When the inputs are already the same sort, we can skip most of the coercion logic and just return. Currently, `_coerce_exprs` is by far the most expensive part of building up many common Z3 ASTs, so this fast-path is a substantial speedup for many use-cases. --- src/api/python/z3/z3.py | 15 +++++++++++++++ 1 file changed, 15 insertions(+) diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index 128726dae..df6230420 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -1245,6 +1245,18 @@ def _coerce_expr_merge(s, a): else: return s +def _check_same_sort(a, b, ctx=None): + if not isinstance(a, ExprRef): + return False + if not isinstance(b, ExprRef): + return False + if ctx is None: + ctx = a.ctx + + a_sort = Z3_get_sort(ctx.ctx, a.ast) + b_sort = Z3_get_sort(ctx.ctx, b.ast) + return Z3_is_eq_sort(ctx.ctx, a_sort, b_sort) + def _coerce_exprs(a, b, ctx=None): if not is_expr(a) and not is_expr(b): @@ -1259,6 +1271,9 @@ def _coerce_exprs(a, b, ctx=None): if isinstance(b, float) and isinstance(a, ArithRef): b = RealVal(b, a.ctx) + if _check_same_sort(a, b, ctx): + return (a, b) + s = None s = _coerce_expr_merge(s, a) s = _coerce_expr_merge(s, b)