diff options
18 files changed, 631 insertions, 121 deletions
diff --git a/subprojects/store-query-viatra/src/main/java/tools/refinery/store/query/viatra/internal/pquery/QueryWrapperFactory.java b/subprojects/store-query-viatra/src/main/java/tools/refinery/store/query/viatra/internal/pquery/QueryWrapperFactory.java index 2b7280f2..502813e1 100644 --- a/subprojects/store-query-viatra/src/main/java/tools/refinery/store/query/viatra/internal/pquery/QueryWrapperFactory.java +++ b/subprojects/store-query-viatra/src/main/java/tools/refinery/store/query/viatra/internal/pquery/QueryWrapperFactory.java | |||
@@ -33,7 +33,7 @@ class QueryWrapperFactory { | |||
33 | private final Dnf2PQuery dnf2PQuery; | 33 | private final Dnf2PQuery dnf2PQuery; |
34 | private final Map<AnySymbolView, SymbolViewWrapper> view2WrapperMap = new LinkedHashMap<>(); | 34 | private final Map<AnySymbolView, SymbolViewWrapper> view2WrapperMap = new LinkedHashMap<>(); |
35 | private final CycleDetectingMapper<RemappedConstraint, RawPQuery> wrapConstraint = new CycleDetectingMapper<>( | 35 | private final CycleDetectingMapper<RemappedConstraint, RawPQuery> wrapConstraint = new CycleDetectingMapper<>( |
36 | RemappedConstraint::toString, this::doWrapConstraint); | 36 | this::doWrapConstraint); |
37 | 37 | ||
38 | QueryWrapperFactory(Dnf2PQuery dnf2PQuery) { | 38 | QueryWrapperFactory(Dnf2PQuery dnf2PQuery) { |
39 | this.dnf2PQuery = dnf2PQuery; | 39 | this.dnf2PQuery = dnf2PQuery; |
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/dnf/Dnf.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/dnf/Dnf.java index 7a3e2a1e..e3c8924b 100644 --- a/subprojects/store-query/src/main/java/tools/refinery/store/query/dnf/Dnf.java +++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/dnf/Dnf.java | |||
@@ -68,7 +68,7 @@ public final class Dnf implements Constraint { | |||
68 | } | 68 | } |
69 | 69 | ||
70 | public boolean isExplicitlyNamed() { | 70 | public boolean isExplicitlyNamed() { |
71 | return name == null; | 71 | return name != null; |
72 | } | 72 | } |
73 | 73 | ||
74 | public String getUniqueName() { | 74 | public String getUniqueName() { |
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/dnf/DnfBuilder.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/dnf/DnfBuilder.java index 8e38ca6b..3d3b5198 100644 --- a/subprojects/store-query/src/main/java/tools/refinery/store/query/dnf/DnfBuilder.java +++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/dnf/DnfBuilder.java | |||
@@ -7,10 +7,7 @@ package tools.refinery.store.query.dnf; | |||
7 | 7 | ||
8 | import tools.refinery.store.query.dnf.callback.*; | 8 | import tools.refinery.store.query.dnf.callback.*; |
9 | import tools.refinery.store.query.literal.Literal; | 9 | import tools.refinery.store.query.literal.Literal; |
10 | import tools.refinery.store.query.term.DataVariable; | 10 | import tools.refinery.store.query.term.*; |
11 | import tools.refinery.store.query.term.NodeVariable; | ||
12 | import tools.refinery.store.query.term.ParameterDirection; | ||
13 | import tools.refinery.store.query.term.Variable; | ||
14 | 11 | ||
15 | import java.util.*; | 12 | import java.util.*; |
16 | 13 | ||
@@ -62,6 +59,18 @@ public final class DnfBuilder { | |||
62 | return variable; | 59 | return variable; |
63 | } | 60 | } |
64 | 61 | ||
62 | public Variable parameter(Parameter parameter) { | ||
63 | return parameter(null, parameter); | ||
64 | } | ||
65 | |||
66 | public Variable parameter(String name, Parameter parameter) { | ||
67 | var type = parameter.tryGetType(); | ||
68 | if (type.isPresent()) { | ||
69 | return parameter(name, type.get(), parameter.getDirection()); | ||
70 | } | ||
71 | return parameter(name, parameter.getDirection()); | ||
72 | } | ||
73 | |||
65 | public DnfBuilder parameter(Variable variable) { | 74 | public DnfBuilder parameter(Variable variable) { |
66 | return parameter(variable, ParameterDirection.OUT); | 75 | return parameter(variable, ParameterDirection.OUT); |
67 | } | 76 | } |
@@ -129,7 +138,7 @@ public final class DnfBuilder { | |||
129 | } | 138 | } |
130 | 139 | ||
131 | public <T> DnfBuilder clause(Class<T> type1, ClauseCallback1Data1<T> callback) { | 140 | public <T> DnfBuilder clause(Class<T> type1, ClauseCallback1Data1<T> callback) { |
132 | return clause(callback.toLiterals(Variable.of("v1", type1))); | 141 | return clause(callback.toLiterals(Variable.of("d1", type1))); |
133 | } | 142 | } |
134 | 143 | ||
135 | public DnfBuilder clause(ClauseCallback2Data0 callback) { | 144 | public DnfBuilder clause(ClauseCallback2Data0 callback) { |
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/equality/DeepDnfEqualityChecker.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/equality/DeepDnfEqualityChecker.java index a212b3f5..d6171314 100644 --- a/subprojects/store-query/src/main/java/tools/refinery/store/query/equality/DeepDnfEqualityChecker.java +++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/equality/DeepDnfEqualityChecker.java | |||
@@ -14,8 +14,7 @@ import tools.refinery.store.util.CycleDetectingMapper; | |||
14 | import java.util.List; | 14 | import java.util.List; |
15 | 15 | ||
16 | public class DeepDnfEqualityChecker implements DnfEqualityChecker { | 16 | public class DeepDnfEqualityChecker implements DnfEqualityChecker { |
17 | private final CycleDetectingMapper<Pair, Boolean> mapper = new CycleDetectingMapper<>(Pair::toString, | 17 | private final CycleDetectingMapper<Pair, Boolean> mapper = new CycleDetectingMapper<>(this::doCheckEqual); |
18 | this::doCheckEqual); | ||
19 | 18 | ||
20 | @Override | 19 | @Override |
21 | public boolean dnfEqual(Dnf left, Dnf right) { | 20 | public boolean dnfEqual(Dnf left, Dnf right) { |
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/AnyDataVariable.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/AnyDataVariable.java index 192c39c5..ed6941da 100644 --- a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/AnyDataVariable.java +++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/AnyDataVariable.java | |||
@@ -22,6 +22,16 @@ public abstract sealed class AnyDataVariable extends Variable implements AnyTerm | |||
22 | } | 22 | } |
23 | 23 | ||
24 | @Override | 24 | @Override |
25 | public boolean isNodeVariable() { | ||
26 | return false; | ||
27 | } | ||
28 | |||
29 | @Override | ||
30 | public boolean isDataVariable() { | ||
31 | return true; | ||
32 | } | ||
33 | |||
34 | @Override | ||
25 | public NodeVariable asNodeVariable() { | 35 | public NodeVariable asNodeVariable() { |
26 | throw new IllegalStateException("%s is a data variable".formatted(this)); | 36 | throw new IllegalStateException("%s is a data variable".formatted(this)); |
27 | } | 37 | } |
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/NodeVariable.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/NodeVariable.java index d679908a..e466f1c9 100644 --- a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/NodeVariable.java +++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/NodeVariable.java | |||
@@ -37,6 +37,16 @@ public final class NodeVariable extends Variable { | |||
37 | } | 37 | } |
38 | 38 | ||
39 | @Override | 39 | @Override |
40 | public boolean isNodeVariable() { | ||
41 | return true; | ||
42 | } | ||
43 | |||
44 | @Override | ||
45 | public boolean isDataVariable() { | ||
46 | return false; | ||
47 | } | ||
48 | |||
49 | @Override | ||
40 | public NodeVariable asNodeVariable() { | 50 | public NodeVariable asNodeVariable() { |
41 | return this; | 51 | return this; |
42 | } | 52 | } |
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/Variable.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/Variable.java index 74384df3..89ef0d89 100644 --- a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/Variable.java +++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/Variable.java | |||
@@ -44,6 +44,10 @@ public abstract sealed class Variable permits AnyDataVariable, NodeVariable { | |||
44 | 44 | ||
45 | public abstract Variable renew(); | 45 | public abstract Variable renew(); |
46 | 46 | ||
47 | public abstract boolean isNodeVariable(); | ||
48 | |||
49 | public abstract boolean isDataVariable(); | ||
50 | |||
47 | public abstract NodeVariable asNodeVariable(); | 51 | public abstract NodeVariable asNodeVariable(); |
48 | 52 | ||
49 | public abstract <T> DataVariable<T> asDataVariable(Class<T> type); | 53 | public abstract <T> DataVariable<T> asDataVariable(Class<T> type); |
diff --git a/subprojects/store-reasoning/build.gradle.kts b/subprojects/store-reasoning/build.gradle.kts index abad0491..6c568df0 100644 --- a/subprojects/store-reasoning/build.gradle.kts +++ b/subprojects/store-reasoning/build.gradle.kts | |||
@@ -10,4 +10,5 @@ plugins { | |||
10 | 10 | ||
11 | dependencies { | 11 | dependencies { |
12 | api(project(":refinery-store-query")) | 12 | api(project(":refinery-store-query")) |
13 | testImplementation(testFixtures(project(":refinery-store-query"))) | ||
13 | } | 14 | } |
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/ReasoningAdapter.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/ReasoningAdapter.java index 6d5d6f89..66e809f7 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/ReasoningAdapter.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/ReasoningAdapter.java | |||
@@ -13,7 +13,8 @@ import tools.refinery.store.reasoning.representation.PartialRelation; | |||
13 | import tools.refinery.store.reasoning.representation.PartialSymbol; | 13 | import tools.refinery.store.reasoning.representation.PartialSymbol; |
14 | 14 | ||
15 | public interface ReasoningAdapter extends ModelAdapter { | 15 | public interface ReasoningAdapter extends ModelAdapter { |
16 | PartialRelation EXISTS = new PartialRelation("exists", 1); | 16 | PartialRelation EXISTS = PartialSymbol.of("exists", 1); |
17 | PartialRelation EQUALS = PartialSymbol.of("equals", 2); | ||
17 | 18 | ||
18 | @Override | 19 | @Override |
19 | ReasoningStoreAdapter getStoreAdapter(); | 20 | ReasoningStoreAdapter getStoreAdapter(); |
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 ac41d170..8bbb75d1 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,124 +5,181 @@ | |||
5 | */ | 5 | */ |
6 | package tools.refinery.store.reasoning.lifting; | 6 | package tools.refinery.store.reasoning.lifting; |
7 | 7 | ||
8 | import org.jetbrains.annotations.Nullable; | 8 | import tools.refinery.store.query.Constraint; |
9 | import tools.refinery.store.query.dnf.Dnf; | 9 | import tools.refinery.store.query.dnf.Dnf; |
10 | import tools.refinery.store.query.dnf.DnfBuilder; | ||
11 | import tools.refinery.store.query.dnf.DnfClause; | 10 | import tools.refinery.store.query.dnf.DnfClause; |
12 | import tools.refinery.store.query.literal.CallLiteral; | 11 | import tools.refinery.store.query.equality.DnfEqualityChecker; |
13 | import tools.refinery.store.query.literal.CallPolarity; | 12 | import tools.refinery.store.query.literal.*; |
14 | import tools.refinery.store.query.literal.Literal; | ||
15 | import tools.refinery.store.query.term.NodeVariable; | 13 | import tools.refinery.store.query.term.NodeVariable; |
14 | import tools.refinery.store.query.term.ParameterDirection; | ||
16 | import tools.refinery.store.query.term.Variable; | 15 | import tools.refinery.store.query.term.Variable; |
17 | import tools.refinery.store.reasoning.ReasoningAdapter; | 16 | import tools.refinery.store.reasoning.ReasoningAdapter; |
17 | import tools.refinery.store.reasoning.literal.Concreteness; | ||
18 | import tools.refinery.store.reasoning.literal.ModalConstraint; | 18 | import tools.refinery.store.reasoning.literal.ModalConstraint; |
19 | import tools.refinery.store.reasoning.literal.Modality; | 19 | import tools.refinery.store.reasoning.literal.Modality; |
20 | import tools.refinery.store.reasoning.literal.PartialLiterals; | ||
21 | import tools.refinery.store.util.CycleDetectingMapper; | ||
22 | 20 | ||
23 | import java.util.ArrayList; | 21 | import java.util.*; |
24 | import java.util.LinkedHashSet; | 22 | import java.util.stream.Collectors; |
25 | import java.util.List; | ||
26 | 23 | ||
27 | public class DnfLifter { | 24 | public class DnfLifter { |
28 | private final CycleDetectingMapper<ModalDnf, Dnf> mapper = new CycleDetectingMapper<>(ModalDnf::toString, | 25 | private final Map<ModalDnf, Dnf> cache = new HashMap<>(); |
29 | this::doLift); | ||
30 | 26 | ||
31 | public Dnf lift(Modality modality, Dnf query) { | 27 | public Dnf lift(Modality modality, Concreteness concreteness, Dnf dnf) { |
32 | return mapper.map(new ModalDnf(modality, query)); | 28 | return cache.computeIfAbsent(new ModalDnf(modality, concreteness, dnf), this::doLift); |
33 | } | 29 | } |
34 | 30 | ||
35 | private Dnf doLift(ModalDnf modalDnf) { | 31 | private Dnf doLift(ModalDnf modalDnf) { |
36 | var modality = modalDnf.modality(); | 32 | var modality = modalDnf.modality(); |
33 | var concreteness = modalDnf.concreteness(); | ||
37 | var dnf = modalDnf.dnf(); | 34 | var dnf = modalDnf.dnf(); |
38 | var builder = Dnf.builder(); | 35 | var builder = Dnf.builder("%s#%s#%s".formatted(dnf.name(), modality, concreteness)); |
39 | builder.symbolicParameters(dnf.getSymbolicParameters()); | 36 | builder.symbolicParameters(dnf.getSymbolicParameters()); |
40 | boolean changed = false; | 37 | builder.functionalDependencies(dnf.getFunctionalDependencies()); |
41 | for (var clause : dnf.getClauses()) { | 38 | for (var clause : dnf.getClauses()) { |
42 | if (liftClause(modality, dnf, clause, builder)) { | 39 | builder.clause(liftClause(modality, concreteness, dnf, clause)); |
43 | changed = true; | ||
44 | } | ||
45 | } | 40 | } |
46 | if (changed) { | 41 | var liftedDnf = builder.build(); |
47 | return builder.build(); | 42 | if (dnf.equalsWithSubstitution(DnfEqualityChecker.DEFAULT, liftedDnf)) { |
43 | return dnf; | ||
48 | } | 44 | } |
49 | return dnf; | 45 | return liftedDnf; |
50 | } | 46 | } |
51 | 47 | ||
52 | private boolean liftClause(Modality modality, Dnf originalDnf, DnfClause clause, DnfBuilder builder) { | 48 | private List<Literal> liftClause(Modality modality, Concreteness concreteness, Dnf dnf, DnfClause clause) { |
53 | boolean changed = false; | 49 | var liftedLiterals = new ArrayList<Literal>(); |
54 | var quantifiedVariables = getQuantifiedDataVariables(originalDnf, clause); | 50 | for (var literal : clause.literals()) { |
55 | var literals = clause.literals(); | 51 | var liftedLiteral = liftLiteral(modality, concreteness, clause, literal); |
56 | var liftedLiterals = new ArrayList<Literal>(literals.size()); | ||
57 | for (var literal : literals) { | ||
58 | Literal liftedLiteral = liftLiteral(modality, literal); | ||
59 | if (liftedLiteral == null) { | ||
60 | liftedLiteral = literal; | ||
61 | } else { | ||
62 | changed = true; | ||
63 | } | ||
64 | liftedLiterals.add(liftedLiteral); | 52 | liftedLiterals.add(liftedLiteral); |
65 | var variable = isExistsLiteralForVariable(modality, liftedLiteral); | ||
66 | if (variable != null) { | ||
67 | // If we already quantify over the existence of the variable with the expected modality, | ||
68 | // we don't need to insert quantification manually. | ||
69 | quantifiedVariables.remove(variable); | ||
70 | } | ||
71 | } | 53 | } |
54 | var quantifiedVariables = getQuantifiedNodeVariables(dnf, clause); | ||
55 | var existsConstraint = ModalConstraint.of(modality, concreteness, ReasoningAdapter.EXISTS); | ||
72 | for (var quantifiedVariable : quantifiedVariables) { | 56 | for (var quantifiedVariable : quantifiedVariables) { |
73 | // Quantify over data variables that are not already quantified with the expected modality. | 57 | liftedLiterals.add(existsConstraint.call(quantifiedVariable)); |
74 | liftedLiterals.add(new CallLiteral(CallPolarity.POSITIVE, | ||
75 | new ModalConstraint(modality, ReasoningAdapter.EXISTS), List.of(quantifiedVariable))); | ||
76 | } | 58 | } |
77 | builder.clause(liftedLiterals); | 59 | return liftedLiterals; |
78 | return changed || !quantifiedVariables.isEmpty(); | ||
79 | } | 60 | } |
80 | 61 | ||
81 | private static LinkedHashSet<Variable> getQuantifiedDataVariables(Dnf originalDnf, DnfClause clause) { | 62 | private Literal liftLiteral(Modality modality, Concreteness concreteness, DnfClause clause, Literal literal) { |
82 | var quantifiedVariables = new LinkedHashSet<>(clause.positiveVariables()); | 63 | if (literal instanceof CallLiteral callLiteral) { |
83 | for (var symbolicParameter : originalDnf.getSymbolicParameters()) { | 64 | return liftCallLiteral(modality, concreteness, clause, callLiteral); |
84 | // The existence of parameters will be checked outside this DNF. | 65 | } else if (literal instanceof EquivalenceLiteral equivalenceLiteral) { |
85 | quantifiedVariables.remove(symbolicParameter.getVariable()); | 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); | ||
86 | } | 77 | } |
87 | quantifiedVariables.removeIf(variable -> !(variable instanceof NodeVariable)); | ||
88 | return quantifiedVariables; | ||
89 | } | 78 | } |
90 | 79 | ||
91 | @Nullable | 80 | private Literal liftCallLiteral(Modality modality, Concreteness concreteness, DnfClause clause, |
92 | private Variable isExistsLiteralForVariable(Modality modality, Literal literal) { | 81 | CallLiteral callLiteral) { |
93 | if (literal instanceof CallLiteral callLiteral && | 82 | Constraint target = callLiteral.getTarget(); |
94 | callLiteral.getPolarity() == CallPolarity.POSITIVE && | 83 | var polarity = callLiteral.getPolarity(); |
95 | callLiteral.getTarget() instanceof ModalConstraint modalConstraint && | 84 | var arguments = callLiteral.getArguments(); |
96 | modalConstraint.modality() == modality && | 85 | return switch (polarity) { |
97 | modalConstraint.constraint().equals(ReasoningAdapter.EXISTS)) { | 86 | case POSITIVE -> ModalConstraint.of(modality, concreteness, target).call( |
98 | return callLiteral.getArguments().get(0); | 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); | ||
99 | } | 113 | } |
100 | return null; | 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); | ||
101 | } | 130 | } |
102 | 131 | ||
103 | @Nullable | 132 | private Dnf createTransitiveHelper(Modality modality, Concreteness concreteness, Constraint target) { |
104 | private Literal liftLiteral(Modality modality, Literal literal) { | 133 | var liftedTarget = ModalConstraint.of(modality, concreteness, target); |
105 | if (!(literal instanceof CallLiteral callLiteral)) { | 134 | var existsConstraint = ModalConstraint.of(modality, concreteness, ReasoningAdapter.EXISTS); |
106 | return null; | 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()); | ||
107 | } | 161 | } |
108 | var target = callLiteral.getTarget(); | 162 | return ModalConstraint.of(modality.negate(), concreteness, ReasoningAdapter.EQUALS).call( |
109 | if (target instanceof ModalConstraint modalTarget) { | 163 | CallPolarity.NEGATIVE, equivalenceLiteral.getLeft(), equivalenceLiteral.getRight()); |
110 | var actualTarget = modalTarget.constraint(); | 164 | } |
111 | if (actualTarget instanceof Dnf dnf) { | 165 | |
112 | var targetModality = modalTarget.modality(); | 166 | private static Set<NodeVariable> getQuantifiedNodeVariables(Dnf dnf, DnfClause clause) { |
113 | var liftedTarget = lift(targetModality, dnf); | 167 | var quantifiedVariables = clause.positiveVariables().stream() |
114 | return new CallLiteral(callLiteral.getPolarity(), liftedTarget, callLiteral.getArguments()); | 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); | ||
115 | } | 174 | } |
116 | // No more lifting to be done, pass any modal call to a partial symbol through. | 175 | } |
117 | return null; | 176 | return quantifiedVariables; |
118 | } else if (target instanceof Dnf dnf) { | 177 | } |
119 | var polarity = callLiteral.getPolarity(); | 178 | |
120 | var liftedTarget = lift(modality.commute(polarity), dnf); | 179 | private record ModalDnf(Modality modality, Concreteness concreteness, Dnf dnf) { |
121 | // Use == instead of equals(), because lift will return the same object by reference is there are no | 180 | @Override |
122 | // changes made during lifting. | 181 | public String toString() { |
123 | return liftedTarget == target ? null : new CallLiteral(polarity, liftedTarget, callLiteral.getArguments()); | 182 | return "%s %s %s".formatted(modality, concreteness, dnf.name()); |
124 | } else { | ||
125 | return PartialLiterals.addModality(callLiteral, modality); | ||
126 | } | 183 | } |
127 | } | 184 | } |
128 | } | 185 | } |
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/lifting/ModalDnf.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/lifting/ModalDnf.java deleted file mode 100644 index 16fb8fbf..00000000 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/lifting/ModalDnf.java +++ /dev/null | |||
@@ -1,16 +0,0 @@ | |||
1 | /* | ||
2 | * SPDX-FileCopyrightText: 2021-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.dnf.Dnf; | ||
9 | import tools.refinery.store.reasoning.literal.Modality; | ||
10 | |||
11 | record ModalDnf(Modality modality, Dnf dnf) { | ||
12 | @Override | ||
13 | public String toString() { | ||
14 | return "%s %s".formatted(modality, dnf.name()); | ||
15 | } | ||
16 | } | ||
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/literal/Concreteness.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/literal/Concreteness.java new file mode 100644 index 00000000..43ac5904 --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/literal/Concreteness.java | |||
@@ -0,0 +1,18 @@ | |||
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.literal; | ||
7 | |||
8 | import java.util.Locale; | ||
9 | |||
10 | public enum Concreteness { | ||
11 | PARTIAL, | ||
12 | CANDIDATE; | ||
13 | |||
14 | @Override | ||
15 | public String toString() { | ||
16 | return name().toLowerCase(Locale.ROOT); | ||
17 | } | ||
18 | } | ||
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 4e5a6099..6e0e91e1 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 | |||
@@ -9,15 +9,25 @@ 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.Reduction; | 10 | import tools.refinery.store.query.literal.Reduction; |
11 | import tools.refinery.store.query.term.Parameter; | 11 | import tools.refinery.store.query.term.Parameter; |
12 | import tools.refinery.store.query.view.AnySymbolView; | ||
12 | 13 | ||
13 | import java.util.List; | 14 | import java.util.List; |
14 | 15 | ||
15 | public record ModalConstraint(Modality modality, Constraint constraint) implements Constraint { | 16 | public record ModalConstraint(Modality modality, Concreteness concreteness, Constraint constraint) |
16 | private static final String FORMAT = "%s %s"; | 17 | implements Constraint { |
18 | public ModalConstraint { | ||
19 | if (constraint instanceof AnySymbolView || constraint instanceof ModalConstraint) { | ||
20 | throw new IllegalArgumentException("Already concrete constraints cannot be abstracted"); | ||
21 | } | ||
22 | } | ||
23 | |||
24 | public ModalConstraint(Modality modality, Constraint constraint) { | ||
25 | this(modality, Concreteness.PARTIAL, constraint); | ||
26 | } | ||
17 | 27 | ||
18 | @Override | 28 | @Override |
19 | public String name() { | 29 | public String name() { |
20 | return FORMAT.formatted(modality, constraint.name()); | 30 | return formatName(constraint.name()); |
21 | } | 31 | } |
22 | 32 | ||
23 | @Override | 33 | @Override |
@@ -36,16 +46,33 @@ public record ModalConstraint(Modality modality, Constraint constraint) implemen | |||
36 | return false; | 46 | return false; |
37 | } | 47 | } |
38 | var otherModalConstraint = (ModalConstraint) other; | 48 | var otherModalConstraint = (ModalConstraint) other; |
39 | return modality == otherModalConstraint.modality && constraint.equals(helper, otherModalConstraint.constraint); | 49 | return modality == otherModalConstraint.modality && |
50 | concreteness == otherModalConstraint.concreteness && | ||
51 | constraint.equals(helper, otherModalConstraint.constraint); | ||
40 | } | 52 | } |
41 | 53 | ||
42 | @Override | 54 | @Override |
43 | public String toReferenceString() { | 55 | public String toReferenceString() { |
44 | return FORMAT.formatted(modality, constraint.toReferenceString()); | 56 | return formatName(constraint.toReferenceString()); |
45 | } | 57 | } |
46 | 58 | ||
47 | @Override | 59 | @Override |
48 | public String toString() { | 60 | public String toString() { |
49 | return FORMAT.formatted(modality, constraint); | 61 | return formatName(constraint.toString()); |
62 | } | ||
63 | |||
64 | private String formatName(String constraintName) { | ||
65 | if (concreteness == Concreteness.PARTIAL) { | ||
66 | return "%s %s".formatted(modality, constraintName); | ||
67 | } | ||
68 | return "%s %s %s".formatted(modality, concreteness, constraintName); | ||
69 | } | ||
70 | |||
71 | public static Constraint of(Modality modality, Concreteness concreteness, Constraint constraint) { | ||
72 | if (constraint instanceof AnySymbolView || constraint instanceof ModalConstraint) { | ||
73 | // Symbol views and lifted constraints are already concrete. Thus, they cannot be abstracted at all. | ||
74 | return constraint; | ||
75 | } | ||
76 | return new ModalConstraint(modality, concreteness, constraint); | ||
50 | } | 77 | } |
51 | } | 78 | } |
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/literal/Modality.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/literal/Modality.java index 96466d5c..c99a0399 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/literal/Modality.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/literal/Modality.java | |||
@@ -11,14 +11,12 @@ import java.util.Locale; | |||
11 | 11 | ||
12 | public enum Modality { | 12 | public enum Modality { |
13 | MUST, | 13 | MUST, |
14 | MAY, | 14 | MAY; |
15 | CURRENT; | ||
16 | 15 | ||
17 | public Modality negate() { | 16 | public Modality negate() { |
18 | return switch(this) { | 17 | return switch(this) { |
19 | case MUST -> MAY; | 18 | case MUST -> MAY; |
20 | case MAY -> MUST; | 19 | case MAY -> MUST; |
21 | case CURRENT -> CURRENT; | ||
22 | }; | 20 | }; |
23 | } | 21 | } |
24 | 22 | ||
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/literal/PartialLiterals.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/literal/PartialLiterals.java index 0e46a795..4f07f17d 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/literal/PartialLiterals.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/literal/PartialLiterals.java | |||
@@ -20,10 +20,6 @@ public final class PartialLiterals { | |||
20 | return addModality(literal, Modality.MUST); | 20 | return addModality(literal, Modality.MUST); |
21 | } | 21 | } |
22 | 22 | ||
23 | public static CallLiteral current(CallLiteral literal) { | ||
24 | return addModality(literal, Modality.CURRENT); | ||
25 | } | ||
26 | |||
27 | public static CallLiteral addModality(CallLiteral literal, Modality modality) { | 23 | public static CallLiteral addModality(CallLiteral literal, Modality modality) { |
28 | var target = literal.getTarget(); | 24 | var target = literal.getTarget(); |
29 | if (target instanceof ModalConstraint) { | 25 | if (target instanceof ModalConstraint) { |
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/representation/PartialSymbol.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/representation/PartialSymbol.java index 3a08bdd8..2f04534a 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/representation/PartialSymbol.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/representation/PartialSymbol.java | |||
@@ -14,4 +14,12 @@ public sealed interface PartialSymbol<A, C> extends AnyPartialSymbol permits Par | |||
14 | A defaultValue(); | 14 | A defaultValue(); |
15 | 15 | ||
16 | C defaultConcreteValue(); | 16 | C defaultConcreteValue(); |
17 | |||
18 | static PartialRelation of(String name, int arity) { | ||
19 | return new PartialRelation(name, arity); | ||
20 | } | ||
21 | |||
22 | static <A, C> PartialFunction<A, C> of(String name, int arity, AbstractDomain<A, C> abstractDomain) { | ||
23 | return new PartialFunction<>(name, arity, abstractDomain); | ||
24 | } | ||
17 | } | 25 | } |
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 new file mode 100644 index 00000000..2d089245 --- /dev/null +++ b/subprojects/store-reasoning/src/test/java/tools/refinery/store/reasoning/lifting/DnfLifterTest.java | |||
@@ -0,0 +1,384 @@ | |||
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 org.junit.jupiter.api.BeforeEach; | ||
9 | import org.junit.jupiter.api.Test; | ||
10 | import tools.refinery.store.query.dnf.Dnf; | ||
11 | import tools.refinery.store.query.dnf.Query; | ||
12 | import tools.refinery.store.query.term.ParameterDirection; | ||
13 | import tools.refinery.store.query.view.AnySymbolView; | ||
14 | import tools.refinery.store.query.view.FunctionView; | ||
15 | import tools.refinery.store.query.view.MustView; | ||
16 | import tools.refinery.store.reasoning.ReasoningAdapter; | ||
17 | import tools.refinery.store.reasoning.literal.Concreteness; | ||
18 | import tools.refinery.store.reasoning.literal.ModalConstraint; | ||
19 | import tools.refinery.store.reasoning.literal.Modality; | ||
20 | import tools.refinery.store.reasoning.representation.PartialRelation; | ||
21 | import tools.refinery.store.reasoning.representation.PartialSymbol; | ||
22 | import tools.refinery.store.representation.Symbol; | ||
23 | import tools.refinery.store.representation.TruthValue; | ||
24 | |||
25 | import java.util.List; | ||
26 | |||
27 | import static org.hamcrest.MatcherAssert.assertThat; | ||
28 | import static tools.refinery.store.query.literal.Literals.check; | ||
29 | import static tools.refinery.store.query.literal.Literals.not; | ||
30 | import static tools.refinery.store.query.term.int_.IntTerms.*; | ||
31 | import static tools.refinery.store.query.tests.QueryMatchers.structurallyEqualTo; | ||
32 | |||
33 | class DnfLifterTest { | ||
34 | private static final Symbol<TruthValue> friendSymbol = Symbol.of("friend", 2, TruthValue.class, | ||
35 | TruthValue.UNKNOWN); | ||
36 | private static final AnySymbolView friendMustView = new MustView(friendSymbol); | ||
37 | private static final Symbol<Integer> age = Symbol.of("age", 1, Integer.class); | ||
38 | private static final FunctionView<Integer> ageView = new FunctionView<>(age); | ||
39 | private static final PartialRelation person = PartialSymbol.of("Person", 1); | ||
40 | private static final PartialRelation friend = PartialSymbol.of("friend", 2); | ||
41 | |||
42 | private DnfLifter sut; | ||
43 | |||
44 | @BeforeEach | ||
45 | void beforeEach() { | ||
46 | sut = new DnfLifter(); | ||
47 | } | ||
48 | |||
49 | @Test | ||
50 | void liftPartialRelationCallTest() { | ||
51 | var input = Query.of("Actual", (builder, p1) -> builder.clause((v1) -> List.of( | ||
52 | friend.call(p1, v1) | ||
53 | ))).getDnf(); | ||
54 | var actual = sut.lift(Modality.MUST, Concreteness.PARTIAL, input); | ||
55 | |||
56 | var expected = Query.of("Expected", (builder, p1) -> builder.clause((v1) -> List.of( | ||
57 | ModalConstraint.of(Modality.MUST, Concreteness.PARTIAL, friend).call(p1, v1), | ||
58 | ModalConstraint.of(Modality.MUST, Concreteness.PARTIAL, ReasoningAdapter.EXISTS).call(v1) | ||
59 | ))).getDnf(); | ||
60 | |||
61 | assertThat(actual, structurallyEqualTo(expected)); | ||
62 | } | ||
63 | |||
64 | @Test | ||
65 | void liftPartialDnfCallTest() { | ||
66 | var called = Query.of("Called", (builder, p1, p2) -> builder.clause( | ||
67 | friend.call(p1, p2), | ||
68 | friend.call(p2, p1) | ||
69 | )); | ||
70 | var input = Query.of("Actual", (builder, p1) -> builder.clause((v1) -> List.of( | ||
71 | called.call(p1, v1) | ||
72 | ))).getDnf(); | ||
73 | var actual = sut.lift(Modality.MUST, Concreteness.PARTIAL, input); | ||
74 | |||
75 | var expected = Query.of("Expected", (builder, p1) -> builder.clause((v1) -> List.of( | ||
76 | ModalConstraint.of(Modality.MUST, Concreteness.PARTIAL, called.getDnf()).call(p1, v1), | ||
77 | ModalConstraint.of(Modality.MUST, Concreteness.PARTIAL, ReasoningAdapter.EXISTS).call(v1) | ||
78 | ))).getDnf(); | ||
79 | |||
80 | assertThat(actual, structurallyEqualTo(expected)); | ||
81 | } | ||
82 | |||
83 | @Test | ||
84 | void liftSymbolViewCallTest() { | ||
85 | var input = Query.of("Actual", (builder, p1) -> builder.clause((v1) -> List.of( | ||
86 | friendMustView.call(p1, v1) | ||
87 | ))).getDnf(); | ||
88 | var actual = sut.lift(Modality.MUST, Concreteness.PARTIAL, input); | ||
89 | |||
90 | var expected = Query.of("Expected", (builder, p1) -> builder.clause((v1) -> List.of( | ||
91 | friendMustView.call(p1, v1), | ||
92 | ModalConstraint.of(Modality.MUST, Concreteness.PARTIAL, ReasoningAdapter.EXISTS).call(v1) | ||
93 | ))).getDnf(); | ||
94 | |||
95 | assertThat(actual, structurallyEqualTo(expected)); | ||
96 | } | ||
97 | |||
98 | @Test | ||
99 | void liftPartialRelationNegativeCallTest() { | ||
100 | var input = Query.of("Actual", (builder, p1) -> builder.clause((v1) -> List.of( | ||
101 | not(friend.call(p1, v1)), | ||
102 | friend.call(v1, p1) | ||
103 | ))).getDnf(); | ||
104 | var actual = sut.lift(Modality.MUST, Concreteness.PARTIAL, input); | ||
105 | |||
106 | var expected = Query.of("Expected", (builder, p1) -> builder.clause((v1) -> List.of( | ||
107 | not(ModalConstraint.of(Modality.MAY, Concreteness.PARTIAL, friend).call(p1, v1)), | ||
108 | ModalConstraint.of(Modality.MUST, Concreteness.PARTIAL, friend).call(v1, p1), | ||
109 | ModalConstraint.of(Modality.MUST, Concreteness.PARTIAL, ReasoningAdapter.EXISTS).call(v1) | ||
110 | ))).getDnf(); | ||
111 | |||
112 | assertThat(actual, structurallyEqualTo(expected)); | ||
113 | } | ||
114 | |||
115 | @Test | ||
116 | void liftPartialRelationQuantifiedNegativeCallTest() { | ||
117 | var input = Query.of("Actual", (builder, p1) -> builder.clause((v1) -> List.of( | ||
118 | person.call(p1), | ||
119 | not(friend.call(p1, v1)) | ||
120 | ))).getDnf(); | ||
121 | var actual = sut.lift(Modality.MAY, Concreteness.PARTIAL, input); | ||
122 | |||
123 | var helper = Query.of("Helper", (builder, p1, p2) -> builder.clause( | ||
124 | ModalConstraint.of(Modality.MUST, Concreteness.PARTIAL, friend).call(p1, p2), | ||
125 | ModalConstraint.of(Modality.MUST, Concreteness.PARTIAL, ReasoningAdapter.EXISTS).call(p2) | ||
126 | )); | ||
127 | var expected = Query.of("Expected", (builder, p1) -> builder.clause((v1) -> List.of( | ||
128 | ModalConstraint.of(Modality.MAY, Concreteness.PARTIAL, person).call(p1), | ||
129 | not(helper.call(p1, v1)) | ||
130 | ))).getDnf(); | ||
131 | |||
132 | assertThat(actual, structurallyEqualTo(expected)); | ||
133 | } | ||
134 | |||
135 | @Test | ||
136 | void liftSymbolViewQuantifiedNegativeCallTest() { | ||
137 | var input = Query.of("Actual", (builder, p1) -> builder.clause((v1) -> List.of( | ||
138 | person.call(p1), | ||
139 | not(friendMustView.call(p1, v1)) | ||
140 | ))).getDnf(); | ||
141 | var actual = sut.lift(Modality.MAY, Concreteness.PARTIAL, input); | ||
142 | |||
143 | var helper = Query.of("Helper", (builder, p1, p2) -> builder.clause( | ||
144 | friendMustView.call(p1, p2), | ||
145 | ModalConstraint.of(Modality.MUST, Concreteness.PARTIAL, ReasoningAdapter.EXISTS).call(p2) | ||
146 | )); | ||
147 | var expected = Query.of("Expected", (builder, p1) -> builder.clause((v1) -> List.of( | ||
148 | ModalConstraint.of(Modality.MAY, Concreteness.PARTIAL, person).call(p1), | ||
149 | not(helper.call(p1, v1)) | ||
150 | ))).getDnf(); | ||
151 | |||
152 | assertThat(actual, structurallyEqualTo(expected)); | ||
153 | } | ||
154 | |||
155 | @Test | ||
156 | void liftPartialRelationQuantifiedNegativeDiagonalCallTest() { | ||
157 | var input = Query.of("Actual", (builder) -> builder.clause((v1) -> List.of( | ||
158 | not(friend.call(v1, v1)) | ||
159 | ))).getDnf(); | ||
160 | var actual = sut.lift(Modality.MAY, Concreteness.PARTIAL, input); | ||
161 | |||
162 | var helper = Query.of("Helper", (builder, p1) -> builder.clause( | ||
163 | ModalConstraint.of(Modality.MUST, Concreteness.PARTIAL, friend).call(p1, p1), | ||
164 | ModalConstraint.of(Modality.MUST, Concreteness.PARTIAL, ReasoningAdapter.EXISTS).call(p1) | ||
165 | )); | ||
166 | var expected = Query.of("Expected", (builder) -> builder.clause((v1) -> List.of( | ||
167 | not(helper.call(v1)) | ||
168 | ))).getDnf(); | ||
169 | |||
170 | assertThat(actual, structurallyEqualTo(expected)); | ||
171 | } | ||
172 | |||
173 | @Test | ||
174 | void liftPartialDnfQuantifiedNegativeInputCallTest() { | ||
175 | var called = Dnf.of("Called", builder -> { | ||
176 | var p1 = builder.parameter("p1", ParameterDirection.IN); | ||
177 | var p2 = builder.parameter("p2", ParameterDirection.OUT); | ||
178 | builder.clause( | ||
179 | friend.call(p1, p2), | ||
180 | friend.call(p2, p1) | ||
181 | ); | ||
182 | }); | ||
183 | var input = Query.of("Actual", (builder, p1) -> builder.clause((v1) -> List.of( | ||
184 | person.call(p1), | ||
185 | not(called.call(p1, v1)) | ||
186 | ))).getDnf(); | ||
187 | var actual = sut.lift(Modality.MAY, Concreteness.PARTIAL, input); | ||
188 | |||
189 | var helper = Dnf.of("Helper", builder -> { | ||
190 | var p1 = builder.parameter("p1", ParameterDirection.IN); | ||
191 | var p2 = builder.parameter("p2", ParameterDirection.OUT); | ||
192 | builder.clause( | ||
193 | ModalConstraint.of(Modality.MUST, Concreteness.PARTIAL, called).call(p1, p2), | ||
194 | ModalConstraint.of(Modality.MUST, Concreteness.PARTIAL, ReasoningAdapter.EXISTS).call(p2) | ||
195 | ); | ||
196 | }); | ||
197 | var expected = Query.of("Expected", (builder, p1) -> builder.clause((v1) -> List.of( | ||
198 | ModalConstraint.of(Modality.MAY, Concreteness.PARTIAL, person).call(p1), | ||
199 | not(helper.call(p1, v1)) | ||
200 | ))).getDnf(); | ||
201 | |||
202 | assertThat(actual, structurallyEqualTo(expected)); | ||
203 | } | ||
204 | |||
205 | @Test | ||
206 | void liftPartialRelationTransitiveCallTest() { | ||
207 | var input = Query.of("Actual", (builder, p1, p2)-> builder.clause( | ||
208 | friend.callTransitive(p1, p2), | ||
209 | not(person.call(p2)) | ||
210 | )).getDnf(); | ||
211 | var actual = sut.lift(Modality.MAY, Concreteness.PARTIAL, input); | ||
212 | |||
213 | var helper = Query.of("Helper", (builder, p1, p2) -> builder.clause( | ||
214 | ModalConstraint.of(Modality.MAY, Concreteness.PARTIAL, friend).call(p1, p2), | ||
215 | ModalConstraint.of(Modality.MAY, Concreteness.PARTIAL, ReasoningAdapter.EXISTS).call(p2) | ||
216 | )); | ||
217 | var helper2 = Query.of("Helper2", (builder, p1, p2) -> { | ||
218 | builder.clause( | ||
219 | ModalConstraint.of(Modality.MAY, Concreteness.PARTIAL, friend).call(p1, p2) | ||
220 | ); | ||
221 | builder.clause((v1) -> List.of( | ||
222 | helper.callTransitive(p1, v1), | ||
223 | ModalConstraint.of(Modality.MAY, Concreteness.PARTIAL, friend).call(v1, p2) | ||
224 | )); | ||
225 | }); | ||
226 | var expected = Query.of("Expected", (builder, p1, p2) -> builder.clause( | ||
227 | helper2.call(p1, p2), | ||
228 | not(ModalConstraint.of(Modality.MUST, Concreteness.PARTIAL, person).call(p2)) | ||
229 | )).getDnf(); | ||
230 | |||
231 | assertThat(actual, structurallyEqualTo(expected)); | ||
232 | } | ||
233 | |||
234 | @Test | ||
235 | void liftPartialSymbolTransitiveCallTest() { | ||
236 | var input = Query.of("Actual", (builder, p1, p2)-> builder.clause( | ||
237 | friendMustView.callTransitive(p1, p2), | ||
238 | not(person.call(p2)) | ||
239 | )).getDnf(); | ||
240 | var actual = sut.lift(Modality.MAY, Concreteness.PARTIAL, input); | ||
241 | |||
242 | var helper = Query.of("Helper", (builder, p1, p2) -> builder.clause( | ||
243 | friendMustView.call(p1, p2), | ||
244 | ModalConstraint.of(Modality.MAY, Concreteness.PARTIAL, ReasoningAdapter.EXISTS).call(p2) | ||
245 | )); | ||
246 | var helper2 = Query.of("Helper2", (builder, p1, p2) -> { | ||
247 | builder.clause( | ||
248 | friendMustView.call(p1, p2) | ||
249 | ); | ||
250 | builder.clause((v1) -> List.of( | ||
251 | helper.callTransitive(p1, v1), | ||
252 | friendMustView.call(v1, p2) | ||
253 | )); | ||
254 | }); | ||
255 | var expected = Query.of("Expected", (builder, p1, p2) -> builder.clause( | ||
256 | helper2.call(p1, p2), | ||
257 | not(ModalConstraint.of(Modality.MUST, Concreteness.PARTIAL, person).call(p2)) | ||
258 | )).getDnf(); | ||
259 | |||
260 | assertThat(actual, structurallyEqualTo(expected)); | ||
261 | } | ||
262 | |||
263 | @Test | ||
264 | void liftPartialRelationTransitiveCallExistsTest() { | ||
265 | var input = Query.of("Actual", (builder, p1) -> builder.clause((v1) -> List.of( | ||
266 | friend.callTransitive(p1, v1), | ||
267 | not(person.call(v1)) | ||
268 | ))).getDnf(); | ||
269 | var actual = sut.lift(Modality.MAY, Concreteness.PARTIAL, input); | ||
270 | |||
271 | var helper = Query.of("Helper", (builder, p1, p2) -> builder.clause( | ||
272 | ModalConstraint.of(Modality.MAY, Concreteness.PARTIAL, friend).call(p1, p2), | ||
273 | ModalConstraint.of(Modality.MAY, Concreteness.PARTIAL, ReasoningAdapter.EXISTS).call(p2) | ||
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( | ||
290 | helper2.call(p1, v1), | ||
291 | not(ModalConstraint.of(Modality.MUST, Concreteness.PARTIAL, person).call(v1)), | ||
292 | ModalConstraint.of(Modality.MAY, Concreteness.PARTIAL, ReasoningAdapter.EXISTS).call(v1) | ||
293 | ))).getDnf(); | ||
294 | |||
295 | assertThat(actual, structurallyEqualTo(expected)); | ||
296 | } | ||
297 | |||
298 | @Test | ||
299 | void liftEquivalentTest() { | ||
300 | var input = Query.of("Actual", (builder, p1, p2) -> builder.clause( | ||
301 | p1.isEquivalent(p2), | ||
302 | person.call(p1) | ||
303 | )).getDnf(); | ||
304 | var actual = sut.lift(Modality.MAY, Concreteness.PARTIAL, input); | ||
305 | |||
306 | var expected = Query.of("Expected", (builder, p1, p2) -> builder.clause( | ||
307 | ModalConstraint.of(Modality.MAY, Concreteness.PARTIAL, person).call(p1), | ||
308 | ModalConstraint.of(Modality.MAY, Concreteness.PARTIAL, ReasoningAdapter.EQUALS).call(p2, p1) | ||
309 | )).getDnf(); | ||
310 | |||
311 | assertThat(actual, structurallyEqualTo(expected)); | ||
312 | } | ||
313 | |||
314 | @Test | ||
315 | void liftNotEquivalentTest() { | ||
316 | var input = Query.of("Actual", (builder, p1, p2) -> builder.clause( | ||
317 | not(p1.isEquivalent(p2)), | ||
318 | friend.call(p1, p2) | ||
319 | )).getDnf(); | ||
320 | var actual = sut.lift(Modality.MAY, Concreteness.PARTIAL, input); | ||
321 | |||
322 | var expected = Query.of("Expected", (builder, p1, p2) -> builder.clause( | ||
323 | ModalConstraint.of(Modality.MAY, Concreteness.PARTIAL, friend).call(p1, p2), | ||
324 | not(ModalConstraint.of(Modality.MUST, Concreteness.PARTIAL, ReasoningAdapter.EQUALS).call(p1, p2)) | ||
325 | )).getDnf(); | ||
326 | |||
327 | assertThat(actual, structurallyEqualTo(expected)); | ||
328 | } | ||
329 | |||
330 | @Test | ||
331 | void liftConstantTest() { | ||
332 | var input = Query.of("Actual", (builder, p1) -> builder.clause((v1) -> List.of( | ||
333 | v1.isConstant(0), | ||
334 | friend.call(v1, p1) | ||
335 | ))).getDnf(); | ||
336 | var actual = sut.lift(Modality.MAY, Concreteness.PARTIAL, input); | ||
337 | |||
338 | var expected = Query.of("Expected", (builder, p1) -> builder.clause((v1) -> List.of( | ||
339 | v1.isConstant(0), | ||
340 | ModalConstraint.of(Modality.MAY, Concreteness.PARTIAL, friend).call(v1, p1), | ||
341 | ModalConstraint.of(Modality.MAY, Concreteness.PARTIAL, ReasoningAdapter.EXISTS).call(v1) | ||
342 | ))).getDnf(); | ||
343 | |||
344 | assertThat(actual, structurallyEqualTo(expected)); | ||
345 | } | ||
346 | |||
347 | @Test | ||
348 | void liftAssignTest() { | ||
349 | var input = Query.of("Actual", Integer.class, (builder, p1, output) -> builder | ||
350 | .clause(Integer.class, (d1) -> List.of( | ||
351 | person.call(p1), | ||
352 | ageView.call(p1, d1), | ||
353 | output.assign(mul(constant(2), d1)) | ||
354 | ))).getDnf(); | ||
355 | var actual = sut.lift(Modality.MAY, Concreteness.PARTIAL, input); | ||
356 | |||
357 | var expected = Query.of("Expected", Integer.class, (builder, p1, output) -> builder | ||
358 | .clause(Integer.class, (d1) -> List.of( | ||
359 | ModalConstraint.of(Modality.MAY, Concreteness.PARTIAL, person).call(p1), | ||
360 | ageView.call(p1, d1), | ||
361 | output.assign(mul(constant(2), d1)) | ||
362 | ))).getDnf(); | ||
363 | |||
364 | assertThat(actual, structurallyEqualTo(expected)); | ||
365 | } | ||
366 | |||
367 | @Test | ||
368 | void liftCheckTest() { | ||
369 | var input = Query.of("Actual", (builder, p1) -> builder.clause(Integer.class, (d1) -> List.of( | ||
370 | person.call(p1), | ||
371 | ageView.call(p1, d1), | ||
372 | check(greaterEq(d1, constant(21))) | ||
373 | ))).getDnf(); | ||
374 | var actual = sut.lift(Modality.MAY, Concreteness.CANDIDATE, input); | ||
375 | |||
376 | var expected = Query.of("Expected", (builder, p1) -> builder.clause(Integer.class, (d1) -> List.of( | ||
377 | ModalConstraint.of(Modality.MAY, Concreteness.CANDIDATE, person).call(p1), | ||
378 | ageView.call(p1, d1), | ||
379 | check(greaterEq(d1, constant(21))) | ||
380 | ))).getDnf(); | ||
381 | |||
382 | assertThat(actual, structurallyEqualTo(expected)); | ||
383 | } | ||
384 | } | ||
diff --git a/subprojects/store/src/main/java/tools/refinery/store/util/CycleDetectingMapper.java b/subprojects/store/src/main/java/tools/refinery/store/util/CycleDetectingMapper.java index 78ad2ad7..2e302663 100644 --- a/subprojects/store/src/main/java/tools/refinery/store/util/CycleDetectingMapper.java +++ b/subprojects/store/src/main/java/tools/refinery/store/util/CycleDetectingMapper.java | |||
@@ -20,6 +20,10 @@ public class CycleDetectingMapper<T, R> { | |||
20 | 20 | ||
21 | private final Map<T, R> results = new HashMap<>(); | 21 | private final Map<T, R> results = new HashMap<>(); |
22 | 22 | ||
23 | public CycleDetectingMapper(Function<T, R> doMap) { | ||
24 | this(Objects::toString, doMap); | ||
25 | } | ||
26 | |||
23 | public CycleDetectingMapper(Function<T, String> getName, Function<T, R> doMap) { | 27 | public CycleDetectingMapper(Function<T, String> getName, Function<T, R> doMap) { |
24 | this.getName = getName; | 28 | this.getName = getName; |
25 | this.doMap = doMap; | 29 | this.doMap = doMap; |