From a636a86accf0ed00d0700e04ac0e1ce4f8cadf64 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Krist=C3=B3f=20Marussy?= Date: Sun, 10 Mar 2024 02:11:15 +0100 Subject: [PATCH] refactor(logic): abstract domain interface Require all abstract domain elements to implement the AbstractValue interface. --- .../tools/refinery/generator/ModelFacade.java | 4 +- .../refinery/generator/ModelGenerator.java | 6 +- .../semantics/internal/DecisionTreeValue.java | 2 +- .../semantics/internal/TerminalNode.java | 2 +- .../tools/refinery/logic/AbstractDomain.java | 27 ++------- .../tools/refinery/logic/AbstractValue.java | 32 +++++++++++ .../CardinalityDomain.java | 39 ++----------- .../CardinalityInterval.java | 10 +--- .../EmptyCardinalityInterval.java | 21 +++++-- .../NonEmptyCardinalityInterval.java | 32 ++++++++++- .../logic/term/truthvalue/TruthValue.java | 56 +++++++++++++++---- .../term/truthvalue/TruthValueDomain.java | 41 +++----------- .../CardinalityIntervalsTest.java | 4 +- .../reasoning/scope/ScopePropagator.java | 2 +- .../store/reasoning/ReasoningAdapter.java | 15 +++-- .../reasoning/actions/MergeActionLiteral.java | 5 +- .../actions/PartialActionLiterals.java | 5 +- .../internal/ReasoningAdapterImpl.java | 18 +++--- .../AbstractPartialInterpretation.java | 4 +- .../interpretation/PartialInterpretation.java | 7 ++- .../AbstractPartialInterpretationRefiner.java | 6 +- .../refinement/ConcreteSymbolRefiner.java | 10 ++-- .../PartialInterpretationRefiner.java | 8 ++- .../RefinementBasedInitializer.java | 5 +- .../representation/PartialFunction.java | 10 ++-- .../representation/PartialSymbol.java | 9 ++- .../store/reasoning/seed/ModelSeed.java | 13 +++-- .../refinery/store/reasoning/seed/Seed.java | 5 +- .../store/reasoning/seed/SeedInitializer.java | 5 +- .../translator/PartialSymbolTranslator.java | 5 +- .../containment/ContainmentLinkRefiner.java | 2 +- .../containment/ContainsRefiner.java | 6 +- .../containment/InferredContainment.java | 4 +- .../UndirectedCrossReferenceInitializer.java | 2 +- .../metamodel/MetamodelBuilder.java | 2 +- .../translator/multiobject/EqualsRefiner.java | 2 +- .../translator/multiobject/ExistsRefiner.java | 2 +- .../multiobject/MultiObjectInitializer.java | 2 +- .../MultiObjectStorageRefiner.java | 2 +- .../opposite/OppositeInterpretation.java | 8 +-- .../translator/opposite/OppositeRefiner.java | 7 ++- 41 files changed, 255 insertions(+), 192 deletions(-) create mode 100644 subprojects/logic/src/main/java/tools/refinery/logic/AbstractValue.java diff --git a/subprojects/generator/src/main/java/tools/refinery/generator/ModelFacade.java b/subprojects/generator/src/main/java/tools/refinery/generator/ModelFacade.java index a00ddc46c..eaf60082c 100644 --- 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 PartialInterpretation getPartialInterpretation(PartialSymbol partialSymbol) { + public , C> PartialInterpretation getPartialInterpretation( + PartialSymbol 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 index 1515dceb6..36190b766 100644 --- 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 solutionSerializerProvider) { + Provider solutionSerializerProvider) { super(problemTrace, store, modelSeed, Concreteness.CANDIDATE); this.solutionSerializerProvider = solutionSerializerProvider; initialVersion = getModel().commit(); @@ -66,7 +67,8 @@ public void generate() { } @Override - public PartialInterpretation getPartialInterpretation(PartialSymbol partialSymbol) { + public , C> PartialInterpretation getPartialInterpretation( + PartialSymbol partialSymbol) { checkSuccessfulGeneration(); return super.getPartialInterpretation(partialSymbol); } diff --git a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/internal/DecisionTreeValue.java b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/internal/DecisionTreeValue.java index 3260ef3d1..a6b559891 100644 --- a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/internal/DecisionTreeValue.java +++ b/subprojects/language-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/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/internal/TerminalNode.java b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/internal/TerminalNode.java index 2ebaecef6..75933fe49 100644 --- a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/internal/TerminalNode.java +++ b/subprojects/language-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 index 607caa48f..0b4d87d25 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 + * SPDX-FileCopyrightText: 2021-2024 The Refinery Authors * * SPDX-License-Identifier: EPL-2.0 */ package tools.refinery.logic; -import java.util.Objects; -import java.util.Optional; - -public non-sealed interface AbstractDomain extends AnyAbstractDomain { +public non-sealed interface AbstractDomain, C> extends AnyAbstractDomain { @Override Class abstractType(); @Override Class concreteType(); - A toAbstract(C concreteValue); - - Optional 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 000000000..0b5e0d012 --- /dev/null +++ b/subprojects/logic/src/main/java/tools/refinery/logic/AbstractValue.java @@ -0,0 +1,32 @@ +/* + * SPDX-FileCopyrightText: 2024 The Refinery Authors + * + * SPDX-License-Identifier: EPL-2.0 + */ +package tools.refinery.logic; + +import org.jetbrains.annotations.Nullable; + +public interface AbstractValue, 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 508a454b6..297756154 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 { @@ -29,41 +26,17 @@ public Class concreteType() { } @Override - public CardinalityInterval toAbstract(Integer concreteValue) { - return CardinalityIntervals.exactly(concreteValue); - } - - @Override - public Optional 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 dbf30defb..996ebde51 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 + 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 29a7f69de..8892b278e 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 + * SPDX-FileCopyrightText: 2021-2024 The Refinery Authors * * 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/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 0919fc36f..efe1464ee 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 + * SPDX-FileCopyrightText: 2021-2024 The Refinery Authors * * 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); 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 bbdd3f978..59bdeab39 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 + * SPDX-FileCopyrightText: 2021-2024 The Refinery Authors * * 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 { TRUE("true"), FALSE("false"), @@ -28,14 +31,41 @@ public static TruthValue toTruthValue(boolean value) { 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 TruthValue not() { }; } - 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 TruthValue join(TruthValue other) { 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 443f744f6..de8a89be2 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 + * SPDX-FileCopyrightText: 2021-2024 The Refinery Authors * * SPDX-License-Identifier: EPL-2.0 */ @@ -7,8 +7,6 @@ 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 { @@ -28,42 +26,17 @@ public Class concreteType() { } @Override - public TruthValue toAbstract(Boolean concreteValue) { - return TruthValue.toTruthValue(concreteValue); - } - - @Override - public Optional 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); } } - diff --git a/subprojects/logic/src/test/java/tools/refinery/logic/term/cardinalityinterval/CardinalityIntervalsTest.java b/subprojects/logic/src/test/java/tools/refinery/logic/term/cardinalityinterval/CardinalityIntervalsTest.java index 5441c8377..d68df3352 100644 --- a/subprojects/logic/src/test/java/tools/refinery/logic/term/cardinalityinterval/CardinalityIntervalsTest.java +++ b/subprojects/logic/src/test/java/tools/refinery/logic/term/cardinalityinterval/CardinalityIntervalsTest.java @@ -15,13 +15,13 @@ class CardinalityIntervalsTest { @Test void betweenEmptyTest() { var interval = CardinalityIntervals.between(2, 1); - assertThat(interval.isEmpty(), equalTo(true)); + assertThat(interval.isError(), equalTo(true)); } @Test void betweenNegativeUpperBoundTest() { var interval = CardinalityIntervals.between(0, -1); assertThat(interval.upperBound(), equalTo(UpperCardinalities.UNBOUNDED)); - assertThat(interval.isEmpty(), equalTo(false)); + assertThat(interval.isError(), equalTo(false)); } } diff --git a/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/ScopePropagator.java b/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/ScopePropagator.java index bfe2ca41a..94e6bbd7a 100644 --- a/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/ScopePropagator.java +++ b/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/ScopePropagator.java @@ -48,7 +48,7 @@ public ScopePropagator scope(PartialRelation type, CardinalityInterval interval) } var newValue = scopes.compute(type, (ignoredKey, oldValue) -> oldValue == null ? interval : oldValue.meet(interval)); - if (newValue.isEmpty()) { + if (newValue.isError()) { throw new TranslationException(type, "Unsatisfiable scope for type %s".formatted(type)); } return this; diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/ReasoningAdapter.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/ReasoningAdapter.java index 7f0ef8b43..a9b3141ad 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/ReasoningAdapter.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/ReasoningAdapter.java @@ -1,11 +1,12 @@ /* - * SPDX-FileCopyrightText: 2021-2023 The Refinery Authors + * SPDX-FileCopyrightText: 2021-2024 The Refinery Authors * * SPDX-License-Identifier: EPL-2.0 */ package tools.refinery.store.reasoning; import org.jetbrains.annotations.Nullable; +import tools.refinery.logic.AbstractValue; import tools.refinery.store.adapter.ModelAdapter; import tools.refinery.store.reasoning.internal.ReasoningBuilderImpl; import tools.refinery.store.reasoning.interpretation.AnyPartialInterpretation; @@ -27,17 +28,19 @@ public interface ReasoningAdapter extends ModelAdapter { default AnyPartialInterpretation getPartialInterpretation(Concreteness concreteness, AnyPartialSymbol partialSymbol) { - return getPartialInterpretation(concreteness, (PartialSymbol) partialSymbol); + var typedPartialSymbol = (PartialSymbol) partialSymbol; + return getPartialInterpretation(concreteness, typedPartialSymbol); } - PartialInterpretation getPartialInterpretation(Concreteness concreteness, - PartialSymbol partialSymbol); + , C> PartialInterpretation getPartialInterpretation( + Concreteness concreteness, PartialSymbol partialSymbol); default AnyPartialInterpretationRefiner getRefiner(AnyPartialSymbol partialSymbol) { - return getRefiner((PartialSymbol) partialSymbol); + var typedPartialSymbol = (PartialSymbol) partialSymbol; + return getRefiner(typedPartialSymbol); } - PartialInterpretationRefiner getRefiner(PartialSymbol partialSymbol); + , C> PartialInterpretationRefiner getRefiner(PartialSymbol partialSymbol); @Nullable Tuple1 split(int parentMultiObject); diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/actions/MergeActionLiteral.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/actions/MergeActionLiteral.java index 79e0237c7..86256331d 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/actions/MergeActionLiteral.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/actions/MergeActionLiteral.java @@ -1,10 +1,11 @@ /* - * SPDX-FileCopyrightText: 2023 The Refinery Authors + * SPDX-FileCopyrightText: 2023-2024 The Refinery Authors * * SPDX-License-Identifier: EPL-2.0 */ package tools.refinery.store.reasoning.actions; +import tools.refinery.logic.AbstractValue; import tools.refinery.store.dse.transition.actions.AbstractActionLiteral; import tools.refinery.store.dse.transition.actions.BoundActionLiteral; import tools.refinery.store.model.Model; @@ -15,7 +16,7 @@ import java.util.List; -public class MergeActionLiteral extends AbstractActionLiteral { +public class MergeActionLiteral, C> extends AbstractActionLiteral { private final PartialSymbol partialSymbol; private final List parameters; private final A value; diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/actions/PartialActionLiterals.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/actions/PartialActionLiterals.java index 7b4c54462..e8e6880af 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/actions/PartialActionLiterals.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/actions/PartialActionLiterals.java @@ -5,6 +5,7 @@ */ package tools.refinery.store.reasoning.actions; +import tools.refinery.logic.AbstractValue; import tools.refinery.logic.term.NodeVariable; import tools.refinery.store.reasoning.representation.PartialRelation; import tools.refinery.store.reasoning.representation.PartialSymbol; @@ -17,8 +18,8 @@ private PartialActionLiterals() { throw new IllegalStateException("This is a static utility class and should not be instantiated directly"); } - public static MergeActionLiteral merge(PartialSymbol partialSymbol, A value, - NodeVariable... parameters) { + public static , C> MergeActionLiteral merge( + PartialSymbol partialSymbol, A value, NodeVariable... parameters) { return new MergeActionLiteral<>(partialSymbol, value, List.of(parameters)); } diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/internal/ReasoningAdapterImpl.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/internal/ReasoningAdapterImpl.java index a287cce3f..386ae1d84 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/internal/ReasoningAdapterImpl.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/internal/ReasoningAdapterImpl.java @@ -1,11 +1,12 @@ /* - * SPDX-FileCopyrightText: 2021-2023 The Refinery Authors + * SPDX-FileCopyrightText: 2021-2024 The Refinery Authors * * SPDX-License-Identifier: EPL-2.0 */ package tools.refinery.store.reasoning.internal; import org.jetbrains.annotations.Nullable; +import tools.refinery.logic.AbstractValue; import tools.refinery.store.model.Interpretation; import tools.refinery.store.model.Model; import tools.refinery.store.reasoning.ReasoningAdapter; @@ -49,7 +50,7 @@ class ReasoningAdapterImpl implements ReasoningAdapter { createPartialInterpretations(); var refinerFactories = storeAdapter.getSymbolRefiners(); - refiners = new HashMap<>(refinerFactories.size()); + refiners = HashMap.newHashMap(refinerFactories.size()); createRefiners(); storageRefiners = storeAdapter.createStorageRefiner(model); @@ -69,7 +70,7 @@ private void createPartialInterpretations() { for (int i = 0; i < concretenessLength; i++) { var concreteness = Concreteness.values()[i]; if (supportedInterpretations.contains(concreteness)) { - partialInterpretations[i] = new HashMap<>(interpretationFactories.size()); + partialInterpretations[i] = HashMap.newHashMap(interpretationFactories.size()); } } // Create the partial interpretations in order so that factories may refer to interpretations of symbols @@ -87,7 +88,7 @@ private void createPartialInterpretations() { } } - private PartialInterpretation createPartialInterpretation( + private , C> PartialInterpretation createPartialInterpretation( Concreteness concreteness, PartialInterpretation.Factory interpreter, AnyPartialSymbol symbol) { // The builder only allows well-typed assignment of interpreters to symbols. @SuppressWarnings("unchecked") @@ -107,7 +108,7 @@ private void createRefiners() { } } - private PartialInterpretationRefiner createRefiner( + private , C> PartialInterpretationRefiner createRefiner( PartialInterpretationRefiner.Factory factory, AnyPartialSymbol symbol) { // The builder only allows well-typed assignment of interpreters to symbols. @SuppressWarnings("unchecked") @@ -126,8 +127,8 @@ public ReasoningStoreAdapterImpl getStoreAdapter() { } @Override - public PartialInterpretation getPartialInterpretation(Concreteness concreteness, - PartialSymbol partialSymbol) { + public , C> PartialInterpretation getPartialInterpretation( + Concreteness concreteness, PartialSymbol partialSymbol) { var map = partialInterpretations[concreteness.ordinal()]; if (map == null) { throw new IllegalArgumentException("No interpretation for concreteness: " + concreteness); @@ -143,7 +144,8 @@ public PartialInterpretation getPartialInterpretation(Concreteness } @Override - public PartialInterpretationRefiner getRefiner(PartialSymbol partialSymbol) { + public , C> PartialInterpretationRefiner getRefiner( + PartialSymbol partialSymbol) { var refiner = refiners.get(partialSymbol); if (refiner == null) { throw new IllegalArgumentException("No refiner for partial symbol: " + partialSymbol); diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/interpretation/AbstractPartialInterpretation.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/interpretation/AbstractPartialInterpretation.java index ed291eaca..4f51957ba 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/interpretation/AbstractPartialInterpretation.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/interpretation/AbstractPartialInterpretation.java @@ -5,11 +5,13 @@ */ package tools.refinery.store.reasoning.interpretation; +import tools.refinery.logic.AbstractValue; import tools.refinery.store.reasoning.ReasoningAdapter; import tools.refinery.store.reasoning.literal.Concreteness; import tools.refinery.store.reasoning.representation.PartialSymbol; -public abstract class AbstractPartialInterpretation implements PartialInterpretation { +public abstract class AbstractPartialInterpretation, C> + implements PartialInterpretation { private final ReasoningAdapter adapter; private final PartialSymbol partialSymbol; private final Concreteness concreteness; diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/interpretation/PartialInterpretation.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/interpretation/PartialInterpretation.java index 86ffe7516..5a304030e 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/interpretation/PartialInterpretation.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/interpretation/PartialInterpretation.java @@ -1,10 +1,11 @@ /* - * SPDX-FileCopyrightText: 2021-2023 The Refinery Authors + * SPDX-FileCopyrightText: 2021-2024 The Refinery Authors * * SPDX-License-Identifier: EPL-2.0 */ package tools.refinery.store.reasoning.interpretation; +import tools.refinery.logic.AbstractValue; import tools.refinery.store.map.Cursor; import tools.refinery.store.model.ModelStoreBuilder; import tools.refinery.store.reasoning.ReasoningAdapter; @@ -14,7 +15,7 @@ import java.util.Set; -public non-sealed interface PartialInterpretation extends AnyPartialInterpretation { +public non-sealed interface PartialInterpretation, C> extends AnyPartialInterpretation { @Override PartialSymbol getPartialSymbol(); @@ -23,7 +24,7 @@ public non-sealed interface PartialInterpretation extends AnyPartialInterp Cursor getAll(); @FunctionalInterface - interface Factory { + interface Factory, C> { PartialInterpretation create(ReasoningAdapter adapter, Concreteness concreteness, PartialSymbol partialSymbol); diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/refinement/AbstractPartialInterpretationRefiner.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/refinement/AbstractPartialInterpretationRefiner.java index a7fc5b7e5..42943490f 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/refinement/AbstractPartialInterpretationRefiner.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/refinement/AbstractPartialInterpretationRefiner.java @@ -1,14 +1,16 @@ /* - * SPDX-FileCopyrightText: 2023 The Refinery Authors + * SPDX-FileCopyrightText: 2023-2024 The Refinery Authors * * SPDX-License-Identifier: EPL-2.0 */ package tools.refinery.store.reasoning.refinement; +import tools.refinery.logic.AbstractValue; import tools.refinery.store.reasoning.ReasoningAdapter; import tools.refinery.store.reasoning.representation.PartialSymbol; -public abstract class AbstractPartialInterpretationRefiner implements PartialInterpretationRefiner { +public abstract class AbstractPartialInterpretationRefiner, C> + implements PartialInterpretationRefiner { private final ReasoningAdapter adapter; private final PartialSymbol partialSymbol; diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/refinement/ConcreteSymbolRefiner.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/refinement/ConcreteSymbolRefiner.java index ebb9b8249..d6ac0e9db 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/refinement/ConcreteSymbolRefiner.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/refinement/ConcreteSymbolRefiner.java @@ -1,10 +1,11 @@ /* - * SPDX-FileCopyrightText: 2023 The Refinery Authors + * SPDX-FileCopyrightText: 2023-2024 The Refinery Authors * * SPDX-License-Identifier: EPL-2.0 */ package tools.refinery.store.reasoning.refinement; +import tools.refinery.logic.AbstractValue; import tools.refinery.store.model.Interpretation; import tools.refinery.store.reasoning.ReasoningAdapter; import tools.refinery.store.reasoning.representation.PartialSymbol; @@ -13,7 +14,8 @@ import java.util.Objects; -public class ConcreteSymbolRefiner extends AbstractPartialInterpretationRefiner { +public class ConcreteSymbolRefiner, C> + extends AbstractPartialInterpretationRefiner { private final Interpretation interpretation; public ConcreteSymbolRefiner(ReasoningAdapter adapter, PartialSymbol partialSymbol, @@ -25,14 +27,14 @@ public ConcreteSymbolRefiner(ReasoningAdapter adapter, PartialSymbol parti @Override public boolean merge(Tuple key, A value) { var currentValue = interpretation.get(key); - var mergedValue = getPartialSymbol().abstractDomain().commonRefinement(currentValue, value); + var mergedValue = currentValue.meet(value); if (!Objects.equals(currentValue, mergedValue)) { interpretation.put(key, mergedValue); } return true; } - public static Factory of(Symbol concreteSymbol) { + public static , C1> Factory of(Symbol concreteSymbol) { return (adapter, partialSymbol) -> new ConcreteSymbolRefiner<>(adapter, partialSymbol, concreteSymbol); } } diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/refinement/PartialInterpretationRefiner.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/refinement/PartialInterpretationRefiner.java index f48d1d1f7..c8b182b8f 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/refinement/PartialInterpretationRefiner.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/refinement/PartialInterpretationRefiner.java @@ -1,22 +1,24 @@ /* - * SPDX-FileCopyrightText: 2023 The Refinery Authors + * SPDX-FileCopyrightText: 2023-2024 The Refinery Authors * * SPDX-License-Identifier: EPL-2.0 */ package tools.refinery.store.reasoning.refinement; +import tools.refinery.logic.AbstractValue; import tools.refinery.store.reasoning.ReasoningAdapter; import tools.refinery.store.reasoning.representation.PartialSymbol; import tools.refinery.store.tuple.Tuple; -public non-sealed interface PartialInterpretationRefiner extends AnyPartialInterpretationRefiner { +public non-sealed interface PartialInterpretationRefiner, C> + extends AnyPartialInterpretationRefiner { @Override PartialSymbol getPartialSymbol(); boolean merge(Tuple key, A value); @FunctionalInterface - interface Factory { + interface Factory, C> { PartialInterpretationRefiner create(ReasoningAdapter adapter, PartialSymbol partialSymbol); } } diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/refinement/RefinementBasedInitializer.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/refinement/RefinementBasedInitializer.java index b6bccb016..1a2c03a65 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/refinement/RefinementBasedInitializer.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/refinement/RefinementBasedInitializer.java @@ -1,16 +1,17 @@ /* - * SPDX-FileCopyrightText: 2023 The Refinery Authors + * SPDX-FileCopyrightText: 2023-2024 The Refinery Authors * * SPDX-License-Identifier: EPL-2.0 */ package tools.refinery.store.reasoning.refinement; +import tools.refinery.logic.AbstractValue; import tools.refinery.store.model.Model; import tools.refinery.store.reasoning.ReasoningAdapter; import tools.refinery.store.reasoning.representation.PartialSymbol; import tools.refinery.store.reasoning.seed.ModelSeed; -public class RefinementBasedInitializer implements PartialModelInitializer { +public class RefinementBasedInitializer, C> implements PartialModelInitializer { private final PartialSymbol partialSymbol; public RefinementBasedInitializer(PartialSymbol partialSymbol) { diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/representation/PartialFunction.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/representation/PartialFunction.java index 236be7f82..88b98da8d 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/representation/PartialFunction.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/representation/PartialFunction.java @@ -1,14 +1,16 @@ /* - * SPDX-FileCopyrightText: 2021-2023 The Refinery Authors + * SPDX-FileCopyrightText: 2021-2024 The Refinery Authors * * SPDX-License-Identifier: EPL-2.0 */ package tools.refinery.store.reasoning.representation; import tools.refinery.logic.AbstractDomain; +import tools.refinery.logic.AbstractValue; -public record PartialFunction(String name, int arity, AbstractDomain abstractDomain) - implements AnyPartialFunction, PartialSymbol { +public record PartialFunction, C>( + String name, int arity, AbstractDomain abstractDomain) implements AnyPartialFunction, + PartialSymbol { @Override public A defaultValue() { return null; @@ -21,7 +23,7 @@ public boolean equals(Object o) { @Override public int hashCode() { - // Compare by identity to make hash table lookups more efficient. + // Compare by identity to make hash table look-ups more efficient. return System.identityHashCode(this); } diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/representation/PartialSymbol.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/representation/PartialSymbol.java index 6986d5187..21cbfefad 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/representation/PartialSymbol.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/representation/PartialSymbol.java @@ -1,13 +1,15 @@ /* - * SPDX-FileCopyrightText: 2021-2023 The Refinery Authors + * SPDX-FileCopyrightText: 2021-2024 The Refinery Authors * * SPDX-License-Identifier: EPL-2.0 */ package tools.refinery.store.reasoning.representation; import tools.refinery.logic.AbstractDomain; +import tools.refinery.logic.AbstractValue; -public sealed interface PartialSymbol extends AnyPartialSymbol permits PartialFunction, PartialRelation { +public sealed interface PartialSymbol, C> extends AnyPartialSymbol + permits PartialFunction, PartialRelation { @Override AbstractDomain abstractDomain(); @@ -17,7 +19,8 @@ static PartialRelation of(String name, int arity) { return new PartialRelation(name, arity); } - static PartialFunction of(String name, int arity, AbstractDomain abstractDomain) { + static , C> PartialFunction of( + String name, int arity, AbstractDomain abstractDomain) { return new PartialFunction<>(name, arity, abstractDomain); } } diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/seed/ModelSeed.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/seed/ModelSeed.java index e6b3eaf94..9cd4862b2 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/seed/ModelSeed.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/seed/ModelSeed.java @@ -1,10 +1,11 @@ /* - * SPDX-FileCopyrightText: 2023 The Refinery Authors + * SPDX-FileCopyrightText: 2023-2024 The Refinery Authors * * SPDX-License-Identifier: EPL-2.0 */ package tools.refinery.store.reasoning.seed; +import tools.refinery.logic.AbstractValue; import tools.refinery.store.map.Cursor; import tools.refinery.store.reasoning.representation.AnyPartialSymbol; import tools.refinery.store.reasoning.representation.PartialSymbol; @@ -29,7 +30,7 @@ public int getNodeCount() { return nodeCount; } - public Seed getSeed(PartialSymbol partialSymbol) { + public > Seed getSeed(PartialSymbol partialSymbol) { var seed = seeds.get(partialSymbol); if (seed == null) { throw new IllegalArgumentException("No seed for partial symbol " + partialSymbol); @@ -48,7 +49,8 @@ public Set getSeededSymbols() { return Collections.unmodifiableSet(seeds.keySet()); } - public Cursor getCursor(PartialSymbol partialSymbol, A defaultValue) { + public > Cursor getCursor(PartialSymbol partialSymbol, + A defaultValue) { return getSeed(partialSymbol).getCursor(defaultValue, nodeCount); } @@ -67,7 +69,7 @@ private Builder(int nodeCount) { this.nodeCount = nodeCount; } - public Builder seed(PartialSymbol partialSymbol, Seed seed) { + public > Builder seed(PartialSymbol partialSymbol, Seed seed) { if (seed.arity() != partialSymbol.arity()) { throw new IllegalStateException("Expected seed of arity %d for partial symbol %s, but got %d instead" .formatted(partialSymbol.arity(), partialSymbol, seed.arity())); @@ -82,7 +84,8 @@ public Builder seed(PartialSymbol partialSymbol, Seed seed) { return this; } - public Builder seed(PartialSymbol partialSymbol, Consumer> callback) { + public > Builder seed(PartialSymbol partialSymbol, + Consumer> callback) { var builder = Seed.builder(partialSymbol); callback.accept(builder); return seed(partialSymbol, builder.build()); diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/seed/Seed.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/seed/Seed.java index d9bad866b..32562f01b 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/seed/Seed.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/seed/Seed.java @@ -1,10 +1,11 @@ /* - * SPDX-FileCopyrightText: 2021-2023 The Refinery Authors + * SPDX-FileCopyrightText: 2021-2024 The Refinery Authors * * SPDX-License-Identifier: EPL-2.0 */ package tools.refinery.store.reasoning.seed; +import tools.refinery.logic.AbstractValue; import tools.refinery.store.map.Cursor; import tools.refinery.store.reasoning.representation.PartialSymbol; import tools.refinery.store.representation.Symbol; @@ -33,7 +34,7 @@ static Builder builder(Symbol symbol) { return builder(symbol.arity(), symbol.valueType(), symbol.defaultValue()); } - static Builder builder(PartialSymbol partialSymbol) { + static > Builder builder(PartialSymbol partialSymbol) { return builder(partialSymbol.arity(), partialSymbol.abstractDomain().abstractType(), partialSymbol.defaultValue()); } diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/seed/SeedInitializer.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/seed/SeedInitializer.java index 9af457d85..138e3a640 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/seed/SeedInitializer.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/seed/SeedInitializer.java @@ -1,16 +1,17 @@ /* - * SPDX-FileCopyrightText: 2023 The Refinery Authors + * SPDX-FileCopyrightText: 2023-2024 The Refinery Authors * * SPDX-License-Identifier: EPL-2.0 */ package tools.refinery.store.reasoning.seed; +import tools.refinery.logic.AbstractValue; import tools.refinery.store.model.Model; import tools.refinery.store.reasoning.refinement.PartialModelInitializer; import tools.refinery.store.reasoning.representation.PartialSymbol; import tools.refinery.store.representation.Symbol; -public class SeedInitializer implements PartialModelInitializer { +public class SeedInitializer> implements PartialModelInitializer { private final Symbol symbol; private final PartialSymbol partialSymbol; diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/PartialSymbolTranslator.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/PartialSymbolTranslator.java index 6cdb287df..f25830981 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/PartialSymbolTranslator.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/PartialSymbolTranslator.java @@ -6,6 +6,7 @@ package tools.refinery.store.reasoning.translator; import org.jetbrains.annotations.Nullable; +import tools.refinery.logic.AbstractValue; import tools.refinery.store.dse.transition.DesignSpaceExplorationBuilder; import tools.refinery.store.dse.transition.Rule; import tools.refinery.store.dse.transition.objectives.Criterion; @@ -25,8 +26,8 @@ import java.util.List; @SuppressWarnings("UnusedReturnValue") -public abstract sealed class PartialSymbolTranslator implements AnyPartialSymbolTranslator - permits PartialRelationTranslator { +public abstract sealed class PartialSymbolTranslator, C> + implements AnyPartialSymbolTranslator permits PartialRelationTranslator { private final PartialSymbol partialSymbol; private boolean configured = false; protected PartialInterpretationRefiner.Factory interpretationRefiner; diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/containment/ContainmentLinkRefiner.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/containment/ContainmentLinkRefiner.java index ef007efc8..e83c33ac7 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/containment/ContainmentLinkRefiner.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/containment/ContainmentLinkRefiner.java @@ -64,7 +64,7 @@ public InferredContainment mustLink(InferredContainment oldValue) { if (mustLinks.contains(factory.linkType)) { return oldValue; } - return new InferredContainment(oldValue.contains().merge(TruthValue.TRUE), + return new InferredContainment(oldValue.contains().meet(TruthValue.TRUE), addToSet(mustLinks, factory.linkType), oldValue.forbiddenLinks()); } diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/containment/ContainsRefiner.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/containment/ContainsRefiner.java index 3fe63339d..008200406 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/containment/ContainsRefiner.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/containment/ContainsRefiner.java @@ -1,5 +1,5 @@ /* - * SPDX-FileCopyrightText: 2023 The Refinery Authors + * SPDX-FileCopyrightText: 2023-2024 The Refinery Authors * * SPDX-License-Identifier: EPL-2.0 */ @@ -23,7 +23,7 @@ class ContainsRefiner extends AbstractPartialInterpretationRefiner(values.length); + EMPTY_VALUES = LinkedHashMap.newLinkedHashMap(values.length); for (var value : values) { EMPTY_VALUES.put(value, new InferredContainment(value, Set.of(), Set.of())); } @@ -53,7 +53,7 @@ public boolean merge(Tuple key, TruthValue value) { } public InferredContainment mergeLink(InferredContainment oldValue, TruthValue toMerge) { - var newContains = oldValue.contains().merge(toMerge); + var newContains = oldValue.contains().meet(toMerge); if (newContains.equals(oldValue.contains())) { return oldValue; } diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/containment/InferredContainment.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/containment/InferredContainment.java index 77c7aaf41..0b6503c3c 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/containment/InferredContainment.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/containment/InferredContainment.java @@ -31,11 +31,11 @@ private static TruthValue adjustContains(TruthValue contains, Set forbiddenLinks) { var result = contains; if (!mustLinks.isEmpty()) { - result = result.merge(TruthValue.TRUE); + result = result.meet(TruthValue.TRUE); } boolean hasErrorLink = mustLinks.stream().anyMatch(forbiddenLinks::contains); if (mustLinks.size() >= 2 || hasErrorLink) { - result = result.merge(TruthValue.ERROR); + result = result.meet(TruthValue.ERROR); } return result; } diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/crossreference/UndirectedCrossReferenceInitializer.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/crossreference/UndirectedCrossReferenceInitializer.java index 5bb1b9679..84dcfdc56 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/crossreference/UndirectedCrossReferenceInitializer.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/crossreference/UndirectedCrossReferenceInitializer.java @@ -73,7 +73,7 @@ private LinkedHashMap getMergedMap(ModelSeed modelSeed) { // Already processed entry. continue; } - var mergedValue = value.merge(oppositeValue == null ? defaultValue : oppositeValue); + var mergedValue = value.meet(oppositeValue == null ? defaultValue : oppositeValue); mergedMap.put(key, mergedValue); if (first != second) { mergedMap.put(oppositeKey, mergedValue); diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/metamodel/MetamodelBuilder.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/metamodel/MetamodelBuilder.java index a5047768a..d1979b8cd 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/metamodel/MetamodelBuilder.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/metamodel/MetamodelBuilder.java @@ -131,7 +131,7 @@ private void processReferenceInfo(PartialRelation linkType, ReferenceInfo info) var oppositeInfo = referenceInfoMap.get(opposite); validateOpposite(linkType, info, opposite, oppositeInfo); targetMultiplicity = oppositeInfo.multiplicity(); - defaultValue = defaultValue.merge(oppositeInfo.defaultValue()); + defaultValue = defaultValue.meet(oppositeInfo.defaultValue()); if (oppositeInfo.containment()) { // Skip processing this reference and process it once we encounter its containment opposite. return; diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiobject/EqualsRefiner.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiobject/EqualsRefiner.java index 0b89ec583..075959328 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiobject/EqualsRefiner.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiobject/EqualsRefiner.java @@ -51,7 +51,7 @@ public boolean merge(Tuple key, TruthValue value) { return false; } var newCount = currentCount.meet(CardinalityIntervals.LONE); - if (newCount.isEmpty()) { + if (newCount.isError()) { return false; } countInterpretation.put(unaryKey, newCount); diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiobject/ExistsRefiner.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiobject/ExistsRefiner.java index 3908fedb8..83fa4377d 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiobject/ExistsRefiner.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiobject/ExistsRefiner.java @@ -42,7 +42,7 @@ public boolean merge(Tuple key, TruthValue value) { } default -> throw new IllegalArgumentException("Unknown TruthValue: " + value); } - if (newCount.isEmpty()) { + if (newCount.isError()) { return false; } countInterpretation.put(key, newCount); diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiobject/MultiObjectInitializer.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiobject/MultiObjectInitializer.java index 694a800b1..eb13174cf 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiobject/MultiObjectInitializer.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiobject/MultiObjectInitializer.java @@ -37,7 +37,7 @@ public void initialize(Model model, ModelSeed modelSeed) { var uniqueTable = new HashMap(); for (int i = 0; i < intervals.length; i++) { var interval = intervals[i]; - if (interval.isEmpty()) { + if (interval.isError()) { throw new TranslationException(ReasoningAdapter.EXISTS_SYMBOL, "Inconsistent existence or equality for node " + i); } diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiobject/MultiObjectStorageRefiner.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiobject/MultiObjectStorageRefiner.java index 147ae4869..ab401f9ee 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiobject/MultiObjectStorageRefiner.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiobject/MultiObjectStorageRefiner.java @@ -28,7 +28,7 @@ public boolean split(int parentNode, int childNode) { return false; } var newParentCount = parentCount.take(1); - if (newParentCount.isEmpty()) { + if (newParentCount.isError()) { return false; } var childKey = Tuple.of(childNode); diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/opposite/OppositeInterpretation.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/opposite/OppositeInterpretation.java index 7290ab407..75828086a 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/opposite/OppositeInterpretation.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/opposite/OppositeInterpretation.java @@ -1,11 +1,11 @@ /* - * SPDX-FileCopyrightText: 2023 The Refinery Authors + * SPDX-FileCopyrightText: 2023-2024 The Refinery Authors * * SPDX-License-Identifier: EPL-2.0 */ package tools.refinery.store.reasoning.translator.opposite; - +import tools.refinery.logic.AbstractValue; import tools.refinery.store.map.AnyVersionedMap; import tools.refinery.store.map.Cursor; import tools.refinery.store.reasoning.ReasoningAdapter; @@ -17,7 +17,7 @@ import java.util.Set; -class OppositeInterpretation extends AbstractPartialInterpretation { +class OppositeInterpretation, C> extends AbstractPartialInterpretation { private final PartialInterpretation opposite; private OppositeInterpretation(ReasoningAdapter adapter, Concreteness concreteness, @@ -36,7 +36,7 @@ public Cursor getAll() { return new OppositeCursor<>(opposite.getAll()); } - public static Factory of(PartialSymbol oppositeSymbol) { + public static , C1> Factory of(PartialSymbol oppositeSymbol) { return (adapter, concreteness, partialSymbol) -> { var opposite = adapter.getPartialInterpretation(concreteness, oppositeSymbol); return new OppositeInterpretation<>(adapter, concreteness, partialSymbol, opposite); diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/opposite/OppositeRefiner.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/opposite/OppositeRefiner.java index d09684dfd..47e3ac6a8 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/opposite/OppositeRefiner.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/opposite/OppositeRefiner.java @@ -1,17 +1,18 @@ /* - * SPDX-FileCopyrightText: 2023 The Refinery Authors + * SPDX-FileCopyrightText: 2023-2024 The Refinery Authors * * SPDX-License-Identifier: EPL-2.0 */ package tools.refinery.store.reasoning.translator.opposite; +import tools.refinery.logic.AbstractValue; import tools.refinery.store.reasoning.ReasoningAdapter; import tools.refinery.store.reasoning.refinement.AbstractPartialInterpretationRefiner; import tools.refinery.store.reasoning.refinement.PartialInterpretationRefiner; import tools.refinery.store.reasoning.representation.PartialSymbol; import tools.refinery.store.tuple.Tuple; -public class OppositeRefiner extends AbstractPartialInterpretationRefiner { +public class OppositeRefiner, C> extends AbstractPartialInterpretationRefiner { private final PartialInterpretationRefiner opposite; protected OppositeRefiner(ReasoningAdapter adapter, PartialSymbol partialSymbol, @@ -26,7 +27,7 @@ public boolean merge(Tuple key, A value) { return opposite.merge(oppositeKey, value); } - public static Factory of(PartialSymbol oppositeSymbol) { + public static , C1> Factory of(PartialSymbol oppositeSymbol) { return (adapter, partialSymbol) -> new OppositeRefiner<>(adapter, partialSymbol, oppositeSymbol); } }