diff options
Diffstat (limited to 'Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/Logic2SmtMapper.xtend')
-rw-r--r-- | Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/Logic2SmtMapper.xtend | 1055 |
1 files changed, 1055 insertions, 0 deletions
diff --git a/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/Logic2SmtMapper.xtend b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/Logic2SmtMapper.xtend new file mode 100644 index 00000000..aad43716 --- /dev/null +++ b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/Logic2SmtMapper.xtend | |||
@@ -0,0 +1,1055 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.smt.reasoner | ||
2 | |||
3 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.TracedOutput | ||
4 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.TypeScopes | ||
5 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.And | ||
6 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Assertion | ||
7 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.BoolLiteral | ||
8 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.BoolTypeReference | ||
9 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference | ||
10 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ConstantDeclaration | ||
11 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ConstantDefinition | ||
12 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement | ||
13 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Distinct | ||
14 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Divison | ||
15 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Equals | ||
16 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Exists | ||
17 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Forall | ||
18 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Function | ||
19 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.FunctionDeclaration | ||
20 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.FunctionDefinition | ||
21 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.IfThenElse | ||
22 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Iff | ||
23 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Impl | ||
24 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.InstanceOf | ||
25 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.IntLiteral | ||
26 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.IntTypeReference | ||
27 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.LessOrEqualThan | ||
28 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.LessThan | ||
29 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Minus | ||
30 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Mod | ||
31 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.MoreOrEqualThan | ||
32 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.MoreThan | ||
33 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Multiply | ||
34 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Not | ||
35 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Or | ||
36 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Plus | ||
37 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.QuantifiedExpression | ||
38 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RealLiteral | ||
39 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RealTypeReference | ||
40 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation | ||
41 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration | ||
42 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition | ||
43 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.SymbolicValue | ||
44 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Term | ||
45 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable | ||
46 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem | ||
47 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTAnd | ||
48 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTAssertion | ||
49 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTBoolTypeReference | ||
50 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTComplexTypeReference | ||
51 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTDocument | ||
52 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTInput | ||
53 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTIntTypeReference | ||
54 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTOr | ||
55 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTQuantifiedExpression | ||
56 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTRealTypeReference | ||
57 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTReasoningTactic | ||
58 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTSortedVariable | ||
59 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTSymbolicValue | ||
60 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTTerm | ||
61 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTType | ||
62 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SmtLanguageFactory | ||
63 | import java.util.ArrayList | ||
64 | import java.util.HashMap | ||
65 | import java.util.LinkedHashMap | ||
66 | import java.util.LinkedList | ||
67 | import java.util.List | ||
68 | import java.util.Map | ||
69 | import org.eclipse.emf.ecore.EObject | ||
70 | import org.eclipse.emf.ecore.util.EcoreUtil | ||
71 | import org.eclipse.xtend.lib.annotations.Accessors | ||
72 | import org.eclipse.xtext.xbase.lib.Functions.Function0 | ||
73 | import org.eclipse.xtext.xbase.lib.Functions.Function1 | ||
74 | import org.eclipse.xtext.xbase.lib.Functions.Function2 | ||
75 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* | ||
76 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTFunctionDefinition | ||
77 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.ContainmentHierarchy | ||
78 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicProblemBuilder | ||
79 | |||
80 | class Logic2SmtMapper{ | ||
81 | val extension SmtLanguageFactory factory = SmtLanguageFactory.eINSTANCE | ||
82 | val Logic2SmtMapper_UnfoldingSupport unfolder = new Logic2SmtMapper_UnfoldingSupport | ||
83 | @Accessors val Logic2Smt_TypeMapper typeMapper; | ||
84 | |||
85 | LogicProblemBuilder b | ||
86 | |||
87 | new(Logic2Smt_TypeMapper typeMapper) { | ||
88 | this.typeMapper = typeMapper | ||
89 | } | ||
90 | |||
91 | public def TracedOutput<SMTDocument, Logic2SmtMapperTrace> transformProblem(LogicProblem problem, TypeScopes scope, SMTReasoningTactic strategy) { | ||
92 | val documentInput = createSMTInput => [getModelCommand = createSMTGetModelCommand] | ||
93 | if(strategy == null) documentInput.satCommand = createSMTSimpleSatCommand | ||
94 | else documentInput.satCommand = createSMTComplexSatCommand => [it.method = EcoreUtil.copy(strategy)] | ||
95 | |||
96 | val document = createSMTDocument => [input = documentInput] | ||
97 | val trace = new Logic2SmtMapperTrace => [ | ||
98 | it.forwardMapper = this | ||
99 | it.problem = problem | ||
100 | ] | ||
101 | // Trafo | ||
102 | this.typeMapper.transformTypes(documentInput,problem,trace, scope) | ||
103 | problem.functions.filter(FunctionDeclaration).forEach[it.transformFunctionDeclaration(documentInput,trace)] | ||
104 | problem.functions.filter(FunctionDefinition) .forEach[it.transformFunctionDefinition(documentInput,trace)] | ||
105 | problem.relations.filter(RelationDeclaration).forEach[it.transformRelationDeclaration(documentInput,trace)] | ||
106 | problem.relations.filter(RelationDefinition) .forEach[it.transformRelationDefinition(documentInput,trace)] | ||
107 | problem.constants.filter(ConstantDeclaration).forEach[it.transformConstantDeclaration(documentInput,trace)] | ||
108 | problem.constants.filter(ConstantDefinition) .forEach[it.transformConstantDefinition(documentInput,trace)] | ||
109 | |||
110 | problem.relations.filter(RelationDefinition).forEach[it.transformRelationDefinition_definition(documentInput,trace)] | ||
111 | documentInput.assertions += problem.assertions.map[transformAssertion(trace)] | ||
112 | // End trafo | ||
113 | |||
114 | document.input.assertions.forEach[it.value.nameAllUnnamedVariable] | ||
115 | document.input.functionDefinition.forEach[it.value.nameAllUnnamedVariable] | ||
116 | document.cleanDocument | ||
117 | return new TracedOutput(document,trace) | ||
118 | } | ||
119 | |||
120 | private def toID(String name) {name.split("\\s+").join("!") } | ||
121 | |||
122 | private def nameAllUnnamedVariable(SMTTerm root) { | ||
123 | var index = 1 | ||
124 | val unnamedVariables = root.eAllContents.filter(SMTSortedVariable).filter[it.name == null].toList | ||
125 | for(unnamedVariable : unnamedVariables) { | ||
126 | unnamedVariable.name = '''var«index++»''' | ||
127 | } | ||
128 | } | ||
129 | |||
130 | // def protected maxIntegerRageDefiniton(SMTInput documentInput) { | ||
131 | // val upperlimit = createSMTFunctionDeclaration | ||
132 | // } | ||
133 | |||
134 | def dispatch protected List<TypeConstraint> transformTypeReference(BoolTypeReference boolTypeReference, Logic2SmtMapperTrace trace) { | ||
135 | return #[new TypeConstraint(createSMTBoolTypeReference,null)] | ||
136 | } | ||
137 | def dispatch protected List<TypeConstraint> transformTypeReference(IntTypeReference intTypeReference, Logic2SmtMapperTrace trace) { | ||
138 | return #[new TypeConstraint(createSMTIntTypeReference,null)] | ||
139 | } | ||
140 | def dispatch protected List<TypeConstraint> transformTypeReference(RealTypeReference realTypeReference, Logic2SmtMapperTrace trace) { | ||
141 | return #[new TypeConstraint(createSMTRealTypeReference,null)] | ||
142 | } | ||
143 | def dispatch protected List<TypeConstraint> transformTypeReference(ComplexTypeReference complexTypeReference, Logic2SmtMapperTrace trace) { | ||
144 | return typeMapper.transformTypeReference(complexTypeReference.referred,trace) | ||
145 | } | ||
146 | |||
147 | /////////////////////////////////////////////////////// | ||
148 | // Definitions | ||
149 | /////////////////////////////////////////////////////// | ||
150 | |||
151 | def transformFunctionDeclaration(FunctionDeclaration function, SMTInput input, Logic2SmtMapperTrace trace) { | ||
152 | val parameterTypeCombinations = unfolder.getPermutations(function.parameters.map[x|transformTypeReference(x,trace)]) | ||
153 | val rangeTypeCombinations = function.range.transformTypeReference(trace) | ||
154 | |||
155 | if(rangeTypeCombinations.size == 1) { | ||
156 | val rangeType = rangeTypeCombinations.head | ||
157 | // Map it as function | ||
158 | var index = 1 | ||
159 | for(combination : parameterTypeCombinations) { | ||
160 | val nameWithIndex = if (parameterTypeCombinations.size > 1) | ||
161 | toID('''function «function.name.toID» «index++»''') | ||
162 | else | ||
163 | toID('''function «function.name.toID»''') | ||
164 | |||
165 | createFunctionDeclaration(function,nameWithIndex,combination,rangeType,true, input,trace) | ||
166 | } | ||
167 | } else { | ||
168 | // Map it as a relation | ||
169 | var index = 1 | ||
170 | for(combination : parameterTypeCombinations) { | ||
171 | val type2function = new HashMap | ||
172 | for(rangeType : rangeTypeCombinations) { | ||
173 | val nameWithIndex = toID('''function «function.name.toID» «index++»''') | ||
174 | val f = createFunctionDeclaration(function,nameWithIndex,combination,rangeType,false,input,trace) | ||
175 | type2function.put(rangeType,f) | ||
176 | } | ||
177 | // for all rangeTypes, there is | ||
178 | // 1. at least one range type that satisfies the relation | ||
179 | input.assertions+=createSMTAssertion => [ | ||
180 | it.value = createSMTForall => [f| | ||
181 | var paramIndex = 1 | ||
182 | for(param : combination) { | ||
183 | val paramName = '''p«paramIndex++»''' | ||
184 | val variable = createSMTSortedVariable => [ | ||
185 | it.name = paramName | ||
186 | it.range = param.type | ||
187 | ] | ||
188 | f.quantifiedVariables += variable | ||
189 | } | ||
190 | f.expression = createSMTOr => [ | ||
191 | operands+=rangeTypeCombinations.map[t| | ||
192 | createSMTExists => [ | ||
193 | val v = createSMTSortedVariable => [ | ||
194 | it.name = "r" | ||
195 | it.range = EcoreUtil.copy(t.type) | ||
196 | ] | ||
197 | it.quantifiedVariables += v | ||
198 | it.expression = createSMTSymbolicValue => [ | ||
199 | it.symbolicReference = type2function.get(t) | ||
200 | it.parameterSubstitutions += f.quantifiedVariables.map[fv| | ||
201 | createSMTSymbolicValue => [it.symbolicReference = fv] | ||
202 | ] | ||
203 | it.parameterSubstitutions += createSMTSymbolicValue => [it.symbolicReference = v] | ||
204 | ] | ||
205 | ] | ||
206 | ] | ||
207 | ] | ||
208 | ] | ||
209 | ] | ||
210 | // 2. at most one range type that satisfies the relation | ||
211 | // TODO a | ||
212 | } | ||
213 | } | ||
214 | } | ||
215 | |||
216 | private def createFunctionDeclaration( | ||
217 | Function function, | ||
218 | String nameWithIndex, | ||
219 | List<TypeConstraint> combination, | ||
220 | TypeConstraint rangeType, | ||
221 | boolean useFunction, | ||
222 | SMTInput input, | ||
223 | Logic2SmtMapperTrace trace | ||
224 | ) { | ||
225 | val smtFunction = if(useFunction) { | ||
226 | createSMTFunctionDeclaration => [ | ||
227 | it.name = nameWithIndex | ||
228 | it.parameters += combination.map[it.type] | ||
229 | it.range = rangeType.type | ||
230 | ] | ||
231 | } else { | ||
232 | createSMTFunctionDeclaration => [ | ||
233 | it.name = nameWithIndex | ||
234 | it.parameters += combination.map[it.type] | ||
235 | it.parameters += rangeType.type | ||
236 | it.range = createSMTBoolTypeReference | ||
237 | ] | ||
238 | } | ||
239 | |||
240 | val descriptor = new Descriptor<Function>((combination+#[rangeType]).toList.map[ | ||
241 | TypeDescriptor.createFromTypeReference(it.type)],function) | ||
242 | trace.functionMap.put(descriptor,smtFunction) | ||
243 | input.functionDeclarations += smtFunction | ||
244 | trace.functionUnfolding.put(function,#[descriptor]) | ||
245 | |||
246 | if(!useFunction) { | ||
247 | input.assertions += createSMTAssertion => [ | ||
248 | it.value = createSMTForall => [f| | ||
249 | var pi = 0 | ||
250 | for(param : combination) { | ||
251 | val variable = createSMTSortedVariable | ||
252 | variable.name = "p"+pi.toString | ||
253 | variable.range = EcoreUtil.copy(combination.get(pi).type) | ||
254 | f.quantifiedVariables+=variable | ||
255 | pi++ | ||
256 | } | ||
257 | val resultParam1 = createSMTSortedVariable => [ | ||
258 | it.name = "res1" | ||
259 | it.range = EcoreUtil.copy(rangeType.type) | ||
260 | ] | ||
261 | f.quantifiedVariables+=resultParam1 | ||
262 | val resultParam2 = createSMTSortedVariable => [ | ||
263 | it.name = "res2" | ||
264 | it.range = EcoreUtil.copy(rangeType.type) | ||
265 | ] | ||
266 | f.quantifiedVariables+=resultParam2 | ||
267 | f.expression = createSMTImpl => [ | ||
268 | it.leftOperand = createSMTAnd => [ | ||
269 | it.operands += createSMTSymbolicValue => [ | ||
270 | it.symbolicReference = smtFunction | ||
271 | it.parameterSubstitutions += (0..<combination.size).map[x| | ||
272 | createSMTSymbolicValue => [it.symbolicReference = f.quantifiedVariables.get(x)]] | ||
273 | it.parameterSubstitutions += createSMTSymbolicValue => [it.symbolicReference = resultParam1] | ||
274 | ] | ||
275 | it.operands += createSMTSymbolicValue => [ | ||
276 | it.symbolicReference = smtFunction | ||
277 | it.parameterSubstitutions += (0..<combination.size).map[x| | ||
278 | createSMTSymbolicValue => [it.symbolicReference = f.quantifiedVariables.get(x)]] | ||
279 | it.parameterSubstitutions += createSMTSymbolicValue => [it.symbolicReference = resultParam2] | ||
280 | ] | ||
281 | ] | ||
282 | it.rightOperand = createSMTEquals => [ | ||
283 | it.leftOperand = createSMTSymbolicValue => [it.symbolicReference = resultParam1] | ||
284 | it.rightOperand = createSMTSymbolicValue => [it.symbolicReference = resultParam2] | ||
285 | ] | ||
286 | ] | ||
287 | ] | ||
288 | ] | ||
289 | } | ||
290 | |||
291 | if(rangeType.constraint != null) { | ||
292 | input.assertions += createSMTAssertion => [ | ||
293 | it.value = createSMTForall => [f| | ||
294 | var pi = 0 | ||
295 | for(param : combination) { | ||
296 | val variable = createSMTSortedVariable | ||
297 | variable.name = "p"+pi.toString | ||
298 | variable.range = EcoreUtil.copy(combination.get(pi).type) | ||
299 | f.quantifiedVariables+=variable | ||
300 | pi++ | ||
301 | } | ||
302 | val resultParam = createSMTSortedVariable => [ | ||
303 | it.name = "res" | ||
304 | it.range = EcoreUtil.copy(rangeType.type) | ||
305 | ] | ||
306 | f.quantifiedVariables += resultParam | ||
307 | f.expression = createSMTImpl => [ | ||
308 | it.leftOperand = if(useFunction) | ||
309 | { | ||
310 | createSMTEquals => [ | ||
311 | leftOperand = createSMTSymbolicValue => [ | ||
312 | it.symbolicReference = smtFunction | ||
313 | it.parameterSubstitutions += (0..<combination.size).map[x| | ||
314 | createSMTSymbolicValue => [it.symbolicReference = f.quantifiedVariables.get(x)] | ||
315 | ] | ||
316 | ] | ||
317 | rightOperand = createSMTSymbolicValue => [it.symbolicReference = resultParam] | ||
318 | ] | ||
319 | } else { | ||
320 | createSMTSymbolicValue => [ | ||
321 | it.symbolicReference = smtFunction | ||
322 | it.parameterSubstitutions += (0..<combination.size).map[x| | ||
323 | createSMTSymbolicValue => [it.symbolicReference = f.quantifiedVariables.get(x)]] | ||
324 | it.parameterSubstitutions += createSMTSymbolicValue => [it.symbolicReference = resultParam] | ||
325 | ] | ||
326 | } | ||
327 | it.rightOperand = rangeType.constraint.apply(resultParam) | ||
328 | ] | ||
329 | ] | ||
330 | ] | ||
331 | } | ||
332 | return smtFunction | ||
333 | } | ||
334 | |||
335 | def transformFunctionDefinition(FunctionDefinition function, SMTInput input, Logic2SmtMapperTrace trace) { | ||
336 | throw new UnsupportedOperationException("TODO: auto-generated method stub") | ||
337 | } | ||
338 | |||
339 | def protected transformRelationDeclaration(RelationDeclaration relation, SMTInput input, Logic2SmtMapperTrace trace) { | ||
340 | val parameterTypeCombinations = unfolder.getPermutations(relation.parameters.map[x|transformTypeReference(x,trace)]) | ||
341 | var relationIndex = 1 | ||
342 | val unfolding = new ArrayList(parameterTypeCombinations.size) | ||
343 | for(parameterTypeCombination : parameterTypeCombinations) { | ||
344 | /// Create a name for the relation | ||
345 | val nameWithIndex = if (parameterTypeCombinations.size > 1) | ||
346 | toID('''relation «relation.name.toID» «relationIndex++»''') | ||
347 | else | ||
348 | toID('''relation «relation.name.toID»''') | ||
349 | |||
350 | // Adding an unfolded relation | ||
351 | val smtRelation = createSMTFunctionDeclaration => [ | ||
352 | name = nameWithIndex | ||
353 | parameters+= parameterTypeCombination.map[typeConstraint | EcoreUtil.copy(typeConstraint.type)] | ||
354 | range = createSMTBoolTypeReference | ||
355 | ] | ||
356 | val Descriptor<Relation> descriptor = new Descriptor<Relation>(parameterTypeCombination.map[ | ||
357 | TypeDescriptor.createFromTypeReference(it.type)],relation) | ||
358 | trace.relationMap.put(descriptor,smtRelation) | ||
359 | input.functionDeclarations += smtRelation | ||
360 | unfolding += descriptor | ||
361 | |||
362 | // If there is a type constraint | ||
363 | if(parameterTypeCombination.exists[it.constraint != null]) { | ||
364 | // create a constraint that specifies that the relation contains elemenents with the required properties | ||
365 | val and = createSMTAnd | ||
366 | val rel = createSMTSymbolicValue => [it.symbolicReference = smtRelation] | ||
367 | val forall = createSMTForall => [ | ||
368 | it.expression = createSMTImpl => [ | ||
369 | it.leftOperand = rel | ||
370 | it.rightOperand = and | ||
371 | ] | ||
372 | ] | ||
373 | var paramIndex = 0 | ||
374 | for(param : parameterTypeCombination) { | ||
375 | val paramName = '''p«paramIndex++»''' | ||
376 | val variable = createSMTSortedVariable => [ | ||
377 | it.name = paramName | ||
378 | it.range = param.type | ||
379 | ] | ||
380 | forall.quantifiedVariables += variable | ||
381 | rel.parameterSubstitutions += createSMTSymbolicValue => [it.symbolicReference = variable] | ||
382 | if(param.constraint != null) { | ||
383 | and.operands+=param.constraint.apply(variable) | ||
384 | } | ||
385 | } | ||
386 | input.assertions += createSMTAssertion => [ | ||
387 | it.value = forall | ||
388 | ] | ||
389 | } | ||
390 | } | ||
391 | trace.relationUnfolding.put(relation,unfolding) | ||
392 | } | ||
393 | def protected transformRelationDefinition(RelationDefinition relation, SMTInput input, Logic2SmtMapperTrace trace) { | ||
394 | val parameterTypeCombinations = unfolder.getPermutations(relation.variables.map[x|transformTypeReference(x.range,trace)]).toList | ||
395 | var relationIndex = 1 | ||
396 | val unfolding = new ArrayList(parameterTypeCombinations.size) | ||
397 | for(parameterTypeCombination : parameterTypeCombinations) { | ||
398 | /// Create a name for the relation | ||
399 | val nameWithIndex = if (parameterTypeCombinations.size > 1) | ||
400 | toID('''relation «relation.name.toID» «relationIndex++»''') | ||
401 | else | ||
402 | toID('''relation «relation.name.toID»''') | ||
403 | |||
404 | // creating an unfolded relation | ||
405 | val smtRelation = createSMTFunctionDefinition => [ | ||
406 | name = nameWithIndex | ||
407 | range = createSMTBoolTypeReference | ||
408 | ] | ||
409 | /* | ||
410 | // adding variables as parameters | ||
411 | val Map<Variable, SMTSortedVariable> variables = new HashMap | ||
412 | var paramIndex = 0 | ||
413 | val constraintList = new LinkedList | ||
414 | for(param : parameterTypeCombination) { | ||
415 | val paramName = relation.variables.get(paramIndex).name.toID | ||
416 | val variable = createSMTSortedVariable => [ | ||
417 | it.name = paramName | ||
418 | it.range = param.type | ||
419 | ] | ||
420 | |||
421 | smtRelation.parameters+=variable | ||
422 | variables.put(relation.variables.get(paramIndex),variable) | ||
423 | if(param.constraint != null) { | ||
424 | constraintList+=param.constraint.apply(variable) | ||
425 | } | ||
426 | paramIndex++ | ||
427 | } | ||
428 | val definition = transformTerm(relation.value,trace,variables) | ||
429 | if(constraintList.empty) { | ||
430 | smtRelation.value = definition.expectLogic.value | ||
431 | } else if(constraintList.size == 1) { | ||
432 | smtRelation.value = createSMTAnd => [ | ||
433 | it.operands += constraintList.head | ||
434 | it.operands += definition.expectLogic.value | ||
435 | ] | ||
436 | } else { | ||
437 | smtRelation.value = createSMTAnd => [ | ||
438 | it.operands += createSMTAnd => [operands += constraintList] | ||
439 | it.operands += definition.expectLogic.value | ||
440 | ] | ||
441 | } | ||
442 | */ | ||
443 | // | ||
444 | val Descriptor<Relation> descriptor = new Descriptor<Relation>(parameterTypeCombination.map[ | ||
445 | TypeDescriptor.createFromTypeReference(it.type)],relation) | ||
446 | trace.relationMap.put(descriptor,smtRelation) | ||
447 | input.functionDefinition += smtRelation | ||
448 | unfolding += descriptor | ||
449 | } | ||
450 | trace.relationUnfolding.put(relation,unfolding) | ||
451 | } | ||
452 | def transformRelationDefinition_definition(RelationDefinition relation, SMTInput input, Logic2SmtMapperTrace trace) { | ||
453 | val parameterTypeCombinations = unfolder.getPermutations(relation.variables.map[x|transformTypeReference(x.range,trace)]).toList | ||
454 | for(parameterTypeCombination : parameterTypeCombinations) { | ||
455 | val Descriptor<Relation> descriptor = new Descriptor<Relation>(parameterTypeCombination.map[ | ||
456 | TypeDescriptor.createFromTypeReference(it.type)],relation) | ||
457 | val smtRelation = descriptor.lookup(trace.relationMap) as SMTFunctionDefinition | ||
458 | |||
459 | // adding variables as parameters | ||
460 | val Map<Variable, SMTSortedVariable> variables = new HashMap | ||
461 | var paramIndex = 0 | ||
462 | val constraintList = new LinkedList | ||
463 | for(param : parameterTypeCombination) { | ||
464 | val paramName = relation.variables.get(paramIndex).name.toID | ||
465 | val variable = createSMTSortedVariable => [ | ||
466 | it.name = paramName | ||
467 | it.range = param.type | ||
468 | ] | ||
469 | |||
470 | smtRelation.parameters+=variable | ||
471 | variables.put(relation.variables.get(paramIndex),variable) | ||
472 | if(param.constraint != null) { | ||
473 | constraintList+=param.constraint.apply(variable) | ||
474 | } | ||
475 | paramIndex++ | ||
476 | } | ||
477 | val definition = transformTerm(relation.value,trace,variables) | ||
478 | if(constraintList.empty) { | ||
479 | smtRelation.value = definition.expectLogic.value | ||
480 | } else if(constraintList.size == 1) { | ||
481 | smtRelation.value = createSMTAnd => [ | ||
482 | it.operands += constraintList.head | ||
483 | it.operands += definition.expectLogic.value | ||
484 | ] | ||
485 | } else { | ||
486 | smtRelation.value = createSMTAnd => [ | ||
487 | it.operands += createSMTAnd => [operands += constraintList] | ||
488 | it.operands += definition.expectLogic.value | ||
489 | ] | ||
490 | } | ||
491 | } | ||
492 | } | ||
493 | |||
494 | def transformConstantDeclaration(ConstantDeclaration constant,SMTInput input, Logic2SmtMapperTrace trace) { | ||
495 | throw new UnsupportedOperationException("TODO: auto-generated method stub") | ||
496 | } | ||
497 | |||
498 | def transformConstantDefinition(ConstantDefinition constant, SMTInput input, Logic2SmtMapperTrace trace) { | ||
499 | throw new UnsupportedOperationException("TODO: auto-generated method stub") | ||
500 | } | ||
501 | |||
502 | |||
503 | def protected SMTAssertion transformAssertion(Assertion assertion, Logic2SmtMapperTrace trace) { | ||
504 | val a = assertion.value.transformTerm(trace,emptyMap) | ||
505 | createSMTAssertion => [value = a.expectLogic.value] | ||
506 | } | ||
507 | |||
508 | /////////////////////////////////////////////////////// | ||
509 | // Logic -> Logic value transformation | ||
510 | /////////////////////////////////////////////////////// | ||
511 | |||
512 | /////////////////////////////////////////////////////// | ||
513 | // Literals | ||
514 | /////////////////////////////////////////////////////// | ||
515 | def dispatch protected TransformedSubterm transformTerm(BoolLiteral literal, Logic2SmtMapperTrace trace, Map<Variable, SMTSortedVariable> variables) { | ||
516 | new LogicSubterm(createSMTBoolLiteral => [value = literal.value]) } | ||
517 | def dispatch protected TransformedSubterm transformTerm(IntLiteral literal, Logic2SmtMapperTrace trace, Map<Variable, SMTSortedVariable> variables) { | ||
518 | if(literal.value>=0) { new NumericSubterm(#[],#[],createSMTIntLiteral => [value = literal.value])} | ||
519 | else {new NumericSubterm(#[],#[],createSMTMinus => [ leftOperand = (createSMTIntLiteral => [value = - (literal.value) ] ) ]) } } | ||
520 | def dispatch protected TransformedSubterm transformTerm(RealLiteral literal, Logic2SmtMapperTrace trace, Map<Variable, SMTSortedVariable> variables) { | ||
521 | new NumericSubterm(#[],#[],createSMTRealLiteral => [value = literal.value]) } | ||
522 | |||
523 | /////////////////////////////////////////////////////// | ||
524 | // NumericOperators | ||
525 | /////////////////////////////////////////////////////// | ||
526 | def dispatch protected TransformedSubterm transformTerm(Plus plus, Logic2SmtMapperTrace trace, Map<Variable, SMTSortedVariable> variables) { | ||
527 | return transformBinaryNumericOperator( | ||
528 | plus.leftOperand,plus.rightOperand, | ||
529 | [l,r|createSMTPlus => [ leftOperand = l rightOperand = r ]], | ||
530 | trace,variables) | ||
531 | } | ||
532 | def dispatch protected TransformedSubterm transformTerm(Minus minus, Logic2SmtMapperTrace trace, Map<Variable, SMTSortedVariable> variables) { | ||
533 | return transformBinaryNumericOperator( | ||
534 | minus.leftOperand,minus.rightOperand, | ||
535 | [l,r|createSMTMinus => [ leftOperand = l rightOperand = r ]], | ||
536 | trace,variables) | ||
537 | } | ||
538 | def dispatch protected TransformedSubterm transformTerm(Multiply multiply, Logic2SmtMapperTrace trace, Map<Variable, SMTSortedVariable> variables) { | ||
539 | return transformBinaryNumericOperator( | ||
540 | multiply.leftOperand,multiply.rightOperand, | ||
541 | [l,r|createSMTMultiply => [ leftOperand = l rightOperand = r ]], | ||
542 | trace,variables) | ||
543 | } | ||
544 | def dispatch protected TransformedSubterm transformTerm(Divison div, Logic2SmtMapperTrace trace, Map<Variable, SMTSortedVariable> variables) { | ||
545 | return transformBinaryNumericOperator( | ||
546 | div.leftOperand,div.rightOperand, | ||
547 | [l,r|createSMTDiv => [ leftOperand = l rightOperand = r ]], | ||
548 | trace,variables) | ||
549 | } | ||
550 | def dispatch protected TransformedSubterm transformTerm(Mod mod, Logic2SmtMapperTrace trace, Map<Variable, SMTSortedVariable> variables) { | ||
551 | return transformBinaryNumericOperator( | ||
552 | mod.leftOperand,mod.rightOperand, | ||
553 | [l,r|createSMTMod => [ leftOperand = l rightOperand = r ]], | ||
554 | trace,variables) | ||
555 | } | ||
556 | |||
557 | def protected TransformedSubterm transformBinaryNumericOperator( | ||
558 | Term leftOperand, | ||
559 | Term rightOperand, | ||
560 | Function2<SMTTerm,SMTTerm,SMTTerm> combinator, | ||
561 | Logic2SmtMapperTrace trace, Map<Variable, SMTSortedVariable> variables) | ||
562 | { | ||
563 | val left = leftOperand. transformTerm(trace,variables).expectNumber.getPossibleValues | ||
564 | val right = rightOperand.transformTerm(trace,variables).expectNumber.getPossibleValues | ||
565 | val values = new ArrayList(left.size * right.size) | ||
566 | for(combination : TransformedSubterm.allCombinations(left,right)) { | ||
567 | val l = combination.get(0) | ||
568 | val r = combination.get(1) | ||
569 | values += new SubtermOption( | ||
570 | #[l,r],#[],#[], | ||
571 | combinator.apply(l.expression, r.expression), | ||
572 | TypeDescriptor.numericTypeDescriptor_Instance | ||
573 | ) | ||
574 | } | ||
575 | return new NumericSubterm(values) | ||
576 | } | ||
577 | |||
578 | /////////////////////////////////////////////////////// | ||
579 | // LogicOperators | ||
580 | /////////////////////////////////////////////////////// | ||
581 | def dispatch protected TransformedSubterm transformTerm(Not not, Logic2SmtMapperTrace trace, Map<Variable, SMTSortedVariable> variables) { | ||
582 | val operand = not.operand.transformTerm(trace,variables).expectLogic | ||
583 | new LogicSubterm(createSMTNot => [operand = operand.value]) } | ||
584 | def dispatch protected TransformedSubterm transformTerm(And and, Logic2SmtMapperTrace trace, Map<Variable, SMTSortedVariable> variables) { | ||
585 | transformBinaryLogicOperator2(and.operands,[x|createSMTAnd => [operands += x]],trace,variables) } | ||
586 | def dispatch protected TransformedSubterm transformTerm(Or or, Logic2SmtMapperTrace trace, Map<Variable, SMTSortedVariable> variables) { | ||
587 | transformBinaryLogicOperator2(or.operands,[x|createSMTOr => [operands += x]],trace,variables) } | ||
588 | def dispatch protected TransformedSubterm transformTerm(Impl impl, Logic2SmtMapperTrace trace, Map<Variable, SMTSortedVariable> variables) { | ||
589 | transformBinaryLogicOperator1(impl.leftOperand,impl.rightOperand,[l,r|createSMTImpl =>[leftOperand = l rightOperand = r]],trace,variables) } | ||
590 | def dispatch protected TransformedSubterm transformTerm(Iff iff, Logic2SmtMapperTrace trace, Map<Variable, SMTSortedVariable> variables) { | ||
591 | transformBinaryLogicOperator1(iff.leftOperand,iff.rightOperand,[l,r|createSMTIff => [leftOperand = l rightOperand = r]],trace,variables)} | ||
592 | |||
593 | /** | ||
594 | * Logic combinator with two values | ||
595 | */ | ||
596 | def protected transformBinaryLogicOperator1( | ||
597 | Term leftOperand, Term rightOperand, | ||
598 | Function2<SMTTerm,SMTTerm,SMTTerm> combinator, | ||
599 | Logic2SmtMapperTrace trace, Map<Variable, SMTSortedVariable> variables) { | ||
600 | val left = leftOperand.transformTerm(trace,variables).expectLogic | ||
601 | val right = rightOperand.transformTerm(trace,variables).expectLogic | ||
602 | return new LogicSubterm(combinator.apply(left.value, right.value)) | ||
603 | } | ||
604 | /** | ||
605 | * Logic combinator with multiple values | ||
606 | */ | ||
607 | def protected transformBinaryLogicOperator2( | ||
608 | Iterable<? extends Term> operands, | ||
609 | Function1<Iterable<? extends SMTTerm>,SMTTerm> combinator, | ||
610 | Logic2SmtMapperTrace trace, Map<Variable, SMTSortedVariable> variables) { | ||
611 | val smtOperands = operands.map[transformTerm(trace,variables).expectLogic.value] | ||
612 | return new LogicSubterm(combinator.apply(smtOperands)) | ||
613 | } | ||
614 | |||
615 | /////////////////////////////////////////////////////// | ||
616 | // Numeric -> Logic | ||
617 | /////////////////////////////////////////////////////// | ||
618 | def dispatch protected TransformedSubterm transformTerm(MoreThan moreThan, Logic2SmtMapperTrace trace, Map<Variable, SMTSortedVariable> variables) { | ||
619 | transformNumericComparison(moreThan.leftOperand,moreThan.rightOperand, [l,r|createSMTMT => [ leftOperand = l rightOperand = r ]],trace,variables)} | ||
620 | def dispatch protected TransformedSubterm transformTerm(LessThan lessThan, Logic2SmtMapperTrace trace, Map<Variable, SMTSortedVariable> variables) { | ||
621 | transformNumericComparison(lessThan.leftOperand,lessThan.rightOperand, [l,r|createSMTLT => [ leftOperand = l rightOperand = r ]],trace,variables)} | ||
622 | def dispatch protected TransformedSubterm transformTerm(MoreOrEqualThan moreThan, Logic2SmtMapperTrace trace, Map<Variable, SMTSortedVariable> variables) { | ||
623 | transformNumericComparison(moreThan.leftOperand,moreThan.rightOperand, [l,r|createSMTMEQ => [ leftOperand = l rightOperand = r ]],trace,variables)} | ||
624 | def dispatch protected TransformedSubterm transformTerm(LessOrEqualThan lessThan, Logic2SmtMapperTrace trace, Map<Variable, SMTSortedVariable> variables) { | ||
625 | transformNumericComparison(lessThan.leftOperand,lessThan.rightOperand, [l,r|createSMTLEQ => [ leftOperand = l rightOperand = r ]],trace,variables)} | ||
626 | |||
627 | def protected transformNumericComparison(Term leftOperand, Term rightOperand, Function2<SMTTerm,SMTTerm,SMTTerm> combinator, Logic2SmtMapperTrace trace, Map<Variable, SMTSortedVariable> variables){ | ||
628 | val left = leftOperand.transformTerm(trace,variables).getPossibleValues | ||
629 | val right = rightOperand.transformTerm(trace,variables).getPossibleValues | ||
630 | val values = new ArrayList(left.size * right.size) | ||
631 | for(combination : TransformedSubterm.allCombinations(left,right)) { | ||
632 | val l = combination.get(0) | ||
633 | val r = combination.get(1) | ||
634 | values += LogicSubterm::resolveToLogic(#[l,r],combinator.apply(l.expression, r.expression)) | ||
635 | } | ||
636 | val res = createSMTOr =>[operands += values] | ||
637 | return new LogicSubterm(res) | ||
638 | } | ||
639 | |||
640 | /////////////////////////////////////////////////////// | ||
641 | // Equals and Distinct | ||
642 | /////////////////////////////////////////////////////// | ||
643 | |||
644 | def dispatch protected TransformedSubterm transformTerm(Equals equals, Logic2SmtMapperTrace trace, Map<Variable, SMTSortedVariable> variables) { | ||
645 | val left = equals.leftOperand.transformTerm(trace,variables) | ||
646 | val rightX = equals.rightOperand.transformTerm(trace,variables) | ||
647 | if(left instanceof LogicSubterm) { | ||
648 | val right = rightX.expectLogic | ||
649 | new LogicSubterm(createSMTEquals => [ | ||
650 | leftOperand = left.value | ||
651 | rightOperand = right.value ]) | ||
652 | } else if(left instanceof NumericSubterm) { | ||
653 | val right = rightX.expectNumber | ||
654 | val leftOperands = left.possibleValues | ||
655 | val rightOperands = right.possibleValues | ||
656 | val values = new ArrayList(leftOperands.size * rightOperands.size) | ||
657 | for(combination : TransformedSubterm.allCombinations(left.possibleValues,right.possibleValues)) { | ||
658 | val l = combination.get(0) | ||
659 | val r = combination.get(1) | ||
660 | values += TransformedSubterm.resolveToLogic(#[l,r], | ||
661 | createSMTEquals => [ | ||
662 | leftOperand = combination.get(0).expression | ||
663 | rightOperand = combination.get(1).expression]) | ||
664 | } | ||
665 | return new LogicSubterm(createSMTOr =>[operands += values]) | ||
666 | } else if(left instanceof ComplexSubterm){ | ||
667 | val right = rightX as ComplexSubterm | ||
668 | |||
669 | val values = new LinkedList | ||
670 | for(combination : TransformedSubterm.allCombinations(left.possibleValues,right.possibleValues)) { | ||
671 | val l = combination.get(0) | ||
672 | val r = combination.get(1) | ||
673 | if(l.type.complexType == r.type.complexType) { | ||
674 | values += TransformedSubterm.resolveToLogic(#[l,r],createSMTEquals => [ | ||
675 | leftOperand = l.expression | ||
676 | rightOperand = r.expression ]) | ||
677 | } /*else dont add*/ | ||
678 | } | ||
679 | |||
680 | if(values.size == 0) { | ||
681 | return new LogicSubterm(createSMTBoolLiteral => [it.value = false]) | ||
682 | } else if(values.size == 1) { | ||
683 | return new LogicSubterm(values.head) | ||
684 | } else { | ||
685 | return new LogicSubterm(createSMTOr => [operands += values]) | ||
686 | } | ||
687 | } | ||
688 | } | ||
689 | |||
690 | def dispatch protected TransformedSubterm transformTerm(Distinct distinct, Logic2SmtMapperTrace trace, Map<Variable, SMTSortedVariable> variables) { | ||
691 | val o = distinct.operands.map[transformTerm(trace,variables)] | ||
692 | if(o.empty) { | ||
693 | throw new IllegalArgumentException('''empty distinct''') | ||
694 | } else if(o.size == 1) { | ||
695 | // 1 element is always distinct | ||
696 | new LogicSubterm(createSMTBoolLiteral => [it.value = true]) | ||
697 | } else { | ||
698 | val head = o.head | ||
699 | if(head instanceof LogicSubterm) { | ||
700 | return new LogicSubterm(createSMTDistinct => [ | ||
701 | it.operands += o.map[expectLogic.value]]) | ||
702 | } else if(head instanceof NumericSubterm) { | ||
703 | val numbers = o.map[expectNumber.possibleValues] | ||
704 | val distincts = new LinkedList | ||
705 | for(combination : TransformedSubterm.allCombinations(numbers)) { | ||
706 | distincts += LogicSubterm::resolveToLogic(combination,createSMTDistinct => [operands += combination.map[it.expression]]) | ||
707 | } | ||
708 | new LogicSubterm(createSMTOr => [it.operands += distincts]) | ||
709 | } else { | ||
710 | val objects = o.map[possibleValues] | ||
711 | val distincts = new LinkedList | ||
712 | for(combination : TransformedSubterm.allCombinations(objects)) { | ||
713 | val Map<SMTType,LinkedList<SubtermOption>> type2Terms = new LinkedHashMap; | ||
714 | for(param:combination) { | ||
715 | val type = param.type.complexType | ||
716 | val value = param | ||
717 | var LinkedList<SubtermOption> list; | ||
718 | if(type2Terms.containsKey(type)) { | ||
719 | list = type2Terms.get(type) | ||
720 | } else { | ||
721 | list = new LinkedList | ||
722 | type2Terms.put(type,list) | ||
723 | } | ||
724 | list+=value | ||
725 | } | ||
726 | |||
727 | val groups = type2Terms.values.map[elementList| | ||
728 | if(elementList.size == 1) return null | ||
729 | else return LogicSubterm.resolveToLogic(elementList,createSMTDistinct => [it.operands += elementList.map[expression]]) | ||
730 | ].filterNull | ||
731 | if(groups.empty) { | ||
732 | // One of the group is trivially satisfied | ||
733 | return new LogicSubterm(createSMTBoolLiteral => [it.value = true]) | ||
734 | } else { | ||
735 | val and = createSMTAnd => [operands += groups] | ||
736 | distincts.add(and) | ||
737 | } | ||
738 | } | ||
739 | if(distincts.size == 1) { | ||
740 | return new LogicSubterm(distincts.head) | ||
741 | } else { | ||
742 | return new LogicSubterm(createSMTOr => [it.operands += distincts]) | ||
743 | } | ||
744 | } | ||
745 | } | ||
746 | } | ||
747 | |||
748 | /////////////////////////////////////////////////////// | ||
749 | // Quantifiers | ||
750 | /////////////////////////////////////////////////////// | ||
751 | |||
752 | def dispatch protected TransformedSubterm transformTerm(Forall forall, Logic2SmtMapperTrace trace, Map<Variable, SMTSortedVariable> variables) { | ||
753 | new LogicSubterm(transformQuantifiedExpression(forall,trace,variables, | ||
754 | [createSMTForall], | ||
755 | [q|createSMTAnd=>[operands+=q]], | ||
756 | [precondition,expression|createSMTImpl=>[leftOperand=precondition rightOperand=expression]])) | ||
757 | } | ||
758 | def dispatch protected TransformedSubterm transformTerm(Exists exists, Logic2SmtMapperTrace trace, Map<Variable, SMTSortedVariable> variables) { | ||
759 | new LogicSubterm(transformQuantifiedExpression(exists,trace,variables, | ||
760 | [createSMTExists], | ||
761 | [q|createSMTOr=>[operands+=q]], | ||
762 | [precondition,expression|createSMTAnd=>[operands+=precondition operands+=expression]])) | ||
763 | } | ||
764 | |||
765 | def protected SMTTerm transformQuantifiedExpression( | ||
766 | QuantifiedExpression q, Logic2SmtMapperTrace trace, Map<Variable, SMTSortedVariable> variables, | ||
767 | Function0<SMTQuantifiedExpression> constructor, | ||
768 | Function1<Iterable<SMTQuantifiedExpression>,SMTTerm> combinator, | ||
769 | Function2<SMTTerm,SMTTerm,SMTTerm> preconditionCombinator | ||
770 | ) { | ||
771 | val permutations = unfolder.getPermutations(q.quantifiedVariables.map[it.range.transformTypeReference(trace)]) | ||
772 | val ArrayList<SMTQuantifiedExpression> unfoldedQuantification = new ArrayList(permutations.size) | ||
773 | |||
774 | for(permutation : permutations) { | ||
775 | val allVariables = new HashMap(variables) | ||
776 | val newSMTVariables = new ArrayList(q.quantifiedVariables.size) | ||
777 | val typePrecondition = new ArrayList<SMTTerm>(q.quantifiedVariables.size) | ||
778 | |||
779 | for(variableIndex: 0..<q.quantifiedVariables.size) { | ||
780 | val logicVariable = q.quantifiedVariables.get(variableIndex) | ||
781 | val elementInPermutation = permutation.get(variableIndex) | ||
782 | |||
783 | val newSMTVariable = createSMTSortedVariable => [ | ||
784 | name = logicVariable.name.toID | ||
785 | range = elementInPermutation.type | ||
786 | ] | ||
787 | allVariables.put(logicVariable, newSMTVariable) | ||
788 | newSMTVariables+=newSMTVariable | ||
789 | if(elementInPermutation.constraint != null) { | ||
790 | typePrecondition += elementInPermutation.constraint.apply(newSMTVariable) | ||
791 | } | ||
792 | } | ||
793 | |||
794 | val expressionOfQuantifiedFormula = | ||
795 | if(typePrecondition.isEmpty) | ||
796 | q.expression.transformTerm(trace,allVariables).expectLogic.value | ||
797 | else if(typePrecondition.size == 1) | ||
798 | preconditionCombinator.apply( | ||
799 | typePrecondition.head, | ||
800 | q.expression.transformTerm(trace,allVariables).expectLogic.value) | ||
801 | else | ||
802 | preconditionCombinator.apply( | ||
803 | createSMTAnd => [it.operands += typePrecondition], | ||
804 | q.expression.transformTerm(trace,allVariables).expectLogic.value) | ||
805 | |||
806 | unfoldedQuantification += constructor.apply => [ | ||
807 | quantifiedVariables += newSMTVariables | ||
808 | expression = expressionOfQuantifiedFormula | ||
809 | ] | ||
810 | |||
811 | // if(newSMTVariables.exists[it.range == null]) { | ||
812 | // println(newSMTVariables.filter[it.range == null].map[name]) | ||
813 | // } | ||
814 | } | ||
815 | |||
816 | if(permutations.size == 1) return unfoldedQuantification.head | ||
817 | else return combinator.apply(unfoldedQuantification) | ||
818 | } | ||
819 | |||
820 | /////////////////////////////////////////////////////// | ||
821 | // If - Then - Else | ||
822 | /////////////////////////////////////////////////////// | ||
823 | def dispatch protected TransformedSubterm transformTerm(IfThenElse ite, Logic2SmtMapperTrace trace, Map<Variable, SMTSortedVariable> variables) { | ||
824 | val condition = ite.condition.transformTerm(trace,variables).expectLogic.value | ||
825 | val positiveTerm = ite.ifTrue.transformTerm(trace,variables) | ||
826 | val positives = positiveTerm.possibleValues | ||
827 | val negativeTerm = ite.ifFalse.transformTerm(trace,variables) | ||
828 | val negatives = negativeTerm.possibleValues | ||
829 | // Simple ITE | ||
830 | if(positives.size == 1 && negatives.size == 1 && positives.head.type == negatives.head.type) { | ||
831 | val t = positives.head.type | ||
832 | if(t.isLogic) { | ||
833 | return new LogicSubterm(createSMTITE => [ | ||
834 | it.condition = condition | ||
835 | it.^if = positives.head.expression | ||
836 | it.^else = negatives.head.expression]) | ||
837 | } else if(t.isNumeric) { | ||
838 | return new NumericSubterm( | ||
839 | (positives.head.variables + negatives.head.variables).toList, | ||
840 | (positives.head.preconditions + negatives.head.preconditions).toList, | ||
841 | createSMTITE => [ | ||
842 | it.condition = condition | ||
843 | it.^if = positives.head.expression | ||
844 | it.^else = negatives.head.expression | ||
845 | ]) | ||
846 | } else { | ||
847 | return new ComplexSubterm( | ||
848 | (positives.head.variables + negatives.head.variables).toList, | ||
849 | (positives.head.preconditions + negatives.head.preconditions).toList, | ||
850 | createSMTITE => [ | ||
851 | it.condition = condition | ||
852 | it.^if = positives.head.expression | ||
853 | it.^else = negatives.head.expression], | ||
854 | t | ||
855 | ) | ||
856 | } | ||
857 | // else the ite need to be unfolded | ||
858 | } else { | ||
859 | if(positiveTerm instanceof LogicSubterm) { | ||
860 | throw new AssertionError('''If the subterm has logic value it should be transformed as "Simple ITE""''') | ||
861 | } else if (positiveTerm instanceof NumericSubterm){ | ||
862 | return new NumericSubterm(unfoldIte(positives, condition, negatives)) | ||
863 | } else { | ||
864 | return new ComplexSubterm(unfoldIte(positives, condition, negatives)) | ||
865 | } | ||
866 | } | ||
867 | } | ||
868 | |||
869 | private def List<SubtermOption> unfoldIte(List<SubtermOption> positives, SMTTerm condition, List<SubtermOption> negatives) { | ||
870 | (positives.map[ | ||
871 | new SubtermOption(#[it],#[],#[condition],it.expression,it.type) | ||
872 | ] + | ||
873 | negatives.map[ | ||
874 | new SubtermOption(#[it],#[],#[createSMTNot => [it.operand = condition]],it.expression,it.type) | ||
875 | ]).toList | ||
876 | } | ||
877 | |||
878 | /////////////////////////////////////////////////////// | ||
879 | // instanceof | ||
880 | /////////////////////////////////////////////////////// | ||
881 | |||
882 | def dispatch protected TransformedSubterm transformTerm(InstanceOf i, Logic2SmtMapperTrace trace, Map<Variable, SMTSortedVariable> variables) { | ||
883 | val value = i.value.transformTerm(trace,variables) | ||
884 | val range = i.range | ||
885 | if(range instanceof BoolTypeReference) { | ||
886 | return new LogicSubterm(createSMTBoolLiteral=>[it.value = (value instanceof LogicSubterm)]) | ||
887 | } else if(range instanceof IntTypeReference || range instanceof RealTypeReference) { | ||
888 | return new LogicSubterm(createSMTBoolLiteral=>[it.value = (value instanceof NumericSubterm)]) | ||
889 | } else { | ||
890 | val requestedTypes = this.typeMapper.transformTypeReference((range as ComplexTypeReference).referred,trace) | ||
891 | val possileValues = value.possibleValues | ||
892 | val options = new ArrayList(requestedTypes.size) | ||
893 | for(typeConstraint : requestedTypes) { | ||
894 | val possibleValue = possileValues.filter[it.type.complexType == (typeConstraint.type as SMTComplexTypeReference).referred].head | ||
895 | if(possibleValue != null) { | ||
896 | val x = if(typeConstraint.constraint != null ) { | ||
897 | if(possibleValue.expression instanceof SMTSymbolicValue && (possibleValue.expression as SMTSymbolicValue).symbolicReference instanceof SMTSortedVariable) { | ||
898 | val referred = (possibleValue.expression as SMTSymbolicValue).symbolicReference as SMTSortedVariable | ||
899 | typeConstraint.constraint.apply(referred) | ||
900 | } else { | ||
901 | createSMTForall => [ | ||
902 | val v = createSMTSortedVariable => [it.range = EcoreUtil.copy(typeConstraint.type)] | ||
903 | it.quantifiedVariables += v | ||
904 | it.expression = createSMTImpl => [ | ||
905 | leftOperand = createSMTEquals => [ | ||
906 | it.leftOperand = possibleValue.expression | ||
907 | it.rightOperand = createSMTSymbolicValue => [it.symbolicReference = v] | ||
908 | ] | ||
909 | rightOperand = typeConstraint.constraint.apply(v) | ||
910 | ] | ||
911 | ] | ||
912 | } | ||
913 | } else if(typeConstraint.constraint == null) { | ||
914 | createSMTBoolLiteral => [it.value = true] | ||
915 | } | ||
916 | options += LogicSubterm::resolveToLogic(#[possibleValue],x) | ||
917 | } | ||
918 | } | ||
919 | |||
920 | if(options.size == 0) { | ||
921 | return new LogicSubterm(createSMTBoolLiteral=>[it.value = false]) | ||
922 | } else if(options.size == 1) { | ||
923 | return new LogicSubterm(options.head) | ||
924 | } else { | ||
925 | return new LogicSubterm(createSMTOr => [it.operands += options]) | ||
926 | } | ||
927 | } | ||
928 | |||
929 | } | ||
930 | |||
931 | /////////////////////////////////////////////////////// | ||
932 | // SymbolicReference | ||
933 | /////////////////////////////////////////////////////// | ||
934 | |||
935 | def dispatch protected TransformedSubterm transformTerm(SymbolicValue symbolicValue, Logic2SmtMapperTrace trace, Map<Variable, SMTSortedVariable> variables) { | ||
936 | val referred = symbolicValue.symbolicReference | ||
937 | val params = symbolicValue.parameterSubstitutions | ||
938 | return transformSymbolicReference(referred,params,trace,variables) | ||
939 | } | ||
940 | |||
941 | def dispatch protected TransformedSubterm transformSymbolicReference(Relation referred, List<Term> parameterSubstitution, Logic2SmtMapperTrace trace, Map<Variable, SMTSortedVariable> variables) { | ||
942 | val parameters = parameterSubstitution.map[transformTerm(it,trace,variables)] | ||
943 | val list = new LinkedList | ||
944 | for(combination : TransformedSubterm.allCombinations(parameters.map[it.possibleValues])) { | ||
945 | val descriptor = new Descriptor(combination.map[it.type],referred) | ||
946 | val targetRelation = descriptor.lookup(trace.relationMap) | ||
947 | if(targetRelation == null) { | ||
948 | throw new AssertionError('''target relation should not be null (yet)''') | ||
949 | |||
950 | } else { | ||
951 | list += TransformedSubterm.resolveToLogic(combination,createSMTSymbolicValue => [ | ||
952 | it.symbolicReference = targetRelation | ||
953 | it.parameterSubstitutions += combination.map[it.expression] | ||
954 | ]) | ||
955 | } | ||
956 | } | ||
957 | |||
958 | if(list.size == 1) { | ||
959 | return new LogicSubterm(list.head) | ||
960 | } else { | ||
961 | return new LogicSubterm(createSMTOr => [ operands += list ]) | ||
962 | } | ||
963 | } | ||
964 | |||
965 | |||
966 | def dispatch protected TransformedSubterm transformSymbolicReference(Function referred, List<Term> parameterSubstitution, Logic2SmtMapperTrace trace, Map<Variable, SMTSortedVariable> variables) { | ||
967 | throw new UnsupportedOperationException | ||
968 | } | ||
969 | |||
970 | def dispatch protected TransformedSubterm transformSymbolicReference(Variable referred, List<Term> parameterSubstitution, Logic2SmtMapperTrace trace, Map<Variable, SMTSortedVariable> variables) { | ||
971 | if(!variables.containsKey(referred)) { | ||
972 | val container = referred.eContainer | ||
973 | println("X" + container) | ||
974 | for(v : variables.keySet) { | ||
975 | println(v) | ||
976 | println("in " +v.eContainer) | ||
977 | } | ||
978 | return null | ||
979 | } | ||
980 | val v = referred.lookup(variables) | ||
981 | |||
982 | val expression = createSMTSymbolicValue => [it.symbolicReference = v] | ||
983 | if(v.range instanceof SMTBoolTypeReference) { | ||
984 | return new LogicSubterm(expression) | ||
985 | } else if(v.range instanceof SMTIntTypeReference || v.range instanceof SMTRealTypeReference) { | ||
986 | return new NumericSubterm(#[],#[],expression) | ||
987 | } else { | ||
988 | return new ComplexSubterm(#[],#[],expression, | ||
989 | new TypeDescriptor((v.range as SMTComplexTypeReference).referred)); | ||
990 | } | ||
991 | } | ||
992 | |||
993 | def dispatch protected TransformedSubterm transformSymbolicReference(DefinedElement referred, List<Term> parameterSubstitution, Logic2SmtMapperTrace trace, Map<Variable, SMTSortedVariable> variables) { | ||
994 | this.typeMapper.transformSymbolicReference(referred,trace) | ||
995 | } | ||
996 | |||
997 | def dispatch protected TransformedSubterm transformSymbolicReference(Void referred, List<Term> parameterSubstitution, Logic2SmtMapperTrace trace, Map<Variable, SMTSortedVariable> variables) { | ||
998 | throw new NullPointerException('''unfilled symbolic reference!''') | ||
999 | } | ||
1000 | |||
1001 | /////////// | ||
1002 | |||
1003 | /*def transformContainment(SMTDocument document, ContainmentHierarchy h, Logic2SmtMapperTrace trace) { | ||
1004 | val containmentRelation_oo = createSMTFunctionDefinition=>[ | ||
1005 | it.name="containment!oo" | ||
1006 | it.range=createSMTBoolTypeReference | ||
1007 | val child = createSMTSortedVariable => [ | ||
1008 | it.name = | ||
1009 | ] | ||
1010 | ] | ||
1011 | }*/ | ||
1012 | |||
1013 | /////////// | ||
1014 | |||
1015 | def cleanDocument(SMTDocument document) { | ||
1016 | val content = document.eAllContents.toList | ||
1017 | for(object:content) { | ||
1018 | for(containmentReference : object.eClass.EAllReferences.filter[containment]) { | ||
1019 | val child = object.eGet(containmentReference) { | ||
1020 | if(child!=null) { | ||
1021 | if(containmentReference.isMany) { | ||
1022 | val list = child as List<EObject> | ||
1023 | for(index : 0..<list.size) { | ||
1024 | val single = list.get(index) | ||
1025 | val newSingle = replaceWith(single) | ||
1026 | if(newSingle!=null) { | ||
1027 | list.set(index,newSingle) | ||
1028 | } | ||
1029 | } | ||
1030 | } else { | ||
1031 | val single = child as EObject | ||
1032 | val newSingle = replaceWith(single) | ||
1033 | if(newSingle!=null) { | ||
1034 | object.eSet(containmentReference,newSingle) | ||
1035 | } | ||
1036 | } | ||
1037 | } | ||
1038 | } | ||
1039 | } | ||
1040 | } | ||
1041 | } | ||
1042 | def private dispatch replaceWith(SMTOr or) { | ||
1043 | if(or.operands.empty) { | ||
1044 | return createSMTBoolLiteral => [it.value = false] | ||
1045 | } else return null | ||
1046 | } | ||
1047 | def private dispatch replaceWith(SMTAnd and) { | ||
1048 | if(and.operands.empty) { | ||
1049 | return createSMTBoolLiteral => [it.value = true] | ||
1050 | } else return null | ||
1051 | } | ||
1052 | def private dispatch replaceWith(EObject object) { | ||
1053 | null | ||
1054 | } | ||
1055 | } \ No newline at end of file | ||