made Z3 optional dependency if there are no numbers

2 files changed, 24 insertions, 7 deletions

diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/META-INF/MANIFEST.MF b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/META-INF/MANIFEST.MF
index f5eb5514..49cf50b0 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/META-INF/MANIFEST.MF
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/META-INF/MANIFEST.MF
@@ -25,7 +25,7 @@ Require-Bundle: hu.bme.mit.inf.dslreasoner.logic.model;bundle-version="1.0.0",
  org.eclipse.xtext;bundle-version="2.10.0",
  org.eclipse.viatra.transformation.runtime.emf;bundle-version="2.0.0",
  org.eclipse.xtext.xbase;bundle-version="2.10.0",
- hu.bme.mit.inf.dslreasoner.ilp.cbc;bundle-version="1.0.0",
+ hu.bme.mit.inf.dslreasoner.ilp.cbc;bundle-version="1.0.0";resolution:=optional,
  org.eclipse.viatra.query.runtime.rete;bundle-version="2.0.0",
  com.microsoft.z3
 Bundle-RequiredExecutionEnvironment: JavaSE-11
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/NumericRefinementUnit.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/NumericRefinementUnit.xtend
index b3e2d78d..0b765854 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/NumericRefinementUnit.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/NumericRefinementUnit.xtend
@@ -35,8 +35,8 @@ class NumericRefinementUnit {
         var ThreadContext threadContext
         val constraint2MustUnitPropagationPrecondition = new HashMap<PConstraint,ViatraQueryMatcher<? extends IPatternMatch>>
         val constraint2CurrentUnitPropagationPrecondition = new HashMap<PConstraint,ViatraQueryMatcher<? extends IPatternMatch>>
-        var NumericTranslator translator = null;
-        
+        var NumericTranslator _translator = null;
+        val ViatraReasonerConfiguration config
         
         val boolean intermediateConsistencyCheck
         val boolean caching;
@@ -53,7 +53,15 @@ class NumericRefinementUnit {
                 this.intermediateConsistencyCheck = config.runIntermediateNumericalConsistencyChecks
                 this.caching = caching
                 this.strategy = config.strategy
-                this.translator = new NumericTranslator(createNumericTranslator(config),config.numericSolverTimeout)
+                this._translator = null
+                this.config = config
+        }
+        
+        def private getTranslator() {
+                if(_translator === null) {
+                        _translator =   new NumericTranslator(createNumericTranslator(config),config.numericSolverTimeout)
+                }
+                return _translator
         }
         
         def createNumericTranslator(ViatraReasonerConfiguration config) {
@@ -115,9 +123,18 @@ class NumericRefinementUnit {
         def getCachingTime(){cachingTime}
         def getNumberOfSolverCalls(){numberOfSolverCalls}
         def getNumberOfCachedSolverCalls(){numberOfCachedSolverCalls}
-        def getSolverFormingProblem(){this.translator.formingProblemTime}
-        def getSolverSolvingProblem(){this.translator.solvingProblemTime}
-        def getSolverSolution(){this.translator.formingSolutionTime}
+        def getSolverFormingProblem(){
+                if(this._translator === null) { return 0; }
+                else return this.translator.formingProblemTime
+        }
+        def getSolverSolvingProblem(){
+                if(this._translator === null) { return 0; }
+                else this.translator.solvingProblemTime
+        }
+        def getSolverSolution(){
+                if(this._translator === null) { return 0; }
+                else this.translator.formingSolutionTime
+        }
         def getNumericSolverSelection(){this.translator.numericSolver}
         
         def boolean maySatisfiable() {