Merge branch 'master' of github.com:viatra/VIATRA-Generator

2 files changed, 11 insertions, 6 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
 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

 

 class SolverLoader {

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

@@ -73,9 +74,9 @@ class SolverLoader {
                                 if (!objectiveEntries.empty) {

                                         throw new IllegalArgumentException("Objectives are not supported by Alloy.")

                                 }

-                                val c = new SmtSolverConfiguration

-                                config.getAsBoolean("fixRandomSeed", console).ifPresent[c.fixRandomSeed = it]

-                                config.getAsType("path", console, [it], String).ifPresent[c.solverPath = it]

+                                val c = new AlloySolverConfiguration

+                                config.getAsInteger("symmetry", console).ifPresent[c.symmetry = it]

+                                config.getAsType("solver",console,[x|AlloyBackendSolver::valueOf(x)],AlloyBackendSolver).ifPresent[c.solver = it]

                                 c

                         }

                         case SMT_SOLVER: {

diff --git a/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/ExpressionEvaluation2Logic.xtend b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/ExpressionEvaluation2Logic.xtend
index b4303739..6393121b 100644
--- a/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/ExpressionEvaluation2Logic.xtend
+++ b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/ExpressionEvaluation2Logic.xtend
@@ -12,11 +12,15 @@ import org.eclipse.xtext.xbase.XMemberFeatureCall
 import org.eclipse.xtext.xbase.XNumberLiteral

 import org.eclipse.xtext.xbase.XUnaryOperation

 

-import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*

-

 class ExpressionEvaluation2Logic {

         val extension LogicProblemBuilder builder = new LogicProblemBuilder

-        val NumericProblemSolver numericSolver = new NumericProblemSolver

+        var NumericProblemSolver _numericSolver = null //new NumericProblemSolver

+        def getNumericSolver() {

+                if(_numericSolver === null) {

+                        _numericSolver = new NumericProblemSolver

+                }

+                return _numericSolver

+        }

         

         def Term transformCheck(XExpression expression, Map<PVariable, Variable> variable2Variable) {

                 return expression.transform(variable2Variable)