Skip to content
This repository has been archived by the owner on Jun 9, 2021. It is now read-only.

Adapt to GaloisInc/cryptol#1128 "persistent-solver2". #197

Merged
merged 1 commit into from
Apr 22, 2021

Conversation

brianhuffman
Copy link
Contributor

No description provided.

@brianhuffman brianhuffman requested a review from robdockins April 8, 2021 00:26
@brianhuffman
Copy link
Contributor Author

The removal of meSolverConfig will require changes to the saw-script package as well.

@robdockins
Copy link
Contributor

This seems OK to me. Although, there is an alternate design we could consider: should the solver instance just be stored in the CryptolEnv? That would persist it for much longer, and may be what you want to do eventually anyway, as it will spawn solvers less often.

@robdockins robdockins mentioned this pull request Apr 16, 2021
@brianhuffman
Copy link
Contributor Author

I'll open a ticket suggesting to store the solver instance in the CryptolEnv. This PR is intended to preserve the existing behavior as much as possible, and we can add solver persistence later (perhaps after we figure out all the issues related to restarting solvers after Ctrl-C).

@brianhuffman
Copy link
Contributor Author

Instead of opening a new saw-core ticket, I just added some notes to GaloisInc/saw-script#953, which is already asking for this exact feature.

@brianhuffman brianhuffman merged commit 1c05dc0 into master Apr 22, 2021
@brianhuffman brianhuffman deleted the persist-solver2 branch April 22, 2021 21:14
brianhuffman pushed a commit to GaloisInc/saw-script that referenced this pull request Apr 26, 2021
This patch includes the following submodule PRs:
- GaloisInc/cryptol#1128 "persist-solver2"
- GaloisInc/saw-core#197 "persist-solver2"
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants