From c42d391998eca46704c8699c90efd3c357442fb0 Mon Sep 17 00:00:00 2001 From: Kristóf Marussy Date: Mon, 26 Jun 2023 19:38:03 +0200 Subject: feat: Dnf lifting Support for count and aggregation is still missing. --- subprojects/store-reasoning/build.gradle.kts | 1 + .../refinery/store/reasoning/ReasoningAdapter.java | 3 +- .../store/reasoning/lifting/DnfLifter.java | 221 +++++++----- .../refinery/store/reasoning/lifting/ModalDnf.java | 16 - .../store/reasoning/literal/Concreteness.java | 18 + .../store/reasoning/literal/ModalConstraint.java | 39 ++- .../refinery/store/reasoning/literal/Modality.java | 4 +- .../store/reasoning/literal/PartialLiterals.java | 4 - .../reasoning/representation/PartialSymbol.java | 8 + .../store/reasoning/lifting/DnfLifterTest.java | 384 +++++++++++++++++++++ 10 files changed, 586 insertions(+), 112 deletions(-) delete mode 100644 subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/lifting/ModalDnf.java create mode 100644 subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/literal/Concreteness.java create mode 100644 subprojects/store-reasoning/src/test/java/tools/refinery/store/reasoning/lifting/DnfLifterTest.java (limited to 'subprojects/store-reasoning') diff --git a/subprojects/store-reasoning/build.gradle.kts b/subprojects/store-reasoning/build.gradle.kts index abad0491..6c568df0 100644 --- a/subprojects/store-reasoning/build.gradle.kts +++ b/subprojects/store-reasoning/build.gradle.kts @@ -10,4 +10,5 @@ plugins { dependencies { api(project(":refinery-store-query")) + testImplementation(testFixtures(project(":refinery-store-query"))) } diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/ReasoningAdapter.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/ReasoningAdapter.java index 6d5d6f89..66e809f7 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/ReasoningAdapter.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/ReasoningAdapter.java @@ -13,7 +13,8 @@ import tools.refinery.store.reasoning.representation.PartialRelation; import tools.refinery.store.reasoning.representation.PartialSymbol; public interface ReasoningAdapter extends ModelAdapter { - PartialRelation EXISTS = new PartialRelation("exists", 1); + PartialRelation EXISTS = PartialSymbol.of("exists", 1); + PartialRelation EQUALS = PartialSymbol.of("equals", 2); @Override ReasoningStoreAdapter getStoreAdapter(); diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/lifting/DnfLifter.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/lifting/DnfLifter.java index ac41d170..8bbb75d1 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/lifting/DnfLifter.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/lifting/DnfLifter.java @@ -5,124 +5,181 @@ */ package tools.refinery.store.reasoning.lifting; -import org.jetbrains.annotations.Nullable; +import tools.refinery.store.query.Constraint; import tools.refinery.store.query.dnf.Dnf; -import tools.refinery.store.query.dnf.DnfBuilder; import tools.refinery.store.query.dnf.DnfClause; -import tools.refinery.store.query.literal.CallLiteral; -import tools.refinery.store.query.literal.CallPolarity; -import tools.refinery.store.query.literal.Literal; +import tools.refinery.store.query.equality.DnfEqualityChecker; +import tools.refinery.store.query.literal.*; import tools.refinery.store.query.term.NodeVariable; +import tools.refinery.store.query.term.ParameterDirection; import tools.refinery.store.query.term.Variable; import tools.refinery.store.reasoning.ReasoningAdapter; +import tools.refinery.store.reasoning.literal.Concreteness; import tools.refinery.store.reasoning.literal.ModalConstraint; import tools.refinery.store.reasoning.literal.Modality; -import tools.refinery.store.reasoning.literal.PartialLiterals; -import tools.refinery.store.util.CycleDetectingMapper; -import java.util.ArrayList; -import java.util.LinkedHashSet; -import java.util.List; +import java.util.*; +import java.util.stream.Collectors; public class DnfLifter { - private final CycleDetectingMapper mapper = new CycleDetectingMapper<>(ModalDnf::toString, - this::doLift); + private final Map cache = new HashMap<>(); - public Dnf lift(Modality modality, Dnf query) { - return mapper.map(new ModalDnf(modality, query)); + public Dnf lift(Modality modality, Concreteness concreteness, Dnf dnf) { + return cache.computeIfAbsent(new ModalDnf(modality, concreteness, dnf), this::doLift); } private Dnf doLift(ModalDnf modalDnf) { var modality = modalDnf.modality(); + var concreteness = modalDnf.concreteness(); var dnf = modalDnf.dnf(); - var builder = Dnf.builder(); + var builder = Dnf.builder("%s#%s#%s".formatted(dnf.name(), modality, concreteness)); builder.symbolicParameters(dnf.getSymbolicParameters()); - boolean changed = false; + builder.functionalDependencies(dnf.getFunctionalDependencies()); for (var clause : dnf.getClauses()) { - if (liftClause(modality, dnf, clause, builder)) { - changed = true; - } + builder.clause(liftClause(modality, concreteness, dnf, clause)); } - if (changed) { - return builder.build(); + var liftedDnf = builder.build(); + if (dnf.equalsWithSubstitution(DnfEqualityChecker.DEFAULT, liftedDnf)) { + return dnf; } - return dnf; + return liftedDnf; } - private boolean liftClause(Modality modality, Dnf originalDnf, DnfClause clause, DnfBuilder builder) { - boolean changed = false; - var quantifiedVariables = getQuantifiedDataVariables(originalDnf, clause); - var literals = clause.literals(); - var liftedLiterals = new ArrayList(literals.size()); - for (var literal : literals) { - Literal liftedLiteral = liftLiteral(modality, literal); - if (liftedLiteral == null) { - liftedLiteral = literal; - } else { - changed = true; - } + private List liftClause(Modality modality, Concreteness concreteness, Dnf dnf, DnfClause clause) { + var liftedLiterals = new ArrayList(); + for (var literal : clause.literals()) { + var liftedLiteral = liftLiteral(modality, concreteness, clause, literal); liftedLiterals.add(liftedLiteral); - var variable = isExistsLiteralForVariable(modality, liftedLiteral); - if (variable != null) { - // If we already quantify over the existence of the variable with the expected modality, - // we don't need to insert quantification manually. - quantifiedVariables.remove(variable); - } } + var quantifiedVariables = getQuantifiedNodeVariables(dnf, clause); + var existsConstraint = ModalConstraint.of(modality, concreteness, ReasoningAdapter.EXISTS); for (var quantifiedVariable : quantifiedVariables) { - // Quantify over data variables that are not already quantified with the expected modality. - liftedLiterals.add(new CallLiteral(CallPolarity.POSITIVE, - new ModalConstraint(modality, ReasoningAdapter.EXISTS), List.of(quantifiedVariable))); + liftedLiterals.add(existsConstraint.call(quantifiedVariable)); } - builder.clause(liftedLiterals); - return changed || !quantifiedVariables.isEmpty(); + return liftedLiterals; } - private static LinkedHashSet getQuantifiedDataVariables(Dnf originalDnf, DnfClause clause) { - var quantifiedVariables = new LinkedHashSet<>(clause.positiveVariables()); - for (var symbolicParameter : originalDnf.getSymbolicParameters()) { - // The existence of parameters will be checked outside this DNF. - quantifiedVariables.remove(symbolicParameter.getVariable()); + private Literal liftLiteral(Modality modality, Concreteness concreteness, DnfClause clause, Literal literal) { + if (literal instanceof CallLiteral callLiteral) { + return liftCallLiteral(modality, concreteness, clause, callLiteral); + } else if (literal instanceof EquivalenceLiteral equivalenceLiteral) { + return liftEquivalenceLiteral(modality, concreteness, equivalenceLiteral); + } else if (literal instanceof ConstantLiteral || + literal instanceof AssignLiteral || + literal instanceof CheckLiteral) { + return literal; + } else if (literal instanceof CountLiteral) { + throw new IllegalArgumentException("Count literal %s cannot be lifted".formatted(literal)); + } else if (literal instanceof AggregationLiteral) { + throw new IllegalArgumentException("Aggregation literal %s cannot be lifted".formatted(literal)); + } else { + throw new IllegalArgumentException("Unknown literal to lift: " + literal); } - quantifiedVariables.removeIf(variable -> !(variable instanceof NodeVariable)); - return quantifiedVariables; } - @Nullable - private Variable isExistsLiteralForVariable(Modality modality, Literal literal) { - if (literal instanceof CallLiteral callLiteral && - callLiteral.getPolarity() == CallPolarity.POSITIVE && - callLiteral.getTarget() instanceof ModalConstraint modalConstraint && - modalConstraint.modality() == modality && - modalConstraint.constraint().equals(ReasoningAdapter.EXISTS)) { - return callLiteral.getArguments().get(0); + private Literal liftCallLiteral(Modality modality, Concreteness concreteness, DnfClause clause, + CallLiteral callLiteral) { + Constraint target = callLiteral.getTarget(); + var polarity = callLiteral.getPolarity(); + var arguments = callLiteral.getArguments(); + return switch (polarity) { + case POSITIVE -> ModalConstraint.of(modality, concreteness, target).call( + CallPolarity.POSITIVE, arguments); + case NEGATIVE -> { + var callModality = modality.negate(); + boolean needsHelper = !polarity.isPositive() && + !callLiteral.getPrivateVariables(clause.positiveVariables()).isEmpty(); + if (needsHelper) { + yield callNegationHelper(callModality, concreteness, clause, callLiteral, target); + } + yield ModalConstraint.of(callModality, concreteness, target).call( + CallPolarity.NEGATIVE, arguments); + } + case TRANSITIVE -> createTransitiveHelper(modality, concreteness, target).call( + CallPolarity.POSITIVE, arguments); + }; + } + + private Literal callNegationHelper(Modality modality, Concreteness concreteness, DnfClause clause, + CallLiteral callLiteral, Constraint target) { + var builder = Dnf.builder(); + var originalArguments = callLiteral.getArguments(); + var uniqueOriginalArguments = List.copyOf(new LinkedHashSet<>(originalArguments)); + + var alwaysInputVariables = callLiteral.getInputVariables(Set.of()); + for (var variable : uniqueOriginalArguments) { + var direction = alwaysInputVariables.contains(variable) ? ParameterDirection.IN : ParameterDirection.OUT; + builder.parameter(variable, direction); } - return null; + + var literals = new ArrayList(); + var liftedConstraint = ModalConstraint.of(modality, concreteness, target); + literals.add(liftedConstraint.call(CallPolarity.POSITIVE, originalArguments)); + + var privateVariables = callLiteral.getPrivateVariables(clause.positiveVariables()); + var existsConstraint = ModalConstraint.of(modality, concreteness, ReasoningAdapter.EXISTS); + for (var variable : uniqueOriginalArguments) { + if (privateVariables.contains(variable)) { + literals.add(existsConstraint.call(variable)); + } + } + + builder.clause(literals); + var liftedTarget = builder.build(); + return liftedTarget.call(CallPolarity.NEGATIVE, uniqueOriginalArguments); } - @Nullable - private Literal liftLiteral(Modality modality, Literal literal) { - if (!(literal instanceof CallLiteral callLiteral)) { - return null; + private Dnf createTransitiveHelper(Modality modality, Concreteness concreteness, Constraint target) { + var liftedTarget = ModalConstraint.of(modality, concreteness, target); + var existsConstraint = ModalConstraint.of(modality, concreteness, ReasoningAdapter.EXISTS); + var existingEndHelperName = "%s#exisitingEnd#%s#%s".formatted(target.name(), modality, concreteness); + var existingEndHelper = Dnf.of(existingEndHelperName, builder -> { + var start = builder.parameter("start"); + var end = builder.parameter("end"); + builder.clause( + liftedTarget.call(start, end), + existsConstraint.call(end) + ); + }); + var transitiveHelperName = "%s#transitive#%s#%s".formatted(target.name(), modality, concreteness); + return Dnf.of(transitiveHelperName, builder -> { + var start = builder.parameter("start"); + var end = builder.parameter("end"); + builder.clause(liftedTarget.call(start, end)); + builder.clause(middle -> List.of( + existingEndHelper.callTransitive(start, middle), + liftedTarget.call(middle, end) + )); + }); + } + + private Literal liftEquivalenceLiteral(Modality modality, Concreteness concreteness, + EquivalenceLiteral equivalenceLiteral) { + if (equivalenceLiteral.isPositive()) { + return ModalConstraint.of(modality, concreteness, ReasoningAdapter.EQUALS).call( + CallPolarity.POSITIVE, equivalenceLiteral.getLeft(), equivalenceLiteral.getRight()); } - var target = callLiteral.getTarget(); - if (target instanceof ModalConstraint modalTarget) { - var actualTarget = modalTarget.constraint(); - if (actualTarget instanceof Dnf dnf) { - var targetModality = modalTarget.modality(); - var liftedTarget = lift(targetModality, dnf); - return new CallLiteral(callLiteral.getPolarity(), liftedTarget, callLiteral.getArguments()); + return ModalConstraint.of(modality.negate(), concreteness, ReasoningAdapter.EQUALS).call( + CallPolarity.NEGATIVE, equivalenceLiteral.getLeft(), equivalenceLiteral.getRight()); + } + + private static Set getQuantifiedNodeVariables(Dnf dnf, DnfClause clause) { + var quantifiedVariables = clause.positiveVariables().stream() + .filter(Variable::isNodeVariable) + .map(Variable::asNodeVariable) + .collect(Collectors.toCollection(HashSet::new)); + for (var symbolicParameter : dnf.getSymbolicParameters()) { + if (symbolicParameter.getVariable() instanceof NodeVariable nodeParameter) { + quantifiedVariables.remove(nodeParameter); } - // No more lifting to be done, pass any modal call to a partial symbol through. - return null; - } else if (target instanceof Dnf dnf) { - var polarity = callLiteral.getPolarity(); - var liftedTarget = lift(modality.commute(polarity), dnf); - // Use == instead of equals(), because lift will return the same object by reference is there are no - // changes made during lifting. - return liftedTarget == target ? null : new CallLiteral(polarity, liftedTarget, callLiteral.getArguments()); - } else { - return PartialLiterals.addModality(callLiteral, modality); + } + return quantifiedVariables; + } + + private record ModalDnf(Modality modality, Concreteness concreteness, Dnf dnf) { + @Override + public String toString() { + return "%s %s %s".formatted(modality, concreteness, dnf.name()); } } } diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/lifting/ModalDnf.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/lifting/ModalDnf.java deleted file mode 100644 index 16fb8fbf..00000000 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/lifting/ModalDnf.java +++ /dev/null @@ -1,16 +0,0 @@ -/* - * SPDX-FileCopyrightText: 2021-2023 The Refinery Authors - * - * SPDX-License-Identifier: EPL-2.0 - */ -package tools.refinery.store.reasoning.lifting; - -import tools.refinery.store.query.dnf.Dnf; -import tools.refinery.store.reasoning.literal.Modality; - -record ModalDnf(Modality modality, Dnf dnf) { - @Override - public String toString() { - return "%s %s".formatted(modality, dnf.name()); - } -} diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/literal/Concreteness.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/literal/Concreteness.java new file mode 100644 index 00000000..43ac5904 --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/literal/Concreteness.java @@ -0,0 +1,18 @@ +/* + * SPDX-FileCopyrightText: 2023 The Refinery Authors + * + * SPDX-License-Identifier: EPL-2.0 + */ +package tools.refinery.store.reasoning.literal; + +import java.util.Locale; + +public enum Concreteness { + PARTIAL, + CANDIDATE; + + @Override + public String toString() { + return name().toLowerCase(Locale.ROOT); + } +} diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/literal/ModalConstraint.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/literal/ModalConstraint.java index 4e5a6099..6e0e91e1 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/literal/ModalConstraint.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/literal/ModalConstraint.java @@ -9,15 +9,25 @@ import tools.refinery.store.query.Constraint; import tools.refinery.store.query.equality.LiteralEqualityHelper; import tools.refinery.store.query.literal.Reduction; import tools.refinery.store.query.term.Parameter; +import tools.refinery.store.query.view.AnySymbolView; import java.util.List; -public record ModalConstraint(Modality modality, Constraint constraint) implements Constraint { - private static final String FORMAT = "%s %s"; +public record ModalConstraint(Modality modality, Concreteness concreteness, Constraint constraint) + implements Constraint { + public ModalConstraint { + if (constraint instanceof AnySymbolView || constraint instanceof ModalConstraint) { + throw new IllegalArgumentException("Already concrete constraints cannot be abstracted"); + } + } + + public ModalConstraint(Modality modality, Constraint constraint) { + this(modality, Concreteness.PARTIAL, constraint); + } @Override public String name() { - return FORMAT.formatted(modality, constraint.name()); + return formatName(constraint.name()); } @Override @@ -36,16 +46,33 @@ public record ModalConstraint(Modality modality, Constraint constraint) implemen return false; } var otherModalConstraint = (ModalConstraint) other; - return modality == otherModalConstraint.modality && constraint.equals(helper, otherModalConstraint.constraint); + return modality == otherModalConstraint.modality && + concreteness == otherModalConstraint.concreteness && + constraint.equals(helper, otherModalConstraint.constraint); } @Override public String toReferenceString() { - return FORMAT.formatted(modality, constraint.toReferenceString()); + return formatName(constraint.toReferenceString()); } @Override public String toString() { - return FORMAT.formatted(modality, constraint); + return formatName(constraint.toString()); + } + + private String formatName(String constraintName) { + if (concreteness == Concreteness.PARTIAL) { + return "%s %s".formatted(modality, constraintName); + } + return "%s %s %s".formatted(modality, concreteness, constraintName); + } + + public static Constraint of(Modality modality, Concreteness concreteness, Constraint constraint) { + if (constraint instanceof AnySymbolView || constraint instanceof ModalConstraint) { + // Symbol views and lifted constraints are already concrete. Thus, they cannot be abstracted at all. + return constraint; + } + return new ModalConstraint(modality, concreteness, constraint); } } diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/literal/Modality.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/literal/Modality.java index 96466d5c..c99a0399 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/literal/Modality.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/literal/Modality.java @@ -11,14 +11,12 @@ import java.util.Locale; public enum Modality { MUST, - MAY, - CURRENT; + MAY; public Modality negate() { return switch(this) { case MUST -> MAY; case MAY -> MUST; - case CURRENT -> CURRENT; }; } diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/literal/PartialLiterals.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/literal/PartialLiterals.java index 0e46a795..4f07f17d 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/literal/PartialLiterals.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/literal/PartialLiterals.java @@ -20,10 +20,6 @@ public final class PartialLiterals { return addModality(literal, Modality.MUST); } - public static CallLiteral current(CallLiteral literal) { - return addModality(literal, Modality.CURRENT); - } - public static CallLiteral addModality(CallLiteral literal, Modality modality) { var target = literal.getTarget(); if (target instanceof ModalConstraint) { diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/representation/PartialSymbol.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/representation/PartialSymbol.java index 3a08bdd8..2f04534a 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/representation/PartialSymbol.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/representation/PartialSymbol.java @@ -14,4 +14,12 @@ public sealed interface PartialSymbol extends AnyPartialSymbol permits Par A defaultValue(); C defaultConcreteValue(); + + static PartialRelation of(String name, int arity) { + return new PartialRelation(name, arity); + } + + static PartialFunction of(String name, int arity, AbstractDomain abstractDomain) { + return new PartialFunction<>(name, arity, abstractDomain); + } } diff --git a/subprojects/store-reasoning/src/test/java/tools/refinery/store/reasoning/lifting/DnfLifterTest.java b/subprojects/store-reasoning/src/test/java/tools/refinery/store/reasoning/lifting/DnfLifterTest.java new file mode 100644 index 00000000..2d089245 --- /dev/null +++ b/subprojects/store-reasoning/src/test/java/tools/refinery/store/reasoning/lifting/DnfLifterTest.java @@ -0,0 +1,384 @@ +/* + * SPDX-FileCopyrightText: 2023 The Refinery Authors + * + * SPDX-License-Identifier: EPL-2.0 + */ +package tools.refinery.store.reasoning.lifting; + +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.view.AnySymbolView; +import tools.refinery.store.query.view.FunctionView; +import tools.refinery.store.query.view.MustView; +import tools.refinery.store.reasoning.ReasoningAdapter; +import tools.refinery.store.reasoning.literal.Concreteness; +import tools.refinery.store.reasoning.literal.ModalConstraint; +import tools.refinery.store.reasoning.literal.Modality; +import tools.refinery.store.reasoning.representation.PartialRelation; +import tools.refinery.store.reasoning.representation.PartialSymbol; +import tools.refinery.store.representation.Symbol; +import tools.refinery.store.representation.TruthValue; + +import java.util.List; + +import static org.hamcrest.MatcherAssert.assertThat; +import static tools.refinery.store.query.literal.Literals.check; +import static tools.refinery.store.query.literal.Literals.not; +import static tools.refinery.store.query.term.int_.IntTerms.*; +import static tools.refinery.store.query.tests.QueryMatchers.structurallyEqualTo; + +class DnfLifterTest { + private static final Symbol friendSymbol = Symbol.of("friend", 2, TruthValue.class, + TruthValue.UNKNOWN); + private static final AnySymbolView friendMustView = new MustView(friendSymbol); + private static final Symbol age = Symbol.of("age", 1, Integer.class); + private static final FunctionView ageView = new FunctionView<>(age); + private static final PartialRelation person = PartialSymbol.of("Person", 1); + private static final PartialRelation friend = PartialSymbol.of("friend", 2); + + private DnfLifter sut; + + @BeforeEach + void beforeEach() { + sut = new DnfLifter(); + } + + @Test + void liftPartialRelationCallTest() { + var input = Query.of("Actual", (builder, p1) -> builder.clause((v1) -> List.of( + friend.call(p1, v1) + ))).getDnf(); + var actual = sut.lift(Modality.MUST, Concreteness.PARTIAL, input); + + var expected = Query.of("Expected", (builder, p1) -> builder.clause((v1) -> List.of( + ModalConstraint.of(Modality.MUST, Concreteness.PARTIAL, friend).call(p1, v1), + ModalConstraint.of(Modality.MUST, Concreteness.PARTIAL, ReasoningAdapter.EXISTS).call(v1) + ))).getDnf(); + + assertThat(actual, structurallyEqualTo(expected)); + } + + @Test + void liftPartialDnfCallTest() { + var called = Query.of("Called", (builder, p1, p2) -> builder.clause( + friend.call(p1, p2), + friend.call(p2, p1) + )); + var input = Query.of("Actual", (builder, p1) -> builder.clause((v1) -> List.of( + called.call(p1, v1) + ))).getDnf(); + var actual = sut.lift(Modality.MUST, Concreteness.PARTIAL, input); + + var expected = Query.of("Expected", (builder, p1) -> builder.clause((v1) -> List.of( + ModalConstraint.of(Modality.MUST, Concreteness.PARTIAL, called.getDnf()).call(p1, v1), + ModalConstraint.of(Modality.MUST, Concreteness.PARTIAL, ReasoningAdapter.EXISTS).call(v1) + ))).getDnf(); + + assertThat(actual, structurallyEqualTo(expected)); + } + + @Test + void liftSymbolViewCallTest() { + var input = Query.of("Actual", (builder, p1) -> builder.clause((v1) -> List.of( + friendMustView.call(p1, v1) + ))).getDnf(); + var actual = sut.lift(Modality.MUST, Concreteness.PARTIAL, input); + + var expected = Query.of("Expected", (builder, p1) -> builder.clause((v1) -> List.of( + friendMustView.call(p1, v1), + ModalConstraint.of(Modality.MUST, Concreteness.PARTIAL, ReasoningAdapter.EXISTS).call(v1) + ))).getDnf(); + + assertThat(actual, structurallyEqualTo(expected)); + } + + @Test + void liftPartialRelationNegativeCallTest() { + var input = Query.of("Actual", (builder, p1) -> builder.clause((v1) -> List.of( + not(friend.call(p1, v1)), + friend.call(v1, p1) + ))).getDnf(); + var actual = sut.lift(Modality.MUST, Concreteness.PARTIAL, input); + + var expected = Query.of("Expected", (builder, p1) -> builder.clause((v1) -> List.of( + not(ModalConstraint.of(Modality.MAY, Concreteness.PARTIAL, friend).call(p1, v1)), + ModalConstraint.of(Modality.MUST, Concreteness.PARTIAL, friend).call(v1, p1), + ModalConstraint.of(Modality.MUST, Concreteness.PARTIAL, ReasoningAdapter.EXISTS).call(v1) + ))).getDnf(); + + assertThat(actual, structurallyEqualTo(expected)); + } + + @Test + void liftPartialRelationQuantifiedNegativeCallTest() { + var input = Query.of("Actual", (builder, p1) -> builder.clause((v1) -> List.of( + person.call(p1), + not(friend.call(p1, v1)) + ))).getDnf(); + var actual = sut.lift(Modality.MAY, Concreteness.PARTIAL, input); + + var helper = Query.of("Helper", (builder, p1, p2) -> builder.clause( + ModalConstraint.of(Modality.MUST, Concreteness.PARTIAL, friend).call(p1, p2), + ModalConstraint.of(Modality.MUST, Concreteness.PARTIAL, ReasoningAdapter.EXISTS).call(p2) + )); + var expected = Query.of("Expected", (builder, p1) -> builder.clause((v1) -> List.of( + ModalConstraint.of(Modality.MAY, Concreteness.PARTIAL, person).call(p1), + not(helper.call(p1, v1)) + ))).getDnf(); + + assertThat(actual, structurallyEqualTo(expected)); + } + + @Test + void liftSymbolViewQuantifiedNegativeCallTest() { + var input = Query.of("Actual", (builder, p1) -> builder.clause((v1) -> List.of( + person.call(p1), + not(friendMustView.call(p1, v1)) + ))).getDnf(); + var actual = sut.lift(Modality.MAY, Concreteness.PARTIAL, input); + + var helper = Query.of("Helper", (builder, p1, p2) -> builder.clause( + friendMustView.call(p1, p2), + ModalConstraint.of(Modality.MUST, Concreteness.PARTIAL, ReasoningAdapter.EXISTS).call(p2) + )); + var expected = Query.of("Expected", (builder, p1) -> builder.clause((v1) -> List.of( + ModalConstraint.of(Modality.MAY, Concreteness.PARTIAL, person).call(p1), + not(helper.call(p1, v1)) + ))).getDnf(); + + assertThat(actual, structurallyEqualTo(expected)); + } + + @Test + void liftPartialRelationQuantifiedNegativeDiagonalCallTest() { + var input = Query.of("Actual", (builder) -> builder.clause((v1) -> List.of( + not(friend.call(v1, v1)) + ))).getDnf(); + var actual = sut.lift(Modality.MAY, Concreteness.PARTIAL, input); + + var helper = Query.of("Helper", (builder, p1) -> builder.clause( + ModalConstraint.of(Modality.MUST, Concreteness.PARTIAL, friend).call(p1, p1), + ModalConstraint.of(Modality.MUST, Concreteness.PARTIAL, ReasoningAdapter.EXISTS).call(p1) + )); + var expected = Query.of("Expected", (builder) -> builder.clause((v1) -> List.of( + not(helper.call(v1)) + ))).getDnf(); + + assertThat(actual, structurallyEqualTo(expected)); + } + + @Test + void liftPartialDnfQuantifiedNegativeInputCallTest() { + var called = Dnf.of("Called", builder -> { + var p1 = builder.parameter("p1", ParameterDirection.IN); + var p2 = builder.parameter("p2", ParameterDirection.OUT); + builder.clause( + friend.call(p1, p2), + friend.call(p2, p1) + ); + }); + var input = Query.of("Actual", (builder, p1) -> builder.clause((v1) -> List.of( + person.call(p1), + not(called.call(p1, v1)) + ))).getDnf(); + var actual = sut.lift(Modality.MAY, Concreteness.PARTIAL, input); + + var helper = Dnf.of("Helper", builder -> { + var p1 = builder.parameter("p1", ParameterDirection.IN); + var p2 = builder.parameter("p2", ParameterDirection.OUT); + builder.clause( + ModalConstraint.of(Modality.MUST, Concreteness.PARTIAL, called).call(p1, p2), + ModalConstraint.of(Modality.MUST, Concreteness.PARTIAL, ReasoningAdapter.EXISTS).call(p2) + ); + }); + var expected = Query.of("Expected", (builder, p1) -> builder.clause((v1) -> List.of( + ModalConstraint.of(Modality.MAY, Concreteness.PARTIAL, person).call(p1), + not(helper.call(p1, v1)) + ))).getDnf(); + + assertThat(actual, structurallyEqualTo(expected)); + } + + @Test + void liftPartialRelationTransitiveCallTest() { + var input = Query.of("Actual", (builder, p1, p2)-> builder.clause( + friend.callTransitive(p1, p2), + not(person.call(p2)) + )).getDnf(); + var actual = sut.lift(Modality.MAY, Concreteness.PARTIAL, input); + + var helper = Query.of("Helper", (builder, p1, p2) -> builder.clause( + ModalConstraint.of(Modality.MAY, Concreteness.PARTIAL, friend).call(p1, p2), + ModalConstraint.of(Modality.MAY, Concreteness.PARTIAL, ReasoningAdapter.EXISTS).call(p2) + )); + var helper2 = Query.of("Helper2", (builder, p1, p2) -> { + builder.clause( + ModalConstraint.of(Modality.MAY, Concreteness.PARTIAL, friend).call(p1, p2) + ); + builder.clause((v1) -> List.of( + helper.callTransitive(p1, v1), + ModalConstraint.of(Modality.MAY, Concreteness.PARTIAL, friend).call(v1, p2) + )); + }); + var expected = Query.of("Expected", (builder, p1, p2) -> builder.clause( + helper2.call(p1, p2), + not(ModalConstraint.of(Modality.MUST, Concreteness.PARTIAL, person).call(p2)) + )).getDnf(); + + assertThat(actual, structurallyEqualTo(expected)); + } + + @Test + void liftPartialSymbolTransitiveCallTest() { + var input = Query.of("Actual", (builder, p1, p2)-> builder.clause( + friendMustView.callTransitive(p1, p2), + not(person.call(p2)) + )).getDnf(); + var actual = sut.lift(Modality.MAY, Concreteness.PARTIAL, input); + + var helper = Query.of("Helper", (builder, p1, p2) -> builder.clause( + friendMustView.call(p1, p2), + ModalConstraint.of(Modality.MAY, Concreteness.PARTIAL, ReasoningAdapter.EXISTS).call(p2) + )); + var helper2 = Query.of("Helper2", (builder, p1, p2) -> { + builder.clause( + friendMustView.call(p1, p2) + ); + builder.clause((v1) -> List.of( + helper.callTransitive(p1, v1), + friendMustView.call(v1, p2) + )); + }); + var expected = Query.of("Expected", (builder, p1, p2) -> builder.clause( + helper2.call(p1, p2), + not(ModalConstraint.of(Modality.MUST, Concreteness.PARTIAL, person).call(p2)) + )).getDnf(); + + assertThat(actual, structurallyEqualTo(expected)); + } + + @Test + void liftPartialRelationTransitiveCallExistsTest() { + var input = Query.of("Actual", (builder, p1) -> builder.clause((v1) -> List.of( + friend.callTransitive(p1, v1), + not(person.call(v1)) + ))).getDnf(); + var actual = sut.lift(Modality.MAY, Concreteness.PARTIAL, input); + + var helper = Query.of("Helper", (builder, p1, p2) -> builder.clause( + ModalConstraint.of(Modality.MAY, Concreteness.PARTIAL, friend).call(p1, p2), + ModalConstraint.of(Modality.MAY, Concreteness.PARTIAL, ReasoningAdapter.EXISTS).call(p2) + )); + var helper2 = Query.of("Helper2", (builder, p1, p2) -> { + builder.clause( + ModalConstraint.of(Modality.MAY, Concreteness.PARTIAL, friend).call(p1, p2) + ); + builder.clause((v1) -> List.of( + helper.callTransitive(p1, v1), + ModalConstraint.of(Modality.MAY, Concreteness.PARTIAL, friend).call(v1, p2) + )); + }); + // Possible optimization: +// var expected = Query.of("Expected", (builder, p1) -> builder.clause((v1) -> List.of( +// helper.callTransitive(p1, v1), +// not(ModalConstraint.of(Modality.MUST, Concreteness.PARTIAL, person).call(v1)), +// ))).getDnf(); + var expected = Query.of("Expected", (builder, p1) -> builder.clause((v1) -> List.of( + helper2.call(p1, v1), + not(ModalConstraint.of(Modality.MUST, Concreteness.PARTIAL, person).call(v1)), + ModalConstraint.of(Modality.MAY, Concreteness.PARTIAL, ReasoningAdapter.EXISTS).call(v1) + ))).getDnf(); + + assertThat(actual, structurallyEqualTo(expected)); + } + + @Test + void liftEquivalentTest() { + var input = Query.of("Actual", (builder, p1, p2) -> builder.clause( + p1.isEquivalent(p2), + person.call(p1) + )).getDnf(); + var actual = sut.lift(Modality.MAY, Concreteness.PARTIAL, input); + + var expected = Query.of("Expected", (builder, p1, p2) -> builder.clause( + ModalConstraint.of(Modality.MAY, Concreteness.PARTIAL, person).call(p1), + ModalConstraint.of(Modality.MAY, Concreteness.PARTIAL, ReasoningAdapter.EQUALS).call(p2, p1) + )).getDnf(); + + assertThat(actual, structurallyEqualTo(expected)); + } + + @Test + void liftNotEquivalentTest() { + var input = Query.of("Actual", (builder, p1, p2) -> builder.clause( + not(p1.isEquivalent(p2)), + friend.call(p1, p2) + )).getDnf(); + var actual = sut.lift(Modality.MAY, Concreteness.PARTIAL, input); + + var expected = Query.of("Expected", (builder, p1, p2) -> builder.clause( + ModalConstraint.of(Modality.MAY, Concreteness.PARTIAL, friend).call(p1, p2), + not(ModalConstraint.of(Modality.MUST, Concreteness.PARTIAL, ReasoningAdapter.EQUALS).call(p1, p2)) + )).getDnf(); + + assertThat(actual, structurallyEqualTo(expected)); + } + + @Test + void liftConstantTest() { + var input = Query.of("Actual", (builder, p1) -> builder.clause((v1) -> List.of( + v1.isConstant(0), + friend.call(v1, p1) + ))).getDnf(); + var actual = sut.lift(Modality.MAY, Concreteness.PARTIAL, input); + + var expected = Query.of("Expected", (builder, p1) -> builder.clause((v1) -> List.of( + v1.isConstant(0), + ModalConstraint.of(Modality.MAY, Concreteness.PARTIAL, friend).call(v1, p1), + ModalConstraint.of(Modality.MAY, Concreteness.PARTIAL, ReasoningAdapter.EXISTS).call(v1) + ))).getDnf(); + + assertThat(actual, structurallyEqualTo(expected)); + } + + @Test + void liftAssignTest() { + var input = Query.of("Actual", Integer.class, (builder, p1, output) -> builder + .clause(Integer.class, (d1) -> List.of( + person.call(p1), + ageView.call(p1, d1), + output.assign(mul(constant(2), d1)) + ))).getDnf(); + var actual = sut.lift(Modality.MAY, Concreteness.PARTIAL, input); + + var expected = Query.of("Expected", Integer.class, (builder, p1, output) -> builder + .clause(Integer.class, (d1) -> List.of( + ModalConstraint.of(Modality.MAY, Concreteness.PARTIAL, person).call(p1), + ageView.call(p1, d1), + output.assign(mul(constant(2), d1)) + ))).getDnf(); + + assertThat(actual, structurallyEqualTo(expected)); + } + + @Test + void liftCheckTest() { + var input = Query.of("Actual", (builder, p1) -> builder.clause(Integer.class, (d1) -> List.of( + person.call(p1), + ageView.call(p1, d1), + check(greaterEq(d1, constant(21))) + ))).getDnf(); + var actual = sut.lift(Modality.MAY, Concreteness.CANDIDATE, input); + + var expected = Query.of("Expected", (builder, p1) -> builder.clause(Integer.class, (d1) -> List.of( + ModalConstraint.of(Modality.MAY, Concreteness.CANDIDATE, person).call(p1), + ageView.call(p1, d1), + check(greaterEq(d1, constant(21))) + ))).getDnf(); + + assertThat(actual, structurallyEqualTo(expected)); + } +} -- cgit v1.2.3-70-g09d2