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 @@
     <eStructuralFeatures xsi:type="ecore:EAttribute" name="kind" eType="#//ReferenceKind"/>
     <eStructuralFeatures xsi:type="ecore:EReference" name="referenceType" eType="#//Relation"/>
     <eStructuralFeatures xsi:type="ecore:EReference" name="invalidMultiplicity" eType="#//Relation"
-        containment="true"/>
+        transient="true" containment="true"/>
   </eClassifiers>
   <eClassifiers xsi:type="ecore:EClass" name="NamedElement" abstract="true">
     <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 {
         api(project(":refinery-store-reasoning"))
         implementation(project(":refinery-store-reasoning-scope"))
         runtimeOnly(libs.eclipseCollections)
+        testImplementation(project(":refinery-generator"))
         testImplementation(project(":refinery-store-dse-visualization"))
         testImplementation(project(":refinery-store-query-interpreter"))
         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;
 import org.eclipse.collections.api.factory.primitive.ObjectIntMaps;
 import org.eclipse.collections.api.map.primitive.MutableObjectIntMap;
 import org.eclipse.collections.api.map.primitive.ObjectIntMap;
-import org.eclipse.emf.ecore.util.EcoreUtil;
 import org.eclipse.xtext.naming.IQualifiedNameConverter;
 import org.eclipse.xtext.naming.QualifiedName;
 import org.eclipse.xtext.scoping.IScope;
@@ -28,7 +27,7 @@ import java.util.HashMap;
 import java.util.LinkedHashMap;
 import java.util.Map;
 
-public class ProblemTraceImpl implements ProblemTrace {
+class ProblemTraceImpl implements ProblemTrace {
         @Inject
         private IQualifiedNameConverter qualifiedNameConverter;
 
@@ -164,24 +163,6 @@ public class ProblemTraceImpl implements ProblemTrace {
         }
 
         private <T> T getElement(IScope scope, QualifiedName qualifiedName, Class<T> type) {
-                var iterator = scope.getElements(qualifiedName).iterator();
-                if (!iterator.hasNext()) {
-                        var qualifiedNameString = qualifiedNameConverter.toString(qualifiedName);
-                        throw new IllegalArgumentException("No such %s: %s"
-                                        .formatted(type.getName(), qualifiedNameString));
-                }
-                var eObjectDescription = iterator.next();
-                if (iterator.hasNext()) {
-                        var qualifiedNameString = qualifiedNameConverter.toString(qualifiedName);
-                        throw new IllegalArgumentException("Ambiguous %s: %s"
-                                        .formatted(type.getName(), qualifiedNameString));
-                }
-                var eObject = EcoreUtil.resolve(eObjectDescription.getEObjectOrProxy(), getProblem());
-                if (!type.isInstance(eObject)) {
-                        var qualifiedNameString = qualifiedNameConverter.toString(qualifiedName);
-                        throw new IllegalArgumentException("Not a %s: %s"
-                                        .formatted(type.getName(), qualifiedNameString));
-                }
-                return type.cast(eObject);
+                return semanticsUtils.getElement(problem, scope, qualifiedName, type);
         }
 }
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;
 import com.google.inject.Inject;
 import com.google.inject.Singleton;
 import org.eclipse.emf.ecore.EObject;
+import org.eclipse.emf.ecore.util.EcoreUtil;
 import org.eclipse.xtext.naming.IQualifiedNameConverter;
 import org.eclipse.xtext.naming.IQualifiedNameProvider;
+import org.eclipse.xtext.naming.QualifiedName;
+import org.eclipse.xtext.scoping.IScope;
+import org.jetbrains.annotations.NotNull;
+import org.jetbrains.annotations.Nullable;
+import tools.refinery.language.model.problem.Problem;
 
 import java.util.Optional;
 
@@ -28,4 +34,39 @@ public class SemanticsUtils {
                 }
                 return Optional.of(qualifiedNameConverter.toString(qualifiedName));
         }
+
+        @Nullable
+        public <T> T maybeGetElement(Problem problem, IScope scope, QualifiedName qualifiedName, Class<T> type) {
+                if (qualifiedName == null) {
+                        throw new IllegalArgumentException("Element name must not be null");
+                }
+                var iterator = scope.getElements(qualifiedName).iterator();
+                if (!iterator.hasNext()) {
+                        return null;
+                }
+                var eObjectDescription = iterator.next();
+                if (iterator.hasNext()) {
+                        var qualifiedNameString = qualifiedNameConverter.toString(qualifiedName);
+                        throw new IllegalArgumentException("Ambiguous %s: %s"
+                                        .formatted(type.getName(), qualifiedNameString));
+                }
+                var eObject = EcoreUtil.resolve(eObjectDescription.getEObjectOrProxy(), problem);
+                if (!type.isInstance(eObject)) {
+                        var qualifiedNameString = qualifiedNameConverter.toString(qualifiedName);
+                        throw new IllegalArgumentException("Not a %s: %s"
+                                        .formatted(type.getName(), qualifiedNameString));
+                }
+                return type.cast(eObject);
+        }
+
+        @NotNull
+        public <T> T getElement(Problem problem, IScope scope, QualifiedName qualifiedName, Class<T> type) {
+                var element = maybeGetElement(problem, scope, qualifiedName, type);
+                if (element == null) {
+                        var qualifiedNameString = qualifiedNameConverter.toString(qualifiedName);
+                        throw new IllegalArgumentException("No such %s: %s"
+                                        .formatted(type.getName(), qualifiedNameString));
+                }
+                return element;
+        }
 }
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 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.language.semantics;
+
+import com.google.inject.Inject;
+import com.google.inject.Provider;
+import org.eclipse.collections.api.factory.primitive.IntObjectMaps;
+import org.eclipse.collections.api.factory.primitive.ObjectIntMaps;
+import org.eclipse.collections.api.map.primitive.MutableIntObjectMap;
+import org.eclipse.collections.api.map.primitive.MutableObjectIntMap;
+import org.eclipse.emf.common.util.URI;
+import org.eclipse.emf.ecore.util.EcoreUtil;
+import org.eclipse.xtext.naming.IQualifiedNameConverter;
+import org.eclipse.xtext.naming.IQualifiedNameProvider;
+import org.eclipse.xtext.naming.QualifiedName;
+import org.eclipse.xtext.resource.FileExtensionProvider;
+import org.eclipse.xtext.resource.IResourceFactory;
+import org.eclipse.xtext.resource.XtextResource;
+import org.eclipse.xtext.resource.XtextResourceSet;
+import org.eclipse.xtext.scoping.IScopeProvider;
+import tools.refinery.language.model.problem.*;
+import tools.refinery.language.utils.ProblemDesugarer;
+import tools.refinery.language.utils.ProblemUtil;
+import tools.refinery.store.model.Model;
+import tools.refinery.store.reasoning.ReasoningAdapter;
+import tools.refinery.store.reasoning.interpretation.PartialInterpretation;
+import tools.refinery.store.reasoning.literal.Concreteness;
+import tools.refinery.store.reasoning.representation.PartialRelation;
+import tools.refinery.store.reasoning.translator.typehierarchy.InferredType;
+import tools.refinery.store.reasoning.translator.typehierarchy.TypeHierarchyTranslator;
+import tools.refinery.store.representation.TruthValue;
+import tools.refinery.store.tuple.Tuple;
+
+import java.io.ByteArrayInputStream;
+import java.io.ByteArrayOutputStream;
+import java.io.IOException;
+import java.util.Locale;
+import java.util.Map;
+import java.util.TreeMap;
+import java.util.TreeSet;
+import java.util.function.Function;
+import java.util.stream.Collectors;
+
+public class SolutionSerializer {
+        private String fileExtension;
+
+        @Inject
+        private Provider<XtextResourceSet> resourceSetProvider;
+
+        @Inject
+        private IResourceFactory resourceFactory;
+
+        @Inject
+        private IQualifiedNameProvider qualifiedNameProvider;
+
+        @Inject
+        private IQualifiedNameConverter qualifiedNameConverter;
+
+        @Inject
+        private SemanticsUtils semanticsUtils;
+
+        @Inject
+        private IScopeProvider scopeProvider;
+
+        @Inject
+        private ProblemDesugarer desugarer;
+
+        private ProblemTrace trace;
+        private Model model;
+        private ReasoningAdapter reasoningAdapter;
+        private PartialInterpretation<TruthValue, Boolean> existsInterpretation;
+        private Problem problem;
+        private final MutableIntObjectMap<Node> nodes = IntObjectMaps.mutable.empty();
+
+        @Inject
+        public void setFileExtensionProvider(FileExtensionProvider fileExtensionProvider) {
+                this.fileExtension = fileExtensionProvider.getPrimaryFileExtension();
+        }
+
+        public Problem serializeSolution(ProblemTrace trace, Model model) {
+                var uri = URI.createFileURI("__synthetic" + fileExtension);
+                return serializeSolution(trace, model, uri);
+        }
+
+        public Problem serializeSolution(ProblemTrace trace, Model model, URI uri) {
+                this.trace = trace;
+                this.model = model;
+                reasoningAdapter = model.getAdapter(ReasoningAdapter.class);
+                existsInterpretation = reasoningAdapter.getPartialInterpretation(Concreteness.CANDIDATE,
+                                ReasoningAdapter.EXISTS_SYMBOL);
+                var originalProblem = trace.getProblem();
+                problem = copyProblem(originalProblem, uri);
+                problem.getStatements().removeIf(SolutionSerializer::shouldRemoveStatement);
+                problem.getNodes().removeIf(this::shouldRemoveNode);
+                addExistsAssertions();
+                addClassAssertions();
+                addReferenceAssertions();
+                return problem;
+        }
+
+        private static boolean shouldRemoveStatement(Statement statement) {
+                return statement instanceof Assertion || statement instanceof ScopeDeclaration;
+        }
+
+        private boolean shouldRemoveNode(Node newNode) {
+                var qualifiedName = qualifiedNameProvider.getFullyQualifiedName(newNode);
+                var scope = scopeProvider.getScope(trace.getProblem(), ProblemPackage.Literals.ASSERTION__RELATION);
+                var originalNode = semanticsUtils.maybeGetElement(problem, scope, qualifiedName, Node.class);
+                if (originalNode == null) {
+                        return false;
+                }
+                int nodeId = trace.getNodeId(originalNode);
+                return !isExistingNode(nodeId);
+        }
+
+        private boolean isExistingNode(int nodeId) {
+                var exists = existsInterpretation.get(Tuple.of(nodeId));
+                if (!exists.isConcrete()) {
+                        throw new IllegalStateException("Invalid EXISTS %s for node %d".formatted(exists, nodeId));
+                }
+                return exists.may();
+        }
+
+        private Problem copyProblem(Problem originalProblem, URI uri) {
+                var newResourceSet = resourceSetProvider.get();
+                if (!fileExtension.equals(uri.fileExtension())) {
+                        uri = uri.appendFileExtension(fileExtension);
+                }
+                var newResource = resourceFactory.createResource(uri);
+                newResourceSet.getResources().add(newResource);
+                var originalResource = originalProblem.eResource();
+                if (originalResource instanceof XtextResource) {
+                        byte[] bytes;
+                        try {
+                                try (var outputStream = new ByteArrayOutputStream()) {
+                                        originalResource.save(outputStream, Map.of());
+                                        bytes = outputStream.toByteArray();
+                                }
+                                try (var inputStream = new ByteArrayInputStream(bytes)) {
+                                        newResource.load(inputStream, Map.of());
+                                }
+                        } catch (IOException e) {
+                                throw new IllegalStateException("Failed to copy problem", e);
+                        }
+                        var contents = newResource.getContents();
+                        if (!contents.isEmpty() && contents.getFirst() instanceof Problem newProblem) {
+                                return newProblem;
+                        }
+                        throw new IllegalStateException("Invalid contents of copied problem");
+                } else {
+                        var newProblem = EcoreUtil.copy(originalProblem);
+                        newResource.getContents().add(newProblem);
+                        return newProblem;
+                }
+        }
+
+        private Relation findRelation(Relation originalRelation) {
+                var qualifiedName = qualifiedNameProvider.getFullyQualifiedName(originalRelation);
+                var scope = scopeProvider.getScope(problem, ProblemPackage.Literals.ASSERTION__RELATION);
+                return semanticsUtils.getElement(problem, scope, qualifiedName, Relation.class);
+        }
+
+        private Relation findPartialRelation(PartialRelation partialRelation) {
+                return findRelation(trace.getRelation(partialRelation));
+        }
+
+        private Node findNode(Node originalNode) {
+                var qualifiedName = qualifiedNameProvider.getFullyQualifiedName(originalNode);
+                return findNode(qualifiedName);
+        }
+
+        private Node findNode(String name) {
+                var qualifiedName = qualifiedNameConverter.toQualifiedName(name);
+                return findNode(qualifiedName);
+        }
+
+        private Node findNode(QualifiedName qualifiedName) {
+                var scope = scopeProvider.getScope(problem, ProblemPackage.Literals.NODE_ASSERTION_ARGUMENT__NODE);
+                return semanticsUtils.maybeGetElement(problem, scope, qualifiedName, Node.class);
+        }
+
+        private void addAssertion(Relation relation, LogicValue value, Node... arguments) {
+                var assertion = ProblemFactory.eINSTANCE.createAssertion();
+                assertion.setRelation(relation);
+                for (var node : arguments) {
+                        var argument = ProblemFactory.eINSTANCE.createNodeAssertionArgument();
+                        argument.setNode(node);
+                        assertion.getArguments().add(argument);
+                }
+                var logicConstant = ProblemFactory.eINSTANCE.createLogicConstant();
+                logicConstant.setLogicValue(value);
+                assertion.setValue(logicConstant);
+                problem.getStatements().add(assertion);
+        }
+
+        private void addExistsAssertions() {
+                var builtinSymbols = desugarer.getBuiltinSymbols(problem)
+                                .orElseThrow(() -> new IllegalStateException("No builtin library in copied problem"));
+                // Make sure to output exists assertions in a deterministic order.
+                var sortedNewNodes = new TreeMap<Integer, Node>();
+                for (var pair : trace.getNodeTrace().keyValuesView()) {
+                        var originalNode = pair.getOne();
+                        int nodeId = pair.getTwo();
+                        var newNode = findNode(originalNode);
+                        // Since all implicit nodes that do not exist has already been remove in serializeSolution,
+                        // we only need to add !exists assertions to ::new nodes (nodes marked as an individual must always exist).
+                        if (ProblemUtil.isNewNode(originalNode)) {
+                                sortedNewNodes.put(nodeId, newNode);
+                        } else {
+                                nodes.put(nodeId, newNode);
+                        }
+                }
+                for (var newNode : sortedNewNodes.values()) {
+                        // If a node is a new node of the class, we should replace it with a normal node.
+                        addAssertion(builtinSymbols.exists(), LogicValue.FALSE, newNode);
+                }
+        }
+
+        private void addClassAssertions() {
+                var types = trace.getMetamodel().typeHierarchy().getPreservedTypes().keySet().stream()
+                                .collect(Collectors.toMap(Function.identity(), this::findPartialRelation));
+                var indexMap = ObjectIntMaps.mutable.empty();
+                var cursor = model.getInterpretation(TypeHierarchyTranslator.TYPE_SYMBOL).getAll();
+                while (cursor.move()) {
+                        var key = cursor.getKey();
+                        var nodeId = key.get(0);
+                        if (isExistingNode(nodeId)) {
+                                createNodeAndAssertType(nodeId, cursor.getValue(), types, indexMap);
+                        }
+                }
+        }
+
+        private void createNodeAndAssertType(int nodeId, InferredType inferredType, Map<PartialRelation, Relation> types,
+                                                                                 MutableObjectIntMap<Object> indexMap) {
+                var candidateTypeSymbol = inferredType.candidateType();
+                var candidateRelation = types.get(candidateTypeSymbol);
+                if (candidateRelation instanceof EnumDeclaration) {
+                        // Type assertions for enum literals are added implicitly.
+                        return;
+                }
+                Node node = nodes.get(nodeId);
+                if (node == null) {
+                        String typeName = candidateRelation.getName();
+                        if (typeName == null || typeName.isEmpty()) {
+                                typeName = "node";
+                        } else {
+                                typeName = typeName.substring(0, 1).toLowerCase(Locale.ROOT) + typeName.substring(1);
+                        }
+                        int index = indexMap.getIfAbsent(typeName, 0);
+                        String nodeName;
+                        do {
+                                index++;
+                                nodeName = typeName + index;
+                        } while (findNode(nodeName) != null);
+                        node = ProblemFactory.eINSTANCE.createNode();
+                        node.setName(nodeName);
+                        problem.getNodes().add(node);
+                        nodes.put(nodeId, node);
+                }
+                addAssertion(candidateRelation, LogicValue.TRUE, node);
+                var typeAnalysisResult = trace.getMetamodel().typeHierarchy().getPreservedTypes().get(candidateTypeSymbol);
+                for (var subtype : typeAnalysisResult.getDirectSubtypes()) {
+                        var subtypeRelation = types.get(subtype);
+                        addAssertion(subtypeRelation, LogicValue.FALSE, node);
+                }
+        }
+
+        private void addReferenceAssertions() {
+                var metamodel = trace.getMetamodel();
+                for (var partialRelation : metamodel.containmentHierarchy().keySet()) {
+                        // No need to add a default value, because in a concrete model, each contained node has only a single
+                        // container.
+                        addAssertions(partialRelation);
+                }
+                for (var partialRelation : metamodel.directedCrossReferences().keySet()) {
+                        addDefaultAssertion(partialRelation);
+                        addAssertions(partialRelation);
+                }
+                // No need to add directed opposite references, because their default value is {@code unknown} and their
+                // actual value will always be computed from the value of the directed forward reference.
+                // However, undirected cross-references have to be serialized in both directions due to the default value of
+                // {@code false}.
+                for (var partialRelation : metamodel.undirectedCrossReferences().keySet()) {
+                        addDefaultAssertion(partialRelation);
+                        addAssertions(partialRelation);
+                }
+        }
+
+        private void addAssertions(PartialRelation partialRelation) {
+                var relation = findPartialRelation(partialRelation);
+                var cursor = reasoningAdapter.getPartialInterpretation(Concreteness.CANDIDATE, partialRelation).getAll();
+                // Make sure to output assertions in a deterministic order.
+                var sortedTuples = new TreeSet<Tuple>();
+                while (cursor.move()) {
+                        var tuple = cursor.getKey();
+                        var from = nodes.get(tuple.get(0));
+                        var to = nodes.get(tuple.get(1));
+                        if (from == null || to == null) {
+                                // One of the endpoints does not exist in the candidate model.
+                                continue;
+                        }
+                        var value = cursor.getValue();
+                        if (!value.isConcrete()) {
+                                throw new IllegalStateException("Invalid %s %s for tuple %s".formatted(partialRelation, value, tuple));
+                        }
+                        if (value.may()) {
+                                sortedTuples.add(tuple);
+                        }
+                }
+                for (var tuple : sortedTuples) {
+                        var from = nodes.get(tuple.get(0));
+                        var to = nodes.get(tuple.get(1));
+                        addAssertion(relation, LogicValue.TRUE, from, to);
+                }
+        }
+
+        private void addDefaultAssertion(PartialRelation partialRelation) {
+                var relation = findPartialRelation(partialRelation);
+                var assertion = ProblemFactory.eINSTANCE.createAssertion();
+                assertion.setDefault(true);
+                assertion.setRelation(relation);
+                int arity = ProblemUtil.getArity(relation);
+                for (int i = 0; i < arity; i++) {
+                        var argument = ProblemFactory.eINSTANCE.createWildcardAssertionArgument();
+                        assertion.getArguments().add(argument);
+                }
+                var logicConstant = ProblemFactory.eINSTANCE.createLogicConstant();
+                logicConstant.setLogicValue(LogicValue.FALSE);
+                assertion.setValue(logicConstant);
+                problem.getStatements().add(assertion);
+        }
+}
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 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.language.semantics;
+
+import com.google.inject.Inject;
+import org.eclipse.xtext.testing.InjectWith;
+import org.eclipse.xtext.testing.extensions.InjectionExtension;
+import org.junit.jupiter.api.extension.ExtendWith;
+import org.junit.jupiter.params.ParameterizedTest;
+import org.junit.jupiter.params.provider.Arguments;
+import org.junit.jupiter.params.provider.MethodSource;
+import tools.refinery.generator.ModelGeneratorFactory;
+import tools.refinery.generator.ProblemLoader;
+import tools.refinery.language.tests.ProblemInjectorProvider;
+
+import java.io.ByteArrayOutputStream;
+import java.io.IOException;
+import java.util.Map;
+import java.util.stream.Stream;
+
+import static org.hamcrest.MatcherAssert.assertThat;
+import static org.hamcrest.Matchers.is;
+
+@ExtendWith(InjectionExtension.class)
+@InjectWith(ProblemInjectorProvider.class)
+class SolutionSerializerTest {
+        @Inject
+        ProblemLoader loader;
+
+        @Inject
+        ModelGeneratorFactory generatorFactory;
+
+        @Inject
+        SolutionSerializer serializer;
+
+        @ParameterizedTest
+        @MethodSource
+        void solutionSerializerTest(String prefix, String input, String expectedOutput) throws IOException {
+                var problem = loader.loadString(prefix + "\n" + input);
+                var generator = generatorFactory.createGenerator(problem);
+                generator.generate();
+                var solution = serializer.serializeSolution(generator.getProblemTrace(), generator.getModel());
+                String actualOutput;
+                try (var outputStream = new ByteArrayOutputStream()) {
+                        solution.eResource().save(outputStream, Map.of());
+                        actualOutput = outputStream.toString();
+                }
+                assertThat(actualOutput, is(prefix + "\n" + expectedOutput));
+        }
+
+        static Stream<Arguments> solutionSerializerTest() {
+                return Stream.of(Arguments.of("""
+                                class Foo.
+                                """, """
+                                scope Foo = 3.
+                                """, """
+                                !exists(Foo::new).
+                                Foo(foo1).
+                                Foo(foo2).
+                                Foo(foo3).
+                                """), Arguments.of("""
+                                class Foo {
+                                        contains Bar[2] bars
+                                }
+
+                                class Bar.
+                                """, """
+                                scope Foo = 1.
+                                """, """
+                                !exists(Foo::new).
+                                !exists(Bar::new).
+                                Foo(foo1).
+                                Bar(bar1).
+                                Bar(bar2).
+                                bars(foo1, bar1).
+                                bars(foo1, bar2).
+                                """), Arguments.of("""
+                                class Foo {
+                                        Bar[2] bars opposite foo
+                                }
+
+                                class Bar {
+                                        Foo[1] foo opposite bars
+                                }
+                                """, """
+                                scope Foo = 1, Bar = 2.
+                                """, """
+                                !exists(Foo::new).
+                                !exists(Bar::new).
+                                Foo(foo1).
+                                Bar(bar1).
+                                Bar(bar2).
+                                default !bars(*, *).
+                                bars(foo1, bar1).
+                                bars(foo1, bar2).
+                                """), Arguments.of("""
+                                class Person {
+                                        Person[2] friend opposite friend
+                                }
+                                """, """
+                                friend(a, b).
+                                friend(a, c).
+                                friend(b, c).
+
+                                scope Person += 0.
+                                """, """
+                                !exists(Person::new).
+                                Person(a).
+                                Person(b).
+                                Person(c).
+                                default !friend(*, *).
+                                friend(a, b).
+                                friend(a, c).
+                                friend(b, a).
+                                friend(b, c).
+                                friend(c, a).
+                                friend(c, b).
+                                """), Arguments.of("""
+                                class Foo {
+                                        Bar bar
+                                }
+
+                                enum Bar {
+                                        BAR_A,
+                                        BAR_B
+                                }
+                                """, """
+                                bar(foo, BAR_A).
+
+                                scope Foo += 0.
+                                """, """
+                                !exists(Foo::new).
+                                Foo(foo).
+                                default !bar(*, *).
+                                bar(foo, BAR_A).
+                                """), Arguments.of("""
+                                class Foo.
+                                class Bar extends Foo.
+                                """, """
+                                scope Foo = 1, Bar = 0.
+                                """, """
+                                !exists(Foo::new).
+                                !exists(Bar::new).
+                                Foo(foo1).
+                                !Bar(foo1).
+                                """), Arguments.of("""
+                                class Foo {
+                                        Foo[] ref
+                                }
+                                """, """
+                                ref(a, b).
+                                !exists(b).
+
+                                scope Foo += 0.
+                                """, """
+                                !exists(Foo::new).
+                                Foo(a).
+                                default !ref(*, *).
+                                """));
+        }
+}
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 {
                 }
         }
 
+        protected void format(EnumDeclaration enumDeclaration, IFormattableDocument doc) {
+                surroundNewLines(doc, enumDeclaration, this::twoNewLines);
+                var region = regionFor(enumDeclaration);
+                doc.append(region.keyword("enum"), this::oneSpace);
+                doc.prepend(region.keyword("{"), this::oneSpace);
+                doc.append(region.keyword("{"), it -> it.setNewLines(1, 1, 2));
+                doc.prepend(region.keyword("}"), it -> it.setNewLines(1, 1, 2));
+                doc.prepend(region.keyword("."), this::noSpace);
+        }
+
         protected void format(PredicateDefinition predicateDefinition, IFormattableDocument doc) {
                 surroundNewLines(doc, predicateDefinition, this::twoNewLines);
                 var region = regionFor(predicateDefinition);
@@ -151,14 +161,14 @@ public class ProblemFormatter extends AbstractJavaFormatter {
         }
 
         protected void surroundNewLines(IFormattableDocument doc, EObject eObject,
-                        Procedure1<? super IHiddenRegionFormatter> init) {
+                                                                        Procedure1<? super IHiddenRegionFormatter> init) {
                 var region = doc.getRequest().getTextRegionAccess().regionForEObject(eObject);
                 preprendNewLines(doc, region, init);
                 appendNewLines(doc, region, init);
         }
 
         protected void preprendNewLines(IFormattableDocument doc, ISequentialRegion region,
-                        Procedure1<? super IHiddenRegionFormatter> init) {
+                                                                        Procedure1<? super IHiddenRegionFormatter> init) {
                 if (region == null) {
                         return;
                 }
@@ -174,7 +184,7 @@ public class ProblemFormatter extends AbstractJavaFormatter {
         }
 
         protected void appendNewLines(IFormattableDocument doc, ISequentialRegion region,
-                        Procedure1<? super IHiddenRegionFormatter> init) {
+                                                                  Procedure1<? super IHiddenRegionFormatter> init) {
                 if (region == null) {
                         return;
                 }
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
 
         @Override
         protected void sequence_Assertion(ISerializationContext context, Assertion semanticObject) {
-                if (semanticObject.isDefault() ||
-                                !(semanticObject.getValue() instanceof LogicConstant logicConstant) ||
+                if (!(semanticObject.getValue() instanceof LogicConstant logicConstant) ||
                                 logicConstant.getLogicValue() == LogicValue.ERROR) {
                         super.sequence_Assertion(context, semanticObject);
                         return;
@@ -39,6 +38,9 @@ public class PreferShortAssertionsProblemSemanticSequencer extends ProblemSemant
                 }
                 var feeder = createSequencerFeeder(context, semanticObject);
                 var access = grammarAccess.getAssertionAccess();
+                if (semanticObject.isDefault()) {
+                        feeder.accept(access.getDefaultDefaultKeyword_0_0());
+                }
                 feeder.accept(access.getValueShortLogicConstantParserRuleCall_1_1_0_0(), logicConstant);
                 feeder.accept(access.getRelationRelationQualifiedNameParserRuleCall_1_1_1_0_1(), semanticObject.getRelation());
                 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 {
         }
 
         @ParameterizedTest
-        @MethodSource
-        void defaultAssertionTest(LogicValue value, String valueAsString) {
+        @MethodSource("assertionTest")
+        void defaultAssertionTest(LogicValue value, String serializedAssertion) {
                 var pred = createPred();
                 var node = ProblemFactory.eINSTANCE.createNode();
                 node.setName("a");
@@ -88,12 +88,7 @@ class ProblemSerializerTest {
                                 pred foo(node p).
 
                                 indiv a.
-                                default foo(a):\040""" + valueAsString + ".\n");
-        }
-
-        static Stream<Arguments> defaultAssertionTest() {
-                return Stream.of(Arguments.of(LogicValue.TRUE, "true"), Arguments.of(LogicValue.FALSE, "false"),
-                                Arguments.of(LogicValue.UNKNOWN, "unknown"), Arguments.of(LogicValue.ERROR, "error"));
+                                default\040""" + serializedAssertion + "\n");
         }
 
         @Test
@@ -233,19 +228,14 @@ class ProblemSerializerTest {
         }
 
         private void assertSerializedResult(String expected) {
-                var outputStream = new ByteArrayOutputStream();
-                try {
-                        resource.save(outputStream, Map.of());
-                } catch (IOException e) {
-                        throw new AssertionError("Failed to serialize problem", e);
-                } finally {
-                        try {
-                                outputStream.close();
-                        } catch (IOException e) {
-                                // Nothing to handle in a test.
-                        }
-                }
-                var problemString = outputStream.toString();
+                String problemString;
+        try (var outputStream = new ByteArrayOutputStream()) {
+            resource.save(outputStream, Map.of());
+                        problemString = outputStream.toString();
+        } catch (IOException e) {
+            throw new AssertionError("Failed to serialize problem", e);
+        }
+        // Nothing to handle in a test.
 
                 assertThat(problemString.replace("\r\n", "\n"), equalTo(expected.replace("\r\n", "\n")));
         }