Skip to content

Change policy for lambda lifting - #13017

Open
ajreynol wants to merge 12 commits into
cvc5:mainfrom
ajreynol:noLiftLambda
Open

Change policy for lambda lifting#13017
ajreynol wants to merge 12 commits into
cvc5:mainfrom
ajreynol:noLiftLambda

Conversation

@ajreynol

@ajreynol ajreynol commented Sep 29, 2026 •
edited
Loading

Copy link
Copy Markdown
Member

This PR makes it so that lambdas are not eagerly replaced by skolems.

The motivation is to ensure that (most) lambdas are preserved for higher-order sets/relation operators. This makes it so that e.g. getOriginalForm is not necessary as a workaround, making the code more robust.

We continue to distinguish a class of lambdas (with nested functions) which require lifting and we never handle with beta reduction.

🤖 Generated with Claude Code

@ajreynol ajreynol mentioned this pull request Sep 29, 2026
Closed
@mudathirmahgoub mudathirmahgoub mentioned this pull request Oct 6, 2026
Open
@ajreynol ajreynol added normal Priority moderate Complexity and removed work in progress labels Oct 6, 2026
@mudathirmahgoub @claude
Document the new lambda lifting policy
a379ef1 
Comment-only changes on top of cvc5#13017:
- Explain each case of LambdaLift::ppRewrite, and why the APPLY_UF case
  can rely on the arguments having been preprocessed already.
- Explain the conditional lift lemma (getLiftLemma), and why a single
  ordinary function of the class suffices in checkLazyLambda.
- Fix the non-termination example in checkLazyLambda.
- Explain why the extensionality lemma cannot rewrite to false.
- Document the new behavior of computeRelevantTerms, checkExtensionality
  and applyExtensionality in ho_extension.h.
- Update stale documentation outside the PR's files: the lambda inference
  ids (inference_id.h), FunctionConst::getDefinition, and the help text of
  --uf-lazy-ll.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
@mudathirmahgoub

mudathirmahgoub commented Oct 12, 2026

Copy link
Copy Markdown
Contributor

PR #13017 vs main — higher-order benchmarks

All HO_ALL benchmarks of cvc5/sets-and-relations-benchmarks: sleec/smtlib_quantifiers, sleec/smtlib_set_quantifiers and sql. main is 053f65c, the commit this PR was last merged with.

Binaries: configure.sh unrestricted --ninja --auto-download, assertions/tracing off. 14 workers, jobs shuffled.

2812 benchmarks, both configurations.

Soundness check

sat/unsat disagreements: 0

Solved per family

family n timeout main (053f65c) PR #13017 (17517b5) delta only main (053f65c) only PR #13017 (17517b5)
sql 88 10s 86 86 0 0 0
sleec_set_quantifiers 1362 25s 1330 1330 0 0 0
sleec_quantifiers 1362 25s 511 511 0 0 0
total 2812 1927 1927 0 0 0

Status breakdown

family config sat unsat unknown timeout error PAR-2 (s)
sql main (053f65c) 1 85 2 0 0 44
sql PR #13017 (17517b5) 1 85 2 0 0 44
sleec_set_quantifiers main (053f65c) 1192 138 32 0 0 1802
sleec_set_quantifiers PR #13017 (17517b5) 1192 138 32 0 0 1803
sleec_quantifiers main (053f65c) 510 1 851 0 0 43071
sleec_quantifiers PR #13017 (17517b5) 510 1 851 0 0 43072
all main (053f65c) 1703 224 885 0 0 44917
all PR #13017 (17517b5) 1703 224 885 0 0 44919

unknown = the solver answered unknown (e.g. the in-file tlimit-per fired, or incompleteness); timeout = killed at the external limit. PAR-2 charges every unsolved instance twice its family's timeout.

Runtime on commonly-solved instances

family both solve main (053f65c) total PR #13017 (17517b5) total ratio PR #13017 (17517b5)/main (053f65c) median per-instance ratio
sql 86 4.3s 4.3s 1.007 1.025
sleec_set_quantifiers 1330 201.7s 203.0s 1.007 1.000
sleec_quantifiers 511 521.1s 521.9s 1.001 1.000
all 1927 727.1s 729.2s 1.003 1.000

Ratios below 1.00 mean the branch is faster. The median per-instance ratio ignores instances under 0.05s, where timer noise dominates.

Solved only by PR #13017 (17517b5) (0)

Solved only by main (053f65c) (0)

cactus_pr13017_vs_main cactus_pr13017_vs_main_pooled scatter_pr13017_vs_main

liastar7_no_lift_lambda vs liastar7 — fmcad26 benchmarks

liastar7_no_lift_lambda is liastar7 with this PR merged in, plus a commit removing the SkolemManager::getOriginalForm calls from the liastar code: with this PR, the first argument of int.star-contains is the lambda itself instead of a purification skolem.

Binaries: configure.sh unrestricted --ninja --auto-download --gpl --normaliz, assertions/tracing off. CLI binary, default options, 100s timeout, 6 workers, jobs shuffled.

509 benchmarks, both configurations.

Soundness check

sat/unsat disagreements: 0

Solved per family

family n timeout liastar7 (046355d) liastar7_no_lift_lambda (c201ecf) delta only liastar7 (046355d) only liastar7_no_lift_lambda (c201ecf)
bapa_card 120 100s 104 104 0 0 0
bapa_arith 120 100s 120 120 0 0 0
mapa_arith 120 100s 120 120 0 0 0
sql 29 100s 29 29 0 0 0
mapa_card 120 100s 109 109 0 0 0
total 509 482 482 0 0 0

Status breakdown

family config sat unsat unknown timeout error PAR-2 (s)
bapa_card liastar7 (046355d) 61 43 0 16 0 3318
bapa_card liastar7_no_lift_lambda (c201ecf) 61 43 0 16 0 3318
bapa_arith liastar7 (046355d) 74 46 0 0 0 18
bapa_arith liastar7_no_lift_lambda (c201ecf) 74 46 0 0 0 18
mapa_arith liastar7 (046355d) 74 46 0 0 0 15
mapa_arith liastar7_no_lift_lambda (c201ecf) 74 46 0 0 0 15
sql liastar7 (046355d) 8 21 0 0 0 5
sql liastar7_no_lift_lambda (c201ecf) 8 21 0 0 0 4
mapa_card liastar7 (046355d) 66 43 0 11 0 2392
mapa_card liastar7_no_lift_lambda (c201ecf) 66 43 0 11 0 2397
all liastar7 (046355d) 283 199 0 27 0 5747
all liastar7_no_lift_lambda (c201ecf) 283 199 0 27 0 5753

unknown = the solver answered unknown (e.g. the in-file tlimit-per fired, or incompleteness); timeout = killed at the external limit. PAR-2 charges every unsolved instance twice its family's timeout.

Runtime on commonly-solved instances

family both solve liastar7 (046355d) total liastar7_no_lift_lambda (c201ecf) total ratio liastar7_no_lift_lambda (c201ecf)/liastar7 (046355d) median per-instance ratio
bapa_card 104 117.5s 118.0s 1.004 0.984
bapa_arith 120 17.7s 18.1s 1.027 1.000
mapa_arith 120 14.8s 15.4s 1.040 0.719
sql 29 4.9s 4.1s 0.841 0.979
mapa_card 109 192.4s 197.0s 1.024 0.997
all 482 347.2s 352.6s 1.016 0.990

Ratios below 1.00 mean the branch is faster. The median per-instance ratio ignores instances under 0.05s, where timer noise dominates.

Solved only by liastar7_no_lift_lambda (c201ecf) (0)

Solved only by liastar7 (046355d) (0)

cactus_results cactus_results_pooled scatter_results

Co-Authored-By: Claude Opus 5 noreply@anthropic.com

@mudathirmahgoub mudathirmahgoub mentioned this pull request Oct 13, 2026
Merged
mudathirmahgoub added a commit to mudathirmahgoub/cvc5 that referenced this pull request Oct 15, 2026
@mudathirmahgoub
Cactus plot: rel.cyclic-pattern with and without cvc5#13017
105e099
@mudathirmahgoub mudathirmahgoub mentioned this pull request Oct 15, 2026
Open
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@mudathirmahgoub mudathirmahgoub Awaiting requested review from mudathirmahgoub

At least 1 approving review is required to merge this pull request.

Assignees

@mudathirmahgoub mudathirmahgoub

Labels

moderate Complexity normal Priority

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

2 participants

@ajreynol @mudathirmahgoub