aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorLibravatar Kristóf Marussy <kris7topher@gmail.com>2019-08-30 15:53:24 +0200
committerLibravatar Kristóf Marussy <kris7topher@gmail.com>2019-08-30 15:53:24 +0200
commita21a898301a172c56cfb99b749844db1d308babe (patch)
tree9c6132bf13a6f23bf969f2d913cdbf632ac78abc
parentFAM metamodel loader experiments (diff)
parentscopes added to alloy (diff)
downloadVIATRA-Generator-a21a898301a172c56cfb99b749844db1d308babe.tar.gz
VIATRA-Generator-a21a898301a172c56cfb99b749844db1d308babe.tar.zst
VIATRA-Generator-a21a898301a172c56cfb99b749844db1d308babe.zip
Merge remote-tracking branch 'origin/master' into kris
-rw-r--r--Framework/hu.bme.mit.inf.dslreasoner.logic.model/src/hu/bme/mit/inf/dslreasoner/logic/model/builder/LogicProblemBuilder.xtend4
-rw-r--r--Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_RelationMapper.xtend13
-rw-r--r--Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeScopeMapping.xtend44
-rw-r--r--Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/RunCommandMapper.xtend207
4 files changed, 203 insertions, 65 deletions
diff --git a/Framework/hu.bme.mit.inf.dslreasoner.logic.model/src/hu/bme/mit/inf/dslreasoner/logic/model/builder/LogicProblemBuilder.xtend b/Framework/hu.bme.mit.inf.dslreasoner.logic.model/src/hu/bme/mit/inf/dslreasoner/logic/model/builder/LogicProblemBuilder.xtend
index a231af3c..fa97cbef 100644
--- a/Framework/hu.bme.mit.inf.dslreasoner.logic.model/src/hu/bme/mit/inf/dslreasoner/logic/model/builder/LogicProblemBuilder.xtend
+++ b/Framework/hu.bme.mit.inf.dslreasoner.logic.model/src/hu/bme/mit/inf/dslreasoner/logic/model/builder/LogicProblemBuilder.xtend
@@ -494,8 +494,8 @@ class LogicProblemBuilder{
494 def transitiveClosure(Relation relation, TermDescription source, TermDescription target) { 494 def transitiveClosure(Relation relation, TermDescription source, TermDescription target) {
495 createTransitiveClosure => [ 495 createTransitiveClosure => [
496 it.relation = relation 496 it.relation = relation
497 it.leftOperand = leftOperand 497 it.leftOperand = source.toTerm
498 it.rightOperand = rightOperand 498 it.rightOperand = target.toTerm
499 ] 499 ]
500 } 500 }
501 501
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 @@
1package hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder
2
3import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type
4import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSDocument
5import hu.bme.mit.inf.dslreasoner.alloyLanguage.AlloyLanguageFactory
6
7interface 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
12class 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
3import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.AlloySolverConfiguration 3import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.AlloySolverConfiguration
4import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSDocument 4import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSDocument
5import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSInt 5import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSInt
6import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSNumberLiteral
7import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSRunCommand
8import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSString
6import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSTerm 9import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSTerm
7import hu.bme.mit.inf.dslreasoner.alloyLanguage.AlloyLanguageFactory 10import hu.bme.mit.inf.dslreasoner.alloyLanguage.AlloyLanguageFactory
8import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration 11import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration
9import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition
10import java.util.LinkedList
11import java.util.List 12import java.util.List
12 13
13import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*
14
15class RunCommandMapper { 14class 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