diff options
author | 2023-02-17 17:35:48 +0100 | |
---|---|---|
committer | 2023-02-17 17:35:48 +0100 | |
commit | 8183b588cf5bc665c0f96abc6d11b8dc70eecaa3 (patch) | |
tree | bd0001d59cf1d794b35f44161831905e8da62f13 /subprojects/store/src/main/java/tools | |
parent | refactor: EDSL for DNF literals (diff) | |
download | refinery-8183b588cf5bc665c0f96abc6d11b8dc70eecaa3.tar.gz refinery-8183b588cf5bc665c0f96abc6d11b8dc70eecaa3.tar.zst refinery-8183b588cf5bc665c0f96abc6d11b8dc70eecaa3.zip |
feat: PartialInterpretation representations
Diffstat (limited to 'subprojects/store/src/main/java/tools')
24 files changed, 518 insertions, 30 deletions
diff --git a/subprojects/store/src/main/java/tools/refinery/store/partial/literal/ModalDnfCallLiteral.java b/subprojects/store/src/main/java/tools/refinery/store/partial/literal/ModalDnfCallLiteral.java new file mode 100644 index 00000000..8070726a --- /dev/null +++ b/subprojects/store/src/main/java/tools/refinery/store/partial/literal/ModalDnfCallLiteral.java | |||
@@ -0,0 +1,30 @@ | |||
1 | package tools.refinery.store.partial.literal; | ||
2 | |||
3 | import tools.refinery.store.query.Dnf; | ||
4 | import tools.refinery.store.query.Variable; | ||
5 | import tools.refinery.store.query.literal.CallPolarity; | ||
6 | import tools.refinery.store.query.literal.DnfCallLiteral; | ||
7 | import tools.refinery.store.query.literal.PolarLiteral; | ||
8 | |||
9 | import java.util.List; | ||
10 | import java.util.Map; | ||
11 | |||
12 | public class ModalDnfCallLiteral extends ModalLiteral<Dnf> implements PolarLiteral<ModalDnfCallLiteral> { | ||
13 | public ModalDnfCallLiteral(CallPolarity polarity, Modality modality, Dnf target, List<Variable> arguments) { | ||
14 | super(polarity, modality, target, arguments); | ||
15 | } | ||
16 | |||
17 | public ModalDnfCallLiteral(Modality modality, DnfCallLiteral baseLiteral) { | ||
18 | super(modality.commute(baseLiteral.getPolarity()), baseLiteral); | ||
19 | } | ||
20 | |||
21 | @Override | ||
22 | public ModalDnfCallLiteral substitute(Map<Variable, Variable> substitution) { | ||
23 | return new ModalDnfCallLiteral(getPolarity(), getModality(), getTarget(), substituteArguments(substitution)); | ||
24 | } | ||
25 | |||
26 | @Override | ||
27 | public ModalDnfCallLiteral negate() { | ||
28 | return new ModalDnfCallLiteral(getPolarity().negate(), getModality(), getTarget(), getArguments()); | ||
29 | } | ||
30 | } | ||
diff --git a/subprojects/store/src/main/java/tools/refinery/store/partial/literal/ModalLiteral.java b/subprojects/store/src/main/java/tools/refinery/store/partial/literal/ModalLiteral.java new file mode 100644 index 00000000..a1b6c83e --- /dev/null +++ b/subprojects/store/src/main/java/tools/refinery/store/partial/literal/ModalLiteral.java | |||
@@ -0,0 +1,45 @@ | |||
1 | package tools.refinery.store.partial.literal; | ||
2 | |||
3 | import tools.refinery.store.query.RelationLike; | ||
4 | import tools.refinery.store.query.Variable; | ||
5 | import tools.refinery.store.query.literal.CallLiteral; | ||
6 | import tools.refinery.store.query.literal.CallPolarity; | ||
7 | |||
8 | import java.util.List; | ||
9 | import java.util.Objects; | ||
10 | |||
11 | public abstract class ModalLiteral<T extends RelationLike> extends CallLiteral<T> { | ||
12 | private final Modality modality; | ||
13 | |||
14 | protected ModalLiteral(CallPolarity polarity, Modality modality, T target, List<Variable> arguments) { | ||
15 | super(polarity, target, arguments); | ||
16 | this.modality = modality; | ||
17 | } | ||
18 | |||
19 | protected ModalLiteral(Modality modality, CallLiteral<? extends T> baseLiteral) { | ||
20 | this(baseLiteral.getPolarity(), commute(modality, baseLiteral.getPolarity()), baseLiteral.getTarget(), | ||
21 | baseLiteral.getArguments()); | ||
22 | } | ||
23 | |||
24 | public Modality getModality() { | ||
25 | return modality; | ||
26 | } | ||
27 | |||
28 | @Override | ||
29 | public boolean equals(Object o) { | ||
30 | if (this == o) return true; | ||
31 | if (o == null || getClass() != o.getClass()) return false; | ||
32 | if (!super.equals(o)) return false; | ||
33 | ModalLiteral<?> that = (ModalLiteral<?>) o; | ||
34 | return modality == that.modality; | ||
35 | } | ||
36 | |||
37 | @Override | ||
38 | public int hashCode() { | ||
39 | return Objects.hash(super.hashCode(), modality); | ||
40 | } | ||
41 | |||
42 | private static Modality commute(Modality modality, CallPolarity polarity) { | ||
43 | return polarity.isPositive() ? modality : modality.negate(); | ||
44 | } | ||
45 | } | ||
diff --git a/subprojects/store/src/main/java/tools/refinery/store/partial/literal/ModalRelationLiteral.java b/subprojects/store/src/main/java/tools/refinery/store/partial/literal/ModalRelationLiteral.java new file mode 100644 index 00000000..dbaa524f --- /dev/null +++ b/subprojects/store/src/main/java/tools/refinery/store/partial/literal/ModalRelationLiteral.java | |||
@@ -0,0 +1,31 @@ | |||
1 | package tools.refinery.store.partial.literal; | ||
2 | |||
3 | import tools.refinery.store.partial.representation.PartialRelation; | ||
4 | import tools.refinery.store.query.Variable; | ||
5 | import tools.refinery.store.query.literal.CallPolarity; | ||
6 | import tools.refinery.store.query.literal.PolarLiteral; | ||
7 | |||
8 | import java.util.List; | ||
9 | import java.util.Map; | ||
10 | |||
11 | public final class ModalRelationLiteral extends ModalLiteral<PartialRelation> | ||
12 | implements PolarLiteral<ModalRelationLiteral> { | ||
13 | public ModalRelationLiteral(CallPolarity polarity, Modality modality, PartialRelation target, | ||
14 | List<Variable> arguments) { | ||
15 | super(polarity, modality, target, arguments); | ||
16 | } | ||
17 | |||
18 | public ModalRelationLiteral(Modality modality, PartialRelationLiteral baseLiteral) { | ||
19 | super(modality, baseLiteral); | ||
20 | } | ||
21 | |||
22 | @Override | ||
23 | public ModalRelationLiteral substitute(Map<Variable, Variable> substitution) { | ||
24 | return new ModalRelationLiteral(getPolarity(), getModality(), getTarget(), substituteArguments(substitution)); | ||
25 | } | ||
26 | |||
27 | @Override | ||
28 | public ModalRelationLiteral negate() { | ||
29 | return new ModalRelationLiteral(getPolarity().negate(), getModality(), getTarget(), getArguments()); | ||
30 | } | ||
31 | } | ||
diff --git a/subprojects/store/src/main/java/tools/refinery/store/query/literal/Modality.java b/subprojects/store/src/main/java/tools/refinery/store/partial/literal/Modality.java index 93826161..d647ef0a 100644 --- a/subprojects/store/src/main/java/tools/refinery/store/query/literal/Modality.java +++ b/subprojects/store/src/main/java/tools/refinery/store/partial/literal/Modality.java | |||
@@ -1,4 +1,6 @@ | |||
1 | package tools.refinery.store.query.literal; | 1 | package tools.refinery.store.partial.literal; |
2 | |||
3 | import tools.refinery.store.query.literal.CallPolarity; | ||
2 | 4 | ||
3 | import java.util.Locale; | 5 | import java.util.Locale; |
4 | 6 | ||
@@ -15,6 +17,13 @@ public enum Modality { | |||
15 | }; | 17 | }; |
16 | } | 18 | } |
17 | 19 | ||
20 | public Modality commute(CallPolarity polarity) { | ||
21 | if (polarity.isPositive()) { | ||
22 | return this; | ||
23 | } | ||
24 | return this.negate(); | ||
25 | } | ||
26 | |||
18 | @Override | 27 | @Override |
19 | public String toString() { | 28 | public String toString() { |
20 | return name().toLowerCase(Locale.ROOT); | 29 | return name().toLowerCase(Locale.ROOT); |
diff --git a/subprojects/store/src/main/java/tools/refinery/store/partial/literal/PartialLiterals.java b/subprojects/store/src/main/java/tools/refinery/store/partial/literal/PartialLiterals.java new file mode 100644 index 00000000..51d388d3 --- /dev/null +++ b/subprojects/store/src/main/java/tools/refinery/store/partial/literal/PartialLiterals.java | |||
@@ -0,0 +1,33 @@ | |||
1 | package tools.refinery.store.partial.literal; | ||
2 | |||
3 | import tools.refinery.store.query.literal.DnfCallLiteral; | ||
4 | |||
5 | public final class PartialLiterals { | ||
6 | private PartialLiterals() { | ||
7 | throw new IllegalStateException("This is a static utility class and should not be instantiated directly"); | ||
8 | } | ||
9 | |||
10 | public ModalRelationLiteral may(PartialRelationLiteral literal) { | ||
11 | return new ModalRelationLiteral(Modality.MAY, literal); | ||
12 | } | ||
13 | |||
14 | public ModalRelationLiteral must(PartialRelationLiteral literal) { | ||
15 | return new ModalRelationLiteral(Modality.MUST, literal); | ||
16 | } | ||
17 | |||
18 | public ModalRelationLiteral current(PartialRelationLiteral literal) { | ||
19 | return new ModalRelationLiteral(Modality.CURRENT, literal); | ||
20 | } | ||
21 | |||
22 | public ModalDnfCallLiteral may(DnfCallLiteral literal) { | ||
23 | return new ModalDnfCallLiteral(Modality.MAY, literal); | ||
24 | } | ||
25 | |||
26 | public ModalDnfCallLiteral must(DnfCallLiteral literal) { | ||
27 | return new ModalDnfCallLiteral(Modality.MUST, literal); | ||
28 | } | ||
29 | |||
30 | public ModalDnfCallLiteral current(DnfCallLiteral literal) { | ||
31 | return new ModalDnfCallLiteral(Modality.CURRENT, literal); | ||
32 | } | ||
33 | } | ||
diff --git a/subprojects/store/src/main/java/tools/refinery/store/partial/literal/PartialRelationLiteral.java b/subprojects/store/src/main/java/tools/refinery/store/partial/literal/PartialRelationLiteral.java new file mode 100644 index 00000000..dc1a1da3 --- /dev/null +++ b/subprojects/store/src/main/java/tools/refinery/store/partial/literal/PartialRelationLiteral.java | |||
@@ -0,0 +1,27 @@ | |||
1 | package tools.refinery.store.partial.literal; | ||
2 | |||
3 | import tools.refinery.store.partial.representation.PartialRelation; | ||
4 | import tools.refinery.store.query.Variable; | ||
5 | import tools.refinery.store.query.literal.CallLiteral; | ||
6 | import tools.refinery.store.query.literal.CallPolarity; | ||
7 | import tools.refinery.store.query.literal.PolarLiteral; | ||
8 | |||
9 | import java.util.List; | ||
10 | import java.util.Map; | ||
11 | |||
12 | public final class PartialRelationLiteral extends CallLiteral<PartialRelation> | ||
13 | implements PolarLiteral<PartialRelationLiteral> { | ||
14 | public PartialRelationLiteral(CallPolarity polarity, PartialRelation target, List<Variable> substitution) { | ||
15 | super(polarity, target, substitution); | ||
16 | } | ||
17 | |||
18 | @Override | ||
19 | public PartialRelationLiteral substitute(Map<Variable, Variable> substitution) { | ||
20 | return new PartialRelationLiteral(getPolarity(), getTarget(), substituteArguments(substitution)); | ||
21 | } | ||
22 | |||
23 | @Override | ||
24 | public PartialRelationLiteral negate() { | ||
25 | return new PartialRelationLiteral(getPolarity().negate(), getTarget(), getArguments()); | ||
26 | } | ||
27 | } | ||
diff --git a/subprojects/store/src/main/java/tools/refinery/store/partial/representation/AnyPartialFunction.java b/subprojects/store/src/main/java/tools/refinery/store/partial/representation/AnyPartialFunction.java new file mode 100644 index 00000000..1113245e --- /dev/null +++ b/subprojects/store/src/main/java/tools/refinery/store/partial/representation/AnyPartialFunction.java | |||
@@ -0,0 +1,4 @@ | |||
1 | package tools.refinery.store.partial.representation; | ||
2 | |||
3 | public sealed interface AnyPartialFunction extends AnyPartialSymbol permits PartialFunction { | ||
4 | } | ||
diff --git a/subprojects/store/src/main/java/tools/refinery/store/partial/representation/AnyPartialSymbol.java b/subprojects/store/src/main/java/tools/refinery/store/partial/representation/AnyPartialSymbol.java new file mode 100644 index 00000000..25096e74 --- /dev/null +++ b/subprojects/store/src/main/java/tools/refinery/store/partial/representation/AnyPartialSymbol.java | |||
@@ -0,0 +1,11 @@ | |||
1 | package tools.refinery.store.partial.representation; | ||
2 | |||
3 | import tools.refinery.store.representation.AnyAbstractDomain; | ||
4 | |||
5 | public sealed interface AnyPartialSymbol permits AnyPartialFunction, PartialSymbol { | ||
6 | String name(); | ||
7 | |||
8 | int arity(); | ||
9 | |||
10 | AnyAbstractDomain abstractDomain(); | ||
11 | } | ||
diff --git a/subprojects/store/src/main/java/tools/refinery/store/partial/representation/PartialFunction.java b/subprojects/store/src/main/java/tools/refinery/store/partial/representation/PartialFunction.java new file mode 100644 index 00000000..3c186f6f --- /dev/null +++ b/subprojects/store/src/main/java/tools/refinery/store/partial/representation/PartialFunction.java | |||
@@ -0,0 +1,32 @@ | |||
1 | package tools.refinery.store.partial.representation; | ||
2 | |||
3 | import tools.refinery.store.representation.AbstractDomain; | ||
4 | |||
5 | public record PartialFunction<A, C>(String name, int arity, AbstractDomain<A, C> abstractDomain) | ||
6 | implements AnyPartialFunction, PartialSymbol<A, C> { | ||
7 | @Override | ||
8 | public A defaultValue() { | ||
9 | return null; | ||
10 | } | ||
11 | |||
12 | @Override | ||
13 | public C defaultConcreteValue() { | ||
14 | return null; | ||
15 | } | ||
16 | |||
17 | @Override | ||
18 | public boolean equals(Object o) { | ||
19 | return this == o; | ||
20 | } | ||
21 | |||
22 | @Override | ||
23 | public int hashCode() { | ||
24 | // Compare by identity to make hash table lookups more efficient. | ||
25 | return System.identityHashCode(this); | ||
26 | } | ||
27 | |||
28 | @Override | ||
29 | public String toString() { | ||
30 | return "%s/%d".formatted(name, arity); | ||
31 | } | ||
32 | } | ||
diff --git a/subprojects/store/src/main/java/tools/refinery/store/partial/representation/PartialRelation.java b/subprojects/store/src/main/java/tools/refinery/store/partial/representation/PartialRelation.java new file mode 100644 index 00000000..127355ca --- /dev/null +++ b/subprojects/store/src/main/java/tools/refinery/store/partial/representation/PartialRelation.java | |||
@@ -0,0 +1,66 @@ | |||
1 | package tools.refinery.store.partial.representation; | ||
2 | |||
3 | import tools.refinery.store.partial.literal.ModalRelationLiteral; | ||
4 | import tools.refinery.store.partial.literal.PartialRelationLiteral; | ||
5 | import tools.refinery.store.query.RelationLike; | ||
6 | import tools.refinery.store.query.Variable; | ||
7 | import tools.refinery.store.query.literal.CallPolarity; | ||
8 | import tools.refinery.store.partial.literal.Modality; | ||
9 | import tools.refinery.store.representation.AbstractDomain; | ||
10 | import tools.refinery.store.representation.TruthValue; | ||
11 | import tools.refinery.store.representation.TruthValueDomain; | ||
12 | |||
13 | import java.util.List; | ||
14 | |||
15 | public record PartialRelation(String name, int arity) implements PartialSymbol<TruthValue, Boolean>, RelationLike { | ||
16 | @Override | ||
17 | public AbstractDomain<TruthValue, Boolean> abstractDomain() { | ||
18 | return TruthValueDomain.INSTANCE; | ||
19 | } | ||
20 | |||
21 | @Override | ||
22 | public TruthValue defaultValue() { | ||
23 | return TruthValue.FALSE; | ||
24 | } | ||
25 | |||
26 | @Override | ||
27 | public Boolean defaultConcreteValue() { | ||
28 | return false; | ||
29 | } | ||
30 | |||
31 | public ModalRelationLiteral call(CallPolarity polarity, Modality modality, List<Variable> arguments) { | ||
32 | return new ModalRelationLiteral(polarity, modality, this, arguments); | ||
33 | } | ||
34 | |||
35 | public PartialRelationLiteral call(CallPolarity polarity, List<Variable> arguments) { | ||
36 | return new PartialRelationLiteral(polarity, this, arguments); | ||
37 | } | ||
38 | |||
39 | public PartialRelationLiteral call(CallPolarity polarity, Variable... arguments) { | ||
40 | return call(polarity, List.of(arguments)); | ||
41 | } | ||
42 | |||
43 | public PartialRelationLiteral call(Variable... arguments) { | ||
44 | return call(CallPolarity.POSITIVE, arguments); | ||
45 | } | ||
46 | |||
47 | public PartialRelationLiteral callTransitive(Variable left, Variable right) { | ||
48 | return call(CallPolarity.TRANSITIVE, List.of(left, right)); | ||
49 | } | ||
50 | |||
51 | @Override | ||
52 | public boolean equals(Object o) { | ||
53 | return this == o; | ||
54 | } | ||
55 | |||
56 | @Override | ||
57 | public int hashCode() { | ||
58 | // Compare by identity to make hash table lookups more efficient. | ||
59 | return System.identityHashCode(this); | ||
60 | } | ||
61 | |||
62 | @Override | ||
63 | public String toString() { | ||
64 | return "%s/%d".formatted(name, arity); | ||
65 | } | ||
66 | } | ||
diff --git a/subprojects/store/src/main/java/tools/refinery/store/partial/representation/PartialSymbol.java b/subprojects/store/src/main/java/tools/refinery/store/partial/representation/PartialSymbol.java new file mode 100644 index 00000000..38533fa9 --- /dev/null +++ b/subprojects/store/src/main/java/tools/refinery/store/partial/representation/PartialSymbol.java | |||
@@ -0,0 +1,12 @@ | |||
1 | package tools.refinery.store.partial.representation; | ||
2 | |||
3 | import tools.refinery.store.representation.AbstractDomain; | ||
4 | |||
5 | public sealed interface PartialSymbol<A, C> extends AnyPartialSymbol permits PartialFunction, PartialRelation { | ||
6 | @Override | ||
7 | AbstractDomain<A, C> abstractDomain(); | ||
8 | |||
9 | A defaultValue(); | ||
10 | |||
11 | C defaultConcreteValue(); | ||
12 | } | ||
diff --git a/subprojects/store/src/main/java/tools/refinery/store/query/Dnf.java b/subprojects/store/src/main/java/tools/refinery/store/query/Dnf.java index 1eb9ac76..b080094f 100644 --- a/subprojects/store/src/main/java/tools/refinery/store/query/Dnf.java +++ b/subprojects/store/src/main/java/tools/refinery/store/query/Dnf.java | |||
@@ -74,16 +74,16 @@ public final class Dnf implements RelationLike { | |||
74 | return clauses; | 74 | return clauses; |
75 | } | 75 | } |
76 | 76 | ||
77 | public DnfCallLiteral call(CallPolarity polarity, List<Variable> substitution) { | 77 | public DnfCallLiteral call(CallPolarity polarity, List<Variable> arguments) { |
78 | return new DnfCallLiteral(polarity, this, substitution); | 78 | return new DnfCallLiteral(polarity, this, arguments); |
79 | } | 79 | } |
80 | 80 | ||
81 | public DnfCallLiteral call(CallPolarity polarity, Variable... substitution) { | 81 | public DnfCallLiteral call(CallPolarity polarity, Variable... arguments) { |
82 | return call(polarity, List.of(substitution)); | 82 | return call(polarity, List.of(arguments)); |
83 | } | 83 | } |
84 | 84 | ||
85 | public DnfCallLiteral call(Variable... substitution) { | 85 | public DnfCallLiteral call(Variable... arguments) { |
86 | return call(CallPolarity.POSITIVE, substitution); | 86 | return call(CallPolarity.POSITIVE, arguments); |
87 | } | 87 | } |
88 | 88 | ||
89 | public DnfCallLiteral callTransitive(Variable left, Variable right) { | 89 | public DnfCallLiteral callTransitive(Variable left, Variable right) { |
diff --git a/subprojects/store/src/main/java/tools/refinery/store/query/DnfUtils.java b/subprojects/store/src/main/java/tools/refinery/store/query/DnfUtils.java index c7a2849c..17564d43 100644 --- a/subprojects/store/src/main/java/tools/refinery/store/query/DnfUtils.java +++ b/subprojects/store/src/main/java/tools/refinery/store/query/DnfUtils.java | |||
@@ -1,5 +1,6 @@ | |||
1 | package tools.refinery.store.query; | 1 | package tools.refinery.store.query; |
2 | 2 | ||
3 | import java.util.Map; | ||
3 | import java.util.UUID; | 4 | import java.util.UUID; |
4 | 5 | ||
5 | public final class DnfUtils { | 6 | public final class DnfUtils { |
@@ -16,4 +17,8 @@ public final class DnfUtils { | |||
16 | return originalName + uniqueString; | 17 | return originalName + uniqueString; |
17 | } | 18 | } |
18 | } | 19 | } |
20 | |||
21 | public static Variable maybeSubstitute(Variable variable, Map<Variable, Variable> substitution) { | ||
22 | return substitution.getOrDefault(variable, variable); | ||
23 | } | ||
19 | } | 24 | } |
diff --git a/subprojects/store/src/main/java/tools/refinery/store/query/literal/CallLiteral.java b/subprojects/store/src/main/java/tools/refinery/store/query/literal/CallLiteral.java index 59120434..5e1ae94d 100644 --- a/subprojects/store/src/main/java/tools/refinery/store/query/literal/CallLiteral.java +++ b/subprojects/store/src/main/java/tools/refinery/store/query/literal/CallLiteral.java | |||
@@ -1,28 +1,30 @@ | |||
1 | package tools.refinery.store.query.literal; | 1 | package tools.refinery.store.query.literal; |
2 | 2 | ||
3 | import tools.refinery.store.query.Variable; | 3 | import tools.refinery.store.query.DnfUtils; |
4 | import tools.refinery.store.query.RelationLike; | 4 | import tools.refinery.store.query.RelationLike; |
5 | import tools.refinery.store.query.Variable; | ||
5 | 6 | ||
6 | import java.util.List; | 7 | import java.util.List; |
8 | import java.util.Map; | ||
7 | import java.util.Objects; | 9 | import java.util.Objects; |
8 | import java.util.Set; | 10 | import java.util.Set; |
9 | 11 | ||
10 | public abstract class CallLiteral<T extends RelationLike> implements Literal { | 12 | public abstract class CallLiteral<T extends RelationLike> implements Literal { |
11 | private final CallPolarity polarity; | 13 | private final CallPolarity polarity; |
12 | private final T target; | 14 | private final T target; |
13 | private final List<Variable> substitution; | 15 | private final List<Variable> arguments; |
14 | 16 | ||
15 | protected CallLiteral(CallPolarity polarity, T target, List<Variable> substitution) { | 17 | protected CallLiteral(CallPolarity polarity, T target, List<Variable> arguments) { |
16 | if (substitution.size() != target.arity()) { | 18 | if (arguments.size() != target.arity()) { |
17 | throw new IllegalArgumentException("%s needs %d arguments, but got %s".formatted(target.name(), | 19 | throw new IllegalArgumentException("%s needs %d arguments, but got %s".formatted(target.name(), |
18 | target.arity(), substitution.size())); | 20 | target.arity(), arguments.size())); |
19 | } | 21 | } |
20 | if (polarity.isTransitive() && target.arity() != 2) { | 22 | if (polarity.isTransitive() && target.arity() != 2) { |
21 | throw new IllegalArgumentException("Transitive closures can only take binary relations"); | 23 | throw new IllegalArgumentException("Transitive closures can only take binary relations"); |
22 | } | 24 | } |
23 | this.polarity = polarity; | 25 | this.polarity = polarity; |
24 | this.target = target; | 26 | this.target = target; |
25 | this.substitution = substitution; | 27 | this.arguments = arguments; |
26 | } | 28 | } |
27 | 29 | ||
28 | public CallPolarity getPolarity() { | 30 | public CallPolarity getPolarity() { |
@@ -33,28 +35,32 @@ public abstract class CallLiteral<T extends RelationLike> implements Literal { | |||
33 | return target; | 35 | return target; |
34 | } | 36 | } |
35 | 37 | ||
36 | public List<Variable> getSubstitution() { | 38 | public List<Variable> getArguments() { |
37 | return substitution; | 39 | return arguments; |
38 | } | 40 | } |
39 | 41 | ||
40 | @Override | 42 | @Override |
41 | public void collectAllVariables(Set<Variable> variables) { | 43 | public void collectAllVariables(Set<Variable> variables) { |
42 | if (polarity.isPositive()) { | 44 | if (polarity.isPositive()) { |
43 | variables.addAll(substitution); | 45 | variables.addAll(arguments); |
44 | } | 46 | } |
45 | } | 47 | } |
46 | 48 | ||
49 | protected List<Variable> substituteArguments(Map<Variable, Variable> substitution) { | ||
50 | return arguments.stream().map(variable -> DnfUtils.maybeSubstitute(variable, substitution)).toList(); | ||
51 | } | ||
52 | |||
47 | @Override | 53 | @Override |
48 | public boolean equals(Object o) { | 54 | public boolean equals(Object o) { |
49 | if (this == o) return true; | 55 | if (this == o) return true; |
50 | if (o == null || getClass() != o.getClass()) return false; | 56 | if (o == null || getClass() != o.getClass()) return false; |
51 | CallLiteral<?> callAtom = (CallLiteral<?>) o; | 57 | CallLiteral<?> callAtom = (CallLiteral<?>) o; |
52 | return polarity == callAtom.polarity && Objects.equals(target, callAtom.target) && | 58 | return polarity == callAtom.polarity && Objects.equals(target, callAtom.target) && |
53 | Objects.equals(substitution, callAtom.substitution); | 59 | Objects.equals(arguments, callAtom.arguments); |
54 | } | 60 | } |
55 | 61 | ||
56 | @Override | 62 | @Override |
57 | public int hashCode() { | 63 | public int hashCode() { |
58 | return Objects.hash(polarity, target, substitution); | 64 | return Objects.hash(polarity, target, arguments); |
59 | } | 65 | } |
60 | } | 66 | } |
diff --git a/subprojects/store/src/main/java/tools/refinery/store/query/literal/ConstantLiteral.java b/subprojects/store/src/main/java/tools/refinery/store/query/literal/ConstantLiteral.java index 41426fdd..746d23af 100644 --- a/subprojects/store/src/main/java/tools/refinery/store/query/literal/ConstantLiteral.java +++ b/subprojects/store/src/main/java/tools/refinery/store/query/literal/ConstantLiteral.java | |||
@@ -1,7 +1,9 @@ | |||
1 | package tools.refinery.store.query.literal; | 1 | package tools.refinery.store.query.literal; |
2 | 2 | ||
3 | import tools.refinery.store.query.DnfUtils; | ||
3 | import tools.refinery.store.query.Variable; | 4 | import tools.refinery.store.query.Variable; |
4 | 5 | ||
6 | import java.util.Map; | ||
5 | import java.util.Set; | 7 | import java.util.Set; |
6 | 8 | ||
7 | public record ConstantLiteral(Variable variable, int nodeId) implements Literal { | 9 | public record ConstantLiteral(Variable variable, int nodeId) implements Literal { |
@@ -9,4 +11,9 @@ public record ConstantLiteral(Variable variable, int nodeId) implements Literal | |||
9 | public void collectAllVariables(Set<Variable> variables) { | 11 | public void collectAllVariables(Set<Variable> variables) { |
10 | variables.add(variable); | 12 | variables.add(variable); |
11 | } | 13 | } |
14 | |||
15 | @Override | ||
16 | public ConstantLiteral substitute(Map<Variable, Variable> substitution) { | ||
17 | return new ConstantLiteral(DnfUtils.maybeSubstitute(variable, substitution), nodeId); | ||
18 | } | ||
12 | } | 19 | } |
diff --git a/subprojects/store/src/main/java/tools/refinery/store/query/literal/DnfCallLiteral.java b/subprojects/store/src/main/java/tools/refinery/store/query/literal/DnfCallLiteral.java index 86149b33..40499222 100644 --- a/subprojects/store/src/main/java/tools/refinery/store/query/literal/DnfCallLiteral.java +++ b/subprojects/store/src/main/java/tools/refinery/store/query/literal/DnfCallLiteral.java | |||
@@ -4,14 +4,20 @@ import tools.refinery.store.query.Dnf; | |||
4 | import tools.refinery.store.query.Variable; | 4 | import tools.refinery.store.query.Variable; |
5 | 5 | ||
6 | import java.util.List; | 6 | import java.util.List; |
7 | import java.util.Map; | ||
7 | 8 | ||
8 | public final class DnfCallLiteral extends CallLiteral<Dnf> implements PolarLiteral<DnfCallLiteral> { | 9 | public final class DnfCallLiteral extends CallLiteral<Dnf> implements PolarLiteral<DnfCallLiteral> { |
9 | public DnfCallLiteral(CallPolarity polarity, Dnf target, List<Variable> substitution) { | 10 | public DnfCallLiteral(CallPolarity polarity, Dnf target, List<Variable> arguments) { |
10 | super(polarity, target, substitution); | 11 | super(polarity, target, arguments); |
12 | } | ||
13 | |||
14 | @Override | ||
15 | public DnfCallLiteral substitute(Map<Variable, Variable> substitution) { | ||
16 | return new DnfCallLiteral(getPolarity(), getTarget(), substituteArguments(substitution)); | ||
11 | } | 17 | } |
12 | 18 | ||
13 | @Override | 19 | @Override |
14 | public DnfCallLiteral negate() { | 20 | public DnfCallLiteral negate() { |
15 | return new DnfCallLiteral(getPolarity().negate(), getTarget(), getSubstitution()); | 21 | return new DnfCallLiteral(getPolarity().negate(), getTarget(), getArguments()); |
16 | } | 22 | } |
17 | } | 23 | } |
diff --git a/subprojects/store/src/main/java/tools/refinery/store/query/literal/EquivalenceLiteral.java b/subprojects/store/src/main/java/tools/refinery/store/query/literal/EquivalenceLiteral.java index 75afd50b..5fee54b1 100644 --- a/subprojects/store/src/main/java/tools/refinery/store/query/literal/EquivalenceLiteral.java +++ b/subprojects/store/src/main/java/tools/refinery/store/query/literal/EquivalenceLiteral.java | |||
@@ -1,7 +1,9 @@ | |||
1 | package tools.refinery.store.query.literal; | 1 | package tools.refinery.store.query.literal; |
2 | 2 | ||
3 | import tools.refinery.store.query.DnfUtils; | ||
3 | import tools.refinery.store.query.Variable; | 4 | import tools.refinery.store.query.Variable; |
4 | 5 | ||
6 | import java.util.Map; | ||
5 | import java.util.Set; | 7 | import java.util.Set; |
6 | 8 | ||
7 | public record EquivalenceLiteral(boolean positive, Variable left, Variable right) | 9 | public record EquivalenceLiteral(boolean positive, Variable left, Variable right) |
@@ -16,4 +18,10 @@ public record EquivalenceLiteral(boolean positive, Variable left, Variable right | |||
16 | public EquivalenceLiteral negate() { | 18 | public EquivalenceLiteral negate() { |
17 | return new EquivalenceLiteral(!positive, left, right); | 19 | return new EquivalenceLiteral(!positive, left, right); |
18 | } | 20 | } |
21 | |||
22 | @Override | ||
23 | public EquivalenceLiteral substitute(Map<Variable, Variable> substitution) { | ||
24 | return new EquivalenceLiteral(positive, DnfUtils.maybeSubstitute(left, substitution), | ||
25 | DnfUtils.maybeSubstitute(right, substitution)); | ||
26 | } | ||
19 | } | 27 | } |
diff --git a/subprojects/store/src/main/java/tools/refinery/store/query/literal/Literal.java b/subprojects/store/src/main/java/tools/refinery/store/query/literal/Literal.java index 676ac7fd..e0f5f605 100644 --- a/subprojects/store/src/main/java/tools/refinery/store/query/literal/Literal.java +++ b/subprojects/store/src/main/java/tools/refinery/store/query/literal/Literal.java | |||
@@ -2,8 +2,11 @@ package tools.refinery.store.query.literal; | |||
2 | 2 | ||
3 | import tools.refinery.store.query.Variable; | 3 | import tools.refinery.store.query.Variable; |
4 | 4 | ||
5 | import java.util.Map; | ||
5 | import java.util.Set; | 6 | import java.util.Set; |
6 | 7 | ||
7 | public interface Literal { | 8 | public interface Literal { |
8 | void collectAllVariables(Set<Variable> variables); | 9 | void collectAllVariables(Set<Variable> variables); |
10 | |||
11 | Literal substitute(Map<Variable, Variable> substitution); | ||
9 | } | 12 | } |
diff --git a/subprojects/store/src/main/java/tools/refinery/store/query/literal/RelationViewLiteral.java b/subprojects/store/src/main/java/tools/refinery/store/query/literal/RelationViewLiteral.java index 7fa99abb..4718b550 100644 --- a/subprojects/store/src/main/java/tools/refinery/store/query/literal/RelationViewLiteral.java +++ b/subprojects/store/src/main/java/tools/refinery/store/query/literal/RelationViewLiteral.java | |||
@@ -4,15 +4,21 @@ import tools.refinery.store.query.Variable; | |||
4 | import tools.refinery.store.query.view.AnyRelationView; | 4 | import tools.refinery.store.query.view.AnyRelationView; |
5 | 5 | ||
6 | import java.util.List; | 6 | import java.util.List; |
7 | import java.util.Map; | ||
7 | 8 | ||
8 | public final class RelationViewLiteral extends CallLiteral<AnyRelationView> | 9 | public final class RelationViewLiteral extends CallLiteral<AnyRelationView> |
9 | implements PolarLiteral<RelationViewLiteral> { | 10 | implements PolarLiteral<RelationViewLiteral> { |
10 | public RelationViewLiteral(CallPolarity polarity, AnyRelationView target, List<Variable> substitution) { | 11 | public RelationViewLiteral(CallPolarity polarity, AnyRelationView target, List<Variable> arguments) { |
11 | super(polarity, target, substitution); | 12 | super(polarity, target, arguments); |
13 | } | ||
14 | |||
15 | @Override | ||
16 | public RelationViewLiteral substitute(Map<Variable, Variable> substitution) { | ||
17 | return new RelationViewLiteral(getPolarity(), getTarget(), substituteArguments(substitution)); | ||
12 | } | 18 | } |
13 | 19 | ||
14 | @Override | 20 | @Override |
15 | public RelationViewLiteral negate() { | 21 | public RelationViewLiteral negate() { |
16 | return new RelationViewLiteral(getPolarity().negate(), getTarget(), getSubstitution()); | 22 | return new RelationViewLiteral(getPolarity().negate(), getTarget(), getArguments()); |
17 | } | 23 | } |
18 | } | 24 | } |
diff --git a/subprojects/store/src/main/java/tools/refinery/store/query/view/RelationView.java b/subprojects/store/src/main/java/tools/refinery/store/query/view/RelationView.java index 0bea962d..6accd27a 100644 --- a/subprojects/store/src/main/java/tools/refinery/store/query/view/RelationView.java +++ b/subprojects/store/src/main/java/tools/refinery/store/query/view/RelationView.java | |||
@@ -51,16 +51,16 @@ public abstract non-sealed class RelationView<T> implements AnyRelationView { | |||
51 | return (() -> new CursorAsIterator<>(model.getInterpretation(symbol).getAll(), this::forwardMap, this::filter)); | 51 | return (() -> new CursorAsIterator<>(model.getInterpretation(symbol).getAll(), this::forwardMap, this::filter)); |
52 | } | 52 | } |
53 | 53 | ||
54 | public RelationViewLiteral call(CallPolarity polarity, List<Variable> substitution) { | 54 | public RelationViewLiteral call(CallPolarity polarity, List<Variable> arguments) { |
55 | return new RelationViewLiteral(polarity, this, substitution); | 55 | return new RelationViewLiteral(polarity, this, arguments); |
56 | } | 56 | } |
57 | 57 | ||
58 | public RelationViewLiteral call(CallPolarity polarity, Variable... substitution) { | 58 | public RelationViewLiteral call(CallPolarity polarity, Variable... arguments) { |
59 | return call(polarity, List.of(substitution)); | 59 | return call(polarity, List.of(arguments)); |
60 | } | 60 | } |
61 | 61 | ||
62 | public RelationViewLiteral call(Variable... substitution) { | 62 | public RelationViewLiteral call(Variable... arguments) { |
63 | return call(CallPolarity.POSITIVE, substitution); | 63 | return call(CallPolarity.POSITIVE, arguments); |
64 | } | 64 | } |
65 | 65 | ||
66 | public RelationViewLiteral callTransitive(Variable left, Variable right) { | 66 | public RelationViewLiteral callTransitive(Variable left, Variable right) { |
diff --git a/subprojects/store/src/main/java/tools/refinery/store/representation/AbstractDomain.java b/subprojects/store/src/main/java/tools/refinery/store/representation/AbstractDomain.java new file mode 100644 index 00000000..18903ead --- /dev/null +++ b/subprojects/store/src/main/java/tools/refinery/store/representation/AbstractDomain.java | |||
@@ -0,0 +1,29 @@ | |||
1 | package tools.refinery.store.representation; | ||
2 | |||
3 | import java.util.Optional; | ||
4 | |||
5 | public non-sealed interface AbstractDomain<A, C> extends AnyAbstractDomain { | ||
6 | @Override | ||
7 | Class<A> abstractType(); | ||
8 | |||
9 | @Override | ||
10 | Class<C> concreteType(); | ||
11 | |||
12 | A toAbstract(C concreteValue); | ||
13 | |||
14 | Optional<C> toConcrete(A abstractValue); | ||
15 | |||
16 | default boolean isConcrete(A abstractValue) { | ||
17 | return toConcrete(abstractValue).isPresent(); | ||
18 | } | ||
19 | |||
20 | boolean isRefinement(A originalValue, A refinedValue); | ||
21 | |||
22 | A commonRefinement(A leftValue, A rightValue); | ||
23 | |||
24 | A commonAncestor(A leftValue, A rightValue); | ||
25 | |||
26 | A unknown(); | ||
27 | |||
28 | boolean isError(A abstractValue); | ||
29 | } | ||
diff --git a/subprojects/store/src/main/java/tools/refinery/store/representation/AnyAbstractDomain.java b/subprojects/store/src/main/java/tools/refinery/store/representation/AnyAbstractDomain.java new file mode 100644 index 00000000..4c428a1e --- /dev/null +++ b/subprojects/store/src/main/java/tools/refinery/store/representation/AnyAbstractDomain.java | |||
@@ -0,0 +1,7 @@ | |||
1 | package tools.refinery.store.representation; | ||
2 | |||
3 | public sealed interface AnyAbstractDomain permits AbstractDomain { | ||
4 | Class<?> abstractType(); | ||
5 | |||
6 | Class<?> concreteType(); | ||
7 | } | ||
diff --git a/subprojects/store/src/main/java/tools/refinery/store/representation/TruthValueDomain.java b/subprojects/store/src/main/java/tools/refinery/store/representation/TruthValueDomain.java new file mode 100644 index 00000000..29858bce --- /dev/null +++ b/subprojects/store/src/main/java/tools/refinery/store/representation/TruthValueDomain.java | |||
@@ -0,0 +1,60 @@ | |||
1 | package tools.refinery.store.representation; | ||
2 | |||
3 | import java.util.Optional; | ||
4 | |||
5 | public final class TruthValueDomain implements AbstractDomain<TruthValue, Boolean> { | ||
6 | public static final TruthValueDomain INSTANCE = new TruthValueDomain(); | ||
7 | |||
8 | private TruthValueDomain() { | ||
9 | } | ||
10 | |||
11 | @Override | ||
12 | public Class<TruthValue> abstractType() { | ||
13 | return null; | ||
14 | } | ||
15 | |||
16 | @Override | ||
17 | public Class<Boolean> concreteType() { | ||
18 | return null; | ||
19 | } | ||
20 | |||
21 | @Override | ||
22 | public TruthValue toAbstract(Boolean concreteValue) { | ||
23 | return null; | ||
24 | } | ||
25 | |||
26 | @Override | ||
27 | public Optional<Boolean> toConcrete(TruthValue abstractValue) { | ||
28 | return Optional.empty(); | ||
29 | } | ||
30 | |||
31 | @Override | ||
32 | public boolean isConcrete(TruthValue abstractValue) { | ||
33 | return AbstractDomain.super.isConcrete(abstractValue); | ||
34 | } | ||
35 | |||
36 | @Override | ||
37 | public boolean isRefinement(TruthValue originalValue, TruthValue refinedValue) { | ||
38 | return false; | ||
39 | } | ||
40 | |||
41 | @Override | ||
42 | public TruthValue commonRefinement(TruthValue leftValue, TruthValue rightValue) { | ||
43 | return null; | ||
44 | } | ||
45 | |||
46 | @Override | ||
47 | public TruthValue commonAncestor(TruthValue leftValue, TruthValue rightValue) { | ||
48 | return null; | ||
49 | } | ||
50 | |||
51 | @Override | ||
52 | public TruthValue unknown() { | ||
53 | return null; | ||
54 | } | ||
55 | |||
56 | @Override | ||
57 | public boolean isError(TruthValue abstractValue) { | ||
58 | return false; | ||
59 | } | ||
60 | } | ||
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 new file mode 100644 index 00000000..e4b462f0 --- /dev/null +++ b/subprojects/store/src/main/java/tools/refinery/store/util/CycleDetectingMapper.java | |||
@@ -0,0 +1,51 @@ | |||
1 | package tools.refinery.store.util; | ||
2 | |||
3 | import java.util.HashMap; | ||
4 | import java.util.LinkedHashSet; | ||
5 | import java.util.Map; | ||
6 | import java.util.Set; | ||
7 | import java.util.function.Function; | ||
8 | import java.util.stream.Collectors; | ||
9 | |||
10 | public class CycleDetectingMapper<T, R> { | ||
11 | private static final String SEPARATOR = " -> "; | ||
12 | |||
13 | private final Function<T, String> getName; | ||
14 | |||
15 | private final Function<T, R> doMap; | ||
16 | |||
17 | private final Set<T> inProgress = new LinkedHashSet<>(); | ||
18 | |||
19 | private final Map<T, R> results = new HashMap<>(); | ||
20 | |||
21 | public CycleDetectingMapper(Function<T, String> getName, Function<T, R> doMap) { | ||
22 | this.getName = getName; | ||
23 | this.doMap = doMap; | ||
24 | } | ||
25 | |||
26 | public R map(T input) { | ||
27 | if (inProgress.contains(input)) { | ||
28 | var path = inProgress.stream().map(getName).collect(Collectors.joining(SEPARATOR)); | ||
29 | throw new IllegalArgumentException("Circular reference %s%s%s detected".formatted(path, SEPARATOR, | ||
30 | getName.apply(input))); | ||
31 | } | ||
32 | // We can't use computeIfAbsent here, because translating referenced queries calls this method in a reentrant | ||
33 | // way, which would cause a ConcurrentModificationException with computeIfAbsent. | ||
34 | @SuppressWarnings("squid:S3824") | ||
35 | var result = results.get(input); | ||
36 | if (result == null) { | ||
37 | inProgress.add(input); | ||
38 | try { | ||
39 | result = doMap.apply(input); | ||
40 | results.put(input, result); | ||
41 | } finally { | ||
42 | inProgress.remove(input); | ||
43 | } | ||
44 | } | ||
45 | return result; | ||
46 | } | ||
47 | |||
48 | public R getAlreadyMapped(T input) { | ||
49 | return results.get(input); | ||
50 | } | ||
51 | } | ||