From 60f01f46ba232ed6416054f0a6115cb2a9b70b4e Mon Sep 17 00:00:00 2001
From: OszkarSemerath <oszka@152.66.252.189>
Date: Sat, 10 Jun 2017 19:05:05 +0200
Subject: Migrating Additional projects

---
 .../model/generated/SmtLanguage.ecore              | 304 +++++++++++++++++++++
 .../model/generated/SmtLanguage.genmodel           | 238 ++++++++++++++++
 2 files changed, 542 insertions(+)
 create mode 100644 Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/model/generated/SmtLanguage.ecore
 create mode 100644 Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/model/generated/SmtLanguage.genmodel

(limited to 'Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/model')

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 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<ecore:EPackage xmi:version="2.0" xmlns:xmi="http://www.omg.org/XMI" xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance"
+    xmlns:ecore="http://www.eclipse.org/emf/2002/Ecore" name="smtLanguage" nsURI="http://www.bme.hu/mit/inf/dslreasoner/SmtLanguage"
+    nsPrefix="smtLanguage">
+  <eClassifiers xsi:type="ecore:EClass" name="SMTDocument">
+    <eStructuralFeatures xsi:type="ecore:EReference" name="input" eType="#//SMTInput"
+        containment="true"/>
+    <eStructuralFeatures xsi:type="ecore:EReference" name="output" eType="#//SMTOutput"
+        containment="true"/>
+  </eClassifiers>
+  <eClassifiers xsi:type="ecore:EClass" name="SMTInput">
+    <eStructuralFeatures xsi:type="ecore:EReference" name="options" upperBound="-1"
+        eType="#//SMTOption" containment="true"/>
+    <eStructuralFeatures xsi:type="ecore:EReference" name="typeDeclarations" upperBound="-1"
+        eType="#//SMTType" containment="true"/>
+    <eStructuralFeatures xsi:type="ecore:EReference" name="functionDeclarations" upperBound="-1"
+        eType="#//SMTFunctionDeclaration" containment="true"/>
+    <eStructuralFeatures xsi:type="ecore:EReference" name="functionDefinition" upperBound="-1"
+        eType="#//SMTFunctionDefinition" containment="true"/>
+    <eStructuralFeatures xsi:type="ecore:EReference" name="assertions" upperBound="-1"
+        eType="#//SMTAssertion" containment="true"/>
+    <eStructuralFeatures xsi:type="ecore:EReference" name="satCommand" eType="#//SMTSatCommand"
+        containment="true"/>
+    <eStructuralFeatures xsi:type="ecore:EReference" name="getModelCommand" eType="#//SMTGetModelCommand"
+        containment="true"/>
+  </eClassifiers>
+  <eClassifiers xsi:type="ecore:EClass" name="SMTOutput">
+    <eStructuralFeatures xsi:type="ecore:EReference" name="satResult" eType="#//SMTResult"
+        containment="true"/>
+    <eStructuralFeatures xsi:type="ecore:EReference" name="getModelResult" eType="#//SMTResult"
+        containment="true"/>
+    <eStructuralFeatures xsi:type="ecore:EReference" name="statistics" eType="#//SMTStatisticsSection"
+        containment="true"/>
+  </eClassifiers>
+  <eClassifiers xsi:type="ecore:EClass" name="SMTOption">
+    <eStructuralFeatures xsi:type="ecore:EAttribute" name="name" eType="ecore:EDataType http://www.eclipse.org/emf/2002/Ecore#//EString"/>
+    <eStructuralFeatures xsi:type="ecore:EReference" name="value" eType="#//SMTAtomicTerm"
+        containment="true"/>
+  </eClassifiers>
+  <eClassifiers xsi:type="ecore:EClass" name="SMTType">
+    <eStructuralFeatures xsi:type="ecore:EAttribute" name="name" eType="ecore:EDataType http://www.eclipse.org/emf/2002/Ecore#//EString"/>
+  </eClassifiers>
+  <eClassifiers xsi:type="ecore:EClass" name="SMTEnumLiteral" eSuperTypes="#//SMTSymbolicDeclaration"/>
+  <eClassifiers xsi:type="ecore:EClass" name="SMTEnumeratedTypeDeclaration" eSuperTypes="#//SMTType">
+    <eStructuralFeatures xsi:type="ecore:EReference" name="elements" upperBound="-1"
+        eType="#//SMTEnumLiteral" containment="true"/>
+  </eClassifiers>
+  <eClassifiers xsi:type="ecore:EClass" name="SMTSetTypeDeclaration" eSuperTypes="#//SMTType"/>
+  <eClassifiers xsi:type="ecore:EClass" name="SMTTypeReference"/>
+  <eClassifiers xsi:type="ecore:EClass" name="SMTComplexTypeReference" eSuperTypes="#//SMTTypeReference">
+    <eStructuralFeatures xsi:type="ecore:EReference" name="referred" eType="#//SMTType"/>
+  </eClassifiers>
+  <eClassifiers xsi:type="ecore:EClass" name="SMTPrimitiveTypeReference" eSuperTypes="#//SMTTypeReference"/>
+  <eClassifiers xsi:type="ecore:EClass" name="SMTIntTypeReference" eSuperTypes="#//SMTPrimitiveTypeReference"/>
+  <eClassifiers xsi:type="ecore:EClass" name="SMTBoolTypeReference" eSuperTypes="#//SMTPrimitiveTypeReference"/>
+  <eClassifiers xsi:type="ecore:EClass" name="SMTRealTypeReference" eSuperTypes="#//SMTPrimitiveTypeReference"/>
+  <eClassifiers xsi:type="ecore:EClass" name="SMTFunctionDeclaration" eSuperTypes="#//SMTSymbolicDeclaration">
+    <eStructuralFeatures xsi:type="ecore:EReference" name="parameters" upperBound="-1"
+        eType="#//SMTTypeReference" containment="true"/>
+    <eStructuralFeatures xsi:type="ecore:EReference" name="range" eType="#//SMTTypeReference"
+        containment="true"/>
+  </eClassifiers>
+  <eClassifiers xsi:type="ecore:EClass" name="SMTFunctionDefinition" eSuperTypes="#//SMTSymbolicDeclaration">
+    <eStructuralFeatures xsi:type="ecore:EReference" name="parameters" upperBound="-1"
+        eType="#//SMTSortedVariable" containment="true"/>
+    <eStructuralFeatures xsi:type="ecore:EReference" name="range" eType="#//SMTTypeReference"
+        containment="true"/>
+    <eStructuralFeatures xsi:type="ecore:EReference" name="value" eType="#//SMTTerm"
+        containment="true"/>
+  </eClassifiers>
+  <eClassifiers xsi:type="ecore:EClass" name="SMTTerm"/>
+  <eClassifiers xsi:type="ecore:EClass" name="SMTSymbolicDeclaration">
+    <eStructuralFeatures xsi:type="ecore:EAttribute" name="name" eType="ecore:EDataType http://www.eclipse.org/emf/2002/Ecore#//EString"/>
+  </eClassifiers>
+  <eClassifiers xsi:type="ecore:EClass" name="SMTSymbolicValue" eSuperTypes="#//SMTTerm">
+    <eStructuralFeatures xsi:type="ecore:EReference" name="symbolicReference" eType="#//SMTSymbolicDeclaration"/>
+    <eStructuralFeatures xsi:type="ecore:EReference" name="parameterSubstitutions"
+        upperBound="-1" eType="#//SMTTerm" containment="true"/>
+  </eClassifiers>
+  <eClassifiers xsi:type="ecore:EClass" name="SMTAtomicTerm" eSuperTypes="#//SMTTerm"/>
+  <eClassifiers xsi:type="ecore:EClass" name="SMTIntLiteral" eSuperTypes="#//SMTAtomicTerm">
+    <eStructuralFeatures xsi:type="ecore:EAttribute" name="value" eType="ecore:EDataType http://www.eclipse.org/emf/2002/Ecore#//EInt"/>
+  </eClassifiers>
+  <eClassifiers xsi:type="ecore:EClass" name="SMTBoolLiteral" eSuperTypes="#//SMTAtomicTerm">
+    <eStructuralFeatures xsi:type="ecore:EAttribute" name="value" eType="ecore:EDataType http://www.eclipse.org/emf/2002/Ecore#//EBoolean"/>
+  </eClassifiers>
+  <eClassifiers xsi:type="ecore:EClass" name="SMTRealLiteral" eSuperTypes="#//SMTAtomicTerm">
+    <eStructuralFeatures xsi:type="ecore:EAttribute" name="value" eType="ecore:EDataType http://www.eclipse.org/emf/2002/Ecore#//EBigDecimal"/>
+  </eClassifiers>
+  <eClassifiers xsi:type="ecore:EClass" name="SMTSortedVariable" eSuperTypes="#//SMTSymbolicDeclaration">
+    <eStructuralFeatures xsi:type="ecore:EReference" name="range" eType="#//SMTTypeReference"
+        containment="true"/>
+  </eClassifiers>
+  <eClassifiers xsi:type="ecore:EClass" name="SMTQuantifiedExpression" eSuperTypes="#//SMTTerm">
+    <eStructuralFeatures xsi:type="ecore:EReference" name="quantifiedVariables" upperBound="-1"
+        eType="#//SMTSortedVariable" containment="true"/>
+    <eStructuralFeatures xsi:type="ecore:EReference" name="expression" eType="#//SMTTerm"
+        containment="true"/>
+    <eStructuralFeatures xsi:type="ecore:EReference" name="pattern" eType="#//SMTTerm"
+        containment="true"/>
+  </eClassifiers>
+  <eClassifiers xsi:type="ecore:EClass" name="SMTExists" eSuperTypes="#//SMTQuantifiedExpression"/>
+  <eClassifiers xsi:type="ecore:EClass" name="SMTForall" eSuperTypes="#//SMTQuantifiedExpression"/>
+  <eClassifiers xsi:type="ecore:EClass" name="SMTBoolOperation" eSuperTypes="#//SMTTerm"/>
+  <eClassifiers xsi:type="ecore:EClass" name="SMTAnd" eSuperTypes="#//SMTBoolOperation">
+    <eStructuralFeatures xsi:type="ecore:EReference" name="operands" upperBound="-1"
+        eType="#//SMTTerm" containment="true"/>
+  </eClassifiers>
+  <eClassifiers xsi:type="ecore:EClass" name="SMTOr" eSuperTypes="#//SMTBoolOperation">
+    <eStructuralFeatures xsi:type="ecore:EReference" name="operands" upperBound="-1"
+        eType="#//SMTTerm" containment="true"/>
+  </eClassifiers>
+  <eClassifiers xsi:type="ecore:EClass" name="SMTImpl" eSuperTypes="#//SMTBoolOperation">
+    <eStructuralFeatures xsi:type="ecore:EReference" name="leftOperand" eType="#//SMTTerm"
+        containment="true"/>
+    <eStructuralFeatures xsi:type="ecore:EReference" name="rightOperand" eType="#//SMTTerm"
+        containment="true"/>
+  </eClassifiers>
+  <eClassifiers xsi:type="ecore:EClass" name="SMTNot" eSuperTypes="#//SMTBoolOperation">
+    <eStructuralFeatures xsi:type="ecore:EReference" name="operand" eType="#//SMTTerm"
+        containment="true"/>
+  </eClassifiers>
+  <eClassifiers xsi:type="ecore:EClass" name="SMTIff" eSuperTypes="#//SMTBoolOperation">
+    <eStructuralFeatures xsi:type="ecore:EReference" name="leftOperand" eType="#//SMTTerm"
+        containment="true"/>
+    <eStructuralFeatures xsi:type="ecore:EReference" name="rightOperand" eType="#//SMTTerm"
+        containment="true"/>
+  </eClassifiers>
+  <eClassifiers xsi:type="ecore:EClass" name="SMTITE" eSuperTypes="#//SMTTerm">
+    <eStructuralFeatures xsi:type="ecore:EReference" name="condition" eType="#//SMTTerm"
+        containment="true"/>
+    <eStructuralFeatures xsi:type="ecore:EReference" name="if" eType="#//SMTTerm"
+        containment="true"/>
+    <eStructuralFeatures xsi:type="ecore:EReference" name="else" eType="#//SMTTerm"
+        containment="true"/>
+  </eClassifiers>
+  <eClassifiers xsi:type="ecore:EClass" name="SMTLet" eSuperTypes="#//SMTTerm">
+    <eStructuralFeatures xsi:type="ecore:EReference" name="inlineConstantDefinitions"
+        upperBound="-1" eType="#//SMTInlineConstantDefinition" containment="true"/>
+    <eStructuralFeatures xsi:type="ecore:EReference" name="term" eType="#//SMTTerm"
+        containment="true"/>
+  </eClassifiers>
+  <eClassifiers xsi:type="ecore:EClass" name="SMTInlineConstantDefinition" eSuperTypes="#//SMTSymbolicDeclaration">
+    <eStructuralFeatures xsi:type="ecore:EReference" name="definition" eType="#//SMTTerm"
+        containment="true"/>
+  </eClassifiers>
+  <eClassifiers xsi:type="ecore:EClass" name="SMTRelation" eSuperTypes="#//SMTTerm"/>
+  <eClassifiers xsi:type="ecore:EClass" name="SMTEquals" eSuperTypes="#//SMTRelation">
+    <eStructuralFeatures xsi:type="ecore:EReference" name="leftOperand" eType="#//SMTTerm"
+        containment="true"/>
+    <eStructuralFeatures xsi:type="ecore:EReference" name="rightOperand" eType="#//SMTTerm"
+        containment="true"/>
+  </eClassifiers>
+  <eClassifiers xsi:type="ecore:EClass" name="SMTDistinct" eSuperTypes="#//SMTRelation">
+    <eStructuralFeatures xsi:type="ecore:EReference" name="operands" upperBound="-1"
+        eType="#//SMTTerm" containment="true"/>
+  </eClassifiers>
+  <eClassifiers xsi:type="ecore:EClass" name="SMTLT" eSuperTypes="#//SMTRelation">
+    <eStructuralFeatures xsi:type="ecore:EReference" name="leftOperand" eType="#//SMTTerm"
+        containment="true"/>
+    <eStructuralFeatures xsi:type="ecore:EReference" name="rightOperand" eType="#//SMTTerm"
+        containment="true"/>
+  </eClassifiers>
+  <eClassifiers xsi:type="ecore:EClass" name="SMTMT" eSuperTypes="#//SMTRelation">
+    <eStructuralFeatures xsi:type="ecore:EReference" name="leftOperand" eType="#//SMTTerm"
+        containment="true"/>
+    <eStructuralFeatures xsi:type="ecore:EReference" name="rightOperand" eType="#//SMTTerm"
+        containment="true"/>
+  </eClassifiers>
+  <eClassifiers xsi:type="ecore:EClass" name="SMTLEQ" eSuperTypes="#//SMTRelation">
+    <eStructuralFeatures xsi:type="ecore:EReference" name="leftOperand" eType="#//SMTTerm"
+        containment="true"/>
+    <eStructuralFeatures xsi:type="ecore:EReference" name="rightOperand" eType="#//SMTTerm"
+        containment="true"/>
+  </eClassifiers>
+  <eClassifiers xsi:type="ecore:EClass" name="SMTMEQ" eSuperTypes="#//SMTRelation">
+    <eStructuralFeatures xsi:type="ecore:EReference" name="leftOperand" eType="#//SMTTerm"
+        containment="true"/>
+    <eStructuralFeatures xsi:type="ecore:EReference" name="rightOperand" eType="#//SMTTerm"
+        containment="true"/>
+  </eClassifiers>
+  <eClassifiers xsi:type="ecore:EClass" name="SMTIntOperation" eSuperTypes="#//SMTTerm">
+    <eStructuralFeatures xsi:type="ecore:EReference" name="leftOperand" eType="#//SMTTerm"
+        containment="true"/>
+    <eStructuralFeatures xsi:type="ecore:EReference" name="rightOperand" eType="#//SMTTerm"
+        containment="true"/>
+  </eClassifiers>
+  <eClassifiers xsi:type="ecore:EClass" name="SMTPlus" eSuperTypes="#//SMTIntOperation"/>
+  <eClassifiers xsi:type="ecore:EClass" name="SMTMinus" eSuperTypes="#//SMTIntOperation"/>
+  <eClassifiers xsi:type="ecore:EClass" name="SMTMultiply" eSuperTypes="#//SMTIntOperation"/>
+  <eClassifiers xsi:type="ecore:EClass" name="SMTDivison" eSuperTypes="#//SMTIntOperation"/>
+  <eClassifiers xsi:type="ecore:EClass" name="SMTDiv" eSuperTypes="#//SMTIntOperation"/>
+  <eClassifiers xsi:type="ecore:EClass" name="SMTMod" eSuperTypes="#//SMTIntOperation"/>
+  <eClassifiers xsi:type="ecore:EClass" name="SMTAssertion">
+    <eStructuralFeatures xsi:type="ecore:EReference" name="value" eType="#//SMTTerm"
+        containment="true"/>
+  </eClassifiers>
+  <eClassifiers xsi:type="ecore:EClass" name="SMTCardinalityConstraint">
+    <eStructuralFeatures xsi:type="ecore:EReference" name="type" eType="#//SMTTypeReference"
+        containment="true"/>
+    <eStructuralFeatures xsi:type="ecore:EReference" name="elements" upperBound="-1"
+        eType="#//SMTSymbolicValue" containment="true"/>
+  </eClassifiers>
+  <eClassifiers xsi:type="ecore:EClass" name="SMTSatCommand"/>
+  <eClassifiers xsi:type="ecore:EClass" name="SMTSimpleSatCommand" eSuperTypes="#//SMTSatCommand"/>
+  <eClassifiers xsi:type="ecore:EClass" name="SMTComplexSatCommand" eSuperTypes="#//SMTSatCommand">
+    <eStructuralFeatures xsi:type="ecore:EReference" name="method" eType="#//SMTReasoningTactic"
+        containment="true"/>
+  </eClassifiers>
+  <eClassifiers xsi:type="ecore:EClass" name="SMTGetModelCommand"/>
+  <eClassifiers xsi:type="ecore:EClass" name="SMTReasoningTactic"/>
+  <eClassifiers xsi:type="ecore:EClass" name="SMTBuiltinTactic" eSuperTypes="#//SMTReasoningTactic">
+    <eStructuralFeatures xsi:type="ecore:EAttribute" name="name" eType="ecore:EDataType http://www.eclipse.org/emf/2002/Ecore#//EString"/>
+  </eClassifiers>
+  <eClassifiers xsi:type="ecore:EClass" name="SMTReasoningCombinator" eSuperTypes="#//SMTReasoningTactic"/>
+  <eClassifiers xsi:type="ecore:EClass" name="SMTAndThenCombinator" eSuperTypes="#//SMTReasoningCombinator">
+    <eStructuralFeatures xsi:type="ecore:EReference" name="tactics" upperBound="-1"
+        eType="#//SMTReasoningTactic" containment="true"/>
+  </eClassifiers>
+  <eClassifiers xsi:type="ecore:EClass" name="SMTOrElseCombinator" eSuperTypes="#//SMTReasoningCombinator">
+    <eStructuralFeatures xsi:type="ecore:EReference" name="tactics" upperBound="-1"
+        eType="#//SMTReasoningTactic" containment="true"/>
+  </eClassifiers>
+  <eClassifiers xsi:type="ecore:EClass" name="SMTParOrCombinator" eSuperTypes="#//SMTReasoningCombinator">
+    <eStructuralFeatures xsi:type="ecore:EReference" name="tactics" upperBound="-1"
+        eType="#//SMTReasoningTactic" containment="true"/>
+  </eClassifiers>
+  <eClassifiers xsi:type="ecore:EClass" name="SMTParThenCombinator" eSuperTypes="#//SMTReasoningCombinator">
+    <eStructuralFeatures xsi:type="ecore:EReference" name="preProcessingTactic" eType="#//SMTReasoningTactic"
+        containment="true"/>
+    <eStructuralFeatures xsi:type="ecore:EReference" name="paralellyPostpricessingTactic"
+        eType="#//SMTReasoningTactic" containment="true"/>
+  </eClassifiers>
+  <eClassifiers xsi:type="ecore:EClass" name="SMTTryForCombinator" eSuperTypes="#//SMTReasoningCombinator">
+    <eStructuralFeatures xsi:type="ecore:EReference" name="tactic" eType="#//SMTReasoningTactic"
+        containment="true"/>
+    <eStructuralFeatures xsi:type="ecore:EAttribute" name="time" eType="ecore:EDataType http://www.eclipse.org/emf/2002/Ecore#//EInt"/>
+  </eClassifiers>
+  <eClassifiers xsi:type="ecore:EClass" name="SMTIfCombinator" eSuperTypes="#//SMTReasoningCombinator">
+    <eStructuralFeatures xsi:type="ecore:EReference" name="probe" eType="#//ReasoningProbe"
+        containment="true"/>
+    <eStructuralFeatures xsi:type="ecore:EReference" name="ifTactic" eType="#//SMTReasoningTactic"
+        containment="true"/>
+    <eStructuralFeatures xsi:type="ecore:EReference" name="elseTactic" eType="#//SMTReasoningTactic"
+        containment="true"/>
+  </eClassifiers>
+  <eClassifiers xsi:type="ecore:EClass" name="SMTWhenCombinator" eSuperTypes="#//SMTReasoningCombinator">
+    <eStructuralFeatures xsi:type="ecore:EReference" name="probe" eType="#//ReasoningProbe"
+        containment="true"/>
+    <eStructuralFeatures xsi:type="ecore:EReference" name="tactic" eType="#//SMTReasoningTactic"
+        containment="true"/>
+  </eClassifiers>
+  <eClassifiers xsi:type="ecore:EClass" name="SMTFailIfCombinator" eSuperTypes="#//SMTReasoningCombinator">
+    <eStructuralFeatures xsi:type="ecore:EReference" name="probe" eType="#//ReasoningProbe"
+        containment="true"/>
+  </eClassifiers>
+  <eClassifiers xsi:type="ecore:EClass" name="SMTUsingParamCombinator" eSuperTypes="#//SMTReasoningCombinator">
+    <eStructuralFeatures xsi:type="ecore:EReference" name="tactic" eType="#//SMTReasoningTactic"
+        containment="true"/>
+    <eStructuralFeatures xsi:type="ecore:EReference" name="parameters" upperBound="-1"
+        eType="#//ReasoningTacticParameter" containment="true"/>
+  </eClassifiers>
+  <eClassifiers xsi:type="ecore:EClass" name="ReasoningProbe">
+    <eStructuralFeatures xsi:type="ecore:EAttribute" name="name" eType="ecore:EDataType http://www.eclipse.org/emf/2002/Ecore#//EString"/>
+  </eClassifiers>
+  <eClassifiers xsi:type="ecore:EClass" name="ReasoningTacticParameter">
+    <eStructuralFeatures xsi:type="ecore:EAttribute" name="name" eType="ecore:EDataType http://www.eclipse.org/emf/2002/Ecore#//EString"/>
+    <eStructuralFeatures xsi:type="ecore:EReference" name="value" eType="#//SMTAtomicTerm"
+        containment="true"/>
+  </eClassifiers>
+  <eClassifiers xsi:type="ecore:EClass" name="SMTResult"/>
+  <eClassifiers xsi:type="ecore:EClass" name="SMTErrorResult" eSuperTypes="#//SMTResult">
+    <eStructuralFeatures xsi:type="ecore:EAttribute" name="message" eType="ecore:EDataType http://www.eclipse.org/emf/2002/Ecore#//EString"/>
+  </eClassifiers>
+  <eClassifiers xsi:type="ecore:EClass" name="SMTUnsupportedResult" eSuperTypes="#//SMTResult">
+    <eStructuralFeatures xsi:type="ecore:EAttribute" name="command" eType="ecore:EDataType http://www.eclipse.org/emf/2002/Ecore#//EString"/>
+  </eClassifiers>
+  <eClassifiers xsi:type="ecore:EClass" name="SMTSatResult" eSuperTypes="#//SMTResult">
+    <eStructuralFeatures xsi:type="ecore:EAttribute" name="sat" eType="ecore:EDataType http://www.eclipse.org/emf/2002/Ecore#//EBoolean"/>
+    <eStructuralFeatures xsi:type="ecore:EAttribute" name="unsat" eType="ecore:EDataType http://www.eclipse.org/emf/2002/Ecore#//EBoolean"/>
+    <eStructuralFeatures xsi:type="ecore:EAttribute" name="unknown" eType="ecore:EDataType http://www.eclipse.org/emf/2002/Ecore#//EBoolean"/>
+  </eClassifiers>
+  <eClassifiers xsi:type="ecore:EClass" name="SMTModelResult" eSuperTypes="#//SMTResult">
+    <eStructuralFeatures xsi:type="ecore:EReference" name="newFunctionDeclarations"
+        upperBound="-1" eType="#//SMTFunctionDeclaration" containment="true"/>
+    <eStructuralFeatures xsi:type="ecore:EReference" name="typeDefinitions" upperBound="-1"
+        eType="#//SMTCardinalityConstraint" containment="true"/>
+    <eStructuralFeatures xsi:type="ecore:EReference" name="newFunctionDefinitions"
+        upperBound="-1" eType="#//SMTFunctionDefinition" containment="true"/>
+  </eClassifiers>
+  <eClassifiers xsi:type="ecore:EClass" name="SMTStatisticValue">
+    <eStructuralFeatures xsi:type="ecore:EAttribute" name="name" eType="ecore:EDataType http://www.eclipse.org/emf/2002/Ecore#//EString"/>
+  </eClassifiers>
+  <eClassifiers xsi:type="ecore:EClass" name="SMTStatisticIntValue" eSuperTypes="#//SMTStatisticValue">
+    <eStructuralFeatures xsi:type="ecore:EAttribute" name="value" eType="ecore:EDataType http://www.eclipse.org/emf/2002/Ecore#//EInt"/>
+  </eClassifiers>
+  <eClassifiers xsi:type="ecore:EClass" name="SMTStatisticDoubleValue" eSuperTypes="#//SMTStatisticValue">
+    <eStructuralFeatures xsi:type="ecore:EAttribute" name="value" eType="ecore:EDataType http://www.eclipse.org/emf/2002/Ecore#//EBigDecimal"/>
+  </eClassifiers>
+  <eClassifiers xsi:type="ecore:EClass" name="SMTStatisticsSection">
+    <eStructuralFeatures xsi:type="ecore:EReference" name="values" upperBound="-1"
+        eType="#//SMTStatisticValue" containment="true"/>
+  </eClassifiers>
+</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 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<genmodel:GenModel xmi:version="2.0" xmlns:xmi="http://www.omg.org/XMI" xmlns:ecore="http://www.eclipse.org/emf/2002/Ecore"
+    xmlns:genmodel="http://www.eclipse.org/emf/2002/GenModel" modelDirectory="/hu.bme.mit.inf.dslreasoner.smt.language/src-gen"
+    editDirectory="/hu.bme.mit.inf.dslreasoner.smt.language.edit/src" editorDirectory="/hu.bme.mit.inf.dslreasoner.smt.language.editor/src"
+    modelPluginID="hu.bme.mit.inf.dslreasoner.smt.language" forceOverwrite="true"
+    modelName="SmtLanguage" updateClasspath="false" rootExtendsClass="org.eclipse.emf.ecore.impl.MinimalEObjectImpl$Container"
+    complianceLevel="5.0" copyrightFields="false" editPluginID="hu.bme.mit.inf.dslreasoner.smt.language.edit"
+    editorPluginID="hu.bme.mit.inf.dslreasoner.smt.language.editor" runtimeVersion="2.10">
+  <genPackages prefix="SmtLanguage" basePackage="hu.bme.mit.inf.dslreasoner" disposableProviderFactory="true"
+      fileExtensions="smt2" ecorePackage="SmtLanguage.ecore#/">
+    <genClasses ecoreClass="SmtLanguage.ecore#//SMTDocument">
+      <genFeatures property="None" children="true" createChild="true" ecoreFeature="ecore:EReference SmtLanguage.ecore#//SMTDocument/input"/>
+      <genFeatures property="None" children="true" createChild="true" ecoreFeature="ecore:EReference SmtLanguage.ecore#//SMTDocument/output"/>
+    </genClasses>
+    <genClasses ecoreClass="SmtLanguage.ecore#//SMTInput">
+      <genFeatures property="None" children="true" createChild="true" ecoreFeature="ecore:EReference SmtLanguage.ecore#//SMTInput/options"/>
+      <genFeatures property="None" children="true" createChild="true" ecoreFeature="ecore:EReference SmtLanguage.ecore#//SMTInput/typeDeclarations"/>
+      <genFeatures property="None" children="true" createChild="true" ecoreFeature="ecore:EReference SmtLanguage.ecore#//SMTInput/functionDeclarations"/>
+      <genFeatures property="None" children="true" createChild="true" ecoreFeature="ecore:EReference SmtLanguage.ecore#//SMTInput/functionDefinition"/>
+      <genFeatures property="None" children="true" createChild="true" ecoreFeature="ecore:EReference SmtLanguage.ecore#//SMTInput/assertions"/>
+      <genFeatures property="None" children="true" createChild="true" ecoreFeature="ecore:EReference SmtLanguage.ecore#//SMTInput/satCommand"/>
+      <genFeatures property="None" children="true" createChild="true" ecoreFeature="ecore:EReference SmtLanguage.ecore#//SMTInput/getModelCommand"/>
+    </genClasses>
+    <genClasses ecoreClass="SmtLanguage.ecore#//SMTOutput">
+      <genFeatures property="None" children="true" createChild="true" ecoreFeature="ecore:EReference SmtLanguage.ecore#//SMTOutput/satResult"/>
+      <genFeatures property="None" children="true" createChild="true" ecoreFeature="ecore:EReference SmtLanguage.ecore#//SMTOutput/getModelResult"/>
+      <genFeatures property="None" children="true" createChild="true" ecoreFeature="ecore:EReference SmtLanguage.ecore#//SMTOutput/statistics"/>
+    </genClasses>
+    <genClasses ecoreClass="SmtLanguage.ecore#//SMTOption">
+      <genFeatures createChild="false" ecoreFeature="ecore:EAttribute SmtLanguage.ecore#//SMTOption/name"/>
+      <genFeatures property="None" children="true" createChild="true" ecoreFeature="ecore:EReference SmtLanguage.ecore#//SMTOption/value"/>
+    </genClasses>
+    <genClasses ecoreClass="SmtLanguage.ecore#//SMTType">
+      <genFeatures createChild="false" ecoreFeature="ecore:EAttribute SmtLanguage.ecore#//SMTType/name"/>
+    </genClasses>
+    <genClasses ecoreClass="SmtLanguage.ecore#//SMTEnumLiteral"/>
+    <genClasses ecoreClass="SmtLanguage.ecore#//SMTEnumeratedTypeDeclaration">
+      <genFeatures property="None" children="true" createChild="true" ecoreFeature="ecore:EReference SmtLanguage.ecore#//SMTEnumeratedTypeDeclaration/elements"/>
+    </genClasses>
+    <genClasses ecoreClass="SmtLanguage.ecore#//SMTSetTypeDeclaration"/>
+    <genClasses ecoreClass="SmtLanguage.ecore#//SMTTypeReference"/>
+    <genClasses ecoreClass="SmtLanguage.ecore#//SMTComplexTypeReference">
+      <genFeatures notify="false" createChild="false" propertySortChoices="true" ecoreFeature="ecore:EReference SmtLanguage.ecore#//SMTComplexTypeReference/referred"/>
+    </genClasses>
+    <genClasses ecoreClass="SmtLanguage.ecore#//SMTPrimitiveTypeReference"/>
+    <genClasses ecoreClass="SmtLanguage.ecore#//SMTIntTypeReference"/>
+    <genClasses ecoreClass="SmtLanguage.ecore#//SMTBoolTypeReference"/>
+    <genClasses ecoreClass="SmtLanguage.ecore#//SMTRealTypeReference"/>
+    <genClasses ecoreClass="SmtLanguage.ecore#//SMTFunctionDeclaration">
+      <genFeatures property="None" children="true" createChild="true" ecoreFeature="ecore:EReference SmtLanguage.ecore#//SMTFunctionDeclaration/parameters"/>
+      <genFeatures property="None" children="true" createChild="true" ecoreFeature="ecore:EReference SmtLanguage.ecore#//SMTFunctionDeclaration/range"/>
+    </genClasses>
+    <genClasses ecoreClass="SmtLanguage.ecore#//SMTFunctionDefinition">
+      <genFeatures property="None" children="true" createChild="true" ecoreFeature="ecore:EReference SmtLanguage.ecore#//SMTFunctionDefinition/parameters"/>
+      <genFeatures property="None" children="true" createChild="true" ecoreFeature="ecore:EReference SmtLanguage.ecore#//SMTFunctionDefinition/range"/>
+      <genFeatures property="None" children="true" createChild="true" ecoreFeature="ecore:EReference SmtLanguage.ecore#//SMTFunctionDefinition/value"/>
+    </genClasses>
+    <genClasses ecoreClass="SmtLanguage.ecore#//SMTTerm"/>
+    <genClasses ecoreClass="SmtLanguage.ecore#//SMTSymbolicDeclaration">
+      <genFeatures createChild="false" ecoreFeature="ecore:EAttribute SmtLanguage.ecore#//SMTSymbolicDeclaration/name"/>
+    </genClasses>
+    <genClasses ecoreClass="SmtLanguage.ecore#//SMTSymbolicValue">
+      <genFeatures notify="false" createChild="false" propertySortChoices="true" ecoreFeature="ecore:EReference SmtLanguage.ecore#//SMTSymbolicValue/symbolicReference"/>
+      <genFeatures property="None" children="true" createChild="true" ecoreFeature="ecore:EReference SmtLanguage.ecore#//SMTSymbolicValue/parameterSubstitutions"/>
+    </genClasses>
+    <genClasses ecoreClass="SmtLanguage.ecore#//SMTAtomicTerm"/>
+    <genClasses ecoreClass="SmtLanguage.ecore#//SMTIntLiteral">
+      <genFeatures createChild="false" ecoreFeature="ecore:EAttribute SmtLanguage.ecore#//SMTIntLiteral/value"/>
+    </genClasses>
+    <genClasses ecoreClass="SmtLanguage.ecore#//SMTBoolLiteral">
+      <genFeatures createChild="false" ecoreFeature="ecore:EAttribute SmtLanguage.ecore#//SMTBoolLiteral/value"/>
+    </genClasses>
+    <genClasses ecoreClass="SmtLanguage.ecore#//SMTRealLiteral">
+      <genFeatures createChild="false" ecoreFeature="ecore:EAttribute SmtLanguage.ecore#//SMTRealLiteral/value"/>
+    </genClasses>
+    <genClasses ecoreClass="SmtLanguage.ecore#//SMTSortedVariable">
+      <genFeatures property="None" children="true" createChild="true" ecoreFeature="ecore:EReference SmtLanguage.ecore#//SMTSortedVariable/range"/>
+    </genClasses>
+    <genClasses ecoreClass="SmtLanguage.ecore#//SMTQuantifiedExpression">
+      <genFeatures property="None" children="true" createChild="true" ecoreFeature="ecore:EReference SmtLanguage.ecore#//SMTQuantifiedExpression/quantifiedVariables"/>
+      <genFeatures property="None" children="true" createChild="true" ecoreFeature="ecore:EReference SmtLanguage.ecore#//SMTQuantifiedExpression/expression"/>
+      <genFeatures property="None" children="true" createChild="true" ecoreFeature="ecore:EReference SmtLanguage.ecore#//SMTQuantifiedExpression/pattern"/>
+    </genClasses>
+    <genClasses ecoreClass="SmtLanguage.ecore#//SMTExists"/>
+    <genClasses ecoreClass="SmtLanguage.ecore#//SMTForall"/>
+    <genClasses ecoreClass="SmtLanguage.ecore#//SMTBoolOperation"/>
+    <genClasses ecoreClass="SmtLanguage.ecore#//SMTAnd">
+      <genFeatures property="None" children="true" createChild="true" ecoreFeature="ecore:EReference SmtLanguage.ecore#//SMTAnd/operands"/>
+    </genClasses>
+    <genClasses ecoreClass="SmtLanguage.ecore#//SMTOr">
+      <genFeatures property="None" children="true" createChild="true" ecoreFeature="ecore:EReference SmtLanguage.ecore#//SMTOr/operands"/>
+    </genClasses>
+    <genClasses ecoreClass="SmtLanguage.ecore#//SMTImpl">
+      <genFeatures property="None" children="true" createChild="true" ecoreFeature="ecore:EReference SmtLanguage.ecore#//SMTImpl/leftOperand"/>
+      <genFeatures property="None" children="true" createChild="true" ecoreFeature="ecore:EReference SmtLanguage.ecore#//SMTImpl/rightOperand"/>
+    </genClasses>
+    <genClasses ecoreClass="SmtLanguage.ecore#//SMTNot">
+      <genFeatures property="None" children="true" createChild="true" ecoreFeature="ecore:EReference SmtLanguage.ecore#//SMTNot/operand"/>
+    </genClasses>
+    <genClasses ecoreClass="SmtLanguage.ecore#//SMTIff">
+      <genFeatures property="None" children="true" createChild="true" ecoreFeature="ecore:EReference SmtLanguage.ecore#//SMTIff/leftOperand"/>
+      <genFeatures property="None" children="true" createChild="true" ecoreFeature="ecore:EReference SmtLanguage.ecore#//SMTIff/rightOperand"/>
+    </genClasses>
+    <genClasses ecoreClass="SmtLanguage.ecore#//SMTITE">
+      <genFeatures property="None" children="true" createChild="true" ecoreFeature="ecore:EReference SmtLanguage.ecore#//SMTITE/condition"/>
+      <genFeatures property="None" children="true" createChild="true" ecoreFeature="ecore:EReference SmtLanguage.ecore#//SMTITE/if"/>
+      <genFeatures property="None" children="true" createChild="true" ecoreFeature="ecore:EReference SmtLanguage.ecore#//SMTITE/else"/>
+    </genClasses>
+    <genClasses ecoreClass="SmtLanguage.ecore#//SMTLet">
+      <genFeatures property="None" children="true" createChild="true" ecoreFeature="ecore:EReference SmtLanguage.ecore#//SMTLet/inlineConstantDefinitions"/>
+      <genFeatures property="None" children="true" createChild="true" ecoreFeature="ecore:EReference SmtLanguage.ecore#//SMTLet/term"/>
+    </genClasses>
+    <genClasses ecoreClass="SmtLanguage.ecore#//SMTInlineConstantDefinition">
+      <genFeatures property="None" children="true" createChild="true" ecoreFeature="ecore:EReference SmtLanguage.ecore#//SMTInlineConstantDefinition/definition"/>
+    </genClasses>
+    <genClasses ecoreClass="SmtLanguage.ecore#//SMTRelation"/>
+    <genClasses ecoreClass="SmtLanguage.ecore#//SMTEquals">
+      <genFeatures property="None" children="true" createChild="true" ecoreFeature="ecore:EReference SmtLanguage.ecore#//SMTEquals/leftOperand"/>
+      <genFeatures property="None" children="true" createChild="true" ecoreFeature="ecore:EReference SmtLanguage.ecore#//SMTEquals/rightOperand"/>
+    </genClasses>
+    <genClasses ecoreClass="SmtLanguage.ecore#//SMTDistinct">
+      <genFeatures property="None" children="true" createChild="true" ecoreFeature="ecore:EReference SmtLanguage.ecore#//SMTDistinct/operands"/>
+    </genClasses>
+    <genClasses ecoreClass="SmtLanguage.ecore#//SMTLT">
+      <genFeatures property="None" children="true" createChild="true" ecoreFeature="ecore:EReference SmtLanguage.ecore#//SMTLT/leftOperand"/>
+      <genFeatures property="None" children="true" createChild="true" ecoreFeature="ecore:EReference SmtLanguage.ecore#//SMTLT/rightOperand"/>
+    </genClasses>
+    <genClasses ecoreClass="SmtLanguage.ecore#//SMTMT">
+      <genFeatures property="None" children="true" createChild="true" ecoreFeature="ecore:EReference SmtLanguage.ecore#//SMTMT/leftOperand"/>
+      <genFeatures property="None" children="true" createChild="true" ecoreFeature="ecore:EReference SmtLanguage.ecore#//SMTMT/rightOperand"/>
+    </genClasses>
+    <genClasses ecoreClass="SmtLanguage.ecore#//SMTLEQ">
+      <genFeatures property="None" children="true" createChild="true" ecoreFeature="ecore:EReference SmtLanguage.ecore#//SMTLEQ/leftOperand"/>
+      <genFeatures property="None" children="true" createChild="true" ecoreFeature="ecore:EReference SmtLanguage.ecore#//SMTLEQ/rightOperand"/>
+    </genClasses>
+    <genClasses ecoreClass="SmtLanguage.ecore#//SMTMEQ">
+      <genFeatures property="None" children="true" createChild="true" ecoreFeature="ecore:EReference SmtLanguage.ecore#//SMTMEQ/leftOperand"/>
+      <genFeatures property="None" children="true" createChild="true" ecoreFeature="ecore:EReference SmtLanguage.ecore#//SMTMEQ/rightOperand"/>
+    </genClasses>
+    <genClasses ecoreClass="SmtLanguage.ecore#//SMTIntOperation">
+      <genFeatures property="None" children="true" createChild="true" ecoreFeature="ecore:EReference SmtLanguage.ecore#//SMTIntOperation/leftOperand"/>
+      <genFeatures property="None" children="true" createChild="true" ecoreFeature="ecore:EReference SmtLanguage.ecore#//SMTIntOperation/rightOperand"/>
+    </genClasses>
+    <genClasses ecoreClass="SmtLanguage.ecore#//SMTPlus"/>
+    <genClasses ecoreClass="SmtLanguage.ecore#//SMTMinus"/>
+    <genClasses ecoreClass="SmtLanguage.ecore#//SMTMultiply"/>
+    <genClasses ecoreClass="SmtLanguage.ecore#//SMTDivison"/>
+    <genClasses ecoreClass="SmtLanguage.ecore#//SMTDiv"/>
+    <genClasses ecoreClass="SmtLanguage.ecore#//SMTMod"/>
+    <genClasses ecoreClass="SmtLanguage.ecore#//SMTAssertion">
+      <genFeatures property="None" children="true" createChild="true" ecoreFeature="ecore:EReference SmtLanguage.ecore#//SMTAssertion/value"/>
+    </genClasses>
+    <genClasses ecoreClass="SmtLanguage.ecore#//SMTCardinalityConstraint">
+      <genFeatures property="None" children="true" createChild="true" ecoreFeature="ecore:EReference SmtLanguage.ecore#//SMTCardinalityConstraint/type"/>
+      <genFeatures property="None" children="true" createChild="true" ecoreFeature="ecore:EReference SmtLanguage.ecore#//SMTCardinalityConstraint/elements"/>
+    </genClasses>
+    <genClasses ecoreClass="SmtLanguage.ecore#//SMTSatCommand"/>
+    <genClasses ecoreClass="SmtLanguage.ecore#//SMTSimpleSatCommand"/>
+    <genClasses ecoreClass="SmtLanguage.ecore#//SMTComplexSatCommand">
+      <genFeatures property="None" children="true" createChild="true" ecoreFeature="ecore:EReference SmtLanguage.ecore#//SMTComplexSatCommand/method"/>
+    </genClasses>
+    <genClasses ecoreClass="SmtLanguage.ecore#//SMTGetModelCommand"/>
+    <genClasses ecoreClass="SmtLanguage.ecore#//SMTReasoningTactic"/>
+    <genClasses ecoreClass="SmtLanguage.ecore#//SMTBuiltinTactic">
+      <genFeatures createChild="false" ecoreFeature="ecore:EAttribute SmtLanguage.ecore#//SMTBuiltinTactic/name"/>
+    </genClasses>
+    <genClasses ecoreClass="SmtLanguage.ecore#//SMTReasoningCombinator"/>
+    <genClasses ecoreClass="SmtLanguage.ecore#//SMTAndThenCombinator">
+      <genFeatures property="None" children="true" createChild="true" ecoreFeature="ecore:EReference SmtLanguage.ecore#//SMTAndThenCombinator/tactics"/>
+    </genClasses>
+    <genClasses ecoreClass="SmtLanguage.ecore#//SMTOrElseCombinator">
+      <genFeatures property="None" children="true" createChild="true" ecoreFeature="ecore:EReference SmtLanguage.ecore#//SMTOrElseCombinator/tactics"/>
+    </genClasses>
+    <genClasses ecoreClass="SmtLanguage.ecore#//SMTParOrCombinator">
+      <genFeatures property="None" children="true" createChild="true" ecoreFeature="ecore:EReference SmtLanguage.ecore#//SMTParOrCombinator/tactics"/>
+    </genClasses>
+    <genClasses ecoreClass="SmtLanguage.ecore#//SMTParThenCombinator">
+      <genFeatures property="None" children="true" createChild="true" ecoreFeature="ecore:EReference SmtLanguage.ecore#//SMTParThenCombinator/preProcessingTactic"/>
+      <genFeatures property="None" children="true" createChild="true" ecoreFeature="ecore:EReference SmtLanguage.ecore#//SMTParThenCombinator/paralellyPostpricessingTactic"/>
+    </genClasses>
+    <genClasses ecoreClass="SmtLanguage.ecore#//SMTTryForCombinator">
+      <genFeatures property="None" children="true" createChild="true" ecoreFeature="ecore:EReference SmtLanguage.ecore#//SMTTryForCombinator/tactic"/>
+      <genFeatures createChild="false" ecoreFeature="ecore:EAttribute SmtLanguage.ecore#//SMTTryForCombinator/time"/>
+    </genClasses>
+    <genClasses ecoreClass="SmtLanguage.ecore#//SMTIfCombinator">
+      <genFeatures property="None" children="true" createChild="true" ecoreFeature="ecore:EReference SmtLanguage.ecore#//SMTIfCombinator/probe"/>
+      <genFeatures property="None" children="true" createChild="true" ecoreFeature="ecore:EReference SmtLanguage.ecore#//SMTIfCombinator/ifTactic"/>
+      <genFeatures property="None" children="true" createChild="true" ecoreFeature="ecore:EReference SmtLanguage.ecore#//SMTIfCombinator/elseTactic"/>
+    </genClasses>
+    <genClasses ecoreClass="SmtLanguage.ecore#//SMTWhenCombinator">
+      <genFeatures property="None" children="true" createChild="true" ecoreFeature="ecore:EReference SmtLanguage.ecore#//SMTWhenCombinator/probe"/>
+      <genFeatures property="None" children="true" createChild="true" ecoreFeature="ecore:EReference SmtLanguage.ecore#//SMTWhenCombinator/tactic"/>
+    </genClasses>
+    <genClasses ecoreClass="SmtLanguage.ecore#//SMTFailIfCombinator">
+      <genFeatures property="None" children="true" createChild="true" ecoreFeature="ecore:EReference SmtLanguage.ecore#//SMTFailIfCombinator/probe"/>
+    </genClasses>
+    <genClasses ecoreClass="SmtLanguage.ecore#//SMTUsingParamCombinator">
+      <genFeatures property="None" children="true" createChild="true" ecoreFeature="ecore:EReference SmtLanguage.ecore#//SMTUsingParamCombinator/tactic"/>
+      <genFeatures property="None" children="true" createChild="true" ecoreFeature="ecore:EReference SmtLanguage.ecore#//SMTUsingParamCombinator/parameters"/>
+    </genClasses>
+    <genClasses ecoreClass="SmtLanguage.ecore#//ReasoningProbe">
+      <genFeatures createChild="false" ecoreFeature="ecore:EAttribute SmtLanguage.ecore#//ReasoningProbe/name"/>
+    </genClasses>
+    <genClasses ecoreClass="SmtLanguage.ecore#//ReasoningTacticParameter">
+      <genFeatures createChild="false" ecoreFeature="ecore:EAttribute SmtLanguage.ecore#//ReasoningTacticParameter/name"/>
+      <genFeatures property="None" children="true" createChild="true" ecoreFeature="ecore:EReference SmtLanguage.ecore#//ReasoningTacticParameter/value"/>
+    </genClasses>
+    <genClasses ecoreClass="SmtLanguage.ecore#//SMTResult"/>
+    <genClasses ecoreClass="SmtLanguage.ecore#//SMTErrorResult">
+      <genFeatures createChild="false" ecoreFeature="ecore:EAttribute SmtLanguage.ecore#//SMTErrorResult/message"/>
+    </genClasses>
+    <genClasses ecoreClass="SmtLanguage.ecore#//SMTUnsupportedResult">
+      <genFeatures createChild="false" ecoreFeature="ecore:EAttribute SmtLanguage.ecore#//SMTUnsupportedResult/command"/>
+    </genClasses>
+    <genClasses ecoreClass="SmtLanguage.ecore#//SMTSatResult">
+      <genFeatures createChild="false" ecoreFeature="ecore:EAttribute SmtLanguage.ecore#//SMTSatResult/sat"/>
+      <genFeatures createChild="false" ecoreFeature="ecore:EAttribute SmtLanguage.ecore#//SMTSatResult/unsat"/>
+      <genFeatures createChild="false" ecoreFeature="ecore:EAttribute SmtLanguage.ecore#//SMTSatResult/unknown"/>
+    </genClasses>
+    <genClasses ecoreClass="SmtLanguage.ecore#//SMTModelResult">
+      <genFeatures property="None" children="true" createChild="true" ecoreFeature="ecore:EReference SmtLanguage.ecore#//SMTModelResult/newFunctionDeclarations"/>
+      <genFeatures property="None" children="true" createChild="true" ecoreFeature="ecore:EReference SmtLanguage.ecore#//SMTModelResult/typeDefinitions"/>
+      <genFeatures property="None" children="true" createChild="true" ecoreFeature="ecore:EReference SmtLanguage.ecore#//SMTModelResult/newFunctionDefinitions"/>
+    </genClasses>
+    <genClasses ecoreClass="SmtLanguage.ecore#//SMTStatisticValue">
+      <genFeatures createChild="false" ecoreFeature="ecore:EAttribute SmtLanguage.ecore#//SMTStatisticValue/name"/>
+    </genClasses>
+    <genClasses ecoreClass="SmtLanguage.ecore#//SMTStatisticIntValue">
+      <genFeatures createChild="false" ecoreFeature="ecore:EAttribute SmtLanguage.ecore#//SMTStatisticIntValue/value"/>
+    </genClasses>
+    <genClasses ecoreClass="SmtLanguage.ecore#//SMTStatisticDoubleValue">
+      <genFeatures createChild="false" ecoreFeature="ecore:EAttribute SmtLanguage.ecore#//SMTStatisticDoubleValue/value"/>
+    </genClasses>
+    <genClasses ecoreClass="SmtLanguage.ecore#//SMTStatisticsSection">
+      <genFeatures property="None" children="true" createChild="true" ecoreFeature="ecore:EReference SmtLanguage.ecore#//SMTStatisticsSection/values"/>
+    </genClasses>
+  </genPackages>
+</genmodel:GenModel>
-- 
cgit v1.2.3-70-g09d2