aboutsummaryrefslogtreecommitdiffstats
path: root/subprojects/store-reasoning/src
diff options
context:
space:
mode:
authorLibravatar Kristóf Marussy <kristof@marussy.com>2023-06-26 21:32:01 +0200
committerLibravatar Kristóf Marussy <kristof@marussy.com>2023-06-29 02:23:01 +0200
commit60667ddcfa9faba3845bd73a9f632dfa447d669b (patch)
tree96d0d7c4de8c3b6364b9203db2c1005368fde017 /subprojects/store-reasoning/src
parentfeat: Dnf lifting (diff)
downloadrefinery-60667ddcfa9faba3845bd73a9f632dfa447d669b.tar.gz
refinery-60667ddcfa9faba3845bd73a9f632dfa447d669b.tar.zst
refinery-60667ddcfa9faba3845bd73a9f632dfa447d669b.zip
refactor: Dnf lifter
* Use method object pattern to simplify code. * Optimize existential quantification in transitive queries.
Diffstat (limited to 'subprojects/store-reasoning/src')
-rw-r--r--subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/lifting/ClauseLifter.java180
-rw-r--r--subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/lifting/DnfLifter.java143
-rw-r--r--subprojects/store-reasoning/src/test/java/tools/refinery/store/reasoning/lifting/DnfLifterTest.java53
3 files changed, 218 insertions, 158 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 */
6package tools.refinery.store.reasoning.lifting;
7
8import tools.refinery.store.query.Constraint;
9import tools.refinery.store.query.dnf.Dnf;
10import tools.refinery.store.query.dnf.DnfClause;
11import tools.refinery.store.query.literal.*;
12import tools.refinery.store.query.term.NodeVariable;
13import tools.refinery.store.query.term.ParameterDirection;
14import tools.refinery.store.query.term.Variable;
15import tools.refinery.store.reasoning.ReasoningAdapter;
16import tools.refinery.store.reasoning.literal.Concreteness;
17import tools.refinery.store.reasoning.literal.ModalConstraint;
18import tools.refinery.store.reasoning.literal.Modality;
19
20import java.util.*;
21import java.util.stream.Collectors;
22
23class 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 */
6package tools.refinery.store.reasoning.lifting; 6package tools.refinery.store.reasoning.lifting;
7 7
8import tools.refinery.store.query.Constraint;
9import tools.refinery.store.query.dnf.Dnf; 8import tools.refinery.store.query.dnf.Dnf;
10import tools.refinery.store.query.dnf.DnfClause; 9import tools.refinery.store.query.dnf.DnfClause;
11import tools.refinery.store.query.equality.DnfEqualityChecker; 10import tools.refinery.store.query.equality.DnfEqualityChecker;
12import tools.refinery.store.query.literal.*; 11import tools.refinery.store.query.literal.Literal;
13import tools.refinery.store.query.term.NodeVariable;
14import tools.refinery.store.query.term.ParameterDirection;
15import tools.refinery.store.query.term.Variable;
16import tools.refinery.store.reasoning.ReasoningAdapter;
17import tools.refinery.store.reasoning.literal.Concreteness; 12import tools.refinery.store.reasoning.literal.Concreteness;
18import tools.refinery.store.reasoning.literal.ModalConstraint;
19import tools.refinery.store.reasoning.literal.Modality; 13import tools.refinery.store.reasoning.literal.Modality;
20 14
21import java.util.*; 15import java.util.HashMap;
22import java.util.stream.Collectors; 16import java.util.List;
17import java.util.Map;
23 18
24public class DnfLifter { 19public 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) {
diff --git a/subprojects/store-reasoning/src/test/java/tools/refinery/store/reasoning/lifting/DnfLifterTest.java b/subprojects/store-reasoning/src/test/java/tools/refinery/store/reasoning/lifting/DnfLifterTest.java
index 2d089245..ceb9404a 100644
--- a/subprojects/store-reasoning/src/test/java/tools/refinery/store/reasoning/lifting/DnfLifterTest.java
+++ b/subprojects/store-reasoning/src/test/java/tools/refinery/store/reasoning/lifting/DnfLifterTest.java
@@ -239,21 +239,21 @@ class DnfLifterTest {
239 )).getDnf(); 239 )).getDnf();
240 var actual = sut.lift(Modality.MAY, Concreteness.PARTIAL, input); 240 var actual = sut.lift(Modality.MAY, Concreteness.PARTIAL, input);
241 241
242 var helper = Query.of("Helper", (builder, p1, p2) -> builder.clause( 242 var endExistsHelper = Query.of("EndExistsHelper", (builder, p1, p2) -> builder.clause(
243 friendMustView.call(p1, p2), 243 friendMustView.call(p1, p2),
244 ModalConstraint.of(Modality.MAY, Concreteness.PARTIAL, ReasoningAdapter.EXISTS).call(p2) 244 ModalConstraint.of(Modality.MAY, Concreteness.PARTIAL, ReasoningAdapter.EXISTS).call(p2)
245 )); 245 ));
246 var helper2 = Query.of("Helper2", (builder, p1, p2) -> { 246 var transitiveHelper = Query.of("TransitiveHelper", (builder, p1, p2) -> {
247 builder.clause( 247 builder.clause(
248 friendMustView.call(p1, p2) 248 friendMustView.call(p1, p2)
249 ); 249 );
250 builder.clause((v1) -> List.of( 250 builder.clause((v1) -> List.of(
251 helper.callTransitive(p1, v1), 251 endExistsHelper.callTransitive(p1, v1),
252 friendMustView.call(v1, p2) 252 friendMustView.call(v1, p2)
253 )); 253 ));
254 }); 254 });
255 var expected = Query.of("Expected", (builder, p1, p2) -> builder.clause( 255 var expected = Query.of("Expected", (builder, p1, p2) -> builder.clause(
256 helper2.call(p1, p2), 256 transitiveHelper.call(p1, p2),
257 not(ModalConstraint.of(Modality.MUST, Concreteness.PARTIAL, person).call(p2)) 257 not(ModalConstraint.of(Modality.MUST, Concreteness.PARTIAL, person).call(p2))
258 )).getDnf(); 258 )).getDnf();
259 259
@@ -272,24 +272,35 @@ class DnfLifterTest {
272 ModalConstraint.of(Modality.MAY, Concreteness.PARTIAL, friend).call(p1, p2), 272 ModalConstraint.of(Modality.MAY, Concreteness.PARTIAL, friend).call(p1, p2),
273 ModalConstraint.of(Modality.MAY, Concreteness.PARTIAL, ReasoningAdapter.EXISTS).call(p2) 273 ModalConstraint.of(Modality.MAY, Concreteness.PARTIAL, ReasoningAdapter.EXISTS).call(p2)
274 )); 274 ));
275 var helper2 = Query.of("Helper2", (builder, p1, p2) -> {
276 builder.clause(
277 ModalConstraint.of(Modality.MAY, Concreteness.PARTIAL, friend).call(p1, p2)
278 );
279 builder.clause((v1) -> List.of(
280 helper.callTransitive(p1, v1),
281 ModalConstraint.of(Modality.MAY, Concreteness.PARTIAL, friend).call(v1, p2)
282 ));
283 });
284 // Possible optimization:
285// var expected = Query.of("Expected", (builder, p1) -> builder.clause((v1) -> List.of(
286// helper.callTransitive(p1, v1),
287// not(ModalConstraint.of(Modality.MUST, Concreteness.PARTIAL, person).call(v1)),
288// ))).getDnf();
289 var expected = Query.of("Expected", (builder, p1) -> builder.clause((v1) -> List.of( 275 var expected = Query.of("Expected", (builder, p1) -> builder.clause((v1) -> List.of(
290 helper2.call(p1, v1), 276 helper.callTransitive(p1, v1),
291 not(ModalConstraint.of(Modality.MUST, Concreteness.PARTIAL, person).call(v1)), 277 not(ModalConstraint.of(Modality.MUST, Concreteness.PARTIAL, person).call(v1))
292 ModalConstraint.of(Modality.MAY, Concreteness.PARTIAL, ReasoningAdapter.EXISTS).call(v1) 278 ))).getDnf();
279
280 assertThat(actual, structurallyEqualTo(expected));
281 }
282
283 @Test
284 void liftMultipleTransitiveCallExistsTest() {
285 var input = Query.of("Actual", (builder, p1) -> builder.clause((v1) -> List.of(
286 friend.callTransitive(p1, v1),
287 friendMustView.callTransitive(p1, v1),
288 not(person.call(v1))
289 ))).getDnf();
290 var actual = sut.lift(Modality.MAY, Concreteness.PARTIAL, input);
291
292 var helper = Query.of("Helper", (builder, p1, p2) -> builder.clause(
293 ModalConstraint.of(Modality.MAY, Concreteness.PARTIAL, friend).call(p1, p2),
294 ModalConstraint.of(Modality.MAY, Concreteness.PARTIAL, ReasoningAdapter.EXISTS).call(p2)
295 ));
296 var helper2 = Query.of("Helper2", (builder, p1, p2) -> builder.clause(
297 friendMustView.call(p1, p2),
298 ModalConstraint.of(Modality.MAY, Concreteness.PARTIAL, ReasoningAdapter.EXISTS).call(p2)
299 ));
300 var expected = Query.of("Expected", (builder, p1) -> builder.clause((v1) -> List.of(
301 helper.callTransitive(p1, v1),
302 helper2.callTransitive(p1, v1),
303 not(ModalConstraint.of(Modality.MUST, Concreteness.PARTIAL, person).call(v1))
293 ))).getDnf(); 304 ))).getDnf();
294 305
295 assertThat(actual, structurallyEqualTo(expected)); 306 assertThat(actual, structurallyEqualTo(expected));
generated by cgit v1.2.3-54-g00ecf (git 2.45.2) at 2024-06-29 09:49:31 +0000