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.

Author: nelhage

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)