From 60667ddcfa9faba3845bd73a9f632dfa447d669b Mon Sep 17 00:00:00 2001 From: Kristóf Marussy Date: Mon, 26 Jun 2023 21:32:01 +0200 Subject: refactor: Dnf lifter * Use method object pattern to simplify code. * Optimize existential quantification in transitive queries. --- .../store/reasoning/lifting/ClauseLifter.java | 180 +++++++++++++++++++++ .../store/reasoning/lifting/DnfLifter.java | 143 +--------------- 2 files changed, 186 insertions(+), 137 deletions(-) create mode 100644 subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/lifting/ClauseLifter.java (limited to 'subprojects/store-reasoning/src/main/java/tools') diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/lifting/ClauseLifter.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/lifting/ClauseLifter.java new file mode 100644 index 00000000..d3b0ace8 --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/lifting/ClauseLifter.java @@ -0,0 +1,180 @@ +/* + * SPDX-FileCopyrightText: 2023 The Refinery Authors + * + * SPDX-License-Identifier: EPL-2.0 + */ +package tools.refinery.store.reasoning.lifting; + +import tools.refinery.store.query.Constraint; +import tools.refinery.store.query.dnf.Dnf; +import tools.refinery.store.query.dnf.DnfClause; +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 java.util.*; +import java.util.stream.Collectors; + +class ClauseLifter { + private final Modality modality; + private final Concreteness concreteness; + private final DnfClause clause; + private final Set quantifiedVariables; + private final Set existentialQuantifiersToAdd; + + public ClauseLifter(Modality modality, Concreteness concreteness, Dnf dnf, DnfClause clause) { + this.modality = modality; + this.concreteness = concreteness; + this.clause = clause; + quantifiedVariables = getQuantifiedNodeVariables(dnf, clause); + existentialQuantifiersToAdd = new LinkedHashSet<>(quantifiedVariables); + } + + private static Set getQuantifiedNodeVariables(Dnf dnf, DnfClause clause) { + var quantifiedVariables = clause.positiveVariables().stream() + .filter(Variable::isNodeVariable) + .map(Variable::asNodeVariable) + .collect(Collectors.toCollection(LinkedHashSet::new)); + for (var symbolicParameter : dnf.getSymbolicParameters()) { + if (symbolicParameter.getVariable() instanceof NodeVariable nodeParameter) { + quantifiedVariables.remove(nodeParameter); + } + } + return Collections.unmodifiableSet(quantifiedVariables); + } + + public List liftClause() { + var liftedLiterals = new ArrayList(); + for (var literal : clause.literals()) { + var liftedLiteral = liftLiteral(literal); + liftedLiterals.add(liftedLiteral); + } + var existsConstraint = ModalConstraint.of(modality, concreteness, ReasoningAdapter.EXISTS); + for (var quantifiedVariable : existentialQuantifiersToAdd) { + liftedLiterals.add(existsConstraint.call(quantifiedVariable)); + } + return liftedLiterals; + } + + private Literal liftLiteral(Literal literal) { + if (literal instanceof CallLiteral callLiteral) { + return liftCallLiteral(callLiteral); + } else if (literal instanceof EquivalenceLiteral equivalenceLiteral) { + return liftEquivalenceLiteral(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); + } + } + + private Literal liftCallLiteral(CallLiteral callLiteral) { + var polarity = callLiteral.getPolarity(); + return switch (polarity) { + case POSITIVE -> { + Constraint target = callLiteral.getTarget(); + var arguments = callLiteral.getArguments(); + yield ModalConstraint.of(modality, concreteness, target).call(CallPolarity.POSITIVE, arguments); + } + case NEGATIVE -> callNegationHelper(callLiteral); + case TRANSITIVE -> callTransitiveHelper(callLiteral); + }; + } + + private Literal callNegationHelper(CallLiteral callLiteral) { + var target = callLiteral.getTarget(); + var originalArguments = callLiteral.getArguments(); + var negatedModality = modality.negate(); + var privateVariables = callLiteral.getPrivateVariables(clause.positiveVariables()); + if (privateVariables.isEmpty()) { + // If there is no universal quantification, we may directly call the original Dnf. + return ModalConstraint.of(negatedModality, concreteness, target) + .call(CallPolarity.NEGATIVE, originalArguments); + } + + var builder = Dnf.builder("%s#negation#%s#%s#%s" + .formatted(target.name(), modality, concreteness, privateVariables)); + 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); + } + + var literals = new ArrayList(); + var liftedConstraint = ModalConstraint.of(negatedModality, concreteness, target); + literals.add(liftedConstraint.call(CallPolarity.POSITIVE, originalArguments)); + + var existsConstraint = ModalConstraint.of(negatedModality, 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); + } + + private Literal callTransitiveHelper(CallLiteral callLiteral) { + var target = callLiteral.getTarget(); + var originalArguments = callLiteral.getArguments(); + 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) + ); + }); + + // The start and end of a transitive path is always a node. + var pathEnd = (NodeVariable) originalArguments.get(1); + if (quantifiedVariables.contains(pathEnd)) { + // The end of the path needs existential quantification anyway, so we don't need a second helper. + // We replace the call to EXISTS with the transitive path call. + existentialQuantifiersToAdd.remove(pathEnd); + return existingEndHelper.call(CallPolarity.TRANSITIVE, originalArguments); + } + + var transitiveHelperName = "%s#transitive#%s#%s".formatted(target.name(), modality, concreteness); + var transitiveHelper = Dnf.of(transitiveHelperName, builder -> { + var start = builder.parameter("start"); + var end = builder.parameter("end"); + // Make sure the end of the path is not existentially quantified. + builder.clause(liftedTarget.call(start, end)); + builder.clause(middle -> List.of( + existingEndHelper.callTransitive(start, middle), + liftedTarget.call(middle, end) + )); + }); + + return transitiveHelper.call(CallPolarity.POSITIVE, originalArguments); + } + + private Literal liftEquivalenceLiteral(EquivalenceLiteral equivalenceLiteral) { + if (equivalenceLiteral.isPositive()) { + return ModalConstraint.of(modality, concreteness, ReasoningAdapter.EQUALS) + .call(CallPolarity.POSITIVE, equivalenceLiteral.getLeft(), equivalenceLiteral.getRight()); + } + return ModalConstraint.of(modality.negate(), concreteness, ReasoningAdapter.EQUALS) + .call(CallPolarity.NEGATIVE, equivalenceLiteral.getLeft(), equivalenceLiteral.getRight()); + } +} 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 8bbb75d1..c3b23b43 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,21 +5,16 @@ */ package tools.refinery.store.reasoning.lifting; -import tools.refinery.store.query.Constraint; import tools.refinery.store.query.dnf.Dnf; import tools.refinery.store.query.dnf.DnfClause; 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.query.literal.Literal; import tools.refinery.store.reasoning.literal.Concreteness; -import tools.refinery.store.reasoning.literal.ModalConstraint; import tools.refinery.store.reasoning.literal.Modality; -import java.util.*; -import java.util.stream.Collectors; +import java.util.HashMap; +import java.util.List; +import java.util.Map; public class DnfLifter { private final Map cache = new HashMap<>(); @@ -46,134 +41,8 @@ public class DnfLifter { } 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 quantifiedVariables = getQuantifiedNodeVariables(dnf, clause); - var existsConstraint = ModalConstraint.of(modality, concreteness, ReasoningAdapter.EXISTS); - for (var quantifiedVariable : quantifiedVariables) { - liftedLiterals.add(existsConstraint.call(quantifiedVariable)); - } - return liftedLiterals; - } - - 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); - } - } - - 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); - } - - 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); - } - - 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()); - } - 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); - } - } - return quantifiedVariables; + var lifter = new ClauseLifter(modality, concreteness, dnf, clause); + return lifter.liftClause(); } private record ModalDnf(Modality modality, Concreteness concreteness, Dnf dnf) { -- cgit v1.2.3-54-g00ecf