diff --git a/README.md b/README.md index d63b2be..599e4a6 100644 --- a/README.md +++ b/README.md @@ -67,4 +67,6 @@ problem, then dumps it to standard output: $ java -jar semgus-java.jar max2-exp.sem.json ``` +The current JSON format is in line with the 2-23-24 edition of Semgus-Parser which introduced support for parametric sorts. + For more information, check out all the declarations and accompanying JavaDocs in the source code. diff --git a/build.gradle.kts b/build.gradle.kts index c6a5660..d424c8f 100644 --- a/build.gradle.kts +++ b/build.gradle.kts @@ -1,6 +1,7 @@ plugins { java `maven-publish` + id("com.github.johnrengelman.shadow") version "7.0.0" } group = "org.semgus" @@ -38,6 +39,15 @@ tasks.getByName("jar") { } } +tasks.shadowJar { + configurations = listOf(project.configurations.getByName("runtimeClasspath")) // Include runtime dependencies in shadow JAR + manifest { + attributes( + "Main-Class" to "org.semgus.java.Main" + ) + } +} + publishing { publications { create("maven") { diff --git a/src/main/java/org/semgus/java/event/EventParser.java b/src/main/java/org/semgus/java/event/EventParser.java index 741c6ad..d39d23a 100644 --- a/src/main/java/org/semgus/java/event/EventParser.java +++ b/src/main/java/org/semgus/java/event/EventParser.java @@ -117,7 +117,7 @@ public static SpecEvent parseEvent(String eventJson) throws ParseException, Dese */ public static SpecEvent parseEvent(JSONObject eventDto) throws DeserializationException { String eventType = JsonUtils.getString(eventDto, "$event"); - return switch (eventType) { + SpecEvent event = switch (eventType) { // meta events case "set-info" -> parseSetInfo(eventDto); case "end-of-stream" -> new MetaSpecEvent.StreamEndEvent(); @@ -138,6 +138,8 @@ public static SpecEvent parseEvent(JSONObject eventDto) throws DeserializationEx default -> throw new DeserializationException( String.format("Unknown specification event \"%s\"", eventType), "$event"); }; + + return event; } /** @@ -164,13 +166,13 @@ private static DeclareFunctionEvent parseDeclareFunction(JSONObject eventDto) th String name = JsonUtils.getString(eventDto, "name"); JSONObject rankDto = JsonUtils.getObject(eventDto, "rank"); - Identifier returnType; - List argumentTypes; + Sort returnType; + List argumentTypes; try { - returnType = Identifier.deserializeAt(rankDto, "returnSort"); + returnType = Sort.deserializeAt(rankDto, "returnSort"); JSONArray argumentTypesDto = JsonUtils.getArray(rankDto, "argumentSorts"); try { - argumentTypes = Identifier.deserializeList(argumentTypesDto); + argumentTypes = Sort.deserializeList(argumentTypesDto); } catch (DeserializationException e) { throw e.prepend("argumentSorts"); } @@ -196,6 +198,7 @@ private static DefineFunctionEvent parseDefineFunction(JSONObject eventDto) thro TypedVar[] arguments = new TypedVar[declEvent.argumentTypes().size()]; SmtTerm body; + HashMap annotationMap = new HashMap<>(); try { List argNames = JsonUtils.getStrings(defnDto, "arguments"); if (argNames.size() != arguments.length) { @@ -210,11 +213,31 @@ private static DefineFunctionEvent parseDefineFunction(JSONObject eventDto) thro } body = SmtTerm.deserializeAt(defnDto, "body"); + + var bodyObj = JsonUtils.getObject(defnDto, "body"); + + if (bodyObj.containsKey("annotations")) { + Object annotationsObj = bodyObj.get("annotations"); + + if (!(annotationsObj instanceof JSONArray annotations)) { + throw new DeserializationException("Annotation is neither null nor an array"); + } + + JsonUtils.ensureObjects(annotations); + for (Object annotationItemObj : annotations) { + var annotationItem = (JSONObject) annotationItemObj; + var keywordObj = JsonUtils.getObject(annotationItem, "keyword"); + var keyword = JsonUtils.getString(keywordObj, "name"); + var value = AttributeValue.deserializeAt(annotationItem, "value"); + annotationMap.put(keyword, value); + } + } } catch (DeserializationException e) { throw e.prepend("definition"); } - return new DefineFunctionEvent(declEvent.name(), declEvent.returnType(), Arrays.asList(arguments), body); + return new DefineFunctionEvent(declEvent.name(), declEvent.returnType(), + Arrays.asList(arguments), body, annotationMap); } /** @@ -246,9 +269,9 @@ private static DefineDatatypeEvent parseDefineDatatype(JSONObject eventDto) thro String constructorName = JsonUtils.getString(constructorDto, "name"); JSONArray argumentTypesDto = JsonUtils.getArray(constructorDto, "children"); - List argumentTypes; + List argumentTypes; try { - argumentTypes = Identifier.deserializeList(argumentTypesDto); + argumentTypes = Sort.deserializeList(argumentTypesDto); } catch (DeserializationException e) { throw e.prepend("children"); } @@ -331,10 +354,10 @@ private static HornClauseEvent parseHornClause(JSONObject eventDto) throws Deser "constructor"); } - // parse constructor arg type identifiers - List constructorArgTypes; + // parse constructor arg type sorts + List constructorArgTypes; try { - constructorArgTypes = Identifier.deserializeList(constructorArgTypesDto); + constructorArgTypes = Sort.deserializeList(constructorArgTypesDto); } catch (DeserializationException e) { throw e.prepend("constructor.argumentSorts"); } diff --git a/src/main/java/org/semgus/java/event/SmtSpecEvent.java b/src/main/java/org/semgus/java/event/SmtSpecEvent.java index ebfe7f8..300cbc9 100644 --- a/src/main/java/org/semgus/java/event/SmtSpecEvent.java +++ b/src/main/java/org/semgus/java/event/SmtSpecEvent.java @@ -1,10 +1,13 @@ package org.semgus.java.event; -import org.semgus.java.object.Identifier; +import org.semgus.java.object.AttributeValue; +import org.semgus.java.object.Sort; import org.semgus.java.object.SmtTerm; import org.semgus.java.object.TypedVar; +import java.util.HashMap; import java.util.List; +import java.util.Map; import java.util.stream.Collectors; /** @@ -21,8 +24,8 @@ public sealed interface SmtSpecEvent extends SpecEvent { */ record DeclareFunctionEvent( String name, - Identifier returnType, - List argumentTypes + Sort returnType, + List argumentTypes ) implements SmtSpecEvent { // NO-OP } @@ -34,14 +37,21 @@ record DeclareFunctionEvent( * @param returnType The return type of the function. * @param arguments The arguments to the function. * @param body The body of the function. + * @param annotations The annotations (usually about input/output variables) on the function body. (optional) */ record DefineFunctionEvent( String name, - Identifier returnType, + Sort returnType, List arguments, - SmtTerm body + SmtTerm body, + Map annotations ) implements SmtSpecEvent { + public DefineFunctionEvent(String name, Sort returnType, List arguments, + SmtTerm body) { + this(name, returnType, arguments, body, new HashMap<>()); + } + /** * Constructs a {@link org.semgus.java.object.SmtTerm.Lambda} lambda abstraction from the function definition. * @@ -76,7 +86,7 @@ record DefineDatatypeEvent(String name, List constructors) implemen * @param name The name of the constructor. * @param argumentTypes The types of the arguments to the constructor. */ - public record Constructor(String name, List argumentTypes) { + public record Constructor(String name, List argumentTypes) { // NO-OP } diff --git a/src/main/java/org/semgus/java/object/Identifier.java b/src/main/java/org/semgus/java/object/Identifier.java index d833328..09aaa6b 100644 --- a/src/main/java/org/semgus/java/object/Identifier.java +++ b/src/main/java/org/semgus/java/object/Identifier.java @@ -48,44 +48,28 @@ public static Identifier deserialize(Object idDtoRaw) throws DeserializationExce } return new Identifier((String)nameRaw, indices); - } - throw new DeserializationException("Identifier must either be a string or an array!"); - } - - /** - * Deserializes an identifier from the SemGuS JSON format at a given key in a parent JSON object. - * - * @param parentDto The parent JSON object. - * @param key The key whose value should be deserialized. - * @return The deserialized identifier. - * @throws DeserializationException If the value at {@code key} is not a valid representation of an identifier. - */ - public static Identifier deserializeAt(JSONObject parentDto, String key) throws DeserializationException { - Object identifierDto = JsonUtils.get(parentDto, key); - try { - return deserialize(identifierDto); - } catch (DeserializationException e) { - throw e.prepend(key); - } - } - - /** - * Deserializes a list of identifiers from a JSON array. - * - * @param idsDto The JSON array of identifiers. - * @return The list of the deserialized identifiers. - * @throws DeserializationException If {@code idsDto} is not an array of valid representations of identifiers. - */ - public static List deserializeList(JSONArray idsDto) throws DeserializationException { - Identifier[] ids = new Identifier[idsDto.size()]; - for (int i = 0; i < ids.length; i++) { - try { - ids[i] = deserialize(idsDto.get(i)); - } catch (DeserializationException e) { - throw e.prepend(i); + } else if (idDtoRaw instanceof JSONObject idDto) { + // it's possibly a (Seq Int) or other types defined in a similar way + Object nameRaw = idDto.get("kind"); + if (!(nameRaw instanceof String name)) { + throw new DeserializationException("Identifier name must be a string!", 0); + } + Object paramsRaw = idDto.get("params"); + if (!(paramsRaw instanceof JSONArray params)) { + throw new DeserializationException("'params' is not a JSON array!", 1); + } + Index[] indices = new Index[params.size()]; + for (int i = 0; i < indices.length; i++) { + try { + indices[i] = Index.deserialize(params.get(i)); + } catch (DeserializationException e) { + throw e.prepend(i + 1); + } } + + return new Identifier(name, indices); } - return Arrays.asList(ids); + throw new DeserializationException("Identifier must either be a string, an array or an object containing keys 'kind' and 'params'!"); } @Override @@ -93,9 +77,9 @@ public String toString() { if (indices.length == 0) { return name; } - StringBuilder sb = new StringBuilder("(").append(name); + StringBuilder sb = new StringBuilder("(_ ").append(name); for (Index index : indices) { - sb.append(" ").append(index); + sb.append(" ").append(index.toString()); } return sb.append(")").toString(); } @@ -113,26 +97,10 @@ public sealed interface Index { * @throws DeserializationException If {@code indexDtoRaw} is not a valid representation of an index value. */ static Index deserialize(Object indexDtoRaw) throws DeserializationException { - if (indexDtoRaw instanceof String index) { - return new NString(index); - } else if (indexDtoRaw instanceof Long index) { + if (indexDtoRaw instanceof Long index) { return new NInt(index.intValue()); } - throw new DeserializationException("Identifier index must either be a string or integer constant!"); - } - - /** - * A string index value. - * - * @param value The string value. - */ - record NString(String value) implements Index { - - @Override - public String toString() { - return "\"" + value + "\""; - } - + throw new DeserializationException("Identifier index must be an integer constant!"); } /** diff --git a/src/main/java/org/semgus/java/object/RelationApp.java b/src/main/java/org/semgus/java/object/RelationApp.java index 294b324..5ea112f 100644 --- a/src/main/java/org/semgus/java/object/RelationApp.java +++ b/src/main/java/org/semgus/java/object/RelationApp.java @@ -35,10 +35,10 @@ public static RelationApp deserialize(JSONObject relAppDto) throws Deserializati sigDto.size(), args.size())); } - // deserialize type identifiers - List types; + // deserialize type sorts + List types; try { - types = Identifier.deserializeList(sigDto); + types = Sort.deserializeList(sigDto); } catch (DeserializationException e) { throw e.prepend("signature"); } diff --git a/src/main/java/org/semgus/java/object/SmtContext.java b/src/main/java/org/semgus/java/object/SmtContext.java index cff8319..0fa971a 100644 --- a/src/main/java/org/semgus/java/object/SmtContext.java +++ b/src/main/java/org/semgus/java/object/SmtContext.java @@ -52,7 +52,7 @@ public String toString() { * @param name The name of the constructor. * @param argumentTypes The types of the constructor's arguments. */ - public record Constructor(String name, List argumentTypes) { + public record Constructor(String name, List argumentTypes) { @Override public String toString() { @@ -61,7 +61,7 @@ public String toString() { } StringBuilder sb = new StringBuilder("(").append(name); - for (Identifier argumentType : argumentTypes) { + for (Sort argumentType : argumentTypes) { sb.append(" ").append(argumentType); } return sb.append(")").toString(); diff --git a/src/main/java/org/semgus/java/object/SmtTerm.java b/src/main/java/org/semgus/java/object/SmtTerm.java index 113371f..fb3ed6f 100644 --- a/src/main/java/org/semgus/java/object/SmtTerm.java +++ b/src/main/java/org/semgus/java/object/SmtTerm.java @@ -69,9 +69,9 @@ static SmtTerm deserializeAt(JSONObject parentDto, String key) throws Deserializ * @throws DeserializationException If {@code termDto} is not a valid representation of a function application. */ private static SmtTerm deserializeApplication(JSONObject termDto) throws DeserializationException { - // deserialize function and return type identifiers - Identifier id = Identifier.deserializeAt(termDto, "name"); - Identifier returnType = Identifier.deserializeAt(termDto, "returnSort"); + // deserialize function and return type sorts + Sort id = Sort.deserializeAt(termDto, "name"); + Sort returnType = Sort.deserializeAt(termDto, "returnSort"); // zip together argument terms and argument types JSONArray argTypes = JsonUtils.getArray(termDto, "argumentSorts"); @@ -84,9 +84,9 @@ private static SmtTerm deserializeApplication(JSONObject termDto) throws Deseria Application.TypedTerm[] argTerms = new Application.TypedTerm[argTypes.size()]; for (int i = 0; i < argTerms.length; i++) { // deserialize type - Identifier type; + Sort type; try { - type = Identifier.deserialize(argTypes.get(i)); + type = Sort.deserialize(argTypes.get(i)); } catch (DeserializationException e) { throw e.prepend("argumentSorts." + i); } @@ -122,7 +122,7 @@ private static SmtTerm deserializeQuantifier(JSONObject termDto, Quantifier.Type JSONObject bindingDto = bindingsDto.get(i); try { bindings[i] = new TypedVar(JsonUtils.getString(bindingDto, "name"), - Identifier.deserializeAt(bindingDto, "sort")); + Sort.deserializeAt(bindingDto, "sort")); } catch (DeserializationException e) { throw e.prepend("bindings." + i); } @@ -180,7 +180,7 @@ private static SmtTerm deserializeMatch(JSONObject termDto) throws Deserializati * @throws DeserializationException If {@code termDto} is not a valid representation of a variable. */ private static SmtTerm deserializeVariable(JSONObject termDto) throws DeserializationException { - return new Variable(JsonUtils.getString(termDto, "name"), Identifier.deserializeAt(termDto, "sort")); + return new Variable(JsonUtils.getString(termDto, "name"), Sort.deserializeAt(termDto, "sort")); } /** @@ -261,11 +261,11 @@ private static int readHexChar(char hexChar) throws DeserializationException { /** * Represents a function application in an SMT formula. * - * @param name The identifier for the function. + * @param name The Sort for the function. * @param returnType The function's return type. * @param arguments The arguments to the function. */ - record Application(Identifier name, Identifier returnType, List arguments) implements SmtTerm { + record Application(Sort name, Sort returnType, List arguments) implements SmtTerm { @Override public String toString() { @@ -279,7 +279,7 @@ public String toString() { * @param type The argument type. * @param term The subterm being passed as an argument. */ - public record TypedTerm(Identifier type, SmtTerm term) { + public record TypedTerm(Sort type, SmtTerm term) { @Override public String toString() { @@ -398,9 +398,9 @@ public String toString() { * Represents a variable in an SMT formula. * * @param name The name of the variable. - * @param type The identifier for the type of the variable. + * @param type The Sort for the type of the variable. */ - record Variable(String name, Identifier type) implements SmtTerm { + record Variable(String name, Sort type) implements SmtTerm { @Override public String toString() { diff --git a/src/main/java/org/semgus/java/object/Sort.java b/src/main/java/org/semgus/java/object/Sort.java new file mode 100644 index 0000000..ff7e3a7 --- /dev/null +++ b/src/main/java/org/semgus/java/object/Sort.java @@ -0,0 +1,104 @@ +package org.semgus.java.object; + +import org.json.simple.JSONArray; +import org.json.simple.JSONObject; +import org.semgus.java.util.DeserializationException; +import org.semgus.java.util.JsonUtils; + +import java.util.Arrays; +import java.util.List; +import org.semgus.java.object.Identifier; + +/** + * Represents a sort as per the SMTLIB spec. Is either an identifier, or an identifier taking sorts as arguments + * (i.e., a type without parameters or a type with parameters specified) + * + * @param base The identifier itself. + * @param sorts The optional parameters to the sort. + */ +public record Sort(Identifier ident, Sort... params) { + /** + * Deserializes an identifier which may or may not be indexed. + * + * @param idDtoRaw A JSON value representing an optionally-indexed identifier. + * @return The deserialized identifier. + * @throws DeserializationException If {@code idDtoRaw} is not a valid representation of an identifier. + */ + public static Sort deserialize(Object idDtoRaw) throws DeserializationException { + if (idDtoRaw instanceof JSONObject idDto) { // if it's an object; then it's a parametrized sort. + // first kind is name, params are params + // parse identifier name + if (!idDto.containsKey("kind") || !idDto.containsKey("params")) { + throw new DeserializationException("Parametric sort is missing information!"); + } + Identifier ident = Identifier.deserialize(idDto.get("kind")); + + if (idDto.get("params") instanceof JSONArray idParams) { + // parse args + Sort[] params = new Sort[idParams.size()]; + for (int i = 0; i < params.length; i++) { + try { + params[i] = Sort.deserialize(idParams.get(i)); + } catch (DeserializationException e) { + throw e.prepend(i); + } + } + return new Sort(ident, params); + } + else { + throw new DeserializationException("Parametric sort's parameters must be specified as a list!"); + } + } + else { + return new Sort(Identifier.deserialize(idDtoRaw)); + } + } + + /** + * Deserializes a sort from the SemGuS JSON format at a given key in a parent JSON object. + * + * @param parentDto The parent JSON object. + * @param key The key whose value should be deserialized. + * @return The deserialized sort. + * @throws DeserializationException If the value at {@code key} is not a valid representation of an sort. + */ + public static Sort deserializeAt(JSONObject parentDto, String key) throws DeserializationException { + Object identifierDto = JsonUtils.get(parentDto, key); + try { + return deserialize(identifierDto); + } catch (DeserializationException e) { + throw e.prepend(key); + } + } + + /** + * Deserializes a list of sorts from a JSON array. + * + * @param idsDto The JSON array of sorts. + * @return The list of the deserialized sorts. + * @throws DeserializationException If {@code idsDto} is not an array of valid representations of sorts. + */ + public static List deserializeList(JSONArray idsDto) throws DeserializationException { + Sort[] ids = new Sort[idsDto.size()]; + for (int i = 0; i < ids.length; i++) { + try { + ids[i] = deserialize(idsDto.get(i)); + } catch (DeserializationException e) { + throw e.prepend(i); + } + } + return Arrays.asList(ids); + } + + @Override + public String toString() { + if (params.length == 0) { + return ident.toString(); + } + StringBuilder sb = new StringBuilder("(").append(ident.toString()); + for (Sort sort : params) { + sb.append(" ").append(sort.toString()); + } + return sb.append(")").toString(); + } +} \ No newline at end of file diff --git a/src/main/java/org/semgus/java/object/TypedVar.java b/src/main/java/org/semgus/java/object/TypedVar.java index 766e610..a58d5d0 100644 --- a/src/main/java/org/semgus/java/object/TypedVar.java +++ b/src/main/java/org/semgus/java/object/TypedVar.java @@ -10,17 +10,17 @@ * @param name The variable's name. * @param type The name of the variable's type. */ -public record TypedVar(String name, Identifier type) { +public record TypedVar(String name, Sort type) { /** - * Zips a list of variable names and a list of type identifiers into a list of typed variables. The two lists should + * Zips a list of variable names and a list of type Sorts into a list of typed variables. The two lists should * have the same length. * * @param names A list of variable names. - * @param types A list of type identifiers. + * @param types A list of type Sorts. * @return A new list of typed variables. */ - public static List fromNamesAndTypes(List names, List types) { + public static List fromNamesAndTypes(List names, List types) { return IntStream.range(0, names.size()) .mapToObj(i -> new TypedVar(names.get(i), types.get(i))) .collect(Collectors.toList());