diff options
Diffstat (limited to 'Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality')
4 files changed, 623 insertions, 0 deletions
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/PolyhedronScopePropagator.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/PolyhedronScopePropagator.xtend new file mode 100644 index 00000000..8f210ffb --- /dev/null +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/PolyhedronScopePropagator.xtend | |||
@@ -0,0 +1,153 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality | ||
2 | |||
3 | import com.google.common.collect.ImmutableList | ||
4 | import com.google.common.collect.ImmutableMap | ||
5 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type | ||
6 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialComplexTypeInterpretation | ||
7 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation | ||
8 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialPrimitiveInterpretation | ||
9 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.Scope | ||
10 | import java.util.ArrayDeque | ||
11 | import java.util.HashMap | ||
12 | import java.util.HashSet | ||
13 | import java.util.Map | ||
14 | import java.util.Set | ||
15 | |||
16 | class PolyhedronScopePropagator extends ScopePropagator { | ||
17 | val Map<Scope, LinearBoundedExpression> scopeBounds | ||
18 | val LinearConstraint topLevelBounds | ||
19 | val PolyhedronSaturationOperator operator | ||
20 | |||
21 | new(PartialInterpretation p, Set<? extends Type> possibleNewDynamicTypes, PolyhedronSolver solver) { | ||
22 | super(p) | ||
23 | val instanceCounts = possibleNewDynamicTypes.toInvertedMap[new Dimension(name, 0, null)] | ||
24 | val primitiveDimensions = new HashMap | ||
25 | val constraintsBuilder = ImmutableList.builder | ||
26 | val scopeBoundsBuilder = ImmutableMap.builder | ||
27 | // Dimensions for instantiable types were created according to the type analysis, | ||
28 | // but for any possible primitive types, we create them on demand, | ||
29 | // as there is no Type directly associated with a PartialPrimitiveInterpretation. | ||
30 | for (scope : p.scopes) { | ||
31 | switch (targetTypeInterpretation : scope.targetTypeInterpretation) { | ||
32 | PartialPrimitiveInterpretation: { | ||
33 | val dimension = primitiveDimensions.computeIfAbsent(targetTypeInterpretation) [ interpretation | | ||
34 | new Dimension(interpretation.eClass.name, 0, null) | ||
35 | ] | ||
36 | scopeBoundsBuilder.put(scope, dimension) | ||
37 | } | ||
38 | PartialComplexTypeInterpretation: { | ||
39 | val complexType = targetTypeInterpretation.interpretationOf | ||
40 | val dimensions = findSubtypeDimensions(complexType, instanceCounts) | ||
41 | switch (dimensions.size) { | ||
42 | case 0: | ||
43 | if (scope.minNewElements > 0) { | ||
44 | throw new IllegalArgumentException("Found scope for " + complexType.name + | ||
45 | ", but the type cannot be instantiated") | ||
46 | } | ||
47 | case 1: | ||
48 | scopeBoundsBuilder.put(scope, dimensions.head) | ||
49 | default: { | ||
50 | val constraint = new LinearConstraint(dimensions.toInvertedMap[1], null, null) | ||
51 | constraintsBuilder.add(constraint) | ||
52 | scopeBoundsBuilder.put(scope, constraint) | ||
53 | } | ||
54 | } | ||
55 | } | ||
56 | default: | ||
57 | throw new IllegalArgumentException("Unknown PartialTypeInterpretation: " + targetTypeInterpretation) | ||
58 | } | ||
59 | } | ||
60 | val allDimensions = ImmutableList.builder.addAll(instanceCounts.values).addAll(primitiveDimensions.values).build | ||
61 | scopeBounds = scopeBoundsBuilder.build | ||
62 | topLevelBounds = new LinearConstraint(allDimensions.toInvertedMap[1], null, null) | ||
63 | constraintsBuilder.add(topLevelBounds) | ||
64 | val expressionsToSaturate = ImmutableList.builder.addAll(scopeBounds.values).add(topLevelBounds).build | ||
65 | val polyhedron = new Polyhedron(allDimensions, constraintsBuilder.build, expressionsToSaturate) | ||
66 | operator = solver.createSaturationOperator(polyhedron) | ||
67 | } | ||
68 | |||
69 | private def findSubtypeDimensions(Type type, Map<Type, Dimension> instanceCounts) { | ||
70 | val subtypes = new HashSet | ||
71 | val dimensions = new HashSet | ||
72 | val stack = new ArrayDeque | ||
73 | stack.addLast(type) | ||
74 | while (!stack.empty) { | ||
75 | val subtype = stack.removeLast | ||
76 | if (subtypes.add(subtype)) { | ||
77 | val dimension = instanceCounts.get(subtype) | ||
78 | if (dimension !== null) { | ||
79 | dimensions.add(dimension) | ||
80 | } | ||
81 | stack.addAll(subtype.subtypes) | ||
82 | } | ||
83 | } | ||
84 | dimensions | ||
85 | } | ||
86 | |||
87 | override void propagateAllScopeConstraints() { | ||
88 | populatePolyhedronFromScope() | ||
89 | val result = operator.saturate() | ||
90 | if (result == PolyhedronSaturationResult.EMPTY) { | ||
91 | throw new IllegalStateException("Scope bounds cannot be satisfied") | ||
92 | } else { | ||
93 | populateScopesFromPolyhedron() | ||
94 | if (result != PolyhedronSaturationResult.SATURATED) { | ||
95 | super.propagateAllScopeConstraints() | ||
96 | } | ||
97 | } | ||
98 | } | ||
99 | |||
100 | private def populatePolyhedronFromScope() { | ||
101 | topLevelBounds.lowerBound = partialInterpretation.minNewElements | ||
102 | if (partialInterpretation.maxNewElements >= 0) { | ||
103 | topLevelBounds.upperBound = partialInterpretation.maxNewElements | ||
104 | } | ||
105 | for (pair : scopeBounds.entrySet) { | ||
106 | val scope = pair.key | ||
107 | val bounds = pair.value | ||
108 | bounds.lowerBound = scope.minNewElements | ||
109 | if (scope.maxNewElements >= 0) { | ||
110 | bounds.upperBound = scope.maxNewElements | ||
111 | } | ||
112 | } | ||
113 | } | ||
114 | |||
115 | private def populateScopesFromPolyhedron() { | ||
116 | checkFiniteBounds(topLevelBounds) | ||
117 | if (partialInterpretation.minNewElements > topLevelBounds.lowerBound) { | ||
118 | throw new IllegalArgumentException('''Lower bound of «topLevelBounds» smaller than top-level scope: «partialInterpretation.minNewElements»''') | ||
119 | } else if (partialInterpretation.minNewElements != topLevelBounds.lowerBound) { | ||
120 | partialInterpretation.minNewElements = topLevelBounds.lowerBound | ||
121 | } | ||
122 | if (partialInterpretation.maxNewElements >= 0 && | ||
123 | partialInterpretation.maxNewElements < topLevelBounds.upperBound) { | ||
124 | throw new IllegalArgumentException('''Upper bound of «topLevelBounds» larger than top-level scope: «partialInterpretation.maxNewElements»''') | ||
125 | } else if (partialInterpretation.maxNewElements != topLevelBounds.upperBound) { | ||
126 | partialInterpretation.maxNewElements = topLevelBounds.upperBound | ||
127 | } | ||
128 | for (pair : scopeBounds.entrySet) { | ||
129 | val scope = pair.key | ||
130 | val bounds = pair.value | ||
131 | checkFiniteBounds(bounds) | ||
132 | if (scope.minNewElements > bounds.lowerBound) { | ||
133 | throw new IllegalArgumentException('''Lower bound of «bounds» smaller than «scope.targetTypeInterpretation» scope: «scope.minNewElements»''') | ||
134 | } else if (scope.minNewElements != bounds.lowerBound) { | ||
135 | scope.minNewElements = bounds.lowerBound | ||
136 | } | ||
137 | if (scope.maxNewElements >= 0 && scope.maxNewElements < bounds.upperBound) { | ||
138 | throw new IllegalArgumentException('''Upper bound of «bounds» larger than «scope.targetTypeInterpretation» scope: «scope.maxNewElements»''') | ||
139 | } else if (scope.maxNewElements != bounds.upperBound) { | ||
140 | scope.maxNewElements = bounds.upperBound | ||
141 | } | ||
142 | } | ||
143 | } | ||
144 | |||
145 | private def checkFiniteBounds(LinearBoundedExpression bounds) { | ||
146 | if (bounds.lowerBound === null) { | ||
147 | throw new IllegalArgumentException("Infinite lower bound: " + bounds) | ||
148 | } | ||
149 | if (bounds.upperBound === null) { | ||
150 | throw new IllegalArgumentException("Infinite upper bound: " + bounds) | ||
151 | } | ||
152 | } | ||
153 | } | ||
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/PolyhedronSolver.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/PolyhedronSolver.xtend new file mode 100644 index 00000000..08bf25b9 --- /dev/null +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/PolyhedronSolver.xtend | |||
@@ -0,0 +1,115 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality | ||
2 | |||
3 | import java.util.List | ||
4 | import java.util.Map | ||
5 | import org.eclipse.xtend.lib.annotations.Accessors | ||
6 | import org.eclipse.xtend.lib.annotations.FinalFieldsConstructor | ||
7 | |||
8 | interface PolyhedronSolver { | ||
9 | def PolyhedronSaturationOperator createSaturationOperator(Polyhedron polyhedron) | ||
10 | } | ||
11 | |||
12 | enum PolyhedronSaturationResult { | ||
13 | SATURATED, | ||
14 | EMPTY, | ||
15 | UNKNOWN | ||
16 | } | ||
17 | |||
18 | interface PolyhedronSaturationOperator extends AutoCloseable { | ||
19 | def Polyhedron getPolyhedron() | ||
20 | |||
21 | def PolyhedronSaturationResult saturate() | ||
22 | } | ||
23 | |||
24 | @FinalFieldsConstructor | ||
25 | @Accessors | ||
26 | class Polyhedron { | ||
27 | /** | ||
28 | * The list of dimensions (variables) for this polyhedron. | ||
29 | * | ||
30 | * This list must not be modified after the polyhedron was created. | ||
31 | * However, lower and upper bounds of the dimensions may be changed. | ||
32 | * | ||
33 | * Names of dimensions in this list are assumed to be unique. | ||
34 | */ | ||
35 | val List<Dimension> dimensions | ||
36 | |||
37 | /** | ||
38 | * The list of constraints defining this polyhedron. | ||
39 | * | ||
40 | * The list and its elements may be freely modified. | ||
41 | */ | ||
42 | val List<LinearConstraint> constraints | ||
43 | |||
44 | /** | ||
45 | * The list of constraints that should be saturated (tightened) | ||
46 | * when a {@link PolyhedronSaturationOperator} is invoked. | ||
47 | * | ||
48 | * This list may be freely modified. | ||
49 | * | ||
50 | * Place all dimensions and constraints here to saturate all the bounds. | ||
51 | */ | ||
52 | val List<LinearBoundedExpression> expressionsToSaturate | ||
53 | |||
54 | override toString() ''' | ||
55 | Dimensions: | ||
56 | «FOR dimension : dimensions» | ||
57 | «dimension» | ||
58 | «ENDFOR» | ||
59 | Constraints: | ||
60 | «FOR constraint : constraints» | ||
61 | «constraint» | ||
62 | «ENDFOR» | ||
63 | ««« Saturate: | ||
64 | ««« «FOR expression : expressionsToSaturate» | ||
65 | ««« «IF expression instanceof Dimension»dimension«ELSEIF expression instanceof LinearConstraint»constraint«ELSE»unknown«ENDIF» «expression» | ||
66 | ««« «ENDFOR» | ||
67 | ''' | ||
68 | |||
69 | } | ||
70 | |||
71 | @Accessors | ||
72 | abstract class LinearBoundedExpression { | ||
73 | var Integer lowerBound | ||
74 | var Integer upperBound | ||
75 | } | ||
76 | |||
77 | @Accessors | ||
78 | class Dimension extends LinearBoundedExpression { | ||
79 | val String name | ||
80 | |||
81 | @FinalFieldsConstructor | ||
82 | new() { | ||
83 | } | ||
84 | |||
85 | new(String name, Integer lowerBound, Integer upperBound) { | ||
86 | this(name) | ||
87 | this.lowerBound = lowerBound | ||
88 | this.upperBound = upperBound | ||
89 | } | ||
90 | |||
91 | override toString() { | ||
92 | '''«IF lowerBound !== null»«lowerBound» <= «ENDIF»«name»«IF upperBound !== null» <= «upperBound»«ENDIF»''' | ||
93 | } | ||
94 | |||
95 | } | ||
96 | |||
97 | @Accessors | ||
98 | class LinearConstraint extends LinearBoundedExpression { | ||
99 | val Map<Dimension, Integer> coefficients | ||
100 | |||
101 | @FinalFieldsConstructor | ||
102 | new() { | ||
103 | } | ||
104 | |||
105 | new(Map<Dimension, Integer> coefficients, Integer lowerBound, Integer upperBound) { | ||
106 | this(coefficients) | ||
107 | this.lowerBound = lowerBound | ||
108 | this.upperBound = upperBound | ||
109 | } | ||
110 | |||
111 | override toString() { | ||
112 | '''«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»''' | ||
113 | } | ||
114 | |||
115 | } | ||
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/ScopePropagator.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/ScopePropagator.xtend new file mode 100644 index 00000000..c8fb3409 --- /dev/null +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/ScopePropagator.xtend | |||
@@ -0,0 +1,149 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality | ||
2 | |||
3 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialComplexTypeInterpretation | ||
4 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation | ||
5 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialTypeInterpratation | ||
6 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.Scope | ||
7 | import java.util.HashMap | ||
8 | import java.util.HashSet | ||
9 | import java.util.Map | ||
10 | import java.util.Set | ||
11 | import org.eclipse.xtend.lib.annotations.Accessors | ||
12 | |||
13 | enum ScopePropagatorStrategy { | ||
14 | BasicTypeHierarchy, | ||
15 | PolyhedralTypeHierarchy | ||
16 | } | ||
17 | |||
18 | class ScopePropagator { | ||
19 | @Accessors(PROTECTED_GETTER) PartialInterpretation partialInterpretation | ||
20 | Map<PartialTypeInterpratation, Scope> type2Scope | ||
21 | |||
22 | val Map<Scope, Set<Scope>> superScopes | ||
23 | val Map<Scope, Set<Scope>> subScopes | ||
24 | |||
25 | new(PartialInterpretation p) { | ||
26 | partialInterpretation = p | ||
27 | type2Scope = new HashMap | ||
28 | for (scope : p.scopes) { | ||
29 | type2Scope.put(scope.targetTypeInterpretation, scope) | ||
30 | } | ||
31 | |||
32 | superScopes = new HashMap | ||
33 | subScopes = new HashMap | ||
34 | for (scope : p.scopes) { | ||
35 | superScopes.put(scope, new HashSet) | ||
36 | subScopes.put(scope, new HashSet) | ||
37 | } | ||
38 | |||
39 | for (scope : p.scopes) { | ||
40 | val target = scope.targetTypeInterpretation | ||
41 | if (target instanceof PartialComplexTypeInterpretation) { | ||
42 | val supertypeInterpretations = target.supertypeInterpretation | ||
43 | for (supertypeInterpretation : supertypeInterpretations) { | ||
44 | val supertypeScope = type2Scope.get(supertypeInterpretation) | ||
45 | superScopes.get(scope).add(supertypeScope) | ||
46 | subScopes.get(supertypeScope).add(scope) | ||
47 | } | ||
48 | } | ||
49 | } | ||
50 | } | ||
51 | |||
52 | def propagateAllScopeConstraints() { | ||
53 | var boolean hadChanged | ||
54 | do { | ||
55 | hadChanged = false | ||
56 | for (superScopeEntry : superScopes.entrySet) { | ||
57 | val sub = superScopeEntry.key | ||
58 | hadChanged = propagateLowerLimitUp(sub, partialInterpretation) || hadChanged | ||
59 | hadChanged = propagateUpperLimitDown(sub, partialInterpretation) || hadChanged | ||
60 | for (sup : superScopeEntry.value) { | ||
61 | hadChanged = propagateLowerLimitUp(sub, sup) || hadChanged | ||
62 | hadChanged = propagateUpperLimitDown(sub, sup) || hadChanged | ||
63 | } | ||
64 | } | ||
65 | } while (hadChanged) | ||
66 | } | ||
67 | |||
68 | def propagateAdditionToType(PartialTypeInterpratation t) { | ||
69 | // println('''Adding to «(t as PartialComplexTypeInterpretation).interpretationOf.name»''') | ||
70 | val targetScope = type2Scope.get(t) | ||
71 | targetScope.removeOne | ||
72 | val sups = superScopes.get(targetScope) | ||
73 | sups.forEach[removeOne] | ||
74 | if (this.partialInterpretation.minNewElements > 0) { | ||
75 | this.partialInterpretation.minNewElements = this.partialInterpretation.minNewElements - 1 | ||
76 | } | ||
77 | if (this.partialInterpretation.maxNewElements > 0) { | ||
78 | this.partialInterpretation.maxNewElements = this.partialInterpretation.maxNewElements - 1 | ||
79 | } else if (this.partialInterpretation.maxNewElements === 0) { | ||
80 | throw new IllegalArgumentException('''Inconsistent object creation: lower node limit is 0!''') | ||
81 | } | ||
82 | propagateAllScopeConstraints | ||
83 | |||
84 | // println('''Target Scope: «targetScope.minNewElements» - «targetScope.maxNewElements»''') | ||
85 | // println(''' «this.partialInterpretation.minNewElements» - «this.partialInterpretation.maxNewElements»''') | ||
86 | // this.partialInterpretation.scopes.forEach[println(''' «(it.targetTypeInterpretation as PartialComplexTypeInterpretation).interpretationOf.name»: «it.minNewElements»-«it.maxNewElements»''')] | ||
87 | // println('''All constraints are propagated upon increasing «(t as PartialComplexTypeInterpretation).interpretationOf.name»''') | ||
88 | } | ||
89 | |||
90 | private def propagateLowerLimitUp(Scope subScope, Scope superScope) { | ||
91 | if (subScope.minNewElements > superScope.minNewElements) { | ||
92 | superScope.minNewElements = subScope.minNewElements | ||
93 | return true | ||
94 | } else { | ||
95 | return false | ||
96 | } | ||
97 | } | ||
98 | |||
99 | private def propagateUpperLimitDown(Scope subScope, Scope superScope) { | ||
100 | if (superScope.maxNewElements >= 0 && | ||
101 | (superScope.maxNewElements < subScope.maxNewElements || subScope.maxNewElements < 0)) { | ||
102 | // println(''' | ||
103 | // «(subScope.targetTypeInterpretation as PartialComplexTypeInterpretation).interpretationOf.name» -> «(superScope.targetTypeInterpretation as PartialComplexTypeInterpretation).interpretationOf.name» | ||
104 | // subScope.maxNewElements «subScope.maxNewElements» = superScope.maxNewElements «superScope.maxNewElements» | ||
105 | // ''') | ||
106 | subScope.maxNewElements = superScope.maxNewElements | ||
107 | return true | ||
108 | } else { | ||
109 | return false | ||
110 | } | ||
111 | } | ||
112 | |||
113 | private def propagateLowerLimitUp(Scope subScope, PartialInterpretation p) { | ||
114 | if (subScope.minNewElements > p.minNewElements) { | ||
115 | // println(''' | ||
116 | // «(subScope.targetTypeInterpretation as PartialComplexTypeInterpretation).interpretationOf.name» -> nodes | ||
117 | // p.minNewElements «p.minNewElements» = subScope.minNewElements «subScope.minNewElements» | ||
118 | // ''') | ||
119 | p.minNewElements = subScope.minNewElements | ||
120 | return true | ||
121 | } else { | ||
122 | return false | ||
123 | } | ||
124 | } | ||
125 | |||
126 | private def propagateUpperLimitDown(Scope subScope, PartialInterpretation p) { | ||
127 | if (p.maxNewElements >= 0 && (p.maxNewElements < subScope.maxNewElements || subScope.maxNewElements < 0)) { | ||
128 | // println(''' | ||
129 | // «(subScope.targetTypeInterpretation as PartialComplexTypeInterpretation).interpretationOf.name» -> nodes | ||
130 | // subScope.maxNewElements «subScope.maxNewElements» = p.maxNewElements «p.maxNewElements» | ||
131 | // ''') | ||
132 | subScope.maxNewElements = p.maxNewElements | ||
133 | return true | ||
134 | } else { | ||
135 | return false | ||
136 | } | ||
137 | } | ||
138 | |||
139 | private def removeOne(Scope scope) { | ||
140 | if (scope.maxNewElements === 0) { | ||
141 | throw new IllegalArgumentException('''Inconsistent object creation: «scope.targetTypeInterpretation»''') | ||
142 | } else if (scope.maxNewElements > 0) { | ||
143 | scope.maxNewElements = scope.maxNewElements - 1 | ||
144 | } | ||
145 | if (scope.minNewElements > 0) { | ||
146 | scope.minNewElements = scope.minNewElements - 1 | ||
147 | } | ||
148 | } | ||
149 | } | ||
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/Z3PolyhedronSolver.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/Z3PolyhedronSolver.xtend new file mode 100644 index 00000000..f1a84f2d --- /dev/null +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/Z3PolyhedronSolver.xtend | |||
@@ -0,0 +1,206 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality | ||
2 | |||
3 | import com.microsoft.z3.ArithExpr | ||
4 | import com.microsoft.z3.Context | ||
5 | import com.microsoft.z3.Expr | ||
6 | import com.microsoft.z3.IntNum | ||
7 | import com.microsoft.z3.Optimize | ||
8 | import com.microsoft.z3.Status | ||
9 | import com.microsoft.z3.Symbol | ||
10 | import java.util.Map | ||
11 | import org.eclipse.xtend.lib.annotations.Accessors | ||
12 | import org.eclipse.xtend.lib.annotations.FinalFieldsConstructor | ||
13 | |||
14 | class Z3PolyhedronSolver implements PolyhedronSolver { | ||
15 | val boolean lpRelaxation | ||
16 | |||
17 | @FinalFieldsConstructor | ||
18 | new() { | ||
19 | } | ||
20 | |||
21 | new() { | ||
22 | this(true) | ||
23 | } | ||
24 | |||
25 | override createSaturationOperator(Polyhedron polyhedron) { | ||
26 | new Z3SaturationOperator(polyhedron, lpRelaxation) | ||
27 | } | ||
28 | } | ||
29 | |||
30 | class Z3SaturationOperator implements PolyhedronSaturationOperator { | ||
31 | static val INFINITY_SYMBOL_NAME = "oo" | ||
32 | static val MULT_SYMBOL_NAME = "*" | ||
33 | |||
34 | extension val Context context | ||
35 | val Symbol infinitySymbol | ||
36 | val Symbol multSymbol | ||
37 | @Accessors val Polyhedron polyhedron | ||
38 | val Map<Dimension, ArithExpr> variables | ||
39 | |||
40 | new(Polyhedron polyhedron, boolean lpRelaxation) { | ||
41 | context = new Context | ||
42 | infinitySymbol = context.mkSymbol(INFINITY_SYMBOL_NAME) | ||
43 | multSymbol = context.mkSymbol(MULT_SYMBOL_NAME) | ||
44 | this.polyhedron = polyhedron | ||
45 | variables = polyhedron.dimensions.toInvertedMap [ dimension | | ||
46 | val name = dimension.name | ||
47 | if (lpRelaxation) { | ||
48 | mkRealConst(name) | ||
49 | } else { | ||
50 | mkIntConst(name) | ||
51 | } | ||
52 | ] | ||
53 | } | ||
54 | |||
55 | override saturate() { | ||
56 | val status = doSaturate() | ||
57 | convertStatusToSaturationResult(status) | ||
58 | } | ||
59 | |||
60 | private def convertStatusToSaturationResult(Status status) { | ||
61 | switch (status) { | ||
62 | case SATISFIABLE: | ||
63 | PolyhedronSaturationResult.SATURATED | ||
64 | case UNSATISFIABLE: | ||
65 | PolyhedronSaturationResult.EMPTY | ||
66 | case UNKNOWN: | ||
67 | PolyhedronSaturationResult.UNKNOWN | ||
68 | default: | ||
69 | throw new IllegalArgumentException("Unknown Status: " + status) | ||
70 | } | ||
71 | } | ||
72 | |||
73 | private def doSaturate() { | ||
74 | for (expressionToSaturate : polyhedron.expressionsToSaturate) { | ||
75 | val expr = expressionToSaturate.toExpr | ||
76 | val lowerResult = saturateLowerBound(expr, expressionToSaturate) | ||
77 | if (lowerResult != Status.SATISFIABLE) { | ||
78 | return lowerResult | ||
79 | } | ||
80 | val upperResult = saturateUpperBound(expr, expressionToSaturate) | ||
81 | if (upperResult != Status.SATISFIABLE) { | ||
82 | return upperResult | ||
83 | } | ||
84 | } | ||
85 | Status.SATISFIABLE | ||
86 | } | ||
87 | |||
88 | private def saturateLowerBound(ArithExpr expr, LinearBoundedExpression expressionToSaturate) { | ||
89 | val optimize = prepareOptimize | ||
90 | val handle = optimize.MkMinimize(expr) | ||
91 | val status = optimize.Check() | ||
92 | if (status == Status.SATISFIABLE) { | ||
93 | val value = switch (resultExpr : handle.lower) { | ||
94 | IntNum: | ||
95 | resultExpr.getInt() | ||
96 | default: | ||
97 | if (isNegativeInfinity(resultExpr)) { | ||
98 | null | ||
99 | } else { | ||
100 | throw new IllegalArgumentException("Integer result expected, got: " + resultExpr) | ||
101 | } | ||
102 | } | ||
103 | expressionToSaturate.lowerBound = value | ||
104 | } | ||
105 | status | ||
106 | } | ||
107 | |||
108 | private def saturateUpperBound(ArithExpr expr, LinearBoundedExpression expressionToSaturate) { | ||
109 | val optimize = prepareOptimize | ||
110 | val handle = optimize.MkMaximize(expr) | ||
111 | val status = optimize.Check() | ||
112 | if (status == Status.SATISFIABLE) { | ||
113 | val value = switch (resultExpr : handle.upper) { | ||
114 | IntNum: | ||
115 | resultExpr.getInt() | ||
116 | default: | ||
117 | if (isPositiveInfinity(resultExpr)) { | ||
118 | null | ||
119 | } else { | ||
120 | throw new IllegalArgumentException("Integer result expected, got: " + resultExpr) | ||
121 | } | ||
122 | } | ||
123 | expressionToSaturate.upperBound = value | ||
124 | } | ||
125 | status | ||
126 | } | ||
127 | |||
128 | private def isPositiveInfinity(Expr expr) { | ||
129 | expr.app && expr.getFuncDecl.name == infinitySymbol | ||
130 | } | ||
131 | |||
132 | private def isNegativeInfinity(Expr expr) { | ||
133 | // Negative infinity is represented as (* (- 1) oo) | ||
134 | if (!expr.app || expr.getFuncDecl.name != multSymbol || expr.numArgs != 2) { | ||
135 | return false | ||
136 | } | ||
137 | isPositiveInfinity(expr.args.get(1)) | ||
138 | } | ||
139 | |||
140 | private def prepareOptimize() { | ||
141 | val optimize = mkOptimize() | ||
142 | assertConstraints(optimize) | ||
143 | optimize | ||
144 | } | ||
145 | |||
146 | private def assertConstraints(Optimize it) { | ||
147 | for (pair : variables.entrySet) { | ||
148 | assertBounds(pair.value, pair.key) | ||
149 | } | ||
150 | for (constraint : polyhedron.constraints) { | ||
151 | val expr = createLinearCombination(constraint.coefficients) | ||
152 | assertBounds(expr, constraint) | ||
153 | } | ||
154 | } | ||
155 | |||
156 | private def assertBounds(Optimize it, ArithExpr expression, LinearBoundedExpression bounds) { | ||
157 | val lowerBound = bounds.lowerBound | ||
158 | val upperBound = bounds.upperBound | ||
159 | if (lowerBound == upperBound) { | ||
160 | if (lowerBound === null) { | ||
161 | return | ||
162 | } | ||
163 | Assert(mkEq(expression, mkInt(lowerBound))) | ||
164 | } else { | ||
165 | if (lowerBound !== null) { | ||
166 | Assert(mkGe(expression, mkInt(lowerBound))) | ||
167 | } | ||
168 | if (upperBound !== null) { | ||
169 | Assert(mkLe(expression, mkInt(upperBound))) | ||
170 | } | ||
171 | } | ||
172 | } | ||
173 | |||
174 | private def toExpr(LinearBoundedExpression linearBoundedExpression) { | ||
175 | switch (linearBoundedExpression) { | ||
176 | Dimension: variables.get(linearBoundedExpression) | ||
177 | LinearConstraint: createLinearCombination(linearBoundedExpression.coefficients) | ||
178 | default: throw new IllegalArgumentException("Unknown linear bounded expression:" + linearBoundedExpression) | ||
179 | } | ||
180 | } | ||
181 | |||
182 | private def createLinearCombination(Map<Dimension, Integer> coefficients) { | ||
183 | val size = coefficients.size | ||
184 | val array = newArrayOfSize(size) | ||
185 | var int i = 0 | ||
186 | for (pair : coefficients.entrySet) { | ||
187 | val variable = variables.get(pair.key) | ||
188 | if (variable === null) { | ||
189 | throw new IllegalArgumentException("Unknown dimension: " + pair.key.name) | ||
190 | } | ||
191 | val coefficient = pair.value | ||
192 | val term = if (coefficient == 1) { | ||
193 | variable | ||
194 | } else { | ||
195 | mkMul(mkInt(coefficient), variable) | ||
196 | } | ||
197 | array.set(i, term) | ||
198 | i++ | ||
199 | } | ||
200 | mkAdd(array) | ||
201 | } | ||
202 | |||
203 | override close() throws Exception { | ||
204 | context.close() | ||
205 | } | ||
206 | } | ||