feat: Dnf reduction and structural equality

23 files changed, 506 insertions, 58 deletions

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
index 760b264b..b6744b50 100644
--- 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
@@ -1,5 +1,7 @@
 package tools.refinery.store.query;
 
+import tools.refinery.store.query.equality.DnfEqualityChecker;
+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;
@@ -7,6 +9,8 @@ import tools.refinery.store.query.literal.LiteralReduction;
 import java.util.*;
 
 public final class Dnf implements RelationLike {
+        private static final String INDENTATION = "    ";
+
         private final String name;
 
         private final String uniqueName;
@@ -50,7 +54,11 @@ public final class Dnf implements RelationLike {
 
         @Override
         public String name() {
-                return name;
+                return name == null ? uniqueName : name;
+        }
+
+        public boolean isExplicitlyNamed() {
+                return name == null;
         }
 
         public String getUniqueName() {
@@ -102,6 +110,61 @@ public final class Dnf implements RelationLike {
                 return call(CallPolarity.TRANSITIVE, List.of(left, right));
         }
 
+        public boolean equalsWithSubstitution(DnfEqualityChecker callEqualityChecker, Dnf other) {
+                if (arity() != other.arity()) {
+                        return false;
+                }
+                int numClauses = clauses.size();
+                if (numClauses != other.clauses.size()) {
+                        return false;
+                }
+                for (int i = 0; i < numClauses; i++) {
+                        var literalEqualityHelper = new LiteralEqualityHelper(callEqualityChecker, parameters, other.parameters);
+                        if (!clauses.get(i).equalsWithSubstitution(literalEqualityHelper, other.clauses.get(i))) {
+                                return false;
+                        }
+                }
+                return true;
+        }
+
+        @Override
+        public String toString() {
+                var builder = new StringBuilder();
+                builder.append("pred ").append(name()).append("(");
+                var parameterIterator = parameters.iterator();
+                if (parameterIterator.hasNext()) {
+                        builder.append(parameterIterator.next());
+                        while (parameterIterator.hasNext()) {
+                                builder.append(", ").append(parameterIterator.next());
+                        }
+                }
+                builder.append(") <->");
+                var clauseIterator = clauses.iterator();
+                if (clauseIterator.hasNext()) {
+                        appendClause(clauseIterator.next(), builder);
+                        while (clauseIterator.hasNext()) {
+                                builder.append("\n;");
+                                appendClause(clauseIterator.next(), builder);
+                        }
+                } else {
+                        builder.append("\n").append(INDENTATION).append("<no clauses>");
+                }
+                builder.append(".\n");
+                return builder.toString();
+        }
+
+        private static void appendClause(DnfClause clause, StringBuilder builder) {
+                var iterator = clause.literals().iterator();
+                if (!iterator.hasNext()) {
+                        builder.append("\n").append(INDENTATION).append("<empty>");
+                        return;
+                }
+                builder.append("\n").append(INDENTATION).append(iterator.next());
+                while (iterator.hasNext()) {
+                        builder.append(",\n").append(INDENTATION).append(iterator.next());
+                }
+        }
+
         public static DnfBuilder builder() {
                 return builder(null);
         }
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
index b18b5177..ca47e979 100644
--- 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
@@ -52,7 +52,8 @@ public class DnfBuilder {
         }
 
         public DnfBuilder clause(Collection<Literal> literals) {
-                var filteredLiterals = new ArrayList<Literal>(literals.size());
+                // Remove duplicates by using a hashed data structure.
+                var filteredLiterals = new LinkedHashSet<Literal>(literals.size());
                 for (var literal : literals) {
                         var reduction = literal.getReduction();
                         switch (reduction) {
@@ -65,10 +66,10 @@ public class DnfBuilder {
                                 // Clauses with {@code false} literals can be omitted entirely.
                                 return this;
                         }
-                        default -> throw new IllegalStateException("Invalid reduction %s".formatted(reduction));
+                        default -> throw new IllegalArgumentException("Invalid reduction: " + reduction);
                         }
                 }
-                clauses.add(Collections.unmodifiableList(filteredLiterals));
+                clauses.add(List.copyOf(filteredLiterals));
                 return this;
         }
 
@@ -77,10 +78,7 @@ public class DnfBuilder {
         }
 
         public DnfBuilder clauses(DnfClause... clauses) {
-                for (var clause : clauses) {
-                        this.clause(clause);
-                }
-                return this;
+                return clauses(List.of(clauses));
         }
 
         public DnfBuilder clauses(Collection<DnfClause> clauses) {
@@ -91,18 +89,27 @@ public class DnfBuilder {
         }
 
         public Dnf build() {
+                var postProcessedClauses = postProcessClauses();
+                return new Dnf(name, Collections.unmodifiableList(parameters),
+                                Collections.unmodifiableList(functionalDependencies),
+                                Collections.unmodifiableList(postProcessedClauses));
+        }
+
+        private List<DnfClause> postProcessClauses() {
                 var postProcessedClauses = new ArrayList<DnfClause>(clauses.size());
-                for (var constraints : clauses) {
+                for (var literals : clauses) {
+                        if (literals.isEmpty()) {
+                                // Predicate will always match, the other clauses are irrelevant.
+                                return List.of(new DnfClause(Set.of(), List.of()));
+                        }
                         var variables = new HashSet<Variable>();
-                        for (var constraint : constraints) {
+                        for (var constraint : literals) {
                                 constraint.collectAllVariables(variables);
                         }
                         parameters.forEach(variables::remove);
                         postProcessedClauses.add(new DnfClause(Collections.unmodifiableSet(variables),
-                                        Collections.unmodifiableList(constraints)));
+                                        Collections.unmodifiableList(literals)));
                 }
-                return new Dnf(name, Collections.unmodifiableList(parameters),
-                                Collections.unmodifiableList(functionalDependencies),
-                                Collections.unmodifiableList(postProcessedClauses));
+                return postProcessedClauses;
         }
 }
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/DnfClause.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/DnfClause.java
index 2ba6becc..c6e8b8c9 100644
--- a/subprojects/store-query/src/main/java/tools/refinery/store/query/DnfClause.java
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/DnfClause.java
@@ -1,9 +1,22 @@
 package tools.refinery.store.query;
 
+import tools.refinery.store.query.equality.LiteralEqualityHelper;
 import tools.refinery.store.query.literal.Literal;
 
 import java.util.List;
 import java.util.Set;
 
 public record DnfClause(Set<Variable> quantifiedVariables, List<Literal> literals) {
+        public boolean equalsWithSubstitution(LiteralEqualityHelper helper, DnfClause other) {
+                int size = literals.size();
+                if (size != other.literals.size()) {
+                        return false;
+                }
+                for (int i = 0; i < size; i++) {
+                        if (!literals.get(i).equalsWithSubstitution(helper, other.literals.get(i))) {
+                                return false;
+                        }
+                }
+                return true;
+        }
 }
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/DnfUtils.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/DnfUtils.java
index 17564d43..c7a2849c 100644
--- a/subprojects/store-query/src/main/java/tools/refinery/store/query/DnfUtils.java
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/DnfUtils.java
@@ -1,6 +1,5 @@
 package tools.refinery.store.query;
 
-import java.util.Map;
 import java.util.UUID;
 
 public final class DnfUtils {
@@ -17,8 +16,4 @@ public final class DnfUtils {
                         return originalName + uniqueString;
                 }
         }
-
-        public static Variable maybeSubstitute(Variable variable, Map<Variable, Variable> substitution) {
-                return substitution.getOrDefault(variable, variable);
-        }
 }
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/EmptyResultSet.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/EmptyResultSet.java
new file mode 100644
index 00000000..a01a5a2f
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/EmptyResultSet.java
@@ -0,0 +1,49 @@
+package tools.refinery.store.query;
+
+import tools.refinery.store.tuple.Tuple;
+import tools.refinery.store.tuple.TupleLike;
+
+import java.util.Optional;
+import java.util.stream.Stream;
+
+public class EmptyResultSet implements ResultSet {
+        @Override
+        public boolean hasResult() {
+                return false;
+        }
+
+        @Override
+        public boolean hasResult(Tuple parameters) {
+                return false;
+        }
+
+        @Override
+        public Optional<TupleLike> oneResult() {
+                return Optional.empty();
+        }
+
+        @Override
+        public Optional<TupleLike> oneResult(Tuple parameters) {
+                return Optional.empty();
+        }
+
+        @Override
+        public Stream<TupleLike> allResults() {
+                return Stream.of();
+        }
+
+        @Override
+        public Stream<TupleLike> allResults(Tuple parameters) {
+                return Stream.of();
+        }
+
+        @Override
+        public int countResults() {
+                return 0;
+        }
+
+        @Override
+        public int countResults(Tuple parameters) {
+                return 0;
+        }
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/Variable.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/Variable.java
index 2eb87649..d0e0dead 100644
--- a/subprojects/store-query/src/main/java/tools/refinery/store/query/Variable.java
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/Variable.java
@@ -20,15 +20,15 @@ public class Variable {
 
         }
         public String getName() {
-                return name;
+                return name == null ? uniqueName : name;
         }
 
-        public String getUniqueName() {
-                return uniqueName;
+        public boolean isExplicitlyNamed() {
+                return name != null;
         }
 
-        public boolean isNamed() {
-                return name != null;
+        public String getUniqueName() {
+                return uniqueName;
         }
 
         public ConstantLiteral isConstant(int value) {
@@ -44,6 +44,11 @@ public class Variable {
         }
 
         @Override
+        public String toString() {
+                return getName();
+        }
+
+        @Override
         public boolean equals(Object o) {
                 if (this == o) return true;
                 if (o == null || getClass() != o.getClass()) return false;
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
new file mode 100644
index 00000000..ebd7f5b0
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/equality/DeepDnfEqualityChecker.java
@@ -0,0 +1,31 @@
+package tools.refinery.store.query.equality;
+
+import tools.refinery.store.query.Dnf;
+import tools.refinery.store.util.CycleDetectingMapper;
+
+import java.util.List;
+
+public class DeepDnfEqualityChecker implements DnfEqualityChecker {
+        private final CycleDetectingMapper<Pair, Boolean> mapper = new CycleDetectingMapper<>(Pair::toString,
+                        this::doCheckEqual);
+
+        @Override
+        public boolean dnfEqual(Dnf left, Dnf right) {
+                return mapper.map(new Pair(left, right));
+        }
+
+        protected boolean doCheckEqual(Pair pair) {
+                return pair.left.equalsWithSubstitution(this, pair.right);
+        }
+
+        protected List<Pair> getInProgress() {
+                return mapper.getInProgress();
+        }
+
+        protected record Pair(Dnf left, Dnf right) {
+                @Override
+                public String toString() {
+                        return "(%s, %s)".formatted(left.name(), right.name());
+                }
+        }
+}
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
new file mode 100644
index 00000000..eb77de17
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/equality/DnfEqualityChecker.java
@@ -0,0 +1,8 @@
+package tools.refinery.store.query.equality;
+
+import tools.refinery.store.query.Dnf;
+
+@FunctionalInterface
+public interface DnfEqualityChecker {
+        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
new file mode 100644
index 00000000..23f1acc7
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/equality/LiteralEqualityHelper.java
@@ -0,0 +1,48 @@
+package tools.refinery.store.query.equality;
+
+import tools.refinery.store.query.Dnf;
+import tools.refinery.store.query.Variable;
+
+import java.util.HashMap;
+import java.util.List;
+import java.util.Map;
+
+public class LiteralEqualityHelper {
+        private final DnfEqualityChecker dnfEqualityChecker;
+        private final Map<Variable, Variable> leftToRight;
+        private final Map<Variable, Variable> rightToLeft;
+
+        public LiteralEqualityHelper(DnfEqualityChecker dnfEqualityChecker, List<Variable> leftParameters,
+                                                                 List<Variable> 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), rightParameters.get(i))) {
+                                throw new IllegalArgumentException("Parameter lists cannot be unified: duplicate parameter " + i);
+                        }
+                }
+        }
+
+        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;
+                }
+                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/literal/BooleanLiteral.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/BooleanLiteral.java
index fd2f1eec..6d751be8 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
@@ -1,18 +1,19 @@
 package tools.refinery.store.query.literal;
 
 import tools.refinery.store.query.Variable;
+import tools.refinery.store.query.equality.LiteralEqualityHelper;
+import tools.refinery.store.query.substitution.Substitution;
 
-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);
+public enum BooleanLiteral implements PolarLiteral<BooleanLiteral> {
+        TRUE(true),
+        FALSE(false);
 
-        private final LiteralReduction reduction;
+        private final boolean value;
 
-        private BooleanLiteral(LiteralReduction reduction) {
-                this.reduction = reduction;
+        BooleanLiteral(boolean value) {
+                this.value = value;
         }
 
         @Override
@@ -21,14 +22,29 @@ public class BooleanLiteral implements Literal {
         }
 
         @Override
-        public Literal substitute(Map<Variable, Variable> substitution) {
+        public Literal substitute(Substitution substitution) {
                 // No variables to substitute.
                 return this;
         }
 
         @Override
         public LiteralReduction getReduction() {
-                return reduction;
+                return value ? LiteralReduction.ALWAYS_TRUE : LiteralReduction.ALWAYS_FALSE;
+        }
+
+        @Override
+        public BooleanLiteral negate() {
+                return fromBoolean(!value);
+        }
+
+        @Override
+        public boolean equalsWithSubstitution(LiteralEqualityHelper helper, Literal other) {
+                return equals(other);
+        }
+
+        @Override
+        public String toString() {
+                return Boolean.toString(value);
         }
 
         public static BooleanLiteral fromBoolean(boolean 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 5e1ae94d..091b4e04 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
@@ -1,11 +1,11 @@
 package tools.refinery.store.query.literal;
 
-import tools.refinery.store.query.DnfUtils;
 import tools.refinery.store.query.RelationLike;
 import tools.refinery.store.query.Variable;
+import tools.refinery.store.query.equality.LiteralEqualityHelper;
+import tools.refinery.store.query.substitution.Substitution;
 
 import java.util.List;
-import java.util.Map;
 import java.util.Objects;
 import java.util.Set;
 
@@ -31,6 +31,8 @@ public abstract class CallLiteral<T extends RelationLike> implements Literal {
                 return polarity;
         }
 
+        public abstract Class<T> getTargetType();
+
         public T getTarget() {
                 return target;
         }
@@ -46,8 +48,44 @@ public abstract class CallLiteral<T extends RelationLike> implements Literal {
                 }
         }
 
-        protected List<Variable> substituteArguments(Map<Variable, Variable> substitution) {
-                return arguments.stream().map(variable -> DnfUtils.maybeSubstitute(variable, substitution)).toList();
+        protected List<Variable> substituteArguments(Substitution substitution) {
+                return arguments.stream().map(substitution::getSubstitute).toList();
+        }
+
+        /**
+         * Compares the target of this call literal with another object.
+         *
+         * @param helper      Equality helper for comparing {@link Variable} and {@link tools.refinery.store.query.Dnf}
+         *                    instances.
+         * @param otherTarget The object to compare the target to.
+         * @return {@code true} if {@code otherTarget} is equal to the return value of {@link #getTarget()} according to
+         * {@code helper}, {@code false} otherwise.
+         */
+        protected boolean targetEquals(LiteralEqualityHelper helper, T otherTarget) {
+                return target.equals(otherTarget);
+        }
+
+        @Override
+        public boolean equalsWithSubstitution(LiteralEqualityHelper helper, Literal other) {
+                if (other.getClass() != getClass()) {
+                        return false;
+                }
+                var otherCallLiteral = (CallLiteral<?>) other;
+                if (getTargetType() != otherCallLiteral.getTargetType() || polarity != otherCallLiteral.polarity) {
+                        return false;
+                }
+                var arity = arguments.size();
+                if (arity != otherCallLiteral.arguments.size()) {
+                        return false;
+                }
+                for (int i = 0; i < arity; i++) {
+                        if (!helper.variableEqual(arguments.get(i), otherCallLiteral.arguments.get(i))) {
+                                return false;
+                        }
+                }
+                @SuppressWarnings("unchecked")
+                var otherTarget = (T) otherCallLiteral.target;
+                return targetEquals(helper, otherTarget);
         }
 
         @Override
@@ -63,4 +101,33 @@ public abstract class CallLiteral<T extends RelationLike> implements Literal {
         public int hashCode() {
                 return Objects.hash(polarity, target, arguments);
         }
+
+        protected String targetToString() {
+                return "@%s %s".formatted(getTargetType().getSimpleName(), target.name());
+        }
+
+        @Override
+        public String toString() {
+                var builder = new StringBuilder();
+                if (!polarity.isPositive()) {
+                        builder.append("!(");
+                }
+                builder.append(targetToString());
+                if (polarity.isTransitive()) {
+                        builder.append("+");
+                }
+                builder.append("(");
+                var argumentIterator = arguments.iterator();
+                if (argumentIterator.hasNext()) {
+                        builder.append(argumentIterator.next());
+                        while (argumentIterator.hasNext()) {
+                                builder.append(", ").append(argumentIterator.next());
+                        }
+                }
+                builder.append(")");
+                if (!polarity.isPositive()) {
+                        builder.append(")");
+                }
+                return builder.toString();
+        }
 }
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 746d23af..d01c7d20 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
@@ -1,9 +1,9 @@
 package tools.refinery.store.query.literal;
 
-import tools.refinery.store.query.DnfUtils;
 import tools.refinery.store.query.Variable;
+import tools.refinery.store.query.equality.LiteralEqualityHelper;
+import tools.refinery.store.query.substitution.Substitution;
 
-import java.util.Map;
 import java.util.Set;
 
 public record ConstantLiteral(Variable variable, int nodeId) implements Literal {
@@ -13,7 +13,21 @@ public record ConstantLiteral(Variable variable, int nodeId) implements Literal
         }
 
         @Override
-        public ConstantLiteral substitute(Map<Variable, Variable> substitution) {
-                return new ConstantLiteral(DnfUtils.maybeSubstitute(variable, substitution), nodeId);
+        public ConstantLiteral substitute(Substitution substitution) {
+                return new ConstantLiteral(substitution.getSubstitute(variable), nodeId);
+        }
+
+        @Override
+        public boolean equalsWithSubstitution(LiteralEqualityHelper helper, Literal other) {
+                if (other.getClass() != getClass()) {
+                        return false;
+                }
+                var otherConstantLiteral = (ConstantLiteral) other;
+                return helper.variableEqual(variable, otherConstantLiteral.variable) && nodeId == otherConstantLiteral.nodeId;
+        }
+
+        @Override
+        public String toString() {
+                return "%s === @Constant %d".formatted(variable, nodeId);
         }
 }
diff --git a/subprojects/store-query/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 de6c6005..27917265 100644
--- a/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/DnfCallLiteral.java
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/DnfCallLiteral.java
@@ -2,9 +2,10 @@ package tools.refinery.store.query.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.substitution.Substitution;
 
 import java.util.List;
-import java.util.Map;
 
 public final class DnfCallLiteral extends CallLiteral<Dnf> implements PolarLiteral<DnfCallLiteral> {
         public DnfCallLiteral(CallPolarity polarity, Dnf target, List<Variable> arguments) {
@@ -12,7 +13,12 @@ public final class DnfCallLiteral extends CallLiteral<Dnf> implements PolarLiter
         }
 
         @Override
-        public DnfCallLiteral substitute(Map<Variable, Variable> substitution) {
+        public Class<Dnf> getTargetType() {
+                return Dnf.class;
+        }
+
+        @Override
+        public DnfCallLiteral substitute(Substitution substitution) {
                 return new DnfCallLiteral(getPolarity(), getTarget(), substituteArguments(substitution));
         }
 
@@ -26,4 +32,9 @@ public final class DnfCallLiteral extends CallLiteral<Dnf> implements PolarLiter
                 var dnfReduction = getTarget().getReduction();
                 return getPolarity().isPositive() ? dnfReduction : dnfReduction.negate();
         }
+
+        @Override
+        protected boolean targetEquals(LiteralEqualityHelper helper, Dnf otherTarget) {
+                return helper.dnfEqual(getTarget(), otherTarget);
+        }
 }
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 f30179b2..61c753c3 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
@@ -1,9 +1,9 @@
 package tools.refinery.store.query.literal;
 
-import tools.refinery.store.query.DnfUtils;
 import tools.refinery.store.query.Variable;
+import tools.refinery.store.query.equality.LiteralEqualityHelper;
+import tools.refinery.store.query.substitution.Substitution;
 
-import java.util.Map;
 import java.util.Set;
 
 public record EquivalenceLiteral(boolean positive, Variable left, Variable right)
@@ -20,9 +20,8 @@ public record EquivalenceLiteral(boolean positive, Variable left, Variable right
         }
 
         @Override
-        public EquivalenceLiteral substitute(Map<Variable, Variable> substitution) {
-                return new EquivalenceLiteral(positive, DnfUtils.maybeSubstitute(left, substitution),
-                                DnfUtils.maybeSubstitute(right, substitution));
+        public EquivalenceLiteral substitute(Substitution substitution) {
+                return new EquivalenceLiteral(positive, substitution.getSubstitute(left), substitution.getSubstitute(right));
         }
 
         @Override
@@ -32,4 +31,19 @@ public record EquivalenceLiteral(boolean positive, Variable left, Variable right
                 }
                 return LiteralReduction.NOT_REDUCIBLE;
         }
+
+        @Override
+        public boolean equalsWithSubstitution(LiteralEqualityHelper helper, Literal other) {
+                if (other.getClass() != getClass()) {
+                        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);
+        }
 }
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 a6893acf..ddd91775 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
@@ -1,16 +1,20 @@
 package tools.refinery.store.query.literal;
 
 import tools.refinery.store.query.Variable;
+import tools.refinery.store.query.equality.LiteralEqualityHelper;
+import tools.refinery.store.query.substitution.Substitution;
 
-import java.util.Map;
 import java.util.Set;
 
 public interface Literal {
         void collectAllVariables(Set<Variable> variables);
 
-        Literal substitute(Map<Variable, Variable> substitution);
+        Literal substitute(Substitution substitution);
 
         default LiteralReduction getReduction() {
                 return LiteralReduction.NOT_REDUCIBLE;
         }
+
+        @SuppressWarnings("BooleanMethodIsAlwaysInverted")
+        boolean equalsWithSubstitution(LiteralEqualityHelper helper, Literal other);
 }
diff --git a/subprojects/store-query/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..fb8b3332 100644
--- a/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/RelationViewLiteral.java
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/RelationViewLiteral.java
@@ -1,10 +1,10 @@
 package tools.refinery.store.query.literal;
 
 import tools.refinery.store.query.Variable;
+import tools.refinery.store.query.substitution.Substitution;
 import tools.refinery.store.query.view.AnyRelationView;
 
 import java.util.List;
-import java.util.Map;
 
 public final class RelationViewLiteral extends CallLiteral<AnyRelationView>
                 implements PolarLiteral<RelationViewLiteral> {
@@ -13,7 +13,18 @@ public final class RelationViewLiteral extends CallLiteral<AnyRelationView>
         }
 
         @Override
-        public RelationViewLiteral substitute(Map<Variable, Variable> substitution) {
+        public Class<AnyRelationView> getTargetType() {
+                return AnyRelationView.class;
+        }
+
+        @Override
+        protected String targetToString() {
+                var target = getTarget();
+                return "@RelationView(\"%s\") %s".formatted(target.getViewName(), target.getSymbol().name());
+        }
+
+        @Override
+        public RelationViewLiteral substitute(Substitution substitution) {
                 return new RelationViewLiteral(getPolarity(), getTarget(), substituteArguments(substitution));
         }
 
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/substitution/MapBasedSubstitution.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/substitution/MapBasedSubstitution.java
new file mode 100644
index 00000000..ffc65047
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/substitution/MapBasedSubstitution.java
@@ -0,0 +1,13 @@
+package tools.refinery.store.query.substitution;
+
+import tools.refinery.store.query.Variable;
+
+import java.util.Map;
+
+public record MapBasedSubstitution(Map<Variable, Variable> map, Substitution fallback) implements Substitution {
+        @Override
+        public Variable getSubstitute(Variable variable) {
+                var value = map.get(variable);
+                return value == null ? fallback.getSubstitute(variable) : value;
+        }
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/substitution/RenewingSubstitution.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/substitution/RenewingSubstitution.java
new file mode 100644
index 00000000..54d18a3f
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/substitution/RenewingSubstitution.java
@@ -0,0 +1,19 @@
+package tools.refinery.store.query.substitution;
+
+import tools.refinery.store.query.Variable;
+
+import java.util.HashMap;
+import java.util.Map;
+
+public class RenewingSubstitution implements Substitution {
+        private final Map<Variable, Variable> alreadyRenewed = new HashMap<>();
+
+        @Override
+        public Variable getSubstitute(Variable variable) {
+                return alreadyRenewed.computeIfAbsent(variable, RenewingSubstitution::renew);
+        }
+
+        private static Variable renew(Variable variable) {
+                return variable.isExplicitlyNamed() ? new Variable(variable.getName()) : new Variable();
+        }
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/substitution/StatelessSubstitution.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/substitution/StatelessSubstitution.java
new file mode 100644
index 00000000..d33ad6fb
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/substitution/StatelessSubstitution.java
@@ -0,0 +1,18 @@
+package tools.refinery.store.query.substitution;
+
+import tools.refinery.store.query.Variable;
+
+public enum StatelessSubstitution implements Substitution {
+        FAILING {
+                @Override
+                public Variable getSubstitute(Variable variable) {
+                        throw new IllegalArgumentException("No substitute for " + variable);
+                }
+        },
+        IDENTITY {
+                @Override
+                public Variable getSubstitute(Variable variable) {
+                        return variable;
+                }
+        }
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/substitution/Substitution.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/substitution/Substitution.java
new file mode 100644
index 00000000..9d086bf5
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/substitution/Substitution.java
@@ -0,0 +1,8 @@
+package tools.refinery.store.query.substitution;
+
+import tools.refinery.store.query.Variable;
+
+@FunctionalInterface
+public interface Substitution {
+        Variable getSubstitute(Variable variable);
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/substitution/Substitutions.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/substitution/Substitutions.java
new file mode 100644
index 00000000..26cf1a20
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/substitution/Substitutions.java
@@ -0,0 +1,27 @@
+package tools.refinery.store.query.substitution;
+
+import tools.refinery.store.query.Variable;
+
+import java.util.Map;
+
+public final class Substitutions {
+        private Substitutions() {
+                throw new IllegalStateException("This is a static utility class and should not be instantiate directly");
+        }
+
+        public static Substitution total(Map<Variable, Variable> map) {
+                return new MapBasedSubstitution(map, StatelessSubstitution.FAILING);
+        }
+
+        public static Substitution partial(Map<Variable, Variable> map) {
+                return new MapBasedSubstitution(map, StatelessSubstitution.IDENTITY);
+        }
+
+        public static Substitution renewing(Map<Variable, Variable> map) {
+                return new MapBasedSubstitution(map, renewing());
+        }
+
+        public static Substitution renewing() {
+                return new RenewingSubstitution();
+        }
+}
diff --git a/subprojects/store-query/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..bc3ac1ea 100644
--- a/subprojects/store-query/src/main/java/tools/refinery/store/query/view/AnyRelationView.java
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/view/AnyRelationView.java
@@ -10,6 +10,8 @@ import java.util.Set;
 public sealed interface AnyRelationView extends RelationLike permits RelationView {
         AnySymbol getSymbol();
 
+        String getViewName();
+
         default Set<FunctionalDependency<Integer>> getFunctionalDependencies() {
                 return Set.of();
         }
diff --git a/subprojects/store-query/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 2714a8c5..ea9fd5e2 100644
--- a/subprojects/store-query/src/main/java/tools/refinery/store/query/view/RelationView.java
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/view/RelationView.java
@@ -21,11 +21,11 @@ import java.util.UUID;
 public abstract non-sealed class RelationView<T> implements AnyRelationView {
         private final Symbol<T> symbol;
 
-        private final String name;
+        private final String viewName;
 
-        protected RelationView(Symbol<T> symbol, String name) {
+        protected RelationView(Symbol<T> symbol, String viewName) {
                 this.symbol = symbol;
-                this.name = name;
+                this.viewName = viewName;
         }
 
         protected RelationView(Symbol<T> representation) {
@@ -38,8 +38,13 @@ public abstract non-sealed class RelationView<T> implements AnyRelationView {
         }
 
         @Override
+        public String getViewName() {
+                return viewName;
+        }
+
+        @Override
         public String name() {
-                return symbol.name() + "#" + name;
+                return symbol.name() + "#" + viewName;
         }
 
         public abstract boolean filter(Tuple key, T value);
@@ -72,11 +77,11 @@ public abstract non-sealed class RelationView<T> implements AnyRelationView {
                 if (this == o) return true;
                 if (o == null || getClass() != o.getClass()) return false;
                 RelationView<?> that = (RelationView<?>) o;
-                return Objects.equals(symbol, that.symbol) && Objects.equals(name, that.name);
+                return Objects.equals(symbol, that.symbol) && Objects.equals(viewName, that.viewName);
         }
 
         @Override
         public int hashCode() {
-                return Objects.hash(symbol, name);
+                return Objects.hash(symbol, viewName);
         }
 }