diff options
Diffstat (limited to 'Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language')
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:<?xml version="1.0" encoding="UTF-8"?> <launchConfigurationWorkingSet factoryID="org.eclipse.ui.internal.WorkingSetFactory" id="1299248699643_13" label="working set" name="working set"> <item factoryID="org.eclipse.ui.internal.model.ResourceFactory" path="/hu.bme.mit.inf.dslreasoner.smt.language" type="4"/> <item factoryID="org.eclipse.ui.internal.model.ResourceFactory" path="/hu.bme.mit.inf.dslreasoner.smt.language.generator" type="4"/> <item factoryID="org.eclipse.ui.internal.model.ResourceFactory" path="/hu.bme.mit.inf.dslreasoner.smt.language.tests" type="4"/> <item factoryID="org.eclipse.ui.internal.model.ResourceFactory" path="/hu.bme.mit.inf.dslreasoner.smt.language.ui" type="4"/> </launchConfigurationWorkingSet>}"/> | ||
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 @@ | |||
1 | eclipse.preferences.version=1 | ||
2 | encoding/<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 @@ | |||
1 | eclipse.preferences.version=1 | ||
2 | org.eclipse.jdt.core.compiler.codegen.inlineJsrBytecode=enabled | ||
3 | org.eclipse.jdt.core.compiler.codegen.targetPlatform=1.8 | ||
4 | org.eclipse.jdt.core.compiler.compliance=1.8 | ||
5 | org.eclipse.jdt.core.compiler.problem.assertIdentifier=error | ||
6 | org.eclipse.jdt.core.compiler.problem.enumIdentifier=error | ||
7 | org.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 @@ | |||
1 | Manifest-Version: 1.0 | ||
2 | Bundle-ManifestVersion: 2 | ||
3 | Bundle-Name: hu.bme.mit.inf.dslreasoner.smt.language | ||
4 | Bundle-Vendor: My Company | ||
5 | Bundle-Version: 1.0.0.qualifier | ||
6 | Bundle-SymbolicName: hu.bme.mit.inf.dslreasoner.smt.language; singleton:=true | ||
7 | Bundle-ActivationPolicy: lazy | ||
8 | Require-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 | ||
22 | Import-Package: org.apache.log4j, | ||
23 | org.eclipse.xtext.xbase.lib | ||
24 | Bundle-RequiredExecutionEnvironment: J2SE-1.5 | ||
25 | Export-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 @@ | |||
1 | source.. = src/,\ | ||
2 | src-gen/,\ | ||
3 | xtend-gen/ | ||
4 | bin.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 @@ | |||
1 | module hu.bme.mit.inf.dslreasoner.GenerateSmtLanguage | ||
2 | |||
3 | import org.eclipse.emf.mwe.utils.* | ||
4 | import org.eclipse.xtext.generator.* | ||
5 | import org.eclipse.xtext.ui.generator.* | ||
6 | |||
7 | var grammarURI = "classpath:/hu/bme/mit/inf/dslreasoner/SmtLanguage.xtext" | ||
8 | var fileExtensions = "smt2" | ||
9 | var projectName = "hu.bme.mit.inf.dslreasoner.smt.language" | ||
10 | var runtimeProject = "../${projectName}" | ||
11 | var generateXtendStub = true | ||
12 | var encoding = "UTF-8" | ||
13 | |||
14 | Workflow { | ||
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 @@ | |||
1 | grammar hu.bme.mit.inf.dslreasoner.SmtLanguage with org.eclipse.xtext.common.Terminals | ||
2 | |||
3 | generate smtLanguage "http://www.bme.hu/mit/inf/dslreasoner/SmtLanguage" | ||
4 | |||
5 | import "http://www.eclipse.org/emf/2002/Ecore" as ecore | ||
6 | |||
7 | SMTDocument: | ||
8 | input=SMTInput | ||
9 | ( | ||
10 | '--------------' | ||
11 | output=SMTOutput | ||
12 | )?; | ||
13 | |||
14 | SMTInput: | ||
15 | (options += SMTOption)* | ||
16 | ( | ||
17 | typeDeclarations+=SMTType | | ||
18 | functionDeclarations+=SMTFunctionDeclaration | | ||
19 | functionDefinition+=SMTFunctionDefinition | | ||
20 | assertions += SMTAssertion | ||
21 | )* | ||
22 | satCommand = SMTSatCommand | ||
23 | getModelCommand = SMTGetModelCommand; | ||
24 | |||
25 | SMTOutput:( | ||
26 | (satResult = SMTResult | ||
27 | getModelResult = SMTResult) | 'timeout' {SMTOutput}) | ||
28 | statistics=SMTStatisticsSection?; | ||
29 | |||
30 | ////////////////////////////////// | ||
31 | // SMT terminals | ||
32 | ////////////////////////////////// | ||
33 | |||
34 | terminal SL_COMMENT : ';' !('\n'|'\r')* ('\r'? '\n')?; | ||
35 | |||
36 | terminal ID : ('a'..'z'|'A'..'Z'|'_') ('a'..'z'|'A'..'Z'|'_'|'-'|'!'|'0'..'9')*; | ||
37 | // ('a'..'z'|'A'..'Z'|'_'/*|'+'|'-'|'/'|'*'|'='|'%'|'?'|'!'|'.'|'$'|'~'|'&'/*|'^'*/|'<'|'>'/*|'@'*/) | ||
38 | // ('a'..'z'|'A'..'Z'|'_'/*|'+'|'-'|'/'|'*'|'='|'%'|'?'|'!'|'.'|'$'|'~'|'&'/*|'^'|*/'<'|'>'/*|'@'*/|'0'..'9')* | ||
39 | SMTID: ID; | ||
40 | |||
41 | terminal PROPERTYNAME : ':' + ID; | ||
42 | terminal REAL returns ecore::EBigDecimal: INT '.' INT; | ||
43 | |||
44 | ////////////////////////////////// | ||
45 | // Options | ||
46 | ////////////////////////////////// | ||
47 | SMTOption: '(' 'set-option' name = PROPERTYNAME value = SMTAtomicTerm ')'; | ||
48 | |||
49 | ////////////////////////////////// | ||
50 | // Type declarations | ||
51 | ////////////////////////////////// | ||
52 | SMTType: SMTEnumeratedTypeDeclaration | SMTSetTypeDeclaration; | ||
53 | |||
54 | SMTEnumLiteral: name = SMTID; | ||
55 | SMTEnumeratedTypeDeclaration: '(' 'declare-datatypes' '(' ')' '(' '(' name = SMTID elements+=SMTEnumLiteral+ ')' ')' ')'; | ||
56 | SMTSetTypeDeclaration: '(' 'declare-sort' name = SMTID ')'; | ||
57 | |||
58 | SMTTypeReference: SMTComplexTypeReference | SMTPrimitiveTypeReference; | ||
59 | SMTComplexTypeReference: referred = [SMTType]; | ||
60 | SMTPrimitiveTypeReference: SMTIntTypeReference | SMTBoolTypeReference | SMTRealTypeReference; | ||
61 | |||
62 | SMTIntTypeReference: {SMTIntTypeReference} "Int"; | ||
63 | SMTBoolTypeReference: {SMTBoolTypeReference} "Bool"; | ||
64 | SMTRealTypeReference: {SMTRealTypeReference} "Real"; | ||
65 | |||
66 | ////////////////////////////////// | ||
67 | // Functions and constants | ||
68 | ////////////////////////////////// | ||
69 | |||
70 | SMTFunctionDeclaration: '(' 'declare-fun' name = SMTID '(' parameters+=SMTTypeReference* ')' range = SMTTypeReference ')'; | ||
71 | |||
72 | /*DeclaredFunctionDefinition: | ||
73 | '(' 'define-fun' declaration=[Function] '(' parameters+=SortedVariable* ')' range = TypeReference value = Term ')';*/ | ||
74 | |||
75 | SMTFunctionDefinition: | ||
76 | '(' 'define-fun' name=SMTID '(' parameters+=SMTSortedVariable* ')' range = SMTTypeReference value = SMTTerm ')'; | ||
77 | |||
78 | |||
79 | ////////////////////////////////// | ||
80 | // Expressions | ||
81 | ////////////////////////////////// | ||
82 | SMTTerm: | ||
83 | SMTSymbolicValue| | ||
84 | SMTAtomicTerm | | ||
85 | SMTBoolOperation | | ||
86 | SMTIntOperation | | ||
87 | SMTITE | | ||
88 | SMTLet | | ||
89 | SMTRelation | | ||
90 | SMTQuantifiedExpression; | ||
91 | |||
92 | SMTSymbolicDeclaration: SMTFunctionDeclaration | SMTFunctionDefinition | SMTSortedVariable | SMTEnumLiteral | SMTInlineConstantDefinition; | ||
93 | |||
94 | SMTSymbolicValue: | ||
95 | '(' symbolicReference = [SMTSymbolicDeclaration] ( parameterSubstitutions += SMTTerm )+ ')' | | ||
96 | symbolicReference = [SMTSymbolicDeclaration]; | ||
97 | |||
98 | SMTAtomicTerm: SMTIntLiteral | SMTBoolLiteral | SMTRealLiteral; | ||
99 | SMTIntLiteral: value=INT; | ||
100 | BOOLEANTERMINAL returns ecore::EBoolean: 'true' | 'false'; | ||
101 | SMTBoolLiteral: value=BOOLEANTERMINAL; | ||
102 | SMTRealLiteral: value=REAL; | ||
103 | |||
104 | // Quantified operations | ||
105 | SMTSortedVariable: '(' name = SMTID range = SMTTypeReference ')'; | ||
106 | //QuantifiedVariableValue: variable = [QuantifiedVariable]; | ||
107 | |||
108 | SMTQuantifiedExpression: SMTExists | SMTForall; | ||
109 | SMTExists: '(' 'exists' '(' (quantifiedVariables += SMTSortedVariable)+ ')' | ||
110 | (expression=SMTTerm | ('(' '!' expression = SMTTerm ':pattern' '(' pattern = SMTTerm ')' ')')) ')' | ||
111 | ; | ||
112 | SMTForall: '(' 'forall' '(' (quantifiedVariables += SMTSortedVariable)+ ')' | ||
113 | (expression=SMTTerm | ('(' '!' expression = SMTTerm ':pattern' '(' pattern = SMTTerm ')' ')')) ')' | ||
114 | ; | ||
115 | |||
116 | // Boolean operations | ||
117 | SMTBoolOperation: SMTAnd | SMTOr | SMTImpl | SMTNot | SMTIff; | ||
118 | SMTAnd: '(' 'and' operands+=SMTTerm+ ')'; | ||
119 | SMTOr: '(' 'or' operands+=SMTTerm+ ')'; | ||
120 | SMTImpl: '(' '=>' leftOperand=SMTTerm rightOperand=SMTTerm ')'; | ||
121 | SMTNot: '(' 'not' operand=SMTTerm ')'; | ||
122 | SMTIff: '(' 'iff' leftOperand=SMTTerm rightOperand=SMTTerm ')'; | ||
123 | |||
124 | // If-then-else | ||
125 | SMTITE: '(' 'ite' condition = SMTTerm if=SMTTerm else = SMTTerm ')'; | ||
126 | |||
127 | //Let | ||
128 | SMTLet: '(' 'let' '(' (inlineConstantDefinitions+=SMTInlineConstantDefinition)+ ')' term=SMTTerm ')'; | ||
129 | SMTInlineConstantDefinition: | ||
130 | '(' name=SMTID definition=SMTTerm ')' | ||
131 | ; | ||
132 | |||
133 | // Relations | ||
134 | SMTRelation: SMTEquals | SMTDistinct | SMTLT | SMTMT | SMTLEQ | SMTMEQ; | ||
135 | SMTEquals: '(' '=' leftOperand=SMTTerm rightOperand=SMTTerm ')'; | ||
136 | SMTDistinct: '(' 'distinct' operands+=SMTTerm+ ')'; | ||
137 | SMTLT: '(' '<' leftOperand=SMTTerm rightOperand=SMTTerm ')'; | ||
138 | SMTMT: '(' '>' leftOperand=SMTTerm rightOperand=SMTTerm ')'; | ||
139 | SMTLEQ: '(' '<=' leftOperand=SMTTerm rightOperand=SMTTerm ')'; | ||
140 | SMTMEQ: '(' '>=' leftOperand=SMTTerm rightOperand=SMTTerm ')'; | ||
141 | |||
142 | // Int operations | ||
143 | SMTIntOperation: SMTPlus | SMTMinus | SMTMultiply | SMTDivison | SMTDiv | SMTMod; | ||
144 | SMTPlus: '(' '+' leftOperand=SMTTerm rightOperand=SMTTerm ')'; | ||
145 | SMTMinus: '(' '-' leftOperand=SMTTerm (rightOperand=SMTTerm)? ')'; | ||
146 | SMTMultiply: '(' '*' leftOperand=SMTTerm rightOperand=SMTTerm ')'; | ||
147 | SMTDivison: '(' '/' leftOperand=SMTTerm rightOperand=SMTTerm ')'; | ||
148 | SMTDiv: '(' 'div' leftOperand=SMTTerm rightOperand=SMTTerm ')'; | ||
149 | SMTMod: '(' 'mod' leftOperand=SMTTerm rightOperand=SMTTerm ')'; | ||
150 | |||
151 | ////////////////////////////////// | ||
152 | // Assertion | ||
153 | ////////////////////////////////// | ||
154 | SMTAssertion: '(' 'assert' value=SMTTerm ')'; | ||
155 | SMTCardinalityConstraint: | ||
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 | ////////////////////////////////// | ||
165 | SMTSatCommand: SMTSimpleSatCommand | SMTComplexSatCommand; | ||
166 | SMTSimpleSatCommand : '(' 'check-sat' {SMTSimpleSatCommand} ')'; | ||
167 | SMTComplexSatCommand: '(' 'check-sat-using' method = SMTReasoningTactic ')'; | ||
168 | SMTGetModelCommand: '(' 'get-model' {SMTGetModelCommand} ')'; | ||
169 | |||
170 | SMTReasoningTactic: SMTBuiltinTactic | SMTReasoningCombinator; | ||
171 | SMTBuiltinTactic: name = ID; | ||
172 | SMTReasoningCombinator: | ||
173 | SMTAndThenCombinator | SMTOrElseCombinator | SMTParOrCombinator | SMTParThenCombinator | SMTTryForCombinator | | ||
174 | SMTIfCombinator | SMTWhenCombinator | SMTFailIfCombinator | SMTUsingParamCombinator | ||
175 | ; | ||
176 | // executes the given tactics sequencially. | ||
177 | SMTAndThenCombinator: '(' 'and-then' (tactics+=SMTReasoningTactic)+ ')'; | ||
178 | // tries the given tactics in sequence until one of them succeeds. | ||
179 | SMTOrElseCombinator: '(' 'or-else' (tactics+=SMTReasoningTactic)+ ')'; | ||
180 | // executes the given tactics in parallel until one of them succeeds. | ||
181 | SMTParOrCombinator: '(' 'par-or' (tactics+=SMTReasoningTactic)+ ')'; | ||
182 | // executes tactic1 and then tactic2 to every subgoal produced by tactic1. All subgoals are processed in parallel. | ||
183 | SMTParThenCombinator: '(' '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. | ||
185 | SMTTryForCombinator: '(' 'try-for' tactic=SMTReasoningTactic time=INT ')'; | ||
186 | // if <probe> evaluates to true, then execute the first tactic. Otherwise execute the second. | ||
187 | SMTIfCombinator: '(' 'if' probe=ReasoningProbe ifTactic=SMTReasoningTactic elseTactic=SMTReasoningTactic ')'; | ||
188 | // shorthand for (if <probe> <tactic> skip). | ||
189 | SMTWhenCombinator: '(' 'when' probe=ReasoningProbe tactic=SMTReasoningTactic ')'; | ||
190 | // fail if <probe> evaluates to true. | ||
191 | SMTFailIfCombinator: '(' 'fail-if' probe=ReasoningProbe ')'; | ||
192 | //executes the given tactic using the given attributes, where <attribute> ::= <keyword> <value>. ! is a syntax sugar for using-params. | ||
193 | SMTUsingParamCombinator: '(' ('using-params' | '!') tactic=SMTReasoningTactic (parameters+=ReasoningTacticParameter)* ')'; | ||
194 | |||
195 | ReasoningProbe: name=ID; | ||
196 | ReasoningTacticParameter: name=PROPERTYNAME value=SMTAtomicTerm; | ||
197 | |||
198 | ////////////////////////////////// | ||
199 | // Result | ||
200 | ////////////////////////////////// | ||
201 | |||
202 | SMTResult: SMTUnsupportedResult | SMTSatResult | SMTModelResult | SMTErrorResult; | ||
203 | SMTErrorResult: '(' 'error' message = STRING ')'; | ||
204 | SMTUnsupportedResult: 'unsupported' ';' command=ID; | ||
205 | SMTSatResult: sat?='sat' | unsat?='unsat' | unknown?='unknown'; | ||
206 | SMTModelResult: {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 | |||
219 | SMTStatisticValue: SMTStatisticIntValue | SMTStatisticDoubleValue; | ||
220 | SMTStatisticIntValue: name = PROPERTYNAME value=INT; | ||
221 | SMTStatisticDoubleValue: name = PROPERTYNAME value = REAL; | ||
222 | SMTStatisticsSection: '(' {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 | */ | ||
4 | package 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 | */ | ||
9 | public 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 | */ | ||
4 | package hu.bme.mit.inf.dslreasoner; | ||
5 | |||
6 | /** | ||
7 | * Initialization support for running Xtext languages | ||
8 | * without equinox extension registry | ||
9 | */ | ||
10 | public 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 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.formatting | ||
2 | |||
3 | import org.eclipse.xtext.formatting.impl.AbstractDeclarativeFormatter | ||
4 | import org.eclipse.xtext.formatting.impl.FormattingConfig | ||
5 | import 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 | */ | ||
16 | class 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 | */ | ||
4 | package hu.bme.mit.inf.dslreasoner.generator | ||
5 | |||
6 | import org.eclipse.emf.ecore.resource.Resource | ||
7 | import org.eclipse.xtext.generator.IGenerator | ||
8 | import 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 | */ | ||
15 | class 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 | */ | ||
4 | package hu.bme.mit.inf.dslreasoner.scoping | ||
5 | |||
6 | import java.util.Set | ||
7 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTSortedVariable | ||
8 | import org.eclipse.emf.ecore.EObject | ||
9 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTQuantifiedExpression | ||
10 | import java.util.Collections | ||
11 | import java.util.HashSet | ||
12 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTInlineConstantDefinition | ||
13 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTLet | ||
14 | import java.util.Collection | ||
15 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTFunctionDefinition | ||
16 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTSymbolicValue | ||
17 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTDocument | ||
18 | import org.eclipse.xtext.scoping.IScope | ||
19 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTSymbolicDeclaration | ||
20 | import org.eclipse.emf.ecore.EReference | ||
21 | import java.util.HashMap | ||
22 | import java.util.Map | ||
23 | import org.eclipse.xtext.scoping.Scopes | ||
24 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTModelResult | ||
25 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTComplexTypeReference | ||
26 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTEnumLiteral | ||
27 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTEnumeratedTypeDeclaration | ||
28 | import 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 | */ | ||
37 | class 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 | */ | ||
4 | package 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 | */ | ||
12 | class 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 | } | ||