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:
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.xtend143
1 files changed, 83 insertions, 60 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..b2241fe2 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
@@ -15,31 +15,29 @@ import org.eclipse.xtext.xbase.lib.Functions.Function1
15import hu.bme.mit.inf.dslreasoner.visualisation.pi2graphviz.GraphvizVisualiser 15import hu.bme.mit.inf.dslreasoner.visualisation.pi2graphviz.GraphvizVisualiser
16import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.DiversityDescriptor 16import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.DiversityDescriptor
17import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder.SolverConfiguration 17import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder.SolverConfiguration
18import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolver
19import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration
20import ca.mcgill.ecse.dslreasoner.vampire.reasoner.BackendSolver
21import java.util.prefs.BackingStoreException
18 22
19class SolverLoader { 23class SolverLoader {
20 def loadSolver(Solver solver, Map<String, String> config) { 24 def loadSolver(Solver solver, Map<String, String> config) {
21 switch(solver) { 25 switch (solver) {
22 case ALLOY_SOLVER: return new AlloySolver 26 case ALLOY_SOLVER: return new AlloySolver
23 case SMT_SOLVER: return new SMTSolver 27 case SMT_SOLVER: return new SMTSolver
24 case VIATRA_SOLVER: return new ViatraReasoner 28 case VIATRA_SOLVER: return new ViatraReasoner
29 case TPTP_SOLVER: return new VampireSolver
25 } 30 }
26 } 31 }
27 32
28 33 private def <Type> Optional<Type> getAsType(Map<String, String> config, String key, ScriptConsole console,
29 34 Function1<String, Type> parser, Class<Type> requestedType) {
30 private def <Type> Optional<Type> getAsType( 35 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) 36 val stringValue = config.get(key)
39 try{ 37 try {
40 val parsedValue = parser.apply(stringValue) 38 val parsedValue = parser.apply(stringValue)
41 return Optional.of(parsedValue) 39 return Optional.of(parsedValue)
42 } catch(Exception e) { 40 } catch (Exception e) {
43 console.writeError('''Unable to parse configuration value for "«key»" to «requestedType.simpleName»!''') 41 console.writeError('''Unable to parse configuration value for "«key»" to «requestedType.simpleName»!''')
44 return Optional::empty 42 return Optional::empty
45 } 43 }
@@ -47,103 +45,128 @@ class SolverLoader {
47 return Optional::empty 45 return Optional::empty
48 } 46 }
49 } 47 }
48
50 private def getAsInteger(Map<String, String> config, String key, ScriptConsole console) { 49 private def getAsInteger(Map<String, String> config, String key, ScriptConsole console) {
51 return getAsType(config,key,console,[x|Integer.parseInt(x)],Integer) 50 return getAsType(config, key, console, [x|Integer.parseInt(x)], Integer)
52 } 51 }
52
53 private def getAsBoolean(Map<String, String> config, String key, ScriptConsole console) { 53 private def getAsBoolean(Map<String, String> config, String key, ScriptConsole console) {
54 return getAsType(config,key,console,[x|Boolean.parseBoolean(x)],Boolean) 54 return getAsType(config, key, console, [x|Boolean.parseBoolean(x)], Boolean)
55 } 55 }
56
56 private def getAsDouble(Map<String, String> config, String key, ScriptConsole console) { 57 private def getAsDouble(Map<String, String> config, String key, ScriptConsole console) {
57 return getAsType(config,key,console,[x|Double.parseDouble(x)],Double) 58 return getAsType(config, key, console, [x|Double.parseDouble(x)], Double)
58 } 59 }
59 60
60 def loadSolverConfig( 61 def loadSolverConfig(Solver solver, Map<String, String> config, ScriptConsole console) {
61 Solver solver, 62 if (solver === Solver::ALLOY_SOLVER) {
62 Map<String, String> config, 63 return new AlloySolverConfiguration => [ c |
63 ScriptConsole console) 64 config.getAsInteger("symmetry", console).ifPresent[c.symmetry = it]
64 { 65 config.getAsType("solver", console, [x|AlloyBackendSolver::valueOf(x)], AlloyBackendSolver).ifPresent [
65 if(solver === Solver::ALLOY_SOLVER) { 66 c.solver = it
66 return new AlloySolverConfiguration => [c| 67 ]
67 config.getAsInteger("symmetry",console)
68 .ifPresent[c.symmetry = it]
69 config.getAsType("solver",console,[x|AlloyBackendSolver::valueOf(x)],AlloyBackendSolver)
70 .ifPresent[c.solver = it]
71 ] 68 ]
72 } else if(solver === Solver::SMT_SOLVER) { 69 } else if (solver === Solver::SMT_SOLVER) {
73 return new SmtSolverConfiguration => [c| 70 return new SmtSolverConfiguration => [ c |
74 config.getAsBoolean("fixRandomSeed",console).ifPresent[c.fixRandomSeed = it] 71 config.getAsBoolean("fixRandomSeed", console).ifPresent[c.fixRandomSeed = it]
75 config.getAsType("path",console,[it],String).ifPresent[c.solverPath = it] 72 config.getAsType("path", console, [it], String).ifPresent[c.solverPath = it]
76 ] 73 ]
77 } else if(solver === Solver::VIATRA_SOLVER) { 74 } else if (solver === Solver::TPTP_SOLVER) {
78 return new ViatraReasonerConfiguration => [c| 75 return new VampireSolverConfiguration => [ c |
76 try {
77 val stringValue = config.get("solver")
78 c.solver = switch stringValue {
79 case "cvc4": BackendSolver::CVC4
80 case "vampire": BackendSolver::VAMPIRE
81 case "vampire-local": BackendSolver::LOCVAMP
82 default: throw new Exception
83 }
84 } catch (Exception e) {
85 console.writeError('''Incorrect Solver specification, using default.''')
86 }
87 if (c.solver != BackendSolver::LOCVAMP) c.server = true
88
89 ]
90 } else if (solver === Solver::VIATRA_SOLVER) {
91 return new ViatraReasonerConfiguration => [ c |
79 c.debugCongiguration.partialInterpretatioVisualiser = new GraphvizVisualiser 92 c.debugCongiguration.partialInterpretatioVisualiser = new GraphvizVisualiser
80 if(config.containsKey("diversity-range")) { 93 if (config.containsKey("diversity-range")) {
81 val stringValue = config.get("diversity-range") 94 val stringValue = config.get("diversity-range")
82 try{ 95 try {
83 val range = Integer.parseInt(stringValue) 96 val range = Integer.parseInt(stringValue)
84 c.diversityRequirement = new DiversityDescriptor => [ 97 c.diversityRequirement = new DiversityDescriptor => [
85 it.ensureDiversity = true 98 it.ensureDiversity = true
86 it.range = range 99 it.range = range
87 ] 100 ]
88 } catch (NumberFormatException e) {console.writeError('''Malformed number format: «e.message»''')} 101 } catch (NumberFormatException e) {
102 console.writeError('''Malformed number format: «e.message»''')
103 }
89 } 104 }
90 if(config.containsKey("numeric-solver-at-end")) { 105 if (config.containsKey("numeric-solver-at-end")) {
91 val stringValue = config.get("numeric-solver-at-end") 106 val stringValue = config.get("numeric-solver-at-end")
92 if(stringValue.equals("true")) { 107 if (stringValue.equals("true")) {
93 println("numeric-solver-at-end") 108 println("numeric-solver-at-end")
94 c.runIntermediateNumericalConsistencyChecks = false 109 c.runIntermediateNumericalConsistencyChecks = false
95 } 110 }
96 } 111 }
97 if(config.containsKey("fitness-punishSize")) { 112 if (config.containsKey("fitness-punishSize")) {
98 val stringValue = config.get("fitness-punishSize") 113 val stringValue = config.get("fitness-punishSize")
99 try { 114 try {
100 c.punishSize = Boolean.parseBoolean(stringValue) 115 c.punishSize = Boolean.parseBoolean(stringValue)
101 } catch(Exception e) {} 116 } catch (Exception e) {
117 }
102 } 118 }
103 if(config.containsKey("fitness-scope")) { 119 if (config.containsKey("fitness-scope")) {
104 val stringValue = config.get("fitness-scope") 120 val stringValue = config.get("fitness-scope")
105 try { 121 try {
106 c.scopeWeight = Integer.parseInt(stringValue) 122 c.scopeWeight = Integer.parseInt(stringValue)
107 } catch(Exception e) {} 123 } catch (Exception e) {
124 }
108 } 125 }
109 if(config.containsKey("fitness-missing-containent")) { 126 if (config.containsKey("fitness-missing-containent")) {
110 val stringValue = config.get("fitness-missing-containent") 127 val stringValue = config.get("fitness-missing-containent")
111 try { 128 try {
112 c.conaintmentWeight = Integer.parseInt(stringValue) 129 c.conaintmentWeight = Integer.parseInt(stringValue)
113 } catch(Exception e) {} 130 } catch (Exception e) {
131 }
114 } 132 }
115 if(config.containsKey("fitness-missing-noncontainent")) { 133 if (config.containsKey("fitness-missing-noncontainent")) {
116 val stringValue = config.get("fitness-missing-noncontainent") 134 val stringValue = config.get("fitness-missing-noncontainent")
117 try { 135 try {
118 c.nonContainmentWeight = Integer.parseInt(stringValue) 136 c.nonContainmentWeight = Integer.parseInt(stringValue)
119 } catch(Exception e) {} 137 } catch (Exception e) {
138 }
120 } 139 }
121 if(config.containsKey("fitness-missing-wf")) { 140 if (config.containsKey("fitness-missing-wf")) {
122 val stringValue = config.get("fitness-missing-wf") 141 val stringValue = config.get("fitness-missing-wf")
123 try { 142 try {
124 c.unfinishedWFWeight = Integer.parseInt(stringValue) 143 c.unfinishedWFWeight = Integer.parseInt(stringValue)
125 } catch(Exception e) {} 144 } catch (Exception e) {
145 }
126 } 146 }
127 if(config.containsKey("fitness-objectCreationCosts")) { 147 if (config.containsKey("fitness-objectCreationCosts")) {
128 val stringValue = config.get("fitness-objectCreationCosts") 148 val stringValue = config.get("fitness-objectCreationCosts")
129 try { 149 try {
130 c.calculateObjectCreationCosts = Boolean.parseBoolean(stringValue) 150 c.calculateObjectCreationCosts = Boolean.parseBoolean(stringValue)
131 } catch(Exception e) {} 151 } catch (Exception e) {
152 }
132 } 153 }
133 ] 154 ]
134 } else { 155 } else {
135 throw new UnsupportedOperationException('''Unknown solver: «solver»''') 156 throw new UnsupportedOperationException('''Unknown solver: «solver»''')
136 } 157 }
137 } 158 }
138 159
139 def dispatch void setRunIndex(AlloySolverConfiguration config, Map<String, String> parameters, int runIndex, ScriptConsole console) { 160 def dispatch void setRunIndex(AlloySolverConfiguration config, Map<String, String> parameters, int runIndex,
140 parameters.getAsBoolean("randomize",console).ifPresent[ 161 ScriptConsole console) {
141 if(it) { 162 parameters.getAsBoolean("randomize", console).ifPresent [
142 config.randomise = runIndex-1 163 if (it) {
164 config.randomise = runIndex - 1
143 } 165 }
144 ] 166 ]
145 } 167 }
146 def dispatch void setRunIndex(LogicSolverConfiguration config, Map<String, String> parameters, int runIndex, ScriptConsole console) { 168
147 169 def dispatch void setRunIndex(LogicSolverConfiguration config, Map<String, String> parameters, int runIndex,
170 ScriptConsole console) {
148 } 171 }
149} \ No newline at end of file 172}
generated by cgit v1.2.3-54-g00ecf (git 2.45.0) at 2024-05-05 08:55:01 +0000