Ready for strategies case study

5 files changed, 40 insertions, 6 deletions

diff --git a/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericDrealProblemSolver.java b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericDrealProblemSolver.java
index 70aa933a..f098d575 100644
--- a/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericDrealProblemSolver.java
+++ b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericDrealProblemSolver.java
@@ -43,7 +43,7 @@ public class NumericDrealProblemSolver extends NumericProblemSolver{
         private Map<String, String> curVar2Decl;

         

         private final int TIMEOUT_DOCKER = 5000;

-        private final int TIMEOUT_LOCAL = 100000;

+        private final int TIMEOUT_LOCAL = -1;

         private final int DEBUG_PRINT = 3;

 

         public NumericDrealProblemSolver(boolean useDocker, String drealLocalPath) throws IOException, InterruptedException {

@@ -75,7 +75,9 @@ public class NumericDrealProblemSolver extends NumericProblemSolver{
 //              p.waitFor();

                 //TODO timeout if needed

                 long startTime = System.nanoTime();

-                if (!p.waitFor(timeout, TimeUnit.MILLISECONDS)) {

+                if (timeout == -1) {

+                        p.waitFor();

+                } else if (!p.waitFor(timeout, TimeUnit.MILLISECONDS)) {

                         p.destroy();

                         if (p.isAlive()) {

                             p.destroyForcibly();

@@ -406,6 +408,7 @@ public class NumericDrealProblemSolver extends NumericProblemSolver{
                 //CREATE DREAL STM2 FILE CONTENTS

                 long startformingProblem = System.nanoTime();

                 List<String> numProbContent = formNumericProblemInstance(matches);

+                if (DEBUG_PRINT > 2) printOutput(numProbContent);

                 endformingProblem = System.nanoTime()-startformingProblem;

                 

                 if (numProbContent == null) {

@@ -446,7 +449,6 @@ public class NumericDrealProblemSolver extends NumericProblemSolver{
                         System.out.println(result);

                 }

                 if (DEBUG_PRINT > 2) {

-                        printOutput(numProbContent);

                         if (outputs != null) printOutput(outputs.get(0));

                 }

                 

diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PExpressionGenerator.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PExpressionGenerator.xtend
index 62ff92b2..9835356e 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PExpressionGenerator.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PExpressionGenerator.xtend
@@ -10,6 +10,8 @@ import org.eclipse.xtext.xbase.XNumberLiteral
 import org.eclipse.xtext.xbase.XUnaryOperation

 import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.PrimitiveTypeReference

 import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RealTypeReference

+import org.eclipse.xtext.xbase.XIfExpression

+import org.eclipse.xtext.xbase.XBlockExpression

 

 class PExpressionGenerator {

         static val N_Base = "org.eclipse.xtext.xbase.lib."

@@ -113,4 +115,17 @@ class PExpressionGenerator {
         def dispatch CharSequence translateExpression(XExpression expression, Map<PVariable,String> valueName, Map<PVariable, PrimitiveTypeReference> variable2Type) {

                 throw new UnsupportedOperationException('''Unsupported expression in check or eval: «expression.class.name», «expression»"''')

         }

+        

+        def dispatch CharSequence translateExpression(XIfExpression e, Map<PVariable,String> valueName, Map<PVariable, PrimitiveTypeReference> variable2Type) {

+                val i = e.^if.translateExpression(valueName,variable2Type)

+                val t = e.then.translateExpression(valueName,variable2Type)

+                val el = e.^else.translateExpression(valueName,variable2Type)

+                

+                return '''(if(«i»){«t»}else{«el»})'''

+        }

+        

+        def dispatch CharSequence translateExpression(XBlockExpression e, Map<PVariable,String> valueName, Map<PVariable, PrimitiveTypeReference> variable2Type) {

+                //Assuming 1-item blocks only

+                return (e as XBlockExpression).expressions.get(0).translateExpression(valueName,variable2Type)

+        }

 }
\ No newline at end of file
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 5ad78506..a692e1e5 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
@@ -110,7 +110,7 @@ class ViatraReasoner extends LogicReasoner {
                                 new SolutionStore(numberOfRequiredSolutions)

                         }

                 solutionStore.registerSolutionFoundHandler(new LoggerSolutionFoundHandler(viatraConfig))

-                val numericSolver = new NumericSolver(method, viatraConfig, true)//was formerly hard-coded to false for caching

+                val numericSolver = new NumericSolver(method, viatraConfig, false)//was formerly hard-coded to false for caching

                 val solutionSaver = method.solutionSaver

                 solutionSaver.numericSolver = numericSolver

                 val solutionCopier = solutionSaver.solutionCopier

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 44964079..28edff41 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
@@ -24,10 +24,12 @@ import java.util.List
 import java.util.Map

 import org.eclipse.emf.ecore.EObject

 import org.eclipse.viatra.dse.base.ThreadContext

+import org.eclipse.viatra.dse.objectives.Fitness

 import org.eclipse.viatra.query.runtime.api.IPatternMatch

 import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher

 import org.eclipse.viatra.query.runtime.matchers.psystem.PConstraint

 import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.ExpressionEvaluation

+import org.eclipse.viatra.dse.objectives.IObjective

 

 class NumericSolver {

         val ModelGenerationMethod method

@@ -206,7 +208,6 @@ class NumericSolver {
                                         }

                                 } else {

                                         if (needsFilling){

-                                                //TODO ASSUME Always True

                                                 //GET LIST OF VARS TO FILL

                                                 val fillMap = t.delegateGetSolution(dataObjects, propagatedConstraints, selectSolver(phase))

                                                 if (fillMap === null) finalResult = false

@@ -225,7 +226,9 @@ class NumericSolver {
                 //STRATEGY

                 if (phase == 2) {

                         if (!finalResult) return finalResult

-                        else finalResult = isSatisfiable(matches, 3)

+                        else {

+                                finalResult = isSatisfiable(matches, 3)

+                        }

                 }

                 return finalResult

         }

@@ -243,6 +246,14 @@ class NumericSolver {
                 // -1 : take all numeric constraints

                 // -2 : SKIP (take no numeric constraints)

                 if (strategy == ExplorationStrategy.CrossingScenario) {

+//                      //if has structural (non-WF) fitness issues, skip numeric handling

+//                      val IObjective ob = threadContext.objectives.filter[it instanceof ModelGenerationCompositeObjective].get(0)

+//                      val compo = ob as ModelGenerationCompositeObjective

+//                      if (compo.getNonWFFitness(threadContext) > 0) {

+//                              println("bootleg numeric-skip")

+//                              return -2;

+//                      }

+                        

                         //assumikng standard input, w/ visinBlocked and CollisionExists between pre-included actors

                         val PartialInterpretation head = threadContext.getModel() as PartialInterpretation;

                         val List<PartialRelationInterpretation> relations = head.getPartialrelationinterpretation();

diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/UnfinishedWFObjective.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/UnfinishedWFObjective.xtend
index 1b61ffa5..b5b44254 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/UnfinishedWFObjective.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/UnfinishedWFObjective.xtend
@@ -37,6 +37,12 @@ class UnfinishedWFObjective implements IObjective {
         override getComparator() { Comparators.LOWER_IS_BETTER }

 

         override getFitness(ThreadContext context) {

+//              //MEGA ASSUMPTION Below TODO

+//              //if has no unfilled variables, return 0

+//              val model = context.getModel as PartialInterpretation

+//              val unfilledDataObjects = model.newElements.filter(PrimitiveElement).filter[!model.openWorldElements.contains(it)].filter[!it.isValueSet].toList

+//              if (unfilledDataObjects.isEmpty) return 0.0

+                

                 var sumOfMatches = 0

                 for (matcher : matchers) {

                         val number = matcher.countMatches