feat: integrate DSE with partial interpretation

12 files changed, 95 insertions, 218 deletions

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/BoundScopePropagator.java
index 99c501ce..62aadb4a 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/BoundScopePropagator.java
@@ -3,7 +3,7 @@
  *
  * SPDX-License-Identifier: EPL-2.0
  */
-package tools.refinery.store.reasoning.scope.internal;
+package tools.refinery.store.reasoning.scope;
 
 import com.google.ortools.linearsolver.MPConstraint;
 import com.google.ortools.linearsolver.MPObjective;
@@ -13,18 +13,15 @@ import org.eclipse.collections.api.factory.primitive.IntObjectMaps;
 import org.eclipse.collections.api.factory.primitive.IntSets;
 import org.eclipse.collections.api.map.primitive.MutableIntObjectMap;
 import org.eclipse.collections.api.set.primitive.MutableIntSet;
+import tools.refinery.store.dse.propagation.BoundPropagator;
+import tools.refinery.store.dse.propagation.PropagationResult;
 import tools.refinery.store.model.Interpretation;
 import tools.refinery.store.model.Model;
 import tools.refinery.store.query.ModelQueryAdapter;
-import tools.refinery.store.reasoning.refinement.RefinementResult;
-import tools.refinery.store.reasoning.scope.ScopePropagatorAdapter;
-import tools.refinery.store.reasoning.scope.ScopePropagatorStoreAdapter;
 import tools.refinery.store.representation.cardinality.*;
 import tools.refinery.store.tuple.Tuple;
 
-class ScopePropagatorAdapterImpl implements ScopePropagatorAdapter {
-        private final Model model;
-        private final ScopePropagatorStoreAdapterImpl storeAdapter;
+class BoundScopePropagator implements BoundPropagator {
         private final ModelQueryAdapter queryEngine;
         private final Interpretation<CardinalityInterval> countInterpretation;
         private final MPSolver solver;
@@ -34,30 +31,22 @@ class ScopePropagatorAdapterImpl implements ScopePropagatorAdapter {
         private final TypeScopePropagator[] propagators;
         private boolean changed = true;
 
-        public ScopePropagatorAdapterImpl(Model model, ScopePropagatorStoreAdapterImpl storeAdapter) {
-                this.model = model;
-                this.storeAdapter = storeAdapter;
+        public BoundScopePropagator(Model model, ScopePropagator storeAdapter) {
                 queryEngine = model.getAdapter(ModelQueryAdapter.class);
                 countInterpretation = model.getInterpretation(storeAdapter.getCountSymbol());
                 solver = MPSolver.createSolver("GLOP");
                 objective = solver.objective();
                 initializeVariables();
                 countInterpretation.addListener(this::countChanged, true);
-                var propagatorFactories = storeAdapter.getPropagatorFactories();
+                var propagatorFactories = storeAdapter.getTypeScopePropagatorFactories();
                 propagators = new TypeScopePropagator[propagatorFactories.size()];
                 for (int i = 0; i < propagators.length; i++) {
                         propagators[i] = propagatorFactories.get(i).createPropagator(this);
                 }
         }
 
-        @Override
-        public Model getModel() {
-                return model;
-        }
-
-        @Override
-        public ScopePropagatorStoreAdapter getStoreAdapter() {
-                return storeAdapter;
+        ModelQueryAdapter getQueryEngine() {
+                return queryEngine;
         }
 
         private void initializeVariables() {
@@ -149,29 +138,16 @@ class ScopePropagatorAdapterImpl implements ScopePropagatorAdapter {
         }
 
         @Override
-        public RefinementResult propagate() {
-                var result = RefinementResult.UNCHANGED;
-                RefinementResult currentRoundResult;
-                do {
-                        currentRoundResult = propagateOne();
-                        result = result.andThen(currentRoundResult);
-                        if (result.isRejected()) {
-                                return result;
-                        }
-                } while (currentRoundResult != RefinementResult.UNCHANGED);
-                return result;
-        }
-
-        private RefinementResult propagateOne() {
+        public PropagationResult propagateOne() {
                 queryEngine.flushChanges();
                 if (!changed) {
-                        return RefinementResult.UNCHANGED;
+                        return PropagationResult.UNCHANGED;
                 }
                 changed = false;
                 for (var propagator : propagators) {
                         propagator.updateBounds();
                 }
-                var result = RefinementResult.UNCHANGED;
+                var result = PropagationResult.UNCHANGED;
                 if (activeVariables.isEmpty()) {
                         return checkEmptiness();
                 }
@@ -190,16 +166,16 @@ class ScopePropagatorAdapterImpl implements ScopePropagatorAdapter {
                 return result;
         }
 
-        private RefinementResult checkEmptiness() {
+        private PropagationResult checkEmptiness() {
                 var emptinessCheckingResult = solver.solve();
                 return switch (emptinessCheckingResult) {
-                        case OPTIMAL, UNBOUNDED -> RefinementResult.UNCHANGED;
-                        case INFEASIBLE -> RefinementResult.REJECTED;
+                        case OPTIMAL, UNBOUNDED -> PropagationResult.UNCHANGED;
+                        case INFEASIBLE -> PropagationResult.REJECTED;
                         default -> throw new IllegalStateException("Failed to check for consistency: " + emptinessCheckingResult);
                 };
         }
 
-        private RefinementResult propagateNode(int nodeId, MPVariable variable) {
+        private PropagationResult propagateNode(int nodeId, MPVariable variable) {
                 objective.setCoefficient(variable, 1);
                 try {
                         objective.setMinimization();
@@ -209,7 +185,7 @@ class ScopePropagatorAdapterImpl implements ScopePropagatorAdapter {
                         case OPTIMAL -> lowerBound = RoundingUtil.roundUp(objective.value());
                         case UNBOUNDED -> lowerBound = 0;
                         case INFEASIBLE -> {
-                                return RefinementResult.REJECTED;
+                                return PropagationResult.REJECTED;
                         }
                         default -> throw new IllegalStateException("Failed to solve for minimum of %s: %s"
                                         .formatted(variable, minimizationResult));
@@ -234,7 +210,7 @@ class ScopePropagatorAdapterImpl implements ScopePropagatorAdapter {
                                 throw new IllegalArgumentException("Failed to refine multiplicity %s of node %d to %s"
                                                 .formatted(oldInterval, nodeId, newInterval));
                         }
-                        return newInterval.equals(oldInterval) ? RefinementResult.UNCHANGED : RefinementResult.REFINED;
+                        return newInterval.equals(oldInterval) ? PropagationResult.UNCHANGED : PropagationResult.PROPAGATED;
                 } finally {
                         objective.setCoefficient(variable, 0);
                 }
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/LowerTypeScopePropagator.java
index 393c4b72..5d903f41 100644
--- 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/LowerTypeScopePropagator.java
@@ -3,7 +3,7 @@
  *
  * SPDX-License-Identifier: EPL-2.0
  */
-package tools.refinery.store.reasoning.scope.internal;
+package tools.refinery.store.reasoning.scope;
 
 import tools.refinery.store.dse.transition.DesignSpaceExplorationBuilder;
 import tools.refinery.store.dse.transition.objectives.Criteria;
@@ -28,7 +28,7 @@ import static tools.refinery.store.reasoning.translator.multiobject.MultiObjectT
 class LowerTypeScopePropagator extends TypeScopePropagator {
         private final int lowerBound;
 
-        private LowerTypeScopePropagator(ScopePropagatorAdapterImpl adapter, int lowerBound, RelationalQuery allQuery,
+        private LowerTypeScopePropagator(BoundScopePropagator adapter, int lowerBound, RelationalQuery allQuery,
                                                                          RelationalQuery multiQuery) {
                 super(adapter, allQuery, multiQuery);
                 this.lowerBound = lowerBound;
@@ -58,7 +58,7 @@ class LowerTypeScopePropagator extends TypeScopePropagator {
                 }
 
                 @Override
-                public TypeScopePropagator createPropagator(ScopePropagatorAdapterImpl adapter) {
+                public TypeScopePropagator createPropagator(BoundScopePropagator adapter) {
                         return new LowerTypeScopePropagator(adapter, lowerBound, allMay, multiMay);
                 }
 
@@ -72,10 +72,10 @@ class LowerTypeScopePropagator extends TypeScopePropagator {
                         super.configure(storeBuilder);
 
                         var requiredObjects = Query.of(type.name() + "#required", Integer.class, (builder, output) -> builder
-                                        .clause(Integer.class, currentCount -> List.of(
-                                                        new CountCandidateLowerBoundLiteral(currentCount, type, List.of(Variable.of())),
-                                                        output.assign(sub(currentCount, constant(lowerBound))),
-                                                        check(greater(currentCount, constant(0)))
+                                        .clause(Integer.class, candidateLowerBound -> List.of(
+                                                        new CountCandidateLowerBoundLiteral(candidateLowerBound, type, List.of(Variable.of())),
+                                                        output.assign(sub(constant(lowerBound), candidateLowerBound)),
+                                                        check(greater(output, constant(0)))
                                         )));
 
                         storeBuilder.getAdapter(ReasoningBuilder.class).objective(Objectives.value(requiredObjects));
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/RoundingUtil.java
index a6d663ea..986771a1 100644
--- 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/RoundingUtil.java
@@ -3,7 +3,7 @@
  *
  * SPDX-License-Identifier: EPL-2.0
  */
-package tools.refinery.store.reasoning.scope.internal;
+package tools.refinery.store.reasoning.scope;
 
 final class RoundingUtil {
         private static final double TOLERANCE = 0.01;
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/ScopePropagator.java
index 531a7440..25b1966c 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/ScopePropagator.java
@@ -3,15 +3,13 @@
  *
  * SPDX-License-Identifier: EPL-2.0
  */
-package tools.refinery.store.reasoning.scope.internal;
+package tools.refinery.store.reasoning.scope;
 
 import com.google.ortools.Loader;
-import tools.refinery.store.adapter.AbstractModelAdapterBuilder;
-import tools.refinery.store.model.ModelStore;
+import tools.refinery.store.dse.propagation.PropagationBuilder;
 import tools.refinery.store.model.ModelStoreBuilder;
+import tools.refinery.store.model.ModelStoreConfiguration;
 import tools.refinery.store.reasoning.representation.PartialRelation;
-import tools.refinery.store.reasoning.scope.ScopePropagatorBuilder;
-import tools.refinery.store.reasoning.scope.ScopePropagatorStoreAdapter;
 import tools.refinery.store.reasoning.translator.TranslationException;
 import tools.refinery.store.reasoning.translator.multiobject.MultiObjectTranslator;
 import tools.refinery.store.representation.Symbol;
@@ -20,14 +18,16 @@ import tools.refinery.store.representation.cardinality.FiniteUpperCardinality;
 
 import java.util.*;
 
-public class ScopePropagatorBuilderImpl extends AbstractModelAdapterBuilder<ScopePropagatorStoreAdapter>
-                implements ScopePropagatorBuilder {
-        private Symbol<CardinalityInterval> countSymbol = MultiObjectTranslator.COUNT_STORAGE;
+public class ScopePropagator implements ModelStoreConfiguration {
+        private final Symbol<CardinalityInterval> countSymbol;
         private final Map<PartialRelation, CardinalityInterval> scopes = new LinkedHashMap<>();
-        private List<TypeScopePropagator.Factory> typeScopePropagatorFactories;
+        private final List<TypeScopePropagator.Factory> typeScopePropagatorFactories = new ArrayList<>();
 
-        @Override
-        public ScopePropagatorBuilder countSymbol(Symbol<CardinalityInterval> countSymbol) {
+        public ScopePropagator() {
+                this(MultiObjectTranslator.COUNT_STORAGE);
+        }
+
+        public ScopePropagator(Symbol<CardinalityInterval> countSymbol) {
                 if (countSymbol.arity() != 1) {
                         throw new IllegalArgumentException("Count symbol must have arty 1, got %s with arity %d instead"
                                         .formatted(countSymbol, countSymbol.arity()));
@@ -39,11 +39,9 @@ public class ScopePropagatorBuilderImpl extends AbstractModelAdapterBuilder<Scop
                         throw new IllegalArgumentException("Count symbol must default value null");
                 }
                 this.countSymbol = countSymbol;
-                return this;
         }
 
-        @Override
-        public ScopePropagatorBuilder scope(PartialRelation type, CardinalityInterval interval) {
+        public ScopePropagator scope(PartialRelation type, CardinalityInterval interval) {
                 if (type.arity() != 1) {
                         throw new TranslationException(type, "Only types with arity 1 may have scopes, got %s with arity %d"
                                         .formatted(type, type.arity()));
@@ -56,9 +54,29 @@ public class ScopePropagatorBuilderImpl extends AbstractModelAdapterBuilder<Scop
                 return this;
         }
 
+        public ScopePropagator scopes(Map<PartialRelation, CardinalityInterval> scopes) {
+                return scopes(scopes.entrySet());
+        }
+
+        public ScopePropagator scopes(Collection<Map.Entry<PartialRelation, CardinalityInterval>> scopes) {
+                for (var entry : scopes) {
+                        scope(entry.getKey(), entry.getValue());
+                }
+                return this;
+        }
+
         @Override
-        protected void doConfigure(ModelStoreBuilder storeBuilder) {
-                typeScopePropagatorFactories = new ArrayList<>(scopes.size());
+        public void apply(ModelStoreBuilder storeBuilder) {
+                createTypeScopePropagatorFactories();
+                Loader.loadNativeLibraries();
+                for (var factory : typeScopePropagatorFactories) {
+                        factory.configure(storeBuilder);
+                }
+                storeBuilder.getAdapter(PropagationBuilder.class)
+                                .propagator(model -> new BoundScopePropagator(model, this));
+        }
+
+        private void createTypeScopePropagatorFactories() {
                 for (var entry : scopes.entrySet()) {
                         var type = entry.getKey();
                         var bounds = entry.getValue();
@@ -72,15 +90,13 @@ public class ScopePropagatorBuilderImpl extends AbstractModelAdapterBuilder<Scop
                                 typeScopePropagatorFactories.add(upperFactory);
                         }
                 }
-                for (var factory : typeScopePropagatorFactories) {
-                        factory.configure(storeBuilder);
-                }
         }
 
-        @Override
-        protected ScopePropagatorStoreAdapter doBuild(ModelStore store) {
-                Loader.loadNativeLibraries();
-                return new ScopePropagatorStoreAdapterImpl(store, countSymbol, Collections.unmodifiableMap(scopes),
-                                Collections.unmodifiableList(typeScopePropagatorFactories));
+        Symbol<CardinalityInterval> getCountSymbol() {
+                return countSymbol;
+        }
+
+        List<TypeScopePropagator.Factory> getTypeScopePropagatorFactories() {
+                return typeScopePropagatorFactories;
         }
 }
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
deleted file mode 100644
index c2d3f59e..00000000
--- a/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/ScopePropagatorAdapter.java
+++ /dev/null
@@ -1,21 +0,0 @@
-/*
- * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
- *
- * SPDX-License-Identifier: EPL-2.0
- */
-package tools.refinery.store.reasoning.scope;
-
-import tools.refinery.store.adapter.ModelAdapter;
-import tools.refinery.store.reasoning.refinement.RefinementResult;
-import tools.refinery.store.reasoning.scope.internal.ScopePropagatorBuilderImpl;
-
-public interface ScopePropagatorAdapter extends ModelAdapter {
-        @Override
-        ScopePropagatorStoreAdapter getStoreAdapter();
-
-        RefinementResult propagate();
-
-        static ScopePropagatorBuilder builder() {
-                return new ScopePropagatorBuilderImpl();
-        }
-}
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
deleted file mode 100644
index a17e04a4..00000000
--- a/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/ScopePropagatorBuilder.java
+++ /dev/null
@@ -1,21 +0,0 @@
-/*
- * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
- *
- * SPDX-License-Identifier: EPL-2.0
- */
-package tools.refinery.store.reasoning.scope;
-
-import tools.refinery.store.adapter.ModelAdapterBuilder;
-import tools.refinery.store.model.ModelStore;
-import tools.refinery.store.reasoning.representation.PartialRelation;
-import tools.refinery.store.representation.Symbol;
-import tools.refinery.store.representation.cardinality.CardinalityInterval;
-
-public interface ScopePropagatorBuilder extends ModelAdapterBuilder {
-        ScopePropagatorBuilder countSymbol(Symbol<CardinalityInterval> countSymbol);
-
-        ScopePropagatorBuilder scope(PartialRelation type, CardinalityInterval interval);
-
-        @Override
-        ScopePropagatorStoreAdapter build(ModelStore store);
-}
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
deleted file mode 100644
index 65d9c38d..00000000
--- a/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/ScopePropagatorStoreAdapter.java
+++ /dev/null
@@ -1,16 +0,0 @@
-/*
- * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
- *
- * SPDX-License-Identifier: EPL-2.0
- */
-package tools.refinery.store.reasoning.scope;
-
-import tools.refinery.store.adapter.ModelStoreAdapter;
-import tools.refinery.store.reasoning.representation.PartialRelation;
-import tools.refinery.store.representation.cardinality.CardinalityInterval;
-
-import java.util.Map;
-
-public interface ScopePropagatorStoreAdapter extends ModelStoreAdapter {
-        Map<PartialRelation, CardinalityInterval> getScopes();
-}
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/TypeScopePropagator.java
index cfb95829..db80be7f 100644
--- 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/TypeScopePropagator.java
@@ -3,11 +3,10 @@
  *
  * SPDX-License-Identifier: EPL-2.0
  */
-package tools.refinery.store.reasoning.scope.internal;
+package tools.refinery.store.reasoning.scope;
 
 import com.google.ortools.linearsolver.MPConstraint;
 import tools.refinery.store.model.ModelStoreBuilder;
-import tools.refinery.store.query.ModelQueryAdapter;
 import tools.refinery.store.query.ModelQueryBuilder;
 import tools.refinery.store.query.dnf.AnyQuery;
 import tools.refinery.store.query.dnf.RelationalQuery;
@@ -17,15 +16,15 @@ import tools.refinery.store.tuple.Tuple;
 import java.util.Collection;
 
 abstract class TypeScopePropagator {
-        private final ScopePropagatorAdapterImpl adapter;
+        private final BoundScopePropagator adapter;
         private final ResultSet<Boolean> allNodes;
         private final ResultSet<Boolean> multiNodes;
         protected final MPConstraint constraint;
 
-        protected TypeScopePropagator(ScopePropagatorAdapterImpl adapter, RelationalQuery allQuery,
-                                                           RelationalQuery multiQuery) {
+        protected TypeScopePropagator(BoundScopePropagator adapter, RelationalQuery allQuery,
+                                                                  RelationalQuery multiQuery) {
                 this.adapter = adapter;
-                var queryEngine = adapter.getModel().getAdapter(ModelQueryAdapter.class);
+                var queryEngine = adapter.getQueryEngine();
                 allNodes = queryEngine.getResultSet(allQuery);
                 multiNodes = queryEngine.getResultSet(multiQuery);
                 constraint = adapter.makeConstraint();
@@ -56,7 +55,7 @@ abstract class TypeScopePropagator {
         }
 
         public abstract static class Factory {
-                public abstract TypeScopePropagator createPropagator(ScopePropagatorAdapterImpl adapter);
+                public abstract TypeScopePropagator createPropagator(BoundScopePropagator adapter);
 
                 protected abstract Collection<AnyQuery> getQueries();
 
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/UpperTypeScopePropagator.java
index a0be0fb4..062f976c 100644
--- 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/UpperTypeScopePropagator.java
@@ -3,7 +3,7 @@
  *
  * SPDX-License-Identifier: EPL-2.0
  */
-package tools.refinery.store.reasoning.scope.internal;
+package tools.refinery.store.reasoning.scope;
 
 import tools.refinery.store.query.dnf.AnyQuery;
 import tools.refinery.store.query.dnf.Query;
@@ -19,7 +19,7 @@ import static tools.refinery.store.reasoning.translator.multiobject.MultiObjectT
 class UpperTypeScopePropagator extends TypeScopePropagator {
         private final int upperBound;
 
-        private UpperTypeScopePropagator(ScopePropagatorAdapterImpl adapter, int upperBound, RelationalQuery allQuery,
+        private UpperTypeScopePropagator(BoundScopePropagator adapter, int upperBound, RelationalQuery allQuery,
                                                                          RelationalQuery multiQuery) {
                 super(adapter, allQuery, multiQuery);
                 this.upperBound = upperBound;
@@ -47,7 +47,7 @@ class UpperTypeScopePropagator extends TypeScopePropagator {
                 }
 
                 @Override
-                public TypeScopePropagator createPropagator(ScopePropagatorAdapterImpl adapter) {
+                public TypeScopePropagator createPropagator(BoundScopePropagator adapter) {
                         return new UpperTypeScopePropagator(adapter, upperBound, allMust, multiMust);
                 }
 
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
deleted file mode 100644
index 282ffe6f..00000000
--- a/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/internal/ScopePropagatorStoreAdapterImpl.java
+++ /dev/null
@@ -1,58 +0,0 @@
-/*
- * 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.adapter.ModelAdapter;
-import tools.refinery.store.model.Model;
-import tools.refinery.store.model.ModelStore;
-import tools.refinery.store.reasoning.representation.PartialRelation;
-import tools.refinery.store.reasoning.scope.ScopePropagatorStoreAdapter;
-import tools.refinery.store.representation.Symbol;
-import tools.refinery.store.representation.cardinality.CardinalityInterval;
-
-import java.util.List;
-import java.util.Map;
-
-// Not a record, because we want to control getter visibility.
-@SuppressWarnings("ClassCanBeRecord")
-class ScopePropagatorStoreAdapterImpl implements ScopePropagatorStoreAdapter {
-        private final ModelStore store;
-        private final Symbol<CardinalityInterval> countSymbol;
-        private final Map<PartialRelation, CardinalityInterval> scopes;
-        private final List<TypeScopePropagator.Factory> propagatorFactories;
-
-        public ScopePropagatorStoreAdapterImpl(
-                        ModelStore store, Symbol<CardinalityInterval> countSymbol,
-                        Map<PartialRelation, CardinalityInterval> scopes, List<TypeScopePropagator.Factory> propagatorFactories) {
-                this.store = store;
-                this.countSymbol = countSymbol;
-                this.scopes = scopes;
-                this.propagatorFactories = propagatorFactories;
-        }
-
-        @Override
-        public ModelStore getStore() {
-                return store;
-        }
-
-        Symbol<CardinalityInterval> getCountSymbol() {
-                return countSymbol;
-        }
-
-        @Override
-        public Map<PartialRelation, CardinalityInterval> getScopes() {
-                return scopes;
-        }
-
-        public List<TypeScopePropagator.Factory> getPropagatorFactories() {
-                return propagatorFactories;
-        }
-
-        @Override
-        public ModelAdapter createModelAdapter(Model model) {
-                return new ScopePropagatorAdapterImpl(model, this);
-        }
-}
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
index 42ce2f56..5fc70ae1 100644
--- 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
@@ -7,13 +7,14 @@ package tools.refinery.store.reasoning.scope;
 
 import org.junit.jupiter.api.BeforeEach;
 import org.junit.jupiter.api.Test;
+import tools.refinery.store.dse.propagation.PropagationAdapter;
+import tools.refinery.store.dse.propagation.PropagationResult;
 import tools.refinery.store.model.Interpretation;
 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.refinement.RefinementResult;
 import tools.refinery.store.reasoning.representation.PartialRelation;
 import tools.refinery.store.reasoning.seed.ModelSeed;
 import tools.refinery.store.reasoning.translator.PartialRelationTranslator;
@@ -38,11 +39,12 @@ class MultiObjectTest {
         void beforeEach() {
                 store = ModelStore.builder()
                                 .with(ViatraModelQueryAdapter.builder())
+                                .with(PropagationAdapter.builder())
                                 .with(ReasoningAdapter.builder())
                                 .with(new MultiObjectTranslator())
                                 .with(PartialRelationTranslator.of(person)
                                                 .symbol(Symbol.of("Person", 1, TruthValue.class, TruthValue.FALSE)))
-                                .with(ScopePropagatorAdapter.builder()
+                                .with(new ScopePropagator()
                                                 .scope(person, CardinalityIntervals.between(5, 15)))
                                 .build();
                 model = null;
@@ -57,7 +59,7 @@ class MultiObjectTest {
                                                 .put(Tuple.of(0), CardinalityIntervals.SET))
                                 .seed(person, builder -> builder.reducedValue(TruthValue.TRUE))
                                 .build());
-                assertThat(propagate(), is(RefinementResult.REFINED));
+                assertThat(propagate(), is(PropagationResult.PROPAGATED));
                 assertThat(countStorage.get(Tuple.of(0)), is(CardinalityIntervals.between(2, 12)));
         }
 
@@ -69,7 +71,7 @@ class MultiObjectTest {
                                                 .put(Tuple.of(0), CardinalityIntervals.between(5, 20)))
                                 .seed(person, builder -> builder.reducedValue(TruthValue.TRUE))
                                 .build());
-                assertThat(propagate(), is(RefinementResult.REFINED));
+                assertThat(propagate(), is(PropagationResult.PROPAGATED));
                 assertThat(countStorage.get(Tuple.of(0)), is(CardinalityIntervals.between(5, 12)));
         }
 
@@ -81,7 +83,7 @@ class MultiObjectTest {
                                                 .put(Tuple.of(0), CardinalityIntervals.SET))
                                 .seed(person, builder -> builder.reducedValue(TruthValue.TRUE))
                                 .build());
-                assertThat(propagate(), is(RefinementResult.REJECTED));
+                assertThat(propagate(), is(PropagationResult.REJECTED));
         }
 
         @Test
@@ -90,7 +92,7 @@ class MultiObjectTest {
                                 .seed(MultiObjectTranslator.COUNT_SYMBOL, builder -> builder.reducedValue(CardinalityIntervals.ONE))
                                 .seed(person, builder -> builder.reducedValue(TruthValue.TRUE))
                                 .build());
-                assertThat(propagate(), is(RefinementResult.UNCHANGED));
+                assertThat(propagate(), is(PropagationResult.UNCHANGED));
         }
 
         @Test
@@ -99,7 +101,7 @@ class MultiObjectTest {
                                 .seed(MultiObjectTranslator.COUNT_SYMBOL, builder -> builder.reducedValue(CardinalityIntervals.ONE))
                                 .seed(person, builder -> builder.reducedValue(TruthValue.TRUE))
                                 .build());
-                assertThat(propagate(), is(RefinementResult.REJECTED));
+                assertThat(propagate(), is(PropagationResult.REJECTED));
         }
 
         @Test
@@ -110,7 +112,7 @@ class MultiObjectTest {
                                                 .put(Tuple.of(0), CardinalityIntervals.atLeast(20)))
                                 .seed(person, builder -> builder.reducedValue(TruthValue.TRUE))
                                 .build());
-                assertThat(propagate(), is(RefinementResult.REJECTED));
+                assertThat(propagate(), is(PropagationResult.REJECTED));
         }
 
         @Test
@@ -121,7 +123,7 @@ class MultiObjectTest {
                                                 .put(Tuple.of(0), CardinalityIntervals.atMost(1)))
                                 .seed(person, builder -> builder.reducedValue(TruthValue.TRUE))
                                 .build());
-                assertThat(propagate(), is(RefinementResult.REJECTED));
+                assertThat(propagate(), is(PropagationResult.REJECTED));
         }
 
         @Test
@@ -133,7 +135,7 @@ class MultiObjectTest {
                                                 .put(Tuple.of(1), CardinalityIntervals.SET))
                                 .seed(person, builder -> builder.reducedValue(TruthValue.TRUE))
                                 .build());
-                assertThat(propagate(), is(RefinementResult.REFINED));
+                assertThat(propagate(), is(PropagationResult.PROPAGATED));
                 assertThat(countStorage.get(Tuple.of(0)), is(CardinalityIntervals.atMost(12)));
                 assertThat(countStorage.get(Tuple.of(1)), is(CardinalityIntervals.atMost(12)));
         }
@@ -147,7 +149,7 @@ class MultiObjectTest {
                                                 .put(Tuple.of(1), CardinalityIntervals.atMost(11)))
                                 .seed(person, builder -> builder.reducedValue(TruthValue.TRUE))
                                 .build());
-                assertThat(propagate(), is(RefinementResult.REFINED));
+                assertThat(propagate(), is(PropagationResult.PROPAGATED));
                 assertThat(countStorage.get(Tuple.of(0)), is(CardinalityIntervals.between(7, 12)));
                 assertThat(countStorage.get(Tuple.of(1)), is(CardinalityIntervals.atMost(5)));
         }
@@ -161,7 +163,7 @@ class MultiObjectTest {
                                                 .put(Tuple.of(1), CardinalityIntervals.exactly(11)))
                                 .seed(person, builder -> builder.reducedValue(TruthValue.TRUE))
                                 .build());
-                assertThat(propagate(), is(RefinementResult.REJECTED));
+                assertThat(propagate(), is(PropagationResult.REJECTED));
         }
 
         @Test
@@ -173,7 +175,7 @@ class MultiObjectTest {
                                                 .put(Tuple.of(1), CardinalityIntervals.atMost(2)))
                                 .seed(person, builder -> builder.reducedValue(TruthValue.TRUE))
                                 .build());
-                assertThat(propagate(), is(RefinementResult.REJECTED));
+                assertThat(propagate(), is(PropagationResult.REJECTED));
         }
 
         @Test
@@ -185,14 +187,14 @@ class MultiObjectTest {
                                                 .put(Tuple.of(1), CardinalityIntervals.SET))
                                 .seed(person, builder -> builder.reducedValue(TruthValue.TRUE))
                                 .build());
-                assertThat(propagate(), is(RefinementResult.REFINED));
+                assertThat(propagate(), is(PropagationResult.PROPAGATED));
                 assertThat(countStorage.get(Tuple.of(0)), is(CardinalityIntervals.LONE));
                 assertThat(countStorage.get(Tuple.of(1)), is(CardinalityIntervals.between(1, 12)));
                 countStorage.put(Tuple.of(0), CardinalityIntervals.ONE);
-                assertThat(propagate(), is(RefinementResult.REFINED));
+                assertThat(propagate(), is(PropagationResult.PROPAGATED));
                 assertThat(countStorage.get(Tuple.of(1)), is(CardinalityIntervals.between(1, 11)));
                 countStorage.put(Tuple.of(1), CardinalityIntervals.ONE);
-                assertThat(propagate(), is(RefinementResult.UNCHANGED));
+                assertThat(propagate(), is(PropagationResult.UNCHANGED));
         }
 
         private void createModel(ModelSeed modelSeed) {
@@ -200,7 +202,7 @@ class MultiObjectTest {
                 countStorage = model.getInterpretation(MultiObjectTranslator.COUNT_STORAGE);
         }
 
-        private RefinementResult propagate() {
-                return model.getAdapter(ScopePropagatorAdapter.class).propagate();
+        private PropagationResult propagate() {
+                return model.getAdapter(PropagationAdapter.class).propagate();
         }
 }
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/RoundingUtilTest.java
index 9daed660..e697298e 100644
--- 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/RoundingUtilTest.java
@@ -3,7 +3,7 @@
  *
  * SPDX-License-Identifier: EPL-2.0
  */
-package tools.refinery.store.reasoning.scope.internal;
+package tools.refinery.store.reasoning.scope;
 
 import org.junit.jupiter.params.ParameterizedTest;
 import org.junit.jupiter.params.provider.Arguments;