aboutsummaryrefslogtreecommitdiffstats
path: root/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/model/generated/SmtLanguage.ecore
diff options
context:
space:
mode:
Diffstat (limited to 'Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/model/generated/SmtLanguage.ecore')
-rw-r--r--Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/model/generated/SmtLanguage.ecore304
1 files changed, 304 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>