aboutsummaryrefslogtreecommitdiffstats
path: root/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language
diff options
context:
space:
mode:
Diffstat (limited to 'Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language')
-rw-r--r--Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/.classpath9
-rw-r--r--Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/.gitignore4
-rw-r--r--Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/.launch/Generate Language Infrastructure (hu.bme.mit.inf.dslreasoner.smt.language).launch17
-rw-r--r--Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/.project34
-rw-r--r--Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/.settings/org.eclipse.core.resources.prefs2
-rw-r--r--Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/.settings/org.eclipse.jdt.core.prefs7
-rw-r--r--Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/META-INF/MANIFEST.MF37
-rw-r--r--Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/build.properties7
-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
-rw-r--r--Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/plugin.xml16
-rw-r--r--Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/plugin.xml_gen16
-rw-r--r--Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/src/hu/bme/mit/inf/dslreasoner/GenerateSmtLanguage.mwe2133
-rw-r--r--Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/src/hu/bme/mit/inf/dslreasoner/SmtLanguage.xtext222
-rw-r--r--Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/src/hu/bme/mit/inf/dslreasoner/SmtLanguageRuntimeModule.java11
-rw-r--r--Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/src/hu/bme/mit/inf/dslreasoner/SmtLanguageStandaloneSetup.java16
-rw-r--r--Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/src/hu/bme/mit/inf/dslreasoner/formatting/SmtLanguageFormatter.xtend34
-rw-r--r--Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/src/hu/bme/mit/inf/dslreasoner/generator/SmtLanguageGenerator.xtend24
-rw-r--r--Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/src/hu/bme/mit/inf/dslreasoner/scoping/SmtLanguageScopeProvider.xtend138
-rw-r--r--Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/src/hu/bme/mit/inf/dslreasoner/validation/SmtLanguageValidator.xtend24
20 files changed, 1293 insertions, 0 deletions
diff --git a/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/.classpath b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/.classpath
new file mode 100644
index 00000000..1287f96c
--- /dev/null
+++ b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/.classpath
@@ -0,0 +1,9 @@
1<?xml version="1.0" encoding="UTF-8"?>
2<classpath>
3 <classpathentry kind="src" path="src"/>
4 <classpathentry kind="src" path="src-gen"/>
5 <classpathentry kind="src" path="xtend-gen"/>
6 <classpathentry kind="con" path="org.eclipse.jdt.launching.JRE_CONTAINER/org.eclipse.jdt.internal.debug.ui.launcher.StandardVMType/JavaSE-1.8"/>
7 <classpathentry kind="con" path="org.eclipse.pde.core.requiredPlugins"/>
8 <classpathentry kind="output" path="bin"/>
9</classpath>
diff --git a/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/.gitignore b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/.gitignore
new file mode 100644
index 00000000..8ae4e44d
--- /dev/null
+++ b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/.gitignore
@@ -0,0 +1,4 @@
1/bin/
2/src-gen/
3/vql-gen/
4/xtend-gen/
diff --git a/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/.launch/Generate Language Infrastructure (hu.bme.mit.inf.dslreasoner.smt.language).launch b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/.launch/Generate Language Infrastructure (hu.bme.mit.inf.dslreasoner.smt.language).launch
new file mode 100644
index 00000000..e448edbe
--- /dev/null
+++ b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/.launch/Generate Language Infrastructure (hu.bme.mit.inf.dslreasoner.smt.language).launch
@@ -0,0 +1,17 @@
1<?xml version="1.0" encoding="UTF-8" standalone="no"?>
2<launchConfiguration type="org.eclipse.emf.mwe2.launch.Mwe2LaunchConfigurationType">
3<stringAttribute key="org.eclipse.debug.core.ATTR_REFRESH_SCOPE" value="${working_set:&lt;?xml version=&quot;1.0&quot; encoding=&quot;UTF-8&quot;?&gt;&#10;&lt;launchConfigurationWorkingSet factoryID=&quot;org.eclipse.ui.internal.WorkingSetFactory&quot; id=&quot;1299248699643_13&quot; label=&quot;working set&quot; name=&quot;working set&quot;&gt;&#10;&lt;item factoryID=&quot;org.eclipse.ui.internal.model.ResourceFactory&quot; path=&quot;/hu.bme.mit.inf.dslreasoner.smt.language&quot; type=&quot;4&quot;/&gt;&#10;&lt;item factoryID=&quot;org.eclipse.ui.internal.model.ResourceFactory&quot; path=&quot;/hu.bme.mit.inf.dslreasoner.smt.language.generator&quot; type=&quot;4&quot;/&gt;&#10;&lt;item factoryID=&quot;org.eclipse.ui.internal.model.ResourceFactory&quot; path=&quot;/hu.bme.mit.inf.dslreasoner.smt.language.tests&quot; type=&quot;4&quot;/&gt;&#10;&lt;item factoryID=&quot;org.eclipse.ui.internal.model.ResourceFactory&quot; path=&quot;/hu.bme.mit.inf.dslreasoner.smt.language.ui&quot; type=&quot;4&quot;/&gt;&#10;&lt;/launchConfigurationWorkingSet&gt;}"/>
4<listAttribute key="org.eclipse.debug.core.MAPPED_RESOURCE_PATHS">
5<listEntry value="/hu.bme.mit.inf.dslreasoner.smt.language"/>
6</listAttribute>
7<listAttribute key="org.eclipse.debug.core.MAPPED_RESOURCE_TYPES">
8<listEntry value="4"/>
9</listAttribute>
10<listAttribute key="org.eclipse.debug.ui.favoriteGroups">
11<listEntry value="org.eclipse.debug.ui.launchGroup.run"/>
12</listAttribute>
13<stringAttribute key="org.eclipse.jdt.launching.MAIN_TYPE" value="org.eclipse.emf.mwe2.launch.runtime.Mwe2Launcher"/>
14<stringAttribute key="org.eclipse.jdt.launching.PROGRAM_ARGUMENTS" value="src/hu/bme/mit/inf/dslreasoner/GenerateSmtLanguage.mwe2"/>
15<stringAttribute key="org.eclipse.jdt.launching.PROJECT_ATTR" value="hu.bme.mit.inf.dslreasoner.smt.language"/>
16<stringAttribute key="org.eclipse.jdt.launching.VM_ARGUMENTS" value="-Xmx512m"/>
17</launchConfiguration>
diff --git a/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/.project b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/.project
new file mode 100644
index 00000000..b4b09620
--- /dev/null
+++ b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/.project
@@ -0,0 +1,34 @@
1<?xml version="1.0" encoding="UTF-8"?>
2<projectDescription>
3 <name>hu.bme.mit.inf.dslreasoner.smt.language</name>
4 <comment></comment>
5 <projects>
6 </projects>
7 <buildSpec>
8 <buildCommand>
9 <name>org.eclipse.jdt.core.javabuilder</name>
10 <arguments>
11 </arguments>
12 </buildCommand>
13 <buildCommand>
14 <name>org.eclipse.pde.ManifestBuilder</name>
15 <arguments>
16 </arguments>
17 </buildCommand>
18 <buildCommand>
19 <name>org.eclipse.pde.SchemaBuilder</name>
20 <arguments>
21 </arguments>
22 </buildCommand>
23 <buildCommand>
24 <name>org.eclipse.xtext.ui.shared.xtextBuilder</name>
25 <arguments>
26 </arguments>
27 </buildCommand>
28 </buildSpec>
29 <natures>
30 <nature>org.eclipse.jdt.core.javanature</nature>
31 <nature>org.eclipse.pde.PluginNature</nature>
32 <nature>org.eclipse.xtext.ui.shared.xtextNature</nature>
33 </natures>
34</projectDescription>
diff --git a/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/.settings/org.eclipse.core.resources.prefs b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/.settings/org.eclipse.core.resources.prefs
new file mode 100644
index 00000000..4824b802
--- /dev/null
+++ b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/.settings/org.eclipse.core.resources.prefs
@@ -0,0 +1,2 @@
1eclipse.preferences.version=1
2encoding/<project>=UTF-8
diff --git a/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/.settings/org.eclipse.jdt.core.prefs b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/.settings/org.eclipse.jdt.core.prefs
new file mode 100644
index 00000000..295926d9
--- /dev/null
+++ b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/.settings/org.eclipse.jdt.core.prefs
@@ -0,0 +1,7 @@
1eclipse.preferences.version=1
2org.eclipse.jdt.core.compiler.codegen.inlineJsrBytecode=enabled
3org.eclipse.jdt.core.compiler.codegen.targetPlatform=1.8
4org.eclipse.jdt.core.compiler.compliance=1.8
5org.eclipse.jdt.core.compiler.problem.assertIdentifier=error
6org.eclipse.jdt.core.compiler.problem.enumIdentifier=error
7org.eclipse.jdt.core.compiler.source=1.8
diff --git a/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/META-INF/MANIFEST.MF b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/META-INF/MANIFEST.MF
new file mode 100644
index 00000000..ec8f78ce
--- /dev/null
+++ b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/META-INF/MANIFEST.MF
@@ -0,0 +1,37 @@
1Manifest-Version: 1.0
2Bundle-ManifestVersion: 2
3Bundle-Name: hu.bme.mit.inf.dslreasoner.smt.language
4Bundle-Vendor: My Company
5Bundle-Version: 1.0.0.qualifier
6Bundle-SymbolicName: hu.bme.mit.inf.dslreasoner.smt.language; singleton:=true
7Bundle-ActivationPolicy: lazy
8Require-Bundle: org.eclipse.xtext;visibility:=reexport,
9 org.eclipse.xtext.xbase;resolution:=optional;visibility:=reexport,
10 org.eclipse.xtext.generator;resolution:=optional,
11 org.apache.commons.logging;bundle-version="1.0.4";resolution:=optional,
12 org.eclipse.emf.codegen.ecore;resolution:=optional,
13 org.eclipse.emf.mwe.utils;resolution:=optional,
14 org.eclipse.emf.mwe2.launch;resolution:=optional,
15 org.eclipse.xtext.util,
16 org.eclipse.emf.ecore,
17 org.eclipse.emf.common,
18 org.antlr.runtime,
19 org.eclipse.xtext.common.types,
20 org.objectweb.asm;bundle-version="[5.0.1,6.0.0)";resolution:=optional,
21 org.eclipse.xtext.xbase.lib
22Import-Package: org.apache.log4j,
23 org.eclipse.xtext.xbase.lib
24Bundle-RequiredExecutionEnvironment: J2SE-1.5
25Export-Package: hu.bme.mit.inf.dslreasoner,
26 hu.bme.mit.inf.dslreasoner.services,
27 hu.bme.mit.inf.dslreasoner.smtLanguage,
28 hu.bme.mit.inf.dslreasoner.smtLanguage.impl,
29 hu.bme.mit.inf.dslreasoner.smtLanguage.util,
30 hu.bme.mit.inf.dslreasoner.serializer,
31 hu.bme.mit.inf.dslreasoner.parser.antlr,
32 hu.bme.mit.inf.dslreasoner.parser.antlr.internal,
33 hu.bme.mit.inf.dslreasoner.validation,
34 hu.bme.mit.inf.dslreasoner.scoping,
35 hu.bme.mit.inf.dslreasoner.generator,
36 hu.bme.mit.inf.dslreasoner.formatting
37
diff --git a/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/build.properties b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/build.properties
new file mode 100644
index 00000000..07a42688
--- /dev/null
+++ b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/build.properties
@@ -0,0 +1,7 @@
1source.. = src/,\
2 src-gen/,\
3 xtend-gen/
4bin.includes = model/,\
5 META-INF/,\
6 .,\
7 plugin.xml \ No newline at end of file
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>
diff --git a/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/plugin.xml b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/plugin.xml
new file mode 100644
index 00000000..fea6dabe
--- /dev/null
+++ b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/plugin.xml
@@ -0,0 +1,16 @@
1<?xml version="1.0" encoding="UTF-8"?>
2<?eclipse version="3.0"?>
3
4<plugin>
5
6 <extension point="org.eclipse.emf.ecore.generated_package">
7 <package
8 uri = "http://www.bme.hu/mit/inf/dslreasoner/SmtLanguage"
9 class = "hu.bme.mit.inf.dslreasoner.smtLanguage.SmtLanguagePackage"
10 genModel = "model/generated/SmtLanguage.genmodel" />
11
12 </extension>
13
14
15
16</plugin>
diff --git a/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/plugin.xml_gen b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/plugin.xml_gen
new file mode 100644
index 00000000..3665b60a
--- /dev/null
+++ b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/plugin.xml_gen
@@ -0,0 +1,16 @@
1<?xml version="1.0" encoding="UTF-8"?>
2<?eclipse version="3.0"?>
3
4<plugin>
5
6 <extension point="org.eclipse.emf.ecore.generated_package">
7 <package
8 uri = "http://www.bme.hu/mit/inf/dslreasoner/SmtLanguage"
9 class = "hu.bme.mit.inf.dslreasoner.smtLanguage.SmtLanguagePackage"
10 genModel = "model/generated/SmtLanguage.genmodel" />
11
12 </extension>
13
14
15
16</plugin>
diff --git a/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/src/hu/bme/mit/inf/dslreasoner/GenerateSmtLanguage.mwe2 b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/src/hu/bme/mit/inf/dslreasoner/GenerateSmtLanguage.mwe2
new file mode 100644
index 00000000..e27dbd64
--- /dev/null
+++ b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/src/hu/bme/mit/inf/dslreasoner/GenerateSmtLanguage.mwe2
@@ -0,0 +1,133 @@
1module hu.bme.mit.inf.dslreasoner.GenerateSmtLanguage
2
3import org.eclipse.emf.mwe.utils.*
4import org.eclipse.xtext.generator.*
5import org.eclipse.xtext.ui.generator.*
6
7var grammarURI = "classpath:/hu/bme/mit/inf/dslreasoner/SmtLanguage.xtext"
8var fileExtensions = "smt2"
9var projectName = "hu.bme.mit.inf.dslreasoner.smt.language"
10var runtimeProject = "../${projectName}"
11var generateXtendStub = true
12var encoding = "UTF-8"
13
14Workflow {
15 bean = StandaloneSetup {
16 scanClassPath = true
17 platformUri = "${runtimeProject}/.."
18 // The following two lines can be removed, if Xbase is not used.
19 registerGeneratedEPackage = "org.eclipse.xtext.xbase.XbasePackage"
20 registerGenModelFile = "platform:/resource/org.eclipse.xtext.xbase/model/Xbase.genmodel"
21 }
22
23 component = DirectoryCleaner {
24 directory = "${runtimeProject}/src-gen"
25 }
26
27 component = DirectoryCleaner {
28 directory = "${runtimeProject}/model/generated"
29 }
30
31 component = DirectoryCleaner {
32 directory = "${runtimeProject}.ui/src-gen"
33 }
34
35 component = DirectoryCleaner {
36 directory = "${runtimeProject}.tests/src-gen"
37 }
38
39 component = Generator {
40 pathRtProject = runtimeProject
41 pathUiProject = "${runtimeProject}.ui"
42 //pathTestProject = "${runtimeProject}.tests"
43 projectNameRt = projectName
44 projectNameUi = "${projectName}.ui"
45 encoding = encoding
46 language = auto-inject {
47 uri = grammarURI
48
49 // Java API to access grammar elements (required by several other fragments)
50 fragment = grammarAccess.GrammarAccessFragment auto-inject {}
51
52 // generates Java API for the generated EPackages
53 fragment = ecore.EMFGeneratorFragment auto-inject {}
54
55 // the old serialization component
56 // fragment = parseTreeConstructor.ParseTreeConstructorFragment auto-inject {}
57
58 // serializer 2.0
59 fragment = serializer.SerializerFragment auto-inject {
60 generateStub = false
61 }
62
63 // a custom ResourceFactory for use with EMF
64 fragment = resourceFactory.ResourceFactoryFragment auto-inject {}
65
66 // The antlr parser generator fragment.
67 fragment = parser.antlr.XtextAntlrGeneratorFragment auto-inject {
68 // options = {
69 // backtrack = true
70 // }
71 }
72
73 // Xtend-based API for validation
74 fragment = validation.ValidatorFragment auto-inject {
75 // composedCheck = "org.eclipse.xtext.validation.ImportUriValidator"
76 // composedCheck = "org.eclipse.xtext.validation.NamesAreUniqueValidator"
77 }
78
79 // old scoping and exporting API
80 // fragment = scoping.ImportURIScopingFragment auto-inject {}
81 // fragment = exporting.SimpleNamesFragment auto-inject {}
82
83 // scoping and exporting API
84 fragment = scoping.ImportNamespacesScopingFragment auto-inject {}
85 fragment = exporting.QualifiedNamesFragment auto-inject {}
86 fragment = builder.BuilderIntegrationFragment auto-inject {}
87
88 // generator API
89 fragment = generator.GeneratorFragment auto-inject {}
90
91 // formatter API
92 fragment = formatting.FormatterFragment auto-inject {}
93
94 // labeling API
95 fragment = labeling.LabelProviderFragment auto-inject {}
96
97 // outline API
98 fragment = outline.OutlineTreeProviderFragment auto-inject {}
99 fragment = outline.QuickOutlineFragment auto-inject {}
100
101 // quickfix API
102 fragment = quickfix.QuickfixProviderFragment auto-inject {}
103
104 // content assist API
105 fragment = contentAssist.ContentAssistFragment auto-inject {}
106
107 // generates a more lightweight Antlr parser and lexer tailored for content assist
108 fragment = parser.antlr.XtextAntlrUiGeneratorFragment auto-inject {}
109
110 // generates junit test support classes into Generator#pathTestProject
111 //fragment = junit.Junit4Fragment auto-inject {}
112
113 // rename refactoring
114 fragment = refactoring.RefactorElementNameFragment auto-inject {}
115
116 // provides the necessary bindings for java types integration
117 fragment = types.TypesGeneratorFragment auto-inject {}
118
119 // generates the required bindings only if the grammar inherits from Xbase
120 fragment = xbase.XbaseGeneratorFragment auto-inject {}
121
122 // generates the required bindings only if the grammar inherits from Xtype
123 fragment = xbase.XtypeGeneratorFragment auto-inject {}
124
125 // provides a preference page for template proposals
126 fragment = templates.CodetemplatesGeneratorFragment auto-inject {}
127
128 // provides a compare view
129 fragment = compare.CompareFragment auto-inject {}
130 }
131 }
132}
133
diff --git a/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/src/hu/bme/mit/inf/dslreasoner/SmtLanguage.xtext b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/src/hu/bme/mit/inf/dslreasoner/SmtLanguage.xtext
new file mode 100644
index 00000000..320e1cfe
--- /dev/null
+++ b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/src/hu/bme/mit/inf/dslreasoner/SmtLanguage.xtext
@@ -0,0 +1,222 @@
1grammar hu.bme.mit.inf.dslreasoner.SmtLanguage with org.eclipse.xtext.common.Terminals
2
3generate smtLanguage "http://www.bme.hu/mit/inf/dslreasoner/SmtLanguage"
4
5import "http://www.eclipse.org/emf/2002/Ecore" as ecore
6
7SMTDocument:
8 input=SMTInput
9 (
10 '--------------'
11 output=SMTOutput
12 )?;
13
14SMTInput:
15 (options += SMTOption)*
16 (
17 typeDeclarations+=SMTType |
18 functionDeclarations+=SMTFunctionDeclaration |
19 functionDefinition+=SMTFunctionDefinition |
20 assertions += SMTAssertion
21 )*
22 satCommand = SMTSatCommand
23 getModelCommand = SMTGetModelCommand;
24
25SMTOutput:(
26 (satResult = SMTResult
27 getModelResult = SMTResult) | 'timeout' {SMTOutput})
28 statistics=SMTStatisticsSection?;
29
30//////////////////////////////////
31// SMT terminals
32//////////////////////////////////
33
34terminal SL_COMMENT : ';' !('\n'|'\r')* ('\r'? '\n')?;
35
36terminal ID : ('a'..'z'|'A'..'Z'|'_') ('a'..'z'|'A'..'Z'|'_'|'-'|'!'|'0'..'9')*;
37// ('a'..'z'|'A'..'Z'|'_'/*|'+'|'-'|'/'|'*'|'='|'%'|'?'|'!'|'.'|'$'|'~'|'&'/*|'^'*/|'<'|'>'/*|'@'*/)
38// ('a'..'z'|'A'..'Z'|'_'/*|'+'|'-'|'/'|'*'|'='|'%'|'?'|'!'|'.'|'$'|'~'|'&'/*|'^'|*/'<'|'>'/*|'@'*/|'0'..'9')*
39SMTID: ID;
40
41terminal PROPERTYNAME : ':' + ID;
42terminal REAL returns ecore::EBigDecimal: INT '.' INT;
43
44//////////////////////////////////
45// Options
46//////////////////////////////////
47SMTOption: '(' 'set-option' name = PROPERTYNAME value = SMTAtomicTerm ')';
48
49//////////////////////////////////
50// Type declarations
51//////////////////////////////////
52SMTType: SMTEnumeratedTypeDeclaration | SMTSetTypeDeclaration;
53
54SMTEnumLiteral: name = SMTID;
55SMTEnumeratedTypeDeclaration: '(' 'declare-datatypes' '(' ')' '(' '(' name = SMTID elements+=SMTEnumLiteral+ ')' ')' ')';
56SMTSetTypeDeclaration: '(' 'declare-sort' name = SMTID ')';
57
58SMTTypeReference: SMTComplexTypeReference | SMTPrimitiveTypeReference;
59SMTComplexTypeReference: referred = [SMTType];
60SMTPrimitiveTypeReference: SMTIntTypeReference | SMTBoolTypeReference | SMTRealTypeReference;
61
62SMTIntTypeReference: {SMTIntTypeReference} "Int";
63SMTBoolTypeReference: {SMTBoolTypeReference} "Bool";
64SMTRealTypeReference: {SMTRealTypeReference} "Real";
65
66//////////////////////////////////
67// Functions and constants
68//////////////////////////////////
69
70SMTFunctionDeclaration: '(' 'declare-fun' name = SMTID '(' parameters+=SMTTypeReference* ')' range = SMTTypeReference ')';
71
72/*DeclaredFunctionDefinition:
73 '(' 'define-fun' declaration=[Function] '(' parameters+=SortedVariable* ')' range = TypeReference value = Term ')';*/
74
75SMTFunctionDefinition:
76 '(' 'define-fun' name=SMTID '(' parameters+=SMTSortedVariable* ')' range = SMTTypeReference value = SMTTerm ')';
77
78
79//////////////////////////////////
80// Expressions
81//////////////////////////////////
82SMTTerm:
83 SMTSymbolicValue|
84 SMTAtomicTerm |
85 SMTBoolOperation |
86 SMTIntOperation |
87 SMTITE |
88 SMTLet |
89 SMTRelation |
90 SMTQuantifiedExpression;
91
92SMTSymbolicDeclaration: SMTFunctionDeclaration | SMTFunctionDefinition | SMTSortedVariable | SMTEnumLiteral | SMTInlineConstantDefinition;
93
94SMTSymbolicValue:
95 '(' symbolicReference = [SMTSymbolicDeclaration] ( parameterSubstitutions += SMTTerm )+ ')' |
96 symbolicReference = [SMTSymbolicDeclaration];
97
98SMTAtomicTerm: SMTIntLiteral | SMTBoolLiteral | SMTRealLiteral;
99SMTIntLiteral: value=INT;
100BOOLEANTERMINAL returns ecore::EBoolean: 'true' | 'false';
101SMTBoolLiteral: value=BOOLEANTERMINAL;
102SMTRealLiteral: value=REAL;
103
104// Quantified operations
105SMTSortedVariable: '(' name = SMTID range = SMTTypeReference ')';
106//QuantifiedVariableValue: variable = [QuantifiedVariable];
107
108SMTQuantifiedExpression: SMTExists | SMTForall;
109SMTExists: '(' 'exists' '(' (quantifiedVariables += SMTSortedVariable)+ ')'
110 (expression=SMTTerm | ('(' '!' expression = SMTTerm ':pattern' '(' pattern = SMTTerm ')' ')')) ')'
111;
112SMTForall: '(' 'forall' '(' (quantifiedVariables += SMTSortedVariable)+ ')'
113 (expression=SMTTerm | ('(' '!' expression = SMTTerm ':pattern' '(' pattern = SMTTerm ')' ')')) ')'
114;
115
116// Boolean operations
117SMTBoolOperation: SMTAnd | SMTOr | SMTImpl | SMTNot | SMTIff;
118SMTAnd: '(' 'and' operands+=SMTTerm+ ')';
119SMTOr: '(' 'or' operands+=SMTTerm+ ')';
120SMTImpl: '(' '=>' leftOperand=SMTTerm rightOperand=SMTTerm ')';
121SMTNot: '(' 'not' operand=SMTTerm ')';
122SMTIff: '(' 'iff' leftOperand=SMTTerm rightOperand=SMTTerm ')';
123
124// If-then-else
125SMTITE: '(' 'ite' condition = SMTTerm if=SMTTerm else = SMTTerm ')';
126
127//Let
128SMTLet: '(' 'let' '(' (inlineConstantDefinitions+=SMTInlineConstantDefinition)+ ')' term=SMTTerm ')';
129SMTInlineConstantDefinition:
130 '(' name=SMTID definition=SMTTerm ')'
131;
132
133// Relations
134SMTRelation: SMTEquals | SMTDistinct | SMTLT | SMTMT | SMTLEQ | SMTMEQ;
135SMTEquals: '(' '=' leftOperand=SMTTerm rightOperand=SMTTerm ')';
136SMTDistinct: '(' 'distinct' operands+=SMTTerm+ ')';
137SMTLT: '(' '<' leftOperand=SMTTerm rightOperand=SMTTerm ')';
138SMTMT: '(' '>' leftOperand=SMTTerm rightOperand=SMTTerm ')';
139SMTLEQ: '(' '<=' leftOperand=SMTTerm rightOperand=SMTTerm ')';
140SMTMEQ: '(' '>=' leftOperand=SMTTerm rightOperand=SMTTerm ')';
141
142// Int operations
143SMTIntOperation: SMTPlus | SMTMinus | SMTMultiply | SMTDivison | SMTDiv | SMTMod;
144SMTPlus: '(' '+' leftOperand=SMTTerm rightOperand=SMTTerm ')';
145SMTMinus: '(' '-' leftOperand=SMTTerm (rightOperand=SMTTerm)? ')';
146SMTMultiply: '(' '*' leftOperand=SMTTerm rightOperand=SMTTerm ')';
147SMTDivison: '(' '/' leftOperand=SMTTerm rightOperand=SMTTerm ')';
148SMTDiv: '(' 'div' leftOperand=SMTTerm rightOperand=SMTTerm ')';
149SMTMod: '(' 'mod' leftOperand=SMTTerm rightOperand=SMTTerm ')';
150
151//////////////////////////////////
152// Assertion
153//////////////////////////////////
154SMTAssertion: '(' 'assert' value=SMTTerm ')';
155SMTCardinalityConstraint:
156 '(' 'forall' '(' '(' ID type=SMTTypeReference ')' ')'
157 (('(' 'or'('(' '=' ID elements+=SMTSymbolicValue ')')* ')') | // With multiple element
158 ('(' '=' ID elements+=SMTSymbolicValue ')')) //With single element
159 ')'
160;
161
162//////////////////////////////////
163// Goals
164//////////////////////////////////
165SMTSatCommand: SMTSimpleSatCommand | SMTComplexSatCommand;
166SMTSimpleSatCommand : '(' 'check-sat' {SMTSimpleSatCommand} ')';
167SMTComplexSatCommand: '(' 'check-sat-using' method = SMTReasoningTactic ')';
168SMTGetModelCommand: '(' 'get-model' {SMTGetModelCommand} ')';
169
170SMTReasoningTactic: SMTBuiltinTactic | SMTReasoningCombinator;
171SMTBuiltinTactic: name = ID;
172SMTReasoningCombinator:
173 SMTAndThenCombinator | SMTOrElseCombinator | SMTParOrCombinator | SMTParThenCombinator | SMTTryForCombinator |
174 SMTIfCombinator | SMTWhenCombinator | SMTFailIfCombinator | SMTUsingParamCombinator
175;
176// executes the given tactics sequencially.
177SMTAndThenCombinator: '(' 'and-then' (tactics+=SMTReasoningTactic)+ ')';
178// tries the given tactics in sequence until one of them succeeds.
179SMTOrElseCombinator: '(' 'or-else' (tactics+=SMTReasoningTactic)+ ')';
180// executes the given tactics in parallel until one of them succeeds.
181SMTParOrCombinator: '(' 'par-or' (tactics+=SMTReasoningTactic)+ ')';
182// executes tactic1 and then tactic2 to every subgoal produced by tactic1. All subgoals are processed in parallel.
183SMTParThenCombinator: '(' 'par-then' preProcessingTactic=SMTReasoningTactic paralellyPostpricessingTactic = SMTReasoningTactic ')';
184// excutes the given tactic for at most <num> milliseconds, it fails if the execution takes more than <num> milliseconds.
185SMTTryForCombinator: '(' 'try-for' tactic=SMTReasoningTactic time=INT ')';
186// if <probe> evaluates to true, then execute the first tactic. Otherwise execute the second.
187SMTIfCombinator: '(' 'if' probe=ReasoningProbe ifTactic=SMTReasoningTactic elseTactic=SMTReasoningTactic ')';
188// shorthand for (if <probe> <tactic> skip).
189SMTWhenCombinator: '(' 'when' probe=ReasoningProbe tactic=SMTReasoningTactic ')';
190// fail if <probe> evaluates to true.
191SMTFailIfCombinator: '(' 'fail-if' probe=ReasoningProbe ')';
192//executes the given tactic using the given attributes, where <attribute> ::= <keyword> <value>. ! is a syntax sugar for using-params.
193SMTUsingParamCombinator: '(' ('using-params' | '!') tactic=SMTReasoningTactic (parameters+=ReasoningTacticParameter)* ')';
194
195ReasoningProbe: name=ID;
196ReasoningTacticParameter: name=PROPERTYNAME value=SMTAtomicTerm;
197
198//////////////////////////////////
199// Result
200//////////////////////////////////
201
202SMTResult: SMTUnsupportedResult | SMTSatResult | SMTModelResult | SMTErrorResult;
203SMTErrorResult: '(' 'error' message = STRING ')';
204SMTUnsupportedResult: 'unsupported' ';' command=ID;
205SMTSatResult: sat?='sat' | unsat?='unsat' | unknown?='unknown';
206SMTModelResult: {SMTModelResult} '(' 'model'
207 (
208 newFunctionDeclarations+=SMTFunctionDeclaration |
209 typeDefinitions+=SMTCardinalityConstraint |
210 newFunctionDefinitions+=SMTFunctionDefinition
211 )*
212 ')';
213
214//////////////////////////////////
215// Statistics
216//////////////////////////////////
217//IntOrReal returns ecore::EDouble: INT | REAL;
218
219SMTStatisticValue: SMTStatisticIntValue | SMTStatisticDoubleValue;
220SMTStatisticIntValue: name = PROPERTYNAME value=INT;
221SMTStatisticDoubleValue: name = PROPERTYNAME value = REAL;
222SMTStatisticsSection: '(' {SMTStatisticsSection} values += SMTStatisticValue* ')'; \ No newline at end of file
diff --git a/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/src/hu/bme/mit/inf/dslreasoner/SmtLanguageRuntimeModule.java b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/src/hu/bme/mit/inf/dslreasoner/SmtLanguageRuntimeModule.java
new file mode 100644
index 00000000..dabb0c29
--- /dev/null
+++ b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/src/hu/bme/mit/inf/dslreasoner/SmtLanguageRuntimeModule.java
@@ -0,0 +1,11 @@
1/*
2 * generated by Xtext
3 */
4package hu.bme.mit.inf.dslreasoner;
5
6/**
7 * Use this class to register components to be used at runtime / without the Equinox extension registry.
8 */
9public class SmtLanguageRuntimeModule extends hu.bme.mit.inf.dslreasoner.AbstractSmtLanguageRuntimeModule {
10
11}
diff --git a/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/src/hu/bme/mit/inf/dslreasoner/SmtLanguageStandaloneSetup.java b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/src/hu/bme/mit/inf/dslreasoner/SmtLanguageStandaloneSetup.java
new file mode 100644
index 00000000..ed297373
--- /dev/null
+++ b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/src/hu/bme/mit/inf/dslreasoner/SmtLanguageStandaloneSetup.java
@@ -0,0 +1,16 @@
1/*
2* generated by Xtext
3*/
4package hu.bme.mit.inf.dslreasoner;
5
6/**
7 * Initialization support for running Xtext languages
8 * without equinox extension registry
9 */
10public class SmtLanguageStandaloneSetup extends SmtLanguageStandaloneSetupGenerated{
11
12 public static void doSetup() {
13 new SmtLanguageStandaloneSetup().createInjectorAndDoEMFRegistration();
14 }
15}
16
diff --git a/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/src/hu/bme/mit/inf/dslreasoner/formatting/SmtLanguageFormatter.xtend b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/src/hu/bme/mit/inf/dslreasoner/formatting/SmtLanguageFormatter.xtend
new file mode 100644
index 00000000..9e3e3943
--- /dev/null
+++ b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/src/hu/bme/mit/inf/dslreasoner/formatting/SmtLanguageFormatter.xtend
@@ -0,0 +1,34 @@
1package hu.bme.mit.inf.dslreasoner.formatting
2
3import org.eclipse.xtext.formatting.impl.AbstractDeclarativeFormatter
4import org.eclipse.xtext.formatting.impl.FormattingConfig
5import hu.bme.mit.inf.dslreasoner.services.SmtLanguageGrammarAccess
6
7
8/**
9 * This class contains custom formatting description.
10 *
11 * see : http://www.eclipse.org/Xtext/documentation.html#formatting
12 * on how and when to use it
13 *
14 * Also see {@link org.eclipse.xtext.xtext.XtextFormattingTokenSerializer} as an example
15 */
16class SmtLanguageFormatter extends AbstractDeclarativeFormatter {
17
18// @Inject extension SmtLanguageGrammarAccess
19
20 override protected void configureFormatting(FormattingConfig c) {
21 val f = getGrammarAccess as SmtLanguageGrammarAccess
22 c.setAutoLinewrap(100000);
23 for(pair : f.findKeywordPairs("(",")")) {
24 c.setNoSpace().after(pair.getFirst());
25 c.setNoSpace().before(pair.getSecond());
26 }
27 c.setLinewrap.after(f.SMTAssertionRule)
28 c.setLinewrap.after(f.SMTFunctionDeclarationRule)
29 c.setLinewrap.after(f.SMTFunctionDefinitionRule)
30 c.setLinewrap.after(f.SMTEnumeratedTypeDeclarationRule)
31 c.setLinewrap.after(f.SMTSetTypeDeclarationRule)
32 c.setLinewrap.after(f.SMTOptionRule)
33 }
34}
diff --git a/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/src/hu/bme/mit/inf/dslreasoner/generator/SmtLanguageGenerator.xtend b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/src/hu/bme/mit/inf/dslreasoner/generator/SmtLanguageGenerator.xtend
new file mode 100644
index 00000000..e61c082e
--- /dev/null
+++ b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/src/hu/bme/mit/inf/dslreasoner/generator/SmtLanguageGenerator.xtend
@@ -0,0 +1,24 @@
1/*
2 * generated by Xtext
3 */
4package hu.bme.mit.inf.dslreasoner.generator
5
6import org.eclipse.emf.ecore.resource.Resource
7import org.eclipse.xtext.generator.IGenerator
8import org.eclipse.xtext.generator.IFileSystemAccess
9
10/**
11 * Generates code from your model files on save.
12 *
13 * see http://www.eclipse.org/Xtext/documentation.html#TutorialCodeGeneration
14 */
15class SmtLanguageGenerator implements IGenerator {
16
17 override void doGenerate(Resource resource, IFileSystemAccess fsa) {
18// fsa.generateFile('greetings.txt', 'People to greet: ' +
19// resource.allContents
20// .filter(typeof(Greeting))
21// .map[name]
22// .join(', '))
23 }
24}
diff --git a/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/src/hu/bme/mit/inf/dslreasoner/scoping/SmtLanguageScopeProvider.xtend b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/src/hu/bme/mit/inf/dslreasoner/scoping/SmtLanguageScopeProvider.xtend
new file mode 100644
index 00000000..e93e0543
--- /dev/null
+++ b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/src/hu/bme/mit/inf/dslreasoner/scoping/SmtLanguageScopeProvider.xtend
@@ -0,0 +1,138 @@
1/*
2 * generated by Xtext
3 */
4package hu.bme.mit.inf.dslreasoner.scoping
5
6import java.util.Set
7import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTSortedVariable
8import org.eclipse.emf.ecore.EObject
9import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTQuantifiedExpression
10import java.util.Collections
11import java.util.HashSet
12import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTInlineConstantDefinition
13import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTLet
14import java.util.Collection
15import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTFunctionDefinition
16import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTSymbolicValue
17import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTDocument
18import org.eclipse.xtext.scoping.IScope
19import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTSymbolicDeclaration
20import org.eclipse.emf.ecore.EReference
21import java.util.HashMap
22import java.util.Map
23import org.eclipse.xtext.scoping.Scopes
24import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTModelResult
25import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTComplexTypeReference
26import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTEnumLiteral
27import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTEnumeratedTypeDeclaration
28import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTFunctionDeclaration
29
30/**
31 * This class contains custom scoping description.
32 *
33 * see : http://www.eclipse.org/Xtext/documentation.html#scoping
34 * on how and when to use it
35 *
36 */
37class SmtLanguageScopeProvider extends org.eclipse.xtext.scoping.impl.AbstractDeclarativeScopeProvider {
38 /**
39 * Search for the first instance of containerType up in the containment hierarchy.
40 * @param containerType
41 * @param from
42 * @return
43 */
44 @SuppressWarnings("unchecked")
45 def private <ContainerType> ContainerType getTop(Class<ContainerType> containerType, EObject from){
46 var actualLevel = from.eContainer();
47 while(actualLevel!=null){
48 if(containerType.isInstance(actualLevel)) { return actualLevel as ContainerType}
49 else { actualLevel = actualLevel.eContainer() }
50 }
51 return null;
52 }
53
54 def private Set<SMTSortedVariable> getQuantifiedVariables(EObject from) {
55 //The most inner quantified variables are in this expression:
56 val quantifiedExpression = getTop(typeof(SMTQuantifiedExpression), from);
57 if(quantifiedExpression==null) return Collections.emptySet();
58
59 //The variables can be referred by a symbolic reference
60 val Set<SMTSortedVariable> result = new HashSet(quantifiedExpression.getQuantifiedVariables());
61 //The variables can defined in an outer quantifier
62 result.addAll(getQuantifiedVariables(quantifiedExpression));
63 //println(result.map[name].join(","))
64 return result;
65 }
66
67 def private Set<SMTInlineConstantDefinition> getInlineConstantDefinitions(EObject from) {
68 //The most inner quantified variables are in this expression:
69 val let = getTop(typeof(SMTLet), from);
70 if(let==null) return Collections.emptySet();
71
72 //The variables can be referred by a symbolic reference
73 val result = new HashSet(let.getInlineConstantDefinitions());
74 //The variables can defined in an outer quantifier
75 result.addAll(getInlineConstantDefinitions(let));
76 return result;
77 }
78
79 def private Collection<SMTSortedVariable> getParameters(SMTSymbolicValue from) {
80 val functionDefinition = getTop(typeof(SMTFunctionDefinition), from);
81 if(functionDefinition!=null) {
82 return functionDefinition.getParameters();
83 }
84 else return Collections.emptySet();
85 }
86
87 def private Set<SMTEnumLiteral> getFiniteElements(SMTSymbolicValue value) {
88 val Set<SMTEnumLiteral> result = new HashSet();
89 val document = getTop(typeof(SMTDocument),value)
90 for(type : document.input.getTypeDeclarations().filter(typeof(SMTEnumeratedTypeDeclaration))) {
91 result.addAll(type.getElements());
92 }
93 return result;
94 }
95
96 def private Set<SMTSymbolicDeclaration> getFunctions(SMTSymbolicValue value) {
97 val document = getTop(typeof(SMTDocument),value);
98 val input = document.input
99 var SMTModelResult output = null;
100 if(document.output != null && document.output.getModelResult instanceof SMTModelResult) {
101 output = document.output.getModelResult as SMTModelResult
102 }
103
104 val Map<String, SMTFunctionDeclaration> declarations = new HashMap
105 val Set<SMTFunctionDefinition> definitions =new HashSet
106
107 input.functionDeclarations.forEach[declarations.put(it.name,it)]
108 if(output != null) {
109 output.newFunctionDeclarations.forEach[declarations.put(it.name,it)]
110 }
111 input.functionDefinition.filter[!declarations.containsKey(it.name)].forEach[definitions += it]
112 if(output != null) {
113 output.newFunctionDefinitions.filter[!declarations.containsKey(it.name)].forEach[definitions += it]
114 }
115
116 val referrables = new HashSet<SMTSymbolicDeclaration>;
117 referrables.addAll(declarations.values)
118 referrables.addAll(definitions)
119 return referrables
120 }
121
122 def public IScope scope_SMTSymbolicValue_symbolicReference(SMTSymbolicValue value, EReference ref) {
123 val Set<SMTSymbolicDeclaration> referrables = new HashSet;
124
125 referrables.addAll(value.getFiniteElements)
126 referrables.addAll(value.getParameters)
127 referrables.addAll(value.getFunctions)
128 referrables.addAll(value.getQuantifiedVariables)
129 referrables.addAll(value.getInlineConstantDefinitions)
130
131 return Scopes.scopeFor(referrables);
132 }
133
134 // Any type defined in the input section can be referred.
135 def public IScope scope_SMTComplexTypeReference_referred(SMTComplexTypeReference reference, EReference ref){
136 return Scopes.scopeFor(getTop(typeof(SMTDocument),reference).input.typeDeclarations)
137 }
138}
diff --git a/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/src/hu/bme/mit/inf/dslreasoner/validation/SmtLanguageValidator.xtend b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/src/hu/bme/mit/inf/dslreasoner/validation/SmtLanguageValidator.xtend
new file mode 100644
index 00000000..2ae6130f
--- /dev/null
+++ b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/src/hu/bme/mit/inf/dslreasoner/validation/SmtLanguageValidator.xtend
@@ -0,0 +1,24 @@
1/*
2 * generated by Xtext
3 */
4package hu.bme.mit.inf.dslreasoner.validation
5//import org.eclipse.xtext.validation.Check
6
7/**
8 * Custom validation rules.
9 *
10 * see http://www.eclipse.org/Xtext/documentation.html#validation
11 */
12class SmtLanguageValidator extends AbstractSmtLanguageValidator {
13
14// public static val INVALID_NAME = 'invalidName'
15//
16// @Check
17// def checkGreetingStartsWithCapital(Greeting greeting) {
18// if (!Character.isUpperCase(greeting.name.charAt(0))) {
19// warning('Name should start with a capital',
20// MyDslPackage.Literals.GREETING__NAME,
21// INVALID_NAME)
22// }
23// }
24}
generated by cgit v1.2.3-54-g00ecf (git 2.45.2) at 2024-07-08 17:55:36 +0000