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_FilteredTypesSimple.xtend_')
-rw-r--r-- | Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/Logic2Smt_TypeMapper_FilteredTypesSimple.xtend_ | 44 |
1 files changed, 29 insertions, 15 deletions
diff --git a/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/Logic2Smt_TypeMapper_FilteredTypesSimple.xtend_ b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/Logic2Smt_TypeMapper_FilteredTypesSimple.xtend_ index 79fc38e6..ceb7cc06 100644 --- a/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/Logic2Smt_TypeMapper_FilteredTypesSimple.xtend_ +++ b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/Logic2Smt_TypeMapper_FilteredTypesSimple.xtend_ | |||
@@ -1,24 +1,38 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.smt.reasoner | 1 | package hu.bme.mit.inf.dslreasoner.smt.reasoner |
2 | 2 | ||
3 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTType | 3 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.TypeScopes |
4 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type | ||
5 | import java.util.HashMap | ||
6 | import java.util.Map | ||
7 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTInput | ||
8 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTFunctionDefinition | ||
9 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTEnumLiteral | ||
10 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTEnumeratedTypeDeclaration | ||
11 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement | 4 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement |
12 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* | 5 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.LogiclanguageFactory |
6 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type | ||
7 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDeclaration | ||
8 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition | ||
13 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem | 9 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem |
14 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.TypeScopes | 10 | import hu.bme.mit.inf.dslreasoner.logic.model.patterns.PossibleDynamicTypeMatcher |
11 | import hu.bme.mit.inf.dslreasoner.logic.model.patterns.SupertypeStarMatcher | ||
12 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTComplexTypeReference | ||
15 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTDocument | 13 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTDocument |
14 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTEnumLiteral | ||
15 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTEnumeratedTypeDeclaration | ||
16 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTFunctionDeclaration | ||
17 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTFunctionDefinition | ||
18 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTInput | ||
19 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTModelResult | ||
20 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTSetTypeDeclaration | ||
21 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTSymbolicDeclaration | ||
22 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTTerm | ||
23 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTType | ||
16 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SmtLanguageFactory | 24 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SmtLanguageFactory |
17 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.LogiclanguageFactory | 25 | import java.util.ArrayList |
26 | import java.util.HashMap | ||
27 | import java.util.LinkedList | ||
18 | import java.util.List | 28 | import java.util.List |
19 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition | 29 | import java.util.Map |
20 | import org.eclipse.viatra.query.runtime.api.ViatraQueryEngine | 30 | import org.eclipse.viatra.query.runtime.api.ViatraQueryEngine |
21 | import org.eclipse.viatra.query.runtime.emf.EMFScope | 31 | import org.eclipse.viatra.query.runtime.emf.EMFScope |
32 | import org.eclipse.xtext.xbase.lib.Functions.Function0 | ||
33 | import org.eclipse.xtext.xbase.lib.Functions.Function1 | ||
34 | |||
35 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* | ||
22 | 36 | ||
23 | class Logic2Smt_TypeMapperTrace_FilteredTypesSimple implements Logic2Smt_TypeMapperTrace{ | 37 | class Logic2Smt_TypeMapperTrace_FilteredTypesSimple implements Logic2Smt_TypeMapperTrace{ |
24 | public var Map<Type, SMTType> independentClasses = new HashMap | 38 | public var Map<Type, SMTType> independentClasses = new HashMap |
@@ -58,8 +72,8 @@ class Logic2Smt_TypeMapper_FilteredTypesSimple implements Logic2Smt_TypeMapper{ | |||
58 | val extension SmtLanguageFactory factory = SmtLanguageFactory.eINSTANCE | 72 | val extension SmtLanguageFactory factory = SmtLanguageFactory.eINSTANCE |
59 | val LogiclanguageFactory factory2 = LogiclanguageFactory.eINSTANCE | 73 | val LogiclanguageFactory factory2 = LogiclanguageFactory.eINSTANCE |
60 | 74 | ||
61 | private def toID(List<String> names) {names.join("!") } | 75 | private def String toID(List<String> names) { names.map[split("\\s+").join("!")].join("!") } |
62 | private def toID(String name) {name.split("\\s+").toID} | 76 | private def String toID(String name) { name.split("\\s+").join("!")} |
63 | 77 | ||
64 | override transformTypes(SMTInput document, LogicProblem problem, Logic2SmtMapperTrace trace, TypeScopes scopes) { | 78 | override transformTypes(SMTInput document, LogicProblem problem, Logic2SmtMapperTrace trace, TypeScopes scopes) { |
65 | val typeTrace = new Logic2Smt_TypeMapperTrace_FilteredTypes | 79 | val typeTrace = new Logic2Smt_TypeMapperTrace_FilteredTypes |
@@ -80,7 +94,7 @@ class Logic2Smt_TypeMapper_FilteredTypesSimple implements Logic2Smt_TypeMapper{ | |||
80 | this.transformUndefinedElements(scopes,trace,document) | 94 | this.transformUndefinedElements(scopes,trace,document) |
81 | 95 | ||
82 | 96 | ||
83 | this.transforTypes(connectedTypes, connectedElements, trace, document, engine) | 97 | this.transformType(connectedTypes, connectedElements, trace, document, engine) |
84 | // 3.2: Type definition to new elements | 98 | // 3.2: Type definition to new elements |
85 | if(hasNewElements) { | 99 | if(hasNewElements) { |
86 | this.transformNewTypes(connectedTypesWithoutDefintypesWithoutDefinedSupertype,trace,document,engine); | 100 | this.transformNewTypes(connectedTypesWithoutDefintypesWithoutDefinedSupertype,trace,document,engine); |