diff options
author | Kristóf Marussy <marussy@mit.bme.hu> | 2023-09-14 19:29:36 +0200 |
---|---|---|
committer | GitHub <noreply@github.com> | 2023-09-14 19:29:36 +0200 |
commit | 98ed3b6db5f4e51961a161050cc31c66015116e8 (patch) | |
tree | 8bfd6d9bc8d6ed23b9eb0f889dd40b6c24fe8f92 /subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/PartialRelationTranslator.java | |
parent | Merge pull request #38 from nagilooh/design-space-exploration (diff) | |
parent | Merge remote-tracking branch 'upstream/main' into partial-interpretation (diff) | |
download | refinery-98ed3b6db5f4e51961a161050cc31c66015116e8.tar.gz refinery-98ed3b6db5f4e51961a161050cc31c66015116e8.tar.zst refinery-98ed3b6db5f4e51961a161050cc31c66015116e8.zip |
Merge pull request #39 from kris7t/partial-interpretation
Implement partial interpretation based model generation
Diffstat (limited to 'subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/PartialRelationTranslator.java')
-rw-r--r-- | subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/PartialRelationTranslator.java | 390 |
1 files changed, 390 insertions, 0 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 new file mode 100644 index 00000000..c2039afc --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/PartialRelationTranslator.java | |||
@@ -0,0 +1,390 @@ | |||
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; | ||
7 | |||
8 | import tools.refinery.store.dse.transition.Rule; | ||
9 | import tools.refinery.store.dse.transition.objectives.Criteria; | ||
10 | import tools.refinery.store.dse.transition.objectives.Criterion; | ||
11 | import tools.refinery.store.dse.transition.objectives.Objective; | ||
12 | import tools.refinery.store.dse.transition.objectives.Objectives; | ||
13 | import tools.refinery.store.model.ModelStoreBuilder; | ||
14 | import tools.refinery.store.query.Constraint; | ||
15 | import tools.refinery.store.query.dnf.Query; | ||
16 | import tools.refinery.store.query.dnf.QueryBuilder; | ||
17 | import tools.refinery.store.query.dnf.RelationalQuery; | ||
18 | import tools.refinery.store.query.literal.Literal; | ||
19 | import tools.refinery.store.query.term.NodeVariable; | ||
20 | import tools.refinery.store.query.view.MayView; | ||
21 | import tools.refinery.store.query.view.MustView; | ||
22 | import tools.refinery.store.reasoning.ReasoningAdapter; | ||
23 | import tools.refinery.store.reasoning.ReasoningBuilder; | ||
24 | import tools.refinery.store.reasoning.interpretation.PartialInterpretation; | ||
25 | import tools.refinery.store.reasoning.interpretation.PartialRelationRewriter; | ||
26 | import tools.refinery.store.reasoning.interpretation.QueryBasedRelationInterpretationFactory; | ||
27 | import tools.refinery.store.reasoning.interpretation.QueryBasedRelationRewriter; | ||
28 | import tools.refinery.store.reasoning.lifting.DnfLifter; | ||
29 | import tools.refinery.store.reasoning.literal.Concreteness; | ||
30 | import tools.refinery.store.reasoning.literal.Modality; | ||
31 | import tools.refinery.store.reasoning.literal.PartialLiterals; | ||
32 | import tools.refinery.store.reasoning.refinement.ConcreteSymbolRefiner; | ||
33 | import tools.refinery.store.reasoning.refinement.PartialInterpretationRefiner; | ||
34 | import tools.refinery.store.reasoning.refinement.PartialModelInitializer; | ||
35 | import tools.refinery.store.reasoning.refinement.StorageRefiner; | ||
36 | import tools.refinery.store.reasoning.representation.PartialRelation; | ||
37 | import tools.refinery.store.representation.AnySymbol; | ||
38 | import tools.refinery.store.representation.Symbol; | ||
39 | import tools.refinery.store.representation.TruthValue; | ||
40 | |||
41 | import java.util.ArrayList; | ||
42 | import java.util.function.BiConsumer; | ||
43 | |||
44 | import static tools.refinery.store.query.literal.Literals.not; | ||
45 | |||
46 | @SuppressWarnings("UnusedReturnValue") | ||
47 | public final class PartialRelationTranslator extends PartialSymbolTranslator<TruthValue, Boolean> { | ||
48 | private final PartialRelation partialRelation; | ||
49 | private PartialRelationRewriter rewriter; | ||
50 | private RelationalQuery query; | ||
51 | private RelationalQuery may; | ||
52 | private RelationalQuery must; | ||
53 | private RelationalQuery candidateMay; | ||
54 | private RelationalQuery candidateMust; | ||
55 | private RoundingMode roundingMode; | ||
56 | |||
57 | private PartialRelationTranslator(PartialRelation partialRelation) { | ||
58 | super(partialRelation); | ||
59 | this.partialRelation = partialRelation; | ||
60 | } | ||
61 | |||
62 | public PartialRelation getPartialRelation() { | ||
63 | return partialRelation; | ||
64 | } | ||
65 | |||
66 | @Override | ||
67 | public PartialRelationTranslator symbol(AnySymbol storageSymbol) { | ||
68 | super.symbol(storageSymbol); | ||
69 | return this; | ||
70 | } | ||
71 | |||
72 | @Override | ||
73 | public <T> PartialRelationTranslator symbol(Symbol<T> storageSymbol, | ||
74 | StorageRefiner.Factory<T> storageRefiner) { | ||
75 | super.symbol(storageSymbol, storageRefiner); | ||
76 | return this; | ||
77 | } | ||
78 | |||
79 | @Override | ||
80 | public PartialRelationTranslator interpretation( | ||
81 | PartialInterpretation.Factory<TruthValue, Boolean> interpretationFactory) { | ||
82 | super.interpretation(interpretationFactory); | ||
83 | return this; | ||
84 | } | ||
85 | |||
86 | @Override | ||
87 | public PartialRelationTranslator refiner( | ||
88 | PartialInterpretationRefiner.Factory<TruthValue, Boolean> interpretationRefiner) { | ||
89 | super.refiner(interpretationRefiner); | ||
90 | return this; | ||
91 | } | ||
92 | |||
93 | public PartialRelationTranslator rewriter(PartialRelationRewriter rewriter) { | ||
94 | checkNotConfigured(); | ||
95 | if (this.rewriter != null) { | ||
96 | throw new IllegalArgumentException("Rewriter was already set"); | ||
97 | } | ||
98 | this.rewriter = rewriter; | ||
99 | return this; | ||
100 | } | ||
101 | |||
102 | @Override | ||
103 | public PartialRelationTranslator initializer(PartialModelInitializer initializer) { | ||
104 | super.initializer(initializer); | ||
105 | return this; | ||
106 | } | ||
107 | |||
108 | @Override | ||
109 | public PartialRelationTranslator decision(Rule decisionRule) { | ||
110 | super.decision(decisionRule); | ||
111 | return this; | ||
112 | } | ||
113 | |||
114 | @Override | ||
115 | public PartialRelationTranslator accept(Criterion acceptanceCriterion) { | ||
116 | super.accept(acceptanceCriterion); | ||
117 | return this; | ||
118 | } | ||
119 | |||
120 | @Override | ||
121 | public PartialRelationTranslator exclude(Criterion exclusionCriterion) { | ||
122 | super.exclude(exclusionCriterion); | ||
123 | return this; | ||
124 | } | ||
125 | |||
126 | @Override | ||
127 | public PartialRelationTranslator objective(Objective objective) { | ||
128 | super.objective(objective); | ||
129 | return this; | ||
130 | } | ||
131 | |||
132 | public PartialRelationTranslator query(RelationalQuery query) { | ||
133 | checkNotConfigured(); | ||
134 | if (this.query != null) { | ||
135 | throw new IllegalArgumentException("Query was already set"); | ||
136 | } | ||
137 | this.query = query; | ||
138 | return this; | ||
139 | } | ||
140 | |||
141 | public PartialRelationTranslator may(RelationalQuery may) { | ||
142 | checkNotConfigured(); | ||
143 | if (this.may != null) { | ||
144 | throw new IllegalArgumentException("May query was already set"); | ||
145 | } | ||
146 | this.may = may; | ||
147 | return this; | ||
148 | } | ||
149 | |||
150 | public PartialRelationTranslator mayNever() { | ||
151 | var never = createQuery(partialRelation.name() + "#never", (builder, parameters) -> {}); | ||
152 | may(never); | ||
153 | return this; | ||
154 | } | ||
155 | |||
156 | public PartialRelationTranslator must(RelationalQuery must) { | ||
157 | checkNotConfigured(); | ||
158 | if (this.must != null) { | ||
159 | throw new IllegalArgumentException("Must query was already set"); | ||
160 | } | ||
161 | this.must = must; | ||
162 | return this; | ||
163 | } | ||
164 | |||
165 | public PartialRelationTranslator candidate(RelationalQuery candidate) { | ||
166 | candidateMay(candidate); | ||
167 | candidateMust(candidate); | ||
168 | return this; | ||
169 | } | ||
170 | |||
171 | public PartialRelationTranslator candidateMay(RelationalQuery candidateMay) { | ||
172 | checkNotConfigured(); | ||
173 | if (this.candidateMay != null) { | ||
174 | throw new IllegalArgumentException("Candidate may query was already set"); | ||
175 | } | ||
176 | this.candidateMay = candidateMay; | ||
177 | return this; | ||
178 | } | ||
179 | |||
180 | public PartialRelationTranslator candidateMust(RelationalQuery candidateMust) { | ||
181 | checkNotConfigured(); | ||
182 | if (this.candidateMust != null) { | ||
183 | throw new IllegalArgumentException("Candidate must query was already set"); | ||
184 | } | ||
185 | this.candidateMust = candidateMust; | ||
186 | return this; | ||
187 | } | ||
188 | |||
189 | public PartialRelationTranslator roundingMode(RoundingMode roundingMode) { | ||
190 | checkNotConfigured(); | ||
191 | if (this.roundingMode != null) { | ||
192 | throw new IllegalArgumentException("Rounding mode was already set"); | ||
193 | } | ||
194 | this.roundingMode = roundingMode; | ||
195 | return this; | ||
196 | } | ||
197 | |||
198 | @Override | ||
199 | protected void doConfigure(ModelStoreBuilder storeBuilder) { | ||
200 | setFallbackRoundingMode(); | ||
201 | createFallbackQueryFromRewriter(); | ||
202 | liftQueries(storeBuilder); | ||
203 | createFallbackQueriesFromSymbol(); | ||
204 | setFallbackCandidateQueries(); | ||
205 | createFallbackRewriter(); | ||
206 | createFallbackInterpretation(); | ||
207 | createFallbackRefiner(); | ||
208 | createFallbackExclude(); | ||
209 | createFallbackObjective(); | ||
210 | super.doConfigure(storeBuilder); | ||
211 | } | ||
212 | |||
213 | private void setFallbackRoundingMode() { | ||
214 | if (roundingMode == null) { | ||
215 | roundingMode = query == null && storageSymbol != null ? RoundingMode.PREFER_FALSE : RoundingMode.NONE; | ||
216 | } | ||
217 | } | ||
218 | |||
219 | private RelationalQuery createQuery(String name, BiConsumer<QueryBuilder, NodeVariable[]> callback) { | ||
220 | int arity = partialRelation.arity(); | ||
221 | var queryBuilder = Query.builder(name); | ||
222 | var parameters = new NodeVariable[arity]; | ||
223 | for (int i = 0; i < arity; i++) { | ||
224 | parameters[i] = queryBuilder.parameter("p" + 1); | ||
225 | } | ||
226 | callback.accept(queryBuilder, parameters); | ||
227 | return queryBuilder.build(); | ||
228 | } | ||
229 | |||
230 | private RelationalQuery createQuery(String name, Constraint constraint) { | ||
231 | return createQuery(name, (builder, parameters) -> builder.clause(constraint.call(parameters))); | ||
232 | } | ||
233 | |||
234 | private void createFallbackQueryFromRewriter() { | ||
235 | if (rewriter != null && query == null) { | ||
236 | query = createQuery(partialRelation.name(), partialRelation); | ||
237 | } | ||
238 | } | ||
239 | |||
240 | private void createFallbackQueriesFromSymbol() { | ||
241 | if (storageSymbol == null || storageSymbol.valueType() != TruthValue.class) { | ||
242 | return; | ||
243 | } | ||
244 | // We checked in the guard clause that this is safe. | ||
245 | @SuppressWarnings("unchecked") | ||
246 | var typedStorageSymbol = (Symbol<TruthValue>) storageSymbol; | ||
247 | var defaultValue = typedStorageSymbol.defaultValue(); | ||
248 | if (may == null && !defaultValue.may()) { | ||
249 | may = createQuery(DnfLifter.decorateName(partialRelation.name(), Modality.MAY, Concreteness.PARTIAL), | ||
250 | new MayView(typedStorageSymbol)); | ||
251 | } | ||
252 | if (must == null && !defaultValue.must()) { | ||
253 | must = createQuery(DnfLifter.decorateName(partialRelation.name(), Modality.MUST, Concreteness.PARTIAL), | ||
254 | new MustView(typedStorageSymbol)); | ||
255 | } | ||
256 | } | ||
257 | |||
258 | private void liftQueries(ModelStoreBuilder storeBuilder) { | ||
259 | if (rewriter instanceof QueryBasedRelationRewriter queryBasedRelationRewriter) { | ||
260 | liftQueriesFromQueryBasedRewriter(queryBasedRelationRewriter); | ||
261 | } else if (query != null) { | ||
262 | liftQueriesFromFourValuedQuery(storeBuilder); | ||
263 | } | ||
264 | } | ||
265 | |||
266 | private void liftQueriesFromQueryBasedRewriter(QueryBasedRelationRewriter queryBasedRelationRewriter) { | ||
267 | if (may == null) { | ||
268 | may = queryBasedRelationRewriter.getMay(); | ||
269 | } | ||
270 | if (must == null) { | ||
271 | must = queryBasedRelationRewriter.getMust(); | ||
272 | } | ||
273 | if (candidateMay == null) { | ||
274 | candidateMay = queryBasedRelationRewriter.getCandidateMay(); | ||
275 | } | ||
276 | if (candidateMust == null) { | ||
277 | candidateMust = queryBasedRelationRewriter.getCandidateMust(); | ||
278 | } | ||
279 | } | ||
280 | |||
281 | private void liftQueriesFromFourValuedQuery(ModelStoreBuilder storeBuilder) { | ||
282 | var reasoningBuilder = storeBuilder.getAdapter(ReasoningBuilder.class); | ||
283 | if (may == null) { | ||
284 | may = reasoningBuilder.lift(Modality.MAY, Concreteness.PARTIAL, query); | ||
285 | } | ||
286 | if (must == null) { | ||
287 | must = reasoningBuilder.lift(Modality.MUST, Concreteness.PARTIAL, query); | ||
288 | } | ||
289 | if (candidateMay == null) { | ||
290 | candidateMay = reasoningBuilder.lift(Modality.MAY, Concreteness.CANDIDATE, query); | ||
291 | } | ||
292 | if (candidateMust == null) { | ||
293 | candidateMust = reasoningBuilder.lift(Modality.MAY, Concreteness.CANDIDATE, query); | ||
294 | } | ||
295 | } | ||
296 | |||
297 | private void setFallbackCandidateQueries() { | ||
298 | if (candidateMay == null) { | ||
299 | candidateMay = switch (roundingMode) { | ||
300 | case NONE, PREFER_TRUE -> may; | ||
301 | case PREFER_FALSE -> must; | ||
302 | }; | ||
303 | } | ||
304 | if (candidateMust == null) { | ||
305 | candidateMust = switch (roundingMode) { | ||
306 | case NONE, PREFER_FALSE -> must; | ||
307 | case PREFER_TRUE -> may; | ||
308 | }; | ||
309 | } | ||
310 | } | ||
311 | |||
312 | private void createFallbackRewriter() { | ||
313 | if (rewriter == null) { | ||
314 | rewriter = new QueryBasedRelationRewriter(may, must, candidateMay, candidateMust); | ||
315 | } | ||
316 | } | ||
317 | |||
318 | private void createFallbackInterpretation() { | ||
319 | if (interpretationFactory == null) { | ||
320 | interpretationFactory = new QueryBasedRelationInterpretationFactory(may, must, candidateMay, candidateMust); | ||
321 | } | ||
322 | } | ||
323 | |||
324 | private void createFallbackRefiner() { | ||
325 | if (interpretationRefiner == null && storageSymbol != null && storageSymbol.valueType() == TruthValue.class) { | ||
326 | // We checked in the condition that this is safe. | ||
327 | @SuppressWarnings("unchecked") | ||
328 | var typedStorageSymbol = (Symbol<TruthValue>) storageSymbol; | ||
329 | interpretationRefiner = ConcreteSymbolRefiner.of(typedStorageSymbol); | ||
330 | } | ||
331 | } | ||
332 | |||
333 | private void createFallbackExclude() { | ||
334 | if (excludeWasSet) { | ||
335 | return; | ||
336 | } | ||
337 | var excludeQuery = createQuery("exclude", (builder, parameters) -> { | ||
338 | var literals = new ArrayList<Literal>(parameters.length + 2); | ||
339 | literals.add(PartialLiterals.must(partialRelation.call(parameters))); | ||
340 | literals.add(not(PartialLiterals.may(partialRelation.call(parameters)))); | ||
341 | for (var parameter : parameters) { | ||
342 | literals.add(PartialLiterals.must(ReasoningAdapter.EXISTS_SYMBOL.call(parameter))); | ||
343 | } | ||
344 | builder.clause(literals); | ||
345 | }); | ||
346 | exclude = Criteria.whenHasMatch(excludeQuery); | ||
347 | } | ||
348 | |||
349 | private void createFallbackObjective() { | ||
350 | if (acceptWasSet && objectiveWasSet) { | ||
351 | return; | ||
352 | } | ||
353 | var invalidCandidate = createQuery("invalidCandidate", (builder, parameters) -> builder | ||
354 | .clause( | ||
355 | PartialLiterals.candidateMust(partialRelation.call(parameters)), | ||
356 | 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 | )); | ||
366 | var reject = createQuery("reject", (builder, parameters) -> { | ||
367 | var literals = new ArrayList<Literal>(parameters.length + 1); | ||
368 | literals.add(invalidCandidate.call(parameters)); | ||
369 | for (var parameter : parameters) { | ||
370 | literals.add(PartialLiterals.candidateMust(ReasoningAdapter.EXISTS_SYMBOL.call(parameter))); | ||
371 | } | ||
372 | builder.clause(literals); | ||
373 | }); | ||
374 | if (!acceptWasSet) { | ||
375 | accept = Criteria.whenNoMatch(reject); | ||
376 | } | ||
377 | if (!objectiveWasSet) { | ||
378 | objective = Objectives.count(reject); | ||
379 | } | ||
380 | } | ||
381 | |||
382 | public PartialRelationRewriter getRewriter() { | ||
383 | checkConfigured(); | ||
384 | return rewriter; | ||
385 | } | ||
386 | |||
387 | public static PartialRelationTranslator of(PartialRelation relation) { | ||
388 | return new PartialRelationTranslator(relation); | ||
389 | } | ||
390 | } | ||