fix: contains assertions

7 files changed, 120 insertions, 24 deletions

diff --git a/subprojects/language-ide/src/main/java/tools/refinery/language/ide/contentassist/ProblemCrossrefProposalProvider.java b/subprojects/language-ide/src/main/java/tools/refinery/language/ide/contentassist/ProblemCrossrefProposalProvider.java
index 27e936a1..166b4400 100644
--- a/subprojects/language-ide/src/main/java/tools/refinery/language/ide/contentassist/ProblemCrossrefProposalProvider.java
+++ b/subprojects/language-ide/src/main/java/tools/refinery/language/ide/contentassist/ProblemCrossrefProposalProvider.java
@@ -169,12 +169,6 @@ public class ProblemCrossrefProposalProvider extends IdeCrossrefProposalProvider
                         return supertypeShouldBeVisible(candidate, context, builtinSymbols, candidateEObjectOrProxy);
                 }
 
-                if (eReference.equals(ProblemPackage.Literals.ASSERTION__RELATION)) {
-                        // Currently, we don't support assertions on the {@code contains} relation.
-                        return !builtinSymbols.contains().equals(candidateEObjectOrProxy) &&
-                                        !builtinSymbols.contained().equals(candidateEObjectOrProxy);
-                }
-
                 return true;
         }
 
diff --git a/subprojects/store-reasoning-scope/src/test/java/tools/refinery/store/reasoning/scope/PredicateScopeTest.java b/subprojects/store-reasoning-scope/src/test/java/tools/refinery/store/reasoning/scope/PredicateScopeTest.java
index d21bd12e..a2c56a6b 100644
--- a/subprojects/store-reasoning-scope/src/test/java/tools/refinery/store/reasoning/scope/PredicateScopeTest.java
+++ b/subprojects/store-reasoning-scope/src/test/java/tools/refinery/store/reasoning/scope/PredicateScopeTest.java
@@ -84,6 +84,8 @@ class PredicateScopeTest {
                                 .seed(MultiObjectTranslator.COUNT_SYMBOL, builder -> builder.reducedValue(CardinalityIntervals.ONE))
                                 .seed(ContainmentHierarchyTranslator.CONTAINED_SYMBOL,
                                                 builder -> builder.reducedValue(TruthValue.UNKNOWN))
+                                .seed(ContainmentHierarchyTranslator.CONTAINS_SYMBOL,
+                                                builder -> builder.reducedValue(TruthValue.UNKNOWN))
                                 .seed(index, builder -> builder.reducedValue(TruthValue.TRUE))
                                 .seed(next, builder -> builder
                                                 .reducedValue(TruthValue.UNKNOWN)
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/containment/ContainmentHierarchyTranslator.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/containment/ContainmentHierarchyTranslator.java
index 61037be3..c85bd8b7 100644
--- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/containment/ContainmentHierarchyTranslator.java
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/containment/ContainmentHierarchyTranslator.java
@@ -52,9 +52,10 @@ public class ContainmentHierarchyTranslator implements ModelStoreConfiguration {
 
         private final Symbol<InferredContainment> containsStorage = Symbol.of("CONTAINS", 2, InferredContainment.class,
                         InferredContainment.UNKNOWN);
+        private final AnySymbolView mustAnyContainmentLinkView = new MustAnyContainmentLinkView(containsStorage);
         private final AnySymbolView forbiddenContainsView = new ForbiddenContainsView(containsStorage);
         private final RelationalQuery containsMayNewTargetHelper;
-        private final RelationalQuery containsMayExistingHelper;
+        private final RelationalQuery containsWithoutLink;
         private final RelationalQuery weakComponents;
         private final RelationalQuery strongComponents;
         private final Map<PartialRelation, ContainmentInfo> containmentInfoMap;
@@ -67,18 +68,15 @@ public class ContainmentHierarchyTranslator implements ModelStoreConfiguration {
                 containsMayNewTargetHelper = Query.of(name + "#mayNewTargetHelper", (builder, child) -> builder
                                 .clause(Integer.class, existingContainers -> List.of(
                                                 may(CONTAINED_SYMBOL.call(child)),
-                                                new CountLowerBoundLiteral(existingContainers, CONTAINS_SYMBOL, List.of(Variable.of(), child)),
+                                                new CountLowerBoundLiteral(existingContainers, CONTAINS_SYMBOL,
+                                                                List.of(Variable.of(), child)),
                                                 check(less(existingContainers, constant(1)))
                                 )));
 
-                containsMayExistingHelper = Query.of(name + "#mayExistingHelper", (builder, parent, child) -> builder
-                                .clause(Integer.class, existingContainers -> List.of(
-                                                must(CONTAINS_SYMBOL.call(parent, child)),
-                                                not(forbiddenContainsView.call(parent, child))
-                                                // Violation of monotonicity:
-                                                // Containment edges violating upper multiplicity will not be marked as {@code ERROR}, but the
-                                                // {@code invalidNumberOfContainers} error pattern will already mark the node as invalid.
-                                )));
+                containsWithoutLink = Query.of(name + "#withoutLink", (builder, parent, child) -> builder.clause(
+                                must(CONTAINS_SYMBOL.call(parent, child)),
+                                not(mustAnyContainmentLinkView.call(parent, child))
+                ));
 
                 var mustExistBothContains = Query.of(name + "#mustExistBoth", (builder, parent, child) -> builder.clause(
                                 must(CONTAINS_SYMBOL.call(parent, child)),
@@ -139,13 +137,21 @@ public class ContainmentHierarchyTranslator implements ModelStoreConfiguration {
                 var mayNewHelper = Query.of(name + "#mayNewHelper", (builder, parent, child) -> builder.clause(
                                 mayNewSourceHelper.call(parent),
                                 mayNewTargetHelper.call(child),
-                                not(must(CONTAINS_SYMBOL.call(parent, child))),
+                                not(mustAnyContainmentLinkView.call(parent, child)),
                                 not(forbiddenLinkView.call(parent, child))
                 ));
 
+                var existingContainsLink = Query.of(name + "#existingContaints", (builder, parent, child) -> builder
+                                .clause(
+                                                must(linkType.call(parent, child))
+                                )
+                                .clause(
+                                                containsWithoutLink.call(parent, child)
+                                ));
+
                 var mayExistingHelper = Query.of(name + "#mayExistingHelper", (builder, parent, child) -> builder.clause(
-                                must(linkType.call(parent, child)),
-                                containsMayExistingHelper.call(parent, child),
+                                existingContainsLink.call(parent, child),
+                                not(forbiddenContainsView.call(parent, child)),
                                 may(sourceType.call(parent)),
                                 may(targetType.call(child)),
                                 not(forbiddenLinkView.call(parent, child))
@@ -224,7 +230,9 @@ public class ContainmentHierarchyTranslator implements ModelStoreConfiguration {
                                 }))
                                 .must(Query.of(mustName, (builder, parent, child) -> builder.clause(
                                                 new MustContainsView(containsStorage).call(parent, child)
-                                ))));
+                                )))
+                                .refiner(ContainsRefiner.of(containsStorage))
+                                .initializer(new RefinementBasedInitializer<>(CONTAINS_SYMBOL)));
         }
 
         private void translateInvalidContainer(ModelStoreBuilder storeBuilder) {
@@ -245,7 +253,7 @@ public class ContainmentHierarchyTranslator implements ModelStoreConfiguration {
                                 )
                                 .clause(container -> List.of(
                                                 MultiObjectTranslator.MULTI_VIEW.call(multi),
-                                                must(CONTAINS_SYMBOL.call(container, multi)),
+                                                mustAnyContainmentLinkView.call(container, multi),
                                                 not(MultiObjectTranslator.MULTI_VIEW.call(container))
                                 ))
                                 .action(
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/containment/ContainmentLinkRefiner.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/containment/ContainmentLinkRefiner.java
index 497ed98f..e44fcffd 100644
--- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/containment/ContainmentLinkRefiner.java
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/containment/ContainmentLinkRefiner.java
@@ -24,8 +24,8 @@ class ContainmentLinkRefiner extends AbstractPartialInterpretationRefiner<TruthV
         private final PartialInterpretationRefiner<TruthValue, Boolean> sourceRefiner;
         private final PartialInterpretationRefiner<TruthValue, Boolean> targetRefiner;
 
-        public ContainmentLinkRefiner(ReasoningAdapter adapter, PartialSymbol<TruthValue, Boolean> partialSymbol,
-                                                                  Factory factory) {
+        private ContainmentLinkRefiner(ReasoningAdapter adapter, PartialSymbol<TruthValue, Boolean> partialSymbol,
+                                                                   Factory factory) {
                 super(adapter, partialSymbol);
                 this.factory = factory;
                 interpretation = adapter.getModel().getInterpretation(factory.symbol);
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/containment/ContainsRefiner.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/containment/ContainsRefiner.java
new file mode 100644
index 00000000..a7196a1c
--- /dev/null
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/containment/ContainsRefiner.java
@@ -0,0 +1,71 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.reasoning.translator.containment;
+
+import tools.refinery.store.model.Interpretation;
+import tools.refinery.store.reasoning.ReasoningAdapter;
+import tools.refinery.store.reasoning.refinement.AbstractPartialInterpretationRefiner;
+import tools.refinery.store.reasoning.refinement.PartialInterpretationRefiner;
+import tools.refinery.store.reasoning.representation.PartialSymbol;
+import tools.refinery.store.representation.Symbol;
+import tools.refinery.store.representation.TruthValue;
+import tools.refinery.store.tuple.Tuple;
+
+import java.util.LinkedHashMap;
+import java.util.Map;
+import java.util.Set;
+
+class ContainsRefiner extends AbstractPartialInterpretationRefiner<TruthValue, Boolean> {
+        private static final Map<TruthValue, InferredContainment> EMPTY_VALUES;
+
+        static {
+                var values = TruthValue.values();
+                EMPTY_VALUES = new LinkedHashMap<>(values.length);
+                for (var value : values) {
+                        EMPTY_VALUES.put(value, new InferredContainment(value, Set.of(), Set.of()));
+                }
+        }
+
+        private final Interpretation<InferredContainment> interpretation;
+        private final PartialInterpretationRefiner<TruthValue, Boolean> containedRefiner;
+
+        private ContainsRefiner(ReasoningAdapter adapter, PartialSymbol<TruthValue, Boolean> partialSymbol,
+                                                        Symbol<InferredContainment> containsStorage) {
+                super(adapter, partialSymbol);
+                interpretation = adapter.getModel().getInterpretation(containsStorage);
+                containedRefiner = adapter.getRefiner(ContainmentHierarchyTranslator.CONTAINED_SYMBOL);
+        }
+
+        @Override
+        public boolean merge(Tuple key, TruthValue value) {
+                var oldValue = interpretation.get(key);
+                var newValue = mergeLink(oldValue, value);
+                if (oldValue != newValue) {
+                        interpretation.put(key, newValue);
+                }
+                if (value.must()) {
+                        return containedRefiner.merge(Tuple.of(key.get(1)), TruthValue.TRUE);
+                }
+                return true;
+        }
+
+        public InferredContainment mergeLink(InferredContainment oldValue, TruthValue toMerge) {
+                var newContains = oldValue.contains().merge(toMerge);
+                if (newContains.equals(oldValue.contains())) {
+                        return oldValue;
+                }
+                var mustLinks = oldValue.mustLinks();
+                var forbiddenLinks = oldValue.forbiddenLinks();
+                if (mustLinks.isEmpty() && forbiddenLinks.isEmpty()) {
+                        return EMPTY_VALUES.get(newContains);
+                }
+                return new InferredContainment(newContains, mustLinks, forbiddenLinks);
+        }
+
+        public static PartialInterpretationRefiner.Factory<TruthValue, Boolean> of(Symbol<InferredContainment> symbol) {
+                return (adapter, partialSymbol) -> new ContainsRefiner(adapter, partialSymbol, symbol);
+        }
+}
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/containment/InferredContainment.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/containment/InferredContainment.java
index 8df23d9a..8a757ed2 100644
--- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/containment/InferredContainment.java
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/containment/InferredContainment.java
@@ -24,7 +24,7 @@ final class InferredContainment {
                 this.contains = adjustContains(contains, mustLinks, forbiddenLinks);
                 this.mustLinks = mustLinks;
                 this.forbiddenLinks = forbiddenLinks;
-                hashCode = Objects.hash(contains, mustLinks, forbiddenLinks);
+                hashCode = Objects.hash(this.contains, mustLinks, forbiddenLinks);
         }
 
         private static TruthValue adjustContains(TruthValue contains, Set<PartialRelation> mustLinks,
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/containment/MustAnyContainmentLinkView.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/containment/MustAnyContainmentLinkView.java
new file mode 100644
index 00000000..1cc537c6
--- /dev/null
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/containment/MustAnyContainmentLinkView.java
@@ -0,0 +1,21 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.reasoning.translator.containment;
+
+import tools.refinery.store.query.view.TuplePreservingView;
+import tools.refinery.store.representation.Symbol;
+import tools.refinery.store.tuple.Tuple;
+
+class MustAnyContainmentLinkView extends TuplePreservingView<InferredContainment> {
+        public MustAnyContainmentLinkView(Symbol<InferredContainment> symbol) {
+                super(symbol, "contains#mustAnyLink");
+        }
+
+        @Override
+        protected boolean doFilter(Tuple key, InferredContainment value) {
+                return !value.mustLinks().isEmpty();
+        }
+}