From 9666818c58bb4c30ef6b0c88cc680bc559b123c6 Mon Sep 17 00:00:00 2001 From: Kristóf Marussy Date: Mon, 10 Jul 2023 18:38:11 +0200 Subject: feat: DNF rewriting * DuplicateDnfRewriter replaces DNF with their canonical representatives * ClauseInputParameterResolver removes input parameters by demand set transformation * CompositeRewriter for rewriter stacks --- .../query/rewriter/DuplicateDnfRemoverTest.java | 164 ++++++++++++++++ .../query/rewriter/InputParameterResolverTest.java | 208 +++++++++++++++++++++ 2 files changed, 372 insertions(+) create mode 100644 subprojects/store-query/src/test/java/tools/refinery/store/query/rewriter/DuplicateDnfRemoverTest.java create mode 100644 subprojects/store-query/src/test/java/tools/refinery/store/query/rewriter/InputParameterResolverTest.java (limited to 'subprojects/store-query/src/test/java') diff --git a/subprojects/store-query/src/test/java/tools/refinery/store/query/rewriter/DuplicateDnfRemoverTest.java b/subprojects/store-query/src/test/java/tools/refinery/store/query/rewriter/DuplicateDnfRemoverTest.java new file mode 100644 index 00000000..ebb24ab5 --- /dev/null +++ b/subprojects/store-query/src/test/java/tools/refinery/store/query/rewriter/DuplicateDnfRemoverTest.java @@ -0,0 +1,164 @@ +/* + * SPDX-FileCopyrightText: 2023 The Refinery Authors + * + * SPDX-License-Identifier: EPL-2.0 + */ +package tools.refinery.store.query.rewriter; + +import org.junit.jupiter.api.BeforeEach; +import org.junit.jupiter.api.Test; +import tools.refinery.store.query.dnf.Query; +import tools.refinery.store.query.literal.AbstractCallLiteral; +import tools.refinery.store.query.literal.Reduction; +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 java.util.List; + +import static org.hamcrest.MatcherAssert.assertThat; +import static org.hamcrest.Matchers.is; +import static org.hamcrest.Matchers.not; +import static tools.refinery.store.query.literal.Literals.not; + +class DuplicateDnfRemoverTest { + private final static Symbol friend = Symbol.of("friend", 2); + private final static AnySymbolView friendView = new KeyOnlyView<>(friend); + + private DuplicateDnfRemover sut; + + @BeforeEach + void beforeEach() { + sut = new DuplicateDnfRemover(); + } + + @Test + void removeDuplicateSimpleTest() { + var one = Query.of("One", (builder, x, y) -> builder.clause( + friendView.call(x, y), + friendView.call(y, x) + )); + var two = Query.of("Two", (builder, x, y) -> builder.clause( + friendView.call(x, y), + friendView.call(y, x) + )); + + var oneResult = sut.rewrite(one); + var twoResult = sut.rewrite(two); + + assertThat(oneResult, is(twoResult)); + assertThat(one, is(oneResult)); + } + + @Test + void notDuplicateSimpleTest() { + var one = Query.of("One", (builder, x, y) -> builder.clause( + friendView.call(x, y), + friendView.call(y, x) + )); + var two = Query.of("Two", (builder, x, y) -> builder.clause((z) -> List.of( + friendView.call(x, y), + friendView.call(y, z) + ))); + + var oneResult = sut.rewrite(one); + var twoResult = sut.rewrite(two); + + assertThat(one, is(oneResult)); + assertThat(two, is(twoResult)); + } + + @Test + void removeDuplicateRecursiveTest() { + var oneSubQuery = Query.of("OneSubQuery", (builder, x, y) -> builder.clause( + friendView.call(x, y), + friendView.call(y, x) + )); + var one = Query.of("One", (builder, x) -> builder.clause( + oneSubQuery.call(x, Variable.of()) + )); + var twoSubQuery = Query.of("TwoSubQuery", (builder, x, y) -> builder.clause( + friendView.call(x, y), + friendView.call(y, x) + )); + var two = Query.of("Two", (builder, x) -> builder.clause( + twoSubQuery.call(x, Variable.of()) + )); + + var oneResult = sut.rewrite(one); + var twoResult = sut.rewrite(two); + + assertThat(oneResult, is(twoResult)); + assertThat(one, is(oneResult)); + } + + @Test + void notDuplicateRecursiveTest() { + var oneSubQuery = Query.of("OneSubQuery", (builder, x, y) -> builder.clause( + friendView.call(x, y), + friendView.call(y, x) + )); + var one = Query.of("One", (builder, x) -> builder.clause( + oneSubQuery.call(x, Variable.of()) + )); + var twoSubQuery = Query.of("TwoSubQuery", (builder, x, y) -> builder.clause( + friendView.call(x, y), + friendView.call(y, x) + )); + var two = Query.of("Two", (builder, x) -> builder.clause( + twoSubQuery.call(Variable.of(), x) + )); + + var oneResult = sut.rewrite(one); + var twoResult = sut.rewrite(two); + + assertThat(one, is(oneResult)); + assertThat(oneResult, is(not(twoResult))); + + var oneCall = (AbstractCallLiteral) oneResult.getDnf().getClauses().get(0).literals().get(0); + var twoCall = (AbstractCallLiteral) twoResult.getDnf().getClauses().get(0).literals().get(0); + + assertThat(oneCall.getTarget(), is(twoCall.getTarget())); + } + + @Test + void removeContradictionTest() { + var oneSubQuery = Query.of("OneSubQuery", (builder, x, y) -> builder.clause( + friendView.call(x, y), + friendView.call(y, x) + )); + var twoSubQuery = Query.of("TwoSubQuery", (builder, x, y) -> builder.clause( + friendView.call(x, y), + friendView.call(y, x) + )); + var query = Query.of("Contradiction", (builder, x, y) -> builder.clause( + oneSubQuery.call(x, y), + not(twoSubQuery.call(x, y)) + )); + + var result = sut.rewrite(query); + + assertThat(result.getDnf().getReduction(), is(Reduction.ALWAYS_FALSE)); + } + + @Test + void removeQuantifiedContradictionTest() { + var oneSubQuery = Query.of("OneSubQuery", (builder, x, y) -> builder.clause( + friendView.call(x, y), + friendView.call(y, x) + )); + var twoSubQuery = Query.of("TwoSubQuery", (builder, x, y) -> builder.clause( + friendView.call(x, y), + friendView.call(y, x) + )); + var query = Query.of("Contradiction", (builder, x) -> builder.clause( + oneSubQuery.call(x, Variable.of()), + not(twoSubQuery.call(x, Variable.of())) + )); + + var result = sut.rewrite(query); + + assertThat(result.getDnf().getReduction(), is(Reduction.ALWAYS_FALSE)); + } +} diff --git a/subprojects/store-query/src/test/java/tools/refinery/store/query/rewriter/InputParameterResolverTest.java b/subprojects/store-query/src/test/java/tools/refinery/store/query/rewriter/InputParameterResolverTest.java new file mode 100644 index 00000000..ddb2a069 --- /dev/null +++ b/subprojects/store-query/src/test/java/tools/refinery/store/query/rewriter/InputParameterResolverTest.java @@ -0,0 +1,208 @@ +/* + * SPDX-FileCopyrightText: 2023 The Refinery Authors + * + * SPDX-License-Identifier: EPL-2.0 + */ +package tools.refinery.store.query.rewriter; + +import org.junit.jupiter.api.BeforeEach; +import org.junit.jupiter.api.Test; +import tools.refinery.store.query.dnf.Dnf; +import tools.refinery.store.query.dnf.Query; +import tools.refinery.store.query.term.ParameterDirection; +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 java.util.List; + +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 InputParameterResolverTest { + private final static Symbol person = Symbol.of("Person", 1); + private final static Symbol friend = Symbol.of("friend", 2); + private final static AnySymbolView personView = new KeyOnlyView<>(person); + private final static AnySymbolView friendView = new KeyOnlyView<>(friend); + + private InputParameterResolver sut; + + @BeforeEach + void beforeEach() { + sut = new InputParameterResolver(); + } + + @Test + void inlineSingleClauseTest() { + var dnf = Dnf.of("SubQuery", builder -> { + var x = builder.parameter("x", ParameterDirection.OUT); + builder.clause(friendView.call(x, Variable.of())); + }); + var query = Query.of("Actual", (builder, x) -> builder.clause( + dnf.call(x), + personView.call(x) + )); + + var actual = sut.rewrite(query); + + var expected = Query.of("Expected", (builder, x) -> builder.clause( + friendView.call(x, Variable.of()), + personView.call(x) + )); + + assertThat(actual.getDnf(), structurallyEqualTo(expected.getDnf())); + } + + @Test + void inlineSingleClauseWIthInputTest() { + var dnf = Dnf.of("SubQuery", builder -> { + var x = builder.parameter("x", ParameterDirection.IN); + builder.clause(not(friendView.call(x, Variable.of()))); + }); + var query = Query.of("Actual", (builder, x) -> builder.clause( + dnf.call(x), + personView.call(x) + )); + + var actual = sut.rewrite(query); + + var expected = Query.of("Expected", (builder, x) -> builder.clause( + personView.call(x), + not(friendView.call(x, Variable.of())) + )); + + assertThat(actual.getDnf(), structurallyEqualTo(expected.getDnf())); + } + + @Test + void singleLiteralDemandSetTest() { + var dnf = Dnf.of("SubQuery", builder -> { + var x = builder.parameter("x", ParameterDirection.IN); + builder.clause(not(friendView.call(x, Variable.of()))); + builder.clause(not(friendView.call(Variable.of(), x))); + }); + var query = Query.of("Actual", (builder, x) -> builder.clause( + dnf.call(x), + personView.call(x) + )); + + var actual = sut.rewrite(query); + + var expectedSubQuery = Dnf.of("ExpectedSubQuery", builder -> { + var x = builder.parameter("x", ParameterDirection.OUT); + builder.clause( + personView.call(x), + not(friendView.call(x, Variable.of())) + ); + builder.clause( + personView.call(x), + not(friendView.call(Variable.of(), x)) + ); + }); + var expected = Query.of("Expected", (builder, x) -> builder.clause( + personView.call(x), + expectedSubQuery.call(x) + )); + + assertThat(actual.getDnf(), structurallyEqualTo(expected.getDnf())); + } + + @Test + void multipleLiteralDemandSetTest() { + var dnf = Dnf.of("SubQuery", builder -> { + var x = builder.parameter("x", ParameterDirection.IN); + var y = builder.parameter("y", ParameterDirection.IN); + builder.clause(not(friendView.call(x, y))); + builder.clause(not(friendView.call(y, x))); + }); + var query = Query.of("Actual", (builder, p1) -> builder.clause(p2 -> List.of( + not(dnf.call(p1, p2)), + personView.call(p1), + personView.call(p2) + ))); + + var actual = sut.rewrite(query); + + var context = Dnf.of("Context", builder -> { + var x = builder.parameter("x", ParameterDirection.OUT); + var y = builder.parameter("y", ParameterDirection.OUT); + builder.clause( + personView.call(x), + personView.call(y) + ); + }); + var expectedSubQuery = Dnf.of("ExpectedSubQuery", builder -> { + var x = builder.parameter("x", ParameterDirection.OUT); + var y = builder.parameter("x", ParameterDirection.OUT); + builder.clause( + context.call(x, y), + not(friendView.call(x, y)) + ); + builder.clause( + context.call(x, y), + not(friendView.call(y, x)) + ); + }); + var expected = Query.of("Expected", (builder, p1) -> builder.clause(p2 -> List.of( + context.call(p1, p2), + not(expectedSubQuery.call(p1, p2)) + ))); + + assertThat(actual.getDnf(), structurallyEqualTo(expected.getDnf())); + } + + @Test + void multipleParameterDemandSetTest() { + var dnf = Dnf.of("SubQuery", builder -> { + var x = builder.parameter("x", ParameterDirection.IN); + var y = builder.parameter("y", ParameterDirection.IN); + builder.clause(not(friendView.call(x, y))); + builder.clause(not(friendView.call(y, x))); + }); + var query = Query.of("Actual", (builder, p1) -> builder.clause( + not(dnf.call(p1, p1)), + personView.call(p1) + )); + + var actual = sut.rewrite(query); + + var expectedSubQuery = Dnf.of("ExpectedSubQuery", builder -> { + var x = builder.parameter("x", ParameterDirection.OUT); + var y = builder.parameter("y", ParameterDirection.OUT); + builder.clause( + y.isEquivalent(x), + personView.call(x), + not(friendView.call(x, x)) + ); + }); + var expected = Query.of("Expected", (builder, p1) -> builder.clause( + personView.call(p1), + not(expectedSubQuery.call(p1, p1)) + )); + + assertThat(actual.getDnf(), structurallyEqualTo(expected.getDnf())); + } + + @Test + void eliminateDoubleNegationTest() { + var dnf = Dnf.of("SubQuery", builder -> { + var x = builder.parameter("x", ParameterDirection.IN); + builder.clause(not(friendView.call(x, Variable.of()))); + }); + var query = Query.of("Actual", (builder, p1) -> builder.clause( + personView.call(p1), + not(dnf.call(p1)) + )); + + var actual = sut.rewrite(query); + + var expected = Query.of("Actual", (builder, p1) -> builder.clause( + personView.call(p1), + friendView.call(p1, Variable.of()) + )); + + assertThat(actual.getDnf(), structurallyEqualTo(expected.getDnf())); + } +} -- cgit v1.2.3-54-g00ecf