diff options
author | Kristóf Marussy <kristof@marussy.com> | 2023-09-03 14:11:29 +0200 |
---|---|---|
committer | Kristóf Marussy <kristof@marussy.com> | 2023-09-03 14:11:29 +0200 |
commit | 5ab558ad2d7c3a8e47bdd21b1dbe7190d430125c (patch) | |
tree | e9f10f5a8450aba6a151ef42ac7d40a1e986f17e /subprojects/store-reasoning-scope | |
parent | chore(build): replce deprecated Gradle API use (diff) | |
download | refinery-5ab558ad2d7c3a8e47bdd21b1dbe7190d430125c.tar.gz refinery-5ab558ad2d7c3a8e47bdd21b1dbe7190d430125c.tar.zst refinery-5ab558ad2d7c3a8e47bdd21b1dbe7190d430125c.zip |
feat: type scope propagator
Diffstat (limited to 'subprojects/store-reasoning-scope')
14 files changed, 1012 insertions, 0 deletions
diff --git a/subprojects/store-reasoning-scope/build.gradle.kts b/subprojects/store-reasoning-scope/build.gradle.kts new file mode 100644 index 00000000..6e41dc8e --- /dev/null +++ b/subprojects/store-reasoning-scope/build.gradle.kts | |||
@@ -0,0 +1,17 @@ | |||
1 | /* | ||
2 | * SPDX-FileCopyrightText: 2021-2023 The Refinery Authors <https://refinery.tools/> | ||
3 | * | ||
4 | * SPDX-License-Identifier: EPL-2.0 | ||
5 | */ | ||
6 | |||
7 | plugins { | ||
8 | id("tools.refinery.gradle.java-library") | ||
9 | } | ||
10 | |||
11 | dependencies { | ||
12 | api(project(":refinery-store-reasoning")) | ||
13 | implementation(libs.eclipseCollections.api) | ||
14 | implementation(libs.ortools) | ||
15 | runtimeOnly(libs.eclipseCollections) | ||
16 | testImplementation(project(":refinery-store-query-viatra")) | ||
17 | } | ||
diff --git a/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/ScopePropagatorAdapter.java b/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/ScopePropagatorAdapter.java new file mode 100644 index 00000000..c2d3f59e --- /dev/null +++ b/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/ScopePropagatorAdapter.java | |||
@@ -0,0 +1,21 @@ | |||
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.adapter.ModelAdapter; | ||
9 | import tools.refinery.store.reasoning.refinement.RefinementResult; | ||
10 | import tools.refinery.store.reasoning.scope.internal.ScopePropagatorBuilderImpl; | ||
11 | |||
12 | public interface ScopePropagatorAdapter extends ModelAdapter { | ||
13 | @Override | ||
14 | ScopePropagatorStoreAdapter getStoreAdapter(); | ||
15 | |||
16 | RefinementResult propagate(); | ||
17 | |||
18 | static ScopePropagatorBuilder builder() { | ||
19 | return new ScopePropagatorBuilderImpl(); | ||
20 | } | ||
21 | } | ||
diff --git a/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/ScopePropagatorBuilder.java b/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/ScopePropagatorBuilder.java new file mode 100644 index 00000000..a17e04a4 --- /dev/null +++ b/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/ScopePropagatorBuilder.java | |||
@@ -0,0 +1,21 @@ | |||
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.adapter.ModelAdapterBuilder; | ||
9 | import tools.refinery.store.model.ModelStore; | ||
10 | import tools.refinery.store.reasoning.representation.PartialRelation; | ||
11 | import tools.refinery.store.representation.Symbol; | ||
12 | import tools.refinery.store.representation.cardinality.CardinalityInterval; | ||
13 | |||
14 | public interface ScopePropagatorBuilder extends ModelAdapterBuilder { | ||
15 | ScopePropagatorBuilder countSymbol(Symbol<CardinalityInterval> countSymbol); | ||
16 | |||
17 | ScopePropagatorBuilder scope(PartialRelation type, CardinalityInterval interval); | ||
18 | |||
19 | @Override | ||
20 | ScopePropagatorStoreAdapter build(ModelStore store); | ||
21 | } | ||
diff --git a/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/ScopePropagatorStoreAdapter.java b/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/ScopePropagatorStoreAdapter.java new file mode 100644 index 00000000..65d9c38d --- /dev/null +++ b/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/ScopePropagatorStoreAdapter.java | |||
@@ -0,0 +1,16 @@ | |||
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.adapter.ModelStoreAdapter; | ||
9 | import tools.refinery.store.reasoning.representation.PartialRelation; | ||
10 | import tools.refinery.store.representation.cardinality.CardinalityInterval; | ||
11 | |||
12 | import java.util.Map; | ||
13 | |||
14 | public interface ScopePropagatorStoreAdapter extends ModelStoreAdapter { | ||
15 | Map<PartialRelation, CardinalityInterval> getScopes(); | ||
16 | } | ||
diff --git a/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/internal/LowerTypeScopePropagator.java b/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/internal/LowerTypeScopePropagator.java new file mode 100644 index 00000000..b1c421b7 --- /dev/null +++ b/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/internal/LowerTypeScopePropagator.java | |||
@@ -0,0 +1,58 @@ | |||
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.internal; | ||
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.may; | ||
17 | |||
18 | class LowerTypeScopePropagator extends TypeScopePropagator { | ||
19 | private final int lowerBound; | ||
20 | |||
21 | private LowerTypeScopePropagator(ScopePropagatorAdapterImpl adapter, int lowerBound, RelationalQuery allQuery, | ||
22 | RelationalQuery multiQuery) { | ||
23 | super(adapter, allQuery, multiQuery); | ||
24 | this.lowerBound = lowerBound; | ||
25 | } | ||
26 | |||
27 | @Override | ||
28 | public void updateBounds() { | ||
29 | constraint.setLb(lowerBound - getSingleCount()); | ||
30 | } | ||
31 | |||
32 | public static class Factory implements TypeScopePropagator.Factory { | ||
33 | private final int lowerBound; | ||
34 | private final RelationalQuery allMay; | ||
35 | private final RelationalQuery multiMay; | ||
36 | |||
37 | public Factory(RelationalQuery multi, PartialRelation type, int lowerBound) { | ||
38 | this.lowerBound = lowerBound; | ||
39 | allMay = Query.of(type.name() + "#may", (builder, instance) -> builder.clause( | ||
40 | may(type.call(instance)) | ||
41 | )); | ||
42 | multiMay = Query.of(type.name() + "#multiMay", (builder, instance) -> builder.clause( | ||
43 | may(type.call(instance)), | ||
44 | multi.call(instance) | ||
45 | )); | ||
46 | } | ||
47 | |||
48 | @Override | ||
49 | public TypeScopePropagator createPropagator(ScopePropagatorAdapterImpl adapter) { | ||
50 | return new LowerTypeScopePropagator(adapter, lowerBound, allMay, multiMay); | ||
51 | } | ||
52 | |||
53 | @Override | ||
54 | public Collection<AnyQuery> getQueries() { | ||
55 | return List.of(allMay, multiMay); | ||
56 | } | ||
57 | } | ||
58 | } | ||
diff --git a/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/internal/RoundingUtil.java b/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/internal/RoundingUtil.java new file mode 100644 index 00000000..a6d663ea --- /dev/null +++ b/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/internal/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.internal; | ||
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/internal/ScopePropagatorAdapterImpl.java b/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/internal/ScopePropagatorAdapterImpl.java new file mode 100644 index 00000000..0d594701 --- /dev/null +++ b/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/internal/ScopePropagatorAdapterImpl.java | |||
@@ -0,0 +1,244 @@ | |||
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.internal; | ||
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.model.Interpretation; | ||
17 | import tools.refinery.store.model.Model; | ||
18 | import tools.refinery.store.query.ModelQueryAdapter; | ||
19 | import tools.refinery.store.reasoning.refinement.RefinementResult; | ||
20 | import tools.refinery.store.reasoning.scope.ScopePropagatorAdapter; | ||
21 | import tools.refinery.store.reasoning.scope.ScopePropagatorStoreAdapter; | ||
22 | import tools.refinery.store.representation.cardinality.*; | ||
23 | import tools.refinery.store.tuple.Tuple; | ||
24 | |||
25 | class ScopePropagatorAdapterImpl implements ScopePropagatorAdapter { | ||
26 | private final Model model; | ||
27 | private final ScopePropagatorStoreAdapterImpl storeAdapter; | ||
28 | private final ModelQueryAdapter queryEngine; | ||
29 | private final Interpretation<CardinalityInterval> countInterpretation; | ||
30 | private final MPSolver solver; | ||
31 | private final MPObjective objective; | ||
32 | private final MutableIntObjectMap<MPVariable> variables = IntObjectMaps.mutable.empty(); | ||
33 | private final MutableIntSet activeVariables = IntSets.mutable.empty(); | ||
34 | private final TypeScopePropagator[] propagators; | ||
35 | private boolean changed = true; | ||
36 | |||
37 | public ScopePropagatorAdapterImpl(Model model, ScopePropagatorStoreAdapterImpl storeAdapter) { | ||
38 | this.model = model; | ||
39 | this.storeAdapter = storeAdapter; | ||
40 | queryEngine = model.getAdapter(ModelQueryAdapter.class); | ||
41 | countInterpretation = model.getInterpretation(storeAdapter.getCountSymbol()); | ||
42 | solver = MPSolver.createSolver("GLOP"); | ||
43 | objective = solver.objective(); | ||
44 | initializeVariables(); | ||
45 | countInterpretation.addListener(this::countChanged, true); | ||
46 | var propagatorFactories = storeAdapter.getPropagatorFactories(); | ||
47 | propagators = new TypeScopePropagator[propagatorFactories.size()]; | ||
48 | for (int i = 0; i < propagators.length; i++) { | ||
49 | propagators[i] = propagatorFactories.get(i).createPropagator(this); | ||
50 | } | ||
51 | } | ||
52 | |||
53 | @Override | ||
54 | public Model getModel() { | ||
55 | return model; | ||
56 | } | ||
57 | |||
58 | @Override | ||
59 | public ScopePropagatorStoreAdapter getStoreAdapter() { | ||
60 | return storeAdapter; | ||
61 | } | ||
62 | |||
63 | private void initializeVariables() { | ||
64 | var cursor = countInterpretation.getAll(); | ||
65 | while (cursor.move()) { | ||
66 | var interval = cursor.getValue(); | ||
67 | if (!interval.equals(CardinalityIntervals.ONE)) { | ||
68 | int nodeId = cursor.getKey().get(0); | ||
69 | createVariable(nodeId, interval); | ||
70 | activeVariables.add(nodeId); | ||
71 | } | ||
72 | } | ||
73 | } | ||
74 | |||
75 | private MPVariable createVariable(int nodeId, CardinalityInterval interval) { | ||
76 | double lowerBound = interval.lowerBound(); | ||
77 | double upperBound = getUpperBound(interval); | ||
78 | var variable = solver.makeNumVar(lowerBound, upperBound, "x" + nodeId); | ||
79 | variables.put(nodeId, variable); | ||
80 | return variable; | ||
81 | } | ||
82 | |||
83 | private void countChanged(Tuple key, CardinalityInterval fromValue, CardinalityInterval toValue, | ||
84 | boolean ignoredRestoring) { | ||
85 | int nodeId = key.get(0); | ||
86 | if ((toValue == null || toValue.equals(CardinalityIntervals.ONE))) { | ||
87 | if (fromValue != null && !fromValue.equals(CardinalityIntervals.ONE)) { | ||
88 | var variable = variables.get(nodeId); | ||
89 | if (variable == null || !activeVariables.remove(nodeId)) { | ||
90 | throw new AssertionError("Variable not active: " + nodeId); | ||
91 | } | ||
92 | variable.setBounds(0, 0); | ||
93 | markAsChanged(); | ||
94 | } | ||
95 | return; | ||
96 | } | ||
97 | if (fromValue == null || fromValue.equals(CardinalityIntervals.ONE)) { | ||
98 | activeVariables.add(nodeId); | ||
99 | } | ||
100 | var variable = variables.get(nodeId); | ||
101 | if (variable == null) { | ||
102 | createVariable(nodeId, toValue); | ||
103 | markAsChanged(); | ||
104 | return; | ||
105 | } | ||
106 | double lowerBound = toValue.lowerBound(); | ||
107 | double upperBound = getUpperBound(toValue); | ||
108 | if (variable.lb() != lowerBound) { | ||
109 | variable.setLb(lowerBound); | ||
110 | markAsChanged(); | ||
111 | } | ||
112 | if (variable.ub() != upperBound) { | ||
113 | variable.setUb(upperBound); | ||
114 | markAsChanged(); | ||
115 | } | ||
116 | } | ||
117 | |||
118 | MPConstraint makeConstraint() { | ||
119 | return solver.makeConstraint(); | ||
120 | } | ||
121 | |||
122 | MPVariable getVariable(int nodeId) { | ||
123 | var variable = variables.get(nodeId); | ||
124 | if (variable != null) { | ||
125 | return variable; | ||
126 | } | ||
127 | var interval = countInterpretation.get(Tuple.of(nodeId)); | ||
128 | if (interval == null || interval.equals(CardinalityIntervals.ONE)) { | ||
129 | interval = CardinalityIntervals.NONE; | ||
130 | } else { | ||
131 | activeVariables.add(nodeId); | ||
132 | markAsChanged(); | ||
133 | } | ||
134 | return createVariable(nodeId, interval); | ||
135 | } | ||
136 | |||
137 | void markAsChanged() { | ||
138 | changed = true; | ||
139 | } | ||
140 | |||
141 | @Override | ||
142 | public RefinementResult propagate() { | ||
143 | var result = RefinementResult.UNCHANGED; | ||
144 | RefinementResult currentRoundResult; | ||
145 | do { | ||
146 | currentRoundResult = propagateOne(); | ||
147 | result = result.andThen(currentRoundResult); | ||
148 | if (result.isRejected()) { | ||
149 | return result; | ||
150 | } | ||
151 | } while (currentRoundResult != RefinementResult.UNCHANGED); | ||
152 | return result; | ||
153 | } | ||
154 | |||
155 | private RefinementResult propagateOne() { | ||
156 | queryEngine.flushChanges(); | ||
157 | if (!changed) { | ||
158 | return RefinementResult.UNCHANGED; | ||
159 | } | ||
160 | changed = false; | ||
161 | for (var propagator : propagators) { | ||
162 | propagator.updateBounds(); | ||
163 | } | ||
164 | var result = RefinementResult.UNCHANGED; | ||
165 | if (activeVariables.isEmpty()) { | ||
166 | return checkEmptiness(); | ||
167 | } | ||
168 | var iterator = activeVariables.intIterator(); | ||
169 | while (iterator.hasNext()) { | ||
170 | int nodeId = iterator.next(); | ||
171 | var variable = variables.get(nodeId); | ||
172 | if (variable == null) { | ||
173 | throw new AssertionError("Missing active variable: " + nodeId); | ||
174 | } | ||
175 | result = result.andThen(propagateNode(nodeId, variable)); | ||
176 | if (result.isRejected()) { | ||
177 | return result; | ||
178 | } | ||
179 | } | ||
180 | return result; | ||
181 | } | ||
182 | |||
183 | private RefinementResult checkEmptiness() { | ||
184 | var emptinessCheckingResult = solver.solve(); | ||
185 | return switch (emptinessCheckingResult) { | ||
186 | case OPTIMAL, UNBOUNDED -> RefinementResult.UNCHANGED; | ||
187 | case INFEASIBLE -> RefinementResult.REJECTED; | ||
188 | default -> throw new IllegalStateException("Failed to check for consistency: " + emptinessCheckingResult); | ||
189 | }; | ||
190 | } | ||
191 | |||
192 | private RefinementResult propagateNode(int nodeId, MPVariable variable) { | ||
193 | objective.setCoefficient(variable, 1); | ||
194 | try { | ||
195 | objective.setMinimization(); | ||
196 | var minimizationResult = solver.solve(); | ||
197 | int lowerBound; | ||
198 | switch (minimizationResult) { | ||
199 | case OPTIMAL -> lowerBound = RoundingUtil.roundUp(objective.value()); | ||
200 | case UNBOUNDED -> lowerBound = 0; | ||
201 | case INFEASIBLE -> { | ||
202 | return RefinementResult.REJECTED; | ||
203 | } | ||
204 | default -> throw new IllegalStateException("Failed to solve for minimum of %s: %s" | ||
205 | .formatted(variable, minimizationResult)); | ||
206 | } | ||
207 | |||
208 | objective.setMaximization(); | ||
209 | var maximizationResult = solver.solve(); | ||
210 | UpperCardinality upperBound; | ||
211 | switch (maximizationResult) { | ||
212 | case OPTIMAL -> upperBound = UpperCardinalities.atMost(RoundingUtil.roundDown(objective.value())); | ||
213 | case UNBOUNDED -> upperBound = UpperCardinalities.UNBOUNDED; | ||
214 | case INFEASIBLE -> { | ||
215 | return RefinementResult.REJECTED; | ||
216 | } | ||
217 | default -> throw new IllegalStateException("Failed to solve for maximum of %s: %s" | ||
218 | .formatted(variable, minimizationResult)); | ||
219 | } | ||
220 | |||
221 | var newInterval = CardinalityIntervals.between(lowerBound, upperBound); | ||
222 | var oldInterval = countInterpretation.put(Tuple.of(nodeId), newInterval); | ||
223 | if (newInterval.lowerBound() < oldInterval.lowerBound() || | ||
224 | newInterval.upperBound().compareTo(oldInterval.upperBound()) > 0) { | ||
225 | throw new IllegalArgumentException("Failed to refine multiplicity %s of node %d to %s" | ||
226 | .formatted(oldInterval, nodeId, newInterval)); | ||
227 | } | ||
228 | return newInterval.equals(oldInterval) ? RefinementResult.UNCHANGED : RefinementResult.REFINED; | ||
229 | } finally { | ||
230 | objective.setCoefficient(variable, 0); | ||
231 | } | ||
232 | } | ||
233 | |||
234 | private static double getUpperBound(CardinalityInterval interval) { | ||
235 | var upperBound = interval.upperBound(); | ||
236 | if (upperBound instanceof FiniteUpperCardinality finiteUpperCardinality) { | ||
237 | return finiteUpperCardinality.finiteUpperBound(); | ||
238 | } else if (upperBound instanceof UnboundedUpperCardinality) { | ||
239 | return Double.POSITIVE_INFINITY; | ||
240 | } else { | ||
241 | throw new IllegalArgumentException("Unknown upper bound: " + upperBound); | ||
242 | } | ||
243 | } | ||
244 | } | ||
diff --git a/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/internal/ScopePropagatorBuilderImpl.java b/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/internal/ScopePropagatorBuilderImpl.java new file mode 100644 index 00000000..f383ebeb --- /dev/null +++ b/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/internal/ScopePropagatorBuilderImpl.java | |||
@@ -0,0 +1,105 @@ | |||
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.internal; | ||
7 | |||
8 | import com.google.ortools.Loader; | ||
9 | import tools.refinery.store.adapter.AbstractModelAdapterBuilder; | ||
10 | import tools.refinery.store.model.ModelStore; | ||
11 | import tools.refinery.store.model.ModelStoreBuilder; | ||
12 | import tools.refinery.store.query.ModelQueryBuilder; | ||
13 | import tools.refinery.store.query.dnf.Query; | ||
14 | import tools.refinery.store.reasoning.representation.PartialRelation; | ||
15 | import tools.refinery.store.reasoning.scope.ScopePropagatorBuilder; | ||
16 | import tools.refinery.store.reasoning.scope.ScopePropagatorStoreAdapter; | ||
17 | import tools.refinery.store.reasoning.translator.TranslationException; | ||
18 | import tools.refinery.store.reasoning.translator.multiobject.MultiObjectTranslator; | ||
19 | import tools.refinery.store.representation.Symbol; | ||
20 | import tools.refinery.store.representation.cardinality.CardinalityInterval; | ||
21 | import tools.refinery.store.representation.cardinality.FiniteUpperCardinality; | ||
22 | |||
23 | import java.util.*; | ||
24 | |||
25 | import static tools.refinery.store.query.literal.Literals.not; | ||
26 | import static tools.refinery.store.reasoning.ReasoningAdapter.EQUALS_SYMBOL; | ||
27 | import static tools.refinery.store.reasoning.ReasoningAdapter.EXISTS_SYMBOL; | ||
28 | import static tools.refinery.store.reasoning.literal.PartialLiterals.may; | ||
29 | import static tools.refinery.store.reasoning.literal.PartialLiterals.must; | ||
30 | |||
31 | public class ScopePropagatorBuilderImpl extends AbstractModelAdapterBuilder<ScopePropagatorStoreAdapter> | ||
32 | implements ScopePropagatorBuilder { | ||
33 | private Symbol<CardinalityInterval> countSymbol = MultiObjectTranslator.COUNT_STORAGE; | ||
34 | private final Map<PartialRelation, CardinalityInterval> scopes = new LinkedHashMap<>(); | ||
35 | private List<TypeScopePropagator.Factory> typeScopePropagatorFactories; | ||
36 | |||
37 | @Override | ||
38 | public ScopePropagatorBuilder countSymbol(Symbol<CardinalityInterval> countSymbol) { | ||
39 | if (countSymbol.arity() != 1) { | ||
40 | throw new IllegalArgumentException("Count symbol must have arty 1, got %s with arity %d instead" | ||
41 | .formatted(countSymbol, countSymbol.arity())); | ||
42 | } | ||
43 | if (!countSymbol.valueType().equals(CardinalityInterval.class)) { | ||
44 | throw new IllegalArgumentException("Count symbol must have CardinalityInterval values"); | ||
45 | } | ||
46 | if (countSymbol.defaultValue() != null) { | ||
47 | throw new IllegalArgumentException("Count symbol must default value null"); | ||
48 | } | ||
49 | this.countSymbol = countSymbol; | ||
50 | return this; | ||
51 | } | ||
52 | |||
53 | @Override | ||
54 | public ScopePropagatorBuilder scope(PartialRelation type, CardinalityInterval interval) { | ||
55 | if (type.arity() != 1) { | ||
56 | throw new TranslationException(type, "Only types with arity 1 may have scopes, got %s with arity %d" | ||
57 | .formatted(type, type.arity())); | ||
58 | } | ||
59 | var newValue = scopes.compute(type, (ignoredKey, oldValue) -> | ||
60 | oldValue == null ? interval : oldValue.meet(interval)); | ||
61 | if (newValue.isEmpty()) { | ||
62 | throw new TranslationException(type, "Unsatisfiable scope for type %s".formatted(type)); | ||
63 | } | ||
64 | return this; | ||
65 | } | ||
66 | |||
67 | @Override | ||
68 | protected void doConfigure(ModelStoreBuilder storeBuilder) { | ||
69 | var multiQuery = Query.of("MULTI", (builder, instance) -> builder | ||
70 | .clause( | ||
71 | may(EXISTS_SYMBOL.call(instance)), | ||
72 | not(must(EXISTS_SYMBOL.call(instance))) | ||
73 | ) | ||
74 | .clause( | ||
75 | may(EXISTS_SYMBOL.call(instance)), | ||
76 | not(must(EQUALS_SYMBOL.call(instance, instance))) | ||
77 | ) | ||
78 | ); | ||
79 | typeScopePropagatorFactories = new ArrayList<>(scopes.size()); | ||
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(multiQuery, type, bounds.lowerBound()); | ||
85 | typeScopePropagatorFactories.add(lowerFactory); | ||
86 | } | ||
87 | if (bounds.upperBound() instanceof FiniteUpperCardinality finiteUpperCardinality) { | ||
88 | var upperFactory = new UpperTypeScopePropagator.Factory(multiQuery, type, | ||
89 | finiteUpperCardinality.finiteUpperBound()); | ||
90 | typeScopePropagatorFactories.add(upperFactory); | ||
91 | } | ||
92 | } | ||
93 | var queryBuilder = storeBuilder.getAdapter(ModelQueryBuilder.class); | ||
94 | for (var factory : typeScopePropagatorFactories) { | ||
95 | queryBuilder.queries(factory.getQueries()); | ||
96 | } | ||
97 | } | ||
98 | |||
99 | @Override | ||
100 | protected ScopePropagatorStoreAdapter doBuild(ModelStore store) { | ||
101 | Loader.loadNativeLibraries(); | ||
102 | return new ScopePropagatorStoreAdapterImpl(store, countSymbol, Collections.unmodifiableMap(scopes), | ||
103 | Collections.unmodifiableList(typeScopePropagatorFactories)); | ||
104 | } | ||
105 | } | ||
diff --git a/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/internal/ScopePropagatorStoreAdapterImpl.java b/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/internal/ScopePropagatorStoreAdapterImpl.java new file mode 100644 index 00000000..282ffe6f --- /dev/null +++ b/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/internal/ScopePropagatorStoreAdapterImpl.java | |||
@@ -0,0 +1,58 @@ | |||
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.internal; | ||
7 | |||
8 | import tools.refinery.store.adapter.ModelAdapter; | ||
9 | import tools.refinery.store.model.Model; | ||
10 | import tools.refinery.store.model.ModelStore; | ||
11 | import tools.refinery.store.reasoning.representation.PartialRelation; | ||
12 | import tools.refinery.store.reasoning.scope.ScopePropagatorStoreAdapter; | ||
13 | import tools.refinery.store.representation.Symbol; | ||
14 | import tools.refinery.store.representation.cardinality.CardinalityInterval; | ||
15 | |||
16 | import java.util.List; | ||
17 | import java.util.Map; | ||
18 | |||
19 | // Not a record, because we want to control getter visibility. | ||
20 | @SuppressWarnings("ClassCanBeRecord") | ||
21 | class ScopePropagatorStoreAdapterImpl implements ScopePropagatorStoreAdapter { | ||
22 | private final ModelStore store; | ||
23 | private final Symbol<CardinalityInterval> countSymbol; | ||
24 | private final Map<PartialRelation, CardinalityInterval> scopes; | ||
25 | private final List<TypeScopePropagator.Factory> propagatorFactories; | ||
26 | |||
27 | public ScopePropagatorStoreAdapterImpl( | ||
28 | ModelStore store, Symbol<CardinalityInterval> countSymbol, | ||
29 | Map<PartialRelation, CardinalityInterval> scopes, List<TypeScopePropagator.Factory> propagatorFactories) { | ||
30 | this.store = store; | ||
31 | this.countSymbol = countSymbol; | ||
32 | this.scopes = scopes; | ||
33 | this.propagatorFactories = propagatorFactories; | ||
34 | } | ||
35 | |||
36 | @Override | ||
37 | public ModelStore getStore() { | ||
38 | return store; | ||
39 | } | ||
40 | |||
41 | Symbol<CardinalityInterval> getCountSymbol() { | ||
42 | return countSymbol; | ||
43 | } | ||
44 | |||
45 | @Override | ||
46 | public Map<PartialRelation, CardinalityInterval> getScopes() { | ||
47 | return scopes; | ||
48 | } | ||
49 | |||
50 | public List<TypeScopePropagator.Factory> getPropagatorFactories() { | ||
51 | return propagatorFactories; | ||
52 | } | ||
53 | |||
54 | @Override | ||
55 | public ModelAdapter createModelAdapter(Model model) { | ||
56 | return new ScopePropagatorAdapterImpl(model, this); | ||
57 | } | ||
58 | } | ||
diff --git a/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/internal/TypeScopePropagator.java b/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/internal/TypeScopePropagator.java new file mode 100644 index 00000000..98f6ed8b --- /dev/null +++ b/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/internal/TypeScopePropagator.java | |||
@@ -0,0 +1,61 @@ | |||
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.internal; | ||
7 | |||
8 | import com.google.ortools.linearsolver.MPConstraint; | ||
9 | import tools.refinery.store.query.ModelQueryAdapter; | ||
10 | import tools.refinery.store.query.dnf.AnyQuery; | ||
11 | import tools.refinery.store.query.dnf.RelationalQuery; | ||
12 | import tools.refinery.store.query.resultset.ResultSet; | ||
13 | import tools.refinery.store.tuple.Tuple; | ||
14 | |||
15 | import java.util.Collection; | ||
16 | |||
17 | abstract class TypeScopePropagator { | ||
18 | private final ScopePropagatorAdapterImpl adapter; | ||
19 | private final ResultSet<Boolean> allNodes; | ||
20 | private final ResultSet<Boolean> multiNodes; | ||
21 | protected final MPConstraint constraint; | ||
22 | |||
23 | protected TypeScopePropagator(ScopePropagatorAdapterImpl adapter, RelationalQuery allQuery, | ||
24 | RelationalQuery multiQuery) { | ||
25 | this.adapter = adapter; | ||
26 | var queryEngine = adapter.getModel().getAdapter(ModelQueryAdapter.class); | ||
27 | allNodes = queryEngine.getResultSet(allQuery); | ||
28 | multiNodes = queryEngine.getResultSet(multiQuery); | ||
29 | constraint = adapter.makeConstraint(); | ||
30 | constraint.setBounds(0, Double.POSITIVE_INFINITY); | ||
31 | var cursor = multiNodes.getAll(); | ||
32 | while (cursor.move()) { | ||
33 | var variable = adapter.getVariable(cursor.getKey().get(0)); | ||
34 | constraint.setCoefficient(variable, 1); | ||
35 | } | ||
36 | allNodes.addListener(this::allChanged); | ||
37 | multiNodes.addListener(this::multiChanged); | ||
38 | } | ||
39 | |||
40 | public abstract void updateBounds(); | ||
41 | |||
42 | protected int getSingleCount() { | ||
43 | return allNodes.size() - multiNodes.size(); | ||
44 | } | ||
45 | |||
46 | private void allChanged(Tuple ignoredKey, Boolean ignoredOldValue, Boolean ignoredNewValue) { | ||
47 | adapter.markAsChanged(); | ||
48 | } | ||
49 | |||
50 | private void multiChanged(Tuple key, Boolean ignoredOldValue, Boolean newValue) { | ||
51 | var variable = adapter.getVariable(key.get(0)); | ||
52 | constraint.setCoefficient(variable, Boolean.TRUE.equals(newValue) ? 1 : 0); | ||
53 | adapter.markAsChanged(); | ||
54 | } | ||
55 | |||
56 | interface Factory { | ||
57 | TypeScopePropagator createPropagator(ScopePropagatorAdapterImpl adapter); | ||
58 | |||
59 | Collection<AnyQuery> getQueries(); | ||
60 | } | ||
61 | } | ||
diff --git a/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/internal/UpperTypeScopePropagator.java b/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/internal/UpperTypeScopePropagator.java new file mode 100644 index 00000000..9f09ed56 --- /dev/null +++ b/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/internal/UpperTypeScopePropagator.java | |||
@@ -0,0 +1,58 @@ | |||
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.internal; | ||
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 | |||
18 | class UpperTypeScopePropagator extends TypeScopePropagator { | ||
19 | private final int upperBound; | ||
20 | |||
21 | private UpperTypeScopePropagator(ScopePropagatorAdapterImpl adapter, int upperBound, RelationalQuery allQuery, | ||
22 | RelationalQuery multiQuery) { | ||
23 | super(adapter, allQuery, multiQuery); | ||
24 | this.upperBound = upperBound; | ||
25 | } | ||
26 | |||
27 | @Override | ||
28 | public void updateBounds() { | ||
29 | constraint.setUb(upperBound - getSingleCount()); | ||
30 | } | ||
31 | |||
32 | public static class Factory implements TypeScopePropagator.Factory { | ||
33 | private final int upperBound; | ||
34 | private final RelationalQuery allMust; | ||
35 | private final RelationalQuery multiMust; | ||
36 | |||
37 | public Factory(RelationalQuery multi, PartialRelation type, int upperBound) { | ||
38 | this.upperBound = upperBound; | ||
39 | allMust = Query.of(type.name() + "#must", (builder, instance) -> builder.clause( | ||
40 | must(type.call(instance)) | ||
41 | )); | ||
42 | multiMust = Query.of(type.name() + "#multiMust", (builder, instance) -> builder.clause( | ||
43 | must(type.call(instance)), | ||
44 | multi.call(instance) | ||
45 | )); | ||
46 | } | ||
47 | |||
48 | @Override | ||
49 | public TypeScopePropagator createPropagator(ScopePropagatorAdapterImpl adapter) { | ||
50 | return new UpperTypeScopePropagator(adapter, upperBound, allMust, multiMust); | ||
51 | } | ||
52 | |||
53 | @Override | ||
54 | public Collection<AnyQuery> getQueries() { | ||
55 | return List.of(allMust, multiMust); | ||
56 | } | ||
57 | } | ||
58 | } | ||
diff --git a/subprojects/store-reasoning-scope/src/test/java/tools/refinery/store/reasoning/scope/MPSolverTest.java b/subprojects/store-reasoning-scope/src/test/java/tools/refinery/store/reasoning/scope/MPSolverTest.java new file mode 100644 index 00000000..c9745d22 --- /dev/null +++ b/subprojects/store-reasoning-scope/src/test/java/tools/refinery/store/reasoning/scope/MPSolverTest.java | |||
@@ -0,0 +1,52 @@ | |||
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 com.google.ortools.linearsolver.MPSolver; | ||
10 | import org.junit.jupiter.api.BeforeAll; | ||
11 | import org.junit.jupiter.api.Test; | ||
12 | |||
13 | import static org.hamcrest.MatcherAssert.assertThat; | ||
14 | import static org.hamcrest.Matchers.closeTo; | ||
15 | import static org.hamcrest.Matchers.is; | ||
16 | |||
17 | class MPSolverTest { | ||
18 | @BeforeAll | ||
19 | static void beforeAll() { | ||
20 | Loader.loadNativeLibraries(); | ||
21 | } | ||
22 | |||
23 | @Test | ||
24 | void updateProblemTest() { | ||
25 | var solver = MPSolver.createSolver("GLOP"); | ||
26 | var x = solver.makeNumVar(0, Double.POSITIVE_INFINITY, "x"); | ||
27 | var y = solver.makeNumVar(0, 1, "y"); | ||
28 | var constraint = solver.makeConstraint(5, 5); | ||
29 | constraint.setCoefficient(x, 1); | ||
30 | constraint.setCoefficient(y, 1); | ||
31 | var objective = solver.objective(); | ||
32 | |||
33 | objective.setCoefficient(x, 1); | ||
34 | objective.setMinimization(); | ||
35 | assertThat(solver.solve(), is(MPSolver.ResultStatus.OPTIMAL)); | ||
36 | assertThat(objective.value(), closeTo(4, 0.01)); | ||
37 | |||
38 | objective.setMaximization(); | ||
39 | assertThat(solver.solve(), is(MPSolver.ResultStatus.OPTIMAL)); | ||
40 | assertThat(objective.value(), closeTo(5, 0.01)); | ||
41 | |||
42 | objective.setCoefficient(x, 0); | ||
43 | objective.setCoefficient(y, 1); | ||
44 | objective.setMinimization(); | ||
45 | assertThat(solver.solve(), is(MPSolver.ResultStatus.OPTIMAL)); | ||
46 | assertThat(objective.value(), closeTo(0, 0.01)); | ||
47 | |||
48 | objective.setMaximization(); | ||
49 | assertThat(solver.solve(), is(MPSolver.ResultStatus.OPTIMAL)); | ||
50 | assertThat(objective.value(), closeTo(1, 0.01)); | ||
51 | } | ||
52 | } | ||
diff --git a/subprojects/store-reasoning-scope/src/test/java/tools/refinery/store/reasoning/scope/MultiObjectTest.java b/subprojects/store-reasoning-scope/src/test/java/tools/refinery/store/reasoning/scope/MultiObjectTest.java new file mode 100644 index 00000000..42ce2f56 --- /dev/null +++ b/subprojects/store-reasoning-scope/src/test/java/tools/refinery/store/reasoning/scope/MultiObjectTest.java | |||
@@ -0,0 +1,206 @@ | |||
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 org.junit.jupiter.api.BeforeEach; | ||
9 | import org.junit.jupiter.api.Test; | ||
10 | import tools.refinery.store.model.Interpretation; | ||
11 | import tools.refinery.store.model.Model; | ||
12 | import tools.refinery.store.model.ModelStore; | ||
13 | import tools.refinery.store.query.viatra.ViatraModelQueryAdapter; | ||
14 | import tools.refinery.store.reasoning.ReasoningAdapter; | ||
15 | import tools.refinery.store.reasoning.ReasoningStoreAdapter; | ||
16 | import tools.refinery.store.reasoning.refinement.RefinementResult; | ||
17 | import tools.refinery.store.reasoning.representation.PartialRelation; | ||
18 | import tools.refinery.store.reasoning.seed.ModelSeed; | ||
19 | import tools.refinery.store.reasoning.translator.PartialRelationTranslator; | ||
20 | import tools.refinery.store.reasoning.translator.multiobject.MultiObjectTranslator; | ||
21 | import tools.refinery.store.representation.Symbol; | ||
22 | import tools.refinery.store.representation.TruthValue; | ||
23 | import tools.refinery.store.representation.cardinality.CardinalityInterval; | ||
24 | import tools.refinery.store.representation.cardinality.CardinalityIntervals; | ||
25 | import tools.refinery.store.tuple.Tuple; | ||
26 | |||
27 | import static org.hamcrest.MatcherAssert.assertThat; | ||
28 | import static org.hamcrest.Matchers.is; | ||
29 | |||
30 | class MultiObjectTest { | ||
31 | private static final PartialRelation person = new PartialRelation("Person", 1); | ||
32 | |||
33 | private ModelStore store; | ||
34 | private Model model; | ||
35 | private Interpretation<CardinalityInterval> countStorage; | ||
36 | |||
37 | @BeforeEach | ||
38 | void beforeEach() { | ||
39 | store = ModelStore.builder() | ||
40 | .with(ViatraModelQueryAdapter.builder()) | ||
41 | .with(ReasoningAdapter.builder()) | ||
42 | .with(new MultiObjectTranslator()) | ||
43 | .with(PartialRelationTranslator.of(person) | ||
44 | .symbol(Symbol.of("Person", 1, TruthValue.class, TruthValue.FALSE))) | ||
45 | .with(ScopePropagatorAdapter.builder() | ||
46 | .scope(person, CardinalityIntervals.between(5, 15))) | ||
47 | .build(); | ||
48 | model = null; | ||
49 | countStorage = null; | ||
50 | } | ||
51 | |||
52 | @Test | ||
53 | void oneMultiObjectSatisfiableTest() { | ||
54 | createModel(ModelSeed.builder(4) | ||
55 | .seed(MultiObjectTranslator.COUNT_SYMBOL, builder -> builder | ||
56 | .reducedValue(CardinalityIntervals.ONE) | ||
57 | .put(Tuple.of(0), CardinalityIntervals.SET)) | ||
58 | .seed(person, builder -> builder.reducedValue(TruthValue.TRUE)) | ||
59 | .build()); | ||
60 | assertThat(propagate(), is(RefinementResult.REFINED)); | ||
61 | assertThat(countStorage.get(Tuple.of(0)), is(CardinalityIntervals.between(2, 12))); | ||
62 | } | ||
63 | |||
64 | @Test | ||
65 | void oneMultiObjectExistingBoundSatisfiableTest() { | ||
66 | createModel(ModelSeed.builder(4) | ||
67 | .seed(MultiObjectTranslator.COUNT_SYMBOL, builder -> builder | ||
68 | .reducedValue(CardinalityIntervals.ONE) | ||
69 | .put(Tuple.of(0), CardinalityIntervals.between(5, 20))) | ||
70 | .seed(person, builder -> builder.reducedValue(TruthValue.TRUE)) | ||
71 | .build()); | ||
72 | assertThat(propagate(), is(RefinementResult.REFINED)); | ||
73 | assertThat(countStorage.get(Tuple.of(0)), is(CardinalityIntervals.between(5, 12))); | ||
74 | } | ||
75 | |||
76 | @Test | ||
77 | void oneMultiObjectUnsatisfiableUpperTest() { | ||
78 | createModel(ModelSeed.builder(21) | ||
79 | .seed(MultiObjectTranslator.COUNT_SYMBOL, builder -> builder | ||
80 | .reducedValue(CardinalityIntervals.ONE) | ||
81 | .put(Tuple.of(0), CardinalityIntervals.SET)) | ||
82 | .seed(person, builder -> builder.reducedValue(TruthValue.TRUE)) | ||
83 | .build()); | ||
84 | assertThat(propagate(), is(RefinementResult.REJECTED)); | ||
85 | } | ||
86 | |||
87 | @Test | ||
88 | void noMultiObjectSatisfiableTest() { | ||
89 | createModel(ModelSeed.builder(10) | ||
90 | .seed(MultiObjectTranslator.COUNT_SYMBOL, builder -> builder.reducedValue(CardinalityIntervals.ONE)) | ||
91 | .seed(person, builder -> builder.reducedValue(TruthValue.TRUE)) | ||
92 | .build()); | ||
93 | assertThat(propagate(), is(RefinementResult.UNCHANGED)); | ||
94 | } | ||
95 | |||
96 | @Test | ||
97 | void noMultiObjectUnsatisfiableTest() { | ||
98 | createModel(ModelSeed.builder(2) | ||
99 | .seed(MultiObjectTranslator.COUNT_SYMBOL, builder -> builder.reducedValue(CardinalityIntervals.ONE)) | ||
100 | .seed(person, builder -> builder.reducedValue(TruthValue.TRUE)) | ||
101 | .build()); | ||
102 | assertThat(propagate(), is(RefinementResult.REJECTED)); | ||
103 | } | ||
104 | |||
105 | @Test | ||
106 | void oneMultiObjectExistingBoundUnsatisfiableLowerTest() { | ||
107 | createModel(ModelSeed.builder(4) | ||
108 | .seed(MultiObjectTranslator.COUNT_SYMBOL, builder -> builder | ||
109 | .reducedValue(CardinalityIntervals.ONE) | ||
110 | .put(Tuple.of(0), CardinalityIntervals.atLeast(20))) | ||
111 | .seed(person, builder -> builder.reducedValue(TruthValue.TRUE)) | ||
112 | .build()); | ||
113 | assertThat(propagate(), is(RefinementResult.REJECTED)); | ||
114 | } | ||
115 | |||
116 | @Test | ||
117 | void oneMultiObjectExistingBoundUnsatisfiableUpperTest() { | ||
118 | createModel(ModelSeed.builder(4) | ||
119 | .seed(MultiObjectTranslator.COUNT_SYMBOL, builder -> builder | ||
120 | .reducedValue(CardinalityIntervals.ONE) | ||
121 | .put(Tuple.of(0), CardinalityIntervals.atMost(1))) | ||
122 | .seed(person, builder -> builder.reducedValue(TruthValue.TRUE)) | ||
123 | .build()); | ||
124 | assertThat(propagate(), is(RefinementResult.REJECTED)); | ||
125 | } | ||
126 | |||
127 | @Test | ||
128 | void twoMultiObjectsSatisfiableTest() { | ||
129 | createModel(ModelSeed.builder(5) | ||
130 | .seed(MultiObjectTranslator.COUNT_SYMBOL, builder -> builder | ||
131 | .reducedValue(CardinalityIntervals.ONE) | ||
132 | .put(Tuple.of(0), CardinalityIntervals.SET) | ||
133 | .put(Tuple.of(1), CardinalityIntervals.SET)) | ||
134 | .seed(person, builder -> builder.reducedValue(TruthValue.TRUE)) | ||
135 | .build()); | ||
136 | assertThat(propagate(), is(RefinementResult.REFINED)); | ||
137 | assertThat(countStorage.get(Tuple.of(0)), is(CardinalityIntervals.atMost(12))); | ||
138 | assertThat(countStorage.get(Tuple.of(1)), is(CardinalityIntervals.atMost(12))); | ||
139 | } | ||
140 | |||
141 | @Test | ||
142 | void twoMultiObjectsExistingBoundSatisfiableTest() { | ||
143 | createModel(ModelSeed.builder(5) | ||
144 | .seed(MultiObjectTranslator.COUNT_SYMBOL, builder -> builder | ||
145 | .reducedValue(CardinalityIntervals.ONE) | ||
146 | .put(Tuple.of(0), CardinalityIntervals.between(7, 20)) | ||
147 | .put(Tuple.of(1), CardinalityIntervals.atMost(11))) | ||
148 | .seed(person, builder -> builder.reducedValue(TruthValue.TRUE)) | ||
149 | .build()); | ||
150 | assertThat(propagate(), is(RefinementResult.REFINED)); | ||
151 | assertThat(countStorage.get(Tuple.of(0)), is(CardinalityIntervals.between(7, 12))); | ||
152 | assertThat(countStorage.get(Tuple.of(1)), is(CardinalityIntervals.atMost(5))); | ||
153 | } | ||
154 | |||
155 | @Test | ||
156 | void twoMultiObjectsExistingBoundUnsatisfiableUpperTest() { | ||
157 | createModel(ModelSeed.builder(5) | ||
158 | .seed(MultiObjectTranslator.COUNT_SYMBOL, builder -> builder | ||
159 | .reducedValue(CardinalityIntervals.ONE) | ||
160 | .put(Tuple.of(0), CardinalityIntervals.between(7, 20)) | ||
161 | .put(Tuple.of(1), CardinalityIntervals.exactly(11))) | ||
162 | .seed(person, builder -> builder.reducedValue(TruthValue.TRUE)) | ||
163 | .build()); | ||
164 | assertThat(propagate(), is(RefinementResult.REJECTED)); | ||
165 | } | ||
166 | |||
167 | @Test | ||
168 | void twoMultiObjectsExistingBoundUnsatisfiableLowerTest() { | ||
169 | createModel(ModelSeed.builder(3) | ||
170 | .seed(MultiObjectTranslator.COUNT_SYMBOL, builder -> builder | ||
171 | .reducedValue(CardinalityIntervals.ONE) | ||
172 | .put(Tuple.of(0), CardinalityIntervals.LONE) | ||
173 | .put(Tuple.of(1), CardinalityIntervals.atMost(2))) | ||
174 | .seed(person, builder -> builder.reducedValue(TruthValue.TRUE)) | ||
175 | .build()); | ||
176 | assertThat(propagate(), is(RefinementResult.REJECTED)); | ||
177 | } | ||
178 | |||
179 | @Test | ||
180 | void multiToSingleTest() { | ||
181 | createModel(ModelSeed.builder(5) | ||
182 | .seed(MultiObjectTranslator.COUNT_SYMBOL, builder -> builder | ||
183 | .reducedValue(CardinalityIntervals.ONE) | ||
184 | .put(Tuple.of(0), CardinalityIntervals.LONE) | ||
185 | .put(Tuple.of(1), CardinalityIntervals.SET)) | ||
186 | .seed(person, builder -> builder.reducedValue(TruthValue.TRUE)) | ||
187 | .build()); | ||
188 | assertThat(propagate(), is(RefinementResult.REFINED)); | ||
189 | assertThat(countStorage.get(Tuple.of(0)), is(CardinalityIntervals.LONE)); | ||
190 | assertThat(countStorage.get(Tuple.of(1)), is(CardinalityIntervals.between(1, 12))); | ||
191 | countStorage.put(Tuple.of(0), CardinalityIntervals.ONE); | ||
192 | assertThat(propagate(), is(RefinementResult.REFINED)); | ||
193 | assertThat(countStorage.get(Tuple.of(1)), is(CardinalityIntervals.between(1, 11))); | ||
194 | countStorage.put(Tuple.of(1), CardinalityIntervals.ONE); | ||
195 | assertThat(propagate(), is(RefinementResult.UNCHANGED)); | ||
196 | } | ||
197 | |||
198 | private void createModel(ModelSeed modelSeed) { | ||
199 | model = store.getAdapter(ReasoningStoreAdapter.class).createInitialModel(modelSeed); | ||
200 | countStorage = model.getInterpretation(MultiObjectTranslator.COUNT_STORAGE); | ||
201 | } | ||
202 | |||
203 | private RefinementResult propagate() { | ||
204 | return model.getAdapter(ScopePropagatorAdapter.class).propagate(); | ||
205 | } | ||
206 | } | ||
diff --git a/subprojects/store-reasoning-scope/src/test/java/tools/refinery/store/reasoning/scope/internal/RoundingUtilTest.java b/subprojects/store-reasoning-scope/src/test/java/tools/refinery/store/reasoning/scope/internal/RoundingUtilTest.java new file mode 100644 index 00000000..9daed660 --- /dev/null +++ b/subprojects/store-reasoning-scope/src/test/java/tools/refinery/store/reasoning/scope/internal/RoundingUtilTest.java | |||
@@ -0,0 +1,69 @@ | |||
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.internal; | ||
7 | |||
8 | import org.junit.jupiter.params.ParameterizedTest; | ||
9 | import org.junit.jupiter.params.provider.Arguments; | ||
10 | import org.junit.jupiter.params.provider.MethodSource; | ||
11 | |||
12 | import java.util.stream.Stream; | ||
13 | |||
14 | import static org.hamcrest.MatcherAssert.assertThat; | ||
15 | import static org.hamcrest.Matchers.is; | ||
16 | |||
17 | class RoundingUtilTest { | ||
18 | @ParameterizedTest | ||
19 | @MethodSource | ||
20 | void roundUpTest(double value, int expected) { | ||
21 | int actual = RoundingUtil.roundUp(value); | ||
22 | assertThat(actual, is(expected)); | ||
23 | } | ||
24 | |||
25 | static Stream<Arguments> roundUpTest() { | ||
26 | return Stream.of( | ||
27 | Arguments.of(0.0, 0), | ||
28 | Arguments.of(-0.0, 0), | ||
29 | Arguments.of(-0.9, 0), | ||
30 | Arguments.of(-2, 0), | ||
31 | Arguments.of(0.009, 0), | ||
32 | Arguments.of(0.011, 1), | ||
33 | Arguments.of(0.1, 1), | ||
34 | Arguments.of(0.991, 1), | ||
35 | Arguments.of(1, 1), | ||
36 | Arguments.of(1.009, 1), | ||
37 | Arguments.of(1.011, 2), | ||
38 | Arguments.of(1.5, 2), | ||
39 | Arguments.of(2, 2), | ||
40 | Arguments.of(100.5, 101) | ||
41 | ); | ||
42 | } | ||
43 | |||
44 | @ParameterizedTest | ||
45 | @MethodSource | ||
46 | void roundDownTest(double value, int expected) { | ||
47 | int actual = RoundingUtil.roundDown(value); | ||
48 | assertThat(actual, is(expected)); | ||
49 | } | ||
50 | |||
51 | static Stream<Arguments> roundDownTest() { | ||
52 | return Stream.of( | ||
53 | Arguments.of(0.0, 0), | ||
54 | Arguments.of(-0.0, 0), | ||
55 | Arguments.of(-0.9, 0), | ||
56 | Arguments.of(-2, 0), | ||
57 | Arguments.of(0.989, 0), | ||
58 | Arguments.of(0.991, 1), | ||
59 | Arguments.of(1, 1), | ||
60 | Arguments.of(1.5, 1), | ||
61 | Arguments.of(1.009, 1), | ||
62 | Arguments.of(1.989, 1), | ||
63 | Arguments.of(1.991, 2), | ||
64 | Arguments.of(2, 2), | ||
65 | Arguments.of(2.009, 2), | ||
66 | Arguments.of(100.5, 100) | ||
67 | ); | ||
68 | } | ||
69 | } | ||