diff options
author | 2019-08-02 01:26:19 +0200 | |
---|---|---|
committer | 2019-08-02 01:26:19 +0200 | |
commit | 07664df29b4aa491597ca76c31556a746ae95635 (patch) | |
tree | 62ea2a16b97ab3e806f0ac00f5bf0f6c16e49d4e /Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra | |
parent | Fix enum literal support for FAM (diff) | |
download | VIATRA-Generator-07664df29b4aa491597ca76c31556a746ae95635.tar.gz VIATRA-Generator-07664df29b4aa491597ca76c31556a746ae95635.tar.zst VIATRA-Generator-07664df29b4aa491597ca76c31556a746ae95635.zip |
Handle floating point rounding errors in Cbc
Diffstat (limited to 'Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra')
-rw-r--r-- | Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/CbcPolyhedronSolver.xtend | 35 |
1 files changed, 28 insertions, 7 deletions
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 index 4bd46fbf..c772aebc 100644 --- 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 | |||
@@ -26,6 +26,8 @@ class CbcPolyhedronSolver implements PolyhedronSolver { | |||
26 | } | 26 | } |
27 | 27 | ||
28 | class CbcSaturationOperator extends AbstractPolyhedronSaturationOperator { | 28 | class CbcSaturationOperator extends AbstractPolyhedronSaturationOperator { |
29 | static val EPSILON = 1e-6 | ||
30 | |||
29 | val boolean lpRelaxation | 31 | val boolean lpRelaxation |
30 | val double timeoutSeconds | 32 | val double timeoutSeconds |
31 | val boolean silent | 33 | val boolean silent |
@@ -139,12 +141,21 @@ class CbcSaturationOperator extends AbstractPolyhedronSaturationOperator { | |||
139 | entries, rowLowerBounds, rowUpperBounds, objective, lpRelaxation, timeoutSeconds, silent) | 141 | entries, rowLowerBounds, rowUpperBounds, objective, lpRelaxation, timeoutSeconds, silent) |
140 | switch (minimizationResult) { | 142 | switch (minimizationResult) { |
141 | CbcResult.SolutionBounded: { | 143 | CbcResult.SolutionBounded: { |
142 | val value = Math.floor(minimizationResult.value) | 144 | val doubleValue = minimizationResult.value |
143 | expressionToSaturate.lowerBound = value as int | 145 | val roundedValue = Math.floor(doubleValue) |
144 | setBound(expressionToSaturate, constraints, value, columnLowerBounds, rowLowerBounds) | 146 | val intValue = roundedValue as int |
147 | val oldBound = expressionToSaturate.lowerBound | ||
148 | if (oldBound === null || intValue > oldBound) { | ||
149 | expressionToSaturate.lowerBound = intValue | ||
150 | setBound(expressionToSaturate, constraints, roundedValue, columnLowerBounds, rowLowerBounds) | ||
151 | } else if (oldBound - doubleValue > EPSILON) { | ||
152 | throw new IllegalStateException("Unexpected decrease of lower bound by " + (oldBound - doubleValue)) | ||
153 | } | ||
145 | } | 154 | } |
146 | case CbcResult.SOLUTION_UNBOUNDED: { | 155 | case CbcResult.SOLUTION_UNBOUNDED: { |
147 | expressionToSaturate.lowerBound = null | 156 | if (expressionToSaturate.lowerBound !== null) { |
157 | throw new IllegalStateException("Finite lower bound became infinite") | ||
158 | } | ||
148 | setBound(expressionToSaturate, constraints, Double.NEGATIVE_INFINITY, columnLowerBounds, rowLowerBounds) | 159 | setBound(expressionToSaturate, constraints, Double.NEGATIVE_INFINITY, columnLowerBounds, rowLowerBounds) |
149 | } | 160 | } |
150 | case CbcResult.UNSAT: | 161 | case CbcResult.UNSAT: |
@@ -163,11 +174,21 @@ class CbcSaturationOperator extends AbstractPolyhedronSaturationOperator { | |||
163 | entries, rowLowerBounds, rowUpperBounds, objective, lpRelaxation, timeoutSeconds, silent) | 174 | entries, rowLowerBounds, rowUpperBounds, objective, lpRelaxation, timeoutSeconds, silent) |
164 | switch (maximizationResult) { | 175 | switch (maximizationResult) { |
165 | CbcResult.SolutionBounded: { | 176 | CbcResult.SolutionBounded: { |
166 | val value = Math.ceil(-maximizationResult.value) | 177 | val doubleValue = -maximizationResult.value |
167 | expressionToSaturate.upperBound = value as int | 178 | val roundedValue = Math.ceil(doubleValue) |
168 | setBound(expressionToSaturate, constraints, value, columnUpperBounds, rowUpperBounds) | 179 | val intValue = roundedValue as int |
180 | val oldBound = expressionToSaturate.upperBound | ||
181 | if (oldBound === null || intValue < oldBound) { | ||
182 | expressionToSaturate.upperBound = intValue | ||
183 | setBound(expressionToSaturate, constraints, roundedValue, columnUpperBounds, rowUpperBounds) | ||
184 | } else if (doubleValue - oldBound > EPSILON) { | ||
185 | throw new IllegalStateException("Unexpected increase of upper bound by " + (doubleValue - oldBound)) | ||
186 | } | ||
169 | } | 187 | } |
170 | case CbcResult.SOLUTION_UNBOUNDED: { | 188 | case CbcResult.SOLUTION_UNBOUNDED: { |
189 | if (expressionToSaturate.lowerBound !== null) { | ||
190 | throw new IllegalStateException("Finite upper bound became infinite") | ||
191 | } | ||
171 | expressionToSaturate.upperBound = null | 192 | expressionToSaturate.upperBound = null |
172 | setBound(expressionToSaturate, constraints, Double.POSITIVE_INFINITY, columnUpperBounds, rowUpperBounds) | 193 | setBound(expressionToSaturate, constraints, Double.POSITIVE_INFINITY, columnUpperBounds, rowUpperBounds) |
173 | } | 194 | } |