diff options
Diffstat (limited to 'Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme')
-rw-r--r-- | Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericProblemSolver.java | 39 |
1 files changed, 29 insertions, 10 deletions
diff --git a/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericProblemSolver.java b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericProblemSolver.java index 070b71ad..a5b9fc66 100644 --- a/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericProblemSolver.java +++ b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericProblemSolver.java | |||
@@ -56,6 +56,10 @@ public class NumericProblemSolver { | |||
56 | private Context ctx; | 56 | private Context ctx; |
57 | private Solver s; | 57 | private Solver s; |
58 | private Map<Object, Expr> varMap; | 58 | private Map<Object, Expr> varMap; |
59 | |||
60 | long endformingProblem=0; | ||
61 | long endSolvingProblem=0; | ||
62 | long endFormingSolution=0; | ||
59 | 63 | ||
60 | public NumericProblemSolver() { | 64 | public NumericProblemSolver() { |
61 | HashMap<String, String> cfg = new HashMap<String, String>(); | 65 | HashMap<String, String> cfg = new HashMap<String, String>(); |
@@ -70,7 +74,18 @@ public class NumericProblemSolver { | |||
70 | return ctx; | 74 | return ctx; |
71 | } | 75 | } |
72 | 76 | ||
73 | 77 | public long getEndformingProblem() { | |
78 | return endformingProblem; | ||
79 | } | ||
80 | |||
81 | public long getEndSolvingProblem() { | ||
82 | return endSolvingProblem; | ||
83 | } | ||
84 | |||
85 | public long getEndFormingSolution() { | ||
86 | return endFormingSolution; | ||
87 | } | ||
88 | |||
74 | private ArrayList<JvmIdentifiableElement> getJvmIdentifiableElements(XExpression expression) { | 89 | private ArrayList<JvmIdentifiableElement> getJvmIdentifiableElements(XExpression expression) { |
75 | ArrayList<JvmIdentifiableElement> allElem = new ArrayList<JvmIdentifiableElement>(); | 90 | ArrayList<JvmIdentifiableElement> allElem = new ArrayList<JvmIdentifiableElement>(); |
76 | XExpression left = ((XBinaryOperation) expression).getLeftOperand(); | 91 | XExpression left = ((XBinaryOperation) expression).getLeftOperand(); |
@@ -91,26 +106,30 @@ public class NumericProblemSolver { | |||
91 | } | 106 | } |
92 | 107 | ||
93 | public boolean isSatisfiable(Map<XExpression, Iterable<Map<JvmIdentifiableElement,PrimitiveElement>>> matches) throws Exception { | 108 | public boolean isSatisfiable(Map<XExpression, Iterable<Map<JvmIdentifiableElement,PrimitiveElement>>> matches) throws Exception { |
109 | long startformingProblem = System.nanoTime(); | ||
94 | BoolExpr problemInstance = formNumericProblemInstance(matches); | 110 | BoolExpr problemInstance = formNumericProblemInstance(matches); |
95 | s.add(problemInstance); | 111 | s.add(problemInstance); |
112 | endformingProblem = System.nanoTime()-startformingProblem; | ||
113 | long startSolvingProblem = System.nanoTime(); | ||
96 | boolean result = (s.check() == Status.SATISFIABLE); | 114 | boolean result = (s.check() == Status.SATISFIABLE); |
115 | endSolvingProblem = System.nanoTime()-startSolvingProblem; | ||
97 | this.ctx.close(); | 116 | this.ctx.close(); |
98 | return result; | 117 | return result; |
99 | } | 118 | } |
100 | 119 | ||
101 | public Map<PrimitiveElement,Number> getOneSolution(List<PrimitiveElement> objs, Map<XExpression, Iterable<Map<JvmIdentifiableElement,PrimitiveElement>>> matches) throws Exception { | 120 | public Map<PrimitiveElement,Number> getOneSolution(List<PrimitiveElement> objs, Map<XExpression, Iterable<Map<JvmIdentifiableElement,PrimitiveElement>>> matches) throws Exception { |
102 | Map<PrimitiveElement,Number> sol = new HashMap<PrimitiveElement, Number>(); | 121 | Map<PrimitiveElement,Number> sol = new HashMap<PrimitiveElement, Number>(); |
103 | long startformingProblem = System.currentTimeMillis(); | 122 | long startformingProblem = System.nanoTime(); |
104 | BoolExpr problemInstance = formNumericProblemInstance(matches); | 123 | BoolExpr problemInstance = formNumericProblemInstance(matches); |
105 | long endformingProblem = System.currentTimeMillis(); | 124 | endformingProblem = System.nanoTime()-startformingProblem; |
106 | System.out.println("Forming problem: " + (endformingProblem - startformingProblem)); | 125 | //System.out.println("Forming problem: " + (endformingProblem - startformingProblem)); |
107 | s.add(problemInstance); | 126 | s.add(problemInstance); |
108 | long startSolvingProblem = System.currentTimeMillis(); | 127 | long startSolvingProblem = System.nanoTime(); |
109 | if (s.check() == Status.SATISFIABLE) { | 128 | if (s.check() == Status.SATISFIABLE) { |
110 | Model m = s.getModel(); | 129 | Model m = s.getModel(); |
111 | long endSolvingProblem = System.currentTimeMillis(); | 130 | endSolvingProblem = System.nanoTime()-startSolvingProblem; |
112 | System.out.println("Solving problem: " + (endSolvingProblem - startSolvingProblem)); | 131 | System.out.println("Solving problem: " + (endSolvingProblem - startSolvingProblem)); |
113 | long startFormingSolution = System.currentTimeMillis(); | 132 | long startFormingSolution = System.nanoTime(); |
114 | for (PrimitiveElement o: objs) { | 133 | for (PrimitiveElement o: objs) { |
115 | if(varMap.containsKey(o)) { | 134 | if(varMap.containsKey(o)) { |
116 | if (o instanceof IntegerElement) { | 135 | if (o instanceof IntegerElement) { |
@@ -128,10 +147,10 @@ public class NumericProblemSolver { | |||
128 | //System.out.println("not used var:" + o); | 147 | //System.out.println("not used var:" + o); |
129 | } | 148 | } |
130 | } | 149 | } |
131 | long endFormingSolution = System.currentTimeMillis(); | 150 | endFormingSolution = System.nanoTime()-startFormingSolution; |
132 | System.out.println("Forming solution: " + (endFormingSolution - startFormingSolution)); | 151 | //System.out.println("Forming solution: " + (endFormingSolution - startFormingSolution)); |
133 | } else { | 152 | } else { |
134 | System.out.println("Unsatisfiable"); | 153 | System.out.println("Unsatisfiable numerical problem"); |
135 | } | 154 | } |
136 | this.ctx.close(); | 155 | this.ctx.close(); |
137 | return sol; | 156 | return sol; |