feat: concrete count in partial models

10 files changed, 613 insertions, 20 deletions

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);
+        }
+}