5 files changed, 131 insertions, 191 deletions

diff --git a/subprojects/store-query/src/test/java/tools/refinery/store/query/dnf/DnfBuilderLiteralEliminationTest.java b/subprojects/store-query/src/test/java/tools/refinery/store/query/dnf/DnfBuilderLiteralEliminationTest.java
index e17496e3..6a2dc0c7 100644
--- a/subprojects/store-query/src/test/java/tools/refinery/store/query/dnf/DnfBuilderLiteralEliminationTest.java
+++ b/subprojects/store-query/src/test/java/tools/refinery/store/query/dnf/DnfBuilderLiteralEliminationTest.java
@@ -20,7 +20,7 @@ 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.check;
 import static tools.refinery.store.query.literal.Literals.not;
 import static tools.refinery.store.query.tests.QueryMatchers.structurallyEqualTo;
 
@@ -47,7 +47,7 @@ class DnfBuilderLiteralEliminationTest {
         void eliminateTrueAssumptionTest() {
                 var actual = Dnf.builder()
                                 .parameters(p, q)
-                                .clause(assume(BoolTerms.constant(true)), friendView.call(p, q))
+                                .clause(check(BoolTerms.constant(true)), friendView.call(p, q))
                                 .build();
                 var expected = Dnf.builder().parameters(p, q).clause(friendView.call(p, q)).build();
 
@@ -75,7 +75,7 @@ class DnfBuilderLiteralEliminationTest {
                 var actual = Dnf.builder()
                                 .parameters(p, q)
                                 .clause(friendView.call(p, q))
-                                .clause(friendView.call(q, p), assume(BoolTerms.constant(value)))
+                                .clause(friendView.call(q, p), check(BoolTerms.constant(value)))
                                 .build();
                 var expected = Dnf.builder().parameters(p, q).clause(friendView.call(p, q)).build();
 
@@ -207,4 +207,53 @@ class DnfBuilderLiteralEliminationTest {
 
                 assertThat(actual, structurallyEqualTo(expected));
         }
+
+        @Test
+        void removeContradictoryTest() {
+                var actual = Dnf.of(builder -> builder.clause((p, q) -> List.of(
+                                friendView.call(p, q),
+                                not(friendView.call(p, q))
+                )));
+                var expected = Dnf.builder().build();
+
+                assertThat(actual, structurallyEqualTo(expected));
+        }
+
+        @Test
+        void removeContradictoryUniversalTest() {
+                var actual = Dnf.of(builder -> builder.clause((p, q) -> List.of(
+                                friendView.call(q, q),
+                                friendView.call(p, q),
+                                not(friendView.call(p, Variable.of()))
+                )));
+                var expected = Dnf.builder().build();
+
+                assertThat(actual, structurallyEqualTo(expected));
+        }
+
+        @Test
+        void removeContradictoryExistentialUniversalTest() {
+                var actual = Dnf.of(builder -> builder.clause((p) -> List.of(
+                                friendView.call(p, Variable.of()),
+                                not(friendView.call(p, Variable.of()))
+                )));
+                var expected = Dnf.builder().build();
+
+                assertThat(actual, structurallyEqualTo(expected));
+        }
+
+        @Test
+        void removeContradictoryUniversalParameterTest() {
+                var actual = Dnf.of(builder -> {
+                        var p = builder.parameter("p");
+                        builder.clause((q) -> List.of(
+                                        friendView.call(q, q),
+                                        friendView.call(p, q),
+                                        not(friendView.call(p, Variable.of()))
+                        ));
+                });
+                var expected = Dnf.builder().parameter(p).build();
+
+                assertThat(actual, structurallyEqualTo(expected));
+        }
 }
diff --git a/subprojects/store-query/src/test/java/tools/refinery/store/query/dnf/DnfToDefinitionStringTest.java b/subprojects/store-query/src/test/java/tools/refinery/store/query/dnf/DnfToDefinitionStringTest.java
index d75d7f17..12cfaa4e 100644
--- a/subprojects/store-query/src/test/java/tools/refinery/store/query/dnf/DnfToDefinitionStringTest.java
+++ b/subprojects/store-query/src/test/java/tools/refinery/store/query/dnf/DnfToDefinitionStringTest.java
@@ -50,7 +50,7 @@ class DnfToDefinitionStringTest {
                 var dnf = Dnf.builder("Example").parameter(p, ParameterDirection.IN).clause().build();
 
                 assertThat(dnf.toDefinitionString(), is("""
-                                pred Example(@In p) <->
+                                pred Example(in p) <->
                                     <empty>.
                                 """));
         }
@@ -73,7 +73,7 @@ class DnfToDefinitionStringTest {
                                 .build();
 
                 assertThat(dnf.toDefinitionString(), is("""
-                                pred Example(@In p) <->
+                                pred Example(in p) <->
                                     !(@RelationView("key") friend(p, q)).
                                 """));
         }
diff --git a/subprojects/store-query/src/test/java/tools/refinery/store/query/dnf/HashCodeTest.java b/subprojects/store-query/src/test/java/tools/refinery/store/query/dnf/HashCodeTest.java
new file mode 100644
index 00000000..0c8eaeed
--- /dev/null
+++ b/subprojects/store-query/src/test/java/tools/refinery/store/query/dnf/HashCodeTest.java
@@ -0,0 +1,67 @@
+/*
+ * SPDX-FileCopyrightText: 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.term.NodeVariable;
+import tools.refinery.store.query.term.Variable;
+import tools.refinery.store.query.view.AnySymbolView;
+import tools.refinery.store.query.view.KeyOnlyView;
+import tools.refinery.store.representation.Symbol;
+
+import static org.hamcrest.MatcherAssert.assertThat;
+import static org.hamcrest.Matchers.is;
+import static org.hamcrest.Matchers.not;
+
+class HashCodeTest {
+        private static final Symbol<Boolean> person = Symbol.of("Person", 1);
+        private static final Symbol<Boolean> friend = Symbol.of("friend", 2);
+        private static final AnySymbolView personView = new KeyOnlyView<>(person);
+        private static final AnySymbolView friendView = new KeyOnlyView<>(friend);
+        private static final NodeVariable p = Variable.of("p");
+        private static final NodeVariable q = Variable.of("q");
+
+        @Test
+        void flatEqualsTest() {
+                var expected = Dnf.builder("Expected").parameters(q).clause(personView.call(q)).build();
+                var actual = Dnf.builder("Actual").parameters(p).clause(personView.call(p)).build();
+
+                assertThat(actual.hashCodeWithSubstitution(), is(expected.hashCodeWithSubstitution()));
+        }
+
+        @Test
+        void flatNotEqualsTest() {
+                var expected = Dnf.builder("Expected").parameters(q).clause(friendView.call(q, q)).build();
+                var actual = Dnf.builder("Actual").parameters(p).clause(friendView.call(p, q)).build();
+
+                assertThat(actual.hashCodeWithSubstitution(), not(expected.hashCodeWithSubstitution()));
+        }
+
+        @Test
+        void deepEqualsTest() {
+                var expected2 = Dnf.builder("Expected2").parameters(p).clause(personView.call(p)).build();
+                var expected = Dnf.builder("Expected").parameters(q).clause(
+                                expected2.call(q)
+                ).build();
+                var actual = Dnf.builder("Actual").parameters(q).clause(
+                                expected2.call(q)
+                ).build();
+
+                assertThat(actual.hashCodeWithSubstitution(), is(expected.hashCodeWithSubstitution()));
+        }
+
+        @Test
+        void deepNotEqualsTest() {
+                var expected = Dnf.builder("Expected").parameters(q).clause(
+                                Dnf.builder("Expected2").parameters(p).clause(personView.call(p)).build().call(q)
+                ).build();
+                var actual = Dnf.builder("Actual").parameters(q).clause(
+                                Dnf.builder("Actual2").parameters(p).clause(personView.call(p)).build().call(q)
+                ).build();
+
+                assertThat(actual.hashCodeWithSubstitution(), not(expected.hashCodeWithSubstitution()));
+        }
+}
diff --git a/subprojects/store-query/src/test/java/tools/refinery/store/query/dnf/TopologicalSortTest.java b/subprojects/store-query/src/test/java/tools/refinery/store/query/dnf/TopologicalSortTest.java
index e22dbb21..854bd469 100644
--- a/subprojects/store-query/src/test/java/tools/refinery/store/query/dnf/TopologicalSortTest.java
+++ b/subprojects/store-query/src/test/java/tools/refinery/store/query/dnf/TopologicalSortTest.java
@@ -6,6 +6,7 @@
 package tools.refinery.store.query.dnf;
 
 import org.junit.jupiter.api.Test;
+import tools.refinery.store.query.InvalidQueryException;
 import tools.refinery.store.query.term.NodeVariable;
 import tools.refinery.store.query.term.ParameterDirection;
 import tools.refinery.store.query.term.Variable;
@@ -80,7 +81,7 @@ class TopologicalSortTest {
                                                 example.call(r, t, q, s),
                                                 friendView.call(r, t)
                                 );
-                assertThrows(IllegalArgumentException.class, builder::build);
+                assertThrows(InvalidQueryException.class, builder::build);
         }
 
         @Test
@@ -93,7 +94,7 @@ class TopologicalSortTest {
                                                 example.call(p, q, r, s),
                                                 example.call(r, t, q, s)
                                 );
-                assertThrows(IllegalArgumentException.class, builder::build);
+                assertThrows(InvalidQueryException.class, builder::build);
         }
 
         @Test
@@ -107,6 +108,6 @@ class TopologicalSortTest {
                                                 example.call(r, t, q, s),
                                                 example.call(p, q, r, t)
                                 );
-                assertThrows(IllegalArgumentException.class, builder::build);
+                assertThrows(InvalidQueryException.class, builder::build);
         }
 }
diff --git a/subprojects/store-query/src/test/java/tools/refinery/store/query/dnf/VariableDirectionTest.java b/subprojects/store-query/src/test/java/tools/refinery/store/query/dnf/VariableDirectionTest.java
index c52d26b2..fc3f5d48 100644
--- a/subprojects/store-query/src/test/java/tools/refinery/store/query/dnf/VariableDirectionTest.java
+++ b/subprojects/store-query/src/test/java/tools/refinery/store/query/dnf/VariableDirectionTest.java
@@ -28,9 +28,8 @@ import static org.hamcrest.Matchers.hasItem;
 import static org.hamcrest.Matchers.not;
 import static org.junit.jupiter.api.Assertions.assertDoesNotThrow;
 import static org.junit.jupiter.api.Assertions.assertThrows;
-import static tools.refinery.store.query.literal.Literals.assume;
 import static tools.refinery.store.query.literal.Literals.not;
-import static tools.refinery.store.query.term.int_.IntTerms.*;
+import static tools.refinery.store.query.term.int_.IntTerms.INT_SUM;
 
 class VariableDirectionTest {
         private static final Symbol<Boolean> person = Symbol.of("Person", 1);
@@ -49,7 +48,7 @@ class VariableDirectionTest {
         @MethodSource("clausesWithVariableInput")
         void unboundOutVariableTest(List<? extends Literal> clause) {
                 var builder = Dnf.builder().parameter(p, ParameterDirection.OUT).clause(clause);
-                assertThrows(IllegalArgumentException.class, builder::build);
+                assertThrows(InvalidClauseException.class, builder::build);
         }
 
         @ParameterizedTest
@@ -101,7 +100,7 @@ class VariableDirectionTest {
                 var clauseWithEquivalence = new ArrayList<Literal>(clause);
                 clauseWithEquivalence.add(r.isEquivalent(p));
                 var builder = Dnf.builder().clause(clauseWithEquivalence);
-                assertThrows(IllegalArgumentException.class, builder::build);
+                assertThrows(InvalidClauseException.class, builder::build);
         }
 
         static Stream<Arguments> clausesNotBindingVariable() {
@@ -119,7 +118,7 @@ class VariableDirectionTest {
         @MethodSource("literalsWithPrivateVariable")
         void unboundTwicePrivateVariableTest(Literal literal) {
                 var builder = Dnf.builder().clause(not(personView.call(p)), literal);
-                assertThrows(IllegalArgumentException.class, builder::build);
+                assertThrows(InvalidClauseException.class, builder::build);
         }
 
         @ParameterizedTest
@@ -127,7 +126,7 @@ class VariableDirectionTest {
         void unboundTwiceByEquivalencePrivateVariableTest(Literal literal) {
                 var r = Variable.of("r");
                 var builder = Dnf.builder().clause(not(personView.call(r)), r.isEquivalent(p), literal);
-                assertThrows(IllegalArgumentException.class, builder::build);
+                assertThrows(InvalidClauseException.class, builder::build);
         }
 
         static Stream<Arguments> literalsWithPrivateVariable() {
@@ -160,7 +159,7 @@ class VariableDirectionTest {
         @MethodSource("literalsWithRequiredVariableInput")
         void unboundPrivateVariableTest(Literal literal) {
                 var builder = Dnf.builder().clause(literal);
-                assertThrows(IllegalArgumentException.class, builder::build);
+                assertThrows(InvalidClauseException.class, builder::build);
         }
 
         @ParameterizedTest
@@ -246,182 +245,6 @@ class VariableDirectionTest {
                 );
         }
 
-        @ParameterizedTest
-        @MethodSource("clausesWithDataVariableInput")
-        void unboundOutDataVariableTest(List<? extends Literal> clause) {
-                var builder = Dnf.builder().parameter(x, ParameterDirection.OUT).clause(clause);
-                assertThrows(IllegalArgumentException.class, builder::build);
-        }
-
-        @ParameterizedTest
-        @MethodSource("clausesWithDataVariableInput")
-        void unboundInDataVariableTest(List<? extends Literal> clause) {
-                var builder = Dnf.builder().parameter(x, ParameterDirection.IN).clause(clause);
-                var dnf = assertDoesNotThrow(builder::build);
-                var clauses = dnf.getClauses();
-                if (clauses.size() > 0) {
-                        assertThat(clauses.get(0).positiveVariables(), hasItem(x));
-                }
-        }
-
-        @ParameterizedTest
-        @MethodSource("clausesWithDataVariableInput")
-        void boundPrivateDataVariableTest(List<? extends Literal> clause) {
-                var clauseWithBinding = new ArrayList<Literal>(clause);
-                clauseWithBinding.add(x.assign(constant(27)));
-                var builder = Dnf.builder().clause(clauseWithBinding);
-                var dnf = assertDoesNotThrow(builder::build);
-                var clauses = dnf.getClauses();
-                if (clauses.size() > 0) {
-                        assertThat(clauses.get(0).positiveVariables(), hasItem(x));
-                }
-        }
-
-        static Stream<Arguments> clausesWithDataVariableInput() {
-                return Stream.concat(
-                                clausesNotBindingDataVariable(),
-                                literalToClauseArgumentStream(literalsWithRequiredDataVariableInput())
-                );
-        }
-
-        @ParameterizedTest
-        @MethodSource("clausesNotBindingDataVariable")
-        void unboundPrivateDataVariableTest(List<? extends Literal> clause) {
-                var builder = Dnf.builder().clause(clause);
-                var dnf = assertDoesNotThrow(builder::build);
-                var clauses = dnf.getClauses();
-                if (clauses.size() > 0) {
-                        assertThat(clauses.get(0).positiveVariables(), not(hasItem(x)));
-                }
-        }
-
-        static Stream<Arguments> clausesNotBindingDataVariable() {
-                return Stream.concat(
-                                Stream.of(
-                                                Arguments.of(List.of()),
-                                                Arguments.of(List.of(BooleanLiteral.TRUE)),
-                                                Arguments.of(List.of(BooleanLiteral.FALSE))
-                                ),
-                                literalToClauseArgumentStream(literalsWithPrivateDataVariable())
-                );
-        }
-
-        @ParameterizedTest
-        @MethodSource("literalsWithPrivateDataVariable")
-        void unboundTwicePrivateDataVariableTest(Literal literal) {
-                var builder = Dnf.builder().clause(not(ageView.call(p, x)), literal);
-                assertThrows(IllegalArgumentException.class, builder::build);
-        }
-
-        static Stream<Arguments> literalsWithPrivateDataVariable() {
-                var dnfWithOutput = Dnf.builder("WithDataOutput")
-                                .parameter(y, ParameterDirection.OUT)
-                                .parameter(q, ParameterDirection.OUT)
-                                .clause(ageView.call(q, y))
-                                .build();
-
-                return Stream.of(
-                                Arguments.of(not(ageView.call(q, x))),
-                                Arguments.of(y.assign(ageView.count(q, x))),
-                                Arguments.of(not(dnfWithOutput.call(x, q)))
-                );
-        }
-
-        @ParameterizedTest
-        @MethodSource("literalsWithRequiredDataVariableInput")
-        void unboundPrivateDataVariableTest(Literal literal) {
-                var builder = Dnf.builder().clause(literal);
-                assertThrows(IllegalArgumentException.class, builder::build);
-        }
-
-        static Stream<Arguments> literalsWithRequiredDataVariableInput() {
-                var dnfWithInput = Dnf.builder("WithDataInput")
-                                .parameter(y, ParameterDirection.IN)
-                                .parameter(q, ParameterDirection.OUT)
-                                .clause(ageView.call(q, x))
-                                .build();
-                // We are passing {@code y} to the parameter named {@code right} of {@code greaterEq}.
-                @SuppressWarnings("SuspiciousNameCombination")
-                var dnfWithInputToAggregate = Dnf.builder("WithDataInputToAggregate")
-                                .parameter(y, ParameterDirection.IN)
-                                .parameter(q, ParameterDirection.OUT)
-                                .parameter(x, ParameterDirection.OUT)
-                                .clause(
-                                                friendView.call(p, q),
-                                                ageView.call(q, x),
-                                                assume(greaterEq(x, y))
-                                )
-                                .build();
-
-                return Stream.of(
-                                Arguments.of(dnfWithInput.call(x, q)),
-                                Arguments.of(not(dnfWithInput.call(x, q))),
-                                Arguments.of(y.assign(dnfWithInput.count(x, q))),
-                                Arguments.of(y.assign(dnfWithInputToAggregate.aggregateBy(z, INT_SUM, x, q, z)))
-                );
-        }
-
-        @ParameterizedTest
-        @MethodSource("literalsWithDataVariableOutput")
-        void boundDataParameterTest(Literal literal) {
-                var builder = Dnf.builder().parameter(x, ParameterDirection.OUT).clause(literal);
-                var dnf = assertDoesNotThrow(builder::build);
-                assertThat(dnf.getClauses().get(0).positiveVariables(), hasItem(x));
-        }
-
-        @ParameterizedTest
-        @MethodSource("literalsWithDataVariableOutput")
-        void boundTwiceDataParameterTest(Literal literal) {
-                var builder = Dnf.builder().parameter(x, ParameterDirection.IN).clause(literal);
-                assertThrows(IllegalArgumentException.class, builder::build);
-        }
-
-        @ParameterizedTest
-        @MethodSource("literalsWithDataVariableOutput")
-        void boundPrivateDataVariableOutputTest(Literal literal) {
-                var dnfWithInput = Dnf.builder("WithInput")
-                                .parameter(x, ParameterDirection.IN)
-                                .clause(assume(greaterEq(x, constant(24))))
-                                .build();
-                var builder = Dnf.builder().clause(dnfWithInput.call(x), literal);
-                var dnf = assertDoesNotThrow(builder::build);
-                assertThat(dnf.getClauses().get(0).positiveVariables(), hasItem(x));
-        }
-
-        @ParameterizedTest
-        @MethodSource("literalsWithDataVariableOutput")
-        void boundTwicePrivateDataVariableOutputTest(Literal literal) {
-                var builder = Dnf.builder().clause(x.assign(constant(27)), literal);
-                assertThrows(IllegalArgumentException.class, builder::build);
-        }
-
-        static Stream<Arguments> literalsWithDataVariableOutput() {
-                var dnfWithOutput = Dnf.builder("WithOutput")
-                                .parameter(q, ParameterDirection.OUT)
-                                .clause(personView.call(q))
-                                .build();
-                var dnfWithDataOutput = Dnf.builder("WithDataOutput")
-                                .parameter(y, ParameterDirection.OUT)
-                                .parameter(q, ParameterDirection.OUT)
-                                .clause(ageView.call(q, y))
-                                .build();
-                var dnfWithOutputToAggregate = Dnf.builder("WithDataOutputToAggregate")
-                                .parameter(q, ParameterDirection.OUT)
-                                .parameter(y, ParameterDirection.OUT)
-                                .clause(ageView.call(q, y))
-                                .build();
-
-                return Stream.of(
-                                Arguments.of(x.assign(constant(24))),
-                                Arguments.of(ageView.call(q, x)),
-                                Arguments.of(x.assign(personView.count(q))),
-                                Arguments.of(x.assign(ageView.aggregate(INT_SUM, q))),
-                                Arguments.of(dnfWithDataOutput.call(x, q)),
-                                Arguments.of(x.assign(dnfWithOutput.count(q))),
-                                Arguments.of(x.assign(dnfWithOutputToAggregate.aggregateBy(z, INT_SUM, q, z)))
-                );
-        }
-
         private static Stream<Arguments> literalToClauseArgumentStream(Stream<Arguments> literalArgumentsStream) {
                 return literalArgumentsStream.map(arguments -> Arguments.of(List.of(arguments.get()[0])));
         }