diff --git a/src/org/sosy_lab/java_smt/api/SolverContext.java b/src/org/sosy_lab/java_smt/api/SolverContext.java index 3fbd476c77..d3f6a6918a 100644 --- a/src/org/sosy_lab/java_smt/api/SolverContext.java +++ b/src/org/sosy_lab/java_smt/api/SolverContext.java @@ -65,6 +65,16 @@ 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}. Options are carried over from proverToCopy. + * + * @param proverToCopy An existing {@link ProverEnvironment}, whichs assertion stack is to be + * copied into the new one. + */ + ProverEnvironment copyProverEnvironment(ProverEnvironment proverToCopy); + /** * 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 +86,20 @@ 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 + * 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 InterpolatingProverEnvironment}, whichs assertion stack + * is to be copied into the new one. + */ + InterpolatingProverEnvironment copyProverEnvironmentWithInterpolation( + InterpolatingProverEnvironment proverToCopy); + /** * Create a fresh new {@link OptimizationProverEnvironment} which encapsulates an assertion stack * and allows solving optimization queries. @@ -85,6 +109,18 @@ enum ProverOptions { */ 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 ab49b14cfc..ba046dc705 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/AbstractSolverContext.java +++ b/src/org/sosy_lab/java_smt/basicimpl/AbstractSolverContext.java @@ -46,8 +46,21 @@ public final ProverEnvironment newProverEnvironment(ProverOptions... options) { return out; } + @Override + 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 + out = new ProverWithAssumptionsWrapper(out); + } + return out; + } + protected abstract ProverEnvironment newProverEnvironment0(Set options); + protected abstract ProverEnvironment copyProverEnvironment0(ProverEnvironment proverToCopy); + @SuppressWarnings("resource") @Override public final InterpolatingProverEnvironment newProverEnvironmentWithInterpolation( @@ -62,9 +75,26 @@ public final InterpolatingProverEnvironment newProverEnvironmentWithInterpola return out; } + @SuppressWarnings("resource") + @Override + public final InterpolatingProverEnvironment copyProverEnvironmentWithInterpolation( + InterpolatingProverEnvironment proverToCopy) { + + 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 + out = new InterpolatingProverWithAssumptionsWrapper<>(out, fmgr); + } + return out; + } + protected abstract InterpolatingProverEnvironment newProverEnvironmentWithInterpolation0( Set pSet); + protected abstract InterpolatingProverEnvironment copyProverEnvironmentWithInterpolation0( + InterpolatingProverEnvironment proverToCopy); + @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..ea6b8585cc 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,13 @@ public ProverEnvironment newProverEnvironment(ProverOptions... pOptions) { return new LoggingProverEnvironment(logger, delegate.newProverEnvironment(pOptions)); } + @SuppressWarnings("resource") + @Override + public ProverEnvironment copyProverEnvironment(ProverEnvironment proverToCopy) { + // TODO: log this? Because this is not a normal new prover? + return new LoggingProverEnvironment(logger, delegate.copyProverEnvironment(proverToCopy)); + } + @SuppressWarnings("resource") @Override public InterpolatingProverEnvironment newProverEnvironmentWithInterpolation( @@ -49,6 +56,15 @@ public InterpolatingProverEnvironment newProverEnvironmentWithInterpolation( logger, delegate.newProverEnvironmentWithInterpolation(options)); } + @SuppressWarnings("resource") + @Override + public InterpolatingProverEnvironment copyProverEnvironmentWithInterpolation( + InterpolatingProverEnvironment proverToCopy) { + // TODO: log this? Because this is not a normal new prover? + return new LoggingInterpolatingProverEnvironment<>( + logger, delegate.copyProverEnvironmentWithInterpolation(proverToCopy)); + } + @SuppressWarnings("resource") @Override public OptimizationProverEnvironment newOptimizationProverEnvironment(ProverOptions... options) { @@ -56,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 214d2dd576..48a9ae409a 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,12 @@ public ProverEnvironment newProverEnvironment(ProverOptions... pOptions) { return new StatisticsProverEnvironment(delegate.newProverEnvironment(pOptions), stats); } + @SuppressWarnings("resource") + @Override + public ProverEnvironment copyProverEnvironment(ProverEnvironment proverToCopy) { + return new StatisticsProverEnvironment(delegate.copyProverEnvironment(proverToCopy), stats); + } + @SuppressWarnings("resource") @Override public InterpolatingProverEnvironment newProverEnvironmentWithInterpolation( @@ -47,6 +53,14 @@ public InterpolatingProverEnvironment newProverEnvironmentWithInterpolation( delegate.newProverEnvironmentWithInterpolation(pOptions), stats); } + @SuppressWarnings("resource") + @Override + public InterpolatingProverEnvironment copyProverEnvironmentWithInterpolation( + InterpolatingProverEnvironment proverToCopy) { + return new StatisticsInterpolatingProverEnvironment<>( + delegate.copyProverEnvironmentWithInterpolation(proverToCopy), stats); + } + @SuppressWarnings("resource") @Override public OptimizationProverEnvironment newOptimizationProverEnvironment(ProverOptions... pOptions) { @@ -54,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 bea5a9fb00..03556a3d19 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) { } } + @SuppressWarnings("resource") + @Override + public ProverEnvironment copyProverEnvironment(ProverEnvironment proverToCopy) { + synchronized (sync) { + if (useSeperateProvers) { + SolverContext otherContext = createOtherContext(); + return new SynchronizedProverEnvironmentWithContext( + otherContext.copyProverEnvironment(proverToCopy), + sync, + delegate.getFormulaManager(), + otherContext.getFormulaManager()); + } else { + return new SynchronizedProverEnvironment( + delegate.copyProverEnvironment(proverToCopy), delegate); + } + } + } + @SuppressWarnings("resource") @Override public InterpolatingProverEnvironment newProverEnvironmentWithInterpolation( @@ -113,6 +131,25 @@ public InterpolatingProverEnvironment newProverEnvironmentWithInterpolation( } } + @SuppressWarnings("resource") + @Override + public InterpolatingProverEnvironment copyProverEnvironmentWithInterpolation( + InterpolatingProverEnvironment proverToCopy) { + synchronized (sync) { + if (useSeperateProvers) { + SolverContext otherContext = createOtherContext(); + return new SynchronizedInterpolatingProverEnvironmentWithContext<>( + otherContext.copyProverEnvironmentWithInterpolation(proverToCopy), + sync, + delegate.getFormulaManager(), + otherContext.getFormulaManager()); + } else { + return new SynchronizedInterpolatingProverEnvironment<>( + delegate.copyProverEnvironmentWithInterpolation(proverToCopy), delegate); + } + } + } + @SuppressWarnings("resource") @Override public OptimizationProverEnvironment newOptimizationProverEnvironment(ProverOptions... pOptions) { @@ -124,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 6c90828e93..9d1d643efe 100644 --- a/src/org/sosy_lab/java_smt/solvers/boolector/BoolectorSolverContext.java +++ b/src/org/sosy_lab/java_smt/solvers/boolector/BoolectorSolverContext.java @@ -204,18 +204,37 @@ protected ProverEnvironment newProverEnvironment0(Set pOptions) { manager, creator, creator.getEnv(), shutdownNotifier, pOptions, isAnyStackAlive); } + @Override + protected ProverEnvironment copyProverEnvironment0(ProverEnvironment proverToCopy) { + 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( + InterpolatingProverEnvironment proverToCopy) { + throw new UnsupportedOperationException( + "Boolector does not support the copying of ProverEnvironments"); + } + @Override protected OptimizationProverEnvironment newOptimizationProverEnvironment0( Set pSet) { 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 b5bd086812..ac11fb19f0 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,12 @@ public ProverEnvironment newProverEnvironment0(Set pOptions) { getFormulaManager().getBooleanFormulaManager()); } + @Override + protected ProverEnvironment copyProverEnvironment0(ProverEnvironment proverToCopy) { + throw new UnsupportedOperationException( + "CVC4 does not support the copying of " + "ProverEnvironments"); + } + @Override protected boolean supportsAssumptionSolving() { return false; @@ -148,9 +154,22 @@ protected InterpolatingProverEnvironment newProverEnvironmentWithInterpolatio throw new UnsupportedOperationException("CVC4 does not support interpolation"); } + @Override + protected InterpolatingProverEnvironment copyProverEnvironmentWithInterpolation0( + InterpolatingProverEnvironment proverToCopy) { + throw new UnsupportedOperationException( + "CVC4 does not support the copying of " + "ProverEnvironments"); + } + @Override 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 03a99a65da..8701cdb55c 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,12 @@ public ProverEnvironment newProverEnvironment0(Set pOptions) { creator, shutdownNotifier, randomSeed, pOptions, getFormulaManager()); } + @Override + protected ProverEnvironment copyProverEnvironment0(ProverEnvironment proverToCopy) { + throw new UnsupportedOperationException( + "CVC5 does not support the copying of ProverEnvironments"); + } + @Override protected boolean supportsAssumptionSolving() { return false; @@ -168,9 +174,22 @@ protected InterpolatingProverEnvironment newProverEnvironmentWithInterpolatio throw new UnsupportedOperationException("CVC5 does not support Craig interpolation."); } + @Override + protected InterpolatingProverEnvironment copyProverEnvironmentWithInterpolation0( + InterpolatingProverEnvironment proverToCopy) { + throw new UnsupportedOperationException( + "CVC5 does not support the copying of ProverEnvironments"); + } + @Override 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 6c356e10cf..84edbc91b1 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,12 @@ protected ProverEnvironment newProverEnvironment0(Set options) { return new Mathsat5TheoremProver(this, shutdownNotifier, creator, options); } + @Override + protected ProverEnvironment copyProverEnvironment0(ProverEnvironment proverToCopy) { + throw new UnsupportedOperationException( + "MathSAT5 does not support copying of prover environments"); + } + @Override protected InterpolatingProverEnvironment newProverEnvironmentWithInterpolation0( Set options) { @@ -273,6 +279,13 @@ protected InterpolatingProverEnvironment newProverEnvironmentWithInterpolatio return new Mathsat5InterpolatingProver(this, shutdownNotifier, creator, options); } + @Override + protected InterpolatingProverEnvironment copyProverEnvironmentWithInterpolation0( + InterpolatingProverEnvironment proverToCopy) { + throw new UnsupportedOperationException( + "MathSAT5 does not support copying of prover environments"); + } + @Override public OptimizationProverEnvironment newOptimizationProverEnvironment0( Set options) { @@ -280,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 36a7444539..4dfdaca094 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,12 @@ protected ProverEnvironment newProverEnvironment0(Set options) { return (PrincessTheoremProver) creator.getEnv().getNewProver(false, manager, creator, options); } + @Override + protected ProverEnvironment copyProverEnvironment0(ProverEnvironment proverToCopy) { + throw new UnsupportedOperationException( + "Princess does not support the copying of ProverEnvironments"); + } + @SuppressWarnings("resource") @Override protected InterpolatingProverEnvironment newProverEnvironmentWithInterpolation0( @@ -85,12 +91,25 @@ protected InterpolatingProverEnvironment newProverEnvironmentWithInterpolatio creator.getEnv().getNewProver(true, manager, creator, options); } + @Override + protected InterpolatingProverEnvironment copyProverEnvironmentWithInterpolation0( + InterpolatingProverEnvironment proverToCopy) { + throw new UnsupportedOperationException( + "Princess does not support the copying of ProverEnvironments"); + } + @Override public OptimizationProverEnvironment newOptimizationProverEnvironment0( Set options) { 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 e9620756df..5aa35f5e27 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,12 @@ protected ProverEnvironment newProverEnvironment0(Set options) { return new SmtInterpolTheoremProver(manager, newScript, options, shutdownNotifier); } + @Override + protected ProverEnvironment copyProverEnvironment0(ProverEnvironment proverToCopy) { + throw new UnsupportedOperationException( + "SMTInterpol does not support the copying of ProverEnvironments"); + } + @SuppressWarnings("resource") @Override protected InterpolatingProverEnvironment newProverEnvironmentWithInterpolation0( @@ -252,12 +258,25 @@ protected InterpolatingProverEnvironment newProverEnvironmentWithInterpolatio return prover; } + @Override + protected InterpolatingProverEnvironment copyProverEnvironmentWithInterpolation0( + InterpolatingProverEnvironment proverToCopy) { + throw new UnsupportedOperationException( + "SMTInterpol does not support the copying of ProverEnvironments"); + } + @Override public OptimizationProverEnvironment newOptimizationProverEnvironment0( Set options) { 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 c68e90aa3c..1c0132d783 100644 --- a/src/org/sosy_lab/java_smt/solvers/yices2/Yices2SolverContext.java +++ b/src/org/sosy_lab/java_smt/solvers/yices2/Yices2SolverContext.java @@ -107,18 +107,37 @@ protected ProverEnvironment newProverEnvironment0(Set pOptions) { return new Yices2TheoremProver(creator, pOptions, bfmgr, shutdownManager); } + @Override + protected ProverEnvironment copyProverEnvironment0(ProverEnvironment proverToCopy) { + 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( + InterpolatingProverEnvironment proverToCopy) { + throw new UnsupportedOperationException( + "Yices2 does not support the copying of " + "ProverEnvironments"); + } + @Override protected OptimizationProverEnvironment newOptimizationProverEnvironment0( Set pSet) { 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 933c4a77eb..68eec404a0 100644 --- a/src/org/sosy_lab/java_smt/solvers/z3/Z3AbstractProver.java +++ b/src/org/sosy_lab/java_smt/solvers/z3/Z3AbstractProver.java @@ -45,8 +45,11 @@ abstract class Z3AbstractProver extends AbstractProverWithAllSat { protected final long z3context; private final Z3FormulaManager mgr; + // m_n_obj in Z3 protected final long z3solver; + private final Set options; + private final UniqueIdGenerator trackId = new UniqueIdGenerator(); private final @Nullable Map storedConstraints; @@ -61,10 +64,28 @@ abstract class Z3AbstractProver extends AbstractProverWithAllSat { ImmutableMap pSolverOptions, @Nullable PathCounterTemplate pLogfile, ShutdownNotifier pShutdownNotifier) { + this( + pCreator, + pMgr, + Native.mkSolver(pCreator.getEnv()), + pOptions, + pSolverOptions, + pLogfile, + pShutdownNotifier); + } + + 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 = Native.mkSolver(z3context); + z3solver = pZ3solver; interruptListener = reason -> Native.solverInterrupt(z3context, z3solver); shutdownNotifier.register(interruptListener); @@ -73,6 +94,11 @@ abstract class Z3AbstractProver extends AbstractProverWithAllSat { logfile = pLogfile; mgr = pMgr; + options = pOptions; + postProcessProverCreation(pSolverOptions); + } + + private void postProcessProverCreation(ImmutableMap pSolverOptions) { Native.solverIncRef(z3context, z3solver); long z3params = Native.mkParams(z3context); @@ -352,4 +378,12 @@ public R allSat(AllSatCallback callback, List important) protected void assertContraint(long negatedModel) { Native.solverAssert(z3context, z3solver, 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 d081dd5e8e..70bb01e00f 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,12 @@ 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.Set; import java.util.function.Consumer; import java.util.logging.Level; @@ -48,6 +52,10 @@ public final class Z3SolverContext extends AbstractSolverContext { private final Z3FormulaManager manager; private boolean closed = false; + private final ReferenceQueue referenceQueue = new ReferenceQueue<>(); + 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"; @@ -216,20 +224,61 @@ 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) { + 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); + } + + // Get the original options from the previous solver + Set options = ((Z3AbstractProver) proverToCopy).getZ3ProverOptions(); + + return new Z3TheoremProver( + creator, + manager, + z3solver, + options, + generateSolverOptions(options), + extraOptions.logfile, + shutdownNotifier); + } + + private 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 +287,12 @@ protected InterpolatingProverEnvironment newProverEnvironmentWithInterpolatio throw new UnsupportedOperationException("Z3 does not support interpolation"); } + @Override + protected InterpolatingProverEnvironment copyProverEnvironmentWithInterpolation0( + InterpolatingProverEnvironment proverToCopy) { + throw new UnsupportedOperationException("Z3 does not support interpolation"); + } + @Override public OptimizationProverEnvironment newOptimizationProverEnvironment0( Set options) { @@ -259,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(); 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..ccd1b91eec 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, pZ3solver, pOptions, pSolverOptions, pLogfile, pShutdownNotifier); + } + @Override @Nullable public Void addConstraint(BooleanFormula f) throws InterruptedException { 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..f0e83081a4 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,65 @@ public void testFormulaAccessAfterClose() { assertThat(bmgr.isTrue(opTerm)).isFalse(); assertThat(bmgr.isFalse(opTerm)).isFalse(); } + + @Test + public void testProverCopying() throws SolverException, InterruptedException { + requireProverCopying(); + try (ProverEnvironment prover = context.newProverEnvironment()) { + assertThat(prover.isUnsat()).isFalse(); + try (ProverEnvironment copiedProver = context.copyProverEnvironment(prover)) { + assertThat(copiedProver.isUnsat()).isFalse(); + } + } + } + + @SuppressWarnings("resource") + @Test + public void testProverCopyCloseInitialProver() throws SolverException, InterruptedException { + requireProverCopying(); + ProverEnvironment prover = context.newProverEnvironment(); + try (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. + */ + @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()) { + 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(); + } + } + } }