blob: 3165917a5e0cfa306f28455eca6e8779bf09537b (
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
|
package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality
import org.eclipse.xtend.lib.annotations.Data
import org.eclipse.xtend.lib.annotations.FinalFieldsConstructor
enum PolyhedralScopePropagatorConstraints {
TypeHierarchy,
Relational
}
enum PolyhedralScopePropagatorSolver {
Z3Real,
Z3Integer,
Cbc,
Clp
}
abstract class ScopePropagatorStrategy {
public static val None = new Simple("None")
public static val Basic = new Simple("Basic")
public static val BasicTypeHierarchy = new Simple("BasicTypeHierarchy")
private new() {
}
def boolean requiresUpperBoundIndexing()
static class Simple extends ScopePropagatorStrategy {
val String name
@FinalFieldsConstructor
private new() {
}
override requiresUpperBoundIndexing() {
false
}
override toString() {
name
}
}
@Data
static class Polyhedral extends ScopePropagatorStrategy {
public static val UNLIMITED_TIME = -1
val PolyhedralScopePropagatorConstraints constraints
val PolyhedralScopePropagatorSolver solver
val boolean updateHeuristic
val double timeoutSeconds
@FinalFieldsConstructor
new() {
}
new(PolyhedralScopePropagatorConstraints constraints, PolyhedralScopePropagatorSolver solver, boolean updateHeuristic) {
this(constraints, solver, updateHeuristic, UNLIMITED_TIME)
}
new(PolyhedralScopePropagatorConstraints constraints, PolyhedralScopePropagatorSolver solver) {
this(constraints, solver, true)
}
override requiresUpperBoundIndexing() {
constraints == PolyhedralScopePropagatorConstraints.Relational
}
}
}
|
