blob: f93dcd1852b4e27b08eed551c9234b4b1af1d177 (
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
|
package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality
import com.google.common.cache.Cache
import com.google.common.cache.CacheBuilder
import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation
import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type
import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.ModelGenerationStatistics
import java.util.Map
import org.eclipse.xtend.lib.annotations.Accessors
import org.eclipse.xtend.lib.annotations.FinalFieldsConstructor
@FinalFieldsConstructor
abstract class PolyhedronScopePropagatorStrategy {
val ModelGenerationStatistics statistics
@Accessors(PUBLIC_GETTER) var Polyhedron polyhedron
def void setPolyhedron(Polyhedron polyhedron, Map<Type, LinearBoundedExpression> typeBounds,
Map<Map<Dimension, Integer>, LinearBoundedExpression> initialExpressionsCache) {
if (this.polyhedron !== null) {
throw new IllegalStateException("polyhedron was already set")
}
this.polyhedron = polyhedron
initialize()
}
def boolean saturate() {
if (polyhedron === null) {
throw new IllegalStateException("polyhedron was not set")
}
doSaturate()
}
def boolean isRelevantRelation(Relation relation) {
false
}
protected def incrementScopePropagationSolverCount() {
statistics.incrementScopePropagationSolverCount()
}
protected def void initialize() {
}
protected def boolean doSaturate()
}
@FinalFieldsConstructor
class CachingSimplePolyhedronScopePropagatorStrategy extends PolyhedronScopePropagatorStrategy {
static val CACHE_SIZE = 10000
val PolyhedronSolver solver
val Cache<PolyhedronSignature, PolyhedronSignature> cache = CacheBuilder.newBuilder.maximumSize(CACHE_SIZE).build
var PolyhedronSaturationOperator operator
new(PolyhedronSolver solver, ModelGenerationStatistics statistics) {
super(statistics)
this.solver = solver
}
override protected initialize() {
operator = solver.createSaturationOperator(polyhedron)
}
override protected doSaturate() {
val signature = polyhedron.createSignature
val cachedSignature = cache.getIfPresent(signature)
switch (cachedSignature) {
case null: {
incrementScopePropagationSolverCount()
val result = operator.saturate()
if (result == PolyhedronSaturationResult.EMPTY) {
cache.put(signature, PolyhedronSignature.EMPTY)
false
} else {
val resultSignature = polyhedron.createSignature
cache.put(signature, resultSignature)
true
}
}
case PolyhedronSignature.EMPTY:
false
PolyhedronSignature.Bounds: {
polyhedron.applySignature(signature)
true
}
default:
throw new IllegalStateException("Unknown polyhedron signature: " + signature)
}
}
}
|
