1 files changed, 59 insertions, 0 deletions

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);
+        }
+}