Merge pull request #39 from kris7t/partial-interpretation

Implement partial interpretation based model generation

9 files changed, 559 insertions, 0 deletions

diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiobject/EqualsRefiner.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiobject/EqualsRefiner.java
new file mode 100644
index 00000000..d8db4ec4
--- /dev/null
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiobject/EqualsRefiner.java
@@ -0,0 +1,64 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.reasoning.translator.multiobject;
+
+import tools.refinery.store.model.Interpretation;
+import tools.refinery.store.reasoning.ReasoningAdapter;
+import tools.refinery.store.reasoning.refinement.AbstractPartialInterpretationRefiner;
+import tools.refinery.store.reasoning.representation.PartialSymbol;
+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;
+
+public class EqualsRefiner extends AbstractPartialInterpretationRefiner<TruthValue, Boolean> {
+        private final Interpretation<CardinalityInterval> countInterpretation;
+
+        private EqualsRefiner(ReasoningAdapter adapter, PartialSymbol<TruthValue, Boolean> partialSymbol,
+                          Symbol<CardinalityInterval> countSymbol) {
+                super(adapter, partialSymbol);
+                countInterpretation = adapter.getModel().getInterpretation(countSymbol);
+        }
+
+        @Override
+        public boolean merge(Tuple key, TruthValue value) {
+                if (value == TruthValue.UNKNOWN) {
+                        return true;
+                }
+                if (value == TruthValue.ERROR) {
+                        return false;
+                }
+                int left = key.get(0);
+                int right = key.get(1);
+                boolean isDiagonal = left == right;
+                if (isDiagonal && value == TruthValue.FALSE) {
+                        return false;
+                }
+                if (!isDiagonal) {
+                        return !value.may();
+                }
+                if (value != TruthValue.TRUE) {
+                        throw new IllegalArgumentException("Unknown TruthValue: " + value);
+                }
+                // {@code isDiagonal} is true, so this could be {@code left} or {@code right}.
+                var unaryKey = Tuple.of(left);
+                var currentCount = countInterpretation.get(unaryKey);
+                if (currentCount == null) {
+                        return false;
+                }
+                var newCount = currentCount.meet(CardinalityIntervals.LONE);
+                if (newCount.isEmpty()) {
+                        return false;
+                }
+                countInterpretation.put(unaryKey, newCount);
+                return true;
+        }
+
+        public static Factory<TruthValue, Boolean> of(Symbol<CardinalityInterval> countSymbol) {
+                return (adapter, partialSymbol) -> new EqualsRefiner(adapter, partialSymbol, countSymbol);
+        }
+}
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiobject/EqualsRelationRewriter.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiobject/EqualsRelationRewriter.java
new file mode 100644
index 00000000..61b9488c
--- /dev/null
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiobject/EqualsRelationRewriter.java
@@ -0,0 +1,85 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.reasoning.translator.multiobject;
+
+import tools.refinery.store.query.dnf.Query;
+import tools.refinery.store.query.dnf.RelationalQuery;
+import tools.refinery.store.query.literal.AbstractCallLiteral;
+import tools.refinery.store.query.literal.CallLiteral;
+import tools.refinery.store.query.literal.Literal;
+import tools.refinery.store.query.term.Variable;
+import tools.refinery.store.query.view.AnySymbolView;
+import tools.refinery.store.reasoning.interpretation.QueryBasedRelationRewriter;
+import tools.refinery.store.reasoning.literal.Concreteness;
+import tools.refinery.store.reasoning.literal.Modality;
+import tools.refinery.store.representation.cardinality.UpperCardinalities;
+import tools.refinery.store.representation.cardinality.UpperCardinality;
+
+import java.util.List;
+import java.util.Set;
+
+import static tools.refinery.store.query.literal.Literals.check;
+import static tools.refinery.store.query.term.uppercardinality.UpperCardinalityTerms.constant;
+import static tools.refinery.store.query.term.uppercardinality.UpperCardinalityTerms.lessEq;
+
+class EqualsRelationRewriter extends QueryBasedRelationRewriter {
+        private EqualsRelationRewriter(RelationalQuery may, RelationalQuery must) {
+                super(may, must, may, may);
+        }
+
+        @Override
+        public List<Literal> rewriteLiteral(Set<Variable> positiveVariables, AbstractCallLiteral literal,
+                                                                                Modality modality, Concreteness concreteness) {
+                if (!(literal instanceof CallLiteral callLiteral)) {
+                        return super.rewriteLiteral(positiveVariables, literal, modality, concreteness);
+                }
+                var left = callLiteral.getArguments().get(0).asNodeVariable();
+                var right = callLiteral.getArguments().get(1).asNodeVariable();
+                boolean useMay = modality == Modality.MAY || concreteness == Concreteness.CANDIDATE;
+                return switch (callLiteral.getPolarity()) {
+                        case POSITIVE, TRANSITIVE -> {
+                                if (useMay) {
+                                        if (positiveVariables.contains(left) || positiveVariables.contains(right)) {
+                                                // No need to enumerate arguments if at least one is already bound, since they will be unified.
+                                                yield List.of(left.isEquivalent(right));
+                                        } else {
+                                                yield List.of(
+                                                                left.isEquivalent(right),
+                                                                getMay().call(left, right)
+                                                );
+                                        }
+                                } else {
+                                        yield List.of(
+                                                        left.isEquivalent(right),
+                                                        getMust().call(left, right)
+                                        );
+                                }
+                        }
+                        case NEGATIVE -> {
+                                if (useMay) {
+                                        yield List.of(left.notEquivalent(right));
+                                } else {
+                                        yield super.rewriteLiteral(positiveVariables, literal, modality, concreteness);
+                                }
+                        }
+                };
+        }
+
+        public static EqualsRelationRewriter of(AnySymbolView upperCardinalityView) {
+                var may = Query.of("equals#may", (builder, p1, p2) -> builder
+                                .clause(
+                                                p1.isEquivalent(p2),
+                                                upperCardinalityView.call(p1, Variable.of(UpperCardinality.class))
+                                ));
+                var must = Query.of("equals#must", (builder, p1, p2) -> builder
+                                .clause(UpperCardinality.class, upper -> List.of(
+                                                p1.isEquivalent(p2),
+                                                upperCardinalityView.call(p1, upper),
+                                                check(lessEq(upper, constant(UpperCardinalities.ONE)))
+                                )));
+                return new EqualsRelationRewriter(may, must);
+        }
+}
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiobject/ExistsRefiner.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiobject/ExistsRefiner.java
new file mode 100644
index 00000000..f134fe92
--- /dev/null
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiobject/ExistsRefiner.java
@@ -0,0 +1,55 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.reasoning.translator.multiobject;
+
+import tools.refinery.store.model.Interpretation;
+import tools.refinery.store.reasoning.ReasoningAdapter;
+import tools.refinery.store.reasoning.refinement.AbstractPartialInterpretationRefiner;
+import tools.refinery.store.reasoning.representation.PartialSymbol;
+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;
+
+public class ExistsRefiner extends AbstractPartialInterpretationRefiner<TruthValue, Boolean> {
+        private final Interpretation<CardinalityInterval> countInterpretation;
+
+        private ExistsRefiner(ReasoningAdapter adapter, PartialSymbol<TruthValue, Boolean> partialSymbol,
+                                                   Symbol<CardinalityInterval> countSymbol) {
+                super(adapter, partialSymbol);
+                countInterpretation = adapter.getModel().getInterpretation(countSymbol);
+        }
+
+        @Override
+        public boolean merge(Tuple key, TruthValue value) {
+                var currentCount = countInterpretation.get(key);
+                if (currentCount == null) {
+                        return false;
+                }
+                CardinalityInterval newCount;
+                switch (value) {
+                case UNKNOWN -> {
+                        return true;
+                }
+                case TRUE -> newCount = currentCount.meet(CardinalityIntervals.SOME);
+                case FALSE -> newCount = currentCount.meet(CardinalityIntervals.NONE);
+                case ERROR -> {
+                        return false;
+                }
+                default -> throw new IllegalArgumentException("Unknown TruthValue: " + value);
+                }
+                if (newCount.isEmpty()) {
+                        return false;
+                }
+                countInterpretation.put(key, newCount);
+                return true;
+        }
+
+        public static Factory<TruthValue, Boolean> of(Symbol<CardinalityInterval> countSymbol) {
+                return (adapter, partialSymbol) -> new ExistsRefiner(adapter, partialSymbol, countSymbol);
+        }
+}
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiobject/LowerCardinalityView.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiobject/LowerCardinalityView.java
new file mode 100644
index 00000000..9873888c
--- /dev/null
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiobject/LowerCardinalityView.java
@@ -0,0 +1,22 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.reasoning.translator.multiobject;
+
+import tools.refinery.store.query.term.Parameter;
+import tools.refinery.store.query.view.AbstractFunctionView;
+import tools.refinery.store.representation.Symbol;
+import tools.refinery.store.representation.cardinality.CardinalityInterval;
+
+class LowerCardinalityView extends AbstractFunctionView<CardinalityInterval> {
+        public LowerCardinalityView(Symbol<CardinalityInterval> symbol) {
+                super(symbol, "lower", new Parameter(Integer.class));
+        }
+
+        @Override
+        protected Object forwardMapValue(CardinalityInterval value) {
+                return value.lowerBound();
+        }
+}
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiobject/MultiObjectInitializer.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiobject/MultiObjectInitializer.java
new file mode 100644
index 00000000..89918155
--- /dev/null
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiobject/MultiObjectInitializer.java
@@ -0,0 +1,135 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.reasoning.translator.multiobject;
+
+import org.jetbrains.annotations.NotNull;
+import tools.refinery.store.model.Model;
+import tools.refinery.store.reasoning.ReasoningAdapter;
+import tools.refinery.store.reasoning.refinement.PartialModelInitializer;
+import tools.refinery.store.reasoning.seed.ModelSeed;
+import tools.refinery.store.reasoning.translator.TranslationException;
+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 java.util.Arrays;
+import java.util.HashMap;
+import java.util.function.Function;
+
+class MultiObjectInitializer implements PartialModelInitializer {
+        private final Symbol<CardinalityInterval> countSymbol;
+
+        public MultiObjectInitializer(Symbol<CardinalityInterval> countSymbol) {
+                this.countSymbol = countSymbol;
+        }
+
+        @Override
+        public void initialize(Model model, ModelSeed modelSeed) {
+                var intervals = initializeIntervals(model, modelSeed);
+                initializeExists(intervals, model, modelSeed);
+                initializeEquals(intervals, model, modelSeed);
+                var countInterpretation = model.getInterpretation(countSymbol);
+                var uniqueTable = new HashMap<CardinalityInterval, CardinalityInterval>();
+                for (int i = 0; i < intervals.length; i++) {
+                        var interval = intervals[i];
+                        if (interval.isEmpty()) {
+                                throw new TranslationException(ReasoningAdapter.EXISTS_SYMBOL,
+                                                "Inconsistent existence or equality for node " + i);
+                        }
+                        var uniqueInterval = uniqueTable.computeIfAbsent(intervals[i], Function.identity());
+                        countInterpretation.put(Tuple.of(i), uniqueInterval);
+                }
+        }
+
+        @NotNull
+        private CardinalityInterval[] initializeIntervals(Model model, ModelSeed modelSeed) {
+                var intervals = new CardinalityInterval[modelSeed.getNodeCount()];
+                if (modelSeed.containsSeed(MultiObjectTranslator.COUNT_SYMBOL)) {
+                        Arrays.fill(intervals, CardinalityIntervals.ONE);
+                        var cursor = modelSeed.getCursor(MultiObjectTranslator.COUNT_SYMBOL, CardinalityIntervals.ONE);
+                        while (cursor.move()) {
+                                model.checkCancelled();
+                                int i = cursor.getKey().get(0);
+                                checkNodeId(intervals, i);
+                                intervals[i] = cursor.getValue();
+                        }
+                } else {
+                        Arrays.fill(intervals, CardinalityIntervals.SET);
+                        if (!modelSeed.containsSeed(ReasoningAdapter.EXISTS_SYMBOL) ||
+                                        !modelSeed.containsSeed(ReasoningAdapter.EQUALS_SYMBOL)) {
+                                throw new TranslationException(MultiObjectTranslator.COUNT_SYMBOL,
+                                                "Seed for %s and %s is required if there is no seed for %s".formatted(
+                                                                ReasoningAdapter.EXISTS_SYMBOL, ReasoningAdapter.EQUALS_SYMBOL,
+                                                                MultiObjectTranslator.COUNT_SYMBOL));
+                        }
+                }
+                return intervals;
+        }
+
+        private void initializeExists(CardinalityInterval[] intervals, Model model, ModelSeed modelSeed) {
+                if (!modelSeed.containsSeed(ReasoningAdapter.EXISTS_SYMBOL)) {
+                        return;
+                }
+                var cursor = modelSeed.getCursor(ReasoningAdapter.EXISTS_SYMBOL, TruthValue.UNKNOWN);
+                while (cursor.move()) {
+                        model.checkCancelled();
+                        int i = cursor.getKey().get(0);
+                        checkNodeId(intervals, i);
+                        switch (cursor.getValue()) {
+                        case TRUE -> intervals[i] = intervals[i].meet(CardinalityIntervals.SOME);
+                        case FALSE -> intervals[i] = intervals[i].meet(CardinalityIntervals.NONE);
+                        case ERROR -> throw new TranslationException(ReasoningAdapter.EXISTS_SYMBOL,
+                                        "Inconsistent existence for node " + i);
+                        default -> throw new TranslationException(ReasoningAdapter.EXISTS_SYMBOL,
+                                        "Invalid existence truth value %s for node %d".formatted(cursor.getValue(), i));
+                        }
+                }
+        }
+
+        private void initializeEquals(CardinalityInterval[] intervals, Model model, ModelSeed modelSeed) {
+                if (!modelSeed.containsSeed(ReasoningAdapter.EQUALS_SYMBOL)) {
+                        return;
+                }
+                var seed = modelSeed.getSeed(ReasoningAdapter.EQUALS_SYMBOL);
+                var cursor = seed.getCursor(TruthValue.FALSE, modelSeed.getNodeCount());
+                while (cursor.move()) {
+                        model.checkCancelled();
+                        var key = cursor.getKey();
+                        int i = key.get(0);
+                        int otherIndex = key.get(1);
+                        if (i != otherIndex) {
+                                throw new TranslationException(ReasoningAdapter.EQUALS_SYMBOL,
+                                                "Off-diagonal equivalence (%d, %d) is not permitted".formatted(i, otherIndex));
+                        }
+                        checkNodeId(intervals, i);
+                        switch (cursor.getValue()) {
+                        case TRUE -> intervals[i] = intervals[i].meet(CardinalityIntervals.LONE);
+                        case UNKNOWN -> {
+                                // Nothing do to, {@code intervals} is initialized with unknown equality.
+                        }
+                        case ERROR -> throw new TranslationException(ReasoningAdapter.EQUALS_SYMBOL,
+                                        "Inconsistent equality for node " + i);
+                        default -> throw new TranslationException(ReasoningAdapter.EQUALS_SYMBOL,
+                                        "Invalid equality truth value %s for node %d".formatted(cursor.getValue(), i));
+                        }
+                }
+                for (int i = 0; i < intervals.length; i++) {
+                        model.checkCancelled();
+                        if (seed.get(Tuple.of(i, i)) == TruthValue.FALSE) {
+                                throw new TranslationException(ReasoningAdapter.EQUALS_SYMBOL, "Inconsistent equality for node " + i);
+                        }
+                }
+        }
+
+        private void checkNodeId(CardinalityInterval[] intervals, int nodeId) {
+                if (nodeId < 0 || nodeId >= intervals.length) {
+                        throw new IllegalArgumentException("Expected node id %d to be lower than model size %d"
+                                        .formatted(nodeId, intervals.length));
+                }
+        }
+}
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiobject/MultiObjectStorageRefiner.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiobject/MultiObjectStorageRefiner.java
new file mode 100644
index 00000000..e48934d8
--- /dev/null
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiobject/MultiObjectStorageRefiner.java
@@ -0,0 +1,45 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.reasoning.translator.multiobject;
+
+import tools.refinery.store.model.Interpretation;
+import tools.refinery.store.model.Model;
+import tools.refinery.store.reasoning.refinement.StorageRefiner;
+import tools.refinery.store.representation.Symbol;
+import tools.refinery.store.representation.cardinality.CardinalityInterval;
+import tools.refinery.store.representation.cardinality.CardinalityIntervals;
+import tools.refinery.store.tuple.Tuple;
+
+class MultiObjectStorageRefiner implements StorageRefiner {
+        private final Interpretation<CardinalityInterval> countInterpretation;
+
+        public MultiObjectStorageRefiner(Symbol<CardinalityInterval> countSymbol, Model model) {
+                countInterpretation = model.getInterpretation(countSymbol);
+        }
+
+        @Override
+        public boolean split(int parentNode, int childNode) {
+                var parentKey = Tuple.of(parentNode);
+                var parentCount = countInterpretation.get(parentKey);
+                if (parentCount == null) {
+                        return false;
+                }
+                var newParentCount = parentCount.take(1);
+                if (newParentCount.isEmpty()) {
+                        return false;
+                }
+                var childKey = Tuple.of(childNode);
+                countInterpretation.put(parentKey, newParentCount);
+                countInterpretation.put(childKey, CardinalityIntervals.ONE);
+                return true;
+        }
+
+        @Override
+        public boolean cleanup(int nodeToDelete) {
+                var previousCount = countInterpretation.put(Tuple.of(nodeToDelete), null);
+                return previousCount.lowerBound() == 0;
+        }
+}
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
new file mode 100644
index 00000000..97fda9d5
--- /dev/null
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiobject/MultiObjectTranslator.java
@@ -0,0 +1,107 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.reasoning.translator.multiobject;
+
+import tools.refinery.store.dse.propagation.PropagationBuilder;
+import tools.refinery.store.dse.transition.Rule;
+import tools.refinery.store.dse.transition.objectives.Criteria;
+import tools.refinery.store.dse.transition.objectives.Objectives;
+import tools.refinery.store.model.ModelStoreBuilder;
+import tools.refinery.store.model.ModelStoreConfiguration;
+import tools.refinery.store.query.dnf.Query;
+import tools.refinery.store.query.literal.Literals;
+import tools.refinery.store.query.term.Variable;
+import tools.refinery.store.query.term.int_.IntTerms;
+import tools.refinery.store.query.term.uppercardinality.UpperCardinalityTerms;
+import tools.refinery.store.query.view.AnySymbolView;
+import tools.refinery.store.reasoning.ReasoningAdapter;
+import tools.refinery.store.reasoning.ReasoningBuilder;
+import tools.refinery.store.reasoning.actions.PartialActionLiterals;
+import tools.refinery.store.reasoning.representation.PartialFunction;
+import tools.refinery.store.reasoning.translator.PartialRelationTranslator;
+import tools.refinery.store.reasoning.translator.RoundingMode;
+import tools.refinery.store.representation.Symbol;
+import tools.refinery.store.representation.cardinality.CardinalityDomain;
+import tools.refinery.store.representation.cardinality.CardinalityInterval;
+import tools.refinery.store.representation.cardinality.UpperCardinalities;
+import tools.refinery.store.representation.cardinality.UpperCardinality;
+
+import java.util.List;
+
+import static tools.refinery.store.query.literal.Literals.check;
+import static tools.refinery.store.query.term.int_.IntTerms.*;
+
+public class MultiObjectTranslator implements ModelStoreConfiguration {
+        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);
+        public static final AnySymbolView MULTI_VIEW = new MultiView(COUNT_STORAGE);
+        public static final PartialFunction<CardinalityInterval, Integer> COUNT_SYMBOL = new PartialFunction<>("COUNT", 1,
+                        CardinalityDomain.INSTANCE);
+
+        @Override
+        public void apply(ModelStoreBuilder storeBuilder) {
+                storeBuilder.symbol(COUNT_STORAGE);
+
+                var aboveLowerBound = Query.of("count#aboveLowerBound", Integer.class, (builder, node, output) -> builder
+                                .clause(
+                                                MULTI_VIEW.call(node),
+                                                LOWER_CARDINALITY_VIEW.call(node, output),
+                                                check(greater(output, IntTerms.constant(0)))
+                                ));
+                var missingCardinality = Query.of("count#missing", Integer.class, (builder, output) -> builder
+                                .clause(
+                                                output.assign(aboveLowerBound.aggregate(INT_SUM, Variable.of()))
+                                ));
+
+                storeBuilder.with(PartialRelationTranslator.of(ReasoningAdapter.EXISTS_SYMBOL)
+                                .may(Query.of("exists#may", (builder, p1) -> builder
+                                                .clause(UpperCardinality.class, upper -> List.of(
+                                                                UPPER_CARDINALITY_VIEW.call(p1, upper),
+                                                                check(UpperCardinalityTerms.greaterEq(upper,
+                                                                                UpperCardinalityTerms.constant(UpperCardinalities.ONE)))
+                                                ))))
+                                .must(Query.of("exists#must", (builder, p1) -> builder
+                                                .clause(Integer.class, lower -> List.of(
+                                                                LOWER_CARDINALITY_VIEW.call(p1, lower),
+                                                                check(greaterEq(lower, constant(1)))
+                                                ))))
+                                .candidate(Query.of("exists#candidate", (builder, p1) -> builder
+                                                .clause(
+                                                                LOWER_CARDINALITY_VIEW.call(p1, Variable.of(Integer.class)),
+                                                                Literals.not(MULTI_VIEW.call(p1))
+                                                )))
+                                .roundingMode(RoundingMode.PREFER_FALSE)
+                                .refiner(ExistsRefiner.of(COUNT_STORAGE))
+                                .exclude(null)
+                                .accept(Criteria.whenNoMatch(aboveLowerBound))
+                                .objective(Objectives.value(missingCardinality)));
+
+                storeBuilder.with(PartialRelationTranslator.of(ReasoningAdapter.EQUALS_SYMBOL)
+                                .rewriter(EqualsRelationRewriter.of(UPPER_CARDINALITY_VIEW))
+                                .refiner(EqualsRefiner.of(COUNT_STORAGE))
+                                .exclude(null)
+                                .accept(null)
+                                .objective(null));
+
+                var reasoningBuilder = storeBuilder.getAdapter(ReasoningBuilder.class);
+                reasoningBuilder.initializer(new MultiObjectInitializer(COUNT_STORAGE));
+                reasoningBuilder.storageRefiner(COUNT_STORAGE, MultiObjectStorageRefiner::new);
+
+                storeBuilder.tryGetAdapter(PropagationBuilder.class)
+                                .ifPresent(propagationBuilder -> propagationBuilder.rule(
+                                                Rule.of("exists#cleanup", (builder, node) -> builder
+                                                                .clause(UpperCardinality.class, upper -> List.of(
+                                                                                UPPER_CARDINALITY_VIEW.call(node, upper),
+                                                                                check(UpperCardinalityTerms.less(upper,
+                                                                                                UpperCardinalityTerms.constant(UpperCardinalities.ONE)))
+                                                                ))
+                                                                .action(
+                                                                                PartialActionLiterals.cleanup(node)
+                                                                ))));
+        }
+}
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiobject/MultiView.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiobject/MultiView.java
new file mode 100644
index 00000000..498bcd83
--- /dev/null
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiobject/MultiView.java
@@ -0,0 +1,23 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.reasoning.translator.multiobject;
+
+import tools.refinery.store.query.view.TuplePreservingView;
+import tools.refinery.store.representation.Symbol;
+import tools.refinery.store.representation.cardinality.CardinalityInterval;
+import tools.refinery.store.representation.cardinality.CardinalityIntervals;
+import tools.refinery.store.tuple.Tuple;
+
+class MultiView extends TuplePreservingView<CardinalityInterval> {
+        protected MultiView(Symbol<CardinalityInterval> symbol) {
+                super(symbol, "multi");
+        }
+
+        @Override
+        protected boolean doFilter(Tuple key, CardinalityInterval value) {
+                return !CardinalityIntervals.ONE.equals(value);
+        }
+}
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiobject/UpperCardinalityView.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiobject/UpperCardinalityView.java
new file mode 100644
index 00000000..6be6ae1b
--- /dev/null
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiobject/UpperCardinalityView.java
@@ -0,0 +1,23 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.reasoning.translator.multiobject;
+
+import tools.refinery.store.query.term.Parameter;
+import tools.refinery.store.query.view.AbstractFunctionView;
+import tools.refinery.store.representation.Symbol;
+import tools.refinery.store.representation.cardinality.CardinalityInterval;
+import tools.refinery.store.representation.cardinality.UpperCardinality;
+
+class UpperCardinalityView extends AbstractFunctionView<CardinalityInterval> {
+        public UpperCardinalityView(Symbol<CardinalityInterval> symbol) {
+                super(symbol, "upper", new Parameter(UpperCardinality.class));
+        }
+
+        @Override
+        protected Object forwardMapValue(CardinalityInterval value) {
+                return value.upperBound();
+        }
+}