feat: declarative DSE rules and model refinement

12 files changed, 400 insertions, 23 deletions

diff --git a/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/DesignSpaceExplorationAdapter.java b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/DesignSpaceExplorationAdapter.java
index 37448309..d326f1dd 100644
--- a/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/DesignSpaceExplorationAdapter.java
+++ b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/DesignSpaceExplorationAdapter.java
@@ -7,25 +7,22 @@ package tools.refinery.store.dse.transition;
 
 import tools.refinery.store.adapter.ModelAdapter;
 import tools.refinery.store.dse.transition.internal.DesignSpaceExplorationBuilderImpl;
-import tools.refinery.store.map.Version;
-import tools.refinery.store.tuple.Tuple;
-import tools.refinery.store.tuple.Tuple1;
 
-import java.util.Collection;
 import java.util.List;
 
 public interface DesignSpaceExplorationAdapter extends ModelAdapter {
-
-
-
         @Override
         DesignSpaceExplorationStoreAdapter getStoreAdapter();
 
         static DesignSpaceExplorationBuilder builder() {
                 return new DesignSpaceExplorationBuilderImpl();
         }
+
         List<Transformation> getTransformations();
+
         boolean checkAccept();
+
         boolean checkExclude();
+
         ObjectiveValue getObjectiveValue();
 }
diff --git a/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/objectives/AndCriterion.java b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/objectives/AndCriterion.java
new file mode 100644
index 00000000..0ad2b7a4
--- /dev/null
+++ b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/objectives/AndCriterion.java
@@ -0,0 +1,53 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.dse.transition.objectives;
+
+import tools.refinery.store.model.Model;
+import tools.refinery.store.model.ModelStore;
+import tools.refinery.store.query.literal.Reduction;
+
+import java.util.ArrayList;
+import java.util.Collection;
+
+public final class AndCriterion extends CompositeCriterion {
+        AndCriterion(Collection<? extends Criterion> criteria) {
+                super(criteria);
+        }
+
+        @Override
+        public Reduction getReduction(ModelStore store) {
+                for (var criterion : getCriteria()) {
+                        var reduction = criterion.getReduction(store);
+                        if (reduction == Reduction.ALWAYS_FALSE) {
+                                return Reduction.ALWAYS_FALSE;
+                        } else if (reduction == Reduction.NOT_REDUCIBLE) {
+                                return Reduction.NOT_REDUCIBLE;
+                        }
+                }
+                return Reduction.ALWAYS_TRUE;
+        }
+
+        @Override
+        public CriterionCalculator createCalculator(Model model) {
+                var calculators = new ArrayList<CriterionCalculator>();
+                for (var criterion : getCriteria()) {
+                        var reduction = criterion.getReduction(model.getStore());
+                        if (reduction == Reduction.ALWAYS_FALSE) {
+                                return () -> false;
+                        } else if (reduction == Reduction.NOT_REDUCIBLE) {
+                                calculators.add(criterion.createCalculator(model));
+                        }
+                }
+                return () -> {
+                        for (var calculator : calculators) {
+                                if (!calculator.isSatisfied()) {
+                                        return false;
+                                }
+                        }
+                        return true;
+                };
+        }
+}
diff --git a/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/objectives/CompositeCriterion.java b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/objectives/CompositeCriterion.java
new file mode 100644
index 00000000..5746cc7e
--- /dev/null
+++ b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/objectives/CompositeCriterion.java
@@ -0,0 +1,43 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.dse.transition.objectives;
+
+import tools.refinery.store.model.ModelStore;
+import tools.refinery.store.model.ModelStoreBuilder;
+import tools.refinery.store.query.literal.Reduction;
+
+import java.util.*;
+
+public abstract sealed class CompositeCriterion implements Criterion permits AndCriterion, OrCriterion {
+        private final List<Criterion> criteria;
+
+        protected CompositeCriterion(Collection<? extends Criterion> criteria) {
+                var deDuplicatedCriteria = new LinkedHashSet<Criterion>();
+                for (var criterion : criteria) {
+                        if (criterion.getClass() == this.getClass()) {
+                                var childCriteria = ((CompositeCriterion) criterion).getCriteria();
+                                deDuplicatedCriteria.addAll(childCriteria);
+                        } else {
+                                deDuplicatedCriteria.add(criterion);
+                        }
+                }
+                this.criteria = List.copyOf(deDuplicatedCriteria);
+        }
+
+        public List<Criterion> getCriteria() {
+                return criteria;
+        }
+
+        @Override
+        public abstract Reduction getReduction(ModelStore store);
+
+        @Override
+        public void configure(ModelStoreBuilder storeBuilder) {
+                for (var criterion : criteria) {
+                        criterion.configure(storeBuilder);
+                }
+        }
+}
diff --git a/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/objectives/CompositeObjective.java b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/objectives/CompositeObjective.java
new file mode 100644
index 00000000..192a824b
--- /dev/null
+++ b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/objectives/CompositeObjective.java
@@ -0,0 +1,69 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.dse.transition.objectives;
+
+import tools.refinery.store.model.Model;
+import tools.refinery.store.model.ModelStore;
+import tools.refinery.store.model.ModelStoreBuilder;
+
+import java.util.ArrayList;
+import java.util.Collection;
+import java.util.Collections;
+import java.util.List;
+
+public class CompositeObjective implements Objective {
+        private final List<Objective> objectives;
+
+        CompositeObjective(Collection<? extends Objective> objectives) {
+                var unwrappedObjectives = new ArrayList<Objective>();
+                for (var objective : objectives) {
+                        if (objective instanceof CompositeObjective compositeObjective) {
+                                unwrappedObjectives.addAll(compositeObjective.getObjectives());
+                        } else {
+                                unwrappedObjectives.add(objective);
+                        }
+                }
+                this.objectives = Collections.unmodifiableList(unwrappedObjectives);
+        }
+
+        public List<Objective> getObjectives() {
+                return objectives;
+        }
+
+        @Override
+        public boolean isAlwaysZero(ModelStore store) {
+                for (var objective : objectives) {
+                        if (!objective.isAlwaysZero(store)) {
+                                return false;
+                        }
+                }
+                return true;
+        }
+
+        @Override
+        public ObjectiveCalculator createCalculator(Model model) {
+                var calculators = new ArrayList<ObjectiveCalculator>();
+                for (var objective : objectives) {
+                        if (!objective.isAlwaysZero(model.getStore())) {
+                                calculators.add(objective.createCalculator(model));
+                        }
+                }
+                return () -> {
+                        double value = 0;
+                        for (var calculator : calculators) {
+                                value += calculator.getValue();
+                        }
+                        return value;
+                };
+        }
+
+        @Override
+        public void configure(ModelStoreBuilder storeBuilder) {
+                for (var objective : objectives) {
+                        objective.configure(storeBuilder);
+                }
+        }
+}
diff --git a/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/objectives/CountObjective.java b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/objectives/CountObjective.java
new file mode 100644
index 00000000..fbd05ded
--- /dev/null
+++ b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/objectives/CountObjective.java
@@ -0,0 +1,47 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.dse.transition.objectives;
+
+import tools.refinery.store.model.Model;
+import tools.refinery.store.model.ModelStore;
+import tools.refinery.store.model.ModelStoreBuilder;
+import tools.refinery.store.query.ModelQueryAdapter;
+import tools.refinery.store.query.ModelQueryBuilder;
+import tools.refinery.store.query.ModelQueryStoreAdapter;
+import tools.refinery.store.query.dnf.RelationalQuery;
+import tools.refinery.store.query.literal.Reduction;
+
+public class CountObjective implements Objective {
+        private final RelationalQuery query;
+        private final double weight;
+
+        public CountObjective(RelationalQuery query) {
+                this(query, 1);
+        }
+
+        public CountObjective(RelationalQuery query, double weight) {
+                this.query = query;
+                this.weight = weight;
+        }
+
+        @Override
+        public boolean isAlwaysZero(ModelStore store) {
+                var queryStore = store.getAdapter(ModelQueryStoreAdapter.class);
+                var canonicalQuery = queryStore.getCanonicalQuery(query);
+                return canonicalQuery.getDnf().getReduction() == Reduction.ALWAYS_FALSE;
+        }
+
+        @Override
+        public ObjectiveCalculator createCalculator(Model model) {
+                var resultSet = model.getAdapter(ModelQueryAdapter.class).getResultSet(query);
+                return () -> resultSet.size() * weight;
+        }
+
+        @Override
+        public void configure(ModelStoreBuilder storeBuilder) {
+                storeBuilder.getAdapter(ModelQueryBuilder.class).query(query);
+        }
+}
diff --git a/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/objectives/Criteria.java b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/objectives/Criteria.java
new file mode 100644
index 00000000..0e4ec5c9
--- /dev/null
+++ b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/objectives/Criteria.java
@@ -0,0 +1,47 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.dse.transition.objectives;
+
+import tools.refinery.store.query.dnf.AnyQuery;
+
+import java.util.Collection;
+import java.util.List;
+
+public final class Criteria {
+        private Criteria() {
+                throw new IllegalStateException("This is a static utility class and should not be instantiated directly");
+        }
+
+        public static QueryCriterion whenHasMatch(AnyQuery query) {
+                return new QueryCriterion(query, true);
+        }
+
+        public static QueryCriterion whenNoMatch(AnyQuery query) {
+                return new QueryCriterion(query, false);
+        }
+
+        public static Criterion and(Criterion... criteria) {
+                return and(List.of(criteria));
+        }
+
+        public static Criterion and(Collection<? extends Criterion> criteria) {
+                if (criteria.size() == 1) {
+                        return criteria.iterator().next();
+                }
+                return new AndCriterion(criteria);
+        }
+
+        public static Criterion or(Criterion... criteria) {
+                return or(List.of(criteria));
+        }
+
+        public static Criterion or(Collection<? extends Criterion> criteria) {
+                if (criteria.size() == 1) {
+                        return criteria.iterator().next();
+                }
+                return new OrCriterion(criteria);
+        }
+}
diff --git a/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/objectives/Criterion.java b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/objectives/Criterion.java
index 4365cf9c..c827f20e 100644
--- a/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/objectives/Criterion.java
+++ b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/objectives/Criterion.java
@@ -6,10 +6,17 @@
 package tools.refinery.store.dse.transition.objectives;
 
 import tools.refinery.store.model.Model;
+import tools.refinery.store.model.ModelStore;
 import tools.refinery.store.model.ModelStoreBuilder;
+import tools.refinery.store.query.literal.Reduction;
 
 public interface Criterion {
         default void configure(ModelStoreBuilder storeBuilder) {
         }
+
+        default Reduction getReduction(ModelStore store) {
+                return Reduction.NOT_REDUCIBLE;
+        }
+
         CriterionCalculator createCalculator(Model model);
 }
diff --git a/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/objectives/Objective.java b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/objectives/Objective.java
index d2476a2e..49c34d87 100644
--- a/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/objectives/Objective.java
+++ b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/objectives/Objective.java
@@ -6,10 +6,18 @@
 package tools.refinery.store.dse.transition.objectives;
 
 import tools.refinery.store.model.Model;
+import tools.refinery.store.model.ModelStore;
 import tools.refinery.store.model.ModelStoreBuilder;
 
 public interface Objective {
         default void configure(ModelStoreBuilder storeBuilder) {
         }
+
+        // The name {@code isAlwaysZero} is more straightforward than something like {@code canBeNonZero}.
+        @SuppressWarnings("BooleanMethodIsAlwaysInverted")
+        default boolean isAlwaysZero(ModelStore store) {
+                return false;
+        }
+
         ObjectiveCalculator createCalculator(Model model);
 }
diff --git a/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/objectives/Objectives.java b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/objectives/Objectives.java
new file mode 100644
index 00000000..e552d14c
--- /dev/null
+++ b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/objectives/Objectives.java
@@ -0,0 +1,41 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.dse.transition.objectives;
+
+import tools.refinery.store.query.dnf.FunctionalQuery;
+import tools.refinery.store.query.dnf.RelationalQuery;
+
+import java.util.Collection;
+import java.util.List;
+
+public final class Objectives {
+        private Objectives() {
+                throw new IllegalStateException("This is a static utility class and should not be instantiated directly");
+        }
+
+        public static CountObjective count(RelationalQuery query, double weight) {
+                return new CountObjective(query, weight);
+        }
+
+        public static CountObjective count(RelationalQuery query) {
+                return new CountObjective(query);
+        }
+
+        public static QueryObjective value(FunctionalQuery<? extends Number> query) {
+                return new QueryObjective(query);
+        }
+
+        public static Objective sum(Objective... objectives) {
+                return sum(List.of(objectives));
+        }
+
+        public static Objective sum(Collection<? extends Objective> objectives) {
+                if (objectives.size() == 1) {
+                        return objectives.iterator().next();
+                }
+                return new CompositeObjective(objectives);
+        }
+}
diff --git a/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/objectives/OrCriterion.java b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/objectives/OrCriterion.java
new file mode 100644
index 00000000..7a8d7778
--- /dev/null
+++ b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/objectives/OrCriterion.java
@@ -0,0 +1,53 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.dse.transition.objectives;
+
+import tools.refinery.store.model.Model;
+import tools.refinery.store.model.ModelStore;
+import tools.refinery.store.query.literal.Reduction;
+
+import java.util.ArrayList;
+import java.util.Collection;
+
+public final class OrCriterion extends CompositeCriterion {
+        OrCriterion(Collection<? extends Criterion> criteria) {
+                super(criteria);
+        }
+
+        @Override
+        public Reduction getReduction(ModelStore store) {
+                for (var criterion : getCriteria()) {
+                        var reduction = criterion.getReduction(store);
+                        if (reduction == Reduction.ALWAYS_TRUE) {
+                                return Reduction.ALWAYS_TRUE;
+                        } else if (reduction == Reduction.NOT_REDUCIBLE) {
+                                return Reduction.NOT_REDUCIBLE;
+                        }
+                }
+                return Reduction.ALWAYS_FALSE;
+        }
+
+        @Override
+        public CriterionCalculator createCalculator(Model model) {
+                var calculators = new ArrayList<CriterionCalculator>();
+                for (var criterion : getCriteria()) {
+                        var reduction = criterion.getReduction(model.getStore());
+                        if (reduction == Reduction.ALWAYS_TRUE) {
+                                return () -> true;
+                        } else if (reduction == Reduction.NOT_REDUCIBLE) {
+                                calculators.add(criterion.createCalculator(model));
+                        }
+                }
+                return () -> {
+                        for (var calculator : calculators) {
+                                if (calculator.isSatisfied()) {
+                                        return true;
+                                }
+                        }
+                        return false;
+                };
+        }
+}
diff --git a/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/objectives/QueryCriteria.java b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/objectives/QueryCriterion.java
index 8d0a56cf..e15e4e41 100644
--- a/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/objectives/QueryCriteria.java
+++ b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/objectives/QueryCriterion.java
@@ -6,30 +6,45 @@
 package tools.refinery.store.dse.transition.objectives;
 
 import tools.refinery.store.model.Model;
+import tools.refinery.store.model.ModelStore;
 import tools.refinery.store.model.ModelStoreBuilder;
 import tools.refinery.store.query.ModelQueryAdapter;
 import tools.refinery.store.query.ModelQueryBuilder;
+import tools.refinery.store.query.ModelQueryStoreAdapter;
 import tools.refinery.store.query.dnf.AnyQuery;
+import tools.refinery.store.query.literal.Reduction;
 
-public class QueryCriteria implements Criterion {
-        protected final boolean acceptIfHasMatch;
+public class QueryCriterion implements Criterion {
+        protected final boolean satisfiedIfHasMatch;
         protected final AnyQuery query;
 
         /**
          * Criteria based on the existence of matches evaluated on the model.
-         * @param query The query evaluated on the model.
-         * @param acceptIfHasMatch If true, the criteria satisfied if the query has any match on the model. Otherwise,
+         *
+         * @param query               The query evaluated on the model.
+         * @param satisfiedIfHasMatch If true, the criteria satisfied if the query has any match on the model. Otherwise,
          *                            the criteria satisfied if the query has no match on the model.
          */
-        public QueryCriteria(AnyQuery query, boolean acceptIfHasMatch) {
+        public QueryCriterion(AnyQuery query, boolean satisfiedIfHasMatch) {
                 this.query = query;
-                this.acceptIfHasMatch = acceptIfHasMatch;
+                this.satisfiedIfHasMatch = satisfiedIfHasMatch;
+        }
+
+        @Override
+        public Reduction getReduction(ModelStore store) {
+                var queryStore = store.getAdapter(ModelQueryStoreAdapter.class);
+                var canonicalQuery = queryStore.getCanonicalQuery(query);
+                var reduction = canonicalQuery.getDnf().getReduction();
+                if (satisfiedIfHasMatch) {
+                        return reduction;
+                }
+                return reduction.negate();
         }
 
         @Override
         public CriterionCalculator createCalculator(Model model) {
                 var resultSet = model.getAdapter(ModelQueryAdapter.class).getResultSet(query);
-                if(acceptIfHasMatch) {
+                if (satisfiedIfHasMatch) {
                         return () -> resultSet.size() > 0;
                 } else {
                         return () -> resultSet.size() == 0;
diff --git a/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/objectives/QueryObjective.java b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/objectives/QueryObjective.java
index 9553e0e0..9f4bb536 100644
--- a/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/objectives/QueryObjective.java
+++ b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/objectives/QueryObjective.java
@@ -15,6 +15,10 @@ public class QueryObjective implements Objective {
         protected final FunctionalQuery<? extends Number> objectiveFunction;
 
         public QueryObjective(FunctionalQuery<? extends Number> objectiveFunction) {
+                if (objectiveFunction.arity() != 0) {
+                        throw new IllegalArgumentException("Objective functions must have 0 parameters, got %d instead"
+                                        .formatted(objectiveFunction.arity()));
+                }
                 this.objectiveFunction = objectiveFunction;
         }
 
@@ -23,22 +27,15 @@ public class QueryObjective implements Objective {
                 var resultSet = model.getAdapter(ModelQueryAdapter.class).getResultSet(objectiveFunction);
                 return () -> {
                         var cursor = resultSet.getAll();
-                        boolean hasElement = cursor.move();
-                        if(hasElement) {
-                                double result = cursor.getValue().doubleValue();
-                                if(cursor.move()) {
-                                        throw new IllegalStateException("Query providing the objective function has multiple values!");
-                                }
-                                return result;
-                        } else {
+                        if (!cursor.move()) {
                                 throw new IllegalStateException("Query providing the objective function has no values!");
                         }
+                        return cursor.getValue().doubleValue();
                 };
         }
 
         @Override
         public void configure(ModelStoreBuilder storeBuilder) {
-                Objective.super.configure(storeBuilder);
                 storeBuilder.getAdapter(ModelQueryBuilder.class).query(objectiveFunction);
         }
 }