From: Morgan Deters Date: Wed, 26 Sep 2012 18:51:48 +0000 (+0000) Subject: Fix a handful of things for Mac, and Java bindings. X-Git-Tag: cvc5-1.0.0~7782 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=c1e936b9cec3d731778b95504770e48c28fd1a65;p=cvc5.git 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 facf5a21c..780200917 100644 --- 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 c5211474a..e9bc26b32 100755 --- 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 < 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 16af3c67f..3bb433c51 100755 --- 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 index 000000000..834191a0c --- /dev/null +++ b/contrib/mac-build @@ -0,0 +1,55 @@ +#!/bin/bash +# +# mac-build script +# Morgan Deters +# 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 d4688fc25..45ce4f4ef 100644 --- 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(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(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 9ae2023f6..ddab66546 100644 --- 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 34feaacbb..70171c918 100644 --- 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 e04db5846..9f3360696 100644 --- 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; }