Enable parallel TryCloseMacro; fix progress bar for macros

key.core/src/main/java/de/uka/ilkd/key/macros/DefaultAutoMacro.java

@@ -74,7 +74,7 @@ public ProofMacroFinishedInfo applyTo(UserInterfaceControl uic, Proof proof,
             AutoProvers.create(goalChooser, proof.getInitConfig().getProfile());
 
         final ProofMacroListener pml =
-            new ProgressBarListener(goals.size(), getMaxSteps(proof), listener);
+            new ProgressBarListener(1, getMaxSteps(proof), listener);
         applyStrategy.addProverTaskObserver(pml);
 
         try {

key.core/src/main/java/de/uka/ilkd/key/macros/ProofMacro.java

@@ -245,9 +245,9 @@ public void taskStarted(TaskStartedInfo info) {
             String suffix = getMessageSuffix();
             // info.size() <= 0 means the inner prover reports an unknown workload: the
             // parallel prover commits concurrently and emits no per-step progress. Propagate
-            // it so the bar goes indeterminate ("busy") instead of a determinate one frozen
-            // at 0%. A positive inner size keeps the normal determinate bar (single-core).
-            int size = info.size() <= 0 ? 0 : numberGoals * numberSteps;
+            // -1 so the bar goes indeterminate ("busy"). A positive inner size keeps the
+            // normal determinate bar (single-core).
+            int size = info.size() <= 0 ? -1 : numberGoals * numberSteps;
             super.taskStarted(new DefaultTaskStartedInfo(TaskKind.Macro, info.message() + suffix,
                 size));
             if (size > 0) {
@@ -256,7 +256,7 @@ public void taskStarted(TaskStartedInfo info) {
         }
 
         protected String getMessageSuffix() {
-            return " [" + (completedGoals + 1) + "/" + numberGoals + "]";
+            return numberGoals <= 1 ? "" : "[" + (completedGoals + 1) + "/" + numberGoals + "]";
         }
 
         @Override

key.core/src/main/java/de/uka/ilkd/key/macros/StrategyProofMacro.java

@@ -110,7 +110,7 @@ public ProofMacroFinishedInfo applyTo(UserInterfaceControl uic, Proof proof,
         //
         // The observer to handle the progress bar
         final ProofMacroListener pml =
-            new ProgressBarListener(goals.size(), getMaxSteps(proof), listener);
+            new ProgressBarListener(1, getMaxSteps(proof), listener);
         applyStrategy.addProverTaskObserver(pml);
         // add a focus manager if there is a focus
         if (posInOcc != null) {

key.core/src/main/java/de/uka/ilkd/key/macros/TryCloseMacro.java

@@ -147,23 +147,18 @@ public ProofMacroFinishedInfo applyTo(UserInterfaceControl uic, Proof proof,
             return null;
         }
 
-        //
-        // create the rule application engine. This macro closes one goal at a time under a tight
-        // per-goal step budget (the numberSteps field, e.g. FullAutoPilotProofMacro's
-        // NUMBER_OF_TRY_STEPS default), so it is pinned to the single-threaded prover: a single
-        // goal offers no parallelism, and several workers exploring its subtree apply rules in a
-        // less step-efficient order than the single-threaded prover, which can exhaust the budget
-        // before the goal closes (leaving a closable goal pruned). Wide, generously-budgeted runs
-        // keep using the multi-core prover.
+        // create the rule application engine
         final Profile profile = proof.getServices().getProfile();
         final ProverCore<Proof, Goal> applyStrategy = AutoProvers.create(
-            profile.<Proof, Goal>getSelectedGoalChooserBuilder().create(), profile, false);
+            profile.<Proof, Goal>getSelectedGoalChooserBuilder().create(), profile);
         // assert: all goals have the same proof
 
-        //
+        int maxSteps = numberSteps > 0 ? numberSteps
+                : proof.getSettings().getStrategySettings().getMaxSteps();
+
         // The observer to handle the progress bar
         final TryCloseProgressBarListener pml =
-            new TryCloseProgressBarListener(goals.size(), numberSteps, listener);
+            new TryCloseProgressBarListener(goals.size(), maxSteps, listener);
         final ImmutableList<Goal> ignoredOpenGoals = setDifference(proof.openGoals(), goals);
         applyStrategy.addProverTaskObserver(pml);
 
@@ -177,10 +172,8 @@ public ProofMacroFinishedInfo applyTo(UserInterfaceControl uic, Proof proof,
         try {
             for (final Goal goal : goals) {
                 Node node = goal.node();
-                int maxSteps = numberSteps > 0 ? numberSteps
-                        : proof.getSettings().getStrategySettings().getMaxSteps();
                 final ProofSearchInformation<Proof, Goal> result = applyStrategy.start(proof,
-                    ImmutableList.<Goal>nil().prepend(goal), maxSteps, -1, false);
+                    ImmutableList.singleton(goal), maxSteps, -1, false);
                 // final Goal closedGoal;
 
                 // retreat if not closed

key.core/src/main/java/de/uka/ilkd/key/pp/LogicPrinter.java

@@ -90,6 +90,9 @@ public class LogicPrinter {
     private QuantifiableVariablePrintMode quantifiableVariablePrintMode =
         QuantifiableVariablePrintMode.NORMAL;
 
+    // Stop printing after maxChar characters; -1 prints whole term independent of size
+    private int maxChar = -1;
+
     private enum QuantifiableVariablePrintMode {
         NORMAL, WITH_OUT_DECLARATION
     }
@@ -157,6 +160,37 @@ public static String quickPrintTerm(JTerm t, Services services) {
             NotationInfo.DEFAULT_UNICODE_ENABLED, NotationInfo.DEFAULT_HIDE_PACKAGE_PREFIX);
     }
 
+
+    /**
+     * converts a term to a String
+     *
+     * @param t a term.
+     * @param maxChar number of characters to be printed (-1 = unlimited
+     * @param services the Services class with information about the logic
+     * @return the printed semisequent.
+     */
+    public static String quickPrintTerm(JTerm t, int maxChar, Services services) {
+        LogicPrinter p = quickPrinter(services, NotationInfo.DEFAULT_PRETTY_SYNTAX,
+            NotationInfo.DEFAULT_UNICODE_ENABLED,
+            NotationInfo.DEFAULT_HIDE_PACKAGE_PREFIX);
+        p.setMaxChar(maxChar);
+        p.layouter().beginC();
+        p.printTerm(t);
+        p.layouter().end();
+        final String result = p.result();
+        return result + (result.length() >= maxChar ? "..." : "");
+    }
+
+    /**
+     * sets the maximal number of characters to be printed
+     *
+     * @param maxChar number of characters to be printed (-1 = unlimited)
+     */
+    public void setMaxChar(int maxChar) {
+        this.maxChar = maxChar;
+    }
+
+
     /**
      * Converts a term to a string.
      *
@@ -821,7 +855,9 @@ public void printTerm(JTerm t) {
             if (parens) {
                 layouter.print("(");
             }
-            notation.print(t, this);
+            if (maxChar == -1 || layouter.backend().count() < maxChar) {
+                notation.print(t, this);
+            }
             if (parens) {
                 layouter.print(")");
             }

key.core/src/main/java/de/uka/ilkd/key/prover/impl/AutoProvers.java

@@ -44,16 +44,6 @@ public static ProverCore<Proof, Goal> create(GoalChooser<Proof, Goal> goalChoose
      * Creates the auto-prover selected by the current configuration, optionally forcing the
      * single-threaded prover.
      *
-     * <p>
-     * {@code allowParallel == false} pins the run to {@link ApplyStrategy} even when the multi-core
-     * prover is enabled. This is for drivers that close one goal at a time under a tight per-goal
-     * step budget (notably {@link de.uka.ilkd.key.macros.TryCloseMacro}): there is no parallelism
-     * to
-     * gain from a single goal, and several workers exploring one goal's subtree apply rules in a
-     * different, less step-efficient order than the single-threaded prover -- which can exhaust the
-     * budget before the goal closes. The wide, generously-budgeted runs (interactive automode and
-     * most macros) keep using the parallel prover, where it pays off.
-     *
      * @param goalChooser the goal chooser to use
      * @param profile the profile of the proof to be processed
      * @param allowParallel whether the parallel prover may be used at all for this run

key.core/src/main/java/de/uka/ilkd/key/prover/impl/ParallelProver.java

@@ -305,11 +305,11 @@ public synchronized ApplyStrategyInfo<Proof, Goal> start(Proof proof, ImmutableL
         this.nonCloseableGoal = null;
         this.firstError.set(null);
 
-        // size 0 -> the status line shows an indeterminate ("busy") bar: the parallel prover does
-        // not report a meaningful per-step progress value (workers commit concurrently), so a
-        // determinate bar would either sit at zero or need thread-unsafe cross-worker counting.
+        // the status line shows an indeterminate ("busy") bar (<code>size == -1</code>):
+        // the parallel prover does not report a meaningful per-step progress value (workers
+        // commit concurrently)
         fireTaskStarted(new DefaultTaskStartedInfo(TaskStartedInfo.TaskKind.Strategy,
-            PROCESSING_STRATEGY, 0));
+            PROCESSING_STRATEGY, -1));
 
         ApplyStrategyInfo<Proof, Goal> result = runParallel(goals);
 

key.core/src/test/java/de/uka/ilkd/key/prover/mt/MtMacroStressTest.java

@@ -33,10 +33,7 @@
  * The first scenario guards pruning a subtree that was <em>produced by many workers</em>: a
  * parallel run is stopped by a tiny step budget, the resulting partial subtree is pruned back to
  * the root, and a second parallel run must then close the proof &mdash; a corrupted tree from the
- * prune would show up as an inconsistent goal set, a failure to close, or an exception. (This was
- * formerly phrased via {@link de.uka.ilkd.key.macros.TryCloseMacro}, but that macro deliberately
- * pins itself to the single-threaded prover &mdash; see {@code AutoProvers.create} &mdash; so the
- * prune-after-parallel-exploration scenario is exercised directly here.)
+ * prune would show up as an inconsistent goal set, a failure to close, or an exception.
  *
  * <p>
  * The second scenario runs {@link FinishSymbolicExecutionMacro} on the parallel prover: its filter
@@ -86,7 +83,7 @@ static void restoreSettings() {
      * Each repetition: run the parallel prover with a tiny step budget at a high worker count
      * (produces a partial, many-worker-built subtree), prune that subtree back to the root, assert
      * the goal set is consistent, then run the parallel prover to completion and assert the proof
-     * closes -- proving the prune left a consistent, completable tree.
+     * closes, which proves that the prune left a consistent, completable tree.
      */
     @Test
     void pruneOfParallelSubtreeStaysSafeUnderManyWorkers() throws Exception {

key.ui/src/main/java/de/uka/ilkd/key/gui/GoalList.java

@@ -229,12 +229,15 @@ public boolean contains(Name name) {
                         }
                     }); // do not print term labels
             try {
+                sp.setMaxChar(MAX_DISPLAYED_SEQUENT_LENGTH);
                 sp.printSequent(seq);
                 // Only read the result once printing has completed: result() returns the raw
                 // backend buffer without flushing, so on a failed print it would yield a
                 // truncated/empty sequent. Read it here on the success path instead.
                 res = sp.result().replace('\n', ' ');
-                res = res.substring(0, Math.min(MAX_DISPLAYED_SEQUENT_LENGTH, res.length()));
+                if (res.length() > MAX_DISPLAYED_SEQUENT_LENGTH) {
+                    res = res.substring(0, MAX_DISPLAYED_SEQUENT_LENGTH) + "...";
+                }
             } catch (Exception ex) {
                 LOGGER.warn("GoalList: Problem printing sequent.", ex);
                 res = "<unable to print sequent>";

key.ui/src/main/java/de/uka/ilkd/key/gui/MainStatusLine.java

@@ -78,17 +78,22 @@ public void reset() {
 
     /**
      * Set the range of values the progress bar can display (see <code>setMaximum</code> of
-     * <code>ProgressBar</code>). A non-positive maximum means "unknown workload" -- the parallel
-     * prover reports no per-step progress -- and switches the bar to indeterminate ("busy") mode so
+     * <code>ProgressBar</code>). A negative <code>value</code> means
+     * "unknown workload", e.g. the parallel prover reports
+     * no per-step progress and switches the bar to indeterminate ("busy") mode so
      * it animates instead of sitting frozen at zero.
+     * The <code>value</code> 0 means no bar and positive number describes the maximum workload.
      */
     public void setProgressBarMaximum(int value) {
-        if (value <= 0) {
+        if (value < 0) {
             progressBar.setIndeterminate(true);
+        } else if (value == 0) {
+            progressBar.setIndeterminate(false);
         } else {
             progressBar.setIndeterminate(false);
             progressBar.setMaximum(value);
         }
+        progressBar.setEnabled(value != 0);
     }
 
     /**

key.ui/src/main/java/de/uka/ilkd/key/gui/MainWindow.java

@@ -899,14 +899,14 @@ public void hideStatusProgress() {
 
     private void setStatusLineImmediately(String str, int max) {
         statusLine.setStatusText(str);
-        // A non-positive maximum means "unknown workload" -- the parallel prover (whose workers
-        // commit concurrently) and symbolic-execution stop conditions report no per-step progress.
+        // A negative maximum means "unknown workload", e.g. the parallel prover (whose workers
+        // commit concurrently).
         // Show the progress panel and let setProgressBarMaximum switch the bar to indeterminate
         // ("busy") mode so it animates, instead of hiding it and sitting frozen. A positive maximum
         // drives the normal determinate bar. (The panel is hidden again at task end via reset() /
-        // hideStatusProgress().)
+        // hideStatusProgress().) A maximum of 0 hides the bar
         getStatusLine().setProgressBarMaximum(max);
-        statusLine.setProgressPanelVisible(true);
+        statusLine.setProgressPanelVisible(max != 0);
         statusLine.validate();
         statusLine.paintImmediately(0, 0, statusLine.getWidth(), statusLine.getHeight());
     }

key.ui/src/main/java/de/uka/ilkd/key/gui/WindowUserInterfaceControl.java

@@ -264,8 +264,6 @@ private void taskFinishedInternal(TaskFinishedInfo info) {
                 mainWindow.displayResults(info.toString());
             }
         }
-        // this seems to be a good place to free some memory
-        Runtime.getRuntime().gc();
     }
 
     /**

key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/ProofTreePopupFactory.java

@@ -488,9 +488,8 @@ public void eventCutting() {
 
                     @Override
                     public void eventException(Throwable throwable) {
-                        // Clear the "Cutting..." status and its indeterminate ("busy") progress
-                        // bar; the success path does this in eventEnd, and without it the bar
-                        // keeps animating forever after a failed cut.
+                        // Clear the "Cutting..." status text; the success path does
+                        // this in eventEnd
                         mediator.getUI().resetStatus(this);
                         mediator.startInterface(true);