From f5afda733ffdf4f52da932e03919c20b99bf7fa6 Mon Sep 17 00:00:00 2001 From: Aren Babikian Date: Tue, 15 Dec 2020 13:18:17 -0500 Subject: Add config flag for selecting numeric solver. Integ with Z3 --- .../mit/inf/dslreasoner/application/execution/SolverLoader.xtend | 9 +++++++++ 1 file changed, 9 insertions(+) (limited to 'Application/hu.bme.mit.inf.dslreasoner.application/src') 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 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) { -- cgit v1.2.3-70-g09d2