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.

Sign up for GitHub

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

Jump to bottom

[FEATURE] Remove unused let-definitions #995

Closed
konnov opened this issue Sep 21, 2021 · 0 comments · Fixed by #997
Closed

[FEATURE] Remove unused let-definitions #995

konnov opened this issue Sep 21, 2021 · 0 comments · Fixed by #997
Assignees
@konnov
Labels
Fprepro Feature: TLA+ preprocessor new New issue to be triaged. refactoring
Milestone
September iteration

Comments

@konnov
Copy link
Collaborator

konnov commented Sep 21, 2021

The recent fix of Skolemization #985 introduces two let-definitions for each let-definition: a skolemized one and an unskolemized one. While the produced TLA+ specification is equivalent to an original one, it sometimes contains unused let-definitions. This may lead to performance issues, as both definitions are still translated to SMT.
@konnov konnov added new New issue to be triaged. refactoring Fprepro Feature: TLA+ preprocessor labels Sep 21, 2021
@konnov konnov added this to the September iteration milestone Sep 21, 2021
@konnov konnov self-assigned this Sep 21, 2021
konnov added a commit that referenced this issue Sep 21, 2021
@konnov
closes #995: remove unused let-definitions
8500ebf
@konnov konnov mentioned this issue Sep 21, 2021
Merged
4 tasks
@apalache-bot apalache-bot mentioned this issue Sep 27, 2021
Merged
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@konnov konnov

Labels
Fprepro Feature: TLA+ preprocessor new New issue to be triaged. refactoring
Projects
None yet
Milestone
September iteration
Development

Successfully merging a pull request may close this issue.

Remove unused let definitions apalache-mc/apalache
1 participant
@konnov