aboutsummaryrefslogtreecommitdiffstats
path: root/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/BasicScopeGlobalConstraint.xtend
blob: 67f447ed67b690e1a9332f28a4c1d774a59ba158 (plain) (blame)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
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
		}
	}
}