diff options
Diffstat (limited to 'Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/model/generated')
2 files changed, 542 insertions, 0 deletions
diff --git a/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/model/generated/SmtLanguage.ecore b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/model/generated/SmtLanguage.ecore new file mode 100644 index 00000000..e49cb530 --- /dev/null +++ b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/model/generated/SmtLanguage.ecore | |||
@@ -0,0 +1,304 @@ | |||
1 | <?xml version="1.0" encoding="UTF-8"?> | ||
2 | <ecore:EPackage xmi:version="2.0" xmlns:xmi="http://www.omg.org/XMI" xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance" | ||
3 | xmlns:ecore="http://www.eclipse.org/emf/2002/Ecore" name="smtLanguage" nsURI="http://www.bme.hu/mit/inf/dslreasoner/SmtLanguage" | ||
4 | nsPrefix="smtLanguage"> | ||
5 | <eClassifiers xsi:type="ecore:EClass" name="SMTDocument"> | ||
6 | <eStructuralFeatures xsi:type="ecore:EReference" name="input" eType="#//SMTInput" | ||
7 | containment="true"/> | ||
8 | <eStructuralFeatures xsi:type="ecore:EReference" name="output" eType="#//SMTOutput" | ||
9 | containment="true"/> | ||
10 | </eClassifiers> | ||
11 | <eClassifiers xsi:type="ecore:EClass" name="SMTInput"> | ||
12 | <eStructuralFeatures xsi:type="ecore:EReference" name="options" upperBound="-1" | ||
13 | eType="#//SMTOption" containment="true"/> | ||
14 | <eStructuralFeatures xsi:type="ecore:EReference" name="typeDeclarations" upperBound="-1" | ||
15 | eType="#//SMTType" containment="true"/> | ||
16 | <eStructuralFeatures xsi:type="ecore:EReference" name="functionDeclarations" upperBound="-1" | ||
17 | eType="#//SMTFunctionDeclaration" containment="true"/> | ||
18 | <eStructuralFeatures xsi:type="ecore:EReference" name="functionDefinition" upperBound="-1" | ||
19 | eType="#//SMTFunctionDefinition" containment="true"/> | ||
20 | <eStructuralFeatures xsi:type="ecore:EReference" name="assertions" upperBound="-1" | ||
21 | eType="#//SMTAssertion" containment="true"/> | ||
22 | <eStructuralFeatures xsi:type="ecore:EReference" name="satCommand" eType="#//SMTSatCommand" | ||
23 | containment="true"/> | ||
24 | <eStructuralFeatures xsi:type="ecore:EReference" name="getModelCommand" eType="#//SMTGetModelCommand" | ||
25 | containment="true"/> | ||
26 | </eClassifiers> | ||
27 | <eClassifiers xsi:type="ecore:EClass" name="SMTOutput"> | ||
28 | <eStructuralFeatures xsi:type="ecore:EReference" name="satResult" eType="#//SMTResult" | ||
29 | containment="true"/> | ||
30 | <eStructuralFeatures xsi:type="ecore:EReference" name="getModelResult" eType="#//SMTResult" | ||
31 | containment="true"/> | ||
32 | <eStructuralFeatures xsi:type="ecore:EReference" name="statistics" eType="#//SMTStatisticsSection" | ||
33 | containment="true"/> | ||
34 | </eClassifiers> | ||
35 | <eClassifiers xsi:type="ecore:EClass" name="SMTOption"> | ||
36 | <eStructuralFeatures xsi:type="ecore:EAttribute" name="name" eType="ecore:EDataType http://www.eclipse.org/emf/2002/Ecore#//EString"/> | ||
37 | <eStructuralFeatures xsi:type="ecore:EReference" name="value" eType="#//SMTAtomicTerm" | ||
38 | containment="true"/> | ||
39 | </eClassifiers> | ||
40 | <eClassifiers xsi:type="ecore:EClass" name="SMTType"> | ||
41 | <eStructuralFeatures xsi:type="ecore:EAttribute" name="name" eType="ecore:EDataType http://www.eclipse.org/emf/2002/Ecore#//EString"/> | ||
42 | </eClassifiers> | ||
43 | <eClassifiers xsi:type="ecore:EClass" name="SMTEnumLiteral" eSuperTypes="#//SMTSymbolicDeclaration"/> | ||
44 | <eClassifiers xsi:type="ecore:EClass" name="SMTEnumeratedTypeDeclaration" eSuperTypes="#//SMTType"> | ||
45 | <eStructuralFeatures xsi:type="ecore:EReference" name="elements" upperBound="-1" | ||
46 | eType="#//SMTEnumLiteral" containment="true"/> | ||
47 | </eClassifiers> | ||
48 | <eClassifiers xsi:type="ecore:EClass" name="SMTSetTypeDeclaration" eSuperTypes="#//SMTType"/> | ||
49 | <eClassifiers xsi:type="ecore:EClass" name="SMTTypeReference"/> | ||
50 | <eClassifiers xsi:type="ecore:EClass" name="SMTComplexTypeReference" eSuperTypes="#//SMTTypeReference"> | ||
51 | <eStructuralFeatures xsi:type="ecore:EReference" name="referred" eType="#//SMTType"/> | ||
52 | </eClassifiers> | ||
53 | <eClassifiers xsi:type="ecore:EClass" name="SMTPrimitiveTypeReference" eSuperTypes="#//SMTTypeReference"/> | ||
54 | <eClassifiers xsi:type="ecore:EClass" name="SMTIntTypeReference" eSuperTypes="#//SMTPrimitiveTypeReference"/> | ||
55 | <eClassifiers xsi:type="ecore:EClass" name="SMTBoolTypeReference" eSuperTypes="#//SMTPrimitiveTypeReference"/> | ||
56 | <eClassifiers xsi:type="ecore:EClass" name="SMTRealTypeReference" eSuperTypes="#//SMTPrimitiveTypeReference"/> | ||
57 | <eClassifiers xsi:type="ecore:EClass" name="SMTFunctionDeclaration" eSuperTypes="#//SMTSymbolicDeclaration"> | ||
58 | <eStructuralFeatures xsi:type="ecore:EReference" name="parameters" upperBound="-1" | ||
59 | eType="#//SMTTypeReference" containment="true"/> | ||
60 | <eStructuralFeatures xsi:type="ecore:EReference" name="range" eType="#//SMTTypeReference" | ||
61 | containment="true"/> | ||
62 | </eClassifiers> | ||
63 | <eClassifiers xsi:type="ecore:EClass" name="SMTFunctionDefinition" eSuperTypes="#//SMTSymbolicDeclaration"> | ||
64 | <eStructuralFeatures xsi:type="ecore:EReference" name="parameters" upperBound="-1" | ||
65 | eType="#//SMTSortedVariable" containment="true"/> | ||
66 | <eStructuralFeatures xsi:type="ecore:EReference" name="range" eType="#//SMTTypeReference" | ||
67 | containment="true"/> | ||
68 | <eStructuralFeatures xsi:type="ecore:EReference" name="value" eType="#//SMTTerm" | ||
69 | containment="true"/> | ||
70 | </eClassifiers> | ||
71 | <eClassifiers xsi:type="ecore:EClass" name="SMTTerm"/> | ||
72 | <eClassifiers xsi:type="ecore:EClass" name="SMTSymbolicDeclaration"> | ||
73 | <eStructuralFeatures xsi:type="ecore:EAttribute" name="name" eType="ecore:EDataType http://www.eclipse.org/emf/2002/Ecore#//EString"/> | ||
74 | </eClassifiers> | ||
75 | <eClassifiers xsi:type="ecore:EClass" name="SMTSymbolicValue" eSuperTypes="#//SMTTerm"> | ||
76 | <eStructuralFeatures xsi:type="ecore:EReference" name="symbolicReference" eType="#//SMTSymbolicDeclaration"/> | ||
77 | <eStructuralFeatures xsi:type="ecore:EReference" name="parameterSubstitutions" | ||
78 | upperBound="-1" eType="#//SMTTerm" containment="true"/> | ||
79 | </eClassifiers> | ||
80 | <eClassifiers xsi:type="ecore:EClass" name="SMTAtomicTerm" eSuperTypes="#//SMTTerm"/> | ||
81 | <eClassifiers xsi:type="ecore:EClass" name="SMTIntLiteral" eSuperTypes="#//SMTAtomicTerm"> | ||
82 | <eStructuralFeatures xsi:type="ecore:EAttribute" name="value" eType="ecore:EDataType http://www.eclipse.org/emf/2002/Ecore#//EInt"/> | ||
83 | </eClassifiers> | ||
84 | <eClassifiers xsi:type="ecore:EClass" name="SMTBoolLiteral" eSuperTypes="#//SMTAtomicTerm"> | ||
85 | <eStructuralFeatures xsi:type="ecore:EAttribute" name="value" eType="ecore:EDataType http://www.eclipse.org/emf/2002/Ecore#//EBoolean"/> | ||
86 | </eClassifiers> | ||
87 | <eClassifiers xsi:type="ecore:EClass" name="SMTRealLiteral" eSuperTypes="#//SMTAtomicTerm"> | ||
88 | <eStructuralFeatures xsi:type="ecore:EAttribute" name="value" eType="ecore:EDataType http://www.eclipse.org/emf/2002/Ecore#//EBigDecimal"/> | ||
89 | </eClassifiers> | ||
90 | <eClassifiers xsi:type="ecore:EClass" name="SMTSortedVariable" eSuperTypes="#//SMTSymbolicDeclaration"> | ||
91 | <eStructuralFeatures xsi:type="ecore:EReference" name="range" eType="#//SMTTypeReference" | ||
92 | containment="true"/> | ||
93 | </eClassifiers> | ||
94 | <eClassifiers xsi:type="ecore:EClass" name="SMTQuantifiedExpression" eSuperTypes="#//SMTTerm"> | ||
95 | <eStructuralFeatures xsi:type="ecore:EReference" name="quantifiedVariables" upperBound="-1" | ||
96 | eType="#//SMTSortedVariable" containment="true"/> | ||
97 | <eStructuralFeatures xsi:type="ecore:EReference" name="expression" eType="#//SMTTerm" | ||
98 | containment="true"/> | ||
99 | <eStructuralFeatures xsi:type="ecore:EReference" name="pattern" eType="#//SMTTerm" | ||
100 | containment="true"/> | ||
101 | </eClassifiers> | ||
102 | <eClassifiers xsi:type="ecore:EClass" name="SMTExists" eSuperTypes="#//SMTQuantifiedExpression"/> | ||
103 | <eClassifiers xsi:type="ecore:EClass" name="SMTForall" eSuperTypes="#//SMTQuantifiedExpression"/> | ||
104 | <eClassifiers xsi:type="ecore:EClass" name="SMTBoolOperation" eSuperTypes="#//SMTTerm"/> | ||
105 | <eClassifiers xsi:type="ecore:EClass" name="SMTAnd" eSuperTypes="#//SMTBoolOperation"> | ||
106 | <eStructuralFeatures xsi:type="ecore:EReference" name="operands" upperBound="-1" | ||
107 | eType="#//SMTTerm" containment="true"/> | ||
108 | </eClassifiers> | ||
109 | <eClassifiers xsi:type="ecore:EClass" name="SMTOr" eSuperTypes="#//SMTBoolOperation"> | ||
110 | <eStructuralFeatures xsi:type="ecore:EReference" name="operands" upperBound="-1" | ||
111 | eType="#//SMTTerm" containment="true"/> | ||
112 | </eClassifiers> | ||
113 | <eClassifiers xsi:type="ecore:EClass" name="SMTImpl" eSuperTypes="#//SMTBoolOperation"> | ||
114 | <eStructuralFeatures xsi:type="ecore:EReference" name="leftOperand" eType="#//SMTTerm" | ||
115 | containment="true"/> | ||
116 | <eStructuralFeatures xsi:type="ecore:EReference" name="rightOperand" eType="#//SMTTerm" | ||
117 | containment="true"/> | ||
118 | </eClassifiers> | ||
119 | <eClassifiers xsi:type="ecore:EClass" name="SMTNot" eSuperTypes="#//SMTBoolOperation"> | ||
120 | <eStructuralFeatures xsi:type="ecore:EReference" name="operand" eType="#//SMTTerm" | ||
121 | containment="true"/> | ||
122 | </eClassifiers> | ||
123 | <eClassifiers xsi:type="ecore:EClass" name="SMTIff" eSuperTypes="#//SMTBoolOperation"> | ||
124 | <eStructuralFeatures xsi:type="ecore:EReference" name="leftOperand" eType="#//SMTTerm" | ||
125 | containment="true"/> | ||
126 | <eStructuralFeatures xsi:type="ecore:EReference" name="rightOperand" eType="#//SMTTerm" | ||
127 | containment="true"/> | ||
128 | </eClassifiers> | ||
129 | <eClassifiers xsi:type="ecore:EClass" name="SMTITE" eSuperTypes="#//SMTTerm"> | ||
130 | <eStructuralFeatures xsi:type="ecore:EReference" name="condition" eType="#//SMTTerm" | ||
131 | containment="true"/> | ||
132 | <eStructuralFeatures xsi:type="ecore:EReference" name="if" eType="#//SMTTerm" | ||
133 | containment="true"/> | ||
134 | <eStructuralFeatures xsi:type="ecore:EReference" name="else" eType="#//SMTTerm" | ||
135 | containment="true"/> | ||
136 | </eClassifiers> | ||
137 | <eClassifiers xsi:type="ecore:EClass" name="SMTLet" eSuperTypes="#//SMTTerm"> | ||
138 | <eStructuralFeatures xsi:type="ecore:EReference" name="inlineConstantDefinitions" | ||
139 | upperBound="-1" eType="#//SMTInlineConstantDefinition" containment="true"/> | ||
140 | <eStructuralFeatures xsi:type="ecore:EReference" name="term" eType="#//SMTTerm" | ||
141 | containment="true"/> | ||
142 | </eClassifiers> | ||
143 | <eClassifiers xsi:type="ecore:EClass" name="SMTInlineConstantDefinition" eSuperTypes="#//SMTSymbolicDeclaration"> | ||
144 | <eStructuralFeatures xsi:type="ecore:EReference" name="definition" eType="#//SMTTerm" | ||
145 | containment="true"/> | ||
146 | </eClassifiers> | ||
147 | <eClassifiers xsi:type="ecore:EClass" name="SMTRelation" eSuperTypes="#//SMTTerm"/> | ||
148 | <eClassifiers xsi:type="ecore:EClass" name="SMTEquals" eSuperTypes="#//SMTRelation"> | ||
149 | <eStructuralFeatures xsi:type="ecore:EReference" name="leftOperand" eType="#//SMTTerm" | ||
150 | containment="true"/> | ||
151 | <eStructuralFeatures xsi:type="ecore:EReference" name="rightOperand" eType="#//SMTTerm" | ||
152 | containment="true"/> | ||
153 | </eClassifiers> | ||
154 | <eClassifiers xsi:type="ecore:EClass" name="SMTDistinct" eSuperTypes="#//SMTRelation"> | ||
155 | <eStructuralFeatures xsi:type="ecore:EReference" name="operands" upperBound="-1" | ||
156 | eType="#//SMTTerm" containment="true"/> | ||
157 | </eClassifiers> | ||
158 | <eClassifiers xsi:type="ecore:EClass" name="SMTLT" eSuperTypes="#//SMTRelation"> | ||
159 | <eStructuralFeatures xsi:type="ecore:EReference" name="leftOperand" eType="#//SMTTerm" | ||
160 | containment="true"/> | ||
161 | <eStructuralFeatures xsi:type="ecore:EReference" name="rightOperand" eType="#//SMTTerm" | ||
162 | containment="true"/> | ||
163 | </eClassifiers> | ||
164 | <eClassifiers xsi:type="ecore:EClass" name="SMTMT" eSuperTypes="#//SMTRelation"> | ||
165 | <eStructuralFeatures xsi:type="ecore:EReference" name="leftOperand" eType="#//SMTTerm" | ||
166 | containment="true"/> | ||
167 | <eStructuralFeatures xsi:type="ecore:EReference" name="rightOperand" eType="#//SMTTerm" | ||
168 | containment="true"/> | ||
169 | </eClassifiers> | ||
170 | <eClassifiers xsi:type="ecore:EClass" name="SMTLEQ" eSuperTypes="#//SMTRelation"> | ||
171 | <eStructuralFeatures xsi:type="ecore:EReference" name="leftOperand" eType="#//SMTTerm" | ||
172 | containment="true"/> | ||
173 | <eStructuralFeatures xsi:type="ecore:EReference" name="rightOperand" eType="#//SMTTerm" | ||
174 | containment="true"/> | ||
175 | </eClassifiers> | ||
176 | <eClassifiers xsi:type="ecore:EClass" name="SMTMEQ" eSuperTypes="#//SMTRelation"> | ||
177 | <eStructuralFeatures xsi:type="ecore:EReference" name="leftOperand" eType="#//SMTTerm" | ||
178 | containment="true"/> | ||
179 | <eStructuralFeatures xsi:type="ecore:EReference" name="rightOperand" eType="#//SMTTerm" | ||
180 | containment="true"/> | ||
181 | </eClassifiers> | ||
182 | <eClassifiers xsi:type="ecore:EClass" name="SMTIntOperation" eSuperTypes="#//SMTTerm"> | ||
183 | <eStructuralFeatures xsi:type="ecore:EReference" name="leftOperand" eType="#//SMTTerm" | ||
184 | containment="true"/> | ||
185 | <eStructuralFeatures xsi:type="ecore:EReference" name="rightOperand" eType="#//SMTTerm" | ||
186 | containment="true"/> | ||
187 | </eClassifiers> | ||
188 | <eClassifiers xsi:type="ecore:EClass" name="SMTPlus" eSuperTypes="#//SMTIntOperation"/> | ||
189 | <eClassifiers xsi:type="ecore:EClass" name="SMTMinus" eSuperTypes="#//SMTIntOperation"/> | ||
190 | <eClassifiers xsi:type="ecore:EClass" name="SMTMultiply" eSuperTypes="#//SMTIntOperation"/> | ||
191 | <eClassifiers xsi:type="ecore:EClass" name="SMTDivison" eSuperTypes="#//SMTIntOperation"/> | ||
192 | <eClassifiers xsi:type="ecore:EClass" name="SMTDiv" eSuperTypes="#//SMTIntOperation"/> | ||
193 | <eClassifiers xsi:type="ecore:EClass" name="SMTMod" eSuperTypes="#//SMTIntOperation"/> | ||
194 | <eClassifiers xsi:type="ecore:EClass" name="SMTAssertion"> | ||
195 | <eStructuralFeatures xsi:type="ecore:EReference" name="value" eType="#//SMTTerm" | ||
196 | containment="true"/> | ||
197 | </eClassifiers> | ||
198 | <eClassifiers xsi:type="ecore:EClass" name="SMTCardinalityConstraint"> | ||
199 | <eStructuralFeatures xsi:type="ecore:EReference" name="type" eType="#//SMTTypeReference" | ||
200 | containment="true"/> | ||
201 | <eStructuralFeatures xsi:type="ecore:EReference" name="elements" upperBound="-1" | ||
202 | eType="#//SMTSymbolicValue" containment="true"/> | ||
203 | </eClassifiers> | ||
204 | <eClassifiers xsi:type="ecore:EClass" name="SMTSatCommand"/> | ||
205 | <eClassifiers xsi:type="ecore:EClass" name="SMTSimpleSatCommand" eSuperTypes="#//SMTSatCommand"/> | ||
206 | <eClassifiers xsi:type="ecore:EClass" name="SMTComplexSatCommand" eSuperTypes="#//SMTSatCommand"> | ||
207 | <eStructuralFeatures xsi:type="ecore:EReference" name="method" eType="#//SMTReasoningTactic" | ||
208 | containment="true"/> | ||
209 | </eClassifiers> | ||
210 | <eClassifiers xsi:type="ecore:EClass" name="SMTGetModelCommand"/> | ||
211 | <eClassifiers xsi:type="ecore:EClass" name="SMTReasoningTactic"/> | ||
212 | <eClassifiers xsi:type="ecore:EClass" name="SMTBuiltinTactic" eSuperTypes="#//SMTReasoningTactic"> | ||
213 | <eStructuralFeatures xsi:type="ecore:EAttribute" name="name" eType="ecore:EDataType http://www.eclipse.org/emf/2002/Ecore#//EString"/> | ||
214 | </eClassifiers> | ||
215 | <eClassifiers xsi:type="ecore:EClass" name="SMTReasoningCombinator" eSuperTypes="#//SMTReasoningTactic"/> | ||
216 | <eClassifiers xsi:type="ecore:EClass" name="SMTAndThenCombinator" eSuperTypes="#//SMTReasoningCombinator"> | ||
217 | <eStructuralFeatures xsi:type="ecore:EReference" name="tactics" upperBound="-1" | ||
218 | eType="#//SMTReasoningTactic" containment="true"/> | ||
219 | </eClassifiers> | ||
220 | <eClassifiers xsi:type="ecore:EClass" name="SMTOrElseCombinator" eSuperTypes="#//SMTReasoningCombinator"> | ||
221 | <eStructuralFeatures xsi:type="ecore:EReference" name="tactics" upperBound="-1" | ||
222 | eType="#//SMTReasoningTactic" containment="true"/> | ||
223 | </eClassifiers> | ||
224 | <eClassifiers xsi:type="ecore:EClass" name="SMTParOrCombinator" eSuperTypes="#//SMTReasoningCombinator"> | ||
225 | <eStructuralFeatures xsi:type="ecore:EReference" name="tactics" upperBound="-1" | ||
226 | eType="#//SMTReasoningTactic" containment="true"/> | ||
227 | </eClassifiers> | ||
228 | <eClassifiers xsi:type="ecore:EClass" name="SMTParThenCombinator" eSuperTypes="#//SMTReasoningCombinator"> | ||
229 | <eStructuralFeatures xsi:type="ecore:EReference" name="preProcessingTactic" eType="#//SMTReasoningTactic" | ||
230 | containment="true"/> | ||
231 | <eStructuralFeatures xsi:type="ecore:EReference" name="paralellyPostpricessingTactic" | ||
232 | eType="#//SMTReasoningTactic" containment="true"/> | ||
233 | </eClassifiers> | ||
234 | <eClassifiers xsi:type="ecore:EClass" name="SMTTryForCombinator" eSuperTypes="#//SMTReasoningCombinator"> | ||
235 | <eStructuralFeatures xsi:type="ecore:EReference" name="tactic" eType="#//SMTReasoningTactic" | ||
236 | containment="true"/> | ||
237 | <eStructuralFeatures xsi:type="ecore:EAttribute" name="time" eType="ecore:EDataType http://www.eclipse.org/emf/2002/Ecore#//EInt"/> | ||
238 | </eClassifiers> | ||
239 | <eClassifiers xsi:type="ecore:EClass" name="SMTIfCombinator" eSuperTypes="#//SMTReasoningCombinator"> | ||
240 | <eStructuralFeatures xsi:type="ecore:EReference" name="probe" eType="#//ReasoningProbe" | ||
241 | containment="true"/> | ||
242 | <eStructuralFeatures xsi:type="ecore:EReference" name="ifTactic" eType="#//SMTReasoningTactic" | ||
243 | containment="true"/> | ||
244 | <eStructuralFeatures xsi:type="ecore:EReference" name="elseTactic" eType="#//SMTReasoningTactic" | ||
245 | containment="true"/> | ||
246 | </eClassifiers> | ||
247 | <eClassifiers xsi:type="ecore:EClass" name="SMTWhenCombinator" eSuperTypes="#//SMTReasoningCombinator"> | ||
248 | <eStructuralFeatures xsi:type="ecore:EReference" name="probe" eType="#//ReasoningProbe" | ||
249 | containment="true"/> | ||
250 | <eStructuralFeatures xsi:type="ecore:EReference" name="tactic" eType="#//SMTReasoningTactic" | ||
251 | containment="true"/> | ||
252 | </eClassifiers> | ||
253 | <eClassifiers xsi:type="ecore:EClass" name="SMTFailIfCombinator" eSuperTypes="#//SMTReasoningCombinator"> | ||
254 | <eStructuralFeatures xsi:type="ecore:EReference" name="probe" eType="#//ReasoningProbe" | ||
255 | containment="true"/> | ||
256 | </eClassifiers> | ||
257 | <eClassifiers xsi:type="ecore:EClass" name="SMTUsingParamCombinator" eSuperTypes="#//SMTReasoningCombinator"> | ||
258 | <eStructuralFeatures xsi:type="ecore:EReference" name="tactic" eType="#//SMTReasoningTactic" | ||
259 | containment="true"/> | ||
260 | <eStructuralFeatures xsi:type="ecore:EReference" name="parameters" upperBound="-1" | ||
261 | eType="#//ReasoningTacticParameter" containment="true"/> | ||
262 | </eClassifiers> | ||
263 | <eClassifiers xsi:type="ecore:EClass" name="ReasoningProbe"> | ||
264 | <eStructuralFeatures xsi:type="ecore:EAttribute" name="name" eType="ecore:EDataType http://www.eclipse.org/emf/2002/Ecore#//EString"/> | ||
265 | </eClassifiers> | ||
266 | <eClassifiers xsi:type="ecore:EClass" name="ReasoningTacticParameter"> | ||
267 | <eStructuralFeatures xsi:type="ecore:EAttribute" name="name" eType="ecore:EDataType http://www.eclipse.org/emf/2002/Ecore#//EString"/> | ||
268 | <eStructuralFeatures xsi:type="ecore:EReference" name="value" eType="#//SMTAtomicTerm" | ||
269 | containment="true"/> | ||
270 | </eClassifiers> | ||
271 | <eClassifiers xsi:type="ecore:EClass" name="SMTResult"/> | ||
272 | <eClassifiers xsi:type="ecore:EClass" name="SMTErrorResult" eSuperTypes="#//SMTResult"> | ||
273 | <eStructuralFeatures xsi:type="ecore:EAttribute" name="message" eType="ecore:EDataType http://www.eclipse.org/emf/2002/Ecore#//EString"/> | ||
274 | </eClassifiers> | ||
275 | <eClassifiers xsi:type="ecore:EClass" name="SMTUnsupportedResult" eSuperTypes="#//SMTResult"> | ||
276 | <eStructuralFeatures xsi:type="ecore:EAttribute" name="command" eType="ecore:EDataType http://www.eclipse.org/emf/2002/Ecore#//EString"/> | ||
277 | </eClassifiers> | ||
278 | <eClassifiers xsi:type="ecore:EClass" name="SMTSatResult" eSuperTypes="#//SMTResult"> | ||
279 | <eStructuralFeatures xsi:type="ecore:EAttribute" name="sat" eType="ecore:EDataType http://www.eclipse.org/emf/2002/Ecore#//EBoolean"/> | ||
280 | <eStructuralFeatures xsi:type="ecore:EAttribute" name="unsat" eType="ecore:EDataType http://www.eclipse.org/emf/2002/Ecore#//EBoolean"/> | ||
281 | <eStructuralFeatures xsi:type="ecore:EAttribute" name="unknown" eType="ecore:EDataType http://www.eclipse.org/emf/2002/Ecore#//EBoolean"/> | ||
282 | </eClassifiers> | ||
283 | <eClassifiers xsi:type="ecore:EClass" name="SMTModelResult" eSuperTypes="#//SMTResult"> | ||
284 | <eStructuralFeatures xsi:type="ecore:EReference" name="newFunctionDeclarations" | ||
285 | upperBound="-1" eType="#//SMTFunctionDeclaration" containment="true"/> | ||
286 | <eStructuralFeatures xsi:type="ecore:EReference" name="typeDefinitions" upperBound="-1" | ||
287 | eType="#//SMTCardinalityConstraint" containment="true"/> | ||
288 | <eStructuralFeatures xsi:type="ecore:EReference" name="newFunctionDefinitions" | ||
289 | upperBound="-1" eType="#//SMTFunctionDefinition" containment="true"/> | ||
290 | </eClassifiers> | ||
291 | <eClassifiers xsi:type="ecore:EClass" name="SMTStatisticValue"> | ||
292 | <eStructuralFeatures xsi:type="ecore:EAttribute" name="name" eType="ecore:EDataType http://www.eclipse.org/emf/2002/Ecore#//EString"/> | ||
293 | </eClassifiers> | ||
294 | <eClassifiers xsi:type="ecore:EClass" name="SMTStatisticIntValue" eSuperTypes="#//SMTStatisticValue"> | ||
295 | <eStructuralFeatures xsi:type="ecore:EAttribute" name="value" eType="ecore:EDataType http://www.eclipse.org/emf/2002/Ecore#//EInt"/> | ||
296 | </eClassifiers> | ||
297 | <eClassifiers xsi:type="ecore:EClass" name="SMTStatisticDoubleValue" eSuperTypes="#//SMTStatisticValue"> | ||
298 | <eStructuralFeatures xsi:type="ecore:EAttribute" name="value" eType="ecore:EDataType http://www.eclipse.org/emf/2002/Ecore#//EBigDecimal"/> | ||
299 | </eClassifiers> | ||
300 | <eClassifiers xsi:type="ecore:EClass" name="SMTStatisticsSection"> | ||
301 | <eStructuralFeatures xsi:type="ecore:EReference" name="values" upperBound="-1" | ||
302 | eType="#//SMTStatisticValue" containment="true"/> | ||
303 | </eClassifiers> | ||
304 | </ecore:EPackage> | ||
diff --git a/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/model/generated/SmtLanguage.genmodel b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/model/generated/SmtLanguage.genmodel new file mode 100644 index 00000000..500f4dae --- /dev/null +++ b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/model/generated/SmtLanguage.genmodel | |||
@@ -0,0 +1,238 @@ | |||
1 | <?xml version="1.0" encoding="UTF-8"?> | ||
2 | <genmodel:GenModel xmi:version="2.0" xmlns:xmi="http://www.omg.org/XMI" xmlns:ecore="http://www.eclipse.org/emf/2002/Ecore" | ||
3 | xmlns:genmodel="http://www.eclipse.org/emf/2002/GenModel" modelDirectory="/hu.bme.mit.inf.dslreasoner.smt.language/src-gen" | ||
4 | editDirectory="/hu.bme.mit.inf.dslreasoner.smt.language.edit/src" editorDirectory="/hu.bme.mit.inf.dslreasoner.smt.language.editor/src" | ||
5 | modelPluginID="hu.bme.mit.inf.dslreasoner.smt.language" forceOverwrite="true" | ||
6 | modelName="SmtLanguage" updateClasspath="false" rootExtendsClass="org.eclipse.emf.ecore.impl.MinimalEObjectImpl$Container" | ||
7 | complianceLevel="5.0" copyrightFields="false" editPluginID="hu.bme.mit.inf.dslreasoner.smt.language.edit" | ||
8 | editorPluginID="hu.bme.mit.inf.dslreasoner.smt.language.editor" runtimeVersion="2.10"> | ||
9 | <genPackages prefix="SmtLanguage" basePackage="hu.bme.mit.inf.dslreasoner" disposableProviderFactory="true" | ||
10 | fileExtensions="smt2" ecorePackage="SmtLanguage.ecore#/"> | ||
11 | <genClasses ecoreClass="SmtLanguage.ecore#//SMTDocument"> | ||
12 | <genFeatures property="None" children="true" createChild="true" ecoreFeature="ecore:EReference SmtLanguage.ecore#//SMTDocument/input"/> | ||
13 | <genFeatures property="None" children="true" createChild="true" ecoreFeature="ecore:EReference SmtLanguage.ecore#//SMTDocument/output"/> | ||
14 | </genClasses> | ||
15 | <genClasses ecoreClass="SmtLanguage.ecore#//SMTInput"> | ||
16 | <genFeatures property="None" children="true" createChild="true" ecoreFeature="ecore:EReference SmtLanguage.ecore#//SMTInput/options"/> | ||
17 | <genFeatures property="None" children="true" createChild="true" ecoreFeature="ecore:EReference SmtLanguage.ecore#//SMTInput/typeDeclarations"/> | ||
18 | <genFeatures property="None" children="true" createChild="true" ecoreFeature="ecore:EReference SmtLanguage.ecore#//SMTInput/functionDeclarations"/> | ||
19 | <genFeatures property="None" children="true" createChild="true" ecoreFeature="ecore:EReference SmtLanguage.ecore#//SMTInput/functionDefinition"/> | ||
20 | <genFeatures property="None" children="true" createChild="true" ecoreFeature="ecore:EReference SmtLanguage.ecore#//SMTInput/assertions"/> | ||
21 | <genFeatures property="None" children="true" createChild="true" ecoreFeature="ecore:EReference SmtLanguage.ecore#//SMTInput/satCommand"/> | ||
22 | <genFeatures property="None" children="true" createChild="true" ecoreFeature="ecore:EReference SmtLanguage.ecore#//SMTInput/getModelCommand"/> | ||
23 | </genClasses> | ||
24 | <genClasses ecoreClass="SmtLanguage.ecore#//SMTOutput"> | ||
25 | <genFeatures property="None" children="true" createChild="true" ecoreFeature="ecore:EReference SmtLanguage.ecore#//SMTOutput/satResult"/> | ||
26 | <genFeatures property="None" children="true" createChild="true" ecoreFeature="ecore:EReference SmtLanguage.ecore#//SMTOutput/getModelResult"/> | ||
27 | <genFeatures property="None" children="true" createChild="true" ecoreFeature="ecore:EReference SmtLanguage.ecore#//SMTOutput/statistics"/> | ||
28 | </genClasses> | ||
29 | <genClasses ecoreClass="SmtLanguage.ecore#//SMTOption"> | ||
30 | <genFeatures createChild="false" ecoreFeature="ecore:EAttribute SmtLanguage.ecore#//SMTOption/name"/> | ||
31 | <genFeatures property="None" children="true" createChild="true" ecoreFeature="ecore:EReference SmtLanguage.ecore#//SMTOption/value"/> | ||
32 | </genClasses> | ||
33 | <genClasses ecoreClass="SmtLanguage.ecore#//SMTType"> | ||
34 | <genFeatures createChild="false" ecoreFeature="ecore:EAttribute SmtLanguage.ecore#//SMTType/name"/> | ||
35 | </genClasses> | ||
36 | <genClasses ecoreClass="SmtLanguage.ecore#//SMTEnumLiteral"/> | ||
37 | <genClasses ecoreClass="SmtLanguage.ecore#//SMTEnumeratedTypeDeclaration"> | ||
38 | <genFeatures property="None" children="true" createChild="true" ecoreFeature="ecore:EReference SmtLanguage.ecore#//SMTEnumeratedTypeDeclaration/elements"/> | ||
39 | </genClasses> | ||
40 | <genClasses ecoreClass="SmtLanguage.ecore#//SMTSetTypeDeclaration"/> | ||
41 | <genClasses ecoreClass="SmtLanguage.ecore#//SMTTypeReference"/> | ||
42 | <genClasses ecoreClass="SmtLanguage.ecore#//SMTComplexTypeReference"> | ||
43 | <genFeatures notify="false" createChild="false" propertySortChoices="true" ecoreFeature="ecore:EReference SmtLanguage.ecore#//SMTComplexTypeReference/referred"/> | ||
44 | </genClasses> | ||
45 | <genClasses ecoreClass="SmtLanguage.ecore#//SMTPrimitiveTypeReference"/> | ||
46 | <genClasses ecoreClass="SmtLanguage.ecore#//SMTIntTypeReference"/> | ||
47 | <genClasses ecoreClass="SmtLanguage.ecore#//SMTBoolTypeReference"/> | ||
48 | <genClasses ecoreClass="SmtLanguage.ecore#//SMTRealTypeReference"/> | ||
49 | <genClasses ecoreClass="SmtLanguage.ecore#//SMTFunctionDeclaration"> | ||
50 | <genFeatures property="None" children="true" createChild="true" ecoreFeature="ecore:EReference SmtLanguage.ecore#//SMTFunctionDeclaration/parameters"/> | ||
51 | <genFeatures property="None" children="true" createChild="true" ecoreFeature="ecore:EReference SmtLanguage.ecore#//SMTFunctionDeclaration/range"/> | ||
52 | </genClasses> | ||
53 | <genClasses ecoreClass="SmtLanguage.ecore#//SMTFunctionDefinition"> | ||
54 | <genFeatures property="None" children="true" createChild="true" ecoreFeature="ecore:EReference SmtLanguage.ecore#//SMTFunctionDefinition/parameters"/> | ||
55 | <genFeatures property="None" children="true" createChild="true" ecoreFeature="ecore:EReference SmtLanguage.ecore#//SMTFunctionDefinition/range"/> | ||
56 | <genFeatures property="None" children="true" createChild="true" ecoreFeature="ecore:EReference SmtLanguage.ecore#//SMTFunctionDefinition/value"/> | ||
57 | </genClasses> | ||
58 | <genClasses ecoreClass="SmtLanguage.ecore#//SMTTerm"/> | ||
59 | <genClasses ecoreClass="SmtLanguage.ecore#//SMTSymbolicDeclaration"> | ||
60 | <genFeatures createChild="false" ecoreFeature="ecore:EAttribute SmtLanguage.ecore#//SMTSymbolicDeclaration/name"/> | ||
61 | </genClasses> | ||
62 | <genClasses ecoreClass="SmtLanguage.ecore#//SMTSymbolicValue"> | ||
63 | <genFeatures notify="false" createChild="false" propertySortChoices="true" ecoreFeature="ecore:EReference SmtLanguage.ecore#//SMTSymbolicValue/symbolicReference"/> | ||
64 | <genFeatures property="None" children="true" createChild="true" ecoreFeature="ecore:EReference SmtLanguage.ecore#//SMTSymbolicValue/parameterSubstitutions"/> | ||
65 | </genClasses> | ||
66 | <genClasses ecoreClass="SmtLanguage.ecore#//SMTAtomicTerm"/> | ||
67 | <genClasses ecoreClass="SmtLanguage.ecore#//SMTIntLiteral"> | ||
68 | <genFeatures createChild="false" ecoreFeature="ecore:EAttribute SmtLanguage.ecore#//SMTIntLiteral/value"/> | ||
69 | </genClasses> | ||
70 | <genClasses ecoreClass="SmtLanguage.ecore#//SMTBoolLiteral"> | ||
71 | <genFeatures createChild="false" ecoreFeature="ecore:EAttribute SmtLanguage.ecore#//SMTBoolLiteral/value"/> | ||
72 | </genClasses> | ||
73 | <genClasses ecoreClass="SmtLanguage.ecore#//SMTRealLiteral"> | ||
74 | <genFeatures createChild="false" ecoreFeature="ecore:EAttribute SmtLanguage.ecore#//SMTRealLiteral/value"/> | ||
75 | </genClasses> | ||
76 | <genClasses ecoreClass="SmtLanguage.ecore#//SMTSortedVariable"> | ||
77 | <genFeatures property="None" children="true" createChild="true" ecoreFeature="ecore:EReference SmtLanguage.ecore#//SMTSortedVariable/range"/> | ||
78 | </genClasses> | ||
79 | <genClasses ecoreClass="SmtLanguage.ecore#//SMTQuantifiedExpression"> | ||
80 | <genFeatures property="None" children="true" createChild="true" ecoreFeature="ecore:EReference SmtLanguage.ecore#//SMTQuantifiedExpression/quantifiedVariables"/> | ||
81 | <genFeatures property="None" children="true" createChild="true" ecoreFeature="ecore:EReference SmtLanguage.ecore#//SMTQuantifiedExpression/expression"/> | ||
82 | <genFeatures property="None" children="true" createChild="true" ecoreFeature="ecore:EReference SmtLanguage.ecore#//SMTQuantifiedExpression/pattern"/> | ||
83 | </genClasses> | ||
84 | <genClasses ecoreClass="SmtLanguage.ecore#//SMTExists"/> | ||
85 | <genClasses ecoreClass="SmtLanguage.ecore#//SMTForall"/> | ||
86 | <genClasses ecoreClass="SmtLanguage.ecore#//SMTBoolOperation"/> | ||
87 | <genClasses ecoreClass="SmtLanguage.ecore#//SMTAnd"> | ||
88 | <genFeatures property="None" children="true" createChild="true" ecoreFeature="ecore:EReference SmtLanguage.ecore#//SMTAnd/operands"/> | ||
89 | </genClasses> | ||
90 | <genClasses ecoreClass="SmtLanguage.ecore#//SMTOr"> | ||
91 | <genFeatures property="None" children="true" createChild="true" ecoreFeature="ecore:EReference SmtLanguage.ecore#//SMTOr/operands"/> | ||
92 | </genClasses> | ||
93 | <genClasses ecoreClass="SmtLanguage.ecore#//SMTImpl"> | ||
94 | <genFeatures property="None" children="true" createChild="true" ecoreFeature="ecore:EReference SmtLanguage.ecore#//SMTImpl/leftOperand"/> | ||
95 | <genFeatures property="None" children="true" createChild="true" ecoreFeature="ecore:EReference SmtLanguage.ecore#//SMTImpl/rightOperand"/> | ||
96 | </genClasses> | ||
97 | <genClasses ecoreClass="SmtLanguage.ecore#//SMTNot"> | ||
98 | <genFeatures property="None" children="true" createChild="true" ecoreFeature="ecore:EReference SmtLanguage.ecore#//SMTNot/operand"/> | ||
99 | </genClasses> | ||
100 | <genClasses ecoreClass="SmtLanguage.ecore#//SMTIff"> | ||
101 | <genFeatures property="None" children="true" createChild="true" ecoreFeature="ecore:EReference SmtLanguage.ecore#//SMTIff/leftOperand"/> | ||
102 | <genFeatures property="None" children="true" createChild="true" ecoreFeature="ecore:EReference SmtLanguage.ecore#//SMTIff/rightOperand"/> | ||
103 | </genClasses> | ||
104 | <genClasses ecoreClass="SmtLanguage.ecore#//SMTITE"> | ||
105 | <genFeatures property="None" children="true" createChild="true" ecoreFeature="ecore:EReference SmtLanguage.ecore#//SMTITE/condition"/> | ||
106 | <genFeatures property="None" children="true" createChild="true" ecoreFeature="ecore:EReference SmtLanguage.ecore#//SMTITE/if"/> | ||
107 | <genFeatures property="None" children="true" createChild="true" ecoreFeature="ecore:EReference SmtLanguage.ecore#//SMTITE/else"/> | ||
108 | </genClasses> | ||
109 | <genClasses ecoreClass="SmtLanguage.ecore#//SMTLet"> | ||
110 | <genFeatures property="None" children="true" createChild="true" ecoreFeature="ecore:EReference SmtLanguage.ecore#//SMTLet/inlineConstantDefinitions"/> | ||
111 | <genFeatures property="None" children="true" createChild="true" ecoreFeature="ecore:EReference SmtLanguage.ecore#//SMTLet/term"/> | ||
112 | </genClasses> | ||
113 | <genClasses ecoreClass="SmtLanguage.ecore#//SMTInlineConstantDefinition"> | ||
114 | <genFeatures property="None" children="true" createChild="true" ecoreFeature="ecore:EReference SmtLanguage.ecore#//SMTInlineConstantDefinition/definition"/> | ||
115 | </genClasses> | ||
116 | <genClasses ecoreClass="SmtLanguage.ecore#//SMTRelation"/> | ||
117 | <genClasses ecoreClass="SmtLanguage.ecore#//SMTEquals"> | ||
118 | <genFeatures property="None" children="true" createChild="true" ecoreFeature="ecore:EReference SmtLanguage.ecore#//SMTEquals/leftOperand"/> | ||
119 | <genFeatures property="None" children="true" createChild="true" ecoreFeature="ecore:EReference SmtLanguage.ecore#//SMTEquals/rightOperand"/> | ||
120 | </genClasses> | ||
121 | <genClasses ecoreClass="SmtLanguage.ecore#//SMTDistinct"> | ||
122 | <genFeatures property="None" children="true" createChild="true" ecoreFeature="ecore:EReference SmtLanguage.ecore#//SMTDistinct/operands"/> | ||
123 | </genClasses> | ||
124 | <genClasses ecoreClass="SmtLanguage.ecore#//SMTLT"> | ||
125 | <genFeatures property="None" children="true" createChild="true" ecoreFeature="ecore:EReference SmtLanguage.ecore#//SMTLT/leftOperand"/> | ||
126 | <genFeatures property="None" children="true" createChild="true" ecoreFeature="ecore:EReference SmtLanguage.ecore#//SMTLT/rightOperand"/> | ||
127 | </genClasses> | ||
128 | <genClasses ecoreClass="SmtLanguage.ecore#//SMTMT"> | ||
129 | <genFeatures property="None" children="true" createChild="true" ecoreFeature="ecore:EReference SmtLanguage.ecore#//SMTMT/leftOperand"/> | ||
130 | <genFeatures property="None" children="true" createChild="true" ecoreFeature="ecore:EReference SmtLanguage.ecore#//SMTMT/rightOperand"/> | ||
131 | </genClasses> | ||
132 | <genClasses ecoreClass="SmtLanguage.ecore#//SMTLEQ"> | ||
133 | <genFeatures property="None" children="true" createChild="true" ecoreFeature="ecore:EReference SmtLanguage.ecore#//SMTLEQ/leftOperand"/> | ||
134 | <genFeatures property="None" children="true" createChild="true" ecoreFeature="ecore:EReference SmtLanguage.ecore#//SMTLEQ/rightOperand"/> | ||
135 | </genClasses> | ||
136 | <genClasses ecoreClass="SmtLanguage.ecore#//SMTMEQ"> | ||
137 | <genFeatures property="None" children="true" createChild="true" ecoreFeature="ecore:EReference SmtLanguage.ecore#//SMTMEQ/leftOperand"/> | ||
138 | <genFeatures property="None" children="true" createChild="true" ecoreFeature="ecore:EReference SmtLanguage.ecore#//SMTMEQ/rightOperand"/> | ||
139 | </genClasses> | ||
140 | <genClasses ecoreClass="SmtLanguage.ecore#//SMTIntOperation"> | ||
141 | <genFeatures property="None" children="true" createChild="true" ecoreFeature="ecore:EReference SmtLanguage.ecore#//SMTIntOperation/leftOperand"/> | ||
142 | <genFeatures property="None" children="true" createChild="true" ecoreFeature="ecore:EReference SmtLanguage.ecore#//SMTIntOperation/rightOperand"/> | ||
143 | </genClasses> | ||
144 | <genClasses ecoreClass="SmtLanguage.ecore#//SMTPlus"/> | ||
145 | <genClasses ecoreClass="SmtLanguage.ecore#//SMTMinus"/> | ||
146 | <genClasses ecoreClass="SmtLanguage.ecore#//SMTMultiply"/> | ||
147 | <genClasses ecoreClass="SmtLanguage.ecore#//SMTDivison"/> | ||
148 | <genClasses ecoreClass="SmtLanguage.ecore#//SMTDiv"/> | ||
149 | <genClasses ecoreClass="SmtLanguage.ecore#//SMTMod"/> | ||
150 | <genClasses ecoreClass="SmtLanguage.ecore#//SMTAssertion"> | ||
151 | <genFeatures property="None" children="true" createChild="true" ecoreFeature="ecore:EReference SmtLanguage.ecore#//SMTAssertion/value"/> | ||
152 | </genClasses> | ||
153 | <genClasses ecoreClass="SmtLanguage.ecore#//SMTCardinalityConstraint"> | ||
154 | <genFeatures property="None" children="true" createChild="true" ecoreFeature="ecore:EReference SmtLanguage.ecore#//SMTCardinalityConstraint/type"/> | ||
155 | <genFeatures property="None" children="true" createChild="true" ecoreFeature="ecore:EReference SmtLanguage.ecore#//SMTCardinalityConstraint/elements"/> | ||
156 | </genClasses> | ||
157 | <genClasses ecoreClass="SmtLanguage.ecore#//SMTSatCommand"/> | ||
158 | <genClasses ecoreClass="SmtLanguage.ecore#//SMTSimpleSatCommand"/> | ||
159 | <genClasses ecoreClass="SmtLanguage.ecore#//SMTComplexSatCommand"> | ||
160 | <genFeatures property="None" children="true" createChild="true" ecoreFeature="ecore:EReference SmtLanguage.ecore#//SMTComplexSatCommand/method"/> | ||
161 | </genClasses> | ||
162 | <genClasses ecoreClass="SmtLanguage.ecore#//SMTGetModelCommand"/> | ||
163 | <genClasses ecoreClass="SmtLanguage.ecore#//SMTReasoningTactic"/> | ||
164 | <genClasses ecoreClass="SmtLanguage.ecore#//SMTBuiltinTactic"> | ||
165 | <genFeatures createChild="false" ecoreFeature="ecore:EAttribute SmtLanguage.ecore#//SMTBuiltinTactic/name"/> | ||
166 | </genClasses> | ||
167 | <genClasses ecoreClass="SmtLanguage.ecore#//SMTReasoningCombinator"/> | ||
168 | <genClasses ecoreClass="SmtLanguage.ecore#//SMTAndThenCombinator"> | ||
169 | <genFeatures property="None" children="true" createChild="true" ecoreFeature="ecore:EReference SmtLanguage.ecore#//SMTAndThenCombinator/tactics"/> | ||
170 | </genClasses> | ||
171 | <genClasses ecoreClass="SmtLanguage.ecore#//SMTOrElseCombinator"> | ||
172 | <genFeatures property="None" children="true" createChild="true" ecoreFeature="ecore:EReference SmtLanguage.ecore#//SMTOrElseCombinator/tactics"/> | ||
173 | </genClasses> | ||
174 | <genClasses ecoreClass="SmtLanguage.ecore#//SMTParOrCombinator"> | ||
175 | <genFeatures property="None" children="true" createChild="true" ecoreFeature="ecore:EReference SmtLanguage.ecore#//SMTParOrCombinator/tactics"/> | ||
176 | </genClasses> | ||
177 | <genClasses ecoreClass="SmtLanguage.ecore#//SMTParThenCombinator"> | ||
178 | <genFeatures property="None" children="true" createChild="true" ecoreFeature="ecore:EReference SmtLanguage.ecore#//SMTParThenCombinator/preProcessingTactic"/> | ||
179 | <genFeatures property="None" children="true" createChild="true" ecoreFeature="ecore:EReference SmtLanguage.ecore#//SMTParThenCombinator/paralellyPostpricessingTactic"/> | ||
180 | </genClasses> | ||
181 | <genClasses ecoreClass="SmtLanguage.ecore#//SMTTryForCombinator"> | ||
182 | <genFeatures property="None" children="true" createChild="true" ecoreFeature="ecore:EReference SmtLanguage.ecore#//SMTTryForCombinator/tactic"/> | ||
183 | <genFeatures createChild="false" ecoreFeature="ecore:EAttribute SmtLanguage.ecore#//SMTTryForCombinator/time"/> | ||
184 | </genClasses> | ||
185 | <genClasses ecoreClass="SmtLanguage.ecore#//SMTIfCombinator"> | ||
186 | <genFeatures property="None" children="true" createChild="true" ecoreFeature="ecore:EReference SmtLanguage.ecore#//SMTIfCombinator/probe"/> | ||
187 | <genFeatures property="None" children="true" createChild="true" ecoreFeature="ecore:EReference SmtLanguage.ecore#//SMTIfCombinator/ifTactic"/> | ||
188 | <genFeatures property="None" children="true" createChild="true" ecoreFeature="ecore:EReference SmtLanguage.ecore#//SMTIfCombinator/elseTactic"/> | ||
189 | </genClasses> | ||
190 | <genClasses ecoreClass="SmtLanguage.ecore#//SMTWhenCombinator"> | ||
191 | <genFeatures property="None" children="true" createChild="true" ecoreFeature="ecore:EReference SmtLanguage.ecore#//SMTWhenCombinator/probe"/> | ||
192 | <genFeatures property="None" children="true" createChild="true" ecoreFeature="ecore:EReference SmtLanguage.ecore#//SMTWhenCombinator/tactic"/> | ||
193 | </genClasses> | ||
194 | <genClasses ecoreClass="SmtLanguage.ecore#//SMTFailIfCombinator"> | ||
195 | <genFeatures property="None" children="true" createChild="true" ecoreFeature="ecore:EReference SmtLanguage.ecore#//SMTFailIfCombinator/probe"/> | ||
196 | </genClasses> | ||
197 | <genClasses ecoreClass="SmtLanguage.ecore#//SMTUsingParamCombinator"> | ||
198 | <genFeatures property="None" children="true" createChild="true" ecoreFeature="ecore:EReference SmtLanguage.ecore#//SMTUsingParamCombinator/tactic"/> | ||
199 | <genFeatures property="None" children="true" createChild="true" ecoreFeature="ecore:EReference SmtLanguage.ecore#//SMTUsingParamCombinator/parameters"/> | ||
200 | </genClasses> | ||
201 | <genClasses ecoreClass="SmtLanguage.ecore#//ReasoningProbe"> | ||
202 | <genFeatures createChild="false" ecoreFeature="ecore:EAttribute SmtLanguage.ecore#//ReasoningProbe/name"/> | ||
203 | </genClasses> | ||
204 | <genClasses ecoreClass="SmtLanguage.ecore#//ReasoningTacticParameter"> | ||
205 | <genFeatures createChild="false" ecoreFeature="ecore:EAttribute SmtLanguage.ecore#//ReasoningTacticParameter/name"/> | ||
206 | <genFeatures property="None" children="true" createChild="true" ecoreFeature="ecore:EReference SmtLanguage.ecore#//ReasoningTacticParameter/value"/> | ||
207 | </genClasses> | ||
208 | <genClasses ecoreClass="SmtLanguage.ecore#//SMTResult"/> | ||
209 | <genClasses ecoreClass="SmtLanguage.ecore#//SMTErrorResult"> | ||
210 | <genFeatures createChild="false" ecoreFeature="ecore:EAttribute SmtLanguage.ecore#//SMTErrorResult/message"/> | ||
211 | </genClasses> | ||
212 | <genClasses ecoreClass="SmtLanguage.ecore#//SMTUnsupportedResult"> | ||
213 | <genFeatures createChild="false" ecoreFeature="ecore:EAttribute SmtLanguage.ecore#//SMTUnsupportedResult/command"/> | ||
214 | </genClasses> | ||
215 | <genClasses ecoreClass="SmtLanguage.ecore#//SMTSatResult"> | ||
216 | <genFeatures createChild="false" ecoreFeature="ecore:EAttribute SmtLanguage.ecore#//SMTSatResult/sat"/> | ||
217 | <genFeatures createChild="false" ecoreFeature="ecore:EAttribute SmtLanguage.ecore#//SMTSatResult/unsat"/> | ||
218 | <genFeatures createChild="false" ecoreFeature="ecore:EAttribute SmtLanguage.ecore#//SMTSatResult/unknown"/> | ||
219 | </genClasses> | ||
220 | <genClasses ecoreClass="SmtLanguage.ecore#//SMTModelResult"> | ||
221 | <genFeatures property="None" children="true" createChild="true" ecoreFeature="ecore:EReference SmtLanguage.ecore#//SMTModelResult/newFunctionDeclarations"/> | ||
222 | <genFeatures property="None" children="true" createChild="true" ecoreFeature="ecore:EReference SmtLanguage.ecore#//SMTModelResult/typeDefinitions"/> | ||
223 | <genFeatures property="None" children="true" createChild="true" ecoreFeature="ecore:EReference SmtLanguage.ecore#//SMTModelResult/newFunctionDefinitions"/> | ||
224 | </genClasses> | ||
225 | <genClasses ecoreClass="SmtLanguage.ecore#//SMTStatisticValue"> | ||
226 | <genFeatures createChild="false" ecoreFeature="ecore:EAttribute SmtLanguage.ecore#//SMTStatisticValue/name"/> | ||
227 | </genClasses> | ||
228 | <genClasses ecoreClass="SmtLanguage.ecore#//SMTStatisticIntValue"> | ||
229 | <genFeatures createChild="false" ecoreFeature="ecore:EAttribute SmtLanguage.ecore#//SMTStatisticIntValue/value"/> | ||
230 | </genClasses> | ||
231 | <genClasses ecoreClass="SmtLanguage.ecore#//SMTStatisticDoubleValue"> | ||
232 | <genFeatures createChild="false" ecoreFeature="ecore:EAttribute SmtLanguage.ecore#//SMTStatisticDoubleValue/value"/> | ||
233 | </genClasses> | ||
234 | <genClasses ecoreClass="SmtLanguage.ecore#//SMTStatisticsSection"> | ||
235 | <genFeatures property="None" children="true" createChild="true" ecoreFeature="ecore:EReference SmtLanguage.ecore#//SMTStatisticsSection/values"/> | ||
236 | </genClasses> | ||
237 | </genPackages> | ||
238 | </genmodel:GenModel> | ||