Installing the Incremental SMT Re-resolution software tool (Eclipse IDE)

The incremental SMT tool uses Z3 to perform SMT analysis in the Cloud Deployment case study.

Download the Z3 software tool from the website: http://z3.codeplex.com

Z3 provides support for Java and following these instructions 
http://leodemoura.github.io/blog/2012/12/10/z3-for-java.html
the jar file "com.microsoft.z3.jar" can be built for your particular system architecture.

For logging purposes, the tool uses Apache log4j, available to download from:
http://logging.apache.org/log4j/1.2/download.html

Download the Eclipse IDE from http://www.eclipse.org/downloads/

Installing the source code in Eclipse IDE

1. Creating a new workspace, select File -> Import... Under the General folder, 
   select "Existing Projects into Workspace" and click Next. Click on "Select 
   archive file" and choose the incremental-tool.zip source code archive.

2. Right click on the Z3Verification project and select Java Build Path. Clicking
   on libraries add the JAR files: log4j-1.2.17.jar and com.microsoft.z3.jar
   
Running the experiments 
   
1. Select Run->Run Configurations... from the menu. 
   Create a new configuration under Java Application
   
2. Main tab: The project is CompositionalSMT and the Main Class: experiments.WebPageExperiments.java

3. Arguments tab: a path pointing to the file IncrementalEngine/log/experiments_log4j.properties

4. Environment tab: create a variable DYLD_LIBRARY_PATH=/Users/kennethjohnson/z3/build pointing to the
   library directory of the Z3 installation
   
5. Click Run