build: move modules into subproject directory

5 files changed, 946 insertions, 0 deletions

diff --git a/subprojects/language/src/test/java/tools/refinery/language/tests/ProblemParsingTest.xtend b/subprojects/language/src/test/java/tools/refinery/language/tests/ProblemParsingTest.xtend
new file mode 100644
index 00000000..53d31a6c
--- /dev/null
+++ b/subprojects/language/src/test/java/tools/refinery/language/tests/ProblemParsingTest.xtend
@@ -0,0 +1,64 @@
+/*
+ * generated by Xtext 2.26.0.M1
+ */
+package tools.refinery.language.tests
+
+import com.google.inject.Inject
+import org.eclipse.xtext.testing.InjectWith
+import org.eclipse.xtext.testing.extensions.InjectionExtension
+import org.eclipse.xtext.testing.util.ParseHelper
+import org.junit.jupiter.api.Test
+import org.junit.jupiter.api.^extension.ExtendWith
+import tools.refinery.language.model.problem.Problem
+import tools.refinery.language.model.tests.ProblemTestUtil
+
+import static org.hamcrest.MatcherAssert.assertThat
+import static org.hamcrest.Matchers.*
+
+@ExtendWith(InjectionExtension)
+@InjectWith(ProblemInjectorProvider)
+class ProblemParsingTest {
+        @Inject
+        ParseHelper<Problem> parseHelper
+
+        @Inject
+        extension ProblemTestUtil
+
+        @Test
+        def void exampleTest() {
+                val it = parseHelper.parse('''
+                        class Family {
+                                contains Person[] members
+                        }
+                        
+                        class Person {
+                                Person[0..*] children opposite parent
+                                Person[0..1] parent opposite children
+                                int age
+                                TaxStatus taxStatus
+                        }
+                        
+                        enum TaxStatus {
+                                child, student, adult, retired
+                        }
+                        
+                        % A child cannot have any dependents.
+                        error invalidTaxStatus(Person p) <->
+                                taxStatus(p, child), children(p, _q).
+                        
+                        indiv family.
+                        Family(family).
+                        members(family, anne): true.
+                        members(family, bob).
+                        members(family, ciri).
+                        children(anne, ciri).
+                        ?children(bob, ciri).
+                        taxStatus(anne, adult).
+                        age(anne, 35).
+                        bobAge: 27.
+                        age(bob, bobAge).
+                        !age(ciri, bobAge).
+                ''')
+                assertThat(errors, empty)
+        }
+}
diff --git a/subprojects/language/src/test/java/tools/refinery/language/tests/formatting2/ProblemFormatterTest.java b/subprojects/language/src/test/java/tools/refinery/language/tests/formatting2/ProblemFormatterTest.java
new file mode 100644
index 00000000..41ad2d31
--- /dev/null
+++ b/subprojects/language/src/test/java/tools/refinery/language/tests/formatting2/ProblemFormatterTest.java
@@ -0,0 +1,235 @@
+package tools.refinery.language.tests.formatting2;
+
+import static org.hamcrest.MatcherAssert.assertThat;
+import static org.hamcrest.Matchers.equalTo;
+
+import java.util.List;
+
+import org.eclipse.xtext.formatting2.FormatterRequest;
+import org.eclipse.xtext.formatting2.IFormatter2;
+import org.eclipse.xtext.formatting2.regionaccess.ITextRegionAccess;
+import org.eclipse.xtext.formatting2.regionaccess.ITextReplacement;
+import org.eclipse.xtext.formatting2.regionaccess.TextRegionAccessBuilder;
+import org.eclipse.xtext.resource.XtextResource;
+import org.eclipse.xtext.testing.InjectWith;
+import org.eclipse.xtext.testing.extensions.InjectionExtension;
+import org.eclipse.xtext.testing.util.ParseHelper;
+import org.junit.jupiter.api.Test;
+import org.junit.jupiter.api.extension.ExtendWith;
+
+import com.google.inject.Inject;
+import com.google.inject.Provider;
+
+import tools.refinery.language.model.problem.Problem;
+import tools.refinery.language.tests.ProblemInjectorProvider;
+
+@ExtendWith(InjectionExtension.class)
+@InjectWith(ProblemInjectorProvider.class)
+class ProblemFormatterTest {
+        @Inject
+        private ParseHelper<Problem> parseHelper;
+
+        @Inject
+        private Provider<FormatterRequest> formatterRequestProvider;
+
+        @Inject
+        private TextRegionAccessBuilder regionBuilder;
+
+        @Inject
+        private IFormatter2 formatter2;
+
+        @Test
+        void problemNameTest() {
+                testFormatter("  problem  problem  .  ", "problem problem.\n");
+        }
+
+        @Test
+        void assertionTest() {
+                testFormatter("  equals (  a  ,  b  ,  *  )  :  true  .  ", "equals(a, b, *): true.\n");
+        }
+
+        @Test
+        void defaultAssertionTest() {
+                testFormatter("  default  equals (  a  ,  b  ,  *  )  :  true  .  ", "default equals(a, b, *): true.\n");
+        }
+
+        @Test
+        void assertionShortTrueTest() {
+                testFormatter("  equals (  a  ,  b  ,  *  )  .  ", "equals(a, b, *).\n");
+        }
+
+        @Test
+        void defaultAssertionShortTrueTest() {
+                testFormatter("  default  equals (  a  ,  b  ,  *  )  .  ", "default equals(a, b, *).\n");
+        }
+
+        @Test
+        void assertionShortFalseTest() {
+                testFormatter("  !  equals (  a  ,  b  ,  *  )  .  ", "!equals(a, b, *).\n");
+        }
+
+        @Test
+        void defaultAssertionShortFalseTest() {
+                testFormatter("  default  !  equals (  a  ,  b  ,  *  )  .  ", "default !equals(a, b, *).\n");
+        }
+
+        @Test
+        void assertionShortUnknownTest() {
+                testFormatter("  ?  equals (  a  ,  b  ,  *  )  .  ", "?equals(a, b, *).\n");
+        }
+
+        @Test
+        void defaultAssertionShortUnknownTest() {
+                testFormatter("  default  ?  equals (  a  ,  b  ,  *  )  .  ", "default ?equals(a, b, *).\n");
+        }
+
+        @Test
+        void multipleAssertionsTest() {
+                testFormatter("  exists (  a  )  .  ?  equals  (  a  ,  a  ).", """
+                                exists(a).
+                                ?equals(a, a).
+                                """);
+        }
+
+        @Test
+        void multipleAssertionsNamedProblemTest() {
+                testFormatter("  problem  foo  .  exists (  a  )  .  ?  equals  (  a  ,  a  ).", """
+                                problem foo.
+
+                                exists(a).
+                                ?equals(a, a).
+                                """);
+        }
+
+        @Test
+        void classWithoutBodyTest() {
+                testFormatter("  class  Foo  .  ", "class Foo.\n");
+        }
+
+        @Test
+        void abstractClassWithoutBodyTest() {
+                testFormatter("  abstract  class  Foo  .  ", "abstract class Foo.\n");
+        }
+
+        @Test
+        void classExtendsWithoutBodyTest() {
+                testFormatter("  class  Foo.  class  Bar  .  class  Quux  extends  Foo  ,  Bar  .  ", """
+                                class Foo.
+
+                                class Bar.
+
+                                class Quux extends Foo, Bar.
+                                """);
+        }
+
+        @Test
+        void classWithEmptyBodyTest() {
+                testFormatter("  class  Foo  {  }  ", """
+                                class Foo {
+                                }
+                                """);
+        }
+
+        @Test
+        void classExtendsWithBodyTest() {
+                testFormatter("  class  Foo.  class  Bar  .  class  Quux  extends  Foo  ,  Bar  {  }  ", """
+                                class Foo.
+
+                                class Bar.
+
+                                class Quux extends Foo, Bar {
+                                }
+                                """);
+        }
+
+        @Test
+        void predicateWithoutBodyTest() {
+                testFormatter("  pred  foo  (  node  a  ,  b  )  .  ", "pred foo(node a, b).\n");
+        }
+
+        @Test
+        void predicateWithBodyTest() {
+                testFormatter(
+                                "  pred  foo  (  node  a  ,  b  )  <->  equal  (a  ,  _c  )  ,  !  equal  (  a  ,  b  )  ;  equal+(  a  ,  b  )  .  ",
+                                "pred foo(node a, b) <-> equal(a, _c), !equal(a, b); equal+(a, b).\n");
+        }
+
+        @Test
+        void predicatesWithoutBodyTest() {
+                testFormatter("  pred  foo  (  node  a  ,  b  )  .  pred  bar  (  node  c  )  .  ", """
+                                pred foo(node a, b).
+
+                                pred bar(node c).
+                                """);
+        }
+
+        @Test
+        void predicateCommentsTest() {
+                testFormatter("""
+                                  % Some foo
+                                pred  foo  (  node  a  ,  b  )  .
+                                  % Some bar
+                                pred  bar  (  node  c  )  .
+                                """, """
+                                % Some foo
+                                pred foo(node a, b).
+
+                                % Some bar
+                                pred bar(node c).
+                                """);
+        }
+
+        @Test
+        void individualDeclarationTest() {
+                testFormatter("  indiv  a  ,  b  .  ", "indiv a, b.\n");
+        }
+
+        @Test
+        void mixedDeclarationsTest() {
+                testFormatter("""
+                                problem test.
+                                pred foo(node a).
+                                class Foo.
+                                foo(n1, n2).
+                                indiv i1.
+                                !foo(i1, n1).
+                                pred bar(node a, node b).
+                                pred quux().
+                                default !bar(*, *).
+                                """, """
+                                problem test.
+
+                                pred foo(node a).
+
+                                class Foo.
+
+                                foo(n1, n2).
+                                indiv i1.
+                                !foo(i1, n1).
+
+                                pred bar(node a, node b).
+
+                                pred quux().
+
+                                default !bar(*, *).
+                                """);
+        }
+
+        private void testFormatter(String toFormat, String expected) {
+                Problem problem;
+                try {
+                        problem = parseHelper.parse(toFormat);
+                } catch (Exception e) {
+                        throw new RuntimeException("Failed to parse document", e);
+                }
+                var resource = (XtextResource) problem.eResource();
+                FormatterRequest request = formatterRequestProvider.get();
+                request.setAllowIdentityEdits(false);
+                request.setFormatUndefinedHiddenRegionsOnly(false);
+                ITextRegionAccess regionAccess = regionBuilder.forNodeModel(resource).create();
+                request.setTextRegionAccess(regionAccess);
+                List<ITextReplacement> replacements = formatter2.format(request);
+                var formattedString = regionAccess.getRewriter().renderToString(replacements);
+                assertThat(formattedString, equalTo(expected));
+        }
+}
diff --git a/subprojects/language/src/test/java/tools/refinery/language/tests/rules/DirectRuleParsingTest.xtend b/subprojects/language/src/test/java/tools/refinery/language/tests/rules/DirectRuleParsingTest.xtend
new file mode 100644
index 00000000..d60651a0
--- /dev/null
+++ b/subprojects/language/src/test/java/tools/refinery/language/tests/rules/DirectRuleParsingTest.xtend
@@ -0,0 +1,96 @@
+package tools.refinery.language.tests.rules
+
+import com.google.inject.Inject
+import org.eclipse.xtext.testing.InjectWith
+import org.eclipse.xtext.testing.extensions.InjectionExtension
+import org.eclipse.xtext.testing.util.ParseHelper
+import org.junit.jupiter.api.Test
+import org.junit.jupiter.api.^extension.ExtendWith
+import tools.refinery.language.model.problem.Problem
+import tools.refinery.language.tests.ProblemInjectorProvider
+import tools.refinery.language.model.tests.ProblemTestUtil
+
+import static org.hamcrest.MatcherAssert.assertThat
+import static org.hamcrest.Matchers.*
+
+@ExtendWith(InjectionExtension)
+@InjectWith(ProblemInjectorProvider)
+class DirectRuleParsingTest {
+        @Inject
+        ParseHelper<Problem> parseHelper
+
+        @Inject
+        extension ProblemTestUtil
+        
+        @Test
+        def void relationValueRewriteTest() {
+                val it = parseHelper.parse('''
+                        pred Person(p).
+                        direct rule r(p1): Person(p1) = true ~> Person(p1) = false.
+                ''')
+                assertThat(errors, empty)
+        }
+        
+        @Test
+        def void relationValueMergeTest() {
+                val it = parseHelper.parse('''
+                        pred Person(p).
+                        direct rule r(p1): Person(p1): true ~> Person(p1): false.
+                ''')
+                assertThat(errors, empty)
+        }
+        
+        @Test
+        def void newNodeTest() {
+                val it = parseHelper.parse('''
+                        pred Person(p).
+                        direct rule r(p1): Person(p1) = true ~> new p2, Person(p2) = unknown.
+                ''')
+                assertThat(errors, empty)
+                assertThat(rule("r").param(0), equalTo(rule("r").conj(0).lit(0).valueAtom.arg(0).variable))
+                assertThat(rule("r").actionLit(0).newVar,
+                        equalTo(rule("r").actionLit(1).valueAtom.arg(0).variable)
+                )
+        }
+        
+        @Test
+        def void differentScopeTest() {
+                val it = parseHelper.parse('''
+                        pred Friend(a, b).
+                        direct rule r(p1): Friend(p1, p2) = false ~> new p2, Friend(p1, p2) = true.
+                ''')
+                assertThat(errors, empty)
+                assertThat(rule("r").conj(0).lit(0).valueAtom.arg(1).variable,
+                        not(equalTo(rule("r").actionLit(1).valueAtom.arg(1).variable)))
+        }
+        
+        @Test
+        def void parameterShadowingTest() {
+                val it = parseHelper.parse('''
+                        pred Friend(a, b).
+                        direct rule r(p1, p2): Friend(p1, p2) = false ~> new p2, Friend(p1, p2) = true.
+                ''')
+                assertThat(errors, empty)
+                assertThat(rule("r").param(1),
+                        not(equalTo(rule("r").actionLit(1).valueAtom.arg(1).variable)))
+        }
+        
+        @Test
+        def void deleteParameterNodeTest() {
+                val it = parseHelper.parse('''
+                        pred Person(p).
+                        direct rule r(p1): Person(p1): false ~> delete p1.
+                ''')
+                assertThat(errors, empty)
+        }
+        
+        @Test
+        def void deleteDifferentScopeNodeTest() {
+                val it = parseHelper.parse('''
+                        pred Friend(p).
+                        direct rule r(p1): Friend(p1, p2) = true ~> delete p2.
+                ''')
+                assertThat(errors, not(empty))
+        }
+        
+}
diff --git a/subprojects/language/src/test/java/tools/refinery/language/tests/scoping/NodeScopingTest.xtend b/subprojects/language/src/test/java/tools/refinery/language/tests/scoping/NodeScopingTest.xtend
new file mode 100644
index 00000000..3a046341
--- /dev/null
+++ b/subprojects/language/src/test/java/tools/refinery/language/tests/scoping/NodeScopingTest.xtend
@@ -0,0 +1,322 @@
+package tools.refinery.language.tests.scoping
+
+import com.google.inject.Inject
+import java.util.stream.Stream
+import org.eclipse.xtext.testing.InjectWith
+import org.eclipse.xtext.testing.extensions.InjectionExtension
+import org.eclipse.xtext.testing.util.ParseHelper
+import org.junit.jupiter.api.Test
+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 org.junit.jupiter.params.provider.ValueSource
+import tools.refinery.language.model.problem.Problem
+import tools.refinery.language.model.tests.ProblemTestUtil
+import tools.refinery.language.tests.ProblemInjectorProvider
+
+import static org.hamcrest.MatcherAssert.assertThat
+import static org.hamcrest.Matchers.*
+
+@ExtendWith(InjectionExtension)
+@InjectWith(ProblemInjectorProvider)
+class NodeScopingTest {
+        @Inject
+        ParseHelper<Problem> parseHelper
+
+        @Inject
+        extension ProblemTestUtil
+
+        @ParameterizedTest
+        @ValueSource(strings=#["", "builtin::"])
+        def void builtInArgumentTypeTest(String prefix) {
+                val it = parseHelper.parse('''
+                        pred predicate(«prefix»node a, «prefix»data b, «prefix»int c).
+                ''')
+                assertThat(errors, empty)
+                assertThat(pred('predicate').param(0).parameterType, equalTo(builtin.findClass('node')))
+                assertThat(pred('predicate').param(1).parameterType, equalTo(builtin.findClass('data')))
+                assertThat(pred('predicate').param(2).parameterType, equalTo(builtin.findClass('int')))
+        }
+
+        @Test
+        def void implicitNodeInAssertionTest() {
+                val it = parseHelper.parse('''
+                        pred predicate(node x, node y) <-> node(x).
+                        predicate(a, a).
+                        ?predicate(a, b).
+                ''')
+                assertThat(errors, empty)
+                assertThat(nodeNames, hasItems('a', 'b'))
+                assertThat(assertion(0).arg(0).node, equalTo(node('a')))
+                assertThat(assertion(0).arg(1).node, equalTo(node('a')))
+                assertThat(assertion(1).arg(0).node, equalTo(node('a')))
+                assertThat(assertion(1).arg(1).node, equalTo(node('b')))
+        }
+
+        @Test
+        def void implicitNodeInNodeValueAssertionTest() {
+                val it = parseHelper.parse('''
+                        a: 16.
+                ''')
+                assertThat(errors, empty)
+                assertThat(nodeNames, hasItems('a'))
+                assertThat(nodeValueAssertion(0).node, equalTo(node('a')))
+        }
+
+        @Test
+        def void implicitNodeInPredicateTest() {
+                val it = parseHelper.parse('''
+                        pred predicate(node a) <-> node(b).
+                        predicate(b).
+                ''')
+                assertThat(errors, empty)
+                assertThat(nodeNames, hasItem("b"))
+                assertThat(pred("predicate").conj(0).lit(0).arg(0).node, equalTo(node("b")))
+                assertThat(assertion(0).arg(0).node, equalTo(node("b")))
+        }
+
+        @ParameterizedTest
+        @MethodSource("individualNodeReferenceSource")
+        def void individualNodeInAssertionTest(String qualifiedNamePrefix, boolean namedProblem) {
+                val it = parseHelper.parse('''
+                        «IF namedProblem»problem test.«ENDIF»
+                        indiv a, b.
+                        pred predicate(node x, node y) <-> node(x).
+                        predicate(«qualifiedNamePrefix»a, «qualifiedNamePrefix»a).
+                        ?predicate(«qualifiedNamePrefix»a, «qualifiedNamePrefix»b).
+                ''')
+                assertThat(errors, empty)
+                assertThat(nodeNames, empty)
+                assertThat(assertion(0).arg(0).node, equalTo(individualNode('a')))
+                assertThat(assertion(0).arg(1).node, equalTo(individualNode('a')))
+                assertThat(assertion(1).arg(0).node, equalTo(individualNode('a')))
+                assertThat(assertion(1).arg(1).node, equalTo(individualNode('b')))
+        }
+
+        @ParameterizedTest
+        @MethodSource("individualNodeReferenceSource")
+        def void individualNodeInNodeValueAssertionTest(String qualifiedNamePrefix, boolean namedProblem) {
+                val it = parseHelper.parse('''
+                        «IF namedProblem»problem test.«ENDIF»
+                        indiv a.
+                        «qualifiedNamePrefix»a: 16.
+                ''')
+                assertThat(errors, empty)
+                assertThat(nodeNames, empty)
+                assertThat(nodeValueAssertion(0).node, equalTo(individualNode('a')))
+        }
+
+        @ParameterizedTest
+        @MethodSource("individualNodeReferenceSource")
+        def void individualNodeInPredicateTest(String qualifiedNamePrefix, boolean namedProblem) {
+                val it = parseHelper.parse('''
+                        «IF namedProblem»problem test.«ENDIF»
+                        indiv b.
+                        pred predicate(node a) <-> node(«qualifiedNamePrefix»b).
+                ''')
+                assertThat(errors, empty)
+                assertThat(nodeNames, empty)
+                assertThat(pred("predicate").conj(0).lit(0).arg(0).node, equalTo(individualNode("b")))
+        }
+        
+        static def individualNodeReferenceSource() {
+                Stream.of(
+                        Arguments.of("", false),
+                        Arguments.of("", true),
+                        Arguments.of("test::", true)
+                )
+        }
+
+        @ParameterizedTest
+        @MethodSource("builtInNodeReferencesSource")
+        def void builtInNodeTest(String qualifiedName) {
+                val it = parseHelper.parse('''
+                        pred predicate(node x) <-> node(x).
+                        predicate(«qualifiedName»).
+                ''')
+                assertThat(errors, empty)
+                assertThat(nodes, empty)
+                assertThat(assertion(0).arg(0).node, equalTo(builtin.findClass('int').newNode))
+        }
+
+        @ParameterizedTest
+        @MethodSource("builtInNodeReferencesSource")
+        def void builtInNodeInNodeValueAssertionTest(String qualifiedName) {
+                val it = parseHelper.parse('''
+                        «qualifiedName»: 16.
+                ''')
+                assertThat(errors, empty)
+                assertThat(nodes, empty)
+                assertThat(nodeValueAssertion(0).node, equalTo(builtin.findClass('int').newNode))
+        }
+
+        @ParameterizedTest
+        @MethodSource("builtInNodeReferencesSource")
+        def void builtInNodeInPredicateTest(String qualifiedName) {
+                val it = parseHelper.parse('''
+                        pred predicate(node x) <-> node(«qualifiedName»).
+                ''')
+                assertThat(errors, empty)
+                assertThat(pred("predicate").conj(0).lit(0).arg(0).node, equalTo(builtin.findClass('int').newNode))
+        }
+
+        static def builtInNodeReferencesSource() {
+                Stream.of(
+                        Arguments.of("int::new"),
+                        Arguments.of("builtin::int::new")
+                )
+        }
+
+        @ParameterizedTest(name="{0}, namedProblem={1}")
+        @MethodSource("classNewNodeReferencesSource")
+        def void classNewNodeTest(String qualifiedName, boolean namedProblem) {
+                val it = parseHelper.parse('''
+                        «IF namedProblem»problem test.«ENDIF»
+                        class Foo.
+                        pred predicate(node x) <-> node(x).
+                        predicate(«qualifiedName»).
+                ''')
+                assertThat(errors, empty)
+                assertThat(nodes, empty)
+                assertThat(assertion(0).arg(0).node, equalTo(findClass('Foo').newNode))
+        }
+
+        @ParameterizedTest(name="{0}, namedProblem={1}")
+        @MethodSource("classNewNodeReferencesSource")
+        def void classNewNodeInNodeValueAssertionTest(String qualifiedName, boolean namedProblem) {
+                val it = parseHelper.parse('''
+                        «IF namedProblem»problem test.«ENDIF»
+                        class Foo.
+                        «qualifiedName»: 16.
+                ''')
+                assertThat(errors, empty)
+                assertThat(nodes, empty)
+                assertThat(nodeValueAssertion(0).node, equalTo(findClass('Foo').newNode))
+        }
+
+        @ParameterizedTest(name="{0}, namedProblem={1}")
+        @MethodSource("classNewNodeReferencesSource")
+        def void classNewNodeInPredicateTest(String qualifiedName, boolean namedProblem) {
+                val it = parseHelper.parse('''
+                        «IF namedProblem»problem test.«ENDIF»
+                        class Foo.
+                        pred predicate(node x) <-> node(«qualifiedName»).
+                ''')
+                assertThat(errors, empty)
+                assertThat(pred("predicate").conj(0).lit(0).arg(0).node, equalTo(findClass('Foo').newNode))
+        }
+
+        static def classNewNodeReferencesSource() {
+                Stream.of(
+                        Arguments.of("Foo::new", false),
+                        Arguments.of("Foo::new", true),
+                        Arguments.of("test::Foo::new", true)
+                )
+        }
+
+        @Test
+        def void newNodeIsNotSpecial() {
+                val it = parseHelper.parse('''
+                        class Foo.
+                        pred predicate(node x) <-> node(x).
+                        predicate(new).
+                ''')
+                assertThat(errors, empty)
+                assertThat(nodeNames, hasItem('new'))
+                assertThat(assertion(0).arg(0).node, not(equalTo(findClass('Foo').newNode)))
+        }
+
+        @ParameterizedTest(name="{0}, namedProblem={1}")
+        @MethodSource("enumLiteralReferencesSource")
+        def void enumLiteralTest(String qualifiedName, boolean namedProblem) {
+                val it = parseHelper.parse('''
+                        «IF namedProblem»problem test.«ENDIF»
+                        enum Foo { alpha, beta }
+                        pred predicate(Foo a) <-> node(a).
+                        predicate(«qualifiedName»).
+                ''')
+                assertThat(errors, empty)
+                assertThat(nodes, empty)
+                assertThat(assertion(0).arg(0).node, equalTo(findEnum("Foo").literal("alpha")))
+        }
+
+        @ParameterizedTest(name="{0}, namedProblem={1}")
+        @MethodSource("enumLiteralReferencesSource")
+        def void enumLiteralInNodeValueAssertionTest(String qualifiedName, boolean namedProblem) {
+                val it = parseHelper.parse('''
+                        «IF namedProblem»problem test.«ENDIF»
+                        enum Foo { alpha, beta }
+                        «qualifiedName»: 16.
+                ''')
+                assertThat(errors, empty)
+                assertThat(nodes, empty)
+                assertThat(nodeValueAssertion(0).node, equalTo(findEnum("Foo").literal("alpha")))
+        }
+
+        @ParameterizedTest(name="{0}, namedProblem={1}")
+        @MethodSource("enumLiteralReferencesSource")
+        def void enumLiteralInPredicateTest(String qualifiedName, boolean namedProblem) {
+                val it = parseHelper.parse('''
+                        «IF namedProblem»problem test.«ENDIF»
+                        enum Foo { alpha, beta }
+                        pred predicate(Foo a) <-> node(«qualifiedName»).
+                ''')
+                assertThat(errors, empty)
+                assertThat(nodes, empty)
+                assertThat(pred("predicate").conj(0).lit(0).arg(0).node, equalTo(findEnum("Foo").literal("alpha")))
+        }
+
+        static def enumLiteralReferencesSource() {
+                Stream.of(
+                        Arguments.of("alpha", false),
+                        Arguments.of("alpha", true),
+                        Arguments.of("Foo::alpha", false),
+                        Arguments.of("Foo::alpha", true),
+                        Arguments.of("test::alpha", true),
+                        Arguments.of("test::Foo::alpha", true)
+                )
+        }
+
+        @ParameterizedTest
+        @MethodSource("builtInEnumLiteralReferencesSource")
+        def void builtInEnumLiteralTest(String qualifiedName) {
+                val it = parseHelper.parse('''
+                        pred predicate(node a) <-> node(a).
+                        predicate(«qualifiedName»).
+                ''')
+                assertThat(errors, empty)
+                assertThat(nodes, empty)
+                assertThat(assertion(0).arg(0).node, equalTo(builtin.findEnum("bool").literal("true")))
+        }
+
+        @ParameterizedTest
+        @MethodSource("builtInEnumLiteralReferencesSource")
+        def void builtInEnumLiteralInNodeValueAssertionTest(String qualifiedName) {
+                val it = parseHelper.parse('''
+                        «qualifiedName»: 16.
+                ''')
+                assertThat(errors, empty)
+                assertThat(nodes, empty)
+                assertThat(nodeValueAssertion(0).node, equalTo(builtin.findEnum("bool").literal("true")))
+        }
+
+        @ParameterizedTest
+        @MethodSource("builtInEnumLiteralReferencesSource")
+        def void bultInEnumLiteralInPredicateTest(String qualifiedName) {
+                val it = parseHelper.parse('''
+                        pred predicate() <-> node(«qualifiedName»).
+                ''')
+                assertThat(errors, empty)
+                assertThat(pred("predicate").conj(0).lit(0).arg(0).node, equalTo(builtin.findEnum("bool").literal("true")))
+        }
+
+        static def builtInEnumLiteralReferencesSource() {
+                Stream.of(
+                        Arguments.of("true"),
+                        Arguments.of("bool::true"),
+                        Arguments.of("builtin::true"),
+                        Arguments.of("builtin::bool::true")
+                )
+        }
+}
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
new file mode 100644
index 00000000..ba3aaeb7
--- /dev/null
+++ b/subprojects/language/src/test/java/tools/refinery/language/tests/serializer/ProblemSerializerTest.java
@@ -0,0 +1,229 @@
+package tools.refinery.language.tests.serializer;
+
+import static org.hamcrest.MatcherAssert.assertThat;
+import static org.hamcrest.Matchers.equalTo;
+
+import java.io.ByteArrayOutputStream;
+import java.io.IOException;
+import java.util.Map;
+import java.util.stream.Stream;
+
+import org.eclipse.emf.common.util.URI;
+import org.eclipse.emf.ecore.resource.Resource;
+import org.eclipse.emf.ecore.resource.ResourceSet;
+import org.eclipse.xtext.testing.InjectWith;
+import org.eclipse.xtext.testing.extensions.InjectionExtension;
+import org.junit.jupiter.api.BeforeEach;
+import org.junit.jupiter.api.Test;
+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 com.google.inject.Inject;
+
+import tools.refinery.language.model.ProblemUtil;
+import tools.refinery.language.model.problem.Atom;
+import tools.refinery.language.model.problem.LogicValue;
+import tools.refinery.language.model.problem.Node;
+import tools.refinery.language.model.problem.PredicateDefinition;
+import tools.refinery.language.model.problem.Problem;
+import tools.refinery.language.model.problem.ProblemFactory;
+import tools.refinery.language.model.problem.Relation;
+import tools.refinery.language.model.problem.VariableOrNode;
+import tools.refinery.language.model.tests.ProblemTestUtil;
+import tools.refinery.language.tests.ProblemInjectorProvider;
+
+@ExtendWith(InjectionExtension.class)
+@InjectWith(ProblemInjectorProvider.class)
+class ProblemSerializerTest {
+        @Inject
+        private ResourceSet resourceSet;
+
+        @Inject
+        private ProblemTestUtil testUtil;
+
+        private Resource resource;
+
+        private Problem problem;
+
+        private Problem builtin;
+
+        @BeforeEach
+        void beforeEach() {
+                problem = ProblemFactory.eINSTANCE.createProblem();
+                resource = resourceSet.createResource(URI.createFileURI("test.problem"));
+                resource.getContents().add(problem);
+                builtin = ProblemUtil.getBuiltInLibrary(problem).get();
+        }
+
+        @ParameterizedTest
+        @MethodSource
+        void assertionTest(LogicValue value, String serializedAssertion) {
+                var pred = createPred();
+                var node = ProblemFactory.eINSTANCE.createNode();
+                node.setName("a");
+                var individualDeclaration = ProblemFactory.eINSTANCE.createIndividualDeclaration();
+                individualDeclaration.getNodes().add(node);
+                problem.getStatements().add(individualDeclaration);
+                createAssertion(pred, node, value);
+
+                assertSerializedResult("""
+                                pred foo(node p).
+
+                                indiv a.
+                                """ + serializedAssertion + "\n");
+        }
+
+        static Stream<Arguments> assertionTest() {
+                return Stream.of(Arguments.of(LogicValue.TRUE, "foo(a)."), Arguments.of(LogicValue.FALSE, "!foo(a)."),
+                                Arguments.of(LogicValue.UNKNOWN, "?foo(a)."), Arguments.of(LogicValue.ERROR, "foo(a): error."));
+        }
+
+        @Test
+        void implicitNodeTest() {
+                var pred = createPred();
+                var node = ProblemFactory.eINSTANCE.createNode();
+                node.setName("a");
+                problem.getNodes().add(node);
+                createAssertion(pred, node);
+
+                assertSerializedResult("""
+                                pred foo(node p).
+
+                                foo(a).
+                                """);
+        }
+
+        private PredicateDefinition createPred() {
+                var pred = ProblemFactory.eINSTANCE.createPredicateDefinition();
+                pred.setName("foo");
+                var parameter = ProblemFactory.eINSTANCE.createParameter();
+                var nodeType = testUtil.findClass(builtin, "node");
+                parameter.setParameterType(nodeType);
+                parameter.setName("p");
+                pred.getParameters().add(parameter);
+                problem.getStatements().add(pred);
+                return pred;
+        }
+
+        @Test
+        void newNodeTest() {
+                var classDeclaration = ProblemFactory.eINSTANCE.createClassDeclaration();
+                classDeclaration.setName("Foo");
+                var newNode = ProblemFactory.eINSTANCE.createNode();
+                newNode.setName("new");
+                classDeclaration.setNewNode(newNode);
+                problem.getStatements().add(classDeclaration);
+                createAssertion(classDeclaration, newNode);
+
+                assertSerializedResult("""
+                                class Foo.
+
+                                Foo(Foo::new).
+                                """);
+        }
+
+        private void createAssertion(Relation relation, Node node) {
+                createAssertion(relation, node, LogicValue.TRUE);
+        }
+
+        private void createAssertion(Relation relation, Node node, LogicValue value) {
+                var assertion = ProblemFactory.eINSTANCE.createAssertion();
+                assertion.setRelation(relation);
+                var argument = ProblemFactory.eINSTANCE.createNodeAssertionArgument();
+                argument.setNode(node);
+                assertion.getArguments().add(argument);
+                assertion.setValue(value);
+                problem.getStatements().add(assertion);
+        }
+
+        @Test
+        void implicitVariableTest() {
+                var pred = ProblemFactory.eINSTANCE.createPredicateDefinition();
+                pred.setName("foo");
+                var nodeType = testUtil.findClass(builtin, "node");
+                var parameter1 = ProblemFactory.eINSTANCE.createParameter();
+                parameter1.setParameterType(nodeType);
+                parameter1.setName("p1");
+                pred.getParameters().add(parameter1);
+                var parameter2 = ProblemFactory.eINSTANCE.createParameter();
+                parameter2.setParameterType(nodeType);
+                parameter2.setName("p2");
+                pred.getParameters().add(parameter2);
+                var conjunction = ProblemFactory.eINSTANCE.createConjunction();
+                var variable = ProblemFactory.eINSTANCE.createImplicitVariable();
+                variable.setName("q");
+                conjunction.getImplicitVariables().add(variable);
+                var equals = testUtil.reference(nodeType, "equals");
+                conjunction.getLiterals().add(createAtom(equals, parameter1, variable));
+                conjunction.getLiterals().add(createAtom(equals, variable, parameter2));
+                pred.getBodies().add(conjunction);
+                problem.getStatements().add(pred);
+
+                assertSerializedResult("""
+                                pred foo(node p1, node p2) <-> equals(p1, q), equals(q, p2).
+                                """);
+        }
+
+        private Atom createAtom(Relation relation, VariableOrNode variable1, VariableOrNode variable2) {
+                var atom = ProblemFactory.eINSTANCE.createAtom();
+                atom.setRelation(relation);
+                var arg1 = ProblemFactory.eINSTANCE.createVariableOrNodeArgument();
+                arg1.setVariableOrNode(variable1);
+                atom.getArguments().add(arg1);
+                var arg2 = ProblemFactory.eINSTANCE.createVariableOrNodeArgument();
+                arg2.setVariableOrNode(variable2);
+                atom.getArguments().add(arg2);
+                return atom;
+        }
+
+        @Test
+        void singletonVariableTest() {
+                var pred = ProblemFactory.eINSTANCE.createPredicateDefinition();
+                pred.setName("foo");
+                var nodeType = testUtil.findClass(builtin, "node");
+                var parameter = ProblemFactory.eINSTANCE.createParameter();
+                parameter.setParameterType(nodeType);
+                parameter.setName("p");
+                pred.getParameters().add(parameter);
+                var conjunction = ProblemFactory.eINSTANCE.createConjunction();
+                var atom = ProblemFactory.eINSTANCE.createAtom();
+                var equals = testUtil.reference(nodeType, "equals");
+                atom.setRelation(equals);
+                var arg1 = ProblemFactory.eINSTANCE.createVariableOrNodeArgument();
+                arg1.setVariableOrNode(parameter);
+                atom.getArguments().add(arg1);
+                var arg2 = ProblemFactory.eINSTANCE.createVariableOrNodeArgument();
+                var variable = ProblemFactory.eINSTANCE.createImplicitVariable();
+                variable.setName("_q");
+                arg2.setSingletonVariable(variable);
+                arg2.setVariableOrNode(variable);
+                atom.getArguments().add(arg2);
+                conjunction.getLiterals().add(atom);
+                pred.getBodies().add(conjunction);
+                problem.getStatements().add(pred);
+
+                assertSerializedResult("""
+                                pred foo(node p) <-> equals(p, _q).
+                                """);
+        }
+
+        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();
+
+                assertThat(problemString, equalTo(expected));
+        }
+}