feat: basic partial interpretation infrastructure

65 files changed, 1968 insertions, 795 deletions

diff --git a/subprojects/store-reasoning/build.gradle.kts b/subprojects/store-reasoning/build.gradle.kts
index 6c568df0..5885da83 100644
--- a/subprojects/store-reasoning/build.gradle.kts
+++ b/subprojects/store-reasoning/build.gradle.kts
@@ -11,4 +11,5 @@ plugins {
 dependencies {
         api(project(":refinery-store-query"))
         testImplementation(testFixtures(project(":refinery-store-query")))
+        testImplementation(project(":refinery-store-query-viatra"))
 }
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/MergeResult.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/MergeResult.java
deleted file mode 100644
index d3a216d8..00000000
--- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/MergeResult.java
+++ /dev/null
@@ -1,20 +0,0 @@
-/*
- * SPDX-FileCopyrightText: 2021-2023 The Refinery Authors <https://refinery.tools/>
- *
- * SPDX-License-Identifier: EPL-2.0
- */
-package tools.refinery.store.reasoning;
-
-public enum MergeResult {
-        UNCHANGED,
-        REFINED,
-        REJECTED;
-
-        public MergeResult andAlso(MergeResult other) {
-                return switch (this) {
-                        case UNCHANGED -> other;
-                        case REFINED -> other == REJECTED ? REJECTED : REFINED;
-                        case REJECTED -> REJECTED;
-                };
-        }
-}
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/ReasoningAdapter.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/ReasoningAdapter.java
index 66e809f7..17aec09c 100644
--- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/ReasoningAdapter.java
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/ReasoningAdapter.java
@@ -5,27 +5,46 @@
  */
 package tools.refinery.store.reasoning;
 
+import org.jetbrains.annotations.Nullable;
 import tools.refinery.store.adapter.ModelAdapter;
-import tools.refinery.store.query.resultset.ResultSet;
-import tools.refinery.store.query.dnf.Dnf;
+import tools.refinery.store.reasoning.internal.ReasoningBuilderImpl;
+import tools.refinery.store.reasoning.interpretation.AnyPartialInterpretation;
+import tools.refinery.store.reasoning.interpretation.PartialInterpretation;
+import tools.refinery.store.reasoning.literal.Concreteness;
+import tools.refinery.store.reasoning.refinement.AnyPartialInterpretationRefiner;
+import tools.refinery.store.reasoning.refinement.PartialInterpretationRefiner;
 import tools.refinery.store.reasoning.representation.AnyPartialSymbol;
 import tools.refinery.store.reasoning.representation.PartialRelation;
 import tools.refinery.store.reasoning.representation.PartialSymbol;
+import tools.refinery.store.tuple.Tuple1;
 
 public interface ReasoningAdapter extends ModelAdapter {
-        PartialRelation EXISTS = PartialSymbol.of("exists", 1);
-        PartialRelation EQUALS = PartialSymbol.of("equals", 2);
+        PartialRelation EXISTS_SYMBOL = PartialSymbol.of("exists", 1);
+        PartialRelation EQUALS_SYMBOL = PartialSymbol.of("equals", 2);
 
         @Override
         ReasoningStoreAdapter getStoreAdapter();
 
-        default AnyPartialInterpretation getPartialInterpretation(AnyPartialSymbol partialSymbol) {
-                // Cast to disambiguate overloads.
-                var typedPartialSymbol = (PartialSymbol<?, ?>) partialSymbol;
-                return getPartialInterpretation(typedPartialSymbol);
+        default AnyPartialInterpretation getPartialInterpretation(Concreteness concreteness,
+                                                                                                                          AnyPartialSymbol partialSymbol) {
+                return getPartialInterpretation(concreteness, (PartialSymbol<?, ?>) partialSymbol);
         }
 
-        <A, C> PartialInterpretation<A, C> getPartialInterpretation(PartialSymbol<A, C> partialSymbol);
+        <A, C> PartialInterpretation<A, C> getPartialInterpretation(Concreteness concreteness,
+                                                                                                                                PartialSymbol<A, C> partialSymbol);
 
-        ResultSet<Boolean> getLiftedResultSet(Dnf query);
+        default AnyPartialInterpretationRefiner getRefiner(AnyPartialSymbol partialSymbol) {
+                return getRefiner((PartialSymbol<?, ?>) partialSymbol);
+        }
+
+        <A, C> PartialInterpretationRefiner<A, C> getRefiner(PartialSymbol<A, C> partialSymbol);
+
+        @Nullable
+        Tuple1 split(int parentMultiObject);
+
+        boolean cleanup(int nodeToDelete);
+
+        static ReasoningBuilder builder() {
+                return new ReasoningBuilderImpl();
+        }
 }
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/ReasoningBuilder.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/ReasoningBuilder.java
index d3a337e8..6d416436 100644
--- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/ReasoningBuilder.java
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/ReasoningBuilder.java
@@ -7,26 +7,28 @@ package tools.refinery.store.reasoning;
 
 import tools.refinery.store.adapter.ModelAdapterBuilder;
 import tools.refinery.store.model.ModelStore;
-import tools.refinery.store.reasoning.literal.Modality;
 import tools.refinery.store.query.dnf.Dnf;
-
-import java.util.Collection;
-import java.util.List;
+import tools.refinery.store.query.dnf.Query;
+import tools.refinery.store.reasoning.literal.Concreteness;
+import tools.refinery.store.reasoning.literal.Modality;
+import tools.refinery.store.reasoning.refinement.PartialModelInitializer;
+import tools.refinery.store.reasoning.refinement.StorageRefiner;
+import tools.refinery.store.reasoning.translator.AnyPartialSymbolTranslator;
+import tools.refinery.store.representation.Symbol;
 
 @SuppressWarnings("UnusedReturnValue")
 public interface ReasoningBuilder extends ModelAdapterBuilder {
-        default ReasoningBuilder liftedQueries(Dnf... liftedQueries) {
-                return liftedQueries(List.of(liftedQueries));
-        }
+        ReasoningBuilder initialNodeCount(int nodeCount);
+
+        ReasoningBuilder partialSymbol(AnyPartialSymbolTranslator translator);
+
+        <T> ReasoningBuilder storageRefiner(Symbol<T> symbol, StorageRefiner.Factory<T> refiner);
 
-        default ReasoningBuilder liftedQueries(Collection<Dnf> liftedQueries) {
-                liftedQueries.forEach(this::liftedQuery);
-                return this;
-        }
+        ReasoningBuilder initializer(PartialModelInitializer initializer);
 
-        ReasoningBuilder liftedQuery(Dnf liftedQuery);
+        <T> Query<T> lift(Modality modality, Concreteness concreteness, Query<T> query);
 
-        Dnf lift(Modality modality, Dnf query);
+        Dnf lift(Modality modality, Concreteness concreteness, Dnf dnf);
 
         @Override
         ReasoningStoreAdapter build(ModelStore store);
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/ReasoningStoreAdapter.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/ReasoningStoreAdapter.java
index c9795255..fae60d9e 100644
--- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/ReasoningStoreAdapter.java
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/ReasoningStoreAdapter.java
@@ -8,14 +8,15 @@ package tools.refinery.store.reasoning;
 import tools.refinery.store.adapter.ModelStoreAdapter;
 import tools.refinery.store.model.Model;
 import tools.refinery.store.reasoning.representation.AnyPartialSymbol;
-import tools.refinery.store.query.dnf.Dnf;
 
 import java.util.Collection;
 
 public interface ReasoningStoreAdapter extends ModelStoreAdapter {
         Collection<AnyPartialSymbol> getPartialSymbols();
 
-        Collection<Dnf> getLiftedQueries();
+        Collection<AnyPartialSymbol> getRefinablePartialSymbols();
+
+        Model createInitialModel();
 
         @Override
         ReasoningAdapter createModelAdapter(Model model);
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/internal/PartialQueryRewriter.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/internal/PartialQueryRewriter.java
new file mode 100644
index 00000000..132022d1
--- /dev/null
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/internal/PartialQueryRewriter.java
@@ -0,0 +1,103 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.reasoning.internal;
+
+import tools.refinery.store.query.dnf.Dnf;
+import tools.refinery.store.query.dnf.DnfClause;
+import tools.refinery.store.query.literal.AbstractCallLiteral;
+import tools.refinery.store.query.literal.Literal;
+import tools.refinery.store.query.rewriter.AbstractRecursiveRewriter;
+import tools.refinery.store.reasoning.interpretation.PartialRelationRewriter;
+import tools.refinery.store.reasoning.lifting.DnfLifter;
+import tools.refinery.store.reasoning.literal.Concreteness;
+import tools.refinery.store.reasoning.literal.ModalConstraint;
+import tools.refinery.store.reasoning.literal.Modality;
+import tools.refinery.store.reasoning.representation.PartialRelation;
+
+import java.util.*;
+
+class PartialQueryRewriter extends AbstractRecursiveRewriter {
+        private final DnfLifter lifter;
+        private final Map<PartialRelation, PartialRelationRewriter> relationRewriterMap = new HashMap<>();
+
+        PartialQueryRewriter(DnfLifter lifter) {
+                this.lifter = lifter;
+        }
+
+        public void addRelationRewriter(PartialRelation partialRelation, PartialRelationRewriter interpreter) {
+                if (relationRewriterMap.put(partialRelation, interpreter) != null) {
+                        throw new IllegalArgumentException("Duplicate partial relation: " + partialRelation);
+                }
+        }
+
+        @Override
+        protected Dnf doRewrite(Dnf dnf) {
+                var builder = Dnf.builderFrom(dnf);
+                for (var clause : dnf.getClauses()) {
+                        builder.clause(rewriteClause(clause));
+                }
+                return builder.build();
+        }
+
+        private List<Literal> rewriteClause(DnfClause clause) {
+                var completedLiterals = new ArrayList<Literal>();
+                var workList = new ArrayDeque<>(clause.literals());
+                while (!workList.isEmpty()) {
+                        var literal = workList.removeFirst();
+                        rewrite(literal, completedLiterals, workList);
+                }
+                return completedLiterals;
+        }
+
+        private void rewrite(Literal literal, List<Literal> completedLiterals, Deque<Literal> workList) {
+                if (!(literal instanceof AbstractCallLiteral callLiteral)) {
+                        completedLiterals.add(literal);
+                        return;
+                }
+                var target = callLiteral.getTarget();
+                if (target instanceof Dnf dnf) {
+                        rewriteRecursively(callLiteral, dnf, completedLiterals);
+                } else if (target instanceof ModalConstraint modalConstraint) {
+                        var modality = modalConstraint.modality();
+                        var concreteness = modalConstraint.concreteness();
+                        var constraint = modalConstraint.constraint();
+                        if (constraint instanceof Dnf dnf) {
+                                rewriteRecursively(callLiteral, modality, concreteness, dnf, completedLiterals);
+                        } else if (constraint instanceof PartialRelation partialRelation) {
+                                rewrite(callLiteral, modality, concreteness, partialRelation, workList);
+                        } else {
+                                throw new IllegalArgumentException("Cannot interpret modal constraint: " + modalConstraint);
+                        }
+                } else {
+                        completedLiterals.add(literal);
+                }
+        }
+
+        private void rewriteRecursively(AbstractCallLiteral callLiteral, Modality modality, Concreteness concreteness,
+                                                                        Dnf dnf, List<Literal> completedLiterals) {
+                var liftedDnf = lifter.lift(modality, concreteness, dnf);
+                rewriteRecursively(callLiteral, liftedDnf, completedLiterals);
+        }
+
+        private void rewriteRecursively(AbstractCallLiteral callLiteral, Dnf dnf, List<Literal> completedLiterals) {
+                var rewrittenDnf = rewrite(dnf);
+                var rewrittenLiteral = callLiteral.withTarget(rewrittenDnf);
+                completedLiterals.add(rewrittenLiteral);
+        }
+
+        private void rewrite(AbstractCallLiteral callLiteral, Modality modality, Concreteness concreteness,
+                                                 PartialRelation partialRelation, Deque<Literal> workList) {
+                var rewriter = relationRewriterMap.get(partialRelation);
+                if (rewriter == null) {
+                        throw new IllegalArgumentException("Do not know how to interpret partial relation: " + partialRelation);
+                }
+                var literals = rewriter.rewriteLiteral(callLiteral, modality, concreteness);
+                int length = literals.size();
+                for (int i = length - 1; i >= 0; i--) {
+                        workList.addFirst(literals.get(i));
+                }
+        }
+}
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/internal/ReasoningAdapterImpl.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/internal/ReasoningAdapterImpl.java
index 1bd3ad2e..396c2dcc 100644
--- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/internal/ReasoningAdapterImpl.java
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/internal/ReasoningAdapterImpl.java
@@ -5,20 +5,99 @@
  */
 package tools.refinery.store.reasoning.internal;
 
+import org.jetbrains.annotations.Nullable;
+import tools.refinery.store.model.Interpretation;
 import tools.refinery.store.model.Model;
 import tools.refinery.store.reasoning.ReasoningAdapter;
-import tools.refinery.store.reasoning.PartialInterpretation;
+import tools.refinery.store.reasoning.interpretation.AnyPartialInterpretation;
+import tools.refinery.store.reasoning.interpretation.PartialInterpretation;
+import tools.refinery.store.reasoning.literal.Concreteness;
+import tools.refinery.store.reasoning.refinement.AnyPartialInterpretationRefiner;
+import tools.refinery.store.reasoning.refinement.PartialInterpretationRefiner;
+import tools.refinery.store.reasoning.refinement.StorageRefiner;
+import tools.refinery.store.reasoning.representation.AnyPartialSymbol;
 import tools.refinery.store.reasoning.representation.PartialSymbol;
-import tools.refinery.store.query.dnf.Dnf;
-import tools.refinery.store.query.resultset.ResultSet;
+import tools.refinery.store.representation.Symbol;
+import tools.refinery.store.tuple.Tuple;
+import tools.refinery.store.tuple.Tuple1;
 
-public class ReasoningAdapterImpl implements ReasoningAdapter {
+import java.util.HashMap;
+import java.util.Map;
+
+class ReasoningAdapterImpl implements ReasoningAdapter {
+        static final Symbol<Integer> NODE_COUNT_SYMBOL = Symbol.of("MODEL_SIZE", 0, Integer.class, 0);
         private final Model model;
         private final ReasoningStoreAdapterImpl storeAdapter;
+        private final Map<AnyPartialSymbol, AnyPartialInterpretation>[] partialInterpretations;
+        private final Map<AnyPartialSymbol, AnyPartialInterpretationRefiner> refiners;
+        private final StorageRefiner[] storageRefiners;
+        private final Interpretation<Integer> nodeCountInterpretation;
 
         ReasoningAdapterImpl(Model model, ReasoningStoreAdapterImpl storeAdapter) {
                 this.model = model;
                 this.storeAdapter = storeAdapter;
+
+                int concretenessLength = Concreteness.values().length;
+                // Creation of a generic array.
+                @SuppressWarnings({"unchecked", "squid:S1905"})
+                var interpretationsArray = (Map<AnyPartialSymbol, AnyPartialInterpretation>[]) new Map[concretenessLength];
+                partialInterpretations = interpretationsArray;
+                createPartialInterpretations();
+
+                var refinerFactories = storeAdapter.getSymbolRefiners();
+                refiners = new HashMap<>(refinerFactories.size());
+                createRefiners();
+
+                storageRefiners = storeAdapter.createRepresentationRefiners(model);
+
+                nodeCountInterpretation = model.getInterpretation(NODE_COUNT_SYMBOL);
+        }
+
+        private void createPartialInterpretations() {
+                int concretenessLength = Concreteness.values().length;
+                var interpretationFactories = storeAdapter.getSymbolInterpreters();
+                for (int i = 0; i < concretenessLength; i++) {
+                        partialInterpretations[i] = new HashMap<>(interpretationFactories.size());
+                }
+                // Create the partial interpretations in order so that factories may refer to interpretations of symbols
+                // preceding them in the ordered {@code interpretationFactories} map, e.g., for opposite interpretations.
+                for (var entry : interpretationFactories.entrySet()) {
+                        var partialSymbol = entry.getKey();
+                        var factory = entry.getValue();
+                        for (int i = 0; i < concretenessLength; i++) {
+                                var concreteness = Concreteness.values()[i];
+                                var interpretation = createPartialInterpretation(concreteness, factory, partialSymbol);
+                                partialInterpretations[i].put(partialSymbol, interpretation);
+                        }
+                }
+        }
+
+        private <A, C> PartialInterpretation<A, C> createPartialInterpretation(
+                        Concreteness concreteness, PartialInterpretation.Factory<A, C> interpreter, AnyPartialSymbol symbol) {
+                // The builder only allows well-typed assignment of interpreters to symbols.
+                @SuppressWarnings("unchecked")
+                var typedSymbol = (PartialSymbol<A, C>) symbol;
+                return interpreter.create(this, concreteness, typedSymbol);
+        }
+
+        private void createRefiners() {
+                var refinerFactories = storeAdapter.getSymbolRefiners();
+                // Create the partial interpretations refiners in order so that factories may refer to refiners of symbols
+                // preceding them in the ordered {@code interpretationFactories} map, e.g., for opposite interpretations.
+                for (var entry : refinerFactories.entrySet()) {
+                        var partialSymbol = entry.getKey();
+                        var factory = entry.getValue();
+                        var refiner = createRefiner(factory, partialSymbol);
+                        refiners.put(partialSymbol, refiner);
+                }
+        }
+
+        private <A, C> PartialInterpretationRefiner<A, C> createRefiner(
+                        PartialInterpretationRefiner.Factory<A, C> factory, AnyPartialSymbol symbol) {
+                // The builder only allows well-typed assignment of interpreters to symbols.
+                @SuppressWarnings("unchecked")
+                var typedSymbol = (PartialSymbol<A, C>) symbol;
+                return factory.create(this, typedSymbol);
         }
 
         @Override
@@ -32,12 +111,59 @@ public class ReasoningAdapterImpl implements ReasoningAdapter {
         }
 
         @Override
-        public <A, C> PartialInterpretation<A, C> getPartialInterpretation(PartialSymbol<A, C> partialSymbol) {
-                return null;
+        public <A, C> PartialInterpretation<A, C> getPartialInterpretation(Concreteness concreteness,
+                                                                                                                                           PartialSymbol<A, C> partialSymbol) {
+                var map = partialInterpretations[concreteness.ordinal()];
+                var interpretation = map.get(partialSymbol);
+                if (interpretation == null) {
+                        throw new IllegalArgumentException("No interpretation for partial symbol: " + partialSymbol);
+                }
+                // The builder only allows well-typed assignment of interpreters to symbols.
+                @SuppressWarnings("unchecked")
+                var typedInterpretation = (PartialInterpretation<A, C>) interpretation;
+                return typedInterpretation;
+        }
+
+        @Override
+        public <A, C> PartialInterpretationRefiner<A, C> getRefiner(PartialSymbol<A, C> partialSymbol) {
+                var refiner = refiners.get(partialSymbol);
+                if (refiner == null) {
+                        throw new IllegalArgumentException("No refiner for partial symbol: " + partialSymbol);
+                }
+                // The builder only allows well-typed assignment of refiners to symbols.
+                @SuppressWarnings("unchecked")
+                var typedRefiner = (PartialInterpretationRefiner<A, C>) refiner;
+                return typedRefiner;
+        }
+
+        @Override
+        @Nullable
+        public Tuple1 split(int parentNode) {
+                int newNodeId = nodeCountInterpretation.get(Tuple.of());
+                nodeCountInterpretation.put(Tuple.of(), newNodeId + 1);
+                // Avoid creating an iterator object.
+                //noinspection ForLoopReplaceableByForEach
+                for (int i = 0; i < storageRefiners.length; i++) {
+                        if (!storageRefiners[i].split(parentNode, newNodeId)) {
+                                return null;
+                        }
+                }
+                return Tuple.of(newNodeId);
         }
 
         @Override
-        public ResultSet<Boolean> getLiftedResultSet(Dnf query) {
-                return null;
+        public boolean cleanup(int nodeToDelete) {
+                // Avoid creating an iterator object.
+                //noinspection ForLoopReplaceableByForEach
+                for (int i = 0; i < storageRefiners.length; i++) {
+                        if (!storageRefiners[i].cleanup(nodeToDelete)) {
+                                return false;
+                        }
+                }
+                int currentModelSize = nodeCountInterpretation.get(Tuple.of());
+                if (nodeToDelete == currentModelSize - 1) {
+                        nodeCountInterpretation.put(Tuple.of(), nodeToDelete);
+                }
+                return true;
         }
 }
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/internal/ReasoningBuilderImpl.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/internal/ReasoningBuilderImpl.java
index aa71496c..f7a91284 100644
--- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/internal/ReasoningBuilderImpl.java
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/internal/ReasoningBuilderImpl.java
@@ -7,25 +7,138 @@ package tools.refinery.store.reasoning.internal;
 
 import tools.refinery.store.adapter.AbstractModelAdapterBuilder;
 import tools.refinery.store.model.ModelStore;
+import tools.refinery.store.model.ModelStoreBuilder;
+import tools.refinery.store.query.ModelQueryBuilder;
 import tools.refinery.store.query.dnf.Dnf;
+import tools.refinery.store.query.dnf.Query;
 import tools.refinery.store.reasoning.ReasoningBuilder;
+import tools.refinery.store.reasoning.interpretation.PartialInterpretation;
+import tools.refinery.store.reasoning.refinement.DefaultStorageRefiner;
+import tools.refinery.store.reasoning.translator.AnyPartialSymbolTranslator;
+import tools.refinery.store.reasoning.translator.PartialRelationTranslator;
+import tools.refinery.store.reasoning.lifting.DnfLifter;
+import tools.refinery.store.reasoning.literal.Concreteness;
 import tools.refinery.store.reasoning.literal.Modality;
+import tools.refinery.store.reasoning.refinement.PartialInterpretationRefiner;
+import tools.refinery.store.reasoning.refinement.PartialModelInitializer;
+import tools.refinery.store.reasoning.refinement.StorageRefiner;
+import tools.refinery.store.reasoning.representation.AnyPartialSymbol;
+import tools.refinery.store.representation.AnySymbol;
+import tools.refinery.store.representation.Symbol;
+
+import java.util.*;
 
 public class ReasoningBuilderImpl extends AbstractModelAdapterBuilder<ReasoningStoreAdapterImpl>
                 implements ReasoningBuilder {
+        private final DnfLifter lifter = new DnfLifter();
+        private final PartialQueryRewriter queryRewriter = new PartialQueryRewriter(lifter);
+        private final Map<AnyPartialSymbol, AnyPartialSymbolTranslator> translators = new LinkedHashMap<>();
+        private final Map<AnyPartialSymbol, PartialInterpretation.Factory<?, ?>> symbolInterpreters = new LinkedHashMap<>();
+        private final Map<AnyPartialSymbol, PartialInterpretationRefiner.Factory<?, ?>> symbolRefiners =
+                        new LinkedHashMap<>();
+        private final Map<AnySymbol, StorageRefiner.Factory<?>> registeredStorageRefiners = new LinkedHashMap<>();
+        private final List<PartialModelInitializer> initializers = new ArrayList<>();
+        private int initialNodeCount = 0;
+
+        @Override
+        public ReasoningBuilder initialNodeCount(int nodeCount) {
+                if (nodeCount < 0) {
+                        throw new IllegalArgumentException("Initial model size must not be negative");
+                }
+                initialNodeCount = nodeCount;
+                return this;
+        }
+
         @Override
-        public ReasoningBuilder liftedQuery(Dnf liftedQuery) {
-                return null;
+        public ReasoningBuilder partialSymbol(AnyPartialSymbolTranslator translator) {
+                var partialSymbol = translator.getPartialSymbol();
+                var oldConfiguration = translators.put(partialSymbol, translator);
+                if (oldConfiguration != null && oldConfiguration != translator) {
+                        throw new IllegalArgumentException("Duplicate configuration for symbol: " + partialSymbol);
+                }
+                return this;
         }
 
         @Override
-        public Dnf lift(Modality modality, Dnf query) {
+        public <T> ReasoningBuilder storageRefiner(Symbol<T> symbol, StorageRefiner.Factory<T> refiner) {
                 checkNotConfigured();
-                return null;
+                if (registeredStorageRefiners.put(symbol, refiner) != null) {
+                        throw new IllegalArgumentException("Duplicate representation refiner for symbol: " + symbol);
+                }
+                return this;
+        }
+
+        @Override
+        public ReasoningBuilder initializer(PartialModelInitializer initializer) {
+                checkNotConfigured();
+                initializers.add(initializer);
+                return this;
+        }
+
+        @Override
+        public <T> Query<T> lift(Modality modality, Concreteness concreteness, Query<T> query) {
+                return lifter.lift(modality, concreteness, query);
+        }
+
+        @Override
+        public Dnf lift(Modality modality, Concreteness concreteness, Dnf dnf) {
+                return lifter.lift(modality, concreteness, dnf);
+        }
+
+        @Override
+        protected void doConfigure(ModelStoreBuilder storeBuilder) {
+                storeBuilder.symbols(ReasoningAdapterImpl.NODE_COUNT_SYMBOL);
+                for (var translator : translators.values()) {
+                        translator.configure(storeBuilder);
+                        if (translator instanceof PartialRelationTranslator relationConfiguration) {
+                                doConfigure(relationConfiguration);
+                        } else {
+                                throw new IllegalArgumentException("Unknown partial symbol translator %s for partial symbol %s"
+                                                .formatted(translator, translator.getPartialSymbol()));
+                        }
+                }
+                storeBuilder.symbols(registeredStorageRefiners.keySet());
+                var queryBuilder = storeBuilder.getAdapter(ModelQueryBuilder.class);
+                queryBuilder.rewriter(queryRewriter);
+        }
+
+        private void doConfigure(PartialRelationTranslator relationConfiguration) {
+                var partialRelation = relationConfiguration.getPartialRelation();
+                queryRewriter.addRelationRewriter(partialRelation, relationConfiguration.getRewriter());
+                symbolInterpreters.put(partialRelation, relationConfiguration.getInterpretationFactory());
+                var refiner = relationConfiguration.getInterpretationRefiner();
+                if (refiner != null) {
+                        symbolRefiners.put(partialRelation, refiner);
+                }
         }
 
         @Override
         public ReasoningStoreAdapterImpl doBuild(ModelStore store) {
-                return null;
+                return new ReasoningStoreAdapterImpl(store, initialNodeCount, Collections.unmodifiableMap(symbolInterpreters),
+                                Collections.unmodifiableMap(symbolRefiners), getStorageRefiners(store),
+                                Collections.unmodifiableList(initializers));
+        }
+
+        private Map<AnySymbol, StorageRefiner.Factory<?>> getStorageRefiners(ModelStore store) {
+                var symbols = store.getSymbols();
+                var storageRefiners = new LinkedHashMap<AnySymbol, StorageRefiner.Factory<?>>(symbols.size());
+                for (var symbol : symbols) {
+                        var refiner = registeredStorageRefiners.remove(symbol);
+                        if (refiner == null) {
+                                if (symbol.arity() == 0) {
+                                        // Arity-0 symbols don't need a default refiner, because they are unaffected by object
+                                        // creation/removal. Only a custom refiner ({@code refiner != null}) might need to update them.
+                                        continue;
+                                }
+                                // By default, copy over all affected tuples on object creation and remove all affected tuples on
+                                // object removal.
+                                refiner = DefaultStorageRefiner.factory();
+                        }
+                        storageRefiners.put(symbol, refiner);
+                }
+                if (!registeredStorageRefiners.isEmpty()) {
+                        throw new IllegalArgumentException("Unused storage refiners: " + registeredStorageRefiners.keySet());
+                }
+                return Collections.unmodifiableMap(storageRefiners);
         }
 }
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/internal/ReasoningStoreAdapterImpl.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/internal/ReasoningStoreAdapterImpl.java
index cdddd8d6..e8b581c6 100644
--- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/internal/ReasoningStoreAdapterImpl.java
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/internal/ReasoningStoreAdapterImpl.java
@@ -5,19 +5,45 @@
  */
 package tools.refinery.store.reasoning.internal;
 
-import tools.refinery.store.reasoning.ReasoningStoreAdapter;
 import tools.refinery.store.model.Model;
 import tools.refinery.store.model.ModelStore;
+import tools.refinery.store.query.ModelQueryAdapter;
+import tools.refinery.store.reasoning.ReasoningStoreAdapter;
+import tools.refinery.store.reasoning.interpretation.PartialInterpretation;
+import tools.refinery.store.reasoning.refinement.PartialInterpretationRefiner;
+import tools.refinery.store.reasoning.refinement.PartialModelInitializer;
+import tools.refinery.store.reasoning.refinement.StorageRefiner;
 import tools.refinery.store.reasoning.representation.AnyPartialSymbol;
-import tools.refinery.store.query.dnf.Dnf;
+import tools.refinery.store.representation.AnySymbol;
+import tools.refinery.store.representation.Symbol;
+import tools.refinery.store.tuple.Tuple;
 
 import java.util.Collection;
+import java.util.List;
+import java.util.Map;
 
-public class ReasoningStoreAdapterImpl implements ReasoningStoreAdapter {
+class ReasoningStoreAdapterImpl implements ReasoningStoreAdapter {
         private final ModelStore store;
+        private final Map<AnyPartialSymbol, PartialInterpretation.Factory<?, ?>> symbolInterpreters;
+        private final Map<AnyPartialSymbol, PartialInterpretationRefiner.Factory<?, ?>> symbolRefiners;
+        private final Map<AnySymbol, StorageRefiner.Factory<?>> representationRefiners;
+        private final Object initialModelLock = new Object();
+        private final int initialNodeCount;
+        private List<PartialModelInitializer> initializers;
+        private long initialCommitId = Model.NO_STATE_ID;
 
-        ReasoningStoreAdapterImpl(ModelStore store) {
+        ReasoningStoreAdapterImpl(ModelStore store,
+                                                          int initialNodeCount,
+                                                          Map<AnyPartialSymbol, PartialInterpretation.Factory<?, ?>> symbolInterpreters,
+                                                          Map<AnyPartialSymbol, PartialInterpretationRefiner.Factory<?, ?>> symbolRefiners,
+                                                          Map<AnySymbol, StorageRefiner.Factory<?>> representationRefiners,
+                                                          List<PartialModelInitializer> initializers) {
                 this.store = store;
+                this.initialNodeCount = initialNodeCount;
+                this.symbolInterpreters = symbolInterpreters;
+                this.symbolRefiners = symbolRefiners;
+                this.representationRefiners = representationRefiners;
+                this.initializers = initializers;
         }
 
         @Override
@@ -27,12 +53,65 @@ public class ReasoningStoreAdapterImpl implements ReasoningStoreAdapter {
 
         @Override
         public Collection<AnyPartialSymbol> getPartialSymbols() {
-                return null;
+                return symbolInterpreters.keySet();
         }
 
         @Override
-        public Collection<Dnf> getLiftedQueries() {
-                return null;
+        public Collection<AnyPartialSymbol> getRefinablePartialSymbols() {
+                return symbolRefiners.keySet();
+        }
+
+        // Use of wildcard return value only in internal method not exposed as API, so there is less chance of confusion.
+        @SuppressWarnings("squid:S1452")
+        Map<AnyPartialSymbol, PartialInterpretation.Factory<?, ?>> getSymbolInterpreters() {
+                return symbolInterpreters;
+        }
+
+        // Use of wildcard return value only in internal method not exposed as API, so there is less chance of confusion.
+        @SuppressWarnings("squid:S1452")
+        Map<AnyPartialSymbol, PartialInterpretationRefiner.Factory<?, ?>> getSymbolRefiners() {
+                return symbolRefiners;
+        }
+
+        StorageRefiner[] createRepresentationRefiners(Model model) {
+                var refiners = new StorageRefiner[representationRefiners.size()];
+                int i = 0;
+                for (var entry : representationRefiners.entrySet()) {
+                        var symbol = entry.getKey();
+                        var factory = entry.getValue();
+                        refiners[i] = createRepresentationRefiner(factory, model, symbol);
+                }
+                return refiners;
+        }
+
+        private <T> StorageRefiner createRepresentationRefiner(
+                        StorageRefiner.Factory<T> factory, Model model, AnySymbol symbol) {
+                // The builder only allows well-typed assignment of refiners to symbols.
+                @SuppressWarnings("unchecked")
+                var typedSymbol = (Symbol<T>) symbol;
+                return factory.create(typedSymbol, model);
+        }
+
+        @Override
+        public Model createInitialModel() {
+                synchronized (initialModelLock) {
+                        if (initialCommitId == Model.NO_STATE_ID) {
+                                return doCreateInitialModel();
+                        }
+                        return store.createModelForState(initialCommitId);
+                }
+        }
+
+        private Model doCreateInitialModel() {
+                var model = store.createEmptyModel();
+                model.getInterpretation(ReasoningAdapterImpl.NODE_COUNT_SYMBOL).put(Tuple.of(), initialNodeCount);
+                for (var initializer : initializers) {
+                        initializer.initialize(model, initialNodeCount);
+                }
+                model.getAdapter(ModelQueryAdapter.class).flushChanges();
+                initialCommitId = model.commit();
+                initializers = null;
+                return model;
         }
 
         @Override
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/interpretation/AbstractPartialInterpretation.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/interpretation/AbstractPartialInterpretation.java
new file mode 100644
index 00000000..ed291eac
--- /dev/null
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/interpretation/AbstractPartialInterpretation.java
@@ -0,0 +1,38 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.reasoning.interpretation;
+
+import tools.refinery.store.reasoning.ReasoningAdapter;
+import tools.refinery.store.reasoning.literal.Concreteness;
+import tools.refinery.store.reasoning.representation.PartialSymbol;
+
+public abstract class AbstractPartialInterpretation<A, C> implements PartialInterpretation<A, C> {
+        private final ReasoningAdapter adapter;
+        private final PartialSymbol<A, C> partialSymbol;
+        private final Concreteness concreteness;
+
+        protected AbstractPartialInterpretation(ReasoningAdapter adapter, Concreteness concreteness,
+                                                                                        PartialSymbol<A, C> partialSymbol) {
+                this.adapter = adapter;
+                this.partialSymbol = partialSymbol;
+                this.concreteness = concreteness;
+        }
+
+        @Override
+        public ReasoningAdapter getAdapter() {
+                return adapter;
+        }
+
+        @Override
+        public PartialSymbol<A, C> getPartialSymbol() {
+                return partialSymbol;
+        }
+
+        @Override
+        public Concreteness getConcreteness() {
+                return concreteness;
+        }
+}
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/AnyPartialInterpretation.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/interpretation/AnyPartialInterpretation.java
index 000171a1..cd709bc4 100644
--- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/AnyPartialInterpretation.java
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/interpretation/AnyPartialInterpretation.java
@@ -3,8 +3,10 @@
  *
  * SPDX-License-Identifier: EPL-2.0
  */
-package tools.refinery.store.reasoning;
+package tools.refinery.store.reasoning.interpretation;
 
+import tools.refinery.store.reasoning.ReasoningAdapter;
+import tools.refinery.store.reasoning.literal.Concreteness;
 import tools.refinery.store.reasoning.representation.AnyPartialSymbol;
 
 public sealed interface AnyPartialInterpretation permits PartialInterpretation {
@@ -12,7 +14,5 @@ public sealed interface AnyPartialInterpretation permits PartialInterpretation {
 
         AnyPartialSymbol getPartialSymbol();
 
-        int countUnfinished();
-
-        int countErrors();
+        Concreteness getConcreteness();
 }
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/PartialInterpretation.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/interpretation/PartialInterpretation.java
index 4140d640..3d3d6056 100644
--- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/PartialInterpretation.java
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/interpretation/PartialInterpretation.java
@@ -3,10 +3,12 @@
  *
  * SPDX-License-Identifier: EPL-2.0
  */
-package tools.refinery.store.reasoning;
+package tools.refinery.store.reasoning.interpretation;
 
-import tools.refinery.store.reasoning.representation.PartialSymbol;
 import tools.refinery.store.map.Cursor;
+import tools.refinery.store.reasoning.ReasoningAdapter;
+import tools.refinery.store.reasoning.literal.Concreteness;
+import tools.refinery.store.reasoning.representation.PartialSymbol;
 import tools.refinery.store.tuple.Tuple;
 
 public non-sealed interface PartialInterpretation<A, C> extends AnyPartialInterpretation {
@@ -17,9 +19,8 @@ public non-sealed interface PartialInterpretation<A, C> extends AnyPartialInterp
 
         Cursor<Tuple, A> getAll();
 
-        MergeResult merge(Tuple key, A value);
-
-        C getConcrete(Tuple key);
-
-        Cursor<Tuple, C> getAllConcrete();
+        interface Factory<A, C> {
+                PartialInterpretation<A, C> create(ReasoningAdapter adapter, Concreteness concreteness,
+                                                                                   PartialSymbol<A, C> partialSymbol);
+        }
 }
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/interpretation/PartialRelationRewriter.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/interpretation/PartialRelationRewriter.java
new file mode 100644
index 00000000..da8ae0a8
--- /dev/null
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/interpretation/PartialRelationRewriter.java
@@ -0,0 +1,17 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.reasoning.interpretation;
+
+import tools.refinery.store.query.literal.AbstractCallLiteral;
+import tools.refinery.store.query.literal.Literal;
+import tools.refinery.store.reasoning.literal.Concreteness;
+import tools.refinery.store.reasoning.literal.Modality;
+
+import java.util.List;
+
+public interface PartialRelationRewriter {
+        List<Literal> rewriteLiteral(AbstractCallLiteral literal, Modality modality, Concreteness concreteness);
+}
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/interpretation/QueryBasedRelationInterpretationFactory.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/interpretation/QueryBasedRelationInterpretationFactory.java
new file mode 100644
index 00000000..2535714a
--- /dev/null
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/interpretation/QueryBasedRelationInterpretationFactory.java
@@ -0,0 +1,180 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.reasoning.interpretation;
+
+import tools.refinery.store.map.Cursor;
+import tools.refinery.store.query.ModelQueryAdapter;
+import tools.refinery.store.query.dnf.Query;
+import tools.refinery.store.query.resultset.ResultSet;
+import tools.refinery.store.reasoning.ReasoningAdapter;
+import tools.refinery.store.reasoning.literal.Concreteness;
+import tools.refinery.store.reasoning.representation.PartialSymbol;
+import tools.refinery.store.representation.TruthValue;
+import tools.refinery.store.tuple.Tuple;
+
+public class QueryBasedRelationInterpretationFactory implements PartialInterpretation.Factory<TruthValue, Boolean> {
+        private final Query<Boolean> may;
+        private final Query<Boolean> must;
+        private final Query<Boolean> candidateMay;
+        private final Query<Boolean> candidateMust;
+
+        public QueryBasedRelationInterpretationFactory(
+                        Query<Boolean> may, Query<Boolean> must, Query<Boolean> candidateMay, Query<Boolean> candidateMust) {
+                this.may = may;
+                this.must = must;
+                this.candidateMay = candidateMay;
+                this.candidateMust = candidateMust;
+        }
+
+        @Override
+        public PartialInterpretation<TruthValue, Boolean> create(
+                        ReasoningAdapter adapter, Concreteness concreteness, PartialSymbol<TruthValue, Boolean> partialSymbol) {
+                var queryEngine = adapter.getModel().getAdapter(ModelQueryAdapter.class);
+                ResultSet<Boolean> mayResultSet;
+                ResultSet<Boolean> mustResultSet;
+                switch (concreteness) {
+                case PARTIAL -> {
+                        mayResultSet = queryEngine.getResultSet(may);
+                        mustResultSet = queryEngine.getResultSet(must);
+                }
+                case CANDIDATE -> {
+                        mayResultSet = queryEngine.getResultSet(candidateMay);
+                        mustResultSet = queryEngine.getResultSet(candidateMust);
+                }
+                default -> throw new IllegalArgumentException("Unknown concreteness: " + concreteness);
+                }
+                if (mayResultSet.equals(mustResultSet)) {
+                        return new TwoValuedInterpretation(adapter, concreteness, partialSymbol, mustResultSet);
+                } else {
+                        return new FourValuedInterpretation(
+                                        adapter, concreteness, partialSymbol, mayResultSet, mustResultSet);
+                }
+        }
+
+        private static class TwoValuedInterpretation extends AbstractPartialInterpretation<TruthValue, Boolean> {
+                private final ResultSet<Boolean> resultSet;
+
+                protected TwoValuedInterpretation(
+                                ReasoningAdapter adapter, Concreteness concreteness, PartialSymbol<TruthValue, Boolean> partialSymbol,
+                                ResultSet<Boolean> resultSet) {
+                        super(adapter, concreteness, partialSymbol);
+                        this.resultSet = resultSet;
+                }
+
+                @Override
+                public TruthValue get(Tuple key) {
+                        return TruthValue.toTruthValue(resultSet.get(key));
+                }
+
+                @Override
+                public Cursor<Tuple, TruthValue> getAll() {
+                        return new TwoValuedCursor(resultSet.getAll());
+                }
+
+                private record TwoValuedCursor(Cursor<Tuple, Boolean> cursor) implements Cursor<Tuple, TruthValue> {
+                        @Override
+                        public Tuple getKey() {
+                                return cursor.getKey();
+                        }
+
+                        @Override
+                        public TruthValue getValue() {
+                                return TruthValue.toTruthValue(cursor.getValue());
+                        }
+
+                        @Override
+                        public boolean isTerminated() {
+                                return cursor.isTerminated();
+                        }
+
+                        @Override
+                        public boolean move() {
+                                return cursor.move();
+                        }
+                }
+        }
+
+        private static class FourValuedInterpretation extends AbstractPartialInterpretation<TruthValue, Boolean> {
+                private final ResultSet<Boolean> mayResultSet;
+                private final ResultSet<Boolean> mustResultSet;
+
+                public FourValuedInterpretation(
+                                ReasoningAdapter adapter, Concreteness concreteness, PartialSymbol<TruthValue, Boolean> partialSymbol,
+                                ResultSet<Boolean> mayResultSet, ResultSet<Boolean> mustResultSet) {
+                        super(adapter, concreteness, partialSymbol);
+                        this.mayResultSet = mayResultSet;
+                        this.mustResultSet = mustResultSet;
+                }
+
+                @Override
+                public TruthValue get(Tuple key) {
+                        boolean isMay = mayResultSet.get(key);
+                        boolean isMust = mustResultSet.get(key);
+                        if (isMust) {
+                                return isMay ? TruthValue.TRUE : TruthValue.ERROR;
+                        } else {
+                                return isMay ? TruthValue.UNKNOWN : TruthValue.FALSE;
+                        }
+                }
+
+                @Override
+                public Cursor<Tuple, TruthValue> getAll() {
+                        return new FourValuedCursor();
+                }
+
+                private final class FourValuedCursor implements Cursor<Tuple, TruthValue> {
+                        private final Cursor<Tuple, Boolean> mayCursor;
+                        private Cursor<Tuple, Boolean> mustCursor;
+
+                        private FourValuedCursor() {
+                                this.mayCursor = mayResultSet.getAll();
+                        }
+
+                        @Override
+                        public Tuple getKey() {
+                                return mustCursor == null ? mayCursor.getKey() : mustCursor.getKey();
+                        }
+
+                        @Override
+                        public TruthValue getValue() {
+                                if (mustCursor != null) {
+                                        return TruthValue.ERROR;
+                                }
+                                if (Boolean.TRUE.equals(mustResultSet.get(mayCursor.getKey()))) {
+                                        return TruthValue.TRUE;
+                                }
+                                return TruthValue.UNKNOWN;
+                        }
+
+                        @Override
+                        public boolean isTerminated() {
+                                return mustCursor != null && mustCursor.isTerminated();
+                        }
+
+                        @Override
+                        public boolean move() {
+                                if (mayCursor.isTerminated()) {
+                                        return moveMust();
+                                }
+                                if (mayCursor.move()) {
+                                        return true;
+                                }
+                                mustCursor = mustResultSet.getAll();
+                                return moveMust();
+                        }
+
+                        private boolean moveMust() {
+                                while (mustCursor.move()) {
+                                        // We already iterated over {@code TRUE} truth values with {@code mayCursor}.
+                                        if (!Boolean.TRUE.equals(mayResultSet.get(mustCursor.getKey()))) {
+                                                return true;
+                                        }
+                                }
+                                return false;
+                        }
+                }
+        }
+}
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/interpretation/QueryBasedRelationRewriter.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/interpretation/QueryBasedRelationRewriter.java
new file mode 100644
index 00000000..3be9e9ac
--- /dev/null
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/interpretation/QueryBasedRelationRewriter.java
@@ -0,0 +1,44 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.reasoning.interpretation;
+
+import tools.refinery.store.query.dnf.Query;
+import tools.refinery.store.query.literal.AbstractCallLiteral;
+import tools.refinery.store.query.literal.Literal;
+import tools.refinery.store.reasoning.literal.Concreteness;
+import tools.refinery.store.reasoning.literal.Modality;
+
+import java.util.List;
+
+public class QueryBasedRelationRewriter implements PartialRelationRewriter {
+        private final Query<Boolean> may;
+        private final Query<Boolean> must;
+        private final Query<Boolean> candidateMay;
+        private final Query<Boolean> candidateMust;
+
+        public QueryBasedRelationRewriter(Query<Boolean> may, Query<Boolean> must, Query<Boolean> candidateMay,
+                                                                          Query<Boolean> candidateMust) {
+                this.may = may;
+                this.must = must;
+                this.candidateMay = candidateMay;
+                this.candidateMust = candidateMust;
+        }
+
+        @Override
+        public List<Literal> rewriteLiteral(AbstractCallLiteral literal, Modality modality, Concreteness concreteness) {
+                var query = switch (concreteness) {
+                        case PARTIAL -> switch (modality) {
+                                case MAY -> may;
+                                case MUST -> must;
+                        };
+                        case CANDIDATE -> switch (modality) {
+                                case MAY -> candidateMay;
+                                case MUST -> candidateMust;
+                        };
+                };
+                return List.of(literal.withTarget(query.getDnf()));
+        }
+}
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/lifting/ClauseLifter.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/lifting/ClauseLifter.java
index d3b0ace8..7bf092a3 100644
--- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/lifting/ClauseLifter.java
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/lifting/ClauseLifter.java
@@ -54,7 +54,7 @@ class ClauseLifter {
                         var liftedLiteral = liftLiteral(literal);
                         liftedLiterals.add(liftedLiteral);
                 }
-                var existsConstraint = ModalConstraint.of(modality, concreteness, ReasoningAdapter.EXISTS);
+                var existsConstraint = ModalConstraint.of(modality, concreteness, ReasoningAdapter.EXISTS_SYMBOL);
                 for (var quantifiedVariable : existentialQuantifiersToAdd) {
                         liftedLiterals.add(existsConstraint.call(quantifiedVariable));
                 }
@@ -117,7 +117,7 @@ class ClauseLifter {
                 var liftedConstraint = ModalConstraint.of(negatedModality, concreteness, target);
                 literals.add(liftedConstraint.call(CallPolarity.POSITIVE, originalArguments));
 
-                var existsConstraint = ModalConstraint.of(negatedModality, concreteness, ReasoningAdapter.EXISTS);
+                var existsConstraint = ModalConstraint.of(negatedModality, concreteness, ReasoningAdapter.EXISTS_SYMBOL);
                 for (var variable : uniqueOriginalArguments) {
                         if (privateVariables.contains(variable)) {
                                 literals.add(existsConstraint.call(variable));
@@ -134,7 +134,7 @@ class ClauseLifter {
                 var originalArguments = callLiteral.getArguments();
                 var liftedTarget = ModalConstraint.of(modality, concreteness, target);
 
-                var existsConstraint = ModalConstraint.of(modality, concreteness, ReasoningAdapter.EXISTS);
+                var existsConstraint = ModalConstraint.of(modality, concreteness, ReasoningAdapter.EXISTS_SYMBOL);
                 var existingEndHelperName = "%s#exisitingEnd#%s#%s".formatted(target.name(), modality, concreteness);
                 var existingEndHelper = Dnf.of(existingEndHelperName, builder -> {
                         var start = builder.parameter("start");
@@ -171,10 +171,10 @@ class ClauseLifter {
 
         private Literal liftEquivalenceLiteral(EquivalenceLiteral equivalenceLiteral) {
                 if (equivalenceLiteral.isPositive()) {
-                        return ModalConstraint.of(modality, concreteness, ReasoningAdapter.EQUALS)
+                        return ModalConstraint.of(modality, concreteness, ReasoningAdapter.EQUALS_SYMBOL)
                                         .call(CallPolarity.POSITIVE, equivalenceLiteral.getLeft(), equivalenceLiteral.getRight());
                 }
-                return ModalConstraint.of(modality.negate(), concreteness, ReasoningAdapter.EQUALS)
+                return ModalConstraint.of(modality.negate(), concreteness, ReasoningAdapter.EQUALS_SYMBOL)
                                 .call(CallPolarity.NEGATIVE, equivalenceLiteral.getLeft(), equivalenceLiteral.getRight());
         }
 }
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/lifting/DnfLifter.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/lifting/DnfLifter.java
index c3b23b43..2e68fa3e 100644
--- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/lifting/DnfLifter.java
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/lifting/DnfLifter.java
@@ -7,6 +7,7 @@ package tools.refinery.store.reasoning.lifting;
 
 import tools.refinery.store.query.dnf.Dnf;
 import tools.refinery.store.query.dnf.DnfClause;
+import tools.refinery.store.query.dnf.Query;
 import tools.refinery.store.query.equality.DnfEqualityChecker;
 import tools.refinery.store.query.literal.Literal;
 import tools.refinery.store.reasoning.literal.Concreteness;
@@ -19,6 +20,11 @@ import java.util.Map;
 public class DnfLifter {
         private final Map<ModalDnf, Dnf> cache = new HashMap<>();
 
+        public <T> Query<T> lift(Modality modality, Concreteness concreteness, Query<T> query) {
+                var liftedDnf = lift(modality, concreteness, query.getDnf());
+                return query.withDnf(liftedDnf);
+        }
+
         public Dnf lift(Modality modality, Concreteness concreteness, Dnf dnf) {
                 return cache.computeIfAbsent(new ModalDnf(modality, concreteness, dnf), this::doLift);
         }
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/literal/PartialLiterals.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/literal/PartialLiterals.java
index 4f07f17d..2c879397 100644
--- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/literal/PartialLiterals.java
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/literal/PartialLiterals.java
@@ -13,20 +13,28 @@ public final class PartialLiterals {
         }
 
         public static CallLiteral may(CallLiteral literal) {
-                return addModality(literal, Modality.MAY);
+                return addModality(literal, Modality.MAY, Concreteness.PARTIAL);
         }
 
         public static CallLiteral must(CallLiteral literal) {
-                return addModality(literal, Modality.MUST);
+                return addModality(literal, Modality.MUST, Concreteness.PARTIAL);
         }
 
-        public static CallLiteral addModality(CallLiteral literal, Modality modality) {
+        public static CallLiteral candidateMay(CallLiteral literal) {
+                return addModality(literal, Modality.MAY, Concreteness.CANDIDATE);
+        }
+
+        public static CallLiteral candidateMust(CallLiteral literal) {
+                return addModality(literal, Modality.MUST, Concreteness.CANDIDATE);
+        }
+
+        public static CallLiteral addModality(CallLiteral literal, Modality modality, Concreteness concreteness) {
                 var target = literal.getTarget();
                 if (target instanceof ModalConstraint) {
                         throw new IllegalArgumentException("Literal %s already has modality".formatted(literal));
                 }
                 var polarity = literal.getPolarity();
-                var modalTarget = new ModalConstraint(modality.commute(polarity), target);
+                var modalTarget = new ModalConstraint(modality.commute(polarity), concreteness, target);
                 return new CallLiteral(polarity, modalTarget, literal.getArguments());
         }
 }
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/refinement/AnyPartialInterpretationRefiner.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/refinement/AnyPartialInterpretationRefiner.java
new file mode 100644
index 00000000..6c381511
--- /dev/null
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/refinement/AnyPartialInterpretationRefiner.java
@@ -0,0 +1,15 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.reasoning.refinement;
+
+import tools.refinery.store.reasoning.ReasoningAdapter;
+import tools.refinery.store.reasoning.representation.AnyPartialSymbol;
+
+public sealed interface AnyPartialInterpretationRefiner permits PartialInterpretationRefiner {
+        ReasoningAdapter getAdapter();
+
+        AnyPartialSymbol getPartialSymbol();
+}
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/refinement/ConcreteSymbolRefiner.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/refinement/ConcreteSymbolRefiner.java
new file mode 100644
index 00000000..756118a0
--- /dev/null
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/refinement/ConcreteSymbolRefiner.java
@@ -0,0 +1,51 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.reasoning.refinement;
+
+import tools.refinery.store.model.Interpretation;
+import tools.refinery.store.reasoning.ReasoningAdapter;
+import tools.refinery.store.reasoning.representation.PartialSymbol;
+import tools.refinery.store.representation.Symbol;
+import tools.refinery.store.tuple.Tuple;
+
+import java.util.Objects;
+
+public class ConcreteSymbolRefiner<A, C> implements PartialInterpretationRefiner<A, C> {
+        private final ReasoningAdapter adapter;
+        private final PartialSymbol<A, C> partialSymbol;
+        private final Interpretation<A> interpretation;
+
+        public ConcreteSymbolRefiner(ReasoningAdapter adapter, PartialSymbol<A, C> partialSymbol,
+                                                                 Symbol<A> concreteSymbol) {
+                this.adapter = adapter;
+                this.partialSymbol = partialSymbol;
+                interpretation = adapter.getModel().getInterpretation(concreteSymbol);
+        }
+
+        @Override
+        public ReasoningAdapter getAdapter() {
+                return adapter;
+        }
+
+        @Override
+        public PartialSymbol<A, C> getPartialSymbol() {
+                return partialSymbol;
+        }
+
+        @Override
+        public boolean merge(Tuple key, A value) {
+                var currentValue = interpretation.get(key);
+                var mergedValue = partialSymbol.abstractDomain().commonRefinement(currentValue, value);
+                if (!Objects.equals(currentValue, mergedValue)) {
+                        interpretation.put(key, mergedValue);
+                }
+                return true;
+        }
+
+        public static <A1, C1> PartialInterpretationRefiner.Factory<A1, C1> of(Symbol<A1> concreteSymbol) {
+                return (adapter, partialSymbol) -> new ConcreteSymbolRefiner<>(adapter, partialSymbol, concreteSymbol);
+        }
+}
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/refinement/DefaultStorageRefiner.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/refinement/DefaultStorageRefiner.java
new file mode 100644
index 00000000..0d7d6c5c
--- /dev/null
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/refinement/DefaultStorageRefiner.java
@@ -0,0 +1,80 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.reasoning.refinement;
+
+import tools.refinery.store.model.Interpretation;
+import tools.refinery.store.tuple.Tuple;
+
+public class DefaultStorageRefiner<T> implements StorageRefiner {
+        private static final StorageRefiner.Factory<Object> FACTORY = (symbol, model) -> {
+                var interpretation = model.getInterpretation(symbol);
+                return new DefaultStorageRefiner<>(interpretation);
+        };
+
+        private final Interpretation<T> interpretation;
+
+        public DefaultStorageRefiner(Interpretation<T> interpretation) {
+                this.interpretation = interpretation;
+        }
+
+        @Override
+        public boolean split(int parentNode, int childNode) {
+                var symbol = interpretation.getSymbol();
+                int arity = symbol.arity();
+                for (int i = 0; i < arity; i++) {
+                        int adjacentSize = interpretation.getAdjacentSize(i, parentNode);
+                        if (adjacentSize == 0) {
+                                continue;
+                        }
+                        var toSetKeys = new Tuple[adjacentSize];
+                        // This is safe, because we won't pass the array to the outside.
+                        @SuppressWarnings("unchecked")
+                        var toSetValues = (T[]) new Object[adjacentSize];
+                        var cursor = interpretation.getAdjacent(i, parentNode);
+                        int j = 0;
+                        while (cursor.move()) {
+                                toSetKeys[j] = cursor.getKey().set(i, childNode);
+                                toSetValues[j] = cursor.getValue();
+                                j++;
+                        }
+                        for (j = 0; j < adjacentSize; j++) {
+                                interpretation.put(toSetKeys[j], toSetValues[j]);
+                        }
+                }
+                return true;
+        }
+
+        @Override
+        public boolean cleanup(int nodeToDelete) {
+                var symbol = interpretation.getSymbol();
+                int arity = symbol.arity();
+                var defaultValue = symbol.defaultValue();
+                for (int i = 0; i < arity; i++) {
+                        int adjacentSize = interpretation.getAdjacentSize(i, nodeToDelete);
+                        if (adjacentSize == 0) {
+                                continue;
+                        }
+                        var toDelete = new Tuple[adjacentSize];
+                        var cursor = interpretation.getAdjacent(i, nodeToDelete);
+                        int j = 0;
+                        while (cursor.move()) {
+                                toDelete[j] = cursor.getKey();
+                                j++;
+                        }
+                        for (j = 0; j < adjacentSize; j++) {
+                                interpretation.put(toDelete[j], defaultValue);
+                        }
+                }
+                return true;
+        }
+
+        public static <T> StorageRefiner.Factory<T> factory() {
+                // This is safe, because {@code FACTORY} doesn't depend on {@code T} at all.
+                @SuppressWarnings("unchecked")
+                var typedFactory = (StorageRefiner.Factory<T>) FACTORY;
+                return typedFactory;
+        }
+}
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/refinement/PartialInterpretationRefiner.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/refinement/PartialInterpretationRefiner.java
new file mode 100644
index 00000000..f48d1d1f
--- /dev/null
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/refinement/PartialInterpretationRefiner.java
@@ -0,0 +1,22 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.reasoning.refinement;
+
+import tools.refinery.store.reasoning.ReasoningAdapter;
+import tools.refinery.store.reasoning.representation.PartialSymbol;
+import tools.refinery.store.tuple.Tuple;
+
+public non-sealed interface PartialInterpretationRefiner<A, C> extends AnyPartialInterpretationRefiner {
+        @Override
+        PartialSymbol<A, C> getPartialSymbol();
+
+        boolean merge(Tuple key, A value);
+
+        @FunctionalInterface
+        interface Factory<A, C> {
+                PartialInterpretationRefiner<A, C> create(ReasoningAdapter adapter, PartialSymbol<A, C> partialSymbol);
+        }
+}
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/refinement/PartialModelInitializer.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/refinement/PartialModelInitializer.java
new file mode 100644
index 00000000..79c1670f
--- /dev/null
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/refinement/PartialModelInitializer.java
@@ -0,0 +1,13 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.reasoning.refinement;
+
+import tools.refinery.store.model.Model;
+
+@FunctionalInterface
+public interface PartialModelInitializer {
+        void initialize(Model model, int nodeCount);
+}
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/refinement/StorageRefiner.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/refinement/StorageRefiner.java
new file mode 100644
index 00000000..004696fd
--- /dev/null
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/refinement/StorageRefiner.java
@@ -0,0 +1,20 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.reasoning.refinement;
+
+import tools.refinery.store.model.Model;
+import tools.refinery.store.representation.Symbol;
+
+public interface StorageRefiner {
+        boolean split(int parentNode, int childNode);
+
+        boolean cleanup(int nodeToDelete);
+
+        @FunctionalInterface
+        interface Factory<T> {
+                StorageRefiner create(Symbol<T> symbol, Model model);
+        }
+}
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/representation/PartialFunction.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/representation/PartialFunction.java
index d58d026f..e59c8af8 100644
--- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/representation/PartialFunction.java
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/representation/PartialFunction.java
@@ -15,11 +15,6 @@ public record PartialFunction<A, C>(String name, int arity, AbstractDomain<A, C>
         }
 
         @Override
-        public C defaultConcreteValue() {
-                return null;
-        }
-
-        @Override
         public boolean equals(Object o) {
                 return this == o;
         }
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/representation/PartialRelation.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/representation/PartialRelation.java
index 6b2f050b..4ccb7033 100644
--- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/representation/PartialRelation.java
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/representation/PartialRelation.java
@@ -26,11 +26,6 @@ public record PartialRelation(String name, int arity) implements PartialSymbol<T
         }
 
         @Override
-        public Boolean defaultConcreteValue() {
-                return false;
-        }
-
-        @Override
         public List<Parameter> getParameters() {
                 var parameters = new Parameter[arity];
                 Arrays.fill(parameters, Parameter.NODE_OUT);
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/representation/PartialSymbol.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/representation/PartialSymbol.java
index 2f04534a..38b2e466 100644
--- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/representation/PartialSymbol.java
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/representation/PartialSymbol.java
@@ -13,8 +13,6 @@ public sealed interface PartialSymbol<A, C> extends AnyPartialSymbol permits Par
 
         A defaultValue();
 
-        C defaultConcreteValue();
-
         static PartialRelation of(String name, int arity) {
                 return new PartialRelation(name, arity);
         }
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/seed/MapBasedSeed.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/seed/MapBasedSeed.java
new file mode 100644
index 00000000..b5a3d844
--- /dev/null
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/seed/MapBasedSeed.java
@@ -0,0 +1,117 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.reasoning.seed;
+
+import tools.refinery.store.map.Cursor;
+import tools.refinery.store.map.Cursors;
+import tools.refinery.store.tuple.Tuple;
+
+import java.util.Map;
+import java.util.Objects;
+
+record MapBasedSeed<T>(int arity, Class<T> valueType, T reducedValue, Map<Tuple, T> map) implements Seed<T> {
+        @Override
+        public T get(Tuple key) {
+                var value = map.get(key);
+                return value == null ? reducedValue : value;
+        }
+
+        @Override
+        public Cursor<Tuple, T> getCursor(T defaultValue, int nodeCount) {
+                if (Objects.equals(defaultValue, reducedValue)) {
+                        return Cursors.of(map);
+                }
+                return new CartesianProductCursor<>(arity, nodeCount, reducedValue, defaultValue, map);
+        }
+
+        private static class CartesianProductCursor<T> implements Cursor<Tuple, T> {
+                private final int nodeCount;
+                private final T reducedValue;
+                private final T defaultValue;
+                private final Map<Tuple, T> map;
+                private final int[] counter;
+                private State state = State.INITIAL;
+                private Tuple key;
+                private T value;
+
+                private CartesianProductCursor(int arity, int nodeCount, T reducedValue, T defaultValue, Map<Tuple, T> map) {
+                        this.nodeCount = nodeCount;
+                        this.reducedValue = reducedValue;
+                        this.defaultValue = defaultValue;
+                        this.map = map;
+                        counter = new int[arity];
+                }
+
+                @Override
+                public Tuple getKey() {
+                        return key;
+                }
+
+                @Override
+                public T getValue() {
+                        return value;
+                }
+
+                @Override
+                public boolean isTerminated() {
+                        return state == State.TERMINATED;
+                }
+
+                @Override
+                public boolean move() {
+                        return switch (state) {
+                                case INITIAL -> {
+                                        state = State.STARTED;
+                                        yield checkValue() || moveToNext();
+                                }
+                                case STARTED -> moveToNext();
+                                case TERMINATED -> false;
+                        };
+                }
+
+                private boolean moveToNext() {
+                        do {
+                                increment();
+                        } while (!checkValue());
+                        return state != State.TERMINATED;
+                }
+
+                private void increment() {
+                        int i = counter.length - 1;
+                        while (i >= 0) {
+                                counter[i]++;
+                                if (counter[i] < nodeCount) {
+                                        return;
+                                }
+                                counter[i] = 0;
+                                i--;
+                        }
+                }
+
+                private boolean checkValue() {
+                        if (state == State.TERMINATED) {
+                                return false;
+                        }
+                        if (counter[0] >= nodeCount) {
+                                state = State.TERMINATED;
+                                return false;
+                        }
+                        key = Tuple.of(counter);
+                        var valueInMap = map.get(key);
+                        if (Objects.equals(valueInMap, defaultValue)) {
+                                return false;
+                        }
+                        value = valueInMap == null ? reducedValue : valueInMap;
+                        return true;
+                }
+
+                private enum State {
+                        INITIAL,
+                        STARTED,
+                        TERMINATED
+                }
+        }
+}
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/seed/Seed.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/seed/Seed.java
index 08079f12..64b98683 100644
--- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/seed/Seed.java
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/seed/Seed.java
@@ -6,14 +6,68 @@
 package tools.refinery.store.reasoning.seed;
 
 import tools.refinery.store.map.Cursor;
+import tools.refinery.store.reasoning.representation.PartialSymbol;
+import tools.refinery.store.representation.Symbol;
 import tools.refinery.store.tuple.Tuple;
 
+import java.util.Collections;
+import java.util.LinkedHashMap;
+import java.util.Map;
+
 public interface Seed<T> {
         int arity();
 
+        Class<T> valueType();
+
         T reducedValue();
 
         T get(Tuple key);
 
         Cursor<Tuple, T> getCursor(T defaultValue, int nodeCount);
+
+        static <T> Builder<T> builder(int arity, Class<T> valueType, T reducedValue) {
+                return new Builder<>(arity, valueType, reducedValue);
+        }
+
+        static <T> Builder<T> builder(Symbol<T> symbol) {
+                return builder(symbol.arity(), symbol.valueType(), symbol.defaultValue());
+        }
+
+        static <T> Builder<T> builder(PartialSymbol<T, ?> partialSymbol) {
+                return builder(partialSymbol.arity(), partialSymbol.abstractDomain().abstractType(),
+                                partialSymbol.defaultValue());
+        }
+
+        @SuppressWarnings("UnusedReturnValue")
+        class Builder<T> {
+                private final int arity;
+                private final Class<T> valueType;
+                private final T reducedValue;
+                private final Map<Tuple, T> map = new LinkedHashMap<>();
+
+                private Builder(int arity, Class<T> valueType, T reducedValue) {
+                        this.arity = arity;
+                        this.valueType = valueType;
+                        this.reducedValue = reducedValue;
+                }
+
+                public Builder<T> put(Tuple key, T value) {
+                        if (key.getSize() != arity) {
+                                throw new IllegalArgumentException("Expected %s to have %d elements".formatted(key, arity));
+                        }
+                        map.put(key, value);
+                        return this;
+                }
+
+                public Builder<T> putAll(Map<Tuple, T> map) {
+                        for (var entry : map.entrySet()) {
+                                put(entry.getKey(), entry.getValue());
+                        }
+                        return this;
+                }
+
+                public Seed<T> build() {
+                        return new MapBasedSeed<>(arity, valueType, reducedValue, Collections.unmodifiableMap(map));
+                }
+        }
 }
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/seed/SeedInitializer.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/seed/SeedInitializer.java
new file mode 100644
index 00000000..884d6515
--- /dev/null
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/seed/SeedInitializer.java
@@ -0,0 +1,27 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.reasoning.seed;
+
+import tools.refinery.store.model.Model;
+import tools.refinery.store.reasoning.refinement.PartialModelInitializer;
+import tools.refinery.store.representation.Symbol;
+
+public class SeedInitializer<T> implements PartialModelInitializer {
+        private final Symbol<T> symbol;
+        private final Seed<T> seed;
+
+        public SeedInitializer(Symbol<T> symbol, Seed<T> seed) {
+                this.symbol = symbol;
+                this.seed = seed;
+        }
+
+        @Override
+        public void initialize(Model model, int nodeCount) {
+                var interpretation = model.getInterpretation(symbol);
+                var cursor = seed.getCursor(symbol.defaultValue(), nodeCount);
+                interpretation.putAll(cursor);
+        }
+}
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/seed/UniformSeed.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/seed/UniformSeed.java
deleted file mode 100644
index 451d1513..00000000
--- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/seed/UniformSeed.java
+++ /dev/null
@@ -1,27 +0,0 @@
-/*
- * SPDX-FileCopyrightText: 2021-2023 The Refinery Authors <https://refinery.tools/>
- *
- * SPDX-License-Identifier: EPL-2.0
- */
-package tools.refinery.store.reasoning.seed;
-
-import tools.refinery.store.map.Cursor;
-import tools.refinery.store.tuple.Tuple;
-
-public record UniformSeed<T>(int arity, T reducedValue) implements Seed<T> {
-        public UniformSeed {
-                if (arity < 0) {
-                        throw new IllegalArgumentException("Arity must not be negative");
-                }
-        }
-
-        @Override
-        public T get(Tuple key) {
-                return reducedValue;
-        }
-
-        @Override
-        public Cursor<Tuple, T> getCursor(T defaultValue, int nodeCount) {
-                return null;
-        }
-}
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/Advice.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/Advice.java
deleted file mode 100644
index d6a9e02c..00000000
--- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/Advice.java
+++ /dev/null
@@ -1,159 +0,0 @@
-/*
- * SPDX-FileCopyrightText: 2021-2023 The Refinery Authors <https://refinery.tools/>
- *
- * SPDX-License-Identifier: EPL-2.0
- */
-package tools.refinery.store.reasoning.translator;
-
-import tools.refinery.store.query.substitution.Substitution;
-import tools.refinery.store.reasoning.representation.AnyPartialSymbol;
-import tools.refinery.store.reasoning.representation.PartialRelation;
-import tools.refinery.store.query.term.Variable;
-import tools.refinery.store.query.literal.Literal;
-
-import java.util.*;
-
-public final class Advice {
-        private final AnyPartialSymbol source;
-        private final PartialRelation target;
-        private final AdviceSlot slot;
-        private final boolean mandatory;
-        private final List<Variable> parameters;
-        private final List<Literal> literals;
-        private boolean processed;
-
-        public Advice(AnyPartialSymbol source, PartialRelation target, AdviceSlot slot, boolean mandatory, List<Variable> parameters, List<Literal> literals) {
-                if (mandatory && !slot.isMonotonic()) {
-                        throw new IllegalArgumentException("Only monotonic advice can be mandatory");
-                }
-                this.source = source;
-                this.target = target;
-                this.slot = slot;
-                this.mandatory = mandatory;
-                checkArity(parameters);
-                this.parameters = parameters;
-                this.literals = literals;
-        }
-
-        public AnyPartialSymbol source() {
-                return source;
-        }
-
-        public PartialRelation target() {
-                return target;
-        }
-
-        public AdviceSlot slot() {
-                return slot;
-        }
-
-        public boolean mandatory() {
-                return mandatory;
-        }
-
-        public List<Variable> parameters() {
-                return parameters;
-        }
-
-        public List<Literal> literals() {
-                return literals;
-        }
-
-        public boolean processed() {
-                return processed;
-        }
-
-        public List<Literal> substitute(List<Variable> substituteParameters) {
-                checkArity(substituteParameters);
-                markProcessed();
-                // Use a renewing substitution to remove any non-parameter variables and avoid clashed between variables
-                // coming from different advice in the same clause.
-                var substitution = Substitution.builder().putManyChecked(parameters, substituteParameters).renewing().build();
-                return literals.stream().map(literal -> literal.substitute(substitution)).toList();
-        }
-
-        private void markProcessed() {
-                processed = true;
-        }
-
-        public void checkProcessed() {
-                if (mandatory && !processed) {
-                        throw new IllegalStateException("Mandatory advice %s was not processed".formatted(this));
-                }
-        }
-
-        private void checkArity(List<Variable> toCheck) {
-                if (toCheck.size() != target.arity()) {
-                        throw new IllegalArgumentException("%s needs %d parameters, but got %s".formatted(target.name(),
-                                        target.arity(), parameters.size()));
-                }
-        }
-
-        public static Builder builderFor(AnyPartialSymbol source, PartialRelation target, AdviceSlot slot) {
-                return new Builder(source, target, slot);
-        }
-
-
-        @Override
-        public String toString() {
-                return "Advice[source=%s, target=%s, slot=%s, mandatory=%s, parameters=%s, literals=%s]".formatted(source,
-                                target, slot, mandatory, parameters, literals);
-        }
-
-        public static class Builder {
-                private final AnyPartialSymbol source;
-                private final PartialRelation target;
-                private final AdviceSlot slot;
-                private boolean mandatory;
-                private final List<Variable> parameters = new ArrayList<>();
-                private final List<Literal> literals = new ArrayList<>();
-
-                private Builder(AnyPartialSymbol source, PartialRelation target, AdviceSlot slot) {
-                        this.source = source;
-                        this.target = target;
-                        this.slot = slot;
-                }
-
-                public Builder mandatory(boolean mandatory) {
-                        this.mandatory = mandatory;
-                        return this;
-                }
-
-                public Builder mandatory() {
-                        return mandatory(false);
-                }
-
-                public Builder parameters(List<Variable> variables) {
-                        parameters.addAll(variables);
-                        return this;
-                }
-
-                public Builder parameters(Variable... variables) {
-                        return parameters(List.of(variables));
-                }
-
-                public Builder parameter(Variable variable) {
-                        parameters.add(variable);
-                        return this;
-                }
-
-                public Builder literals(Collection<Literal> literals) {
-                        this.literals.addAll(literals);
-                        return this;
-                }
-
-                public Builder literals(Literal... literals) {
-                        return literals(List.of(literals));
-                }
-
-                public Builder literal(Literal literal) {
-                        literals.add(literal);
-                        return this;
-                }
-
-                public Advice build() {
-                        return new Advice(source, target, slot, mandatory, Collections.unmodifiableList(parameters),
-                                        Collections.unmodifiableList(literals));
-                }
-        }
-}
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/AdviceSlot.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/AdviceSlot.java
deleted file mode 100644
index bab20340..00000000
--- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/AdviceSlot.java
+++ /dev/null
@@ -1,30 +0,0 @@
-/*
- * SPDX-FileCopyrightText: 2021-2023 The Refinery Authors <https://refinery.tools/>
- *
- * SPDX-License-Identifier: EPL-2.0
- */
-package tools.refinery.store.reasoning.translator;
-
-import tools.refinery.store.representation.TruthValue;
-
-public enum AdviceSlot {
-        EXTEND_MUST(true),
-
-        RESTRICT_MAY(true),
-
-        /**
-         * Same as {@link #RESTRICT_MAY}, but only active if the value of the relation is not {@link TruthValue#TRUE} or
-         * {@link TruthValue#ERROR}.
-         */
-        RESTRICT_NEW(false);
-
-        private final boolean monotonic;
-
-        AdviceSlot(boolean monotonic) {
-                this.monotonic = monotonic;
-        }
-
-        public boolean isMonotonic() {
-                return monotonic;
-        }
-}
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/AnyPartialSymbolTranslator.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/AnyPartialSymbolTranslator.java
new file mode 100644
index 00000000..48c84348
--- /dev/null
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/AnyPartialSymbolTranslator.java
@@ -0,0 +1,16 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.reasoning.translator;
+
+import tools.refinery.store.model.ModelStoreBuilder;
+import tools.refinery.store.model.ModelStoreConfiguration;
+import tools.refinery.store.reasoning.representation.AnyPartialSymbol;
+
+public sealed interface AnyPartialSymbolTranslator extends ModelStoreConfiguration permits PartialSymbolTranslator {
+        AnyPartialSymbol getPartialSymbol();
+
+        void configure(ModelStoreBuilder storeBuilder);
+}
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/PartialRelationTranslator.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/PartialRelationTranslator.java
new file mode 100644
index 00000000..fe8e8d6c
--- /dev/null
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/PartialRelationTranslator.java
@@ -0,0 +1,263 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.reasoning.translator;
+
+import tools.refinery.store.model.ModelStoreBuilder;
+import tools.refinery.store.query.Constraint;
+import tools.refinery.store.query.ModelQueryBuilder;
+import tools.refinery.store.query.dnf.Query;
+import tools.refinery.store.query.dnf.RelationalQuery;
+import tools.refinery.store.query.term.Variable;
+import tools.refinery.store.query.view.MayView;
+import tools.refinery.store.query.view.MustView;
+import tools.refinery.store.reasoning.ReasoningBuilder;
+import tools.refinery.store.reasoning.interpretation.PartialInterpretation;
+import tools.refinery.store.reasoning.interpretation.PartialRelationRewriter;
+import tools.refinery.store.reasoning.interpretation.QueryBasedRelationInterpretationFactory;
+import tools.refinery.store.reasoning.interpretation.QueryBasedRelationRewriter;
+import tools.refinery.store.reasoning.literal.Concreteness;
+import tools.refinery.store.reasoning.literal.Modality;
+import tools.refinery.store.reasoning.refinement.ConcreteSymbolRefiner;
+import tools.refinery.store.reasoning.refinement.PartialInterpretationRefiner;
+import tools.refinery.store.reasoning.refinement.StorageRefiner;
+import tools.refinery.store.reasoning.representation.PartialRelation;
+import tools.refinery.store.representation.AnySymbol;
+import tools.refinery.store.representation.Symbol;
+import tools.refinery.store.representation.TruthValue;
+
+@SuppressWarnings("UnusedReturnValue")
+public final class PartialRelationTranslator extends PartialSymbolTranslator<TruthValue, Boolean> {
+        private final PartialRelation partialRelation;
+        private PartialRelationRewriter rewriter;
+        private Query<Boolean> query;
+        private Query<Boolean> may;
+        private Query<Boolean> must;
+        private Query<Boolean> candidateMay;
+        private Query<Boolean> candidateMust;
+        private RoundingMode roundingMode;
+
+        private PartialRelationTranslator(PartialRelation partialRelation) {
+                super(partialRelation);
+                this.partialRelation = partialRelation;
+        }
+
+        public PartialRelation getPartialRelation() {
+                return partialRelation;
+        }
+
+        @Override
+        public PartialRelationTranslator symbol(AnySymbol storageSymbol) {
+                super.symbol(storageSymbol);
+                return this;
+        }
+
+        @Override
+        public <T> PartialRelationTranslator symbol(Symbol<T> storageSymbol,
+                                                                                                StorageRefiner.Factory<T> storageRefiner) {
+                super.symbol(storageSymbol, storageRefiner);
+                return this;
+        }
+
+        @Override
+        public PartialRelationTranslator interpretation(
+                        PartialInterpretation.Factory<TruthValue, Boolean> interpretationFactory) {
+                super.interpretation(interpretationFactory);
+                return this;
+        }
+
+        @Override
+        public PartialRelationTranslator refiner(
+                        PartialInterpretationRefiner.Factory<TruthValue, Boolean> interpretationRefiner) {
+                super.refiner(interpretationRefiner);
+                return this;
+        }
+
+        public PartialRelationTranslator rewriter(PartialRelationRewriter rewriter) {
+                checkNotConfigured();
+                if (this.rewriter != null) {
+                        throw new IllegalArgumentException("Rewriter was already set");
+                }
+                this.rewriter = rewriter;
+                return this;
+        }
+
+        public PartialRelationTranslator query(RelationalQuery query) {
+                checkNotConfigured();
+                if (this.query != null) {
+                        throw new IllegalArgumentException("Query was already set");
+                }
+                this.query = query;
+                return this;
+        }
+
+        public PartialRelationTranslator may(RelationalQuery may) {
+                checkNotConfigured();
+                if (this.may != null) {
+                        throw new IllegalArgumentException("May query was already set");
+                }
+                this.may = may;
+                return this;
+        }
+
+        public PartialRelationTranslator must(RelationalQuery must) {
+                checkNotConfigured();
+                if (this.must != null) {
+                        throw new IllegalArgumentException("Must query was already set");
+                }
+                this.must = must;
+                return this;
+        }
+
+        public PartialRelationTranslator candidate(RelationalQuery candidate) {
+                candidateMay(candidate);
+                candidateMust(candidate);
+                return this;
+        }
+
+        public PartialRelationTranslator candidateMay(RelationalQuery candidateMay) {
+                checkNotConfigured();
+                if (this.candidateMay != null) {
+                        throw new IllegalArgumentException("Candidate may query was already set");
+                }
+                this.candidateMay = candidateMay;
+                return this;
+        }
+
+        public PartialRelationTranslator candidateMust(RelationalQuery candidateMust) {
+                checkNotConfigured();
+                if (this.candidateMust != null) {
+                        throw new IllegalArgumentException("Candidate must query was already set");
+                }
+                this.candidateMust = candidateMust;
+                return this;
+        }
+
+        public PartialRelationTranslator roundingMode(RoundingMode roundingMode) {
+                checkNotConfigured();
+                if (this.roundingMode != null) {
+                        throw new IllegalArgumentException("Rounding mode was already set");
+                }
+                this.roundingMode = roundingMode;
+                return this;
+        }
+
+        @Override
+        protected void doConfigure(ModelStoreBuilder storeBuilder) {
+                setFallbackRoundingMode();
+                createFallbackQueryFromRewriter();
+                liftQueries(storeBuilder);
+                createFallbackQueriesFromSymbol();
+                setFallbackCandidateQueries();
+                createFallbackRewriter();
+                createFallbackInterpretation(storeBuilder);
+                createFallbackRefiner();
+                super.doConfigure(storeBuilder);
+        }
+
+        private void setFallbackRoundingMode() {
+                if (roundingMode == null) {
+                        roundingMode = query == null && storageSymbol != null ? RoundingMode.PREFER_FALSE : RoundingMode.NONE;
+                }
+        }
+
+        private RelationalQuery createQuery(Constraint constraint) {
+                int arity = partialRelation.arity();
+                var queryBuilder = Query.builder(partialRelation.name());
+                var parameters = new Variable[arity];
+                for (int i = 0; i < arity; i++) {
+                        parameters[i] = queryBuilder.parameter("p" + 1);
+                }
+                queryBuilder.clause(constraint.call(parameters));
+                return queryBuilder.build();
+        }
+
+        private void createFallbackQueryFromRewriter() {
+                if (rewriter != null && query == null) {
+                        query = createQuery(partialRelation);
+                }
+        }
+
+        private void createFallbackQueriesFromSymbol() {
+                if (storageSymbol == null || storageSymbol.valueType() != TruthValue.class) {
+                        return;
+                }
+                // We checked in the guard clause that this is safe.
+                @SuppressWarnings("unchecked")
+                var typedStorageSymbol = (Symbol<TruthValue>) storageSymbol;
+                var defaultValue = typedStorageSymbol.defaultValue();
+                if (may == null && !defaultValue.may()) {
+                        may = createQuery(new MayView(typedStorageSymbol));
+                }
+                if (must == null && !defaultValue.must()) {
+                        must = createQuery(new MustView(typedStorageSymbol));
+                }
+        }
+
+        private void liftQueries(ModelStoreBuilder storeBuilder) {
+                if (query != null) {
+                        var reasoningBuilder = storeBuilder.getAdapter(ReasoningBuilder.class);
+                        if (may == null) {
+                                may = reasoningBuilder.lift(Modality.MAY, Concreteness.PARTIAL, query);
+                        }
+                        if (must == null) {
+                                must = reasoningBuilder.lift(Modality.MUST, Concreteness.PARTIAL, query);
+                        }
+                        if (candidateMay == null) {
+                                candidateMay = reasoningBuilder.lift(Modality.MAY, Concreteness.CANDIDATE, query);
+                        }
+                        if (candidateMust == null) {
+                                candidateMust = reasoningBuilder.lift(Modality.MAY, Concreteness.CANDIDATE, query);
+                        }
+                }
+        }
+
+        private void setFallbackCandidateQueries() {
+                if (candidateMay == null) {
+                        candidateMay = switch (roundingMode) {
+                                case NONE, PREFER_TRUE -> may;
+                                case PREFER_FALSE -> must;
+                        };
+                }
+                if (candidateMust == null) {
+                        candidateMust = switch (roundingMode) {
+                                case NONE, PREFER_FALSE -> must;
+                                case PREFER_TRUE -> may;
+                        };
+                }
+        }
+
+        private void createFallbackRewriter() {
+                if (rewriter == null) {
+                        rewriter = new QueryBasedRelationRewriter(may, must, candidateMay, candidateMust);
+                }
+        }
+
+        private void createFallbackInterpretation(ModelStoreBuilder storeBuilder) {
+                if (interpretationFactory == null) {
+                        var queryBuilder = storeBuilder.getAdapter(ModelQueryBuilder.class);
+                        interpretationFactory = new QueryBasedRelationInterpretationFactory(may, must, candidateMay, candidateMust);
+                        queryBuilder.queries(may, must, candidateMay, candidateMust);
+                }
+        }
+
+        private void createFallbackRefiner() {
+                if (interpretationRefiner == null && storageSymbol != null && storageSymbol.valueType() == TruthValue.class) {
+                        // We checked in the condition that this is safe.
+                        @SuppressWarnings("unchecked")
+                        var typedStorageSymbol = (Symbol<TruthValue>) storageSymbol;
+                        interpretationRefiner = ConcreteSymbolRefiner.of(typedStorageSymbol);
+                }
+        }
+
+        public PartialRelationRewriter getRewriter() {
+                checkConfigured();
+                return rewriter;
+        }
+
+        public static PartialRelationTranslator of(PartialRelation relation) {
+                return new PartialRelationTranslator(relation);
+        }
+}
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/PartialSymbolTranslator.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/PartialSymbolTranslator.java
new file mode 100644
index 00000000..07d1d19b
--- /dev/null
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/PartialSymbolTranslator.java
@@ -0,0 +1,156 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.reasoning.translator;
+
+import tools.refinery.store.model.ModelStoreBuilder;
+import tools.refinery.store.reasoning.ReasoningBuilder;
+import tools.refinery.store.reasoning.interpretation.PartialInterpretation;
+import tools.refinery.store.reasoning.refinement.PartialInterpretationRefiner;
+import tools.refinery.store.reasoning.refinement.PartialModelInitializer;
+import tools.refinery.store.reasoning.refinement.StorageRefiner;
+import tools.refinery.store.reasoning.representation.PartialSymbol;
+import tools.refinery.store.reasoning.seed.Seed;
+import tools.refinery.store.reasoning.seed.SeedInitializer;
+import tools.refinery.store.representation.AnySymbol;
+import tools.refinery.store.representation.Symbol;
+
+@SuppressWarnings("UnusedReturnValue")
+public abstract sealed class PartialSymbolTranslator<A, C> implements AnyPartialSymbolTranslator
+                permits PartialRelationTranslator {
+        private final PartialSymbol<A, C> partialSymbol;
+        private boolean configured = false;
+        protected PartialInterpretationRefiner.Factory<A, C> interpretationRefiner;
+        protected AnySymbol storageSymbol;
+        protected StorageRefiner.Factory<?> storageRefiner;
+        protected PartialInterpretation.Factory<A, C> interpretationFactory;
+        protected PartialModelInitializer initializer;
+
+        PartialSymbolTranslator(PartialSymbol<A, C> partialSymbol) {
+                this.partialSymbol = partialSymbol;
+        }
+
+        @Override
+        public PartialSymbol<A, C> getPartialSymbol() {
+                return partialSymbol;
+        }
+
+        @Override
+        public void apply(ModelStoreBuilder storeBuilder) {
+                storeBuilder.getAdapter(ReasoningBuilder.class).partialSymbol(this);
+        }
+
+        public boolean isConfigured() {
+                return configured;
+        }
+
+        protected void checkConfigured() {
+                if (!configured) {
+                        throw new IllegalStateException("Partial symbol was not configured");
+                }
+        }
+
+        protected void checkNotConfigured() {
+                if (configured) {
+                        throw new IllegalStateException("Partial symbol was already configured");
+                }
+        }
+
+        public PartialSymbolTranslator<A, C> symbol(AnySymbol storageSymbol) {
+                return symbol((Symbol<?>) storageSymbol, null);
+        }
+
+        public <T> PartialSymbolTranslator<A, C> symbol(Symbol<T> storageSymbol,
+                                                                                                        StorageRefiner.Factory<T> storageRefiner) {
+                checkNotConfigured();
+                if (this.storageSymbol != null) {
+                        throw new IllegalStateException("Representation symbol was already set");
+                }
+                this.storageSymbol = storageSymbol;
+                this.storageRefiner = storageRefiner;
+                return this;
+        }
+
+        public PartialSymbolTranslator<A, C> interpretation(PartialInterpretation.Factory<A, C> interpretationFactory) {
+                checkNotConfigured();
+                if (this.interpretationFactory != null) {
+                        throw new IllegalStateException("Interpretation factory was already set");
+                }
+                this.interpretationFactory = interpretationFactory;
+                return this;
+        }
+
+        public PartialSymbolTranslator<A, C> refiner(PartialInterpretationRefiner.Factory<A, C> interpretationRefiner) {
+                checkNotConfigured();
+                if (this.interpretationRefiner != null) {
+                        throw new IllegalStateException("Interpretation refiner was already set");
+                }
+                this.interpretationRefiner = interpretationRefiner;
+                return this;
+        }
+
+        public PartialSymbolTranslator<A, C> initializer(PartialModelInitializer initializer) {
+                checkNotConfigured();
+                if (this.initializer != null) {
+                        throw new IllegalStateException("Initializer was already set");
+                }
+                this.initializer = initializer;
+                return this;
+        }
+
+        public <T> PartialSymbolTranslator<A, C> seed(Seed<T> seed) {
+                if (storageSymbol == null) {
+                        throw new IllegalArgumentException("Seed requires setting a storage symbol");
+                }
+                if (!seed.valueType().equals(storageSymbol.valueType())) {
+                        throw new IllegalArgumentException("Seed type %s does not match storage symbol type %s"
+                                        .formatted(seed.valueType(), storageSymbol.valueType()));
+                }
+                // The guard clause only allows a well-typed seed.
+                @SuppressWarnings("unchecked")
+                var typedStorageSymbol = (Symbol<T>) storageSymbol;
+                return initializer(new SeedInitializer<>(typedStorageSymbol, seed));
+        }
+
+        @Override
+        public void configure(ModelStoreBuilder storeBuilder) {
+                checkNotConfigured();
+                doConfigure(storeBuilder);
+                configured = true;
+        }
+
+        protected void doConfigure(ModelStoreBuilder storeBuilder) {
+                if (interpretationFactory == null) {
+                        throw new IllegalArgumentException("Interpretation factory must be set");
+                }
+                var reasoningBuilder = storeBuilder.getAdapter(ReasoningBuilder.class);
+                if (storageSymbol != null) {
+                        storeBuilder.symbol(storageSymbol);
+                        if (storageRefiner != null) {
+                                registerStorageRefiner(reasoningBuilder, storageRefiner);
+                        }
+                }
+                if (initializer != null) {
+                        reasoningBuilder.initializer(initializer);
+                }
+        }
+
+        private <T> void registerStorageRefiner(ReasoningBuilder reasoningBuilder, StorageRefiner.Factory<T> factory) {
+                // The builder only allows setting a well-typed representation refiner.
+                @SuppressWarnings("unchecked")
+                var typedStorageSymbol = (Symbol<T>) storageSymbol;
+                reasoningBuilder.storageRefiner(typedStorageSymbol, factory);
+        }
+
+        public PartialInterpretation.Factory<A, C> getInterpretationFactory() {
+                checkConfigured();
+                return interpretationFactory;
+        }
+
+        public PartialInterpretationRefiner.Factory<A, C> getInterpretationRefiner() {
+                checkConfigured();
+                return interpretationRefiner;
+        }
+}
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/RoundingMode.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/RoundingMode.java
new file mode 100644
index 00000000..dd956a50
--- /dev/null
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/RoundingMode.java
@@ -0,0 +1,12 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.reasoning.translator;
+
+public enum RoundingMode {
+        NONE,
+        PREFER_TRUE,
+        PREFER_FALSE
+}
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/TranslatedRelation.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/TranslatedRelation.java
deleted file mode 100644
index 4a5a8843..00000000
--- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/TranslatedRelation.java
+++ /dev/null
@@ -1,27 +0,0 @@
-/*
- * SPDX-FileCopyrightText: 2021-2023 The Refinery Authors <https://refinery.tools/>
- *
- * SPDX-License-Identifier: EPL-2.0
- */
-package tools.refinery.store.reasoning.translator;
-
-import tools.refinery.store.model.Model;
-import tools.refinery.store.query.term.Variable;
-import tools.refinery.store.query.literal.CallPolarity;
-import tools.refinery.store.query.literal.Literal;
-import tools.refinery.store.reasoning.PartialInterpretation;
-import tools.refinery.store.reasoning.literal.Modality;
-import tools.refinery.store.reasoning.representation.PartialRelation;
-import tools.refinery.store.representation.TruthValue;
-
-import java.util.List;
-
-public interface TranslatedRelation {
-        PartialRelation getSource();
-
-        void configure(List<Advice> advices);
-
-        List<Literal> call(CallPolarity polarity, Modality modality, List<Variable> arguments);
-
-        PartialInterpretation<TruthValue, Boolean> createPartialInterpretation(Model model);
-}
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/TranslationUnit.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/TranslationUnit.java
deleted file mode 100644
index 6e44a7d7..00000000
--- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/TranslationUnit.java
+++ /dev/null
@@ -1,32 +0,0 @@
-/*
- * SPDX-FileCopyrightText: 2021-2023 The Refinery Authors <https://refinery.tools/>
- *
- * SPDX-License-Identifier: EPL-2.0
- */
-package tools.refinery.store.reasoning.translator;
-
-import tools.refinery.store.model.Model;
-import tools.refinery.store.reasoning.ReasoningBuilder;
-
-import java.util.Collection;
-
-public abstract class TranslationUnit {
-        private ReasoningBuilder reasoningBuilder;
-
-        protected ReasoningBuilder getReasoningBuilder() {
-                return reasoningBuilder;
-        }
-
-        public void setPartialInterpretationBuilder(ReasoningBuilder reasoningBuilder) {
-                this.reasoningBuilder = reasoningBuilder;
-                configureReasoningBuilder();
-        }
-
-        protected void configureReasoningBuilder() {
-                // Nothing to configure by default.
-        }
-
-        public abstract Collection<TranslatedRelation> getTranslatedRelations();
-
-        public abstract void initializeModel(Model model, int nodeCount);
-}
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/base/BaseDecisionInterpretation.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/base/BaseDecisionInterpretation.java
deleted file mode 100644
index 2a151aa2..00000000
--- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/base/BaseDecisionInterpretation.java
+++ /dev/null
@@ -1,93 +0,0 @@
-/*
- * SPDX-FileCopyrightText: 2021-2023 The Refinery Authors <https://refinery.tools/>
- *
- * SPDX-License-Identifier: EPL-2.0
- */
-package tools.refinery.store.reasoning.translator.base;
-
-import tools.refinery.store.map.Cursor;
-import tools.refinery.store.model.Interpretation;
-import tools.refinery.store.query.resultset.ResultSet;
-import tools.refinery.store.reasoning.MergeResult;
-import tools.refinery.store.reasoning.PartialInterpretation;
-import tools.refinery.store.reasoning.ReasoningAdapter;
-import tools.refinery.store.reasoning.representation.PartialRelation;
-import tools.refinery.store.representation.TruthValue;
-import tools.refinery.store.tuple.Tuple;
-
-public class BaseDecisionInterpretation implements PartialInterpretation<TruthValue, Boolean> {
-        private final ReasoningAdapter reasoningAdapter;
-        private PartialRelation partialRelation;
-        private final ResultSet<Boolean> mustResultSet;
-        private final ResultSet<Boolean> mayResultSet;
-        private final ResultSet<Boolean> errorResultSet;
-        private final ResultSet<Boolean> currentResultSet;
-        private final Interpretation<TruthValue> interpretation;
-
-        public BaseDecisionInterpretation(ReasoningAdapter reasoningAdapter, ResultSet<Boolean> mustResultSet,
-                                                                          ResultSet<Boolean> mayResultSet, ResultSet<Boolean> errorResultSet,
-                                                                          ResultSet<Boolean> currentResultSet, Interpretation<TruthValue> interpretation) {
-                this.reasoningAdapter = reasoningAdapter;
-                this.mustResultSet = mustResultSet;
-                this.mayResultSet = mayResultSet;
-                this.errorResultSet = errorResultSet;
-                this.currentResultSet = currentResultSet;
-                this.interpretation = interpretation;
-        }
-
-        @Override
-        public ReasoningAdapter getAdapter() {
-                return reasoningAdapter;
-        }
-
-        @Override
-        public int countUnfinished() {
-                return 0;
-        }
-
-        @Override
-        public int countErrors() {
-                return errorResultSet.size();
-        }
-
-        @Override
-        public PartialRelation getPartialSymbol() {
-                return partialRelation;
-        }
-
-        @Override
-        public TruthValue get(Tuple key) {
-                return null;
-        }
-
-        @Override
-        public Cursor<Tuple, TruthValue> getAll() {
-                return null;
-        }
-
-        @Override
-        public MergeResult merge(Tuple key, TruthValue value) {
-                TruthValue newValue;
-                switch (value) {
-                case UNKNOWN -> {
-                        return MergeResult.UNCHANGED;
-                }
-                case TRUE -> newValue = mayResultSet.get(key) ? TruthValue.TRUE : TruthValue.ERROR;
-                case FALSE -> newValue = mustResultSet.get(key) ? TruthValue.ERROR : TruthValue.FALSE;
-                case ERROR -> newValue = TruthValue.ERROR;
-                default -> throw new IllegalArgumentException("Unknown truth value: " + value);
-                }
-                var oldValue = interpretation.put(key, newValue);
-                return oldValue == TruthValue.ERROR ? MergeResult.UNCHANGED : MergeResult.REFINED;
-        }
-
-        @Override
-        public Boolean getConcrete(Tuple key) {
-                return currentResultSet.get(key);
-        }
-
-        @Override
-        public Cursor<Tuple, Boolean> getAllConcrete() {
-                return null;
-        }
-}
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/base/BaseDecisionTranslationUnit.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/base/BaseDecisionTranslationUnit.java
deleted file mode 100644
index a1e4b816..00000000
--- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/base/BaseDecisionTranslationUnit.java
+++ /dev/null
@@ -1,49 +0,0 @@
-/*
- * SPDX-FileCopyrightText: 2021-2023 The Refinery Authors <https://refinery.tools/>
- *
- * SPDX-License-Identifier: EPL-2.0
- */
-package tools.refinery.store.reasoning.translator.base;
-
-import tools.refinery.store.model.Model;
-import tools.refinery.store.reasoning.representation.PartialRelation;
-import tools.refinery.store.reasoning.seed.Seed;
-import tools.refinery.store.reasoning.seed.UniformSeed;
-import tools.refinery.store.reasoning.translator.TranslatedRelation;
-import tools.refinery.store.reasoning.translator.TranslationUnit;
-import tools.refinery.store.representation.Symbol;
-import tools.refinery.store.representation.TruthValue;
-
-import java.util.Collection;
-import java.util.List;
-
-public class BaseDecisionTranslationUnit extends TranslationUnit {
-        private final PartialRelation partialRelation;
-        private final Seed<TruthValue> seed;
-        private final Symbol<TruthValue> symbol;
-
-        public BaseDecisionTranslationUnit(PartialRelation partialRelation, Seed<TruthValue> seed) {
-                if (seed.arity() != partialRelation.arity()) {
-                        throw new IllegalArgumentException("Expected seed with arity %d for %s, got arity %s"
-                                        .formatted(partialRelation.arity(), partialRelation, seed.arity()));
-                }
-                this.partialRelation = partialRelation;
-                this.seed = seed;
-                symbol = Symbol.of(partialRelation.name(), partialRelation.arity(), TruthValue.class, TruthValue.UNKNOWN);
-        }
-
-        public BaseDecisionTranslationUnit(PartialRelation partialRelation) {
-                this(partialRelation, new UniformSeed<>(partialRelation.arity(), TruthValue.UNKNOWN));
-        }
-
-        @Override
-        public Collection<TranslatedRelation> getTranslatedRelations() {
-                return List.of(new TranslatedBaseDecision(getReasoningBuilder(), partialRelation, symbol));
-        }
-
-        @Override
-        public void initializeModel(Model model, int nodeCount) {
-                var interpretation = model.getInterpretation(symbol);
-                interpretation.putAll(seed.getCursor(TruthValue.UNKNOWN, nodeCount));
-        }
-}
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/base/TranslatedBaseDecision.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/base/TranslatedBaseDecision.java
deleted file mode 100644
index 4782eb46..00000000
--- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/base/TranslatedBaseDecision.java
+++ /dev/null
@@ -1,54 +0,0 @@
-/*
- * SPDX-FileCopyrightText: 2021-2023 The Refinery Authors <https://refinery.tools/>
- *
- * SPDX-License-Identifier: EPL-2.0
- */
-package tools.refinery.store.reasoning.translator.base;
-
-import tools.refinery.store.model.Model;
-import tools.refinery.store.query.term.Variable;
-import tools.refinery.store.query.literal.CallPolarity;
-import tools.refinery.store.query.literal.Literal;
-import tools.refinery.store.reasoning.PartialInterpretation;
-import tools.refinery.store.reasoning.ReasoningBuilder;
-import tools.refinery.store.reasoning.literal.Modality;
-import tools.refinery.store.reasoning.representation.PartialRelation;
-import tools.refinery.store.reasoning.translator.Advice;
-import tools.refinery.store.reasoning.translator.TranslatedRelation;
-import tools.refinery.store.representation.Symbol;
-import tools.refinery.store.representation.TruthValue;
-
-import java.util.List;
-
-class TranslatedBaseDecision implements TranslatedRelation {
-        private final ReasoningBuilder reasoningBuilder;
-        private final PartialRelation partialRelation;
-        private final Symbol<TruthValue> symbol;
-
-        public TranslatedBaseDecision(ReasoningBuilder reasoningBuilder, PartialRelation partialRelation,
-                                                                  Symbol<TruthValue> symbol) {
-                this.reasoningBuilder = reasoningBuilder;
-                this.partialRelation = partialRelation;
-                this.symbol = symbol;
-        }
-
-        @Override
-        public PartialRelation getSource() {
-                return partialRelation;
-        }
-
-        @Override
-        public void configure(List<Advice> advices) {
-
-        }
-
-        @Override
-        public List<Literal> call(CallPolarity polarity, Modality modality, List<Variable> arguments) {
-                return null;
-        }
-
-        @Override
-        public PartialInterpretation<TruthValue, Boolean> createPartialInterpretation(Model model) {
-                return null;
-        }
-}
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/InferredMayTypeView.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/InferredMayTypeView.java
deleted file mode 100644
index 40de4644..00000000
--- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/InferredMayTypeView.java
+++ /dev/null
@@ -1,40 +0,0 @@
-/*
- * SPDX-FileCopyrightText: 2021-2023 The Refinery Authors <https://refinery.tools/>
- *
- * SPDX-License-Identifier: EPL-2.0
- */
-package tools.refinery.store.reasoning.translator.typehierarchy;
-
-import tools.refinery.store.reasoning.representation.PartialRelation;
-import tools.refinery.store.query.view.TuplePreservingView;
-import tools.refinery.store.tuple.Tuple;
-
-import java.util.Objects;
-
-class InferredMayTypeView extends TuplePreservingView<InferredType> {
-        private final PartialRelation type;
-
-        InferredMayTypeView(PartialRelation type) {
-                super(TypeHierarchyTranslationUnit.INFERRED_TYPE_SYMBOL, "%s#may".formatted(type));
-                this.type = type;
-        }
-
-        @Override
-        protected boolean doFilter(Tuple key, InferredType value) {
-                return value.mayConcreteTypes().contains(type);
-        }
-
-        @Override
-        public boolean equals(Object o) {
-                if (this == o) return true;
-                if (o == null || getClass() != o.getClass()) return false;
-                if (!super.equals(o)) return false;
-                InferredMayTypeView that = (InferredMayTypeView) o;
-                return Objects.equals(type, that.type);
-        }
-
-        @Override
-        public int hashCode() {
-                return Objects.hash(super.hashCode(), type);
-        }
-}
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/InferredMustTypeView.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/InferredMustTypeView.java
deleted file mode 100644
index 1a121547..00000000
--- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/InferredMustTypeView.java
+++ /dev/null
@@ -1,40 +0,0 @@
-/*
- * SPDX-FileCopyrightText: 2021-2023 The Refinery Authors <https://refinery.tools/>
- *
- * SPDX-License-Identifier: EPL-2.0
- */
-package tools.refinery.store.reasoning.translator.typehierarchy;
-
-import tools.refinery.store.reasoning.representation.PartialRelation;
-import tools.refinery.store.query.view.TuplePreservingView;
-import tools.refinery.store.tuple.Tuple;
-
-import java.util.Objects;
-
-class InferredMustTypeView extends TuplePreservingView<InferredType> {
-        private final PartialRelation type;
-
-        InferredMustTypeView(PartialRelation type) {
-                super(TypeHierarchyTranslationUnit.INFERRED_TYPE_SYMBOL, "%s#must".formatted(type));
-                this.type = type;
-        }
-
-        @Override
-        protected boolean doFilter(Tuple key, InferredType value) {
-                return value.mustTypes().contains(type);
-        }
-
-        @Override
-        public boolean equals(Object o) {
-                if (this == o) return true;
-                if (o == null || getClass() != o.getClass()) return false;
-                if (!super.equals(o)) return false;
-                InferredMustTypeView that = (InferredMustTypeView) o;
-                return Objects.equals(type, that.type);
-        }
-
-        @Override
-        public int hashCode() {
-                return Objects.hash(super.hashCode(), type);
-        }
-}
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeHierarchyTranslationUnit.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeHierarchyTranslationUnit.java
deleted file mode 100644
index 06e3c05f..00000000
--- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeHierarchyTranslationUnit.java
+++ /dev/null
@@ -1,37 +0,0 @@
-/*
- * SPDX-FileCopyrightText: 2021-2023 The Refinery Authors <https://refinery.tools/>
- *
- * SPDX-License-Identifier: EPL-2.0
- */
-package tools.refinery.store.reasoning.translator.typehierarchy;
-
-import tools.refinery.store.model.Model;
-import tools.refinery.store.reasoning.representation.PartialRelation;
-import tools.refinery.store.reasoning.translator.TranslatedRelation;
-import tools.refinery.store.reasoning.translator.TranslationUnit;
-import tools.refinery.store.representation.Symbol;
-
-import java.util.Collection;
-import java.util.List;
-import java.util.Map;
-
-public class TypeHierarchyTranslationUnit extends TranslationUnit {
-        static final Symbol<InferredType> INFERRED_TYPE_SYMBOL = Symbol.of(
-                        "inferredType", 1, InferredType.class, InferredType.UNTYPED);
-
-        private final TypeAnalyzer typeAnalyzer;
-
-        public TypeHierarchyTranslationUnit(Map<PartialRelation, TypeInfo> typeInfoMap) {
-                typeAnalyzer = new TypeAnalyzer(typeInfoMap);
-        }
-
-        @Override
-        public Collection<TranslatedRelation> getTranslatedRelations() {
-                return List.of();
-        }
-
-        @Override
-        public void initializeModel(Model model, int nodeCount) {
-
-        }
-}
diff --git a/subprojects/store-reasoning/src/test/java/tools/refinery/store/reasoning/PartialModelTest.java b/subprojects/store-reasoning/src/test/java/tools/refinery/store/reasoning/PartialModelTest.java
new file mode 100644
index 00000000..f948ad6a
--- /dev/null
+++ b/subprojects/store-reasoning/src/test/java/tools/refinery/store/reasoning/PartialModelTest.java
@@ -0,0 +1,91 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.reasoning;
+
+import org.junit.jupiter.api.Test;
+import tools.refinery.store.model.ModelStore;
+import tools.refinery.store.query.ModelQueryAdapter;
+import tools.refinery.store.query.dnf.Query;
+import tools.refinery.store.query.term.Variable;
+import tools.refinery.store.query.viatra.ViatraModelQueryAdapter;
+import tools.refinery.store.query.view.ForbiddenView;
+import tools.refinery.store.reasoning.literal.Concreteness;
+import tools.refinery.store.reasoning.representation.PartialRelation;
+import tools.refinery.store.reasoning.seed.Seed;
+import tools.refinery.store.reasoning.translator.PartialRelationTranslator;
+import tools.refinery.store.representation.Symbol;
+import tools.refinery.store.representation.TruthValue;
+import tools.refinery.store.tuple.Tuple;
+
+import static org.hamcrest.MatcherAssert.assertThat;
+import static org.hamcrest.Matchers.is;
+import static tools.refinery.store.query.literal.Literals.not;
+import static tools.refinery.store.reasoning.literal.PartialLiterals.may;
+
+class PartialModelTest {
+        @Test
+        void partialModelTest() {
+                var personStorage = Symbol.of("Person", 1, TruthValue.class, TruthValue.FALSE);
+                var friendStorage = Symbol.of("friend", 2, TruthValue.class, TruthValue.UNKNOWN);
+
+                var person = new PartialRelation("Person", 1);
+                var friend = new PartialRelation("friend", 2);
+                var lonely = new PartialRelation("lonely", 1);
+
+                var store = ModelStore.builder()
+                                .with(ViatraModelQueryAdapter.builder())
+                                .with(ReasoningAdapter.builder()
+                                                .initialNodeCount(4))
+                                .with(PartialRelationTranslator.of(ReasoningAdapter.EXISTS_SYMBOL)
+                                                .symbol(Symbol.of("exists", 1, TruthValue.class, TruthValue.FALSE))
+                                                .seed(Seed.builder(ReasoningAdapter.EXISTS_SYMBOL)
+                                                                .put(Tuple.of(0), TruthValue.TRUE)
+                                                                .put(Tuple.of(1), TruthValue.UNKNOWN)
+                                                                .put(Tuple.of(2), TruthValue.TRUE)
+                                                                .put(Tuple.of(3), TruthValue.TRUE)
+                                                                .build()))
+                                .with(PartialRelationTranslator.of(person)
+                                                .symbol(personStorage)
+                                                .seed(Seed.builder(personStorage)
+                                                                .put(Tuple.of(0), TruthValue.TRUE)
+                                                                .put(Tuple.of(1), TruthValue.TRUE)
+                                                                .put(Tuple.of(2), TruthValue.UNKNOWN)
+                                                                .build()))
+                                .with(PartialRelationTranslator.of(friend)
+                                                .symbol(friendStorage)
+                                                .may(Query.of((builder, p1, p2) -> builder.clause(
+                                                                may(person.call(p1)),
+                                                                may(person.call(p2)),
+                                                                // not(must(EQUALS_SYMBOL.call(p1, p2))),
+                                                                not(new ForbiddenView(friendStorage).call(p1, p2))
+                                                )))
+                                                .seed(Seed.builder(friendStorage)
+                                                                .put(Tuple.of(0, 1), TruthValue.TRUE)
+                                                                .put(Tuple.of(1, 2), TruthValue.FALSE)
+                                                                .build()))
+                                .with(PartialRelationTranslator.of(lonely)
+                                                .query(Query.of((builder, p1) -> builder.clause(
+                                                                person.call(p1),
+                                                                not(friend.call(p1, Variable.of())))
+                                                )))
+                                .build();
+
+                var model = store.getAdapter(ReasoningStoreAdapter.class).createInitialModel();
+
+                var queryAdapter = model.getAdapter(ModelQueryAdapter.class);
+                var reasoningAdapter = model.getAdapter(ReasoningAdapter.class);
+                var friendInterpretation = reasoningAdapter.getPartialInterpretation(Concreteness.PARTIAL, friend);
+                assertThat(friendInterpretation.get(Tuple.of(0, 1)), is(TruthValue.TRUE));
+                assertThat(friendInterpretation.get(Tuple.of(1, 0)), is(TruthValue.UNKNOWN));
+                assertThat(friendInterpretation.get(Tuple.of(3, 0)), is(TruthValue.FALSE));
+                var friendRefiner = reasoningAdapter.getRefiner(friend);
+                assertThat(friendRefiner.merge(Tuple.of(0, 1), TruthValue.FALSE), is(true));
+                assertThat(friendRefiner.merge(Tuple.of(1, 0), TruthValue.TRUE), is(true));
+                queryAdapter.flushChanges();
+                assertThat(friendInterpretation.get(Tuple.of(0, 1)), is(TruthValue.ERROR));
+                assertThat(friendInterpretation.get(Tuple.of(1, 0)), is(TruthValue.TRUE));
+        }
+}
diff --git a/subprojects/store-reasoning/src/test/java/tools/refinery/store/reasoning/lifting/DnfLifterTest.java b/subprojects/store-reasoning/src/test/java/tools/refinery/store/reasoning/lifting/DnfLifterTest.java
index ceb9404a..793d1cec 100644
--- a/subprojects/store-reasoning/src/test/java/tools/refinery/store/reasoning/lifting/DnfLifterTest.java
+++ b/subprojects/store-reasoning/src/test/java/tools/refinery/store/reasoning/lifting/DnfLifterTest.java
@@ -55,7 +55,7 @@ class DnfLifterTest {
 
                 var expected = Query.of("Expected", (builder, p1) -> builder.clause((v1) -> List.of(
                                 ModalConstraint.of(Modality.MUST, Concreteness.PARTIAL, friend).call(p1, v1),
-                                ModalConstraint.of(Modality.MUST, Concreteness.PARTIAL, ReasoningAdapter.EXISTS).call(v1)
+                                ModalConstraint.of(Modality.MUST, Concreteness.PARTIAL, ReasoningAdapter.EXISTS_SYMBOL).call(v1)
                 ))).getDnf();
 
                 assertThat(actual, structurallyEqualTo(expected));
@@ -74,7 +74,7 @@ class DnfLifterTest {
 
                 var expected = Query.of("Expected", (builder, p1) -> builder.clause((v1) -> List.of(
                                 ModalConstraint.of(Modality.MUST, Concreteness.PARTIAL, called.getDnf()).call(p1, v1),
-                                ModalConstraint.of(Modality.MUST, Concreteness.PARTIAL, ReasoningAdapter.EXISTS).call(v1)
+                                ModalConstraint.of(Modality.MUST, Concreteness.PARTIAL, ReasoningAdapter.EXISTS_SYMBOL).call(v1)
                 ))).getDnf();
 
                 assertThat(actual, structurallyEqualTo(expected));
@@ -89,7 +89,7 @@ class DnfLifterTest {
 
                 var expected = Query.of("Expected", (builder, p1) -> builder.clause((v1) -> List.of(
                                 friendMustView.call(p1, v1),
-                                ModalConstraint.of(Modality.MUST, Concreteness.PARTIAL, ReasoningAdapter.EXISTS).call(v1)
+                                ModalConstraint.of(Modality.MUST, Concreteness.PARTIAL, ReasoningAdapter.EXISTS_SYMBOL).call(v1)
                 ))).getDnf();
 
                 assertThat(actual, structurallyEqualTo(expected));
@@ -106,7 +106,7 @@ class DnfLifterTest {
                 var expected = Query.of("Expected", (builder, p1) -> builder.clause((v1) -> List.of(
                                 not(ModalConstraint.of(Modality.MAY, Concreteness.PARTIAL, friend).call(p1, v1)),
                                 ModalConstraint.of(Modality.MUST, Concreteness.PARTIAL, friend).call(v1, p1),
-                                ModalConstraint.of(Modality.MUST, Concreteness.PARTIAL, ReasoningAdapter.EXISTS).call(v1)
+                                ModalConstraint.of(Modality.MUST, Concreteness.PARTIAL, ReasoningAdapter.EXISTS_SYMBOL).call(v1)
                 ))).getDnf();
 
                 assertThat(actual, structurallyEqualTo(expected));
@@ -122,7 +122,7 @@ class DnfLifterTest {
 
                 var helper = Query.of("Helper", (builder, p1, p2) -> builder.clause(
                                 ModalConstraint.of(Modality.MUST, Concreteness.PARTIAL, friend).call(p1, p2),
-                                ModalConstraint.of(Modality.MUST, Concreteness.PARTIAL, ReasoningAdapter.EXISTS).call(p2)
+                                ModalConstraint.of(Modality.MUST, Concreteness.PARTIAL, ReasoningAdapter.EXISTS_SYMBOL).call(p2)
                 ));
                 var expected = Query.of("Expected", (builder, p1) -> builder.clause((v1) -> List.of(
                                 ModalConstraint.of(Modality.MAY, Concreteness.PARTIAL, person).call(p1),
@@ -142,7 +142,7 @@ class DnfLifterTest {
 
                 var helper = Query.of("Helper", (builder, p1, p2) -> builder.clause(
                                 friendMustView.call(p1, p2),
-                                ModalConstraint.of(Modality.MUST, Concreteness.PARTIAL, ReasoningAdapter.EXISTS).call(p2)
+                                ModalConstraint.of(Modality.MUST, Concreteness.PARTIAL, ReasoningAdapter.EXISTS_SYMBOL).call(p2)
                 ));
                 var expected = Query.of("Expected", (builder, p1) -> builder.clause((v1) -> List.of(
                                 ModalConstraint.of(Modality.MAY, Concreteness.PARTIAL, person).call(p1),
@@ -161,7 +161,7 @@ class DnfLifterTest {
 
                 var helper = Query.of("Helper", (builder, p1) -> builder.clause(
                                 ModalConstraint.of(Modality.MUST, Concreteness.PARTIAL, friend).call(p1, p1),
-                                ModalConstraint.of(Modality.MUST, Concreteness.PARTIAL, ReasoningAdapter.EXISTS).call(p1)
+                                ModalConstraint.of(Modality.MUST, Concreteness.PARTIAL, ReasoningAdapter.EXISTS_SYMBOL).call(p1)
                 ));
                 var expected = Query.of("Expected", (builder) -> builder.clause((v1) -> List.of(
                                 not(helper.call(v1))
@@ -191,7 +191,7 @@ class DnfLifterTest {
                         var p2 = builder.parameter("p2", ParameterDirection.OUT);
                         builder.clause(
                                         ModalConstraint.of(Modality.MUST, Concreteness.PARTIAL, called).call(p1, p2),
-                                        ModalConstraint.of(Modality.MUST, Concreteness.PARTIAL, ReasoningAdapter.EXISTS).call(p2)
+                                        ModalConstraint.of(Modality.MUST, Concreteness.PARTIAL, ReasoningAdapter.EXISTS_SYMBOL).call(p2)
                         );
                 });
                 var expected = Query.of("Expected", (builder, p1) -> builder.clause((v1) -> List.of(
@@ -212,7 +212,7 @@ class DnfLifterTest {
 
                 var helper = Query.of("Helper", (builder, p1, p2) -> builder.clause(
                                 ModalConstraint.of(Modality.MAY, Concreteness.PARTIAL, friend).call(p1, p2),
-                                ModalConstraint.of(Modality.MAY, Concreteness.PARTIAL, ReasoningAdapter.EXISTS).call(p2)
+                                ModalConstraint.of(Modality.MAY, Concreteness.PARTIAL, ReasoningAdapter.EXISTS_SYMBOL).call(p2)
                 ));
                 var helper2 = Query.of("Helper2", (builder, p1, p2) -> {
                         builder.clause(
@@ -241,7 +241,7 @@ class DnfLifterTest {
 
                 var endExistsHelper = Query.of("EndExistsHelper", (builder, p1, p2) -> builder.clause(
                                 friendMustView.call(p1, p2),
-                                ModalConstraint.of(Modality.MAY, Concreteness.PARTIAL, ReasoningAdapter.EXISTS).call(p2)
+                                ModalConstraint.of(Modality.MAY, Concreteness.PARTIAL, ReasoningAdapter.EXISTS_SYMBOL).call(p2)
                 ));
                 var transitiveHelper = Query.of("TransitiveHelper", (builder, p1, p2) -> {
                         builder.clause(
@@ -270,7 +270,7 @@ class DnfLifterTest {
 
                 var helper = Query.of("Helper", (builder, p1, p2) -> builder.clause(
                                 ModalConstraint.of(Modality.MAY, Concreteness.PARTIAL, friend).call(p1, p2),
-                                ModalConstraint.of(Modality.MAY, Concreteness.PARTIAL, ReasoningAdapter.EXISTS).call(p2)
+                                ModalConstraint.of(Modality.MAY, Concreteness.PARTIAL, ReasoningAdapter.EXISTS_SYMBOL).call(p2)
                 ));
                 var expected = Query.of("Expected", (builder, p1) -> builder.clause((v1) -> List.of(
                                 helper.callTransitive(p1, v1),
@@ -291,11 +291,11 @@ class DnfLifterTest {
 
                 var helper = Query.of("Helper", (builder, p1, p2) -> builder.clause(
                                 ModalConstraint.of(Modality.MAY, Concreteness.PARTIAL, friend).call(p1, p2),
-                                ModalConstraint.of(Modality.MAY, Concreteness.PARTIAL, ReasoningAdapter.EXISTS).call(p2)
+                                ModalConstraint.of(Modality.MAY, Concreteness.PARTIAL, ReasoningAdapter.EXISTS_SYMBOL).call(p2)
                 ));
                 var helper2 = Query.of("Helper2", (builder, p1, p2) -> builder.clause(
                                 friendMustView.call(p1, p2),
-                                ModalConstraint.of(Modality.MAY, Concreteness.PARTIAL, ReasoningAdapter.EXISTS).call(p2)
+                                ModalConstraint.of(Modality.MAY, Concreteness.PARTIAL, ReasoningAdapter.EXISTS_SYMBOL).call(p2)
                 ));
                 var expected = Query.of("Expected", (builder, p1) -> builder.clause((v1) -> List.of(
                                 helper.callTransitive(p1, v1),
@@ -316,7 +316,7 @@ class DnfLifterTest {
 
                 var expected = Query.of("Expected", (builder, p1, p2) -> builder.clause(
                                 ModalConstraint.of(Modality.MAY, Concreteness.PARTIAL, person).call(p1),
-                                ModalConstraint.of(Modality.MAY, Concreteness.PARTIAL, ReasoningAdapter.EQUALS).call(p2, p1)
+                                ModalConstraint.of(Modality.MAY, Concreteness.PARTIAL, ReasoningAdapter.EQUALS_SYMBOL).call(p2, p1)
                 )).getDnf();
 
                 assertThat(actual, structurallyEqualTo(expected));
@@ -332,7 +332,7 @@ class DnfLifterTest {
 
                 var expected = Query.of("Expected", (builder, p1, p2) -> builder.clause(
                                 ModalConstraint.of(Modality.MAY, Concreteness.PARTIAL, friend).call(p1, p2),
-                                not(ModalConstraint.of(Modality.MUST, Concreteness.PARTIAL, ReasoningAdapter.EQUALS).call(p1, p2))
+                                not(ModalConstraint.of(Modality.MUST, Concreteness.PARTIAL, ReasoningAdapter.EQUALS_SYMBOL).call(p1, p2))
                 )).getDnf();
 
                 assertThat(actual, structurallyEqualTo(expected));
@@ -349,7 +349,7 @@ class DnfLifterTest {
                 var expected = Query.of("Expected", (builder, p1) -> builder.clause((v1) -> List.of(
                                 v1.isConstant(0),
                                 ModalConstraint.of(Modality.MAY, Concreteness.PARTIAL, friend).call(v1, p1),
-                                ModalConstraint.of(Modality.MAY, Concreteness.PARTIAL, ReasoningAdapter.EXISTS).call(v1)
+                                ModalConstraint.of(Modality.MAY, Concreteness.PARTIAL, ReasoningAdapter.EXISTS_SYMBOL).call(v1)
                 ))).getDnf();
 
                 assertThat(actual, structurallyEqualTo(expected));
diff --git a/subprojects/store-reasoning/src/test/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeAnalyzerExampleHierarchyTest.java b/subprojects/store-reasoning/src/test/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeAnalyzerExampleHierarchyTest.java
index 05a476c6..b4ba16fc 100644
--- a/subprojects/store-reasoning/src/test/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeAnalyzerExampleHierarchyTest.java
+++ b/subprojects/store-reasoning/src/test/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeAnalyzerExampleHierarchyTest.java
@@ -5,6 +5,7 @@
  */
 package tools.refinery.store.reasoning.translator.typehierarchy;
 
+import org.hamcrest.Matchers;
 import org.junit.jupiter.api.BeforeEach;
 import org.junit.jupiter.api.Test;
 import tools.refinery.store.reasoning.representation.PartialRelation;
@@ -65,16 +66,16 @@ class TypeAnalyzerExampleHierarchyTest {
         @Test
         void inferredTypesTest() {
                 assertAll(
-                                () -> assertThat(sut.getUnknownType(), is(new InferredType(Set.of(), Set.of(c1, c2, c3, c4), null))),
-                                () -> assertThat(tester.getInferredType(a1), is(new InferredType(Set.of(a1, a4), Set.of(c1, c2), c1))),
-                                () -> assertThat(tester.getInferredType(a3), is(new InferredType(Set.of(a3), Set.of(c2, c3), c2))),
-                                () -> assertThat(tester.getInferredType(a4), is(new InferredType(Set.of(a4), Set.of(c1, c2, c4), c1))),
-                                () -> assertThat(tester.getInferredType(a5), is(new InferredType(Set.of(a5), Set.of(), null))),
-                                () -> assertThat(tester.getInferredType(c1), is(new InferredType(Set.of(a1, a4, c1), Set.of(c1), c1))),
+                                () -> assertThat(sut.getUnknownType(), Matchers.is(new InferredType(Set.of(), Set.of(c1, c2, c3, c4), null))),
+                                () -> assertThat(tester.getInferredType(a1), Matchers.is(new InferredType(Set.of(a1, a4), Set.of(c1, c2), c1))),
+                                () -> assertThat(tester.getInferredType(a3), Matchers.is(new InferredType(Set.of(a3), Set.of(c2, c3), c2))),
+                                () -> assertThat(tester.getInferredType(a4), Matchers.is(new InferredType(Set.of(a4), Set.of(c1, c2, c4), c1))),
+                                () -> assertThat(tester.getInferredType(a5), Matchers.is(new InferredType(Set.of(a5), Set.of(), null))),
+                                () -> assertThat(tester.getInferredType(c1), Matchers.is(new InferredType(Set.of(a1, a4, c1), Set.of(c1), c1))),
                                 () -> assertThat(tester.getInferredType(c2),
-                                                is(new InferredType(Set.of(a1, a3, a4, c2), Set.of(c2), c2))),
-                                () -> assertThat(tester.getInferredType(c3), is(new InferredType(Set.of(a3, c3), Set.of(c3), c3))),
-                                () -> assertThat(tester.getInferredType(c4), is(new InferredType(Set.of(a4, c4), Set.of(c4), c4)))
+                                                Matchers.is(new InferredType(Set.of(a1, a3, a4, c2), Set.of(c2), c2))),
+                                () -> assertThat(tester.getInferredType(c3), Matchers.is(new InferredType(Set.of(a3, c3), Set.of(c3), c3))),
+                                () -> assertThat(tester.getInferredType(c4), Matchers.is(new InferredType(Set.of(a4, c4), Set.of(c4), c4)))
                 );
         }
 
@@ -84,8 +85,8 @@ class TypeAnalyzerExampleHierarchyTest {
                 var a3Result = tester.getPreservedType(a3);
                 var expected = new InferredType(Set.of(a1, a3, a4, c2), Set.of(c2), c2);
                 assertAll(
-                                () -> assertThat(a1Result.merge(a3Result.asInferredType(), TruthValue.TRUE), is(expected)),
-                                () -> assertThat(a3Result.merge(a1Result.asInferredType(), TruthValue.TRUE), is(expected)),
+                                () -> assertThat(a1Result.merge(a3Result.asInferredType(), TruthValue.TRUE), Matchers.is(expected)),
+                                () -> assertThat(a3Result.merge(a1Result.asInferredType(), TruthValue.TRUE), Matchers.is(expected)),
                                 () -> assertThat(a1Result.merge(sut.getUnknownType(), TruthValue.TRUE), is(a1Result.asInferredType())),
                                 () -> assertThat(a3Result.merge(sut.getUnknownType(), TruthValue.TRUE), is(a3Result.asInferredType())),
                                 () -> assertThat(a1Result.merge(a1Result.asInferredType(), TruthValue.TRUE),
@@ -100,19 +101,19 @@ class TypeAnalyzerExampleHierarchyTest {
                 var a4Result = tester.getPreservedType(a4);
                 assertAll(
                                 () -> assertThat(a1Result.merge(a3Result.asInferredType(), TruthValue.FALSE),
-                                                is(new InferredType(Set.of(a3, c3), Set.of(c3), c3))),
+                                                Matchers.is(new InferredType(Set.of(a3, c3), Set.of(c3), c3))),
                                 () -> assertThat(a3Result.merge(a1Result.asInferredType(), TruthValue.FALSE),
-                                                is(new InferredType(Set.of(a1, a4, c1), Set.of(c1), c1))),
+                                                Matchers.is(new InferredType(Set.of(a1, a4, c1), Set.of(c1), c1))),
                                 () -> assertThat(a4Result.merge(a3Result.asInferredType(), TruthValue.FALSE),
-                                                is(new InferredType(Set.of(a3, c3), Set.of(c3), c3))),
+                                                Matchers.is(new InferredType(Set.of(a3, c3), Set.of(c3), c3))),
                                 () -> assertThat(a3Result.merge(a4Result.asInferredType(), TruthValue.FALSE),
-                                                is(new InferredType(Set.of(a4), Set.of(c1, c4), c1))),
+                                                Matchers.is(new InferredType(Set.of(a4), Set.of(c1, c4), c1))),
                                 () -> assertThat(a1Result.merge(sut.getUnknownType(), TruthValue.FALSE),
-                                                is(new InferredType(Set.of(), Set.of(c3, c4), null))),
+                                                Matchers.is(new InferredType(Set.of(), Set.of(c3, c4), null))),
                                 () -> assertThat(a3Result.merge(sut.getUnknownType(), TruthValue.FALSE),
-                                                is(new InferredType(Set.of(), Set.of(c1, c4), null))),
+                                                Matchers.is(new InferredType(Set.of(), Set.of(c1, c4), null))),
                                 () -> assertThat(a4Result.merge(sut.getUnknownType(), TruthValue.FALSE),
-                                                is(new InferredType(Set.of(), Set.of(c3), null)))
+                                                Matchers.is(new InferredType(Set.of(), Set.of(c3), null)))
                 );
         }
 
@@ -122,8 +123,8 @@ class TypeAnalyzerExampleHierarchyTest {
                 var a4Result = tester.getPreservedType(a4);
                 var expected = new InferredType(Set.of(c1, a1, a4), Set.of(), null);
                 assertAll(
-                                () -> assertThat(c1Result.merge(a4Result.asInferredType(), TruthValue.ERROR), is(expected)),
-                                () -> assertThat(a4Result.merge(c1Result.asInferredType(), TruthValue.ERROR), is(expected))
+                                () -> assertThat(c1Result.merge(a4Result.asInferredType(), TruthValue.ERROR), Matchers.is(expected)),
+                                () -> assertThat(a4Result.merge(c1Result.asInferredType(), TruthValue.ERROR), Matchers.is(expected))
                 );
         }
 
@@ -145,9 +146,9 @@ class TypeAnalyzerExampleHierarchyTest {
                 var c3Result = tester.getPreservedType(c3);
                 assertAll(
                                 () -> assertThat(a1Result.merge(c3Result.asInferredType(), TruthValue.TRUE),
-                                                is(new InferredType(Set.of(a1, a3, c3), Set.of(), null))),
+                                                Matchers.is(new InferredType(Set.of(a1, a3, c3), Set.of(), null))),
                                 () -> assertThat(c3Result.merge(a1Result.asInferredType(), TruthValue.TRUE),
-                                                is(new InferredType(Set.of(a1, a3, a4, c3), Set.of(), null)))
+                                                Matchers.is(new InferredType(Set.of(a1, a3, a4, c3), Set.of(), null)))
                 );
         }
 
@@ -158,13 +159,13 @@ class TypeAnalyzerExampleHierarchyTest {
                 var c1Result = tester.getPreservedType(c1);
                 assertAll(
                                 () -> assertThat(a4Result.merge(a1Result.asInferredType(), TruthValue.FALSE),
-                                                is(new InferredType(Set.of(a1, a4), Set.of(), null))),
+                                                Matchers.is(new InferredType(Set.of(a1, a4), Set.of(), null))),
                                 () -> assertThat(a1Result.merge(c1Result.asInferredType(), TruthValue.FALSE),
-                                                is(new InferredType(Set.of(a1, a4, c1), Set.of(), null))),
+                                                Matchers.is(new InferredType(Set.of(a1, a4, c1), Set.of(), null))),
                                 () -> assertThat(a4Result.merge(c1Result.asInferredType(), TruthValue.FALSE),
-                                                is(new InferredType(Set.of(a1, a4, c1), Set.of(), null))),
+                                                Matchers.is(new InferredType(Set.of(a1, a4, c1), Set.of(), null))),
                                 () -> assertThat(a1Result.merge(a1Result.asInferredType(), TruthValue.FALSE),
-                                                is(new InferredType(Set.of(a1, a4), Set.of(), null)))
+                                                Matchers.is(new InferredType(Set.of(a1, a4), Set.of(), null)))
                 );
         }
 
@@ -174,9 +175,9 @@ class TypeAnalyzerExampleHierarchyTest {
                 var a5Result = tester.getPreservedType(a5);
                 assertAll(
                                 () -> assertThat(c1Result.merge(a5Result.asInferredType(), TruthValue.TRUE),
-                                                is(new InferredType(Set.of(a1, a4, a5, c1), Set.of(), null))),
+                                                Matchers.is(new InferredType(Set.of(a1, a4, a5, c1), Set.of(), null))),
                                 () -> assertThat(a5Result.merge(c1Result.asInferredType(), TruthValue.TRUE),
-                                                is(new InferredType(Set.of(a1, a4, a5, c1), Set.of(), null)))
+                                                Matchers.is(new InferredType(Set.of(a1, a4, a5, c1), Set.of(), null)))
                 );
         }
 
@@ -198,9 +199,9 @@ class TypeAnalyzerExampleHierarchyTest {
                 var a5Result = tester.getPreservedType(a5);
                 assertAll(
                                 () -> assertThat(c1Result.merge(a5Result.asInferredType(), TruthValue.ERROR),
-                                                is(new InferredType(Set.of(a1, a4, a5, c1), Set.of(), null))),
+                                                Matchers.is(new InferredType(Set.of(a1, a4, a5, c1), Set.of(), null))),
                                 () -> assertThat(a5Result.merge(c1Result.asInferredType(), TruthValue.ERROR),
-                                                is(new InferredType(Set.of(a1, a4, a5, c1), Set.of(), null))),
+                                                Matchers.is(new InferredType(Set.of(a1, a4, a5, c1), Set.of(), null))),
                                 () -> assertThat(a5Result.merge(a5Result.asInferredType(), TruthValue.ERROR),
                                                 is(a5Result.asInferredType()))
                 );
diff --git a/subprojects/store-reasoning/src/test/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeAnalyzerTest.java b/subprojects/store-reasoning/src/test/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeAnalyzerTest.java
index d0ef9d57..315f9672 100644
--- a/subprojects/store-reasoning/src/test/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeAnalyzerTest.java
+++ b/subprojects/store-reasoning/src/test/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeAnalyzerTest.java
@@ -5,6 +5,7 @@
  */
 package tools.refinery.store.reasoning.translator.typehierarchy;
 
+import org.hamcrest.Matchers;
 import org.junit.jupiter.api.Test;
 import tools.refinery.store.reasoning.representation.PartialRelation;
 import tools.refinery.store.representation.TruthValue;
@@ -141,8 +142,8 @@ class TypeAnalyzerTest {
 
                 var expected = new InferredType(Set.of(c3), Set.of(c1, c2, c3), c3);
                 assertAll(
-                                () -> assertThat(tester.getInferredType(c3), is(expected)),
-                                () -> assertThat(c3Result.merge(sut.getUnknownType(), TruthValue.TRUE), is(expected))
+                                () -> assertThat(tester.getInferredType(c3), Matchers.is(expected)),
+                                () -> assertThat(c3Result.merge(sut.getUnknownType(), TruthValue.TRUE), Matchers.is(expected))
                 );
         }
 
@@ -166,7 +167,7 @@ class TypeAnalyzerTest {
                 var a1Result = tester.getPreservedType(a1);
 
                 assertThat(c1Result.merge(a1Result.asInferredType(), TruthValue.FALSE),
-                                is(new InferredType(Set.of(a1), Set.of(c2, c3, c4), c2)));
+                                Matchers.is(new InferredType(Set.of(a1), Set.of(c2, c3, c4), c2)));
         }
 
         @Test
@@ -189,7 +190,7 @@ class TypeAnalyzerTest {
                 var a1Result = tester.getPreservedType(a1);
 
                 assertThat(c1Result.merge(a1Result.asInferredType(), TruthValue.FALSE),
-                                is(new InferredType(Set.of(a1), Set.of(c2, c3, c4), c3)));
+                                Matchers.is(new InferredType(Set.of(a1), Set.of(c2, c3, c4), c3)));
         }
 
         @Test
diff --git a/subprojects/store/src/main/java/tools/refinery/store/map/Cursors.java b/subprojects/store/src/main/java/tools/refinery/store/map/Cursors.java
index 1080a248..5e69e7af 100644
--- a/subprojects/store/src/main/java/tools/refinery/store/map/Cursors.java
+++ b/subprojects/store/src/main/java/tools/refinery/store/map/Cursors.java
@@ -5,6 +5,9 @@
  */
 package tools.refinery.store.map;
 
+import java.util.Iterator;
+import java.util.Map;
+
 public final class Cursors {
     private Cursors() {
         throw new IllegalStateException("This is a static utility class and should not be instantiated directly");
@@ -18,6 +21,14 @@ public final class Cursors {
                 return new Singleton<>(key, value);
         }
 
+        public static <K, V> Cursor<K, V> of(Iterator<Map.Entry<K, V>> iterator) {
+                return new IteratorBasedCursor<>(iterator);
+        }
+
+        public static <K, V> Cursor<K, V> of(Map<K, V> map) {
+                return of(map.entrySet().iterator());
+        }
+
     private static class Empty<K, V> implements Cursor<K, V> {
         private boolean terminated = false;
 
diff --git a/subprojects/store/src/main/java/tools/refinery/store/map/IteratorBasedCursor.java b/subprojects/store/src/main/java/tools/refinery/store/map/IteratorBasedCursor.java
new file mode 100644
index 00000000..0ed9b730
--- /dev/null
+++ b/subprojects/store/src/main/java/tools/refinery/store/map/IteratorBasedCursor.java
@@ -0,0 +1,44 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.map;
+
+import java.util.Iterator;
+import java.util.Map;
+
+public class IteratorBasedCursor<K, V> implements Cursor<K, V> {
+        private final Iterator<Map.Entry<K, V>> iterator;
+        private Map.Entry<K, V> entry;
+        private boolean terminated;
+
+        public IteratorBasedCursor(Iterator<Map.Entry<K, V>> iterator) {
+                this.iterator = iterator;
+        }
+
+        @Override
+        public K getKey() {
+                return entry.getKey();
+        }
+
+        @Override
+        public V getValue() {
+                return entry.getValue();
+        }
+
+        @Override
+        public boolean isTerminated() {
+                return terminated;
+        }
+
+        @Override
+        public boolean move() {
+                if (!terminated && iterator.hasNext()) {
+                        entry = iterator.next();
+                        return true;
+                }
+                terminated = true;
+                return false;
+        }
+}
diff --git a/subprojects/store/src/main/java/tools/refinery/store/model/ModelStoreBuilder.java b/subprojects/store/src/main/java/tools/refinery/store/model/ModelStoreBuilder.java
index 3a4024b5..8f652762 100644
--- a/subprojects/store/src/main/java/tools/refinery/store/model/ModelStoreBuilder.java
+++ b/subprojects/store/src/main/java/tools/refinery/store/model/ModelStoreBuilder.java
@@ -29,7 +29,9 @@ public interface ModelStoreBuilder {
 
         <T> ModelStoreBuilder symbol(Symbol<T> symbol);
 
-        <T extends ModelAdapterBuilder> ModelStoreBuilder with(T adapterBuilder);
+        ModelStoreBuilder with(ModelAdapterBuilder adapterBuilder);
+
+        ModelStoreBuilder with(ModelStoreConfiguration configuration);
 
         <T extends ModelAdapterBuilder> Optional<T> tryGetAdapter(Class<? extends T> adapterType);
 
diff --git a/subprojects/store/src/main/java/tools/refinery/store/model/ModelStoreConfiguration.java b/subprojects/store/src/main/java/tools/refinery/store/model/ModelStoreConfiguration.java
new file mode 100644
index 00000000..e94af5f8
--- /dev/null
+++ b/subprojects/store/src/main/java/tools/refinery/store/model/ModelStoreConfiguration.java
@@ -0,0 +1,11 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.model;
+
+@FunctionalInterface
+public interface ModelStoreConfiguration {
+        void apply(ModelStoreBuilder storeBuilder);
+}
diff --git a/subprojects/store/src/main/java/tools/refinery/store/model/internal/BaseIndexer.java b/subprojects/store/src/main/java/tools/refinery/store/model/internal/BaseIndexer.java
index d9245c1d..3d7f59d7 100644
--- a/subprojects/store/src/main/java/tools/refinery/store/model/internal/BaseIndexer.java
+++ b/subprojects/store/src/main/java/tools/refinery/store/model/internal/BaseIndexer.java
@@ -9,14 +9,9 @@ import org.eclipse.collections.api.factory.Maps;
 import org.eclipse.collections.api.factory.primitive.IntObjectMaps;
 import org.eclipse.collections.api.map.MutableMap;
 import org.eclipse.collections.api.map.primitive.MutableIntObjectMap;
-import tools.refinery.store.map.AnyVersionedMap;
-import tools.refinery.store.map.Cursor;
-import tools.refinery.store.map.Cursors;
-import tools.refinery.store.map.VersionedMap;
+import tools.refinery.store.map.*;
 import tools.refinery.store.tuple.Tuple;
 
-import java.util.Iterator;
-import java.util.Map;
 import java.util.Set;
 
 class BaseIndexer<T> {
@@ -91,40 +86,12 @@ class BaseIndexer<T> {
                 return new IndexCursor<>(adjacentTuples, versionedMap);
         }
 
-        private static class IndexCursor<T> implements Cursor<Tuple, T> {
+        private static class IndexCursor<T> extends IteratorBasedCursor<Tuple, T> {
                 private final Set<AnyVersionedMap> dependingMaps;
-                private final Iterator<Map.Entry<Tuple, T>> iterator;
-                private Map.Entry<Tuple, T> entry;
-                private boolean terminated;
 
-                public IndexCursor(MutableMap<Tuple, T> adjacentTuples, VersionedMap<Tuple, T> versionedMap) {
+                public IndexCursor(MutableMap<Tuple, T> map, VersionedMap<Tuple, T> versionedMap) {
+                        super(map.entrySet().iterator());
                         dependingMaps = versionedMap == null ? Set.of() : Set.of(versionedMap);
-                        iterator = adjacentTuples.entrySet().iterator();
-                }
-
-                @Override
-                public Tuple getKey() {
-                        return entry.getKey();
-                }
-
-                @Override
-                public T getValue() {
-                        return entry.getValue();
-                }
-
-                @Override
-                public boolean isTerminated() {
-                        return terminated;
-                }
-
-                @Override
-                public boolean move() {
-                        if (!terminated && iterator.hasNext()) {
-                                entry = iterator.next();
-                                return true;
-                        }
-                        terminated = true;
-                        return false;
                 }
 
                 @Override
diff --git a/subprojects/store/src/main/java/tools/refinery/store/model/internal/ModelStoreBuilderImpl.java b/subprojects/store/src/main/java/tools/refinery/store/model/internal/ModelStoreBuilderImpl.java
index aafbe130..5c688178 100644
--- a/subprojects/store/src/main/java/tools/refinery/store/model/internal/ModelStoreBuilderImpl.java
+++ b/subprojects/store/src/main/java/tools/refinery/store/model/internal/ModelStoreBuilderImpl.java
@@ -11,6 +11,7 @@ import tools.refinery.store.map.VersionedMapStore;
 import tools.refinery.store.map.VersionedMapStoreImpl;
 import tools.refinery.store.model.ModelStore;
 import tools.refinery.store.model.ModelStoreBuilder;
+import tools.refinery.store.model.ModelStoreConfiguration;
 import tools.refinery.store.model.TupleHashProvider;
 import tools.refinery.store.representation.AnySymbol;
 import tools.refinery.store.representation.Symbol;
@@ -26,7 +27,8 @@ public class ModelStoreBuilderImpl implements ModelStoreBuilder {
         @Override
         public <T> ModelStoreBuilder symbol(Symbol<T> symbol) {
                 if (!allSymbols.add(symbol)) {
-                        throw new IllegalArgumentException("Symbol %s already added".formatted(symbol));
+                        // No need to add symbol twice.
+                        return this;
                 }
                 var equivalenceClass = new SymbolEquivalenceClass<>(symbol);
                 var symbolsInEquivalenceClass = equivalenceClasses.computeIfAbsent(equivalenceClass,
@@ -36,7 +38,7 @@ public class ModelStoreBuilderImpl implements ModelStoreBuilder {
         }
 
         @Override
-        public <T extends ModelAdapterBuilder> ModelStoreBuilder with(T adapterBuilder) {
+        public ModelStoreBuilder with(ModelAdapterBuilder adapterBuilder) {
                 for (var existingAdapter : adapters) {
                         if (existingAdapter.getClass().equals(adapterBuilder.getClass())) {
                                 throw new IllegalArgumentException("%s adapter was already configured for store builder"
@@ -48,6 +50,12 @@ public class ModelStoreBuilderImpl implements ModelStoreBuilder {
         }
 
         @Override
+        public ModelStoreBuilder with(ModelStoreConfiguration configuration) {
+                configuration.apply(this);
+                return this;
+        }
+
+        @Override
         public <T extends ModelAdapterBuilder> Optional<T> tryGetAdapter(Class<? extends T> adapterType) {
                 return AdapterUtils.tryGetAdapter(adapters, adapterType);
         }
@@ -59,13 +67,14 @@ public class ModelStoreBuilderImpl implements ModelStoreBuilder {
 
         @Override
         public ModelStore build() {
+                // First configure adapters and let them register any symbols we don't know about yet.
+                for (int i = adapters.size() - 1; i >= 0; i--) {
+                        adapters.get(i).configure(this);
+                }
                 var stores = new HashMap<AnySymbol, VersionedMapStore<Tuple, ?>>(allSymbols.size());
                 for (var entry : equivalenceClasses.entrySet()) {
                         createStores(stores, entry.getKey(), entry.getValue());
                 }
-                for (int i = adapters.size() - 1; i >= 0; i--) {
-                        adapters.get(i).configure(this);
-                }
                 var modelStore = new ModelStoreImpl(stores, adapters.size());
                 for (var adapterBuilder : adapters) {
                         var storeAdapter = adapterBuilder.build(modelStore);
diff --git a/subprojects/store/src/main/java/tools/refinery/store/representation/AbstractDomain.java b/subprojects/store/src/main/java/tools/refinery/store/representation/AbstractDomain.java
index 52c740e8..dfdb43bd 100644
--- a/subprojects/store/src/main/java/tools/refinery/store/representation/AbstractDomain.java
+++ b/subprojects/store/src/main/java/tools/refinery/store/representation/AbstractDomain.java
@@ -5,6 +5,7 @@
  */
 package tools.refinery.store.representation;
 
+import java.util.Objects;
 import java.util.Optional;
 
 public non-sealed interface AbstractDomain<A, C> extends AnyAbstractDomain {
@@ -22,7 +23,9 @@ public non-sealed interface AbstractDomain<A, C> extends AnyAbstractDomain {
                 return toConcrete(abstractValue).isPresent();
         }
 
-        boolean isRefinement(A originalValue, A refinedValue);
+        default boolean isRefinement(A originalValue, A refinedValue) {
+                return Objects.equals(commonRefinement(originalValue, refinedValue), refinedValue);
+        }
 
         A commonRefinement(A leftValue, A rightValue);
 
diff --git a/subprojects/store/src/main/java/tools/refinery/store/representation/TruthValue.java b/subprojects/store/src/main/java/tools/refinery/store/representation/TruthValue.java
index 40baf9a5..f81ee9a4 100644
--- a/subprojects/store/src/main/java/tools/refinery/store/representation/TruthValue.java
+++ b/subprojects/store/src/main/java/tools/refinery/store/representation/TruthValue.java
@@ -36,6 +36,10 @@ public enum TruthValue {
                 return this != UNKNOWN;
         }
 
+        public boolean isConcrete() {
+                return this == TRUE || this == FALSE;
+        }
+
         public boolean must() {
                 return this == TRUE || this == ERROR;
         }
@@ -55,9 +59,18 @@ public enum TruthValue {
         public TruthValue merge(TruthValue other) {
                 return switch (this) {
                         case TRUE -> other == UNKNOWN || other == TRUE ? TRUE : ERROR;
-                        case FALSE -> other == TruthValue.UNKNOWN || other == TruthValue.FALSE ? FALSE : ERROR;
+                        case FALSE -> other == UNKNOWN || other == FALSE ? FALSE : ERROR;
                         case UNKNOWN -> other;
-                        default -> ERROR;
+                        case ERROR -> ERROR;
+                };
+        }
+
+        public TruthValue join(TruthValue other) {
+                return switch (this) {
+                        case TRUE -> other == ERROR || other == TRUE ? TRUE : UNKNOWN;
+                        case FALSE -> other == ERROR || other == FALSE ? FALSE : UNKNOWN;
+                        case UNKNOWN -> UNKNOWN;
+                        case ERROR -> other;
                 };
         }
 }
diff --git a/subprojects/store/src/main/java/tools/refinery/store/representation/TruthValueDomain.java b/subprojects/store/src/main/java/tools/refinery/store/representation/TruthValueDomain.java
index 89f8dd19..61696dca 100644
--- a/subprojects/store/src/main/java/tools/refinery/store/representation/TruthValueDomain.java
+++ b/subprojects/store/src/main/java/tools/refinery/store/representation/TruthValueDomain.java
@@ -7,6 +7,8 @@ package tools.refinery.store.representation;
 
 import java.util.Optional;
 
+// Singleton pattern, because there is only one domain for truth values.
+@SuppressWarnings("squid:S6548")
 public final class TruthValueDomain implements AbstractDomain<TruthValue, Boolean> {
         public static final TruthValueDomain INSTANCE = new TruthValueDomain();
 
@@ -15,51 +17,50 @@ public final class TruthValueDomain implements AbstractDomain<TruthValue, Boolea
 
         @Override
         public Class<TruthValue> abstractType() {
-                return null;
+                return TruthValue.class;
         }
 
         @Override
         public Class<Boolean> concreteType() {
-                return null;
+                return Boolean.class;
         }
 
         @Override
         public TruthValue toAbstract(Boolean concreteValue) {
-                return null;
+                return TruthValue.toTruthValue(concreteValue);
         }
 
         @Override
         public Optional<Boolean> toConcrete(TruthValue abstractValue) {
-                return Optional.empty();
+                return switch (abstractValue) {
+                        case TRUE -> Optional.of(true);
+                        case FALSE -> Optional.of(false);
+                        default -> Optional.empty();
+                };
         }
 
         @Override
         public boolean isConcrete(TruthValue abstractValue) {
-                return AbstractDomain.super.isConcrete(abstractValue);
-        }
-
-        @Override
-        public boolean isRefinement(TruthValue originalValue, TruthValue refinedValue) {
-                return false;
+                return abstractValue.isConcrete();
         }
 
         @Override
         public TruthValue commonRefinement(TruthValue leftValue, TruthValue rightValue) {
-                return null;
+                return leftValue.merge(rightValue);
         }
 
         @Override
         public TruthValue commonAncestor(TruthValue leftValue, TruthValue rightValue) {
-                return null;
+                return leftValue.join(rightValue);
         }
 
         @Override
         public TruthValue unknown() {
-                return null;
+                return TruthValue.UNKNOWN;
         }
 
         @Override
         public boolean isError(TruthValue abstractValue) {
-                return false;
+                return !abstractValue.isConsistent();
         }
 }
diff --git a/subprojects/store/src/main/java/tools/refinery/store/tuple/Tuple.java b/subprojects/store/src/main/java/tools/refinery/store/tuple/Tuple.java
index aae7b344..e9761763 100644
--- a/subprojects/store/src/main/java/tools/refinery/store/tuple/Tuple.java
+++ b/subprojects/store/src/main/java/tools/refinery/store/tuple/Tuple.java
@@ -12,6 +12,8 @@ public sealed interface Tuple extends Comparable<Tuple> permits Tuple0, Tuple1,
 
         int get(int element);
 
+        Tuple set(int element, int value);
+
         @Override
         default int compareTo(@NotNull Tuple other) {
                 int size = getSize();
diff --git a/subprojects/store/src/main/java/tools/refinery/store/tuple/Tuple0.java b/subprojects/store/src/main/java/tools/refinery/store/tuple/Tuple0.java
index a9aa9bf2..5f525798 100644
--- a/subprojects/store/src/main/java/tools/refinery/store/tuple/Tuple0.java
+++ b/subprojects/store/src/main/java/tools/refinery/store/tuple/Tuple0.java
@@ -29,6 +29,11 @@ public final class Tuple0 implements Tuple {
         }
 
         @Override
+        public Tuple set(int element, int value) {
+                throw new IndexOutOfBoundsException(element);
+        }
+
+        @Override
         public String toString() {
                 return TUPLE_BEGIN + TUPLE_END;
         }
diff --git a/subprojects/store/src/main/java/tools/refinery/store/tuple/Tuple1.java b/subprojects/store/src/main/java/tools/refinery/store/tuple/Tuple1.java
index 388ee3a9..fb9497d2 100644
--- a/subprojects/store/src/main/java/tools/refinery/store/tuple/Tuple1.java
+++ b/subprojects/store/src/main/java/tools/refinery/store/tuple/Tuple1.java
@@ -38,6 +38,14 @@ public final class Tuple1 implements Tuple {
         }
 
         @Override
+        public Tuple set(int element, int value) {
+                if (element == 0) {
+                        return Tuple.of(value);
+                }
+                throw new IndexOutOfBoundsException(element);
+        }
+
+        @Override
         public String toString() {
                 return TUPLE_BEGIN + value0 + TUPLE_END;
         }
diff --git a/subprojects/store/src/main/java/tools/refinery/store/tuple/Tuple2.java b/subprojects/store/src/main/java/tools/refinery/store/tuple/Tuple2.java
index 6d886fd3..2213df97 100644
--- a/subprojects/store/src/main/java/tools/refinery/store/tuple/Tuple2.java
+++ b/subprojects/store/src/main/java/tools/refinery/store/tuple/Tuple2.java
@@ -25,6 +25,15 @@ public record Tuple2(int value0, int value1) implements Tuple {
         }
 
         @Override
+        public Tuple set(int element, int value) {
+                return switch (element) {
+                        case 0 -> Tuple.of(value, value1);
+                        case 1 -> Tuple.of(value0, value);
+                        default -> throw new ArrayIndexOutOfBoundsException(element);
+                };
+        }
+
+        @Override
         public String toString() {
                 return TUPLE_BEGIN + value0 + TUPLE_SEPARATOR + value1 + TUPLE_END;
         }
diff --git a/subprojects/store/src/main/java/tools/refinery/store/tuple/Tuple3.java b/subprojects/store/src/main/java/tools/refinery/store/tuple/Tuple3.java
index 734e45c2..417770e8 100644
--- a/subprojects/store/src/main/java/tools/refinery/store/tuple/Tuple3.java
+++ b/subprojects/store/src/main/java/tools/refinery/store/tuple/Tuple3.java
@@ -26,6 +26,16 @@ public record Tuple3(int value0, int value1, int value2) implements Tuple {
         }
 
         @Override
+        public Tuple set(int element, int value) {
+                return switch (element) {
+                        case 0 -> Tuple.of(value, value1, value2);
+                        case 1 -> Tuple.of(value0, value, value2);
+                        case 2 -> Tuple.of(value0, value1, value);
+                        default -> throw new ArrayIndexOutOfBoundsException(element);
+                };
+        }
+
+        @Override
         public String toString() {
                 return TUPLE_BEGIN + value0 + TUPLE_SEPARATOR + value1 + TUPLE_SEPARATOR + value2 + TUPLE_END;
         }
diff --git a/subprojects/store/src/main/java/tools/refinery/store/tuple/Tuple4.java b/subprojects/store/src/main/java/tools/refinery/store/tuple/Tuple4.java
index e1b93e7b..c4915198 100644
--- a/subprojects/store/src/main/java/tools/refinery/store/tuple/Tuple4.java
+++ b/subprojects/store/src/main/java/tools/refinery/store/tuple/Tuple4.java
@@ -27,6 +27,17 @@ public record Tuple4(int value0, int value1, int value2, int value3) implements
         }
 
         @Override
+        public Tuple set(int element, int value) {
+                return switch (element) {
+                        case 0 -> Tuple.of(value, value1, value2, value3);
+                        case 1 -> Tuple.of(value0, value, value2, value3);
+                        case 2 -> Tuple.of(value0, value1, value, value3);
+                        case 3 -> Tuple.of(value0, value1, value2, value);
+                        default -> throw new ArrayIndexOutOfBoundsException(element);
+                };
+        }
+
+        @Override
         public String toString() {
                 return TUPLE_BEGIN + value0 + TUPLE_SEPARATOR + value1 + TUPLE_SEPARATOR + value2 + TUPLE_SEPARATOR + value3 +
                                 TUPLE_END;
diff --git a/subprojects/store/src/main/java/tools/refinery/store/tuple/TupleN.java b/subprojects/store/src/main/java/tools/refinery/store/tuple/TupleN.java
index b66af491..b42b4b6a 100644
--- a/subprojects/store/src/main/java/tools/refinery/store/tuple/TupleN.java
+++ b/subprojects/store/src/main/java/tools/refinery/store/tuple/TupleN.java
@@ -32,6 +32,16 @@ public final class TupleN implements Tuple {
         }
 
         @Override
+        public Tuple set(int element, int value) {
+                int size = getSize();
+                var newValues = new int[size];
+                for (int i = 0; i < size; i++) {
+                        newValues[i] = element == i ? value : values[i];
+                }
+                return Tuple.of(newValues);
+        }
+
+        @Override
         public String toString() {
                 var valuesString = Arrays.stream(values)
                                 .mapToObj(Integer::toString)