-
Notifications
You must be signed in to change notification settings - Fork 34
ScalaZ3 and Visual Studio 2012 Express for Windows Desktop
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.
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.
Many of the changes discussed below have been incorporated into the branch located at: https://github.com/vo1stv/ScalaZ3/tree/VS2012Express
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.
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 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";
}
You need the compiled classfiles and the javah from the JDK for this. On my host, this requires 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 a user-defined variable (PATH_TO_ECLIPSE_SCALA) that maps 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}.
- Launch Visual Studio 2012 Express
- From the Start Page, choose New Project
- Choose to create a Win32 Project named scalaz3.
- Create the project in the MyDocuments\GitHub\ScalaZ3\projects folder. It's not necessary to create a subfolder for the project, but the IDE will probably create one called scalaz3 regardless.
- Under Application Settings, select the DLL application type. Also check the empty project checkbox.
- Click Finish to create the project.
- Add the files from ScalaZ3: src/c to the project.
- Under additional include directories, add "....\src\c" and "....\target\c\include;" and the path to the include location(s) of the JDK (e.g C:\Program Files (x86)\Java\jdk1.7.0_21\include and C:\Program Files (x86)\Java\jdk1.7.0_21\include\win32) and the path to Z3 (e.g. C:\z3-4.1.2\lib)
- Under Link options, add z3.lib. Also add the path to the Win32 (i.e 32-bit x86 platform) z3.lib library to the Additional Library Directories
- Edit src\c\casts.h to insert the following line after the include statement for jni.h:
#define inline
- Because of the issue discussed at http://stackoverflow.com/questions/6754126/msvc-vs-gcc-variable-declaration-in-function, a few edits are required to the C files to make them compatible with C89 conventions. The number of mods is small: functions Java_z3_Z3Wrapper_substitute and Java_z3_Z3Wrapper_mkTactic. The fix simply requires pre-declaring variables at the beginning of functions instead of mid-way through.
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.
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