diff options
author | 2020-12-15 13:18:17 -0500 | |
---|---|---|
committer | 2021-01-06 00:02:49 +0100 | |
commit | f5afda733ffdf4f52da932e03919c20b99bf7fa6 (patch) | |
tree | fc875240bafc47c02e19d22b32e4c5a99fcfd941 /Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme | |
parent | implement getOneSolution with Dreal Integration (diff) | |
download | VIATRA-Generator-f5afda733ffdf4f52da932e03919c20b99bf7fa6.tar.gz VIATRA-Generator-f5afda733ffdf4f52da932e03919c20b99bf7fa6.tar.zst VIATRA-Generator-f5afda733ffdf4f52da932e03919c20b99bf7fa6.zip |
Add config flag for selecting numeric solver. Integ with Z3
Diffstat (limited to 'Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme')
-rw-r--r-- | Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/SolverLoader.xtend | 9 |
1 files changed, 9 insertions, 0 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 fd50ad51..bb21f8ee 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 | |||
@@ -29,6 +29,7 @@ import org.eclipse.viatra.query.patternlanguage.emf.vql.PatternModel | |||
29 | import org.eclipse.xtext.EcoreUtil2 | 29 | import org.eclipse.xtext.EcoreUtil2 |
30 | import org.eclipse.xtext.xbase.lib.Functions.Function1 | 30 | import org.eclipse.xtext.xbase.lib.Functions.Function1 |
31 | import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.AlloyBackendSolver | 31 | import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.AlloyBackendSolver |
32 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.NumericSolverSelection | ||
32 | 33 | ||
33 | class SolverLoader { | 34 | class SolverLoader { |
34 | def loadSolver(Solver solver, Map<String, String> config) { | 35 | def loadSolver(Solver solver, Map<String, String> config) { |
@@ -139,6 +140,14 @@ class SolverLoader { | |||
139 | val stringValue = config.get("fitness-objectCreationCosts") | 140 | val stringValue = config.get("fitness-objectCreationCosts") |
140 | c.calculateObjectCreationCosts = Boolean.parseBoolean(stringValue) | 141 | c.calculateObjectCreationCosts = Boolean.parseBoolean(stringValue) |
141 | } | 142 | } |
143 | if (config.containsKey("numeric-solver")) { | ||
144 | val stringValue = config.get("numeric-solver") | ||
145 | c.numericSolverSelection = switch (stringValue) { | ||
146 | case "dreal": NumericSolverSelection.DREAL | ||
147 | case "z3": NumericSolverSelection.Z3 | ||
148 | default: throw new IllegalArgumentException("Unknown numeric solver selection: " + stringValue) | ||
149 | } | ||
150 | } | ||
142 | if (config.containsKey("scopePropagator")) { | 151 | if (config.containsKey("scopePropagator")) { |
143 | val stringValue = config.get("scopePropagator") | 152 | val stringValue = config.get("scopePropagator") |
144 | c.scopePropagatorStrategy = switch (stringValue) { | 153 | c.scopePropagatorStrategy = switch (stringValue) { |