1 files changed, 80 insertions, 0 deletions
diff --git a/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericTranslator.xtend b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericTranslator.xtend
new file mode 100644
index 00000000..81bc1796
--- /dev/null
+++ b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericTranslator.xtend
@@ -0,0 +1,80 @@
+package hu.bme.mit.inf.dslreasoner.viatra2logic
+import org.eclipse.xtext.xbase.XExpression
+import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.ExpressionEvaluation
+import org.eclipse.xtext.common.types.JvmIdentifiableElement
+import java.util.Set
+import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PrimitiveElement
+import java.util.Map
+import com.microsoft.z3.BoolExpr
+import org.eclipse.viatra.query.runtime.matchers.psystem.PConstraint
+import java.util.Map.Entry
+import org.eclipse.xtext.xbase.XFeatureCall
+import java.util.Comparator
+import java.util.ArrayList
+import java.util.HashMap
+import java.util.List
+class NumericTranslator {
+        
+        private XExpressionExtractor extractor = new XExpressionExtractor();
+        
+        long formingProblemTime=0;
+        long solvingProblemTime=0;
+        long formingSolutionTime=0;
+        
+        val comparator = new Comparator<JvmIdentifiableElement>(){
+                        override compare(JvmIdentifiableElement o1, JvmIdentifiableElement o2) {
+                                //println('''«o1.simpleName» - «o2.simpleName»''')
+                                o1.simpleName.compareTo(o2.simpleName)
+                        }
+                }
+        def Map<JvmIdentifiableElement, PrimitiveElement> arrayToMap(Object[] tuple, ArrayList<JvmIdentifiableElement> variablesInOrder) {
+                val res = new HashMap
+                for(var i=0; i<tuple.length; i++) {
+                        res.put(variablesInOrder.get(i),tuple.get(i) as PrimitiveElement)
+                }
+                return res
+        }
+        def formNumericProblemInstance(Map<PConstraint, Iterable<Object[]>> matches) throws Exception {
+                val res = new HashMap
+                for (Entry<PConstraint, Iterable<Object[]>> entry: matches.entrySet()) {
+                        val ExpressionEvaluation constraint = entry.getKey() as ExpressionEvaluation;
+                        val XExpression expression = extractor.extractExpression(constraint.getEvaluator());
+                        val Iterable<Object[]> tuples = entry.getValue();
+                        val features = expression.eAllContents.filter(XFeatureCall).map[it.feature].toSet
+                        val variablesInOrder = new ArrayList(features)
+                        variablesInOrder.toList.sort(comparator)
+                        //println(variablesInOrder)
+                        val map = tuples.map[it.arrayToMap(variablesInOrder)]
+                        res.put(expression,map)
+                }
+                return res
+        }
+        
+        def delegateIsSatisfiable(Map<PConstraint, Iterable<Object[]>> matches) {
+                val input = formNumericProblemInstance(matches)
+                val solver = new NumericProblemSolver
+                val satisfiability = solver.isSatisfiable(input)
+                solver.updateTimes
+                return satisfiability
+        }
+        
+        def delegateGetSolution(List<PrimitiveElement> primitiveElements, Map<PConstraint, Iterable<Object[]>> matches) {
+                val input = formNumericProblemInstance(matches)
+                val solver = new NumericProblemSolver
+                val solution = solver.getOneSolution(primitiveElements,input)
+                solver.updateTimes
+                return solution
+        }
+        
+        private def updateTimes(NumericProblemSolver s) {
+                this.formingProblemTime += s.getEndformingProblem
+                this.solvingProblemTime += s.getEndSolvingProblem
+                this.formingSolutionTime += s.getEndFormingSolution
+        }
+        
+        def getFormingProblemTime() {formingProblemTime}
+        def getSolvingProblemTime() {solvingProblemTime}
+        def getFormingSolutionTime() {formingSolutionTime}
+}
+\ No newline at end of file

diff --git a/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericTranslator.xtend b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericTranslator.xtend new file mode 100644 index 00000000..81bc1796 --- /dev/null +++ b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericTranslator.xtend
@@ -0,0 +1,80 @@
	1	package hu.bme.mit.inf.dslreasoner.viatra2logic
	2
	3	import org.eclipse.xtext.xbase.XExpression
	4	import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.ExpressionEvaluation
	5	import org.eclipse.xtext.common.types.JvmIdentifiableElement
	6	import java.util.Set
	7	import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PrimitiveElement
	8	import java.util.Map
	9	import com.microsoft.z3.BoolExpr
	10	import org.eclipse.viatra.query.runtime.matchers.psystem.PConstraint
	11	import java.util.Map.Entry
	12	import org.eclipse.xtext.xbase.XFeatureCall
	13	import java.util.Comparator
	14	import java.util.ArrayList
	15	import java.util.HashMap
	16	import java.util.List
	17
	18	class NumericTranslator {
	19
	20	private XExpressionExtractor extractor = new XExpressionExtractor();
	21
	22	long formingProblemTime=0;
	23	long solvingProblemTime=0;
	24	long formingSolutionTime=0;
	25
	26	val comparator = new Comparator<JvmIdentifiableElement>(){
	27	override compare(JvmIdentifiableElement o1, JvmIdentifiableElement o2) {
	28	//println('''«o1.simpleName» - «o2.simpleName»''')
	29	o1.simpleName.compareTo(o2.simpleName)
	30	}
	31	}
	32	def Map<JvmIdentifiableElement, PrimitiveElement> arrayToMap(Object[] tuple, ArrayList<JvmIdentifiableElement> variablesInOrder) {
	33	val res = new HashMap
	34	for(var i=0; i<tuple.length; i++) {
	35	res.put(variablesInOrder.get(i),tuple.get(i) as PrimitiveElement)
	36	}
	37	return res
	38	}
	39	def formNumericProblemInstance(Map<PConstraint, Iterable<Object[]>> matches) throws Exception {
	40	val res = new HashMap
	41	for (Entry<PConstraint, Iterable<Object[]>> entry: matches.entrySet()) {
	42	val ExpressionEvaluation constraint = entry.getKey() as ExpressionEvaluation;
	43	val XExpression expression = extractor.extractExpression(constraint.getEvaluator());
	44	val Iterable<Object[]> tuples = entry.getValue();
	45	val features = expression.eAllContents.filter(XFeatureCall).map[it.feature].toSet
	46	val variablesInOrder = new ArrayList(features)
	47	variablesInOrder.toList.sort(comparator)
	48	//println(variablesInOrder)
	49	val map = tuples.map[it.arrayToMap(variablesInOrder)]
	50	res.put(expression,map)
	51	}
	52	return res
	53	}
	54
	55	def delegateIsSatisfiable(Map<PConstraint, Iterable<Object[]>> matches) {
	56	val input = formNumericProblemInstance(matches)
	57	val solver = new NumericProblemSolver
	58	val satisfiability = solver.isSatisfiable(input)
	59	solver.updateTimes
	60	return satisfiability
	61	}
	62
	63	def delegateGetSolution(List<PrimitiveElement> primitiveElements, Map<PConstraint, Iterable<Object[]>> matches) {
	64	val input = formNumericProblemInstance(matches)
	65	val solver = new NumericProblemSolver
	66	val solution = solver.getOneSolution(primitiveElements,input)
	67	solver.updateTimes
	68	return solution
	69	}
	70
	71	private def updateTimes(NumericProblemSolver s) {
	72	this.formingProblemTime += s.getEndformingProblem
	73	this.solvingProblemTime += s.getEndSolvingProblem
	74	this.formingSolutionTime += s.getEndFormingSolution
	75	}
	76
	77	def getFormingProblemTime() {formingProblemTime}
	78	def getSolvingProblemTime() {solvingProblemTime}
	79	def getFormingSolutionTime() {formingSolutionTime}
	80	} \ No newline at end of file