Make ParallelAlgorithm generate nested algorithms from the threads th…

…at they run in

At least MathSAT5 does not like to be accessed from a thread that is different
from the thread it was created in
(see https://github.com/sosy-lab/java-smt/issues/339\). To work around this,
move the generation of nested algorithms into the individual threads that they run in.

Before this commit, the initialization of the algorithms nested in ParallelAlgorithm
was done sequentially at the construction of ParallelAlgorithm.
With this commit, this initialization moves to the run of ParallelAlgorithm,
and happens concurrently for the nested algorithms.

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/branches/svcomp24-parallel-portfolio-approach@45076 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c

src/org/sosy_lab/cpachecker/core/algorithm/ParallelAlgorithm.java

@@ -273,28 +273,29 @@ private Callable<ParallelAnalysisResult> createParallelAnalysis(
     final ResourceLimitChecker singleAnalysisOverallLimit =
         ResourceLimitChecker.fromConfiguration(singleConfig, singleLogger, singleShutdownManager);
 
-    final CoreComponentsFactory coreComponents =
-        new CoreComponentsFactory(
-            singleConfig,
-            singleLogger,
-            singleShutdownManager.getNotifier(),
-            aggregatedReachedSetManager.asView());
-
-    final ConfigurableProgramAnalysis cpa = coreComponents.createCPA(cfa, specification);
-    final Algorithm algorithm = coreComponents.createAlgorithm(cpa, cfa, specification);
-    final ReachedSet reached = coreComponents.createReachedSet(cpa);
-
-    AtomicBoolean terminated = new AtomicBoolean(false);
-    StatisticsEntry statisticsEntry =
-        stats.getNewSubStatistics(
-            reached,
-            singleConfigFileName.toString(),
-            Iterables.getOnlyElement(
-                FluentIterable.from(singleAnalysisOverallLimit.getResourceLimits())
-                    .filter(ThreadCpuTimeLimit.class),
-                null),
-            terminated);
     return () -> {
+      final CoreComponentsFactory coreComponents =
+          new CoreComponentsFactory(
+              singleConfig,
+              singleLogger,
+              singleShutdownManager.getNotifier(),
+              aggregatedReachedSetManager.asView());
+
+      final ConfigurableProgramAnalysis cpa = coreComponents.createCPA(cfa, specification);
+      final Algorithm algorithm = coreComponents.createAlgorithm(cpa, cfa, specification);
+      final ReachedSet reached = coreComponents.createReachedSet(cpa);
+
+      AtomicBoolean terminated = new AtomicBoolean(false);
+      StatisticsEntry statisticsEntry =
+          stats.getNewSubStatistics(
+              reached,
+              singleConfigFileName.toString(),
+              Iterables.getOnlyElement(
+                  FluentIterable.from(singleAnalysisOverallLimit.getResourceLimits())
+                      .filter(ThreadCpuTimeLimit.class),
+                  null),
+              terminated);
+
       if (algorithm instanceof ConditionAdjustmentEventSubscriber) {
         conditionAdjustmentEventSubscribers.add((ConditionAdjustmentEventSubscriber) algorithm);
       }