11 files changed, 84 insertions, 80 deletions

diff --git a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/ModelInitializer.java b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/ModelInitializer.java
index c2bca2a5..ccfb630f 100644
--- a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/ModelInitializer.java
+++ b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/ModelInitializer.java
@@ -1,5 +1,5 @@
 /*
- * SPDX-FileCopyrightText: 2021-2023 The Refinery Authors <https://refinery.tools/>
+ * SPDX-FileCopyrightText: 2021-2024 The Refinery Authors <https://refinery.tools/>
  *
  * SPDX-License-Identifier: EPL-2.0
  */
@@ -8,20 +8,24 @@ package tools.refinery.language.semantics;
 import com.google.inject.Inject;
 import tools.refinery.language.library.BuiltinLibrary;
 import tools.refinery.language.model.problem.*;
+import tools.refinery.language.scoping.imports.ImportAdapterProvider;
 import tools.refinery.language.scoping.imports.ImportCollector;
 import tools.refinery.language.semantics.internal.MutableSeed;
 import tools.refinery.language.utils.BuiltinSymbols;
-import tools.refinery.language.utils.ProblemDesugarer;
 import tools.refinery.language.utils.ProblemUtil;
+import tools.refinery.logic.Constraint;
+import tools.refinery.logic.dnf.InvalidClauseException;
+import tools.refinery.logic.dnf.Query;
+import tools.refinery.logic.dnf.RelationalQuery;
+import tools.refinery.logic.literal.*;
+import tools.refinery.logic.term.NodeVariable;
+import tools.refinery.logic.term.Variable;
+import tools.refinery.logic.term.cardinalityinterval.CardinalityInterval;
+import tools.refinery.logic.term.cardinalityinterval.CardinalityIntervals;
+import tools.refinery.logic.term.truthvalue.TruthValue;
+import tools.refinery.logic.term.uppercardinality.UpperCardinalities;
 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.PartialRelation;
 import tools.refinery.store.reasoning.scope.ScopePropagator;
@@ -29,25 +33,21 @@ import tools.refinery.store.reasoning.seed.ModelSeed;
 import tools.refinery.store.reasoning.seed.Seed;
 import tools.refinery.store.reasoning.translator.TranslationException;
 import tools.refinery.store.reasoning.translator.containment.ContainmentHierarchyTranslator;
-import tools.refinery.store.reasoning.translator.metamodel.*;
+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.metamodel.ReferenceInfo;
 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.*;
 
 public class ModelInitializer {
         @Inject
-        private ProblemDesugarer desugarer;
-
-        @Inject
         private SemanticsUtils semanticsUtils;
 
         @Inject
@@ -56,6 +56,9 @@ public class ModelInitializer {
         @Inject
         private ImportCollector importCollector;
 
+        @Inject
+        private ImportAdapterProvider importAdapterProvider;
+
         private Problem problem;
 
         private final Set<Problem> importedProblems = new HashSet<>();
@@ -93,8 +96,7 @@ public class ModelInitializer {
                 importedProblems.add(problem);
                 problemTrace.setProblem(problem);
                 try {
-                        builtinSymbols = desugarer.getBuiltinSymbols(problem).orElseThrow(() -> new IllegalArgumentException(
-                                        "Problem has no builtin library"));
+                        builtinSymbols = importAdapterProvider.getBuiltinSymbols(problem);
                         var nodeInfo = collectPartialRelation(builtinSymbols.node(), 1, TruthValue.TRUE, TruthValue.TRUE);
                         nodeRelation = nodeInfo.partialRelation();
                         metamodelBuilder.type(nodeRelation);
@@ -202,20 +204,7 @@ public class ModelInitializer {
         private void collectNodes() {
                 for (var importedProblem : importedProblems) {
                         for (var statement : importedProblem.getStatements()) {
-                                if (statement instanceof NodeDeclaration nodeDeclaration) {
-                                        for (var node : nodeDeclaration.getNodes()) {
-                                                collectNode(node);
-                                        }
-                                } else if (statement instanceof ClassDeclaration classDeclaration) {
-                                        var newNode = classDeclaration.getNewNode();
-                                        if (newNode != null) {
-                                                collectNode(newNode);
-                                        }
-                                } else if (statement instanceof EnumDeclaration enumDeclaration) {
-                                        for (var literal : enumDeclaration.getLiterals()) {
-                                                collectNode(literal);
-                                        }
-                                }
+                                collectNodes(statement);
                         }
                 }
                 for (var node : problem.getNodes()) {
@@ -223,6 +212,23 @@ public class ModelInitializer {
                 }
         }
 
+        private void collectNodes(Statement statement) {
+                if (statement instanceof NodeDeclaration nodeDeclaration) {
+                        for (var node : nodeDeclaration.getNodes()) {
+                                collectNode(node);
+                        }
+                } else if (statement instanceof ClassDeclaration classDeclaration) {
+                        var newNode = classDeclaration.getNewNode();
+                        if (newNode != null) {
+                                collectNode(newNode);
+                        }
+                } else if (statement instanceof EnumDeclaration enumDeclaration) {
+                        for (var literal : enumDeclaration.getLiterals()) {
+                                collectNode(literal);
+                        }
+                }
+        }
+
         private void collectNode(Node node) {
                 problemTrace.collectNode(node);
         }
@@ -243,15 +249,14 @@ public class ModelInitializer {
 
         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 {
-                                throw new TracedException(featureDeclaration, "Unknown feature declaration");
+                for (var referenceDeclaration : classDeclaration.getFeatureDeclarations()) {
+                        if (referenceDeclaration.getReferenceType() instanceof DatatypeDeclaration) {
+                                throw new TracedException(referenceDeclaration, "Attributes are not yet supported");
+                        }
+                        collectPartialRelation(referenceDeclaration, 2, null, TruthValue.UNKNOWN);
+                        var invalidMultiplicityConstraint = referenceDeclaration.getInvalidMultiplicity();
+                        if (invalidMultiplicityConstraint != null) {
+                                collectPartialRelation(invalidMultiplicityConstraint, 1, TruthValue.FALSE, TruthValue.FALSE);
                         }
                 }
         }
@@ -319,10 +324,8 @@ public class ModelInitializer {
                 } catch (RuntimeException e) {
                         throw TracedException.addTrace(classDeclaration, e);
                 }
-                for (var featureDeclaration : classDeclaration.getFeatureDeclarations()) {
-                        if (featureDeclaration instanceof ReferenceDeclaration referenceDeclaration) {
-                                collectReferenceDeclarationMetamodel(classDeclaration, referenceDeclaration);
-                        }
+                for (var referenceDeclaration : classDeclaration.getFeatureDeclarations()) {
+                        collectReferenceDeclarationMetamodel(classDeclaration, referenceDeclaration);
                 }
         }
 
@@ -681,8 +684,8 @@ public class ModelInitializer {
                         var argumentList = toArgumentList(List.of(comparisonExpr.getLeft(), comparisonExpr.getRight()),
                                         localScope, literals);
                         boolean positive = switch (comparisonExpr.getOp()) {
-                                case EQ -> true;
-                                case NOT_EQ -> false;
+                                case NODE_EQ -> true;
+                                case NODE_NOT_EQ -> false;
                                 default -> throw new TracedException(
                                                 comparisonExpr, "Unsupported operator");
                         };
@@ -726,14 +729,18 @@ public class ModelInitializer {
         private void collectScopes() {
                 for (var importedProblem : importedProblems) {
                         for (var statement : importedProblem.getStatements()) {
-                                if (statement instanceof ScopeDeclaration scopeDeclaration) {
-                                        for (var typeScope : scopeDeclaration.getTypeScopes()) {
-                                                if (typeScope.isIncrement()) {
-                                                        collectTypeScopeIncrement(typeScope);
-                                                } else {
-                                                        collectTypeScope(typeScope);
-                                                }
-                                        }
+                                collectScopes(statement);
+                        }
+                }
+        }
+
+        private void collectScopes(Statement statement) {
+                if (statement instanceof ScopeDeclaration scopeDeclaration) {
+                        for (var typeScope : scopeDeclaration.getTypeScopes()) {
+                                if (typeScope.isIncrement()) {
+                                        collectTypeScopeIncrement(typeScope);
+                                } else {
+                                        collectTypeScope(typeScope);
                                 }
                         }
                 }
diff --git a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/SemanticsUtils.java b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/SemanticsUtils.java
index 9c40e6df..5e0526bc 100644
--- a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/SemanticsUtils.java
+++ b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/SemanticsUtils.java
@@ -7,7 +7,6 @@ package tools.refinery.language.semantics;
 
 import com.google.inject.Inject;
 import com.google.inject.Singleton;
-import com.google.inject.name.Named;
 import org.eclipse.emf.ecore.EClass;
 import org.eclipse.emf.ecore.EObject;
 import org.eclipse.emf.ecore.util.EcoreUtil;
@@ -20,7 +19,6 @@ import org.eclipse.xtext.scoping.IScope;
 import org.jetbrains.annotations.NotNull;
 import org.jetbrains.annotations.Nullable;
 import tools.refinery.language.model.problem.Problem;
-import tools.refinery.language.naming.ProblemQualifiedNameProvider;
 
 import java.util.Optional;
 
@@ -30,17 +28,13 @@ public class SemanticsUtils {
         private IQualifiedNameProvider qualifiedNameProvider;
 
         @Inject
-        @Named(ProblemQualifiedNameProvider.NAMED_DELEGATE)
-        private IQualifiedNameProvider delegateQualifiedNameProvider;
-
-        @Inject
         private IQualifiedNameConverter qualifiedNameConverter;
 
         @Inject
         private IResourceDescriptionsProvider resourceDescriptionsProvider;
 
         public Optional<String> getNameWithoutRootPrefix(EObject eObject) {
-                var qualifiedName = delegateQualifiedNameProvider.getFullyQualifiedName(eObject);
+                var qualifiedName = qualifiedNameProvider.getFullyQualifiedName(eObject);
                 if (qualifiedName == null) {
                         return Optional.empty();
                 }
diff --git a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/SolutionSerializer.java b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/SolutionSerializer.java
index 377a66f3..f097143f 100644
--- a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/SolutionSerializer.java
+++ b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/SolutionSerializer.java
@@ -21,7 +21,8 @@ import org.eclipse.xtext.resource.XtextResourceSet;
 import org.eclipse.xtext.scoping.IScopeProvider;
 import tools.refinery.language.model.problem.*;
 import tools.refinery.language.naming.NamingUtil;
-import tools.refinery.language.utils.ProblemDesugarer;
+import tools.refinery.language.scoping.imports.ImportAdapterProvider;
+import tools.refinery.language.typesystem.SignatureProvider;
 import tools.refinery.language.utils.ProblemUtil;
 import tools.refinery.store.model.Model;
 import tools.refinery.store.reasoning.ReasoningAdapter;
@@ -30,7 +31,7 @@ import tools.refinery.store.reasoning.literal.Concreteness;
 import tools.refinery.store.reasoning.representation.PartialRelation;
 import tools.refinery.store.reasoning.translator.typehierarchy.InferredType;
 import tools.refinery.store.reasoning.translator.typehierarchy.TypeHierarchyTranslator;
-import tools.refinery.store.representation.TruthValue;
+import tools.refinery.logic.term.truthvalue.TruthValue;
 import tools.refinery.store.tuple.Tuple;
 
 import java.io.ByteArrayInputStream;
@@ -57,10 +58,13 @@ public class SolutionSerializer {
         private IScopeProvider scopeProvider;
 
         @Inject
-        private ProblemDesugarer desugarer;
+        private NodeNameProvider nameProvider;
 
         @Inject
-        private NodeNameProvider nameProvider;
+        private ImportAdapterProvider importAdapterProvider;
+
+        @Inject
+        private SignatureProvider signatureProvider;
 
         private ProblemTrace trace;
         private Model model;
@@ -223,8 +227,7 @@ public class SolutionSerializer {
         }
 
         private void addExistsAssertions() {
-                var builtinSymbols = desugarer.getBuiltinSymbols(problem).orElseThrow(() -> new IllegalStateException("No " +
-                                "builtin library in copied problem"));
+                var builtinSymbols = importAdapterProvider.getBuiltinSymbols(problem);
                 // Make sure to output exists assertions in a deterministic order.
                 var sortedNewNodes = new TreeMap<Integer, Node>();
                 for (var pair : trace.getNodeTrace().keyValuesView()) {
@@ -336,7 +339,7 @@ public class SolutionSerializer {
                 var assertion = ProblemFactory.eINSTANCE.createAssertion();
                 assertion.setDefault(true);
                 assertion.setRelation(relation);
-                int arity = ProblemUtil.getArity(relation);
+                int arity = signatureProvider.getArity(relation);
                 for (int i = 0; i < arity; i++) {
                         var argument = ProblemFactory.eINSTANCE.createWildcardAssertionArgument();
                         assertion.getArguments().add(argument);
diff --git a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/internal/DecisionTree.java b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/internal/DecisionTree.java
index 5d25f148..8aa1af28 100644
--- a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/internal/DecisionTree.java
+++ b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/internal/DecisionTree.java
@@ -7,7 +7,7 @@ package tools.refinery.language.semantics.internal;
 
 import org.eclipse.collections.api.factory.primitive.IntObjectMaps;
 import tools.refinery.store.map.Cursor;
-import tools.refinery.store.representation.TruthValue;
+import tools.refinery.logic.term.truthvalue.TruthValue;
 import tools.refinery.store.tuple.Tuple;
 
 class DecisionTree implements MutableSeed<TruthValue> {
diff --git a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/internal/DecisionTreeCursor.java b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/internal/DecisionTreeCursor.java
index 71b54cbd..8b8fed36 100644
--- a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/internal/DecisionTreeCursor.java
+++ b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/internal/DecisionTreeCursor.java
@@ -6,7 +6,7 @@
 package tools.refinery.language.semantics.internal;
 
 import tools.refinery.store.map.Cursor;
-import tools.refinery.store.representation.TruthValue;
+import tools.refinery.logic.term.truthvalue.TruthValue;
 import tools.refinery.store.tuple.Tuple;
 
 import java.util.ArrayDeque;
diff --git a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/internal/DecisionTreeNode.java b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/internal/DecisionTreeNode.java
index 31d6fc78..eb79e0c8 100644
--- a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/internal/DecisionTreeNode.java
+++ b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/internal/DecisionTreeNode.java
@@ -7,7 +7,7 @@ package tools.refinery.language.semantics.internal;
 
 import org.eclipse.collections.api.LazyIntIterable;
 import tools.refinery.store.tuple.Tuple;
-import tools.refinery.store.representation.TruthValue;
+import tools.refinery.logic.term.truthvalue.TruthValue;
 
 abstract class DecisionTreeNode {
         public DecisionTreeValue getReducedValue() {
diff --git a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/internal/DecisionTreeValue.java b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/internal/DecisionTreeValue.java
index 5053e7ac..a6b55989 100644
--- a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/internal/DecisionTreeValue.java
+++ b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/internal/DecisionTreeValue.java
@@ -5,7 +5,7 @@
  */
 package tools.refinery.language.semantics.internal;
 
-import tools.refinery.store.representation.TruthValue;
+import tools.refinery.logic.term.truthvalue.TruthValue;
 
 public enum DecisionTreeValue {
         UNSET(null),
@@ -25,7 +25,7 @@ public enum DecisionTreeValue {
         }
 
         public TruthValue merge(TruthValue other) {
-                return truthValue == null ? other : truthValue.merge(other);
+                return truthValue == null ? other : truthValue.meet(other);
         }
 
         public DecisionTreeValue overwrite(DecisionTreeValue other) {
diff --git a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/internal/IntermediateNode.java b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/internal/IntermediateNode.java
index 2ad216ce..8942068c 100644
--- a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/internal/IntermediateNode.java
+++ b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/internal/IntermediateNode.java
@@ -10,7 +10,7 @@ import org.eclipse.collections.api.factory.primitive.IntObjectMaps;
 import org.eclipse.collections.api.map.primitive.MutableIntObjectMap;
 import org.eclipse.collections.api.tuple.primitive.IntObjectPair;
 import tools.refinery.store.tuple.Tuple;
-import tools.refinery.store.representation.TruthValue;
+import tools.refinery.logic.term.truthvalue.TruthValue;
 
 final class IntermediateNode extends DecisionTreeNode {
         private final MutableIntObjectMap<DecisionTreeNode> children;
diff --git a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/internal/MutableSeed.java b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/internal/MutableSeed.java
index 693b9e1f..85611059 100644
--- a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/internal/MutableSeed.java
+++ b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/internal/MutableSeed.java
@@ -6,7 +6,7 @@
 package tools.refinery.language.semantics.internal;
 
 import tools.refinery.store.reasoning.seed.Seed;
-import tools.refinery.store.representation.TruthValue;
+import tools.refinery.logic.term.truthvalue.TruthValue;
 import tools.refinery.store.tuple.Tuple;
 
 public interface MutableSeed<T> extends Seed<T> {
diff --git a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/internal/NullaryMutableSeed.java b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/internal/NullaryMutableSeed.java
index f100c5a6..09107a37 100644
--- a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/internal/NullaryMutableSeed.java
+++ b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/internal/NullaryMutableSeed.java
@@ -7,7 +7,7 @@ package tools.refinery.language.semantics.internal;
 
 import tools.refinery.store.map.Cursor;
 import tools.refinery.store.map.Cursors;
-import tools.refinery.store.representation.TruthValue;
+import tools.refinery.logic.term.truthvalue.TruthValue;
 import tools.refinery.store.tuple.Tuple;
 
 class NullaryMutableSeed implements MutableSeed<TruthValue> {
diff --git a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/internal/TerminalNode.java b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/internal/TerminalNode.java
index dc501479..75933fe4 100644
--- a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/internal/TerminalNode.java
+++ b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/internal/TerminalNode.java
@@ -10,7 +10,7 @@ import org.eclipse.collections.api.factory.primitive.IntObjectMaps;
 import org.eclipse.collections.api.map.primitive.MutableIntObjectMap;
 import org.eclipse.collections.api.tuple.primitive.IntObjectPair;
 import tools.refinery.store.tuple.Tuple;
-import tools.refinery.store.representation.TruthValue;
+import tools.refinery.logic.term.truthvalue.TruthValue;
 
 class TerminalNode extends DecisionTreeNode {
         private MutableIntObjectMap<TruthValue> children;
@@ -48,7 +48,7 @@ class TerminalNode extends DecisionTreeNode {
         protected void mergeAllValues(int nextLevel, Tuple tuple, TruthValue value) {
                 otherwise = DecisionTreeValue.fromTruthValue(otherwise.merge(value));
                 children = IntObjectMaps.mutable.from(children.keyValuesView(), IntObjectPair::getOne,
-                                pair -> pair.getTwo().merge(value));
+                                pair -> pair.getTwo().meet(value));
                 reduceChildren();
         }