3 files changed, 25 insertions, 6 deletions

diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasoner.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasoner.xtend
index 1f902b90..144e5e6f 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasoner.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasoner.xtend
@@ -38,6 +38,7 @@ import org.eclipse.viatra.dse.api.DesignSpaceExplorer
 import org.eclipse.viatra.dse.api.DesignSpaceExplorer.DseLoggingLevel

 import org.eclipse.viatra.dse.solutionstore.SolutionStore

 import org.eclipse.viatra.dse.statecode.IStateCoderFactory

+import hu.bme.mit.inf.dslreasoner.viatra2logic.NumericDrealProblemSolver

 

 class ViatraReasoner extends LogicReasoner {

         val PartialInterpretationInitialiser initialiser = new PartialInterpretationInitialiser()

@@ -109,7 +110,7 @@ class ViatraReasoner extends LogicReasoner {
                                 new SolutionStore(numberOfRequiredSolutions)

                         }

                 solutionStore.registerSolutionFoundHandler(new LoggerSolutionFoundHandler(viatraConfig))

-                val numericSolver = new NumericSolver(method, viatraConfig.runIntermediateNumericalConsistencyChecks, false)

+                val numericSolver = new NumericSolver(method, viatraConfig, false)

                 val solutionSaver = method.solutionSaver

                 solutionSaver.numericSolver = numericSolver

                 val solutionCopier = solutionSaver.solutionCopier

@@ -165,7 +166,9 @@ class ViatraReasoner extends LogicReasoner {
                 viatraConfig.progressMonitor.workedSearchFinished

                 

                 //dreal teardown

-                numericSolver.numericDrealSolver.teardown()

+                if (viatraConfig.numericSolverSelection == NumericSolverSelection.DREAL){

+                        (numericSolver.numericSolverSelection as NumericDrealProblemSolver).teardown()

+                }

 

                 // additionalMatches = strategy.solutionStoreWithCopy.additionalMatches

                 val statistics = createStatistics => [

diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasonerConfiguration.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasonerConfiguration.xtend
index fbe6da9d..ebfd5d81 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasonerConfiguration.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasonerConfiguration.xtend
@@ -33,6 +33,11 @@ enum PunishSizeStrategy {
         LARGER_IS_BETTER

 }

 

+enum NumericSolverSelection {

+        DREAL,

+        Z3

+}

+

 class ViatraReasonerConfiguration extends LogicSolverConfiguration {

         // public var Iterable<PQuery> existingQueries

         public var nameNewElements = false

@@ -70,6 +75,7 @@ class ViatraReasonerConfiguration extends LogicSolverConfiguration {
         public var nonContainmentWeight = 1

         public var unfinishedWFWeight = 1

         public var calculateObjectCreationCosts = false

+        public var numericSolverSelection = NumericSolverSelection.DREAL //currently defaulted to DREAL

         

         public var ScopePropagatorStrategy scopePropagatorStrategy = new ScopePropagatorStrategy.Polyhedral(

                 PolyhedralScopePropagatorConstraints.Relational, PolyhedralScopePropagatorSolver.Clp)

diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/NumericSolver.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/NumericSolver.xtend
index 0e789671..4b0ea544 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/NumericSolver.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/NumericSolver.xtend
@@ -1,6 +1,8 @@
 package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse

 

+import hu.bme.mit.inf.dslreasoner.viatra2logic.NumericDrealProblemSolver

 import hu.bme.mit.inf.dslreasoner.viatra2logic.NumericTranslator

+import hu.bme.mit.inf.dslreasoner.viatra2logic.NumericZ3ProblemSolver

 import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.BooleanElement

 import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.IntegerElement

 import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation

@@ -8,6 +10,8 @@ import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.par
 import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.RealElement

 import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.StringElement

 import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ModelGenerationMethod

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

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

 import java.math.BigDecimal

 import java.util.HashMap

 import java.util.LinkedHashMap

@@ -25,7 +29,7 @@ class NumericSolver {
         var ThreadContext threadContext

         val constraint2MustUnitPropagationPrecondition = new HashMap<PConstraint,ViatraQueryMatcher<? extends IPatternMatch>>

         val constraint2CurrentUnitPropagationPrecondition = new HashMap<PConstraint,ViatraQueryMatcher<? extends IPatternMatch>>

-        NumericTranslator t = new NumericTranslator

+        NumericTranslator t

         

         val boolean intermediateConsistencyCheck

         val boolean caching;

@@ -36,12 +40,18 @@ class NumericSolver {
         var int numberOfSolverCalls = 0

         var int numberOfCachedSolverCalls = 0

         

-        new(ModelGenerationMethod method, boolean intermediateConsistencyCheck, boolean caching) {

+        new(ModelGenerationMethod method, ViatraReasonerConfiguration config, boolean caching) {

                 this.method = method

-                this.intermediateConsistencyCheck = intermediateConsistencyCheck

+                this.intermediateConsistencyCheck = config.runIntermediateNumericalConsistencyChecks

+                this.t = new NumericTranslator(createNumericTranslator(config.numericSolverSelection))

                 this.caching = caching

         }

         

+        def createNumericTranslator(NumericSolverSelection solverSelection) {

+                if (solverSelection == NumericSolverSelection.DREAL) return new NumericDrealProblemSolver

+                if (solverSelection == NumericSolverSelection.Z3) return new NumericZ3ProblemSolver

+        }

+        

         def init(ThreadContext context) {

                 // This makes the NumericSolver single-threaded,

                 // but that's not a problem, because we only use the solver on a single thread anyways.

@@ -68,7 +78,7 @@ class NumericSolver {
         def getSolverFormingProblem(){this.t.formingProblemTime}

         def getSolverSolvingProblem(){this.t.solvingProblemTime}

         def getSolverSolution(){this.t.formingSolutionTime}

-        def getNumericDrealSolver(){this.t.drealSolver}

+        def getNumericSolverSelection(){this.t.numericSolver}

         

         def boolean maySatisfiable() {

                 if(intermediateConsistencyCheck) {