1 files changed, 149 insertions, 58 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..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
 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.ALSString
 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
-import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition
-import java.util.LinkedList
 import java.util.List
-import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*
 class RunCommandMapper {
-        private val extension AlloyLanguageFactory factory = AlloyLanguageFactory.eINSTANCE
+        val extension AlloyLanguageFactory factory = AlloyLanguageFactory.eINSTANCE
-        private val Logic2AlloyLanguageMapper_Support support = new Logic2AlloyLanguageMapper_Support;
+        val Logic2AlloyLanguageMapper_Support support = new Logic2AlloyLanguageMapper_Support;
-        private val Logic2AlloyLanguageMapper_TypeMapper typeMapper;
+        val Logic2AlloyLanguageMapper_TypeMapper typeMapper;
+        val Logic2AlloyLanguageMapper_TypeScopeMapping typeScopeMapping;
        
-        public new(Logic2AlloyLanguageMapper_TypeMapper typeMapper) {
+        new(Logic2AlloyLanguageMapper_TypeMapper typeMapper) {
                this.typeMapper = typeMapper
+                this.typeScopeMapping = new Logic2AlloyLanguageMapper_AsConstraint(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
                
@@ -36,28 +37,47 @@ class RunCommandMapper {
                                it.term = support.unfoldAnd(equals)
                        ]
                }
-                val typeScopes = new LinkedList
+                
-                for(definedScope : config.typeScopes.maxNewElementsByType.entrySet) {
+                /*
-                                val key = definedScope.key
+                val upperLimits = new LinkedList
-                                val amount = definedScope.value
+                val lowerLimits = new LinkedList
-                                val exactly = config.typeScopes.minNewElementsByType.containsKey(key) && config.typeScopes.minNewElementsByType.get(key) === amount
+                
-                                
+                /*val typesWithScopeConstraint = config.typeScopes.maxNewElementsByType.keySet + config.typeScopes.minNewElementsByType.keySet
-                                val existing = key.transitiveClosureStar[it.subtypes].filter(TypeDefinition).map[elements].flatten.toSet
+                for(type : typesWithScopeConstraint) {
-                                if(amount == 0 && exactly) {
+                        val max = if(config.typeScopes.maxNewElementsByType.containsKey(type)) {
-                                        specification.factDeclarations += createALSFactDeclaration => [
+                                config.typeScopes.maxNewElementsByType.get(type)
-                                                it.term = createALSEquals => [
+                        } else {
-                                                        it.leftOperand = support.unfoldPlus(typeMapper.transformTypeReference(key,mapper,trace).map[t|createALSReference => [it.referred = t]].toList)
+                                LogicSolverConfiguration::Unlimited
-                                                        it.rightOperand =  support.unfoldPlus( existing.map[typeMapper.transformReference(it,trace)].toList )
+                        }
-                                                ]
+                        val min = if(config.typeScopes.minNewElementsByType.containsKey(type)) {
+                                config.typeScopes.minNewElementsByType.get(type)
+                        } else {
+                                0
+                        }
+                        
+                        val exactly = min === max
+                        
+                        if(max === 0) {
+                                val existing = type.transitiveClosureStar[it.subtypes].filter(TypeDefinition).map[elements].flatten.toSet
+                                specification.factDeclarations += createALSFactDeclaration => [
+                                        it.term = createALSEquals => [
+                                                it.leftOperand = support.unfoldPlus(typeMapper.transformTypeReference(type,mapper,trace).map[t|createALSReference => [it.referred = t]].toList)
+                                                it.rightOperand =  support.unfoldPlus( existing.map[typeMapper.transformReference(it,trace)].toList )
                                        ]
-                                }
+                                ]
-                                val int n = existing.size-amount
+                        } else if(max !== LogicSolverConfiguration::Unlimited) {
-                                typeScopes += createALSSigScope => [
+                                upperLimits += createALSSigScope => [
-                                        it.type = typeMapper.transformTypeReference(key,mapper,trace).head
+                                        it.type = typeMapper.transformTypeReference(type,mapper,trace).head
-                                        it.number = n
+                                        it.number = max
                                        it.exactly =exactly
                                ]
+                        } else {
+                                // do nothing
                        }
+                        if(min != 0 && ! exactly) {
+                                lowerLimits += type->min
+                        }
+                }*/
                
                specification.runCommand = createALSRunCommand => [
                        it.typeScopes+= createALSSigScope => [
@@ -65,41 +85,112 @@ 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
+                for(upperLimit : config.typeScopes.maxNewElementsByType.entrySet) {
-                                        // => scope can be empty
+                        val limit = upperLimit.value
-                                        it.typeScopes+= createALSIntScope => [
+                        if(limit != LogicSolverConfiguration::Unlimited) {
-                                                it.number = 0
+                                this.typeScopeMapping.addUpperMultiplicity(specification,upperLimit.key,limit,mapper,trace)
-                                        ]
-                                } 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!''')
-                                }
-                        } 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
-                                        }
-                                ]
                        }
-                        if(config.typeScopes.maxNewStrings === LogicSolverConfiguration::Unlimited) {
+                }
-                                throw new UnsupportedOperationException('''An string scope have to be specified for Alloy!''')
+                
+                for(lowerLimit : config.typeScopes.minNewElementsByType.entrySet) {
+                        val limit = lowerLimit.value
+                        if(limit != 0) {
+                                this.typeScopeMapping.addLowerMultiplicity(specification,lowerLimit.key,limit,mapper,trace)
+                        }
+                }
+                
+                setIntegerScope(specification,config,specification.runCommand)
+                setStringScope(specification,config,specification.runCommand)
+        }
+        
+        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 {
-                                if(config.typeScopes.maxNewStrings != 0) {
+                                if(specification.eAllContents.filter(ALSString).empty) {
                                        it.typeScopes += createALSStringScope => [it.number = 0]
+                                } else {
+                                        throw new UnsupportedOperationException('''A 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 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 minKnownInteger = if(knownIntegers.empty) { Integer.MAX_VALUE } else { knownIntegers.min }
+                        val maxKnownInteger = if(knownIntegers.empty) { Integer.MIN_VALUE } else { knownIntegers.max }
+                        val integersInProblem = specification.eAllContents.filter(ALSNumberLiteral).map[it.value].toList
+                        val minIntegerInProblem = if(integersInProblem.empty) { Integer.MAX_VALUE } else { integersInProblem.min }
+                        val maxIntegerInProblem = if(integersInProblem.empty) { Integer.MIN_VALUE } else { integersInProblem.max }
+                        // And select the range of integers
+                        val min = #[minKnownInteger,minIntegerInProblem].min
+                        val max = #[maxKnownInteger,maxIntegerInProblem].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

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