Persist solver #1075
Merged
Persist solver #1075
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
The solver instance is now passed down into the typechecking actions from outside rather than being created on each invocation of a typechecking action. Likewise, the solver has been pulled out as a parameter of the `ModuleInput` record that is passed into a `ModuleCmd`. At present, these are still created fresh for each module command inside `liftModuleCmd`. However, it would be relatively easy to continue this lifting process and persist the solver across and entire REPL session. The current refactoring should, I believe, be sufficent to address GaloisInc/saw-script#953 Fixes #996
for typechecking purposes. This may be convenient for users of Cryptol-as-a-library who need to manage their own resources.
brianhuffman
approved these changes
Feb 16, 2021
brianhuffman
pushed a commit
to GaloisInc/saw-core
that referenced
this pull request
Mar 2, 2021
brianhuffman
pushed a commit
to GaloisInc/saw-script
that referenced
this pull request
Mar 3, 2021
The following included cryptol PRs required changes to saw-script: - GaloisInc/cryptol#1077 "nopat-refactor" - GaloisInc/cryptol#1075 "persist-solver"
brianhuffman
pushed a commit
to GaloisInc/saw-script
that referenced
this pull request
Mar 3, 2021
The following included cryptol PRs required changes to saw-script: - GaloisInc/cryptol#1077 "nopat-refactor" - GaloisInc/cryptol#1075 "persist-solver"
brianhuffman
pushed a commit
to GaloisInc/saw-script
that referenced
this pull request
Mar 4, 2021
The following included cryptol PRs required changes to saw-script: - GaloisInc/cryptol#1077 "nopat-refactor" - GaloisInc/cryptol#1075 "persist-solver"
brianhuffman
pushed a commit
to GaloisInc/saw-script
that referenced
this pull request
Mar 8, 2021
The following included cryptol PRs required changes to saw-script: - GaloisInc/cryptol#1077 "nopat-refactor" - GaloisInc/cryptol#1075 "persist-solver"
brianhuffman
pushed a commit
to GaloisInc/saw-script
that referenced
this pull request
Mar 8, 2021
The following included cryptol PRs required changes to saw-script: - GaloisInc/cryptol#1077 "nopat-refactor" - GaloisInc/cryptol#1075 "persist-solver"
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Refactor the use of SMT solvers for typechecking to allow for the solver instances to be reused for a longer period.