diff options
author | Kristóf Marussy <kristof@marussy.com> | 2023-09-03 17:57:38 +0200 |
---|---|---|
committer | Kristóf Marussy <kristof@marussy.com> | 2023-09-03 17:57:38 +0200 |
commit | cd96a9a4f54d45cda3ddf5df474946445d557090 (patch) | |
tree | 7a96a177236888ede9a51ffdd51940a672cfd070 /subprojects/store-reasoning-scope | |
parent | build: runtimeOnly Eclipse Collections if posible (diff) | |
download | refinery-cd96a9a4f54d45cda3ddf5df474946445d557090.tar.gz refinery-cd96a9a4f54d45cda3ddf5df474946445d557090.tar.zst refinery-cd96a9a4f54d45cda3ddf5df474946445d557090.zip |
feat: scope propagator in language
Diffstat (limited to 'subprojects/store-reasoning-scope')
4 files changed, 59 insertions, 20 deletions
diff --git a/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/internal/MultiView.java b/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/internal/MultiView.java new file mode 100644 index 00000000..cea4e07d --- /dev/null +++ b/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/internal/MultiView.java | |||
@@ -0,0 +1,23 @@ | |||
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.view.TuplePreservingView; | ||
9 | import tools.refinery.store.representation.Symbol; | ||
10 | import tools.refinery.store.representation.cardinality.CardinalityInterval; | ||
11 | import tools.refinery.store.representation.cardinality.CardinalityIntervals; | ||
12 | import tools.refinery.store.tuple.Tuple; | ||
13 | |||
14 | class MultiView extends TuplePreservingView<CardinalityInterval> { | ||
15 | protected MultiView(Symbol<CardinalityInterval> symbol) { | ||
16 | super(symbol, "multi"); | ||
17 | } | ||
18 | |||
19 | @Override | ||
20 | protected boolean doFilter(Tuple key, CardinalityInterval value) { | ||
21 | return !CardinalityIntervals.ONE.equals(value); | ||
22 | } | ||
23 | } | ||
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 index 0d594701..c257df6b 100644 --- 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 | |||
@@ -210,10 +210,9 @@ class ScopePropagatorAdapterImpl implements ScopePropagatorAdapter { | |||
210 | UpperCardinality upperBound; | 210 | UpperCardinality upperBound; |
211 | switch (maximizationResult) { | 211 | switch (maximizationResult) { |
212 | case OPTIMAL -> upperBound = UpperCardinalities.atMost(RoundingUtil.roundDown(objective.value())); | 212 | case OPTIMAL -> upperBound = UpperCardinalities.atMost(RoundingUtil.roundDown(objective.value())); |
213 | case UNBOUNDED -> upperBound = UpperCardinalities.UNBOUNDED; | 213 | // Problem was feasible when minimizing, the only possible source of {@code UNBOUNDED_OR_INFEASIBLE} is |
214 | case INFEASIBLE -> { | 214 | // an unbounded maximization problem. See https://github.com/google/or-tools/issues/3319 |
215 | return RefinementResult.REJECTED; | 215 | case UNBOUNDED, INFEASIBLE -> upperBound = UpperCardinalities.UNBOUNDED; |
216 | } | ||
217 | default -> throw new IllegalStateException("Failed to solve for maximum of %s: %s" | 216 | default -> throw new IllegalStateException("Failed to solve for maximum of %s: %s" |
218 | .formatted(variable, minimizationResult)); | 217 | .formatted(variable, minimizationResult)); |
219 | } | 218 | } |
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 index f383ebeb..11ca7381 100644 --- 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 | |||
@@ -22,12 +22,6 @@ import tools.refinery.store.representation.cardinality.FiniteUpperCardinality; | |||
22 | 22 | ||
23 | import java.util.*; | 23 | import java.util.*; |
24 | 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> | 25 | public class ScopePropagatorBuilderImpl extends AbstractModelAdapterBuilder<ScopePropagatorStoreAdapter> |
32 | implements ScopePropagatorBuilder { | 26 | implements ScopePropagatorBuilder { |
33 | private Symbol<CardinalityInterval> countSymbol = MultiObjectTranslator.COUNT_STORAGE; | 27 | private Symbol<CardinalityInterval> countSymbol = MultiObjectTranslator.COUNT_STORAGE; |
@@ -66,16 +60,8 @@ public class ScopePropagatorBuilderImpl extends AbstractModelAdapterBuilder<Scop | |||
66 | 60 | ||
67 | @Override | 61 | @Override |
68 | protected void doConfigure(ModelStoreBuilder storeBuilder) { | 62 | protected void doConfigure(ModelStoreBuilder storeBuilder) { |
69 | var multiQuery = Query.of("MULTI", (builder, instance) -> builder | 63 | var multiQuery = Query.of("MULTI", (builder, instance) -> builder.clause( |
70 | .clause( | 64 | new MultiView(countSymbol).call(instance))); |
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()); | 65 | typeScopePropagatorFactories = new ArrayList<>(scopes.size()); |
80 | for (var entry : scopes.entrySet()) { | 66 | for (var entry : scopes.entrySet()) { |
81 | var type = entry.getKey(); | 67 | var type = entry.getKey(); |
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 index c9745d22..95c4ac68 100644 --- 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 | |||
@@ -49,4 +49,35 @@ class MPSolverTest { | |||
49 | assertThat(solver.solve(), is(MPSolver.ResultStatus.OPTIMAL)); | 49 | assertThat(solver.solve(), is(MPSolver.ResultStatus.OPTIMAL)); |
50 | assertThat(objective.value(), closeTo(1, 0.01)); | 50 | assertThat(objective.value(), closeTo(1, 0.01)); |
51 | } | 51 | } |
52 | |||
53 | @Test | ||
54 | void unboundedIsInfeasibleTest() { | ||
55 | var solver = MPSolver.createSolver("GLOP"); | ||
56 | var x = solver.makeNumVar(0, Double.POSITIVE_INFINITY, "x"); | ||
57 | var objective = solver.objective(); | ||
58 | objective.setCoefficient(x, 1); | ||
59 | |||
60 | objective.setMinimization(); | ||
61 | assertThat(solver.solve(), is(MPSolver.ResultStatus.OPTIMAL)); | ||
62 | assertThat(objective.value(), closeTo(0, 0.01)); | ||
63 | |||
64 | objective.setMaximization(); | ||
65 | assertThat(solver.solve(), is(MPSolver.ResultStatus.INFEASIBLE)); | ||
66 | } | ||
67 | |||
68 | @Test | ||
69 | void constantTest() { | ||
70 | var solver = MPSolver.createSolver("GLOP"); | ||
71 | var x = solver.makeNumVar(1, 1, "x"); | ||
72 | var objective = solver.objective(); | ||
73 | objective.setCoefficient(x, 1); | ||
74 | |||
75 | objective.setMinimization(); | ||
76 | assertThat(solver.solve(), is(MPSolver.ResultStatus.OPTIMAL)); | ||
77 | assertThat(objective.value(), closeTo(1, 0.01)); | ||
78 | |||
79 | objective.setMaximization(); | ||
80 | assertThat(solver.solve(), is(MPSolver.ResultStatus.OPTIMAL)); | ||
81 | assertThat(objective.value(), closeTo(1, 0.01)); | ||
82 | } | ||
52 | } | 83 | } |