From d14947950fdc78430ad964a29da03640a3a407a3 Mon Sep 17 00:00:00 2001 From: Daniel Larraz Date: Fri, 14 Aug 2026 09:31:09 -0500 Subject: [PATCH] Build assertion messages only when the assertion fails _assert takes an already-built message, so every caller that formats one pays for it whether or not the check passes. Two of those are on paths taken constantly: instance_check, reached from _sort and so from every sort(), and _higherorder_apply, reached from every function application. Formatting dominates both -- printing the operand costs far more than the comparison it decorates. Raise from the failing branch instead. Term building gets 2-4x faster: x.sort() 1.70 us -> 0.45 us f(x) 14.05 us -> 5.10 us x + y 10.08 us -> 3.33 us a[x] 7.39 us -> 3.61 us And(x==1, y==2) 26.90 us -> 13.54 us The messages and the exceptions raised are unchanged. Formatting the operand can also raise, which turns a passing assertion into an error: printing a term whose kind the printer has no case for fails, so the check reports the wrong problem, or invents one where there is none. Co-Authored-By: Claude Opus 5 (1M context) --- cvc5_pythonic_api/cvc5_pythonic.py | 28 +++++++++++++--------------- 1 file changed, 13 insertions(+), 15 deletions(-) diff --git a/cvc5_pythonic_api/cvc5_pythonic.py b/cvc5_pythonic_api/cvc5_pythonic.py index 3b18d6d..ae28db2 100644 --- a/cvc5_pythonic_api/cvc5_pythonic.py +++ b/cvc5_pythonic_api/cvc5_pythonic.py @@ -760,10 +760,10 @@ def is_sort(s): def instance_check(item, instance): - _assert( - isinstance(item, instance), - "Expected {}, but got a {}".format(instance, type(item)), - ) + # The message is built only on failure. Formatting it up front costs most + # of the time this check takes, and it is on the path of every `sort()`. + if not isinstance(item, instance): + raise SMTException("Expected {}, but got a {}".format(instance, type(item))) def _to_sort_ref(s, ctx): @@ -957,11 +957,11 @@ def _higherorder_apply(func, args, kind): """Create an SMT application from a FuncDeclRef and a kind of application""" args = _get_args(args) num = len(args) - if debugging(): - _assert( - num == func.arity(), - "Incorrect number of arguments to %s" % func, - ) + # The message is built only on failure: printing `func` is a quarter of + # the time an application takes, and it can raise for a function that the + # printer has no case for. + if debugging() and num != func.arity(): + raise SMTException("Incorrect number of arguments to %s" % func) _args = [] for i in range(num): tmp = func.domain(i).cast(args[i]) @@ -6399,7 +6399,8 @@ def setOption(self, name=None, value=None, **kwargs): if name is not None: kwargs[name] = value for k, v in kwargs.items(): - _assert(isinstance(k, str), "non-string key " + str(k)) + if not isinstance(k, str): + raise SMTException("non-string key " + str(k)) if isinstance(v, bool): v = "true" if v else "false" elif not isinstance(v, str): @@ -8752,11 +8753,8 @@ def CreateDatatypes(*ds): fname = fs[k][0] ftype = fs[k][1] if isinstance(ftype, Datatype): - if debugging(): - _assert( - ftype.name in uninterp_sorts, - "Missing datatype: " + ftype.name, - ) + if debugging() and ftype.name not in uninterp_sorts: + raise SMTException("Missing datatype: " + ftype.name) ftype = uninterp_sorts[ftype.name] else: if debugging():