From f8a3c575e400259a4985233c07b7a50e5d4d82c5 Mon Sep 17 00:00:00 2001 From: Kristóf Marussy Date: Fri, 24 Feb 2023 20:21:15 +0100 Subject: feat: Dnf reduction and structural equality --- .../store/partial/literal/ModalDnfCallLiteral.java | 15 +- .../store/partial/literal/ModalLiteral.java | 18 ++ .../partial/literal/ModalRelationLiteral.java | 10 +- .../partial/literal/PartialRelationLiteral.java | 9 +- .../TypeAnalyzerExampleHierarchyTest.java | 61 +++--- .../translator/typehierarchy/TypeAnalyzerTest.java | 9 +- .../internal/ViatraModelQueryAdapterImpl.java | 9 +- .../internal/ViatraModelQueryBuilderImpl.java | 29 ++- .../internal/ViatraModelQueryStoreAdapterImpl.java | 19 +- .../refinery/store/query/viatra/QueryTest.java | 40 ++++ subprojects/store-query/build.gradle | 2 + .../main/java/tools/refinery/store/query/Dnf.java | 65 +++++- .../tools/refinery/store/query/DnfBuilder.java | 33 ++-- .../java/tools/refinery/store/query/DnfClause.java | 13 ++ .../java/tools/refinery/store/query/DnfUtils.java | 5 - .../tools/refinery/store/query/EmptyResultSet.java | 49 +++++ .../java/tools/refinery/store/query/Variable.java | 15 +- .../query/equality/DeepDnfEqualityChecker.java | 31 +++ .../store/query/equality/DnfEqualityChecker.java | 8 + .../query/equality/LiteralEqualityHelper.java | 48 +++++ .../store/query/literal/BooleanLiteral.java | 34 +++- .../refinery/store/query/literal/CallLiteral.java | 75 ++++++- .../store/query/literal/ConstantLiteral.java | 22 ++- .../store/query/literal/DnfCallLiteral.java | 15 +- .../store/query/literal/EquivalenceLiteral.java | 24 ++- .../refinery/store/query/literal/Literal.java | 8 +- .../store/query/literal/RelationViewLiteral.java | 15 +- .../query/substitution/MapBasedSubstitution.java | 13 ++ .../query/substitution/RenewingSubstitution.java | 19 ++ .../query/substitution/StatelessSubstitution.java | 18 ++ .../store/query/substitution/Substitution.java | 8 + .../store/query/substitution/Substitutions.java | 27 +++ .../refinery/store/query/view/AnyRelationView.java | 2 + .../refinery/store/query/view/RelationView.java | 17 +- .../tools/refinery/store/query/DnfBuilderTest.java | 218 +++++++++++++++++++++ .../refinery/store/query/DnfToStringTest.java | 172 ++++++++++++++++ .../store/query/tests/StructurallyEqualToTest.java | 77 ++++++++ .../MismatchDescribingDnfEqualityChecker.java | 43 ++++ .../refinery/store/query/tests/QueryMatchers.java | 14 ++ .../store/query/tests/StructurallyEqualTo.java | 36 ++++ .../refinery/store/util/CycleDetectingMapper.java | 9 +- 41 files changed, 1236 insertions(+), 118 deletions(-) create mode 100644 subprojects/store-query/src/main/java/tools/refinery/store/query/EmptyResultSet.java create mode 100644 subprojects/store-query/src/main/java/tools/refinery/store/query/equality/DeepDnfEqualityChecker.java create mode 100644 subprojects/store-query/src/main/java/tools/refinery/store/query/equality/DnfEqualityChecker.java create mode 100644 subprojects/store-query/src/main/java/tools/refinery/store/query/equality/LiteralEqualityHelper.java create mode 100644 subprojects/store-query/src/main/java/tools/refinery/store/query/substitution/MapBasedSubstitution.java create mode 100644 subprojects/store-query/src/main/java/tools/refinery/store/query/substitution/RenewingSubstitution.java create mode 100644 subprojects/store-query/src/main/java/tools/refinery/store/query/substitution/StatelessSubstitution.java create mode 100644 subprojects/store-query/src/main/java/tools/refinery/store/query/substitution/Substitution.java create mode 100644 subprojects/store-query/src/main/java/tools/refinery/store/query/substitution/Substitutions.java create mode 100644 subprojects/store-query/src/test/java/tools/refinery/store/query/DnfBuilderTest.java create mode 100644 subprojects/store-query/src/test/java/tools/refinery/store/query/DnfToStringTest.java create mode 100644 subprojects/store-query/src/test/java/tools/refinery/store/query/tests/StructurallyEqualToTest.java create mode 100644 subprojects/store-query/src/testFixtures/java/tools/refinery/store/query/tests/MismatchDescribingDnfEqualityChecker.java create mode 100644 subprojects/store-query/src/testFixtures/java/tools/refinery/store/query/tests/QueryMatchers.java create mode 100644 subprojects/store-query/src/testFixtures/java/tools/refinery/store/query/tests/StructurallyEqualTo.java diff --git a/subprojects/store-partial/src/main/java/tools/refinery/store/partial/literal/ModalDnfCallLiteral.java b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/literal/ModalDnfCallLiteral.java index a49e0625..8c157187 100644 --- a/subprojects/store-partial/src/main/java/tools/refinery/store/partial/literal/ModalDnfCallLiteral.java +++ b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/literal/ModalDnfCallLiteral.java @@ -2,13 +2,14 @@ package tools.refinery.store.partial.literal; import tools.refinery.store.query.Dnf; import tools.refinery.store.query.Variable; +import tools.refinery.store.query.equality.LiteralEqualityHelper; import tools.refinery.store.query.literal.CallPolarity; import tools.refinery.store.query.literal.DnfCallLiteral; import tools.refinery.store.query.literal.LiteralReduction; import tools.refinery.store.query.literal.PolarLiteral; +import tools.refinery.store.query.substitution.Substitution; import java.util.List; -import java.util.Map; public class ModalDnfCallLiteral extends ModalLiteral implements PolarLiteral { public ModalDnfCallLiteral(CallPolarity polarity, Modality modality, Dnf target, List arguments) { @@ -20,7 +21,17 @@ public class ModalDnfCallLiteral extends ModalLiteral implements PolarLiter } @Override - public ModalDnfCallLiteral substitute(Map substitution) { + public Class getTargetType() { + return Dnf.class; + } + + @Override + protected boolean targetEquals(LiteralEqualityHelper helper, Dnf otherTarget) { + return helper.dnfEqual(getTarget(), otherTarget); + } + + @Override + public ModalDnfCallLiteral substitute(Substitution substitution) { return new ModalDnfCallLiteral(getPolarity(), getModality(), getTarget(), substituteArguments(substitution)); } diff --git a/subprojects/store-partial/src/main/java/tools/refinery/store/partial/literal/ModalLiteral.java b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/literal/ModalLiteral.java index a1b6c83e..cebe9c9d 100644 --- a/subprojects/store-partial/src/main/java/tools/refinery/store/partial/literal/ModalLiteral.java +++ b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/literal/ModalLiteral.java @@ -2,8 +2,10 @@ package tools.refinery.store.partial.literal; import tools.refinery.store.query.RelationLike; import tools.refinery.store.query.Variable; +import tools.refinery.store.query.equality.LiteralEqualityHelper; import tools.refinery.store.query.literal.CallLiteral; import tools.refinery.store.query.literal.CallPolarity; +import tools.refinery.store.query.literal.Literal; import java.util.List; import java.util.Objects; @@ -25,6 +27,22 @@ public abstract class ModalLiteral extends CallLiteral) other; + return modality == otherModalLiteral.modality; + } + + @Override + protected String targetToString() { + return "%s %s".formatted(modality, super.targetToString()); + } + @Override public boolean equals(Object o) { if (this == o) return true; diff --git a/subprojects/store-partial/src/main/java/tools/refinery/store/partial/literal/ModalRelationLiteral.java b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/literal/ModalRelationLiteral.java index dbaa524f..39054f22 100644 --- a/subprojects/store-partial/src/main/java/tools/refinery/store/partial/literal/ModalRelationLiteral.java +++ b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/literal/ModalRelationLiteral.java @@ -4,9 +4,9 @@ import tools.refinery.store.partial.representation.PartialRelation; import tools.refinery.store.query.Variable; import tools.refinery.store.query.literal.CallPolarity; import tools.refinery.store.query.literal.PolarLiteral; +import tools.refinery.store.query.substitution.Substitution; import java.util.List; -import java.util.Map; public final class ModalRelationLiteral extends ModalLiteral implements PolarLiteral { @@ -15,12 +15,18 @@ public final class ModalRelationLiteral extends ModalLiteral super(polarity, modality, target, arguments); } + public ModalRelationLiteral(Modality modality, PartialRelationLiteral baseLiteral) { super(modality, baseLiteral); } @Override - public ModalRelationLiteral substitute(Map substitution) { + public Class getTargetType() { + return PartialRelation.class; + } + + @Override + public ModalRelationLiteral substitute(Substitution substitution) { return new ModalRelationLiteral(getPolarity(), getModality(), getTarget(), substituteArguments(substitution)); } diff --git a/subprojects/store-partial/src/main/java/tools/refinery/store/partial/literal/PartialRelationLiteral.java b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/literal/PartialRelationLiteral.java index dc1a1da3..b81d9a3d 100644 --- a/subprojects/store-partial/src/main/java/tools/refinery/store/partial/literal/PartialRelationLiteral.java +++ b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/literal/PartialRelationLiteral.java @@ -5,9 +5,9 @@ import tools.refinery.store.query.Variable; import tools.refinery.store.query.literal.CallLiteral; import tools.refinery.store.query.literal.CallPolarity; import tools.refinery.store.query.literal.PolarLiteral; +import tools.refinery.store.query.substitution.Substitution; import java.util.List; -import java.util.Map; public final class PartialRelationLiteral extends CallLiteral implements PolarLiteral { @@ -16,7 +16,12 @@ public final class PartialRelationLiteral extends CallLiteral } @Override - public PartialRelationLiteral substitute(Map substitution) { + public Class getTargetType() { + return PartialRelation.class; + } + + @Override + public PartialRelationLiteral substitute(Substitution substitution) { return new PartialRelationLiteral(getPolarity(), getTarget(), substituteArguments(substitution)); } diff --git a/subprojects/store-partial/src/test/java/tools/refinery/store/partial/translator/typehierarchy/TypeAnalyzerExampleHierarchyTest.java b/subprojects/store-partial/src/test/java/tools/refinery/store/partial/translator/typehierarchy/TypeAnalyzerExampleHierarchyTest.java index ad81e28f..5f528328 100644 --- a/subprojects/store-partial/src/test/java/tools/refinery/store/partial/translator/typehierarchy/TypeAnalyzerExampleHierarchyTest.java +++ b/subprojects/store-partial/src/test/java/tools/refinery/store/partial/translator/typehierarchy/TypeAnalyzerExampleHierarchyTest.java @@ -1,6 +1,5 @@ package tools.refinery.store.partial.translator.typehierarchy; -import org.hamcrest.Matchers; import org.junit.jupiter.api.BeforeEach; import org.junit.jupiter.api.Test; import tools.refinery.store.partial.representation.PartialRelation; @@ -61,16 +60,16 @@ class TypeAnalyzerExampleHierarchyTest { @Test void inferredTypesTest() { assertAll( - () -> assertThat(sut.getUnknownType(), Matchers.is(new InferredType(Set.of(), Set.of(c1, c2, c3, c4), null))), - () -> assertThat(tester.getInferredType(a1), Matchers.is(new InferredType(Set.of(a1, a4), Set.of(c1, c2), c1))), - () -> assertThat(tester.getInferredType(a3), Matchers.is(new InferredType(Set.of(a3), Set.of(c2, c3), c2))), - () -> assertThat(tester.getInferredType(a4), Matchers.is(new InferredType(Set.of(a4), Set.of(c1, c2, c4), c1))), - () -> assertThat(tester.getInferredType(a5), Matchers.is(new InferredType(Set.of(a5), Set.of(), null))), - () -> assertThat(tester.getInferredType(c1), Matchers.is(new InferredType(Set.of(a1, a4, c1), Set.of(c1), c1))), + () -> assertThat(sut.getUnknownType(), is(new InferredType(Set.of(), Set.of(c1, c2, c3, c4), null))), + () -> assertThat(tester.getInferredType(a1), is(new InferredType(Set.of(a1, a4), Set.of(c1, c2), c1))), + () -> assertThat(tester.getInferredType(a3), is(new InferredType(Set.of(a3), Set.of(c2, c3), c2))), + () -> assertThat(tester.getInferredType(a4), is(new InferredType(Set.of(a4), Set.of(c1, c2, c4), c1))), + () -> assertThat(tester.getInferredType(a5), is(new InferredType(Set.of(a5), Set.of(), null))), + () -> assertThat(tester.getInferredType(c1), is(new InferredType(Set.of(a1, a4, c1), Set.of(c1), c1))), () -> assertThat(tester.getInferredType(c2), - Matchers.is(new InferredType(Set.of(a1, a3, a4, c2), Set.of(c2), c2))), - () -> assertThat(tester.getInferredType(c3), Matchers.is(new InferredType(Set.of(a3, c3), Set.of(c3), c3))), - () -> assertThat(tester.getInferredType(c4), Matchers.is(new InferredType(Set.of(a4, c4), Set.of(c4), c4))) + is(new InferredType(Set.of(a1, a3, a4, c2), Set.of(c2), c2))), + () -> assertThat(tester.getInferredType(c3), is(new InferredType(Set.of(a3, c3), Set.of(c3), c3))), + () -> assertThat(tester.getInferredType(c4), is(new InferredType(Set.of(a4, c4), Set.of(c4), c4))) ); } @@ -80,8 +79,8 @@ class TypeAnalyzerExampleHierarchyTest { var a3Result = tester.getPreservedType(a3); var expected = new InferredType(Set.of(a1, a3, a4, c2), Set.of(c2), c2); assertAll( - () -> assertThat(a1Result.merge(a3Result.asInferredType(), TruthValue.TRUE), Matchers.is(expected)), - () -> assertThat(a3Result.merge(a1Result.asInferredType(), TruthValue.TRUE), Matchers.is(expected)), + () -> assertThat(a1Result.merge(a3Result.asInferredType(), TruthValue.TRUE), is(expected)), + () -> assertThat(a3Result.merge(a1Result.asInferredType(), TruthValue.TRUE), is(expected)), () -> assertThat(a1Result.merge(sut.getUnknownType(), TruthValue.TRUE), is(a1Result.asInferredType())), () -> assertThat(a3Result.merge(sut.getUnknownType(), TruthValue.TRUE), is(a3Result.asInferredType())), () -> assertThat(a1Result.merge(a1Result.asInferredType(), TruthValue.TRUE), @@ -96,19 +95,19 @@ class TypeAnalyzerExampleHierarchyTest { var a4Result = tester.getPreservedType(a4); assertAll( () -> assertThat(a1Result.merge(a3Result.asInferredType(), TruthValue.FALSE), - Matchers.is(new InferredType(Set.of(a3, c3), Set.of(c3), c3))), + is(new InferredType(Set.of(a3, c3), Set.of(c3), c3))), () -> assertThat(a3Result.merge(a1Result.asInferredType(), TruthValue.FALSE), - Matchers.is(new InferredType(Set.of(a1, a4, c1), Set.of(c1), c1))), + is(new InferredType(Set.of(a1, a4, c1), Set.of(c1), c1))), () -> assertThat(a4Result.merge(a3Result.asInferredType(), TruthValue.FALSE), - Matchers.is(new InferredType(Set.of(a3, c3), Set.of(c3), c3))), + is(new InferredType(Set.of(a3, c3), Set.of(c3), c3))), () -> assertThat(a3Result.merge(a4Result.asInferredType(), TruthValue.FALSE), - Matchers.is(new InferredType(Set.of(a4), Set.of(c1, c4), c1))), + is(new InferredType(Set.of(a4), Set.of(c1, c4), c1))), () -> assertThat(a1Result.merge(sut.getUnknownType(), TruthValue.FALSE), - Matchers.is(new InferredType(Set.of(), Set.of(c3, c4), null))), + is(new InferredType(Set.of(), Set.of(c3, c4), null))), () -> assertThat(a3Result.merge(sut.getUnknownType(), TruthValue.FALSE), - Matchers.is(new InferredType(Set.of(), Set.of(c1, c4), null))), + is(new InferredType(Set.of(), Set.of(c1, c4), null))), () -> assertThat(a4Result.merge(sut.getUnknownType(), TruthValue.FALSE), - Matchers.is(new InferredType(Set.of(), Set.of(c3), null))) + is(new InferredType(Set.of(), Set.of(c3), null))) ); } @@ -118,8 +117,8 @@ class TypeAnalyzerExampleHierarchyTest { var a4Result = tester.getPreservedType(a4); var expected = new InferredType(Set.of(c1, a1, a4), Set.of(), null); assertAll( - () -> assertThat(c1Result.merge(a4Result.asInferredType(), TruthValue.ERROR), Matchers.is(expected)), - () -> assertThat(a4Result.merge(c1Result.asInferredType(), TruthValue.ERROR), Matchers.is(expected)) + () -> assertThat(c1Result.merge(a4Result.asInferredType(), TruthValue.ERROR), is(expected)), + () -> assertThat(a4Result.merge(c1Result.asInferredType(), TruthValue.ERROR), is(expected)) ); } @@ -141,9 +140,9 @@ class TypeAnalyzerExampleHierarchyTest { var c3Result = tester.getPreservedType(c3); assertAll( () -> assertThat(a1Result.merge(c3Result.asInferredType(), TruthValue.TRUE), - Matchers.is(new InferredType(Set.of(a1, a3, c3), Set.of(), null))), + is(new InferredType(Set.of(a1, a3, c3), Set.of(), null))), () -> assertThat(c3Result.merge(a1Result.asInferredType(), TruthValue.TRUE), - Matchers.is(new InferredType(Set.of(a1, a3, a4, c3), Set.of(), null))) + is(new InferredType(Set.of(a1, a3, a4, c3), Set.of(), null))) ); } @@ -154,13 +153,13 @@ class TypeAnalyzerExampleHierarchyTest { var c1Result = tester.getPreservedType(c1); assertAll( () -> assertThat(a4Result.merge(a1Result.asInferredType(), TruthValue.FALSE), - Matchers.is(new InferredType(Set.of(a1, a4), Set.of(), null))), + is(new InferredType(Set.of(a1, a4), Set.of(), null))), () -> assertThat(a1Result.merge(c1Result.asInferredType(), TruthValue.FALSE), - Matchers.is(new InferredType(Set.of(a1, a4, c1), Set.of(), null))), + is(new InferredType(Set.of(a1, a4, c1), Set.of(), null))), () -> assertThat(a4Result.merge(c1Result.asInferredType(), TruthValue.FALSE), - Matchers.is(new InferredType(Set.of(a1, a4, c1), Set.of(), null))), + is(new InferredType(Set.of(a1, a4, c1), Set.of(), null))), () -> assertThat(a1Result.merge(a1Result.asInferredType(), TruthValue.FALSE), - Matchers.is(new InferredType(Set.of(a1, a4), Set.of(), null))) + is(new InferredType(Set.of(a1, a4), Set.of(), null))) ); } @@ -170,9 +169,9 @@ class TypeAnalyzerExampleHierarchyTest { var a5Result = tester.getPreservedType(a5); assertAll( () -> assertThat(c1Result.merge(a5Result.asInferredType(), TruthValue.TRUE), - Matchers.is(new InferredType(Set.of(a1, a4, a5, c1), Set.of(), null))), + is(new InferredType(Set.of(a1, a4, a5, c1), Set.of(), null))), () -> assertThat(a5Result.merge(c1Result.asInferredType(), TruthValue.TRUE), - Matchers.is(new InferredType(Set.of(a1, a4, a5, c1), Set.of(), null))) + is(new InferredType(Set.of(a1, a4, a5, c1), Set.of(), null))) ); } @@ -194,9 +193,9 @@ class TypeAnalyzerExampleHierarchyTest { var a5Result = tester.getPreservedType(a5); assertAll( () -> assertThat(c1Result.merge(a5Result.asInferredType(), TruthValue.ERROR), - Matchers.is(new InferredType(Set.of(a1, a4, a5, c1), Set.of(), null))), + is(new InferredType(Set.of(a1, a4, a5, c1), Set.of(), null))), () -> assertThat(a5Result.merge(c1Result.asInferredType(), TruthValue.ERROR), - Matchers.is(new InferredType(Set.of(a1, a4, a5, c1), Set.of(), null))), + is(new InferredType(Set.of(a1, a4, a5, c1), Set.of(), null))), () -> assertThat(a5Result.merge(a5Result.asInferredType(), TruthValue.ERROR), is(a5Result.asInferredType())) ); diff --git a/subprojects/store-partial/src/test/java/tools/refinery/store/partial/translator/typehierarchy/TypeAnalyzerTest.java b/subprojects/store-partial/src/test/java/tools/refinery/store/partial/translator/typehierarchy/TypeAnalyzerTest.java index 1aab75bb..02903026 100644 --- a/subprojects/store-partial/src/test/java/tools/refinery/store/partial/translator/typehierarchy/TypeAnalyzerTest.java +++ b/subprojects/store-partial/src/test/java/tools/refinery/store/partial/translator/typehierarchy/TypeAnalyzerTest.java @@ -1,6 +1,5 @@ package tools.refinery.store.partial.translator.typehierarchy; -import org.hamcrest.Matchers; import org.junit.jupiter.api.Test; import tools.refinery.store.partial.representation.PartialRelation; import tools.refinery.store.representation.TruthValue; @@ -137,8 +136,8 @@ class TypeAnalyzerTest { var expected = new InferredType(Set.of(c3), Set.of(c1, c2, c3), c3); assertAll( - () -> assertThat(tester.getInferredType(c3), Matchers.is(expected)), - () -> assertThat(c3Result.merge(sut.getUnknownType(), TruthValue.TRUE), Matchers.is(expected)) + () -> assertThat(tester.getInferredType(c3), is(expected)), + () -> assertThat(c3Result.merge(sut.getUnknownType(), TruthValue.TRUE), is(expected)) ); } @@ -162,7 +161,7 @@ class TypeAnalyzerTest { var a1Result = tester.getPreservedType(a1); assertThat(c1Result.merge(a1Result.asInferredType(), TruthValue.FALSE), - Matchers.is(new InferredType(Set.of(a1), Set.of(c2, c3, c4), c2))); + is(new InferredType(Set.of(a1), Set.of(c2, c3, c4), c2))); } @Test @@ -185,7 +184,7 @@ class TypeAnalyzerTest { var a1Result = tester.getPreservedType(a1); assertThat(c1Result.merge(a1Result.asInferredType(), TruthValue.FALSE), - Matchers.is(new InferredType(Set.of(a1), Set.of(c2, c3, c4), c3))); + is(new InferredType(Set.of(a1), Set.of(c2, c3, c4), c3))); } @Test diff --git a/subprojects/store-query-viatra/src/main/java/tools/refinery/store/query/viatra/internal/ViatraModelQueryAdapterImpl.java b/subprojects/store-query-viatra/src/main/java/tools/refinery/store/query/viatra/internal/ViatraModelQueryAdapterImpl.java index e5d8e2f6..e0341598 100644 --- a/subprojects/store-query-viatra/src/main/java/tools/refinery/store/query/viatra/internal/ViatraModelQueryAdapterImpl.java +++ b/subprojects/store-query-viatra/src/main/java/tools/refinery/store/query/viatra/internal/ViatraModelQueryAdapterImpl.java @@ -8,6 +8,7 @@ import org.eclipse.viatra.query.runtime.matchers.backend.IQueryBackend; import org.eclipse.viatra.query.runtime.matchers.backend.IQueryBackendFactory; import tools.refinery.store.model.Model; import tools.refinery.store.query.Dnf; +import tools.refinery.store.query.EmptyResultSet; import tools.refinery.store.query.ResultSet; import tools.refinery.store.query.viatra.ViatraModelQueryAdapter; @@ -15,7 +16,7 @@ import java.lang.invoke.MethodHandle; import java.lang.invoke.MethodHandles; import java.util.Collection; import java.util.Collections; -import java.util.HashMap; +import java.util.LinkedHashMap; import java.util.Map; public class ViatraModelQueryAdapterImpl implements ViatraModelQueryAdapter { @@ -51,11 +52,15 @@ public class ViatraModelQueryAdapterImpl implements ViatraModelQueryAdapter { GenericQueryGroup.of( Collections.>unmodifiableCollection(querySpecifications.values()).stream() ).prepare(queryEngine); - resultSets = new HashMap<>(querySpecifications.size()); + var vacuousQueries = storeAdapter.getVacuousQueries(); + resultSets = new LinkedHashMap<>(querySpecifications.size() + vacuousQueries.size()); for (var entry : querySpecifications.entrySet()) { var matcher = queryEngine.getMatcher(entry.getValue()); resultSets.put(entry.getKey(), matcher); } + for (var vacuousQuery : vacuousQueries) { + resultSets.put(vacuousQuery, new EmptyResultSet()); + } setUpdatePropagationDelayed(true); } diff --git a/subprojects/store-query-viatra/src/main/java/tools/refinery/store/query/viatra/internal/ViatraModelQueryBuilderImpl.java b/subprojects/store-query-viatra/src/main/java/tools/refinery/store/query/viatra/internal/ViatraModelQueryBuilderImpl.java index af20033a..13641ace 100644 --- a/subprojects/store-query-viatra/src/main/java/tools/refinery/store/query/viatra/internal/ViatraModelQueryBuilderImpl.java +++ b/subprojects/store-query-viatra/src/main/java/tools/refinery/store/query/viatra/internal/ViatraModelQueryBuilderImpl.java @@ -14,14 +14,13 @@ import tools.refinery.store.query.viatra.ViatraModelQueryBuilder; import tools.refinery.store.query.viatra.internal.pquery.Dnf2PQuery; import tools.refinery.store.query.viatra.internal.pquery.RawPatternMatcher; -import java.util.Collections; -import java.util.LinkedHashMap; -import java.util.Map; +import java.util.*; import java.util.function.Function; public class ViatraModelQueryBuilderImpl extends AbstractModelAdapterBuilder implements ViatraModelQueryBuilder { private ViatraQueryEngineOptions.Builder engineOptionsBuilder; private final Dnf2PQuery dnf2PQuery = new Dnf2PQuery(); + private final Set vacuousQueries = new LinkedHashSet<>(); private final Map> querySpecifications = new LinkedHashMap<>(); public ViatraModelQueryBuilderImpl(ModelStoreBuilder storeBuilder) { @@ -64,11 +63,21 @@ public class ViatraModelQueryBuilderImpl extends AbstractModelAdapterBuilder imp @Override public ViatraModelQueryBuilder query(Dnf query) { - if (querySpecifications.containsKey(query)) { - throw new IllegalArgumentException("%s was already added to the query engine".formatted(query.name())); + if (querySpecifications.containsKey(query) || vacuousQueries.contains(query)) { + // Ignore duplicate queries. + return this; + } + var reduction = query.getReduction(); + switch (reduction) { + case NOT_REDUCIBLE -> { + var pQuery = dnf2PQuery.translate(query); + querySpecifications.put(query, pQuery.build()); + } + case ALWAYS_FALSE -> vacuousQueries.add(query); + case ALWAYS_TRUE -> throw new IllegalArgumentException( + "Query %s is relationally unsafe (it matches every tuple)".formatted(query.name())); + default -> throw new IllegalArgumentException("Unknown reduction: " + reduction); } - var pQuery = dnf2PQuery.translate(query); - querySpecifications.put(query, pQuery.build()); return this; } @@ -89,6 +98,10 @@ public class ViatraModelQueryBuilderImpl extends AbstractModelAdapterBuilder imp public ViatraModelQueryBuilder hint(Dnf dnf, QueryEvaluationHint queryEvaluationHint) { var pQuery = dnf2PQuery.getAlreadyTranslated(dnf); if (pQuery == null) { + if (vacuousQueries.contains(dnf)) { + // Ignore hits for queries that will never be executed by the query engine. + return this; + } throw new IllegalArgumentException( "Cannot specify hint for %s, because it was not added to the query engine".formatted(dnf.name())); } @@ -100,7 +113,7 @@ public class ViatraModelQueryBuilderImpl extends AbstractModelAdapterBuilder imp public ViatraModelQueryStoreAdapterImpl createStoreAdapter(ModelStore store) { validateSymbols(store); return new ViatraModelQueryStoreAdapterImpl(store, engineOptionsBuilder.build(), dnf2PQuery.getRelationViews(), - Collections.unmodifiableMap(querySpecifications)); + Collections.unmodifiableMap(querySpecifications), Collections.unmodifiableSet(vacuousQueries)); } private void validateSymbols(ModelStore store) { diff --git a/subprojects/store-query-viatra/src/main/java/tools/refinery/store/query/viatra/internal/ViatraModelQueryStoreAdapterImpl.java b/subprojects/store-query-viatra/src/main/java/tools/refinery/store/query/viatra/internal/ViatraModelQueryStoreAdapterImpl.java index 8323118b..00660d0b 100644 --- a/subprojects/store-query-viatra/src/main/java/tools/refinery/store/query/viatra/internal/ViatraModelQueryStoreAdapterImpl.java +++ b/subprojects/store-query-viatra/src/main/java/tools/refinery/store/query/viatra/internal/ViatraModelQueryStoreAdapterImpl.java @@ -10,22 +10,29 @@ import tools.refinery.store.query.viatra.ViatraModelQueryStoreAdapter; import tools.refinery.store.query.viatra.internal.pquery.RawPatternMatcher; import tools.refinery.store.query.view.AnyRelationView; -import java.util.Collection; -import java.util.Map; +import java.util.*; public class ViatraModelQueryStoreAdapterImpl implements ViatraModelQueryStoreAdapter { private final ModelStore store; private final ViatraQueryEngineOptions engineOptions; private final Map inputKeys; private final Map> querySpecifications; + private final Set vacuousQueries; + private final Set allQueries; ViatraModelQueryStoreAdapterImpl(ModelStore store, ViatraQueryEngineOptions engineOptions, Map inputKeys, - Map> querySpecifications) { + Map> querySpecifications, + Set vacuousQueries) { this.store = store; this.engineOptions = engineOptions; this.inputKeys = inputKeys; this.querySpecifications = querySpecifications; + this.vacuousQueries = vacuousQueries; + var mutableAllQueries = new LinkedHashSet(querySpecifications.size() + vacuousQueries.size()); + mutableAllQueries.addAll(querySpecifications.keySet()); + mutableAllQueries.addAll(vacuousQueries); + this.allQueries = Collections.unmodifiableSet(mutableAllQueries); } @Override @@ -43,13 +50,17 @@ public class ViatraModelQueryStoreAdapterImpl implements ViatraModelQueryStoreAd @Override public Collection getQueries() { - return querySpecifications.keySet(); + return allQueries; } Map> getQuerySpecifications() { return querySpecifications; } + Set getVacuousQueries() { + return vacuousQueries; + } + @Override public ViatraQueryEngineOptions getEngineOptions() { return engineOptions; diff --git a/subprojects/store-query-viatra/src/test/java/tools/refinery/store/query/viatra/QueryTest.java b/subprojects/store-query-viatra/src/test/java/tools/refinery/store/query/viatra/QueryTest.java index 6a3a62e3..54ae70c3 100644 --- a/subprojects/store-query-viatra/src/test/java/tools/refinery/store/query/viatra/QueryTest.java +++ b/subprojects/store-query-viatra/src/test/java/tools/refinery/store/query/viatra/QueryTest.java @@ -17,6 +17,7 @@ import java.util.Set; import java.util.stream.Stream; import static org.junit.jupiter.api.Assertions.assertEquals; +import static org.junit.jupiter.api.Assertions.assertThrows; import static tools.refinery.store.query.literal.Literals.not; class QueryTest { @@ -669,6 +670,45 @@ class QueryTest { assertEquals(3, predicateResultSet.countResults()); } + @Test + void alwaysFalseTest() { + var person = new Symbol<>("Person", 1, Boolean.class, false); + + var p1 = new Variable("p1"); + var predicate = Dnf.builder("AlwaysFalse").parameters(p1).build(); + + var store = ModelStore.builder() + .symbols(person) + .with(ViatraModelQuery.ADAPTER) + .queries(predicate) + .build(); + + var model = store.createEmptyModel(); + var personInterpretation = model.getInterpretation(person); + var queryEngine = model.getAdapter(ModelQuery.ADAPTER); + var predicateResultSet = queryEngine.getResultSet(predicate); + + personInterpretation.put(Tuple.of(0), true); + personInterpretation.put(Tuple.of(1), true); + personInterpretation.put(Tuple.of(2), true); + + queryEngine.flushChanges(); + assertEquals(0, predicateResultSet.countResults()); + } + + @Test + void alwaysTrueTest() { + var person = new Symbol<>("Person", 1, Boolean.class, false); + + var p1 = new Variable("p1"); + var predicate = Dnf.builder("AlwaysTrue").parameters(p1).clause().build(); + + var storeBuilder = ModelStore.builder().symbols(person); + var queryBuilder = storeBuilder.with(ViatraModelQuery.ADAPTER); + + assertThrows(IllegalArgumentException.class, () -> queryBuilder.queries(predicate)); + } + static void compareMatchSets(Stream matchSet, Set expected) { Set translatedMatchSet = new HashSet<>(); var iterator = matchSet.iterator(); diff --git a/subprojects/store-query/build.gradle b/subprojects/store-query/build.gradle index 2b76e608..97761936 100644 --- a/subprojects/store-query/build.gradle +++ b/subprojects/store-query/build.gradle @@ -1,7 +1,9 @@ plugins { id 'refinery-java-library' + id 'refinery-java-test-fixtures' } dependencies { api project(':refinery-store') + testFixturesApi libs.hamcrest } diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/Dnf.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/Dnf.java index 760b264b..b6744b50 100644 --- a/subprojects/store-query/src/main/java/tools/refinery/store/query/Dnf.java +++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/Dnf.java @@ -1,5 +1,7 @@ package tools.refinery.store.query; +import tools.refinery.store.query.equality.DnfEqualityChecker; +import tools.refinery.store.query.equality.LiteralEqualityHelper; import tools.refinery.store.query.literal.CallPolarity; import tools.refinery.store.query.literal.DnfCallLiteral; import tools.refinery.store.query.literal.LiteralReduction; @@ -7,6 +9,8 @@ import tools.refinery.store.query.literal.LiteralReduction; import java.util.*; public final class Dnf implements RelationLike { + private static final String INDENTATION = " "; + private final String name; private final String uniqueName; @@ -50,7 +54,11 @@ public final class Dnf implements RelationLike { @Override public String name() { - return name; + return name == null ? uniqueName : name; + } + + public boolean isExplicitlyNamed() { + return name == null; } public String getUniqueName() { @@ -102,6 +110,61 @@ public final class Dnf implements RelationLike { return call(CallPolarity.TRANSITIVE, List.of(left, right)); } + public boolean equalsWithSubstitution(DnfEqualityChecker callEqualityChecker, Dnf other) { + if (arity() != other.arity()) { + return false; + } + int numClauses = clauses.size(); + if (numClauses != other.clauses.size()) { + return false; + } + for (int i = 0; i < numClauses; i++) { + var literalEqualityHelper = new LiteralEqualityHelper(callEqualityChecker, parameters, other.parameters); + if (!clauses.get(i).equalsWithSubstitution(literalEqualityHelper, other.clauses.get(i))) { + return false; + } + } + return true; + } + + @Override + public String toString() { + var builder = new StringBuilder(); + builder.append("pred ").append(name()).append("("); + var parameterIterator = parameters.iterator(); + if (parameterIterator.hasNext()) { + builder.append(parameterIterator.next()); + while (parameterIterator.hasNext()) { + builder.append(", ").append(parameterIterator.next()); + } + } + builder.append(") <->"); + var clauseIterator = clauses.iterator(); + if (clauseIterator.hasNext()) { + appendClause(clauseIterator.next(), builder); + while (clauseIterator.hasNext()) { + builder.append("\n;"); + appendClause(clauseIterator.next(), builder); + } + } else { + builder.append("\n").append(INDENTATION).append(""); + } + builder.append(".\n"); + return builder.toString(); + } + + private static void appendClause(DnfClause clause, StringBuilder builder) { + var iterator = clause.literals().iterator(); + if (!iterator.hasNext()) { + builder.append("\n").append(INDENTATION).append(""); + return; + } + builder.append("\n").append(INDENTATION).append(iterator.next()); + while (iterator.hasNext()) { + builder.append(",\n").append(INDENTATION).append(iterator.next()); + } + } + public static DnfBuilder builder() { return builder(null); } diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/DnfBuilder.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/DnfBuilder.java index b18b5177..ca47e979 100644 --- a/subprojects/store-query/src/main/java/tools/refinery/store/query/DnfBuilder.java +++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/DnfBuilder.java @@ -52,7 +52,8 @@ public class DnfBuilder { } public DnfBuilder clause(Collection literals) { - var filteredLiterals = new ArrayList(literals.size()); + // Remove duplicates by using a hashed data structure. + var filteredLiterals = new LinkedHashSet(literals.size()); for (var literal : literals) { var reduction = literal.getReduction(); switch (reduction) { @@ -65,10 +66,10 @@ public class DnfBuilder { // Clauses with {@code false} literals can be omitted entirely. return this; } - default -> throw new IllegalStateException("Invalid reduction %s".formatted(reduction)); + default -> throw new IllegalArgumentException("Invalid reduction: " + reduction); } } - clauses.add(Collections.unmodifiableList(filteredLiterals)); + clauses.add(List.copyOf(filteredLiterals)); return this; } @@ -77,10 +78,7 @@ public class DnfBuilder { } public DnfBuilder clauses(DnfClause... clauses) { - for (var clause : clauses) { - this.clause(clause); - } - return this; + return clauses(List.of(clauses)); } public DnfBuilder clauses(Collection clauses) { @@ -91,18 +89,27 @@ public class DnfBuilder { } public Dnf build() { + var postProcessedClauses = postProcessClauses(); + return new Dnf(name, Collections.unmodifiableList(parameters), + Collections.unmodifiableList(functionalDependencies), + Collections.unmodifiableList(postProcessedClauses)); + } + + private List postProcessClauses() { var postProcessedClauses = new ArrayList(clauses.size()); - for (var constraints : clauses) { + for (var literals : clauses) { + if (literals.isEmpty()) { + // Predicate will always match, the other clauses are irrelevant. + return List.of(new DnfClause(Set.of(), List.of())); + } var variables = new HashSet(); - for (var constraint : constraints) { + for (var constraint : literals) { constraint.collectAllVariables(variables); } parameters.forEach(variables::remove); postProcessedClauses.add(new DnfClause(Collections.unmodifiableSet(variables), - Collections.unmodifiableList(constraints))); + Collections.unmodifiableList(literals))); } - return new Dnf(name, Collections.unmodifiableList(parameters), - Collections.unmodifiableList(functionalDependencies), - Collections.unmodifiableList(postProcessedClauses)); + return postProcessedClauses; } } diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/DnfClause.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/DnfClause.java index 2ba6becc..c6e8b8c9 100644 --- a/subprojects/store-query/src/main/java/tools/refinery/store/query/DnfClause.java +++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/DnfClause.java @@ -1,9 +1,22 @@ package tools.refinery.store.query; +import tools.refinery.store.query.equality.LiteralEqualityHelper; import tools.refinery.store.query.literal.Literal; import java.util.List; import java.util.Set; public record DnfClause(Set quantifiedVariables, List literals) { + public boolean equalsWithSubstitution(LiteralEqualityHelper helper, DnfClause other) { + int size = literals.size(); + if (size != other.literals.size()) { + return false; + } + for (int i = 0; i < size; i++) { + if (!literals.get(i).equalsWithSubstitution(helper, other.literals.get(i))) { + return false; + } + } + return true; + } } diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/DnfUtils.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/DnfUtils.java index 17564d43..c7a2849c 100644 --- a/subprojects/store-query/src/main/java/tools/refinery/store/query/DnfUtils.java +++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/DnfUtils.java @@ -1,6 +1,5 @@ package tools.refinery.store.query; -import java.util.Map; import java.util.UUID; public final class DnfUtils { @@ -17,8 +16,4 @@ public final class DnfUtils { return originalName + uniqueString; } } - - public static Variable maybeSubstitute(Variable variable, Map substitution) { - return substitution.getOrDefault(variable, variable); - } } diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/EmptyResultSet.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/EmptyResultSet.java new file mode 100644 index 00000000..a01a5a2f --- /dev/null +++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/EmptyResultSet.java @@ -0,0 +1,49 @@ +package tools.refinery.store.query; + +import tools.refinery.store.tuple.Tuple; +import tools.refinery.store.tuple.TupleLike; + +import java.util.Optional; +import java.util.stream.Stream; + +public class EmptyResultSet implements ResultSet { + @Override + public boolean hasResult() { + return false; + } + + @Override + public boolean hasResult(Tuple parameters) { + return false; + } + + @Override + public Optional oneResult() { + return Optional.empty(); + } + + @Override + public Optional oneResult(Tuple parameters) { + return Optional.empty(); + } + + @Override + public Stream allResults() { + return Stream.of(); + } + + @Override + public Stream allResults(Tuple parameters) { + return Stream.of(); + } + + @Override + public int countResults() { + return 0; + } + + @Override + public int countResults(Tuple parameters) { + return 0; + } +} diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/Variable.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/Variable.java index 2eb87649..d0e0dead 100644 --- a/subprojects/store-query/src/main/java/tools/refinery/store/query/Variable.java +++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/Variable.java @@ -20,15 +20,15 @@ public class Variable { } public String getName() { - return name; + return name == null ? uniqueName : name; } - public String getUniqueName() { - return uniqueName; + public boolean isExplicitlyNamed() { + return name != null; } - public boolean isNamed() { - return name != null; + public String getUniqueName() { + return uniqueName; } public ConstantLiteral isConstant(int value) { @@ -43,6 +43,11 @@ public class Variable { return new EquivalenceLiteral(false, this, other); } + @Override + public String toString() { + return getName(); + } + @Override public boolean equals(Object o) { if (this == o) return true; diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/equality/DeepDnfEqualityChecker.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/equality/DeepDnfEqualityChecker.java new file mode 100644 index 00000000..ebd7f5b0 --- /dev/null +++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/equality/DeepDnfEqualityChecker.java @@ -0,0 +1,31 @@ +package tools.refinery.store.query.equality; + +import tools.refinery.store.query.Dnf; +import tools.refinery.store.util.CycleDetectingMapper; + +import java.util.List; + +public class DeepDnfEqualityChecker implements DnfEqualityChecker { + private final CycleDetectingMapper mapper = new CycleDetectingMapper<>(Pair::toString, + this::doCheckEqual); + + @Override + public boolean dnfEqual(Dnf left, Dnf right) { + return mapper.map(new Pair(left, right)); + } + + protected boolean doCheckEqual(Pair pair) { + return pair.left.equalsWithSubstitution(this, pair.right); + } + + protected List getInProgress() { + return mapper.getInProgress(); + } + + protected record Pair(Dnf left, Dnf right) { + @Override + public String toString() { + return "(%s, %s)".formatted(left.name(), right.name()); + } + } +} diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/equality/DnfEqualityChecker.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/equality/DnfEqualityChecker.java new file mode 100644 index 00000000..eb77de17 --- /dev/null +++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/equality/DnfEqualityChecker.java @@ -0,0 +1,8 @@ +package tools.refinery.store.query.equality; + +import tools.refinery.store.query.Dnf; + +@FunctionalInterface +public interface DnfEqualityChecker { + boolean dnfEqual(Dnf left, Dnf right); +} diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/equality/LiteralEqualityHelper.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/equality/LiteralEqualityHelper.java new file mode 100644 index 00000000..23f1acc7 --- /dev/null +++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/equality/LiteralEqualityHelper.java @@ -0,0 +1,48 @@ +package tools.refinery.store.query.equality; + +import tools.refinery.store.query.Dnf; +import tools.refinery.store.query.Variable; + +import java.util.HashMap; +import java.util.List; +import java.util.Map; + +public class LiteralEqualityHelper { + private final DnfEqualityChecker dnfEqualityChecker; + private final Map leftToRight; + private final Map rightToLeft; + + public LiteralEqualityHelper(DnfEqualityChecker dnfEqualityChecker, List leftParameters, + List rightParameters) { + this.dnfEqualityChecker = dnfEqualityChecker; + var arity = leftParameters.size(); + if (arity != rightParameters.size()) { + throw new IllegalArgumentException("Parameter lists have unequal length"); + } + leftToRight = new HashMap<>(arity); + rightToLeft = new HashMap<>(arity); + for (int i = 0; i < arity; i++) { + if (!variableEqual(leftParameters.get(i), rightParameters.get(i))) { + throw new IllegalArgumentException("Parameter lists cannot be unified: duplicate parameter " + i); + } + } + } + + public boolean dnfEqual(Dnf left, Dnf right) { + return dnfEqualityChecker.dnfEqual(left, right); + } + + public boolean variableEqual(Variable left, Variable right) { + if (checkMapping(leftToRight, left, right) && checkMapping(rightToLeft, right, left)) { + leftToRight.put(left, right); + rightToLeft.put(right, left); + return true; + } + return false; + } + + private static boolean checkMapping(Map map, Variable key, Variable expectedValue) { + var currentValue = map.get(key); + return currentValue == null || currentValue.equals(expectedValue); + } +} diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/BooleanLiteral.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/BooleanLiteral.java index fd2f1eec..6d751be8 100644 --- a/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/BooleanLiteral.java +++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/BooleanLiteral.java @@ -1,18 +1,19 @@ package tools.refinery.store.query.literal; import tools.refinery.store.query.Variable; +import tools.refinery.store.query.equality.LiteralEqualityHelper; +import tools.refinery.store.query.substitution.Substitution; -import java.util.Map; import java.util.Set; -public class BooleanLiteral implements Literal { - public static final BooleanLiteral TRUE = new BooleanLiteral(LiteralReduction.ALWAYS_TRUE); - public static final BooleanLiteral FALSE = new BooleanLiteral(LiteralReduction.ALWAYS_FALSE); +public enum BooleanLiteral implements PolarLiteral { + TRUE(true), + FALSE(false); - private final LiteralReduction reduction; + private final boolean value; - private BooleanLiteral(LiteralReduction reduction) { - this.reduction = reduction; + BooleanLiteral(boolean value) { + this.value = value; } @Override @@ -21,14 +22,29 @@ public class BooleanLiteral implements Literal { } @Override - public Literal substitute(Map substitution) { + public Literal substitute(Substitution substitution) { // No variables to substitute. return this; } @Override public LiteralReduction getReduction() { - return reduction; + return value ? LiteralReduction.ALWAYS_TRUE : LiteralReduction.ALWAYS_FALSE; + } + + @Override + public BooleanLiteral negate() { + return fromBoolean(!value); + } + + @Override + public boolean equalsWithSubstitution(LiteralEqualityHelper helper, Literal other) { + return equals(other); + } + + @Override + public String toString() { + return Boolean.toString(value); } public static BooleanLiteral fromBoolean(boolean value) { diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/CallLiteral.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/CallLiteral.java index 5e1ae94d..091b4e04 100644 --- a/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/CallLiteral.java +++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/CallLiteral.java @@ -1,11 +1,11 @@ package tools.refinery.store.query.literal; -import tools.refinery.store.query.DnfUtils; import tools.refinery.store.query.RelationLike; import tools.refinery.store.query.Variable; +import tools.refinery.store.query.equality.LiteralEqualityHelper; +import tools.refinery.store.query.substitution.Substitution; import java.util.List; -import java.util.Map; import java.util.Objects; import java.util.Set; @@ -31,6 +31,8 @@ public abstract class CallLiteral implements Literal { return polarity; } + public abstract Class getTargetType(); + public T getTarget() { return target; } @@ -46,8 +48,44 @@ public abstract class CallLiteral implements Literal { } } - protected List substituteArguments(Map substitution) { - return arguments.stream().map(variable -> DnfUtils.maybeSubstitute(variable, substitution)).toList(); + protected List substituteArguments(Substitution substitution) { + return arguments.stream().map(substitution::getSubstitute).toList(); + } + + /** + * Compares the target of this call literal with another object. + * + * @param helper Equality helper for comparing {@link Variable} and {@link tools.refinery.store.query.Dnf} + * instances. + * @param otherTarget The object to compare the target to. + * @return {@code true} if {@code otherTarget} is equal to the return value of {@link #getTarget()} according to + * {@code helper}, {@code false} otherwise. + */ + protected boolean targetEquals(LiteralEqualityHelper helper, T otherTarget) { + return target.equals(otherTarget); + } + + @Override + public boolean equalsWithSubstitution(LiteralEqualityHelper helper, Literal other) { + if (other.getClass() != getClass()) { + return false; + } + var otherCallLiteral = (CallLiteral) other; + if (getTargetType() != otherCallLiteral.getTargetType() || polarity != otherCallLiteral.polarity) { + return false; + } + var arity = arguments.size(); + if (arity != otherCallLiteral.arguments.size()) { + return false; + } + for (int i = 0; i < arity; i++) { + if (!helper.variableEqual(arguments.get(i), otherCallLiteral.arguments.get(i))) { + return false; + } + } + @SuppressWarnings("unchecked") + var otherTarget = (T) otherCallLiteral.target; + return targetEquals(helper, otherTarget); } @Override @@ -63,4 +101,33 @@ public abstract class CallLiteral implements Literal { public int hashCode() { return Objects.hash(polarity, target, arguments); } + + protected String targetToString() { + return "@%s %s".formatted(getTargetType().getSimpleName(), target.name()); + } + + @Override + public String toString() { + var builder = new StringBuilder(); + if (!polarity.isPositive()) { + builder.append("!("); + } + builder.append(targetToString()); + if (polarity.isTransitive()) { + builder.append("+"); + } + builder.append("("); + var argumentIterator = arguments.iterator(); + if (argumentIterator.hasNext()) { + builder.append(argumentIterator.next()); + while (argumentIterator.hasNext()) { + builder.append(", ").append(argumentIterator.next()); + } + } + builder.append(")"); + if (!polarity.isPositive()) { + builder.append(")"); + } + return builder.toString(); + } } diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/ConstantLiteral.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/ConstantLiteral.java index 746d23af..d01c7d20 100644 --- a/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/ConstantLiteral.java +++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/ConstantLiteral.java @@ -1,9 +1,9 @@ package tools.refinery.store.query.literal; -import tools.refinery.store.query.DnfUtils; import tools.refinery.store.query.Variable; +import tools.refinery.store.query.equality.LiteralEqualityHelper; +import tools.refinery.store.query.substitution.Substitution; -import java.util.Map; import java.util.Set; public record ConstantLiteral(Variable variable, int nodeId) implements Literal { @@ -13,7 +13,21 @@ public record ConstantLiteral(Variable variable, int nodeId) implements Literal } @Override - public ConstantLiteral substitute(Map substitution) { - return new ConstantLiteral(DnfUtils.maybeSubstitute(variable, substitution), nodeId); + public ConstantLiteral substitute(Substitution substitution) { + return new ConstantLiteral(substitution.getSubstitute(variable), nodeId); + } + + @Override + public boolean equalsWithSubstitution(LiteralEqualityHelper helper, Literal other) { + if (other.getClass() != getClass()) { + return false; + } + var otherConstantLiteral = (ConstantLiteral) other; + return helper.variableEqual(variable, otherConstantLiteral.variable) && nodeId == otherConstantLiteral.nodeId; + } + + @Override + public String toString() { + return "%s === @Constant %d".formatted(variable, nodeId); } } diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/DnfCallLiteral.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/DnfCallLiteral.java index de6c6005..27917265 100644 --- a/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/DnfCallLiteral.java +++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/DnfCallLiteral.java @@ -2,9 +2,10 @@ package tools.refinery.store.query.literal; import tools.refinery.store.query.Dnf; import tools.refinery.store.query.Variable; +import tools.refinery.store.query.equality.LiteralEqualityHelper; +import tools.refinery.store.query.substitution.Substitution; import java.util.List; -import java.util.Map; public final class DnfCallLiteral extends CallLiteral implements PolarLiteral { public DnfCallLiteral(CallPolarity polarity, Dnf target, List arguments) { @@ -12,7 +13,12 @@ public final class DnfCallLiteral extends CallLiteral implements PolarLiter } @Override - public DnfCallLiteral substitute(Map substitution) { + public Class getTargetType() { + return Dnf.class; + } + + @Override + public DnfCallLiteral substitute(Substitution substitution) { return new DnfCallLiteral(getPolarity(), getTarget(), substituteArguments(substitution)); } @@ -26,4 +32,9 @@ public final class DnfCallLiteral extends CallLiteral implements PolarLiter var dnfReduction = getTarget().getReduction(); return getPolarity().isPositive() ? dnfReduction : dnfReduction.negate(); } + + @Override + protected boolean targetEquals(LiteralEqualityHelper helper, Dnf otherTarget) { + return helper.dnfEqual(getTarget(), otherTarget); + } } diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/EquivalenceLiteral.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/EquivalenceLiteral.java index f30179b2..61c753c3 100644 --- a/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/EquivalenceLiteral.java +++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/EquivalenceLiteral.java @@ -1,9 +1,9 @@ package tools.refinery.store.query.literal; -import tools.refinery.store.query.DnfUtils; import tools.refinery.store.query.Variable; +import tools.refinery.store.query.equality.LiteralEqualityHelper; +import tools.refinery.store.query.substitution.Substitution; -import java.util.Map; import java.util.Set; public record EquivalenceLiteral(boolean positive, Variable left, Variable right) @@ -20,9 +20,8 @@ public record EquivalenceLiteral(boolean positive, Variable left, Variable right } @Override - public EquivalenceLiteral substitute(Map substitution) { - return new EquivalenceLiteral(positive, DnfUtils.maybeSubstitute(left, substitution), - DnfUtils.maybeSubstitute(right, substitution)); + public EquivalenceLiteral substitute(Substitution substitution) { + return new EquivalenceLiteral(positive, substitution.getSubstitute(left), substitution.getSubstitute(right)); } @Override @@ -32,4 +31,19 @@ public record EquivalenceLiteral(boolean positive, Variable left, Variable right } return LiteralReduction.NOT_REDUCIBLE; } + + @Override + public boolean equalsWithSubstitution(LiteralEqualityHelper helper, Literal other) { + if (other.getClass() != getClass()) { + return false; + } + var otherEquivalenceLiteral = (EquivalenceLiteral) other; + return helper.variableEqual(left, otherEquivalenceLiteral.left) && helper.variableEqual(right, + otherEquivalenceLiteral.right); + } + + @Override + public String toString() { + return "%s %s %s".formatted(left, positive ? "===" : "!==", right); + } } diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/Literal.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/Literal.java index a6893acf..ddd91775 100644 --- a/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/Literal.java +++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/Literal.java @@ -1,16 +1,20 @@ package tools.refinery.store.query.literal; import tools.refinery.store.query.Variable; +import tools.refinery.store.query.equality.LiteralEqualityHelper; +import tools.refinery.store.query.substitution.Substitution; -import java.util.Map; import java.util.Set; public interface Literal { void collectAllVariables(Set variables); - Literal substitute(Map substitution); + Literal substitute(Substitution substitution); default LiteralReduction getReduction() { return LiteralReduction.NOT_REDUCIBLE; } + + @SuppressWarnings("BooleanMethodIsAlwaysInverted") + boolean equalsWithSubstitution(LiteralEqualityHelper helper, Literal other); } diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/RelationViewLiteral.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/RelationViewLiteral.java index 4718b550..fb8b3332 100644 --- a/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/RelationViewLiteral.java +++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/RelationViewLiteral.java @@ -1,10 +1,10 @@ package tools.refinery.store.query.literal; import tools.refinery.store.query.Variable; +import tools.refinery.store.query.substitution.Substitution; import tools.refinery.store.query.view.AnyRelationView; import java.util.List; -import java.util.Map; public final class RelationViewLiteral extends CallLiteral implements PolarLiteral { @@ -13,7 +13,18 @@ public final class RelationViewLiteral extends CallLiteral } @Override - public RelationViewLiteral substitute(Map substitution) { + public Class getTargetType() { + return AnyRelationView.class; + } + + @Override + protected String targetToString() { + var target = getTarget(); + return "@RelationView(\"%s\") %s".formatted(target.getViewName(), target.getSymbol().name()); + } + + @Override + public RelationViewLiteral substitute(Substitution substitution) { return new RelationViewLiteral(getPolarity(), getTarget(), substituteArguments(substitution)); } diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/substitution/MapBasedSubstitution.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/substitution/MapBasedSubstitution.java new file mode 100644 index 00000000..ffc65047 --- /dev/null +++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/substitution/MapBasedSubstitution.java @@ -0,0 +1,13 @@ +package tools.refinery.store.query.substitution; + +import tools.refinery.store.query.Variable; + +import java.util.Map; + +public record MapBasedSubstitution(Map map, Substitution fallback) implements Substitution { + @Override + public Variable getSubstitute(Variable variable) { + var value = map.get(variable); + return value == null ? fallback.getSubstitute(variable) : value; + } +} diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/substitution/RenewingSubstitution.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/substitution/RenewingSubstitution.java new file mode 100644 index 00000000..54d18a3f --- /dev/null +++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/substitution/RenewingSubstitution.java @@ -0,0 +1,19 @@ +package tools.refinery.store.query.substitution; + +import tools.refinery.store.query.Variable; + +import java.util.HashMap; +import java.util.Map; + +public class RenewingSubstitution implements Substitution { + private final Map alreadyRenewed = new HashMap<>(); + + @Override + public Variable getSubstitute(Variable variable) { + return alreadyRenewed.computeIfAbsent(variable, RenewingSubstitution::renew); + } + + private static Variable renew(Variable variable) { + return variable.isExplicitlyNamed() ? new Variable(variable.getName()) : new Variable(); + } +} diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/substitution/StatelessSubstitution.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/substitution/StatelessSubstitution.java new file mode 100644 index 00000000..d33ad6fb --- /dev/null +++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/substitution/StatelessSubstitution.java @@ -0,0 +1,18 @@ +package tools.refinery.store.query.substitution; + +import tools.refinery.store.query.Variable; + +public enum StatelessSubstitution implements Substitution { + FAILING { + @Override + public Variable getSubstitute(Variable variable) { + throw new IllegalArgumentException("No substitute for " + variable); + } + }, + IDENTITY { + @Override + public Variable getSubstitute(Variable variable) { + return variable; + } + } +} diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/substitution/Substitution.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/substitution/Substitution.java new file mode 100644 index 00000000..9d086bf5 --- /dev/null +++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/substitution/Substitution.java @@ -0,0 +1,8 @@ +package tools.refinery.store.query.substitution; + +import tools.refinery.store.query.Variable; + +@FunctionalInterface +public interface Substitution { + Variable getSubstitute(Variable variable); +} diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/substitution/Substitutions.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/substitution/Substitutions.java new file mode 100644 index 00000000..26cf1a20 --- /dev/null +++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/substitution/Substitutions.java @@ -0,0 +1,27 @@ +package tools.refinery.store.query.substitution; + +import tools.refinery.store.query.Variable; + +import java.util.Map; + +public final class Substitutions { + private Substitutions() { + throw new IllegalStateException("This is a static utility class and should not be instantiate directly"); + } + + public static Substitution total(Map map) { + return new MapBasedSubstitution(map, StatelessSubstitution.FAILING); + } + + public static Substitution partial(Map map) { + return new MapBasedSubstitution(map, StatelessSubstitution.IDENTITY); + } + + public static Substitution renewing(Map map) { + return new MapBasedSubstitution(map, renewing()); + } + + public static Substitution renewing() { + return new RenewingSubstitution(); + } +} diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/view/AnyRelationView.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/view/AnyRelationView.java index 328cde3a..bc3ac1ea 100644 --- a/subprojects/store-query/src/main/java/tools/refinery/store/query/view/AnyRelationView.java +++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/view/AnyRelationView.java @@ -10,6 +10,8 @@ import java.util.Set; public sealed interface AnyRelationView extends RelationLike permits RelationView { AnySymbol getSymbol(); + String getViewName(); + default Set> getFunctionalDependencies() { return Set.of(); } diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/view/RelationView.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/view/RelationView.java index 2714a8c5..ea9fd5e2 100644 --- a/subprojects/store-query/src/main/java/tools/refinery/store/query/view/RelationView.java +++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/view/RelationView.java @@ -21,11 +21,11 @@ import java.util.UUID; public abstract non-sealed class RelationView implements AnyRelationView { private final Symbol symbol; - private final String name; + private final String viewName; - protected RelationView(Symbol symbol, String name) { + protected RelationView(Symbol symbol, String viewName) { this.symbol = symbol; - this.name = name; + this.viewName = viewName; } protected RelationView(Symbol representation) { @@ -37,9 +37,14 @@ public abstract non-sealed class RelationView implements AnyRelationView { return symbol; } + @Override + public String getViewName() { + return viewName; + } + @Override public String name() { - return symbol.name() + "#" + name; + return symbol.name() + "#" + viewName; } public abstract boolean filter(Tuple key, T value); @@ -72,11 +77,11 @@ public abstract non-sealed class RelationView implements AnyRelationView { if (this == o) return true; if (o == null || getClass() != o.getClass()) return false; RelationView that = (RelationView) o; - return Objects.equals(symbol, that.symbol) && Objects.equals(name, that.name); + return Objects.equals(symbol, that.symbol) && Objects.equals(viewName, that.viewName); } @Override public int hashCode() { - return Objects.hash(symbol, name); + return Objects.hash(symbol, viewName); } } 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) <-> + . + """)); + } + + @Test + void noParametersTest() { + var dnf = Dnf.builder("Example").build(); + + assertThat(dnf.toString(), is(""" + pred Example() <-> + . + """)); + } + + @Test + void emptyClauseTest() { + var p = new Variable("p"); + var dnf = Dnf.builder("Example").parameter(p).clause().build(); + + assertThat(dnf.toString(), is(""" + pred Example(p) <-> + . + """)); + } + + @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 ")); + } +} diff --git a/subprojects/store-query/src/testFixtures/java/tools/refinery/store/query/tests/MismatchDescribingDnfEqualityChecker.java b/subprojects/store-query/src/testFixtures/java/tools/refinery/store/query/tests/MismatchDescribingDnfEqualityChecker.java new file mode 100644 index 00000000..aaab2e7e --- /dev/null +++ b/subprojects/store-query/src/testFixtures/java/tools/refinery/store/query/tests/MismatchDescribingDnfEqualityChecker.java @@ -0,0 +1,43 @@ +package tools.refinery.store.query.tests; + +import org.hamcrest.Description; +import tools.refinery.store.query.equality.DeepDnfEqualityChecker; + +class MismatchDescribingDnfEqualityChecker extends DeepDnfEqualityChecker { + private final Description description; + private boolean described; + + MismatchDescribingDnfEqualityChecker(Description description) { + this.description = description; + } + + public boolean isDescribed() { + return described; + } + + @Override + protected boolean doCheckEqual(Pair pair) { + boolean result = super.doCheckEqual(pair); + if (!result && !described) { + describeMismatch(pair); + // Only describe the first found (innermost) mismatch. + described = true; + } + return result; + } + + private void describeMismatch(Pair pair) { + var inProgress = getInProgress(); + int size = inProgress.size(); + if (size <= 1) { + description.appendText("was ").appendValue(pair.left()); + return; + } + var last = inProgress.get(size - 1); + description.appendText("expected ").appendValue(last.right()); + for (int i = size - 2; i >= 0; i--) { + description.appendText(" called from ").appendText(inProgress.get(i).left().name()); + } + description.appendText(" was not structurally equal to ").appendValue(last.right()); + } +} diff --git a/subprojects/store-query/src/testFixtures/java/tools/refinery/store/query/tests/QueryMatchers.java b/subprojects/store-query/src/testFixtures/java/tools/refinery/store/query/tests/QueryMatchers.java new file mode 100644 index 00000000..83614278 --- /dev/null +++ b/subprojects/store-query/src/testFixtures/java/tools/refinery/store/query/tests/QueryMatchers.java @@ -0,0 +1,14 @@ +package tools.refinery.store.query.tests; + +import org.hamcrest.Matcher; +import tools.refinery.store.query.Dnf; + +public final class QueryMatchers { + private QueryMatchers() { + throw new IllegalStateException("This is a static utility class and should not be instantiated directly"); + } + + public static Matcher structurallyEqualTo(Dnf expected) { + return new StructurallyEqualTo(expected); + } +} diff --git a/subprojects/store-query/src/testFixtures/java/tools/refinery/store/query/tests/StructurallyEqualTo.java b/subprojects/store-query/src/testFixtures/java/tools/refinery/store/query/tests/StructurallyEqualTo.java new file mode 100644 index 00000000..a42396dd --- /dev/null +++ b/subprojects/store-query/src/testFixtures/java/tools/refinery/store/query/tests/StructurallyEqualTo.java @@ -0,0 +1,36 @@ +package tools.refinery.store.query.tests; + +import org.hamcrest.Description; +import org.hamcrest.TypeSafeMatcher; +import tools.refinery.store.query.Dnf; +import tools.refinery.store.query.equality.DeepDnfEqualityChecker; + +public class StructurallyEqualTo extends TypeSafeMatcher { + private final Dnf expected; + + public StructurallyEqualTo(Dnf expected) { + this.expected = expected; + } + + @Override + protected boolean matchesSafely(Dnf item) { + var checker = new DeepDnfEqualityChecker(); + return checker.dnfEqual(expected, item); + } + + @Override + protected void describeMismatchSafely(Dnf item, Description mismatchDescription) { + var describingChecker = new MismatchDescribingDnfEqualityChecker(mismatchDescription); + if (describingChecker.dnfEqual(expected, item)) { + throw new IllegalStateException("Mismatched Dnf was matching on repeated comparison"); + } + if (!describingChecker.isDescribed()) { + super.describeMismatchSafely(item, mismatchDescription); + } + } + + @Override + public void describeTo(Description description) { + description.appendText("structurally equal to ").appendValue(expected); + } +} diff --git a/subprojects/store/src/main/java/tools/refinery/store/util/CycleDetectingMapper.java b/subprojects/store/src/main/java/tools/refinery/store/util/CycleDetectingMapper.java index e4b462f0..8a151d01 100644 --- a/subprojects/store/src/main/java/tools/refinery/store/util/CycleDetectingMapper.java +++ b/subprojects/store/src/main/java/tools/refinery/store/util/CycleDetectingMapper.java @@ -1,9 +1,6 @@ package tools.refinery.store.util; -import java.util.HashMap; -import java.util.LinkedHashSet; -import java.util.Map; -import java.util.Set; +import java.util.*; import java.util.function.Function; import java.util.stream.Collectors; @@ -45,6 +42,10 @@ public class CycleDetectingMapper { return result; } + public List getInProgress() { + return List.copyOf(inProgress); + } + public R getAlreadyMapped(T input) { return results.get(input); } -- cgit v1.2.3-54-g00ecf