blob: 9c6cb82e34d22a9ed6ecb595690a335d09f653d0 (
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
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
|
package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality
import java.util.List
import java.util.Map
import org.eclipse.xtend.lib.annotations.Accessors
import org.eclipse.xtend.lib.annotations.FinalFieldsConstructor
interface PolyhedronSolver {
def PolyhedronSaturationOperator createSaturationOperator(Polyhedron polyhedron)
}
enum PolyhedronSaturationResult {
SATURATED,
EMPTY,
UNKNOWN
}
interface PolyhedronSaturationOperator extends AutoCloseable {
def Polyhedron getPolyhedron()
def PolyhedronSaturationResult saturate()
}
@FinalFieldsConstructor
@Accessors
class Polyhedron {
/**
* The list of dimensions (variables) for this polyhedron.
*
* This list must not be modified after the polyhedron was created.
* However, lower and upper bounds of the dimensions may be changed.
*
* Names of dimensions in this list are assumed to be unique.
*/
val List<Dimension> dimensions
/**
* The list of constraints defining this polyhedron.
*
* The list and its elements may be freely modified.
*/
val List<LinearConstraint> constraints
/**
* The list of constraints that should be saturated (tightened)
* when a {@link PolyhedronSaturationOperator} is invoked.
*
* This list may be freely modified.
*
* Place all dimensions and constraints here to saturate all the bounds.
*/
val List<LinearBoundedExpression> expressionsToSaturate
override toString() '''
Dimensions:
«FOR dimension : dimensions»
«dimension»
«ENDFOR»
Constraints:
«FOR constraint : constraints»
«constraint»
«ENDFOR»
'''
}
@Accessors
abstract class LinearBoundedExpression {
var Integer lowerBound
var Integer upperBound
def void tightenLowerBound(Integer tighterBound) {
if (lowerBound === null || (tighterBound !== null && lowerBound < tighterBound)) {
lowerBound = tighterBound
}
}
def void tightenUpperBound(Integer tighterBound) {
if (upperBound === null || (tighterBound !== null && upperBound > tighterBound)) {
upperBound = tighterBound
}
}
}
@Accessors
class Dimension extends LinearBoundedExpression {
val String name
@FinalFieldsConstructor
new() {
}
new(String name, Integer lowerBound, Integer upperBound) {
this(name)
this.lowerBound = lowerBound
this.upperBound = upperBound
}
override toString() {
'''«IF lowerBound !== null»«lowerBound» <= «ENDIF»«name»«IF upperBound !== null» <= «upperBound»«ENDIF»'''
}
}
@Accessors
class LinearConstraint extends LinearBoundedExpression {
val Map<Dimension, Integer> coefficients
@FinalFieldsConstructor
new() {
}
new(Map<Dimension, Integer> coefficients, Integer lowerBound, Integer upperBound) {
this(coefficients)
this.lowerBound = lowerBound
this.upperBound = upperBound
}
override toString() {
'''«IF lowerBound !== null»«lowerBound» <= «ENDIF»«FOR pair : coefficients.entrySet SEPARATOR " + "»«IF pair.value != 1»«pair.value» * «ENDIF»«pair.key.name»«ENDFOR»«IF upperBound !== null» <= «upperBound»«ENDIF»'''
}
}
|
