fix some Mac issues

diff --git a/configure.ac b/configure.ac
index 3ef0ac689aee1d1fefd1efb7720dd2c5941e8861..30284b3f9568c18ddbdd9421d4208356346e7784 100644 (file)
--- a/configure.ac
+++ b/configure.ac
@@ -407,7 +407,7 @@ case "$with_build" in
     if test -z "${enable_muzzle+set}"       ; then enable_muzzle=no                 ; fi
     ;;
   debug) # unoptimized, debug symbols, assertions, tracing, dumping
-    CVC4CPPFLAGS=-DCVC4_DEBUG
+    CVC4CPPFLAGS='-DCVC4_DEBUG'
     CVC4CXXFLAGS='-fno-inline'
     CVC4CFLAGS='-fno-inline'
     CVC4LDFLAGS=
@@ -709,6 +709,25 @@ namespace __gnu_cxx { template<> struct hash<uint64_t> {}; }])],
                   [AC_MSG_RESULT([yes])])
 AC_LANG_POP([C++])
 
+# Check whether "long" and "int64_t" are distinct types w.r.t. overloading.
+# Even if they have the same size, they can be distinct, and some platforms
+# can have problems with ambiguous function calls when auto-converting
+# int64_t to long, and others will complain if you overload a function
+# that takes an int64_t with one that takes a long (giving a redefinition
+# error).  So we have to keep both happy.  Probably the same underlying
+# issue as the hash specialization above, but let's check separately
+# for flexibility.
+AC_MSG_CHECKING([for the relationship between long and int64_t])
+AC_LANG_PUSH([C++])
+AC_COMPILE_IFELSE([AC_LANG_SOURCE([
+#include <stdint.h>
+void foo(long);
+void foo(int64_t);])],
+                  [AC_MSG_RESULT([no relationship detected]); CVC4_NEED_INT64_T_OVERLOADS=1],
+                  [AC_MSG_RESULT([typedef or similar]); CVC4_NEED_INT64_T_OVERLOADS=0])
+AC_LANG_POP([C++])
+AC_SUBST([CVC4_NEED_INT64_T_OVERLOADS])
+
 # Check for ANTLR runantlr script (defined in config/antlr.m4)
 AC_PROG_ANTLR
 

diff --git a/src/options/mkoptions b/src/options/mkoptions
index 69d7643c76a82d7b8470e996d02ca44b4d5d7e11..8947aba42cc1a913f76c94a7534ba96078c00c8a 100755 (executable)
--- a/src/options/mkoptions
+++ b/src/options/mkoptions
@@ -1153,6 +1153,7 @@ function output_module {
       module_global_definitions \
       template \
       ; do
+    echo -n .
     eval text="\${text//\\\$\\{$var\\}/\${$var}}"
   done
   error="$(echo "$text" | grep '.*\${[^}]*}.*' | head -n 1)"
@@ -1205,10 +1206,12 @@ EOF
 
   ) >"$output.tmp"
 
+  echo -n .
   if diff -q "$output" "$output.tmp" &>/dev/null; then
     rm -f "$output.tmp"
   else
     mv -f "$output.tmp" "$output"
+    echo
     echo "regenerated $output"
   fi
 }
@@ -1308,6 +1311,7 @@ for var in \
     common_manpage_smt_documentation \
     remaining_manpage_smt_documentation \
     ; do
+  echo -n .
   eval text="\${text//\\\$\\{$var\\}/\${$var}}"
 done
 error="$(echo "$text" | grep '.*\${[^}]*}.*' | head -n 1)"
@@ -1361,8 +1365,10 @@ echo "$text"
 
 ) >"$output.tmp"
 
-diff -q "$output" "$output.tmp" &>/dev/null || (mv -f "$output.tmp" "$output" && echo "regenerated $output")
+echo -n .
+diff -q "$output" "$output.tmp" &>/dev/null || (mv -f "$output.tmp" "$output" && echo && echo "regenerated $output")
 rm -f "$output.tmp"
 
 done
 
+echo

diff --git a/src/util/integer.h.in b/src/util/integer.h.in
index 1fdaf0215acc072c55b364f1c4fca3c9b025e49b..1f01740835a9bbe2201a0e0b6debc17c1751d495 100644 (file)
--- a/src/util/integer.h.in
+++ b/src/util/integer.h.in
@@ -5,18 +5,23 @@
  ** Major contributors: none
  ** Minor contributors (to current version): dejan, cconway, mdeters
  ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009-2012  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
  ** New York University
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **
- ** \brief A multiprecision integer constant
+ ** \brief A multi-precision integer constant
  **
- ** A multiprecision integer constant.
+ ** A multi-precision integer constant.
  **/
 
-// this is used to avoid a public header dependence on cvc4autoconfig.h
+// these gestures are used to avoid a public header dependence on cvc4autoconfig.h
+
+#if @CVC4_NEED_INT64_T_OVERLOADS@
+#  define CVC4_NEED_INT64_T_OVERLOADS
+#endif
+
 #if /* use CLN */ @CVC4_USE_CLN_IMP@
 #  define CVC4_CLN_IMP
 #endif /* @CVC4_USE_CLN_IMP@ */

diff --git a/src/util/integer_cln_imp.h b/src/util/integer_cln_imp.h
index 8f7daf4f5865b5041480cb0e0a8f913c469d7be1..7fd6a269495da7a4a7d2fc4352ebe1b479ca6a3c 100644 (file)
--- a/src/util/integer_cln_imp.h
+++ b/src/util/integer_cln_imp.h
@@ -120,8 +120,12 @@ public:
   Integer(  signed long int z) : d_value(z) {}
   Integer(unsigned long int z) : d_value(z) {}
 
-  ~Integer() {}
+#ifdef CVC4_NEED_INT64_T_OVERLOADS
+  Integer( int64_t z) : d_value(static_cast<long>(z)) {}
+  Integer(uint64_t z) : d_value(static_cast<unsigned long>(z)) {}
+#endif /* CVC4_NEED_INT64_T_OVERLOADS */
 
+  ~Integer() {}
 
   Integer& operator=(const Integer& x){
     if(this == &x) return *this;

diff --git a/src/util/integer_gmp_imp.h b/src/util/integer_gmp_imp.h
index c553baff9bb3958288cb3365e451bcca28e0d68d..5b6468a9ebf4f6b01d5ca38b13ff2aa7259606fc 100644 (file)
--- a/src/util/integer_gmp_imp.h
+++ b/src/util/integer_gmp_imp.h
@@ -72,8 +72,12 @@ public:
   Integer(  signed long int z) : d_value(z) {}
   Integer(unsigned long int z) : d_value(z) {}
 
-  ~Integer() {}
+#ifdef CVC4_NEED_INT64_T_OVERLOADS
+  Integer( int64_t z) : d_value(static_cast<long>(z)) {}
+  Integer(uint64_t z) : d_value(static_cast<unsigned long>(z)) {}
+#endif /* CVC4_NEED_INT64_T_OVERLOADS */
 
+  ~Integer() {}
 
   Integer& operator=(const Integer& x){
     if(this == &x) return *this;

diff --git a/src/util/rational.h.in b/src/util/rational.h.in
index f9755937762cb2980f6429b27c95fe47813077e1..c8e42a2537f5f1d6c1c057677b7a2afe6602e947 100644 (file)
--- a/src/util/rational.h.in
+++ b/src/util/rational.h.in
@@ -5,7 +5,7 @@
  ** Major contributors: none
  ** Minor contributors (to current version): dejan, mdeters, cconway
  ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009-2012  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
  ** New York University
  ** See the file COPYING in the top-level source directory for licensing
@@ -16,7 +16,12 @@
  ** A multi-precision rational constant.
  **/
 
-// this is used to avoid a public header dependence on cvc4autoconfig.h
+// these gestures are used to avoid a public header dependence on cvc4autoconfig.h
+
+#if @CVC4_NEED_INT64_T_OVERLOADS@
+#  define CVC4_NEED_INT64_T_OVERLOADS
+#endif
+
 #if /* use CLN */ @CVC4_USE_CLN_IMP@
 #  define CVC4_CLN_IMP
 #endif /* @CVC4_USE_CLN_IMP@ */

diff --git a/src/util/rational_cln_imp.h b/src/util/rational_cln_imp.h
index 4247a1e63f11b4ffecd4b1cc95529996512795f0..182e813cda55a9b59edff0246975b5e94a9c3684 100644 (file)
--- a/src/util/rational_cln_imp.h
+++ b/src/util/rational_cln_imp.h
@@ -131,6 +131,11 @@ public:
   Rational(signed long int n) : d_value(n) { }
   Rational(unsigned long int n) : d_value(n) { }
 
+#ifdef CVC4_NEED_INT64_T_OVERLOADS
+  Rational(int64_t n) : d_value(static_cast<long>(n)) { }
+  Rational(uint64_t n) : d_value(static_cast<unsigned long>(n)) { }
+#endif /* CVC4_NEED_INT64_T_OVERLOADS */
+
   /**
    * Constructs a canonical Rational from a numerator and denominator.
    */
@@ -147,6 +152,15 @@ public:
     d_value /= d;
   }
 
+#ifdef CVC4_NEED_INT64_T_OVERLOADS
+  Rational(int64_t n, int64_t d) : d_value(static_cast<long>(n)) {
+    d_value /= static_cast<long>(d);
+  }
+  Rational(uint64_t n, uint64_t d) : d_value(static_cast<unsigned long>(n)) {
+    d_value /= static_cast<unsigned long>(d);
+  }
+#endif /* CVC4_NEED_INT64_T_OVERLOADS */
+
   Rational(const Integer& n, const Integer& d) :
     d_value(n.get_cl_I())
   {

diff --git a/src/util/rational_gmp_imp.h b/src/util/rational_gmp_imp.h
index 0c8a46f33167469c1f2aee51c9f9b5f05635344f..b86dc32f24efd37b5ededa21f8fea2e012dcab1b 100644 (file)
--- a/src/util/rational_gmp_imp.h
+++ b/src/util/rational_gmp_imp.h
@@ -111,6 +111,15 @@ public:
     d_value.canonicalize();
   }
 
+#ifdef CVC4_NEED_INT64_T_OVERLOADS
+  Rational(int64_t n) : d_value(static_cast<long>(n), 1) {
+    d_value.canonicalize();
+  }
+  Rational(uint64_t n) : d_value(static_cast<unsigned long>(n), 1) {
+    d_value.canonicalize();
+  }
+#endif /* CVC4_NEED_INT64_T_OVERLOADS */
+
   /**
    * Constructs a canonical Rational from a numerator and denominator.
    */
@@ -127,6 +136,15 @@ public:
     d_value.canonicalize();
   }
 
+#ifdef CVC4_NEED_INT64_T_OVERLOADS
+  Rational(int64_t n, int64_t d) : d_value(static_cast<long>(n), static_cast<long>(d)) {
+    d_value.canonicalize();
+  }
+  Rational(uint64_t n, uint64_t d) : d_value(static_cast<unsigned long>(n), static_cast<unsigned long>(d)) {
+    d_value.canonicalize();
+  }
+#endif /* CVC4_NEED_INT64_T_OVERLOADS */
+
   Rational(const Integer& n, const Integer& d) :
     d_value(n.get_mpz(), d.get_mpz())
   {