4 files changed, 252 insertions, 111 deletions

diff --git a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/ModelInitializer.java b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/ModelInitializer.java
index 38bf5a61..c2bca2a5 100644
--- a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/ModelInitializer.java
+++ b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/ModelInitializer.java
@@ -6,7 +6,9 @@
 package tools.refinery.language.semantics;
 
 import com.google.inject.Inject;
+import tools.refinery.language.library.BuiltinLibrary;
 import tools.refinery.language.model.problem.*;
+import tools.refinery.language.scoping.imports.ImportCollector;
 import tools.refinery.language.semantics.internal.MutableSeed;
 import tools.refinery.language.utils.BuiltinSymbols;
 import tools.refinery.language.utils.ProblemDesugarer;
@@ -51,8 +53,13 @@ public class ModelInitializer {
         @Inject
         private ProblemTraceImpl problemTrace;
 
+        @Inject
+        private ImportCollector importCollector;
+
         private Problem problem;
 
+        private final Set<Problem> importedProblems = new HashSet<>();
+
         private BuiltinSymbols builtinSymbols;
 
         private PartialRelation nodeRelation;
@@ -82,6 +89,8 @@ public class ModelInitializer {
                         throw new IllegalArgumentException("Problem was already set");
                 }
                 this.problem = problem;
+                loadImportedProblems();
+                importedProblems.add(problem);
                 problemTrace.setProblem(problem);
                 try {
                         builtinSymbols = desugarer.getBuiltinSymbols(problem).orElseThrow(() -> new IllegalArgumentException(
@@ -128,6 +137,29 @@ public class ModelInitializer {
                 }
         }
 
+        private void loadImportedProblems() {
+                var resource = problem.eResource();
+                if (resource == null) {
+                        return;
+                }
+                var resourceSet = resource.getResourceSet();
+                if (resourceSet == null) {
+                        return;
+                }
+                var importedUris = importCollector.getAllImports(resource).toUriSet();
+                for (var uri : importedUris) {
+                        if (BuiltinLibrary.BUILTIN_LIBRARY_URI.equals(uri)) {
+                                // We hard-code the behavior of the builtin library.
+                                continue;
+                        }
+                        var importedResource = resourceSet.getResource(uri, false);
+                        if (importedResource != null && !importedResource.getContents().isEmpty() &&
+                                        importedResource.getContents().getFirst() instanceof Problem importedProblem) {
+                                importedProblems.add(importedProblem);
+                        }
+                }
+        }
+
         public void configureStoreBuilder(ModelStoreBuilder storeBuilder) {
                 checkProblem();
                 try {
@@ -168,19 +200,21 @@ public class ModelInitializer {
         }
 
         private void collectNodes() {
-                for (var statement : problem.getStatements()) {
-                        if (statement instanceof IndividualDeclaration individualDeclaration) {
-                                for (var individual : individualDeclaration.getNodes()) {
-                                        collectNode(individual);
-                                }
-                        } else if (statement instanceof ClassDeclaration classDeclaration) {
-                                var newNode = classDeclaration.getNewNode();
-                                if (newNode != null) {
-                                        collectNode(newNode);
-                                }
-                        } else if (statement instanceof EnumDeclaration enumDeclaration) {
-                                for (var literal : enumDeclaration.getLiterals()) {
-                                        collectNode(literal);
+                for (var importedProblem : importedProblems) {
+                        for (var statement : importedProblem.getStatements()) {
+                                if (statement instanceof NodeDeclaration nodeDeclaration) {
+                                        for (var node : nodeDeclaration.getNodes()) {
+                                                collectNode(node);
+                                        }
+                                } else if (statement instanceof ClassDeclaration classDeclaration) {
+                                        var newNode = classDeclaration.getNewNode();
+                                        if (newNode != null) {
+                                                collectNode(newNode);
+                                        }
+                                } else if (statement instanceof EnumDeclaration enumDeclaration) {
+                                        for (var literal : enumDeclaration.getLiterals()) {
+                                                collectNode(literal);
+                                        }
                                 }
                         }
                 }
@@ -194,13 +228,15 @@ public class ModelInitializer {
         }
 
         private void collectPartialSymbols() {
-                for (var statement : problem.getStatements()) {
-                        if (statement instanceof ClassDeclaration classDeclaration) {
-                                collectClassDeclarationSymbols(classDeclaration);
-                        } else if (statement instanceof EnumDeclaration enumDeclaration) {
-                                collectPartialRelation(enumDeclaration, 1, TruthValue.FALSE, TruthValue.FALSE);
-                        } else if (statement instanceof PredicateDefinition predicateDefinition) {
-                                collectPredicateDefinitionSymbol(predicateDefinition);
+                for (var importedProblem : importedProblems) {
+                        for (var statement : importedProblem.getStatements()) {
+                                if (statement instanceof ClassDeclaration classDeclaration) {
+                                        collectClassDeclarationSymbols(classDeclaration);
+                                } else if (statement instanceof EnumDeclaration enumDeclaration) {
+                                        collectPartialRelation(enumDeclaration, 1, TruthValue.FALSE, TruthValue.FALSE);
+                                } else if (statement instanceof PredicateDefinition predicateDefinition) {
+                                        collectPredicateDefinitionSymbol(predicateDefinition);
+                                }
                         }
                 }
         }
@@ -247,15 +283,17 @@ public class ModelInitializer {
         }
 
         private String getName(Relation relation) {
-                return semanticsUtils.getName(relation).orElseGet(() -> "::" + relationInfoMap.size());
+                return semanticsUtils.getNameWithoutRootPrefix(relation).orElseGet(() -> "::" + relationInfoMap.size());
         }
 
         private void collectMetamodel() {
-                for (var statement : problem.getStatements()) {
-                        if (statement instanceof ClassDeclaration classDeclaration) {
-                                collectClassDeclarationMetamodel(classDeclaration);
-                        } else if (statement instanceof EnumDeclaration enumDeclaration) {
-                                collectEnumMetamodel(enumDeclaration);
+                for (var importedProblem : importedProblems) {
+                        for (var statement : importedProblem.getStatements()) {
+                                if (statement instanceof ClassDeclaration classDeclaration) {
+                                        collectClassDeclarationMetamodel(classDeclaration);
+                                } else if (statement instanceof EnumDeclaration enumDeclaration) {
+                                        collectEnumMetamodel(enumDeclaration);
+                                }
                         }
                 }
         }
@@ -350,17 +388,17 @@ public class ModelInitializer {
         }
 
         private void collectAssertions() {
-                for (var statement : problem.getStatements()) {
-                        if (statement instanceof ClassDeclaration classDeclaration) {
-                                collectClassDeclarationAssertions(classDeclaration);
-                        } else if (statement instanceof EnumDeclaration enumDeclaration) {
-                                collectEnumAssertions(enumDeclaration);
-                        } else if (statement instanceof IndividualDeclaration individualDeclaration) {
-                                for (var individual : individualDeclaration.getNodes()) {
-                                        collectIndividualAssertions(individual);
+                for (var importedProblem : importedProblems) {
+                        for (var statement : importedProblem.getStatements()) {
+                                if (statement instanceof ClassDeclaration classDeclaration) {
+                                        collectClassDeclarationAssertions(classDeclaration);
+                                } else if (statement instanceof EnumDeclaration enumDeclaration) {
+                                        collectEnumAssertions(enumDeclaration);
+                                } else if (statement instanceof NodeDeclaration nodeDeclaration) {
+                                        collectNodeDeclarationAssertions(nodeDeclaration);
+                                } else if (statement instanceof Assertion assertion) {
+                                        collectAssertion(assertion);
                                 }
-                        } else if (statement instanceof Assertion assertion) {
-                                collectAssertion(assertion);
                         }
                 }
         }
@@ -379,7 +417,7 @@ public class ModelInitializer {
         private void collectEnumAssertions(EnumDeclaration enumDeclaration) {
                 var overlay = MutableSeed.of(1, null);
                 for (var literal : enumDeclaration.getLiterals()) {
-                        collectIndividualAssertions(literal);
+                        collectCardinalityAssertions(literal, TruthValue.TRUE);
                         var nodeId = getNodeId(literal);
                         overlay.mergeValue(Tuple.of(nodeId), TruthValue.TRUE);
                 }
@@ -387,9 +425,25 @@ public class ModelInitializer {
                 info.assertions().overwriteValues(overlay);
         }
 
-        private void collectIndividualAssertions(Node node) {
+        private void collectNodeDeclarationAssertions(NodeDeclaration nodeDeclaration) {
+                var kind = nodeDeclaration.getKind();
+                TruthValue value;
+                switch (kind) {
+                case ATOM -> value = TruthValue.TRUE;
+                case MULTI -> value = TruthValue.UNKNOWN;
+                case NODE -> {
+                        return;
+                }
+                default -> throw new IllegalArgumentException("Unknown node kind: " + kind);
+                }
+                for (var node : nodeDeclaration.getNodes()) {
+                        collectCardinalityAssertions(node, value);
+                }
+        }
+
+        private void collectCardinalityAssertions(Node node, TruthValue value) {
                 var nodeId = getNodeId(node);
-                collectCardinalityAssertions(nodeId, TruthValue.TRUE);
+                collectCardinalityAssertions(nodeId, value);
         }
 
         private void collectCardinalityAssertions(int nodeId, TruthValue value) {
@@ -415,9 +469,11 @@ public class ModelInitializer {
         }
 
         private void fixClassDeclarationAssertions() {
-                for (var statement : problem.getStatements()) {
-                        if (statement instanceof ClassDeclaration classDeclaration) {
-                                fixClassDeclarationAssertions(classDeclaration);
+                for (var importedProblem : importedProblems) {
+                        for (var statement : importedProblem.getStatements()) {
+                                if (statement instanceof ClassDeclaration classDeclaration) {
+                                        fixClassDeclarationAssertions(classDeclaration);
+                                }
                         }
                 }
         }
@@ -485,9 +541,11 @@ public class ModelInitializer {
         }
 
         private void collectPredicates(ModelStoreBuilder storeBuilder) {
-                for (var statement : problem.getStatements()) {
-                        if (statement instanceof PredicateDefinition predicateDefinition) {
-                                collectPredicateDefinitionTraced(predicateDefinition, storeBuilder);
+                for (var importedProblem : importedProblems) {
+                        for (var statement : importedProblem.getStatements()) {
+                                if (statement instanceof PredicateDefinition predicateDefinition) {
+                                        collectPredicateDefinitionTraced(predicateDefinition, storeBuilder);
+                                }
                         }
                 }
         }
@@ -587,18 +645,21 @@ public class ModelInitializer {
 
         private void toLiterals(Expr expr, Map<tools.refinery.language.model.problem.Variable, Variable> localScope,
                                                         List<Literal> literals) {
-                if (expr instanceof LogicConstant logicConstant) {
+                switch (expr) {
+                case LogicConstant logicConstant -> {
                         switch (logicConstant.getLogicValue()) {
                         case TRUE -> literals.add(BooleanLiteral.TRUE);
                         case FALSE -> literals.add(BooleanLiteral.FALSE);
                         default -> throw new TracedException(logicConstant, "Unsupported literal");
                         }
-                } else if (expr instanceof Atom atom) {
+                }
+                case Atom atom -> {
                         var target = getPartialRelation(atom.getRelation());
                         var polarity = atom.isTransitiveClosure() ? CallPolarity.TRANSITIVE : CallPolarity.POSITIVE;
                         var argumentList = toArgumentList(atom.getArguments(), localScope, literals);
                         literals.add(target.call(polarity, argumentList));
-                } else if (expr instanceof NegationExpr negationExpr) {
+                }
+                case NegationExpr negationExpr -> {
                         var body = negationExpr.getBody();
                         if (!(body instanceof Atom atom)) {
                                 throw new TracedException(body, "Cannot negate literal");
@@ -615,7 +676,8 @@ public class ModelInitializer {
                         var negatedScope = extendScope(localScope, negationExpr.getImplicitVariables());
                         var argumentList = toArgumentList(atom.getArguments(), negatedScope, literals);
                         literals.add(constraint.call(CallPolarity.NEGATIVE, argumentList));
-                } else if (expr instanceof ComparisonExpr comparisonExpr) {
+                }
+                case ComparisonExpr comparisonExpr -> {
                         var argumentList = toArgumentList(List.of(comparisonExpr.getLeft(), comparisonExpr.getRight()),
                                         localScope, literals);
                         boolean positive = switch (comparisonExpr.getOp()) {
@@ -625,8 +687,8 @@ public class ModelInitializer {
                                                 comparisonExpr, "Unsupported operator");
                         };
                         literals.add(new EquivalenceLiteral(positive, argumentList.get(0), argumentList.get(1)));
-                } else {
-                        throw new TracedException(expr, "Unsupported literal");
+                }
+                default -> throw new TracedException(expr, "Unsupported literal");
                 }
         }
 
@@ -641,7 +703,7 @@ public class ModelInitializer {
                         var variableOrNode = variableOrNodeExpr.getVariableOrNode();
                         if (variableOrNode instanceof Node node) {
                                 int nodeId = getNodeId(node);
-                                var tempVariable = Variable.of(semanticsUtils.getName(node).orElse("_" + nodeId));
+                                var tempVariable = Variable.of(semanticsUtils.getNameWithoutRootPrefix(node).orElse("_" + nodeId));
                                 literals.add(new ConstantLiteral(tempVariable, nodeId));
                                 argumentList.add(tempVariable);
                         } else if (variableOrNode instanceof tools.refinery.language.model.problem.Variable problemVariable) {
@@ -662,13 +724,15 @@ public class ModelInitializer {
         }
 
         private void collectScopes() {
-                for (var statement : problem.getStatements()) {
-                        if (statement instanceof ScopeDeclaration scopeDeclaration) {
-                                for (var typeScope : scopeDeclaration.getTypeScopes()) {
-                                        if (typeScope.isIncrement()) {
-                                                collectTypeScopeIncrement(typeScope);
-                                        } else {
-                                                collectTypeScope(typeScope);
+                for (var importedProblem : importedProblems) {
+                        for (var statement : importedProblem.getStatements()) {
+                                if (statement instanceof ScopeDeclaration scopeDeclaration) {
+                                        for (var typeScope : scopeDeclaration.getTypeScopes()) {
+                                                if (typeScope.isIncrement()) {
+                                                        collectTypeScopeIncrement(typeScope);
+                                                } else {
+                                                        collectTypeScope(typeScope);
+                                                }
                                         }
                                 }
                         }
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 f686e980..aef0fd89 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
@@ -79,7 +79,7 @@ class ProblemTraceImpl implements ProblemTrace {
                 try {
                         return nodeTrace.getOrThrow(node);
                 } catch (IllegalStateException e) {
-                        var qualifiedName = semanticsUtils.getName(node);
+                        var qualifiedName = semanticsUtils.getNameWithoutRootPrefix(node);
                         throw new TracedException(node, "No node ID for " + qualifiedName, e);
                 }
         }
@@ -144,7 +144,7 @@ class ProblemTraceImpl implements ProblemTrace {
         public PartialRelation getPartialRelation(Relation relation) {
                 var partialRelation = mutableRelationTrace.get(relation);
                 if (partialRelation == null) {
-                        var qualifiedName = semanticsUtils.getName(relation);
+                        var qualifiedName = semanticsUtils.getNameWithoutRootPrefix(relation);
                         throw new TracedException(relation, "No partial relation for " + qualifiedName);
                 }
                 return partialRelation;
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 b72ba697..9c40e6df 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
@@ -1,5 +1,5 @@
 /*
- * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ * SPDX-FileCopyrightText: 2023-2024 The Refinery Authors <https://refinery.tools/>
  *
  * SPDX-License-Identifier: EPL-2.0
  */
@@ -7,15 +7,20 @@ package tools.refinery.language.semantics;
 
 import com.google.inject.Inject;
 import com.google.inject.Singleton;
+import com.google.inject.name.Named;
+import org.eclipse.emf.ecore.EClass;
 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.resource.IEObjectDescription;
+import org.eclipse.xtext.resource.IResourceDescriptionsProvider;
 import org.eclipse.xtext.scoping.IScope;
 import org.jetbrains.annotations.NotNull;
 import org.jetbrains.annotations.Nullable;
 import tools.refinery.language.model.problem.Problem;
+import tools.refinery.language.naming.ProblemQualifiedNameProvider;
 
 import java.util.Optional;
 
@@ -25,10 +30,17 @@ public class SemanticsUtils {
         private IQualifiedNameProvider qualifiedNameProvider;
 
         @Inject
+        @Named(ProblemQualifiedNameProvider.NAMED_DELEGATE)
+        private IQualifiedNameProvider delegateQualifiedNameProvider;
+
+        @Inject
         private IQualifiedNameConverter qualifiedNameConverter;
 
-        public Optional<String> getName(EObject eObject) {
-                var qualifiedName = qualifiedNameProvider.getFullyQualifiedName(eObject);
+        @Inject
+        private IResourceDescriptionsProvider resourceDescriptionsProvider;
+
+        public Optional<String> getNameWithoutRootPrefix(EObject eObject) {
+                var qualifiedName = delegateQualifiedNameProvider.getFullyQualifiedName(eObject);
                 if (qualifiedName == null) {
                         return Optional.empty();
                 }
@@ -36,11 +48,31 @@ public class SemanticsUtils {
         }
 
         @Nullable
+        public <T> T maybeGetLocalElement(Problem problem, QualifiedName qualifiedName, Class<T> type, EClass eClass) {
+                var resource = problem.eResource();
+                var resourceSet = resource.getResourceSet();
+                var resourceDescriptions = resourceDescriptionsProvider.getResourceDescriptions(resourceSet);
+                var resourceDescription = resourceDescriptions.getResourceDescription(resource.getURI());
+                if (resourceDescription == null) {
+                        return null;
+                }
+                var eObjectDescriptions = resourceDescription.getExportedObjects(eClass, qualifiedName, false);
+                return maybeGet(problem, eObjectDescriptions, qualifiedName, type);
+        }
+
+        @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();
+                var eObjectDescriptions = scope.getElements(qualifiedName);
+                return maybeGet(problem, eObjectDescriptions, qualifiedName, type);
+        }
+
+        @Nullable
+        private <T> T maybeGet(Problem problem, Iterable<IEObjectDescription> eObjectDescriptions,
+                                                   QualifiedName qualifiedName, Class<T> type) {
+                var iterator = eObjectDescriptions.iterator();
                 if (!iterator.hasNext()) {
                         return null;
                 }
@@ -60,8 +92,19 @@ public class SemanticsUtils {
         }
 
         @NotNull
+        public <T> T getLocalElement(Problem problem, QualifiedName qualifiedName, Class<T> type, EClass eClass) {
+                var element = maybeGetLocalElement(problem, qualifiedName, type, eClass);
+                return getOrThrow(element, qualifiedName, type);
+        }
+
+        @NotNull
         public <T> T getElement(Problem problem, IScope scope, QualifiedName qualifiedName, Class<T> type) {
                 var element = maybeGetElement(problem, scope, qualifiedName, type);
+                return getOrThrow(element, qualifiedName, type);
+        }
+
+        @NotNull
+        private <T> T getOrThrow(@Nullable T element, QualifiedName qualifiedName, Class<T> type) {
                 if (element == null) {
                         var qualifiedNameString = qualifiedNameConverter.toString(qualifiedName);
                         throw new IllegalArgumentException("No such %s: %s"
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;
 import org.eclipse.collections.api.factory.primitive.IntObjectMaps;
 import org.eclipse.collections.api.map.primitive.MutableIntObjectMap;
 import org.eclipse.emf.common.util.URI;
+import org.eclipse.emf.ecore.EObject;
+import org.eclipse.emf.ecore.resource.Resource;
 import org.eclipse.emf.ecore.util.EcoreUtil;
 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.naming.NamingUtil;
 import tools.refinery.language.utils.ProblemDesugarer;
 import tools.refinery.language.utils.ProblemUtil;
 import tools.refinery.store.model.Model;
@@ -34,15 +36,11 @@ import tools.refinery.store.tuple.Tuple;
 import java.io.ByteArrayInputStream;
 import java.io.ByteArrayOutputStream;
 import java.io.IOException;
-import java.util.Map;
-import java.util.TreeMap;
-import java.util.TreeSet;
+import java.util.*;
 import java.util.function.Function;
 import java.util.stream.Collectors;
 
 public class SolutionSerializer {
-        private String fileExtension;
-
         @Inject
         private Provider<XtextResourceSet> resourceSetProvider;
 
@@ -68,16 +66,17 @@ public class SolutionSerializer {
         private Model model;
         private ReasoningAdapter reasoningAdapter;
         private PartialInterpretation<TruthValue, Boolean> existsInterpretation;
+        private Resource originalResource;
+        private Problem originalProblem;
+        private QualifiedName originalProblemName;
         private Problem problem;
+        private QualifiedName newProblemName;
+        private NodeDeclaration nodeDeclaration;
         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);
+                var uri = URI.createURI("__solution_%s.%s".formatted(UUID.randomUUID().toString().replace('-', '_'),
+                                ProblemUtil.MODULE_EXTENSION));
                 return serializeSolution(trace, model, uri);
         }
 
@@ -87,14 +86,26 @@ public class SolutionSerializer {
                 reasoningAdapter = model.getAdapter(ReasoningAdapter.class);
                 existsInterpretation = reasoningAdapter.getPartialInterpretation(Concreteness.CANDIDATE,
                                 ReasoningAdapter.EXISTS_SYMBOL);
-                var originalProblem = trace.getProblem();
+                originalProblem = trace.getProblem();
+                originalProblemName = qualifiedNameProvider.getFullyQualifiedName(originalProblem);
                 problem = copyProblem(originalProblem, uri);
+                problem.setKind(ProblemUtil.getDefaultModuleKind(uri));
+                problem.setExplicitKind(false);
+                problem.setName(null);
+                newProblemName = qualifiedNameProvider.getFullyQualifiedName(originalProblem);
                 problem.getStatements().removeIf(SolutionSerializer::shouldRemoveStatement);
-                problem.getNodes().removeIf(this::shouldRemoveNode);
+                removeNonExistentImplicitNodes();
+                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;
         }
 
@@ -102,15 +113,28 @@ public class SolutionSerializer {
                 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;
+        private void removeNonExistentImplicitNodes() {
+                var originalImplicitNodes = originalProblem.getNodes();
+                var newImplicitNodes = problem.getNodes();
+                if (newImplicitNodes.size() != originalImplicitNodes.size()) {
+                        throw new IllegalStateException("Expected %d implicit nodes in problem, but got %d after copying"
+                                        .formatted(originalImplicitNodes.size(), newImplicitNodes.size()));
+                }
+                var iterator = newImplicitNodes.iterator();
+                for (var originalNode : originalImplicitNodes) {
+                        if (!iterator.hasNext()) {
+                                throw new AssertionError("Unexpected end of copied implicit node list");
+                        }
+                        var newNode = iterator.next();
+                        if (!Objects.equals(originalNode.getName(), newNode.getName())) {
+                                throw new IllegalStateException("Expected copy of '%s' to have the same name, got '%s' instead"
+                                                .formatted(originalNode.getName(), newNode.getName()));
+                        }
+                        int nodeId = trace.getNodeId(originalNode);
+                        if (!isExistingNode(nodeId)) {
+                                iterator.remove();
+                        }
                 }
-                int nodeId = trace.getNodeId(originalNode);
-                return !isExistingNode(nodeId);
         }
 
         private boolean isExistingNode(int nodeId) {
@@ -122,13 +146,10 @@ public class SolutionSerializer {
         }
 
         private Problem copyProblem(Problem originalProblem, URI uri) {
-                var newResourceSet = resourceSetProvider.get();
-                if (!fileExtension.equals(uri.fileExtension())) {
-                        uri = uri.appendFileExtension(fileExtension);
-                }
+                originalResource = originalProblem.eResource();
+                var resourceSet = originalResource.getResourceSet();
                 var newResource = resourceFactory.createResource(uri);
-                newResourceSet.getResources().add(newResource);
-                var originalResource = originalProblem.eResource();
+                resourceSet.getResources().add(newResource);
                 if (originalResource instanceof XtextResource) {
                         byte[] bytes;
                         try {
@@ -143,6 +164,7 @@ public class SolutionSerializer {
                                 throw new IllegalStateException("Failed to copy problem", e);
                         }
                         var contents = newResource.getContents();
+                        EcoreUtil.resolveAll(newResource);
                         if (!contents.isEmpty() && contents.getFirst() instanceof Problem newProblem) {
                                 return newProblem;
                         }
@@ -154,10 +176,24 @@ public class SolutionSerializer {
                 }
         }
 
+        private QualifiedName getConvertedName(EObject original) {
+                var qualifiedName = qualifiedNameProvider.getFullyQualifiedName(original);
+                if (originalProblemName != null && qualifiedName.startsWith(originalProblemName)) {
+                        qualifiedName = qualifiedName.skipFirst(originalProblemName.getSegmentCount());
+                }
+                if (newProblemName != null) {
+                        qualifiedName = newProblemName.append(qualifiedName);
+                }
+                return NamingUtil.addRootPrefix(qualifiedName);
+        }
+
         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);
+                if (originalRelation.eResource() != originalResource) {
+                        return originalRelation;
+                }
+                var qualifiedName = getConvertedName(originalRelation);
+                return semanticsUtils.getLocalElement(problem, qualifiedName, Relation.class,
+                                ProblemPackage.Literals.RELATION);
         }
 
         private Relation findPartialRelation(PartialRelation partialRelation) {
@@ -165,13 +201,11 @@ public class SolutionSerializer {
         }
 
         private Node findNode(Node originalNode) {
-                var qualifiedName = qualifiedNameProvider.getFullyQualifiedName(originalNode);
-                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);
+                if (originalNode.eResource() != originalResource) {
+                        return originalNode;
+                }
+                var qualifiedName = getConvertedName(originalNode);
+                return semanticsUtils.maybeGetLocalElement(problem, qualifiedName, Node.class, ProblemPackage.Literals.NODE);
         }
 
         private void addAssertion(Relation relation, LogicValue value, Node... arguments) {
@@ -189,17 +223,17 @@ public class SolutionSerializer {
         }
 
         private void addExistsAssertions() {
-                var builtinSymbols = desugarer.getBuiltinSymbols(problem)
-                                .orElseThrow(() -> new IllegalStateException("No builtin library in copied problem"));
+                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)) {
+                        // Since all implicit nodes that do not exist has already been removed in serializeSolution,
+                        // we only need to add !exists assertions to ::new nodes and explicitly declared nodes that do not exist.
+                        if (ProblemUtil.isMultiNode(originalNode) || (ProblemUtil.isDeclaredNode(originalNode) && !isExistingNode(nodeId))) {
                                 sortedNewNodes.put(nodeId, newNode);
                         } else {
                                 nodes.put(nodeId, newNode);
@@ -212,8 +246,8 @@ public class SolutionSerializer {
         }
 
         private void addClassAssertions() {
-                var types = trace.getMetamodel().typeHierarchy().getPreservedTypes().keySet().stream()
-                                .collect(Collectors.toMap(Function.identity(), this::findPartialRelation));
+                var types =
+                                trace.getMetamodel().typeHierarchy().getPreservedTypes().keySet().stream().collect(Collectors.toMap(Function.identity(), this::findPartialRelation));
                 var cursor = model.getInterpretation(TypeHierarchyTranslator.TYPE_SYMBOL).getAll();
                 while (cursor.move()) {
                         var key = cursor.getKey();
@@ -237,7 +271,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);