1 files changed, 192 insertions, 0 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
new file mode 100644
index 00000000..70e8e9c2
--- /dev/null
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/NumericSolver.xtend
@@ -0,0 +1,192 @@
+package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse
+import hu.bme.mit.inf.dslreasoner.viatra2logic.NumericTranslator
+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.PrimitiveElement
+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 java.math.BigDecimal
+import java.util.HashMap
+import java.util.LinkedHashMap
+import java.util.LinkedHashSet
+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.query.runtime.api.IPatternMatch
+import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher
+import org.eclipse.viatra.query.runtime.matchers.psystem.PConstraint
+class NumericSolver {
+        val ModelGenerationMethod method
+        var ThreadContext threadContext
+        val constraint2MustUnitPropagationPrecondition = new HashMap<PConstraint,ViatraQueryMatcher<? extends IPatternMatch>>
+        val constraint2CurrentUnitPropagationPrecondition = new HashMap<PConstraint,ViatraQueryMatcher<? extends IPatternMatch>>
+        NumericTranslator t = new NumericTranslator
+        
+        val boolean intermediateConsistencyCheck
+        val boolean caching;
+        Map<LinkedHashMap<PConstraint, Iterable<List<Integer>>>,Boolean> satisfiabilityCache = new HashMap
+        
+        var long runtime = 0
+        var long cachingTime = 0 
+        var int numberOfSolverCalls = 0
+        var int numberOfCachedSolverCalls = 0
+        
+        new(ModelGenerationMethod method, boolean intermediateConsistencyCheck, boolean caching) {
+                this.method = method
+                this.intermediateConsistencyCheck = intermediateConsistencyCheck
+                this.caching = caching
+        }
+        
+        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.
+                this.threadContext = context
+                val engine = threadContext.queryEngine
+                for(entry : method.mustUnitPropagationPreconditions.entrySet) {
+                        val constraint = entry.key
+                        val querySpec = entry.value
+                        val matcher = querySpec.getMatcher(engine);
+                        constraint2MustUnitPropagationPrecondition.put(constraint,matcher)
+                }
+                for(entry : method.currentUnitPropagationPreconditions.entrySet) {
+                        val constraint = entry.key
+                        val querySpec = entry.value
+                        val matcher = querySpec.getMatcher(engine);
+                        constraint2CurrentUnitPropagationPrecondition.put(constraint,matcher)
+                }
+        }
+        
+        def getRuntime(){runtime}
+        def getCachingTime(){cachingTime}
+        def getNumberOfSolverCalls(){numberOfSolverCalls}
+        def getNumberOfCachedSolverCalls(){numberOfCachedSolverCalls}
+        def getSolverFormingProblem(){this.t.formingProblemTime}
+        def getSolverSolvingProblem(){this.t.solvingProblemTime}
+        def getSolverSolution(){this.t.formingSolutionTime}
+        
+        def boolean maySatisfiable() {
+                if(intermediateConsistencyCheck) {
+                        return isSatisfiable(this.constraint2MustUnitPropagationPrecondition)
+                } else {
+                        return true
+                }
+        }
+        def boolean currentSatisfiable() {
+                isSatisfiable(this.constraint2CurrentUnitPropagationPrecondition)
+        }
+        
+        private def boolean isSatisfiable(Map<PConstraint,ViatraQueryMatcher<? extends IPatternMatch>> matches) {
+                val start = System.nanoTime
+                var boolean finalResult 
+                if(matches.empty){
+                        finalResult=true
+                } else {
+                        val propagatedConstraints = new HashMap
+                        for(entry : matches.entrySet) {
+                                val constraint = entry.key
+                                //println(constraint)
+                                val allMatches = entry.value.allMatches.map[it.toArray]
+                                //println(allMatches.toList)
+                                propagatedConstraints.put(constraint,allMatches)
+                        }
+                        if(propagatedConstraints.values.forall[empty]) {
+                                finalResult=true
+                        } else {
+                                if(caching) {
+                                        val code = getCode(propagatedConstraints)
+                                        val cachedResult = satisfiabilityCache.get(code)
+                                        if(cachedResult === null) {
+        //                                      println('''new problem, call solver''')
+        //                                      for(entry : code.entrySet) {
+        //                                              println('''«entry.key» -> «entry.value»''')
+        //                                      }
+                                                //println(code.hashCode)
+                                                this.numberOfSolverCalls++
+                                                val res = t.delegateIsSatisfiable(propagatedConstraints)
+                                                satisfiabilityCache.put(code,res)
+                                                finalResult=res
+                                        } else {
+                                                //println('''similar problem, answer from cache''')
+                                                finalResult=cachedResult
+                                                this.numberOfCachedSolverCalls++
+                                        }
+                                } else {
+                                        finalResult= t.delegateIsSatisfiable(propagatedConstraints)
+                                        this.numberOfSolverCalls++
+                                }
+                        }
+                }       
+                this.runtime+=System.nanoTime-start
+                return finalResult
+        }
+        
+        def getCode(HashMap<PConstraint, Iterable<Object[]>> propagatedConstraints) {
+                val start = System.nanoTime
+                val involvedObjects = new LinkedHashSet(propagatedConstraints.values.flatten.map[toList].flatten.toList).toList
+                val res = new LinkedHashMap(propagatedConstraints.mapValues[matches | matches.map[objects | objects.map[object | involvedObjects.indexOf(object)].toList]])
+                this.cachingTime += System.nanoTime-start
+                return res
+        }
+        
+        def fillSolutionCopy(Map<EObject, EObject> trace) {
+                val model = threadContext.getModel as PartialInterpretation
+                val dataObjects = model.newElements.filter(PrimitiveElement).filter[!model.openWorldElements.contains(it)].toList
+                if(constraint2CurrentUnitPropagationPrecondition.empty) {
+                        fillWithDefaultValues(dataObjects,trace)
+                } else {
+                        val propagatedConstraints = new HashMap
+                        for(entry : constraint2CurrentUnitPropagationPrecondition.entrySet) {
+                                val constraint = entry.key
+                                val allMatches = entry.value.allMatches.map[it.toArray]
+                                propagatedConstraints.put(constraint,allMatches)
+                        }
+                        
+                        if(propagatedConstraints.values.forall[empty]) {
+                                fillWithDefaultValues(dataObjects,trace)
+                        } else {
+                                val solution = t.delegateGetSolution(dataObjects,propagatedConstraints)
+                                fillWithSolutions(dataObjects,solution,trace)
+                        }
+                }
+        }
+        
+        def protected fillWithDefaultValues(List<PrimitiveElement> elements, Map<EObject, EObject> trace) {
+                for(element : elements) {
+                        if(element.valueSet==false) {
+                                val value = getDefaultValue(element)
+                                val target = trace.get(element) as PrimitiveElement
+                                target.fillWithValue(value)
+                        }
+                }
+        }
+        
+        def protected dispatch getDefaultValue(BooleanElement e) {false}
+        def protected dispatch getDefaultValue(IntegerElement e) {0}
+        def protected dispatch getDefaultValue(RealElement e) {0.0}
+        def protected dispatch getDefaultValue(StringElement e) {""}
+        
+        def protected fillWithSolutions(List<PrimitiveElement> elements, Map<PrimitiveElement, Number> solution, Map<EObject, EObject> trace) {
+                for(element : elements) {
+                        if(element.valueSet==false) {
+                                if(solution.containsKey(element)) {
+                                        val value = solution.get(element)
+                                        val target = trace.get(element) as PrimitiveElement
+                                        target.fillWithValue(value)
+                                } else {
+                                        val target = trace.get(element) as PrimitiveElement
+                                        target.fillWithValue(target.defaultValue)
+                                }
+                        }
+                }
+        }
+        
+        def protected dispatch fillWithValue(BooleanElement e, Object value) {e.valueSet=true e.value=value as Boolean}
+        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=BigDecimal.valueOf(value as Double) }
+        def protected dispatch fillWithValue(StringElement e, Object value) {e.valueSet=true e.value=value as String}
+}
+\ 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 new file mode 100644 index 00000000..70e8e9c2 --- /dev/null +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/NumericSolver.xtend
@@ -0,0 +1,192 @@
	1	package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse
	2
	3	import hu.bme.mit.inf.dslreasoner.viatra2logic.NumericTranslator
	4	import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.BooleanElement
	5	import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.IntegerElement
	6	import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation
	7	import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PrimitiveElement
	8	import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.RealElement
	9	import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.StringElement
	10	import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ModelGenerationMethod
	11	import java.math.BigDecimal
	12	import java.util.HashMap
	13	import java.util.LinkedHashMap
	14	import java.util.LinkedHashSet
	15	import java.util.List
	16	import java.util.Map
	17	import org.eclipse.emf.ecore.EObject
	18	import org.eclipse.viatra.dse.base.ThreadContext
	19	import org.eclipse.viatra.query.runtime.api.IPatternMatch
	20	import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher
	21	import org.eclipse.viatra.query.runtime.matchers.psystem.PConstraint
	22
	23	class NumericSolver {
	24	val ModelGenerationMethod method
	25	var ThreadContext threadContext
	26	val constraint2MustUnitPropagationPrecondition = new HashMap<PConstraint,ViatraQueryMatcher<? extends IPatternMatch>>
	27	val constraint2CurrentUnitPropagationPrecondition = new HashMap<PConstraint,ViatraQueryMatcher<? extends IPatternMatch>>
	28	NumericTranslator t = new NumericTranslator
	29
	30	val boolean intermediateConsistencyCheck
	31	val boolean caching;
	32	Map<LinkedHashMap<PConstraint, Iterable<List<Integer>>>,Boolean> satisfiabilityCache = new HashMap
	33
	34	var long runtime = 0
	35	var long cachingTime = 0
	36	var int numberOfSolverCalls = 0
	37	var int numberOfCachedSolverCalls = 0
	38
	39	new(ModelGenerationMethod method, boolean intermediateConsistencyCheck, boolean caching) {
	40	this.method = method
	41	this.intermediateConsistencyCheck = intermediateConsistencyCheck
	42	this.caching = caching
	43	}
	44
	45	def init(ThreadContext context) {
	46	// This makes the NumericSolver single-threaded,
	47	// but that's not a problem, because we only use the solver on a single thread anyways.
	48	this.threadContext = context
	49	val engine = threadContext.queryEngine
	50	for(entry : method.mustUnitPropagationPreconditions.entrySet) {
	51	val constraint = entry.key
	52	val querySpec = entry.value
	53	val matcher = querySpec.getMatcher(engine);
	54	constraint2MustUnitPropagationPrecondition.put(constraint,matcher)
	55	}
	56	for(entry : method.currentUnitPropagationPreconditions.entrySet) {
	57	val constraint = entry.key
	58	val querySpec = entry.value
	59	val matcher = querySpec.getMatcher(engine);
	60	constraint2CurrentUnitPropagationPrecondition.put(constraint,matcher)
	61	}
	62	}
	63
	64	def getRuntime(){runtime}
	65	def getCachingTime(){cachingTime}
	66	def getNumberOfSolverCalls(){numberOfSolverCalls}
	67	def getNumberOfCachedSolverCalls(){numberOfCachedSolverCalls}
	68	def getSolverFormingProblem(){this.t.formingProblemTime}
	69	def getSolverSolvingProblem(){this.t.solvingProblemTime}
	70	def getSolverSolution(){this.t.formingSolutionTime}
	71
	72	def boolean maySatisfiable() {
	73	if(intermediateConsistencyCheck) {
	74	return isSatisfiable(this.constraint2MustUnitPropagationPrecondition)
	75	} else {
	76	return true
	77	}
	78	}
	79	def boolean currentSatisfiable() {
	80	isSatisfiable(this.constraint2CurrentUnitPropagationPrecondition)
	81	}
	82
	83	private def boolean isSatisfiable(Map<PConstraint,ViatraQueryMatcher<? extends IPatternMatch>> matches) {
	84	val start = System.nanoTime
	85	var boolean finalResult
	86	if(matches.empty){
	87	finalResult=true
	88	} else {
	89	val propagatedConstraints = new HashMap
	90	for(entry : matches.entrySet) {
	91	val constraint = entry.key
	92	//println(constraint)
	93	val allMatches = entry.value.allMatches.map[it.toArray]
	94	//println(allMatches.toList)
	95	propagatedConstraints.put(constraint,allMatches)
	96	}
	97	if(propagatedConstraints.values.forall[empty]) {
	98	finalResult=true
	99	} else {
	100	if(caching) {
	101	val code = getCode(propagatedConstraints)
	102	val cachedResult = satisfiabilityCache.get(code)
	103	if(cachedResult === null) {
	104	// println('''new problem, call solver''')
	105	// for(entry : code.entrySet) {
	106	// println('''«entry.key» -> «entry.value»''')
	107	// }
	108	//println(code.hashCode)
	109	this.numberOfSolverCalls++
	110	val res = t.delegateIsSatisfiable(propagatedConstraints)
	111	satisfiabilityCache.put(code,res)
	112	finalResult=res
	113	} else {
	114	//println('''similar problem, answer from cache''')
	115	finalResult=cachedResult
	116	this.numberOfCachedSolverCalls++
	117	}
	118	} else {
	119	finalResult= t.delegateIsSatisfiable(propagatedConstraints)
	120	this.numberOfSolverCalls++
	121	}
	122	}
	123	}
	124	this.runtime+=System.nanoTime-start
	125	return finalResult
	126	}
	127
	128	def getCode(HashMap<PConstraint, Iterable<Object[]>> propagatedConstraints) {
	129	val start = System.nanoTime
	130	val involvedObjects = new LinkedHashSet(propagatedConstraints.values.flatten.map[toList].flatten.toList).toList
	131	val res = new LinkedHashMap(propagatedConstraints.mapValues[matches \| matches.map[objects \| objects.map[object \| involvedObjects.indexOf(object)].toList]])
	132	this.cachingTime += System.nanoTime-start
	133	return res
	134	}
	135
	136	def fillSolutionCopy(Map<EObject, EObject> trace) {
	137	val model = threadContext.getModel as PartialInterpretation
	138	val dataObjects = model.newElements.filter(PrimitiveElement).filter[!model.openWorldElements.contains(it)].toList
	139	if(constraint2CurrentUnitPropagationPrecondition.empty) {
	140	fillWithDefaultValues(dataObjects,trace)
	141	} else {
	142	val propagatedConstraints = new HashMap
	143	for(entry : constraint2CurrentUnitPropagationPrecondition.entrySet) {
	144	val constraint = entry.key
	145	val allMatches = entry.value.allMatches.map[it.toArray]
	146	propagatedConstraints.put(constraint,allMatches)
	147	}
	148
	149	if(propagatedConstraints.values.forall[empty]) {
	150	fillWithDefaultValues(dataObjects,trace)
	151	} else {
	152	val solution = t.delegateGetSolution(dataObjects,propagatedConstraints)
	153	fillWithSolutions(dataObjects,solution,trace)
	154	}
	155	}
	156	}
	157
	158	def protected fillWithDefaultValues(List<PrimitiveElement> elements, Map<EObject, EObject> trace) {
	159	for(element : elements) {
	160	if(element.valueSet==false) {
	161	val value = getDefaultValue(element)
	162	val target = trace.get(element) as PrimitiveElement
	163	target.fillWithValue(value)
	164	}
	165	}
	166	}
	167
	168	def protected dispatch getDefaultValue(BooleanElement e) {false}
	169	def protected dispatch getDefaultValue(IntegerElement e) {0}
	170	def protected dispatch getDefaultValue(RealElement e) {0.0}
	171	def protected dispatch getDefaultValue(StringElement e) {""}
	172
	173	def protected fillWithSolutions(List<PrimitiveElement> elements, Map<PrimitiveElement, Number> solution, Map<EObject, EObject> trace) {
	174	for(element : elements) {
	175	if(element.valueSet==false) {
	176	if(solution.containsKey(element)) {
	177	val value = solution.get(element)
	178	val target = trace.get(element) as PrimitiveElement
	179	target.fillWithValue(value)
	180	} else {
	181	val target = trace.get(element) as PrimitiveElement
	182	target.fillWithValue(target.defaultValue)
	183	}
	184	}
	185	}
	186	}
	187
	188	def protected dispatch fillWithValue(BooleanElement e, Object value) {e.valueSet=true e.value=value as Boolean}
	189	def protected dispatch fillWithValue(IntegerElement e, Object value) {e.valueSet=true e.value=value as Integer}
	190	def protected dispatch fillWithValue(RealElement e, Object value) {e.valueSet=true e.value=BigDecimal.valueOf(value as Double) }
	191	def protected dispatch fillWithValue(StringElement e, Object value) {e.valueSet=true e.value=value as String}
	192	} \ No newline at end of file