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.

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

322 feature request clone proverenvironment with stack #324

Open
wants to merge 13 commits into
base: master
Choose a base branch
from

Conversation

baierd
Copy link
Collaborator

@baierd baierd commented Jul 31, 2023

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).

* @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);
Copy link
Member

@kfriedberger kfriedberger Jul 31, 2023

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

So you would suggest to always copy the options 1:1?

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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);
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Why is there no copy-method for the OptimizationProver? The current API is incomplete.

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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?

Copy link
Collaborator Author

@baierd baierd Aug 2, 2023

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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);
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I do not understand this test: Is the whole copying-thing working or not?

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

@baierd
Copy link
Collaborator Author

baierd commented Aug 2, 2023

By the way, with your additions in #325 , we could easily provide a default implementation for this feature.

@kfriedberger
Copy link
Member

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?)?

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Development

Successfully merging this pull request may close these issues.

Feature Request: Clone ProverEnvironment with Stack
2 participants