From 71372b4d57b1c51cd892aa07343c3dbc8de3e727 Mon Sep 17 00:00:00 2001 From: Kristóf Marussy Date: Sat, 25 Feb 2023 00:55:36 +0100 Subject: refactor: rename PartialInterpretation adapter --- .../store/reasoning/AnyPartialInterpretation.java | 13 ++ .../refinery/store/reasoning/MergeResult.java | 15 ++ .../store/reasoning/PartialInterpretation.java | 22 +++ .../tools/refinery/store/reasoning/Reasoning.java | 24 +++ .../refinery/store/reasoning/ReasoningAdapter.java | 22 +++ .../refinery/store/reasoning/ReasoningBuilder.java | 28 +++ .../store/reasoning/ReasoningStoreAdapter.java | 17 ++ .../reasoning/internal/ReasoningAdapterImpl.java | 38 ++++ .../reasoning/internal/ReasoningBuilderImpl.java | 29 +++ .../internal/ReasoningStoreAdapterImpl.java | 37 ++++ .../store/reasoning/lifting/DnfLifter.java | 107 +++++++++++ .../refinery/store/reasoning/lifting/ModalDnf.java | 11 ++ .../reasoning/literal/ModalDnfCallLiteral.java | 48 +++++ .../store/reasoning/literal/ModalLiteral.java | 63 +++++++ .../reasoning/literal/ModalRelationLiteral.java | 37 ++++ .../refinery/store/reasoning/literal/Modality.java | 31 ++++ .../store/reasoning/literal/PartialLiterals.java | 33 ++++ .../reasoning/literal/PartialRelationLiteral.java | 32 ++++ .../representation/AnyPartialFunction.java | 4 + .../reasoning/representation/AnyPartialSymbol.java | 11 ++ .../reasoning/representation/PartialFunction.java | 32 ++++ .../reasoning/representation/PartialRelation.java | 66 +++++++ .../reasoning/representation/PartialSymbol.java | 12 ++ .../reasoning/rule/RelationRefinementAction.java | 36 ++++ .../tools/refinery/store/reasoning/rule/Rule.java | 38 ++++ .../refinery/store/reasoning/rule/RuleAction.java | 12 ++ .../store/reasoning/rule/RuleActionExecutor.java | 9 + .../store/reasoning/rule/RuleExecutor.java | 34 ++++ .../store/reasoning/translator/Advice.java | 159 ++++++++++++++++ .../store/reasoning/translator/AdviceSlot.java | 25 +++ .../refinery/store/reasoning/translator/Seed.java | 12 ++ .../reasoning/translator/TranslationUnit.java | 48 +++++ .../translator/typehierarchy/EliminatedType.java | 6 + .../translator/typehierarchy/ExtendedTypeInfo.java | 101 ++++++++++ .../typehierarchy/InferredMayTypeRelationView.java | 19 ++ .../InferredMustTypeRelationView.java | 19 ++ .../translator/typehierarchy/InferredType.java | 30 +++ .../translator/typehierarchy/PreservedType.java | 136 ++++++++++++++ .../typehierarchy/TypeAnalysisResult.java | 4 + .../translator/typehierarchy/TypeAnalyzer.java | 202 ++++++++++++++++++++ .../TypeHierarchyTranslationUnit.java | 52 ++++++ .../translator/typehierarchy/TypeInfo.java | 46 +++++ .../translator/typehierarchy/InferredTypeTest.java | 32 ++++ .../TypeAnalyzerExampleHierarchyTest.java | 203 +++++++++++++++++++++ .../translator/typehierarchy/TypeAnalyzerTest.java | 200 ++++++++++++++++++++ .../typehierarchy/TypeAnalyzerTester.java | 51 ++++++ 46 files changed, 2206 insertions(+) create mode 100644 subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/AnyPartialInterpretation.java create mode 100644 subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/MergeResult.java create 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/Reasoning.java create mode 100644 subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/ReasoningAdapter.java create mode 100644 subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/ReasoningBuilder.java create mode 100644 subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/ReasoningStoreAdapter.java create mode 100644 subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/internal/ReasoningAdapterImpl.java create mode 100644 subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/internal/ReasoningBuilderImpl.java create mode 100644 subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/internal/ReasoningStoreAdapterImpl.java create mode 100644 subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/lifting/DnfLifter.java create mode 100644 subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/lifting/ModalDnf.java create mode 100644 subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/literal/ModalDnfCallLiteral.java create mode 100644 subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/literal/ModalLiteral.java create mode 100644 subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/literal/ModalRelationLiteral.java create mode 100644 subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/literal/Modality.java create mode 100644 subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/literal/PartialLiterals.java create mode 100644 subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/literal/PartialRelationLiteral.java create mode 100644 subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/representation/AnyPartialFunction.java create mode 100644 subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/representation/AnyPartialSymbol.java create mode 100644 subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/representation/PartialFunction.java create mode 100644 subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/representation/PartialRelation.java create mode 100644 subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/representation/PartialSymbol.java create mode 100644 subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/rule/RelationRefinementAction.java create mode 100644 subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/rule/Rule.java create mode 100644 subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/rule/RuleAction.java create mode 100644 subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/rule/RuleActionExecutor.java create mode 100644 subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/rule/RuleExecutor.java create mode 100644 subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/Advice.java create 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/Seed.java create mode 100644 subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/TranslationUnit.java create mode 100644 subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/EliminatedType.java create mode 100644 subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/ExtendedTypeInfo.java create mode 100644 subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/InferredMayTypeRelationView.java create mode 100644 subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/InferredMustTypeRelationView.java create mode 100644 subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/InferredType.java create mode 100644 subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/PreservedType.java create mode 100644 subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeAnalysisResult.java create mode 100644 subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeAnalyzer.java create mode 100644 subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeHierarchyTranslationUnit.java create mode 100644 subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeInfo.java create mode 100644 subprojects/store-reasoning/src/test/java/tools/refinery/store/reasoning/translator/typehierarchy/InferredTypeTest.java create mode 100644 subprojects/store-reasoning/src/test/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeAnalyzerExampleHierarchyTest.java create mode 100644 subprojects/store-reasoning/src/test/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeAnalyzerTest.java create mode 100644 subprojects/store-reasoning/src/test/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeAnalyzerTester.java (limited to 'subprojects/store-reasoning/src') 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 new file mode 100644 index 00000000..ebe82c8b --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/AnyPartialInterpretation.java @@ -0,0 +1,13 @@ +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 new file mode 100644 index 00000000..0d51598b --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/MergeResult.java @@ -0,0 +1,15 @@ +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 new file mode 100644 index 00000000..99656da8 --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/PartialInterpretation.java @@ -0,0 +1,22 @@ +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(); + + Cursor getAllErrors(); + + 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/Reasoning.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/Reasoning.java new file mode 100644 index 00000000..d7d0a999 --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/Reasoning.java @@ -0,0 +1,24 @@ +package tools.refinery.store.reasoning; + +import tools.refinery.store.reasoning.internal.ReasoningBuilderImpl; +import tools.refinery.store.adapter.ModelAdapterBuilderFactory; +import tools.refinery.store.model.ModelStoreBuilder; +import tools.refinery.store.reasoning.representation.PartialRelation; + +public final class Reasoning extends ModelAdapterBuilderFactory { + public static final Reasoning ADAPTER = new Reasoning(); + + public static final PartialRelation EXISTS = new PartialRelation("exists", 1); + + public static final PartialRelation EQUALS = new PartialRelation("equals", 1); + + private Reasoning() { + super(ReasoningAdapter.class, ReasoningStoreAdapter.class, ReasoningBuilder.class); + } + + @Override + public ReasoningBuilder createBuilder(ModelStoreBuilder storeBuilder) { + return new ReasoningBuilderImpl(storeBuilder); + } +} 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 new file mode 100644 index 00000000..e602242e --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/ReasoningAdapter.java @@ -0,0 +1,22 @@ +package tools.refinery.store.reasoning; + +import tools.refinery.store.adapter.ModelAdapter; +import tools.refinery.store.reasoning.representation.AnyPartialSymbol; +import tools.refinery.store.reasoning.representation.PartialSymbol; +import tools.refinery.store.query.Dnf; +import tools.refinery.store.query.ResultSet; + +public interface ReasoningAdapter extends ModelAdapter { + @Override + ReasoningStoreAdapter getStoreAdapter(); + + default AnyPartialInterpretation getPartialInterpretation(AnyPartialSymbol partialSymbol) { + // Cast to disambiguate overloads. + var typedPartialSymbol = (PartialSymbol) partialSymbol; + return getPartialInterpretation(typedPartialSymbol); + } + + PartialInterpretation getPartialInterpretation(PartialSymbol partialSymbol); + + ResultSet getLiftedResultSet(Dnf query); +} 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 new file mode 100644 index 00000000..588c2711 --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/ReasoningBuilder.java @@ -0,0 +1,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; + +import java.util.Collection; +import java.util.List; + +@SuppressWarnings("UnusedReturnValue") +public interface ReasoningBuilder extends ModelAdapterBuilder { + default ReasoningBuilder liftedQueries(Dnf... liftedQueries) { + return liftedQueries(List.of(liftedQueries)); + } + + default ReasoningBuilder liftedQueries(Collection liftedQueries) { + liftedQueries.forEach(this::liftedQuery); + return this; + } + + ReasoningBuilder liftedQuery(Dnf liftedQuery); + + Dnf lift(Modality modality, Dnf query); + + @Override + ReasoningStoreAdapter createStoreAdapter(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 new file mode 100644 index 00000000..69c0f5eb --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/ReasoningStoreAdapter.java @@ -0,0 +1,17 @@ +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; + +import java.util.Collection; + +public interface ReasoningStoreAdapter extends ModelStoreAdapter { + Collection getPartialSymbols(); + + Collection getLiftedQueries(); + + @Override + ReasoningAdapter createModelAdapter(Model model); +} 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 new file mode 100644 index 00000000..a7a56680 --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/internal/ReasoningAdapterImpl.java @@ -0,0 +1,38 @@ +package tools.refinery.store.reasoning.internal; + +import tools.refinery.store.model.Model; +import tools.refinery.store.reasoning.ReasoningAdapter; +import tools.refinery.store.reasoning.PartialInterpretation; +import tools.refinery.store.reasoning.representation.PartialSymbol; +import tools.refinery.store.query.Dnf; +import tools.refinery.store.query.ResultSet; + +public class ReasoningAdapterImpl implements ReasoningAdapter { + private final Model model; + private final ReasoningStoreAdapterImpl storeAdapter; + + ReasoningAdapterImpl(Model model, ReasoningStoreAdapterImpl storeAdapter) { + this.model = model; + this.storeAdapter = storeAdapter; + } + + @Override + public Model getModel() { + return model; + } + + @Override + public ReasoningStoreAdapterImpl getStoreAdapter() { + return storeAdapter; + } + + @Override + public PartialInterpretation getPartialInterpretation(PartialSymbol partialSymbol) { + return null; + } + + @Override + public ResultSet getLiftedResultSet(Dnf query) { + return null; + } +} 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 new file mode 100644 index 00000000..2860e2b9 --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/internal/ReasoningBuilderImpl.java @@ -0,0 +1,29 @@ +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.reasoning.ReasoningBuilder; +import tools.refinery.store.reasoning.literal.Modality; +import tools.refinery.store.query.Dnf; + +public class ReasoningBuilderImpl extends AbstractModelAdapterBuilder implements ReasoningBuilder { + public ReasoningBuilderImpl(ModelStoreBuilder storeBuilder) { + super(storeBuilder); + } + + @Override + public ReasoningBuilder liftedQuery(Dnf liftedQuery) { + return null; + } + + @Override + public Dnf lift(Modality modality, Dnf query) { + return null; + } + + @Override + public ReasoningStoreAdapterImpl createStoreAdapter(ModelStore store) { + return null; + } +} 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 new file mode 100644 index 00000000..763dad6d --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/internal/ReasoningStoreAdapterImpl.java @@ -0,0 +1,37 @@ +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.reasoning.representation.AnyPartialSymbol; +import tools.refinery.store.query.Dnf; + +import java.util.Collection; + +public class ReasoningStoreAdapterImpl implements ReasoningStoreAdapter { + private final ModelStore store; + + ReasoningStoreAdapterImpl(ModelStore store) { + this.store = store; + } + + @Override + public ModelStore getStore() { + return store; + } + + @Override + public Collection getPartialSymbols() { + return null; + } + + @Override + public Collection getLiftedQueries() { + return null; + } + + @Override + public ReasoningAdapterImpl createModelAdapter(Model model) { + return new ReasoningAdapterImpl(model, this); + } +} 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 new file mode 100644 index 00000000..966e080a --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/lifting/DnfLifter.java @@ -0,0 +1,107 @@ +package tools.refinery.store.reasoning.lifting; + +import org.jetbrains.annotations.Nullable; +import tools.refinery.store.reasoning.literal.ModalDnfCallLiteral; +import tools.refinery.store.reasoning.Reasoning; +import tools.refinery.store.reasoning.literal.ModalRelationLiteral; +import tools.refinery.store.reasoning.literal.PartialRelationLiteral; +import tools.refinery.store.query.Dnf; +import tools.refinery.store.query.DnfBuilder; +import tools.refinery.store.query.DnfClause; +import tools.refinery.store.query.Variable; +import tools.refinery.store.query.literal.CallPolarity; +import tools.refinery.store.query.literal.DnfCallLiteral; +import tools.refinery.store.query.literal.Literal; +import tools.refinery.store.reasoning.literal.Modality; +import tools.refinery.store.util.CycleDetectingMapper; + +import java.util.ArrayList; +import java.util.HashSet; +import java.util.List; + +public class DnfLifter { + private final CycleDetectingMapper mapper = new CycleDetectingMapper<>(ModalDnf::toString, + this::doLift); + + public Dnf lift(Modality modality, Dnf query) { + return mapper.map(new ModalDnf(modality, query)); + } + + private Dnf doLift(ModalDnf modalDnf) { + var modality = modalDnf.modality(); + var dnf = modalDnf.dnf(); + var builder = Dnf.builder(); + builder.parameters(dnf.getParameters()); + boolean changed = false; + for (var clause : dnf.getClauses()) { + if (liftClause(modality, clause, builder)) { + changed = true; + } + } + if (changed) { + return builder.build(); + } + return dnf; + } + + private boolean liftClause(Modality modality, DnfClause clause, DnfBuilder builder) { + boolean changed = false; + var quantifiedVariables = new HashSet<>(clause.quantifiedVariables()); + var literals = clause.literals(); + var liftedLiterals = new ArrayList(literals.size()); + for (var literal : literals) { + Literal liftedLiteral = liftLiteral(modality, literal); + if (liftedLiteral == null) { + liftedLiteral = literal; + } else { + changed = true; + } + liftedLiterals.add(liftedLiteral); + var variable = isExistsLiteralForVariable(modality, liftedLiteral); + if (variable != null) { + // If we already quantify over the existence of the variable with the expected modality, + // we don't need to insert quantification manually. + quantifiedVariables.remove(variable); + } + } + for (var quantifiedVariable : quantifiedVariables) { + // Quantify over variables that are not already quantified with the expected modality. + liftedLiterals.add(Reasoning.EXISTS.call(CallPolarity.POSITIVE, modality, + List.of(quantifiedVariable))); + } + builder.clause(liftedLiterals); + return changed || !quantifiedVariables.isEmpty(); + } + + @Nullable + private Variable isExistsLiteralForVariable(Modality modality, Literal literal) { + if (literal instanceof ModalRelationLiteral modalRelationLiteral && + modalRelationLiteral.getPolarity() == CallPolarity.POSITIVE && + modalRelationLiteral.getModality() == modality && + modalRelationLiteral.getTarget().equals(Reasoning.EXISTS)) { + return modalRelationLiteral.getArguments().get(0); + } + return null; + } + + @Nullable + private Literal liftLiteral(Modality modality, Literal literal) { + if (literal instanceof PartialRelationLiteral partialRelationLiteral) { + return new ModalRelationLiteral(modality, partialRelationLiteral); + } else if (literal instanceof DnfCallLiteral dnfCallLiteral) { + var polarity = dnfCallLiteral.getPolarity(); + var target = dnfCallLiteral.getTarget(); + var liftedTarget = lift(modality.commute(polarity), target); + if (target.equals(liftedTarget)) { + return null; + } + return new DnfCallLiteral(polarity, liftedTarget, dnfCallLiteral.getArguments()); + } else if (literal instanceof ModalDnfCallLiteral modalDnfCallLiteral) { + var liftedTarget = lift(modalDnfCallLiteral.getModality(), modalDnfCallLiteral.getTarget()); + return new DnfCallLiteral(modalDnfCallLiteral.getPolarity(), liftedTarget, + modalDnfCallLiteral.getArguments()); + } else { + return null; + } + } +} diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/lifting/ModalDnf.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/lifting/ModalDnf.java new file mode 100644 index 00000000..7aa98bf2 --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/lifting/ModalDnf.java @@ -0,0 +1,11 @@ +package tools.refinery.store.reasoning.lifting; + +import tools.refinery.store.query.Dnf; +import tools.refinery.store.reasoning.literal.Modality; + +public record ModalDnf(Modality modality, Dnf dnf) { + @Override + public String toString() { + return "%s %s".formatted(modality, dnf.name()); + } +} diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/literal/ModalDnfCallLiteral.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/literal/ModalDnfCallLiteral.java new file mode 100644 index 00000000..1090f1ae --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/literal/ModalDnfCallLiteral.java @@ -0,0 +1,48 @@ +package tools.refinery.store.reasoning.literal; + +import tools.refinery.store.query.Dnf; +import tools.refinery.store.query.Variable; +import tools.refinery.store.query.equality.LiteralEqualityHelper; +import tools.refinery.store.query.literal.CallPolarity; +import tools.refinery.store.query.literal.DnfCallLiteral; +import tools.refinery.store.query.literal.LiteralReduction; +import tools.refinery.store.query.literal.PolarLiteral; +import tools.refinery.store.query.substitution.Substitution; + +import java.util.List; + +public class ModalDnfCallLiteral extends ModalLiteral implements PolarLiteral { + public ModalDnfCallLiteral(CallPolarity polarity, Modality modality, Dnf target, List arguments) { + super(polarity, modality, target, arguments); + } + + public ModalDnfCallLiteral(Modality modality, DnfCallLiteral baseLiteral) { + super(modality.commute(baseLiteral.getPolarity()), baseLiteral); + } + + @Override + public Class getTargetType() { + return Dnf.class; + } + + @Override + protected boolean targetEquals(LiteralEqualityHelper helper, Dnf otherTarget) { + return helper.dnfEqual(getTarget(), otherTarget); + } + + @Override + public ModalDnfCallLiteral substitute(Substitution substitution) { + return new ModalDnfCallLiteral(getPolarity(), getModality(), getTarget(), substituteArguments(substitution)); + } + + @Override + public ModalDnfCallLiteral negate() { + return new ModalDnfCallLiteral(getPolarity().negate(), getModality(), getTarget(), getArguments()); + } + + @Override + public LiteralReduction getReduction() { + var dnfReduction = getTarget().getReduction(); + return getPolarity().isPositive() ? dnfReduction : dnfReduction.negate(); + } +} diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/literal/ModalLiteral.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/literal/ModalLiteral.java new file mode 100644 index 00000000..5992f172 --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/literal/ModalLiteral.java @@ -0,0 +1,63 @@ +package tools.refinery.store.reasoning.literal; + +import tools.refinery.store.query.RelationLike; +import tools.refinery.store.query.Variable; +import tools.refinery.store.query.equality.LiteralEqualityHelper; +import tools.refinery.store.query.literal.CallLiteral; +import tools.refinery.store.query.literal.CallPolarity; +import tools.refinery.store.query.literal.Literal; + +import java.util.List; +import java.util.Objects; + +public abstract class ModalLiteral extends CallLiteral { + private final Modality modality; + + protected ModalLiteral(CallPolarity polarity, Modality modality, T target, List arguments) { + super(polarity, target, arguments); + this.modality = modality; + } + + protected ModalLiteral(Modality modality, CallLiteral baseLiteral) { + this(baseLiteral.getPolarity(), commute(modality, baseLiteral.getPolarity()), baseLiteral.getTarget(), + baseLiteral.getArguments()); + } + + public Modality getModality() { + return modality; + } + + @Override + public boolean equalsWithSubstitution(LiteralEqualityHelper helper, Literal other) { + if (!super.equalsWithSubstitution(helper, other)) { + return false; + } + // If {@link CallLiteral#equalsWithSubstitution(LiteralEqualityHelper, Literal)} has returned {@code true}, + // we must have the same dynamic type as {@code other}. + var otherModalLiteral = (ModalLiteral) other; + return modality == otherModalLiteral.modality; + } + + @Override + protected String targetToString() { + return "%s %s".formatted(modality, super.targetToString()); + } + + @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; + ModalLiteral that = (ModalLiteral) o; + return modality == that.modality; + } + + @Override + public int hashCode() { + return Objects.hash(super.hashCode(), modality); + } + + private static Modality commute(Modality modality, CallPolarity polarity) { + return polarity.isPositive() ? modality : modality.negate(); + } +} diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/literal/ModalRelationLiteral.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/literal/ModalRelationLiteral.java new file mode 100644 index 00000000..9c72bd37 --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/literal/ModalRelationLiteral.java @@ -0,0 +1,37 @@ +package tools.refinery.store.reasoning.literal; + +import tools.refinery.store.reasoning.representation.PartialRelation; +import tools.refinery.store.query.Variable; +import tools.refinery.store.query.literal.CallPolarity; +import tools.refinery.store.query.literal.PolarLiteral; +import tools.refinery.store.query.substitution.Substitution; + +import java.util.List; + +public final class ModalRelationLiteral extends ModalLiteral + implements PolarLiteral { + public ModalRelationLiteral(CallPolarity polarity, Modality modality, PartialRelation target, + List arguments) { + super(polarity, modality, target, arguments); + } + + + public ModalRelationLiteral(Modality modality, PartialRelationLiteral baseLiteral) { + super(modality, baseLiteral); + } + + @Override + public Class getTargetType() { + return PartialRelation.class; + } + + @Override + public ModalRelationLiteral substitute(Substitution substitution) { + return new ModalRelationLiteral(getPolarity(), getModality(), getTarget(), substituteArguments(substitution)); + } + + @Override + public ModalRelationLiteral negate() { + return new ModalRelationLiteral(getPolarity().negate(), getModality(), getTarget(), getArguments()); + } +} diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/literal/Modality.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/literal/Modality.java new file mode 100644 index 00000000..f0cb59de --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/literal/Modality.java @@ -0,0 +1,31 @@ +package tools.refinery.store.reasoning.literal; + +import tools.refinery.store.query.literal.CallPolarity; + +import java.util.Locale; + +public enum Modality { + MUST, + MAY, + CURRENT; + + public Modality negate() { + return switch(this) { + case MUST -> MAY; + case MAY -> MUST; + case CURRENT -> CURRENT; + }; + } + + public Modality commute(CallPolarity polarity) { + if (polarity.isPositive()) { + return this; + } + return this.negate(); + } + + @Override + public String toString() { + return name().toLowerCase(Locale.ROOT); + } +} 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 new file mode 100644 index 00000000..10e4c7f7 --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/literal/PartialLiterals.java @@ -0,0 +1,33 @@ +package tools.refinery.store.reasoning.literal; + +import tools.refinery.store.query.literal.DnfCallLiteral; + +public final class PartialLiterals { + private PartialLiterals() { + throw new IllegalStateException("This is a static utility class and should not be instantiated directly"); + } + + public ModalRelationLiteral may(PartialRelationLiteral literal) { + return new ModalRelationLiteral(Modality.MAY, literal); + } + + public ModalRelationLiteral must(PartialRelationLiteral literal) { + return new ModalRelationLiteral(Modality.MUST, literal); + } + + public ModalRelationLiteral current(PartialRelationLiteral literal) { + return new ModalRelationLiteral(Modality.CURRENT, literal); + } + + public ModalDnfCallLiteral may(DnfCallLiteral literal) { + return new ModalDnfCallLiteral(Modality.MAY, literal); + } + + public ModalDnfCallLiteral must(DnfCallLiteral literal) { + return new ModalDnfCallLiteral(Modality.MUST, literal); + } + + public ModalDnfCallLiteral current(DnfCallLiteral literal) { + return new ModalDnfCallLiteral(Modality.CURRENT, literal); + } +} diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/literal/PartialRelationLiteral.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/literal/PartialRelationLiteral.java new file mode 100644 index 00000000..aff84538 --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/literal/PartialRelationLiteral.java @@ -0,0 +1,32 @@ +package tools.refinery.store.reasoning.literal; + +import tools.refinery.store.reasoning.representation.PartialRelation; +import tools.refinery.store.query.Variable; +import tools.refinery.store.query.literal.CallLiteral; +import tools.refinery.store.query.literal.CallPolarity; +import tools.refinery.store.query.literal.PolarLiteral; +import tools.refinery.store.query.substitution.Substitution; + +import java.util.List; + +public final class PartialRelationLiteral extends CallLiteral + implements PolarLiteral { + public PartialRelationLiteral(CallPolarity polarity, PartialRelation target, List substitution) { + super(polarity, target, substitution); + } + + @Override + public Class getTargetType() { + return PartialRelation.class; + } + + @Override + public PartialRelationLiteral substitute(Substitution substitution) { + return new PartialRelationLiteral(getPolarity(), getTarget(), substituteArguments(substitution)); + } + + @Override + public PartialRelationLiteral negate() { + return new PartialRelationLiteral(getPolarity().negate(), getTarget(), getArguments()); + } +} diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/representation/AnyPartialFunction.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/representation/AnyPartialFunction.java new file mode 100644 index 00000000..e74cd58b --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/representation/AnyPartialFunction.java @@ -0,0 +1,4 @@ +package tools.refinery.store.reasoning.representation; + +public sealed interface AnyPartialFunction extends AnyPartialSymbol permits PartialFunction { +} diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/representation/AnyPartialSymbol.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/representation/AnyPartialSymbol.java new file mode 100644 index 00000000..6ff5031b --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/representation/AnyPartialSymbol.java @@ -0,0 +1,11 @@ +package tools.refinery.store.reasoning.representation; + +import tools.refinery.store.representation.AnyAbstractDomain; + +public sealed interface AnyPartialSymbol permits AnyPartialFunction, PartialSymbol { + String name(); + + int arity(); + + AnyAbstractDomain abstractDomain(); +} 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 new file mode 100644 index 00000000..59eeeefe --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/representation/PartialFunction.java @@ -0,0 +1,32 @@ +package tools.refinery.store.reasoning.representation; + +import tools.refinery.store.representation.AbstractDomain; + +public record PartialFunction(String name, int arity, AbstractDomain abstractDomain) + implements AnyPartialFunction, PartialSymbol { + @Override + public A defaultValue() { + return null; + } + + @Override + public C defaultConcreteValue() { + return null; + } + + @Override + public boolean equals(Object o) { + return this == o; + } + + @Override + public int hashCode() { + // Compare by identity to make hash table lookups more efficient. + return System.identityHashCode(this); + } + + @Override + public String toString() { + return "%s/%d".formatted(name, arity); + } +} 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 new file mode 100644 index 00000000..f884f8d6 --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/representation/PartialRelation.java @@ -0,0 +1,66 @@ +package tools.refinery.store.reasoning.representation; + +import tools.refinery.store.reasoning.literal.Modality; +import tools.refinery.store.reasoning.literal.PartialRelationLiteral; +import tools.refinery.store.reasoning.literal.ModalRelationLiteral; +import tools.refinery.store.query.RelationLike; +import tools.refinery.store.query.Variable; +import tools.refinery.store.query.literal.CallPolarity; +import tools.refinery.store.representation.AbstractDomain; +import tools.refinery.store.representation.TruthValue; +import tools.refinery.store.representation.TruthValueDomain; + +import java.util.List; + +public record PartialRelation(String name, int arity) implements PartialSymbol, RelationLike { + @Override + public AbstractDomain abstractDomain() { + return TruthValueDomain.INSTANCE; + } + + @Override + public TruthValue defaultValue() { + return TruthValue.FALSE; + } + + @Override + public Boolean defaultConcreteValue() { + return false; + } + + public ModalRelationLiteral call(CallPolarity polarity, Modality modality, List arguments) { + return new ModalRelationLiteral(polarity, modality, this, arguments); + } + + public PartialRelationLiteral call(CallPolarity polarity, List arguments) { + return new PartialRelationLiteral(polarity, this, arguments); + } + + public PartialRelationLiteral call(CallPolarity polarity, Variable... arguments) { + return call(polarity, List.of(arguments)); + } + + public PartialRelationLiteral call(Variable... arguments) { + return call(CallPolarity.POSITIVE, arguments); + } + + public PartialRelationLiteral callTransitive(Variable left, Variable right) { + return call(CallPolarity.TRANSITIVE, List.of(left, right)); + } + + @Override + public boolean equals(Object o) { + return this == o; + } + + @Override + public int hashCode() { + // Compare by identity to make hash table lookups more efficient. + return System.identityHashCode(this); + } + + @Override + public String toString() { + return "%s/%d".formatted(name, 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 new file mode 100644 index 00000000..1af11f2e --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/representation/PartialSymbol.java @@ -0,0 +1,12 @@ +package tools.refinery.store.reasoning.representation; + +import tools.refinery.store.representation.AbstractDomain; + +public sealed interface PartialSymbol extends AnyPartialSymbol permits PartialFunction, PartialRelation { + @Override + AbstractDomain abstractDomain(); + + A defaultValue(); + + C defaultConcreteValue(); +} diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/rule/RelationRefinementAction.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/rule/RelationRefinementAction.java new file mode 100644 index 00000000..c7681b53 --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/rule/RelationRefinementAction.java @@ -0,0 +1,36 @@ +package tools.refinery.store.reasoning.rule; + +import tools.refinery.store.reasoning.Reasoning; +import tools.refinery.store.reasoning.representation.PartialRelation; +import tools.refinery.store.model.Model; +import tools.refinery.store.query.Variable; +import tools.refinery.store.representation.TruthValue; +import tools.refinery.store.tuple.Tuple; + +import java.util.List; + +public record RelationRefinementAction(PartialRelation target, List arguments, TruthValue value) + implements RuleAction { + public RelationRefinementAction { + if (arguments.size() != target.arity()) { + throw new IllegalArgumentException("%s needs %d parameters, but got %s".formatted(target.name(), + target.arity(), arguments.size())); + } + if (value == TruthValue.UNKNOWN) { + throw new IllegalArgumentException("Refining with UNKNOWN has no effect"); + } + } + + @Override + public RuleActionExecutor createExecutor(int[] argumentIndices, Model model) { + var targetInterpretation = model.getAdapter(Reasoning.ADAPTER).getPartialInterpretation(target); + return activationTuple -> { + int arity = argumentIndices.length; + var arguments = new int[arity]; + for (int i = 0; i < arity; i++) { + arguments[i] = activationTuple.get(argumentIndices[i]); + } + return targetInterpretation.merge(Tuple.of(arguments), value); + }; + } +} diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/rule/Rule.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/rule/Rule.java new file mode 100644 index 00000000..8a812518 --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/rule/Rule.java @@ -0,0 +1,38 @@ +package tools.refinery.store.reasoning.rule; + +import tools.refinery.store.model.Model; +import tools.refinery.store.query.Dnf; + +import java.util.ArrayList; +import java.util.HashSet; +import java.util.List; + +public record Rule(Dnf precondition, List actions) { + public Rule { + var parameterSet = new HashSet<>(precondition.getParameters()); + for (var action : actions) { + for (var argument : action.arguments()) { + if (!parameterSet.contains(argument)) { + throw new IllegalArgumentException( + "Argument %s of action %s does not appear in the parameter list %s of %s" + .formatted(argument, action, precondition.getParameters(), precondition.name())); + } + } + } + } + + public RuleExecutor createExecutor(Model model) { + var parameters = precondition.getParameters(); + var actionExecutors = new ArrayList(actions.size()); + for (var action : actions) { + var arguments = action.arguments(); + int arity = arguments.size(); + var argumentIndices = new int[arity]; + for (int i = 0; i < arity; i++) { + argumentIndices[i] = parameters.indexOf(arguments.get(i)); + } + actionExecutors.add(action.createExecutor(argumentIndices, model)); + } + return new RuleExecutor(this, model, actionExecutors); + } +} diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/rule/RuleAction.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/rule/RuleAction.java new file mode 100644 index 00000000..bf980759 --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/rule/RuleAction.java @@ -0,0 +1,12 @@ +package tools.refinery.store.reasoning.rule; + +import tools.refinery.store.model.Model; +import tools.refinery.store.query.Variable; + +import java.util.List; + +public interface RuleAction { + List arguments(); + + RuleActionExecutor createExecutor(int[] argumentIndices, Model model); +} diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/rule/RuleActionExecutor.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/rule/RuleActionExecutor.java new file mode 100644 index 00000000..80bfa6f8 --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/rule/RuleActionExecutor.java @@ -0,0 +1,9 @@ +package tools.refinery.store.reasoning.rule; + +import tools.refinery.store.reasoning.MergeResult; +import tools.refinery.store.tuple.TupleLike; + +@FunctionalInterface +public interface RuleActionExecutor { + MergeResult execute(TupleLike activationTuple); +} diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/rule/RuleExecutor.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/rule/RuleExecutor.java new file mode 100644 index 00000000..1e5322b4 --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/rule/RuleExecutor.java @@ -0,0 +1,34 @@ +package tools.refinery.store.reasoning.rule; + +import tools.refinery.store.reasoning.MergeResult; +import tools.refinery.store.model.Model; +import tools.refinery.store.tuple.TupleLike; + +import java.util.List; + +public final class RuleExecutor { + private final Rule rule; + private final Model model; + private final List actionExecutors; + + RuleExecutor(Rule rule, Model model, List actionExecutors) { + this.rule = rule; + this.model = model; + this.actionExecutors = actionExecutors; + } + + public Rule getRule() { + return rule; + } + + public Model getModel() { + return model; + } + public MergeResult execute(TupleLike activationTuple) { + MergeResult mergeResult = MergeResult.UNCHANGED; + for (var actionExecutor : actionExecutors) { + mergeResult = mergeResult.andAlso(actionExecutor.execute(activationTuple)); + } + return mergeResult; + } +} 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 new file mode 100644 index 00000000..7909a7e1 --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/Advice.java @@ -0,0 +1,159 @@ +package tools.refinery.store.reasoning.translator; + +import tools.refinery.store.reasoning.representation.AnyPartialSymbol; +import tools.refinery.store.reasoning.representation.PartialRelation; +import tools.refinery.store.query.Variable; +import tools.refinery.store.query.literal.Literal; +import tools.refinery.store.query.substitution.Substitutions; + +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(); + int arity = parameters.size(); + var variableMap = new HashMap(arity); + for (int i = 0; i < arity; i++) { + variableMap.put(parameters.get(i), substituteParameters.get(i)); + } + // 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 = Substitutions.renewing(variableMap); + 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 new file mode 100644 index 00000000..f3bd9c5e --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/AdviceSlot.java @@ -0,0 +1,25 @@ +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/Seed.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/Seed.java new file mode 100644 index 00000000..779eadbe --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/Seed.java @@ -0,0 +1,12 @@ +package tools.refinery.store.reasoning.translator; + +import tools.refinery.store.map.Cursor; +import tools.refinery.store.tuple.Tuple; + +public interface Seed { + int arity(); + + T get(Tuple key); + + Cursor getCursor(T defaultValue, int nodeCount); +} 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 new file mode 100644 index 00000000..e45d20c8 --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/TranslationUnit.java @@ -0,0 +1,48 @@ +package tools.refinery.store.reasoning.translator; + +import tools.refinery.store.reasoning.ReasoningBuilder; +import tools.refinery.store.model.Model; +import tools.refinery.store.model.ModelStoreBuilder; +import tools.refinery.store.reasoning.AnyPartialInterpretation; +import tools.refinery.store.reasoning.literal.Modality; +import tools.refinery.store.reasoning.representation.AnyPartialSymbol; +import tools.refinery.store.reasoning.representation.PartialRelation; +import tools.refinery.store.query.Variable; +import tools.refinery.store.query.literal.CallPolarity; +import tools.refinery.store.query.literal.Literal; + +import java.util.Collection; +import java.util.List; +import java.util.Map; + +public abstract class TranslationUnit { + private ReasoningBuilder reasoningBuilder; + + protected ReasoningBuilder getPartialInterpretationBuilder() { + return reasoningBuilder; + } + + public void setPartialInterpretationBuilder(ReasoningBuilder reasoningBuilder) { + this.reasoningBuilder = reasoningBuilder; + } + + protected ModelStoreBuilder getModelStoreBuilder() { + return reasoningBuilder.getStoreBuilder(); + } + + public abstract Collection getTranslatedPartialSymbols(); + + public Collection computeAdvices() { + // No advices to give by default. + return List.of(); + } + + public abstract void configure(Collection advices); + + public abstract List call(CallPolarity polarity, Modality modality, PartialRelation target, + List arguments); + + public abstract Map createPartialInterpretations(Model model); + + public abstract void initializeModel(Model model, int nodeCount); +} diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/EliminatedType.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/EliminatedType.java new file mode 100644 index 00000000..1b8d7cc9 --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/EliminatedType.java @@ -0,0 +1,6 @@ +package tools.refinery.store.reasoning.translator.typehierarchy; + +import tools.refinery.store.reasoning.representation.PartialRelation; + +record EliminatedType(PartialRelation replacement) implements TypeAnalysisResult { +} diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/ExtendedTypeInfo.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/ExtendedTypeInfo.java new file mode 100644 index 00000000..43b8e1dd --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/ExtendedTypeInfo.java @@ -0,0 +1,101 @@ +package tools.refinery.store.reasoning.translator.typehierarchy; + +import org.jetbrains.annotations.NotNull; +import tools.refinery.store.reasoning.representation.PartialRelation; + +import java.util.HashSet; +import java.util.LinkedHashSet; +import java.util.Objects; +import java.util.Set; + +final class ExtendedTypeInfo implements Comparable { + private final int index; + private final PartialRelation type; + private final TypeInfo typeInfo; + private final Set allSubtypes = new LinkedHashSet<>(); + private final Set allSupertypes; + private final Set concreteSubtypesAndSelf = new LinkedHashSet<>(); + private Set directSubtypes; + private final Set unsortedDirectSupertypes = new HashSet<>(); + + public ExtendedTypeInfo(int index, PartialRelation type, TypeInfo typeInfo) { + this.index = index; + this.type = type; + this.typeInfo = typeInfo; + this.allSupertypes = new LinkedHashSet<>(typeInfo.supertypes()); + } + + public PartialRelation getType() { + return type; + } + + public TypeInfo getTypeInfo() { + return typeInfo; + } + + public boolean isAbstractType() { + return getTypeInfo().abstractType(); + } + + public Set getAllSubtypes() { + return allSubtypes; + } + + public Set getAllSupertypes() { + return allSupertypes; + } + + public Set getAllSupertypesAndSelf() { + var allSubtypesAndSelf = new HashSet(allSupertypes.size() + 1); + addMust(allSubtypesAndSelf); + return allSubtypesAndSelf; + } + + public Set getConcreteSubtypesAndSelf() { + return concreteSubtypesAndSelf; + } + + public Set getDirectSubtypes() { + return directSubtypes; + } + + public Set getUnsortedDirectSupertypes() { + return unsortedDirectSupertypes; + } + + public void setDirectSubtypes(Set directSubtypes) { + this.directSubtypes = directSubtypes; + } + + public boolean allowsAllConcreteTypes(Set concreteTypes) { + for (var concreteType : concreteTypes) { + if (!concreteSubtypesAndSelf.contains(concreteType)) { + return false; + } + } + return true; + } + + public void addMust(Set mustTypes) { + mustTypes.add(type); + mustTypes.addAll(allSupertypes); + } + + @Override + public int compareTo(@NotNull ExtendedTypeInfo extendedTypeInfo) { + return Integer.compare(index, extendedTypeInfo.index); + } + + @Override + public boolean equals(Object o) { + if (this == o) return true; + if (o == null || getClass() != o.getClass()) return false; + ExtendedTypeInfo that = (ExtendedTypeInfo) o; + return index == that.index; + } + + @Override + public int hashCode() { + return Objects.hash(index); + } +} diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/InferredMayTypeRelationView.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/InferredMayTypeRelationView.java new file mode 100644 index 00000000..12c37c86 --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/InferredMayTypeRelationView.java @@ -0,0 +1,19 @@ +package tools.refinery.store.reasoning.translator.typehierarchy; + +import tools.refinery.store.reasoning.representation.PartialRelation; +import tools.refinery.store.query.view.TuplePreservingRelationView; +import tools.refinery.store.tuple.Tuple; + +class InferredMayTypeRelationView extends TuplePreservingRelationView { + private final PartialRelation type; + + InferredMayTypeRelationView(PartialRelation type) { + super(TypeHierarchyTranslationUnit.INFERRED_TYPE_SYMBOL, "%s#may".formatted(type)); + this.type = type; + } + + @Override + public boolean filter(Tuple key, InferredType value) { + return value.mayConcreteTypes().contains(type); + } +} diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/InferredMustTypeRelationView.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/InferredMustTypeRelationView.java new file mode 100644 index 00000000..975f627e --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/InferredMustTypeRelationView.java @@ -0,0 +1,19 @@ +package tools.refinery.store.reasoning.translator.typehierarchy; + +import tools.refinery.store.reasoning.representation.PartialRelation; +import tools.refinery.store.query.view.TuplePreservingRelationView; +import tools.refinery.store.tuple.Tuple; + +class InferredMustTypeRelationView extends TuplePreservingRelationView { + private final PartialRelation type; + + InferredMustTypeRelationView(PartialRelation type) { + super(TypeHierarchyTranslationUnit.INFERRED_TYPE_SYMBOL, "%s#must".formatted(type)); + this.type = type; + } + + @Override + public boolean filter(Tuple key, InferredType value) { + return value.mustTypes().contains(type); + } +} diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/InferredType.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/InferredType.java new file mode 100644 index 00000000..a366e262 --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/InferredType.java @@ -0,0 +1,30 @@ +package tools.refinery.store.reasoning.translator.typehierarchy; + +import tools.refinery.store.reasoning.representation.PartialRelation; + +import java.util.Collections; +import java.util.Set; + +record InferredType(Set mustTypes, Set mayConcreteTypes, + PartialRelation currentType) { + public static final InferredType UNTYPED = new InferredType(Set.of(), Set.of(), null); + + public InferredType(Set mustTypes, Set mayConcreteTypes, + PartialRelation currentType) { + this.mustTypes = Collections.unmodifiableSet(mustTypes); + this.mayConcreteTypes = Collections.unmodifiableSet(mayConcreteTypes); + this.currentType = currentType; + } + + public boolean isConsistent() { + return currentType != null || mustTypes.isEmpty(); + } + + public boolean isMust(PartialRelation partialRelation) { + return mustTypes.contains(partialRelation); + } + + public boolean isMayConcrete(PartialRelation partialRelation) { + return mayConcreteTypes.contains(partialRelation); + } +} diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/PreservedType.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/PreservedType.java new file mode 100644 index 00000000..63dba964 --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/PreservedType.java @@ -0,0 +1,136 @@ +package tools.refinery.store.reasoning.translator.typehierarchy; + +import tools.refinery.store.reasoning.representation.PartialRelation; +import tools.refinery.store.representation.TruthValue; + +import java.util.*; + +final class PreservedType implements TypeAnalysisResult { + private final ExtendedTypeInfo extendedTypeInfo; + private final List directSubtypes; + private final List allExternalTypeInfoList; + private final InferredType inferredType; + + public PreservedType(ExtendedTypeInfo extendedTypeInfo, List allExternalTypeInfoList) { + this.extendedTypeInfo = extendedTypeInfo; + directSubtypes = List.copyOf(extendedTypeInfo.getDirectSubtypes()); + this.allExternalTypeInfoList = allExternalTypeInfoList; + inferredType = propagateMust(extendedTypeInfo.getAllSupertypesAndSelf(), + extendedTypeInfo.getConcreteSubtypesAndSelf()); + } + + public PartialRelation type() { + return extendedTypeInfo.getType(); + } + + public List getDirectSubtypes() { + return directSubtypes; + } + + public boolean isAbstractType() { + return extendedTypeInfo.isAbstractType(); + } + + public boolean isVacuous() { + return isAbstractType() && directSubtypes.isEmpty(); + } + + public InferredType asInferredType() { + return inferredType; + } + + public InferredType merge(InferredType inferredType, TruthValue value) { + return switch (value) { + case UNKNOWN -> inferredType; + case TRUE -> addMust(inferredType); + case FALSE -> removeMay(inferredType); + case ERROR -> addError(inferredType); + }; + } + + private InferredType addMust(InferredType inferredType) { + var originalMustTypes = inferredType.mustTypes(); + if (originalMustTypes.contains(type())) { + return inferredType; + } + var mustTypes = new HashSet<>(originalMustTypes); + extendedTypeInfo.addMust(mustTypes); + var originalMayConcreteTypes = inferredType.mayConcreteTypes(); + var mayConcreteTypes = new LinkedHashSet<>(originalMayConcreteTypes); + Set mayConcreteTypesResult; + if (mayConcreteTypes.retainAll(extendedTypeInfo.getConcreteSubtypesAndSelf())) { + mayConcreteTypesResult = mayConcreteTypes; + } else { + mayConcreteTypesResult = originalMayConcreteTypes; + } + return propagateMust(mustTypes, mayConcreteTypesResult); + } + + private InferredType removeMay(InferredType inferredType) { + var originalMayConcreteTypes = inferredType.mayConcreteTypes(); + var mayConcreteTypes = new LinkedHashSet<>(originalMayConcreteTypes); + if (!mayConcreteTypes.removeAll(extendedTypeInfo.getConcreteSubtypesAndSelf())) { + return inferredType; + } + return propagateMust(inferredType.mustTypes(), mayConcreteTypes); + } + + private InferredType addError(InferredType inferredType) { + var originalMustTypes = inferredType.mustTypes(); + if (originalMustTypes.contains(type())) { + if (inferredType.mayConcreteTypes().isEmpty()) { + return inferredType; + } + return new InferredType(originalMustTypes, Set.of(), null); + } + var mustTypes = new HashSet<>(originalMustTypes); + extendedTypeInfo.addMust(mustTypes); + return new InferredType(mustTypes, Set.of(), null); + } + + private InferredType propagateMust(Set originalMustTypes, + Set mayConcreteTypes) { + // It is possible that there is not type at all, do not force one by propagation. + var maybeUntyped = originalMustTypes.isEmpty(); + // Para-consistent case, do not propagate must types to avoid logical explosion. + var paraConsistentOrSurelyUntyped = mayConcreteTypes.isEmpty(); + if (maybeUntyped || paraConsistentOrSurelyUntyped) { + return new InferredType(originalMustTypes, mayConcreteTypes, null); + } + var currentType = computeCurrentType(mayConcreteTypes); + var mustTypes = new HashSet<>(originalMustTypes); + boolean changed = false; + for (var newMustExtendedTypeInfo : allExternalTypeInfoList) { + var newMustType = newMustExtendedTypeInfo.getType(); + if (mustTypes.contains(newMustType)) { + continue; + } + if (newMustExtendedTypeInfo.allowsAllConcreteTypes(mayConcreteTypes)) { + newMustExtendedTypeInfo.addMust(mustTypes); + changed = true; + } + } + if (!changed) { + return new InferredType(originalMustTypes, mayConcreteTypes, currentType); + } + return new InferredType(mustTypes, mayConcreteTypes, currentType); + } + + /** + * Returns a concrete type that is allowed by a (consistent, i.e., nonempty) set of may concrete types. + * + * @param mayConcreteTypes The set of allowed concrete types. Must not be empty. + * @return The first concrete type that is allowed by {@code matConcreteTypes}. + */ + private PartialRelation computeCurrentType(Set mayConcreteTypes) { + for (var concreteExtendedTypeInfo : allExternalTypeInfoList) { + var concreteType = concreteExtendedTypeInfo.getType(); + if (!concreteExtendedTypeInfo.isAbstractType() && mayConcreteTypes.contains(concreteType)) { + return concreteType; + } + } + // We have already filtered out the para-consistent case in {@link #propagateMust(Set, + // Set}. + throw new AssertionError("No concrete type in %s".formatted(mayConcreteTypes)); + } +} diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeAnalysisResult.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeAnalysisResult.java new file mode 100644 index 00000000..4f915108 --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeAnalysisResult.java @@ -0,0 +1,4 @@ +package tools.refinery.store.reasoning.translator.typehierarchy; + +sealed interface TypeAnalysisResult permits EliminatedType, PreservedType { +} diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeAnalyzer.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeAnalyzer.java new file mode 100644 index 00000000..62f8e750 --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeAnalyzer.java @@ -0,0 +1,202 @@ +package tools.refinery.store.reasoning.translator.typehierarchy; + +import tools.refinery.store.reasoning.representation.PartialRelation; + +import java.util.*; + +class TypeAnalyzer { + private final Map extendedTypeInfoMap; + private final Map replacements = new LinkedHashMap<>(); + private final InferredType unknownType; + private final Map analysisResults; + + public TypeAnalyzer(Map typeInfoMap) { + int size = typeInfoMap.size(); + extendedTypeInfoMap = new LinkedHashMap<>(size); + var concreteTypes = new LinkedHashSet(); + int index = 0; + for (var entry : typeInfoMap.entrySet()) { + var type = entry.getKey(); + var typeInfo = entry.getValue(); + extendedTypeInfoMap.put(type, new ExtendedTypeInfo(index, type, typeInfo)); + if (!typeInfo.abstractType()) { + concreteTypes.add(type); + } + index++; + } + unknownType = new InferredType(Set.of(), concreteTypes, null); + computeAllSupertypes(); + computeAllAndConcreteSubtypes(); + computeDirectSubtypes(); + eliminateTrivialSupertypes(); + analysisResults = computeAnalysisResults(); + } + + public InferredType getUnknownType() { + return unknownType; + } + + public Map getAnalysisResults() { + return analysisResults; + } + + private void computeAllSupertypes() { + boolean changed; + do { + changed = false; + for (var extendedTypeInfo : extendedTypeInfoMap.values()) { + var found = new HashSet(); + var allSupertypes = extendedTypeInfo.getAllSupertypes(); + for (var supertype : allSupertypes) { + found.addAll(extendedTypeInfoMap.get(supertype).getAllSupertypes()); + } + if (allSupertypes.addAll(found)) { + changed = true; + } + } + } while (changed); + } + + private void computeAllAndConcreteSubtypes() { + for (var extendedTypeInfo : extendedTypeInfoMap.values()) { + var type = extendedTypeInfo.getType(); + if (!extendedTypeInfo.isAbstractType()) { + extendedTypeInfo.getConcreteSubtypesAndSelf().add(type); + } + for (var supertype : extendedTypeInfo.getAllSupertypes()) { + if (type.equals(supertype)) { + throw new IllegalArgumentException("%s cannot be a supertype of itself".formatted(type)); + } + var supertypeInfo = extendedTypeInfoMap.get(supertype); + supertypeInfo.getAllSubtypes().add(type); + if (!extendedTypeInfo.isAbstractType()) { + supertypeInfo.getConcreteSubtypesAndSelf().add(type); + } + } + } + } + + private void computeDirectSubtypes() { + for (var extendedTypeInfo : extendedTypeInfoMap.values()) { + var allSubtypes = extendedTypeInfo.getAllSubtypes(); + var directSubtypes = new LinkedHashSet<>(allSubtypes); + var indirectSubtypes = new LinkedHashSet(allSubtypes.size()); + for (var subtype : allSubtypes) { + indirectSubtypes.addAll(extendedTypeInfoMap.get(subtype).getAllSubtypes()); + } + directSubtypes.removeAll(indirectSubtypes); + extendedTypeInfo.setDirectSubtypes(directSubtypes); + } + } + + private void eliminateTrivialSupertypes() { + boolean changed; + do { + var toRemove = new ArrayList(); + for (var entry : extendedTypeInfoMap.entrySet()) { + var extendedTypeInfo = entry.getValue(); + boolean isAbstract = extendedTypeInfo.isAbstractType(); + // Do not eliminate abstract types with 0 subtypes, because they can be used para-consistently, i.e., + // an object determined to must have an abstract type with 0 subtypes may not ever exist. + boolean hasSingleDirectSubtype = extendedTypeInfo.getDirectSubtypes().size() == 1; + if (isAbstract && hasSingleDirectSubtype) { + toRemove.add(entry.getKey()); + } + } + toRemove.forEach(this::removeTrivialType); + changed = !toRemove.isEmpty(); + } while (changed); + } + + private void removeTrivialType(PartialRelation trivialType) { + var extendedTypeInfo = extendedTypeInfoMap.get(trivialType); + var iterator = extendedTypeInfo.getDirectSubtypes().iterator(); + if (!iterator.hasNext()) { + throw new AssertionError("Expected trivial supertype %s to have a direct subtype" + .formatted(trivialType)); + } + PartialRelation replacement = setReplacement(trivialType, iterator.next()); + if (iterator.hasNext()) { + throw new AssertionError("Expected trivial supertype %s to have at most 1 direct subtype" + .formatted(trivialType)); + } + replacements.put(trivialType, replacement); + for (var supertype : extendedTypeInfo.getAllSupertypes()) { + var extendedSupertypeInfo = extendedTypeInfoMap.get(supertype); + if (!extendedSupertypeInfo.getAllSubtypes().remove(trivialType)) { + throw new AssertionError("Expected %s to be subtype of %s".formatted(trivialType, supertype)); + } + var directSubtypes = extendedSupertypeInfo.getDirectSubtypes(); + if (directSubtypes.remove(trivialType)) { + directSubtypes.add(replacement); + } + } + for (var subtype : extendedTypeInfo.getAllSubtypes()) { + var extendedSubtypeInfo = extendedTypeInfoMap.get(subtype); + if (!extendedSubtypeInfo.getAllSupertypes().remove(trivialType)) { + throw new AssertionError("Expected %s to be supertype of %s".formatted(trivialType, subtype)); + } + } + extendedTypeInfoMap.remove(trivialType); + } + + private PartialRelation setReplacement(PartialRelation trivialRelation, PartialRelation replacement) { + if (replacement == null) { + return trivialRelation; + } + var resolved = setReplacement(replacement, replacements.get(replacement)); + replacements.put(trivialRelation, resolved); + return resolved; + } + + private Map computeAnalysisResults() { + var allExtendedTypeInfoList = sortTypes(); + var results = new LinkedHashMap( + allExtendedTypeInfoList.size() + replacements.size()); + for (var extendedTypeInfo : allExtendedTypeInfoList) { + var type = extendedTypeInfo.getType(); + results.put(type, new PreservedType(extendedTypeInfo, allExtendedTypeInfoList)); + } + for (var entry : replacements.entrySet()) { + var type = entry.getKey(); + results.put(type, new EliminatedType(entry.getValue())); + } + return Collections.unmodifiableMap(results); + } + + private List sortTypes() { + // Invert {@code directSubtypes} to keep track of the out-degree of types. + for (var extendedTypeInfo : extendedTypeInfoMap.values()) { + for (var directSubtype : extendedTypeInfo.getDirectSubtypes()) { + var extendedDirectSubtypeInfo = extendedTypeInfoMap.get(directSubtype); + extendedDirectSubtypeInfo.getUnsortedDirectSupertypes().add(extendedTypeInfo.getType()); + } + } + // Build a inverse topological order ({@code extends} edges always points to earlier nodes in the order, + // breaking ties according to the original order ({@link ExtendedTypeInfo#index}) to form a 'stable' sort. + // See, e.g., https://stackoverflow.com/a/11236027. + var priorityQueue = new PriorityQueue(); + for (var extendedTypeInfo : extendedTypeInfoMap.values()) { + if (extendedTypeInfo.getUnsortedDirectSupertypes().isEmpty()) { + priorityQueue.add(extendedTypeInfo); + } + } + var sorted = new ArrayList(extendedTypeInfoMap.size()); + while (!priorityQueue.isEmpty()) { + var extendedTypeInfo = priorityQueue.remove(); + sorted.add(extendedTypeInfo); + for (var directSubtype : extendedTypeInfo.getDirectSubtypes()) { + var extendedDirectSubtypeInfo = extendedTypeInfoMap.get(directSubtype); + var unsortedDirectSupertypes = extendedDirectSubtypeInfo.getUnsortedDirectSupertypes(); + if (!unsortedDirectSupertypes.remove(extendedTypeInfo.getType())) { + throw new AssertionError("Expected %s to be a direct supertype of %s" + .formatted(extendedTypeInfo.getType(), directSubtype)); + } + if (unsortedDirectSupertypes.isEmpty()) { + priorityQueue.add(extendedDirectSubtypeInfo); + } + } + } + return Collections.unmodifiableList(sorted); + } +} 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 new file mode 100644 index 00000000..c800b4cd --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeHierarchyTranslationUnit.java @@ -0,0 +1,52 @@ +package tools.refinery.store.reasoning.translator.typehierarchy; + +import tools.refinery.store.reasoning.AnyPartialInterpretation; +import tools.refinery.store.reasoning.literal.Modality; +import tools.refinery.store.reasoning.representation.AnyPartialSymbol; +import tools.refinery.store.reasoning.representation.PartialRelation; +import tools.refinery.store.reasoning.translator.Advice; +import tools.refinery.store.reasoning.translator.TranslationUnit; +import tools.refinery.store.model.Model; +import tools.refinery.store.query.Variable; +import tools.refinery.store.query.literal.CallPolarity; +import tools.refinery.store.query.literal.Literal; +import tools.refinery.store.representation.Symbol; + +import java.util.*; + +public class TypeHierarchyTranslationUnit extends TranslationUnit { + static final Symbol INFERRED_TYPE_SYMBOL = new Symbol<>("inferredType", 1, + InferredType.class, InferredType.UNTYPED); + + private final TypeAnalyzer typeAnalyzer; + + public TypeHierarchyTranslationUnit(Map typeInfoMap) { + typeAnalyzer = new TypeAnalyzer(typeInfoMap); + } + + @Override + public Collection getTranslatedPartialSymbols() { + return null; + } + + @Override + public void configure(Collection advices) { + + } + + @Override + public List call(CallPolarity polarity, Modality modality, PartialRelation target, + List arguments) { + return null; + } + + @Override + public Map createPartialInterpretations(Model model) { + return null; + } + + @Override + public void initializeModel(Model model, int nodeCount) { + + } +} diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeInfo.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeInfo.java new file mode 100644 index 00000000..313df4df --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeInfo.java @@ -0,0 +1,46 @@ +package tools.refinery.store.reasoning.translator.typehierarchy; + +import tools.refinery.store.reasoning.representation.PartialRelation; + +import java.util.*; + +public record TypeInfo(Collection supertypes, boolean abstractType) { + public static Builder builder() { + return new Builder(); + } + + public static class Builder { + private final Set supertypes = new LinkedHashSet<>(); + private boolean abstractType; + + private Builder() { + } + + public Builder supertypes(Collection supertypes) { + this.supertypes.addAll(supertypes); + return this; + } + + public Builder supertypes(PartialRelation... supertypes) { + return supertypes(List.of(supertypes)); + } + + public Builder supertype(PartialRelation supertype) { + supertypes.add(supertype); + return this; + } + + public Builder abstractType(boolean abstractType) { + this.abstractType = abstractType; + return this; + } + + public Builder abstractType() { + return abstractType(true); + } + + public TypeInfo build() { + return new TypeInfo(Collections.unmodifiableSet(supertypes), abstractType); + } + } +} diff --git a/subprojects/store-reasoning/src/test/java/tools/refinery/store/reasoning/translator/typehierarchy/InferredTypeTest.java b/subprojects/store-reasoning/src/test/java/tools/refinery/store/reasoning/translator/typehierarchy/InferredTypeTest.java new file mode 100644 index 00000000..a8df2312 --- /dev/null +++ b/subprojects/store-reasoning/src/test/java/tools/refinery/store/reasoning/translator/typehierarchy/InferredTypeTest.java @@ -0,0 +1,32 @@ +package tools.refinery.store.reasoning.translator.typehierarchy; + +import org.junit.jupiter.api.Test; +import tools.refinery.store.reasoning.representation.PartialRelation; + +import java.util.Set; + +import static org.hamcrest.MatcherAssert.assertThat; +import static org.hamcrest.Matchers.is; + +class InferredTypeTest { + private final PartialRelation c1 = new PartialRelation("C1", 1); + private final PartialRelation c2 = new PartialRelation("C2", 1); + + @Test + void untypedIsConsistentTest() { + var sut = new InferredType(Set.of(), Set.of(c1, c2), null); + assertThat(sut.isConsistent(), is(true)); + } + + @Test + void typedIsConsistentTest() { + var sut = new InferredType(Set.of(c1), Set.of(c1, c2), c1); + assertThat(sut.isConsistent(), is(true)); + } + + @Test + void typedIsInconsistentTest() { + var sut = new InferredType(Set.of(c1), Set.of(), null); + assertThat(sut.isConsistent(), is(false)); + } +} diff --git a/subprojects/store-reasoning/src/test/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeAnalyzerExampleHierarchyTest.java b/subprojects/store-reasoning/src/test/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeAnalyzerExampleHierarchyTest.java new file mode 100644 index 00000000..b2c1ef1b --- /dev/null +++ b/subprojects/store-reasoning/src/test/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeAnalyzerExampleHierarchyTest.java @@ -0,0 +1,203 @@ +package tools.refinery.store.reasoning.translator.typehierarchy; + +import org.junit.jupiter.api.BeforeEach; +import org.junit.jupiter.api.Test; +import tools.refinery.store.reasoning.representation.PartialRelation; +import tools.refinery.store.representation.TruthValue; + +import java.util.LinkedHashMap; +import java.util.Set; + +import static org.hamcrest.MatcherAssert.assertThat; +import static org.hamcrest.Matchers.is; +import static org.junit.jupiter.api.Assertions.assertAll; + +class TypeAnalyzerExampleHierarchyTest { + private final PartialRelation a1 = new PartialRelation("A1", 1); + private final PartialRelation a2 = new PartialRelation("A2", 1); + private final PartialRelation a3 = new PartialRelation("A3", 1); + private final PartialRelation a4 = new PartialRelation("A4", 1); + private final PartialRelation a5 = new PartialRelation("A5", 1); + private final PartialRelation c1 = new PartialRelation("C1", 1); + private final PartialRelation c2 = new PartialRelation("C2", 1); + private final PartialRelation c3 = new PartialRelation("C3", 1); + private final PartialRelation c4 = new PartialRelation("C4", 1); + + private TypeAnalyzer sut; + private TypeAnalyzerTester tester; + + @BeforeEach + void beforeEach() { + var typeInfoMap = new LinkedHashMap(); + typeInfoMap.put(a1, TypeInfo.builder().abstractType().build()); + typeInfoMap.put(a2, TypeInfo.builder().abstractType().build()); + typeInfoMap.put(a3, TypeInfo.builder().abstractType().build()); + typeInfoMap.put(a4, TypeInfo.builder().abstractType().build()); + typeInfoMap.put(a5, TypeInfo.builder().abstractType().build()); + typeInfoMap.put(c1, TypeInfo.builder().supertypes(a1, a4).build()); + typeInfoMap.put(c2, TypeInfo.builder().supertypes(a1, a2, a3, a4).build()); + typeInfoMap.put(c3, TypeInfo.builder().supertype(a3).build()); + typeInfoMap.put(c4, TypeInfo.builder().supertype(a4).build()); + sut = new TypeAnalyzer(typeInfoMap); + tester = new TypeAnalyzerTester(sut); + } + + @Test + void analysisResultsTest() { + assertAll( + () -> tester.assertAbstractType(a1, c1, c2), + () -> tester.assertEliminatedType(a2, c2), + () -> tester.assertAbstractType(a3, c2, c3), + () -> tester.assertAbstractType(a4, c1, c2, c4), + () -> tester.assertVacuousType(a5), + () -> tester.assertConcreteType(c1), + () -> tester.assertConcreteType(c2), + () -> tester.assertConcreteType(c3), + () -> tester.assertConcreteType(c4) + ); + } + + @Test + void inferredTypesTest() { + assertAll( + () -> assertThat(sut.getUnknownType(), is(new InferredType(Set.of(), Set.of(c1, c2, c3, c4), null))), + () -> assertThat(tester.getInferredType(a1), is(new InferredType(Set.of(a1, a4), Set.of(c1, c2), c1))), + () -> assertThat(tester.getInferredType(a3), is(new InferredType(Set.of(a3), Set.of(c2, c3), c2))), + () -> assertThat(tester.getInferredType(a4), is(new InferredType(Set.of(a4), Set.of(c1, c2, c4), c1))), + () -> assertThat(tester.getInferredType(a5), is(new InferredType(Set.of(a5), Set.of(), null))), + () -> assertThat(tester.getInferredType(c1), is(new InferredType(Set.of(a1, a4, c1), Set.of(c1), c1))), + () -> assertThat(tester.getInferredType(c2), + is(new InferredType(Set.of(a1, a3, a4, c2), Set.of(c2), c2))), + () -> assertThat(tester.getInferredType(c3), is(new InferredType(Set.of(a3, c3), Set.of(c3), c3))), + () -> assertThat(tester.getInferredType(c4), is(new InferredType(Set.of(a4, c4), Set.of(c4), c4))) + ); + } + + @Test + void consistentMustTest() { + var a1Result = tester.getPreservedType(a1); + var a3Result = tester.getPreservedType(a3); + var expected = new InferredType(Set.of(a1, a3, a4, c2), Set.of(c2), c2); + assertAll( + () -> assertThat(a1Result.merge(a3Result.asInferredType(), TruthValue.TRUE), is(expected)), + () -> assertThat(a3Result.merge(a1Result.asInferredType(), TruthValue.TRUE), is(expected)), + () -> assertThat(a1Result.merge(sut.getUnknownType(), TruthValue.TRUE), is(a1Result.asInferredType())), + () -> assertThat(a3Result.merge(sut.getUnknownType(), TruthValue.TRUE), is(a3Result.asInferredType())), + () -> assertThat(a1Result.merge(a1Result.asInferredType(), TruthValue.TRUE), + is(a1Result.asInferredType())) + ); + } + + @Test + void consistentMayNotTest() { + var a1Result = tester.getPreservedType(a1); + var a3Result = tester.getPreservedType(a3); + var a4Result = tester.getPreservedType(a4); + assertAll( + () -> assertThat(a1Result.merge(a3Result.asInferredType(), TruthValue.FALSE), + is(new InferredType(Set.of(a3, c3), Set.of(c3), c3))), + () -> assertThat(a3Result.merge(a1Result.asInferredType(), TruthValue.FALSE), + is(new InferredType(Set.of(a1, a4, c1), Set.of(c1), c1))), + () -> assertThat(a4Result.merge(a3Result.asInferredType(), TruthValue.FALSE), + is(new InferredType(Set.of(a3, c3), Set.of(c3), c3))), + () -> assertThat(a3Result.merge(a4Result.asInferredType(), TruthValue.FALSE), + is(new InferredType(Set.of(a4), Set.of(c1, c4), c1))), + () -> assertThat(a1Result.merge(sut.getUnknownType(), TruthValue.FALSE), + is(new InferredType(Set.of(), Set.of(c3, c4), null))), + () -> assertThat(a3Result.merge(sut.getUnknownType(), TruthValue.FALSE), + is(new InferredType(Set.of(), Set.of(c1, c4), null))), + () -> assertThat(a4Result.merge(sut.getUnknownType(), TruthValue.FALSE), + is(new InferredType(Set.of(), Set.of(c3), null))) + ); + } + + @Test + void consistentErrorTest() { + var c1Result = tester.getPreservedType(c1); + var a4Result = tester.getPreservedType(a4); + var expected = new InferredType(Set.of(c1, a1, a4), Set.of(), null); + assertAll( + () -> assertThat(c1Result.merge(a4Result.asInferredType(), TruthValue.ERROR), is(expected)), + () -> assertThat(a4Result.merge(c1Result.asInferredType(), TruthValue.ERROR), is(expected)) + ); + } + + @Test + void consistentUnknownTest() { + var c1Result = tester.getPreservedType(c1); + var a4Result = tester.getPreservedType(a4); + assertAll( + () -> assertThat(c1Result.merge(a4Result.asInferredType(), TruthValue.UNKNOWN), + is(a4Result.asInferredType())), + () -> assertThat(a4Result.merge(c1Result.asInferredType(), TruthValue.UNKNOWN), + is(c1Result.asInferredType())) + ); + } + + @Test + void inconsistentMustTest() { + var a1Result = tester.getPreservedType(a1); + var c3Result = tester.getPreservedType(c3); + assertAll( + () -> assertThat(a1Result.merge(c3Result.asInferredType(), TruthValue.TRUE), + is(new InferredType(Set.of(a1, a3, c3), Set.of(), null))), + () -> assertThat(c3Result.merge(a1Result.asInferredType(), TruthValue.TRUE), + is(new InferredType(Set.of(a1, a3, a4, c3), Set.of(), null))) + ); + } + + @Test + void inconsistentMayNotTest() { + var a1Result = tester.getPreservedType(a1); + var a4Result = tester.getPreservedType(a4); + var c1Result = tester.getPreservedType(c1); + assertAll( + () -> assertThat(a4Result.merge(a1Result.asInferredType(), TruthValue.FALSE), + is(new InferredType(Set.of(a1, a4), Set.of(), null))), + () -> assertThat(a1Result.merge(c1Result.asInferredType(), TruthValue.FALSE), + is(new InferredType(Set.of(a1, a4, c1), Set.of(), null))), + () -> assertThat(a4Result.merge(c1Result.asInferredType(), TruthValue.FALSE), + is(new InferredType(Set.of(a1, a4, c1), Set.of(), null))), + () -> assertThat(a1Result.merge(a1Result.asInferredType(), TruthValue.FALSE), + is(new InferredType(Set.of(a1, a4), Set.of(), null))) + ); + } + + @Test + void vacuousMustTest() { + var c1Result = tester.getPreservedType(c1); + var a5Result = tester.getPreservedType(a5); + assertAll( + () -> assertThat(c1Result.merge(a5Result.asInferredType(), TruthValue.TRUE), + is(new InferredType(Set.of(a1, a4, a5, c1), Set.of(), null))), + () -> assertThat(a5Result.merge(c1Result.asInferredType(), TruthValue.TRUE), + is(new InferredType(Set.of(a1, a4, a5, c1), Set.of(), null))) + ); + } + + @Test + void vacuousMayNotTest() { + var c1Result = tester.getPreservedType(c1); + var a5Result = tester.getPreservedType(a5); + assertAll( + () -> assertThat(c1Result.merge(a5Result.asInferredType(), TruthValue.FALSE), + is(a5Result.asInferredType())), + () -> assertThat(a5Result.merge(c1Result.asInferredType(), TruthValue.FALSE), + is(c1Result.asInferredType())) + ); + } + + @Test + void vacuousErrorTest() { + var c1Result = tester.getPreservedType(c1); + var a5Result = tester.getPreservedType(a5); + assertAll( + () -> assertThat(c1Result.merge(a5Result.asInferredType(), TruthValue.ERROR), + is(new InferredType(Set.of(a1, a4, a5, c1), Set.of(), null))), + () -> assertThat(a5Result.merge(c1Result.asInferredType(), TruthValue.ERROR), + is(new InferredType(Set.of(a1, a4, a5, c1), Set.of(), null))), + () -> assertThat(a5Result.merge(a5Result.asInferredType(), TruthValue.ERROR), + is(a5Result.asInferredType())) + ); + } +} diff --git a/subprojects/store-reasoning/src/test/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeAnalyzerTest.java b/subprojects/store-reasoning/src/test/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeAnalyzerTest.java new file mode 100644 index 00000000..b7b69ed8 --- /dev/null +++ b/subprojects/store-reasoning/src/test/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeAnalyzerTest.java @@ -0,0 +1,200 @@ +package tools.refinery.store.reasoning.translator.typehierarchy; + +import org.junit.jupiter.api.Test; +import tools.refinery.store.reasoning.representation.PartialRelation; +import tools.refinery.store.representation.TruthValue; + +import java.util.LinkedHashMap; +import java.util.Set; + +import static org.hamcrest.MatcherAssert.assertThat; +import static org.hamcrest.Matchers.is; +import static org.junit.jupiter.api.Assertions.assertAll; +import static org.junit.jupiter.api.Assertions.assertThrows; + +class TypeAnalyzerTest { + @Test + void directSupertypesTest() { + var c1 = new PartialRelation("C1", 1); + var c2 = new PartialRelation("C2", 1); + var c3 = new PartialRelation("C3", 1); + var typeInfoMap = new LinkedHashMap(); + typeInfoMap.put(c1, TypeInfo.builder().supertypes(c2, c3).build()); + typeInfoMap.put(c2, TypeInfo.builder().supertype(c3).build()); + typeInfoMap.put(c3, TypeInfo.builder().build()); + + var sut = new TypeAnalyzer(typeInfoMap); + var tester = new TypeAnalyzerTester(sut); + + assertAll( + () -> tester.assertConcreteType(c1), + () -> tester.assertConcreteType(c2, c1), + () -> tester.assertConcreteType(c3, c2) + ); + } + + @Test + void typeEliminationAbstractToConcreteTest() { + var c1 = new PartialRelation("C1", 1); + var c2 = new PartialRelation("C2", 1); + var a11 = new PartialRelation("A11", 1); + var a12 = new PartialRelation("A12", 1); + var a21 = new PartialRelation("A21", 1); + var a22 = new PartialRelation("A22", 1); + var a3 = new PartialRelation("A3", 1); + var typeInfoMap = new LinkedHashMap(); + typeInfoMap.put(a3, TypeInfo.builder().abstractType().build()); + typeInfoMap.put(a21, TypeInfo.builder().abstractType().supertype(a3).build()); + typeInfoMap.put(a22, TypeInfo.builder().abstractType().supertype(a3).build()); + typeInfoMap.put(a11, TypeInfo.builder().abstractType().supertypes(a21, a22).build()); + typeInfoMap.put(a12, TypeInfo.builder().abstractType().supertypes(a21, a22).build()); + typeInfoMap.put(c1, TypeInfo.builder().supertypes(a11, a12).build()); + typeInfoMap.put(c2, TypeInfo.builder().supertype(a3).build()); + + var sut = new TypeAnalyzer(typeInfoMap); + var tester = new TypeAnalyzerTester(sut); + + assertAll( + () -> tester.assertConcreteType(c1), + () -> tester.assertConcreteType(c2), + () -> tester.assertEliminatedType(a11, c1), + () -> tester.assertEliminatedType(a12, c1), + () -> tester.assertEliminatedType(a21, c1), + () -> tester.assertEliminatedType(a22, c1), + () -> tester.assertAbstractType(a3, c1, c2) + ); + } + + @Test + void typeEliminationConcreteToAbstractTest() { + var c1 = new PartialRelation("C1", 1); + var c2 = new PartialRelation("C2", 1); + var a11 = new PartialRelation("A11", 1); + var a12 = new PartialRelation("A12", 1); + var a21 = new PartialRelation("A21", 1); + var a22 = new PartialRelation("A22", 1); + var a3 = new PartialRelation("A3", 1); + var typeInfoMap = new LinkedHashMap(); + typeInfoMap.put(c1, TypeInfo.builder().supertypes(a11, a12).build()); + typeInfoMap.put(c2, TypeInfo.builder().supertype(a3).build()); + typeInfoMap.put(a11, TypeInfo.builder().abstractType().supertypes(a21, a22).build()); + typeInfoMap.put(a12, TypeInfo.builder().abstractType().supertypes(a21, a22).build()); + typeInfoMap.put(a21, TypeInfo.builder().abstractType().supertype(a3).build()); + typeInfoMap.put(a22, TypeInfo.builder().abstractType().supertype(a3).build()); + typeInfoMap.put(a3, TypeInfo.builder().abstractType().build()); + + var sut = new TypeAnalyzer(typeInfoMap); + var tester = new TypeAnalyzerTester(sut); + + assertAll( + () -> tester.assertConcreteType(c1), + () -> tester.assertConcreteType(c2), + () -> tester.assertEliminatedType(a11, c1), + () -> tester.assertEliminatedType(a12, c1), + () -> tester.assertEliminatedType(a21, c1), + () -> tester.assertEliminatedType(a22, c1), + () -> tester.assertAbstractType(a3, c1, c2) + ); + } + + @Test + void preserveConcreteTypeTest() { + var c1 = new PartialRelation("C1", 1); + var a1 = new PartialRelation("A1", 1); + var c2 = new PartialRelation("C2", 1); + var a2 = new PartialRelation("A2", 1); + var typeInfoMap = new LinkedHashMap(); + typeInfoMap.put(c1, TypeInfo.builder().supertype(a1).build()); + typeInfoMap.put(a1, TypeInfo.builder().abstractType().supertype(c2).build()); + typeInfoMap.put(c2, TypeInfo.builder().supertype(a2).build()); + typeInfoMap.put(a2, TypeInfo.builder().abstractType().build()); + + var sut = new TypeAnalyzer(typeInfoMap); + var tester = new TypeAnalyzerTester(sut); + + assertAll( + () -> tester.assertConcreteType(c1), + () -> tester.assertEliminatedType(a1, c1), + () -> tester.assertConcreteType(c2, c1), + () -> tester.assertEliminatedType(a2, c2) + ); + } + + @Test + void mostGeneralCurrentTypeTest() { + var c1 = new PartialRelation("C1", 1); + var c2 = new PartialRelation("C2", 1); + var c3 = new PartialRelation("C3", 1); + var typeInfoMap = new LinkedHashMap(); + typeInfoMap.put(c1, TypeInfo.builder().supertype(c3).build()); + typeInfoMap.put(c2, TypeInfo.builder().supertype(c3).build()); + typeInfoMap.put(c3, TypeInfo.builder().build()); + + var sut = new TypeAnalyzer(typeInfoMap); + var tester = new TypeAnalyzerTester(sut); + var c3Result = tester.getPreservedType(c3); + + var expected = new InferredType(Set.of(c3), Set.of(c1, c2, c3), c3); + assertAll( + () -> assertThat(tester.getInferredType(c3), is(expected)), + () -> assertThat(c3Result.merge(sut.getUnknownType(), TruthValue.TRUE), is(expected)) + ); + } + + @Test + void preferFirstConcreteTypeTest() { + var a1 = new PartialRelation("A1", 1); + var c1 = new PartialRelation("C1", 1); + var c2 = new PartialRelation("C2", 1); + var c3 = new PartialRelation("C3", 1); + var c4 = new PartialRelation("C4", 1); + var typeInfoMap = new LinkedHashMap(); + typeInfoMap.put(c1, TypeInfo.builder().supertype(a1).build()); + typeInfoMap.put(c2, TypeInfo.builder().supertype(a1).build()); + typeInfoMap.put(c3, TypeInfo.builder().supertype(a1).build()); + typeInfoMap.put(c4, TypeInfo.builder().supertype(c3).build()); + typeInfoMap.put(a1, TypeInfo.builder().abstractType().build()); + + var sut = new TypeAnalyzer(typeInfoMap); + var tester = new TypeAnalyzerTester(sut); + var c1Result = tester.getPreservedType(c1); + var a1Result = tester.getPreservedType(a1); + + assertThat(c1Result.merge(a1Result.asInferredType(), TruthValue.FALSE), + is(new InferredType(Set.of(a1), Set.of(c2, c3, c4), c2))); + } + + @Test + void preferFirstMostGeneralConcreteTypeTest() { + var a1 = new PartialRelation("A1", 1); + var c1 = new PartialRelation("C1", 1); + var c2 = new PartialRelation("C2", 1); + var c3 = new PartialRelation("C3", 1); + var c4 = new PartialRelation("C4", 1); + var typeInfoMap = new LinkedHashMap(); + typeInfoMap.put(c4, TypeInfo.builder().supertype(c3).build()); + typeInfoMap.put(c3, TypeInfo.builder().supertype(a1).build()); + typeInfoMap.put(c2, TypeInfo.builder().supertype(a1).build()); + typeInfoMap.put(c1, TypeInfo.builder().supertype(a1).build()); + typeInfoMap.put(a1, TypeInfo.builder().abstractType().build()); + + var sut = new TypeAnalyzer(typeInfoMap); + var tester = new TypeAnalyzerTester(sut); + var c1Result = tester.getPreservedType(c1); + var a1Result = tester.getPreservedType(a1); + + assertThat(c1Result.merge(a1Result.asInferredType(), TruthValue.FALSE), + is(new InferredType(Set.of(a1), Set.of(c2, c3, c4), c3))); + } + + @Test + void circularTypeHierarchyTest() { + var c1 = new PartialRelation("C1", 1); + var c2 = new PartialRelation("C2", 1); + var typeInfoMap = new LinkedHashMap(); + typeInfoMap.put(c1, TypeInfo.builder().supertype(c2).build()); + typeInfoMap.put(c2, TypeInfo.builder().supertype(c1).build()); + + assertThrows(IllegalArgumentException.class, () -> new TypeAnalyzer(typeInfoMap)); + } +} diff --git a/subprojects/store-reasoning/src/test/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeAnalyzerTester.java b/subprojects/store-reasoning/src/test/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeAnalyzerTester.java new file mode 100644 index 00000000..56407730 --- /dev/null +++ b/subprojects/store-reasoning/src/test/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeAnalyzerTester.java @@ -0,0 +1,51 @@ +package tools.refinery.store.reasoning.translator.typehierarchy; + +import tools.refinery.store.reasoning.representation.PartialRelation; + +import static org.hamcrest.MatcherAssert.assertThat; +import static org.hamcrest.Matchers.*; +import static org.hamcrest.Matchers.is; + +class TypeAnalyzerTester { + private final TypeAnalyzer sut; + + public TypeAnalyzerTester(TypeAnalyzer sut) { + this.sut = sut; + } + + public void assertAbstractType(PartialRelation partialRelation, PartialRelation... directSubtypes) { + assertPreservedType(partialRelation, true, false, directSubtypes); + } + + public void assertVacuousType(PartialRelation partialRelation) { + assertPreservedType(partialRelation, true, true); + } + + public void assertConcreteType(PartialRelation partialRelation, PartialRelation... directSubtypes) { + assertPreservedType(partialRelation, false, false, directSubtypes); + } + + private void assertPreservedType(PartialRelation partialRelation, boolean isAbstract, boolean isVacuous, + PartialRelation... directSubtypes) { + var result = sut.getAnalysisResults().get(partialRelation); + assertThat(result, is(instanceOf(PreservedType.class))); + var preservedResult = (PreservedType) result; + assertThat(preservedResult.isAbstractType(), is(isAbstract)); + assertThat(preservedResult.isVacuous(), is(isVacuous)); + assertThat(preservedResult.getDirectSubtypes(), hasItems(directSubtypes)); + } + + public void assertEliminatedType(PartialRelation partialRelation, PartialRelation replacement) { + var result = sut.getAnalysisResults().get(partialRelation); + assertThat(result, is(instanceOf(EliminatedType.class))); + assertThat(((EliminatedType) result).replacement(), is(replacement)); + } + + public PreservedType getPreservedType(PartialRelation partialRelation) { + return (PreservedType) sut.getAnalysisResults().get(partialRelation); + } + + public InferredType getInferredType(PartialRelation partialRelation) { + return getPreservedType(partialRelation).asInferredType(); + } +} -- cgit v1.2.3-54-g00ecf