refactor: query equality and hash code

Allow computing hash codes up to the renaming of variables.

Also introduces CheckLiteral instead of AssumeLiteral for more straightforward
naming.

4 files changed, 76 insertions, 9 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..9d9bf3c0 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();
 
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/VariableDirectionTest.java b/subprojects/store-query/src/test/java/tools/refinery/store/query/dnf/VariableDirectionTest.java
index c52d26b2..c509da4d 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,7 +28,7 @@ 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.check;
 import static tools.refinery.store.query.literal.Literals.not;
 import static tools.refinery.store.query.term.int_.IntTerms.*;
 
@@ -349,7 +349,7 @@ class VariableDirectionTest {
                                 .clause(
                                                 friendView.call(p, q),
                                                 ageView.call(q, x),
-                                                assume(greaterEq(x, y))
+                                                check(greaterEq(x, y))
                                 )
                                 .build();
 
@@ -381,7 +381,7 @@ class VariableDirectionTest {
         void boundPrivateDataVariableOutputTest(Literal literal) {
                 var dnfWithInput = Dnf.builder("WithInput")
                                 .parameter(x, ParameterDirection.IN)
-                                .clause(assume(greaterEq(x, constant(24))))
+                                .clause(check(greaterEq(x, constant(24))))
                                 .build();
                 var builder = Dnf.builder().clause(dnfWithInput.call(x), literal);
                 var dnf = assertDoesNotThrow(builder::build);
diff --git a/subprojects/store-query/src/test/java/tools/refinery/store/query/term/TermSubstitutionTest.java b/subprojects/store-query/src/test/java/tools/refinery/store/query/term/TermSubstitutionTest.java
index 1cbc101a..1fae2492 100644
--- a/subprojects/store-query/src/test/java/tools/refinery/store/query/term/TermSubstitutionTest.java
+++ b/subprojects/store-query/src/test/java/tools/refinery/store/query/term/TermSubstitutionTest.java
@@ -9,8 +9,8 @@ import org.junit.jupiter.api.Assertions;
 import org.junit.jupiter.params.ParameterizedTest;
 import org.junit.jupiter.params.provider.Arguments;
 import org.junit.jupiter.params.provider.MethodSource;
-import tools.refinery.store.query.dnf.Dnf;
-import tools.refinery.store.query.equality.LiteralEqualityHelper;
+import tools.refinery.store.query.equality.DnfEqualityChecker;
+import tools.refinery.store.query.equality.SubstitutingLiteralEqualityHelper;
 import tools.refinery.store.query.substitution.Substitution;
 import tools.refinery.store.query.term.bool.BoolTerms;
 import tools.refinery.store.query.term.int_.IntTerms;
@@ -48,7 +48,7 @@ class TermSubstitutionTest {
         void substitutionTest(AnyTerm term) {
                 var substitutedTerm1 = term.substitute(substitution);
                 Assertions.assertNotEquals(term, substitutedTerm1, "Original term is not equal to substituted term");
-                var helper = new LiteralEqualityHelper(Dnf::equals, List.of(), List.of());
+                var helper = new SubstitutingLiteralEqualityHelper(DnfEqualityChecker.DEFAULT, List.of(), List.of());
                 Assertions.assertTrue(term.equalsWithSubstitution(helper, substitutedTerm1), "Terms are equal by helper");
                 // The {@link #substitution} is its own inverse.
                 var substitutedTerm2 = substitutedTerm1.substitute(substitution);