diff options
Diffstat (limited to 'subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/internal/PartialClauseRewriter.java')
-rw-r--r-- | subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/internal/PartialClauseRewriter.java | 111 |
1 files changed, 79 insertions, 32 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 c560162e..40993235 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 | |||
@@ -7,8 +7,10 @@ package tools.refinery.store.reasoning.internal; | |||
7 | 7 | ||
8 | import tools.refinery.store.query.Constraint; | 8 | import tools.refinery.store.query.Constraint; |
9 | import tools.refinery.store.query.dnf.Dnf; | 9 | import tools.refinery.store.query.dnf.Dnf; |
10 | import tools.refinery.store.query.dnf.DnfBuilder; | ||
10 | import tools.refinery.store.query.dnf.DnfClause; | 11 | import tools.refinery.store.query.dnf.DnfClause; |
11 | import tools.refinery.store.query.literal.AbstractCallLiteral; | 12 | import tools.refinery.store.query.literal.AbstractCallLiteral; |
13 | import tools.refinery.store.query.literal.AbstractCountLiteral; | ||
12 | import tools.refinery.store.query.literal.CallPolarity; | 14 | import tools.refinery.store.query.literal.CallPolarity; |
13 | import tools.refinery.store.query.literal.Literal; | 15 | import tools.refinery.store.query.literal.Literal; |
14 | import tools.refinery.store.query.term.Aggregator; | 16 | import tools.refinery.store.query.term.Aggregator; |
@@ -17,6 +19,7 @@ import tools.refinery.store.query.term.Term; | |||
17 | import tools.refinery.store.query.term.Variable; | 19 | import tools.refinery.store.query.term.Variable; |
18 | import tools.refinery.store.query.term.int_.IntTerms; | 20 | import tools.refinery.store.query.term.int_.IntTerms; |
19 | import tools.refinery.store.query.term.uppercardinality.UpperCardinalityTerms; | 21 | import tools.refinery.store.query.term.uppercardinality.UpperCardinalityTerms; |
22 | import tools.refinery.store.reasoning.ReasoningAdapter; | ||
20 | import tools.refinery.store.reasoning.literal.*; | 23 | import tools.refinery.store.reasoning.literal.*; |
21 | import tools.refinery.store.reasoning.representation.PartialRelation; | 24 | import tools.refinery.store.reasoning.representation.PartialRelation; |
22 | import tools.refinery.store.reasoning.translator.multiobject.MultiObjectTranslator; | 25 | import tools.refinery.store.reasoning.translator.multiobject.MultiObjectTranslator; |
@@ -58,6 +61,14 @@ class PartialClauseRewriter { | |||
58 | rewriteCountUpperBound(countUpperBoundLiteral); | 61 | rewriteCountUpperBound(countUpperBoundLiteral); |
59 | return; | 62 | return; |
60 | } | 63 | } |
64 | if (callLiteral instanceof CountCandidateLowerBoundLiteral countCandidateLowerBoundLiteral) { | ||
65 | rewriteCountCandidateLowerBound(countCandidateLowerBoundLiteral); | ||
66 | return; | ||
67 | } | ||
68 | if (callLiteral instanceof CountCandidateUpperBoundLiteral countCandidateUpperBoundLiteral) { | ||
69 | rewriteCountCandidateUpperBound(countCandidateUpperBoundLiteral); | ||
70 | return; | ||
71 | } | ||
61 | var target = callLiteral.getTarget(); | 72 | var target = callLiteral.getTarget(); |
62 | if (target instanceof Dnf dnf) { | 73 | if (target instanceof Dnf dnf) { |
63 | rewriteRecursively(callLiteral, dnf); | 74 | rewriteRecursively(callLiteral, dnf); |
@@ -78,48 +89,26 @@ class PartialClauseRewriter { | |||
78 | } | 89 | } |
79 | 90 | ||
80 | private void rewriteCountLowerBound(CountLowerBoundLiteral literal) { | 91 | private void rewriteCountLowerBound(CountLowerBoundLiteral literal) { |
81 | rewriteCount(literal, "lower", Modality.MUST, MultiObjectTranslator.LOWER_CARDINALITY_VIEW, 1, IntTerms::mul, | 92 | rewritePartialCount(literal, "lower", Modality.MUST, MultiObjectTranslator.LOWER_CARDINALITY_VIEW, 1, |
82 | IntTerms.INT_SUM); | 93 | IntTerms::mul, IntTerms.INT_SUM); |
83 | } | 94 | } |
84 | 95 | ||
85 | private void rewriteCountUpperBound(CountUpperBoundLiteral literal) { | 96 | private void rewriteCountUpperBound(CountUpperBoundLiteral literal) { |
86 | rewriteCount(literal, "upper", Modality.MAY, MultiObjectTranslator.UPPER_CARDINALITY_VIEW, | 97 | rewritePartialCount(literal, "upper", Modality.MAY, MultiObjectTranslator.UPPER_CARDINALITY_VIEW, |
87 | UpperCardinalities.ONE, UpperCardinalityTerms::mul, UpperCardinalityTerms.UPPER_CARDINALITY_SUM); | 98 | UpperCardinalities.ONE, UpperCardinalityTerms::mul, UpperCardinalityTerms.UPPER_CARDINALITY_SUM); |
88 | } | 99 | } |
89 | 100 | ||
90 | private <T> void rewriteCount(ConcreteCountLiteral<T> literal, String name, Modality modality, Constraint view, | 101 | private <T> void rewritePartialCount(AbstractCountLiteral<T> literal, String name, Modality modality, |
91 | T one, BinaryOperator<Term<T>> mul, Aggregator<T, T> sum) { | 102 | Constraint view, T one, BinaryOperator<Term<T>> mul, Aggregator<T, T> sum) { |
92 | var type = literal.getResultType(); | 103 | var type = literal.getResultType(); |
93 | var target = literal.getTarget(); | 104 | var countResult = computeCountVariables(literal, Concreteness.PARTIAL, name); |
94 | var concreteness = literal.getConcreteness(); | 105 | var builder = countResult.builder(); |
95 | int arity = target.arity(); | ||
96 | var parameters = target.getParameters(); | ||
97 | var literalArguments = literal.getArguments(); | ||
98 | var privateVariables = literal.getPrivateVariables(positiveVariables); | ||
99 | |||
100 | var builder = Dnf.builder("%s#%s#%s".formatted(target.name(), concreteness, name)); | ||
101 | var rewrittenArguments = new ArrayList<Variable>(parameters.size()); | ||
102 | var variablesToCount = new ArrayList<Variable>(); | ||
103 | var helperArguments = new ArrayList<Variable>(); | ||
104 | var literalToRewrittenArgumentMap = new HashMap<Variable, Variable>(); | ||
105 | for (int i = 0; i < arity; i++) { | ||
106 | var literalArgument = literalArguments.get(i); | ||
107 | var parameter = parameters.get(i); | ||
108 | var rewrittenArgument = literalToRewrittenArgumentMap.computeIfAbsent(literalArgument, key -> { | ||
109 | helperArguments.add(key); | ||
110 | var newArgument = builder.parameter(parameter); | ||
111 | if (privateVariables.contains(key)) { | ||
112 | variablesToCount.add(newArgument); | ||
113 | } | ||
114 | return newArgument; | ||
115 | }); | ||
116 | rewrittenArguments.add(rewrittenArgument); | ||
117 | } | ||
118 | var outputVariable = builder.parameter(type); | 106 | var outputVariable = builder.parameter(type); |
107 | var variablesToCount = countResult.variablesToCount(); | ||
119 | 108 | ||
120 | var literals = new ArrayList<Literal>(); | 109 | var literals = new ArrayList<Literal>(); |
121 | literals.add(new ModalConstraint(modality, literal.getConcreteness(), target) | 110 | literals.add(new ModalConstraint(modality, Concreteness.PARTIAL, literal.getTarget()) |
122 | .call(CallPolarity.POSITIVE, rewrittenArguments)); | 111 | .call(CallPolarity.POSITIVE, countResult.rewrittenArguments())); |
123 | switch (variablesToCount.size()) { | 112 | switch (variablesToCount.size()) { |
124 | case 0 -> literals.add(outputVariable.assign(new ConstantTerm<>(type, one))); | 113 | case 0 -> literals.add(outputVariable.assign(new ConstantTerm<>(type, one))); |
125 | case 1 -> literals.add(view.call(variablesToCount.get(0), | 114 | case 1 -> literals.add(view.call(variablesToCount.get(0), |
@@ -141,11 +130,65 @@ class PartialClauseRewriter { | |||
141 | 130 | ||
142 | var helperQuery = builder.build(); | 131 | var helperQuery = builder.build(); |
143 | var aggregationVariable = Variable.of(type); | 132 | var aggregationVariable = Variable.of(type); |
133 | var helperArguments = countResult.helperArguments(); | ||
144 | helperArguments.add(aggregationVariable); | 134 | helperArguments.add(aggregationVariable); |
145 | workList.addFirst(literal.getResultVariable().assign(helperQuery.aggregateBy(aggregationVariable, sum, | 135 | workList.addFirst(literal.getResultVariable().assign(helperQuery.aggregateBy(aggregationVariable, sum, |
146 | helperArguments))); | 136 | helperArguments))); |
147 | } | 137 | } |
148 | 138 | ||
139 | private void rewriteCountCandidateLowerBound(CountCandidateLowerBoundLiteral literal) { | ||
140 | rewriteCandidateCount(literal, "lower", Modality.MAY); | ||
141 | } | ||
142 | |||
143 | private void rewriteCountCandidateUpperBound(CountCandidateUpperBoundLiteral literal) { | ||
144 | rewriteCandidateCount(literal, "upper", Modality.MUST); | ||
145 | } | ||
146 | |||
147 | private void rewriteCandidateCount(AbstractCountLiteral<Integer> literal, String name, Modality modality) { | ||
148 | var countResult = computeCountVariables(literal, Concreteness.CANDIDATE, name); | ||
149 | var builder = countResult.builder(); | ||
150 | |||
151 | var literals = new ArrayList<Literal>(); | ||
152 | literals.add(new ModalConstraint(modality, Concreteness.CANDIDATE, literal.getTarget()) | ||
153 | .call(CallPolarity.POSITIVE, countResult.rewrittenArguments())); | ||
154 | for (var variable : countResult.variablesToCount()) { | ||
155 | literals.add(new ModalConstraint(modality, Concreteness.CANDIDATE, ReasoningAdapter.EXISTS_SYMBOL) | ||
156 | .call(variable)); | ||
157 | } | ||
158 | builder.clause(literals); | ||
159 | |||
160 | var helperQuery = builder.build(); | ||
161 | workList.addFirst(literal.getResultVariable().assign(helperQuery.count(countResult.helperArguments()))); | ||
162 | } | ||
163 | |||
164 | private CountResult computeCountVariables(AbstractCountLiteral<?> literal, Concreteness concreteness, | ||
165 | String name) { | ||
166 | var target = literal.getTarget(); | ||
167 | int arity = target.arity(); | ||
168 | var parameters = target.getParameters(); | ||
169 | var literalArguments = literal.getArguments(); | ||
170 | var privateVariables = literal.getPrivateVariables(positiveVariables); | ||
171 | var builder = Dnf.builder("%s#%s#%s".formatted(target.name(), concreteness, name)); | ||
172 | var rewrittenArguments = new ArrayList<Variable>(parameters.size()); | ||
173 | var variablesToCount = new ArrayList<Variable>(); | ||
174 | var helperArguments = new ArrayList<Variable>(); | ||
175 | var literalToRewrittenArgumentMap = new HashMap<Variable, Variable>(); | ||
176 | for (int i = 0; i < arity; i++) { | ||
177 | var literalArgument = literalArguments.get(i); | ||
178 | var parameter = parameters.get(i); | ||
179 | var rewrittenArgument = literalToRewrittenArgumentMap.computeIfAbsent(literalArgument, key -> { | ||
180 | helperArguments.add(key); | ||
181 | var newArgument = builder.parameter(parameter); | ||
182 | if (privateVariables.contains(key)) { | ||
183 | variablesToCount.add(newArgument); | ||
184 | } | ||
185 | return newArgument; | ||
186 | }); | ||
187 | rewrittenArguments.add(rewrittenArgument); | ||
188 | } | ||
189 | return new CountResult(builder, rewrittenArguments, helperArguments, variablesToCount); | ||
190 | } | ||
191 | |||
149 | private void markAsDone(Literal literal) { | 192 | private void markAsDone(Literal literal) { |
150 | completedLiterals.add(literal); | 193 | completedLiterals.add(literal); |
151 | positiveVariables.addAll(literal.getOutputVariables()); | 194 | positiveVariables.addAll(literal.getOutputVariables()); |
@@ -173,4 +216,8 @@ class PartialClauseRewriter { | |||
173 | workList.addFirst(literals.get(i)); | 216 | workList.addFirst(literals.get(i)); |
174 | } | 217 | } |
175 | } | 218 | } |
219 | |||
220 | private record CountResult(DnfBuilder builder, List<Variable> rewrittenArguments, List<Variable> helperArguments, | ||
221 | List<Variable> variablesToCount) { | ||
222 | } | ||
176 | } | 223 | } |