diff options
Diffstat (limited to 'Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/RunCommandMapper.xtend')
-rw-r--r-- | Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/RunCommandMapper.xtend | 105 |
1 files changed, 105 insertions, 0 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 new file mode 100644 index 00000000..3e96f7f4 --- /dev/null +++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/RunCommandMapper.xtend | |||
@@ -0,0 +1,105 @@ | |||
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 | ||