1 files changed, 296 insertions, 23 deletions
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 b8ea25e5..b8fcb6a0 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,14 +1,19 @@
 package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse
 import hu.bme.mit.inf.dslreasoner.viatra2logic.NumericDrealProblemSolver
+import hu.bme.mit.inf.dslreasoner.viatra2logic.NumericDynamicProblemSolver
 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.BinaryElementRelationLink
 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
+import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialRelationInterpretation
 import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PrimitiveElement
 import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.RealElement
+import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.RelationLink
 import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.StringElement
+import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ExplorationStrategy
 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
@@ -22,6 +27,7 @@ import org.eclipse.viatra.dse.base.ThreadContext
 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
 class NumericSolver {
        val ModelGenerationMethod method
@@ -34,6 +40,7 @@ class NumericSolver {
        val boolean caching;
        Map<LinkedHashMap<PConstraint, Iterable<List<Integer>>>,Boolean> satisfiabilityCache = new HashMap
        val String drealLocalPath;
+        val ExplorationStrategy strategy;
        
        var long runtime = 0
        var long cachingTime = 0 
@@ -45,24 +52,43 @@ class NumericSolver {
                this.intermediateConsistencyCheck = config.runIntermediateNumericalConsistencyChecks
                this.caching = caching
                this.drealLocalPath = config.drealLocalPath
-                this.t = new NumericTranslator(createNumericTranslator(config.numericSolverSelection))
+                this.strategy = config.strategy
+                this.t = new NumericTranslator(createNumericTranslator(config))
        }
        
-        def createNumericTranslator(NumericSolverSelection solverSelection) {
+        def createNumericTranslator(ViatraReasonerConfiguration config) {
-                if (solverSelection == NumericSolverSelection.DREAL_DOCKER) 
+                val solverSelection = config.numericSolverSelection
-                        return new NumericDrealProblemSolver(true, null)
+                val strategy = config.strategy
-                if (solverSelection == NumericSolverSelection.DREAL_LOCAL)
+                if (strategy == ExplorationStrategy.None) {
-                        return new NumericDrealProblemSolver(false, drealLocalPath)
+                        //initialise the specified
-                if (solverSelection == NumericSolverSelection.Z3) {
+                        if (solverSelection == NumericSolverSelection.DREAL_DOCKER) 
+                                return new NumericDrealProblemSolver(true, null)
+                        if (solverSelection == NumericSolverSelection.DREAL_LOCAL)
+                                return new NumericDrealProblemSolver(false, drealLocalPath)
+                        if (solverSelection == NumericSolverSelection.Z3) {
+                                //TODO THIS IS HARD-CODED for now
+//                      val root = "/data/viatra/VIATRA-Generator";
+                        val root = "/home/models/VIATRA-Generator";
+                                //END HARD-CODED
+        //                      String root = (new File(System.getProperty("user.dir"))).getParentFile().getParent();
+                        System.load(root + "/Solvers/SMT-Solver/com.microsoft.z3/lib/libz3.so");
+                        System.load(root + "/Solvers/SMT-Solver/com.microsoft.z3/lib/libz3java.so");
+        //              System.load("libz3.so");
+        //              System.load("libz3java.so");
+                                return new NumericZ3ProblemSolver
+                        }
+                }
+                else {
+                        //initialise both dreal-local and z3
+                        
                        //TODO THIS IS HARD-CODED for now
-                        val root = "/data/viatra/VIATRA-Generator";
+//                      val root = "/data/viatra/VIATRA-Generator";
+                        val root = "/home/models/VIATRA-Generator";
                        //END HARD-CODED
 //                      String root = (new File(System.getProperty("user.dir"))).getParentFile().getParent();
                System.load(root + "/Solvers/SMT-Solver/com.microsoft.z3/lib/libz3.so");
                System.load(root + "/Solvers/SMT-Solver/com.microsoft.z3/lib/libz3java.so");
-//              System.load("libz3.so");
+                        return new NumericDynamicProblemSolver(drealLocalPath)
-//              System.load("libz3java.so");
-                        return new NumericZ3ProblemSolver
                }
        }
        
@@ -95,31 +121,49 @@ class NumericSolver {
        def getNumericSolverSelection(){this.t.numericSolver}
        
        def boolean maySatisfiable() {
+                val int phase = determinePhase()
+                
                if(intermediateConsistencyCheck) {
-                        return isSatisfiable(this.constraint2MustUnitPropagationPrecondition)
+                        return isSatisfiable(this.constraint2MustUnitPropagationPrecondition, phase)
                } else {
                        return true
                }
        }
        def boolean currentSatisfiable() {
-                isSatisfiable(this.constraint2CurrentUnitPropagationPrecondition)
+                val int phase = determinePhase()
+                //TODO generalize this
+                isSatisfiable(this.constraint2CurrentUnitPropagationPrecondition, phase)
        }
        
-        private def boolean isSatisfiable(Map<PConstraint,ViatraQueryMatcher<? extends IPatternMatch>> matches) {
+        private def boolean isSatisfiable(Map<PConstraint,ViatraQueryMatcher<? extends IPatternMatch>> matches, int phase) {
                val start = System.nanoTime
                var boolean finalResult 
+                val boolean needsFilling = needsFilling
+                val model = threadContext.getModel as PartialInterpretation
+                val dataObjects = model.newElements.filter(PrimitiveElement).filter[!model.openWorldElements.contains(it)].toList
+        
                if(matches.empty){
                        finalResult=true
                } else {
                        val propagatedConstraints = new HashMap
-//                      println("<<<<START-STEP>>>>")
+                        //Filter constraints if there are phase-related restricutions
+                        //null whitelist means accept everything
+                        val whitelist = getConstraintWhitelist(phase)
+                        println("<<<<START-STEP>>>> (" + phase + ")")
                        for(entry : matches.entrySet) {
-                                val constraint = entry.key
+                                if (entry.value !== null){
-//                              println("--match?-- " + constraint)
+                                        val name = (entry.key as ExpressionEvaluation).body.pattern.simpleName
-                                val allMatches = entry.value.allMatches.map[it.toArray]
+                                        if (whitelist === null || whitelist.contains(name)) {
-//                              println("---------- " + entry.value.allMatches)
+//                                              println(name)
-                                propagatedConstraints.put(constraint,allMatches)
+                                                val constraint = entry.key
+//                                              println("--match?-- " + constraint)
+                                                val allMatches = entry.value.allMatches.map[it.toArray]
+                //                              println("---------- " + entry.value.allMatches)
+                                                propagatedConstraints.put(constraint,allMatches)
+                                        }
+                                }
                        }
+                        //check numeric problem
                        if(propagatedConstraints.values.forall[empty]) {
                                finalResult=true
                        } else {
@@ -133,16 +177,35 @@ class NumericSolver {
        //                                      }
                                                //println(code.hashCode)
                                                this.numberOfSolverCalls++
-                                                val res = t.delegateIsSatisfiable(propagatedConstraints)
+                                                var boolean res = false
+                                                if (needsFilling){
+                                                        //TODO ASSUME Always True
+                                                        //GET LIST OF VARS TO FILL
+                                                        val fillMap = t.delegateGetSolution(dataObjects, propagatedConstraints, selectSolver(phase))
+                                                        fillWithPartialSolutionsDirectly(dataObjects, fillMap)
+                                                        res = true
+                                                } else {
+                                                        res = t.delegateIsSatisfiable(propagatedConstraints, selectSolver(phase))
+                                                }
+                                                //TODO FIX CACHING
                                                satisfiabilityCache.put(code,res)
                                                finalResult=res
                                        } else {
                                                //println('''similar problem, answer from cache''')
+                                                println('''potential issue, answer from cache''')
                                                finalResult=cachedResult
                                                this.numberOfCachedSolverCalls++
                                        }
                                } else {
-                                        finalResult= t.delegateIsSatisfiable(propagatedConstraints)
+                                        if (needsFilling){
+                                                //TODO ASSUME Always True
+                                                //GET LIST OF VARS TO FILL
+                                                val fillMap = t.delegateGetSolution(dataObjects, propagatedConstraints, selectSolver(phase))
+                                                fillWithPartialSolutionsDirectly(dataObjects, fillMap)
+                                                finalResult = true
+                                        } else {
+                                                finalResult = t.delegateIsSatisfiable(propagatedConstraints, selectSolver(phase))
+                                        }
                                        this.numberOfSolverCalls++
                                }
                        }
@@ -151,6 +214,201 @@ class NumericSolver {
                return finalResult
        }
        
+        def selectSolver(int phase) {
+                if (strategy === ExplorationStrategy.CrossingScenario){
+                        if (phase == 1) return "dreal"
+                        else return "dreal"
+                }
+                return "irrelevant"
+        }
+        
+        def int determinePhase() {
+                // >= 0 : an actual phase
+                // -1 : take all numeric constraints
+                // -2 : SKIP (take no numeric constraints)
+                if (strategy == ExplorationStrategy.CrossingScenario) {
+                        //assumikng standard input, w/ visinBlocked and CollisionExists between pre-included actors
+                        val PartialInterpretation head = threadContext.getModel() as PartialInterpretation;
+                        val List<PartialRelationInterpretation> relations = head.getPartialrelationinterpretation();
+                        var boolean foundActorWithDefinedPos = false;
+                        for (PartialRelationInterpretation rel : relations) {
+                                if(rel.getInterpretationOf().getName().equals("xPos attribute Actor")) {
+                                        for (RelationLink link : rel.getRelationlinks()) {
+                                                val PrimitiveElement param2 = (link as BinaryElementRelationLink).getParam2() as PrimitiveElement;
+                                                if (param2.isValueSet()) {
+                                                        foundActorWithDefinedPos = true;
+                                                }
+                                        }
+                                }
+                                
+                                if(rel.getInterpretationOf().getName().equals("blockedBy reference VisionBlocked")) {
+                                        if (!rel.getRelationlinks().isEmpty()) {
+                                                return 3;
+                                        }
+                                }
+                        }
+                        //it means that there is no blockedBy
+                        //so we are at most at phase 2
+                        if (foundActorWithDefinedPos) return 2;
+                        return 1;                       
+                }
+                return -1;
+        }
+        
+        def getConstraintWhitelist(int phase) {
+                val List<String> wl = newArrayList
+                //null return means accept everything
+                if (strategy === ExplorationStrategy.None){
+                        return null
+                } else if (strategy === ExplorationStrategy.CrossingScenario){
+                        /*
+                                                "define_placedOn_actorOnVerticalLane",
+                                                "define_placedOn_actorOnHorizLane",
+                                                
+                                                "define_actor_maxXp",
+                                                "define_actor_minXp",
+                                                "define_actor_maxYp",
+                                                "define_actor_minYp",
+                                                
+                                                "define_actor_wrtLane",
+                                                        
+                                                "define_actor_minimumDistance",
+                                                
+                                                "define_actor_actorOnVertLaneHasxSpeed0",
+                                                "define_actor_actorOnVertLaneMinYs",
+                                                "define_actor_actorOnVertLaneMaxYs",
+                                                "define_actor_actorOnHorizLaneHasySpeed0",
+                                                "define_actor_actorOnHorizLaneMinXs",
+                                                "define_actor_actorOnHorizLaneMaxXs",
+                                                
+                                                "define_actor_pedestrianWidth",
+                                                "define_actor_pedestrianLength",
+                                                "define_actor_vehicleWidth",
+                                                "define_actor_vehicleWidth",
+                                                "define_actor_vehicleLength",
+                                                "define_actor_vehicleLength",
+                                                
+                                                "collisionExists_timeWithinBound",
+                                                "collisionExists_timeNotNegative",
+                                                "collisionExists_defineCollision_y1",
+                                                "collisionExists_defineCollision_y2",
+                                                "collisionExists_defineCollision_x1",
+                                                "collisionExists_defineCollision_x2",
+                                                
+                                                "visionBlocked_ites_notOnSameVertLine",
+                                                "visionBlocked_ites_top",
+                                                "visionBlocked_ites_bottom",
+                                                "visionBlocked_xdistBSlargerThanxdistTS",
+                                                "visionBlocked_xdistBTlargerThanxdistST",
+                                                "visionBlocked_ydistBSlargerThanydistTS",
+                                                "visionBlocked_ydistBTlargerThanydistST"
+                         */
+                        
+                        //HINTS:
+                        //define_actor_wrtLane
+                        //28.5 is structural hint
+                        switch (phase) {
+                                case 1: {                                       
+                                        wl.addAll(#[
+                                                "define_placedOn_actorOnVerticalLane",
+                                                "define_placedOn_actorOnHorizLane",
+                                                
+                                                "define_actor_maxXp",
+                                                "define_actor_minXp",
+                                                "define_actor_maxYp",
+                                                "define_actor_minYp",
+                                                
+                                                "define_actor_pedestrianWidth",
+                                                "define_actor_pedestrianLength",
+                                                "define_actor_vehicleWidth",
+                                                "define_actor_vehicleWidth",
+                                                "define_actor_vehicleLength",
+                                                "define_actor_vehicleLength"
+                                        ])
+                                }
+                                case 2: {
+                                        wl.addAll(#[
+                                                
+                                                "define_placedOn_actorOnVerticalLane",
+                                                "define_placedOn_actorOnHorizLane",
+                                                
+                                                "define_actor_maxXp",
+                                                "define_actor_minXp",
+                                                "define_actor_maxYp",
+                                                "define_actor_minYp",
+                                                        
+                                                "define_actor_minimumDistance",
+                                                
+                                                "define_actor_pedestrianWidth",
+                                                "define_actor_pedestrianLength",
+                                                "define_actor_vehicleWidth",
+                                                "define_actor_vehicleWidth",
+                                                "define_actor_vehicleLength",
+                                                "define_actor_vehicleLength",
+                                                
+                                                "visionBlocked_ites_notOnSameVertLine",
+                                                "visionBlocked_ites_top",
+                                                "visionBlocked_ites_bottom",
+                                                "visionBlocked_xdistBSlargerThanxdistTS",
+                                                "visionBlocked_xdistBTlargerThanxdistST",
+                                                "visionBlocked_ydistBSlargerThanydistTS",
+                                                "visionBlocked_ydistBTlargerThanydistST"
+                                        ])                              
+                                }
+                                case 3: {
+                                        wl.addAll(#[
+                                                
+                                                "define_placedOn_actorOnVerticalLane",
+                                                "define_placedOn_actorOnHorizLane",
+                                                
+                                                "define_actor_maxXp",
+                                                "define_actor_minXp",
+                                                "define_actor_maxYp",
+                                                "define_actor_minYp",
+                                                        
+                                                "define_actor_minimumDistance",
+                                                
+                                                "define_actor_actorOnVertLaneHasxSpeed0",
+                                                "define_actor_actorOnVertLaneMinYs",
+                                                "define_actor_actorOnVertLaneMaxYs",
+                                                "define_actor_actorOnHorizLaneHasySpeed0",
+                                                "define_actor_actorOnHorizLaneMinXs",
+                                                "define_actor_actorOnHorizLaneMaxXs",
+                                                
+                                                "define_actor_pedestrianWidth",
+                                                "define_actor_pedestrianLength",
+                                                "define_actor_vehicleWidth",
+                                                "define_actor_vehicleWidth",
+                                                "define_actor_vehicleLength",
+                                                "define_actor_vehicleLength",
+                                                
+                                                "collisionExists_timeWithinBound",
+                                                "collisionExists_timeNotNegative",
+                                                "collisionExists_defineCollision_y1",
+                                                "collisionExists_defineCollision_y2",
+                                                "collisionExists_defineCollision_x1",
+                                                "collisionExists_defineCollision_x2"
+                                        ])
+                                }
+                                default: {
+                                        //this is for 3 if we implement 4
+//                                      bl.addAll(#[0, 1, 2, 3, 4, 5, 6, 7])
+                                        
+                                        //this is for 4 if we do it
+                                        wl.addAll(#[])
+                                        return null
+                                }
+                        }
+                }               
+                return wl
+        }
+        
+        def getNeedsFilling(){
+                if (strategy == ExplorationStrategy.CrossingScenario) return true
+                return false
+        }
+        
        def getCode(HashMap<PConstraint, Iterable<Object[]>> propagatedConstraints) {
                val start = System.nanoTime
                val involvedObjects = new LinkedHashSet(propagatedConstraints.values.flatten.map[toList].flatten.toList).toList
@@ -175,7 +433,7 @@ class NumericSolver {
                        if(propagatedConstraints.values.forall[empty]) {
                                fillWithDefaultValues(dataObjects,trace)
                        } else {
-                                val solution = t.delegateGetSolution(dataObjects,propagatedConstraints)
+                                val solution = t.delegateGetSolution(dataObjects,propagatedConstraints, "dreal")
                                fillWithSolutions(dataObjects,solution,trace)
                        }
                }
@@ -215,4 +473,19 @@ class NumericSolver {
        def protected dispatch fillWithValue(IntegerElement e, Object value) {e.valueSet=true e.value=value as Integer}
        def protected dispatch fillWithValue(RealElement e, Object value) {e.valueSet=true e.value=value as Double }
        def protected dispatch fillWithValue(StringElement e, Object value) {e.valueSet=true e.value=value as String}
+        
+        def protected fillWithPartialSolutionsDirectly(List<PrimitiveElement> elements, Map<PrimitiveElement, Number> solution) {
+                for(element : elements) {
+                        //we allow overwriting of already set variables
+                        if(solution.containsKey(element)) {
+                                val value = solution.get(element)
+                                if (value !== null){
+                                        element.fillWithValue(value)
+                                        println("<" + element + "> is filled")
+                                } else {
+                                        println("<" + element + "> is unfilled")
+                                }
+                        }
+                }
+        }
 }
 \ 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/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 b8ea25e5..b8fcb6a0 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,14 +1,19 @@
1	package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse	1	package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse
2		2
3	import hu.bme.mit.inf.dslreasoner.viatra2logic.NumericDrealProblemSolver	3	import hu.bme.mit.inf.dslreasoner.viatra2logic.NumericDrealProblemSolver
		4	import hu.bme.mit.inf.dslreasoner.viatra2logic.NumericDynamicProblemSolver
4	import hu.bme.mit.inf.dslreasoner.viatra2logic.NumericTranslator	5	import hu.bme.mit.inf.dslreasoner.viatra2logic.NumericTranslator
5	import hu.bme.mit.inf.dslreasoner.viatra2logic.NumericZ3ProblemSolver	6	import hu.bme.mit.inf.dslreasoner.viatra2logic.NumericZ3ProblemSolver
		7	import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.BinaryElementRelationLink
6	import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.BooleanElement	8	import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.BooleanElement
7	import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.IntegerElement	9	import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.IntegerElement
8	import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation	10	import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation
		11	import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialRelationInterpretation
9	import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PrimitiveElement	12	import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PrimitiveElement
10	import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.RealElement	13	import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.RealElement
		14	import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.RelationLink
11	import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.StringElement	15	import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.StringElement
		16	import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ExplorationStrategy
12	import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ModelGenerationMethod	17	import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ModelGenerationMethod
13	import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.NumericSolverSelection	18	import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.NumericSolverSelection
14	import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ViatraReasonerConfiguration	19	import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ViatraReasonerConfiguration
@@ -22,6 +27,7 @@ import org.eclipse.viatra.dse.base.ThreadContext
22	import org.eclipse.viatra.query.runtime.api.IPatternMatch	27	import org.eclipse.viatra.query.runtime.api.IPatternMatch
23	import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher	28	import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher
24	import org.eclipse.viatra.query.runtime.matchers.psystem.PConstraint	29	import org.eclipse.viatra.query.runtime.matchers.psystem.PConstraint
		30	import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.ExpressionEvaluation
25		31
26	class NumericSolver {	32	class NumericSolver {
27	val ModelGenerationMethod method	33	val ModelGenerationMethod method
@@ -34,6 +40,7 @@ class NumericSolver {
34	val boolean caching;	40	val boolean caching;
35	Map<LinkedHashMap<PConstraint, Iterable<List<Integer>>>,Boolean> satisfiabilityCache = new HashMap	41	Map<LinkedHashMap<PConstraint, Iterable<List<Integer>>>,Boolean> satisfiabilityCache = new HashMap
36	val String drealLocalPath;	42	val String drealLocalPath;
		43	val ExplorationStrategy strategy;
37		44
38	var long runtime = 0	45	var long runtime = 0
39	var long cachingTime = 0	46	var long cachingTime = 0
@@ -45,24 +52,43 @@ class NumericSolver {
45	this.intermediateConsistencyCheck = config.runIntermediateNumericalConsistencyChecks	52	this.intermediateConsistencyCheck = config.runIntermediateNumericalConsistencyChecks
46	this.caching = caching	53	this.caching = caching
47	this.drealLocalPath = config.drealLocalPath	54	this.drealLocalPath = config.drealLocalPath
48	this.t = new NumericTranslator(createNumericTranslator(config.numericSolverSelection))	55	this.strategy = config.strategy
		56	this.t = new NumericTranslator(createNumericTranslator(config))
49	}	57	}
50		58
51	def createNumericTranslator(NumericSolverSelection solverSelection) {	59	def createNumericTranslator(ViatraReasonerConfiguration config) {
52	if (solverSelection == NumericSolverSelection.DREAL_DOCKER)	60	val solverSelection = config.numericSolverSelection
53	return new NumericDrealProblemSolver(true, null)	61	val strategy = config.strategy
54	if (solverSelection == NumericSolverSelection.DREAL_LOCAL)	62	if (strategy == ExplorationStrategy.None) {
55	return new NumericDrealProblemSolver(false, drealLocalPath)	63	//initialise the specified
56	if (solverSelection == NumericSolverSelection.Z3) {	64	if (solverSelection == NumericSolverSelection.DREAL_DOCKER)
		65	return new NumericDrealProblemSolver(true, null)
		66	if (solverSelection == NumericSolverSelection.DREAL_LOCAL)
		67	return new NumericDrealProblemSolver(false, drealLocalPath)
		68	if (solverSelection == NumericSolverSelection.Z3) {
		69	//TODO THIS IS HARD-CODED for now
		70	// val root = "/data/viatra/VIATRA-Generator";
		71	val root = "/home/models/VIATRA-Generator";
		72	//END HARD-CODED
		73	// String root = (new File(System.getProperty("user.dir"))).getParentFile().getParent();
		74	System.load(root + "/Solvers/SMT-Solver/com.microsoft.z3/lib/libz3.so");
		75	System.load(root + "/Solvers/SMT-Solver/com.microsoft.z3/lib/libz3java.so");
		76	// System.load("libz3.so");
		77	// System.load("libz3java.so");
		78	return new NumericZ3ProblemSolver
		79	}
		80	}
		81	else {
		82	//initialise both dreal-local and z3
		83
57	//TODO THIS IS HARD-CODED for now	84	//TODO THIS IS HARD-CODED for now
58	val root = "/data/viatra/VIATRA-Generator";	85	// val root = "/data/viatra/VIATRA-Generator";
		86	val root = "/home/models/VIATRA-Generator";
59	//END HARD-CODED	87	//END HARD-CODED
60	// String root = (new File(System.getProperty("user.dir"))).getParentFile().getParent();	88	// String root = (new File(System.getProperty("user.dir"))).getParentFile().getParent();
61	System.load(root + "/Solvers/SMT-Solver/com.microsoft.z3/lib/libz3.so");	89	System.load(root + "/Solvers/SMT-Solver/com.microsoft.z3/lib/libz3.so");
62	System.load(root + "/Solvers/SMT-Solver/com.microsoft.z3/lib/libz3java.so");	90	System.load(root + "/Solvers/SMT-Solver/com.microsoft.z3/lib/libz3java.so");
63	// System.load("libz3.so");	91	return new NumericDynamicProblemSolver(drealLocalPath)
64	// System.load("libz3java.so");
65	return new NumericZ3ProblemSolver
66	}	92	}
67	}	93	}
68		94
@@ -95,31 +121,49 @@ class NumericSolver {
95	def getNumericSolverSelection(){this.t.numericSolver}	121	def getNumericSolverSelection(){this.t.numericSolver}
96		122
97	def boolean maySatisfiable() {	123	def boolean maySatisfiable() {
		124	val int phase = determinePhase()
		125
98	if(intermediateConsistencyCheck) {	126	if(intermediateConsistencyCheck) {
99	return isSatisfiable(this.constraint2MustUnitPropagationPrecondition)	127	return isSatisfiable(this.constraint2MustUnitPropagationPrecondition, phase)
100	} else {	128	} else {
101	return true	129	return true
102	}	130	}
103	}	131	}
104	def boolean currentSatisfiable() {	132	def boolean currentSatisfiable() {
105	isSatisfiable(this.constraint2CurrentUnitPropagationPrecondition)	133	val int phase = determinePhase()
		134	//TODO generalize this
		135	isSatisfiable(this.constraint2CurrentUnitPropagationPrecondition, phase)
106	}	136	}
107		137
108	private def boolean isSatisfiable(Map<PConstraint,ViatraQueryMatcher<? extends IPatternMatch>> matches) {	138	private def boolean isSatisfiable(Map<PConstraint,ViatraQueryMatcher<? extends IPatternMatch>> matches, int phase) {
109	val start = System.nanoTime	139	val start = System.nanoTime
110	var boolean finalResult	140	var boolean finalResult
		141	val boolean needsFilling = needsFilling
		142	val model = threadContext.getModel as PartialInterpretation
		143	val dataObjects = model.newElements.filter(PrimitiveElement).filter[!model.openWorldElements.contains(it)].toList
		144
111	if(matches.empty){	145	if(matches.empty){
112	finalResult=true	146	finalResult=true
113	} else {	147	} else {
114	val propagatedConstraints = new HashMap	148	val propagatedConstraints = new HashMap
115	// println("<<<<START-STEP>>>>")	149	//Filter constraints if there are phase-related restricutions
		150	//null whitelist means accept everything
		151	val whitelist = getConstraintWhitelist(phase)
		152	println("<<<<START-STEP>>>> (" + phase + ")")
116	for(entry : matches.entrySet) {	153	for(entry : matches.entrySet) {
117	val constraint = entry.key	154	if (entry.value !== null){
118	// println("--match?-- " + constraint)	155	val name = (entry.key as ExpressionEvaluation).body.pattern.simpleName
119	val allMatches = entry.value.allMatches.map[it.toArray]	156	if (whitelist === null \|\| whitelist.contains(name)) {
120	// println("---------- " + entry.value.allMatches)	157	// println(name)
121	propagatedConstraints.put(constraint,allMatches)	158	val constraint = entry.key
		159	// println("--match?-- " + constraint)
		160	val allMatches = entry.value.allMatches.map[it.toArray]
		161	// println("---------- " + entry.value.allMatches)
		162	propagatedConstraints.put(constraint,allMatches)
		163	}
		164	}
122	}	165	}
		166	//check numeric problem
123	if(propagatedConstraints.values.forall[empty]) {	167	if(propagatedConstraints.values.forall[empty]) {
124	finalResult=true	168	finalResult=true
125	} else {	169	} else {
@@ -133,16 +177,35 @@ class NumericSolver {
133	// }	177	// }
134	//println(code.hashCode)	178	//println(code.hashCode)
135	this.numberOfSolverCalls++	179	this.numberOfSolverCalls++
136	val res = t.delegateIsSatisfiable(propagatedConstraints)	180	var boolean res = false
		181	if (needsFilling){
		182	//TODO ASSUME Always True
		183	//GET LIST OF VARS TO FILL
		184	val fillMap = t.delegateGetSolution(dataObjects, propagatedConstraints, selectSolver(phase))
		185	fillWithPartialSolutionsDirectly(dataObjects, fillMap)
		186	res = true
		187	} else {
		188	res = t.delegateIsSatisfiable(propagatedConstraints, selectSolver(phase))
		189	}
		190	//TODO FIX CACHING
137	satisfiabilityCache.put(code,res)	191	satisfiabilityCache.put(code,res)
138	finalResult=res	192	finalResult=res
139	} else {	193	} else {
140	//println('''similar problem, answer from cache''')	194	//println('''similar problem, answer from cache''')
		195	println('''potential issue, answer from cache''')
141	finalResult=cachedResult	196	finalResult=cachedResult
142	this.numberOfCachedSolverCalls++	197	this.numberOfCachedSolverCalls++
143	}	198	}
144	} else {	199	} else {
145	finalResult= t.delegateIsSatisfiable(propagatedConstraints)	200	if (needsFilling){
		201	//TODO ASSUME Always True
		202	//GET LIST OF VARS TO FILL
		203	val fillMap = t.delegateGetSolution(dataObjects, propagatedConstraints, selectSolver(phase))
		204	fillWithPartialSolutionsDirectly(dataObjects, fillMap)
		205	finalResult = true
		206	} else {
		207	finalResult = t.delegateIsSatisfiable(propagatedConstraints, selectSolver(phase))
		208	}
146	this.numberOfSolverCalls++	209	this.numberOfSolverCalls++
147	}	210	}
148	}	211	}
@@ -151,6 +214,201 @@ class NumericSolver {
151	return finalResult	214	return finalResult
152	}	215	}
153		216
		217	def selectSolver(int phase) {
		218	if (strategy === ExplorationStrategy.CrossingScenario){
		219	if (phase == 1) return "dreal"
		220	else return "dreal"
		221	}
		222	return "irrelevant"
		223	}
		224
		225	def int determinePhase() {
		226	// >= 0 : an actual phase
		227	// -1 : take all numeric constraints
		228	// -2 : SKIP (take no numeric constraints)
		229	if (strategy == ExplorationStrategy.CrossingScenario) {
		230	//assumikng standard input, w/ visinBlocked and CollisionExists between pre-included actors
		231	val PartialInterpretation head = threadContext.getModel() as PartialInterpretation;
		232	val List<PartialRelationInterpretation> relations = head.getPartialrelationinterpretation();
		233	var boolean foundActorWithDefinedPos = false;
		234	for (PartialRelationInterpretation rel : relations) {
		235	if(rel.getInterpretationOf().getName().equals("xPos attribute Actor")) {
		236	for (RelationLink link : rel.getRelationlinks()) {
		237	val PrimitiveElement param2 = (link as BinaryElementRelationLink).getParam2() as PrimitiveElement;
		238	if (param2.isValueSet()) {
		239	foundActorWithDefinedPos = true;
		240	}
		241	}
		242	}
		243
		244	if(rel.getInterpretationOf().getName().equals("blockedBy reference VisionBlocked")) {
		245	if (!rel.getRelationlinks().isEmpty()) {
		246	return 3;
		247	}
		248	}
		249	}
		250	//it means that there is no blockedBy
		251	//so we are at most at phase 2
		252	if (foundActorWithDefinedPos) return 2;
		253	return 1;
		254	}
		255	return -1;
		256	}
		257
		258	def getConstraintWhitelist(int phase) {
		259	val List<String> wl = newArrayList
		260	//null return means accept everything
		261	if (strategy === ExplorationStrategy.None){
		262	return null
		263	} else if (strategy === ExplorationStrategy.CrossingScenario){
		264	/*
		265	"define_placedOn_actorOnVerticalLane",
		266	"define_placedOn_actorOnHorizLane",
		267
		268	"define_actor_maxXp",
		269	"define_actor_minXp",
		270	"define_actor_maxYp",
		271	"define_actor_minYp",
		272
		273	"define_actor_wrtLane",
		274
		275	"define_actor_minimumDistance",
		276
		277	"define_actor_actorOnVertLaneHasxSpeed0",
		278	"define_actor_actorOnVertLaneMinYs",
		279	"define_actor_actorOnVertLaneMaxYs",
		280	"define_actor_actorOnHorizLaneHasySpeed0",
		281	"define_actor_actorOnHorizLaneMinXs",
		282	"define_actor_actorOnHorizLaneMaxXs",
		283
		284	"define_actor_pedestrianWidth",
		285	"define_actor_pedestrianLength",
		286	"define_actor_vehicleWidth",
		287	"define_actor_vehicleWidth",
		288	"define_actor_vehicleLength",
		289	"define_actor_vehicleLength",
		290
		291	"collisionExists_timeWithinBound",
		292	"collisionExists_timeNotNegative",
		293	"collisionExists_defineCollision_y1",
		294	"collisionExists_defineCollision_y2",
		295	"collisionExists_defineCollision_x1",
		296	"collisionExists_defineCollision_x2",
		297
		298	"visionBlocked_ites_notOnSameVertLine",
		299	"visionBlocked_ites_top",
		300	"visionBlocked_ites_bottom",
		301	"visionBlocked_xdistBSlargerThanxdistTS",
		302	"visionBlocked_xdistBTlargerThanxdistST",
		303	"visionBlocked_ydistBSlargerThanydistTS",
		304	"visionBlocked_ydistBTlargerThanydistST"
		305	*/
		306
		307	//HINTS:
		308	//define_actor_wrtLane
		309	//28.5 is structural hint
		310	switch (phase) {
		311	case 1: {
		312	wl.addAll(#[
		313	"define_placedOn_actorOnVerticalLane",
		314	"define_placedOn_actorOnHorizLane",
		315
		316	"define_actor_maxXp",
		317	"define_actor_minXp",
		318	"define_actor_maxYp",
		319	"define_actor_minYp",
		320
		321	"define_actor_pedestrianWidth",
		322	"define_actor_pedestrianLength",
		323	"define_actor_vehicleWidth",
		324	"define_actor_vehicleWidth",
		325	"define_actor_vehicleLength",
		326	"define_actor_vehicleLength"
		327
		328	])
		329	}
		330	case 2: {
		331	wl.addAll(#[
		332
		333	"define_placedOn_actorOnVerticalLane",
		334	"define_placedOn_actorOnHorizLane",
		335
		336	"define_actor_maxXp",
		337	"define_actor_minXp",
		338	"define_actor_maxYp",
		339	"define_actor_minYp",
		340
		341	"define_actor_minimumDistance",
		342
		343	"define_actor_pedestrianWidth",
		344	"define_actor_pedestrianLength",
		345	"define_actor_vehicleWidth",
		346	"define_actor_vehicleWidth",
		347	"define_actor_vehicleLength",
		348	"define_actor_vehicleLength",
		349
		350	"visionBlocked_ites_notOnSameVertLine",
		351	"visionBlocked_ites_top",
		352	"visionBlocked_ites_bottom",
		353	"visionBlocked_xdistBSlargerThanxdistTS",
		354	"visionBlocked_xdistBTlargerThanxdistST",
		355	"visionBlocked_ydistBSlargerThanydistTS",
		356	"visionBlocked_ydistBTlargerThanydistST"
		357	])
		358	}
		359	case 3: {
		360	wl.addAll(#[
		361
		362	"define_placedOn_actorOnVerticalLane",
		363	"define_placedOn_actorOnHorizLane",
		364
		365	"define_actor_maxXp",
		366	"define_actor_minXp",
		367	"define_actor_maxYp",
		368	"define_actor_minYp",
		369
		370	"define_actor_minimumDistance",
		371
		372	"define_actor_actorOnVertLaneHasxSpeed0",
		373	"define_actor_actorOnVertLaneMinYs",
		374	"define_actor_actorOnVertLaneMaxYs",
		375	"define_actor_actorOnHorizLaneHasySpeed0",
		376	"define_actor_actorOnHorizLaneMinXs",
		377	"define_actor_actorOnHorizLaneMaxXs",
		378
		379	"define_actor_pedestrianWidth",
		380	"define_actor_pedestrianLength",
		381	"define_actor_vehicleWidth",
		382	"define_actor_vehicleWidth",
		383	"define_actor_vehicleLength",
		384	"define_actor_vehicleLength",
		385
		386	"collisionExists_timeWithinBound",
		387	"collisionExists_timeNotNegative",
		388	"collisionExists_defineCollision_y1",
		389	"collisionExists_defineCollision_y2",
		390	"collisionExists_defineCollision_x1",
		391	"collisionExists_defineCollision_x2"
		392	])
		393	}
		394	default: {
		395	//this is for 3 if we implement 4
		396	// bl.addAll(#[0, 1, 2, 3, 4, 5, 6, 7])
		397
		398	//this is for 4 if we do it
		399	wl.addAll(#[])
		400	return null
		401	}
		402	}
		403	}
		404	return wl
		405	}
		406
		407	def getNeedsFilling(){
		408	if (strategy == ExplorationStrategy.CrossingScenario) return true
		409	return false
		410	}
		411
154	def getCode(HashMap<PConstraint, Iterable<Object[]>> propagatedConstraints) {	412	def getCode(HashMap<PConstraint, Iterable<Object[]>> propagatedConstraints) {
155	val start = System.nanoTime	413	val start = System.nanoTime
156	val involvedObjects = new LinkedHashSet(propagatedConstraints.values.flatten.map[toList].flatten.toList).toList	414	val involvedObjects = new LinkedHashSet(propagatedConstraints.values.flatten.map[toList].flatten.toList).toList
@@ -175,7 +433,7 @@ class NumericSolver {
175	if(propagatedConstraints.values.forall[empty]) {	433	if(propagatedConstraints.values.forall[empty]) {
176	fillWithDefaultValues(dataObjects,trace)	434	fillWithDefaultValues(dataObjects,trace)
177	} else {	435	} else {
178	val solution = t.delegateGetSolution(dataObjects,propagatedConstraints)	436	val solution = t.delegateGetSolution(dataObjects,propagatedConstraints, "dreal")
179	fillWithSolutions(dataObjects,solution,trace)	437	fillWithSolutions(dataObjects,solution,trace)
180	}	438	}
181	}	439	}
@@ -215,4 +473,19 @@ class NumericSolver {
215	def protected dispatch fillWithValue(IntegerElement e, Object value) {e.valueSet=true e.value=value as Integer}	473	def protected dispatch fillWithValue(IntegerElement e, Object value) {e.valueSet=true e.value=value as Integer}
216	def protected dispatch fillWithValue(RealElement e, Object value) {e.valueSet=true e.value=value as Double }	474	def protected dispatch fillWithValue(RealElement e, Object value) {e.valueSet=true e.value=value as Double }
217	def protected dispatch fillWithValue(StringElement e, Object value) {e.valueSet=true e.value=value as String}	475	def protected dispatch fillWithValue(StringElement e, Object value) {e.valueSet=true e.value=value as String}
		476
		477	def protected fillWithPartialSolutionsDirectly(List<PrimitiveElement> elements, Map<PrimitiveElement, Number> solution) {
		478	for(element : elements) {
		479	//we allow overwriting of already set variables
		480	if(solution.containsKey(element)) {
		481	val value = solution.get(element)
		482	if (value !== null){
		483	element.fillWithValue(value)
		484	println("<" + element + "> is filled")
		485	} else {
		486	println("<" + element + "> is unfilled")
		487	}
		488	}
		489	}
		490	}
218	} \ No newline at end of file	491	} \ No newline at end of file