From 5804b34b42a47c6d188ce9763313c1156605cc70 Mon Sep 17 00:00:00 2001 From: Arne Keller Date: Wed, 27 Sep 2023 18:45:27 +0200 Subject: [PATCH 01/14] SMT: add Z3_QF variant --- .../uka/ilkd/key/smt/solvertypes/Z3_QF.props | 22 +++++++++++++++++++ 1 file changed, 22 insertions(+) create mode 100644 key.core/src/main/resources/de/uka/ilkd/key/smt/solvertypes/Z3_QF.props diff --git a/key.core/src/main/resources/de/uka/ilkd/key/smt/solvertypes/Z3_QF.props b/key.core/src/main/resources/de/uka/ilkd/key/smt/solvertypes/Z3_QF.props new file mode 100644 index 00000000000..0a678f1fee1 --- /dev/null +++ b/key.core/src/main/resources/de/uka/ilkd/key/smt/solvertypes/Z3_QF.props @@ -0,0 +1,22 @@ +params=-in -smt2 +timeout=-1 +name=Z3_QF +info=Z3 solver by Microsoft. Translation excludes quantifiers, making this variant much faster for certain problems. +command=z3 +version=--version +minVersion=Z3 version 4.4.1 +handlers=de.uka.ilkd.key.smt.newsmt2.BooleanConnectiveHandler,\ +de.uka.ilkd.key.smt.newsmt2.PolymorphicHandler,\ +de.uka.ilkd.key.smt.newsmt2.LogicalVariableHandler,\ +de.uka.ilkd.key.smt.newsmt2.NumberConstantsHandler,\ +de.uka.ilkd.key.smt.newsmt2.IntegerOpHandler,\ +de.uka.ilkd.key.smt.newsmt2.InstanceOfHandler,\ +de.uka.ilkd.key.smt.newsmt2.CastHandler,\ +de.uka.ilkd.key.smt.newsmt2.SumProdHandler,\ +de.uka.ilkd.key.smt.newsmt2.UpdateHandler,\ +de.uka.ilkd.key.smt.newsmt2.FieldConstantHandler,\ +de.uka.ilkd.key.smt.newsmt2.FloatHandler,\ +de.uka.ilkd.key.smt.newsmt2.CastingFunctionsHandler,\ +de.uka.ilkd.key.smt.newsmt2.DefinedSymbolsHandler,\ +de.uka.ilkd.key.smt.newsmt2.UninterpretedSymbolsHandler +handlerOptions=getUnsatCore \ No newline at end of file From c4e5b16831442addc111fa54d4fa9047b014f1c2 Mon Sep 17 00:00:00 2001 From: Arne Keller Date: Wed, 27 Sep 2023 18:45:42 +0200 Subject: [PATCH 02/14] gradle: specify inputs and outputs of tasks This way the solvers.txt will automatically be regenerated. --- key.core/build.gradle | 24 +++++++++++++++--------- 1 file changed, 15 insertions(+), 9 deletions(-) diff --git a/key.core/build.gradle b/key.core/build.gradle index 0a006775166..dbaf7281e9c 100644 --- a/key.core/build.gradle +++ b/key.core/build.gradle @@ -71,6 +71,10 @@ task generateSMTListings { def resourcesDir = "${project.projectDir}/src/main/resources" def outputDir = resourcesDir // in the future that should be "${project.buildDir}/resources/main" // ${project.buildDir} + inputs.files fileTree("$resourcesDir/$pack", { + exclude "$resourcesDir/$pack/DefinedSymbolsHandler.preamble.xml" + }) + outputs.files file("$outputDir/$pack/DefinedSymbolsHandler.preamble.xml") doLast { new File("$outputDir/$pack/DefinedSymbolsHandler.preamble.xml").withWriter { list -> list.writeLine '' @@ -92,6 +96,10 @@ task generateSolverPropsList { def resourcesDir = "${project.projectDir}/src/main/resources" def outputDir = resourcesDir // in the future that should be "${project.buildDir}/resources/main" // ${project.buildDir} + inputs.files fileTree("$outputDir/$pack/", { + exclude "./solvers.txt" + }) + outputs.files file("$outputDir/$pack/solvers.txt") doLast { def list = [] def dir = new File("$outputDir/$pack/") @@ -101,14 +109,12 @@ task generateSolverPropsList { } }) list.sort() - if (!file("$outputDir/$pack/solvers.txt").exists()) { - String files = '' - for (String propsFile : list) { - files += propsFile + System.lineSeparator() - } - new File("$outputDir/$pack/solvers.txt").withWriter { listSolvers -> - listSolvers.write files - } + String files = '' + for (String propsFile : list) { + files += propsFile + System.lineSeparator() + } + new File("$outputDir/$pack/solvers.txt").withWriter { listSolvers -> + listSolvers.write files } } } @@ -196,7 +202,7 @@ static def gitRevParse(String args) { } // @AW: Say something here. From POV this explain by itself. -processResources.dependsOn generateVersionFiles +processResources.dependsOn generateVersionFiles, generateSolverPropsList, generateSMTListings def antlr4OutputKey = "$projectDir/build/generated-src/antlr4/main/de/uka/ilkd/key/nparser" task runAntlr4Key(type: JavaExec) { From 601482a2ee1ca223143029fd3feb1269463d3840 Mon Sep 17 00:00:00 2001 From: Arne Keller Date: Fri, 13 Oct 2023 10:13:12 +0200 Subject: [PATCH 03/14] SMT: tweak Z3_QF description wording --- .../resources/de/uka/ilkd/key/smt/solvertypes/Z3_QF.props | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/key.core/src/main/resources/de/uka/ilkd/key/smt/solvertypes/Z3_QF.props b/key.core/src/main/resources/de/uka/ilkd/key/smt/solvertypes/Z3_QF.props index 0a678f1fee1..1a6a8874eda 100644 --- a/key.core/src/main/resources/de/uka/ilkd/key/smt/solvertypes/Z3_QF.props +++ b/key.core/src/main/resources/de/uka/ilkd/key/smt/solvertypes/Z3_QF.props @@ -1,7 +1,7 @@ params=-in -smt2 timeout=-1 name=Z3_QF -info=Z3 solver by Microsoft. Translation excludes quantifiers, making this variant much faster for certain problems. +info=Z3 solver by Microsoft. SMT translation of the sequent excludes quantified terms, making this variant much faster for certain problems. command=z3 version=--version minVersion=Z3 version 4.4.1 @@ -19,4 +19,4 @@ de.uka.ilkd.key.smt.newsmt2.FloatHandler,\ de.uka.ilkd.key.smt.newsmt2.CastingFunctionsHandler,\ de.uka.ilkd.key.smt.newsmt2.DefinedSymbolsHandler,\ de.uka.ilkd.key.smt.newsmt2.UninterpretedSymbolsHandler -handlerOptions=getUnsatCore \ No newline at end of file +handlerOptions=getUnsatCore From 37cea992701f60121c18bf9388a91c26a267baf1 Mon Sep 17 00:00:00 2001 From: Richard Bubel Date: Thu, 19 Oct 2023 16:32:32 +0200 Subject: [PATCH 04/14] Fix issue #3186: Preserve nullable/non_null modifiers on paramters of model methods --- .../key/speclang/jml/pretranslation/TextualJMLMethodDecl.java | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/key.core/src/main/java/de/uka/ilkd/key/speclang/jml/pretranslation/TextualJMLMethodDecl.java b/key.core/src/main/java/de/uka/ilkd/key/speclang/jml/pretranslation/TextualJMLMethodDecl.java index 08bbcc87615..4dc43db5789 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/speclang/jml/pretranslation/TextualJMLMethodDecl.java +++ b/key.core/src/main/java/de/uka/ilkd/key/speclang/jml/pretranslation/TextualJMLMethodDecl.java @@ -38,7 +38,9 @@ public String getParsableDeclaration() { }).collect(Collectors.joining(" ")); String paramsString = methodDefinition.param_list().param_decl().stream() - .map(it -> it.typespec().getText() + " " + it.p.getText() + .map(it -> (it.NULLABLE() != null ? "/*@ nullable @*/" + : it.NON_NULL() != null ? "/*@ non_null @*/" : "") + + " " + it.typespec().getText() + " " + it.p.getText() + StringUtil.repeat("[]", it.LBRACKET().size())) .collect(Collectors.joining(",")); return String.format("%s %s %s (%s);", m, methodDefinition.typespec().getText(), From 200351741f89bdc418b241d963748d016fa81f52 Mon Sep 17 00:00:00 2001 From: Richard Bubel Date: Thu, 19 Oct 2023 16:49:38 +0200 Subject: [PATCH 05/14] Addendum to fix for issue #3186: Also reattach non_null/nullable modifiers to return type declaration of model methods --- .../speclang/jml/pretranslation/TextualJMLMethodDecl.java | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/key.core/src/main/java/de/uka/ilkd/key/speclang/jml/pretranslation/TextualJMLMethodDecl.java b/key.core/src/main/java/de/uka/ilkd/key/speclang/jml/pretranslation/TextualJMLMethodDecl.java index 4dc43db5789..1a5e0574215 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/speclang/jml/pretranslation/TextualJMLMethodDecl.java +++ b/key.core/src/main/java/de/uka/ilkd/key/speclang/jml/pretranslation/TextualJMLMethodDecl.java @@ -33,7 +33,12 @@ public String getParsableDeclaration() { if (JMLTransformer.javaMods.contains(it)) { return it.toString(); } else { - return StringUtil.repeat(" ", it.toString().length()); + JMLModifier jmlMod = JMLModifier.valueOf(it.name()); + if (jmlMod == JMLModifier.NON_NULL || jmlMod == JMLModifier.NULLABLE) { + return "/*@ " + jmlMod.toString() + " @*/"; + } else { + return StringUtil.repeat(" ", it.toString().length()); + } } }).collect(Collectors.joining(" ")); From 35a93ce26979972feeaa454407943d0ba74b2e2b Mon Sep 17 00:00:00 2001 From: Richard Bubel Date: Fri, 20 Oct 2023 09:51:51 +0200 Subject: [PATCH 06/14] Add test for nullability modifiers in model method declarations --- gradle/wrapper/gradle-wrapper.properties | 2 +- .../njml/MethodlevelTranslatorTest.java | 73 ++++++++++++++++++- 2 files changed, 72 insertions(+), 3 deletions(-) diff --git a/gradle/wrapper/gradle-wrapper.properties b/gradle/wrapper/gradle-wrapper.properties index fae08049a6f..e411586a54a 100644 --- a/gradle/wrapper/gradle-wrapper.properties +++ b/gradle/wrapper/gradle-wrapper.properties @@ -1,5 +1,5 @@ distributionBase=GRADLE_USER_HOME distributionPath=wrapper/dists -distributionUrl=https\://services.gradle.org/distributions/gradle-8.1.1-bin.zip +distributionUrl=https\://services.gradle.org/distributions/gradle-8.4-bin.zip zipStoreBase=GRADLE_USER_HOME zipStorePath=wrapper/dists diff --git a/key.core/src/test/java/de/uka/ilkd/key/speclang/njml/MethodlevelTranslatorTest.java b/key.core/src/test/java/de/uka/ilkd/key/speclang/njml/MethodlevelTranslatorTest.java index 6be3e51a9bc..ec837a6c34f 100644 --- a/key.core/src/test/java/de/uka/ilkd/key/speclang/njml/MethodlevelTranslatorTest.java +++ b/key.core/src/test/java/de/uka/ilkd/key/speclang/njml/MethodlevelTranslatorTest.java @@ -5,14 +5,15 @@ import java.io.IOException; import java.io.InputStream; +import java.util.List; import java.util.stream.Stream; import org.antlr.v4.runtime.CommonTokenStream; import org.junit.jupiter.api.DynamicTest; +import org.junit.jupiter.api.Test; import org.junit.jupiter.api.TestFactory; -import static org.junit.jupiter.api.Assertions.assertEquals; -import static org.junit.jupiter.api.Assertions.assertNotEquals; +import static org.junit.jupiter.api.Assertions.*; /** * @author Alexander Weigl @@ -41,6 +42,74 @@ public void parseAndInterpret(String expr) { assertEquals(0, parser.getNumberOfSyntaxErrors()); } + @Test + public void parseModelMethodsNullable() { + String modelMethodNullable = """ + /*@ public model_behavior + requires true; + accessible n, this.a; + model nullable Object foo(nullable Nullable n) { + return null; + } + @*/ + """; + JmlLexer lexer = JmlFacade.createLexer(modelMethodNullable); + JmlParser parser = new JmlParser(new CommonTokenStream(lexer)); + JmlParser.Classlevel_commentsContext ctx = null; + try { + ctx = parser.classlevel_comments(); + if (parser.getNumberOfSyntaxErrors() != 0) { + debugLexer(modelMethodNullable); + } + } catch (Exception e) { + debugLexer(modelMethodNullable); + System.out.println(e.getMessage()); + } + assertEquals(0, parser.getNumberOfSyntaxErrors()); + + List modelMethodModifiers = + ctx.classlevel_comment(1).modifiers().modifier(); + assertTrue(modelMethodModifiers.stream().anyMatch(it -> it.NULLABLE() != null)); + JmlParser.Param_listContext modelMethodParameters = + ctx.classlevel_comment(2).classlevel_element().method_declaration().param_list(); + assertTrue( + modelMethodParameters.param_decl().stream().anyMatch(it -> it.NULLABLE() != null)); + } + + @Test + public void parseModelMethodsNonNull() { + String modelMethodNullable = """ + /*@ public model_behavior + requires true; + accessible n, this.a; + model non_null Object foo(non_null Nullable n) { + return null; + } + @*/ + """; + JmlLexer lexer = JmlFacade.createLexer(modelMethodNullable); + JmlParser parser = new JmlParser(new CommonTokenStream(lexer)); + JmlParser.Classlevel_commentsContext ctx = null; + try { + ctx = parser.classlevel_comments(); + if (parser.getNumberOfSyntaxErrors() != 0) { + debugLexer(modelMethodNullable); + } + } catch (Exception e) { + debugLexer(modelMethodNullable); + System.out.println(e.getMessage()); + } + assertEquals(0, parser.getNumberOfSyntaxErrors()); + + List modelMethodModifiers = + ctx.classlevel_comment(1).modifiers().modifier(); + assertTrue(modelMethodModifiers.stream().anyMatch(it -> it.NON_NULL() != null)); + JmlParser.Param_listContext modelMethodParameters = + ctx.classlevel_comment(2).classlevel_element().method_declaration().param_list(); + assertTrue( + modelMethodParameters.param_decl().stream().anyMatch(it -> it.NON_NULL() != null)); + } + private void debugLexer(String expr) { JmlLexer lexer = JmlFacade.createLexer(expr); DebugJmlLexer.debug(lexer); From 92238e4d647d97d4c3591b74db8720175e4d51ec Mon Sep 17 00:00:00 2001 From: Richard Bubel Date: Fri, 20 Oct 2023 10:57:25 +0200 Subject: [PATCH 07/14] Fix test to also test the textual translator and not just the parser --- .../pretranslation/TextualJMLMethodDecl.java | 2 +- .../njml/MethodlevelTranslatorTest.java | 36 ++++++++++++++++--- 2 files changed, 33 insertions(+), 5 deletions(-) diff --git a/key.core/src/main/java/de/uka/ilkd/key/speclang/jml/pretranslation/TextualJMLMethodDecl.java b/key.core/src/main/java/de/uka/ilkd/key/speclang/jml/pretranslation/TextualJMLMethodDecl.java index 1a5e0574215..7f72a1d0c39 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/speclang/jml/pretranslation/TextualJMLMethodDecl.java +++ b/key.core/src/main/java/de/uka/ilkd/key/speclang/jml/pretranslation/TextualJMLMethodDecl.java @@ -35,7 +35,7 @@ public String getParsableDeclaration() { } else { JMLModifier jmlMod = JMLModifier.valueOf(it.name()); if (jmlMod == JMLModifier.NON_NULL || jmlMod == JMLModifier.NULLABLE) { - return "/*@ " + jmlMod.toString() + " @*/"; + return "/*@ " + jmlMod + " @*/"; } else { return StringUtil.repeat(" ", it.toString().length()); } diff --git a/key.core/src/test/java/de/uka/ilkd/key/speclang/njml/MethodlevelTranslatorTest.java b/key.core/src/test/java/de/uka/ilkd/key/speclang/njml/MethodlevelTranslatorTest.java index ec837a6c34f..97b61cbe38b 100644 --- a/key.core/src/test/java/de/uka/ilkd/key/speclang/njml/MethodlevelTranslatorTest.java +++ b/key.core/src/test/java/de/uka/ilkd/key/speclang/njml/MethodlevelTranslatorTest.java @@ -8,6 +8,8 @@ import java.util.List; import java.util.stream.Stream; +import de.uka.ilkd.key.speclang.jml.pretranslation.JMLModifier; +import de.uka.ilkd.key.speclang.jml.pretranslation.TextualJMLMethodDecl; import org.antlr.v4.runtime.CommonTokenStream; import org.junit.jupiter.api.DynamicTest; import org.junit.jupiter.api.Test; @@ -67,13 +69,25 @@ model nullable Object foo(nullable Nullable n) { } assertEquals(0, parser.getNumberOfSyntaxErrors()); + // Test parser List modelMethodModifiers = - ctx.classlevel_comment(1).modifiers().modifier(); + ctx.classlevel_comment(1).modifiers().modifier(); assertTrue(modelMethodModifiers.stream().anyMatch(it -> it.NULLABLE() != null)); JmlParser.Param_listContext modelMethodParameters = - ctx.classlevel_comment(2).classlevel_element().method_declaration().param_list(); + ctx.classlevel_comment(2).classlevel_element().method_declaration().param_list(); assertTrue( - modelMethodParameters.param_decl().stream().anyMatch(it -> it.NULLABLE() != null)); + modelMethodParameters.param_decl().stream().anyMatch(it -> it.NULLABLE() != null)); + + // Test translation + final TextualTranslator translator = new TextualTranslator(); + ctx.accept(translator); + final var translationOpt = + translator.constructs.stream().filter(c -> c instanceof TextualJMLMethodDecl).findFirst(); + + assertTrue(translationOpt.isPresent(), "No model method declaration found"); + final var methodDecl = ((TextualJMLMethodDecl)translationOpt.get()).getParsableDeclaration(); + assertTrue(methodDecl.contains("/*@ nullable @*/ Object"), "Return value is not nullable"); + assertTrue(methodDecl.contains("/*@ nullable @*/ Nullable n"), "Parameter is not nullable"); } @Test @@ -97,10 +111,11 @@ model non_null Object foo(non_null Nullable n) { } } catch (Exception e) { debugLexer(modelMethodNullable); - System.out.println(e.getMessage()); } assertEquals(0, parser.getNumberOfSyntaxErrors()); + // Test parser + List modelMethodModifiers = ctx.classlevel_comment(1).modifiers().modifier(); assertTrue(modelMethodModifiers.stream().anyMatch(it -> it.NON_NULL() != null)); @@ -108,6 +123,19 @@ model non_null Object foo(non_null Nullable n) { ctx.classlevel_comment(2).classlevel_element().method_declaration().param_list(); assertTrue( modelMethodParameters.param_decl().stream().anyMatch(it -> it.NON_NULL() != null)); + + // Test translation + + final TextualTranslator translator = new TextualTranslator(); + ctx.accept(translator); + final var translationOpt = + translator.constructs.stream().filter(c -> c instanceof TextualJMLMethodDecl).findFirst(); + + assertTrue(translationOpt.isPresent(), "No model method declaration found"); + final var methodDecl = ((TextualJMLMethodDecl)translationOpt.get()).getParsableDeclaration(); + assertTrue(methodDecl.contains("/*@ non_null @*/ Object"), "Return value is not non_null"); + assertTrue(methodDecl.contains("/*@ non_null @*/ Nullable n"), "Parameter is not non_null"); + } private void debugLexer(String expr) { From 645864a7ffd1bef0712a1bdeba74864b836f2e19 Mon Sep 17 00:00:00 2001 From: Richard Bubel Date: Fri, 20 Oct 2023 11:01:20 +0200 Subject: [PATCH 08/14] Spotless fixes --- .../njml/MethodlevelTranslatorTest.java | 20 +++++++++++-------- 1 file changed, 12 insertions(+), 8 deletions(-) diff --git a/key.core/src/test/java/de/uka/ilkd/key/speclang/njml/MethodlevelTranslatorTest.java b/key.core/src/test/java/de/uka/ilkd/key/speclang/njml/MethodlevelTranslatorTest.java index 97b61cbe38b..e004c234881 100644 --- a/key.core/src/test/java/de/uka/ilkd/key/speclang/njml/MethodlevelTranslatorTest.java +++ b/key.core/src/test/java/de/uka/ilkd/key/speclang/njml/MethodlevelTranslatorTest.java @@ -8,8 +8,8 @@ import java.util.List; import java.util.stream.Stream; -import de.uka.ilkd.key.speclang.jml.pretranslation.JMLModifier; import de.uka.ilkd.key.speclang.jml.pretranslation.TextualJMLMethodDecl; + import org.antlr.v4.runtime.CommonTokenStream; import org.junit.jupiter.api.DynamicTest; import org.junit.jupiter.api.Test; @@ -71,21 +71,23 @@ model nullable Object foo(nullable Nullable n) { // Test parser List modelMethodModifiers = - ctx.classlevel_comment(1).modifiers().modifier(); + ctx.classlevel_comment(1).modifiers().modifier(); assertTrue(modelMethodModifiers.stream().anyMatch(it -> it.NULLABLE() != null)); JmlParser.Param_listContext modelMethodParameters = - ctx.classlevel_comment(2).classlevel_element().method_declaration().param_list(); + ctx.classlevel_comment(2).classlevel_element().method_declaration().param_list(); assertTrue( - modelMethodParameters.param_decl().stream().anyMatch(it -> it.NULLABLE() != null)); + modelMethodParameters.param_decl().stream().anyMatch(it -> it.NULLABLE() != null)); // Test translation final TextualTranslator translator = new TextualTranslator(); ctx.accept(translator); final var translationOpt = - translator.constructs.stream().filter(c -> c instanceof TextualJMLMethodDecl).findFirst(); + translator.constructs.stream().filter(c -> c instanceof TextualJMLMethodDecl) + .findFirst(); assertTrue(translationOpt.isPresent(), "No model method declaration found"); - final var methodDecl = ((TextualJMLMethodDecl)translationOpt.get()).getParsableDeclaration(); + final var methodDecl = + ((TextualJMLMethodDecl) translationOpt.get()).getParsableDeclaration(); assertTrue(methodDecl.contains("/*@ nullable @*/ Object"), "Return value is not nullable"); assertTrue(methodDecl.contains("/*@ nullable @*/ Nullable n"), "Parameter is not nullable"); } @@ -129,10 +131,12 @@ model non_null Object foo(non_null Nullable n) { final TextualTranslator translator = new TextualTranslator(); ctx.accept(translator); final var translationOpt = - translator.constructs.stream().filter(c -> c instanceof TextualJMLMethodDecl).findFirst(); + translator.constructs.stream().filter(c -> c instanceof TextualJMLMethodDecl) + .findFirst(); assertTrue(translationOpt.isPresent(), "No model method declaration found"); - final var methodDecl = ((TextualJMLMethodDecl)translationOpt.get()).getParsableDeclaration(); + final var methodDecl = + ((TextualJMLMethodDecl) translationOpt.get()).getParsableDeclaration(); assertTrue(methodDecl.contains("/*@ non_null @*/ Object"), "Return value is not non_null"); assertTrue(methodDecl.contains("/*@ non_null @*/ Nullable n"), "Parameter is not non_null"); From ef68bf9227bda695e2a6ea6b96c0dcdbcd1a9490 Mon Sep 17 00:00:00 2001 From: Richard Bubel Date: Fri, 20 Oct 2023 23:30:52 +0200 Subject: [PATCH 09/14] Revert lazy term index updates The optimization introduced some subtle bug. I have an example that can reproduce it. As it is part of a lab, I cannot share it at the moment (publicly). I assume the revert may also fix #3259 This commit reverts: 8b7e5b15673c2f61965d13d40e3155f11fd2a8c1 e18b309282b77088160ffd26f11f3b5ecee787bd 81a18ccb6fd11e6faf40442604db36e33a14fdfe --- .../rule/ModalitySideProofRule.java | 2 - .../de/uka/ilkd/key/logic/Semisequent.java | 5 - .../ilkd/key/proof/BuiltInRuleAppIndex.java | 64 ++--- .../main/java/de/uka/ilkd/key/proof/Goal.java | 6 - .../de/uka/ilkd/key/proof/RuleAppIndex.java | 25 +- .../de/uka/ilkd/key/proof/TacletAppIndex.java | 243 ++++++++---------- .../key/proof/rulefilter/SetRuleFilter.java | 14 +- .../uka/ilkd/key/prover/impl/PerfScope.java | 5 +- .../strategy/QueueRuleApplicationManager.java | 3 +- .../ilkd/key/strategy/RuleAppContainer.java | 7 - 10 files changed, 149 insertions(+), 225 deletions(-) diff --git a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/rule/ModalitySideProofRule.java b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/rule/ModalitySideProofRule.java index 992bc81fe02..b16dec84ea4 100644 --- a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/rule/ModalitySideProofRule.java +++ b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/rule/ModalitySideProofRule.java @@ -6,7 +6,6 @@ import java.util.LinkedHashSet; import java.util.List; import java.util.Set; -import javax.annotation.Nonnull; import de.uka.ilkd.key.java.Services; import de.uka.ilkd.key.logic.Name; @@ -133,7 +132,6 @@ public IBuiltInRuleApp createApp(PosInOccurrence pos, TermServices services) { /** * {@inheritDoc} */ - @Nonnull @Override public ImmutableList apply(Goal goal, Services services, RuleApp ruleApp) throws RuleAbortException { diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/Semisequent.java b/key.core/src/main/java/de/uka/ilkd/key/logic/Semisequent.java index 0d01c78681c..8660bb7e5fd 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/Semisequent.java +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/Semisequent.java @@ -144,7 +144,6 @@ public boolean isEmpty() { */ private SemisequentChangeInfo insertAndRemoveRedundancyHelper(int idx, SequentFormula sequentFormula, SemisequentChangeInfo semiCI, FormulaChangeInfo fci) { - assert idx >= 0; // Search for equivalent formulas and weakest constraint ImmutableList searchList = semiCI.getFormulaList(); @@ -260,7 +259,6 @@ private SemisequentChangeInfo removeRedundance(int idx, SequentFormula sequentFo */ public SemisequentChangeInfo replace(PosInOccurrence pos, SequentFormula sequentFormula) { final int idx = indexOf(pos.sequentFormula()); - assert idx >= 0; final FormulaChangeInfo fci = new FormulaChangeInfo(pos, sequentFormula); return insertAndRemoveRedundancyHelper(idx, sequentFormula, remove(idx), fci); } @@ -424,9 +422,6 @@ public ImmutableList asList() { @Override public boolean equals(Object o) { - if (this == o) { - return true; - } if (!(o instanceof Semisequent)) { return false; } diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/BuiltInRuleAppIndex.java b/key.core/src/main/java/de/uka/ilkd/key/proof/BuiltInRuleAppIndex.java index 99fb06e8aaf..43eb5e8961b 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/BuiltInRuleAppIndex.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/BuiltInRuleAppIndex.java @@ -3,8 +3,6 @@ * SPDX-License-Identifier: GPL-2.0-only */ package de.uka.ilkd.key.proof; -import java.util.concurrent.atomic.AtomicLong; - import de.uka.ilkd.key.logic.*; import de.uka.ilkd.key.rule.BuiltInRule; import de.uka.ilkd.key.rule.IBuiltInRuleApp; @@ -13,25 +11,27 @@ import org.key_project.util.collection.ImmutableSLList; public class BuiltInRuleAppIndex { - public static final AtomicLong PERF_CREATE_ALL = new AtomicLong(); - public static final AtomicLong PERF_UPDATE = new AtomicLong(); + private final BuiltInRuleIndex index; - private SequentChangeInfo sequentChangeInfo = null; + private NewRuleListener newRuleListener = NullNewRuleListener.INSTANCE; public BuiltInRuleAppIndex(BuiltInRuleIndex index) { this.index = index; } - private BuiltInRuleAppIndex(BuiltInRuleIndex index, SequentChangeInfo sequentChangeInfo) { + + public BuiltInRuleAppIndex(BuiltInRuleIndex index, NewRuleListener p_newRuleListener) { this.index = index; - this.sequentChangeInfo = sequentChangeInfo; + this.newRuleListener = p_newRuleListener; } + /** * returns a list of built-in rules application applicable for the given goal and position */ public ImmutableList getBuiltInRule(Goal goal, PosInOccurrence pos) { + ImmutableList result = ImmutableSLList.nil(); ImmutableList rules = index.rules(); @@ -51,8 +51,11 @@ public ImmutableList getBuiltInRule(Goal goal, PosInOccurrence * returns a copy of this index */ public BuiltInRuleAppIndex copy() { - return new BuiltInRuleAppIndex(index.copy(), - sequentChangeInfo == null ? null : sequentChangeInfo.copy()); + return new BuiltInRuleAppIndex(index.copy()); + } + + public void setNewRuleListener(NewRuleListener p_newRuleListener) { + newRuleListener = p_newRuleListener; } public BuiltInRuleIndex builtInRuleIndex() { @@ -79,8 +82,7 @@ private void scanSimplificationRule(Goal goal, NewRuleListener listener) { } } - private static void scanSimplificationRule(ImmutableList rules, Goal goal, - boolean antec, + private void scanSimplificationRule(ImmutableList rules, Goal goal, boolean antec, NewRuleListener listener) { final Node node = goal.node(); final Sequent seq = node.sequent(); @@ -90,8 +92,7 @@ private static void scanSimplificationRule(ImmutableList rules, Goa } } - private static void scanSimplificationRule(ImmutableList rules, Goal goal, - boolean antec, + private void scanSimplificationRule(ImmutableList rules, Goal goal, boolean antec, SequentFormula cfma, NewRuleListener listener) { final PosInOccurrence pos = new PosInOccurrence(cfma, PosInTerm.getTopLevel(), antec); ImmutableList subrules = ImmutableSLList.nil(); @@ -109,7 +110,7 @@ private static void scanSimplificationRule(ImmutableList rules, Goa } // TODO: optimise? - private static void scanSimplificationRule(ImmutableList rules, Goal goal, + private void scanSimplificationRule(ImmutableList rules, Goal goal, PosInOccurrence pos, NewRuleListener listener) { ImmutableList it = rules; while (!it.isEmpty()) { @@ -125,11 +126,8 @@ private static void scanSimplificationRule(ImmutableList rules, Goa } } - public void reportRuleApps(Goal goal, NewRuleListener l) { - var time = System.nanoTime(); + public void reportRuleApps(NewRuleListener l, Goal goal) { scanSimplificationRule(goal, l); - sequentChangeInfo = null; - PERF_CREATE_ALL.getAndAdd(System.nanoTime() - time); } /** @@ -137,32 +135,12 @@ public void reportRuleApps(Goal goal, NewRuleListener l) { * * @param sci SequentChangeInfo describing the change of the sequent */ - public void sequentChanged(SequentChangeInfo sci) { - if (sequentChangeInfo == null) { - // Nothing stored, store change - sequentChangeInfo = sci.copy(); - } else { - assert sequentChangeInfo.sequent() == sci.getOriginalSequent(); - sequentChangeInfo.combine(sci); - } - } + public void sequentChanged(Goal goal, SequentChangeInfo sci, NewRuleListener listener) { + scanAddedFormulas(goal, true, sci, listener); + scanAddedFormulas(goal, false, sci, listener); - public void resetSequentChanges() { - sequentChangeInfo = null; - } - - public void flushSequentChanges(Goal goal, NewRuleListener listener) { - if (sequentChangeInfo == null) { - return; - } - var time = System.nanoTime(); - scanAddedFormulas(goal, true, sequentChangeInfo, listener); - scanAddedFormulas(goal, false, sequentChangeInfo, listener); - - scanModifiedFormulas(goal, true, sequentChangeInfo, listener); - scanModifiedFormulas(goal, false, sequentChangeInfo, listener); - sequentChangeInfo = null; - PERF_UPDATE.getAndAdd(System.nanoTime() - time); + scanModifiedFormulas(goal, true, sci, listener); + scanModifiedFormulas(goal, false, sci, listener); } private void scanAddedFormulas(Goal goal, boolean antec, SequentChangeInfo sci, diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/Goal.java b/key.core/src/main/java/de/uka/ilkd/key/proof/Goal.java index b4c89a5bf0a..c03f57c3c9f 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/Goal.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/Goal.java @@ -366,12 +366,6 @@ public void setSequent(SequentChangeInfo sci) { assert sci.sequent().equals(sci.getOriginalSequent()); return; } - // sci.hasChanged() can be true for added: f, removed: f - // This afaik only ever happens in TestApplyTaclet.testBugBrokenApply - // Since SequentChangeInfo does not filter this we have to - // work with maybe sci.original.equals(sci.sequent) - // Checking this is probably too expensive for what it's worth - assert sci.sequent() != sci.getOriginalSequent(); node().setSequent(sci.sequent()); node().getNodeInfo().setSequentChangeInfo(sci); var time = System.nanoTime(); diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/RuleAppIndex.java b/key.core/src/main/java/de/uka/ilkd/key/proof/RuleAppIndex.java index 222edfa7743..db86a7be58f 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/RuleAppIndex.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/RuleAppIndex.java @@ -91,6 +91,7 @@ private RuleAppIndex(TacletIndex tacletIndex, TacletAppIndex interactiveTacletAp private void setNewRuleListeners() { interactiveTacletAppIndex.setNewRuleListener(newRuleListener); automatedTacletAppIndex.setNewRuleListener(newRuleListener); + builtInRuleAppIndex.setNewRuleListener(newRuleListener); } /** @@ -235,7 +236,8 @@ public ImmutableList getRewriteTaclet(TacletFilter filter, * constraint and position */ public ImmutableList getBuiltInRules(Goal g, PosInOccurrence pos) { - return builtInRuleAppIndex.getBuiltInRule(g, pos); + + return builtInRuleAppIndex().getBuiltInRule(g, pos); } @@ -293,9 +295,11 @@ public void removeNoPosTacletApp(NoPosTacletApp tacletApp) { * @param sci SequentChangeInfo describing the change of the sequent */ public void sequentChanged(SequentChangeInfo sci) { - interactiveTacletAppIndex.sequentChanged(sci); + if (!autoMode) { + interactiveTacletAppIndex.sequentChanged(sci); + } automatedTacletAppIndex.sequentChanged(sci); - builtInRuleAppIndex.sequentChanged(sci); + builtInRuleAppIndex.sequentChanged(goal, sci, newRuleListener); } /** @@ -314,7 +318,6 @@ public void clearIndexes() { // Currently this only applies to the taclet index interactiveTacletAppIndex.clearIndexes(); automatedTacletAppIndex.clearIndexes(); - builtInRuleAppIndex.resetSequentChanges(); } /** @@ -325,16 +328,18 @@ public void fillCache() { interactiveTacletAppIndex.fillCache(); } automatedTacletAppIndex.fillCache(); - builtInRuleAppIndex.flushSequentChanges(goal, newRuleListener); } /** * Report all rule applications that are supposed to be applied automatically, and that are * currently stored by the index + * + * @param l the NewRuleListener + * @param services the Services */ - public void reportAutomatedRuleApps() { - automatedTacletAppIndex.reportRuleApps(newRuleListener, goal.proof().getServices()); - builtInRuleAppIndex.reportRuleApps(goal, newRuleListener); + public void reportAutomatedRuleApps(NewRuleListener l, Services services) { + automatedTacletAppIndex.reportRuleApps(l, services); + builtInRuleAppIndex.reportRuleApps(l, goal); } /** @@ -343,7 +348,7 @@ public void reportAutomatedRuleApps() { * @param p_goal the Goal which to scan */ public void scanBuiltInRules(Goal p_goal) { - builtInRuleAppIndex.scanApplicableRules(p_goal, newRuleListener); + builtInRuleAppIndex().scanApplicableRules(p_goal, newRuleListener); } /** @@ -377,7 +382,7 @@ public RuleAppIndex copy(Goal goal) { TacletAppIndex copiedAutomatedTacletAppIndex = automatedTacletAppIndex.copyWith(copiedTacletIndex, goal); return new RuleAppIndex(copiedTacletIndex, copiedInteractiveTacletAppIndex, - copiedAutomatedTacletAppIndex, builtInRuleAppIndex.copy(), goal, autoMode); + copiedAutomatedTacletAppIndex, builtInRuleAppIndex().copy(), goal, autoMode); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/TacletAppIndex.java b/key.core/src/main/java/de/uka/ilkd/key/proof/TacletAppIndex.java index 9f4cce98b73..46e401d1d5a 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/TacletAppIndex.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/TacletAppIndex.java @@ -7,7 +7,6 @@ import java.util.Map; import java.util.concurrent.atomic.AtomicLong; import javax.annotation.Nonnull; -import javax.annotation.Nullable; import de.uka.ilkd.key.java.Services; import de.uka.ilkd.key.logic.PosInOccurrence; @@ -58,25 +57,30 @@ public class TacletAppIndex { */ private RuleFilter ruleFilter; - private State state; - + /** + * The sequent with the formulas for which taclet indices are hold by this object. Invariant: + * seq != null implies that the indices antecIndex, + * succIndex are up to date for the sequent seq + */ + private Sequent seq; + private final Map cache; public TacletAppIndex(TacletIndex tacletIndex, Goal goal, Services services) { - this(tacletIndex, null, null, goal, new State(), TacletFilter.TRUE, + this(tacletIndex, null, null, goal, null, TacletFilter.TRUE, new TermTacletAppIndexCacheSet(services.getCaches().getTermTacletAppIndexCache()), services.getCaches().getTermTacletAppIndexCache()); } private TacletAppIndex(TacletIndex tacletIndex, SemisequentTacletAppIndex antecIndex, - SemisequentTacletAppIndex succIndex, @Nonnull Goal goal, State state, + SemisequentTacletAppIndex succIndex, @Nonnull Goal goal, Sequent seq, RuleFilter ruleFilter, TermTacletAppIndexCacheSet indexCaches, Map cache) { this.tacletIndex = tacletIndex; this.antecIndex = antecIndex; this.succIndex = succIndex; this.goal = goal; - this.state = state; + this.seq = seq; this.ruleFilter = ruleFilter; this.indexCaches = indexCaches; this.cache = cache; @@ -97,13 +101,13 @@ public void setRuleFilter(RuleFilter p_ruleFilter) { * returns a new TacletAppIndex with a given TacletIndex */ TacletAppIndex copyWith(TacletIndex p_tacletIndex, Goal goal) { - return new TacletAppIndex(p_tacletIndex, antecIndex, succIndex, goal, state.copy(), + return new TacletAppIndex(p_tacletIndex, antecIndex, succIndex, goal, getSequent(), ruleFilter, indexCaches, cache); } /** * Delete all cached information about taclet apps. This also makes the index cache of this - * index independent of the caches of other indexes (expensive) + * index independent from the caches of other indexes (expensive) */ public void clearAndDetachCache() { clearIndexes(); @@ -111,7 +115,7 @@ public void clearAndDetachCache() { } public void clearIndexes() { - this.state.clear(); + seq = null; // This leads to a delayed rebuild antecIndex = null; succIndex = null; } @@ -131,75 +135,44 @@ private void createNewIndexCache() { * (NewRuleListener gets informed) */ public void fillCache() { - update(false); + ensureIndicesExist(); } - private void createAllFromGoal(boolean silent) { + private void createAllFromGoal() { var time = System.nanoTime(); + try { + this.seq = getNode().sequent(); - this.state.seq = goal.sequent(); - var listener = silent ? NullNewRuleListener.INSTANCE : newRuleListener; - - antecIndex = - new SemisequentTacletAppIndex(this.state.seq, true, getServices(), tacletIndex, - listener, ruleFilter, indexCaches); - succIndex = - new SemisequentTacletAppIndex(this.state.seq, false, getServices(), tacletIndex, - listener, ruleFilter, indexCaches); - - // Full rebuild from the taclet index - this.state.sci = null; - this.state.newRules = null; - - PERF_CREATE_ALL.getAndAdd(System.nanoTime() - time); - } - - private void update(boolean silent) { - if (!isOutdated()) { - return; - } - if (this.state.sci != null && this.state.sci.sequent() == goal.sequent()) { - deltaUpdateIndices(this.state.sci, silent); - } else { - createAllFromGoal(silent); - } - this.state.sci = null; - } - - private void deltaUpdateIndices(SequentChangeInfo sci, boolean silent) { - var time = System.nanoTime(); - this.state.seq = sci.sequent(); - - var listener = silent ? NullNewRuleListener.INSTANCE : newRuleListener; - // Sequent changes - antecIndex = - antecIndex.sequentChanged(sci, getServices(), tacletIndex, listener); - succIndex = - succIndex.sequentChanged(sci, getServices(), tacletIndex, listener); - - if (this.state.newRules != null) { - // New rules antecIndex = - antecIndex.addTaclets(this.state.newRules, getServices(), tacletIndex, listener); + new SemisequentTacletAppIndex(getSequent(), true, getServices(), tacletIndex(), + newRuleListener, ruleFilter, indexCaches); succIndex = - succIndex.addTaclets(this.state.newRules, getServices(), tacletIndex, listener); - this.state.newRules = null; + new SemisequentTacletAppIndex(getSequent(), false, getServices(), tacletIndex(), + newRuleListener, ruleFilter, indexCaches); + } finally { + PERF_CREATE_ALL.getAndAdd(System.nanoTime() - time); } + } - PERF_UPDATE.getAndAdd(System.nanoTime() - time); + private void ensureIndicesExist() { + if (isOutdated()) { + // Indices are not up-to-date + createAllFromGoal(); + } } /** - * @return true iff this index is currently outdated; this does not detect other modifications - * like an altered user constraint + * @return true iff this index is currently outdated with respect to the sequent of the + * associated goal; this does not detect other modifications + * like an altered user + * constraint */ private boolean isOutdated() { - assert state.seq == null || (state.seq != goal.sequent()) == (state.sci != null); - return state.seq != goal.sequent() || state.newRules != null; + return getGoal() == null || getSequent() != getNode().sequent(); } private SemisequentTacletAppIndex getIndex(PosInOccurrence pos) { - update(false); + ensureIndicesExist(); return pos.isInAntec() ? antecIndex : succIndex; } @@ -263,7 +236,7 @@ static TacletApp createTacletApp(NoPosTacletApp tacletApp, PosInOccurrence pos, */ public ImmutableList getNoFindTaclet(TacletFilter filter, Services services) { RuleFilter effectiveFilter = new AndRuleFilter(filter, ruleFilter); - return tacletIndex.getNoFindTaclet(effectiveFilter, services); + return tacletIndex().getNoFindTaclet(effectiveFilter, services); } /** @@ -325,21 +298,33 @@ public ImmutableList getTacletAppAtAndBelow(PosInOccurrence pos, Tacl * @param sci SequentChangeInfo describing the change of the sequent */ public void sequentChanged(SequentChangeInfo sci) { - if (state.sci == null) { - if (state.seq != sci.getOriginalSequent()) { - // we are not up-to-date and have to rebuild everything - clearIndexes(); - } else { - // Nothing stored, store change - state.sci = sci.copy(); - } + if (sci.getOriginalSequent() != getSequent()) { + // we are not up-to-date and have to rebuild everything (lazy) + clearIndexes(); } else { - assert state.sci.sequent() == sci.getOriginalSequent(); - // Combine the changes - state.sci.combine(sci); + var time = System.nanoTime(); + updateIndices(sci); + PERF_UPDATE.getAndAdd(System.nanoTime() - time); } } + private void updateIndices(SequentChangeInfo sci) { + seq = sci.sequent(); + + antecIndex = + antecIndex.sequentChanged(sci, getServices(), tacletIndex, newRuleListener); + + succIndex = + succIndex.sequentChanged(sci, getServices(), tacletIndex, newRuleListener); + } + + private void updateIndices(final SetRuleFilter newTaclets) { + antecIndex = + antecIndex.addTaclets(newTaclets, getServices(), tacletIndex, newRuleListener); + succIndex = + succIndex.addTaclets(newTaclets, getServices(), tacletIndex, newRuleListener); + } + /** * updates the internal caches after a new Taclet with instantiation information has been added @@ -355,6 +340,12 @@ public void addedNoPosTacletApp(NoPosTacletApp tacletApp) { createNewIndexCache(); } + if (isOutdated()) { + // we are not up-to-date and have to rebuild everything (lazy) + clearIndexes(); + return; + } + if (tacletApp.taclet() instanceof NoFindTaclet) { if (ruleFilter.filter(tacletApp.taclet())) { newRuleListener.ruleAdded(tacletApp, null); @@ -362,10 +353,10 @@ public void addedNoPosTacletApp(NoPosTacletApp tacletApp) { return; } - if (state.newRules == null) { - state.newRules = new SetRuleFilter(); - } - state.newRules.addRuleToSet(tacletApp.taclet()); + final SetRuleFilter newTaclets = new SetRuleFilter(); + newTaclets.addRuleToSet(tacletApp.taclet()); + + updateIndices(newTaclets); } /** @@ -385,24 +376,32 @@ public void addedNoPosTacletApps(Iterable tacletApps) { } } - if (state.newRules == null) { - state.newRules = new SetRuleFilter(); + if (isOutdated()) { + // we are not up-to-date and have to rebuild everything (lazy) + clearIndexes(); + return; } + + final SetRuleFilter newTaclets = new SetRuleFilter(); for (NoPosTacletApp tacletApp : tacletApps) { if (tacletApp.taclet() instanceof NoFindTaclet) { if (ruleFilter.filter(tacletApp.taclet())) { newRuleListener.ruleAdded(tacletApp, null); } } else { - state.newRules.addRuleToSet(tacletApp.taclet()); + newTaclets.addRuleToSet(tacletApp.taclet()); } } - if (state.newRules.isEmpty()) { - state.newRules = null; + if (newTaclets.isEmpty()) { + return; } + + updateIndices(newTaclets); } + + /** * updates the internal caches after a Taclet with instantiation information has been removed * from the TacletIndex. @@ -434,8 +433,31 @@ private static ImmutableList prepend(ImmutableList l1, return l1; } + private Goal getGoal() { + return goal; + } + + private Sequent getSequent() { + return seq; + } + private Services getServices() { - return goal.node().proof().getServices(); + return getProof().getServices(); + } + + private Proof getProof() { + return getNode().proof(); + } + + private Node getNode() { + return goal.node(); + } + + /** + * returns the Taclet index for this ruleAppIndex. + */ + public TacletIndex tacletIndex() { + return tacletIndex; } /** @@ -443,60 +465,13 @@ private Services getServices() { * taclet app. */ public void reportRuleApps(NewRuleListener l, Services services) { - if (antecIndex != null && succIndex != null) { - update(true); + if (antecIndex != null) { antecIndex.reportRuleApps(l); + } + if (succIndex != null) { succIndex.reportRuleApps(l); } l.rulesAdded(getNoFindTaclet(TacletFilter.TRUE, services), null); } - - private static final class State { - /** - * The sequent with the formulas for which taclet indices are hold by this object. - * Invariant: - * seq != null implies that the indices antecIndex, - * succIndex are up-to-date for the sequent seq - */ - @Nullable - public Sequent seq; - - /** - * Used for delta updates. If this is nonnull, originalSequent == seq and resultingSequent - * == - * goal.sequent. - */ - @Nullable - public SequentChangeInfo sci; - @Nullable - public SetRuleFilter newRules; - - public State() { - this(null, null, null); - } - - public State(@Nullable Sequent seq, @Nullable SequentChangeInfo sequentChangeInfo, - @Nullable SetRuleFilter newRules) { - this.seq = seq; - this.sci = sequentChangeInfo; - this.newRules = newRules; - } - - public State copy() { - return new State( - seq, - sci == null ? null : sci.copy(), - newRules == null ? null : newRules.copy()); - } - - public void clear() { - // This leads to a delayed rebuild - this.seq = null; - // This is needed since delta updates must be disabled as well (e.g. new taclet was - // added) - this.sci = null; - this.newRules = null; - } - } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/rulefilter/SetRuleFilter.java b/key.core/src/main/java/de/uka/ilkd/key/proof/rulefilter/SetRuleFilter.java index 1486b88372f..9eabaf47b2c 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/rulefilter/SetRuleFilter.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/rulefilter/SetRuleFilter.java @@ -13,19 +13,7 @@ */ public class SetRuleFilter implements RuleFilter { - private final HashSet set; - - public SetRuleFilter() { - this.set = new LinkedHashSet<>(); - } - - private SetRuleFilter(HashSet set) { - this.set = set; - } - - public SetRuleFilter copy() { - return new SetRuleFilter(new LinkedHashSet<>(this.set)); - } + private final HashSet set = new LinkedHashSet<>(); public void addRuleToSet(Rule rule) { set.add(rule); diff --git a/key.core/src/main/java/de/uka/ilkd/key/prover/impl/PerfScope.java b/key.core/src/main/java/de/uka/ilkd/key/prover/impl/PerfScope.java index 5ac50a990cd..0094f9574e3 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/prover/impl/PerfScope.java +++ b/key.core/src/main/java/de/uka/ilkd/key/prover/impl/PerfScope.java @@ -8,7 +8,6 @@ import java.util.Locale; import java.util.concurrent.atomic.AtomicLong; -import de.uka.ilkd.key.proof.BuiltInRuleAppIndex; import de.uka.ilkd.key.proof.Goal; import de.uka.ilkd.key.proof.SemisequentTacletAppIndex; import de.uka.ilkd.key.proof.TacletAppIndex; @@ -39,13 +38,11 @@ public class PerfScope { new Pair<>("Goal setSequent", Goal.PERF_SET_SEQUENT), new Pair<>("Goal update tag manager", Goal.PERF_UPDATE_TAG_MANAGER), new Pair<>("Goal update rule app index", Goal.PERF_UPDATE_RULE_APP_INDEX), + new Pair<>("Taclet app index update", TacletAppIndex.PERF_UPDATE), new Pair<>("Semi Taclet app index update remove", SemisequentTacletAppIndex.PERF_REMOVE), new Pair<>("Semi Taclet app index update add", SemisequentTacletAppIndex.PERF_ADD), new Pair<>("Semi Taclet app index update update", SemisequentTacletAppIndex.PERF_UPDATE), - new Pair<>("Taclet app index update", TacletAppIndex.PERF_UPDATE), new Pair<>("Taclet app index create all", TacletAppIndex.PERF_CREATE_ALL), - new Pair<>("Builtin app index update", BuiltInRuleAppIndex.PERF_UPDATE), - new Pair<>("Builtin app index create all", BuiltInRuleAppIndex.PERF_CREATE_ALL), new Pair<>("Goal update listeners", Goal.PERF_UPDATE_LISTENERS), new Pair<>("TacletApp execute", TacletApp.PERF_EXECUTE), new Pair<>("TacletApp pre", TacletApp.PERF_PRE), diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/QueueRuleApplicationManager.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/QueueRuleApplicationManager.java index 44f5b7001f4..d6354bdfcd3 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/strategy/QueueRuleApplicationManager.java +++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/QueueRuleApplicationManager.java @@ -99,7 +99,8 @@ private void ensureQueueExists() { // FocussedRuleApplicationManager) the rule index // reports its contents to the rule manager of the goal, which is not // necessarily this object - goal.ruleAppIndex().reportAutomatedRuleApps(); + goal.ruleAppIndex().reportAutomatedRuleApps(goal.getRuleAppManager(), + goal.proof().getServices()); } /** diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/RuleAppContainer.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/RuleAppContainer.java index b8872ca935e..81fc05f4425 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/strategy/RuleAppContainer.java +++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/RuleAppContainer.java @@ -118,11 +118,4 @@ public static ImmutableList createAppContainers( return result; } - @Override - public String toString() { - return "RuleAppContainer{" + - "ruleApp=" + ruleApp.rule().name() + - ", cost=" + cost + - '}'; - } } From a3b31940111e4f288fb790dc83e590aebde4c4bf Mon Sep 17 00:00:00 2001 From: Alexander Weigl Date: Sat, 28 Oct 2023 15:54:19 +0200 Subject: [PATCH 10/14] fix classcastexception in logic printer (adapted from main for Java 11) occured by java-enhanced-for example --- .../src/main/java/de/uka/ilkd/key/pp/LogicPrinter.java | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/key.core/src/main/java/de/uka/ilkd/key/pp/LogicPrinter.java b/key.core/src/main/java/de/uka/ilkd/key/pp/LogicPrinter.java index d6ee751ffa7..813ca5473cc 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/pp/LogicPrinter.java +++ b/key.core/src/main/java/de/uka/ilkd/key/pp/LogicPrinter.java @@ -405,10 +405,11 @@ protected void printNewVarcond(NewVarcond sv) { printSchemaVariable(sv.getSchemaVariable()); layouter.print(",").brk(); if (sv.isDefinedByType()) { - if (sv.getType() instanceof ArrayType) { - layouter.print(((ArrayType) sv.getType()).getAlternativeNameRepresentation()); + final var type = sv.getType(); + if (type.getJavaType() instanceof ArrayType) { + layouter.print(((ArrayType)type.getJavaType()).getAlternativeNameRepresentation()); } else { - layouter.print(sv.getType().getFullName()); + layouter.print(type.getFullName()); } } else { layouter.print("\\typeof(").brk(0); From 5f1be71394841eaa0d26cd8838997f310aa4095b Mon Sep 17 00:00:00 2001 From: Richard Bubel Date: Sat, 28 Oct 2023 18:16:08 +0200 Subject: [PATCH 11/14] Adapt Test to Java 11 (which does not support text blocks --- .../njml/MethodlevelTranslatorTest.java | 27 +++++++------------ 1 file changed, 9 insertions(+), 18 deletions(-) diff --git a/key.core/src/test/java/de/uka/ilkd/key/speclang/njml/MethodlevelTranslatorTest.java b/key.core/src/test/java/de/uka/ilkd/key/speclang/njml/MethodlevelTranslatorTest.java index e004c234881..f6cd87c6f10 100644 --- a/key.core/src/test/java/de/uka/ilkd/key/speclang/njml/MethodlevelTranslatorTest.java +++ b/key.core/src/test/java/de/uka/ilkd/key/speclang/njml/MethodlevelTranslatorTest.java @@ -46,15 +46,10 @@ public void parseAndInterpret(String expr) { @Test public void parseModelMethodsNullable() { - String modelMethodNullable = """ - /*@ public model_behavior - requires true; - accessible n, this.a; - model nullable Object foo(nullable Nullable n) { - return null; - } - @*/ - """; + String modelMethodNullable = + "/*@ public model_behavior\n requires true;\n accessible n, this.a;\n" + + "model nullable Object foo(nullable Nullable n) {\n" + + "return null;} @*/"; JmlLexer lexer = JmlFacade.createLexer(modelMethodNullable); JmlParser parser = new JmlParser(new CommonTokenStream(lexer)); JmlParser.Classlevel_commentsContext ctx = null; @@ -94,15 +89,11 @@ model nullable Object foo(nullable Nullable n) { @Test public void parseModelMethodsNonNull() { - String modelMethodNullable = """ - /*@ public model_behavior - requires true; - accessible n, this.a; - model non_null Object foo(non_null Nullable n) { - return null; - } - @*/ - """; + String modelMethodNullable = "/*@ public model_behavior\n" + + "requires true;\n" + + "accessible n, this.a;\n" + + "model non_null Object foo(non_null Nullable n) {\n" + + "return null;}@*/"; JmlLexer lexer = JmlFacade.createLexer(modelMethodNullable); JmlParser parser = new JmlParser(new CommonTokenStream(lexer)); JmlParser.Classlevel_commentsContext ctx = null; From 495401ab3bd0bd4ad743beca9852d028ce494b33 Mon Sep 17 00:00:00 2001 From: Richard Bubel Date: Sat, 28 Oct 2023 18:16:29 +0200 Subject: [PATCH 12/14] Spotless changes --- key.core/src/main/java/de/uka/ilkd/key/pp/LogicPrinter.java | 2 +- .../src/main/java/de/uka/ilkd/key/proof/TacletAppIndex.java | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/key.core/src/main/java/de/uka/ilkd/key/pp/LogicPrinter.java b/key.core/src/main/java/de/uka/ilkd/key/pp/LogicPrinter.java index 813ca5473cc..e843173e17a 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/pp/LogicPrinter.java +++ b/key.core/src/main/java/de/uka/ilkd/key/pp/LogicPrinter.java @@ -407,7 +407,7 @@ protected void printNewVarcond(NewVarcond sv) { if (sv.isDefinedByType()) { final var type = sv.getType(); if (type.getJavaType() instanceof ArrayType) { - layouter.print(((ArrayType)type.getJavaType()).getAlternativeNameRepresentation()); + layouter.print(((ArrayType) type.getJavaType()).getAlternativeNameRepresentation()); } else { layouter.print(type.getFullName()); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/TacletAppIndex.java b/key.core/src/main/java/de/uka/ilkd/key/proof/TacletAppIndex.java index 46e401d1d5a..e38935fb458 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/TacletAppIndex.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/TacletAppIndex.java @@ -63,7 +63,7 @@ public class TacletAppIndex { * succIndex are up to date for the sequent seq */ private Sequent seq; - + private final Map cache; public TacletAppIndex(TacletIndex tacletIndex, Goal goal, Services services) { From 93cf0b0f893fdcf7bfc22788c79785c89405bea8 Mon Sep 17 00:00:00 2001 From: Richard Bubel Date: Wed, 8 Nov 2023 20:12:15 +0100 Subject: [PATCH 13/14] Fix stuck CounterExample Dialog In case of an exception when translating the formula to SMT input, the CE Dialog could not be dismissed, requiring KeY to be restarted. --- .../AbstractCounterExampleGenerator.java | 4 - .../ilkd/key/smt/SMTSolverImplementation.java | 2 +- .../de/uka/ilkd/key/smt/SolverLauncher.java | 5 +- .../uka/ilkd/key/gui/smt/ProgressDialog.java | 1 - .../key/gui/testgen/CounterExampleAction.java | 96 ++----------------- 5 files changed, 12 insertions(+), 96 deletions(-) diff --git a/key.core.testgen/src/main/java/de/uka/ilkd/key/smt/counterexample/AbstractCounterExampleGenerator.java b/key.core.testgen/src/main/java/de/uka/ilkd/key/smt/counterexample/AbstractCounterExampleGenerator.java index 36f3689a7ab..61546a95392 100644 --- a/key.core.testgen/src/main/java/de/uka/ilkd/key/smt/counterexample/AbstractCounterExampleGenerator.java +++ b/key.core.testgen/src/main/java/de/uka/ilkd/key/smt/counterexample/AbstractCounterExampleGenerator.java @@ -68,14 +68,12 @@ public void searchCounterExample(UserInterfaceControl ui, Proof oldProof, Sequen throw new IllegalStateException( "Can't find SMT solver " + SolverTypes.Z3_CE_SOLVER.getName()); } - final Proof proof = createProof(ui, oldProof, oldSequent, "Semantics Blasting: " + oldProof.name()); final SemanticsBlastingMacro macro = new SemanticsBlastingMacro(); TaskFinishedInfo info = ProofMacroFinishedInfo.getDefaultInfo(macro, proof); final ProverTaskListener ptl = ui.getProofControl().getDefaultProverTaskListener(); ptl.taskStarted(new DefaultTaskStartedInfo(TaskKind.Macro, macro.getName(), 0)); - try { synchronized (macro) { // TODO: Useless? No other thread has access to macro wait for // macro to terminate @@ -99,8 +97,6 @@ public void searchCounterExample(UserInterfaceControl ui, Proof oldProof, Sequen solvers.add(SolverTypes.Z3_CE_SOLVER); launcher.launch(solvers, SMTProblem.createSMTProblems(proof), proof.getServices()); - - } /** diff --git a/key.core/src/main/java/de/uka/ilkd/key/smt/SMTSolverImplementation.java b/key.core/src/main/java/de/uka/ilkd/key/smt/SMTSolverImplementation.java index d49395a117a..a3394921a9e 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/smt/SMTSolverImplementation.java +++ b/key.core/src/main/java/de/uka/ilkd/key/smt/SMTSolverImplementation.java @@ -255,7 +255,7 @@ public void run() { String[] commands; try { commands = translateToCommand(problem.getSequent()); - } catch (IllegalFormulaException e) { + } catch (Throwable e) { interruptionOccurred(e); listener.processInterrupted(this, problem, e); setSolverState(SolverState.Stopped); diff --git a/key.core/src/main/java/de/uka/ilkd/key/smt/SolverLauncher.java b/key.core/src/main/java/de/uka/ilkd/key/smt/SolverLauncher.java index 03a8b7090fb..6dfacf097f6 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/smt/SolverLauncher.java +++ b/key.core/src/main/java/de/uka/ilkd/key/smt/SolverLauncher.java @@ -286,7 +286,6 @@ private void launchSolvers(Queue solvers, Collection prob // Launch all solvers until the queue is empty or the launcher is // interrupted. launchLoop(solvers); - // at this point either there are no solvers left to start or // the whole launching process was interrupted. waitForRunningSolvers(); @@ -294,7 +293,6 @@ private void launchSolvers(Queue solvers, Collection prob cleanUp(solvers); notifyListenersOfStop(); - } private void notifyListenersOfStart(Collection problems, @@ -320,7 +318,6 @@ private void launchLoop(Queue solvers) { // if there is nothing to do, wait for the next solver // finishing its task. wait.await(); - } catch (InterruptedException e) { launcherInterrupted(e); } @@ -386,8 +383,8 @@ private void notifySolverHasFinished(SMTSolver solver) { lock.lock(); try { session.removeCurrentlyRunning(solver); - wait.signal(); } finally { + wait.signal(); lock.unlock(); } } diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/smt/ProgressDialog.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/smt/ProgressDialog.java index 13a8bb0d6eb..c048e4a057b 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/smt/ProgressDialog.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/smt/ProgressDialog.java @@ -205,7 +205,6 @@ private JButton getStopButton() { if (modus.equals(Modus.SOLVERS_RUNNING)) { listener.stopButtonClicked(); } - }); } return stopButton; diff --git a/keyext.ui.testgen/src/main/java/de/uka/ilkd/key/gui/testgen/CounterExampleAction.java b/keyext.ui.testgen/src/main/java/de/uka/ilkd/key/gui/testgen/CounterExampleAction.java index db480ebfc49..be7ec1c3e2e 100644 --- a/keyext.ui.testgen/src/main/java/de/uka/ilkd/key/gui/testgen/CounterExampleAction.java +++ b/keyext.ui.testgen/src/main/java/de/uka/ilkd/key/gui/testgen/CounterExampleAction.java @@ -9,9 +9,7 @@ import javax.swing.*; import de.uka.ilkd.key.control.AutoModeListener; -import de.uka.ilkd.key.control.UserInterfaceControl; import de.uka.ilkd.key.core.InterruptListener; -import de.uka.ilkd.key.core.KeYMediator; import de.uka.ilkd.key.core.KeYSelectionEvent; import de.uka.ilkd.key.core.KeYSelectionListener; import de.uka.ilkd.key.gui.IssueDialog; @@ -22,8 +20,6 @@ import de.uka.ilkd.key.logic.Sequent; import de.uka.ilkd.key.macros.SemanticsBlastingMacro; import de.uka.ilkd.key.proof.*; -import de.uka.ilkd.key.proof.init.InitConfig; -import de.uka.ilkd.key.proof.mgt.SpecificationRepository; import de.uka.ilkd.key.settings.DefaultSMTSettings; import de.uka.ilkd.key.settings.ProofIndependentSettings; import de.uka.ilkd.key.smt.SolverLauncherListener; @@ -70,15 +66,12 @@ public void init() { @Override public void selectedNodeChanged(KeYSelectionEvent e) { final Proof proof = getMediator().getSelectedProof(); - if (proof == null) { // no proof loaded setEnabled(false); } else { final Node selNode = getMediator().getSelectedNode(); // Can be applied only to root nodes - - setEnabled(haveZ3CE && selNode.childrenCount() == 0 && !selNode.isClosed()); } } @@ -102,7 +95,6 @@ public void autoModeStarted(ProofEvent e) { @Override public void autoModeStopped(ProofEvent e) { getMediator().addKeYSelectionListener(selListener); - selListener.selectedNodeChanged(null); } }); selListener.selectedNodeChanged(new KeYSelectionEvent(getMediator().getSelectionModel())); @@ -112,16 +104,16 @@ public void autoModeStopped(ProofEvent e) { public void actionPerformed(ActionEvent e) { try { // Get required information - Goal goal = getMediator().getSelectedGoal(); - Node node = goal.node(); - Proof oldProof = node.proof(); - Sequent oldSequent = node.sequent(); - // Start SwingWorker (CEWorker) in which counter example search is performed. - getMediator().stopInterface(true); - getMediator().setInteractive(false); - CEWorker worker = new CEWorker(oldProof, oldSequent); - getMediator().addInterruptedListener(worker); - worker.execute(); + final Goal goal = getMediator().getSelectedGoal(); + if (goal != null) { + final Node node = goal.node(); + // Start SwingWorker (CEWorker) in which counter example search is performed. + getMediator().stopInterface(true); + getMediator().setInteractive(false); + CEWorker worker = new CEWorker(node.proof(), node.sequent()); + getMediator().addInterruptedListener(worker); + worker.execute(); + } } catch (Exception exc) { LOGGER.error("", exc); IssueDialog.showExceptionDialog(mainWindow, exc); @@ -165,74 +157,6 @@ protected SolverLauncherListener createSolverListener(DefaultSMTSettings setting } } - /** - * Performs the {@link SemanticsBlastingMacro} in a {@link Proof} registered in the - * {@link MainWindow} and thus visible to the user. Results are shown with help of the - * {@link SolverListener}. - *

- * This class provides only the user interface and no counter example generation logic which - * is implemented by the {@link AbstractCounterExampleGenerator}. - */ - public static class MainWindowCounterExampleGenerator extends AbstractCounterExampleGenerator { - /** - * The {@link KeYMediator} to use. - */ - private final KeYMediator mediator; - - /** - * Constructor. - * - * @param mediator The {@link KeYMediator} to use. - */ - public MainWindowCounterExampleGenerator(KeYMediator mediator) { - this.mediator = mediator; - } - - /** - * {@inheritDoc} - */ - @Override - protected Proof createProof(UserInterfaceControl ui, Proof oldProof, Sequent oldSequent, - String proofName) { - Sequent newSequent = createNewSequent(oldSequent); - InitConfig newInitConfig = oldProof.getInitConfig().deepCopy(); - Proof proof = new Proof(proofName, newSequent, "", newInitConfig.createTacletIndex(), - newInitConfig.createBuiltInRuleIndex(), newInitConfig); - - proof.setEnv(oldProof.getEnv()); - proof.setNamespaces(oldProof.getNamespaces()); - - ProofAggregate pa = new SingleProof(proof, "XXX"); - - ui.registerProofAggregate(pa); - - SpecificationRepository spec = proof.getServices().getSpecificationRepository(); - spec.registerProof(spec.getProofOblInput(oldProof), proof); - - mediator.goalChosen(proof.getOpenGoal(proof.root())); - - return proof; - } - - /** - * {@inheritDoc} - */ - @Override - protected void semanticsBlastingCompleted(UserInterfaceControl ui) { - mediator.setInteractive(true); - mediator.startInterface(true); - } - - /** - * {@inheritDoc} - */ - @Override - protected SolverLauncherListener createSolverListener(DefaultSMTSettings settings, - Proof proof) { - return new SolverListener(settings, proof); - } - } - private class CEWorker extends SwingWorker implements InterruptListener { private final Proof oldProof; private final Sequent oldSequent; From 4f5a25baadc97f437eea653738b8642d3a284f45 Mon Sep 17 00:00:00 2001 From: Richard Bubel Date: Thu, 9 Nov 2023 15:01:30 +0100 Subject: [PATCH 14/14] Pruning a closed proof (and reopening it) did not update the proof status in the task tree and also did not select any node/goal. --- .../de/uka/ilkd/key/core/KeYMediator.java | 6 +++++- .../java/de/uka/ilkd/key/gui/TaskTree.java | 21 ++++++++++--------- 2 files changed, 16 insertions(+), 11 deletions(-) diff --git a/key.ui/src/main/java/de/uka/ilkd/key/core/KeYMediator.java b/key.ui/src/main/java/de/uka/ilkd/key/core/KeYMediator.java index 3102b2ba53c..e2b7eb31f7c 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/core/KeYMediator.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/core/KeYMediator.java @@ -265,12 +265,16 @@ protected boolean filter(Taclet taclet) { public void setBack(Node node) { getUI().getProofControl().pruneTo(node); finishSetBack(node.proof()); + keySelectionModel.setSelectedNode(node); } public void setBack(Goal goal) { if (getSelectedProof() != null) { getUI().getProofControl().pruneTo(goal); - finishSetBack(goal.proof()); + final Proof proof = goal.proof(); + finishSetBack(proof); + Node node = goal.node() == proof.root() ? goal.node() : goal.node().parent(); + keySelectionModel.setSelectedNode(node); } } diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/TaskTree.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/TaskTree.java index 100ff854d80..8a8ff4981b1 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/TaskTree.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/TaskTree.java @@ -24,7 +24,6 @@ import de.uka.ilkd.key.gui.fonticons.IconFactory; import de.uka.ilkd.key.gui.notification.events.AbandonTaskEvent; import de.uka.ilkd.key.proof.Proof; -import de.uka.ilkd.key.proof.ProofTreeAdapter; import de.uka.ilkd.key.proof.ProofTreeEvent; import de.uka.ilkd.key.proof.ProofTreeListener; import de.uka.ilkd.key.proof.mgt.BasicTask; @@ -285,7 +284,7 @@ private void checkPopup(MouseEvent e) { /** * a prooftree listener, so that it is known when the proof has closed */ - class TaskTreeProofTreeListener extends ProofTreeAdapter { + class TaskTreeProofTreeListener implements ProofTreeListener { /** * invoked if all goals of the proof are closed @@ -295,17 +294,19 @@ public void proofClosed(ProofTreeEvent e) { } /** - * invoked if the list of goals changed (goals were added, removed etc. + * invoked if a proof has been pruned, potentially reopening branches */ - public void proofGoalRemoved(ProofTreeEvent e) { - } - - /** invoked if the current goal of the proof changed */ - public void proofGoalsAdded(ProofTreeEvent e) { + public void proofPruned(ProofTreeEvent e) { + delegateView.repaint(); } - /** invoked if the current goal of the proof changed */ - public void proofGoalsChanged(ProofTreeEvent e) { + /** + * The structure of the proof has changed radically. Any client should rescan the whole + * proof + * tree. + */ + public void proofStructureChanged(ProofTreeEvent e) { + delegateView.repaint(); } } // end of prooftreelistener