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
|
package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality
import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type
import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.ModelGenerationStatistics
import java.util.Collection
import java.util.Map
import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation
interface PolyhedronExtensionOperator {
def void extendPolyhedron(ExtendedLinearExpressionBuilderFactory factory)
}
class ExtendedPolyhedronScopePropagatorStrategy extends PolyhedronScopePropagatorStrategy {
val PolyhedronSolver solver
val Collection<PolyhedronExtensionOperator> extensionOperators
var Map<Type, LinearBoundedExpression> typeBounds
var Map<Map<Dimension, Integer>, LinearBoundedExpression> initialExpressionsCache
new(PolyhedronSolver solver, Collection<PolyhedronExtensionOperator> extensionOperators,
ModelGenerationStatistics statistics) {
super(statistics)
this.solver = solver
this.extensionOperators = extensionOperators
}
override setPolyhedron(Polyhedron polyhedron, Map<Type, LinearBoundedExpression> typeBounds,
Map<Map<Dimension, Integer>, LinearBoundedExpression> initialExpressionsCache) {
super.setPolyhedron(polyhedron, typeBounds, initialExpressionsCache)
this.typeBounds = typeBounds
this.initialExpressionsCache = initialExpressionsCache
}
override isRelevantRelation(Relation relation) {
true
}
override protected doSaturate() {
val builder = new ExtendedPolyhedronBuilder(polyhedron, typeBounds, initialExpressionsCache)
for (extensionOperator : extensionOperators) {
extensionOperator.extendPolyhedron(builder)
}
val extendedPolyhedron = builder.buildPolyhedron()
val saturationOperator = solver.createSaturationOperator(extendedPolyhedron)
val result = try {
saturationOperator.saturate()
} finally {
saturationOperator.close()
}
if (result == PolyhedronSaturationResult.EMPTY) {
// The partial model cannot be refined any more, we can't provide objective bounds.
for (pair : builder.saturationListeners) {
pair.value.boundsSaturated(null, null)
}
return false
}
for (pair : builder.saturationListeners) {
val expression = pair.key
pair.value.boundsSaturated(expression.lowerBound, expression.upperBound)
}
true
}
}
|
