1 files changed, 146 insertions, 25 deletions
diff --git a/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/ScopeLoader.xtend b/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/ScopeLoader.xtend
index ee1a92f0..9b2b4a3e 100644
--- a/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/ScopeLoader.xtend
+++ b/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/ScopeLoader.xtend
@@ -14,49 +14,172 @@ import hu.bme.mit.inf.dslreasoner.application.applicationConfiguration.StringTyp
 import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic
 import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic_Trace
 import hu.bme.mit.inf.dslreasoner.logic.model.builder.TypeScopes
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition
 import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem
+import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partial2logicannotations.PartialModelRelation2Assertion
+import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.BinaryElementRelationLink
+import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.IntegerElement
+import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.NaryRelationLink
+import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PrimitiveElement
+import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.RealElement
+import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.StringElement
+import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.UnaryElementRelationLink
+import java.math.BigDecimal
+import java.util.HashMap
+import java.util.LinkedList
+import java.util.List
+import java.util.Map
+import java.util.Set
 import org.eclipse.emf.ecore.EClass
+import org.eclipse.xtend.lib.annotations.Data
+import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.IntLiteral
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RealLiteral
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.StringLiteral
+@Data class KnownElements {
+        val Map<Type,Set<DefinedElement>> knownElementsByType
+        val Set<Integer> knownIntegers
+        val Set<BigDecimal> knownReals
+        val Set<String> knownStrings
+}
 class ScopeLoader {     
-        def TypeScopes loadScope(ScopeSpecification specification, LogicProblem problem, Ecore2Logic ecore2Logic, Ecore2Logic_Trace trace) {
+        def loadScope(ScopeSpecification specification, LogicProblem problem, Ecore2Logic ecore2Logic, Ecore2Logic_Trace trace) {
                val res = new TypeScopes
+                val knownElements = initialiseknownElements(problem,res)
+                val inconsistencies = new LinkedList<String>()
+                
                for(scopeSpecification : specification.scopes) {
-                        setSpecification(scopeSpecification,res,ecore2Logic,trace)
+                        setSpecification(scopeSpecification,res,knownElements,ecore2Logic,trace,inconsistencies)
                }
-                return res 
+                
+                return res -> inconsistencies
+        }
+        
+        def protected initialiseknownElements(LogicProblem p, TypeScopes s) {
+                val Map<Type,Set<DefinedElement>> res = new HashMap
+                for(definedType : p.types.filter(TypeDefinition)) {
+                        val supertypes = definedType.<Type>transitiveClosureStar[x|x.supertypes]
+                        for(supertype : supertypes) {
+                                for(element : definedType.elements) {
+                                        res.putOrAddToSet(supertype,element)
+                                }
+                        }
+                }
+                val partailModelContents = p.annotations.filter(PartialModelRelation2Assertion).map[target].toList.map[eAllContents.toIterable].flatten.toList
+                s.knownIntegers += partailModelContents.filter(IntLiteral).map[it.value]
+                s.knownReals += partailModelContents.filter(RealLiteral).map[it.value]
+                s.knownStrings += partailModelContents.filter(StringLiteral).map[it.value]
+                                
+                res
+        }
+        
+        def dispatch getElements(UnaryElementRelationLink link) {
+                #[link.param1]
+        }
+        def dispatch getElements(BinaryElementRelationLink link) {
+                #[link.param1,link.param2]
+        }
+        def dispatch getElements(NaryRelationLink link) {
+                link.elements
        }
        
-        def dispatch setSpecification(ObjectTypeScope scope, TypeScopes aggregated, Ecore2Logic ecore2Logic, Ecore2Logic_Trace trace) {
+        def dispatch setSpecification(ObjectTypeScope scope, TypeScopes aggregated, Map<Type, Set<DefinedElement>> knownElements, Ecore2Logic ecore2Logic, Ecore2Logic_Trace trace, List<String> inconsistencies) {
-                //val existingObjects = 
+                val numberOfKnownElements = knownElements.values.flatten.toSet.size
-                aggregated.minNewElements = getLowerLimit(scope.number)
+                
-                aggregated.maxNewElements = getUpperLimit(scope.number)
+                aggregated.minNewElements = updateLowerLimit(scope.isSetsNew,numberOfKnownElements,aggregated.minNewElements,getLowerLimit(scope.number))
+                aggregated.maxNewElements = updateUpperLimit(scope.isSetsNew,numberOfKnownElements,aggregated.maxNewElements,getUpperLimit(scope.number))
        }
-        def dispatch setSpecification(ClassTypeScope scope, TypeScopes aggregated, Ecore2Logic ecore2Logic, Ecore2Logic_Trace trace) {
+        def dispatch setSpecification(ClassTypeScope scope, TypeScopes aggregated, Map<Type, Set<DefinedElement>> knownElements, Ecore2Logic ecore2Logic, Ecore2Logic_Trace trace, List<String> inconsistencies) {
                val target = scope.type.element
-                if(target.feature != null) {
+                if(target.feature !== null) {
                        throw new IllegalArgumentException('''Feature scopes are not supported: "«target.feature.name»"!''')
                } else {
                        val targetClassifier = target.classifier
                        if(targetClassifier instanceof EClass) {
                                val type = ecore2Logic.TypeofEClass(trace,targetClassifier)
-                                aggregated.minNewElementsByType.put(type,getLowerLimit(scope.number))
+                                val known = type.lookup(knownElements).size
-                                aggregated.maxNewElementsByType.put(type,getUpperLimit(scope.number))
+                                aggregated.minNewElementsByType.put(type,
+                                                updateLowerLimit(
+                                                        scope.setsNew,
+                                                        known,
+                                                        type.lookup(aggregated.minNewElementsByType),
+                                                        getLowerLimit(scope.number)
+                                                )
+                                        )
+                                aggregated.maxNewElementsByType.put(type,
+                                                updateUpperLimit(
+                                                        scope.setsNew,
+                                                        known,
+                                                        type.lookup(aggregated.minNewElementsByType),
+                                                        getUpperLimit(scope.number)
+                                                )
+                                        )
                        } else {
                                throw new IllegalArgumentException('''Non-EClass scopes are not supported: "«targetClassifier.name»"!''')
                        }
                }
        }
-        def dispatch setSpecification(IntegerTypeScope scope, TypeScopes aggregated, Ecore2Logic ecore2Logic, Ecore2Logic_Trace trace) {
+        def dispatch setSpecification(IntegerTypeScope scope, TypeScopes aggregated, Map<Type, Set<DefinedElement>> knownElements, Ecore2Logic ecore2Logic, Ecore2Logic_Trace trace, List<String> inconsistencies) {
-                aggregated.minNewIntegers = scope.number.lowerLimit
+                val number = scope.number
-                aggregated.maxNewIntegers = scope.number.upperLimit
+                if(number instanceof IntEnumberation) {
+                        addToKnownCollection(aggregated.knownIntegers,number.entry,scope.isSetsNew,inconsistencies)
+                } else {
+                        aggregated.minNewIntegers = updateLowerLimit(scope.isSetsNew,aggregated.knownIntegers.size,aggregated.minNewIntegers,number.lowerLimit)
+                        aggregated.maxNewIntegers = updateLowerLimit(scope.isSetsNew,aggregated.knownIntegers.size,aggregated.maxNewIntegers,number.upperLimit)
+                }
+        }
+        
+        def dispatch setSpecification(RealTypeScope scope, TypeScopes aggregated, Map<Type, Set<DefinedElement>> knownElements, Ecore2Logic ecore2Logic, Ecore2Logic_Trace trace, List<String> inconsistencies) {
+                val number = scope.number
+                if(number instanceof RealEnumeration) {
+                        val x = number.entry;
+                        <BigDecimal>addToKnownCollection(aggregated.knownReals,x,scope.isSetsNew,inconsistencies)
+                } else {
+                        aggregated.minNewReals = updateLowerLimit(scope.isSetsNew,aggregated.knownReals.size,aggregated.minNewReals,number.lowerLimit)
+                        aggregated.maxNewReals = updateLowerLimit(scope.isSetsNew,aggregated.knownReals.size,aggregated.maxNewReals,number.upperLimit)
+                }
+        }
+        def dispatch setSpecification(StringTypeScope scope, TypeScopes aggregated, Map<Type, Set<DefinedElement>> knownElements, Ecore2Logic ecore2Logic, Ecore2Logic_Trace trace, List<String> inconsistencies) {
+                val number = scope.number
+                if(number instanceof StringEnumeration) {
+                        <String>addToKnownCollection(aggregated.knownStrings,number.entry,scope.isSetsNew,inconsistencies)
+                } else {
+                        aggregated.minNewStrings = updateLowerLimit(scope.isSetsNew,aggregated.knownStrings.size,aggregated.minNewStrings,number.lowerLimit)
+                        aggregated.maxNewStrings = updateLowerLimit(scope.isSetsNew,aggregated.knownStrings.size,aggregated.maxNewStrings,number.upperLimit)
+                }
+        }
+        def <Type> addToKnownCollection(Set<Type> known, List<Type> definedInScope, boolean isSetNew, List<String> inconsistencies) {
+                if(isSetNew) {
+                                known += definedInScope
+                        } else {
+                                if(!definedInScope.containsAll(known)) {
+                                        val notDefinedInScope = known.filter[!definedInScope.contains(it)]
+                                        inconsistencies += '''Inconsistent scope: problem already contains literal«IF notDefinedInScope.size > 0»s«ENDIF» that excluded by a scope: «FOR e: notDefinedInScope SEPARATOR ", "»«e»«ENDFOR».'''
+                                }
+                                known.clear
+                                known += definedInScope
+                        }
        }
-        def dispatch setSpecification(RealTypeScope scope, TypeScopes aggregated, Ecore2Logic ecore2Logic, Ecore2Logic_Trace trace) {
+        
-                aggregated.minNewReals = scope.number.lowerLimit
+        def updateLowerLimit(boolean isAdditional, int known, int original, int value) {
-                aggregated.maxNewReals = scope.number.upperLimit
+                if(isAdditional) {
+                        return Math.max(original,value)
+                } else {
+                        return Math.max(original,value-known)
+                }
        }
-        def dispatch setSpecification(StringTypeScope scope, TypeScopes aggregated, Ecore2Logic ecore2Logic, Ecore2Logic_Trace trace) {
+        def updateUpperLimit(boolean isAdditional, int known, int original, int value) {
-                aggregated.minNewStrings = scope.number.lowerLimit
+                if(isAdditional) {
-                aggregated.maxNewStrings = scope.number.upperLimit
+                        return Math.min(original,value)
+                } else {
+                        val target = if(value == Integer.MAX_VALUE) { Integer.MAX_VALUE } else {value-known}
+                        return Math.min(original,target)
+                }
        }
        
        def dispatch getLowerLimit(IntervallNumber specification) {
@@ -70,14 +193,12 @@ class ScopeLoader {
        def dispatch getLowerLimit(RealEnumeration specification) { 0 }
        def dispatch getLowerLimit(StringEnumeration specification) { 0 }
        def dispatch getUpperLimit(IntervallNumber specification) {
-                if(specification.isMaxUnlimited) return -1
+                if(specification.isMaxUnlimited) return Integer.MAX_VALUE
                else return specification.maxNumber
        }
        def dispatch getUpperLimit(ExactNumber specification) {
-                if(specification.isExactUnlimited) return -1
+                if(specification.isExactUnlimited) return Integer.MAX_VALUE
                else return specification.exactNumber
        }
-        def dispatch getUpperLimit(IntEnumberation specification) { 0 }
+        
-        def dispatch getUpperLimit(RealEnumeration specification) { 0 }
-        def dispatch getUpperLimit(StringEnumeration specification) { 0 }
 }
 \ No newline at end of file

diff --git a/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/ScopeLoader.xtend b/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/ScopeLoader.xtend index ee1a92f0..9b2b4a3e 100644 --- a/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/ScopeLoader.xtend +++ b/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/ScopeLoader.xtend
@@ -14,49 +14,172 @@ import hu.bme.mit.inf.dslreasoner.application.applicationConfiguration.StringTyp
14	import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic	14	import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic
15	import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic_Trace	15	import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic_Trace
16	import hu.bme.mit.inf.dslreasoner.logic.model.builder.TypeScopes	16	import hu.bme.mit.inf.dslreasoner.logic.model.builder.TypeScopes
		17	import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement
		18	import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type
		19	import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition
17	import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem	20	import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem
		21	import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partial2logicannotations.PartialModelRelation2Assertion
		22	import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.BinaryElementRelationLink
		23	import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.IntegerElement
		24	import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.NaryRelationLink
		25	import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PrimitiveElement
		26	import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.RealElement
		27	import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.StringElement
		28	import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.UnaryElementRelationLink
		29	import java.math.BigDecimal
		30	import java.util.HashMap
		31	import java.util.LinkedList
		32	import java.util.List
		33	import java.util.Map
		34	import java.util.Set
18	import org.eclipse.emf.ecore.EClass	35	import org.eclipse.emf.ecore.EClass
		36	import org.eclipse.xtend.lib.annotations.Data
		37
		38	import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*
		39	import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.IntLiteral
		40	import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RealLiteral
		41	import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.StringLiteral
		42
		43	@Data class KnownElements {
		44	val Map<Type,Set<DefinedElement>> knownElementsByType
		45	val Set<Integer> knownIntegers
		46	val Set<BigDecimal> knownReals
		47	val Set<String> knownStrings
		48	}
19		49
20	class ScopeLoader {	50	class ScopeLoader {
21	def TypeScopes loadScope(ScopeSpecification specification, LogicProblem problem, Ecore2Logic ecore2Logic, Ecore2Logic_Trace trace) {	51	def loadScope(ScopeSpecification specification, LogicProblem problem, Ecore2Logic ecore2Logic, Ecore2Logic_Trace trace) {
22	val res = new TypeScopes	52	val res = new TypeScopes
		53	val knownElements = initialiseknownElements(problem,res)
		54	val inconsistencies = new LinkedList<String>()
		55
23	for(scopeSpecification : specification.scopes) {	56	for(scopeSpecification : specification.scopes) {
24	setSpecification(scopeSpecification,res,ecore2Logic,trace)	57	setSpecification(scopeSpecification,res,knownElements,ecore2Logic,trace,inconsistencies)
25	}	58	}
26	return res	59
		60	return res -> inconsistencies
		61	}
		62
		63	def protected initialiseknownElements(LogicProblem p, TypeScopes s) {
		64	val Map<Type,Set<DefinedElement>> res = new HashMap
		65	for(definedType : p.types.filter(TypeDefinition)) {
		66	val supertypes = definedType.<Type>transitiveClosureStar[x\|x.supertypes]
		67	for(supertype : supertypes) {
		68	for(element : definedType.elements) {
		69	res.putOrAddToSet(supertype,element)
		70	}
		71	}
		72	}
		73	val partailModelContents = p.annotations.filter(PartialModelRelation2Assertion).map[target].toList.map[eAllContents.toIterable].flatten.toList
		74	s.knownIntegers += partailModelContents.filter(IntLiteral).map[it.value]
		75	s.knownReals += partailModelContents.filter(RealLiteral).map[it.value]
		76	s.knownStrings += partailModelContents.filter(StringLiteral).map[it.value]
		77
		78	res
		79	}
		80
		81	def dispatch getElements(UnaryElementRelationLink link) {
		82	#[link.param1]
		83	}
		84	def dispatch getElements(BinaryElementRelationLink link) {
		85	#[link.param1,link.param2]
		86	}
		87	def dispatch getElements(NaryRelationLink link) {
		88	link.elements
27	}	89	}
28		90
29	def dispatch setSpecification(ObjectTypeScope scope, TypeScopes aggregated, Ecore2Logic ecore2Logic, Ecore2Logic_Trace trace) {	91	def dispatch setSpecification(ObjectTypeScope scope, TypeScopes aggregated, Map<Type, Set<DefinedElement>> knownElements, Ecore2Logic ecore2Logic, Ecore2Logic_Trace trace, List<String> inconsistencies) {
30	//val existingObjects =	92	val numberOfKnownElements = knownElements.values.flatten.toSet.size
31	aggregated.minNewElements = getLowerLimit(scope.number)	93
32	aggregated.maxNewElements = getUpperLimit(scope.number)	94	aggregated.minNewElements = updateLowerLimit(scope.isSetsNew,numberOfKnownElements,aggregated.minNewElements,getLowerLimit(scope.number))
		95	aggregated.maxNewElements = updateUpperLimit(scope.isSetsNew,numberOfKnownElements,aggregated.maxNewElements,getUpperLimit(scope.number))
33	}	96	}
34	def dispatch setSpecification(ClassTypeScope scope, TypeScopes aggregated, Ecore2Logic ecore2Logic, Ecore2Logic_Trace trace) {	97	def dispatch setSpecification(ClassTypeScope scope, TypeScopes aggregated, Map<Type, Set<DefinedElement>> knownElements, Ecore2Logic ecore2Logic, Ecore2Logic_Trace trace, List<String> inconsistencies) {
35	val target = scope.type.element	98	val target = scope.type.element
36	if(target.feature != null) {	99	if(target.feature !== null) {
37	throw new IllegalArgumentException('''Feature scopes are not supported: "«target.feature.name»"!''')	100	throw new IllegalArgumentException('''Feature scopes are not supported: "«target.feature.name»"!''')
38	} else {	101	} else {
39	val targetClassifier = target.classifier	102	val targetClassifier = target.classifier
40	if(targetClassifier instanceof EClass) {	103	if(targetClassifier instanceof EClass) {
41	val type = ecore2Logic.TypeofEClass(trace,targetClassifier)	104	val type = ecore2Logic.TypeofEClass(trace,targetClassifier)
42	aggregated.minNewElementsByType.put(type,getLowerLimit(scope.number))	105	val known = type.lookup(knownElements).size
43	aggregated.maxNewElementsByType.put(type,getUpperLimit(scope.number))	106	aggregated.minNewElementsByType.put(type,
		107	updateLowerLimit(
		108	scope.setsNew,
		109	known,
		110	type.lookup(aggregated.minNewElementsByType),
		111	getLowerLimit(scope.number)
		112	)
		113	)
		114	aggregated.maxNewElementsByType.put(type,
		115	updateUpperLimit(
		116	scope.setsNew,
		117	known,
		118	type.lookup(aggregated.minNewElementsByType),
		119	getUpperLimit(scope.number)
		120	)
		121	)
44	} else {	122	} else {
45	throw new IllegalArgumentException('''Non-EClass scopes are not supported: "«targetClassifier.name»"!''')	123	throw new IllegalArgumentException('''Non-EClass scopes are not supported: "«targetClassifier.name»"!''')
46	}	124	}
47	}	125	}
48	}	126	}
49	def dispatch setSpecification(IntegerTypeScope scope, TypeScopes aggregated, Ecore2Logic ecore2Logic, Ecore2Logic_Trace trace) {	127	def dispatch setSpecification(IntegerTypeScope scope, TypeScopes aggregated, Map<Type, Set<DefinedElement>> knownElements, Ecore2Logic ecore2Logic, Ecore2Logic_Trace trace, List<String> inconsistencies) {
50	aggregated.minNewIntegers = scope.number.lowerLimit	128	val number = scope.number
51	aggregated.maxNewIntegers = scope.number.upperLimit	129	if(number instanceof IntEnumberation) {
		130	addToKnownCollection(aggregated.knownIntegers,number.entry,scope.isSetsNew,inconsistencies)
		131	} else {
		132	aggregated.minNewIntegers = updateLowerLimit(scope.isSetsNew,aggregated.knownIntegers.size,aggregated.minNewIntegers,number.lowerLimit)
		133	aggregated.maxNewIntegers = updateLowerLimit(scope.isSetsNew,aggregated.knownIntegers.size,aggregated.maxNewIntegers,number.upperLimit)
		134	}
		135	}
		136
		137	def dispatch setSpecification(RealTypeScope scope, TypeScopes aggregated, Map<Type, Set<DefinedElement>> knownElements, Ecore2Logic ecore2Logic, Ecore2Logic_Trace trace, List<String> inconsistencies) {
		138	val number = scope.number
		139	if(number instanceof RealEnumeration) {
		140	val x = number.entry;
		141	<BigDecimal>addToKnownCollection(aggregated.knownReals,x,scope.isSetsNew,inconsistencies)
		142	} else {
		143	aggregated.minNewReals = updateLowerLimit(scope.isSetsNew,aggregated.knownReals.size,aggregated.minNewReals,number.lowerLimit)
		144	aggregated.maxNewReals = updateLowerLimit(scope.isSetsNew,aggregated.knownReals.size,aggregated.maxNewReals,number.upperLimit)
		145	}
		146	}
		147	def dispatch setSpecification(StringTypeScope scope, TypeScopes aggregated, Map<Type, Set<DefinedElement>> knownElements, Ecore2Logic ecore2Logic, Ecore2Logic_Trace trace, List<String> inconsistencies) {
		148	val number = scope.number
		149	if(number instanceof StringEnumeration) {
		150	<String>addToKnownCollection(aggregated.knownStrings,number.entry,scope.isSetsNew,inconsistencies)
		151	} else {
		152	aggregated.minNewStrings = updateLowerLimit(scope.isSetsNew,aggregated.knownStrings.size,aggregated.minNewStrings,number.lowerLimit)
		153	aggregated.maxNewStrings = updateLowerLimit(scope.isSetsNew,aggregated.knownStrings.size,aggregated.maxNewStrings,number.upperLimit)
		154	}
		155	}
		156	def <Type> addToKnownCollection(Set<Type> known, List<Type> definedInScope, boolean isSetNew, List<String> inconsistencies) {
		157	if(isSetNew) {
		158	known += definedInScope
		159	} else {
		160	if(!definedInScope.containsAll(known)) {
		161	val notDefinedInScope = known.filter[!definedInScope.contains(it)]
		162	inconsistencies += '''Inconsistent scope: problem already contains literal«IF notDefinedInScope.size > 0»s«ENDIF» that excluded by a scope: «FOR e: notDefinedInScope SEPARATOR ", "»«e»«ENDFOR».'''
		163	}
		164	known.clear
		165	known += definedInScope
		166	}
52	}	167	}
53	def dispatch setSpecification(RealTypeScope scope, TypeScopes aggregated, Ecore2Logic ecore2Logic, Ecore2Logic_Trace trace) {	168
54	aggregated.minNewReals = scope.number.lowerLimit	169	def updateLowerLimit(boolean isAdditional, int known, int original, int value) {
55	aggregated.maxNewReals = scope.number.upperLimit	170	if(isAdditional) {
		171	return Math.max(original,value)
		172	} else {
		173	return Math.max(original,value-known)
		174	}
56	}	175	}
57	def dispatch setSpecification(StringTypeScope scope, TypeScopes aggregated, Ecore2Logic ecore2Logic, Ecore2Logic_Trace trace) {	176	def updateUpperLimit(boolean isAdditional, int known, int original, int value) {
58	aggregated.minNewStrings = scope.number.lowerLimit	177	if(isAdditional) {
59	aggregated.maxNewStrings = scope.number.upperLimit	178	return Math.min(original,value)
		179	} else {
		180	val target = if(value == Integer.MAX_VALUE) { Integer.MAX_VALUE } else {value-known}
		181	return Math.min(original,target)
		182	}
60	}	183	}
61		184
62	def dispatch getLowerLimit(IntervallNumber specification) {	185	def dispatch getLowerLimit(IntervallNumber specification) {
@@ -70,14 +193,12 @@ class ScopeLoader {
70	def dispatch getLowerLimit(RealEnumeration specification) { 0 }	193	def dispatch getLowerLimit(RealEnumeration specification) { 0 }
71	def dispatch getLowerLimit(StringEnumeration specification) { 0 }	194	def dispatch getLowerLimit(StringEnumeration specification) { 0 }
72	def dispatch getUpperLimit(IntervallNumber specification) {	195	def dispatch getUpperLimit(IntervallNumber specification) {
73	if(specification.isMaxUnlimited) return -1	196	if(specification.isMaxUnlimited) return Integer.MAX_VALUE
74	else return specification.maxNumber	197	else return specification.maxNumber
75	}	198	}
76	def dispatch getUpperLimit(ExactNumber specification) {	199	def dispatch getUpperLimit(ExactNumber specification) {
77	if(specification.isExactUnlimited) return -1	200	if(specification.isExactUnlimited) return Integer.MAX_VALUE
78	else return specification.exactNumber	201	else return specification.exactNumber
79	}	202	}
80	def dispatch getUpperLimit(IntEnumberation specification) { 0 }	203
81	def dispatch getUpperLimit(RealEnumeration specification) { 0 }
82	def dispatch getUpperLimit(StringEnumeration specification) { 0 }
83	} \ No newline at end of file	204	} \ No newline at end of file