More selective and cheaper care-pair generation

Status: Open lead. Owner: unassigned.

Investigate whether proposing fewer care pairs, or producing them on demand, reduces total solving time. This is the first investigation to try before using care information to reduce combination obligations. No prototype or new performance evaluation has been selected.

Implemented baseline

The combination chapter explains the current heuristic. The EUF generator groups flattened applications by the congruence class of their function term, deduplicates shared arguments, and enumerates distinct argument pairs within each group. A group with k arguments can still generate k(k - 1)/2 pairs.

The general component driver already prioritizes disagreements on care pairs. It retains complete model-partition comparison and complete-arrangement fallback. QF_UFLIA collects care pairs for each checked EUF model. The dedicated Real route already caches care computations for an unchanged EUF assignment; adding that cache is not new work. Its earlier optimization and measurements remain historical evidence, not a prediction for another change.

Paper basis and candidate changes

Dejan Jovanović and Clark Barrett, Being Careful about Theory Combination, Formal Methods in System Design 42(1), 2013, pp. 67–90, §4.2, describes EUF care pairs using congruence and known disequalities. It expands their Sharing is Caring: Combination of Theories, FroCoS 2011, pp. 195–210.

Audit which of the paper’s exclusions can help Primo’s heuristic: argument pairs already known equal or disequal, application results already in the same congruence class, and application pairs separated by another known-disequal argument. Map these conditions to the curried representation before using them; the current generator does not implement the full §4.2 construction.

Separately investigate lazy generation within large function classes. This is an engineering proposal, not an implemented paper mechanism. Account for the cost of identifying the next useful pair, scope validation, and the current deterministic choice order. If an alternative changes decision ordering, record that as a search-policy change rather than attributing all effects to reduced generation work.

Keep complete model comparison, explained consequences, and fallback intact. A filtered-out care suggestion does not authorize omitting an equality required for acceptance. Any additional cache must account for closure changes, backtracking, new terms, and the model token to which its results belong.

First experiment and acceptance

Profile the current generator and consumer separately. Compare the unchanged baseline, a control without care priority, and one refinement at a time. Measure generated and inspected pairs, generation time, peak memory, SAT choices and calls, fallback frequency, solved count, total runtime, and PAR2. Fewer generated pairs alone do not establish an improvement.

Extend the existing generation regressions and selection and validation tests for duplicate arguments, settled pairs and results, multiargument applications, newly relevant pairs after merges or rollback, and disagreements outside the care list. Run the applicable fresh fuzzing gates and independent SAT-model validation before accepting performance results.

Use paired evaluations on representative QF_UFLRA and QF_UFLIA inputs, including both large care classes and cases with little care work. Reject or restrict a refinement if its bookkeeping or changed search loses the savings, or if gains on a few cases hide substantial broader regressions. Record the decision and reproducible evidence before closing the lead.