Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

faster PCUICSR #1081

Open
wants to merge 1 commit into
base: main
Choose a base branch
from
Open

faster PCUICSR #1081

wants to merge 1 commit into from

Conversation

mrhaandi
Copy link
Contributor

@mrhaandi mrhaandi commented May 8, 2024

Replaced slow firstorder calls by appropriate constructor, left, right calls.
This improves performance from
5m49.68s | 2644580 ko | PCUICSR.vo
to
0m49.37s | 1443968 ko | PCUICSR.vo,
also improving overall project compilation speed.

@TheoWinterhalter
Copy link
Member

I'm amazed that it's only two occurrences that take up that long!

@ppedrot
Copy link
Collaborator

ppedrot commented May 9, 2024

FTR I have had firstorder on my radar for a while. It's very inefficient because it strongly normalizes all terms from the context. (It's a bit sad that these instances will disappear for benching purposes, btw.)

@TheoWinterhalter
Copy link
Member

Would that be reason enough to keep them though? Could we keep them as a special CI that only runs for benchmarks?

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.

None yet

3 participants