Skip to content

Use lazily expanding flat term everywhere and clean up class#834

Open
mezpusz wants to merge 2 commits intomasterfrom
clean-up-flatterm
Open

Use lazily expanding flat term everywhere and clean up class#834
mezpusz wants to merge 2 commits intomasterfrom
clean-up-flatterm

Conversation

@mezpusz
Copy link
Copy Markdown
Contributor

@mezpusz mezpusz commented Mar 27, 2026

I got around to fixing the lazily expanded flat term variant to literals too, which means I could remove the other variant completely and simplify the code a bit.

Minor but relatively stable improvement (mostly for SAT) for both Discount and Otter over FOL TPTP with one seemingly flipping problem instance in both (maybe @quickbeam123 's more stable measurement is needed here. ;)):

Discount:

run 0 unsat: 9208 (1) sat: 1032 (0) cputime: 57559.88 s instructions: 222882769 Mi memory: 1452257.26 MB
run 1 unsat: 9208 (1) sat: 1042 (10) cputime: 57305.22 s instructions: 222743871 Mi memory: 1461347.47 MB

Otter:

run 0 unsat: 9320 (1) sat: 1021 (0) cputime: 62631.56 s instructions: 222819399 Mi memory: 1684459.84 MB
run 1 unsat: 9320 (1) sat: 1025 (4) cputime: 62627.07 s instructions: 222755867 Mi memory: 1693718.59 MB

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant