diff options
author | 2019-10-25 04:15:39 -0400 | |
---|---|---|
committer | 2019-10-25 04:15:39 -0400 | |
commit | 25a4b1b53add70e268c3083682f8a3508c618ec2 (patch) | |
tree | 6d46e62be49cfe6c5640e2e9af80aae90da6a212 /Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_Support.xtend | |
parent | mid-measurement push (diff) | |
download | VIATRA-Generator-25a4b1b53add70e268c3083682f8a3508c618ec2.tar.gz VIATRA-Generator-25a4b1b53add70e268c3083682f8a3508c618ec2.tar.zst VIATRA-Generator-25a4b1b53add70e268c3083682f8a3508c618ec2.zip |
VAMPIRE: post-submission push
Diffstat (limited to 'Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_Support.xtend')
-rw-r--r-- | Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_Support.xtend | 207 |
1 files changed, 207 insertions, 0 deletions
diff --git a/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_Support.xtend b/Solvers/Alloy-Solver2/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..0b8d2857 --- /dev/null +++ b/Solvers/Alloy-Solver2/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 | ||