diff options
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 | 182 |
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 @@ | |||
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 | } |