diff options
author | Kristóf Marussy <kristof@marussy.com> | 2023-12-22 02:19:38 +0100 |
---|---|---|
committer | Kristóf Marussy <kristof@marussy.com> | 2023-12-24 17:32:54 +0100 |
commit | c65275be9fce0fbba70094c754690a8bd9228ab4 (patch) | |
tree | 8ba97d3668229482f8e25272ebfe62c2d27cca12 | |
parent | refactor(language): use file extension provider (diff) | |
download | refinery-c65275be9fce0fbba70094c754690a8bd9228ab4.tar.gz refinery-c65275be9fce0fbba70094c754690a8bd9228ab4.tar.zst refinery-c65275be9fce0fbba70094c754690a8bd9228ab4.zip |
feat: solution serializer
9 files changed, 572 insertions, 48 deletions
diff --git a/subprojects/language-model/src/main/resources/model/problem.ecore b/subprojects/language-model/src/main/resources/model/problem.ecore index 204f922c..74229a89 100644 --- a/subprojects/language-model/src/main/resources/model/problem.ecore +++ b/subprojects/language-model/src/main/resources/model/problem.ecore | |||
@@ -23,7 +23,7 @@ | |||
23 | <eStructuralFeatures xsi:type="ecore:EAttribute" name="kind" eType="#//ReferenceKind"/> | 23 | <eStructuralFeatures xsi:type="ecore:EAttribute" name="kind" eType="#//ReferenceKind"/> |
24 | <eStructuralFeatures xsi:type="ecore:EReference" name="referenceType" eType="#//Relation"/> | 24 | <eStructuralFeatures xsi:type="ecore:EReference" name="referenceType" eType="#//Relation"/> |
25 | <eStructuralFeatures xsi:type="ecore:EReference" name="invalidMultiplicity" eType="#//Relation" | 25 | <eStructuralFeatures xsi:type="ecore:EReference" name="invalidMultiplicity" eType="#//Relation" |
26 | containment="true"/> | 26 | transient="true" containment="true"/> |
27 | </eClassifiers> | 27 | </eClassifiers> |
28 | <eClassifiers xsi:type="ecore:EClass" name="NamedElement" abstract="true"> | 28 | <eClassifiers xsi:type="ecore:EClass" name="NamedElement" abstract="true"> |
29 | <eStructuralFeatures xsi:type="ecore:EAttribute" name="name" eType="ecore:EDataType http://www.eclipse.org/emf/2002/Ecore#//EString"/> | 29 | <eStructuralFeatures xsi:type="ecore:EAttribute" name="name" eType="ecore:EDataType http://www.eclipse.org/emf/2002/Ecore#//EString"/> |
diff --git a/subprojects/language-semantics/build.gradle.kts b/subprojects/language-semantics/build.gradle.kts index 689f621e..777ef993 100644 --- a/subprojects/language-semantics/build.gradle.kts +++ b/subprojects/language-semantics/build.gradle.kts | |||
@@ -16,6 +16,7 @@ dependencies { | |||
16 | api(project(":refinery-store-reasoning")) | 16 | api(project(":refinery-store-reasoning")) |
17 | implementation(project(":refinery-store-reasoning-scope")) | 17 | implementation(project(":refinery-store-reasoning-scope")) |
18 | runtimeOnly(libs.eclipseCollections) | 18 | runtimeOnly(libs.eclipseCollections) |
19 | testImplementation(project(":refinery-generator")) | ||
19 | testImplementation(project(":refinery-store-dse-visualization")) | 20 | testImplementation(project(":refinery-store-dse-visualization")) |
20 | testImplementation(project(":refinery-store-query-interpreter")) | 21 | testImplementation(project(":refinery-store-query-interpreter")) |
21 | testImplementation(testFixtures(project(":refinery-language"))) | 22 | testImplementation(testFixtures(project(":refinery-language"))) |
diff --git a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/ProblemTraceImpl.java b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/ProblemTraceImpl.java index cc634949..f686e980 100644 --- a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/ProblemTraceImpl.java +++ b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/ProblemTraceImpl.java | |||
@@ -9,7 +9,6 @@ import com.google.inject.Inject; | |||
9 | import org.eclipse.collections.api.factory.primitive.ObjectIntMaps; | 9 | import org.eclipse.collections.api.factory.primitive.ObjectIntMaps; |
10 | import org.eclipse.collections.api.map.primitive.MutableObjectIntMap; | 10 | import org.eclipse.collections.api.map.primitive.MutableObjectIntMap; |
11 | import org.eclipse.collections.api.map.primitive.ObjectIntMap; | 11 | import org.eclipse.collections.api.map.primitive.ObjectIntMap; |
12 | import org.eclipse.emf.ecore.util.EcoreUtil; | ||
13 | import org.eclipse.xtext.naming.IQualifiedNameConverter; | 12 | import org.eclipse.xtext.naming.IQualifiedNameConverter; |
14 | import org.eclipse.xtext.naming.QualifiedName; | 13 | import org.eclipse.xtext.naming.QualifiedName; |
15 | import org.eclipse.xtext.scoping.IScope; | 14 | import org.eclipse.xtext.scoping.IScope; |
@@ -28,7 +27,7 @@ import java.util.HashMap; | |||
28 | import java.util.LinkedHashMap; | 27 | import java.util.LinkedHashMap; |
29 | import java.util.Map; | 28 | import java.util.Map; |
30 | 29 | ||
31 | public class ProblemTraceImpl implements ProblemTrace { | 30 | class ProblemTraceImpl implements ProblemTrace { |
32 | @Inject | 31 | @Inject |
33 | private IQualifiedNameConverter qualifiedNameConverter; | 32 | private IQualifiedNameConverter qualifiedNameConverter; |
34 | 33 | ||
@@ -164,24 +163,6 @@ public class ProblemTraceImpl implements ProblemTrace { | |||
164 | } | 163 | } |
165 | 164 | ||
166 | private <T> T getElement(IScope scope, QualifiedName qualifiedName, Class<T> type) { | 165 | private <T> T getElement(IScope scope, QualifiedName qualifiedName, Class<T> type) { |
167 | var iterator = scope.getElements(qualifiedName).iterator(); | 166 | return semanticsUtils.getElement(problem, scope, qualifiedName, type); |
168 | if (!iterator.hasNext()) { | ||
169 | var qualifiedNameString = qualifiedNameConverter.toString(qualifiedName); | ||
170 | throw new IllegalArgumentException("No such %s: %s" | ||
171 | .formatted(type.getName(), qualifiedNameString)); | ||
172 | } | ||
173 | var eObjectDescription = iterator.next(); | ||
174 | if (iterator.hasNext()) { | ||
175 | var qualifiedNameString = qualifiedNameConverter.toString(qualifiedName); | ||
176 | throw new IllegalArgumentException("Ambiguous %s: %s" | ||
177 | .formatted(type.getName(), qualifiedNameString)); | ||
178 | } | ||
179 | var eObject = EcoreUtil.resolve(eObjectDescription.getEObjectOrProxy(), getProblem()); | ||
180 | if (!type.isInstance(eObject)) { | ||
181 | var qualifiedNameString = qualifiedNameConverter.toString(qualifiedName); | ||
182 | throw new IllegalArgumentException("Not a %s: %s" | ||
183 | .formatted(type.getName(), qualifiedNameString)); | ||
184 | } | ||
185 | return type.cast(eObject); | ||
186 | } | 167 | } |
187 | } | 168 | } |
diff --git a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/SemanticsUtils.java b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/SemanticsUtils.java index b195a8e7..b72ba697 100644 --- a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/SemanticsUtils.java +++ b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/SemanticsUtils.java | |||
@@ -8,8 +8,14 @@ package tools.refinery.language.semantics; | |||
8 | import com.google.inject.Inject; | 8 | import com.google.inject.Inject; |
9 | import com.google.inject.Singleton; | 9 | import com.google.inject.Singleton; |
10 | import org.eclipse.emf.ecore.EObject; | 10 | import org.eclipse.emf.ecore.EObject; |
11 | import org.eclipse.emf.ecore.util.EcoreUtil; | ||
11 | import org.eclipse.xtext.naming.IQualifiedNameConverter; | 12 | import org.eclipse.xtext.naming.IQualifiedNameConverter; |
12 | import org.eclipse.xtext.naming.IQualifiedNameProvider; | 13 | import org.eclipse.xtext.naming.IQualifiedNameProvider; |
14 | import org.eclipse.xtext.naming.QualifiedName; | ||
15 | import org.eclipse.xtext.scoping.IScope; | ||
16 | import org.jetbrains.annotations.NotNull; | ||
17 | import org.jetbrains.annotations.Nullable; | ||
18 | import tools.refinery.language.model.problem.Problem; | ||
13 | 19 | ||
14 | import java.util.Optional; | 20 | import java.util.Optional; |
15 | 21 | ||
@@ -28,4 +34,39 @@ public class SemanticsUtils { | |||
28 | } | 34 | } |
29 | return Optional.of(qualifiedNameConverter.toString(qualifiedName)); | 35 | return Optional.of(qualifiedNameConverter.toString(qualifiedName)); |
30 | } | 36 | } |
37 | |||
38 | @Nullable | ||
39 | public <T> T maybeGetElement(Problem problem, IScope scope, QualifiedName qualifiedName, Class<T> type) { | ||
40 | if (qualifiedName == null) { | ||
41 | throw new IllegalArgumentException("Element name must not be null"); | ||
42 | } | ||
43 | var iterator = scope.getElements(qualifiedName).iterator(); | ||
44 | if (!iterator.hasNext()) { | ||
45 | return null; | ||
46 | } | ||
47 | var eObjectDescription = iterator.next(); | ||
48 | if (iterator.hasNext()) { | ||
49 | var qualifiedNameString = qualifiedNameConverter.toString(qualifiedName); | ||
50 | throw new IllegalArgumentException("Ambiguous %s: %s" | ||
51 | .formatted(type.getName(), qualifiedNameString)); | ||
52 | } | ||
53 | var eObject = EcoreUtil.resolve(eObjectDescription.getEObjectOrProxy(), problem); | ||
54 | if (!type.isInstance(eObject)) { | ||
55 | var qualifiedNameString = qualifiedNameConverter.toString(qualifiedName); | ||
56 | throw new IllegalArgumentException("Not a %s: %s" | ||
57 | .formatted(type.getName(), qualifiedNameString)); | ||
58 | } | ||
59 | return type.cast(eObject); | ||
60 | } | ||
61 | |||
62 | @NotNull | ||
63 | public <T> T getElement(Problem problem, IScope scope, QualifiedName qualifiedName, Class<T> type) { | ||
64 | var element = maybeGetElement(problem, scope, qualifiedName, type); | ||
65 | if (element == null) { | ||
66 | var qualifiedNameString = qualifiedNameConverter.toString(qualifiedName); | ||
67 | throw new IllegalArgumentException("No such %s: %s" | ||
68 | .formatted(type.getName(), qualifiedNameString)); | ||
69 | } | ||
70 | return element; | ||
71 | } | ||
31 | } | 72 | } |
diff --git a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/SolutionSerializer.java b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/SolutionSerializer.java new file mode 100644 index 00000000..57af599e --- /dev/null +++ b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/SolutionSerializer.java | |||
@@ -0,0 +1,335 @@ | |||
1 | /* | ||
2 | * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/> | ||
3 | * | ||
4 | * SPDX-License-Identifier: EPL-2.0 | ||
5 | */ | ||
6 | package tools.refinery.language.semantics; | ||
7 | |||
8 | import com.google.inject.Inject; | ||
9 | import com.google.inject.Provider; | ||
10 | import org.eclipse.collections.api.factory.primitive.IntObjectMaps; | ||
11 | import org.eclipse.collections.api.factory.primitive.ObjectIntMaps; | ||
12 | import org.eclipse.collections.api.map.primitive.MutableIntObjectMap; | ||
13 | import org.eclipse.collections.api.map.primitive.MutableObjectIntMap; | ||
14 | import org.eclipse.emf.common.util.URI; | ||
15 | import org.eclipse.emf.ecore.util.EcoreUtil; | ||
16 | import org.eclipse.xtext.naming.IQualifiedNameConverter; | ||
17 | import org.eclipse.xtext.naming.IQualifiedNameProvider; | ||
18 | import org.eclipse.xtext.naming.QualifiedName; | ||
19 | import org.eclipse.xtext.resource.FileExtensionProvider; | ||
20 | import org.eclipse.xtext.resource.IResourceFactory; | ||
21 | import org.eclipse.xtext.resource.XtextResource; | ||
22 | import org.eclipse.xtext.resource.XtextResourceSet; | ||
23 | import org.eclipse.xtext.scoping.IScopeProvider; | ||
24 | import tools.refinery.language.model.problem.*; | ||
25 | import tools.refinery.language.utils.ProblemDesugarer; | ||
26 | import tools.refinery.language.utils.ProblemUtil; | ||
27 | import tools.refinery.store.model.Model; | ||
28 | import tools.refinery.store.reasoning.ReasoningAdapter; | ||
29 | import tools.refinery.store.reasoning.interpretation.PartialInterpretation; | ||
30 | import tools.refinery.store.reasoning.literal.Concreteness; | ||
31 | import tools.refinery.store.reasoning.representation.PartialRelation; | ||
32 | import tools.refinery.store.reasoning.translator.typehierarchy.InferredType; | ||
33 | import tools.refinery.store.reasoning.translator.typehierarchy.TypeHierarchyTranslator; | ||
34 | import tools.refinery.store.representation.TruthValue; | ||
35 | import tools.refinery.store.tuple.Tuple; | ||
36 | |||
37 | import java.io.ByteArrayInputStream; | ||
38 | import java.io.ByteArrayOutputStream; | ||
39 | import java.io.IOException; | ||
40 | import java.util.Locale; | ||
41 | import java.util.Map; | ||
42 | import java.util.TreeMap; | ||
43 | import java.util.TreeSet; | ||
44 | import java.util.function.Function; | ||
45 | import java.util.stream.Collectors; | ||
46 | |||
47 | public class SolutionSerializer { | ||
48 | private String fileExtension; | ||
49 | |||
50 | @Inject | ||
51 | private Provider<XtextResourceSet> resourceSetProvider; | ||
52 | |||
53 | @Inject | ||
54 | private IResourceFactory resourceFactory; | ||
55 | |||
56 | @Inject | ||
57 | private IQualifiedNameProvider qualifiedNameProvider; | ||
58 | |||
59 | @Inject | ||
60 | private IQualifiedNameConverter qualifiedNameConverter; | ||
61 | |||
62 | @Inject | ||
63 | private SemanticsUtils semanticsUtils; | ||
64 | |||
65 | @Inject | ||
66 | private IScopeProvider scopeProvider; | ||
67 | |||
68 | @Inject | ||
69 | private ProblemDesugarer desugarer; | ||
70 | |||
71 | private ProblemTrace trace; | ||
72 | private Model model; | ||
73 | private ReasoningAdapter reasoningAdapter; | ||
74 | private PartialInterpretation<TruthValue, Boolean> existsInterpretation; | ||
75 | private Problem problem; | ||
76 | private final MutableIntObjectMap<Node> nodes = IntObjectMaps.mutable.empty(); | ||
77 | |||
78 | @Inject | ||
79 | public void setFileExtensionProvider(FileExtensionProvider fileExtensionProvider) { | ||
80 | this.fileExtension = fileExtensionProvider.getPrimaryFileExtension(); | ||
81 | } | ||
82 | |||
83 | public Problem serializeSolution(ProblemTrace trace, Model model) { | ||
84 | var uri = URI.createFileURI("__synthetic" + fileExtension); | ||
85 | return serializeSolution(trace, model, uri); | ||
86 | } | ||
87 | |||
88 | public Problem serializeSolution(ProblemTrace trace, Model model, URI uri) { | ||
89 | this.trace = trace; | ||
90 | this.model = model; | ||
91 | reasoningAdapter = model.getAdapter(ReasoningAdapter.class); | ||
92 | existsInterpretation = reasoningAdapter.getPartialInterpretation(Concreteness.CANDIDATE, | ||
93 | ReasoningAdapter.EXISTS_SYMBOL); | ||
94 | var originalProblem = trace.getProblem(); | ||
95 | problem = copyProblem(originalProblem, uri); | ||
96 | problem.getStatements().removeIf(SolutionSerializer::shouldRemoveStatement); | ||
97 | problem.getNodes().removeIf(this::shouldRemoveNode); | ||
98 | addExistsAssertions(); | ||
99 | addClassAssertions(); | ||
100 | addReferenceAssertions(); | ||
101 | return problem; | ||
102 | } | ||
103 | |||
104 | private static boolean shouldRemoveStatement(Statement statement) { | ||
105 | return statement instanceof Assertion || statement instanceof ScopeDeclaration; | ||
106 | } | ||
107 | |||
108 | private boolean shouldRemoveNode(Node newNode) { | ||
109 | var qualifiedName = qualifiedNameProvider.getFullyQualifiedName(newNode); | ||
110 | var scope = scopeProvider.getScope(trace.getProblem(), ProblemPackage.Literals.ASSERTION__RELATION); | ||
111 | var originalNode = semanticsUtils.maybeGetElement(problem, scope, qualifiedName, Node.class); | ||
112 | if (originalNode == null) { | ||
113 | return false; | ||
114 | } | ||
115 | int nodeId = trace.getNodeId(originalNode); | ||
116 | return !isExistingNode(nodeId); | ||
117 | } | ||
118 | |||
119 | private boolean isExistingNode(int nodeId) { | ||
120 | var exists = existsInterpretation.get(Tuple.of(nodeId)); | ||
121 | if (!exists.isConcrete()) { | ||
122 | throw new IllegalStateException("Invalid EXISTS %s for node %d".formatted(exists, nodeId)); | ||
123 | } | ||
124 | return exists.may(); | ||
125 | } | ||
126 | |||
127 | private Problem copyProblem(Problem originalProblem, URI uri) { | ||
128 | var newResourceSet = resourceSetProvider.get(); | ||
129 | if (!fileExtension.equals(uri.fileExtension())) { | ||
130 | uri = uri.appendFileExtension(fileExtension); | ||
131 | } | ||
132 | var newResource = resourceFactory.createResource(uri); | ||
133 | newResourceSet.getResources().add(newResource); | ||
134 | var originalResource = originalProblem.eResource(); | ||
135 | if (originalResource instanceof XtextResource) { | ||
136 | byte[] bytes; | ||
137 | try { | ||
138 | try (var outputStream = new ByteArrayOutputStream()) { | ||
139 | originalResource.save(outputStream, Map.of()); | ||
140 | bytes = outputStream.toByteArray(); | ||
141 | } | ||
142 | try (var inputStream = new ByteArrayInputStream(bytes)) { | ||
143 | newResource.load(inputStream, Map.of()); | ||
144 | } | ||
145 | } catch (IOException e) { | ||
146 | throw new IllegalStateException("Failed to copy problem", e); | ||
147 | } | ||
148 | var contents = newResource.getContents(); | ||
149 | if (!contents.isEmpty() && contents.getFirst() instanceof Problem newProblem) { | ||
150 | return newProblem; | ||
151 | } | ||
152 | throw new IllegalStateException("Invalid contents of copied problem"); | ||
153 | } else { | ||
154 | var newProblem = EcoreUtil.copy(originalProblem); | ||
155 | newResource.getContents().add(newProblem); | ||
156 | return newProblem; | ||
157 | } | ||
158 | } | ||
159 | |||
160 | private Relation findRelation(Relation originalRelation) { | ||
161 | var qualifiedName = qualifiedNameProvider.getFullyQualifiedName(originalRelation); | ||
162 | var scope = scopeProvider.getScope(problem, ProblemPackage.Literals.ASSERTION__RELATION); | ||
163 | return semanticsUtils.getElement(problem, scope, qualifiedName, Relation.class); | ||
164 | } | ||
165 | |||
166 | private Relation findPartialRelation(PartialRelation partialRelation) { | ||
167 | return findRelation(trace.getRelation(partialRelation)); | ||
168 | } | ||
169 | |||
170 | private Node findNode(Node originalNode) { | ||
171 | var qualifiedName = qualifiedNameProvider.getFullyQualifiedName(originalNode); | ||
172 | return findNode(qualifiedName); | ||
173 | } | ||
174 | |||
175 | private Node findNode(String name) { | ||
176 | var qualifiedName = qualifiedNameConverter.toQualifiedName(name); | ||
177 | return findNode(qualifiedName); | ||
178 | } | ||
179 | |||
180 | private Node findNode(QualifiedName qualifiedName) { | ||
181 | var scope = scopeProvider.getScope(problem, ProblemPackage.Literals.NODE_ASSERTION_ARGUMENT__NODE); | ||
182 | return semanticsUtils.maybeGetElement(problem, scope, qualifiedName, Node.class); | ||
183 | } | ||
184 | |||
185 | private void addAssertion(Relation relation, LogicValue value, Node... arguments) { | ||
186 | var assertion = ProblemFactory.eINSTANCE.createAssertion(); | ||
187 | assertion.setRelation(relation); | ||
188 | for (var node : arguments) { | ||
189 | var argument = ProblemFactory.eINSTANCE.createNodeAssertionArgument(); | ||
190 | argument.setNode(node); | ||
191 | assertion.getArguments().add(argument); | ||
192 | } | ||
193 | var logicConstant = ProblemFactory.eINSTANCE.createLogicConstant(); | ||
194 | logicConstant.setLogicValue(value); | ||
195 | assertion.setValue(logicConstant); | ||
196 | problem.getStatements().add(assertion); | ||
197 | } | ||
198 | |||
199 | private void addExistsAssertions() { | ||
200 | var builtinSymbols = desugarer.getBuiltinSymbols(problem) | ||
201 | .orElseThrow(() -> new IllegalStateException("No builtin library in copied problem")); | ||
202 | // Make sure to output exists assertions in a deterministic order. | ||
203 | var sortedNewNodes = new TreeMap<Integer, Node>(); | ||
204 | for (var pair : trace.getNodeTrace().keyValuesView()) { | ||
205 | var originalNode = pair.getOne(); | ||
206 | int nodeId = pair.getTwo(); | ||
207 | var newNode = findNode(originalNode); | ||
208 | // Since all implicit nodes that do not exist has already been remove in serializeSolution, | ||
209 | // we only need to add !exists assertions to ::new nodes (nodes marked as an individual must always exist). | ||
210 | if (ProblemUtil.isNewNode(originalNode)) { | ||
211 | sortedNewNodes.put(nodeId, newNode); | ||
212 | } else { | ||
213 | nodes.put(nodeId, newNode); | ||
214 | } | ||
215 | } | ||
216 | for (var newNode : sortedNewNodes.values()) { | ||
217 | // If a node is a new node of the class, we should replace it with a normal node. | ||
218 | addAssertion(builtinSymbols.exists(), LogicValue.FALSE, newNode); | ||
219 | } | ||
220 | } | ||
221 | |||
222 | private void addClassAssertions() { | ||
223 | var types = trace.getMetamodel().typeHierarchy().getPreservedTypes().keySet().stream() | ||
224 | .collect(Collectors.toMap(Function.identity(), this::findPartialRelation)); | ||
225 | var indexMap = ObjectIntMaps.mutable.empty(); | ||
226 | var cursor = model.getInterpretation(TypeHierarchyTranslator.TYPE_SYMBOL).getAll(); | ||
227 | while (cursor.move()) { | ||
228 | var key = cursor.getKey(); | ||
229 | var nodeId = key.get(0); | ||
230 | if (isExistingNode(nodeId)) { | ||
231 | createNodeAndAssertType(nodeId, cursor.getValue(), types, indexMap); | ||
232 | } | ||
233 | } | ||
234 | } | ||
235 | |||
236 | private void createNodeAndAssertType(int nodeId, InferredType inferredType, Map<PartialRelation, Relation> types, | ||
237 | MutableObjectIntMap<Object> indexMap) { | ||
238 | var candidateTypeSymbol = inferredType.candidateType(); | ||
239 | var candidateRelation = types.get(candidateTypeSymbol); | ||
240 | if (candidateRelation instanceof EnumDeclaration) { | ||
241 | // Type assertions for enum literals are added implicitly. | ||
242 | return; | ||
243 | } | ||
244 | Node node = nodes.get(nodeId); | ||
245 | if (node == null) { | ||
246 | String typeName = candidateRelation.getName(); | ||
247 | if (typeName == null || typeName.isEmpty()) { | ||
248 | typeName = "node"; | ||
249 | } else { | ||
250 | typeName = typeName.substring(0, 1).toLowerCase(Locale.ROOT) + typeName.substring(1); | ||
251 | } | ||
252 | int index = indexMap.getIfAbsent(typeName, 0); | ||
253 | String nodeName; | ||
254 | do { | ||
255 | index++; | ||
256 | nodeName = typeName + index; | ||
257 | } while (findNode(nodeName) != null); | ||
258 | node = ProblemFactory.eINSTANCE.createNode(); | ||
259 | node.setName(nodeName); | ||
260 | problem.getNodes().add(node); | ||
261 | nodes.put(nodeId, node); | ||
262 | } | ||
263 | addAssertion(candidateRelation, LogicValue.TRUE, node); | ||
264 | var typeAnalysisResult = trace.getMetamodel().typeHierarchy().getPreservedTypes().get(candidateTypeSymbol); | ||
265 | for (var subtype : typeAnalysisResult.getDirectSubtypes()) { | ||
266 | var subtypeRelation = types.get(subtype); | ||
267 | addAssertion(subtypeRelation, LogicValue.FALSE, node); | ||
268 | } | ||
269 | } | ||
270 | |||
271 | private void addReferenceAssertions() { | ||
272 | var metamodel = trace.getMetamodel(); | ||
273 | for (var partialRelation : metamodel.containmentHierarchy().keySet()) { | ||
274 | // No need to add a default value, because in a concrete model, each contained node has only a single | ||
275 | // container. | ||
276 | addAssertions(partialRelation); | ||
277 | } | ||
278 | for (var partialRelation : metamodel.directedCrossReferences().keySet()) { | ||
279 | addDefaultAssertion(partialRelation); | ||
280 | addAssertions(partialRelation); | ||
281 | } | ||
282 | // No need to add directed opposite references, because their default value is {@code unknown} and their | ||
283 | // actual value will always be computed from the value of the directed forward reference. | ||
284 | // However, undirected cross-references have to be serialized in both directions due to the default value of | ||
285 | // {@code false}. | ||
286 | for (var partialRelation : metamodel.undirectedCrossReferences().keySet()) { | ||
287 | addDefaultAssertion(partialRelation); | ||
288 | addAssertions(partialRelation); | ||
289 | } | ||
290 | } | ||
291 | |||
292 | private void addAssertions(PartialRelation partialRelation) { | ||
293 | var relation = findPartialRelation(partialRelation); | ||
294 | var cursor = reasoningAdapter.getPartialInterpretation(Concreteness.CANDIDATE, partialRelation).getAll(); | ||
295 | // Make sure to output assertions in a deterministic order. | ||
296 | var sortedTuples = new TreeSet<Tuple>(); | ||
297 | while (cursor.move()) { | ||
298 | var tuple = cursor.getKey(); | ||
299 | var from = nodes.get(tuple.get(0)); | ||
300 | var to = nodes.get(tuple.get(1)); | ||
301 | if (from == null || to == null) { | ||
302 | // One of the endpoints does not exist in the candidate model. | ||
303 | continue; | ||
304 | } | ||
305 | var value = cursor.getValue(); | ||
306 | if (!value.isConcrete()) { | ||
307 | throw new IllegalStateException("Invalid %s %s for tuple %s".formatted(partialRelation, value, tuple)); | ||
308 | } | ||
309 | if (value.may()) { | ||
310 | sortedTuples.add(tuple); | ||
311 | } | ||
312 | } | ||
313 | for (var tuple : sortedTuples) { | ||
314 | var from = nodes.get(tuple.get(0)); | ||
315 | var to = nodes.get(tuple.get(1)); | ||
316 | addAssertion(relation, LogicValue.TRUE, from, to); | ||
317 | } | ||
318 | } | ||
319 | |||
320 | private void addDefaultAssertion(PartialRelation partialRelation) { | ||
321 | var relation = findPartialRelation(partialRelation); | ||
322 | var assertion = ProblemFactory.eINSTANCE.createAssertion(); | ||
323 | assertion.setDefault(true); | ||
324 | assertion.setRelation(relation); | ||
325 | int arity = ProblemUtil.getArity(relation); | ||
326 | for (int i = 0; i < arity; i++) { | ||
327 | var argument = ProblemFactory.eINSTANCE.createWildcardAssertionArgument(); | ||
328 | assertion.getArguments().add(argument); | ||
329 | } | ||
330 | var logicConstant = ProblemFactory.eINSTANCE.createLogicConstant(); | ||
331 | logicConstant.setLogicValue(LogicValue.FALSE); | ||
332 | assertion.setValue(logicConstant); | ||
333 | problem.getStatements().add(assertion); | ||
334 | } | ||
335 | } | ||
diff --git a/subprojects/language-semantics/src/test/java/tools/refinery/language/semantics/SolutionSerializerTest.java b/subprojects/language-semantics/src/test/java/tools/refinery/language/semantics/SolutionSerializerTest.java new file mode 100644 index 00000000..2d759c86 --- /dev/null +++ b/subprojects/language-semantics/src/test/java/tools/refinery/language/semantics/SolutionSerializerTest.java | |||
@@ -0,0 +1,164 @@ | |||
1 | /* | ||
2 | * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/> | ||
3 | * | ||
4 | * SPDX-License-Identifier: EPL-2.0 | ||
5 | */ | ||
6 | package tools.refinery.language.semantics; | ||
7 | |||
8 | import com.google.inject.Inject; | ||
9 | import org.eclipse.xtext.testing.InjectWith; | ||
10 | import org.eclipse.xtext.testing.extensions.InjectionExtension; | ||
11 | import org.junit.jupiter.api.extension.ExtendWith; | ||
12 | import org.junit.jupiter.params.ParameterizedTest; | ||
13 | import org.junit.jupiter.params.provider.Arguments; | ||
14 | import org.junit.jupiter.params.provider.MethodSource; | ||
15 | import tools.refinery.generator.ModelGeneratorFactory; | ||
16 | import tools.refinery.generator.ProblemLoader; | ||
17 | import tools.refinery.language.tests.ProblemInjectorProvider; | ||
18 | |||
19 | import java.io.ByteArrayOutputStream; | ||
20 | import java.io.IOException; | ||
21 | import java.util.Map; | ||
22 | import java.util.stream.Stream; | ||
23 | |||
24 | import static org.hamcrest.MatcherAssert.assertThat; | ||
25 | import static org.hamcrest.Matchers.is; | ||
26 | |||
27 | @ExtendWith(InjectionExtension.class) | ||
28 | @InjectWith(ProblemInjectorProvider.class) | ||
29 | class SolutionSerializerTest { | ||
30 | @Inject | ||
31 | ProblemLoader loader; | ||
32 | |||
33 | @Inject | ||
34 | ModelGeneratorFactory generatorFactory; | ||
35 | |||
36 | @Inject | ||
37 | SolutionSerializer serializer; | ||
38 | |||
39 | @ParameterizedTest | ||
40 | @MethodSource | ||
41 | void solutionSerializerTest(String prefix, String input, String expectedOutput) throws IOException { | ||
42 | var problem = loader.loadString(prefix + "\n" + input); | ||
43 | var generator = generatorFactory.createGenerator(problem); | ||
44 | generator.generate(); | ||
45 | var solution = serializer.serializeSolution(generator.getProblemTrace(), generator.getModel()); | ||
46 | String actualOutput; | ||
47 | try (var outputStream = new ByteArrayOutputStream()) { | ||
48 | solution.eResource().save(outputStream, Map.of()); | ||
49 | actualOutput = outputStream.toString(); | ||
50 | } | ||
51 | assertThat(actualOutput, is(prefix + "\n" + expectedOutput)); | ||
52 | } | ||
53 | |||
54 | static Stream<Arguments> solutionSerializerTest() { | ||
55 | return Stream.of(Arguments.of(""" | ||
56 | class Foo. | ||
57 | """, """ | ||
58 | scope Foo = 3. | ||
59 | """, """ | ||
60 | !exists(Foo::new). | ||
61 | Foo(foo1). | ||
62 | Foo(foo2). | ||
63 | Foo(foo3). | ||
64 | """), Arguments.of(""" | ||
65 | class Foo { | ||
66 | contains Bar[2] bars | ||
67 | } | ||
68 | |||
69 | class Bar. | ||
70 | """, """ | ||
71 | scope Foo = 1. | ||
72 | """, """ | ||
73 | !exists(Foo::new). | ||
74 | !exists(Bar::new). | ||
75 | Foo(foo1). | ||
76 | Bar(bar1). | ||
77 | Bar(bar2). | ||
78 | bars(foo1, bar1). | ||
79 | bars(foo1, bar2). | ||
80 | """), Arguments.of(""" | ||
81 | class Foo { | ||
82 | Bar[2] bars opposite foo | ||
83 | } | ||
84 | |||
85 | class Bar { | ||
86 | Foo[1] foo opposite bars | ||
87 | } | ||
88 | """, """ | ||
89 | scope Foo = 1, Bar = 2. | ||
90 | """, """ | ||
91 | !exists(Foo::new). | ||
92 | !exists(Bar::new). | ||
93 | Foo(foo1). | ||
94 | Bar(bar1). | ||
95 | Bar(bar2). | ||
96 | default !bars(*, *). | ||
97 | bars(foo1, bar1). | ||
98 | bars(foo1, bar2). | ||
99 | """), Arguments.of(""" | ||
100 | class Person { | ||
101 | Person[2] friend opposite friend | ||
102 | } | ||
103 | """, """ | ||
104 | friend(a, b). | ||
105 | friend(a, c). | ||
106 | friend(b, c). | ||
107 | |||
108 | scope Person += 0. | ||
109 | """, """ | ||
110 | !exists(Person::new). | ||
111 | Person(a). | ||
112 | Person(b). | ||
113 | Person(c). | ||
114 | default !friend(*, *). | ||
115 | friend(a, b). | ||
116 | friend(a, c). | ||
117 | friend(b, a). | ||
118 | friend(b, c). | ||
119 | friend(c, a). | ||
120 | friend(c, b). | ||
121 | """), Arguments.of(""" | ||
122 | class Foo { | ||
123 | Bar bar | ||
124 | } | ||
125 | |||
126 | enum Bar { | ||
127 | BAR_A, | ||
128 | BAR_B | ||
129 | } | ||
130 | """, """ | ||
131 | bar(foo, BAR_A). | ||
132 | |||
133 | scope Foo += 0. | ||
134 | """, """ | ||
135 | !exists(Foo::new). | ||
136 | Foo(foo). | ||
137 | default !bar(*, *). | ||
138 | bar(foo, BAR_A). | ||
139 | """), Arguments.of(""" | ||
140 | class Foo. | ||
141 | class Bar extends Foo. | ||
142 | """, """ | ||
143 | scope Foo = 1, Bar = 0. | ||
144 | """, """ | ||
145 | !exists(Foo::new). | ||
146 | !exists(Bar::new). | ||
147 | Foo(foo1). | ||
148 | !Bar(foo1). | ||
149 | """), Arguments.of(""" | ||
150 | class Foo { | ||
151 | Foo[] ref | ||
152 | } | ||
153 | """, """ | ||
154 | ref(a, b). | ||
155 | !exists(b). | ||
156 | |||
157 | scope Foo += 0. | ||
158 | """, """ | ||
159 | !exists(Foo::new). | ||
160 | Foo(a). | ||
161 | default !ref(*, *). | ||
162 | """)); | ||
163 | } | ||
164 | } | ||
diff --git a/subprojects/language/src/main/java/tools/refinery/language/formatting2/ProblemFormatter.java b/subprojects/language/src/main/java/tools/refinery/language/formatting2/ProblemFormatter.java index 55a5ac20..770a1a19 100644 --- a/subprojects/language/src/main/java/tools/refinery/language/formatting2/ProblemFormatter.java +++ b/subprojects/language/src/main/java/tools/refinery/language/formatting2/ProblemFormatter.java | |||
@@ -75,6 +75,16 @@ public class ProblemFormatter extends AbstractJavaFormatter { | |||
75 | } | 75 | } |
76 | } | 76 | } |
77 | 77 | ||
78 | protected void format(EnumDeclaration enumDeclaration, IFormattableDocument doc) { | ||
79 | surroundNewLines(doc, enumDeclaration, this::twoNewLines); | ||
80 | var region = regionFor(enumDeclaration); | ||
81 | doc.append(region.keyword("enum"), this::oneSpace); | ||
82 | doc.prepend(region.keyword("{"), this::oneSpace); | ||
83 | doc.append(region.keyword("{"), it -> it.setNewLines(1, 1, 2)); | ||
84 | doc.prepend(region.keyword("}"), it -> it.setNewLines(1, 1, 2)); | ||
85 | doc.prepend(region.keyword("."), this::noSpace); | ||
86 | } | ||
87 | |||
78 | protected void format(PredicateDefinition predicateDefinition, IFormattableDocument doc) { | 88 | protected void format(PredicateDefinition predicateDefinition, IFormattableDocument doc) { |
79 | surroundNewLines(doc, predicateDefinition, this::twoNewLines); | 89 | surroundNewLines(doc, predicateDefinition, this::twoNewLines); |
80 | var region = regionFor(predicateDefinition); | 90 | var region = regionFor(predicateDefinition); |
@@ -151,14 +161,14 @@ public class ProblemFormatter extends AbstractJavaFormatter { | |||
151 | } | 161 | } |
152 | 162 | ||
153 | protected void surroundNewLines(IFormattableDocument doc, EObject eObject, | 163 | protected void surroundNewLines(IFormattableDocument doc, EObject eObject, |
154 | Procedure1<? super IHiddenRegionFormatter> init) { | 164 | Procedure1<? super IHiddenRegionFormatter> init) { |
155 | var region = doc.getRequest().getTextRegionAccess().regionForEObject(eObject); | 165 | var region = doc.getRequest().getTextRegionAccess().regionForEObject(eObject); |
156 | preprendNewLines(doc, region, init); | 166 | preprendNewLines(doc, region, init); |
157 | appendNewLines(doc, region, init); | 167 | appendNewLines(doc, region, init); |
158 | } | 168 | } |
159 | 169 | ||
160 | protected void preprendNewLines(IFormattableDocument doc, ISequentialRegion region, | 170 | protected void preprendNewLines(IFormattableDocument doc, ISequentialRegion region, |
161 | Procedure1<? super IHiddenRegionFormatter> init) { | 171 | Procedure1<? super IHiddenRegionFormatter> init) { |
162 | if (region == null) { | 172 | if (region == null) { |
163 | return; | 173 | return; |
164 | } | 174 | } |
@@ -174,7 +184,7 @@ public class ProblemFormatter extends AbstractJavaFormatter { | |||
174 | } | 184 | } |
175 | 185 | ||
176 | protected void appendNewLines(IFormattableDocument doc, ISequentialRegion region, | 186 | protected void appendNewLines(IFormattableDocument doc, ISequentialRegion region, |
177 | Procedure1<? super IHiddenRegionFormatter> init) { | 187 | Procedure1<? super IHiddenRegionFormatter> init) { |
178 | if (region == null) { | 188 | if (region == null) { |
179 | return; | 189 | return; |
180 | } | 190 | } |
diff --git a/subprojects/language/src/main/java/tools/refinery/language/serializer/PreferShortAssertionsProblemSemanticSequencer.java b/subprojects/language/src/main/java/tools/refinery/language/serializer/PreferShortAssertionsProblemSemanticSequencer.java index b9cafbc2..3432b2d8 100644 --- a/subprojects/language/src/main/java/tools/refinery/language/serializer/PreferShortAssertionsProblemSemanticSequencer.java +++ b/subprojects/language/src/main/java/tools/refinery/language/serializer/PreferShortAssertionsProblemSemanticSequencer.java | |||
@@ -21,8 +21,7 @@ public class PreferShortAssertionsProblemSemanticSequencer extends ProblemSemant | |||
21 | 21 | ||
22 | @Override | 22 | @Override |
23 | protected void sequence_Assertion(ISerializationContext context, Assertion semanticObject) { | 23 | protected void sequence_Assertion(ISerializationContext context, Assertion semanticObject) { |
24 | if (semanticObject.isDefault() || | 24 | if (!(semanticObject.getValue() instanceof LogicConstant logicConstant) || |
25 | !(semanticObject.getValue() instanceof LogicConstant logicConstant) || | ||
26 | logicConstant.getLogicValue() == LogicValue.ERROR) { | 25 | logicConstant.getLogicValue() == LogicValue.ERROR) { |
27 | super.sequence_Assertion(context, semanticObject); | 26 | super.sequence_Assertion(context, semanticObject); |
28 | return; | 27 | return; |
@@ -39,6 +38,9 @@ public class PreferShortAssertionsProblemSemanticSequencer extends ProblemSemant | |||
39 | } | 38 | } |
40 | var feeder = createSequencerFeeder(context, semanticObject); | 39 | var feeder = createSequencerFeeder(context, semanticObject); |
41 | var access = grammarAccess.getAssertionAccess(); | 40 | var access = grammarAccess.getAssertionAccess(); |
41 | if (semanticObject.isDefault()) { | ||
42 | feeder.accept(access.getDefaultDefaultKeyword_0_0()); | ||
43 | } | ||
42 | feeder.accept(access.getValueShortLogicConstantParserRuleCall_1_1_0_0(), logicConstant); | 44 | feeder.accept(access.getValueShortLogicConstantParserRuleCall_1_1_0_0(), logicConstant); |
43 | feeder.accept(access.getRelationRelationQualifiedNameParserRuleCall_1_1_1_0_1(), semanticObject.getRelation()); | 45 | feeder.accept(access.getRelationRelationQualifiedNameParserRuleCall_1_1_1_0_1(), semanticObject.getRelation()); |
44 | var iterator = semanticObject.getArguments().iterator(); | 46 | var iterator = semanticObject.getArguments().iterator(); |
diff --git a/subprojects/language/src/test/java/tools/refinery/language/tests/serializer/ProblemSerializerTest.java b/subprojects/language/src/test/java/tools/refinery/language/tests/serializer/ProblemSerializerTest.java index 9f4f2bbf..4a3a9ac2 100644 --- a/subprojects/language/src/test/java/tools/refinery/language/tests/serializer/ProblemSerializerTest.java +++ b/subprojects/language/src/test/java/tools/refinery/language/tests/serializer/ProblemSerializerTest.java | |||
@@ -74,8 +74,8 @@ class ProblemSerializerTest { | |||
74 | } | 74 | } |
75 | 75 | ||
76 | @ParameterizedTest | 76 | @ParameterizedTest |
77 | @MethodSource | 77 | @MethodSource("assertionTest") |
78 | void defaultAssertionTest(LogicValue value, String valueAsString) { | 78 | void defaultAssertionTest(LogicValue value, String serializedAssertion) { |
79 | var pred = createPred(); | 79 | var pred = createPred(); |
80 | var node = ProblemFactory.eINSTANCE.createNode(); | 80 | var node = ProblemFactory.eINSTANCE.createNode(); |
81 | node.setName("a"); | 81 | node.setName("a"); |
@@ -88,12 +88,7 @@ class ProblemSerializerTest { | |||
88 | pred foo(node p). | 88 | pred foo(node p). |
89 | 89 | ||
90 | indiv a. | 90 | indiv a. |
91 | default foo(a):\040""" + valueAsString + ".\n"); | 91 | default\040""" + serializedAssertion + "\n"); |
92 | } | ||
93 | |||
94 | static Stream<Arguments> defaultAssertionTest() { | ||
95 | return Stream.of(Arguments.of(LogicValue.TRUE, "true"), Arguments.of(LogicValue.FALSE, "false"), | ||
96 | Arguments.of(LogicValue.UNKNOWN, "unknown"), Arguments.of(LogicValue.ERROR, "error")); | ||
97 | } | 92 | } |
98 | 93 | ||
99 | @Test | 94 | @Test |
@@ -233,19 +228,14 @@ class ProblemSerializerTest { | |||
233 | } | 228 | } |
234 | 229 | ||
235 | private void assertSerializedResult(String expected) { | 230 | private void assertSerializedResult(String expected) { |
236 | var outputStream = new ByteArrayOutputStream(); | 231 | String problemString; |
237 | try { | 232 | try (var outputStream = new ByteArrayOutputStream()) { |
238 | resource.save(outputStream, Map.of()); | 233 | resource.save(outputStream, Map.of()); |
239 | } catch (IOException e) { | 234 | problemString = outputStream.toString(); |
240 | throw new AssertionError("Failed to serialize problem", e); | 235 | } catch (IOException e) { |
241 | } finally { | 236 | throw new AssertionError("Failed to serialize problem", e); |
242 | try { | 237 | } |
243 | outputStream.close(); | 238 | // Nothing to handle in a test. |
244 | } catch (IOException e) { | ||
245 | // Nothing to handle in a test. | ||
246 | } | ||
247 | } | ||
248 | var problemString = outputStream.toString(); | ||
249 | 239 | ||
250 | assertThat(problemString.replace("\r\n", "\n"), equalTo(expected.replace("\r\n", "\n"))); | 240 | assertThat(problemString.replace("\r\n", "\n"), equalTo(expected.replace("\r\n", "\n"))); |
251 | } | 241 | } |