diff options
author | Kristóf Marussy <kristof@marussy.com> | 2023-07-19 01:51:35 +0200 |
---|---|---|
committer | Kristóf Marussy <kristof@marussy.com> | 2023-07-20 15:54:50 +0200 |
commit | 0f77d138484aaa508ba60ebba4b3b2b329df9dc3 (patch) | |
tree | 3b34725e4e4fa00ffd65e5d204cb58b9fc0d4acc /subprojects/store-reasoning | |
parent | feat: basic partial interpretation infrastructure (diff) | |
download | refinery-0f77d138484aaa508ba60ebba4b3b2b329df9dc3.tar.gz refinery-0f77d138484aaa508ba60ebba4b3b2b329df9dc3.tar.zst refinery-0f77d138484aaa508ba60ebba4b3b2b329df9dc3.zip |
feat: multi-object based EQUALS and EXISTS
Adds translator for EQUALS and EXISTS symbols based on the multi-object
formalism. Only diagonal equality links are supported (e.g., distinct nodes may
not be EQUALS with each other).
Also introduces initial model seeds to separate partial interpreter construction
and graph initialization better.
Diffstat (limited to 'subprojects/store-reasoning')
29 files changed, 872 insertions, 226 deletions
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 6d416436..f560c74c 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 | |||
@@ -8,7 +8,9 @@ package tools.refinery.store.reasoning; | |||
8 | import tools.refinery.store.adapter.ModelAdapterBuilder; | 8 | import tools.refinery.store.adapter.ModelAdapterBuilder; |
9 | import tools.refinery.store.model.ModelStore; | 9 | import tools.refinery.store.model.ModelStore; |
10 | import tools.refinery.store.query.dnf.Dnf; | 10 | import tools.refinery.store.query.dnf.Dnf; |
11 | import tools.refinery.store.query.dnf.FunctionalQuery; | ||
11 | import tools.refinery.store.query.dnf.Query; | 12 | import tools.refinery.store.query.dnf.Query; |
13 | import tools.refinery.store.query.dnf.RelationalQuery; | ||
12 | import tools.refinery.store.reasoning.literal.Concreteness; | 14 | import tools.refinery.store.reasoning.literal.Concreteness; |
13 | import tools.refinery.store.reasoning.literal.Modality; | 15 | import tools.refinery.store.reasoning.literal.Modality; |
14 | import tools.refinery.store.reasoning.refinement.PartialModelInitializer; | 16 | import tools.refinery.store.reasoning.refinement.PartialModelInitializer; |
@@ -18,8 +20,6 @@ import tools.refinery.store.representation.Symbol; | |||
18 | 20 | ||
19 | @SuppressWarnings("UnusedReturnValue") | 21 | @SuppressWarnings("UnusedReturnValue") |
20 | public interface ReasoningBuilder extends ModelAdapterBuilder { | 22 | public interface ReasoningBuilder extends ModelAdapterBuilder { |
21 | ReasoningBuilder initialNodeCount(int nodeCount); | ||
22 | |||
23 | ReasoningBuilder partialSymbol(AnyPartialSymbolTranslator translator); | 23 | ReasoningBuilder partialSymbol(AnyPartialSymbolTranslator translator); |
24 | 24 | ||
25 | <T> ReasoningBuilder storageRefiner(Symbol<T> symbol, StorageRefiner.Factory<T> refiner); | 25 | <T> ReasoningBuilder storageRefiner(Symbol<T> symbol, StorageRefiner.Factory<T> refiner); |
@@ -28,6 +28,10 @@ public interface ReasoningBuilder extends ModelAdapterBuilder { | |||
28 | 28 | ||
29 | <T> Query<T> lift(Modality modality, Concreteness concreteness, Query<T> query); | 29 | <T> Query<T> lift(Modality modality, Concreteness concreteness, Query<T> query); |
30 | 30 | ||
31 | RelationalQuery lift(Modality modality, Concreteness concreteness, RelationalQuery query); | ||
32 | |||
33 | <T> FunctionalQuery<T> lift(Modality modality, Concreteness concreteness, FunctionalQuery<T> query); | ||
34 | |||
31 | Dnf lift(Modality modality, Concreteness concreteness, Dnf dnf); | 35 | Dnf lift(Modality modality, Concreteness concreteness, Dnf dnf); |
32 | 36 | ||
33 | @Override | 37 | @Override |
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 fae60d9e..6f9354eb 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 | |||
@@ -8,6 +8,7 @@ package tools.refinery.store.reasoning; | |||
8 | import tools.refinery.store.adapter.ModelStoreAdapter; | 8 | import tools.refinery.store.adapter.ModelStoreAdapter; |
9 | import tools.refinery.store.model.Model; | 9 | import tools.refinery.store.model.Model; |
10 | import tools.refinery.store.reasoning.representation.AnyPartialSymbol; | 10 | import tools.refinery.store.reasoning.representation.AnyPartialSymbol; |
11 | import tools.refinery.store.reasoning.seed.ModelSeed; | ||
11 | 12 | ||
12 | import java.util.Collection; | 13 | import java.util.Collection; |
13 | 14 | ||
@@ -16,7 +17,7 @@ public interface ReasoningStoreAdapter extends ModelStoreAdapter { | |||
16 | 17 | ||
17 | Collection<AnyPartialSymbol> getRefinablePartialSymbols(); | 18 | Collection<AnyPartialSymbol> getRefinablePartialSymbols(); |
18 | 19 | ||
19 | Model createInitialModel(); | 20 | Model createInitialModel(ModelSeed modelSeed); |
20 | 21 | ||
21 | @Override | 22 | @Override |
22 | ReasoningAdapter createModelAdapter(Model model); | 23 | ReasoningAdapter createModelAdapter(Model model); |
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/internal/PartialClauseRewriter.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/internal/PartialClauseRewriter.java new file mode 100644 index 00000000..bc379c64 --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/internal/PartialClauseRewriter.java | |||
@@ -0,0 +1,91 @@ | |||
1 | /* | ||
2 | * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/> | ||
3 | * | ||
4 | * SPDX-License-Identifier: EPL-2.0 | ||
5 | */ | ||
6 | package tools.refinery.store.reasoning.internal; | ||
7 | |||
8 | import tools.refinery.store.query.dnf.Dnf; | ||
9 | import tools.refinery.store.query.dnf.DnfClause; | ||
10 | import tools.refinery.store.query.literal.AbstractCallLiteral; | ||
11 | import tools.refinery.store.query.literal.Literal; | ||
12 | import tools.refinery.store.query.term.Variable; | ||
13 | import tools.refinery.store.reasoning.literal.Concreteness; | ||
14 | import tools.refinery.store.reasoning.literal.ModalConstraint; | ||
15 | import tools.refinery.store.reasoning.literal.Modality; | ||
16 | import tools.refinery.store.reasoning.representation.PartialRelation; | ||
17 | |||
18 | import java.util.*; | ||
19 | |||
20 | class PartialClauseRewriter { | ||
21 | private final PartialQueryRewriter rewriter; | ||
22 | private final List<Literal> completedLiterals = new ArrayList<>(); | ||
23 | private final Deque<Literal> workList = new ArrayDeque<>(); | ||
24 | private final Set<Variable> positiveVariables = new LinkedHashSet<>(); | ||
25 | private final Set<Variable> unmodifiablePositiveVariables = Collections.unmodifiableSet(positiveVariables); | ||
26 | |||
27 | public PartialClauseRewriter(PartialQueryRewriter rewriter) { | ||
28 | this.rewriter = rewriter; | ||
29 | } | ||
30 | |||
31 | public List<Literal> rewriteClause(DnfClause clause) { | ||
32 | workList.addAll(clause.literals()); | ||
33 | while (!workList.isEmpty()) { | ||
34 | var literal = workList.removeFirst(); | ||
35 | rewrite(literal); | ||
36 | } | ||
37 | return completedLiterals; | ||
38 | } | ||
39 | |||
40 | private void rewrite(Literal literal) { | ||
41 | if (!(literal instanceof AbstractCallLiteral callLiteral)) { | ||
42 | markAsDone(literal); | ||
43 | return; | ||
44 | } | ||
45 | var target = callLiteral.getTarget(); | ||
46 | if (target instanceof Dnf dnf) { | ||
47 | rewriteRecursively(callLiteral, dnf); | ||
48 | } else if (target instanceof ModalConstraint modalConstraint) { | ||
49 | var modality = modalConstraint.modality(); | ||
50 | var concreteness = modalConstraint.concreteness(); | ||
51 | var constraint = modalConstraint.constraint(); | ||
52 | if (constraint instanceof Dnf dnf) { | ||
53 | rewriteRecursively(callLiteral, modality, concreteness, dnf); | ||
54 | } else if (constraint instanceof PartialRelation partialRelation) { | ||
55 | rewrite(callLiteral, modality, concreteness, partialRelation); | ||
56 | } else { | ||
57 | throw new IllegalArgumentException("Cannot interpret modal constraint: " + modalConstraint); | ||
58 | } | ||
59 | } else { | ||
60 | markAsDone(literal); | ||
61 | } | ||
62 | } | ||
63 | |||
64 | private void markAsDone(Literal literal) { | ||
65 | completedLiterals.add(literal); | ||
66 | positiveVariables.addAll(literal.getOutputVariables()); | ||
67 | } | ||
68 | |||
69 | private void rewriteRecursively(AbstractCallLiteral callLiteral, Modality modality, Concreteness concreteness, | ||
70 | Dnf dnf) { | ||
71 | var liftedDnf = rewriter.getLifter().lift(modality, concreteness, dnf); | ||
72 | rewriteRecursively(callLiteral, liftedDnf); | ||
73 | } | ||
74 | |||
75 | private void rewriteRecursively(AbstractCallLiteral callLiteral, Dnf dnf) { | ||
76 | var rewrittenDnf = rewriter.rewrite(dnf); | ||
77 | var rewrittenLiteral = callLiteral.withTarget(rewrittenDnf); | ||
78 | completedLiterals.add(rewrittenLiteral); | ||
79 | } | ||
80 | |||
81 | private void rewrite(AbstractCallLiteral callLiteral, Modality modality, Concreteness concreteness, | ||
82 | PartialRelation partialRelation) { | ||
83 | var relationRewriter = rewriter.getRelationRewriter(partialRelation); | ||
84 | var literals = relationRewriter.rewriteLiteral( | ||
85 | unmodifiablePositiveVariables, callLiteral, modality, concreteness); | ||
86 | int length = literals.size(); | ||
87 | for (int i = length - 1; i >= 0; i--) { | ||
88 | workList.addFirst(literals.get(i)); | ||
89 | } | ||
90 | } | ||
91 | } | ||
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/internal/PartialQueryRewriter.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/internal/PartialQueryRewriter.java index 132022d1..79cba263 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/internal/PartialQueryRewriter.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/internal/PartialQueryRewriter.java | |||
@@ -6,18 +6,13 @@ | |||
6 | package tools.refinery.store.reasoning.internal; | 6 | package tools.refinery.store.reasoning.internal; |
7 | 7 | ||
8 | import tools.refinery.store.query.dnf.Dnf; | 8 | import tools.refinery.store.query.dnf.Dnf; |
9 | import tools.refinery.store.query.dnf.DnfClause; | ||
10 | import tools.refinery.store.query.literal.AbstractCallLiteral; | ||
11 | import tools.refinery.store.query.literal.Literal; | ||
12 | import tools.refinery.store.query.rewriter.AbstractRecursiveRewriter; | 9 | import tools.refinery.store.query.rewriter.AbstractRecursiveRewriter; |
13 | import tools.refinery.store.reasoning.interpretation.PartialRelationRewriter; | 10 | import tools.refinery.store.reasoning.interpretation.PartialRelationRewriter; |
14 | import tools.refinery.store.reasoning.lifting.DnfLifter; | 11 | import tools.refinery.store.reasoning.lifting.DnfLifter; |
15 | import tools.refinery.store.reasoning.literal.Concreteness; | ||
16 | import tools.refinery.store.reasoning.literal.ModalConstraint; | ||
17 | import tools.refinery.store.reasoning.literal.Modality; | ||
18 | import tools.refinery.store.reasoning.representation.PartialRelation; | 12 | import tools.refinery.store.reasoning.representation.PartialRelation; |
19 | 13 | ||
20 | import java.util.*; | 14 | import java.util.HashMap; |
15 | import java.util.Map; | ||
21 | 16 | ||
22 | class PartialQueryRewriter extends AbstractRecursiveRewriter { | 17 | class PartialQueryRewriter extends AbstractRecursiveRewriter { |
23 | private final DnfLifter lifter; | 18 | private final DnfLifter lifter; |
@@ -27,6 +22,18 @@ class PartialQueryRewriter extends AbstractRecursiveRewriter { | |||
27 | this.lifter = lifter; | 22 | this.lifter = lifter; |
28 | } | 23 | } |
29 | 24 | ||
25 | DnfLifter getLifter() { | ||
26 | return lifter; | ||
27 | } | ||
28 | |||
29 | PartialRelationRewriter getRelationRewriter(PartialRelation partialRelation) { | ||
30 | var rewriter = relationRewriterMap.get(partialRelation); | ||
31 | if (rewriter == null) { | ||
32 | throw new IllegalArgumentException("Do not know how to interpret partial relation: " + partialRelation); | ||
33 | } | ||
34 | return rewriter; | ||
35 | } | ||
36 | |||
30 | public void addRelationRewriter(PartialRelation partialRelation, PartialRelationRewriter interpreter) { | 37 | public void addRelationRewriter(PartialRelation partialRelation, PartialRelationRewriter interpreter) { |
31 | if (relationRewriterMap.put(partialRelation, interpreter) != null) { | 38 | if (relationRewriterMap.put(partialRelation, interpreter) != null) { |
32 | throw new IllegalArgumentException("Duplicate partial relation: " + partialRelation); | 39 | throw new IllegalArgumentException("Duplicate partial relation: " + partialRelation); |
@@ -37,67 +44,10 @@ class PartialQueryRewriter extends AbstractRecursiveRewriter { | |||
37 | protected Dnf doRewrite(Dnf dnf) { | 44 | protected Dnf doRewrite(Dnf dnf) { |
38 | var builder = Dnf.builderFrom(dnf); | 45 | var builder = Dnf.builderFrom(dnf); |
39 | for (var clause : dnf.getClauses()) { | 46 | for (var clause : dnf.getClauses()) { |
40 | builder.clause(rewriteClause(clause)); | 47 | var clauseRewriter = new PartialClauseRewriter(this); |
48 | var rewrittenClauses = clauseRewriter.rewriteClause(clause); | ||
49 | builder.clause(rewrittenClauses); | ||
41 | } | 50 | } |
42 | return builder.build(); | 51 | return builder.build(); |
43 | } | 52 | } |
44 | |||
45 | private List<Literal> rewriteClause(DnfClause clause) { | ||
46 | var completedLiterals = new ArrayList<Literal>(); | ||
47 | var workList = new ArrayDeque<>(clause.literals()); | ||
48 | while (!workList.isEmpty()) { | ||
49 | var literal = workList.removeFirst(); | ||
50 | rewrite(literal, completedLiterals, workList); | ||
51 | } | ||
52 | return completedLiterals; | ||
53 | } | ||
54 | |||
55 | private void rewrite(Literal literal, List<Literal> completedLiterals, Deque<Literal> workList) { | ||
56 | if (!(literal instanceof AbstractCallLiteral callLiteral)) { | ||
57 | completedLiterals.add(literal); | ||
58 | return; | ||
59 | } | ||
60 | var target = callLiteral.getTarget(); | ||
61 | if (target instanceof Dnf dnf) { | ||
62 | rewriteRecursively(callLiteral, dnf, completedLiterals); | ||
63 | } else if (target instanceof ModalConstraint modalConstraint) { | ||
64 | var modality = modalConstraint.modality(); | ||
65 | var concreteness = modalConstraint.concreteness(); | ||
66 | var constraint = modalConstraint.constraint(); | ||
67 | if (constraint instanceof Dnf dnf) { | ||
68 | rewriteRecursively(callLiteral, modality, concreteness, dnf, completedLiterals); | ||
69 | } else if (constraint instanceof PartialRelation partialRelation) { | ||
70 | rewrite(callLiteral, modality, concreteness, partialRelation, workList); | ||
71 | } else { | ||
72 | throw new IllegalArgumentException("Cannot interpret modal constraint: " + modalConstraint); | ||
73 | } | ||
74 | } else { | ||
75 | completedLiterals.add(literal); | ||
76 | } | ||
77 | } | ||
78 | |||
79 | private void rewriteRecursively(AbstractCallLiteral callLiteral, Modality modality, Concreteness concreteness, | ||
80 | Dnf dnf, List<Literal> completedLiterals) { | ||
81 | var liftedDnf = lifter.lift(modality, concreteness, dnf); | ||
82 | rewriteRecursively(callLiteral, liftedDnf, completedLiterals); | ||
83 | } | ||
84 | |||
85 | private void rewriteRecursively(AbstractCallLiteral callLiteral, Dnf dnf, List<Literal> completedLiterals) { | ||
86 | var rewrittenDnf = rewrite(dnf); | ||
87 | var rewrittenLiteral = callLiteral.withTarget(rewrittenDnf); | ||
88 | completedLiterals.add(rewrittenLiteral); | ||
89 | } | ||
90 | |||
91 | private void rewrite(AbstractCallLiteral callLiteral, Modality modality, Concreteness concreteness, | ||
92 | PartialRelation partialRelation, Deque<Literal> workList) { | ||
93 | var rewriter = relationRewriterMap.get(partialRelation); | ||
94 | if (rewriter == null) { | ||
95 | throw new IllegalArgumentException("Do not know how to interpret partial relation: " + partialRelation); | ||
96 | } | ||
97 | var literals = rewriter.rewriteLiteral(callLiteral, modality, concreteness); | ||
98 | int length = literals.size(); | ||
99 | for (int i = length - 1; i >= 0; i--) { | ||
100 | workList.addFirst(literals.get(i)); | ||
101 | } | ||
102 | } | ||
103 | } | 53 | } |
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 396c2dcc..579b08dd 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 | |||
@@ -48,7 +48,7 @@ class ReasoningAdapterImpl implements ReasoningAdapter { | |||
48 | refiners = new HashMap<>(refinerFactories.size()); | 48 | refiners = new HashMap<>(refinerFactories.size()); |
49 | createRefiners(); | 49 | createRefiners(); |
50 | 50 | ||
51 | storageRefiners = storeAdapter.createRepresentationRefiners(model); | 51 | storageRefiners = storeAdapter.createStprageRefiner(model); |
52 | 52 | ||
53 | nodeCountInterpretation = model.getInterpretation(NODE_COUNT_SYMBOL); | 53 | nodeCountInterpretation = model.getInterpretation(NODE_COUNT_SYMBOL); |
54 | } | 54 | } |
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 f7a91284..2af84e2d 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 | |||
@@ -10,7 +10,9 @@ import tools.refinery.store.model.ModelStore; | |||
10 | import tools.refinery.store.model.ModelStoreBuilder; | 10 | import tools.refinery.store.model.ModelStoreBuilder; |
11 | import tools.refinery.store.query.ModelQueryBuilder; | 11 | import tools.refinery.store.query.ModelQueryBuilder; |
12 | import tools.refinery.store.query.dnf.Dnf; | 12 | import tools.refinery.store.query.dnf.Dnf; |
13 | import tools.refinery.store.query.dnf.FunctionalQuery; | ||
13 | import tools.refinery.store.query.dnf.Query; | 14 | import tools.refinery.store.query.dnf.Query; |
15 | import tools.refinery.store.query.dnf.RelationalQuery; | ||
14 | import tools.refinery.store.reasoning.ReasoningBuilder; | 16 | import tools.refinery.store.reasoning.ReasoningBuilder; |
15 | import tools.refinery.store.reasoning.interpretation.PartialInterpretation; | 17 | import tools.refinery.store.reasoning.interpretation.PartialInterpretation; |
16 | import tools.refinery.store.reasoning.refinement.DefaultStorageRefiner; | 18 | import tools.refinery.store.reasoning.refinement.DefaultStorageRefiner; |
@@ -38,16 +40,6 @@ public class ReasoningBuilderImpl extends AbstractModelAdapterBuilder<ReasoningS | |||
38 | new LinkedHashMap<>(); | 40 | new LinkedHashMap<>(); |
39 | private final Map<AnySymbol, StorageRefiner.Factory<?>> registeredStorageRefiners = new LinkedHashMap<>(); | 41 | private final Map<AnySymbol, StorageRefiner.Factory<?>> registeredStorageRefiners = new LinkedHashMap<>(); |
40 | private final List<PartialModelInitializer> initializers = new ArrayList<>(); | 42 | private final List<PartialModelInitializer> initializers = new ArrayList<>(); |
41 | private int initialNodeCount = 0; | ||
42 | |||
43 | @Override | ||
44 | public ReasoningBuilder initialNodeCount(int nodeCount) { | ||
45 | if (nodeCount < 0) { | ||
46 | throw new IllegalArgumentException("Initial model size must not be negative"); | ||
47 | } | ||
48 | initialNodeCount = nodeCount; | ||
49 | return this; | ||
50 | } | ||
51 | 43 | ||
52 | @Override | 44 | @Override |
53 | public ReasoningBuilder partialSymbol(AnyPartialSymbolTranslator translator) { | 45 | public ReasoningBuilder partialSymbol(AnyPartialSymbolTranslator translator) { |
@@ -81,6 +73,16 @@ public class ReasoningBuilderImpl extends AbstractModelAdapterBuilder<ReasoningS | |||
81 | } | 73 | } |
82 | 74 | ||
83 | @Override | 75 | @Override |
76 | public RelationalQuery lift(Modality modality, Concreteness concreteness, RelationalQuery query) { | ||
77 | return lifter.lift(modality, concreteness, query); | ||
78 | } | ||
79 | |||
80 | @Override | ||
81 | public <T> FunctionalQuery<T> lift(Modality modality, Concreteness concreteness, FunctionalQuery<T> query) { | ||
82 | return lifter.lift(modality, concreteness, query); | ||
83 | } | ||
84 | |||
85 | @Override | ||
84 | public Dnf lift(Modality modality, Concreteness concreteness, Dnf dnf) { | 86 | public Dnf lift(Modality modality, Concreteness concreteness, Dnf dnf) { |
85 | return lifter.lift(modality, concreteness, dnf); | 87 | return lifter.lift(modality, concreteness, dnf); |
86 | } | 88 | } |
@@ -114,7 +116,7 @@ public class ReasoningBuilderImpl extends AbstractModelAdapterBuilder<ReasoningS | |||
114 | 116 | ||
115 | @Override | 117 | @Override |
116 | public ReasoningStoreAdapterImpl doBuild(ModelStore store) { | 118 | public ReasoningStoreAdapterImpl doBuild(ModelStore store) { |
117 | return new ReasoningStoreAdapterImpl(store, initialNodeCount, Collections.unmodifiableMap(symbolInterpreters), | 119 | return new ReasoningStoreAdapterImpl(store, Collections.unmodifiableMap(symbolInterpreters), |
118 | Collections.unmodifiableMap(symbolRefiners), getStorageRefiners(store), | 120 | Collections.unmodifiableMap(symbolRefiners), getStorageRefiners(store), |
119 | Collections.unmodifiableList(initializers)); | 121 | Collections.unmodifiableList(initializers)); |
120 | } | 122 | } |
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 e8b581c6..3dac53ef 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 | |||
@@ -14,6 +14,7 @@ import tools.refinery.store.reasoning.refinement.PartialInterpretationRefiner; | |||
14 | import tools.refinery.store.reasoning.refinement.PartialModelInitializer; | 14 | import tools.refinery.store.reasoning.refinement.PartialModelInitializer; |
15 | import tools.refinery.store.reasoning.refinement.StorageRefiner; | 15 | import tools.refinery.store.reasoning.refinement.StorageRefiner; |
16 | import tools.refinery.store.reasoning.representation.AnyPartialSymbol; | 16 | import tools.refinery.store.reasoning.representation.AnyPartialSymbol; |
17 | import tools.refinery.store.reasoning.seed.ModelSeed; | ||
17 | import tools.refinery.store.representation.AnySymbol; | 18 | import tools.refinery.store.representation.AnySymbol; |
18 | import tools.refinery.store.representation.Symbol; | 19 | import tools.refinery.store.representation.Symbol; |
19 | import tools.refinery.store.tuple.Tuple; | 20 | import tools.refinery.store.tuple.Tuple; |
@@ -26,23 +27,18 @@ class ReasoningStoreAdapterImpl implements ReasoningStoreAdapter { | |||
26 | private final ModelStore store; | 27 | private final ModelStore store; |
27 | private final Map<AnyPartialSymbol, PartialInterpretation.Factory<?, ?>> symbolInterpreters; | 28 | private final Map<AnyPartialSymbol, PartialInterpretation.Factory<?, ?>> symbolInterpreters; |
28 | private final Map<AnyPartialSymbol, PartialInterpretationRefiner.Factory<?, ?>> symbolRefiners; | 29 | private final Map<AnyPartialSymbol, PartialInterpretationRefiner.Factory<?, ?>> symbolRefiners; |
29 | private final Map<AnySymbol, StorageRefiner.Factory<?>> representationRefiners; | 30 | private final Map<AnySymbol, StorageRefiner.Factory<?>> storageRefiners; |
30 | private final Object initialModelLock = new Object(); | 31 | private final List<PartialModelInitializer> initializers; |
31 | private final int initialNodeCount; | ||
32 | private List<PartialModelInitializer> initializers; | ||
33 | private long initialCommitId = Model.NO_STATE_ID; | ||
34 | 32 | ||
35 | ReasoningStoreAdapterImpl(ModelStore store, | 33 | ReasoningStoreAdapterImpl(ModelStore store, |
36 | int initialNodeCount, | ||
37 | Map<AnyPartialSymbol, PartialInterpretation.Factory<?, ?>> symbolInterpreters, | 34 | Map<AnyPartialSymbol, PartialInterpretation.Factory<?, ?>> symbolInterpreters, |
38 | Map<AnyPartialSymbol, PartialInterpretationRefiner.Factory<?, ?>> symbolRefiners, | 35 | Map<AnyPartialSymbol, PartialInterpretationRefiner.Factory<?, ?>> symbolRefiners, |
39 | Map<AnySymbol, StorageRefiner.Factory<?>> representationRefiners, | 36 | Map<AnySymbol, StorageRefiner.Factory<?>> storageRefiners, |
40 | List<PartialModelInitializer> initializers) { | 37 | List<PartialModelInitializer> initializers) { |
41 | this.store = store; | 38 | this.store = store; |
42 | this.initialNodeCount = initialNodeCount; | ||
43 | this.symbolInterpreters = symbolInterpreters; | 39 | this.symbolInterpreters = symbolInterpreters; |
44 | this.symbolRefiners = symbolRefiners; | 40 | this.symbolRefiners = symbolRefiners; |
45 | this.representationRefiners = representationRefiners; | 41 | this.storageRefiners = storageRefiners; |
46 | this.initializers = initializers; | 42 | this.initializers = initializers; |
47 | } | 43 | } |
48 | 44 | ||
@@ -73,44 +69,32 @@ class ReasoningStoreAdapterImpl implements ReasoningStoreAdapter { | |||
73 | return symbolRefiners; | 69 | return symbolRefiners; |
74 | } | 70 | } |
75 | 71 | ||
76 | StorageRefiner[] createRepresentationRefiners(Model model) { | 72 | StorageRefiner[] createStprageRefiner(Model model) { |
77 | var refiners = new StorageRefiner[representationRefiners.size()]; | 73 | var refiners = new StorageRefiner[storageRefiners.size()]; |
78 | int i = 0; | 74 | int i = 0; |
79 | for (var entry : representationRefiners.entrySet()) { | 75 | for (var entry : storageRefiners.entrySet()) { |
80 | var symbol = entry.getKey(); | 76 | var symbol = entry.getKey(); |
81 | var factory = entry.getValue(); | 77 | var factory = entry.getValue(); |
82 | refiners[i] = createRepresentationRefiner(factory, model, symbol); | 78 | refiners[i] = createStorageRefiner(factory, model, symbol); |
79 | i++; | ||
83 | } | 80 | } |
84 | return refiners; | 81 | return refiners; |
85 | } | 82 | } |
86 | 83 | ||
87 | private <T> StorageRefiner createRepresentationRefiner( | 84 | private <T> StorageRefiner createStorageRefiner(StorageRefiner.Factory<T> factory, Model model, AnySymbol symbol) { |
88 | StorageRefiner.Factory<T> factory, Model model, AnySymbol symbol) { | ||
89 | // The builder only allows well-typed assignment of refiners to symbols. | 85 | // The builder only allows well-typed assignment of refiners to symbols. |
90 | @SuppressWarnings("unchecked") | 86 | @SuppressWarnings("unchecked") |
91 | var typedSymbol = (Symbol<T>) symbol; | 87 | var typedSymbol = (Symbol<T>) symbol; |
92 | return factory.create(typedSymbol, model); | 88 | return factory.create(typedSymbol, model); |
93 | } | 89 | } |
94 | 90 | ||
95 | @Override | 91 | public Model createInitialModel(ModelSeed modelSeed) { |
96 | public Model createInitialModel() { | ||
97 | synchronized (initialModelLock) { | ||
98 | if (initialCommitId == Model.NO_STATE_ID) { | ||
99 | return doCreateInitialModel(); | ||
100 | } | ||
101 | return store.createModelForState(initialCommitId); | ||
102 | } | ||
103 | } | ||
104 | |||
105 | private Model doCreateInitialModel() { | ||
106 | var model = store.createEmptyModel(); | 92 | var model = store.createEmptyModel(); |
107 | model.getInterpretation(ReasoningAdapterImpl.NODE_COUNT_SYMBOL).put(Tuple.of(), initialNodeCount); | 93 | model.getInterpretation(ReasoningAdapterImpl.NODE_COUNT_SYMBOL).put(Tuple.of(), modelSeed.getNodeCount()); |
108 | for (var initializer : initializers) { | 94 | for (var initializer : initializers) { |
109 | initializer.initialize(model, initialNodeCount); | 95 | initializer.initialize(model, modelSeed); |
110 | } | 96 | } |
111 | model.getAdapter(ModelQueryAdapter.class).flushChanges(); | 97 | model.getAdapter(ModelQueryAdapter.class).flushChanges(); |
112 | initialCommitId = model.commit(); | ||
113 | initializers = null; | ||
114 | return model; | 98 | return model; |
115 | } | 99 | } |
116 | 100 | ||
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/interpretation/PartialRelationRewriter.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/interpretation/PartialRelationRewriter.java index da8ae0a8..6ad35c20 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/interpretation/PartialRelationRewriter.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/interpretation/PartialRelationRewriter.java | |||
@@ -7,11 +7,15 @@ package tools.refinery.store.reasoning.interpretation; | |||
7 | 7 | ||
8 | import tools.refinery.store.query.literal.AbstractCallLiteral; | 8 | import tools.refinery.store.query.literal.AbstractCallLiteral; |
9 | import tools.refinery.store.query.literal.Literal; | 9 | import tools.refinery.store.query.literal.Literal; |
10 | import tools.refinery.store.query.term.Variable; | ||
10 | import tools.refinery.store.reasoning.literal.Concreteness; | 11 | import tools.refinery.store.reasoning.literal.Concreteness; |
11 | import tools.refinery.store.reasoning.literal.Modality; | 12 | import tools.refinery.store.reasoning.literal.Modality; |
12 | 13 | ||
13 | import java.util.List; | 14 | import java.util.List; |
15 | import java.util.Set; | ||
14 | 16 | ||
17 | @FunctionalInterface | ||
15 | public interface PartialRelationRewriter { | 18 | public interface PartialRelationRewriter { |
16 | List<Literal> rewriteLiteral(AbstractCallLiteral literal, Modality modality, Concreteness concreteness); | 19 | List<Literal> rewriteLiteral(Set<Variable> positiveVariables, AbstractCallLiteral literal, Modality modality, |
20 | Concreteness concreteness); | ||
17 | } | 21 | } |
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/interpretation/QueryBasedRelationRewriter.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/interpretation/QueryBasedRelationRewriter.java index 3be9e9ac..78fdbb89 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/interpretation/QueryBasedRelationRewriter.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/interpretation/QueryBasedRelationRewriter.java | |||
@@ -5,30 +5,49 @@ | |||
5 | */ | 5 | */ |
6 | package tools.refinery.store.reasoning.interpretation; | 6 | package tools.refinery.store.reasoning.interpretation; |
7 | 7 | ||
8 | import tools.refinery.store.query.dnf.Query; | 8 | import tools.refinery.store.query.dnf.RelationalQuery; |
9 | import tools.refinery.store.query.literal.AbstractCallLiteral; | 9 | import tools.refinery.store.query.literal.AbstractCallLiteral; |
10 | import tools.refinery.store.query.literal.Literal; | 10 | import tools.refinery.store.query.literal.Literal; |
11 | import tools.refinery.store.query.term.Variable; | ||
11 | import tools.refinery.store.reasoning.literal.Concreteness; | 12 | import tools.refinery.store.reasoning.literal.Concreteness; |
12 | import tools.refinery.store.reasoning.literal.Modality; | 13 | import tools.refinery.store.reasoning.literal.Modality; |
13 | 14 | ||
14 | import java.util.List; | 15 | import java.util.List; |
16 | import java.util.Set; | ||
15 | 17 | ||
16 | public class QueryBasedRelationRewriter implements PartialRelationRewriter { | 18 | public class QueryBasedRelationRewriter implements PartialRelationRewriter { |
17 | private final Query<Boolean> may; | 19 | private final RelationalQuery may; |
18 | private final Query<Boolean> must; | 20 | private final RelationalQuery must; |
19 | private final Query<Boolean> candidateMay; | 21 | private final RelationalQuery candidateMay; |
20 | private final Query<Boolean> candidateMust; | 22 | private final RelationalQuery candidateMust; |
21 | 23 | ||
22 | public QueryBasedRelationRewriter(Query<Boolean> may, Query<Boolean> must, Query<Boolean> candidateMay, | 24 | public QueryBasedRelationRewriter(RelationalQuery may, RelationalQuery must, RelationalQuery candidateMay, |
23 | Query<Boolean> candidateMust) { | 25 | RelationalQuery candidateMust) { |
24 | this.may = may; | 26 | this.may = may; |
25 | this.must = must; | 27 | this.must = must; |
26 | this.candidateMay = candidateMay; | 28 | this.candidateMay = candidateMay; |
27 | this.candidateMust = candidateMust; | 29 | this.candidateMust = candidateMust; |
28 | } | 30 | } |
29 | 31 | ||
32 | public RelationalQuery getMay() { | ||
33 | return may; | ||
34 | } | ||
35 | |||
36 | public RelationalQuery getMust() { | ||
37 | return must; | ||
38 | } | ||
39 | |||
40 | public RelationalQuery getCandidateMay() { | ||
41 | return candidateMay; | ||
42 | } | ||
43 | |||
44 | public RelationalQuery getCandidateMust() { | ||
45 | return candidateMust; | ||
46 | } | ||
47 | |||
30 | @Override | 48 | @Override |
31 | public List<Literal> rewriteLiteral(AbstractCallLiteral literal, Modality modality, Concreteness concreteness) { | 49 | public List<Literal> rewriteLiteral(Set<Variable> positiveVariables, AbstractCallLiteral literal, |
50 | Modality modality, Concreteness concreteness) { | ||
32 | var query = switch (concreteness) { | 51 | var query = switch (concreteness) { |
33 | case PARTIAL -> switch (modality) { | 52 | case PARTIAL -> switch (modality) { |
34 | case MAY -> may; | 53 | case MAY -> may; |
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 2e68fa3e..6ac3efc0 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/lifting/DnfLifter.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/lifting/DnfLifter.java | |||
@@ -5,9 +5,7 @@ | |||
5 | */ | 5 | */ |
6 | package tools.refinery.store.reasoning.lifting; | 6 | package tools.refinery.store.reasoning.lifting; |
7 | 7 | ||
8 | import tools.refinery.store.query.dnf.Dnf; | 8 | import tools.refinery.store.query.dnf.*; |
9 | import tools.refinery.store.query.dnf.DnfClause; | ||
10 | import tools.refinery.store.query.dnf.Query; | ||
11 | import tools.refinery.store.query.equality.DnfEqualityChecker; | 9 | import tools.refinery.store.query.equality.DnfEqualityChecker; |
12 | import tools.refinery.store.query.literal.Literal; | 10 | import tools.refinery.store.query.literal.Literal; |
13 | import tools.refinery.store.reasoning.literal.Concreteness; | 11 | import tools.refinery.store.reasoning.literal.Concreteness; |
@@ -25,6 +23,16 @@ public class DnfLifter { | |||
25 | return query.withDnf(liftedDnf); | 23 | return query.withDnf(liftedDnf); |
26 | } | 24 | } |
27 | 25 | ||
26 | public <T> RelationalQuery lift(Modality modality, Concreteness concreteness, RelationalQuery query) { | ||
27 | var liftedDnf = lift(modality, concreteness, query.getDnf()); | ||
28 | return query.withDnf(liftedDnf); | ||
29 | } | ||
30 | |||
31 | public <T> FunctionalQuery<T> lift(Modality modality, Concreteness concreteness, FunctionalQuery<T> query) { | ||
32 | var liftedDnf = lift(modality, concreteness, query.getDnf()); | ||
33 | return query.withDnf(liftedDnf); | ||
34 | } | ||
35 | |||
28 | public Dnf lift(Modality modality, Concreteness concreteness, Dnf dnf) { | 36 | public Dnf lift(Modality modality, Concreteness concreteness, Dnf dnf) { |
29 | return cache.computeIfAbsent(new ModalDnf(modality, concreteness, dnf), this::doLift); | 37 | return cache.computeIfAbsent(new ModalDnf(modality, concreteness, dnf), this::doLift); |
30 | } | 38 | } |
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/refinement/AbstractPartialInterpretationRefiner.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/refinement/AbstractPartialInterpretationRefiner.java new file mode 100644 index 00000000..a7fc5b7e --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/refinement/AbstractPartialInterpretationRefiner.java | |||
@@ -0,0 +1,29 @@ | |||
1 | /* | ||
2 | * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/> | ||
3 | * | ||
4 | * SPDX-License-Identifier: EPL-2.0 | ||
5 | */ | ||
6 | package tools.refinery.store.reasoning.refinement; | ||
7 | |||
8 | import tools.refinery.store.reasoning.ReasoningAdapter; | ||
9 | import tools.refinery.store.reasoning.representation.PartialSymbol; | ||
10 | |||
11 | public abstract class AbstractPartialInterpretationRefiner<A, C> implements PartialInterpretationRefiner<A, C> { | ||
12 | private final ReasoningAdapter adapter; | ||
13 | private final PartialSymbol<A, C> partialSymbol; | ||
14 | |||
15 | protected AbstractPartialInterpretationRefiner(ReasoningAdapter adapter, PartialSymbol<A, C> partialSymbol) { | ||
16 | this.adapter = adapter; | ||
17 | this.partialSymbol = partialSymbol; | ||
18 | } | ||
19 | |||
20 | @Override | ||
21 | public ReasoningAdapter getAdapter() { | ||
22 | return adapter; | ||
23 | } | ||
24 | |||
25 | @Override | ||
26 | public PartialSymbol<A, C> getPartialSymbol() { | ||
27 | return partialSymbol; | ||
28 | } | ||
29 | } | ||
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/refinement/ConcreteSymbolRefiner.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/refinement/ConcreteSymbolRefiner.java index 756118a0..ebb9b824 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/refinement/ConcreteSymbolRefiner.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/refinement/ConcreteSymbolRefiner.java | |||
@@ -13,39 +13,26 @@ import tools.refinery.store.tuple.Tuple; | |||
13 | 13 | ||
14 | import java.util.Objects; | 14 | import java.util.Objects; |
15 | 15 | ||
16 | public class ConcreteSymbolRefiner<A, C> implements PartialInterpretationRefiner<A, C> { | 16 | public class ConcreteSymbolRefiner<A, C> extends AbstractPartialInterpretationRefiner<A, C> { |
17 | private final ReasoningAdapter adapter; | ||
18 | private final PartialSymbol<A, C> partialSymbol; | ||
19 | private final Interpretation<A> interpretation; | 17 | private final Interpretation<A> interpretation; |
20 | 18 | ||
21 | public ConcreteSymbolRefiner(ReasoningAdapter adapter, PartialSymbol<A, C> partialSymbol, | 19 | public ConcreteSymbolRefiner(ReasoningAdapter adapter, PartialSymbol<A, C> partialSymbol, |
22 | Symbol<A> concreteSymbol) { | 20 | Symbol<A> concreteSymbol) { |
23 | this.adapter = adapter; | 21 | super(adapter, partialSymbol); |
24 | this.partialSymbol = partialSymbol; | ||
25 | interpretation = adapter.getModel().getInterpretation(concreteSymbol); | 22 | interpretation = adapter.getModel().getInterpretation(concreteSymbol); |
26 | } | 23 | } |
27 | 24 | ||
28 | @Override | 25 | @Override |
29 | public ReasoningAdapter getAdapter() { | ||
30 | return adapter; | ||
31 | } | ||
32 | |||
33 | @Override | ||
34 | public PartialSymbol<A, C> getPartialSymbol() { | ||
35 | return partialSymbol; | ||
36 | } | ||
37 | |||
38 | @Override | ||
39 | public boolean merge(Tuple key, A value) { | 26 | public boolean merge(Tuple key, A value) { |
40 | var currentValue = interpretation.get(key); | 27 | var currentValue = interpretation.get(key); |
41 | var mergedValue = partialSymbol.abstractDomain().commonRefinement(currentValue, value); | 28 | var mergedValue = getPartialSymbol().abstractDomain().commonRefinement(currentValue, value); |
42 | if (!Objects.equals(currentValue, mergedValue)) { | 29 | if (!Objects.equals(currentValue, mergedValue)) { |
43 | interpretation.put(key, mergedValue); | 30 | interpretation.put(key, mergedValue); |
44 | } | 31 | } |
45 | return true; | 32 | return true; |
46 | } | 33 | } |
47 | 34 | ||
48 | public static <A1, C1> PartialInterpretationRefiner.Factory<A1, C1> of(Symbol<A1> concreteSymbol) { | 35 | public static <A1, C1> Factory<A1, C1> of(Symbol<A1> concreteSymbol) { |
49 | return (adapter, partialSymbol) -> new ConcreteSymbolRefiner<>(adapter, partialSymbol, concreteSymbol); | 36 | return (adapter, partialSymbol) -> new ConcreteSymbolRefiner<>(adapter, partialSymbol, concreteSymbol); |
50 | } | 37 | } |
51 | } | 38 | } |
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/refinement/DefaultStorageRefiner.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/refinement/DefaultStorageRefiner.java index 0d7d6c5c..d4ec2e8b 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/refinement/DefaultStorageRefiner.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/refinement/DefaultStorageRefiner.java | |||
@@ -6,18 +6,17 @@ | |||
6 | package tools.refinery.store.reasoning.refinement; | 6 | package tools.refinery.store.reasoning.refinement; |
7 | 7 | ||
8 | import tools.refinery.store.model.Interpretation; | 8 | import tools.refinery.store.model.Interpretation; |
9 | import tools.refinery.store.model.Model; | ||
10 | import tools.refinery.store.representation.Symbol; | ||
9 | import tools.refinery.store.tuple.Tuple; | 11 | import tools.refinery.store.tuple.Tuple; |
10 | 12 | ||
11 | public class DefaultStorageRefiner<T> implements StorageRefiner { | 13 | public class DefaultStorageRefiner<T> implements StorageRefiner { |
12 | private static final StorageRefiner.Factory<Object> FACTORY = (symbol, model) -> { | 14 | private static final StorageRefiner.Factory<Object> FACTORY = DefaultStorageRefiner::new; |
13 | var interpretation = model.getInterpretation(symbol); | ||
14 | return new DefaultStorageRefiner<>(interpretation); | ||
15 | }; | ||
16 | 15 | ||
17 | private final Interpretation<T> interpretation; | 16 | private final Interpretation<T> interpretation; |
18 | 17 | ||
19 | public DefaultStorageRefiner(Interpretation<T> interpretation) { | 18 | public DefaultStorageRefiner(Symbol<T> symbol, Model model) { |
20 | this.interpretation = interpretation; | 19 | interpretation = model.getInterpretation(symbol); |
21 | } | 20 | } |
22 | 21 | ||
23 | @Override | 22 | @Override |
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/refinement/PartialModelInitializer.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/refinement/PartialModelInitializer.java index 79c1670f..0c82695c 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/refinement/PartialModelInitializer.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/refinement/PartialModelInitializer.java | |||
@@ -6,8 +6,9 @@ | |||
6 | package tools.refinery.store.reasoning.refinement; | 6 | package tools.refinery.store.reasoning.refinement; |
7 | 7 | ||
8 | import tools.refinery.store.model.Model; | 8 | import tools.refinery.store.model.Model; |
9 | import tools.refinery.store.reasoning.seed.ModelSeed; | ||
9 | 10 | ||
10 | @FunctionalInterface | 11 | @FunctionalInterface |
11 | public interface PartialModelInitializer { | 12 | public interface PartialModelInitializer { |
12 | void initialize(Model model, int nodeCount); | 13 | void initialize(Model model, ModelSeed modelSeed); |
13 | } | 14 | } |
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/seed/MapBasedSeed.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/seed/MapBasedSeed.java index b5a3d844..8b1c3bb3 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/seed/MapBasedSeed.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/seed/MapBasedSeed.java | |||
@@ -75,7 +75,7 @@ record MapBasedSeed<T>(int arity, Class<T> valueType, T reducedValue, Map<Tuple, | |||
75 | private boolean moveToNext() { | 75 | private boolean moveToNext() { |
76 | do { | 76 | do { |
77 | increment(); | 77 | increment(); |
78 | } while (!checkValue()); | 78 | } while (state != State.TERMINATED && !checkValue()); |
79 | return state != State.TERMINATED; | 79 | return state != State.TERMINATED; |
80 | } | 80 | } |
81 | 81 | ||
@@ -89,16 +89,10 @@ record MapBasedSeed<T>(int arity, Class<T> valueType, T reducedValue, Map<Tuple, | |||
89 | counter[i] = 0; | 89 | counter[i] = 0; |
90 | i--; | 90 | i--; |
91 | } | 91 | } |
92 | state = State.TERMINATED; | ||
92 | } | 93 | } |
93 | 94 | ||
94 | private boolean checkValue() { | 95 | private boolean checkValue() { |
95 | if (state == State.TERMINATED) { | ||
96 | return false; | ||
97 | } | ||
98 | if (counter[0] >= nodeCount) { | ||
99 | state = State.TERMINATED; | ||
100 | return false; | ||
101 | } | ||
102 | key = Tuple.of(counter); | 96 | key = Tuple.of(counter); |
103 | var valueInMap = map.get(key); | 97 | var valueInMap = map.get(key); |
104 | if (Objects.equals(valueInMap, defaultValue)) { | 98 | if (Objects.equals(valueInMap, defaultValue)) { |
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/seed/ModelSeed.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/seed/ModelSeed.java new file mode 100644 index 00000000..3641730d --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/seed/ModelSeed.java | |||
@@ -0,0 +1,86 @@ | |||
1 | /* | ||
2 | * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/> | ||
3 | * | ||
4 | * SPDX-License-Identifier: EPL-2.0 | ||
5 | */ | ||
6 | package tools.refinery.store.reasoning.seed; | ||
7 | |||
8 | import tools.refinery.store.map.Cursor; | ||
9 | import tools.refinery.store.reasoning.representation.AnyPartialSymbol; | ||
10 | import tools.refinery.store.reasoning.representation.PartialSymbol; | ||
11 | import tools.refinery.store.tuple.Tuple; | ||
12 | |||
13 | import java.util.Collections; | ||
14 | import java.util.LinkedHashMap; | ||
15 | import java.util.Map; | ||
16 | import java.util.function.Consumer; | ||
17 | |||
18 | public class ModelSeed { | ||
19 | private final int nodeCount; | ||
20 | private final Map<AnyPartialSymbol, Seed<?>> seeds; | ||
21 | |||
22 | private ModelSeed(int nodeCount, Map<AnyPartialSymbol, Seed<?>> seeds) { | ||
23 | this.nodeCount = nodeCount; | ||
24 | this.seeds = seeds; | ||
25 | } | ||
26 | |||
27 | public int getNodeCount() { | ||
28 | return nodeCount; | ||
29 | } | ||
30 | |||
31 | public <A> Seed<A> getSeed(PartialSymbol<A, ?> partialSymbol) { | ||
32 | var seed = seeds.get(partialSymbol); | ||
33 | if (seed == null) { | ||
34 | throw new IllegalArgumentException("No seed for partial symbol " + partialSymbol); | ||
35 | } | ||
36 | // The builder makes sure only well-typed seeds can be added. | ||
37 | @SuppressWarnings("unchecked") | ||
38 | var typedSeed = (Seed<A>) seed; | ||
39 | return typedSeed; | ||
40 | } | ||
41 | |||
42 | public <A> Cursor<Tuple, A> getCursor(PartialSymbol<A, ?> partialSymbol, A defaultValue) { | ||
43 | return getSeed(partialSymbol).getCursor(defaultValue, nodeCount); | ||
44 | } | ||
45 | |||
46 | public static Builder builder(int nodeCount) { | ||
47 | return new Builder(nodeCount); | ||
48 | } | ||
49 | |||
50 | public static class Builder { | ||
51 | private final int nodeCount; | ||
52 | private final Map<AnyPartialSymbol, Seed<?>> seeds = new LinkedHashMap<>(); | ||
53 | |||
54 | private Builder(int nodeCount) { | ||
55 | if (nodeCount < 0) { | ||
56 | throw new IllegalArgumentException("Node count must not be negative"); | ||
57 | } | ||
58 | this.nodeCount = nodeCount; | ||
59 | } | ||
60 | |||
61 | public <A> Builder seed(PartialSymbol<A, ?> partialSymbol, Seed<A> seed) { | ||
62 | if (seed.arity() != partialSymbol.arity()) { | ||
63 | throw new IllegalStateException("Expected seed of arity %d for partial symbol %s, but got %d instead" | ||
64 | .formatted(partialSymbol.arity(), partialSymbol, seed.arity())); | ||
65 | } | ||
66 | if (!seed.valueType().equals(partialSymbol.abstractDomain().abstractType())) { | ||
67 | throw new IllegalStateException("Expected seed of type %s for partial symbol %s, but got %s instead" | ||
68 | .formatted(partialSymbol.abstractDomain().abstractType(), partialSymbol, seed.valueType())); | ||
69 | } | ||
70 | if (seeds.put(partialSymbol, seed) != null) { | ||
71 | throw new IllegalArgumentException("Duplicate seed for partial symbol " + partialSymbol); | ||
72 | } | ||
73 | return this; | ||
74 | } | ||
75 | |||
76 | public <A> Builder seed(PartialSymbol<A, ?> partialSymbol, Consumer<Seed.Builder<A>> callback) { | ||
77 | var builder = Seed.builder(partialSymbol); | ||
78 | callback.accept(builder); | ||
79 | return seed(partialSymbol, builder.build()); | ||
80 | } | ||
81 | |||
82 | public ModelSeed build() { | ||
83 | return new ModelSeed(nodeCount, Collections.unmodifiableMap(seeds)); | ||
84 | } | ||
85 | } | ||
86 | } | ||
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 64b98683..732efbcc 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 | |||
@@ -42,7 +42,7 @@ public interface Seed<T> { | |||
42 | class Builder<T> { | 42 | class Builder<T> { |
43 | private final int arity; | 43 | private final int arity; |
44 | private final Class<T> valueType; | 44 | private final Class<T> valueType; |
45 | private final T reducedValue; | 45 | private T reducedValue; |
46 | private final Map<Tuple, T> map = new LinkedHashMap<>(); | 46 | private final Map<Tuple, T> map = new LinkedHashMap<>(); |
47 | 47 | ||
48 | private Builder(int arity, Class<T> valueType, T reducedValue) { | 48 | private Builder(int arity, Class<T> valueType, T reducedValue) { |
@@ -51,6 +51,11 @@ public interface Seed<T> { | |||
51 | this.reducedValue = reducedValue; | 51 | this.reducedValue = reducedValue; |
52 | } | 52 | } |
53 | 53 | ||
54 | public Builder<T> reducedValue(T reducedValue) { | ||
55 | this.reducedValue = reducedValue; | ||
56 | return this; | ||
57 | } | ||
58 | |||
54 | public Builder<T> put(Tuple key, T value) { | 59 | public Builder<T> put(Tuple key, T value) { |
55 | if (key.getSize() != arity) { | 60 | if (key.getSize() != arity) { |
56 | throw new IllegalArgumentException("Expected %s to have %d elements".formatted(key, arity)); | 61 | throw new IllegalArgumentException("Expected %s to have %d elements".formatted(key, arity)); |
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/seed/SeedInitializer.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/seed/SeedInitializer.java index 884d6515..9af457d8 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/seed/SeedInitializer.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/seed/SeedInitializer.java | |||
@@ -7,21 +7,22 @@ package tools.refinery.store.reasoning.seed; | |||
7 | 7 | ||
8 | import tools.refinery.store.model.Model; | 8 | import tools.refinery.store.model.Model; |
9 | import tools.refinery.store.reasoning.refinement.PartialModelInitializer; | 9 | import tools.refinery.store.reasoning.refinement.PartialModelInitializer; |
10 | import tools.refinery.store.reasoning.representation.PartialSymbol; | ||
10 | import tools.refinery.store.representation.Symbol; | 11 | import tools.refinery.store.representation.Symbol; |
11 | 12 | ||
12 | public class SeedInitializer<T> implements PartialModelInitializer { | 13 | public class SeedInitializer<T> implements PartialModelInitializer { |
13 | private final Symbol<T> symbol; | 14 | private final Symbol<T> symbol; |
14 | private final Seed<T> seed; | 15 | private final PartialSymbol<T, ?> partialSymbol; |
15 | 16 | ||
16 | public SeedInitializer(Symbol<T> symbol, Seed<T> seed) { | 17 | public SeedInitializer(Symbol<T> symbol, PartialSymbol<T, ?> partialSymbol) { |
17 | this.symbol = symbol; | 18 | this.symbol = symbol; |
18 | this.seed = seed; | 19 | this.partialSymbol = partialSymbol; |
19 | } | 20 | } |
20 | 21 | ||
21 | @Override | 22 | @Override |
22 | public void initialize(Model model, int nodeCount) { | 23 | public void initialize(Model model, ModelSeed modelSeed) { |
23 | var interpretation = model.getInterpretation(symbol); | 24 | var interpretation = model.getInterpretation(symbol); |
24 | var cursor = seed.getCursor(symbol.defaultValue(), nodeCount); | 25 | var cursor = modelSeed.getCursor(partialSymbol, symbol.defaultValue()); |
25 | interpretation.putAll(cursor); | 26 | interpretation.putAll(cursor); |
26 | } | 27 | } |
27 | } | 28 | } |
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/PartialRelationTranslator.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/PartialRelationTranslator.java index fe8e8d6c..aee74eb3 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/PartialRelationTranslator.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/PartialRelationTranslator.java | |||
@@ -32,11 +32,11 @@ import tools.refinery.store.representation.TruthValue; | |||
32 | public final class PartialRelationTranslator extends PartialSymbolTranslator<TruthValue, Boolean> { | 32 | public final class PartialRelationTranslator extends PartialSymbolTranslator<TruthValue, Boolean> { |
33 | private final PartialRelation partialRelation; | 33 | private final PartialRelation partialRelation; |
34 | private PartialRelationRewriter rewriter; | 34 | private PartialRelationRewriter rewriter; |
35 | private Query<Boolean> query; | 35 | private RelationalQuery query; |
36 | private Query<Boolean> may; | 36 | private RelationalQuery may; |
37 | private Query<Boolean> must; | 37 | private RelationalQuery must; |
38 | private Query<Boolean> candidateMay; | 38 | private RelationalQuery candidateMay; |
39 | private Query<Boolean> candidateMust; | 39 | private RelationalQuery candidateMust; |
40 | private RoundingMode roundingMode; | 40 | private RoundingMode roundingMode; |
41 | 41 | ||
42 | private PartialRelationTranslator(PartialRelation partialRelation) { | 42 | private PartialRelationTranslator(PartialRelation partialRelation) { |
@@ -197,20 +197,41 @@ public final class PartialRelationTranslator extends PartialSymbolTranslator<Tru | |||
197 | } | 197 | } |
198 | 198 | ||
199 | private void liftQueries(ModelStoreBuilder storeBuilder) { | 199 | private void liftQueries(ModelStoreBuilder storeBuilder) { |
200 | if (query != null) { | 200 | if (rewriter instanceof QueryBasedRelationRewriter queryBasedRelationRewriter) { |
201 | var reasoningBuilder = storeBuilder.getAdapter(ReasoningBuilder.class); | 201 | liftQueriesFromQueryBasedRewriter(queryBasedRelationRewriter); |
202 | if (may == null) { | 202 | } else if (query != null) { |
203 | may = reasoningBuilder.lift(Modality.MAY, Concreteness.PARTIAL, query); | 203 | liftQueriesFromFourValuedQuery(storeBuilder); |
204 | } | 204 | } |
205 | if (must == null) { | 205 | } |
206 | must = reasoningBuilder.lift(Modality.MUST, Concreteness.PARTIAL, query); | 206 | |
207 | } | 207 | private void liftQueriesFromQueryBasedRewriter(QueryBasedRelationRewriter queryBasedRelationRewriter) { |
208 | if (candidateMay == null) { | 208 | if (may == null) { |
209 | candidateMay = reasoningBuilder.lift(Modality.MAY, Concreteness.CANDIDATE, query); | 209 | may = queryBasedRelationRewriter.getMay(); |
210 | } | 210 | } |
211 | if (candidateMust == null) { | 211 | if (must == null) { |
212 | candidateMust = reasoningBuilder.lift(Modality.MAY, Concreteness.CANDIDATE, query); | 212 | must = queryBasedRelationRewriter.getMust(); |
213 | } | 213 | } |
214 | if (candidateMay == null) { | ||
215 | candidateMay = queryBasedRelationRewriter.getCandidateMay(); | ||
216 | } | ||
217 | if (candidateMust == null) { | ||
218 | candidateMust = queryBasedRelationRewriter.getCandidateMust(); | ||
219 | } | ||
220 | } | ||
221 | |||
222 | private void liftQueriesFromFourValuedQuery(ModelStoreBuilder storeBuilder) { | ||
223 | var reasoningBuilder = storeBuilder.getAdapter(ReasoningBuilder.class); | ||
224 | if (may == null) { | ||
225 | may = reasoningBuilder.lift(Modality.MAY, Concreteness.PARTIAL, query); | ||
226 | } | ||
227 | if (must == null) { | ||
228 | must = reasoningBuilder.lift(Modality.MUST, Concreteness.PARTIAL, query); | ||
229 | } | ||
230 | if (candidateMay == null) { | ||
231 | candidateMay = reasoningBuilder.lift(Modality.MAY, Concreteness.CANDIDATE, query); | ||
232 | } | ||
233 | if (candidateMust == null) { | ||
234 | candidateMust = reasoningBuilder.lift(Modality.MAY, Concreteness.CANDIDATE, query); | ||
214 | } | 235 | } |
215 | } | 236 | } |
216 | 237 | ||
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/PartialSymbolTranslator.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/PartialSymbolTranslator.java index 07d1d19b..542acdb3 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/PartialSymbolTranslator.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/PartialSymbolTranslator.java | |||
@@ -12,7 +12,6 @@ import tools.refinery.store.reasoning.refinement.PartialInterpretationRefiner; | |||
12 | import tools.refinery.store.reasoning.refinement.PartialModelInitializer; | 12 | import tools.refinery.store.reasoning.refinement.PartialModelInitializer; |
13 | import tools.refinery.store.reasoning.refinement.StorageRefiner; | 13 | import tools.refinery.store.reasoning.refinement.StorageRefiner; |
14 | import tools.refinery.store.reasoning.representation.PartialSymbol; | 14 | import tools.refinery.store.reasoning.representation.PartialSymbol; |
15 | import tools.refinery.store.reasoning.seed.Seed; | ||
16 | import tools.refinery.store.reasoning.seed.SeedInitializer; | 15 | import tools.refinery.store.reasoning.seed.SeedInitializer; |
17 | import tools.refinery.store.representation.AnySymbol; | 16 | import tools.refinery.store.representation.AnySymbol; |
18 | import tools.refinery.store.representation.Symbol; | 17 | import tools.refinery.store.representation.Symbol; |
@@ -100,20 +99,6 @@ public abstract sealed class PartialSymbolTranslator<A, C> implements AnyPartial | |||
100 | return this; | 99 | return this; |
101 | } | 100 | } |
102 | 101 | ||
103 | public <T> PartialSymbolTranslator<A, C> seed(Seed<T> seed) { | ||
104 | if (storageSymbol == null) { | ||
105 | throw new IllegalArgumentException("Seed requires setting a storage symbol"); | ||
106 | } | ||
107 | if (!seed.valueType().equals(storageSymbol.valueType())) { | ||
108 | throw new IllegalArgumentException("Seed type %s does not match storage symbol type %s" | ||
109 | .formatted(seed.valueType(), storageSymbol.valueType())); | ||
110 | } | ||
111 | // The guard clause only allows a well-typed seed. | ||
112 | @SuppressWarnings("unchecked") | ||
113 | var typedStorageSymbol = (Symbol<T>) storageSymbol; | ||
114 | return initializer(new SeedInitializer<>(typedStorageSymbol, seed)); | ||
115 | } | ||
116 | |||
117 | @Override | 102 | @Override |
118 | public void configure(ModelStoreBuilder storeBuilder) { | 103 | public void configure(ModelStoreBuilder storeBuilder) { |
119 | checkNotConfigured(); | 104 | checkNotConfigured(); |
@@ -132,6 +117,7 @@ public abstract sealed class PartialSymbolTranslator<A, C> implements AnyPartial | |||
132 | registerStorageRefiner(reasoningBuilder, storageRefiner); | 117 | registerStorageRefiner(reasoningBuilder, storageRefiner); |
133 | } | 118 | } |
134 | } | 119 | } |
120 | createFallbackInitializer(); | ||
135 | if (initializer != null) { | 121 | if (initializer != null) { |
136 | reasoningBuilder.initializer(initializer); | 122 | reasoningBuilder.initializer(initializer); |
137 | } | 123 | } |
@@ -144,6 +130,17 @@ public abstract sealed class PartialSymbolTranslator<A, C> implements AnyPartial | |||
144 | reasoningBuilder.storageRefiner(typedStorageSymbol, factory); | 130 | reasoningBuilder.storageRefiner(typedStorageSymbol, factory); |
145 | } | 131 | } |
146 | 132 | ||
133 | private void createFallbackInitializer() { | ||
134 | if (initializer == null && | ||
135 | storageSymbol != null && | ||
136 | storageSymbol.valueType().equals(partialSymbol.abstractDomain().abstractType())) { | ||
137 | // The guard clause makes this safe. | ||
138 | @SuppressWarnings("unchecked") | ||
139 | var typedStorageSymbol = (Symbol<A>) storageSymbol; | ||
140 | initializer = new SeedInitializer<>(typedStorageSymbol, partialSymbol); | ||
141 | } | ||
142 | } | ||
143 | |||
147 | public PartialInterpretation.Factory<A, C> getInterpretationFactory() { | 144 | public PartialInterpretation.Factory<A, C> getInterpretationFactory() { |
148 | checkConfigured(); | 145 | checkConfigured(); |
149 | return interpretationFactory; | 146 | return interpretationFactory; |
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiobject/EqualsRefiner.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiobject/EqualsRefiner.java new file mode 100644 index 00000000..d8db4ec4 --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiobject/EqualsRefiner.java | |||
@@ -0,0 +1,64 @@ | |||
1 | /* | ||
2 | * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/> | ||
3 | * | ||
4 | * SPDX-License-Identifier: EPL-2.0 | ||
5 | */ | ||
6 | package tools.refinery.store.reasoning.translator.multiobject; | ||
7 | |||
8 | import tools.refinery.store.model.Interpretation; | ||
9 | import tools.refinery.store.reasoning.ReasoningAdapter; | ||
10 | import tools.refinery.store.reasoning.refinement.AbstractPartialInterpretationRefiner; | ||
11 | import tools.refinery.store.reasoning.representation.PartialSymbol; | ||
12 | import tools.refinery.store.representation.Symbol; | ||
13 | import tools.refinery.store.representation.TruthValue; | ||
14 | import tools.refinery.store.representation.cardinality.CardinalityInterval; | ||
15 | import tools.refinery.store.representation.cardinality.CardinalityIntervals; | ||
16 | import tools.refinery.store.tuple.Tuple; | ||
17 | |||
18 | public class EqualsRefiner extends AbstractPartialInterpretationRefiner<TruthValue, Boolean> { | ||
19 | private final Interpretation<CardinalityInterval> countInterpretation; | ||
20 | |||
21 | private EqualsRefiner(ReasoningAdapter adapter, PartialSymbol<TruthValue, Boolean> partialSymbol, | ||
22 | Symbol<CardinalityInterval> countSymbol) { | ||
23 | super(adapter, partialSymbol); | ||
24 | countInterpretation = adapter.getModel().getInterpretation(countSymbol); | ||
25 | } | ||
26 | |||
27 | @Override | ||
28 | public boolean merge(Tuple key, TruthValue value) { | ||
29 | if (value == TruthValue.UNKNOWN) { | ||
30 | return true; | ||
31 | } | ||
32 | if (value == TruthValue.ERROR) { | ||
33 | return false; | ||
34 | } | ||
35 | int left = key.get(0); | ||
36 | int right = key.get(1); | ||
37 | boolean isDiagonal = left == right; | ||
38 | if (isDiagonal && value == TruthValue.FALSE) { | ||
39 | return false; | ||
40 | } | ||
41 | if (!isDiagonal) { | ||
42 | return !value.may(); | ||
43 | } | ||
44 | if (value != TruthValue.TRUE) { | ||
45 | throw new IllegalArgumentException("Unknown TruthValue: " + value); | ||
46 | } | ||
47 | // {@code isDiagonal} is true, so this could be {@code left} or {@code right}. | ||
48 | var unaryKey = Tuple.of(left); | ||
49 | var currentCount = countInterpretation.get(unaryKey); | ||
50 | if (currentCount == null) { | ||
51 | return false; | ||
52 | } | ||
53 | var newCount = currentCount.meet(CardinalityIntervals.LONE); | ||
54 | if (newCount.isEmpty()) { | ||
55 | return false; | ||
56 | } | ||
57 | countInterpretation.put(unaryKey, newCount); | ||
58 | return true; | ||
59 | } | ||
60 | |||
61 | public static Factory<TruthValue, Boolean> of(Symbol<CardinalityInterval> countSymbol) { | ||
62 | return (adapter, partialSymbol) -> new EqualsRefiner(adapter, partialSymbol, countSymbol); | ||
63 | } | ||
64 | } | ||
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiobject/EqualsRelationRewriter.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiobject/EqualsRelationRewriter.java new file mode 100644 index 00000000..c7bc9fff --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiobject/EqualsRelationRewriter.java | |||
@@ -0,0 +1,84 @@ | |||
1 | /* | ||
2 | * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/> | ||
3 | * | ||
4 | * SPDX-License-Identifier: EPL-2.0 | ||
5 | */ | ||
6 | package tools.refinery.store.reasoning.translator.multiobject; | ||
7 | |||
8 | import tools.refinery.store.query.dnf.Query; | ||
9 | import tools.refinery.store.query.dnf.RelationalQuery; | ||
10 | import tools.refinery.store.query.literal.AbstractCallLiteral; | ||
11 | import tools.refinery.store.query.literal.CallLiteral; | ||
12 | import tools.refinery.store.query.literal.Literal; | ||
13 | import tools.refinery.store.query.term.Variable; | ||
14 | import tools.refinery.store.reasoning.interpretation.QueryBasedRelationRewriter; | ||
15 | import tools.refinery.store.reasoning.literal.Concreteness; | ||
16 | import tools.refinery.store.reasoning.literal.Modality; | ||
17 | import tools.refinery.store.representation.cardinality.UpperCardinalities; | ||
18 | import tools.refinery.store.representation.cardinality.UpperCardinality; | ||
19 | |||
20 | import java.util.List; | ||
21 | import java.util.Set; | ||
22 | |||
23 | import static tools.refinery.store.query.literal.Literals.check; | ||
24 | import static tools.refinery.store.query.term.uppercardinality.UpperCardinalityTerms.constant; | ||
25 | import static tools.refinery.store.query.term.uppercardinality.UpperCardinalityTerms.lessEq; | ||
26 | |||
27 | class EqualsRelationRewriter extends QueryBasedRelationRewriter { | ||
28 | private EqualsRelationRewriter(RelationalQuery may, RelationalQuery must) { | ||
29 | super(may, must, may, may); | ||
30 | } | ||
31 | |||
32 | @Override | ||
33 | public List<Literal> rewriteLiteral(Set<Variable> positiveVariables, AbstractCallLiteral literal, | ||
34 | Modality modality, Concreteness concreteness) { | ||
35 | if (!(literal instanceof CallLiteral callLiteral)) { | ||
36 | return super.rewriteLiteral(positiveVariables, literal, modality, concreteness); | ||
37 | } | ||
38 | var left = callLiteral.getArguments().get(0).asNodeVariable(); | ||
39 | var right = callLiteral.getArguments().get(1).asNodeVariable(); | ||
40 | boolean useMay = modality == Modality.MAY || concreteness == Concreteness.CANDIDATE; | ||
41 | return switch (callLiteral.getPolarity()) { | ||
42 | case POSITIVE, TRANSITIVE -> { | ||
43 | if (useMay) { | ||
44 | if (positiveVariables.contains(left) || positiveVariables.contains(right)) { | ||
45 | // No need to enumerate arguments if at least one is already bound, since they will be unified. | ||
46 | yield List.of(left.isEquivalent(right)); | ||
47 | } else { | ||
48 | yield List.of( | ||
49 | left.isEquivalent(right), | ||
50 | getMay().call(left, right) | ||
51 | ); | ||
52 | } | ||
53 | } else { | ||
54 | yield List.of( | ||
55 | left.isEquivalent(right), | ||
56 | getMust().call(left, right) | ||
57 | ); | ||
58 | } | ||
59 | } | ||
60 | case NEGATIVE -> { | ||
61 | if (useMay) { | ||
62 | yield List.of(left.notEquivalent(right)); | ||
63 | } else { | ||
64 | yield super.rewriteLiteral(positiveVariables, literal, modality, concreteness); | ||
65 | } | ||
66 | } | ||
67 | }; | ||
68 | } | ||
69 | |||
70 | public static EqualsRelationRewriter of(UpperCardinalityView upperCardinalityView) { | ||
71 | var may = Query.of("MAY_EQUALS", (builder, p1, p2) -> builder | ||
72 | .clause( | ||
73 | p1.isEquivalent(p2), | ||
74 | upperCardinalityView.call(p1, Variable.of(UpperCardinality.class)) | ||
75 | )); | ||
76 | var must = Query.of("MUST_EQUALS", (builder, p1, p2) -> builder | ||
77 | .clause(UpperCardinality.class, upper -> List.of( | ||
78 | p1.isEquivalent(p2), | ||
79 | upperCardinalityView.call(p1, upper), | ||
80 | check(lessEq(upper, constant(UpperCardinalities.ONE))) | ||
81 | ))); | ||
82 | return new EqualsRelationRewriter(may, must); | ||
83 | } | ||
84 | } | ||
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiobject/ExistsRefiner.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiobject/ExistsRefiner.java new file mode 100644 index 00000000..f134fe92 --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiobject/ExistsRefiner.java | |||
@@ -0,0 +1,55 @@ | |||
1 | /* | ||
2 | * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/> | ||
3 | * | ||
4 | * SPDX-License-Identifier: EPL-2.0 | ||
5 | */ | ||
6 | package tools.refinery.store.reasoning.translator.multiobject; | ||
7 | |||
8 | import tools.refinery.store.model.Interpretation; | ||
9 | import tools.refinery.store.reasoning.ReasoningAdapter; | ||
10 | import tools.refinery.store.reasoning.refinement.AbstractPartialInterpretationRefiner; | ||
11 | import tools.refinery.store.reasoning.representation.PartialSymbol; | ||
12 | import tools.refinery.store.representation.Symbol; | ||
13 | import tools.refinery.store.representation.TruthValue; | ||
14 | import tools.refinery.store.representation.cardinality.CardinalityInterval; | ||
15 | import tools.refinery.store.representation.cardinality.CardinalityIntervals; | ||
16 | import tools.refinery.store.tuple.Tuple; | ||
17 | |||
18 | public class ExistsRefiner extends AbstractPartialInterpretationRefiner<TruthValue, Boolean> { | ||
19 | private final Interpretation<CardinalityInterval> countInterpretation; | ||
20 | |||
21 | private ExistsRefiner(ReasoningAdapter adapter, PartialSymbol<TruthValue, Boolean> partialSymbol, | ||
22 | Symbol<CardinalityInterval> countSymbol) { | ||
23 | super(adapter, partialSymbol); | ||
24 | countInterpretation = adapter.getModel().getInterpretation(countSymbol); | ||
25 | } | ||
26 | |||
27 | @Override | ||
28 | public boolean merge(Tuple key, TruthValue value) { | ||
29 | var currentCount = countInterpretation.get(key); | ||
30 | if (currentCount == null) { | ||
31 | return false; | ||
32 | } | ||
33 | CardinalityInterval newCount; | ||
34 | switch (value) { | ||
35 | case UNKNOWN -> { | ||
36 | return true; | ||
37 | } | ||
38 | case TRUE -> newCount = currentCount.meet(CardinalityIntervals.SOME); | ||
39 | case FALSE -> newCount = currentCount.meet(CardinalityIntervals.NONE); | ||
40 | case ERROR -> { | ||
41 | return false; | ||
42 | } | ||
43 | default -> throw new IllegalArgumentException("Unknown TruthValue: " + value); | ||
44 | } | ||
45 | if (newCount.isEmpty()) { | ||
46 | return false; | ||
47 | } | ||
48 | countInterpretation.put(key, newCount); | ||
49 | return true; | ||
50 | } | ||
51 | |||
52 | public static Factory<TruthValue, Boolean> of(Symbol<CardinalityInterval> countSymbol) { | ||
53 | return (adapter, partialSymbol) -> new ExistsRefiner(adapter, partialSymbol, countSymbol); | ||
54 | } | ||
55 | } | ||
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiobject/LowerCardinalityView.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiobject/LowerCardinalityView.java new file mode 100644 index 00000000..9873888c --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiobject/LowerCardinalityView.java | |||
@@ -0,0 +1,22 @@ | |||
1 | /* | ||
2 | * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/> | ||
3 | * | ||
4 | * SPDX-License-Identifier: EPL-2.0 | ||
5 | */ | ||
6 | package tools.refinery.store.reasoning.translator.multiobject; | ||
7 | |||
8 | import tools.refinery.store.query.term.Parameter; | ||
9 | import tools.refinery.store.query.view.AbstractFunctionView; | ||
10 | import tools.refinery.store.representation.Symbol; | ||
11 | import tools.refinery.store.representation.cardinality.CardinalityInterval; | ||
12 | |||
13 | class LowerCardinalityView extends AbstractFunctionView<CardinalityInterval> { | ||
14 | public LowerCardinalityView(Symbol<CardinalityInterval> symbol) { | ||
15 | super(symbol, "lower", new Parameter(Integer.class)); | ||
16 | } | ||
17 | |||
18 | @Override | ||
19 | protected Object forwardMapValue(CardinalityInterval value) { | ||
20 | return value.lowerBound(); | ||
21 | } | ||
22 | } | ||
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiobject/MultiObjectInitializer.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiobject/MultiObjectInitializer.java new file mode 100644 index 00000000..6917b8ed --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiobject/MultiObjectInitializer.java | |||
@@ -0,0 +1,93 @@ | |||
1 | /* | ||
2 | * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/> | ||
3 | * | ||
4 | * SPDX-License-Identifier: EPL-2.0 | ||
5 | */ | ||
6 | package tools.refinery.store.reasoning.translator.multiobject; | ||
7 | |||
8 | import tools.refinery.store.model.Model; | ||
9 | import tools.refinery.store.reasoning.ReasoningAdapter; | ||
10 | import tools.refinery.store.reasoning.refinement.PartialModelInitializer; | ||
11 | import tools.refinery.store.reasoning.seed.ModelSeed; | ||
12 | import tools.refinery.store.representation.Symbol; | ||
13 | import tools.refinery.store.representation.TruthValue; | ||
14 | import tools.refinery.store.representation.cardinality.CardinalityInterval; | ||
15 | import tools.refinery.store.representation.cardinality.CardinalityIntervals; | ||
16 | import tools.refinery.store.tuple.Tuple; | ||
17 | |||
18 | import java.util.Arrays; | ||
19 | |||
20 | class MultiObjectInitializer implements PartialModelInitializer { | ||
21 | private final Symbol<CardinalityInterval> countSymbol; | ||
22 | |||
23 | public MultiObjectInitializer(Symbol<CardinalityInterval> countSymbol) { | ||
24 | this.countSymbol = countSymbol; | ||
25 | } | ||
26 | |||
27 | @Override | ||
28 | public void initialize(Model model, ModelSeed modelSeed) { | ||
29 | var intervals = new CardinalityInterval[modelSeed.getNodeCount()]; | ||
30 | Arrays.fill(intervals, CardinalityIntervals.SET); | ||
31 | initializeExists(intervals, modelSeed); | ||
32 | initializeEquals(intervals, modelSeed); | ||
33 | var countInterpretation = model.getInterpretation(countSymbol); | ||
34 | for (int i = 0; i < intervals.length; i++) { | ||
35 | var interval = intervals[i]; | ||
36 | if (interval.isEmpty()) { | ||
37 | throw new IllegalArgumentException("Inconsistent existence or equality for node " + i); | ||
38 | } | ||
39 | countInterpretation.put(Tuple.of(i), intervals[i]); | ||
40 | } | ||
41 | } | ||
42 | |||
43 | private void initializeExists(CardinalityInterval[] intervals, ModelSeed modelSeed) { | ||
44 | var cursor = modelSeed.getCursor(ReasoningAdapter.EXISTS_SYMBOL, TruthValue.UNKNOWN); | ||
45 | while (cursor.move()) { | ||
46 | int i = cursor.getKey().get(0); | ||
47 | checkNodeId(intervals, i); | ||
48 | switch (cursor.getValue()) { | ||
49 | case TRUE -> intervals[i] = intervals[i].meet(CardinalityIntervals.SOME); | ||
50 | case FALSE -> intervals[i] = intervals[i].meet(CardinalityIntervals.NONE); | ||
51 | case ERROR -> throw new IllegalArgumentException("Inconsistent existence for node " + i); | ||
52 | default -> throw new IllegalArgumentException("Invalid existence truth value %s for node %d" | ||
53 | .formatted(cursor.getValue(), i)); | ||
54 | } | ||
55 | } | ||
56 | } | ||
57 | |||
58 | private void initializeEquals(CardinalityInterval[] intervals, ModelSeed modelSeed) { | ||
59 | var seed = modelSeed.getSeed(ReasoningAdapter.EQUALS_SYMBOL); | ||
60 | var cursor = seed.getCursor(TruthValue.FALSE, modelSeed.getNodeCount()); | ||
61 | while (cursor.move()) { | ||
62 | var key = cursor.getKey(); | ||
63 | int i = key.get(0); | ||
64 | int otherIndex = key.get(1); | ||
65 | if (i != otherIndex) { | ||
66 | throw new IllegalArgumentException("Off-diagonal equivalence (%d, %d) is not permitted" | ||
67 | .formatted(i, otherIndex)); | ||
68 | } | ||
69 | checkNodeId(intervals, i); | ||
70 | switch (cursor.getValue()) { | ||
71 | case TRUE -> intervals[i] = intervals[i].meet(CardinalityIntervals.LONE); | ||
72 | case UNKNOWN -> { | ||
73 | // Nothing do to, {@code intervals} is initialized with unknown equality. | ||
74 | } | ||
75 | case ERROR -> throw new IllegalArgumentException("Inconsistent equality for node " + i); | ||
76 | default -> throw new IllegalArgumentException("Invalid equality truth value %s for node %d" | ||
77 | .formatted(cursor.getValue(), i)); | ||
78 | } | ||
79 | } | ||
80 | for (int i = 0; i < intervals.length; i++) { | ||
81 | if (seed.get(Tuple.of(i, i)) == TruthValue.FALSE) { | ||
82 | throw new IllegalArgumentException("Inconsistent equality for node " + i); | ||
83 | } | ||
84 | } | ||
85 | } | ||
86 | |||
87 | private void checkNodeId(CardinalityInterval[] intervals, int nodeId) { | ||
88 | if (nodeId < 0 || nodeId >= intervals.length) { | ||
89 | throw new IllegalArgumentException("Expected node id %d to be lower than model size %d" | ||
90 | .formatted(nodeId, intervals.length)); | ||
91 | } | ||
92 | } | ||
93 | } | ||
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiobject/MultiObjectStorageRefiner.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiobject/MultiObjectStorageRefiner.java new file mode 100644 index 00000000..e48934d8 --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiobject/MultiObjectStorageRefiner.java | |||
@@ -0,0 +1,45 @@ | |||
1 | /* | ||
2 | * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/> | ||
3 | * | ||
4 | * SPDX-License-Identifier: EPL-2.0 | ||
5 | */ | ||
6 | package tools.refinery.store.reasoning.translator.multiobject; | ||
7 | |||
8 | import tools.refinery.store.model.Interpretation; | ||
9 | import tools.refinery.store.model.Model; | ||
10 | import tools.refinery.store.reasoning.refinement.StorageRefiner; | ||
11 | import tools.refinery.store.representation.Symbol; | ||
12 | import tools.refinery.store.representation.cardinality.CardinalityInterval; | ||
13 | import tools.refinery.store.representation.cardinality.CardinalityIntervals; | ||
14 | import tools.refinery.store.tuple.Tuple; | ||
15 | |||
16 | class MultiObjectStorageRefiner implements StorageRefiner { | ||
17 | private final Interpretation<CardinalityInterval> countInterpretation; | ||
18 | |||
19 | public MultiObjectStorageRefiner(Symbol<CardinalityInterval> countSymbol, Model model) { | ||
20 | countInterpretation = model.getInterpretation(countSymbol); | ||
21 | } | ||
22 | |||
23 | @Override | ||
24 | public boolean split(int parentNode, int childNode) { | ||
25 | var parentKey = Tuple.of(parentNode); | ||
26 | var parentCount = countInterpretation.get(parentKey); | ||
27 | if (parentCount == null) { | ||
28 | return false; | ||
29 | } | ||
30 | var newParentCount = parentCount.take(1); | ||
31 | if (newParentCount.isEmpty()) { | ||
32 | return false; | ||
33 | } | ||
34 | var childKey = Tuple.of(childNode); | ||
35 | countInterpretation.put(parentKey, newParentCount); | ||
36 | countInterpretation.put(childKey, CardinalityIntervals.ONE); | ||
37 | return true; | ||
38 | } | ||
39 | |||
40 | @Override | ||
41 | public boolean cleanup(int nodeToDelete) { | ||
42 | var previousCount = countInterpretation.put(Tuple.of(nodeToDelete), null); | ||
43 | return previousCount.lowerBound() == 0; | ||
44 | } | ||
45 | } | ||
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiobject/MultiObjectTranslator.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiobject/MultiObjectTranslator.java new file mode 100644 index 00000000..0367214b --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiobject/MultiObjectTranslator.java | |||
@@ -0,0 +1,60 @@ | |||
1 | /* | ||
2 | * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/> | ||
3 | * | ||
4 | * SPDX-License-Identifier: EPL-2.0 | ||
5 | */ | ||
6 | package tools.refinery.store.reasoning.translator.multiobject; | ||
7 | |||
8 | import tools.refinery.store.model.ModelStoreBuilder; | ||
9 | import tools.refinery.store.model.ModelStoreConfiguration; | ||
10 | import tools.refinery.store.query.dnf.Query; | ||
11 | import tools.refinery.store.reasoning.ReasoningAdapter; | ||
12 | import tools.refinery.store.reasoning.ReasoningBuilder; | ||
13 | import tools.refinery.store.reasoning.translator.PartialRelationTranslator; | ||
14 | import tools.refinery.store.reasoning.translator.RoundingMode; | ||
15 | import tools.refinery.store.representation.Symbol; | ||
16 | import tools.refinery.store.representation.cardinality.CardinalityInterval; | ||
17 | import tools.refinery.store.representation.cardinality.UpperCardinalities; | ||
18 | import tools.refinery.store.representation.cardinality.UpperCardinality; | ||
19 | |||
20 | import java.util.List; | ||
21 | |||
22 | import static tools.refinery.store.query.literal.Literals.check; | ||
23 | import static tools.refinery.store.query.term.int_.IntTerms.constant; | ||
24 | import static tools.refinery.store.query.term.int_.IntTerms.greaterEq; | ||
25 | import static tools.refinery.store.query.term.uppercardinality.UpperCardinalityTerms.constant; | ||
26 | import static tools.refinery.store.query.term.uppercardinality.UpperCardinalityTerms.greaterEq; | ||
27 | |||
28 | public class MultiObjectTranslator implements ModelStoreConfiguration { | ||
29 | private final Symbol<CardinalityInterval> countSymbol = Symbol.of("COUNT", 1, CardinalityInterval.class, | ||
30 | null); | ||
31 | private final LowerCardinalityView lowerCardinalityView = new LowerCardinalityView(countSymbol); | ||
32 | private final UpperCardinalityView upperCardinalityView = new UpperCardinalityView(countSymbol); | ||
33 | |||
34 | @Override | ||
35 | public void apply(ModelStoreBuilder storeBuilder) { | ||
36 | storeBuilder.symbol(countSymbol); | ||
37 | |||
38 | storeBuilder.with(PartialRelationTranslator.of(ReasoningAdapter.EXISTS_SYMBOL) | ||
39 | .may(Query.of("MAY_EXISTS", (builder, p1) -> builder | ||
40 | .clause(UpperCardinality.class, upper -> List.of( | ||
41 | upperCardinalityView.call(p1, upper), | ||
42 | check(greaterEq(upper, constant(UpperCardinalities.ONE))) | ||
43 | )))) | ||
44 | .must(Query.of("MUST_EXISTS", (builder, p1) -> builder | ||
45 | .clause(Integer.class, lower -> List.of( | ||
46 | lowerCardinalityView.call(p1, lower), | ||
47 | check(greaterEq(lower, constant(1))) | ||
48 | )))) | ||
49 | .roundingMode(RoundingMode.PREFER_FALSE) | ||
50 | .refiner(ExistsRefiner.of(countSymbol))); | ||
51 | |||
52 | storeBuilder.with(PartialRelationTranslator.of(ReasoningAdapter.EQUALS_SYMBOL) | ||
53 | .rewriter(EqualsRelationRewriter.of(upperCardinalityView)) | ||
54 | .refiner(EqualsRefiner.of(countSymbol))); | ||
55 | |||
56 | var reasoningBuilder = storeBuilder.getAdapter(ReasoningBuilder.class); | ||
57 | reasoningBuilder.initializer(new MultiObjectInitializer(countSymbol)); | ||
58 | reasoningBuilder.storageRefiner(countSymbol, MultiObjectStorageRefiner::new); | ||
59 | } | ||
60 | } | ||
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiobject/UpperCardinalityView.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiobject/UpperCardinalityView.java new file mode 100644 index 00000000..6be6ae1b --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiobject/UpperCardinalityView.java | |||
@@ -0,0 +1,23 @@ | |||
1 | /* | ||
2 | * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/> | ||
3 | * | ||
4 | * SPDX-License-Identifier: EPL-2.0 | ||
5 | */ | ||
6 | package tools.refinery.store.reasoning.translator.multiobject; | ||
7 | |||
8 | import tools.refinery.store.query.term.Parameter; | ||
9 | import tools.refinery.store.query.view.AbstractFunctionView; | ||
10 | import tools.refinery.store.representation.Symbol; | ||
11 | import tools.refinery.store.representation.cardinality.CardinalityInterval; | ||
12 | import tools.refinery.store.representation.cardinality.UpperCardinality; | ||
13 | |||
14 | class UpperCardinalityView extends AbstractFunctionView<CardinalityInterval> { | ||
15 | public UpperCardinalityView(Symbol<CardinalityInterval> symbol) { | ||
16 | super(symbol, "upper", new Parameter(UpperCardinality.class)); | ||
17 | } | ||
18 | |||
19 | @Override | ||
20 | protected Object forwardMapValue(CardinalityInterval value) { | ||
21 | return value.upperBound(); | ||
22 | } | ||
23 | } | ||
diff --git a/subprojects/store-reasoning/src/test/java/tools/refinery/store/reasoning/PartialModelTest.java b/subprojects/store-reasoning/src/test/java/tools/refinery/store/reasoning/PartialModelTest.java index f948ad6a..b2188f5d 100644 --- a/subprojects/store-reasoning/src/test/java/tools/refinery/store/reasoning/PartialModelTest.java +++ b/subprojects/store-reasoning/src/test/java/tools/refinery/store/reasoning/PartialModelTest.java | |||
@@ -14,78 +14,95 @@ import tools.refinery.store.query.viatra.ViatraModelQueryAdapter; | |||
14 | import tools.refinery.store.query.view.ForbiddenView; | 14 | import tools.refinery.store.query.view.ForbiddenView; |
15 | import tools.refinery.store.reasoning.literal.Concreteness; | 15 | import tools.refinery.store.reasoning.literal.Concreteness; |
16 | import tools.refinery.store.reasoning.representation.PartialRelation; | 16 | import tools.refinery.store.reasoning.representation.PartialRelation; |
17 | import tools.refinery.store.reasoning.seed.Seed; | 17 | import tools.refinery.store.reasoning.seed.ModelSeed; |
18 | import tools.refinery.store.reasoning.translator.PartialRelationTranslator; | 18 | import tools.refinery.store.reasoning.translator.PartialRelationTranslator; |
19 | import tools.refinery.store.reasoning.translator.multiobject.MultiObjectTranslator; | ||
19 | import tools.refinery.store.representation.Symbol; | 20 | import tools.refinery.store.representation.Symbol; |
20 | import tools.refinery.store.representation.TruthValue; | 21 | import tools.refinery.store.representation.TruthValue; |
21 | import tools.refinery.store.tuple.Tuple; | 22 | import tools.refinery.store.tuple.Tuple; |
22 | 23 | ||
23 | import static org.hamcrest.MatcherAssert.assertThat; | 24 | import static org.hamcrest.MatcherAssert.assertThat; |
24 | import static org.hamcrest.Matchers.is; | 25 | import static org.hamcrest.Matchers.is; |
26 | import static org.hamcrest.Matchers.not; | ||
27 | import static org.hamcrest.Matchers.nullValue; | ||
25 | import static tools.refinery.store.query.literal.Literals.not; | 28 | import static tools.refinery.store.query.literal.Literals.not; |
29 | import static tools.refinery.store.reasoning.ReasoningAdapter.EQUALS_SYMBOL; | ||
30 | import static tools.refinery.store.reasoning.ReasoningAdapter.EXISTS_SYMBOL; | ||
26 | import static tools.refinery.store.reasoning.literal.PartialLiterals.may; | 31 | import static tools.refinery.store.reasoning.literal.PartialLiterals.may; |
32 | import static tools.refinery.store.reasoning.literal.PartialLiterals.must; | ||
27 | 33 | ||
28 | class PartialModelTest { | 34 | class PartialModelTest { |
29 | @Test | 35 | @Test |
30 | void partialModelTest() { | 36 | void partialModelTest() { |
31 | var personStorage = Symbol.of("Person", 1, TruthValue.class, TruthValue.FALSE); | ||
32 | var friendStorage = Symbol.of("friend", 2, TruthValue.class, TruthValue.UNKNOWN); | ||
33 | |||
34 | var person = new PartialRelation("Person", 1); | 37 | var person = new PartialRelation("Person", 1); |
35 | var friend = new PartialRelation("friend", 2); | 38 | var friend = new PartialRelation("friend", 2); |
36 | var lonely = new PartialRelation("lonely", 1); | 39 | var lonely = new PartialRelation("lonely", 1); |
37 | 40 | ||
41 | var personStorage = Symbol.of("Person", 1, TruthValue.class, TruthValue.FALSE); | ||
42 | var friendStorage = Symbol.of("friend", 2, TruthValue.class, TruthValue.UNKNOWN); | ||
43 | |||
38 | var store = ModelStore.builder() | 44 | var store = ModelStore.builder() |
39 | .with(ViatraModelQueryAdapter.builder()) | 45 | .with(ViatraModelQueryAdapter.builder()) |
40 | .with(ReasoningAdapter.builder() | 46 | .with(ReasoningAdapter.builder()) |
41 | .initialNodeCount(4)) | 47 | .with(new MultiObjectTranslator()) |
42 | .with(PartialRelationTranslator.of(ReasoningAdapter.EXISTS_SYMBOL) | ||
43 | .symbol(Symbol.of("exists", 1, TruthValue.class, TruthValue.FALSE)) | ||
44 | .seed(Seed.builder(ReasoningAdapter.EXISTS_SYMBOL) | ||
45 | .put(Tuple.of(0), TruthValue.TRUE) | ||
46 | .put(Tuple.of(1), TruthValue.UNKNOWN) | ||
47 | .put(Tuple.of(2), TruthValue.TRUE) | ||
48 | .put(Tuple.of(3), TruthValue.TRUE) | ||
49 | .build())) | ||
50 | .with(PartialRelationTranslator.of(person) | 48 | .with(PartialRelationTranslator.of(person) |
51 | .symbol(personStorage) | 49 | .symbol(personStorage)) |
52 | .seed(Seed.builder(personStorage) | ||
53 | .put(Tuple.of(0), TruthValue.TRUE) | ||
54 | .put(Tuple.of(1), TruthValue.TRUE) | ||
55 | .put(Tuple.of(2), TruthValue.UNKNOWN) | ||
56 | .build())) | ||
57 | .with(PartialRelationTranslator.of(friend) | 50 | .with(PartialRelationTranslator.of(friend) |
58 | .symbol(friendStorage) | 51 | .symbol(friendStorage) |
59 | .may(Query.of((builder, p1, p2) -> builder.clause( | 52 | .may(Query.of("mayPerson", (builder, p1, p2) -> builder.clause( |
60 | may(person.call(p1)), | 53 | may(person.call(p1)), |
61 | may(person.call(p2)), | 54 | may(person.call(p2)), |
62 | // not(must(EQUALS_SYMBOL.call(p1, p2))), | 55 | not(must(EQUALS_SYMBOL.call(p1, p2))), |
63 | not(new ForbiddenView(friendStorage).call(p1, p2)) | 56 | not(new ForbiddenView(friendStorage).call(p1, p2)) |
64 | ))) | 57 | )))) |
65 | .seed(Seed.builder(friendStorage) | ||
66 | .put(Tuple.of(0, 1), TruthValue.TRUE) | ||
67 | .put(Tuple.of(1, 2), TruthValue.FALSE) | ||
68 | .build())) | ||
69 | .with(PartialRelationTranslator.of(lonely) | 58 | .with(PartialRelationTranslator.of(lonely) |
70 | .query(Query.of((builder, p1) -> builder.clause( | 59 | .query(Query.of("lonely", (builder, p1) -> builder.clause( |
71 | person.call(p1), | 60 | person.call(p1), |
72 | not(friend.call(p1, Variable.of()))) | 61 | not(friend.call(p1, Variable.of()))) |
73 | ))) | 62 | ))) |
74 | .build(); | 63 | .build(); |
75 | 64 | ||
76 | var model = store.getAdapter(ReasoningStoreAdapter.class).createInitialModel(); | 65 | var modelSeed = ModelSeed.builder(4) |
66 | .seed(EXISTS_SYMBOL, builder -> builder | ||
67 | .put(Tuple.of(0), TruthValue.TRUE) | ||
68 | .put(Tuple.of(1), TruthValue.UNKNOWN) | ||
69 | .put(Tuple.of(2), TruthValue.TRUE) | ||
70 | .put(Tuple.of(3), TruthValue.TRUE)) | ||
71 | .seed(EQUALS_SYMBOL, builder -> builder | ||
72 | .put(Tuple.of(0, 0), TruthValue.TRUE) | ||
73 | .put(Tuple.of(1, 1), TruthValue.UNKNOWN) | ||
74 | .put(Tuple.of(2, 2), TruthValue.UNKNOWN) | ||
75 | .put(Tuple.of(3, 3), TruthValue.TRUE)) | ||
76 | .seed(person, builder -> builder | ||
77 | .put(Tuple.of(0), TruthValue.TRUE) | ||
78 | .put(Tuple.of(1), TruthValue.TRUE) | ||
79 | .put(Tuple.of(2), TruthValue.UNKNOWN)) | ||
80 | .seed(friend, builder -> builder | ||
81 | .reducedValue(TruthValue.UNKNOWN) | ||
82 | .put(Tuple.of(0, 1), TruthValue.TRUE) | ||
83 | .put(Tuple.of(1, 2), TruthValue.FALSE)) | ||
84 | .build(); | ||
85 | var model = store.getAdapter(ReasoningStoreAdapter.class).createInitialModel(modelSeed); | ||
77 | 86 | ||
78 | var queryAdapter = model.getAdapter(ModelQueryAdapter.class); | 87 | var queryAdapter = model.getAdapter(ModelQueryAdapter.class); |
79 | var reasoningAdapter = model.getAdapter(ReasoningAdapter.class); | 88 | var reasoningAdapter = model.getAdapter(ReasoningAdapter.class); |
80 | var friendInterpretation = reasoningAdapter.getPartialInterpretation(Concreteness.PARTIAL, friend); | 89 | var friendInterpretation = reasoningAdapter.getPartialInterpretation(Concreteness.PARTIAL, friend); |
90 | var friendRefiner = reasoningAdapter.getRefiner(friend); | ||
91 | |||
81 | assertThat(friendInterpretation.get(Tuple.of(0, 1)), is(TruthValue.TRUE)); | 92 | assertThat(friendInterpretation.get(Tuple.of(0, 1)), is(TruthValue.TRUE)); |
82 | assertThat(friendInterpretation.get(Tuple.of(1, 0)), is(TruthValue.UNKNOWN)); | 93 | assertThat(friendInterpretation.get(Tuple.of(1, 0)), is(TruthValue.UNKNOWN)); |
83 | assertThat(friendInterpretation.get(Tuple.of(3, 0)), is(TruthValue.FALSE)); | 94 | assertThat(friendInterpretation.get(Tuple.of(3, 0)), is(TruthValue.FALSE)); |
84 | var friendRefiner = reasoningAdapter.getRefiner(friend); | 95 | |
85 | assertThat(friendRefiner.merge(Tuple.of(0, 1), TruthValue.FALSE), is(true)); | 96 | assertThat(friendRefiner.merge(Tuple.of(0, 1), TruthValue.FALSE), is(true)); |
86 | assertThat(friendRefiner.merge(Tuple.of(1, 0), TruthValue.TRUE), is(true)); | 97 | assertThat(friendRefiner.merge(Tuple.of(1, 0), TruthValue.TRUE), is(true)); |
98 | var splitResult = reasoningAdapter.split(1); | ||
99 | assertThat(splitResult, not(nullValue())); | ||
100 | var newPerson = splitResult.get(0); | ||
87 | queryAdapter.flushChanges(); | 101 | queryAdapter.flushChanges(); |
102 | |||
88 | assertThat(friendInterpretation.get(Tuple.of(0, 1)), is(TruthValue.ERROR)); | 103 | assertThat(friendInterpretation.get(Tuple.of(0, 1)), is(TruthValue.ERROR)); |
89 | assertThat(friendInterpretation.get(Tuple.of(1, 0)), is(TruthValue.TRUE)); | 104 | assertThat(friendInterpretation.get(Tuple.of(1, 0)), is(TruthValue.TRUE)); |
105 | assertThat(friendInterpretation.get(Tuple.of(0, newPerson)), is(TruthValue.ERROR)); | ||
106 | assertThat(friendInterpretation.get(Tuple.of(newPerson, 0)), is(TruthValue.TRUE)); | ||
90 | } | 107 | } |
91 | } | 108 | } |