6 files changed, 43 insertions, 0 deletions

diff --git a/subprojects/store/src/main/java/tools/refinery/store/representation/cardinality/CardinalityInterval.java b/subprojects/store/src/main/java/tools/refinery/store/representation/cardinality/CardinalityInterval.java
index 704ca2fc..b20c685a 100644
--- a/subprojects/store/src/main/java/tools/refinery/store/representation/cardinality/CardinalityInterval.java
+++ b/subprojects/store/src/main/java/tools/refinery/store/representation/cardinality/CardinalityInterval.java
@@ -18,6 +18,8 @@ public sealed interface CardinalityInterval permits NonEmptyCardinalityInterval,
 
         CardinalityInterval add(CardinalityInterval other);
 
+        CardinalityInterval take(int count);
+
         CardinalityInterval multiply(CardinalityInterval other);
 
         CardinalityInterval meet(CardinalityInterval other);
diff --git a/subprojects/store/src/main/java/tools/refinery/store/representation/cardinality/EmptyCardinalityInterval.java b/subprojects/store/src/main/java/tools/refinery/store/representation/cardinality/EmptyCardinalityInterval.java
index 49911c29..9e371e21 100644
--- a/subprojects/store/src/main/java/tools/refinery/store/representation/cardinality/EmptyCardinalityInterval.java
+++ b/subprojects/store/src/main/java/tools/refinery/store/representation/cardinality/EmptyCardinalityInterval.java
@@ -5,6 +5,8 @@
  */
 package tools.refinery.store.representation.cardinality;
 
+// Singleton implementation, because there is only a single empty interval.
+@SuppressWarnings("squid:S6548")
 public final class EmptyCardinalityInterval implements CardinalityInterval {
         static final EmptyCardinalityInterval INSTANCE = new EmptyCardinalityInterval();
 
@@ -43,6 +45,11 @@ public final class EmptyCardinalityInterval implements CardinalityInterval {
         }
 
         @Override
+        public CardinalityInterval take(int count) {
+                return this;
+        }
+
+        @Override
         public CardinalityInterval multiply(CardinalityInterval other) {
                 return this;
         }
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 82afdbbc..acd82beb 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
@@ -6,6 +6,7 @@
 package tools.refinery.store.representation.cardinality;
 
 import org.jetbrains.annotations.NotNull;
+import org.jetbrains.annotations.Nullable;
 
 import java.util.function.IntBinaryOperator;
 
@@ -22,6 +23,15 @@ public record FiniteUpperCardinality(int finiteUpperBound) implements UpperCardi
         }
 
         @Override
+        @Nullable
+        public UpperCardinality take(int count) {
+                if (finiteUpperBound < count) {
+                        return null;
+                }
+                return new FiniteUpperCardinality(finiteUpperBound - count);
+        }
+
+        @Override
         public UpperCardinality multiply(UpperCardinality other) {
                 return lift(other, (a, b) -> a * b);
         }
diff --git a/subprojects/store/src/main/java/tools/refinery/store/representation/cardinality/NonEmptyCardinalityInterval.java b/subprojects/store/src/main/java/tools/refinery/store/representation/cardinality/NonEmptyCardinalityInterval.java
index 38bd53bf..2e7780da 100644
--- a/subprojects/store/src/main/java/tools/refinery/store/representation/cardinality/NonEmptyCardinalityInterval.java
+++ b/subprojects/store/src/main/java/tools/refinery/store/representation/cardinality/NonEmptyCardinalityInterval.java
@@ -53,6 +53,16 @@ public record NonEmptyCardinalityInterval(int lowerBound, UpperCardinality upper
                 return lift(other, Math::min, UpperCardinality::max, this);
         }
 
+        @Override
+        public CardinalityInterval take(int count) {
+                int newLowerBound = Math.max(lowerBound - count, 0);
+                var newUpperBound = upperBound.take(count);
+                if (newUpperBound == null) {
+                        return CardinalityIntervals.ERROR;
+                }
+                return CardinalityIntervals.between(newLowerBound, newUpperBound);
+        }
+
         private CardinalityInterval lift(CardinalityInterval other, IntBinaryOperator lowerOperator,
                                                                          BinaryOperator<UpperCardinality> upperOperator,
                                                                          CardinalityInterval whenEmpty) {
diff --git a/subprojects/store/src/main/java/tools/refinery/store/representation/cardinality/UnboundedUpperCardinality.java b/subprojects/store/src/main/java/tools/refinery/store/representation/cardinality/UnboundedUpperCardinality.java
index a5634020..e3a334cd 100644
--- a/subprojects/store/src/main/java/tools/refinery/store/representation/cardinality/UnboundedUpperCardinality.java
+++ b/subprojects/store/src/main/java/tools/refinery/store/representation/cardinality/UnboundedUpperCardinality.java
@@ -7,6 +7,8 @@ package tools.refinery.store.representation.cardinality;
 
 import org.jetbrains.annotations.NotNull;
 
+// Singleton implementation, because there is only a single countable infinity.
+@SuppressWarnings("squid:S6548")
 public final class UnboundedUpperCardinality implements UpperCardinality {
         static final UnboundedUpperCardinality INSTANCE = new UnboundedUpperCardinality();
 
@@ -20,10 +22,17 @@ public final class UnboundedUpperCardinality implements UpperCardinality {
         }
 
         @Override
+        public UpperCardinality take(int count) {
+                return this;
+        }
+
+        @Override
         public UpperCardinality multiply(UpperCardinality other) {
                 return this;
         }
 
+        // This should always be greater than any finite cardinality.
+        @SuppressWarnings("ComparatorMethodParameterNotUsed")
         @Override
         public int compareTo(@NotNull UpperCardinality upperCardinality) {
                 if (upperCardinality instanceof FiniteUpperCardinality) {
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 5dbaa922..5600ab4c 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
@@ -5,6 +5,8 @@
  */
 package tools.refinery.store.representation.cardinality;
 
+import org.jetbrains.annotations.Nullable;
+
 public sealed interface UpperCardinality extends Comparable<UpperCardinality> permits FiniteUpperCardinality,
                 UnboundedUpperCardinality {
         default UpperCardinality min(UpperCardinality other) {
@@ -17,6 +19,9 @@ public sealed interface UpperCardinality extends Comparable<UpperCardinality> pe
 
         UpperCardinality add(UpperCardinality other);
 
+        @Nullable
+        UpperCardinality take(int count);
+
         UpperCardinality multiply(UpperCardinality other);
 
         int compareToInt(int value);