Build assertion messages only when the assertion fails

[daniel-larraz]

_assert takes an already-built message, so every caller that formats one pays for it whether or not the check passes. Two of those sit on paths taken constantly:

• instance_check — reached from _sort, and so from every sort() call
• _higherorder_apply — reached from every function application

In both, building the message costs more than everything else the check does. Printing the operand is the expensive part: "%s" % func measures at ~3.3 µs, against ~0.2 µs for the comparison it decorates.

Change

Move the formatting behind the failing branch, written the way the rest of the file already writes checks whose message is computed (_assert(False, ...) under an if). Four sites in total; the other two are cold, but left inconsistent they invite the pattern back.

The condition, the message text, and the exception type are all unchanged. I diffed the raised errors against main for each of the four:

SMTException: Expected <class 'cvc5.cvc5_python_base.Term'>, but got a <class 'int'>
SMTException: Incorrect number of arguments to f
SMTException: non-string key 5
SMTException: Missing datatype: E

Identical before and after.

Effect

Term building gets 2–4x faster. Three alternating runs of each, 20k iterations per measurement:

	main	this PR
x.sort()	1.73 / 1.59 / 1.80	0.48 / 0.46 / 0.42	3.8x
f(x)	14.55 / 12.80 / 14.73	5.29 / 5.18 / 4.73	2.8x
x + y	10.37 / 9.16 / 10.49	3.51 / 3.39 / 3.10	3.0x
x == y	10.35 / 9.19 / 10.54	3.50 / 3.40 / 3.08	3.0x
a[x]	7.58 / 6.66 / 7.63	3.67 / 3.67 / 3.27	2.1x
And(x==1, y==2)	27.42 / 24.18 / 27.76	14.00 / 14.10 / 12.20	2.0x

(microseconds per call)

The two fixes compound: an application coerces each argument through domain(i).cast(...), which goes through _sort and so through instance_check as well.

Correctness, not just speed

Formatting the operand can itself 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. Building the message only on the failing path removes that class of bug from every one of these sites.

Testing

• test_doc.py: 0 failures.
• test_unit.py: OK.
• black --check --required-version 24: clean.
• pyright: 633 errors, unchanged from main.
• Raised errors diffed against main for all four sites, as above.

🤖 Generated with Claude Code

[alex-ozdemir]

Good find. It is too bad that Python doesn't have any call-by-name or laziness features, which could be used to eliminate this overhead.

I have just one request.

[daniel-larraz]

Thanks — switched all four sites to raise SMTException(...).

I went with that over a _fail(...) helper because direct raise SMTException(...) already appears six times in this file, so it needs no new API. Happy to swap to _fail(...) if you'd rather have the named helper.

One thing worth deciding separately: _assert(False, ...) is a pre-existing idiom here, at ten other sites (_coerce_expr_merge, ArithSortRef.cast, _py2expr, FPNumRef construction, and others). This PR no longer adds any, but it doesn't retire the existing ones either. Say the word if you'd like a follow-up converting them — that's the case where _fail(...) would earn its keep, since it would give all eleven a single target.

Re-verified after the change: the raised exception and message are byte-identical to main for all four, and the speedup is unaffected.

x.sort()          1.70 us -> 0.45 us   3.8x
f(x)             14.05 us -> 5.10 us   2.8x
x + y            10.08 us -> 3.33 us   3.0x
x == y           10.19 us -> 3.33 us   3.1x
a[x]              7.39 us -> 3.61 us   2.0x
And(x==1, y==2)  26.90 us -> 13.54 us  2.0x

Doctests, unit tests, black, and pyright (633, unchanged) all still pass.

[alex-ozdemir]

LGTM