8 files changed, 144 insertions, 114 deletions

diff --git a/subprojects/logic/src/main/java/tools/refinery/logic/AbstractDomain.java b/subprojects/logic/src/main/java/tools/refinery/logic/AbstractDomain.java
index 607caa48..0b4d87d2 100644
--- a/subprojects/logic/src/main/java/tools/refinery/logic/AbstractDomain.java
+++ b/subprojects/logic/src/main/java/tools/refinery/logic/AbstractDomain.java
@@ -1,37 +1,20 @@
 /*
- * SPDX-FileCopyrightText: 2021-2023 The Refinery Authors <https://refinery.tools/>
+ * SPDX-FileCopyrightText: 2021-2024 The Refinery Authors <https://refinery.tools/>
  *
  * SPDX-License-Identifier: EPL-2.0
  */
 package tools.refinery.logic;
 
-import java.util.Objects;
-import java.util.Optional;
-
-public non-sealed interface AbstractDomain<A, C> extends AnyAbstractDomain {
+public non-sealed interface AbstractDomain<A extends AbstractValue<A, C>, C> extends AnyAbstractDomain {
         @Override
         Class<A> abstractType();
 
         @Override
         Class<C> concreteType();
 
-        A toAbstract(C concreteValue);
-
-        Optional<C> toConcrete(A abstractValue);
-
-        default boolean isConcrete(A abstractValue) {
-                return toConcrete(abstractValue).isPresent();
-        }
-
-        default boolean isRefinement(A originalValue, A refinedValue) {
-                return Objects.equals(commonRefinement(originalValue, refinedValue), refinedValue);
-        }
-
-        A commonRefinement(A leftValue, A rightValue);
-
-        A commonAncestor(A leftValue, A rightValue);
-
         A unknown();
 
-        boolean isError(A abstractValue);
+        A error();
+
+        A toAbstract(C concreteValue);
 }
diff --git a/subprojects/logic/src/main/java/tools/refinery/logic/AbstractValue.java b/subprojects/logic/src/main/java/tools/refinery/logic/AbstractValue.java
new file mode 100644
index 00000000..0b5e0d01
--- /dev/null
+++ b/subprojects/logic/src/main/java/tools/refinery/logic/AbstractValue.java
@@ -0,0 +1,32 @@
+/*
+ * SPDX-FileCopyrightText: 2024 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.logic;
+
+import org.jetbrains.annotations.Nullable;
+
+public interface AbstractValue<A extends AbstractValue<A, C>, C> {
+        @Nullable
+        C getConcrete();
+
+        default boolean isConcrete() {
+                return getConcrete() == null;
+        }
+
+        @Nullable
+        C getArbitrary();
+
+        default boolean isError() {
+                return getArbitrary() == null;
+        }
+
+        A join(A other);
+
+        A meet(A other);
+
+        default boolean isRefinementOf(A other) {
+                return equals(meet(other));
+        }
+}
diff --git a/subprojects/logic/src/main/java/tools/refinery/logic/term/cardinalityinterval/CardinalityDomain.java b/subprojects/logic/src/main/java/tools/refinery/logic/term/cardinalityinterval/CardinalityDomain.java
index 508a454b..29775615 100644
--- a/subprojects/logic/src/main/java/tools/refinery/logic/term/cardinalityinterval/CardinalityDomain.java
+++ b/subprojects/logic/src/main/java/tools/refinery/logic/term/cardinalityinterval/CardinalityDomain.java
@@ -5,11 +5,8 @@
  */
 package tools.refinery.logic.term.cardinalityinterval;
 
-import tools.refinery.logic.term.uppercardinality.FiniteUpperCardinality;
 import tools.refinery.logic.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> {
@@ -29,41 +26,17 @@ public class CardinalityDomain implements AbstractDomain<CardinalityInterval, In
         }
 
         @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);
+        public CardinalityInterval unknown() {
+                return CardinalityIntervals.SET;
         }
 
         @Override
-        public CardinalityInterval unknown() {
-                return CardinalityIntervals.SET;
+        public CardinalityInterval error() {
+                return CardinalityIntervals.ERROR;
         }
 
         @Override
-        public boolean isError(CardinalityInterval abstractValue) {
-                return abstractValue.isEmpty();
+        public CardinalityInterval toAbstract(Integer concreteValue) {
+                return CardinalityIntervals.exactly(concreteValue);
         }
 }
diff --git a/subprojects/logic/src/main/java/tools/refinery/logic/term/cardinalityinterval/CardinalityInterval.java b/subprojects/logic/src/main/java/tools/refinery/logic/term/cardinalityinterval/CardinalityInterval.java
index dbf30def..996ebde5 100644
--- a/subprojects/logic/src/main/java/tools/refinery/logic/term/cardinalityinterval/CardinalityInterval.java
+++ b/subprojects/logic/src/main/java/tools/refinery/logic/term/cardinalityinterval/CardinalityInterval.java
@@ -5,15 +5,15 @@
  */
 package tools.refinery.logic.term.cardinalityinterval;
 
+import tools.refinery.logic.AbstractValue;
 import tools.refinery.logic.term.uppercardinality.UpperCardinality;
 
-public sealed interface CardinalityInterval permits NonEmptyCardinalityInterval, EmptyCardinalityInterval {
+public sealed interface CardinalityInterval extends AbstractValue<CardinalityInterval, Integer>
+                permits NonEmptyCardinalityInterval, EmptyCardinalityInterval {
         int lowerBound();
 
         UpperCardinality upperBound();
 
-        boolean isEmpty();
-
         CardinalityInterval min(CardinalityInterval other);
 
         CardinalityInterval max(CardinalityInterval other);
@@ -23,8 +23,4 @@ public sealed interface CardinalityInterval permits NonEmptyCardinalityInterval,
         CardinalityInterval take(int count);
 
         CardinalityInterval multiply(CardinalityInterval other);
-
-        CardinalityInterval meet(CardinalityInterval other);
-
-        CardinalityInterval join(CardinalityInterval other);
 }
diff --git a/subprojects/logic/src/main/java/tools/refinery/logic/term/cardinalityinterval/EmptyCardinalityInterval.java b/subprojects/logic/src/main/java/tools/refinery/logic/term/cardinalityinterval/EmptyCardinalityInterval.java
index 29a7f69d..8892b278 100644
--- a/subprojects/logic/src/main/java/tools/refinery/logic/term/cardinalityinterval/EmptyCardinalityInterval.java
+++ b/subprojects/logic/src/main/java/tools/refinery/logic/term/cardinalityinterval/EmptyCardinalityInterval.java
@@ -1,10 +1,11 @@
 /*
- * SPDX-FileCopyrightText: 2021-2023 The Refinery Authors <https://refinery.tools/>
+ * SPDX-FileCopyrightText: 2021-2024 The Refinery Authors <https://refinery.tools/>
  *
  * SPDX-License-Identifier: EPL-2.0
  */
 package tools.refinery.logic.term.cardinalityinterval;
 
+import org.jetbrains.annotations.Nullable;
 import tools.refinery.logic.term.uppercardinality.UpperCardinalities;
 import tools.refinery.logic.term.uppercardinality.UpperCardinality;
 
@@ -18,16 +19,28 @@ public final class EmptyCardinalityInterval implements CardinalityInterval {
         }
 
         @Override
-        public int lowerBound() {
-                return 1;
+        @Nullable
+        public Integer getConcrete() {
+                return null;
+        }
+
+        @Override
+        @Nullable
+        public Integer getArbitrary() {
+                return null;
         }
 
         @Override
-        public boolean isEmpty() {
+        public boolean isRefinementOf(CardinalityInterval other) {
                 return true;
         }
 
         @Override
+        public int lowerBound() {
+                return 1;
+        }
+
+        @Override
         public UpperCardinality upperBound() {
                 return UpperCardinalities.ZERO;
         }
diff --git a/subprojects/logic/src/main/java/tools/refinery/logic/term/cardinalityinterval/NonEmptyCardinalityInterval.java b/subprojects/logic/src/main/java/tools/refinery/logic/term/cardinalityinterval/NonEmptyCardinalityInterval.java
index 0919fc36..efe1464e 100644
--- a/subprojects/logic/src/main/java/tools/refinery/logic/term/cardinalityinterval/NonEmptyCardinalityInterval.java
+++ b/subprojects/logic/src/main/java/tools/refinery/logic/term/cardinalityinterval/NonEmptyCardinalityInterval.java
@@ -1,10 +1,12 @@
 /*
- * SPDX-FileCopyrightText: 2021-2023 The Refinery Authors <https://refinery.tools/>
+ * SPDX-FileCopyrightText: 2021-2024 The Refinery Authors <https://refinery.tools/>
  *
  * SPDX-License-Identifier: EPL-2.0
  */
 package tools.refinery.logic.term.cardinalityinterval;
 
+import org.jetbrains.annotations.NotNull;
+import org.jetbrains.annotations.Nullable;
 import tools.refinery.logic.term.uppercardinality.FiniteUpperCardinality;
 import tools.refinery.logic.term.uppercardinality.UpperCardinality;
 
@@ -23,11 +25,37 @@ public record NonEmptyCardinalityInterval(int lowerBound, UpperCardinality upper
         }
 
         @Override
-        public boolean isEmpty() {
+        @Nullable
+        public Integer getConcrete() {
+        return isConcrete() ? lowerBound : null;
+    }
+
+        @Override
+        public boolean isConcrete() {
+                return upperBound instanceof FiniteUpperCardinality finiteUpperCardinality &&
+                                finiteUpperCardinality.finiteUpperBound() == lowerBound;
+        }
+
+        @Override
+        @NotNull
+        public Integer getArbitrary() {
+                return lowerBound;
+        }
+
+        @Override
+        public boolean isError() {
                 return false;
         }
 
         @Override
+        public boolean isRefinementOf(CardinalityInterval other) {
+                if (!(other instanceof NonEmptyCardinalityInterval nonEmptyOther)) {
+                        return false;
+                }
+                return lowerBound >= nonEmptyOther.lowerBound() && upperBound.compareTo(nonEmptyOther.upperBound()) <= 0;
+        }
+
+        @Override
         public CardinalityInterval min(CardinalityInterval other) {
                 return lift(other, Math::min, UpperCardinality::min);
         }
diff --git a/subprojects/logic/src/main/java/tools/refinery/logic/term/truthvalue/TruthValue.java b/subprojects/logic/src/main/java/tools/refinery/logic/term/truthvalue/TruthValue.java
index bbdd3f97..59bdeab3 100644
--- a/subprojects/logic/src/main/java/tools/refinery/logic/term/truthvalue/TruthValue.java
+++ b/subprojects/logic/src/main/java/tools/refinery/logic/term/truthvalue/TruthValue.java
@@ -1,11 +1,14 @@
 /*
- * SPDX-FileCopyrightText: 2021-2023 The Refinery Authors <https://refinery.tools/>
+ * SPDX-FileCopyrightText: 2021-2024 The Refinery Authors <https://refinery.tools/>
  *
  * SPDX-License-Identifier: EPL-2.0
  */
 package tools.refinery.logic.term.truthvalue;
 
-public enum TruthValue {
+import org.jetbrains.annotations.Nullable;
+import tools.refinery.logic.AbstractValue;
+
+public enum TruthValue implements AbstractValue<TruthValue, Boolean> {
         TRUE("true"),
 
         FALSE("false"),
@@ -28,14 +31,41 @@ public enum TruthValue {
                 return value ? TRUE : FALSE;
         }
 
+        @Override
+        @Nullable
+        public Boolean getArbitrary() {
+                return switch (this) {
+                        case TRUE -> true;
+                        case FALSE, UNKNOWN -> false;
+                        case ERROR -> null;
+                };
+        }
+
+        @Override
+        public boolean isError() {
+                return this == ERROR;
+        }
+
         public boolean isConsistent() {
-                return this != ERROR;
+                return !isError();
         }
 
+
         public boolean isComplete() {
                 return this != UNKNOWN;
         }
 
+        @Override
+        @Nullable
+        public Boolean getConcrete() {
+                return switch (this) {
+                        case TRUE -> true;
+                        case FALSE -> false;
+                        default -> null;
+                };
+        }
+
+        @Override
         public boolean isConcrete() {
                 return this == TRUE || this == FALSE;
         }
@@ -56,15 +86,7 @@ public enum TruthValue {
                 };
         }
 
-        public TruthValue merge(TruthValue other) {
-                return switch (this) {
-                        case TRUE -> other == UNKNOWN || other == TRUE ? TRUE : ERROR;
-                        case FALSE -> other == UNKNOWN || other == FALSE ? FALSE : ERROR;
-                        case UNKNOWN -> other;
-                        case ERROR -> ERROR;
-                };
-        }
-
+        @Override
         public TruthValue join(TruthValue other) {
                 return switch (this) {
                         case TRUE -> other == ERROR || other == TRUE ? TRUE : UNKNOWN;
@@ -73,4 +95,14 @@ public enum TruthValue {
                         case ERROR -> other;
                 };
         }
+
+        @Override
+        public TruthValue meet(TruthValue other) {
+                return switch (this) {
+                        case TRUE -> other == UNKNOWN || other == TRUE ? TRUE : ERROR;
+                        case FALSE -> other == UNKNOWN || other == FALSE ? FALSE : ERROR;
+                        case UNKNOWN -> other;
+                        case ERROR -> ERROR;
+                };
+        }
 }
diff --git a/subprojects/logic/src/main/java/tools/refinery/logic/term/truthvalue/TruthValueDomain.java b/subprojects/logic/src/main/java/tools/refinery/logic/term/truthvalue/TruthValueDomain.java
index 443f744f..de8a89be 100644
--- a/subprojects/logic/src/main/java/tools/refinery/logic/term/truthvalue/TruthValueDomain.java
+++ b/subprojects/logic/src/main/java/tools/refinery/logic/term/truthvalue/TruthValueDomain.java
@@ -1,5 +1,5 @@
 /*
- * SPDX-FileCopyrightText: 2021-2023 The Refinery Authors <https://refinery.tools/>
+ * SPDX-FileCopyrightText: 2021-2024 The Refinery Authors <https://refinery.tools/>
  *
  * SPDX-License-Identifier: EPL-2.0
  */
@@ -7,8 +7,6 @@ package tools.refinery.logic.term.truthvalue;
 
 import tools.refinery.logic.AbstractDomain;
 
-import java.util.Optional;
-
 // Singleton pattern, because there is only one domain for truth values.
 @SuppressWarnings("squid:S6548")
 public final class TruthValueDomain implements AbstractDomain<TruthValue, Boolean> {
@@ -28,42 +26,17 @@ public final class TruthValueDomain implements AbstractDomain<TruthValue, Boolea
         }
 
         @Override
-        public TruthValue toAbstract(Boolean concreteValue) {
-                return TruthValue.toTruthValue(concreteValue);
-        }
-
-        @Override
-        public Optional<Boolean> toConcrete(TruthValue abstractValue) {
-                return switch (abstractValue) {
-                        case TRUE -> Optional.of(true);
-                        case FALSE -> Optional.of(false);
-                        default -> Optional.empty();
-                };
-        }
-
-        @Override
-        public boolean isConcrete(TruthValue abstractValue) {
-                return abstractValue.isConcrete();
-        }
-
-        @Override
-        public TruthValue commonRefinement(TruthValue leftValue, TruthValue rightValue) {
-                return leftValue.merge(rightValue);
+        public TruthValue unknown() {
+                return TruthValue.UNKNOWN;
         }
 
         @Override
-        public TruthValue commonAncestor(TruthValue leftValue, TruthValue rightValue) {
-                return leftValue.join(rightValue);
+        public TruthValue error() {
+                return TruthValue.ERROR;
         }
 
         @Override
-        public TruthValue unknown() {
-                return TruthValue.UNKNOWN;
-        }
-
-        @Override
-        public boolean isError(TruthValue abstractValue) {
-                return !abstractValue.isConsistent();
+        public TruthValue toAbstract(Boolean concreteValue) {
+                return TruthValue.toTruthValue(concreteValue);
         }
 }
-