Expand OSS steps when saving a proof for more deterministic Proofs

key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/TruthValueTracingUtil.java

@@ -261,7 +261,7 @@ private static void evaluateNode(
                 }
             } else if (parent.getAppliedRuleApp() instanceof OneStepSimplifierRuleApp app) {
                 PosInOccurrence parentPio = null;
-                for (RuleApp protocolApp : app.getProtocol()) {
+                for (var protocolApp : app.getProtocol()) {
                     if (parentPio != null) {
                         updatePredicateResultBasedOnNewMinorIdsOSS(protocolApp.posInOccurrence(),
                             parentPio, termLabelName, services.getTermBuilder(), nodeResult);

key.core/src/main/java/de/uka/ilkd/key/proof/io/IProofFileParser.java

@@ -34,7 +34,7 @@ enum ProofElementID {
         USER_INTERACTION("userinteraction"), PROOF_SCRIPT("proofscript"), NEW_NAMES("newnames"),
         AUTOMODE_TIME("autoModeTime"), KeY_LOG("keyLog"), KeY_USER("keyUser"),
         KeY_VERSION("keyVersion"), KeY_SETTINGS("keySettings"), OPEN_GOAL("opengoal"),
-        NOTES("notes"), SOLVERTYPE("solverType"), MODALITY("modality");
+        NOTES("notes"), SOLVERTYPE("solverType"), MODALITY("modality"), OSS_STEP("ossStep");
 
         private final String rawName;
 

key.core/src/main/java/de/uka/ilkd/key/proof/io/OutputStreamProofSaver.java

@@ -82,7 +82,8 @@ public class OutputStreamProofSaver {
      * Whether the proof steps should be output (usually true).
      */
     protected final boolean saveProofSteps;
-
+    /// Whether steps by the [OneStepSimplifier] should be expanded.
+    protected final boolean expandOneStepSimplifier;
 
     /**
      * Extracts java source directory from {@link Proof#header()}, if it exists.
@@ -97,7 +98,7 @@ public static File getJavaSourceLocation(Proof proof) {
             final int begin = header.indexOf('\"', i);
             final int end = header.indexOf('\"', begin + 1);
             final String sourceLocation = header.substring(begin + 1, end);
-            if (sourceLocation.length() > 0) {
+            if (!sourceLocation.isEmpty()) {
                 return new File(sourceLocation);
             }
         }
@@ -112,6 +113,7 @@ public OutputStreamProofSaver(Proof proof, String internalVersion) {
         this.proof = proof;
         this.internalVersion = internalVersion;
         this.saveProofSteps = true;
+        this.expandOneStepSimplifier = true;
     }
 
     /**
@@ -121,10 +123,12 @@ public OutputStreamProofSaver(Proof proof, String internalVersion) {
      * @param internalVersion currently running KeY version
      * @param saveProofSteps whether to save the performed proof steps
      */
-    public OutputStreamProofSaver(Proof proof, String internalVersion, boolean saveProofSteps) {
+    public OutputStreamProofSaver(Proof proof, String internalVersion, boolean saveProofSteps,
+            boolean expandOneStepSimplifier) {
         this.proof = proof;
         this.internalVersion = internalVersion;
         this.saveProofSteps = saveProofSteps;
+        this.expandOneStepSimplifier = expandOneStepSimplifier;
     }
 
     /**
@@ -346,10 +350,22 @@ private String newNames2Proof(Node n) {
      * @param output the writer in which the rule is printed
      * @throws IOException an exception thrown when printing fails
      */
-
     private void printSingleTacletApp(TacletApp appliedRuleApp, Node node, String prefix,
             Appendable output) throws IOException {
+        printSingleTacletApp(appliedRuleApp, node, prefix, output, false);
+    }
 
+    /**
+     * Print applied taclet rule for a single taclet rule application into the passed writer.
+     *
+     * @param appliedRuleApp the rule application to be printed
+     * @param prefix a string which the printed rule is concatenated to
+     * @param output the writer in which the rule is printed
+     * @param isOSSStep whether this node is an expanded OSS rule app step
+     * @throws IOException an exception thrown when printing fails
+     */
+    private void printSingleTacletApp(TacletApp appliedRuleApp, Node node, String prefix,
+            Appendable output, boolean isOSSStep) throws IOException {
         output.append(prefix);
         output.append("(rule \"");
         output.append(appliedRuleApp.rule().name().toString());
@@ -364,6 +380,9 @@ private void printSingleTacletApp(TacletApp appliedRuleApp, Node node, String pr
         }
         output.append("");
         userInteraction2Proof(node, output);
+        if (isOSSStep) {
+            output.append(" (ossStep)");
+        }
         notes2Proof(node, output);
         output.append(")\n");
     }
@@ -546,7 +565,7 @@ private void printRuleJustification(IBuiltInRuleApp appliedRuleApp, Appendable o
     private void printSingleBuiltInRuleApp(IBuiltInRuleApp appliedRuleApp, Node node, String prefix,
             Appendable output) throws IOException {
         output.append(prefix);
-        output.append(" (builtin \"");
+        output.append("(builtin \"");
         output.append(appliedRuleApp.rule().name().toString());
         output.append("\"");
         output.append(posInOccurrence2Proof(node.sequent(), appliedRuleApp.posInOccurrence()));
@@ -610,11 +629,37 @@ private void printSingleNode(Node node, String prefix, Appendable output) throws
 
         if (appliedRuleApp instanceof TacletApp) {
             printSingleTacletApp((TacletApp) appliedRuleApp, node, prefix, output);
+        } else if (expandOneStepSimplifier
+                && appliedRuleApp instanceof OneStepSimplifierRuleApp ossa) {
+            printExpandedOneStepSimplifierRuleApp(ossa, node, prefix, output);
         } else if (appliedRuleApp instanceof IBuiltInRuleApp) {
             printSingleBuiltInRuleApp((IBuiltInRuleApp) appliedRuleApp, node, prefix, output);
         }
     }
 
+    private void printExpandedOneStepSimplifierRuleApp(OneStepSimplifierRuleApp ossa, Node node,
+            String prefix, Appendable output) throws IOException {
+        OneStepSimplifier.Protocol protocol = ossa.getProtocol();
+        for (int i = 0; i < protocol.size(); i++) {
+            var app = protocol.get(i);
+            Node n = new Node(node.proof());
+            if (i == 0) {
+                n.setNameRecorder(node.getNameRecorder());
+            }
+            int seqFNum = node.sequent().formulaNumberInSequent(ossa.posInOccurrence());
+            Sequent seq = node.sequent()
+                    .replaceFormula(seqFNum, app.posInOccurrence().sequentFormula()).sequent();
+            n.setSequent(seq);
+            if (app instanceof TacletApp ta) {
+                printSingleTacletApp(ta, n, prefix, output, true);
+            } else if (app instanceof IBuiltInRuleApp ba) {
+                // This case does not currently happen, but just in case any built-ins get added to
+                // the OSS...
+                printSingleBuiltInRuleApp(ba, n, prefix, output);
+            }
+        }
+    }
+
     /**
      * Print applied rule(s) for a proof node and its decendants into the passed writer.
      *
@@ -624,7 +669,6 @@ private void printSingleNode(Node node, String prefix, Appendable output) throws
      * @throws IOException an exception thrown when printing fails
      */
     private void collectProof(Node node, String prefix, Appendable output) throws IOException {
-
         printSingleNode(node, prefix, output);
         Iterator<Node> childrenIt;
 

key.core/src/main/java/de/uka/ilkd/key/proof/io/ProofSaver.java

@@ -50,7 +50,7 @@ public static void saveToFile(Path file, Proof proof) throws IOException {
      * @throws IOException on any I/O error
      */
     public static void saveProofObligationToFile(Path file, Proof proof) throws IOException {
-        ProofSaver saver = new ProofSaver(proof, file, false);
+        ProofSaver saver = new ProofSaver(proof, file, false, false);
         saver.save();
     }
 
@@ -88,9 +88,12 @@ public ProofSaver(Proof proof, Path file, String internalVersion) {
      * @param proof proof to save
      * @param file file to save proof into
      * @param saveProofSteps whether to save proof steps (false -> only proof obligation)
+     * @param expandOneStepSimplifier whether to expand
+     *        {@link de.uka.ilkd.key.rule.OneStepSimplifier} rule apps
      */
-    public ProofSaver(Proof proof, Path file, boolean saveProofSteps) {
-        this(proof, file, KeYConstants.INTERNAL_VERSION, saveProofSteps);
+    public ProofSaver(Proof proof, Path file, boolean saveProofSteps,
+            boolean expandOneStepSimplifier) {
+        this(proof, file, KeYConstants.INTERNAL_VERSION, saveProofSteps, expandOneStepSimplifier);
     }
 
     /**
@@ -100,9 +103,12 @@ public ProofSaver(Proof proof, Path file, boolean saveProofSteps) {
      * @param file file to save proof into
      * @param internalVersion version of KeY to add to the proof log
      * @param saveProofSteps whether to save proof steps (false -> only proof obligation)
+     * @param expandOneStepSimplifier whether to expand
+     *        {@link de.uka.ilkd.key.rule.OneStepSimplifier} rule apps
      */
-    public ProofSaver(Proof proof, Path file, String internalVersion, boolean saveProofSteps) {
-        super(proof, internalVersion, saveProofSteps);
+    public ProofSaver(Proof proof, Path file, String internalVersion, boolean saveProofSteps,
+            boolean expandOneStepSimplifier) {
+        super(proof, internalVersion, saveProofSteps, expandOneStepSimplifier);
         this.file = file;
     }
 

key.core/src/main/java/de/uka/ilkd/key/rule/OneStepSimplifier.java

@@ -419,7 +419,7 @@ private RuleApp makeReplaceKnownTacletApp(JTerm formula,
 
         SVInstantiations svi = SVInstantiations.EMPTY_SVINSTANTIATIONS;
         FormulaSV sv = SchemaVariableFactory.createFormulaSV(new Name("b"));
-        svi.add(sv, (JTerm) pio.sequentFormula().formula(), lastProof.getServices());
+        svi.add(sv, pio.sequentFormula().formula(), lastProof.getServices());
 
         PosInOccurrence applicatinPIO =
             new PosInOccurrence(new SequentFormula(formula), PosInTerm.getTopLevel(), // TODO: This
@@ -431,9 +431,8 @@ private RuleApp makeReplaceKnownTacletApp(JTerm formula,
                                // renamings and term labels
         ImmutableList<AssumesFormulaInstantiation> ifInst = ImmutableSLList.nil();
         ifInst = ifInst.append(new AssumesFormulaInstDirect(pio.sequentFormula()));
-        TacletApp ta = PosTacletApp.createPosTacletApp(taclet, svi, ifInst, applicatinPIO,
+        return PosTacletApp.createPosTacletApp(taclet, svi, ifInst, applicatinPIO,
             lastProof.getServices());
-        return ta;
     }
 
     /**