diff options
author | Kristóf Marussy <kristof@marussy.com> | 2023-08-19 20:31:17 +0200 |
---|---|---|
committer | Kristóf Marussy <kristof@marussy.com> | 2023-08-19 20:31:17 +0200 |
commit | dc5fd2a009e43eb2486f50dea6eb9b487ad02c37 (patch) | |
tree | 4f20c29f368b79edce302318b8f9241112ffdd4e /subprojects/store-reasoning/src/main | |
parent | feat: interruptible VIATRA engine (diff) | |
download | refinery-dc5fd2a009e43eb2486f50dea6eb9b487ad02c37.tar.gz refinery-dc5fd2a009e43eb2486f50dea6eb9b487ad02c37.tar.zst refinery-dc5fd2a009e43eb2486f50dea6eb9b487ad02c37.zip |
fix: abstract type chain elimination
Diffstat (limited to 'subprojects/store-reasoning/src/main')
-rw-r--r-- | subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeHierarchy.java | 44 |
1 files changed, 29 insertions, 15 deletions
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeHierarchy.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeHierarchy.java index c32a06cb..35ec54ad 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeHierarchy.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeHierarchy.java | |||
@@ -126,25 +126,37 @@ public class TypeHierarchy { | |||
126 | } | 126 | } |
127 | 127 | ||
128 | private void eliminateTrivialSupertypes() { | 128 | private void eliminateTrivialSupertypes() { |
129 | boolean changed; | 129 | Set<PartialRelation> toInspect = new HashSet<>(extendedTypeInfoMap.keySet()); |
130 | do { | 130 | while (!toInspect.isEmpty()) { |
131 | var toRemove = new ArrayList<PartialRelation>(); | 131 | var toRemove = new ArrayList<PartialRelation>(); |
132 | for (var entry : extendedTypeInfoMap.entrySet()) { | 132 | for (var partialRelation : toInspect) { |
133 | var extendedTypeInfo = entry.getValue(); | 133 | var extendedTypeInfo = extendedTypeInfoMap.get(partialRelation); |
134 | boolean isAbstract = extendedTypeInfo.isAbstractType(); | 134 | if (extendedTypeInfo != null && isTrivialSupertype(extendedTypeInfo)) { |
135 | // Do not eliminate abstract types with 0 subtypes, because they can be used para-consistently, i.e., | 135 | toRemove.add(partialRelation); |
136 | // an object determined to <b>must</b> have an abstract type with 0 subtypes <b>may not</b> ever exist. | ||
137 | boolean hasSingleDirectSubtype = extendedTypeInfo.getDirectSubtypes().size() == 1; | ||
138 | if (isAbstract && hasSingleDirectSubtype) { | ||
139 | toRemove.add(entry.getKey()); | ||
140 | } | 136 | } |
141 | } | 137 | } |
142 | toRemove.forEach(this::removeTrivialType); | 138 | toInspect.clear(); |
143 | changed = !toRemove.isEmpty(); | 139 | for (var partialRelation : toRemove) { |
144 | } while (changed); | 140 | removeTrivialType(partialRelation, toInspect); |
141 | } | ||
142 | } | ||
145 | } | 143 | } |
146 | 144 | ||
147 | private void removeTrivialType(PartialRelation trivialType) { | 145 | private boolean isTrivialSupertype(ExtendedTypeInfo extendedTypeInfo) { |
146 | if (!extendedTypeInfo.isAbstractType()) { | ||
147 | return false; | ||
148 | } | ||
149 | var subtypeIterator = extendedTypeInfo.getDirectSubtypes().iterator(); | ||
150 | if (!subtypeIterator.hasNext()) { | ||
151 | // Do not eliminate abstract types with 0 subtypes, because they can be used para-consistently, i.e., | ||
152 | // an object determined to <b>must</b> have an abstract type with 0 subtypes <b>may not</b> ever exist. | ||
153 | return false; | ||
154 | } | ||
155 | var directSubtype = subtypeIterator.next(); | ||
156 | return !extendedTypeInfoMap.get(directSubtype).isAbstractType() && !subtypeIterator.hasNext(); | ||
157 | } | ||
158 | |||
159 | private void removeTrivialType(PartialRelation trivialType, Set<PartialRelation> toInspect) { | ||
148 | var extendedTypeInfo = extendedTypeInfoMap.get(trivialType); | 160 | var extendedTypeInfo = extendedTypeInfoMap.get(trivialType); |
149 | var iterator = extendedTypeInfo.getDirectSubtypes().iterator(); | 161 | var iterator = extendedTypeInfo.getDirectSubtypes().iterator(); |
150 | if (!iterator.hasNext()) { | 162 | if (!iterator.hasNext()) { |
@@ -156,7 +168,6 @@ public class TypeHierarchy { | |||
156 | throw new AssertionError("Expected trivial supertype %s to have at most 1 direct subtype" | 168 | throw new AssertionError("Expected trivial supertype %s to have at most 1 direct subtype" |
157 | .formatted(trivialType)); | 169 | .formatted(trivialType)); |
158 | } | 170 | } |
159 | replacements.put(trivialType, replacement); | ||
160 | for (var supertype : extendedTypeInfo.getAllSupertypes()) { | 171 | for (var supertype : extendedTypeInfo.getAllSupertypes()) { |
161 | var extendedSupertypeInfo = extendedTypeInfoMap.get(supertype); | 172 | var extendedSupertypeInfo = extendedTypeInfoMap.get(supertype); |
162 | if (!extendedSupertypeInfo.getAllSubtypes().remove(trivialType)) { | 173 | if (!extendedSupertypeInfo.getAllSubtypes().remove(trivialType)) { |
@@ -165,6 +176,9 @@ public class TypeHierarchy { | |||
165 | var directSubtypes = extendedSupertypeInfo.getDirectSubtypes(); | 176 | var directSubtypes = extendedSupertypeInfo.getDirectSubtypes(); |
166 | if (directSubtypes.remove(trivialType)) { | 177 | if (directSubtypes.remove(trivialType)) { |
167 | directSubtypes.add(replacement); | 178 | directSubtypes.add(replacement); |
179 | if (extendedSupertypeInfo.isAbstractType() && directSubtypes.size() == 1) { | ||
180 | toInspect.add(supertype); | ||
181 | } | ||
168 | } | 182 | } |
169 | } | 183 | } |
170 | for (var subtype : extendedTypeInfo.getAllSubtypes()) { | 184 | for (var subtype : extendedTypeInfo.getAllSubtypes()) { |