diff options
Diffstat (limited to 'subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiobject/MultiObjectInitializer.java')
-rw-r--r-- | subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiobject/MultiObjectInitializer.java | 135 |
1 files changed, 135 insertions, 0 deletions
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiobject/MultiObjectInitializer.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiobject/MultiObjectInitializer.java new file mode 100644 index 00000000..89918155 --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiobject/MultiObjectInitializer.java | |||
@@ -0,0 +1,135 @@ | |||
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.multiobject; | ||
7 | |||
8 | import org.jetbrains.annotations.NotNull; | ||
9 | import tools.refinery.store.model.Model; | ||
10 | import tools.refinery.store.reasoning.ReasoningAdapter; | ||
11 | import tools.refinery.store.reasoning.refinement.PartialModelInitializer; | ||
12 | import tools.refinery.store.reasoning.seed.ModelSeed; | ||
13 | import tools.refinery.store.reasoning.translator.TranslationException; | ||
14 | import tools.refinery.store.representation.Symbol; | ||
15 | import tools.refinery.store.representation.TruthValue; | ||
16 | import tools.refinery.store.representation.cardinality.CardinalityInterval; | ||
17 | import tools.refinery.store.representation.cardinality.CardinalityIntervals; | ||
18 | import tools.refinery.store.tuple.Tuple; | ||
19 | |||
20 | import java.util.Arrays; | ||
21 | import java.util.HashMap; | ||
22 | import java.util.function.Function; | ||
23 | |||
24 | class MultiObjectInitializer implements PartialModelInitializer { | ||
25 | private final Symbol<CardinalityInterval> countSymbol; | ||
26 | |||
27 | public MultiObjectInitializer(Symbol<CardinalityInterval> countSymbol) { | ||
28 | this.countSymbol = countSymbol; | ||
29 | } | ||
30 | |||
31 | @Override | ||
32 | public void initialize(Model model, ModelSeed modelSeed) { | ||
33 | var intervals = initializeIntervals(model, modelSeed); | ||
34 | initializeExists(intervals, model, modelSeed); | ||
35 | initializeEquals(intervals, model, modelSeed); | ||
36 | var countInterpretation = model.getInterpretation(countSymbol); | ||
37 | var uniqueTable = new HashMap<CardinalityInterval, CardinalityInterval>(); | ||
38 | for (int i = 0; i < intervals.length; i++) { | ||
39 | var interval = intervals[i]; | ||
40 | if (interval.isEmpty()) { | ||
41 | throw new TranslationException(ReasoningAdapter.EXISTS_SYMBOL, | ||
42 | "Inconsistent existence or equality for node " + i); | ||
43 | } | ||
44 | var uniqueInterval = uniqueTable.computeIfAbsent(intervals[i], Function.identity()); | ||
45 | countInterpretation.put(Tuple.of(i), uniqueInterval); | ||
46 | } | ||
47 | } | ||
48 | |||
49 | @NotNull | ||
50 | private CardinalityInterval[] initializeIntervals(Model model, ModelSeed modelSeed) { | ||
51 | var intervals = new CardinalityInterval[modelSeed.getNodeCount()]; | ||
52 | if (modelSeed.containsSeed(MultiObjectTranslator.COUNT_SYMBOL)) { | ||
53 | Arrays.fill(intervals, CardinalityIntervals.ONE); | ||
54 | var cursor = modelSeed.getCursor(MultiObjectTranslator.COUNT_SYMBOL, CardinalityIntervals.ONE); | ||
55 | while (cursor.move()) { | ||
56 | model.checkCancelled(); | ||
57 | int i = cursor.getKey().get(0); | ||
58 | checkNodeId(intervals, i); | ||
59 | intervals[i] = cursor.getValue(); | ||
60 | } | ||
61 | } else { | ||
62 | Arrays.fill(intervals, CardinalityIntervals.SET); | ||
63 | if (!modelSeed.containsSeed(ReasoningAdapter.EXISTS_SYMBOL) || | ||
64 | !modelSeed.containsSeed(ReasoningAdapter.EQUALS_SYMBOL)) { | ||
65 | throw new TranslationException(MultiObjectTranslator.COUNT_SYMBOL, | ||
66 | "Seed for %s and %s is required if there is no seed for %s".formatted( | ||
67 | ReasoningAdapter.EXISTS_SYMBOL, ReasoningAdapter.EQUALS_SYMBOL, | ||
68 | MultiObjectTranslator.COUNT_SYMBOL)); | ||
69 | } | ||
70 | } | ||
71 | return intervals; | ||
72 | } | ||
73 | |||
74 | private void initializeExists(CardinalityInterval[] intervals, Model model, ModelSeed modelSeed) { | ||
75 | if (!modelSeed.containsSeed(ReasoningAdapter.EXISTS_SYMBOL)) { | ||
76 | return; | ||
77 | } | ||
78 | var cursor = modelSeed.getCursor(ReasoningAdapter.EXISTS_SYMBOL, TruthValue.UNKNOWN); | ||
79 | while (cursor.move()) { | ||
80 | model.checkCancelled(); | ||
81 | int i = cursor.getKey().get(0); | ||
82 | checkNodeId(intervals, i); | ||
83 | switch (cursor.getValue()) { | ||
84 | case TRUE -> intervals[i] = intervals[i].meet(CardinalityIntervals.SOME); | ||
85 | case FALSE -> intervals[i] = intervals[i].meet(CardinalityIntervals.NONE); | ||
86 | case ERROR -> throw new TranslationException(ReasoningAdapter.EXISTS_SYMBOL, | ||
87 | "Inconsistent existence for node " + i); | ||
88 | default -> throw new TranslationException(ReasoningAdapter.EXISTS_SYMBOL, | ||
89 | "Invalid existence truth value %s for node %d".formatted(cursor.getValue(), i)); | ||
90 | } | ||
91 | } | ||
92 | } | ||
93 | |||
94 | private void initializeEquals(CardinalityInterval[] intervals, Model model, ModelSeed modelSeed) { | ||
95 | if (!modelSeed.containsSeed(ReasoningAdapter.EQUALS_SYMBOL)) { | ||
96 | return; | ||
97 | } | ||
98 | var seed = modelSeed.getSeed(ReasoningAdapter.EQUALS_SYMBOL); | ||
99 | var cursor = seed.getCursor(TruthValue.FALSE, modelSeed.getNodeCount()); | ||
100 | while (cursor.move()) { | ||
101 | model.checkCancelled(); | ||
102 | var key = cursor.getKey(); | ||
103 | int i = key.get(0); | ||
104 | int otherIndex = key.get(1); | ||
105 | if (i != otherIndex) { | ||
106 | throw new TranslationException(ReasoningAdapter.EQUALS_SYMBOL, | ||
107 | "Off-diagonal equivalence (%d, %d) is not permitted".formatted(i, otherIndex)); | ||
108 | } | ||
109 | checkNodeId(intervals, i); | ||
110 | switch (cursor.getValue()) { | ||
111 | case TRUE -> intervals[i] = intervals[i].meet(CardinalityIntervals.LONE); | ||
112 | case UNKNOWN -> { | ||
113 | // Nothing do to, {@code intervals} is initialized with unknown equality. | ||
114 | } | ||
115 | case ERROR -> throw new TranslationException(ReasoningAdapter.EQUALS_SYMBOL, | ||
116 | "Inconsistent equality for node " + i); | ||
117 | default -> throw new TranslationException(ReasoningAdapter.EQUALS_SYMBOL, | ||
118 | "Invalid equality truth value %s for node %d".formatted(cursor.getValue(), i)); | ||
119 | } | ||
120 | } | ||
121 | for (int i = 0; i < intervals.length; i++) { | ||
122 | model.checkCancelled(); | ||
123 | if (seed.get(Tuple.of(i, i)) == TruthValue.FALSE) { | ||
124 | throw new TranslationException(ReasoningAdapter.EQUALS_SYMBOL, "Inconsistent equality for node " + i); | ||
125 | } | ||
126 | } | ||
127 | } | ||
128 | |||
129 | private void checkNodeId(CardinalityInterval[] intervals, int nodeId) { | ||
130 | if (nodeId < 0 || nodeId >= intervals.length) { | ||
131 | throw new IllegalArgumentException("Expected node id %d to be lower than model size %d" | ||
132 | .formatted(nodeId, intervals.length)); | ||
133 | } | ||
134 | } | ||
135 | } | ||