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
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
|
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.Data
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»
'''
def createSignature() {
val size = dimensions.size + constraints.size
val lowerBounds = newArrayOfSize(size)
val upperBounds = newArrayOfSize(size)
var int i = 0
for (dimension : dimensions) {
lowerBounds.set(i, dimension.lowerBound)
upperBounds.set(i, dimension.upperBound)
i++
}
for (constraint : constraints) {
lowerBounds.set(i, constraint.lowerBound)
upperBounds.set(i, constraint.upperBound)
i++
}
new PolyhedronSignature.Bounds(lowerBounds, upperBounds)
}
def applySignature(PolyhedronSignature.Bounds signature) {
val lowerBounds = signature.lowerBounds
val upperBounds = signature.upperBounds
var int i = 0
for (dimension : dimensions) {
dimension.lowerBound = lowerBounds.get(i)
dimension.upperBound = upperBounds.get(i)
i++
}
for (constraint : constraints) {
constraint.lowerBound = lowerBounds.get(i)
constraint.upperBound = upperBounds.get(i)
i++
}
}
}
abstract class PolyhedronSignature {
public static val EMPTY = new PolyhedronSignature {
override toString() {
"PolyhedronSignature.EMPTY"
}
}
private new() {
}
@Data
static class Bounds extends PolyhedronSignature {
val Integer[] lowerBounds
val Integer[] upperBounds
}
}
@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
}
}
def void assertEqualsTo(int bound) {
tightenLowerBound(bound)
tightenUpperBound(bound)
}
}
@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»'''
}
}
|
