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 /subprojects/language-semantics | |
parent | refactor(language): use file extension provider (diff) | |
download | refinery-c65275be9fce0fbba70094c754690a8bd9228ab4.tar.gz refinery-c65275be9fce0fbba70094c754690a8bd9228ab4.tar.zst refinery-c65275be9fce0fbba70094c754690a8bd9228ab4.zip |
feat: solution serializer
Diffstat (limited to 'subprojects/language-semantics')
5 files changed, 543 insertions, 21 deletions
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 | } | ||