mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-31 19:52:29 +00:00
Code Activity

Add a fast-path to _coerce_exprs.

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-19 13:26:06 -07:00
parent 3ce8aca411
commit f6168cad62
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: else:
return s 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): def _coerce_exprs(a, b, ctx=None):
if not is_expr(a) and not is_expr(b): 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): if isinstance(b, float) and isinstance(a, ArithRef):
b = RealVal(b, a.ctx) b = RealVal(b, a.ctx)
if _check_same_sort(a, b, ctx):
return (a, b)
s = None s = None
s = _coerce_expr_merge(s, a) s = _coerce_expr_merge(s, a)
s = _coerce_expr_merge(s, b) s = _coerce_expr_merge(s, b)