diff options
author | 2023-11-17 17:21:59 +0100 | |
---|---|---|
committer | 2023-11-19 14:41:16 +0100 | |
commit | 78cca26065698c65fc5fe11e3b99a8ba41f0f295 (patch) | |
tree | 370c156b526ba36c9158f79fc80b7cbdb7d00ada /subprojects/store-reasoning-scope/src/main | |
parent | chore(deps): bump dependencies (diff) | |
download | refinery-78cca26065698c65fc5fe11e3b99a8ba41f0f295.tar.gz refinery-78cca26065698c65fc5fe11e3b99a8ba41f0f295.tar.zst refinery-78cca26065698c65fc5fe11e3b99a8ba41f0f295.zip |
fix: upper and lower scopes
Make sure the scope bound guides the best-first search and is always obeyed even
if it can't be fully represented using the scoped partial model abstraction.
For representable bounds (classes and unary predicate that are always fully
knwon to be false or true in the initial model) this leads to duplicated
computations.
Diffstat (limited to 'subprojects/store-reasoning-scope/src/main')
2 files changed, 30 insertions, 8 deletions
diff --git a/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/LowerTypeScopePropagator.java b/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/LowerTypeScopePropagator.java index 86401b7e..702e570f 100644 --- a/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/LowerTypeScopePropagator.java +++ b/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/LowerTypeScopePropagator.java | |||
@@ -13,9 +13,12 @@ import tools.refinery.store.query.dnf.AnyQuery; | |||
13 | import tools.refinery.store.query.dnf.Query; | 13 | import tools.refinery.store.query.dnf.Query; |
14 | import tools.refinery.store.query.dnf.RelationalQuery; | 14 | import tools.refinery.store.query.dnf.RelationalQuery; |
15 | import tools.refinery.store.query.term.Variable; | 15 | import tools.refinery.store.query.term.Variable; |
16 | import tools.refinery.store.query.term.uppercardinality.UpperCardinalityTerms; | ||
16 | import tools.refinery.store.reasoning.ReasoningBuilder; | 17 | import tools.refinery.store.reasoning.ReasoningBuilder; |
17 | import tools.refinery.store.reasoning.literal.CountCandidateLowerBoundLiteral; | 18 | import tools.refinery.store.reasoning.literal.CountCandidateLowerBoundLiteral; |
19 | import tools.refinery.store.reasoning.literal.CountUpperBoundLiteral; | ||
18 | import tools.refinery.store.reasoning.representation.PartialRelation; | 20 | import tools.refinery.store.reasoning.representation.PartialRelation; |
21 | import tools.refinery.store.representation.cardinality.UpperCardinality; | ||
19 | 22 | ||
20 | import java.util.Collection; | 23 | import java.util.Collection; |
21 | import java.util.List; | 24 | import java.util.List; |
@@ -77,10 +80,18 @@ class LowerTypeScopePropagator extends TypeScopePropagator { | |||
77 | output.assign(sub(constant(lowerBound), candidateLowerBound)), | 80 | output.assign(sub(constant(lowerBound), candidateLowerBound)), |
78 | check(greater(output, constant(0))) | 81 | check(greater(output, constant(0))) |
79 | ))); | 82 | ))); |
83 | var tooFewObjects = Query.of(type.name() + "#tooFew", builder -> builder | ||
84 | .clause(UpperCardinality.class, upperBound -> List.of( | ||
85 | new CountUpperBoundLiteral(upperBound, type, List.of(Variable.of())), | ||
86 | check(UpperCardinalityTerms.less(upperBound, | ||
87 | UpperCardinalityTerms.constant(UpperCardinality.of(lowerBound)))) | ||
88 | ))); | ||
80 | 89 | ||
81 | storeBuilder.getAdapter(ReasoningBuilder.class).objective(Objectives.value(requiredObjects)); | 90 | storeBuilder.getAdapter(ReasoningBuilder.class).objective(Objectives.value(requiredObjects)); |
82 | storeBuilder.tryGetAdapter(DesignSpaceExplorationBuilder.class).ifPresent(dseBuilder -> | 91 | storeBuilder.tryGetAdapter(DesignSpaceExplorationBuilder.class).ifPresent(dseBuilder -> { |
83 | dseBuilder.accept(Criteria.whenNoMatch(requiredObjects))); | 92 | dseBuilder.accept(Criteria.whenNoMatch(requiredObjects)); |
93 | dseBuilder.exclude(Criteria.whenHasMatch(tooFewObjects)); | ||
94 | }); | ||
84 | } | 95 | } |
85 | } | 96 | } |
86 | } | 97 | } |
diff --git a/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/UpperTypeScopePropagator.java b/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/UpperTypeScopePropagator.java index 634e93bc..b2f8d39b 100644 --- a/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/UpperTypeScopePropagator.java +++ b/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/UpperTypeScopePropagator.java | |||
@@ -7,20 +7,22 @@ package tools.refinery.store.reasoning.scope; | |||
7 | 7 | ||
8 | import tools.refinery.store.dse.transition.DesignSpaceExplorationBuilder; | 8 | import tools.refinery.store.dse.transition.DesignSpaceExplorationBuilder; |
9 | import tools.refinery.store.dse.transition.objectives.Criteria; | 9 | import tools.refinery.store.dse.transition.objectives.Criteria; |
10 | import tools.refinery.store.dse.transition.objectives.Objectives; | ||
10 | import tools.refinery.store.model.ModelStoreBuilder; | 11 | import tools.refinery.store.model.ModelStoreBuilder; |
11 | import tools.refinery.store.query.dnf.AnyQuery; | 12 | import tools.refinery.store.query.dnf.AnyQuery; |
12 | import tools.refinery.store.query.dnf.Query; | 13 | import tools.refinery.store.query.dnf.Query; |
13 | import tools.refinery.store.query.dnf.RelationalQuery; | 14 | import tools.refinery.store.query.dnf.RelationalQuery; |
14 | import tools.refinery.store.query.term.Variable; | 15 | import tools.refinery.store.query.term.Variable; |
16 | import tools.refinery.store.reasoning.ReasoningBuilder; | ||
15 | import tools.refinery.store.reasoning.literal.CountCandidateUpperBoundLiteral; | 17 | import tools.refinery.store.reasoning.literal.CountCandidateUpperBoundLiteral; |
18 | import tools.refinery.store.reasoning.literal.CountLowerBoundLiteral; | ||
16 | import tools.refinery.store.reasoning.representation.PartialRelation; | 19 | import tools.refinery.store.reasoning.representation.PartialRelation; |
17 | 20 | ||
18 | import java.util.Collection; | 21 | import java.util.Collection; |
19 | import java.util.List; | 22 | import java.util.List; |
20 | 23 | ||
21 | import static tools.refinery.store.query.literal.Literals.check; | 24 | import static tools.refinery.store.query.literal.Literals.check; |
22 | import static tools.refinery.store.query.term.int_.IntTerms.constant; | 25 | import static tools.refinery.store.query.term.int_.IntTerms.*; |
23 | import static tools.refinery.store.query.term.int_.IntTerms.greater; | ||
24 | import static tools.refinery.store.reasoning.literal.PartialLiterals.must; | 26 | import static tools.refinery.store.reasoning.literal.PartialLiterals.must; |
25 | import static tools.refinery.store.reasoning.translator.multiobject.MultiObjectTranslator.MULTI_VIEW; | 27 | import static tools.refinery.store.reasoning.translator.multiobject.MultiObjectTranslator.MULTI_VIEW; |
26 | 28 | ||
@@ -70,14 +72,23 @@ class UpperTypeScopePropagator extends TypeScopePropagator { | |||
70 | public void configure(ModelStoreBuilder storeBuilder) { | 72 | public void configure(ModelStoreBuilder storeBuilder) { |
71 | super.configure(storeBuilder); | 73 | super.configure(storeBuilder); |
72 | 74 | ||
73 | var tooManyObjects = Query.of(type.name() + "#tooMany", builder -> builder | 75 | var excessObjects = Query.of(type.name() + "#excess", Integer.class, (builder, output) -> builder |
74 | .clause(Integer.class, candidateUpperBound -> List.of( | 76 | .clause(Integer.class, candidateUpperBound -> List.of( |
75 | new CountCandidateUpperBoundLiteral(candidateUpperBound, type, List.of(Variable.of())), | 77 | new CountCandidateUpperBoundLiteral(candidateUpperBound, type, List.of(Variable.of())), |
76 | check(greater(candidateUpperBound, constant(upperBound))) | 78 | output.assign(sub(candidateUpperBound, constant(upperBound))), |
79 | check(greater(output, constant(0))) | ||
80 | ))); | ||
81 | var tooManyObjects = Query.of(type.name() + "#tooMany", builder -> builder | ||
82 | .clause(Integer.class, lowerBound -> List.of( | ||
83 | new CountLowerBoundLiteral(lowerBound, type, List.of(Variable.of())), | ||
84 | check(greater(lowerBound, constant(upperBound))) | ||
77 | ))); | 85 | ))); |
78 | 86 | ||
79 | storeBuilder.tryGetAdapter(DesignSpaceExplorationBuilder.class).ifPresent(dseBuilder -> | 87 | storeBuilder.getAdapter(ReasoningBuilder.class).objective(Objectives.value(excessObjects)); |
80 | dseBuilder.accept(Criteria.whenNoMatch(tooManyObjects))); | 88 | storeBuilder.tryGetAdapter(DesignSpaceExplorationBuilder.class).ifPresent(dseBuilder -> { |
89 | dseBuilder.accept(Criteria.whenNoMatch(excessObjects)); | ||
90 | dseBuilder.exclude(Criteria.whenHasMatch(tooManyObjects)); | ||
91 | }); | ||
81 | } | 92 | } |
82 | } | 93 | } |
83 | } | 94 | } |