feat: scope propagator in language

11 files changed, 165 insertions, 36 deletions

diff --git a/subprojects/frontend/src/editor/EditorTheme.ts b/subprojects/frontend/src/editor/EditorTheme.ts
index 308d5be0..055b62e2 100644
--- a/subprojects/frontend/src/editor/EditorTheme.ts
+++ b/subprojects/frontend/src/editor/EditorTheme.ts
@@ -105,7 +105,7 @@ export default styled('div', {
         color: theme.palette.text.primary,
       },
     },
-    '.tok-problem-abstract, .tok-problem-new': {
+    '.tok-problem-abstract': {
       fontStyle: 'italic',
     },
     '.tok-problem-containment': {
diff --git a/subprojects/frontend/src/graph/dotSource.ts b/subprojects/frontend/src/graph/dotSource.ts
index 963a9663..b24bca2f 100644
--- a/subprojects/frontend/src/graph/dotSource.ts
+++ b/subprojects/frontend/src/graph/dotSource.ts
@@ -20,8 +20,6 @@ function nodeName(graph: GraphStore, metadata: NodeMetadata): string {
   switch (metadata.kind) {
     case 'INDIVIDUAL':
       return `<b>${name}</b>`;
-    case 'NEW':
-      return `<i>${name}</i>`;
     default:
       return name;
   }
@@ -44,6 +42,7 @@ interface NodeData {
   exists: string;
   equalsSelf: string;
   unaryPredicates: Map<RelationMetadata, string>;
+  count: string;
 }
 
 function computeNodeData(graph: GraphStore): NodeData[] {
@@ -56,6 +55,7 @@ function computeNodeData(graph: GraphStore): NodeData[] {
     exists: 'FALSE',
     equalsSelf: 'FALSE',
     unaryPredicates: new Map(),
+    count: '[0]',
   }));
 
   relations.forEach((relation) => {
@@ -107,6 +107,15 @@ function computeNodeData(graph: GraphStore): NodeData[] {
     }
   });
 
+  partialInterpretation['builtin::count']?.forEach(([index, value]) => {
+    if (typeof index === 'number' && typeof value === 'string') {
+      const data = nodeData[index];
+      if (data !== undefined) {
+        data.count = value;
+      }
+    }
+  });
+
   return nodeData;
 }
 
@@ -132,9 +141,10 @@ function createNodes(graph: GraphStore, lines: string[]): void {
     const classes = classList.join(' ');
     const name = nodeName(graph, node);
     const border = node.kind === 'INDIVIDUAL' ? 2 : 1;
+    const count = data.equalsSelf !== 'TRUE' ? ` ${data.count}` : '';
     lines.push(`n${i} [id="${node.name}", class="${classes}", label=<
         <table border="${border}" cellborder="0" cellspacing="0" style="rounded" bgcolor="white">
-          <tr><td cellpadding="4.5" width="32" bgcolor="green">${name}</td></tr>`);
+          <tr><td cellpadding="4.5" width="32" bgcolor="green">${name}${count}</td></tr>`);
     if (data.unaryPredicates.size > 0) {
       lines.push(
         '<hr/><tr><td cellpadding="4.5"><table fixedsize="TRUE" align="left" border="0" cellborder="0" cellspacing="0" cellpadding="1.5">',
diff --git a/subprojects/language-semantics/build.gradle.kts b/subprojects/language-semantics/build.gradle.kts
index b6f3f709..4374f78c 100644
--- a/subprojects/language-semantics/build.gradle.kts
+++ b/subprojects/language-semantics/build.gradle.kts
@@ -14,5 +14,6 @@ dependencies {
         api(project(":refinery-store"))
         api(project(":refinery-store-query"))
         api(project(":refinery-store-reasoning"))
+        implementation(project(":refinery-store-reasoning-scope"))
         runtimeOnly(libs.eclipseCollections)
 }
diff --git a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/model/ModelInitializer.java b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/model/ModelInitializer.java
index 13e25d0a..89c41a8e 100644
--- a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/model/ModelInitializer.java
+++ b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/model/ModelInitializer.java
@@ -24,6 +24,7 @@ import tools.refinery.store.query.term.Variable;
 import tools.refinery.store.reasoning.ReasoningAdapter;
 import tools.refinery.store.reasoning.representation.AnyPartialSymbol;
 import tools.refinery.store.reasoning.representation.PartialRelation;
+import tools.refinery.store.reasoning.scope.ScopePropagatorBuilder;
 import tools.refinery.store.reasoning.seed.ModelSeed;
 import tools.refinery.store.reasoning.seed.Seed;
 import tools.refinery.store.reasoning.translator.containment.ContainmentHierarchyTranslator;
@@ -72,6 +73,8 @@ public class ModelInitializer {
 
         private Metamodel metamodel;
 
+        private Map<Tuple, CardinalityInterval> countSeed = new LinkedHashMap<>();
+
         private ModelSeed modelSeed;
 
         public Problem getProblem() {
@@ -135,6 +138,10 @@ public class ModelInitializer {
                         relationTrace.put(relation, partialRelation);
                         modelSeedBuilder.seed(partialRelation, info.toSeed(nodeCount));
                 }
+                collectScopes();
+                modelSeedBuilder.seed(MultiObjectTranslator.COUNT_SYMBOL, builder -> builder
+                                .reducedValue(CardinalityIntervals.SET)
+                                .putAll(countSeed));
                 modelSeed = modelSeedBuilder.build();
                 collectPredicates();
                 return modelSeed;
@@ -288,20 +295,26 @@ public class ModelInitializer {
                 CardinalityInterval interval;
                 if (problemMultiplicity == null) {
                         interval = CardinalityIntervals.LONE;
-                } else if (problemMultiplicity instanceof ExactMultiplicity exactMultiplicity) {
-                        interval = CardinalityIntervals.exactly(exactMultiplicity.getExactValue());
+                } else {
+                        interval = getCardinalityInterval(problemMultiplicity);
+                }
+                var constraint = getRelationInfo(referenceDeclaration.getInvalidMultiplicity()).partialRelation();
+                return ConstrainedMultiplicity.of(interval, constraint);
+        }
+
+        private static CardinalityInterval getCardinalityInterval(
+                        tools.refinery.language.model.problem.Multiplicity problemMultiplicity) {
+                if (problemMultiplicity instanceof ExactMultiplicity exactMultiplicity) {
+                        return CardinalityIntervals.exactly(exactMultiplicity.getExactValue());
                 } else if (problemMultiplicity instanceof RangeMultiplicity rangeMultiplicity) {
                         var upperBound = rangeMultiplicity.getUpperBound();
-                        interval = CardinalityIntervals.between(rangeMultiplicity.getLowerBound(),
+                        return CardinalityIntervals.between(rangeMultiplicity.getLowerBound(),
                                         upperBound < 0 ? UpperCardinalities.UNBOUNDED : UpperCardinalities.atMost(upperBound));
                 } else {
                         throw new TracedException(problemMultiplicity, "Unknown multiplicity");
                 }
-                var constraint = getRelationInfo(referenceDeclaration.getInvalidMultiplicity()).partialRelation();
-                return ConstrainedMultiplicity.of(interval, constraint);
         }
 
-
         private void collectAssertions() {
                 for (var statement : problem.getStatements()) {
                         if (statement instanceof ClassDeclaration classDeclaration) {
@@ -598,6 +611,50 @@ public class ModelInitializer {
                 return argumentList;
         }
 
+        private void collectScopes() {
+                for (var statement : problem.getStatements()) {
+                        if (statement instanceof ScopeDeclaration scopeDeclaration) {
+                                for (var typeScope : scopeDeclaration.getTypeScopes()) {
+                                        if (typeScope.isIncrement()) {
+                                                collectTypeScopeIncrement(typeScope);
+                                        } else {
+                                                collectTypeScope(typeScope);
+                                        }
+                                }
+                        }
+                }
+        }
+
+        private void collectTypeScopeIncrement(TypeScope typeScope) {
+                if (!(typeScope.getTargetType() instanceof ClassDeclaration classDeclaration)) {
+                        throw new TracedException(typeScope, "Target of incremental type scope must be a class declaration");
+                }
+                var newNode = classDeclaration.getNewNode();
+                if (newNode == null) {
+                        throw new TracedException(typeScope, "Target of incremental type scope must be concrete class");
+                }
+                int newNodeId = nodeTrace.get(newNode);
+                var type = relationTrace.get(classDeclaration);
+                var typeInfo = metamodel.typeHierarchy().getAnalysisResult(type);
+                if (!typeInfo.getDirectSubtypes().isEmpty()) {
+                        throw new TracedException(typeScope, "Target of incremental type scope cannot have any subclasses");
+                }
+                var interval = getCardinalityInterval(typeScope.getMultiplicity());
+                countSeed.compute(Tuple.of(newNodeId), (key, oldValue) ->
+                                oldValue == null ? interval : oldValue.meet(interval));
+        }
+
+        private void collectTypeScope(TypeScope typeScope) {
+                var scopePropagatorBuilder = storeBuilder.tryGetAdapter(ScopePropagatorBuilder.class).orElseThrow(
+                                () -> new TracedException(typeScope, "Type scopes require a ScopePropagatorBuilder"));
+                var type = relationTrace.get(typeScope.getTargetType());
+                if (type == null) {
+                        throw new TracedException(typeScope, "Unknown target type");
+                }
+                var interval = getCardinalityInterval(typeScope.getMultiplicity());
+                scopePropagatorBuilder.scope(type, interval);
+        }
+
         private record RelationInfo(PartialRelation partialRelation, MutableSeed<TruthValue> assertions,
                                                                 MutableSeed<TruthValue> defaultAssertions) {
                 public RelationInfo(String name, int arity, TruthValue value, TruthValue defaultValue) {
diff --git a/subprojects/language-web/build.gradle.kts b/subprojects/language-web/build.gradle.kts
index a4ccdd9f..9f772d41 100644
--- a/subprojects/language-web/build.gradle.kts
+++ b/subprojects/language-web/build.gradle.kts
@@ -19,6 +19,7 @@ dependencies {
         implementation(project(":refinery-language-ide"))
         implementation(project(":refinery-language-semantics"))
         implementation(project(":refinery-store-query-viatra"))
+        implementation(project(":refinery-store-reasoning-scope"))
         implementation(libs.gson)
         implementation(libs.jetty.server)
         implementation(libs.jetty.servlet)
diff --git a/subprojects/language-web/src/main/java/tools/refinery/language/web/semantics/SemanticsWorker.java b/subprojects/language-web/src/main/java/tools/refinery/language/web/semantics/SemanticsWorker.java
index 108b87dc..8470bb99 100644
--- a/subprojects/language-web/src/main/java/tools/refinery/language/web/semantics/SemanticsWorker.java
+++ b/subprojects/language-web/src/main/java/tools/refinery/language/web/semantics/SemanticsWorker.java
@@ -22,15 +22,18 @@ import tools.refinery.language.semantics.metadata.MetadataCreator;
 import tools.refinery.language.semantics.model.ModelInitializer;
 import tools.refinery.language.semantics.model.SemanticsUtils;
 import tools.refinery.language.semantics.model.TracedException;
+import tools.refinery.store.map.Cursor;
 import tools.refinery.store.model.Model;
 import tools.refinery.store.model.ModelStore;
 import tools.refinery.store.query.viatra.ViatraModelQueryAdapter;
 import tools.refinery.store.reasoning.ReasoningAdapter;
 import tools.refinery.store.reasoning.ReasoningStoreAdapter;
 import tools.refinery.store.reasoning.literal.Concreteness;
+import tools.refinery.store.reasoning.refinement.RefinementResult;
 import tools.refinery.store.reasoning.representation.PartialRelation;
+import tools.refinery.store.reasoning.scope.ScopePropagatorAdapter;
 import tools.refinery.store.reasoning.translator.TranslationException;
-import tools.refinery.store.representation.TruthValue;
+import tools.refinery.store.reasoning.translator.multiobject.MultiObjectTranslator;
 import tools.refinery.store.tuple.Tuple;
 import tools.refinery.viatra.runtime.CancellationToken;
 
@@ -75,7 +78,8 @@ class SemanticsWorker implements Callable<SemanticsResult> {
                                 .with(ViatraModelQueryAdapter.builder()
                                                 .cancellationToken(cancellationToken))
                                 .with(ReasoningAdapter.builder()
-                                                .requiredInterpretations(Concreteness.PARTIAL));
+                                                .requiredInterpretations(Concreteness.PARTIAL))
+                                .with(ScopePropagatorAdapter.builder());
                 cancellationToken.checkCancelled();
                 try {
                         var modelSeed = initializer.createModel(problem, builder);
@@ -90,6 +94,9 @@ class SemanticsWorker implements Callable<SemanticsResult> {
                         cancellationToken.checkCancelled();
                         var cancellableModelSeed = CancellableSeed.wrap(cancellationToken, modelSeed);
                         var model = store.getAdapter(ReasoningStoreAdapter.class).createInitialModel(cancellableModelSeed);
+                        if (model.getAdapter(ScopePropagatorAdapter.class).propagate() == RefinementResult.REJECTED) {
+                                return new SemanticsInternalErrorResult("Scopes are unsatisfiable");
+                        }
                         cancellationToken.checkCancelled();
                         var partialInterpretation = getPartialInterpretation(initializer, model);
 
@@ -113,13 +120,18 @@ class SemanticsWorker implements Callable<SemanticsResult> {
                         json.add(name, tuples);
                         cancellationToken.checkCancelled();
                 }
+                json.add("builtin::count", getCountJson(model));
                 return json;
         }
 
         private static JsonArray getTuplesJson(ReasoningAdapter adapter, PartialRelation partialSymbol) {
                 var interpretation = adapter.getPartialInterpretation(Concreteness.PARTIAL, partialSymbol);
                 var cursor = interpretation.getAll();
-                var map = new TreeMap<Tuple, TruthValue>();
+                return getTuplesJson(cursor);
+        }
+
+        private static JsonArray getTuplesJson(Cursor<Tuple, ?> cursor) {
+                var map = new TreeMap<Tuple, Object>();
                 while (cursor.move()) {
                         map.put(cursor.getKey(), cursor.getValue());
                 }
@@ -130,7 +142,7 @@ class SemanticsWorker implements Callable<SemanticsResult> {
                 return tuples;
         }
 
-        private static JsonArray toArray(Tuple tuple, TruthValue value) {
+        private static JsonArray toArray(Tuple tuple, Object value) {
                 int arity = tuple.getSize();
                 var json = new JsonArray(arity + 1);
                 for (int i = 0; i < arity; i++) {
@@ -140,6 +152,12 @@ class SemanticsWorker implements Callable<SemanticsResult> {
                 return json;
         }
 
+        private static JsonArray getCountJson(Model model) {
+                var interpretation = model.getInterpretation(MultiObjectTranslator.COUNT_STORAGE);
+                var cursor = interpretation.getAll();
+                return getTuplesJson(cursor);
+        }
+
         private SemanticsResult getTracedErrorResult(EObject sourceElement, String message) {
                 if (sourceElement == null || !problem.eResource().equals(sourceElement.eResource())) {
                         return new SemanticsInternalErrorResult(message);
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));
+        }
 }
diff --git a/subprojects/store/src/main/java/tools/refinery/store/representation/cardinality/NonEmptyCardinalityInterval.java b/subprojects/store/src/main/java/tools/refinery/store/representation/cardinality/NonEmptyCardinalityInterval.java
index 2e7780da..bfaeea25 100644
--- a/subprojects/store/src/main/java/tools/refinery/store/representation/cardinality/NonEmptyCardinalityInterval.java
+++ b/subprojects/store/src/main/java/tools/refinery/store/representation/cardinality/NonEmptyCardinalityInterval.java
@@ -83,7 +83,10 @@ public record NonEmptyCardinalityInterval(int lowerBound, UpperCardinality upper
 
         @Override
         public String toString() {
-                var closeBracket = upperBound instanceof UnboundedUpperCardinality ? ")" : "]";
-                return "[%d..%s%s".formatted(lowerBound, upperBound, closeBracket);
+                if (upperBound instanceof FiniteUpperCardinality finiteUpperCardinality &&
+                                finiteUpperCardinality.finiteUpperBound() == lowerBound) {
+                        return "[%d]".formatted(lowerBound);
+                }
+                return "[%d..%s]".formatted(lowerBound, upperBound);
         }
 }