diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-08-28 01:10:16 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-08-28 01:10:16 +0000 |
commit | cf287f593931a1c4fc141e18845b4c5d36879889 (patch) | |
tree | 4dad0f555b7db01fbeedcd9eace394cd8f7a0fb4 /src/util | |
parent | b7b1c1d99ffa333704af2c8ecd60b1af8833a28b (diff) |
Improved compatibility layer, now supports quantifiers. Also incorporates
numerous bugfixes, and the cvc3 system test is enabled.
Diffstat (limited to 'src/util')
-rw-r--r-- | src/util/Makefile.am | 54 | ||||
-rw-r--r-- | src/util/rational_cln_imp.h | 4 | ||||
-rw-r--r-- | src/util/rational_gmp_imp.h | 2 |
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) { |