diff options
Diffstat (limited to 'Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/RunCommandMapper.xtend')
| -rw-r--r-- | Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/RunCommandMapper.xtend | 105 |
1 files changed, 0 insertions, 105 deletions
diff --git a/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/RunCommandMapper.xtend b/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/RunCommandMapper.xtend deleted file mode 100644 index fdc35412..00000000 --- a/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/RunCommandMapper.xtend +++ /dev/null | |||
| @@ -1,105 +0,0 @@ | |||
| 1 | package hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder | ||
| 2 | |||
| 3 | import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.AlloySolverConfiguration | ||
| 4 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSDocument | ||
| 5 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSInt | ||
| 6 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSTerm | ||
| 7 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.AlloyLanguageFactory | ||
| 8 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration | ||
| 9 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition | ||
| 10 | import java.util.LinkedList | ||
| 11 | import java.util.List | ||
| 12 | |||
| 13 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* | ||
| 14 | |||
| 15 | class RunCommandMapper { | ||
| 16 | private val extension AlloyLanguageFactory factory = AlloyLanguageFactory.eINSTANCE | ||
| 17 | private val Logic2AlloyLanguageMapper_Support support = new Logic2AlloyLanguageMapper_Support; | ||
| 18 | private val Logic2AlloyLanguageMapper_TypeMapper typeMapper; | ||
| 19 | |||
| 20 | public new(Logic2AlloyLanguageMapper_TypeMapper typeMapper) { | ||
| 21 | this.typeMapper = typeMapper | ||
| 22 | } | ||
| 23 | |||
| 24 | def public transformRunCommand(Logic2AlloyLanguageMapper mapper, ALSDocument specification, Logic2AlloyLanguageMapperTrace trace, AlloySolverConfiguration config) | ||
| 25 | { | ||
| 26 | //val knownStringNumber = specification.eAllContents.filter(ALSStringLiteral).map[it.value].toSet.size | ||
| 27 | |||
| 28 | // add fact to ensure the existence of all literals in the scope | ||
| 29 | if(!config.typeScopes.knownStrings.empty) { | ||
| 30 | specification.factDeclarations += createALSFactDeclaration => [ | ||
| 31 | it.name = "EnsureAllStrings" | ||
| 32 | val List<? extends ALSTerm> equals = config.typeScopes.knownStrings.map[x|createALSEquals => [ | ||
| 33 | it.leftOperand =createALSStringLiteral => [it.value = x] | ||
| 34 | it.rightOperand =createALSStringLiteral => [it.value = x] | ||
| 35 | ]].toList | ||
| 36 | it.term = support.unfoldAnd(equals) | ||
| 37 | ] | ||
| 38 | } | ||
| 39 | val typeScopes = new LinkedList | ||
| 40 | for(definedScope : config.typeScopes.maxNewElementsByType.entrySet) { | ||
| 41 | val key = definedScope.key | ||
| 42 | val amount = definedScope.value | ||
| 43 | val exactly = config.typeScopes.minNewElementsByType.containsKey(key) && config.typeScopes.minNewElementsByType.get(key) === amount | ||
| 44 | |||
| 45 | val existing = key.transitiveClosureStar[it.subtypes].filter(TypeDefinition).map[elements].flatten.toSet | ||
| 46 | if(amount == 0 && exactly) { | ||
| 47 | specification.factDeclarations += createALSFactDeclaration => [ | ||
| 48 | it.term = createALSEquals => [ | ||
| 49 | it.leftOperand = support.unfoldPlus(typeMapper.transformTypeReference(key,mapper,trace).map[t|createALSReference => [it.referred = t]].toList) | ||
| 50 | it.rightOperand = support.unfoldPlus( existing.map[typeMapper.transformReference(it,trace)].toList ) | ||
| 51 | ] | ||
| 52 | ] | ||
| 53 | } | ||
| 54 | val int n = existing.size-amount | ||
| 55 | typeScopes += createALSSigScope => [ | ||
| 56 | it.type = typeMapper.transformTypeReference(key,mapper,trace).head | ||
| 57 | it.number = n | ||
| 58 | it.exactly =exactly | ||
| 59 | ] | ||
| 60 | } | ||
| 61 | |||
| 62 | specification.runCommand = createALSRunCommand => [ | ||
| 63 | it.typeScopes+= createALSSigScope => [ | ||
| 64 | it.type= typeMapper.getUndefinedSupertype(trace) | ||
| 65 | it.number = typeMapper.getUndefinedSupertypeScope(config.typeScopes.maxNewElements,trace) | ||
| 66 | it.exactly = (config.typeScopes.maxNewElements == config.typeScopes.minNewElements) | ||
| 67 | ] | ||
| 68 | if(config.typeScopes.maxNewIntegers == LogicSolverConfiguration::Unlimited) { | ||
| 69 | val integersUsed = specification.eAllContents.filter(ALSInt) | ||
| 70 | if(integersUsed.empty) { | ||
| 71 | // If no integer scope is defined, but the problem has no integers | ||
| 72 | // => scope can be empty | ||
| 73 | it.typeScopes+= createALSIntScope => [ | ||
| 74 | it.number = 0 | ||
| 75 | ] | ||
| 76 | } else { | ||
| 77 | // If no integer scope is defined, and the problem has integers | ||
| 78 | // => error | ||
| 79 | throw new UnsupportedOperationException('''An integer scope have to be specified for Alloy!''') | ||
| 80 | } | ||
| 81 | } else { | ||
| 82 | it.typeScopes += createALSIntScope => [ | ||
| 83 | if(config.typeScopes.knownIntegers.empty) { | ||
| 84 | number = Integer.SIZE-Integer.numberOfLeadingZeros(config.typeScopes.maxNewIntegers+1/2) | ||
| 85 | } else { | ||
| 86 | var scope = Math.max( | ||
| 87 | Math.abs(config.typeScopes.knownIntegers.max), | ||
| 88 | Math.abs(config.typeScopes.knownIntegers.min)) | ||
| 89 | if(scope*2+1 < config.typeScopes.knownIntegers.size + config.typeScopes.maxNewIntegers) { | ||
| 90 | scope += ((config.typeScopes.knownIntegers.size + config.typeScopes.maxNewIntegers) - (scope*2))/2 | ||
| 91 | } | ||
| 92 | number = Integer.SIZE-Integer.numberOfLeadingZeros(scope)+1 | ||
| 93 | } | ||
| 94 | ] | ||
| 95 | } | ||
| 96 | if(config.typeScopes.maxNewStrings === LogicSolverConfiguration::Unlimited) { | ||
| 97 | throw new UnsupportedOperationException('''An string scope have to be specified for Alloy!''') | ||
| 98 | } else { | ||
| 99 | if(config.typeScopes.maxNewStrings != 0) { | ||
| 100 | it.typeScopes += createALSStringScope => [it.number = 0] | ||
| 101 | } | ||
| 102 | } | ||
| 103 | ] | ||
| 104 | } | ||
| 105 | } \ No newline at end of file | ||