From 0bdb400deef88cb2a7c0b8c90afebf84b29c04d5 Mon Sep 17 00:00:00 2001 From: Kristóf Marussy Date: Sat, 9 Sep 2023 12:57:49 +0200 Subject: feat: integrate DSE with partial interpretation --- .../reasoning/scope/BoundScopePropagator.java | 229 +++++++++++++++++++ .../reasoning/scope/LowerTypeScopePropagator.java | 86 +++++++ .../store/reasoning/scope/RoundingUtil.java | 26 +++ .../store/reasoning/scope/ScopePropagator.java | 102 +++++++++ .../reasoning/scope/ScopePropagatorAdapter.java | 21 -- .../reasoning/scope/ScopePropagatorBuilder.java | 21 -- .../scope/ScopePropagatorStoreAdapter.java | 16 -- .../store/reasoning/scope/TypeScopePropagator.java | 66 ++++++ .../reasoning/scope/UpperTypeScopePropagator.java | 59 +++++ .../scope/internal/LowerTypeScopePropagator.java | 86 ------- .../reasoning/scope/internal/RoundingUtil.java | 26 --- .../scope/internal/ScopePropagatorAdapterImpl.java | 253 --------------------- .../scope/internal/ScopePropagatorBuilderImpl.java | 86 ------- .../internal/ScopePropagatorStoreAdapterImpl.java | 58 ----- .../scope/internal/TypeScopePropagator.java | 67 ------ .../scope/internal/UpperTypeScopePropagator.java | 59 ----- .../store/reasoning/scope/MultiObjectTest.java | 38 ++-- .../store/reasoning/scope/RoundingUtilTest.java | 69 ++++++ .../reasoning/scope/internal/RoundingUtilTest.java | 69 ------ 19 files changed, 657 insertions(+), 780 deletions(-) create mode 100644 subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/BoundScopePropagator.java create mode 100644 subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/LowerTypeScopePropagator.java create mode 100644 subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/RoundingUtil.java create mode 100644 subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/ScopePropagator.java delete mode 100644 subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/ScopePropagatorAdapter.java delete mode 100644 subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/ScopePropagatorBuilder.java delete mode 100644 subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/ScopePropagatorStoreAdapter.java create mode 100644 subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/TypeScopePropagator.java create mode 100644 subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/UpperTypeScopePropagator.java delete mode 100644 subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/internal/LowerTypeScopePropagator.java delete mode 100644 subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/internal/RoundingUtil.java delete mode 100644 subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/internal/ScopePropagatorAdapterImpl.java delete mode 100644 subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/internal/ScopePropagatorBuilderImpl.java delete mode 100644 subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/internal/ScopePropagatorStoreAdapterImpl.java delete mode 100644 subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/internal/TypeScopePropagator.java delete mode 100644 subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/internal/UpperTypeScopePropagator.java create mode 100644 subprojects/store-reasoning-scope/src/test/java/tools/refinery/store/reasoning/scope/RoundingUtilTest.java delete mode 100644 subprojects/store-reasoning-scope/src/test/java/tools/refinery/store/reasoning/scope/internal/RoundingUtilTest.java (limited to 'subprojects/store-reasoning-scope/src') diff --git a/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/BoundScopePropagator.java b/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/BoundScopePropagator.java new file mode 100644 index 00000000..62aadb4a --- /dev/null +++ b/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/BoundScopePropagator.java @@ -0,0 +1,229 @@ +/* + * SPDX-FileCopyrightText: 2023 The Refinery Authors + * + * SPDX-License-Identifier: EPL-2.0 + */ +package tools.refinery.store.reasoning.scope; + +import com.google.ortools.linearsolver.MPConstraint; +import com.google.ortools.linearsolver.MPObjective; +import com.google.ortools.linearsolver.MPSolver; +import com.google.ortools.linearsolver.MPVariable; +import org.eclipse.collections.api.factory.primitive.IntObjectMaps; +import org.eclipse.collections.api.factory.primitive.IntSets; +import org.eclipse.collections.api.map.primitive.MutableIntObjectMap; +import org.eclipse.collections.api.set.primitive.MutableIntSet; +import tools.refinery.store.dse.propagation.BoundPropagator; +import tools.refinery.store.dse.propagation.PropagationResult; +import tools.refinery.store.model.Interpretation; +import tools.refinery.store.model.Model; +import tools.refinery.store.query.ModelQueryAdapter; +import tools.refinery.store.representation.cardinality.*; +import tools.refinery.store.tuple.Tuple; + +class BoundScopePropagator implements BoundPropagator { + private final ModelQueryAdapter queryEngine; + private final Interpretation countInterpretation; + private final MPSolver solver; + private final MPObjective objective; + private final MutableIntObjectMap variables = IntObjectMaps.mutable.empty(); + private final MutableIntSet activeVariables = IntSets.mutable.empty(); + private final TypeScopePropagator[] propagators; + private boolean changed = true; + + public BoundScopePropagator(Model model, ScopePropagator storeAdapter) { + queryEngine = model.getAdapter(ModelQueryAdapter.class); + countInterpretation = model.getInterpretation(storeAdapter.getCountSymbol()); + solver = MPSolver.createSolver("GLOP"); + objective = solver.objective(); + initializeVariables(); + countInterpretation.addListener(this::countChanged, true); + var propagatorFactories = storeAdapter.getTypeScopePropagatorFactories(); + propagators = new TypeScopePropagator[propagatorFactories.size()]; + for (int i = 0; i < propagators.length; i++) { + propagators[i] = propagatorFactories.get(i).createPropagator(this); + } + } + + ModelQueryAdapter getQueryEngine() { + return queryEngine; + } + + private void initializeVariables() { + var cursor = countInterpretation.getAll(); + while (cursor.move()) { + var interval = cursor.getValue(); + if (!interval.equals(CardinalityIntervals.ONE)) { + int nodeId = cursor.getKey().get(0); + createVariable(nodeId, interval); + activeVariables.add(nodeId); + } + } + } + + private MPVariable createVariable(int nodeId, CardinalityInterval interval) { + double lowerBound = interval.lowerBound(); + double upperBound = getUpperBound(interval); + var variable = solver.makeNumVar(lowerBound, upperBound, "x" + nodeId); + variables.put(nodeId, variable); + return variable; + } + + private void countChanged(Tuple key, CardinalityInterval fromValue, CardinalityInterval toValue, + boolean ignoredRestoring) { + int nodeId = key.get(0); + if ((toValue == null || toValue.equals(CardinalityIntervals.ONE))) { + if (fromValue != null && !fromValue.equals(CardinalityIntervals.ONE)) { + removeActiveVariable(toValue, nodeId); + } + return; + } + if (fromValue == null || fromValue.equals(CardinalityIntervals.ONE)) { + activeVariables.add(nodeId); + } + var variable = variables.get(nodeId); + if (variable == null) { + createVariable(nodeId, toValue); + markAsChanged(); + return; + } + double lowerBound = toValue.lowerBound(); + double upperBound = getUpperBound(toValue); + if (variable.lb() != lowerBound) { + variable.setLb(lowerBound); + markAsChanged(); + } + if (variable.ub() != upperBound) { + variable.setUb(upperBound); + markAsChanged(); + } + } + + private void removeActiveVariable(CardinalityInterval toValue, int nodeId) { + var variable = variables.get(nodeId); + if (variable == null || !activeVariables.remove(nodeId)) { + throw new AssertionError("Variable not active: " + nodeId); + } + if (toValue == null) { + variable.setBounds(0, 0); + } else { + // Until queries are flushed and the constraints can be properly updated, + // the variable corresponding to the (previous) multi-object has to stand in for a single object. + variable.setBounds(1, 1); + } + markAsChanged(); + } + + MPConstraint makeConstraint() { + return solver.makeConstraint(); + } + + MPVariable getVariable(int nodeId) { + var variable = variables.get(nodeId); + if (variable != null) { + return variable; + } + var interval = countInterpretation.get(Tuple.of(nodeId)); + if (interval == null || interval.equals(CardinalityIntervals.ONE)) { + interval = CardinalityIntervals.NONE; + } else { + activeVariables.add(nodeId); + markAsChanged(); + } + return createVariable(nodeId, interval); + } + + void markAsChanged() { + changed = true; + } + + @Override + public PropagationResult propagateOne() { + queryEngine.flushChanges(); + if (!changed) { + return PropagationResult.UNCHANGED; + } + changed = false; + for (var propagator : propagators) { + propagator.updateBounds(); + } + var result = PropagationResult.UNCHANGED; + if (activeVariables.isEmpty()) { + return checkEmptiness(); + } + var iterator = activeVariables.intIterator(); + while (iterator.hasNext()) { + int nodeId = iterator.next(); + var variable = variables.get(nodeId); + if (variable == null) { + throw new AssertionError("Missing active variable: " + nodeId); + } + result = result.andThen(propagateNode(nodeId, variable)); + if (result.isRejected()) { + return result; + } + } + return result; + } + + private PropagationResult checkEmptiness() { + var emptinessCheckingResult = solver.solve(); + return switch (emptinessCheckingResult) { + case OPTIMAL, UNBOUNDED -> PropagationResult.UNCHANGED; + case INFEASIBLE -> PropagationResult.REJECTED; + default -> throw new IllegalStateException("Failed to check for consistency: " + emptinessCheckingResult); + }; + } + + private PropagationResult propagateNode(int nodeId, MPVariable variable) { + objective.setCoefficient(variable, 1); + try { + objective.setMinimization(); + var minimizationResult = solver.solve(); + int lowerBound; + switch (minimizationResult) { + case OPTIMAL -> lowerBound = RoundingUtil.roundUp(objective.value()); + case UNBOUNDED -> lowerBound = 0; + case INFEASIBLE -> { + return PropagationResult.REJECTED; + } + default -> throw new IllegalStateException("Failed to solve for minimum of %s: %s" + .formatted(variable, minimizationResult)); + } + + objective.setMaximization(); + var maximizationResult = solver.solve(); + UpperCardinality upperBound; + switch (maximizationResult) { + case OPTIMAL -> upperBound = UpperCardinalities.atMost(RoundingUtil.roundDown(objective.value())); + // Problem was feasible when minimizing, the only possible source of {@code UNBOUNDED_OR_INFEASIBLE} is + // an unbounded maximization problem. See https://github.com/google/or-tools/issues/3319 + case UNBOUNDED, INFEASIBLE -> upperBound = UpperCardinalities.UNBOUNDED; + default -> throw new IllegalStateException("Failed to solve for maximum of %s: %s" + .formatted(variable, minimizationResult)); + } + + var newInterval = CardinalityIntervals.between(lowerBound, upperBound); + var oldInterval = countInterpretation.put(Tuple.of(nodeId), newInterval); + if (newInterval.lowerBound() < oldInterval.lowerBound() || + newInterval.upperBound().compareTo(oldInterval.upperBound()) > 0) { + throw new IllegalArgumentException("Failed to refine multiplicity %s of node %d to %s" + .formatted(oldInterval, nodeId, newInterval)); + } + return newInterval.equals(oldInterval) ? PropagationResult.UNCHANGED : PropagationResult.PROPAGATED; + } finally { + objective.setCoefficient(variable, 0); + } + } + + private static double getUpperBound(CardinalityInterval interval) { + var upperBound = interval.upperBound(); + if (upperBound instanceof FiniteUpperCardinality finiteUpperCardinality) { + return finiteUpperCardinality.finiteUpperBound(); + } else if (upperBound instanceof UnboundedUpperCardinality) { + return Double.POSITIVE_INFINITY; + } else { + throw new IllegalArgumentException("Unknown upper bound: " + upperBound); + } + } +} 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 new file mode 100644 index 00000000..5d903f41 --- /dev/null +++ b/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/LowerTypeScopePropagator.java @@ -0,0 +1,86 @@ +/* + * SPDX-FileCopyrightText: 2023 The Refinery Authors + * + * SPDX-License-Identifier: EPL-2.0 + */ +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.CountCandidateLowerBoundLiteral; +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.*; +import static tools.refinery.store.reasoning.literal.PartialLiterals.may; +import static tools.refinery.store.reasoning.translator.multiobject.MultiObjectTranslator.MULTI_VIEW; + +class LowerTypeScopePropagator extends TypeScopePropagator { + private final int lowerBound; + + private LowerTypeScopePropagator(BoundScopePropagator adapter, int lowerBound, RelationalQuery allQuery, + RelationalQuery multiQuery) { + super(adapter, allQuery, multiQuery); + this.lowerBound = lowerBound; + } + + @Override + public void updateBounds() { + constraint.setLb((lowerBound - getSingleCount())); + } + + public static class Factory extends TypeScopePropagator.Factory { + private final PartialRelation type; + private final int lowerBound; + private final RelationalQuery allMay; + private final RelationalQuery multiMay; + + public Factory(PartialRelation type, int lowerBound) { + this.type = type; + this.lowerBound = lowerBound; + allMay = Query.of(type.name() + "#may", (builder, instance) -> builder.clause( + may(type.call(instance)) + )); + multiMay = Query.of(type.name() + "#multiMay", (builder, instance) -> builder.clause( + may(type.call(instance)), + MULTI_VIEW.call(instance) + )); + } + + @Override + public TypeScopePropagator createPropagator(BoundScopePropagator adapter) { + return new LowerTypeScopePropagator(adapter, lowerBound, allMay, multiMay); + } + + @Override + protected Collection getQueries() { + return List.of(allMay, multiMay); + } + + @Override + public void configure(ModelStoreBuilder storeBuilder) { + super.configure(storeBuilder); + + var requiredObjects = Query.of(type.name() + "#required", Integer.class, (builder, output) -> builder + .clause(Integer.class, candidateLowerBound -> List.of( + new CountCandidateLowerBoundLiteral(candidateLowerBound, type, List.of(Variable.of())), + output.assign(sub(constant(lowerBound), candidateLowerBound)), + check(greater(output, constant(0))) + ))); + + storeBuilder.getAdapter(ReasoningBuilder.class).objective(Objectives.value(requiredObjects)); + storeBuilder.tryGetAdapter(DesignSpaceExplorationBuilder.class).ifPresent(dseBuilder -> + dseBuilder.accept(Criteria.whenNoMatch(requiredObjects))); + } + } +} diff --git a/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/RoundingUtil.java b/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/RoundingUtil.java new file mode 100644 index 00000000..986771a1 --- /dev/null +++ b/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/RoundingUtil.java @@ -0,0 +1,26 @@ +/* + * SPDX-FileCopyrightText: 2023 The Refinery Authors + * + * SPDX-License-Identifier: EPL-2.0 + */ +package tools.refinery.store.reasoning.scope; + +final class RoundingUtil { + private static final double TOLERANCE = 0.01; + + private RoundingUtil() { + throw new IllegalStateException("This is a static utility class and should not be instantiated directly"); + } + + public static int roundUp(double value) { + double ceil = Math.ceil(value - TOLERANCE); + int intCeil = (int) ceil; + return Math.max(intCeil, 0); + } + + public static int roundDown(double value) { + double floor = Math.floor(value + TOLERANCE); + int intFloor = (int) floor; + return Math.max(intFloor, 0); + } +} diff --git a/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/ScopePropagator.java b/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/ScopePropagator.java new file mode 100644 index 00000000..25b1966c --- /dev/null +++ b/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/ScopePropagator.java @@ -0,0 +1,102 @@ +/* + * SPDX-FileCopyrightText: 2023 The Refinery Authors + * + * SPDX-License-Identifier: EPL-2.0 + */ +package tools.refinery.store.reasoning.scope; + +import com.google.ortools.Loader; +import tools.refinery.store.dse.propagation.PropagationBuilder; +import tools.refinery.store.model.ModelStoreBuilder; +import tools.refinery.store.model.ModelStoreConfiguration; +import tools.refinery.store.reasoning.representation.PartialRelation; +import tools.refinery.store.reasoning.translator.TranslationException; +import tools.refinery.store.reasoning.translator.multiobject.MultiObjectTranslator; +import tools.refinery.store.representation.Symbol; +import tools.refinery.store.representation.cardinality.CardinalityInterval; +import tools.refinery.store.representation.cardinality.FiniteUpperCardinality; + +import java.util.*; + +public class ScopePropagator implements ModelStoreConfiguration { + private final Symbol countSymbol; + private final Map scopes = new LinkedHashMap<>(); + private final List typeScopePropagatorFactories = new ArrayList<>(); + + public ScopePropagator() { + this(MultiObjectTranslator.COUNT_STORAGE); + } + + public ScopePropagator(Symbol countSymbol) { + if (countSymbol.arity() != 1) { + throw new IllegalArgumentException("Count symbol must have arty 1, got %s with arity %d instead" + .formatted(countSymbol, countSymbol.arity())); + } + if (!countSymbol.valueType().equals(CardinalityInterval.class)) { + throw new IllegalArgumentException("Count symbol must have CardinalityInterval values"); + } + if (countSymbol.defaultValue() != null) { + throw new IllegalArgumentException("Count symbol must default value null"); + } + this.countSymbol = countSymbol; + } + + public ScopePropagator scope(PartialRelation type, CardinalityInterval interval) { + if (type.arity() != 1) { + throw new TranslationException(type, "Only types with arity 1 may have scopes, got %s with arity %d" + .formatted(type, type.arity())); + } + var newValue = scopes.compute(type, (ignoredKey, oldValue) -> + oldValue == null ? interval : oldValue.meet(interval)); + if (newValue.isEmpty()) { + throw new TranslationException(type, "Unsatisfiable scope for type %s".formatted(type)); + } + return this; + } + + public ScopePropagator scopes(Map scopes) { + return scopes(scopes.entrySet()); + } + + public ScopePropagator scopes(Collection> scopes) { + for (var entry : scopes) { + scope(entry.getKey(), entry.getValue()); + } + return this; + } + + @Override + public void apply(ModelStoreBuilder storeBuilder) { + createTypeScopePropagatorFactories(); + Loader.loadNativeLibraries(); + for (var factory : typeScopePropagatorFactories) { + factory.configure(storeBuilder); + } + storeBuilder.getAdapter(PropagationBuilder.class) + .propagator(model -> new BoundScopePropagator(model, this)); + } + + private void createTypeScopePropagatorFactories() { + for (var entry : scopes.entrySet()) { + var type = entry.getKey(); + var bounds = entry.getValue(); + if (bounds.lowerBound() > 0) { + var lowerFactory = new LowerTypeScopePropagator.Factory(type, bounds.lowerBound()); + typeScopePropagatorFactories.add(lowerFactory); + } + if (bounds.upperBound() instanceof FiniteUpperCardinality finiteUpperCardinality) { + var upperFactory = new UpperTypeScopePropagator.Factory(type, + finiteUpperCardinality.finiteUpperBound()); + typeScopePropagatorFactories.add(upperFactory); + } + } + } + + Symbol getCountSymbol() { + return countSymbol; + } + + List getTypeScopePropagatorFactories() { + return typeScopePropagatorFactories; + } +} diff --git a/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/ScopePropagatorAdapter.java b/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/ScopePropagatorAdapter.java deleted file mode 100644 index c2d3f59e..00000000 --- a/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/ScopePropagatorAdapter.java +++ /dev/null @@ -1,21 +0,0 @@ -/* - * SPDX-FileCopyrightText: 2023 The Refinery Authors - * - * SPDX-License-Identifier: EPL-2.0 - */ -package tools.refinery.store.reasoning.scope; - -import tools.refinery.store.adapter.ModelAdapter; -import tools.refinery.store.reasoning.refinement.RefinementResult; -import tools.refinery.store.reasoning.scope.internal.ScopePropagatorBuilderImpl; - -public interface ScopePropagatorAdapter extends ModelAdapter { - @Override - ScopePropagatorStoreAdapter getStoreAdapter(); - - RefinementResult propagate(); - - static ScopePropagatorBuilder builder() { - return new ScopePropagatorBuilderImpl(); - } -} diff --git a/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/ScopePropagatorBuilder.java b/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/ScopePropagatorBuilder.java deleted file mode 100644 index a17e04a4..00000000 --- a/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/ScopePropagatorBuilder.java +++ /dev/null @@ -1,21 +0,0 @@ -/* - * SPDX-FileCopyrightText: 2023 The Refinery Authors - * - * SPDX-License-Identifier: EPL-2.0 - */ -package tools.refinery.store.reasoning.scope; - -import tools.refinery.store.adapter.ModelAdapterBuilder; -import tools.refinery.store.model.ModelStore; -import tools.refinery.store.reasoning.representation.PartialRelation; -import tools.refinery.store.representation.Symbol; -import tools.refinery.store.representation.cardinality.CardinalityInterval; - -public interface ScopePropagatorBuilder extends ModelAdapterBuilder { - ScopePropagatorBuilder countSymbol(Symbol countSymbol); - - ScopePropagatorBuilder scope(PartialRelation type, CardinalityInterval interval); - - @Override - ScopePropagatorStoreAdapter build(ModelStore store); -} diff --git a/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/ScopePropagatorStoreAdapter.java b/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/ScopePropagatorStoreAdapter.java deleted file mode 100644 index 65d9c38d..00000000 --- a/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/ScopePropagatorStoreAdapter.java +++ /dev/null @@ -1,16 +0,0 @@ -/* - * SPDX-FileCopyrightText: 2023 The Refinery Authors - * - * SPDX-License-Identifier: EPL-2.0 - */ -package tools.refinery.store.reasoning.scope; - -import tools.refinery.store.adapter.ModelStoreAdapter; -import tools.refinery.store.reasoning.representation.PartialRelation; -import tools.refinery.store.representation.cardinality.CardinalityInterval; - -import java.util.Map; - -public interface ScopePropagatorStoreAdapter extends ModelStoreAdapter { - Map getScopes(); -} diff --git a/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/TypeScopePropagator.java b/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/TypeScopePropagator.java new file mode 100644 index 00000000..db80be7f --- /dev/null +++ b/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/TypeScopePropagator.java @@ -0,0 +1,66 @@ +/* + * SPDX-FileCopyrightText: 2023 The Refinery Authors + * + * SPDX-License-Identifier: EPL-2.0 + */ +package tools.refinery.store.reasoning.scope; + +import com.google.ortools.linearsolver.MPConstraint; +import tools.refinery.store.model.ModelStoreBuilder; +import tools.refinery.store.query.ModelQueryBuilder; +import tools.refinery.store.query.dnf.AnyQuery; +import tools.refinery.store.query.dnf.RelationalQuery; +import tools.refinery.store.query.resultset.ResultSet; +import tools.refinery.store.tuple.Tuple; + +import java.util.Collection; + +abstract class TypeScopePropagator { + private final BoundScopePropagator adapter; + private final ResultSet allNodes; + private final ResultSet multiNodes; + protected final MPConstraint constraint; + + protected TypeScopePropagator(BoundScopePropagator adapter, RelationalQuery allQuery, + RelationalQuery multiQuery) { + this.adapter = adapter; + var queryEngine = adapter.getQueryEngine(); + allNodes = queryEngine.getResultSet(allQuery); + multiNodes = queryEngine.getResultSet(multiQuery); + constraint = adapter.makeConstraint(); + constraint.setBounds(0, Double.POSITIVE_INFINITY); + var cursor = multiNodes.getAll(); + while (cursor.move()) { + var variable = adapter.getVariable(cursor.getKey().get(0)); + constraint.setCoefficient(variable, 1); + } + allNodes.addListener(this::allChanged); + multiNodes.addListener(this::multiChanged); + } + + public abstract void updateBounds(); + + protected int getSingleCount() { + return allNodes.size() - multiNodes.size(); + } + + private void allChanged(Tuple ignoredKey, Boolean ignoredOldValue, Boolean ignoredNewValue) { + adapter.markAsChanged(); + } + + private void multiChanged(Tuple key, Boolean ignoredOldValue, Boolean newValue) { + var variable = adapter.getVariable(key.get(0)); + constraint.setCoefficient(variable, Boolean.TRUE.equals(newValue) ? 1 : 0); + adapter.markAsChanged(); + } + + public abstract static class Factory { + public abstract TypeScopePropagator createPropagator(BoundScopePropagator adapter); + + protected abstract Collection getQueries(); + + public void configure(ModelStoreBuilder storeBuilder) { + storeBuilder.getAdapter(ModelQueryBuilder.class).queries(getQueries()); + } + } +} 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 new file mode 100644 index 00000000..062f976c --- /dev/null +++ b/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/UpperTypeScopePropagator.java @@ -0,0 +1,59 @@ +/* + * SPDX-FileCopyrightText: 2023 The Refinery Authors + * + * SPDX-License-Identifier: EPL-2.0 + */ +package tools.refinery.store.reasoning.scope; + +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.reasoning.representation.PartialRelation; + +import java.util.Collection; +import java.util.List; + +import static tools.refinery.store.reasoning.literal.PartialLiterals.must; +import static tools.refinery.store.reasoning.translator.multiobject.MultiObjectTranslator.MULTI_VIEW; + +class UpperTypeScopePropagator extends TypeScopePropagator { + private final int upperBound; + + private UpperTypeScopePropagator(BoundScopePropagator adapter, int upperBound, RelationalQuery allQuery, + RelationalQuery multiQuery) { + super(adapter, allQuery, multiQuery); + this.upperBound = upperBound; + } + + @Override + public void updateBounds() { + constraint.setUb(upperBound - getSingleCount()); + } + + public static class Factory extends TypeScopePropagator.Factory { + private final int upperBound; + private final RelationalQuery allMust; + private final RelationalQuery multiMust; + + public Factory(PartialRelation type, int upperBound) { + this.upperBound = upperBound; + allMust = Query.of(type.name() + "#must", (builder, instance) -> builder.clause( + must(type.call(instance)) + )); + multiMust = Query.of(type.name() + "#multiMust", (builder, instance) -> builder.clause( + must(type.call(instance)), + MULTI_VIEW.call(instance) + )); + } + + @Override + public TypeScopePropagator createPropagator(BoundScopePropagator adapter) { + return new UpperTypeScopePropagator(adapter, upperBound, allMust, multiMust); + } + + @Override + protected Collection getQueries() { + return List.of(allMust, multiMust); + } + } +} diff --git a/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/internal/LowerTypeScopePropagator.java b/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/internal/LowerTypeScopePropagator.java deleted file mode 100644 index 393c4b72..00000000 --- a/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/internal/LowerTypeScopePropagator.java +++ /dev/null @@ -1,86 +0,0 @@ -/* - * SPDX-FileCopyrightText: 2023 The Refinery Authors - * - * SPDX-License-Identifier: EPL-2.0 - */ -package tools.refinery.store.reasoning.scope.internal; - -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.CountCandidateLowerBoundLiteral; -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.*; -import static tools.refinery.store.reasoning.literal.PartialLiterals.may; -import static tools.refinery.store.reasoning.translator.multiobject.MultiObjectTranslator.MULTI_VIEW; - -class LowerTypeScopePropagator extends TypeScopePropagator { - private final int lowerBound; - - private LowerTypeScopePropagator(ScopePropagatorAdapterImpl adapter, int lowerBound, RelationalQuery allQuery, - RelationalQuery multiQuery) { - super(adapter, allQuery, multiQuery); - this.lowerBound = lowerBound; - } - - @Override - public void updateBounds() { - constraint.setLb((lowerBound - getSingleCount())); - } - - public static class Factory extends TypeScopePropagator.Factory { - private final PartialRelation type; - private final int lowerBound; - private final RelationalQuery allMay; - private final RelationalQuery multiMay; - - public Factory(PartialRelation type, int lowerBound) { - this.type = type; - this.lowerBound = lowerBound; - allMay = Query.of(type.name() + "#may", (builder, instance) -> builder.clause( - may(type.call(instance)) - )); - multiMay = Query.of(type.name() + "#multiMay", (builder, instance) -> builder.clause( - may(type.call(instance)), - MULTI_VIEW.call(instance) - )); - } - - @Override - public TypeScopePropagator createPropagator(ScopePropagatorAdapterImpl adapter) { - return new LowerTypeScopePropagator(adapter, lowerBound, allMay, multiMay); - } - - @Override - protected Collection getQueries() { - return List.of(allMay, multiMay); - } - - @Override - public void configure(ModelStoreBuilder storeBuilder) { - super.configure(storeBuilder); - - var requiredObjects = Query.of(type.name() + "#required", Integer.class, (builder, output) -> builder - .clause(Integer.class, currentCount -> List.of( - new CountCandidateLowerBoundLiteral(currentCount, type, List.of(Variable.of())), - output.assign(sub(currentCount, constant(lowerBound))), - check(greater(currentCount, constant(0))) - ))); - - storeBuilder.getAdapter(ReasoningBuilder.class).objective(Objectives.value(requiredObjects)); - storeBuilder.tryGetAdapter(DesignSpaceExplorationBuilder.class).ifPresent(dseBuilder -> - dseBuilder.accept(Criteria.whenNoMatch(requiredObjects))); - } - } -} diff --git a/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/internal/RoundingUtil.java b/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/internal/RoundingUtil.java deleted file mode 100644 index a6d663ea..00000000 --- a/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/internal/RoundingUtil.java +++ /dev/null @@ -1,26 +0,0 @@ -/* - * SPDX-FileCopyrightText: 2023 The Refinery Authors - * - * SPDX-License-Identifier: EPL-2.0 - */ -package tools.refinery.store.reasoning.scope.internal; - -final class RoundingUtil { - private static final double TOLERANCE = 0.01; - - private RoundingUtil() { - throw new IllegalStateException("This is a static utility class and should not be instantiated directly"); - } - - public static int roundUp(double value) { - double ceil = Math.ceil(value - TOLERANCE); - int intCeil = (int) ceil; - return Math.max(intCeil, 0); - } - - public static int roundDown(double value) { - double floor = Math.floor(value + TOLERANCE); - int intFloor = (int) floor; - return Math.max(intFloor, 0); - } -} diff --git a/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/internal/ScopePropagatorAdapterImpl.java b/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/internal/ScopePropagatorAdapterImpl.java deleted file mode 100644 index 99c501ce..00000000 --- a/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/internal/ScopePropagatorAdapterImpl.java +++ /dev/null @@ -1,253 +0,0 @@ -/* - * SPDX-FileCopyrightText: 2023 The Refinery Authors - * - * SPDX-License-Identifier: EPL-2.0 - */ -package tools.refinery.store.reasoning.scope.internal; - -import com.google.ortools.linearsolver.MPConstraint; -import com.google.ortools.linearsolver.MPObjective; -import com.google.ortools.linearsolver.MPSolver; -import com.google.ortools.linearsolver.MPVariable; -import org.eclipse.collections.api.factory.primitive.IntObjectMaps; -import org.eclipse.collections.api.factory.primitive.IntSets; -import org.eclipse.collections.api.map.primitive.MutableIntObjectMap; -import org.eclipse.collections.api.set.primitive.MutableIntSet; -import tools.refinery.store.model.Interpretation; -import tools.refinery.store.model.Model; -import tools.refinery.store.query.ModelQueryAdapter; -import tools.refinery.store.reasoning.refinement.RefinementResult; -import tools.refinery.store.reasoning.scope.ScopePropagatorAdapter; -import tools.refinery.store.reasoning.scope.ScopePropagatorStoreAdapter; -import tools.refinery.store.representation.cardinality.*; -import tools.refinery.store.tuple.Tuple; - -class ScopePropagatorAdapterImpl implements ScopePropagatorAdapter { - private final Model model; - private final ScopePropagatorStoreAdapterImpl storeAdapter; - private final ModelQueryAdapter queryEngine; - private final Interpretation countInterpretation; - private final MPSolver solver; - private final MPObjective objective; - private final MutableIntObjectMap variables = IntObjectMaps.mutable.empty(); - private final MutableIntSet activeVariables = IntSets.mutable.empty(); - private final TypeScopePropagator[] propagators; - private boolean changed = true; - - public ScopePropagatorAdapterImpl(Model model, ScopePropagatorStoreAdapterImpl storeAdapter) { - this.model = model; - this.storeAdapter = storeAdapter; - queryEngine = model.getAdapter(ModelQueryAdapter.class); - countInterpretation = model.getInterpretation(storeAdapter.getCountSymbol()); - solver = MPSolver.createSolver("GLOP"); - objective = solver.objective(); - initializeVariables(); - countInterpretation.addListener(this::countChanged, true); - var propagatorFactories = storeAdapter.getPropagatorFactories(); - propagators = new TypeScopePropagator[propagatorFactories.size()]; - for (int i = 0; i < propagators.length; i++) { - propagators[i] = propagatorFactories.get(i).createPropagator(this); - } - } - - @Override - public Model getModel() { - return model; - } - - @Override - public ScopePropagatorStoreAdapter getStoreAdapter() { - return storeAdapter; - } - - private void initializeVariables() { - var cursor = countInterpretation.getAll(); - while (cursor.move()) { - var interval = cursor.getValue(); - if (!interval.equals(CardinalityIntervals.ONE)) { - int nodeId = cursor.getKey().get(0); - createVariable(nodeId, interval); - activeVariables.add(nodeId); - } - } - } - - private MPVariable createVariable(int nodeId, CardinalityInterval interval) { - double lowerBound = interval.lowerBound(); - double upperBound = getUpperBound(interval); - var variable = solver.makeNumVar(lowerBound, upperBound, "x" + nodeId); - variables.put(nodeId, variable); - return variable; - } - - private void countChanged(Tuple key, CardinalityInterval fromValue, CardinalityInterval toValue, - boolean ignoredRestoring) { - int nodeId = key.get(0); - if ((toValue == null || toValue.equals(CardinalityIntervals.ONE))) { - if (fromValue != null && !fromValue.equals(CardinalityIntervals.ONE)) { - removeActiveVariable(toValue, nodeId); - } - return; - } - if (fromValue == null || fromValue.equals(CardinalityIntervals.ONE)) { - activeVariables.add(nodeId); - } - var variable = variables.get(nodeId); - if (variable == null) { - createVariable(nodeId, toValue); - markAsChanged(); - return; - } - double lowerBound = toValue.lowerBound(); - double upperBound = getUpperBound(toValue); - if (variable.lb() != lowerBound) { - variable.setLb(lowerBound); - markAsChanged(); - } - if (variable.ub() != upperBound) { - variable.setUb(upperBound); - markAsChanged(); - } - } - - private void removeActiveVariable(CardinalityInterval toValue, int nodeId) { - var variable = variables.get(nodeId); - if (variable == null || !activeVariables.remove(nodeId)) { - throw new AssertionError("Variable not active: " + nodeId); - } - if (toValue == null) { - variable.setBounds(0, 0); - } else { - // Until queries are flushed and the constraints can be properly updated, - // the variable corresponding to the (previous) multi-object has to stand in for a single object. - variable.setBounds(1, 1); - } - markAsChanged(); - } - - MPConstraint makeConstraint() { - return solver.makeConstraint(); - } - - MPVariable getVariable(int nodeId) { - var variable = variables.get(nodeId); - if (variable != null) { - return variable; - } - var interval = countInterpretation.get(Tuple.of(nodeId)); - if (interval == null || interval.equals(CardinalityIntervals.ONE)) { - interval = CardinalityIntervals.NONE; - } else { - activeVariables.add(nodeId); - markAsChanged(); - } - return createVariable(nodeId, interval); - } - - void markAsChanged() { - changed = true; - } - - @Override - public RefinementResult propagate() { - var result = RefinementResult.UNCHANGED; - RefinementResult currentRoundResult; - do { - currentRoundResult = propagateOne(); - result = result.andThen(currentRoundResult); - if (result.isRejected()) { - return result; - } - } while (currentRoundResult != RefinementResult.UNCHANGED); - return result; - } - - private RefinementResult propagateOne() { - queryEngine.flushChanges(); - if (!changed) { - return RefinementResult.UNCHANGED; - } - changed = false; - for (var propagator : propagators) { - propagator.updateBounds(); - } - var result = RefinementResult.UNCHANGED; - if (activeVariables.isEmpty()) { - return checkEmptiness(); - } - var iterator = activeVariables.intIterator(); - while (iterator.hasNext()) { - int nodeId = iterator.next(); - var variable = variables.get(nodeId); - if (variable == null) { - throw new AssertionError("Missing active variable: " + nodeId); - } - result = result.andThen(propagateNode(nodeId, variable)); - if (result.isRejected()) { - return result; - } - } - return result; - } - - private RefinementResult checkEmptiness() { - var emptinessCheckingResult = solver.solve(); - return switch (emptinessCheckingResult) { - case OPTIMAL, UNBOUNDED -> RefinementResult.UNCHANGED; - case INFEASIBLE -> RefinementResult.REJECTED; - default -> throw new IllegalStateException("Failed to check for consistency: " + emptinessCheckingResult); - }; - } - - private RefinementResult propagateNode(int nodeId, MPVariable variable) { - objective.setCoefficient(variable, 1); - try { - objective.setMinimization(); - var minimizationResult = solver.solve(); - int lowerBound; - switch (minimizationResult) { - case OPTIMAL -> lowerBound = RoundingUtil.roundUp(objective.value()); - case UNBOUNDED -> lowerBound = 0; - case INFEASIBLE -> { - return RefinementResult.REJECTED; - } - default -> throw new IllegalStateException("Failed to solve for minimum of %s: %s" - .formatted(variable, minimizationResult)); - } - - objective.setMaximization(); - var maximizationResult = solver.solve(); - UpperCardinality upperBound; - switch (maximizationResult) { - case OPTIMAL -> upperBound = UpperCardinalities.atMost(RoundingUtil.roundDown(objective.value())); - // Problem was feasible when minimizing, the only possible source of {@code UNBOUNDED_OR_INFEASIBLE} is - // an unbounded maximization problem. See https://github.com/google/or-tools/issues/3319 - case UNBOUNDED, INFEASIBLE -> upperBound = UpperCardinalities.UNBOUNDED; - default -> throw new IllegalStateException("Failed to solve for maximum of %s: %s" - .formatted(variable, minimizationResult)); - } - - var newInterval = CardinalityIntervals.between(lowerBound, upperBound); - var oldInterval = countInterpretation.put(Tuple.of(nodeId), newInterval); - if (newInterval.lowerBound() < oldInterval.lowerBound() || - newInterval.upperBound().compareTo(oldInterval.upperBound()) > 0) { - throw new IllegalArgumentException("Failed to refine multiplicity %s of node %d to %s" - .formatted(oldInterval, nodeId, newInterval)); - } - return newInterval.equals(oldInterval) ? RefinementResult.UNCHANGED : RefinementResult.REFINED; - } finally { - objective.setCoefficient(variable, 0); - } - } - - private static double getUpperBound(CardinalityInterval interval) { - var upperBound = interval.upperBound(); - if (upperBound instanceof FiniteUpperCardinality finiteUpperCardinality) { - return finiteUpperCardinality.finiteUpperBound(); - } else if (upperBound instanceof UnboundedUpperCardinality) { - return Double.POSITIVE_INFINITY; - } else { - throw new IllegalArgumentException("Unknown upper bound: " + upperBound); - } - } -} diff --git a/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/internal/ScopePropagatorBuilderImpl.java b/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/internal/ScopePropagatorBuilderImpl.java deleted file mode 100644 index 531a7440..00000000 --- a/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/internal/ScopePropagatorBuilderImpl.java +++ /dev/null @@ -1,86 +0,0 @@ -/* - * SPDX-FileCopyrightText: 2023 The Refinery Authors - * - * SPDX-License-Identifier: EPL-2.0 - */ -package tools.refinery.store.reasoning.scope.internal; - -import com.google.ortools.Loader; -import tools.refinery.store.adapter.AbstractModelAdapterBuilder; -import tools.refinery.store.model.ModelStore; -import tools.refinery.store.model.ModelStoreBuilder; -import tools.refinery.store.reasoning.representation.PartialRelation; -import tools.refinery.store.reasoning.scope.ScopePropagatorBuilder; -import tools.refinery.store.reasoning.scope.ScopePropagatorStoreAdapter; -import tools.refinery.store.reasoning.translator.TranslationException; -import tools.refinery.store.reasoning.translator.multiobject.MultiObjectTranslator; -import tools.refinery.store.representation.Symbol; -import tools.refinery.store.representation.cardinality.CardinalityInterval; -import tools.refinery.store.representation.cardinality.FiniteUpperCardinality; - -import java.util.*; - -public class ScopePropagatorBuilderImpl extends AbstractModelAdapterBuilder - implements ScopePropagatorBuilder { - private Symbol countSymbol = MultiObjectTranslator.COUNT_STORAGE; - private final Map scopes = new LinkedHashMap<>(); - private List typeScopePropagatorFactories; - - @Override - public ScopePropagatorBuilder countSymbol(Symbol countSymbol) { - if (countSymbol.arity() != 1) { - throw new IllegalArgumentException("Count symbol must have arty 1, got %s with arity %d instead" - .formatted(countSymbol, countSymbol.arity())); - } - if (!countSymbol.valueType().equals(CardinalityInterval.class)) { - throw new IllegalArgumentException("Count symbol must have CardinalityInterval values"); - } - if (countSymbol.defaultValue() != null) { - throw new IllegalArgumentException("Count symbol must default value null"); - } - this.countSymbol = countSymbol; - return this; - } - - @Override - public ScopePropagatorBuilder scope(PartialRelation type, CardinalityInterval interval) { - if (type.arity() != 1) { - throw new TranslationException(type, "Only types with arity 1 may have scopes, got %s with arity %d" - .formatted(type, type.arity())); - } - var newValue = scopes.compute(type, (ignoredKey, oldValue) -> - oldValue == null ? interval : oldValue.meet(interval)); - if (newValue.isEmpty()) { - throw new TranslationException(type, "Unsatisfiable scope for type %s".formatted(type)); - } - return this; - } - - @Override - protected void doConfigure(ModelStoreBuilder storeBuilder) { - typeScopePropagatorFactories = new ArrayList<>(scopes.size()); - for (var entry : scopes.entrySet()) { - var type = entry.getKey(); - var bounds = entry.getValue(); - if (bounds.lowerBound() > 0) { - var lowerFactory = new LowerTypeScopePropagator.Factory(type, bounds.lowerBound()); - typeScopePropagatorFactories.add(lowerFactory); - } - if (bounds.upperBound() instanceof FiniteUpperCardinality finiteUpperCardinality) { - var upperFactory = new UpperTypeScopePropagator.Factory(type, - finiteUpperCardinality.finiteUpperBound()); - typeScopePropagatorFactories.add(upperFactory); - } - } - for (var factory : typeScopePropagatorFactories) { - factory.configure(storeBuilder); - } - } - - @Override - protected ScopePropagatorStoreAdapter doBuild(ModelStore store) { - Loader.loadNativeLibraries(); - return new ScopePropagatorStoreAdapterImpl(store, countSymbol, Collections.unmodifiableMap(scopes), - Collections.unmodifiableList(typeScopePropagatorFactories)); - } -} diff --git a/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/internal/ScopePropagatorStoreAdapterImpl.java b/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/internal/ScopePropagatorStoreAdapterImpl.java deleted file mode 100644 index 282ffe6f..00000000 --- a/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/internal/ScopePropagatorStoreAdapterImpl.java +++ /dev/null @@ -1,58 +0,0 @@ -/* - * SPDX-FileCopyrightText: 2023 The Refinery Authors - * - * SPDX-License-Identifier: EPL-2.0 - */ -package tools.refinery.store.reasoning.scope.internal; - -import tools.refinery.store.adapter.ModelAdapter; -import tools.refinery.store.model.Model; -import tools.refinery.store.model.ModelStore; -import tools.refinery.store.reasoning.representation.PartialRelation; -import tools.refinery.store.reasoning.scope.ScopePropagatorStoreAdapter; -import tools.refinery.store.representation.Symbol; -import tools.refinery.store.representation.cardinality.CardinalityInterval; - -import java.util.List; -import java.util.Map; - -// Not a record, because we want to control getter visibility. -@SuppressWarnings("ClassCanBeRecord") -class ScopePropagatorStoreAdapterImpl implements ScopePropagatorStoreAdapter { - private final ModelStore store; - private final Symbol countSymbol; - private final Map scopes; - private final List propagatorFactories; - - public ScopePropagatorStoreAdapterImpl( - ModelStore store, Symbol countSymbol, - Map scopes, List propagatorFactories) { - this.store = store; - this.countSymbol = countSymbol; - this.scopes = scopes; - this.propagatorFactories = propagatorFactories; - } - - @Override - public ModelStore getStore() { - return store; - } - - Symbol getCountSymbol() { - return countSymbol; - } - - @Override - public Map getScopes() { - return scopes; - } - - public List getPropagatorFactories() { - return propagatorFactories; - } - - @Override - public ModelAdapter createModelAdapter(Model model) { - return new ScopePropagatorAdapterImpl(model, this); - } -} diff --git a/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/internal/TypeScopePropagator.java b/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/internal/TypeScopePropagator.java deleted file mode 100644 index cfb95829..00000000 --- a/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/internal/TypeScopePropagator.java +++ /dev/null @@ -1,67 +0,0 @@ -/* - * SPDX-FileCopyrightText: 2023 The Refinery Authors - * - * SPDX-License-Identifier: EPL-2.0 - */ -package tools.refinery.store.reasoning.scope.internal; - -import com.google.ortools.linearsolver.MPConstraint; -import tools.refinery.store.model.ModelStoreBuilder; -import tools.refinery.store.query.ModelQueryAdapter; -import tools.refinery.store.query.ModelQueryBuilder; -import tools.refinery.store.query.dnf.AnyQuery; -import tools.refinery.store.query.dnf.RelationalQuery; -import tools.refinery.store.query.resultset.ResultSet; -import tools.refinery.store.tuple.Tuple; - -import java.util.Collection; - -abstract class TypeScopePropagator { - private final ScopePropagatorAdapterImpl adapter; - private final ResultSet allNodes; - private final ResultSet multiNodes; - protected final MPConstraint constraint; - - protected TypeScopePropagator(ScopePropagatorAdapterImpl adapter, RelationalQuery allQuery, - RelationalQuery multiQuery) { - this.adapter = adapter; - var queryEngine = adapter.getModel().getAdapter(ModelQueryAdapter.class); - allNodes = queryEngine.getResultSet(allQuery); - multiNodes = queryEngine.getResultSet(multiQuery); - constraint = adapter.makeConstraint(); - constraint.setBounds(0, Double.POSITIVE_INFINITY); - var cursor = multiNodes.getAll(); - while (cursor.move()) { - var variable = adapter.getVariable(cursor.getKey().get(0)); - constraint.setCoefficient(variable, 1); - } - allNodes.addListener(this::allChanged); - multiNodes.addListener(this::multiChanged); - } - - public abstract void updateBounds(); - - protected int getSingleCount() { - return allNodes.size() - multiNodes.size(); - } - - private void allChanged(Tuple ignoredKey, Boolean ignoredOldValue, Boolean ignoredNewValue) { - adapter.markAsChanged(); - } - - private void multiChanged(Tuple key, Boolean ignoredOldValue, Boolean newValue) { - var variable = adapter.getVariable(key.get(0)); - constraint.setCoefficient(variable, Boolean.TRUE.equals(newValue) ? 1 : 0); - adapter.markAsChanged(); - } - - public abstract static class Factory { - public abstract TypeScopePropagator createPropagator(ScopePropagatorAdapterImpl adapter); - - protected abstract Collection getQueries(); - - public void configure(ModelStoreBuilder storeBuilder) { - storeBuilder.getAdapter(ModelQueryBuilder.class).queries(getQueries()); - } - } -} diff --git a/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/internal/UpperTypeScopePropagator.java b/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/internal/UpperTypeScopePropagator.java deleted file mode 100644 index a0be0fb4..00000000 --- a/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/internal/UpperTypeScopePropagator.java +++ /dev/null @@ -1,59 +0,0 @@ -/* - * SPDX-FileCopyrightText: 2023 The Refinery Authors - * - * SPDX-License-Identifier: EPL-2.0 - */ -package tools.refinery.store.reasoning.scope.internal; - -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.reasoning.representation.PartialRelation; - -import java.util.Collection; -import java.util.List; - -import static tools.refinery.store.reasoning.literal.PartialLiterals.must; -import static tools.refinery.store.reasoning.translator.multiobject.MultiObjectTranslator.MULTI_VIEW; - -class UpperTypeScopePropagator extends TypeScopePropagator { - private final int upperBound; - - private UpperTypeScopePropagator(ScopePropagatorAdapterImpl adapter, int upperBound, RelationalQuery allQuery, - RelationalQuery multiQuery) { - super(adapter, allQuery, multiQuery); - this.upperBound = upperBound; - } - - @Override - public void updateBounds() { - constraint.setUb(upperBound - getSingleCount()); - } - - public static class Factory extends TypeScopePropagator.Factory { - private final int upperBound; - private final RelationalQuery allMust; - private final RelationalQuery multiMust; - - public Factory(PartialRelation type, int upperBound) { - this.upperBound = upperBound; - allMust = Query.of(type.name() + "#must", (builder, instance) -> builder.clause( - must(type.call(instance)) - )); - multiMust = Query.of(type.name() + "#multiMust", (builder, instance) -> builder.clause( - must(type.call(instance)), - MULTI_VIEW.call(instance) - )); - } - - @Override - public TypeScopePropagator createPropagator(ScopePropagatorAdapterImpl adapter) { - return new UpperTypeScopePropagator(adapter, upperBound, allMust, multiMust); - } - - @Override - protected Collection getQueries() { - return List.of(allMust, multiMust); - } - } -} diff --git a/subprojects/store-reasoning-scope/src/test/java/tools/refinery/store/reasoning/scope/MultiObjectTest.java b/subprojects/store-reasoning-scope/src/test/java/tools/refinery/store/reasoning/scope/MultiObjectTest.java index 42ce2f56..5fc70ae1 100644 --- a/subprojects/store-reasoning-scope/src/test/java/tools/refinery/store/reasoning/scope/MultiObjectTest.java +++ b/subprojects/store-reasoning-scope/src/test/java/tools/refinery/store/reasoning/scope/MultiObjectTest.java @@ -7,13 +7,14 @@ package tools.refinery.store.reasoning.scope; import org.junit.jupiter.api.BeforeEach; import org.junit.jupiter.api.Test; +import tools.refinery.store.dse.propagation.PropagationAdapter; +import tools.refinery.store.dse.propagation.PropagationResult; import tools.refinery.store.model.Interpretation; import tools.refinery.store.model.Model; import tools.refinery.store.model.ModelStore; import tools.refinery.store.query.viatra.ViatraModelQueryAdapter; import tools.refinery.store.reasoning.ReasoningAdapter; import tools.refinery.store.reasoning.ReasoningStoreAdapter; -import tools.refinery.store.reasoning.refinement.RefinementResult; import tools.refinery.store.reasoning.representation.PartialRelation; import tools.refinery.store.reasoning.seed.ModelSeed; import tools.refinery.store.reasoning.translator.PartialRelationTranslator; @@ -38,11 +39,12 @@ class MultiObjectTest { void beforeEach() { store = ModelStore.builder() .with(ViatraModelQueryAdapter.builder()) + .with(PropagationAdapter.builder()) .with(ReasoningAdapter.builder()) .with(new MultiObjectTranslator()) .with(PartialRelationTranslator.of(person) .symbol(Symbol.of("Person", 1, TruthValue.class, TruthValue.FALSE))) - .with(ScopePropagatorAdapter.builder() + .with(new ScopePropagator() .scope(person, CardinalityIntervals.between(5, 15))) .build(); model = null; @@ -57,7 +59,7 @@ class MultiObjectTest { .put(Tuple.of(0), CardinalityIntervals.SET)) .seed(person, builder -> builder.reducedValue(TruthValue.TRUE)) .build()); - assertThat(propagate(), is(RefinementResult.REFINED)); + assertThat(propagate(), is(PropagationResult.PROPAGATED)); assertThat(countStorage.get(Tuple.of(0)), is(CardinalityIntervals.between(2, 12))); } @@ -69,7 +71,7 @@ class MultiObjectTest { .put(Tuple.of(0), CardinalityIntervals.between(5, 20))) .seed(person, builder -> builder.reducedValue(TruthValue.TRUE)) .build()); - assertThat(propagate(), is(RefinementResult.REFINED)); + assertThat(propagate(), is(PropagationResult.PROPAGATED)); assertThat(countStorage.get(Tuple.of(0)), is(CardinalityIntervals.between(5, 12))); } @@ -81,7 +83,7 @@ class MultiObjectTest { .put(Tuple.of(0), CardinalityIntervals.SET)) .seed(person, builder -> builder.reducedValue(TruthValue.TRUE)) .build()); - assertThat(propagate(), is(RefinementResult.REJECTED)); + assertThat(propagate(), is(PropagationResult.REJECTED)); } @Test @@ -90,7 +92,7 @@ class MultiObjectTest { .seed(MultiObjectTranslator.COUNT_SYMBOL, builder -> builder.reducedValue(CardinalityIntervals.ONE)) .seed(person, builder -> builder.reducedValue(TruthValue.TRUE)) .build()); - assertThat(propagate(), is(RefinementResult.UNCHANGED)); + assertThat(propagate(), is(PropagationResult.UNCHANGED)); } @Test @@ -99,7 +101,7 @@ class MultiObjectTest { .seed(MultiObjectTranslator.COUNT_SYMBOL, builder -> builder.reducedValue(CardinalityIntervals.ONE)) .seed(person, builder -> builder.reducedValue(TruthValue.TRUE)) .build()); - assertThat(propagate(), is(RefinementResult.REJECTED)); + assertThat(propagate(), is(PropagationResult.REJECTED)); } @Test @@ -110,7 +112,7 @@ class MultiObjectTest { .put(Tuple.of(0), CardinalityIntervals.atLeast(20))) .seed(person, builder -> builder.reducedValue(TruthValue.TRUE)) .build()); - assertThat(propagate(), is(RefinementResult.REJECTED)); + assertThat(propagate(), is(PropagationResult.REJECTED)); } @Test @@ -121,7 +123,7 @@ class MultiObjectTest { .put(Tuple.of(0), CardinalityIntervals.atMost(1))) .seed(person, builder -> builder.reducedValue(TruthValue.TRUE)) .build()); - assertThat(propagate(), is(RefinementResult.REJECTED)); + assertThat(propagate(), is(PropagationResult.REJECTED)); } @Test @@ -133,7 +135,7 @@ class MultiObjectTest { .put(Tuple.of(1), CardinalityIntervals.SET)) .seed(person, builder -> builder.reducedValue(TruthValue.TRUE)) .build()); - assertThat(propagate(), is(RefinementResult.REFINED)); + assertThat(propagate(), is(PropagationResult.PROPAGATED)); assertThat(countStorage.get(Tuple.of(0)), is(CardinalityIntervals.atMost(12))); assertThat(countStorage.get(Tuple.of(1)), is(CardinalityIntervals.atMost(12))); } @@ -147,7 +149,7 @@ class MultiObjectTest { .put(Tuple.of(1), CardinalityIntervals.atMost(11))) .seed(person, builder -> builder.reducedValue(TruthValue.TRUE)) .build()); - assertThat(propagate(), is(RefinementResult.REFINED)); + assertThat(propagate(), is(PropagationResult.PROPAGATED)); assertThat(countStorage.get(Tuple.of(0)), is(CardinalityIntervals.between(7, 12))); assertThat(countStorage.get(Tuple.of(1)), is(CardinalityIntervals.atMost(5))); } @@ -161,7 +163,7 @@ class MultiObjectTest { .put(Tuple.of(1), CardinalityIntervals.exactly(11))) .seed(person, builder -> builder.reducedValue(TruthValue.TRUE)) .build()); - assertThat(propagate(), is(RefinementResult.REJECTED)); + assertThat(propagate(), is(PropagationResult.REJECTED)); } @Test @@ -173,7 +175,7 @@ class MultiObjectTest { .put(Tuple.of(1), CardinalityIntervals.atMost(2))) .seed(person, builder -> builder.reducedValue(TruthValue.TRUE)) .build()); - assertThat(propagate(), is(RefinementResult.REJECTED)); + assertThat(propagate(), is(PropagationResult.REJECTED)); } @Test @@ -185,14 +187,14 @@ class MultiObjectTest { .put(Tuple.of(1), CardinalityIntervals.SET)) .seed(person, builder -> builder.reducedValue(TruthValue.TRUE)) .build()); - assertThat(propagate(), is(RefinementResult.REFINED)); + assertThat(propagate(), is(PropagationResult.PROPAGATED)); assertThat(countStorage.get(Tuple.of(0)), is(CardinalityIntervals.LONE)); assertThat(countStorage.get(Tuple.of(1)), is(CardinalityIntervals.between(1, 12))); countStorage.put(Tuple.of(0), CardinalityIntervals.ONE); - assertThat(propagate(), is(RefinementResult.REFINED)); + assertThat(propagate(), is(PropagationResult.PROPAGATED)); assertThat(countStorage.get(Tuple.of(1)), is(CardinalityIntervals.between(1, 11))); countStorage.put(Tuple.of(1), CardinalityIntervals.ONE); - assertThat(propagate(), is(RefinementResult.UNCHANGED)); + assertThat(propagate(), is(PropagationResult.UNCHANGED)); } private void createModel(ModelSeed modelSeed) { @@ -200,7 +202,7 @@ class MultiObjectTest { countStorage = model.getInterpretation(MultiObjectTranslator.COUNT_STORAGE); } - private RefinementResult propagate() { - return model.getAdapter(ScopePropagatorAdapter.class).propagate(); + private PropagationResult propagate() { + return model.getAdapter(PropagationAdapter.class).propagate(); } } diff --git a/subprojects/store-reasoning-scope/src/test/java/tools/refinery/store/reasoning/scope/RoundingUtilTest.java b/subprojects/store-reasoning-scope/src/test/java/tools/refinery/store/reasoning/scope/RoundingUtilTest.java new file mode 100644 index 00000000..e697298e --- /dev/null +++ b/subprojects/store-reasoning-scope/src/test/java/tools/refinery/store/reasoning/scope/RoundingUtilTest.java @@ -0,0 +1,69 @@ +/* + * SPDX-FileCopyrightText: 2023 The Refinery Authors + * + * SPDX-License-Identifier: EPL-2.0 + */ +package tools.refinery.store.reasoning.scope; + +import org.junit.jupiter.params.ParameterizedTest; +import org.junit.jupiter.params.provider.Arguments; +import org.junit.jupiter.params.provider.MethodSource; + +import java.util.stream.Stream; + +import static org.hamcrest.MatcherAssert.assertThat; +import static org.hamcrest.Matchers.is; + +class RoundingUtilTest { + @ParameterizedTest + @MethodSource + void roundUpTest(double value, int expected) { + int actual = RoundingUtil.roundUp(value); + assertThat(actual, is(expected)); + } + + static Stream roundUpTest() { + return Stream.of( + Arguments.of(0.0, 0), + Arguments.of(-0.0, 0), + Arguments.of(-0.9, 0), + Arguments.of(-2, 0), + Arguments.of(0.009, 0), + Arguments.of(0.011, 1), + Arguments.of(0.1, 1), + Arguments.of(0.991, 1), + Arguments.of(1, 1), + Arguments.of(1.009, 1), + Arguments.of(1.011, 2), + Arguments.of(1.5, 2), + Arguments.of(2, 2), + Arguments.of(100.5, 101) + ); + } + + @ParameterizedTest + @MethodSource + void roundDownTest(double value, int expected) { + int actual = RoundingUtil.roundDown(value); + assertThat(actual, is(expected)); + } + + static Stream roundDownTest() { + return Stream.of( + Arguments.of(0.0, 0), + Arguments.of(-0.0, 0), + Arguments.of(-0.9, 0), + Arguments.of(-2, 0), + Arguments.of(0.989, 0), + Arguments.of(0.991, 1), + Arguments.of(1, 1), + Arguments.of(1.5, 1), + Arguments.of(1.009, 1), + Arguments.of(1.989, 1), + Arguments.of(1.991, 2), + Arguments.of(2, 2), + Arguments.of(2.009, 2), + Arguments.of(100.5, 100) + ); + } +} diff --git a/subprojects/store-reasoning-scope/src/test/java/tools/refinery/store/reasoning/scope/internal/RoundingUtilTest.java b/subprojects/store-reasoning-scope/src/test/java/tools/refinery/store/reasoning/scope/internal/RoundingUtilTest.java deleted file mode 100644 index 9daed660..00000000 --- a/subprojects/store-reasoning-scope/src/test/java/tools/refinery/store/reasoning/scope/internal/RoundingUtilTest.java +++ /dev/null @@ -1,69 +0,0 @@ -/* - * SPDX-FileCopyrightText: 2023 The Refinery Authors - * - * SPDX-License-Identifier: EPL-2.0 - */ -package tools.refinery.store.reasoning.scope.internal; - -import org.junit.jupiter.params.ParameterizedTest; -import org.junit.jupiter.params.provider.Arguments; -import org.junit.jupiter.params.provider.MethodSource; - -import java.util.stream.Stream; - -import static org.hamcrest.MatcherAssert.assertThat; -import static org.hamcrest.Matchers.is; - -class RoundingUtilTest { - @ParameterizedTest - @MethodSource - void roundUpTest(double value, int expected) { - int actual = RoundingUtil.roundUp(value); - assertThat(actual, is(expected)); - } - - static Stream roundUpTest() { - return Stream.of( - Arguments.of(0.0, 0), - Arguments.of(-0.0, 0), - Arguments.of(-0.9, 0), - Arguments.of(-2, 0), - Arguments.of(0.009, 0), - Arguments.of(0.011, 1), - Arguments.of(0.1, 1), - Arguments.of(0.991, 1), - Arguments.of(1, 1), - Arguments.of(1.009, 1), - Arguments.of(1.011, 2), - Arguments.of(1.5, 2), - Arguments.of(2, 2), - Arguments.of(100.5, 101) - ); - } - - @ParameterizedTest - @MethodSource - void roundDownTest(double value, int expected) { - int actual = RoundingUtil.roundDown(value); - assertThat(actual, is(expected)); - } - - static Stream roundDownTest() { - return Stream.of( - Arguments.of(0.0, 0), - Arguments.of(-0.0, 0), - Arguments.of(-0.9, 0), - Arguments.of(-2, 0), - Arguments.of(0.989, 0), - Arguments.of(0.991, 1), - Arguments.of(1, 1), - Arguments.of(1.5, 1), - Arguments.of(1.009, 1), - Arguments.of(1.989, 1), - Arguments.of(1.991, 2), - Arguments.of(2, 2), - Arguments.of(2.009, 2), - Arguments.of(100.5, 100) - ); - } -} -- cgit v1.2.3-70-g09d2