Add config flag for selecting numeric solver. Integ with Z3

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
 import org.eclipse.xtext.EcoreUtil2

 import org.eclipse.xtext.xbase.lib.Functions.Function1

 import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.AlloyBackendSolver

+import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.NumericSolverSelection

 

 class SolverLoader {

         def loadSolver(Solver solver, Map<String, String> config) {

@@ -139,6 +140,14 @@ class SolverLoader {
                                         val stringValue = config.get("fitness-objectCreationCosts")

                                         c.calculateObjectCreationCosts = Boolean.parseBoolean(stringValue)

                                 }

+                                if (config.containsKey("numeric-solver")) {

+                                        val stringValue = config.get("numeric-solver")

+                                        c.numericSolverSelection = switch (stringValue) {

+                                                case "dreal": NumericSolverSelection.DREAL

+                                                case "z3": NumericSolverSelection.Z3

+                                                default: throw new IllegalArgumentException("Unknown numeric solver selection: " + stringValue)

+                                        }

+                                }

                                 if (config.containsKey("scopePropagator")) {

                                         val stringValue = config.get("scopePropagator")

                                         c.scopePropagatorStrategy = switch (stringValue) {