32 files changed, 3568 insertions, 0 deletions
diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/.classpath b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/.classpath
new file mode 100644
index 00000000..de68b5f7
--- /dev/null
+++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/.classpath
@@ -0,0 +1,11 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<classpath>
+        <classpathentry kind="src" path="xtend-gen"/>
+        <classpathentry kind="src" path="queries"/>
+        <classpathentry kind="src" path="vql-gen"/>
+        <classpathentry exported="true" kind="lib" path="lib/alloy4.2_2015-02-22.jar"/>
+        <classpathentry kind="con" path="org.eclipse.jdt.launching.JRE_CONTAINER/org.eclipse.jdt.internal.debug.ui.launcher.StandardVMType/JavaSE-1.8"/>
+        <classpathentry kind="con" path="org.eclipse.pde.core.requiredPlugins"/>
+        <classpathentry kind="src" path="src"/>
+        <classpathentry kind="output" path="bin"/>
+</classpath>
diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/.gitignore b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/.gitignore
new file mode 100644
index 00000000..e42fe9ea
--- /dev/null
+++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/.gitignore
@@ -0,0 +1,4 @@
+/bin/
+/src-gen/
+/vql-gen/
+/xtend-gen/
+\ No newline at end of file
diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/.project b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/.project
new file mode 100644
index 00000000..a1c16519
--- /dev/null
+++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/.project
@@ -0,0 +1,40 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<projectDescription>
+        <name>hu.bme.mit.inf.dlsreasoner.alloy.reasoner</name>
+        <comment></comment>
+        <projects>
+        </projects>
+        <buildSpec>
+                <buildCommand>
+                        <name>org.eclipse.viatra.query.tooling.core.projectbuilder</name>
+                        <arguments>
+                        </arguments>
+                </buildCommand>
+                <buildCommand>
+                        <name>org.eclipse.xtext.ui.shared.xtextBuilder</name>
+                        <arguments>
+                        </arguments>
+                </buildCommand>
+                <buildCommand>
+                        <name>org.eclipse.jdt.core.javabuilder</name>
+                        <arguments>
+                        </arguments>
+                </buildCommand>
+                <buildCommand>
+                        <name>org.eclipse.pde.ManifestBuilder</name>
+                        <arguments>
+                        </arguments>
+                </buildCommand>
+                <buildCommand>
+                        <name>org.eclipse.pde.SchemaBuilder</name>
+                        <arguments>
+                        </arguments>
+                </buildCommand>
+        </buildSpec>
+        <natures>
+                <nature>org.eclipse.pde.PluginNature</nature>
+                <nature>org.eclipse.jdt.core.javanature</nature>
+                <nature>org.eclipse.xtext.ui.shared.xtextNature</nature>
+                <nature>org.eclipse.viatra.query.projectnature</nature>
+        </natures>
+</projectDescription>
diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/.settings/org.eclipse.incquery.patternlanguage.emf.EMFPatternLanguage.prefs b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/.settings/org.eclipse.incquery.patternlanguage.emf.EMFPatternLanguage.prefs
new file mode 100644
index 00000000..7d03706a
--- /dev/null
+++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/.settings/org.eclipse.incquery.patternlanguage.emf.EMFPatternLanguage.prefs
@@ -0,0 +1,29 @@
+BuilderConfiguration.is_project_specific=true
+autobuilding=true
+eclipse.preferences.version=1
+generateGeneratedAnnotation=false
+generateSuppressWarnings=true
+generatedAnnotationComment=
+includeDateInGenerated=false
+outlet.DEFAULT_OUTPUT.cleanDirectory=false
+outlet.DEFAULT_OUTPUT.cleanupDerived=true
+outlet.DEFAULT_OUTPUT.createDirectory=true
+outlet.DEFAULT_OUTPUT.derived=true
+outlet.DEFAULT_OUTPUT.directory=./viatra-gen
+outlet.DEFAULT_OUTPUT.hideLocalSyntheticVariables=true
+outlet.DEFAULT_OUTPUT.installDslAsPrimarySource=false
+outlet.DEFAULT_OUTPUT.keepLocalHistory=true
+outlet.DEFAULT_OUTPUT.override=true
+outlet.DEFAULT_OUTPUT.sourceFolder.ecore-gen.directory=
+outlet.DEFAULT_OUTPUT.sourceFolder.ecore-gen.ignore=
+outlet.DEFAULT_OUTPUT.sourceFolder.queries.directory=
+outlet.DEFAULT_OUTPUT.sourceFolder.queries.ignore=
+outlet.DEFAULT_OUTPUT.sourceFolder.src-gen.directory=
+outlet.DEFAULT_OUTPUT.sourceFolder.src-gen.ignore=
+outlet.DEFAULT_OUTPUT.sourceFolder.src.directory=
+outlet.DEFAULT_OUTPUT.sourceFolder.src.ignore=
+outlet.DEFAULT_OUTPUT.sourceFolder.xtend-gen.directory=
+outlet.DEFAULT_OUTPUT.sourceFolder.xtend-gen.ignore=
+outlet.DEFAULT_OUTPUT.userOutputPerSourceFolder=
+targetJavaVersion=JAVA5
+useJavaCompilerCompliance=true
diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/.settings/org.eclipse.jdt.core.prefs b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/.settings/org.eclipse.jdt.core.prefs
new file mode 100644
index 00000000..295926d9
--- /dev/null
+++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/.settings/org.eclipse.jdt.core.prefs
@@ -0,0 +1,7 @@
+eclipse.preferences.version=1
+org.eclipse.jdt.core.compiler.codegen.inlineJsrBytecode=enabled
+org.eclipse.jdt.core.compiler.codegen.targetPlatform=1.8
+org.eclipse.jdt.core.compiler.compliance=1.8
+org.eclipse.jdt.core.compiler.problem.assertIdentifier=error
+org.eclipse.jdt.core.compiler.problem.enumIdentifier=error
+org.eclipse.jdt.core.compiler.source=1.8
diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/.settings/org.eclipse.viatra.query.patternlanguage.emf.EMFPatternLanguage.prefs b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/.settings/org.eclipse.viatra.query.patternlanguage.emf.EMFPatternLanguage.prefs
new file mode 100644
index 00000000..c6f56e64
--- /dev/null
+++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/.settings/org.eclipse.viatra.query.patternlanguage.emf.EMFPatternLanguage.prefs
@@ -0,0 +1,29 @@
+BuilderConfiguration.is_project_specific=true
+autobuilding=true
+eclipse.preferences.version=1
+generateGeneratedAnnotation=false
+generateSuppressWarnings=true
+generatedAnnotationComment=
+includeDateInGenerated=false
+outlet.DEFAULT_OUTPUT.cleanDirectory=true
+outlet.DEFAULT_OUTPUT.cleanupDerived=true
+outlet.DEFAULT_OUTPUT.createDirectory=true
+outlet.DEFAULT_OUTPUT.derived=true
+outlet.DEFAULT_OUTPUT.directory=./vql-gen
+outlet.DEFAULT_OUTPUT.hideLocalSyntheticVariables=true
+outlet.DEFAULT_OUTPUT.installDslAsPrimarySource=false
+outlet.DEFAULT_OUTPUT.keepLocalHistory=true
+outlet.DEFAULT_OUTPUT.override=true
+outlet.DEFAULT_OUTPUT.sourceFolder.ecore-gen.directory=
+outlet.DEFAULT_OUTPUT.sourceFolder.ecore-gen.ignore=
+outlet.DEFAULT_OUTPUT.sourceFolder.queries.directory=
+outlet.DEFAULT_OUTPUT.sourceFolder.queries.ignore=
+outlet.DEFAULT_OUTPUT.sourceFolder.src.directory=
+outlet.DEFAULT_OUTPUT.sourceFolder.src.ignore=
+outlet.DEFAULT_OUTPUT.sourceFolder.viatra-gen.directory=
+outlet.DEFAULT_OUTPUT.sourceFolder.viatra-gen.ignore=
+outlet.DEFAULT_OUTPUT.sourceFolder.xtend-gen.directory=
+outlet.DEFAULT_OUTPUT.sourceFolder.xtend-gen.ignore=
+outlet.DEFAULT_OUTPUT.userOutputPerSourceFolder=
+targetJavaVersion=JAVA5
+useJavaCompilerCompliance=true
diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/META-INF/MANIFEST.MF b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/META-INF/MANIFEST.MF
new file mode 100644
index 00000000..13ad2d10
--- /dev/null
+++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/META-INF/MANIFEST.MF
@@ -0,0 +1,26 @@
+Manifest-Version: 1.0
+Bundle-ManifestVersion: 2
+Bundle-Name: %pluginName
+Bundle-SymbolicName: hu.bme.mit.inf.dlsreasoner.alloy.reasoner;singleton:=true
+Bundle-Version: 1.0.0.qualifier
+Bundle-ClassPath: lib/alloy4.2_2015-02-22.jar,
+ .
+Bundle-Vendor: %providerName
+Bundle-Localization: plugin
+Export-Package: hu.bme.mit.inf.dlsreasoner.alloy.reasoner,
+ hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder,
+ hu.bme.mit.inf.dlsreasoner.alloy.reasoner.queries,
+ hu.bme.mit.inf.dlsreasoner.alloy.reasoner.queries.util
+Require-Bundle: com.google.guava,
+ org.eclipse.xtend.lib,
+ org.eclipse.xtext.xbase.lib,
+ org.eclipse.core.runtime,
+ org.eclipse.emf.ecore;visibility:=reexport,
+ hu.bme.mit.inf.dslreasoner.logic.model;bundle-version="1.0.0";visibility:=reexport,
+ hu.bme.mit.inf.dslreasoner.alloy.language;bundle-version="1.0.0",
+ org.eclipse.viatra.query.runtime;bundle-version="[1.2.0,2.0.0)",
+ org.eclipse.viatra.query.runtime.base.itc;bundle-version="1.3.0",
+ hu.bme.mit.inf.dslreasoner.ecore2logic;bundle-version="1.0.0"
+Bundle-RequiredExecutionEnvironment: JavaSE-1.8
+Bundle-ActivationPolicy: lazy
+Import-Package: org.apache.log4j;version="1.2.15"
diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/build.properties b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/build.properties
new file mode 100644
index 00000000..bb9e5d4d
--- /dev/null
+++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/build.properties
@@ -0,0 +1,10 @@
+bin.includes = .,\
+               model/,\
+               META-INF/,\
+               plugin.xml,\
+               plugin.properties
+jars.compile.order = .
+source.. = ecore-gen/,\
+           src/,\
+           src-gen/
+output.. = bin/
diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/plugin.properties b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/plugin.properties
new file mode 100644
index 00000000..14541a0a
--- /dev/null
+++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/plugin.properties
@@ -0,0 +1,4 @@
+#
+pluginName = AlloyLanguage Model
+providerName = www.example.org
diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/plugin.xml b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/plugin.xml
new file mode 100644
index 00000000..23c55a4d
--- /dev/null
+++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/plugin.xml
@@ -0,0 +1,21 @@
+<?xml version="1.0" encoding="UTF-8"?><?eclipse version="3.0"?><!--
+--><plugin>
+  <extension point="org.eclipse.emf.ecore.generated_package">
+    <!-- @generated AlloyLanguage -->
+    <package class="hu.bme.mit.inf.dlsreasoner.alloy.reasoner.alloylanguage.AlloylanguagePackage" genModel="model/AlloyLanguage.genmodel" uri="hu.bme.mit.inf.dlsreasoner.alloy.reasoner.language"/>
+  </extension>
+  <extension id="hu.bme.mit.inf.dlsreasoner.alloy.reasoner.queries.SignatureQueries" point="org.eclipse.viatra.query.runtime.queryspecification">
+    <group group="org.eclipse.viatra.query.runtime.extensibility.SingletonExtensionFactory:hu.bme.mit.inf.dlsreasoner.alloy.reasoner.queries.SignatureQueries" id="hu.bme.mit.inf.dlsreasoner.alloy.reasoner.queries.SignatureQueries">
+      <query-specification fqn="hu.bme.mit.inf.dlsreasoner.alloy.reasoner.queries.directSubset"/>
+      <query-specification fqn="hu.bme.mit.inf.dlsreasoner.alloy.reasoner.queries.subset"/>
+    </group>
+  </extension>
+  <extension id="hu.bme.mit.inf.dlsreasoner.alloy.reasoner.queries.TypeQueries" point="org.eclipse.viatra.query.runtime.queryspecification">
+    <group group="org.eclipse.viatra.query.runtime.extensibility.SingletonExtensionFactory:hu.bme.mit.inf.dlsreasoner.alloy.reasoner.queries.TypeQueries" id="hu.bme.mit.inf.dlsreasoner.alloy.reasoner.queries.TypeQueries">
+      <query-specification fqn="hu.bme.mit.inf.dlsreasoner.alloy.reasoner.queries.supertype"/>
+      <query-specification fqn="hu.bme.mit.inf.dlsreasoner.alloy.reasoner.queries.topmostCommonSubtypes"/>
+      <query-specification fqn="hu.bme.mit.inf.dlsreasoner.alloy.reasoner.queries.lowermostCommonSupertype"/>
+      <query-specification fqn="hu.bme.mit.inf.dlsreasoner.alloy.reasoner.queries.lowestCommonSupertypeOfAllOccuranceOfElement"/>
+    </group>
+  </extension>
+</plugin>
diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/queries/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/queries/signatureQueries.vql b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/queries/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/queries/signatureQueries.vql
new file mode 100644
index 00000000..a020953c
--- /dev/null
+++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/queries/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/queries/signatureQueries.vql
@@ -0,0 +1,17 @@
+package hu.bme.mit.inf.dlsreasoner.alloy.reasoner.queries
+import epackage "http://www.bme.hu/mit/inf/dslreasoner/AlloyLanguage"
+pattern directSubset(x: ALSSignatureDeclaration, y: ALSSignatureDeclaration) {
+        ALSSignatureBody.declarations(b,y);
+        ALSSignatureBody.supertype(b,x);
+} or {
+        ALSSignatureBody.declarations(b,y);
+        ALSSignatureBody.superset(b,x);
+}
+pattern subset(x: ALSSignatureDeclaration, y: ALSSignatureDeclaration) {
+        x == y;
+} or {
+        find directSubset+(x,y);
+}
diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/queries/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/queries/typeQueries.vql b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/queries/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/queries/typeQueries.vql
new file mode 100644
index 00000000..8d93cafb
--- /dev/null
+++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/queries/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/queries/typeQueries.vql
@@ -0,0 +1,85 @@
+package hu.bme.mit.inf.dlsreasoner.alloy.reasoner.queries
+import epackage "http://www.bme.hu/mit/inf/dslreasoner/logic/model/language"
+private pattern supertypeEdge(type1: Type, type2: Type) {
+        Type.supertypes(type1,type2);
+}
+pattern supertype(type1: Type, type2: Type) {
+        type1 == type2;
+} or {
+        find supertypeEdge+(type1,type2);
+}
+private pattern commonSubtype(type1: Type, type2: Type, common: Type) {
+        find supertype(common,type1);
+        find supertype(common,type2);
+}
+private pattern commonSupertype(type1: Type, type2: Type, common: Type) {
+        find supertype(common,type1);
+        find supertype(common,type2);
+}
+private pattern hasHigherCommonSubtype(type1: Type, type2: Type, common: Type, higher: Type) {
+        find supertype(higher,type1);
+        find supertype(higher,type2);
+        Type.supertypes(common,higher);
+        higher != common;
+}
+private pattern hasLowerCommonSupertype(type1: Type, type2: Type, common: Type, lower: Type) {
+        find supertype(type1,lower);
+        find supertype(type2,lower);
+        Type.supertypes(lower,common);
+        lower != common;
+}
+pattern topmostCommonSubtypes(type1: Type, type2: Type, common: Type) {
+        find commonSubtype(type1, type2, common);
+        neg find hasHigherCommonSubtype(type1, type2, common, _);
+}
+pattern lowermostCommonSupertype(type1: Type, type2: Type, common: Type) {
+        find commonSupertype(type1, type2, common);
+        neg find hasLowerCommonSupertype(type1, type2, common, _);
+}
+/*pattern topmostCommonSubtypesInObject(type1: Type, type2: Type, common: Type) {
+        find commonSubtype(type1, type2, common);
+        neg find supertypeEdge(type1,_);
+        neg find supertypeEdge(type2,_);
+        neg find hasHigherCommonSubtype(type1, type2, common, _);
+}
+pattern topmostCommonSubtypesInType(in: Type, type1: Type, type2: Type, common: Type) {
+        find commonSubtype(type1, type2, common);
+        find supertypeEdge(type1,in);
+        find supertypeEdge(type2,in);
+        neg find hasHigherCommonSubtype(type1, type2, common, _);
+}
+ */
+pattern lowestCommonSupertypeOfAllOccuranceOfElement(element: DefinedElement, type: Type) {
+        find typeContainsAllOccuranceOfElement(element,type);
+        neg find hasLowerCommonSupertypeOfAllOccuranceOfElement(element, type, _);
+}
+private pattern hasLowerCommonSupertypeOfAllOccuranceOfElement(element: DefinedElement, type: Type, lower: Type) {
+        find typeContainsAllOccuranceOfElement(element, type);
+        find typeContainsAllOccuranceOfElement(element, lower);
+        find supertype(lower, type);
+        type != lower;
+}
+private pattern typeContainsAllOccuranceOfElement(element: DefinedElement, type: Type) {
+        find supertype(containerType,type);
+        TypeDefinition.elements(containerType,element);
+        neg find typeDoesNotCoverElementOccurance(element,type,_);
+}
+private pattern typeDoesNotCoverElementOccurance(element: DefinedElement, type: Type, uncoveredOccurance: TypeDefinition) {
+        find supertype(containerType,type);
+        TypeDefinition.elements(containerType,element);
+        TypeDefinition.elements(uncoveredOccurance,element);
+        neg find supertype(uncoveredOccurance,type);
+}
+\ No newline at end of file
diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/AlloyAnalyzerConfiguration.xtend b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/AlloyAnalyzerConfiguration.xtend
new file mode 100644
index 00000000..cdf21174
--- /dev/null
+++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/AlloyAnalyzerConfiguration.xtend
@@ -0,0 +1,32 @@
+package hu.bme.mit.inf.dlsreasoner.alloy.reasoner
+import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration
+class AlloySolverConfiguration extends LogicSolverConfiguration {
+        /*public var boolean createCommonSupertype
+        public var int intScope = 1 // 5 by default
+        public def setIntScopeFor(int max) {
+                intScope = 31 - Integer.numberOfLeadingZeros(max) + 1
+        }*/
+        public var int symmetry = 0 // by default
+        public var AlloyBackendSolver solver = AlloyBackendSolver.SAT4J
+        public var boolean writeToFile = false
+}
+enum AlloyBackendSolver {
+        BerkMinPIPE,
+        SpearPIPE,
+        MiniSatJNI,
+        MiniSatProverJNI,
+        LingelingJNI,
+        PLingelingJNI,
+        GlucoseJNI,
+        CryptoMiniSatJNI,
+        SAT4J,
+        CNF,
+        KodKod
+}
+enum TypeMappingTechnique {
+        FilteredTypes
+}
+\ No newline at end of file
diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/AlloySolver.xtend b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/AlloySolver.xtend
new file mode 100644
index 00000000..7dfc3161
--- /dev/null
+++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/AlloySolver.xtend
@@ -0,0 +1,72 @@
+package hu.bme.mit.inf.dlsreasoner.alloy.reasoner
+import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder.Alloy2LogicMapper
+import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder.AlloyHandler
+import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder.AlloyModelInterpretation
+import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder.Logic2AlloyLanguageMapper
+import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder.Logic2AlloyLanguageMapperTrace
+import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder.MonitoredAlloySolution
+import hu.bme.mit.inf.dslreasoner.AlloyLanguageStandaloneSetupGenerated
+import hu.bme.mit.inf.dslreasoner.alloyLanguage.AlloyLanguagePackage
+import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasoner
+import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasonerException
+import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration
+import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem
+import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult
+import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace
+import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder.Logic2AlloyLanguageMapper_TypeMapper_FilteredTypes
+import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder.AlloyModelInterpretation_TypeInterpretation_FilteredTypes
+import org.eclipse.emf.common.util.URI
+class AlloySolver extends LogicReasoner{
+        
+        new() {
+                AlloyLanguagePackage.eINSTANCE.eClass
+                val x = new AlloyLanguageStandaloneSetupGenerated
+                x.createInjectorAndDoEMFRegistration
+        }
+        
+        val Logic2AlloyLanguageMapper forwardMapper = new Logic2AlloyLanguageMapper(new Logic2AlloyLanguageMapper_TypeMapper_FilteredTypes)
+        val AlloyHandler handler = new AlloyHandler
+        val Alloy2LogicMapper backwardMapper = new Alloy2LogicMapper
+        
+        val fileName = "problem.als"
+        
+        override solve(LogicProblem problem, LogicSolverConfiguration configuration, ReasonerWorkspace workspace) throws LogicReasonerException {
+                if(configuration instanceof AlloySolverConfiguration) {
+                        val transformationStart = System.currentTimeMillis
+                        val result = forwardMapper.transformProblem(problem,configuration)
+                        val alloyProblem = result.output
+                        
+                        /*val x = alloyProblem.eAllContents.filter(ALSFunctionCall).filter[it.referredDefinition == null].toList
+                        println(x)*/
+                        val forwardTrace = result.trace
+                        
+                        var String fileURI = null;
+                        var String alloyCode = null;
+                        if(configuration.writeToFile) {
+                                fileURI = workspace.writeModel(alloyProblem,fileName).toFileString
+                        } else {
+                                alloyCode = workspace.writeModelToString(alloyProblem,fileName)
+                        }
+                        
+                        //val alloyCode = workspace.readText(fileName)
+                        //val FunctionWithTimeout<MonitoredAlloySolution> call = new FunctionWithTimeout[] 
+                        
+                        val transformationTime = System.currentTimeMillis - transformationStart
+                        val result2 = handler.callSolver(alloyProblem,workspace,configuration,fileURI,alloyCode)
+                        workspace.deactivateModel(fileName)
+                        val logicResult = backwardMapper.transformOutput(problem,result2,forwardTrace,transformationTime)
+                        return logicResult
+                } else throw new IllegalArgumentException('''The configuration have to be an «AlloySolverConfiguration.simpleName»!''')
+        }
+        
+        override getInterpretation(ModelResult modelResult) {
+                return new AlloyModelInterpretation(
+                        new AlloyModelInterpretation_TypeInterpretation_FilteredTypes,
+                        (modelResult.representation as MonitoredAlloySolution).solution,
+                        forwardMapper,
+                        modelResult.trace as Logic2AlloyLanguageMapperTrace
+                );
+        }       
+}
+\ No newline at end of file
diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Alloy2LogicMapper.xtend b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Alloy2LogicMapper.xtend
new file mode 100644
index 00000000..637752b0
--- /dev/null
+++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Alloy2LogicMapper.xtend
@@ -0,0 +1,48 @@
+package hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder
+import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem
+import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicresultFactory
+class Alloy2LogicMapper {
+        val extension LogicresultFactory resultFactory = LogicresultFactory.eINSTANCE
+        
+        public def transformOutput(LogicProblem problem, MonitoredAlloySolution solution, Logic2AlloyLanguageMapperTrace trace, long transformationTime) {
+                if(solution == null) {
+                        return createInsuficientResourcesResult => [
+                                it.problem = problem
+                                it.statistics = transformStatistics(solution,transformationTime)
+                        ]
+                } else {
+                        val logicResult = solution.solution
+                        if(logicResult.satisfiable) {
+                                return createModelResult => [
+                                        it.problem = problem
+                                        it.representation += solution
+                                        it.maxInteger = logicResult.max
+                                        it.minInteger = logicResult.min
+                                        it.trace = trace
+                                        it.statistics = transformStatistics(solution,transformationTime)
+                                ]
+                        } else {
+                                return createInconsistencyResult => [
+                                        it.problem = problem
+                                        //trace?
+                                        it.statistics = transformStatistics(solution,transformationTime)
+                                ]
+                        }
+                }
+        }
+        
+        def transformStatistics(MonitoredAlloySolution solution, long transformationTime) {
+                createStatistics => [
+                        it.transformationTime = transformationTime as int
+                        if(solution != null) {
+                                it.solverTime = solution.runtimeTime as int
+                                it.entries += LogicresultFactory.eINSTANCE.createIntStatisticEntry => [
+                                        it.name = "KoodkodToCNFTransformationTime"
+                                        it.value = solution.getKodkodTime as int
+                                ]
+                        }
+                ]
+        }
+}
+\ No newline at end of file
diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyHandler.xtend b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyHandler.xtend
new file mode 100644
index 00000000..6bac4130
--- /dev/null
+++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyHandler.xtend
@@ -0,0 +1,145 @@
+package hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder
+import edu.mit.csail.sdg.alloy4.A4Reporter
+import edu.mit.csail.sdg.alloy4.Err
+import edu.mit.csail.sdg.alloy4.ErrorWarning
+import edu.mit.csail.sdg.alloy4compiler.ast.Command
+import edu.mit.csail.sdg.alloy4compiler.parser.CompModule
+import edu.mit.csail.sdg.alloy4compiler.parser.CompUtil
+import edu.mit.csail.sdg.alloy4compiler.translator.A4Options
+import edu.mit.csail.sdg.alloy4compiler.translator.A4Solution
+import edu.mit.csail.sdg.alloy4compiler.translator.TranslateAlloyToKodkod
+import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace
+import java.util.LinkedList
+import java.util.List
+import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.AlloyBackendSolver
+import org.eclipse.xtend.lib.annotations.Data
+import java.util.Map
+import java.util.HashMap
+import edu.mit.csail.sdg.alloy4compiler.translator.A4Options.SatSolver
+import org.eclipse.emf.common.CommonPlugin
+import java.util.ArrayList
+import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSDocument
+import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.AlloySolverConfiguration
+class AlloySolverException extends Exception{
+        new(String s) { super(s) }
+        new(String s, Exception e) { super(s,e) }
+        new(String s, List<String> errors, Exception e) {
+                super(s + '\n' + errors.join('\n'), e)
+        }
+}
+@Data class MonitoredAlloySolution{
+        List<String> warnings
+        List<String> debugs
+        long kodkodTime
+        long runtimeTime
+        
+        A4Solution solution
+}
+class AlloyHandler {
+        
+        //val fileName = "problem.als"
+        
+        public def callSolver(ALSDocument problem, ReasonerWorkspace workspace, AlloySolverConfiguration configuration, String path, String alloyCode) {
+                //Prepare
+                
+                val warnings = new LinkedList<String>
+                val debugs = new LinkedList<String>
+                val runtime = new ArrayList<Long>
+                val reporter = new A4Reporter() {
+                        override debug(String message) { debugs += message }
+                        override resultSAT (Object command, long solvingTime, Object solution) { runtime += solvingTime }
+                        override resultUNSAT (Object command, long solvingTime, Object solution) { runtime += solvingTime }
+                        override warning(ErrorWarning msg) { warnings += msg.message }
+                }
+                
+                val options = new A4Options() => [
+                        it.symmetry = configuration.symmetry
+                        it.noOverflow = true
+                        it.solver = getSolver(configuration.solver, configuration)
+                        if(configuration.solver.externalSolver) {
+                                it.solverDirectory = configuration.solverPath
+                        }
+                        it.tempDirectory = CommonPlugin.resolve(workspace.workspaceURI).toFileString
+                ]
+                
+                // Transform
+                var Command command = null;
+                var CompModule compModule = null
+                
+                val kodkodTransformStart = System.currentTimeMillis();
+                
+                try {
+                        if(configuration.writeToFile) {
+                                compModule = CompUtil.parseEverything_fromFile(reporter,null,path)
+                        } else {
+                                compModule = CompUtil.parseEverything_fromString(reporter,alloyCode)
+                        }
+                        if(compModule.allCommands.size != 1)
+                                throw new UnsupportedOperationException('''Alloy files with multiple commands are not supported!''')
+                        command = compModule.allCommands.head
+                } catch (Err e){
+                        throw new AlloySolverException(e.message,warnings,e)
+                }
+                val kodkodTransformFinish = System.currentTimeMillis - kodkodTransformStart
+                
+                //Execute
+                var A4Solution answer = null;
+                try {
+                        answer = TranslateAlloyToKodkod.execute_command(reporter,compModule.allSigs,command,options)
+                }catch(Exception e) {
+                        warnings +=e.message
+                }
+                
+                var long runtimeFromAnswer;
+                if(runtime.empty) {
+                        runtimeFromAnswer = System.currentTimeMillis - (kodkodTransformStart + kodkodTransformFinish)
+                } else {
+                        runtimeFromAnswer = runtime.head
+                }
+                
+                return new MonitoredAlloySolution(warnings,debugs,kodkodTransformFinish,runtimeFromAnswer,answer)
+        }
+        
+        val static Map<SolverConfiguration, SatSolver> previousSolverConfigurations = new HashMap
+        def getSolverConfiguration(AlloyBackendSolver backedSolver, String path, String[] options) {
+                val config = new SolverConfiguration(backedSolver,path,options)
+                if(previousSolverConfigurations.containsKey(config)) {
+                        return previousSolverConfigurations.get(config)
+                } else {
+                        val id ='''DSLReasoner_Alloy_«previousSolverConfigurations.size»_«backedSolver»'''
+                        val newSolver = A4Options.SatSolver.make(id,id,path,options)
+                        previousSolverConfigurations.put(config,newSolver)
+                        return newSolver
+                }
+        }
+        
+        def getSolver(AlloyBackendSolver backedSolver, AlloySolverConfiguration configuration) {
+                switch(backedSolver){
+                        case BerkMinPIPE: return A4Options.SatSolver.BerkMinPIPE
+                        case SpearPIPE: return A4Options.SatSolver.SpearPIPE
+                        case MiniSatJNI: return A4Options.SatSolver.MiniSatJNI
+                        case MiniSatProverJNI: return A4Options.SatSolver.MiniSatProverJNI
+                        case LingelingJNI: return A4Options.SatSolver.LingelingJNI
+                        case PLingelingJNI: return getSolverConfiguration(backedSolver,configuration.solverPath,null)
+                        case GlucoseJNI: return A4Options.SatSolver.GlucoseJNI
+                        case CryptoMiniSatJNI: return A4Options.SatSolver.CryptoMiniSatJNI
+                        case SAT4J: return A4Options.SatSolver.SAT4J
+                        case CNF: return A4Options.SatSolver.CNF
+                        case KodKod: return A4Options.SatSolver.KK
+                }
+        }
+        
+        def isExternalSolver(AlloyBackendSolver backedSolver) {
+                return !(backedSolver == AlloyBackendSolver.SAT4J)
+        }
+}
+@Data class SolverConfiguration {
+        AlloyBackendSolver backedSolver
+        String path
+        String[] options
+}
diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyModelInterpretation.xtend b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyModelInterpretation.xtend
new file mode 100644
index 00000000..d00291e0
--- /dev/null
+++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyModelInterpretation.xtend
@@ -0,0 +1,331 @@
+package hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder
+import edu.mit.csail.sdg.alloy4compiler.ast.ExprVar
+import edu.mit.csail.sdg.alloy4compiler.ast.Sig.Field
+import edu.mit.csail.sdg.alloy4compiler.translator.A4Solution
+import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicModelInterpretation
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ConstantDeclaration
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.FunctionDeclaration
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.LogiclanguageFactory
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDeclaration
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition
+import java.util.Arrays
+import java.util.HashMap
+import java.util.LinkedList
+import java.util.List
+import java.util.Map
+import java.util.Set
+import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*
+import edu.mit.csail.sdg.alloy4compiler.ast.Sig
+import java.util.ArrayList
+interface AlloyModelInterpretation_TypeInterpretation {
+        def void resolveUnknownAtoms(
+                Iterable<ExprVar> objectAtoms, 
+                A4Solution solution,
+                Logic2AlloyLanguageMapperTrace forwardTrace,
+                Map<String, Sig> name2AlloySig,
+                Map<String, Field> name2AlloyField,
+                Map<String,DefinedElement> expression2DefinedElement,
+                Map<TypeDeclaration, List<DefinedElement>> interpretationOfUndefinedType)
+}
+class AlloyModelInterpretation_TypeInterpretation_FilteredTypes implements AlloyModelInterpretation_TypeInterpretation{
+        protected val extension LogiclanguageFactory factory = LogiclanguageFactory.eINSTANCE
+        
+        override resolveUnknownAtoms(
+                Iterable<ExprVar> objectAtoms, 
+                A4Solution solution,
+                Logic2AlloyLanguageMapperTrace forwardTrace,
+                Map<String, Sig> name2AlloySig,
+                Map<String, Field> name2AlloyField,
+                Map<String,DefinedElement> expression2DefinedElement,
+                Map<TypeDeclaration, List<DefinedElement>> interpretationOfUndefinedType)
+        {
+                /*val Map<String,DefinedElement> expression2DefinedElement = new HashMap()
+                val Map<TypeDeclaration, List<DefinedElement>> interpretationOfUndefinedType = new HashMap;*/
+                
+                val typeTrace = forwardTrace.typeMapperTrace as Logic2AlloyLanguageMapper_TypeMapperTrace_FilteredTypes
+                
+                // 1. Evaluate the defined elements
+                for(definedElementMappingEntry : typeTrace.definedElement2Declaration.entrySet) {
+                        val name = definedElementMappingEntry.value.name
+                        val matchingSig = '''this/«name»'''.toString.lookup(name2AlloySig)
+                        val elementsOfSingletonSignature = solution.eval(matchingSig)
+                        if(elementsOfSingletonSignature.size != 1) {
+                                throw new IllegalArgumentException('''Defined element is unambigous: "«name»", possible values: «elementsOfSingletonSignature»!''')
+                        } else {
+                                val expressionOfDefinedElement  = elementsOfSingletonSignature.head.atom(0)// as ExprVar
+                                expression2DefinedElement.put(expressionOfDefinedElement, definedElementMappingEntry.key)
+                        }
+                }
+                
+                // 2. evaluate the signatures and create new elements if necessary
+                for(type2SingatureEntry : typeTrace.type2ALSType.entrySet) {
+                        val type = type2SingatureEntry.key
+                        if(type instanceof TypeDeclaration) {
+                                val name = type2SingatureEntry.value.name
+                                val matchingSig = '''this/«name»'''.toString.lookup(name2AlloySig)
+                                val elementsOfSignature = solution.eval(matchingSig)
+                                val elementList = new ArrayList(elementsOfSignature.size)
+                                var newVariableIndex = 1;
+                                for(elementOfSignature : elementsOfSignature) {
+                                        val expressionOfDefinedElement  = elementOfSignature.atom(0)
+                                        if(expression2DefinedElement.containsKey(expressionOfDefinedElement)) {
+                                                elementList += expressionOfDefinedElement.lookup(expression2DefinedElement)
+                                        } else {
+                                                val newElementName = '''newObject «newVariableIndex.toString»'''
+                                                val newRepresentation = createDefinedElement => [
+                                                        it.name = newElementName
+                                                ]
+                                                elementList += newRepresentation
+                                                expression2DefinedElement.put(expressionOfDefinedElement,newRepresentation)
+                                        }
+                                }
+                                interpretationOfUndefinedType.put(type,elementList)
+                        }
+                }
+        }
+}
+/*
+class AlloyModelInterpretation_TypeInterpretation_Horizontal implements AlloyModelInterpretation_TypeInterpretation{
+        protected val extension LogiclanguageFactory factory = LogiclanguageFactory.eINSTANCE
+        
+        override resolveUnknownAtoms(Iterable<ExprVar> objectAtoms, Logic2AlloyLanguageMapperTrace forwardTrace, Map<String,DefinedElement> alloyAtom2LogicElement) {
+                val Map<TypeDeclaration, List<DefinedElement>> interpretationOfUndefinedType = new HashMap;
+                
+                //TMP sig maps to identify alloy signatures by their names
+                val Map<String,Type> sigName2LogicType =
+                        forwardTrace.type2ALSType.keySet.toMap[x|forwardTrace.type2ALSType.get(x).name]
+                //val Map<String,DefinedElement> elementNameNamel2DefinedElement = 
+                //      forwardTrace.definedElement2Declaration.keySet.toMap[x|forwardTrace.definedElement2Declaration.get(x).name]
+                        
+                // Fill the interpretation map with empty lists
+                forwardTrace.type2ALSType.keySet.filter(TypeDeclaration).forEach[x|interpretationOfUndefinedType.put(x,new LinkedList)]
+                
+                // exporing individuals
+                for(atom: objectAtoms) {
+                        val typeName = getName(atom.type)
+                        //val atomName = atom.name
+                        
+                        if(sigName2LogicType.containsKey(typeName)) {
+                                val type = sigName2LogicType.get(typeName)
+                                val elementsOfType = interpretationOfUndefinedType.get(type)
+                                val element = createDefinedElement => [
+                                        it.name += type.name
+                                        it.name += (elementsOfType.size+1).toString
+                                ]
+                                alloyAtom2LogicElement.put(atom.label,element)
+                                elementsOfType+=element
+                        }
+                        else throw new UnsupportedOperationException('''Unknown atom: «atom»''')
+                }
+                
+                return interpretationOfUndefinedType
+        }
+        
+        def private getName(edu.mit.csail.sdg.alloy4compiler.ast.Type type) {
+                val name = type.toString
+                if(name.startsWith("{this/") && name.endsWith("}")) {
+                        return type.toString.replaceFirst("\\{this\\/","").replace("}","")
+                }
+                else throw new IllegalArgumentException('''Unknown type format: "«name»"!''')
+        }
+        //def private getName(ExprVar atom) { atom.toString.split("\\$") }
+}*/
+class AlloyModelInterpretation implements LogicModelInterpretation{
+        
+        protected val extension LogiclanguageFactory factory = LogiclanguageFactory.eINSTANCE
+        protected val AlloyModelInterpretation_TypeInterpretation typeInterpretator
+                
+        protected val Logic2AlloyLanguageMapper forwardMapper
+        protected val Logic2AlloyLanguageMapperTrace forwardTrace;
+        
+        private var ExprVar logicLanguage;
+        
+        private var String logicBooleanTrue;
+        private var String logicBooleanFalse;
+                
+        private val Map<String, DefinedElement> alloyAtom2LogicElement = new HashMap
+        private val Map<TypeDeclaration, List<DefinedElement>> interpretationOfUndefinedType = new HashMap
+        
+        private val Map<ConstantDeclaration, Object> constant2Value
+        private val Map<FunctionDeclaration, ? extends Map<ParameterSubstitution, Object>> function2Value
+        private val Map<RelationDeclaration, ? extends Set<ParameterSubstitution>> relation2Value
+        
+        private val int minInt
+        private val int maxInt
+        
+        public new (AlloyModelInterpretation_TypeInterpretation typeInterpretator, A4Solution solution, Logic2AlloyLanguageMapper forwardMapper, Logic2AlloyLanguageMapperTrace trace) {
+                this.typeInterpretator = typeInterpretator
+                this.forwardMapper = forwardMapper
+                this.forwardTrace = trace
+                
+                // Maps to trace language elements to the parsed problem.
+                val Map<String, Sig> name2AlloySig = new HashMap
+                val Map<String, Field> name2AlloyField = new HashMap
+                // exploring signatures
+                for(sig:solution.allReachableSigs) {
+                        name2AlloySig.put(sig.label,sig)
+                        for(field : sig.fields) {
+                                name2AlloyField.put(field.label,field)
+                        }
+                }
+                
+                val unknownAtoms = collectUnknownAndResolveKnownAtoms(solution.allAtoms)
+                this.typeInterpretator.resolveUnknownAtoms(
+                        unknownAtoms,
+                        solution,
+                        forwardTrace,
+                        name2AlloySig,
+                        name2AlloyField,
+                        alloyAtom2LogicElement,
+                        interpretationOfUndefinedType)
+                
+                // eval consants
+                constant2Value = forwardTrace.constantDeclaration2LanguageField.mapValues[
+                        solution.eval(it.name.lookup(name2AlloyField)).head.atom(1).atomLabel2Term
+                ]
+                // eval functions
+                val hostedfunction2Value = forwardTrace.functionDeclaration2HostedField.mapValues[ function |
+                        newHashMap(
+                                solution.eval(function.name.lookup(name2AlloyField))
+                                        .map[t | new ParameterSubstitution(#[t.atom(0).atomLabel2Term]) -> t.atom(1).atomLabel2Term])]
+                
+                val globalfunction2Value = forwardTrace.functionDeclaration2LanguageField.keySet.toInvertedMap[ function |
+                        val alsFunction = function.lookup(forwardTrace.functionDeclaration2LanguageField)
+                        val paramIndexes = 1..(function.parameters.size)
+                        return newHashMap(
+                                solution.eval(alsFunction.name.lookup(name2AlloyField)).map[t |
+                                        new ParameterSubstitution(paramIndexes.map[t.atom(it).atomLabel2Term])
+                                                ->
+                                        t.atom(function.parameters.size + 1).atomLabel2Term
+                                ])]
+                this.function2Value = Union(hostedfunction2Value,globalfunction2Value)
+                // eval relations
+                val hostedRelation2Value = forwardTrace.relationDeclaration2Field.mapValues[ relation |
+                        solution.eval(relation.name.lookup(name2AlloyField)).map[ t |
+                                new ParameterSubstitution(#[t.atom(0).atomLabel2Term,t.atom(1).atomLabel2Term])].toSet]
+                val globalRelation2Value = forwardTrace.relationDeclaration2Global.mapValues[ relation |
+                        solution.eval(relation.name.lookup(name2AlloyField)).map[ t |
+                                new ParameterSubstitution((1..<t.arity).map[int a|t.atom(a).atomLabel2Term])].toSet]
+                this.relation2Value = Union(hostedRelation2Value,globalRelation2Value)
+                
+                //Int limits
+                this.minInt = solution.min
+                this.maxInt = solution.max
+                
+                //print(trace)
+        }
+        
+        def List<ExprVar> collectUnknownAndResolveKnownAtoms(Iterable<ExprVar> allAtoms) {
+                val List<ExprVar> unknownAtoms = new LinkedList
+                
+                for(atom: allAtoms) {
+                        val typeName = getName(atom.type)
+                        val atomName = atom.name
+                        //println(atom.toString + "  < -  " + typeName)
+                        if(typeName == forwardTrace.logicLanguage.name) {
+                                this.logicLanguage = atom
+                        } else if(typeName == "Int" || typeName == "seq/Int") {
+                                // do nothing, integers will be parsed from the string
+                        } else if(forwardTrace.boolType != null && typeName == forwardTrace.boolType.name) {
+                                if(atomName.head == forwardTrace.boolTrue.name) { this.logicBooleanTrue = atom.label }
+                                else if(atomName.head == forwardTrace.boolFalse.name) { this.logicBooleanFalse = atom.label}
+                                else throw new UnsupportedOperationException('''Unknown boolean value: «atom»''')
+                        }
+                        else unknownAtoms += atom
+                }
+                
+                return unknownAtoms
+        }
+        
+        def private getName(edu.mit.csail.sdg.alloy4compiler.ast.Type type) {
+                val name = type.toString
+                if(name.startsWith("{this/") && name.endsWith("}")) {
+                        return type.toString.replaceFirst("\\{this\\/","").replace("}","")
+                }
+                else throw new IllegalArgumentException('''Unknown type format: "«name»"!''')
+        }
+        def private getName(ExprVar atom) { atom.toString.split("\\$") }
+        
+        def print(Logic2AlloyLanguageMapperTrace trace) {
+                println('''Undefined-----''')
+                interpretationOfUndefinedType.forEach[k,v|println('''«k.name» -> «v.map[name]»''')]
+                //println('''Defined-----''')
+                //trace.type2ALSType.keySet.filter(TypeDefinition).forEach[println('''«it.name» -> «it.elements.map[name.join]»''')]
+                
+                println('''Constants-----''')
+                constant2Value.forEach[k, v|println('''«k.name» : «v»''')]
+                println('''Functions-----''')
+                function2Value.forEach[f,m|m.forEach[k,v| println('''«f.name» : «k» |-> «v»''')]]
+                println('''Relations-----''')
+                relation2Value.forEach[r,s|s.forEach[t | println('''«r.name»: («t»)''')]]
+        }
+        override getElements(Type type) { getElementsDispatch(type) }
+        def private dispatch getElementsDispatch(TypeDeclaration declaration) { return declaration.lookup(this.interpretationOfUndefinedType) }
+        def private dispatch getElementsDispatch(TypeDefinition declaration) { return declaration.elements }
+        
+        override getInterpretation(FunctionDeclaration function, Object[] parameterSubstitution) {
+                val transformedParams = new ParameterSubstitution(parameterSubstitution)
+                return transformedParams.lookup(
+                        function.lookup(this.function2Value)
+                )
+        }
+        
+        override getInterpretation(RelationDeclaration relation, Object[] parameterSubstitution) {
+                relation.lookup(this.relation2Value).contains(new ParameterSubstitution(parameterSubstitution))
+        }
+        
+        override getInterpretation(ConstantDeclaration constant) {
+                constant.lookup(this.constant2Value)
+        }
+        
+        override getMinimalInteger() { this.minInt }
+        override getMaximalInteger() { this.maxInt }
+        
+        // Alloy term -> logic term
+        def private atomLabel2Term(String label) {
+                if(label.number) return Integer.parseInt(label)
+                else if(label == this.logicBooleanTrue) return true
+                else if(label == this.logicBooleanFalse) return false
+                else if(this.alloyAtom2LogicElement.containsKey(label)) return label.lookup(alloyAtom2LogicElement)
+                else throw new IllegalArgumentException('''Unknown atom label: "«label»"!''')
+        }
+        def private isNumber(String s) {
+                try{
+                        Integer.parseInt(s)
+                        return true
+                }catch(NumberFormatException e) {
+                        return false
+                }
+        }
+}
+/**
+ * Helper class for efficiently matching parameter substitutions for functions and relations.
+ */
+class ParameterSubstitution{
+        val Object[] data;
+        
+        new(Object[] data) { this.data = data }
+        
+        override equals(Object obj) {
+                if(obj === this) return true
+                else if(obj == null) return false
+                if(obj instanceof ParameterSubstitution) {
+                        return Arrays.equals(this.data,obj.data)
+                }
+                return false
+        }
+        
+        override hashCode() {
+                Arrays.hashCode(data)
+        }
+}
+\ No newline at end of file
diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper.xtend b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper.xtend
new file mode 100644
index 00000000..23b9027f
--- /dev/null
+++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper.xtend
@@ -0,0 +1,467 @@
+package hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder
+import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.AlloySolverConfiguration
+import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSDocument
+import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSEnumLiteral
+import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSMultiplicity
+import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSNumericOperator
+import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSTerm
+import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSVariableDeclaration
+import hu.bme.mit.inf.dslreasoner.alloyLanguage.AlloyLanguageFactory
+import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration
+import hu.bme.mit.inf.dslreasoner.logic.model.builder.TracedOutput
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.And
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Assertion
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.BoolLiteral
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.BoolTypeReference
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ConstantDeclaration
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ConstantDefinition
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Distinct
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Divison
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Equals
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Exists
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Forall
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.FunctionDeclaration
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.FunctionDefinition
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Iff
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Impl
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.InstanceOf
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.IntLiteral
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.IntTypeReference
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.LessOrEqualThan
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.LessThan
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Minus
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Mod
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.MoreOrEqualThan
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.MoreThan
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Multiply
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Not
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Or
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Plus
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RealLiteral
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RealTypeReference
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.SymbolicValue
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Term
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable
+import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem
+import java.util.Collections
+import java.util.HashMap
+import java.util.List
+import java.util.Map
+import org.eclipse.viatra.query.runtime.api.ViatraQueryEngine
+import org.eclipse.viatra.query.runtime.emf.EMFScope
+import org.eclipse.xtend.lib.annotations.Accessors
+import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*
+import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.Annotation
+import hu.bme.mit.inf.dslreasoner.ecore2logic.ecore2logicannotations.InverseRelationAssertion
+import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.AssertionAnnotation
+import java.util.Collection
+import hu.bme.mit.inf.dslreasoner.ecore2logic.ecore2logicannotations.LowerMultiplicityAssertion
+import hu.bme.mit.inf.dslreasoner.ecore2logic.ecore2logicannotations.UpperMultiplicityAssertion
+import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSDirectProduct
+class Logic2AlloyLanguageMapper {
+        private val extension AlloyLanguageFactory factory = AlloyLanguageFactory.eINSTANCE
+        private val Logic2AlloyLanguageMapper_Support support = new Logic2AlloyLanguageMapper_Support;
+        @Accessors(PUBLIC_GETTER) private val Logic2AlloyLanguageMapper_TypeMapper typeMapper;
+        @Accessors(PUBLIC_GETTER) private val Logic2AlloyLanguageMapper_ConstantMapper constantMapper = new Logic2AlloyLanguageMapper_ConstantMapper(this)
+        @Accessors(PUBLIC_GETTER) private val Logic2AlloyLanguageMapper_FunctionMapper functionMapper = new Logic2AlloyLanguageMapper_FunctionMapper(this)
+        @Accessors(PUBLIC_GETTER) private val Logic2AlloyLanguageMapper_RelationMapper relationMapper = new Logic2AlloyLanguageMapper_RelationMapper(this)
+        @Accessors(PUBLIC_GETTER) private val Logic2AlloyLanguageMapper_Containment containmentMapper = new Logic2AlloyLanguageMapper_Containment(this)
+        
+        public new(Logic2AlloyLanguageMapper_TypeMapper typeMapper) {
+                this.typeMapper = typeMapper
+        }
+        
+        public def TracedOutput<ALSDocument,Logic2AlloyLanguageMapperTrace> transformProblem(LogicProblem problem, AlloySolverConfiguration config) {
+                val logicLanguage = createALSSignatureBody => [
+                                it.multiplicity = ALSMultiplicity.ONE
+                                it.declarations +=
+                                        createALSSignatureDeclaration => [
+                                                        it.name = support.toID(#["util", "language"]) ] 
+                ]
+                
+                val specification = createALSDocument=>[
+                        it.signatureBodies+=logicLanguage
+                ]
+                val trace = new Logic2AlloyLanguageMapperTrace => [
+                        it.specification = specification
+                        it.logicLanguage = logicLanguage.declarations.head
+                        it.logicLanguageBody = logicLanguage
+                        
+                        it.incqueryEngine = ViatraQueryEngine.on(new EMFScope(problem))
+                ]
+                
+                typeMapper.transformTypes(problem.types,problem.elements,this,trace)
+                
+                trace.constantDefinitions = problem.collectConstantDefinitions
+                trace.functionDefinitions = problem.collectFunctionDefinitions
+                trace.relationDefinitions = problem.collectRelationDefinitions
+                
+                problem.constants.forEach[this.constantMapper.transformConstant(it,trace)]
+                problem.functions.forEach[this.functionMapper.transformFunction(it, trace)]
+                problem.relations.forEach[this.relationMapper.transformRelation(it, trace)]
+                
+                problem.constants.filter(ConstantDefinition).forEach[this.constantMapper.transformConstantDefinitionSpecification(it,trace)]
+                problem.functions.filter(FunctionDefinition).forEach[this.functionMapper.transformFunctionDefinitionSpecification(it,trace)]
+                problem.relations.filter(RelationDefinition).forEach[this.relationMapper.transformRelationDefinitionSpecification(it,trace)]
+                
+                val containment = problem.getContainmentHierarchies.head
+                if(containment !== null) {
+                        this.containmentMapper.transformContainmentHierarchy(containment,trace)
+                }
+                
+                ////////////////////
+                // Collect EMF-specific assertions
+                ////////////////////
+                val assertion2InverseRelation = problem.annotations.collectAnnotations(InverseRelationAssertion)
+                val assertion2UpperMultiplicityAssertion = problem.annotations.collectAnnotations(UpperMultiplicityAssertion)
+                val assertion2LowerMultiplicityAssertion = problem.annotations.collectAnnotations(LowerMultiplicityAssertion)
+                
+                ////////////////////
+                // Transform Assertions
+                ////////////////////
+                for(assertion : problem.assertions) {
+                        if(assertion2InverseRelation.containsKey(assertion)) {
+                                transformInverseAssertion(assertion.lookup(assertion2InverseRelation),trace)
+                        } else if(assertion2UpperMultiplicityAssertion.containsKey(assertion)) {
+                                transformUpperMultiplicityAssertion(assertion.lookup(assertion2UpperMultiplicityAssertion),trace)
+                        } else if(assertion2LowerMultiplicityAssertion.containsKey(assertion)) {
+                                transformLowerMultiplicityAssertion(assertion.lookup(assertion2LowerMultiplicityAssertion),trace)
+                        } else {
+                                transformAssertion(assertion,trace)
+                        }
+                }
+                
+                transformRunCommand(specification, trace, config)
+                
+                return new TracedOutput(specification,trace)
+        }
+        
+        def transformInverseAssertion(InverseRelationAssertion assertion, Logic2AlloyLanguageMapperTrace trace) {
+                val a = assertion.inverseA
+                val b = assertion.inverseB
+                if(a instanceof RelationDeclaration && b instanceof RelationDeclaration &&
+                        !trace.relationDefinitions.containsKey(a) && !trace.relationDefinitions.containsKey(b))
+                {
+                        val fact = createALSFactDeclaration => [
+                                it.name = support.toID(assertion.target.name)
+                                it.term = createALSEquals => [
+                                        it.leftOperand = relationMapper.transformRelationReference(a as RelationDeclaration, trace)
+                                        it.rightOperand = createALSInverseRelation => [it.operand = relationMapper.transformRelationReference(b as RelationDeclaration, trace) ]
+                                ]
+                        ]
+                        trace.specification.factDeclarations += fact
+                } else {
+                        return transformAssertion(assertion.target,trace)
+                }
+        }
+        
+        def transformUpperMultiplicityAssertion(UpperMultiplicityAssertion assertion, Logic2AlloyLanguageMapperTrace trace) {
+                val x = assertion.relation
+                if(x instanceof RelationDeclaration && !trace.relationDefinitions.containsKey(x)) {
+                        val relation = relationMapper.getRelationReference((x as RelationDeclaration),trace)
+                        val type = relation.type
+                        
+                        if(type instanceof ALSDirectProduct) {
+                                type.rightMultiplicit = type.rightMultiplicit.addUpper
+                        } else {
+                                relation.multiplicity = relation.multiplicity.addUpper
+                        }
+                        
+                        if(assertion.upper === 1) {
+                                return true
+                        } else {
+                                return transformAssertion(assertion.target,trace)
+                        }
+                        
+                } else {
+                        return transformAssertion(assertion.target,trace)
+                }
+        }
+        
+        def transformLowerMultiplicityAssertion(LowerMultiplicityAssertion assertion, Logic2AlloyLanguageMapperTrace trace) {
+                val x = assertion.relation
+                if(x instanceof RelationDeclaration && !trace.relationDefinitions.containsKey(x)) {
+                        val relation = relationMapper.getRelationReference((x as RelationDeclaration),trace)
+                        val type = relation.type
+                        
+                        if(type instanceof ALSDirectProduct) {
+                                type.rightMultiplicit = type.rightMultiplicit.addLower
+                        } else {
+                                relation.multiplicity = relation.multiplicity.addLower
+                        }
+                        
+                        if(assertion.lower === 1) {
+                                return true
+                        } else {
+                                return transformAssertion(assertion.target,trace)
+                        }
+                        
+                } else {
+                        return transformAssertion(assertion.target,trace)
+                }
+        }
+        
+        private def addLower(ALSMultiplicity multiplicity) {
+                if(multiplicity === ALSMultiplicity::SET || multiplicity === null) {
+                        return ALSMultiplicity::SOME
+                } else if(multiplicity === ALSMultiplicity::LONE) {
+                        return ALSMultiplicity::ONE
+                } else {
+                        throw new IllegalArgumentException('''Lower multiplicity is already set!''')
+                }
+        }
+        private def addUpper(ALSMultiplicity multiplicity) {
+                if(multiplicity === ALSMultiplicity::SET || multiplicity === null) {
+                        return ALSMultiplicity::LONE
+                } else if(multiplicity === ALSMultiplicity::SOME) {
+                        return ALSMultiplicity::ONE
+                } else {
+                        throw new IllegalArgumentException('''Upper multiplicity is already set!''')
+                }
+        }
+        
+        private def <T extends AssertionAnnotation>  collectAnnotations(Collection<? extends Annotation> collection, Class<T> annotationKind) {
+                val res = new HashMap
+                collection.filter(annotationKind).forEach[res.put(it.target,it)]
+                return res
+        }
+        
+        private def collectConstantDefinitions(LogicProblem problem) {
+                val res = new HashMap
+                problem.constants.filter(ConstantDefinition).filter[it.defines!==null].forEach[
+                        res.put(it.defines,it)
+                ]
+                return res
+        }
+        private def collectFunctionDefinitions(LogicProblem problem) {
+                val res = new HashMap
+                problem.functions.filter(FunctionDefinition).filter[it.defines!==null].forEach[
+                        res.put(it.defines,it)
+                ]
+                return res
+        }
+        private def collectRelationDefinitions(LogicProblem problem) {
+                val res = new HashMap
+                problem.relations.filter(RelationDefinition).filter[it.defines!==null].forEach[
+                        res.put(it.defines,it)
+                ]
+                return res
+        }
+        
+        ////////////////////
+        // Type References
+        ////////////////////
+        def dispatch protected ALSTerm transformTypeReference(BoolTypeReference boolTypeReference, Logic2AlloyLanguageMapperTrace trace) {
+                return createALSReference => [ it.referred = support.getBooleanType(trace) ]
+        }
+        def dispatch protected ALSTerm transformTypeReference(IntTypeReference intTypeReference, Logic2AlloyLanguageMapperTrace trace) { createALSInt }
+        def dispatch protected ALSTerm transformTypeReference(RealTypeReference realTypeReference, Logic2AlloyLanguageMapperTrace trace) {throw new UnsupportedOperationException('''Real types are not supported in Alloy.''')}
+        def dispatch protected ALSTerm transformTypeReference(ComplexTypeReference complexTypeReference, Logic2AlloyLanguageMapperTrace trace) {
+                val types = typeMapper.transformTypeReference(complexTypeReference.referred, this, trace)
+                return support.unfoldPlus(types.map[t|createALSReference=>[referred = t]])
+        }       
+        
+        //////////////
+        // Scopes
+        //////////////
+        
+        def transformRunCommand(ALSDocument specification, Logic2AlloyLanguageMapperTrace trace, AlloySolverConfiguration config) {
+                specification.runCommand = createALSRunCommand => [
+                        it.typeScopes+= createALSSigScope => [
+                                it.type= typeMapper.getUndefinedSupertype(trace)
+                                it.number = typeMapper.getUndefinedSupertypeScope(config.typeScopes.maxNewElements,trace) 
+                                //it.exactly = (config.typeScopes.maxElements == config.typeScopes.minElements)
+                        ]
+                        if(config.typeScopes.maxIntScope == LogicSolverConfiguration::Unlimited) throw new UnsupportedOperationException(
+                                '''An integer scope have to be specified for Alloy!''')
+                        it.typeScopes += createALSIntScope => [
+                                number = Integer.SIZE-Integer.numberOfLeadingZeros(config.typeScopes.maxIntScope)
+                        ]
+//                      for(definedScope : config.typeScopes.allDefinedScope) {
+//                              it.typeScopes += createALSSigScope => [
+//                                      it.type = definedScope.type.lookup(trace.type2ALSType)
+//                                      it.number = definedScope.upperLimit
+//                                      it.exactly = (definedScope.upperLimit == definedScope.lowerLimit)
+//                              ]
+//                      }
+                ]
+        }
+        
+        
+        //////////////
+        // Assertions + Terms
+        //////////////
+        
+        def protected transformAssertion(Assertion assertion, Logic2AlloyLanguageMapperTrace trace) {
+                val res = createALSFactDeclaration => [
+                        it.name = support.toID(assertion.name)
+                        it.term = assertion.value.transformTerm(trace,Collections.EMPTY_MAP)
+                ]
+                trace.specification.factDeclarations += res
+        }       
+        
+        def dispatch protected ALSTerm transformTerm(BoolLiteral literal, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) {
+                var ALSEnumLiteral ref;
+                if(literal.value==true) {ref = support.getBooleanTrue(trace)}
+                else {ref = support.getBooleanFalse(trace)}
+                val refFinal = ref
+                
+                return  support.booleanToLogicValue((createALSReference => [referred = refFinal]),trace)
+        }
+        def dispatch protected ALSTerm transformTerm(RealLiteral literal, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) {
+                throw new UnsupportedOperationException("RealLiteral is not supported")
+        }
+        def dispatch protected ALSTerm transformTerm(IntLiteral literal, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables)  {
+                if(literal.value>=0) { createALSNumberLiteral => [value = literal.value]}
+                else {createALSUnaryMinus  => [it.operand = createALSNumberLiteral => [value = literal.value] ] } 
+        }
+        
+        def dispatch protected ALSTerm transformTerm(Not not, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) {
+                createALSNot=>[operand = not.operand.transformTerm(trace,variables)] }
+        def dispatch protected ALSTerm transformTerm(And and, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) {
+                support.unfoldAnd(and.operands.map[transformTerm(trace,variables)]) }
+        def dispatch protected ALSTerm transformTerm(Or or, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) {
+                support.unfoldOr(or.operands.map[transformTerm(trace,variables)],trace) }
+        def dispatch protected ALSTerm transformTerm(Impl impl, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) {
+                createALSImpl => [leftOperand = impl.leftOperand.transformTerm(trace,variables) rightOperand = impl.rightOperand.transformTerm(trace,variables)] }
+        def dispatch protected ALSTerm transformTerm(Iff iff, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) {
+                createALSIff => [leftOperand = iff.leftOperand.transformTerm(trace,variables) rightOperand = iff.rightOperand.transformTerm(trace,variables)] }
+        def dispatch protected ALSTerm transformTerm(MoreThan moreThan, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) {
+                createALSMore => [leftOperand = moreThan.leftOperand.transformTerm(trace,variables) rightOperand = moreThan.rightOperand.transformTerm(trace,variables)] }
+        def dispatch protected ALSTerm transformTerm(LessThan lessThan, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) {
+                createALSLess => [leftOperand = lessThan.leftOperand.transformTerm(trace,variables) rightOperand = lessThan.rightOperand.transformTerm(trace,variables)] }
+        def dispatch protected ALSTerm transformTerm(MoreOrEqualThan moreThan, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) {
+                createALSMeq => [leftOperand = moreThan.leftOperand.transformTerm(trace,variables) rightOperand = moreThan.rightOperand.transformTerm(trace,variables)] }
+        def dispatch protected ALSTerm transformTerm(LessOrEqualThan lessThan, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) {
+                createALSLeq => [leftOperand = lessThan.leftOperand.transformTerm(trace,variables) rightOperand = lessThan.rightOperand.transformTerm(trace,variables)] }
+        def dispatch protected ALSTerm transformTerm(Equals equals, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) {
+                createALSEquals => [leftOperand = equals.leftOperand.transformTerm(trace,variables) rightOperand = equals.rightOperand.transformTerm(trace,variables)] }
+        def dispatch protected ALSTerm transformTerm(Distinct distinct, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) {
+                support.unfoldDistinctTerms(this,distinct.operands,trace,variables) }
+                
+        def dispatch protected ALSTerm transformTerm(Plus plus, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) {
+                createALSFunctionCall => [it.params += plus.leftOperand.transformTerm(trace,variables) it.params += plus.rightOperand.transformTerm(trace,variables) it.referredNumericOperator = ALSNumericOperator.PLUS] }
+        def dispatch protected ALSTerm transformTerm(Minus minus, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) {
+                createALSFunctionCall => [it.params += minus.leftOperand.transformTerm(trace,variables) it.params += minus.rightOperand.transformTerm(trace,variables) it.referredNumericOperator = ALSNumericOperator.SUB] }
+        def dispatch protected ALSTerm transformTerm(Multiply multiply, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) {
+                createALSFunctionCall => [it.params += multiply.leftOperand.transformTerm(trace,variables) it.params += multiply.rightOperand.transformTerm(trace,variables) it.referredNumericOperator = ALSNumericOperator.MUL] }
+        def dispatch protected ALSTerm transformTerm(Divison div, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) {
+                createALSFunctionCall => [it.params += div.leftOperand.transformTerm(trace,variables) it.params += div.rightOperand.transformTerm(trace,variables) it.referredNumericOperator = ALSNumericOperator.DIV] }
+        def dispatch protected ALSTerm transformTerm(Mod mod, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) {
+                createALSFunctionCall => [it.params += mod.leftOperand.transformTerm(trace,variables) it.params += mod.rightOperand.transformTerm(trace,variables) it.referredNumericOperator = ALSNumericOperator.REM] }
+        
+        def dispatch protected ALSTerm transformTerm(Forall forall, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) {
+                support.createQuantifiedExpression(this,forall,ALSMultiplicity.ALL,trace,variables) }
+        def dispatch protected ALSTerm transformTerm(Exists exists, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) {
+                support.createQuantifiedExpression(this,exists,ALSMultiplicity.SOME,trace,variables) }
+        
+        def dispatch protected ALSTerm transformTerm(InstanceOf instanceOf, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) {
+                return createALSSubset => [
+                        it.leftOperand = instanceOf.value.transformTerm(trace,variables)
+                        it.rightOperand = instanceOf.range.transformTypeReference(trace)
+                ]
+        }
+        
+        def dispatch protected ALSTerm transformTerm(SymbolicValue symbolicValue, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) {
+                symbolicValue.symbolicReference.transformSymbolicReference(symbolicValue.parameterSubstitutions,trace,variables) }
+        
+        def dispatch protected ALSTerm transformSymbolicReference(DefinedElement referred, List<Term> parameterSubstitutions, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) {
+                typeMapper.transformReference(referred,trace)}
+        def dispatch protected ALSTerm transformSymbolicReference(ConstantDeclaration constant, List<Term> parameterSubstitutions, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) {
+                if(trace.constantDefinitions.containsKey(constant)) {
+                        return this.transformSymbolicReference(constant.lookup(trace.constantDefinitions),parameterSubstitutions,trace,variables)
+                } else {
+                        val res = createALSJoin=> [
+                                leftOperand = createALSReference => [ referred = trace.logicLanguage ]
+                                rightOperand = createALSReference => [ referred = constant.lookup(trace.constantDeclaration2LanguageField) ]
+                        ]
+                        return support.postprocessResultOfSymbolicReference(constant.type,res,trace)
+                }
+        }
+        def dispatch protected ALSTerm transformSymbolicReference(ConstantDefinition constant, List<Term> parameterSubstitutions, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) {
+                val res = createALSFunctionCall => [
+                        it.referredDefinition = constant.lookup(trace.constantDefinition2Function)
+                ]
+                return support.postprocessResultOfSymbolicReference(constant.type,res,trace)
+        }
+        def dispatch protected ALSTerm transformSymbolicReference(Variable variable, List<Term> parameterSubstitutions, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) {
+                val res = createALSReference => [referred = variable.lookup(variables)]
+                return support.postprocessResultOfSymbolicReference(variable.range,res,trace)
+        }
+        def dispatch protected ALSTerm transformSymbolicReference(FunctionDeclaration function, List<Term> parameterSubstitutions, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) {
+                if(trace.functionDefinitions.containsKey(function)) {
+                        return this.transformSymbolicReference(function.lookup(trace.functionDefinitions),parameterSubstitutions,trace,variables)
+                } else {
+                        if(functionMapper.transformedToHostedField(function,trace)) {
+                                val param = parameterSubstitutions.get(0).transformTerm(trace,variables)
+                                val res = createALSJoin => [
+                                        leftOperand = support.prepareParameterOfSymbolicReference(function.parameters.get(0),param,trace)
+                                        rightOperand = createALSReference => [referred = function.lookup(trace.functionDeclaration2HostedField)]
+                                ]
+                                return support.postprocessResultOfSymbolicReference(function.range,res,trace)
+                        } else {
+                                val functionExpression = createALSJoin=>[
+                                                leftOperand = createALSReference => [referred = trace.logicLanguage]
+                                                rightOperand = createALSReference => [referred = function.lookup(trace.functionDeclaration2LanguageField)]
+                                        ]
+                                val res =  support.unfoldDotJoin(this,parameterSubstitutions,functionExpression,trace,variables)
+                                return support.postprocessResultOfSymbolicReference(function.range,res,trace)
+                        }
+                }
+        }
+        def dispatch protected ALSTerm transformSymbolicReference(FunctionDefinition function, List<Term> parameterSubstitutions, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) {
+                val result = createALSFunctionCall => [
+                        it.referredDefinition = function.lookup(trace.functionDefinition2Function)
+                        it.params += parameterSubstitutions.map[it.transformTerm(trace,variables)]
+                ]
+                return support.postprocessResultOfSymbolicReference(function.range,result,trace)
+        }
+        def dispatch protected ALSTerm transformSymbolicReference(RelationDeclaration relation, List<Term> parameterSubstitutions,
+                Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) {
+                if(trace.relationDefinitions.containsKey(relation)) {
+                        this.transformSymbolicReference(relation.lookup(trace.relationDefinitions),parameterSubstitutions,trace,variables)
+                } else {
+                        if(relationMapper.transformToHostedField(relation,trace)) {
+                                val alsRelation = relation.lookup(trace.relationDeclaration2Field)
+                                // R(a,b) =>
+                                // b in a.R
+                                return createALSSubset => [
+                                        it.leftOperand = parameterSubstitutions.get(1).transformTerm(trace,variables)
+                                        it.rightOperand = createALSJoin => [
+                                                it.leftOperand = parameterSubstitutions.get(0).transformTerm(trace,variables)
+                                                it.rightOperand = createALSReference => [ it.referred = alsRelation ]
+                                        ]
+                                ]
+                        } else {
+                                val target = createALSJoin => [
+                                        leftOperand = createALSReference => [referred = trace.logicLanguage]
+                                        rightOperand = createALSReference => [ referred = relation.lookup(trace.relationDeclaration2Global) ]]
+                                val source = support.unfoldTermDirectProduct(this,parameterSubstitutions,trace,variables)
+                                
+                                return  createALSSubset => [
+                                        leftOperand = source
+                                        rightOperand = target
+                                ]
+                        }
+                }
+        }
+        
+        
+        def dispatch protected ALSTerm transformSymbolicReference(RelationDefinition relation, List<Term> parameterSubstitutions,
+                Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables)
+        {
+                return createALSFunctionCall => [
+                        it.referredDefinition = relation.lookup(trace.relationDefinition2Predicate)
+                        it.params += parameterSubstitutions.map[p | p.transformTerm(trace,variables)]
+                ]
+        }
+}
+\ No newline at end of file
diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapperTrace.xtend b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapperTrace.xtend
new file mode 100644
index 00000000..22f49c98
--- /dev/null
+++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapperTrace.xtend
@@ -0,0 +1,49 @@
+package hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder
+import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSDocument
+import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSEnumDeclaration
+import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSEnumLiteral
+import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSFieldDeclaration
+import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSFunctionDefinition
+import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSRelationDefinition
+import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSSignatureBody
+import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSSignatureDeclaration
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ConstantDeclaration
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ConstantDefinition
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.FunctionDeclaration
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.FunctionDefinition
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition
+import java.util.HashMap
+import java.util.Map
+import org.eclipse.viatra.query.runtime.api.ViatraQueryEngine
+interface Logic2AlloyLanguageMapper_TypeMapperTrace {}
+class Logic2AlloyLanguageMapperTrace {
+        public var ViatraQueryEngine incqueryEngine;
+        
+        public var ALSDocument specification;
+        public var ALSSignatureDeclaration logicLanguage;
+        public var ALSSignatureBody logicLanguageBody;
+        public var ALSEnumDeclaration boolType;
+        public var ALSEnumLiteral boolTrue;
+        public var ALSEnumLiteral boolFalse;
+        
+        public var Logic2AlloyLanguageMapper_TypeMapperTrace typeMapperTrace 
+        
+        public val Map<ConstantDeclaration, ALSFieldDeclaration> constantDeclaration2LanguageField = new HashMap
+        public val Map<ConstantDefinition, ALSFunctionDefinition> constantDefinition2Function = new HashMap
+        
+        public val Map<FunctionDeclaration,ALSFieldDeclaration> functionDeclaration2HostedField = new HashMap
+        public val Map<FunctionDeclaration,ALSFieldDeclaration> functionDeclaration2LanguageField = new HashMap
+        public val Map<FunctionDefinition,ALSFunctionDefinition> functionDefinition2Function = new HashMap
+        
+        public val Map<RelationDeclaration,ALSFieldDeclaration> relationDeclaration2Global = new HashMap
+        public val Map<RelationDeclaration, ALSFieldDeclaration> relationDeclaration2Field = new HashMap
+        public val Map<RelationDefinition,ALSRelationDefinition> relationDefinition2Predicate = new HashMap
+        
+        public var Map<ConstantDeclaration, ConstantDefinition> constantDefinitions
+        public var Map<FunctionDeclaration, FunctionDefinition> functionDefinitions
+        public var Map<RelationDeclaration, RelationDefinition> relationDefinitions
+}
+\ No newline at end of file
diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_ConstantMapper.xtend b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_ConstantMapper.xtend
new file mode 100644
index 00000000..401c2ec2
--- /dev/null
+++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_ConstantMapper.xtend
@@ -0,0 +1,43 @@
+package hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder
+import hu.bme.mit.inf.dslreasoner.alloyLanguage.AlloyLanguageFactory
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ConstantDeclaration
+import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSMultiplicity
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ConstantDefinition
+import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*
+class Logic2AlloyLanguageMapper_ConstantMapper {
+        private val extension AlloyLanguageFactory factory = AlloyLanguageFactory.eINSTANCE
+        private val Logic2AlloyLanguageMapper_Support support = new Logic2AlloyLanguageMapper_Support;
+        val Logic2AlloyLanguageMapper base;
+        public new(Logic2AlloyLanguageMapper base) {
+                this.base = base
+        }
+        
+        def protected dispatch transformConstant(ConstantDeclaration constant, Logic2AlloyLanguageMapperTrace trace) {
+                if(!trace.constantDefinitions.containsKey(constant)) {
+                        val c = createALSFieldDeclaration=> [
+                                name = support.toID(constant.name)
+                                it.type = base.transformTypeReference(constant.type,trace)
+                                it.multiplicity = ALSMultiplicity.ONE
+                        ]
+                        trace.logicLanguageBody.fields+= c
+                        trace.constantDeclaration2LanguageField.put(constant,c)
+                }
+        }
+        
+        def protected dispatch transformConstant(ConstantDefinition constant, Logic2AlloyLanguageMapperTrace trace) {
+                val c = createALSFunctionDefinition=> [
+                        name = support.toID(constant.name)
+                        it.type = base.transformTypeReference(constant.type,trace)
+                        // the value is set later
+                ]
+                trace.specification.functionDefinitions += c
+                trace.constantDefinition2Function.put(constant,c)
+        }
+        
+        def protected transformConstantDefinitionSpecification(ConstantDefinition constant, Logic2AlloyLanguageMapperTrace trace) {
+                val definition = constant.lookup(trace.constantDefinition2Function)
+                definition.value = base.transformTerm(constant.value, trace,emptyMap)
+        }
+}
+\ No newline at end of file
diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_Containment.xtend b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_Containment.xtend
new file mode 100644
index 00000000..fd519c1e
--- /dev/null
+++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_Containment.xtend
@@ -0,0 +1,260 @@
+package hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder
+import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSMultiplicity
+import hu.bme.mit.inf.dslreasoner.alloyLanguage.AlloyLanguageFactory
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.LogiclanguageFactory
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration
+import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.ContainmentHierarchy
+import java.util.HashMap
+class Logic2AlloyLanguageMapper_Containment {
+        val extension AlloyLanguageFactory factory = AlloyLanguageFactory.eINSTANCE
+        private val Logic2AlloyLanguageMapper_Support support = new Logic2AlloyLanguageMapper_Support;
+        val Logic2AlloyLanguageMapper base;
+        public new(Logic2AlloyLanguageMapper base) {
+                this.base = base
+        }
+        
+        def protected transformContainmentHierarchy(ContainmentHierarchy containment, Logic2AlloyLanguageMapperTrace trace) {
+                // Single root
+                val rootField = createALSFieldDeclaration => [
+                        it.name= support.toID(#["util", "root"])
+                        it.multiplicity = ALSMultiplicity.ONE
+                        it.type = typesOrderedInContainment(containment,trace)
+                ]
+                trace.logicLanguageBody.fields += rootField
+                
+                val contains = createALSFieldDeclaration => [
+                        it.name = support.toID(#["util", "contains"])
+                        //it.multiplicity = ALSMultiplicity::SET
+                        it.type = createALSDirectProduct => [
+                                it.leftMultiplicit = ALSMultiplicity::LONE
+                                it.rightMultiplicit = ALSMultiplicity::SET
+                                it.leftOperand = typesOrderedInContainment(containment,trace)
+                                it.rightOperand = typesOrderedInContainment(containment,trace)
+                        ]
+                ]
+                trace.logicLanguageBody.fields += contains
+                
+                val containmentRelationDefinition = createALSFactDeclaration => [
+                        it.name = support.toID(#["util", "containmentDefinition"])              
+                ]
+                
+                if(containment.containmentRelations.forall[it instanceof RelationDeclaration]) {
+                        val containmentRelations = containment.containmentRelations.filter(RelationDeclaration).map[relation|
+                                base.relationMapper.transformRelationReference(relation,trace)
+                        ].toList
+                        
+                        containmentRelationDefinition.term = createALSEquals => [
+                                leftOperand = createALSJoin => [
+                                        leftOperand = createALSReference => [referred = trace.logicLanguage]
+                                        rightOperand = createALSReference => [ referred = contains ]]
+                                rightOperand = support.unfoldPlus(containmentRelations)
+                        ]
+                } else {
+                        val parent = createALSVariableDeclaration => [
+                                it.name = "parent"
+                                it.range = typesOrderedInContainment(containment, trace)
+                        ]
+                        val child = createALSVariableDeclaration => [
+                                it.name = "child"
+                                it.range = typesOrderedInContainment(containment, trace)
+                        ]
+                        
+                        val logicFactory = LogiclanguageFactory.eINSTANCE
+                        val logicParentVariable = logicFactory.createVariable
+                        val logicChildVariable = logicFactory.createVariable
+                        val logicParent = logicFactory.createSymbolicValue => [it.symbolicReference = logicParentVariable]
+                        val logicChild = logicFactory.createSymbolicValue => [it.symbolicReference = logicChildVariable]
+                        val variableMap = new HashMap => [put(logicParentVariable,parent) put(logicChildVariable,child)]
+                        val possibleRelations = containment.containmentRelations.map[relation |
+                                base.transformSymbolicReference(relation,#[logicParent,logicChild],trace,variableMap)
+                        ]
+                        
+                        containmentRelationDefinition.term = createALSQuantifiedEx => [
+                                it.type = ALSMultiplicity.ALL
+                                it.variables += parent
+                                it.variables += child
+                                it.expression = createALSIff => [
+                                        it.leftOperand = createALSSubset => [
+                                                it.leftOperand = createALSDirectProduct => [
+                                                        it.leftOperand = createALSReference => [it.referred = child]
+                                                        it.rightOperand = createALSReference => [it.referred = parent]
+                                                ]
+                                                it.rightOperand = createALSJoin => [
+                                                        leftOperand = createALSReference => [referred = trace.logicLanguage]
+                                                        rightOperand = createALSReference => [ referred = contains ]
+                                                ]
+                                        ]
+                                        it.rightOperand = support.unfoldOr(possibleRelations,trace)
+                                ]
+                        ]
+                }
+                
+                trace.specification.factDeclarations += containmentRelationDefinition
+                
+                // With the exception of the root, every object has at least one parent
+                // No parent for root
+                trace.specification.factDeclarations += createALSFactDeclaration => [
+                        it.name = support.toID(#["util", "noParentForRoot"])
+                        it.term = createALSQuantifiedEx => [
+                                it.type = ALSMultiplicity::NO
+                                val parent = createALSVariableDeclaration => [
+                                        it.name = "parent"
+                                        it.range = typesOrderedInContainment(containment,trace)
+                                ]
+                                it.variables += parent
+                                it.expression = createALSSubset => [
+                                        it.leftOperand = createALSDirectProduct => [
+                                                it.leftOperand = createALSReference => [it.referred = parent]
+                                                it.rightOperand = createALSJoin => [
+                                                        it.leftOperand = createALSReference => [it.referred = trace.logicLanguage]
+                                                        it.rightOperand = createALSReference => [it.referred = rootField]
+                                                ]
+                                        ]
+                                        it.rightOperand = createALSJoin => [
+                                                leftOperand = createALSReference => [referred = trace.logicLanguage]
+                                                rightOperand = createALSReference => [ referred = contains ]
+                                        ]
+                                ]
+                        ]
+                ]
+                // Parent for nonroot
+                trace.specification.factDeclarations += createALSFactDeclaration => [
+                        it.name = support.toID(#["util", "atLeastOneParent"])
+                        it.term = createALSQuantifiedEx => [
+                                it.type = ALSMultiplicity::ALL
+                                val child = createALSVariableDeclaration => [
+                                        it.name = "child"
+                                        it.range = typesOrderedInContainment(containment,trace)
+                                ]
+                                it.variables += child
+                                it.expression = createALSOr => [
+                                        it.leftOperand = createALSEquals => [
+                                                it.leftOperand = createALSReference => [it.referred = child]
+                                                it.rightOperand = createALSJoin => [
+                                                        it.leftOperand = createALSReference => [it.referred = trace.logicLanguage]
+                                                        it.rightOperand = createALSReference => [it.referred = rootField]
+                                                ]
+                                        ]
+                                        it.rightOperand = createALSQuantifiedEx => [
+                                                it.type = ALSMultiplicity::SOME
+                                                val parent = createALSVariableDeclaration => [
+                                                        it.name = "parent"
+                                                        it.range = typesOrderedInContainment(containment, trace)
+                                                ]
+                                                it.variables += parent
+                                                it.expression = createALSSubset => [
+                                                        it.leftOperand = createALSDirectProduct => [
+                                                                it.leftOperand = createALSReference => [it.referred = parent]
+                                                                it.rightOperand = createALSReference => [it.referred = child]
+                                                        ]
+                                                        it.rightOperand = createALSJoin => [
+                                                                leftOperand = createALSReference => [referred = trace.logicLanguage]
+                                                                rightOperand = createALSReference => [ referred = contains ]
+                                                        ]
+                                                ]
+                                        ]
+                                ]
+                        ]
+                ]
+                
+                // Every object has at most one parent
+//              trace.specification.factDeclarations += createALSFactDeclaration => [
+//                      it.name = support.toID(#["util", "atMostOneParent"])
+//                      it.term = createALSQuantifiedEx => [
+//                              it.type = ALSMultiplicity::ALL
+//                              val child = createALSVariableDeclaration => [
+//                                      it.name = "child"
+//                                      it.range = typesOrderedInContainment(containment,trace)
+//                              ]
+//                              it.variables += child
+//                              it.expression = createALSQuantifiedEx => [
+//                                      it.type = ALSMultiplicity::LONE
+//                                      val parent = createALSVariableDeclaration => [
+//                                              it.name = "parent"
+//                                              it.range = typesOrderedInContainment(containment, trace)
+//                                      ]
+//                                      it.variables += parent
+//                                      it.expression = createALSFunctionCall => [
+//                                              it.referredDefinition = containmentRelation
+//                                              it.params += createALSReference => [
+//                                                      it.referred = parent
+//                                                      it.referred = child
+//                                              ]
+//                                      ]
+//                              ]
+//                      ]
+//              ]
+                
+                // No circle in containment
+                trace.specification.factDeclarations += createALSFactDeclaration => [
+                        it.name = support.toID(#["util", "noCircularContainment"])
+                        it.term = createALSQuantifiedEx => [
+                                it.type = ALSMultiplicity::NO
+                                val variable = createALSVariableDeclaration => [
+                                        it.name = "circle"
+                                        it.range = typesOrderedInContainment(containment,trace)
+                                ]
+                                it.variables += variable
+                                it.expression = createALSSubset => [
+                                        it.leftOperand = createALSDirectProduct => [
+                                                it.leftOperand = createALSReference => [it.referred = variable]
+                                                it.rightOperand = createALSReference => [it.referred = variable]
+                                        ]
+                                        it.rightOperand = createAlSTransitiveClosure => [
+                                                it.operand = createALSJoin => [
+                                                        leftOperand = createALSReference => [referred = trace.logicLanguage]
+                                                        rightOperand = createALSReference => [ referred = contains ]
+                                                ]
+                                        ]
+                                ]
+                        ]
+                ]
+                
+        }
+        
+        /*def protected calculateContainmentTypeCoveringSignatures(ContainmentHierarchy containment, Logic2AlloyLanguageMapperTrace trace) {
+                val types = containment.typesOrderedInHierarchy
+                val signaturesInContainment = types.map[base.typeMapper.transformTypeReference(it, base, trace)].flatten.toList
+//              val uncoveredSignatures = new ArrayList(signaturesInContainment)
+//              val coveringSignatures = new LinkedList
+//              
+                val engine = ViatraQueryEngine.on(new EMFScope(trace.specification))
+                //val directSubsetMatcher = DirectSubsetMatcher.on(engine)
+                // x <= y
+                val subsetMatcher = SubsetMatcher.on(engine) 
+                
+                if()
+        }*/
+        
+        /*def boolean coveringAllSignaturesInContainment(ALSSignatureDeclaration target, List<ALSSignatureDeclaration> signaturesInContainment, SubsetMatcher matcher) {
+                for(signatureInContainment : signaturesInContainment) {
+                        if(!matcher.hasMatch(signatureInContainment,target)) {
+                                return false
+                        }
+                }
+                return true
+        }*/
+        
+        /*def boolean coveringSignatureNotInContainment(ALSSignatureDeclaration target, List<ALSSignatureDeclaration> signaturesInContainment, SubsetMatcher matcher) {
+                val subtypes = matcher.getAllValuesOfx(target);
+                for(subType : subtypes) {
+                        val isSubtypeOfASignatureInContainment = signaturesInContainment.exists[contained |
+                                matcher.hasMatch(subType,contained)
+                        ]
+                        if(!isSubtypeOfASignatureInContainment) {
+                                return false
+                        }
+                }
+                return true
+        }*/
+        
+        def protected typesOrderedInContainment(ContainmentHierarchy containment, Logic2AlloyLanguageMapperTrace trace) {
+                val types = containment.typesOrderedInHierarchy
+                val signaturesInContainment = types.map[base.typeMapper.transformTypeReference(it, base, trace)].flatten
+                // val allSignatures = trace.specification.signatureBodies.map[declarations].flatten
+                val typeReferences = signaturesInContainment.map[sig | createALSReference => [it.referred = sig]].toList
+                return support.unfoldPlus(typeReferences)
+        }
+}
+\ No newline at end of file
diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_FunctionMapper.xtend b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_FunctionMapper.xtend
new file mode 100644
index 00000000..ff18ef80
--- /dev/null
+++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_FunctionMapper.xtend
@@ -0,0 +1,87 @@
+package hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder
+import hu.bme.mit.inf.dslreasoner.alloyLanguage.AlloyLanguageFactory
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.FunctionDeclaration
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference
+import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSMultiplicity
+import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSSignatureBody
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.FunctionDefinition
+import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*
+import java.util.HashMap
+class Logic2AlloyLanguageMapper_FunctionMapper {
+        private val extension AlloyLanguageFactory factory = AlloyLanguageFactory.eINSTANCE
+        private val Logic2AlloyLanguageMapper_Support support = new Logic2AlloyLanguageMapper_Support;
+        val Logic2AlloyLanguageMapper base;
+        public new(Logic2AlloyLanguageMapper base) {
+                this.base = base
+        }
+        
+        def protected dispatch transformFunction(FunctionDeclaration f, Logic2AlloyLanguageMapperTrace trace) {
+                if(!trace.constantDefinitions.containsKey(f)) {
+                        if(transformedToHostedField(f,trace)) transformFunctionToFieldOfSignature(f,trace)
+                        else transformFunctionToGlobalRelation(f,trace)
+                }
+        }
+        
+        def protected transformedToHostedField(FunctionDeclaration f, Logic2AlloyLanguageMapperTrace trace) {
+                if(f.parameters.size == 1 && f.parameters.head instanceof ComplexTypeReference) {
+                        val head = f.parameters.head
+                        if(head instanceof ComplexTypeReference) {
+                                val types = base.typeMapper.transformTypeReference(head.referred,base,trace)
+                                return types.size == 1
+                        }
+                }
+                return (f.parameters.size == 1 && f.parameters.head instanceof ComplexTypeReference)
+        }
+        def protected transformFunctionToFieldOfSignature(FunctionDeclaration f,Logic2AlloyLanguageMapperTrace trace) {
+                val param = (f.parameters.head as ComplexTypeReference)
+                val referred = param.referred
+                val field = createALSFieldDeclaration => [
+                        it.name = support.toID(f.getName)
+                        it.multiplicity = ALSMultiplicity.ONE
+                        it.type = base.transformTypeReference(f.range,trace)
+                ]
+                val host = base.typeMapper.transformTypeReference(referred,base,trace).get(0)
+                (host.eContainer as ALSSignatureBody).fields += field
+                trace.functionDeclaration2HostedField.put(f, field)
+        }
+        def protected transformFunctionToGlobalRelation(FunctionDeclaration f, Logic2AlloyLanguageMapperTrace trace) {
+                val field = createALSFieldDeclaration => [
+                        it.name = support.toID(f.name)
+                        it.multiplicity = ALSMultiplicity.SET
+                        it.type = createALSDirectProduct => [
+                                it.leftOperand = support.unfoldReferenceDirectProduct(base,f.parameters,trace)
+                                it.rightMultiplicit = ALSMultiplicity.ONE
+                                it.rightOperand = base.transformTypeReference(f.range,trace)
+                        ]
+                ]
+                trace.logicLanguageBody.fields += field
+                trace.functionDeclaration2LanguageField.put(f, field)
+        }
+        
+        def protected dispatch transformFunction(FunctionDefinition f, Logic2AlloyLanguageMapperTrace trace) {
+                val res = createALSFunctionDefinition => [
+                        name = support.toID(f.name)
+                        // variables + specification later
+                ]
+                trace.specification.functionDefinitions+=res;
+                trace.functionDefinition2Function.put(f,res)
+        }
+        
+        def protected transformFunctionDefinitionSpecification(FunctionDefinition f, Logic2AlloyLanguageMapperTrace trace) {
+                val target = f.lookup(trace.functionDefinition2Function)
+                val variableMap = new HashMap
+                for(variable : f.variable) {
+                        val v = createALSVariableDeclaration => [
+                                it.name = support.toID(variable.name)
+                                it.range = base.transformTypeReference(variable.range,trace)
+                                // specification later
+                        ]
+                        target.variables+=v
+                        variableMap.put(variable,v)
+                }
+                target.value = base.transformTerm(f.value,trace,variableMap)
+        }
+        
+}
+\ No newline at end of file
diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_RelationMapper.xtend b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_RelationMapper.xtend
new file mode 100644
index 00000000..9dd4da2f
--- /dev/null
+++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_RelationMapper.xtend
@@ -0,0 +1,111 @@
+package hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder
+import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSMultiplicity
+import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSSignatureBody
+import hu.bme.mit.inf.dslreasoner.alloyLanguage.AlloyLanguageFactory
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition
+import java.util.HashMap
+import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*
+class Logic2AlloyLanguageMapper_RelationMapper {        
+        private val extension AlloyLanguageFactory factory = AlloyLanguageFactory.eINSTANCE
+        private val Logic2AlloyLanguageMapper_Support support = new Logic2AlloyLanguageMapper_Support;
+        val Logic2AlloyLanguageMapper base;
+        public new(Logic2AlloyLanguageMapper base) {
+                this.base = base
+        }
+                
+        def dispatch protected void  transformRelation(RelationDeclaration r, Logic2AlloyLanguageMapperTrace trace) {
+                if(!trace.relationDefinitions.containsKey(r)) {
+                        if(r.transformToHostedField(trace)) {
+                                transformRelationDeclarationToHostedField(r,trace)
+                        } else {
+                                transformRelationDeclarationToGlobalField(r,trace)
+                        }
+                }
+        }
+        
+        def protected transformToHostedField(RelationDeclaration r, Logic2AlloyLanguageMapperTrace trace) {
+                val first = r.parameters.get(0)
+                if(r.parameters.size == 2) {
+                        if(first instanceof ComplexTypeReference) {
+                                val types = base.typeMapper.transformTypeReference(first.referred,base,trace)
+                                if(types.size == 1) {
+                                        return true
+                                }
+                        }
+                }
+                return false
+        }
+        
+        def protected transformRelationDeclarationToHostedField(RelationDeclaration r, Logic2AlloyLanguageMapperTrace trace) {
+                val hostType = (r.parameters.head as ComplexTypeReference).referred
+                
+                val targetBody = base.typeMapper.transformTypeReference(hostType,base,trace).get(0).eContainer as ALSSignatureBody
+                val field = createALSFieldDeclaration => [
+                        it.name = support.toID(r.getName)
+                        it.multiplicity = ALSMultiplicity.SET
+                        it.type = base.transformTypeReference(r.parameters.get(1),trace)
+                ]
+                targetBody.fields += field
+                trace.relationDeclaration2Field.put(r,field)
+                
+        }
+        
+        def protected transformRelationDeclarationToGlobalField(RelationDeclaration r, Logic2AlloyLanguageMapperTrace trace) {
+                val field = createALSFieldDeclaration => [
+                        it.name = support.toID(r.name)
+                        it.type = support.unfoldReferenceDirectProduct(base,r.parameters,trace)
+                ]
+                trace.logicLanguageBody.fields += field
+                trace.relationDeclaration2Global.put(r, field)
+        }
+        def dispatch protected void transformRelation(RelationDefinition r, Logic2AlloyLanguageMapperTrace trace) {
+                val res = createALSRelationDefinition => [
+                        name = support.toID(r.name)
+                        // fill the variables later
+                        // fill the expression later
+                ]
+                
+                trace.relationDefinition2Predicate.put(r,res)
+                trace.specification.relationDefinitions+=res;
+        }
+        
+        def protected void transformRelationDefinitionSpecification(RelationDefinition r, Logic2AlloyLanguageMapperTrace trace) {
+                val predicate = r.lookup(trace.relationDefinition2Predicate)
+                if(predicate !== null) {
+                        val variableMap = new HashMap
+                        for(variable : r.variables) {
+                                val v = createALSVariableDeclaration => [
+                                        it.name = support.toID(variable.name)
+                                        it.range = base.transformTypeReference(variable.range,trace)
+                                ]
+                                predicate.variables+=v
+                                variableMap.put(variable,v)
+                        }
+                        predicate.value = base.transformTerm(r.value,trace,variableMap)
+                }
+        }
+        
+        def public transformRelationReference(RelationDeclaration relation, Logic2AlloyLanguageMapperTrace trace) {
+                if(relation.transformToHostedField(trace)) {
+                        return createALSReference => [it.referred = relation.lookup(trace.relationDeclaration2Field) ]
+                } else {
+                        return createALSJoin => [
+                                leftOperand = createALSReference => [referred = trace.logicLanguage]
+                                rightOperand = createALSReference => [ referred = relation.lookup(trace.relationDeclaration2Global) ]]
+                }
+        }
+        
+        def public getRelationReference(RelationDeclaration relation, Logic2AlloyLanguageMapperTrace trace) {
+                if(relation.transformToHostedField(trace)) {
+                        return relation.lookup(trace.relationDeclaration2Field)
+                } else {
+                        return relation.lookup(trace.relationDeclaration2Global)
+                }
+        }
+}
+\ No newline at end of file
diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_Support.xtend b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_Support.xtend
new file mode 100644
index 00000000..39896c27
--- /dev/null
+++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_Support.xtend
@@ -0,0 +1,207 @@
+package hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder
+import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSEquals
+import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSMultiplicity
+import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSReference
+import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSTerm
+import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSVariableDeclaration
+import hu.bme.mit.inf.dslreasoner.alloyLanguage.AlloyLanguageFactory
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.BoolTypeReference
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.QuantifiedExpression
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Term
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeReference
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable
+import java.util.ArrayList
+import java.util.HashMap
+import java.util.List
+import java.util.Map
+import org.eclipse.emf.ecore.util.EcoreUtil
+class Logic2AlloyLanguageMapper_Support {
+        private val extension AlloyLanguageFactory factory = AlloyLanguageFactory.eINSTANCE
+        
+        /// ID handling
+        def protected String toIDMultiple(String... ids) {
+                ids.map[it.split("\\s+").join("'")].join("'")
+        }
+        
+        def protected  String toID(String ids) {
+                ids.split("\\s+").join("'")
+        }
+        def protected  String toID(List<String> ids) {
+                ids.map[it.split("\\s+").join("'")].join("'")
+        }
+        
+        /// Support functions
+        
+        def protected getBooleanType(Logic2AlloyLanguageMapperTrace trace) {
+                if(trace.boolType!=null) {
+                        return trace.boolType
+                } else {
+                        trace.boolType = createALSEnumDeclaration => [
+                                it.name = toID(#["util","boolean"])
+                                trace.boolTrue = createALSEnumLiteral =>[it.name=toID(#["util","boolean","true"])]
+                                it.literal += trace.boolTrue
+                                trace.boolFalse = createALSEnumLiteral =>[it.name=toID(#["util","boolean","false"])]
+                                it.literal += trace.boolFalse
+                        ]
+                        trace.specification.enumDeclarations+=trace.boolType
+                        return trace.boolType
+                }
+        }
+        def protected getBooleanTrue(Logic2AlloyLanguageMapperTrace trace) {
+                getBooleanType(trace)
+                return trace.boolTrue   
+        }
+        def protected getBooleanFalse(Logic2AlloyLanguageMapperTrace trace) {
+                getBooleanType(trace)
+                return trace.boolFalse
+        }
+        
+        def protected booleanToLogicValue(ALSTerm boolReference, Logic2AlloyLanguageMapperTrace trace) {
+                //println((boolReference as ALSReference).referred)
+                createALSEquals => [
+                        leftOperand = EcoreUtil.copy(boolReference)
+                        rightOperand = createALSReference => [referred = getBooleanTrue(trace)]
+                ]
+        }
+        def protected booleanToEnumValue(ALSTerm value, Logic2AlloyLanguageMapperTrace trace) {
+                if(value instanceof ALSEquals) {
+                        val rightOperand = value.rightOperand
+                        if(rightOperand instanceof ALSReference) {
+                                if(rightOperand.referred == getBooleanTrue(trace)) {
+                                        return value.leftOperand
+                                }
+                        }
+                }
+                return value;
+        }
+        def protected prepareParameterOfSymbolicReference(TypeReference type, ALSTerm term, Logic2AlloyLanguageMapperTrace trace) {
+                if(type instanceof BoolTypeReference) {
+                        return booleanToEnumValue(term,trace)
+                }
+                else return term
+        }
+        def protected postprocessResultOfSymbolicReference(TypeReference type, ALSTerm term, Logic2AlloyLanguageMapperTrace trace) {
+                if(type instanceof BoolTypeReference) {
+                        return booleanToLogicValue(term,trace)
+                }
+                else return term
+        }
+         
+        def protected ALSTerm unfoldAnd(List<? extends ALSTerm> operands) {
+                if(operands.size == 1) { return operands.head }
+                else if(operands.size > 1) { return createALSAnd=>[
+                        leftOperand=operands.head
+                        rightOperand=operands.subList(1,operands.size).unfoldAnd
+                ]}
+                else throw new UnsupportedOperationException('''Logic operator with 0 operands!''')
+        }
+        
+        def protected ALSTerm unfoldOr(List<? extends ALSTerm> operands, Logic2AlloyLanguageMapperTrace trace) {
+                if(operands.size == 0) { return unfoldTrueStatement(trace)}
+                else if(operands.size == 1) { return operands.head }
+                else if(operands.size > 1) { return createALSOr=>[
+                        leftOperand=operands.head
+                        rightOperand=unfoldOr(operands.subList(1,operands.size),trace)
+                ]}
+                //else throw new UnsupportedOperationException('''Logic operator with 0 operands!''')
+        }
+        
+        protected def unfoldTrueStatement(Logic2AlloyLanguageMapperTrace trace) {
+                createALSEquals => [
+                                it.leftOperand = createALSReference => [it.referred = getBooleanTrue(trace)]
+                                it.rightOperand = createALSReference => [it.referred = getBooleanTrue(trace)]
+                        ]
+        }
+        
+        protected def unfoldTFalseStatement(Logic2AlloyLanguageMapper m, Logic2AlloyLanguageMapperTrace trace) {
+                createALSEquals => [
+                                it.leftOperand = createALSReference => [it.referred = getBooleanTrue(trace)]
+                                it.rightOperand = createALSReference => [it.referred = getBooleanTrue(trace)]
+                        ]
+        }
+        
+        def protected ALSTerm unfoldPlus(List<? extends ALSTerm> operands) {
+                if(operands.size == 1) { return operands.head }
+                else if(operands.size > 1) { return createALSPlus=>[
+                        leftOperand=operands.head
+                        rightOperand=operands.subList(1,operands.size).unfoldPlus
+                ]}
+                else return createALSNone
+        }
+        
+        def protected ALSTerm unfoldIntersection(List<? extends ALSTerm> operands) {
+                if(operands.size == 1) { return operands.head }
+                else if(operands.size > 1) { return createALSIntersection=>[
+                        leftOperand=operands.head
+                        rightOperand=operands.subList(1,operands.size).unfoldIntersection
+                ]}
+                else throw new UnsupportedOperationException('''Logic operator with 0 operands!''')
+        }
+        
+        def protected ALSTerm unfoldDistinctTerms(Logic2AlloyLanguageMapper m, List<Term> operands, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) {
+                if(operands.size == 1) { return m.transformTerm(operands.head,trace,variables) }
+                else if(operands.size > 1) {
+                        val notEquals = new ArrayList<ALSTerm>(operands.size*operands.size/2)
+                        for(i:0..<operands.size) {
+                                for(j: i+1..<operands.size) {
+                                        notEquals+=createALSNotEquals=>[
+                                                leftOperand = m.transformTerm(operands.get(i),trace,variables)
+                                                rightOperand = m.transformTerm(operands.get(j),trace,variables)
+                                        ]
+                                }
+                        }
+                        return notEquals.unfoldAnd
+                 }
+                else throw new UnsupportedOperationException('''Logic operator with 0 operands!''')
+        }
+        
+        def protected ALSTerm unfoldReferenceDirectProduct(Logic2AlloyLanguageMapper m, List<TypeReference> references,Logic2AlloyLanguageMapperTrace trace) {
+                if(references.size == 1) return m.transformTypeReference(references.head,trace)
+                else if(references.size > 1) return createALSDirectProduct => [
+                        it.leftOperand = m.transformTypeReference(references.head,trace)
+                        it.rightOperand = unfoldReferenceDirectProduct(m,references.subList(1,references.size),trace)
+                ]
+                else throw new UnsupportedOperationException
+        }
+        
+        def protected ALSTerm unfoldDotJoin(Logic2AlloyLanguageMapper m, List<Term> elements, ALSTerm target, Logic2AlloyLanguageMapperTrace trace,
+                Map<Variable, ALSVariableDeclaration> variables) {
+                if (elements.size == 1) {
+                        return createALSJoin => [
+                                it.leftOperand = m.transformTerm(elements.head,trace, variables)
+                                it.rightOperand = target
+                        ]
+                } else if (elements.size > 1) {
+                        return createALSJoin => [
+                                it.leftOperand = m.transformTerm(elements.last,trace, variables)
+                                it.rightOperand = m.unfoldDotJoin(elements.subList(0, elements.size - 1), target, trace, variables)
+                        ]
+                } else
+                        throw new UnsupportedOperationException
+        }
+        
+        def protected ALSTerm unfoldTermDirectProduct(Logic2AlloyLanguageMapper m, List<Term> references,Logic2AlloyLanguageMapperTrace trace,Map<Variable, ALSVariableDeclaration> variables) {
+                if(references.size == 1) return m.transformTerm(references.head,trace,variables)
+                else if(references.size > 1) return createALSDirectProduct => [
+                        it.leftOperand = m.transformTerm(references.head,trace,variables)
+                        it.rightOperand = unfoldTermDirectProduct(m,references.subList(1,references.size),trace, variables)
+                ]
+                else throw new UnsupportedOperationException
+        }
+        
+        def protected createQuantifiedExpression(Logic2AlloyLanguageMapper m, QuantifiedExpression q, ALSMultiplicity multiplicity, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) {
+                val variableMap = q.quantifiedVariables.toInvertedMap[v | createALSVariableDeclaration=> [
+                                it.name = toID(v.name)
+                                it.range = m.transformTypeReference(v.range,trace) ]]
+                        
+                createALSQuantifiedEx=>[
+                        it.type = multiplicity
+                        it.variables += variableMap.values
+                        it.expression = m.transformTerm(q.expression,trace,variables.withAddition(variableMap))
+                ]
+        }
+        
+        def protected withAddition(Map<Variable, ALSVariableDeclaration> v1, Map<Variable, ALSVariableDeclaration> v2) { new HashMap(v1) => [putAll(v2)] }
+}
+\ No newline at end of file
diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapper.xtend b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapper.xtend
new file mode 100644
index 00000000..9927f1cc
--- /dev/null
+++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapper.xtend
@@ -0,0 +1,16 @@
+package hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder
+import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSSignatureDeclaration
+import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSTerm
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type
+import java.util.Collection
+import java.util.List
+interface Logic2AlloyLanguageMapper_TypeMapper {
+        def void transformTypes(Collection<Type> types, Collection<DefinedElement> elements, Logic2AlloyLanguageMapper mapper, Logic2AlloyLanguageMapperTrace trace);
+        def List<ALSSignatureDeclaration> transformTypeReference(Type referred, Logic2AlloyLanguageMapper mapper, Logic2AlloyLanguageMapperTrace trace)
+        def ALSSignatureDeclaration getUndefinedSupertype(Logic2AlloyLanguageMapperTrace trace)
+        def int getUndefinedSupertypeScope(int undefinedScope,Logic2AlloyLanguageMapperTrace trace)
+        def ALSTerm transformReference(DefinedElement referred,Logic2AlloyLanguageMapperTrace trace)
+}
diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapper_FilteredTypes.xtend b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapper_FilteredTypes.xtend
new file mode 100644
index 00000000..ade9860b
--- /dev/null
+++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapper_FilteredTypes.xtend
@@ -0,0 +1,268 @@
+package hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder
+import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.queries.TypeQueries
+import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSMultiplicity
+import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSSignatureBody
+import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSSignatureDeclaration
+import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSTerm
+import hu.bme.mit.inf.dslreasoner.alloyLanguage.AlloyLanguageFactory
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition
+import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicproblemPackage
+import java.util.ArrayList
+import java.util.Collection
+import java.util.HashMap
+import java.util.List
+import java.util.Map
+import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*
+class Logic2AlloyLanguageMapper_TypeMapperTrace_FilteredTypes
+        implements Logic2AlloyLanguageMapper_TypeMapperTrace
+{
+        public var ALSSignatureDeclaration objectSupperClass;
+        public val Map<Type, ALSSignatureDeclaration> type2ALSType = new HashMap;
+        public val Map<DefinedElement, ALSSignatureDeclaration> definedElement2Declaration = new HashMap
+}
+/**
+ * Each object is an element of an Object set, and types are subsets of the objects.
+ */
+class Logic2AlloyLanguageMapper_TypeMapper_FilteredTypes implements Logic2AlloyLanguageMapper_TypeMapper{
+        private val Logic2AlloyLanguageMapper_Support support = new Logic2AlloyLanguageMapper_Support;
+        private val extension AlloyLanguageFactory factory = AlloyLanguageFactory.eINSTANCE
+        
+        new() {
+                // Initialize package
+                LogicproblemPackage.eINSTANCE.class
+        }
+        
+        override transformTypes(Collection<Type> types, Collection<DefinedElement> elements, Logic2AlloyLanguageMapper mapper, Logic2AlloyLanguageMapperTrace trace) {
+                val typeTrace = new Logic2AlloyLanguageMapper_TypeMapperTrace_FilteredTypes
+                trace.typeMapperTrace = typeTrace
+                
+                // 1. A global type for Objects is created
+                val objectSig = createALSSignatureDeclaration => [it.name = support.toID(#["util","Object"])]
+                val objectBody = createALSSignatureBody => [
+                        it.declarations += objectSig
+                        it.abstract = true
+                ]
+                typeTrace.objectSupperClass = objectSig
+                trace.specification.signatureBodies += objectBody
+                
+                // 2. Each type is mapped to a unique sig
+                for(type : types) {
+                        val sig = createALSSignatureDeclaration => [it.name = support.toIDMultiple("type",type.name)]
+                        val body = createALSSignatureBody => [it.declarations += sig]
+                        trace.specification.signatureBodies += body
+                        typeTrace.type2ALSType.put(type,sig)
+                }
+                
+                // 3. The elements of a defined type is mapped to singleton signatures
+                // 3.1 Collect the elements
+                val elementMatcher = TypeQueries.instance.getLowestCommonSupertypeOfAllOccuranceOfElement(trace.incqueryEngine)
+                val topmostType2Elements = new HashMap<ALSSignatureDeclaration,List<DefinedElement>>
+                for(element : elements) {
+                        val topmostTypes = elementMatcher.getAllValuesOftype(element)
+                        var ALSSignatureDeclaration selectedTopmostType;
+                        if(topmostTypes.empty) {
+                                selectedTopmostType = objectSig
+                        } else{
+                                selectedTopmostType = topmostTypes.head.lookup(typeTrace.type2ALSType)
+                        }
+                        topmostType2Elements.putOrAddToList(selectedTopmostType,element)
+                }
+                
+                // 4. For each topmost types several singleton classes are generated, which represents the elements.
+                // For the sake of clarity, common bodies are used.
+                for(topmostEntry : topmostType2Elements.entrySet) {
+                        
+                        for(element : topmostEntry.value) {
+                                val signature = createALSSignatureDeclaration => [it.name = support.toIDMultiple("element",element.name)]
+                                typeTrace.definedElement2Declaration.put(element,signature)
+                        }
+                        
+                        val body = createALSSignatureBody => [
+                                it.multiplicity = ALSMultiplicity.ONE
+                                it.declarations += topmostEntry.value.map[it.lookup(typeTrace.definedElement2Declaration)]
+                        ]
+                        
+                        val containerLogicType = topmostEntry.key
+                        body.superset += containerLogicType
+                        
+                        trace.specification.signatureBodies+=body
+                }
+                
+                // 5.1 Each Defined Type is specified as the union of its elements
+                for(definedType : types.filter(TypeDefinition)) {
+                        trace.specification.factDeclarations += createALSFactDeclaration => [
+                                it.name = support.toIDMultiple("typedefinition",definedType.name)
+                                it.term = createALSEquals => [
+                                        it.leftOperand = createALSReference => [ it.referred = definedType.lookup(typeTrace.type2ALSType) ]
+                                        it.rightOperand = support.unfoldPlus(definedType.elements.map[e|
+                                                createALSReference => [it.referred = e.lookup(typeTrace.definedElement2Declaration)]])
+                                ]
+                        ]
+                }
+                // 5.2 Each Defined Element is unique
+                for(definedType : types.filter(TypeDefinition)) {
+                        val allElementsIncludingSubtypes = 
+                                definedType.<Type>transitiveClosureStar[it.subtypes].filter(TypeDefinition)
+                                        .map[elements].flatten.toSet.toList
+                        if(allElementsIncludingSubtypes.size>=2) {
+                                trace.specification.factDeclarations += createALSFactDeclaration => [
+                                        it.name = support.toIDMultiple("typeElementsUnique",definedType.name)
+                                        it.term = unfoldDistinctElements(allElementsIncludingSubtypes,trace)
+                                ]
+                        }
+                }
+                
+                // 6. Each inheritance is modeled by subset operator 'in'
+                for(type : types) {
+                        val sigBody = type.lookup(typeTrace.type2ALSType).eContainer as ALSSignatureBody
+                        if(type.supertypes.empty)  {
+                                sigBody.superset += typeTrace.objectSupperClass
+                        } else {
+                                sigBody.superset += type.supertypes.map[lookup(typeTrace.type2ALSType)]
+                        }
+                }
+                
+                
+                // 7. Each type is in the intersection of the supertypes
+                for(type : types.filter[it.supertypes.size>=2]) {
+                        trace.specification.factDeclarations += createALSFactDeclaration => [
+                                it.name = support.toIDMultiple("abstract",type.name)
+                                it.term = createALSEquals => [
+                                        it.leftOperand = createALSReference => [ it.referred = type.lookup(typeTrace.type2ALSType) ]
+                                        it.rightOperand = support.unfoldIntersection(type.supertypes.map[e|
+                                                createALSReference => [it.referred = e.lookup(typeTrace.type2ALSType)]])
+                                ]
+                        ]
+                }
+                
+                // 8. Each abstract type is equal to the union of the subtypes
+                for(type : types.filter[isIsAbstract]) {
+                        trace.specification.factDeclarations += createALSFactDeclaration => [
+                                it.name = support.toIDMultiple("abstract",type.name)
+                                it.term = createALSEquals => [
+                                        it.leftOperand = createALSReference => [ it.referred = type.lookup(typeTrace.type2ALSType) ]
+                                        it.rightOperand = support.unfoldPlus(type.subtypes.map[e|
+                                                createALSReference => [it.referred = e.lookup(typeTrace.type2ALSType)]])
+                                ]
+                        ]
+                }
+                // 8.1 The object type is the union of the root types.
+                val rootTypes = types.filter[it.supertypes.empty].toList
+                trace.specification.factDeclarations += createALSFactDeclaration => [
+                        it.name = support.toIDMultiple(#["ObjectTypeDefinition"])
+                        it.term = createALSEquals => [
+                                it.leftOperand = createALSReference => [ it.referred = typeTrace.objectSupperClass ]
+                                it.rightOperand = support.unfoldPlus(rootTypes.map[e|
+                                        createALSReference => [it.referred = e.lookup(typeTrace.type2ALSType)]])
+                        ]
+                ]
+                
+                // 9. For each type X (including Object)
+                //    only the common subtypes are in the intersection
+                //    of the two subtype.
+                // 9.1. for the object
+                {
+                        val rootTypeList = types.filter[it.supertypes.empty].toList
+                        for(type1Index: 0..<rootTypeList.size) {
+                                for(type2Index: 0..<type1Index) {
+                                        trace.specification.factDeclarations += 
+                                                commonSubtypeOnlyInDiamonds(rootTypeList.get(type1Index),rootTypeList.get(type2Index),trace)
+                                }
+                        }
+                }
+                
+                //9.3 for the subtypes of each objects
+                {
+                        for(inScope : types) {
+                                val subtypeList = inScope.subtypes//.toList
+                                if(subtypeList.size>=2) {
+                                        for(type1Index: 0..<subtypeList.size) {
+                                                for(type2Index: 0..<type1Index) {
+                                                        trace.specification.factDeclarations += 
+                                                                commonSubtypeOnlyInDiamonds(subtypeList.get(type1Index),subtypeList.get(type2Index),trace)
+                                                }
+                                        }
+                                }
+                        }
+                }
+        }
+        
+        private def isEnumlikeType(Type type) {
+                if(type instanceof TypeDefinition) {
+                        val elements = type.elements
+                        return elements.forall[it.definedInType.size === 1 && it.definedInType.head === type]
+                }
+                return false
+        }
+        
+        private def isEnumlikeElement(DefinedElement d) {
+                d.definedInType.size === 1 && d.definedInType.head.isEnumlikeType 
+        }
+        
+        def getTypeTrace(Logic2AlloyLanguageMapperTrace trace) {
+                val res = trace.typeMapperTrace
+                if(res instanceof Logic2AlloyLanguageMapper_TypeMapperTrace_FilteredTypes) {
+                        return res
+                } else {
+                        throw new IllegalArgumentException('''
+                        Expected type mapping trace: «Logic2AlloyLanguageMapper_TypeMapperTrace_FilteredTypes.name»,
+                        but found «res.class.name»''')
+                }
+        }
+        
+        def private commonSubtypeOnlyInDiamonds(Type t1, Type t2, Logic2AlloyLanguageMapperTrace trace) {
+                val topmostCommonSubtypes = TypeQueries.instance.getTopmostCommonSubtypes(trace.incqueryEngine)
+                val allTopmostCommon = topmostCommonSubtypes.getAllValuesOfcommon(t1,t2).toList
+                return createALSFactDeclaration => [
+                                it.name = support.toIDMultiple("common","types",t1.name,t2.name)
+                                it.term = createALSEquals => [
+                                        it.leftOperand = createALSIntersection => [
+                                                it.leftOperand = createALSReference => [it.referred = t1.lookup(trace.typeTrace.type2ALSType)]
+                                                it.rightOperand = createALSReference => [it.referred = t2.lookup(trace.typeTrace.type2ALSType)]
+                                        ]
+                                        it.rightOperand = support.unfoldPlus(allTopmostCommon.map[t|createALSReference => [it.referred = t.lookup(trace.typeTrace.type2ALSType)]])
+                                ]
+                        ]
+        }
+        
+        def private unfoldDistinctElements(
+                List<DefinedElement> operands,
+                Logic2AlloyLanguageMapperTrace trace
+        ) {
+                if(operands.size == 1 || operands.size == 0) {support.unfoldTrueStatement(trace);}
+                else {
+                        val notEquals = new ArrayList<ALSTerm>(operands.size*operands.size/2)
+                        for(i:0..<operands.size) {
+                                for(j: i+1..<operands.size) {
+                                        notEquals+=createALSNotEquals=>[
+                                                leftOperand = createALSReference => [it.referred = trace.typeTrace.definedElement2Declaration.get(operands.get(i)) ]
+                                                rightOperand = createALSReference => [it.referred = trace.typeTrace.definedElement2Declaration.get(operands.get(j)) ]
+                                        ]
+                                }
+                        }
+                        return support.unfoldAnd(notEquals)
+                }
+        }
+        
+        override transformTypeReference(Type referred, Logic2AlloyLanguageMapper mapper, Logic2AlloyLanguageMapperTrace trace) {
+                return #[trace.typeTrace.type2ALSType.get(referred)]
+        }
+        
+        override getUndefinedSupertype(Logic2AlloyLanguageMapperTrace trace) {
+                trace.typeTrace.objectSupperClass
+        }
+        
+        override transformReference(DefinedElement referred, Logic2AlloyLanguageMapperTrace trace) {
+                createALSReference => [it.referred = referred.lookup(trace.typeTrace.definedElement2Declaration)]
+        }
+        
+        override getUndefinedSupertypeScope(int undefinedScope, Logic2AlloyLanguageMapperTrace trace) {
+                return undefinedScope + trace.typeTrace.definedElement2Declaration.size
+        }
+        
+}
+\ No newline at end of file
diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapper_Horizontal.xtend_old b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapper_Horizontal.xtend_old
new file mode 100644
index 00000000..7383904d
--- /dev/null
+++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapper_Horizontal.xtend_old
@@ -0,0 +1,428 @@
+package hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder
+import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSIntersection
+import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSMultiplicity
+import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSSignatureDeclaration
+import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSTerm
+import hu.bme.mit.inf.dslreasoner.alloyLanguage.AlloyLanguageFactory
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDeclaration
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition
+import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem
+import hu.bme.mit.inf.dslreasoner.logic.model.patterns.SupertypeStarMatcher
+import java.util.HashMap
+import java.util.LinkedHashSet
+import java.util.LinkedList
+import java.util.List
+import java.util.Map
+import org.eclipse.viatra.query.runtime.api.ViatraQueryEngine
+import org.eclipse.viatra.query.runtime.emf.EMFScope
+import org.eclipse.xtend.lib.annotations.Data
+import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*
+class Logic2AlloyLanguageMapper_TypeMapperTrace_Horizontal
+        implements Logic2AlloyLanguageMapper_TypeMapperTrace {
+        public var ALSSignatureDeclaration declaredSupertype
+        public var ALSSignatureDeclaration definedSupertype
+        public val Map<DefinedElement, ALSSignatureDeclaration> definedElement2Declaration = new HashMap
+        
+        public val Map<TypeDefinition,  ALSSignatureDeclaration> definition2definition = new HashMap
+        public val Map<TypeDeclaration, ALSSignatureDeclaration> declaration2definition = new HashMap
+        public val Map<TypeDeclaration, ALSSignatureDeclaration> undefined2definition = new HashMap
+        public val Map<TypeDeclaration, ALSSignatureDeclaration> new2declaration = new HashMap
+        
+        def getAllDefinedTypes() {
+                return (definition2definition.values) +
+                       (declaration2definition.values) +
+                       (undefined2definition.values)
+        }
+        def getAllDeclaredTypes() {
+                return new2declaration.values
+        }
+        
+        public val Map<Type,List<ALSSignatureDeclaration>> type2AllSignatures = new HashMap;
+}
+@Data
+class DynamicTypeConstraints {
+        List<List<Type>> positiveCNF
+        LinkedHashSet<Type> negative
+        public new() {
+                this.positiveCNF = new LinkedList
+                this.negative = new LinkedHashSet
+        }
+        def public void addPositiveTypeOptions(List<Type> typeDisjunction) {
+                this.positiveCNF.add(typeDisjunction)
+        }
+        def public void addNegativeTypes(Iterable<Type> negativeTypes) {
+                this.negative.addAll(negativeTypes)
+        }
+}
+/**
+ * Dynamic types are represented by disjoint sets, and 
+ * static types are represented by the union of the dynamic type sets.
+ * 
+ * Definition                         Declaration
+ *     |                              /         \
+ *     |                  W/DefinedSuper       Wo/DefinedSuper
+ *     |                     |                  /           \
+ *     |                     |      undefined2declaration  new2declaration
+ * definition2definition  definition2declaration
+ * +----------------------------------------------------+  +-------------+
+ *        Defined                                              Declared
+ */
+class Logic2AlloyLanguageMapper_TypeMapper_Horizontal implements Logic2AlloyLanguageMapper_TypeMapper{
+        private val Logic2AlloyLanguageMapper_Support support = new Logic2AlloyLanguageMapper_Support;
+        private val extension AlloyLanguageFactory factory = AlloyLanguageFactory.eINSTANCE
+        
+        override transformTypes(LogicProblem problem, Logic2AlloyLanguageMapper mapper, Logic2AlloyLanguageMapperTrace trace) {
+                // 0. Creating the traces
+                val typeTrace = new Logic2AlloyLanguageMapper_TypeMapperTrace_Horizontal
+                trace.typeMapperTrace = typeTrace
+                /**
+                 * Static type -> list of possible dynamic type map
+                 */
+                val typeToConcreteSubtypes = problem.typeToConcreteSubtypes(trace)
+                
+                
+                
+                // 1. Transforming the types
+                
+                // There are two kind of types:
+                // A: one with defined supertypes (including itself), that only has defined elements
+                // Those types can have instances only from the defined elements, ie they are subset of problem.elements
+                // B: one without defined supertypes 
+                // Those types can have instances from two sources
+                // B.1 from elements that dont have definitions
+                // B.2 from newly created elements
+                val allConcreteTypes = problem.types.filter[!it.isAbstract]
+                val definitions = allConcreteTypes.filter(TypeDefinition).toList
+                val declarationsWithDefinedSupertype = allConcreteTypes.filter(TypeDeclaration).filter[it.hasDefinedSupertype].toList
+                val declarationsWithoutDefinedSupertype = allConcreteTypes.filter(TypeDeclaration).filter[!it.hasDefinedSupertype].toList
+                
+                // 2. If there are defined elements
+                if(trace.typeTrace.definedSupertype != null) {
+                        // 3 mapping the elements
+                        problem.elements.transformDefinedSupertype(trace)
+                        // 4. if there are elements that are added to types, then it have to be mapped to defined parts
+                        if(problem.elements.exists[!it.definedInType.empty]) {
+                                definitions.forEach[it.transformDefinition2Definition(trace)]
+                                declarationsWithDefinedSupertype.forEach[it.transformDeclaration2Definition(trace)]
+                        }
+                        // 5. if there are elements that are not added to types, then it have to be mapped to declarations without definitions
+                        if(problem.elements.exists[it.definedInType.empty]) {
+                                declarationsWithoutDefinedSupertype.forEach[it.transformUndefined2Definition(trace)]
+                        }
+                        
+                        definedConcreteTypesAreFull(trace)
+                        definedConcreteTypesAreDisjoint(trace)
+                        problem.definedConcreteTypesAreSatisfyingDefinitions(typeToConcreteSubtypes,trace)
+                }
+                
+                // Transforming the declared and defined concrete types
+                problem.elements.transformDefinedSupertype(trace)
+                if(trace.typeTrace.definedSupertype != null) {
+                        problem.elements.transformDefinedElements(trace)
+                        declarationsWithoutDefinedSupertype.forEach[it.transformNew2Declaration(trace)]
+                }
+                
+                // 2: Caching the types by filling type2AllSignatures
+                for(typeToConcreteSubtypesEntry : typeToConcreteSubtypes.entrySet) {
+                        val type = typeToConcreteSubtypesEntry.key
+                        val List<ALSSignatureDeclaration> signatures = new LinkedList
+                        
+                }
+        }
+        
+        def getTypeTrace(Logic2AlloyLanguageMapperTrace trace) {
+                val res = trace.typeMapperTrace
+                if(res instanceof Logic2AlloyLanguageMapper_TypeMapperTrace_Horizontal) {
+                        return res
+                } else {
+                        throw new IllegalArgumentException('''
+                        Expected type mapping trace: «Logic2AlloyLanguageMapper_TypeMapperTrace_Horizontal.name»,
+                        but found «res.class.name»''')
+                }
+        }
+        
+        private def boolean hasDefinedSupertype(Type type) {
+                if(type instanceof TypeDefinition) {
+                        return true
+                } else {
+                        if(type.supertypes.empty) return false
+                        else return type.supertypes.exists[it.hasDefinedSupertype]
+                }
+        }
+        
+        private def transformDefinedSupertype(List<DefinedElement> elements, Logic2AlloyLanguageMapperTrace trace) {
+                trace.typeTrace.definedSupertype = createALSSignatureDeclaration => [
+                        it.name = support.toID(#["util","defined","Object"])
+                ]
+                trace.specification.signatureBodies += createALSSignatureBody => [
+                        it.abstract = true
+                        it.declarations += trace.typeTrace.definedSupertype
+                ]
+        }
+        
+        private def transformDefinedElements(List<DefinedElement> elements,
+                Logic2AlloyLanguageMapperTrace trace){
+                if(trace.typeTrace.definedSupertype != null) {                  
+                        // 2. Create elements as singleton signatures subtype of definedSupertype
+                        val elementBodies = createALSSignatureBody => [
+                                it.multiplicity = ALSMultiplicity::ONE
+                                it.supertype = trace.typeTrace.definedSupertype
+                        ]
+                        trace.specification.signatureBodies += elementBodies
+                        for(element : elements) {
+                                val elementDeclaration = createALSSignatureDeclaration => [
+                                        it.name = support.toIDMultiple(#["element"],element.name)
+                                ]
+                                elementBodies.declarations += elementDeclaration
+                                trace.typeTrace.definedElement2Declaration.put(element,elementDeclaration)
+                        }
+                        // 3. Specify that definedSupertype is equal to the union of specified
+                        /*trace.specification.factDeclarations += createALSFactDeclaration => [
+                                it.name = support.toID(#["util","typehierarchy","definitionOfElements"])
+                                it.term = createALSEquals => [
+                                        it.leftOperand = createALSReference => [it.referred = trace.typeTrace.definedSupertype]
+                                        it.rightOperand = support.unfoldPlus(elements.map[element|createALSReference=>[
+                                                it.referred = element.lookup(trace.typeTrace.definedElement2Declaration)
+                                        ]])
+                                ]
+                        ]*/
+                }
+        }
+        
+        ///// Type definitions
+        
+        protected def void transformDefinition2Definition(TypeDefinition type, Logic2AlloyLanguageMapperTrace trace) {
+                val sig = createALSSignatureDeclaration => [it.name = support.toIDMultiple(#["definition2definition"],type.name)]
+                val body = createALSSignatureBody => [
+                        it.declarations += sig
+                        it.superset += trace.typeTrace.definedSupertype
+                ]
+                trace.specification.signatureBodies += body
+                trace.typeTrace.definition2definition.put(type,sig)
+        }
+        protected def void transformDeclaration2Definition(TypeDeclaration type, Logic2AlloyLanguageMapperTrace trace) {
+                val sig = createALSSignatureDeclaration => [it.name = support.toIDMultiple(#["declaration2definition"],type.name)]
+                val body = createALSSignatureBody => [
+                        it.declarations += sig
+                        it.superset += trace.typeTrace.definedSupertype
+                ]
+                trace.specification.signatureBodies += body
+                trace.typeTrace.declaration2definition.put(type,sig)
+        }
+        protected def void transformUndefined2Definition(TypeDeclaration type, Logic2AlloyLanguageMapperTrace trace) {
+                val sig = createALSSignatureDeclaration => [it.name = support.toIDMultiple(#["undefined2definition"],type.name)]
+                val body = createALSSignatureBody => [
+                        it.declarations += sig
+                        it.supertype = trace.typeTrace.definedSupertype
+                ]
+                trace.specification.signatureBodies += body
+                trace.typeTrace.undefined2definition.put(type,sig)
+        }
+        protected def void transformNew2Declaration(TypeDeclaration type, Logic2AlloyLanguageMapperTrace trace) {
+                val sig = createALSSignatureDeclaration => [it.name = support.toIDMultiple(#["declaredPartOfDeclaration"],type.name)]
+                val body = createALSSignatureBody => [
+                        it.declarations += sig
+                        it.supertype = trace.typeTrace.declaredSupertype
+                ]
+                trace.specification.signatureBodies += body
+                trace.typeTrace.new2declaration.put(type,sig)
+        }
+        
+        /**
+         * The dynamic types cover each concrete types
+         */
+        protected def definedConcreteTypesAreFull(Logic2AlloyLanguageMapperTrace trace) {
+                trace.specification.factDeclarations += createALSFactDeclaration => [
+                        it.name = support.toID(#["util","typehierarchy","elementFull"])
+                                it.term = createALSEquals => [
+                                        it.leftOperand = createALSReference => [it.referred = trace.typeTrace.definedSupertype]
+                                        it.rightOperand = support.unfoldPlus(
+                                                trace.typeTrace.allDefinedTypes.map[type|
+                                                        createALSReference=>[referred = type]
+                                                ].toList
+                                        )
+                                ]
+                ]
+                
+        }
+        /**
+         * The dynamic types are disjoint
+         */
+        protected def definedConcreteTypesAreDisjoint(Logic2AlloyLanguageMapperTrace trace) {
+                val types = trace.getTypeTrace.allDefinedTypes.toList
+                if (types.size >= 2) {
+                        trace.specification.factDeclarations += createALSFactDeclaration => [
+                                it.name = support.toID(#["util", "typehierarchy", "elementFull"])
+                                it.term = types.disjointSets
+                        ]
+                }
+        }
+        /**
+         * The dynamic types are subtypes of the types where it is defined, but not subtypes where it is not
+         */
+        protected def definedConcreteTypesAreSatisfyingDefinitions(LogicProblem problem, Map<Type,List<Type>> typeToConcreteSubtypes, Logic2AlloyLanguageMapperTrace trace) {
+                val constraintOnElements = problem.elements.typeConstraints(typeToConcreteSubtypes)
+                for(constraintOnElement : constraintOnElements.entrySet) {
+                        val element = constraintOnElement.key
+                        val elementSignature = element.lookup(trace.typeTrace.definedElement2Declaration)
+                        val constraint = constraintOnElement.value
+                        
+                        var ALSTerm negativeConstraints;
+                        if(constraint.negative.isEmpty) {
+                                negativeConstraints = null
+                        } else {
+                                negativeConstraints = support.unfoldAnd(constraint.negative.map[type|
+                                        createALSNot=> [ elementInDefinedType(elementSignature, type, trace) ]
+                                ].toList)
+                        }
+                        
+                        var ALSTerm positiveTypeConstraints
+                        if(constraint.positiveCNF.isEmpty) {
+                                positiveTypeConstraints = null
+                        } else {
+                                positiveTypeConstraints = support.unfoldAnd(constraint.positiveCNF.map[ typeConstraintFromDefinition |
+                                        support.unfoldOr(typeConstraintFromDefinition.map[type |
+                                                elementInDefinedType(elementSignature,type,trace)
+                                        ].toList,trace)
+                                ])
+                        }
+                        
+                        var ALSTerm typeConstraint
+                        if(negativeConstraints != null && positiveTypeConstraints == null) {
+                                typeConstraint = negativeConstraints
+                        } else if (negativeConstraints == null && positiveTypeConstraints != null) {
+                                typeConstraint = positiveTypeConstraints
+                        } else if (negativeConstraints != null && positiveTypeConstraints != null) {
+                                val and = createALSAnd
+                                and.leftOperand = positiveTypeConstraints
+                                and.rightOperand = negativeConstraints
+                                typeConstraint = and
+                        } else {
+                                typeConstraint = null
+                        }
+                        
+                        if(typeConstraint != null) {
+                                val fact =  createALSFactDeclaration => [
+                                        name = support.toIDMultiple(#["util","typehierarchy","definition"],element.name)
+                                ]
+                                fact.term = typeConstraint
+                                trace.specification.factDeclarations +=fact
+                        }
+                        // otherwise there is no type constraint on element
+                }
+        }
+        
+        private def elementInDefinedType(
+                ALSSignatureDeclaration elementSignature,
+                Type type,
+                Logic2AlloyLanguageMapperTrace trace)
+        {
+                var ALSSignatureDeclaration signature
+                if(type instanceof TypeDeclaration) {
+                        if(trace.typeTrace.declaration2definition.containsKey(type)) {
+                                signature = type.lookup(trace.typeTrace.declaration2definition)
+                        } else if(trace.typeTrace.undefined2definition.containsKey(type)) {
+                                signature = type.lookup(trace.typeTrace.undefined2definition)
+                        } else {
+                                return null
+                        }
+                } else if(type instanceof TypeDefinition) {
+                        if(trace.typeTrace.definition2definition.containsKey(type)) {
+                                signature = type.lookup(trace.typeTrace.definition2definition)
+                        } else {
+                                return null
+                        }
+                } else throw new IllegalArgumentException('''Unknownt type «type.class.name»''')
+                
+                val finalSignature = signature
+                return createALSSubset => [
+                        leftOperand = createALSReference => [
+                                referred = elementSignature
+                        ]
+                        rightOperand = createALSReference => [
+                                referred = finalSignature
+                        ]
+                ]
+        }
+        
+        def private typeToConcreteSubtypes(LogicProblem problem, Logic2AlloyLanguageMapperTrace trace) {
+                if(trace.incqueryEngine == null) {
+                        trace.incqueryEngine = ViatraQueryEngine.on(new EMFScope(problem))
+                }
+                val matcher = SupertypeStarMatcher.on(trace.incqueryEngine)
+                val Map<Type,List<Type>> typeToConcreteSubtypes = new HashMap
+                for(supertype : problem.types) {
+                        typeToConcreteSubtypes.put(
+                                supertype,
+                                matcher.getAllValuesOfsubtype(supertype)
+                                        .filter[!it.isIsAbstract].toList)
+                }
+                return typeToConcreteSubtypes
+        }
+        
+        /**
+         * Gives type constraints in a form of CNF 
+         */
+        def private Map<DefinedElement,DynamicTypeConstraints> typeConstraints(List<DefinedElement> elements, Map<Type,List<Type>> typeToConcreteSubtypes) {
+                val Map<DefinedElement,DynamicTypeConstraints> constraints = new HashMap
+                elements.forEach[constraints.put(it,new DynamicTypeConstraints)]
+                
+                for(type : typeToConcreteSubtypes.keySet.filter(TypeDefinition)) {
+                        val subtypes = type.lookup(typeToConcreteSubtypes)
+                        for(elementInType:type.elements) {
+                                elementInType.lookup(constraints).addPositiveTypeOptions(subtypes)
+                        }
+                        for(elementNotInType:elements.filter[!type.elements.contains(it)]) {
+                                elementNotInType.lookup(constraints).addNegativeTypes(subtypes)
+                        }
+                }
+                
+                return constraints
+        }
+        
+        private def ALSTerm disjointSets(List<ALSSignatureDeclaration> signatures) {
+                if(signatures.size >= 2){
+                        val top = createALSEquals => [
+                                it.leftOperand = signatures.intersectionOfTypes
+                                it.rightOperand = createALSNone
+                        ]
+                        if(signatures.size > 2) {
+                                return createALSAnd => [
+                                        it.leftOperand = top
+                                        it.rightOperand = signatures.subList(1,signatures.size).disjointSets
+                                ]
+                        } else{
+                                return top
+                        }
+                } else {
+                        throw new UnsupportedOperationException()
+                }
+        }
+        
+        private def ALSIntersection intersectionOfTypes(List<ALSSignatureDeclaration> signatures) {
+                if(signatures.size == 2) {
+                        return createALSIntersection => [
+                                leftOperand = createALSReference => [it.referred = signatures.get(0)]
+                                rightOperand = createALSReference => [it.referred = signatures.get(1)]
+                        ]
+                } else if(signatures.size > 2) {
+                        return createALSIntersection => [
+                                leftOperand = createALSReference => [it.referred = signatures.get(0)]
+                                rightOperand = signatures.subList(1,signatures.size).intersectionOfTypes
+                        ]
+                } else throw new UnsupportedOperationException()
+        }
+        
+        
+        override transformTypeReference(ComplexTypeReference complexTypeReference, Logic2AlloyLanguageMapper mapper, Logic2AlloyLanguageMapperTrace trace) {
+                //trace.typeTrace.
+        }
+}
+\ No newline at end of file
diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapper_InheritanceAndHorizontal.xtend b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapper_InheritanceAndHorizontal.xtend
new file mode 100644
index 00000000..6533ad36
--- /dev/null
+++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapper_InheritanceAndHorizontal.xtend
@@ -0,0 +1,50 @@
+package hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder
+import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSSignatureDeclaration
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDeclaration
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition
+import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem
+import java.util.HashMap
+import java.util.Map
+import java.util.Collection
+class Logic2AlloyLanguageMapper_TypeMapperTrace_InheritanceAndHorizontal implements Logic2AlloyLanguageMapper_TypeMapperTrace {
+        val Map<TypeDeclaration,ALSSignatureDeclaration> newElementTypes = new HashMap
+        val Map<Type,ALSSignatureDeclaration> definedElementTypes = new HashMap
+        var ALSSignatureDeclaration undefinedSupertype
+        var ALSSignatureDeclaration definedSupertype
+}
+class Logic2AlloyLanguageMapper_TypeMapper_InheritanceAndHorizontal implements Logic2AlloyLanguageMapper_TypeMapper{
+        
+        override transformTypes(Collection<Type> types, Collection<DefinedElement> elements, Logic2AlloyLanguageMapper mapper, Logic2AlloyLanguageMapperTrace trace) {
+                throw new UnsupportedOperationException("TODO: auto-generated method stub")
+        }
+        
+        private def boolean hasDefinedSupertype(Type type) {
+                if(type instanceof TypeDefinition) {
+                        return true
+                } else {
+                        if(type.supertypes.empty) return false
+                        else return type.supertypes.exists[it.hasDefinedSupertype]
+                }
+        }       
+        
+        override transformTypeReference(Type referred, Logic2AlloyLanguageMapper mapper, Logic2AlloyLanguageMapperTrace trace) {
+                throw new UnsupportedOperationException("TODO: auto-generated method stub")
+        }
+        
+        override getUndefinedSupertype(Logic2AlloyLanguageMapperTrace trace) {
+                throw new UnsupportedOperationException("TODO: auto-generated method stub")
+        }
+        
+        override transformReference(DefinedElement referred, Logic2AlloyLanguageMapperTrace trace) {
+                throw new UnsupportedOperationException("TODO: auto-generated method stub")
+        }
+        
+        override getUndefinedSupertypeScope(int undefinedScope, Logic2AlloyLanguageMapperTrace trace) {
+                throw new UnsupportedOperationException("TODO: auto-generated method stub")
+        }
+}
+\ No newline at end of file
diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/unused/AlloyModelInterpretation.xtend_ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/unused/AlloyModelInterpretation.xtend_
new file mode 100644
index 00000000..05b97b0c
--- /dev/null
+++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/unused/AlloyModelInterpretation.xtend_
@@ -0,0 +1,212 @@
+package hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder
+import edu.mit.csail.sdg.alloy4compiler.ast.ExprVar
+import edu.mit.csail.sdg.alloy4compiler.ast.Sig.Field
+import edu.mit.csail.sdg.alloy4compiler.translator.A4Solution
+import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicModelInterpretation
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ConstantDeclaration
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.FunctionDeclaration
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.LogiclanguageFactory
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDeclaration
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition
+import java.util.Arrays
+import java.util.HashMap
+import java.util.LinkedList
+import java.util.List
+import java.util.Map
+import java.util.Set
+import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*
+class AlloyModelInterpretation implements LogicModelInterpretation{
+        
+        protected val extension LogiclanguageFactory factory = LogiclanguageFactory.eINSTANCE
+        //protected val extension LogicProblemBuilder builder = new LogicProblemBuilder
+        
+        protected val Logic2AlloyLanguageMapper forwardMapper
+        protected val Logic2AlloyLanguageMapperTrace forwardTrace;
+        
+        private var ExprVar logicLanguage;
+        private var String logicBooleanTrue;
+        private var String logicBooleanFalse;
+                
+        val Map<String,DefinedElement> alloyAtom2LogicElement = new HashMap
+        private val Map<TypeDeclaration, List<DefinedElement>> interpretationOfUndefinedType = new HashMap
+        
+        private val Map<ConstantDeclaration, Object> constant2Value
+        private val Map<FunctionDeclaration, ? extends Map<ParameterSubstitution, Object>> function2Value
+        private val Map<RelationDeclaration, ? extends Set<ParameterSubstitution>> relation2Value
+        
+        private val int minInt
+        private val int maxInt
+        
+        public new (A4Solution solution, Logic2AlloyLanguageMapper forwardMapper, Logic2AlloyLanguageMapperTrace trace) {
+                
+                this.forwardMapper = forwardMapper
+                this.forwardTrace = trace
+                
+                //TMP sig maps to identify alloy signatures by their names
+                val Map<String,Type> sigName2LogicType =
+                        forwardTrace.type2ALSType.keySet.toMap[x|forwardTrace.type2ALSType.get(x).name]
+                val Map<String,DefinedElement> elementNameNamel2DefinedElement = 
+                        forwardTrace.definedElement2Declaration.keySet.toMap[x|forwardTrace.definedElement2Declaration.get(x).name]
+                        
+                // Fill the interpretation map with empty lists
+                forwardTrace.type2ALSType.keySet.filter(TypeDeclaration).forEach[x|interpretationOfUndefinedType.put(x,new LinkedList)]
+                
+                // exporing individuals
+                for(atom: solution.allAtoms) {
+                        val typeName = getName(atom.type)
+                        val atomName = atom.name
+                        //println(atom.toString + "  < -  " + typeName)
+                        if(typeName == forwardTrace.logicLanguage.name) {
+                                this.logicLanguage = atom
+                        } else if(typeName == "Int" || typeName == "seq/Int") {
+                                // do nothing
+                        } else if(sigName2LogicType.containsKey(typeName) && typeName.lookup(sigName2LogicType) instanceof TypeDefinition) {
+                                val element = elementNameNamel2DefinedElement.get(atomName.head)
+                                alloyAtom2LogicElement.put(atom.label,element)
+                        } else if(sigName2LogicType.containsKey(typeName)) {
+                                val type = sigName2LogicType.get(typeName)
+                                val elementsOfType = interpretationOfUndefinedType.get(type)
+                                val element = createDefinedElement => [
+                                        it.name += type.name
+                                        it.name += (elementsOfType.size+1).toString
+                                ]
+                                alloyAtom2LogicElement.put(atom.label,element)
+                                elementsOfType+=element
+                        } else if(forwardTrace.boolType != null && typeName == forwardTrace.boolType.name) {
+                                if(atomName.head == forwardTrace.boolTrue.name) { this.logicBooleanTrue = atom.label }
+                                else if(atomName.head == forwardTrace.boolFalse.name) { this.logicBooleanFalse = atom.label}
+                                else throw new UnsupportedOperationException('''Unknown boolean value: «atom»''')
+                        }
+                        else throw new UnsupportedOperationException('''Unknown atom: «atom»''')
+                }
+                
+                //TMP field maps
+                val Map<String, Field> name2AlloyField = new HashMap
+                // exploring signatures
+                for(sig:solution.allReachableSigs) {
+                        for(field : sig.fields) {
+                                name2AlloyField.put(field.label,field)
+                        }
+                }
+                
+                // eval consants
+                constant2Value = forwardTrace.constantDeclaration2LanguageField.mapValues[
+                        solution.eval(it.name.lookup(name2AlloyField)).head.atom(1).atomLabel2Term
+                ]
+                // eval functions
+                val hostedfunction2Value = forwardTrace.functionDeclaration2HostedField.mapValues[ function |
+                        newHashMap(
+                                solution.eval(function.name.lookup(name2AlloyField))
+                                        .map[t | new ParameterSubstitution(#[t.atom(0).atomLabel2Term]) -> t.atom(1).atomLabel2Term])]
+                
+                val globalfunction2Value = forwardTrace.functionDeclaration2LanguageField.keySet.toInvertedMap[ function |
+                        val alsFunction = function.lookup(forwardTrace.functionDeclaration2LanguageField)
+                        val paramIndexes = 1..(function.parameters.size)
+                        return newHashMap(
+                                solution.eval(alsFunction.name.lookup(name2AlloyField)).map[t |
+                                        new ParameterSubstitution(paramIndexes.map[t.atom(it).atomLabel2Term])
+                                                ->
+                                        t.atom(function.parameters.size + 1).atomLabel2Term
+                                ])]
+                this.function2Value = Union(hostedfunction2Value,globalfunction2Value)
+                // eval relations
+                val hostedRelation2Value = forwardTrace.relationDeclaration2Field.mapValues[ relation |
+                        solution.eval(relation.name.lookup(name2AlloyField)).map[ t |
+                                new ParameterSubstitution(#[t.atom(0).atomLabel2Term,t.atom(1).atomLabel2Term])].toSet]
+                val globalRelation2Value = forwardTrace.relationDeclaration2Global.mapValues[ relation |
+                        solution.eval(relation.name.lookup(name2AlloyField)).map[ t |
+                                new ParameterSubstitution((1..<t.arity).map[int a|t.atom(a).atomLabel2Term])].toSet]
+                this.relation2Value = Union(hostedRelation2Value,globalRelation2Value)
+                
+                //Int limits
+                this.minInt = solution.min
+                this.maxInt = solution.max
+                
+                //print
+        }
+        
+        def print() {
+                println('''Elements-----''')
+                interpretationOfUndefinedType.forEach[k,v|println('''«k.name» -> «v»''')]
+                
+                println('''Constants-----''')
+                constant2Value.forEach[k, v|println('''«k.name» : «v»''')]
+                println('''Functions-----''')
+                function2Value.forEach[f,m|m.forEach[k,v| println('''«f.name» : «k» |-> «v»''')]]
+                println('''Relations-----''')
+                relation2Value.forEach[r,s|s.forEach[t | println('''«r.name»: («t»)''')]]
+        }
+        
+        def private getName(edu.mit.csail.sdg.alloy4compiler.ast.Type type) {
+                val name = type.toString
+                if(name.startsWith("{this/") && name.endsWith("}")) {
+                        return type.toString.replaceFirst("\\{this\\/","").replace("}","")
+                }
+                else throw new IllegalArgumentException('''Unknown type format: "«name»"!''')
+        }
+        def private getName(ExprVar atom) { atom.toString.split("\\$") }
+        override getElements(Type type) { getElementsDispatch(type) }
+        def private dispatch getElementsDispatch(TypeDeclaration declaration) { return declaration.lookup(this.interpretationOfUndefinedType) }
+        def private dispatch getElementsDispatch(TypeDefinition declaration) { return declaration.elements }
+        
+        override getInterpretation(FunctionDeclaration function, Object[] parameterSubstitution) {
+                val transformedParams = new ParameterSubstitution(parameterSubstitution)
+                return transformedParams.lookup(
+                        function.lookup(this.function2Value)
+                )
+        }
+        
+        override getInterpretation(RelationDeclaration relation, Object[] parameterSubstitution) {
+                relation.lookup(this.relation2Value).contains(new ParameterSubstitution(parameterSubstitution))
+        }
+        
+        override getInterpretation(ConstantDeclaration constant) {
+                constant.lookup(this.constant2Value)
+        }
+        
+        override getMinimalInteger() { this.minInt }
+        override getMaximalInteger() { this.maxInt }
+        
+        // Alloy term -> logic term
+        def private atomLabel2Term(String label) {
+                if(label.number) return Integer.parseInt(label)
+                else if(label == this.logicBooleanTrue) return true
+                else if(label == this.logicBooleanFalse) return false
+                else if(this.alloyAtom2LogicElement.containsKey(label)) return label.lookup(alloyAtom2LogicElement)
+                else throw new IllegalArgumentException('''Unknown atom label: "«label»"!''')
+        }
+        def isNumber(String s) {
+                try{
+                        Integer.parseInt(s)
+                        return true
+                }catch(NumberFormatException e) {
+                        return false
+                }
+        }
+}
+class ParameterSubstitution{
+        val Object[] data;
+        
+        new(Object[] data) { this.data = data }
+        
+        override equals(Object obj) {
+                if(obj === this) return true
+                else if(obj == null) return false
+                if(obj instanceof ParameterSubstitution) {
+                        return Arrays.equals(this.data,obj.data)
+                }
+                return false
+        }
+        
+        override hashCode() {
+                Arrays.hashCode(data)
+        }
+}
+\ No newline at end of file
diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/unused/FunctionWithTimeout.xtend_ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/unused/FunctionWithTimeout.xtend_
new file mode 100644
index 00000000..8c03af6e
--- /dev/null
+++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/unused/FunctionWithTimeout.xtend_
@@ -0,0 +1,40 @@
+package hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder
+import org.eclipse.xtext.xbase.lib.Functions.Function0
+import java.util.concurrent.Executors
+import java.util.concurrent.Callable
+import java.util.concurrent.TimeUnit
+import java.util.concurrent.TimeoutException
+import java.util.concurrent.ExecutionException
+class FunctionWithTimeout<Type> {
+        val Function0<Type> function;
+        
+        new(Function0<Type> function) {
+                this.function = function
+        }
+        
+        def execute(long millisecs) {
+                if(millisecs>0) {
+                        val executor = Executors.newCachedThreadPool();
+                        val task = new Callable<Type>() {
+                           override Type call() { function.apply }
+                        };
+                        val future = executor.submit(task);
+                        try {
+                           val result = future.get(millisecs, TimeUnit.MILLISECONDS);
+                           return result
+                        } catch (TimeoutException ex) {
+                           // handle the timeout
+                        } catch (InterruptedException e) {
+                           // handle the interrupts
+                        } catch (ExecutionException e) {
+                           // handle other exceptions
+                        } finally {
+                           future.cancel(true); // may or may not desire this
+                        }
+                        return null
+                }
+                else return function.apply
+        }       
+}
+\ No newline at end of file
diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/unused/Logic2AlloyApiMapper.xtend_ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/unused/Logic2AlloyApiMapper.xtend_
new file mode 100644
index 00000000..29acd681
--- /dev/null
+++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/unused/Logic2AlloyApiMapper.xtend_
@@ -0,0 +1,345 @@
+package hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder
+import java.util.Map
+import hu.bme.mit.inf.dslreasoner.logic.model.builder.TracedOutput
+import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem
+import java.util.List
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.BoolTypeReference
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.IntTypeReference
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RealTypeReference
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference
+import edu.mit.csail.sdg.alloy4compiler.ast.ExprConstant
+import edu.mit.csail.sdg.alloy4compiler.ast.Expr
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Assertion
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.BoolLiteral
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.IntLiteral
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Not
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.And
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Or
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Impl
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Iff
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.MoreThan
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.LessThan
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.MoreOrEqualThan
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.LessOrEqualThan
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Equals
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Plus
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Minus
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Multiply
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Divison
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Mod
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Forall
+import java.util.HashMap
+import edu.mit.csail.sdg.alloy4compiler.ast.Decl
+import java.util.ArrayList
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Exists
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RealLiteral
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDeclaration
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement
+import edu.mit.csail.sdg.alloy4compiler.ast.Attr
+import edu.mit.csail.sdg.alloy4compiler.ast.Sig.PrimSig
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Term
+import javax.naming.OperationNotSupportedException
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.SymbolicValue
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Constant
+import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.alloylanguage.AlloySpecification
+import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.alloylanguage.Multiplicity
+import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.alloylanguage.InverseReference
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type
+class AlloyInput{
+        public val List<PrimSig> typeDeclarations=new ArrayList
+        public val List<Expr> functionDeclarations=new ArrayList
+        public val List<Expr> assertions=new ArrayList
+        public val List<Expr> multiplicityConstraints=new ArrayList
+        public val List<Expr> inverseConstraints=new ArrayList
+}
+class Logic2AlloyApiMapperTrace {
+        val Map<Type, PrimSig> typeMap
+        val Map<DefinedElement, PrimSig> elementMap
+        //val Map<Function, SMTFunctionDeclaration> functionMap
+        val Map<Relation,Expr> relationMap
+        //val Map<Constant,SMTFunctionDeclaration> constantMap
+        
+        new () {
+                this.typeMap = new HashMap
+                this.elementMap = new HashMap
+                //this.functionMap = new HashMap
+                this.relationMap = new HashMap
+                //this.constantMap = new HashMap
+        }
+        new (Map<Type, PrimSig> typeMap,
+                 Map<DefinedElement, PrimSig> elementMap,
+                 //Map<Function, SMTFunctionDeclaration> functionMap,
+                 Map<Relation,Expr> relationMap/*,
+                 Map<Constant,SMTFunctionDeclaration> constantMap*/)
+        {
+                this.typeMap = typeMap
+                this.elementMap = elementMap
+                //this.functionMap = functionMap
+                this.relationMap = relationMap
+                //this.constantMap = constantMap
+        }
+        
+        def types() { typeMap }
+        def elements() { elementMap }
+        //def functions() { functionMap }
+        def relations() { relationMap }
+        //def constants() { constantMap }
+}
+class Logic2AlloyApiMapper{
+        //TODO output
+        public def TracedOutput<List<PrimSig>, Logic2AlloyApiMapperTrace> transformProblem(LogicProblem problem) {
+                val documentInput = new AlloyInput()
+                //createSMTInput => [satCommand = createSMTSimpleSatCommand getModelCommand = createSMTGetModelCommand]
+                //val document = createSMTDocument => [input = documentInput]
+                val List<PrimSig> document=new ArrayList
+                val trace = new Logic2AlloyApiMapperTrace
+                
+                // Trafo
+                documentInput.typeDeclarations          += problem.types.map[transformType(trace)]
+                //documentInput.functionDeclarations    += problem.functions.map[transformFunction(trace)]
+                documentInput.functionDeclarations      += problem.relations.map[transformRelation(trace)]
+                //documentInput.functionDeclarations    += problem.constants.map[transformConstant(trace)]
+                documentInput.assertions                        += problem.assertions.map[transformAssertion(trace)]
+                
+                
+                val alloySpecification = problem.specifications.filter(AlloySpecification).head
+                
+                for(mult: alloySpecification.multiplicities){
+                        if(mult.min>0){
+                                documentInput.multiplicityConstraints+=mult.transformMultiplicityLowerBound(trace)
+                        }
+                        if(mult.max!=-1){
+                                documentInput.multiplicityConstraints+=mult.transformMultiplicityUpperBound(trace)
+                        }
+                }
+                
+                for(inv: alloySpecification.inverses){
+                        documentInput.inverseConstraints += inv.transformInverse(trace)
+                }
+                // End trafo
+                
+                return new TracedOutput(document,trace)
+        }
+        
+        def Expr transformMultiplicityLowerBound(Multiplicity multiplicity, Logic2AlloyApiMapperTrace trace){
+                
+                val Decl forallVariable=(trace.relations.get(multiplicity.multiplicityOf)).oneOf("o") as Decl
+                return (forallVariable.get.cardinality.gte(ExprConstant.makeNUMBER(multiplicity.min))).forAll(forallVariable)
+                
+        }
+        
+        def Expr transformMultiplicityUpperBound(Multiplicity multiplicity, Logic2AlloyApiMapperTrace trace){
+                
+                val Decl forallVariable=(trace.relations.get(multiplicity.multiplicityOf)).oneOf("o") as Decl
+                return (forallVariable.get.cardinality.lte(ExprConstant.makeNUMBER(multiplicity.max))).forAll(forallVariable)
+                
+        }
+        
+        def Expr transformInverse(InverseReference inverse, Logic2AlloyApiMapperTrace trace){
+                return trace.relations.get(inverse.inverseOf.get(0)).equal(trace.relations.get(inverse.inverseOf.get(1)).transpose)     
+        }
+        
+        private def toID(List<String> names) {names.join("!") }
+        
+        def dispatch protected transformType(TypeDefinition declaration, Logic2AlloyApiMapperTrace trace) {
+                val result = new PrimSig(declaration.name.toID, Attr.ABSTRACT)
+                trace.types.put(declaration,result)
+                return result
+        }
+        
+        def protected transformDefinedElement(TypeDefinition enumType, DefinedElement element, Logic2AlloyApiMapperTrace trace) {
+                val result=new PrimSig(element.name.toID, trace.types.get(enumType), Attr.ONE)
+                trace.elements.put(element,result)
+                return result
+        }
+                
+        def dispatch protected transformType(TypeDeclaration declaration, Logic2AlloyApiMapperTrace trace) {
+                //TODO �r�kles, absztrakt
+                val result = new PrimSig(declaration.name.toID)
+                trace.types.put(declaration,result)
+                return result
+        }
+        
+        def dispatch protected transformTypeReference(BoolTypeReference boolTypeReference, Logic2AlloyApiMapperTrace trace) {
+                throw new UnsupportedOperationException("BoolTypeReference is not supported.")
+        }
+        def dispatch protected transformTypeReference(IntTypeReference intTypeReference, Logic2AlloyApiMapperTrace trace) {
+                return PrimSig.SIGINT
+        }
+        def dispatch protected transformTypeReference(RealTypeReference realTypeReference, Logic2AlloyApiMapperTrace trace) {
+                throw new UnsupportedOperationException("RealTypeReference is not supported.")
+        }
+        def dispatch protected PrimSig transformTypeReference(ComplexTypeReference complexTypeReference, Logic2AlloyApiMapperTrace trace) {
+                return trace.types.get(complexTypeReference.referred)
+        }
+        
+        /*def protected transformFunction(Function declaration, Logic2AlloyApiMapperTrace trace) {
+                val functionDeclaration = createSMTFunctionDeclaration => [
+                        name = declaration.name.toID
+                        range = declaration.range.transformTypeReference(trace)
+                        parameters+= declaration.parameters.map[transformTypeReference(trace)]
+                ]
+                trace.functions.put(declaration,functionDeclaration)
+                return functionDeclaration
+        }*/
+        
+        def transformRelation(Relation relation, Logic2AlloyApiMapperTrace trace) {
+                if(relation.parameters.size==2){
+                        trace.relations.put(relation,(relation.parameters.get(0).transformTypeReference(trace) as PrimSig).addField(relation.name.toID, (relation.parameters.get(1).transformTypeReference(trace) as PrimSig).setOf))
+                } else{
+                        throw new OperationNotSupportedException("More parameters are not supported.")
+                } 
+        }
+        
+        /*def transformConstant(Constant constant, Logic2AlloyApiMapperTrace trace) {
+                val smtConstant = createSMTFunctionDeclaration => [
+                        name = constant.name.toID
+                        range = transformTypeReference(constant.type, trace)
+                ]
+                trace.constants.put(constant,smtConstant)
+                return smtConstant
+        }*/
+        
+        def protected Expr transformAssertion(Assertion assertion, Logic2AlloyApiMapperTrace trace) {
+                
+                return assertion.value.transformTerm(trace,emptyMap)
+        }
+        
+        def dispatch protected Expr transformTerm(BoolLiteral literal, Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables) {
+                throw new UnsupportedOperationException("Bool is not supported")
+                //open util/boolean, autoPay: Bool
+                //https://code.google.com/p/valloy2009/source/browse/trunk/src/models/util/boolean.als?r=142
+        }
+        def dispatch protected Expr transformTerm(IntLiteral literal, Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables)  {
+                return ExprConstant.makeNUMBER(literal.value)
+        }
+        def dispatch protected Expr transformTerm(RealLiteral literal, Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables) {
+                throw new UnsupportedOperationException("Real number is not supported")
+        }
+        def dispatch protected Expr transformTerm(Not not, Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables) {
+                return not.operand.transformTerm(trace,variables).not}
+        def dispatch protected Expr transformTerm(And and, Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables) {
+                val List<Expr> operands= and.operands.map[transformTerm(trace,variables)]
+                var andTerm=operands.get(0)
+                for(Integer i: 1..(operands.size-1)){
+                        andTerm=andTerm.and(operands.get(i))
+                }
+                return andTerm
+        }
+        def dispatch protected Expr transformTerm(Or or, Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables) {
+                val List<Expr> operands= or.operands.map[transformTerm(trace,variables)]
+                var orTerm=operands.get(0)
+                for(Integer i: 1..(operands.size-1)){
+                        orTerm=orTerm.or(operands.get(i))
+                }
+                return orTerm
+        }
+        def dispatch protected Expr transformTerm(Impl impl, Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables) {
+                return impl.leftOperand.transformTerm(trace,variables).implies(impl.rightOperand.transformTerm(trace,variables))
+        }
+        def dispatch protected Expr transformTerm(Iff ifExpression, Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables) {
+                return ifExpression.leftOperand.transformTerm(trace,variables).iff(ifExpression.rightOperand.transformTerm(trace,variables))
+        }
+        def dispatch protected Expr transformTerm(MoreThan moreThan, Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables) {
+                return moreThan.leftOperand.transformTerm(trace,variables).gt(moreThan.rightOperand.transformTerm(trace,variables))
+        }
+        def dispatch protected Expr transformTerm(LessThan lessThan, Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables) {
+                return lessThan.leftOperand.transformTerm(trace,variables).lt(lessThan.rightOperand.transformTerm(trace,variables))
+        }
+        def dispatch protected Expr transformTerm(MoreOrEqualThan moreThan, Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables) {
+                return moreThan.leftOperand.transformTerm(trace,variables).gte(moreThan.rightOperand.transformTerm(trace,variables))
+        }
+        def dispatch protected Expr transformTerm(LessOrEqualThan lessThan, Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables) {
+                return lessThan.leftOperand.transformTerm(trace,variables).lte(lessThan.rightOperand.transformTerm(trace,variables))
+        }
+        def dispatch protected Expr transformTerm(Equals equals, Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables) {
+                return equals.leftOperand.transformTerm(trace,variables).equal(equals.rightOperand.transformTerm(trace,variables))
+        }
+        /*def dispatch protected Expr transformTerm(Distinct distinct, Logic2AlloyApiMapperTrace trace, Map<Variable, SMTSortedVariable> variables) {
+                createSMTDistinct => [ operands += distinct.operands.map[transformTerm(trace,variables)]]}*/
+        def dispatch protected Expr transformTerm(Plus plus, Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables) {
+                return plus.leftOperand.transformTerm(trace,variables).plus(plus.rightOperand.transformTerm(trace,variables))
+        }
+        def dispatch protected Expr transformTerm(Minus minus, Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables) {
+                return minus.leftOperand.transformTerm(trace,variables).minus(minus.rightOperand.transformTerm(trace,variables))
+        }
+        def dispatch protected Expr transformTerm(Multiply multiply, Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables) {
+                return multiply.leftOperand.transformTerm(trace,variables).mul(multiply.rightOperand.transformTerm(trace,variables))
+        }
+        def dispatch protected Expr transformTerm(Divison div, Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables) {
+                return div.leftOperand.transformTerm(trace,variables).div(div.rightOperand.transformTerm(trace,variables))
+        }
+        def dispatch protected Expr transformTerm(Mod mod, Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables) {
+                throw new UnsupportedOperationException("Modulo is not supported.")
+        }
+        def dispatch protected Expr transformTerm(Forall forall, Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables) {
+                return configureForall(forall,trace,variables) 
+        }
+        def dispatch protected Expr transformTerm(Exists exists, Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables) {
+                return configureExists(exists,trace,variables)
+        }
+        def dispatch protected Expr transformTerm(SymbolicValue symbolicValue, Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables) {
+                symbolicValue.symbolicReference.transformSymbolicReference(symbolicValue.parameterSubstitutions,trace,variables) }
+        
+        def private configureForall(
+                Forall quantifiedExpression,
+                Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables)
+        {
+                val allVariables = new HashMap(variables)
+                val newAlloyVariables = new ArrayList<Decl>(quantifiedExpression.quantifiedVariables.size)
+                
+                for(logicVariable: quantifiedExpression.quantifiedVariables) {
+                        val newAlloyVariable = (logicVariable.range.transformTypeReference(trace)).oneOf(logicVariable.name.toID) as Decl
+                        allVariables.put(logicVariable, newAlloyVariable)
+                        newAlloyVariables += newAlloyVariable
+                }
+                val variable0=newAlloyVariables.get(0)
+                newAlloyVariables.remove(0)
+                return (quantifiedExpression.expression.transformTerm(trace,allVariables)).forAll(variable0, newAlloyVariables)
+        }
+        
+        def private configureExists(
+                Exists quantifiedExpression,
+                Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables)
+        {
+                val allVariables = new HashMap(variables)
+                val newAlloyVariables = new ArrayList<Decl>(quantifiedExpression.quantifiedVariables.size)
+                
+                for(logicVariable: quantifiedExpression.quantifiedVariables) {
+                        val newAlloyVariable = (logicVariable.range.transformTypeReference(trace)).oneOf(logicVariable.name.toID) as Decl
+                        allVariables.put(logicVariable, newAlloyVariable)
+                        newAlloyVariables += newAlloyVariable
+                }
+                val variable0=newAlloyVariables.get(0)
+                newAlloyVariables.remove(0)
+                return (quantifiedExpression.expression.transformTerm(trace,allVariables)).forSome(variable0, newAlloyVariables)
+        }
+        
+        def dispatch protected Expr transformSymbolicReference(DefinedElement referred, List<Term> parameterSubstitutions, Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables) {
+                return trace.elements.get(referred)
+        }
+        def dispatch protected Expr transformSymbolicReference(Variable variable, List<Term> parameterSubstitutions, Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables) {
+                return variables.get(variable).get
+        }
+        /*def dispatch protected Expr transformSymbolicReference(Function function, List<Term> parameterSubstitutions, Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables) {
+                val result = createSMTSymbolicValue => [sv | sv.symbolicReference = trace.functions.get(function)]
+                for(paramSubstitution : parameterSubstitutions) {
+                        result.parameterSubstitutions.add(paramSubstitution.transformTerm(trace,variables))
+                }
+                return result
+        }*/
+        def dispatch protected Expr transformSymbolicReference(Relation relation, List<Term> parameterSubstitutions, Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables) {
+                return trace.relations.get(relation)
+        }
+        def dispatch protected Expr transformSymbolicReference(Constant constant, List<Term> parameterSubstitutions, Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables) {
+                //createSMTSymbolicValue => [symbolicReference = trace.constants.get(constant)]
+                throw new UnsupportedOperationException("Constant is not supported")
+        }
+}
+\ No newline at end of file
diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/unused/oldTypes b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/unused/oldTypes
new file mode 100644
index 00000000..5e349ac8
--- /dev/null
+++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/unused/oldTypes
@@ -0,0 +1,74 @@
+/*def dispatch boolean hasDeclaredElement(TypeDefinition type) { return false; }
+        def dispatch boolean hasDeclaredElement(TypeDeclaration type) {
+                if(type.isAbstract) {
+                        type.subtypes.exists[it.hasDeclaredElement]
+                } else return true;
+        }
+        
+        def dispatch List<TypeDefinition> allEnumSubtypes(TypeDefinition type) { return #[type] }
+        def dispatch List<TypeDefinition> allEnumSubtypes(TypeDeclaration type) {
+                return type.subtypes.map[it.allEnumSubtypes].flatten.toList
+        }
+        
+        def protected transformTypes(List<Type> types, Logic2AlloyLanguageMapperTrace trace) {
+                val Map<TypeDeclaration,ALSSignatureDeclaration> signatureTrace = new HashMap;
+                
+                // Creating the root type
+                val objectType = createALSSignatureDeclaration => [ name=#["util","object"].toID it.abstract = true ]
+                trace.objectSupperClass = objectType
+                trace.specification.typeDeclarations += objectType
+                
+                // Creating the images of the types
+                for(type : types) {
+                        if(type instanceof TypeDefinition) {
+                                if(type.elements.empty) {
+                                        trace.type2ALSType.put(type,#[]);
+                                } else {
+                                        val e = createALSEnumDeclaration => [
+                                                it.name = type.name.toID
+                                                it.literal += type.elements.map[transformDefinedElement(trace)]
+                                        ]
+                                        trace.type2ALSType.put(type,#[e])
+                                        trace.specification.typeDeclarations += e
+                                }
+                        }
+                        else if(type instanceof TypeDeclaration) {
+                                if(hasDeclaredElement(type)) {
+                                        val s = createALSSignatureDeclaration => [
+                                                name=type.name.toID
+                                                it.abstract = type.isIsAbstract
+                                        ]
+                                        trace.type2ALSType.put(type,new LinkedList=>[add(s)])
+                                        signatureTrace.put(type, s)
+                                        trace.specification.typeDeclarations += s
+                                }
+                                else {
+                                        signatureTrace.put(type, null)
+                                        trace.type2ALSType.put(type,new LinkedList);// empty
+                                }
+                        }
+                        else throw new IllegalArgumentException('''Unknown type «type.class.name»''')
+                }
+                
+                
+                for(type: types.filter(TypeDeclaration)) {
+                        // Adding inheritance
+                        val s = type.lookup(signatureTrace)
+                        if(s!=null) {
+                                for(supertype : type.supertypes) {
+                                        s.supertype += (supertype as TypeDeclaration).lookup(signatureTrace)
+                                }
+                                if(type.supertypes.empty) {
+                                        s.supertype += objectType
+                                }
+                        }
+                        // Adding enum subtypes
+                        type.lookup(trace.type2ALSType)+=type.allEnumSubtypes.map[it.lookup(trace.type2ALSType)].flatten
+                }
+        }
+        
+        def protected transformDefinedElement(DefinedElement element, Logic2AlloyLanguageMapperTrace trace) {
+                val result = createALSEnumLiteral => [name = element.name.toID]
+                trace.definedElement2EnumProperty.put(element,result)
+                return result
+        }*/
+\ No newline at end of file