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, 299 insertions, 84 deletions

diff --git a/subprojects/store-query/src/test/java/tools/refinery/store/query/DnfBuilderTest.java b/subprojects/store-query/src/test/java/tools/refinery/store/query/dnf/DnfBuilderLiteralEliminationTest.java
index 01e2ccf6..4edea401 100644
--- a/subprojects/store-query/src/test/java/tools/refinery/store/query/DnfBuilderTest.java
+++ b/subprojects/store-query/src/test/java/tools/refinery/store/query/dnf/DnfBuilderLiteralEliminationTest.java
@@ -3,31 +3,36 @@
  *
  * SPDX-License-Identifier: EPL-2.0
  */
-package tools.refinery.store.query;
+package tools.refinery.store.query.dnf;
 
 import org.junit.jupiter.api.Test;
 import org.junit.jupiter.params.ParameterizedTest;
 import org.junit.jupiter.params.provider.CsvSource;
-import tools.refinery.store.query.dnf.Dnf;
 import tools.refinery.store.query.literal.BooleanLiteral;
+import tools.refinery.store.query.term.NodeVariable;
 import tools.refinery.store.query.term.Variable;
 import tools.refinery.store.query.term.bool.BoolTerms;
 import tools.refinery.store.query.view.KeyOnlyView;
+import tools.refinery.store.query.view.SymbolView;
 import tools.refinery.store.representation.Symbol;
 
+import java.util.List;
+
 import static org.hamcrest.MatcherAssert.assertThat;
 import static tools.refinery.store.query.literal.Literals.assume;
 import static tools.refinery.store.query.literal.Literals.not;
 import static tools.refinery.store.query.tests.QueryMatchers.structurallyEqualTo;
 
-class DnfBuilderTest {
+class DnfBuilderLiteralEliminationTest {
+        private final Symbol<Boolean> friend = new Symbol<>("friend", 2, Boolean.class, false);
+        private final SymbolView<Boolean> friendView = new KeyOnlyView<>(friend);
+        private final NodeVariable p = Variable.of("p");
+        private final NodeVariable q = Variable.of("q");
+        private final Dnf trueDnf = Dnf.builder().parameter(p).clause().build();
+        private final Dnf falseDnf = Dnf.builder().parameter(p).build();
+
         @Test
         void eliminateTrueTest() {
-                var p = Variable.of("p");
-                var q = Variable.of("q");
-                var friend = new Symbol<>("friend", 2, Boolean.class, false);
-                var friendView = new KeyOnlyView<>(friend);
-
                 var actual = Dnf.builder()
                                 .parameters(p, q)
                                 .clause(BooleanLiteral.TRUE, friendView.call(p, q))
@@ -39,11 +44,6 @@ class DnfBuilderTest {
 
         @Test
         void eliminateTrueAssumptionTest() {
-                var p = Variable.of("p");
-                var q = Variable.of("q");
-                var friend = new Symbol<>("friend", 2, Boolean.class, false);
-                var friendView = new KeyOnlyView<>(friend);
-
                 var actual = Dnf.builder()
                                 .parameters(p, q)
                                 .clause(assume(BoolTerms.constant(true)), friendView.call(p, q))
@@ -55,11 +55,6 @@ class DnfBuilderTest {
 
         @Test
         void eliminateFalseTest() {
-                var p = Variable.of("p");
-                var q = Variable.of("q");
-                var friend = new Symbol<>("friend", 2, Boolean.class, false);
-                var friendView = new KeyOnlyView<>(friend);
-
                 var actual = Dnf.builder()
                                 .parameters(p, q)
                                 .clause(friendView.call(p, q))
@@ -76,11 +71,6 @@ class DnfBuilderTest {
                         "null"
         }, nullValues = "null")
         void eliminateFalseAssumptionTest(Boolean value) {
-                var p = Variable.of("p");
-                var q = Variable.of("q");
-                var friend = new Symbol<>("friend", 2, Boolean.class, false);
-                var friendView = new KeyOnlyView<>(friend);
-
                 var actual = Dnf.builder()
                                 .parameters(p, q)
                                 .clause(friendView.call(p, q))
@@ -93,11 +83,6 @@ class DnfBuilderTest {
 
         @Test
         void alwaysTrueTest() {
-                var p = Variable.of("p");
-                var q = Variable.of("q");
-                var friend = new Symbol<>("friend", 2, Boolean.class, false);
-                var friendView = new KeyOnlyView<>(friend);
-
                 var actual = Dnf.builder()
                                 .parameters(p, q)
                                 .clause(friendView.call(p, q))
@@ -110,11 +95,6 @@ class DnfBuilderTest {
 
         @Test
         void alwaysFalseTest() {
-                var p = Variable.of("p");
-                var q = Variable.of("q");
-                var friend = new Symbol<>("friend", 2, Boolean.class, false);
-                var friendView = new KeyOnlyView<>(friend);
-
                 var actual = Dnf.builder()
                                 .parameters(p, q)
                                 .clause(friendView.call(p, q), BooleanLiteral.FALSE)
@@ -126,12 +106,6 @@ class DnfBuilderTest {
 
         @Test
         void eliminateTrueDnfTest() {
-                var p = Variable.of("p");
-                var q = Variable.of("q");
-                var friend = new Symbol<>("friend", 2, Boolean.class, false);
-                var friendView = new KeyOnlyView<>(friend);
-                var trueDnf = Dnf.builder().parameter(p).clause().build();
-
                 var actual = Dnf.builder()
                                 .parameters(p, q)
                                 .clause(trueDnf.call(q), friendView.call(p, q))
@@ -143,12 +117,6 @@ class DnfBuilderTest {
 
         @Test
         void eliminateFalseDnfTest() {
-                var p = Variable.of("p");
-                var q = Variable.of("q");
-                var friend = new Symbol<>("friend", 2, Boolean.class, false);
-                var friendView = new KeyOnlyView<>(friend);
-                var falseDnf = Dnf.builder().parameter(p).build();
-
                 var actual = Dnf.builder()
                                 .parameters(p, q)
                                 .clause(friendView.call(p, q))
@@ -161,12 +129,6 @@ class DnfBuilderTest {
 
         @Test
         void alwaysTrueDnfTest() {
-                var p = Variable.of("p");
-                var q = Variable.of("q");
-                var friend = new Symbol<>("friend", 2, Boolean.class, false);
-                var friendView = new KeyOnlyView<>(friend);
-                var trueDnf = Dnf.builder().parameter(p).clause().build();
-
                 var actual = Dnf.builder()
                                 .parameters(p, q)
                                 .clause(friendView.call(p, q))
@@ -179,12 +141,6 @@ class DnfBuilderTest {
 
         @Test
         void alwaysFalseDnfTest() {
-                var p = Variable.of("p");
-                var q = Variable.of("q");
-                var friend = new Symbol<>("friend", 2, Boolean.class, false);
-                var friendView = new KeyOnlyView<>(friend);
-                var falseDnf = Dnf.builder().parameter(p).build();
-
                 var actual = Dnf.builder()
                                 .parameters(p, q)
                                 .clause(friendView.call(p, q), falseDnf.call(q))
@@ -196,12 +152,6 @@ class DnfBuilderTest {
 
         @Test
         void eliminateNotFalseDnfTest() {
-                var p = Variable.of("p");
-                var q = Variable.of("q");
-                var friend = new Symbol<>("friend", 2, Boolean.class, false);
-                var friendView = new KeyOnlyView<>(friend);
-                var falseDnf = Dnf.builder().parameter(p).build();
-
                 var actual = Dnf.builder()
                                 .parameters(p, q)
                                 .clause(not(falseDnf.call(q)), friendView.call(p, q))
@@ -213,12 +163,6 @@ class DnfBuilderTest {
 
         @Test
         void eliminateNotTrueDnfTest() {
-                var p = Variable.of("p");
-                var q = Variable.of("q");
-                var friend = new Symbol<>("friend", 2, Boolean.class, false);
-                var friendView = new KeyOnlyView<>(friend);
-                var trueDnf = Dnf.builder().parameter(p).clause().build();
-
                 var actual = Dnf.builder()
                                 .parameters(p, q)
                                 .clause(friendView.call(p, q))
@@ -231,12 +175,6 @@ class DnfBuilderTest {
 
         @Test
         void alwaysNotFalseDnfTest() {
-                var p = Variable.of("p");
-                var q = Variable.of("q");
-                var friend = new Symbol<>("friend", 2, Boolean.class, false);
-                var friendView = new KeyOnlyView<>(friend);
-                var falseDnf = Dnf.builder().parameter(p).build();
-
                 var actual = Dnf.builder()
                                 .parameters(p, q)
                                 .clause(friendView.call(p, q))
@@ -249,12 +187,6 @@ class DnfBuilderTest {
 
         @Test
         void alwaysNotTrueDnfTest() {
-                var p = Variable.of("p");
-                var q = Variable.of("q");
-                var friend = new Symbol<>("friend", 2, Boolean.class, false);
-                var friendView = new KeyOnlyView<>(friend);
-                var trueDnf = Dnf.builder().parameter(p).clause().build();
-
                 var actual = Dnf.builder()
                                 .parameters(p, q)
                                 .clause(friendView.call(p, q), not(trueDnf.call(q)))
@@ -263,4 +195,15 @@ class DnfBuilderTest {
 
                 assertThat(actual, structurallyEqualTo(expected));
         }
+
+        @Test
+        void removeDuplicateTest() {
+                var actual = Dnf.of(builder -> builder.clause((p, q) -> List.of(
+                                friendView.call(p, q),
+                                friendView.call(p, q)
+                )));
+                var expected = Dnf.of(builder -> builder.clause((p, q) -> List.of(friendView.call(p, q))));
+
+                assertThat(actual, structurallyEqualTo(expected));
+        }
 }
diff --git a/subprojects/store-query/src/test/java/tools/refinery/store/query/dnf/DnfBuilderVariableUnificationTest.java b/subprojects/store-query/src/test/java/tools/refinery/store/query/dnf/DnfBuilderVariableUnificationTest.java
new file mode 100644
index 00000000..a54ad4d6
--- /dev/null
+++ b/subprojects/store-query/src/test/java/tools/refinery/store/query/dnf/DnfBuilderVariableUnificationTest.java
@@ -0,0 +1,273 @@
+/*
+ * SPDX-FileCopyrightText: 2021-2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.query.dnf;
+
+import org.junit.jupiter.api.Test;
+import tools.refinery.store.query.view.KeyOnlyView;
+import tools.refinery.store.query.view.SymbolView;
+import tools.refinery.store.representation.Symbol;
+
+import java.util.List;
+
+import static org.hamcrest.MatcherAssert.assertThat;
+import static tools.refinery.store.query.tests.QueryMatchers.structurallyEqualTo;
+
+class DnfBuilderVariableUnificationTest {
+        private final Symbol<Boolean> friend = new Symbol<>("friend", 2, Boolean.class, false);
+        private final Symbol<Boolean> children = new Symbol<>("friend", 2, Boolean.class, false);
+        private final SymbolView<Boolean> friendView = new KeyOnlyView<>(friend);
+        private final SymbolView<Boolean> childrenView = new KeyOnlyView<>(children);
+
+        @Test
+        void equalToParameterTest() {
+                var actual = Dnf.of(builder -> {
+                        var p = builder.parameter("p");
+                        builder.clause(q -> List.of(
+                                        friendView.call(p, q),
+                                        p.isEquivalent(q)
+                        ));
+                });
+                var expected = Dnf.of(builder -> {
+                        var p = builder.parameter("p");
+                        builder.clause(friendView.call(p, p));
+                });
+
+                assertThat(actual, structurallyEqualTo(expected));
+        }
+
+        @Test
+        void equalToParameterReverseTest() {
+                var actual = Dnf.of(builder -> {
+                        var p = builder.parameter("p");
+                        builder.clause(q -> List.of(
+                                        friendView.call(p, q),
+                                        q.isEquivalent(p)
+                        ));
+                });
+                var expected = Dnf.of(builder -> {
+                        var p = builder.parameter("p");
+                        builder.clause(friendView.call(p, p));
+                });
+
+                assertThat(actual, structurallyEqualTo(expected));
+        }
+
+        @Test
+        void equalQuantifiedTest() {
+                var actual = Dnf.of(builder -> builder.clause((p, q) -> List.of(
+                                friendView.call(p, q),
+                                p.isEquivalent(q)
+                )));
+                var expected = Dnf.of(builder -> builder.clause(p -> List.of(friendView.call(p, p))));
+
+                assertThat(actual, structurallyEqualTo(expected));
+        }
+
+        @Test
+        void equalQuantifiedTransitiveTest() {
+                var actual = Dnf.of(builder -> builder.clause((p, q, r) -> List.of(
+                                friendView.call(p, q),
+                                p.isEquivalent(q),
+                                childrenView.call(p, r),
+                                q.isEquivalent(r)
+                )));
+                var expected = Dnf.of(builder -> builder.clause(p -> List.of(
+                                friendView.call(p, p),
+                                childrenView.call(p, p)
+                )));
+
+                assertThat(actual, structurallyEqualTo(expected));
+        }
+
+        @Test
+        void equalQuantifiedTransitiveRemoveDuplicateTest() {
+                var actual = Dnf.of(builder -> builder.clause((p, q, r) -> List.of(
+                                friendView.call(p, q),
+                                p.isEquivalent(q),
+                                friendView.call(p, r),
+                                q.isEquivalent(r)
+                )));
+                var expected = Dnf.of(builder -> builder.clause(p -> List.of(friendView.call(p, p))));
+
+                assertThat(actual, structurallyEqualTo(expected));
+        }
+
+        @Test
+        void parametersEqualTest() {
+                var actual = Dnf.of(builder -> {
+                        var p = builder.parameter("p");
+                        var q = builder.parameter("q");
+                        builder.clause(
+                                        friendView.call(p, q),
+                                        p.isEquivalent(q)
+                        );
+                });
+                var expected = Dnf.of(builder -> {
+                        var p = builder.parameter("p");
+                        var q = builder.parameter("q");
+                        builder.clause(
+                                        q.isEquivalent(p),
+                                        friendView.call(p, p)
+                        );
+                });
+
+                assertThat(actual, structurallyEqualTo(expected));
+        }
+
+        @Test
+        void parametersEqualTransitiveTest() {
+                var actual = Dnf.of(builder -> {
+                        var p = builder.parameter("p");
+                        var q = builder.parameter("q");
+                        var r = builder.parameter("r");
+                        builder.clause(
+                                        friendView.call(p, q),
+                                        childrenView.call(p, r),
+                                        p.isEquivalent(q),
+                                        r.isEquivalent(q)
+                        );
+                });
+                var expected = Dnf.of(builder -> {
+                        var p = builder.parameter("p");
+                        var q = builder.parameter("q");
+                        var r = builder.parameter("r");
+                        builder.clause(
+                                        q.isEquivalent(p),
+                                        r.isEquivalent(p),
+                                        friendView.call(p, p),
+                                        childrenView.call(p, p)
+                        );
+                });
+
+                assertThat(actual, structurallyEqualTo(expected));
+        }
+
+        @Test
+        void parameterAndQuantifiedEqualsTest() {
+                var actual = Dnf.of(builder -> {
+                        var p = builder.parameter("p");
+                        var q = builder.parameter("q");
+                        builder.clause((r) -> List.of(
+                                        friendView.call(p, r),
+                                        p.isEquivalent(r),
+                                        childrenView.call(q, r),
+                                        q.isEquivalent(r)
+                        ));
+                });
+                var expected = Dnf.of(builder -> {
+                        var p = builder.parameter("p");
+                        var q = builder.parameter("q");
+                        builder.clause(
+                                        q.isEquivalent(p),
+                                        friendView.call(p, p),
+                                        childrenView.call(p, p)
+                        );
+                });
+
+                assertThat(actual, structurallyEqualTo(expected));
+        }
+
+        @Test
+        void parameterAndQuantifiedEqualsReverseFirstTest() {
+                var actual = Dnf.of(builder -> {
+                        var p = builder.parameter("p");
+                        var q = builder.parameter("q");
+                        builder.clause((r) -> List.of(
+                                        friendView.call(p, r),
+                                        r.isEquivalent(p),
+                                        childrenView.call(q, r),
+                                        q.isEquivalent(r)
+                        ));
+                });
+                var expected = Dnf.of(builder -> {
+                        var p = builder.parameter("p");
+                        var q = builder.parameter("q");
+                        builder.clause(
+                                        q.isEquivalent(p),
+                                        friendView.call(p, p),
+                                        childrenView.call(p, p)
+                        );
+                });
+
+                assertThat(actual, structurallyEqualTo(expected));
+        }
+
+        @Test
+        void parameterAndQuantifiedEqualsReverseSecondTest() {
+                var actual = Dnf.of(builder -> {
+                        var p = builder.parameter("p");
+                        var q = builder.parameter("q");
+                        builder.clause((r) -> List.of(
+                                        friendView.call(p, r),
+                                        p.isEquivalent(r),
+                                        childrenView.call(q, r),
+                                        r.isEquivalent(q)
+                        ));
+                });
+                var expected = Dnf.of(builder -> {
+                        var p = builder.parameter("p");
+                        var q = builder.parameter("q");
+                        builder.clause(
+                                        q.isEquivalent(p),
+                                        friendView.call(p, p),
+                                        childrenView.call(p, p)
+                        );
+                });
+
+                assertThat(actual, structurallyEqualTo(expected));
+        }
+
+        @Test
+        void parameterAndQuantifiedEqualsReverseBoth() {
+                var actual = Dnf.of(builder -> {
+                        var p = builder.parameter("p");
+                        var q = builder.parameter("q");
+                        builder.clause((r) -> List.of(
+                                        friendView.call(p, r),
+                                        p.isEquivalent(r),
+                                        childrenView.call(q, r),
+                                        r.isEquivalent(q)
+                        ));
+                });
+                var expected = Dnf.of(builder -> {
+                        var p = builder.parameter("p");
+                        var q = builder.parameter("q");
+                        builder.clause(
+                                        q.isEquivalent(p),
+                                        friendView.call(p, p),
+                                        childrenView.call(p, p)
+                        );
+                });
+
+                assertThat(actual, structurallyEqualTo(expected));
+        }
+
+        @Test
+        void parameterAndTwoQuantifiedEqualsTest() {
+                var actual = Dnf.of(builder -> {
+                        var p = builder.parameter("p");
+                        var q = builder.parameter("q");
+                        builder.clause((r, s) -> List.of(
+                                        r.isEquivalent(s),
+                                        friendView.call(p, r),
+                                        p.isEquivalent(r),
+                                        childrenView.call(q, s),
+                                        q.isEquivalent(s)
+                        ));
+                });
+                var expected = Dnf.of(builder -> {
+                        var p = builder.parameter("p");
+                        var q = builder.parameter("q");
+                        builder.clause(
+                                        q.isEquivalent(p),
+                                        friendView.call(p, p),
+                                        childrenView.call(p, p)
+                        );
+                });
+
+                assertThat(actual, structurallyEqualTo(expected));
+        }
+}
diff --git a/subprojects/store-query/src/test/java/tools/refinery/store/query/DnfToDefinitionStringTest.java b/subprojects/store-query/src/test/java/tools/refinery/store/query/dnf/DnfToDefinitionStringTest.java
index e89ab682..2e93d78a 100644
--- a/subprojects/store-query/src/test/java/tools/refinery/store/query/DnfToDefinitionStringTest.java
+++ b/subprojects/store-query/src/test/java/tools/refinery/store/query/dnf/DnfToDefinitionStringTest.java
@@ -3,10 +3,9 @@
  *
  * SPDX-License-Identifier: EPL-2.0
  */
-package tools.refinery.store.query;
+package tools.refinery.store.query.dnf;
 
 import org.junit.jupiter.api.Test;
-import tools.refinery.store.query.dnf.Dnf;
 import tools.refinery.store.query.term.Variable;
 import tools.refinery.store.query.view.KeyOnlyView;
 import tools.refinery.store.representation.Symbol;
@@ -43,7 +42,7 @@ class DnfToDefinitionStringTest {
                 var dnf = Dnf.builder("Example").parameter(p).clause().build();
 
                 assertThat(dnf.toDefinitionString(), is("""
-                                pred Example(p) <->
+                                pred Example(@In p) <->
                                     <empty>.
                                 """));
         }