4 files changed, 46 insertions, 6 deletions

diff --git a/subprojects/store-partial/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 a49e0625..8c157187 100644
--- a/subprojects/store-partial/src/main/java/tools/refinery/store/partial/literal/ModalDnfCallLiteral.java
+++ b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/literal/ModalDnfCallLiteral.java
@@ -2,13 +2,14 @@ package tools.refinery.store.partial.literal;
 
 import tools.refinery.store.query.Dnf;
 import tools.refinery.store.query.Variable;
+import tools.refinery.store.query.equality.LiteralEqualityHelper;
 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 tools.refinery.store.query.substitution.Substitution;
 
 import java.util.List;
-import java.util.Map;
 
 public class ModalDnfCallLiteral extends ModalLiteral<Dnf> implements PolarLiteral<ModalDnfCallLiteral> {
         public ModalDnfCallLiteral(CallPolarity polarity, Modality modality, Dnf target, List<Variable> arguments) {
@@ -20,7 +21,17 @@ public class ModalDnfCallLiteral extends ModalLiteral<Dnf> implements PolarLiter
         }
 
         @Override
-        public ModalDnfCallLiteral substitute(Map<Variable, Variable> substitution) {
+        public Class<Dnf> getTargetType() {
+                return Dnf.class;
+        }
+
+        @Override
+        protected boolean targetEquals(LiteralEqualityHelper helper, Dnf otherTarget) {
+                return helper.dnfEqual(getTarget(), otherTarget);
+        }
+
+        @Override
+        public ModalDnfCallLiteral substitute(Substitution substitution) {
                 return new ModalDnfCallLiteral(getPolarity(), getModality(), getTarget(), substituteArguments(substitution));
         }
 
diff --git a/subprojects/store-partial/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..cebe9c9d 100644
--- a/subprojects/store-partial/src/main/java/tools/refinery/store/partial/literal/ModalLiteral.java
+++ b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/literal/ModalLiteral.java
@@ -2,8 +2,10 @@ package tools.refinery.store.partial.literal;
 
 import tools.refinery.store.query.RelationLike;
 import tools.refinery.store.query.Variable;
+import tools.refinery.store.query.equality.LiteralEqualityHelper;
 import tools.refinery.store.query.literal.CallLiteral;
 import tools.refinery.store.query.literal.CallPolarity;
+import tools.refinery.store.query.literal.Literal;
 
 import java.util.List;
 import java.util.Objects;
@@ -26,6 +28,22 @@ public abstract class ModalLiteral<T extends RelationLike> extends CallLiteral<T
         }
 
         @Override
+        public boolean equalsWithSubstitution(LiteralEqualityHelper helper, Literal other) {
+                if (!super.equalsWithSubstitution(helper, other)) {
+                        return false;
+                }
+                // If {@link CallLiteral#equalsWithSubstitution(LiteralEqualityHelper, Literal)} has returned {@code true},
+                // we must have the same dynamic type as {@code other}.
+                var otherModalLiteral = (ModalLiteral<?>) other;
+                return modality == otherModalLiteral.modality;
+        }
+
+        @Override
+        protected String targetToString() {
+                return "%s %s".formatted(modality, super.targetToString());
+        }
+
+        @Override
         public boolean equals(Object o) {
                 if (this == o) return true;
                 if (o == null || getClass() != o.getClass()) return false;
diff --git a/subprojects/store-partial/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..39054f22 100644
--- a/subprojects/store-partial/src/main/java/tools/refinery/store/partial/literal/ModalRelationLiteral.java
+++ b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/literal/ModalRelationLiteral.java
@@ -4,9 +4,9 @@ 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.PolarLiteral;
+import tools.refinery.store.query.substitution.Substitution;
 
 import java.util.List;
-import java.util.Map;
 
 public final class ModalRelationLiteral extends ModalLiteral<PartialRelation>
                 implements PolarLiteral<ModalRelationLiteral> {
@@ -15,12 +15,18 @@ public final class ModalRelationLiteral extends ModalLiteral<PartialRelation>
                 super(polarity, modality, target, arguments);
         }
 
+
         public ModalRelationLiteral(Modality modality, PartialRelationLiteral baseLiteral) {
                 super(modality, baseLiteral);
         }
 
         @Override
-        public ModalRelationLiteral substitute(Map<Variable, Variable> substitution) {
+        public Class<PartialRelation> getTargetType() {
+                return PartialRelation.class;
+        }
+
+        @Override
+        public ModalRelationLiteral substitute(Substitution substitution) {
                 return new ModalRelationLiteral(getPolarity(), getModality(), getTarget(), substituteArguments(substitution));
         }
 
diff --git a/subprojects/store-partial/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..b81d9a3d 100644
--- a/subprojects/store-partial/src/main/java/tools/refinery/store/partial/literal/PartialRelationLiteral.java
+++ b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/literal/PartialRelationLiteral.java
@@ -5,9 +5,9 @@ import tools.refinery.store.query.Variable;
 import tools.refinery.store.query.literal.CallLiteral;
 import tools.refinery.store.query.literal.CallPolarity;
 import tools.refinery.store.query.literal.PolarLiteral;
+import tools.refinery.store.query.substitution.Substitution;
 
 import java.util.List;
-import java.util.Map;
 
 public final class PartialRelationLiteral extends CallLiteral<PartialRelation>
                 implements PolarLiteral<PartialRelationLiteral> {
@@ -16,7 +16,12 @@ public final class PartialRelationLiteral extends CallLiteral<PartialRelation>
         }
 
         @Override
-        public PartialRelationLiteral substitute(Map<Variable, Variable> substitution) {
+        public Class<PartialRelation> getTargetType() {
+                return PartialRelation.class;
+        }
+
+        @Override
+        public PartialRelationLiteral substitute(Substitution substitution) {
                 return new PartialRelationLiteral(getPolarity(), getTarget(), substituteArguments(substitution));
         }