From 05cc697cce50c87541cb619854be7ecbcfb586e9 Mon Sep 17 00:00:00 2001 From: OszkarSemerath Date: Wed, 16 Aug 2017 18:53:37 +0200 Subject: Adding transitive closure to the logic language --- .../reasoner/builder/Logic2AlloyLanguageMapper.xtend | 17 ++++++++++++----- 1 file changed, 12 insertions(+), 5 deletions(-) (limited to 'Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder') 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 { if(config.typeScopes.maxNewIntegers == LogicSolverConfiguration::Unlimited) throw new UnsupportedOperationException( '''An integer scope have to be specified for Alloy!''') it.typeScopes += createALSIntScope => [ - val knownIntegerMax = config.typeScopes.knownIntegers.max - val knownIntegerMin = config.typeScopes.knownIntegers.min - val needNewPlaces = Math.max(knownIntegerMax - knownIntegerMin - config.typeScopes.maxNewIntegers,0) - val maxAbsoluteValue = Math.max(Math.abs(knownIntegerMax)+needNewPlaces+1/2, Math.abs(knownIntegerMin)+needNewPlaces/2) - number = Integer.SIZE-Integer.numberOfLeadingZeros(maxAbsoluteValue) + if(config.typeScopes.knownIntegers.empty) { + number = Integer.SIZE-Integer.numberOfLeadingZeros(config.typeScopes.maxNewIntegers+1/2) + } else { + var scope = Math.max( + Math.abs(config.typeScopes.knownIntegers.max), + Math.abs(config.typeScopes.knownIntegers.min)) + if(scope*2+1 < config.typeScopes.knownIntegers.size + config.typeScopes.maxNewIntegers) { + scope += ((config.typeScopes.knownIntegers.size + config.typeScopes.maxNewIntegers) - (scope*2))/2 + } + number = Integer.SIZE-Integer.numberOfLeadingZeros(scope) + } + ] // for(definedScope : config.typeScopes.allDefinedScope) { // it.typeScopes += createALSSigScope => [ -- cgit v1.2.3-54-g00ecf