From 4e698774925468062974b990143c1091e23ed63b Mon Sep 17 00:00:00 2001 From: Kristóf Marussy Date: Mon, 1 May 2023 02:07:23 +0200 Subject: 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 --- .../tools/refinery/store/query/DnfBuilderTest.java | 266 -------------------- .../store/query/DnfToDefinitionStringTest.java | 179 -------------- .../dnf/DnfBuilderLiteralEliminationTest.java | 209 ++++++++++++++++ .../dnf/DnfBuilderVariableUnificationTest.java | 273 +++++++++++++++++++++ .../store/query/dnf/DnfToDefinitionStringTest.java | 178 ++++++++++++++ 5 files changed, 660 insertions(+), 445 deletions(-) delete mode 100644 subprojects/store-query/src/test/java/tools/refinery/store/query/DnfBuilderTest.java delete mode 100644 subprojects/store-query/src/test/java/tools/refinery/store/query/DnfToDefinitionStringTest.java create mode 100644 subprojects/store-query/src/test/java/tools/refinery/store/query/dnf/DnfBuilderLiteralEliminationTest.java create mode 100644 subprojects/store-query/src/test/java/tools/refinery/store/query/dnf/DnfBuilderVariableUnificationTest.java create mode 100644 subprojects/store-query/src/test/java/tools/refinery/store/query/dnf/DnfToDefinitionStringTest.java (limited to 'subprojects/store-query/src/test/java') 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 deleted file mode 100644 index 01e2ccf6..00000000 --- a/subprojects/store-query/src/test/java/tools/refinery/store/query/DnfBuilderTest.java +++ /dev/null @@ -1,266 +0,0 @@ -/* - * SPDX-FileCopyrightText: 2021-2023 The Refinery Authors - * - * SPDX-License-Identifier: EPL-2.0 - */ -package tools.refinery.store.query; - -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.Variable; -import tools.refinery.store.query.term.bool.BoolTerms; -import tools.refinery.store.query.view.KeyOnlyView; -import tools.refinery.store.representation.Symbol; - -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 { - @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)) - .build(); - var expected = Dnf.builder().parameters(p, q).clause(friendView.call(p, q)).build(); - - assertThat(actual, structurallyEqualTo(expected)); - } - - @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)) - .build(); - var expected = Dnf.builder().parameters(p, q).clause(friendView.call(p, q)).build(); - - assertThat(actual, structurallyEqualTo(expected)); - } - - @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)) - .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)); - } - - @ParameterizedTest - @CsvSource(value = { - "false", - "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)) - .clause(friendView.call(q, p), assume(BoolTerms.constant(value))) - .build(); - var expected = Dnf.builder().parameters(p, q).clause(friendView.call(p, q)).build(); - - assertThat(actual, structurallyEqualTo(expected)); - } - - @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)) - .clause(BooleanLiteral.TRUE) - .build(); - var expected = Dnf.builder().parameters(p, q).clause().build(); - - assertThat(actual, structurallyEqualTo(expected)); - } - - @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) - .build(); - var expected = Dnf.builder().parameters(p, q).build(); - - assertThat(actual, structurallyEqualTo(expected)); - } - - @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)) - .build(); - var expected = Dnf.builder().parameters(p, q).clause(friendView.call(p, q)).build(); - - assertThat(actual, structurallyEqualTo(expected)); - } - - @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)) - .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 = 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)) - .clause(trueDnf.call(q)) - .build(); - var expected = Dnf.builder().parameters(p, q).clause().build(); - - assertThat(actual, structurallyEqualTo(expected)); - } - - @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)) - .build(); - var expected = Dnf.builder().parameters(p, q).build(); - - assertThat(actual, structurallyEqualTo(expected)); - } - - @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)) - .build(); - var expected = Dnf.builder().parameters(p, q).clause(friendView.call(p, q)).build(); - - assertThat(actual, structurallyEqualTo(expected)); - } - - @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)) - .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 = 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)) - .clause(not(falseDnf.call(q))) - .build(); - var expected = Dnf.builder().parameters(p, q).clause().build(); - - assertThat(actual, structurallyEqualTo(expected)); - } - - @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))) - .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/DnfToDefinitionStringTest.java b/subprojects/store-query/src/test/java/tools/refinery/store/query/DnfToDefinitionStringTest.java deleted file mode 100644 index e89ab682..00000000 --- a/subprojects/store-query/src/test/java/tools/refinery/store/query/DnfToDefinitionStringTest.java +++ /dev/null @@ -1,179 +0,0 @@ -/* - * SPDX-FileCopyrightText: 2021-2023 The Refinery Authors - * - * SPDX-License-Identifier: EPL-2.0 - */ -package tools.refinery.store.query; - -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; - -import static org.hamcrest.MatcherAssert.assertThat; -import static org.hamcrest.Matchers.is; -import static tools.refinery.store.query.literal.Literals.not; - -class DnfToDefinitionStringTest { - @Test - void noClausesTest() { - var p = Variable.of("p"); - var dnf = Dnf.builder("Example").parameter(p).build(); - - assertThat(dnf.toDefinitionString(), is(""" - pred Example(p) <-> - . - """)); - } - - @Test - void noParametersTest() { - var dnf = Dnf.builder("Example").build(); - - assertThat(dnf.toDefinitionString(), is(""" - pred Example() <-> - . - """)); - } - - @Test - void emptyClauseTest() { - var p = Variable.of("p"); - var dnf = Dnf.builder("Example").parameter(p).clause().build(); - - assertThat(dnf.toDefinitionString(), is(""" - pred Example(p) <-> - . - """)); - } - - @Test - void relationViewPositiveTest() { - 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 dnf = Dnf.builder("Example").parameter(p).clause(friendView.call(p, q)).build(); - - assertThat(dnf.toDefinitionString(), is(""" - pred Example(p) <-> - @RelationView("key") friend(p, q). - """)); - } - - @Test - void relationViewNegativeTest() { - 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 dnf = Dnf.builder("Example").parameter(p).clause(not(friendView.call(p, q))).build(); - - assertThat(dnf.toDefinitionString(), is(""" - pred Example(p) <-> - !(@RelationView("key") friend(p, q)). - """)); - } - - @Test - void relationViewTransitiveTest() { - 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 dnf = Dnf.builder("Example").parameter(p).clause(friendView.callTransitive(p, q)).build(); - - assertThat(dnf.toDefinitionString(), is(""" - pred Example(p) <-> - @RelationView("key") friend+(p, q). - """)); - } - - @Test - void multipleParametersTest() { - 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 dnf = Dnf.builder("Example").parameters(p, q).clause(friendView.call(p, q)).build(); - - assertThat(dnf.toDefinitionString(), is(""" - pred Example(p, q) <-> - @RelationView("key") friend(p, q). - """)); - } - - @Test - void multipleLiteralsTest() { - var p = Variable.of("p"); - var q = Variable.of("q"); - var person = new Symbol<>("person", 1, Boolean.class, false); - var personView = new KeyOnlyView<>(person); - var friend = new Symbol<>("friend", 2, Boolean.class, false); - var friendView = new KeyOnlyView<>(friend); - var dnf = Dnf.builder("Example") - .parameter(p) - .clause( - personView.call(p), - personView.call(q), - friendView.call(p, q) - ) - .build(); - - assertThat(dnf.toDefinitionString(), is(""" - pred Example(p) <-> - @RelationView("key") person(p), - @RelationView("key") person(q), - @RelationView("key") friend(p, q). - """)); - } - - @Test - void multipleClausesTest() { - 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 dnf = Dnf.builder("Example") - .parameter(p) - .clause(friendView.call(p, q)) - .clause(friendView.call(q, p)) - .build(); - - assertThat(dnf.toDefinitionString(), is(""" - pred Example(p) <-> - @RelationView("key") friend(p, q) - ; - @RelationView("key") friend(q, p). - """)); - } - - @Test - void dnfTest() { - var p = Variable.of("p"); - var q = Variable.of("q"); - var r = Variable.of("r"); - var s = Variable.of("s"); - var person = new Symbol<>("person", 1, Boolean.class, false); - var personView = new KeyOnlyView<>(person); - var friend = new Symbol<>("friend", 2, Boolean.class, false); - var friendView = new KeyOnlyView<>(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.toDefinitionString(), 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/dnf/DnfBuilderLiteralEliminationTest.java b/subprojects/store-query/src/test/java/tools/refinery/store/query/dnf/DnfBuilderLiteralEliminationTest.java new file mode 100644 index 00000000..4edea401 --- /dev/null +++ b/subprojects/store-query/src/test/java/tools/refinery/store/query/dnf/DnfBuilderLiteralEliminationTest.java @@ -0,0 +1,209 @@ +/* + * SPDX-FileCopyrightText: 2021-2023 The Refinery Authors + * + * SPDX-License-Identifier: EPL-2.0 + */ +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.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 DnfBuilderLiteralEliminationTest { + private final Symbol friend = new Symbol<>("friend", 2, Boolean.class, false); + private final SymbolView 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 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 eliminateTrueAssumptionTest() { + var actual = Dnf.builder() + .parameters(p, q) + .clause(assume(BoolTerms.constant(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 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)); + } + + @ParameterizedTest + @CsvSource(value = { + "false", + "null" + }, nullValues = "null") + void eliminateFalseAssumptionTest(Boolean value) { + var actual = Dnf.builder() + .parameters(p, q) + .clause(friendView.call(p, q)) + .clause(friendView.call(q, p), assume(BoolTerms.constant(value))) + .build(); + var expected = Dnf.builder().parameters(p, q).clause(friendView.call(p, q)).build(); + + assertThat(actual, structurallyEqualTo(expected)); + } + + @Test + void alwaysTrueTest() { + 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 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 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 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 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 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 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 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 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 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)); + } + + @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 + * + * 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 friend = new Symbol<>("friend", 2, Boolean.class, false); + private final Symbol children = new Symbol<>("friend", 2, Boolean.class, false); + private final SymbolView friendView = new KeyOnlyView<>(friend); + private final SymbolView 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/dnf/DnfToDefinitionStringTest.java b/subprojects/store-query/src/test/java/tools/refinery/store/query/dnf/DnfToDefinitionStringTest.java new file mode 100644 index 00000000..2e93d78a --- /dev/null +++ b/subprojects/store-query/src/test/java/tools/refinery/store/query/dnf/DnfToDefinitionStringTest.java @@ -0,0 +1,178 @@ +/* + * SPDX-FileCopyrightText: 2021-2023 The Refinery Authors + * + * SPDX-License-Identifier: EPL-2.0 + */ +package tools.refinery.store.query.dnf; + +import org.junit.jupiter.api.Test; +import tools.refinery.store.query.term.Variable; +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 tools.refinery.store.query.literal.Literals.not; + +class DnfToDefinitionStringTest { + @Test + void noClausesTest() { + var p = Variable.of("p"); + var dnf = Dnf.builder("Example").parameter(p).build(); + + assertThat(dnf.toDefinitionString(), is(""" + pred Example(p) <-> + . + """)); + } + + @Test + void noParametersTest() { + var dnf = Dnf.builder("Example").build(); + + assertThat(dnf.toDefinitionString(), is(""" + pred Example() <-> + . + """)); + } + + @Test + void emptyClauseTest() { + var p = Variable.of("p"); + var dnf = Dnf.builder("Example").parameter(p).clause().build(); + + assertThat(dnf.toDefinitionString(), is(""" + pred Example(@In p) <-> + . + """)); + } + + @Test + void relationViewPositiveTest() { + 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 dnf = Dnf.builder("Example").parameter(p).clause(friendView.call(p, q)).build(); + + assertThat(dnf.toDefinitionString(), is(""" + pred Example(p) <-> + @RelationView("key") friend(p, q). + """)); + } + + @Test + void relationViewNegativeTest() { + 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 dnf = Dnf.builder("Example").parameter(p).clause(not(friendView.call(p, q))).build(); + + assertThat(dnf.toDefinitionString(), is(""" + pred Example(p) <-> + !(@RelationView("key") friend(p, q)). + """)); + } + + @Test + void relationViewTransitiveTest() { + 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 dnf = Dnf.builder("Example").parameter(p).clause(friendView.callTransitive(p, q)).build(); + + assertThat(dnf.toDefinitionString(), is(""" + pred Example(p) <-> + @RelationView("key") friend+(p, q). + """)); + } + + @Test + void multipleParametersTest() { + 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 dnf = Dnf.builder("Example").parameters(p, q).clause(friendView.call(p, q)).build(); + + assertThat(dnf.toDefinitionString(), is(""" + pred Example(p, q) <-> + @RelationView("key") friend(p, q). + """)); + } + + @Test + void multipleLiteralsTest() { + var p = Variable.of("p"); + var q = Variable.of("q"); + var person = new Symbol<>("person", 1, Boolean.class, false); + var personView = new KeyOnlyView<>(person); + var friend = new Symbol<>("friend", 2, Boolean.class, false); + var friendView = new KeyOnlyView<>(friend); + var dnf = Dnf.builder("Example") + .parameter(p) + .clause( + personView.call(p), + personView.call(q), + friendView.call(p, q) + ) + .build(); + + assertThat(dnf.toDefinitionString(), is(""" + pred Example(p) <-> + @RelationView("key") person(p), + @RelationView("key") person(q), + @RelationView("key") friend(p, q). + """)); + } + + @Test + void multipleClausesTest() { + 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 dnf = Dnf.builder("Example") + .parameter(p) + .clause(friendView.call(p, q)) + .clause(friendView.call(q, p)) + .build(); + + assertThat(dnf.toDefinitionString(), is(""" + pred Example(p) <-> + @RelationView("key") friend(p, q) + ; + @RelationView("key") friend(q, p). + """)); + } + + @Test + void dnfTest() { + var p = Variable.of("p"); + var q = Variable.of("q"); + var r = Variable.of("r"); + var s = Variable.of("s"); + var person = new Symbol<>("person", 1, Boolean.class, false); + var personView = new KeyOnlyView<>(person); + var friend = new Symbol<>("friend", 2, Boolean.class, false); + var friendView = new KeyOnlyView<>(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.toDefinitionString(), is(""" + pred Example(p) <-> + @RelationView("key") person(p), + @RelationView("key") person(q), + !(@Dnf Called(p, q)). + """)); + } +} -- cgit v1.2.3-54-g00ecf