Improved compatibility layer, now supports quantifiers. Also incorporates

numerous bugfixes, and the cvc3 system test is enabled.

3 files changed, 4 insertions, 56 deletions

diff --git a/src/util/Makefile.am b/src/util/Makefile.am
index 432e6ef26..7d3664d47 100644
--- a/src/util/Makefile.am
+++ b/src/util/Makefile.am
@@ -89,52 +89,6 @@ BUILT_SOURCES = \
 	rational.h \
 	integer.h \
 	tls.h
-if CVC4_DEBUG
-if CVC4_TRACING
-# listing Debug_tags too ensures that make doesn't auto-remove it
-# after building (if it does, we don't get the "cached" effect with
-# the .tmp files below, and we have to re-compile and re-link each
-# time, even when there are no changes).
-BUILT_SOURCES += \
-	Debug_tags.h \
-	Debug_tags
-endif
-endif
-if CVC4_TRACING
-# listing Trace_tags too ensures that make doesn't auto-remove it
-# after building (if it does, we don't get the "cached" effect with
-# the .tmp files below, and we have to re-compile and re-link each
-# time, even when there are no changes).
-BUILT_SOURCES += \
-	Trace_tags.h \
-	Trace_tags
-endif
-
-%_tags.h: %_tags
-	$(AM_V_GEN)( \
-	  echo 'static char const* const $^[] = {'; \
-	  for tag in `cat $^`; do \
-	    echo "\"$$tag\","; \
-	  done; \
-	  echo 'NULL'; \
-	  echo '};' \
-	) >"$@"
-
-# This .tmp business is to keep from having to re-compile options.cpp
-# (and then re-link the libraries) if nothing has changed.
-%_tags: %_tags.tmp
-	$(AM_V_GEN)\
-	diff -q "$^" "$@" &>/dev/null || mv "$^" "$@" || true
-# .PHONY ensures the .tmp version is always rebuilt (to check for any changes)
-.PHONY: Debug_tags.tmp Trace_tags.tmp
-# The "sed" invocation below is particularly obnoxious, but it works around
-# inconsistencies in REs on different platforms, using only a basic regular
-# expression (no |, no \<, ...).
-Debug_tags.tmp Trace_tags.tmp:
-	$(AM_V_GEN)\
-	grep '\<$(@:_tags.tmp=)\(\.isOn\)* *( *\".*\" *)' \
-		`find @srcdir@/../ -name "*.cpp" -or -name "*.h" -or -name "*.cc" -or -name "*.g"` | \
-	sed 's/^$(@:_tags.tmp=)\(\.isOn\)* *( *\"\([^"]*\)\".*/\2/;s/.*[^a-zA-Z0-9_]$(@:_tags.tmp=)\(\.isOn\)* *( *\"\([^"]*\)\".*/\2/' | LC_ALL=C sort | uniq >"$@"
 
 if CVC4_CLN_IMP
 libutil_la_SOURCES += \
@@ -181,10 +135,4 @@ DISTCLEANFILES = \
 	tls.h.tmp \
 	integer.h \
 	rational.h \
-	tls.h \
-	Debug_tags.tmp \
-	Debug_tags.h \
-	Debug_tags \
-	Trace_tags.tmp \
-	Trace_tags.h \
-	Trace_tags
+	tls.h
diff --git a/src/util/rational_cln_imp.h b/src/util/rational_cln_imp.h
index 258060e02..969a8b5eb 100644
--- a/src/util/rational_cln_imp.h
+++ b/src/util/rational_cln_imp.h
@@ -87,7 +87,7 @@ public:
    * For more information about what is a valid rational string,
    * see GMP's documentation for mpq_set_str().
    */
-  explicit Rational(const char * s, int base = 10) throw (std::invalid_argument){
+  explicit Rational(const char* s, unsigned base = 10) throw (std::invalid_argument){
     cln::cl_read_flags flags;
 
     flags.syntax = cln::syntax_rational;
@@ -101,7 +101,7 @@ public:
       throw std::invalid_argument(ss.str());
     }
   }
-  Rational(const std::string& s, int base = 10) throw (std::invalid_argument){
+  Rational(const std::string& s, unsigned base = 10) throw (std::invalid_argument){
     cln::cl_read_flags flags;
 
     flags.syntax = cln::syntax_rational;
diff --git a/src/util/rational_gmp_imp.h b/src/util/rational_gmp_imp.h
index 22f1e91b2..0c8a46f33 100644
--- a/src/util/rational_gmp_imp.h
+++ b/src/util/rational_gmp_imp.h
@@ -81,7 +81,7 @@ public:
    * For more information about what is a valid rational string,
    * see GMP's documentation for mpq_set_str().
    */
-  explicit Rational(const char * s, int base = 10): d_value(s,base) {
+  explicit Rational(const char* s, unsigned base = 10): d_value(s, base) {
     d_value.canonicalize();
   }
   Rational(const std::string& s, unsigned base = 10) : d_value(s, base) {