diff options
author | OszkarSemerath <oszka@152.66.252.189> | 2017-06-10 19:05:05 +0200 |
---|---|---|
committer | OszkarSemerath <oszka@152.66.252.189> | 2017-06-10 19:05:05 +0200 |
commit | 60f01f46ba232ed6416054f0a6115cb2a9b70b4e (patch) | |
tree | 5edf8aeb07abc51f3fec63bbd15c926e1de09552 /Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/src/hu/bme/mit/inf/dslreasoner/scoping | |
parent | Initial commit, migrating from SVN (diff) | |
download | VIATRA-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.language/src/hu/bme/mit/inf/dslreasoner/scoping')
-rw-r--r-- | Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/src/hu/bme/mit/inf/dslreasoner/scoping/SmtLanguageScopeProvider.xtend | 138 |
1 files changed, 138 insertions, 0 deletions
diff --git a/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/src/hu/bme/mit/inf/dslreasoner/scoping/SmtLanguageScopeProvider.xtend b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/src/hu/bme/mit/inf/dslreasoner/scoping/SmtLanguageScopeProvider.xtend new file mode 100644 index 00000000..e93e0543 --- /dev/null +++ b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/src/hu/bme/mit/inf/dslreasoner/scoping/SmtLanguageScopeProvider.xtend | |||
@@ -0,0 +1,138 @@ | |||
1 | /* | ||
2 | * generated by Xtext | ||
3 | */ | ||
4 | package hu.bme.mit.inf.dslreasoner.scoping | ||
5 | |||
6 | import java.util.Set | ||
7 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTSortedVariable | ||
8 | import org.eclipse.emf.ecore.EObject | ||
9 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTQuantifiedExpression | ||
10 | import java.util.Collections | ||
11 | import java.util.HashSet | ||
12 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTInlineConstantDefinition | ||
13 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTLet | ||
14 | import java.util.Collection | ||
15 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTFunctionDefinition | ||
16 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTSymbolicValue | ||
17 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTDocument | ||
18 | import org.eclipse.xtext.scoping.IScope | ||
19 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTSymbolicDeclaration | ||
20 | import org.eclipse.emf.ecore.EReference | ||
21 | import java.util.HashMap | ||
22 | import java.util.Map | ||
23 | import org.eclipse.xtext.scoping.Scopes | ||
24 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTModelResult | ||
25 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTComplexTypeReference | ||
26 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTEnumLiteral | ||
27 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTEnumeratedTypeDeclaration | ||
28 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTFunctionDeclaration | ||
29 | |||
30 | /** | ||
31 | * This class contains custom scoping description. | ||
32 | * | ||
33 | * see : http://www.eclipse.org/Xtext/documentation.html#scoping | ||
34 | * on how and when to use it | ||
35 | * | ||
36 | */ | ||
37 | class SmtLanguageScopeProvider extends org.eclipse.xtext.scoping.impl.AbstractDeclarativeScopeProvider { | ||
38 | /** | ||
39 | * Search for the first instance of containerType up in the containment hierarchy. | ||
40 | * @param containerType | ||
41 | * @param from | ||
42 | * @return | ||
43 | */ | ||
44 | @SuppressWarnings("unchecked") | ||
45 | def private <ContainerType> ContainerType getTop(Class<ContainerType> containerType, EObject from){ | ||
46 | var actualLevel = from.eContainer(); | ||
47 | while(actualLevel!=null){ | ||
48 | if(containerType.isInstance(actualLevel)) { return actualLevel as ContainerType} | ||
49 | else { actualLevel = actualLevel.eContainer() } | ||
50 | } | ||
51 | return null; | ||
52 | } | ||
53 | |||
54 | def private Set<SMTSortedVariable> getQuantifiedVariables(EObject from) { | ||
55 | //The most inner quantified variables are in this expression: | ||
56 | val quantifiedExpression = getTop(typeof(SMTQuantifiedExpression), from); | ||
57 | if(quantifiedExpression==null) return Collections.emptySet(); | ||
58 | |||
59 | //The variables can be referred by a symbolic reference | ||
60 | val Set<SMTSortedVariable> result = new HashSet(quantifiedExpression.getQuantifiedVariables()); | ||
61 | //The variables can defined in an outer quantifier | ||
62 | result.addAll(getQuantifiedVariables(quantifiedExpression)); | ||
63 | //println(result.map[name].join(",")) | ||
64 | return result; | ||
65 | } | ||
66 | |||
67 | def private Set<SMTInlineConstantDefinition> getInlineConstantDefinitions(EObject from) { | ||
68 | //The most inner quantified variables are in this expression: | ||
69 | val let = getTop(typeof(SMTLet), from); | ||
70 | if(let==null) return Collections.emptySet(); | ||
71 | |||
72 | //The variables can be referred by a symbolic reference | ||
73 | val result = new HashSet(let.getInlineConstantDefinitions()); | ||
74 | //The variables can defined in an outer quantifier | ||
75 | result.addAll(getInlineConstantDefinitions(let)); | ||
76 | return result; | ||
77 | } | ||
78 | |||
79 | def private Collection<SMTSortedVariable> getParameters(SMTSymbolicValue from) { | ||
80 | val functionDefinition = getTop(typeof(SMTFunctionDefinition), from); | ||
81 | if(functionDefinition!=null) { | ||
82 | return functionDefinition.getParameters(); | ||
83 | } | ||
84 | else return Collections.emptySet(); | ||
85 | } | ||
86 | |||
87 | def private Set<SMTEnumLiteral> getFiniteElements(SMTSymbolicValue value) { | ||
88 | val Set<SMTEnumLiteral> result = new HashSet(); | ||
89 | val document = getTop(typeof(SMTDocument),value) | ||
90 | for(type : document.input.getTypeDeclarations().filter(typeof(SMTEnumeratedTypeDeclaration))) { | ||
91 | result.addAll(type.getElements()); | ||
92 | } | ||
93 | return result; | ||
94 | } | ||
95 | |||
96 | def private Set<SMTSymbolicDeclaration> getFunctions(SMTSymbolicValue value) { | ||
97 | val document = getTop(typeof(SMTDocument),value); | ||
98 | val input = document.input | ||
99 | var SMTModelResult output = null; | ||
100 | if(document.output != null && document.output.getModelResult instanceof SMTModelResult) { | ||
101 | output = document.output.getModelResult as SMTModelResult | ||
102 | } | ||
103 | |||
104 | val Map<String, SMTFunctionDeclaration> declarations = new HashMap | ||
105 | val Set<SMTFunctionDefinition> definitions =new HashSet | ||
106 | |||
107 | input.functionDeclarations.forEach[declarations.put(it.name,it)] | ||
108 | if(output != null) { | ||
109 | output.newFunctionDeclarations.forEach[declarations.put(it.name,it)] | ||
110 | } | ||
111 | input.functionDefinition.filter[!declarations.containsKey(it.name)].forEach[definitions += it] | ||
112 | if(output != null) { | ||
113 | output.newFunctionDefinitions.filter[!declarations.containsKey(it.name)].forEach[definitions += it] | ||
114 | } | ||
115 | |||
116 | val referrables = new HashSet<SMTSymbolicDeclaration>; | ||
117 | referrables.addAll(declarations.values) | ||
118 | referrables.addAll(definitions) | ||
119 | return referrables | ||
120 | } | ||
121 | |||
122 | def public IScope scope_SMTSymbolicValue_symbolicReference(SMTSymbolicValue value, EReference ref) { | ||
123 | val Set<SMTSymbolicDeclaration> referrables = new HashSet; | ||
124 | |||
125 | referrables.addAll(value.getFiniteElements) | ||
126 | referrables.addAll(value.getParameters) | ||
127 | referrables.addAll(value.getFunctions) | ||
128 | referrables.addAll(value.getQuantifiedVariables) | ||
129 | referrables.addAll(value.getInlineConstantDefinitions) | ||
130 | |||
131 | return Scopes.scopeFor(referrables); | ||
132 | } | ||
133 | |||
134 | // Any type defined in the input section can be referred. | ||
135 | def public IScope scope_SMTComplexTypeReference_referred(SMTComplexTypeReference reference, EReference ref){ | ||
136 | return Scopes.scopeFor(getTop(typeof(SMTDocument),reference).input.typeDeclarations) | ||
137 | } | ||
138 | } | ||