From 78cca26065698c65fc5fe11e3b99a8ba41f0f295 Mon Sep 17 00:00:00 2001 From: Kristóf Marussy Date: Fri, 17 Nov 2023 17:21:59 +0100 Subject: 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. --- .../reasoning/scope/LowerTypeScopePropagator.java | 15 ++++++++++++-- .../reasoning/scope/UpperTypeScopePropagator.java | 23 ++++++++++++++++------ 2 files changed, 30 insertions(+), 8 deletions(-) (limited to 'subprojects/store-reasoning-scope/src') 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; import tools.refinery.store.query.dnf.Query; import tools.refinery.store.query.dnf.RelationalQuery; import tools.refinery.store.query.term.Variable; +import tools.refinery.store.query.term.uppercardinality.UpperCardinalityTerms; import tools.refinery.store.reasoning.ReasoningBuilder; import tools.refinery.store.reasoning.literal.CountCandidateLowerBoundLiteral; +import tools.refinery.store.reasoning.literal.CountUpperBoundLiteral; import tools.refinery.store.reasoning.representation.PartialRelation; +import tools.refinery.store.representation.cardinality.UpperCardinality; import java.util.Collection; import java.util.List; @@ -77,10 +80,18 @@ class LowerTypeScopePropagator extends TypeScopePropagator { output.assign(sub(constant(lowerBound), candidateLowerBound)), check(greater(output, constant(0))) ))); + var tooFewObjects = Query.of(type.name() + "#tooFew", builder -> builder + .clause(UpperCardinality.class, upperBound -> List.of( + new CountUpperBoundLiteral(upperBound, type, List.of(Variable.of())), + check(UpperCardinalityTerms.less(upperBound, + UpperCardinalityTerms.constant(UpperCardinality.of(lowerBound)))) + ))); storeBuilder.getAdapter(ReasoningBuilder.class).objective(Objectives.value(requiredObjects)); - storeBuilder.tryGetAdapter(DesignSpaceExplorationBuilder.class).ifPresent(dseBuilder -> - dseBuilder.accept(Criteria.whenNoMatch(requiredObjects))); + storeBuilder.tryGetAdapter(DesignSpaceExplorationBuilder.class).ifPresent(dseBuilder -> { + dseBuilder.accept(Criteria.whenNoMatch(requiredObjects)); + dseBuilder.exclude(Criteria.whenHasMatch(tooFewObjects)); + }); } } } 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; import tools.refinery.store.dse.transition.DesignSpaceExplorationBuilder; import tools.refinery.store.dse.transition.objectives.Criteria; +import tools.refinery.store.dse.transition.objectives.Objectives; import tools.refinery.store.model.ModelStoreBuilder; import tools.refinery.store.query.dnf.AnyQuery; import tools.refinery.store.query.dnf.Query; import tools.refinery.store.query.dnf.RelationalQuery; import tools.refinery.store.query.term.Variable; +import tools.refinery.store.reasoning.ReasoningBuilder; import tools.refinery.store.reasoning.literal.CountCandidateUpperBoundLiteral; +import tools.refinery.store.reasoning.literal.CountLowerBoundLiteral; import tools.refinery.store.reasoning.representation.PartialRelation; import java.util.Collection; import java.util.List; import static tools.refinery.store.query.literal.Literals.check; -import static tools.refinery.store.query.term.int_.IntTerms.constant; -import static tools.refinery.store.query.term.int_.IntTerms.greater; +import static tools.refinery.store.query.term.int_.IntTerms.*; import static tools.refinery.store.reasoning.literal.PartialLiterals.must; import static tools.refinery.store.reasoning.translator.multiobject.MultiObjectTranslator.MULTI_VIEW; @@ -70,14 +72,23 @@ class UpperTypeScopePropagator extends TypeScopePropagator { public void configure(ModelStoreBuilder storeBuilder) { super.configure(storeBuilder); - var tooManyObjects = Query.of(type.name() + "#tooMany", builder -> builder + var excessObjects = Query.of(type.name() + "#excess", Integer.class, (builder, output) -> builder .clause(Integer.class, candidateUpperBound -> List.of( new CountCandidateUpperBoundLiteral(candidateUpperBound, type, List.of(Variable.of())), - check(greater(candidateUpperBound, constant(upperBound))) + output.assign(sub(candidateUpperBound, constant(upperBound))), + check(greater(output, constant(0))) + ))); + var tooManyObjects = Query.of(type.name() + "#tooMany", builder -> builder + .clause(Integer.class, lowerBound -> List.of( + new CountLowerBoundLiteral(lowerBound, type, List.of(Variable.of())), + check(greater(lowerBound, constant(upperBound))) ))); - storeBuilder.tryGetAdapter(DesignSpaceExplorationBuilder.class).ifPresent(dseBuilder -> - dseBuilder.accept(Criteria.whenNoMatch(tooManyObjects))); + storeBuilder.getAdapter(ReasoningBuilder.class).objective(Objectives.value(excessObjects)); + storeBuilder.tryGetAdapter(DesignSpaceExplorationBuilder.class).ifPresent(dseBuilder -> { + dseBuilder.accept(Criteria.whenNoMatch(excessObjects)); + dseBuilder.exclude(Criteria.whenHasMatch(tooManyObjects)); + }); } } } -- cgit v1.2.3-70-g09d2