Skip to content
GitLab
Commit 7187fa44 authored by aziz's avatar aziz
Browse files

Merge remote-tracking branch 'origin/master' into 2802-FMU_Cosimulation 




Signed-off-by: default avataraziz <aziz@fortiss.org>
parents 7d05a1d9 cccdb14e
Hide whitespace changes
Inline Side-by-side
com.microsoft.z3/.classpath
View file @ 7187fa44
<?xml version="1.0" encoding="UTF-8"?>
<classpath>
<classpathentry exported="true" kind="lib" path="lib/com.microsoft.z3.jar"/>
<classpathentry exported="true" kind="lib" path="lib/com.microsoft.z3.jar" sourcepath="lib/com.microsoft.z3-src.jar"/>
<classpathentry kind="con" path="org.eclipse.jdt.launching.JRE_CONTAINER/org.eclipse.jdt.internal.debug.ui.launcher.StandardVMType/JavaSE-1.8"/>
<classpathentry kind="con" path="org.eclipse.pde.core.requiredPlugins"/>
<classpathentry kind="src" path="src"/>
......
com.microsoft.z3/html/developer/.ratings 0 → 100644
View file @ 7187fa44
documentation.html d453042662ce194dd18088037f800ed7c5b9f647 GREEN
com.microsoft.z3/html/developer/documentation.html 0 → 100644
View file @ 7187fa44
<html><body>
<h1>Developer Documentation for Microsoft Z3 Bundle (<i>com.microsoft.z3</i>)</h1>
This plugin bundles the Microsoft Z3 Theorem Prover. It provides the following:
<ul>
<li>Native libraries for Windows (x86, x64), Linux (x86, x64), and Mac OS X (x64)</li>
<li>Logic required to pre-load shared native libraries (implemented in the plugin activator)</li>
<li>Z3 Java bindings</li>
<li>API wrapper that implements convenience functions to work with Z3.</li>
</ul>
The binary distribution of Z3 consists of several native shared libraries that depend on each other. This setup requires different measures on the different operating systems and AF3 versions (notably: developer installation and binary RCP distribution).
<h2>Developer Installation</h2>
<h3>Windows</h3>
The pre-loading logic implemented in the activator is sufficient.
<h3>Linux</h3>
In the <i>Run/Debug Configuration</i>, the <code>LD_LIBRARY_PATH</code> environment variable needs to be set to <code>&#36;&#123;workspace_loc&#125/../git/af3/com.microsoft.z3/lib/x32</code>, or <code>&#36;&#123;workspace_loc&#125/../git/af3/com.microsoft.z3/lib/x64</code>, respectively (see <i>Environment</i> tab).
<h3>Mac OS X</h3>
In the <i>Run/Debug Configuration</i>, the <code>DYLD_LIBRARY_PATH</code> environment variable needs to be set to <code>&#36;&#123;workspace_loc&#125/../git/af3/com.microsoft.z3/lib/x64</code> (see <i>Environment</i> tab).
<h2>RCP Distribution</h2>
<h3>Windows</h3>
The pre-loading logic implemented in the activator is sufficient.
<h3>Linux</h3>
A wrapper shell script that sets <code>LD_LIBRARY_PATH</code> is generated by the following snippet in the <code>af3-phoenix-04-product-linux</code> Jenkins job.
<pre>
msdir=$(find . -name 'com.microsoft.z3_[\.0-9]*' -type d)
echo '#!/bin/bash' > autofocus3-phoenix
echo "LD_LIBRARY_PATH=\$LD_LIBRARY_PATH:${msdir}/lib/x64 ./autofocus3-phoenix.bin \$*" >> autofocus3-phoenix
chmod a+x autofocus3-phoenix
</pre>
<h3>Mac OS X</h3>
<p>Since a native Mac OS application is desired, using the a wrapper script that sets the <code>LD_LIBRARY_PATH</code> environment variable in the UNIX sub system is not an option.</p>
<p>However, the equivalent <code>DYLD_LIBRARY_PATH</code> in the native Mac subsystem, is nowadays purged by <a href=" https://developer.apple.com/library/content/documentation/Security/Conceptual/System_Integrity_Protection_Guide/RuntimeProtections/RuntimeProtections.html">Mac OS X System Integrity Protection</a>.
Therefore, the native libraries are copied the Eclipse launcher directory (since shared libraries residing in the same directory as the application are found). This is performed by the following script in the <code>af3-phoenix-04-product-macosx</code> Jenkins job.
<pre>
# See https://af3-developer.fortiss.org/issues/3385
echo "Copying native Z3 libs to Eclipse launcher directory"
Z3_LIB_DIR=$(find ../Eclipse -name 'com.microsoft.z3_[\.0-9]*')
cp $Z3_LIB_DIR/lib/x64/*.dylib .
</pre>
</body>
</html>
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment