From 4e698774925468062974b990143c1091e23ed63b Mon Sep 17 00:00:00 2001 From: Kristóf Marussy Date: Mon, 1 May 2023 02:07:23 +0200 Subject: feat: query parameter binding validation * Introduce parameter directions for constraints and DNF * Introduce variable directions for literals * Infer and check variable directions in DNF and topologically sort literals by their input variables --- .../store/reasoning/lifting/DnfLifter.java | 25 ++++++++++++++-------- .../store/reasoning/literal/ModalConstraint.java | 6 +++--- .../reasoning/representation/PartialRelation.java | 11 +++++----- 3 files changed, 24 insertions(+), 18 deletions(-) (limited to 'subprojects/store-reasoning/src/main') 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 594005f1..ac41d170 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 @@ -12,7 +12,7 @@ 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.term.DataVariable; +import tools.refinery.store.query.term.NodeVariable; import tools.refinery.store.query.term.Variable; import tools.refinery.store.reasoning.ReasoningAdapter; import tools.refinery.store.reasoning.literal.ModalConstraint; @@ -21,7 +21,7 @@ import tools.refinery.store.reasoning.literal.PartialLiterals; import tools.refinery.store.util.CycleDetectingMapper; import java.util.ArrayList; -import java.util.HashSet; +import java.util.LinkedHashSet; import java.util.List; public class DnfLifter { @@ -36,10 +36,10 @@ public class DnfLifter { var modality = modalDnf.modality(); var dnf = modalDnf.dnf(); var builder = Dnf.builder(); - builder.parameters(dnf.getParameters()); + builder.symbolicParameters(dnf.getSymbolicParameters()); boolean changed = false; for (var clause : dnf.getClauses()) { - if (liftClause(modality, clause, builder)) { + if (liftClause(modality, dnf, clause, builder)) { changed = true; } } @@ -49,12 +49,9 @@ public class DnfLifter { return dnf; } - private boolean liftClause(Modality modality, DnfClause clause, DnfBuilder builder) { + private boolean liftClause(Modality modality, Dnf originalDnf, DnfClause clause, DnfBuilder builder) { boolean changed = false; - var quantifiedVariables = new HashSet<>(clause.boundVariables() - .stream() - .filter(DataVariable.class::isInstance) - .toList()); + var quantifiedVariables = getQuantifiedDataVariables(originalDnf, clause); var literals = clause.literals(); var liftedLiterals = new ArrayList(literals.size()); for (var literal : literals) { @@ -81,6 +78,16 @@ public class DnfLifter { return changed || !quantifiedVariables.isEmpty(); } + 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()); + } + quantifiedVariables.removeIf(variable -> !(variable instanceof NodeVariable)); + return quantifiedVariables; + } + @Nullable private Variable isExistsLiteralForVariable(Modality modality, Literal literal) { if (literal instanceof CallLiteral callLiteral && 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 7fa98104..ce557d82 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 @@ -8,7 +8,7 @@ package tools.refinery.store.reasoning.literal; import tools.refinery.store.query.Constraint; import tools.refinery.store.query.equality.LiteralEqualityHelper; import tools.refinery.store.query.literal.LiteralReduction; -import tools.refinery.store.query.term.Sort; +import tools.refinery.store.query.term.Parameter; import java.util.List; @@ -21,8 +21,8 @@ public record ModalConstraint(Modality modality, Constraint constraint) implemen } @Override - public List getSorts() { - return constraint.getSorts(); + public List getParameters() { + return constraint.getParameters(); } @Override diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/representation/PartialRelation.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/representation/PartialRelation.java index fc3dc074..1f74ce38 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/representation/PartialRelation.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/representation/PartialRelation.java @@ -6,8 +6,7 @@ package tools.refinery.store.reasoning.representation; import tools.refinery.store.query.Constraint; -import tools.refinery.store.query.term.NodeSort; -import tools.refinery.store.query.term.Sort; +import tools.refinery.store.query.term.Parameter; import tools.refinery.store.representation.AbstractDomain; import tools.refinery.store.representation.TruthValue; import tools.refinery.store.representation.TruthValueDomain; @@ -32,10 +31,10 @@ public record PartialRelation(String name, int arity) implements PartialSymbol getSorts() { - var sorts = new Sort[arity()]; - Arrays.fill(sorts, NodeSort.INSTANCE); - return List.of(sorts); + public List getParameters() { + var parameters = new Parameter[arity]; + Arrays.fill(parameters, Parameter.NODE_IN_OUT); + return List.of(parameters); } @Override -- cgit v1.2.3-54-g00ecf