diff options
Diffstat (limited to 'subprojects/store-reasoning/src/main/java/tools')
2 files changed, 186 insertions, 137 deletions
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 @@ | |||
1 | /* | ||
2 | * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/> | ||
3 | * | ||
4 | * SPDX-License-Identifier: EPL-2.0 | ||
5 | */ | ||
6 | package tools.refinery.store.reasoning.lifting; | ||
7 | |||
8 | import tools.refinery.store.query.Constraint; | ||
9 | import tools.refinery.store.query.dnf.Dnf; | ||
10 | import tools.refinery.store.query.dnf.DnfClause; | ||
11 | import tools.refinery.store.query.literal.*; | ||
12 | import tools.refinery.store.query.term.NodeVariable; | ||
13 | import tools.refinery.store.query.term.ParameterDirection; | ||
14 | import tools.refinery.store.query.term.Variable; | ||
15 | import tools.refinery.store.reasoning.ReasoningAdapter; | ||
16 | import tools.refinery.store.reasoning.literal.Concreteness; | ||
17 | import tools.refinery.store.reasoning.literal.ModalConstraint; | ||
18 | import tools.refinery.store.reasoning.literal.Modality; | ||
19 | |||
20 | import java.util.*; | ||
21 | import java.util.stream.Collectors; | ||
22 | |||
23 | class ClauseLifter { | ||
24 | private final Modality modality; | ||
25 | private final Concreteness concreteness; | ||
26 | private final DnfClause clause; | ||
27 | private final Set<NodeVariable> quantifiedVariables; | ||
28 | private final Set<NodeVariable> existentialQuantifiersToAdd; | ||
29 | |||
30 | public ClauseLifter(Modality modality, Concreteness concreteness, Dnf dnf, DnfClause clause) { | ||
31 | this.modality = modality; | ||
32 | this.concreteness = concreteness; | ||
33 | this.clause = clause; | ||
34 | quantifiedVariables = getQuantifiedNodeVariables(dnf, clause); | ||
35 | existentialQuantifiersToAdd = new LinkedHashSet<>(quantifiedVariables); | ||
36 | } | ||
37 | |||
38 | private static Set<NodeVariable> getQuantifiedNodeVariables(Dnf dnf, DnfClause clause) { | ||
39 | var quantifiedVariables = clause.positiveVariables().stream() | ||
40 | .filter(Variable::isNodeVariable) | ||
41 | .map(Variable::asNodeVariable) | ||
42 | .collect(Collectors.toCollection(LinkedHashSet::new)); | ||
43 | for (var symbolicParameter : dnf.getSymbolicParameters()) { | ||
44 | if (symbolicParameter.getVariable() instanceof NodeVariable nodeParameter) { | ||
45 | quantifiedVariables.remove(nodeParameter); | ||
46 | } | ||
47 | } | ||
48 | return Collections.unmodifiableSet(quantifiedVariables); | ||
49 | } | ||
50 | |||
51 | public List<Literal> liftClause() { | ||
52 | var liftedLiterals = new ArrayList<Literal>(); | ||
53 | for (var literal : clause.literals()) { | ||
54 | var liftedLiteral = liftLiteral(literal); | ||
55 | liftedLiterals.add(liftedLiteral); | ||
56 | } | ||
57 | var existsConstraint = ModalConstraint.of(modality, concreteness, ReasoningAdapter.EXISTS); | ||
58 | for (var quantifiedVariable : existentialQuantifiersToAdd) { | ||
59 | liftedLiterals.add(existsConstraint.call(quantifiedVariable)); | ||
60 | } | ||
61 | return liftedLiterals; | ||
62 | } | ||
63 | |||
64 | private Literal liftLiteral(Literal literal) { | ||
65 | if (literal instanceof CallLiteral callLiteral) { | ||
66 | return liftCallLiteral(callLiteral); | ||
67 | } else if (literal instanceof EquivalenceLiteral equivalenceLiteral) { | ||
68 | return liftEquivalenceLiteral(equivalenceLiteral); | ||
69 | } else if (literal instanceof ConstantLiteral || | ||
70 | literal instanceof AssignLiteral<?> || | ||
71 | literal instanceof CheckLiteral) { | ||
72 | return literal; | ||
73 | } else if (literal instanceof CountLiteral) { | ||
74 | throw new IllegalArgumentException("Count literal %s cannot be lifted".formatted(literal)); | ||
75 | } else if (literal instanceof AggregationLiteral<?,?>) { | ||
76 | throw new IllegalArgumentException("Aggregation literal %s cannot be lifted".formatted(literal)); | ||
77 | } else { | ||
78 | throw new IllegalArgumentException("Unknown literal to lift: " + literal); | ||
79 | } | ||
80 | } | ||
81 | |||
82 | private Literal liftCallLiteral(CallLiteral callLiteral) { | ||
83 | var polarity = callLiteral.getPolarity(); | ||
84 | return switch (polarity) { | ||
85 | case POSITIVE -> { | ||
86 | Constraint target = callLiteral.getTarget(); | ||
87 | var arguments = callLiteral.getArguments(); | ||
88 | yield ModalConstraint.of(modality, concreteness, target).call(CallPolarity.POSITIVE, arguments); | ||
89 | } | ||
90 | case NEGATIVE -> callNegationHelper(callLiteral); | ||
91 | case TRANSITIVE -> callTransitiveHelper(callLiteral); | ||
92 | }; | ||
93 | } | ||
94 | |||
95 | private Literal callNegationHelper(CallLiteral callLiteral) { | ||
96 | var target = callLiteral.getTarget(); | ||
97 | var originalArguments = callLiteral.getArguments(); | ||
98 | var negatedModality = modality.negate(); | ||
99 | var privateVariables = callLiteral.getPrivateVariables(clause.positiveVariables()); | ||
100 | if (privateVariables.isEmpty()) { | ||
101 | // If there is no universal quantification, we may directly call the original Dnf. | ||
102 | return ModalConstraint.of(negatedModality, concreteness, target) | ||
103 | .call(CallPolarity.NEGATIVE, originalArguments); | ||
104 | } | ||
105 | |||
106 | var builder = Dnf.builder("%s#negation#%s#%s#%s" | ||
107 | .formatted(target.name(), modality, concreteness, privateVariables)); | ||
108 | var uniqueOriginalArguments = List.copyOf(new LinkedHashSet<>(originalArguments)); | ||
109 | |||
110 | var alwaysInputVariables = callLiteral.getInputVariables(Set.of()); | ||
111 | for (var variable : uniqueOriginalArguments) { | ||
112 | var direction = alwaysInputVariables.contains(variable) ? ParameterDirection.IN : ParameterDirection.OUT; | ||
113 | builder.parameter(variable, direction); | ||
114 | } | ||
115 | |||
116 | var literals = new ArrayList<Literal>(); | ||
117 | var liftedConstraint = ModalConstraint.of(negatedModality, concreteness, target); | ||
118 | literals.add(liftedConstraint.call(CallPolarity.POSITIVE, originalArguments)); | ||
119 | |||
120 | var existsConstraint = ModalConstraint.of(negatedModality, concreteness, ReasoningAdapter.EXISTS); | ||
121 | for (var variable : uniqueOriginalArguments) { | ||
122 | if (privateVariables.contains(variable)) { | ||
123 | literals.add(existsConstraint.call(variable)); | ||
124 | } | ||
125 | } | ||
126 | |||
127 | builder.clause(literals); | ||
128 | var liftedTarget = builder.build(); | ||
129 | return liftedTarget.call(CallPolarity.NEGATIVE, uniqueOriginalArguments); | ||
130 | } | ||
131 | |||
132 | private Literal callTransitiveHelper(CallLiteral callLiteral) { | ||
133 | var target = callLiteral.getTarget(); | ||
134 | var originalArguments = callLiteral.getArguments(); | ||
135 | var liftedTarget = ModalConstraint.of(modality, concreteness, target); | ||
136 | |||
137 | var existsConstraint = ModalConstraint.of(modality, concreteness, ReasoningAdapter.EXISTS); | ||
138 | var existingEndHelperName = "%s#exisitingEnd#%s#%s".formatted(target.name(), modality, concreteness); | ||
139 | var existingEndHelper = Dnf.of(existingEndHelperName, builder -> { | ||
140 | var start = builder.parameter("start"); | ||
141 | var end = builder.parameter("end"); | ||
142 | builder.clause( | ||
143 | liftedTarget.call(start, end), | ||
144 | existsConstraint.call(end) | ||
145 | ); | ||
146 | }); | ||
147 | |||
148 | // The start and end of a transitive path is always a node. | ||
149 | var pathEnd = (NodeVariable) originalArguments.get(1); | ||
150 | if (quantifiedVariables.contains(pathEnd)) { | ||
151 | // The end of the path needs existential quantification anyway, so we don't need a second helper. | ||
152 | // We replace the call to EXISTS with the transitive path call. | ||
153 | existentialQuantifiersToAdd.remove(pathEnd); | ||
154 | return existingEndHelper.call(CallPolarity.TRANSITIVE, originalArguments); | ||
155 | } | ||
156 | |||
157 | var transitiveHelperName = "%s#transitive#%s#%s".formatted(target.name(), modality, concreteness); | ||
158 | var transitiveHelper = Dnf.of(transitiveHelperName, builder -> { | ||
159 | var start = builder.parameter("start"); | ||
160 | var end = builder.parameter("end"); | ||
161 | // Make sure the end of the path is not existentially quantified. | ||
162 | builder.clause(liftedTarget.call(start, end)); | ||
163 | builder.clause(middle -> List.of( | ||
164 | existingEndHelper.callTransitive(start, middle), | ||
165 | liftedTarget.call(middle, end) | ||
166 | )); | ||
167 | }); | ||
168 | |||
169 | return transitiveHelper.call(CallPolarity.POSITIVE, originalArguments); | ||
170 | } | ||
171 | |||
172 | private Literal liftEquivalenceLiteral(EquivalenceLiteral equivalenceLiteral) { | ||
173 | if (equivalenceLiteral.isPositive()) { | ||
174 | return ModalConstraint.of(modality, concreteness, ReasoningAdapter.EQUALS) | ||
175 | .call(CallPolarity.POSITIVE, equivalenceLiteral.getLeft(), equivalenceLiteral.getRight()); | ||
176 | } | ||
177 | return ModalConstraint.of(modality.negate(), concreteness, ReasoningAdapter.EQUALS) | ||
178 | .call(CallPolarity.NEGATIVE, equivalenceLiteral.getLeft(), equivalenceLiteral.getRight()); | ||
179 | } | ||
180 | } | ||
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 @@ | |||
5 | */ | 5 | */ |
6 | package tools.refinery.store.reasoning.lifting; | 6 | package tools.refinery.store.reasoning.lifting; |
7 | 7 | ||
8 | import tools.refinery.store.query.Constraint; | ||
9 | import tools.refinery.store.query.dnf.Dnf; | 8 | import tools.refinery.store.query.dnf.Dnf; |
10 | import tools.refinery.store.query.dnf.DnfClause; | 9 | import tools.refinery.store.query.dnf.DnfClause; |
11 | import tools.refinery.store.query.equality.DnfEqualityChecker; | 10 | import tools.refinery.store.query.equality.DnfEqualityChecker; |
12 | import tools.refinery.store.query.literal.*; | 11 | import tools.refinery.store.query.literal.Literal; |
13 | import tools.refinery.store.query.term.NodeVariable; | ||
14 | import tools.refinery.store.query.term.ParameterDirection; | ||
15 | import tools.refinery.store.query.term.Variable; | ||
16 | import tools.refinery.store.reasoning.ReasoningAdapter; | ||
17 | import tools.refinery.store.reasoning.literal.Concreteness; | 12 | import tools.refinery.store.reasoning.literal.Concreteness; |
18 | import tools.refinery.store.reasoning.literal.ModalConstraint; | ||
19 | import tools.refinery.store.reasoning.literal.Modality; | 13 | import tools.refinery.store.reasoning.literal.Modality; |
20 | 14 | ||
21 | import java.util.*; | 15 | import java.util.HashMap; |
22 | import java.util.stream.Collectors; | 16 | import java.util.List; |
17 | import java.util.Map; | ||
23 | 18 | ||
24 | public class DnfLifter { | 19 | public class DnfLifter { |
25 | private final Map<ModalDnf, Dnf> cache = new HashMap<>(); | 20 | private final Map<ModalDnf, Dnf> cache = new HashMap<>(); |
@@ -46,134 +41,8 @@ public class DnfLifter { | |||
46 | } | 41 | } |
47 | 42 | ||
48 | private List<Literal> liftClause(Modality modality, Concreteness concreteness, Dnf dnf, DnfClause clause) { | 43 | private List<Literal> liftClause(Modality modality, Concreteness concreteness, Dnf dnf, DnfClause clause) { |
49 | var liftedLiterals = new ArrayList<Literal>(); | 44 | var lifter = new ClauseLifter(modality, concreteness, dnf, clause); |
50 | for (var literal : clause.literals()) { | 45 | return lifter.liftClause(); |
51 | var liftedLiteral = liftLiteral(modality, concreteness, clause, literal); | ||
52 | liftedLiterals.add(liftedLiteral); | ||
53 | } | ||
54 | var quantifiedVariables = getQuantifiedNodeVariables(dnf, clause); | ||
55 | var existsConstraint = ModalConstraint.of(modality, concreteness, ReasoningAdapter.EXISTS); | ||
56 | for (var quantifiedVariable : quantifiedVariables) { | ||
57 | liftedLiterals.add(existsConstraint.call(quantifiedVariable)); | ||
58 | } | ||
59 | return liftedLiterals; | ||
60 | } | ||
61 | |||
62 | private Literal liftLiteral(Modality modality, Concreteness concreteness, DnfClause clause, Literal literal) { | ||
63 | if (literal instanceof CallLiteral callLiteral) { | ||
64 | return liftCallLiteral(modality, concreteness, clause, callLiteral); | ||
65 | } else if (literal instanceof EquivalenceLiteral equivalenceLiteral) { | ||
66 | return liftEquivalenceLiteral(modality, concreteness, equivalenceLiteral); | ||
67 | } else if (literal instanceof ConstantLiteral || | ||
68 | literal instanceof AssignLiteral<?> || | ||
69 | literal instanceof CheckLiteral) { | ||
70 | return literal; | ||
71 | } else if (literal instanceof CountLiteral) { | ||
72 | throw new IllegalArgumentException("Count literal %s cannot be lifted".formatted(literal)); | ||
73 | } else if (literal instanceof AggregationLiteral<?,?>) { | ||
74 | throw new IllegalArgumentException("Aggregation literal %s cannot be lifted".formatted(literal)); | ||
75 | } else { | ||
76 | throw new IllegalArgumentException("Unknown literal to lift: " + literal); | ||
77 | } | ||
78 | } | ||
79 | |||
80 | private Literal liftCallLiteral(Modality modality, Concreteness concreteness, DnfClause clause, | ||
81 | CallLiteral callLiteral) { | ||
82 | Constraint target = callLiteral.getTarget(); | ||
83 | var polarity = callLiteral.getPolarity(); | ||
84 | var arguments = callLiteral.getArguments(); | ||
85 | return switch (polarity) { | ||
86 | case POSITIVE -> ModalConstraint.of(modality, concreteness, target).call( | ||
87 | CallPolarity.POSITIVE, arguments); | ||
88 | case NEGATIVE -> { | ||
89 | var callModality = modality.negate(); | ||
90 | boolean needsHelper = !polarity.isPositive() && | ||
91 | !callLiteral.getPrivateVariables(clause.positiveVariables()).isEmpty(); | ||
92 | if (needsHelper) { | ||
93 | yield callNegationHelper(callModality, concreteness, clause, callLiteral, target); | ||
94 | } | ||
95 | yield ModalConstraint.of(callModality, concreteness, target).call( | ||
96 | CallPolarity.NEGATIVE, arguments); | ||
97 | } | ||
98 | case TRANSITIVE -> createTransitiveHelper(modality, concreteness, target).call( | ||
99 | CallPolarity.POSITIVE, arguments); | ||
100 | }; | ||
101 | } | ||
102 | |||
103 | private Literal callNegationHelper(Modality modality, Concreteness concreteness, DnfClause clause, | ||
104 | CallLiteral callLiteral, Constraint target) { | ||
105 | var builder = Dnf.builder(); | ||
106 | var originalArguments = callLiteral.getArguments(); | ||
107 | var uniqueOriginalArguments = List.copyOf(new LinkedHashSet<>(originalArguments)); | ||
108 | |||
109 | var alwaysInputVariables = callLiteral.getInputVariables(Set.of()); | ||
110 | for (var variable : uniqueOriginalArguments) { | ||
111 | var direction = alwaysInputVariables.contains(variable) ? ParameterDirection.IN : ParameterDirection.OUT; | ||
112 | builder.parameter(variable, direction); | ||
113 | } | ||
114 | |||
115 | var literals = new ArrayList<Literal>(); | ||
116 | var liftedConstraint = ModalConstraint.of(modality, concreteness, target); | ||
117 | literals.add(liftedConstraint.call(CallPolarity.POSITIVE, originalArguments)); | ||
118 | |||
119 | var privateVariables = callLiteral.getPrivateVariables(clause.positiveVariables()); | ||
120 | var existsConstraint = ModalConstraint.of(modality, concreteness, ReasoningAdapter.EXISTS); | ||
121 | for (var variable : uniqueOriginalArguments) { | ||
122 | if (privateVariables.contains(variable)) { | ||
123 | literals.add(existsConstraint.call(variable)); | ||
124 | } | ||
125 | } | ||
126 | |||
127 | builder.clause(literals); | ||
128 | var liftedTarget = builder.build(); | ||
129 | return liftedTarget.call(CallPolarity.NEGATIVE, uniqueOriginalArguments); | ||
130 | } | ||
131 | |||
132 | private Dnf createTransitiveHelper(Modality modality, Concreteness concreteness, Constraint target) { | ||
133 | var liftedTarget = ModalConstraint.of(modality, concreteness, target); | ||
134 | var existsConstraint = ModalConstraint.of(modality, concreteness, ReasoningAdapter.EXISTS); | ||
135 | var existingEndHelperName = "%s#exisitingEnd#%s#%s".formatted(target.name(), modality, concreteness); | ||
136 | var existingEndHelper = Dnf.of(existingEndHelperName, builder -> { | ||
137 | var start = builder.parameter("start"); | ||
138 | var end = builder.parameter("end"); | ||
139 | builder.clause( | ||
140 | liftedTarget.call(start, end), | ||
141 | existsConstraint.call(end) | ||
142 | ); | ||
143 | }); | ||
144 | var transitiveHelperName = "%s#transitive#%s#%s".formatted(target.name(), modality, concreteness); | ||
145 | return Dnf.of(transitiveHelperName, builder -> { | ||
146 | var start = builder.parameter("start"); | ||
147 | var end = builder.parameter("end"); | ||
148 | builder.clause(liftedTarget.call(start, end)); | ||
149 | builder.clause(middle -> List.of( | ||
150 | existingEndHelper.callTransitive(start, middle), | ||
151 | liftedTarget.call(middle, end) | ||
152 | )); | ||
153 | }); | ||
154 | } | ||
155 | |||
156 | private Literal liftEquivalenceLiteral(Modality modality, Concreteness concreteness, | ||
157 | EquivalenceLiteral equivalenceLiteral) { | ||
158 | if (equivalenceLiteral.isPositive()) { | ||
159 | return ModalConstraint.of(modality, concreteness, ReasoningAdapter.EQUALS).call( | ||
160 | CallPolarity.POSITIVE, equivalenceLiteral.getLeft(), equivalenceLiteral.getRight()); | ||
161 | } | ||
162 | return ModalConstraint.of(modality.negate(), concreteness, ReasoningAdapter.EQUALS).call( | ||
163 | CallPolarity.NEGATIVE, equivalenceLiteral.getLeft(), equivalenceLiteral.getRight()); | ||
164 | } | ||
165 | |||
166 | private static Set<NodeVariable> getQuantifiedNodeVariables(Dnf dnf, DnfClause clause) { | ||
167 | var quantifiedVariables = clause.positiveVariables().stream() | ||
168 | .filter(Variable::isNodeVariable) | ||
169 | .map(Variable::asNodeVariable) | ||
170 | .collect(Collectors.toCollection(HashSet::new)); | ||
171 | for (var symbolicParameter : dnf.getSymbolicParameters()) { | ||
172 | if (symbolicParameter.getVariable() instanceof NodeVariable nodeParameter) { | ||
173 | quantifiedVariables.remove(nodeParameter); | ||
174 | } | ||
175 | } | ||
176 | return quantifiedVariables; | ||
177 | } | 46 | } |
178 | 47 | ||
179 | private record ModalDnf(Modality modality, Concreteness concreteness, Dnf dnf) { | 48 | private record ModalDnf(Modality modality, Concreteness concreteness, Dnf dnf) { |