feat: scope propagator in language

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 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.reasoning.scope.internal;
+
+import tools.refinery.store.query.view.TuplePreservingView;
+import tools.refinery.store.representation.Symbol;
+import tools.refinery.store.representation.cardinality.CardinalityInterval;
+import tools.refinery.store.representation.cardinality.CardinalityIntervals;
+import tools.refinery.store.tuple.Tuple;
+
+class MultiView extends TuplePreservingView<CardinalityInterval> {
+        protected MultiView(Symbol<CardinalityInterval> symbol) {
+                super(symbol, "multi");
+        }
+
+        @Override
+        protected boolean doFilter(Tuple key, CardinalityInterval value) {
+                return !CardinalityIntervals.ONE.equals(value);
+        }
+}
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 {
                         UpperCardinality upperBound;
                         switch (maximizationResult) {
                         case OPTIMAL -> upperBound = UpperCardinalities.atMost(RoundingUtil.roundDown(objective.value()));
-                        case UNBOUNDED -> upperBound = UpperCardinalities.UNBOUNDED;
-                        case INFEASIBLE -> {
-                                return RefinementResult.REJECTED;
-                        }
+                        // Problem was feasible when minimizing, the only possible source of {@code UNBOUNDED_OR_INFEASIBLE} is
+                        // an unbounded maximization problem. See https://github.com/google/or-tools/issues/3319
+                        case UNBOUNDED, INFEASIBLE -> upperBound = UpperCardinalities.UNBOUNDED;
                         default -> throw new IllegalStateException("Failed to solve for maximum of %s: %s"
                                         .formatted(variable, minimizationResult));
                         }
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;
 
 import java.util.*;
 
-import static tools.refinery.store.query.literal.Literals.not;
-import static tools.refinery.store.reasoning.ReasoningAdapter.EQUALS_SYMBOL;
-import static tools.refinery.store.reasoning.ReasoningAdapter.EXISTS_SYMBOL;
-import static tools.refinery.store.reasoning.literal.PartialLiterals.may;
-import static tools.refinery.store.reasoning.literal.PartialLiterals.must;
-
 public class ScopePropagatorBuilderImpl extends AbstractModelAdapterBuilder<ScopePropagatorStoreAdapter>
                 implements ScopePropagatorBuilder {
         private Symbol<CardinalityInterval> countSymbol = MultiObjectTranslator.COUNT_STORAGE;
@@ -66,16 +60,8 @@ public class ScopePropagatorBuilderImpl extends AbstractModelAdapterBuilder<Scop
 
         @Override
         protected void doConfigure(ModelStoreBuilder storeBuilder) {
-                var multiQuery = Query.of("MULTI", (builder, instance) -> builder
-                                .clause(
-                                                may(EXISTS_SYMBOL.call(instance)),
-                                                not(must(EXISTS_SYMBOL.call(instance)))
-                                )
-                                .clause(
-                                                may(EXISTS_SYMBOL.call(instance)),
-                                                not(must(EQUALS_SYMBOL.call(instance, instance)))
-                                )
-                );
+                var multiQuery = Query.of("MULTI", (builder, instance) -> builder.clause(
+                                new MultiView(countSymbol).call(instance)));
                 typeScopePropagatorFactories = new ArrayList<>(scopes.size());
                 for (var entry : scopes.entrySet()) {
                         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 {
                 assertThat(solver.solve(), is(MPSolver.ResultStatus.OPTIMAL));
                 assertThat(objective.value(), closeTo(1, 0.01));
         }
+
+        @Test
+        void unboundedIsInfeasibleTest() {
+                var solver = MPSolver.createSolver("GLOP");
+                var x = solver.makeNumVar(0, Double.POSITIVE_INFINITY, "x");
+                var objective = solver.objective();
+                objective.setCoefficient(x, 1);
+
+                objective.setMinimization();
+                assertThat(solver.solve(), is(MPSolver.ResultStatus.OPTIMAL));
+                assertThat(objective.value(), closeTo(0, 0.01));
+
+                objective.setMaximization();
+                assertThat(solver.solve(), is(MPSolver.ResultStatus.INFEASIBLE));
+        }
+
+        @Test
+        void constantTest() {
+                var solver = MPSolver.createSolver("GLOP");
+                var x = solver.makeNumVar(1, 1, "x");
+                var objective = solver.objective();
+                objective.setCoefficient(x, 1);
+
+                objective.setMinimization();
+                assertThat(solver.solve(), is(MPSolver.ResultStatus.OPTIMAL));
+                assertThat(objective.value(), closeTo(1, 0.01));
+
+                objective.setMaximization();
+                assertThat(solver.solve(), is(MPSolver.ResultStatus.OPTIMAL));
+                assertThat(objective.value(), closeTo(1, 0.01));
+        }
 }