diff options
19 files changed, 843 insertions, 305 deletions
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/proxy/PartialRelationTranslatorProxy.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/proxy/PartialRelationTranslatorProxy.java new file mode 100644 index 00000000..45dc5bd2 --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/proxy/PartialRelationTranslatorProxy.java | |||
@@ -0,0 +1,52 @@ | |||
1 | /* | ||
2 | * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/> | ||
3 | * | ||
4 | * SPDX-License-Identifier: EPL-2.0 | ||
5 | */ | ||
6 | package tools.refinery.store.reasoning.translator.proxy; | ||
7 | |||
8 | import tools.refinery.store.model.ModelStoreBuilder; | ||
9 | import tools.refinery.store.model.ModelStoreConfiguration; | ||
10 | import tools.refinery.store.query.literal.AbstractCallLiteral; | ||
11 | import tools.refinery.store.query.literal.Literal; | ||
12 | import tools.refinery.store.query.term.Variable; | ||
13 | import tools.refinery.store.reasoning.interpretation.PartialRelationRewriter; | ||
14 | import tools.refinery.store.reasoning.literal.Concreteness; | ||
15 | import tools.refinery.store.reasoning.literal.ModalConstraint; | ||
16 | import tools.refinery.store.reasoning.literal.Modality; | ||
17 | import tools.refinery.store.reasoning.representation.PartialRelation; | ||
18 | import tools.refinery.store.reasoning.translator.PartialRelationTranslator; | ||
19 | |||
20 | import java.util.List; | ||
21 | import java.util.Set; | ||
22 | |||
23 | public class PartialRelationTranslatorProxy implements ModelStoreConfiguration, PartialRelationRewriter { | ||
24 | private final PartialRelation partialRelation; | ||
25 | private final PartialRelation targetRelation; | ||
26 | private final boolean mutable; | ||
27 | |||
28 | public PartialRelationTranslatorProxy(PartialRelation partialRelation, PartialRelation targetRelation, | ||
29 | boolean mutable) { | ||
30 | this.partialRelation = partialRelation; | ||
31 | this.targetRelation = targetRelation; | ||
32 | this.mutable = mutable; | ||
33 | } | ||
34 | |||
35 | @Override | ||
36 | public void apply(ModelStoreBuilder storeBuilder) { | ||
37 | var translator = PartialRelationTranslator.of(partialRelation) | ||
38 | .interpretation(((adapter, concreteness, partialSymbol) -> | ||
39 | adapter.getPartialInterpretation(concreteness, targetRelation))) | ||
40 | .rewriter(this); | ||
41 | if (mutable) { | ||
42 | translator.refiner((adapter, partialSymbol) -> adapter.getRefiner(targetRelation)); | ||
43 | } | ||
44 | storeBuilder.with(translator); | ||
45 | } | ||
46 | |||
47 | @Override | ||
48 | public List<Literal> rewriteLiteral(Set<Variable> positiveVariables, AbstractCallLiteral literal, | ||
49 | Modality modality, Concreteness concreteness) { | ||
50 | return List.of(literal.withTarget(ModalConstraint.of(modality, concreteness, targetRelation))); | ||
51 | } | ||
52 | } | ||
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/CandidateTypeView.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/CandidateTypeView.java new file mode 100644 index 00000000..faf1b958 --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/CandidateTypeView.java | |||
@@ -0,0 +1,21 @@ | |||
1 | /* | ||
2 | * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/> | ||
3 | * | ||
4 | * SPDX-License-Identifier: EPL-2.0 | ||
5 | */ | ||
6 | package tools.refinery.store.reasoning.translator.typehierarchy; | ||
7 | |||
8 | import tools.refinery.store.reasoning.representation.PartialRelation; | ||
9 | import tools.refinery.store.representation.Symbol; | ||
10 | import tools.refinery.store.tuple.Tuple; | ||
11 | |||
12 | class CandidateTypeView extends InferredTypeView { | ||
13 | public CandidateTypeView(Symbol<InferredType> symbol, PartialRelation type) { | ||
14 | super(symbol, "candidate", type); | ||
15 | } | ||
16 | |||
17 | @Override | ||
18 | protected boolean doFilter(Tuple key, InferredType value) { | ||
19 | return type.equals(value.candidateType()); | ||
20 | } | ||
21 | } | ||
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 deleted file mode 100644 index 6e4728db..00000000 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/EliminatedType.java +++ /dev/null | |||
@@ -1,11 +0,0 @@ | |||
1 | /* | ||
2 | * SPDX-FileCopyrightText: 2021-2023 The Refinery Authors <https://refinery.tools/> | ||
3 | * | ||
4 | * SPDX-License-Identifier: EPL-2.0 | ||
5 | */ | ||
6 | package tools.refinery.store.reasoning.translator.typehierarchy; | ||
7 | |||
8 | import tools.refinery.store.reasoning.representation.PartialRelation; | ||
9 | |||
10 | record EliminatedType(PartialRelation replacement) implements TypeAnalysisResult { | ||
11 | } | ||
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 index fd05158b..1ae94ae1 100644 --- 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 | |||
@@ -11,18 +11,18 @@ import java.util.Collections; | |||
11 | import java.util.Set; | 11 | import java.util.Set; |
12 | 12 | ||
13 | record InferredType(Set<PartialRelation> mustTypes, Set<PartialRelation> mayConcreteTypes, | 13 | record InferredType(Set<PartialRelation> mustTypes, Set<PartialRelation> mayConcreteTypes, |
14 | PartialRelation currentType) { | 14 | PartialRelation candidateType) { |
15 | public static final InferredType UNTYPED = new InferredType(Set.of(), Set.of(), null); | 15 | public static final InferredType UNTYPED = new InferredType(Set.of(), Set.of(), null); |
16 | 16 | ||
17 | public InferredType(Set<PartialRelation> mustTypes, Set<PartialRelation> mayConcreteTypes, | 17 | public InferredType(Set<PartialRelation> mustTypes, Set<PartialRelation> mayConcreteTypes, |
18 | PartialRelation currentType) { | 18 | PartialRelation candidateType) { |
19 | this.mustTypes = Collections.unmodifiableSet(mustTypes); | 19 | this.mustTypes = Collections.unmodifiableSet(mustTypes); |
20 | this.mayConcreteTypes = Collections.unmodifiableSet(mayConcreteTypes); | 20 | this.mayConcreteTypes = Collections.unmodifiableSet(mayConcreteTypes); |
21 | this.currentType = currentType; | 21 | this.candidateType = candidateType; |
22 | } | 22 | } |
23 | 23 | ||
24 | public boolean isConsistent() { | 24 | public boolean isConsistent() { |
25 | return currentType != null || mustTypes.isEmpty(); | 25 | return candidateType != null || mustTypes.isEmpty(); |
26 | } | 26 | } |
27 | 27 | ||
28 | public boolean isMust(PartialRelation partialRelation) { | 28 | public boolean isMust(PartialRelation partialRelation) { |
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/InferredTypeRefiner.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/InferredTypeRefiner.java new file mode 100644 index 00000000..40a7b3fa --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/InferredTypeRefiner.java | |||
@@ -0,0 +1,38 @@ | |||
1 | /* | ||
2 | * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/> | ||
3 | * | ||
4 | * SPDX-License-Identifier: EPL-2.0 | ||
5 | */ | ||
6 | package tools.refinery.store.reasoning.translator.typehierarchy; | ||
7 | |||
8 | import tools.refinery.store.model.Interpretation; | ||
9 | import tools.refinery.store.reasoning.ReasoningAdapter; | ||
10 | import tools.refinery.store.reasoning.refinement.AbstractPartialInterpretationRefiner; | ||
11 | import tools.refinery.store.reasoning.representation.PartialSymbol; | ||
12 | import tools.refinery.store.representation.Symbol; | ||
13 | import tools.refinery.store.representation.TruthValue; | ||
14 | import tools.refinery.store.tuple.Tuple; | ||
15 | |||
16 | class InferredTypeRefiner extends AbstractPartialInterpretationRefiner<TruthValue, Boolean> { | ||
17 | private final Interpretation<InferredType> interpretation; | ||
18 | private final TypeAnalysisResult result; | ||
19 | |||
20 | private InferredTypeRefiner(ReasoningAdapter adapter, PartialSymbol<TruthValue, Boolean> partialSymbol, | ||
21 | Symbol<InferredType> symbol, TypeAnalysisResult result) { | ||
22 | super(adapter, partialSymbol); | ||
23 | interpretation = adapter.getModel().getInterpretation(symbol); | ||
24 | this.result = result; | ||
25 | } | ||
26 | |||
27 | @Override | ||
28 | public boolean merge(Tuple key, TruthValue value) { | ||
29 | var currentType = interpretation.get(key); | ||
30 | var newType = result.merge(currentType, value); | ||
31 | interpretation.put(key, newType); | ||
32 | return true; | ||
33 | } | ||
34 | |||
35 | public static Factory<TruthValue, Boolean> of(Symbol<InferredType> symbol, TypeAnalysisResult result) { | ||
36 | return (adapter, partialSymbol) -> new InferredTypeRefiner(adapter, partialSymbol, symbol, result); | ||
37 | } | ||
38 | } | ||
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/InferredTypeView.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/InferredTypeView.java new file mode 100644 index 00000000..3c074df5 --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/InferredTypeView.java | |||
@@ -0,0 +1,35 @@ | |||
1 | /* | ||
2 | * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/> | ||
3 | * | ||
4 | * SPDX-License-Identifier: EPL-2.0 | ||
5 | */ | ||
6 | package tools.refinery.store.reasoning.translator.typehierarchy; | ||
7 | |||
8 | import tools.refinery.store.query.view.TuplePreservingView; | ||
9 | import tools.refinery.store.reasoning.representation.PartialRelation; | ||
10 | import tools.refinery.store.representation.Symbol; | ||
11 | |||
12 | import java.util.Objects; | ||
13 | |||
14 | abstract class InferredTypeView extends TuplePreservingView<InferredType> { | ||
15 | protected final PartialRelation type; | ||
16 | |||
17 | protected InferredTypeView(Symbol<InferredType> symbol, String name, PartialRelation type) { | ||
18 | super(symbol, type.name() + "#" + name); | ||
19 | this.type = type; | ||
20 | } | ||
21 | |||
22 | @Override | ||
23 | public boolean equals(Object o) { | ||
24 | if (this == o) return true; | ||
25 | if (o == null || getClass() != o.getClass()) return false; | ||
26 | if (!super.equals(o)) return false; | ||
27 | InferredTypeView that = (InferredTypeView) o; | ||
28 | return Objects.equals(type, that.type); | ||
29 | } | ||
30 | |||
31 | @Override | ||
32 | public int hashCode() { | ||
33 | return Objects.hash(super.hashCode(), type); | ||
34 | } | ||
35 | } | ||
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/MayTypeView.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/MayTypeView.java new file mode 100644 index 00000000..dcaf61c5 --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/MayTypeView.java | |||
@@ -0,0 +1,21 @@ | |||
1 | /* | ||
2 | * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/> | ||
3 | * | ||
4 | * SPDX-License-Identifier: EPL-2.0 | ||
5 | */ | ||
6 | package tools.refinery.store.reasoning.translator.typehierarchy; | ||
7 | |||
8 | import tools.refinery.store.reasoning.representation.PartialRelation; | ||
9 | import tools.refinery.store.representation.Symbol; | ||
10 | import tools.refinery.store.tuple.Tuple; | ||
11 | |||
12 | class MayTypeView extends InferredTypeView { | ||
13 | public MayTypeView(Symbol<InferredType> symbol, PartialRelation type) { | ||
14 | super(symbol, "may", type); | ||
15 | } | ||
16 | |||
17 | @Override | ||
18 | protected boolean doFilter(Tuple key, InferredType value) { | ||
19 | return value.mayConcreteTypes().contains(type); | ||
20 | } | ||
21 | } | ||
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/MustTypeView.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/MustTypeView.java new file mode 100644 index 00000000..833e1594 --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/MustTypeView.java | |||
@@ -0,0 +1,21 @@ | |||
1 | /* | ||
2 | * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/> | ||
3 | * | ||
4 | * SPDX-License-Identifier: EPL-2.0 | ||
5 | */ | ||
6 | package tools.refinery.store.reasoning.translator.typehierarchy; | ||
7 | |||
8 | import tools.refinery.store.reasoning.representation.PartialRelation; | ||
9 | import tools.refinery.store.representation.Symbol; | ||
10 | import tools.refinery.store.tuple.Tuple; | ||
11 | |||
12 | class MustTypeView extends InferredTypeView { | ||
13 | public MustTypeView(Symbol<InferredType> symbol, PartialRelation type) { | ||
14 | super(symbol, "must", type); | ||
15 | } | ||
16 | |||
17 | @Override | ||
18 | protected boolean doFilter(Tuple key, InferredType value) { | ||
19 | return value.mustTypes().contains(type); | ||
20 | } | ||
21 | } | ||
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 deleted file mode 100644 index 0696f4c3..00000000 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/PreservedType.java +++ /dev/null | |||
@@ -1,141 +0,0 @@ | |||
1 | /* | ||
2 | * SPDX-FileCopyrightText: 2021-2023 The Refinery Authors <https://refinery.tools/> | ||
3 | * | ||
4 | * SPDX-License-Identifier: EPL-2.0 | ||
5 | */ | ||
6 | package tools.refinery.store.reasoning.translator.typehierarchy; | ||
7 | |||
8 | import tools.refinery.store.reasoning.representation.PartialRelation; | ||
9 | import tools.refinery.store.representation.TruthValue; | ||
10 | |||
11 | import java.util.*; | ||
12 | |||
13 | final class PreservedType implements TypeAnalysisResult { | ||
14 | private final ExtendedTypeInfo extendedTypeInfo; | ||
15 | private final List<PartialRelation> directSubtypes; | ||
16 | private final List<ExtendedTypeInfo> allExternalTypeInfoList; | ||
17 | private final InferredType inferredType; | ||
18 | |||
19 | public PreservedType(ExtendedTypeInfo extendedTypeInfo, List<ExtendedTypeInfo> allExternalTypeInfoList) { | ||
20 | this.extendedTypeInfo = extendedTypeInfo; | ||
21 | directSubtypes = List.copyOf(extendedTypeInfo.getDirectSubtypes()); | ||
22 | this.allExternalTypeInfoList = allExternalTypeInfoList; | ||
23 | inferredType = propagateMust(extendedTypeInfo.getAllSupertypesAndSelf(), | ||
24 | extendedTypeInfo.getConcreteSubtypesAndSelf()); | ||
25 | } | ||
26 | |||
27 | public PartialRelation type() { | ||
28 | return extendedTypeInfo.getType(); | ||
29 | } | ||
30 | |||
31 | public List<PartialRelation> getDirectSubtypes() { | ||
32 | return directSubtypes; | ||
33 | } | ||
34 | |||
35 | public boolean isAbstractType() { | ||
36 | return extendedTypeInfo.isAbstractType(); | ||
37 | } | ||
38 | |||
39 | public boolean isVacuous() { | ||
40 | return isAbstractType() && directSubtypes.isEmpty(); | ||
41 | } | ||
42 | |||
43 | public InferredType asInferredType() { | ||
44 | return inferredType; | ||
45 | } | ||
46 | |||
47 | public InferredType merge(InferredType inferredType, TruthValue value) { | ||
48 | return switch (value) { | ||
49 | case UNKNOWN -> inferredType; | ||
50 | case TRUE -> addMust(inferredType); | ||
51 | case FALSE -> removeMay(inferredType); | ||
52 | case ERROR -> addError(inferredType); | ||
53 | }; | ||
54 | } | ||
55 | |||
56 | private InferredType addMust(InferredType inferredType) { | ||
57 | var originalMustTypes = inferredType.mustTypes(); | ||
58 | if (originalMustTypes.contains(type())) { | ||
59 | return inferredType; | ||
60 | } | ||
61 | var mustTypes = new HashSet<>(originalMustTypes); | ||
62 | extendedTypeInfo.addMust(mustTypes); | ||
63 | var originalMayConcreteTypes = inferredType.mayConcreteTypes(); | ||
64 | var mayConcreteTypes = new LinkedHashSet<>(originalMayConcreteTypes); | ||
65 | Set<PartialRelation> mayConcreteTypesResult; | ||
66 | if (mayConcreteTypes.retainAll(extendedTypeInfo.getConcreteSubtypesAndSelf())) { | ||
67 | mayConcreteTypesResult = mayConcreteTypes; | ||
68 | } else { | ||
69 | mayConcreteTypesResult = originalMayConcreteTypes; | ||
70 | } | ||
71 | return propagateMust(mustTypes, mayConcreteTypesResult); | ||
72 | } | ||
73 | |||
74 | private InferredType removeMay(InferredType inferredType) { | ||
75 | var originalMayConcreteTypes = inferredType.mayConcreteTypes(); | ||
76 | var mayConcreteTypes = new LinkedHashSet<>(originalMayConcreteTypes); | ||
77 | if (!mayConcreteTypes.removeAll(extendedTypeInfo.getConcreteSubtypesAndSelf())) { | ||
78 | return inferredType; | ||
79 | } | ||
80 | return propagateMust(inferredType.mustTypes(), mayConcreteTypes); | ||
81 | } | ||
82 | |||
83 | private InferredType addError(InferredType inferredType) { | ||
84 | var originalMustTypes = inferredType.mustTypes(); | ||
85 | if (originalMustTypes.contains(type())) { | ||
86 | if (inferredType.mayConcreteTypes().isEmpty()) { | ||
87 | return inferredType; | ||
88 | } | ||
89 | return new InferredType(originalMustTypes, Set.of(), null); | ||
90 | } | ||
91 | var mustTypes = new HashSet<>(originalMustTypes); | ||
92 | extendedTypeInfo.addMust(mustTypes); | ||
93 | return new InferredType(mustTypes, Set.of(), null); | ||
94 | } | ||
95 | |||
96 | private InferredType propagateMust(Set<PartialRelation> originalMustTypes, | ||
97 | Set<PartialRelation> mayConcreteTypes) { | ||
98 | // It is possible that there is not type at all, do not force one by propagation. | ||
99 | var maybeUntyped = originalMustTypes.isEmpty(); | ||
100 | // Para-consistent case, do not propagate must types to avoid logical explosion. | ||
101 | var paraConsistentOrSurelyUntyped = mayConcreteTypes.isEmpty(); | ||
102 | if (maybeUntyped || paraConsistentOrSurelyUntyped) { | ||
103 | return new InferredType(originalMustTypes, mayConcreteTypes, null); | ||
104 | } | ||
105 | var currentType = computeCurrentType(mayConcreteTypes); | ||
106 | var mustTypes = new HashSet<>(originalMustTypes); | ||
107 | boolean changed = false; | ||
108 | for (var newMustExtendedTypeInfo : allExternalTypeInfoList) { | ||
109 | var newMustType = newMustExtendedTypeInfo.getType(); | ||
110 | if (mustTypes.contains(newMustType)) { | ||
111 | continue; | ||
112 | } | ||
113 | if (newMustExtendedTypeInfo.allowsAllConcreteTypes(mayConcreteTypes)) { | ||
114 | newMustExtendedTypeInfo.addMust(mustTypes); | ||
115 | changed = true; | ||
116 | } | ||
117 | } | ||
118 | if (!changed) { | ||
119 | return new InferredType(originalMustTypes, mayConcreteTypes, currentType); | ||
120 | } | ||
121 | return new InferredType(mustTypes, mayConcreteTypes, currentType); | ||
122 | } | ||
123 | |||
124 | /** | ||
125 | * Returns a concrete type that is allowed by a (consistent, i.e., nonempty) set of <b>may</b> concrete types. | ||
126 | * | ||
127 | * @param mayConcreteTypes The set of allowed concrete types. Must not be empty. | ||
128 | * @return The first concrete type that is allowed by {@code matConcreteTypes}. | ||
129 | */ | ||
130 | private PartialRelation computeCurrentType(Set<PartialRelation> mayConcreteTypes) { | ||
131 | for (var concreteExtendedTypeInfo : allExternalTypeInfoList) { | ||
132 | var concreteType = concreteExtendedTypeInfo.getType(); | ||
133 | if (!concreteExtendedTypeInfo.isAbstractType() && mayConcreteTypes.contains(concreteType)) { | ||
134 | return concreteType; | ||
135 | } | ||
136 | } | ||
137 | // We have already filtered out the para-consistent case in {@link #propagateMust(Set<PartialRelation>, | ||
138 | // Set<PartialRelation>}. | ||
139 | throw new AssertionError("No concrete type in %s".formatted(mayConcreteTypes)); | ||
140 | } | ||
141 | } | ||
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 index fbf8a7c9..39a76745 100644 --- 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 | |||
@@ -5,5 +5,137 @@ | |||
5 | */ | 5 | */ |
6 | package tools.refinery.store.reasoning.translator.typehierarchy; | 6 | package tools.refinery.store.reasoning.translator.typehierarchy; |
7 | 7 | ||
8 | sealed interface TypeAnalysisResult permits EliminatedType, PreservedType { | 8 | import tools.refinery.store.reasoning.representation.PartialRelation; |
9 | import tools.refinery.store.representation.TruthValue; | ||
10 | |||
11 | import java.util.*; | ||
12 | |||
13 | final class TypeAnalysisResult { | ||
14 | private final ExtendedTypeInfo extendedTypeInfo; | ||
15 | private final List<PartialRelation> directSubtypes; | ||
16 | private final List<ExtendedTypeInfo> allExternalTypeInfoList; | ||
17 | private final InferredType inferredType; | ||
18 | |||
19 | public TypeAnalysisResult(ExtendedTypeInfo extendedTypeInfo, List<ExtendedTypeInfo> allExternalTypeInfoList) { | ||
20 | this.extendedTypeInfo = extendedTypeInfo; | ||
21 | directSubtypes = List.copyOf(extendedTypeInfo.getDirectSubtypes()); | ||
22 | this.allExternalTypeInfoList = allExternalTypeInfoList; | ||
23 | inferredType = propagateMust(extendedTypeInfo.getAllSupertypesAndSelf(), | ||
24 | extendedTypeInfo.getConcreteSubtypesAndSelf()); | ||
25 | } | ||
26 | |||
27 | public PartialRelation type() { | ||
28 | return extendedTypeInfo.getType(); | ||
29 | } | ||
30 | |||
31 | public List<PartialRelation> getDirectSubtypes() { | ||
32 | return directSubtypes; | ||
33 | } | ||
34 | |||
35 | public boolean isAbstractType() { | ||
36 | return extendedTypeInfo.isAbstractType(); | ||
37 | } | ||
38 | |||
39 | public boolean isVacuous() { | ||
40 | return isAbstractType() && directSubtypes.isEmpty(); | ||
41 | } | ||
42 | |||
43 | public InferredType asInferredType() { | ||
44 | return inferredType; | ||
45 | } | ||
46 | |||
47 | public InferredType merge(InferredType inferredType, TruthValue value) { | ||
48 | return switch (value) { | ||
49 | case UNKNOWN -> inferredType; | ||
50 | case TRUE -> addMust(inferredType); | ||
51 | case FALSE -> removeMay(inferredType); | ||
52 | case ERROR -> addError(inferredType); | ||
53 | }; | ||
54 | } | ||
55 | |||
56 | private InferredType addMust(InferredType inferredType) { | ||
57 | var originalMustTypes = inferredType.mustTypes(); | ||
58 | if (originalMustTypes.contains(type())) { | ||
59 | return inferredType; | ||
60 | } | ||
61 | var mustTypes = new HashSet<>(originalMustTypes); | ||
62 | extendedTypeInfo.addMust(mustTypes); | ||
63 | var originalMayConcreteTypes = inferredType.mayConcreteTypes(); | ||
64 | var mayConcreteTypes = new LinkedHashSet<>(originalMayConcreteTypes); | ||
65 | Set<PartialRelation> mayConcreteTypesResult; | ||
66 | if (mayConcreteTypes.retainAll(extendedTypeInfo.getConcreteSubtypesAndSelf())) { | ||
67 | mayConcreteTypesResult = mayConcreteTypes; | ||
68 | } else { | ||
69 | mayConcreteTypesResult = originalMayConcreteTypes; | ||
70 | } | ||
71 | return propagateMust(mustTypes, mayConcreteTypesResult); | ||
72 | } | ||
73 | |||
74 | private InferredType removeMay(InferredType inferredType) { | ||
75 | var originalMayConcreteTypes = inferredType.mayConcreteTypes(); | ||
76 | var mayConcreteTypes = new LinkedHashSet<>(originalMayConcreteTypes); | ||
77 | if (!mayConcreteTypes.removeAll(extendedTypeInfo.getConcreteSubtypesAndSelf())) { | ||
78 | return inferredType; | ||
79 | } | ||
80 | return propagateMust(inferredType.mustTypes(), mayConcreteTypes); | ||
81 | } | ||
82 | |||
83 | private InferredType addError(InferredType inferredType) { | ||
84 | var originalMustTypes = inferredType.mustTypes(); | ||
85 | if (originalMustTypes.contains(type())) { | ||
86 | if (inferredType.mayConcreteTypes().isEmpty()) { | ||
87 | return inferredType; | ||
88 | } | ||
89 | return new InferredType(originalMustTypes, Set.of(), null); | ||
90 | } | ||
91 | var mustTypes = new HashSet<>(originalMustTypes); | ||
92 | extendedTypeInfo.addMust(mustTypes); | ||
93 | return new InferredType(mustTypes, Set.of(), null); | ||
94 | } | ||
95 | |||
96 | private InferredType propagateMust(Set<PartialRelation> originalMustTypes, | ||
97 | Set<PartialRelation> mayConcreteTypes) { | ||
98 | // It is possible that there is not type at all, do not force one by propagation. | ||
99 | var maybeUntyped = originalMustTypes.isEmpty(); | ||
100 | // Para-consistent case, do not propagate must types to avoid logical explosion. | ||
101 | var paraConsistentOrSurelyUntyped = mayConcreteTypes.isEmpty(); | ||
102 | if (maybeUntyped || paraConsistentOrSurelyUntyped) { | ||
103 | return new InferredType(originalMustTypes, mayConcreteTypes, null); | ||
104 | } | ||
105 | var currentType = computeCurrentType(mayConcreteTypes); | ||
106 | var mustTypes = new HashSet<>(originalMustTypes); | ||
107 | boolean changed = false; | ||
108 | for (var newMustExtendedTypeInfo : allExternalTypeInfoList) { | ||
109 | var newMustType = newMustExtendedTypeInfo.getType(); | ||
110 | if (mustTypes.contains(newMustType)) { | ||
111 | continue; | ||
112 | } | ||
113 | if (newMustExtendedTypeInfo.allowsAllConcreteTypes(mayConcreteTypes)) { | ||
114 | newMustExtendedTypeInfo.addMust(mustTypes); | ||
115 | changed = true; | ||
116 | } | ||
117 | } | ||
118 | if (!changed) { | ||
119 | return new InferredType(originalMustTypes, mayConcreteTypes, currentType); | ||
120 | } | ||
121 | return new InferredType(mustTypes, mayConcreteTypes, currentType); | ||
122 | } | ||
123 | |||
124 | /** | ||
125 | * Returns a concrete type that is allowed by a (consistent, i.e., nonempty) set of <b>may</b> concrete types. | ||
126 | * | ||
127 | * @param mayConcreteTypes The set of allowed concrete types. Must not be empty. | ||
128 | * @return The first concrete type that is allowed by {@code matConcreteTypes}. | ||
129 | */ | ||
130 | private PartialRelation computeCurrentType(Set<PartialRelation> mayConcreteTypes) { | ||
131 | for (var concreteExtendedTypeInfo : allExternalTypeInfoList) { | ||
132 | var concreteType = concreteExtendedTypeInfo.getType(); | ||
133 | if (!concreteExtendedTypeInfo.isAbstractType() && mayConcreteTypes.contains(concreteType)) { | ||
134 | return concreteType; | ||
135 | } | ||
136 | } | ||
137 | // We have already filtered out the para-consistent case in {@link #propagateMust(Set<PartialRelation>, | ||
138 | // Set<PartialRelation>}. | ||
139 | throw new AssertionError("No concrete type in %s".formatted(mayConcreteTypes)); | ||
140 | } | ||
9 | } | 141 | } |
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/TypeHierarchy.java index e97ce954..99069ab9 100644 --- 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/TypeHierarchy.java | |||
@@ -9,14 +9,16 @@ import tools.refinery.store.reasoning.representation.PartialRelation; | |||
9 | 9 | ||
10 | import java.util.*; | 10 | import java.util.*; |
11 | 11 | ||
12 | class TypeAnalyzer { | 12 | public class TypeHierarchy { |
13 | private final Set<PartialRelation> allTypes; | ||
13 | private final Map<PartialRelation, ExtendedTypeInfo> extendedTypeInfoMap; | 14 | private final Map<PartialRelation, ExtendedTypeInfo> extendedTypeInfoMap; |
14 | private final Map<PartialRelation, PartialRelation> replacements = new LinkedHashMap<>(); | 15 | private final Map<PartialRelation, PartialRelation> replacements = new LinkedHashMap<>(); |
15 | private final InferredType unknownType; | 16 | private final InferredType unknownType; |
16 | private final Map<PartialRelation, TypeAnalysisResult> analysisResults; | 17 | private final Map<PartialRelation, TypeAnalysisResult> preservedTypes; |
17 | 18 | ||
18 | public TypeAnalyzer(Map<PartialRelation, TypeInfo> typeInfoMap) { | 19 | TypeHierarchy(Map<PartialRelation, TypeInfo> typeInfoMap) { |
19 | int size = typeInfoMap.size(); | 20 | int size = typeInfoMap.size(); |
21 | allTypes = Collections.unmodifiableSet(new LinkedHashSet<>(typeInfoMap.keySet())); | ||
20 | extendedTypeInfoMap = new LinkedHashMap<>(size); | 22 | extendedTypeInfoMap = new LinkedHashMap<>(size); |
21 | var concreteTypes = new LinkedHashSet<PartialRelation>(); | 23 | var concreteTypes = new LinkedHashSet<PartialRelation>(); |
22 | int index = 0; | 24 | int index = 0; |
@@ -34,15 +36,39 @@ class TypeAnalyzer { | |||
34 | computeAllAndConcreteSubtypes(); | 36 | computeAllAndConcreteSubtypes(); |
35 | computeDirectSubtypes(); | 37 | computeDirectSubtypes(); |
36 | eliminateTrivialSupertypes(); | 38 | eliminateTrivialSupertypes(); |
37 | analysisResults = computeAnalysisResults(); | 39 | preservedTypes = computeAnalysisResults(); |
40 | } | ||
41 | |||
42 | public boolean isEmpty() { | ||
43 | return extendedTypeInfoMap.isEmpty(); | ||
38 | } | 44 | } |
39 | 45 | ||
40 | public InferredType getUnknownType() { | 46 | public InferredType getUnknownType() { |
41 | return unknownType; | 47 | return unknownType; |
42 | } | 48 | } |
43 | 49 | ||
44 | public Map<PartialRelation, TypeAnalysisResult> getAnalysisResults() { | 50 | public Set<PartialRelation> getAllTypes() { |
45 | return analysisResults; | 51 | return allTypes; |
52 | } | ||
53 | |||
54 | public Map<PartialRelation, TypeAnalysisResult> getPreservedTypes() { | ||
55 | return preservedTypes; | ||
56 | } | ||
57 | |||
58 | public Map<PartialRelation, PartialRelation> getEliminatedTypes() { | ||
59 | return Collections.unmodifiableMap(replacements); | ||
60 | } | ||
61 | |||
62 | public TypeAnalysisResult getAnalysisResult(PartialRelation type) { | ||
63 | var preservedResult = preservedTypes.get(type); | ||
64 | if (preservedResult != null) { | ||
65 | return preservedResult; | ||
66 | } | ||
67 | var eliminatedResult = replacements.get(type); | ||
68 | if (eliminatedResult != null) { | ||
69 | return preservedTypes.get(eliminatedResult); | ||
70 | } | ||
71 | throw new IllegalArgumentException("Unknown type: " + type); | ||
46 | } | 72 | } |
47 | 73 | ||
48 | private void computeAllSupertypes() { | 74 | private void computeAllSupertypes() { |
@@ -156,17 +182,13 @@ class TypeAnalyzer { | |||
156 | 182 | ||
157 | private Map<PartialRelation, TypeAnalysisResult> computeAnalysisResults() { | 183 | private Map<PartialRelation, TypeAnalysisResult> computeAnalysisResults() { |
158 | var allExtendedTypeInfoList = sortTypes(); | 184 | var allExtendedTypeInfoList = sortTypes(); |
159 | var results = new LinkedHashMap<PartialRelation, TypeAnalysisResult>( | 185 | var preservedResults = new LinkedHashMap<PartialRelation, TypeAnalysisResult>( |
160 | allExtendedTypeInfoList.size() + replacements.size()); | 186 | allExtendedTypeInfoList.size()); |
161 | for (var extendedTypeInfo : allExtendedTypeInfoList) { | 187 | for (var extendedTypeInfo : allExtendedTypeInfoList) { |
162 | var type = extendedTypeInfo.getType(); | 188 | var type = extendedTypeInfo.getType(); |
163 | results.put(type, new PreservedType(extendedTypeInfo, allExtendedTypeInfoList)); | 189 | preservedResults.put(type, new TypeAnalysisResult(extendedTypeInfo, allExtendedTypeInfoList)); |
164 | } | 190 | } |
165 | for (var entry : replacements.entrySet()) { | 191 | return Collections.unmodifiableMap(preservedResults); |
166 | var type = entry.getKey(); | ||
167 | results.put(type, new EliminatedType(entry.getValue())); | ||
168 | } | ||
169 | return Collections.unmodifiableMap(results); | ||
170 | } | 192 | } |
171 | 193 | ||
172 | private List<ExtendedTypeInfo> sortTypes() { | 194 | private List<ExtendedTypeInfo> sortTypes() { |
@@ -204,4 +226,8 @@ class TypeAnalyzer { | |||
204 | } | 226 | } |
205 | return Collections.unmodifiableList(sorted); | 227 | return Collections.unmodifiableList(sorted); |
206 | } | 228 | } |
229 | |||
230 | public static TypeHierarchyBuilder builder() { | ||
231 | return new TypeHierarchyBuilder(); | ||
232 | } | ||
207 | } | 233 | } |
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeHierarchyBuilder.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeHierarchyBuilder.java new file mode 100644 index 00000000..0fca4810 --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeHierarchyBuilder.java | |||
@@ -0,0 +1,62 @@ | |||
1 | /* | ||
2 | * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/> | ||
3 | * | ||
4 | * SPDX-License-Identifier: EPL-2.0 | ||
5 | */ | ||
6 | package tools.refinery.store.reasoning.translator.typehierarchy; | ||
7 | |||
8 | import tools.refinery.store.reasoning.representation.PartialRelation; | ||
9 | |||
10 | import java.util.Collection; | ||
11 | import java.util.LinkedHashMap; | ||
12 | import java.util.List; | ||
13 | import java.util.Map; | ||
14 | |||
15 | public class TypeHierarchyBuilder { | ||
16 | private final Map<PartialRelation, TypeInfo> typeInfoMap = new LinkedHashMap<>(); | ||
17 | |||
18 | public TypeHierarchyBuilder type(PartialRelation partialRelation, TypeInfo typeInfo) { | ||
19 | if (partialRelation.arity() != 1) { | ||
20 | throw new IllegalArgumentException("Only types of arity 1 are supported, hot %d instead" | ||
21 | .formatted(partialRelation.arity())); | ||
22 | } | ||
23 | var putResult = typeInfoMap.put(partialRelation, typeInfo); | ||
24 | if (putResult != null && !putResult.equals(typeInfo)) { | ||
25 | throw new IllegalArgumentException("Duplicate type info for partial relation: " + partialRelation); | ||
26 | } | ||
27 | return this; | ||
28 | } | ||
29 | |||
30 | public TypeHierarchyBuilder type(PartialRelation partialRelation, boolean abstractType, | ||
31 | PartialRelation... supertypes) { | ||
32 | return type(partialRelation, abstractType, List.of(supertypes)); | ||
33 | } | ||
34 | |||
35 | public TypeHierarchyBuilder type(PartialRelation partialRelation, boolean abstractType, | ||
36 | Collection<PartialRelation> supertypes) { | ||
37 | return type(partialRelation, new TypeInfo(supertypes, abstractType)); | ||
38 | } | ||
39 | |||
40 | public TypeHierarchyBuilder type(PartialRelation partialRelation, PartialRelation... supertypes) { | ||
41 | return type(partialRelation, List.of(supertypes)); | ||
42 | } | ||
43 | |||
44 | public TypeHierarchyBuilder type(PartialRelation partialRelation, Collection<PartialRelation> supertypes) { | ||
45 | return type(partialRelation, false, supertypes); | ||
46 | } | ||
47 | |||
48 | public TypeHierarchyBuilder types(Collection<Map.Entry<PartialRelation, TypeInfo>> entries) { | ||
49 | for (var entry : entries) { | ||
50 | type(entry.getKey(), entry.getValue()); | ||
51 | } | ||
52 | return this; | ||
53 | } | ||
54 | |||
55 | public TypeHierarchyBuilder types(Map<PartialRelation, TypeInfo> map) { | ||
56 | return types(map.entrySet()); | ||
57 | } | ||
58 | |||
59 | public TypeHierarchy build() { | ||
60 | return new TypeHierarchy(typeInfoMap); | ||
61 | } | ||
62 | } | ||
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeHierarchyInitializer.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeHierarchyInitializer.java new file mode 100644 index 00000000..6648a454 --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeHierarchyInitializer.java | |||
@@ -0,0 +1,57 @@ | |||
1 | /* | ||
2 | * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/> | ||
3 | * | ||
4 | * SPDX-License-Identifier: EPL-2.0 | ||
5 | */ | ||
6 | package tools.refinery.store.reasoning.translator.typehierarchy; | ||
7 | |||
8 | import tools.refinery.store.model.Model; | ||
9 | import tools.refinery.store.reasoning.refinement.PartialModelInitializer; | ||
10 | import tools.refinery.store.reasoning.representation.PartialRelation; | ||
11 | import tools.refinery.store.reasoning.seed.ModelSeed; | ||
12 | import tools.refinery.store.representation.Symbol; | ||
13 | import tools.refinery.store.representation.TruthValue; | ||
14 | import tools.refinery.store.tuple.Tuple; | ||
15 | |||
16 | import java.util.Arrays; | ||
17 | |||
18 | public class TypeHierarchyInitializer implements PartialModelInitializer { | ||
19 | private final TypeHierarchy typeHierarchy; | ||
20 | private final Symbol<InferredType> typeSymbol; | ||
21 | |||
22 | public TypeHierarchyInitializer(TypeHierarchy typeHierarchy, Symbol<InferredType> typeSymbol) { | ||
23 | this.typeHierarchy = typeHierarchy; | ||
24 | this.typeSymbol = typeSymbol; | ||
25 | } | ||
26 | |||
27 | @Override | ||
28 | public void initialize(Model model, ModelSeed modelSeed) { | ||
29 | var inferredTypes = new InferredType[modelSeed.getNodeCount()]; | ||
30 | Arrays.fill(inferredTypes, typeHierarchy.getUnknownType()); | ||
31 | for (var type : typeHierarchy.getAllTypes()) { | ||
32 | initializeType(type, inferredTypes, modelSeed); | ||
33 | } | ||
34 | var typeInterpretation = model.getInterpretation(typeSymbol); | ||
35 | for (int i = 0; i < inferredTypes.length; i++) { | ||
36 | typeInterpretation.put(Tuple.of(i), inferredTypes[i]); | ||
37 | } | ||
38 | } | ||
39 | |||
40 | private void initializeType(PartialRelation type, InferredType[] inferredTypes, ModelSeed modelSeed) { | ||
41 | var cursor = modelSeed.getCursor(type, TruthValue.UNKNOWN); | ||
42 | var analysisResult = typeHierarchy.getAnalysisResult(type); | ||
43 | while (cursor.move()) { | ||
44 | var i = cursor.getKey().get(0); | ||
45 | checkNodeId(inferredTypes, i); | ||
46 | var value = cursor.getValue(); | ||
47 | inferredTypes[i] = analysisResult.merge(inferredTypes[i], value); | ||
48 | } | ||
49 | } | ||
50 | |||
51 | private void checkNodeId(InferredType[] inferredTypes, int nodeId) { | ||
52 | if (nodeId < 0 || nodeId >= inferredTypes.length) { | ||
53 | throw new IllegalArgumentException("Expected node id %d to be lower than model size %d" | ||
54 | .formatted(nodeId, inferredTypes.length)); | ||
55 | } | ||
56 | } | ||
57 | } | ||
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeHierarchyTranslator.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeHierarchyTranslator.java new file mode 100644 index 00000000..6a45acd3 --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeHierarchyTranslator.java | |||
@@ -0,0 +1,81 @@ | |||
1 | /* | ||
2 | * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/> | ||
3 | * | ||
4 | * SPDX-License-Identifier: EPL-2.0 | ||
5 | */ | ||
6 | package tools.refinery.store.reasoning.translator.typehierarchy; | ||
7 | |||
8 | import tools.refinery.store.model.ModelStoreBuilder; | ||
9 | import tools.refinery.store.model.ModelStoreConfiguration; | ||
10 | import tools.refinery.store.query.dnf.Query; | ||
11 | import tools.refinery.store.reasoning.ReasoningBuilder; | ||
12 | import tools.refinery.store.reasoning.literal.PartialLiterals; | ||
13 | import tools.refinery.store.reasoning.representation.PartialRelation; | ||
14 | import tools.refinery.store.reasoning.translator.PartialRelationTranslator; | ||
15 | import tools.refinery.store.reasoning.translator.proxy.PartialRelationTranslatorProxy; | ||
16 | import tools.refinery.store.representation.Symbol; | ||
17 | |||
18 | public class TypeHierarchyTranslator implements ModelStoreConfiguration { | ||
19 | private final Symbol<InferredType> typeSymbol = Symbol.of("TYPE", 1, InferredType.class, InferredType.UNTYPED); | ||
20 | private final TypeHierarchy typeHierarchy; | ||
21 | |||
22 | public TypeHierarchyTranslator(TypeHierarchy typeHierarchy) { | ||
23 | this.typeHierarchy = typeHierarchy; | ||
24 | } | ||
25 | |||
26 | @Override | ||
27 | public void apply(ModelStoreBuilder storeBuilder) { | ||
28 | if (typeHierarchy.isEmpty()) { | ||
29 | return; | ||
30 | } | ||
31 | |||
32 | storeBuilder.symbol(typeSymbol); | ||
33 | |||
34 | for (var entry : typeHierarchy.getPreservedTypes().entrySet()) { | ||
35 | storeBuilder.with(createPreservedTypeTranslator(entry.getKey(), entry.getValue())); | ||
36 | } | ||
37 | |||
38 | for (var entry : typeHierarchy.getEliminatedTypes().entrySet()) { | ||
39 | storeBuilder.with(createEliminatedTypeTranslator(entry.getKey(), entry.getValue())); | ||
40 | } | ||
41 | |||
42 | var reasoningBuilder = storeBuilder.getAdapter(ReasoningBuilder.class); | ||
43 | reasoningBuilder.initializer(new TypeHierarchyInitializer(typeHierarchy, typeSymbol)); | ||
44 | } | ||
45 | |||
46 | private ModelStoreConfiguration createPreservedTypeTranslator(PartialRelation type, TypeAnalysisResult result) { | ||
47 | var may = Query.of(type.name() + "#may", (builder, p1) -> { | ||
48 | if (result.isAbstractType()) { | ||
49 | for (var subtype : result.getDirectSubtypes()) { | ||
50 | builder.clause(PartialLiterals.may(subtype.call(p1))); | ||
51 | } | ||
52 | } else { | ||
53 | builder.clause(new MayTypeView(typeSymbol, type).call(p1)); | ||
54 | } | ||
55 | }); | ||
56 | |||
57 | var must = Query.of(type.name() + "#must", (builder, p1) -> builder.clause( | ||
58 | new MustTypeView(typeSymbol, type).call(p1) | ||
59 | )); | ||
60 | |||
61 | var candidate = Query.of(type.name() + "#candidate", (builder, p1) -> { | ||
62 | if (!result.isAbstractType()) { | ||
63 | builder.clause(new CandidateTypeView(typeSymbol, type).call(p1)); | ||
64 | } | ||
65 | for (var subtype : result.getDirectSubtypes()) { | ||
66 | builder.clause(PartialLiterals.candidateMust(subtype.call(p1))); | ||
67 | } | ||
68 | }); | ||
69 | |||
70 | return PartialRelationTranslator.of(type) | ||
71 | .may(may) | ||
72 | .must(must) | ||
73 | .candidate(candidate) | ||
74 | .refiner(InferredTypeRefiner.of(typeSymbol, result)); | ||
75 | } | ||
76 | |||
77 | private ModelStoreConfiguration createEliminatedTypeTranslator( | ||
78 | PartialRelation type, PartialRelation replacement) { | ||
79 | return new PartialRelationTranslatorProxy(type, replacement, true); | ||
80 | } | ||
81 | } | ||
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 index 9f897e46..68ed4089 100644 --- 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 | |||
@@ -10,42 +10,4 @@ import tools.refinery.store.reasoning.representation.PartialRelation; | |||
10 | import java.util.*; | 10 | import java.util.*; |
11 | 11 | ||
12 | public record TypeInfo(Collection<PartialRelation> supertypes, boolean abstractType) { | 12 | public record TypeInfo(Collection<PartialRelation> supertypes, boolean abstractType) { |
13 | public static Builder builder() { | ||
14 | return new Builder(); | ||
15 | } | ||
16 | |||
17 | public static class Builder { | ||
18 | private final Set<PartialRelation> supertypes = new LinkedHashSet<>(); | ||
19 | private boolean abstractType; | ||
20 | |||
21 | private Builder() { | ||
22 | } | ||
23 | |||
24 | public Builder supertypes(Collection<PartialRelation> supertypes) { | ||
25 | this.supertypes.addAll(supertypes); | ||
26 | return this; | ||
27 | } | ||
28 | |||
29 | public Builder supertypes(PartialRelation... supertypes) { | ||
30 | return supertypes(List.of(supertypes)); | ||
31 | } | ||
32 | |||
33 | public Builder supertype(PartialRelation supertype) { | ||
34 | supertypes.add(supertype); | ||
35 | return this; | ||
36 | } | ||
37 | |||
38 | public Builder abstractType(boolean abstractType) { | ||
39 | this.abstractType = abstractType; | ||
40 | return this; | ||
41 | } | ||
42 | |||
43 | public Builder abstractType() { | ||
44 | return abstractType(true); | ||
45 | } | ||
46 | |||
47 | public TypeInfo build() { | ||
48 | return new TypeInfo(Collections.unmodifiableSet(supertypes), abstractType); | ||
49 | } | ||
50 | } | ||
51 | } | 13 | } |
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/TypeAnalysisExampleHierarchyTest.java index b4ba16fc..d9a5477e 100644 --- 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/TypeAnalysisExampleHierarchyTest.java | |||
@@ -11,14 +11,13 @@ import org.junit.jupiter.api.Test; | |||
11 | import tools.refinery.store.reasoning.representation.PartialRelation; | 11 | import tools.refinery.store.reasoning.representation.PartialRelation; |
12 | import tools.refinery.store.representation.TruthValue; | 12 | import tools.refinery.store.representation.TruthValue; |
13 | 13 | ||
14 | import java.util.LinkedHashMap; | ||
15 | import java.util.Set; | 14 | import java.util.Set; |
16 | 15 | ||
17 | import static org.hamcrest.MatcherAssert.assertThat; | 16 | import static org.hamcrest.MatcherAssert.assertThat; |
18 | import static org.hamcrest.Matchers.is; | 17 | import static org.hamcrest.Matchers.is; |
19 | import static org.junit.jupiter.api.Assertions.assertAll; | 18 | import static org.junit.jupiter.api.Assertions.assertAll; |
20 | 19 | ||
21 | class TypeAnalyzerExampleHierarchyTest { | 20 | class TypeAnalysisExampleHierarchyTest { |
22 | private final PartialRelation a1 = new PartialRelation("A1", 1); | 21 | private final PartialRelation a1 = new PartialRelation("A1", 1); |
23 | private final PartialRelation a2 = new PartialRelation("A2", 1); | 22 | private final PartialRelation a2 = new PartialRelation("A2", 1); |
24 | private final PartialRelation a3 = new PartialRelation("A3", 1); | 23 | private final PartialRelation a3 = new PartialRelation("A3", 1); |
@@ -29,23 +28,23 @@ class TypeAnalyzerExampleHierarchyTest { | |||
29 | private final PartialRelation c3 = new PartialRelation("C3", 1); | 28 | private final PartialRelation c3 = new PartialRelation("C3", 1); |
30 | private final PartialRelation c4 = new PartialRelation("C4", 1); | 29 | private final PartialRelation c4 = new PartialRelation("C4", 1); |
31 | 30 | ||
32 | private TypeAnalyzer sut; | 31 | private TypeHierarchy sut; |
33 | private TypeAnalyzerTester tester; | 32 | private TypeHierarchyTester tester; |
34 | 33 | ||
35 | @BeforeEach | 34 | @BeforeEach |
36 | void beforeEach() { | 35 | void beforeEach() { |
37 | var typeInfoMap = new LinkedHashMap<PartialRelation, TypeInfo>(); | 36 | sut = TypeHierarchy.builder() |
38 | typeInfoMap.put(a1, TypeInfo.builder().abstractType().build()); | 37 | .type(a1, true) |
39 | typeInfoMap.put(a2, TypeInfo.builder().abstractType().build()); | 38 | .type(a2, true) |
40 | typeInfoMap.put(a3, TypeInfo.builder().abstractType().build()); | 39 | .type(a3, true) |
41 | typeInfoMap.put(a4, TypeInfo.builder().abstractType().build()); | 40 | .type(a4, true) |
42 | typeInfoMap.put(a5, TypeInfo.builder().abstractType().build()); | 41 | .type(a5, true) |
43 | typeInfoMap.put(c1, TypeInfo.builder().supertypes(a1, a4).build()); | 42 | .type(c1, a1, a4) |
44 | typeInfoMap.put(c2, TypeInfo.builder().supertypes(a1, a2, a3, a4).build()); | 43 | .type(c2, a1, a2, a3, a4) |
45 | typeInfoMap.put(c3, TypeInfo.builder().supertype(a3).build()); | 44 | .type(c3, a3) |
46 | typeInfoMap.put(c4, TypeInfo.builder().supertype(a4).build()); | 45 | .type(c4, a4) |
47 | sut = new TypeAnalyzer(typeInfoMap); | 46 | .build(); |
48 | tester = new TypeAnalyzerTester(sut); | 47 | tester = new TypeHierarchyTester(sut); |
49 | } | 48 | } |
50 | 49 | ||
51 | @Test | 50 | @Test |
diff --git a/subprojects/store-reasoning/src/test/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeHierarchyPartialModelTest.java b/subprojects/store-reasoning/src/test/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeHierarchyPartialModelTest.java new file mode 100644 index 00000000..cd9df19a --- /dev/null +++ b/subprojects/store-reasoning/src/test/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeHierarchyPartialModelTest.java | |||
@@ -0,0 +1,186 @@ | |||
1 | /* | ||
2 | * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/> | ||
3 | * | ||
4 | * SPDX-License-Identifier: EPL-2.0 | ||
5 | */ | ||
6 | package tools.refinery.store.reasoning.translator.typehierarchy; | ||
7 | |||
8 | import org.junit.jupiter.api.BeforeEach; | ||
9 | import org.junit.jupiter.api.Test; | ||
10 | import tools.refinery.store.model.Model; | ||
11 | import tools.refinery.store.model.ModelStore; | ||
12 | import tools.refinery.store.query.ModelQueryAdapter; | ||
13 | import tools.refinery.store.query.viatra.ViatraModelQueryAdapter; | ||
14 | import tools.refinery.store.reasoning.ReasoningAdapter; | ||
15 | import tools.refinery.store.reasoning.ReasoningStoreAdapter; | ||
16 | import tools.refinery.store.reasoning.literal.Concreteness; | ||
17 | import tools.refinery.store.reasoning.representation.PartialRelation; | ||
18 | import tools.refinery.store.reasoning.seed.ModelSeed; | ||
19 | import tools.refinery.store.representation.TruthValue; | ||
20 | import tools.refinery.store.tuple.Tuple; | ||
21 | |||
22 | import static org.hamcrest.MatcherAssert.assertThat; | ||
23 | import static org.hamcrest.Matchers.is; | ||
24 | |||
25 | class TypeHierarchyPartialModelTest { | ||
26 | private final PartialRelation person = new PartialRelation("Person", 1); | ||
27 | private final PartialRelation member = new PartialRelation("Member", 1); | ||
28 | private final PartialRelation student = new PartialRelation("Student", 1); | ||
29 | private final PartialRelation teacher = new PartialRelation("Teacher", 1); | ||
30 | private final PartialRelation pet = new PartialRelation("Pet", 1); | ||
31 | |||
32 | private Model model; | ||
33 | |||
34 | @BeforeEach | ||
35 | void beforeEach() { | ||
36 | var typeHierarchy = TypeHierarchy.builder() | ||
37 | .type(person, true) | ||
38 | .type(member, true, person) | ||
39 | .type(student, member) | ||
40 | .type(teacher, member) | ||
41 | .type(pet) | ||
42 | .build(); | ||
43 | |||
44 | var store = ModelStore.builder() | ||
45 | .with(ViatraModelQueryAdapter.builder()) | ||
46 | .with(ReasoningAdapter.builder()) | ||
47 | .with(new TypeHierarchyTranslator(typeHierarchy)) | ||
48 | .build(); | ||
49 | |||
50 | var seed = ModelSeed.builder(4) | ||
51 | .seed(person, builder -> builder | ||
52 | .reducedValue(TruthValue.UNKNOWN) | ||
53 | .put(Tuple.of(3), TruthValue.FALSE)) | ||
54 | .seed(member, builder -> builder | ||
55 | .reducedValue(TruthValue.UNKNOWN) | ||
56 | .put(Tuple.of(1), TruthValue.TRUE) | ||
57 | .put(Tuple.of(2), TruthValue.TRUE)) | ||
58 | .seed(student, builder -> builder | ||
59 | .reducedValue(TruthValue.UNKNOWN) | ||
60 | .put(Tuple.of(0), TruthValue.TRUE) | ||
61 | .put(Tuple.of(2), TruthValue.FALSE)) | ||
62 | .seed(teacher, builder -> builder.reducedValue(TruthValue.UNKNOWN)) | ||
63 | .seed(pet, builder -> builder.reducedValue(TruthValue.UNKNOWN)) | ||
64 | .build(); | ||
65 | model = store.getAdapter(ReasoningStoreAdapter.class).createInitialModel(seed); | ||
66 | } | ||
67 | |||
68 | @Test | ||
69 | void initialModelTest() { | ||
70 | var reasoningAdapter = model.getAdapter(ReasoningAdapter.class); | ||
71 | |||
72 | var personInterpretation = reasoningAdapter.getPartialInterpretation(Concreteness.PARTIAL, person); | ||
73 | assertThat(personInterpretation.get(Tuple.of(0)), is(TruthValue.TRUE)); | ||
74 | assertThat(personInterpretation.get(Tuple.of(1)), is(TruthValue.TRUE)); | ||
75 | assertThat(personInterpretation.get(Tuple.of(2)), is(TruthValue.TRUE)); | ||
76 | assertThat(personInterpretation.get(Tuple.of(3)), is(TruthValue.FALSE)); | ||
77 | |||
78 | var memberInterpretation = reasoningAdapter.getPartialInterpretation(Concreteness.PARTIAL, member); | ||
79 | assertThat(memberInterpretation.get(Tuple.of(0)), is(TruthValue.TRUE)); | ||
80 | assertThat(memberInterpretation.get(Tuple.of(1)), is(TruthValue.TRUE)); | ||
81 | assertThat(memberInterpretation.get(Tuple.of(2)), is(TruthValue.TRUE)); | ||
82 | assertThat(memberInterpretation.get(Tuple.of(3)), is(TruthValue.FALSE)); | ||
83 | |||
84 | var studentInterpretation = reasoningAdapter.getPartialInterpretation(Concreteness.PARTIAL, student); | ||
85 | assertThat(studentInterpretation.get(Tuple.of(0)), is(TruthValue.TRUE)); | ||
86 | assertThat(studentInterpretation.get(Tuple.of(1)), is(TruthValue.UNKNOWN)); | ||
87 | assertThat(studentInterpretation.get(Tuple.of(2)), is(TruthValue.FALSE)); | ||
88 | assertThat(studentInterpretation.get(Tuple.of(3)), is(TruthValue.FALSE)); | ||
89 | |||
90 | var teacherInterpretation = reasoningAdapter.getPartialInterpretation(Concreteness.PARTIAL, teacher); | ||
91 | assertThat(teacherInterpretation.get(Tuple.of(0)), is(TruthValue.FALSE)); | ||
92 | assertThat(teacherInterpretation.get(Tuple.of(1)), is(TruthValue.UNKNOWN)); | ||
93 | assertThat(teacherInterpretation.get(Tuple.of(2)), is(TruthValue.TRUE)); | ||
94 | assertThat(teacherInterpretation.get(Tuple.of(3)), is(TruthValue.FALSE)); | ||
95 | |||
96 | var petInterpretation = reasoningAdapter.getPartialInterpretation(Concreteness.PARTIAL, pet); | ||
97 | assertThat(petInterpretation.get(Tuple.of(0)), is(TruthValue.FALSE)); | ||
98 | assertThat(petInterpretation.get(Tuple.of(1)), is(TruthValue.FALSE)); | ||
99 | assertThat(petInterpretation.get(Tuple.of(2)), is(TruthValue.FALSE)); | ||
100 | assertThat(petInterpretation.get(Tuple.of(3)), is(TruthValue.UNKNOWN)); | ||
101 | } | ||
102 | |||
103 | @Test | ||
104 | void initialModelCandidateTest() { | ||
105 | var reasoningAdapter = model.getAdapter(ReasoningAdapter.class); | ||
106 | |||
107 | var personCandidateInterpretation = reasoningAdapter.getPartialInterpretation(Concreteness.CANDIDATE, person); | ||
108 | assertThat(personCandidateInterpretation.get(Tuple.of(0)), is(TruthValue.TRUE)); | ||
109 | assertThat(personCandidateInterpretation.get(Tuple.of(1)), is(TruthValue.TRUE)); | ||
110 | assertThat(personCandidateInterpretation.get(Tuple.of(2)), is(TruthValue.TRUE)); | ||
111 | assertThat(personCandidateInterpretation.get(Tuple.of(3)), is(TruthValue.FALSE)); | ||
112 | |||
113 | var memberCandidateInterpretation = reasoningAdapter.getPartialInterpretation(Concreteness.CANDIDATE, member); | ||
114 | assertThat(memberCandidateInterpretation.get(Tuple.of(0)), is(TruthValue.TRUE)); | ||
115 | assertThat(memberCandidateInterpretation.get(Tuple.of(1)), is(TruthValue.TRUE)); | ||
116 | assertThat(memberCandidateInterpretation.get(Tuple.of(2)), is(TruthValue.TRUE)); | ||
117 | assertThat(memberCandidateInterpretation.get(Tuple.of(3)), is(TruthValue.FALSE)); | ||
118 | |||
119 | var studentCandidateInterpretation = reasoningAdapter.getPartialInterpretation(Concreteness.CANDIDATE, student); | ||
120 | assertThat(studentCandidateInterpretation.get(Tuple.of(0)), is(TruthValue.TRUE)); | ||
121 | assertThat(studentCandidateInterpretation.get(Tuple.of(1)), is(TruthValue.TRUE)); | ||
122 | assertThat(studentCandidateInterpretation.get(Tuple.of(2)), is(TruthValue.FALSE)); | ||
123 | assertThat(studentCandidateInterpretation.get(Tuple.of(3)), is(TruthValue.FALSE)); | ||
124 | |||
125 | var teacherCandidateInterpretation = reasoningAdapter.getPartialInterpretation(Concreteness.CANDIDATE, teacher); | ||
126 | assertThat(teacherCandidateInterpretation.get(Tuple.of(0)), is(TruthValue.FALSE)); | ||
127 | assertThat(teacherCandidateInterpretation.get(Tuple.of(1)), is(TruthValue.FALSE)); | ||
128 | assertThat(teacherCandidateInterpretation.get(Tuple.of(2)), is(TruthValue.TRUE)); | ||
129 | assertThat(teacherCandidateInterpretation.get(Tuple.of(3)), is(TruthValue.FALSE)); | ||
130 | |||
131 | var petCandidateInterpretation = reasoningAdapter.getPartialInterpretation(Concreteness.CANDIDATE, pet); | ||
132 | assertThat(petCandidateInterpretation.get(Tuple.of(0)), is(TruthValue.FALSE)); | ||
133 | assertThat(petCandidateInterpretation.get(Tuple.of(1)), is(TruthValue.FALSE)); | ||
134 | assertThat(petCandidateInterpretation.get(Tuple.of(2)), is(TruthValue.FALSE)); | ||
135 | assertThat(petCandidateInterpretation.get(Tuple.of(3)), is(TruthValue.FALSE)); | ||
136 | } | ||
137 | |||
138 | @Test | ||
139 | void refinedModelTest() { | ||
140 | var reasoningAdapter = model.getAdapter(ReasoningAdapter.class); | ||
141 | var studentRefiner = reasoningAdapter.getRefiner(student); | ||
142 | studentRefiner.merge(Tuple.of(1), TruthValue.FALSE); | ||
143 | studentRefiner.merge(Tuple.of(3), TruthValue.TRUE); | ||
144 | model.getAdapter(ModelQueryAdapter.class).flushChanges(); | ||
145 | |||
146 | var personInterpretation = reasoningAdapter.getPartialInterpretation(Concreteness.PARTIAL, person); | ||
147 | assertThat(personInterpretation.get(Tuple.of(1)), is(TruthValue.TRUE)); | ||
148 | assertThat(personInterpretation.get(Tuple.of(3)), is(TruthValue.ERROR)); | ||
149 | |||
150 | var personCandidateInterpretation = reasoningAdapter.getPartialInterpretation(Concreteness.CANDIDATE, person); | ||
151 | assertThat(personCandidateInterpretation.get(Tuple.of(1)), is(TruthValue.TRUE)); | ||
152 | assertThat(personCandidateInterpretation.get(Tuple.of(3)), is(TruthValue.FALSE)); | ||
153 | |||
154 | var memberInterpretation = reasoningAdapter.getPartialInterpretation(Concreteness.PARTIAL, member); | ||
155 | assertThat(memberInterpretation.get(Tuple.of(1)), is(TruthValue.TRUE)); | ||
156 | assertThat(memberInterpretation.get(Tuple.of(3)), is(TruthValue.ERROR)); | ||
157 | |||
158 | var memberCandidateInterpretation = reasoningAdapter.getPartialInterpretation(Concreteness.CANDIDATE, member); | ||
159 | assertThat(memberCandidateInterpretation.get(Tuple.of(1)), is(TruthValue.TRUE)); | ||
160 | assertThat(memberCandidateInterpretation.get(Tuple.of(3)), is(TruthValue.FALSE)); | ||
161 | |||
162 | var studentInterpretation = reasoningAdapter.getPartialInterpretation(Concreteness.PARTIAL, student); | ||
163 | assertThat(studentInterpretation.get(Tuple.of(1)), is(TruthValue.FALSE)); | ||
164 | assertThat(studentInterpretation.get(Tuple.of(3)), is(TruthValue.ERROR)); | ||
165 | |||
166 | var studentCandidateInterpretation = reasoningAdapter.getPartialInterpretation(Concreteness.CANDIDATE, student); | ||
167 | assertThat(studentCandidateInterpretation.get(Tuple.of(1)), is(TruthValue.FALSE)); | ||
168 | assertThat(studentCandidateInterpretation.get(Tuple.of(3)), is(TruthValue.FALSE)); | ||
169 | |||
170 | var teacherInterpretation = reasoningAdapter.getPartialInterpretation(Concreteness.PARTIAL, teacher); | ||
171 | assertThat(teacherInterpretation.get(Tuple.of(1)), is(TruthValue.TRUE)); | ||
172 | assertThat(teacherInterpretation.get(Tuple.of(3)), is(TruthValue.FALSE)); | ||
173 | |||
174 | var teacherCandidateInterpretation = reasoningAdapter.getPartialInterpretation(Concreteness.CANDIDATE, teacher); | ||
175 | assertThat(teacherCandidateInterpretation.get(Tuple.of(1)), is(TruthValue.TRUE)); | ||
176 | assertThat(teacherCandidateInterpretation.get(Tuple.of(3)), is(TruthValue.FALSE)); | ||
177 | |||
178 | var petInterpretation = reasoningAdapter.getPartialInterpretation(Concreteness.PARTIAL, pet); | ||
179 | assertThat(petInterpretation.get(Tuple.of(1)), is(TruthValue.FALSE)); | ||
180 | assertThat(petInterpretation.get(Tuple.of(3)), is(TruthValue.FALSE)); | ||
181 | |||
182 | var petCandidateInterpretation = reasoningAdapter.getPartialInterpretation(Concreteness.CANDIDATE, pet); | ||
183 | assertThat(petCandidateInterpretation.get(Tuple.of(1)), is(TruthValue.FALSE)); | ||
184 | assertThat(petCandidateInterpretation.get(Tuple.of(3)), is(TruthValue.FALSE)); | ||
185 | } | ||
186 | } | ||
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/TypeHierarchyTest.java index 315f9672..1f922a79 100644 --- 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/TypeHierarchyTest.java | |||
@@ -10,27 +10,25 @@ import org.junit.jupiter.api.Test; | |||
10 | import tools.refinery.store.reasoning.representation.PartialRelation; | 10 | import tools.refinery.store.reasoning.representation.PartialRelation; |
11 | import tools.refinery.store.representation.TruthValue; | 11 | import tools.refinery.store.representation.TruthValue; |
12 | 12 | ||
13 | import java.util.LinkedHashMap; | ||
14 | import java.util.Set; | 13 | import java.util.Set; |
15 | 14 | ||
16 | import static org.hamcrest.MatcherAssert.assertThat; | 15 | import static org.hamcrest.MatcherAssert.assertThat; |
17 | import static org.hamcrest.Matchers.is; | ||
18 | import static org.junit.jupiter.api.Assertions.assertAll; | 16 | import static org.junit.jupiter.api.Assertions.assertAll; |
19 | import static org.junit.jupiter.api.Assertions.assertThrows; | 17 | import static org.junit.jupiter.api.Assertions.assertThrows; |
20 | 18 | ||
21 | class TypeAnalyzerTest { | 19 | class TypeHierarchyTest { |
22 | @Test | 20 | @Test |
23 | void directSupertypesTest() { | 21 | void directSupertypesTest() { |
24 | var c1 = new PartialRelation("C1", 1); | 22 | var c1 = new PartialRelation("C1", 1); |
25 | var c2 = new PartialRelation("C2", 1); | 23 | var c2 = new PartialRelation("C2", 1); |
26 | var c3 = new PartialRelation("C3", 1); | 24 | var c3 = new PartialRelation("C3", 1); |
27 | var typeInfoMap = new LinkedHashMap<PartialRelation, TypeInfo>(); | ||
28 | typeInfoMap.put(c1, TypeInfo.builder().supertypes(c2, c3).build()); | ||
29 | typeInfoMap.put(c2, TypeInfo.builder().supertype(c3).build()); | ||
30 | typeInfoMap.put(c3, TypeInfo.builder().build()); | ||
31 | 25 | ||
32 | var sut = new TypeAnalyzer(typeInfoMap); | 26 | var sut = TypeHierarchy.builder() |
33 | var tester = new TypeAnalyzerTester(sut); | 27 | .type(c1, c2, c3) |
28 | .type(c2, c3) | ||
29 | .type(c3) | ||
30 | .build(); | ||
31 | var tester = new TypeHierarchyTester(sut); | ||
34 | 32 | ||
35 | assertAll( | 33 | assertAll( |
36 | () -> tester.assertConcreteType(c1), | 34 | () -> tester.assertConcreteType(c1), |
@@ -48,17 +46,17 @@ class TypeAnalyzerTest { | |||
48 | var a21 = new PartialRelation("A21", 1); | 46 | var a21 = new PartialRelation("A21", 1); |
49 | var a22 = new PartialRelation("A22", 1); | 47 | var a22 = new PartialRelation("A22", 1); |
50 | var a3 = new PartialRelation("A3", 1); | 48 | var a3 = new PartialRelation("A3", 1); |
51 | var typeInfoMap = new LinkedHashMap<PartialRelation, TypeInfo>(); | 49 | |
52 | typeInfoMap.put(a3, TypeInfo.builder().abstractType().build()); | 50 | var sut = TypeHierarchy.builder() |
53 | typeInfoMap.put(a21, TypeInfo.builder().abstractType().supertype(a3).build()); | 51 | .type(a3, true) |
54 | typeInfoMap.put(a22, TypeInfo.builder().abstractType().supertype(a3).build()); | 52 | .type(a21, true, a3) |
55 | typeInfoMap.put(a11, TypeInfo.builder().abstractType().supertypes(a21, a22).build()); | 53 | .type(a22, true, a3) |
56 | typeInfoMap.put(a12, TypeInfo.builder().abstractType().supertypes(a21, a22).build()); | 54 | .type(a11, true, a21, a22) |
57 | typeInfoMap.put(c1, TypeInfo.builder().supertypes(a11, a12).build()); | 55 | .type(a12, true, a21, a22) |
58 | typeInfoMap.put(c2, TypeInfo.builder().supertype(a3).build()); | 56 | .type(c1, a11, a12) |
59 | 57 | .type(c2, a3) | |
60 | var sut = new TypeAnalyzer(typeInfoMap); | 58 | .build(); |
61 | var tester = new TypeAnalyzerTester(sut); | 59 | var tester = new TypeHierarchyTester(sut); |
62 | 60 | ||
63 | assertAll( | 61 | assertAll( |
64 | () -> tester.assertConcreteType(c1), | 62 | () -> tester.assertConcreteType(c1), |
@@ -80,17 +78,17 @@ class TypeAnalyzerTest { | |||
80 | var a21 = new PartialRelation("A21", 1); | 78 | var a21 = new PartialRelation("A21", 1); |
81 | var a22 = new PartialRelation("A22", 1); | 79 | var a22 = new PartialRelation("A22", 1); |
82 | var a3 = new PartialRelation("A3", 1); | 80 | var a3 = new PartialRelation("A3", 1); |
83 | var typeInfoMap = new LinkedHashMap<PartialRelation, TypeInfo>(); | 81 | |
84 | typeInfoMap.put(c1, TypeInfo.builder().supertypes(a11, a12).build()); | 82 | var sut = TypeHierarchy.builder() |
85 | typeInfoMap.put(c2, TypeInfo.builder().supertype(a3).build()); | 83 | .type(c1, a11, a12) |
86 | typeInfoMap.put(a11, TypeInfo.builder().abstractType().supertypes(a21, a22).build()); | 84 | .type(c2, a3) |
87 | typeInfoMap.put(a12, TypeInfo.builder().abstractType().supertypes(a21, a22).build()); | 85 | .type(a11, true, a21, a22) |
88 | typeInfoMap.put(a21, TypeInfo.builder().abstractType().supertype(a3).build()); | 86 | .type(a12, true, a21, a22) |
89 | typeInfoMap.put(a22, TypeInfo.builder().abstractType().supertype(a3).build()); | 87 | .type(a21, true, a3) |
90 | typeInfoMap.put(a3, TypeInfo.builder().abstractType().build()); | 88 | .type(a22, true, a3) |
91 | 89 | .type(a3, true) | |
92 | var sut = new TypeAnalyzer(typeInfoMap); | 90 | .build(); |
93 | var tester = new TypeAnalyzerTester(sut); | 91 | var tester = new TypeHierarchyTester(sut); |
94 | 92 | ||
95 | assertAll( | 93 | assertAll( |
96 | () -> tester.assertConcreteType(c1), | 94 | () -> tester.assertConcreteType(c1), |
@@ -109,14 +107,14 @@ class TypeAnalyzerTest { | |||
109 | var a1 = new PartialRelation("A1", 1); | 107 | var a1 = new PartialRelation("A1", 1); |
110 | var c2 = new PartialRelation("C2", 1); | 108 | var c2 = new PartialRelation("C2", 1); |
111 | var a2 = new PartialRelation("A2", 1); | 109 | var a2 = new PartialRelation("A2", 1); |
112 | var typeInfoMap = new LinkedHashMap<PartialRelation, TypeInfo>(); | ||
113 | typeInfoMap.put(c1, TypeInfo.builder().supertype(a1).build()); | ||
114 | typeInfoMap.put(a1, TypeInfo.builder().abstractType().supertype(c2).build()); | ||
115 | typeInfoMap.put(c2, TypeInfo.builder().supertype(a2).build()); | ||
116 | typeInfoMap.put(a2, TypeInfo.builder().abstractType().build()); | ||
117 | 110 | ||
118 | var sut = new TypeAnalyzer(typeInfoMap); | 111 | var sut = TypeHierarchy.builder() |
119 | var tester = new TypeAnalyzerTester(sut); | 112 | .type(c1, a1) |
113 | .type(a1, true, c2) | ||
114 | .type(c2, a2) | ||
115 | .type(a2, true) | ||
116 | .build(); | ||
117 | var tester = new TypeHierarchyTester(sut); | ||
120 | 118 | ||
121 | assertAll( | 119 | assertAll( |
122 | () -> tester.assertConcreteType(c1), | 120 | () -> tester.assertConcreteType(c1), |
@@ -131,13 +129,13 @@ class TypeAnalyzerTest { | |||
131 | var c1 = new PartialRelation("C1", 1); | 129 | var c1 = new PartialRelation("C1", 1); |
132 | var c2 = new PartialRelation("C2", 1); | 130 | var c2 = new PartialRelation("C2", 1); |
133 | var c3 = new PartialRelation("C3", 1); | 131 | var c3 = new PartialRelation("C3", 1); |
134 | var typeInfoMap = new LinkedHashMap<PartialRelation, TypeInfo>(); | ||
135 | typeInfoMap.put(c1, TypeInfo.builder().supertype(c3).build()); | ||
136 | typeInfoMap.put(c2, TypeInfo.builder().supertype(c3).build()); | ||
137 | typeInfoMap.put(c3, TypeInfo.builder().build()); | ||
138 | 132 | ||
139 | var sut = new TypeAnalyzer(typeInfoMap); | 133 | var sut = TypeHierarchy.builder() |
140 | var tester = new TypeAnalyzerTester(sut); | 134 | .type(c1, c3) |
135 | .type(c2, c3) | ||
136 | .type(c3) | ||
137 | .build(); | ||
138 | var tester = new TypeHierarchyTester(sut); | ||
141 | var c3Result = tester.getPreservedType(c3); | 139 | var c3Result = tester.getPreservedType(c3); |
142 | 140 | ||
143 | var expected = new InferredType(Set.of(c3), Set.of(c1, c2, c3), c3); | 141 | var expected = new InferredType(Set.of(c3), Set.of(c1, c2, c3), c3); |
@@ -154,15 +152,15 @@ class TypeAnalyzerTest { | |||
154 | var c2 = new PartialRelation("C2", 1); | 152 | var c2 = new PartialRelation("C2", 1); |
155 | var c3 = new PartialRelation("C3", 1); | 153 | var c3 = new PartialRelation("C3", 1); |
156 | var c4 = new PartialRelation("C4", 1); | 154 | var c4 = new PartialRelation("C4", 1); |
157 | var typeInfoMap = new LinkedHashMap<PartialRelation, TypeInfo>(); | 155 | |
158 | typeInfoMap.put(c1, TypeInfo.builder().supertype(a1).build()); | 156 | var sut = TypeHierarchy.builder() |
159 | typeInfoMap.put(c2, TypeInfo.builder().supertype(a1).build()); | 157 | .type(c1, a1) |
160 | typeInfoMap.put(c3, TypeInfo.builder().supertype(a1).build()); | 158 | .type(c2, a1) |
161 | typeInfoMap.put(c4, TypeInfo.builder().supertype(c3).build()); | 159 | .type(c3, a1) |
162 | typeInfoMap.put(a1, TypeInfo.builder().abstractType().build()); | 160 | .type(c4, c3) |
163 | 161 | .type(a1, true) | |
164 | var sut = new TypeAnalyzer(typeInfoMap); | 162 | .build(); |
165 | var tester = new TypeAnalyzerTester(sut); | 163 | var tester = new TypeHierarchyTester(sut); |
166 | var c1Result = tester.getPreservedType(c1); | 164 | var c1Result = tester.getPreservedType(c1); |
167 | var a1Result = tester.getPreservedType(a1); | 165 | var a1Result = tester.getPreservedType(a1); |
168 | 166 | ||
@@ -177,15 +175,15 @@ class TypeAnalyzerTest { | |||
177 | var c2 = new PartialRelation("C2", 1); | 175 | var c2 = new PartialRelation("C2", 1); |
178 | var c3 = new PartialRelation("C3", 1); | 176 | var c3 = new PartialRelation("C3", 1); |
179 | var c4 = new PartialRelation("C4", 1); | 177 | var c4 = new PartialRelation("C4", 1); |
180 | var typeInfoMap = new LinkedHashMap<PartialRelation, TypeInfo>(); | 178 | |
181 | typeInfoMap.put(c4, TypeInfo.builder().supertype(c3).build()); | 179 | var sut = TypeHierarchy.builder() |
182 | typeInfoMap.put(c3, TypeInfo.builder().supertype(a1).build()); | 180 | .type(c4, c3) |
183 | typeInfoMap.put(c2, TypeInfo.builder().supertype(a1).build()); | 181 | .type(c3, a1) |
184 | typeInfoMap.put(c1, TypeInfo.builder().supertype(a1).build()); | 182 | .type(c2, a1) |
185 | typeInfoMap.put(a1, TypeInfo.builder().abstractType().build()); | 183 | .type(c1, a1) |
186 | 184 | .type(a1, true) | |
187 | var sut = new TypeAnalyzer(typeInfoMap); | 185 | .build(); |
188 | var tester = new TypeAnalyzerTester(sut); | 186 | var tester = new TypeHierarchyTester(sut); |
189 | var c1Result = tester.getPreservedType(c1); | 187 | var c1Result = tester.getPreservedType(c1); |
190 | var a1Result = tester.getPreservedType(a1); | 188 | var a1Result = tester.getPreservedType(a1); |
191 | 189 | ||
@@ -197,10 +195,10 @@ class TypeAnalyzerTest { | |||
197 | void circularTypeHierarchyTest() { | 195 | void circularTypeHierarchyTest() { |
198 | var c1 = new PartialRelation("C1", 1); | 196 | var c1 = new PartialRelation("C1", 1); |
199 | var c2 = new PartialRelation("C2", 1); | 197 | var c2 = new PartialRelation("C2", 1); |
200 | var typeInfoMap = new LinkedHashMap<PartialRelation, TypeInfo>(); | 198 | var builder = TypeHierarchy.builder() |
201 | typeInfoMap.put(c1, TypeInfo.builder().supertype(c2).build()); | 199 | .type(c1, c2) |
202 | typeInfoMap.put(c2, TypeInfo.builder().supertype(c1).build()); | 200 | .type(c2, c1); |
203 | 201 | ||
204 | assertThrows(IllegalArgumentException.class, () -> new TypeAnalyzer(typeInfoMap)); | 202 | assertThrows(IllegalArgumentException.class, builder::build); |
205 | } | 203 | } |
206 | } | 204 | } |
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/TypeHierarchyTester.java index 2924816e..647bd782 100644 --- 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/TypeHierarchyTester.java | |||
@@ -11,10 +11,10 @@ import static org.hamcrest.MatcherAssert.assertThat; | |||
11 | import static org.hamcrest.Matchers.*; | 11 | import static org.hamcrest.Matchers.*; |
12 | import static org.hamcrest.Matchers.is; | 12 | import static org.hamcrest.Matchers.is; |
13 | 13 | ||
14 | class TypeAnalyzerTester { | 14 | class TypeHierarchyTester { |
15 | private final TypeAnalyzer sut; | 15 | private final TypeHierarchy sut; |
16 | 16 | ||
17 | public TypeAnalyzerTester(TypeAnalyzer sut) { | 17 | public TypeHierarchyTester(TypeHierarchy sut) { |
18 | this.sut = sut; | 18 | this.sut = sut; |
19 | } | 19 | } |
20 | 20 | ||
@@ -32,22 +32,21 @@ class TypeAnalyzerTester { | |||
32 | 32 | ||
33 | private void assertPreservedType(PartialRelation partialRelation, boolean isAbstract, boolean isVacuous, | 33 | private void assertPreservedType(PartialRelation partialRelation, boolean isAbstract, boolean isVacuous, |
34 | PartialRelation... directSubtypes) { | 34 | PartialRelation... directSubtypes) { |
35 | var result = sut.getAnalysisResults().get(partialRelation); | 35 | var result = sut.getPreservedTypes().get(partialRelation); |
36 | assertThat(result, is(instanceOf(PreservedType.class))); | 36 | assertThat(result, not(nullValue())); |
37 | var preservedResult = (PreservedType) result; | 37 | assertThat(result.isAbstractType(), is(isAbstract)); |
38 | assertThat(preservedResult.isAbstractType(), is(isAbstract)); | 38 | assertThat(result.isVacuous(), is(isVacuous)); |
39 | assertThat(preservedResult.isVacuous(), is(isVacuous)); | 39 | assertThat(result.getDirectSubtypes(), hasItems(directSubtypes)); |
40 | assertThat(preservedResult.getDirectSubtypes(), hasItems(directSubtypes)); | ||
41 | } | 40 | } |
42 | 41 | ||
43 | public void assertEliminatedType(PartialRelation partialRelation, PartialRelation replacement) { | 42 | public void assertEliminatedType(PartialRelation partialRelation, PartialRelation replacement) { |
44 | var result = sut.getAnalysisResults().get(partialRelation); | 43 | var result = sut.getEliminatedTypes().get(partialRelation); |
45 | assertThat(result, is(instanceOf(EliminatedType.class))); | 44 | assertThat(result, not(nullValue())); |
46 | assertThat(((EliminatedType) result).replacement(), is(replacement)); | 45 | assertThat(result, is(replacement)); |
47 | } | 46 | } |
48 | 47 | ||
49 | public PreservedType getPreservedType(PartialRelation partialRelation) { | 48 | public TypeAnalysisResult getPreservedType(PartialRelation partialRelation) { |
50 | return (PreservedType) sut.getAnalysisResults().get(partialRelation); | 49 | return sut.getPreservedTypes().get(partialRelation); |
51 | } | 50 | } |
52 | 51 | ||
53 | public InferredType getInferredType(PartialRelation partialRelation) { | 52 | public InferredType getInferredType(PartialRelation partialRelation) { |