refactor: query equality and hash code

Allow computing hash codes up to the renaming of variables.

Also introduces CheckLiteral instead of AssumeLiteral for more straightforward
naming.

30 files changed, 388 insertions, 211 deletions

diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/dnf/ClausePostProcessor.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/dnf/ClausePostProcessor.java
index b5e7092b..1a45c20a 100644
--- a/subprojects/store-query/src/main/java/tools/refinery/store/query/dnf/ClausePostProcessor.java
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/dnf/ClausePostProcessor.java
@@ -67,13 +67,13 @@ class ClausePostProcessor {
                 for (var literal : literals) {
                         if (isPositiveEquivalence(literal)) {
                                 var equivalenceLiteral = (EquivalenceLiteral) literal;
-                                mergeVariables(equivalenceLiteral.left(), equivalenceLiteral.right());
+                                mergeVariables(equivalenceLiteral.getLeft(), equivalenceLiteral.getRight());
                         }
                 }
         }
 
         private static boolean isPositiveEquivalence(Literal literal) {
-                return literal instanceof EquivalenceLiteral equivalenceLiteral && equivalenceLiteral.positive();
+                return literal instanceof EquivalenceLiteral equivalenceLiteral && equivalenceLiteral.isPositive();
         }
 
         private void mergeVariables(NodeVariable left, NodeVariable right) {
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/dnf/Dnf.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/dnf/Dnf.java
index 50b245f7..7a3e2a1e 100644
--- a/subprojects/store-query/src/main/java/tools/refinery/store/query/dnf/Dnf.java
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/dnf/Dnf.java
@@ -6,9 +6,11 @@
 package tools.refinery.store.query.dnf;
 
 import tools.refinery.store.query.Constraint;
-import tools.refinery.store.query.literal.Reduction;
 import tools.refinery.store.query.equality.DnfEqualityChecker;
 import tools.refinery.store.query.equality.LiteralEqualityHelper;
+import tools.refinery.store.query.equality.SubstitutingLiteralEqualityHelper;
+import tools.refinery.store.query.equality.SubstitutingLiteralHashCodeHelper;
+import tools.refinery.store.query.literal.Reduction;
 import tools.refinery.store.query.term.Parameter;
 import tools.refinery.store.query.term.Variable;
 
@@ -129,7 +131,7 @@ public final class Dnf implements Constraint {
                         return false;
                 }
                 for (int i = 0; i < numClauses; i++) {
-                        var literalEqualityHelper = new LiteralEqualityHelper(callEqualityChecker, symbolicParameters,
+                        var literalEqualityHelper = new SubstitutingLiteralEqualityHelper(callEqualityChecker, symbolicParameters,
                                         other.symbolicParameters);
                         if (!clauses.get(i).equalsWithSubstitution(literalEqualityHelper, other.clauses.get(i))) {
                                 return false;
@@ -146,6 +148,18 @@ public final class Dnf implements Constraint {
                 return false;
         }
 
+        public int hashCodeWithSubstitution() {
+                var helper = new SubstitutingLiteralHashCodeHelper();
+                int result = 0;
+                for (var symbolicParameter : symbolicParameters) {
+                        result = result * 31 + symbolicParameter.hashCodeWithSubstitution(helper);
+                }
+                for (var clause : clauses) {
+                        result = result * 31 + clause.hashCodeWithSubstitution(helper);
+                }
+                return result;
+        }
+
         @Override
         public String toString() {
                 return "%s/%d".formatted(name(), arity());
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/dnf/DnfClause.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/dnf/DnfClause.java
index fdd0d47c..94327bad 100644
--- a/subprojects/store-query/src/main/java/tools/refinery/store/query/dnf/DnfClause.java
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/dnf/DnfClause.java
@@ -6,6 +6,7 @@
 package tools.refinery.store.query.dnf;
 
 import tools.refinery.store.query.equality.LiteralEqualityHelper;
+import tools.refinery.store.query.equality.LiteralHashCodeHelper;
 import tools.refinery.store.query.literal.Literal;
 import tools.refinery.store.query.term.Variable;
 
@@ -25,4 +26,12 @@ public record DnfClause(Set<Variable> positiveVariables, List<Literal> literals)
                 }
                 return true;
         }
+
+        public int hashCodeWithSubstitution(LiteralHashCodeHelper helper) {
+                int result = 0;
+                for (var literal : literals) {
+                        result = result * 31 + literal.hashCodeWithSubstitution(helper);
+                }
+                return result;
+        }
 }
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/dnf/SymbolicParameter.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/dnf/SymbolicParameter.java
index e0d3ba1f..1e96cf27 100644
--- a/subprojects/store-query/src/main/java/tools/refinery/store/query/dnf/SymbolicParameter.java
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/dnf/SymbolicParameter.java
@@ -5,6 +5,7 @@
  */
 package tools.refinery.store.query.dnf;
 
+import tools.refinery.store.query.equality.LiteralHashCodeHelper;
 import tools.refinery.store.query.term.Parameter;
 import tools.refinery.store.query.term.ParameterDirection;
 import tools.refinery.store.query.term.Variable;
@@ -27,6 +28,10 @@ public final class SymbolicParameter extends Parameter {
                 return variable.isUnifiable();
         }
 
+        public int hashCodeWithSubstitution(LiteralHashCodeHelper helper) {
+                return Objects.hash(super.hashCode(), helper.getVariableHashCode(variable));
+        }
+
         @Override
         public String toString() {
                 var direction = getDirection();
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/equality/DeepDnfEqualityChecker.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/equality/DeepDnfEqualityChecker.java
index 1eeb5723..a212b3f5 100644
--- a/subprojects/store-query/src/main/java/tools/refinery/store/query/equality/DeepDnfEqualityChecker.java
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/equality/DeepDnfEqualityChecker.java
@@ -38,7 +38,7 @@ public class DeepDnfEqualityChecker implements DnfEqualityChecker {
                         return false;
                 }
                 for (int i = 0; i < numClauses; i++) {
-                        var literalEqualityHelper = new LiteralEqualityHelper(this, symbolicParameters,
+                        var literalEqualityHelper = new SubstitutingLiteralEqualityHelper(this, symbolicParameters,
                                         other.getSymbolicParameters());
                         if (!equalsWithSubstitutionRaw(literalEqualityHelper, clauses.get(i), other.getClauses().get(i))) {
                                 return false;
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/equality/DnfEqualityChecker.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/equality/DnfEqualityChecker.java
index 4a8bee3b..e2cfd79b 100644
--- a/subprojects/store-query/src/main/java/tools/refinery/store/query/equality/DnfEqualityChecker.java
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/equality/DnfEqualityChecker.java
@@ -7,7 +7,11 @@ package tools.refinery.store.query.equality;
 
 import tools.refinery.store.query.dnf.Dnf;
 
+import java.util.Objects;
+
 @FunctionalInterface
 public interface DnfEqualityChecker {
+        DnfEqualityChecker DEFAULT = Objects::equals;
+
         boolean dnfEqual(Dnf left, Dnf right);
 }
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/equality/LiteralEqualityHelper.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/equality/LiteralEqualityHelper.java
index 9315fb30..5abc76ce 100644
--- a/subprojects/store-query/src/main/java/tools/refinery/store/query/equality/LiteralEqualityHelper.java
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/equality/LiteralEqualityHelper.java
@@ -6,49 +6,22 @@
 package tools.refinery.store.query.equality;
 
 import tools.refinery.store.query.dnf.Dnf;
-import tools.refinery.store.query.dnf.SymbolicParameter;
 import tools.refinery.store.query.term.Variable;
 
-import java.util.HashMap;
-import java.util.List;
-import java.util.Map;
+import java.util.Objects;
 
-public class LiteralEqualityHelper {
-        private final DnfEqualityChecker dnfEqualityChecker;
-        private final Map<Variable, Variable> leftToRight;
-        private final Map<Variable, Variable> rightToLeft;
-
-        public LiteralEqualityHelper(DnfEqualityChecker dnfEqualityChecker, List<SymbolicParameter> leftParameters,
-                                                                 List<SymbolicParameter> rightParameters) {
-                this.dnfEqualityChecker = dnfEqualityChecker;
-                var arity = leftParameters.size();
-                if (arity != rightParameters.size()) {
-                        throw new IllegalArgumentException("Parameter lists have unequal length");
-                }
-                leftToRight = new HashMap<>(arity);
-                rightToLeft = new HashMap<>(arity);
-                for (int i = 0; i < arity; i++) {
-                        if (!variableEqual(leftParameters.get(i).getVariable(), rightParameters.get(i).getVariable())) {
-                                throw new IllegalArgumentException("Parameter lists cannot be unified: duplicate parameter " + i);
-                        }
+public interface LiteralEqualityHelper extends DnfEqualityChecker {
+        LiteralEqualityHelper DEFAULT = new LiteralEqualityHelper() {
+                @Override
+                public boolean variableEqual(Variable left, Variable right) {
+                        return Objects.equals(left, right);
                 }
-        }
-
-        public boolean dnfEqual(Dnf left, Dnf right) {
-                return dnfEqualityChecker.dnfEqual(left, right);
-        }
 
-        public boolean variableEqual(Variable left, Variable right) {
-                if (checkMapping(leftToRight, left, right) && checkMapping(rightToLeft, right, left)) {
-                        leftToRight.put(left, right);
-                        rightToLeft.put(right, left);
-                        return true;
+                @Override
+                public boolean dnfEqual(Dnf left, Dnf right) {
+                        return DnfEqualityChecker.DEFAULT.dnfEqual(left, right);
                 }
-                return false;
-        }
+        };
 
-        private static boolean checkMapping(Map<Variable, Variable> map, Variable key, Variable expectedValue) {
-                var currentValue = map.get(key);
-                return currentValue == null || currentValue.equals(expectedValue);
-        }
+        boolean variableEqual(Variable left, Variable right);
 }
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/equality/LiteralHashCodeHelper.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/equality/LiteralHashCodeHelper.java
new file mode 100644
index 00000000..5495160a
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/equality/LiteralHashCodeHelper.java
@@ -0,0 +1,17 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.query.equality;
+
+import tools.refinery.store.query.term.Variable;
+
+import java.util.Objects;
+
+@FunctionalInterface
+public interface LiteralHashCodeHelper {
+        LiteralHashCodeHelper DEFAULT = Objects::hashCode;
+
+        int getVariableHashCode(Variable variable);
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/equality/SubstitutingLiteralEqualityHelper.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/equality/SubstitutingLiteralEqualityHelper.java
new file mode 100644
index 00000000..50a79e07
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/equality/SubstitutingLiteralEqualityHelper.java
@@ -0,0 +1,59 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.query.equality;
+
+import tools.refinery.store.query.dnf.Dnf;
+import tools.refinery.store.query.dnf.SymbolicParameter;
+import tools.refinery.store.query.term.Variable;
+
+import java.util.HashMap;
+import java.util.List;
+import java.util.Map;
+
+public class SubstitutingLiteralEqualityHelper implements LiteralEqualityHelper {
+        private final DnfEqualityChecker dnfEqualityChecker;
+        private final Map<Variable, Variable> leftToRight;
+        private final Map<Variable, Variable> rightToLeft;
+
+        public SubstitutingLiteralEqualityHelper(DnfEqualityChecker dnfEqualityChecker,
+                                                                                         List<SymbolicParameter> leftParameters,
+                                                                                         List<SymbolicParameter> rightParameters) {
+                this.dnfEqualityChecker = dnfEqualityChecker;
+                var arity = leftParameters.size();
+                if (arity != rightParameters.size()) {
+                        throw new IllegalArgumentException("Parameter lists have unequal length");
+                }
+                leftToRight = new HashMap<>(arity);
+                rightToLeft = new HashMap<>(arity);
+                for (int i = 0; i < arity; i++) {
+                        if (!variableEqual(leftParameters.get(i).getVariable(), rightParameters.get(i).getVariable())) {
+                                throw new IllegalArgumentException("Parameter lists cannot be unified: duplicate parameter " + i);
+                        }
+                }
+        }
+
+        @Override
+        public boolean dnfEqual(Dnf left, Dnf right) {
+                return dnfEqualityChecker.dnfEqual(left, right);
+        }
+
+        @Override
+        public boolean variableEqual(Variable left, Variable right) {
+                if (left.tryGetType().equals(right.tryGetType()) &&
+                                checkMapping(leftToRight, left, right) &&
+                                checkMapping(rightToLeft, right, left)) {
+                        leftToRight.put(left, right);
+                        rightToLeft.put(right, left);
+                        return true;
+                }
+                return false;
+        }
+
+        private static boolean checkMapping(Map<Variable, Variable> map, Variable key, Variable expectedValue) {
+                var currentValue = map.get(key);
+                return currentValue == null || currentValue.equals(expectedValue);
+        }
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/equality/SubstitutingLiteralHashCodeHelper.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/equality/SubstitutingLiteralHashCodeHelper.java
new file mode 100644
index 00000000..a40ecd58
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/equality/SubstitutingLiteralHashCodeHelper.java
@@ -0,0 +1,30 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.query.equality;
+
+import tools.refinery.store.query.term.Variable;
+
+import java.util.LinkedHashMap;
+import java.util.Map;
+
+public class SubstitutingLiteralHashCodeHelper implements LiteralHashCodeHelper {
+        private final Map<Variable, Integer> assignedHashCodes = new LinkedHashMap<>();
+
+        // 0 is for {@code null}, so we start with 1.
+        private int next = 1;
+
+        @Override
+        public int getVariableHashCode(Variable variable) {
+                if (variable == null) {
+                        return 0;
+                }
+                return assignedHashCodes.computeIfAbsent(variable, key -> {
+                        int sequenceNumber = next;
+                        next++;
+                        return variable.hashCodeWithSubstitution(sequenceNumber);
+                });
+        }
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/AbstractCallLiteral.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/AbstractCallLiteral.java
index 8ef8e8b4..a355dc3b 100644
--- a/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/AbstractCallLiteral.java
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/AbstractCallLiteral.java
@@ -7,13 +7,14 @@ package tools.refinery.store.query.literal;
 
 import tools.refinery.store.query.Constraint;
 import tools.refinery.store.query.equality.LiteralEqualityHelper;
+import tools.refinery.store.query.equality.LiteralHashCodeHelper;
 import tools.refinery.store.query.substitution.Substitution;
 import tools.refinery.store.query.term.ParameterDirection;
 import tools.refinery.store.query.term.Variable;
 
 import java.util.*;
 
-public abstract class AbstractCallLiteral implements Literal {
+public abstract class AbstractCallLiteral extends AbstractLiteral {
         private final Constraint target;
         private final List<Variable> arguments;
         private final Set<Variable> inArguments;
@@ -112,7 +113,7 @@ public abstract class AbstractCallLiteral implements Literal {
 
         @Override
         public boolean equalsWithSubstitution(LiteralEqualityHelper helper, Literal other) {
-                if (other == null || getClass() != other.getClass()) {
+                if (!super.equalsWithSubstitution(helper, other)) {
                         return false;
                 }
                 var otherCallLiteral = (AbstractCallLiteral) other;
@@ -129,15 +130,11 @@ public abstract class AbstractCallLiteral implements Literal {
         }
 
         @Override
-        public boolean equals(Object o) {
-                if (this == o) return true;
-                if (o == null || getClass() != o.getClass()) return false;
-                AbstractCallLiteral that = (AbstractCallLiteral) o;
-                return target.equals(that.target) && arguments.equals(that.arguments);
-        }
-
-        @Override
-        public int hashCode() {
-                return Objects.hash(getClass(), target, arguments);
+        public int hashCodeWithSubstitution(LiteralHashCodeHelper helper) {
+                int result = super.hashCodeWithSubstitution(helper) * 31 + target.hashCode();
+                for (var argument : arguments) {
+                        result = result * 31 + helper.getVariableHashCode(argument);
+                }
+                return result;
         }
 }
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/AbstractLiteral.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/AbstractLiteral.java
new file mode 100644
index 00000000..7d3cabd7
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/AbstractLiteral.java
@@ -0,0 +1,34 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.query.literal;
+
+import tools.refinery.store.query.equality.LiteralEqualityHelper;
+import tools.refinery.store.query.equality.LiteralHashCodeHelper;
+
+public abstract class AbstractLiteral implements Literal {
+        @Override
+        public boolean equalsWithSubstitution(LiteralEqualityHelper helper, Literal other) {
+                return other != null && getClass() == other.getClass();
+        }
+
+        @Override
+        public int hashCodeWithSubstitution(LiteralHashCodeHelper helper) {
+                return getClass().hashCode();
+        }
+
+        @Override
+        public boolean equals(Object o) {
+                if (this == o) return true;
+                if (o == null || getClass() != o.getClass()) return false;
+                AbstractLiteral that = (AbstractLiteral) o;
+                return equalsWithSubstitution(LiteralEqualityHelper.DEFAULT, that);
+        }
+
+        @Override
+        public int hashCode() {
+                return hashCodeWithSubstitution(LiteralHashCodeHelper.DEFAULT);
+        }
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/AggregationLiteral.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/AggregationLiteral.java
index 3a5eb5c7..615fd493 100644
--- a/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/AggregationLiteral.java
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/AggregationLiteral.java
@@ -7,6 +7,7 @@ package tools.refinery.store.query.literal;
 
 import tools.refinery.store.query.Constraint;
 import tools.refinery.store.query.equality.LiteralEqualityHelper;
+import tools.refinery.store.query.equality.LiteralHashCodeHelper;
 import tools.refinery.store.query.substitution.Substitution;
 import tools.refinery.store.query.term.*;
 
@@ -14,6 +15,8 @@ import java.util.List;
 import java.util.Objects;
 import java.util.Set;
 
+// {@link Object#equals(Object)} is implemented by {@link AbstractLiteral}.
+@SuppressWarnings("squid:S2160")
 public class AggregationLiteral<R, T> extends AbstractCallLiteral {
         private final DataVariable<R> resultVariable;
         private final DataVariable<T> inputVariable;
@@ -100,18 +103,9 @@ public class AggregationLiteral<R, T> extends AbstractCallLiteral {
         }
 
         @Override
-        public boolean equals(Object o) {
-                if (this == o) return true;
-                if (o == null || getClass() != o.getClass()) return false;
-                if (!super.equals(o)) return false;
-                AggregationLiteral<?, ?> that = (AggregationLiteral<?, ?>) o;
-                return resultVariable.equals(that.resultVariable) && inputVariable.equals(that.inputVariable) &&
-                                aggregator.equals(that.aggregator);
-        }
-
-        @Override
-        public int hashCode() {
-                return Objects.hash(super.hashCode(), resultVariable, inputVariable, aggregator);
+        public int hashCodeWithSubstitution(LiteralHashCodeHelper helper) {
+                return Objects.hash(super.hashCodeWithSubstitution(helper), helper.getVariableHashCode(resultVariable),
+                                helper.getVariableHashCode(inputVariable), aggregator);
         }
 
         @Override
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/AssignLiteral.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/AssignLiteral.java
index dbf999a2..d8a4b494 100644
--- a/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/AssignLiteral.java
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/AssignLiteral.java
@@ -6,6 +6,7 @@
 package tools.refinery.store.query.literal;
 
 import tools.refinery.store.query.equality.LiteralEqualityHelper;
+import tools.refinery.store.query.equality.LiteralHashCodeHelper;
 import tools.refinery.store.query.substitution.Substitution;
 import tools.refinery.store.query.term.DataVariable;
 import tools.refinery.store.query.term.Term;
@@ -15,8 +16,11 @@ import java.util.Collections;
 import java.util.Objects;
 import java.util.Set;
 
-public record AssignLiteral<T>(DataVariable<T> variable, Term<T> term) implements Literal {
-        public AssignLiteral {
+public class AssignLiteral<T> extends AbstractLiteral {
+        private final DataVariable<T> variable;
+        private final Term<T> term;
+
+        public AssignLiteral(DataVariable<T> variable, Term<T> term) {
                 if (!term.getType().equals(variable.getType())) {
                         throw new IllegalArgumentException("Term %s must be of type %s, got %s instead".formatted(
                                         term, variable.getType().getName(), term.getType().getName()));
@@ -26,6 +30,16 @@ public record AssignLiteral<T>(DataVariable<T> variable, Term<T> term) implement
                         throw new IllegalArgumentException("Result variable %s must not appear in the term %s".formatted(
                                         variable, term));
                 }
+                this.variable = variable;
+                this.term = term;
+        }
+
+        public DataVariable<T> getVariable() {
+                return variable;
+        }
+
+        public Term<T> getTerm() {
+                return term;
         }
 
         @Override
@@ -53,27 +67,19 @@ public record AssignLiteral<T>(DataVariable<T> variable, Term<T> term) implement
                 if (other == null || getClass() != other.getClass()) {
                         return false;
                 }
-                var otherLetLiteral = (AssignLiteral<?>) other;
-                return helper.variableEqual(variable, otherLetLiteral.variable) && term.equalsWithSubstitution(helper,
-                                otherLetLiteral.term);
-        }
-
-        @Override
-        public String toString() {
-                return "%s is (%s)".formatted(variable, term);
+                var otherAssignLiteral = (AssignLiteral<?>) other;
+                return helper.variableEqual(variable, otherAssignLiteral.variable) &&
+                                term.equalsWithSubstitution(helper, otherAssignLiteral.term);
         }
 
         @Override
-        public boolean equals(Object obj) {
-                if (obj == this) return true;
-                if (obj == null || obj.getClass() != this.getClass()) return false;
-                var that = (AssignLiteral<?>) obj;
-                return Objects.equals(this.variable, that.variable) &&
-                                Objects.equals(this.term, that.term);
+        public int hashCodeWithSubstitution(LiteralHashCodeHelper helper) {
+                return Objects.hash(super.hashCodeWithSubstitution(helper), helper.getVariableHashCode(variable),
+                                term.hashCodeWithSubstitution(helper));
         }
 
         @Override
-        public int hashCode() {
-                return Objects.hash(getClass(), variable, term);
+        public String toString() {
+                return "%s is (%s)".formatted(variable, term);
         }
 }
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
index f312d202..6cd320da 100644
--- 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
@@ -6,6 +6,7 @@
 package tools.refinery.store.query.literal;
 
 import tools.refinery.store.query.equality.LiteralEqualityHelper;
+import tools.refinery.store.query.equality.LiteralHashCodeHelper;
 import tools.refinery.store.query.substitution.Substitution;
 import tools.refinery.store.query.term.Variable;
 
@@ -53,6 +54,11 @@ public enum BooleanLiteral implements CanNegate<BooleanLiteral> {
         }
 
         @Override
+        public int hashCodeWithSubstitution(LiteralHashCodeHelper helper) {
+                return hashCode();
+        }
+
+        @Override
         public String toString() {
                 return Boolean.toString(value);
         }
diff --git a/subprojects/store-query/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 29772aee..a311dada 100644
--- a/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/CallLiteral.java
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/CallLiteral.java
@@ -7,12 +7,15 @@ package tools.refinery.store.query.literal;
 
 import tools.refinery.store.query.Constraint;
 import tools.refinery.store.query.equality.LiteralEqualityHelper;
+import tools.refinery.store.query.equality.LiteralHashCodeHelper;
 import tools.refinery.store.query.substitution.Substitution;
 import tools.refinery.store.query.term.ParameterDirection;
 import tools.refinery.store.query.term.Variable;
 
 import java.util.*;
 
+// {@link Object#equals(Object)} is implemented by {@link AbstractLiteral}.
+@SuppressWarnings("squid:S2160")
 public final class CallLiteral extends AbstractCallLiteral implements CanNegate<CallLiteral> {
         private final CallPolarity polarity;
 
@@ -85,22 +88,13 @@ public final class CallLiteral extends AbstractCallLiteral implements CanNegate<
         }
 
         @Override
-        public CallLiteral negate() {
-                return new CallLiteral(polarity.negate(), getTarget(), getArguments());
+        public int hashCodeWithSubstitution(LiteralHashCodeHelper helper) {
+                return Objects.hash(super.hashCodeWithSubstitution(helper), polarity);
         }
 
         @Override
-        public boolean equals(Object o) {
-                if (this == o) return true;
-                if (o == null || getClass() != o.getClass()) return false;
-                if (!super.equals(o)) return false;
-                CallLiteral that = (CallLiteral) o;
-                return polarity == that.polarity;
-        }
-
-        @Override
-        public int hashCode() {
-                return Objects.hash(super.hashCode(), polarity);
+        public CallLiteral negate() {
+                return new CallLiteral(polarity.negate(), getTarget(), getArguments());
         }
 
         @Override
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/AssumeLiteral.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/CheckLiteral.java
index 1ca04c77..1271183a 100644
--- a/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/AssumeLiteral.java
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/CheckLiteral.java
@@ -6,21 +6,31 @@
 package tools.refinery.store.query.literal;
 
 import tools.refinery.store.query.equality.LiteralEqualityHelper;
+import tools.refinery.store.query.equality.LiteralHashCodeHelper;
 import tools.refinery.store.query.substitution.Substitution;
 import tools.refinery.store.query.term.ConstantTerm;
 import tools.refinery.store.query.term.Term;
 import tools.refinery.store.query.term.Variable;
+import tools.refinery.store.query.term.bool.BoolNotTerm;
+import tools.refinery.store.query.term.bool.BoolTerms;
 
 import java.util.Collections;
 import java.util.Objects;
 import java.util.Set;
 
-public record AssumeLiteral(Term<Boolean> term) implements Literal {
-        public AssumeLiteral {
+public class CheckLiteral extends AbstractLiteral implements CanNegate<CheckLiteral> {
+        private final Term<Boolean> term;
+
+        public CheckLiteral(Term<Boolean> term) {
                 if (!term.getType().equals(Boolean.class)) {
                         throw new IllegalArgumentException("Term %s must be of type %s, got %s instead".formatted(
                                         term, Boolean.class.getName(), term.getType().getName()));
                 }
+                this.term = term;
+        }
+
+        public Term<Boolean> getTerm() {
+                return term;
         }
 
         @Override
@@ -38,10 +48,17 @@ public record AssumeLiteral(Term<Boolean> term) implements Literal {
                 return Set.of();
         }
 
-
         @Override
         public Literal substitute(Substitution substitution) {
-                return new AssumeLiteral(term.substitute(substitution));
+                return new CheckLiteral(term.substitute(substitution));
+        }
+
+        @Override
+        public CheckLiteral negate() {
+                if (term instanceof BoolNotTerm notTerm) {
+                        return new CheckLiteral(notTerm.getBody());
+                }
+                return new CheckLiteral(BoolTerms.not(term));
         }
 
         @Override
@@ -49,11 +66,16 @@ public record AssumeLiteral(Term<Boolean> term) implements Literal {
                 if (other == null || getClass() != other.getClass()) {
                         return false;
                 }
-                var otherAssumeLiteral = (AssumeLiteral) other;
+                var otherAssumeLiteral = (CheckLiteral) other;
                 return term.equalsWithSubstitution(helper, otherAssumeLiteral.term);
         }
 
         @Override
+        public int hashCodeWithSubstitution(LiteralHashCodeHelper helper) {
+                return Objects.hash(super.hashCodeWithSubstitution(helper), term.hashCodeWithSubstitution(helper));
+        }
+
+        @Override
         public Literal reduce() {
                 if (term instanceof ConstantTerm<Boolean> constantTerm) {
                         // Return {@link BooleanLiteral#FALSE} for {@code false} or {@code null} literals.
@@ -67,17 +89,4 @@ public record AssumeLiteral(Term<Boolean> term) implements Literal {
         public String toString() {
                 return "(%s)".formatted(term);
         }
-
-        @Override
-        public boolean equals(Object obj) {
-                if (obj == this) return true;
-                if (obj == null || obj.getClass() != this.getClass()) return false;
-                var that = (AssumeLiteral) obj;
-                return Objects.equals(this.term, that.term);
-        }
-
-        @Override
-        public int hashCode() {
-                return Objects.hash(getClass(), term);
-        }
 }
diff --git a/subprojects/store-query/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 73545620..d83bd584 100644
--- a/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/ConstantLiteral.java
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/ConstantLiteral.java
@@ -6,6 +6,7 @@
 package tools.refinery.store.query.literal;
 
 import tools.refinery.store.query.equality.LiteralEqualityHelper;
+import tools.refinery.store.query.equality.LiteralHashCodeHelper;
 import tools.refinery.store.query.substitution.Substitution;
 import tools.refinery.store.query.term.NodeVariable;
 import tools.refinery.store.query.term.Variable;
@@ -13,7 +14,24 @@ import tools.refinery.store.query.term.Variable;
 import java.util.Objects;
 import java.util.Set;
 
-public record ConstantLiteral(NodeVariable variable, int nodeId) implements Literal {
+public class ConstantLiteral extends AbstractLiteral {
+        private final NodeVariable variable;
+        private final int nodeId;
+
+        public ConstantLiteral(NodeVariable variable, int nodeId) {
+                this.variable = variable;
+                this.nodeId = nodeId;
+        }
+
+        public NodeVariable getVariable() {
+                return variable;
+        }
+
+        public int getNodeId() {
+                return nodeId;
+        }
+
+
         @Override
         public Set<Variable> getOutputVariables() {
                 return Set.of(variable);
@@ -43,23 +61,13 @@ public record ConstantLiteral(NodeVariable variable, int nodeId) implements Lite
                 return helper.variableEqual(variable, otherConstantLiteral.variable) && nodeId == otherConstantLiteral.nodeId;
         }
 
-
-        @Override
-        public String toString() {
-                return "%s === @Constant %d".formatted(variable, nodeId);
-        }
-
         @Override
-        public boolean equals(Object obj) {
-                if (obj == this) return true;
-                if (obj == null || obj.getClass() != this.getClass()) return false;
-                var that = (ConstantLiteral) obj;
-                return Objects.equals(this.variable, that.variable) &&
-                                this.nodeId == that.nodeId;
+        public int hashCodeWithSubstitution(LiteralHashCodeHelper helper) {
+                return Objects.hash(super.hashCodeWithSubstitution(helper), helper.getVariableHashCode(variable), nodeId);
         }
 
         @Override
-        public int hashCode() {
-                return Objects.hash(getClass(), variable, nodeId);
+        public String toString() {
+                return "%s === @Constant %d".formatted(variable, nodeId);
         }
 }
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/CountLiteral.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/CountLiteral.java
index 4d4749c8..ac4b8788 100644
--- a/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/CountLiteral.java
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/CountLiteral.java
@@ -7,6 +7,7 @@ package tools.refinery.store.query.literal;
 
 import tools.refinery.store.query.Constraint;
 import tools.refinery.store.query.equality.LiteralEqualityHelper;
+import tools.refinery.store.query.equality.LiteralHashCodeHelper;
 import tools.refinery.store.query.substitution.Substitution;
 import tools.refinery.store.query.term.DataVariable;
 import tools.refinery.store.query.term.Variable;
@@ -16,6 +17,8 @@ import java.util.List;
 import java.util.Objects;
 import java.util.Set;
 
+// {@link Object#equals(Object)} is implemented by {@link AbstractLiteral}.
+@SuppressWarnings("squid:S2160")
 public class CountLiteral extends AbstractCallLiteral {
         private final DataVariable<Integer> resultVariable;
 
@@ -68,17 +71,8 @@ public class CountLiteral extends AbstractCallLiteral {
         }
 
         @Override
-        public boolean equals(Object o) {
-                if (this == o) return true;
-                if (o == null || getClass() != o.getClass()) return false;
-                if (!super.equals(o)) return false;
-                CountLiteral that = (CountLiteral) o;
-                return resultVariable.equals(that.resultVariable);
-        }
-
-        @Override
-        public int hashCode() {
-                return Objects.hash(super.hashCode(), resultVariable);
+        public int hashCodeWithSubstitution(LiteralHashCodeHelper helper) {
+                return Objects.hash(super.hashCodeWithSubstitution(helper), helper.getVariableHashCode(resultVariable));
         }
 
         @Override
diff --git a/subprojects/store-query/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 28ba7625..61b7344f 100644
--- a/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/EquivalenceLiteral.java
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/EquivalenceLiteral.java
@@ -6,6 +6,7 @@
 package tools.refinery.store.query.literal;
 
 import tools.refinery.store.query.equality.LiteralEqualityHelper;
+import tools.refinery.store.query.equality.LiteralHashCodeHelper;
 import tools.refinery.store.query.substitution.Substitution;
 import tools.refinery.store.query.term.NodeVariable;
 import tools.refinery.store.query.term.Variable;
@@ -13,8 +14,29 @@ import tools.refinery.store.query.term.Variable;
 import java.util.Objects;
 import java.util.Set;
 
-public record EquivalenceLiteral(boolean positive, NodeVariable left, NodeVariable right)
-                implements CanNegate<EquivalenceLiteral> {
+public final class EquivalenceLiteral extends AbstractLiteral implements CanNegate<EquivalenceLiteral> {
+        private final boolean positive;
+        private final NodeVariable left;
+        private final NodeVariable right;
+
+        public EquivalenceLiteral(boolean positive, NodeVariable left, NodeVariable right) {
+                this.positive = positive;
+                this.left = left;
+                this.right = right;
+        }
+
+        public boolean isPositive() {
+                return positive;
+        }
+
+        public NodeVariable getLeft() {
+                return left;
+        }
+
+        public NodeVariable getRight() {
+                return right;
+        }
+
         @Override
         public Set<Variable> getOutputVariables() {
                 return Set.of(left);
@@ -55,27 +77,18 @@ public record EquivalenceLiteral(boolean positive, NodeVariable left, NodeVariab
                         return false;
                 }
                 var otherEquivalenceLiteral = (EquivalenceLiteral) other;
-                return helper.variableEqual(left, otherEquivalenceLiteral.left) && helper.variableEqual(right,
-                                otherEquivalenceLiteral.right);
-        }
-
-        @Override
-        public String toString() {
-                return "%s %s %s".formatted(left, positive ? "===" : "!==", right);
+                return helper.variableEqual(left, otherEquivalenceLiteral.left) &&
+                                helper.variableEqual(right, otherEquivalenceLiteral.right);
         }
 
         @Override
-        public boolean equals(Object obj) {
-                if (obj == this) return true;
-                if (obj == null || obj.getClass() != this.getClass()) return false;
-                var that = (EquivalenceLiteral) obj;
-                return this.positive == that.positive &&
-                                Objects.equals(this.left, that.left) &&
-                                Objects.equals(this.right, that.right);
+        public int hashCodeWithSubstitution(LiteralHashCodeHelper helper) {
+                return Objects.hash(super.hashCodeWithSubstitution(helper), helper.getVariableHashCode(left),
+                                helper.getVariableHashCode(right));
         }
 
         @Override
-        public int hashCode() {
-                return Objects.hash(getClass(), positive, left, right);
+        public String toString() {
+                return "%s %s %s".formatted(left, positive ? "===" : "!==", right);
         }
 }
diff --git a/subprojects/store-query/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 ce6c11fe..cb16ab00 100644
--- a/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/Literal.java
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/Literal.java
@@ -6,6 +6,7 @@
 package tools.refinery.store.query.literal;
 
 import tools.refinery.store.query.equality.LiteralEqualityHelper;
+import tools.refinery.store.query.equality.LiteralHashCodeHelper;
 import tools.refinery.store.query.substitution.Substitution;
 import tools.refinery.store.query.term.Variable;
 
@@ -26,4 +27,6 @@ public interface Literal {
 
         @SuppressWarnings("BooleanMethodIsAlwaysInverted")
         boolean equalsWithSubstitution(LiteralEqualityHelper helper, Literal other);
+
+        int hashCodeWithSubstitution(LiteralHashCodeHelper helper);
 }
diff --git a/subprojects/store-query/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 b3a87811..6056da45 100644
--- a/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/Literals.java
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/Literals.java
@@ -16,7 +16,7 @@ public final class Literals {
                 return literal.negate();
         }
 
-        public static AssumeLiteral assume(Term<Boolean> term) {
-                return new AssumeLiteral(term);
+        public static CheckLiteral check(Term<Boolean> term) {
+                return new CheckLiteral(term);
         }
 }
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/AbstractTerm.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/AbstractTerm.java
index d0ae3c12..5cecc35b 100644
--- a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/AbstractTerm.java
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/AbstractTerm.java
@@ -6,6 +6,7 @@
 package tools.refinery.store.query.term;
 
 import tools.refinery.store.query.equality.LiteralEqualityHelper;
+import tools.refinery.store.query.equality.LiteralHashCodeHelper;
 
 import java.util.Objects;
 
@@ -17,13 +18,18 @@ public abstract class AbstractTerm<T> implements Term<T> {
         }
 
         @Override
+        public Class<T> getType() {
+                return type;
+        }
+
+        @Override
         public boolean equalsWithSubstitution(LiteralEqualityHelper helper, AnyTerm other) {
-                return getClass().equals(other.getClass()) && type.equals(other.getType());
+                return other != null && getClass() == other.getClass() && type.equals(other.getType());
         }
 
         @Override
-        public Class<T> getType() {
-                return type;
+        public int hashCodeWithSubstitution(LiteralHashCodeHelper helper) {
+                return Objects.hash(getClass(), type);
         }
 
         @Override
@@ -31,11 +37,11 @@ public abstract class AbstractTerm<T> implements Term<T> {
                 if (this == o) return true;
                 if (o == null || getClass() != o.getClass()) return false;
                 AbstractTerm<?> that = (AbstractTerm<?>) o;
-                return type.equals(that.type);
+                return equalsWithSubstitution(LiteralEqualityHelper.DEFAULT, that);
         }
 
         @Override
         public int hashCode() {
-                return Objects.hash(getClass(), type);
+                return hashCodeWithSubstitution(LiteralHashCodeHelper.DEFAULT);
         }
 }
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/AnyTerm.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/AnyTerm.java
index c12c0166..f136b68d 100644
--- a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/AnyTerm.java
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/AnyTerm.java
@@ -6,6 +6,7 @@
 package tools.refinery.store.query.term;
 
 import tools.refinery.store.query.equality.LiteralEqualityHelper;
+import tools.refinery.store.query.equality.LiteralHashCodeHelper;
 import tools.refinery.store.query.substitution.Substitution;
 
 import java.util.Set;
@@ -17,5 +18,7 @@ public sealed interface AnyTerm permits AnyDataVariable, Term {
 
         boolean equalsWithSubstitution(LiteralEqualityHelper helper, AnyTerm other);
 
+        int hashCodeWithSubstitution(LiteralHashCodeHelper helper);
+
         Set<AnyDataVariable> getInputVariables();
 }
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/BinaryTerm.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/BinaryTerm.java
index 8ad17839..09c86db6 100644
--- a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/BinaryTerm.java
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/BinaryTerm.java
@@ -6,6 +6,7 @@
 package tools.refinery.store.query.term;
 
 import tools.refinery.store.query.equality.LiteralEqualityHelper;
+import tools.refinery.store.query.equality.LiteralHashCodeHelper;
 import tools.refinery.store.query.substitution.Substitution;
 import tools.refinery.store.query.valuation.Valuation;
 
@@ -14,6 +15,8 @@ import java.util.HashSet;
 import java.util.Objects;
 import java.util.Set;
 
+// {@link Object#equals(Object)} is implemented by {@link AbstractTerm}.
+@SuppressWarnings("squid:S2160")
 public abstract class BinaryTerm<R, T1, T2> extends AbstractTerm<R> {
         private final Class<T1> leftType;
         private final Class<T2> rightType;
@@ -80,6 +83,12 @@ public abstract class BinaryTerm<R, T1, T2> extends AbstractTerm<R> {
         }
 
         @Override
+        public int hashCodeWithSubstitution(LiteralHashCodeHelper helper) {
+                return Objects.hash(super.hashCodeWithSubstitution(helper), leftType.hashCode(), rightType.hashCode(),
+                                left.hashCodeWithSubstitution(helper), right.hashCodeWithSubstitution(helper));
+        }
+
+        @Override
         public Term<R> substitute(Substitution substitution) {
                 return doSubstitute(substitution, left.substitute(substitution), right.substitute(substitution));
         }
@@ -93,21 +102,4 @@ public abstract class BinaryTerm<R, T1, T2> extends AbstractTerm<R> {
                 inputVariables.addAll(right.getInputVariables());
                 return Collections.unmodifiableSet(inputVariables);
         }
-
-        @Override
-        public boolean equals(Object o) {
-                if (this == o) return true;
-                if (o == null || getClass() != o.getClass()) return false;
-                if (!super.equals(o)) return false;
-                BinaryTerm<?, ?, ?> that = (BinaryTerm<?, ?, ?>) o;
-                return Objects.equals(leftType, that.leftType) &&
-                                Objects.equals(rightType, that.rightType) &&
-                                Objects.equals(left, that.left) &&
-                                Objects.equals(right, that.right);
-        }
-
-        @Override
-        public int hashCode() {
-                return Objects.hash(super.hashCode(), leftType, rightType, left, right);
-        }
 }
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/ConstantTerm.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/ConstantTerm.java
index 2f6c56d1..e722c84f 100644
--- a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/ConstantTerm.java
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/ConstantTerm.java
@@ -6,12 +6,15 @@
 package tools.refinery.store.query.term;
 
 import tools.refinery.store.query.equality.LiteralEqualityHelper;
+import tools.refinery.store.query.equality.LiteralHashCodeHelper;
 import tools.refinery.store.query.substitution.Substitution;
 import tools.refinery.store.query.valuation.Valuation;
 
 import java.util.Objects;
 import java.util.Set;
 
+// {@link Object#equals(Object)} is implemented by {@link AbstractTerm}.
+@SuppressWarnings("squid:S2160")
 public final class ConstantTerm<T> extends AbstractTerm<T> {
         private final T value;
 
@@ -47,6 +50,11 @@ public final class ConstantTerm<T> extends AbstractTerm<T> {
         }
 
         @Override
+        public int hashCodeWithSubstitution(LiteralHashCodeHelper helper) {
+                return Objects.hash(super.hashCodeWithSubstitution(helper), Objects.hash(value));
+        }
+
+        @Override
         public Set<AnyDataVariable> getInputVariables() {
                 return Set.of();
         }
@@ -55,17 +63,4 @@ public final class ConstantTerm<T> extends AbstractTerm<T> {
         public String toString() {
                 return value.toString();
         }
-
-        @Override
-        public boolean equals(Object o) {
-                if (this == o) return true;
-                if (o == null || getClass() != o.getClass()) return false;
-                ConstantTerm<?> that = (ConstantTerm<?>) o;
-                return Objects.equals(value, that.value);
-        }
-
-        @Override
-        public int hashCode() {
-                return Objects.hash(value);
-        }
 }
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/DataVariable.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/DataVariable.java
index 00950360..e71c69ac 100644
--- a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/DataVariable.java
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/DataVariable.java
@@ -7,6 +7,7 @@ package tools.refinery.store.query.term;
 
 import org.jetbrains.annotations.Nullable;
 import tools.refinery.store.query.equality.LiteralEqualityHelper;
+import tools.refinery.store.query.equality.LiteralHashCodeHelper;
 import tools.refinery.store.query.literal.Literal;
 import tools.refinery.store.query.substitution.Substitution;
 import tools.refinery.store.query.valuation.Valuation;
@@ -62,6 +63,16 @@ public final class DataVariable<T> extends AnyDataVariable implements Term<T> {
                 return other instanceof DataVariable<?> dataVariable && helper.variableEqual(this, dataVariable);
         }
 
+        @Override
+        public int hashCodeWithSubstitution(LiteralHashCodeHelper helper) {
+                return helper.getVariableHashCode(this);
+        }
+
+        @Override
+        public int hashCodeWithSubstitution(int sequenceNumber) {
+                return Objects.hash(type, sequenceNumber);
+        }
+
         public Literal assign(AssignedValue<T> value) {
                 return value.toLiteral(this);
         }
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/NodeVariable.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/NodeVariable.java
index a2f3261f..d679908a 100644
--- a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/NodeVariable.java
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/NodeVariable.java
@@ -46,6 +46,11 @@ public final class NodeVariable extends Variable {
                 throw new IllegalStateException("%s is a node variable".formatted(this));
         }
 
+        @Override
+        public int hashCodeWithSubstitution(int sequenceNumber) {
+                return sequenceNumber;
+        }
+
         public ConstantLiteral isConstant(int value) {
                 return new ConstantLiteral(this, value);
         }
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/UnaryTerm.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/UnaryTerm.java
index a46ebe31..6451ea00 100644
--- a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/UnaryTerm.java
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/UnaryTerm.java
@@ -6,12 +6,15 @@
 package tools.refinery.store.query.term;
 
 import tools.refinery.store.query.equality.LiteralEqualityHelper;
+import tools.refinery.store.query.equality.LiteralHashCodeHelper;
 import tools.refinery.store.query.substitution.Substitution;
 import tools.refinery.store.query.valuation.Valuation;
 
 import java.util.Objects;
 import java.util.Set;
 
+// {@link Object#equals(Object)} is implemented by {@link AbstractTerm}.
+@SuppressWarnings("squid:S2160")
 public abstract class UnaryTerm<R, T> extends AbstractTerm<R> {
         private final Class<T> bodyType;
         private final Term<T> body;
@@ -52,6 +55,11 @@ public abstract class UnaryTerm<R, T> extends AbstractTerm<R> {
         }
 
         @Override
+        public int hashCodeWithSubstitution(LiteralHashCodeHelper helper) {
+                return Objects.hash(super.hashCodeWithSubstitution(helper), bodyType, body.hashCodeWithSubstitution(helper));
+        }
+
+        @Override
         public Term<R> substitute(Substitution substitution) {
                 return doSubstitute(substitution, body.substitute(substitution));
         }
@@ -62,18 +70,4 @@ public abstract class UnaryTerm<R, T> extends AbstractTerm<R> {
         public Set<AnyDataVariable> getInputVariables() {
                 return body.getInputVariables();
         }
-
-        @Override
-        public boolean equals(Object o) {
-                if (this == o) return true;
-                if (o == null || getClass() != o.getClass()) return false;
-                if (!super.equals(o)) return false;
-                UnaryTerm<?, ?> unaryTerm = (UnaryTerm<?, ?>) o;
-                return Objects.equals(bodyType, unaryTerm.bodyType) && Objects.equals(body, unaryTerm.body);
-        }
-
-        @Override
-        public int hashCode() {
-                return Objects.hash(super.hashCode(), bodyType, body);
-        }
 }
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/Variable.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/Variable.java
index a0268c8e..74384df3 100644
--- a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/Variable.java
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/Variable.java
@@ -48,6 +48,8 @@ public abstract sealed class Variable permits AnyDataVariable, NodeVariable {
 
         public abstract <T> DataVariable<T> asDataVariable(Class<T> type);
 
+        public abstract int hashCodeWithSubstitution(int sequenceNumber);
+
         @Override
         public String toString() {
                 return getName();