diff options
Diffstat (limited to 'Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/Logic2Smt_TypeMapper_Horizontal.xtend')
| -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, 63 insertions, 0 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 new file mode 100644 index 00000000..a5abbb44 --- /dev/null +++ b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/Logic2Smt_TypeMapper_Horizontal.xtend | |||
| @@ -0,0 +1,63 @@ | |||
| 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 | ||