From 022a1e52e0cf20f64d9cd6685c65d945c04eaecc Mon Sep 17 00:00:00 2001 From: ArenBabikian Date: Sat, 13 Jun 2020 19:24:25 -0400 Subject: remove Alloy solver copy --- .../reasoner/AlloyAnalyzerConfiguration.xtend | 28 -- .../dlsreasoner/alloy/reasoner/AlloySolver.xtend | 91 ---- .../alloy/reasoner/builder/Alloy2LogicMapper.xtend | 66 --- .../alloy/reasoner/builder/AlloyHandler.xtend | 228 ---------- .../builder/AlloyModelInterpretation.xtend | 249 ----------- ...loyModelInterpretation_TypeInterpretation.xtend | 21 - ...retation_TypeInterpretation_FilteredTypes.xtend | 72 --- ...peInterpretation_InheritanceAndHorizontal.xtend | 20 - .../builder/Logic2AlloyLanguageMapper.xtend | 491 --------------------- .../builder/Logic2AlloyLanguageMapperTrace.xtend | 56 --- .../Logic2AlloyLanguageMapper_ConstantMapper.xtend | 43 -- .../Logic2AlloyLanguageMapper_Containment.xtend | 260 ----------- .../Logic2AlloyLanguageMapper_FunctionMapper.xtend | 87 ---- .../Logic2AlloyLanguageMapper_RelationMapper.xtend | 199 --------- .../Logic2AlloyLanguageMapper_Support.xtend | 207 --------- .../Logic2AlloyLanguageMapper_TypeMapper.xtend | 18 - ...guageMapper_TypeMapperTrace_FilteredTypes.xtend | 15 - ..._TypeMapperTrace_InheritanceAndHorizontal.xtend | 15 - ...oyLanguageMapper_TypeMapper_FilteredTypes.xtend | 263 ----------- ...apper_TypeMapper_InheritanceAndHorizontal.xtend | 122 ----- .../alloy/reasoner/builder/RunCommandMapper.xtend | 105 ----- 21 files changed, 2656 deletions(-) delete mode 100644 Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/AlloyAnalyzerConfiguration.xtend delete mode 100644 Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/AlloySolver.xtend delete mode 100644 Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Alloy2LogicMapper.xtend delete mode 100644 Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyHandler.xtend delete mode 100644 Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyModelInterpretation.xtend delete mode 100644 Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyModelInterpretation_TypeInterpretation.xtend delete mode 100644 Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyModelInterpretation_TypeInterpretation_FilteredTypes.xtend delete mode 100644 Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyModelInterpretation_TypeInterpretation_InheritanceAndHorizontal.xtend delete mode 100644 Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper.xtend delete mode 100644 Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapperTrace.xtend delete mode 100644 Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_ConstantMapper.xtend delete mode 100644 Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_Containment.xtend delete mode 100644 Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_FunctionMapper.xtend delete mode 100644 Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_RelationMapper.xtend delete mode 100644 Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_Support.xtend delete mode 100644 Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapper.xtend delete mode 100644 Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapperTrace_FilteredTypes.xtend delete mode 100644 Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapperTrace_InheritanceAndHorizontal.xtend delete mode 100644 Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapper_FilteredTypes.xtend delete mode 100644 Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapper_InheritanceAndHorizontal.xtend delete mode 100644 Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/RunCommandMapper.xtend (limited to 'Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme') 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 - //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.. [ - 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 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 errors, Exception e) { - super(s + '\n' + errors.join('\n'), e) - } -} - -@Data class MonitoredAlloySolution{ - List warnings - List debugs - long kodkodTime - val List> 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 - val debugs = new LinkedList - val runtime = new ArrayList - 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> 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 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>>{ - - val List warnings - val List debugs - val A4Reporter reporter - val A4Options options - - val Command command - val CompModule compModule - val AlloySolverConfiguration configuration - - val List> answers = new LinkedList() - - new(List warnings, - List 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 integerAtoms = new TreeSet - private SortedSet stringAtoms = new TreeSet - - private val Map alloyAtom2LogicElement = new HashMap - private val Map> interpretationOfUndefinedType = new HashMap - - private val Map constant2Value - private val Map> function2Value - private val Map> 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 name2AlloySig = new HashMap - val Map 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.. collectUnknownAndResolveKnownAtoms(A4Solution solution) { - val Iterable allAtoms = solution.allAtoms - val List 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 objectAtoms, - A4Solution solution, - Logic2AlloyLanguageMapperTrace forwardTrace, - Map name2AlloySig, - Map name2AlloyField, - Map expression2DefinedElement, - Map> 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 objectAtoms, - A4Solution solution, - Logic2AlloyLanguageMapperTrace forwardTrace, - Map name2AlloySig, - Map name2AlloyField, - Map expression2DefinedElement, - Map> interpretationOfUndefinedType) - { - /*val Map expression2DefinedElement = new HashMap() - val Map> 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 objectAtoms, A4Solution solution, Logic2AlloyLanguageMapperTrace forwardTrace, Map name2AlloySig, Map name2AlloyField, Map expression2DefinedElement, Map> 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 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 collectAnnotations(Collection collection, Class 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 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 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 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 variables) { - createALSStringLiteral => [it.value = literal.value] - } - - def dispatch protected ALSTerm transformTerm(Not not, Logic2AlloyLanguageMapperTrace trace, Map variables) { - createALSNot=>[operand = not.operand.transformTerm(trace,variables)] } - def dispatch protected ALSTerm transformTerm(And and, Logic2AlloyLanguageMapperTrace trace, Map variables) { - support.unfoldAnd(and.operands.map[transformTerm(trace,variables)]) } - def dispatch protected ALSTerm transformTerm(Or or, Logic2AlloyLanguageMapperTrace trace, Map variables) { - support.unfoldOr(or.operands.map[transformTerm(trace,variables)],trace) } - def dispatch protected ALSTerm transformTerm(Impl impl, Logic2AlloyLanguageMapperTrace trace, Map variables) { - createALSImpl => [leftOperand = impl.leftOperand.transformTerm(trace,variables) rightOperand = impl.rightOperand.transformTerm(trace,variables)] } - def dispatch protected ALSTerm transformTerm(Iff iff, Logic2AlloyLanguageMapperTrace trace, Map variables) { - createALSIff => [leftOperand = iff.leftOperand.transformTerm(trace,variables) rightOperand = iff.rightOperand.transformTerm(trace,variables)] } - def dispatch protected ALSTerm transformTerm(MoreThan moreThan, Logic2AlloyLanguageMapperTrace trace, Map variables) { - createALSMore => [leftOperand = moreThan.leftOperand.transformTerm(trace,variables) rightOperand = moreThan.rightOperand.transformTerm(trace,variables)] } - def dispatch protected ALSTerm transformTerm(LessThan lessThan, Logic2AlloyLanguageMapperTrace trace, Map variables) { - createALSLess => [leftOperand = lessThan.leftOperand.transformTerm(trace,variables) rightOperand = lessThan.rightOperand.transformTerm(trace,variables)] } - def dispatch protected ALSTerm transformTerm(MoreOrEqualThan moreThan, Logic2AlloyLanguageMapperTrace trace, Map variables) { - createALSMeq => [leftOperand = moreThan.leftOperand.transformTerm(trace,variables) rightOperand = moreThan.rightOperand.transformTerm(trace,variables)] } - def dispatch protected ALSTerm transformTerm(LessOrEqualThan lessThan, Logic2AlloyLanguageMapperTrace trace, Map variables) { - createALSLeq => [leftOperand = lessThan.leftOperand.transformTerm(trace,variables) rightOperand = lessThan.rightOperand.transformTerm(trace,variables)] } - def dispatch protected ALSTerm transformTerm(Equals equals, Logic2AlloyLanguageMapperTrace trace, Map variables) { - createALSEquals => [leftOperand = equals.leftOperand.transformTerm(trace,variables) rightOperand = equals.rightOperand.transformTerm(trace,variables)] } - def dispatch protected ALSTerm transformTerm(Distinct distinct, Logic2AlloyLanguageMapperTrace trace, Map variables) { - support.unfoldDistinctTerms(this,distinct.operands,trace,variables) } - - def dispatch protected ALSTerm transformTerm(Plus plus, Logic2AlloyLanguageMapperTrace trace, Map 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 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 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 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 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 variables) { - support.createQuantifiedExpression(this,forall,ALSMultiplicity.ALL,trace,variables) } - def dispatch protected ALSTerm transformTerm(Exists exists, Logic2AlloyLanguageMapperTrace trace, Map variables) { - support.createQuantifiedExpression(this,exists,ALSMultiplicity.SOME,trace,variables) } - - def dispatch protected ALSTerm transformTerm(InstanceOf instanceOf, Logic2AlloyLanguageMapperTrace trace, Map 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 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 variables) { - symbolicValue.symbolicReference.transformSymbolicReference(symbolicValue.parameterSubstitutions,trace,variables) } - - def dispatch protected ALSTerm transformSymbolicReference(DefinedElement referred, List parameterSubstitutions, Logic2AlloyLanguageMapperTrace trace, Map variables) { - typeMapper.transformReference(referred,trace) - } - def dispatch protected ALSTerm transformSymbolicReference(ConstantDeclaration constant, List parameterSubstitutions, Logic2AlloyLanguageMapperTrace trace, Map 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 parameterSubstitutions, Logic2AlloyLanguageMapperTrace trace, Map 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 parameterSubstitutions, Logic2AlloyLanguageMapperTrace trace, Map variables) { - val res = createALSReference => [referred = variable.lookup(variables)] - return support.postprocessResultOfSymbolicReference(variable.range,res,trace) - } - def dispatch protected ALSTerm transformSymbolicReference(FunctionDeclaration function, List parameterSubstitutions, Logic2AlloyLanguageMapperTrace trace, Map 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 parameterSubstitutions, Logic2AlloyLanguageMapperTrace trace, Map 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 parameterSubstitutions, - Logic2AlloyLanguageMapperTrace trace, Map 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 parameterSubstitutions, - Logic2AlloyLanguageMapperTrace trace, Map 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 constantDeclaration2LanguageField = new HashMap - public val Map constantDefinition2Function = new HashMap - - public val Map functionDeclaration2HostedField = new HashMap - public val Map functionDeclaration2LanguageField = new HashMap - public val Map functionDefinition2Function = new HashMap - - public val Map relationDeclaration2Global = new HashMap - public val Map relationDeclaration2Field = new HashMap - public val Map relationDefinition2Predicate = new HashMap - - public val Map transitiveClosureTarget2Global = new HashMap - public val Map transitiveClosureTarget2Field = new HashMap - - public var Map constantDefinitions - public var Map functionDefinitions - public var Map relationDefinitions - - public var Map relationInTransitiveToGlobalField = new HashMap - public var Map 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 signaturesInContainment, SubsetMatcher matcher) { - for(signatureInContainment : signaturesInContainment) { - if(!matcher.hasMatch(signatureInContainment,target)) { - return false - } - } - return true - }*/ - - /*def boolean coveringSignatureNotInContainment(ALSSignatureDeclaration target, List 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 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 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 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 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 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 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 operands, Logic2AlloyLanguageMapperTrace trace, Map variables) { - if(operands.size == 1) { return m.transformTerm(operands.head,trace,variables) } - else if(operands.size > 1) { - val notEquals = new ArrayList(operands.size*operands.size/2) - for(i:0..[ - 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 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 elements, ALSTerm target, Logic2AlloyLanguageMapperTrace trace, - Map 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 references,Logic2AlloyLanguageMapperTrace trace,Map 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 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 v1, Map 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 types, Collection elements, Logic2AlloyLanguageMapper mapper, Logic2AlloyLanguageMapperTrace trace); - def List 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 type2ALSType = new HashMap; - public val Map 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 type2ALSType = new HashMap; - public val Map definedElement2Declaration = new HashMap - public val Map> 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 types, Collection 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> - 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.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..=2) { - for(type1Index: 0.. [ - 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 operands, - Logic2AlloyLanguageMapperTrace trace - ) { - if(operands.size == 1 || operands.size == 0) {support.unfoldTrueStatement(trace);} - else { - val notEquals = new ArrayList(operands.size*operands.size/2) - for(i:0..[ - 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 types, Collection 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 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 -- cgit v1.2.3-70-g09d2