feat(reasoning): lower bound propagationrules

4 files changed, 218 insertions, 52 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 1183d456..c862bc33 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
@@ -5,14 +5,18 @@
  */
 package tools.refinery.store.reasoning.translator.containment;
 
+import tools.refinery.logic.dnf.Dnf;
 import tools.refinery.logic.dnf.Query;
 import tools.refinery.logic.dnf.RelationalQuery;
 import tools.refinery.logic.literal.Connectivity;
 import tools.refinery.logic.literal.Literal;
 import tools.refinery.logic.literal.RepresentativeElectionLiteral;
+import tools.refinery.logic.term.ConstantTerm;
 import tools.refinery.logic.term.Variable;
 import tools.refinery.logic.term.cardinalityinterval.CardinalityIntervals;
+import tools.refinery.logic.term.int_.IntTerms;
 import tools.refinery.logic.term.uppercardinality.FiniteUpperCardinality;
+import tools.refinery.store.dse.propagation.PropagationBuilder;
 import tools.refinery.store.dse.transition.DesignSpaceExplorationBuilder;
 import tools.refinery.store.dse.transition.Rule;
 import tools.refinery.store.model.ModelStoreBuilder;
@@ -26,6 +30,7 @@ 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;
@@ -35,10 +40,10 @@ import java.util.ArrayList;
 import java.util.List;
 import java.util.Map;
 
-import static tools.refinery.logic.term.int_.IntTerms.constant;
-import static tools.refinery.logic.term.int_.IntTerms.less;
 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.EXISTS_SYMBOL;
 import static tools.refinery.store.reasoning.actions.PartialActionLiterals.add;
 import static tools.refinery.store.reasoning.actions.PartialActionLiterals.focus;
@@ -107,6 +112,7 @@ public class ContainmentHierarchyTranslator implements ModelStoreConfiguration {
                         translateInvalidMultiplicity(storeBuilder, linkType, info);
                 }
                 translateFocusNotContained(storeBuilder);
+                storeBuilder.tryGetAdapter(PropagationBuilder.class).ifPresent(this::configurePropagationBuilder);
         }
 
         private void translateContainmentLinkType(ModelStoreBuilder storeBuilder, PartialRelation linkType,
@@ -119,10 +125,10 @@ public class ContainmentHierarchyTranslator implements ModelStoreConfiguration {
                 var mayNewSourceHelper = Query.of(name + "#mayNewSourceHelper", (builder, parent) -> {
                         var literals = new ArrayList<Literal>();
                         literals.add(may(sourceType.call(parent)));
-                        if (upperCardinality instanceof FiniteUpperCardinality finiteUpperCardinality) {
+                        if (upperCardinality instanceof FiniteUpperCardinality(var finiteUpperBound)) {
                                 var existingCount = Variable.of("existingCount", Integer.class);
                                 literals.add(new CountLowerBoundLiteral(existingCount, linkType, List.of(parent, Variable.of())));
-                                literals.add(check(less(existingCount, constant(finiteUpperCardinality.finiteUpperBound()))));
+                                literals.add(check(less(existingCount, constant(finiteUpperBound))));
                         }
                         builder.clause(literals);
                 });
@@ -260,4 +266,55 @@ public class ContainmentHierarchyTranslator implements ModelStoreConfiguration {
                                                 focus(multi, Variable.of())
                                 )));
         }
+
+        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");
+                        var p2 = builder.parameter("target");
+                        var output = builder.parameter("containmentLink", PartialRelation.class);
+                        for (var containmentLink : containmentInfoMap.keySet()) {
+                                builder.clause(
+                                                must(CONTAINS_SYMBOL.call(p1, p2)),
+                                                may(containmentLink.call(p1, p2)),
+                                                output.assign(new ConstantTerm<>(PartialRelation.class, containmentLink))
+                                );
+                        }
+                });
+                for (var containmentLink : containmentInfoMap.keySet()) {
+                        propagationBuilder.rule(Rule.of(containmentLink.name() + "#single", (builder, p1, p2) -> builder
+                                        .clause(Integer.class, containmentCount -> List.of(
+                                                        must(CONTAINS_SYMBOL.call(p1, p2)),
+                                                        may(containmentLink.call(p1, p2)),
+                                                        not(must(containmentLink.call(p1, p2))),
+                                                        containmentCount.assign(possibleContainment.count(p1, p2,
+                                    Variable.of(PartialRelation.class))),
+                                                        check(IntTerms.eq(containmentCount, constant(1)))
+                                        ))
+                                        .action(
+                                                        add(containmentLink, p1, p2)
+                                        )
+                        ));
+                }
+        }
 }
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 56c9d682..be9fcb9d 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,8 +12,14 @@ 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;
 
@@ -21,12 +27,15 @@ 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.literal.PartialLiterals.candidateMay;
-import static tools.refinery.store.reasoning.literal.PartialLiterals.may;
+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;
 
-class CrossReferenceUtils {
+public class CrossReferenceUtils {
         private CrossReferenceUtils() {
                 throw new IllegalStateException("This is a static utility class and should not be instantiated directly");
         }
@@ -77,4 +86,72 @@ 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(
+                                                not(MULTI_VIEW.call(p1)),
+                                                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(
+                                                not(MULTI_VIEW.call(p2)),
+                                                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 1985a43f..2facb56d 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,13 +20,14 @@ 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;
 
 import static tools.refinery.logic.literal.Literals.not;
 import static tools.refinery.store.reasoning.actions.PartialActionLiterals.add;
-import static tools.refinery.store.reasoning.actions.PartialActionLiterals.merge;
+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;
 
@@ -78,6 +79,7 @@ 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) {
@@ -135,7 +137,8 @@ public class DirectedCrossReferenceTranslator implements ModelStoreConfiguration
                 return CrossReferenceUtils.createMayHelper(linkType, type, multiplicity, inverse);
         }
 
-        private RelationalQuery createCandidateMayHelper(PartialRelation type, Multiplicity multiplicity, boolean inverse) {
+        private RelationalQuery createCandidateMayHelper(PartialRelation type, Multiplicity multiplicity,
+                                                                                                         boolean inverse) {
                 return CrossReferenceUtils.createCandidateMayHelper(linkType, type, multiplicity, inverse);
         }
 
@@ -145,32 +148,48 @@ public class DirectedCrossReferenceTranslator implements ModelStoreConfiguration
                 var targetType = info.targetType();
                 var mayNewSource = createMayHelper(sourceType, info.sourceMultiplicity(), false);
                 var mayNewTarget = createMayHelper(targetType, info.targetMultiplicity(), true);
-                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(
-                                        merge(linkType, TruthValue.FALSE, p1, p2)
-                        );
-                }));
+                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);
+                        }
+                }
+        }
 }
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 af0ddd2e..0a718033 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,12 +19,13 @@ 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;
 
 import static tools.refinery.logic.literal.Literals.not;
 import static tools.refinery.store.reasoning.actions.PartialActionLiterals.add;
-import static tools.refinery.store.reasoning.actions.PartialActionLiterals.merge;
+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;
 
@@ -72,6 +73,7 @@ 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) {
@@ -125,22 +127,33 @@ public class UndirectedCrossReferenceTranslator implements ModelStoreConfigurati
                 var name = linkType.name();
                 var type = info.type();
                 var mayNewSource = CrossReferenceUtils.createMayHelper(linkType, type, info.multiplicity(), false);
-                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))
-                                );
+                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);
                         }
-                        builder.action(
-                                        merge(linkType, TruthValue.FALSE, p1, p2)
-                        );
-                }));
+                }
         }
 }