aboutsummaryrefslogtreecommitdiffstats
path: root/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/internal
diff options
context:
space:
mode:
Diffstat (limited to 'subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/internal')
-rw-r--r--subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/internal/PartialClauseRewriter.java223
-rw-r--r--subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/internal/PartialQueryRewriter.java53
-rw-r--r--subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/internal/ReasoningAdapterImpl.java186
-rw-r--r--subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/internal/ReasoningBuilderImpl.java153
-rw-r--r--subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/internal/ReasoningStoreAdapterImpl.java92
5 files changed, 687 insertions, 20 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
new file mode 100644
index 00000000..40993235
--- /dev/null
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/internal/PartialClauseRewriter.java
@@ -0,0 +1,223 @@
1/*
2 * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
3 *
4 * SPDX-License-Identifier: EPL-2.0
5 */
6package tools.refinery.store.reasoning.internal;
7
8import tools.refinery.store.query.Constraint;
9import tools.refinery.store.query.dnf.Dnf;
10import tools.refinery.store.query.dnf.DnfBuilder;
11import tools.refinery.store.query.dnf.DnfClause;
12import tools.refinery.store.query.literal.AbstractCallLiteral;
13import tools.refinery.store.query.literal.AbstractCountLiteral;
14import tools.refinery.store.query.literal.CallPolarity;
15import tools.refinery.store.query.literal.Literal;
16import tools.refinery.store.query.term.Aggregator;
17import tools.refinery.store.query.term.ConstantTerm;
18import tools.refinery.store.query.term.Term;
19import tools.refinery.store.query.term.Variable;
20import tools.refinery.store.query.term.int_.IntTerms;
21import tools.refinery.store.query.term.uppercardinality.UpperCardinalityTerms;
22import tools.refinery.store.reasoning.ReasoningAdapter;
23import tools.refinery.store.reasoning.literal.*;
24import tools.refinery.store.reasoning.representation.PartialRelation;
25import tools.refinery.store.reasoning.translator.multiobject.MultiObjectTranslator;
26import tools.refinery.store.representation.cardinality.UpperCardinalities;
27
28import java.util.*;
29import java.util.function.BinaryOperator;
30
31class PartialClauseRewriter {
32 private final PartialQueryRewriter rewriter;
33 private final List<Literal> completedLiterals = new ArrayList<>();
34 private final Deque<Literal> workList = new ArrayDeque<>();
35 private final Set<Variable> positiveVariables = new LinkedHashSet<>();
36 private final Set<Variable> unmodifiablePositiveVariables = Collections.unmodifiableSet(positiveVariables);
37
38 public PartialClauseRewriter(PartialQueryRewriter rewriter) {
39 this.rewriter = rewriter;
40 }
41
42 public List<Literal> rewriteClause(DnfClause clause) {
43 workList.addAll(clause.literals());
44 while (!workList.isEmpty()) {
45 var literal = workList.removeFirst();
46 rewrite(literal);
47 }
48 return completedLiterals;
49 }
50
51 private void rewrite(Literal literal) {
52 if (!(literal instanceof AbstractCallLiteral callLiteral)) {
53 markAsDone(literal);
54 return;
55 }
56 if (callLiteral instanceof CountLowerBoundLiteral countLowerBoundLiteral) {
57 rewriteCountLowerBound(countLowerBoundLiteral);
58 return;
59 }
60 if (callLiteral instanceof CountUpperBoundLiteral countUpperBoundLiteral) {
61 rewriteCountUpperBound(countUpperBoundLiteral);
62 return;
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 }
72 var target = callLiteral.getTarget();
73 if (target instanceof Dnf dnf) {
74 rewriteRecursively(callLiteral, dnf);
75 } else if (target instanceof ModalConstraint modalConstraint) {
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 }
86 } else {
87 markAsDone(literal);
88 }
89 }
90
91 private void rewriteCountLowerBound(CountLowerBoundLiteral literal) {
92 rewritePartialCount(literal, "lower", Modality.MUST, MultiObjectTranslator.LOWER_CARDINALITY_VIEW, 1,
93 IntTerms::mul, IntTerms.INT_SUM);
94 }
95
96 private void rewriteCountUpperBound(CountUpperBoundLiteral literal) {
97 rewritePartialCount(literal, "upper", Modality.MAY, MultiObjectTranslator.UPPER_CARDINALITY_VIEW,
98 UpperCardinalities.ONE, UpperCardinalityTerms::mul, UpperCardinalityTerms.UPPER_CARDINALITY_SUM);
99 }
100
101 private <T> void rewritePartialCount(AbstractCountLiteral<T> literal, String name, Modality modality,
102 Constraint view, T one, BinaryOperator<Term<T>> mul, Aggregator<T, T> sum) {
103 var type = literal.getResultType();
104 var countResult = computeCountVariables(literal, Concreteness.PARTIAL, name);
105 var builder = countResult.builder();
106 var outputVariable = builder.parameter(type);
107 var variablesToCount = countResult.variablesToCount();
108
109 var literals = new ArrayList<Literal>();
110 literals.add(new ModalConstraint(modality, Concreteness.PARTIAL, literal.getTarget())
111 .call(CallPolarity.POSITIVE, countResult.rewrittenArguments()));
112 switch (variablesToCount.size()) {
113 case 0 -> literals.add(outputVariable.assign(new ConstantTerm<>(type, one)));
114 case 1 -> literals.add(view.call(variablesToCount.get(0),
115 outputVariable));
116 default -> {
117 var firstCount = Variable.of(type);
118 literals.add(view.call(variablesToCount.get(0), firstCount));
119 int length = variablesToCount.size();
120 Term<T> accumulator = firstCount;
121 for (int i = 1; i < length; i++) {
122 var countVariable = Variable.of(type);
123 literals.add(view.call(variablesToCount.get(i), countVariable));
124 accumulator = mul.apply(accumulator, countVariable);
125 }
126 literals.add(outputVariable.assign(accumulator));
127 }
128 }
129 builder.clause(literals);
130
131 var helperQuery = builder.build();
132 var aggregationVariable = Variable.of(type);
133 var helperArguments = countResult.helperArguments();
134 helperArguments.add(aggregationVariable);
135 workList.addFirst(literal.getResultVariable().assign(helperQuery.aggregateBy(aggregationVariable, sum,
136 helperArguments)));
137 }
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
192 private void markAsDone(Literal literal) {
193 completedLiterals.add(literal);
194 positiveVariables.addAll(literal.getOutputVariables());
195 }
196
197 private void rewriteRecursively(AbstractCallLiteral callLiteral, Modality modality, Concreteness concreteness,
198 Dnf dnf) {
199 var liftedDnf = rewriter.getLifter().lift(modality, concreteness, dnf);
200 rewriteRecursively(callLiteral, liftedDnf);
201 }
202
203 private void rewriteRecursively(AbstractCallLiteral callLiteral, Dnf dnf) {
204 var rewrittenDnf = rewriter.rewrite(dnf);
205 var rewrittenLiteral = callLiteral.withTarget(rewrittenDnf);
206 markAsDone(rewrittenLiteral);
207 }
208
209 private void rewrite(AbstractCallLiteral callLiteral, Modality modality, Concreteness concreteness,
210 PartialRelation partialRelation) {
211 var relationRewriter = rewriter.getRelationRewriter(partialRelation);
212 var literals = relationRewriter.rewriteLiteral(
213 unmodifiablePositiveVariables, callLiteral, modality, concreteness);
214 int length = literals.size();
215 for (int i = length - 1; i >= 0; i--) {
216 workList.addFirst(literals.get(i));
217 }
218 }
219
220 private record CountResult(DnfBuilder builder, List<Variable> rewrittenArguments, List<Variable> helperArguments,
221 List<Variable> variablesToCount) {
222 }
223}
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/internal/PartialQueryRewriter.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/internal/PartialQueryRewriter.java
new file mode 100644
index 00000000..79cba263
--- /dev/null
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/internal/PartialQueryRewriter.java
@@ -0,0 +1,53 @@
1/*
2 * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
3 *
4 * SPDX-License-Identifier: EPL-2.0
5 */
6package tools.refinery.store.reasoning.internal;
7
8import tools.refinery.store.query.dnf.Dnf;
9import tools.refinery.store.query.rewriter.AbstractRecursiveRewriter;
10import tools.refinery.store.reasoning.interpretation.PartialRelationRewriter;
11import tools.refinery.store.reasoning.lifting.DnfLifter;
12import tools.refinery.store.reasoning.representation.PartialRelation;
13
14import java.util.HashMap;
15import java.util.Map;
16
17class PartialQueryRewriter extends AbstractRecursiveRewriter {
18 private final DnfLifter lifter;
19 private final Map<PartialRelation, PartialRelationRewriter> relationRewriterMap = new HashMap<>();
20
21 PartialQueryRewriter(DnfLifter lifter) {
22 this.lifter = lifter;
23 }
24
25 DnfLifter getLifter() {
26 return lifter;
27 }
28
29 PartialRelationRewriter getRelationRewriter(PartialRelation partialRelation) {
30 var rewriter = relationRewriterMap.get(partialRelation);
31 if (rewriter == null) {
32 throw new IllegalArgumentException("Do not know how to interpret partial relation: " + partialRelation);
33 }
34 return rewriter;
35 }
36
37 public void addRelationRewriter(PartialRelation partialRelation, PartialRelationRewriter interpreter) {
38 if (relationRewriterMap.put(partialRelation, interpreter) != null) {
39 throw new IllegalArgumentException("Duplicate partial relation: " + partialRelation);
40 }
41 }
42
43 @Override
44 protected Dnf doRewrite(Dnf dnf) {
45 var builder = Dnf.builderFrom(dnf);
46 for (var clause : dnf.getClauses()) {
47 var clauseRewriter = new PartialClauseRewriter(this);
48 var rewrittenClauses = clauseRewriter.rewriteClause(clause);
49 builder.clause(rewrittenClauses);
50 }
51 return builder.build();
52 }
53}
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/internal/ReasoningAdapterImpl.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/internal/ReasoningAdapterImpl.java
index 1bd3ad2e..bd16bdfa 100644
--- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/internal/ReasoningAdapterImpl.java
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/internal/ReasoningAdapterImpl.java
@@ -5,20 +5,114 @@
5 */ 5 */
6package tools.refinery.store.reasoning.internal; 6package tools.refinery.store.reasoning.internal;
7 7
8import org.jetbrains.annotations.Nullable;
9import tools.refinery.store.model.Interpretation;
8import tools.refinery.store.model.Model; 10import tools.refinery.store.model.Model;
9import tools.refinery.store.reasoning.ReasoningAdapter; 11import tools.refinery.store.reasoning.ReasoningAdapter;
10import tools.refinery.store.reasoning.PartialInterpretation; 12import tools.refinery.store.reasoning.interpretation.AnyPartialInterpretation;
13import tools.refinery.store.reasoning.interpretation.PartialInterpretation;
14import tools.refinery.store.reasoning.literal.Concreteness;
15import tools.refinery.store.reasoning.refinement.AnyPartialInterpretationRefiner;
16import tools.refinery.store.reasoning.refinement.PartialInterpretationRefiner;
17import tools.refinery.store.reasoning.refinement.StorageRefiner;
18import tools.refinery.store.reasoning.representation.AnyPartialSymbol;
11import tools.refinery.store.reasoning.representation.PartialSymbol; 19import tools.refinery.store.reasoning.representation.PartialSymbol;
12import tools.refinery.store.query.dnf.Dnf; 20import tools.refinery.store.reasoning.translator.multiobject.MultiObjectTranslator;
13import tools.refinery.store.query.resultset.ResultSet; 21import tools.refinery.store.representation.Symbol;
22import tools.refinery.store.representation.cardinality.CardinalityInterval;
23import tools.refinery.store.representation.cardinality.CardinalityIntervals;
24import tools.refinery.store.tuple.Tuple;
25import tools.refinery.store.tuple.Tuple1;
14 26
15public class ReasoningAdapterImpl implements ReasoningAdapter { 27import java.util.HashMap;
28import java.util.Map;
29
30class ReasoningAdapterImpl implements ReasoningAdapter {
31 static final Symbol<Integer> NODE_COUNT_SYMBOL = Symbol.of("MODEL_SIZE", 0, Integer.class, 0);
16 private final Model model; 32 private final Model model;
17 private final ReasoningStoreAdapterImpl storeAdapter; 33 private final ReasoningStoreAdapterImpl storeAdapter;
34 private final Map<AnyPartialSymbol, AnyPartialInterpretation>[] partialInterpretations;
35 private final Map<AnyPartialSymbol, AnyPartialInterpretationRefiner> refiners;
36 private final StorageRefiner[] storageRefiners;
37 private final Interpretation<Integer> nodeCountInterpretation;
38 private final Interpretation<CardinalityInterval> countInterpretation;
18 39
19 ReasoningAdapterImpl(Model model, ReasoningStoreAdapterImpl storeAdapter) { 40 ReasoningAdapterImpl(Model model, ReasoningStoreAdapterImpl storeAdapter) {
20 this.model = model; 41 this.model = model;
21 this.storeAdapter = storeAdapter; 42 this.storeAdapter = storeAdapter;
43
44 int concretenessLength = Concreteness.values().length;
45 // Creation of a generic array.
46 @SuppressWarnings({"unchecked", "squid:S1905"})
47 var interpretationsArray = (Map<AnyPartialSymbol, AnyPartialInterpretation>[]) new Map[concretenessLength];
48 partialInterpretations = interpretationsArray;
49 createPartialInterpretations();
50
51 var refinerFactories = storeAdapter.getSymbolRefiners();
52 refiners = new HashMap<>(refinerFactories.size());
53 createRefiners();
54
55 storageRefiners = storeAdapter.createStorageRefiner(model);
56
57 nodeCountInterpretation = model.getInterpretation(NODE_COUNT_SYMBOL);
58 if (model.getStore().getSymbols().contains(MultiObjectTranslator.COUNT_STORAGE)) {
59 countInterpretation = model.getInterpretation(MultiObjectTranslator.COUNT_STORAGE);
60 } else {
61 countInterpretation = null;
62 }
63 }
64
65 private void createPartialInterpretations() {
66 var supportedInterpretations = storeAdapter.getSupportedInterpretations();
67 int concretenessLength = Concreteness.values().length;
68 var interpretationFactories = storeAdapter.getSymbolInterpreters();
69 for (int i = 0; i < concretenessLength; i++) {
70 var concreteness = Concreteness.values()[i];
71 if (supportedInterpretations.contains(concreteness)) {
72 partialInterpretations[i] = new HashMap<>(interpretationFactories.size());
73 }
74 }
75 // Create the partial interpretations in order so that factories may refer to interpretations of symbols
76 // preceding them in the ordered {@code interpretationFactories} map, e.g., for opposite interpretations.
77 for (var entry : interpretationFactories.entrySet()) {
78 var partialSymbol = entry.getKey();
79 var factory = entry.getValue();
80 for (int i = 0; i < concretenessLength; i++) {
81 if (partialInterpretations[i] != null) {
82 var concreteness = Concreteness.values()[i];
83 var interpretation = createPartialInterpretation(concreteness, factory, partialSymbol);
84 partialInterpretations[i].put(partialSymbol, interpretation);
85 }
86 }
87 }
88 }
89
90 private <A, C> PartialInterpretation<A, C> createPartialInterpretation(
91 Concreteness concreteness, PartialInterpretation.Factory<A, C> interpreter, AnyPartialSymbol symbol) {
92 // The builder only allows well-typed assignment of interpreters to symbols.
93 @SuppressWarnings("unchecked")
94 var typedSymbol = (PartialSymbol<A, C>) symbol;
95 return interpreter.create(this, concreteness, typedSymbol);
96 }
97
98 private void createRefiners() {
99 var refinerFactories = storeAdapter.getSymbolRefiners();
100 // Create the partial interpretations refiners in order so that factories may refer to refiners of symbols
101 // preceding them in the ordered {@code interpretationFactories} map, e.g., for opposite interpretations.
102 for (var entry : refinerFactories.entrySet()) {
103 var partialSymbol = entry.getKey();
104 var factory = entry.getValue();
105 var refiner = createRefiner(factory, partialSymbol);
106 refiners.put(partialSymbol, refiner);
107 }
108 }
109
110 private <A, C> PartialInterpretationRefiner<A, C> createRefiner(
111 PartialInterpretationRefiner.Factory<A, C> factory, AnyPartialSymbol symbol) {
112 // The builder only allows well-typed assignment of interpreters to symbols.
113 @SuppressWarnings("unchecked")
114 var typedSymbol = (PartialSymbol<A, C>) symbol;
115 return factory.create(this, typedSymbol);
22 } 116 }
23 117
24 @Override 118 @Override
@@ -32,12 +126,88 @@ public class ReasoningAdapterImpl implements ReasoningAdapter {
32 } 126 }
33 127
34 @Override 128 @Override
35 public <A, C> PartialInterpretation<A, C> getPartialInterpretation(PartialSymbol<A, C> partialSymbol) { 129 public <A, C> PartialInterpretation<A, C> getPartialInterpretation(Concreteness concreteness,
36 return null; 130 PartialSymbol<A, C> partialSymbol) {
131 var map = partialInterpretations[concreteness.ordinal()];
132 if (map == null) {
133 throw new IllegalArgumentException("No interpretation for concreteness: " + concreteness);
134 }
135 var interpretation = map.get(partialSymbol);
136 if (interpretation == null) {
137 throw new IllegalArgumentException("No interpretation for partial symbol: " + partialSymbol);
138 }
139 // The builder only allows well-typed assignment of interpreters to symbols.
140 @SuppressWarnings("unchecked")
141 var typedInterpretation = (PartialInterpretation<A, C>) interpretation;
142 return typedInterpretation;
143 }
144
145 @Override
146 public <A, C> PartialInterpretationRefiner<A, C> getRefiner(PartialSymbol<A, C> partialSymbol) {
147 var refiner = refiners.get(partialSymbol);
148 if (refiner == null) {
149 throw new IllegalArgumentException("No refiner for partial symbol: " + partialSymbol);
150 }
151 // The builder only allows well-typed assignment of refiners to symbols.
152 @SuppressWarnings("unchecked")
153 var typedRefiner = (PartialInterpretationRefiner<A, C>) refiner;
154 return typedRefiner;
155 }
156
157 @Override
158 @Nullable
159 public Tuple1 split(int parentNode) {
160 int newNodeId = nodeCountInterpretation.get(Tuple.of());
161 nodeCountInterpretation.put(Tuple.of(), newNodeId + 1);
162 // Avoid creating an iterator object.
163 //noinspection ForLoopReplaceableByForEach
164 for (int i = 0; i < storageRefiners.length; i++) {
165 if (!storageRefiners[i].split(parentNode, newNodeId)) {
166 return null;
167 }
168 }
169 return Tuple.of(newNodeId);
170 }
171
172 @Override
173 public @Nullable Tuple1 focus(int parentObject) {
174 if (countInterpretation == null) {
175 throw new IllegalStateException("Cannot focus without " + MultiObjectTranslator.class.getSimpleName());
176 }
177 var tuple = Tuple.of(parentObject);
178 var count = countInterpretation.get(tuple);
179 if (CardinalityIntervals.ONE.equals(count)) {
180 return tuple;
181 }
182 if (CardinalityIntervals.LONE.equals(count)) {
183 countInterpretation.put(tuple, CardinalityIntervals.ONE);
184 return tuple;
185 }
186 if (CardinalityIntervals.NONE.equals(count)) {
187 return null;
188 }
189 return split(parentObject);
190 }
191
192 @Override
193 public boolean cleanup(int nodeToDelete) {
194 // Avoid creating an iterator object.
195 //noinspection ForLoopReplaceableByForEach
196 for (int i = 0; i < storageRefiners.length; i++) {
197 if (!storageRefiners[i].cleanup(nodeToDelete)) {
198 return false;
199 }
200 }
201 int currentModelSize = nodeCountInterpretation.get(Tuple.of());
202 if (nodeToDelete == currentModelSize - 1) {
203 nodeCountInterpretation.put(Tuple.of(), nodeToDelete);
204 }
205 return true;
37 } 206 }
38 207
39 @Override 208 @Override
40 public ResultSet<Boolean> getLiftedResultSet(Dnf query) { 209 public int getNodeCount() {
41 return null; 210 Integer nodeCount = nodeCountInterpretation.get(Tuple.of());
211 return nodeCount == null ? 0 : nodeCount;
42 } 212 }
43} 213}
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/internal/ReasoningBuilderImpl.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/internal/ReasoningBuilderImpl.java
index aa71496c..722458c8 100644
--- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/internal/ReasoningBuilderImpl.java
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/internal/ReasoningBuilderImpl.java
@@ -6,26 +6,169 @@
6package tools.refinery.store.reasoning.internal; 6package tools.refinery.store.reasoning.internal;
7 7
8import tools.refinery.store.adapter.AbstractModelAdapterBuilder; 8import tools.refinery.store.adapter.AbstractModelAdapterBuilder;
9import tools.refinery.store.dse.transition.DesignSpaceExplorationBuilder;
10import tools.refinery.store.dse.transition.objectives.Objective;
11import tools.refinery.store.dse.transition.objectives.Objectives;
9import tools.refinery.store.model.ModelStore; 12import tools.refinery.store.model.ModelStore;
13import tools.refinery.store.model.ModelStoreBuilder;
14import tools.refinery.store.query.ModelQueryBuilder;
10import tools.refinery.store.query.dnf.Dnf; 15import tools.refinery.store.query.dnf.Dnf;
16import tools.refinery.store.query.dnf.FunctionalQuery;
17import tools.refinery.store.query.dnf.Query;
18import tools.refinery.store.query.dnf.RelationalQuery;
11import tools.refinery.store.reasoning.ReasoningBuilder; 19import tools.refinery.store.reasoning.ReasoningBuilder;
20import tools.refinery.store.reasoning.interpretation.PartialInterpretation;
21import tools.refinery.store.reasoning.lifting.DnfLifter;
22import tools.refinery.store.reasoning.literal.Concreteness;
12import tools.refinery.store.reasoning.literal.Modality; 23import tools.refinery.store.reasoning.literal.Modality;
24import tools.refinery.store.reasoning.refinement.DefaultStorageRefiner;
25import tools.refinery.store.reasoning.refinement.PartialInterpretationRefiner;
26import tools.refinery.store.reasoning.refinement.PartialModelInitializer;
27import tools.refinery.store.reasoning.refinement.StorageRefiner;
28import tools.refinery.store.reasoning.representation.AnyPartialSymbol;
29import tools.refinery.store.reasoning.translator.AnyPartialSymbolTranslator;
30import tools.refinery.store.reasoning.translator.PartialRelationTranslator;
31import tools.refinery.store.representation.AnySymbol;
32import tools.refinery.store.representation.Symbol;
33import tools.refinery.store.statecoding.StateCoderBuilder;
34
35import java.util.*;
13 36
14public class ReasoningBuilderImpl extends AbstractModelAdapterBuilder<ReasoningStoreAdapterImpl> 37public class ReasoningBuilderImpl extends AbstractModelAdapterBuilder<ReasoningStoreAdapterImpl>
15 implements ReasoningBuilder { 38 implements ReasoningBuilder {
39 private final DnfLifter lifter = new DnfLifter();
40 private final PartialQueryRewriter queryRewriter = new PartialQueryRewriter(lifter);
41 private Set<Concreteness> requiredInterpretations = Set.of(Concreteness.values());
42 private final Map<AnyPartialSymbol, AnyPartialSymbolTranslator> translators = new LinkedHashMap<>();
43 private final Map<AnyPartialSymbol, PartialInterpretation.Factory<?, ?>> symbolInterpreters =
44 new LinkedHashMap<>();
45 private final Map<AnyPartialSymbol, PartialInterpretationRefiner.Factory<?, ?>> symbolRefiners =
46 new LinkedHashMap<>();
47 private final Map<AnySymbol, StorageRefiner.Factory<?>> registeredStorageRefiners = new LinkedHashMap<>();
48 private final List<PartialModelInitializer> initializers = new ArrayList<>();
49 private final List<Objective> objectives = new ArrayList<>();
50
51 @Override
52 public ReasoningBuilder requiredInterpretations(Collection<Concreteness> requiredInterpretations) {
53 this.requiredInterpretations = Set.copyOf(requiredInterpretations);
54 return this;
55 }
56
57 @Override
58 public ReasoningBuilder partialSymbol(AnyPartialSymbolTranslator translator) {
59 var partialSymbol = translator.getPartialSymbol();
60 var oldConfiguration = translators.put(partialSymbol, translator);
61 if (oldConfiguration != null && oldConfiguration != translator) {
62 throw new IllegalArgumentException("Duplicate configuration for symbol: " + partialSymbol);
63 }
64 return this;
65 }
66
16 @Override 67 @Override
17 public ReasoningBuilder liftedQuery(Dnf liftedQuery) { 68 public <T> ReasoningBuilder storageRefiner(Symbol<T> symbol, StorageRefiner.Factory<T> refiner) {
18 return null; 69 checkNotConfigured();
70 if (registeredStorageRefiners.put(symbol, refiner) != null) {
71 throw new IllegalArgumentException("Duplicate representation refiner for symbol: " + symbol);
72 }
73 return this;
74 }
75
76 @Override
77 public ReasoningBuilder initializer(PartialModelInitializer initializer) {
78 checkNotConfigured();
79 initializers.add(initializer);
80 return this;
19 } 81 }
20 82
21 @Override 83 @Override
22 public Dnf lift(Modality modality, Dnf query) { 84 public ReasoningBuilder objective(Objective objective) {
23 checkNotConfigured(); 85 checkNotConfigured();
24 return null; 86 objectives.add(objective);
87 return this;
88 }
89
90 @Override
91 public <T> Query<T> lift(Modality modality, Concreteness concreteness, Query<T> query) {
92 return lifter.lift(modality, concreteness, query);
93 }
94
95 @Override
96 public RelationalQuery lift(Modality modality, Concreteness concreteness, RelationalQuery query) {
97 return lifter.lift(modality, concreteness, query);
98 }
99
100 @Override
101 public <T> FunctionalQuery<T> lift(Modality modality, Concreteness concreteness, FunctionalQuery<T> query) {
102 return lifter.lift(modality, concreteness, query);
103 }
104
105 @Override
106 public Dnf lift(Modality modality, Concreteness concreteness, Dnf dnf) {
107 return lifter.lift(modality, concreteness, dnf);
108 }
109
110 @Override
111 protected void doConfigure(ModelStoreBuilder storeBuilder) {
112 storeBuilder.symbols(ReasoningAdapterImpl.NODE_COUNT_SYMBOL);
113 storeBuilder.tryGetAdapter(StateCoderBuilder.class)
114 .ifPresent(stateCoderBuilder -> stateCoderBuilder.exclude(ReasoningAdapterImpl.NODE_COUNT_SYMBOL));
115 for (var translator : translators.values()) {
116 translator.configure(storeBuilder);
117 if (translator instanceof PartialRelationTranslator relationConfiguration) {
118 doConfigure(storeBuilder, relationConfiguration);
119 } else {
120 throw new IllegalArgumentException("Unknown partial symbol translator %s for partial symbol %s"
121 .formatted(translator, translator.getPartialSymbol()));
122 }
123 }
124 storeBuilder.symbols(registeredStorageRefiners.keySet());
125 var queryBuilder = storeBuilder.getAdapter(ModelQueryBuilder.class);
126 queryBuilder.rewriter(queryRewriter);
127 if (!objectives.isEmpty()) {
128 storeBuilder.tryGetAdapter(DesignSpaceExplorationBuilder.class)
129 .ifPresent(dseBuilder -> dseBuilder.objective(Objectives.sum(objectives)));
130 }
131 }
132
133 private void doConfigure(ModelStoreBuilder storeBuilder, PartialRelationTranslator relationConfiguration) {
134 var partialRelation = relationConfiguration.getPartialRelation();
135 queryRewriter.addRelationRewriter(partialRelation, relationConfiguration.getRewriter());
136 var interpretationFactory = relationConfiguration.getInterpretationFactory();
137 interpretationFactory.configure(storeBuilder, requiredInterpretations);
138 symbolInterpreters.put(partialRelation, interpretationFactory);
139 var refiner = relationConfiguration.getInterpretationRefiner();
140 if (refiner != null) {
141 symbolRefiners.put(partialRelation, refiner);
142 }
25 } 143 }
26 144
27 @Override 145 @Override
28 public ReasoningStoreAdapterImpl doBuild(ModelStore store) { 146 public ReasoningStoreAdapterImpl doBuild(ModelStore store) {
29 return null; 147 return new ReasoningStoreAdapterImpl(store, requiredInterpretations,
148 Collections.unmodifiableMap(symbolInterpreters), Collections.unmodifiableMap(symbolRefiners),
149 getStorageRefiners(store), Collections.unmodifiableList(initializers));
150 }
151
152 private Map<AnySymbol, StorageRefiner.Factory<?>> getStorageRefiners(ModelStore store) {
153 var symbols = store.getSymbols();
154 var storageRefiners = new LinkedHashMap<AnySymbol, StorageRefiner.Factory<?>>(symbols.size());
155 for (var symbol : symbols) {
156 var refiner = registeredStorageRefiners.remove(symbol);
157 if (refiner == null) {
158 if (symbol.arity() == 0) {
159 // Arity-0 symbols don't need a default refiner, because they are unaffected by object
160 // creation/removal. Only a custom refiner ({@code refiner != null}) might need to update them.
161 continue;
162 }
163 // By default, copy over all affected tuples on object creation and remove all affected tuples on
164 // object removal.
165 refiner = DefaultStorageRefiner.factory();
166 }
167 storageRefiners.put(symbol, refiner);
168 }
169 if (!registeredStorageRefiners.isEmpty()) {
170 throw new IllegalArgumentException("Unused storage refiners: " + registeredStorageRefiners.keySet());
171 }
172 return Collections.unmodifiableMap(storageRefiners);
30 } 173 }
31} 174}
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/internal/ReasoningStoreAdapterImpl.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/internal/ReasoningStoreAdapterImpl.java
index cdddd8d6..9ef6fb16 100644
--- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/internal/ReasoningStoreAdapterImpl.java
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/internal/ReasoningStoreAdapterImpl.java
@@ -5,19 +5,46 @@
5 */ 5 */
6package tools.refinery.store.reasoning.internal; 6package tools.refinery.store.reasoning.internal;
7 7
8import tools.refinery.store.reasoning.ReasoningStoreAdapter; 8import tools.refinery.store.dse.propagation.PropagationAdapter;
9import tools.refinery.store.model.Model; 9import tools.refinery.store.model.Model;
10import tools.refinery.store.model.ModelStore; 10import tools.refinery.store.model.ModelStore;
11import tools.refinery.store.query.ModelQueryAdapter;
12import tools.refinery.store.reasoning.ReasoningStoreAdapter;
13import tools.refinery.store.reasoning.interpretation.PartialInterpretation;
14import tools.refinery.store.reasoning.literal.Concreteness;
15import tools.refinery.store.reasoning.refinement.PartialInterpretationRefiner;
16import tools.refinery.store.reasoning.refinement.PartialModelInitializer;
17import tools.refinery.store.reasoning.refinement.StorageRefiner;
11import tools.refinery.store.reasoning.representation.AnyPartialSymbol; 18import tools.refinery.store.reasoning.representation.AnyPartialSymbol;
12import tools.refinery.store.query.dnf.Dnf; 19import tools.refinery.store.reasoning.seed.ModelSeed;
20import tools.refinery.store.representation.AnySymbol;
21import tools.refinery.store.representation.Symbol;
22import tools.refinery.store.tuple.Tuple;
13 23
14import java.util.Collection; 24import java.util.Collection;
25import java.util.List;
26import java.util.Map;
27import java.util.Set;
15 28
16public class ReasoningStoreAdapterImpl implements ReasoningStoreAdapter { 29class ReasoningStoreAdapterImpl implements ReasoningStoreAdapter {
17 private final ModelStore store; 30 private final ModelStore store;
31 private final Set<Concreteness> supportedInterpretations;
32 private final Map<AnyPartialSymbol, PartialInterpretation.Factory<?, ?>> symbolInterpreters;
33 private final Map<AnyPartialSymbol, PartialInterpretationRefiner.Factory<?, ?>> symbolRefiners;
34 private final Map<AnySymbol, StorageRefiner.Factory<?>> storageRefiners;
35 private final List<PartialModelInitializer> initializers;
18 36
19 ReasoningStoreAdapterImpl(ModelStore store) { 37 ReasoningStoreAdapterImpl(ModelStore store, Set<Concreteness> supportedInterpretations,
38 Map<AnyPartialSymbol, PartialInterpretation.Factory<?, ?>> symbolInterpreters,
39 Map<AnyPartialSymbol, PartialInterpretationRefiner.Factory<?, ?>> symbolRefiners,
40 Map<AnySymbol, StorageRefiner.Factory<?>> storageRefiners,
41 List<PartialModelInitializer> initializers) {
20 this.store = store; 42 this.store = store;
43 this.supportedInterpretations = supportedInterpretations;
44 this.symbolInterpreters = symbolInterpreters;
45 this.symbolRefiners = symbolRefiners;
46 this.storageRefiners = storageRefiners;
47 this.initializers = initializers;
21 } 48 }
22 49
23 @Override 50 @Override
@@ -26,13 +53,64 @@ public class ReasoningStoreAdapterImpl implements ReasoningStoreAdapter {
26 } 53 }
27 54
28 @Override 55 @Override
56 public Set<Concreteness> getSupportedInterpretations() {
57 return supportedInterpretations;
58 }
59
60 @Override
29 public Collection<AnyPartialSymbol> getPartialSymbols() { 61 public Collection<AnyPartialSymbol> getPartialSymbols() {
30 return null; 62 return symbolInterpreters.keySet();
31 } 63 }
32 64
33 @Override 65 @Override
34 public Collection<Dnf> getLiftedQueries() { 66 public Collection<AnyPartialSymbol> getRefinablePartialSymbols() {
35 return null; 67 return symbolRefiners.keySet();
68 }
69
70 // Use of wildcard return value only in internal method not exposed as API, so there is less chance of confusion.
71 @SuppressWarnings("squid:S1452")
72 Map<AnyPartialSymbol, PartialInterpretation.Factory<?, ?>> getSymbolInterpreters() {
73 return symbolInterpreters;
74 }
75
76 // Use of wildcard return value only in internal method not exposed as API, so there is less chance of confusion.
77 @SuppressWarnings("squid:S1452")
78 Map<AnyPartialSymbol, PartialInterpretationRefiner.Factory<?, ?>> getSymbolRefiners() {
79 return symbolRefiners;
80 }
81
82 StorageRefiner[] createStorageRefiner(Model model) {
83 var refiners = new StorageRefiner[storageRefiners.size()];
84 int i = 0;
85 for (var entry : storageRefiners.entrySet()) {
86 var symbol = entry.getKey();
87 var factory = entry.getValue();
88 refiners[i] = createStorageRefiner(factory, model, symbol);
89 i++;
90 }
91 return refiners;
92 }
93
94 private <T> StorageRefiner createStorageRefiner(StorageRefiner.Factory<T> factory, Model model, AnySymbol symbol) {
95 // The builder only allows well-typed assignment of refiners to symbols.
96 @SuppressWarnings("unchecked")
97 var typedSymbol = (Symbol<T>) symbol;
98 return factory.create(typedSymbol, model);
99 }
100
101 public Model createInitialModel(ModelSeed modelSeed) {
102 var model = store.createEmptyModel();
103 model.getInterpretation(ReasoningAdapterImpl.NODE_COUNT_SYMBOL).put(Tuple.of(), modelSeed.getNodeCount());
104 for (var initializer : initializers) {
105 initializer.initialize(model, modelSeed);
106 }
107 model.tryGetAdapter(PropagationAdapter.class).ifPresent(propagationAdapter -> {
108 if (propagationAdapter.propagate().isRejected()) {
109 throw new IllegalArgumentException("Inconsistent initial mode: propagation failed");
110 }
111 });
112 model.getAdapter(ModelQueryAdapter.class).flushChanges();
113 return model;
36 } 114 }
37 115
38 @Override 116 @Override
generated by cgit v1.2.3-54-g00ecf (git 2.45.2) at 2024-06-28 17:07:02 +0000