diff options
author | 2017-08-16 15:19:47 +0200 | |
---|---|---|
committer | 2017-08-16 15:19:47 +0200 | |
commit | e0a3073dd0b3b78d1421cc200567618f99a8206c (patch) | |
tree | 2c7cfcfe55d35d9973fbc25acdf3705725bc4352 /Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper.xtend | |
parent | Added known primitives to the scope (diff) | |
download | VIATRA-Generator-e0a3073dd0b3b78d1421cc200567618f99a8206c.tar.gz VIATRA-Generator-e0a3073dd0b3b78d1421cc200567618f99a8206c.tar.zst VIATRA-Generator-e0a3073dd0b3b78d1421cc200567618f99a8206c.zip |
Alloy mapping of integer scopes
Diffstat (limited to 'Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper.xtend')
-rw-r--r-- | Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper.xtend | 8 |
1 files changed, 6 insertions, 2 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 65fdcfdf..e5c443f6 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 | |||
@@ -279,10 +279,14 @@ class Logic2AlloyLanguageMapper { | |||
279 | it.number = typeMapper.getUndefinedSupertypeScope(config.typeScopes.maxNewElements,trace) | 279 | it.number = typeMapper.getUndefinedSupertypeScope(config.typeScopes.maxNewElements,trace) |
280 | it.exactly = (config.typeScopes.maxNewElements == config.typeScopes.minNewElements) | 280 | it.exactly = (config.typeScopes.maxNewElements == config.typeScopes.minNewElements) |
281 | ] | 281 | ] |
282 | if(config.typeScopes.maxIntScope == 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 | number = Integer.SIZE-Integer.numberOfLeadingZeros(config.typeScopes.maxIntScope) | 285 | val knownIntegerMax = config.typeScopes.knownIntegers.max |
286 | val knownIntegerMin = config.typeScopes.knownIntegers.min | ||
287 | val needNewPlaces = Math.max(knownIntegerMax - knownIntegerMin - config.typeScopes.maxNewIntegers,0) | ||
288 | val maxAbsoluteValue = Math.max(Math.abs(knownIntegerMax)+needNewPlaces+1/2, Math.abs(knownIntegerMin)+needNewPlaces/2) | ||
289 | number = Integer.SIZE-Integer.numberOfLeadingZeros(maxAbsoluteValue) | ||
286 | ] | 290 | ] |
287 | // for(definedScope : config.typeScopes.allDefinedScope) { | 291 | // for(definedScope : config.typeScopes.allDefinedScope) { |
288 | // it.typeScopes += createALSSigScope => [ | 292 | // it.typeScopes += createALSSigScope => [ |