Merge pull request #39 from kris7t/partial-interpretation

Implement partial interpretation based model generation

18 files changed, 1179 insertions, 48 deletions

diff --git a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/metadata/BuiltInDetail.java b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/metadata/BuiltInDetail.java
new file mode 100644
index 00000000..6f706069
--- /dev/null
+++ b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/metadata/BuiltInDetail.java
@@ -0,0 +1,10 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.language.semantics.metadata;
+
+public record BuiltInDetail() implements RelationDetail {
+        public static final BuiltInDetail INSTANCE = new BuiltInDetail();
+}
diff --git a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/metadata/ClassDetail.java b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/metadata/ClassDetail.java
new file mode 100644
index 00000000..1d3190f5
--- /dev/null
+++ b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/metadata/ClassDetail.java
@@ -0,0 +1,16 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.language.semantics.metadata;
+
+public record ClassDetail(boolean abstractClass) implements RelationDetail {
+        public static final ClassDetail CONCRETE_CLASS = new ClassDetail(false);
+
+        public static final ClassDetail ABSTRACT_CLASS = new ClassDetail(true);
+
+        public static ClassDetail ofAbstractClass(boolean abstractClass) {
+                return abstractClass ? ABSTRACT_CLASS : CONCRETE_CLASS;
+        }
+}
diff --git a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/metadata/Metadata.java b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/metadata/Metadata.java
new file mode 100644
index 00000000..d2dcb43a
--- /dev/null
+++ b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/metadata/Metadata.java
@@ -0,0 +1,12 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.language.semantics.metadata;
+
+public sealed interface Metadata permits NodeMetadata, RelationMetadata {
+        String name();
+
+        String simpleName();
+}
diff --git a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/metadata/MetadataCreator.java b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/metadata/MetadataCreator.java
new file mode 100644
index 00000000..cc262129
--- /dev/null
+++ b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/metadata/MetadataCreator.java
@@ -0,0 +1,200 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.language.semantics.metadata;
+
+import com.google.inject.Inject;
+import org.eclipse.emf.ecore.EObject;
+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.eclipse.xtext.scoping.IScopeProvider;
+import tools.refinery.language.model.problem.*;
+import tools.refinery.language.semantics.model.ModelInitializer;
+import tools.refinery.language.semantics.model.TracedException;
+import tools.refinery.language.utils.ProblemUtil;
+import tools.refinery.store.reasoning.representation.PartialRelation;
+
+import java.util.*;
+
+public class MetadataCreator {
+        @Inject
+        private IScopeProvider scopeProvider;
+
+        @Inject
+        private IQualifiedNameProvider qualifiedNameProvider;
+
+        @Inject
+        private IQualifiedNameConverter qualifiedNameConverter;
+
+        private ModelInitializer initializer;
+
+        private IScope nodeScope;
+
+        private IScope relationScope;
+
+        public void setInitializer(ModelInitializer initializer) {
+                if (initializer == null) {
+                        throw new IllegalArgumentException("Initializer was already set");
+                }
+                this.initializer = initializer;
+                var problem = initializer.getProblem();
+                nodeScope = scopeProvider.getScope(problem, ProblemPackage.Literals.NODE_ASSERTION_ARGUMENT__NODE);
+                relationScope = scopeProvider.getScope(problem, ProblemPackage.Literals.ASSERTION__RELATION);
+        }
+
+        public static String unnamedNode(int nodeId) {
+                return "::" + nodeId;
+        }
+
+        public List<NodeMetadata> getNodesMetadata() {
+                return getNodesMetadata(initializer.getNodeCount(), true);
+        }
+
+        public List<NodeMetadata> getNodesMetadata(int nodeCount, boolean preserveNewNodes) {
+                var nodes = new NodeMetadata[Math.max(initializer.getNodeCount(), nodeCount)];
+                for (var entry : initializer.getNodeTrace().keyValuesView()) {
+                        var node = entry.getOne();
+                        var id = entry.getTwo();
+                        nodes[id] = getNodeMetadata(id, node, preserveNewNodes);
+                }
+                for (int i = 0; i < nodes.length; i++) {
+                        if (nodes[i] == null) {
+                                var nodeName = unnamedNode(i);
+                                nodes[i] = new NodeMetadata(nodeName, nodeName, NodeKind.IMPLICIT);
+                        }
+                }
+                return List.of(nodes);
+        }
+
+        private NodeMetadata getNodeMetadata(int nodeId, Node node, boolean preserveNewNodes) {
+                var kind = getNodeKind(node);
+                if (!preserveNewNodes && kind == NodeKind.NEW) {
+                        var nodeName = unnamedNode(nodeId);
+                        return new NodeMetadata(nodeName, nodeName, NodeKind.IMPLICIT);
+                }
+                var qualifiedName = getQualifiedName(node);
+                var simpleName = getSimpleName(node, qualifiedName, nodeScope);
+                return new NodeMetadata(qualifiedNameConverter.toString(qualifiedName),
+                                qualifiedNameConverter.toString(simpleName), getNodeKind(node));
+        }
+
+        private NodeKind getNodeKind(Node node) {
+                if (ProblemUtil.isImplicitNode(node)) {
+                        return NodeKind.IMPLICIT;
+                } else if (ProblemUtil.isIndividualNode(node)) {
+                        return NodeKind.INDIVIDUAL;
+                } else if (ProblemUtil.isNewNode(node)) {
+                        return NodeKind.NEW;
+                } else {
+                        throw new TracedException(node, "Unknown node type");
+                }
+        }
+
+        public List<RelationMetadata> getRelationsMetadata() {
+                var relationTrace = initializer.getRelationTrace();
+                var relations = new ArrayList<RelationMetadata>(relationTrace.size());
+                for (var entry : relationTrace.entrySet()) {
+                        var relation = entry.getKey();
+                        var partialRelation = entry.getValue();
+                        var metadata = getRelationMetadata(relation, partialRelation);
+                        relations.add(metadata);
+                }
+                return Collections.unmodifiableList(relations);
+        }
+
+        private RelationMetadata getRelationMetadata(Relation relation, PartialRelation partialRelation) {
+                var qualifiedName = getQualifiedName(relation);
+                var qualifiedNameString = qualifiedNameConverter.toString(qualifiedName);
+                var simpleName = getSimpleName(relation, qualifiedName, relationScope);
+                var simpleNameString = qualifiedNameConverter.toString(simpleName);
+                var arity = partialRelation.arity();
+                var detail = getRelationDetail(relation, partialRelation);
+                return new RelationMetadata(qualifiedNameString, simpleNameString, arity, detail);
+        }
+
+        private RelationDetail getRelationDetail(Relation relation, PartialRelation partialRelation) {
+                if (ProblemUtil.isBuiltIn(relation) && !ProblemUtil.isError(relation)) {
+                        return getBuiltInDetail();
+                }
+                if (relation instanceof ClassDeclaration classDeclaration) {
+                        return getClassDetail(classDeclaration);
+                } else if (relation instanceof ReferenceDeclaration) {
+                        return getReferenceDetail(partialRelation);
+                } else if (relation instanceof EnumDeclaration) {
+                        return getEnumDetail();
+                } else if (relation instanceof PredicateDefinition predicateDefinition) {
+                        return getPredicateDetail(predicateDefinition);
+                } else {
+                        throw new TracedException(relation, "Unknown relation");
+                }
+        }
+
+        private RelationDetail getBuiltInDetail() {
+                return BuiltInDetail.INSTANCE;
+        }
+
+        private RelationDetail getClassDetail(ClassDeclaration classDeclaration) {
+                return ClassDetail.ofAbstractClass(classDeclaration.isAbstract());
+        }
+
+        private RelationDetail getReferenceDetail(PartialRelation partialRelation) {
+                var metamodel = initializer.getMetamodel();
+                var opposite = metamodel.oppositeReferences().get(partialRelation);
+                if (opposite == null) {
+                        boolean isContainment = metamodel.containmentHierarchy().containsKey(partialRelation);
+                        return ReferenceDetail.ofContainment(isContainment);
+                } else {
+                        boolean isContainer = metamodel.containmentHierarchy().containsKey(opposite);
+                        return new OppositeReferenceDetail(isContainer, opposite.name());
+                }
+        }
+
+        private RelationDetail getEnumDetail() {
+                return ClassDetail.CONCRETE_CLASS;
+        }
+
+        private RelationDetail getPredicateDetail(PredicateDefinition predicate) {
+                return PredicateDetail.ofError(predicate.isError());
+        }
+
+        private QualifiedName getQualifiedName(EObject eObject) {
+                var qualifiedName = qualifiedNameProvider.getFullyQualifiedName(eObject);
+                if (qualifiedName == null) {
+                        throw new TracedException(eObject, "Unknown qualified name");
+                }
+                return qualifiedName;
+        }
+
+        private QualifiedName getSimpleName(EObject eObject, QualifiedName qualifiedName, IScope scope) {
+                var descriptions = scope.getElements(eObject);
+                var names = new HashSet<QualifiedName>();
+                for (var description : descriptions) {
+                        // {@code getQualifiedName()} will refer to the full name for objects that are loaded from the global
+                        // scope, but {@code getName()} returns the qualified name that we set in
+                        // {@code ProblemResourceDescriptionStrategy}.
+                        names.add(description.getName());
+                }
+                var iterator = names.stream().sorted(Comparator.comparingInt(QualifiedName::getSegmentCount)).iterator();
+                while (iterator.hasNext()) {
+                        var simpleName = iterator.next();
+                        if (names.contains(simpleName) && isUnique(scope, simpleName)) {
+                                return simpleName;
+                        }
+                }
+                throw new TracedException(eObject, "Ambiguous qualified name: " +
+                                qualifiedNameConverter.toString(qualifiedName));
+        }
+
+        private boolean isUnique(IScope scope, QualifiedName name) {
+                var iterator = scope.getElements(name).iterator();
+                if (!iterator.hasNext()) {
+                        return false;
+                }
+                iterator.next();
+                return !iterator.hasNext();
+        }
+}
diff --git a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/metadata/NodeKind.java b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/metadata/NodeKind.java
new file mode 100644
index 00000000..01f0cd09
--- /dev/null
+++ b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/metadata/NodeKind.java
@@ -0,0 +1,12 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.language.semantics.metadata;
+
+public enum NodeKind {
+        IMPLICIT,
+        INDIVIDUAL,
+        NEW
+}
diff --git a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/metadata/NodeMetadata.java b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/metadata/NodeMetadata.java
new file mode 100644
index 00000000..812952c0
--- /dev/null
+++ b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/metadata/NodeMetadata.java
@@ -0,0 +1,9 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.language.semantics.metadata;
+
+public record NodeMetadata(String name, String simpleName, NodeKind kind) implements Metadata {
+}
diff --git a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/metadata/OppositeReferenceDetail.java b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/metadata/OppositeReferenceDetail.java
new file mode 100644
index 00000000..26d7461c
--- /dev/null
+++ b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/metadata/OppositeReferenceDetail.java
@@ -0,0 +1,9 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.language.semantics.metadata;
+
+public record OppositeReferenceDetail(boolean container, String opposite) implements RelationDetail {
+}
diff --git a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/metadata/PredicateDetail.java b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/metadata/PredicateDetail.java
new file mode 100644
index 00000000..ca397eca
--- /dev/null
+++ b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/metadata/PredicateDetail.java
@@ -0,0 +1,16 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.language.semantics.metadata;
+
+public record PredicateDetail(boolean error) implements RelationDetail {
+        public static final PredicateDetail PREDICATE = new PredicateDetail(false);
+
+        public static final PredicateDetail ERROR_PREDICATE = new PredicateDetail(true);
+
+        public static PredicateDetail ofError(boolean error) {
+                return error ? ERROR_PREDICATE : PREDICATE;
+        }
+}
diff --git a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/metadata/ReferenceDetail.java b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/metadata/ReferenceDetail.java
new file mode 100644
index 00000000..36771566
--- /dev/null
+++ b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/metadata/ReferenceDetail.java
@@ -0,0 +1,16 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.language.semantics.metadata;
+
+public record ReferenceDetail(boolean containment) implements RelationDetail {
+        public static final ReferenceDetail CROSS_REFERENCE = new ReferenceDetail(false);
+
+        public static final ReferenceDetail CONTAINMENT_REFERENCE = new ReferenceDetail(true);
+
+        public static ReferenceDetail ofContainment(boolean containment) {
+                return containment ? CONTAINMENT_REFERENCE : CROSS_REFERENCE;
+        }
+}
diff --git a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/metadata/RelationDetail.java b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/metadata/RelationDetail.java
new file mode 100644
index 00000000..105179fd
--- /dev/null
+++ b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/metadata/RelationDetail.java
@@ -0,0 +1,10 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.language.semantics.metadata;
+
+public sealed interface RelationDetail permits ClassDetail, ReferenceDetail, PredicateDetail, OppositeReferenceDetail,
+                BuiltInDetail {
+}
diff --git a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/metadata/RelationMetadata.java b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/metadata/RelationMetadata.java
new file mode 100644
index 00000000..5abcc253
--- /dev/null
+++ b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/metadata/RelationMetadata.java
@@ -0,0 +1,9 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.language.semantics.metadata;
+
+public record RelationMetadata(String name, String simpleName, int arity, RelationDetail detail) implements Metadata {
+}
diff --git a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/model/ModelInitializer.java b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/model/ModelInitializer.java
index 06b8ad77..85c8d701 100644
--- a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/model/ModelInitializer.java
+++ b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/model/ModelInitializer.java
@@ -9,67 +9,408 @@ import com.google.inject.Inject;
 import org.eclipse.collections.api.factory.primitive.ObjectIntMaps;
 import org.eclipse.collections.api.map.primitive.MutableObjectIntMap;
 import tools.refinery.language.model.problem.*;
-import tools.refinery.language.semantics.model.internal.DecisionTree;
+import tools.refinery.language.semantics.model.internal.MutableSeed;
+import tools.refinery.language.utils.BuiltinSymbols;
 import tools.refinery.language.utils.ProblemDesugarer;
-import tools.refinery.language.utils.RelationInfo;
-import tools.refinery.store.representation.Symbol;
+import tools.refinery.language.utils.ProblemUtil;
+import tools.refinery.store.dse.propagation.PropagationBuilder;
+import tools.refinery.store.model.ModelStoreBuilder;
+import tools.refinery.store.query.Constraint;
+import tools.refinery.store.query.dnf.InvalidClauseException;
+import tools.refinery.store.query.dnf.Query;
+import tools.refinery.store.query.dnf.RelationalQuery;
+import tools.refinery.store.query.literal.*;
+import tools.refinery.store.query.term.NodeVariable;
+import tools.refinery.store.query.term.Variable;
+import tools.refinery.store.reasoning.ReasoningAdapter;
+import tools.refinery.store.reasoning.representation.AnyPartialSymbol;
+import tools.refinery.store.reasoning.representation.PartialRelation;
+import tools.refinery.store.reasoning.scope.ScopePropagator;
+import tools.refinery.store.reasoning.seed.ModelSeed;
+import tools.refinery.store.reasoning.seed.Seed;
+import tools.refinery.store.reasoning.translator.containment.ContainmentHierarchyTranslator;
+import tools.refinery.store.reasoning.translator.metamodel.Metamodel;
+import tools.refinery.store.reasoning.translator.metamodel.MetamodelBuilder;
+import tools.refinery.store.reasoning.translator.metamodel.MetamodelTranslator;
+import tools.refinery.store.reasoning.translator.multiobject.MultiObjectTranslator;
+import tools.refinery.store.reasoning.translator.multiplicity.ConstrainedMultiplicity;
+import tools.refinery.store.reasoning.translator.multiplicity.Multiplicity;
+import tools.refinery.store.reasoning.translator.multiplicity.UnconstrainedMultiplicity;
+import tools.refinery.store.reasoning.translator.predicate.PredicateTranslator;
 import tools.refinery.store.representation.TruthValue;
+import tools.refinery.store.representation.cardinality.CardinalityInterval;
+import tools.refinery.store.representation.cardinality.CardinalityIntervals;
+import tools.refinery.store.representation.cardinality.UpperCardinalities;
 import tools.refinery.store.tuple.Tuple;
 
-import java.util.HashMap;
-import java.util.Map;
+import java.util.*;
 
 public class ModelInitializer {
         @Inject
         private ProblemDesugarer desugarer;
 
+        @Inject
+        private SemanticsUtils semanticsUtils;
+
+        private Problem problem;
+
+        private ModelStoreBuilder storeBuilder;
+
+        private BuiltinSymbols builtinSymbols;
+
+        private PartialRelation nodeRelation;
+
         private final MutableObjectIntMap<Node> nodeTrace = ObjectIntMaps.mutable.empty();
 
-        private final Map<tools.refinery.language.model.problem.Relation, Symbol<TruthValue>> relationTrace =
-                        new HashMap<>();
+        private final Map<Relation, RelationInfo> relationInfoMap = new LinkedHashMap<>();
+
+        private final Map<PartialRelation, RelationInfo> partialRelationInfoMap = new HashMap<>();
+
+        private final Map<AnyPartialSymbol, Relation> inverseTrace = new HashMap<>();
+
+        private Map<Relation, PartialRelation> relationTrace;
+
+        private final MetamodelBuilder metamodelBuilder = Metamodel.builder();
+
+        private Metamodel metamodel;
+
+        private final Map<Tuple, CardinalityInterval> countSeed = new LinkedHashMap<>();
+
+        private ScopePropagator scopePropagator;
+
+        private ModelSeed modelSeed;
+
+        public Problem getProblem() {
+                return problem;
+        }
+
+        public int getNodeCount() {
+                return nodeTrace.size();
+        }
+
+        public MutableObjectIntMap<Node> getNodeTrace() {
+                return nodeTrace;
+        }
+
+        public Map<Relation, PartialRelation> getRelationTrace() {
+                return relationTrace;
+        }
 
-        private int nodeCount = 0;
+        public Relation getInverseTrace(AnyPartialSymbol partialRelation) {
+                return inverseTrace.get(partialRelation);
+        }
+
+        public Metamodel getMetamodel() {
+                return metamodel;
+        }
 
-        public void createModel(Problem problem) {
-                var builtinSymbols = desugarer.getBuiltinSymbols(problem).orElseThrow(() -> new IllegalArgumentException(
+        public ModelSeed createModel(Problem problem, ModelStoreBuilder storeBuilder) {
+                this.problem = problem;
+                this.storeBuilder = storeBuilder;
+                builtinSymbols = desugarer.getBuiltinSymbols(problem).orElseThrow(() -> new IllegalArgumentException(
                                 "Problem has no builtin library"));
-                var collectedSymbols = desugarer.collectSymbols(problem);
-                for (var node : collectedSymbols.nodes().keySet()) {
-                        nodeTrace.put(node, nodeCount);
-                        nodeCount += 1;
-                }
-                for (var pair : collectedSymbols.relations().entrySet()) {
-                        var relation = pair.getKey();
-                        var relationInfo = pair.getValue();
-                        var isEqualsRelation = relation == builtinSymbols.equals();
-                        var decisionTree = mergeAssertions(relationInfo, isEqualsRelation);
-                        var defaultValue = isEqualsRelation ? TruthValue.FALSE : TruthValue.UNKNOWN;
-                        relationTrace.put(relation, Symbol.of(
-                                        relationInfo.name(), relationInfo.arity(), TruthValue.class, defaultValue));
-                }
-        }
-
-        private DecisionTree mergeAssertions(RelationInfo relationInfo, boolean isEqualsRelation) {
-                var arity = relationInfo.arity();
-                var defaultAssertions = new DecisionTree(arity, isEqualsRelation ? null : TruthValue.UNKNOWN);
-                var assertions = new DecisionTree(arity);
-                for (var assertion : relationInfo.assertions()) {
-                        var tuple = getTuple(assertion);
-                        var value = getTruthValue(assertion.getValue());
-                        if (assertion.isDefault()) {
-                                defaultAssertions.mergeValue(tuple, value);
+                var nodeInfo = collectPartialRelation(builtinSymbols.node(), 1, TruthValue.TRUE, TruthValue.TRUE);
+                nodeRelation = nodeInfo.partialRelation();
+                metamodelBuilder.type(nodeRelation);
+                putRelationInfo(builtinSymbols.exists(), new RelationInfo(ReasoningAdapter.EXISTS_SYMBOL, null,
+                                TruthValue.TRUE));
+                putRelationInfo(builtinSymbols.equals(), new RelationInfo(ReasoningAdapter.EQUALS_SYMBOL,
+                                (TruthValue) null,
+                                null));
+                putRelationInfo(builtinSymbols.contained(), new RelationInfo(ContainmentHierarchyTranslator.CONTAINED_SYMBOL,
+                                null, TruthValue.UNKNOWN));
+                putRelationInfo(builtinSymbols.contains(), new RelationInfo(ContainmentHierarchyTranslator.CONTAINS_SYMBOL,
+                                null, TruthValue.UNKNOWN));
+                putRelationInfo(builtinSymbols.invalidContainer(),
+                                new RelationInfo(ContainmentHierarchyTranslator.INVALID_CONTAINER, TruthValue.FALSE,
+                                                TruthValue.FALSE));
+                collectNodes();
+                collectPartialSymbols();
+                collectMetamodel();
+                metamodel = metamodelBuilder.build();
+                collectAssertions();
+                storeBuilder.with(new MultiObjectTranslator());
+                storeBuilder.with(new MetamodelTranslator(metamodel));
+                relationTrace = new LinkedHashMap<>(relationInfoMap.size());
+                int nodeCount = getNodeCount();
+                var modelSeedBuilder = ModelSeed.builder(nodeCount);
+                for (var entry : relationInfoMap.entrySet()) {
+                        var relation = entry.getKey();
+                        var info = entry.getValue();
+                        var partialRelation = info.partialRelation();
+                        relationTrace.put(relation, partialRelation);
+                        modelSeedBuilder.seed(partialRelation, info.toSeed(nodeCount));
+                }
+                collectScopes();
+                if (scopePropagator != null) {
+                        if (storeBuilder.tryGetAdapter(PropagationBuilder.class).isEmpty()) {
+                                throw new TracedException(problem, "Type scopes require a PropagationBuilder");
+                        }
+                        storeBuilder.with(scopePropagator);
+                }
+                modelSeedBuilder.seed(MultiObjectTranslator.COUNT_SYMBOL, builder -> builder
+                                .reducedValue(CardinalityIntervals.SET)
+                                .putAll(countSeed));
+                modelSeed = modelSeedBuilder.build();
+                collectPredicates();
+                return modelSeed;
+        }
+
+        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 node : problem.getNodes()) {
+                        collectNode(node);
+                }
+        }
+
+        private void collectNode(Node node) {
+                nodeTrace.getIfAbsentPut(node, this::getNodeCount);
+        }
+
+        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);
+                        }
+                }
+        }
+
+        private void collectClassDeclarationSymbols(ClassDeclaration classDeclaration) {
+                collectPartialRelation(classDeclaration, 1, null, TruthValue.UNKNOWN);
+                for (var featureDeclaration : classDeclaration.getFeatureDeclarations()) {
+                        if (featureDeclaration instanceof ReferenceDeclaration referenceDeclaration) {
+                                collectPartialRelation(referenceDeclaration, 2, null, TruthValue.UNKNOWN);
+                                var invalidMultiplicityConstraint = referenceDeclaration.getInvalidMultiplicity();
+                                if (invalidMultiplicityConstraint != null) {
+                                        collectPartialRelation(invalidMultiplicityConstraint, 1, TruthValue.FALSE, TruthValue.FALSE);
+                                }
                         } else {
-                                assertions.mergeValue(tuple, value);
+                                throw new TracedException(featureDeclaration, "Unknown feature declaration");
+                        }
+                }
+        }
+
+        private void collectPredicateDefinitionSymbol(PredicateDefinition predicateDefinition) {
+                int arity = predicateDefinition.getParameters().size();
+                if (predicateDefinition.isError()) {
+                        collectPartialRelation(predicateDefinition, arity, TruthValue.FALSE, TruthValue.FALSE);
+                } else {
+                        collectPartialRelation(predicateDefinition, arity, null, TruthValue.UNKNOWN);
+                }
+        }
+
+        private void putRelationInfo(Relation relation, RelationInfo info) {
+                relationInfoMap.put(relation, info);
+                partialRelationInfoMap.put(info.partialRelation(), info);
+                inverseTrace.put(info.partialRelation(), relation);
+        }
+
+        private RelationInfo collectPartialRelation(Relation relation, int arity, TruthValue value,
+                                                                                                TruthValue defaultValue) {
+                return relationInfoMap.computeIfAbsent(relation, key -> {
+                        var name = getName(relation);
+                        var info = new RelationInfo(name, arity, value, defaultValue);
+                        partialRelationInfoMap.put(info.partialRelation(), info);
+                        inverseTrace.put(info.partialRelation(), relation);
+                        return info;
+                });
+        }
+
+        private String getName(Relation relation) {
+                return semanticsUtils.getName(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);
+                        }
+                }
+        }
+
+        private void collectEnumMetamodel(EnumDeclaration enumDeclaration) {
+                try {
+                        metamodelBuilder.type(getPartialRelation(enumDeclaration), nodeRelation);
+                } catch (RuntimeException e) {
+                        throw TracedException.addTrace(enumDeclaration, e);
+                }
+        }
+
+        private void collectClassDeclarationMetamodel(ClassDeclaration classDeclaration) {
+                var superTypes = classDeclaration.getSuperTypes();
+                var partialSuperTypes = new ArrayList<PartialRelation>(superTypes.size() + 1);
+                partialSuperTypes.add(nodeRelation);
+                for (var superType : superTypes) {
+                        partialSuperTypes.add(getPartialRelation(superType));
+                }
+                try {
+                        metamodelBuilder.type(getPartialRelation(classDeclaration), classDeclaration.isAbstract(),
+                                        partialSuperTypes);
+                } catch (RuntimeException e) {
+                        throw TracedException.addTrace(classDeclaration, e);
+                }
+                for (var featureDeclaration : classDeclaration.getFeatureDeclarations()) {
+                        if (featureDeclaration instanceof ReferenceDeclaration referenceDeclaration) {
+                                collectReferenceDeclarationMetamodel(classDeclaration, referenceDeclaration);
                         }
                 }
-                defaultAssertions.overwriteValues(assertions);
-                if (isEqualsRelation) {
-                        for (int i = 0; i < nodeCount; i++) {
-                                defaultAssertions.setIfMissing(Tuple.of(i, i), TruthValue.TRUE);
+        }
+
+        private void collectReferenceDeclarationMetamodel(ClassDeclaration classDeclaration,
+                                                                                                          ReferenceDeclaration referenceDeclaration) {
+                var relation = getPartialRelation(referenceDeclaration);
+                var source = getPartialRelation(classDeclaration);
+                var target = getPartialRelation(referenceDeclaration.getReferenceType());
+                boolean containment = referenceDeclaration.getKind() == ReferenceKind.CONTAINMENT;
+                var opposite = referenceDeclaration.getOpposite();
+                PartialRelation oppositeRelation = null;
+                if (opposite != null) {
+                        oppositeRelation = getPartialRelation(opposite);
+                }
+                var multiplicity = getMultiplicityConstraint(referenceDeclaration);
+                try {
+                        metamodelBuilder.reference(relation, source, containment, multiplicity, target, oppositeRelation);
+                } catch (RuntimeException e) {
+                        throw TracedException.addTrace(classDeclaration, e);
+                }
+        }
+
+        private Multiplicity getMultiplicityConstraint(ReferenceDeclaration referenceDeclaration) {
+                if (!ProblemUtil.hasMultiplicityConstraint(referenceDeclaration)) {
+                        return UnconstrainedMultiplicity.INSTANCE;
+                }
+                var problemMultiplicity = referenceDeclaration.getMultiplicity();
+                CardinalityInterval interval;
+                if (problemMultiplicity == null) {
+                        interval = CardinalityIntervals.LONE;
+                } else {
+                        interval = getCardinalityInterval(problemMultiplicity);
+                }
+                var constraint = getRelationInfo(referenceDeclaration.getInvalidMultiplicity()).partialRelation();
+                return ConstrainedMultiplicity.of(interval, constraint);
+        }
+
+        private static CardinalityInterval getCardinalityInterval(
+                        tools.refinery.language.model.problem.Multiplicity problemMultiplicity) {
+                if (problemMultiplicity instanceof ExactMultiplicity exactMultiplicity) {
+                        return CardinalityIntervals.exactly(exactMultiplicity.getExactValue());
+                } else if (problemMultiplicity instanceof RangeMultiplicity rangeMultiplicity) {
+                        var upperBound = rangeMultiplicity.getUpperBound();
+                        return CardinalityIntervals.between(rangeMultiplicity.getLowerBound(),
+                                        upperBound < 0 ? UpperCardinalities.UNBOUNDED : UpperCardinalities.atMost(upperBound));
+                } else {
+                        throw new TracedException(problemMultiplicity, "Unknown multiplicity");
+                }
+        }
+
+        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);
+                                }
+                        } else if (statement instanceof Assertion assertion) {
+                                collectAssertion(assertion);
                         }
-                        defaultAssertions.setAllMissing(TruthValue.FALSE);
                 }
-                return defaultAssertions;
+        }
+
+        private void collectClassDeclarationAssertions(ClassDeclaration classDeclaration) {
+                var newNode = classDeclaration.getNewNode();
+                if (newNode == null) {
+                        return;
+                }
+                var newNodeId = getNodeId(newNode);
+                collectCardinalityAssertions(newNodeId, TruthValue.UNKNOWN);
+                var tuple = Tuple.of(newNodeId);
+                mergeValue(classDeclaration, tuple, TruthValue.TRUE);
+                var typeInfo = metamodel.typeHierarchy().getAnalysisResult(getPartialRelation(classDeclaration));
+                for (var subType : typeInfo.getDirectSubtypes()) {
+                        partialRelationInfoMap.get(subType).assertions().mergeValue(tuple, TruthValue.FALSE);
+                }
+        }
+
+        private void collectEnumAssertions(EnumDeclaration enumDeclaration) {
+                var overlay = MutableSeed.of(1, null);
+                for (var literal : enumDeclaration.getLiterals()) {
+                        collectIndividualAssertions(literal);
+                        var nodeId = getNodeId(literal);
+                        overlay.mergeValue(Tuple.of(nodeId), TruthValue.TRUE);
+                }
+                var info = getRelationInfo(enumDeclaration);
+                info.assertions().overwriteValues(overlay);
+        }
+
+        private void collectIndividualAssertions(Node node) {
+                var nodeId = getNodeId(node);
+                collectCardinalityAssertions(nodeId, TruthValue.TRUE);
+        }
+
+        private void collectCardinalityAssertions(int nodeId, TruthValue value) {
+                mergeValue(builtinSymbols.exists(), Tuple.of(nodeId), value);
+                mergeValue(builtinSymbols.equals(), Tuple.of(nodeId, nodeId), value);
+        }
+
+        private void collectAssertion(Assertion assertion) {
+                var tuple = getTuple(assertion);
+                var value = getTruthValue(assertion.getValue());
+                var relation = assertion.getRelation();
+                var info = getRelationInfo(relation);
+                var partialRelation = info.partialRelation();
+                if (partialRelation.arity() != tuple.getSize()) {
+                        throw new TracedException(assertion, "Expected %d arguments for %s, got %d instead"
+                                        .formatted(partialRelation.arity(), partialRelation, tuple.getSize()));
+                }
+                if (assertion.isDefault()) {
+                        info.defaultAssertions().mergeValue(tuple, value);
+                } else {
+                        info.assertions().mergeValue(tuple, value);
+                }
+        }
+
+        private void mergeValue(Relation relation, Tuple key, TruthValue value) {
+                getRelationInfo(relation).assertions().mergeValue(key, value);
+        }
+
+        private RelationInfo getRelationInfo(Relation relation) {
+                var info = relationInfoMap.get(relation);
+                if (info == null) {
+                        throw new IllegalArgumentException("Unknown relation: " + relation);
+                }
+                return info;
+        }
+
+        private PartialRelation getPartialRelation(Relation relation) {
+                return getRelationInfo(relation).partialRelation();
+        }
+
+        private int getNodeId(Node node) {
+                return nodeTrace.getOrThrow(node);
         }
 
         private Tuple getTuple(Assertion assertion) {
@@ -79,11 +420,11 @@ public class ModelInitializer {
                 for (int i = 0; i < arity; i++) {
                         var argument = arguments.get(i);
                         if (argument instanceof NodeAssertionArgument nodeArgument) {
-                                nodes[i] = nodeTrace.getOrThrow(nodeArgument.getNode());
+                                nodes[i] = getNodeId(nodeArgument.getNode());
                         } else if (argument instanceof WildcardAssertionArgument) {
                                 nodes[i] = -1;
                         } else {
-                                throw new IllegalArgumentException("Unknown assertion argument: " + argument);
+                                throw new TracedException(argument, "Unsupported assertion argument");
                         }
                 }
                 return Tuple.of(nodes);
@@ -100,4 +441,249 @@ public class ModelInitializer {
                         case ERROR -> TruthValue.ERROR;
                 };
         }
+
+        private void collectPredicates() {
+                for (var statement : problem.getStatements()) {
+                        if (statement instanceof PredicateDefinition predicateDefinition) {
+                                collectPredicateDefinitionTraced(predicateDefinition);
+                        }
+                }
+        }
+
+        private void collectPredicateDefinitionTraced(PredicateDefinition predicateDefinition) {
+                try {
+                        collectPredicateDefinition(predicateDefinition);
+                } catch (InvalidClauseException e) {
+                        int clauseIndex = e.getClauseIndex();
+                        var bodies = predicateDefinition.getBodies();
+                        if (clauseIndex < bodies.size()) {
+                                throw new TracedException(bodies.get(clauseIndex), e);
+                        } else {
+                                throw new TracedException(predicateDefinition, e);
+                        }
+                } catch (RuntimeException e) {
+                        throw TracedException.addTrace(predicateDefinition, e);
+                }
+        }
+
+        private void collectPredicateDefinition(PredicateDefinition predicateDefinition) {
+                var partialRelation = getPartialRelation(predicateDefinition);
+                var query = toQuery(partialRelation.name(), predicateDefinition);
+                boolean mutable;
+                TruthValue defaultValue;
+                if (predicateDefinition.isError()) {
+                        mutable = false;
+                        defaultValue = TruthValue.FALSE;
+                } else {
+                        var seed = modelSeed.getSeed(partialRelation);
+                        defaultValue = seed.reducedValue() == TruthValue.FALSE ? TruthValue.FALSE : TruthValue.UNKNOWN;
+                        var cursor = seed.getCursor(defaultValue, getNodeCount());
+                        // The symbol should be mutable if there is at least one non-default entry in the seed.
+                        mutable = cursor.move();
+                }
+                var translator = new PredicateTranslator(partialRelation, query, mutable, defaultValue);
+                storeBuilder.with(translator);
+        }
+
+        private RelationalQuery toQuery(String name, PredicateDefinition predicateDefinition) {
+                var problemParameters = predicateDefinition.getParameters();
+                int arity = problemParameters.size();
+                var parameters = new NodeVariable[arity];
+                var parameterMap = new HashMap<tools.refinery.language.model.problem.Variable, Variable>(arity);
+                var commonLiterals = new ArrayList<Literal>();
+                for (int i = 0; i < arity; i++) {
+                        var problemParameter = problemParameters.get(i);
+                        var parameter = Variable.of(problemParameter.getName());
+                        parameters[i] = parameter;
+                        parameterMap.put(problemParameter, parameter);
+                        var parameterType = problemParameter.getParameterType();
+                        if (parameterType != null) {
+                                var partialType = getPartialRelation(parameterType);
+                                commonLiterals.add(partialType.call(parameter));
+                        }
+                }
+                var builder = Query.builder(name).parameters(parameters);
+                for (var body : predicateDefinition.getBodies()) {
+                        try {
+                                var localScope = extendScope(parameterMap, body.getImplicitVariables());
+                                var problemLiterals = body.getLiterals();
+                                var literals = new ArrayList<>(commonLiterals);
+                                for (var problemLiteral : problemLiterals) {
+                                        toLiteralsTraced(problemLiteral, localScope, literals);
+                                }
+                                builder.clause(literals);
+                        } catch (RuntimeException e) {
+                                throw TracedException.addTrace(body, e);
+                        }
+                }
+                return builder.build();
+        }
+
+        private Map<tools.refinery.language.model.problem.Variable, Variable> extendScope(
+                        Map<tools.refinery.language.model.problem.Variable, Variable> existing,
+                        Collection<? extends tools.refinery.language.model.problem.Variable> newVariables) {
+                if (newVariables.isEmpty()) {
+                        return existing;
+                }
+                int localScopeSize = existing.size() + newVariables.size();
+                var localScope = new HashMap<tools.refinery.language.model.problem.Variable, Variable>(localScopeSize);
+                localScope.putAll(existing);
+                for (var newVariable : newVariables) {
+                        localScope.put(newVariable, Variable.of(newVariable.getName()));
+                }
+                return localScope;
+        }
+
+        private void toLiteralsTraced(Expr expr, Map<tools.refinery.language.model.problem.Variable, Variable> localScope,
+                                                                  List<Literal> literals) {
+                try {
+                        toLiterals(expr, localScope, literals);
+                } catch (RuntimeException e) {
+                        throw TracedException.addTrace(expr, e);
+                }
+        }
+
+        private void toLiterals(Expr expr, Map<tools.refinery.language.model.problem.Variable, Variable> localScope,
+                                                        List<Literal> literals) {
+                if (expr instanceof 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) {
+                        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) {
+                        var body = negationExpr.getBody();
+                        if (!(body instanceof Atom atom)) {
+                                throw new TracedException(body, "Cannot negate literal");
+                        }
+                        var target = getPartialRelation(atom.getRelation());
+                        Constraint constraint;
+                        if (atom.isTransitiveClosure()) {
+                                constraint = Query.of(target.name() + "#transitive", (builder, p1, p2) -> builder.clause(
+                                                target.callTransitive(p1, p2)
+                                )).getDnf();
+                        } else {
+                                constraint = target;
+                        }
+                        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) {
+                        var argumentList = toArgumentList(List.of(comparisonExpr.getLeft(), comparisonExpr.getRight()),
+                                        localScope, literals);
+                        boolean positive = switch (comparisonExpr.getOp()) {
+                                case EQ -> true;
+                                case NOT_EQ -> false;
+                                default -> throw new TracedException(
+                                                comparisonExpr, "Unsupported operator");
+                        };
+                        literals.add(new EquivalenceLiteral(positive, argumentList.get(0), argumentList.get(1)));
+                } else {
+                        throw new TracedException(expr, "Unsupported literal");
+                }
+        }
+
+        private List<Variable> toArgumentList(
+                        List<Expr> expressions, Map<tools.refinery.language.model.problem.Variable, Variable> localScope,
+                        List<Literal> literals) {
+                var argumentList = new ArrayList<Variable>(expressions.size());
+                for (var expr : expressions) {
+                        if (!(expr instanceof VariableOrNodeExpr variableOrNodeExpr)) {
+                                throw new TracedException(expr, "Unsupported argument");
+                        }
+                        var variableOrNode = variableOrNodeExpr.getVariableOrNode();
+                        if (variableOrNode instanceof Node node) {
+                                int nodeId = getNodeId(node);
+                                var tempVariable = Variable.of(semanticsUtils.getName(node).orElse("_" + nodeId));
+                                literals.add(new ConstantLiteral(tempVariable, nodeId));
+                                argumentList.add(tempVariable);
+                        } else if (variableOrNode instanceof tools.refinery.language.model.problem.Variable problemVariable) {
+                                if (variableOrNodeExpr.getSingletonVariable() == problemVariable) {
+                                        argumentList.add(Variable.of(problemVariable.getName()));
+                                } else {
+                                        var variable = localScope.get(problemVariable);
+                                        if (variable == null) {
+                                                throw new TracedException(variableOrNode, "Unknown variable: " + problemVariable.getName());
+                                        }
+                                        argumentList.add(variable);
+                                }
+                        } else {
+                                throw new TracedException(variableOrNode, "Unknown argument");
+                        }
+                }
+                return argumentList;
+        }
+
+        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);
+                                        }
+                                }
+                        }
+                }
+        }
+
+        private void collectTypeScopeIncrement(TypeScope typeScope) {
+                if (!(typeScope.getTargetType() instanceof ClassDeclaration classDeclaration)) {
+                        throw new TracedException(typeScope, "Target of incremental type scope must be a class declaration");
+                }
+                var newNode = classDeclaration.getNewNode();
+                if (newNode == null) {
+                        throw new TracedException(typeScope, "Target of incremental type scope must be concrete class");
+                }
+                int newNodeId = nodeTrace.get(newNode);
+                var type = relationTrace.get(classDeclaration);
+                var typeInfo = metamodel.typeHierarchy().getAnalysisResult(type);
+                if (!typeInfo.getDirectSubtypes().isEmpty()) {
+                        throw new TracedException(typeScope, "Target of incremental type scope cannot have any subclasses");
+                }
+                var interval = getCardinalityInterval(typeScope.getMultiplicity());
+                countSeed.compute(Tuple.of(newNodeId), (key, oldValue) ->
+                                oldValue == null ? interval : oldValue.meet(interval));
+        }
+
+        private void collectTypeScope(TypeScope typeScope) {
+                var type = relationTrace.get(typeScope.getTargetType());
+                if (type == null) {
+                        throw new TracedException(typeScope, "Unknown target type");
+                }
+                var interval = getCardinalityInterval(typeScope.getMultiplicity());
+                if (scopePropagator == null) {
+                        scopePropagator = new ScopePropagator();
+                }
+                scopePropagator.scope(type, interval);
+        }
+
+        private record RelationInfo(PartialRelation partialRelation, MutableSeed<TruthValue> assertions,
+                                                                MutableSeed<TruthValue> defaultAssertions) {
+                public RelationInfo(String name, int arity, TruthValue value, TruthValue defaultValue) {
+                        this(new PartialRelation(name, arity), value, defaultValue);
+                }
+
+                public RelationInfo(PartialRelation partialRelation, TruthValue value, TruthValue defaultValue) {
+                        this(partialRelation, MutableSeed.of(partialRelation.arity(), value),
+                                        MutableSeed.of(partialRelation.arity(), defaultValue));
+                }
+
+                public Seed<TruthValue> toSeed(int nodeCount) {
+                        defaultAssertions.overwriteValues(assertions);
+                        if (partialRelation.equals(ReasoningAdapter.EQUALS_SYMBOL)) {
+                                for (int i = 0; i < nodeCount; i++) {
+                                        defaultAssertions.setIfMissing(Tuple.of(i, i), TruthValue.TRUE);
+                                }
+                                defaultAssertions.setAllMissing(TruthValue.FALSE);
+                        }
+                        return defaultAssertions;
+                }
+        }
 }
diff --git a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/model/SemanticsUtils.java b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/model/SemanticsUtils.java
new file mode 100644
index 00000000..47c89e9b
--- /dev/null
+++ b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/model/SemanticsUtils.java
@@ -0,0 +1,31 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.language.semantics.model;
+
+import com.google.inject.Inject;
+import com.google.inject.Singleton;
+import org.eclipse.emf.ecore.EObject;
+import org.eclipse.xtext.naming.IQualifiedNameConverter;
+import org.eclipse.xtext.naming.IQualifiedNameProvider;
+
+import java.util.Optional;
+
+@Singleton
+public class SemanticsUtils {
+        @Inject
+        private IQualifiedNameProvider qualifiedNameProvider;
+
+        @Inject
+        private IQualifiedNameConverter qualifiedNameConverter;
+
+        public Optional<String> getName(EObject eObject) {
+                var qualifiedName = qualifiedNameProvider.getFullyQualifiedName(eObject);
+                if (qualifiedName == null) {
+                        return Optional.empty();
+                }
+                return Optional.of(qualifiedNameConverter.toString(qualifiedName));
+        }
+}
diff --git a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/model/TracedException.java b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/model/TracedException.java
new file mode 100644
index 00000000..38fd8a67
--- /dev/null
+++ b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/model/TracedException.java
@@ -0,0 +1,51 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.language.semantics.model;
+
+import org.eclipse.emf.ecore.EObject;
+
+public class TracedException extends RuntimeException {
+        private final transient EObject sourceElement;
+
+        public TracedException(EObject sourceElement) {
+                this.sourceElement = sourceElement;
+        }
+
+        public TracedException(EObject sourceElement, String message) {
+                super(message);
+                this.sourceElement = sourceElement;
+        }
+
+        public TracedException(EObject sourceElement, String message, Throwable cause) {
+                super(message, cause);
+                this.sourceElement = sourceElement;
+        }
+
+        public TracedException(EObject sourceElement, Throwable cause) {
+                super(cause);
+                this.sourceElement = sourceElement;
+        }
+
+        public EObject getSourceElement() {
+                return sourceElement;
+        }
+
+        @Override
+        public String getMessage() {
+                var message = super.getMessage();
+                if (message == null) {
+                        return "Internal error";
+                }
+                return message;
+        }
+
+        public static TracedException addTrace(EObject sourceElement, Throwable cause) {
+                if (cause instanceof TracedException tracedException && tracedException.sourceElement != null) {
+                        return tracedException;
+                }
+                return new TracedException(sourceElement, cause);
+        }
+}
diff --git a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/model/internal/DecisionTree.java b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/model/internal/DecisionTree.java
index c1afecf9..32112e61 100644
--- a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/model/internal/DecisionTree.java
+++ b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/model/internal/DecisionTree.java
@@ -7,10 +7,10 @@ package tools.refinery.language.semantics.model.internal;
 
 import org.eclipse.collections.api.factory.primitive.IntObjectMaps;
 import tools.refinery.store.map.Cursor;
-import tools.refinery.store.tuple.Tuple;
 import tools.refinery.store.representation.TruthValue;
+import tools.refinery.store.tuple.Tuple;
 
-public class DecisionTree {
+class DecisionTree implements MutableSeed<TruthValue> {
         private final int levels;
 
         private final DecisionTreeNode root;
@@ -29,30 +29,53 @@ public class DecisionTree {
                 this(levels, null);
         }
 
+        @Override
+        public int arity() {
+                return levels;
+        }
+
+        @Override
+        public Class<TruthValue> valueType() {
+                return TruthValue.class;
+        }
+
+        @Override
+        public TruthValue reducedValue() {
+                return root.getOtherwiseReducedValue().getTruthValue();
+        }
+
+        @Override
         public TruthValue get(Tuple tuple) {
                 return root.getValue(levels - 1, tuple).getTruthValue();
         }
 
+        @Override
         public void mergeValue(Tuple tuple, TruthValue truthValue) {
                 if (truthValue != null) {
                         root.mergeValue(levels - 1, tuple, truthValue);
                 }
         }
 
+        @Override
         public void setIfMissing(Tuple tuple, TruthValue truthValue) {
                 if (truthValue != null) {
                         root.setIfMissing(levels - 1, tuple, truthValue);
                 }
         }
 
+        @Override
         public void setAllMissing(TruthValue truthValue) {
                 if (truthValue != null) {
                         root.setAllMissing(truthValue);
                 }
         }
 
-        public void overwriteValues(DecisionTree values) {
-                root.overwriteValues(values.root);
+        @Override
+        public void overwriteValues(MutableSeed<TruthValue> values) {
+                if (!(values instanceof DecisionTree decisionTree)) {
+                        throw new IllegalArgumentException("Incompatible overwrite: " + values);
+                }
+                root.overwriteValues(decisionTree.root);
         }
 
         public TruthValue getReducedValue() {
@@ -60,6 +83,7 @@ public class DecisionTree {
                 return reducedValue == null ? null : reducedValue.getTruthValue();
         }
 
+        @Override
         public Cursor<Tuple, TruthValue> getCursor(TruthValue defaultValue, int nodeCount) {
                 return new DecisionTreeCursor(levels, defaultValue, nodeCount, root);
         }
diff --git a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/model/internal/DecisionTreeCursor.java b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/model/internal/DecisionTreeCursor.java
index 9a1e15a3..a9fc644a 100644
--- a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/model/internal/DecisionTreeCursor.java
+++ b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/model/internal/DecisionTreeCursor.java
@@ -67,6 +67,15 @@ class DecisionTreeCursor implements Cursor<Tuple, TruthValue> {
 
         @Override
         public boolean move() {
+                while (moveOne()) {
+                        if (!value.equals(defaultValue)) {
+                                return true;
+                        }
+                }
+                return false;
+        }
+
+        private boolean moveOne() {
                 boolean found = false;
                 if (path.isEmpty() && !terminated) {
                         found = root.moveNext(levels - 1, this);
diff --git a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/model/internal/MutableSeed.java b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/model/internal/MutableSeed.java
new file mode 100644
index 00000000..99019e2a
--- /dev/null
+++ b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/model/internal/MutableSeed.java
@@ -0,0 +1,28 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.language.semantics.model.internal;
+
+import tools.refinery.store.reasoning.seed.Seed;
+import tools.refinery.store.representation.TruthValue;
+import tools.refinery.store.tuple.Tuple;
+
+public interface MutableSeed<T> extends Seed<T> {
+        void mergeValue(Tuple tuple, T value);
+
+        void setIfMissing(Tuple tuple, T value);
+
+        void setAllMissing(T value);
+
+        void overwriteValues(MutableSeed<T> other);
+
+        static MutableSeed<TruthValue> of(int levels, TruthValue initialValue) {
+                if (levels == 0) {
+                        return new NullaryMutableSeed(initialValue);
+                } else {
+                        return new DecisionTree(levels, initialValue);
+                }
+        }
+}
diff --git a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/model/internal/NullaryMutableSeed.java b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/model/internal/NullaryMutableSeed.java
new file mode 100644
index 00000000..80644b1f
--- /dev/null
+++ b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/model/internal/NullaryMutableSeed.java
@@ -0,0 +1,83 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.language.semantics.model.internal;
+
+import tools.refinery.store.map.Cursor;
+import tools.refinery.store.map.Cursors;
+import tools.refinery.store.representation.TruthValue;
+import tools.refinery.store.tuple.Tuple;
+
+class NullaryMutableSeed implements MutableSeed<TruthValue> {
+        private DecisionTreeValue value;
+
+        public NullaryMutableSeed(TruthValue reducedValue) {
+
+                value = DecisionTreeValue.fromTruthValue(reducedValue);
+        }
+
+        @Override
+        public int arity() {
+                return 0;
+        }
+
+        @Override
+        public Class<TruthValue> valueType() {
+                return TruthValue.class;
+        }
+
+        @Override
+        public TruthValue reducedValue() {
+                return value.getTruthValue();
+        }
+
+        @Override
+        public TruthValue get(Tuple key) {
+                validateKey(key);
+                return reducedValue();
+        }
+
+        private static void validateKey(Tuple key) {
+                if (key.getSize() > 0) {
+                        throw new IllegalArgumentException("Invalid key: " + key);
+                }
+        }
+
+        @Override
+        public Cursor<Tuple, TruthValue> getCursor(TruthValue defaultValue, int nodeCount) {
+                if (value == DecisionTreeValue.UNSET || value.getTruthValue() == defaultValue) {
+                        return Cursors.empty();
+                }
+                return Cursors.singleton(Tuple.of(), value.getTruthValue());
+        }
+
+        @Override
+        public void mergeValue(Tuple tuple, TruthValue value) {
+                this.value = DecisionTreeValue.fromTruthValue(this.value.merge(value));
+        }
+
+        @Override
+        public void setIfMissing(Tuple tuple, TruthValue value) {
+                validateKey(tuple);
+                setAllMissing(value);
+        }
+
+        @Override
+        public void setAllMissing(TruthValue value) {
+                if (this.value == DecisionTreeValue.UNSET) {
+                        this.value = DecisionTreeValue.fromTruthValue(value);
+                }
+        }
+
+        @Override
+        public void overwriteValues(MutableSeed<TruthValue> other) {
+                if (!(other instanceof NullaryMutableSeed nullaryMutableSeed)) {
+                        throw new IllegalArgumentException("Incompatible overwrite: " + other);
+                }
+                if (nullaryMutableSeed.value != DecisionTreeValue.UNSET) {
+                        value = nullaryMutableSeed.value;
+                }
+        }
+}