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 | 77 |
1 files changed, 68 insertions, 9 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 dcd89981..9ae1ba6b 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,13 +1,17 @@ | |||
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.dslreasoner.application.applicationConfiguration.Solver | 3 | import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.AlloyBackendSolver |
4 | import java.util.Map | ||
5 | import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.AlloySolver | 4 | import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.AlloySolver |
6 | import hu.bme.mit.inf.dslreasoner.smt.reasoner.SMTSolver | ||
7 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ViatraReasoner | ||
8 | import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.AlloySolverConfiguration | 5 | import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.AlloySolverConfiguration |
6 | import hu.bme.mit.inf.dslreasoner.application.applicationConfiguration.Solver | ||
7 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration | ||
8 | import hu.bme.mit.inf.dslreasoner.smt.reasoner.SMTSolver | ||
9 | import hu.bme.mit.inf.dslreasoner.smt.reasoner.SmtSolverConfiguration | 9 | import hu.bme.mit.inf.dslreasoner.smt.reasoner.SmtSolverConfiguration |
10 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ViatraReasoner | ||
10 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ViatraReasonerConfiguration | 11 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ViatraReasonerConfiguration |
12 | import java.util.Map | ||
13 | import java.util.Optional | ||
14 | import org.eclipse.xtext.xbase.lib.Functions.Function1 | ||
11 | 15 | ||
12 | class SolverLoader { | 16 | class SolverLoader { |
13 | def loadSolver(Solver solver, Map<String, String> config) { | 17 | def loadSolver(Solver solver, Map<String, String> config) { |
@@ -18,11 +22,66 @@ class SolverLoader { | |||
18 | } | 22 | } |
19 | } | 23 | } |
20 | 24 | ||
21 | def loadSolverConfig(Solver solver, Map<String, String> config) { | 25 | |
22 | switch(solver) { | 26 | |
23 | case ALLOY_SOLVER: return new AlloySolverConfiguration | 27 | private def <Type> Optional<Type> getAsType( |
24 | case SMT_SOLVER: return new SmtSolverConfiguration | 28 | Map<String, String> config, |
25 | case VIATRA_SOLVER: return new ViatraReasonerConfiguration | 29 | String key, |
30 | ScriptConsole console, | ||
31 | Function1<String,Type> parser, | ||
32 | Class<Type> requestedType) | ||
33 | { | ||
34 | if(config.containsKey(key)) { | ||
35 | val stringValue = config.get(key) | ||
36 | try{ | ||
37 | val parsedValue = parser.apply(stringValue) | ||
38 | return Optional.of(parsedValue) | ||
39 | } catch(Exception e) { | ||
40 | console.writeError('''Unable to parse configuration value for "«key»" to «requestedType.simpleName»!''') | ||
41 | return Optional::empty | ||
42 | } | ||
43 | } else { | ||
44 | return Optional::empty | ||
45 | } | ||
46 | } | ||
47 | private def getAsInteger(Map<String, String> config, String key, ScriptConsole console) { | ||
48 | return getAsType(config,key,console,[x|Integer.parseInt(x)],Integer) | ||
49 | } | ||
50 | private def getAsBoolean(Map<String, String> config, String key, ScriptConsole console) { | ||
51 | return getAsType(config,key,console,[x|Boolean.parseBoolean(x)],Boolean) | ||
52 | } | ||
53 | private def getAsDouble(Map<String, String> config, String key, ScriptConsole console) { | ||
54 | return getAsType(config,key,console,[x|Double.parseDouble(x)],Double) | ||
55 | } | ||
56 | |||
57 | def loadSolverConfig( | ||
58 | Solver solver, | ||
59 | Map<String, String> config, | ||
60 | ScriptConsole console) | ||
61 | { | ||
62 | if(solver === Solver::ALLOY_SOLVER) { | ||
63 | return new AlloySolverConfiguration => [c| | ||
64 | config.getAsInteger("symmetry",console) | ||
65 | .ifPresent[c.symmetry = it] | ||
66 | config.getAsType("solver",console,[x|AlloyBackendSolver::valueOf(x)],AlloyBackendSolver) | ||
67 | .ifPresent[c.solver = it] | ||
68 | ] | ||
69 | } else if(solver === Solver::SMT_SOLVER) { | ||
70 | return new SmtSolverConfiguration => [c| | ||
71 | config.getAsBoolean("fixRandomSeed",console).ifPresent[c.fixRandomSeed = it] | ||
72 | ] | ||
73 | } else if(solver === Solver::VIATRA_SOLVER) { | ||
74 | return new ViatraReasonerConfiguration => [c| | ||
75 | ] | ||
76 | } else { | ||
77 | throw new UnsupportedOperationException('''Unknown solver: «solver»''') | ||
26 | } | 78 | } |
27 | } | 79 | } |
80 | |||
81 | def dispatch void setRunIndex(AlloySolverConfiguration config, Map<String, String> parameters, int runIndex, ScriptConsole console) { | ||
82 | parameters.getAsBoolean("randomise",console).ifPresent[config.randomise = runIndex] | ||
83 | } | ||
84 | def dispatch void setRunIndex(LogicSolverConfiguration config, Map<String, String> parameters, int runIndex, ScriptConsole console) { | ||
85 | |||
86 | } | ||
28 | } \ No newline at end of file | 87 | } \ No newline at end of file |