diff options
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 | 41 |
1 files changed, 27 insertions, 14 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 5c16f406..4ecebb62 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 | |||
@@ -65,6 +65,7 @@ import org.eclipse.viatra.query.runtime.emf.EMFScope | |||
65 | import org.eclipse.xtend.lib.annotations.Accessors | 65 | import org.eclipse.xtend.lib.annotations.Accessors |
66 | 66 | ||
67 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* | 67 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* |
68 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSInt | ||
68 | 69 | ||
69 | class Logic2AlloyLanguageMapper { | 70 | class Logic2AlloyLanguageMapper { |
70 | private val extension AlloyLanguageFactory factory = AlloyLanguageFactory.eINSTANCE | 71 | private val extension AlloyLanguageFactory factory = AlloyLanguageFactory.eINSTANCE |
@@ -311,22 +312,34 @@ class Logic2AlloyLanguageMapper { | |||
311 | it.number = typeMapper.getUndefinedSupertypeScope(config.typeScopes.maxNewElements,trace) | 312 | it.number = typeMapper.getUndefinedSupertypeScope(config.typeScopes.maxNewElements,trace) |
312 | it.exactly = (config.typeScopes.maxNewElements == config.typeScopes.minNewElements) | 313 | it.exactly = (config.typeScopes.maxNewElements == config.typeScopes.minNewElements) |
313 | ] | 314 | ] |
314 | if(config.typeScopes.maxNewIntegers == LogicSolverConfiguration::Unlimited) throw new UnsupportedOperationException( | 315 | if(config.typeScopes.maxNewIntegers == LogicSolverConfiguration::Unlimited) { |
315 | '''An integer scope have to be specified for Alloy!''') | 316 | val integersUsed = specification.eAllContents.filter(ALSInt) |
316 | it.typeScopes += createALSIntScope => [ | 317 | if(integersUsed.empty) { |
317 | if(config.typeScopes.knownIntegers.empty) { | 318 | // If no integer scope is defined, but the problem has no integers |
318 | number = Integer.SIZE-Integer.numberOfLeadingZeros(config.typeScopes.maxNewIntegers+1/2) | 319 | // => scope can be empty |
320 | it.typeScopes+= createALSIntScope => [ | ||
321 | it.number = 0 | ||
322 | ] | ||
319 | } else { | 323 | } else { |
320 | var scope = Math.max( | 324 | // If no integer scope is defined, and the problem has integers |
321 | Math.abs(config.typeScopes.knownIntegers.max), | 325 | // => error |
322 | Math.abs(config.typeScopes.knownIntegers.min)) | 326 | throw new UnsupportedOperationException('''An integer scope have to be specified for Alloy!''') |
323 | if(scope*2+1 < config.typeScopes.knownIntegers.size + config.typeScopes.maxNewIntegers) { | ||
324 | scope += ((config.typeScopes.knownIntegers.size + config.typeScopes.maxNewIntegers) - (scope*2))/2 | ||
325 | } | ||
326 | number = Integer.SIZE-Integer.numberOfLeadingZeros(scope) | ||
327 | } | 327 | } |
328 | 328 | } else { | |
329 | ] | 329 | it.typeScopes += createALSIntScope => [ |
330 | if(config.typeScopes.knownIntegers.empty) { | ||
331 | number = Integer.SIZE-Integer.numberOfLeadingZeros(config.typeScopes.maxNewIntegers+1/2) | ||
332 | } else { | ||
333 | var scope = Math.max( | ||
334 | Math.abs(config.typeScopes.knownIntegers.max), | ||
335 | Math.abs(config.typeScopes.knownIntegers.min)) | ||
336 | if(scope*2+1 < config.typeScopes.knownIntegers.size + config.typeScopes.maxNewIntegers) { | ||
337 | scope += ((config.typeScopes.knownIntegers.size + config.typeScopes.maxNewIntegers) - (scope*2))/2 | ||
338 | } | ||
339 | number = Integer.SIZE-Integer.numberOfLeadingZeros(scope) | ||
340 | } | ||
341 | ] | ||
342 | } | ||
330 | // for(definedScope : config.typeScopes.allDefinedScope) { | 343 | // for(definedScope : config.typeScopes.allDefinedScope) { |
331 | // it.typeScopes += createALSSigScope => [ | 344 | // it.typeScopes += createALSSigScope => [ |
332 | // it.type = definedScope.type.lookup(trace.type2ALSType) | 345 | // it.type = definedScope.type.lookup(trace.type2ALSType) |