diff options
author | 2020-11-26 13:56:17 +0100 | |
---|---|---|
committer | 2020-11-26 13:56:17 +0100 | |
commit | 8a219bb3ee05e16a8da20247947addb86bf9cb96 (patch) | |
tree | 67163ee3fe180ab41d0926614737d4db840add8d /Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme | |
parent | Fix Z3 dependency (diff) | |
parent | NumericProblemSolver is initialized only if it is necessary (diff) | |
download | VIATRA-Generator-8a219bb3ee05e16a8da20247947addb86bf9cb96.tar.gz VIATRA-Generator-8a219bb3ee05e16a8da20247947addb86bf9cb96.tar.zst VIATRA-Generator-8a219bb3ee05e16a8da20247947addb86bf9cb96.zip |
Merge branch 'master' of github.com:viatra/VIATRA-Generator
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 | 7 |
1 files changed, 4 insertions, 3 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 a549df00..fd50ad51 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 | |||
@@ -28,6 +28,7 @@ import java.util.Optional | |||
28 | import org.eclipse.viatra.query.patternlanguage.emf.vql.PatternModel | 28 | 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 | 32 | ||
32 | class SolverLoader { | 33 | class SolverLoader { |
33 | def loadSolver(Solver solver, Map<String, String> config) { | 34 | def loadSolver(Solver solver, Map<String, String> config) { |
@@ -73,9 +74,9 @@ class SolverLoader { | |||
73 | if (!objectiveEntries.empty) { | 74 | if (!objectiveEntries.empty) { |
74 | throw new IllegalArgumentException("Objectives are not supported by Alloy.") | 75 | throw new IllegalArgumentException("Objectives are not supported by Alloy.") |
75 | } | 76 | } |
76 | val c = new SmtSolverConfiguration | 77 | val c = new AlloySolverConfiguration |
77 | config.getAsBoolean("fixRandomSeed", console).ifPresent[c.fixRandomSeed = it] | 78 | config.getAsInteger("symmetry", console).ifPresent[c.symmetry = it] |
78 | config.getAsType("path", console, [it], String).ifPresent[c.solverPath = it] | 79 | config.getAsType("solver",console,[x|AlloyBackendSolver::valueOf(x)],AlloyBackendSolver).ifPresent[c.solver = it] |
79 | c | 80 | c |
80 | } | 81 | } |
81 | case SMT_SOLVER: { | 82 | case SMT_SOLVER: { |