refactor: split query and partial from store

Allows more complicated dependency hiearchies (e.g., use
store-query-viatra for testing store-partial) and better separation of
test fixtures.

83 files changed, 1095 insertions, 246 deletions

diff --git a/settings.gradle b/settings.gradle
index 3149380d..94a3c2e6 100644
--- a/settings.gradle
+++ b/settings.gradle
@@ -7,6 +7,8 @@ include 'language-model'
 include 'language-semantics'
 include 'language-web'
 include 'store'
+include 'store-partial'
+include 'store-query'
 include 'store-query-viatra'
 
 for (project in rootProject.children) {
diff --git a/subprojects/store-partial/build.gradle b/subprojects/store-partial/build.gradle
new file mode 100644
index 00000000..cb440d9f
--- /dev/null
+++ b/subprojects/store-partial/build.gradle
@@ -0,0 +1,7 @@
+plugins {
+        id 'refinery-java-library'
+}
+
+dependencies {
+        api project(':refinery-store-query')
+}
diff --git a/subprojects/store-partial/src/main/java/tools/refinery/store/partial/AnyPartialSymbolInterpretation.java b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/AnyPartialSymbolInterpretation.java
new file mode 100644
index 00000000..b6b1f2be
--- /dev/null
+++ b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/AnyPartialSymbolInterpretation.java
@@ -0,0 +1,13 @@
+package tools.refinery.store.partial;
+
+import tools.refinery.store.partial.representation.AnyPartialSymbol;
+
+public sealed interface AnyPartialSymbolInterpretation permits PartialSymbolInterpretation {
+        PartialInterpretationAdapter getAdapter();
+
+        AnyPartialSymbol getPartialSymbol();
+
+        int countUnfinished();
+
+        int countErrors();
+}
diff --git a/subprojects/store-partial/src/main/java/tools/refinery/store/partial/MergeResult.java b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/MergeResult.java
new file mode 100644
index 00000000..82414d87
--- /dev/null
+++ b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/MergeResult.java
@@ -0,0 +1,15 @@
+package tools.refinery.store.partial;
+
+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/src/main/java/tools/refinery/store/partial/PartialInterpretation.java b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/PartialInterpretation.java
index 331fa294..d76f8728 100644
--- a/subprojects/store/src/main/java/tools/refinery/store/partial/PartialInterpretation.java
+++ b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/PartialInterpretation.java
@@ -1,13 +1,18 @@
 package tools.refinery.store.partial;
 
+import tools.refinery.store.partial.internal.PartialInterpretationBuilderImpl;
 import tools.refinery.store.adapter.ModelAdapterBuilderFactory;
 import tools.refinery.store.model.ModelStoreBuilder;
-import tools.refinery.store.partial.internal.PartialInterpretationBuilderImpl;
+import tools.refinery.store.partial.representation.PartialRelation;
 
 public final class PartialInterpretation extends ModelAdapterBuilderFactory<PartialInterpretationAdapter,
                 PartialInterpretationStoreAdapter, PartialInterpretationBuilder> {
         public static final PartialInterpretation ADAPTER = new PartialInterpretation();
 
+        public static final PartialRelation EXISTS = new PartialRelation("exists", 1);
+
+        public static final PartialRelation EQUALS = new PartialRelation("equals", 1);
+
         private PartialInterpretation() {
                 super(PartialInterpretationAdapter.class, PartialInterpretationStoreAdapter.class, PartialInterpretationBuilder.class);
         }
diff --git a/subprojects/store-partial/src/main/java/tools/refinery/store/partial/PartialInterpretationAdapter.java b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/PartialInterpretationAdapter.java
new file mode 100644
index 00000000..b811ae7a
--- /dev/null
+++ b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/PartialInterpretationAdapter.java
@@ -0,0 +1,20 @@
+package tools.refinery.store.partial;
+
+import tools.refinery.store.adapter.ModelAdapter;
+import tools.refinery.store.partial.representation.AnyPartialSymbol;
+import tools.refinery.store.partial.representation.PartialSymbol;
+import tools.refinery.store.query.Dnf;
+import tools.refinery.store.query.ResultSet;
+
+public interface PartialInterpretationAdapter extends ModelAdapter {
+        @Override
+        PartialInterpretationStoreAdapter getStoreAdapter();
+
+        default AnyPartialSymbolInterpretation getPartialInterpretation(AnyPartialSymbol partialSymbol) {
+                return getPartialInterpretation((PartialSymbol<?, ?>) partialSymbol);
+        }
+
+        <A, C> PartialSymbolInterpretation<A, C> getPartialInterpretation(PartialSymbol<A, C> partialSymbol);
+
+        ResultSet getLiftedResultSet(Dnf query);
+}
diff --git a/subprojects/store-partial/src/main/java/tools/refinery/store/partial/PartialInterpretationBuilder.java b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/PartialInterpretationBuilder.java
new file mode 100644
index 00000000..db042466
--- /dev/null
+++ b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/PartialInterpretationBuilder.java
@@ -0,0 +1,28 @@
+package tools.refinery.store.partial;
+
+import tools.refinery.store.adapter.ModelAdapterBuilder;
+import tools.refinery.store.model.ModelStore;
+import tools.refinery.store.query.Dnf;
+import tools.refinery.store.partial.literal.Modality;
+
+import java.util.Collection;
+import java.util.List;
+
+@SuppressWarnings("UnusedReturnValue")
+public interface PartialInterpretationBuilder extends ModelAdapterBuilder {
+        default PartialInterpretationBuilder liftedQueries(Dnf... liftedQueries) {
+                return liftedQueries(List.of(liftedQueries));
+        }
+
+        default PartialInterpretationBuilder liftedQueries(Collection<Dnf> liftedQueries) {
+                liftedQueries.forEach(this::liftedQuery);
+                return this;
+        }
+
+        PartialInterpretationBuilder liftedQuery(Dnf liftedQuery);
+
+        Dnf lift(Modality modality, Dnf query);
+
+        @Override
+        PartialInterpretationStoreAdapter createStoreAdapter(ModelStore store);
+}
diff --git a/subprojects/store/src/main/java/tools/refinery/store/partial/PartialInterpretationStoreAdapter.java b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/PartialInterpretationStoreAdapter.java
index d4eb770d..a1813671 100644
--- a/subprojects/store/src/main/java/tools/refinery/store/partial/PartialInterpretationStoreAdapter.java
+++ b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/PartialInterpretationStoreAdapter.java
@@ -2,8 +2,16 @@ package tools.refinery.store.partial;
 
 import tools.refinery.store.adapter.ModelStoreAdapter;
 import tools.refinery.store.model.Model;
+import tools.refinery.store.partial.representation.AnyPartialSymbol;
+import tools.refinery.store.query.Dnf;
+
+import java.util.Collection;
 
 public interface PartialInterpretationStoreAdapter extends ModelStoreAdapter {
+        Collection<AnyPartialSymbol> getPartialSymbols();
+
+        Collection<Dnf> getLiftedQueries();
+
         @Override
         PartialInterpretationAdapter createModelAdapter(Model model);
 }
diff --git a/subprojects/store-partial/src/main/java/tools/refinery/store/partial/PartialSymbolInterpretation.java b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/PartialSymbolInterpretation.java
new file mode 100644
index 00000000..fa9e9216
--- /dev/null
+++ b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/PartialSymbolInterpretation.java
@@ -0,0 +1,22 @@
+package tools.refinery.store.partial;
+
+import tools.refinery.store.partial.representation.PartialSymbol;
+import tools.refinery.store.map.Cursor;
+import tools.refinery.store.tuple.Tuple;
+
+public non-sealed interface PartialSymbolInterpretation<A, C> extends AnyPartialSymbolInterpretation {
+        @Override
+        PartialSymbol<A, C> getPartialSymbol();
+
+        A get(Tuple key);
+
+        Cursor<Tuple, A> getAll();
+
+        Cursor<Tuple, A> getAllErrors();
+
+        MergeResult merge(Tuple key, A value);
+
+        C getConcrete(Tuple key);
+
+        Cursor<Tuple, C> getAllConcrete();
+}
diff --git a/subprojects/store/src/main/java/tools/refinery/store/partial/internal/PartialInterpretationAdapterImpl.java b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/internal/PartialInterpretationAdapterImpl.java
index 4b3977c0..c482d8a2 100644
--- a/subprojects/store/src/main/java/tools/refinery/store/partial/internal/PartialInterpretationAdapterImpl.java
+++ b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/internal/PartialInterpretationAdapterImpl.java
@@ -2,6 +2,10 @@ package tools.refinery.store.partial.internal;
 
 import tools.refinery.store.model.Model;
 import tools.refinery.store.partial.PartialInterpretationAdapter;
+import tools.refinery.store.partial.PartialSymbolInterpretation;
+import tools.refinery.store.partial.representation.PartialSymbol;
+import tools.refinery.store.query.Dnf;
+import tools.refinery.store.query.ResultSet;
 
 public class PartialInterpretationAdapterImpl implements PartialInterpretationAdapter {
         private final Model model;
@@ -21,4 +25,14 @@ public class PartialInterpretationAdapterImpl implements PartialInterpretationAd
         public PartialInterpretationStoreAdapterImpl getStoreAdapter() {
                 return storeAdapter;
         }
+
+        @Override
+        public <A, C> PartialSymbolInterpretation<A, C> getPartialInterpretation(PartialSymbol<A, C> partialSymbol) {
+                return null;
+        }
+
+        @Override
+        public ResultSet getLiftedResultSet(Dnf query) {
+                return null;
+        }
 }
diff --git a/subprojects/store/src/main/java/tools/refinery/store/partial/internal/PartialInterpretationBuilderImpl.java b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/internal/PartialInterpretationBuilderImpl.java
index 4609dc32..5853aeaf 100644
--- a/subprojects/store/src/main/java/tools/refinery/store/partial/internal/PartialInterpretationBuilderImpl.java
+++ b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/internal/PartialInterpretationBuilderImpl.java
@@ -4,6 +4,8 @@ import tools.refinery.store.adapter.AbstractModelAdapterBuilder;
 import tools.refinery.store.model.ModelStore;
 import tools.refinery.store.model.ModelStoreBuilder;
 import tools.refinery.store.partial.PartialInterpretationBuilder;
+import tools.refinery.store.partial.literal.Modality;
+import tools.refinery.store.query.Dnf;
 
 public class PartialInterpretationBuilderImpl extends AbstractModelAdapterBuilder implements PartialInterpretationBuilder {
         public PartialInterpretationBuilderImpl(ModelStoreBuilder storeBuilder) {
@@ -11,6 +13,16 @@ public class PartialInterpretationBuilderImpl extends AbstractModelAdapterBuilde
         }
 
         @Override
+        public PartialInterpretationBuilder liftedQuery(Dnf liftedQuery) {
+                return null;
+        }
+
+        @Override
+        public Dnf lift(Modality modality, Dnf query) {
+                return null;
+        }
+
+        @Override
         public PartialInterpretationStoreAdapterImpl createStoreAdapter(ModelStore store) {
                 return null;
         }
diff --git a/subprojects/store/src/main/java/tools/refinery/store/partial/internal/PartialInterpretationStoreAdapterImpl.java b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/internal/PartialInterpretationStoreAdapterImpl.java
index 970b802b..0486af6e 100644
--- a/subprojects/store/src/main/java/tools/refinery/store/partial/internal/PartialInterpretationStoreAdapterImpl.java
+++ b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/internal/PartialInterpretationStoreAdapterImpl.java
@@ -1,8 +1,12 @@
 package tools.refinery.store.partial.internal;
 
+import tools.refinery.store.partial.PartialInterpretationStoreAdapter;
 import tools.refinery.store.model.Model;
 import tools.refinery.store.model.ModelStore;
-import tools.refinery.store.partial.PartialInterpretationStoreAdapter;
+import tools.refinery.store.partial.representation.AnyPartialSymbol;
+import tools.refinery.store.query.Dnf;
+
+import java.util.Collection;
 
 public class PartialInterpretationStoreAdapterImpl implements PartialInterpretationStoreAdapter {
         private final ModelStore store;
@@ -17,6 +21,16 @@ public class PartialInterpretationStoreAdapterImpl implements PartialInterpretat
         }
 
         @Override
+        public Collection<AnyPartialSymbol> getPartialSymbols() {
+                return null;
+        }
+
+        @Override
+        public Collection<Dnf> getLiftedQueries() {
+                return null;
+        }
+
+        @Override
         public PartialInterpretationAdapterImpl createModelAdapter(Model model) {
                 return new PartialInterpretationAdapterImpl(model, this);
         }
diff --git a/subprojects/store-partial/src/main/java/tools/refinery/store/partial/lifting/DnfLifter.java b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/lifting/DnfLifter.java
new file mode 100644
index 00000000..1c35b925
--- /dev/null
+++ b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/lifting/DnfLifter.java
@@ -0,0 +1,107 @@
+package tools.refinery.store.partial.lifting;
+
+import org.jetbrains.annotations.Nullable;
+import tools.refinery.store.partial.literal.ModalDnfCallLiteral;
+import tools.refinery.store.partial.PartialInterpretation;
+import tools.refinery.store.partial.literal.ModalRelationLiteral;
+import tools.refinery.store.partial.literal.PartialRelationLiteral;
+import tools.refinery.store.query.Dnf;
+import tools.refinery.store.query.DnfBuilder;
+import tools.refinery.store.query.DnfClause;
+import tools.refinery.store.query.Variable;
+import tools.refinery.store.query.literal.CallPolarity;
+import tools.refinery.store.query.literal.DnfCallLiteral;
+import tools.refinery.store.query.literal.Literal;
+import tools.refinery.store.partial.literal.Modality;
+import tools.refinery.store.util.CycleDetectingMapper;
+
+import java.util.ArrayList;
+import java.util.HashSet;
+import java.util.List;
+
+public class DnfLifter {
+        private final CycleDetectingMapper<ModalDnf, Dnf> mapper = new CycleDetectingMapper<>(ModalDnf::toString,
+                        this::doLift);
+
+        public Dnf lift(Modality modality, Dnf query) {
+                return mapper.map(new ModalDnf(modality, query));
+        }
+
+        private Dnf doLift(ModalDnf modalDnf) {
+                var modality = modalDnf.modality();
+                var dnf = modalDnf.dnf();
+                var builder = Dnf.builder();
+                builder.parameters(dnf.getParameters());
+                boolean changed = false;
+                for (var clause : dnf.getClauses()) {
+                        if (liftClause(modality, clause, builder)) {
+                                changed = true;
+                        }
+                }
+                if (changed) {
+                        return builder.build();
+                }
+                return dnf;
+        }
+
+        private boolean liftClause(Modality modality, DnfClause clause, DnfBuilder builder) {
+                boolean changed = false;
+                var quantifiedVariables = new HashSet<>(clause.quantifiedVariables());
+                var literals = clause.literals();
+                var liftedLiterals = new ArrayList<Literal>(literals.size());
+                for (var literal : literals) {
+                        Literal liftedLiteral = liftLiteral(modality, literal);
+                        if (liftedLiteral == null) {
+                                liftedLiteral = literal;
+                        } else {
+                                changed = true;
+                        }
+                        liftedLiterals.add(liftedLiteral);
+                        var variable = isExistsLiteralForVariable(modality, liftedLiteral);
+                        if (variable != null) {
+                                // If we already quantify over the existence of the variable with the expected modality,
+                                // we don't need to insert quantification manually.
+                                quantifiedVariables.remove(variable);
+                        }
+                }
+                for (var quantifiedVariable : quantifiedVariables) {
+                        // Quantify over variables that are not already quantified with the expected modality.
+                        liftedLiterals.add(PartialInterpretation.EXISTS.call(CallPolarity.POSITIVE, modality,
+                                        List.of(quantifiedVariable)));
+                }
+                builder.clause(liftedLiterals);
+                return changed || !quantifiedVariables.isEmpty();
+        }
+
+        @Nullable
+        private Variable isExistsLiteralForVariable(Modality modality, Literal literal) {
+                if (literal instanceof ModalRelationLiteral modalRelationLiteral &&
+                                modalRelationLiteral.getPolarity() == CallPolarity.POSITIVE &&
+                                modalRelationLiteral.getModality() == modality &&
+                                modalRelationLiteral.getTarget().equals(PartialInterpretation.EXISTS)) {
+                        return modalRelationLiteral.getArguments().get(0);
+                }
+                return null;
+        }
+
+        @Nullable
+        private Literal liftLiteral(Modality modality, Literal literal) {
+                if (literal instanceof PartialRelationLiteral partialRelationLiteral) {
+                        return new ModalRelationLiteral(modality, partialRelationLiteral);
+                } else if (literal instanceof DnfCallLiteral dnfCallLiteral) {
+                        var polarity = dnfCallLiteral.getPolarity();
+                        var target = dnfCallLiteral.getTarget();
+                        var liftedTarget = lift(modality.commute(polarity), target);
+                        if (target.equals(liftedTarget)) {
+                                return null;
+                        }
+                        return new DnfCallLiteral(polarity, liftedTarget, dnfCallLiteral.getArguments());
+                } else if (literal instanceof ModalDnfCallLiteral modalDnfCallLiteral) {
+                        var liftedTarget = lift(modalDnfCallLiteral.getModality(), modalDnfCallLiteral.getTarget());
+                        return new DnfCallLiteral(modalDnfCallLiteral.getPolarity(), liftedTarget,
+                                        modalDnfCallLiteral.getArguments());
+                } else {
+                        return null;
+                }
+        }
+}
diff --git a/subprojects/store-partial/src/main/java/tools/refinery/store/partial/lifting/ModalDnf.java b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/lifting/ModalDnf.java
new file mode 100644
index 00000000..6fe54ad9
--- /dev/null
+++ b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/lifting/ModalDnf.java
@@ -0,0 +1,11 @@
+package tools.refinery.store.partial.lifting;
+
+import tools.refinery.store.query.Dnf;
+import tools.refinery.store.partial.literal.Modality;
+
+public record ModalDnf(Modality modality, Dnf dnf) {
+        @Override
+        public String toString() {
+                return "%s %s".formatted(modality, dnf.name());
+        }
+}
diff --git a/subprojects/store/src/main/java/tools/refinery/store/partial/literal/ModalDnfCallLiteral.java b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/literal/ModalDnfCallLiteral.java
index 8070726a..a49e0625 100644
--- a/subprojects/store/src/main/java/tools/refinery/store/partial/literal/ModalDnfCallLiteral.java
+++ b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/literal/ModalDnfCallLiteral.java
@@ -4,6 +4,7 @@ import tools.refinery.store.query.Dnf;
 import tools.refinery.store.query.Variable;
 import tools.refinery.store.query.literal.CallPolarity;
 import tools.refinery.store.query.literal.DnfCallLiteral;
+import tools.refinery.store.query.literal.LiteralReduction;
 import tools.refinery.store.query.literal.PolarLiteral;
 
 import java.util.List;
@@ -27,4 +28,10 @@ public class ModalDnfCallLiteral extends ModalLiteral<Dnf> implements PolarLiter
         public ModalDnfCallLiteral negate() {
                 return new ModalDnfCallLiteral(getPolarity().negate(), getModality(), getTarget(), getArguments());
         }
+
+        @Override
+        public LiteralReduction getReduction() {
+                var dnfReduction = getTarget().getReduction();
+                return getPolarity().isPositive() ? dnfReduction : dnfReduction.negate();
+        }
 }
diff --git a/subprojects/store/src/main/java/tools/refinery/store/partial/literal/ModalLiteral.java b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/literal/ModalLiteral.java
index a1b6c83e..a1b6c83e 100644
--- a/subprojects/store/src/main/java/tools/refinery/store/partial/literal/ModalLiteral.java
+++ b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/literal/ModalLiteral.java
diff --git a/subprojects/store/src/main/java/tools/refinery/store/partial/literal/ModalRelationLiteral.java b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/literal/ModalRelationLiteral.java
index dbaa524f..dbaa524f 100644
--- a/subprojects/store/src/main/java/tools/refinery/store/partial/literal/ModalRelationLiteral.java
+++ b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/literal/ModalRelationLiteral.java
diff --git a/subprojects/store/src/main/java/tools/refinery/store/partial/literal/Modality.java b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/literal/Modality.java
index d647ef0a..d647ef0a 100644
--- a/subprojects/store/src/main/java/tools/refinery/store/partial/literal/Modality.java
+++ b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/literal/Modality.java
diff --git a/subprojects/store/src/main/java/tools/refinery/store/partial/literal/PartialLiterals.java b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/literal/PartialLiterals.java
index 51d388d3..51d388d3 100644
--- a/subprojects/store/src/main/java/tools/refinery/store/partial/literal/PartialLiterals.java
+++ b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/literal/PartialLiterals.java
diff --git a/subprojects/store/src/main/java/tools/refinery/store/partial/literal/PartialRelationLiteral.java b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/literal/PartialRelationLiteral.java
index dc1a1da3..dc1a1da3 100644
--- a/subprojects/store/src/main/java/tools/refinery/store/partial/literal/PartialRelationLiteral.java
+++ b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/literal/PartialRelationLiteral.java
diff --git a/subprojects/store/src/main/java/tools/refinery/store/partial/representation/AnyPartialFunction.java b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/representation/AnyPartialFunction.java
index 1113245e..1113245e 100644
--- a/subprojects/store/src/main/java/tools/refinery/store/partial/representation/AnyPartialFunction.java
+++ b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/representation/AnyPartialFunction.java
diff --git a/subprojects/store/src/main/java/tools/refinery/store/partial/representation/AnyPartialSymbol.java b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/representation/AnyPartialSymbol.java
index 25096e74..25096e74 100644
--- a/subprojects/store/src/main/java/tools/refinery/store/partial/representation/AnyPartialSymbol.java
+++ b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/representation/AnyPartialSymbol.java
diff --git a/subprojects/store/src/main/java/tools/refinery/store/partial/representation/PartialFunction.java b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/representation/PartialFunction.java
index 3c186f6f..3c186f6f 100644
--- a/subprojects/store/src/main/java/tools/refinery/store/partial/representation/PartialFunction.java
+++ b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/representation/PartialFunction.java
diff --git a/subprojects/store/src/main/java/tools/refinery/store/partial/representation/PartialRelation.java b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/representation/PartialRelation.java
index 127355ca..51c2f28d 100644
--- a/subprojects/store/src/main/java/tools/refinery/store/partial/representation/PartialRelation.java
+++ b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/representation/PartialRelation.java
@@ -1,11 +1,11 @@
 package tools.refinery.store.partial.representation;
 
-import tools.refinery.store.partial.literal.ModalRelationLiteral;
+import tools.refinery.store.partial.literal.Modality;
 import tools.refinery.store.partial.literal.PartialRelationLiteral;
+import tools.refinery.store.partial.literal.ModalRelationLiteral;
 import tools.refinery.store.query.RelationLike;
 import tools.refinery.store.query.Variable;
 import tools.refinery.store.query.literal.CallPolarity;
-import tools.refinery.store.partial.literal.Modality;
 import tools.refinery.store.representation.AbstractDomain;
 import tools.refinery.store.representation.TruthValue;
 import tools.refinery.store.representation.TruthValueDomain;
diff --git a/subprojects/store/src/main/java/tools/refinery/store/partial/representation/PartialSymbol.java b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/representation/PartialSymbol.java
index 38533fa9..38533fa9 100644
--- a/subprojects/store/src/main/java/tools/refinery/store/partial/representation/PartialSymbol.java
+++ b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/representation/PartialSymbol.java
diff --git a/subprojects/store-partial/src/main/java/tools/refinery/store/partial/rule/RelationRefinementAction.java b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/rule/RelationRefinementAction.java
new file mode 100644
index 00000000..6c89653d
--- /dev/null
+++ b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/rule/RelationRefinementAction.java
@@ -0,0 +1,36 @@
+package tools.refinery.store.partial.rule;
+
+import tools.refinery.store.partial.PartialInterpretation;
+import tools.refinery.store.partial.representation.PartialRelation;
+import tools.refinery.store.model.Model;
+import tools.refinery.store.query.Variable;
+import tools.refinery.store.representation.TruthValue;
+import tools.refinery.store.tuple.Tuple;
+
+import java.util.List;
+
+public record RelationRefinementAction(PartialRelation target, List<Variable> arguments, TruthValue value)
+                implements RuleAction {
+        public RelationRefinementAction {
+                if (arguments.size() != target.arity()) {
+                        throw new IllegalArgumentException("%s needs %d parameters, but got %s".formatted(target.name(),
+                                        target.arity(), arguments.size()));
+                }
+                if (value == TruthValue.UNKNOWN) {
+                        throw new IllegalArgumentException("Refining with UNKNOWN has no effect");
+                }
+        }
+
+        @Override
+        public RuleActionExecutor createExecutor(int[] argumentIndices, Model model) {
+                var targetInterpretation = model.getAdapter(PartialInterpretation.ADAPTER).getPartialInterpretation(target);
+                return activationTuple -> {
+                        int arity = argumentIndices.length;
+                        var arguments = new int[arity];
+                        for (int i = 0; i < arity; i++) {
+                                arguments[i] = activationTuple.get(argumentIndices[i]);
+                        }
+                        return targetInterpretation.merge(Tuple.of(arguments), value);
+                };
+        }
+}
diff --git a/subprojects/store-partial/src/main/java/tools/refinery/store/partial/rule/Rule.java b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/rule/Rule.java
new file mode 100644
index 00000000..c114b8cf
--- /dev/null
+++ b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/rule/Rule.java
@@ -0,0 +1,38 @@
+package tools.refinery.store.partial.rule;
+
+import tools.refinery.store.model.Model;
+import tools.refinery.store.query.Dnf;
+
+import java.util.ArrayList;
+import java.util.HashSet;
+import java.util.List;
+
+public record Rule(Dnf precondition, List<RuleAction> actions) {
+        public Rule {
+                var parameterSet = new HashSet<>(precondition.getParameters());
+                for (var action : actions) {
+                        for (var argument : action.arguments()) {
+                                if (!parameterSet.contains(argument)) {
+                                        throw new IllegalArgumentException(
+                                                        "Argument %s of action %s does not appear in the parameter list %s of %s"
+                                                                        .formatted(argument, action, precondition.getParameters(), precondition.name()));
+                                }
+                        }
+                }
+        }
+
+        public RuleExecutor createExecutor(Model model) {
+                var parameters = precondition.getParameters();
+                var actionExecutors = new ArrayList<RuleActionExecutor>(actions.size());
+                for (var action : actions) {
+                        var arguments = action.arguments();
+                        int arity = arguments.size();
+                        var argumentIndices = new int[arity];
+                        for (int i = 0; i < arity; i++) {
+                                argumentIndices[i] = parameters.indexOf(arguments.get(i));
+                        }
+                        actionExecutors.add(action.createExecutor(argumentIndices, model));
+                }
+                return new RuleExecutor(this, model, actionExecutors);
+        }
+}
diff --git a/subprojects/store-partial/src/main/java/tools/refinery/store/partial/rule/RuleAction.java b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/rule/RuleAction.java
new file mode 100644
index 00000000..7a8ede40
--- /dev/null
+++ b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/rule/RuleAction.java
@@ -0,0 +1,12 @@
+package tools.refinery.store.partial.rule;
+
+import tools.refinery.store.model.Model;
+import tools.refinery.store.query.Variable;
+
+import java.util.List;
+
+public interface RuleAction {
+        List<Variable> arguments();
+
+        RuleActionExecutor createExecutor(int[] argumentIndices, Model model);
+}
diff --git a/subprojects/store-partial/src/main/java/tools/refinery/store/partial/rule/RuleActionExecutor.java b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/rule/RuleActionExecutor.java
new file mode 100644
index 00000000..1c2db5f1
--- /dev/null
+++ b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/rule/RuleActionExecutor.java
@@ -0,0 +1,9 @@
+package tools.refinery.store.partial.rule;
+
+import tools.refinery.store.partial.MergeResult;
+import tools.refinery.store.tuple.TupleLike;
+
+@FunctionalInterface
+public interface RuleActionExecutor {
+        MergeResult execute(TupleLike activationTuple);
+}
diff --git a/subprojects/store-partial/src/main/java/tools/refinery/store/partial/rule/RuleExecutor.java b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/rule/RuleExecutor.java
new file mode 100644
index 00000000..41d79306
--- /dev/null
+++ b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/rule/RuleExecutor.java
@@ -0,0 +1,34 @@
+package tools.refinery.store.partial.rule;
+
+import tools.refinery.store.partial.MergeResult;
+import tools.refinery.store.model.Model;
+import tools.refinery.store.tuple.TupleLike;
+
+import java.util.List;
+
+public final class RuleExecutor {
+        private final Rule rule;
+        private final Model model;
+        private final List<RuleActionExecutor> actionExecutors;
+
+        RuleExecutor(Rule rule, Model model, List<RuleActionExecutor> actionExecutors) {
+                this.rule = rule;
+                this.model = model;
+                this.actionExecutors = actionExecutors;
+        }
+
+        public Rule getRule() {
+                return rule;
+        }
+
+        public Model getModel() {
+                return model;
+        }
+        public MergeResult execute(TupleLike activationTuple) {
+                MergeResult mergeResult = MergeResult.UNCHANGED;
+                for (var actionExecutor : actionExecutors) {
+                        mergeResult = mergeResult.andAlso(actionExecutor.execute(activationTuple));
+                }
+                return mergeResult;
+        }
+}
diff --git a/subprojects/store-partial/src/main/java/tools/refinery/store/partial/translator/Advice.java b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/translator/Advice.java
new file mode 100644
index 00000000..65040a8e
--- /dev/null
+++ b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/translator/Advice.java
@@ -0,0 +1,155 @@
+package tools.refinery.store.partial.translator;
+
+import tools.refinery.store.partial.representation.AnyPartialSymbol;
+import tools.refinery.store.partial.representation.PartialRelation;
+import tools.refinery.store.query.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();
+                int arity = parameters.size();
+                var substitution = new HashMap<Variable, Variable>(arity);
+                for (int i = 0; i < arity; i++) {
+                        substitution.put(parameters.get(i), substituteParameters.get(i));
+                }
+                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-partial/src/main/java/tools/refinery/store/partial/translator/AdviceSlot.java b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/translator/AdviceSlot.java
new file mode 100644
index 00000000..3702a8ac
--- /dev/null
+++ b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/translator/AdviceSlot.java
@@ -0,0 +1,25 @@
+package tools.refinery.store.partial.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-partial/src/main/java/tools/refinery/store/partial/translator/Seed.java b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/translator/Seed.java
new file mode 100644
index 00000000..c56b06ed
--- /dev/null
+++ b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/translator/Seed.java
@@ -0,0 +1,12 @@
+package tools.refinery.store.partial.translator;
+
+import tools.refinery.store.map.Cursor;
+import tools.refinery.store.tuple.Tuple;
+
+public interface Seed<T> {
+        int arity();
+
+        T get(Tuple key);
+
+        Cursor<Tuple, T> getCursor(T defaultValue, int nodeCount);
+}
diff --git a/subprojects/store-partial/src/main/java/tools/refinery/store/partial/translator/TranslationUnit.java b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/translator/TranslationUnit.java
new file mode 100644
index 00000000..26bd909b
--- /dev/null
+++ b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/translator/TranslationUnit.java
@@ -0,0 +1,48 @@
+package tools.refinery.store.partial.translator;
+
+import tools.refinery.store.partial.PartialInterpretationBuilder;
+import tools.refinery.store.model.Model;
+import tools.refinery.store.model.ModelStoreBuilder;
+import tools.refinery.store.partial.AnyPartialSymbolInterpretation;
+import tools.refinery.store.partial.literal.Modality;
+import tools.refinery.store.partial.representation.AnyPartialSymbol;
+import tools.refinery.store.partial.representation.PartialRelation;
+import tools.refinery.store.query.Variable;
+import tools.refinery.store.query.literal.CallPolarity;
+import tools.refinery.store.query.literal.Literal;
+
+import java.util.Collection;
+import java.util.List;
+import java.util.Map;
+
+public abstract class TranslationUnit {
+        private PartialInterpretationBuilder partialInterpretationBuilder;
+
+        protected PartialInterpretationBuilder getPartialInterpretationBuilder() {
+                return partialInterpretationBuilder;
+        }
+
+        public void setPartialInterpretationBuilder(PartialInterpretationBuilder partialInterpretationBuilder) {
+                this.partialInterpretationBuilder = partialInterpretationBuilder;
+        }
+
+        protected ModelStoreBuilder getModelStoreBuilder() {
+                return partialInterpretationBuilder.getStoreBuilder();
+        }
+
+        public abstract Collection<AnyPartialSymbol> getTranslatedPartialSymbols();
+
+        public Collection<Advice> computeAdvices() {
+                // No advices to give by default.
+                return List.of();
+        }
+
+        public abstract void configure(Collection<Advice> advices);
+
+        public abstract List<Literal> call(CallPolarity polarity, Modality modality, PartialRelation target,
+                                                                           List<Variable> arguments);
+
+        public abstract Map<AnyPartialSymbol, AnyPartialSymbolInterpretation> createPartialInterpretations(Model model);
+
+        public abstract void initializeModel(Model model, int nodeCount);
+}
diff --git a/subprojects/store/src/main/java/tools/refinery/store/partial/translator/typehierarchy/EliminatedType.java b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/translator/typehierarchy/EliminatedType.java
index 9adf6bc8..9adf6bc8 100644
--- a/subprojects/store/src/main/java/tools/refinery/store/partial/translator/typehierarchy/EliminatedType.java
+++ b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/translator/typehierarchy/EliminatedType.java
diff --git a/subprojects/store/src/main/java/tools/refinery/store/partial/translator/typehierarchy/ExtendedTypeInfo.java b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/translator/typehierarchy/ExtendedTypeInfo.java
index d3f66a4c..d3f66a4c 100644
--- a/subprojects/store/src/main/java/tools/refinery/store/partial/translator/typehierarchy/ExtendedTypeInfo.java
+++ b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/translator/typehierarchy/ExtendedTypeInfo.java
diff --git a/subprojects/store-partial/src/main/java/tools/refinery/store/partial/translator/typehierarchy/InferredMayTypeRelationView.java b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/translator/typehierarchy/InferredMayTypeRelationView.java
new file mode 100644
index 00000000..ff761936
--- /dev/null
+++ b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/translator/typehierarchy/InferredMayTypeRelationView.java
@@ -0,0 +1,19 @@
+package tools.refinery.store.partial.translator.typehierarchy;
+
+import tools.refinery.store.partial.representation.PartialRelation;
+import tools.refinery.store.query.view.TuplePreservingRelationView;
+import tools.refinery.store.tuple.Tuple;
+
+class InferredMayTypeRelationView extends TuplePreservingRelationView<InferredType> {
+        private final PartialRelation type;
+
+        InferredMayTypeRelationView(PartialRelation type) {
+                super(TypeHierarchyTranslationUnit.INFERRED_TYPE_SYMBOL, "%s#may".formatted(type));
+                this.type = type;
+        }
+
+        @Override
+        public boolean filter(Tuple key, InferredType value) {
+                return value.mayConcreteTypes().contains(type);
+        }
+}
diff --git a/subprojects/store-partial/src/main/java/tools/refinery/store/partial/translator/typehierarchy/InferredMustTypeRelationView.java b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/translator/typehierarchy/InferredMustTypeRelationView.java
new file mode 100644
index 00000000..4eca0a1c
--- /dev/null
+++ b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/translator/typehierarchy/InferredMustTypeRelationView.java
@@ -0,0 +1,19 @@
+package tools.refinery.store.partial.translator.typehierarchy;
+
+import tools.refinery.store.partial.representation.PartialRelation;
+import tools.refinery.store.query.view.TuplePreservingRelationView;
+import tools.refinery.store.tuple.Tuple;
+
+class InferredMustTypeRelationView extends TuplePreservingRelationView<InferredType> {
+        private final PartialRelation type;
+
+        InferredMustTypeRelationView(PartialRelation type) {
+                super(TypeHierarchyTranslationUnit.INFERRED_TYPE_SYMBOL, "%s#must".formatted(type));
+                this.type = type;
+        }
+
+        @Override
+        public boolean filter(Tuple key, InferredType value) {
+                return value.mustTypes().contains(type);
+        }
+}
diff --git a/subprojects/store/src/main/java/tools/refinery/store/partial/translator/typehierarchy/InferredType.java b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/translator/typehierarchy/InferredType.java
index 729b1fb5..729b1fb5 100644
--- a/subprojects/store/src/main/java/tools/refinery/store/partial/translator/typehierarchy/InferredType.java
+++ b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/translator/typehierarchy/InferredType.java
diff --git a/subprojects/store/src/main/java/tools/refinery/store/partial/translator/typehierarchy/PreservedType.java b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/translator/typehierarchy/PreservedType.java
index 0299ae03..0299ae03 100644
--- a/subprojects/store/src/main/java/tools/refinery/store/partial/translator/typehierarchy/PreservedType.java
+++ b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/translator/typehierarchy/PreservedType.java
diff --git a/subprojects/store/src/main/java/tools/refinery/store/partial/translator/typehierarchy/TypeAnalysisResult.java b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/translator/typehierarchy/TypeAnalysisResult.java
index 0745f84e..0745f84e 100644
--- a/subprojects/store/src/main/java/tools/refinery/store/partial/translator/typehierarchy/TypeAnalysisResult.java
+++ b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/translator/typehierarchy/TypeAnalysisResult.java
diff --git a/subprojects/store/src/main/java/tools/refinery/store/partial/translator/typehierarchy/TypeAnalyzer.java b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/translator/typehierarchy/TypeAnalyzer.java
index 062b4c49..062b4c49 100644
--- a/subprojects/store/src/main/java/tools/refinery/store/partial/translator/typehierarchy/TypeAnalyzer.java
+++ b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/translator/typehierarchy/TypeAnalyzer.java
diff --git a/subprojects/store-partial/src/main/java/tools/refinery/store/partial/translator/typehierarchy/TypeHierarchyTranslationUnit.java b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/translator/typehierarchy/TypeHierarchyTranslationUnit.java
new file mode 100644
index 00000000..7f438f71
--- /dev/null
+++ b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/translator/typehierarchy/TypeHierarchyTranslationUnit.java
@@ -0,0 +1,52 @@
+package tools.refinery.store.partial.translator.typehierarchy;
+
+import tools.refinery.store.partial.AnyPartialSymbolInterpretation;
+import tools.refinery.store.partial.literal.Modality;
+import tools.refinery.store.partial.representation.AnyPartialSymbol;
+import tools.refinery.store.partial.representation.PartialRelation;
+import tools.refinery.store.partial.translator.Advice;
+import tools.refinery.store.partial.translator.TranslationUnit;
+import tools.refinery.store.model.Model;
+import tools.refinery.store.query.Variable;
+import tools.refinery.store.query.literal.CallPolarity;
+import tools.refinery.store.query.literal.Literal;
+import tools.refinery.store.representation.Symbol;
+
+import java.util.*;
+
+public class TypeHierarchyTranslationUnit extends TranslationUnit {
+        static final Symbol<InferredType> INFERRED_TYPE_SYMBOL = new Symbol<>("inferredType", 1,
+                        InferredType.class, InferredType.UNTYPED);
+
+        private final Map<PartialRelation, TypeInfo> typeInfoMap;
+
+        public TypeHierarchyTranslationUnit(Map<PartialRelation, TypeInfo> typeInfoMap) {
+                this.typeInfoMap = new LinkedHashMap<>(typeInfoMap);
+        }
+
+        @Override
+        public Collection<AnyPartialSymbol> getTranslatedPartialSymbols() {
+                return null;
+        }
+
+        @Override
+        public void configure(Collection<Advice> advices) {
+
+        }
+
+        @Override
+        public List<Literal> call(CallPolarity polarity, Modality modality, PartialRelation target,
+                                                          List<Variable> arguments) {
+                return null;
+        }
+
+        @Override
+        public Map<AnyPartialSymbol, AnyPartialSymbolInterpretation> createPartialInterpretations(Model model) {
+                return null;
+        }
+
+        @Override
+        public void initializeModel(Model model, int nodeCount) {
+
+        }
+}
diff --git a/subprojects/store/src/main/java/tools/refinery/store/partial/translator/typehierarchy/TypeInfo.java b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/translator/typehierarchy/TypeInfo.java
index 1b0922fe..1b0922fe 100644
--- a/subprojects/store/src/main/java/tools/refinery/store/partial/translator/typehierarchy/TypeInfo.java
+++ b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/translator/typehierarchy/TypeInfo.java
diff --git a/subprojects/store/src/test/java/tools/refinery/store/partial/translator/typehierarchy/InferredTypeTest.java b/subprojects/store-partial/src/test/java/tools/refinery/store/partial/translator/typehierarchy/InferredTypeTest.java
index 9efa76ef..9efa76ef 100644
--- a/subprojects/store/src/test/java/tools/refinery/store/partial/translator/typehierarchy/InferredTypeTest.java
+++ b/subprojects/store-partial/src/test/java/tools/refinery/store/partial/translator/typehierarchy/InferredTypeTest.java
diff --git a/subprojects/store/src/test/java/tools/refinery/store/partial/translator/typehierarchy/TypeAnalyzerExampleHierarchyTest.java b/subprojects/store-partial/src/test/java/tools/refinery/store/partial/translator/typehierarchy/TypeAnalyzerExampleHierarchyTest.java
index 5f528328..ad81e28f 100644
--- a/subprojects/store/src/test/java/tools/refinery/store/partial/translator/typehierarchy/TypeAnalyzerExampleHierarchyTest.java
+++ b/subprojects/store-partial/src/test/java/tools/refinery/store/partial/translator/typehierarchy/TypeAnalyzerExampleHierarchyTest.java
@@ -1,5 +1,6 @@
 package tools.refinery.store.partial.translator.typehierarchy;
 
+import org.hamcrest.Matchers;
 import org.junit.jupiter.api.BeforeEach;
 import org.junit.jupiter.api.Test;
 import tools.refinery.store.partial.representation.PartialRelation;
@@ -60,16 +61,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)))
                 );
         }
 
@@ -79,8 +80,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),
@@ -95,19 +96,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)))
                 );
         }
 
@@ -117,8 +118,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))
                 );
         }
 
@@ -140,9 +141,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)))
                 );
         }
 
@@ -153,13 +154,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)))
                 );
         }
 
@@ -169,9 +170,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)))
                 );
         }
 
@@ -193,9 +194,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/src/test/java/tools/refinery/store/partial/translator/typehierarchy/TypeAnalyzerTest.java b/subprojects/store-partial/src/test/java/tools/refinery/store/partial/translator/typehierarchy/TypeAnalyzerTest.java
index 02903026..1aab75bb 100644
--- a/subprojects/store/src/test/java/tools/refinery/store/partial/translator/typehierarchy/TypeAnalyzerTest.java
+++ b/subprojects/store-partial/src/test/java/tools/refinery/store/partial/translator/typehierarchy/TypeAnalyzerTest.java
@@ -1,5 +1,6 @@
 package tools.refinery.store.partial.translator.typehierarchy;
 
+import org.hamcrest.Matchers;
 import org.junit.jupiter.api.Test;
 import tools.refinery.store.partial.representation.PartialRelation;
 import tools.refinery.store.representation.TruthValue;
@@ -136,8 +137,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))
                 );
         }
 
@@ -161,7 +162,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
@@ -184,7 +185,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/test/java/tools/refinery/store/partial/translator/typehierarchy/TypeAnalyzerTester.java b/subprojects/store-partial/src/test/java/tools/refinery/store/partial/translator/typehierarchy/TypeAnalyzerTester.java
index ce600ea6..ce600ea6 100644
--- a/subprojects/store/src/test/java/tools/refinery/store/partial/translator/typehierarchy/TypeAnalyzerTester.java
+++ b/subprojects/store-partial/src/test/java/tools/refinery/store/partial/translator/typehierarchy/TypeAnalyzerTester.java
diff --git a/subprojects/store-query-viatra/build.gradle b/subprojects/store-query-viatra/build.gradle
index c12b48fe..13a7544f 100644
--- a/subprojects/store-query-viatra/build.gradle
+++ b/subprojects/store-query-viatra/build.gradle
@@ -10,7 +10,7 @@ configurations.testRuntimeClasspath {
 dependencies {
         implementation libs.ecore
         api libs.viatra
-        api project(':refinery-store')
+        api project(':refinery-store-query')
         testImplementation libs.slf4j.simple
         testImplementation libs.slf4j.log4j
 }
diff --git a/subprojects/store-query/build.gradle b/subprojects/store-query/build.gradle
new file mode 100644
index 00000000..2b76e608
--- /dev/null
+++ b/subprojects/store-query/build.gradle
@@ -0,0 +1,7 @@
+plugins {
+        id 'refinery-java-library'
+}
+
+dependencies {
+        api project(':refinery-store')
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/Dnf.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/Dnf.java
new file mode 100644
index 00000000..760b264b
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/Dnf.java
@@ -0,0 +1,112 @@
+package tools.refinery.store.query;
+
+import tools.refinery.store.query.literal.CallPolarity;
+import tools.refinery.store.query.literal.DnfCallLiteral;
+import tools.refinery.store.query.literal.LiteralReduction;
+
+import java.util.*;
+
+public final class Dnf implements RelationLike {
+        private final String name;
+
+        private final String uniqueName;
+
+        private final List<Variable> parameters;
+
+        private final List<FunctionalDependency<Variable>> functionalDependencies;
+
+        private final List<DnfClause> clauses;
+
+        Dnf(String name, List<Variable> parameters, List<FunctionalDependency<Variable>> functionalDependencies,
+                List<DnfClause> clauses) {
+                validateFunctionalDependencies(parameters, functionalDependencies);
+                this.name = name;
+                this.uniqueName = DnfUtils.generateUniqueName(name);
+                this.parameters = parameters;
+                this.functionalDependencies = functionalDependencies;
+                this.clauses = clauses;
+        }
+
+        private static void validateFunctionalDependencies(
+                        Collection<Variable> parameters, Collection<FunctionalDependency<Variable>> functionalDependencies) {
+                var parameterSet = new HashSet<>(parameters);
+                for (var functionalDependency : functionalDependencies) {
+                        validateParameters(parameters, parameterSet, functionalDependency.forEach(), functionalDependency);
+                        validateParameters(parameters, parameterSet, functionalDependency.unique(), functionalDependency);
+                }
+        }
+
+        private static void validateParameters(Collection<Variable> parameters, Set<Variable> parameterSet,
+                                                                                   Collection<Variable> toValidate,
+                                                                                   FunctionalDependency<Variable> functionalDependency) {
+                for (var variable : toValidate) {
+                        if (!parameterSet.contains(variable)) {
+                                throw new IllegalArgumentException(
+                                                "Variable %s of functional dependency %s does not appear in the parameter list %s"
+                                                                .formatted(variable, functionalDependency, parameters));
+                        }
+                }
+        }
+
+        @Override
+        public String name() {
+                return name;
+        }
+
+        public String getUniqueName() {
+                return uniqueName;
+        }
+
+        public List<Variable> getParameters() {
+                return parameters;
+        }
+
+        public List<FunctionalDependency<Variable>> getFunctionalDependencies() {
+                return functionalDependencies;
+        }
+
+        @Override
+        public int arity() {
+                return parameters.size();
+        }
+
+        public List<DnfClause> getClauses() {
+                return clauses;
+        }
+
+        public LiteralReduction getReduction() {
+                if (clauses.isEmpty()) {
+                        return LiteralReduction.ALWAYS_FALSE;
+                }
+                for (var clause : clauses) {
+                        if (clause.literals().isEmpty()) {
+                                return LiteralReduction.ALWAYS_TRUE;
+                        }
+                }
+                return LiteralReduction.NOT_REDUCIBLE;
+        }
+
+        public DnfCallLiteral call(CallPolarity polarity, List<Variable> arguments) {
+                return new DnfCallLiteral(polarity, this, arguments);
+        }
+
+        public DnfCallLiteral call(CallPolarity polarity, Variable... arguments) {
+                return call(polarity, List.of(arguments));
+        }
+
+        public DnfCallLiteral call(Variable... arguments) {
+                return call(CallPolarity.POSITIVE, arguments);
+        }
+
+        public DnfCallLiteral callTransitive(Variable left, Variable right) {
+                return call(CallPolarity.TRANSITIVE, List.of(left, right));
+        }
+
+        public static DnfBuilder builder() {
+                return builder(null);
+        }
+
+        public static DnfBuilder builder(String name) {
+                return new DnfBuilder(name);
+        }
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/DnfBuilder.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/DnfBuilder.java
new file mode 100644
index 00000000..b18b5177
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/DnfBuilder.java
@@ -0,0 +1,108 @@
+package tools.refinery.store.query;
+
+import tools.refinery.store.query.literal.Literal;
+
+import java.util.*;
+
+@SuppressWarnings("UnusedReturnValue")
+public class DnfBuilder {
+        private final String name;
+
+        private final List<Variable> parameters = new ArrayList<>();
+
+        private final List<FunctionalDependency<Variable>> functionalDependencies = new ArrayList<>();
+
+        private final List<List<Literal>> clauses = new ArrayList<>();
+
+        DnfBuilder(String name) {
+                this.name = name;
+        }
+
+        public DnfBuilder parameter(Variable variable) {
+                parameters.add(variable);
+                return this;
+        }
+
+        public DnfBuilder parameters(Variable... variables) {
+                return parameters(List.of(variables));
+        }
+
+        public DnfBuilder parameters(Collection<Variable> variables) {
+                parameters.addAll(variables);
+                return this;
+        }
+
+        public DnfBuilder functionalDependencies(Collection<FunctionalDependency<Variable>> functionalDependencies) {
+                this.functionalDependencies.addAll(functionalDependencies);
+                return this;
+        }
+
+        public DnfBuilder functionalDependency(FunctionalDependency<Variable> functionalDependency) {
+                functionalDependencies.add(functionalDependency);
+                return this;
+        }
+
+        public DnfBuilder functionalDependency(Set<Variable> forEach, Set<Variable> unique) {
+                return functionalDependency(new FunctionalDependency<>(forEach, unique));
+        }
+
+        public DnfBuilder clause(Literal... literals) {
+                clause(List.of(literals));
+                return this;
+        }
+
+        public DnfBuilder clause(Collection<Literal> literals) {
+                var filteredLiterals = new ArrayList<Literal>(literals.size());
+                for (var literal : literals) {
+                        var reduction = literal.getReduction();
+                        switch (reduction) {
+                        case NOT_REDUCIBLE -> filteredLiterals.add(literal);
+                        case ALWAYS_TRUE -> {
+                                // Literals reducible to {@code true} can be omitted, because the model is always assumed to have at
+                                // least on object.
+                        }
+                        case ALWAYS_FALSE -> {
+                                // Clauses with {@code false} literals can be omitted entirely.
+                                return this;
+                        }
+                        default -> throw new IllegalStateException("Invalid reduction %s".formatted(reduction));
+                        }
+                }
+                clauses.add(Collections.unmodifiableList(filteredLiterals));
+                return this;
+        }
+
+        public DnfBuilder clause(DnfClause clause) {
+                return clause(clause.literals());
+        }
+
+        public DnfBuilder clauses(DnfClause... clauses) {
+                for (var clause : clauses) {
+                        this.clause(clause);
+                }
+                return this;
+        }
+
+        public DnfBuilder clauses(Collection<DnfClause> clauses) {
+                for (var clause : clauses) {
+                        this.clause(clause);
+                }
+                return this;
+        }
+
+        public Dnf build() {
+                var postProcessedClauses = new ArrayList<DnfClause>(clauses.size());
+                for (var constraints : clauses) {
+                        var variables = new HashSet<Variable>();
+                        for (var constraint : constraints) {
+                                constraint.collectAllVariables(variables);
+                        }
+                        parameters.forEach(variables::remove);
+                        postProcessedClauses.add(new DnfClause(Collections.unmodifiableSet(variables),
+                                        Collections.unmodifiableList(constraints)));
+                }
+                return new Dnf(name, Collections.unmodifiableList(parameters),
+                                Collections.unmodifiableList(functionalDependencies),
+                                Collections.unmodifiableList(postProcessedClauses));
+        }
+}
diff --git a/subprojects/store/src/main/java/tools/refinery/store/query/DnfClause.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/DnfClause.java
index 2ba6becc..2ba6becc 100644
--- a/subprojects/store/src/main/java/tools/refinery/store/query/DnfClause.java
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/DnfClause.java
diff --git a/subprojects/store/src/main/java/tools/refinery/store/query/DnfUtils.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/DnfUtils.java
index 17564d43..17564d43 100644
--- a/subprojects/store/src/main/java/tools/refinery/store/query/DnfUtils.java
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/DnfUtils.java
diff --git a/subprojects/store/src/main/java/tools/refinery/store/query/FunctionalDependency.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/FunctionalDependency.java
index 63a81713..63a81713 100644
--- a/subprojects/store/src/main/java/tools/refinery/store/query/FunctionalDependency.java
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/FunctionalDependency.java
diff --git a/subprojects/store/src/main/java/tools/refinery/store/query/ModelQuery.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/ModelQuery.java
index 6a1aeabb..6a1aeabb 100644
--- a/subprojects/store/src/main/java/tools/refinery/store/query/ModelQuery.java
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/ModelQuery.java
diff --git a/subprojects/store/src/main/java/tools/refinery/store/query/ModelQueryAdapter.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/ModelQueryAdapter.java
index f7762444..f7762444 100644
--- a/subprojects/store/src/main/java/tools/refinery/store/query/ModelQueryAdapter.java
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/ModelQueryAdapter.java
diff --git a/subprojects/store/src/main/java/tools/refinery/store/query/ModelQueryBuilder.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/ModelQueryBuilder.java
index b3cfb4b4..b3cfb4b4 100644
--- a/subprojects/store/src/main/java/tools/refinery/store/query/ModelQueryBuilder.java
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/ModelQueryBuilder.java
diff --git a/subprojects/store/src/main/java/tools/refinery/store/query/ModelQueryStoreAdapter.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/ModelQueryStoreAdapter.java
index 3efeacaa..091d6d06 100644
--- a/subprojects/store/src/main/java/tools/refinery/store/query/ModelQueryStoreAdapter.java
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/ModelQueryStoreAdapter.java
@@ -1,8 +1,8 @@
 package tools.refinery.store.query;
 
+import tools.refinery.store.query.view.AnyRelationView;
 import tools.refinery.store.adapter.ModelStoreAdapter;
 import tools.refinery.store.model.Model;
-import tools.refinery.store.query.view.AnyRelationView;
 
 import java.util.Collection;
 
diff --git a/subprojects/store/src/main/java/tools/refinery/store/query/RelationLike.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/RelationLike.java
index 8c784d8b..8c784d8b 100644
--- a/subprojects/store/src/main/java/tools/refinery/store/query/RelationLike.java
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/RelationLike.java
diff --git a/subprojects/store/src/main/java/tools/refinery/store/query/ResultSet.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/ResultSet.java
index 3542e252..3542e252 100644
--- a/subprojects/store/src/main/java/tools/refinery/store/query/ResultSet.java
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/ResultSet.java
diff --git a/subprojects/store/src/main/java/tools/refinery/store/query/Variable.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/Variable.java
index 2eb87649..2eb87649 100644
--- a/subprojects/store/src/main/java/tools/refinery/store/query/Variable.java
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/Variable.java
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/BooleanLiteral.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/BooleanLiteral.java
new file mode 100644
index 00000000..fd2f1eec
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/BooleanLiteral.java
@@ -0,0 +1,37 @@
+package tools.refinery.store.query.literal;
+
+import tools.refinery.store.query.Variable;
+
+import java.util.Map;
+import java.util.Set;
+
+public class BooleanLiteral implements Literal {
+        public static final BooleanLiteral TRUE = new BooleanLiteral(LiteralReduction.ALWAYS_TRUE);
+        public static final BooleanLiteral FALSE = new BooleanLiteral(LiteralReduction.ALWAYS_FALSE);
+
+        private final LiteralReduction reduction;
+
+        private BooleanLiteral(LiteralReduction reduction) {
+                this.reduction = reduction;
+        }
+
+        @Override
+        public void collectAllVariables(Set<Variable> variables) {
+                // No variables to collect.
+        }
+
+        @Override
+        public Literal substitute(Map<Variable, Variable> substitution) {
+                // No variables to substitute.
+                return this;
+        }
+
+        @Override
+        public LiteralReduction getReduction() {
+                return reduction;
+        }
+
+        public static BooleanLiteral fromBoolean(boolean value) {
+                return value ? TRUE : FALSE;
+        }
+}
diff --git a/subprojects/store/src/main/java/tools/refinery/store/query/literal/CallLiteral.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/CallLiteral.java
index 5e1ae94d..5e1ae94d 100644
--- a/subprojects/store/src/main/java/tools/refinery/store/query/literal/CallLiteral.java
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/CallLiteral.java
diff --git a/subprojects/store/src/main/java/tools/refinery/store/query/literal/CallPolarity.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/CallPolarity.java
index 84b4b771..84b4b771 100644
--- a/subprojects/store/src/main/java/tools/refinery/store/query/literal/CallPolarity.java
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/CallPolarity.java
diff --git a/subprojects/store/src/main/java/tools/refinery/store/query/literal/ConstantLiteral.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/ConstantLiteral.java
index 746d23af..746d23af 100644
--- a/subprojects/store/src/main/java/tools/refinery/store/query/literal/ConstantLiteral.java
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/ConstantLiteral.java
diff --git a/subprojects/store/src/main/java/tools/refinery/store/query/literal/DnfCallLiteral.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/DnfCallLiteral.java
index 40499222..de6c6005 100644
--- a/subprojects/store/src/main/java/tools/refinery/store/query/literal/DnfCallLiteral.java
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/DnfCallLiteral.java
@@ -20,4 +20,10 @@ public final class DnfCallLiteral extends CallLiteral<Dnf> implements PolarLiter
         public DnfCallLiteral negate() {
                 return new DnfCallLiteral(getPolarity().negate(), getTarget(), getArguments());
         }
+
+        @Override
+        public LiteralReduction getReduction() {
+                var dnfReduction = getTarget().getReduction();
+                return getPolarity().isPositive() ? dnfReduction : dnfReduction.negate();
+        }
 }
diff --git a/subprojects/store/src/main/java/tools/refinery/store/query/literal/EquivalenceLiteral.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/EquivalenceLiteral.java
index 5fee54b1..f30179b2 100644
--- a/subprojects/store/src/main/java/tools/refinery/store/query/literal/EquivalenceLiteral.java
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/EquivalenceLiteral.java
@@ -24,4 +24,12 @@ public record EquivalenceLiteral(boolean positive, Variable left, Variable right
                 return new EquivalenceLiteral(positive, DnfUtils.maybeSubstitute(left, substitution),
                                 DnfUtils.maybeSubstitute(right, substitution));
         }
+
+        @Override
+        public LiteralReduction getReduction() {
+                if (left.equals(right)) {
+                        return positive ? LiteralReduction.ALWAYS_TRUE : LiteralReduction.ALWAYS_FALSE;
+                }
+                return LiteralReduction.NOT_REDUCIBLE;
+        }
 }
diff --git a/subprojects/store/src/main/java/tools/refinery/store/query/literal/Literal.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/Literal.java
index e0f5f605..a6893acf 100644
--- a/subprojects/store/src/main/java/tools/refinery/store/query/literal/Literal.java
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/Literal.java
@@ -9,4 +9,8 @@ public interface Literal {
         void collectAllVariables(Set<Variable> variables);
 
         Literal substitute(Map<Variable, Variable> substitution);
+
+        default LiteralReduction getReduction() {
+                return LiteralReduction.NOT_REDUCIBLE;
+        }
 }
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/LiteralReduction.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/LiteralReduction.java
new file mode 100644
index 00000000..146089f6
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/LiteralReduction.java
@@ -0,0 +1,26 @@
+package tools.refinery.store.query.literal;
+
+public enum LiteralReduction {
+        /**
+         * Signifies that a literal should be preserved in the clause.
+         */
+        NOT_REDUCIBLE,
+
+        /**
+         * Signifies that the literal may be omitted from the cause (if the model being queried is nonempty).
+         */
+        ALWAYS_TRUE,
+
+        /**
+         * Signifies that the clause with the literal may be omitted entirely.
+         */
+        ALWAYS_FALSE;
+
+        public LiteralReduction negate() {
+                return switch (this) {
+                        case NOT_REDUCIBLE -> NOT_REDUCIBLE;
+                        case ALWAYS_TRUE -> ALWAYS_FALSE;
+                        case ALWAYS_FALSE -> ALWAYS_TRUE;
+                };
+        }
+}
diff --git a/subprojects/store/src/main/java/tools/refinery/store/query/literal/Literals.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/Literals.java
index 2c7e893f..2c7e893f 100644
--- a/subprojects/store/src/main/java/tools/refinery/store/query/literal/Literals.java
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/Literals.java
diff --git a/subprojects/store/src/main/java/tools/refinery/store/query/literal/PolarLiteral.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/PolarLiteral.java
index 32523675..32523675 100644
--- a/subprojects/store/src/main/java/tools/refinery/store/query/literal/PolarLiteral.java
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/PolarLiteral.java
diff --git a/subprojects/store/src/main/java/tools/refinery/store/query/literal/RelationViewLiteral.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/RelationViewLiteral.java
index 4718b550..4718b550 100644
--- a/subprojects/store/src/main/java/tools/refinery/store/query/literal/RelationViewLiteral.java
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/RelationViewLiteral.java
diff --git a/subprojects/store/src/main/java/tools/refinery/store/query/view/AnyRelationView.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/view/AnyRelationView.java
index 328cde3a..328cde3a 100644
--- a/subprojects/store/src/main/java/tools/refinery/store/query/view/AnyRelationView.java
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/view/AnyRelationView.java
diff --git a/subprojects/store/src/main/java/tools/refinery/store/query/view/FilteredRelationView.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/view/FilteredRelationView.java
index 64c601bb..64c601bb 100644
--- a/subprojects/store/src/main/java/tools/refinery/store/query/view/FilteredRelationView.java
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/view/FilteredRelationView.java
diff --git a/subprojects/store/src/main/java/tools/refinery/store/query/view/FunctionalRelationView.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/view/FunctionalRelationView.java
index 3d278a8b..3d278a8b 100644
--- a/subprojects/store/src/main/java/tools/refinery/store/query/view/FunctionalRelationView.java
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/view/FunctionalRelationView.java
diff --git a/subprojects/store/src/main/java/tools/refinery/store/query/view/KeyOnlyRelationView.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/view/KeyOnlyRelationView.java
index e1b2e45b..e1b2e45b 100644
--- a/subprojects/store/src/main/java/tools/refinery/store/query/view/KeyOnlyRelationView.java
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/view/KeyOnlyRelationView.java
diff --git a/subprojects/store/src/main/java/tools/refinery/store/query/view/RelationView.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/view/RelationView.java
index 6accd27a..2714a8c5 100644
--- a/subprojects/store/src/main/java/tools/refinery/store/query/view/RelationView.java
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/view/RelationView.java
@@ -1,8 +1,8 @@
 package tools.refinery.store.query.view;
 
+import tools.refinery.store.query.Variable;
 import tools.refinery.store.map.CursorAsIterator;
 import tools.refinery.store.model.Model;
-import tools.refinery.store.query.Variable;
 import tools.refinery.store.query.literal.CallPolarity;
 import tools.refinery.store.query.literal.RelationViewLiteral;
 import tools.refinery.store.representation.Symbol;
diff --git a/subprojects/store/src/main/java/tools/refinery/store/query/view/RelationViewImplication.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/view/RelationViewImplication.java
index 2ba1fcc4..2ba1fcc4 100644
--- a/subprojects/store/src/main/java/tools/refinery/store/query/view/RelationViewImplication.java
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/view/RelationViewImplication.java
diff --git a/subprojects/store/src/main/java/tools/refinery/store/query/view/TuplePreservingRelationView.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/view/TuplePreservingRelationView.java
index 8cc4986e..8cc4986e 100644
--- a/subprojects/store/src/main/java/tools/refinery/store/query/view/TuplePreservingRelationView.java
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/view/TuplePreservingRelationView.java
diff --git a/subprojects/store/src/main/java/tools/refinery/store/partial/PartialInterpretationAdapter.java b/subprojects/store/src/main/java/tools/refinery/store/partial/PartialInterpretationAdapter.java
deleted file mode 100644
index 2c83a200..00000000
--- a/subprojects/store/src/main/java/tools/refinery/store/partial/PartialInterpretationAdapter.java
+++ /dev/null
@@ -1,9 +0,0 @@
-package tools.refinery.store.partial;
-
-import tools.refinery.store.adapter.ModelAdapter;
-
-public interface PartialInterpretationAdapter extends ModelAdapter {
-        @Override
-        PartialInterpretationStoreAdapter getStoreAdapter();
-}
-
diff --git a/subprojects/store/src/main/java/tools/refinery/store/partial/PartialInterpretationBuilder.java b/subprojects/store/src/main/java/tools/refinery/store/partial/PartialInterpretationBuilder.java
deleted file mode 100644
index 0ec13836..00000000
--- a/subprojects/store/src/main/java/tools/refinery/store/partial/PartialInterpretationBuilder.java
+++ /dev/null
@@ -1,9 +0,0 @@
-package tools.refinery.store.partial;
-
-import tools.refinery.store.adapter.ModelAdapterBuilder;
-import tools.refinery.store.model.ModelStore;
-
-public interface PartialInterpretationBuilder extends ModelAdapterBuilder {
-        @Override
-        PartialInterpretationStoreAdapter createStoreAdapter(ModelStore store);
-}
diff --git a/subprojects/store/src/main/java/tools/refinery/store/query/Dnf.java b/subprojects/store/src/main/java/tools/refinery/store/query/Dnf.java
deleted file mode 100644
index b080094f..00000000
--- a/subprojects/store/src/main/java/tools/refinery/store/query/Dnf.java
+++ /dev/null
@@ -1,187 +0,0 @@
-package tools.refinery.store.query;
-
-import tools.refinery.store.query.literal.CallPolarity;
-import tools.refinery.store.query.literal.DnfCallLiteral;
-import tools.refinery.store.query.literal.Literal;
-
-import java.util.*;
-
-public final class Dnf implements RelationLike {
-        private final String name;
-
-        private final String uniqueName;
-
-        private final List<Variable> parameters;
-
-        private final List<FunctionalDependency<Variable>> functionalDependencies;
-
-        private final List<DnfClause> clauses;
-
-        private Dnf(String name, List<Variable> parameters, List<FunctionalDependency<Variable>> functionalDependencies,
-                                List<DnfClause> clauses) {
-                validateFunctionalDependencies(parameters, functionalDependencies);
-                this.name = name;
-                this.uniqueName = DnfUtils.generateUniqueName(name);
-                this.parameters = parameters;
-                this.functionalDependencies = functionalDependencies;
-                this.clauses = clauses;
-        }
-
-        private static void validateFunctionalDependencies(
-                        Collection<Variable> parameters, Collection<FunctionalDependency<Variable>> functionalDependencies) {
-                var parameterSet = new HashSet<>(parameters);
-                for (var functionalDependency : functionalDependencies) {
-                        validateParameters(parameters, parameterSet, functionalDependency.forEach(), functionalDependency);
-                        validateParameters(parameters, parameterSet, functionalDependency.unique(), functionalDependency);
-                }
-        }
-
-        private static void validateParameters(Collection<Variable> parameters, Set<Variable> parameterSet,
-                                                                                   Collection<Variable> toValidate,
-                                                                                   FunctionalDependency<Variable> functionalDependency) {
-                for (var variable : toValidate) {
-                        if (!parameterSet.contains(variable)) {
-                                throw new IllegalArgumentException(
-                                                "Variable %s of functional dependency %s does not appear in the parameter list %s"
-                                                                .formatted(variable, functionalDependency, parameters));
-                        }
-                }
-        }
-
-        @Override
-        public String name() {
-                return name;
-        }
-
-        public String getUniqueName() {
-                return uniqueName;
-        }
-
-        public List<Variable> getParameters() {
-                return parameters;
-        }
-
-        public List<FunctionalDependency<Variable>> getFunctionalDependencies() {
-                return functionalDependencies;
-        }
-
-        @Override
-        public int arity() {
-                return parameters.size();
-        }
-
-        public List<DnfClause> getClauses() {
-                return clauses;
-        }
-
-        public DnfCallLiteral call(CallPolarity polarity, List<Variable> arguments) {
-                return new DnfCallLiteral(polarity, this, arguments);
-        }
-
-        public DnfCallLiteral call(CallPolarity polarity, Variable... arguments) {
-                return call(polarity, List.of(arguments));
-        }
-
-        public DnfCallLiteral call(Variable... arguments) {
-                return call(CallPolarity.POSITIVE, arguments);
-        }
-
-        public DnfCallLiteral callTransitive(Variable left, Variable right) {
-                return call(CallPolarity.TRANSITIVE, List.of(left, right));
-        }
-
-        public static Builder builder() {
-                return builder(null);
-        }
-
-        public static Builder builder(String name) {
-                return new Builder(name);
-        }
-
-        @SuppressWarnings("UnusedReturnValue")
-        public static class Builder {
-                private final String name;
-
-                private final List<Variable> parameters = new ArrayList<>();
-
-                private final List<FunctionalDependency<Variable>> functionalDependencies = new ArrayList<>();
-
-                private final List<List<Literal>> clauses = new ArrayList<>();
-
-                private Builder(String name) {
-                        this.name = name;
-                }
-
-                public Builder parameter(Variable variable) {
-                        parameters.add(variable);
-                        return this;
-                }
-
-                public Builder parameters(Variable... variables) {
-                        return parameters(List.of(variables));
-                }
-
-                public Builder parameters(Collection<Variable> variables) {
-                        parameters.addAll(variables);
-                        return this;
-                }
-
-                public Builder functionalDependencies(Collection<FunctionalDependency<Variable>> functionalDependencies) {
-                        this.functionalDependencies.addAll(functionalDependencies);
-                        return this;
-                }
-
-                public Builder functionalDependency(FunctionalDependency<Variable> functionalDependency) {
-                        functionalDependencies.add(functionalDependency);
-                        return this;
-                }
-
-                public Builder functionalDependency(Set<Variable> forEach, Set<Variable> unique) {
-                        return functionalDependency(new FunctionalDependency<>(forEach, unique));
-                }
-
-                public Builder clause(Literal... atoms) {
-                        clauses.add(List.of(atoms));
-                        return this;
-                }
-
-                public Builder clause(Collection<Literal> atoms) {
-                        clauses.add(List.copyOf(atoms));
-                        return this;
-                }
-
-                public Builder clause(DnfClause clause) {
-                        return clause(clause.literals());
-                }
-
-                public Builder clauses(DnfClause... clauses) {
-                        for (var clause : clauses) {
-                                this.clause(clause);
-                        }
-                        return this;
-                }
-
-                public Builder clauses(Collection<DnfClause> clauses) {
-                        for (var clause : clauses) {
-                                this.clause(clause);
-                        }
-                        return this;
-                }
-
-                public Dnf build() {
-                        var postProcessedClauses = new ArrayList<DnfClause>();
-                        for (var constraints : clauses) {
-                                var variables = new HashSet<Variable>();
-                                for (var constraint : constraints) {
-                                        constraint.collectAllVariables(variables);
-                                }
-                                parameters.forEach(variables::remove);
-                                postProcessedClauses.add(new DnfClause(Collections.unmodifiableSet(variables),
-                                                Collections.unmodifiableList(constraints)));
-                        }
-                        return new Dnf(name, Collections.unmodifiableList(parameters),
-                                        Collections.unmodifiableList(functionalDependencies),
-                                        Collections.unmodifiableList(postProcessedClauses));
-                }
-        }
-}