Fix a handful of things for Mac, and Java bindings.

Also add a "mac-build" script that sets up prerequisites for Mac.

diff --git a/contrib/Makefile.am b/contrib/Makefile.am
index facf5a21c29c14fe7464e8ae110b8fb999d0530c..780200917e42f152c1b8176e6863be5933551105 100644 (file)
--- a/contrib/Makefile.am
+++ b/contrib/Makefile.am
@@ -11,6 +11,7 @@ EXTRA_DIST = \
        configure-in-place \
        depgraph \
        get-antlr-3.4 \
+       mac-build \
        run-script-smtcomp2012 \
        theoryskel/kinds \
        theoryskel/Makefile \

diff --git a/contrib/get-antlr-3.4 b/contrib/get-antlr-3.4
index c5211474a1295a4c04701c751409a920b6a64777..e9bc26b32c476b6606d8852c45e3c41998e39dac 100755 (executable)
--- a/contrib/get-antlr-3.4
+++ b/contrib/get-antlr-3.4
@@ -14,13 +14,24 @@ if ! [ -e src/parser/cvc/Cvc.g ]; then
   exit 1
 fi
 
+function webget {
+  if which wget &>/dev/null; then
+    wget -c -O "$2" "$1"
+  elif which curl &>/dev/null; then
+    curl "$1" >"$2"
+  else
+    echo "Can't figure out how to download from web.  Please install wget or curl." >&2
+    exit 1
+  fi
+}
+
 set -x
 mkdir -p antlr-3.4/share/java
 mkdir -p antlr-3.4/bin
 mkdir -p antlr-3.4/src
 cd antlr-3.4
-wget -c -O share/java/antlr-3.4-complete.jar http://antlr.org/download/antlr-3.4-complete.jar
-wget -c -O src/libantlr3c-3.4.tar.gz http://antlr.org/download/C/libantlr3c-3.4.tar.gz
+webget http://antlr.org/download/antlr-3.4-complete.jar share/java/antlr-3.4-complete.jar 
+webget http://antlr.org/download/C/libantlr3c-3.4.tar.gz src/libantlr3c-3.4.tar.gz
 tee bin/antlr3 <<EOF
 #!/bin/sh
 export CLASSPATH=/usr/share/java/stringtemplate.jar:`pwd`/share/java/antlr-3.4-complete.jar:\$CLASSPATH
@@ -32,7 +43,7 @@ tar xfzv libantlr3c-3.4.tar.gz
 cd libantlr3c-3.4
 ./configure --enable-64bit --prefix=`pwd`/../..
 cp Makefile Makefile.orig
-sed 's,^CFLAGS = .*,\0 -fexceptions,' Makefile.orig > Makefile
+sed 's,^\(CFLAGS = .*\),\1 -fexceptions,' Makefile.orig > Makefile
 make
 make install
 set +x

diff --git a/contrib/get-bug-attachments b/contrib/get-bug-attachments
index 16af3c67f46bb2dbacf643e406f6afa221a4003f..3bb433c511e454d82d81790b9c7d3eafdf7ff76b 100755 (executable)
--- a/contrib/get-bug-attachments
+++ b/contrib/get-bug-attachments
@@ -28,7 +28,7 @@ function webcat {
 
 function webget {
   if which wget &>/dev/null; then
-    tmpfile="$(mktemp)"
+    tmpfile="$(mktemp get_bug_attach.$$.XXXXXXXX)"
     filename="$(wget -qS -O "$tmpfile" "$1" 2>&1 | grep 'Content-disposition: attachment' | sed 's,.*filename="\(.*\)".*,\1,')"
     ext="$(echo "$filename" | sed 's,.*\.\(.*\),\1,')"
     if [ -e "$2.$ext" ] && ! diff -q "$tmpfile" "$2.$ext" &>/dev/null; then
@@ -45,8 +45,23 @@ function webget {
       echo "$2.$ext"
     fi
   elif which curl &>/dev/null; then
-    mkdir -p "$(dirname "$2")"
-    curl "$1" >"$2"
+    tmpfile="$(mktemp get_bug_attach.$$.XXXXXXXX)"
+    filename="$(curl --head "$1" 2>&1 | grep 'Content-disposition: attachment' | sed 's,.*filename="\(.*\)".*,\1,')"
+    curl "$1" >"$tmpfile" 2>/dev/null
+    ext="$(echo "$filename" | sed 's,.*\.\(.*\),\1,')"
+    if [ -e "$2.$ext" ] && ! diff -q "$tmpfile" "$2.$ext" &>/dev/null; then
+      c=a
+      while [ -e "$2$c.$ext" ] && ! diff -q "$tmpfile" "$2$c.$ext" &>/dev/null; do
+        c=$(echo $c | tr a-y b-z)
+      done
+      mkdir -p "$(dirname "$2")"
+      mv "$tmpfile" "$2$c.$ext"
+      echo "$2$c.$ext"
+    else
+      mkdir -p "$(dirname "$2")"
+      mv "$tmpfile" "$2.$ext"
+      echo "$2.$ext"
+    fi
   else
     echo "Please install wget or curl." >&2;
     exit 1
@@ -61,15 +76,17 @@ for attachment in $(\
   | sort -nu); do
 
   let count++
-  echo -n "Downloading attachment $attachment..."
+  printf "%-30s " "Downloading attachment $attachment..."
   webget "http://church.cims.nyu.edu/bugs/attachment.cgi?id=$attachment" "test/regress/regress0/bug$bugid"
 
 done
 
 if [ $count -eq 0 ]; then
-  echo "There are no bug testcase attachments for bug #$bugid."
+  echo "There are no bug attachments for bug #$bugid."
 else
-  echo "Downloaded $count bug testcases for bug #$bugid."
+  s=s
+  [ $count -eq 1 ] && s=
+  echo "Downloaded $count bug attachment$s for bug #$bugid."
 fi
 
 done

diff --git a/contrib/mac-build b/contrib/mac-build
new file mode 100644 (file)
index 0000000..834191a
--- /dev/null
+++ b/contrib/mac-build
@@ -0,0 +1,55 @@
+#!/bin/bash
+#
+# mac-build script
+# Morgan Deters <mdeters@cs.nyu.edu>
+# Tue, 25 Sep 2012 15:44:27 -0400
+#
+
+macports_prereq="boost gmp gtime readline"
+
+export PATH="/opt/local/bin:$PATH"
+
+if [ $# -ne 0 ]; then
+  echo "usage: `basename $0`" >&2
+  echo >&2
+  echo "This script attempts to set up the build requirements for CVC4 for Mac OS X." >&2
+  echo "MacPorts must be installed (but this script installs prerequisite port" >&2
+  echo "packages for CVC4).  If this script is successful, it prints a configure" >&2
+  echo "line that you can use to configure CVC4." >&2
+fi
+
+function reporterror {
+  echo
+  echo =============================================================================
+  echo
+  echo "There was an error setting up the prerequisites.  Look above for details."
+  echo
+  exit 1
+}
+
+echo =============================================================================
+echo
+echo "running: sudo port install $macports_prereq"
+if which port &>/dev/null; then
+  echo "You may be asked for your password to install these packages."
+  echo
+  sudo port install $macports_prereq || reporterror
+else
+  echo
+  echo "ERROR: You must have MacPorts installed for Mac builds of CVC4."
+  echo "ERROR: See http://www.macports.org/"
+  reporterror
+fi
+echo
+echo =============================================================================
+echo
+contrib/get-antlr-3.4 | grep -v 'Now configure CVC4 with' | grep -v '\./configure --with-antlr-dir='
+[ ${PIPESTATUS[0]} -eq 0 ] || reporterror
+echo
+echo =============================================================================
+echo
+echo 'Now just run:'
+echo '  ./configure LDFLAGS=-L/opt/local/lib CPPFLAGS=-I/opt/local/include --with-antlr-dir=`pwd`/antlr-3.4 ANTLR=`pwd`/antlr-3.4/bin/antlr3'
+echo '  make'
+echo
+echo =============================================================================

diff --git a/src/bindings/compat/java/include/cvc3/JniUtils.h b/src/bindings/compat/java/include/cvc3/JniUtils.h
index d4688fc25dfe3deec7867aad1dc5095a02881485..45ce4f4efe4686be0456e55bceb7d865433f5c28 100644 (file)
--- a/src/bindings/compat/java/include/cvc3/JniUtils.h
+++ b/src/bindings/compat/java/include/cvc3/JniUtils.h
@@ -169,7 +169,7 @@ namespace Java_cvc3_JniUtils {
        env->FindClass("java/lang/Object"),
        NULL);
 
-    for (int i = 0; i < v.size(); ++i) {
+    for (size_t i = 0; i < v.size(); ++i) {
       env->SetObjectArrayElement(jarray, i, embed_copy<T>(env, v[i]));
     }
 
@@ -183,7 +183,7 @@ namespace Java_cvc3_JniUtils {
        env->FindClass("java/lang/Object"),
        NULL);
 
-    for (int i = 0; i < v.size(); ++i) {
+    for (size_t i = 0; i < v.size(); ++i) {
       env->SetObjectArrayElement(jarray, i, embed_const_ref<T>(env, &v[i]));
     }
 
@@ -196,7 +196,7 @@ namespace Java_cvc3_JniUtils {
     {
       jobjectArray jarray = (jobjectArray) env->NewObjectArray(v.size(),
           env->FindClass("[Ljava/lang/Object;"), NULL);
-      for (int i = 0; i < v.size(); ++i)
+      for (size_t i = 0; i < v.size(); ++i)
         {
           env->SetObjectArrayElement(jarray, i, toJavaVConstRef(env, v[i]));
         }

diff --git a/src/bindings/compat/java/src/cvc3/JniUtils.cpp b/src/bindings/compat/java/src/cvc3/JniUtils.cpp
index 9ae2023f61b1100535586a4edbaf91b3e6fe2ab7..ddab6654687fb2e5ef6f9afa54b6ad2669f95470 100644 (file)
--- a/src/bindings/compat/java/src/cvc3/JniUtils.cpp
+++ b/src/bindings/compat/java/src/cvc3/JniUtils.cpp
@@ -63,6 +63,7 @@ namespace Java_cvc3_JniUtils {
     }
     
     DebugAssert(false, "JniUtils::toJava(QueryResult): unreachable");
+    return toJava(env, ""); // to avoid compiler warning
   }
 
   jstring toJava(JNIEnv* env, CVC3::FormulaValue result) {

diff --git a/src/bindings/compat/java/src/cvc3/ValidityChecker_impl.cpp b/src/bindings/compat/java/src/cvc3/ValidityChecker_impl.cpp
index 34feaacbb25e107403564738dc5e6b51bb2cfc08..70171c918067fc70dd6d8d518bcb940e6a57d923 100644 (file)
--- a/src/bindings/compat/java/src/cvc3/ValidityChecker_impl.cpp
+++ b/src/bindings/compat/java/src/cvc3/ValidityChecker_impl.cpp
@@ -847,7 +847,7 @@ vc->loadFile(fileName, toCppInputLanguage(env, lang), false);
 
 DEFINITION: Java_cvc3_ValidityChecker_jniGetStatistics
 jobject m ValidityChecker vc
-return embed_mut_ref(env, &vc->getStatistics());
+return embed_copy(env, vc->getStatistics());
 
 DEFINITION: Java_cvc3_ValidityChecker_jniPrintStatistics
 void m ValidityChecker vc

diff --git a/src/util/statistics.h b/src/util/statistics.h
index e04db584679a7a359450a139b30f95792de4f038..9f3360696edf0d208246c159a50304db86c1a1f2 100644 (file)
--- a/src/util/statistics.h
+++ b/src/util/statistics.h
@@ -68,6 +68,8 @@ public:
     friend class StatisticsBase;
 
   public:
+    iterator() : d_it() { }
+    iterator(const iterator& it) : d_it(it.d_it) { }
     value_type operator*() const;
     iterator& operator++() { ++d_it; return *this; }
     iterator operator++(int) { iterator old = *this; ++d_it; return old; }