diff options
author | 2019-08-30 15:53:24 +0200 | |
---|---|---|
committer | 2019-08-30 15:53:24 +0200 | |
commit | a21a898301a172c56cfb99b749844db1d308babe (patch) | |
tree | 9c6132bf13a6f23bf969f2d913cdbf632ac78abc /Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy | |
parent | FAM metamodel loader experiments (diff) | |
parent | scopes added to alloy (diff) | |
download | VIATRA-Generator-a21a898301a172c56cfb99b749844db1d308babe.tar.gz VIATRA-Generator-a21a898301a172c56cfb99b749844db1d308babe.tar.zst VIATRA-Generator-a21a898301a172c56cfb99b749844db1d308babe.zip |
Merge remote-tracking branch 'origin/master' into kris
Diffstat (limited to 'Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy')
3 files changed, 201 insertions, 63 deletions
diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_RelationMapper.xtend b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_RelationMapper.xtend index 0762efce..8de9688b 100644 --- a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_RelationMapper.xtend +++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_RelationMapper.xtend | |||
@@ -133,11 +133,11 @@ class Logic2AlloyLanguageMapper_RelationMapper { | |||
133 | public def dispatch void prepareTransitiveClosure(RelationDefinition relation, Logic2AlloyLanguageMapperTrace trace) { | 133 | public def dispatch void prepareTransitiveClosure(RelationDefinition relation, Logic2AlloyLanguageMapperTrace trace) { |
134 | if(relation.parameters.size === 2) { | 134 | if(relation.parameters.size === 2) { |
135 | /** 1. Create a relation that can be used in ^relation expressions */ | 135 | /** 1. Create a relation that can be used in ^relation expressions */ |
136 | val declaration = this.createRelationDeclaration('''AsDeclaration «relation.name»''',relation.parameters,trace) | 136 | val declaration = this.createRelationDeclaration(support.toID('''AsDeclaration «relation.name»'''),relation.parameters,trace) |
137 | trace.relationInTransitiveToHosterField.put(relation,declaration) | 137 | trace.relationInTransitiveToHosterField.put(relation,declaration) |
138 | /** 2. Add fact that the declaration corresponds to the definition */ | 138 | /** 2. Add fact that the declaration corresponds to the definition */ |
139 | val fact = createALSFactDeclaration => [ | 139 | val fact = createALSFactDeclaration => [ |
140 | it.name = '''EqualsAsDeclaration «relation.name»''' | 140 | it.name = support.toID('''EqualsAsDeclaration «relation.name»''') |
141 | it.term = createALSQuantifiedEx => [ | 141 | it.term = createALSQuantifiedEx => [ |
142 | val a = createALSVariableDeclaration => [ | 142 | val a = createALSVariableDeclaration => [ |
143 | it.name = "a" | 143 | it.name = "a" |
@@ -157,7 +157,7 @@ class Logic2AlloyLanguageMapper_RelationMapper { | |||
157 | it.params += createALSReference => [ it.referred = b ] | 157 | it.params += createALSReference => [ it.referred = b ] |
158 | ] | 158 | ] |
159 | it.rightOperand = createALSSubset => [ | 159 | it.rightOperand = createALSSubset => [ |
160 | it.leftOperand = createALSJoin => [ | 160 | it.leftOperand = createALSDirectProduct => [ |
161 | it.leftOperand = createALSReference => [ referred = a ] | 161 | it.leftOperand = createALSReference => [ referred = a ] |
162 | it.rightOperand = createALSReference => [ referred = b ] | 162 | it.rightOperand = createALSReference => [ referred = b ] |
163 | ] | 163 | ] |
@@ -183,12 +183,15 @@ class Logic2AlloyLanguageMapper_RelationMapper { | |||
183 | rightOperand = createALSReference => [ referred =relation.lookup(trace.relationInTransitiveToGlobalField) ] | 183 | rightOperand = createALSReference => [ referred =relation.lookup(trace.relationInTransitiveToGlobalField) ] |
184 | ] | 184 | ] |
185 | } else if(trace.relationInTransitiveToHosterField.containsKey(relation)){ | 185 | } else if(trace.relationInTransitiveToHosterField.containsKey(relation)){ |
186 | createALSReference => [it.referred = relation.lookup(trace.relationInTransitiveToHosterField) ] | 186 | createALSJoin => [ |
187 | leftOperand = createALSReference => [referred = trace.logicLanguage] | ||
188 | rightOperand = createALSReference => [it.referred = relation.lookup(trace.relationInTransitiveToHosterField) ] | ||
189 | ] | ||
187 | } else { | 190 | } else { |
188 | throw new AssertionError('''Relation «relation.name» is not prepared to transitive closure!''') | 191 | throw new AssertionError('''Relation «relation.name» is not prepared to transitive closure!''') |
189 | } | 192 | } |
190 | return createALSSubset => [ | 193 | return createALSSubset => [ |
191 | it.leftOperand = createALSJoin => [ | 194 | it.leftOperand = createALSDirectProduct => [ |
192 | it.leftOperand = source | 195 | it.leftOperand = source |
193 | it.rightOperand = target | 196 | it.rightOperand = target |
194 | ] | 197 | ] |
diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeScopeMapping.xtend b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeScopeMapping.xtend new file mode 100644 index 00000000..a270cb73 --- /dev/null +++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeScopeMapping.xtend | |||
@@ -0,0 +1,44 @@ | |||
1 | package hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder | ||
2 | |||
3 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type | ||
4 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSDocument | ||
5 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.AlloyLanguageFactory | ||
6 | |||
7 | interface Logic2AlloyLanguageMapper_TypeScopeMapping { | ||
8 | def void addLowerMultiplicity(ALSDocument document, Type type, int lowerMultiplicty, Logic2AlloyLanguageMapper mapper, Logic2AlloyLanguageMapperTrace trace) | ||
9 | def void addUpperMultiplicity(ALSDocument document, Type type, int upperMultiplicty, Logic2AlloyLanguageMapper mapper, Logic2AlloyLanguageMapperTrace trace) | ||
10 | } | ||
11 | |||
12 | class Logic2AlloyLanguageMapper_AsConstraint implements Logic2AlloyLanguageMapper_TypeScopeMapping { | ||
13 | val extension AlloyLanguageFactory factory = AlloyLanguageFactory.eINSTANCE | ||
14 | val Logic2AlloyLanguageMapper_Support support = new Logic2AlloyLanguageMapper_Support; | ||
15 | val Logic2AlloyLanguageMapper_TypeMapper typeMapper | ||
16 | |||
17 | new(Logic2AlloyLanguageMapper_TypeMapper mapper) { | ||
18 | this.typeMapper = mapper | ||
19 | } | ||
20 | |||
21 | override addLowerMultiplicity(ALSDocument document, Type type, int lowerMultiplicty, Logic2AlloyLanguageMapper mapper, Logic2AlloyLanguageMapperTrace trace) { | ||
22 | document.factDeclarations += createALSFactDeclaration => [ | ||
23 | it.name = support.toID(#["LowerMultiplicity",support.toID(type.name),lowerMultiplicty.toString]) | ||
24 | it.term = createALSLeq => [ | ||
25 | it.leftOperand = createALSCardinality => [ | ||
26 | it.operand = support.unfoldPlus(typeMapper.transformTypeReference(type,mapper,trace).map[t|createALSReference => [it.referred = t]].toList) | ||
27 | ] | ||
28 | it.rightOperand = createALSNumberLiteral => [it.value = lowerMultiplicty] | ||
29 | ] | ||
30 | ] | ||
31 | } | ||
32 | |||
33 | override addUpperMultiplicity(ALSDocument document, Type type, int upperMultiplicty, Logic2AlloyLanguageMapper mapper, Logic2AlloyLanguageMapperTrace trace) { | ||
34 | document.factDeclarations += createALSFactDeclaration => [ | ||
35 | it.name = support.toID(#["UpperMultiplicity",support.toID(type.name),upperMultiplicty.toString]) | ||
36 | it.term = createALSMeq => [ | ||
37 | it.leftOperand = createALSCardinality => [ | ||
38 | it.operand = support.unfoldPlus(typeMapper.transformTypeReference(type,mapper,trace).map[t|createALSReference => [it.referred = t]].toList) | ||
39 | ] | ||
40 | it.rightOperand = createALSNumberLiteral => [it.value = upperMultiplicty] | ||
41 | ] | ||
42 | ] | ||
43 | } | ||
44 | } \ No newline at end of file | ||
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..494197bc 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,25 +3,26 @@ package hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder | |||
3 | import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.AlloySolverConfiguration | 3 | import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.AlloySolverConfiguration |
4 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSDocument | 4 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSDocument |
5 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSInt | 5 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSInt |
6 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSNumberLiteral | ||
7 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSRunCommand | ||
8 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSString | ||
6 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSTerm | 9 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSTerm |
7 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.AlloyLanguageFactory | 10 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.AlloyLanguageFactory |
8 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration | 11 | 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 | import java.util.List |
12 | 13 | ||
13 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* | ||
14 | |||
15 | class RunCommandMapper { | 14 | class RunCommandMapper { |
16 | private val extension AlloyLanguageFactory factory = AlloyLanguageFactory.eINSTANCE | 15 | val extension AlloyLanguageFactory factory = AlloyLanguageFactory.eINSTANCE |
17 | private val Logic2AlloyLanguageMapper_Support support = new Logic2AlloyLanguageMapper_Support; | 16 | val Logic2AlloyLanguageMapper_Support support = new Logic2AlloyLanguageMapper_Support; |
18 | private val Logic2AlloyLanguageMapper_TypeMapper typeMapper; | 17 | val Logic2AlloyLanguageMapper_TypeMapper typeMapper; |
18 | val Logic2AlloyLanguageMapper_TypeScopeMapping typeScopeMapping; | ||
19 | 19 | ||
20 | public new(Logic2AlloyLanguageMapper_TypeMapper typeMapper) { | 20 | new(Logic2AlloyLanguageMapper_TypeMapper typeMapper) { |
21 | this.typeMapper = typeMapper | 21 | this.typeMapper = typeMapper |
22 | this.typeScopeMapping = new Logic2AlloyLanguageMapper_AsConstraint(typeMapper) | ||
22 | } | 23 | } |
23 | 24 | ||
24 | def public transformRunCommand(Logic2AlloyLanguageMapper mapper, ALSDocument specification, Logic2AlloyLanguageMapperTrace trace, AlloySolverConfiguration config) | 25 | def transformRunCommand(Logic2AlloyLanguageMapper mapper, ALSDocument specification, Logic2AlloyLanguageMapperTrace trace, AlloySolverConfiguration config) |
25 | { | 26 | { |
26 | //val knownStringNumber = specification.eAllContents.filter(ALSStringLiteral).map[it.value].toSet.size | 27 | //val knownStringNumber = specification.eAllContents.filter(ALSStringLiteral).map[it.value].toSet.size |
27 | 28 | ||
@@ -36,28 +37,47 @@ class RunCommandMapper { | |||
36 | it.term = support.unfoldAnd(equals) | 37 | it.term = support.unfoldAnd(equals) |
37 | ] | 38 | ] |
38 | } | 39 | } |
39 | val typeScopes = new LinkedList | 40 | |
40 | for(definedScope : config.typeScopes.maxNewElementsByType.entrySet) { | 41 | /* |
41 | val key = definedScope.key | 42 | val upperLimits = new LinkedList |
42 | val amount = definedScope.value | 43 | val lowerLimits = new LinkedList |
43 | val exactly = config.typeScopes.minNewElementsByType.containsKey(key) && config.typeScopes.minNewElementsByType.get(key) === amount | 44 | |
44 | 45 | /*val typesWithScopeConstraint = config.typeScopes.maxNewElementsByType.keySet + config.typeScopes.minNewElementsByType.keySet | |
45 | val existing = key.transitiveClosureStar[it.subtypes].filter(TypeDefinition).map[elements].flatten.toSet | 46 | for(type : typesWithScopeConstraint) { |
46 | if(amount == 0 && exactly) { | 47 | val max = if(config.typeScopes.maxNewElementsByType.containsKey(type)) { |
47 | specification.factDeclarations += createALSFactDeclaration => [ | 48 | config.typeScopes.maxNewElementsByType.get(type) |
48 | it.term = createALSEquals => [ | 49 | } else { |
49 | it.leftOperand = support.unfoldPlus(typeMapper.transformTypeReference(key,mapper,trace).map[t|createALSReference => [it.referred = t]].toList) | 50 | LogicSolverConfiguration::Unlimited |
50 | it.rightOperand = support.unfoldPlus( existing.map[typeMapper.transformReference(it,trace)].toList ) | 51 | } |
51 | ] | 52 | val min = if(config.typeScopes.minNewElementsByType.containsKey(type)) { |
53 | config.typeScopes.minNewElementsByType.get(type) | ||
54 | } else { | ||
55 | 0 | ||
56 | } | ||
57 | |||
58 | val exactly = min === max | ||
59 | |||
60 | if(max === 0) { | ||
61 | val existing = type.transitiveClosureStar[it.subtypes].filter(TypeDefinition).map[elements].flatten.toSet | ||
62 | specification.factDeclarations += createALSFactDeclaration => [ | ||
63 | it.term = createALSEquals => [ | ||
64 | it.leftOperand = support.unfoldPlus(typeMapper.transformTypeReference(type,mapper,trace).map[t|createALSReference => [it.referred = t]].toList) | ||
65 | it.rightOperand = support.unfoldPlus( existing.map[typeMapper.transformReference(it,trace)].toList ) | ||
52 | ] | 66 | ] |
53 | } | 67 | ] |
54 | val int n = existing.size-amount | 68 | } else if(max !== LogicSolverConfiguration::Unlimited) { |
55 | typeScopes += createALSSigScope => [ | 69 | upperLimits += createALSSigScope => [ |
56 | it.type = typeMapper.transformTypeReference(key,mapper,trace).head | 70 | it.type = typeMapper.transformTypeReference(type,mapper,trace).head |
57 | it.number = n | 71 | it.number = max |
58 | it.exactly =exactly | 72 | it.exactly =exactly |
59 | ] | 73 | ] |
74 | } else { | ||
75 | // do nothing | ||
60 | } | 76 | } |
77 | if(min != 0 && ! exactly) { | ||
78 | lowerLimits += type->min | ||
79 | } | ||
80 | }*/ | ||
61 | 81 | ||
62 | specification.runCommand = createALSRunCommand => [ | 82 | specification.runCommand = createALSRunCommand => [ |
63 | it.typeScopes+= createALSSigScope => [ | 83 | it.typeScopes+= createALSSigScope => [ |
@@ -65,41 +85,112 @@ class RunCommandMapper { | |||
65 | it.number = typeMapper.getUndefinedSupertypeScope(config.typeScopes.maxNewElements,trace) | 85 | it.number = typeMapper.getUndefinedSupertypeScope(config.typeScopes.maxNewElements,trace) |
66 | it.exactly = (config.typeScopes.maxNewElements == config.typeScopes.minNewElements) | 86 | it.exactly = (config.typeScopes.maxNewElements == config.typeScopes.minNewElements) |
67 | ] | 87 | ] |
68 | if(config.typeScopes.maxNewIntegers == LogicSolverConfiguration::Unlimited) { | 88 | |
69 | val integersUsed = specification.eAllContents.filter(ALSInt) | 89 | ] |
70 | if(integersUsed.empty) { | 90 | |
71 | // If no integer scope is defined, but the problem has no integers | 91 | for(upperLimit : config.typeScopes.maxNewElementsByType.entrySet) { |
72 | // => scope can be empty | 92 | val limit = upperLimit.value |
73 | it.typeScopes+= createALSIntScope => [ | 93 | if(limit != LogicSolverConfiguration::Unlimited) { |
74 | it.number = 0 | 94 | this.typeScopeMapping.addUpperMultiplicity(specification,upperLimit.key,limit,mapper,trace) |
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 | } | 95 | } |
96 | if(config.typeScopes.maxNewStrings === LogicSolverConfiguration::Unlimited) { | 96 | } |
97 | throw new UnsupportedOperationException('''An string scope have to be specified for Alloy!''') | 97 | |
98 | for(lowerLimit : config.typeScopes.minNewElementsByType.entrySet) { | ||
99 | val limit = lowerLimit.value | ||
100 | if(limit != 0) { | ||
101 | this.typeScopeMapping.addLowerMultiplicity(specification,lowerLimit.key,limit,mapper,trace) | ||
102 | } | ||
103 | } | ||
104 | |||
105 | setIntegerScope(specification,config,specification.runCommand) | ||
106 | setStringScope(specification,config,specification.runCommand) | ||
107 | } | ||
108 | |||
109 | protected def Boolean setStringScope(ALSDocument specification, AlloySolverConfiguration config, ALSRunCommand it) { | ||
110 | if(config.typeScopes.maxNewStrings === LogicSolverConfiguration::Unlimited) { | ||
111 | throw new UnsupportedOperationException('''A string scope have to be specified for Alloy!''') | ||
112 | } else { | ||
113 | if(config.typeScopes.maxNewStrings == 0) { | ||
114 | it.typeScopes += createALSStringScope => [it.number = 0] | ||
98 | } else { | 115 | } else { |
99 | if(config.typeScopes.maxNewStrings != 0) { | 116 | if(specification.eAllContents.filter(ALSString).empty) { |
100 | it.typeScopes += createALSStringScope => [it.number = 0] | 117 | it.typeScopes += createALSStringScope => [it.number = 0] |
118 | } else { | ||
119 | throw new UnsupportedOperationException('''A string scope have to be specified for Alloy!''') | ||
101 | } | 120 | } |
102 | } | 121 | } |
103 | ] | 122 | } |
123 | } | ||
124 | |||
125 | protected def setIntegerScope(ALSDocument specification, AlloySolverConfiguration config, ALSRunCommand command) { | ||
126 | //AlloySolverConfiguration config, ALSRunCommand it | ||
127 | |||
128 | // If the scope is unlimited ... | ||
129 | if(config.typeScopes.maxNewIntegers == LogicSolverConfiguration::Unlimited) { | ||
130 | val integersUsed = specification.eAllContents.filter(ALSInt) | ||
131 | if(integersUsed.empty) { | ||
132 | // ... but the problem has no integers => scope can be empty | ||
133 | command.typeScopes+= createALSIntScope => [ it.number = 0 ] | ||
134 | } else { | ||
135 | // If no integer scope is defined, and the problem has integers => error | ||
136 | throw new UnsupportedOperationException('''An integer scope have to be specified for Alloy!''') | ||
137 | } | ||
138 | } else { | ||
139 | // If the scope is limited, collect the integers in the problem and the scope,... | ||
140 | //val maxIntScope = config.typeScopes.maxNewIntegers | ||
141 | //val minIntScope = config.typeScopes.minNewIntegers | ||
142 | val knownIntegers = config.typeScopes.knownIntegers | ||
143 | val minKnownInteger = if(knownIntegers.empty) { Integer.MAX_VALUE } else { knownIntegers.min } | ||
144 | val maxKnownInteger = if(knownIntegers.empty) { Integer.MIN_VALUE } else { knownIntegers.max } | ||
145 | val integersInProblem = specification.eAllContents.filter(ALSNumberLiteral).map[it.value].toList | ||
146 | val minIntegerInProblem = if(integersInProblem.empty) { Integer.MAX_VALUE } else { integersInProblem.min } | ||
147 | val maxIntegerInProblem = if(integersInProblem.empty) { Integer.MIN_VALUE } else { integersInProblem.max } | ||
148 | // And select the range of integers | ||
149 | val min = #[minKnownInteger,minIntegerInProblem].min | ||
150 | val max = #[maxKnownInteger,maxIntegerInProblem].max | ||
151 | //val abs = Math.max(Math.abs(min),Math.abs(max)) | ||
152 | |||
153 | |||
154 | command.typeScopes += createALSIntScope => [ | ||
155 | it.number = toBits(min, max) | ||
156 | ] | ||
157 | } | ||
158 | |||
159 | // if(config.typeScopes.knownIntegers.empty) { | ||
160 | // return Integer.SIZE-Integer.numberOfLeadingZeros((config.typeScopes.maxNewIntegers+1)/2) | ||
161 | // } else { | ||
162 | // var scope = Math.max( | ||
163 | // Math.abs(config.typeScopes.knownIntegers.max), | ||
164 | // Math.abs(config.typeScopes.knownIntegers.min)) | ||
165 | // if(scope*2+1 < config.typeScopes.knownIntegers.size + config.typeScopes.maxNewIntegers) { | ||
166 | // scope += ((config.typeScopes.knownIntegers.size + config.typeScopes.maxNewIntegers) - (scope*2))/2 | ||
167 | // } | ||
168 | // return Integer.SIZE-Integer.numberOfLeadingZeros(scope)+1 | ||
169 | // } | ||
170 | } | ||
171 | |||
172 | private static def toBits(int min, int max) { | ||
173 | // 4 Int = {-8, ..., 7} | ||
174 | // x Int = {- (2^(x-1)) , ... , 2^(x-1)-1} | ||
175 | var int bits = 1 | ||
176 | // range = 2^(x-1) | ||
177 | var int range = 1 | ||
178 | while((!(-range <= min)) || (!(max <= range-1))) { | ||
179 | bits++ | ||
180 | range*=2 | ||
181 | } | ||
182 | return bits | ||
104 | } | 183 | } |
184 | // | ||
185 | // def static void main(String[] args) { | ||
186 | // println('''0,0->«toBits(0,0)»''') | ||
187 | // println('''1,1->«toBits(1,1)»''') | ||
188 | // println('''-1,-1->«toBits(-1,-1)»''') | ||
189 | // println('''5,6->«toBits(5,6)»''') | ||
190 | // println('''0,6->«toBits(0,6)»''') | ||
191 | // println('''-10,0->«toBits(-10,0)»''') | ||
192 | // println('''-8,7->«toBits(-8,7)»''') | ||
193 | // println('''-100,100->«toBits(-100,100)»''') | ||
194 | // println('''-300,300->«toBits(-300,300)»''') | ||
195 | // } | ||
105 | } \ No newline at end of file | 196 | } \ No newline at end of file |