diff options
author | 2023-07-19 01:51:35 +0200 | |
---|---|---|
committer | 2023-07-20 15:54:50 +0200 | |
commit | 0f77d138484aaa508ba60ebba4b3b2b329df9dc3 (patch) | |
tree | 3b34725e4e4fa00ffd65e5d204cb58b9fc0d4acc /subprojects/store/src/main/java/tools | |
parent | feat: basic partial interpretation infrastructure (diff) | |
download | refinery-0f77d138484aaa508ba60ebba4b3b2b329df9dc3.tar.gz refinery-0f77d138484aaa508ba60ebba4b3b2b329df9dc3.tar.zst refinery-0f77d138484aaa508ba60ebba4b3b2b329df9dc3.zip |
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.
Diffstat (limited to 'subprojects/store/src/main/java/tools')
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, | |||
18 | 18 | ||
19 | CardinalityInterval add(CardinalityInterval other); | 19 | CardinalityInterval add(CardinalityInterval other); |
20 | 20 | ||
21 | CardinalityInterval take(int count); | ||
22 | |||
21 | CardinalityInterval multiply(CardinalityInterval other); | 23 | CardinalityInterval multiply(CardinalityInterval other); |
22 | 24 | ||
23 | CardinalityInterval meet(CardinalityInterval other); | 25 | 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 @@ | |||
5 | */ | 5 | */ |
6 | package tools.refinery.store.representation.cardinality; | 6 | package tools.refinery.store.representation.cardinality; |
7 | 7 | ||
8 | // Singleton implementation, because there is only a single empty interval. | ||
9 | @SuppressWarnings("squid:S6548") | ||
8 | public final class EmptyCardinalityInterval implements CardinalityInterval { | 10 | public final class EmptyCardinalityInterval implements CardinalityInterval { |
9 | static final EmptyCardinalityInterval INSTANCE = new EmptyCardinalityInterval(); | 11 | static final EmptyCardinalityInterval INSTANCE = new EmptyCardinalityInterval(); |
10 | 12 | ||
@@ -43,6 +45,11 @@ public final class EmptyCardinalityInterval implements CardinalityInterval { | |||
43 | } | 45 | } |
44 | 46 | ||
45 | @Override | 47 | @Override |
48 | public CardinalityInterval take(int count) { | ||
49 | return this; | ||
50 | } | ||
51 | |||
52 | @Override | ||
46 | public CardinalityInterval multiply(CardinalityInterval other) { | 53 | public CardinalityInterval multiply(CardinalityInterval other) { |
47 | return this; | 54 | return this; |
48 | } | 55 | } |
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 @@ | |||
6 | package tools.refinery.store.representation.cardinality; | 6 | package tools.refinery.store.representation.cardinality; |
7 | 7 | ||
8 | import org.jetbrains.annotations.NotNull; | 8 | import org.jetbrains.annotations.NotNull; |
9 | import org.jetbrains.annotations.Nullable; | ||
9 | 10 | ||
10 | import java.util.function.IntBinaryOperator; | 11 | import java.util.function.IntBinaryOperator; |
11 | 12 | ||
@@ -22,6 +23,15 @@ public record FiniteUpperCardinality(int finiteUpperBound) implements UpperCardi | |||
22 | } | 23 | } |
23 | 24 | ||
24 | @Override | 25 | @Override |
26 | @Nullable | ||
27 | public UpperCardinality take(int count) { | ||
28 | if (finiteUpperBound < count) { | ||
29 | return null; | ||
30 | } | ||
31 | return new FiniteUpperCardinality(finiteUpperBound - count); | ||
32 | } | ||
33 | |||
34 | @Override | ||
25 | public UpperCardinality multiply(UpperCardinality other) { | 35 | public UpperCardinality multiply(UpperCardinality other) { |
26 | return lift(other, (a, b) -> a * b); | 36 | return lift(other, (a, b) -> a * b); |
27 | } | 37 | } |
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 | |||
53 | return lift(other, Math::min, UpperCardinality::max, this); | 53 | return lift(other, Math::min, UpperCardinality::max, this); |
54 | } | 54 | } |
55 | 55 | ||
56 | @Override | ||
57 | public CardinalityInterval take(int count) { | ||
58 | int newLowerBound = Math.max(lowerBound - count, 0); | ||
59 | var newUpperBound = upperBound.take(count); | ||
60 | if (newUpperBound == null) { | ||
61 | return CardinalityIntervals.ERROR; | ||
62 | } | ||
63 | return CardinalityIntervals.between(newLowerBound, newUpperBound); | ||
64 | } | ||
65 | |||
56 | private CardinalityInterval lift(CardinalityInterval other, IntBinaryOperator lowerOperator, | 66 | private CardinalityInterval lift(CardinalityInterval other, IntBinaryOperator lowerOperator, |
57 | BinaryOperator<UpperCardinality> upperOperator, | 67 | BinaryOperator<UpperCardinality> upperOperator, |
58 | CardinalityInterval whenEmpty) { | 68 | 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; | |||
7 | 7 | ||
8 | import org.jetbrains.annotations.NotNull; | 8 | import org.jetbrains.annotations.NotNull; |
9 | 9 | ||
10 | // Singleton implementation, because there is only a single countable infinity. | ||
11 | @SuppressWarnings("squid:S6548") | ||
10 | public final class UnboundedUpperCardinality implements UpperCardinality { | 12 | public final class UnboundedUpperCardinality implements UpperCardinality { |
11 | static final UnboundedUpperCardinality INSTANCE = new UnboundedUpperCardinality(); | 13 | static final UnboundedUpperCardinality INSTANCE = new UnboundedUpperCardinality(); |
12 | 14 | ||
@@ -20,10 +22,17 @@ public final class UnboundedUpperCardinality implements UpperCardinality { | |||
20 | } | 22 | } |
21 | 23 | ||
22 | @Override | 24 | @Override |
25 | public UpperCardinality take(int count) { | ||
26 | return this; | ||
27 | } | ||
28 | |||
29 | @Override | ||
23 | public UpperCardinality multiply(UpperCardinality other) { | 30 | public UpperCardinality multiply(UpperCardinality other) { |
24 | return this; | 31 | return this; |
25 | } | 32 | } |
26 | 33 | ||
34 | // This should always be greater than any finite cardinality. | ||
35 | @SuppressWarnings("ComparatorMethodParameterNotUsed") | ||
27 | @Override | 36 | @Override |
28 | public int compareTo(@NotNull UpperCardinality upperCardinality) { | 37 | public int compareTo(@NotNull UpperCardinality upperCardinality) { |
29 | if (upperCardinality instanceof FiniteUpperCardinality) { | 38 | 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 @@ | |||
5 | */ | 5 | */ |
6 | package tools.refinery.store.representation.cardinality; | 6 | package tools.refinery.store.representation.cardinality; |
7 | 7 | ||
8 | import org.jetbrains.annotations.Nullable; | ||
9 | |||
8 | public sealed interface UpperCardinality extends Comparable<UpperCardinality> permits FiniteUpperCardinality, | 10 | public sealed interface UpperCardinality extends Comparable<UpperCardinality> permits FiniteUpperCardinality, |
9 | UnboundedUpperCardinality { | 11 | UnboundedUpperCardinality { |
10 | default UpperCardinality min(UpperCardinality other) { | 12 | default UpperCardinality min(UpperCardinality other) { |
@@ -17,6 +19,9 @@ public sealed interface UpperCardinality extends Comparable<UpperCardinality> pe | |||
17 | 19 | ||
18 | UpperCardinality add(UpperCardinality other); | 20 | UpperCardinality add(UpperCardinality other); |
19 | 21 | ||
22 | @Nullable | ||
23 | UpperCardinality take(int count); | ||
24 | |||
20 | UpperCardinality multiply(UpperCardinality other); | 25 | UpperCardinality multiply(UpperCardinality other); |
21 | 26 | ||
22 | int compareToInt(int value); | 27 | int compareToInt(int value); |