5 files changed, 88 insertions, 28 deletions

diff --git a/subprojects/logic/src/main/java/tools/refinery/logic/term/cardinalityinterval/NonEmptyCardinalityInterval.java b/subprojects/logic/src/main/java/tools/refinery/logic/term/cardinalityinterval/NonEmptyCardinalityInterval.java
index efe1464e..d564ff66 100644
--- a/subprojects/logic/src/main/java/tools/refinery/logic/term/cardinalityinterval/NonEmptyCardinalityInterval.java
+++ b/subprojects/logic/src/main/java/tools/refinery/logic/term/cardinalityinterval/NonEmptyCardinalityInterval.java
@@ -32,8 +32,7 @@ public record NonEmptyCardinalityInterval(int lowerBound, UpperCardinality upper
 
         @Override
         public boolean isConcrete() {
-                return upperBound instanceof FiniteUpperCardinality finiteUpperCardinality &&
-                                finiteUpperCardinality.finiteUpperBound() == lowerBound;
+                return upperBound instanceof FiniteUpperCardinality(var finiteUpperBound) && finiteUpperBound == lowerBound;
         }
 
         @Override
@@ -49,10 +48,10 @@ public record NonEmptyCardinalityInterval(int lowerBound, UpperCardinality upper
 
         @Override
         public boolean isRefinementOf(CardinalityInterval other) {
-                if (!(other instanceof NonEmptyCardinalityInterval nonEmptyOther)) {
+                if (!(other instanceof NonEmptyCardinalityInterval(var otherLowerBound, var otherUpperBound))) {
                         return false;
                 }
-                return lowerBound >= nonEmptyOther.lowerBound() && upperBound.compareTo(nonEmptyOther.upperBound()) <= 0;
+                return lowerBound >= otherLowerBound && upperBound.compareTo(otherUpperBound) <= 0;
         }
 
         @Override
@@ -98,9 +97,9 @@ public record NonEmptyCardinalityInterval(int lowerBound, UpperCardinality upper
         private CardinalityInterval lift(CardinalityInterval other, IntBinaryOperator lowerOperator,
                                                                          BinaryOperator<UpperCardinality> upperOperator,
                                                                          CardinalityInterval whenEmpty) {
-                if (other instanceof NonEmptyCardinalityInterval nonEmptyOther) {
-                        return CardinalityIntervals.between(lowerOperator.applyAsInt(lowerBound, nonEmptyOther.lowerBound),
-                                        upperOperator.apply(upperBound, nonEmptyOther.upperBound));
+                if (other instanceof NonEmptyCardinalityInterval(var otherLowerBound, var otherUpperBound)) {
+                        return CardinalityIntervals.between(lowerOperator.applyAsInt(lowerBound, otherLowerBound),
+                                        upperOperator.apply(upperBound, otherUpperBound));
                 }
                 if (other instanceof EmptyCardinalityInterval) {
                         return whenEmpty;
@@ -115,8 +114,8 @@ public record NonEmptyCardinalityInterval(int lowerBound, UpperCardinality upper
 
         @Override
         public String toString() {
-                if (upperBound instanceof FiniteUpperCardinality finiteUpperCardinality &&
-                                finiteUpperCardinality.finiteUpperBound() == lowerBound) {
+                if (upperBound instanceof FiniteUpperCardinality(var finiteUpperBound) &&
+                                finiteUpperBound == lowerBound) {
                         return "[%d]".formatted(lowerBound);
                 }
                 return "[%d..%s]".formatted(lowerBound, upperBound);
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/actions/PartialActionLiterals.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/actions/PartialActionLiterals.java
index e8e6880a..18f238d7 100644
--- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/actions/PartialActionLiterals.java
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/actions/PartialActionLiterals.java
@@ -36,8 +36,4 @@ public final class PartialActionLiterals {
         public static FocusActionLiteral focus(NodeVariable parent, NodeVariable child) {
                 return new FocusActionLiteral(parent, child);
         }
-
-        public static CleanupActionLiteral cleanup(NodeVariable node) {
-                return new CleanupActionLiteral(node);
-        }
 }
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/crossreference/CrossReferenceUtils.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/crossreference/CrossReferenceUtils.java
index be9fcb9d..41d185d7 100644
--- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/crossreference/CrossReferenceUtils.java
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/crossreference/CrossReferenceUtils.java
@@ -30,10 +30,10 @@ import static tools.refinery.logic.literal.Literals.check;
 import static tools.refinery.logic.literal.Literals.not;
 import static tools.refinery.logic.term.int_.IntTerms.constant;
 import static tools.refinery.logic.term.int_.IntTerms.less;
+import static tools.refinery.store.reasoning.ReasoningAdapter.EQUALS_SYMBOL;
 import static tools.refinery.store.reasoning.actions.PartialActionLiterals.add;
 import static tools.refinery.store.reasoning.actions.PartialActionLiterals.remove;
 import static tools.refinery.store.reasoning.literal.PartialLiterals.*;
-import static tools.refinery.store.reasoning.translator.multiobject.MultiObjectTranslator.MULTI_VIEW;
 
 public class CrossReferenceUtils {
         private CrossReferenceUtils() {
@@ -93,7 +93,6 @@ public class CrossReferenceUtils {
                 var lowerBoundCardinality = UpperCardinalities.atMost(lowerBound);
                 propagationBuilder.rule(Rule.of(name + "#lowerSource", (builder, p1, p2) -> builder
                                 .clause(UpperCardinality.class, upperBound -> List.of(
-                                                not(MULTI_VIEW.call(p1)),
                                                 must(sourceType.call(p1)),
                                                 new CountUpperBoundLiteral(upperBound, linkType, List.of(p1, Variable.of())),
                                                 check(UpperCardinalityTerms.lessEq(upperBound,
@@ -127,7 +126,6 @@ public class CrossReferenceUtils {
                 var lowerBoundCardinality = UpperCardinalities.atMost(lowerBound);
                 propagationBuilder.rule(Rule.of(name + "#lowerTarget", (builder, p1, p2) -> builder
                                 .clause(UpperCardinality.class, upperBound -> List.of(
-                                                not(MULTI_VIEW.call(p2)),
                                                 must(targetType.call(p2)),
                                                 new CountUpperBoundLiteral(upperBound, linkType, List.of(Variable.of(), p2)),
                                                 check(UpperCardinalityTerms.lessEq(upperBound,
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiobject/CleanupPropagator.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiobject/CleanupPropagator.java
new file mode 100644
index 00000000..f14b4783
--- /dev/null
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiobject/CleanupPropagator.java
@@ -0,0 +1,78 @@
+/*
+ * SPDX-FileCopyrightText: 2024 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.reasoning.translator.multiobject;
+
+import tools.refinery.logic.dnf.Query;
+import tools.refinery.logic.dnf.RelationalQuery;
+import tools.refinery.logic.term.uppercardinality.UpperCardinalities;
+import tools.refinery.logic.term.uppercardinality.UpperCardinality;
+import tools.refinery.logic.term.uppercardinality.UpperCardinalityTerms;
+import tools.refinery.store.dse.propagation.BoundPropagator;
+import tools.refinery.store.dse.propagation.PropagationResult;
+import tools.refinery.store.dse.propagation.Propagator;
+import tools.refinery.store.model.Model;
+import tools.refinery.store.model.ModelStoreBuilder;
+import tools.refinery.store.query.ModelQueryAdapter;
+import tools.refinery.store.query.ModelQueryBuilder;
+import tools.refinery.store.query.resultset.ResultSet;
+import tools.refinery.store.reasoning.ReasoningAdapter;
+
+import java.util.List;
+
+import static tools.refinery.logic.literal.Literals.check;
+import static tools.refinery.store.reasoning.translator.multiobject.MultiObjectTranslator.UPPER_CARDINALITY_VIEW;
+
+/**
+ * Clean up non-existing objects in a separate propagator to avoid interference with propagation rules that assume
+ * that each object in their activation set is still part of the model when they are called.
+ */
+public class CleanupPropagator implements Propagator {
+        private static final RelationalQuery CLEANUP_QUERY = Query.of("exists#cleanup", (builder, node) -> builder
+                        .clause(UpperCardinality.class, upper -> List.of(
+                                        UPPER_CARDINALITY_VIEW.call(node, upper),
+                                        check(UpperCardinalityTerms.less(upper,
+                                                        UpperCardinalityTerms.constant(UpperCardinalities.ONE)))
+                        ))
+        );
+
+        @Override
+        public void configure(ModelStoreBuilder storeBuilder) {
+                storeBuilder.getAdapter(ModelQueryBuilder.class).query(CLEANUP_QUERY);
+        }
+
+        @Override
+        public BoundPropagator bindToModel(Model model) {
+                return new BoundCleanupPropagator(model);
+        }
+
+        private static class BoundCleanupPropagator implements BoundPropagator {
+                private final Model model;
+                private final ModelQueryAdapter queryEngine;
+                private final ResultSet<Boolean> resultSet;
+                private ReasoningAdapter reasoningAdapter;
+
+                public BoundCleanupPropagator(Model model) {
+                        this.model = model;
+                        queryEngine = model.getAdapter(ModelQueryAdapter.class);
+                        resultSet = queryEngine.getResultSet(CLEANUP_QUERY);
+                }
+
+                @Override
+                public PropagationResult propagateOne() {
+                        if (reasoningAdapter == null) {
+                                reasoningAdapter = model.getAdapter(ReasoningAdapter.class);
+                        }
+                        queryEngine.flushChanges();
+                        boolean propagated = false;
+                        var cursor = resultSet.getAll();
+                        while (cursor.move()) {
+                                propagated = true;
+                                reasoningAdapter.cleanup(cursor.getKey().get(0));
+                        }
+                        return propagated ? PropagationResult.PROPAGATED : PropagationResult.UNCHANGED;
+                }
+        }
+}
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiobject/MultiObjectTranslator.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiobject/MultiObjectTranslator.java
index be15b6d7..05d96689 100644
--- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiobject/MultiObjectTranslator.java
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiobject/MultiObjectTranslator.java
@@ -15,7 +15,6 @@ import tools.refinery.logic.term.uppercardinality.UpperCardinalities;
 import tools.refinery.logic.term.uppercardinality.UpperCardinality;
 import tools.refinery.logic.term.uppercardinality.UpperCardinalityTerms;
 import tools.refinery.store.dse.propagation.PropagationBuilder;
-import tools.refinery.store.dse.transition.Rule;
 import tools.refinery.store.dse.transition.objectives.Criteria;
 import tools.refinery.store.dse.transition.objectives.Objectives;
 import tools.refinery.store.model.ModelStoreBuilder;
@@ -23,7 +22,6 @@ import tools.refinery.store.model.ModelStoreConfiguration;
 import tools.refinery.store.query.view.AnySymbolView;
 import tools.refinery.store.reasoning.ReasoningAdapter;
 import tools.refinery.store.reasoning.ReasoningBuilder;
-import tools.refinery.store.reasoning.actions.PartialActionLiterals;
 import tools.refinery.store.reasoning.representation.PartialFunction;
 import tools.refinery.store.reasoning.translator.PartialRelationTranslator;
 import tools.refinery.store.reasoning.translator.RoundingMode;
@@ -93,15 +91,6 @@ public class MultiObjectTranslator implements ModelStoreConfiguration {
                 reasoningBuilder.storageRefiner(COUNT_STORAGE, MultiObjectStorageRefiner::new);
 
                 storeBuilder.tryGetAdapter(PropagationBuilder.class)
-                                .ifPresent(propagationBuilder -> propagationBuilder.rule(
-                                                Rule.of("exists#cleanup", (builder, node) -> builder
-                                                                .clause(UpperCardinality.class, upper -> List.of(
-                                                                                UPPER_CARDINALITY_VIEW.call(node, upper),
-                                                                                check(UpperCardinalityTerms.less(upper,
-                                                                                                UpperCardinalityTerms.constant(UpperCardinalities.ONE)))
-                                                                ))
-                                                                .action(
-                                                                                PartialActionLiterals.cleanup(node)
-                                                                ))));
+                                .ifPresent(propagationBuilder -> propagationBuilder.propagator(new CleanupPropagator()));
         }
 }