aboutsummaryrefslogtreecommitdiffstats
path: root/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/SolverLoader.xtend
diff options
context:
space:
mode:
authorLibravatar Kristóf Marussy <kris7topher@gmail.com>2019-04-08 00:58:00 +0200
committerLibravatar Kristóf Marussy <kris7topher@gmail.com>2019-04-08 00:58:00 +0200
commitc1f185fd8fc2c3dfc123d9271726c588963c7c01 (patch)
tree88a5bb94017e7d3f0fbce0a51a78c2549b0977bd /Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/SolverLoader.xtend
parentInfrastructure for objective functions (diff)
downloadVIATRA-Generator-c1f185fd8fc2c3dfc123d9271726c588963c7c01.tar.gz
VIATRA-Generator-c1f185fd8fc2c3dfc123d9271726c588963c7c01.tar.zst
VIATRA-Generator-c1f185fd8fc2c3dfc123d9271726c588963c7c01.zip
Objective POC implementation
Diffstat (limited to 'Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/SolverLoader.xtend')
-rw-r--r--Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/SolverLoader.xtend182
1 files changed, 128 insertions, 54 deletions
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 @@
1package hu.bme.mit.inf.dslreasoner.application.execution 1package hu.bme.mit.inf.dslreasoner.application.execution
2 2
3import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.AlloyBackendSolver
4import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.AlloySolver 3import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.AlloySolver
5import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.AlloySolverConfiguration 4import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.AlloySolverConfiguration
5import hu.bme.mit.inf.dslreasoner.application.applicationConfiguration.CostObjectiveFunction
6import hu.bme.mit.inf.dslreasoner.application.applicationConfiguration.ObjectiveEntry
7import hu.bme.mit.inf.dslreasoner.application.applicationConfiguration.OptimizationEntry
6import hu.bme.mit.inf.dslreasoner.application.applicationConfiguration.Solver 8import hu.bme.mit.inf.dslreasoner.application.applicationConfiguration.Solver
9import hu.bme.mit.inf.dslreasoner.application.applicationConfiguration.ThresholdEntry
7import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration 10import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration
8import hu.bme.mit.inf.dslreasoner.smt.reasoner.SMTSolver 11import hu.bme.mit.inf.dslreasoner.smt.reasoner.SMTSolver
9import hu.bme.mit.inf.dslreasoner.smt.reasoner.SmtSolverConfiguration 12import hu.bme.mit.inf.dslreasoner.smt.reasoner.SmtSolverConfiguration
13import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.CostObjectiveConfiguration
14import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.CostObjectiveElementConfiguration
15import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.DiversityDescriptor
10import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ViatraReasoner 16import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ViatraReasoner
11import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ViatraReasonerConfiguration 17import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ViatraReasonerConfiguration
18import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization.ObjectiveKind
19import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization.ObjectiveThreshold
20import hu.bme.mit.inf.dslreasoner.visualisation.pi2graphviz.GraphvizVisualiser
21import java.util.List
12import java.util.Map 22import java.util.Map
13import java.util.Optional 23import java.util.Optional
24import org.eclipse.viatra.query.patternlanguage.emf.vql.PatternModel
25import org.eclipse.xtext.EcoreUtil2
14import org.eclipse.xtext.xbase.lib.Functions.Function1 26import org.eclipse.xtext.xbase.lib.Functions.Function1
15import hu.bme.mit.inf.dslreasoner.visualisation.pi2graphviz.GraphvizVisualiser
16import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.DiversityDescriptor
17 27
18class SolverLoader { 28class 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}