diff --git a/src/main/java/common/ConfigurationTTool.java b/src/main/java/common/ConfigurationTTool.java
index 89ee1289482e0189fd96831a50a105a8618ef2c9..05ab636c1568fdf59e8406396061bd6a189727a5 100755
--- a/src/main/java/common/ConfigurationTTool.java
+++ b/src/main/java/common/ConfigurationTTool.java
@@ -1682,4 +1682,43 @@ public class ConfigurationTTool {
}
}
+ // Returns an error string in case of failure
+ public static String loadZ3Libs() {
+ if ((ConfigurationTTool.Z3LIBS == null) || (ConfigurationTTool.Z3LIBS.length() == 0)) {
+ return "Z3 libraries not configured.\n Set them in configuration file (e.g. config.xml)\n" +
+ "For instance:\n<Z3LIBS data=\"/opt/z3/bin/libz3.so:/opt/z3/bin/libz3java.so\" />\n";
+ }
+
+ try {
+
+
+
+ String [] libs = ConfigurationTTool.Z3LIBS.split(":");
+ boolean setLibPath = false;
+
+ for (int i=0; i<libs.length; i++) {
+ // get the path and set it as a property of java lib path
+
+
+
+ String tmp = libs[i].trim();
+ if (tmp.length() > 0) {
+ if (setLibPath == false) {
+ File f = new File(tmp);
+ String dir = f.getParent();
+ System.setProperty("java.library.path", dir);
+ setLibPath = true;
+ }
+ TraceManager.addDev("Loading Z3 lib: " + tmp);
+ System.load(tmp);
+ }
+ }
+
+ } catch (UnsatisfiedLinkError e) {
+ return ("Z3 libs + " + ConfigurationTTool.Z3LIBS + " could not be loaded\n");
+ }
+
+ return null;
+ }
+
} //
diff --git a/src/main/java/tmltranslator/dsez3engine/OptimizationModel.java b/src/main/java/tmltranslator/dsez3engine/OptimizationModel.java
index 4c425580778c7321eb3c30e75b66655fb45b7100..96ee9a13b36c87b9af3f1eed8aeec317b53e589d 100644
--- a/src/main/java/tmltranslator/dsez3engine/OptimizationModel.java
+++ b/src/main/java/tmltranslator/dsez3engine/OptimizationModel.java
@@ -75,9 +75,46 @@ public class OptimizationModel {
return result;
}
+ public OptimizationResult findFeasibleMapping() {
+ Context ctx;
+ OptimizationResult result = null;
+ try {
+
+ // These examples need model generation turned on.
+ HashMap<String, String> cfg = new HashMap<String, String>();
+ cfg.put("model", "true");
+ ctx = new Context(cfg);
+
+
+ result = findFeasibleMapping(ctx);
+
+ Log.close();
+ if (Log.isOpen())
+ TraceManager.addDev("Log is still open!");
+ } catch (Z3Exception ex) {
+ TraceManager.addDev("Z3 Managed Exception: " + ex.getMessage());
+ TraceManager.addDev("Stack trace: ");
+ ex.printStackTrace(
+ System.out);
+ if (result == null) {
+ result = new OptimizationResult();
+ }
+ result.error = "Z3 Exception: " + ex.getMessage();
+ } catch (Exception ex) {
+ TraceManager.addDev("Unknown Exception: " + ex.getMessage());
+ TraceManager.addDev("Stack trace: ");
+ ex.printStackTrace(System.out);
+ if (result == null) {
+ result = new OptimizationResult();
+ }
+ result.error = "Z3 Unknown Exception: " + ex.getMessage();
+ }
+ return result;
+ }
- public void findFeasibleMapping(Context ctx) throws TestFailedException {
+ public OptimizationResult findFeasibleMapping(Context ctx) {
+ OptimizationResult result = new OptimizationResult();
TraceManager.addDev("\nFind feasible Mapping");
//Decision variables
@@ -393,14 +430,17 @@ public class OptimizationModel {
TraceManager.addDev("start[" + taskCast.getName() + "] = " + optimized_result_start[t]);
}
-
+ result.result = "Feasible mapping found";
} else {
- TraceManager.addDev("Failed to solve mapping problem");
- throw new TestFailedException();
+ TraceManager.addDev("No suitable mapping could be found");
+ result.mappingFound = false;
}
+ return result;
+
+
}//findFeasibleMapping()
diff --git a/src/main/java/ui/window/JDialogDSEZ3.java b/src/main/java/ui/window/JDialogDSEZ3.java
index 3d75afdaf4b1f136d9d1bf1ba9c55fb4a63c5209..8d1ae3a22367250e883421b6368047ed1c48efd6 100644
--- a/src/main/java/ui/window/JDialogDSEZ3.java
+++ b/src/main/java/ui/window/JDialogDSEZ3.java
@@ -63,6 +63,7 @@ import javax.swing.event.ListSelectionListener;
import java.awt.*;
import java.awt.event.ActionEvent;
import java.awt.event.ActionListener;
+import java.io.File;
import java.util.*;
@@ -316,7 +317,7 @@ public class JDialogDSEZ3 extends JDialog implements ActionListener, ListSelecti
outputText.append("Loading Z3 libs\n");
- String error = loadZ3Libs();
+ String error = ConfigurationTTool.loadZ3Libs();
if (error != null) {
outputText.append(error);
@@ -324,21 +325,8 @@ public class JDialogDSEZ3 extends JDialog implements ActionListener, ListSelecti
return;
}
+ outputText.append("Z3 libs loaded.\n\n");
-
- /*try {
- System.load("/opt/z3/bin/libz3.so");
- System.load("/opt/z3/bin/libz3java.so");
- } catch (UnsatisfiedLinkError e) {
- outputText.append("Z3 lib could not be loaded\n");
- stopProcess();
- return;
- }*/
-
- outputText.append("Z3 libs loaded.\n");
-
-
- Context ctx = null;
outputText.append("Looking for optimized mapping, please wait\n");
OptimizationResult result = null;
try {
@@ -364,29 +352,7 @@ public class JDialogDSEZ3 extends JDialog implements ActionListener, ListSelecti
}
- // Returns an error string in case of failure
- private String loadZ3Libs() {
- if ((ConfigurationTTool.Z3LIBS == null) || (ConfigurationTTool.Z3LIBS.length() == 0)) {
- return "Z3 libraries not configured.\n Set them in configuration file (e.g. config.xml)\n" +
- "For instance:\n<Z3LIBS data=\"/opt/z3/bin/libz3.so:/opt/z3/bin/libz3java.so\" />\n";
- }
-
- try {
- String [] libs = ConfigurationTTool.Z3LIBS.split(":");
- for (int i=0; i<libs.length; i++) {
- String tmp = libs[i].trim();
- if (tmp.length() > 0) {
- TraceManager.addDev("Loading Z3 lib: " + tmp);
- System.load(tmp);
- }
- }
- } catch (UnsatisfiedLinkError e) {
- return ("Z3 libs + " + ConfigurationTTool.Z3LIBS + " could not be loaded\n");
- }
-
- return null;
- }
diff --git a/ttool/src/test/java/tmltranslator/dsez3engine/InputInstanceTest.java b/ttool/src/test/java/tmltranslator/dsez3engine/InputInstanceTest.java
index 89bfd2a0e55a36de72fe954cf7c36c1a41aeb251..ec7d3ae149c3a7ebcea0189e07dc9c3078b03fe1 100644
--- a/ttool/src/test/java/tmltranslator/dsez3engine/InputInstanceTest.java
+++ b/ttool/src/test/java/tmltranslator/dsez3engine/InputInstanceTest.java
@@ -1,6 +1,7 @@
package tmltranslator.dsez3engine;
import com.microsoft.z3.*;
+import common.ConfigurationTTool;
import org.junit.Assert;
import org.junit.Before;
import org.junit.Test;
@@ -205,33 +206,26 @@ public class InputInstanceTest {
@Test
public void findOptimizedMapping() {
- try {
-
- // These examples need model generation turned on.
- HashMap<String, String> cfg = new HashMap<String, String>();
- cfg.put("model", "true");
- Context ctx = new Context(cfg);
-
-
- optimizationModel.findOptimizedMapping(ctx);
+ String error = ConfigurationTTool.loadZ3Libs();
+ if (error != null) {
+ // we cannot run the test since Z3 is not installed
+ return;
+ }
+ OptimizationResult result = optimizationModel.findOptimizedMapping();
Log.close();
- if (Log.isOpen())
+ /*if (Log.isOpen())
TraceManager.addDev("Log is still open!");
} catch (Z3Exception ex) {
- TraceManager.addDev("Z3 Managed Exception: " + ex.getMessage());
- TraceManager.addDev("Stack trace: ");
- ex.printStackTrace(
- System.out);
- } catch (OptimizationModel.TestFailedException ex) {
- TraceManager.addDev("TEST CASE FAILED: " + ex.getMessage());
- TraceManager.addDev("Stack trace: ");
- ex.printStackTrace(System.out);
+ TraceManager.addDev("Z3 Managed Exception: " + ex.getMessage());
+ TraceManager.addDev("Stack trace: ");
+ ex.printStackTrace(
+ System.out);
} catch (Exception ex) {
TraceManager.addDev("Unknown Exception: " + ex.getMessage());
TraceManager.addDev("Stack trace: ");
ex.printStackTrace(System.out);
- }
+ }*/
assertEquals(1, optimizationModel.getOptimizedSolutionX().get("X[task__A][MainCPU] = ").intValue());
assertEquals(0, optimizationModel.getOptimizedSolutionX().get("X[task__A][dsp] = ").intValue());
@@ -252,34 +246,15 @@ public class InputInstanceTest {
@Test
public void findFeasibleMapping() {
-
- try {
-
- // These examples need model generation turned on.
- HashMap<String, String> cfg = new HashMap<String, String>();
- cfg.put("model", "true");
- Context ctx = new Context(cfg);
-
-
- optimizationModel.findFeasibleMapping(ctx);
+ String error = ConfigurationTTool.loadZ3Libs();
+ if (error != null) {
+ // we cannot run the test since Z3 is not installed
+ return;
+ }
+ OptimizationResult result = optimizationModel.findFeasibleMapping();
Log.close();
- if (Log.isOpen())
- TraceManager.addDev("Log is still open!");
- } catch (Z3Exception ex) {
- TraceManager.addDev("Z3 Managed Exception: " + ex.getMessage());
- TraceManager.addDev("Stack trace: ");
- ex.printStackTrace(
- System.out);
- } catch (OptimizationModel.TestFailedException ex) {
- TraceManager.addDev("TEST CASE FAILED: " + ex.getMessage());
- TraceManager.addDev("Stack trace: ");
- ex.printStackTrace(System.out);
- } catch (Exception ex) {
- TraceManager.addDev("Unknown Exception: " + ex.getMessage());
- TraceManager.addDev("Stack trace: ");
- ex.printStackTrace(System.out);
- }
+
}