refactor: enable data variable unification

This is needed for demand set transformation of DNFs with input data parameters,
where the result of the transformation has an out data parameter that has to be
unified with the variable in the parent clause.

8 files changed, 36 insertions, 67 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 f2749094..5d77b9aa 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
@@ -11,7 +11,6 @@ import tools.refinery.store.query.literal.*;
 import tools.refinery.store.query.substitution.MapBasedSubstitution;
 import tools.refinery.store.query.substitution.StatelessSubstitution;
 import tools.refinery.store.query.substitution.Substitution;
-import tools.refinery.store.query.term.NodeVariable;
 import tools.refinery.store.query.term.ParameterDirection;
 import tools.refinery.store.query.term.Variable;
 
@@ -21,8 +20,8 @@ import java.util.function.Function;
 class ClausePostProcessor {
         private final Map<Variable, ParameterInfo> parameters;
         private final List<Literal> literals;
-        private final Map<NodeVariable, NodeVariable> representatives = new LinkedHashMap<>();
-        private final Map<NodeVariable, Set<NodeVariable>> equivalencePartition = new HashMap<>();
+        private final Map<Variable, Variable> representatives = new LinkedHashMap<>();
+        private final Map<Variable, Set<Variable>> equivalencePartition = new HashMap<>();
         private List<Literal> substitutedLiterals;
         private final Set<Variable> existentiallyQuantifiedVariables = new LinkedHashSet<>();
         private Set<Variable> positiveVariables;
@@ -78,7 +77,7 @@ class ClausePostProcessor {
                 return literal instanceof EquivalenceLiteral equivalenceLiteral && equivalenceLiteral.isPositive();
         }
 
-        private void mergeVariables(NodeVariable left, NodeVariable right) {
+        private void mergeVariables(Variable left, Variable right) {
                 var leftRepresentative = getRepresentative(left);
                 var rightRepresentative = getRepresentative(right);
                 var leftInfo = parameters.get(leftRepresentative);
@@ -91,7 +90,7 @@ class ClausePostProcessor {
                 }
         }
 
-        private void doMergeVariables(NodeVariable parentRepresentative, NodeVariable newChildRepresentative) {
+        private void doMergeVariables(Variable parentRepresentative, Variable newChildRepresentative) {
                 var parentSet = getEquivalentVariables(parentRepresentative);
                 var childSet = getEquivalentVariables(newChildRepresentative);
                 parentSet.addAll(childSet);
@@ -101,18 +100,18 @@ class ClausePostProcessor {
                 }
         }
 
-        private NodeVariable getRepresentative(NodeVariable variable) {
+        private Variable getRepresentative(Variable variable) {
                 return representatives.computeIfAbsent(variable, Function.identity());
         }
 
-        private Set<NodeVariable> getEquivalentVariables(NodeVariable variable) {
+        private Set<Variable> getEquivalentVariables(Variable variable) {
                 var representative = getRepresentative(variable);
                 if (!representative.equals(variable)) {
                         throw new AssertionError("NodeVariable %s already has a representative %s"
                                         .formatted(variable, representative));
                 }
                 return equivalencePartition.computeIfAbsent(variable, key -> {
-                        var set = new HashSet<NodeVariable>(1);
+                        var set = new HashSet<Variable>(1);
                         set.add(key);
                         return set;
                 });
@@ -123,7 +122,7 @@ class ClausePostProcessor {
                         var left = pair.getKey();
                         var right = pair.getValue();
                         if (!left.equals(right) && parameters.containsKey(left) && parameters.containsKey(right)) {
-                                substitutedLiterals.add(left.isEquivalent(right));
+                                substitutedLiterals.add(new EquivalenceLiteral(true, left, right));
                         }
                 }
         }
@@ -149,20 +148,7 @@ class ClausePostProcessor {
 
         private void computeExistentiallyQuantifiedVariables() {
                 for (var literal : substitutedLiterals) {
-                        for (var variable : literal.getOutputVariables()) {
-                                boolean added = existentiallyQuantifiedVariables.add(variable);
-                                if (!variable.isUnifiable()) {
-                                        var parameterInfo = parameters.get(variable);
-                                        if (parameterInfo != null && parameterInfo.direction() == ParameterDirection.IN) {
-                                                throw new IllegalArgumentException("Trying to bind %s parameter %s"
-                                                                .formatted(ParameterDirection.IN, variable));
-                                        }
-                                        if (!added) {
-                                                throw new IllegalArgumentException("Variable %s has multiple assigned values"
-                                                                .formatted(variable));
-                                        }
-                                }
-                        }
+                        existentiallyQuantifiedVariables.addAll(literal.getOutputVariables());
                 }
         }
 
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 1e96cf27..fe9cefcc 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
@@ -24,10 +24,6 @@ public final class SymbolicParameter extends Parameter {
                 return variable;
         }
 
-        public boolean isUnifiable() {
-                return variable.isUnifiable();
-        }
-
         public int hashCodeWithSubstitution(LiteralHashCodeHelper helper) {
                 return Objects.hash(super.hashCode(), helper.getVariableHashCode(variable));
         }
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 a355dc3b..263c2e20 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
@@ -14,6 +14,8 @@ import tools.refinery.store.query.term.Variable;
 
 import java.util.*;
 
+// {@link Object#equals(Object)} is implemented by {@link AbstractLiteral}.
+@SuppressWarnings("squid:S2160")
 public abstract class AbstractCallLiteral extends AbstractLiteral {
         private final Constraint target;
         private final List<Variable> arguments;
@@ -42,16 +44,12 @@ public abstract class AbstractCallLiteral extends AbstractLiteral {
                         }
                         switch (parameter.getDirection()) {
                         case IN -> {
-                                if (mutableOutArguments.remove(argument)) {
-                                        checkInOutUnifiable(argument);
-                                }
+                                mutableOutArguments.remove(argument);
                                 mutableInArguments.add(argument);
                         }
                         case OUT -> {
-                                if (mutableInArguments.contains(argument)) {
-                                        checkInOutUnifiable(argument);
-                                } else if (!mutableOutArguments.add(argument)) {
-                                        checkDuplicateOutUnifiable(argument);
+                                if (!mutableInArguments.contains(argument)) {
+                                        mutableOutArguments.add(argument);
                                 }
                         }
                         }
@@ -60,19 +58,6 @@ public abstract class AbstractCallLiteral extends AbstractLiteral {
                 outArguments = Collections.unmodifiableSet(mutableOutArguments);
         }
 
-        private static void checkInOutUnifiable(Variable argument) {
-                if (!argument.isUnifiable()) {
-                        throw new IllegalArgumentException("Argument %s cannot appear with both %s and %s direction"
-                                        .formatted(argument, ParameterDirection.IN, ParameterDirection.OUT));
-                }
-        }
-
-        private static void checkDuplicateOutUnifiable(Variable argument) {
-                if (!argument.isUnifiable()) {
-                        throw new IllegalArgumentException("Argument %s cannot be bound multiple times".formatted(argument));
-                }
-        }
-
         public Constraint getTarget() {
                 return target;
         }
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 61b7344f..9a0c22d1 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
@@ -8,18 +8,23 @@ 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;
 
 import java.util.Objects;
 import java.util.Set;
 
+// {@link Object#equals(Object)} is implemented by {@link AbstractLiteral}.
+@SuppressWarnings("squid:S2160")
 public final class EquivalenceLiteral extends AbstractLiteral implements CanNegate<EquivalenceLiteral> {
         private final boolean positive;
-        private final NodeVariable left;
-        private final NodeVariable right;
+        private final Variable left;
+        private final Variable right;
 
-        public EquivalenceLiteral(boolean positive, NodeVariable left, NodeVariable right) {
+        public EquivalenceLiteral(boolean positive, Variable left, Variable right) {
+                if (!left.tryGetType().equals(right.tryGetType())) {
+                        throw new IllegalArgumentException("Variables %s and %s of different type cannot be equivalent"
+                                        .formatted(left, right));
+                }
                 this.positive = positive;
                 this.left = left;
                 this.right = right;
@@ -29,11 +34,11 @@ public final class EquivalenceLiteral extends AbstractLiteral implements CanNega
                 return positive;
         }
 
-        public NodeVariable getLeft() {
+        public Variable getLeft() {
                 return left;
         }
 
-        public NodeVariable getRight() {
+        public Variable getRight() {
                 return right;
         }
 
@@ -59,8 +64,8 @@ public final class EquivalenceLiteral extends AbstractLiteral implements CanNega
 
         @Override
         public EquivalenceLiteral substitute(Substitution substitution) {
-                return new EquivalenceLiteral(positive, substitution.getTypeSafeSubstitute(left),
-                                substitution.getTypeSafeSubstitute(right));
+                return new EquivalenceLiteral(positive, substitution.getSubstitute(left),
+                                substitution.getSubstitute(right));
         }
 
         @Override
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/AnyDataVariable.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/AnyDataVariable.java
index ed6941da..4d88051b 100644
--- a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/AnyDataVariable.java
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/AnyDataVariable.java
@@ -47,11 +47,6 @@ public abstract sealed class AnyDataVariable extends Variable implements AnyTerm
         }
 
         @Override
-        public boolean isUnifiable() {
-                return false;
-        }
-
-        @Override
         public abstract AnyDataVariable renew(@Nullable String name);
 
         @Override
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 e71c69ac..9b62e545 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
@@ -8,6 +8,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.EquivalenceLiteral;
 import tools.refinery.store.query.literal.Literal;
 import tools.refinery.store.query.substitution.Substitution;
 import tools.refinery.store.query.valuation.Valuation;
@@ -90,4 +91,12 @@ public final class DataVariable<T> extends AnyDataVariable implements Term<T> {
         public int hashCode() {
                 return Objects.hash(super.hashCode(), type);
         }
+
+        public EquivalenceLiteral isEquivalent(DataVariable<T> other) {
+                return new EquivalenceLiteral(true, this, other);
+        }
+
+        public EquivalenceLiteral notEquivalent(DataVariable<T> other) {
+                return new EquivalenceLiteral(false, this, other);
+        }
 }
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 e466f1c9..2f9c8bf1 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
@@ -22,11 +22,6 @@ public final class NodeVariable extends Variable {
         }
 
         @Override
-        public boolean isUnifiable() {
-                return true;
-        }
-
-        @Override
         public NodeVariable renew(@Nullable String name) {
                 return Variable.of(name);
         }
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 89ef0d89..1b553704 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
@@ -38,8 +38,6 @@ public abstract sealed class Variable permits AnyDataVariable, NodeVariable {
                 return uniqueName;
         }
 
-        public abstract boolean isUnifiable();
-
         public abstract Variable renew(@Nullable String name);
 
         public abstract Variable renew();