feat: basic semantics mapping and visualization

5 files changed, 366 insertions, 42 deletions

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 fe67ed2c..93c7c8e5 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,66 +9,298 @@ 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.utils.BuiltinSymbols;
 import tools.refinery.language.utils.ProblemDesugarer;
-import tools.refinery.store.representation.Symbol;
+import tools.refinery.language.utils.ProblemUtil;
+import tools.refinery.store.model.ModelStoreBuilder;
+import tools.refinery.store.reasoning.ReasoningAdapter;
+import tools.refinery.store.reasoning.representation.PartialRelation;
+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.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.ArrayList;
+import java.util.LinkedHashMap;
 import java.util.Map;
 
 public class ModelInitializer {
         @Inject
         private ProblemDesugarer desugarer;
 
+        @Inject
+        private SemanticsUtils semanticsUtils;
+
+        private Problem problem;
+
+        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 int nodeCount = 0;
+        private Map<Relation, PartialRelation> relationTrace;
+
+        private final MetamodelBuilder metamodelBuilder = Metamodel.builder();
+
+        public int getNodeCount() {
+                return nodeTrace.size();
+        }
+
+        public MutableObjectIntMap<Node> getNodeTrace() {
+                return nodeTrace;
+        }
 
-        /*public void createModel(Problem problem) {
-                var builtinSymbols = desugarer.getBuiltinSymbols(problem).orElseThrow(() -> new IllegalArgumentException(
+        public Map<Relation, PartialRelation> getRelationTrace() {
+                return relationTrace;
+        }
+
+        public ModelSeed createModel(Problem problem, ModelStoreBuilder builder) {
+                this.problem = problem;
+                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, true);
+                relationInfoMap.put(builtinSymbols.exists(), new RelationInfo(ReasoningAdapter.EXISTS_SYMBOL, null,
+                                TruthValue.TRUE));
+                relationInfoMap.put(builtinSymbols.equals(), new RelationInfo(ReasoningAdapter.EQUALS_SYMBOL, (TruthValue) null,
+                                null));
+                relationInfoMap.put(builtinSymbols.contained(), new RelationInfo(ContainmentHierarchyTranslator.CONTAINED_SYMBOL,
+                                null, TruthValue.UNKNOWN));
+                relationInfoMap.put(builtinSymbols.contains(), new RelationInfo(ContainmentHierarchyTranslator.CONTAINS_SYMBOL,
+                                null, TruthValue.UNKNOWN));
+                relationInfoMap.put(builtinSymbols.invalidNumberOfContainers(),
+                                new RelationInfo(ContainmentHierarchyTranslator.INVALID_NUMBER_OF_CONTAINERS, TruthValue.FALSE,
+                                                TruthValue.FALSE));
+                collectNodes();
+                collectPartialSymbols();
+                collectAssertions();
+                var metamodel = metamodelBuilder.build();
+                builder.with(ReasoningAdapter.builder());
+                builder.with(new MultiObjectTranslator());
+                builder.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));
+                }
+                return modelSeedBuilder.build();
+        }
+
+        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) {
+                                collectClassDeclaration(classDeclaration);
+                        } else if (statement instanceof EnumDeclaration enumDeclaration) {
+                                collectPartialRelation(enumDeclaration, 1, null, TruthValue.FALSE);
+                        } else if (statement instanceof PredicateDefinition predicateDefinition) {
+                                // TODO Implement predicate definitions
+                        }
+                }
+        }
+
+        private void collectClassDeclaration(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 IllegalArgumentException("Unknown feature declaration: " + featureDeclaration);
+                        }
+                }
+        }
+
+        private RelationInfo collectPartialRelation(Relation relation, int arity, TruthValue value,
+                                                                                                TruthValue defaultValue) {
+                return relationInfoMap.computeIfAbsent(relation, key -> {
+                        var name = getName(relation);
+                        return new RelationInfo(name, arity, value, defaultValue);
+                });
+        }
+
+        private String getName(Relation relation) {
+                return semanticsUtils.getName(relation).orElseGet(() -> "#" + relationInfoMap.size());
+        }
+
+        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.overwriteValues(assertions);
-                if (isEqualsRelation) {
-                        for (int i = 0; i < nodeCount; i++) {
-                                defaultAssertions.setIfMissing(Tuple.of(i, i), TruthValue.TRUE);
+        }
+
+        private void collectClassDeclarationAssertions(ClassDeclaration classDeclaration) {
+                var superTypes = classDeclaration.getSuperTypes();
+                var partialSuperTypes = new ArrayList<PartialRelation>(superTypes.size() + 1);
+                partialSuperTypes.add(nodeRelation);
+                for (var superType : superTypes) {
+                        partialSuperTypes.add(getRelationInfo(superType).partialRelation());
+                }
+                var info = getRelationInfo(classDeclaration);
+                metamodelBuilder.type(info.partialRelation(), classDeclaration.isAbstract(),
+                                partialSuperTypes);
+                var newNode = classDeclaration.getNewNode();
+                if (newNode != null) {
+                        var newNodeId = getNodeId(newNode);
+                        collectCardinalityAssertions(newNodeId, TruthValue.UNKNOWN);
+                        mergeValue(classDeclaration, Tuple.of(newNodeId), TruthValue.TRUE);
+                }
+                for (var featureDeclaration : classDeclaration.getFeatureDeclarations()) {
+                        if (featureDeclaration instanceof ReferenceDeclaration referenceDeclaration) {
+                                collectReferenceDeclarationAssertions(classDeclaration, referenceDeclaration);
+                        } else {
+                                throw new IllegalArgumentException("Unknown feature declaration: " + featureDeclaration);
                         }
-                        defaultAssertions.setAllMissing(TruthValue.FALSE);
                 }
-                return defaultAssertions;
-        }*/
+        }
+
+        private void collectReferenceDeclarationAssertions(ClassDeclaration classDeclaration,
+                                                                                                           ReferenceDeclaration referenceDeclaration) {
+                var relation = getRelationInfo(referenceDeclaration).partialRelation();
+                var source = getRelationInfo(classDeclaration).partialRelation();
+                var target = getRelationInfo(referenceDeclaration.getReferenceType()).partialRelation();
+                boolean containment = referenceDeclaration.getKind() == ReferenceKind.CONTAINMENT;
+                var opposite = referenceDeclaration.getOpposite();
+                PartialRelation oppositeRelation = null;
+                if (opposite != null) {
+                        oppositeRelation = getRelationInfo(opposite).partialRelation();
+                }
+                var multiplicity = getMultiplicityConstraint(referenceDeclaration);
+                metamodelBuilder.reference(relation, source, containment, multiplicity, target, oppositeRelation);
+        }
+
+        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 if (problemMultiplicity instanceof ExactMultiplicity exactMultiplicity) {
+                        interval = CardinalityIntervals.exactly(exactMultiplicity.getExactValue());
+                } else if (problemMultiplicity instanceof RangeMultiplicity rangeMultiplicity) {
+                        var upperBound = rangeMultiplicity.getUpperBound();
+                        interval = CardinalityIntervals.between(rangeMultiplicity.getLowerBound(),
+                                        upperBound < 0 ? UpperCardinalities.UNBOUNDED : UpperCardinalities.atMost(upperBound));
+                } else {
+                        throw new IllegalArgumentException("Unknown multiplicity: " + problemMultiplicity);
+                }
+                var constraint = getRelationInfo(referenceDeclaration.getInvalidMultiplicity()).partialRelation();
+                return ConstrainedMultiplicity.of(interval, constraint);
+        }
+
+        private void collectEnumAssertions(EnumDeclaration enumDeclaration) {
+                var info = getRelationInfo(enumDeclaration);
+                metamodelBuilder.type(info.partialRelation(), nodeRelation);
+                var overlay = new DecisionTree(1, null);
+                for (var literal : enumDeclaration.getLiterals()) {
+                        collectIndividualAssertions(literal);
+                        var nodeId = getNodeId(literal);
+                        overlay.mergeValue(Tuple.of(nodeId), TruthValue.TRUE);
+                }
+                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 relation = assertion.getRelation();
+                var tuple = getTuple(assertion);
+                var value = getTruthValue(assertion.getValue());
+                if (assertion.isDefault()) {
+                        mergeDefaultValue(relation, tuple, value);
+                } else {
+                        mergeValue(relation, tuple, value);
+                }
+        }
+
+        private void mergeValue(Relation relation, Tuple key, TruthValue value) {
+                getRelationInfo(relation).assertions().mergeValue(key, value);
+        }
+
+        private void mergeDefaultValue(Relation relation, Tuple key, TruthValue value) {
+                getRelationInfo(relation).defaultAssertions().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 int getNodeId(Node node) {
+                return nodeTrace.getOrThrow(node);
+        }
 
         private Tuple getTuple(Assertion assertion) {
                 var arguments = assertion.getArguments();
@@ -77,7 +309,7 @@ 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 {
@@ -98,4 +330,27 @@ public class ModelInitializer {
                         case ERROR -> TruthValue.ERROR;
                 };
         }
+
+        private record RelationInfo(PartialRelation partialRelation, DecisionTree assertions,
+                                                                DecisionTree 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, new DecisionTree(partialRelation.arity(), value),
+                                        new DecisionTree(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/internal/DecisionTree.java b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/model/internal/DecisionTree.java
index c1afecf9..d693dec3 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,11 @@ 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.reasoning.seed.Seed;
 import tools.refinery.store.tuple.Tuple;
 import tools.refinery.store.representation.TruthValue;
 
-public class DecisionTree {
+public class DecisionTree implements Seed<TruthValue> {
         private final int levels;
 
         private final DecisionTreeNode root;
@@ -29,6 +30,22 @@ 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.getReducedValue().getTruthValue();
+        }
+
+        @Override
         public TruthValue get(Tuple tuple) {
                 return root.getValue(levels - 1, tuple).getTruthValue();
         }
@@ -60,6 +77,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/test/java/tools/refinery/language/semantics/model/tests/DecisionTreeTests.java b/subprojects/language-semantics/src/test/java/tools/refinery/language/semantics/model/tests/DecisionTreeTests.java
index b3fcbabb..3c43d3bd 100644
--- a/subprojects/language-semantics/src/test/java/tools/refinery/language/semantics/model/tests/DecisionTreeTests.java
+++ b/subprojects/language-semantics/src/test/java/tools/refinery/language/semantics/model/tests/DecisionTreeTests.java
@@ -134,6 +134,17 @@ class DecisionTreeTests {
         }
 
         @Test
+        void overwriteIterationTest() {
+                var sut = new DecisionTree(1, TruthValue.TRUE);
+                var overwrite = new DecisionTree(1, null);
+                overwrite.mergeValue(Tuple.of(0), TruthValue.UNKNOWN);
+                sut.overwriteValues(overwrite);
+                var map = iterateAll(sut, TruthValue.UNKNOWN, 2);
+                assertThat(map.keySet(), hasSize(1));
+                assertThat(map, hasEntry(Tuple.of(1), TruthValue.TRUE));
+        }
+
+        @Test
         void overwriteNothingTest() {
                 var sut = new DecisionTree(2, TruthValue.UNKNOWN);
                 var values = new DecisionTree(2, null);