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