21 files changed, 0 insertions, 2656 deletions

diff --git a/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/AlloyAnalyzerConfiguration.xtend b/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/AlloyAnalyzerConfiguration.xtend
deleted file mode 100644
index b16ed27f..00000000
--- a/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/AlloyAnalyzerConfiguration.xtend
+++ /dev/null
@@ -1,28 +0,0 @@
-package hu.bme.mit.inf.dlsreasoner.alloy.reasoner
-
-import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration
-
-class AlloySolverConfiguration extends LogicSolverConfiguration {
-        public var int symmetry = 20 // by default
-        public var AlloyBackendSolver solver = AlloyBackendSolver.SAT4J
-        public var TypeMappingTechnique typeMapping = TypeMappingTechnique.InheritanceAndHorizontal
-        public var randomise = 0
-}
-
-enum AlloyBackendSolver {
-        BerkMinPIPE,
-        SpearPIPE,
-        MiniSatJNI,
-        MiniSatProverJNI,
-        LingelingJNI,
-        PLingelingJNI,
-        GlucoseJNI,
-        CryptoMiniSatJNI,
-        SAT4J,
-        CNF,
-        KodKod
-}
-
-enum TypeMappingTechnique {
-        FilteredTypes, InheritanceAndHorizontal
-}
\ No newline at end of file
diff --git a/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/AlloySolver.xtend b/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/AlloySolver.xtend
deleted file mode 100644
index 9cfa7391..00000000
--- a/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/AlloySolver.xtend
+++ /dev/null
@@ -1,91 +0,0 @@
-package hu.bme.mit.inf.dlsreasoner.alloy.reasoner
-
-import edu.mit.csail.sdg.alloy4compiler.translator.A4Solution
-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.Logic2AlloyLanguageMapper_TypeMapper_FilteredTypes
-import hu.bme.mit.inf.dslreasoner.AlloyLanguageStandaloneSetupGenerated
-import hu.bme.mit.inf.dslreasoner.alloyLanguage.AlloyLanguagePackage
-import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel
-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
-
-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 {
-                val alloyConfig = configuration.asConfig
-                val writeFile = (
-                        configuration.documentationLevel===DocumentationLevel::NORMAL ||
-                        configuration.documentationLevel===DocumentationLevel::FULL)
-                
-                // Start: Logic -> Alloy mapping
-                val transformationStart = System.currentTimeMillis
-                val result = forwardMapper.transformProblem(problem,alloyConfig)
-                val alloyProblem = result.output
-                val forwardTrace = result.trace
-                
-                //var String fileURI = null;
-                var String alloyCode = workspace.writeModelToString(alloyProblem,fileName)
-                if(writeFile) {
-                        workspace.writeModel(alloyProblem,fileName)
-                }
-                val transformationTime = System.currentTimeMillis - transformationStart
-                alloyConfig.progressMonitor.workedForwardTransformation
-                // Finish: Logic -> Alloy mapping
-                
-                // Start: Solving Alloy problem
-                //val solverStart = System.currentTimeMillis
-                val result2 = handler.callSolver(alloyProblem,workspace,alloyConfig,alloyCode)
-                alloyConfig.progressMonitor.workedSearchFinished
-                
-                val logicResult = backwardMapper.transformOutput(problem,configuration.solutionScope.numberOfRequiredSolution,result2,forwardTrace,transformationTime)
-                alloyConfig.progressMonitor.workedBackwardTransformationFinished
-                //val solverFinish = System.currentTimeMillis-solverStart
-                // Finish: Solving Alloy problem
-                
-                //logicResult.statistics = 
-                
-                return logicResult
-        }
-        
-        def asConfig(LogicSolverConfiguration configuration) {
-                if(configuration instanceof AlloySolverConfiguration) {
-                        return configuration
-                } else {
-                        throw new IllegalArgumentException('''The configuration has to be an «AlloySolverConfiguration.simpleName»!''')       
-                }
-        }
-        
-        override getInterpretations(ModelResult modelResult) {
-                //val answers = (modelResult.representation as MonitoredAlloySolution).aswers.map[key]
-                val sols = modelResult.representation// as List<A4Solution>
-                //val res = answers.map 
-                sols.map[
-                        new AlloyModelInterpretation(
-                                forwardMapper.typeMapper.typeInterpreter,
-                                it as A4Solution,
-                                forwardMapper,
-                                modelResult.trace as Logic2AlloyLanguageMapperTrace
-                        )
-                ]
-        }       
-}
\ No newline at end of file
diff --git a/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Alloy2LogicMapper.xtend b/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Alloy2LogicMapper.xtend
deleted file mode 100644
index 09b67599..00000000
--- a/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Alloy2LogicMapper.xtend
+++ /dev/null
@@ -1,66 +0,0 @@
-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, int requiredNumberOfSolution, MonitoredAlloySolution monitoredAlloySolution, Logic2AlloyLanguageMapperTrace trace, long transformationTime) {
-                val models = monitoredAlloySolution.aswers.map[it.key].toList
-                
-                if(!monitoredAlloySolution.finishedBeforeTimeout) {
-                        return createInsuficientResourcesResult => [
-                                it.problem = problem
-                                it.representation += models
-                                it.trace = trace
-                                it.statistics = transformStatistics(monitoredAlloySolution,transformationTime)
-                        ]
-                } else {
-                        if(models.last.satisfiable || requiredNumberOfSolution == -1) {
-                                return createModelResult => [
-                                        it.problem = problem
-                                        it.representation += models
-                                        it.trace = trace
-                                        it.statistics = transformStatistics(monitoredAlloySolution,transformationTime)
-                                ]
-                        } else {
-                                return createInconsistencyResult => [
-                                        it.problem = problem
-                                        it.representation += models
-                                        it.trace = trace
-                                        it.statistics = transformStatistics(monitoredAlloySolution,transformationTime)
-                                ]
-                        }
-                }
-        }
-        
-        def transformStatistics(MonitoredAlloySolution solution, long transformationTime) {
-                createStatistics => [
-                        it.transformationTime = transformationTime as int
-                        for(solutionIndex : 0..<solution.aswers.size) {
-                                val solutionTime = solution.aswers.get(solutionIndex).value
-                                 it.entries+= createIntStatisticEntry => [
-                                        it.name = '''Answer«solutionIndex»Time'''
-                                        it.value = solutionTime.intValue
-                                ]
-                        }
-                        it.entries+= createIntStatisticEntry => [
-                                it.name = "Alloy2KodKodTransformationTime"
-                                it.value = solution.kodkodTime as int
-                        ]
-                        it.entries+= createIntStatisticEntry => [
-                                it.name = "Alloy2KodKodTransformationTime"
-                                it.value = solution.kodkodTime as int
-                        ]
-                        it.entries+= createStringStatisticEntry => [
-                                it.name = "warnings"
-                                it.value = '''[«FOR warning : solution.warnings SEPARATOR ","»«warning»«ENDFOR»]'''
-                        ]
-                ]
-        }
-        
-        def sum(Iterable<Long> ints) {
-                ints.reduce[p1, p2|p1+p2]
-        }
-}
\ No newline at end of file
diff --git a/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyHandler.xtend b/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyHandler.xtend
deleted file mode 100644
index eee2d649..00000000
--- a/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyHandler.xtend
+++ /dev/null
@@ -1,228 +0,0 @@
-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.A4Options.SatSolver
-import edu.mit.csail.sdg.alloy4compiler.translator.A4Solution
-import edu.mit.csail.sdg.alloy4compiler.translator.TranslateAlloyToKodkod
-import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.AlloyBackendSolver
-import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.AlloySolverConfiguration
-import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSDocument
-import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration
-import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace
-import java.util.ArrayList
-import java.util.HashMap
-import java.util.LinkedList
-import java.util.List
-import java.util.Map
-import java.util.concurrent.Callable
-import java.util.concurrent.ExecutionException
-import java.util.concurrent.ExecutorService
-import java.util.concurrent.Executors
-import java.util.concurrent.TimeUnit
-import java.util.concurrent.TimeoutException
-import org.eclipse.xtend.lib.annotations.Data
-
-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
-        val List<Pair<A4Solution, Long>> aswers
-        val boolean finishedBeforeTimeout
-}
-
-class AlloyHandler {
-        
-        //val fileName = "problem.als"
-        
-        def callSolver(ALSDocument problem, ReasonerWorkspace workspace, AlloySolverConfiguration configuration,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.inferPartialInstance
-                        //it.tempDirectory = CommonPlugin.resolve(workspace.workspaceURI).toFileString
-                ]
-                
-                // Transform
-                var Command command = null;
-                var CompModule compModule = null
-                
-                // Start: Alloy -> Kodkod
-                val kodkodTransformStart = System.currentTimeMillis();
-                try {
-                        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
-                // Finish: Alloy -> Kodkod
-                
-                val callable = new AlloyCallerWithTimeout(warnings,debugs,reporter,options,command,compModule,configuration)
-                var List<Pair<A4Solution, Long>> answers
-                var boolean finished
-                if(configuration.runtimeLimit == LogicSolverConfiguration::Unlimited) {
-                        answers = callable.call
-                        finished = true
-                } else {
-                        val ExecutorService executor = Executors.newCachedThreadPool();
-                        val future = executor.submit(callable)
-                        try{
-                                answers = future.get(configuration.runtimeLimit,TimeUnit.SECONDS)
-                                finished = true
-                        } catch (TimeoutException ex) {
-                                // handle the timeout
-                        } catch (InterruptedException e) {
-                                // handle the interrupts
-                        } catch (ExecutionException e) {
-                                // handle other exceptions
-                        } finally {
-                                future.cancel(true);
-                                
-                                answers = callable.partialAnswers
-                                finished = false
-                        }
-                }
-
-                new MonitoredAlloySolution(warnings,debugs,kodkodTransformFinish,answers,finished)
-        }
-        
-        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)
-        }
-}
-
-class AlloyCallerWithTimeout implements Callable<List<Pair<A4Solution,Long>>>{
-        
-        val List<String> warnings
-        val List<String> debugs
-        val A4Reporter reporter
-        val A4Options options
-        
-        val Command command
-        val CompModule compModule
-        val AlloySolverConfiguration configuration
-        
-        val List<Pair<A4Solution,Long>> answers = new LinkedList()
-        
-        new(List<String> warnings,
-                List<String> debugs,
-                A4Reporter reporter,
-                A4Options options,
-                Command command,
-                CompModule compModule,
-                AlloySolverConfiguration configuration)
-        {
-                this.warnings = warnings
-                this.debugs = debugs
-                this.reporter = reporter
-                this.options = options
-                this.command = command
-                this.compModule = compModule
-                this.configuration = configuration
-        }
-        
-        override call() throws Exception {
-                val startTime = System.currentTimeMillis
-                
-                // Start: Execute
-                var A4Solution lastAnswer = null
-                try {
-                        if(!configuration.progressMonitor.isCancelled) {
-                                do{
-                                        if(lastAnswer == null) {
-                                                lastAnswer = TranslateAlloyToKodkod.execute_command(reporter,compModule.allSigs,command,options)
-                                        } else {
-                                                lastAnswer = lastAnswer.next
-                                        }
-                                        configuration.progressMonitor.workedBackwardTransformation(configuration.solutionScope.numberOfRequiredSolution)
-                                        
-                                        val runtime = System.currentTimeMillis -startTime
-                                        synchronized(this) {
-                                                answers += (lastAnswer->runtime)
-                                        }
-                                } while(lastAnswer.satisfiable != false && !hasEnoughSolution(answers) && !configuration.progressMonitor.isCancelled)
-                                
-                        }
-                }catch(Exception e) {
-                        warnings +=e.message
-                }
-                // Finish: execute
-                return answers
-        }
-        
-        def hasEnoughSolution(List<?> answers) {
-                if(configuration.solutionScope.numberOfRequiredSolution < 0) return false
-                else return answers.size() == configuration.solutionScope.numberOfRequiredSolution
-        }
-        
-        public def getPartialAnswers() {
-                return answers
-        }
-}
-
-@Data class SolverConfiguration {
-        AlloyBackendSolver backedSolver
-        String path
-        String[] options
-}
\ No newline at end of file
diff --git a/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyModelInterpretation.xtend b/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyModelInterpretation.xtend
deleted file mode 100644
index dcb4bb32..00000000
--- a/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyModelInterpretation.xtend
+++ /dev/null
@@ -1,249 +0,0 @@
-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
-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 java.util.SortedSet
-import java.util.TreeSet
-
-import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*
-
-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 SortedSet<Integer> integerAtoms = new TreeSet
-        private SortedSet<String> stringAtoms = new TreeSet
-                
-        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)
-                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(A4Solution solution) {
-                val Iterable<ExprVar> allAtoms = solution.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") {
-                                val value = Integer.parseInt(atomName.join)
-                                this.integerAtoms.add(value)
-                        } 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 if(typeName == "String") {
-                                val value = parseString(atomName.join)
-                                this.stringAtoms.add(value)
-                        } else {
-                                unknownAtoms += atom
-                        }
-                }
-                val integerSignature = solution.allReachableSigs.filter[it.label=="Int"].head
-                for(i : solution.eval(integerSignature)) {
-                        val value = Integer.parseInt(i.atom(0))
-                        this.integerAtoms.add(value)
-                }
-                val stringSignature = solution.allReachableSigs.filter[it.label=="String"].head
-                for(i : solution.eval(stringSignature)) {
-                        val value = parseString(i.atom(0))
-                        this.stringAtoms.add(value)
-                }
-                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)
-        }
-
-        // 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 if(label.isString) return parseString(label)
-                else throw new IllegalArgumentException('''Unknown atom label: "«label»"!''')
-        }
-        def private isNumber(String s) {
-                try{
-                        Integer.parseInt(s)
-                        return true
-                }catch(NumberFormatException e) {
-                        return false
-                }
-        }
-        def private isString(String label) {
-                label.startsWith("\"") && label.endsWith("\"")
-        }
-        def private parseString(String label) {
-                label.substring(1,label.length-1)
-        }
-        
-        override getAllIntegersInStructure() {
-                this.integerAtoms
-        }
-        
-        override getAllRealsInStructure() {
-                new TreeSet
-        }
-        
-        override getAllStringsInStructure() {
-                this.stringAtoms
-        }
-}
-
-/**
- * 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-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyModelInterpretation_TypeInterpretation.xtend b/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyModelInterpretation_TypeInterpretation.xtend
deleted file mode 100644
index 7082c946..00000000
--- a/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyModelInterpretation_TypeInterpretation.xtend
+++ /dev/null
@@ -1,21 +0,0 @@
-package hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder
-
-import edu.mit.csail.sdg.alloy4compiler.ast.ExprVar
-import edu.mit.csail.sdg.alloy4compiler.translator.A4Solution
-import edu.mit.csail.sdg.alloy4compiler.ast.Sig
-import java.util.Map
-import edu.mit.csail.sdg.alloy4compiler.ast.Sig.Field
-import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement
-import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDeclaration
-import java.util.List
-
-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)
-}
\ No newline at end of file
diff --git a/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyModelInterpretation_TypeInterpretation_FilteredTypes.xtend b/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyModelInterpretation_TypeInterpretation_FilteredTypes.xtend
deleted file mode 100644
index d486649c..00000000
--- a/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyModelInterpretation_TypeInterpretation_FilteredTypes.xtend
+++ /dev/null
@@ -1,72 +0,0 @@
-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
-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.logiclanguage.DefinedElement
-import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.LogiclanguageFactory
-import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDeclaration
-import java.util.ArrayList
-import java.util.List
-import java.util.Map
-
-import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*
-
-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)
-                        }
-                }
-        }
-}
\ No newline at end of file
diff --git a/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyModelInterpretation_TypeInterpretation_InheritanceAndHorizontal.xtend b/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyModelInterpretation_TypeInterpretation_InheritanceAndHorizontal.xtend
deleted file mode 100644
index 249820b6..00000000
--- a/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyModelInterpretation_TypeInterpretation_InheritanceAndHorizontal.xtend
+++ /dev/null
@@ -1,20 +0,0 @@
-package hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder
-
-import edu.mit.csail.sdg.alloy4compiler.ast.ExprVar
-import edu.mit.csail.sdg.alloy4compiler.translator.A4Solution
-import java.util.Map
-import edu.mit.csail.sdg.alloy4compiler.ast.Sig
-import edu.mit.csail.sdg.alloy4compiler.ast.Sig.Field
-import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement
-import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDeclaration
-import java.util.List
-import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.LogiclanguageFactory
-
-class AlloyModelInterpretation_TypeInterpretation_InheritanceAndHorizontal 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) {
-                throw new UnsupportedOperationException("TODO: auto-generated method stub")
-        }
-        
-}
\ No newline at end of file
diff --git a/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper.xtend b/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper.xtend
deleted file mode 100644
index 65eaad47..00000000
--- a/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper.xtend
+++ /dev/null
@@ -1,491 +0,0 @@
-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.ALSDirectProduct
-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.ecore2logic.ecore2logicannotations.InverseRelationAssertion
-import hu.bme.mit.inf.dslreasoner.ecore2logic.ecore2logicannotations.LowerMultiplicityAssertion
-import hu.bme.mit.inf.dslreasoner.ecore2logic.ecore2logicannotations.UpperMultiplicityAssertion
-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.StringLiteral
-import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.StringTypeReference
-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.TransitiveClosure
-import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable
-import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.Annotation
-import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.AssertionAnnotation
-import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem
-import java.util.Collection
-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.*
-
-class Logic2AlloyLanguageMapper {
-        private val extension AlloyLanguageFactory factory = AlloyLanguageFactory.eINSTANCE
-        private val Logic2AlloyLanguageMapper_Support support = new Logic2AlloyLanguageMapper_Support;
-        private val RunCommandMapper runCommandMapper
-        @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
-                this.runCommandMapper = new RunCommandMapper(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))
-                ]
-                specification.transformRandomisation(config.randomise)
-                
-                typeMapper.transformTypes(problem.types,problem.elements,this,trace)
-                
-                trace.constantDefinitions = problem.collectConstantDefinitions
-                trace.functionDefinitions = problem.collectFunctionDefinitions
-                trace.relationDefinitions = problem.collectRelationDefinitions
-                val calledInTransitiveClosure = problem.collectTransitiveRelationCalls
-                
-                problem.constants.forEach[this.constantMapper.transformConstant(it, trace)]
-                problem.functions.forEach[this.functionMapper.transformFunction(it, trace)]
-                problem.relations.forEach[this.relationMapper.transformRelation(it, trace)]
-                calledInTransitiveClosure.forEach[this.relationMapper.prepareTransitiveClosure(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)
-                        }
-                }
-                
-                runCommandMapper.transformRunCommand(this, specification, trace, config)
-                
-                return new TracedOutput(specification,trace)
-        }
-        
-        def transformRandomisation(ALSDocument document, int randomisation) {
-                if(randomisation !== 0) {
-                        document.signatureBodies += createALSSignatureBody => [
-                                val declaration = createALSSignatureDeclaration => [
-                                        it.name = support.toID(#["language","util","randomseed"])
-                                ]
-                                it.declarations += declaration
-                                it.multiplicity = ALSMultiplicity::ONE
-                                for(i : 1..randomisation) {
-                                        it.fields+=createALSFieldDeclaration => [
-                                                it.name = support.toID(#["language","util","randomseedField",i.toString])
-                                                it.multiplicity = ALSMultiplicity::ONE
-                                                it.type = createALSReference => [referred = declaration]
-                                        ]
-                                }
-                        ]
-                }
-        }
-        
-        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 if(multiplicity == ALSMultiplicity::ONE) {
-                        return ALSMultiplicity::ONE
-                } else {
-                        throw new IllegalArgumentException('''Lower multiplicity is already set!''')
-                }
-        }
-        private def addUpper(ALSMultiplicity multiplicity) {
-                if(multiplicity === ALSMultiplicity::ALL) {
-                        return ALSMultiplicity::LONE
-                } else if(multiplicity === ALSMultiplicity::SET || multiplicity === null) {
-                        return ALSMultiplicity::LONE
-                } else if(multiplicity === ALSMultiplicity::SOME) {
-                        return ALSMultiplicity::ONE
-                } else if(multiplicity == ALSMultiplicity::ONE) {
-                        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
-        }
-        private def collectTransitiveRelationCalls(LogicProblem problem) {
-                return problem.eAllContents.filter(TransitiveClosure).map[it.relation].toSet
-        }
-        
-        ////////////////////
-        // 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) { createALSInt }
-        def dispatch protected ALSTerm transformTypeReference(StringTypeReference stringTypeReference, Logic2AlloyLanguageMapperTrace trace) { createALSString }
-        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]])
-        }
-        
-        //////////////
-        // 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) {
-                val v = literal.value.intValue
-                if(v>=0) { createALSNumberLiteral => [value = v]}
-                else {createALSUnaryMinus  => [it.operand = createALSNumberLiteral => [value = v] ] } 
-        }
-        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(StringLiteral literal, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables)  {
-                createALSStringLiteral => [it.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(TransitiveClosure tc, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) {
-                return this.relationMapper.transformTransitiveRelationReference(
-                        tc.relation,
-                        tc.leftOperand.transformTerm(trace,variables),
-                        tc.rightOperand.transformTerm(trace,variables),
-                        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-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapperTrace.xtend b/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapperTrace.xtend
deleted file mode 100644
index 6aadb285..00000000
--- a/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapperTrace.xtend
+++ /dev/null
@@ -1,56 +0,0 @@
-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
-import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation
-
-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 val Map<RelationDeclaration, ALSFieldDeclaration> transitiveClosureTarget2Global = new HashMap
-        public val Map<RelationDeclaration, ALSFieldDeclaration> transitiveClosureTarget2Field = new HashMap
-        
-        public var Map<ConstantDeclaration, ConstantDefinition> constantDefinitions
-        public var Map<FunctionDeclaration, FunctionDefinition> functionDefinitions
-        public var Map<RelationDeclaration, RelationDefinition> relationDefinitions
-        
-        public var Map<Relation, ALSFieldDeclaration> relationInTransitiveToGlobalField = new HashMap
-        public var Map<Relation, ALSFieldDeclaration> relationInTransitiveToHosterField = new HashMap
-}
\ No newline at end of file
diff --git a/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_ConstantMapper.xtend b/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_ConstantMapper.xtend
deleted file mode 100644
index 22650a92..00000000
--- a/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_ConstantMapper.xtend
+++ /dev/null
@@ -1,43 +0,0 @@
-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-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_Containment.xtend b/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_Containment.xtend
deleted file mode 100644
index 399a4eaf..00000000
--- a/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_Containment.xtend
+++ /dev/null
@@ -1,260 +0,0 @@
-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-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_FunctionMapper.xtend b/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_FunctionMapper.xtend
deleted file mode 100644
index 0915c306..00000000
--- a/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_FunctionMapper.xtend
+++ /dev/null
@@ -1,87 +0,0 @@
-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-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_RelationMapper.xtend b/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_RelationMapper.xtend
deleted file mode 100644
index d300a28b..00000000
--- a/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_RelationMapper.xtend
+++ /dev/null
@@ -1,199 +0,0 @@
-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.*
-import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeReference
-import java.util.List
-import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation
-import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSTerm
-
-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 public void transformRelation(RelationDeclaration r, Logic2AlloyLanguageMapperTrace trace) {
-                if(!trace.relationDefinitions.containsKey(r)) {
-                        if(r.transformToHostedField(trace)) {
-                                transformRelationDeclarationToHostedField(r,trace)
-                        } else {
-                                transformRelationDeclarationToGlobalField(r,trace)
-                        }
-                }
-        }
-        
-        def public createRelationDeclaration(String name, List<TypeReference> paramTypes, Logic2AlloyLanguageMapperTrace trace) {
-                val field = createALSFieldDeclaration => [
-                        it.name = support.toID(name)
-                        it.type = support.unfoldReferenceDirectProduct(base,paramTypes,trace)
-                ]
-                trace.logicLanguageBody.fields += field
-                return field
-        }
-        
-        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 public 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)
-                }
-        }
-        
-        public def dispatch void prepareTransitiveClosure(RelationDeclaration relation, Logic2AlloyLanguageMapperTrace trace) {
-                // There is nothing to do, relation can be used in ^relation expressions
-                if(transformToHostedField(relation,trace)) {
-                        trace.relationInTransitiveToHosterField.put(relation,relation.lookup(trace.relationDeclaration2Field))
-                } else {
-                        trace.relationInTransitiveToGlobalField.put(relation,relation.lookup(trace.relationDeclaration2Global))
-                }
-        }
-        public def dispatch void prepareTransitiveClosure(RelationDefinition relation, Logic2AlloyLanguageMapperTrace trace) {
-                if(relation.parameters.size === 2) {
-                        /** 1. Create a relation that can be used in ^relation expressions */ 
-                        val declaration = this.createRelationDeclaration('''AsDeclaration «relation.name»''',relation.parameters,trace)
-                        trace.relationInTransitiveToHosterField.put(relation,declaration)
-                        /** 2. Add fact that the declaration corresponds to the definition */
-                        val fact = createALSFactDeclaration => [
-                                it.name = '''EqualsAsDeclaration «relation.name»'''
-                                it.term = createALSQuantifiedEx => [
-                                        val a = createALSVariableDeclaration => [
-                                                it.name = "a"
-                                                it.range = base.transformTypeReference(relation.parameters.get(0),trace)
-                                        ]
-                                        val b = createALSVariableDeclaration => [
-                                                it.name = "b"
-                                                it.range = base.transformTypeReference(relation.parameters.get(1),trace)
-                                        ]
-                                        it.variables += a
-                                        it.variables += b
-                                        it.type = ALSMultiplicity::ALL
-                                        it.expression = createALSIff => [
-                                                it.leftOperand = createALSFunctionCall => [
-                                                        it.referredDefinition = relation.lookup(trace.relationDefinition2Predicate)
-                                                        it.params += createALSReference => [ it.referred = a ]
-                                                        it.params += createALSReference => [ it.referred = b ]
-                                                ]
-                                                it.rightOperand = createALSSubset => [
-                                                        it.leftOperand = createALSJoin => [
-                                                                it.leftOperand = createALSReference => [ referred = a ]
-                                                                it.rightOperand = createALSReference => [ referred = b ]
-                                                        ]
-                                                        it.rightOperand = createALSJoin => [
-                                                                leftOperand = createALSReference => [referred = trace.logicLanguage]
-                                                                rightOperand = createALSReference => [ referred = declaration ]
-                                                        ]
-                                                ]
-                                        ]
-                                ]
-                        ]
-                        trace.specification.factDeclarations += fact
-                        return
-                } else {
-                        throw new AssertionError('''A non-binary relation "«relation.name»" is used in transitive clousure!''')
-                }
-        }
-                
-        def public transformTransitiveRelationReference(Relation relation, ALSTerm source, ALSTerm target, Logic2AlloyLanguageMapperTrace trace) {
-                val alsTargetRelation = if(trace.relationInTransitiveToGlobalField.containsKey(relation)) {
-                        createALSJoin => [
-                                leftOperand = createALSReference => [referred = trace.logicLanguage]
-                                rightOperand = createALSReference => [ referred =relation.lookup(trace.relationInTransitiveToGlobalField) ]
-                        ]
-                } else if(trace.relationInTransitiveToHosterField.containsKey(relation)){
-                        createALSReference => [it.referred = relation.lookup(trace.relationInTransitiveToHosterField) ]
-                } else {
-                        throw new AssertionError('''Relation «relation.name» is not prepared to transitive closure!''')
-                }
-                return createALSSubset => [
-                        it.leftOperand = createALSJoin => [
-                                it.leftOperand = source
-                                it.rightOperand = target
-                        ]
-                        it.rightOperand = createAlSTransitiveClosure => [it.operand = alsTargetRelation]
-                        
-                ]
-        }
-}
\ No newline at end of file
diff --git a/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_Support.xtend b/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_Support.xtend
deleted file mode 100644
index 0b8d2857..00000000
--- a/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_Support.xtend
+++ /dev/null
@@ -1,207 +0,0 @@
-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-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapper.xtend b/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapper.xtend
deleted file mode 100644
index c998de1f..00000000
--- a/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapper.xtend
+++ /dev/null
@@ -1,18 +0,0 @@
-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)
-        
-        def AlloyModelInterpretation_TypeInterpretation getTypeInterpreter()
-}
diff --git a/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapperTrace_FilteredTypes.xtend b/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapperTrace_FilteredTypes.xtend
deleted file mode 100644
index 17b1a87b..00000000
--- a/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapperTrace_FilteredTypes.xtend
+++ /dev/null
@@ -1,15 +0,0 @@
-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 java.util.HashMap
-import java.util.Map
-
-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
-}
\ No newline at end of file
diff --git a/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapperTrace_InheritanceAndHorizontal.xtend b/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapperTrace_InheritanceAndHorizontal.xtend
deleted file mode 100644
index 1b04a877..00000000
--- a/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapperTrace_InheritanceAndHorizontal.xtend
+++ /dev/null
@@ -1,15 +0,0 @@
-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 java.util.HashMap
-import java.util.List
-import java.util.Map
-
-class Logic2AlloyLanguageMapper_TypeMapperTrace_InheritanceAndHorizontal implements Logic2AlloyLanguageMapper_TypeMapperTrace {
-        public var ALSSignatureDeclaration objectSupperClass;
-        public val Map<Type, ALSSignatureDeclaration> type2ALSType = new HashMap;
-        public val Map<DefinedElement, ALSSignatureDeclaration> definedElement2Declaration = new HashMap
-        public val Map<Type, List<ALSSignatureDeclaration>> typeSelection = new HashMap 
-}
diff --git a/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapper_FilteredTypes.xtend b/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapper_FilteredTypes.xtend
deleted file mode 100644
index 9e548ab6..00000000
--- a/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapper_FilteredTypes.xtend
+++ /dev/null
@@ -1,263 +0,0 @@
-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 static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*
-
-/**
- * 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) {
-                if(undefinedScope == Integer.MAX_VALUE) return undefinedScope else return undefinedScope + trace.typeTrace.definedElement2Declaration.size
-        }
-        
-        override getTypeInterpreter() {
-                return new AlloyModelInterpretation_TypeInterpretation_FilteredTypes
-        }
-}
\ No newline at end of file
diff --git a/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapper_InheritanceAndHorizontal.xtend b/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapper_InheritanceAndHorizontal.xtend
deleted file mode 100644
index 7d90b2b0..00000000
--- a/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapper_InheritanceAndHorizontal.xtend
+++ /dev/null
@@ -1,122 +0,0 @@
-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.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.Collection
-import java.util.LinkedList
-
-class Logic2AlloyLanguageMapper_TypeMapper_InheritanceAndHorizontal implements Logic2AlloyLanguageMapper_TypeMapper{
-        private val extension AlloyLanguageFactory factory = AlloyLanguageFactory.eINSTANCE
-        private val Logic2AlloyLanguageMapper_Support support = new Logic2AlloyLanguageMapper_Support;
-        
-        new() {
-                LogicproblemPackage.eINSTANCE.class
-        }
-        
-        override transformTypes(Collection<Type> types, Collection<DefinedElement> elements, Logic2AlloyLanguageMapper mapper, Logic2AlloyLanguageMapperTrace trace) {
-                val typeTrace = new Logic2AlloyLanguageMapper_TypeMapperTrace_InheritanceAndHorizontal
-                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]
-                        body.abstract = type.isIsAbstract || (type instanceof TypeDefinition)
-                        
-                        trace.specification.signatureBodies += body
-                        typeTrace.type2ALSType.put(type,sig)
-                        
-                        typeTrace.typeSelection.put(type,new LinkedList()=>[add(sig)])
-                }
-                
-                for(element : elements) {
-                        val mostSpecificTypes = element.definedInType.filter[it.subtypes.empty]
-                        if(mostSpecificTypes.size== 1) {
-                                val mostSpecificSubtype = mostSpecificTypes.head
-                                val elementContainer = createALSSignatureBody => [
-                                        it.multiplicity = ALSMultiplicity::ONE
-                                        it.supertype =typeTrace.type2ALSType.get(mostSpecificSubtype)
-                                ]
-                                val signature = createALSSignatureDeclaration => [it.name = support.toIDMultiple("element",element.name)]
-                                elementContainer.declarations += signature
-                                typeTrace.definedElement2Declaration.put(element,signature)
-                                trace.specification.signatureBodies += elementContainer
-                        } else {
-                                throw new UnsupportedOperationException
-                        }
-                }
-                
-                // 6. Each inheritance is modeled by extend keyword
-                for(type : types) {
-                        if(type.supertypes.size == 0) {
-                                (typeTrace.type2ALSType.get(type).eContainer as ALSSignatureBody).supertype = typeTrace.objectSupperClass
-                        }if(type.supertypes.size == 1) {
-                                val alsType = typeTrace.type2ALSType.get(type.supertypes.head)
-                                (typeTrace.type2ALSType.get(type).eContainer as ALSSignatureBody).supertype = alsType
-                                
-                        } else if(type.supertypes.size > 1){
-                                val alsMainType = typeTrace.type2ALSType.get(type.supertypes.head)
-                                (typeTrace.type2ALSType.get(type).eContainer as ALSSignatureBody).supertype = alsMainType
-                                for(otherType : type.supertypes.filter[it != alsMainType]) {
-                                        typeTrace.typeSelection.get(otherType).add(typeTrace.type2ALSType.get(type))
-                                }
-                        }
-                }
-        }
-        
-        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]
-                }
-        }
-        
-        def getTypeTrace(Logic2AlloyLanguageMapperTrace trace) {
-                val res = trace.typeMapperTrace
-                if(res instanceof Logic2AlloyLanguageMapper_TypeMapperTrace_InheritanceAndHorizontal) {
-                        return res
-                } else {
-                        throw new IllegalArgumentException('''
-                        Expected type mapping trace: «Logic2AlloyLanguageMapper_TypeMapperTrace_FilteredTypes.name»,
-                        but found «res.class.name»''')
-                }
-        }
-        
-        override transformTypeReference(Type referred, Logic2AlloyLanguageMapper mapper, Logic2AlloyLanguageMapperTrace trace) {
-                trace.typeTrace.typeSelection.get(referred)
-        }
-        
-        override getUndefinedSupertype(Logic2AlloyLanguageMapperTrace trace) {
-                trace.typeTrace.objectSupperClass
-        }
-        
-        override transformReference(DefinedElement referred, Logic2AlloyLanguageMapperTrace trace) {
-                val r =  trace.typeTrace.definedElement2Declaration.get(referred)
-                return createALSReference => [it.referred =r]
-        }
-        
-        override getUndefinedSupertypeScope(int undefinedScope, Logic2AlloyLanguageMapperTrace trace) {
-                return undefinedScope + trace.typeTrace.definedElement2Declaration.size
-        }
-        
-        override getTypeInterpreter() {
-                return new AlloyModelInterpretation_TypeInterpretation_InheritanceAndHorizontal
-        }
-        
-}
\ No newline at end of file
diff --git a/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/RunCommandMapper.xtend b/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/RunCommandMapper.xtend
deleted file mode 100644
index fdc35412..00000000
--- a/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/RunCommandMapper.xtend
+++ /dev/null
@@ -1,105 +0,0 @@
-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.ALSInt
-import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSTerm
-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.logiclanguage.TypeDefinition
-import java.util.LinkedList
-import java.util.List
-
-import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*
-
-class RunCommandMapper {
-        private val extension AlloyLanguageFactory factory = AlloyLanguageFactory.eINSTANCE
-        private val Logic2AlloyLanguageMapper_Support support = new Logic2AlloyLanguageMapper_Support;
-        private val Logic2AlloyLanguageMapper_TypeMapper typeMapper;
-        
-        public new(Logic2AlloyLanguageMapper_TypeMapper typeMapper) {
-                this.typeMapper = typeMapper
-        }
-        
-        def public transformRunCommand(Logic2AlloyLanguageMapper mapper, ALSDocument specification, Logic2AlloyLanguageMapperTrace trace, AlloySolverConfiguration config)
-        {
-                //val knownStringNumber = specification.eAllContents.filter(ALSStringLiteral).map[it.value].toSet.size
-                
-                // add fact to ensure the existence of all literals in the scope
-                if(!config.typeScopes.knownStrings.empty) {
-                        specification.factDeclarations += createALSFactDeclaration => [
-                                it.name = "EnsureAllStrings"
-                                val List<? extends ALSTerm> equals = config.typeScopes.knownStrings.map[x|createALSEquals => [
-                                        it.leftOperand =createALSStringLiteral => [it.value = x]
-                                        it.rightOperand =createALSStringLiteral => [it.value = x]
-                                ]].toList
-                                it.term = support.unfoldAnd(equals)
-                        ]
-                }
-                val typeScopes = new LinkedList
-                for(definedScope : config.typeScopes.maxNewElementsByType.entrySet) {
-                                val key = definedScope.key
-                                val amount = definedScope.value
-                                val exactly = config.typeScopes.minNewElementsByType.containsKey(key) && config.typeScopes.minNewElementsByType.get(key) === amount
-                                
-                                val existing = key.transitiveClosureStar[it.subtypes].filter(TypeDefinition).map[elements].flatten.toSet
-                                if(amount == 0 && exactly) {
-                                        specification.factDeclarations += createALSFactDeclaration => [
-                                                it.term = createALSEquals => [
-                                                        it.leftOperand = support.unfoldPlus(typeMapper.transformTypeReference(key,mapper,trace).map[t|createALSReference => [it.referred = t]].toList)
-                                                        it.rightOperand =  support.unfoldPlus( existing.map[typeMapper.transformReference(it,trace)].toList )
-                                                ]
-                                        ]
-                                }
-                                val int n = existing.size-amount
-                                typeScopes += createALSSigScope => [
-                                        it.type = typeMapper.transformTypeReference(key,mapper,trace).head
-                                        it.number = n
-                                        it.exactly =exactly
-                                ]
-                        }
-                
-                specification.runCommand = createALSRunCommand => [
-                        it.typeScopes+= createALSSigScope => [
-                                it.type= typeMapper.getUndefinedSupertype(trace)
-                                it.number = typeMapper.getUndefinedSupertypeScope(config.typeScopes.maxNewElements,trace) 
-                                it.exactly = (config.typeScopes.maxNewElements == config.typeScopes.minNewElements)
-                        ]
-                        if(config.typeScopes.maxNewIntegers == LogicSolverConfiguration::Unlimited) {
-                                val integersUsed = specification.eAllContents.filter(ALSInt)
-                                if(integersUsed.empty) {
-                                        // If no integer scope is defined, but the problem has no integers
-                                        // => scope can be empty
-                                        it.typeScopes+= createALSIntScope => [
-                                                it.number = 0
-                                        ]
-                                } else {
-                                        // If no integer scope is defined, and the problem has integers
-                                        // => error
-                                        throw new UnsupportedOperationException('''An integer scope have to be specified for Alloy!''')
-                                }
-                        } else {
-                                it.typeScopes += createALSIntScope => [
-                                        if(config.typeScopes.knownIntegers.empty) {
-                                                number = Integer.SIZE-Integer.numberOfLeadingZeros(config.typeScopes.maxNewIntegers+1/2)
-                                        } else {
-                                                var scope = Math.max(
-                                                        Math.abs(config.typeScopes.knownIntegers.max),
-                                                        Math.abs(config.typeScopes.knownIntegers.min))
-                                                if(scope*2+1 < config.typeScopes.knownIntegers.size + config.typeScopes.maxNewIntegers) {
-                                                        scope += ((config.typeScopes.knownIntegers.size + config.typeScopes.maxNewIntegers) - (scope*2))/2
-                                                }
-                                                number = Integer.SIZE-Integer.numberOfLeadingZeros(scope)+1
-                                        }
-                                ]
-                        }
-                        if(config.typeScopes.maxNewStrings === LogicSolverConfiguration::Unlimited) {
-                                throw new UnsupportedOperationException('''An string scope have to be specified for Alloy!''')
-                        } else {
-                                if(config.typeScopes.maxNewStrings != 0) {
-                                        it.typeScopes += createALSStringScope => [it.number = 0]
-                                }
-                        }
-                ]
-        }
-}
\ No newline at end of file