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.

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;
 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));
+            });
                 }
         }
 }