18 files changed, 1039 insertions, 1 deletions

diff --git a/gradle/libs.versions.toml b/gradle/libs.versions.toml
index a38d589c..e4c59339 100644
--- a/gradle/libs.versions.toml
+++ b/gradle/libs.versions.toml
@@ -40,6 +40,7 @@ mockito-junit = { group = "org.mockito", name = "mockito-junit-jupiter", version
 mwe-utils = { group = "org.eclipse.emf", name = "org.eclipse.emf.mwe.utils", version = "1.9.0" }
 mwe2-launch = { group = "org.eclipse.emf", name = "org.eclipse.emf.mwe2.launch", version.ref = "mwe2" }
 mwe2-lib = { group = "org.eclipse.emf", name = "org.eclipse.emf.mwe2.lib", version.ref = "mwe2" }
+ortools = { group = "com.google.ortools", name = "ortools-java", version = "9.7.2996" }
 slf4j-api = { group = "org.slf4j", name = "slf4j-api", version.ref = "slf4j" }
 slf4j-simple = { group = "org.slf4j", name = "slf4j-simple", version.ref = "slf4j" }
 slf4j-log4j = { group = "org.slf4j", name = "log4j-over-slf4j", version.ref = "slf4j" }
diff --git a/settings.gradle.kts b/settings.gradle.kts
index 15aa7a58..d0f82de8 100644
--- a/settings.gradle.kts
+++ b/settings.gradle.kts
@@ -17,6 +17,7 @@ include(
                 "store-query",
                 "store-query-viatra",
                 "store-reasoning",
+                "store-reasoning-scope",
                 "viatra-runtime",
                 "viatra-runtime-localsearch",
                 "viatra-runtime-rete",
diff --git a/subprojects/store-reasoning-scope/build.gradle.kts b/subprojects/store-reasoning-scope/build.gradle.kts
new file mode 100644
index 00000000..6e41dc8e
--- /dev/null
+++ b/subprojects/store-reasoning-scope/build.gradle.kts
@@ -0,0 +1,17 @@
+/*
+ * SPDX-FileCopyrightText: 2021-2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+
+plugins {
+        id("tools.refinery.gradle.java-library")
+}
+
+dependencies {
+        api(project(":refinery-store-reasoning"))
+        implementation(libs.eclipseCollections.api)
+        implementation(libs.ortools)
+        runtimeOnly(libs.eclipseCollections)
+        testImplementation(project(":refinery-store-query-viatra"))
+}
diff --git a/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/ScopePropagatorAdapter.java b/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/ScopePropagatorAdapter.java
new file mode 100644
index 00000000..c2d3f59e
--- /dev/null
+++ b/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/ScopePropagatorAdapter.java
@@ -0,0 +1,21 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.reasoning.scope;
+
+import tools.refinery.store.adapter.ModelAdapter;
+import tools.refinery.store.reasoning.refinement.RefinementResult;
+import tools.refinery.store.reasoning.scope.internal.ScopePropagatorBuilderImpl;
+
+public interface ScopePropagatorAdapter extends ModelAdapter {
+        @Override
+        ScopePropagatorStoreAdapter getStoreAdapter();
+
+        RefinementResult propagate();
+
+        static ScopePropagatorBuilder builder() {
+                return new ScopePropagatorBuilderImpl();
+        }
+}
diff --git a/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/ScopePropagatorBuilder.java b/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/ScopePropagatorBuilder.java
new file mode 100644
index 00000000..a17e04a4
--- /dev/null
+++ b/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/ScopePropagatorBuilder.java
@@ -0,0 +1,21 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.reasoning.scope;
+
+import tools.refinery.store.adapter.ModelAdapterBuilder;
+import tools.refinery.store.model.ModelStore;
+import tools.refinery.store.reasoning.representation.PartialRelation;
+import tools.refinery.store.representation.Symbol;
+import tools.refinery.store.representation.cardinality.CardinalityInterval;
+
+public interface ScopePropagatorBuilder extends ModelAdapterBuilder {
+        ScopePropagatorBuilder countSymbol(Symbol<CardinalityInterval> countSymbol);
+
+        ScopePropagatorBuilder scope(PartialRelation type, CardinalityInterval interval);
+
+        @Override
+        ScopePropagatorStoreAdapter build(ModelStore store);
+}
diff --git a/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/ScopePropagatorStoreAdapter.java b/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/ScopePropagatorStoreAdapter.java
new file mode 100644
index 00000000..65d9c38d
--- /dev/null
+++ b/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/ScopePropagatorStoreAdapter.java
@@ -0,0 +1,16 @@
+/*
+ * 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.adapter.ModelStoreAdapter;
+import tools.refinery.store.reasoning.representation.PartialRelation;
+import tools.refinery.store.representation.cardinality.CardinalityInterval;
+
+import java.util.Map;
+
+public interface ScopePropagatorStoreAdapter extends ModelStoreAdapter {
+        Map<PartialRelation, CardinalityInterval> getScopes();
+}
diff --git a/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/internal/LowerTypeScopePropagator.java b/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/internal/LowerTypeScopePropagator.java
new file mode 100644
index 00000000..b1c421b7
--- /dev/null
+++ b/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/internal/LowerTypeScopePropagator.java
@@ -0,0 +1,58 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.reasoning.scope.internal;
+
+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.may;
+
+class LowerTypeScopePropagator extends TypeScopePropagator {
+        private final int lowerBound;
+
+        private LowerTypeScopePropagator(ScopePropagatorAdapterImpl adapter, int lowerBound, RelationalQuery allQuery,
+                                                                        RelationalQuery multiQuery) {
+                super(adapter, allQuery, multiQuery);
+                this.lowerBound = lowerBound;
+        }
+
+        @Override
+        public void updateBounds() {
+                constraint.setLb(lowerBound - getSingleCount());
+        }
+
+        public static class Factory implements TypeScopePropagator.Factory {
+                private final int lowerBound;
+                private final RelationalQuery allMay;
+                private final RelationalQuery multiMay;
+
+                public Factory(RelationalQuery multi, PartialRelation type, int lowerBound) {
+                        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.call(instance)
+                        ));
+                }
+
+                @Override
+                public TypeScopePropagator createPropagator(ScopePropagatorAdapterImpl adapter) {
+                        return new LowerTypeScopePropagator(adapter, lowerBound, allMay, multiMay);
+                }
+
+                @Override
+                public Collection<AnyQuery> getQueries() {
+                        return List.of(allMay, multiMay);
+                }
+        }
+}
diff --git a/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/internal/RoundingUtil.java b/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/internal/RoundingUtil.java
new file mode 100644
index 00000000..a6d663ea
--- /dev/null
+++ b/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/internal/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.internal;
+
+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/internal/ScopePropagatorAdapterImpl.java b/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/internal/ScopePropagatorAdapterImpl.java
new file mode 100644
index 00000000..0d594701
--- /dev/null
+++ b/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/internal/ScopePropagatorAdapterImpl.java
@@ -0,0 +1,244 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.reasoning.scope.internal;
+
+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.model.Interpretation;
+import tools.refinery.store.model.Model;
+import tools.refinery.store.query.ModelQueryAdapter;
+import tools.refinery.store.reasoning.refinement.RefinementResult;
+import tools.refinery.store.reasoning.scope.ScopePropagatorAdapter;
+import tools.refinery.store.reasoning.scope.ScopePropagatorStoreAdapter;
+import tools.refinery.store.representation.cardinality.*;
+import tools.refinery.store.tuple.Tuple;
+
+class ScopePropagatorAdapterImpl implements ScopePropagatorAdapter {
+        private final Model model;
+        private final ScopePropagatorStoreAdapterImpl storeAdapter;
+        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 ScopePropagatorAdapterImpl(Model model, ScopePropagatorStoreAdapterImpl storeAdapter) {
+                this.model = model;
+                this.storeAdapter = storeAdapter;
+                queryEngine = model.getAdapter(ModelQueryAdapter.class);
+                countInterpretation = model.getInterpretation(storeAdapter.getCountSymbol());
+                solver = MPSolver.createSolver("GLOP");
+                objective = solver.objective();
+                initializeVariables();
+                countInterpretation.addListener(this::countChanged, true);
+                var propagatorFactories = storeAdapter.getPropagatorFactories();
+                propagators = new TypeScopePropagator[propagatorFactories.size()];
+                for (int i = 0; i < propagators.length; i++) {
+                        propagators[i] = propagatorFactories.get(i).createPropagator(this);
+                }
+        }
+
+        @Override
+        public Model getModel() {
+                return model;
+        }
+
+        @Override
+        public ScopePropagatorStoreAdapter getStoreAdapter() {
+                return storeAdapter;
+        }
+
+        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)) {
+                                var variable = variables.get(nodeId);
+                                if (variable == null || !activeVariables.remove(nodeId)) {
+                                        throw new AssertionError("Variable not active: " + nodeId);
+                                }
+                                variable.setBounds(0, 0);
+                                markAsChanged();
+                        }
+                        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();
+                }
+        }
+
+        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 RefinementResult propagate() {
+                var result = RefinementResult.UNCHANGED;
+                RefinementResult currentRoundResult;
+                do {
+                        currentRoundResult = propagateOne();
+                        result = result.andThen(currentRoundResult);
+                        if (result.isRejected()) {
+                                return result;
+                        }
+                } while (currentRoundResult != RefinementResult.UNCHANGED);
+                return result;
+        }
+
+        private RefinementResult propagateOne() {
+                queryEngine.flushChanges();
+                if (!changed) {
+                        return RefinementResult.UNCHANGED;
+                }
+                changed = false;
+                for (var propagator : propagators) {
+                        propagator.updateBounds();
+                }
+                var result = RefinementResult.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 RefinementResult checkEmptiness() {
+                var emptinessCheckingResult = solver.solve();
+                return switch (emptinessCheckingResult) {
+                        case OPTIMAL, UNBOUNDED -> RefinementResult.UNCHANGED;
+                        case INFEASIBLE -> RefinementResult.REJECTED;
+                        default -> throw new IllegalStateException("Failed to check for consistency: " + emptinessCheckingResult);
+                };
+        }
+
+        private RefinementResult propagateNode(int nodeId, MPVariable variable) {
+                objective.setCoefficient(variable, 1);
+                try {
+                        objective.setMinimization();
+                        var minimizationResult = solver.solve();
+                        int lowerBound;
+                        switch (minimizationResult) {
+                        case OPTIMAL -> lowerBound = RoundingUtil.roundUp(objective.value());
+                        case UNBOUNDED -> lowerBound = 0;
+                        case INFEASIBLE -> {
+                                return RefinementResult.REJECTED;
+                        }
+                        default -> throw new IllegalStateException("Failed to solve for minimum of %s: %s"
+                                        .formatted(variable, minimizationResult));
+                        }
+
+                        objective.setMaximization();
+                        var maximizationResult = solver.solve();
+                        UpperCardinality upperBound;
+                        switch (maximizationResult) {
+                        case OPTIMAL -> upperBound = UpperCardinalities.atMost(RoundingUtil.roundDown(objective.value()));
+                        case UNBOUNDED -> upperBound = UpperCardinalities.UNBOUNDED;
+                        case INFEASIBLE -> {
+                                return RefinementResult.REJECTED;
+                        }
+                        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) ? RefinementResult.UNCHANGED : RefinementResult.REFINED;
+                } 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/internal/ScopePropagatorBuilderImpl.java b/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/internal/ScopePropagatorBuilderImpl.java
new file mode 100644
index 00000000..f383ebeb
--- /dev/null
+++ b/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/internal/ScopePropagatorBuilderImpl.java
@@ -0,0 +1,105 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.reasoning.scope.internal;
+
+import com.google.ortools.Loader;
+import tools.refinery.store.adapter.AbstractModelAdapterBuilder;
+import tools.refinery.store.model.ModelStore;
+import tools.refinery.store.model.ModelStoreBuilder;
+import tools.refinery.store.query.ModelQueryBuilder;
+import tools.refinery.store.query.dnf.Query;
+import tools.refinery.store.reasoning.representation.PartialRelation;
+import tools.refinery.store.reasoning.scope.ScopePropagatorBuilder;
+import tools.refinery.store.reasoning.scope.ScopePropagatorStoreAdapter;
+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.*;
+
+import static tools.refinery.store.query.literal.Literals.not;
+import static tools.refinery.store.reasoning.ReasoningAdapter.EQUALS_SYMBOL;
+import static tools.refinery.store.reasoning.ReasoningAdapter.EXISTS_SYMBOL;
+import static tools.refinery.store.reasoning.literal.PartialLiterals.may;
+import static tools.refinery.store.reasoning.literal.PartialLiterals.must;
+
+public class ScopePropagatorBuilderImpl extends AbstractModelAdapterBuilder<ScopePropagatorStoreAdapter>
+                implements ScopePropagatorBuilder {
+        private Symbol<CardinalityInterval> countSymbol = MultiObjectTranslator.COUNT_STORAGE;
+        private final Map<PartialRelation, CardinalityInterval> scopes = new LinkedHashMap<>();
+        private List<TypeScopePropagator.Factory> typeScopePropagatorFactories;
+
+        @Override
+        public ScopePropagatorBuilder countSymbol(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;
+                return this;
+        }
+
+        @Override
+        public ScopePropagatorBuilder 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;
+        }
+
+        @Override
+        protected void doConfigure(ModelStoreBuilder storeBuilder) {
+                var multiQuery = Query.of("MULTI", (builder, instance) -> builder
+                                .clause(
+                                                may(EXISTS_SYMBOL.call(instance)),
+                                                not(must(EXISTS_SYMBOL.call(instance)))
+                                )
+                                .clause(
+                                                may(EXISTS_SYMBOL.call(instance)),
+                                                not(must(EQUALS_SYMBOL.call(instance, instance)))
+                                )
+                );
+                typeScopePropagatorFactories = new ArrayList<>(scopes.size());
+                for (var entry : scopes.entrySet()) {
+                        var type = entry.getKey();
+                        var bounds = entry.getValue();
+                        if (bounds.lowerBound() > 0) {
+                                var lowerFactory = new LowerTypeScopePropagator.Factory(multiQuery, type, bounds.lowerBound());
+                                typeScopePropagatorFactories.add(lowerFactory);
+                        }
+                        if (bounds.upperBound() instanceof FiniteUpperCardinality finiteUpperCardinality) {
+                                var upperFactory = new UpperTypeScopePropagator.Factory(multiQuery, type,
+                                                finiteUpperCardinality.finiteUpperBound());
+                                typeScopePropagatorFactories.add(upperFactory);
+                        }
+                }
+                var queryBuilder = storeBuilder.getAdapter(ModelQueryBuilder.class);
+                for (var factory : typeScopePropagatorFactories) {
+                        queryBuilder.queries(factory.getQueries());
+                }
+        }
+
+        @Override
+        protected ScopePropagatorStoreAdapter doBuild(ModelStore store) {
+                Loader.loadNativeLibraries();
+                return new ScopePropagatorStoreAdapterImpl(store, countSymbol, Collections.unmodifiableMap(scopes),
+                                Collections.unmodifiableList(typeScopePropagatorFactories));
+        }
+}
diff --git a/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/internal/ScopePropagatorStoreAdapterImpl.java b/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/internal/ScopePropagatorStoreAdapterImpl.java
new file mode 100644
index 00000000..282ffe6f
--- /dev/null
+++ b/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/internal/ScopePropagatorStoreAdapterImpl.java
@@ -0,0 +1,58 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.reasoning.scope.internal;
+
+import tools.refinery.store.adapter.ModelAdapter;
+import tools.refinery.store.model.Model;
+import tools.refinery.store.model.ModelStore;
+import tools.refinery.store.reasoning.representation.PartialRelation;
+import tools.refinery.store.reasoning.scope.ScopePropagatorStoreAdapter;
+import tools.refinery.store.representation.Symbol;
+import tools.refinery.store.representation.cardinality.CardinalityInterval;
+
+import java.util.List;
+import java.util.Map;
+
+// Not a record, because we want to control getter visibility.
+@SuppressWarnings("ClassCanBeRecord")
+class ScopePropagatorStoreAdapterImpl implements ScopePropagatorStoreAdapter {
+        private final ModelStore store;
+        private final Symbol<CardinalityInterval> countSymbol;
+        private final Map<PartialRelation, CardinalityInterval> scopes;
+        private final List<TypeScopePropagator.Factory> propagatorFactories;
+
+        public ScopePropagatorStoreAdapterImpl(
+                        ModelStore store, Symbol<CardinalityInterval> countSymbol,
+                        Map<PartialRelation, CardinalityInterval> scopes, List<TypeScopePropagator.Factory> propagatorFactories) {
+                this.store = store;
+                this.countSymbol = countSymbol;
+                this.scopes = scopes;
+                this.propagatorFactories = propagatorFactories;
+        }
+
+        @Override
+        public ModelStore getStore() {
+                return store;
+        }
+
+        Symbol<CardinalityInterval> getCountSymbol() {
+                return countSymbol;
+        }
+
+        @Override
+        public Map<PartialRelation, CardinalityInterval> getScopes() {
+                return scopes;
+        }
+
+        public List<TypeScopePropagator.Factory> getPropagatorFactories() {
+                return propagatorFactories;
+        }
+
+        @Override
+        public ModelAdapter createModelAdapter(Model model) {
+                return new ScopePropagatorAdapterImpl(model, this);
+        }
+}
diff --git a/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/internal/TypeScopePropagator.java b/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/internal/TypeScopePropagator.java
new file mode 100644
index 00000000..98f6ed8b
--- /dev/null
+++ b/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/internal/TypeScopePropagator.java
@@ -0,0 +1,61 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.reasoning.scope.internal;
+
+import com.google.ortools.linearsolver.MPConstraint;
+import tools.refinery.store.query.ModelQueryAdapter;
+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 ScopePropagatorAdapterImpl adapter;
+        private final ResultSet<Boolean> allNodes;
+        private final ResultSet<Boolean> multiNodes;
+        protected final MPConstraint constraint;
+
+        protected TypeScopePropagator(ScopePropagatorAdapterImpl adapter, RelationalQuery allQuery,
+                                                           RelationalQuery multiQuery) {
+                this.adapter = adapter;
+                var queryEngine = adapter.getModel().getAdapter(ModelQueryAdapter.class);
+                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);
+        }
+
+        public abstract void updateBounds();
+
+        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();
+        }
+
+        interface Factory {
+                TypeScopePropagator createPropagator(ScopePropagatorAdapterImpl adapter);
+
+                Collection<AnyQuery> getQueries();
+        }
+}
diff --git a/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/internal/UpperTypeScopePropagator.java b/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/internal/UpperTypeScopePropagator.java
new file mode 100644
index 00000000..9f09ed56
--- /dev/null
+++ b/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/internal/UpperTypeScopePropagator.java
@@ -0,0 +1,58 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.reasoning.scope.internal;
+
+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;
+
+class UpperTypeScopePropagator extends TypeScopePropagator {
+        private final int upperBound;
+
+        private UpperTypeScopePropagator(ScopePropagatorAdapterImpl adapter, int upperBound, RelationalQuery allQuery,
+                                                                         RelationalQuery multiQuery) {
+                super(adapter, allQuery, multiQuery);
+                this.upperBound = upperBound;
+        }
+
+        @Override
+        public void updateBounds() {
+                constraint.setUb(upperBound - getSingleCount());
+        }
+
+        public static class Factory implements TypeScopePropagator.Factory {
+                private final int upperBound;
+                private final RelationalQuery allMust;
+                private final RelationalQuery multiMust;
+
+                public Factory(RelationalQuery multi, 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.call(instance)
+                        ));
+                }
+
+                @Override
+                public TypeScopePropagator createPropagator(ScopePropagatorAdapterImpl adapter) {
+                        return new UpperTypeScopePropagator(adapter, upperBound, allMust, multiMust);
+                }
+
+                @Override
+                public Collection<AnyQuery> getQueries() {
+                        return List.of(allMust, multiMust);
+                }
+        }
+}
diff --git a/subprojects/store-reasoning-scope/src/test/java/tools/refinery/store/reasoning/scope/MPSolverTest.java b/subprojects/store-reasoning-scope/src/test/java/tools/refinery/store/reasoning/scope/MPSolverTest.java
new file mode 100644
index 00000000..c9745d22
--- /dev/null
+++ b/subprojects/store-reasoning-scope/src/test/java/tools/refinery/store/reasoning/scope/MPSolverTest.java
@@ -0,0 +1,52 @@
+/*
+ * 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 com.google.ortools.linearsolver.MPSolver;
+import org.junit.jupiter.api.BeforeAll;
+import org.junit.jupiter.api.Test;
+
+import static org.hamcrest.MatcherAssert.assertThat;
+import static org.hamcrest.Matchers.closeTo;
+import static org.hamcrest.Matchers.is;
+
+class MPSolverTest {
+        @BeforeAll
+        static void beforeAll() {
+                Loader.loadNativeLibraries();
+        }
+
+        @Test
+        void updateProblemTest() {
+                var solver = MPSolver.createSolver("GLOP");
+                var x = solver.makeNumVar(0, Double.POSITIVE_INFINITY, "x");
+                var y = solver.makeNumVar(0, 1, "y");
+                var constraint = solver.makeConstraint(5, 5);
+                constraint.setCoefficient(x, 1);
+                constraint.setCoefficient(y, 1);
+                var objective = solver.objective();
+
+                objective.setCoefficient(x, 1);
+                objective.setMinimization();
+                assertThat(solver.solve(), is(MPSolver.ResultStatus.OPTIMAL));
+                assertThat(objective.value(), closeTo(4, 0.01));
+
+                objective.setMaximization();
+                assertThat(solver.solve(), is(MPSolver.ResultStatus.OPTIMAL));
+                assertThat(objective.value(), closeTo(5, 0.01));
+
+                objective.setCoefficient(x, 0);
+                objective.setCoefficient(y, 1);
+                objective.setMinimization();
+                assertThat(solver.solve(), is(MPSolver.ResultStatus.OPTIMAL));
+                assertThat(objective.value(), closeTo(0, 0.01));
+
+                objective.setMaximization();
+                assertThat(solver.solve(), is(MPSolver.ResultStatus.OPTIMAL));
+                assertThat(objective.value(), closeTo(1, 0.01));
+        }
+}
diff --git a/subprojects/store-reasoning-scope/src/test/java/tools/refinery/store/reasoning/scope/MultiObjectTest.java b/subprojects/store-reasoning-scope/src/test/java/tools/refinery/store/reasoning/scope/MultiObjectTest.java
new file mode 100644
index 00000000..42ce2f56
--- /dev/null
+++ b/subprojects/store-reasoning-scope/src/test/java/tools/refinery/store/reasoning/scope/MultiObjectTest.java
@@ -0,0 +1,206 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.reasoning.scope;
+
+import org.junit.jupiter.api.BeforeEach;
+import org.junit.jupiter.api.Test;
+import tools.refinery.store.model.Interpretation;
+import tools.refinery.store.model.Model;
+import tools.refinery.store.model.ModelStore;
+import tools.refinery.store.query.viatra.ViatraModelQueryAdapter;
+import tools.refinery.store.reasoning.ReasoningAdapter;
+import tools.refinery.store.reasoning.ReasoningStoreAdapter;
+import tools.refinery.store.reasoning.refinement.RefinementResult;
+import tools.refinery.store.reasoning.representation.PartialRelation;
+import tools.refinery.store.reasoning.seed.ModelSeed;
+import tools.refinery.store.reasoning.translator.PartialRelationTranslator;
+import tools.refinery.store.reasoning.translator.multiobject.MultiObjectTranslator;
+import tools.refinery.store.representation.Symbol;
+import tools.refinery.store.representation.TruthValue;
+import tools.refinery.store.representation.cardinality.CardinalityInterval;
+import tools.refinery.store.representation.cardinality.CardinalityIntervals;
+import tools.refinery.store.tuple.Tuple;
+
+import static org.hamcrest.MatcherAssert.assertThat;
+import static org.hamcrest.Matchers.is;
+
+class MultiObjectTest {
+        private static final PartialRelation person = new PartialRelation("Person", 1);
+
+        private ModelStore store;
+        private Model model;
+        private Interpretation<CardinalityInterval> countStorage;
+
+        @BeforeEach
+        void beforeEach() {
+                store = ModelStore.builder()
+                                .with(ViatraModelQueryAdapter.builder())
+                                .with(ReasoningAdapter.builder())
+                                .with(new MultiObjectTranslator())
+                                .with(PartialRelationTranslator.of(person)
+                                                .symbol(Symbol.of("Person", 1, TruthValue.class, TruthValue.FALSE)))
+                                .with(ScopePropagatorAdapter.builder()
+                                                .scope(person, CardinalityIntervals.between(5, 15)))
+                                .build();
+                model = null;
+                countStorage = null;
+        }
+
+        @Test
+        void oneMultiObjectSatisfiableTest() {
+                createModel(ModelSeed.builder(4)
+                                .seed(MultiObjectTranslator.COUNT_SYMBOL, builder -> builder
+                                                .reducedValue(CardinalityIntervals.ONE)
+                                                .put(Tuple.of(0), CardinalityIntervals.SET))
+                                .seed(person, builder -> builder.reducedValue(TruthValue.TRUE))
+                                .build());
+                assertThat(propagate(), is(RefinementResult.REFINED));
+                assertThat(countStorage.get(Tuple.of(0)), is(CardinalityIntervals.between(2, 12)));
+        }
+
+        @Test
+        void oneMultiObjectExistingBoundSatisfiableTest() {
+                createModel(ModelSeed.builder(4)
+                                .seed(MultiObjectTranslator.COUNT_SYMBOL, builder -> builder
+                                                .reducedValue(CardinalityIntervals.ONE)
+                                                .put(Tuple.of(0), CardinalityIntervals.between(5, 20)))
+                                .seed(person, builder -> builder.reducedValue(TruthValue.TRUE))
+                                .build());
+                assertThat(propagate(), is(RefinementResult.REFINED));
+                assertThat(countStorage.get(Tuple.of(0)), is(CardinalityIntervals.between(5, 12)));
+        }
+
+        @Test
+        void oneMultiObjectUnsatisfiableUpperTest() {
+                createModel(ModelSeed.builder(21)
+                                .seed(MultiObjectTranslator.COUNT_SYMBOL, builder -> builder
+                                                .reducedValue(CardinalityIntervals.ONE)
+                                                .put(Tuple.of(0), CardinalityIntervals.SET))
+                                .seed(person, builder -> builder.reducedValue(TruthValue.TRUE))
+                                .build());
+                assertThat(propagate(), is(RefinementResult.REJECTED));
+        }
+
+        @Test
+        void noMultiObjectSatisfiableTest() {
+                createModel(ModelSeed.builder(10)
+                                .seed(MultiObjectTranslator.COUNT_SYMBOL, builder -> builder.reducedValue(CardinalityIntervals.ONE))
+                                .seed(person, builder -> builder.reducedValue(TruthValue.TRUE))
+                                .build());
+                assertThat(propagate(), is(RefinementResult.UNCHANGED));
+        }
+
+        @Test
+        void noMultiObjectUnsatisfiableTest() {
+                createModel(ModelSeed.builder(2)
+                                .seed(MultiObjectTranslator.COUNT_SYMBOL, builder -> builder.reducedValue(CardinalityIntervals.ONE))
+                                .seed(person, builder -> builder.reducedValue(TruthValue.TRUE))
+                                .build());
+                assertThat(propagate(), is(RefinementResult.REJECTED));
+        }
+
+        @Test
+        void oneMultiObjectExistingBoundUnsatisfiableLowerTest() {
+                createModel(ModelSeed.builder(4)
+                                .seed(MultiObjectTranslator.COUNT_SYMBOL, builder -> builder
+                                                .reducedValue(CardinalityIntervals.ONE)
+                                                .put(Tuple.of(0), CardinalityIntervals.atLeast(20)))
+                                .seed(person, builder -> builder.reducedValue(TruthValue.TRUE))
+                                .build());
+                assertThat(propagate(), is(RefinementResult.REJECTED));
+        }
+
+        @Test
+        void oneMultiObjectExistingBoundUnsatisfiableUpperTest() {
+                createModel(ModelSeed.builder(4)
+                                .seed(MultiObjectTranslator.COUNT_SYMBOL, builder -> builder
+                                                .reducedValue(CardinalityIntervals.ONE)
+                                                .put(Tuple.of(0), CardinalityIntervals.atMost(1)))
+                                .seed(person, builder -> builder.reducedValue(TruthValue.TRUE))
+                                .build());
+                assertThat(propagate(), is(RefinementResult.REJECTED));
+        }
+
+        @Test
+        void twoMultiObjectsSatisfiableTest() {
+                createModel(ModelSeed.builder(5)
+                                .seed(MultiObjectTranslator.COUNT_SYMBOL, builder -> builder
+                                                .reducedValue(CardinalityIntervals.ONE)
+                                                .put(Tuple.of(0), CardinalityIntervals.SET)
+                                                .put(Tuple.of(1), CardinalityIntervals.SET))
+                                .seed(person, builder -> builder.reducedValue(TruthValue.TRUE))
+                                .build());
+                assertThat(propagate(), is(RefinementResult.REFINED));
+                assertThat(countStorage.get(Tuple.of(0)), is(CardinalityIntervals.atMost(12)));
+                assertThat(countStorage.get(Tuple.of(1)), is(CardinalityIntervals.atMost(12)));
+        }
+
+        @Test
+        void twoMultiObjectsExistingBoundSatisfiableTest() {
+                createModel(ModelSeed.builder(5)
+                                .seed(MultiObjectTranslator.COUNT_SYMBOL, builder -> builder
+                                                .reducedValue(CardinalityIntervals.ONE)
+                                                .put(Tuple.of(0), CardinalityIntervals.between(7, 20))
+                                                .put(Tuple.of(1), CardinalityIntervals.atMost(11)))
+                                .seed(person, builder -> builder.reducedValue(TruthValue.TRUE))
+                                .build());
+                assertThat(propagate(), is(RefinementResult.REFINED));
+                assertThat(countStorage.get(Tuple.of(0)), is(CardinalityIntervals.between(7, 12)));
+                assertThat(countStorage.get(Tuple.of(1)), is(CardinalityIntervals.atMost(5)));
+        }
+
+        @Test
+        void twoMultiObjectsExistingBoundUnsatisfiableUpperTest() {
+                createModel(ModelSeed.builder(5)
+                                .seed(MultiObjectTranslator.COUNT_SYMBOL, builder -> builder
+                                                .reducedValue(CardinalityIntervals.ONE)
+                                                .put(Tuple.of(0), CardinalityIntervals.between(7, 20))
+                                                .put(Tuple.of(1), CardinalityIntervals.exactly(11)))
+                                .seed(person, builder -> builder.reducedValue(TruthValue.TRUE))
+                                .build());
+                assertThat(propagate(), is(RefinementResult.REJECTED));
+        }
+
+        @Test
+        void twoMultiObjectsExistingBoundUnsatisfiableLowerTest() {
+                createModel(ModelSeed.builder(3)
+                                .seed(MultiObjectTranslator.COUNT_SYMBOL, builder -> builder
+                                                .reducedValue(CardinalityIntervals.ONE)
+                                                .put(Tuple.of(0), CardinalityIntervals.LONE)
+                                                .put(Tuple.of(1), CardinalityIntervals.atMost(2)))
+                                .seed(person, builder -> builder.reducedValue(TruthValue.TRUE))
+                                .build());
+                assertThat(propagate(), is(RefinementResult.REJECTED));
+        }
+
+        @Test
+        void multiToSingleTest() {
+                createModel(ModelSeed.builder(5)
+                                .seed(MultiObjectTranslator.COUNT_SYMBOL, builder -> builder
+                                                .reducedValue(CardinalityIntervals.ONE)
+                                                .put(Tuple.of(0), CardinalityIntervals.LONE)
+                                                .put(Tuple.of(1), CardinalityIntervals.SET))
+                                .seed(person, builder -> builder.reducedValue(TruthValue.TRUE))
+                                .build());
+                assertThat(propagate(), is(RefinementResult.REFINED));
+                assertThat(countStorage.get(Tuple.of(0)), is(CardinalityIntervals.LONE));
+                assertThat(countStorage.get(Tuple.of(1)), is(CardinalityIntervals.between(1, 12)));
+                countStorage.put(Tuple.of(0), CardinalityIntervals.ONE);
+                assertThat(propagate(), is(RefinementResult.REFINED));
+                assertThat(countStorage.get(Tuple.of(1)), is(CardinalityIntervals.between(1, 11)));
+                countStorage.put(Tuple.of(1), CardinalityIntervals.ONE);
+                assertThat(propagate(), is(RefinementResult.UNCHANGED));
+        }
+
+        private void createModel(ModelSeed modelSeed) {
+                model = store.getAdapter(ReasoningStoreAdapter.class).createInitialModel(modelSeed);
+                countStorage = model.getInterpretation(MultiObjectTranslator.COUNT_STORAGE);
+        }
+
+        private RefinementResult propagate() {
+                return model.getAdapter(ScopePropagatorAdapter.class).propagate();
+        }
+}
diff --git a/subprojects/store-reasoning-scope/src/test/java/tools/refinery/store/reasoning/scope/internal/RoundingUtilTest.java b/subprojects/store-reasoning-scope/src/test/java/tools/refinery/store/reasoning/scope/internal/RoundingUtilTest.java
new file mode 100644
index 00000000..9daed660
--- /dev/null
+++ b/subprojects/store-reasoning-scope/src/test/java/tools/refinery/store/reasoning/scope/internal/RoundingUtilTest.java
@@ -0,0 +1,69 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.reasoning.scope.internal;
+
+import org.junit.jupiter.params.ParameterizedTest;
+import org.junit.jupiter.params.provider.Arguments;
+import org.junit.jupiter.params.provider.MethodSource;
+
+import java.util.stream.Stream;
+
+import static org.hamcrest.MatcherAssert.assertThat;
+import static org.hamcrest.Matchers.is;
+
+class RoundingUtilTest {
+        @ParameterizedTest
+        @MethodSource
+        void roundUpTest(double value, int expected) {
+                int actual = RoundingUtil.roundUp(value);
+                assertThat(actual, is(expected));
+        }
+
+        static Stream<Arguments> roundUpTest() {
+                return Stream.of(
+                                Arguments.of(0.0, 0),
+                                Arguments.of(-0.0, 0),
+                                Arguments.of(-0.9, 0),
+                                Arguments.of(-2, 0),
+                                Arguments.of(0.009, 0),
+                                Arguments.of(0.011, 1),
+                                Arguments.of(0.1, 1),
+                                Arguments.of(0.991, 1),
+                                Arguments.of(1, 1),
+                                Arguments.of(1.009, 1),
+                                Arguments.of(1.011, 2),
+                                Arguments.of(1.5, 2),
+                                Arguments.of(2, 2),
+                                Arguments.of(100.5, 101)
+                );
+        }
+
+        @ParameterizedTest
+        @MethodSource
+        void roundDownTest(double value, int expected) {
+                int actual = RoundingUtil.roundDown(value);
+                assertThat(actual, is(expected));
+        }
+
+        static Stream<Arguments> roundDownTest() {
+                return Stream.of(
+                                Arguments.of(0.0, 0),
+                                Arguments.of(-0.0, 0),
+                                Arguments.of(-0.9, 0),
+                                Arguments.of(-2, 0),
+                                Arguments.of(0.989, 0),
+                                Arguments.of(0.991, 1),
+                                Arguments.of(1, 1),
+                                Arguments.of(1.5, 1),
+                                Arguments.of(1.009, 1),
+                                Arguments.of(1.989, 1),
+                                Arguments.of(1.991, 2),
+                                Arguments.of(2, 2),
+                                Arguments.of(2.009, 2),
+                                Arguments.of(100.5, 100)
+                );
+        }
+}
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/refinement/RefinementResult.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/refinement/RefinementResult.java
new file mode 100644
index 00000000..1bc537d1
--- /dev/null
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/refinement/RefinementResult.java
@@ -0,0 +1,24 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.reasoning.refinement;
+
+public enum RefinementResult {
+        UNCHANGED,
+        REFINED,
+        REJECTED;
+
+        public RefinementResult andThen(RefinementResult next) {
+                return switch (this) {
+                        case UNCHANGED -> next;
+                        case REFINED -> next == REJECTED ? REJECTED : REFINED;
+                        case REJECTED -> REJECTED;
+                };
+        }
+
+        public boolean isRejected() {
+                return this == REJECTED;
+        }
+}
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 c62557d7..735896fa 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
@@ -29,7 +29,7 @@ import static tools.refinery.store.query.term.uppercardinality.UpperCardinalityT
 import static tools.refinery.store.query.term.uppercardinality.UpperCardinalityTerms.greaterEq;
 
 public class MultiObjectTranslator implements ModelStoreConfiguration {
-        private static final Symbol<CardinalityInterval> COUNT_STORAGE = Symbol.of("COUNT", 1, CardinalityInterval.class,
+        public static final Symbol<CardinalityInterval> COUNT_STORAGE = Symbol.of("COUNT", 1, CardinalityInterval.class,
                         null);
         public static final AnySymbolView LOWER_CARDINALITY_VIEW = new LowerCardinalityView(COUNT_STORAGE);
         public static final AnySymbolView UPPER_CARDINALITY_VIEW = new UpperCardinalityView(COUNT_STORAGE);