diff options
author | Kristóf Marussy <marussy@mit.bme.hu> | 2020-06-25 19:55:10 +0200 |
---|---|---|
committer | Kristóf Marussy <marussy@mit.bme.hu> | 2020-06-25 19:55:10 +0200 |
commit | c3a6d4b9cf3657070d180aa65ddbf0459e880329 (patch) | |
tree | 780c4fc61578dcb309af53fb0c164c7627e51676 /Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/SolverLoader.xtend | |
parent | New configuration language parser WIP (diff) | |
parent | Scope unsat benchmarks (diff) | |
download | VIATRA-Generator-c3a6d4b9cf3657070d180aa65ddbf0459e880329.tar.gz VIATRA-Generator-c3a6d4b9cf3657070d180aa65ddbf0459e880329.tar.zst VIATRA-Generator-c3a6d4b9cf3657070d180aa65ddbf0459e880329.zip |
Merge branch 'kris'
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.xtend | 190 |
1 files changed, 129 insertions, 61 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 2fe69a47..b1be56cb 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,45 +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 | import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder.SolverConfiguration | ||
18 | 27 | ||
19 | class SolverLoader { | 28 | class SolverLoader { |
20 | def loadSolver(Solver solver, Map<String, String> config) { | 29 | def loadSolver(Solver solver, Map<String, String> config) { |
21 | switch(solver) { | 30 | switch (solver) { |
22 | case ALLOY_SOLVER: return new AlloySolver | 31 | case ALLOY_SOLVER: return new AlloySolver |
23 | case SMT_SOLVER: return new SMTSolver | 32 | case SMT_SOLVER: return new SMTSolver |
24 | case VIATRA_SOLVER: return new ViatraReasoner | 33 | case VIATRA_SOLVER: return new ViatraReasoner |
25 | } | 34 | } |
26 | } | 35 | } |
27 | 36 | ||
28 | 37 | private def <Type> Optional<Type> getAsType(Map<String, String> config, String key, ScriptConsole console, | |
29 | 38 | Function1<String, Type> parser, Class<Type> requestedType) { | |
30 | private def <Type> Optional<Type> getAsType( | 39 | if (config.containsKey(key)) { |
31 | Map<String, String> config, | ||
32 | String key, | ||
33 | ScriptConsole console, | ||
34 | Function1<String,Type> parser, | ||
35 | Class<Type> requestedType) | ||
36 | { | ||
37 | if(config.containsKey(key)) { | ||
38 | val stringValue = config.get(key) | 40 | val stringValue = config.get(key) |
39 | try{ | 41 | try { |
40 | val parsedValue = parser.apply(stringValue) | 42 | val parsedValue = parser.apply(stringValue) |
41 | return Optional.of(parsedValue) | 43 | return Optional.of(parsedValue) |
42 | } catch(Exception e) { | 44 | } catch (Exception e) { |
43 | 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»!''') |
44 | return Optional::empty | 46 | return Optional::empty |
45 | } | 47 | } |
@@ -47,45 +49,54 @@ class SolverLoader { | |||
47 | return Optional::empty | 49 | return Optional::empty |
48 | } | 50 | } |
49 | } | 51 | } |
52 | |||
50 | private def getAsInteger(Map<String, String> config, String key, ScriptConsole console) { | 53 | private def getAsInteger(Map<String, String> config, String key, ScriptConsole console) { |
51 | return getAsType(config,key,console,[x|Integer.parseInt(x)],Integer) | 54 | return getAsType(config, key, console, [x|Integer.parseInt(x)], Integer) |
52 | } | 55 | } |
56 | |||
53 | private def getAsBoolean(Map<String, String> config, String key, ScriptConsole console) { | 57 | private def getAsBoolean(Map<String, String> config, String key, ScriptConsole console) { |
54 | return getAsType(config,key,console,[x|Boolean.parseBoolean(x)],Boolean) | 58 | return getAsType(config, key, console, [x|Boolean.parseBoolean(x)], Boolean) |
55 | } | 59 | } |
60 | |||
56 | private def getAsDouble(Map<String, String> config, String key, ScriptConsole console) { | 61 | private def getAsDouble(Map<String, String> config, String key, ScriptConsole console) { |
57 | return getAsType(config,key,console,[x|Double.parseDouble(x)],Double) | 62 | return getAsType(config, key, console, [x|Double.parseDouble(x)], Double) |
58 | } | 63 | } |
59 | 64 | ||
60 | def loadSolverConfig( | 65 | def loadSolverConfig(Solver solver, Map<String, String> config, List<ObjectiveEntry> objectiveEntries, |
61 | Solver solver, | 66 | ScriptConsole console) { |
62 | Map<String, String> config, | 67 | switch (solver) { |
63 | ScriptConsole console) | 68 | case ALLOY_SOLVER: { |
64 | { | 69 | if (!objectiveEntries.empty) { |
65 | if(solver === Solver::ALLOY_SOLVER) { | 70 | throw new IllegalArgumentException("Objectives are not supported by Alloy.") |
66 | return new AlloySolverConfiguration => [c| | 71 | } |
67 | config.getAsInteger("symmetry",console) | 72 | val c = new SmtSolverConfiguration |
68 | .ifPresent[c.symmetry = it] | 73 | config.getAsBoolean("fixRandomSeed", console).ifPresent[c.fixRandomSeed = it] |
69 | config.getAsType("solver",console,[x|AlloyBackendSolver::valueOf(x)],AlloyBackendSolver) | 74 | config.getAsType("path", console, [it], String).ifPresent[c.solverPath = it] |
70 | .ifPresent[c.solver = it] | 75 | c |
71 | ] | 76 | } |
72 | } else if(solver === Solver::SMT_SOLVER) { | 77 | case SMT_SOLVER: { |
73 | return new SmtSolverConfiguration => [c| | 78 | if (!objectiveEntries.empty) { |
74 | config.getAsBoolean("fixRandomSeed",console).ifPresent[c.fixRandomSeed = it] | 79 | throw new IllegalArgumentException("Objectives are not supported by Z3.") |
75 | config.getAsType("path",console,[it],String).ifPresent[c.solverPath = it] | 80 | } |
76 | ] | 81 | val c = new SmtSolverConfiguration |
77 | } else if(solver === Solver::VIATRA_SOLVER) { | 82 | config.getAsBoolean("fixRandomSeed", console).ifPresent[c.fixRandomSeed = it] |
78 | return new ViatraReasonerConfiguration => [c| | 83 | config.getAsType("path", console, [it], String).ifPresent[c.solverPath = it] |
79 | c.debugCongiguration.partialInterpretatioVisualiser = new GraphvizVisualiser | 84 | c |
80 | if(config.containsKey("diversity-range")) { | 85 | } |
86 | case VIATRA_SOLVER: { | ||
87 | val c = new ViatraReasonerConfiguration | ||
88 | c.debugConfiguration.partialInterpretatioVisualiser = new GraphvizVisualiser | ||
89 | if (config.containsKey("diversity-range")) { | ||
81 | val stringValue = config.get("diversity-range") | 90 | val stringValue = config.get("diversity-range") |
82 | try{ | 91 | try { |
83 | val range = Integer.parseInt(stringValue) | 92 | val range = Integer.parseInt(stringValue) |
84 | c.diversityRequirement = new DiversityDescriptor => [ | 93 | c.diversityRequirement = new DiversityDescriptor => [ |
85 | it.ensureDiversity = true | 94 | it.ensureDiversity = true |
86 | it.range = range | 95 | it.range = range |
87 | ] | 96 | ] |
88 | } catch (NumberFormatException e) {console.writeError('''Malformed number format: «e.message»''')} | 97 | } catch (NumberFormatException e) { |
98 | console.writeError('''Malformed number format: «e.message»''') | ||
99 | } | ||
89 | } | 100 | } |
90 | if(config.containsKey("numeric-solver-at-end")) { | 101 | if(config.containsKey("numeric-solver-at-end")) { |
91 | val stringValue = config.get("numeric-solver-at-end") | 102 | val stringValue = config.get("numeric-solver-at-end") |
@@ -124,26 +135,83 @@ class SolverLoader { | |||
124 | c.unfinishedWFWeight = Integer.parseInt(stringValue) | 135 | c.unfinishedWFWeight = Integer.parseInt(stringValue) |
125 | } catch(Exception e) {} | 136 | } catch(Exception e) {} |
126 | } | 137 | } |
127 | if(config.containsKey("fitness-objectCreationCosts")) { | 138 | for (objectiveEntry : objectiveEntries) { |
128 | val stringValue = config.get("fitness-objectCreationCosts") | 139 | val costObjectiveConfig = new CostObjectiveConfiguration |
129 | try { | 140 | switch (objectiveEntry) { |
130 | c.calculateObjectCreationCosts = Boolean.parseBoolean(stringValue) | 141 | OptimizationEntry: { |
131 | } catch(Exception e) {} | 142 | costObjectiveConfig.findExtremum = true |
143 | costObjectiveConfig.kind = switch (direction : objectiveEntry.direction) { | ||
144 | case MAXIMIZE: | ||
145 | ObjectiveKind.HIGHER_IS_BETTER | ||
146 | case MINIMIZE: | ||
147 | ObjectiveKind.LOWER_IS_BETTER | ||
148 | default: | ||
149 | throw new IllegalArgumentException("Unknown direction: " + direction) | ||
150 | } | ||
151 | costObjectiveConfig.threshold = ObjectiveThreshold.NO_THRESHOLD | ||
152 | } | ||
153 | ThresholdEntry: { | ||
154 | costObjectiveConfig.findExtremum = false | ||
155 | val threshold = objectiveEntry.threshold.doubleValue | ||
156 | switch (operator : objectiveEntry.operator) { | ||
157 | case LESS: { | ||
158 | costObjectiveConfig.kind = ObjectiveKind.LOWER_IS_BETTER | ||
159 | costObjectiveConfig.threshold = new ObjectiveThreshold.Exclusive(threshold) | ||
160 | } | ||
161 | case GREATER: { | ||
162 | costObjectiveConfig.kind = ObjectiveKind.HIGHER_IS_BETTER | ||
163 | costObjectiveConfig.threshold = new ObjectiveThreshold.Exclusive(threshold) | ||
164 | } | ||
165 | case LESS_EQUALS: { | ||
166 | costObjectiveConfig.kind = ObjectiveKind.LOWER_IS_BETTER | ||
167 | costObjectiveConfig.threshold = new ObjectiveThreshold.Exclusive(threshold) | ||
168 | } | ||
169 | case GREATER_EQUALS: { | ||
170 | costObjectiveConfig.kind = ObjectiveKind.HIGHER_IS_BETTER | ||
171 | costObjectiveConfig.threshold = new ObjectiveThreshold.Exclusive(threshold) | ||
172 | } | ||
173 | default: | ||
174 | throw new IllegalArgumentException("Unknown operator: " + operator) | ||
175 | } | ||
176 | } | ||
177 | } | ||
178 | val function = objectiveEntry.function | ||
179 | if (function instanceof CostObjectiveFunction) { | ||
180 | for (costEntry : function.entries) { | ||
181 | val element = new CostObjectiveElementConfiguration | ||
182 | val pattern = costEntry.patternElement.pattern | ||
183 | val packageName = costEntry.patternElement.package?.packageName ?: | ||
184 | EcoreUtil2.getContainerOfType(pattern, PatternModel)?.packageName | ||
185 | element.patternQualifiedName = if (packageName.nullOrEmpty) { | ||
186 | pattern.name | ||
187 | } else { | ||
188 | packageName + "." + pattern.name | ||
189 | } | ||
190 | element.weight = costEntry.weight | ||
191 | costObjectiveConfig.elements += element | ||
192 | } | ||
193 | } else { | ||
194 | throw new IllegalArgumentException("Only cost objectives are supported by VIATRA.") | ||
195 | } | ||
196 | c.costObjectives += costObjectiveConfig | ||
132 | } | 197 | } |
133 | ] | 198 | c |
134 | } else { | 199 | } |
135 | throw new UnsupportedOperationException('''Unknown solver: «solver»''') | 200 | default: |
201 | throw new UnsupportedOperationException('''Unknown solver: «solver»''') | ||
136 | } | 202 | } |
137 | } | 203 | } |
138 | 204 | ||
139 | def dispatch void setRunIndex(AlloySolverConfiguration config, Map<String, String> parameters, int runIndex, ScriptConsole console) { | 205 | def dispatch void setRunIndex(AlloySolverConfiguration config, Map<String, String> parameters, int runIndex, |
140 | parameters.getAsBoolean("randomize",console).ifPresent[ | 206 | ScriptConsole console) { |
141 | if(it) { | 207 | parameters.getAsBoolean("randomize", console).ifPresent [ |
142 | config.randomise = runIndex-1 | 208 | if (it) { |
209 | config.randomise = runIndex - 1 | ||
143 | } | 210 | } |
144 | ] | 211 | ] |
145 | } | 212 | } |
146 | def dispatch void setRunIndex(LogicSolverConfiguration config, Map<String, String> parameters, int runIndex, ScriptConsole console) { | 213 | |
147 | 214 | def dispatch void setRunIndex(LogicSolverConfiguration config, Map<String, String> parameters, int runIndex, | |
215 | ScriptConsole console) { | ||
148 | } | 216 | } |
149 | } \ No newline at end of file | 217 | } |