diff options
Diffstat (limited to 'Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy')
-rw-r--r-- | Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper.xtend | 17 |
1 files changed, 12 insertions, 5 deletions
diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper.xtend b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper.xtend index e5c443f6..ee2f49ed 100644 --- a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper.xtend +++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper.xtend | |||
@@ -282,11 +282,18 @@ class Logic2AlloyLanguageMapper { | |||
282 | if(config.typeScopes.maxNewIntegers == LogicSolverConfiguration::Unlimited) throw new UnsupportedOperationException( | 282 | if(config.typeScopes.maxNewIntegers == LogicSolverConfiguration::Unlimited) throw new UnsupportedOperationException( |
283 | '''An integer scope have to be specified for Alloy!''') | 283 | '''An integer scope have to be specified for Alloy!''') |
284 | it.typeScopes += createALSIntScope => [ | 284 | it.typeScopes += createALSIntScope => [ |
285 | val knownIntegerMax = config.typeScopes.knownIntegers.max | 285 | if(config.typeScopes.knownIntegers.empty) { |
286 | val knownIntegerMin = config.typeScopes.knownIntegers.min | 286 | number = Integer.SIZE-Integer.numberOfLeadingZeros(config.typeScopes.maxNewIntegers+1/2) |
287 | val needNewPlaces = Math.max(knownIntegerMax - knownIntegerMin - config.typeScopes.maxNewIntegers,0) | 287 | } else { |
288 | val maxAbsoluteValue = Math.max(Math.abs(knownIntegerMax)+needNewPlaces+1/2, Math.abs(knownIntegerMin)+needNewPlaces/2) | 288 | var scope = Math.max( |
289 | number = Integer.SIZE-Integer.numberOfLeadingZeros(maxAbsoluteValue) | 289 | Math.abs(config.typeScopes.knownIntegers.max), |
290 | Math.abs(config.typeScopes.knownIntegers.min)) | ||
291 | if(scope*2+1 < config.typeScopes.knownIntegers.size + config.typeScopes.maxNewIntegers) { | ||
292 | scope += ((config.typeScopes.knownIntegers.size + config.typeScopes.maxNewIntegers) - (scope*2))/2 | ||
293 | } | ||
294 | number = Integer.SIZE-Integer.numberOfLeadingZeros(scope) | ||
295 | } | ||
296 | |||
290 | ] | 297 | ] |
291 | // for(definedScope : config.typeScopes.allDefinedScope) { | 298 | // for(definedScope : config.typeScopes.allDefinedScope) { |
292 | // it.typeScopes += createALSSigScope => [ | 299 | // it.typeScopes += createALSSigScope => [ |