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

Refactor Z3SolverContext caches #1595

Closed
rodrigo7491 opened this issue Apr 5, 2022 · 0 comments · Fixed by #1703
Closed

Refactor Z3SolverContext caches #1595

rodrigo7491 opened this issue Apr 5, 2022 · 0 comments · Fixed by #1703
Assignees
@rodrigo7491
Labels
Farrays Feature: New SMT encoding with arrays refactoring
Milestone
X1: Arrays Encoding

Comments

@rodrigo7491
Copy link
Collaborator

As pointer out by @konnov during work on #1589, the handling of caches in Z3SolverContext is currently a bit brittle. The issue revolves around the update of mutable maps that deal with lists, e.g., cellCache. One idea is to use filterInPlace for ListBuffer, added in Scala 2.13. It has the same semantics of the deprecated retain for HashMap, with HashMap also using filterInPlace in Scala 2.13. Due to the version requirement, this is conditional on #1509.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@rodrigo7491 rodrigo7491

Labels
Farrays Feature: New SMT encoding with arrays refactoring
Projects
None yet
Milestone
X1: Arrays Encoding
Development

Successfully merging a pull request may close this issue.

Refactor Z3SolverContext cellCache apalache-mc/apalache
1 participant
@rodrigo7491