blob: 08bf25b930b8ab6d1a4cb4874081eae43575e614 (
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
|
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»
««« Saturate:
««« «FOR expression : expressionsToSaturate»
««« «IF expression instanceof Dimension»dimension«ELSEIF expression instanceof LinearConstraint»constraint«ELSE»unknown«ENDIF» «expression»
««« «ENDFOR»
'''
}
@Accessors
abstract class LinearBoundedExpression {
var Integer lowerBound
var Integer upperBound
}
@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»'''
}
}
|