revied vagrant file and more changes according to Falks feedback.

Vagrantfile

@@ -34,20 +34,18 @@ Vagrant.configure(VAGRANTFILE_API_VERSION) do |config|
     domain.uri = 'qemu+unix:///system'
     domain.disk_bus = "virtio"
     domain.memory = 2048
+    domain.name = "psyco-vm"
   end
 
   config.vm.provider :virtualbox do |domain|
-    domain.memory = 4096
+    domain.memory = 2048
     domain.cpus = 2
-    domain.name = "GSOC_VM_windows_source"
+    domain.name = "psyco-vm"
 #    domain.gui = true
   end
 
-  config.vm.synced_folder "../jdart", "/home/vagrant/gsoc-project/jdart"
-  config.vm.synced_folder "../jconstraints", "/home/vagrant/gsoc-project/jconstraints"
-  config.vm.synced_folder "../jconstraints-z3", "/home/vagrant/gsoc-project/jconstraints-z3"
-  config.vm.synced_folder "../jpf-core", "/home/vagrant/gsoc-project/jpf-core"
-  config.vm.synced_folder ".", "/home/vagrant/gsoc-project/psyco_gsoc16"
+  config.vm.synced_folder ".", "/home/vagrant/psyco"
+  #config.vm.synced_folder "../jconstraints-smtinterpol", "/home/vagrant/jconstraints-smtinterpol"
 
   config.vm.provision :shell, :privileged => false, path: "scripts/install.sh"
 end

scripts/install.sh

@@ -24,12 +24,14 @@ set -e
 user=vagrant
 # Directories
 home_dir=/home/${user}
-project_root_dir=${home_dir}/gsoc-project
+project_root_dir=${home_dir}
+jconstraints_conf_dir=${project_root_dir}/.jconstraints
 sudo chown ${user}:${user} ${project_root_dir}
 
 # Set these flags to control what to install
 install_packages=1
 install_z3=1
+install_interpolation=1
 install_jpf_core=1
 install_jdart=1
 install_psyco=1
@@ -72,7 +74,7 @@ if [ ${install_z3} -eq 1 ]; then
     wget https://github.com/Z3Prover/z3/releases/download/z3-${z3_version}/${z3_archive}
     unzip ${z3_archive}
     cd ${z3_full_version}/bin
-    mvn install:install-file -Dfile=com.microsoft.z3.jar -DgroupId=com.microsoft -DartifactId=z3 -Dversion=0.9 -Dpackaging=jar
+    mvn install:install-file -Dfile=com.microsoft.z3.jar -DgroupId=com.microsoft -DartifactId=z3 -Dversion=4.4.1 -Dpackaging=jar
     rm com.microsoft.z3.jar
     sudo mv lib* /usr/lib/
     sudo mv * /usr/bin
@@ -97,10 +99,10 @@ if [ ${install_jpf_core} -eq 1 ]; then
 
     # Install jpf-core
     jpf_core_dir=${project_root_dir}/jpf-core
-    #hg clone http://babelfish.arc.nasa.gov/hg/jpf/jpf-core ${jpf_core_dir}
+    hg clone http://babelfish.arc.nasa.gov/hg/jpf/jpf-core ${jpf_core_dir}
     cd ${jpf_core_dir}
     # Revert to a commit we are sure works with JDart
-    #hg update -r 29
+    hg update -r 29
     ant
 
     echo "jpf-core = ${jpf_core_dir}" >> ${jpf_conf_file}
@@ -110,41 +112,64 @@ if [ ${install_jdart} -eq 1 ]; then
 
     # Install jconstraints
     jconstraints_dir=${project_root_dir}/jconstraints
-    cd ${jconstraints_dir}
-    mvn install
+    git clone https://github.com/psycopaths/jconstraints.git ${jconstraints_dir}
+    pushd ${jconstraints_dir};
+        mvn install
+    popd;
 
     # Install jconstraints-z3
     jconstraints_z3_dir=${project_root_dir}/jconstraints-z3
-    cd ${jconstraints_z3_dir}
-    mvn install
+    git clone https://github.com/psycopaths/jconstraints-z3.git ${jconstraints_z3_dir}
+    pushd ${jconstraints_z3_dir};
+        mvn install
 
-    jconstraints_conf_dir=${project_root_dir}/.jconstraints
     mkdir -p ${jconstraints_conf_dir}/extensions
     ln -s ${jconstraints_conf_dir} ${home_dir}/.jconstraints || true
     cp target/jConstraints-z3-1.0-SNAPSHOT.jar ${home_dir}/.jconstraints/extensions
-    cp ${home_dir}/.m2/repository/com/microsoft/z3/0.9/z3-0.9.jar ${home_dir}/.jconstraints/extensions/com.microsoft.z3.jar
+    popd;
+    cp ${home_dir}/.m2/repository/com/microsoft/z3/4.4.1/z3-4.4.1.jar ${home_dir}/.jconstraints/extensions/com.microsoft.z3.jar
 
     echo "jconstraints = $jconstraints_dir" >> ${jpf_conf_file}
 
     # Install JDart
     jdart_dir=${project_root_dir}/jdart
-    cd ${jdart_dir}
-    ant
+    git clone https://github.com/psycopaths/jdart.git ${jdart_dir}
+    pushd ${jdart_dir};
+        ant
+    popd;
 
     echo "jpf-jdart = ${jdart_dir}" >> ${jpf_conf_file}
     echo "extensions=\${jpf-core},\${jpf-jdart}" >> ${jpf_conf_file}
 
 fi
 
+if [ ${install_interpolation} -eq 1 ]; then
+    jconstraints_smtinterpol_dir=${project_root_dir}/jconstraints-smtinterpol
+    smtinterpol_lib=${project_root_dir}/smtinterpol_lib
+    mkdir -p ${smtinterpol_lib}
+    # Check http://ultimate.informatik.uni-freiburg.de/smtinterpol/download.html for current smtinterpol location
+    wget http://ultimate.informatik.uni-freiburg.de/smtinterpol/smtinterpol-2.1-290-g24167dc.jar -O ${smtinterpol_lib}/smtinterpol.jar
+    cp ${smtinterpol_lib}/smtinterpol.jar ${home_dir}/.jconstraints/extensions/smtinterpol.jar
+    pushd ${home_dir}/.jconstraints/extensions/;
+        mvn install:install-file -Dfile=smtinterpol.jar -DgroupId=de.uni_freiburg.informatik.ultimate -DartifactId=smtinterpol -Dversion=2.0 -Dpackaging=jar
+    popd;
+
+    #git clone https://github.com/psycopaths/jconstraints-smtinterpol.git ${jconstraints_smtinterpol_dir}
+    git clone https://github.com/mmuesly/jconstraints-smtinterpol.git ${jconstraints_smtinterpol_dir}
+    pushd ${jconstraints_smtinterpol_dir};
+        mvn install
+        cp target/jConstraints-smtinterpol-1.0-SNAPSHOT.jar ${home_dir}/.jconstraints/extensions/jconstraints-smtinterpol-1.0-SNAPSHOT.jar
+    popd;
+fi
+
 if [ ${install_psyco} -eq 1 ]; then
 
     # Install jpf-core
-    psyco_dir=${project_root_dir}/psyco_gsoc16
-    #hg clone http://babelfish.arc.nasa.gov/hg/jpf/jpf-core ${jpf_core_dir}
-    cd ${jpf_core_dir}
+    psyco_dir=${project_root_dir}/psyco
+
+    cd ${psyco_dir}
     # Revert to a commit we are sure works with JDart
-    #hg update -r 29
     ant test
 
-    echo "jpf-psyco = ${jpf_core_dir}" >> ${jpf_conf_file}
+    echo "jpf-psyco = ${psyco_dir}" >> ${jpf_conf_file}
 fi

src/examples/gsoc/cev_esas/CEV_1.java

@@ -1,14 +1,3 @@
-/*
- * To change this license header, choose License Headers in Project Properties.
- * To change this template file, choose Tools | Templates
- * and open the template in the editor.
- */
-package gsoc.cev_esas;
-
-/**
- *
- * @author mmuesly
- */
 /*
  * Copyright (C) 2015, United States Government, as represented by the 
  * Administrator of the National Aeronautics and Space Administration.
@@ -24,6 +13,7 @@
  * CONDITIONS OF ANY KIND, either express or implied. See the License for the 
  * specific language governing permissions and limitations under the License.
  */
+package gsoc.cev_esas;
 
 import gov.nasa.jpf.jdart.Symbolic;
 

src/examples/gsoc/cev_esas/ErrorLog.java

@@ -1,16 +1,21 @@
 /*
- * To change this license header, choose License Headers in Project Properties.
- * To change this template file, choose Tools | Templates
- * and open the template in the editor.
+ * Copyright (C) 2015, United States Government, as represented by the 
+ * Administrator of the National Aeronautics and Space Administration.
+ * All rights reserved.
+ *
+ * The PSYCO: A Predicate-based Symbolic Compositional Reasoning environment 
+ * platform is licensed under the Apache License, Version 2.0 (the "License"); you 
+ * may not use this file except in compliance with the License. You may obtain a 
+ * copy of the License at http://www.apache.org/licenses/LICENSE-2.0. 
+ *
+ * Unless required by applicable law or agreed to in writing, software distributed 
+ * under the License is distributed on an "AS IS" BASIS, WITHOUT WARRANTIES OR 
+ * CONDITIONS OF ANY KIND, either express or implied. See the License for the 
+ * specific language governing permissions and limitations under the License.
  */
 package gsoc.cev_esas;
 
 import gov.nasa.jpf.jdart.Symbolic;
-
-/**
- *
- * @author mmuesly
- */
 //import java.util.ArrayList;
 
 /**

src/examples/gsoc/cev_esas/Failures.java

@@ -1,17 +1,24 @@
+
 /*
- * To change this license header, choose License Headers in Project Properties.
- * To change this template file, choose Tools | Templates
- * and open the template in the editor.
+ * Copyright (C) 2015, United States Government, as represented by the 
+ * Administrator of the National Aeronautics and Space Administration.
+ * All rights reserved.
+ *
+ * The PSYCO: A Predicate-based Symbolic Compositional Reasoning environment 
+ * platform is licensed under the Apache License, Version 2.0 (the "License"); you 
+ * may not use this file except in compliance with the License. You may obtain a 
+ * copy of the License at http://www.apache.org/licenses/LICENSE-2.0. 
+ *
+ * Unless required by applicable law or agreed to in writing, software distributed 
+ * under the License is distributed on an "AS IS" BASIS, WITHOUT WARRANTIES OR 
+ * CONDITIONS OF ANY KIND, either express or implied. See the License for the 
+ * specific language governing permissions and limitations under the License.
  */
 package gsoc.cev_esas;
 
 import gov.nasa.jpf.jdart.Symbolic;
 import java.util.EnumSet;
 
-/**
- *
- * @author mmuesly
- */
 public class Failures {
   enum Type { EARTH_SENSOR, LAS_CNTRL, CM_MASS, CM_RCS };
 

src/examples/gsoc/cev_esas/Spacecraft.java

@@ -1,40 +1,20 @@
-/*
- * To change this license header, choose License Headers in Project Properties.
- * To change this template file, choose Tools | Templates
- * and open the template in the editor.
- */
-package gsoc.cev_esas;
 
-/**
+/*
+ * Copyright (C) 2015, United States Government, as represented by the 
+ * Administrator of the National Aeronautics and Space Administration.
+ * All rights reserved.
+ *
+ * The PSYCO: A Predicate-based Symbolic Compositional Reasoning environment 
+ * platform is licensed under the Apache License, Version 2.0 (the "License"); you 
+ * may not use this file except in compliance with the License. You may obtain a 
+ * copy of the License at http://www.apache.org/licenses/LICENSE-2.0. 
  *
- * @author mmuesly
+ * Unless required by applicable law or agreed to in writing, software distributed 
+ * under the License is distributed on an "AS IS" BASIS, WITHOUT WARRANTIES OR 
+ * CONDITIONS OF ANY KIND, either express or implied. See the License for the 
+ * specific language governing permissions and limitations under the License.
  */
-//
-// Copyright (C) 2007 United States Government as represented by the
-// Administrator of the National Aeronautics and Space Administration
-// (NASA).  All Rights Reserved.
-// 
-// This software is distributed under the NASA Open Source Agreement
-// (NOSA), version 1.3.  The NOSA has been approved by the Open Source
-// Initiative.  See the file NOSA-1.3-JPF at the top of the distribution
-// directory tree for the complete NOSA document.
-// 
-// THE SUBJECT SOFTWARE IS PROVIDED "AS IS" WITHOUT ANY WARRANTY OF ANY
-// KIND, EITHER EXPRESSED, IMPLIED, OR STATUTORY, INCLUDING, BUT NOT
-// LIMITED TO, ANY WARRANTY THAT THE SUBJECT SOFTWARE WILL CONFORM TO
-// SPECIFICATIONS, ANY IMPLIED WARRANTIES OF MERCHANTABILITY, FITNESS FOR
-// A PARTICULAR PURPOSE, OR FREEDOM FROM INFRINGEMENT, ANY WARRANTY THAT
-// THE SUBJECT SOFTWARE WILL BE ERROR FREE, OR ANY WARRANTY THAT
-// DOCUMENTATION, IF PROVIDED, WILL CONFORM TO THE SUBJECT SOFTWARE.
-//
-
-//
-// DISCLAIMER - this file is part of the 'ESAS' demonstration project. As
-// such, it is only intended for demonstration purposes, does not contain
-// or refer to actual NASA flight software, and is solely derived from
-// publicly available information. For further details, please refer to the
-// README-ESAS file that is included in this distribution.
-//
+package gsoc.cev_esas;
 
 import gov.nasa.jpf.jdart.Symbolic;
 import java.util.EnumSet;

src/examples/symbolicsearch/quantifierelimination/simpleexample/FirstExample.java

@@ -1,13 +1,17 @@
 /*
- * To change this license header, choose License Headers in Project Properties.
- * To change this template file, choose Tools | Templates
- * and open the template in the editor.
- */
-
-/**
- *The class first Exampel is used to demonstrate the symbolic search setup.
- * Further it is a first Example to demonstate the search's capability.
- * @author mmuesly
+ * Copyright (C) 2015, United States Government, as represented by the 
+ * Administrator of the National Aeronautics and Space Administration.
+ * All rights reserved.
+ *
+ * The PSYCO: A Predicate-based Symbolic Compositional Reasoning environment 
+ * platform is licensed under the Apache License, Version 2.0 (the "License"); you 
+ * may not use this file except in compliance with the License. You may obtain a 
+ * copy of the License at http://www.apache.org/licenses/LICENSE-2.0. 
+ *
+ * Unless required by applicable law or agreed to in writing, software distributed 
+ * under the License is distributed on an "AS IS" BASIS, WITHOUT WARRANTIES OR 
+ * CONDITIONS OF ANY KIND, either express or implied. See the License for the 
+ * specific language governing permissions and limitations under the License.
  */
 package symbolicsearch.quantifierelimination.simpleexample;
 import gov.nasa.jpf.jdart.Symbolic;
@@ -16,9 +20,6 @@ public class FirstExample {
   @Symbolic("true")
   private int x = 0;
 
-//  public FirstExample(){
-//  }
-
   public void m1(int p){
     if(x<5){
       x = x + p;

src/examples/symbolicsearch/startingExample/FirstExample.java

@@ -1,13 +1,17 @@
 /*
- * To change this license header, choose License Headers in Project Properties.
- * To change this template file, choose Tools | Templates
- * and open the template in the editor.
- */
-
-/**
- *The class first Exampel is used to demonstrate the symbolic search setup.
- * Further it is a first Example to demonstate the search's capability.
- * @author mmuesly
+ * Copyright (C) 2015, United States Government, as represented by the 
+ * Administrator of the National Aeronautics and Space Administration.
+ * All rights reserved.
+ *
+ * The PSYCO: A Predicate-based Symbolic Compositional Reasoning environment 
+ * platform is licensed under the Apache License, Version 2.0 (the "License"); you 
+ * may not use this file except in compliance with the License. You may obtain a 
+ * copy of the License at http://www.apache.org/licenses/LICENSE-2.0. 
+ *
+ * Unless required by applicable law or agreed to in writing, software distributed 
+ * under the License is distributed on an "AS IS" BASIS, WITHOUT WARRANTIES OR 
+ * CONDITIONS OF ANY KIND, either express or implied. See the License for the 
+ * specific language governing permissions and limitations under the License.
  */
 package symbolicsearch.startingExample;
 import gov.nasa.jpf.jdart.Symbolic;

src/examples/symbolicsearch/twoStateVariables/TwoStateVariables.java

@@ -1,13 +1,17 @@
 /*
- * To change this license header, choose License Headers in Project Properties.
- * To change this template file, choose Tools | Templates
- * and open the template in the editor.
- */
-
-/**
- *The class first Exampel is used to demonstrate the symbolic search setup.
- * Further it is a first Example to demonstate the search's capability.
- * @author mmuesly
+ * Copyright (C) 2015, United States Government, as represented by the 
+ * Administrator of the National Aeronautics and Space Administration.
+ * All rights reserved.
+ *
+ * The PSYCO: A Predicate-based Symbolic Compositional Reasoning environment 
+ * platform is licensed under the Apache License, Version 2.0 (the "License"); you 
+ * may not use this file except in compliance with the License. You may obtain a 
+ * copy of the License at http://www.apache.org/licenses/LICENSE-2.0. 
+ *
+ * Unless required by applicable law or agreed to in writing, software distributed 
+ * under the License is distributed on an "AS IS" BASIS, WITHOUT WARRANTIES OR 
+ * CONDITIONS OF ANY KIND, either express or implied. See the License for the 
+ * specific language governing permissions and limitations under the License.
  */
 package symbolicsearch.twoStateVariables;
 import symbolicsearch.twoStateVariables.*;
@@ -19,9 +23,6 @@ public class TwoStateVariables {
   @Symbolic("true")
   private int y = 5;
 
-//  public FirstExample(){
-//  }
-
   public void m1(){
     if(x<5){
       x = x + 2;