From e6c380caec1821756deec6c862abebd966159176 Mon Sep 17 00:00:00 2001 From: BaierD Date: Mon, 31 Jul 2023 13:36:31 +0200 Subject: [PATCH 01/13] Add the API calls copyProverEnvironment() and copyProverEnvironmentWithInterpolation() to the SolverContext (and all variations of it) + an implementation for Z3 --- .../sosy_lab/java_smt/api/SolverContext.java | 28 +++++++ .../basicimpl/AbstractSolverContext.java | 32 ++++++++ .../logging/LoggingSolverContext.java | 16 ++++ .../statistics/StatisticsSolverContext.java | 14 ++++ .../SynchronizedSolverContext.java | 36 +++++++++ .../boolector/BoolectorSolverContext.java | 14 ++++ .../solvers/cvc4/CVC4SolverContext.java | 14 ++++ .../solvers/cvc5/CVC5SolverContext.java | 14 ++++ .../mathsat5/Mathsat5SolverContext.java | 14 ++++ .../princess/PrincessSolverContext.java | 14 ++++ .../smtinterpol/SmtInterpolSolverContext.java | 14 ++++ .../solvers/yices2/Yices2SolverContext.java | 14 ++++ .../java_smt/solvers/z3/Z3AbstractProver.java | 33 ++++++++ .../java_smt/solvers/z3/Z3SolverContext.java | 79 ++++++++++++++++--- .../java_smt/solvers/z3/Z3TheoremProver.java | 11 +++ 15 files changed, 334 insertions(+), 13 deletions(-) diff --git a/src/org/sosy_lab/java_smt/api/SolverContext.java b/src/org/sosy_lab/java_smt/api/SolverContext.java index 3fbd476c77..3bbd32384b 100644 --- a/src/org/sosy_lab/java_smt/api/SolverContext.java +++ b/src/org/sosy_lab/java_smt/api/SolverContext.java @@ -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); + /** * Create a fresh new {@link InterpolatingProverEnvironment} which encapsulates an assertion stack * and allows generating and retrieve interpolants for unsatisfiable formulas. If the SMT solver @@ -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); + /** * Create a fresh new {@link OptimizationProverEnvironment} which encapsulates an assertion stack * and allows solving optimization queries. diff --git a/src/org/sosy_lab/java_smt/basicimpl/AbstractSolverContext.java b/src/org/sosy_lab/java_smt/basicimpl/AbstractSolverContext.java index ab49b14cfc..8ec09feb25 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/AbstractSolverContext.java +++ b/src/org/sosy_lab/java_smt/basicimpl/AbstractSolverContext.java @@ -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 options); + protected abstract ProverEnvironment copyProverEnvironment0( + ProverEnvironment proverToCopy, Set options); + @SuppressWarnings("resource") @Override public final InterpolatingProverEnvironment newProverEnvironmentWithInterpolation( @@ -62,9 +77,26 @@ public final InterpolatingProverEnvironment newProverEnvironmentWithInterpola return out; } + @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 pSet); + protected abstract InterpolatingProverEnvironment copyProverEnvironmentWithInterpolation0( + ProverEnvironment proverToCopy, Set pSet); + @SuppressWarnings("resource") @Override public final OptimizationProverEnvironment newOptimizationProverEnvironment( diff --git a/src/org/sosy_lab/java_smt/delegate/logging/LoggingSolverContext.java b/src/org/sosy_lab/java_smt/delegate/logging/LoggingSolverContext.java index b68b9e8c5b..f35cc2f46a 100644 --- a/src/org/sosy_lab/java_smt/delegate/logging/LoggingSolverContext.java +++ b/src/org/sosy_lab/java_smt/delegate/logging/LoggingSolverContext.java @@ -41,6 +41,14 @@ public ProverEnvironment newProverEnvironment(ProverOptions... pOptions) { return new LoggingProverEnvironment(logger, delegate.newProverEnvironment(pOptions)); } + @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( @@ -49,6 +57,14 @@ public InterpolatingProverEnvironment newProverEnvironmentWithInterpolation( logger, delegate.newProverEnvironmentWithInterpolation(options)); } + @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) { diff --git a/src/org/sosy_lab/java_smt/delegate/statistics/StatisticsSolverContext.java b/src/org/sosy_lab/java_smt/delegate/statistics/StatisticsSolverContext.java index 214d2dd576..b1bc76460b 100644 --- a/src/org/sosy_lab/java_smt/delegate/statistics/StatisticsSolverContext.java +++ b/src/org/sosy_lab/java_smt/delegate/statistics/StatisticsSolverContext.java @@ -39,6 +39,13 @@ public ProverEnvironment newProverEnvironment(ProverOptions... pOptions) { return new StatisticsProverEnvironment(delegate.newProverEnvironment(pOptions), stats); } + @Override + public ProverEnvironment copyProverEnvironment( + ProverEnvironment proverToCopy, ProverOptions... options) { + return new StatisticsProverEnvironment( + delegate.copyProverEnvironment(proverToCopy, options), stats); + } + @SuppressWarnings("resource") @Override public InterpolatingProverEnvironment newProverEnvironmentWithInterpolation( @@ -47,6 +54,13 @@ public InterpolatingProverEnvironment newProverEnvironmentWithInterpolation( delegate.newProverEnvironmentWithInterpolation(pOptions), stats); } + @Override + public InterpolatingProverEnvironment copyProverEnvironmentWithInterpolation( + ProverEnvironment proverToCopy, ProverOptions... options) { + return new StatisticsInterpolatingProverEnvironment<>( + delegate.copyProverEnvironmentWithInterpolation(proverToCopy, options), stats); + } + @SuppressWarnings("resource") @Override public OptimizationProverEnvironment newOptimizationProverEnvironment(ProverOptions... pOptions) { diff --git a/src/org/sosy_lab/java_smt/delegate/synchronize/SynchronizedSolverContext.java b/src/org/sosy_lab/java_smt/delegate/synchronize/SynchronizedSolverContext.java index bea5a9fb00..9cfb3f4ca3 100644 --- a/src/org/sosy_lab/java_smt/delegate/synchronize/SynchronizedSolverContext.java +++ b/src/org/sosy_lab/java_smt/delegate/synchronize/SynchronizedSolverContext.java @@ -94,6 +94,24 @@ public ProverEnvironment newProverEnvironment(ProverOptions... pOptions) { } } + @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( @@ -113,6 +131,24 @@ public InterpolatingProverEnvironment newProverEnvironmentWithInterpolation( } } + @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) { diff --git a/src/org/sosy_lab/java_smt/solvers/boolector/BoolectorSolverContext.java b/src/org/sosy_lab/java_smt/solvers/boolector/BoolectorSolverContext.java index 6c90828e93..9143fbfdc2 100644 --- a/src/org/sosy_lab/java_smt/solvers/boolector/BoolectorSolverContext.java +++ b/src/org/sosy_lab/java_smt/solvers/boolector/BoolectorSolverContext.java @@ -204,12 +204,26 @@ protected ProverEnvironment newProverEnvironment0(Set pOptions) { manager, creator, creator.getEnv(), shutdownNotifier, pOptions, isAnyStackAlive); } + @Override + protected ProverEnvironment copyProverEnvironment0( + ProverEnvironment proverToCopy, Set options) { + throw new UnsupportedOperationException( + "Boolector does not support the copying of " + "ProverEnvironments"); + } + @Override protected InterpolatingProverEnvironment newProverEnvironmentWithInterpolation0( Set pSet) { throw new UnsupportedOperationException("Boolector does not support interpolation"); } + @Override + protected InterpolatingProverEnvironment copyProverEnvironmentWithInterpolation0( + ProverEnvironment proverToCopy, Set pSet) { + throw new UnsupportedOperationException( + "Boolector does not support the copying of " + "ProverEnvironments"); + } + @Override protected OptimizationProverEnvironment newOptimizationProverEnvironment0( Set pSet) { diff --git a/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4SolverContext.java b/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4SolverContext.java index b5bd086812..2766aec830 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4SolverContext.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4SolverContext.java @@ -137,6 +137,13 @@ public ProverEnvironment newProverEnvironment0(Set pOptions) { getFormulaManager().getBooleanFormulaManager()); } + @Override + protected ProverEnvironment copyProverEnvironment0( + ProverEnvironment proverToCopy, Set options) { + throw new UnsupportedOperationException( + "CVC4 does not support the copying of " + "ProverEnvironments"); + } + @Override protected boolean supportsAssumptionSolving() { return false; @@ -148,6 +155,13 @@ protected InterpolatingProverEnvironment newProverEnvironmentWithInterpolatio throw new UnsupportedOperationException("CVC4 does not support interpolation"); } + @Override + protected InterpolatingProverEnvironment copyProverEnvironmentWithInterpolation0( + ProverEnvironment proverToCopy, Set pSet) { + throw new UnsupportedOperationException( + "CVC4 does not support the copying of " + "ProverEnvironments"); + } + @Override protected OptimizationProverEnvironment newOptimizationProverEnvironment0( Set pSet) { diff --git a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5SolverContext.java b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5SolverContext.java index 03a99a65da..66a97e7e2b 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5SolverContext.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5SolverContext.java @@ -157,6 +157,13 @@ public ProverEnvironment newProverEnvironment0(Set pOptions) { creator, shutdownNotifier, randomSeed, pOptions, getFormulaManager()); } + @Override + protected ProverEnvironment copyProverEnvironment0( + ProverEnvironment proverToCopy, Set options) { + throw new UnsupportedOperationException( + "CVC5 does not support the copying of " + "ProverEnvironments"); + } + @Override protected boolean supportsAssumptionSolving() { return false; @@ -168,6 +175,13 @@ protected InterpolatingProverEnvironment newProverEnvironmentWithInterpolatio throw new UnsupportedOperationException("CVC5 does not support Craig interpolation."); } + @Override + protected InterpolatingProverEnvironment copyProverEnvironmentWithInterpolation0( + ProverEnvironment proverToCopy, Set pSet) { + throw new UnsupportedOperationException( + "CVC5 does not support the copying of " + "ProverEnvironments"); + } + @Override protected OptimizationProverEnvironment newOptimizationProverEnvironment0( Set pSet) { diff --git a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5SolverContext.java b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5SolverContext.java index 6c356e10cf..f69fec2ae9 100644 --- a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5SolverContext.java +++ b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5SolverContext.java @@ -266,6 +266,13 @@ protected ProverEnvironment newProverEnvironment0(Set options) { return new Mathsat5TheoremProver(this, shutdownNotifier, creator, options); } + @Override + protected ProverEnvironment copyProverEnvironment0( + ProverEnvironment proverToCopy, Set options) { + throw new UnsupportedOperationException( + "MathSAT5 does not support copying of prover " + "environments"); + } + @Override protected InterpolatingProverEnvironment newProverEnvironmentWithInterpolation0( Set options) { @@ -273,6 +280,13 @@ protected InterpolatingProverEnvironment newProverEnvironmentWithInterpolatio return new Mathsat5InterpolatingProver(this, shutdownNotifier, creator, options); } + @Override + protected InterpolatingProverEnvironment copyProverEnvironmentWithInterpolation0( + ProverEnvironment proverToCopy, Set pSet) { + throw new UnsupportedOperationException( + "MathSAT5 does not support copying of prover " + "environments"); + } + @Override public OptimizationProverEnvironment newOptimizationProverEnvironment0( Set options) { diff --git a/src/org/sosy_lab/java_smt/solvers/princess/PrincessSolverContext.java b/src/org/sosy_lab/java_smt/solvers/princess/PrincessSolverContext.java index 36a7444539..91f588fa95 100644 --- a/src/org/sosy_lab/java_smt/solvers/princess/PrincessSolverContext.java +++ b/src/org/sosy_lab/java_smt/solvers/princess/PrincessSolverContext.java @@ -77,6 +77,13 @@ protected ProverEnvironment newProverEnvironment0(Set options) { return (PrincessTheoremProver) creator.getEnv().getNewProver(false, manager, creator, options); } + @Override + protected ProverEnvironment copyProverEnvironment0( + ProverEnvironment proverToCopy, Set options) { + throw new UnsupportedOperationException( + "Princess does not support the copying of " + "ProverEnvironments"); + } + @SuppressWarnings("resource") @Override protected InterpolatingProverEnvironment newProverEnvironmentWithInterpolation0( @@ -85,6 +92,13 @@ protected InterpolatingProverEnvironment newProverEnvironmentWithInterpolatio creator.getEnv().getNewProver(true, manager, creator, options); } + @Override + protected InterpolatingProverEnvironment copyProverEnvironmentWithInterpolation0( + ProverEnvironment proverToCopy, Set pSet) { + throw new UnsupportedOperationException( + "Princess does not support the copying of " + "ProverEnvironments"); + } + @Override public OptimizationProverEnvironment newOptimizationProverEnvironment0( Set options) { diff --git a/src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolSolverContext.java b/src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolSolverContext.java index e9620756df..3fc0dc878d 100644 --- a/src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolSolverContext.java +++ b/src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolSolverContext.java @@ -231,6 +231,13 @@ protected ProverEnvironment newProverEnvironment0(Set options) { return new SmtInterpolTheoremProver(manager, newScript, options, shutdownNotifier); } + @Override + protected ProverEnvironment copyProverEnvironment0( + ProverEnvironment proverToCopy, Set options) { + throw new UnsupportedOperationException( + "SMTInterpol does not support the copying of " + "ProverEnvironments"); + } + @SuppressWarnings("resource") @Override protected InterpolatingProverEnvironment newProverEnvironmentWithInterpolation0( @@ -252,6 +259,13 @@ protected InterpolatingProverEnvironment newProverEnvironmentWithInterpolatio return prover; } + @Override + protected InterpolatingProverEnvironment copyProverEnvironmentWithInterpolation0( + ProverEnvironment proverToCopy, Set pSet) { + throw new UnsupportedOperationException( + "SMTInterpol does not support the copying of " + "ProverEnvironments"); + } + @Override public OptimizationProverEnvironment newOptimizationProverEnvironment0( Set options) { diff --git a/src/org/sosy_lab/java_smt/solvers/yices2/Yices2SolverContext.java b/src/org/sosy_lab/java_smt/solvers/yices2/Yices2SolverContext.java index c68e90aa3c..d7064c4c29 100644 --- a/src/org/sosy_lab/java_smt/solvers/yices2/Yices2SolverContext.java +++ b/src/org/sosy_lab/java_smt/solvers/yices2/Yices2SolverContext.java @@ -107,12 +107,26 @@ protected ProverEnvironment newProverEnvironment0(Set pOptions) { return new Yices2TheoremProver(creator, pOptions, bfmgr, shutdownManager); } + @Override + protected ProverEnvironment copyProverEnvironment0( + ProverEnvironment proverToCopy, Set options) { + throw new UnsupportedOperationException( + "Yices2 does not support the copying of " + "ProverEnvironments"); + } + @Override protected InterpolatingProverEnvironment newProverEnvironmentWithInterpolation0( Set pSet) { throw new UnsupportedOperationException("Yices does not support interpolation"); } + @Override + protected InterpolatingProverEnvironment copyProverEnvironmentWithInterpolation0( + ProverEnvironment proverToCopy, Set pSet) { + throw new UnsupportedOperationException( + "Yices2 does not support the copying of " + "ProverEnvironments"); + } + @Override protected OptimizationProverEnvironment newOptimizationProverEnvironment0( Set pSet) { diff --git a/src/org/sosy_lab/java_smt/solvers/z3/Z3AbstractProver.java b/src/org/sosy_lab/java_smt/solvers/z3/Z3AbstractProver.java index 933c4a77eb..49c3d9d97c 100644 --- a/src/org/sosy_lab/java_smt/solvers/z3/Z3AbstractProver.java +++ b/src/org/sosy_lab/java_smt/solvers/z3/Z3AbstractProver.java @@ -45,6 +45,7 @@ abstract class Z3AbstractProver extends AbstractProverWithAllSat { protected final long z3context; private final Z3FormulaManager mgr; + // m_n_obj in Z3 protected final long z3solver; private final UniqueIdGenerator trackId = new UniqueIdGenerator(); @@ -73,6 +74,34 @@ abstract class Z3AbstractProver extends AbstractProverWithAllSat { logfile = pLogfile; mgr = pMgr; + postProcessProverCreation(pSolverOptions); + } + + Z3AbstractProver( + Z3FormulaCreator pCreator, + Z3FormulaManager pMgr, + final long pZ3solver, + Set pOptions, + ImmutableMap pSolverOptions, + @Nullable PathCounterTemplate pLogfile, + ShutdownNotifier pShutdownNotifier) { + super(pOptions, pMgr.getBooleanFormulaManager(), pShutdownNotifier); + creator = pCreator; + z3context = creator.getEnv(); + z3solver = pZ3solver; + + interruptListener = reason -> Native.solverInterrupt(z3context, z3solver); + shutdownNotifier.register(interruptListener); + storedConstraints = + pOptions.contains(ProverOptions.GENERATE_UNSAT_CORE) ? new HashMap<>() : null; + + logfile = pLogfile; + mgr = pMgr; + + postProcessProverCreation(pSolverOptions); + } + + private void postProcessProverCreation(ImmutableMap pSolverOptions) { Native.solverIncRef(z3context, z3solver); long z3params = Native.mkParams(z3context); @@ -352,4 +381,8 @@ public R allSat(AllSatCallback callback, List important) protected void assertContraint(long negatedModel) { Native.solverAssert(z3context, z3solver, negatedModel); } + + protected final long getZ3Solver() { + return z3solver; + } } diff --git a/src/org/sosy_lab/java_smt/solvers/z3/Z3SolverContext.java b/src/org/sosy_lab/java_smt/solvers/z3/Z3SolverContext.java index d081dd5e8e..f4ddfd3c89 100644 --- a/src/org/sosy_lab/java_smt/solvers/z3/Z3SolverContext.java +++ b/src/org/sosy_lab/java_smt/solvers/z3/Z3SolverContext.java @@ -14,8 +14,13 @@ import com.microsoft.z3.Native; import com.microsoft.z3.enumerations.Z3_ast_print_mode; import java.io.IOException; +import java.lang.ref.PhantomReference; +import java.lang.ref.Reference; +import java.lang.ref.ReferenceQueue; import java.nio.charset.StandardCharsets; import java.nio.file.Path; +import java.util.IdentityHashMap; +import java.util.Map; import java.util.Set; import java.util.function.Consumer; import java.util.logging.Level; @@ -48,6 +53,9 @@ public final class Z3SolverContext extends AbstractSolverContext { private final Z3FormulaManager manager; private boolean closed = false; + private final ReferenceQueue referenceQueue = new ReferenceQueue<>(); + private final Map, Long> referenceMap = new IdentityHashMap<>(); + private static final String OPT_ENGINE_CONFIG_KEY = "optsmt_engine"; private static final String OPT_PRIORITY_CONFIG_KEY = "priority"; @@ -216,20 +224,59 @@ public static synchronized Z3SolverContext create( @Override protected ProverEnvironment newProverEnvironment0(Set options) { Preconditions.checkState(!closed, "solver context is already closed"); - final ImmutableMap solverOptions = - ImmutableMap.builder() - .put(":random-seed", extraOptions.randomSeed) - .put( - ":model", - options.contains(ProverOptions.GENERATE_MODELS) - || options.contains(ProverOptions.GENERATE_ALL_SAT)) - .put( - ":unsat_core", - options.contains(ProverOptions.GENERATE_UNSAT_CORE) - || options.contains(ProverOptions.GENERATE_UNSAT_CORE_OVER_ASSUMPTIONS)) - .buildOrThrow(); return new Z3TheoremProver( - creator, manager, options, solverOptions, extraOptions.logfile, shutdownNotifier); + creator, + manager, + options, + generateSolverOptions(options), + extraOptions.logfile, + shutdownNotifier); + } + + @Override + protected ProverEnvironment copyProverEnvironment0( + ProverEnvironment proverToCopy, Set options) { + Preconditions.checkState(!closed, "solver context is already closed"); + Preconditions.checkArgument( + proverToCopy instanceof Z3AbstractProver, + "You may only copy " + "ProverEnvironments of the same solver."); + + final Long z3solver = + Native.solverTranslate( + creator.getEnv(), ((Z3AbstractProver) proverToCopy).getZ3Solver(), creator.getEnv()); + + Native.solverIncRef(creator.getEnv(), z3solver); + + referenceMap.put(new PhantomReference<>(z3solver, referenceQueue), z3solver); + + Reference ref; + while ((ref = referenceQueue.poll()) != null) { + long z3ast = referenceMap.remove(ref); + Native.solverDecRef(creator.getEnv(), z3ast); + } + + return new Z3TheoremProver( + creator, + manager, + z3solver, + options, + generateSolverOptions(options), + extraOptions.logfile, + shutdownNotifier); + } + + private final ImmutableMap generateSolverOptions(Set options) { + return ImmutableMap.builder() + .put(":random-seed", extraOptions.randomSeed) + .put( + ":model", + options.contains(ProverOptions.GENERATE_MODELS) + || options.contains(ProverOptions.GENERATE_ALL_SAT)) + .put( + ":unsat_core", + options.contains(ProverOptions.GENERATE_UNSAT_CORE) + || options.contains(ProverOptions.GENERATE_UNSAT_CORE_OVER_ASSUMPTIONS)) + .buildOrThrow(); } @Override @@ -238,6 +285,12 @@ protected InterpolatingProverEnvironment newProverEnvironmentWithInterpolatio throw new UnsupportedOperationException("Z3 does not support interpolation"); } + @Override + protected InterpolatingProverEnvironment copyProverEnvironmentWithInterpolation0( + ProverEnvironment proverToCopy, Set pSet) { + throw new UnsupportedOperationException("Z3 does not support interpolation"); + } + @Override public OptimizationProverEnvironment newOptimizationProverEnvironment0( Set options) { diff --git a/src/org/sosy_lab/java_smt/solvers/z3/Z3TheoremProver.java b/src/org/sosy_lab/java_smt/solvers/z3/Z3TheoremProver.java index 6b58152426..b1722a152f 100644 --- a/src/org/sosy_lab/java_smt/solvers/z3/Z3TheoremProver.java +++ b/src/org/sosy_lab/java_smt/solvers/z3/Z3TheoremProver.java @@ -29,6 +29,17 @@ class Z3TheoremProver extends Z3AbstractProver implements ProverEnvironmen super(creator, pMgr, pOptions, pSolverOptions, pLogfile, pShutdownNotifier); } + Z3TheoremProver( + Z3FormulaCreator creator, + Z3FormulaManager pMgr, + final long pZ3solver, + Set pOptions, + ImmutableMap pSolverOptions, + @Nullable PathCounterTemplate pLogfile, + ShutdownNotifier pShutdownNotifier) { + super(creator, pMgr, pOptions, pSolverOptions, pLogfile, pShutdownNotifier); + } + @Override @Nullable public Void addConstraint(BooleanFormula f) throws InterruptedException { From d36cb96ccea5e957266870bccbeab8490bdebb0d Mon Sep 17 00:00:00 2001 From: BaierD Date: Mon, 31 Jul 2023 13:46:05 +0200 Subject: [PATCH 02/13] Add tests for prover copying and utility methods to avoid testing solvers that do not support this feature --- .../java_smt/test/SolverBasedTest0.java | 14 ++++++ .../java_smt/test/SolverContextTest.java | 50 +++++++++++++++++++ 2 files changed, 64 insertions(+) diff --git a/src/org/sosy_lab/java_smt/test/SolverBasedTest0.java b/src/org/sosy_lab/java_smt/test/SolverBasedTest0.java index 349bb30f93..f1c6673114 100644 --- a/src/org/sosy_lab/java_smt/test/SolverBasedTest0.java +++ b/src/org/sosy_lab/java_smt/test/SolverBasedTest0.java @@ -319,6 +319,20 @@ protected void requireSubstitution() { .isNotEqualTo(Solvers.BOOLECTOR); } + protected void requireProverCopying() { + assume() + .withMessage("Solver %s does not support copying of ProverEnvironments", solverToUse()) + .that(solverToUse()) + .isNoneOf( + Solvers.CVC4, + Solvers.CVC5, + Solvers.YICES2, + Solvers.BOOLECTOR, + Solvers.MATHSAT5, + Solvers.PRINCESS, + Solvers.SMTINTERPOL); + } + /** * Use this for checking assertions about BooleanFormulas with Truth: * assertThatFormula(formula).is...(). diff --git a/src/org/sosy_lab/java_smt/test/SolverContextTest.java b/src/org/sosy_lab/java_smt/test/SolverContextTest.java index 27f9ba0f61..39185a9306 100644 --- a/src/org/sosy_lab/java_smt/test/SolverContextTest.java +++ b/src/org/sosy_lab/java_smt/test/SolverContextTest.java @@ -14,6 +14,9 @@ import org.junit.Test; import org.sosy_lab.java_smt.SolverContextFactory.Solvers; import org.sosy_lab.java_smt.api.BooleanFormula; +import org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula; +import org.sosy_lab.java_smt.api.ProverEnvironment; +import org.sosy_lab.java_smt.api.SolverException; public class SolverContextTest extends SolverBasedTest0.ParameterizedSolverBasedTest0 { @@ -119,4 +122,51 @@ public void testFormulaAccessAfterClose() { assertThat(bmgr.isTrue(opTerm)).isFalse(); assertThat(bmgr.isFalse(opTerm)).isFalse(); } + + @Test + public void testProverCopying() throws SolverException, InterruptedException { + requireProverCopying(); + ProverEnvironment prover = context.newProverEnvironment(); + assertThat(prover.isUnsat()).isFalse(); + ProverEnvironment copiedProver = context.copyProverEnvironment(prover); + assertThat(copiedProver.isUnsat()).isFalse(); + } + + @Test + public void testProverCopyCloseInitialProver() throws SolverException, InterruptedException { + requireProverCopying(); + ProverEnvironment prover = context.newProverEnvironment(); + ProverEnvironment copiedProver = context.copyProverEnvironment(prover); + prover.close(); + assertThat(copiedProver.isUnsat()).isFalse(); + } + + /* + * Create a prover, push a SAT and an UNSAT formula on 2 levels, copy the prover, check that + * the stack is copied correctly. + */ + public void testProverCopyWithStackAndAssertions() throws InterruptedException, SolverException { + requireProverCopying(); + IntegerFormula x = imgr.makeVariable("x"); + IntegerFormula one = imgr.makeNumber("1"); + ProverEnvironment prover = context.newProverEnvironment(); + BooleanFormula sat = bmgr.and(imgr.equal(x, one), imgr.greaterOrEquals(x, one)); + BooleanFormula f = bmgr.makeFalse(); + prover.push(); + prover.addConstraint(sat); + assertThat(prover.isUnsat()).isFalse(); + prover.push(); + prover.addConstraint(f); + assertThat(prover.isUnsat()).isTrue(); + + ProverEnvironment copiedProver = context.copyProverEnvironment(prover); + assertThat(copiedProver.isUnsat()).isTrue(); + copiedProver.pop(); + assertThat(copiedProver.isUnsat()).isFalse(); + copiedProver.pop(); + assertThat(copiedProver.isUnsat()).isFalse(); + + // Test that the initial prover is unaffected + assertThat(prover.isUnsat()).isTrue(); + } } From 8f86ab153f4d4634aac73096ed3cc75dcc5523bb Mon Sep 17 00:00:00 2001 From: BaierD Date: Mon, 31 Jul 2023 14:04:39 +0200 Subject: [PATCH 03/13] Suppress ressource warnings for the new copy prover API --- src/org/sosy_lab/java_smt/basicimpl/AbstractSolverContext.java | 1 + .../java_smt/delegate/logging/LoggingSolverContext.java | 2 ++ .../java_smt/delegate/statistics/StatisticsSolverContext.java | 2 ++ .../delegate/synchronize/SynchronizedSolverContext.java | 2 ++ 4 files changed, 7 insertions(+) diff --git a/src/org/sosy_lab/java_smt/basicimpl/AbstractSolverContext.java b/src/org/sosy_lab/java_smt/basicimpl/AbstractSolverContext.java index 8ec09feb25..b80d41942a 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/AbstractSolverContext.java +++ b/src/org/sosy_lab/java_smt/basicimpl/AbstractSolverContext.java @@ -77,6 +77,7 @@ public final InterpolatingProverEnvironment newProverEnvironmentWithInterpola return out; } + @SuppressWarnings("resource") @Override public final InterpolatingProverEnvironment copyProverEnvironmentWithInterpolation( ProverEnvironment proverToCopy, ProverOptions... options) { diff --git a/src/org/sosy_lab/java_smt/delegate/logging/LoggingSolverContext.java b/src/org/sosy_lab/java_smt/delegate/logging/LoggingSolverContext.java index f35cc2f46a..3f60d0ec19 100644 --- a/src/org/sosy_lab/java_smt/delegate/logging/LoggingSolverContext.java +++ b/src/org/sosy_lab/java_smt/delegate/logging/LoggingSolverContext.java @@ -41,6 +41,7 @@ public ProverEnvironment newProverEnvironment(ProverOptions... pOptions) { return new LoggingProverEnvironment(logger, delegate.newProverEnvironment(pOptions)); } + @SuppressWarnings("resource") @Override public ProverEnvironment copyProverEnvironment( ProverEnvironment proverToCopy, ProverOptions... options) { @@ -57,6 +58,7 @@ public InterpolatingProverEnvironment newProverEnvironmentWithInterpolation( logger, delegate.newProverEnvironmentWithInterpolation(options)); } + @SuppressWarnings("resource") @Override public InterpolatingProverEnvironment copyProverEnvironmentWithInterpolation( ProverEnvironment proverToCopy, ProverOptions... options) { diff --git a/src/org/sosy_lab/java_smt/delegate/statistics/StatisticsSolverContext.java b/src/org/sosy_lab/java_smt/delegate/statistics/StatisticsSolverContext.java index b1bc76460b..92f0898bf0 100644 --- a/src/org/sosy_lab/java_smt/delegate/statistics/StatisticsSolverContext.java +++ b/src/org/sosy_lab/java_smt/delegate/statistics/StatisticsSolverContext.java @@ -39,6 +39,7 @@ public ProverEnvironment newProverEnvironment(ProverOptions... pOptions) { return new StatisticsProverEnvironment(delegate.newProverEnvironment(pOptions), stats); } + @SuppressWarnings("resource") @Override public ProverEnvironment copyProverEnvironment( ProverEnvironment proverToCopy, ProverOptions... options) { @@ -54,6 +55,7 @@ public InterpolatingProverEnvironment newProverEnvironmentWithInterpolation( delegate.newProverEnvironmentWithInterpolation(pOptions), stats); } + @SuppressWarnings("resource") @Override public InterpolatingProverEnvironment copyProverEnvironmentWithInterpolation( ProverEnvironment proverToCopy, ProverOptions... options) { diff --git a/src/org/sosy_lab/java_smt/delegate/synchronize/SynchronizedSolverContext.java b/src/org/sosy_lab/java_smt/delegate/synchronize/SynchronizedSolverContext.java index 9cfb3f4ca3..61a8734a52 100644 --- a/src/org/sosy_lab/java_smt/delegate/synchronize/SynchronizedSolverContext.java +++ b/src/org/sosy_lab/java_smt/delegate/synchronize/SynchronizedSolverContext.java @@ -94,6 +94,7 @@ public ProverEnvironment newProverEnvironment(ProverOptions... pOptions) { } } + @SuppressWarnings("resource") @Override public ProverEnvironment copyProverEnvironment( ProverEnvironment proverToCopy, ProverOptions... options) { @@ -131,6 +132,7 @@ public InterpolatingProverEnvironment newProverEnvironmentWithInterpolation( } } + @SuppressWarnings("resource") @Override public InterpolatingProverEnvironment copyProverEnvironmentWithInterpolation( ProverEnvironment proverToCopy, ProverOptions... options) { From 0dfb3e77f96051ed6db22a0b0a0191e66e821ac3 Mon Sep 17 00:00:00 2001 From: BaierD Date: Mon, 31 Jul 2023 14:04:52 +0200 Subject: [PATCH 04/13] Improve tests for new copy prover API --- .../java_smt/test/SolverContextTest.java | 60 ++++++++++--------- 1 file changed, 33 insertions(+), 27 deletions(-) diff --git a/src/org/sosy_lab/java_smt/test/SolverContextTest.java b/src/org/sosy_lab/java_smt/test/SolverContextTest.java index 39185a9306..aea0e73517 100644 --- a/src/org/sosy_lab/java_smt/test/SolverContextTest.java +++ b/src/org/sosy_lab/java_smt/test/SolverContextTest.java @@ -126,19 +126,23 @@ public void testFormulaAccessAfterClose() { @Test public void testProverCopying() throws SolverException, InterruptedException { requireProverCopying(); - ProverEnvironment prover = context.newProverEnvironment(); - assertThat(prover.isUnsat()).isFalse(); - ProverEnvironment copiedProver = context.copyProverEnvironment(prover); - assertThat(copiedProver.isUnsat()).isFalse(); + try (ProverEnvironment prover = context.newProverEnvironment()) { + assertThat(prover.isUnsat()).isFalse(); + try (ProverEnvironment copiedProver = context.copyProverEnvironment(prover)) { + assertThat(copiedProver.isUnsat()).isFalse(); + } + } } @Test public void testProverCopyCloseInitialProver() throws SolverException, InterruptedException { requireProverCopying(); - ProverEnvironment prover = context.newProverEnvironment(); - ProverEnvironment copiedProver = context.copyProverEnvironment(prover); - prover.close(); - assertThat(copiedProver.isUnsat()).isFalse(); + try (ProverEnvironment prover = context.newProverEnvironment()) { + try (ProverEnvironment copiedProver = context.copyProverEnvironment(prover)) { + prover.close(); + assertThat(copiedProver.isUnsat()).isFalse(); + } + } } /* @@ -149,24 +153,26 @@ public void testProverCopyWithStackAndAssertions() throws InterruptedException, requireProverCopying(); IntegerFormula x = imgr.makeVariable("x"); IntegerFormula one = imgr.makeNumber("1"); - ProverEnvironment prover = context.newProverEnvironment(); - BooleanFormula sat = bmgr.and(imgr.equal(x, one), imgr.greaterOrEquals(x, one)); - BooleanFormula f = bmgr.makeFalse(); - prover.push(); - prover.addConstraint(sat); - assertThat(prover.isUnsat()).isFalse(); - prover.push(); - prover.addConstraint(f); - assertThat(prover.isUnsat()).isTrue(); - - ProverEnvironment copiedProver = context.copyProverEnvironment(prover); - assertThat(copiedProver.isUnsat()).isTrue(); - copiedProver.pop(); - assertThat(copiedProver.isUnsat()).isFalse(); - copiedProver.pop(); - assertThat(copiedProver.isUnsat()).isFalse(); - - // Test that the initial prover is unaffected - assertThat(prover.isUnsat()).isTrue(); + try (ProverEnvironment prover = context.newProverEnvironment()) { + BooleanFormula sat = bmgr.and(imgr.equal(x, one), imgr.greaterOrEquals(x, one)); + BooleanFormula f = bmgr.makeFalse(); + prover.push(); + prover.addConstraint(sat); + assertThat(prover.isUnsat()).isFalse(); + prover.push(); + prover.addConstraint(f); + assertThat(prover.isUnsat()).isTrue(); + + try (ProverEnvironment copiedProver = context.copyProverEnvironment(prover)) { + assertThat(copiedProver.isUnsat()).isTrue(); + copiedProver.pop(); + assertThat(copiedProver.isUnsat()).isFalse(); + copiedProver.pop(); + assertThat(copiedProver.isUnsat()).isFalse(); + + // Test that the initial prover is unaffected + assertThat(prover.isUnsat()).isTrue(); + } + } } } From 0fd372f2afd04d547693f0321a4f4635def02fa2 Mon Sep 17 00:00:00 2001 From: BaierD Date: Mon, 31 Jul 2023 14:05:30 +0200 Subject: [PATCH 05/13] Add missing @Test annotation to prover copy test --- src/org/sosy_lab/java_smt/test/SolverContextTest.java | 1 + 1 file changed, 1 insertion(+) diff --git a/src/org/sosy_lab/java_smt/test/SolverContextTest.java b/src/org/sosy_lab/java_smt/test/SolverContextTest.java index aea0e73517..89f4fdbfec 100644 --- a/src/org/sosy_lab/java_smt/test/SolverContextTest.java +++ b/src/org/sosy_lab/java_smt/test/SolverContextTest.java @@ -149,6 +149,7 @@ public void testProverCopyCloseInitialProver() throws SolverException, Interrupt * Create a prover, push a SAT and an UNSAT formula on 2 levels, copy the prover, check that * the stack is copied correctly. */ + @Test public void testProverCopyWithStackAndAssertions() throws InterruptedException, SolverException { requireProverCopying(); IntegerFormula x = imgr.makeVariable("x"); From 4881e3c6d55fd8a31066a5ee904887bfd6b40e37 Mon Sep 17 00:00:00 2001 From: BaierD Date: Mon, 31 Jul 2023 14:08:36 +0200 Subject: [PATCH 06/13] Remove redundant final modifier from Z3 context --- src/org/sosy_lab/java_smt/solvers/z3/Z3SolverContext.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/org/sosy_lab/java_smt/solvers/z3/Z3SolverContext.java b/src/org/sosy_lab/java_smt/solvers/z3/Z3SolverContext.java index f4ddfd3c89..504d34acc4 100644 --- a/src/org/sosy_lab/java_smt/solvers/z3/Z3SolverContext.java +++ b/src/org/sosy_lab/java_smt/solvers/z3/Z3SolverContext.java @@ -265,7 +265,7 @@ protected ProverEnvironment copyProverEnvironment0( shutdownNotifier); } - private final ImmutableMap generateSolverOptions(Set options) { + private ImmutableMap generateSolverOptions(Set options) { return ImmutableMap.builder() .put(":random-seed", extraOptions.randomSeed) .put( From 9193dd6778a4ccce06d1b0b53795c9948febe320 Mon Sep 17 00:00:00 2001 From: BaierD Date: Mon, 31 Jul 2023 14:13:04 +0200 Subject: [PATCH 07/13] Don't use a try catch block for a test that requires a manual close() --- src/org/sosy_lab/java_smt/test/SolverContextTest.java | 9 ++++----- 1 file changed, 4 insertions(+), 5 deletions(-) diff --git a/src/org/sosy_lab/java_smt/test/SolverContextTest.java b/src/org/sosy_lab/java_smt/test/SolverContextTest.java index 89f4fdbfec..fa4e92249f 100644 --- a/src/org/sosy_lab/java_smt/test/SolverContextTest.java +++ b/src/org/sosy_lab/java_smt/test/SolverContextTest.java @@ -137,11 +137,10 @@ public void testProverCopying() throws SolverException, InterruptedException { @Test public void testProverCopyCloseInitialProver() throws SolverException, InterruptedException { requireProverCopying(); - try (ProverEnvironment prover = context.newProverEnvironment()) { - try (ProverEnvironment copiedProver = context.copyProverEnvironment(prover)) { - prover.close(); - assertThat(copiedProver.isUnsat()).isFalse(); - } + ProverEnvironment prover = context.newProverEnvironment(); + try (ProverEnvironment copiedProver = context.copyProverEnvironment(prover)) { + prover.close(); + assertThat(copiedProver.isUnsat()).isFalse(); } } From 198e7b2884386e57c6038eaa1bb342325cb565b1 Mon Sep 17 00:00:00 2001 From: BaierD Date: Mon, 31 Jul 2023 14:17:17 +0200 Subject: [PATCH 08/13] Fix wrong constructor usage for Z3 copied theorem prover --- src/org/sosy_lab/java_smt/solvers/z3/Z3TheoremProver.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/org/sosy_lab/java_smt/solvers/z3/Z3TheoremProver.java b/src/org/sosy_lab/java_smt/solvers/z3/Z3TheoremProver.java index b1722a152f..ccd1b91eec 100644 --- a/src/org/sosy_lab/java_smt/solvers/z3/Z3TheoremProver.java +++ b/src/org/sosy_lab/java_smt/solvers/z3/Z3TheoremProver.java @@ -37,7 +37,7 @@ class Z3TheoremProver extends Z3AbstractProver implements ProverEnvironmen ImmutableMap pSolverOptions, @Nullable PathCounterTemplate pLogfile, ShutdownNotifier pShutdownNotifier) { - super(creator, pMgr, pOptions, pSolverOptions, pLogfile, pShutdownNotifier); + super(creator, pMgr, pZ3solver, pOptions, pSolverOptions, pLogfile, pShutdownNotifier); } @Override From 98303fb426813a2d58920dc496e6f0fd756dde91 Mon Sep 17 00:00:00 2001 From: BaierD Date: Mon, 31 Jul 2023 14:38:00 +0200 Subject: [PATCH 09/13] Fix type used for a Map in Z3 solver context to use the explicit type --- src/org/sosy_lab/java_smt/solvers/z3/Z3SolverContext.java | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/src/org/sosy_lab/java_smt/solvers/z3/Z3SolverContext.java b/src/org/sosy_lab/java_smt/solvers/z3/Z3SolverContext.java index 504d34acc4..2d13f45190 100644 --- a/src/org/sosy_lab/java_smt/solvers/z3/Z3SolverContext.java +++ b/src/org/sosy_lab/java_smt/solvers/z3/Z3SolverContext.java @@ -20,7 +20,6 @@ import java.nio.charset.StandardCharsets; import java.nio.file.Path; import java.util.IdentityHashMap; -import java.util.Map; import java.util.Set; import java.util.function.Consumer; import java.util.logging.Level; @@ -54,7 +53,7 @@ public final class Z3SolverContext extends AbstractSolverContext { private boolean closed = false; private final ReferenceQueue referenceQueue = new ReferenceQueue<>(); - private final Map, Long> referenceMap = new IdentityHashMap<>(); + private final IdentityHashMap, Long> referenceMap = new IdentityHashMap<>(); private static final String OPT_ENGINE_CONFIG_KEY = "optsmt_engine"; private static final String OPT_PRIORITY_CONFIG_KEY = "priority"; From e217830291dc0137544403b38415e1756e766a81 Mon Sep 17 00:00:00 2001 From: BaierD Date: Mon, 31 Jul 2023 14:38:22 +0200 Subject: [PATCH 10/13] Suppress warning for ressource (try-catch block) as we need it for a text --- src/org/sosy_lab/java_smt/test/SolverContextTest.java | 1 + 1 file changed, 1 insertion(+) diff --git a/src/org/sosy_lab/java_smt/test/SolverContextTest.java b/src/org/sosy_lab/java_smt/test/SolverContextTest.java index fa4e92249f..0643d385e1 100644 --- a/src/org/sosy_lab/java_smt/test/SolverContextTest.java +++ b/src/org/sosy_lab/java_smt/test/SolverContextTest.java @@ -134,6 +134,7 @@ public void testProverCopying() throws SolverException, InterruptedException { } } + @SuppressWarnings("resource") @Test public void testProverCopyCloseInitialProver() throws SolverException, InterruptedException { requireProverCopying(); From f63ec0e3071300d995bde975867f1db35aa30f28 Mon Sep 17 00:00:00 2001 From: BaierD Date: Mon, 31 Jul 2023 14:42:52 +0200 Subject: [PATCH 11/13] Disable a test for prover copying after push for Z3 as it can't handle this case --- src/org/sosy_lab/java_smt/test/SolverContextTest.java | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/src/org/sosy_lab/java_smt/test/SolverContextTest.java b/src/org/sosy_lab/java_smt/test/SolverContextTest.java index 0643d385e1..4bd13d4486 100644 --- a/src/org/sosy_lab/java_smt/test/SolverContextTest.java +++ b/src/org/sosy_lab/java_smt/test/SolverContextTest.java @@ -152,6 +152,14 @@ public void testProverCopyCloseInitialProver() throws SolverException, Interrupt @Test public void testProverCopyWithStackAndAssertions() throws InterruptedException, SolverException { requireProverCopying(); + + assume() + .withMessage( + "Solver %s does not support prover copying for non-base-level provers", + solverToUse()) + .that(solverToUse()) + .isNotEqualTo(Solvers.Z3); + IntegerFormula x = imgr.makeVariable("x"); IntegerFormula one = imgr.makeNumber("1"); try (ProverEnvironment prover = context.newProverEnvironment()) { From d614169b8d57f9364878b4bb33370d14c2c6e382 Mon Sep 17 00:00:00 2001 From: BaierD Date: Tue, 1 Aug 2023 15:04:46 +0200 Subject: [PATCH 12/13] Improve Z3AbstractProver constructor and cleanup --- .../java_smt/solvers/z3/Z3AbstractProver.java | 16 ++-------------- .../java_smt/solvers/z3/Z3SolverContext.java | 3 ++- .../java_smt/test/SolverContextTest.java | 3 +-- 3 files changed, 5 insertions(+), 17 deletions(-) diff --git a/src/org/sosy_lab/java_smt/solvers/z3/Z3AbstractProver.java b/src/org/sosy_lab/java_smt/solvers/z3/Z3AbstractProver.java index 49c3d9d97c..b990e239f4 100644 --- a/src/org/sosy_lab/java_smt/solvers/z3/Z3AbstractProver.java +++ b/src/org/sosy_lab/java_smt/solvers/z3/Z3AbstractProver.java @@ -62,19 +62,8 @@ abstract class Z3AbstractProver extends AbstractProverWithAllSat { ImmutableMap pSolverOptions, @Nullable PathCounterTemplate pLogfile, ShutdownNotifier pShutdownNotifier) { - super(pOptions, pMgr.getBooleanFormulaManager(), pShutdownNotifier); - creator = pCreator; - z3context = creator.getEnv(); - z3solver = Native.mkSolver(z3context); - - interruptListener = reason -> Native.solverInterrupt(z3context, z3solver); - shutdownNotifier.register(interruptListener); - storedConstraints = - pOptions.contains(ProverOptions.GENERATE_UNSAT_CORE) ? new HashMap<>() : null; - - logfile = pLogfile; - mgr = pMgr; - postProcessProverCreation(pSolverOptions); + this(pCreator, pMgr, Native.mkSolver(pCreator.getEnv()), pOptions, pSolverOptions, pLogfile, + pShutdownNotifier); } Z3AbstractProver( @@ -97,7 +86,6 @@ abstract class Z3AbstractProver extends AbstractProverWithAllSat { logfile = pLogfile; mgr = pMgr; - postProcessProverCreation(pSolverOptions); } diff --git a/src/org/sosy_lab/java_smt/solvers/z3/Z3SolverContext.java b/src/org/sosy_lab/java_smt/solvers/z3/Z3SolverContext.java index 2d13f45190..ee09e0731a 100644 --- a/src/org/sosy_lab/java_smt/solvers/z3/Z3SolverContext.java +++ b/src/org/sosy_lab/java_smt/solvers/z3/Z3SolverContext.java @@ -53,7 +53,8 @@ public final class Z3SolverContext extends AbstractSolverContext { private boolean closed = false; private final ReferenceQueue referenceQueue = new ReferenceQueue<>(); - private final IdentityHashMap, Long> referenceMap = new IdentityHashMap<>(); + private final IdentityHashMap, Long> referenceMap = + new IdentityHashMap<>(); private static final String OPT_ENGINE_CONFIG_KEY = "optsmt_engine"; private static final String OPT_PRIORITY_CONFIG_KEY = "priority"; diff --git a/src/org/sosy_lab/java_smt/test/SolverContextTest.java b/src/org/sosy_lab/java_smt/test/SolverContextTest.java index 4bd13d4486..f0e83081a4 100644 --- a/src/org/sosy_lab/java_smt/test/SolverContextTest.java +++ b/src/org/sosy_lab/java_smt/test/SolverContextTest.java @@ -155,8 +155,7 @@ public void testProverCopyWithStackAndAssertions() throws InterruptedException, assume() .withMessage( - "Solver %s does not support prover copying for non-base-level provers", - solverToUse()) + "Solver %s does not support prover copying for non-base-level provers", solverToUse()) .that(solverToUse()) .isNotEqualTo(Solvers.Z3); From 28cc2fbc3123256106cbb89743d47ca44257b346 Mon Sep 17 00:00:00 2001 From: BaierD Date: Tue, 1 Aug 2023 18:21:01 +0200 Subject: [PATCH 13/13] Add copy for OptimizationProver and remove options argument from copy prover methods --- .../sosy_lab/java_smt/api/SolverContext.java | 34 ++++++++++++------- .../basicimpl/AbstractSolverContext.java | 15 ++++---- .../logging/LoggingSolverContext.java | 18 ++++++---- .../statistics/StatisticsSolverContext.java | 18 ++++++---- .../SynchronizedSolverContext.java | 21 ++++++++---- .../boolector/BoolectorSolverContext.java | 15 +++++--- .../solvers/cvc4/CVC4SolverContext.java | 11 ++++-- .../solvers/cvc5/CVC5SolverContext.java | 15 +++++--- .../mathsat5/Mathsat5SolverContext.java | 16 ++++++--- .../princess/PrincessSolverContext.java | 15 +++++--- .../smtinterpol/SmtInterpolSolverContext.java | 15 +++++--- .../solvers/yices2/Yices2SolverContext.java | 11 ++++-- .../java_smt/solvers/z3/Z3AbstractProver.java | 15 +++++++- .../java_smt/solvers/z3/Z3SolverContext.java | 15 ++++++-- 14 files changed, 158 insertions(+), 76 deletions(-) diff --git a/src/org/sosy_lab/java_smt/api/SolverContext.java b/src/org/sosy_lab/java_smt/api/SolverContext.java index 3bbd32384b..d3f6a6918a 100644 --- a/src/org/sosy_lab/java_smt/api/SolverContext.java +++ b/src/org/sosy_lab/java_smt/api/SolverContext.java @@ -68,14 +68,12 @@ enum ProverOptions { /** * 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}. + * {@link ProverEnvironment}. Options are carried over from proverToCopy. * * @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); + ProverEnvironment copyProverEnvironment(ProverEnvironment proverToCopy); /** * Create a fresh new {@link InterpolatingProverEnvironment} which encapsulates an assertion stack @@ -91,18 +89,16 @@ enum ProverOptions { /** * 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. + * InterpolatingProverEnvironment} retains the current assertion stack of the given {@link + * InterpolatingProverEnvironment}. 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. Options are carried over from proverToCopy. * - * @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. + * @param proverToCopy An existing {@link InterpolatingProverEnvironment}, whichs assertion stack + * is to be copied into the new one. */ InterpolatingProverEnvironment copyProverEnvironmentWithInterpolation( - ProverEnvironment proverToCopy, ProverOptions... options); + InterpolatingProverEnvironment proverToCopy); /** * Create a fresh new {@link OptimizationProverEnvironment} which encapsulates an assertion stack @@ -113,6 +109,18 @@ InterpolatingProverEnvironment copyProverEnvironmentWithInterpolation( */ OptimizationProverEnvironment newOptimizationProverEnvironment(ProverOptions... options); + /** + * Create a fresh new {@link OptimizationProverEnvironment} which encapsulates an assertion stack + * and allows solving optimization queries. The new {@link OptimizationProverEnvironment} retains + * the current assertion stack of the given {@link OptimizationProverEnvironment}. Options are + * carried over from proverToCopy. + * + * @param proverToCopy An existing {@link ProverEnvironment}, whichs assertion stack is to be + * copied into the new one. + */ + OptimizationProverEnvironment copyOptimizationProverEnvironment( + OptimizationProverEnvironment proverToCopy); + /** * Get version information out of the solver. * diff --git a/src/org/sosy_lab/java_smt/basicimpl/AbstractSolverContext.java b/src/org/sosy_lab/java_smt/basicimpl/AbstractSolverContext.java index b80d41942a..ba046dc705 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/AbstractSolverContext.java +++ b/src/org/sosy_lab/java_smt/basicimpl/AbstractSolverContext.java @@ -47,9 +47,8 @@ public final ProverEnvironment newProverEnvironment(ProverOptions... options) { } @Override - public final ProverEnvironment copyProverEnvironment( - ProverEnvironment proverToCopy, ProverOptions... options) { - ProverEnvironment out = copyProverEnvironment0(proverToCopy, toSet(options)); + public final ProverEnvironment copyProverEnvironment(ProverEnvironment proverToCopy) { + ProverEnvironment out = copyProverEnvironment0(proverToCopy); if (!supportsAssumptionSolving()) { // In the case we do not already have a prover environment with assumptions, // we add a wrapper to it @@ -60,8 +59,7 @@ public final ProverEnvironment copyProverEnvironment( protected abstract ProverEnvironment newProverEnvironment0(Set options); - protected abstract ProverEnvironment copyProverEnvironment0( - ProverEnvironment proverToCopy, Set options); + protected abstract ProverEnvironment copyProverEnvironment0(ProverEnvironment proverToCopy); @SuppressWarnings("resource") @Override @@ -80,10 +78,9 @@ public final InterpolatingProverEnvironment newProverEnvironmentWithInterpola @SuppressWarnings("resource") @Override public final InterpolatingProverEnvironment copyProverEnvironmentWithInterpolation( - ProverEnvironment proverToCopy, ProverOptions... options) { + InterpolatingProverEnvironment proverToCopy) { - InterpolatingProverEnvironment out = - copyProverEnvironmentWithInterpolation0(proverToCopy, toSet(options)); + InterpolatingProverEnvironment out = copyProverEnvironmentWithInterpolation0(proverToCopy); if (!supportsAssumptionSolving()) { // In the case we do not already have a prover environment with assumptions, // we add a wrapper to it @@ -96,7 +93,7 @@ protected abstract InterpolatingProverEnvironment newProverEnvironmentWithInt Set pSet); protected abstract InterpolatingProverEnvironment copyProverEnvironmentWithInterpolation0( - ProverEnvironment proverToCopy, Set pSet); + InterpolatingProverEnvironment proverToCopy); @SuppressWarnings("resource") @Override diff --git a/src/org/sosy_lab/java_smt/delegate/logging/LoggingSolverContext.java b/src/org/sosy_lab/java_smt/delegate/logging/LoggingSolverContext.java index 3f60d0ec19..ea6b8585cc 100644 --- a/src/org/sosy_lab/java_smt/delegate/logging/LoggingSolverContext.java +++ b/src/org/sosy_lab/java_smt/delegate/logging/LoggingSolverContext.java @@ -43,11 +43,9 @@ public ProverEnvironment newProverEnvironment(ProverOptions... pOptions) { @SuppressWarnings("resource") @Override - public ProverEnvironment copyProverEnvironment( - ProverEnvironment proverToCopy, ProverOptions... options) { + public ProverEnvironment copyProverEnvironment(ProverEnvironment proverToCopy) { // TODO: log this? Because this is not a normal new prover? - return new LoggingProverEnvironment( - logger, delegate.copyProverEnvironment(proverToCopy, options)); + return new LoggingProverEnvironment(logger, delegate.copyProverEnvironment(proverToCopy)); } @SuppressWarnings("resource") @@ -61,10 +59,10 @@ public InterpolatingProverEnvironment newProverEnvironmentWithInterpolation( @SuppressWarnings("resource") @Override public InterpolatingProverEnvironment copyProverEnvironmentWithInterpolation( - ProverEnvironment proverToCopy, ProverOptions... options) { + InterpolatingProverEnvironment proverToCopy) { // TODO: log this? Because this is not a normal new prover? return new LoggingInterpolatingProverEnvironment<>( - logger, delegate.copyProverEnvironmentWithInterpolation(proverToCopy, options)); + logger, delegate.copyProverEnvironmentWithInterpolation(proverToCopy)); } @SuppressWarnings("resource") @@ -74,6 +72,14 @@ public OptimizationProverEnvironment newOptimizationProverEnvironment(ProverOpti logger, delegate.newOptimizationProverEnvironment(options)); } + @SuppressWarnings("resource") + @Override + public OptimizationProverEnvironment copyOptimizationProverEnvironment( + OptimizationProverEnvironment proverToCopy) { + return new LoggingOptimizationProverEnvironment( + logger, delegate.copyOptimizationProverEnvironment(proverToCopy)); + } + @Override public String getVersion() { return delegate.getVersion(); diff --git a/src/org/sosy_lab/java_smt/delegate/statistics/StatisticsSolverContext.java b/src/org/sosy_lab/java_smt/delegate/statistics/StatisticsSolverContext.java index 92f0898bf0..48a9ae409a 100644 --- a/src/org/sosy_lab/java_smt/delegate/statistics/StatisticsSolverContext.java +++ b/src/org/sosy_lab/java_smt/delegate/statistics/StatisticsSolverContext.java @@ -41,10 +41,8 @@ public ProverEnvironment newProverEnvironment(ProverOptions... pOptions) { @SuppressWarnings("resource") @Override - public ProverEnvironment copyProverEnvironment( - ProverEnvironment proverToCopy, ProverOptions... options) { - return new StatisticsProverEnvironment( - delegate.copyProverEnvironment(proverToCopy, options), stats); + public ProverEnvironment copyProverEnvironment(ProverEnvironment proverToCopy) { + return new StatisticsProverEnvironment(delegate.copyProverEnvironment(proverToCopy), stats); } @SuppressWarnings("resource") @@ -58,9 +56,9 @@ public InterpolatingProverEnvironment newProverEnvironmentWithInterpolation( @SuppressWarnings("resource") @Override public InterpolatingProverEnvironment copyProverEnvironmentWithInterpolation( - ProverEnvironment proverToCopy, ProverOptions... options) { + InterpolatingProverEnvironment proverToCopy) { return new StatisticsInterpolatingProverEnvironment<>( - delegate.copyProverEnvironmentWithInterpolation(proverToCopy, options), stats); + delegate.copyProverEnvironmentWithInterpolation(proverToCopy), stats); } @SuppressWarnings("resource") @@ -70,6 +68,14 @@ public OptimizationProverEnvironment newOptimizationProverEnvironment(ProverOpti delegate.newOptimizationProverEnvironment(pOptions), stats); } + @SuppressWarnings("resource") + @Override + public OptimizationProverEnvironment copyOptimizationProverEnvironment( + OptimizationProverEnvironment proverToCopy) { + return new StatisticsOptimizationProverEnvironment( + delegate.copyOptimizationProverEnvironment(proverToCopy), stats); + } + @Override public String getVersion() { return delegate.getVersion(); diff --git a/src/org/sosy_lab/java_smt/delegate/synchronize/SynchronizedSolverContext.java b/src/org/sosy_lab/java_smt/delegate/synchronize/SynchronizedSolverContext.java index 61a8734a52..03556a3d19 100644 --- a/src/org/sosy_lab/java_smt/delegate/synchronize/SynchronizedSolverContext.java +++ b/src/org/sosy_lab/java_smt/delegate/synchronize/SynchronizedSolverContext.java @@ -96,19 +96,18 @@ public ProverEnvironment newProverEnvironment(ProverOptions... pOptions) { @SuppressWarnings("resource") @Override - public ProverEnvironment copyProverEnvironment( - ProverEnvironment proverToCopy, ProverOptions... options) { + public ProverEnvironment copyProverEnvironment(ProverEnvironment proverToCopy) { synchronized (sync) { if (useSeperateProvers) { SolverContext otherContext = createOtherContext(); return new SynchronizedProverEnvironmentWithContext( - otherContext.copyProverEnvironment(proverToCopy, options), + otherContext.copyProverEnvironment(proverToCopy), sync, delegate.getFormulaManager(), otherContext.getFormulaManager()); } else { return new SynchronizedProverEnvironment( - delegate.copyProverEnvironment(proverToCopy, options), delegate); + delegate.copyProverEnvironment(proverToCopy), delegate); } } } @@ -135,18 +134,18 @@ public InterpolatingProverEnvironment newProverEnvironmentWithInterpolation( @SuppressWarnings("resource") @Override public InterpolatingProverEnvironment copyProverEnvironmentWithInterpolation( - ProverEnvironment proverToCopy, ProverOptions... options) { + InterpolatingProverEnvironment proverToCopy) { synchronized (sync) { if (useSeperateProvers) { SolverContext otherContext = createOtherContext(); return new SynchronizedInterpolatingProverEnvironmentWithContext<>( - otherContext.copyProverEnvironmentWithInterpolation(proverToCopy, options), + otherContext.copyProverEnvironmentWithInterpolation(proverToCopy), sync, delegate.getFormulaManager(), otherContext.getFormulaManager()); } else { return new SynchronizedInterpolatingProverEnvironment<>( - delegate.copyProverEnvironmentWithInterpolation(proverToCopy, options), delegate); + delegate.copyProverEnvironmentWithInterpolation(proverToCopy), delegate); } } } @@ -162,6 +161,14 @@ public OptimizationProverEnvironment newOptimizationProverEnvironment(ProverOpti } } + @SuppressWarnings("resource") + @Override + public OptimizationProverEnvironment copyOptimizationProverEnvironment( + OptimizationProverEnvironment proverToCopy) { + return new SynchronizedOptimizationProverEnvironment( + delegate.copyOptimizationProverEnvironment(proverToCopy), delegate); + } + @Override public String getVersion() { synchronized (sync) { diff --git a/src/org/sosy_lab/java_smt/solvers/boolector/BoolectorSolverContext.java b/src/org/sosy_lab/java_smt/solvers/boolector/BoolectorSolverContext.java index 9143fbfdc2..9d1d643efe 100644 --- a/src/org/sosy_lab/java_smt/solvers/boolector/BoolectorSolverContext.java +++ b/src/org/sosy_lab/java_smt/solvers/boolector/BoolectorSolverContext.java @@ -205,10 +205,9 @@ protected ProverEnvironment newProverEnvironment0(Set pOptions) { } @Override - protected ProverEnvironment copyProverEnvironment0( - ProverEnvironment proverToCopy, Set options) { + protected ProverEnvironment copyProverEnvironment0(ProverEnvironment proverToCopy) { throw new UnsupportedOperationException( - "Boolector does not support the copying of " + "ProverEnvironments"); + "Boolector does not support the copying of ProverEnvironments"); } @Override @@ -219,9 +218,9 @@ protected InterpolatingProverEnvironment newProverEnvironmentWithInterpolatio @Override protected InterpolatingProverEnvironment copyProverEnvironmentWithInterpolation0( - ProverEnvironment proverToCopy, Set pSet) { + InterpolatingProverEnvironment proverToCopy) { throw new UnsupportedOperationException( - "Boolector does not support the copying of " + "ProverEnvironments"); + "Boolector does not support the copying of ProverEnvironments"); } @Override @@ -230,6 +229,12 @@ protected OptimizationProverEnvironment newOptimizationProverEnvironment0( throw new UnsupportedOperationException("Boolector does not support optimization"); } + @Override + public OptimizationProverEnvironment copyOptimizationProverEnvironment( + OptimizationProverEnvironment proverToCopy) { + throw new UnsupportedOperationException("Boolector does not support optimization"); + } + @Override protected boolean supportsAssumptionSolving() { return true; diff --git a/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4SolverContext.java b/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4SolverContext.java index 2766aec830..ac11fb19f0 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4SolverContext.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4SolverContext.java @@ -138,8 +138,7 @@ public ProverEnvironment newProverEnvironment0(Set pOptions) { } @Override - protected ProverEnvironment copyProverEnvironment0( - ProverEnvironment proverToCopy, Set options) { + protected ProverEnvironment copyProverEnvironment0(ProverEnvironment proverToCopy) { throw new UnsupportedOperationException( "CVC4 does not support the copying of " + "ProverEnvironments"); } @@ -157,7 +156,7 @@ protected InterpolatingProverEnvironment newProverEnvironmentWithInterpolatio @Override protected InterpolatingProverEnvironment copyProverEnvironmentWithInterpolation0( - ProverEnvironment proverToCopy, Set pSet) { + InterpolatingProverEnvironment proverToCopy) { throw new UnsupportedOperationException( "CVC4 does not support the copying of " + "ProverEnvironments"); } @@ -167,4 +166,10 @@ protected OptimizationProverEnvironment newOptimizationProverEnvironment0( Set pSet) { throw new UnsupportedOperationException("CVC4 does not support optimization"); } + + @Override + public OptimizationProverEnvironment copyOptimizationProverEnvironment( + OptimizationProverEnvironment proverToCopy) { + throw new UnsupportedOperationException("CVC4 does not support optimization"); + } } diff --git a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5SolverContext.java b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5SolverContext.java index 66a97e7e2b..8701cdb55c 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5SolverContext.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5SolverContext.java @@ -158,10 +158,9 @@ public ProverEnvironment newProverEnvironment0(Set pOptions) { } @Override - protected ProverEnvironment copyProverEnvironment0( - ProverEnvironment proverToCopy, Set options) { + protected ProverEnvironment copyProverEnvironment0(ProverEnvironment proverToCopy) { throw new UnsupportedOperationException( - "CVC5 does not support the copying of " + "ProverEnvironments"); + "CVC5 does not support the copying of ProverEnvironments"); } @Override @@ -177,9 +176,9 @@ protected InterpolatingProverEnvironment newProverEnvironmentWithInterpolatio @Override protected InterpolatingProverEnvironment copyProverEnvironmentWithInterpolation0( - ProverEnvironment proverToCopy, Set pSet) { + InterpolatingProverEnvironment proverToCopy) { throw new UnsupportedOperationException( - "CVC5 does not support the copying of " + "ProverEnvironments"); + "CVC5 does not support the copying of ProverEnvironments"); } @Override @@ -187,4 +186,10 @@ protected OptimizationProverEnvironment newOptimizationProverEnvironment0( Set pSet) { throw new UnsupportedOperationException("CVC5 does not support optimization"); } + + @Override + public OptimizationProverEnvironment copyOptimizationProverEnvironment( + OptimizationProverEnvironment proverToCopy) { + throw new UnsupportedOperationException("CVC5 does not support optimization"); + } } diff --git a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5SolverContext.java b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5SolverContext.java index f69fec2ae9..84edbc91b1 100644 --- a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5SolverContext.java +++ b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5SolverContext.java @@ -267,10 +267,9 @@ protected ProverEnvironment newProverEnvironment0(Set options) { } @Override - protected ProverEnvironment copyProverEnvironment0( - ProverEnvironment proverToCopy, Set options) { + protected ProverEnvironment copyProverEnvironment0(ProverEnvironment proverToCopy) { throw new UnsupportedOperationException( - "MathSAT5 does not support copying of prover " + "environments"); + "MathSAT5 does not support copying of prover environments"); } @Override @@ -282,9 +281,9 @@ protected InterpolatingProverEnvironment newProverEnvironmentWithInterpolatio @Override protected InterpolatingProverEnvironment copyProverEnvironmentWithInterpolation0( - ProverEnvironment proverToCopy, Set pSet) { + InterpolatingProverEnvironment proverToCopy) { throw new UnsupportedOperationException( - "MathSAT5 does not support copying of prover " + "environments"); + "MathSAT5 does not support copying of prover environments"); } @Override @@ -294,6 +293,13 @@ public OptimizationProverEnvironment newOptimizationProverEnvironment0( return new Mathsat5OptimizationProver(this, shutdownNotifier, creator, options); } + @Override + public OptimizationProverEnvironment copyOptimizationProverEnvironment( + OptimizationProverEnvironment proverToCopy) { + throw new UnsupportedOperationException( + "MathSAT5 does not support copying of prover environments"); + } + @Override public String getVersion() { return msat_get_version(); diff --git a/src/org/sosy_lab/java_smt/solvers/princess/PrincessSolverContext.java b/src/org/sosy_lab/java_smt/solvers/princess/PrincessSolverContext.java index 91f588fa95..4dfdaca094 100644 --- a/src/org/sosy_lab/java_smt/solvers/princess/PrincessSolverContext.java +++ b/src/org/sosy_lab/java_smt/solvers/princess/PrincessSolverContext.java @@ -78,10 +78,9 @@ protected ProverEnvironment newProverEnvironment0(Set options) { } @Override - protected ProverEnvironment copyProverEnvironment0( - ProverEnvironment proverToCopy, Set options) { + protected ProverEnvironment copyProverEnvironment0(ProverEnvironment proverToCopy) { throw new UnsupportedOperationException( - "Princess does not support the copying of " + "ProverEnvironments"); + "Princess does not support the copying of ProverEnvironments"); } @SuppressWarnings("resource") @@ -94,9 +93,9 @@ protected InterpolatingProverEnvironment newProverEnvironmentWithInterpolatio @Override protected InterpolatingProverEnvironment copyProverEnvironmentWithInterpolation0( - ProverEnvironment proverToCopy, Set pSet) { + InterpolatingProverEnvironment proverToCopy) { throw new UnsupportedOperationException( - "Princess does not support the copying of " + "ProverEnvironments"); + "Princess does not support the copying of ProverEnvironments"); } @Override @@ -105,6 +104,12 @@ public OptimizationProverEnvironment newOptimizationProverEnvironment0( throw new UnsupportedOperationException("Princess does not support optimization"); } + @Override + public OptimizationProverEnvironment copyOptimizationProverEnvironment( + OptimizationProverEnvironment proverToCopy) { + throw new UnsupportedOperationException("Princess does not support optimization"); + } + @Override public String getVersion() { return "Princess " + SimpleAPI.version(); diff --git a/src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolSolverContext.java b/src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolSolverContext.java index 3fc0dc878d..5aa35f5e27 100644 --- a/src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolSolverContext.java +++ b/src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolSolverContext.java @@ -232,10 +232,9 @@ protected ProverEnvironment newProverEnvironment0(Set options) { } @Override - protected ProverEnvironment copyProverEnvironment0( - ProverEnvironment proverToCopy, Set options) { + protected ProverEnvironment copyProverEnvironment0(ProverEnvironment proverToCopy) { throw new UnsupportedOperationException( - "SMTInterpol does not support the copying of " + "ProverEnvironments"); + "SMTInterpol does not support the copying of ProverEnvironments"); } @SuppressWarnings("resource") @@ -261,9 +260,9 @@ protected InterpolatingProverEnvironment newProverEnvironmentWithInterpolatio @Override protected InterpolatingProverEnvironment copyProverEnvironmentWithInterpolation0( - ProverEnvironment proverToCopy, Set pSet) { + InterpolatingProverEnvironment proverToCopy) { throw new UnsupportedOperationException( - "SMTInterpol does not support the copying of " + "ProverEnvironments"); + "SMTInterpol does not support the copying of ProverEnvironments"); } @Override @@ -272,6 +271,12 @@ public OptimizationProverEnvironment newOptimizationProverEnvironment0( throw new UnsupportedOperationException("SMTInterpol does not support optimization"); } + @Override + public OptimizationProverEnvironment copyOptimizationProverEnvironment( + OptimizationProverEnvironment proverToCopy) { + throw new UnsupportedOperationException("SMTInterpol does not support optimization"); + } + @Override public String getVersion() { QuotedObject program = (QuotedObject) manager.getEnvironment().getInfo(":name"); diff --git a/src/org/sosy_lab/java_smt/solvers/yices2/Yices2SolverContext.java b/src/org/sosy_lab/java_smt/solvers/yices2/Yices2SolverContext.java index d7064c4c29..1c0132d783 100644 --- a/src/org/sosy_lab/java_smt/solvers/yices2/Yices2SolverContext.java +++ b/src/org/sosy_lab/java_smt/solvers/yices2/Yices2SolverContext.java @@ -108,8 +108,7 @@ protected ProverEnvironment newProverEnvironment0(Set pOptions) { } @Override - protected ProverEnvironment copyProverEnvironment0( - ProverEnvironment proverToCopy, Set options) { + protected ProverEnvironment copyProverEnvironment0(ProverEnvironment proverToCopy) { throw new UnsupportedOperationException( "Yices2 does not support the copying of " + "ProverEnvironments"); } @@ -122,7 +121,7 @@ protected InterpolatingProverEnvironment newProverEnvironmentWithInterpolatio @Override protected InterpolatingProverEnvironment copyProverEnvironmentWithInterpolation0( - ProverEnvironment proverToCopy, Set pSet) { + InterpolatingProverEnvironment proverToCopy) { throw new UnsupportedOperationException( "Yices2 does not support the copying of " + "ProverEnvironments"); } @@ -133,6 +132,12 @@ protected OptimizationProverEnvironment newOptimizationProverEnvironment0( throw new UnsupportedOperationException("Yices does not support optimization"); } + @Override + public OptimizationProverEnvironment copyOptimizationProverEnvironment( + OptimizationProverEnvironment proverToCopy) { + throw new UnsupportedOperationException("Yices does not support optimization"); + } + @Override protected boolean supportsAssumptionSolving() { return true; diff --git a/src/org/sosy_lab/java_smt/solvers/z3/Z3AbstractProver.java b/src/org/sosy_lab/java_smt/solvers/z3/Z3AbstractProver.java index b990e239f4..68eec404a0 100644 --- a/src/org/sosy_lab/java_smt/solvers/z3/Z3AbstractProver.java +++ b/src/org/sosy_lab/java_smt/solvers/z3/Z3AbstractProver.java @@ -48,6 +48,8 @@ abstract class Z3AbstractProver extends AbstractProverWithAllSat { // m_n_obj in Z3 protected final long z3solver; + private final Set options; + private final UniqueIdGenerator trackId = new UniqueIdGenerator(); private final @Nullable Map storedConstraints; @@ -62,7 +64,13 @@ abstract class Z3AbstractProver extends AbstractProverWithAllSat { ImmutableMap pSolverOptions, @Nullable PathCounterTemplate pLogfile, ShutdownNotifier pShutdownNotifier) { - this(pCreator, pMgr, Native.mkSolver(pCreator.getEnv()), pOptions, pSolverOptions, pLogfile, + this( + pCreator, + pMgr, + Native.mkSolver(pCreator.getEnv()), + pOptions, + pSolverOptions, + pLogfile, pShutdownNotifier); } @@ -86,6 +94,7 @@ abstract class Z3AbstractProver extends AbstractProverWithAllSat { logfile = pLogfile; mgr = pMgr; + options = pOptions; postProcessProverCreation(pSolverOptions); } @@ -373,4 +382,8 @@ protected void assertContraint(long negatedModel) { protected final long getZ3Solver() { return z3solver; } + + protected Set getZ3ProverOptions() { + return options; + } } diff --git a/src/org/sosy_lab/java_smt/solvers/z3/Z3SolverContext.java b/src/org/sosy_lab/java_smt/solvers/z3/Z3SolverContext.java index ee09e0731a..70bb01e00f 100644 --- a/src/org/sosy_lab/java_smt/solvers/z3/Z3SolverContext.java +++ b/src/org/sosy_lab/java_smt/solvers/z3/Z3SolverContext.java @@ -234,8 +234,7 @@ protected ProverEnvironment newProverEnvironment0(Set options) { } @Override - protected ProverEnvironment copyProverEnvironment0( - ProverEnvironment proverToCopy, Set options) { + protected ProverEnvironment copyProverEnvironment0(ProverEnvironment proverToCopy) { Preconditions.checkState(!closed, "solver context is already closed"); Preconditions.checkArgument( proverToCopy instanceof Z3AbstractProver, @@ -255,6 +254,9 @@ protected ProverEnvironment copyProverEnvironment0( Native.solverDecRef(creator.getEnv(), z3ast); } + // Get the original options from the previous solver + Set options = ((Z3AbstractProver) proverToCopy).getZ3ProverOptions(); + return new Z3TheoremProver( creator, manager, @@ -287,7 +289,7 @@ protected InterpolatingProverEnvironment newProverEnvironmentWithInterpolatio @Override protected InterpolatingProverEnvironment copyProverEnvironmentWithInterpolation0( - ProverEnvironment proverToCopy, Set pSet) { + InterpolatingProverEnvironment proverToCopy) { throw new UnsupportedOperationException("Z3 does not support interpolation"); } @@ -312,6 +314,13 @@ public OptimizationProverEnvironment newOptimizationProverEnvironment0( shutdownNotifier); } + @Override + public OptimizationProverEnvironment copyOptimizationProverEnvironment( + OptimizationProverEnvironment proverToCopy) { + // TODO: check if we can do this! + throw new UnsupportedOperationException("Z3 does not support copying of optimization provers."); + } + @Override public String getVersion() { Native.IntPtr major = new Native.IntPtr();