Merge pull request #39 from kris7t/partial-interpretation

Implement partial interpretation based model generation

6 files changed, 584 insertions, 0 deletions

diff --git a/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/BoundScopePropagator.java b/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/BoundScopePropagator.java
new file mode 100644
index 00000000..ecca6117
--- /dev/null
+++ b/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/BoundScopePropagator.java
@@ -0,0 +1,240 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.reasoning.scope;
+
+import com.google.ortools.linearsolver.MPConstraint;
+import com.google.ortools.linearsolver.MPObjective;
+import com.google.ortools.linearsolver.MPSolver;
+import com.google.ortools.linearsolver.MPVariable;
+import org.eclipse.collections.api.factory.primitive.IntObjectMaps;
+import org.eclipse.collections.api.factory.primitive.IntSets;
+import org.eclipse.collections.api.map.primitive.MutableIntObjectMap;
+import org.eclipse.collections.api.set.primitive.MutableIntSet;
+import tools.refinery.store.dse.propagation.BoundPropagator;
+import tools.refinery.store.dse.propagation.PropagationResult;
+import tools.refinery.store.model.Interpretation;
+import tools.refinery.store.model.Model;
+import tools.refinery.store.query.ModelQueryAdapter;
+import tools.refinery.store.representation.cardinality.*;
+import tools.refinery.store.tuple.Tuple;
+
+class BoundScopePropagator implements BoundPropagator {
+        private final Model model;
+        private final ModelQueryAdapter queryEngine;
+        private final Interpretation<CardinalityInterval> countInterpretation;
+        private final MPSolver solver;
+        private final MPObjective objective;
+        private final MutableIntObjectMap<MPVariable> variables = IntObjectMaps.mutable.empty();
+        private final MutableIntSet activeVariables = IntSets.mutable.empty();
+        private final TypeScopePropagator[] propagators;
+        private boolean changed = true;
+
+        public BoundScopePropagator(Model model, ScopePropagator storeAdapter) {
+                this.model = model;
+                queryEngine = model.getAdapter(ModelQueryAdapter.class);
+                countInterpretation = model.getInterpretation(storeAdapter.getCountSymbol());
+                solver = MPSolver.createSolver("GLOP");
+                solver.suppressOutput();
+                objective = solver.objective();
+                initializeVariables();
+                countInterpretation.addListener(this::countChanged, true);
+                var propagatorFactories = storeAdapter.getTypeScopePropagatorFactories();
+                propagators = new TypeScopePropagator[propagatorFactories.size()];
+                for (int i = 0; i < propagators.length; i++) {
+                        model.checkCancelled();
+                        propagators[i] = propagatorFactories.get(i).createPropagator(this);
+                }
+        }
+
+        ModelQueryAdapter getQueryEngine() {
+                return queryEngine;
+        }
+
+        private void initializeVariables() {
+                var cursor = countInterpretation.getAll();
+                while (cursor.move()) {
+                        var interval = cursor.getValue();
+                        if (!interval.equals(CardinalityIntervals.ONE)) {
+                                int nodeId = cursor.getKey().get(0);
+                                createVariable(nodeId, interval);
+                                activeVariables.add(nodeId);
+                        }
+                }
+        }
+
+        private MPVariable createVariable(int nodeId, CardinalityInterval interval) {
+                double lowerBound = interval.lowerBound();
+                double upperBound = getUpperBound(interval);
+                var variable = solver.makeNumVar(lowerBound, upperBound, "x" + nodeId);
+                variables.put(nodeId, variable);
+                return variable;
+        }
+
+        private void countChanged(Tuple key, CardinalityInterval fromValue, CardinalityInterval toValue,
+                                                          boolean ignoredRestoring) {
+                int nodeId = key.get(0);
+                if ((toValue == null || toValue.equals(CardinalityIntervals.ONE))) {
+                        if (fromValue != null && !fromValue.equals(CardinalityIntervals.ONE)) {
+                                removeActiveVariable(toValue, nodeId);
+                        }
+                        return;
+                }
+                if (fromValue == null || fromValue.equals(CardinalityIntervals.ONE)) {
+                        activeVariables.add(nodeId);
+                }
+                var variable = variables.get(nodeId);
+                if (variable == null) {
+                        createVariable(nodeId, toValue);
+                        markAsChanged();
+                        return;
+                }
+                double lowerBound = toValue.lowerBound();
+                double upperBound = getUpperBound(toValue);
+                if (variable.lb() != lowerBound) {
+                        variable.setLb(lowerBound);
+                        markAsChanged();
+                }
+                if (variable.ub() != upperBound) {
+                        variable.setUb(upperBound);
+                        markAsChanged();
+                }
+        }
+
+        private void removeActiveVariable(CardinalityInterval toValue, int nodeId) {
+                var variable = variables.get(nodeId);
+                if (variable == null || !activeVariables.remove(nodeId)) {
+                        throw new AssertionError("Variable not active: " + nodeId);
+                }
+                if (toValue == null) {
+                        variable.setBounds(0, 0);
+                } else {
+                        // Until queries are flushed and the constraints can be properly updated,
+                        // the variable corresponding to the (previous) multi-object has to stand in for a single object.
+                        variable.setBounds(1, 1);
+                }
+                markAsChanged();
+        }
+
+        MPConstraint makeConstraint() {
+                return solver.makeConstraint();
+        }
+
+        MPVariable getVariable(int nodeId) {
+                var variable = variables.get(nodeId);
+                if (variable != null) {
+                        return variable;
+                }
+                var interval = countInterpretation.get(Tuple.of(nodeId));
+                if (interval == null || interval.equals(CardinalityIntervals.ONE)) {
+                        interval = CardinalityIntervals.NONE;
+                } else {
+                        activeVariables.add(nodeId);
+                        markAsChanged();
+                }
+                return createVariable(nodeId, interval);
+        }
+
+        void markAsChanged() {
+                changed = true;
+        }
+
+        @Override
+        public PropagationResult propagateOne() {
+                queryEngine.flushChanges();
+                if (!changed) {
+                        return PropagationResult.UNCHANGED;
+                }
+                changed = false;
+                for (var propagator : propagators) {
+                        model.checkCancelled();
+                        if (!propagator.updateBounds()) {
+                                // Avoid logging GLOP error to console by checking for inconsistent constraints in advance.
+                                return PropagationResult.REJECTED;
+                        }
+                }
+                var result = PropagationResult.UNCHANGED;
+                if (activeVariables.isEmpty()) {
+                        return checkEmptiness();
+                }
+                var iterator = activeVariables.intIterator();
+                while (iterator.hasNext()) {
+                        int nodeId = iterator.next();
+                        var variable = variables.get(nodeId);
+                        if (variable == null) {
+                                throw new AssertionError("Missing active variable: " + nodeId);
+                        }
+                        result = result.andThen(propagateNode(nodeId, variable));
+                        if (result.isRejected()) {
+                                return result;
+                        }
+                }
+                return result;
+        }
+
+        private PropagationResult checkEmptiness() {
+                model.checkCancelled();
+                var emptinessCheckingResult = solver.solve();
+                return switch (emptinessCheckingResult) {
+                        case OPTIMAL, UNBOUNDED -> PropagationResult.UNCHANGED;
+                        case INFEASIBLE -> PropagationResult.REJECTED;
+                        default -> throw new IllegalStateException("Failed to check for consistency: " + emptinessCheckingResult);
+                };
+        }
+
+        private PropagationResult propagateNode(int nodeId, MPVariable variable) {
+                objective.setCoefficient(variable, 1);
+                try {
+                        model.checkCancelled();
+                        objective.setMinimization();
+                        var minimizationResult = solver.solve();
+                        int lowerBound;
+                        switch (minimizationResult) {
+                        case OPTIMAL -> lowerBound = RoundingUtil.roundUp(objective.value());
+                        case UNBOUNDED -> lowerBound = 0;
+                        case INFEASIBLE -> {
+                                return PropagationResult.REJECTED;
+                        }
+                        default -> throw new IllegalStateException("Failed to solve for minimum of %s: %s"
+                                        .formatted(variable, minimizationResult));
+                        }
+
+                        model.checkCancelled();
+                        objective.setMaximization();
+                        var maximizationResult = solver.solve();
+                        UpperCardinality upperBound;
+                        switch (maximizationResult) {
+                        case OPTIMAL -> upperBound = UpperCardinalities.atMost(RoundingUtil.roundDown(objective.value()));
+                        // Problem was feasible when minimizing, the only possible source of {@code UNBOUNDED_OR_INFEASIBLE} is
+                        // an unbounded maximization problem. See https://github.com/google/or-tools/issues/3319
+                        case UNBOUNDED, INFEASIBLE -> upperBound = UpperCardinalities.UNBOUNDED;
+                        default -> throw new IllegalStateException("Failed to solve for maximum of %s: %s"
+                                        .formatted(variable, minimizationResult));
+                        }
+
+                        var newInterval = CardinalityIntervals.between(lowerBound, upperBound);
+                        var oldInterval = countInterpretation.put(Tuple.of(nodeId), newInterval);
+                        if (newInterval.lowerBound() < oldInterval.lowerBound() ||
+                                        newInterval.upperBound().compareTo(oldInterval.upperBound()) > 0) {
+                                throw new IllegalArgumentException("Failed to refine multiplicity %s of node %d to %s"
+                                                .formatted(oldInterval, nodeId, newInterval));
+                        }
+                        return newInterval.equals(oldInterval) ? PropagationResult.UNCHANGED : PropagationResult.PROPAGATED;
+                } finally {
+                        objective.setCoefficient(variable, 0);
+                }
+        }
+
+        private static double getUpperBound(CardinalityInterval interval) {
+                var upperBound = interval.upperBound();
+                if (upperBound instanceof FiniteUpperCardinality finiteUpperCardinality) {
+                        return finiteUpperCardinality.finiteUpperBound();
+                } else if (upperBound instanceof UnboundedUpperCardinality) {
+                        return Double.POSITIVE_INFINITY;
+                } else {
+                        throw new IllegalArgumentException("Unknown upper bound: " + upperBound);
+                }
+        }
+}
diff --git a/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/LowerTypeScopePropagator.java b/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/LowerTypeScopePropagator.java
new file mode 100644
index 00000000..2be92464
--- /dev/null
+++ b/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/LowerTypeScopePropagator.java
@@ -0,0 +1,86 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.reasoning.scope;
+
+import tools.refinery.store.dse.transition.DesignSpaceExplorationBuilder;
+import tools.refinery.store.dse.transition.objectives.Criteria;
+import tools.refinery.store.dse.transition.objectives.Objectives;
+import tools.refinery.store.model.ModelStoreBuilder;
+import tools.refinery.store.query.dnf.AnyQuery;
+import tools.refinery.store.query.dnf.Query;
+import tools.refinery.store.query.dnf.RelationalQuery;
+import tools.refinery.store.query.term.Variable;
+import tools.refinery.store.reasoning.ReasoningBuilder;
+import tools.refinery.store.reasoning.literal.CountCandidateLowerBoundLiteral;
+import tools.refinery.store.reasoning.representation.PartialRelation;
+
+import java.util.Collection;
+import java.util.List;
+
+import static tools.refinery.store.query.literal.Literals.check;
+import static tools.refinery.store.query.term.int_.IntTerms.*;
+import static tools.refinery.store.reasoning.literal.PartialLiterals.may;
+import static tools.refinery.store.reasoning.translator.multiobject.MultiObjectTranslator.MULTI_VIEW;
+
+class LowerTypeScopePropagator extends TypeScopePropagator {
+        private final int lowerBound;
+
+        private LowerTypeScopePropagator(BoundScopePropagator adapter, int lowerBound, RelationalQuery allQuery,
+                                                                         RelationalQuery multiQuery) {
+                super(adapter, allQuery, multiQuery);
+                this.lowerBound = lowerBound;
+        }
+
+        @Override
+        protected void doUpdateBounds() {
+                constraint.setLb((lowerBound - getSingleCount()));
+        }
+
+        public static class Factory extends TypeScopePropagator.Factory {
+                private final PartialRelation type;
+                private final int lowerBound;
+                private final RelationalQuery allMay;
+                private final RelationalQuery multiMay;
+
+                public Factory(PartialRelation type, int lowerBound) {
+                        this.type = type;
+                        this.lowerBound = lowerBound;
+                        allMay = Query.of(type.name() + "#may", (builder, instance) -> builder.clause(
+                                        may(type.call(instance))
+                        ));
+                        multiMay = Query.of(type.name() + "#multiMay", (builder, instance) -> builder.clause(
+                                        may(type.call(instance)),
+                                        MULTI_VIEW.call(instance)
+                        ));
+                }
+
+                @Override
+                public TypeScopePropagator createPropagator(BoundScopePropagator adapter) {
+                        return new LowerTypeScopePropagator(adapter, lowerBound, allMay, multiMay);
+                }
+
+                @Override
+                protected Collection<AnyQuery> getQueries() {
+                        return List.of(allMay, multiMay);
+                }
+
+                @Override
+                public void configure(ModelStoreBuilder storeBuilder) {
+                        super.configure(storeBuilder);
+
+                        var requiredObjects = Query.of(type.name() + "#required", Integer.class, (builder, output) -> builder
+                                        .clause(Integer.class, candidateLowerBound -> List.of(
+                                                        new CountCandidateLowerBoundLiteral(candidateLowerBound, type, List.of(Variable.of())),
+                                                        output.assign(sub(constant(lowerBound), candidateLowerBound)),
+                                                        check(greater(output, constant(0)))
+                                        )));
+
+                        storeBuilder.getAdapter(ReasoningBuilder.class).objective(Objectives.value(requiredObjects));
+                        storeBuilder.tryGetAdapter(DesignSpaceExplorationBuilder.class).ifPresent(dseBuilder ->
+                                        dseBuilder.accept(Criteria.whenNoMatch(requiredObjects)));
+                }
+        }
+}
diff --git a/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/RoundingUtil.java b/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/RoundingUtil.java
new file mode 100644
index 00000000..986771a1
--- /dev/null
+++ b/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/RoundingUtil.java
@@ -0,0 +1,26 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.reasoning.scope;
+
+final class RoundingUtil {
+        private static final double TOLERANCE = 0.01;
+
+        private RoundingUtil() {
+                throw new IllegalStateException("This is a static utility class and should not be instantiated directly");
+        }
+
+        public static int roundUp(double value) {
+                double ceil = Math.ceil(value - TOLERANCE);
+                int intCeil = (int) ceil;
+                return Math.max(intCeil, 0);
+        }
+
+        public static int roundDown(double value) {
+                double floor = Math.floor(value + TOLERANCE);
+                int intFloor = (int) floor;
+                return Math.max(intFloor, 0);
+        }
+}
diff --git a/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/ScopePropagator.java b/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/ScopePropagator.java
new file mode 100644
index 00000000..25b1966c
--- /dev/null
+++ b/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/ScopePropagator.java
@@ -0,0 +1,102 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.reasoning.scope;
+
+import com.google.ortools.Loader;
+import tools.refinery.store.dse.propagation.PropagationBuilder;
+import tools.refinery.store.model.ModelStoreBuilder;
+import tools.refinery.store.model.ModelStoreConfiguration;
+import tools.refinery.store.reasoning.representation.PartialRelation;
+import tools.refinery.store.reasoning.translator.TranslationException;
+import tools.refinery.store.reasoning.translator.multiobject.MultiObjectTranslator;
+import tools.refinery.store.representation.Symbol;
+import tools.refinery.store.representation.cardinality.CardinalityInterval;
+import tools.refinery.store.representation.cardinality.FiniteUpperCardinality;
+
+import java.util.*;
+
+public class ScopePropagator implements ModelStoreConfiguration {
+        private final Symbol<CardinalityInterval> countSymbol;
+        private final Map<PartialRelation, CardinalityInterval> scopes = new LinkedHashMap<>();
+        private final List<TypeScopePropagator.Factory> typeScopePropagatorFactories = new ArrayList<>();
+
+        public ScopePropagator() {
+                this(MultiObjectTranslator.COUNT_STORAGE);
+        }
+
+        public ScopePropagator(Symbol<CardinalityInterval> countSymbol) {
+                if (countSymbol.arity() != 1) {
+                        throw new IllegalArgumentException("Count symbol must have arty 1, got %s with arity %d instead"
+                                        .formatted(countSymbol, countSymbol.arity()));
+                }
+                if (!countSymbol.valueType().equals(CardinalityInterval.class)) {
+                        throw new IllegalArgumentException("Count symbol must have CardinalityInterval values");
+                }
+                if (countSymbol.defaultValue() != null) {
+                        throw new IllegalArgumentException("Count symbol must default value null");
+                }
+                this.countSymbol = countSymbol;
+        }
+
+        public ScopePropagator scope(PartialRelation type, CardinalityInterval interval) {
+                if (type.arity() != 1) {
+                        throw new TranslationException(type, "Only types with arity 1 may have scopes, got %s with arity %d"
+                                        .formatted(type, type.arity()));
+                }
+                var newValue = scopes.compute(type, (ignoredKey, oldValue) ->
+                                oldValue == null ? interval : oldValue.meet(interval));
+                if (newValue.isEmpty()) {
+                        throw new TranslationException(type, "Unsatisfiable scope for type %s".formatted(type));
+                }
+                return this;
+        }
+
+        public ScopePropagator scopes(Map<PartialRelation, CardinalityInterval> scopes) {
+                return scopes(scopes.entrySet());
+        }
+
+        public ScopePropagator scopes(Collection<Map.Entry<PartialRelation, CardinalityInterval>> scopes) {
+                for (var entry : scopes) {
+                        scope(entry.getKey(), entry.getValue());
+                }
+                return this;
+        }
+
+        @Override
+        public void apply(ModelStoreBuilder storeBuilder) {
+                createTypeScopePropagatorFactories();
+                Loader.loadNativeLibraries();
+                for (var factory : typeScopePropagatorFactories) {
+                        factory.configure(storeBuilder);
+                }
+                storeBuilder.getAdapter(PropagationBuilder.class)
+                                .propagator(model -> new BoundScopePropagator(model, this));
+        }
+
+        private void createTypeScopePropagatorFactories() {
+                for (var entry : scopes.entrySet()) {
+                        var type = entry.getKey();
+                        var bounds = entry.getValue();
+                        if (bounds.lowerBound() > 0) {
+                                var lowerFactory = new LowerTypeScopePropagator.Factory(type, bounds.lowerBound());
+                                typeScopePropagatorFactories.add(lowerFactory);
+                        }
+                        if (bounds.upperBound() instanceof FiniteUpperCardinality finiteUpperCardinality) {
+                                var upperFactory = new UpperTypeScopePropagator.Factory(type,
+                                                finiteUpperCardinality.finiteUpperBound());
+                                typeScopePropagatorFactories.add(upperFactory);
+                        }
+                }
+        }
+
+        Symbol<CardinalityInterval> getCountSymbol() {
+                return countSymbol;
+        }
+
+        List<TypeScopePropagator.Factory> getTypeScopePropagatorFactories() {
+                return typeScopePropagatorFactories;
+        }
+}
diff --git a/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/TypeScopePropagator.java b/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/TypeScopePropagator.java
new file mode 100644
index 00000000..bb50656b
--- /dev/null
+++ b/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/TypeScopePropagator.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.scope;
+
+import com.google.ortools.linearsolver.MPConstraint;
+import tools.refinery.store.model.ModelStoreBuilder;
+import tools.refinery.store.query.ModelQueryBuilder;
+import tools.refinery.store.query.dnf.AnyQuery;
+import tools.refinery.store.query.dnf.RelationalQuery;
+import tools.refinery.store.query.resultset.ResultSet;
+import tools.refinery.store.tuple.Tuple;
+
+import java.util.Collection;
+
+abstract class TypeScopePropagator {
+        private final BoundScopePropagator adapter;
+        private final ResultSet<Boolean> allNodes;
+        private final ResultSet<Boolean> multiNodes;
+        protected final MPConstraint constraint;
+
+        protected TypeScopePropagator(BoundScopePropagator adapter, RelationalQuery allQuery,
+                                                                  RelationalQuery multiQuery) {
+                this.adapter = adapter;
+                var queryEngine = adapter.getQueryEngine();
+                allNodes = queryEngine.getResultSet(allQuery);
+                multiNodes = queryEngine.getResultSet(multiQuery);
+                constraint = adapter.makeConstraint();
+                constraint.setBounds(0, Double.POSITIVE_INFINITY);
+                var cursor = multiNodes.getAll();
+                while (cursor.move()) {
+                        var variable = adapter.getVariable(cursor.getKey().get(0));
+                        constraint.setCoefficient(variable, 1);
+                }
+                allNodes.addListener(this::allChanged);
+                multiNodes.addListener(this::multiChanged);
+        }
+
+        protected abstract void doUpdateBounds();
+
+        public boolean updateBounds() {
+                doUpdateBounds();
+                return constraint.lb() <= constraint.ub();
+        }
+
+        protected int getSingleCount() {
+                return allNodes.size() - multiNodes.size();
+        }
+
+        private void allChanged(Tuple ignoredKey, Boolean ignoredOldValue, Boolean ignoredNewValue) {
+                adapter.markAsChanged();
+        }
+
+        private void multiChanged(Tuple key, Boolean ignoredOldValue, Boolean newValue) {
+                var variable = adapter.getVariable(key.get(0));
+                constraint.setCoefficient(variable, Boolean.TRUE.equals(newValue) ? 1 : 0);
+                adapter.markAsChanged();
+        }
+
+        public abstract static class Factory {
+                public abstract TypeScopePropagator createPropagator(BoundScopePropagator adapter);
+
+                protected abstract Collection<AnyQuery> getQueries();
+
+                public void configure(ModelStoreBuilder storeBuilder) {
+                        storeBuilder.getAdapter(ModelQueryBuilder.class).queries(getQueries());
+                }
+        }
+}
diff --git a/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/UpperTypeScopePropagator.java b/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/UpperTypeScopePropagator.java
new file mode 100644
index 00000000..4aba5aac
--- /dev/null
+++ b/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/UpperTypeScopePropagator.java
@@ -0,0 +1,59 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.reasoning.scope;
+
+import tools.refinery.store.query.dnf.AnyQuery;
+import tools.refinery.store.query.dnf.Query;
+import tools.refinery.store.query.dnf.RelationalQuery;
+import tools.refinery.store.reasoning.representation.PartialRelation;
+
+import java.util.Collection;
+import java.util.List;
+
+import static tools.refinery.store.reasoning.literal.PartialLiterals.must;
+import static tools.refinery.store.reasoning.translator.multiobject.MultiObjectTranslator.MULTI_VIEW;
+
+class UpperTypeScopePropagator extends TypeScopePropagator {
+        private final int upperBound;
+
+        private UpperTypeScopePropagator(BoundScopePropagator adapter, int upperBound, RelationalQuery allQuery,
+                                                                         RelationalQuery multiQuery) {
+                super(adapter, allQuery, multiQuery);
+                this.upperBound = upperBound;
+        }
+
+        @Override
+        protected void doUpdateBounds() {
+                constraint.setUb((upperBound - getSingleCount()));
+        }
+
+        public static class Factory extends TypeScopePropagator.Factory {
+                private final int upperBound;
+                private final RelationalQuery allMust;
+                private final RelationalQuery multiMust;
+
+                public Factory(PartialRelation type, int upperBound) {
+                        this.upperBound = upperBound;
+                        allMust = Query.of(type.name() + "#must", (builder, instance) -> builder.clause(
+                                        must(type.call(instance))
+                        ));
+                        multiMust = Query.of(type.name() + "#multiMust", (builder, instance) -> builder.clause(
+                                        must(type.call(instance)),
+                                        MULTI_VIEW.call(instance)
+                        ));
+                }
+
+                @Override
+                public TypeScopePropagator createPropagator(BoundScopePropagator adapter) {
+                        return new UpperTypeScopePropagator(adapter, upperBound, allMust, multiMust);
+                }
+
+                @Override
+                protected Collection<AnyQuery> getQueries() {
+                        return List.of(allMust, multiMust);
+                }
+        }
+}