diff options
author | Kristóf Marussy <kristof@marussy.com> | 2023-03-07 16:26:26 +0100 |
---|---|---|
committer | Kristóf Marussy <kristof@marussy.com> | 2023-03-31 15:38:59 +0200 |
commit | 372058e54825ab58a66c25ae528e81a656c22659 (patch) | |
tree | 3686057057ebcad2faae7233dc691ecacc3e9fe2 /subprojects/store-reasoning/src/main/java | |
parent | refactor: use Cursor in query result sets (diff) | |
download | refinery-372058e54825ab58a66c25ae528e81a656c22659.tar.gz refinery-372058e54825ab58a66c25ae528e81a656c22659.tar.zst refinery-372058e54825ab58a66c25ae528e81a656c22659.zip |
feat: terms and improved query evaluation
* Implement data terms for computations in queries.
* Function-like queries with computed results.
* Improved query evaluation, including positive and negative diagonal
cosntraints.
* Preliminary local search support.
* Changes to the DNF representation for count and aggregation support.
feat: terms wip
feat: query terms wip
feat: query evaluation, diagonal constraints, local search wip
fix reasoning compilation wip
Diffstat (limited to 'subprojects/store-reasoning/src/main/java')
28 files changed, 371 insertions, 316 deletions
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/PartialInterpretation.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/PartialInterpretation.java index 99656da8..4f195e97 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/PartialInterpretation.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/PartialInterpretation.java | |||
@@ -12,8 +12,6 @@ public non-sealed interface PartialInterpretation<A, C> extends AnyPartialInterp | |||
12 | 12 | ||
13 | Cursor<Tuple, A> getAll(); | 13 | Cursor<Tuple, A> getAll(); |
14 | 14 | ||
15 | Cursor<Tuple, A> getAllErrors(); | ||
16 | |||
17 | MergeResult merge(Tuple key, A value); | 15 | MergeResult merge(Tuple key, A value); |
18 | 16 | ||
19 | C getConcrete(Tuple key); | 17 | C getConcrete(Tuple key); |
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 e602242e..de039dd9 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 | |||
@@ -3,7 +3,7 @@ package tools.refinery.store.reasoning; | |||
3 | import tools.refinery.store.adapter.ModelAdapter; | 3 | import tools.refinery.store.adapter.ModelAdapter; |
4 | import tools.refinery.store.reasoning.representation.AnyPartialSymbol; | 4 | import tools.refinery.store.reasoning.representation.AnyPartialSymbol; |
5 | import tools.refinery.store.reasoning.representation.PartialSymbol; | 5 | import tools.refinery.store.reasoning.representation.PartialSymbol; |
6 | import tools.refinery.store.query.Dnf; | 6 | import tools.refinery.store.query.dnf.Dnf; |
7 | import tools.refinery.store.query.ResultSet; | 7 | import tools.refinery.store.query.ResultSet; |
8 | 8 | ||
9 | public interface ReasoningAdapter extends ModelAdapter { | 9 | public interface ReasoningAdapter extends ModelAdapter { |
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/ReasoningBuilder.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/ReasoningBuilder.java index 588c2711..4030d296 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/ReasoningBuilder.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/ReasoningBuilder.java | |||
@@ -3,7 +3,7 @@ package tools.refinery.store.reasoning; | |||
3 | import tools.refinery.store.adapter.ModelAdapterBuilder; | 3 | import tools.refinery.store.adapter.ModelAdapterBuilder; |
4 | import tools.refinery.store.model.ModelStore; | 4 | import tools.refinery.store.model.ModelStore; |
5 | import tools.refinery.store.reasoning.literal.Modality; | 5 | import tools.refinery.store.reasoning.literal.Modality; |
6 | import tools.refinery.store.query.Dnf; | 6 | import tools.refinery.store.query.dnf.Dnf; |
7 | 7 | ||
8 | import java.util.Collection; | 8 | import java.util.Collection; |
9 | import java.util.List; | 9 | import java.util.List; |
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/ReasoningStoreAdapter.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/ReasoningStoreAdapter.java index 69c0f5eb..f6a6e414 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/ReasoningStoreAdapter.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/ReasoningStoreAdapter.java | |||
@@ -3,7 +3,7 @@ package tools.refinery.store.reasoning; | |||
3 | import tools.refinery.store.adapter.ModelStoreAdapter; | 3 | import tools.refinery.store.adapter.ModelStoreAdapter; |
4 | import tools.refinery.store.model.Model; | 4 | import tools.refinery.store.model.Model; |
5 | import tools.refinery.store.reasoning.representation.AnyPartialSymbol; | 5 | import tools.refinery.store.reasoning.representation.AnyPartialSymbol; |
6 | import tools.refinery.store.query.Dnf; | 6 | import tools.refinery.store.query.dnf.Dnf; |
7 | 7 | ||
8 | import java.util.Collection; | 8 | import java.util.Collection; |
9 | 9 | ||
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/internal/ReasoningAdapterImpl.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/internal/ReasoningAdapterImpl.java index a7a56680..0acf0d49 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/internal/ReasoningAdapterImpl.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/internal/ReasoningAdapterImpl.java | |||
@@ -4,7 +4,7 @@ import tools.refinery.store.model.Model; | |||
4 | import tools.refinery.store.reasoning.ReasoningAdapter; | 4 | import tools.refinery.store.reasoning.ReasoningAdapter; |
5 | import tools.refinery.store.reasoning.PartialInterpretation; | 5 | import tools.refinery.store.reasoning.PartialInterpretation; |
6 | import tools.refinery.store.reasoning.representation.PartialSymbol; | 6 | import tools.refinery.store.reasoning.representation.PartialSymbol; |
7 | import tools.refinery.store.query.Dnf; | 7 | import tools.refinery.store.query.dnf.Dnf; |
8 | import tools.refinery.store.query.ResultSet; | 8 | import tools.refinery.store.query.ResultSet; |
9 | 9 | ||
10 | public class ReasoningAdapterImpl implements ReasoningAdapter { | 10 | public class ReasoningAdapterImpl implements ReasoningAdapter { |
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/internal/ReasoningBuilderImpl.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/internal/ReasoningBuilderImpl.java index 2860e2b9..e11b14bf 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/internal/ReasoningBuilderImpl.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/internal/ReasoningBuilderImpl.java | |||
@@ -5,7 +5,7 @@ import tools.refinery.store.model.ModelStore; | |||
5 | import tools.refinery.store.model.ModelStoreBuilder; | 5 | import tools.refinery.store.model.ModelStoreBuilder; |
6 | import tools.refinery.store.reasoning.ReasoningBuilder; | 6 | import tools.refinery.store.reasoning.ReasoningBuilder; |
7 | import tools.refinery.store.reasoning.literal.Modality; | 7 | import tools.refinery.store.reasoning.literal.Modality; |
8 | import tools.refinery.store.query.Dnf; | 8 | import tools.refinery.store.query.dnf.Dnf; |
9 | 9 | ||
10 | public class ReasoningBuilderImpl extends AbstractModelAdapterBuilder implements ReasoningBuilder { | 10 | public class ReasoningBuilderImpl extends AbstractModelAdapterBuilder implements ReasoningBuilder { |
11 | public ReasoningBuilderImpl(ModelStoreBuilder storeBuilder) { | 11 | public ReasoningBuilderImpl(ModelStoreBuilder storeBuilder) { |
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/internal/ReasoningStoreAdapterImpl.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/internal/ReasoningStoreAdapterImpl.java index 763dad6d..ac06e68b 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/internal/ReasoningStoreAdapterImpl.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/internal/ReasoningStoreAdapterImpl.java | |||
@@ -4,7 +4,7 @@ import tools.refinery.store.reasoning.ReasoningStoreAdapter; | |||
4 | import tools.refinery.store.model.Model; | 4 | import tools.refinery.store.model.Model; |
5 | import tools.refinery.store.model.ModelStore; | 5 | import tools.refinery.store.model.ModelStore; |
6 | import tools.refinery.store.reasoning.representation.AnyPartialSymbol; | 6 | import tools.refinery.store.reasoning.representation.AnyPartialSymbol; |
7 | import tools.refinery.store.query.Dnf; | 7 | import tools.refinery.store.query.dnf.Dnf; |
8 | 8 | ||
9 | import java.util.Collection; | 9 | import java.util.Collection; |
10 | 10 | ||
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 966e080a..2b0e0f08 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 | |||
@@ -1,18 +1,18 @@ | |||
1 | package tools.refinery.store.reasoning.lifting; | 1 | package tools.refinery.store.reasoning.lifting; |
2 | 2 | ||
3 | import org.jetbrains.annotations.Nullable; | 3 | import org.jetbrains.annotations.Nullable; |
4 | import tools.refinery.store.reasoning.literal.ModalDnfCallLiteral; | 4 | import tools.refinery.store.query.dnf.Dnf; |
5 | import tools.refinery.store.reasoning.Reasoning; | 5 | import tools.refinery.store.query.dnf.DnfBuilder; |
6 | import tools.refinery.store.reasoning.literal.ModalRelationLiteral; | 6 | import tools.refinery.store.query.dnf.DnfClause; |
7 | import tools.refinery.store.reasoning.literal.PartialRelationLiteral; | 7 | import tools.refinery.store.query.literal.CallLiteral; |
8 | import tools.refinery.store.query.Dnf; | ||
9 | import tools.refinery.store.query.DnfBuilder; | ||
10 | import tools.refinery.store.query.DnfClause; | ||
11 | import tools.refinery.store.query.Variable; | ||
12 | import tools.refinery.store.query.literal.CallPolarity; | 8 | import tools.refinery.store.query.literal.CallPolarity; |
13 | import tools.refinery.store.query.literal.DnfCallLiteral; | ||
14 | import tools.refinery.store.query.literal.Literal; | 9 | import tools.refinery.store.query.literal.Literal; |
10 | import tools.refinery.store.query.term.DataVariable; | ||
11 | import tools.refinery.store.query.term.Variable; | ||
12 | import tools.refinery.store.reasoning.Reasoning; | ||
13 | import tools.refinery.store.reasoning.literal.ModalConstraint; | ||
15 | import tools.refinery.store.reasoning.literal.Modality; | 14 | import tools.refinery.store.reasoning.literal.Modality; |
15 | import tools.refinery.store.reasoning.literal.PartialLiterals; | ||
16 | import tools.refinery.store.util.CycleDetectingMapper; | 16 | import tools.refinery.store.util.CycleDetectingMapper; |
17 | 17 | ||
18 | import java.util.ArrayList; | 18 | import java.util.ArrayList; |
@@ -46,7 +46,10 @@ public class DnfLifter { | |||
46 | 46 | ||
47 | private boolean liftClause(Modality modality, DnfClause clause, DnfBuilder builder) { | 47 | private boolean liftClause(Modality modality, DnfClause clause, DnfBuilder builder) { |
48 | boolean changed = false; | 48 | boolean changed = false; |
49 | var quantifiedVariables = new HashSet<>(clause.quantifiedVariables()); | 49 | var quantifiedVariables = new HashSet<>(clause.boundVariables() |
50 | .stream() | ||
51 | .filter(DataVariable.class::isInstance) | ||
52 | .toList()); | ||
50 | var literals = clause.literals(); | 53 | var literals = clause.literals(); |
51 | var liftedLiterals = new ArrayList<Literal>(literals.size()); | 54 | var liftedLiterals = new ArrayList<Literal>(literals.size()); |
52 | for (var literal : literals) { | 55 | for (var literal : literals) { |
@@ -65,8 +68,8 @@ public class DnfLifter { | |||
65 | } | 68 | } |
66 | } | 69 | } |
67 | for (var quantifiedVariable : quantifiedVariables) { | 70 | for (var quantifiedVariable : quantifiedVariables) { |
68 | // Quantify over variables that are not already quantified with the expected modality. | 71 | // Quantify over data variables that are not already quantified with the expected modality. |
69 | liftedLiterals.add(Reasoning.EXISTS.call(CallPolarity.POSITIVE, modality, | 72 | liftedLiterals.add(new CallLiteral(CallPolarity.POSITIVE, new ModalConstraint(modality, Reasoning.EXISTS), |
70 | List.of(quantifiedVariable))); | 73 | List.of(quantifiedVariable))); |
71 | } | 74 | } |
72 | builder.clause(liftedLiterals); | 75 | builder.clause(liftedLiterals); |
@@ -75,33 +78,39 @@ public class DnfLifter { | |||
75 | 78 | ||
76 | @Nullable | 79 | @Nullable |
77 | private Variable isExistsLiteralForVariable(Modality modality, Literal literal) { | 80 | private Variable isExistsLiteralForVariable(Modality modality, Literal literal) { |
78 | if (literal instanceof ModalRelationLiteral modalRelationLiteral && | 81 | if (literal instanceof CallLiteral callLiteral && |
79 | modalRelationLiteral.getPolarity() == CallPolarity.POSITIVE && | 82 | callLiteral.getPolarity() == CallPolarity.POSITIVE && |
80 | modalRelationLiteral.getModality() == modality && | 83 | callLiteral.getTarget() instanceof ModalConstraint modalConstraint && |
81 | modalRelationLiteral.getTarget().equals(Reasoning.EXISTS)) { | 84 | modalConstraint.modality() == modality && |
82 | return modalRelationLiteral.getArguments().get(0); | 85 | modalConstraint.constraint().equals(Reasoning.EXISTS)) { |
86 | return callLiteral.getArguments().get(0); | ||
83 | } | 87 | } |
84 | return null; | 88 | return null; |
85 | } | 89 | } |
86 | 90 | ||
87 | @Nullable | 91 | @Nullable |
88 | private Literal liftLiteral(Modality modality, Literal literal) { | 92 | private Literal liftLiteral(Modality modality, Literal literal) { |
89 | if (literal instanceof PartialRelationLiteral partialRelationLiteral) { | 93 | if (!(literal instanceof CallLiteral callLiteral)) { |
90 | return new ModalRelationLiteral(modality, partialRelationLiteral); | 94 | return null; |
91 | } else if (literal instanceof DnfCallLiteral dnfCallLiteral) { | 95 | } |
92 | var polarity = dnfCallLiteral.getPolarity(); | 96 | var target = callLiteral.getTarget(); |
93 | var target = dnfCallLiteral.getTarget(); | 97 | if (target instanceof ModalConstraint modalTarget) { |
94 | var liftedTarget = lift(modality.commute(polarity), target); | 98 | var actualTarget = modalTarget.constraint(); |
95 | if (target.equals(liftedTarget)) { | 99 | if (actualTarget instanceof Dnf dnf) { |
96 | return null; | 100 | var targetModality = modalTarget.modality(); |
101 | var liftedTarget = lift(targetModality, dnf); | ||
102 | return new CallLiteral(callLiteral.getPolarity(), liftedTarget, callLiteral.getArguments()); | ||
97 | } | 103 | } |
98 | return new DnfCallLiteral(polarity, liftedTarget, dnfCallLiteral.getArguments()); | 104 | // No more lifting to be done, pass any modal call to a partial symbol through. |
99 | } else if (literal instanceof ModalDnfCallLiteral modalDnfCallLiteral) { | ||
100 | var liftedTarget = lift(modalDnfCallLiteral.getModality(), modalDnfCallLiteral.getTarget()); | ||
101 | return new DnfCallLiteral(modalDnfCallLiteral.getPolarity(), liftedTarget, | ||
102 | modalDnfCallLiteral.getArguments()); | ||
103 | } else { | ||
104 | return null; | 105 | return null; |
106 | } else if (target instanceof Dnf dnf) { | ||
107 | var polarity = callLiteral.getPolarity(); | ||
108 | var liftedTarget = lift(modality.commute(polarity), dnf); | ||
109 | // Use == instead of equals(), because lift will return the same object by reference is there are no | ||
110 | // changes made during lifting. | ||
111 | return liftedTarget == target ? null : new CallLiteral(polarity, liftedTarget, callLiteral.getArguments()); | ||
112 | } else { | ||
113 | return PartialLiterals.addModality(callLiteral, modality); | ||
105 | } | 114 | } |
106 | } | 115 | } |
107 | } | 116 | } |
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 index 7aa98bf2..ec381bb8 100644 --- 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 | |||
@@ -1,9 +1,9 @@ | |||
1 | package tools.refinery.store.reasoning.lifting; | 1 | package tools.refinery.store.reasoning.lifting; |
2 | 2 | ||
3 | import tools.refinery.store.query.Dnf; | 3 | import tools.refinery.store.query.dnf.Dnf; |
4 | import tools.refinery.store.reasoning.literal.Modality; | 4 | import tools.refinery.store.reasoning.literal.Modality; |
5 | 5 | ||
6 | public record ModalDnf(Modality modality, Dnf dnf) { | 6 | record ModalDnf(Modality modality, Dnf dnf) { |
7 | @Override | 7 | @Override |
8 | public String toString() { | 8 | public String toString() { |
9 | return "%s %s".formatted(modality, dnf.name()); | 9 | return "%s %s".formatted(modality, dnf.name()); |
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 new file mode 100644 index 00000000..2fbb4607 --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/literal/ModalConstraint.java | |||
@@ -0,0 +1,46 @@ | |||
1 | package tools.refinery.store.reasoning.literal; | ||
2 | |||
3 | import tools.refinery.store.query.Constraint; | ||
4 | import tools.refinery.store.query.equality.LiteralEqualityHelper; | ||
5 | import tools.refinery.store.query.literal.LiteralReduction; | ||
6 | import tools.refinery.store.query.term.Sort; | ||
7 | |||
8 | import java.util.List; | ||
9 | |||
10 | public record ModalConstraint(Modality modality, Constraint constraint) implements Constraint { | ||
11 | private static final String FORMAT = "%s %s"; | ||
12 | |||
13 | @Override | ||
14 | public String name() { | ||
15 | return FORMAT.formatted(modality, constraint.name()); | ||
16 | } | ||
17 | |||
18 | @Override | ||
19 | public List<Sort> getSorts() { | ||
20 | return constraint.getSorts(); | ||
21 | } | ||
22 | |||
23 | @Override | ||
24 | public LiteralReduction getReduction() { | ||
25 | return constraint.getReduction(); | ||
26 | } | ||
27 | |||
28 | @Override | ||
29 | public boolean equals(LiteralEqualityHelper helper, Constraint other) { | ||
30 | if (getClass() != other.getClass()) { | ||
31 | return false; | ||
32 | } | ||
33 | var otherModalConstraint = (ModalConstraint) other; | ||
34 | return modality == otherModalConstraint.modality && constraint.equals(helper, otherModalConstraint.constraint); | ||
35 | } | ||
36 | |||
37 | @Override | ||
38 | public String toReferenceString() { | ||
39 | return FORMAT.formatted(modality, constraint.toReferenceString()); | ||
40 | } | ||
41 | |||
42 | @Override | ||
43 | public String toString() { | ||
44 | return FORMAT.formatted(modality, constraint); | ||
45 | } | ||
46 | } | ||
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/literal/ModalDnfCallLiteral.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/literal/ModalDnfCallLiteral.java deleted file mode 100644 index 1090f1ae..00000000 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/literal/ModalDnfCallLiteral.java +++ /dev/null | |||
@@ -1,48 +0,0 @@ | |||
1 | package tools.refinery.store.reasoning.literal; | ||
2 | |||
3 | import tools.refinery.store.query.Dnf; | ||
4 | import tools.refinery.store.query.Variable; | ||
5 | import tools.refinery.store.query.equality.LiteralEqualityHelper; | ||
6 | import tools.refinery.store.query.literal.CallPolarity; | ||
7 | import tools.refinery.store.query.literal.DnfCallLiteral; | ||
8 | import tools.refinery.store.query.literal.LiteralReduction; | ||
9 | import tools.refinery.store.query.literal.PolarLiteral; | ||
10 | import tools.refinery.store.query.substitution.Substitution; | ||
11 | |||
12 | import java.util.List; | ||
13 | |||
14 | public class ModalDnfCallLiteral extends ModalLiteral<Dnf> implements PolarLiteral<ModalDnfCallLiteral> { | ||
15 | public ModalDnfCallLiteral(CallPolarity polarity, Modality modality, Dnf target, List<Variable> arguments) { | ||
16 | super(polarity, modality, target, arguments); | ||
17 | } | ||
18 | |||
19 | public ModalDnfCallLiteral(Modality modality, DnfCallLiteral baseLiteral) { | ||
20 | super(modality.commute(baseLiteral.getPolarity()), baseLiteral); | ||
21 | } | ||
22 | |||
23 | @Override | ||
24 | public Class<Dnf> getTargetType() { | ||
25 | return Dnf.class; | ||
26 | } | ||
27 | |||
28 | @Override | ||
29 | protected boolean targetEquals(LiteralEqualityHelper helper, Dnf otherTarget) { | ||
30 | return helper.dnfEqual(getTarget(), otherTarget); | ||
31 | } | ||
32 | |||
33 | @Override | ||
34 | public ModalDnfCallLiteral substitute(Substitution substitution) { | ||
35 | return new ModalDnfCallLiteral(getPolarity(), getModality(), getTarget(), substituteArguments(substitution)); | ||
36 | } | ||
37 | |||
38 | @Override | ||
39 | public ModalDnfCallLiteral negate() { | ||
40 | return new ModalDnfCallLiteral(getPolarity().negate(), getModality(), getTarget(), getArguments()); | ||
41 | } | ||
42 | |||
43 | @Override | ||
44 | public LiteralReduction getReduction() { | ||
45 | var dnfReduction = getTarget().getReduction(); | ||
46 | return getPolarity().isPositive() ? dnfReduction : dnfReduction.negate(); | ||
47 | } | ||
48 | } | ||
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/literal/ModalLiteral.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/literal/ModalLiteral.java deleted file mode 100644 index 5992f172..00000000 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/literal/ModalLiteral.java +++ /dev/null | |||
@@ -1,63 +0,0 @@ | |||
1 | package tools.refinery.store.reasoning.literal; | ||
2 | |||
3 | import tools.refinery.store.query.RelationLike; | ||
4 | import tools.refinery.store.query.Variable; | ||
5 | import tools.refinery.store.query.equality.LiteralEqualityHelper; | ||
6 | import tools.refinery.store.query.literal.CallLiteral; | ||
7 | import tools.refinery.store.query.literal.CallPolarity; | ||
8 | import tools.refinery.store.query.literal.Literal; | ||
9 | |||
10 | import java.util.List; | ||
11 | import java.util.Objects; | ||
12 | |||
13 | public abstract class ModalLiteral<T extends RelationLike> extends CallLiteral<T> { | ||
14 | private final Modality modality; | ||
15 | |||
16 | protected ModalLiteral(CallPolarity polarity, Modality modality, T target, List<Variable> arguments) { | ||
17 | super(polarity, target, arguments); | ||
18 | this.modality = modality; | ||
19 | } | ||
20 | |||
21 | protected ModalLiteral(Modality modality, CallLiteral<? extends T> baseLiteral) { | ||
22 | this(baseLiteral.getPolarity(), commute(modality, baseLiteral.getPolarity()), baseLiteral.getTarget(), | ||
23 | baseLiteral.getArguments()); | ||
24 | } | ||
25 | |||
26 | public Modality getModality() { | ||
27 | return modality; | ||
28 | } | ||
29 | |||
30 | @Override | ||
31 | public boolean equalsWithSubstitution(LiteralEqualityHelper helper, Literal other) { | ||
32 | if (!super.equalsWithSubstitution(helper, other)) { | ||
33 | return false; | ||
34 | } | ||
35 | // If {@link CallLiteral#equalsWithSubstitution(LiteralEqualityHelper, Literal)} has returned {@code true}, | ||
36 | // we must have the same dynamic type as {@code other}. | ||
37 | var otherModalLiteral = (ModalLiteral<?>) other; | ||
38 | return modality == otherModalLiteral.modality; | ||
39 | } | ||
40 | |||
41 | @Override | ||
42 | protected String targetToString() { | ||
43 | return "%s %s".formatted(modality, super.targetToString()); | ||
44 | } | ||
45 | |||
46 | @Override | ||
47 | public boolean equals(Object o) { | ||
48 | if (this == o) return true; | ||
49 | if (o == null || getClass() != o.getClass()) return false; | ||
50 | if (!super.equals(o)) return false; | ||
51 | ModalLiteral<?> that = (ModalLiteral<?>) o; | ||
52 | return modality == that.modality; | ||
53 | } | ||
54 | |||
55 | @Override | ||
56 | public int hashCode() { | ||
57 | return Objects.hash(super.hashCode(), modality); | ||
58 | } | ||
59 | |||
60 | private static Modality commute(Modality modality, CallPolarity polarity) { | ||
61 | return polarity.isPositive() ? modality : modality.negate(); | ||
62 | } | ||
63 | } | ||
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/literal/ModalRelationLiteral.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/literal/ModalRelationLiteral.java deleted file mode 100644 index 9c72bd37..00000000 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/literal/ModalRelationLiteral.java +++ /dev/null | |||
@@ -1,37 +0,0 @@ | |||
1 | package tools.refinery.store.reasoning.literal; | ||
2 | |||
3 | import tools.refinery.store.reasoning.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 | import tools.refinery.store.query.substitution.Substitution; | ||
8 | |||
9 | import java.util.List; | ||
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 | |||
19 | public ModalRelationLiteral(Modality modality, PartialRelationLiteral baseLiteral) { | ||
20 | super(modality, baseLiteral); | ||
21 | } | ||
22 | |||
23 | @Override | ||
24 | public Class<PartialRelation> getTargetType() { | ||
25 | return PartialRelation.class; | ||
26 | } | ||
27 | |||
28 | @Override | ||
29 | public ModalRelationLiteral substitute(Substitution substitution) { | ||
30 | return new ModalRelationLiteral(getPolarity(), getModality(), getTarget(), substituteArguments(substitution)); | ||
31 | } | ||
32 | |||
33 | @Override | ||
34 | public ModalRelationLiteral negate() { | ||
35 | return new ModalRelationLiteral(getPolarity().negate(), getModality(), getTarget(), getArguments()); | ||
36 | } | ||
37 | } | ||
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 10e4c7f7..f991f87f 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 | |||
@@ -1,33 +1,31 @@ | |||
1 | package tools.refinery.store.reasoning.literal; | 1 | package tools.refinery.store.reasoning.literal; |
2 | 2 | ||
3 | import tools.refinery.store.query.literal.DnfCallLiteral; | 3 | import tools.refinery.store.query.literal.CallLiteral; |
4 | 4 | ||
5 | public final class PartialLiterals { | 5 | public final class PartialLiterals { |
6 | private PartialLiterals() { | 6 | private PartialLiterals() { |
7 | throw new IllegalStateException("This is a static utility class and should not be instantiated directly"); | 7 | throw new IllegalStateException("This is a static utility class and should not be instantiated directly"); |
8 | } | 8 | } |
9 | 9 | ||
10 | public ModalRelationLiteral may(PartialRelationLiteral literal) { | 10 | public static CallLiteral may(CallLiteral literal) { |
11 | return new ModalRelationLiteral(Modality.MAY, literal); | 11 | return addModality(literal, Modality.MAY); |
12 | } | 12 | } |
13 | 13 | ||
14 | public ModalRelationLiteral must(PartialRelationLiteral literal) { | 14 | public static CallLiteral must(CallLiteral literal) { |
15 | return new ModalRelationLiteral(Modality.MUST, literal); | 15 | return addModality(literal, Modality.MUST); |
16 | } | 16 | } |
17 | 17 | ||
18 | public ModalRelationLiteral current(PartialRelationLiteral literal) { | 18 | public static CallLiteral current(CallLiteral literal) { |
19 | return new ModalRelationLiteral(Modality.CURRENT, literal); | 19 | return addModality(literal, Modality.CURRENT); |
20 | } | 20 | } |
21 | 21 | ||
22 | public ModalDnfCallLiteral may(DnfCallLiteral literal) { | 22 | public static CallLiteral addModality(CallLiteral literal, Modality modality) { |
23 | return new ModalDnfCallLiteral(Modality.MAY, literal); | 23 | var target = literal.getTarget(); |
24 | } | 24 | if (target instanceof ModalConstraint) { |
25 | 25 | throw new IllegalArgumentException("Literal %s already has modality".formatted(literal)); | |
26 | public ModalDnfCallLiteral must(DnfCallLiteral literal) { | 26 | } |
27 | return new ModalDnfCallLiteral(Modality.MUST, literal); | 27 | var polarity = literal.getPolarity(); |
28 | } | 28 | var modalTarget = new ModalConstraint(modality.commute(polarity), target); |
29 | 29 | return new CallLiteral(polarity, modalTarget, literal.getArguments()); | |
30 | public ModalDnfCallLiteral current(DnfCallLiteral literal) { | ||
31 | return new ModalDnfCallLiteral(Modality.CURRENT, literal); | ||
32 | } | 30 | } |
33 | } | 31 | } |
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/literal/PartialRelationLiteral.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/literal/PartialRelationLiteral.java deleted file mode 100644 index aff84538..00000000 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/literal/PartialRelationLiteral.java +++ /dev/null | |||
@@ -1,32 +0,0 @@ | |||
1 | package tools.refinery.store.reasoning.literal; | ||
2 | |||
3 | import tools.refinery.store.reasoning.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 | import tools.refinery.store.query.substitution.Substitution; | ||
9 | |||
10 | import java.util.List; | ||
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 Class<PartialRelation> getTargetType() { | ||
20 | return PartialRelation.class; | ||
21 | } | ||
22 | |||
23 | @Override | ||
24 | public PartialRelationLiteral substitute(Substitution substitution) { | ||
25 | return new PartialRelationLiteral(getPolarity(), getTarget(), substituteArguments(substitution)); | ||
26 | } | ||
27 | |||
28 | @Override | ||
29 | public PartialRelationLiteral negate() { | ||
30 | return new PartialRelationLiteral(getPolarity().negate(), getTarget(), getArguments()); | ||
31 | } | ||
32 | } | ||
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/representation/PartialRelation.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/representation/PartialRelation.java index f884f8d6..9bae53a9 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/representation/PartialRelation.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/representation/PartialRelation.java | |||
@@ -1,18 +1,16 @@ | |||
1 | package tools.refinery.store.reasoning.representation; | 1 | package tools.refinery.store.reasoning.representation; |
2 | 2 | ||
3 | import tools.refinery.store.reasoning.literal.Modality; | 3 | import tools.refinery.store.query.Constraint; |
4 | import tools.refinery.store.reasoning.literal.PartialRelationLiteral; | 4 | import tools.refinery.store.query.term.NodeSort; |
5 | import tools.refinery.store.reasoning.literal.ModalRelationLiteral; | 5 | import tools.refinery.store.query.term.Sort; |
6 | import tools.refinery.store.query.RelationLike; | ||
7 | import tools.refinery.store.query.Variable; | ||
8 | import tools.refinery.store.query.literal.CallPolarity; | ||
9 | import tools.refinery.store.representation.AbstractDomain; | 6 | import tools.refinery.store.representation.AbstractDomain; |
10 | import tools.refinery.store.representation.TruthValue; | 7 | import tools.refinery.store.representation.TruthValue; |
11 | import tools.refinery.store.representation.TruthValueDomain; | 8 | import tools.refinery.store.representation.TruthValueDomain; |
12 | 9 | ||
10 | import java.util.Arrays; | ||
13 | import java.util.List; | 11 | import java.util.List; |
14 | 12 | ||
15 | public record PartialRelation(String name, int arity) implements PartialSymbol<TruthValue, Boolean>, RelationLike { | 13 | public record PartialRelation(String name, int arity) implements PartialSymbol<TruthValue, Boolean>, Constraint { |
16 | @Override | 14 | @Override |
17 | public AbstractDomain<TruthValue, Boolean> abstractDomain() { | 15 | public AbstractDomain<TruthValue, Boolean> abstractDomain() { |
18 | return TruthValueDomain.INSTANCE; | 16 | return TruthValueDomain.INSTANCE; |
@@ -28,24 +26,16 @@ public record PartialRelation(String name, int arity) implements PartialSymbol<T | |||
28 | return false; | 26 | return false; |
29 | } | 27 | } |
30 | 28 | ||
31 | public ModalRelationLiteral call(CallPolarity polarity, Modality modality, List<Variable> arguments) { | 29 | @Override |
32 | return new ModalRelationLiteral(polarity, modality, this, arguments); | 30 | public List<Sort> getSorts() { |
33 | } | 31 | var sorts = new Sort[arity()]; |
34 | 32 | Arrays.fill(sorts, NodeSort.INSTANCE); | |
35 | public PartialRelationLiteral call(CallPolarity polarity, List<Variable> arguments) { | 33 | return List.of(sorts); |
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 | } | 34 | } |
46 | 35 | ||
47 | public PartialRelationLiteral callTransitive(Variable left, Variable right) { | 36 | @Override |
48 | return call(CallPolarity.TRANSITIVE, List.of(left, right)); | 37 | public String toReferenceString() { |
38 | return name; | ||
49 | } | 39 | } |
50 | 40 | ||
51 | @Override | 41 | @Override |
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/rule/RelationRefinementAction.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/rule/RelationRefinementAction.java index c7681b53..e8ed05a3 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/rule/RelationRefinementAction.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/rule/RelationRefinementAction.java | |||
@@ -3,7 +3,7 @@ package tools.refinery.store.reasoning.rule; | |||
3 | import tools.refinery.store.reasoning.Reasoning; | 3 | import tools.refinery.store.reasoning.Reasoning; |
4 | import tools.refinery.store.reasoning.representation.PartialRelation; | 4 | import tools.refinery.store.reasoning.representation.PartialRelation; |
5 | import tools.refinery.store.model.Model; | 5 | import tools.refinery.store.model.Model; |
6 | import tools.refinery.store.query.Variable; | 6 | import tools.refinery.store.query.term.Variable; |
7 | import tools.refinery.store.representation.TruthValue; | 7 | import tools.refinery.store.representation.TruthValue; |
8 | import tools.refinery.store.tuple.Tuple; | 8 | import tools.refinery.store.tuple.Tuple; |
9 | 9 | ||
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/rule/Rule.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/rule/Rule.java index 8a812518..c7b16d47 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/rule/Rule.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/rule/Rule.java | |||
@@ -1,7 +1,7 @@ | |||
1 | package tools.refinery.store.reasoning.rule; | 1 | package tools.refinery.store.reasoning.rule; |
2 | 2 | ||
3 | import tools.refinery.store.model.Model; | 3 | import tools.refinery.store.model.Model; |
4 | import tools.refinery.store.query.Dnf; | 4 | import tools.refinery.store.query.dnf.Dnf; |
5 | 5 | ||
6 | import java.util.ArrayList; | 6 | import java.util.ArrayList; |
7 | import java.util.HashSet; | 7 | import java.util.HashSet; |
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/rule/RuleAction.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/rule/RuleAction.java index bf980759..4753b8bc 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/rule/RuleAction.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/rule/RuleAction.java | |||
@@ -1,7 +1,7 @@ | |||
1 | package tools.refinery.store.reasoning.rule; | 1 | package tools.refinery.store.reasoning.rule; |
2 | 2 | ||
3 | import tools.refinery.store.model.Model; | 3 | import tools.refinery.store.model.Model; |
4 | import tools.refinery.store.query.Variable; | 4 | import tools.refinery.store.query.term.Variable; |
5 | 5 | ||
6 | import java.util.List; | 6 | import java.util.List; |
7 | 7 | ||
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/seed/Seed.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/seed/Seed.java index 042c2636..90633495 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/seed/Seed.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/seed/Seed.java | |||
@@ -1,4 +1,4 @@ | |||
1 | package tools.refinery.store.reasoning.translator; | 1 | package tools.refinery.store.reasoning.seed; |
2 | 2 | ||
3 | import tools.refinery.store.map.Cursor; | 3 | import tools.refinery.store.map.Cursor; |
4 | import tools.refinery.store.tuple.Tuple; | 4 | import tools.refinery.store.tuple.Tuple; |
@@ -6,7 +6,7 @@ import tools.refinery.store.tuple.Tuple; | |||
6 | public interface Seed<T> { | 6 | public interface Seed<T> { |
7 | int arity(); | 7 | int arity(); |
8 | 8 | ||
9 | T getReducedValue(); | 9 | T reducedValue(); |
10 | 10 | ||
11 | T get(Tuple key); | 11 | T get(Tuple key); |
12 | 12 | ||
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/seed/UniformSeed.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/seed/UniformSeed.java new file mode 100644 index 00000000..a030f6ea --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/seed/UniformSeed.java | |||
@@ -0,0 +1,22 @@ | |||
1 | package tools.refinery.store.reasoning.seed; | ||
2 | |||
3 | import tools.refinery.store.map.Cursor; | ||
4 | import tools.refinery.store.tuple.Tuple; | ||
5 | |||
6 | public record UniformSeed<T>(int arity, T reducedValue) implements Seed<T> { | ||
7 | public UniformSeed { | ||
8 | if (arity < 0) { | ||
9 | throw new IllegalArgumentException("Arity must not be negative"); | ||
10 | } | ||
11 | } | ||
12 | |||
13 | @Override | ||
14 | public T get(Tuple key) { | ||
15 | return reducedValue; | ||
16 | } | ||
17 | |||
18 | @Override | ||
19 | public Cursor<Tuple, T> getCursor(T defaultValue, int nodeCount) { | ||
20 | return null; | ||
21 | } | ||
22 | } | ||
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/Advice.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/Advice.java index 7909a7e1..5cdfedf7 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/Advice.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/Advice.java | |||
@@ -2,7 +2,7 @@ package tools.refinery.store.reasoning.translator; | |||
2 | 2 | ||
3 | import tools.refinery.store.reasoning.representation.AnyPartialSymbol; | 3 | import tools.refinery.store.reasoning.representation.AnyPartialSymbol; |
4 | import tools.refinery.store.reasoning.representation.PartialRelation; | 4 | import tools.refinery.store.reasoning.representation.PartialRelation; |
5 | import tools.refinery.store.query.Variable; | 5 | import tools.refinery.store.query.term.Variable; |
6 | import tools.refinery.store.query.literal.Literal; | 6 | import tools.refinery.store.query.literal.Literal; |
7 | import tools.refinery.store.query.substitution.Substitutions; | 7 | import tools.refinery.store.query.substitution.Substitutions; |
8 | 8 | ||
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/TranslatedRelation.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/TranslatedRelation.java new file mode 100644 index 00000000..9bab80c9 --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/TranslatedRelation.java | |||
@@ -0,0 +1,22 @@ | |||
1 | package tools.refinery.store.reasoning.translator; | ||
2 | |||
3 | import tools.refinery.store.model.Model; | ||
4 | import tools.refinery.store.query.term.Variable; | ||
5 | import tools.refinery.store.query.literal.CallPolarity; | ||
6 | import tools.refinery.store.query.literal.Literal; | ||
7 | import tools.refinery.store.reasoning.PartialInterpretation; | ||
8 | import tools.refinery.store.reasoning.literal.Modality; | ||
9 | import tools.refinery.store.reasoning.representation.PartialRelation; | ||
10 | import tools.refinery.store.representation.TruthValue; | ||
11 | |||
12 | import java.util.List; | ||
13 | |||
14 | public interface TranslatedRelation { | ||
15 | PartialRelation getSource(); | ||
16 | |||
17 | void configure(List<Advice> advices); | ||
18 | |||
19 | List<Literal> call(CallPolarity polarity, Modality modality, List<Variable> arguments); | ||
20 | |||
21 | PartialInterpretation<TruthValue, Boolean> createPartialInterpretation(Model model); | ||
22 | } | ||
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/TranslationUnit.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/TranslationUnit.java index e45d20c8..24b93911 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/TranslationUnit.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/TranslationUnit.java | |||
@@ -1,48 +1,32 @@ | |||
1 | package tools.refinery.store.reasoning.translator; | 1 | package tools.refinery.store.reasoning.translator; |
2 | 2 | ||
3 | import tools.refinery.store.reasoning.ReasoningBuilder; | ||
4 | import tools.refinery.store.model.Model; | 3 | import tools.refinery.store.model.Model; |
5 | import tools.refinery.store.model.ModelStoreBuilder; | 4 | import tools.refinery.store.model.ModelStoreBuilder; |
6 | import tools.refinery.store.reasoning.AnyPartialInterpretation; | 5 | import tools.refinery.store.reasoning.ReasoningBuilder; |
7 | import tools.refinery.store.reasoning.literal.Modality; | ||
8 | import tools.refinery.store.reasoning.representation.AnyPartialSymbol; | ||
9 | import tools.refinery.store.reasoning.representation.PartialRelation; | ||
10 | import tools.refinery.store.query.Variable; | ||
11 | import tools.refinery.store.query.literal.CallPolarity; | ||
12 | import tools.refinery.store.query.literal.Literal; | ||
13 | 6 | ||
14 | import java.util.Collection; | 7 | import java.util.Collection; |
15 | import java.util.List; | ||
16 | import java.util.Map; | ||
17 | 8 | ||
18 | public abstract class TranslationUnit { | 9 | public abstract class TranslationUnit { |
19 | private ReasoningBuilder reasoningBuilder; | 10 | private ReasoningBuilder reasoningBuilder; |
20 | 11 | ||
21 | protected ReasoningBuilder getPartialInterpretationBuilder() { | 12 | protected ReasoningBuilder getReasoningBuilder() { |
22 | return reasoningBuilder; | 13 | return reasoningBuilder; |
23 | } | 14 | } |
24 | 15 | ||
25 | public void setPartialInterpretationBuilder(ReasoningBuilder reasoningBuilder) { | 16 | public void setPartialInterpretationBuilder(ReasoningBuilder reasoningBuilder) { |
26 | this.reasoningBuilder = reasoningBuilder; | 17 | this.reasoningBuilder = reasoningBuilder; |
18 | configureReasoningBuilder(); | ||
27 | } | 19 | } |
28 | 20 | ||
29 | protected ModelStoreBuilder getModelStoreBuilder() { | 21 | protected ModelStoreBuilder getModelStoreBuilder() { |
30 | return reasoningBuilder.getStoreBuilder(); | 22 | return reasoningBuilder.getStoreBuilder(); |
31 | } | 23 | } |
32 | 24 | ||
33 | public abstract Collection<AnyPartialSymbol> getTranslatedPartialSymbols(); | 25 | protected void configureReasoningBuilder() { |
34 | 26 | // Nothing to configure by default. | |
35 | public Collection<Advice> computeAdvices() { | ||
36 | // No advices to give by default. | ||
37 | return List.of(); | ||
38 | } | 27 | } |
39 | 28 | ||
40 | public abstract void configure(Collection<Advice> advices); | 29 | public abstract Collection<TranslatedRelation> getTranslatedRelations(); |
41 | |||
42 | public abstract List<Literal> call(CallPolarity polarity, Modality modality, PartialRelation target, | ||
43 | List<Variable> arguments); | ||
44 | |||
45 | public abstract Map<AnyPartialSymbol, AnyPartialInterpretation> createPartialInterpretations(Model model); | ||
46 | 30 | ||
47 | public abstract void initializeModel(Model model, int nodeCount); | 31 | public abstract void initializeModel(Model model, int nodeCount); |
48 | } | 32 | } |
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/base/BaseDecisionInterpretation.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/base/BaseDecisionInterpretation.java new file mode 100644 index 00000000..b703f142 --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/base/BaseDecisionInterpretation.java | |||
@@ -0,0 +1,88 @@ | |||
1 | package tools.refinery.store.reasoning.translator.base; | ||
2 | |||
3 | import tools.refinery.store.map.Cursor; | ||
4 | import tools.refinery.store.model.Interpretation; | ||
5 | import tools.refinery.store.query.ResultSet; | ||
6 | import tools.refinery.store.reasoning.MergeResult; | ||
7 | import tools.refinery.store.reasoning.PartialInterpretation; | ||
8 | import tools.refinery.store.reasoning.ReasoningAdapter; | ||
9 | import tools.refinery.store.reasoning.representation.PartialRelation; | ||
10 | import tools.refinery.store.representation.TruthValue; | ||
11 | import tools.refinery.store.tuple.Tuple; | ||
12 | |||
13 | public class BaseDecisionInterpretation implements PartialInterpretation<TruthValue, Boolean> { | ||
14 | private final ReasoningAdapter reasoningAdapter; | ||
15 | private PartialRelation partialRelation; | ||
16 | private final ResultSet<Boolean> mustResultSet; | ||
17 | private final ResultSet<Boolean> mayResultSet; | ||
18 | private final ResultSet<Boolean> errorResultSet; | ||
19 | private final ResultSet<Boolean> currentResultSet; | ||
20 | private final Interpretation<TruthValue> interpretation; | ||
21 | |||
22 | public BaseDecisionInterpretation(ReasoningAdapter reasoningAdapter, ResultSet<Boolean> mustResultSet, | ||
23 | ResultSet<Boolean> mayResultSet, ResultSet<Boolean> errorResultSet, | ||
24 | ResultSet<Boolean> currentResultSet, Interpretation<TruthValue> interpretation) { | ||
25 | this.reasoningAdapter = reasoningAdapter; | ||
26 | this.mustResultSet = mustResultSet; | ||
27 | this.mayResultSet = mayResultSet; | ||
28 | this.errorResultSet = errorResultSet; | ||
29 | this.currentResultSet = currentResultSet; | ||
30 | this.interpretation = interpretation; | ||
31 | } | ||
32 | |||
33 | @Override | ||
34 | public ReasoningAdapter getAdapter() { | ||
35 | return reasoningAdapter; | ||
36 | } | ||
37 | |||
38 | @Override | ||
39 | public int countUnfinished() { | ||
40 | return 0; | ||
41 | } | ||
42 | |||
43 | @Override | ||
44 | public int countErrors() { | ||
45 | return errorResultSet.size(); | ||
46 | } | ||
47 | |||
48 | @Override | ||
49 | public PartialRelation getPartialSymbol() { | ||
50 | return partialRelation; | ||
51 | } | ||
52 | |||
53 | @Override | ||
54 | public TruthValue get(Tuple key) { | ||
55 | return null; | ||
56 | } | ||
57 | |||
58 | @Override | ||
59 | public Cursor<Tuple, TruthValue> getAll() { | ||
60 | return null; | ||
61 | } | ||
62 | |||
63 | @Override | ||
64 | public MergeResult merge(Tuple key, TruthValue value) { | ||
65 | TruthValue newValue; | ||
66 | switch (value) { | ||
67 | case UNKNOWN -> { | ||
68 | return MergeResult.UNCHANGED; | ||
69 | } | ||
70 | case TRUE -> newValue = mayResultSet.get(key) ? TruthValue.TRUE : TruthValue.ERROR; | ||
71 | case FALSE -> newValue = mustResultSet.get(key) ? TruthValue.ERROR : TruthValue.FALSE; | ||
72 | case ERROR -> newValue = TruthValue.ERROR; | ||
73 | default -> throw new IllegalArgumentException("Unknown truth value: " + value); | ||
74 | } | ||
75 | var oldValue = interpretation.put(key, newValue); | ||
76 | return oldValue == TruthValue.ERROR ? MergeResult.UNCHANGED : MergeResult.REFINED; | ||
77 | } | ||
78 | |||
79 | @Override | ||
80 | public Boolean getConcrete(Tuple key) { | ||
81 | return currentResultSet.get(key); | ||
82 | } | ||
83 | |||
84 | @Override | ||
85 | public Cursor<Tuple, Boolean> getAllConcrete() { | ||
86 | return null; | ||
87 | } | ||
88 | } | ||
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/base/BaseDecisionTranslationUnit.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/base/BaseDecisionTranslationUnit.java new file mode 100644 index 00000000..36e2782a --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/base/BaseDecisionTranslationUnit.java | |||
@@ -0,0 +1,49 @@ | |||
1 | package tools.refinery.store.reasoning.translator.base; | ||
2 | |||
3 | import tools.refinery.store.model.Model; | ||
4 | import tools.refinery.store.reasoning.representation.PartialRelation; | ||
5 | import tools.refinery.store.reasoning.seed.Seed; | ||
6 | import tools.refinery.store.reasoning.seed.UniformSeed; | ||
7 | import tools.refinery.store.reasoning.translator.TranslatedRelation; | ||
8 | import tools.refinery.store.reasoning.translator.TranslationUnit; | ||
9 | import tools.refinery.store.representation.Symbol; | ||
10 | import tools.refinery.store.representation.TruthValue; | ||
11 | |||
12 | import java.util.Collection; | ||
13 | import java.util.List; | ||
14 | |||
15 | public class BaseDecisionTranslationUnit extends TranslationUnit { | ||
16 | private final PartialRelation partialRelation; | ||
17 | private final Seed<TruthValue> seed; | ||
18 | private final Symbol<TruthValue> symbol; | ||
19 | |||
20 | public BaseDecisionTranslationUnit(PartialRelation partialRelation, Seed<TruthValue> seed) { | ||
21 | if (seed.arity() != partialRelation.arity()) { | ||
22 | throw new IllegalArgumentException("Expected seed with arity %d for %s, got arity %s" | ||
23 | .formatted(partialRelation.arity(), partialRelation, seed.arity())); | ||
24 | } | ||
25 | this.partialRelation = partialRelation; | ||
26 | this.seed = seed; | ||
27 | symbol = new Symbol<>(partialRelation.name(), partialRelation.arity(), TruthValue.class, TruthValue.UNKNOWN); | ||
28 | } | ||
29 | |||
30 | public BaseDecisionTranslationUnit(PartialRelation partialRelation) { | ||
31 | this(partialRelation, new UniformSeed<>(partialRelation.arity(), TruthValue.UNKNOWN)); | ||
32 | } | ||
33 | |||
34 | @Override | ||
35 | protected void configureReasoningBuilder() { | ||
36 | getModelStoreBuilder().symbol(symbol); | ||
37 | } | ||
38 | |||
39 | @Override | ||
40 | public Collection<TranslatedRelation> getTranslatedRelations() { | ||
41 | return List.of(new TranslatedBaseDecision(getReasoningBuilder(), partialRelation, symbol)); | ||
42 | } | ||
43 | |||
44 | @Override | ||
45 | public void initializeModel(Model model, int nodeCount) { | ||
46 | var interpretation = model.getInterpretation(symbol); | ||
47 | interpretation.putAll(seed.getCursor(TruthValue.UNKNOWN, nodeCount)); | ||
48 | } | ||
49 | } | ||
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/base/TranslatedBaseDecision.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/base/TranslatedBaseDecision.java new file mode 100644 index 00000000..2294b4fd --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/base/TranslatedBaseDecision.java | |||
@@ -0,0 +1,49 @@ | |||
1 | package tools.refinery.store.reasoning.translator.base; | ||
2 | |||
3 | import tools.refinery.store.model.Model; | ||
4 | import tools.refinery.store.query.term.Variable; | ||
5 | import tools.refinery.store.query.literal.CallPolarity; | ||
6 | import tools.refinery.store.query.literal.Literal; | ||
7 | import tools.refinery.store.reasoning.PartialInterpretation; | ||
8 | import tools.refinery.store.reasoning.ReasoningBuilder; | ||
9 | import tools.refinery.store.reasoning.literal.Modality; | ||
10 | import tools.refinery.store.reasoning.representation.PartialRelation; | ||
11 | import tools.refinery.store.reasoning.translator.Advice; | ||
12 | import tools.refinery.store.reasoning.translator.TranslatedRelation; | ||
13 | import tools.refinery.store.representation.Symbol; | ||
14 | import tools.refinery.store.representation.TruthValue; | ||
15 | |||
16 | import java.util.List; | ||
17 | |||
18 | class TranslatedBaseDecision implements TranslatedRelation { | ||
19 | private final ReasoningBuilder reasoningBuilder; | ||
20 | private final PartialRelation partialRelation; | ||
21 | private final Symbol<TruthValue> symbol; | ||
22 | |||
23 | public TranslatedBaseDecision(ReasoningBuilder reasoningBuilder, PartialRelation partialRelation, | ||
24 | Symbol<TruthValue> symbol) { | ||
25 | this.reasoningBuilder = reasoningBuilder; | ||
26 | this.partialRelation = partialRelation; | ||
27 | this.symbol = symbol; | ||
28 | } | ||
29 | |||
30 | @Override | ||
31 | public PartialRelation getSource() { | ||
32 | return partialRelation; | ||
33 | } | ||
34 | |||
35 | @Override | ||
36 | public void configure(List<Advice> advices) { | ||
37 | |||
38 | } | ||
39 | |||
40 | @Override | ||
41 | public List<Literal> call(CallPolarity polarity, Modality modality, List<Variable> arguments) { | ||
42 | return null; | ||
43 | } | ||
44 | |||
45 | @Override | ||
46 | public PartialInterpretation<TruthValue, Boolean> createPartialInterpretation(Model model) { | ||
47 | return null; | ||
48 | } | ||
49 | } | ||
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeHierarchyTranslationUnit.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeHierarchyTranslationUnit.java index c800b4cd..4b0761f2 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeHierarchyTranslationUnit.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeHierarchyTranslationUnit.java | |||
@@ -1,18 +1,14 @@ | |||
1 | package tools.refinery.store.reasoning.translator.typehierarchy; | 1 | package tools.refinery.store.reasoning.translator.typehierarchy; |
2 | 2 | ||
3 | import tools.refinery.store.reasoning.AnyPartialInterpretation; | 3 | import tools.refinery.store.model.Model; |
4 | import tools.refinery.store.reasoning.literal.Modality; | ||
5 | import tools.refinery.store.reasoning.representation.AnyPartialSymbol; | ||
6 | import tools.refinery.store.reasoning.representation.PartialRelation; | 4 | import tools.refinery.store.reasoning.representation.PartialRelation; |
7 | import tools.refinery.store.reasoning.translator.Advice; | 5 | import tools.refinery.store.reasoning.translator.TranslatedRelation; |
8 | import tools.refinery.store.reasoning.translator.TranslationUnit; | 6 | import tools.refinery.store.reasoning.translator.TranslationUnit; |
9 | import tools.refinery.store.model.Model; | ||
10 | import tools.refinery.store.query.Variable; | ||
11 | import tools.refinery.store.query.literal.CallPolarity; | ||
12 | import tools.refinery.store.query.literal.Literal; | ||
13 | import tools.refinery.store.representation.Symbol; | 7 | import tools.refinery.store.representation.Symbol; |
14 | 8 | ||
15 | import java.util.*; | 9 | import java.util.Collection; |
10 | import java.util.List; | ||
11 | import java.util.Map; | ||
16 | 12 | ||
17 | public class TypeHierarchyTranslationUnit extends TranslationUnit { | 13 | public class TypeHierarchyTranslationUnit extends TranslationUnit { |
18 | static final Symbol<InferredType> INFERRED_TYPE_SYMBOL = new Symbol<>("inferredType", 1, | 14 | static final Symbol<InferredType> INFERRED_TYPE_SYMBOL = new Symbol<>("inferredType", 1, |
@@ -25,24 +21,8 @@ public class TypeHierarchyTranslationUnit extends TranslationUnit { | |||
25 | } | 21 | } |
26 | 22 | ||
27 | @Override | 23 | @Override |
28 | public Collection<AnyPartialSymbol> getTranslatedPartialSymbols() { | 24 | public Collection<TranslatedRelation> getTranslatedRelations() { |
29 | return null; | 25 | return List.of(); |
30 | } | ||
31 | |||
32 | @Override | ||
33 | public void configure(Collection<Advice> advices) { | ||
34 | |||
35 | } | ||
36 | |||
37 | @Override | ||
38 | public List<Literal> call(CallPolarity polarity, Modality modality, PartialRelation target, | ||
39 | List<Variable> arguments) { | ||
40 | return null; | ||
41 | } | ||
42 | |||
43 | @Override | ||
44 | public Map<AnyPartialSymbol, AnyPartialInterpretation> createPartialInterpretations(Model model) { | ||
45 | return null; | ||
46 | } | 26 | } |
47 | 27 | ||
48 | @Override | 28 | @Override |