From 9c9a17611706f4a3110df197528b96ca0bcd5e84 Mon Sep 17 00:00:00 2001 From: Josh Date: Wed, 17 Jun 2026 23:03:01 -0500 Subject: [PATCH 1/3] Add lemma AST object --- .../uiowa/cs/clc/kind2/results/LemmaInfo.java | 133 ++++++++++++++++++ .../uiowa/cs/clc/kind2/results/Result.java | 3 + 2 files changed, 136 insertions(+) create mode 100644 src/main/java/edu/uiowa/cs/clc/kind2/results/LemmaInfo.java diff --git a/src/main/java/edu/uiowa/cs/clc/kind2/results/LemmaInfo.java b/src/main/java/edu/uiowa/cs/clc/kind2/results/LemmaInfo.java new file mode 100644 index 0000000..a3ea0d0 --- /dev/null +++ b/src/main/java/edu/uiowa/cs/clc/kind2/results/LemmaInfo.java @@ -0,0 +1,133 @@ +/* + * Copyright (c) 2020, Board of Trustees of the University of Iowa + * All rights reserved. + * + * Licensed under the BSD 3-Clause License. See LICENSE in the project root for license information. + */ + +package edu.uiowa.cs.clc.kind2.results; + +import com.google.gson.GsonBuilder; +import com.google.gson.JsonElement; +import com.google.gson.JsonObject; + +/** + * Kind2 Lemma Info. + */ +public class LemmaInfo implements AstInfo { + /** + * The original kind2 output for this object in pretty json format. + */ + private final String prettyJson; + /** + * The original kind2 output for this object in json format + */ + private final String json; + /** + * The component name. + */ + private final String name; + /** + * Is this lemma imported? + */ + private final boolean imported; + /** + * Associated file, if any. + */ + private final String file; + /** + * Associated line in the input file, if any. + */ + private final String startLine; + /** + * Associated column in the input file, if any. + */ + private final String startColumn; + /** + * Associated line in the input file, if any. + */ + private final String endLine; + /** + * Associated column in the input file, if any. + */ + private final String endColumn; + + public LemmaInfo(JsonElement jsonElement) { + JsonObject jsonObject = jsonElement.getAsJsonObject(); + prettyJson = new GsonBuilder().setPrettyPrinting().create().toJson(jsonElement); + json = new GsonBuilder().create().toJson(jsonElement); + this.name = jsonObject.get(Labels.name).getAsString(); + this.imported = jsonObject.get(Labels.imported).getAsBoolean(); + this.file = jsonObject.get(Labels.file) == null ? null + : jsonObject.get(Labels.file).getAsString(); + this.startLine = jsonObject.get(Labels.startLine) == null ? null + : jsonObject.get(Labels.startLine).getAsString(); + this.startColumn = jsonObject.get(Labels.startColumn) == null ? null + : jsonObject.get(Labels.startColumn).getAsString(); + this.endLine = jsonObject.get(Labels.endLine) == null ? null + : jsonObject.get(Labels.endLine).getAsString(); + this.endColumn = jsonObject.get(Labels.endColumn) == null ? null + : jsonObject.get(Labels.endColumn).getAsString(); + } + + /** + * @return The original kind2 output for this object in pretty json format. + */ + public String getJson() { + return prettyJson; + } + + /** + * @return The component name. + */ + public String getName() { + return name; + } + + /** + * @return whether or not this lemma is imported. + */ + public boolean isImported() { + return imported; + } + + /** + * @return the uri of the file, if any. + */ + public String getFile() { + return file; + } + + /** + * @return the associated start line in the input file, if any. + */ + public String getStartLine() { + return startLine; + } + + /** + * @return the associated start column in the input file, if any. + */ + public String getStartColumn() { + return startColumn; + } + + /** + * @return the associated end line in the input file, if any. + */ + public String getEndLine() { + return endLine; + } + + /** + * @return the associated end column in the input file, if any. + */ + public String getEndColumn() { + return endColumn; + } + + @Override + public String toString() { + return json; + } +} diff --git a/src/main/java/edu/uiowa/cs/clc/kind2/results/Result.java b/src/main/java/edu/uiowa/cs/clc/kind2/results/Result.java index 932d9cb..a325bdd 100644 --- a/src/main/java/edu/uiowa/cs/clc/kind2/results/Result.java +++ b/src/main/java/edu/uiowa/cs/clc/kind2/results/Result.java @@ -198,6 +198,9 @@ public void initialize(String json) { case "contract": astInfo = new ContractInfo(jsonElement); break; + case "lemma": + astInfo = new LemmaInfo(jsonElement); + break; default: throw new RuntimeException("Failed to analyze kind2 json output"); } From 63e6957bf1914245b56ecb84dd760ea13737aadb Mon Sep 17 00:00:00 2001 From: Josh Date: Wed, 17 Jun 2026 23:03:18 -0500 Subject: [PATCH 2/3] Add termination property type --- .../java/edu/uiowa/cs/clc/kind2/results/PropertyType.java | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/src/main/java/edu/uiowa/cs/clc/kind2/results/PropertyType.java b/src/main/java/edu/uiowa/cs/clc/kind2/results/PropertyType.java index 465bda5..41b84b3 100644 --- a/src/main/java/edu/uiowa/cs/clc/kind2/results/PropertyType.java +++ b/src/main/java/edu/uiowa/cs/clc/kind2/results/PropertyType.java @@ -18,7 +18,8 @@ public enum PropertyType annotation("PropAnnot"), oneModeActive("OneModeActive"), generated("Generated"), - nonVacuityCheck("NonVacuityCheck"); + nonVacuityCheck("NonVacuityCheck"), + termination("Termination"); private final String value; @@ -52,6 +53,9 @@ public static PropertyType getPropertyType(String propertyType) case "NonVacuityCheck": case "nonVacuityCheck": return nonVacuityCheck; + case "Termination": + case "termination": + return termination; default: throw new UnsupportedOperationException("Property type " + propertyType + " is not supported"); } From f101fa7f3b52ddfde2b7a6ccee6265bbfda80dd2 Mon Sep 17 00:00:00 2001 From: Daniel Larraz Date: Thu, 18 Jun 2026 10:35:22 +0200 Subject: [PATCH 3/3] Remove 'imported' attribute --- .../edu/uiowa/cs/clc/kind2/results/LemmaInfo.java | 14 +------------- 1 file changed, 1 insertion(+), 13 deletions(-) diff --git a/src/main/java/edu/uiowa/cs/clc/kind2/results/LemmaInfo.java b/src/main/java/edu/uiowa/cs/clc/kind2/results/LemmaInfo.java index a3ea0d0..96c79f5 100644 --- a/src/main/java/edu/uiowa/cs/clc/kind2/results/LemmaInfo.java +++ b/src/main/java/edu/uiowa/cs/clc/kind2/results/LemmaInfo.java @@ -1,5 +1,5 @@ /* - * Copyright (c) 2020, Board of Trustees of the University of Iowa + * Copyright (c) 2026, Board of Trustees of the University of Iowa * All rights reserved. * * Licensed under the BSD 3-Clause License. See LICENSE in the project root for license information. @@ -27,10 +27,6 @@ public class LemmaInfo implements AstInfo { * The component name. */ private final String name; - /** - * Is this lemma imported? - */ - private final boolean imported; /** * Associated file, if any. */ @@ -57,7 +53,6 @@ public LemmaInfo(JsonElement jsonElement) { prettyJson = new GsonBuilder().setPrettyPrinting().create().toJson(jsonElement); json = new GsonBuilder().create().toJson(jsonElement); this.name = jsonObject.get(Labels.name).getAsString(); - this.imported = jsonObject.get(Labels.imported).getAsBoolean(); this.file = jsonObject.get(Labels.file) == null ? null : jsonObject.get(Labels.file).getAsString(); this.startLine = jsonObject.get(Labels.startLine) == null ? null @@ -84,13 +79,6 @@ public String getName() { return name; } - /** - * @return whether or not this lemma is imported. - */ - public boolean isImported() { - return imported; - } - /** * @return the uri of the file, if any. */