diff options
Diffstat (limited to 'Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver')
2 files changed, 184 insertions, 2 deletions
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/ModelGenerationMethodProvider.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/ModelGenerationMethodProvider.xtend index 0040dbcd..0ceb5b2e 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/ModelGenerationMethodProvider.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/ModelGenerationMethodProvider.xtend | |||
@@ -4,10 +4,10 @@ import com.google.common.collect.ImmutableMap | |||
4 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel | 4 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel |
5 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem | 5 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem |
6 | import hu.bme.mit.inf.dslreasoner.viatra2logic.viatra2logicannotations.TransfomedViatraQuery | 6 | import hu.bme.mit.inf.dslreasoner.viatra2logic.viatra2logicannotations.TransfomedViatraQuery |
7 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.CbcPolyhedronSolver | ||
7 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.PolyhedronScopePropagator | 8 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.PolyhedronScopePropagator |
8 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.ScopePropagator | 9 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.ScopePropagator |
9 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.ScopePropagatorStrategy | 10 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.ScopePropagatorStrategy |
10 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.Z3PolyhedronSolver | ||
11 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.GeneratedPatterns | 11 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.GeneratedPatterns |
12 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.ModalPatternQueries | 12 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.ModalPatternQueries |
13 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.PatternProvider | 13 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.PatternProvider |
@@ -119,7 +119,7 @@ class ModelGenerationMethodProvider { | |||
119 | new ScopePropagator(emptySolution) | 119 | new ScopePropagator(emptySolution) |
120 | case PolyhedralTypeHierarchy: { | 120 | case PolyhedralTypeHierarchy: { |
121 | val types = queries.refineObjectQueries.keySet.map[newType].toSet | 121 | val types = queries.refineObjectQueries.keySet.map[newType].toSet |
122 | val solver = new Z3PolyhedronSolver | 122 | val solver = new CbcPolyhedronSolver |
123 | new PolyhedronScopePropagator(emptySolution, types, solver) | 123 | new PolyhedronScopePropagator(emptySolution, types, solver) |
124 | } | 124 | } |
125 | default: | 125 | default: |
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/CbcPolyhedronSolver.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/CbcPolyhedronSolver.xtend new file mode 100644 index 00000000..1f6d4e8f --- /dev/null +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/CbcPolyhedronSolver.xtend | |||
@@ -0,0 +1,182 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality | ||
2 | |||
3 | import com.google.common.collect.ImmutableMap | ||
4 | import hu.bme.mit.inf.dslreasoner.ilp.cbc.CbcResult | ||
5 | import hu.bme.mit.inf.dslreasoner.ilp.cbc.CbcSolver | ||
6 | import java.util.Map | ||
7 | import org.eclipse.xtend.lib.annotations.Accessors | ||
8 | import org.eclipse.xtend.lib.annotations.FinalFieldsConstructor | ||
9 | |||
10 | @FinalFieldsConstructor | ||
11 | class CbcPolyhedronSolver implements PolyhedronSolver { | ||
12 | val double timeoutSeconds | ||
13 | val boolean silent | ||
14 | |||
15 | new() { | ||
16 | this(10, true) | ||
17 | } | ||
18 | |||
19 | override createSaturationOperator(Polyhedron polyhedron) { | ||
20 | new CbcSaturationOperator(polyhedron, timeoutSeconds, silent) | ||
21 | } | ||
22 | } | ||
23 | |||
24 | class CbcSaturationOperator implements PolyhedronSaturationOperator { | ||
25 | @Accessors val Polyhedron polyhedron | ||
26 | val double timeoutSeconds | ||
27 | val boolean silent | ||
28 | val double[] columnLowerBounds | ||
29 | val double[] columnUpperBounds | ||
30 | val double[] objective | ||
31 | val Map<Dimension, Integer> dimensionsToIndicesMap | ||
32 | |||
33 | new(Polyhedron polyhedron, double timeoutSeconds, boolean silent) { | ||
34 | this.polyhedron = polyhedron | ||
35 | this.timeoutSeconds = timeoutSeconds | ||
36 | this.silent = silent | ||
37 | val numDimensions = polyhedron.dimensions.size | ||
38 | columnLowerBounds = newDoubleArrayOfSize(numDimensions) | ||
39 | columnUpperBounds = newDoubleArrayOfSize(numDimensions) | ||
40 | objective = newDoubleArrayOfSize(numDimensions) | ||
41 | dimensionsToIndicesMap = ImmutableMap.copyOf(polyhedron.dimensions.indexed.toMap([value], [key])) | ||
42 | } | ||
43 | |||
44 | override saturate() { | ||
45 | val numDimensions = polyhedron.dimensions.size | ||
46 | for (var int j = 0; j < numDimensions; j++) { | ||
47 | val dimension = polyhedron.dimensions.get(j) | ||
48 | columnLowerBounds.set(j, dimension.lowerBound.toDouble(Double.NEGATIVE_INFINITY)) | ||
49 | columnUpperBounds.set(j, dimension.upperBound.toDouble(Double.POSITIVE_INFINITY)) | ||
50 | } | ||
51 | val numConstraints = polyhedron.constraints.size | ||
52 | val rowStarts = newIntArrayOfSize(numConstraints + 1) | ||
53 | val rowLowerBounds = newDoubleArrayOfSize(numConstraints) | ||
54 | val rowUpperBounds = newDoubleArrayOfSize(numConstraints) | ||
55 | val numEntries = polyhedron.constraints.map[coefficients.size].reduce[a, b|a + b] ?: 0 | ||
56 | rowStarts.set(numConstraints, numEntries) | ||
57 | val columnIndices = newIntArrayOfSize(numEntries) | ||
58 | val entries = newDoubleArrayOfSize(numEntries) | ||
59 | var int index = 0 | ||
60 | for (var int i = 0; i < numConstraints; i++) { | ||
61 | rowStarts.set(i, index) | ||
62 | val constraint = polyhedron.constraints.get(i) | ||
63 | rowLowerBounds.set(i, constraint.lowerBound.toDouble(Double.NEGATIVE_INFINITY)) | ||
64 | rowUpperBounds.set(i, constraint.upperBound.toDouble(Double.POSITIVE_INFINITY)) | ||
65 | if (!dimensionsToIndicesMap.keySet.containsAll(constraint.coefficients.keySet)) { | ||
66 | throw new IllegalArgumentException("Constrains has unknown dimensions") | ||
67 | } | ||
68 | for (var int j = 0; j < numDimensions; j++) { | ||
69 | val dimension = polyhedron.dimensions.get(j) | ||
70 | val coefficient = constraint.coefficients.get(dimension) | ||
71 | if (coefficient !== null && coefficient != 0) { | ||
72 | columnIndices.set(index, j) | ||
73 | entries.set(index, coefficient) | ||
74 | index++ | ||
75 | } | ||
76 | } | ||
77 | } | ||
78 | if (index != numEntries) { | ||
79 | throw new AssertionError("Last entry does not equal the number of entries in the constraint matrix") | ||
80 | } | ||
81 | for (expressionToSaturate : polyhedron.expressionsToSaturate) { | ||
82 | for (var int j = 0; j < numDimensions; j++) { | ||
83 | objective.set(j, 0) | ||
84 | } | ||
85 | switch (expressionToSaturate) { | ||
86 | Dimension: { | ||
87 | val j = getIndex(expressionToSaturate) | ||
88 | objective.set(j, 1) | ||
89 | } | ||
90 | LinearConstraint: { | ||
91 | for (pair : expressionToSaturate.coefficients.entrySet) { | ||
92 | val j = getIndex(pair.key) | ||
93 | objective.set(j, pair.value) | ||
94 | } | ||
95 | } | ||
96 | default: | ||
97 | throw new IllegalArgumentException("Unknown expression: " + expressionToSaturate) | ||
98 | } | ||
99 | val minimizationResult = CbcSolver.solve(columnLowerBounds, columnUpperBounds, rowStarts, columnIndices, | ||
100 | entries, rowLowerBounds, rowUpperBounds, objective, timeoutSeconds, silent) | ||
101 | switch (minimizationResult) { | ||
102 | CbcResult.SolutionBounded: { | ||
103 | val value = Math.floor(minimizationResult.value) | ||
104 | expressionToSaturate.lowerBound = value as int | ||
105 | setBound(expressionToSaturate, value, columnLowerBounds, rowLowerBounds) | ||
106 | } | ||
107 | case CbcResult.SOLUTION_UNBOUNDED: { | ||
108 | expressionToSaturate.lowerBound = null | ||
109 | setBound(expressionToSaturate, Double.NEGATIVE_INFINITY, columnLowerBounds, rowLowerBounds) | ||
110 | } | ||
111 | case CbcResult.UNSAT: | ||
112 | return PolyhedronSaturationResult.EMPTY | ||
113 | case CbcResult.ABANDONED, | ||
114 | case CbcResult.TIMEOUT: | ||
115 | return PolyhedronSaturationResult.UNKNOWN | ||
116 | default: | ||
117 | throw new RuntimeException("Unknown CbcResult: " + minimizationResult) | ||
118 | } | ||
119 | for (var int j = 0; j < numDimensions; j++) { | ||
120 | val objectiveCoefficient = objective.get(j) | ||
121 | objective.set(j, -objectiveCoefficient) | ||
122 | } | ||
123 | val maximizationResult = CbcSolver.solve(columnLowerBounds, columnUpperBounds, rowStarts, columnIndices, | ||
124 | entries, rowLowerBounds, rowUpperBounds, objective, timeoutSeconds, silent) | ||
125 | switch (maximizationResult) { | ||
126 | CbcResult.SolutionBounded: { | ||
127 | val value = Math.ceil(-maximizationResult.value) | ||
128 | expressionToSaturate.upperBound = value as int | ||
129 | setBound(expressionToSaturate, value, columnUpperBounds, rowUpperBounds) | ||
130 | } | ||
131 | case CbcResult.SOLUTION_UNBOUNDED: { | ||
132 | expressionToSaturate.upperBound = null | ||
133 | setBound(expressionToSaturate, Double.POSITIVE_INFINITY, columnUpperBounds, rowUpperBounds) | ||
134 | } | ||
135 | case CbcResult.UNSAT: | ||
136 | throw new RuntimeException("Minimization was SAT, but maximization is UNSAT") | ||
137 | case CbcResult.ABANDONED, | ||
138 | case CbcResult.TIMEOUT: | ||
139 | return PolyhedronSaturationResult.UNKNOWN | ||
140 | default: | ||
141 | throw new RuntimeException("Unknown CbcResult: " + maximizationResult) | ||
142 | } | ||
143 | } | ||
144 | PolyhedronSaturationResult.SATURATED | ||
145 | } | ||
146 | |||
147 | private def toDouble(Integer nullableInt, double defaultValue) { | ||
148 | if (nullableInt === null) { | ||
149 | defaultValue | ||
150 | } else { | ||
151 | nullableInt.doubleValue | ||
152 | } | ||
153 | } | ||
154 | |||
155 | private def int getIndex(Dimension dimension) { | ||
156 | val index = dimensionsToIndicesMap.get(dimension) | ||
157 | if (index === null) { | ||
158 | throw new IllegalArgumentException("Unknown dimension: " + dimension) | ||
159 | } | ||
160 | index | ||
161 | } | ||
162 | |||
163 | private def void setBound(LinearBoundedExpression expression, double bound, double[] columnBounds, | ||
164 | double[] rowBounds) { | ||
165 | switch (expression) { | ||
166 | Dimension: { | ||
167 | val j = getIndex(expression) | ||
168 | columnBounds.set(j, bound) | ||
169 | } | ||
170 | LinearConstraint: { | ||
171 | val i = polyhedron.constraints.indexOf(expression) | ||
172 | if (i >= 0) { | ||
173 | rowBounds.set(i, bound) | ||
174 | } | ||
175 | } | ||
176 | } | ||
177 | } | ||
178 | |||
179 | override close() throws Exception { | ||
180 | // Nothing to close | ||
181 | } | ||
182 | } | ||