Objective POC implementation

author: Kristóf Marussy <kris7topher@gmail.com> 2019-04-08 00:58:00 +0200
committer: Kristóf Marussy <kris7topher@gmail.com> 2019-04-08 00:58:00 +0200
commit: c1f185fd8fc2c3dfc123d9271726c588963c7c01 (patch)
tree: 88a5bb94017e7d3f0fbce0a51a78c2549b0977bd /Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution
parent: Infrastructure for objective functions (diff)
download: VIATRA-Generator-c1f185fd8fc2c3dfc123d9271726c588963c7c01.tar.gz
VIATRA-Generator-c1f185fd8fc2c3dfc123d9271726c588963c7c01.tar.zst
VIATRA-Generator-c1f185fd8fc2c3dfc123d9271726c588963c7c01.zip
3 files changed, 147 insertions, 59 deletions
diff --git a/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/GenerationTaskExecutor.xtend b/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/GenerationTaskExecutor.xtend
index 35ffaf65..8ea674d3 100644
--- a/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/GenerationTaskExecutor.xtend
+++ b/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/GenerationTaskExecutor.xtend
@@ -133,7 +133,9 @@ class GenerationTaskExecutor {
                        // 5. create a solver and a configuration
                        // 5.1 initialize
                        val solver = solverLoader.loadSolver(task.solver,configurationMap)
-                        val solverConfig = solverLoader.loadSolverConfig(task.solver,configurationMap,console)
+                        val objectiveSpecification = scriptExecutor.getObjectiveSpecification(task.objectives)
+                        val objectiveEntries = objectiveSpecification?.entries ?: emptyList
+                        val solverConfig = solverLoader.loadSolverConfig(task.solver,configurationMap,objectiveEntries,console)
                        
                        
                        // 5.2 set values that defined directly 
diff --git a/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/ScriptExecutor.xtend b/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/ScriptExecutor.xtend
index 0512a5ee..25036df6 100644
--- a/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/ScriptExecutor.xtend
+++ b/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/ScriptExecutor.xtend
@@ -30,6 +30,8 @@ import org.eclipse.core.runtime.Status
 import org.eclipse.core.runtime.jobs.Job
 import org.eclipse.emf.common.util.URI
 import org.eclipse.xtend.lib.annotations.FinalFieldsConstructor
+import hu.bme.mit.inf.dslreasoner.application.applicationConfiguration.ObjectiveSpecification
+import hu.bme.mit.inf.dslreasoner.application.applicationConfiguration.ObjectiveReference
 @FinalFieldsConstructor
 class ScriptExecutor {
@@ -40,7 +42,7 @@ class ScriptExecutor {
        /**
         * Executes a script
         */
-        public def executeScript(URI uri) {
+        def executeScript(URI uri) {
                val job = new Job('''Model Generation: «uri.lastSegment»''') {
                        override protected run(IProgressMonitor monitor) {
                                try{
@@ -57,7 +59,7 @@ class ScriptExecutor {
                job.schedule();
        }
        
-        public def executeScript(ConfigurationScript script, IProgressMonitor monitor) {
+        def executeScript(ConfigurationScript script, IProgressMonitor monitor) {
                script.activateAllEPackageReferences
                val tasks = script.commands.filter(Task)
                
@@ -94,12 +96,12 @@ class ScriptExecutor {
 //              }
        }
        
-        def public dispatch execute(GenerationTask task, IProgressMonitor monitor) {
+        def dispatch void execute(GenerationTask task, IProgressMonitor monitor) {
                val generationTaskExecutor = new GenerationTaskExecutor
                generationTaskExecutor.executeGenerationTask(task,this,scriptConsoleFactory,monitor)
        }
        
-        def public dispatch execute(Task task, IProgressMonitor monitor) {
+        def dispatch void execute(Task task, IProgressMonitor monitor) {
                throw new IllegalArgumentException('''Unsupported task type: «task.class.simpleName»!''')
        }
        
@@ -174,6 +176,16 @@ class ScriptExecutor {
                null
        }
        
+        def dispatch getObjectiveSpecification(ObjectiveSpecification config) {
+                config
+        }
+        def dispatch getObjectiveSpecification(ObjectiveReference config) {
+                config.referred.specification
+        }
+        def dispatch getObjectiveSpecification(Void config) {
+                null
+        }
+        
        def dispatch getConfiguration(ConfigSpecification config) {
                config
        }
diff --git a/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/SolverLoader.xtend b/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/SolverLoader.xtend
index 9eceef5f..f769d46f 100644
--- a/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/SolverLoader.xtend
+++ b/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/SolverLoader.xtend
@@ -1,44 +1,47 @@
 package hu.bme.mit.inf.dslreasoner.application.execution
-import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.AlloyBackendSolver
 import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.AlloySolver
 import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.AlloySolverConfiguration
+import hu.bme.mit.inf.dslreasoner.application.applicationConfiguration.CostObjectiveFunction
+import hu.bme.mit.inf.dslreasoner.application.applicationConfiguration.ObjectiveEntry
+import hu.bme.mit.inf.dslreasoner.application.applicationConfiguration.OptimizationEntry
 import hu.bme.mit.inf.dslreasoner.application.applicationConfiguration.Solver
+import hu.bme.mit.inf.dslreasoner.application.applicationConfiguration.ThresholdEntry
 import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration
 import hu.bme.mit.inf.dslreasoner.smt.reasoner.SMTSolver
 import hu.bme.mit.inf.dslreasoner.smt.reasoner.SmtSolverConfiguration
+import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.CostObjectiveConfiguration
+import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.CostObjectiveElementConfiguration
+import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.DiversityDescriptor
 import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ViatraReasoner
 import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ViatraReasonerConfiguration
+import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization.ObjectiveKind
+import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization.ObjectiveThreshold
+import hu.bme.mit.inf.dslreasoner.visualisation.pi2graphviz.GraphvizVisualiser
+import java.util.List
 import java.util.Map
 import java.util.Optional
+import org.eclipse.viatra.query.patternlanguage.emf.vql.PatternModel
+import org.eclipse.xtext.EcoreUtil2
 import org.eclipse.xtext.xbase.lib.Functions.Function1
-import hu.bme.mit.inf.dslreasoner.visualisation.pi2graphviz.GraphvizVisualiser
-import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.DiversityDescriptor
 class SolverLoader {
        def loadSolver(Solver solver, Map<String, String> config) {
-                switch(solver) {
+                switch (solver) {
                        case ALLOY_SOLVER: return new AlloySolver
                        case SMT_SOLVER: return new SMTSolver
                        case VIATRA_SOLVER: return new ViatraReasoner
                }
        }
-        
-        
+        private def <Type> Optional<Type> getAsType(Map<String, String> config, String key, ScriptConsole console,
-        
+                Function1<String, Type> parser, Class<Type> requestedType) {
-        private def <Type>  Optional<Type> getAsType(
+                if (config.containsKey(key)) {
-                Map<String, String> config,
-                String key,
-                ScriptConsole console,
-                Function1<String,Type> parser,
-                Class<Type> requestedType)
-        {
-                if(config.containsKey(key)) {
                        val stringValue = config.get(key)
-                        try{
+                        try {
                                val parsedValue = parser.apply(stringValue)
                                return Optional.of(parsedValue)
-                        } catch(Exception e) {
+                        } catch (Exception e) {
                                console.writeError('''Unable to parse configuration value for "«key»" to «requestedType.simpleName»!''')
                                return Optional::empty
                        }
@@ -46,60 +49,131 @@ class SolverLoader {
                        return Optional::empty
                }
        }
        private def getAsInteger(Map<String, String> config, String key, ScriptConsole console) {
-                return getAsType(config,key,console,[x|Integer.parseInt(x)],Integer)
+                return getAsType(config, key, console, [x|Integer.parseInt(x)], Integer)
        }
        private def getAsBoolean(Map<String, String> config, String key, ScriptConsole console) {
-                return getAsType(config,key,console,[x|Boolean.parseBoolean(x)],Boolean)
+                return getAsType(config, key, console, [x|Boolean.parseBoolean(x)], Boolean)
        }
        private def getAsDouble(Map<String, String> config, String key, ScriptConsole console) {
-                return getAsType(config,key,console,[x|Double.parseDouble(x)],Double)
+                return getAsType(config, key, console, [x|Double.parseDouble(x)], Double)
        }
-        
-        def loadSolverConfig(
+        def loadSolverConfig(Solver solver, Map<String, String> config, List<ObjectiveEntry> objectiveEntries,
-                Solver solver,
+                ScriptConsole console) {
-                Map<String, String> config,
+                switch (solver) {
-                ScriptConsole console)
+                        case ALLOY_SOLVER: {
-        {
+                                if (!objectiveEntries.empty) {
-                if(solver === Solver::ALLOY_SOLVER) {
+                                        throw new IllegalArgumentException("Objectives are not supported by Alloy.")
-                        return new AlloySolverConfiguration => [c|
+                                }
-                                config.getAsInteger("symmetry",console)
+                                val c = new SmtSolverConfiguration
-                                        .ifPresent[c.symmetry = it]
+                                config.getAsBoolean("fixRandomSeed", console).ifPresent[c.fixRandomSeed = it]
-                                config.getAsType("solver",console,[x|AlloyBackendSolver::valueOf(x)],AlloyBackendSolver)
+                                config.getAsType("path", console, [it], String).ifPresent[c.solverPath = it]
-                                        .ifPresent[c.solver = it]
+                                c
-                        ]
+                        }
-                } else if(solver === Solver::SMT_SOLVER) {
+                        case SMT_SOLVER: {
-                        return new SmtSolverConfiguration => [c|
+                                if (!objectiveEntries.empty) {
-                                config.getAsBoolean("fixRandomSeed",console).ifPresent[c.fixRandomSeed = it]
+                                        throw new IllegalArgumentException("Objectives are not supported by Z3.")
-                                config.getAsType("path",console,[it],String).ifPresent[c.solverPath = it]
+                                }
-                        ]
+                                val c = new SmtSolverConfiguration
-                } else if(solver === Solver::VIATRA_SOLVER) {
+                                config.getAsBoolean("fixRandomSeed", console).ifPresent[c.fixRandomSeed = it]
-                        return new ViatraReasonerConfiguration => [c|
+                                config.getAsType("path", console, [it], String).ifPresent[c.solverPath = it]
+                                c
+                        }
+                        case VIATRA_SOLVER: {
+                                val c = new ViatraReasonerConfiguration
                                c.debugConfiguration.partialInterpretatioVisualiser = new GraphvizVisualiser
-                                if(config.containsKey("diversity-range")) {
+                                if (config.containsKey("diversity-range")) {
                                        val stringValue = config.get("diversity-range")
-                                        try{
+                                        try {
                                                val range = Integer.parseInt(stringValue)
                                                c.diversityRequirement = new DiversityDescriptor => [
                                                        it.ensureDiversity = true
                                                        it.range = range
                                                ]
-                                        } catch (NumberFormatException e) {console.writeError('''Malformed number format: «e.message»''')}
+                                        } catch (NumberFormatException e) {
+                                                console.writeError('''Malformed number format: «e.message»''')
+                                        }
                                }
-                        ]
+                                for (objectiveEntry : objectiveEntries) {
-                } else {
+                                        val costObjectiveConfig = new CostObjectiveConfiguration
-                        throw new UnsupportedOperationException('''Unknown solver: «solver»''')
+                                        switch (objectiveEntry) {
+                                                OptimizationEntry: {
+                                                        costObjectiveConfig.findExtremum = true
+                                                        costObjectiveConfig.kind = switch (direction : objectiveEntry.direction) {
+                                                                case MAXIMIZE:
+                                                                        ObjectiveKind.HIGHER_IS_BETTER
+                                                                case MINIMIZE:
+                                                                        ObjectiveKind.LOWER_IS_BETTER
+                                                                default:
+                                                                        throw new IllegalArgumentException("Unknown direction: " + direction)
+                                                        }
+                                                        costObjectiveConfig.threshold = ObjectiveThreshold.NO_THRESHOLD
+                                                }
+                                                ThresholdEntry: {
+                                                        costObjectiveConfig.findExtremum = false
+                                                        val threshold = objectiveEntry.threshold.doubleValue
+                                                        switch (operator : objectiveEntry.operator) {
+                                                                case LESS: {
+                                                                        costObjectiveConfig.kind = ObjectiveKind.LOWER_IS_BETTER
+                                                                        costObjectiveConfig.threshold = new ObjectiveThreshold.Exclusive(threshold)
+                                                                }
+                                                                case GREATER: {
+                                                                        costObjectiveConfig.kind = ObjectiveKind.HIGHER_IS_BETTER
+                                                                        costObjectiveConfig.threshold = new ObjectiveThreshold.Exclusive(threshold)
+                                                                }
+                                                                case LESS_EQUALS: {
+                                                                        costObjectiveConfig.kind = ObjectiveKind.LOWER_IS_BETTER
+                                                                        costObjectiveConfig.threshold = new ObjectiveThreshold.Exclusive(threshold)
+                                                                }
+                                                                case GREATER_EQUALS: {
+                                                                        costObjectiveConfig.kind = ObjectiveKind.HIGHER_IS_BETTER
+                                                                        costObjectiveConfig.threshold = new ObjectiveThreshold.Exclusive(threshold)
+                                                                }
+                                                                default:
+                                                                        throw new IllegalArgumentException("Unknown operator: " + operator)
+                                                        }
+                                                }
+                                        }
+                                        val function = objectiveEntry.function
+                                        if (function instanceof CostObjectiveFunction) {
+                                                for (costEntry : function.entries) {
+                                                        val element = new CostObjectiveElementConfiguration
+                                                        val pattern = costEntry.patternElement.pattern
+                                                        val packageName = costEntry.patternElement.package?.packageName ?:
+                                                                EcoreUtil2.getContainerOfType(pattern, PatternModel)?.packageName
+                                                        element.patternQualifiedName = if (packageName.nullOrEmpty) {
+                                                                pattern.name
+                                                        } else {
+                                                                packageName + "." + pattern.name
+                                                        }
+                                                        costObjectiveConfig.elements += element
+                                                }
+                                        } else {
+                                                throw new IllegalArgumentException("Only cost objectives are supported by VIATRA.")
+                                        }
+                                        c.costObjectives += costObjectiveConfig
+                                }
+                                c
+                        }
+                        default:
+                                throw new UnsupportedOperationException('''Unknown solver: «solver»''')
                }
        }
-        
-        def dispatch void setRunIndex(AlloySolverConfiguration config, Map<String, String> parameters, int runIndex, ScriptConsole console) {
+        def dispatch void setRunIndex(AlloySolverConfiguration config, Map<String, String> parameters, int runIndex,
-                parameters.getAsBoolean("randomize",console).ifPresent[
+                ScriptConsole console) {
-                        if(it) {
+                parameters.getAsBoolean("randomize", console).ifPresent [
-                                config.randomise = runIndex-1
+                        if (it) {
+                                config.randomise = runIndex - 1
                        }
                ]
        }
-        def dispatch void setRunIndex(LogicSolverConfiguration config, Map<String, String> parameters, int runIndex, ScriptConsole console) {
-                
+        def dispatch void setRunIndex(LogicSolverConfiguration config, Map<String, String> parameters, int runIndex,
+                ScriptConsole console) {
        }
-}
-\ No newline at end of file
+}
author	Kristóf Marussy <kris7topher@gmail.com>	2019-04-08 00:58:00 +0200
committer	Kristóf Marussy <kris7topher@gmail.com>	2019-04-08 00:58:00 +0200
commit	c1f185fd8fc2c3dfc123d9271726c588963c7c01 (patch)
tree	88a5bb94017e7d3f0fbce0a51a78c2549b0977bd /Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution
parent	Infrastructure for objective functions (diff)
download	VIATRA-Generator-c1f185fd8fc2c3dfc123d9271726c588963c7c01.tar.gz VIATRA-Generator-c1f185fd8fc2c3dfc123d9271726c588963c7c01.tar.zst VIATRA-Generator-c1f185fd8fc2c3dfc123d9271726c588963c7c01.zip

diff --git a/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/GenerationTaskExecutor.xtend b/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/GenerationTaskExecutor.xtend index 35ffaf65..8ea674d3 100644 --- a/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/GenerationTaskExecutor.xtend +++ b/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/GenerationTaskExecutor.xtend
@@ -133,7 +133,9 @@ class GenerationTaskExecutor {
133	// 5. create a solver and a configuration	133	// 5. create a solver and a configuration
134	// 5.1 initialize	134	// 5.1 initialize
135	val solver = solverLoader.loadSolver(task.solver,configurationMap)	135	val solver = solverLoader.loadSolver(task.solver,configurationMap)
136	val solverConfig = solverLoader.loadSolverConfig(task.solver,configurationMap,console)	136	val objectiveSpecification = scriptExecutor.getObjectiveSpecification(task.objectives)
		137	val objectiveEntries = objectiveSpecification?.entries ?: emptyList
		138	val solverConfig = solverLoader.loadSolverConfig(task.solver,configurationMap,objectiveEntries,console)
137		139
138		140
139	// 5.2 set values that defined directly	141	// 5.2 set values that defined directly


diff --git a/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/ScriptExecutor.xtend b/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/ScriptExecutor.xtend index 0512a5ee..25036df6 100644 --- a/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/ScriptExecutor.xtend +++ b/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/ScriptExecutor.xtend
@@ -30,6 +30,8 @@ import org.eclipse.core.runtime.Status
30	import org.eclipse.core.runtime.jobs.Job	30	import org.eclipse.core.runtime.jobs.Job
31	import org.eclipse.emf.common.util.URI	31	import org.eclipse.emf.common.util.URI
32	import org.eclipse.xtend.lib.annotations.FinalFieldsConstructor	32	import org.eclipse.xtend.lib.annotations.FinalFieldsConstructor
		33	import hu.bme.mit.inf.dslreasoner.application.applicationConfiguration.ObjectiveSpecification
		34	import hu.bme.mit.inf.dslreasoner.application.applicationConfiguration.ObjectiveReference
33		35
34	@FinalFieldsConstructor	36	@FinalFieldsConstructor
35	class ScriptExecutor {	37	class ScriptExecutor {
@@ -40,7 +42,7 @@ class ScriptExecutor {
40	/**	42	/**
41	* Executes a script	43	* Executes a script
42	*/	44	*/
43	public def executeScript(URI uri) {	45	def executeScript(URI uri) {
44	val job = new Job('''Model Generation: «uri.lastSegment»''') {	46	val job = new Job('''Model Generation: «uri.lastSegment»''') {
45	override protected run(IProgressMonitor monitor) {	47	override protected run(IProgressMonitor monitor) {
46	try{	48	try{
@@ -57,7 +59,7 @@ class ScriptExecutor {
57	job.schedule();	59	job.schedule();
58	}	60	}
59		61
60	public def executeScript(ConfigurationScript script, IProgressMonitor monitor) {	62	def executeScript(ConfigurationScript script, IProgressMonitor monitor) {
61	script.activateAllEPackageReferences	63	script.activateAllEPackageReferences
62	val tasks = script.commands.filter(Task)	64	val tasks = script.commands.filter(Task)
63		65
@@ -94,12 +96,12 @@ class ScriptExecutor {
94	// }	96	// }
95	}	97	}
96		98
97	def public dispatch execute(GenerationTask task, IProgressMonitor monitor) {	99	def dispatch void execute(GenerationTask task, IProgressMonitor monitor) {
98	val generationTaskExecutor = new GenerationTaskExecutor	100	val generationTaskExecutor = new GenerationTaskExecutor
99	generationTaskExecutor.executeGenerationTask(task,this,scriptConsoleFactory,monitor)	101	generationTaskExecutor.executeGenerationTask(task,this,scriptConsoleFactory,monitor)
100	}	102	}
101		103
102	def public dispatch execute(Task task, IProgressMonitor monitor) {	104	def dispatch void execute(Task task, IProgressMonitor monitor) {
103	throw new IllegalArgumentException('''Unsupported task type: «task.class.simpleName»!''')	105	throw new IllegalArgumentException('''Unsupported task type: «task.class.simpleName»!''')
104	}	106	}
105		107
@@ -174,6 +176,16 @@ class ScriptExecutor {
174	null	176	null
175	}	177	}
176		178
		179	def dispatch getObjectiveSpecification(ObjectiveSpecification config) {
		180	config
		181	}
		182	def dispatch getObjectiveSpecification(ObjectiveReference config) {
		183	config.referred.specification
		184	}
		185	def dispatch getObjectiveSpecification(Void config) {
		186	null
		187	}
		188
177	def dispatch getConfiguration(ConfigSpecification config) {	189	def dispatch getConfiguration(ConfigSpecification config) {
178	config	190	config
179	}	191	}


diff --git a/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/SolverLoader.xtend b/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/SolverLoader.xtend index 9eceef5f..f769d46f 100644 --- a/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/SolverLoader.xtend +++ b/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/SolverLoader.xtend
@@ -1,44 +1,47 @@
1	package hu.bme.mit.inf.dslreasoner.application.execution	1	package hu.bme.mit.inf.dslreasoner.application.execution
2		2
3	import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.AlloyBackendSolver
4	import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.AlloySolver	3	import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.AlloySolver
5	import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.AlloySolverConfiguration	4	import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.AlloySolverConfiguration
		5	import hu.bme.mit.inf.dslreasoner.application.applicationConfiguration.CostObjectiveFunction
		6	import hu.bme.mit.inf.dslreasoner.application.applicationConfiguration.ObjectiveEntry
		7	import hu.bme.mit.inf.dslreasoner.application.applicationConfiguration.OptimizationEntry
6	import hu.bme.mit.inf.dslreasoner.application.applicationConfiguration.Solver	8	import hu.bme.mit.inf.dslreasoner.application.applicationConfiguration.Solver
		9	import hu.bme.mit.inf.dslreasoner.application.applicationConfiguration.ThresholdEntry
7	import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration	10	import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration
8	import hu.bme.mit.inf.dslreasoner.smt.reasoner.SMTSolver	11	import hu.bme.mit.inf.dslreasoner.smt.reasoner.SMTSolver
9	import hu.bme.mit.inf.dslreasoner.smt.reasoner.SmtSolverConfiguration	12	import hu.bme.mit.inf.dslreasoner.smt.reasoner.SmtSolverConfiguration
		13	import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.CostObjectiveConfiguration
		14	import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.CostObjectiveElementConfiguration
		15	import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.DiversityDescriptor
10	import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ViatraReasoner	16	import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ViatraReasoner
11	import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ViatraReasonerConfiguration	17	import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ViatraReasonerConfiguration
		18	import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization.ObjectiveKind
		19	import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization.ObjectiveThreshold
		20	import hu.bme.mit.inf.dslreasoner.visualisation.pi2graphviz.GraphvizVisualiser
		21	import java.util.List
12	import java.util.Map	22	import java.util.Map
13	import java.util.Optional	23	import java.util.Optional
		24	import org.eclipse.viatra.query.patternlanguage.emf.vql.PatternModel
		25	import org.eclipse.xtext.EcoreUtil2
14	import org.eclipse.xtext.xbase.lib.Functions.Function1	26	import org.eclipse.xtext.xbase.lib.Functions.Function1
15	import hu.bme.mit.inf.dslreasoner.visualisation.pi2graphviz.GraphvizVisualiser
16	import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.DiversityDescriptor
17		27
18	class SolverLoader {	28	class SolverLoader {
19	def loadSolver(Solver solver, Map<String, String> config) {	29	def loadSolver(Solver solver, Map<String, String> config) {
20	switch(solver) {	30	switch (solver) {
21	case ALLOY_SOLVER: return new AlloySolver	31	case ALLOY_SOLVER: return new AlloySolver
22	case SMT_SOLVER: return new SMTSolver	32	case SMT_SOLVER: return new SMTSolver
23	case VIATRA_SOLVER: return new ViatraReasoner	33	case VIATRA_SOLVER: return new ViatraReasoner
24	}	34	}
25	}	35	}
26		36
27		37	private def <Type> Optional<Type> getAsType(Map<String, String> config, String key, ScriptConsole console,
28		38	Function1<String, Type> parser, Class<Type> requestedType) {
29	private def <Type> Optional<Type> getAsType(	39	if (config.containsKey(key)) {
30	Map<String, String> config,
31	String key,
32	ScriptConsole console,
33	Function1<String,Type> parser,
34	Class<Type> requestedType)
35	{
36	if(config.containsKey(key)) {
37	val stringValue = config.get(key)	40	val stringValue = config.get(key)
38	try{	41	try {
39	val parsedValue = parser.apply(stringValue)	42	val parsedValue = parser.apply(stringValue)
40	return Optional.of(parsedValue)	43	return Optional.of(parsedValue)
41	} catch(Exception e) {	44	} catch (Exception e) {
42	console.writeError('''Unable to parse configuration value for "«key»" to «requestedType.simpleName»!''')	45	console.writeError('''Unable to parse configuration value for "«key»" to «requestedType.simpleName»!''')
43	return Optional::empty	46	return Optional::empty
44	}	47	}
@@ -46,60 +49,131 @@ class SolverLoader {
46	return Optional::empty	49	return Optional::empty
47	}	50	}
48	}	51	}
		52
49	private def getAsInteger(Map<String, String> config, String key, ScriptConsole console) {	53	private def getAsInteger(Map<String, String> config, String key, ScriptConsole console) {
50	return getAsType(config,key,console,[x\|Integer.parseInt(x)],Integer)	54	return getAsType(config, key, console, [x\|Integer.parseInt(x)], Integer)
51	}	55	}
		56
52	private def getAsBoolean(Map<String, String> config, String key, ScriptConsole console) {	57	private def getAsBoolean(Map<String, String> config, String key, ScriptConsole console) {
53	return getAsType(config,key,console,[x\|Boolean.parseBoolean(x)],Boolean)	58	return getAsType(config, key, console, [x\|Boolean.parseBoolean(x)], Boolean)
54	}	59	}
		60
55	private def getAsDouble(Map<String, String> config, String key, ScriptConsole console) {	61	private def getAsDouble(Map<String, String> config, String key, ScriptConsole console) {
56	return getAsType(config,key,console,[x\|Double.parseDouble(x)],Double)	62	return getAsType(config, key, console, [x\|Double.parseDouble(x)], Double)
57	}	63	}
58		64
59	def loadSolverConfig(	65	def loadSolverConfig(Solver solver, Map<String, String> config, List<ObjectiveEntry> objectiveEntries,
60	Solver solver,	66	ScriptConsole console) {
61	Map<String, String> config,	67	switch (solver) {
62	ScriptConsole console)	68	case ALLOY_SOLVER: {
63	{	69	if (!objectiveEntries.empty) {
64	if(solver === Solver::ALLOY_SOLVER) {	70	throw new IllegalArgumentException("Objectives are not supported by Alloy.")
65	return new AlloySolverConfiguration => [c\|	71	}
66	config.getAsInteger("symmetry",console)	72	val c = new SmtSolverConfiguration
67	.ifPresent[c.symmetry = it]	73	config.getAsBoolean("fixRandomSeed", console).ifPresent[c.fixRandomSeed = it]
68	config.getAsType("solver",console,[x\|AlloyBackendSolver::valueOf(x)],AlloyBackendSolver)	74	config.getAsType("path", console, [it], String).ifPresent[c.solverPath = it]
69	.ifPresent[c.solver = it]	75	c
70	]	76	}
71	} else if(solver === Solver::SMT_SOLVER) {	77	case SMT_SOLVER: {
72	return new SmtSolverConfiguration => [c\|	78	if (!objectiveEntries.empty) {
73	config.getAsBoolean("fixRandomSeed",console).ifPresent[c.fixRandomSeed = it]	79	throw new IllegalArgumentException("Objectives are not supported by Z3.")
74	config.getAsType("path",console,[it],String).ifPresent[c.solverPath = it]	80	}
75	]	81	val c = new SmtSolverConfiguration
76	} else if(solver === Solver::VIATRA_SOLVER) {	82	config.getAsBoolean("fixRandomSeed", console).ifPresent[c.fixRandomSeed = it]
77	return new ViatraReasonerConfiguration => [c\|	83	config.getAsType("path", console, [it], String).ifPresent[c.solverPath = it]
		84	c
		85	}
		86	case VIATRA_SOLVER: {
		87	val c = new ViatraReasonerConfiguration
78	c.debugConfiguration.partialInterpretatioVisualiser = new GraphvizVisualiser	88	c.debugConfiguration.partialInterpretatioVisualiser = new GraphvizVisualiser
79	if(config.containsKey("diversity-range")) {	89	if (config.containsKey("diversity-range")) {
80	val stringValue = config.get("diversity-range")	90	val stringValue = config.get("diversity-range")
81	try{	91	try {
82	val range = Integer.parseInt(stringValue)	92	val range = Integer.parseInt(stringValue)
83	c.diversityRequirement = new DiversityDescriptor => [	93	c.diversityRequirement = new DiversityDescriptor => [
84	it.ensureDiversity = true	94	it.ensureDiversity = true
85	it.range = range	95	it.range = range
86	]	96	]
87	} catch (NumberFormatException e) {console.writeError('''Malformed number format: «e.message»''')}	97	} catch (NumberFormatException e) {
		98	console.writeError('''Malformed number format: «e.message»''')
		99	}
88	}	100	}
89	]	101	for (objectiveEntry : objectiveEntries) {
90	} else {	102	val costObjectiveConfig = new CostObjectiveConfiguration
91	throw new UnsupportedOperationException('''Unknown solver: «solver»''')	103	switch (objectiveEntry) {
		104	OptimizationEntry: {
		105	costObjectiveConfig.findExtremum = true
		106	costObjectiveConfig.kind = switch (direction : objectiveEntry.direction) {
		107	case MAXIMIZE:
		108	ObjectiveKind.HIGHER_IS_BETTER
		109	case MINIMIZE:
		110	ObjectiveKind.LOWER_IS_BETTER
		111	default:
		112	throw new IllegalArgumentException("Unknown direction: " + direction)
		113	}
		114	costObjectiveConfig.threshold = ObjectiveThreshold.NO_THRESHOLD
		115	}
		116	ThresholdEntry: {
		117	costObjectiveConfig.findExtremum = false
		118	val threshold = objectiveEntry.threshold.doubleValue
		119	switch (operator : objectiveEntry.operator) {
		120	case LESS: {
		121	costObjectiveConfig.kind = ObjectiveKind.LOWER_IS_BETTER
		122	costObjectiveConfig.threshold = new ObjectiveThreshold.Exclusive(threshold)
		123	}
		124	case GREATER: {
		125	costObjectiveConfig.kind = ObjectiveKind.HIGHER_IS_BETTER
		126	costObjectiveConfig.threshold = new ObjectiveThreshold.Exclusive(threshold)
		127	}
		128	case LESS_EQUALS: {
		129	costObjectiveConfig.kind = ObjectiveKind.LOWER_IS_BETTER
		130	costObjectiveConfig.threshold = new ObjectiveThreshold.Exclusive(threshold)
		131	}
		132	case GREATER_EQUALS: {
		133	costObjectiveConfig.kind = ObjectiveKind.HIGHER_IS_BETTER
		134	costObjectiveConfig.threshold = new ObjectiveThreshold.Exclusive(threshold)
		135	}
		136	default:
		137	throw new IllegalArgumentException("Unknown operator: " + operator)
		138	}
		139	}
		140	}
		141	val function = objectiveEntry.function
		142	if (function instanceof CostObjectiveFunction) {
		143	for (costEntry : function.entries) {
		144	val element = new CostObjectiveElementConfiguration
		145	val pattern = costEntry.patternElement.pattern
		146	val packageName = costEntry.patternElement.package?.packageName ?:
		147	EcoreUtil2.getContainerOfType(pattern, PatternModel)?.packageName
		148	element.patternQualifiedName = if (packageName.nullOrEmpty) {
		149	pattern.name
		150	} else {
		151	packageName + "." + pattern.name
		152	}
		153	costObjectiveConfig.elements += element
		154	}
		155	} else {
		156	throw new IllegalArgumentException("Only cost objectives are supported by VIATRA.")
		157	}
		158	c.costObjectives += costObjectiveConfig
		159	}
		160	c
		161	}
		162	default:
		163	throw new UnsupportedOperationException('''Unknown solver: «solver»''')
92	}	164	}
93	}	165	}
94		166
95	def dispatch void setRunIndex(AlloySolverConfiguration config, Map<String, String> parameters, int runIndex, ScriptConsole console) {	167	def dispatch void setRunIndex(AlloySolverConfiguration config, Map<String, String> parameters, int runIndex,
96	parameters.getAsBoolean("randomize",console).ifPresent[	168	ScriptConsole console) {
97	if(it) {	169	parameters.getAsBoolean("randomize", console).ifPresent [
98	config.randomise = runIndex-1	170	if (it) {
		171	config.randomise = runIndex - 1
99	}	172	}
100	]	173	]
101	}	174	}
102	def dispatch void setRunIndex(LogicSolverConfiguration config, Map<String, String> parameters, int runIndex, ScriptConsole console) {	175
103		176	def dispatch void setRunIndex(LogicSolverConfiguration config, Map<String, String> parameters, int runIndex,
		177	ScriptConsole console) {
104	}	178	}
105	} \ No newline at end of file	179	}