mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-22 15:34:35 +00:00
Code Activity

Add a fast-path to _coerce_exprs. (#7995)

Browse source 
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.
This commit is contained in:
Nelson Elhage 2025-10-21 12:16:54 -07:00 • committed by GitHub
parent 06ed96dbda
commit 9a2867aeb7
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 15 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

15
src/api/python/z3/z3.py
View file

@ -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)