feat: Dnf reduction and structural equality

3 files changed, 467 insertions, 0 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/DnfBuilderTest.java
new file mode 100644
index 00000000..e6701fe3
--- /dev/null
+++ b/subprojects/store-query/src/test/java/tools/refinery/store/query/DnfBuilderTest.java
@@ -0,0 +1,218 @@
+package tools.refinery.store.query;
+
+import org.junit.jupiter.api.Test;
+import tools.refinery.store.query.literal.BooleanLiteral;
+import tools.refinery.store.query.view.KeyOnlyRelationView;
+import tools.refinery.store.representation.Symbol;
+
+import static org.hamcrest.MatcherAssert.assertThat;
+import static tools.refinery.store.query.literal.Literals.not;
+import static tools.refinery.store.query.tests.QueryMatchers.structurallyEqualTo;
+
+class DnfBuilderTest {
+        @Test
+        void eliminateTrueTest() {
+                var p = new Variable("p");
+                var q = new Variable("q");
+                var friend = new Symbol<>("friend", 2, Boolean.class, false);
+                var friendView = new KeyOnlyRelationView<>(friend);
+
+                var actual = Dnf.builder()
+                                .parameters(p, q)
+                                .clause(BooleanLiteral.TRUE, friendView.call(p, q))
+                                .build();
+                var expected = Dnf.builder().parameters(p, q).clause(friendView.call(p, q)).build();
+
+                assertThat(actual, structurallyEqualTo(expected));
+        }
+
+        @Test
+        void eliminateFalseTest() {
+                var p = new Variable("p");
+                var q = new Variable("q");
+                var friend = new Symbol<>("friend", 2, Boolean.class, false);
+                var friendView = new KeyOnlyRelationView<>(friend);
+
+                var actual = Dnf.builder()
+                                .parameters(p, q)
+                                .clause(friendView.call(p, q))
+                                .clause(friendView.call(q, p), BooleanLiteral.FALSE)
+                                .build();
+                var expected = Dnf.builder().parameters(p, q).clause(friendView.call(p, q)).build();
+
+                assertThat(actual, structurallyEqualTo(expected));
+        }
+
+        @Test
+        void alwaysTrueTest() {
+                var p = new Variable("p");
+                var q = new Variable("q");
+                var friend = new Symbol<>("friend", 2, Boolean.class, false);
+                var friendView = new KeyOnlyRelationView<>(friend);
+
+                var actual = Dnf.builder()
+                                .parameters(p, q)
+                                .clause(friendView.call(p, q))
+                                .clause(BooleanLiteral.TRUE)
+                                .build();
+                var expected = Dnf.builder().parameters(p, q).clause().build();
+
+                assertThat(actual, structurallyEqualTo(expected));
+        }
+
+        @Test
+        void alwaysFalseTest() {
+                var p = new Variable("p");
+                var q = new Variable("q");
+                var friend = new Symbol<>("friend", 2, Boolean.class, false);
+                var friendView = new KeyOnlyRelationView<>(friend);
+
+                var actual = Dnf.builder()
+                                .parameters(p, q)
+                                .clause(friendView.call(p, q), BooleanLiteral.FALSE)
+                                .build();
+                var expected = Dnf.builder().parameters(p, q).build();
+
+                assertThat(actual, structurallyEqualTo(expected));
+        }
+
+        @Test
+        void eliminateTrueDnfTest() {
+                var p = new Variable("p");
+                var q = new Variable("q");
+                var friend = new Symbol<>("friend", 2, Boolean.class, false);
+                var friendView = new KeyOnlyRelationView<>(friend);
+                var trueDnf = Dnf.builder().parameter(p).clause().build();
+
+                var actual = Dnf.builder()
+                                .parameters(p, q)
+                                .clause(trueDnf.call(q), friendView.call(p, q))
+                                .build();
+                var expected = Dnf.builder().parameters(p, q).clause(friendView.call(p, q)).build();
+
+                assertThat(actual, structurallyEqualTo(expected));
+        }
+
+        @Test
+        void eliminateFalseDnfTest() {
+                var p = new Variable("p");
+                var q = new Variable("q");
+                var friend = new Symbol<>("friend", 2, Boolean.class, false);
+                var friendView = new KeyOnlyRelationView<>(friend);
+                var falseDnf = Dnf.builder().parameter(p).build();
+
+                var actual = Dnf.builder()
+                                .parameters(p, q)
+                                .clause(friendView.call(p, q))
+                                .clause(friendView.call(q, p), falseDnf.call(q))
+                                .build();
+                var expected = Dnf.builder().parameters(p, q).clause(friendView.call(p, q)).build();
+
+                assertThat(actual, structurallyEqualTo(expected));
+        }
+
+        @Test
+        void alwaysTrueDnfTest() {
+                var p = new Variable("p");
+                var q = new Variable("q");
+                var friend = new Symbol<>("friend", 2, Boolean.class, false);
+                var friendView = new KeyOnlyRelationView<>(friend);
+                var trueDnf = Dnf.builder().parameter(p).clause().build();
+
+                var actual = Dnf.builder()
+                                .parameters(p, q)
+                                .clause(friendView.call(p, q))
+                                .clause(trueDnf.call(q))
+                                .build();
+                var expected = Dnf.builder().parameters(p, q).clause().build();
+
+                assertThat(actual, structurallyEqualTo(expected));
+        }
+
+        @Test
+        void alwaysFalseDnfTest() {
+                var p = new Variable("p");
+                var q = new Variable("q");
+                var friend = new Symbol<>("friend", 2, Boolean.class, false);
+                var friendView = new KeyOnlyRelationView<>(friend);
+                var falseDnf = Dnf.builder().parameter(p).build();
+
+                var actual = Dnf.builder()
+                                .parameters(p, q)
+                                .clause(friendView.call(p, q), falseDnf.call(q))
+                                .build();
+                var expected = Dnf.builder().parameters(p, q).build();
+
+                assertThat(actual, structurallyEqualTo(expected));
+        }
+
+        @Test
+        void eliminateNotFalseDnfTest() {
+                var p = new Variable("p");
+                var q = new Variable("q");
+                var friend = new Symbol<>("friend", 2, Boolean.class, false);
+                var friendView = new KeyOnlyRelationView<>(friend);
+                var falseDnf = Dnf.builder().parameter(p).build();
+
+                var actual = Dnf.builder()
+                                .parameters(p, q)
+                                .clause(not(falseDnf.call(q)), friendView.call(p, q))
+                                .build();
+                var expected = Dnf.builder().parameters(p, q).clause(friendView.call(p, q)).build();
+
+                assertThat(actual, structurallyEqualTo(expected));
+        }
+
+        @Test
+        void eliminateNotTrueDnfTest() {
+                var p = new Variable("p");
+                var q = new Variable("q");
+                var friend = new Symbol<>("friend", 2, Boolean.class, false);
+                var friendView = new KeyOnlyRelationView<>(friend);
+                var trueDnf = Dnf.builder().parameter(p).clause().build();
+
+                var actual = Dnf.builder()
+                                .parameters(p, q)
+                                .clause(friendView.call(p, q))
+                                .clause(friendView.call(q, p), not(trueDnf.call(q)))
+                                .build();
+                var expected = Dnf.builder().parameters(p, q).clause(friendView.call(p, q)).build();
+
+                assertThat(actual, structurallyEqualTo(expected));
+        }
+
+        @Test
+        void alwaysNotFalseDnfTest() {
+                var p = new Variable("p");
+                var q = new Variable("q");
+                var friend = new Symbol<>("friend", 2, Boolean.class, false);
+                var friendView = new KeyOnlyRelationView<>(friend);
+                var falseDnf = Dnf.builder().parameter(p).build();
+
+                var actual = Dnf.builder()
+                                .parameters(p, q)
+                                .clause(friendView.call(p, q))
+                                .clause(not(falseDnf.call(q)))
+                                .build();
+                var expected = Dnf.builder().parameters(p, q).clause().build();
+
+                assertThat(actual, structurallyEqualTo(expected));
+        }
+
+        @Test
+        void alwaysNotTrueDnfTest() {
+                var p = new Variable("p");
+                var q = new Variable("q");
+                var friend = new Symbol<>("friend", 2, Boolean.class, false);
+                var friendView = new KeyOnlyRelationView<>(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)))
+                                .build();
+                var expected = Dnf.builder().parameters(p, q).build();
+
+                assertThat(actual, structurallyEqualTo(expected));
+        }
+}
diff --git a/subprojects/store-query/src/test/java/tools/refinery/store/query/DnfToStringTest.java b/subprojects/store-query/src/test/java/tools/refinery/store/query/DnfToStringTest.java
new file mode 100644
index 00000000..e6e4bef3
--- /dev/null
+++ b/subprojects/store-query/src/test/java/tools/refinery/store/query/DnfToStringTest.java
@@ -0,0 +1,172 @@
+package tools.refinery.store.query;
+
+import org.junit.jupiter.api.Test;
+import tools.refinery.store.query.view.KeyOnlyRelationView;
+import tools.refinery.store.representation.Symbol;
+
+import static org.hamcrest.MatcherAssert.assertThat;
+import static org.hamcrest.Matchers.is;
+import static tools.refinery.store.query.literal.Literals.not;
+
+class DnfToStringTest {
+        @Test
+        void noClausesTest() {
+                var p = new Variable("p");
+                var dnf = Dnf.builder("Example").parameter(p).build();
+
+                assertThat(dnf.toString(), is("""
+                                pred Example(p) <->
+                                    <no clauses>.
+                                """));
+        }
+
+        @Test
+        void noParametersTest() {
+                var dnf = Dnf.builder("Example").build();
+
+                assertThat(dnf.toString(), is("""
+                                pred Example() <->
+                                    <no clauses>.
+                                """));
+        }
+
+        @Test
+        void emptyClauseTest() {
+                var p = new Variable("p");
+                var dnf = Dnf.builder("Example").parameter(p).clause().build();
+
+                assertThat(dnf.toString(), is("""
+                                pred Example(p) <->
+                                    <empty>.
+                                """));
+        }
+
+        @Test
+        void relationViewPositiveTest() {
+                var p = new Variable("p");
+                var q = new Variable("q");
+                var friend = new Symbol<>("friend", 2, Boolean.class, false);
+                var friendView = new KeyOnlyRelationView<>(friend);
+                var dnf = Dnf.builder("Example").parameter(p).clause(friendView.call(p, q)).build();
+
+                assertThat(dnf.toString(), is("""
+                                pred Example(p) <->
+                                    @RelationView("key") friend(p, q).
+                                """));
+        }
+
+        @Test
+        void relationViewNegativeTest() {
+                var p = new Variable("p");
+                var q = new Variable("q");
+                var friend = new Symbol<>("friend", 2, Boolean.class, false);
+                var friendView = new KeyOnlyRelationView<>(friend);
+                var dnf = Dnf.builder("Example").parameter(p).clause(not(friendView.call(p, q))).build();
+
+                assertThat(dnf.toString(), is("""
+                                pred Example(p) <->
+                                    !(@RelationView("key") friend(p, q)).
+                                """));
+        }
+
+        @Test
+        void relationViewTransitiveTest() {
+                var p = new Variable("p");
+                var q = new Variable("q");
+                var friend = new Symbol<>("friend", 2, Boolean.class, false);
+                var friendView = new KeyOnlyRelationView<>(friend);
+                var dnf = Dnf.builder("Example").parameter(p).clause(friendView.callTransitive(p, q)).build();
+
+                assertThat(dnf.toString(), is("""
+                                pred Example(p) <->
+                                    @RelationView("key") friend+(p, q).
+                                """));
+        }
+
+        @Test
+        void multipleParametersTest() {
+                var p = new Variable("p");
+                var q = new Variable("q");
+                var friend = new Symbol<>("friend", 2, Boolean.class, false);
+                var friendView = new KeyOnlyRelationView<>(friend);
+                var dnf = Dnf.builder("Example").parameters(p, q).clause(friendView.call(p, q)).build();
+
+                assertThat(dnf.toString(), is("""
+                                pred Example(p, q) <->
+                                    @RelationView("key") friend(p, q).
+                                """));
+        }
+
+        @Test
+        void multipleLiteralsTest() {
+                var p = new Variable("p");
+                var q = new Variable("q");
+                var person = new Symbol<>("person", 1, Boolean.class, false);
+                var personView = new KeyOnlyRelationView<>(person);
+                var friend = new Symbol<>("friend", 2, Boolean.class, false);
+                var friendView = new KeyOnlyRelationView<>(friend);
+                var dnf = Dnf.builder("Example")
+                                .parameter(p)
+                                .clause(
+                                                personView.call(p),
+                                                personView.call(q),
+                                                friendView.call(p, q)
+                                )
+                                .build();
+
+                assertThat(dnf.toString(), is("""
+                                pred Example(p) <->
+                                    @RelationView("key") person(p),
+                                    @RelationView("key") person(q),
+                                    @RelationView("key") friend(p, q).
+                                """));
+        }
+
+        @Test
+        void multipleClausesTest() {
+                var p = new Variable("p");
+                var q = new Variable("q");
+                var friend = new Symbol<>("friend", 2, Boolean.class, false);
+                var friendView = new KeyOnlyRelationView<>(friend);
+                var dnf = Dnf.builder("Example")
+                                .parameter(p)
+                                .clause(friendView.call(p, q))
+                                .clause(friendView.call(q, p))
+                                .build();
+
+                assertThat(dnf.toString(), is("""
+                                pred Example(p) <->
+                                    @RelationView("key") friend(p, q)
+                                ;
+                                    @RelationView("key") friend(q, p).
+                                """));
+        }
+
+        @Test
+        void dnfTest() {
+                var p = new Variable("p");
+                var q = new Variable("q");
+                var r = new Variable("r");
+                var s = new Variable("s");
+                var person = new Symbol<>("person", 1, Boolean.class, false);
+                var personView = new KeyOnlyRelationView<>(person);
+                var friend = new Symbol<>("friend", 2, Boolean.class, false);
+                var friendView = new KeyOnlyRelationView<>(friend);
+                var called  = Dnf.builder("Called").parameters(r, s).clause(friendView.call(r, s)).build();
+                var dnf = Dnf.builder("Example")
+                                .parameter(p)
+                                .clause(
+                                                personView.call(p),
+                                                personView.call(q),
+                                                not(called.call(p, q))
+                                )
+                                .build();
+
+                assertThat(dnf.toString(), is("""
+                                pred Example(p) <->
+                                    @RelationView("key") person(p),
+                                    @RelationView("key") person(q),
+                                    !(@Dnf Called(p, q)).
+                                """));
+        }
+}
diff --git a/subprojects/store-query/src/test/java/tools/refinery/store/query/tests/StructurallyEqualToTest.java b/subprojects/store-query/src/test/java/tools/refinery/store/query/tests/StructurallyEqualToTest.java
new file mode 100644
index 00000000..0cda22df
--- /dev/null
+++ b/subprojects/store-query/src/test/java/tools/refinery/store/query/tests/StructurallyEqualToTest.java
@@ -0,0 +1,77 @@
+package tools.refinery.store.query.tests;
+
+import org.junit.jupiter.api.Test;
+import tools.refinery.store.query.Dnf;
+import tools.refinery.store.query.Variable;
+import tools.refinery.store.query.view.KeyOnlyRelationView;
+import tools.refinery.store.representation.Symbol;
+
+import static org.hamcrest.CoreMatchers.containsString;
+import static org.hamcrest.MatcherAssert.assertThat;
+import static org.junit.jupiter.api.Assertions.assertThrows;
+import static tools.refinery.store.query.tests.QueryMatchers.structurallyEqualTo;
+
+class StructurallyEqualToTest {
+        @Test
+        void flatEqualsTest() {
+                var p = new Variable("p");
+                var q = new Variable("q");
+                var person = new Symbol<>("Person", 1, Boolean.class, false);
+                var personView = new KeyOnlyRelationView<>(person);
+
+                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, structurallyEqualTo(expected));
+        }
+
+        @Test
+        void flatNotEqualsTest() {
+                var p = new Variable("p");
+                var q = new Variable("q");
+                var person = new Symbol<>("Person", 1, Boolean.class, false);
+                var personView = new KeyOnlyRelationView<>(person);
+
+                var expected = Dnf.builder("Expected").parameters(q).clause(personView.call(q)).build();
+                var actual = Dnf.builder("Actual").parameters(p).clause(personView.call(q)).build();
+
+                var assertion = structurallyEqualTo(expected);
+                assertThrows(AssertionError.class, () -> assertThat(actual, assertion));
+        }
+
+        @Test
+        void deepEqualsTest() {
+                var p = new Variable("p");
+                var q = new Variable("q");
+                var person = new Symbol<>("Person", 1, Boolean.class, false);
+                var personView = new KeyOnlyRelationView<>(person);
+
+                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, structurallyEqualTo(expected));
+        }
+
+        @Test
+        void deepNotEqualsTest() {
+                var p = new Variable("p");
+                var q = new Variable("q");
+                var person = new Symbol<>("Person", 1, Boolean.class, false);
+                var personView = new KeyOnlyRelationView<>(person);
+
+                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(q)).build().call(q)
+                ).build();
+
+                var assertion = structurallyEqualTo(expected);
+                var error = assertThrows(AssertionError.class, () -> assertThat(actual, assertion));
+                assertThat(error.getMessage(), containsString(" called from Expected "));
+        }
+}