ScalaZ3 and Visual Studio 2012 Express for Windows Desktop

Locate z3.lib

z3.lib is needed for access to Z3's C/C++ API. Ages ago, this was provided as a precompiled binary for Windows. It can be rebuilt easily from the source code release for Z3 version 4.1.2 at http://z3.codeplex.com/releases/view/95754. The Visual C++ solution and projects are included: just open the top-level solution z3-prover.sln and select test_capi as your start-up project. I recommend starting with the Release Configuration targetting the x64 platform. The project dependencies are pre-configured. You will also need to open dll.rc in an editor and manually edit the line "#include afxres.h" to read "#include "WinResrc.h"" as described at http://stackoverflow.com/a/17454415/201008.

This step will test your resolve to continue further down the route of using Visual Studio 2012 Express. You will see.

Once you have a z3.lib built for the x64 platform, change the platform to x86 and rebuild in order to support 32-bit Java VMs.

Create a local clone of the ScalaZ3 repository

Version control software is available from GitHub. This doucment is based on the source clonable from https://github.com/epfl-lara/ScalaZ3/tree/2.9.x.

Create an Eclipse Workspace

The version of Eclipse used during creation of this document was Indigo. Suggested workspace location is in MyDocuments\GitHub. This is the default location beneath which GitHub stores local copies of projects you have cloned.

Import ScalaZ3 as a new Scala Project within Eclipse.

Suggested project location (within workspace MyDocuments\GitHub) is ScalaZ3. This is the default location where GitHub stores local clones of the ScalaZ3 project. If you have cloned ScalaZ3 as above, Eclipse will configure .\src\main\java, .\src\main\scala and .\src\test as source folders. Set the output class folder to ScalaZ3\target\scala-2.9.x\classes.

Use Eclipse to Build classpath for ScalaZ3

Use Eclipse to build the classpath. This will fail with one error:

LibraryChecksum cannot be resolved to a variable	Z3Wrapper.java	/ScalaZ3/src/main/java/z3	line 27	Java Problem

You can eliminate this by creating a file named LibraryChecksum.java in folder target\java\z3 with the following contents:

''' package z3;

public class LibraryChecksum { static String value = "TODO: Specific Library Checksum Here"; } '''

Create the JNI headers

You need the compiled classfiles and the javah from the JDK for this. On my host, the JNI headers compile only under the 2.9.x branch, using the rather long command name:

"C:\Program Files\Java\jdk1.7.0_21\bin\javah.exe" -classpath .\target\scala-2.9.x\classes; C:\eclipse\configuration\org.eclipse.osgi\bundles\808\1\.cp\lib\scala-library.jar
-d target\c\include z3.Z3Wrapper

An alternative to the command line is to set up Eclipse External Tools. This simplifies the command somewhat because variables can be used instead of the hard-coded paths above. To date I have not found a variable that returns the fully qualified path of the scala-library.jar. Consequently this option requires customizing the eclipse variables by adding one that points to the fully qualified name as copied to the clipboard by eclipse from the package explorer. I was hoping it would be simpler, something like ${pathto:scala-library.jar}.

Create a Visual C++ project

1. From the Start Page, choose New Project
2. Choose to create a Win32 Project.
3. Create the project in the ScalaZ3 projects folder. It's not necessary to create a subfolder for the project.
4. Under Application Settings, select the DLL application type. Also check the empty project checkbox.
5. Give the project the name libscalaz3 or scalaz3 (see notes).
6. Click Finish to create the project.
7. Add the files from ScalaZ3: src/c to the project.
8. Under the Project Properties, set the Configuration Property C/C++ Precompiled Headers to "not using precompiled headers".
9. Under additional include directories, add ".\target\c\include;" and the path to the include location of the JDK (e.g C:\Program Files\Java\jdk1.7.0_21\include\win32) and the path to Z3 (e.g. C:\z3-4.3.0-x64\include)

You will probably want to add 32-bit and 64-bit configurations. The DLL configuration must match the version of the Java VM (32-bit or 64-bit) installed. The above instructions will create the 32-bit configuration by default. To copy the settings for 64-bit configuration, run the Configuration Manager from the Project Properties dialog.

(Optional) Migrate the Windows DLL project to Eclipse

An article discussing the procedure for migrating Visual Studio projects to makefiles for use in the Eclipse environment can be found at http://www.ibm.com/developerworks/library/os-ecl-vscdt/index.html?ca=dgr-eclipse-1