feat: concrete count in partial models

19 files changed, 807 insertions, 98 deletions

diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/AbstractCountLiteral.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/AbstractCountLiteral.java
new file mode 100644
index 00000000..75f4bd49
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/AbstractCountLiteral.java
@@ -0,0 +1,106 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.query.literal;
+
+import tools.refinery.store.query.Constraint;
+import tools.refinery.store.query.equality.LiteralEqualityHelper;
+import tools.refinery.store.query.equality.LiteralHashCodeHelper;
+import tools.refinery.store.query.term.ConstantTerm;
+import tools.refinery.store.query.term.DataVariable;
+import tools.refinery.store.query.term.Variable;
+
+import java.util.List;
+import java.util.Objects;
+import java.util.Set;
+
+// {@link Object#equals(Object)} is implemented by {@link AbstractLiteral}.
+@SuppressWarnings("squid:S2160")
+public abstract class AbstractCountLiteral<T> extends AbstractCallLiteral {
+        private final Class<T> resultType;
+        private final DataVariable<T> resultVariable;
+
+        protected AbstractCountLiteral(Class<T> resultType, DataVariable<T> resultVariable, Constraint target,
+                                                                   List<Variable> arguments) {
+                super(target, arguments);
+                if (!resultVariable.getType().equals(resultType)) {
+                        throw new IllegalArgumentException("Count result variable %s must be of type %s, got %s instead".formatted(
+                                        resultVariable, resultType, resultVariable.getType().getName()));
+                }
+                if (arguments.contains(resultVariable)) {
+                        throw new IllegalArgumentException("Count result variable %s must not appear in the argument list"
+                                        .formatted(resultVariable));
+                }
+                this.resultType = resultType;
+                this.resultVariable = resultVariable;
+        }
+
+        public Class<T> getResultType() {
+                return resultType;
+        }
+
+        public DataVariable<T> getResultVariable() {
+                return resultVariable;
+        }
+
+        @Override
+        public Set<Variable> getOutputVariables() {
+                return Set.of(resultVariable);
+        }
+
+        protected abstract T zero();
+
+        protected abstract T one();
+
+        @Override
+        public Literal reduce() {
+                var reduction = getTarget().getReduction();
+                return switch (reduction) {
+                        case ALWAYS_FALSE -> getResultVariable().assign(new ConstantTerm<>(resultType, zero()));
+                        // The only way a constant {@code true} predicate can be called in a negative position is to have all of
+                        // its arguments bound as input variables. Thus, there will only be a single match.
+                        case ALWAYS_TRUE -> getResultVariable().assign(new ConstantTerm<>(resultType, one()));
+                        case NOT_REDUCIBLE -> this;
+                };
+        }
+
+        @Override
+        public boolean equalsWithSubstitution(LiteralEqualityHelper helper, Literal other) {
+                if (!super.equalsWithSubstitution(helper, other)) {
+                        return false;
+                }
+                var otherCountLiteral = (AbstractCountLiteral<?>) other;
+                return Objects.equals(resultType, otherCountLiteral.resultType) &&
+                                helper.variableEqual(resultVariable, otherCountLiteral.resultVariable);
+        }
+
+        @Override
+        public int hashCodeWithSubstitution(LiteralHashCodeHelper helper) {
+                return Objects.hash(super.hashCodeWithSubstitution(helper), resultType,
+                                helper.getVariableHashCode(resultVariable));
+        }
+
+        protected abstract String operatorName();
+
+        @Override
+        public String toString() {
+                var builder = new StringBuilder();
+                builder.append(resultVariable);
+                builder.append(" is ");
+                builder.append(operatorName());
+                builder.append(' ');
+                builder.append(getTarget().toReferenceString());
+                builder.append('(');
+                var argumentIterator = getArguments().iterator();
+                if (argumentIterator.hasNext()) {
+                        builder.append(argumentIterator.next());
+                        while (argumentIterator.hasNext()) {
+                                builder.append(", ").append(argumentIterator.next());
+                        }
+                }
+                builder.append(')');
+                return builder.toString();
+        }
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/CountLiteral.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/CountLiteral.java
index 77b77389..e5f6ac0c 100644
--- a/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/CountLiteral.java
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/CountLiteral.java
@@ -6,95 +6,40 @@
 package tools.refinery.store.query.literal;
 
 import tools.refinery.store.query.Constraint;
-import tools.refinery.store.query.equality.LiteralEqualityHelper;
-import tools.refinery.store.query.equality.LiteralHashCodeHelper;
 import tools.refinery.store.query.substitution.Substitution;
 import tools.refinery.store.query.term.DataVariable;
 import tools.refinery.store.query.term.Variable;
-import tools.refinery.store.query.term.int_.IntTerms;
 
 import java.util.List;
-import java.util.Objects;
-import java.util.Set;
-
-// {@link Object#equals(Object)} is implemented by {@link AbstractLiteral}.
-@SuppressWarnings("squid:S2160")
-public class CountLiteral extends AbstractCallLiteral {
-        private final DataVariable<Integer> resultVariable;
 
+public class CountLiteral extends AbstractCountLiteral<Integer> {
         public CountLiteral(DataVariable<Integer> resultVariable, Constraint target, List<Variable> arguments) {
-                super(target, arguments);
-                if (!resultVariable.getType().equals(Integer.class)) {
-                        throw new IllegalArgumentException("Count result variable %s must be of type %s, got %s instead".formatted(
-                                        resultVariable, Integer.class.getName(), resultVariable.getType().getName()));
-                }
-                if (arguments.contains(resultVariable)) {
-                        throw new IllegalArgumentException("Count result variable %s must not appear in the argument list"
-                                        .formatted(resultVariable));
-                }
-                this.resultVariable = resultVariable;
-        }
-
-        public DataVariable<Integer> getResultVariable() {
-                return resultVariable;
+                super(Integer.class, resultVariable, target, arguments);
         }
 
         @Override
-        public Set<Variable> getOutputVariables() {
-                return Set.of(resultVariable);
+        protected Integer zero() {
+                return 0;
         }
 
         @Override
-        public Literal reduce() {
-                var reduction = getTarget().getReduction();
-                return switch (reduction) {
-                        case ALWAYS_FALSE -> getResultVariable().assign(IntTerms.constant(0));
-                        // The only way a constant {@code true} predicate can be called in a negative position is to have all of
-                        // its arguments bound as input variables. Thus, there will only be a single match.
-                        case ALWAYS_TRUE -> getResultVariable().assign(IntTerms.constant(1));
-                        case NOT_REDUCIBLE -> this;
-                };
+        protected Integer one() {
+                return 1;
         }
 
         @Override
         protected Literal doSubstitute(Substitution substitution, List<Variable> substitutedArguments) {
-                return new CountLiteral(substitution.getTypeSafeSubstitute(resultVariable), getTarget(), substitutedArguments);
+                return new CountLiteral(substitution.getTypeSafeSubstitute(getResultVariable()), getTarget(),
+                                substitutedArguments);
         }
 
         @Override
         protected AbstractCallLiteral internalWithTarget(Constraint newTarget) {
-                return new CountLiteral(resultVariable, newTarget, getArguments());
-        }
-
-        @Override
-        public boolean equalsWithSubstitution(LiteralEqualityHelper helper, Literal other) {
-                if (!super.equalsWithSubstitution(helper, other)) {
-                        return false;
-                }
-                var otherCountLiteral = (CountLiteral) other;
-                return helper.variableEqual(resultVariable, otherCountLiteral.resultVariable);
-        }
-
-        @Override
-        public int hashCodeWithSubstitution(LiteralHashCodeHelper helper) {
-                return Objects.hash(super.hashCodeWithSubstitution(helper), helper.getVariableHashCode(resultVariable));
+                return new CountLiteral(getResultVariable(), newTarget, getArguments());
         }
 
         @Override
-        public String toString() {
-                var builder = new StringBuilder();
-                builder.append(resultVariable);
-                builder.append(" is count ");
-                builder.append(getTarget().toReferenceString());
-                builder.append("(");
-                var argumentIterator = getArguments().iterator();
-                if (argumentIterator.hasNext()) {
-                        builder.append(argumentIterator.next());
-                        while (argumentIterator.hasNext()) {
-                                builder.append(", ").append(argumentIterator.next());
-                        }
-                }
-                builder.append(")");
-                return builder.toString();
+        protected String operatorName() {
+                return "count";
         }
 }
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/uppercardinality/UpperCardinalitySumAggregator.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/uppercardinality/UpperCardinalitySumAggregator.java
index 5bbd3081..d31f00a2 100644
--- a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/uppercardinality/UpperCardinalitySumAggregator.java
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/uppercardinality/UpperCardinalitySumAggregator.java
@@ -70,7 +70,7 @@ public class UpperCardinalitySumAggregator implements StatefulAggregator<UpperCa
 
                 @Override
                 public UpperCardinality getResult() {
-                        return countUnbounded > 0 ? UpperCardinalities.UNBOUNDED : UpperCardinalities.valueOf(sumFiniteUpperBounds);
+                        return countUnbounded > 0 ? UpperCardinalities.UNBOUNDED : UpperCardinalities.atMost(sumFiniteUpperBounds);
                 }
 
                 @Override
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/internal/PartialClauseRewriter.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/internal/PartialClauseRewriter.java
index bc379c64..c560162e 100644
--- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/internal/PartialClauseRewriter.java
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/internal/PartialClauseRewriter.java
@@ -5,17 +5,25 @@
  */
 package tools.refinery.store.reasoning.internal;
 
+import tools.refinery.store.query.Constraint;
 import tools.refinery.store.query.dnf.Dnf;
 import tools.refinery.store.query.dnf.DnfClause;
 import tools.refinery.store.query.literal.AbstractCallLiteral;
+import tools.refinery.store.query.literal.CallPolarity;
 import tools.refinery.store.query.literal.Literal;
+import tools.refinery.store.query.term.Aggregator;
+import tools.refinery.store.query.term.ConstantTerm;
+import tools.refinery.store.query.term.Term;
 import tools.refinery.store.query.term.Variable;
-import tools.refinery.store.reasoning.literal.Concreteness;
-import tools.refinery.store.reasoning.literal.ModalConstraint;
-import tools.refinery.store.reasoning.literal.Modality;
+import tools.refinery.store.query.term.int_.IntTerms;
+import tools.refinery.store.query.term.uppercardinality.UpperCardinalityTerms;
+import tools.refinery.store.reasoning.literal.*;
 import tools.refinery.store.reasoning.representation.PartialRelation;
+import tools.refinery.store.reasoning.translator.multiobject.MultiObjectTranslator;
+import tools.refinery.store.representation.cardinality.UpperCardinalities;
 
 import java.util.*;
+import java.util.function.BinaryOperator;
 
 class PartialClauseRewriter {
         private final PartialQueryRewriter rewriter;
@@ -42,6 +50,14 @@ class PartialClauseRewriter {
                         markAsDone(literal);
                         return;
                 }
+                if (callLiteral instanceof CountLowerBoundLiteral countLowerBoundLiteral) {
+                        rewriteCountLowerBound(countLowerBoundLiteral);
+                        return;
+                }
+                if (callLiteral instanceof CountUpperBoundLiteral countUpperBoundLiteral) {
+                        rewriteCountUpperBound(countUpperBoundLiteral);
+                        return;
+                }
                 var target = callLiteral.getTarget();
                 if (target instanceof Dnf dnf) {
                         rewriteRecursively(callLiteral, dnf);
@@ -61,6 +77,75 @@ class PartialClauseRewriter {
                 }
         }
 
+        private void rewriteCountLowerBound(CountLowerBoundLiteral literal) {
+                rewriteCount(literal, "lower", Modality.MUST, MultiObjectTranslator.LOWER_CARDINALITY_VIEW, 1, IntTerms::mul,
+                                IntTerms.INT_SUM);
+        }
+
+        private void rewriteCountUpperBound(CountUpperBoundLiteral literal) {
+                rewriteCount(literal, "upper", Modality.MAY, MultiObjectTranslator.UPPER_CARDINALITY_VIEW,
+                                UpperCardinalities.ONE, UpperCardinalityTerms::mul, UpperCardinalityTerms.UPPER_CARDINALITY_SUM);
+        }
+
+        private <T> void rewriteCount(ConcreteCountLiteral<T> literal, String name, Modality modality, Constraint view,
+                                                                  T one, BinaryOperator<Term<T>> mul, Aggregator<T, T> sum) {
+                var type = literal.getResultType();
+                var target = literal.getTarget();
+                var concreteness = literal.getConcreteness();
+                int arity = target.arity();
+                var parameters = target.getParameters();
+                var literalArguments = literal.getArguments();
+                var privateVariables = literal.getPrivateVariables(positiveVariables);
+
+                var builder = Dnf.builder("%s#%s#%s".formatted(target.name(), concreteness, name));
+                var rewrittenArguments = new ArrayList<Variable>(parameters.size());
+                var variablesToCount = new ArrayList<Variable>();
+                var helperArguments = new ArrayList<Variable>();
+                var literalToRewrittenArgumentMap = new HashMap<Variable, Variable>();
+                for (int i = 0; i < arity; i++) {
+                        var literalArgument = literalArguments.get(i);
+                        var parameter = parameters.get(i);
+                        var rewrittenArgument = literalToRewrittenArgumentMap.computeIfAbsent(literalArgument, key -> {
+                                helperArguments.add(key);
+                                var newArgument = builder.parameter(parameter);
+                                if (privateVariables.contains(key)) {
+                                        variablesToCount.add(newArgument);
+                                }
+                                return newArgument;
+                        });
+                        rewrittenArguments.add(rewrittenArgument);
+                }
+                var outputVariable = builder.parameter(type);
+
+                var literals = new ArrayList<Literal>();
+                literals.add(new ModalConstraint(modality, literal.getConcreteness(), target)
+                                .call(CallPolarity.POSITIVE, rewrittenArguments));
+                switch (variablesToCount.size()) {
+                case 0 -> literals.add(outputVariable.assign(new ConstantTerm<>(type, one)));
+                case 1 -> literals.add(view.call(variablesToCount.get(0),
+                                outputVariable));
+                default -> {
+                        var firstCount = Variable.of(type);
+                        literals.add(view.call(variablesToCount.get(0), firstCount));
+                        int length = variablesToCount.size();
+                        Term<T> accumulator = firstCount;
+                        for (int i = 1; i < length; i++) {
+                                var countVariable = Variable.of(type);
+                                literals.add(view.call(variablesToCount.get(i), countVariable));
+                                accumulator = mul.apply(accumulator, countVariable);
+                        }
+                        literals.add(outputVariable.assign(accumulator));
+                }
+                }
+                builder.clause(literals);
+
+                var helperQuery = builder.build();
+                var aggregationVariable = Variable.of(type);
+                helperArguments.add(aggregationVariable);
+                workList.addFirst(literal.getResultVariable().assign(helperQuery.aggregateBy(aggregationVariable, sum,
+                                helperArguments)));
+        }
+
         private void markAsDone(Literal literal) {
                 completedLiterals.add(literal);
                 positiveVariables.addAll(literal.getOutputVariables());
@@ -75,7 +160,7 @@ class PartialClauseRewriter {
         private void rewriteRecursively(AbstractCallLiteral callLiteral, Dnf dnf) {
                 var rewrittenDnf = rewriter.rewrite(dnf);
                 var rewrittenLiteral = callLiteral.withTarget(rewrittenDnf);
-                completedLiterals.add(rewrittenLiteral);
+                markAsDone(rewrittenLiteral);
         }
 
         private void rewrite(AbstractCallLiteral callLiteral, Modality modality, Concreteness concreteness,
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/lifting/ClauseLifter.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/lifting/ClauseLifter.java
index 89e948dc..17916c02 100644
--- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/lifting/ClauseLifter.java
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/lifting/ClauseLifter.java
@@ -70,9 +70,9 @@ class ClauseLifter {
                                 literal instanceof AssignLiteral<?> ||
                                 literal instanceof CheckLiteral) {
                         return literal;
-                } else if (literal instanceof CountLiteral) {
+                } else if (literal instanceof AbstractCountLiteral<?>) {
                         throw new IllegalArgumentException("Count literal %s cannot be lifted".formatted(literal));
-                } else if (literal instanceof AggregationLiteral<?,?>) {
+                } else if (literal instanceof AggregationLiteral<?, ?>) {
                         throw new IllegalArgumentException("Aggregation literal %s cannot be lifted".formatted(literal));
                 } else if (literal instanceof RepresentativeElectionLiteral) {
                         throw new IllegalArgumentException("SCC literal %s cannot be lifted".formatted(literal));
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/literal/ConcreteCountLiteral.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/literal/ConcreteCountLiteral.java
new file mode 100644
index 00000000..91b30964
--- /dev/null
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/literal/ConcreteCountLiteral.java
@@ -0,0 +1,47 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.reasoning.literal;
+
+import tools.refinery.store.query.Constraint;
+import tools.refinery.store.query.equality.LiteralEqualityHelper;
+import tools.refinery.store.query.equality.LiteralHashCodeHelper;
+import tools.refinery.store.query.literal.AbstractCountLiteral;
+import tools.refinery.store.query.literal.Literal;
+import tools.refinery.store.query.term.DataVariable;
+import tools.refinery.store.query.term.Variable;
+
+import java.util.List;
+import java.util.Objects;
+
+// {@link Object#equals(Object)} is implemented by {@link AbstractLiteral}.
+@SuppressWarnings("squid:S2160")
+public abstract class ConcreteCountLiteral<T> extends AbstractCountLiteral<T> {
+        private final Concreteness concreteness;
+
+        protected ConcreteCountLiteral(Class<T> resultType, DataVariable<T> resultVariable, Concreteness concreteness,
+                                                                   Constraint target, List<Variable> arguments) {
+                super(resultType, resultVariable, target, arguments);
+                this.concreteness = concreteness;
+        }
+
+        public Concreteness getConcreteness() {
+                return concreteness;
+        }
+
+        @Override
+        public boolean equalsWithSubstitution(LiteralEqualityHelper helper, Literal other) {
+                if (!super.equalsWithSubstitution(helper, other)) {
+                        return false;
+                }
+                var otherCountLiteral = (ConcreteCountLiteral<?>) other;
+                return Objects.equals(concreteness, otherCountLiteral.concreteness);
+        }
+
+        @Override
+        public int hashCodeWithSubstitution(LiteralHashCodeHelper helper) {
+                return Objects.hash(super.hashCodeWithSubstitution(helper), concreteness);
+        }
+}
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/literal/CountLowerBoundLiteral.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/literal/CountLowerBoundLiteral.java
new file mode 100644
index 00000000..261088fc
--- /dev/null
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/literal/CountLowerBoundLiteral.java
@@ -0,0 +1,48 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.reasoning.literal;
+
+import tools.refinery.store.query.Constraint;
+import tools.refinery.store.query.literal.AbstractCallLiteral;
+import tools.refinery.store.query.literal.Literal;
+import tools.refinery.store.query.substitution.Substitution;
+import tools.refinery.store.query.term.DataVariable;
+import tools.refinery.store.query.term.Variable;
+
+import java.util.List;
+
+public class CountLowerBoundLiteral extends ConcreteCountLiteral<Integer> {
+        public CountLowerBoundLiteral(DataVariable<Integer> resultVariable, Concreteness concreteness, Constraint target,
+                                                                  List<Variable> arguments) {
+                super(Integer.class, resultVariable, concreteness, target, arguments);
+        }
+
+        @Override
+        protected Integer zero() {
+                return 0;
+        }
+
+        @Override
+        protected Integer one() {
+                return 1;
+        }
+
+        @Override
+        protected Literal doSubstitute(Substitution substitution, List<Variable> substitutedArguments) {
+                return new CountLowerBoundLiteral(substitution.getTypeSafeSubstitute(getResultVariable()), getConcreteness(),
+                                getTarget(), substitutedArguments);
+        }
+
+        @Override
+        protected AbstractCallLiteral internalWithTarget(Constraint newTarget) {
+                return new CountLowerBoundLiteral(getResultVariable(), getConcreteness(), newTarget, getArguments());
+        }
+
+        @Override
+        protected String operatorName() {
+                return "@LowerBound(\"%s\") count".formatted(getConcreteness());
+        }
+}
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/literal/CountUpperBoundLiteral.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/literal/CountUpperBoundLiteral.java
new file mode 100644
index 00000000..960ded69
--- /dev/null
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/literal/CountUpperBoundLiteral.java
@@ -0,0 +1,50 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.reasoning.literal;
+
+import tools.refinery.store.query.Constraint;
+import tools.refinery.store.query.literal.AbstractCallLiteral;
+import tools.refinery.store.query.literal.Literal;
+import tools.refinery.store.query.substitution.Substitution;
+import tools.refinery.store.query.term.DataVariable;
+import tools.refinery.store.query.term.Variable;
+import tools.refinery.store.representation.cardinality.UpperCardinalities;
+import tools.refinery.store.representation.cardinality.UpperCardinality;
+
+import java.util.List;
+
+public class CountUpperBoundLiteral extends ConcreteCountLiteral<UpperCardinality> {
+        public CountUpperBoundLiteral(DataVariable<UpperCardinality> resultVariable, Concreteness concreteness,
+                                                                  Constraint target, List<Variable> arguments) {
+                super(UpperCardinality.class, resultVariable, concreteness, target, arguments);
+        }
+
+        @Override
+        protected UpperCardinality zero() {
+                return UpperCardinalities.ZERO;
+        }
+
+        @Override
+        protected UpperCardinality one() {
+                return UpperCardinalities.UNBOUNDED;
+        }
+
+        @Override
+        protected Literal doSubstitute(Substitution substitution, List<Variable> substitutedArguments) {
+                return new CountUpperBoundLiteral(substitution.getTypeSafeSubstitute(getResultVariable()), getConcreteness(),
+                                getTarget(), substitutedArguments);
+        }
+
+        @Override
+        protected AbstractCallLiteral internalWithTarget(Constraint newTarget) {
+                return new CountUpperBoundLiteral(getResultVariable(), getConcreteness(), newTarget, getArguments());
+        }
+
+        @Override
+        protected String operatorName() {
+                return "@UpperBound(\"%s\") count".formatted(getConcreteness());
+        }
+}
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/seed/ModelSeed.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/seed/ModelSeed.java
index 3641730d..28e6258e 100644
--- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/seed/ModelSeed.java
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/seed/ModelSeed.java
@@ -39,6 +39,10 @@ public class ModelSeed {
                 return typedSeed;
         }
 
+        public boolean containsSeed(AnyPartialSymbol symbol) {
+                return seeds.containsKey(symbol);
+        }
+
         public <A> Cursor<Tuple, A> getCursor(PartialSymbol<A, ?> partialSymbol, A defaultValue) {
                 return getSeed(partialSymbol).getCursor(defaultValue, nodeCount);
         }
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
index c7bc9fff..393a8769 100644
--- 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
@@ -11,6 +11,7 @@ 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;
@@ -67,7 +68,7 @@ class EqualsRelationRewriter extends QueryBasedRelationRewriter {
                 };
         }
 
-        public static EqualsRelationRewriter of(UpperCardinalityView upperCardinalityView) {
+        public static EqualsRelationRewriter of(AnySymbolView upperCardinalityView) {
                 var may = Query.of("MAY_EQUALS", (builder, p1, p2) -> builder
                                 .clause(
                                                 p1.isEquivalent(p2),
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
index 6917b8ed..084bf6f9 100644
--- 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
@@ -5,6 +5,7 @@
  */
 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;
@@ -26,8 +27,7 @@ class MultiObjectInitializer implements PartialModelInitializer {
 
         @Override
         public void initialize(Model model, ModelSeed modelSeed) {
-                var intervals = new CardinalityInterval[modelSeed.getNodeCount()];
-                Arrays.fill(intervals, CardinalityIntervals.SET);
+                var intervals = initializeIntervals(modelSeed);
                 initializeExists(intervals, modelSeed);
                 initializeEquals(intervals, modelSeed);
                 var countInterpretation = model.getInterpretation(countSymbol);
@@ -40,7 +40,33 @@ class MultiObjectInitializer implements PartialModelInitializer {
                 }
         }
 
+        @NotNull
+        private CardinalityInterval[] initializeIntervals(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()) {
+                                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 IllegalArgumentException("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, ModelSeed modelSeed) {
+                if (!modelSeed.containsSeed(ReasoningAdapter.EXISTS_SYMBOL)) {
+                        return;
+                }
                 var cursor = modelSeed.getCursor(ReasoningAdapter.EXISTS_SYMBOL, TruthValue.UNKNOWN);
                 while (cursor.move()) {
                         int i = cursor.getKey().get(0);
@@ -56,6 +82,9 @@ class MultiObjectInitializer implements PartialModelInitializer {
         }
 
         private void initializeEquals(CardinalityInterval[] intervals, 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()) {
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 0367214b..09993c80 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
@@ -8,11 +8,14 @@ package tools.refinery.store.reasoning.translator.multiobject;
 import tools.refinery.store.model.ModelStoreBuilder;
 import tools.refinery.store.model.ModelStoreConfiguration;
 import tools.refinery.store.query.dnf.Query;
+import tools.refinery.store.query.view.AnySymbolView;
 import tools.refinery.store.reasoning.ReasoningAdapter;
 import tools.refinery.store.reasoning.ReasoningBuilder;
+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;
@@ -26,35 +29,37 @@ 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 final Symbol<CardinalityInterval> countSymbol = Symbol.of("COUNT", 1, CardinalityInterval.class,
+        private static final Symbol<CardinalityInterval> COUNT_STORAGE = Symbol.of("COUNT", 1, CardinalityInterval.class,
                         null);
-        private final LowerCardinalityView lowerCardinalityView = new LowerCardinalityView(countSymbol);
-        private final UpperCardinalityView upperCardinalityView = new UpperCardinalityView(countSymbol);
+        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 PartialFunction<CardinalityInterval, Integer> COUNT_SYMBOL = new PartialFunction<>("COUNT", 1,
+                        CardinalityDomain.INSTANCE);
 
         @Override
         public void apply(ModelStoreBuilder storeBuilder) {
-                storeBuilder.symbol(countSymbol);
+                storeBuilder.symbol(COUNT_STORAGE);
 
                 storeBuilder.with(PartialRelationTranslator.of(ReasoningAdapter.EXISTS_SYMBOL)
                                 .may(Query.of("MAY_EXISTS", (builder, p1) -> builder
                                                 .clause(UpperCardinality.class, upper -> List.of(
-                                                                upperCardinalityView.call(p1, upper),
+                                                                UPPER_CARDINALITY_VIEW.call(p1, upper),
                                                                 check(greaterEq(upper, constant(UpperCardinalities.ONE)))
                                                 ))))
                                 .must(Query.of("MUST_EXISTS", (builder, p1) -> builder
                                                 .clause(Integer.class, lower -> List.of(
-                                                                lowerCardinalityView.call(p1, lower),
+                                                                LOWER_CARDINALITY_VIEW.call(p1, lower),
                                                                 check(greaterEq(lower, constant(1)))
                                                 ))))
                                 .roundingMode(RoundingMode.PREFER_FALSE)
-                                .refiner(ExistsRefiner.of(countSymbol)));
+                                .refiner(ExistsRefiner.of(COUNT_STORAGE)));
 
                 storeBuilder.with(PartialRelationTranslator.of(ReasoningAdapter.EQUALS_SYMBOL)
-                                .rewriter(EqualsRelationRewriter.of(upperCardinalityView))
-                                .refiner(EqualsRefiner.of(countSymbol)));
+                                .rewriter(EqualsRelationRewriter.of(UPPER_CARDINALITY_VIEW))
+                                .refiner(EqualsRefiner.of(COUNT_STORAGE)));
 
                 var reasoningBuilder = storeBuilder.getAdapter(ReasoningBuilder.class);
-                reasoningBuilder.initializer(new MultiObjectInitializer(countSymbol));
-                reasoningBuilder.storageRefiner(countSymbol, MultiObjectStorageRefiner::new);
+                reasoningBuilder.initializer(new MultiObjectInitializer(COUNT_STORAGE));
+                reasoningBuilder.storageRefiner(COUNT_STORAGE, MultiObjectStorageRefiner::new);
         }
 }
diff --git a/subprojects/store-reasoning/src/test/java/tools/refinery/store/reasoning/ConcreteCountTest.java b/subprojects/store-reasoning/src/test/java/tools/refinery/store/reasoning/ConcreteCountTest.java
new file mode 100644
index 00000000..21111d7c
--- /dev/null
+++ b/subprojects/store-reasoning/src/test/java/tools/refinery/store/reasoning/ConcreteCountTest.java
@@ -0,0 +1,324 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.reasoning;
+
+import org.junit.jupiter.api.Test;
+import tools.refinery.store.model.ModelStore;
+import tools.refinery.store.query.ModelQueryAdapter;
+import tools.refinery.store.query.dnf.Query;
+import tools.refinery.store.query.resultset.ResultSet;
+import tools.refinery.store.query.term.Variable;
+import tools.refinery.store.query.viatra.ViatraModelQueryAdapter;
+import tools.refinery.store.reasoning.literal.Concreteness;
+import tools.refinery.store.reasoning.literal.CountLowerBoundLiteral;
+import tools.refinery.store.reasoning.literal.CountUpperBoundLiteral;
+import tools.refinery.store.reasoning.representation.PartialRelation;
+import tools.refinery.store.reasoning.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.CardinalityIntervals;
+import tools.refinery.store.representation.cardinality.UpperCardinalities;
+import tools.refinery.store.representation.cardinality.UpperCardinality;
+import tools.refinery.store.tuple.Tuple;
+
+import java.util.List;
+
+import static org.hamcrest.MatcherAssert.assertThat;
+import static org.hamcrest.Matchers.is;
+import static tools.refinery.store.query.literal.Literals.not;
+import static tools.refinery.store.reasoning.literal.PartialLiterals.must;
+
+class ConcreteCountTest {
+        private static final PartialRelation person = new PartialRelation("Person", 1);
+        private static final PartialRelation friend = new PartialRelation("friend", 2);
+
+        @Test
+        void lowerBoundZeroTest() {
+                var query = Query.of("LowerBound", Integer.class, (builder, p1, p2, output) -> builder.clause(
+                                must(person.call(p1)),
+                                must(person.call(p2)),
+                                new CountLowerBoundLiteral(output, Concreteness.PARTIAL, friend, List.of(p1, p2))
+                ));
+
+                var modelSeed = ModelSeed.builder(2)
+                                .seed(MultiObjectTranslator.COUNT_SYMBOL, builder -> builder
+                                                .put(Tuple.of(0), CardinalityIntervals.atLeast(3))
+                                                .put(Tuple.of(1), CardinalityIntervals.atMost(7)))
+                                .seed(person, builder -> builder.reducedValue(TruthValue.TRUE))
+                                .seed(friend, builder -> builder
+                                                .put(Tuple.of(0, 1), TruthValue.TRUE)
+                                                .put(Tuple.of(1, 0), TruthValue.UNKNOWN)
+                                                .put(Tuple.of(1, 1), TruthValue.ERROR))
+                                .build();
+
+                var resultSet = getResultSet(query, modelSeed);
+                assertThat(resultSet.get(Tuple.of(0, 0)), is(0));
+                assertThat(resultSet.get(Tuple.of(0, 1)), is(1));
+                assertThat(resultSet.get(Tuple.of(1, 0)), is(0));
+                assertThat(resultSet.get(Tuple.of(1, 1)), is(1));
+        }
+
+        @Test
+        void upperBoundZeroTest() {
+                var query = Query.of("UpperBound", UpperCardinality.class, (builder, p1, p2, output) -> builder.clause(
+                                must(person.call(p1)),
+                                must(person.call(p2)),
+                                new CountUpperBoundLiteral(output, Concreteness.PARTIAL, friend, List.of(p1, p2))
+                ));
+
+                var modelSeed = ModelSeed.builder(2)
+                                .seed(MultiObjectTranslator.COUNT_SYMBOL, builder -> builder
+                                                .put(Tuple.of(0), CardinalityIntervals.atLeast(3))
+                                                .put(Tuple.of(1), CardinalityIntervals.atMost(7)))
+                                .seed(person, builder -> builder.reducedValue(TruthValue.TRUE))
+                                .seed(friend, builder -> builder
+                                                .put(Tuple.of(0, 1), TruthValue.TRUE)
+                                                .put(Tuple.of(1, 0), TruthValue.UNKNOWN)
+                                                .put(Tuple.of(1, 1), TruthValue.ERROR))
+                                .build();
+
+                var resultSet = getResultSet(query, modelSeed);
+                assertThat(resultSet.get(Tuple.of(0, 0)), is(UpperCardinalities.ZERO));
+                assertThat(resultSet.get(Tuple.of(0, 1)), is(UpperCardinalities.ONE));
+                assertThat(resultSet.get(Tuple.of(1, 0)), is(UpperCardinalities.ONE));
+                assertThat(resultSet.get(Tuple.of(1, 1)), is(UpperCardinalities.ZERO));
+        }
+
+        @Test
+        void lowerBoundOneTest() {
+                var query = Query.of("LowerBound", Integer.class, (builder, p1, output) -> builder.clause(
+                                must(person.call(p1)),
+                                new CountLowerBoundLiteral(output, Concreteness.PARTIAL, friend, List.of(p1, Variable.of()))
+                ));
+
+                var modelSeed = ModelSeed.builder(4)
+                                .seed(MultiObjectTranslator.COUNT_SYMBOL, builder -> builder
+                                                .reducedValue(CardinalityIntervals.ONE)
+                                                .put(Tuple.of(1), CardinalityIntervals.atLeast(3))
+                                                .put(Tuple.of(2), CardinalityIntervals.atMost(7)))
+                                .seed(person, builder -> builder.reducedValue(TruthValue.TRUE))
+                                .seed(friend, builder -> builder
+                                                .put(Tuple.of(0, 1), TruthValue.TRUE)
+                                                .put(Tuple.of(0, 2), TruthValue.TRUE)
+                                                .put(Tuple.of(0, 3), TruthValue.TRUE)
+                                                .put(Tuple.of(1, 0), TruthValue.TRUE)
+                                                .put(Tuple.of(1, 2), TruthValue.UNKNOWN)
+                                                .put(Tuple.of(1, 3), TruthValue.UNKNOWN)
+                                                .put(Tuple.of(2, 0), TruthValue.TRUE)
+                                                .put(Tuple.of(2, 1), TruthValue.ERROR))
+                                .build();
+
+                var resultSet = getResultSet(query, modelSeed);
+                assertThat(resultSet.get(Tuple.of(0)), is(4));
+                assertThat(resultSet.get(Tuple.of(1)), is(1));
+                assertThat(resultSet.get(Tuple.of(2)), is(4));
+                assertThat(resultSet.get(Tuple.of(3)), is(0));
+        }
+
+        @Test
+        void upperBoundOneTest() {
+                var query = Query.of("UpperBound", UpperCardinality.class, (builder, p1, output) -> builder.clause(
+                                must(person.call(p1)),
+                                new CountUpperBoundLiteral(output, Concreteness.PARTIAL, friend, List.of(p1, Variable.of()))
+                ));
+
+                var modelSeed = ModelSeed.builder(4)
+                                .seed(MultiObjectTranslator.COUNT_SYMBOL, builder -> builder
+                                                .reducedValue(CardinalityIntervals.ONE)
+                                                .put(Tuple.of(1), CardinalityIntervals.atLeast(3))
+                                                .put(Tuple.of(2), CardinalityIntervals.atMost(7)))
+                                .seed(person, builder -> builder.reducedValue(TruthValue.TRUE))
+                                .seed(friend, builder -> builder
+                                                .put(Tuple.of(0, 1), TruthValue.TRUE)
+                                                .put(Tuple.of(0, 2), TruthValue.TRUE)
+                                                .put(Tuple.of(0, 3), TruthValue.TRUE)
+                                                .put(Tuple.of(1, 0), TruthValue.TRUE)
+                                                .put(Tuple.of(1, 2), TruthValue.UNKNOWN)
+                                                .put(Tuple.of(1, 3), TruthValue.UNKNOWN)
+                                                .put(Tuple.of(2, 0), TruthValue.TRUE)
+                                                .put(Tuple.of(2, 1), TruthValue.ERROR))
+                                .build();
+
+                var resultSet = getResultSet(query, modelSeed);
+                assertThat(resultSet.get(Tuple.of(0)), is(UpperCardinalities.UNBOUNDED));
+                assertThat(resultSet.get(Tuple.of(1)), is(UpperCardinalities.atMost(9)));
+                assertThat(resultSet.get(Tuple.of(2)), is(UpperCardinalities.ONE));
+                assertThat(resultSet.get(Tuple.of(3)), is(UpperCardinalities.ZERO));
+        }
+
+        @Test
+        void lowerBoundTwoTest() {
+                var subQuery = Query.of("SubQuery", (builder, p1, p2, p3) -> builder.clause(
+                                friend.call(p1, p2),
+                                friend.call(p1, p3),
+                                friend.call(p2, p3)
+                ));
+                var query = Query.of("LowerBound", Integer.class, (builder, p1, output) -> builder.clause(
+                                must(person.call(p1)),
+                                new CountLowerBoundLiteral(output, Concreteness.PARTIAL, subQuery.getDnf(),
+                                                List.of(p1, Variable.of(), Variable.of()))
+                ));
+
+                var modelSeed = ModelSeed.builder(4)
+                                .seed(MultiObjectTranslator.COUNT_SYMBOL, builder -> builder
+                                                .reducedValue(CardinalityIntervals.ONE)
+                                                .put(Tuple.of(0), CardinalityIntervals.between(5, 9))
+                                                .put(Tuple.of(1), CardinalityIntervals.atLeast(3))
+                                                .put(Tuple.of(2), CardinalityIntervals.atMost(7)))
+                                .seed(person, builder -> builder.reducedValue(TruthValue.TRUE))
+                                .seed(friend, builder -> builder
+                                                .put(Tuple.of(0, 1), TruthValue.TRUE)
+                                                .put(Tuple.of(0, 2), TruthValue.TRUE)
+                                                .put(Tuple.of(0, 3), TruthValue.TRUE)
+                                                .put(Tuple.of(1, 0), TruthValue.TRUE)
+                                                .put(Tuple.of(1, 2), TruthValue.TRUE)
+                                                .put(Tuple.of(1, 3), TruthValue.TRUE)
+                                                .put(Tuple.of(2, 0), TruthValue.TRUE)
+                                                .put(Tuple.of(2, 1), TruthValue.ERROR))
+                                .build();
+
+                var resultSet = getResultSet(query, modelSeed);
+                assertThat(resultSet.get(Tuple.of(0)), is(3));
+                assertThat(resultSet.get(Tuple.of(1)), is(5));
+                assertThat(resultSet.get(Tuple.of(2)), is(30));
+                assertThat(resultSet.get(Tuple.of(3)), is(0));
+        }
+
+        @Test
+        void upperBoundTwoTest() {
+                var subQuery = Query.of("SubQuery", (builder, p1, p2, p3) -> builder.clause(
+                                friend.call(p1, p2),
+                                friend.call(p1, p3),
+                                friend.call(p2, p3)
+                ));
+                var query = Query.of("UpperBound", UpperCardinality.class, (builder, p1, output) -> builder.clause(
+                                must(person.call(p1)),
+                                new CountUpperBoundLiteral(output, Concreteness.PARTIAL, subQuery.getDnf(),
+                                                List.of(p1, Variable.of(), Variable.of()))
+                ));
+
+                var modelSeed = ModelSeed.builder(4)
+                                .seed(MultiObjectTranslator.COUNT_SYMBOL, builder -> builder
+                                                .reducedValue(CardinalityIntervals.ONE)
+                                                .put(Tuple.of(0), CardinalityIntervals.between(5, 9))
+                                                .put(Tuple.of(1), CardinalityIntervals.atLeast(3))
+                                                .put(Tuple.of(2), CardinalityIntervals.atMost(7)))
+                                .seed(person, builder -> builder.reducedValue(TruthValue.TRUE))
+                                .seed(friend, builder -> builder
+                                                .put(Tuple.of(0, 1), TruthValue.TRUE)
+                                                .put(Tuple.of(0, 2), TruthValue.TRUE)
+                                                .put(Tuple.of(0, 3), TruthValue.TRUE)
+                                                .put(Tuple.of(1, 0), TruthValue.TRUE)
+                                                .put(Tuple.of(1, 2), TruthValue.UNKNOWN)
+                                                .put(Tuple.of(1, 3), TruthValue.UNKNOWN)
+                                                .put(Tuple.of(2, 0), TruthValue.TRUE)
+                                                .put(Tuple.of(2, 1), TruthValue.ERROR))
+                                .build();
+
+                var resultSet = getResultSet(query, modelSeed);
+                assertThat(resultSet.get(Tuple.of(0)), is(UpperCardinalities.UNBOUNDED));
+                assertThat(resultSet.get(Tuple.of(1)), is(UpperCardinalities.atMost(135)));
+                assertThat(resultSet.get(Tuple.of(2)), is(UpperCardinalities.ZERO));
+                assertThat(resultSet.get(Tuple.of(3)), is(UpperCardinalities.ZERO));
+        }
+
+        @Test
+        void lowerBoundDiagonalTest() {
+                var subQuery = Query.of("SubQuery", (builder, p1, p2, p3) -> builder.clause(
+                                friend.call(p1, p2),
+                                friend.call(p1, p3),
+                                not(friend.call(p2, p3))
+                ));
+                var query = Query.of("LowerBound", Integer.class, (builder, p1, output) -> builder.clause(v1 -> List.of(
+                                must(person.call(p1)),
+                                new CountLowerBoundLiteral(output, Concreteness.PARTIAL, subQuery.getDnf(), List.of(p1, v1, v1))
+                )));
+
+                var modelSeed = ModelSeed.builder(4)
+                                .seed(MultiObjectTranslator.COUNT_SYMBOL, builder -> builder
+                                                .reducedValue(CardinalityIntervals.ONE)
+                                                .put(Tuple.of(0), CardinalityIntervals.between(5, 9))
+                                                .put(Tuple.of(1), CardinalityIntervals.atLeast(3))
+                                                .put(Tuple.of(2), CardinalityIntervals.atMost(7)))
+                                .seed(person, builder -> builder.reducedValue(TruthValue.TRUE))
+                                .seed(friend, builder -> builder
+                                                .put(Tuple.of(0, 1), TruthValue.TRUE)
+                                                .put(Tuple.of(0, 2), TruthValue.TRUE)
+                                                .put(Tuple.of(0, 3), TruthValue.TRUE)
+                                                .put(Tuple.of(1, 0), TruthValue.TRUE)
+                                                .put(Tuple.of(1, 2), TruthValue.UNKNOWN)
+                                                .put(Tuple.of(1, 3), TruthValue.UNKNOWN)
+                                                .put(Tuple.of(2, 0), TruthValue.TRUE)
+                                                .put(Tuple.of(2, 1), TruthValue.ERROR))
+                                .build();
+
+                var resultSet = getResultSet(query, modelSeed);
+                assertThat(resultSet.get(Tuple.of(0)), is(4));
+                assertThat(resultSet.get(Tuple.of(1)), is(5));
+                assertThat(resultSet.get(Tuple.of(2)), is(8));
+                assertThat(resultSet.get(Tuple.of(3)), is(0));
+        }
+
+        @Test
+        void upperBoundDiagonalTest() {
+                var subQuery = Query.of("SubQuery", (builder, p1, p2, p3) -> builder.clause(
+                                friend.call(p1, p2),
+                                friend.call(p1, p3),
+                                not(friend.call(p2, p3))
+                ));
+                var query = Query.of("UpperBound", UpperCardinality.class, (builder, p1, output) -> builder
+                                .clause(v1 -> List.of(
+                                                must(person.call(p1)),
+                                                new CountUpperBoundLiteral(output, Concreteness.PARTIAL, subQuery.getDnf(),
+                                                                List.of(p1, v1, v1))
+                                )));
+
+                var modelSeed = ModelSeed.builder(4)
+                                .seed(MultiObjectTranslator.COUNT_SYMBOL, builder -> builder
+                                                .reducedValue(CardinalityIntervals.ONE)
+                                                .put(Tuple.of(0), CardinalityIntervals.between(5, 9))
+                                                .put(Tuple.of(1), CardinalityIntervals.atLeast(3))
+                                                .put(Tuple.of(2), CardinalityIntervals.atMost(7)))
+                                .seed(person, builder -> builder.reducedValue(TruthValue.TRUE))
+                                .seed(friend, builder -> builder
+                                                .put(Tuple.of(0, 1), TruthValue.TRUE)
+                                                .put(Tuple.of(0, 2), TruthValue.TRUE)
+                                                .put(Tuple.of(0, 3), TruthValue.TRUE)
+                                                .put(Tuple.of(1, 0), TruthValue.TRUE)
+                                                .put(Tuple.of(1, 2), TruthValue.UNKNOWN)
+                                                .put(Tuple.of(1, 3), TruthValue.UNKNOWN)
+                                                .put(Tuple.of(2, 0), TruthValue.TRUE)
+                                                .put(Tuple.of(2, 1), TruthValue.ERROR))
+                                .build();
+
+                var resultSet = getResultSet(query, modelSeed);
+                assertThat(resultSet.get(Tuple.of(0)), is(UpperCardinalities.UNBOUNDED));
+                assertThat(resultSet.get(Tuple.of(1)), is(UpperCardinalities.atMost(17)));
+                assertThat(resultSet.get(Tuple.of(2)), is(UpperCardinalities.atMost(9)));
+                assertThat(resultSet.get(Tuple.of(3)), is(UpperCardinalities.ZERO));
+        }
+
+        private static <T> ResultSet<T> getResultSet(Query<T> query, ModelSeed modelSeed) {
+                var personStorage = Symbol.of("Person", 1, TruthValue.class, TruthValue.FALSE);
+                var friendStorage = Symbol.of("friend", 2, TruthValue.class, TruthValue.FALSE);
+
+                var store = ModelStore.builder()
+                                .with(ViatraModelQueryAdapter.builder()
+                                                .query(query))
+                                .with(ReasoningAdapter.builder())
+                                .with(new MultiObjectTranslator())
+                                .with(PartialRelationTranslator.of(person)
+                                                .symbol(personStorage))
+                                .with(PartialRelationTranslator.of(friend)
+                                                .symbol(friendStorage))
+                                .build();
+
+                var model = store.getAdapter(ReasoningStoreAdapter.class).createInitialModel(modelSeed);
+                return model.getAdapter(ModelQueryAdapter.class).getResultSet(query);
+        }
+}
diff --git a/subprojects/store/src/main/java/tools/refinery/store/representation/cardinality/CardinalityDomain.java b/subprojects/store/src/main/java/tools/refinery/store/representation/cardinality/CardinalityDomain.java
new file mode 100644
index 00000000..7ae2d935
--- /dev/null
+++ b/subprojects/store/src/main/java/tools/refinery/store/representation/cardinality/CardinalityDomain.java
@@ -0,0 +1,68 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.representation.cardinality;
+
+import tools.refinery.store.representation.AbstractDomain;
+
+import java.util.Optional;
+
+// Singleton pattern, because there is only one domain for truth values.
+@SuppressWarnings("squid:S6548")
+public class CardinalityDomain implements AbstractDomain<CardinalityInterval, Integer> {
+        public static final CardinalityDomain INSTANCE = new CardinalityDomain();
+
+        private CardinalityDomain() {
+        }
+
+        @Override
+        public Class<CardinalityInterval> abstractType() {
+                return CardinalityInterval.class;
+        }
+
+        @Override
+        public Class<Integer> concreteType() {
+                return Integer.class;
+        }
+
+        @Override
+        public CardinalityInterval toAbstract(Integer concreteValue) {
+                return CardinalityIntervals.exactly(concreteValue);
+        }
+
+        @Override
+        public Optional<Integer> toConcrete(CardinalityInterval abstractValue) {
+                return isConcrete(abstractValue) ? Optional.of(abstractValue.lowerBound()) : Optional.empty();
+        }
+
+        @Override
+        public boolean isConcrete(CardinalityInterval abstractValue) {
+                if (!(abstractValue instanceof NonEmptyCardinalityInterval nonEmptyValue) ||
+                                !((nonEmptyValue.upperBound()) instanceof FiniteUpperCardinality finiteUpperCardinality)) {
+                        return false;
+                }
+                return nonEmptyValue.lowerBound() == finiteUpperCardinality.finiteUpperBound();
+        }
+
+        @Override
+        public CardinalityInterval commonRefinement(CardinalityInterval leftValue, CardinalityInterval rightValue) {
+                return leftValue.meet(rightValue);
+        }
+
+        @Override
+        public CardinalityInterval commonAncestor(CardinalityInterval leftValue, CardinalityInterval rightValue) {
+                return leftValue.join(rightValue);
+        }
+
+        @Override
+        public CardinalityInterval unknown() {
+                return CardinalityIntervals.SET;
+        }
+
+        @Override
+        public boolean isError(CardinalityInterval abstractValue) {
+                return abstractValue.isEmpty();
+        }
+}
diff --git a/subprojects/store/src/main/java/tools/refinery/store/representation/cardinality/CardinalityIntervals.java b/subprojects/store/src/main/java/tools/refinery/store/representation/cardinality/CardinalityIntervals.java
index ad16a3e8..855fd248 100644
--- a/subprojects/store/src/main/java/tools/refinery/store/representation/cardinality/CardinalityIntervals.java
+++ b/subprojects/store/src/main/java/tools/refinery/store/representation/cardinality/CardinalityIntervals.java
@@ -30,7 +30,7 @@ public final class CardinalityIntervals {
         }
 
         public static CardinalityInterval between(int lowerBound, int upperBound) {
-                return between(lowerBound, UpperCardinalities.valueOf(upperBound));
+                return between(lowerBound, UpperCardinalities.atMost(upperBound));
         }
 
         public static CardinalityInterval atMost(UpperCardinality upperBound) {
@@ -38,7 +38,7 @@ public final class CardinalityIntervals {
         }
 
         public static CardinalityInterval atMost(int upperBound) {
-                return atMost(UpperCardinalities.valueOf(upperBound));
+                return atMost(UpperCardinalities.atMost(upperBound));
         }
 
         public static CardinalityInterval atLeast(int lowerBound) {
@@ -46,6 +46,6 @@ public final class CardinalityIntervals {
         }
 
         public static CardinalityInterval exactly(int lowerBound) {
-                return new NonEmptyCardinalityInterval(lowerBound, UpperCardinalities.valueOf(lowerBound));
+                return new NonEmptyCardinalityInterval(lowerBound, UpperCardinalities.atMost(lowerBound));
         }
 }
diff --git a/subprojects/store/src/main/java/tools/refinery/store/representation/cardinality/FiniteUpperCardinality.java b/subprojects/store/src/main/java/tools/refinery/store/representation/cardinality/FiniteUpperCardinality.java
index acd82beb..088e3925 100644
--- a/subprojects/store/src/main/java/tools/refinery/store/representation/cardinality/FiniteUpperCardinality.java
+++ b/subprojects/store/src/main/java/tools/refinery/store/representation/cardinality/FiniteUpperCardinality.java
@@ -59,7 +59,7 @@ public record FiniteUpperCardinality(int finiteUpperBound) implements UpperCardi
 
         private UpperCardinality lift(@NotNull UpperCardinality other, IntBinaryOperator operator) {
                 if (other instanceof FiniteUpperCardinality finiteUpperCardinality) {
-                        return UpperCardinalities.valueOf(operator.applyAsInt(finiteUpperBound,
+                        return UpperCardinalities.atMost(operator.applyAsInt(finiteUpperBound,
                                         finiteUpperCardinality.finiteUpperBound));
                 }
                 if (other instanceof UnboundedUpperCardinality) {
diff --git a/subprojects/store/src/main/java/tools/refinery/store/representation/cardinality/UpperCardinalities.java b/subprojects/store/src/main/java/tools/refinery/store/representation/cardinality/UpperCardinalities.java
index 1e18dde0..17d1b292 100644
--- a/subprojects/store/src/main/java/tools/refinery/store/representation/cardinality/UpperCardinalities.java
+++ b/subprojects/store/src/main/java/tools/refinery/store/representation/cardinality/UpperCardinalities.java
@@ -26,7 +26,7 @@ public final class UpperCardinalities {
                 throw new IllegalStateException("This is a static utility class and should not be instantiated directly");
         }
 
-        public static UpperCardinality valueOf(int upperBound) {
+        public static UpperCardinality atMost(int upperBound) {
                 if (upperBound < 0) {
                         return UNBOUNDED;
                 }
diff --git a/subprojects/store/src/main/java/tools/refinery/store/representation/cardinality/UpperCardinality.java b/subprojects/store/src/main/java/tools/refinery/store/representation/cardinality/UpperCardinality.java
index 5600ab4c..3f0db028 100644
--- a/subprojects/store/src/main/java/tools/refinery/store/representation/cardinality/UpperCardinality.java
+++ b/subprojects/store/src/main/java/tools/refinery/store/representation/cardinality/UpperCardinality.java
@@ -27,6 +27,6 @@ public sealed interface UpperCardinality extends Comparable<UpperCardinality> pe
         int compareToInt(int value);
 
         static UpperCardinality of(int upperBound) {
-                return UpperCardinalities.valueOf(upperBound);
+                return UpperCardinalities.atMost(upperBound);
         }
 }
diff --git a/subprojects/store/src/test/java/tools/refinery/store/representation/cardinality/UpperCardinalitiesTest.java b/subprojects/store/src/test/java/tools/refinery/store/representation/cardinality/UpperCardinalitiesTest.java
index e61f7b36..e403eec2 100644
--- a/subprojects/store/src/test/java/tools/refinery/store/representation/cardinality/UpperCardinalitiesTest.java
+++ b/subprojects/store/src/test/java/tools/refinery/store/representation/cardinality/UpperCardinalitiesTest.java
@@ -8,9 +8,6 @@ package tools.refinery.store.representation.cardinality;
 import org.junit.jupiter.api.Test;
 import org.junit.jupiter.params.ParameterizedTest;
 import org.junit.jupiter.params.provider.ValueSource;
-import tools.refinery.store.representation.cardinality.FiniteUpperCardinality;
-import tools.refinery.store.representation.cardinality.UnboundedUpperCardinality;
-import tools.refinery.store.representation.cardinality.UpperCardinalities;
 
 import static org.hamcrest.MatcherAssert.assertThat;
 import static org.hamcrest.Matchers.equalTo;
@@ -20,14 +17,14 @@ class UpperCardinalitiesTest {
         @ParameterizedTest
         @ValueSource(ints = {0, 1, 255, 256, 1000, Integer.MAX_VALUE})
         void valueOfBoundedTest(int value) {
-                var upperCardinality = UpperCardinalities.valueOf(value);
+                var upperCardinality = UpperCardinalities.atMost(value);
                 assertThat(upperCardinality, instanceOf(FiniteUpperCardinality.class));
                 assertThat(((FiniteUpperCardinality) upperCardinality).finiteUpperBound(), equalTo(value));
         }
 
         @Test
         void valueOfUnboundedTest() {
-                var upperCardinality = UpperCardinalities.valueOf(-1);
+                var upperCardinality = UpperCardinalities.atMost(-1);
                 assertThat(upperCardinality, instanceOf(UnboundedUpperCardinality.class));
         }
 }