aboutsummaryrefslogtreecommitdiffstats
path: root/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality
diff options
context:
space:
mode:
Diffstat (limited to 'Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality')
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/PolyhedronScopePropagator.xtend153
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/PolyhedronSolver.xtend115
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/ScopePropagator.xtend149
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/Z3PolyhedronSolver.xtend206
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 @@
1package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality
2
3import com.google.common.collect.ImmutableList
4import com.google.common.collect.ImmutableMap
5import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type
6import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialComplexTypeInterpretation
7import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation
8import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialPrimitiveInterpretation
9import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.Scope
10import java.util.ArrayDeque
11import java.util.HashMap
12import java.util.HashSet
13import java.util.Map
14import java.util.Set
15
16class 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 @@
1package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality
2
3import java.util.List
4import java.util.Map
5import org.eclipse.xtend.lib.annotations.Accessors
6import org.eclipse.xtend.lib.annotations.FinalFieldsConstructor
7
8interface PolyhedronSolver {
9 def PolyhedronSaturationOperator createSaturationOperator(Polyhedron polyhedron)
10}
11
12enum PolyhedronSaturationResult {
13 SATURATED,
14 EMPTY,
15 UNKNOWN
16}
17
18interface PolyhedronSaturationOperator extends AutoCloseable {
19 def Polyhedron getPolyhedron()
20
21 def PolyhedronSaturationResult saturate()
22}
23
24@FinalFieldsConstructor
25@Accessors
26class 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
72abstract class LinearBoundedExpression {
73 var Integer lowerBound
74 var Integer upperBound
75}
76
77@Accessors
78class 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
98class 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 @@
1package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality
2
3import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialComplexTypeInterpretation
4import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation
5import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialTypeInterpratation
6import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.Scope
7import java.util.HashMap
8import java.util.HashSet
9import java.util.Map
10import java.util.Set
11import org.eclipse.xtend.lib.annotations.Accessors
12
13enum ScopePropagatorStrategy {
14 BasicTypeHierarchy,
15 PolyhedralTypeHierarchy
16}
17
18class 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 @@
1package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality
2
3import com.microsoft.z3.ArithExpr
4import com.microsoft.z3.Context
5import com.microsoft.z3.Expr
6import com.microsoft.z3.IntNum
7import com.microsoft.z3.Optimize
8import com.microsoft.z3.Status
9import com.microsoft.z3.Symbol
10import java.util.Map
11import org.eclipse.xtend.lib.annotations.Accessors
12import org.eclipse.xtend.lib.annotations.FinalFieldsConstructor
13
14class 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
30class 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}
generated by cgit v1.2.3-54-g00ecf (git 2.45.2) at 2024-07-03 18:22:13 +0000