diff options
Diffstat (limited to 'subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope')
6 files changed, 584 insertions, 0 deletions
diff --git a/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/BoundScopePropagator.java b/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/BoundScopePropagator.java new file mode 100644 index 00000000..ecca6117 --- /dev/null +++ b/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/BoundScopePropagator.java | |||
@@ -0,0 +1,240 @@ | |||
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.scope; | ||
7 | |||
8 | import com.google.ortools.linearsolver.MPConstraint; | ||
9 | import com.google.ortools.linearsolver.MPObjective; | ||
10 | import com.google.ortools.linearsolver.MPSolver; | ||
11 | import com.google.ortools.linearsolver.MPVariable; | ||
12 | import org.eclipse.collections.api.factory.primitive.IntObjectMaps; | ||
13 | import org.eclipse.collections.api.factory.primitive.IntSets; | ||
14 | import org.eclipse.collections.api.map.primitive.MutableIntObjectMap; | ||
15 | import org.eclipse.collections.api.set.primitive.MutableIntSet; | ||
16 | import tools.refinery.store.dse.propagation.BoundPropagator; | ||
17 | import tools.refinery.store.dse.propagation.PropagationResult; | ||
18 | import tools.refinery.store.model.Interpretation; | ||
19 | import tools.refinery.store.model.Model; | ||
20 | import tools.refinery.store.query.ModelQueryAdapter; | ||
21 | import tools.refinery.store.representation.cardinality.*; | ||
22 | import tools.refinery.store.tuple.Tuple; | ||
23 | |||
24 | class BoundScopePropagator implements BoundPropagator { | ||
25 | private final Model model; | ||
26 | private final ModelQueryAdapter queryEngine; | ||
27 | private final Interpretation<CardinalityInterval> countInterpretation; | ||
28 | private final MPSolver solver; | ||
29 | private final MPObjective objective; | ||
30 | private final MutableIntObjectMap<MPVariable> variables = IntObjectMaps.mutable.empty(); | ||
31 | private final MutableIntSet activeVariables = IntSets.mutable.empty(); | ||
32 | private final TypeScopePropagator[] propagators; | ||
33 | private boolean changed = true; | ||
34 | |||
35 | public BoundScopePropagator(Model model, ScopePropagator storeAdapter) { | ||
36 | this.model = model; | ||
37 | queryEngine = model.getAdapter(ModelQueryAdapter.class); | ||
38 | countInterpretation = model.getInterpretation(storeAdapter.getCountSymbol()); | ||
39 | solver = MPSolver.createSolver("GLOP"); | ||
40 | solver.suppressOutput(); | ||
41 | objective = solver.objective(); | ||
42 | initializeVariables(); | ||
43 | countInterpretation.addListener(this::countChanged, true); | ||
44 | var propagatorFactories = storeAdapter.getTypeScopePropagatorFactories(); | ||
45 | propagators = new TypeScopePropagator[propagatorFactories.size()]; | ||
46 | for (int i = 0; i < propagators.length; i++) { | ||
47 | model.checkCancelled(); | ||
48 | propagators[i] = propagatorFactories.get(i).createPropagator(this); | ||
49 | } | ||
50 | } | ||
51 | |||
52 | ModelQueryAdapter getQueryEngine() { | ||
53 | return queryEngine; | ||
54 | } | ||
55 | |||
56 | private void initializeVariables() { | ||
57 | var cursor = countInterpretation.getAll(); | ||
58 | while (cursor.move()) { | ||
59 | var interval = cursor.getValue(); | ||
60 | if (!interval.equals(CardinalityIntervals.ONE)) { | ||
61 | int nodeId = cursor.getKey().get(0); | ||
62 | createVariable(nodeId, interval); | ||
63 | activeVariables.add(nodeId); | ||
64 | } | ||
65 | } | ||
66 | } | ||
67 | |||
68 | private MPVariable createVariable(int nodeId, CardinalityInterval interval) { | ||
69 | double lowerBound = interval.lowerBound(); | ||
70 | double upperBound = getUpperBound(interval); | ||
71 | var variable = solver.makeNumVar(lowerBound, upperBound, "x" + nodeId); | ||
72 | variables.put(nodeId, variable); | ||
73 | return variable; | ||
74 | } | ||
75 | |||
76 | private void countChanged(Tuple key, CardinalityInterval fromValue, CardinalityInterval toValue, | ||
77 | boolean ignoredRestoring) { | ||
78 | int nodeId = key.get(0); | ||
79 | if ((toValue == null || toValue.equals(CardinalityIntervals.ONE))) { | ||
80 | if (fromValue != null && !fromValue.equals(CardinalityIntervals.ONE)) { | ||
81 | removeActiveVariable(toValue, nodeId); | ||
82 | } | ||
83 | return; | ||
84 | } | ||
85 | if (fromValue == null || fromValue.equals(CardinalityIntervals.ONE)) { | ||
86 | activeVariables.add(nodeId); | ||
87 | } | ||
88 | var variable = variables.get(nodeId); | ||
89 | if (variable == null) { | ||
90 | createVariable(nodeId, toValue); | ||
91 | markAsChanged(); | ||
92 | return; | ||
93 | } | ||
94 | double lowerBound = toValue.lowerBound(); | ||
95 | double upperBound = getUpperBound(toValue); | ||
96 | if (variable.lb() != lowerBound) { | ||
97 | variable.setLb(lowerBound); | ||
98 | markAsChanged(); | ||
99 | } | ||
100 | if (variable.ub() != upperBound) { | ||
101 | variable.setUb(upperBound); | ||
102 | markAsChanged(); | ||
103 | } | ||
104 | } | ||
105 | |||
106 | private void removeActiveVariable(CardinalityInterval toValue, int nodeId) { | ||
107 | var variable = variables.get(nodeId); | ||
108 | if (variable == null || !activeVariables.remove(nodeId)) { | ||
109 | throw new AssertionError("Variable not active: " + nodeId); | ||
110 | } | ||
111 | if (toValue == null) { | ||
112 | variable.setBounds(0, 0); | ||
113 | } else { | ||
114 | // Until queries are flushed and the constraints can be properly updated, | ||
115 | // the variable corresponding to the (previous) multi-object has to stand in for a single object. | ||
116 | variable.setBounds(1, 1); | ||
117 | } | ||
118 | markAsChanged(); | ||
119 | } | ||
120 | |||
121 | MPConstraint makeConstraint() { | ||
122 | return solver.makeConstraint(); | ||
123 | } | ||
124 | |||
125 | MPVariable getVariable(int nodeId) { | ||
126 | var variable = variables.get(nodeId); | ||
127 | if (variable != null) { | ||
128 | return variable; | ||
129 | } | ||
130 | var interval = countInterpretation.get(Tuple.of(nodeId)); | ||
131 | if (interval == null || interval.equals(CardinalityIntervals.ONE)) { | ||
132 | interval = CardinalityIntervals.NONE; | ||
133 | } else { | ||
134 | activeVariables.add(nodeId); | ||
135 | markAsChanged(); | ||
136 | } | ||
137 | return createVariable(nodeId, interval); | ||
138 | } | ||
139 | |||
140 | void markAsChanged() { | ||
141 | changed = true; | ||
142 | } | ||
143 | |||
144 | @Override | ||
145 | public PropagationResult propagateOne() { | ||
146 | queryEngine.flushChanges(); | ||
147 | if (!changed) { | ||
148 | return PropagationResult.UNCHANGED; | ||
149 | } | ||
150 | changed = false; | ||
151 | for (var propagator : propagators) { | ||
152 | model.checkCancelled(); | ||
153 | if (!propagator.updateBounds()) { | ||
154 | // Avoid logging GLOP error to console by checking for inconsistent constraints in advance. | ||
155 | return PropagationResult.REJECTED; | ||
156 | } | ||
157 | } | ||
158 | var result = PropagationResult.UNCHANGED; | ||
159 | if (activeVariables.isEmpty()) { | ||
160 | return checkEmptiness(); | ||
161 | } | ||
162 | var iterator = activeVariables.intIterator(); | ||
163 | while (iterator.hasNext()) { | ||
164 | int nodeId = iterator.next(); | ||
165 | var variable = variables.get(nodeId); | ||
166 | if (variable == null) { | ||
167 | throw new AssertionError("Missing active variable: " + nodeId); | ||
168 | } | ||
169 | result = result.andThen(propagateNode(nodeId, variable)); | ||
170 | if (result.isRejected()) { | ||
171 | return result; | ||
172 | } | ||
173 | } | ||
174 | return result; | ||
175 | } | ||
176 | |||
177 | private PropagationResult checkEmptiness() { | ||
178 | model.checkCancelled(); | ||
179 | var emptinessCheckingResult = solver.solve(); | ||
180 | return switch (emptinessCheckingResult) { | ||
181 | case OPTIMAL, UNBOUNDED -> PropagationResult.UNCHANGED; | ||
182 | case INFEASIBLE -> PropagationResult.REJECTED; | ||
183 | default -> throw new IllegalStateException("Failed to check for consistency: " + emptinessCheckingResult); | ||
184 | }; | ||
185 | } | ||
186 | |||
187 | private PropagationResult propagateNode(int nodeId, MPVariable variable) { | ||
188 | objective.setCoefficient(variable, 1); | ||
189 | try { | ||
190 | model.checkCancelled(); | ||
191 | objective.setMinimization(); | ||
192 | var minimizationResult = solver.solve(); | ||
193 | int lowerBound; | ||
194 | switch (minimizationResult) { | ||
195 | case OPTIMAL -> lowerBound = RoundingUtil.roundUp(objective.value()); | ||
196 | case UNBOUNDED -> lowerBound = 0; | ||
197 | case INFEASIBLE -> { | ||
198 | return PropagationResult.REJECTED; | ||
199 | } | ||
200 | default -> throw new IllegalStateException("Failed to solve for minimum of %s: %s" | ||
201 | .formatted(variable, minimizationResult)); | ||
202 | } | ||
203 | |||
204 | model.checkCancelled(); | ||
205 | objective.setMaximization(); | ||
206 | var maximizationResult = solver.solve(); | ||
207 | UpperCardinality upperBound; | ||
208 | switch (maximizationResult) { | ||
209 | case OPTIMAL -> upperBound = UpperCardinalities.atMost(RoundingUtil.roundDown(objective.value())); | ||
210 | // Problem was feasible when minimizing, the only possible source of {@code UNBOUNDED_OR_INFEASIBLE} is | ||
211 | // an unbounded maximization problem. See https://github.com/google/or-tools/issues/3319 | ||
212 | case UNBOUNDED, INFEASIBLE -> upperBound = UpperCardinalities.UNBOUNDED; | ||
213 | default -> throw new IllegalStateException("Failed to solve for maximum of %s: %s" | ||
214 | .formatted(variable, minimizationResult)); | ||
215 | } | ||
216 | |||
217 | var newInterval = CardinalityIntervals.between(lowerBound, upperBound); | ||
218 | var oldInterval = countInterpretation.put(Tuple.of(nodeId), newInterval); | ||
219 | if (newInterval.lowerBound() < oldInterval.lowerBound() || | ||
220 | newInterval.upperBound().compareTo(oldInterval.upperBound()) > 0) { | ||
221 | throw new IllegalArgumentException("Failed to refine multiplicity %s of node %d to %s" | ||
222 | .formatted(oldInterval, nodeId, newInterval)); | ||
223 | } | ||
224 | return newInterval.equals(oldInterval) ? PropagationResult.UNCHANGED : PropagationResult.PROPAGATED; | ||
225 | } finally { | ||
226 | objective.setCoefficient(variable, 0); | ||
227 | } | ||
228 | } | ||
229 | |||
230 | private static double getUpperBound(CardinalityInterval interval) { | ||
231 | var upperBound = interval.upperBound(); | ||
232 | if (upperBound instanceof FiniteUpperCardinality finiteUpperCardinality) { | ||
233 | return finiteUpperCardinality.finiteUpperBound(); | ||
234 | } else if (upperBound instanceof UnboundedUpperCardinality) { | ||
235 | return Double.POSITIVE_INFINITY; | ||
236 | } else { | ||
237 | throw new IllegalArgumentException("Unknown upper bound: " + upperBound); | ||
238 | } | ||
239 | } | ||
240 | } | ||
diff --git a/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/LowerTypeScopePropagator.java b/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/LowerTypeScopePropagator.java new file mode 100644 index 00000000..2be92464 --- /dev/null +++ b/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/LowerTypeScopePropagator.java | |||
@@ -0,0 +1,86 @@ | |||
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.scope; | ||
7 | |||
8 | import tools.refinery.store.dse.transition.DesignSpaceExplorationBuilder; | ||
9 | import tools.refinery.store.dse.transition.objectives.Criteria; | ||
10 | import tools.refinery.store.dse.transition.objectives.Objectives; | ||
11 | import tools.refinery.store.model.ModelStoreBuilder; | ||
12 | import tools.refinery.store.query.dnf.AnyQuery; | ||
13 | import tools.refinery.store.query.dnf.Query; | ||
14 | import tools.refinery.store.query.dnf.RelationalQuery; | ||
15 | import tools.refinery.store.query.term.Variable; | ||
16 | import tools.refinery.store.reasoning.ReasoningBuilder; | ||
17 | import tools.refinery.store.reasoning.literal.CountCandidateLowerBoundLiteral; | ||
18 | import tools.refinery.store.reasoning.representation.PartialRelation; | ||
19 | |||
20 | import java.util.Collection; | ||
21 | import java.util.List; | ||
22 | |||
23 | import static tools.refinery.store.query.literal.Literals.check; | ||
24 | import static tools.refinery.store.query.term.int_.IntTerms.*; | ||
25 | import static tools.refinery.store.reasoning.literal.PartialLiterals.may; | ||
26 | import static tools.refinery.store.reasoning.translator.multiobject.MultiObjectTranslator.MULTI_VIEW; | ||
27 | |||
28 | class LowerTypeScopePropagator extends TypeScopePropagator { | ||
29 | private final int lowerBound; | ||
30 | |||
31 | private LowerTypeScopePropagator(BoundScopePropagator adapter, int lowerBound, RelationalQuery allQuery, | ||
32 | RelationalQuery multiQuery) { | ||
33 | super(adapter, allQuery, multiQuery); | ||
34 | this.lowerBound = lowerBound; | ||
35 | } | ||
36 | |||
37 | @Override | ||
38 | protected void doUpdateBounds() { | ||
39 | constraint.setLb((lowerBound - getSingleCount())); | ||
40 | } | ||
41 | |||
42 | public static class Factory extends TypeScopePropagator.Factory { | ||
43 | private final PartialRelation type; | ||
44 | private final int lowerBound; | ||
45 | private final RelationalQuery allMay; | ||
46 | private final RelationalQuery multiMay; | ||
47 | |||
48 | public Factory(PartialRelation type, int lowerBound) { | ||
49 | this.type = type; | ||
50 | this.lowerBound = lowerBound; | ||
51 | allMay = Query.of(type.name() + "#may", (builder, instance) -> builder.clause( | ||
52 | may(type.call(instance)) | ||
53 | )); | ||
54 | multiMay = Query.of(type.name() + "#multiMay", (builder, instance) -> builder.clause( | ||
55 | may(type.call(instance)), | ||
56 | MULTI_VIEW.call(instance) | ||
57 | )); | ||
58 | } | ||
59 | |||
60 | @Override | ||
61 | public TypeScopePropagator createPropagator(BoundScopePropagator adapter) { | ||
62 | return new LowerTypeScopePropagator(adapter, lowerBound, allMay, multiMay); | ||
63 | } | ||
64 | |||
65 | @Override | ||
66 | protected Collection<AnyQuery> getQueries() { | ||
67 | return List.of(allMay, multiMay); | ||
68 | } | ||
69 | |||
70 | @Override | ||
71 | public void configure(ModelStoreBuilder storeBuilder) { | ||
72 | super.configure(storeBuilder); | ||
73 | |||
74 | var requiredObjects = Query.of(type.name() + "#required", Integer.class, (builder, output) -> builder | ||
75 | .clause(Integer.class, candidateLowerBound -> List.of( | ||
76 | new CountCandidateLowerBoundLiteral(candidateLowerBound, type, List.of(Variable.of())), | ||
77 | output.assign(sub(constant(lowerBound), candidateLowerBound)), | ||
78 | check(greater(output, constant(0))) | ||
79 | ))); | ||
80 | |||
81 | storeBuilder.getAdapter(ReasoningBuilder.class).objective(Objectives.value(requiredObjects)); | ||
82 | storeBuilder.tryGetAdapter(DesignSpaceExplorationBuilder.class).ifPresent(dseBuilder -> | ||
83 | dseBuilder.accept(Criteria.whenNoMatch(requiredObjects))); | ||
84 | } | ||
85 | } | ||
86 | } | ||
diff --git a/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/RoundingUtil.java b/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/RoundingUtil.java new file mode 100644 index 00000000..986771a1 --- /dev/null +++ b/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/RoundingUtil.java | |||
@@ -0,0 +1,26 @@ | |||
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.scope; | ||
7 | |||
8 | final class RoundingUtil { | ||
9 | private static final double TOLERANCE = 0.01; | ||
10 | |||
11 | private RoundingUtil() { | ||
12 | throw new IllegalStateException("This is a static utility class and should not be instantiated directly"); | ||
13 | } | ||
14 | |||
15 | public static int roundUp(double value) { | ||
16 | double ceil = Math.ceil(value - TOLERANCE); | ||
17 | int intCeil = (int) ceil; | ||
18 | return Math.max(intCeil, 0); | ||
19 | } | ||
20 | |||
21 | public static int roundDown(double value) { | ||
22 | double floor = Math.floor(value + TOLERANCE); | ||
23 | int intFloor = (int) floor; | ||
24 | return Math.max(intFloor, 0); | ||
25 | } | ||
26 | } | ||
diff --git a/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/ScopePropagator.java b/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/ScopePropagator.java new file mode 100644 index 00000000..25b1966c --- /dev/null +++ b/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/ScopePropagator.java | |||
@@ -0,0 +1,102 @@ | |||
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.scope; | ||
7 | |||
8 | import com.google.ortools.Loader; | ||
9 | import tools.refinery.store.dse.propagation.PropagationBuilder; | ||
10 | import tools.refinery.store.model.ModelStoreBuilder; | ||
11 | import tools.refinery.store.model.ModelStoreConfiguration; | ||
12 | import tools.refinery.store.reasoning.representation.PartialRelation; | ||
13 | import tools.refinery.store.reasoning.translator.TranslationException; | ||
14 | import tools.refinery.store.reasoning.translator.multiobject.MultiObjectTranslator; | ||
15 | import tools.refinery.store.representation.Symbol; | ||
16 | import tools.refinery.store.representation.cardinality.CardinalityInterval; | ||
17 | import tools.refinery.store.representation.cardinality.FiniteUpperCardinality; | ||
18 | |||
19 | import java.util.*; | ||
20 | |||
21 | public class ScopePropagator implements ModelStoreConfiguration { | ||
22 | private final Symbol<CardinalityInterval> countSymbol; | ||
23 | private final Map<PartialRelation, CardinalityInterval> scopes = new LinkedHashMap<>(); | ||
24 | private final List<TypeScopePropagator.Factory> typeScopePropagatorFactories = new ArrayList<>(); | ||
25 | |||
26 | public ScopePropagator() { | ||
27 | this(MultiObjectTranslator.COUNT_STORAGE); | ||
28 | } | ||
29 | |||
30 | public ScopePropagator(Symbol<CardinalityInterval> countSymbol) { | ||
31 | if (countSymbol.arity() != 1) { | ||
32 | throw new IllegalArgumentException("Count symbol must have arty 1, got %s with arity %d instead" | ||
33 | .formatted(countSymbol, countSymbol.arity())); | ||
34 | } | ||
35 | if (!countSymbol.valueType().equals(CardinalityInterval.class)) { | ||
36 | throw new IllegalArgumentException("Count symbol must have CardinalityInterval values"); | ||
37 | } | ||
38 | if (countSymbol.defaultValue() != null) { | ||
39 | throw new IllegalArgumentException("Count symbol must default value null"); | ||
40 | } | ||
41 | this.countSymbol = countSymbol; | ||
42 | } | ||
43 | |||
44 | public ScopePropagator scope(PartialRelation type, CardinalityInterval interval) { | ||
45 | if (type.arity() != 1) { | ||
46 | throw new TranslationException(type, "Only types with arity 1 may have scopes, got %s with arity %d" | ||
47 | .formatted(type, type.arity())); | ||
48 | } | ||
49 | var newValue = scopes.compute(type, (ignoredKey, oldValue) -> | ||
50 | oldValue == null ? interval : oldValue.meet(interval)); | ||
51 | if (newValue.isEmpty()) { | ||
52 | throw new TranslationException(type, "Unsatisfiable scope for type %s".formatted(type)); | ||
53 | } | ||
54 | return this; | ||
55 | } | ||
56 | |||
57 | public ScopePropagator scopes(Map<PartialRelation, CardinalityInterval> scopes) { | ||
58 | return scopes(scopes.entrySet()); | ||
59 | } | ||
60 | |||
61 | public ScopePropagator scopes(Collection<Map.Entry<PartialRelation, CardinalityInterval>> scopes) { | ||
62 | for (var entry : scopes) { | ||
63 | scope(entry.getKey(), entry.getValue()); | ||
64 | } | ||
65 | return this; | ||
66 | } | ||
67 | |||
68 | @Override | ||
69 | public void apply(ModelStoreBuilder storeBuilder) { | ||
70 | createTypeScopePropagatorFactories(); | ||
71 | Loader.loadNativeLibraries(); | ||
72 | for (var factory : typeScopePropagatorFactories) { | ||
73 | factory.configure(storeBuilder); | ||
74 | } | ||
75 | storeBuilder.getAdapter(PropagationBuilder.class) | ||
76 | .propagator(model -> new BoundScopePropagator(model, this)); | ||
77 | } | ||
78 | |||
79 | private void createTypeScopePropagatorFactories() { | ||
80 | for (var entry : scopes.entrySet()) { | ||
81 | var type = entry.getKey(); | ||
82 | var bounds = entry.getValue(); | ||
83 | if (bounds.lowerBound() > 0) { | ||
84 | var lowerFactory = new LowerTypeScopePropagator.Factory(type, bounds.lowerBound()); | ||
85 | typeScopePropagatorFactories.add(lowerFactory); | ||
86 | } | ||
87 | if (bounds.upperBound() instanceof FiniteUpperCardinality finiteUpperCardinality) { | ||
88 | var upperFactory = new UpperTypeScopePropagator.Factory(type, | ||
89 | finiteUpperCardinality.finiteUpperBound()); | ||
90 | typeScopePropagatorFactories.add(upperFactory); | ||
91 | } | ||
92 | } | ||
93 | } | ||
94 | |||
95 | Symbol<CardinalityInterval> getCountSymbol() { | ||
96 | return countSymbol; | ||
97 | } | ||
98 | |||
99 | List<TypeScopePropagator.Factory> getTypeScopePropagatorFactories() { | ||
100 | return typeScopePropagatorFactories; | ||
101 | } | ||
102 | } | ||
diff --git a/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/TypeScopePropagator.java b/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/TypeScopePropagator.java new file mode 100644 index 00000000..bb50656b --- /dev/null +++ b/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/TypeScopePropagator.java | |||
@@ -0,0 +1,71 @@ | |||
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.scope; | ||
7 | |||
8 | import com.google.ortools.linearsolver.MPConstraint; | ||
9 | import tools.refinery.store.model.ModelStoreBuilder; | ||
10 | import tools.refinery.store.query.ModelQueryBuilder; | ||
11 | import tools.refinery.store.query.dnf.AnyQuery; | ||
12 | import tools.refinery.store.query.dnf.RelationalQuery; | ||
13 | import tools.refinery.store.query.resultset.ResultSet; | ||
14 | import tools.refinery.store.tuple.Tuple; | ||
15 | |||
16 | import java.util.Collection; | ||
17 | |||
18 | abstract class TypeScopePropagator { | ||
19 | private final BoundScopePropagator adapter; | ||
20 | private final ResultSet<Boolean> allNodes; | ||
21 | private final ResultSet<Boolean> multiNodes; | ||
22 | protected final MPConstraint constraint; | ||
23 | |||
24 | protected TypeScopePropagator(BoundScopePropagator adapter, RelationalQuery allQuery, | ||
25 | RelationalQuery multiQuery) { | ||
26 | this.adapter = adapter; | ||
27 | var queryEngine = adapter.getQueryEngine(); | ||
28 | allNodes = queryEngine.getResultSet(allQuery); | ||
29 | multiNodes = queryEngine.getResultSet(multiQuery); | ||
30 | constraint = adapter.makeConstraint(); | ||
31 | constraint.setBounds(0, Double.POSITIVE_INFINITY); | ||
32 | var cursor = multiNodes.getAll(); | ||
33 | while (cursor.move()) { | ||
34 | var variable = adapter.getVariable(cursor.getKey().get(0)); | ||
35 | constraint.setCoefficient(variable, 1); | ||
36 | } | ||
37 | allNodes.addListener(this::allChanged); | ||
38 | multiNodes.addListener(this::multiChanged); | ||
39 | } | ||
40 | |||
41 | protected abstract void doUpdateBounds(); | ||
42 | |||
43 | public boolean updateBounds() { | ||
44 | doUpdateBounds(); | ||
45 | return constraint.lb() <= constraint.ub(); | ||
46 | } | ||
47 | |||
48 | protected int getSingleCount() { | ||
49 | return allNodes.size() - multiNodes.size(); | ||
50 | } | ||
51 | |||
52 | private void allChanged(Tuple ignoredKey, Boolean ignoredOldValue, Boolean ignoredNewValue) { | ||
53 | adapter.markAsChanged(); | ||
54 | } | ||
55 | |||
56 | private void multiChanged(Tuple key, Boolean ignoredOldValue, Boolean newValue) { | ||
57 | var variable = adapter.getVariable(key.get(0)); | ||
58 | constraint.setCoefficient(variable, Boolean.TRUE.equals(newValue) ? 1 : 0); | ||
59 | adapter.markAsChanged(); | ||
60 | } | ||
61 | |||
62 | public abstract static class Factory { | ||
63 | public abstract TypeScopePropagator createPropagator(BoundScopePropagator adapter); | ||
64 | |||
65 | protected abstract Collection<AnyQuery> getQueries(); | ||
66 | |||
67 | public void configure(ModelStoreBuilder storeBuilder) { | ||
68 | storeBuilder.getAdapter(ModelQueryBuilder.class).queries(getQueries()); | ||
69 | } | ||
70 | } | ||
71 | } | ||
diff --git a/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/UpperTypeScopePropagator.java b/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/UpperTypeScopePropagator.java new file mode 100644 index 00000000..4aba5aac --- /dev/null +++ b/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/UpperTypeScopePropagator.java | |||
@@ -0,0 +1,59 @@ | |||
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.scope; | ||
7 | |||
8 | import tools.refinery.store.query.dnf.AnyQuery; | ||
9 | import tools.refinery.store.query.dnf.Query; | ||
10 | import tools.refinery.store.query.dnf.RelationalQuery; | ||
11 | import tools.refinery.store.reasoning.representation.PartialRelation; | ||
12 | |||
13 | import java.util.Collection; | ||
14 | import java.util.List; | ||
15 | |||
16 | import static tools.refinery.store.reasoning.literal.PartialLiterals.must; | ||
17 | import static tools.refinery.store.reasoning.translator.multiobject.MultiObjectTranslator.MULTI_VIEW; | ||
18 | |||
19 | class UpperTypeScopePropagator extends TypeScopePropagator { | ||
20 | private final int upperBound; | ||
21 | |||
22 | private UpperTypeScopePropagator(BoundScopePropagator adapter, int upperBound, RelationalQuery allQuery, | ||
23 | RelationalQuery multiQuery) { | ||
24 | super(adapter, allQuery, multiQuery); | ||
25 | this.upperBound = upperBound; | ||
26 | } | ||
27 | |||
28 | @Override | ||
29 | protected void doUpdateBounds() { | ||
30 | constraint.setUb((upperBound - getSingleCount())); | ||
31 | } | ||
32 | |||
33 | public static class Factory extends TypeScopePropagator.Factory { | ||
34 | private final int upperBound; | ||
35 | private final RelationalQuery allMust; | ||
36 | private final RelationalQuery multiMust; | ||
37 | |||
38 | public Factory(PartialRelation type, int upperBound) { | ||
39 | this.upperBound = upperBound; | ||
40 | allMust = Query.of(type.name() + "#must", (builder, instance) -> builder.clause( | ||
41 | must(type.call(instance)) | ||
42 | )); | ||
43 | multiMust = Query.of(type.name() + "#multiMust", (builder, instance) -> builder.clause( | ||
44 | must(type.call(instance)), | ||
45 | MULTI_VIEW.call(instance) | ||
46 | )); | ||
47 | } | ||
48 | |||
49 | @Override | ||
50 | public TypeScopePropagator createPropagator(BoundScopePropagator adapter) { | ||
51 | return new UpperTypeScopePropagator(adapter, upperBound, allMust, multiMust); | ||
52 | } | ||
53 | |||
54 | @Override | ||
55 | protected Collection<AnyQuery> getQueries() { | ||
56 | return List.of(allMust, multiMust); | ||
57 | } | ||
58 | } | ||
59 | } | ||