322 feature request clone proverenvironment with stack #324
Conversation
…thInterpolation() to the SolverContext (and all variations of it) + an implementation for Z3
…vers that do not support this feature
| * @param options Options specified for the prover environment. All the options specified in | ||
| * {@link ProverOptions} are turned off by default. | ||
| */ | ||
| ProverEnvironment copyProverEnvironment(ProverEnvironment proverToCopy, ProverOptions... options); |
There was a problem hiding this comment.
Leaving the options open for the user might introduce problems, when it comes to featuers like unsat-core and interpolation, because we need to provide tokens/ids for all pushed assertions.
There was a problem hiding this comment.
So you would suggest to always copy the options 1:1?
There was a problem hiding this comment.
If the method should copy a stack and (as optimization) also the solver-internal data, then I would assume that the Prover requires identical options.
However, if we keep this open for the user and are able to copy all assertions directly onto another Prover, and limit the internal optimization to only the case of identical options, then we could cover more potential use-cases, e.g., if a user wants to enable unsat-cores or interpolants later. We need to specify this in the API.
There was a problem hiding this comment.
I removed the options for now. We may want to test if it is possible to alter the options in copied provers first.
| * {@link ProverOptions} are turned off by default. | ||
| */ | ||
| InterpolatingProverEnvironment<?> copyProverEnvironmentWithInterpolation( | ||
| ProverEnvironment proverToCopy, ProverOptions... options); |
There was a problem hiding this comment.
Leaving the options open for the user might introduce problems, when it comes to featuers like unsat-core and interpolation, because we need to provide tokens/ids for all pushed assertions.
There was a problem hiding this comment.
Why is there no copy-method for the OptimizationProver? The current API is incomplete.
There was a problem hiding this comment.
It might be better to provide a copy-method/copy-constructor directly in the ProverEnvironment, because it knows best how to copy its content. The current naming scheme is quite verbous.
There was a problem hiding this comment.
I agree with you on all things.
However, Z3 needs permanent saving of references for the copied prover. Since we can't guarantee that the original prover is not closed, we need to save them in the context.
Of course we could do this via a method as well.
There was a problem hiding this comment.
If Z3 requires permanent memory-tracking for the base-solver and does not allow closing it, then the copy-method is broken by design. Are you sure that there is no bug in using the copy-method?
There was a problem hiding this comment.
I don't think its permanent memory tracking for the base solver, i think the ghost references prevent garbage collection in case a old solver is closed. Hence why i save them in the context.
And i am pretty sure that there is no bug, at least for the ghost reference part. Still, i will write a Z3 Java program to test it.
There was a problem hiding this comment.
If we copy a solver, I would assume that the new solver-instance increments all internal references on its own to avoid garbage-collection in case the old solver-instance is closed. I do not see a requirement for JavaSMT to keep track of the old solver-instance.
| "Solver %s does not support prover copying for non-base-level provers", | ||
| solverToUse()) | ||
| .that(solverToUse()) | ||
| .isNotEqualTo(Solvers.Z3); |
There was a problem hiding this comment.
I do not understand this test: Is the whole copying-thing working or not?
There was a problem hiding this comment.
Yes. For a stack that has not been pushed according to the error message. Which makes it unusable for the use-case of Thomas. I've updated the discussion in the Z3 repo to find out if i made a mistake or if this is intended behavior.
|
By the way, with your additions in #325 , we could easily provide a default implementation for this feature. |
|
Another question: what happens to the returned tokens (formula-names or partition-ids or random ids) related to added/pushed constraints for interpolation? Are the old tokens also valid in the new environment, or is a user required to get new ones (and how should that happen?)? |
I've added two methods to copy a prover to the solver context with an implementation for Z3 including tests.
Note: it seems like Z3 supports this only for the base level (no pushs to the assertion stack).