1 files changed, 72 insertions, 30 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 cbd56abb..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
@@ -5,22 +5,21 @@ 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 {
        val extension AlloyLanguageFactory factory = AlloyLanguageFactory.eINSTANCE
        val Logic2AlloyLanguageMapper_Support support = new Logic2AlloyLanguageMapper_Support;
        val Logic2AlloyLanguageMapper_TypeMapper typeMapper;
+        val Logic2AlloyLanguageMapper_TypeScopeMapping typeScopeMapping;
        
        new(Logic2AlloyLanguageMapper_TypeMapper typeMapper) {
                this.typeMapper = typeMapper
+                this.typeScopeMapping = new Logic2AlloyLanguageMapper_AsConstraint(typeMapper)
        }
        
        def transformRunCommand(Logic2AlloyLanguageMapper mapper, ALSDocument specification, Logic2AlloyLanguageMapperTrace trace, AlloySolverConfiguration config)
@@ -38,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 => [
@@ -67,9 +85,25 @@ class RunCommandMapper {
                                it.number = typeMapper.getUndefinedSupertypeScope(config.typeScopes.maxNewElements,trace) 
                                it.exactly = (config.typeScopes.maxNewElements == config.typeScopes.minNewElements)
                        ]
-                        setIntegerScope(specification,config,it)
+                        
-                        setStringScope(specification,config,it)
                ]
+                
+                for(upperLimit : config.typeScopes.maxNewElementsByType.entrySet) {
+                        val limit = upperLimit.value
+                        if(limit != LogicSolverConfiguration::Unlimited) {
+                                this.typeScopeMapping.addUpperMultiplicity(specification,upperLimit.key,limit,mapper,trace)
+                        }
+                }
+                
+                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) {
@@ -79,7 +113,11 @@ class RunCommandMapper {
                        if(config.typeScopes.maxNewStrings == 0) {
                                it.typeScopes += createALSStringScope => [it.number = 0]
                        } else {
-                                throw new UnsupportedOperationException('''A string scope have to be specified for Alloy!''')
+                                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!''')
+                                }
                        }
                }
        }
@@ -99,13 +137,17 @@ class RunCommandMapper {
                        }
                } else {
                        // If the scope is limited, collect the integers in the problem and the scope,...
-                        val maxIntScope = config.typeScopes.maxNewIntegers
+                        //val maxIntScope = config.typeScopes.maxNewIntegers
-                        val minIntScope = config.typeScopes.minNewIntegers
+                        //val minIntScope = config.typeScopes.minNewIntegers
                        val knownIntegers = config.typeScopes.knownIntegers
-                        val integersInProblem = specification.eAllContents.filter(ALSNumberLiteral).map[it.value]
+                        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 = #[minIntScope,knownIntegers.min,integersInProblem.min].min
+                        val min = #[minKnownInteger,minIntegerInProblem].min
-                        val max = #[maxIntScope,knownIntegers.max,integersInProblem.max].max
+                        val max = #[maxKnownInteger,maxIntegerInProblem].max
                        //val abs = Math.max(Math.abs(min),Math.abs(max))

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 cbd56abb..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
@@ -5,22 +5,21 @@ 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	6	import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSNumberLiteral
7	import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSRunCommand	7	import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSRunCommand
		8	import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSString
8	import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSTerm	9	import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSTerm
9	import hu.bme.mit.inf.dslreasoner.alloyLanguage.AlloyLanguageFactory	10	import hu.bme.mit.inf.dslreasoner.alloyLanguage.AlloyLanguageFactory
10	import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration	11	import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration
11	import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition
12	import java.util.LinkedList
13	import java.util.List	12	import java.util.List
14		13
15	import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*
16
17	class RunCommandMapper {	14	class RunCommandMapper {
18	val extension AlloyLanguageFactory factory = AlloyLanguageFactory.eINSTANCE	15	val extension AlloyLanguageFactory factory = AlloyLanguageFactory.eINSTANCE
19	val Logic2AlloyLanguageMapper_Support support = new Logic2AlloyLanguageMapper_Support;	16	val Logic2AlloyLanguageMapper_Support support = new Logic2AlloyLanguageMapper_Support;
20	val Logic2AlloyLanguageMapper_TypeMapper typeMapper;	17	val Logic2AlloyLanguageMapper_TypeMapper typeMapper;
		18	val Logic2AlloyLanguageMapper_TypeScopeMapping typeScopeMapping;
21		19
22	new(Logic2AlloyLanguageMapper_TypeMapper typeMapper) {	20	new(Logic2AlloyLanguageMapper_TypeMapper typeMapper) {
23	this.typeMapper = typeMapper	21	this.typeMapper = typeMapper
		22	this.typeScopeMapping = new Logic2AlloyLanguageMapper_AsConstraint(typeMapper)
24	}	23	}
25		24
26	def transformRunCommand(Logic2AlloyLanguageMapper mapper, ALSDocument specification, Logic2AlloyLanguageMapperTrace trace, AlloySolverConfiguration config)	25	def transformRunCommand(Logic2AlloyLanguageMapper mapper, ALSDocument specification, Logic2AlloyLanguageMapperTrace trace, AlloySolverConfiguration config)
@@ -38,28 +37,47 @@ class RunCommandMapper {
38	it.term = support.unfoldAnd(equals)	37	it.term = support.unfoldAnd(equals)
39	]	38	]
40	}	39	}
41	val typeScopes = new LinkedList	40
42	for(definedScope : config.typeScopes.maxNewElementsByType.entrySet) {	41	/*
43	val key = definedScope.key	42	val upperLimits = new LinkedList
44	val amount = definedScope.value	43	val lowerLimits = new LinkedList
45	val exactly = config.typeScopes.minNewElementsByType.containsKey(key) && config.typeScopes.minNewElementsByType.get(key) === amount	44
46		45	/*val typesWithScopeConstraint = config.typeScopes.maxNewElementsByType.keySet + config.typeScopes.minNewElementsByType.keySet
47	val existing = key.transitiveClosureStar[it.subtypes].filter(TypeDefinition).map[elements].flatten.toSet	46	for(type : typesWithScopeConstraint) {
48	if(amount == 0 && exactly) {	47	val max = if(config.typeScopes.maxNewElementsByType.containsKey(type)) {
49	specification.factDeclarations += createALSFactDeclaration => [	48	config.typeScopes.maxNewElementsByType.get(type)
50	it.term = createALSEquals => [	49	} else {
51	it.leftOperand = support.unfoldPlus(typeMapper.transformTypeReference(key,mapper,trace).map[t\|createALSReference => [it.referred = t]].toList)	50	LogicSolverConfiguration::Unlimited
52	it.rightOperand = support.unfoldPlus( existing.map[typeMapper.transformReference(it,trace)].toList )	51	}
53	]	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 )
54	]	66	]
55	}	67	]
56	val int n = existing.size-amount	68	} else if(max !== LogicSolverConfiguration::Unlimited) {
57	typeScopes += createALSSigScope => [	69	upperLimits += createALSSigScope => [
58	it.type = typeMapper.transformTypeReference(key,mapper,trace).head	70	it.type = typeMapper.transformTypeReference(type,mapper,trace).head
59	it.number = n	71	it.number = max
60	it.exactly =exactly	72	it.exactly =exactly
61	]	73	]
		74	} else {
		75	// do nothing
		76	}
		77	if(min != 0 && ! exactly) {
		78	lowerLimits += type->min
62	}	79	}
		80	}*/
63		81
64	specification.runCommand = createALSRunCommand => [	82	specification.runCommand = createALSRunCommand => [
65	it.typeScopes+= createALSSigScope => [	83	it.typeScopes+= createALSSigScope => [
@@ -67,9 +85,25 @@ class RunCommandMapper {
67	it.number = typeMapper.getUndefinedSupertypeScope(config.typeScopes.maxNewElements,trace)	85	it.number = typeMapper.getUndefinedSupertypeScope(config.typeScopes.maxNewElements,trace)
68	it.exactly = (config.typeScopes.maxNewElements == config.typeScopes.minNewElements)	86	it.exactly = (config.typeScopes.maxNewElements == config.typeScopes.minNewElements)
69	]	87	]
70	setIntegerScope(specification,config,it)	88
71	setStringScope(specification,config,it)
72	]	89	]
		90
		91	for(upperLimit : config.typeScopes.maxNewElementsByType.entrySet) {
		92	val limit = upperLimit.value
		93	if(limit != LogicSolverConfiguration::Unlimited) {
		94	this.typeScopeMapping.addUpperMultiplicity(specification,upperLimit.key,limit,mapper,trace)
		95	}
		96	}
		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)
73	}	107	}
74		108
75	protected def Boolean setStringScope(ALSDocument specification, AlloySolverConfiguration config, ALSRunCommand it) {	109	protected def Boolean setStringScope(ALSDocument specification, AlloySolverConfiguration config, ALSRunCommand it) {
@@ -79,7 +113,11 @@ class RunCommandMapper {
79	if(config.typeScopes.maxNewStrings == 0) {	113	if(config.typeScopes.maxNewStrings == 0) {
80	it.typeScopes += createALSStringScope => [it.number = 0]	114	it.typeScopes += createALSStringScope => [it.number = 0]
81	} else {	115	} else {
82	throw new UnsupportedOperationException('''A string scope have to be specified for Alloy!''')	116	if(specification.eAllContents.filter(ALSString).empty) {
		117	it.typeScopes += createALSStringScope => [it.number = 0]
		118	} else {
		119	throw new UnsupportedOperationException('''A string scope have to be specified for Alloy!''')
		120	}
83	}	121	}
84	}	122	}
85	}	123	}
@@ -99,13 +137,17 @@ class RunCommandMapper {
99	}	137	}
100	} else {	138	} else {
101	// If the scope is limited, collect the integers in the problem and the scope,...	139	// If the scope is limited, collect the integers in the problem and the scope,...
102	val maxIntScope = config.typeScopes.maxNewIntegers	140	//val maxIntScope = config.typeScopes.maxNewIntegers
103	val minIntScope = config.typeScopes.minNewIntegers	141	//val minIntScope = config.typeScopes.minNewIntegers
104	val knownIntegers = config.typeScopes.knownIntegers	142	val knownIntegers = config.typeScopes.knownIntegers
105	val integersInProblem = specification.eAllContents.filter(ALSNumberLiteral).map[it.value]	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 }
106	// And select the range of integers	148	// And select the range of integers
107	val min = #[minIntScope,knownIntegers.min,integersInProblem.min].min	149	val min = #[minKnownInteger,minIntegerInProblem].min
108	val max = #[maxIntScope,knownIntegers.max,integersInProblem.max].max	150	val max = #[maxKnownInteger,maxIntegerInProblem].max
109	//val abs = Math.max(Math.abs(min),Math.abs(max))	151	//val abs = Math.max(Math.abs(min),Math.abs(max))
110		152
111		153