322 feature request clone proverenvironment with stack

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

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<ProverOptions> 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<ProverOptions> pSet);
 
+  protected abstract InterpolatingProverEnvironment<?> copyProverEnvironmentWithInterpolation0(
+      InterpolatingProverEnvironment<?> proverToCopy);
+
   @SuppressWarnings("resource")
   @Override
   public final OptimizationProverEnvironment newOptimizationProverEnvironment(

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,13 +56,30 @@ 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) {
     return new LoggingOptimizationProverEnvironment(
         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();

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,13 +53,29 @@ 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) {
     return new StatisticsOptimizationProverEnvironment(
         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();

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

src/org/sosy_lab/java_smt/solvers/boolector/BoolectorSolverContext.java

@@ -204,18 +204,37 @@ protected ProverEnvironment newProverEnvironment0(Set<ProverOptions> 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<ProverOptions> 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<ProverOptions> 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;

src/org/sosy_lab/java_smt/solvers/cvc4/CVC4SolverContext.java

@@ -137,6 +137,12 @@ public ProverEnvironment newProverEnvironment0(Set<ProverOptions> 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<ProverOptions> pSet) {
     throw new UnsupportedOperationException("CVC4 does not support optimization");
   }
+
+  @Override
+  public OptimizationProverEnvironment copyOptimizationProverEnvironment(
+      OptimizationProverEnvironment proverToCopy) {
+    throw new UnsupportedOperationException("CVC4 does not support optimization");
+  }
 }

src/org/sosy_lab/java_smt/solvers/cvc5/CVC5SolverContext.java

@@ -157,6 +157,12 @@ public ProverEnvironment newProverEnvironment0(Set<ProverOptions> 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<ProverOptions> pSet) {
     throw new UnsupportedOperationException("CVC5 does not support optimization");
   }
+
+  @Override
+  public OptimizationProverEnvironment copyOptimizationProverEnvironment(
+      OptimizationProverEnvironment proverToCopy) {
+    throw new UnsupportedOperationException("CVC5 does not support optimization");
+  }
 }