From 79eb47516a27ebe1801fb8e9087f3ee1b4d123d1 Mon Sep 17 00:00:00 2001 From: Oszkar Semerath Date: Tue, 27 Aug 2019 18:45:22 +0200 Subject: Alloy RunCommand int scope fix candidate --- .../alloy/reasoner/builder/RunCommandMapper.xtend | 123 ++++++++++++++------- 1 file changed, 86 insertions(+), 37 deletions(-) diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/RunCommandMapper.xtend b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/RunCommandMapper.xtend index 3e96f7f4..cbd56abb 100644 --- a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/RunCommandMapper.xtend +++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/RunCommandMapper.xtend @@ -3,6 +3,8 @@ package hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.AlloySolverConfiguration import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSDocument import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSInt +import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSNumberLiteral +import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSRunCommand import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSTerm import hu.bme.mit.inf.dslreasoner.alloyLanguage.AlloyLanguageFactory import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration @@ -13,15 +15,15 @@ import java.util.List import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* class RunCommandMapper { - private val extension AlloyLanguageFactory factory = AlloyLanguageFactory.eINSTANCE - private val Logic2AlloyLanguageMapper_Support support = new Logic2AlloyLanguageMapper_Support; - private val Logic2AlloyLanguageMapper_TypeMapper typeMapper; + val extension AlloyLanguageFactory factory = AlloyLanguageFactory.eINSTANCE + val Logic2AlloyLanguageMapper_Support support = new Logic2AlloyLanguageMapper_Support; + val Logic2AlloyLanguageMapper_TypeMapper typeMapper; - public new(Logic2AlloyLanguageMapper_TypeMapper typeMapper) { + new(Logic2AlloyLanguageMapper_TypeMapper typeMapper) { this.typeMapper = typeMapper } - def public transformRunCommand(Logic2AlloyLanguageMapper mapper, ALSDocument specification, Logic2AlloyLanguageMapperTrace trace, AlloySolverConfiguration config) + def transformRunCommand(Logic2AlloyLanguageMapper mapper, ALSDocument specification, Logic2AlloyLanguageMapperTrace trace, AlloySolverConfiguration config) { //val knownStringNumber = specification.eAllContents.filter(ALSStringLiteral).map[it.value].toSet.size @@ -65,41 +67,88 @@ class RunCommandMapper { it.number = typeMapper.getUndefinedSupertypeScope(config.typeScopes.maxNewElements,trace) it.exactly = (config.typeScopes.maxNewElements == config.typeScopes.minNewElements) ] - if(config.typeScopes.maxNewIntegers == LogicSolverConfiguration::Unlimited) { - val integersUsed = specification.eAllContents.filter(ALSInt) - if(integersUsed.empty) { - // If no integer scope is defined, but the problem has no integers - // => scope can be empty - it.typeScopes+= createALSIntScope => [ - it.number = 0 - ] - } else { - // If no integer scope is defined, and the problem has integers - // => error - throw new UnsupportedOperationException('''An integer scope have to be specified for Alloy!''') - } + setIntegerScope(specification,config,it) + setStringScope(specification,config,it) + ] + } + + protected def Boolean setStringScope(ALSDocument specification, AlloySolverConfiguration config, ALSRunCommand it) { + if(config.typeScopes.maxNewStrings === LogicSolverConfiguration::Unlimited) { + throw new UnsupportedOperationException('''A string scope have to be specified for Alloy!''') + } else { + if(config.typeScopes.maxNewStrings == 0) { + it.typeScopes += createALSStringScope => [it.number = 0] } else { - it.typeScopes += createALSIntScope => [ - 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)+1 - } - ] + throw new UnsupportedOperationException('''A string scope have to be specified for Alloy!''') } - if(config.typeScopes.maxNewStrings === LogicSolverConfiguration::Unlimited) { - throw new UnsupportedOperationException('''An string scope have to be specified for Alloy!''') + } + } + + protected def setIntegerScope(ALSDocument specification, AlloySolverConfiguration config, ALSRunCommand command) { + //AlloySolverConfiguration config, ALSRunCommand it + + // If the scope is unlimited ... + if(config.typeScopes.maxNewIntegers == LogicSolverConfiguration::Unlimited) { + val integersUsed = specification.eAllContents.filter(ALSInt) + if(integersUsed.empty) { + // ... but the problem has no integers => scope can be empty + command.typeScopes+= createALSIntScope => [ it.number = 0 ] } else { - if(config.typeScopes.maxNewStrings != 0) { - it.typeScopes += createALSStringScope => [it.number = 0] - } + // If no integer scope is defined, and the problem has integers => error + throw new UnsupportedOperationException('''An integer scope have to be specified for Alloy!''') } - ] + } else { + // If the scope is limited, collect the integers in the problem and the scope,... + val maxIntScope = config.typeScopes.maxNewIntegers + val minIntScope = config.typeScopes.minNewIntegers + val knownIntegers = config.typeScopes.knownIntegers + val integersInProblem = specification.eAllContents.filter(ALSNumberLiteral).map[it.value] + // And select the range of integers + val min = #[minIntScope,knownIntegers.min,integersInProblem.min].min + val max = #[maxIntScope,knownIntegers.max,integersInProblem.max].max + //val abs = Math.max(Math.abs(min),Math.abs(max)) + + + command.typeScopes += createALSIntScope => [ + it.number = toBits(min, max) + ] + } + +// if(config.typeScopes.knownIntegers.empty) { +// return 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 +// } +// return Integer.SIZE-Integer.numberOfLeadingZeros(scope)+1 +// } + } + + private static def toBits(int min, int max) { + // 4 Int = {-8, ..., 7} + // x Int = {- (2^(x-1)) , ... , 2^(x-1)-1} + var int bits = 1 + // range = 2^(x-1) + var int range = 1 + while((!(-range <= min)) || (!(max <= range-1))) { + bits++ + range*=2 + } + return bits } +// +// def static void main(String[] args) { +// println('''0,0->«toBits(0,0)»''') +// println('''1,1->«toBits(1,1)»''') +// println('''-1,-1->«toBits(-1,-1)»''') +// println('''5,6->«toBits(5,6)»''') +// println('''0,6->«toBits(0,6)»''') +// println('''-10,0->«toBits(-10,0)»''') +// println('''-8,7->«toBits(-8,7)»''') +// println('''-100,100->«toBits(-100,100)»''') +// println('''-300,300->«toBits(-300,300)»''') +// } } \ No newline at end of file -- cgit v1.2.3-54-g00ecf