Databases
StackOverflow2013
Postsdbo
POUse Z3 managed API on Mono
 

Note that there are some explanatory texts on larger screens.

plurals
  1. POUse Z3 managed API on Mono
    primarykey
    data
    text
    <p>We have a .NET project using Z3 API v4.0. We would like to be able to compile and run the project on Mono.</p> <p>The project compiled fine with MonoDevelop. However, when we run or debugged the program, the following exception occurred</p> <pre><code>System.DllNotFoundException: z3.dll at (wrapper managed-to-native) Microsoft.Z3.Native/LIB:Z3_mk_context_rc (intptr) at Microsoft.Z3.Native.Z3_mk_context_rc (IntPtr a0) [0x00000] in &lt;filename unknown&gt;:0 at Microsoft.Z3.Context..ctor () [0x00000] in &lt;filename unknown&gt;:0 at &lt;StartupCode$Nqueens&gt;.$Nqueens..cctor () [0x00000] in /path/to/file:15 </code></pre> <p>We used Mac OS X and Mono 3.0.2/MonoDevelop 3.0.5 if that matters.</p> <p><em>Has anyone had experience using Z3 API on Mono?</em></p> <p>It sounds like a weird idea, but our situation is described as follows. We have a course using Z3 and all lab computers have Windows and .NET framework installed. However, some students working on their own computers (Linux, Mac) should be able to compile and run the project.</p> <hr> <p><strong>Summary:</strong></p> <p>Thanks to @Leo's suggestion, I am able to run the project under MonoDevelop with a few changes:</p> <p>1) Create an <code>App.config</code> file and add the following information under <code>configuration</code> tag:</p> <pre><code>&lt;dllmap dll="z3.dll" target="libz3.dylib" os="osx" cpu="x86"/&gt; </code></pre> <p>2) Copy <code>libz3.dylib</code> from Mac OS X distribution (or build from source for newer versions) and make sure the shared library and <code>Microsoft.Z3.dll</code> are copied to output folder (<code>bin/Debug</code> on <code>Debug</code> mode) when compiling the project. For this purpose, we manually add to <code>ItemGroup</code> tag in the project file:</p> <pre><code>&lt;None Include="libz3.dylib"&gt; &lt;CopyToOutputDirectory&gt;Always&lt;/CopyToOutputDirectory&gt; &lt;Visible&gt;False&lt;/Visible&gt; &lt;/None&gt; </code></pre> <p>The process should be similar for <code>libz3.so</code> on Linux.</p> <p>We have tried various examples with different theories. There is no error or exception occurring so far.</p>
    singulars
    1. PO
      singulars
      1. PTAnswer
    1. This table or related slice is empty.
    1. PTQuestion
    1. USpad
    1. USpad
    plurals
    1. This table or related slice is empty.
    1. This table or related slice is empty.
    1. This table or related slice is empty.
    1. PO
      singulars
      1. PTAnswer
    1. VO
      singulars
      1. POUse Z3 managed API on Mono
      1. This table or related slice is empty.
      1. VTDownMod
    2. VO
      singulars
      1. POUse Z3 managed API on Mono
      1. This table or related slice is empty.
      1. VTUpMod
    3. VO
      singulars
      1. POUse Z3 managed API on Mono
      1. This table or related slice is empty.
      1. VTUpMod
    1. COWhy the uncommented downvote?
      singulars
      1. POUse Z3 managed API on Mono
      1. USpad
    2. COFYI, I tried this on Linux (Ubuntu) with Mono and libz3.so (compiled from the unstable branch on codeplex) and it also seems to work fine so far.
      singulars
      1. POUse Z3 managed API on Mono
      1. USTaylor
    3. CO@Taylor: Thanks. It indeed makes our student experience with the course much nicer.
      singulars
      1. POUse Z3 managed API on Mono
      1. USpad
 

Querying!

 
Guidance
A row detail

Detail views are divided into sections. All the information in the data section comes from columns in the selected row. The other sections display data from other, related rows.

Related data can be related in a to-one or a to-many fashion. Captions of data related in a to-many fashion link to a list view showing a filtered view of the table.

Try moving around until you find a non-empty to-many entry and click on the label to get to one. You can move back to the root by clicking on the database name in the header.

SQuiL has stopped working due to an internal error.

If you are curious you may find further information in the browser console, which is accessible through the devtools (F12).

Reload