diff options
author | Kristóf Marussy <kristof@marussy.com> | 2024-06-01 14:47:31 +0200 |
---|---|---|
committer | Kristóf Marussy <kristof@marussy.com> | 2024-06-01 20:17:47 +0200 |
commit | efc6158cd3b971547fc77fb042fa7ab7804434b3 (patch) | |
tree | 7661b5cd430d1ce8b9c2297054ff4b0514abcbe9 /subprojects/store-reasoning/src/main/java | |
parent | feat: generate multiple solutions (diff) | |
download | refinery-efc6158cd3b971547fc77fb042fa7ab7804434b3.tar.gz refinery-efc6158cd3b971547fc77fb042fa7ab7804434b3.tar.zst refinery-efc6158cd3b971547fc77fb042fa7ab7804434b3.zip |
fix(reasoning): candidate count literal rewriting
Diffstat (limited to 'subprojects/store-reasoning/src/main/java')
-rw-r--r-- | subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/internal/PartialClauseRewriter.java | 64 |
1 files changed, 28 insertions, 36 deletions
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/internal/PartialClauseRewriter.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/internal/PartialClauseRewriter.java index dc508a7b..f7e86c44 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/internal/PartialClauseRewriter.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/internal/PartialClauseRewriter.java | |||
@@ -1,5 +1,5 @@ | |||
1 | /* | 1 | /* |
2 | * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/> | 2 | * SPDX-FileCopyrightText: 2023-2024 The Refinery Authors <https://refinery.tools/> |
3 | * | 3 | * |
4 | * SPDX-License-Identifier: EPL-2.0 | 4 | * SPDX-License-Identifier: EPL-2.0 |
5 | */ | 5 | */ |
@@ -53,38 +53,30 @@ class PartialClauseRewriter { | |||
53 | markAsDone(literal); | 53 | markAsDone(literal); |
54 | return; | 54 | return; |
55 | } | 55 | } |
56 | if (callLiteral instanceof CountLowerBoundLiteral countLowerBoundLiteral) { | 56 | switch (callLiteral) { |
57 | rewriteCountLowerBound(countLowerBoundLiteral); | 57 | case CountLowerBoundLiteral countLowerBoundLiteral -> rewriteCountLowerBound(countLowerBoundLiteral); |
58 | return; | 58 | case CountUpperBoundLiteral countUpperBoundLiteral -> rewriteCountUpperBound(countUpperBoundLiteral); |
59 | } | 59 | case CountCandidateLowerBoundLiteral countCandidateLowerBoundLiteral -> |
60 | if (callLiteral instanceof CountUpperBoundLiteral countUpperBoundLiteral) { | 60 | rewriteCountCandidateLowerBound(countCandidateLowerBoundLiteral); |
61 | rewriteCountUpperBound(countUpperBoundLiteral); | 61 | case CountCandidateUpperBoundLiteral countCandidateUpperBoundLiteral -> |
62 | return; | 62 | rewriteCountCandidateUpperBound(countCandidateUpperBoundLiteral); |
63 | } | 63 | default -> { |
64 | if (callLiteral instanceof CountCandidateLowerBoundLiteral countCandidateLowerBoundLiteral) { | 64 | var target = callLiteral.getTarget(); |
65 | rewriteCountCandidateLowerBound(countCandidateLowerBoundLiteral); | 65 | switch (target) { |
66 | return; | 66 | case Dnf dnf -> rewriteRecursively(callLiteral, dnf); |
67 | } | 67 | case ModalConstraint modalConstraint -> { |
68 | if (callLiteral instanceof CountCandidateUpperBoundLiteral countCandidateUpperBoundLiteral) { | 68 | var modality = modalConstraint.modality(); |
69 | rewriteCountCandidateUpperBound(countCandidateUpperBoundLiteral); | 69 | var concreteness = modalConstraint.concreteness(); |
70 | return; | 70 | var constraint = modalConstraint.constraint(); |
71 | } | 71 | switch (constraint) { |
72 | var target = callLiteral.getTarget(); | 72 | case Dnf dnf -> rewriteRecursively(callLiteral, modality, concreteness, dnf); |
73 | if (target instanceof Dnf dnf) { | 73 | case PartialRelation partialRelation -> rewrite(callLiteral, modality, concreteness, partialRelation); |
74 | rewriteRecursively(callLiteral, dnf); | 74 | default -> throw new IllegalArgumentException("Cannot interpret modal constraint: " + modalConstraint); |
75 | } else if (target instanceof ModalConstraint modalConstraint) { | 75 | } |
76 | var modality = modalConstraint.modality(); | ||
77 | var concreteness = modalConstraint.concreteness(); | ||
78 | var constraint = modalConstraint.constraint(); | ||
79 | if (constraint instanceof Dnf dnf) { | ||
80 | rewriteRecursively(callLiteral, modality, concreteness, dnf); | ||
81 | } else if (constraint instanceof PartialRelation partialRelation) { | ||
82 | rewrite(callLiteral, modality, concreteness, partialRelation); | ||
83 | } else { | ||
84 | throw new IllegalArgumentException("Cannot interpret modal constraint: " + modalConstraint); | ||
85 | } | 76 | } |
86 | } else { | 77 | default -> markAsDone(literal); |
87 | markAsDone(literal); | 78 | } |
79 | } | ||
88 | } | 80 | } |
89 | } | 81 | } |
90 | 82 | ||
@@ -111,11 +103,11 @@ class PartialClauseRewriter { | |||
111 | .call(CallPolarity.POSITIVE, countResult.rewrittenArguments())); | 103 | .call(CallPolarity.POSITIVE, countResult.rewrittenArguments())); |
112 | switch (variablesToCount.size()) { | 104 | switch (variablesToCount.size()) { |
113 | case 0 -> literals.add(outputVariable.assign(new ConstantTerm<>(type, one))); | 105 | case 0 -> literals.add(outputVariable.assign(new ConstantTerm<>(type, one))); |
114 | case 1 -> literals.add(view.call(variablesToCount.get(0), | 106 | case 1 -> literals.add(view.call(variablesToCount.getFirst(), |
115 | outputVariable)); | 107 | outputVariable)); |
116 | default -> { | 108 | default -> { |
117 | var firstCount = Variable.of(type); | 109 | var firstCount = Variable.of(type); |
118 | literals.add(view.call(variablesToCount.get(0), firstCount)); | 110 | literals.add(view.call(variablesToCount.getFirst(), firstCount)); |
119 | int length = variablesToCount.size(); | 111 | int length = variablesToCount.size(); |
120 | Term<T> accumulator = firstCount; | 112 | Term<T> accumulator = firstCount; |
121 | for (int i = 1; i < length; i++) { | 113 | for (int i = 1; i < length; i++) { |
@@ -137,11 +129,11 @@ class PartialClauseRewriter { | |||
137 | } | 129 | } |
138 | 130 | ||
139 | private void rewriteCountCandidateLowerBound(CountCandidateLowerBoundLiteral literal) { | 131 | private void rewriteCountCandidateLowerBound(CountCandidateLowerBoundLiteral literal) { |
140 | rewriteCandidateCount(literal, "lower", Modality.MAY); | 132 | rewriteCandidateCount(literal, "lower", Modality.MUST); |
141 | } | 133 | } |
142 | 134 | ||
143 | private void rewriteCountCandidateUpperBound(CountCandidateUpperBoundLiteral literal) { | 135 | private void rewriteCountCandidateUpperBound(CountCandidateUpperBoundLiteral literal) { |
144 | rewriteCandidateCount(literal, "upper", Modality.MUST); | 136 | rewriteCandidateCount(literal, "upper", Modality.MAY); |
145 | } | 137 | } |
146 | 138 | ||
147 | private void rewriteCandidateCount(AbstractCountLiteral<Integer> literal, String name, Modality modality) { | 139 | private void rewriteCandidateCount(AbstractCountLiteral<Integer> literal, String name, Modality modality) { |