refactor(logic): abstract domain interface

Require all abstract domain elements to implement the AbstractValue interface.
graphs4value · Apr 7, 2024 · a636a86 · a636a86
1 parent 046087c
commit a636a86
Show file tree

Hide file tree

Showing 41 changed files with 255 additions and 192 deletions.
diff --git a/subprojects/generator/src/main/java/tools/refinery/generator/ModelFacade.java b/subprojects/generator/src/main/java/tools/refinery/generator/ModelFacade.java
@@ -6,6 +6,7 @@
 package tools.refinery.generator;
 
 import tools.refinery.language.semantics.ProblemTrace;
+import tools.refinery.logic.AbstractValue;
 import tools.refinery.store.model.Model;
 import tools.refinery.store.model.ModelStore;
 import tools.refinery.store.reasoning.ReasoningAdapter;
@@ -52,7 +53,8 @@ public Concreteness getConcreteness() {
 		return concreteness;
 	}
 
-	public <A, C> PartialInterpretation<A, C> getPartialInterpretation(PartialSymbol<A, C> partialSymbol) {
+	public <A extends AbstractValue<A, C>, C> PartialInterpretation<A, C> getPartialInterpretation(
+			PartialSymbol<A, C> partialSymbol) {
 		return reasoningAdapter.getPartialInterpretation(concreteness, partialSymbol);
 	}
 }
diff --git a/subprojects/generator/src/main/java/tools/refinery/generator/ModelGenerator.java b/subprojects/generator/src/main/java/tools/refinery/generator/ModelGenerator.java
@@ -9,6 +9,7 @@
 import tools.refinery.language.model.problem.Problem;
 import tools.refinery.language.semantics.ProblemTrace;
 import tools.refinery.language.semantics.SolutionSerializer;
+import tools.refinery.logic.AbstractValue;
 import tools.refinery.store.dse.strategy.BestFirstStoreManager;
 import tools.refinery.store.map.Version;
 import tools.refinery.store.model.ModelStore;
@@ -24,7 +25,7 @@ public class ModelGenerator extends ModelFacade {
 	private boolean lastGenerationSuccessful;
 
 	ModelGenerator(ProblemTrace problemTrace, ModelStore store, ModelSeed modelSeed,
-                          Provider<SolutionSerializer> solutionSerializerProvider) {
+				   Provider<SolutionSerializer> solutionSerializerProvider) {
 		super(problemTrace, store, modelSeed, Concreteness.CANDIDATE);
 		this.solutionSerializerProvider = solutionSerializerProvider;
 		initialVersion = getModel().commit();
@@ -66,7 +67,8 @@ public void generate() {
 	}
 
 	@Override
-	public <A, C> PartialInterpretation<A, C> getPartialInterpretation(PartialSymbol<A, C> partialSymbol) {
+	public <A extends AbstractValue<A, C>, C> PartialInterpretation<A, C> getPartialInterpretation(
+			PartialSymbol<A, C> partialSymbol) {
 		checkSuccessfulGeneration();
 		return super.getPartialInterpretation(partialSymbol);
 	}

diff --git a/...semantics/src/main/java/tools/refinery/language/semantics/internal/DecisionTreeValue.java b/...semantics/src/main/java/tools/refinery/language/semantics/internal/DecisionTreeValue.java
@@ -25,7 +25,7 @@ public TruthValue getTruthValue() {
 	}
 
 	public TruthValue merge(TruthValue other) {
-		return truthValue == null ? other : truthValue.merge(other);
+		return truthValue == null ? other : truthValue.meet(other);
 	}
 
 	public DecisionTreeValue overwrite(DecisionTreeValue other) {

diff --git a/...uage-semantics/src/main/java/tools/refinery/language/semantics/internal/TerminalNode.java b/...uage-semantics/src/main/java/tools/refinery/language/semantics/internal/TerminalNode.java
@@ -48,7 +48,7 @@ public void mergeValue(int level, Tuple tuple, TruthValue value) {
 	protected void mergeAllValues(int nextLevel, Tuple tuple, TruthValue value) {
 		otherwise = DecisionTreeValue.fromTruthValue(otherwise.merge(value));
 		children = IntObjectMaps.mutable.from(children.keyValuesView(), IntObjectPair::getOne,
-				pair -> pair.getTwo().merge(value));
+				pair -> pair.getTwo().meet(value));
 		reduceChildren();
 	}
 

diff --git 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
@@ -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/.../logic/src/main/java/tools/refinery/logic/term/cardinalityinterval/CardinalityDomain.java b/.../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<Integer> concreteType() {
 	}
 
 	@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/...ogic/src/main/java/tools/refinery/logic/term/cardinalityinterval/CardinalityInterval.java b/...ogic/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/...src/main/java/tools/refinery/logic/term/cardinalityinterval/EmptyCardinalityInterval.java b/...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,15 +19,27 @@ private EmptyCardinalityInterval() {
 	}
 
 	@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/.../main/java/tools/refinery/logic/term/cardinalityinterval/NonEmptyCardinalityInterval.java b/.../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,10 +25,36 @@ 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);