1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
|
package hu.bme.mit.inf.dslreasoner.viatra2logic
import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PrimitiveElement
import java.util.ArrayList
import java.util.Comparator
import java.util.HashMap
import java.util.List
import java.util.Map
import java.util.Map.Entry
import org.eclipse.viatra.query.runtime.matchers.psystem.PConstraint
import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.ExpressionEvaluation
import org.eclipse.xtext.common.types.JvmIdentifiableElement
import org.eclipse.xtext.xbase.XExpression
import org.eclipse.xtext.xbase.XFeatureCall
class NumericTranslator {
private XExpressionExtractor extractor = new XExpressionExtractor();
private NumericProblemSolver numericSolver;
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)
}
}
new(NumericProblemSolver numericProblemSolver){
this.numericSolver = numericProblemSolver
}
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 NumericProblemSolver selectProblemSolver(String selection) {
// return new NumericProblemSolver
// add numeric solver decision procedure here
if (numericSolver instanceof NumericDynamicProblemSolver) {
val NumericDynamicProblemSolver dynamicSolver = numericSolver as NumericDynamicProblemSolver
return dynamicSolver.selectSolver(selection);
} else{
if (numericSolver instanceof NumericZ3ProblemSolver) return new NumericZ3ProblemSolver
return numericSolver;
}
}
def delegateIsSatisfiable(Map<PConstraint, Iterable<Object[]>> matches, String select) {
val input = formNumericProblemInstance(matches)
val solver = selectProblemSolver(select)
val satisfiability = solver.isSatisfiable(input)
solver.updateTimes
return satisfiability
}
def delegateGetSolution(List<PrimitiveElement> primitiveElements, Map<PConstraint, Iterable<Object[]>> matches, String select) {
val input = formNumericProblemInstance(matches)
val solver = selectProblemSolver(select)
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}
def getNumericSolver(){numericSolver}
}
|
