From 3776a7c6bc1d6fc3ebbdc9e8afb5ea99207798e0 Mon Sep 17 00:00:00 2001
From: Oszkar Semerath <semerath@mit.bme.hu>
Date: Sat, 9 May 2020 20:33:19 +0200
Subject: Numeric Solver integration to exploration

---
 .../viatra2logic/NumericTranslator.xtend           | 64 ++++++++++++++++++++++
 1 file changed, 64 insertions(+)
 create mode 100644 Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericTranslator.xtend

(limited to 'Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericTranslator.xtend')

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..89719b91
--- /dev/null
+++ b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericTranslator.xtend
@@ -0,0 +1,64 @@
+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();
+	
+	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)
+		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)
+		return solution
+	}
+}
\ No newline at end of file
-- 
cgit v1.2.3-70-g09d2