From bc742b20fa187200def2809e5aef71547f75c65a Mon Sep 17 00:00:00 2001 From: Kristóf Marussy Date: Tue, 18 Jul 2023 20:18:48 +0200 Subject: feat: basic partial interpretation infrastructure --- .../store/reasoning/AnyPartialInterpretation.java | 18 -- .../refinery/store/reasoning/MergeResult.java | 20 -- .../store/reasoning/PartialInterpretation.java | 25 -- .../refinery/store/reasoning/ReasoningAdapter.java | 39 ++- .../refinery/store/reasoning/ReasoningBuilder.java | 28 ++- .../store/reasoning/ReasoningStoreAdapter.java | 5 +- .../reasoning/internal/PartialQueryRewriter.java | 103 ++++++++ .../reasoning/internal/ReasoningAdapterImpl.java | 142 ++++++++++- .../reasoning/internal/ReasoningBuilderImpl.java | 123 +++++++++- .../internal/ReasoningStoreAdapterImpl.java | 93 +++++++- .../AbstractPartialInterpretation.java | 38 +++ .../interpretation/AnyPartialInterpretation.java | 18 ++ .../interpretation/PartialInterpretation.java | 26 ++ .../interpretation/PartialRelationRewriter.java | 17 ++ .../QueryBasedRelationInterpretationFactory.java | 180 ++++++++++++++ .../interpretation/QueryBasedRelationRewriter.java | 44 ++++ .../store/reasoning/lifting/ClauseLifter.java | 10 +- .../store/reasoning/lifting/DnfLifter.java | 6 + .../store/reasoning/literal/PartialLiterals.java | 16 +- .../AnyPartialInterpretationRefiner.java | 15 ++ .../refinement/ConcreteSymbolRefiner.java | 51 ++++ .../refinement/DefaultStorageRefiner.java | 80 +++++++ .../refinement/PartialInterpretationRefiner.java | 22 ++ .../refinement/PartialModelInitializer.java | 13 + .../store/reasoning/refinement/StorageRefiner.java | 20 ++ .../reasoning/representation/PartialFunction.java | 5 - .../reasoning/representation/PartialRelation.java | 5 - .../reasoning/representation/PartialSymbol.java | 2 - .../store/reasoning/seed/MapBasedSeed.java | 117 +++++++++ .../tools/refinery/store/reasoning/seed/Seed.java | 54 +++++ .../store/reasoning/seed/SeedInitializer.java | 27 +++ .../refinery/store/reasoning/seed/UniformSeed.java | 27 --- .../store/reasoning/translator/Advice.java | 159 ------------- .../store/reasoning/translator/AdviceSlot.java | 30 --- .../translator/AnyPartialSymbolTranslator.java | 16 ++ .../translator/PartialRelationTranslator.java | 263 +++++++++++++++++++++ .../translator/PartialSymbolTranslator.java | 156 ++++++++++++ .../store/reasoning/translator/RoundingMode.java | 12 + .../reasoning/translator/TranslatedRelation.java | 27 --- .../reasoning/translator/TranslationUnit.java | 32 --- .../base/BaseDecisionInterpretation.java | 93 -------- .../base/BaseDecisionTranslationUnit.java | 49 ---- .../translator/base/TranslatedBaseDecision.java | 54 ----- .../typehierarchy/InferredMayTypeView.java | 40 ---- .../typehierarchy/InferredMustTypeView.java | 40 ---- .../TypeHierarchyTranslationUnit.java | 37 --- 46 files changed, 1680 insertions(+), 717 deletions(-) delete mode 100644 subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/AnyPartialInterpretation.java delete mode 100644 subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/MergeResult.java delete mode 100644 subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/PartialInterpretation.java create mode 100644 subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/internal/PartialQueryRewriter.java create mode 100644 subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/interpretation/AbstractPartialInterpretation.java create mode 100644 subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/interpretation/AnyPartialInterpretation.java create mode 100644 subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/interpretation/PartialInterpretation.java create mode 100644 subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/interpretation/PartialRelationRewriter.java create mode 100644 subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/interpretation/QueryBasedRelationInterpretationFactory.java create mode 100644 subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/interpretation/QueryBasedRelationRewriter.java create mode 100644 subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/refinement/AnyPartialInterpretationRefiner.java create mode 100644 subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/refinement/ConcreteSymbolRefiner.java create mode 100644 subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/refinement/DefaultStorageRefiner.java create mode 100644 subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/refinement/PartialInterpretationRefiner.java create mode 100644 subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/refinement/PartialModelInitializer.java create mode 100644 subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/refinement/StorageRefiner.java create mode 100644 subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/seed/MapBasedSeed.java create mode 100644 subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/seed/SeedInitializer.java delete mode 100644 subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/seed/UniformSeed.java delete mode 100644 subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/Advice.java delete mode 100644 subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/AdviceSlot.java create mode 100644 subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/AnyPartialSymbolTranslator.java create mode 100644 subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/PartialRelationTranslator.java create mode 100644 subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/PartialSymbolTranslator.java create mode 100644 subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/RoundingMode.java delete mode 100644 subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/TranslatedRelation.java delete mode 100644 subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/TranslationUnit.java delete mode 100644 subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/base/BaseDecisionInterpretation.java delete mode 100644 subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/base/BaseDecisionTranslationUnit.java delete mode 100644 subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/base/TranslatedBaseDecision.java delete mode 100644 subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/InferredMayTypeView.java delete mode 100644 subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/InferredMustTypeView.java delete mode 100644 subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeHierarchyTranslationUnit.java (limited to 'subprojects/store-reasoning/src/main/java/tools') diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/AnyPartialInterpretation.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/AnyPartialInterpretation.java deleted file mode 100644 index 000171a1..00000000 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/AnyPartialInterpretation.java +++ /dev/null @@ -1,18 +0,0 @@ -/* - * SPDX-FileCopyrightText: 2021-2023 The Refinery Authors - * - * SPDX-License-Identifier: EPL-2.0 - */ -package tools.refinery.store.reasoning; - -import tools.refinery.store.reasoning.representation.AnyPartialSymbol; - -public sealed interface AnyPartialInterpretation permits PartialInterpretation { - ReasoningAdapter getAdapter(); - - AnyPartialSymbol getPartialSymbol(); - - int countUnfinished(); - - int countErrors(); -} diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/MergeResult.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/MergeResult.java deleted file mode 100644 index d3a216d8..00000000 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/MergeResult.java +++ /dev/null @@ -1,20 +0,0 @@ -/* - * SPDX-FileCopyrightText: 2021-2023 The Refinery Authors - * - * SPDX-License-Identifier: EPL-2.0 - */ -package tools.refinery.store.reasoning; - -public enum MergeResult { - UNCHANGED, - REFINED, - REJECTED; - - public MergeResult andAlso(MergeResult other) { - return switch (this) { - case UNCHANGED -> other; - case REFINED -> other == REJECTED ? REJECTED : REFINED; - case REJECTED -> REJECTED; - }; - } -} diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/PartialInterpretation.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/PartialInterpretation.java deleted file mode 100644 index 4140d640..00000000 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/PartialInterpretation.java +++ /dev/null @@ -1,25 +0,0 @@ -/* - * SPDX-FileCopyrightText: 2021-2023 The Refinery Authors - * - * SPDX-License-Identifier: EPL-2.0 - */ -package tools.refinery.store.reasoning; - -import tools.refinery.store.reasoning.representation.PartialSymbol; -import tools.refinery.store.map.Cursor; -import tools.refinery.store.tuple.Tuple; - -public non-sealed interface PartialInterpretation extends AnyPartialInterpretation { - @Override - PartialSymbol getPartialSymbol(); - - A get(Tuple key); - - Cursor getAll(); - - MergeResult merge(Tuple key, A value); - - C getConcrete(Tuple key); - - Cursor getAllConcrete(); -} 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 66e809f7..17aec09c 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 @@ -5,27 +5,46 @@ */ package tools.refinery.store.reasoning; +import org.jetbrains.annotations.Nullable; import tools.refinery.store.adapter.ModelAdapter; -import tools.refinery.store.query.resultset.ResultSet; -import tools.refinery.store.query.dnf.Dnf; +import tools.refinery.store.reasoning.internal.ReasoningBuilderImpl; +import tools.refinery.store.reasoning.interpretation.AnyPartialInterpretation; +import tools.refinery.store.reasoning.interpretation.PartialInterpretation; +import tools.refinery.store.reasoning.literal.Concreteness; +import tools.refinery.store.reasoning.refinement.AnyPartialInterpretationRefiner; +import tools.refinery.store.reasoning.refinement.PartialInterpretationRefiner; import tools.refinery.store.reasoning.representation.AnyPartialSymbol; import tools.refinery.store.reasoning.representation.PartialRelation; import tools.refinery.store.reasoning.representation.PartialSymbol; +import tools.refinery.store.tuple.Tuple1; public interface ReasoningAdapter extends ModelAdapter { - PartialRelation EXISTS = PartialSymbol.of("exists", 1); - PartialRelation EQUALS = PartialSymbol.of("equals", 2); + PartialRelation EXISTS_SYMBOL = PartialSymbol.of("exists", 1); + PartialRelation EQUALS_SYMBOL = PartialSymbol.of("equals", 2); @Override ReasoningStoreAdapter getStoreAdapter(); - default AnyPartialInterpretation getPartialInterpretation(AnyPartialSymbol partialSymbol) { - // Cast to disambiguate overloads. - var typedPartialSymbol = (PartialSymbol) partialSymbol; - return getPartialInterpretation(typedPartialSymbol); + default AnyPartialInterpretation getPartialInterpretation(Concreteness concreteness, + AnyPartialSymbol partialSymbol) { + return getPartialInterpretation(concreteness, (PartialSymbol) partialSymbol); } - PartialInterpretation getPartialInterpretation(PartialSymbol partialSymbol); + PartialInterpretation getPartialInterpretation(Concreteness concreteness, + PartialSymbol partialSymbol); - ResultSet getLiftedResultSet(Dnf query); + default AnyPartialInterpretationRefiner getRefiner(AnyPartialSymbol partialSymbol) { + return getRefiner((PartialSymbol) partialSymbol); + } + + PartialInterpretationRefiner getRefiner(PartialSymbol partialSymbol); + + @Nullable + Tuple1 split(int parentMultiObject); + + boolean cleanup(int nodeToDelete); + + static ReasoningBuilder builder() { + return new ReasoningBuilderImpl(); + } } diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/ReasoningBuilder.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/ReasoningBuilder.java index d3a337e8..6d416436 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/ReasoningBuilder.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/ReasoningBuilder.java @@ -7,26 +7,28 @@ package tools.refinery.store.reasoning; import tools.refinery.store.adapter.ModelAdapterBuilder; import tools.refinery.store.model.ModelStore; -import tools.refinery.store.reasoning.literal.Modality; import tools.refinery.store.query.dnf.Dnf; - -import java.util.Collection; -import java.util.List; +import tools.refinery.store.query.dnf.Query; +import tools.refinery.store.reasoning.literal.Concreteness; +import tools.refinery.store.reasoning.literal.Modality; +import tools.refinery.store.reasoning.refinement.PartialModelInitializer; +import tools.refinery.store.reasoning.refinement.StorageRefiner; +import tools.refinery.store.reasoning.translator.AnyPartialSymbolTranslator; +import tools.refinery.store.representation.Symbol; @SuppressWarnings("UnusedReturnValue") public interface ReasoningBuilder extends ModelAdapterBuilder { - default ReasoningBuilder liftedQueries(Dnf... liftedQueries) { - return liftedQueries(List.of(liftedQueries)); - } + ReasoningBuilder initialNodeCount(int nodeCount); + + ReasoningBuilder partialSymbol(AnyPartialSymbolTranslator translator); + + ReasoningBuilder storageRefiner(Symbol symbol, StorageRefiner.Factory refiner); - default ReasoningBuilder liftedQueries(Collection liftedQueries) { - liftedQueries.forEach(this::liftedQuery); - return this; - } + ReasoningBuilder initializer(PartialModelInitializer initializer); - ReasoningBuilder liftedQuery(Dnf liftedQuery); + Query lift(Modality modality, Concreteness concreteness, Query query); - Dnf lift(Modality modality, Dnf query); + Dnf lift(Modality modality, Concreteness concreteness, Dnf dnf); @Override ReasoningStoreAdapter build(ModelStore store); diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/ReasoningStoreAdapter.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/ReasoningStoreAdapter.java index c9795255..fae60d9e 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/ReasoningStoreAdapter.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/ReasoningStoreAdapter.java @@ -8,14 +8,15 @@ package tools.refinery.store.reasoning; import tools.refinery.store.adapter.ModelStoreAdapter; import tools.refinery.store.model.Model; import tools.refinery.store.reasoning.representation.AnyPartialSymbol; -import tools.refinery.store.query.dnf.Dnf; import java.util.Collection; public interface ReasoningStoreAdapter extends ModelStoreAdapter { Collection getPartialSymbols(); - Collection getLiftedQueries(); + Collection getRefinablePartialSymbols(); + + Model createInitialModel(); @Override ReasoningAdapter createModelAdapter(Model model); diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/internal/PartialQueryRewriter.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/internal/PartialQueryRewriter.java new file mode 100644 index 00000000..132022d1 --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/internal/PartialQueryRewriter.java @@ -0,0 +1,103 @@ +/* + * SPDX-FileCopyrightText: 2023 The Refinery Authors + * + * SPDX-License-Identifier: EPL-2.0 + */ +package tools.refinery.store.reasoning.internal; + +import tools.refinery.store.query.dnf.Dnf; +import tools.refinery.store.query.dnf.DnfClause; +import tools.refinery.store.query.literal.AbstractCallLiteral; +import tools.refinery.store.query.literal.Literal; +import tools.refinery.store.query.rewriter.AbstractRecursiveRewriter; +import tools.refinery.store.reasoning.interpretation.PartialRelationRewriter; +import tools.refinery.store.reasoning.lifting.DnfLifter; +import tools.refinery.store.reasoning.literal.Concreteness; +import tools.refinery.store.reasoning.literal.ModalConstraint; +import tools.refinery.store.reasoning.literal.Modality; +import tools.refinery.store.reasoning.representation.PartialRelation; + +import java.util.*; + +class PartialQueryRewriter extends AbstractRecursiveRewriter { + private final DnfLifter lifter; + private final Map relationRewriterMap = new HashMap<>(); + + PartialQueryRewriter(DnfLifter lifter) { + this.lifter = lifter; + } + + public void addRelationRewriter(PartialRelation partialRelation, PartialRelationRewriter interpreter) { + if (relationRewriterMap.put(partialRelation, interpreter) != null) { + throw new IllegalArgumentException("Duplicate partial relation: " + partialRelation); + } + } + + @Override + protected Dnf doRewrite(Dnf dnf) { + var builder = Dnf.builderFrom(dnf); + for (var clause : dnf.getClauses()) { + builder.clause(rewriteClause(clause)); + } + return builder.build(); + } + + private List rewriteClause(DnfClause clause) { + var completedLiterals = new ArrayList(); + var workList = new ArrayDeque<>(clause.literals()); + while (!workList.isEmpty()) { + var literal = workList.removeFirst(); + rewrite(literal, completedLiterals, workList); + } + return completedLiterals; + } + + private void rewrite(Literal literal, List completedLiterals, Deque workList) { + if (!(literal instanceof AbstractCallLiteral callLiteral)) { + completedLiterals.add(literal); + return; + } + var target = callLiteral.getTarget(); + if (target instanceof Dnf dnf) { + rewriteRecursively(callLiteral, dnf, completedLiterals); + } else if (target instanceof ModalConstraint modalConstraint) { + var modality = modalConstraint.modality(); + var concreteness = modalConstraint.concreteness(); + var constraint = modalConstraint.constraint(); + if (constraint instanceof Dnf dnf) { + rewriteRecursively(callLiteral, modality, concreteness, dnf, completedLiterals); + } else if (constraint instanceof PartialRelation partialRelation) { + rewrite(callLiteral, modality, concreteness, partialRelation, workList); + } else { + throw new IllegalArgumentException("Cannot interpret modal constraint: " + modalConstraint); + } + } else { + completedLiterals.add(literal); + } + } + + private void rewriteRecursively(AbstractCallLiteral callLiteral, Modality modality, Concreteness concreteness, + Dnf dnf, List completedLiterals) { + var liftedDnf = lifter.lift(modality, concreteness, dnf); + rewriteRecursively(callLiteral, liftedDnf, completedLiterals); + } + + private void rewriteRecursively(AbstractCallLiteral callLiteral, Dnf dnf, List completedLiterals) { + var rewrittenDnf = rewrite(dnf); + var rewrittenLiteral = callLiteral.withTarget(rewrittenDnf); + completedLiterals.add(rewrittenLiteral); + } + + private void rewrite(AbstractCallLiteral callLiteral, Modality modality, Concreteness concreteness, + PartialRelation partialRelation, Deque workList) { + var rewriter = relationRewriterMap.get(partialRelation); + if (rewriter == null) { + throw new IllegalArgumentException("Do not know how to interpret partial relation: " + partialRelation); + } + var literals = rewriter.rewriteLiteral(callLiteral, modality, concreteness); + int length = literals.size(); + for (int i = length - 1; i >= 0; i--) { + workList.addFirst(literals.get(i)); + } + } +} 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 1bd3ad2e..396c2dcc 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 @@ -5,20 +5,99 @@ */ package tools.refinery.store.reasoning.internal; +import org.jetbrains.annotations.Nullable; +import tools.refinery.store.model.Interpretation; import tools.refinery.store.model.Model; import tools.refinery.store.reasoning.ReasoningAdapter; -import tools.refinery.store.reasoning.PartialInterpretation; +import tools.refinery.store.reasoning.interpretation.AnyPartialInterpretation; +import tools.refinery.store.reasoning.interpretation.PartialInterpretation; +import tools.refinery.store.reasoning.literal.Concreteness; +import tools.refinery.store.reasoning.refinement.AnyPartialInterpretationRefiner; +import tools.refinery.store.reasoning.refinement.PartialInterpretationRefiner; +import tools.refinery.store.reasoning.refinement.StorageRefiner; +import tools.refinery.store.reasoning.representation.AnyPartialSymbol; import tools.refinery.store.reasoning.representation.PartialSymbol; -import tools.refinery.store.query.dnf.Dnf; -import tools.refinery.store.query.resultset.ResultSet; +import tools.refinery.store.representation.Symbol; +import tools.refinery.store.tuple.Tuple; +import tools.refinery.store.tuple.Tuple1; -public class ReasoningAdapterImpl implements ReasoningAdapter { +import java.util.HashMap; +import java.util.Map; + +class ReasoningAdapterImpl implements ReasoningAdapter { + static final Symbol NODE_COUNT_SYMBOL = Symbol.of("MODEL_SIZE", 0, Integer.class, 0); private final Model model; private final ReasoningStoreAdapterImpl storeAdapter; + private final Map[] partialInterpretations; + private final Map refiners; + private final StorageRefiner[] storageRefiners; + private final Interpretation nodeCountInterpretation; ReasoningAdapterImpl(Model model, ReasoningStoreAdapterImpl storeAdapter) { this.model = model; this.storeAdapter = storeAdapter; + + int concretenessLength = Concreteness.values().length; + // Creation of a generic array. + @SuppressWarnings({"unchecked", "squid:S1905"}) + var interpretationsArray = (Map[]) new Map[concretenessLength]; + partialInterpretations = interpretationsArray; + createPartialInterpretations(); + + var refinerFactories = storeAdapter.getSymbolRefiners(); + refiners = new HashMap<>(refinerFactories.size()); + createRefiners(); + + storageRefiners = storeAdapter.createRepresentationRefiners(model); + + nodeCountInterpretation = model.getInterpretation(NODE_COUNT_SYMBOL); + } + + private void createPartialInterpretations() { + int concretenessLength = Concreteness.values().length; + var interpretationFactories = storeAdapter.getSymbolInterpreters(); + for (int i = 0; i < concretenessLength; i++) { + partialInterpretations[i] = new HashMap<>(interpretationFactories.size()); + } + // Create the partial interpretations in order so that factories may refer to interpretations of symbols + // preceding them in the ordered {@code interpretationFactories} map, e.g., for opposite interpretations. + for (var entry : interpretationFactories.entrySet()) { + var partialSymbol = entry.getKey(); + var factory = entry.getValue(); + for (int i = 0; i < concretenessLength; i++) { + var concreteness = Concreteness.values()[i]; + var interpretation = createPartialInterpretation(concreteness, factory, partialSymbol); + partialInterpretations[i].put(partialSymbol, interpretation); + } + } + } + + private PartialInterpretation createPartialInterpretation( + Concreteness concreteness, PartialInterpretation.Factory interpreter, AnyPartialSymbol symbol) { + // The builder only allows well-typed assignment of interpreters to symbols. + @SuppressWarnings("unchecked") + var typedSymbol = (PartialSymbol) symbol; + return interpreter.create(this, concreteness, typedSymbol); + } + + private void createRefiners() { + var refinerFactories = storeAdapter.getSymbolRefiners(); + // Create the partial interpretations refiners in order so that factories may refer to refiners of symbols + // preceding them in the ordered {@code interpretationFactories} map, e.g., for opposite interpretations. + for (var entry : refinerFactories.entrySet()) { + var partialSymbol = entry.getKey(); + var factory = entry.getValue(); + var refiner = createRefiner(factory, partialSymbol); + refiners.put(partialSymbol, refiner); + } + } + + private PartialInterpretationRefiner createRefiner( + PartialInterpretationRefiner.Factory factory, AnyPartialSymbol symbol) { + // The builder only allows well-typed assignment of interpreters to symbols. + @SuppressWarnings("unchecked") + var typedSymbol = (PartialSymbol) symbol; + return factory.create(this, typedSymbol); } @Override @@ -32,12 +111,59 @@ public class ReasoningAdapterImpl implements ReasoningAdapter { } @Override - public PartialInterpretation getPartialInterpretation(PartialSymbol partialSymbol) { - return null; + public PartialInterpretation getPartialInterpretation(Concreteness concreteness, + PartialSymbol partialSymbol) { + var map = partialInterpretations[concreteness.ordinal()]; + var interpretation = map.get(partialSymbol); + if (interpretation == null) { + throw new IllegalArgumentException("No interpretation for partial symbol: " + partialSymbol); + } + // The builder only allows well-typed assignment of interpreters to symbols. + @SuppressWarnings("unchecked") + var typedInterpretation = (PartialInterpretation) interpretation; + return typedInterpretation; + } + + @Override + public PartialInterpretationRefiner getRefiner(PartialSymbol partialSymbol) { + var refiner = refiners.get(partialSymbol); + if (refiner == null) { + throw new IllegalArgumentException("No refiner for partial symbol: " + partialSymbol); + } + // The builder only allows well-typed assignment of refiners to symbols. + @SuppressWarnings("unchecked") + var typedRefiner = (PartialInterpretationRefiner) refiner; + return typedRefiner; + } + + @Override + @Nullable + public Tuple1 split(int parentNode) { + int newNodeId = nodeCountInterpretation.get(Tuple.of()); + nodeCountInterpretation.put(Tuple.of(), newNodeId + 1); + // Avoid creating an iterator object. + //noinspection ForLoopReplaceableByForEach + for (int i = 0; i < storageRefiners.length; i++) { + if (!storageRefiners[i].split(parentNode, newNodeId)) { + return null; + } + } + return Tuple.of(newNodeId); } @Override - public ResultSet getLiftedResultSet(Dnf query) { - return null; + public boolean cleanup(int nodeToDelete) { + // Avoid creating an iterator object. + //noinspection ForLoopReplaceableByForEach + for (int i = 0; i < storageRefiners.length; i++) { + if (!storageRefiners[i].cleanup(nodeToDelete)) { + return false; + } + } + int currentModelSize = nodeCountInterpretation.get(Tuple.of()); + if (nodeToDelete == currentModelSize - 1) { + nodeCountInterpretation.put(Tuple.of(), nodeToDelete); + } + return true; } } diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/internal/ReasoningBuilderImpl.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/internal/ReasoningBuilderImpl.java index aa71496c..f7a91284 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/internal/ReasoningBuilderImpl.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/internal/ReasoningBuilderImpl.java @@ -7,25 +7,138 @@ package tools.refinery.store.reasoning.internal; import tools.refinery.store.adapter.AbstractModelAdapterBuilder; import tools.refinery.store.model.ModelStore; +import tools.refinery.store.model.ModelStoreBuilder; +import tools.refinery.store.query.ModelQueryBuilder; import tools.refinery.store.query.dnf.Dnf; +import tools.refinery.store.query.dnf.Query; import tools.refinery.store.reasoning.ReasoningBuilder; +import tools.refinery.store.reasoning.interpretation.PartialInterpretation; +import tools.refinery.store.reasoning.refinement.DefaultStorageRefiner; +import tools.refinery.store.reasoning.translator.AnyPartialSymbolTranslator; +import tools.refinery.store.reasoning.translator.PartialRelationTranslator; +import tools.refinery.store.reasoning.lifting.DnfLifter; +import tools.refinery.store.reasoning.literal.Concreteness; import tools.refinery.store.reasoning.literal.Modality; +import tools.refinery.store.reasoning.refinement.PartialInterpretationRefiner; +import tools.refinery.store.reasoning.refinement.PartialModelInitializer; +import tools.refinery.store.reasoning.refinement.StorageRefiner; +import tools.refinery.store.reasoning.representation.AnyPartialSymbol; +import tools.refinery.store.representation.AnySymbol; +import tools.refinery.store.representation.Symbol; + +import java.util.*; public class ReasoningBuilderImpl extends AbstractModelAdapterBuilder implements ReasoningBuilder { + private final DnfLifter lifter = new DnfLifter(); + private final PartialQueryRewriter queryRewriter = new PartialQueryRewriter(lifter); + private final Map translators = new LinkedHashMap<>(); + private final Map> symbolInterpreters = new LinkedHashMap<>(); + private final Map> symbolRefiners = + new LinkedHashMap<>(); + private final Map> registeredStorageRefiners = new LinkedHashMap<>(); + private final List initializers = new ArrayList<>(); + private int initialNodeCount = 0; + + @Override + public ReasoningBuilder initialNodeCount(int nodeCount) { + if (nodeCount < 0) { + throw new IllegalArgumentException("Initial model size must not be negative"); + } + initialNodeCount = nodeCount; + return this; + } + @Override - public ReasoningBuilder liftedQuery(Dnf liftedQuery) { - return null; + public ReasoningBuilder partialSymbol(AnyPartialSymbolTranslator translator) { + var partialSymbol = translator.getPartialSymbol(); + var oldConfiguration = translators.put(partialSymbol, translator); + if (oldConfiguration != null && oldConfiguration != translator) { + throw new IllegalArgumentException("Duplicate configuration for symbol: " + partialSymbol); + } + return this; } @Override - public Dnf lift(Modality modality, Dnf query) { + public ReasoningBuilder storageRefiner(Symbol symbol, StorageRefiner.Factory refiner) { checkNotConfigured(); - return null; + if (registeredStorageRefiners.put(symbol, refiner) != null) { + throw new IllegalArgumentException("Duplicate representation refiner for symbol: " + symbol); + } + return this; + } + + @Override + public ReasoningBuilder initializer(PartialModelInitializer initializer) { + checkNotConfigured(); + initializers.add(initializer); + return this; + } + + @Override + public Query lift(Modality modality, Concreteness concreteness, Query query) { + return lifter.lift(modality, concreteness, query); + } + + @Override + public Dnf lift(Modality modality, Concreteness concreteness, Dnf dnf) { + return lifter.lift(modality, concreteness, dnf); + } + + @Override + protected void doConfigure(ModelStoreBuilder storeBuilder) { + storeBuilder.symbols(ReasoningAdapterImpl.NODE_COUNT_SYMBOL); + for (var translator : translators.values()) { + translator.configure(storeBuilder); + if (translator instanceof PartialRelationTranslator relationConfiguration) { + doConfigure(relationConfiguration); + } else { + throw new IllegalArgumentException("Unknown partial symbol translator %s for partial symbol %s" + .formatted(translator, translator.getPartialSymbol())); + } + } + storeBuilder.symbols(registeredStorageRefiners.keySet()); + var queryBuilder = storeBuilder.getAdapter(ModelQueryBuilder.class); + queryBuilder.rewriter(queryRewriter); + } + + private void doConfigure(PartialRelationTranslator relationConfiguration) { + var partialRelation = relationConfiguration.getPartialRelation(); + queryRewriter.addRelationRewriter(partialRelation, relationConfiguration.getRewriter()); + symbolInterpreters.put(partialRelation, relationConfiguration.getInterpretationFactory()); + var refiner = relationConfiguration.getInterpretationRefiner(); + if (refiner != null) { + symbolRefiners.put(partialRelation, refiner); + } } @Override public ReasoningStoreAdapterImpl doBuild(ModelStore store) { - return null; + return new ReasoningStoreAdapterImpl(store, initialNodeCount, Collections.unmodifiableMap(symbolInterpreters), + Collections.unmodifiableMap(symbolRefiners), getStorageRefiners(store), + Collections.unmodifiableList(initializers)); + } + + private Map> getStorageRefiners(ModelStore store) { + var symbols = store.getSymbols(); + var storageRefiners = new LinkedHashMap>(symbols.size()); + for (var symbol : symbols) { + var refiner = registeredStorageRefiners.remove(symbol); + if (refiner == null) { + if (symbol.arity() == 0) { + // Arity-0 symbols don't need a default refiner, because they are unaffected by object + // creation/removal. Only a custom refiner ({@code refiner != null}) might need to update them. + continue; + } + // By default, copy over all affected tuples on object creation and remove all affected tuples on + // object removal. + refiner = DefaultStorageRefiner.factory(); + } + storageRefiners.put(symbol, refiner); + } + if (!registeredStorageRefiners.isEmpty()) { + throw new IllegalArgumentException("Unused storage refiners: " + registeredStorageRefiners.keySet()); + } + return Collections.unmodifiableMap(storageRefiners); } } diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/internal/ReasoningStoreAdapterImpl.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/internal/ReasoningStoreAdapterImpl.java index cdddd8d6..e8b581c6 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/internal/ReasoningStoreAdapterImpl.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/internal/ReasoningStoreAdapterImpl.java @@ -5,19 +5,45 @@ */ package tools.refinery.store.reasoning.internal; -import tools.refinery.store.reasoning.ReasoningStoreAdapter; import tools.refinery.store.model.Model; import tools.refinery.store.model.ModelStore; +import tools.refinery.store.query.ModelQueryAdapter; +import tools.refinery.store.reasoning.ReasoningStoreAdapter; +import tools.refinery.store.reasoning.interpretation.PartialInterpretation; +import tools.refinery.store.reasoning.refinement.PartialInterpretationRefiner; +import tools.refinery.store.reasoning.refinement.PartialModelInitializer; +import tools.refinery.store.reasoning.refinement.StorageRefiner; import tools.refinery.store.reasoning.representation.AnyPartialSymbol; -import tools.refinery.store.query.dnf.Dnf; +import tools.refinery.store.representation.AnySymbol; +import tools.refinery.store.representation.Symbol; +import tools.refinery.store.tuple.Tuple; import java.util.Collection; +import java.util.List; +import java.util.Map; -public class ReasoningStoreAdapterImpl implements ReasoningStoreAdapter { +class ReasoningStoreAdapterImpl implements ReasoningStoreAdapter { private final ModelStore store; + private final Map> symbolInterpreters; + private final Map> symbolRefiners; + private final Map> representationRefiners; + private final Object initialModelLock = new Object(); + private final int initialNodeCount; + private List initializers; + private long initialCommitId = Model.NO_STATE_ID; - ReasoningStoreAdapterImpl(ModelStore store) { + ReasoningStoreAdapterImpl(ModelStore store, + int initialNodeCount, + Map> symbolInterpreters, + Map> symbolRefiners, + Map> representationRefiners, + List initializers) { this.store = store; + this.initialNodeCount = initialNodeCount; + this.symbolInterpreters = symbolInterpreters; + this.symbolRefiners = symbolRefiners; + this.representationRefiners = representationRefiners; + this.initializers = initializers; } @Override @@ -27,12 +53,65 @@ public class ReasoningStoreAdapterImpl implements ReasoningStoreAdapter { @Override public Collection getPartialSymbols() { - return null; + return symbolInterpreters.keySet(); } @Override - public Collection getLiftedQueries() { - return null; + public Collection getRefinablePartialSymbols() { + return symbolRefiners.keySet(); + } + + // Use of wildcard return value only in internal method not exposed as API, so there is less chance of confusion. + @SuppressWarnings("squid:S1452") + Map> getSymbolInterpreters() { + return symbolInterpreters; + } + + // Use of wildcard return value only in internal method not exposed as API, so there is less chance of confusion. + @SuppressWarnings("squid:S1452") + Map> getSymbolRefiners() { + return symbolRefiners; + } + + StorageRefiner[] createRepresentationRefiners(Model model) { + var refiners = new StorageRefiner[representationRefiners.size()]; + int i = 0; + for (var entry : representationRefiners.entrySet()) { + var symbol = entry.getKey(); + var factory = entry.getValue(); + refiners[i] = createRepresentationRefiner(factory, model, symbol); + } + return refiners; + } + + private StorageRefiner createRepresentationRefiner( + StorageRefiner.Factory factory, Model model, AnySymbol symbol) { + // The builder only allows well-typed assignment of refiners to symbols. + @SuppressWarnings("unchecked") + var typedSymbol = (Symbol) symbol; + return factory.create(typedSymbol, model); + } + + @Override + public Model createInitialModel() { + synchronized (initialModelLock) { + if (initialCommitId == Model.NO_STATE_ID) { + return doCreateInitialModel(); + } + return store.createModelForState(initialCommitId); + } + } + + private Model doCreateInitialModel() { + var model = store.createEmptyModel(); + model.getInterpretation(ReasoningAdapterImpl.NODE_COUNT_SYMBOL).put(Tuple.of(), initialNodeCount); + for (var initializer : initializers) { + initializer.initialize(model, initialNodeCount); + } + model.getAdapter(ModelQueryAdapter.class).flushChanges(); + initialCommitId = model.commit(); + initializers = null; + return model; } @Override 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 new file mode 100644 index 00000000..ed291eac --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/interpretation/AbstractPartialInterpretation.java @@ -0,0 +1,38 @@ +/* + * SPDX-FileCopyrightText: 2023 The Refinery Authors + * + * SPDX-License-Identifier: EPL-2.0 + */ +package tools.refinery.store.reasoning.interpretation; + +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 { + private final ReasoningAdapter adapter; + private final PartialSymbol partialSymbol; + private final Concreteness concreteness; + + protected AbstractPartialInterpretation(ReasoningAdapter adapter, Concreteness concreteness, + PartialSymbol partialSymbol) { + this.adapter = adapter; + this.partialSymbol = partialSymbol; + this.concreteness = concreteness; + } + + @Override + public ReasoningAdapter getAdapter() { + return adapter; + } + + @Override + public PartialSymbol getPartialSymbol() { + return partialSymbol; + } + + @Override + public Concreteness getConcreteness() { + return concreteness; + } +} diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/interpretation/AnyPartialInterpretation.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/interpretation/AnyPartialInterpretation.java new file mode 100644 index 00000000..cd709bc4 --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/interpretation/AnyPartialInterpretation.java @@ -0,0 +1,18 @@ +/* + * SPDX-FileCopyrightText: 2021-2023 The Refinery Authors + * + * SPDX-License-Identifier: EPL-2.0 + */ +package tools.refinery.store.reasoning.interpretation; + +import tools.refinery.store.reasoning.ReasoningAdapter; +import tools.refinery.store.reasoning.literal.Concreteness; +import tools.refinery.store.reasoning.representation.AnyPartialSymbol; + +public sealed interface AnyPartialInterpretation permits PartialInterpretation { + ReasoningAdapter getAdapter(); + + AnyPartialSymbol getPartialSymbol(); + + Concreteness getConcreteness(); +} 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 new file mode 100644 index 00000000..3d3d6056 --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/interpretation/PartialInterpretation.java @@ -0,0 +1,26 @@ +/* + * SPDX-FileCopyrightText: 2021-2023 The Refinery Authors + * + * SPDX-License-Identifier: EPL-2.0 + */ +package tools.refinery.store.reasoning.interpretation; + +import tools.refinery.store.map.Cursor; +import tools.refinery.store.reasoning.ReasoningAdapter; +import tools.refinery.store.reasoning.literal.Concreteness; +import tools.refinery.store.reasoning.representation.PartialSymbol; +import tools.refinery.store.tuple.Tuple; + +public non-sealed interface PartialInterpretation extends AnyPartialInterpretation { + @Override + PartialSymbol getPartialSymbol(); + + A get(Tuple key); + + Cursor getAll(); + + interface Factory { + PartialInterpretation create(ReasoningAdapter adapter, Concreteness concreteness, + PartialSymbol partialSymbol); + } +} diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/interpretation/PartialRelationRewriter.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/interpretation/PartialRelationRewriter.java new file mode 100644 index 00000000..da8ae0a8 --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/interpretation/PartialRelationRewriter.java @@ -0,0 +1,17 @@ +/* + * SPDX-FileCopyrightText: 2023 The Refinery Authors + * + * SPDX-License-Identifier: EPL-2.0 + */ +package tools.refinery.store.reasoning.interpretation; + +import tools.refinery.store.query.literal.AbstractCallLiteral; +import tools.refinery.store.query.literal.Literal; +import tools.refinery.store.reasoning.literal.Concreteness; +import tools.refinery.store.reasoning.literal.Modality; + +import java.util.List; + +public interface PartialRelationRewriter { + List rewriteLiteral(AbstractCallLiteral literal, Modality modality, Concreteness concreteness); +} diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/interpretation/QueryBasedRelationInterpretationFactory.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/interpretation/QueryBasedRelationInterpretationFactory.java new file mode 100644 index 00000000..2535714a --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/interpretation/QueryBasedRelationInterpretationFactory.java @@ -0,0 +1,180 @@ +/* + * SPDX-FileCopyrightText: 2023 The Refinery Authors + * + * SPDX-License-Identifier: EPL-2.0 + */ +package tools.refinery.store.reasoning.interpretation; + +import tools.refinery.store.map.Cursor; +import tools.refinery.store.query.ModelQueryAdapter; +import tools.refinery.store.query.dnf.Query; +import tools.refinery.store.query.resultset.ResultSet; +import tools.refinery.store.reasoning.ReasoningAdapter; +import tools.refinery.store.reasoning.literal.Concreteness; +import tools.refinery.store.reasoning.representation.PartialSymbol; +import tools.refinery.store.representation.TruthValue; +import tools.refinery.store.tuple.Tuple; + +public class QueryBasedRelationInterpretationFactory implements PartialInterpretation.Factory { + private final Query may; + private final Query must; + private final Query candidateMay; + private final Query candidateMust; + + public QueryBasedRelationInterpretationFactory( + Query may, Query must, Query candidateMay, Query candidateMust) { + this.may = may; + this.must = must; + this.candidateMay = candidateMay; + this.candidateMust = candidateMust; + } + + @Override + public PartialInterpretation create( + ReasoningAdapter adapter, Concreteness concreteness, PartialSymbol partialSymbol) { + var queryEngine = adapter.getModel().getAdapter(ModelQueryAdapter.class); + ResultSet mayResultSet; + ResultSet mustResultSet; + switch (concreteness) { + case PARTIAL -> { + mayResultSet = queryEngine.getResultSet(may); + mustResultSet = queryEngine.getResultSet(must); + } + case CANDIDATE -> { + mayResultSet = queryEngine.getResultSet(candidateMay); + mustResultSet = queryEngine.getResultSet(candidateMust); + } + default -> throw new IllegalArgumentException("Unknown concreteness: " + concreteness); + } + if (mayResultSet.equals(mustResultSet)) { + return new TwoValuedInterpretation(adapter, concreteness, partialSymbol, mustResultSet); + } else { + return new FourValuedInterpretation( + adapter, concreteness, partialSymbol, mayResultSet, mustResultSet); + } + } + + private static class TwoValuedInterpretation extends AbstractPartialInterpretation { + private final ResultSet resultSet; + + protected TwoValuedInterpretation( + ReasoningAdapter adapter, Concreteness concreteness, PartialSymbol partialSymbol, + ResultSet resultSet) { + super(adapter, concreteness, partialSymbol); + this.resultSet = resultSet; + } + + @Override + public TruthValue get(Tuple key) { + return TruthValue.toTruthValue(resultSet.get(key)); + } + + @Override + public Cursor getAll() { + return new TwoValuedCursor(resultSet.getAll()); + } + + private record TwoValuedCursor(Cursor cursor) implements Cursor { + @Override + public Tuple getKey() { + return cursor.getKey(); + } + + @Override + public TruthValue getValue() { + return TruthValue.toTruthValue(cursor.getValue()); + } + + @Override + public boolean isTerminated() { + return cursor.isTerminated(); + } + + @Override + public boolean move() { + return cursor.move(); + } + } + } + + private static class FourValuedInterpretation extends AbstractPartialInterpretation { + private final ResultSet mayResultSet; + private final ResultSet mustResultSet; + + public FourValuedInterpretation( + ReasoningAdapter adapter, Concreteness concreteness, PartialSymbol partialSymbol, + ResultSet mayResultSet, ResultSet mustResultSet) { + super(adapter, concreteness, partialSymbol); + this.mayResultSet = mayResultSet; + this.mustResultSet = mustResultSet; + } + + @Override + public TruthValue get(Tuple key) { + boolean isMay = mayResultSet.get(key); + boolean isMust = mustResultSet.get(key); + if (isMust) { + return isMay ? TruthValue.TRUE : TruthValue.ERROR; + } else { + return isMay ? TruthValue.UNKNOWN : TruthValue.FALSE; + } + } + + @Override + public Cursor getAll() { + return new FourValuedCursor(); + } + + private final class FourValuedCursor implements Cursor { + private final Cursor mayCursor; + private Cursor mustCursor; + + private FourValuedCursor() { + this.mayCursor = mayResultSet.getAll(); + } + + @Override + public Tuple getKey() { + return mustCursor == null ? mayCursor.getKey() : mustCursor.getKey(); + } + + @Override + public TruthValue getValue() { + if (mustCursor != null) { + return TruthValue.ERROR; + } + if (Boolean.TRUE.equals(mustResultSet.get(mayCursor.getKey()))) { + return TruthValue.TRUE; + } + return TruthValue.UNKNOWN; + } + + @Override + public boolean isTerminated() { + return mustCursor != null && mustCursor.isTerminated(); + } + + @Override + public boolean move() { + if (mayCursor.isTerminated()) { + return moveMust(); + } + if (mayCursor.move()) { + return true; + } + mustCursor = mustResultSet.getAll(); + return moveMust(); + } + + private boolean moveMust() { + while (mustCursor.move()) { + // We already iterated over {@code TRUE} truth values with {@code mayCursor}. + if (!Boolean.TRUE.equals(mayResultSet.get(mustCursor.getKey()))) { + return true; + } + } + return false; + } + } + } +} diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/interpretation/QueryBasedRelationRewriter.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/interpretation/QueryBasedRelationRewriter.java new file mode 100644 index 00000000..3be9e9ac --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/interpretation/QueryBasedRelationRewriter.java @@ -0,0 +1,44 @@ +/* + * SPDX-FileCopyrightText: 2023 The Refinery Authors + * + * SPDX-License-Identifier: EPL-2.0 + */ +package tools.refinery.store.reasoning.interpretation; + +import tools.refinery.store.query.dnf.Query; +import tools.refinery.store.query.literal.AbstractCallLiteral; +import tools.refinery.store.query.literal.Literal; +import tools.refinery.store.reasoning.literal.Concreteness; +import tools.refinery.store.reasoning.literal.Modality; + +import java.util.List; + +public class QueryBasedRelationRewriter implements PartialRelationRewriter { + private final Query may; + private final Query must; + private final Query candidateMay; + private final Query candidateMust; + + public QueryBasedRelationRewriter(Query may, Query must, Query candidateMay, + Query candidateMust) { + this.may = may; + this.must = must; + this.candidateMay = candidateMay; + this.candidateMust = candidateMust; + } + + @Override + public List rewriteLiteral(AbstractCallLiteral literal, Modality modality, Concreteness concreteness) { + var query = switch (concreteness) { + case PARTIAL -> switch (modality) { + case MAY -> may; + case MUST -> must; + }; + case CANDIDATE -> switch (modality) { + case MAY -> candidateMay; + case MUST -> candidateMust; + }; + }; + return List.of(literal.withTarget(query.getDnf())); + } +} diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/lifting/ClauseLifter.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/lifting/ClauseLifter.java index d3b0ace8..7bf092a3 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/lifting/ClauseLifter.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/lifting/ClauseLifter.java @@ -54,7 +54,7 @@ class ClauseLifter { var liftedLiteral = liftLiteral(literal); liftedLiterals.add(liftedLiteral); } - var existsConstraint = ModalConstraint.of(modality, concreteness, ReasoningAdapter.EXISTS); + var existsConstraint = ModalConstraint.of(modality, concreteness, ReasoningAdapter.EXISTS_SYMBOL); for (var quantifiedVariable : existentialQuantifiersToAdd) { liftedLiterals.add(existsConstraint.call(quantifiedVariable)); } @@ -117,7 +117,7 @@ class ClauseLifter { var liftedConstraint = ModalConstraint.of(negatedModality, concreteness, target); literals.add(liftedConstraint.call(CallPolarity.POSITIVE, originalArguments)); - var existsConstraint = ModalConstraint.of(negatedModality, concreteness, ReasoningAdapter.EXISTS); + var existsConstraint = ModalConstraint.of(negatedModality, concreteness, ReasoningAdapter.EXISTS_SYMBOL); for (var variable : uniqueOriginalArguments) { if (privateVariables.contains(variable)) { literals.add(existsConstraint.call(variable)); @@ -134,7 +134,7 @@ class ClauseLifter { var originalArguments = callLiteral.getArguments(); var liftedTarget = ModalConstraint.of(modality, concreteness, target); - var existsConstraint = ModalConstraint.of(modality, concreteness, ReasoningAdapter.EXISTS); + var existsConstraint = ModalConstraint.of(modality, concreteness, ReasoningAdapter.EXISTS_SYMBOL); var existingEndHelperName = "%s#exisitingEnd#%s#%s".formatted(target.name(), modality, concreteness); var existingEndHelper = Dnf.of(existingEndHelperName, builder -> { var start = builder.parameter("start"); @@ -171,10 +171,10 @@ class ClauseLifter { private Literal liftEquivalenceLiteral(EquivalenceLiteral equivalenceLiteral) { if (equivalenceLiteral.isPositive()) { - return ModalConstraint.of(modality, concreteness, ReasoningAdapter.EQUALS) + return ModalConstraint.of(modality, concreteness, ReasoningAdapter.EQUALS_SYMBOL) .call(CallPolarity.POSITIVE, equivalenceLiteral.getLeft(), equivalenceLiteral.getRight()); } - return ModalConstraint.of(modality.negate(), concreteness, ReasoningAdapter.EQUALS) + return ModalConstraint.of(modality.negate(), concreteness, ReasoningAdapter.EQUALS_SYMBOL) .call(CallPolarity.NEGATIVE, equivalenceLiteral.getLeft(), equivalenceLiteral.getRight()); } } diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/lifting/DnfLifter.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/lifting/DnfLifter.java index c3b23b43..2e68fa3e 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/lifting/DnfLifter.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/lifting/DnfLifter.java @@ -7,6 +7,7 @@ package tools.refinery.store.reasoning.lifting; import tools.refinery.store.query.dnf.Dnf; import tools.refinery.store.query.dnf.DnfClause; +import tools.refinery.store.query.dnf.Query; import tools.refinery.store.query.equality.DnfEqualityChecker; import tools.refinery.store.query.literal.Literal; import tools.refinery.store.reasoning.literal.Concreteness; @@ -19,6 +20,11 @@ import java.util.Map; public class DnfLifter { private final Map cache = new HashMap<>(); + public Query lift(Modality modality, Concreteness concreteness, Query query) { + var liftedDnf = lift(modality, concreteness, query.getDnf()); + return query.withDnf(liftedDnf); + } + public Dnf lift(Modality modality, Concreteness concreteness, Dnf dnf) { return cache.computeIfAbsent(new ModalDnf(modality, concreteness, dnf), this::doLift); } diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/literal/PartialLiterals.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/literal/PartialLiterals.java index 4f07f17d..2c879397 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/literal/PartialLiterals.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/literal/PartialLiterals.java @@ -13,20 +13,28 @@ public final class PartialLiterals { } public static CallLiteral may(CallLiteral literal) { - return addModality(literal, Modality.MAY); + return addModality(literal, Modality.MAY, Concreteness.PARTIAL); } public static CallLiteral must(CallLiteral literal) { - return addModality(literal, Modality.MUST); + return addModality(literal, Modality.MUST, Concreteness.PARTIAL); } - public static CallLiteral addModality(CallLiteral literal, Modality modality) { + public static CallLiteral candidateMay(CallLiteral literal) { + return addModality(literal, Modality.MAY, Concreteness.CANDIDATE); + } + + public static CallLiteral candidateMust(CallLiteral literal) { + return addModality(literal, Modality.MUST, Concreteness.CANDIDATE); + } + + public static CallLiteral addModality(CallLiteral literal, Modality modality, Concreteness concreteness) { var target = literal.getTarget(); if (target instanceof ModalConstraint) { throw new IllegalArgumentException("Literal %s already has modality".formatted(literal)); } var polarity = literal.getPolarity(); - var modalTarget = new ModalConstraint(modality.commute(polarity), target); + var modalTarget = new ModalConstraint(modality.commute(polarity), concreteness, target); return new CallLiteral(polarity, modalTarget, literal.getArguments()); } } diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/refinement/AnyPartialInterpretationRefiner.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/refinement/AnyPartialInterpretationRefiner.java new file mode 100644 index 00000000..6c381511 --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/refinement/AnyPartialInterpretationRefiner.java @@ -0,0 +1,15 @@ +/* + * SPDX-FileCopyrightText: 2023 The Refinery Authors + * + * SPDX-License-Identifier: EPL-2.0 + */ +package tools.refinery.store.reasoning.refinement; + +import tools.refinery.store.reasoning.ReasoningAdapter; +import tools.refinery.store.reasoning.representation.AnyPartialSymbol; + +public sealed interface AnyPartialInterpretationRefiner permits PartialInterpretationRefiner { + ReasoningAdapter getAdapter(); + + AnyPartialSymbol getPartialSymbol(); +} 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 new file mode 100644 index 00000000..756118a0 --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/refinement/ConcreteSymbolRefiner.java @@ -0,0 +1,51 @@ +/* + * SPDX-FileCopyrightText: 2023 The Refinery Authors + * + * SPDX-License-Identifier: EPL-2.0 + */ +package tools.refinery.store.reasoning.refinement; + +import tools.refinery.store.model.Interpretation; +import tools.refinery.store.reasoning.ReasoningAdapter; +import tools.refinery.store.reasoning.representation.PartialSymbol; +import tools.refinery.store.representation.Symbol; +import tools.refinery.store.tuple.Tuple; + +import java.util.Objects; + +public class ConcreteSymbolRefiner implements PartialInterpretationRefiner { + private final ReasoningAdapter adapter; + private final PartialSymbol partialSymbol; + private final Interpretation interpretation; + + public ConcreteSymbolRefiner(ReasoningAdapter adapter, PartialSymbol partialSymbol, + Symbol concreteSymbol) { + this.adapter = adapter; + this.partialSymbol = partialSymbol; + interpretation = adapter.getModel().getInterpretation(concreteSymbol); + } + + @Override + public ReasoningAdapter getAdapter() { + return adapter; + } + + @Override + public PartialSymbol getPartialSymbol() { + return partialSymbol; + } + + @Override + public boolean merge(Tuple key, A value) { + var currentValue = interpretation.get(key); + var mergedValue = partialSymbol.abstractDomain().commonRefinement(currentValue, value); + if (!Objects.equals(currentValue, mergedValue)) { + interpretation.put(key, mergedValue); + } + return true; + } + + public static PartialInterpretationRefiner.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/DefaultStorageRefiner.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/refinement/DefaultStorageRefiner.java new file mode 100644 index 00000000..0d7d6c5c --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/refinement/DefaultStorageRefiner.java @@ -0,0 +1,80 @@ +/* + * SPDX-FileCopyrightText: 2023 The Refinery Authors + * + * SPDX-License-Identifier: EPL-2.0 + */ +package tools.refinery.store.reasoning.refinement; + +import tools.refinery.store.model.Interpretation; +import tools.refinery.store.tuple.Tuple; + +public class DefaultStorageRefiner implements StorageRefiner { + private static final StorageRefiner.Factory FACTORY = (symbol, model) -> { + var interpretation = model.getInterpretation(symbol); + return new DefaultStorageRefiner<>(interpretation); + }; + + private final Interpretation interpretation; + + public DefaultStorageRefiner(Interpretation interpretation) { + this.interpretation = interpretation; + } + + @Override + public boolean split(int parentNode, int childNode) { + var symbol = interpretation.getSymbol(); + int arity = symbol.arity(); + for (int i = 0; i < arity; i++) { + int adjacentSize = interpretation.getAdjacentSize(i, parentNode); + if (adjacentSize == 0) { + continue; + } + var toSetKeys = new Tuple[adjacentSize]; + // This is safe, because we won't pass the array to the outside. + @SuppressWarnings("unchecked") + var toSetValues = (T[]) new Object[adjacentSize]; + var cursor = interpretation.getAdjacent(i, parentNode); + int j = 0; + while (cursor.move()) { + toSetKeys[j] = cursor.getKey().set(i, childNode); + toSetValues[j] = cursor.getValue(); + j++; + } + for (j = 0; j < adjacentSize; j++) { + interpretation.put(toSetKeys[j], toSetValues[j]); + } + } + return true; + } + + @Override + public boolean cleanup(int nodeToDelete) { + var symbol = interpretation.getSymbol(); + int arity = symbol.arity(); + var defaultValue = symbol.defaultValue(); + for (int i = 0; i < arity; i++) { + int adjacentSize = interpretation.getAdjacentSize(i, nodeToDelete); + if (adjacentSize == 0) { + continue; + } + var toDelete = new Tuple[adjacentSize]; + var cursor = interpretation.getAdjacent(i, nodeToDelete); + int j = 0; + while (cursor.move()) { + toDelete[j] = cursor.getKey(); + j++; + } + for (j = 0; j < adjacentSize; j++) { + interpretation.put(toDelete[j], defaultValue); + } + } + return true; + } + + public static StorageRefiner.Factory factory() { + // This is safe, because {@code FACTORY} doesn't depend on {@code T} at all. + @SuppressWarnings("unchecked") + var typedFactory = (StorageRefiner.Factory) FACTORY; + return typedFactory; + } +} 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 new file mode 100644 index 00000000..f48d1d1f --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/refinement/PartialInterpretationRefiner.java @@ -0,0 +1,22 @@ +/* + * SPDX-FileCopyrightText: 2023 The Refinery Authors + * + * SPDX-License-Identifier: EPL-2.0 + */ +package tools.refinery.store.reasoning.refinement; + +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 { + @Override + PartialSymbol getPartialSymbol(); + + boolean merge(Tuple key, A value); + + @FunctionalInterface + interface Factory { + PartialInterpretationRefiner create(ReasoningAdapter adapter, PartialSymbol partialSymbol); + } +} diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/refinement/PartialModelInitializer.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/refinement/PartialModelInitializer.java new file mode 100644 index 00000000..79c1670f --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/refinement/PartialModelInitializer.java @@ -0,0 +1,13 @@ +/* + * SPDX-FileCopyrightText: 2023 The Refinery Authors + * + * SPDX-License-Identifier: EPL-2.0 + */ +package tools.refinery.store.reasoning.refinement; + +import tools.refinery.store.model.Model; + +@FunctionalInterface +public interface PartialModelInitializer { + void initialize(Model model, int nodeCount); +} diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/refinement/StorageRefiner.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/refinement/StorageRefiner.java new file mode 100644 index 00000000..004696fd --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/refinement/StorageRefiner.java @@ -0,0 +1,20 @@ +/* + * SPDX-FileCopyrightText: 2023 The Refinery Authors + * + * SPDX-License-Identifier: EPL-2.0 + */ +package tools.refinery.store.reasoning.refinement; + +import tools.refinery.store.model.Model; +import tools.refinery.store.representation.Symbol; + +public interface StorageRefiner { + boolean split(int parentNode, int childNode); + + boolean cleanup(int nodeToDelete); + + @FunctionalInterface + interface Factory { + StorageRefiner create(Symbol symbol, Model model); + } +} 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 d58d026f..e59c8af8 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 @@ -14,11 +14,6 @@ public record PartialFunction(String name, int arity, AbstractDomain return null; } - @Override - public C defaultConcreteValue() { - return null; - } - @Override public boolean equals(Object o) { return this == o; diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/representation/PartialRelation.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/representation/PartialRelation.java index 6b2f050b..4ccb7033 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/representation/PartialRelation.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/representation/PartialRelation.java @@ -25,11 +25,6 @@ public record PartialRelation(String name, int arity) implements PartialSymbol getParameters() { var parameters = new Parameter[arity]; 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 2f04534a..38b2e466 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 @@ -13,8 +13,6 @@ public sealed interface PartialSymbol extends AnyPartialSymbol permits Par A defaultValue(); - C defaultConcreteValue(); - static PartialRelation of(String name, int arity) { return new PartialRelation(name, arity); } diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/seed/MapBasedSeed.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/seed/MapBasedSeed.java new file mode 100644 index 00000000..b5a3d844 --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/seed/MapBasedSeed.java @@ -0,0 +1,117 @@ +/* + * SPDX-FileCopyrightText: 2023 The Refinery Authors + * + * SPDX-License-Identifier: EPL-2.0 + */ +package tools.refinery.store.reasoning.seed; + +import tools.refinery.store.map.Cursor; +import tools.refinery.store.map.Cursors; +import tools.refinery.store.tuple.Tuple; + +import java.util.Map; +import java.util.Objects; + +record MapBasedSeed(int arity, Class valueType, T reducedValue, Map map) implements Seed { + @Override + public T get(Tuple key) { + var value = map.get(key); + return value == null ? reducedValue : value; + } + + @Override + public Cursor getCursor(T defaultValue, int nodeCount) { + if (Objects.equals(defaultValue, reducedValue)) { + return Cursors.of(map); + } + return new CartesianProductCursor<>(arity, nodeCount, reducedValue, defaultValue, map); + } + + private static class CartesianProductCursor implements Cursor { + private final int nodeCount; + private final T reducedValue; + private final T defaultValue; + private final Map map; + private final int[] counter; + private State state = State.INITIAL; + private Tuple key; + private T value; + + private CartesianProductCursor(int arity, int nodeCount, T reducedValue, T defaultValue, Map map) { + this.nodeCount = nodeCount; + this.reducedValue = reducedValue; + this.defaultValue = defaultValue; + this.map = map; + counter = new int[arity]; + } + + @Override + public Tuple getKey() { + return key; + } + + @Override + public T getValue() { + return value; + } + + @Override + public boolean isTerminated() { + return state == State.TERMINATED; + } + + @Override + public boolean move() { + return switch (state) { + case INITIAL -> { + state = State.STARTED; + yield checkValue() || moveToNext(); + } + case STARTED -> moveToNext(); + case TERMINATED -> false; + }; + } + + private boolean moveToNext() { + do { + increment(); + } while (!checkValue()); + return state != State.TERMINATED; + } + + private void increment() { + int i = counter.length - 1; + while (i >= 0) { + counter[i]++; + if (counter[i] < nodeCount) { + return; + } + counter[i] = 0; + i--; + } + } + + private boolean checkValue() { + if (state == State.TERMINATED) { + return false; + } + if (counter[0] >= nodeCount) { + state = State.TERMINATED; + return false; + } + key = Tuple.of(counter); + var valueInMap = map.get(key); + if (Objects.equals(valueInMap, defaultValue)) { + return false; + } + value = valueInMap == null ? reducedValue : valueInMap; + return true; + } + + private enum State { + INITIAL, + STARTED, + TERMINATED + } + } +} 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 08079f12..64b98683 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 @@ -6,14 +6,68 @@ package tools.refinery.store.reasoning.seed; import tools.refinery.store.map.Cursor; +import tools.refinery.store.reasoning.representation.PartialSymbol; +import tools.refinery.store.representation.Symbol; import tools.refinery.store.tuple.Tuple; +import java.util.Collections; +import java.util.LinkedHashMap; +import java.util.Map; + public interface Seed { int arity(); + Class valueType(); + T reducedValue(); T get(Tuple key); Cursor getCursor(T defaultValue, int nodeCount); + + static Builder builder(int arity, Class valueType, T reducedValue) { + return new Builder<>(arity, valueType, reducedValue); + } + + static Builder builder(Symbol symbol) { + return builder(symbol.arity(), symbol.valueType(), symbol.defaultValue()); + } + + static Builder builder(PartialSymbol partialSymbol) { + return builder(partialSymbol.arity(), partialSymbol.abstractDomain().abstractType(), + partialSymbol.defaultValue()); + } + + @SuppressWarnings("UnusedReturnValue") + class Builder { + private final int arity; + private final Class valueType; + private final T reducedValue; + private final Map map = new LinkedHashMap<>(); + + private Builder(int arity, Class valueType, T reducedValue) { + this.arity = arity; + this.valueType = valueType; + this.reducedValue = reducedValue; + } + + public Builder put(Tuple key, T value) { + if (key.getSize() != arity) { + throw new IllegalArgumentException("Expected %s to have %d elements".formatted(key, arity)); + } + map.put(key, value); + return this; + } + + public Builder putAll(Map map) { + for (var entry : map.entrySet()) { + put(entry.getKey(), entry.getValue()); + } + return this; + } + + public Seed build() { + return new MapBasedSeed<>(arity, valueType, reducedValue, Collections.unmodifiableMap(map)); + } + } } 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 new file mode 100644 index 00000000..884d6515 --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/seed/SeedInitializer.java @@ -0,0 +1,27 @@ +/* + * SPDX-FileCopyrightText: 2023 The Refinery Authors + * + * SPDX-License-Identifier: EPL-2.0 + */ +package tools.refinery.store.reasoning.seed; + +import tools.refinery.store.model.Model; +import tools.refinery.store.reasoning.refinement.PartialModelInitializer; +import tools.refinery.store.representation.Symbol; + +public class SeedInitializer implements PartialModelInitializer { + private final Symbol symbol; + private final Seed seed; + + public SeedInitializer(Symbol symbol, Seed seed) { + this.symbol = symbol; + this.seed = seed; + } + + @Override + public void initialize(Model model, int nodeCount) { + var interpretation = model.getInterpretation(symbol); + var cursor = seed.getCursor(symbol.defaultValue(), nodeCount); + interpretation.putAll(cursor); + } +} diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/seed/UniformSeed.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/seed/UniformSeed.java deleted file mode 100644 index 451d1513..00000000 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/seed/UniformSeed.java +++ /dev/null @@ -1,27 +0,0 @@ -/* - * SPDX-FileCopyrightText: 2021-2023 The Refinery Authors - * - * SPDX-License-Identifier: EPL-2.0 - */ -package tools.refinery.store.reasoning.seed; - -import tools.refinery.store.map.Cursor; -import tools.refinery.store.tuple.Tuple; - -public record UniformSeed(int arity, T reducedValue) implements Seed { - public UniformSeed { - if (arity < 0) { - throw new IllegalArgumentException("Arity must not be negative"); - } - } - - @Override - public T get(Tuple key) { - return reducedValue; - } - - @Override - public Cursor getCursor(T defaultValue, int nodeCount) { - return null; - } -} diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/Advice.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/Advice.java deleted file mode 100644 index d6a9e02c..00000000 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/Advice.java +++ /dev/null @@ -1,159 +0,0 @@ -/* - * SPDX-FileCopyrightText: 2021-2023 The Refinery Authors - * - * SPDX-License-Identifier: EPL-2.0 - */ -package tools.refinery.store.reasoning.translator; - -import tools.refinery.store.query.substitution.Substitution; -import tools.refinery.store.reasoning.representation.AnyPartialSymbol; -import tools.refinery.store.reasoning.representation.PartialRelation; -import tools.refinery.store.query.term.Variable; -import tools.refinery.store.query.literal.Literal; - -import java.util.*; - -public final class Advice { - private final AnyPartialSymbol source; - private final PartialRelation target; - private final AdviceSlot slot; - private final boolean mandatory; - private final List parameters; - private final List literals; - private boolean processed; - - public Advice(AnyPartialSymbol source, PartialRelation target, AdviceSlot slot, boolean mandatory, List parameters, List literals) { - if (mandatory && !slot.isMonotonic()) { - throw new IllegalArgumentException("Only monotonic advice can be mandatory"); - } - this.source = source; - this.target = target; - this.slot = slot; - this.mandatory = mandatory; - checkArity(parameters); - this.parameters = parameters; - this.literals = literals; - } - - public AnyPartialSymbol source() { - return source; - } - - public PartialRelation target() { - return target; - } - - public AdviceSlot slot() { - return slot; - } - - public boolean mandatory() { - return mandatory; - } - - public List parameters() { - return parameters; - } - - public List literals() { - return literals; - } - - public boolean processed() { - return processed; - } - - public List substitute(List substituteParameters) { - checkArity(substituteParameters); - markProcessed(); - // Use a renewing substitution to remove any non-parameter variables and avoid clashed between variables - // coming from different advice in the same clause. - var substitution = Substitution.builder().putManyChecked(parameters, substituteParameters).renewing().build(); - return literals.stream().map(literal -> literal.substitute(substitution)).toList(); - } - - private void markProcessed() { - processed = true; - } - - public void checkProcessed() { - if (mandatory && !processed) { - throw new IllegalStateException("Mandatory advice %s was not processed".formatted(this)); - } - } - - private void checkArity(List toCheck) { - if (toCheck.size() != target.arity()) { - throw new IllegalArgumentException("%s needs %d parameters, but got %s".formatted(target.name(), - target.arity(), parameters.size())); - } - } - - public static Builder builderFor(AnyPartialSymbol source, PartialRelation target, AdviceSlot slot) { - return new Builder(source, target, slot); - } - - - @Override - public String toString() { - return "Advice[source=%s, target=%s, slot=%s, mandatory=%s, parameters=%s, literals=%s]".formatted(source, - target, slot, mandatory, parameters, literals); - } - - public static class Builder { - private final AnyPartialSymbol source; - private final PartialRelation target; - private final AdviceSlot slot; - private boolean mandatory; - private final List parameters = new ArrayList<>(); - private final List literals = new ArrayList<>(); - - private Builder(AnyPartialSymbol source, PartialRelation target, AdviceSlot slot) { - this.source = source; - this.target = target; - this.slot = slot; - } - - public Builder mandatory(boolean mandatory) { - this.mandatory = mandatory; - return this; - } - - public Builder mandatory() { - return mandatory(false); - } - - public Builder parameters(List variables) { - parameters.addAll(variables); - return this; - } - - public Builder parameters(Variable... variables) { - return parameters(List.of(variables)); - } - - public Builder parameter(Variable variable) { - parameters.add(variable); - return this; - } - - public Builder literals(Collection literals) { - this.literals.addAll(literals); - return this; - } - - public Builder literals(Literal... literals) { - return literals(List.of(literals)); - } - - public Builder literal(Literal literal) { - literals.add(literal); - return this; - } - - public Advice build() { - return new Advice(source, target, slot, mandatory, Collections.unmodifiableList(parameters), - Collections.unmodifiableList(literals)); - } - } -} diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/AdviceSlot.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/AdviceSlot.java deleted file mode 100644 index bab20340..00000000 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/AdviceSlot.java +++ /dev/null @@ -1,30 +0,0 @@ -/* - * SPDX-FileCopyrightText: 2021-2023 The Refinery Authors - * - * SPDX-License-Identifier: EPL-2.0 - */ -package tools.refinery.store.reasoning.translator; - -import tools.refinery.store.representation.TruthValue; - -public enum AdviceSlot { - EXTEND_MUST(true), - - RESTRICT_MAY(true), - - /** - * Same as {@link #RESTRICT_MAY}, but only active if the value of the relation is not {@link TruthValue#TRUE} or - * {@link TruthValue#ERROR}. - */ - RESTRICT_NEW(false); - - private final boolean monotonic; - - AdviceSlot(boolean monotonic) { - this.monotonic = monotonic; - } - - public boolean isMonotonic() { - return monotonic; - } -} diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/AnyPartialSymbolTranslator.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/AnyPartialSymbolTranslator.java new file mode 100644 index 00000000..48c84348 --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/AnyPartialSymbolTranslator.java @@ -0,0 +1,16 @@ +/* + * SPDX-FileCopyrightText: 2023 The Refinery Authors + * + * SPDX-License-Identifier: EPL-2.0 + */ +package tools.refinery.store.reasoning.translator; + +import tools.refinery.store.model.ModelStoreBuilder; +import tools.refinery.store.model.ModelStoreConfiguration; +import tools.refinery.store.reasoning.representation.AnyPartialSymbol; + +public sealed interface AnyPartialSymbolTranslator extends ModelStoreConfiguration permits PartialSymbolTranslator { + AnyPartialSymbol getPartialSymbol(); + + void configure(ModelStoreBuilder storeBuilder); +} diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/PartialRelationTranslator.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/PartialRelationTranslator.java new file mode 100644 index 00000000..fe8e8d6c --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/PartialRelationTranslator.java @@ -0,0 +1,263 @@ +/* + * SPDX-FileCopyrightText: 2023 The Refinery Authors + * + * SPDX-License-Identifier: EPL-2.0 + */ +package tools.refinery.store.reasoning.translator; + +import tools.refinery.store.model.ModelStoreBuilder; +import tools.refinery.store.query.Constraint; +import tools.refinery.store.query.ModelQueryBuilder; +import tools.refinery.store.query.dnf.Query; +import tools.refinery.store.query.dnf.RelationalQuery; +import tools.refinery.store.query.term.Variable; +import tools.refinery.store.query.view.MayView; +import tools.refinery.store.query.view.MustView; +import tools.refinery.store.reasoning.ReasoningBuilder; +import tools.refinery.store.reasoning.interpretation.PartialInterpretation; +import tools.refinery.store.reasoning.interpretation.PartialRelationRewriter; +import tools.refinery.store.reasoning.interpretation.QueryBasedRelationInterpretationFactory; +import tools.refinery.store.reasoning.interpretation.QueryBasedRelationRewriter; +import tools.refinery.store.reasoning.literal.Concreteness; +import tools.refinery.store.reasoning.literal.Modality; +import tools.refinery.store.reasoning.refinement.ConcreteSymbolRefiner; +import tools.refinery.store.reasoning.refinement.PartialInterpretationRefiner; +import tools.refinery.store.reasoning.refinement.StorageRefiner; +import tools.refinery.store.reasoning.representation.PartialRelation; +import tools.refinery.store.representation.AnySymbol; +import tools.refinery.store.representation.Symbol; +import tools.refinery.store.representation.TruthValue; + +@SuppressWarnings("UnusedReturnValue") +public final class PartialRelationTranslator extends PartialSymbolTranslator { + private final PartialRelation partialRelation; + private PartialRelationRewriter rewriter; + private Query query; + private Query may; + private Query must; + private Query candidateMay; + private Query candidateMust; + private RoundingMode roundingMode; + + private PartialRelationTranslator(PartialRelation partialRelation) { + super(partialRelation); + this.partialRelation = partialRelation; + } + + public PartialRelation getPartialRelation() { + return partialRelation; + } + + @Override + public PartialRelationTranslator symbol(AnySymbol storageSymbol) { + super.symbol(storageSymbol); + return this; + } + + @Override + public PartialRelationTranslator symbol(Symbol storageSymbol, + StorageRefiner.Factory storageRefiner) { + super.symbol(storageSymbol, storageRefiner); + return this; + } + + @Override + public PartialRelationTranslator interpretation( + PartialInterpretation.Factory interpretationFactory) { + super.interpretation(interpretationFactory); + return this; + } + + @Override + public PartialRelationTranslator refiner( + PartialInterpretationRefiner.Factory interpretationRefiner) { + super.refiner(interpretationRefiner); + return this; + } + + public PartialRelationTranslator rewriter(PartialRelationRewriter rewriter) { + checkNotConfigured(); + if (this.rewriter != null) { + throw new IllegalArgumentException("Rewriter was already set"); + } + this.rewriter = rewriter; + return this; + } + + public PartialRelationTranslator query(RelationalQuery query) { + checkNotConfigured(); + if (this.query != null) { + throw new IllegalArgumentException("Query was already set"); + } + this.query = query; + return this; + } + + public PartialRelationTranslator may(RelationalQuery may) { + checkNotConfigured(); + if (this.may != null) { + throw new IllegalArgumentException("May query was already set"); + } + this.may = may; + return this; + } + + public PartialRelationTranslator must(RelationalQuery must) { + checkNotConfigured(); + if (this.must != null) { + throw new IllegalArgumentException("Must query was already set"); + } + this.must = must; + return this; + } + + public PartialRelationTranslator candidate(RelationalQuery candidate) { + candidateMay(candidate); + candidateMust(candidate); + return this; + } + + public PartialRelationTranslator candidateMay(RelationalQuery candidateMay) { + checkNotConfigured(); + if (this.candidateMay != null) { + throw new IllegalArgumentException("Candidate may query was already set"); + } + this.candidateMay = candidateMay; + return this; + } + + public PartialRelationTranslator candidateMust(RelationalQuery candidateMust) { + checkNotConfigured(); + if (this.candidateMust != null) { + throw new IllegalArgumentException("Candidate must query was already set"); + } + this.candidateMust = candidateMust; + return this; + } + + public PartialRelationTranslator roundingMode(RoundingMode roundingMode) { + checkNotConfigured(); + if (this.roundingMode != null) { + throw new IllegalArgumentException("Rounding mode was already set"); + } + this.roundingMode = roundingMode; + return this; + } + + @Override + protected void doConfigure(ModelStoreBuilder storeBuilder) { + setFallbackRoundingMode(); + createFallbackQueryFromRewriter(); + liftQueries(storeBuilder); + createFallbackQueriesFromSymbol(); + setFallbackCandidateQueries(); + createFallbackRewriter(); + createFallbackInterpretation(storeBuilder); + createFallbackRefiner(); + super.doConfigure(storeBuilder); + } + + private void setFallbackRoundingMode() { + if (roundingMode == null) { + roundingMode = query == null && storageSymbol != null ? RoundingMode.PREFER_FALSE : RoundingMode.NONE; + } + } + + private RelationalQuery createQuery(Constraint constraint) { + int arity = partialRelation.arity(); + var queryBuilder = Query.builder(partialRelation.name()); + var parameters = new Variable[arity]; + for (int i = 0; i < arity; i++) { + parameters[i] = queryBuilder.parameter("p" + 1); + } + queryBuilder.clause(constraint.call(parameters)); + return queryBuilder.build(); + } + + private void createFallbackQueryFromRewriter() { + if (rewriter != null && query == null) { + query = createQuery(partialRelation); + } + } + + private void createFallbackQueriesFromSymbol() { + if (storageSymbol == null || storageSymbol.valueType() != TruthValue.class) { + return; + } + // We checked in the guard clause that this is safe. + @SuppressWarnings("unchecked") + var typedStorageSymbol = (Symbol) storageSymbol; + var defaultValue = typedStorageSymbol.defaultValue(); + if (may == null && !defaultValue.may()) { + may = createQuery(new MayView(typedStorageSymbol)); + } + if (must == null && !defaultValue.must()) { + must = createQuery(new MustView(typedStorageSymbol)); + } + } + + private void liftQueries(ModelStoreBuilder storeBuilder) { + if (query != null) { + var reasoningBuilder = storeBuilder.getAdapter(ReasoningBuilder.class); + if (may == null) { + may = reasoningBuilder.lift(Modality.MAY, Concreteness.PARTIAL, query); + } + if (must == null) { + must = reasoningBuilder.lift(Modality.MUST, Concreteness.PARTIAL, query); + } + if (candidateMay == null) { + candidateMay = reasoningBuilder.lift(Modality.MAY, Concreteness.CANDIDATE, query); + } + if (candidateMust == null) { + candidateMust = reasoningBuilder.lift(Modality.MAY, Concreteness.CANDIDATE, query); + } + } + } + + private void setFallbackCandidateQueries() { + if (candidateMay == null) { + candidateMay = switch (roundingMode) { + case NONE, PREFER_TRUE -> may; + case PREFER_FALSE -> must; + }; + } + if (candidateMust == null) { + candidateMust = switch (roundingMode) { + case NONE, PREFER_FALSE -> must; + case PREFER_TRUE -> may; + }; + } + } + + private void createFallbackRewriter() { + if (rewriter == null) { + rewriter = new QueryBasedRelationRewriter(may, must, candidateMay, candidateMust); + } + } + + private void createFallbackInterpretation(ModelStoreBuilder storeBuilder) { + if (interpretationFactory == null) { + var queryBuilder = storeBuilder.getAdapter(ModelQueryBuilder.class); + interpretationFactory = new QueryBasedRelationInterpretationFactory(may, must, candidateMay, candidateMust); + queryBuilder.queries(may, must, candidateMay, candidateMust); + } + } + + private void createFallbackRefiner() { + if (interpretationRefiner == null && storageSymbol != null && storageSymbol.valueType() == TruthValue.class) { + // We checked in the condition that this is safe. + @SuppressWarnings("unchecked") + var typedStorageSymbol = (Symbol) storageSymbol; + interpretationRefiner = ConcreteSymbolRefiner.of(typedStorageSymbol); + } + } + + public PartialRelationRewriter getRewriter() { + checkConfigured(); + return rewriter; + } + + public static PartialRelationTranslator of(PartialRelation relation) { + return new PartialRelationTranslator(relation); + } +} 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 new file mode 100644 index 00000000..07d1d19b --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/PartialSymbolTranslator.java @@ -0,0 +1,156 @@ +/* + * SPDX-FileCopyrightText: 2023 The Refinery Authors + * + * SPDX-License-Identifier: EPL-2.0 + */ +package tools.refinery.store.reasoning.translator; + +import tools.refinery.store.model.ModelStoreBuilder; +import tools.refinery.store.reasoning.ReasoningBuilder; +import tools.refinery.store.reasoning.interpretation.PartialInterpretation; +import tools.refinery.store.reasoning.refinement.PartialInterpretationRefiner; +import tools.refinery.store.reasoning.refinement.PartialModelInitializer; +import tools.refinery.store.reasoning.refinement.StorageRefiner; +import tools.refinery.store.reasoning.representation.PartialSymbol; +import tools.refinery.store.reasoning.seed.Seed; +import tools.refinery.store.reasoning.seed.SeedInitializer; +import tools.refinery.store.representation.AnySymbol; +import tools.refinery.store.representation.Symbol; + +@SuppressWarnings("UnusedReturnValue") +public abstract sealed class PartialSymbolTranslator implements AnyPartialSymbolTranslator + permits PartialRelationTranslator { + private final PartialSymbol partialSymbol; + private boolean configured = false; + protected PartialInterpretationRefiner.Factory interpretationRefiner; + protected AnySymbol storageSymbol; + protected StorageRefiner.Factory storageRefiner; + protected PartialInterpretation.Factory interpretationFactory; + protected PartialModelInitializer initializer; + + PartialSymbolTranslator(PartialSymbol partialSymbol) { + this.partialSymbol = partialSymbol; + } + + @Override + public PartialSymbol getPartialSymbol() { + return partialSymbol; + } + + @Override + public void apply(ModelStoreBuilder storeBuilder) { + storeBuilder.getAdapter(ReasoningBuilder.class).partialSymbol(this); + } + + public boolean isConfigured() { + return configured; + } + + protected void checkConfigured() { + if (!configured) { + throw new IllegalStateException("Partial symbol was not configured"); + } + } + + protected void checkNotConfigured() { + if (configured) { + throw new IllegalStateException("Partial symbol was already configured"); + } + } + + public PartialSymbolTranslator symbol(AnySymbol storageSymbol) { + return symbol((Symbol) storageSymbol, null); + } + + public PartialSymbolTranslator symbol(Symbol storageSymbol, + StorageRefiner.Factory storageRefiner) { + checkNotConfigured(); + if (this.storageSymbol != null) { + throw new IllegalStateException("Representation symbol was already set"); + } + this.storageSymbol = storageSymbol; + this.storageRefiner = storageRefiner; + return this; + } + + public PartialSymbolTranslator interpretation(PartialInterpretation.Factory interpretationFactory) { + checkNotConfigured(); + if (this.interpretationFactory != null) { + throw new IllegalStateException("Interpretation factory was already set"); + } + this.interpretationFactory = interpretationFactory; + return this; + } + + public PartialSymbolTranslator refiner(PartialInterpretationRefiner.Factory interpretationRefiner) { + checkNotConfigured(); + if (this.interpretationRefiner != null) { + throw new IllegalStateException("Interpretation refiner was already set"); + } + this.interpretationRefiner = interpretationRefiner; + return this; + } + + public PartialSymbolTranslator initializer(PartialModelInitializer initializer) { + checkNotConfigured(); + if (this.initializer != null) { + throw new IllegalStateException("Initializer was already set"); + } + this.initializer = initializer; + return this; + } + + public PartialSymbolTranslator seed(Seed seed) { + if (storageSymbol == null) { + throw new IllegalArgumentException("Seed requires setting a storage symbol"); + } + if (!seed.valueType().equals(storageSymbol.valueType())) { + throw new IllegalArgumentException("Seed type %s does not match storage symbol type %s" + .formatted(seed.valueType(), storageSymbol.valueType())); + } + // The guard clause only allows a well-typed seed. + @SuppressWarnings("unchecked") + var typedStorageSymbol = (Symbol) storageSymbol; + return initializer(new SeedInitializer<>(typedStorageSymbol, seed)); + } + + @Override + public void configure(ModelStoreBuilder storeBuilder) { + checkNotConfigured(); + doConfigure(storeBuilder); + configured = true; + } + + protected void doConfigure(ModelStoreBuilder storeBuilder) { + if (interpretationFactory == null) { + throw new IllegalArgumentException("Interpretation factory must be set"); + } + var reasoningBuilder = storeBuilder.getAdapter(ReasoningBuilder.class); + if (storageSymbol != null) { + storeBuilder.symbol(storageSymbol); + if (storageRefiner != null) { + registerStorageRefiner(reasoningBuilder, storageRefiner); + } + } + if (initializer != null) { + reasoningBuilder.initializer(initializer); + } + } + + private void registerStorageRefiner(ReasoningBuilder reasoningBuilder, StorageRefiner.Factory factory) { + // The builder only allows setting a well-typed representation refiner. + @SuppressWarnings("unchecked") + var typedStorageSymbol = (Symbol) storageSymbol; + reasoningBuilder.storageRefiner(typedStorageSymbol, factory); + } + + public PartialInterpretation.Factory getInterpretationFactory() { + checkConfigured(); + return interpretationFactory; + } + + public PartialInterpretationRefiner.Factory getInterpretationRefiner() { + checkConfigured(); + return interpretationRefiner; + } +} diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/RoundingMode.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/RoundingMode.java new file mode 100644 index 00000000..dd956a50 --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/RoundingMode.java @@ -0,0 +1,12 @@ +/* + * SPDX-FileCopyrightText: 2023 The Refinery Authors + * + * SPDX-License-Identifier: EPL-2.0 + */ +package tools.refinery.store.reasoning.translator; + +public enum RoundingMode { + NONE, + PREFER_TRUE, + PREFER_FALSE +} diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/TranslatedRelation.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/TranslatedRelation.java deleted file mode 100644 index 4a5a8843..00000000 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/TranslatedRelation.java +++ /dev/null @@ -1,27 +0,0 @@ -/* - * SPDX-FileCopyrightText: 2021-2023 The Refinery Authors - * - * SPDX-License-Identifier: EPL-2.0 - */ -package tools.refinery.store.reasoning.translator; - -import tools.refinery.store.model.Model; -import tools.refinery.store.query.term.Variable; -import tools.refinery.store.query.literal.CallPolarity; -import tools.refinery.store.query.literal.Literal; -import tools.refinery.store.reasoning.PartialInterpretation; -import tools.refinery.store.reasoning.literal.Modality; -import tools.refinery.store.reasoning.representation.PartialRelation; -import tools.refinery.store.representation.TruthValue; - -import java.util.List; - -public interface TranslatedRelation { - PartialRelation getSource(); - - void configure(List advices); - - List call(CallPolarity polarity, Modality modality, List arguments); - - PartialInterpretation createPartialInterpretation(Model model); -} diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/TranslationUnit.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/TranslationUnit.java deleted file mode 100644 index 6e44a7d7..00000000 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/TranslationUnit.java +++ /dev/null @@ -1,32 +0,0 @@ -/* - * SPDX-FileCopyrightText: 2021-2023 The Refinery Authors - * - * SPDX-License-Identifier: EPL-2.0 - */ -package tools.refinery.store.reasoning.translator; - -import tools.refinery.store.model.Model; -import tools.refinery.store.reasoning.ReasoningBuilder; - -import java.util.Collection; - -public abstract class TranslationUnit { - private ReasoningBuilder reasoningBuilder; - - protected ReasoningBuilder getReasoningBuilder() { - return reasoningBuilder; - } - - public void setPartialInterpretationBuilder(ReasoningBuilder reasoningBuilder) { - this.reasoningBuilder = reasoningBuilder; - configureReasoningBuilder(); - } - - protected void configureReasoningBuilder() { - // Nothing to configure by default. - } - - public abstract Collection getTranslatedRelations(); - - public abstract void initializeModel(Model model, int nodeCount); -} diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/base/BaseDecisionInterpretation.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/base/BaseDecisionInterpretation.java deleted file mode 100644 index 2a151aa2..00000000 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/base/BaseDecisionInterpretation.java +++ /dev/null @@ -1,93 +0,0 @@ -/* - * SPDX-FileCopyrightText: 2021-2023 The Refinery Authors - * - * SPDX-License-Identifier: EPL-2.0 - */ -package tools.refinery.store.reasoning.translator.base; - -import tools.refinery.store.map.Cursor; -import tools.refinery.store.model.Interpretation; -import tools.refinery.store.query.resultset.ResultSet; -import tools.refinery.store.reasoning.MergeResult; -import tools.refinery.store.reasoning.PartialInterpretation; -import tools.refinery.store.reasoning.ReasoningAdapter; -import tools.refinery.store.reasoning.representation.PartialRelation; -import tools.refinery.store.representation.TruthValue; -import tools.refinery.store.tuple.Tuple; - -public class BaseDecisionInterpretation implements PartialInterpretation { - private final ReasoningAdapter reasoningAdapter; - private PartialRelation partialRelation; - private final ResultSet mustResultSet; - private final ResultSet mayResultSet; - private final ResultSet errorResultSet; - private final ResultSet currentResultSet; - private final Interpretation interpretation; - - public BaseDecisionInterpretation(ReasoningAdapter reasoningAdapter, ResultSet mustResultSet, - ResultSet mayResultSet, ResultSet errorResultSet, - ResultSet currentResultSet, Interpretation interpretation) { - this.reasoningAdapter = reasoningAdapter; - this.mustResultSet = mustResultSet; - this.mayResultSet = mayResultSet; - this.errorResultSet = errorResultSet; - this.currentResultSet = currentResultSet; - this.interpretation = interpretation; - } - - @Override - public ReasoningAdapter getAdapter() { - return reasoningAdapter; - } - - @Override - public int countUnfinished() { - return 0; - } - - @Override - public int countErrors() { - return errorResultSet.size(); - } - - @Override - public PartialRelation getPartialSymbol() { - return partialRelation; - } - - @Override - public TruthValue get(Tuple key) { - return null; - } - - @Override - public Cursor getAll() { - return null; - } - - @Override - public MergeResult merge(Tuple key, TruthValue value) { - TruthValue newValue; - switch (value) { - case UNKNOWN -> { - return MergeResult.UNCHANGED; - } - case TRUE -> newValue = mayResultSet.get(key) ? TruthValue.TRUE : TruthValue.ERROR; - case FALSE -> newValue = mustResultSet.get(key) ? TruthValue.ERROR : TruthValue.FALSE; - case ERROR -> newValue = TruthValue.ERROR; - default -> throw new IllegalArgumentException("Unknown truth value: " + value); - } - var oldValue = interpretation.put(key, newValue); - return oldValue == TruthValue.ERROR ? MergeResult.UNCHANGED : MergeResult.REFINED; - } - - @Override - public Boolean getConcrete(Tuple key) { - return currentResultSet.get(key); - } - - @Override - public Cursor getAllConcrete() { - return null; - } -} diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/base/BaseDecisionTranslationUnit.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/base/BaseDecisionTranslationUnit.java deleted file mode 100644 index a1e4b816..00000000 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/base/BaseDecisionTranslationUnit.java +++ /dev/null @@ -1,49 +0,0 @@ -/* - * SPDX-FileCopyrightText: 2021-2023 The Refinery Authors - * - * SPDX-License-Identifier: EPL-2.0 - */ -package tools.refinery.store.reasoning.translator.base; - -import tools.refinery.store.model.Model; -import tools.refinery.store.reasoning.representation.PartialRelation; -import tools.refinery.store.reasoning.seed.Seed; -import tools.refinery.store.reasoning.seed.UniformSeed; -import tools.refinery.store.reasoning.translator.TranslatedRelation; -import tools.refinery.store.reasoning.translator.TranslationUnit; -import tools.refinery.store.representation.Symbol; -import tools.refinery.store.representation.TruthValue; - -import java.util.Collection; -import java.util.List; - -public class BaseDecisionTranslationUnit extends TranslationUnit { - private final PartialRelation partialRelation; - private final Seed seed; - private final Symbol symbol; - - public BaseDecisionTranslationUnit(PartialRelation partialRelation, Seed seed) { - if (seed.arity() != partialRelation.arity()) { - throw new IllegalArgumentException("Expected seed with arity %d for %s, got arity %s" - .formatted(partialRelation.arity(), partialRelation, seed.arity())); - } - this.partialRelation = partialRelation; - this.seed = seed; - symbol = Symbol.of(partialRelation.name(), partialRelation.arity(), TruthValue.class, TruthValue.UNKNOWN); - } - - public BaseDecisionTranslationUnit(PartialRelation partialRelation) { - this(partialRelation, new UniformSeed<>(partialRelation.arity(), TruthValue.UNKNOWN)); - } - - @Override - public Collection getTranslatedRelations() { - return List.of(new TranslatedBaseDecision(getReasoningBuilder(), partialRelation, symbol)); - } - - @Override - public void initializeModel(Model model, int nodeCount) { - var interpretation = model.getInterpretation(symbol); - interpretation.putAll(seed.getCursor(TruthValue.UNKNOWN, nodeCount)); - } -} diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/base/TranslatedBaseDecision.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/base/TranslatedBaseDecision.java deleted file mode 100644 index 4782eb46..00000000 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/base/TranslatedBaseDecision.java +++ /dev/null @@ -1,54 +0,0 @@ -/* - * SPDX-FileCopyrightText: 2021-2023 The Refinery Authors - * - * SPDX-License-Identifier: EPL-2.0 - */ -package tools.refinery.store.reasoning.translator.base; - -import tools.refinery.store.model.Model; -import tools.refinery.store.query.term.Variable; -import tools.refinery.store.query.literal.CallPolarity; -import tools.refinery.store.query.literal.Literal; -import tools.refinery.store.reasoning.PartialInterpretation; -import tools.refinery.store.reasoning.ReasoningBuilder; -import tools.refinery.store.reasoning.literal.Modality; -import tools.refinery.store.reasoning.representation.PartialRelation; -import tools.refinery.store.reasoning.translator.Advice; -import tools.refinery.store.reasoning.translator.TranslatedRelation; -import tools.refinery.store.representation.Symbol; -import tools.refinery.store.representation.TruthValue; - -import java.util.List; - -class TranslatedBaseDecision implements TranslatedRelation { - private final ReasoningBuilder reasoningBuilder; - private final PartialRelation partialRelation; - private final Symbol symbol; - - public TranslatedBaseDecision(ReasoningBuilder reasoningBuilder, PartialRelation partialRelation, - Symbol symbol) { - this.reasoningBuilder = reasoningBuilder; - this.partialRelation = partialRelation; - this.symbol = symbol; - } - - @Override - public PartialRelation getSource() { - return partialRelation; - } - - @Override - public void configure(List advices) { - - } - - @Override - public List call(CallPolarity polarity, Modality modality, List arguments) { - return null; - } - - @Override - public PartialInterpretation createPartialInterpretation(Model model) { - return null; - } -} diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/InferredMayTypeView.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/InferredMayTypeView.java deleted file mode 100644 index 40de4644..00000000 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/InferredMayTypeView.java +++ /dev/null @@ -1,40 +0,0 @@ -/* - * SPDX-FileCopyrightText: 2021-2023 The Refinery Authors - * - * SPDX-License-Identifier: EPL-2.0 - */ -package tools.refinery.store.reasoning.translator.typehierarchy; - -import tools.refinery.store.reasoning.representation.PartialRelation; -import tools.refinery.store.query.view.TuplePreservingView; -import tools.refinery.store.tuple.Tuple; - -import java.util.Objects; - -class InferredMayTypeView extends TuplePreservingView { - private final PartialRelation type; - - InferredMayTypeView(PartialRelation type) { - super(TypeHierarchyTranslationUnit.INFERRED_TYPE_SYMBOL, "%s#may".formatted(type)); - this.type = type; - } - - @Override - protected boolean doFilter(Tuple key, InferredType value) { - return value.mayConcreteTypes().contains(type); - } - - @Override - public boolean equals(Object o) { - if (this == o) return true; - if (o == null || getClass() != o.getClass()) return false; - if (!super.equals(o)) return false; - InferredMayTypeView that = (InferredMayTypeView) o; - return Objects.equals(type, that.type); - } - - @Override - public int hashCode() { - return Objects.hash(super.hashCode(), type); - } -} diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/InferredMustTypeView.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/InferredMustTypeView.java deleted file mode 100644 index 1a121547..00000000 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/InferredMustTypeView.java +++ /dev/null @@ -1,40 +0,0 @@ -/* - * SPDX-FileCopyrightText: 2021-2023 The Refinery Authors - * - * SPDX-License-Identifier: EPL-2.0 - */ -package tools.refinery.store.reasoning.translator.typehierarchy; - -import tools.refinery.store.reasoning.representation.PartialRelation; -import tools.refinery.store.query.view.TuplePreservingView; -import tools.refinery.store.tuple.Tuple; - -import java.util.Objects; - -class InferredMustTypeView extends TuplePreservingView { - private final PartialRelation type; - - InferredMustTypeView(PartialRelation type) { - super(TypeHierarchyTranslationUnit.INFERRED_TYPE_SYMBOL, "%s#must".formatted(type)); - this.type = type; - } - - @Override - protected boolean doFilter(Tuple key, InferredType value) { - return value.mustTypes().contains(type); - } - - @Override - public boolean equals(Object o) { - if (this == o) return true; - if (o == null || getClass() != o.getClass()) return false; - if (!super.equals(o)) return false; - InferredMustTypeView that = (InferredMustTypeView) o; - return Objects.equals(type, that.type); - } - - @Override - public int hashCode() { - return Objects.hash(super.hashCode(), type); - } -} diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeHierarchyTranslationUnit.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeHierarchyTranslationUnit.java deleted file mode 100644 index 06e3c05f..00000000 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeHierarchyTranslationUnit.java +++ /dev/null @@ -1,37 +0,0 @@ -/* - * SPDX-FileCopyrightText: 2021-2023 The Refinery Authors - * - * SPDX-License-Identifier: EPL-2.0 - */ -package tools.refinery.store.reasoning.translator.typehierarchy; - -import tools.refinery.store.model.Model; -import tools.refinery.store.reasoning.representation.PartialRelation; -import tools.refinery.store.reasoning.translator.TranslatedRelation; -import tools.refinery.store.reasoning.translator.TranslationUnit; -import tools.refinery.store.representation.Symbol; - -import java.util.Collection; -import java.util.List; -import java.util.Map; - -public class TypeHierarchyTranslationUnit extends TranslationUnit { - static final Symbol INFERRED_TYPE_SYMBOL = Symbol.of( - "inferredType", 1, InferredType.class, InferredType.UNTYPED); - - private final TypeAnalyzer typeAnalyzer; - - public TypeHierarchyTranslationUnit(Map typeInfoMap) { - typeAnalyzer = new TypeAnalyzer(typeInfoMap); - } - - @Override - public Collection getTranslatedRelations() { - return List.of(); - } - - @Override - public void initializeModel(Model model, int nodeCount) { - - } -} -- cgit v1.2.3-54-g00ecf