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/java/expression/operator/DLEmbeddedExpression.java

@@ -82,7 +82,6 @@ public void visit(Visitor v) {
     }
 
     public void check(Services javaServ, KeYJavaType containingClass) throws ConvertException {
-
         if (functionSymbol == null) {
             throw new ConvertException("null function symbol");
         }
@@ -106,7 +105,9 @@ public void check(Services javaServ, KeYJavaType containingClass) throws Convert
         String qualifier =
             name.lastIndexOf('.') != -1 ? name.substring(0, name.lastIndexOf('.')) : "";
         name = name.substring(name.lastIndexOf('.') + 1);
-        TypeRef tr = new TypeRef(new ProgramElementName(name, qualifier), 0, null, containingClass);
+        ProgramElementName peName = qualifier.isEmpty() ? new ProgramElementName(name)
+                : new ProgramElementName(name, qualifier);
+        TypeRef tr = new TypeRef(peName, 0, null, containingClass);
         ExecutionContext ec = new ExecutionContext(tr, null, null);
 
         for (int i = 0; i < actual; i++) {
@@ -115,7 +116,6 @@ public void check(Services javaServ, KeYJavaType containingClass) throws Convert
 
             Expression child = children.get(i);
 
-
             KeYJavaType kjtActual = javaServ.getTypeConverter().getKeYJavaType(child, ec);
 
             if (kjtExpected != null && !kjtActual.getSort().extendsTrans(kjtExpected.getSort())) {

key.core/src/main/java/de/uka/ilkd/key/ldt/JavaDLTheory.java

@@ -151,51 +151,43 @@ public final SortDependingFunction getExactInstanceofSymbol(Sort sort, TermServi
     @Override
     public boolean isResponsible(Operator op, JTerm[] subs, Services services,
             ExecutionContext ec) {
-        assert false;
         return false;
     }
 
     @Override
     public boolean isResponsible(Operator op, JTerm left, JTerm right, Services services,
             ExecutionContext ec) {
-        assert false;
         return false;
     }
 
     @Override
     public boolean isResponsible(Operator op, JTerm sub, TermServices services,
             ExecutionContext ec) {
-        assert false;
         return false;
     }
 
     @Override
     public JTerm translateLiteral(Literal lit, Services services) {
-        assert false;
         return null;
     }
 
     @Override
     public Function getFunctionFor(Operator op, Services services, ExecutionContext ec) {
-        assert false;
         return null;
     }
 
     @Override
     public boolean hasLiteralFunction(Function f) {
-        assert false;
         return false;
     }
 
     @Override
     public Expression translateTerm(JTerm t, ExtList children, Services services) {
-        assert false;
         return null;
     }
 
     @Override
     public Type getType(JTerm t) {
-        assert false;
         return null;
     }
 }

key.core/src/main/java/de/uka/ilkd/key/logic/ProgramElementName.java

@@ -70,7 +70,7 @@ public ProgramElementName(String name, NameCreationInfo creationInfo, Comment[]
 
     public ProgramElementName(String n, String q) {
         super(q + "::" + n);
-        assert !q.isEmpty() : "Tried to create qualified name with missing qualifier";
+        assert !q.isEmpty() : "Tried to create qualified name with missing qualifier: " + n;
 
         this.qualifierString = q.intern();
         this.shortName = n.intern();

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/IntermediateProofReplayer.java

@@ -406,8 +406,7 @@ public Result replay(ProblemInitializer.ProblemInitializerListener listener,
      */
     private void addChildren(Iterator<Node> children, LinkedList<NodeIntermediate> intermChildren) {
         int i = 0;
-        while (!currGoal.node().isClosed() && children.hasNext() && intermChildren.size() > 0) {
-
+        while (!currGoal.node().isClosed() && children.hasNext() && !intermChildren.isEmpty()) {
             // NOTE: In the case of an unfinished proof, there
             // is another node after the last application which
             // is not represented by an intermediate

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

@@ -80,7 +80,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.
@@ -110,6 +111,7 @@ public OutputStreamProofSaver(Proof proof, String internalVersion) {
         this.proof = proof;
         this.internalVersion = internalVersion;
         this.saveProofSteps = true;
+        this.expandOneStepSimplifier = true;
     }
 
     /**
@@ -119,10 +121,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;
     }
 
     /**
@@ -328,13 +332,31 @@ 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 {
+        /*
+         * An OSS rule application may contain rule applications on top-level formulas that get
+         * deleted when expanding the OSS steps. In that case, the rule after the OSS must also be
+         * deleted, as the formula to be removed was never added in the first place.
+         */
+        String tacletName = appliedRuleApp.taclet().name().toString();
         output.append(prefix);
         output.append("(rule \"");
-        output.append(appliedRuleApp.rule().name().toString());
+        output.append(tacletName);
         output.append("\"");
         output.append(posInOccurrence2Proof(node.sequent(), appliedRuleApp.posInOccurrence()));
         output.append(newNames2Proof(node));
@@ -346,6 +368,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");
     }
@@ -528,7 +553,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()));
@@ -592,11 +617,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();
+        int seqFNum = node.sequent().formulaNumberInSequent(ossa.posInOccurrence());
+        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());
+            }
+            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.
      *
@@ -606,7 +657,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;
 
@@ -695,8 +745,9 @@ public static String posInOccurrence2Proof(Sequent seq,
         if (pos == null) {
             return "";
         }
+        int inSequent = seq.formulaNumberInSequent(pos.isInAntec(), pos.sequentFormula());
         return " (formula \""
-            + seq.formulaNumberInSequent(pos.isInAntec(), pos.sequentFormula())
+            + inSequent
             + "\")" + posInTerm2Proof(pos.posInTerm());
     }
 
@@ -763,7 +814,6 @@ public String assumesFormulaInsts(Node node,
                                     sequentFormula))
                         .append("\")");
             } else if (assumesFormulaInstantiation instanceof AssumesFormulaInstDirect) {
-
                 final String directInstantiation =
                     printTerm((JTerm) sequentFormula.formula(), node.proof().getServices());
 

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;
     }