refactor(reasoning): lower multiplicity propagator

5 files changed, 99 insertions, 175 deletions

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 b15a2576..03a25747 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
@@ -30,7 +30,6 @@ import tools.refinery.store.reasoning.refinement.RefinementBasedInitializer;
 import tools.refinery.store.reasoning.representation.PartialRelation;
 import tools.refinery.store.reasoning.translator.PartialRelationTranslator;
 import tools.refinery.store.reasoning.translator.RoundingMode;
-import tools.refinery.store.reasoning.translator.crossreference.CrossReferenceUtils;
 import tools.refinery.store.reasoning.translator.multiobject.MultiObjectTranslator;
 import tools.refinery.store.reasoning.translator.multiplicity.ConstrainedMultiplicity;
 import tools.refinery.store.reasoning.translator.multiplicity.InvalidMultiplicityErrorTranslator;
@@ -113,7 +112,7 @@ public class ContainmentHierarchyTranslator implements ModelStoreConfiguration {
                         translateInvalidMultiplicity(storeBuilder, linkType, info);
                 }
                 translateFocusNotContained(storeBuilder);
-                storeBuilder.tryGetAdapter(PropagationBuilder.class).ifPresent(this::configurePropagationBuilder);
+                storeBuilder.tryGetAdapter(PropagationBuilder.class).ifPresent(this::configureSingleContainerPropagator);
         }
 
         private void translateContainmentLinkType(ModelStoreBuilder storeBuilder, PartialRelation linkType,
@@ -268,27 +267,6 @@ public class ContainmentHierarchyTranslator implements ModelStoreConfiguration {
                                 )));
         }
 
-        private void configurePropagationBuilder(PropagationBuilder propagationBuilder) {
-                configureLowerMultiplicityPropagator(propagationBuilder);
-                configureSingleContainerPropagator(propagationBuilder);
-        }
-
-        private void configureLowerMultiplicityPropagator(PropagationBuilder propagationBuilder) {
-                for (var entry : containmentInfoMap.entrySet()) {
-                        var info = entry.getValue();
-                        if (info.multiplicity() instanceof ConstrainedMultiplicity constrainedMultiplicity) {
-                                int lowerBound = constrainedMultiplicity.multiplicity().lowerBound();
-                                if (lowerBound >= 1) {
-                                        var linkType = entry.getKey();
-                                        var sourceType = info.sourceType();
-                                        CrossReferenceUtils.configureSourceLowerBound(linkType, sourceType, lowerBound,
-                            propagationBuilder);
-                                }
-                        }
-                }
-                CrossReferenceUtils.configureTargetLowerBound(CONTAINS_SYMBOL, CONTAINED_SYMBOL, 1, propagationBuilder);
-        }
-
         private void configureSingleContainerPropagator(PropagationBuilder propagationBuilder) {
                 var possibleContainment = Dnf.of(CONTAINS_SYMBOL.name() + "#possible", builder -> {
                         var p1 = builder.parameter("source");
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 b322513d..56c9d682 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
@@ -12,14 +12,8 @@ import tools.refinery.logic.literal.Literal;
 import tools.refinery.logic.term.NodeVariable;
 import tools.refinery.logic.term.Variable;
 import tools.refinery.logic.term.uppercardinality.FiniteUpperCardinality;
-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.reasoning.literal.CountCandidateLowerBoundLiteral;
 import tools.refinery.store.reasoning.literal.CountLowerBoundLiteral;
-import tools.refinery.store.reasoning.literal.CountUpperBoundLiteral;
 import tools.refinery.store.reasoning.representation.PartialRelation;
 import tools.refinery.store.reasoning.translator.multiplicity.Multiplicity;
 
@@ -27,14 +21,12 @@ import java.util.ArrayList;
 import java.util.List;
 
 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.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.literal.PartialLiterals.candidateMay;
+import static tools.refinery.store.reasoning.literal.PartialLiterals.may;
 
-public class CrossReferenceUtils {
+class CrossReferenceUtils {
         private CrossReferenceUtils() {
                 throw new IllegalStateException("This is a static utility class and should not be instantiated directly");
         }
@@ -85,70 +77,4 @@ public class CrossReferenceUtils {
                 builder.parameter(variable);
                 return new PreparedBuilder(builder, variable, arguments);
         }
-
-        public static void configureSourceLowerBound(PartialRelation linkType, PartialRelation sourceType,
-                                                                                                 int lowerBound, PropagationBuilder propagationBuilder) {
-                var name = linkType.name();
-                var lowerBoundCardinality = UpperCardinalities.atMost(lowerBound);
-                propagationBuilder.rule(Rule.of(name + "#lowerSource", (builder, p1, p2) -> builder
-                                .clause(UpperCardinality.class, upperBound -> List.of(
-                                                must(sourceType.call(p1)),
-                                                new CountUpperBoundLiteral(upperBound, linkType, List.of(p1, Variable.of())),
-                                                check(UpperCardinalityTerms.lessEq(upperBound,
-                                                                UpperCardinalityTerms.constant(lowerBoundCardinality))),
-                                                may(linkType.call(p1, p2)),
-                                                not(must(linkType.call(p1, p2)))
-                                ))
-                                .action(
-                                                add(linkType, p1, p2)
-                                )
-                ));
-                propagationBuilder.rule(Rule.of(name + "#missingTarget", (builder, p1) -> builder
-                                .clause(UpperCardinality.class, upperBound -> List.of(
-                                                may(sourceType.call(p1)),
-                                                // Violation of monotonicity: stop the propagation of inconsistencies, since the
-                                                // {@code invalidMultiplicity} pattern will already mark the model as invalid.
-                                                not(must(sourceType.call(p1))),
-                                                new CountUpperBoundLiteral(upperBound, linkType, List.of(p1, Variable.of())),
-                                                check(UpperCardinalityTerms.less(upperBound,
-                                                                UpperCardinalityTerms.constant(lowerBoundCardinality)))
-                                ))
-                                .action(
-                                                remove(sourceType, p1)
-                                )
-                ));
-        }
-
-        public static void configureTargetLowerBound(PartialRelation linkType, PartialRelation targetType,
-                                                                                                 int lowerBound, PropagationBuilder propagationBuilder) {
-                var name = linkType.name();
-                var lowerBoundCardinality = UpperCardinalities.atMost(lowerBound);
-                propagationBuilder.rule(Rule.of(name + "#lowerTarget", (builder, p1, p2) -> builder
-                                .clause(UpperCardinality.class, upperBound -> List.of(
-                                                must(targetType.call(p2)),
-                                                new CountUpperBoundLiteral(upperBound, linkType, List.of(Variable.of(), p2)),
-                                                check(UpperCardinalityTerms.lessEq(upperBound,
-                                                                UpperCardinalityTerms.constant(lowerBoundCardinality))),
-                                                may(linkType.call(p1, p2)),
-                                                not(must(linkType.call(p1, p2)))
-                                ))
-                                .action(
-                                                add(linkType, p1, p2)
-                                )
-                ));
-                propagationBuilder.rule(Rule.of(name + "#missingSource", (builder, p1) -> builder
-                                .clause(UpperCardinality.class, upperBound -> List.of(
-                                                may(targetType.call(p1)),
-                                                // Violation of monotonicity: stop the propagation of inconsistencies, since the
-                                                // {@code invalidMultiplicity} pattern will already mark the model as invalid.
-                                                not(must(targetType.call(p1))),
-                                                new CountUpperBoundLiteral(upperBound, linkType, List.of(Variable.of(), p1)),
-                                                check(UpperCardinalityTerms.less(upperBound,
-                                                                UpperCardinalityTerms.constant(lowerBoundCardinality)))
-                                ))
-                                .action(
-                                                remove(targetType, p1)
-                                )
-                ));
-        }
 }
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/crossreference/DirectedCrossReferenceTranslator.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/crossreference/DirectedCrossReferenceTranslator.java
index 2facb56d..d4c2afd2 100644
--- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/crossreference/DirectedCrossReferenceTranslator.java
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/crossreference/DirectedCrossReferenceTranslator.java
@@ -20,7 +20,6 @@ import tools.refinery.store.reasoning.representation.PartialRelation;
 import tools.refinery.store.reasoning.translator.PartialRelationTranslator;
 import tools.refinery.store.reasoning.translator.RoundingMode;
 import tools.refinery.store.reasoning.translator.TranslationException;
-import tools.refinery.store.reasoning.translator.multiplicity.ConstrainedMultiplicity;
 import tools.refinery.store.reasoning.translator.multiplicity.InvalidMultiplicityErrorTranslator;
 import tools.refinery.store.reasoning.translator.multiplicity.Multiplicity;
 import tools.refinery.store.representation.Symbol;
@@ -79,7 +78,6 @@ public class DirectedCrossReferenceTranslator implements ModelStoreConfiguration
                                 info.sourceMultiplicity()));
                 storeBuilder.with(new InvalidMultiplicityErrorTranslator(targetType, linkType, true,
                                 info.targetMultiplicity()));
-                storeBuilder.tryGetAdapter(PropagationBuilder.class).ifPresent(this::configureLowerMultiplicityPropagator);
         }
 
         private void configureWithDefaultUnknown(PartialRelationTranslator translator) {
@@ -148,48 +146,32 @@ public class DirectedCrossReferenceTranslator implements ModelStoreConfiguration
                 var targetType = info.targetType();
                 var mayNewSource = createMayHelper(sourceType, info.sourceMultiplicity(), false);
                 var mayNewTarget = createMayHelper(targetType, info.targetMultiplicity(), true);
-                storeBuilder.tryGetAdapter(PropagationBuilder.class).ifPresent(propagationBuilder -> propagationBuilder
-                                .rule(Rule.of(name + "#invalidLink", (builder, p1, p2) -> {
-                                        builder.clause(
-                                                        may(linkType.call(p1, p2)),
-                                                        not(may(sourceType.call(p1)))
-                                        );
-                                        builder.clause(
-                                                        may(linkType.call(p1, p2)),
-                                                        not(may(targetType.call(p2)))
-                                        );
-                                        if (info.isConstrained()) {
-                                                builder.clause(
-                                                                may(linkType.call(p1, p2)),
-                                                                not(must(linkType.call(p1, p2))),
-                                                                not(mayNewSource.call(p1))
-                                                );
-                                                builder.clause(
-                                                                may(linkType.call(p1, p2)),
-                                                                not(must(linkType.call(p1, p2))),
-                                                                not(mayNewTarget.call(p2))
-                                                );
-                                        }
-                                        builder.action(
-                                                        remove(linkType, p1, p2)
-                                        );
-                                })));
-        }
-
-        private void configureLowerMultiplicityPropagator(PropagationBuilder propagationBuilder) {
-                if (info.sourceMultiplicity() instanceof ConstrainedMultiplicity constrainedMultiplicity) {
-                        int lowerBound = constrainedMultiplicity.multiplicity().lowerBound();
-                        if (lowerBound >= 1) {
-                                var sourceType = info.sourceType();
-                                CrossReferenceUtils.configureSourceLowerBound(linkType, sourceType, lowerBound, propagationBuilder);
-                        }
-                }
-                if (info.targetMultiplicity() instanceof ConstrainedMultiplicity constrainedMultiplicity) {
-                        int lowerBound = constrainedMultiplicity.multiplicity().lowerBound();
-                        if (lowerBound >= 1) {
-                                var targetType = info.targetType();
-                                CrossReferenceUtils.configureTargetLowerBound(linkType, targetType, lowerBound, propagationBuilder);
+                // Fail if there is no {@link PropagationBuilder}, since it is required for soundness.
+                var propagationBuilder = storeBuilder.getAdapter(PropagationBuilder.class);
+                propagationBuilder.rule(Rule.of(name + "#invalidLink", (builder, p1, p2) -> {
+                        builder.clause(
+                                        may(linkType.call(p1, p2)),
+                                        not(may(sourceType.call(p1)))
+                        );
+                        builder.clause(
+                                        may(linkType.call(p1, p2)),
+                                        not(may(targetType.call(p2)))
+                        );
+                        if (info.isConstrained()) {
+                                builder.clause(
+                                                may(linkType.call(p1, p2)),
+                                                not(must(linkType.call(p1, p2))),
+                                                not(mayNewSource.call(p1))
+                                );
+                                builder.clause(
+                                                may(linkType.call(p1, p2)),
+                                                not(must(linkType.call(p1, p2))),
+                                                not(mayNewTarget.call(p2))
+                                );
                         }
-                }
+                        builder.action(
+                                        remove(linkType, p1, p2)
+                        );
+                }));
         }
 }
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/crossreference/UndirectedCrossReferenceTranslator.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/crossreference/UndirectedCrossReferenceTranslator.java
index 0a718033..494211fe 100644
--- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/crossreference/UndirectedCrossReferenceTranslator.java
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/crossreference/UndirectedCrossReferenceTranslator.java
@@ -19,7 +19,6 @@ import tools.refinery.store.reasoning.representation.PartialRelation;
 import tools.refinery.store.reasoning.translator.PartialRelationTranslator;
 import tools.refinery.store.reasoning.translator.RoundingMode;
 import tools.refinery.store.reasoning.translator.TranslationException;
-import tools.refinery.store.reasoning.translator.multiplicity.ConstrainedMultiplicity;
 import tools.refinery.store.reasoning.translator.multiplicity.InvalidMultiplicityErrorTranslator;
 import tools.refinery.store.representation.Symbol;
 
@@ -73,7 +72,6 @@ public class UndirectedCrossReferenceTranslator implements ModelStoreConfigurati
                 }
                 storeBuilder.with(translator);
                 storeBuilder.with(new InvalidMultiplicityErrorTranslator(type, linkType, false, info.multiplicity()));
-                storeBuilder.tryGetAdapter(PropagationBuilder.class).ifPresent(this::configureLowerMultiplicityPropagator);
         }
 
         private void configureWithDefaultUnknown(PartialRelationTranslator translator) {
@@ -127,33 +125,23 @@ public class UndirectedCrossReferenceTranslator implements ModelStoreConfigurati
                 var name = linkType.name();
                 var type = info.type();
                 var mayNewSource = CrossReferenceUtils.createMayHelper(linkType, type, info.multiplicity(), false);
-                storeBuilder.tryGetAdapter(PropagationBuilder.class).ifPresent(propagationBuilder -> propagationBuilder
-                                .rule(Rule.of(name + "#invalidLink", (builder, p1, p2) -> {
-                                        builder.clause(
-                                                        may(linkType.call(p1, p2)),
-                                                        not(may(type.call(p1)))
-                                        );
-                                        if (info.isConstrained()) {
-                                                builder.clause(
-                                                                may(linkType.call(p1, p2)),
-                                                                not(must(linkType.call(p1, p2))),
-                                                                not(mayNewSource.call(p1))
-                                                );
-                                        }
-                                        builder.action(
-                                                        remove(linkType, p1, p2)
-                                        );
-                                })));
-        }
-
-        private void configureLowerMultiplicityPropagator(PropagationBuilder propagationBuilder) {
-                var name = linkType.name();
-                if (info.multiplicity() instanceof ConstrainedMultiplicity constrainedMultiplicity) {
-                        int lowerBound = constrainedMultiplicity.multiplicity().lowerBound();
-                        if (lowerBound >= 1) {
-                                var type = info.type();
-                                CrossReferenceUtils.configureSourceLowerBound(linkType, type, lowerBound, propagationBuilder);
+                // Fail if there is no {@link PropagationBuilder}, since it is required for soundness.
+                var propagationBuilder = storeBuilder.getAdapter(PropagationBuilder.class);
+                propagationBuilder.rule(Rule.of(name + "#invalidLink", (builder, p1, p2) -> {
+                        builder.clause(
+                                        may(linkType.call(p1, p2)),
+                                        not(may(type.call(p1)))
+                        );
+                        if (info.isConstrained()) {
+                                builder.clause(
+                                                may(linkType.call(p1, p2)),
+                                                not(must(linkType.call(p1, p2))),
+                                                not(mayNewSource.call(p1))
+                                );
                         }
-                }
+                        builder.action(
+                                        remove(linkType, p1, p2)
+                        );
+                }));
         }
 }
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiplicity/InvalidMultiplicityErrorTranslator.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiplicity/InvalidMultiplicityErrorTranslator.java
index e2eff921..54e1e4cc 100644
--- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiplicity/InvalidMultiplicityErrorTranslator.java
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiplicity/InvalidMultiplicityErrorTranslator.java
@@ -11,6 +11,8 @@ import tools.refinery.logic.term.uppercardinality.FiniteUpperCardinality;
 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.Objectives;
 import tools.refinery.store.model.ModelStoreBuilder;
 import tools.refinery.store.model.ModelStoreConfiguration;
@@ -24,9 +26,12 @@ import tools.refinery.store.reasoning.translator.TranslationException;
 import java.util.List;
 
 import static tools.refinery.logic.literal.Literals.check;
+import static tools.refinery.logic.literal.Literals.not;
 import static tools.refinery.logic.term.int_.IntTerms.*;
-import static tools.refinery.store.reasoning.literal.PartialLiterals.candidateMust;
-import static tools.refinery.store.reasoning.literal.PartialLiterals.must;
+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.literal.PartialLiterals.may;
 
 public class InvalidMultiplicityErrorTranslator implements ModelStoreConfiguration {
         private final PartialRelation nodeType;
@@ -132,5 +137,50 @@ public class InvalidMultiplicityErrorTranslator implements ModelStoreConfigurati
                                 .candidateMay(candidateMayBuilder.build())
                                 .candidateMust(candidateMustBuilder.build())
                                 .objective(Objectives.value(objective)));
+
+                storeBuilder.tryGetAdapter(PropagationBuilder.class).ifPresent(this::configureLowerMultiplicityPropagator);
+        }
+
+        private void configureLowerMultiplicityPropagator(PropagationBuilder propagationBuilder) {
+                if (!(multiplicity instanceof ConstrainedMultiplicity constrainedMultiplicity)) {
+                        return;
+                }
+                int lowerBound = constrainedMultiplicity.multiplicity().lowerBound();
+                if (lowerBound < 1) {
+                        return;
+                }
+                var name = linkType.name();
+                var lowerBoundCardinality = UpperCardinalities.atMost(lowerBound);
+                var lowerSuffix = inverse ? "#lowerTarget" : "#lowerSource";
+                propagationBuilder.rule(Rule.of(name + lowerSuffix, (builder, p1, p2) -> builder
+                                .clause(UpperCardinality.class, upperBound -> List.of(
+                                                must(nodeType.call(inverse ? p2 : p1)),
+                                                new CountUpperBoundLiteral(upperBound, linkType,
+                                                                inverse ? List.of(Variable.of(), p2) : List.of(p1, Variable.of())),
+                                                check(UpperCardinalityTerms.lessEq(upperBound,
+                                                                UpperCardinalityTerms.constant(lowerBoundCardinality))),
+                                                may(linkType.call(p1, p2)),
+                                                not(must(linkType.call(p1, p2)))
+                                ))
+                                .action(
+                                                add(linkType, p1, p2)
+                                )
+                ));
+                var missingSuffix = inverse ? "#missingSource" : "#missingTarget";
+                propagationBuilder.rule(Rule.of(name + missingSuffix, (builder, p1) -> builder
+                                .clause(UpperCardinality.class, upperBound -> List.of(
+                                                may(nodeType.call(p1)),
+                                                // Violation of monotonicity: stop the propagation of inconsistencies, since the
+                                                // {@code invalidMultiplicity} pattern will already mark the model as invalid.
+                                                not(must(nodeType.call(p1))),
+                                                new CountUpperBoundLiteral(upperBound, linkType,
+                                                                inverse ? List.of(Variable.of(), p1) : List.of(p1, Variable.of())),
+                                                check(UpperCardinalityTerms.less(upperBound,
+                                                                UpperCardinalityTerms.constant(lowerBoundCardinality)))
+                                ))
+                                .action(
+                                                remove(nodeType, p1)
+                                )
+                ));
         }
 }