Commit 9456ad3c authored by Hernan Ponce de Leon's avatar Hernan Ponce de Leon
Browse files

Merge remote-tracking branch 'origin/master' into 3465-IStatementTerm_toZ3

parents 9d3a2981 cccdb14e
<?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"/>
......
documentation.html d453042662ce194dd18088037f800ed7c5b9f647 GREEN
<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