CrossingScenario case study is ready for serverdreal-integration

4 files changed, 10 insertions, 6 deletions

diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/BestFirstStrategyForModelGeneration.java b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/BestFirstStrategyForModelGeneration.java
index a8d2381c..c62d124a 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/BestFirstStrategyForModelGeneration.java
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/BestFirstStrategyForModelGeneration.java
@@ -222,6 +222,7 @@ public class BestFirstStrategyForModelGeneration implements IStrategy {
 //                                      }       

 //                              }

                                 

+//                              System.out.println("--------NEXT");

                                 boolean consistencyCheckResult = checkConsistency(currentTrajectoryWithFitness);

                                 if(consistencyCheckResult == true) { continue mainLoop; }

 

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 8281c3c3..a228afc6 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
@@ -55,7 +55,7 @@ class NumericSolver {
                 this.caching = caching

                 this.drealLocalPath = config.drealLocalPath

                 this.strategy = config.strategy

-                this.t = new NumericTranslator(createNumericTranslator(config))

+                this.t = new NumericTranslator(createNumericTranslator(config), config.drealTimeout)

         }

         

         def createNumericTranslator(ViatraReasonerConfiguration config) {

@@ -77,7 +77,7 @@ class NumericSolver {
                         System.load(root + "/Solvers/SMT-Solver/com.microsoft.z3/lib/libz3java.so");

         //              System.load("libz3.so");

         //              System.load("libz3java.so");

-                                return new NumericZ3ProblemSolver

+                                return new NumericZ3ProblemSolver(config.drealTimeout)

                         }

                 }

                 else {

@@ -150,9 +150,9 @@ class NumericSolver {
                         //Filter constraints if there are phase-related restricutions

                         //null whitelist means accept everything

                         

-                        println("<<<<START-STEP>>>> (" + phase + ")")

+//                      println("<<<<START-STEP>>>> (" + phase + ")")

                         if (phase == -2) {

-                                println("Skipping numeric check")

+//                              println("Skipping numeric check")

                                 //TODO Big assumption

                                 return true

                         }

@@ -235,7 +235,7 @@ class NumericSolver {
         

         def selectSolver(int phase) {

                 if (strategy === ExplorationStrategy.CrossingScenario){

-                        if (phase == 1) return "dreal"

+                        if (phase == 1) return "z3"

                         else return "dreal"

                 }

                 return "irrelevant"

diff --git a/Solvers/VIATRA-Solver/org.eclipse.viatra.dse/src/org/eclipse/viatra/dse/objectives/impl/ModelQueriesGlobalConstraint.java b/Solvers/VIATRA-Solver/org.eclipse.viatra.dse/src/org/eclipse/viatra/dse/objectives/impl/ModelQueriesGlobalConstraint.java
index 7616b4a2..3a990a1e 100644
--- a/Solvers/VIATRA-Solver/org.eclipse.viatra.dse/src/org/eclipse/viatra/dse/objectives/impl/ModelQueriesGlobalConstraint.java
+++ b/Solvers/VIATRA-Solver/org.eclipse.viatra.dse/src/org/eclipse/viatra/dse/objectives/impl/ModelQueriesGlobalConstraint.java
@@ -87,6 +87,8 @@ public class ModelQueriesGlobalConstraint implements IGlobalConstraint {
         for (ViatraQueryMatcher<? extends IPatternMatch> matcher : matchers) {
             if ((type.equals(ModelQueryType.NO_MATCH) && matcher.countMatches() > 0)
                     || (type.equals(ModelQueryType.MUST_HAVE_MATCH) && matcher.countMatches() == 0)) {
+//              System.out.println(type + " " + matcher.countMatches());
+//              System.out.println(matcher.getSpecification().getSimpleName());
                 return false;
             }
         }
diff --git a/Solvers/VIATRA-Solver/org.eclipse.viatra.dse/src/org/eclipse/viatra/dse/solutionstore/SolutionStore.java b/Solvers/VIATRA-Solver/org.eclipse.viatra.dse/src/org/eclipse/viatra/dse/solutionstore/SolutionStore.java
index 578ae277..6e0abd0b 100644
--- a/Solvers/VIATRA-Solver/org.eclipse.viatra.dse/src/org/eclipse/viatra/dse/solutionstore/SolutionStore.java
+++ b/Solvers/VIATRA-Solver/org.eclipse.viatra.dse/src/org/eclipse/viatra/dse/solutionstore/SolutionStore.java
@@ -208,10 +208,11 @@ public class SolutionStore {
         solutionTrajectory.setFitness(fitness);
 
         if (acceptOnlyGoalSolutions && !fitness.isSatisifiesHardObjectives()) {
+//              System.out.println("NOT SAVING");
             unsavedSolutionCallbacks(context, solutionTrajectory);
             return;
         }
-
+        System.out.println("SAVING SOLUTION");
         boolean solutionSaved = solutionSaver.saveSolution(context, id, solutionTrajectory);
 
         if (solutionSaved) {