aboutsummaryrefslogtreecommitdiffstats
path: root/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/Logic2SmtMapper.xtend
diff options
context:
space:
mode:
authorLibravatar OszkarSemerath <oszka@152.66.252.189>2017-06-10 19:05:05 +0200
committerLibravatar OszkarSemerath <oszka@152.66.252.189>2017-06-10 19:05:05 +0200
commit60f01f46ba232ed6416054f0a6115cb2a9b70b4e (patch)
tree5edf8aeb07abc51f3fec63bbd15c926e1de09552 /Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/Logic2SmtMapper.xtend
parentInitial commit, migrating from SVN (diff)
downloadVIATRA-Generator-60f01f46ba232ed6416054f0a6115cb2a9b70b4e.tar.gz
VIATRA-Generator-60f01f46ba232ed6416054f0a6115cb2a9b70b4e.tar.zst
VIATRA-Generator-60f01f46ba232ed6416054f0a6115cb2a9b70b4e.zip
Migrating Additional projects
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.xtend1055
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 @@
1package hu.bme.mit.inf.dslreasoner.smt.reasoner
2
3import hu.bme.mit.inf.dslreasoner.logic.model.builder.TracedOutput
4import hu.bme.mit.inf.dslreasoner.logic.model.builder.TypeScopes
5import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.And
6import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Assertion
7import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.BoolLiteral
8import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.BoolTypeReference
9import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference
10import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ConstantDeclaration
11import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ConstantDefinition
12import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement
13import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Distinct
14import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Divison
15import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Equals
16import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Exists
17import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Forall
18import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Function
19import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.FunctionDeclaration
20import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.FunctionDefinition
21import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.IfThenElse
22import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Iff
23import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Impl
24import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.InstanceOf
25import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.IntLiteral
26import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.IntTypeReference
27import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.LessOrEqualThan
28import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.LessThan
29import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Minus
30import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Mod
31import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.MoreOrEqualThan
32import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.MoreThan
33import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Multiply
34import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Not
35import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Or
36import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Plus
37import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.QuantifiedExpression
38import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RealLiteral
39import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RealTypeReference
40import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation
41import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration
42import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition
43import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.SymbolicValue
44import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Term
45import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable
46import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem
47import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTAnd
48import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTAssertion
49import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTBoolTypeReference
50import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTComplexTypeReference
51import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTDocument
52import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTInput
53import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTIntTypeReference
54import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTOr
55import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTQuantifiedExpression
56import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTRealTypeReference
57import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTReasoningTactic
58import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTSortedVariable
59import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTSymbolicValue
60import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTTerm
61import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTType
62import hu.bme.mit.inf.dslreasoner.smtLanguage.SmtLanguageFactory
63import java.util.ArrayList
64import java.util.HashMap
65import java.util.LinkedHashMap
66import java.util.LinkedList
67import java.util.List
68import java.util.Map
69import org.eclipse.emf.ecore.EObject
70import org.eclipse.emf.ecore.util.EcoreUtil
71import org.eclipse.xtend.lib.annotations.Accessors
72import org.eclipse.xtext.xbase.lib.Functions.Function0
73import org.eclipse.xtext.xbase.lib.Functions.Function1
74import org.eclipse.xtext.xbase.lib.Functions.Function2
75import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*
76import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTFunctionDefinition
77import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.ContainmentHierarchy
78import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicProblemBuilder
79
80class 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
generated by cgit v1.2.3-54-g00ecf (git 2.45.2) at 2024-06-29 08:49:05 +0000