aboutsummaryrefslogtreecommitdiffstats
path: root/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/model
diff options
context:
space:
mode:
Diffstat (limited to 'Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/model')
-rw-r--r--Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/model/generated/SmtLanguage.ecore304
-rw-r--r--Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/model/generated/SmtLanguage.genmodel238
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>
generated by cgit v1.2.3-54-g00ecf (git 2.45.2) at 2024-07-08 21:51:09 +0000