blob: a5abbb443231dc45335063f51683e51911e340c5 (
plain) (
blame)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
|
package hu.bme.mit.inf.dslreasoner.smt.reasoner
import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTInput
import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem
import hu.bme.mit.inf.dslreasoner.logic.model.builder.TypeScopes
import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type
import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement
import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTDocument
import java.util.List
import hu.bme.mit.inf.dslreasoner.smtLanguage.SmtLanguageFactory
import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition
class Logic2Smt_TypeMapperTrace_Horizontal implements Logic2Smt_TypeMapperTrace{
override copy(SMTInput newModel) {
throw new UnsupportedOperationException("TODO: auto-generated method stub")
}
}
class Logic2Smt_TypeMapper_Horizontal implements Logic2Smt_TypeMapper {
val extension SmtLanguageFactory factory = SmtLanguageFactory.eINSTANCE
private def toID(List<String> names) {names.join("!") }
override transformTypes(SMTInput document, LogicProblem problem, Logic2SmtMapperTrace trace, TypeScopes scopes) {
val typeTrace = new Logic2Smt_TypeMapperTrace_Horizontal
trace.typeMapperTrace = typeTrace
// mapping of known elements
}
private def Logic2Smt_TypeMapperTrace_Horizontal getTypeTrace(Logic2SmtMapperTrace trace) {
val typeTrace = trace.typeMapperTrace
if(typeTrace instanceof Logic2Smt_TypeMapperTrace_Horizontal) {
return typeTrace
} else {
throw new IllegalArgumentException('''Unknown trace type: «typeTrace.class.name»''')
}
}
private def boolean hasDefinedSupertype(Type type) {
if(type instanceof TypeDefinition) {
return true
} else {
if(type.supertypes.empty) return false
else return type.supertypes.exists[it.hasDefinedSupertype]
}
}
override transformTypeReference(Type type, Logic2SmtMapperTrace trace) {
throw new UnsupportedOperationException("TODO: auto-generated method stub")
}
override transformSymbolicReference(DefinedElement referred, Logic2SmtMapperTrace trace) {
throw new UnsupportedOperationException("TODO: auto-generated method stub")
}
override getTypeInterpretation(LogicProblem problem, SMTDocument document, SmtModelInterpretation interpretation, Logic2SmtMapperTrace trace) {
throw new UnsupportedOperationException("TODO: auto-generated method stub")
}
}
|
