1 files changed, 103 insertions, 0 deletions

diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/BasicScopeGlobalConstraint.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/BasicScopeGlobalConstraint.xtend
new file mode 100644
index 00000000..67f447ed
--- /dev/null
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/BasicScopeGlobalConstraint.xtend
@@ -0,0 +1,103 @@
+package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse
+
+import com.google.common.collect.ImmutableList
+import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation
+import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialTypeInterpratation
+import java.util.Comparator
+import java.util.List
+import org.eclipse.viatra.dse.base.ThreadContext
+import org.eclipse.viatra.dse.objectives.Comparators
+import org.eclipse.viatra.dse.objectives.IGlobalConstraint
+import org.eclipse.viatra.dse.objectives.IObjective
+import org.eclipse.xtend.lib.annotations.FinalFieldsConstructor
+
+class BasicScopeGlobalConstraint implements IGlobalConstraint, IObjective {
+        val PartialInterpretation p
+        val List<ScopeAssertion> assertions
+
+        new(PartialInterpretation p) {
+                this.p = p
+                assertions = ImmutableList.copyOf(p.scopes.map [
+                        val currentSize = targetTypeInterpretation.elements.size
+                        val minElements = minNewElements + currentSize
+                        val maxElements = if (maxNewElements < 0) {
+                                -1
+                        } else {
+                                maxNewElements + currentSize
+                        }
+                        new ScopeAssertion(minElements, maxElements, targetTypeInterpretation)
+                ])
+        }
+
+        override init(ThreadContext context) {
+                if (context.model != p) {
+                        throw new IllegalArgumentException(
+                                "Partial model must be passed to the constructor of BasicScopeGlobalConstraint")
+                }
+        }
+
+        override checkGlobalConstraint(ThreadContext context) {
+                assertions.forall[upperBoundSatisfied]
+        }
+
+        override getFitness(ThreadContext context) {
+                var double fitness = p.minNewElements
+                for (assertion : assertions) {
+                        if (!assertion.lowerBoundSatisfied) {
+                                fitness += 1
+                        }
+                }
+                fitness
+        }
+
+        override satisifiesHardObjective(Double fitness) {
+                fitness <= 0.01
+        }
+
+        override BasicScopeGlobalConstraint createNew() {
+                this
+        }
+
+        override getName() {
+                class.name
+        }
+
+        override getComparator() {
+                Comparators.LOWER_IS_BETTER
+        }
+
+        override getLevel() {
+                2
+        }
+
+        override isHardObjective() {
+                true
+        }
+
+        override setComparator(Comparator<Double> comparator) {
+                throw new UnsupportedOperationException
+        }
+
+        override setLevel(int level) {
+                throw new UnsupportedOperationException
+        }
+
+        @FinalFieldsConstructor
+        private static class ScopeAssertion {
+                val int lowerBound
+                val int upperBound
+                val PartialTypeInterpratation typeDefinitions
+
+                private def getCount() {
+                        typeDefinitions.elements.size
+                }
+
+                private def isLowerBoundSatisfied() {
+                        count >= lowerBound
+                }
+
+                private def isUpperBoundSatisfied() {
+                        upperBound < 0 || count <= upperBound
+                }
+        }
+}