refactor: serialize solutions as modules

2 files changed, 27 insertions, 7 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 537d94ca..1bd419d8 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
@@ -68,7 +68,9 @@ public class SolutionSerializer {
         private Model model;
         private ReasoningAdapter reasoningAdapter;
         private PartialInterpretation<TruthValue, Boolean> existsInterpretation;
+        private Problem originalProblem;
         private Problem problem;
+        private NodeDeclaration nodeDeclaration;
         private final MutableIntObjectMap<Node> nodes = IntObjectMaps.mutable.empty();
 
         @Inject
@@ -87,14 +89,22 @@ public class SolutionSerializer {
                 reasoningAdapter = model.getAdapter(ReasoningAdapter.class);
                 existsInterpretation = reasoningAdapter.getPartialInterpretation(Concreteness.CANDIDATE,
                                 ReasoningAdapter.EXISTS_SYMBOL);
-                var originalProblem = trace.getProblem();
+                originalProblem = trace.getProblem();
                 problem = copyProblem(originalProblem, uri);
+                problem.setKind(ModuleKind.MODULE);
                 problem.getStatements().removeIf(SolutionSerializer::shouldRemoveStatement);
                 problem.getNodes().removeIf(this::shouldRemoveNode);
+                nodeDeclaration = ProblemFactory.eINSTANCE.createNodeDeclaration();
+                nodeDeclaration.setKind(NodeKind.NODE);
+                nodeDeclaration.getNodes().addAll(problem.getNodes());
+                problem.getStatements().add(nodeDeclaration);
                 nameProvider.setProblem(problem);
                 addExistsAssertions();
                 addClassAssertions();
                 addReferenceAssertions();
+                if (nodeDeclaration.getNodes().isEmpty()) {
+                        problem.getStatements().remove(nodeDeclaration);
+                }
                 return problem;
         }
 
@@ -104,8 +114,8 @@ public class SolutionSerializer {
 
         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);
+                var scope = scopeProvider.getScope(originalProblem, ProblemPackage.Literals.NODE_ASSERTION_ARGUMENT__NODE);
+                var originalNode = semanticsUtils.maybeGetElement(originalProblem, scope, qualifiedName, Node.class);
                 if (originalNode == null) {
                         return false;
                 }
@@ -238,7 +248,7 @@ public class SolutionSerializer {
                         var nodeName = nameProvider.getNextName(typeName);
                         node = ProblemFactory.eINSTANCE.createNode();
                         node.setName(nodeName);
-                        problem.getNodes().add(node);
+                        nodeDeclaration.getNodes().add(node);
                         nodes.put(nodeId, node);
                 }
                 addAssertion(candidateRelation, LogicValue.TRUE, node);
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
index b682a7d6..949b7047 100644
--- 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
@@ -72,7 +72,7 @@ class SolutionSerializerTest {
                         solution.eResource().save(outputStream, Map.of());
                         actualOutput = outputStream.toString();
                 }
-                assertThat(actualOutput, is(prefix + "\n" + expectedOutput));
+                assertThat(actualOutput, is("module.\n\n" + prefix + "\n" + expectedOutput));
         }
 
         static Stream<Arguments> solutionSerializerTest() {
@@ -81,6 +81,7 @@ class SolutionSerializerTest {
                                 """, """
                                 scope Foo = 3.
                                 """, """
+                                declare foo1, foo2, foo3.
                                 !exists(Foo::new).
                                 Foo(foo1).
                                 Foo(foo2).
@@ -94,6 +95,7 @@ class SolutionSerializerTest {
                                 """, """
                                 scope Foo = 1.
                                 """, """
+                                declare foo1, bar1, bar2.
                                 !exists(Foo::new).
                                 !exists(Bar::new).
                                 Foo(foo1).
@@ -112,6 +114,7 @@ class SolutionSerializerTest {
                                 """, """
                                 scope Foo = 1, Bar = 2.
                                 """, """
+                                declare foo1, bar1, bar2.
                                 !exists(Foo::new).
                                 !exists(Bar::new).
                                 Foo(foo1).
@@ -131,6 +134,7 @@ class SolutionSerializerTest {
 
                                 scope Person += 0.
                                 """, """
+                                declare a, b, c.
                                 !exists(Person::new).
                                 Person(a).
                                 Person(b).
@@ -156,6 +160,7 @@ class SolutionSerializerTest {
 
                                 scope Foo += 0.
                                 """, """
+                                declare foo.
                                 !exists(Foo::new).
                                 Foo(foo).
                                 default !bar(*, *).
@@ -166,6 +171,7 @@ class SolutionSerializerTest {
                                 """, """
                                 scope Foo = 1, Bar = 0.
                                 """, """
+                                declare foo1.
                                 !exists(Foo::new).
                                 !exists(Bar::new).
                                 Foo(foo1).
@@ -180,6 +186,7 @@ class SolutionSerializerTest {
 
                                 scope Foo += 0.
                                 """, """
+                                declare a.
                                 !exists(Foo::new).
                                 Foo(a).
                                 default !ref(*, *).
@@ -200,29 +207,32 @@ class SolutionSerializerTest {
                                 !exists(Foo::new).
                                 scope Foo = 2.
                                 """, """
+                                declare foo1, foo2.
                                 !exists(a).
                                 !exists(Foo::new).
                                 Foo(foo1).
                                 Foo(foo2).
                                 """), Arguments.of("""
-                                node a.
+                                declare a.
                                 class Foo.
                                 """, """
                                 Foo(a).
                                 ?exists(a).
                                 scope Foo = 2, Foo += 1.
                                 """, """
+                                declare foo1.
                                 !exists(Foo::new).
                                 Foo(a).
                                 Foo(foo1).
                                 """), Arguments.of("""
-                                node a.
+                                declare a.
                                 class Foo.
                                 """, """
                                 Foo(a).
                                 ?exists(a).
                                 scope Foo = 1, Foo += 1.
                                 """, """
+                                declare foo1.
                                 !exists(a).
                                 !exists(Foo::new).
                                 Foo(foo1).