From 0f77d138484aaa508ba60ebba4b3b2b329df9dc3 Mon Sep 17 00:00:00 2001 From: Kristóf Marussy Date: Wed, 19 Jul 2023 01:51:35 +0200 Subject: feat: multi-object based EQUALS and EXISTS Adds translator for EQUALS and EXISTS symbols based on the multi-object formalism. Only diagonal equality links are supported (e.g., distinct nodes may not be EQUALS with each other). Also introduces initial model seeds to separate partial interpreter construction and graph initialization better. --- .../store/representation/cardinality/CardinalityInterval.java | 2 ++ .../representation/cardinality/EmptyCardinalityInterval.java | 7 +++++++ .../representation/cardinality/FiniteUpperCardinality.java | 10 ++++++++++ .../cardinality/NonEmptyCardinalityInterval.java | 10 ++++++++++ .../representation/cardinality/UnboundedUpperCardinality.java | 9 +++++++++ .../store/representation/cardinality/UpperCardinality.java | 5 +++++ 6 files changed, 43 insertions(+) (limited to 'subprojects/store/src') 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(); @@ -42,6 +44,11 @@ public final class EmptyCardinalityInterval implements CardinalityInterval { return this; } + @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; @@ -21,6 +22,15 @@ public record FiniteUpperCardinality(int finiteUpperBound) implements UpperCardi return lift(other, Integer::sum); } + @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 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(); @@ -19,11 +21,18 @@ public final class UnboundedUpperCardinality implements UpperCardinality { return this; } + @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 permits FiniteUpperCardinality, UnboundedUpperCardinality { default UpperCardinality min(UpperCardinality other) { @@ -17,6 +19,9 @@ public sealed interface UpperCardinality extends Comparable pe UpperCardinality add(UpperCardinality other); + @Nullable + UpperCardinality take(int count); + UpperCardinality multiply(UpperCardinality other); int compareToInt(int value); -- cgit v1.2.3-54-g00ecf