diff options
author | Kristóf Marussy <kristof@marussy.com> | 2023-05-01 02:07:23 +0200 |
---|---|---|
committer | Kristóf Marussy <kristof@marussy.com> | 2023-05-01 02:42:34 +0200 |
commit | 4e698774925468062974b990143c1091e23ed63b (patch) | |
tree | 21f2fc38b6b3b5f3be6ecbdee100d385a2e92c05 /subprojects/store-reasoning/src | |
parent | fix(web): editor cursor styling (diff) | |
download | refinery-4e698774925468062974b990143c1091e23ed63b.tar.gz refinery-4e698774925468062974b990143c1091e23ed63b.tar.zst refinery-4e698774925468062974b990143c1091e23ed63b.zip |
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
Diffstat (limited to 'subprojects/store-reasoning/src')
3 files changed, 24 insertions, 18 deletions
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; | |||
12 | import tools.refinery.store.query.literal.CallLiteral; | 12 | import tools.refinery.store.query.literal.CallLiteral; |
13 | import tools.refinery.store.query.literal.CallPolarity; | 13 | import tools.refinery.store.query.literal.CallPolarity; |
14 | import tools.refinery.store.query.literal.Literal; | 14 | import tools.refinery.store.query.literal.Literal; |
15 | import tools.refinery.store.query.term.DataVariable; | 15 | import tools.refinery.store.query.term.NodeVariable; |
16 | import tools.refinery.store.query.term.Variable; | 16 | import tools.refinery.store.query.term.Variable; |
17 | import tools.refinery.store.reasoning.ReasoningAdapter; | 17 | import tools.refinery.store.reasoning.ReasoningAdapter; |
18 | import tools.refinery.store.reasoning.literal.ModalConstraint; | 18 | import tools.refinery.store.reasoning.literal.ModalConstraint; |
@@ -21,7 +21,7 @@ import tools.refinery.store.reasoning.literal.PartialLiterals; | |||
21 | import tools.refinery.store.util.CycleDetectingMapper; | 21 | import tools.refinery.store.util.CycleDetectingMapper; |
22 | 22 | ||
23 | import java.util.ArrayList; | 23 | import java.util.ArrayList; |
24 | import java.util.HashSet; | 24 | import java.util.LinkedHashSet; |
25 | import java.util.List; | 25 | import java.util.List; |
26 | 26 | ||
27 | public class DnfLifter { | 27 | public class DnfLifter { |
@@ -36,10 +36,10 @@ public class DnfLifter { | |||
36 | var modality = modalDnf.modality(); | 36 | var modality = modalDnf.modality(); |
37 | var dnf = modalDnf.dnf(); | 37 | var dnf = modalDnf.dnf(); |
38 | var builder = Dnf.builder(); | 38 | var builder = Dnf.builder(); |
39 | builder.parameters(dnf.getParameters()); | 39 | builder.symbolicParameters(dnf.getSymbolicParameters()); |
40 | boolean changed = false; | 40 | boolean changed = false; |
41 | for (var clause : dnf.getClauses()) { | 41 | for (var clause : dnf.getClauses()) { |
42 | if (liftClause(modality, clause, builder)) { | 42 | if (liftClause(modality, dnf, clause, builder)) { |
43 | changed = true; | 43 | changed = true; |
44 | } | 44 | } |
45 | } | 45 | } |
@@ -49,12 +49,9 @@ public class DnfLifter { | |||
49 | return dnf; | 49 | return dnf; |
50 | } | 50 | } |
51 | 51 | ||
52 | private boolean liftClause(Modality modality, DnfClause clause, DnfBuilder builder) { | 52 | private boolean liftClause(Modality modality, Dnf originalDnf, DnfClause clause, DnfBuilder builder) { |
53 | boolean changed = false; | 53 | boolean changed = false; |
54 | var quantifiedVariables = new HashSet<>(clause.boundVariables() | 54 | var quantifiedVariables = getQuantifiedDataVariables(originalDnf, clause); |
55 | .stream() | ||
56 | .filter(DataVariable.class::isInstance) | ||
57 | .toList()); | ||
58 | var literals = clause.literals(); | 55 | var literals = clause.literals(); |
59 | var liftedLiterals = new ArrayList<Literal>(literals.size()); | 56 | var liftedLiterals = new ArrayList<Literal>(literals.size()); |
60 | for (var literal : literals) { | 57 | for (var literal : literals) { |
@@ -81,6 +78,16 @@ public class DnfLifter { | |||
81 | return changed || !quantifiedVariables.isEmpty(); | 78 | return changed || !quantifiedVariables.isEmpty(); |
82 | } | 79 | } |
83 | 80 | ||
81 | private static LinkedHashSet<Variable> getQuantifiedDataVariables(Dnf originalDnf, DnfClause clause) { | ||
82 | var quantifiedVariables = new LinkedHashSet<>(clause.positiveVariables()); | ||
83 | for (var symbolicParameter : originalDnf.getSymbolicParameters()) { | ||
84 | // The existence of parameters will be checked outside this DNF. | ||
85 | quantifiedVariables.remove(symbolicParameter.getVariable()); | ||
86 | } | ||
87 | quantifiedVariables.removeIf(variable -> !(variable instanceof NodeVariable)); | ||
88 | return quantifiedVariables; | ||
89 | } | ||
90 | |||
84 | @Nullable | 91 | @Nullable |
85 | private Variable isExistsLiteralForVariable(Modality modality, Literal literal) { | 92 | private Variable isExistsLiteralForVariable(Modality modality, Literal literal) { |
86 | if (literal instanceof CallLiteral callLiteral && | 93 | 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; | |||
8 | import tools.refinery.store.query.Constraint; | 8 | import tools.refinery.store.query.Constraint; |
9 | import tools.refinery.store.query.equality.LiteralEqualityHelper; | 9 | import tools.refinery.store.query.equality.LiteralEqualityHelper; |
10 | import tools.refinery.store.query.literal.LiteralReduction; | 10 | import tools.refinery.store.query.literal.LiteralReduction; |
11 | import tools.refinery.store.query.term.Sort; | 11 | import tools.refinery.store.query.term.Parameter; |
12 | 12 | ||
13 | import java.util.List; | 13 | import java.util.List; |
14 | 14 | ||
@@ -21,8 +21,8 @@ public record ModalConstraint(Modality modality, Constraint constraint) implemen | |||
21 | } | 21 | } |
22 | 22 | ||
23 | @Override | 23 | @Override |
24 | public List<Sort> getSorts() { | 24 | public List<Parameter> getParameters() { |
25 | return constraint.getSorts(); | 25 | return constraint.getParameters(); |
26 | } | 26 | } |
27 | 27 | ||
28 | @Override | 28 | @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 @@ | |||
6 | package tools.refinery.store.reasoning.representation; | 6 | package tools.refinery.store.reasoning.representation; |
7 | 7 | ||
8 | import tools.refinery.store.query.Constraint; | 8 | import tools.refinery.store.query.Constraint; |
9 | import tools.refinery.store.query.term.NodeSort; | 9 | import tools.refinery.store.query.term.Parameter; |
10 | import tools.refinery.store.query.term.Sort; | ||
11 | import tools.refinery.store.representation.AbstractDomain; | 10 | import tools.refinery.store.representation.AbstractDomain; |
12 | import tools.refinery.store.representation.TruthValue; | 11 | import tools.refinery.store.representation.TruthValue; |
13 | import tools.refinery.store.representation.TruthValueDomain; | 12 | import tools.refinery.store.representation.TruthValueDomain; |
@@ -32,10 +31,10 @@ public record PartialRelation(String name, int arity) implements PartialSymbol<T | |||
32 | } | 31 | } |
33 | 32 | ||
34 | @Override | 33 | @Override |
35 | public List<Sort> getSorts() { | 34 | public List<Parameter> getParameters() { |
36 | var sorts = new Sort[arity()]; | 35 | var parameters = new Parameter[arity]; |
37 | Arrays.fill(sorts, NodeSort.INSTANCE); | 36 | Arrays.fill(parameters, Parameter.NODE_IN_OUT); |
38 | return List.of(sorts); | 37 | return List.of(parameters); |
39 | } | 38 | } |
40 | 39 | ||
41 | @Override | 40 | @Override |