1 files changed, 207 insertions, 0 deletions
diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_Support.xtend b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_Support.xtend
new file mode 100644
index 00000000..39896c27
--- /dev/null
+++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_Support.xtend
@@ -0,0 +1,207 @@
+package hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder
+import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSEquals
+import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSMultiplicity
+import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSReference
+import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSTerm
+import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSVariableDeclaration
+import hu.bme.mit.inf.dslreasoner.alloyLanguage.AlloyLanguageFactory
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.BoolTypeReference
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.QuantifiedExpression
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Term
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeReference
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable
+import java.util.ArrayList
+import java.util.HashMap
+import java.util.List
+import java.util.Map
+import org.eclipse.emf.ecore.util.EcoreUtil
+class Logic2AlloyLanguageMapper_Support {
+        private val extension AlloyLanguageFactory factory = AlloyLanguageFactory.eINSTANCE
+        
+        /// ID handling
+        def protected String toIDMultiple(String... ids) {
+                ids.map[it.split("\\s+").join("'")].join("'")
+        }
+        
+        def protected  String toID(String ids) {
+                ids.split("\\s+").join("'")
+        }
+        def protected  String toID(List<String> ids) {
+                ids.map[it.split("\\s+").join("'")].join("'")
+        }
+        
+        /// Support functions
+        
+        def protected getBooleanType(Logic2AlloyLanguageMapperTrace trace) {
+                if(trace.boolType!=null) {
+                        return trace.boolType
+                } else {
+                        trace.boolType = createALSEnumDeclaration => [
+                                it.name = toID(#["util","boolean"])
+                                trace.boolTrue = createALSEnumLiteral =>[it.name=toID(#["util","boolean","true"])]
+                                it.literal += trace.boolTrue
+                                trace.boolFalse = createALSEnumLiteral =>[it.name=toID(#["util","boolean","false"])]
+                                it.literal += trace.boolFalse
+                        ]
+                        trace.specification.enumDeclarations+=trace.boolType
+                        return trace.boolType
+                }
+        }
+        def protected getBooleanTrue(Logic2AlloyLanguageMapperTrace trace) {
+                getBooleanType(trace)
+                return trace.boolTrue   
+        }
+        def protected getBooleanFalse(Logic2AlloyLanguageMapperTrace trace) {
+                getBooleanType(trace)
+                return trace.boolFalse
+        }
+        
+        def protected booleanToLogicValue(ALSTerm boolReference, Logic2AlloyLanguageMapperTrace trace) {
+                //println((boolReference as ALSReference).referred)
+                createALSEquals => [
+                        leftOperand = EcoreUtil.copy(boolReference)
+                        rightOperand = createALSReference => [referred = getBooleanTrue(trace)]
+                ]
+        }
+        def protected booleanToEnumValue(ALSTerm value, Logic2AlloyLanguageMapperTrace trace) {
+                if(value instanceof ALSEquals) {
+                        val rightOperand = value.rightOperand
+                        if(rightOperand instanceof ALSReference) {
+                                if(rightOperand.referred == getBooleanTrue(trace)) {
+                                        return value.leftOperand
+                                }
+                        }
+                }
+                return value;
+        }
+        def protected prepareParameterOfSymbolicReference(TypeReference type, ALSTerm term, Logic2AlloyLanguageMapperTrace trace) {
+                if(type instanceof BoolTypeReference) {
+                        return booleanToEnumValue(term,trace)
+                }
+                else return term
+        }
+        def protected postprocessResultOfSymbolicReference(TypeReference type, ALSTerm term, Logic2AlloyLanguageMapperTrace trace) {
+                if(type instanceof BoolTypeReference) {
+                        return booleanToLogicValue(term,trace)
+                }
+                else return term
+        }
+         
+        def protected ALSTerm unfoldAnd(List<? extends ALSTerm> operands) {
+                if(operands.size == 1) { return operands.head }
+                else if(operands.size > 1) { return createALSAnd=>[
+                        leftOperand=operands.head
+                        rightOperand=operands.subList(1,operands.size).unfoldAnd
+                ]}
+                else throw new UnsupportedOperationException('''Logic operator with 0 operands!''')
+        }
+        
+        def protected ALSTerm unfoldOr(List<? extends ALSTerm> operands, Logic2AlloyLanguageMapperTrace trace) {
+                if(operands.size == 0) { return unfoldTrueStatement(trace)}
+                else if(operands.size == 1) { return operands.head }
+                else if(operands.size > 1) { return createALSOr=>[
+                        leftOperand=operands.head
+                        rightOperand=unfoldOr(operands.subList(1,operands.size),trace)
+                ]}
+                //else throw new UnsupportedOperationException('''Logic operator with 0 operands!''')
+        }
+        
+        protected def unfoldTrueStatement(Logic2AlloyLanguageMapperTrace trace) {
+                createALSEquals => [
+                                it.leftOperand = createALSReference => [it.referred = getBooleanTrue(trace)]
+                                it.rightOperand = createALSReference => [it.referred = getBooleanTrue(trace)]
+                        ]
+        }
+        
+        protected def unfoldTFalseStatement(Logic2AlloyLanguageMapper m, Logic2AlloyLanguageMapperTrace trace) {
+                createALSEquals => [
+                                it.leftOperand = createALSReference => [it.referred = getBooleanTrue(trace)]
+                                it.rightOperand = createALSReference => [it.referred = getBooleanTrue(trace)]
+                        ]
+        }
+        
+        def protected ALSTerm unfoldPlus(List<? extends ALSTerm> operands) {
+                if(operands.size == 1) { return operands.head }
+                else if(operands.size > 1) { return createALSPlus=>[
+                        leftOperand=operands.head
+                        rightOperand=operands.subList(1,operands.size).unfoldPlus
+                ]}
+                else return createALSNone
+        }
+        
+        def protected ALSTerm unfoldIntersection(List<? extends ALSTerm> operands) {
+                if(operands.size == 1) { return operands.head }
+                else if(operands.size > 1) { return createALSIntersection=>[
+                        leftOperand=operands.head
+                        rightOperand=operands.subList(1,operands.size).unfoldIntersection
+                ]}
+                else throw new UnsupportedOperationException('''Logic operator with 0 operands!''')
+        }
+        
+        def protected ALSTerm unfoldDistinctTerms(Logic2AlloyLanguageMapper m, List<Term> operands, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) {
+                if(operands.size == 1) { return m.transformTerm(operands.head,trace,variables) }
+                else if(operands.size > 1) {
+                        val notEquals = new ArrayList<ALSTerm>(operands.size*operands.size/2)
+                        for(i:0..<operands.size) {
+                                for(j: i+1..<operands.size) {
+                                        notEquals+=createALSNotEquals=>[
+                                                leftOperand = m.transformTerm(operands.get(i),trace,variables)
+                                                rightOperand = m.transformTerm(operands.get(j),trace,variables)
+                                        ]
+                                }
+                        }
+                        return notEquals.unfoldAnd
+                 }
+                else throw new UnsupportedOperationException('''Logic operator with 0 operands!''')
+        }
+        
+        def protected ALSTerm unfoldReferenceDirectProduct(Logic2AlloyLanguageMapper m, List<TypeReference> references,Logic2AlloyLanguageMapperTrace trace) {
+                if(references.size == 1) return m.transformTypeReference(references.head,trace)
+                else if(references.size > 1) return createALSDirectProduct => [
+                        it.leftOperand = m.transformTypeReference(references.head,trace)
+                        it.rightOperand = unfoldReferenceDirectProduct(m,references.subList(1,references.size),trace)
+                ]
+                else throw new UnsupportedOperationException
+        }
+        
+        def protected ALSTerm unfoldDotJoin(Logic2AlloyLanguageMapper m, List<Term> elements, ALSTerm target, Logic2AlloyLanguageMapperTrace trace,
+                Map<Variable, ALSVariableDeclaration> variables) {
+                if (elements.size == 1) {
+                        return createALSJoin => [
+                                it.leftOperand = m.transformTerm(elements.head,trace, variables)
+                                it.rightOperand = target
+                        ]
+                } else if (elements.size > 1) {
+                        return createALSJoin => [
+                                it.leftOperand = m.transformTerm(elements.last,trace, variables)
+                                it.rightOperand = m.unfoldDotJoin(elements.subList(0, elements.size - 1), target, trace, variables)
+                        ]
+                } else
+                        throw new UnsupportedOperationException
+        }
+        
+        def protected ALSTerm unfoldTermDirectProduct(Logic2AlloyLanguageMapper m, List<Term> references,Logic2AlloyLanguageMapperTrace trace,Map<Variable, ALSVariableDeclaration> variables) {
+                if(references.size == 1) return m.transformTerm(references.head,trace,variables)
+                else if(references.size > 1) return createALSDirectProduct => [
+                        it.leftOperand = m.transformTerm(references.head,trace,variables)
+                        it.rightOperand = unfoldTermDirectProduct(m,references.subList(1,references.size),trace, variables)
+                ]
+                else throw new UnsupportedOperationException
+        }
+        
+        def protected createQuantifiedExpression(Logic2AlloyLanguageMapper m, QuantifiedExpression q, ALSMultiplicity multiplicity, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) {
+                val variableMap = q.quantifiedVariables.toInvertedMap[v | createALSVariableDeclaration=> [
+                                it.name = toID(v.name)
+                                it.range = m.transformTypeReference(v.range,trace) ]]
+                        
+                createALSQuantifiedEx=>[
+                        it.type = multiplicity
+                        it.variables += variableMap.values
+                        it.expression = m.transformTerm(q.expression,trace,variables.withAddition(variableMap))
+                ]
+        }
+        
+        def protected withAddition(Map<Variable, ALSVariableDeclaration> v1, Map<Variable, ALSVariableDeclaration> v2) { new HashMap(v1) => [putAll(v2)] }
+}
+\ 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/Logic2AlloyLanguageMapper_Support.xtend b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_Support.xtend new file mode 100644 index 00000000..39896c27 --- /dev/null +++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_Support.xtend
@@ -0,0 +1,207 @@
	1	package hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder
	2
	3	import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSEquals
	4	import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSMultiplicity
	5	import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSReference
	6	import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSTerm
	7	import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSVariableDeclaration
	8	import hu.bme.mit.inf.dslreasoner.alloyLanguage.AlloyLanguageFactory
	9	import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.BoolTypeReference
	10	import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.QuantifiedExpression
	11	import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Term
	12	import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeReference
	13	import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable
	14	import java.util.ArrayList
	15	import java.util.HashMap
	16	import java.util.List
	17	import java.util.Map
	18	import org.eclipse.emf.ecore.util.EcoreUtil
	19
	20	class Logic2AlloyLanguageMapper_Support {
	21	private val extension AlloyLanguageFactory factory = AlloyLanguageFactory.eINSTANCE
	22
	23	/// ID handling
	24	def protected String toIDMultiple(String... ids) {
	25	ids.map[it.split("\\s+").join("'")].join("'")
	26	}
	27
	28	def protected String toID(String ids) {
	29	ids.split("\\s+").join("'")
	30	}
	31	def protected String toID(List<String> ids) {
	32	ids.map[it.split("\\s+").join("'")].join("'")
	33	}
	34
	35	/// Support functions
	36
	37	def protected getBooleanType(Logic2AlloyLanguageMapperTrace trace) {
	38	if(trace.boolType!=null) {
	39	return trace.boolType
	40	} else {
	41	trace.boolType = createALSEnumDeclaration => [
	42	it.name = toID(#["util","boolean"])
	43	trace.boolTrue = createALSEnumLiteral =>[it.name=toID(#["util","boolean","true"])]
	44	it.literal += trace.boolTrue
	45	trace.boolFalse = createALSEnumLiteral =>[it.name=toID(#["util","boolean","false"])]
	46	it.literal += trace.boolFalse
	47	]
	48	trace.specification.enumDeclarations+=trace.boolType
	49	return trace.boolType
	50	}
	51	}
	52	def protected getBooleanTrue(Logic2AlloyLanguageMapperTrace trace) {
	53	getBooleanType(trace)
	54	return trace.boolTrue
	55	}
	56	def protected getBooleanFalse(Logic2AlloyLanguageMapperTrace trace) {
	57	getBooleanType(trace)
	58	return trace.boolFalse
	59	}
	60
	61	def protected booleanToLogicValue(ALSTerm boolReference, Logic2AlloyLanguageMapperTrace trace) {
	62	//println((boolReference as ALSReference).referred)
	63	createALSEquals => [
	64	leftOperand = EcoreUtil.copy(boolReference)
	65	rightOperand = createALSReference => [referred = getBooleanTrue(trace)]
	66	]
	67	}
	68	def protected booleanToEnumValue(ALSTerm value, Logic2AlloyLanguageMapperTrace trace) {
	69	if(value instanceof ALSEquals) {
	70	val rightOperand = value.rightOperand
	71	if(rightOperand instanceof ALSReference) {
	72	if(rightOperand.referred == getBooleanTrue(trace)) {
	73	return value.leftOperand
	74	}
	75	}
	76	}
	77	return value;
	78	}
	79	def protected prepareParameterOfSymbolicReference(TypeReference type, ALSTerm term, Logic2AlloyLanguageMapperTrace trace) {
	80	if(type instanceof BoolTypeReference) {
	81	return booleanToEnumValue(term,trace)
	82	}
	83	else return term
	84	}
	85	def protected postprocessResultOfSymbolicReference(TypeReference type, ALSTerm term, Logic2AlloyLanguageMapperTrace trace) {
	86	if(type instanceof BoolTypeReference) {
	87	return booleanToLogicValue(term,trace)
	88	}
	89	else return term
	90	}
	91
	92	def protected ALSTerm unfoldAnd(List<? extends ALSTerm> operands) {
	93	if(operands.size == 1) { return operands.head }
	94	else if(operands.size > 1) { return createALSAnd=>[
	95	leftOperand=operands.head
	96	rightOperand=operands.subList(1,operands.size).unfoldAnd
	97	]}
	98	else throw new UnsupportedOperationException('''Logic operator with 0 operands!''')
	99	}
	100
	101	def protected ALSTerm unfoldOr(List<? extends ALSTerm> operands, Logic2AlloyLanguageMapperTrace trace) {
	102	if(operands.size == 0) { return unfoldTrueStatement(trace)}
	103	else if(operands.size == 1) { return operands.head }
	104	else if(operands.size > 1) { return createALSOr=>[
	105	leftOperand=operands.head
	106	rightOperand=unfoldOr(operands.subList(1,operands.size),trace)
	107	]}
	108	//else throw new UnsupportedOperationException('''Logic operator with 0 operands!''')
	109	}
	110
	111	protected def unfoldTrueStatement(Logic2AlloyLanguageMapperTrace trace) {
	112	createALSEquals => [
	113	it.leftOperand = createALSReference => [it.referred = getBooleanTrue(trace)]
	114	it.rightOperand = createALSReference => [it.referred = getBooleanTrue(trace)]
	115	]
	116	}
	117
	118	protected def unfoldTFalseStatement(Logic2AlloyLanguageMapper m, Logic2AlloyLanguageMapperTrace trace) {
	119	createALSEquals => [
	120	it.leftOperand = createALSReference => [it.referred = getBooleanTrue(trace)]
	121	it.rightOperand = createALSReference => [it.referred = getBooleanTrue(trace)]
	122	]
	123	}
	124
	125	def protected ALSTerm unfoldPlus(List<? extends ALSTerm> operands) {
	126	if(operands.size == 1) { return operands.head }
	127	else if(operands.size > 1) { return createALSPlus=>[
	128	leftOperand=operands.head
	129	rightOperand=operands.subList(1,operands.size).unfoldPlus
	130	]}
	131	else return createALSNone
	132	}
	133
	134	def protected ALSTerm unfoldIntersection(List<? extends ALSTerm> operands) {
	135	if(operands.size == 1) { return operands.head }
	136	else if(operands.size > 1) { return createALSIntersection=>[
	137	leftOperand=operands.head
	138	rightOperand=operands.subList(1,operands.size).unfoldIntersection
	139	]}
	140	else throw new UnsupportedOperationException('''Logic operator with 0 operands!''')
	141	}
	142
	143	def protected ALSTerm unfoldDistinctTerms(Logic2AlloyLanguageMapper m, List<Term> operands, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) {
	144	if(operands.size == 1) { return m.transformTerm(operands.head,trace,variables) }
	145	else if(operands.size > 1) {
	146	val notEquals = new ArrayList<ALSTerm>(operands.size*operands.size/2)
	147	for(i:0..<operands.size) {
	148	for(j: i+1..<operands.size) {
	149	notEquals+=createALSNotEquals=>[
	150	leftOperand = m.transformTerm(operands.get(i),trace,variables)
	151	rightOperand = m.transformTerm(operands.get(j),trace,variables)
	152	]
	153	}
	154	}
	155	return notEquals.unfoldAnd
	156	}
	157	else throw new UnsupportedOperationException('''Logic operator with 0 operands!''')
	158	}
	159
	160	def protected ALSTerm unfoldReferenceDirectProduct(Logic2AlloyLanguageMapper m, List<TypeReference> references,Logic2AlloyLanguageMapperTrace trace) {
	161	if(references.size == 1) return m.transformTypeReference(references.head,trace)
	162	else if(references.size > 1) return createALSDirectProduct => [
	163	it.leftOperand = m.transformTypeReference(references.head,trace)
	164	it.rightOperand = unfoldReferenceDirectProduct(m,references.subList(1,references.size),trace)
	165	]
	166	else throw new UnsupportedOperationException
	167	}
	168
	169	def protected ALSTerm unfoldDotJoin(Logic2AlloyLanguageMapper m, List<Term> elements, ALSTerm target, Logic2AlloyLanguageMapperTrace trace,
	170	Map<Variable, ALSVariableDeclaration> variables) {
	171	if (elements.size == 1) {
	172	return createALSJoin => [
	173	it.leftOperand = m.transformTerm(elements.head,trace, variables)
	174	it.rightOperand = target
	175	]
	176	} else if (elements.size > 1) {
	177	return createALSJoin => [
	178	it.leftOperand = m.transformTerm(elements.last,trace, variables)
	179	it.rightOperand = m.unfoldDotJoin(elements.subList(0, elements.size - 1), target, trace, variables)
	180	]
	181	} else
	182	throw new UnsupportedOperationException
	183	}
	184
	185	def protected ALSTerm unfoldTermDirectProduct(Logic2AlloyLanguageMapper m, List<Term> references,Logic2AlloyLanguageMapperTrace trace,Map<Variable, ALSVariableDeclaration> variables) {
	186	if(references.size == 1) return m.transformTerm(references.head,trace,variables)
	187	else if(references.size > 1) return createALSDirectProduct => [
	188	it.leftOperand = m.transformTerm(references.head,trace,variables)
	189	it.rightOperand = unfoldTermDirectProduct(m,references.subList(1,references.size),trace, variables)
	190	]
	191	else throw new UnsupportedOperationException
	192	}
	193
	194	def protected createQuantifiedExpression(Logic2AlloyLanguageMapper m, QuantifiedExpression q, ALSMultiplicity multiplicity, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) {
	195	val variableMap = q.quantifiedVariables.toInvertedMap[v \| createALSVariableDeclaration=> [
	196	it.name = toID(v.name)
	197	it.range = m.transformTypeReference(v.range,trace) ]]
	198
	199	createALSQuantifiedEx=>[
	200	it.type = multiplicity
	201	it.variables += variableMap.values
	202	it.expression = m.transformTerm(q.expression,trace,variables.withAddition(variableMap))
	203	]
	204	}
	205
	206	def protected withAddition(Map<Variable, ALSVariableDeclaration> v1, Map<Variable, ALSVariableDeclaration> v2) { new HashMap(v1) => [putAll(v2)] }
	207	} \ No newline at end of file