Profile-guided optimization after #4: expression facts, solver setup, and arithmetic fast paths #5

Follow-up to #4 and #3, based on profiling PR head 2dac008f505f1efa94e0d9480d3fb2abe4b79ffc. This is Astra Medium's analysis. The measured findings are in the PR profiling comment.

Problem and scope

PR #4 removes several major costs, but first-time compound queries still rebuild substantial expression knowledge and solver state. There appears to be meaningful optimization headroom beyond the current memoization, literal shortcut, polarity encoding, and compiled-fact reuse.

Focus on first-time queries and related-but-distinct queries. Identical result-cache hits already cost about 0.5 µs; further work there is unlikely to have comparable value. The proposals below are hypotheses supported by profiles, not promised speedups or implemented fixes. Preserve the default consistency-checking contract; enabling early_return=True is not an equivalent optimization.

Evidence: where time remains

Disjoint phase timings on the current head, in milliseconds:

Totals include smaller normalization, relevance, and query-encoding costs not shown as separate columns. On the 40-term sum, expression fact discovery/encoding is 40%, solver initialization 32%, known facts 13%, and solving 13%. On the unknown-sign two-term sum, solving is about 35%, so the large-sum distribution should not be generalized to every workload.

cProfile identifies _exactlyonearg, assert_formula, iter_atoms, applied-predicate hashing, ClauseDB.literal, solver clause initialization, and propagation as important costs. It records roughly 269,000 function calls per 40-term query, including recursive calls. Profiler-inflated runtimes were not used for the wall-time comparisons.

Controlled ablations explain what #4 has already achieved:

• Disabling the literal shortcut raises rational→real from 15.4 to 448 µs.
• Disabling polarity encoding raises the 40-term sum from 25.4 to 41.95 ms. Actual solver input drops from 6,780 to 3,446 clauses, eliminating 86 auxiliaries, with this optimization enabled.
• Removing compiled-fact reuse increases compound-query time by roughly 6–10%.
• Removing result memoization has essentially no adverse effect on first-time compound-query time.

The 40-term sum was about 136.2 ms upstream, 43.1 ms at the PR base, and 25.4 ms at the head. Much of the upstream advantage already came from lightweight local formulas and direct integer-clause compilation; it should not all be attributed to this PR.

1. Emit expensive expression rules directly, or use a compact cardinality encoding

Why this is promising: The Add handlers still build exactly-one conditions as an OR of n conjunctions of n literals. The polarity optimization fixes excessive clause/auxiliary counts, but the intermediate formulas still take quadratic work to construct, hash, traverse, and translate. Some emitted clauses are also wide. This is remaining work after the encoding improvement discussed in #2.

Two experiments, in increasing order of scope:

1. Add a direct clause-emission path for the known Add rules, reusing predicate IDs and bypassing intermediate Formula trees and repeated atom discovery. Start by emitting the same logical clauses as the current optimized encoder. This can reduce allocation and traversal without changing propagation behavior or theory coverage. It does not by itself remove quadratic literal volume in the resulting wide clauses.
2. Represent the exactly-one antecedent using a compact sequential/counting encoding. This may reduce both construction work and total literal occurrences, but introduces auxiliaries and may change propagation/search behavior. Do not equate a smaller clause count with a faster query.

Validation: compare answers and inconsistency behavior against the full current pipeline. For direct emission, compare normalized clause sets/atom mappings where feasible. For a new encoding, exhaustively check small input assignments and query both polarities: the antecedent's meaning must be preserved inside an implication. Use sound auxiliary constraints, not an unjustified one-way definition. Measure sums of 2, 10, 20, 40, 80, and 160 terms; record build time, total literal occurrences, clauses, auxiliaries, and solver time. Include mixed-sign and unknown cases, not just an easy positive sum.

Priority: first candidate. It targets measured overhead while offering a narrower correctness boundary than dropping facts.

2. Generate only the expression knowledge needed, with consistency preserved

Why this is promising: the positive-sum query still generates integer/irrational rules, including the expensive exactly-one formulas. Current discovery is driven by subjects; it is not sufficient to avoid predicate families irrelevant to a particular proof.

An incremental approach would make handler rules lazy and expose which predicates they require/produce. Build a dependency closure from the proposition and explicit assumptions, including known-predicate implications, rather than unconditionally constructing every fact for every visited expression. A related option is staged discovery: first cheap rules, then expensive rules if the result remains unresolved.

The hard part is consistency, not only proving the requested literal. Returning a locally proven result while omitting facts that expose inconsistent assumptions changes the API. Merely mentioning all assumption atoms is not a proof that the closure is sufficient. Staged discovery must still establish consistency before returning under default semantics; the existing early_return mode cannot silently become the default behavior. For uncertain rule shapes or dependency relationships, fall back to the complete pipeline.

Validation: add adversarial cases where one subset proves the proposition but another subset becomes inconsistent only through an expression rule; unrelated explicit contradictions; negation, disjunction, connected subjects, matrix/number mixtures, and supported theory options. Compare True/False/None and exception outcomes, with distinct inputs to avoid result-cache hits. Count which rules were skipped and whether pruning reduces downstream solver initialization as well as discovery.

Expected opportunity: this could avoid work in multiple phases, not only the 40% discovery bucket. However, its semantic complexity makes it a larger investigation than direct emission.

3. Reduce fresh solver setup and improve the extent of fact reuse

Why this is promising: solver initialization is 8.27 ms / 32% of the 40-term query and 0.569 ms / 41% of the two-term positive-sum query. Engine construction copies clauses, checks them, initializes solver structures, and propagates on every uncached call.

Start with smaller experiments:

• Trace the clause representation end to end and eliminate demonstrably redundant copying or scans. If using an internal trusted-data path, preserve validation for public/external inputs.
• Share immutable clause content where possible while keeping mutable watch lists, assignments, counters, decision state, and theory state isolated.
• Measure whether known-fact templates can reuse more than their syntax: precomputed metadata or initialization scaffolding may be useful even when full solver reuse is not.

Only then explore an explicit reusable query context or initialized solver snapshot for a stable expression/assumption universe. Distinguish the base fact set from per-query assumptions and newly discovered facts. Changes in variable allocation, expressions, assumptions, or theory configuration must invalidate or extend the context correctly. A full deep copy could consume the intended saving; measure it before designing around it.

The “persistent facts” improvement currently shares compiled templates, not an initialized solver. In the fresh 40-term profile, all 820 replay calls (41 subjects × 20 queries) used _rebase, rather than the verbatim-append path. New subjects cannot hit the per-subject binding cache. Inspect which layouts actually reach each reuse path before assuming that a cache or fast path is effective.

Validation: alternate positive/negative queries and assumptions; reuse after SAT and UNSAT outcomes; add new expressions; switch fact families and supported theory modes; test independent engines for mutation leaks. Compare one-shot cost, related-query amortized cost, memory retention, and reset/invalidation cost.

Limit: even eliminating the entire measured initialization phase would cap this particular case's isolated speedup at about 1.46×. That is an upper bound, not an achievable forecast. Larger gains require other phases to improve too.

4. Extend the proven-safe shortcut to common arithmetic closures

Why this is promising: the existing literal shortcut gives about 29× on rational→real, but turning it off makes essentially no difference to the compound cases tested. A two-term positive sum still costs about 1.34 ms and a 40-term positive sum about 25.4 ms, despite the desired entailment having a simple structural proof.

Candidate starting cases are positivity of sums whose arguments are explicitly positive, real-valued sums/products under sufficient assumptions, or a small supported class of powers. Prefer deriving these from existing registered rules or shared rule metadata rather than duplicating an unrelated list of special cases.

Define a narrow, reviewable eligibility condition. The shortcut needs both an entailment proof and a justification that returning will preserve inconsistency behavior. Unsupported Boolean contexts, ambiguous expression shapes, and theory configurations should fall through to the normal pipeline. Reuse the existing fast-path testing strategy: compare against an oracle that bypasses both memoization and the shortcut.

Validation: negative and unknown results, negated propositions, inconsistent additional assumptions, noncommutative/matrix inputs, unevaluated expressions where supported, iteration limits, use_known_facts, and LRA options. Test the exact supported envelope exhaustively where small enough, then add differential randomized coverage. Report hit rate as well as per-hit speed: a large microbenchmark gain is useful only when the shape is common.

Tradeoff: potentially very large gains for selected queries, with less benefit to general or unknown-result workloads. This is not a universal replacement for the solver.

5. Smaller supporting improvements: hashing and atom lookup

The profiles show frequent recursive formula hashing, AppliedPredicate.__hash__, ClauseDB.literal, and iter_atoms work. Reusing local predicate objects/IDs, hoisting repeated dictionary lookups, or caching hashes on immutable objects could reduce constants. Measure allocation, hash-call counts, and memory retention before introducing additional interning caches. Stable equality/hash semantics and cache lifetime matter. Direct emission may remove much of this work already, so profile again after larger changes instead of independently optimizing work that will disappear.

Suggested order and acceptance criteria

1. Establish a reproducible first-query/scaling benchmark with phase and encoding-size measurements.
2. Prototype direct emission for the expensive Add rules; evaluate compact cardinality encoding separately.
3. Inspect redundant initialization work and the actual compiled-fact reuse paths.
4. Prototype a narrowly justified arithmetic fast path.
5. Pursue lazy/relevance-based fact generation and reusable solver contexts as larger projects, informed by updated profiles.

For every change:

• Keep default consistency checks and answer/exception coverage intact; do not count a newly returned None as a speedup over a previously proven answer.
• Separate first-time queries, related-but-distinct queries, and identical cache hits.
• Compare total runtime as well as phases; an encoding can save construction time and make search worse.
• Use pinned revisions, alternating baseline/candidate runs, multiple processes and hash seeds, controlled CPU load, and raw sample retention. Include the existing validation suites and representative non-scalar/contradictory workloads.
• Measure memory and cache growth for any additional reuse mechanism.

Measurement provenance and limits

SymPy ddbb536d7e803e4c38d5d5808ad1217368b12655, Python 3.13.5, i5-5257U, pinned logical CPU 2, PYTHONHASHSEED=0, shared host without frequency lock or exclusive CPU lease. Inputs were prebuilt, process/template caches warm, result caches missed on distinct first queries, and GC disabled during timed sections.

Phase values are means over 40 distinct queries. Ablations used three processes per variant and median-of-process-medians, with 60 distinct queries per ordinary case and 15 for the large sum per process. Variant order alternated across rounds. Seven workloads had matching answers in all variant/round combinations. Profiler call trees identified hotspots; unprofiled measurements supplied speedup ratios.

The earlier old/new-system comparison interleaved engines between individual queries, whereas the ablations batch one engine at a time. Small-query absolute times therefore differ; use within-suite ratios. No claimed next-step speedups have been implemented or measured. All observations refer to the pinned PR head, not later revisions.