Add new prover environments with a dedicated prover shutdown notifier to delegates

BaierD · BaierD · commit c85042b3f325 · 2025-06-04T13:41:13.000+02:00
diff --git a/src/org/sosy_lab/java_smt/delegate/debugging/DebuggingBasicProverEnvironment.java b/src/org/sosy_lab/java_smt/delegate/debugging/DebuggingBasicProverEnvironment.java
@@ -15,7 +15,6 @@
 import java.util.List;
 import java.util.Optional;
 import org.checkerframework.checker.nullness.qual.Nullable;
-import org.sosy_lab.common.ShutdownManager;
 import org.sosy_lab.java_smt.api.BasicProverEnvironment;
 import org.sosy_lab.java_smt.api.BooleanFormula;
 import org.sosy_lab.java_smt.api.Model;
@@ -32,11 +31,6 @@ class DebuggingBasicProverEnvironment<T> implements BasicProverEnvironment<T> {
     debugging = pDebugging;
   }
 
-  @Override
-  public ShutdownManager getShutdownManagerForProver() throws UnsupportedOperationException {
-    return delegate.getShutdownManagerForProver();
-  }
-
   @Override
   public void pop() {
     debugging.assertThreadLocal();
diff --git a/src/org/sosy_lab/java_smt/delegate/debugging/DebuggingOptimizationProverEnvironment.java b/src/org/sosy_lab/java_smt/delegate/debugging/DebuggingOptimizationProverEnvironment.java
@@ -9,7 +9,6 @@
 package org.sosy_lab.java_smt.delegate.debugging;
 
 import java.util.Optional;
-import org.sosy_lab.common.ShutdownManager;
 import org.sosy_lab.common.rationals.Rational;
 import org.sosy_lab.java_smt.api.Formula;
 import org.sosy_lab.java_smt.api.OptimizationProverEnvironment;
@@ -27,11 +26,6 @@ public DebuggingOptimizationProverEnvironment(
     debugging = pDebugging;
   }
 
-  @Override
-  public ShutdownManager getShutdownManagerForProver() throws UnsupportedOperationException {
-    return delegate.getShutdownManagerForProver();
-  }
-
   @Override
   public int maximize(Formula objective) {
     debugging.assertThreadLocal();
diff --git a/src/org/sosy_lab/java_smt/delegate/debugging/DebuggingSolverContext.java b/src/org/sosy_lab/java_smt/delegate/debugging/DebuggingSolverContext.java
@@ -11,6 +11,7 @@
 import static com.google.common.base.Preconditions.checkNotNull;
 
 import com.google.common.collect.ImmutableMap;
+import org.sosy_lab.common.ShutdownNotifier;
 import org.sosy_lab.common.configuration.Configuration;
 import org.sosy_lab.common.configuration.InvalidConfigurationException;
 import org.sosy_lab.java_smt.SolverContextFactory.Solvers;
@@ -47,6 +48,15 @@ public ProverEnvironment newProverEnvironment(ProverOptions... options) {
     return new DebuggingProverEnvironment(delegate.newProverEnvironment(options), debugging);
   }
 
+  @SuppressWarnings("resource")
+  @Override
+  public ProverEnvironment newProverEnvironment(
+      ShutdownNotifier pProverShutdownNotifier, ProverOptions... options) {
+    debugging.assertThreadLocal();
+    return new DebuggingProverEnvironment(
+        delegate.newProverEnvironment(pProverShutdownNotifier, options), debugging);
+  }
+
   @SuppressWarnings("resource")
   @Override
   public InterpolatingProverEnvironment<?> newProverEnvironmentWithInterpolation(
@@ -56,6 +66,16 @@ public InterpolatingProverEnvironment<?> newProverEnvironmentWithInterpolation(
         delegate.newProverEnvironmentWithInterpolation(options), debugging);
   }
 
+  @SuppressWarnings("resource")
+  @Override
+  public InterpolatingProverEnvironment<?> newProverEnvironmentWithInterpolation(
+      ShutdownNotifier pProverShutdownNotifier, ProverOptions... options) {
+    debugging.assertThreadLocal();
+    return new DebuggingInterpolatingProverEnvironment<>(
+        delegate.newProverEnvironmentWithInterpolation(pProverShutdownNotifier, options),
+        debugging);
+  }
+
   @SuppressWarnings("resource")
   @Override
   public OptimizationProverEnvironment newOptimizationProverEnvironment(ProverOptions... options) {
@@ -64,6 +84,15 @@ public OptimizationProverEnvironment newOptimizationProverEnvironment(ProverOpti
         delegate.newOptimizationProverEnvironment(options), debugging);
   }
 
+  @SuppressWarnings("resource")
+  @Override
+  public OptimizationProverEnvironment newOptimizationProverEnvironment(
+      ShutdownNotifier pProverShutdownNotifier, ProverOptions... options) {
+    debugging.assertThreadLocal();
+    return new DebuggingOptimizationProverEnvironment(
+        delegate.newOptimizationProverEnvironment(pProverShutdownNotifier, options), debugging);
+  }
+
   @Override
   public String getVersion() {
     debugging.assertThreadLocal();
diff --git a/src/org/sosy_lab/java_smt/delegate/logging/LoggingBasicProverEnvironment.java b/src/org/sosy_lab/java_smt/delegate/logging/LoggingBasicProverEnvironment.java
@@ -18,7 +18,6 @@
 import java.util.Optional;
 import java.util.logging.Level;
 import org.checkerframework.checker.nullness.qual.Nullable;
-import org.sosy_lab.common.ShutdownManager;
 import org.sosy_lab.common.log.LogManager;
 import org.sosy_lab.java_smt.api.BasicProverEnvironment;
 import org.sosy_lab.java_smt.api.BooleanFormula;
@@ -39,11 +38,6 @@ class LoggingBasicProverEnvironment<T> implements BasicProverEnvironment<T> {
     logger = checkNotNull(pLogger);
   }
 
-  @Override
-  public ShutdownManager getShutdownManagerForProver() throws UnsupportedOperationException {
-    return wrapped.getShutdownManagerForProver();
-  }
-
   @Override
   public @Nullable T push(BooleanFormula f) throws InterruptedException {
     logger.log(Level.FINE, "up to level " + level++);
diff --git a/src/org/sosy_lab/java_smt/delegate/logging/LoggingSolverContext.java b/src/org/sosy_lab/java_smt/delegate/logging/LoggingSolverContext.java
@@ -11,6 +11,7 @@
 import static com.google.common.base.Preconditions.checkNotNull;
 
 import com.google.common.collect.ImmutableMap;
+import org.sosy_lab.common.ShutdownNotifier;
 import org.sosy_lab.common.log.LogManager;
 import org.sosy_lab.java_smt.SolverContextFactory.Solvers;
 import org.sosy_lab.java_smt.api.FormulaManager;
@@ -41,6 +42,14 @@ public ProverEnvironment newProverEnvironment(ProverOptions... pOptions) {
     return new LoggingProverEnvironment(logger, delegate.newProverEnvironment(pOptions));
   }
 
+  @SuppressWarnings("resource")
+  @Override
+  public ProverEnvironment newProverEnvironment(
+      ShutdownNotifier pProverShutdownNotifier, ProverOptions... pOptions) {
+    return new LoggingProverEnvironment(
+        logger, delegate.newProverEnvironment(pProverShutdownNotifier, pOptions));
+  }
+
   @SuppressWarnings("resource")
   @Override
   public InterpolatingProverEnvironment<?> newProverEnvironmentWithInterpolation(
@@ -49,13 +58,29 @@ public InterpolatingProverEnvironment<?> newProverEnvironmentWithInterpolation(
         logger, delegate.newProverEnvironmentWithInterpolation(options));
   }
 
+  @SuppressWarnings("resource")
+  @Override
+  public InterpolatingProverEnvironment<?> newProverEnvironmentWithInterpolation(
+      ShutdownNotifier pProverShutdownNotifier, ProverOptions... options) {
+    return new LoggingInterpolatingProverEnvironment<>(
+        logger, delegate.newProverEnvironmentWithInterpolation(pProverShutdownNotifier, options));
+  }
+
   @SuppressWarnings("resource")
   @Override
   public OptimizationProverEnvironment newOptimizationProverEnvironment(ProverOptions... options) {
     return new LoggingOptimizationProverEnvironment(
         logger, delegate.newOptimizationProverEnvironment(options));
   }
 
+  @SuppressWarnings("resource")
+  @Override
+  public OptimizationProverEnvironment newOptimizationProverEnvironment(
+      ShutdownNotifier pProverShutdownNotifier, ProverOptions... options) {
+    return new LoggingOptimizationProverEnvironment(
+        logger, delegate.newOptimizationProverEnvironment(pProverShutdownNotifier, options));
+  }
+
   @Override
   public String getVersion() {
     return delegate.getVersion();
diff --git a/src/org/sosy_lab/java_smt/delegate/logging/PackageSanityTest.java b/src/org/sosy_lab/java_smt/delegate/logging/PackageSanityTest.java
@@ -9,5 +9,12 @@
 package org.sosy_lab.java_smt.delegate.logging;
 
 import com.google.common.testing.AbstractPackageSanityTests;
+import org.sosy_lab.common.ShutdownManager;
 
-public class PackageSanityTest extends AbstractPackageSanityTests {}
+public class PackageSanityTest extends AbstractPackageSanityTests {
+
+  // WTF?
+  {
+    setDefault(org.sosy_lab.common.ShutdownNotifier.class, ShutdownManager.create().getNotifier());
+  }
+}
diff --git a/src/org/sosy_lab/java_smt/delegate/statistics/StatisticsBasicProverEnvironment.java b/src/org/sosy_lab/java_smt/delegate/statistics/StatisticsBasicProverEnvironment.java
@@ -15,7 +15,6 @@
 import java.util.List;
 import java.util.Optional;
 import org.checkerframework.checker.nullness.qual.Nullable;
-import org.sosy_lab.common.ShutdownManager;
 import org.sosy_lab.java_smt.api.BasicProverEnvironment;
 import org.sosy_lab.java_smt.api.BooleanFormula;
 import org.sosy_lab.java_smt.api.Model;
@@ -38,11 +37,6 @@ class StatisticsBasicProverEnvironment<T> implements BasicProverEnvironment<T> {
     stats.provers.getAndIncrement();
   }
 
-  @Override
-  public ShutdownManager getShutdownManagerForProver() throws UnsupportedOperationException {
-    return delegate.getShutdownManagerForProver();
-  }
-
   @Override
   public void pop() {
     stats.pop.getAndIncrement();
diff --git a/src/org/sosy_lab/java_smt/delegate/statistics/StatisticsSolverContext.java b/src/org/sosy_lab/java_smt/delegate/statistics/StatisticsSolverContext.java
@@ -12,6 +12,7 @@
 
 import com.google.common.collect.ImmutableMap;
 import java.util.Map;
+import org.sosy_lab.common.ShutdownNotifier;
 import org.sosy_lab.java_smt.SolverContextFactory.Solvers;
 import org.sosy_lab.java_smt.api.FormulaManager;
 import org.sosy_lab.java_smt.api.InterpolatingProverEnvironment;
@@ -39,6 +40,14 @@ public ProverEnvironment newProverEnvironment(ProverOptions... pOptions) {
     return new StatisticsProverEnvironment(delegate.newProverEnvironment(pOptions), stats);
   }
 
+  @SuppressWarnings("resource")
+  @Override
+  public ProverEnvironment newProverEnvironment(
+      ShutdownNotifier pProverShutdownNotifier, ProverOptions... pOptions) {
+    return new StatisticsProverEnvironment(
+        delegate.newProverEnvironment(pProverShutdownNotifier, pOptions), stats);
+  }
+
   @SuppressWarnings("resource")
   @Override
   public InterpolatingProverEnvironment<?> newProverEnvironmentWithInterpolation(
@@ -47,13 +56,29 @@ public InterpolatingProverEnvironment<?> newProverEnvironmentWithInterpolation(
         delegate.newProverEnvironmentWithInterpolation(pOptions), stats);
   }
 
+  @SuppressWarnings("resource")
+  @Override
+  public InterpolatingProverEnvironment<?> newProverEnvironmentWithInterpolation(
+      ShutdownNotifier pProverShutdownNotifier, ProverOptions... options) {
+    return new StatisticsInterpolatingProverEnvironment<>(
+        delegate.newProverEnvironmentWithInterpolation(pProverShutdownNotifier, options), stats);
+  }
+
   @SuppressWarnings("resource")
   @Override
   public OptimizationProverEnvironment newOptimizationProverEnvironment(ProverOptions... pOptions) {
     return new StatisticsOptimizationProverEnvironment(
         delegate.newOptimizationProverEnvironment(pOptions), stats);
   }
 
+  @SuppressWarnings("resource")
+  @Override
+  public OptimizationProverEnvironment newOptimizationProverEnvironment(
+      ShutdownNotifier pProverShutdownNotifier, ProverOptions... options) {
+    return new StatisticsOptimizationProverEnvironment(
+        delegate.newOptimizationProverEnvironment(pProverShutdownNotifier, options), stats);
+  }
+
   @Override
   public String getVersion() {
     return delegate.getVersion();
diff --git a/src/org/sosy_lab/java_smt/delegate/synchronize/SynchronizedBasicProverEnvironment.java b/src/org/sosy_lab/java_smt/delegate/synchronize/SynchronizedBasicProverEnvironment.java
@@ -16,7 +16,6 @@
 import java.util.List;
 import java.util.Optional;
 import org.checkerframework.checker.nullness.qual.Nullable;
-import org.sosy_lab.common.ShutdownManager;
 import org.sosy_lab.java_smt.api.BasicProverEnvironment;
 import org.sosy_lab.java_smt.api.BooleanFormula;
 import org.sosy_lab.java_smt.api.Model;
@@ -34,11 +33,6 @@ class SynchronizedBasicProverEnvironment<T> implements BasicProverEnvironment<T>
     sync = checkNotNull(pSync);
   }
 
-  @Override
-  public ShutdownManager getShutdownManagerForProver() throws UnsupportedOperationException {
-    return delegate.getShutdownManagerForProver();
-  }
-
   @Override
   public void pop() {
     synchronized (sync) {
diff --git a/src/org/sosy_lab/java_smt/delegate/synchronize/SynchronizedBasicProverEnvironmentWithContext.java b/src/org/sosy_lab/java_smt/delegate/synchronize/SynchronizedBasicProverEnvironmentWithContext.java
@@ -16,7 +16,6 @@
 import java.util.List;
 import java.util.Optional;
 import org.checkerframework.checker.nullness.qual.Nullable;
-import org.sosy_lab.common.ShutdownManager;
 import org.sosy_lab.java_smt.api.BasicProverEnvironment;
 import org.sosy_lab.java_smt.api.BooleanFormula;
 import org.sosy_lab.java_smt.api.FormulaManager;
@@ -151,11 +150,6 @@ public <R> R allSat(AllSatCallback<R> pCallback, List<BooleanFormula> pImportant
     }
   }
 
-  @Override
-  public ShutdownManager getShutdownManagerForProver() throws UnsupportedOperationException {
-    return delegate.getShutdownManagerForProver();
-  }
-
   private class AllSatCallbackWithContext<R> implements AllSatCallback<R> {
 
     private final AllSatCallback<R> delegateCallback;
diff --git a/src/org/sosy_lab/java_smt/delegate/synchronize/SynchronizedInterpolatingProverEnvironmentWithContext.java b/src/org/sosy_lab/java_smt/delegate/synchronize/SynchronizedInterpolatingProverEnvironmentWithContext.java
@@ -12,7 +12,6 @@
 
 import java.util.Collection;
 import java.util.List;
-import org.sosy_lab.common.ShutdownManager;
 import org.sosy_lab.java_smt.api.BooleanFormula;
 import org.sosy_lab.java_smt.api.FormulaManager;
 import org.sosy_lab.java_smt.api.InterpolatingProverEnvironment;
@@ -34,11 +33,6 @@ class SynchronizedInterpolatingProverEnvironmentWithContext<T>
     delegate = checkNotNull(pDelegate);
   }
 
-  @Override
-  public ShutdownManager getShutdownManagerForProver() throws UnsupportedOperationException {
-    return delegate.getShutdownManagerForProver();
-  }
-
   @Override
   public BooleanFormula getInterpolant(Collection<T> pFormulasOfA)
       throws SolverException, InterruptedException {
diff --git 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,25 @@ public ProverEnvironment newProverEnvironment(ProverOptions... pOptions) {
     }
   }
 
+  @SuppressWarnings("resource")
+  @Override
+  public ProverEnvironment newProverEnvironment(
+      ShutdownNotifier pProverShutdownNotifier, ProverOptions... pOptions) {
+    synchronized (sync) {
+      if (useSeperateProvers) {
+        SolverContext otherContext = createOtherContext();
+        return new SynchronizedProverEnvironmentWithContext(
+            otherContext.newProverEnvironment(pProverShutdownNotifier, pOptions),
+            sync,
+            delegate.getFormulaManager(),
+            otherContext.getFormulaManager());
+      } else {
+        return new SynchronizedProverEnvironment(
+            delegate.newProverEnvironment(pProverShutdownNotifier, pOptions), delegate);
+      }
+    }
+  }
+
   @SuppressWarnings("resource")
   @Override
   public InterpolatingProverEnvironment<?> newProverEnvironmentWithInterpolation(
@@ -113,6 +132,26 @@ public InterpolatingProverEnvironment<?> newProverEnvironmentWithInterpolation(
     }
   }
 
+  @SuppressWarnings("resource")
+  @Override
+  public InterpolatingProverEnvironment<?> newProverEnvironmentWithInterpolation(
+      ShutdownNotifier pProverShutdownNotifier, ProverOptions... pOptions) {
+    synchronized (sync) {
+      if (useSeperateProvers) {
+        SolverContext otherContext = createOtherContext();
+        return new SynchronizedInterpolatingProverEnvironmentWithContext<>(
+            otherContext.newProverEnvironmentWithInterpolation(pProverShutdownNotifier, pOptions),
+            sync,
+            delegate.getFormulaManager(),
+            otherContext.getFormulaManager());
+      } else {
+        return new SynchronizedInterpolatingProverEnvironment<>(
+            delegate.newProverEnvironmentWithInterpolation(pProverShutdownNotifier, pOptions),
+            delegate);
+      }
+    }
+  }
+
   @SuppressWarnings("resource")
   @Override
   public OptimizationProverEnvironment newOptimizationProverEnvironment(ProverOptions... pOptions) {
@@ -124,6 +163,18 @@ public OptimizationProverEnvironment newOptimizationProverEnvironment(ProverOpti
     }
   }
 
+  @SuppressWarnings("resource")
+  @Override
+  public OptimizationProverEnvironment newOptimizationProverEnvironment(
+      ShutdownNotifier pProverShutdownNotifier, ProverOptions... pOptions) {
+    synchronized (sync) {
+      // seperate prover environment not available, because we can not translate arbitrary formulae.
+      // if (useSeperateProvers) { }
+      return new SynchronizedOptimizationProverEnvironment(
+          delegate.newOptimizationProverEnvironment(pProverShutdownNotifier, pOptions), delegate);
+    }
+  }
+
   @Override
   public String getVersion() {
     synchronized (sync) {
diff --git a/src/org/sosy_lab/java_smt/solvers/smtinterpol/LoggingSmtInterpolInterpolatingProver.java b/src/org/sosy_lab/java_smt/solvers/smtinterpol/LoggingSmtInterpolInterpolatingProver.java
