feat: query parameter binding validation

* Introduce parameter directions for constraints and DNF
* Introduce variable directions for literals
* Infer and check variable directions in DNF and topologically sort literals by
  their input variables

3 files changed, 24 insertions, 18 deletions

diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/lifting/DnfLifter.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/lifting/DnfLifter.java
index 594005f1..ac41d170 100644
--- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/lifting/DnfLifter.java
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/lifting/DnfLifter.java
@@ -12,7 +12,7 @@ import tools.refinery.store.query.dnf.DnfClause;
 import tools.refinery.store.query.literal.CallLiteral;
 import tools.refinery.store.query.literal.CallPolarity;
 import tools.refinery.store.query.literal.Literal;
-import tools.refinery.store.query.term.DataVariable;
+import tools.refinery.store.query.term.NodeVariable;
 import tools.refinery.store.query.term.Variable;
 import tools.refinery.store.reasoning.ReasoningAdapter;
 import tools.refinery.store.reasoning.literal.ModalConstraint;
@@ -21,7 +21,7 @@ import tools.refinery.store.reasoning.literal.PartialLiterals;
 import tools.refinery.store.util.CycleDetectingMapper;
 
 import java.util.ArrayList;
-import java.util.HashSet;
+import java.util.LinkedHashSet;
 import java.util.List;
 
 public class DnfLifter {
@@ -36,10 +36,10 @@ public class DnfLifter {
                 var modality = modalDnf.modality();
                 var dnf = modalDnf.dnf();
                 var builder = Dnf.builder();
-                builder.parameters(dnf.getParameters());
+                builder.symbolicParameters(dnf.getSymbolicParameters());
                 boolean changed = false;
                 for (var clause : dnf.getClauses()) {
-                        if (liftClause(modality, clause, builder)) {
+                        if (liftClause(modality, dnf, clause, builder)) {
                                 changed = true;
                         }
                 }
@@ -49,12 +49,9 @@ public class DnfLifter {
                 return dnf;
         }
 
-        private boolean liftClause(Modality modality, DnfClause clause, DnfBuilder builder) {
+        private boolean liftClause(Modality modality, Dnf originalDnf, DnfClause clause, DnfBuilder builder) {
                 boolean changed = false;
-                var quantifiedVariables = new HashSet<>(clause.boundVariables()
-                                .stream()
-                                .filter(DataVariable.class::isInstance)
-                                .toList());
+                var quantifiedVariables = getQuantifiedDataVariables(originalDnf, clause);
                 var literals = clause.literals();
                 var liftedLiterals = new ArrayList<Literal>(literals.size());
                 for (var literal : literals) {
@@ -81,6 +78,16 @@ public class DnfLifter {
                 return changed || !quantifiedVariables.isEmpty();
         }
 
+        private static LinkedHashSet<Variable> getQuantifiedDataVariables(Dnf originalDnf, DnfClause clause) {
+                var quantifiedVariables = new LinkedHashSet<>(clause.positiveVariables());
+                for (var symbolicParameter : originalDnf.getSymbolicParameters()) {
+                        // The existence of parameters will be checked outside this DNF.
+                        quantifiedVariables.remove(symbolicParameter.getVariable());
+                }
+                quantifiedVariables.removeIf(variable -> !(variable instanceof NodeVariable));
+                return quantifiedVariables;
+        }
+
         @Nullable
         private Variable isExistsLiteralForVariable(Modality modality, Literal literal) {
                 if (literal instanceof CallLiteral callLiteral &&
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/literal/ModalConstraint.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/literal/ModalConstraint.java
index 7fa98104..ce557d82 100644
--- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/literal/ModalConstraint.java
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/literal/ModalConstraint.java
@@ -8,7 +8,7 @@ package tools.refinery.store.reasoning.literal;
 import tools.refinery.store.query.Constraint;
 import tools.refinery.store.query.equality.LiteralEqualityHelper;
 import tools.refinery.store.query.literal.LiteralReduction;
-import tools.refinery.store.query.term.Sort;
+import tools.refinery.store.query.term.Parameter;
 
 import java.util.List;
 
@@ -21,8 +21,8 @@ public record ModalConstraint(Modality modality, Constraint constraint) implemen
         }
 
         @Override
-        public List<Sort> getSorts() {
-                return constraint.getSorts();
+        public List<Parameter> getParameters() {
+                return constraint.getParameters();
         }
 
         @Override
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/representation/PartialRelation.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/representation/PartialRelation.java
index fc3dc074..1f74ce38 100644
--- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/representation/PartialRelation.java
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/representation/PartialRelation.java
@@ -6,8 +6,7 @@
 package tools.refinery.store.reasoning.representation;
 
 import tools.refinery.store.query.Constraint;
-import tools.refinery.store.query.term.NodeSort;
-import tools.refinery.store.query.term.Sort;
+import tools.refinery.store.query.term.Parameter;
 import tools.refinery.store.representation.AbstractDomain;
 import tools.refinery.store.representation.TruthValue;
 import tools.refinery.store.representation.TruthValueDomain;
@@ -32,10 +31,10 @@ public record PartialRelation(String name, int arity) implements PartialSymbol<T
         }
 
         @Override
-        public List<Sort> getSorts() {
-                var sorts = new Sort[arity()];
-                Arrays.fill(sorts, NodeSort.INSTANCE);
-                return List.of(sorts);
+        public List<Parameter> getParameters() {
+                var parameters = new Parameter[arity];
+                Arrays.fill(parameters, Parameter.NODE_IN_OUT);
+                return List.of(parameters);
         }
 
         @Override