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

322 feature request clone proverenvironment with stack #324

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

322 feature request clone proverenvironment with stack #324

Show file tree
Hide file tree
Changes from 11 commits
Commits
Show all changes
13 commits
Select commit Hold shift + click to select a range
e6c380c
Add the API calls copyProverEnvironment() and copyProverEnvironmentWi…
Jul 31, 2023
d36cb96
Add tests for prover copying and utility methods to avoid testing sol…
Jul 31, 2023
8f86ab1
Suppress ressource warnings for the new copy prover API
Jul 31, 2023
0dfb3e7
Improve tests for new copy prover API
Jul 31, 2023
0fd372f
Add missing @Test annotation to prover copy test
Jul 31, 2023
4881e3c
Remove redundant final modifier from Z3 context
Jul 31, 2023
9193dd6
Don't use a try catch block for a test that requires a manual close()
Jul 31, 2023
198e7b2
Fix wrong constructor usage for Z3 copied theorem prover
Jul 31, 2023
98303fb
Fix type used for a Map in Z3 solver context to use the explicit type
Jul 31, 2023
e217830
Suppress warning for ressource (try-catch block) as we need it for a …
Jul 31, 2023
f63ec0e
Disable a test for prover copying after push for Z3 as it can't handl…
Jul 31, 2023
d614169
Improve Z3AbstractProver constructor and cleanup
Aug 1, 2023
28cc2fb
Add copy for OptimizationProver and remove options argument from copy…
Aug 1, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
28 changes: 28 additions & 0 deletions src/org/sosy_lab/java_smt/api/SolverContext.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -65,6 +65,18 @@ enum ProverOptions {
*/
ProverEnvironment newProverEnvironment(ProverOptions... options);

/**
* Create a new {@link ProverEnvironment} which encapsulates an assertion stack and can be used to
* check formulas for unsatisfiability, but retains the current assertion stack of the given
* {@link ProverEnvironment}.
*
* @param proverToCopy An existing {@link ProverEnvironment}, whichs assertion stack is to be
* copied into the new one.
* @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 •
edited
Loading

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.


/**
* Create a fresh new {@link InterpolatingProverEnvironment} which encapsulates an assertion stack
* and allows generating and retrieve interpolants for unsatisfiable formulas. If the SMT solver
Expand All @@ -76,6 +88,22 @@ enum ProverOptions {
*/
InterpolatingProverEnvironment<?> newProverEnvironmentWithInterpolation(ProverOptions... options);

/**
* Create a fresh new {@link InterpolatingProverEnvironment} which encapsulates an assertion stack
* and allows generating and retrieve interpolants for unsatisfiable formulas. The new {@link
* ProverEnvironment} retains the current assertion stack of the given {@link ProverEnvironment}.
* If the SMT solver is able to handle satisfiability tests with assumptions please consider
* implementing the {@link InterpolatingProverEnvironment} interface, and return an Object of this
* type here.
*
* @param proverToCopy An existing {@link ProverEnvironment}, whichs assertion stack is to be
* copied into the new one.
* @param options Options specified for the prover environment. All the options specified in
* {@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 •
edited
Loading

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.


/**
* Create a fresh new {@link OptimizationProverEnvironment} which encapsulates an assertion stack
* and allows solving optimization queries.
Expand Down
33 changes: 33 additions & 0 deletions src/org/sosy_lab/java_smt/basicimpl/AbstractSolverContext.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -46,8 +46,23 @@ public final ProverEnvironment newProverEnvironment(ProverOptions... options) {
return out;
}

@Override
public final ProverEnvironment copyProverEnvironment(
ProverEnvironment proverToCopy, ProverOptions... options) {
ProverEnvironment out = copyProverEnvironment0(proverToCopy, toSet(options));
if (!supportsAssumptionSolving()) {
// In the case we do not already have a prover environment with assumptions,
// we add a wrapper to it
out = new ProverWithAssumptionsWrapper(out);
}
return out;
}

protected abstract ProverEnvironment newProverEnvironment0(Set<ProverOptions> options);

protected abstract ProverEnvironment copyProverEnvironment0(
ProverEnvironment proverToCopy, Set<ProverOptions> options);

@SuppressWarnings("resource")
@Override
public final InterpolatingProverEnvironment<?> newProverEnvironmentWithInterpolation(
Expand All @@ -62,9 +77,27 @@ public final InterpolatingProverEnvironment<?> newProverEnvironmentWithInterpola
return out;
}

@SuppressWarnings("resource")
@Override
public final InterpolatingProverEnvironment<?> copyProverEnvironmentWithInterpolation(
ProverEnvironment proverToCopy, ProverOptions... options) {

InterpolatingProverEnvironment<?> out =
copyProverEnvironmentWithInterpolation0(proverToCopy, toSet(options));
if (!supportsAssumptionSolving()) {
// In the case we do not already have a prover environment with assumptions,
// we add a wrapper to it
out = new InterpolatingProverWithAssumptionsWrapper<>(out, fmgr);
}
return out;
}

protected abstract InterpolatingProverEnvironment<?> newProverEnvironmentWithInterpolation0(
Set<ProverOptions> pSet);

protected abstract InterpolatingProverEnvironment<?> copyProverEnvironmentWithInterpolation0(
ProverEnvironment proverToCopy, Set<ProverOptions> pSet);

@SuppressWarnings("resource")
@Override
public final OptimizationProverEnvironment newOptimizationProverEnvironment(
Expand Down
18 changes: 18 additions & 0 deletions src/org/sosy_lab/java_smt/delegate/logging/LoggingSolverContext.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -41,6 +41,15 @@ public ProverEnvironment newProverEnvironment(ProverOptions... pOptions) {
return new LoggingProverEnvironment(logger, delegate.newProverEnvironment(pOptions));
}

@SuppressWarnings("resource")
@Override
public ProverEnvironment copyProverEnvironment(
ProverEnvironment proverToCopy, ProverOptions... options) {
// TODO: log this? Because this is not a normal new prover?
return new LoggingProverEnvironment(
logger, delegate.copyProverEnvironment(proverToCopy, options));
}

@SuppressWarnings("resource")
@Override
public InterpolatingProverEnvironment<?> newProverEnvironmentWithInterpolation(
Expand All @@ -49,6 +58,15 @@ public InterpolatingProverEnvironment<?> newProverEnvironmentWithInterpolation(
logger, delegate.newProverEnvironmentWithInterpolation(options));
}

@SuppressWarnings("resource")
@Override
public InterpolatingProverEnvironment<?> copyProverEnvironmentWithInterpolation(
ProverEnvironment proverToCopy, ProverOptions... options) {
// TODO: log this? Because this is not a normal new prover?
return new LoggingInterpolatingProverEnvironment<>(
logger, delegate.copyProverEnvironmentWithInterpolation(proverToCopy, options));
}

@SuppressWarnings("resource")
@Override
public OptimizationProverEnvironment newOptimizationProverEnvironment(ProverOptions... options) {
Expand Down
16 changes: 16 additions & 0 deletions src/org/sosy_lab/java_smt/delegate/statistics/StatisticsSolverContext.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -39,6 +39,14 @@ public ProverEnvironment newProverEnvironment(ProverOptions... pOptions) {
return new StatisticsProverEnvironment(delegate.newProverEnvironment(pOptions), stats);
}

@SuppressWarnings("resource")
@Override
public ProverEnvironment copyProverEnvironment(
ProverEnvironment proverToCopy, ProverOptions... options) {
return new StatisticsProverEnvironment(
delegate.copyProverEnvironment(proverToCopy, options), stats);
}

@SuppressWarnings("resource")
@Override
public InterpolatingProverEnvironment<?> newProverEnvironmentWithInterpolation(
Expand All @@ -47,6 +55,14 @@ public InterpolatingProverEnvironment<?> newProverEnvironmentWithInterpolation(
delegate.newProverEnvironmentWithInterpolation(pOptions), stats);
}

@SuppressWarnings("resource")
@Override
public InterpolatingProverEnvironment<?> copyProverEnvironmentWithInterpolation(
ProverEnvironment proverToCopy, ProverOptions... options) {
return new StatisticsInterpolatingProverEnvironment<>(
delegate.copyProverEnvironmentWithInterpolation(proverToCopy, options), stats);
}

@SuppressWarnings("resource")
@Override
public OptimizationProverEnvironment newOptimizationProverEnvironment(ProverOptions... pOptions) {
Expand Down
38 changes: 38 additions & 0 deletions src/org/sosy_lab/java_smt/delegate/synchronize/SynchronizedSolverContext.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -94,6 +94,25 @@ public ProverEnvironment newProverEnvironment(ProverOptions... pOptions) {
}
}

@SuppressWarnings("resource")
@Override
public ProverEnvironment copyProverEnvironment(
ProverEnvironment proverToCopy, ProverOptions... options) {
synchronized (sync) {
if (useSeperateProvers) {
SolverContext otherContext = createOtherContext();
return new SynchronizedProverEnvironmentWithContext(
otherContext.copyProverEnvironment(proverToCopy, options),
sync,
delegate.getFormulaManager(),
otherContext.getFormulaManager());
} else {
return new SynchronizedProverEnvironment(
delegate.copyProverEnvironment(proverToCopy, options), delegate);
}
}
}

@SuppressWarnings("resource")
@Override
public InterpolatingProverEnvironment<?> newProverEnvironmentWithInterpolation(
Expand All @@ -113,6 +132,25 @@ public InterpolatingProverEnvironment<?> newProverEnvironmentWithInterpolation(
}
}

@SuppressWarnings("resource")
@Override
public InterpolatingProverEnvironment<?> copyProverEnvironmentWithInterpolation(
ProverEnvironment proverToCopy, ProverOptions... options) {
synchronized (sync) {
if (useSeperateProvers) {
SolverContext otherContext = createOtherContext();
return new SynchronizedInterpolatingProverEnvironmentWithContext<>(
otherContext.copyProverEnvironmentWithInterpolation(proverToCopy, options),
sync,
delegate.getFormulaManager(),
otherContext.getFormulaManager());
} else {
return new SynchronizedInterpolatingProverEnvironment<>(
delegate.copyProverEnvironmentWithInterpolation(proverToCopy, options), delegate);
}
}
}

@SuppressWarnings("resource")
@Override
public OptimizationProverEnvironment newOptimizationProverEnvironment(ProverOptions... pOptions) {
Expand Down
14 changes: 14 additions & 0 deletions src/org/sosy_lab/java_smt/solvers/boolector/BoolectorSolverContext.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -204,12 +204,26 @@ protected ProverEnvironment newProverEnvironment0(Set<ProverOptions> pOptions) {
manager, creator, creator.getEnv(), shutdownNotifier, pOptions, isAnyStackAlive);
}

@Override
protected ProverEnvironment copyProverEnvironment0(
ProverEnvironment proverToCopy, Set<ProverOptions> options) {
throw new UnsupportedOperationException(
"Boolector does not support the copying of " + "ProverEnvironments");
}

@Override
protected InterpolatingProverEnvironment<?> newProverEnvironmentWithInterpolation0(
Set<ProverOptions> pSet) {
throw new UnsupportedOperationException("Boolector does not support interpolation");
}

@Override
protected InterpolatingProverEnvironment<?> copyProverEnvironmentWithInterpolation0(
ProverEnvironment proverToCopy, Set<ProverOptions> pSet) {
throw new UnsupportedOperationException(
"Boolector does not support the copying of " + "ProverEnvironments");
}

@Override
protected OptimizationProverEnvironment newOptimizationProverEnvironment0(
Set<ProverOptions> pSet) {
Expand Down
14 changes: 14 additions & 0 deletions src/org/sosy_lab/java_smt/solvers/cvc4/CVC4SolverContext.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -137,6 +137,13 @@ public ProverEnvironment newProverEnvironment0(Set<ProverOptions> pOptions) {
getFormulaManager().getBooleanFormulaManager());
}

@Override
protected ProverEnvironment copyProverEnvironment0(
ProverEnvironment proverToCopy, Set<ProverOptions> options) {
throw new UnsupportedOperationException(
"CVC4 does not support the copying of " + "ProverEnvironments");
}

@Override
protected boolean supportsAssumptionSolving() {
return false;
Expand All @@ -148,6 +155,13 @@ protected InterpolatingProverEnvironment<?> newProverEnvironmentWithInterpolatio
throw new UnsupportedOperationException("CVC4 does not support interpolation");
}

@Override
protected InterpolatingProverEnvironment<?> copyProverEnvironmentWithInterpolation0(
ProverEnvironment proverToCopy, Set<ProverOptions> pSet) {
throw new UnsupportedOperationException(
"CVC4 does not support the copying of " + "ProverEnvironments");
}

@Override
protected OptimizationProverEnvironment newOptimizationProverEnvironment0(
Set<ProverOptions> pSet) {
Expand Down
14 changes: 14 additions & 0 deletions src/org/sosy_lab/java_smt/solvers/cvc5/CVC5SolverContext.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -157,6 +157,13 @@ public ProverEnvironment newProverEnvironment0(Set<ProverOptions> pOptions) {
creator, shutdownNotifier, randomSeed, pOptions, getFormulaManager());
}

@Override
protected ProverEnvironment copyProverEnvironment0(
ProverEnvironment proverToCopy, Set<ProverOptions> options) {
throw new UnsupportedOperationException(
"CVC5 does not support the copying of " + "ProverEnvironments");
}

@Override
protected boolean supportsAssumptionSolving() {
return false;
Expand All @@ -168,6 +175,13 @@ protected InterpolatingProverEnvironment<?> newProverEnvironmentWithInterpolatio
throw new UnsupportedOperationException("CVC5 does not support Craig interpolation.");
}

@Override
protected InterpolatingProverEnvironment<?> copyProverEnvironmentWithInterpolation0(
ProverEnvironment proverToCopy, Set<ProverOptions> pSet) {
throw new UnsupportedOperationException(
"CVC5 does not support the copying of " + "ProverEnvironments");
}

@Override
protected OptimizationProverEnvironment newOptimizationProverEnvironment0(
Set<ProverOptions> pSet) {
Expand Down
14 changes: 14 additions & 0 deletions src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5SolverContext.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -266,13 +266,27 @@ protected ProverEnvironment newProverEnvironment0(Set<ProverOptions> options) {
return new Mathsat5TheoremProver(this, shutdownNotifier, creator, options);
}

@Override
protected ProverEnvironment copyProverEnvironment0(
ProverEnvironment proverToCopy, Set<ProverOptions> options) {
throw new UnsupportedOperationException(
"MathSAT5 does not support copying of prover " + "environments");
}

@Override
protected InterpolatingProverEnvironment<?> newProverEnvironmentWithInterpolation0(
Set<ProverOptions> options) {
Preconditions.checkState(!closed, "solver context is already closed");
return new Mathsat5InterpolatingProver(this, shutdownNotifier, creator, options);
}

@Override
protected InterpolatingProverEnvironment<?> copyProverEnvironmentWithInterpolation0(
ProverEnvironment proverToCopy, Set<ProverOptions> pSet) {
throw new UnsupportedOperationException(
"MathSAT5 does not support copying of prover " + "environments");
}

@Override
public OptimizationProverEnvironment newOptimizationProverEnvironment0(
Set<ProverOptions> options) {
Expand Down
14 changes: 14 additions & 0 deletions src/org/sosy_lab/java_smt/solvers/princess/PrincessSolverContext.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -77,6 +77,13 @@ protected ProverEnvironment newProverEnvironment0(Set<ProverOptions> options) {
return (PrincessTheoremProver) creator.getEnv().getNewProver(false, manager, creator, options);
}

@Override
protected ProverEnvironment copyProverEnvironment0(
ProverEnvironment proverToCopy, Set<ProverOptions> options) {
throw new UnsupportedOperationException(
"Princess does not support the copying of " + "ProverEnvironments");
}

@SuppressWarnings("resource")
@Override
protected InterpolatingProverEnvironment<?> newProverEnvironmentWithInterpolation0(
Expand All @@ -85,6 +92,13 @@ protected InterpolatingProverEnvironment<?> newProverEnvironmentWithInterpolatio
creator.getEnv().getNewProver(true, manager, creator, options);
}

@Override
protected InterpolatingProverEnvironment<?> copyProverEnvironmentWithInterpolation0(
ProverEnvironment proverToCopy, Set<ProverOptions> pSet) {
throw new UnsupportedOperationException(
"Princess does not support the copying of " + "ProverEnvironments");
}

@Override
public OptimizationProverEnvironment newOptimizationProverEnvironment0(
Set<ProverOptions> options) {
Expand Down
14 changes: 14 additions & 0 deletions src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolSolverContext.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -231,6 +231,13 @@ protected ProverEnvironment newProverEnvironment0(Set<ProverOptions> options) {
return new SmtInterpolTheoremProver(manager, newScript, options, shutdownNotifier);
}

@Override
protected ProverEnvironment copyProverEnvironment0(
ProverEnvironment proverToCopy, Set<ProverOptions> options) {
throw new UnsupportedOperationException(
"SMTInterpol does not support the copying of " + "ProverEnvironments");
}

@SuppressWarnings("resource")
@Override
protected InterpolatingProverEnvironment<?> newProverEnvironmentWithInterpolation0(
Expand All @@ -252,6 +259,13 @@ protected InterpolatingProverEnvironment<?> newProverEnvironmentWithInterpolatio
return prover;
}

@Override
protected InterpolatingProverEnvironment<?> copyProverEnvironmentWithInterpolation0(
ProverEnvironment proverToCopy, Set<ProverOptions> pSet) {
throw new UnsupportedOperationException(
"SMTInterpol does not support the copying of " + "ProverEnvironments");
}

@Override
public OptimizationProverEnvironment newOptimizationProverEnvironment0(
Set<ProverOptions> options) {
Expand Down
Loading