diff options
author | Kristóf Marussy <kristof@marussy.com> | 2024-06-01 19:21:04 +0200 |
---|---|---|
committer | Kristóf Marussy <kristof@marussy.com> | 2024-06-01 20:17:48 +0200 |
commit | 77e19919f6001b5ea29e707968d97a97d09743d6 (patch) | |
tree | 50885b976aea6c30117caa9fa3c572c2b0386eff /subprojects | |
parent | feat: partial references (diff) | |
download | refinery-77e19919f6001b5ea29e707968d97a97d09743d6.tar.gz refinery-77e19919f6001b5ea29e707968d97a97d09743d6.tar.zst refinery-77e19919f6001b5ea29e707968d97a97d09743d6.zip |
refactor(reasoning): candidate view should always be a refinement of partial
Merge the candidate may/must queries with the partial may/must queries so that
reasoning in the candidate model uses "Gentzen-style" assumptions about the
candidate values of partal symbols that would be computed as unknown.
This should not lead to performance degradation, because the corresponding joins
were already being computed in the stopping criterion. In many cases, the extra
clauses are immediately optimized away by the query optimizer anyways.
Diffstat (limited to 'subprojects')
2 files changed, 26 insertions, 13 deletions
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/PartialRelationTranslator.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/PartialRelationTranslator.java index 1c3f6a6d..a9031f4c 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/PartialRelationTranslator.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/PartialRelationTranslator.java | |||
@@ -52,6 +52,8 @@ public final class PartialRelationTranslator extends PartialSymbolTranslator<Tru | |||
52 | private RelationalQuery must; | 52 | private RelationalQuery must; |
53 | private RelationalQuery candidateMay; | 53 | private RelationalQuery candidateMay; |
54 | private RelationalQuery candidateMust; | 54 | private RelationalQuery candidateMust; |
55 | private RelationalQuery candidateMayMerged; | ||
56 | private RelationalQuery candidateMustMerged; | ||
55 | private RoundingMode roundingMode; | 57 | private RoundingMode roundingMode; |
56 | 58 | ||
57 | private PartialRelationTranslator(PartialRelation partialRelation) { | 59 | private PartialRelationTranslator(PartialRelation partialRelation) { |
@@ -202,6 +204,7 @@ public final class PartialRelationTranslator extends PartialSymbolTranslator<Tru | |||
202 | liftQueries(storeBuilder); | 204 | liftQueries(storeBuilder); |
203 | createFallbackQueriesFromSymbol(); | 205 | createFallbackQueriesFromSymbol(); |
204 | setFallbackCandidateQueries(); | 206 | setFallbackCandidateQueries(); |
207 | mergeCandidateQueries(); | ||
205 | createFallbackRewriter(); | 208 | createFallbackRewriter(); |
206 | createFallbackInterpretation(); | 209 | createFallbackInterpretation(); |
207 | createFallbackRefiner(); | 210 | createFallbackRefiner(); |
@@ -272,9 +275,11 @@ public final class PartialRelationTranslator extends PartialSymbolTranslator<Tru | |||
272 | } | 275 | } |
273 | if (candidateMay == null) { | 276 | if (candidateMay == null) { |
274 | candidateMay = queryBasedRelationRewriter.getCandidateMay(); | 277 | candidateMay = queryBasedRelationRewriter.getCandidateMay(); |
278 | candidateMayMerged = candidateMay; | ||
275 | } | 279 | } |
276 | if (candidateMust == null) { | 280 | if (candidateMust == null) { |
277 | candidateMust = queryBasedRelationRewriter.getCandidateMust(); | 281 | candidateMust = queryBasedRelationRewriter.getCandidateMust(); |
282 | candidateMustMerged = candidateMust; | ||
278 | } | 283 | } |
279 | } | 284 | } |
280 | 285 | ||
@@ -309,15 +314,31 @@ public final class PartialRelationTranslator extends PartialSymbolTranslator<Tru | |||
309 | } | 314 | } |
310 | } | 315 | } |
311 | 316 | ||
317 | private void mergeCandidateQueries() { | ||
318 | if (candidateMayMerged == null) { | ||
319 | candidateMayMerged = createQuery("candidateMayMerged", (builder, arguments) -> builder | ||
320 | .clause( | ||
321 | candidateMay.call(arguments), | ||
322 | may.call(arguments) | ||
323 | )); | ||
324 | } | ||
325 | if (candidateMustMerged == null) { | ||
326 | candidateMustMerged = createQuery("candidateMustMerged", (builder, arguments) -> builder | ||
327 | .clause(candidateMust.call(arguments)) | ||
328 | .clause(must.call(arguments))); | ||
329 | } | ||
330 | } | ||
331 | |||
312 | private void createFallbackRewriter() { | 332 | private void createFallbackRewriter() { |
313 | if (rewriter == null) { | 333 | if (rewriter == null) { |
314 | rewriter = new QueryBasedRelationRewriter(may, must, candidateMay, candidateMust); | 334 | rewriter = new QueryBasedRelationRewriter(may, must, candidateMayMerged, candidateMustMerged); |
315 | } | 335 | } |
316 | } | 336 | } |
317 | 337 | ||
318 | private void createFallbackInterpretation() { | 338 | private void createFallbackInterpretation() { |
319 | if (interpretationFactory == null) { | 339 | if (interpretationFactory == null) { |
320 | interpretationFactory = new QueryBasedRelationInterpretationFactory(may, must, candidateMay, candidateMust); | 340 | interpretationFactory = new QueryBasedRelationInterpretationFactory(may, must, candidateMayMerged, |
341 | candidateMustMerged); | ||
321 | } | 342 | } |
322 | } | 343 | } |
323 | 344 | ||
@@ -354,14 +375,6 @@ public final class PartialRelationTranslator extends PartialSymbolTranslator<Tru | |||
354 | .clause( | 375 | .clause( |
355 | PartialLiterals.candidateMust(partialRelation.call(parameters)), | 376 | PartialLiterals.candidateMust(partialRelation.call(parameters)), |
356 | not(PartialLiterals.candidateMay(partialRelation.call(parameters))) | 377 | not(PartialLiterals.candidateMay(partialRelation.call(parameters))) |
357 | ) | ||
358 | .clause( | ||
359 | PartialLiterals.candidateMust(partialRelation.call(parameters)), | ||
360 | not(PartialLiterals.may(partialRelation.call(parameters))) | ||
361 | ) | ||
362 | .clause( | ||
363 | PartialLiterals.must(partialRelation.call(parameters)), | ||
364 | not(PartialLiterals.candidateMay(partialRelation.call(parameters))) | ||
365 | )); | 378 | )); |
366 | var reject = createQuery("reject", (builder, parameters) -> { | 379 | var reject = createQuery("reject", (builder, parameters) -> { |
367 | var literals = new ArrayList<Literal>(parameters.length + 1); | 380 | var literals = new ArrayList<Literal>(parameters.length + 1); |
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 index e87b2684..85147921 100644 --- 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 | |||
@@ -149,7 +149,7 @@ class TypeHierarchyPartialModelTest { | |||
149 | 149 | ||
150 | var personCandidateInterpretation = reasoningAdapter.getPartialInterpretation(Concreteness.CANDIDATE, person); | 150 | var personCandidateInterpretation = reasoningAdapter.getPartialInterpretation(Concreteness.CANDIDATE, person); |
151 | assertThat(personCandidateInterpretation.get(Tuple.of(1)), is(TruthValue.TRUE)); | 151 | assertThat(personCandidateInterpretation.get(Tuple.of(1)), is(TruthValue.TRUE)); |
152 | assertThat(personCandidateInterpretation.get(Tuple.of(3)), is(TruthValue.FALSE)); | 152 | assertThat(personCandidateInterpretation.get(Tuple.of(3)), is(TruthValue.ERROR)); |
153 | 153 | ||
154 | var memberInterpretation = reasoningAdapter.getPartialInterpretation(Concreteness.PARTIAL, member); | 154 | var memberInterpretation = reasoningAdapter.getPartialInterpretation(Concreteness.PARTIAL, member); |
155 | assertThat(memberInterpretation.get(Tuple.of(1)), is(TruthValue.TRUE)); | 155 | assertThat(memberInterpretation.get(Tuple.of(1)), is(TruthValue.TRUE)); |
@@ -157,7 +157,7 @@ class TypeHierarchyPartialModelTest { | |||
157 | 157 | ||
158 | var memberCandidateInterpretation = reasoningAdapter.getPartialInterpretation(Concreteness.CANDIDATE, member); | 158 | var memberCandidateInterpretation = reasoningAdapter.getPartialInterpretation(Concreteness.CANDIDATE, member); |
159 | assertThat(memberCandidateInterpretation.get(Tuple.of(1)), is(TruthValue.TRUE)); | 159 | assertThat(memberCandidateInterpretation.get(Tuple.of(1)), is(TruthValue.TRUE)); |
160 | assertThat(memberCandidateInterpretation.get(Tuple.of(3)), is(TruthValue.FALSE)); | 160 | assertThat(memberCandidateInterpretation.get(Tuple.of(3)), is(TruthValue.ERROR)); |
161 | 161 | ||
162 | var studentInterpretation = reasoningAdapter.getPartialInterpretation(Concreteness.PARTIAL, student); | 162 | var studentInterpretation = reasoningAdapter.getPartialInterpretation(Concreteness.PARTIAL, student); |
163 | assertThat(studentInterpretation.get(Tuple.of(1)), is(TruthValue.FALSE)); | 163 | assertThat(studentInterpretation.get(Tuple.of(1)), is(TruthValue.FALSE)); |
@@ -165,7 +165,7 @@ class TypeHierarchyPartialModelTest { | |||
165 | 165 | ||
166 | var studentCandidateInterpretation = reasoningAdapter.getPartialInterpretation(Concreteness.CANDIDATE, student); | 166 | var studentCandidateInterpretation = reasoningAdapter.getPartialInterpretation(Concreteness.CANDIDATE, student); |
167 | assertThat(studentCandidateInterpretation.get(Tuple.of(1)), is(TruthValue.FALSE)); | 167 | assertThat(studentCandidateInterpretation.get(Tuple.of(1)), is(TruthValue.FALSE)); |
168 | assertThat(studentCandidateInterpretation.get(Tuple.of(3)), is(TruthValue.FALSE)); | 168 | assertThat(studentCandidateInterpretation.get(Tuple.of(3)), is(TruthValue.ERROR)); |
169 | 169 | ||
170 | var teacherInterpretation = reasoningAdapter.getPartialInterpretation(Concreteness.PARTIAL, teacher); | 170 | var teacherInterpretation = reasoningAdapter.getPartialInterpretation(Concreteness.PARTIAL, teacher); |
171 | assertThat(teacherInterpretation.get(Tuple.of(1)), is(TruthValue.TRUE)); | 171 | assertThat(teacherInterpretation.get(Tuple.of(1)), is(TruthValue.TRUE)); |