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. --- .../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 + 8 files changed, 201 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 (limited to 'subprojects/store-reasoning/src/main') 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); + } } -- cgit v1.2.3-54-g00ecf