diff options
Diffstat (limited to 'subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/SolutionSerializer.java')
-rw-r--r-- | subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/SolutionSerializer.java | 126 |
1 files changed, 80 insertions, 46 deletions
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 index 09ba34fc..377a66f3 100644 --- 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 | |||
@@ -10,15 +10,17 @@ import com.google.inject.Provider; | |||
10 | import org.eclipse.collections.api.factory.primitive.IntObjectMaps; | 10 | import org.eclipse.collections.api.factory.primitive.IntObjectMaps; |
11 | import org.eclipse.collections.api.map.primitive.MutableIntObjectMap; | 11 | import org.eclipse.collections.api.map.primitive.MutableIntObjectMap; |
12 | import org.eclipse.emf.common.util.URI; | 12 | import org.eclipse.emf.common.util.URI; |
13 | import org.eclipse.emf.ecore.EObject; | ||
14 | import org.eclipse.emf.ecore.resource.Resource; | ||
13 | import org.eclipse.emf.ecore.util.EcoreUtil; | 15 | import org.eclipse.emf.ecore.util.EcoreUtil; |
14 | import org.eclipse.xtext.naming.IQualifiedNameProvider; | 16 | import org.eclipse.xtext.naming.IQualifiedNameProvider; |
15 | import org.eclipse.xtext.naming.QualifiedName; | 17 | import org.eclipse.xtext.naming.QualifiedName; |
16 | import org.eclipse.xtext.resource.FileExtensionProvider; | ||
17 | import org.eclipse.xtext.resource.IResourceFactory; | 18 | import org.eclipse.xtext.resource.IResourceFactory; |
18 | import org.eclipse.xtext.resource.XtextResource; | 19 | import org.eclipse.xtext.resource.XtextResource; |
19 | import org.eclipse.xtext.resource.XtextResourceSet; | 20 | import org.eclipse.xtext.resource.XtextResourceSet; |
20 | import org.eclipse.xtext.scoping.IScopeProvider; | 21 | import org.eclipse.xtext.scoping.IScopeProvider; |
21 | import tools.refinery.language.model.problem.*; | 22 | import tools.refinery.language.model.problem.*; |
23 | import tools.refinery.language.naming.NamingUtil; | ||
22 | import tools.refinery.language.utils.ProblemDesugarer; | 24 | import tools.refinery.language.utils.ProblemDesugarer; |
23 | import tools.refinery.language.utils.ProblemUtil; | 25 | import tools.refinery.language.utils.ProblemUtil; |
24 | import tools.refinery.store.model.Model; | 26 | import tools.refinery.store.model.Model; |
@@ -34,15 +36,11 @@ import tools.refinery.store.tuple.Tuple; | |||
34 | import java.io.ByteArrayInputStream; | 36 | import java.io.ByteArrayInputStream; |
35 | import java.io.ByteArrayOutputStream; | 37 | import java.io.ByteArrayOutputStream; |
36 | import java.io.IOException; | 38 | import java.io.IOException; |
37 | import java.util.Map; | 39 | import java.util.*; |
38 | import java.util.TreeMap; | ||
39 | import java.util.TreeSet; | ||
40 | import java.util.function.Function; | 40 | import java.util.function.Function; |
41 | import java.util.stream.Collectors; | 41 | import java.util.stream.Collectors; |
42 | 42 | ||
43 | public class SolutionSerializer { | 43 | public class SolutionSerializer { |
44 | private String fileExtension; | ||
45 | |||
46 | @Inject | 44 | @Inject |
47 | private Provider<XtextResourceSet> resourceSetProvider; | 45 | private Provider<XtextResourceSet> resourceSetProvider; |
48 | 46 | ||
@@ -68,16 +66,17 @@ public class SolutionSerializer { | |||
68 | private Model model; | 66 | private Model model; |
69 | private ReasoningAdapter reasoningAdapter; | 67 | private ReasoningAdapter reasoningAdapter; |
70 | private PartialInterpretation<TruthValue, Boolean> existsInterpretation; | 68 | private PartialInterpretation<TruthValue, Boolean> existsInterpretation; |
69 | private Resource originalResource; | ||
70 | private Problem originalProblem; | ||
71 | private QualifiedName originalProblemName; | ||
71 | private Problem problem; | 72 | private Problem problem; |
73 | private QualifiedName newProblemName; | ||
74 | private NodeDeclaration nodeDeclaration; | ||
72 | private final MutableIntObjectMap<Node> nodes = IntObjectMaps.mutable.empty(); | 75 | private final MutableIntObjectMap<Node> nodes = IntObjectMaps.mutable.empty(); |
73 | 76 | ||
74 | @Inject | ||
75 | public void setFileExtensionProvider(FileExtensionProvider fileExtensionProvider) { | ||
76 | this.fileExtension = fileExtensionProvider.getPrimaryFileExtension(); | ||
77 | } | ||
78 | |||
79 | public Problem serializeSolution(ProblemTrace trace, Model model) { | 77 | public Problem serializeSolution(ProblemTrace trace, Model model) { |
80 | var uri = URI.createFileURI("__synthetic" + fileExtension); | 78 | var uri = URI.createURI("__solution_%s.%s".formatted(UUID.randomUUID().toString().replace('-', '_'), |
79 | ProblemUtil.MODULE_EXTENSION)); | ||
81 | return serializeSolution(trace, model, uri); | 80 | return serializeSolution(trace, model, uri); |
82 | } | 81 | } |
83 | 82 | ||
@@ -87,14 +86,26 @@ public class SolutionSerializer { | |||
87 | reasoningAdapter = model.getAdapter(ReasoningAdapter.class); | 86 | reasoningAdapter = model.getAdapter(ReasoningAdapter.class); |
88 | existsInterpretation = reasoningAdapter.getPartialInterpretation(Concreteness.CANDIDATE, | 87 | existsInterpretation = reasoningAdapter.getPartialInterpretation(Concreteness.CANDIDATE, |
89 | ReasoningAdapter.EXISTS_SYMBOL); | 88 | ReasoningAdapter.EXISTS_SYMBOL); |
90 | var originalProblem = trace.getProblem(); | 89 | originalProblem = trace.getProblem(); |
90 | originalProblemName = qualifiedNameProvider.getFullyQualifiedName(originalProblem); | ||
91 | problem = copyProblem(originalProblem, uri); | 91 | problem = copyProblem(originalProblem, uri); |
92 | problem.setKind(ProblemUtil.getDefaultModuleKind(uri)); | ||
93 | problem.setExplicitKind(false); | ||
94 | problem.setName(null); | ||
95 | newProblemName = qualifiedNameProvider.getFullyQualifiedName(originalProblem); | ||
92 | problem.getStatements().removeIf(SolutionSerializer::shouldRemoveStatement); | 96 | problem.getStatements().removeIf(SolutionSerializer::shouldRemoveStatement); |
93 | problem.getNodes().removeIf(this::shouldRemoveNode); | 97 | removeNonExistentImplicitNodes(); |
98 | nodeDeclaration = ProblemFactory.eINSTANCE.createNodeDeclaration(); | ||
99 | nodeDeclaration.setKind(NodeKind.NODE); | ||
100 | nodeDeclaration.getNodes().addAll(problem.getNodes()); | ||
101 | problem.getStatements().add(nodeDeclaration); | ||
94 | nameProvider.setProblem(problem); | 102 | nameProvider.setProblem(problem); |
95 | addExistsAssertions(); | 103 | addExistsAssertions(); |
96 | addClassAssertions(); | 104 | addClassAssertions(); |
97 | addReferenceAssertions(); | 105 | addReferenceAssertions(); |
106 | if (nodeDeclaration.getNodes().isEmpty()) { | ||
107 | problem.getStatements().remove(nodeDeclaration); | ||
108 | } | ||
98 | return problem; | 109 | return problem; |
99 | } | 110 | } |
100 | 111 | ||
@@ -102,15 +113,28 @@ public class SolutionSerializer { | |||
102 | return statement instanceof Assertion || statement instanceof ScopeDeclaration; | 113 | return statement instanceof Assertion || statement instanceof ScopeDeclaration; |
103 | } | 114 | } |
104 | 115 | ||
105 | private boolean shouldRemoveNode(Node newNode) { | 116 | private void removeNonExistentImplicitNodes() { |
106 | var qualifiedName = qualifiedNameProvider.getFullyQualifiedName(newNode); | 117 | var originalImplicitNodes = originalProblem.getNodes(); |
107 | var scope = scopeProvider.getScope(trace.getProblem(), ProblemPackage.Literals.ASSERTION__RELATION); | 118 | var newImplicitNodes = problem.getNodes(); |
108 | var originalNode = semanticsUtils.maybeGetElement(problem, scope, qualifiedName, Node.class); | 119 | if (newImplicitNodes.size() != originalImplicitNodes.size()) { |
109 | if (originalNode == null) { | 120 | throw new IllegalStateException("Expected %d implicit nodes in problem, but got %d after copying" |
110 | return false; | 121 | .formatted(originalImplicitNodes.size(), newImplicitNodes.size())); |
122 | } | ||
123 | var iterator = newImplicitNodes.iterator(); | ||
124 | for (var originalNode : originalImplicitNodes) { | ||
125 | if (!iterator.hasNext()) { | ||
126 | throw new AssertionError("Unexpected end of copied implicit node list"); | ||
127 | } | ||
128 | var newNode = iterator.next(); | ||
129 | if (!Objects.equals(originalNode.getName(), newNode.getName())) { | ||
130 | throw new IllegalStateException("Expected copy of '%s' to have the same name, got '%s' instead" | ||
131 | .formatted(originalNode.getName(), newNode.getName())); | ||
132 | } | ||
133 | int nodeId = trace.getNodeId(originalNode); | ||
134 | if (!isExistingNode(nodeId)) { | ||
135 | iterator.remove(); | ||
136 | } | ||
111 | } | 137 | } |
112 | int nodeId = trace.getNodeId(originalNode); | ||
113 | return !isExistingNode(nodeId); | ||
114 | } | 138 | } |
115 | 139 | ||
116 | private boolean isExistingNode(int nodeId) { | 140 | private boolean isExistingNode(int nodeId) { |
@@ -122,13 +146,10 @@ public class SolutionSerializer { | |||
122 | } | 146 | } |
123 | 147 | ||
124 | private Problem copyProblem(Problem originalProblem, URI uri) { | 148 | private Problem copyProblem(Problem originalProblem, URI uri) { |
125 | var newResourceSet = resourceSetProvider.get(); | 149 | originalResource = originalProblem.eResource(); |
126 | if (!fileExtension.equals(uri.fileExtension())) { | 150 | var resourceSet = originalResource.getResourceSet(); |
127 | uri = uri.appendFileExtension(fileExtension); | ||
128 | } | ||
129 | var newResource = resourceFactory.createResource(uri); | 151 | var newResource = resourceFactory.createResource(uri); |
130 | newResourceSet.getResources().add(newResource); | 152 | resourceSet.getResources().add(newResource); |
131 | var originalResource = originalProblem.eResource(); | ||
132 | if (originalResource instanceof XtextResource) { | 153 | if (originalResource instanceof XtextResource) { |
133 | byte[] bytes; | 154 | byte[] bytes; |
134 | try { | 155 | try { |
@@ -143,6 +164,7 @@ public class SolutionSerializer { | |||
143 | throw new IllegalStateException("Failed to copy problem", e); | 164 | throw new IllegalStateException("Failed to copy problem", e); |
144 | } | 165 | } |
145 | var contents = newResource.getContents(); | 166 | var contents = newResource.getContents(); |
167 | EcoreUtil.resolveAll(newResource); | ||
146 | if (!contents.isEmpty() && contents.getFirst() instanceof Problem newProblem) { | 168 | if (!contents.isEmpty() && contents.getFirst() instanceof Problem newProblem) { |
147 | return newProblem; | 169 | return newProblem; |
148 | } | 170 | } |
@@ -154,10 +176,24 @@ public class SolutionSerializer { | |||
154 | } | 176 | } |
155 | } | 177 | } |
156 | 178 | ||
179 | private QualifiedName getConvertedName(EObject original) { | ||
180 | var qualifiedName = qualifiedNameProvider.getFullyQualifiedName(original); | ||
181 | if (originalProblemName != null && qualifiedName.startsWith(originalProblemName)) { | ||
182 | qualifiedName = qualifiedName.skipFirst(originalProblemName.getSegmentCount()); | ||
183 | } | ||
184 | if (newProblemName != null) { | ||
185 | qualifiedName = newProblemName.append(qualifiedName); | ||
186 | } | ||
187 | return NamingUtil.addRootPrefix(qualifiedName); | ||
188 | } | ||
189 | |||
157 | private Relation findRelation(Relation originalRelation) { | 190 | private Relation findRelation(Relation originalRelation) { |
158 | var qualifiedName = qualifiedNameProvider.getFullyQualifiedName(originalRelation); | 191 | if (originalRelation.eResource() != originalResource) { |
159 | var scope = scopeProvider.getScope(problem, ProblemPackage.Literals.ASSERTION__RELATION); | 192 | return originalRelation; |
160 | return semanticsUtils.getElement(problem, scope, qualifiedName, Relation.class); | 193 | } |
194 | var qualifiedName = getConvertedName(originalRelation); | ||
195 | return semanticsUtils.getLocalElement(problem, qualifiedName, Relation.class, | ||
196 | ProblemPackage.Literals.RELATION); | ||
161 | } | 197 | } |
162 | 198 | ||
163 | private Relation findPartialRelation(PartialRelation partialRelation) { | 199 | private Relation findPartialRelation(PartialRelation partialRelation) { |
@@ -165,13 +201,11 @@ public class SolutionSerializer { | |||
165 | } | 201 | } |
166 | 202 | ||
167 | private Node findNode(Node originalNode) { | 203 | private Node findNode(Node originalNode) { |
168 | var qualifiedName = qualifiedNameProvider.getFullyQualifiedName(originalNode); | 204 | if (originalNode.eResource() != originalResource) { |
169 | return findNode(qualifiedName); | 205 | return originalNode; |
170 | } | 206 | } |
171 | 207 | var qualifiedName = getConvertedName(originalNode); | |
172 | private Node findNode(QualifiedName qualifiedName) { | 208 | return semanticsUtils.maybeGetLocalElement(problem, qualifiedName, Node.class, ProblemPackage.Literals.NODE); |
173 | var scope = scopeProvider.getScope(problem, ProblemPackage.Literals.NODE_ASSERTION_ARGUMENT__NODE); | ||
174 | return semanticsUtils.maybeGetElement(problem, scope, qualifiedName, Node.class); | ||
175 | } | 209 | } |
176 | 210 | ||
177 | private void addAssertion(Relation relation, LogicValue value, Node... arguments) { | 211 | private void addAssertion(Relation relation, LogicValue value, Node... arguments) { |
@@ -189,17 +223,17 @@ public class SolutionSerializer { | |||
189 | } | 223 | } |
190 | 224 | ||
191 | private void addExistsAssertions() { | 225 | private void addExistsAssertions() { |
192 | var builtinSymbols = desugarer.getBuiltinSymbols(problem) | 226 | var builtinSymbols = desugarer.getBuiltinSymbols(problem).orElseThrow(() -> new IllegalStateException("No " + |
193 | .orElseThrow(() -> new IllegalStateException("No builtin library in copied problem")); | 227 | "builtin library in copied problem")); |
194 | // Make sure to output exists assertions in a deterministic order. | 228 | // Make sure to output exists assertions in a deterministic order. |
195 | var sortedNewNodes = new TreeMap<Integer, Node>(); | 229 | var sortedNewNodes = new TreeMap<Integer, Node>(); |
196 | for (var pair : trace.getNodeTrace().keyValuesView()) { | 230 | for (var pair : trace.getNodeTrace().keyValuesView()) { |
197 | var originalNode = pair.getOne(); | 231 | var originalNode = pair.getOne(); |
198 | int nodeId = pair.getTwo(); | 232 | int nodeId = pair.getTwo(); |
199 | var newNode = findNode(originalNode); | 233 | var newNode = findNode(originalNode); |
200 | // Since all implicit nodes that do not exist has already been remove in serializeSolution, | 234 | // Since all implicit nodes that do not exist has already been removed in serializeSolution, |
201 | // we only need to add !exists assertions to ::new nodes (nodes marked as an individual must always exist). | 235 | // we only need to add !exists assertions to ::new nodes and explicitly declared nodes that do not exist. |
202 | if (ProblemUtil.isNewNode(originalNode)) { | 236 | if (ProblemUtil.isMultiNode(originalNode) || (ProblemUtil.isDeclaredNode(originalNode) && !isExistingNode(nodeId))) { |
203 | sortedNewNodes.put(nodeId, newNode); | 237 | sortedNewNodes.put(nodeId, newNode); |
204 | } else { | 238 | } else { |
205 | nodes.put(nodeId, newNode); | 239 | nodes.put(nodeId, newNode); |
@@ -212,8 +246,8 @@ public class SolutionSerializer { | |||
212 | } | 246 | } |
213 | 247 | ||
214 | private void addClassAssertions() { | 248 | private void addClassAssertions() { |
215 | var types = trace.getMetamodel().typeHierarchy().getPreservedTypes().keySet().stream() | 249 | var types = |
216 | .collect(Collectors.toMap(Function.identity(), this::findPartialRelation)); | 250 | trace.getMetamodel().typeHierarchy().getPreservedTypes().keySet().stream().collect(Collectors.toMap(Function.identity(), this::findPartialRelation)); |
217 | var cursor = model.getInterpretation(TypeHierarchyTranslator.TYPE_SYMBOL).getAll(); | 251 | var cursor = model.getInterpretation(TypeHierarchyTranslator.TYPE_SYMBOL).getAll(); |
218 | while (cursor.move()) { | 252 | while (cursor.move()) { |
219 | var key = cursor.getKey(); | 253 | var key = cursor.getKey(); |
@@ -237,7 +271,7 @@ public class SolutionSerializer { | |||
237 | var nodeName = nameProvider.getNextName(typeName); | 271 | var nodeName = nameProvider.getNextName(typeName); |
238 | node = ProblemFactory.eINSTANCE.createNode(); | 272 | node = ProblemFactory.eINSTANCE.createNode(); |
239 | node.setName(nodeName); | 273 | node.setName(nodeName); |
240 | problem.getNodes().add(node); | 274 | nodeDeclaration.getNodes().add(node); |
241 | nodes.put(nodeId, node); | 275 | nodes.put(nodeId, node); |
242 | } | 276 | } |
243 | addAssertion(candidateRelation, LogicValue.TRUE, node); | 277 | addAssertion(candidateRelation, LogicValue.TRUE, node); |