diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-09-28 17:29:01 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-09-28 17:29:01 +0000 |
commit | 65f720aac2d497c6e829d9c76638073a10060e7d (patch) | |
tree | 357035797e31f96a37dce30cb97ddb0aaf8f3bb7 /src/util | |
parent | c0c351a89871e0a6881668fa1a8d87349ab8af8e (diff) |
Public interface review items:
* Internal uses of CheckArgument changed to AssertArgument/AlwaysAssertArgument()
* Make util/Assert.h cvc4_private instead of public, so AssertionException and friends are now internal-only
* CheckArgument() throws non-AssertionException
* things outside the core library (parsers, driver) use regular C-style assert,
or a public exception type.
* auto-generated documentation for Smt options and internal options
Also, a small fix to SMT-LIBv1 QF_ABV and QF_AUFBV definitions, which were nonstandard.
Diffstat (limited to 'src/util')
-rw-r--r-- | src/util/Assert.cpp | 2 | ||||
-rw-r--r-- | src/util/Assert.h | 57 | ||||
-rw-r--r-- | src/util/Makefile.am | 1 | ||||
-rw-r--r-- | src/util/ascription_type.h | 2 | ||||
-rw-r--r-- | src/util/bitvector.h | 64 | ||||
-rw-r--r-- | src/util/cardinality.h | 5 | ||||
-rw-r--r-- | src/util/datatype.cpp | 57 | ||||
-rw-r--r-- | src/util/datatype.h | 25 | ||||
-rw-r--r-- | src/util/exception.cpp | 102 | ||||
-rw-r--r-- | src/util/exception.h | 87 | ||||
-rw-r--r-- | src/util/integer_cln_imp.h | 28 | ||||
-rw-r--r-- | src/util/integer_gmp_imp.h | 12 | ||||
-rw-r--r-- | src/util/predicate.h | 2 | ||||
-rw-r--r-- | src/util/rational_cln_imp.h | 5 | ||||
-rw-r--r-- | src/util/rational_gmp_imp.h | 1 | ||||
-rw-r--r-- | src/util/result.h | 14 | ||||
-rw-r--r-- | src/util/sexpr.h | 16 | ||||
-rw-r--r-- | src/util/statistics_registry.cpp | 26 | ||||
-rw-r--r-- | src/util/statistics_registry.h | 61 | ||||
-rw-r--r-- | src/util/subrange_bound.h | 4 |
20 files changed, 375 insertions, 196 deletions
diff --git a/src/util/Assert.cpp b/src/util/Assert.cpp index 11745ad26..e299bef1d 100644 --- a/src/util/Assert.cpp +++ b/src/util/Assert.cpp @@ -27,7 +27,7 @@ using namespace std; namespace CVC4 { #ifdef CVC4_DEBUG -CVC4_THREADLOCAL_PUBLIC(const char*) s_debugLastException = NULL; +CVC4_THREADLOCAL(const char*) s_debugLastException = NULL; #endif /* CVC4_DEBUG */ void AssertionException::construct(const char* header, const char* extra, diff --git a/src/util/Assert.h b/src/util/Assert.h index 3334de4a0..4a6fe4d3a 100644 --- a/src/util/Assert.h +++ b/src/util/Assert.h @@ -16,7 +16,7 @@ ** Assertion utility classes, functions, exceptions, and macros. **/ -#include "cvc4_public.h" +#include "cvc4_private.h" #ifndef __CVC4__ASSERT_H #define __CVC4__ASSERT_H @@ -36,7 +36,7 @@ namespace CVC4 { -class CVC4_PUBLIC AssertionException : public Exception { +class AssertionException : public Exception { protected: void construct(const char* header, const char* extra, const char* function, const char* file, @@ -75,7 +75,7 @@ public: } };/* class AssertionException */ -class CVC4_PUBLIC UnreachableCodeException : public AssertionException { +class UnreachableCodeException : public AssertionException { protected: UnreachableCodeException() : AssertionException() {} @@ -97,7 +97,7 @@ public: } };/* class UnreachableCodeException */ -class CVC4_PUBLIC UnhandledCaseException : public UnreachableCodeException { +class UnhandledCaseException : public UnreachableCodeException { protected: UnhandledCaseException() : UnreachableCodeException() {} @@ -129,7 +129,7 @@ public: } };/* class UnhandledCaseException */ -class CVC4_PUBLIC UnimplementedOperationException : public AssertionException { +class UnimplementedOperationException : public AssertionException { protected: UnimplementedOperationException() : AssertionException() {} @@ -151,14 +151,14 @@ public: } };/* class UnimplementedOperationException */ -class CVC4_PUBLIC IllegalArgumentException : public AssertionException { +class AssertArgumentException : public AssertionException { protected: - IllegalArgumentException() : AssertionException() {} + AssertArgumentException() : AssertionException() {} public: - IllegalArgumentException(const char* argDesc, const char* function, - const char* file, unsigned line, - const char* fmt, ...) : + AssertArgumentException(const char* argDesc, const char* function, + const char* file, unsigned line, + const char* fmt, ...) : AssertionException() { va_list args; va_start(args, fmt); @@ -168,17 +168,17 @@ public: va_end(args); } - IllegalArgumentException(const char* argDesc, const char* function, - const char* file, unsigned line) : + AssertArgumentException(const char* argDesc, const char* function, + const char* file, unsigned line) : AssertionException() { construct("Illegal argument detected", ( std::string("`") + argDesc + "' is a bad argument" ).c_str(), function, file, line); } - IllegalArgumentException(const char* condStr, const char* argDesc, - const char* function, const char* file, - unsigned line, const char* fmt, ...) : + AssertArgumentException(const char* condStr, const char* argDesc, + const char* function, const char* file, + unsigned line, const char* fmt, ...) : AssertionException() { va_list args; va_start(args, fmt); @@ -189,18 +189,18 @@ public: va_end(args); } - IllegalArgumentException(const char* condStr, const char* argDesc, - const char* function, const char* file, - unsigned line) : + AssertArgumentException(const char* condStr, const char* argDesc, + const char* function, const char* file, + unsigned line) : AssertionException() { construct("Illegal argument detected", ( std::string("`") + argDesc + "' is a bad argument; expected " + condStr + " to hold" ).c_str(), function, file, line); } -};/* class IllegalArgumentException */ +};/* class AssertArgumentException */ -class CVC4_PUBLIC InternalErrorException : public AssertionException { +class InternalErrorException : public AssertionException { protected: InternalErrorException() : AssertionException() {} @@ -235,7 +235,7 @@ public: #ifdef CVC4_DEBUG -extern CVC4_THREADLOCAL_PUBLIC(const char*) s_debugLastException; +extern CVC4_THREADLOCAL(const char*) s_debugLastException; /** * Special assertion failure handling in debug mode; in non-debug @@ -247,8 +247,7 @@ extern CVC4_THREADLOCAL_PUBLIC(const char*) s_debugLastException; * debug builds only; in debug builds, it handles all assertion * failures (even those that exist in non-debug builds). */ -void debugAssertionFailed(const AssertionException& thisException, - const char* lastException) CVC4_PUBLIC; +void debugAssertionFailed(const AssertionException& thisException, const char* lastException); // If we're currently handling an exception, print a warning instead; // otherwise std::terminate() is called by the runtime and we lose @@ -283,22 +282,28 @@ void debugAssertionFailed(const AssertionException& thisException, #define InternalError(msg...) \ throw ::CVC4::InternalErrorException(__PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg) #define IllegalArgument(arg, msg...) \ - throw ::CVC4::IllegalArgumentException(#arg, __PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg) + throw ::CVC4::IllegalArgumentException("", #arg, __PRETTY_FUNCTION__, ## msg) #define CheckArgument(cond, arg, msg...) \ - AlwaysAssertArgument(cond, arg, ## msg) + do { \ + if(EXPECT_FALSE( ! (cond) )) { \ + throw ::CVC4::IllegalArgumentException(#cond, #arg, __PRETTY_FUNCTION__, ## msg); \ + } \ + } while(0) #define AlwaysAssertArgument(cond, arg, msg...) \ do { \ if(EXPECT_FALSE( ! (cond) )) { \ - throw ::CVC4::IllegalArgumentException(#cond, #arg, __PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg); \ + throw ::CVC4::AssertArgumentException(#cond, #arg, __PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg); \ } \ } while(0) #ifdef CVC4_ASSERTIONS # define Assert(cond, msg...) AlwaysAssert(cond, ## msg) # define AssertArgument(cond, arg, msg...) AlwaysAssertArgument(cond, arg, ## msg) +# define DebugCheckArgument(cond, arg, msg...) CheckArgument(cond, arg, ## msg) #else /* ! CVC4_ASSERTIONS */ # define Assert(cond, msg...) /*EXPECT_TRUE( cond )*/ # define AssertArgument(cond, arg, msg...) /*EXPECT_TRUE( cond )*/ +# define DebugCheckArgument(cond, arg, msg...) /*EXPECT_TRUE( cond )*/ #endif /* CVC4_ASSERTIONS */ }/* CVC4 namespace */ diff --git a/src/util/Makefile.am b/src/util/Makefile.am index 7d9a055fd..fcbadf490 100644 --- a/src/util/Makefile.am +++ b/src/util/Makefile.am @@ -27,6 +27,7 @@ libutil_la_SOURCES = \ Makefile.in \ debug.h \ exception.h \ + exception.cpp \ hash.h \ bool.h \ proof.h \ diff --git a/src/util/ascription_type.h b/src/util/ascription_type.h index 579746332..4421d6ca7 100644 --- a/src/util/ascription_type.h +++ b/src/util/ascription_type.h @@ -46,7 +46,7 @@ public: };/* class AscriptionType */ /** - * A hash strategy for type ascription operators. + * A hash function for type ascription operators. */ struct CVC4_PUBLIC AscriptionTypeHashFunction { inline size_t operator()(const AscriptionType& at) const { diff --git a/src/util/bitvector.h b/src/util/bitvector.h index 185bb55d9..a3d4f1b60 100644 --- a/src/util/bitvector.h +++ b/src/util/bitvector.h @@ -23,7 +23,7 @@ #define __CVC4__BITVECTOR_H #include <iostream> -#include "util/Assert.h" +#include "util/exception.h" #include "util/integer.h" namespace CVC4 { @@ -99,8 +99,8 @@ public: return d_value != y.d_value; } - BitVector equals(const BitVector& y) const { - Assert(d_size == y.d_size); + BitVector equals(const BitVector& y) const { + CheckArgument(d_size == y.d_size, y); return d_value == y.d_value; } @@ -118,19 +118,19 @@ public: // xor BitVector operator ^(const BitVector& y) const { - Assert (d_size == y.d_size); + CheckArgument(d_size == y.d_size, y); return BitVector(d_size, d_value.bitwiseXor(y.d_value)); } // or BitVector operator |(const BitVector& y) const { - Assert (d_size == y.d_size); + CheckArgument(d_size == y.d_size, y); return BitVector(d_size, d_value.bitwiseOr(y.d_value)); } // and BitVector operator &(const BitVector& y) const { - Assert (d_size == y.d_size); + CheckArgument(d_size == y.d_size, y); return BitVector(d_size, d_value.bitwiseAnd(y.d_value)); } @@ -162,13 +162,13 @@ public: BitVector operator +(const BitVector& y) const { - Assert (d_size == y.d_size); + CheckArgument(d_size == y.d_size, y); Integer sum = d_value + y.d_value; return BitVector(d_size, sum); } BitVector operator -(const BitVector& y) const { - Assert (d_size == y.d_size); + CheckArgument(d_size == y.d_size, y); // to maintain the invariant that we are only adding BitVectors of the // same size BitVector one(d_size, Integer(1)); @@ -181,35 +181,38 @@ public: } BitVector operator *(const BitVector& y) const { - Assert (d_size == y.d_size); + CheckArgument(d_size == y.d_size, y); Integer prod = d_value * y.d_value; return BitVector(d_size, prod); } BitVector unsignedDiv (const BitVector& y) const { - Assert (d_size == y.d_size); + CheckArgument(d_size == y.d_size, y); // TODO: decide whether we really want these semantics if (y.d_value == 0) { return BitVector(d_size, Integer(0)); } - Assert (d_value >= 0 && y.d_value > 0); + CheckArgument(d_value >= 0, this); + CheckArgument(y.d_value > 0, y); return BitVector(d_size, d_value.floorDivideQuotient(y.d_value)); } BitVector unsignedRem(const BitVector& y) const { - Assert (d_size == y.d_size); + CheckArgument(d_size == y.d_size, y); // TODO: decide whether we really want these semantics if (y.d_value == 0) { return BitVector(d_size, Integer(0)); } - Assert (d_value >= 0 && y.d_value > 0); + CheckArgument(d_value >= 0, this); + CheckArgument(y.d_value > 0, y); return BitVector(d_size, d_value.floorDivideRemainder(y.d_value)); } bool signedLessThan(const BitVector& y) const { - Assert(d_size == y.d_size); - Assert(d_value >= 0 && y.d_value >= 0); + CheckArgument(d_size == y.d_size, y); + CheckArgument(d_value >= 0, this); + CheckArgument(y.d_value >= 0, y); Integer a = (*this).toSignedInt(); Integer b = y.toSignedInt(); @@ -217,14 +220,16 @@ public: } bool unsignedLessThan(const BitVector& y) const { - Assert(d_size == y.d_size); - Assert(d_value >= 0 && y.d_value >= 0); + CheckArgument(d_size == y.d_size, y); + CheckArgument(d_value >= 0, this); + CheckArgument(y.d_value >= 0, y); return d_value < y.d_value; } bool signedLessThanEq(const BitVector& y) const { - Assert(d_size == y.d_size); - Assert(d_value >= 0 && y.d_value >= 0); + CheckArgument(d_size == y.d_size, y); + CheckArgument(d_value >= 0, this); + CheckArgument(y.d_value >= 0, y); Integer a = (*this).toSignedInt(); Integer b = y.toSignedInt(); @@ -232,8 +237,9 @@ public: } bool unsignedLessThanEq(const BitVector& y) const { - Assert(d_size == y.d_size); - Assert(d_value >= 0 && y.d_value >= 0); + CheckArgument(d_size == y.d_size, this); + CheckArgument(d_value >= 0, this); + CheckArgument(y.d_value >= 0, y); return d_value <= y.d_value; } @@ -269,7 +275,7 @@ public: } // making sure we don't lose information casting - Assert(y.d_value < Integer(1).multiplyByPow2(32)); + CheckArgument(y.d_value < Integer(1).multiplyByPow2(32), y); uint32_t amount = y.d_value.toUnsignedInt(); Integer res = d_value.multiplyByPow2(amount); return BitVector(d_size, res); @@ -281,7 +287,7 @@ public: } // making sure we don't lose information casting - Assert(y.d_value < Integer(1).multiplyByPow2(32)); + CheckArgument(y.d_value < Integer(1).multiplyByPow2(32), y); uint32_t amount = y.d_value.toUnsignedInt(); Integer res = d_value.divByPow2(amount); return BitVector(d_size, res); @@ -302,7 +308,7 @@ public: } // making sure we don't lose information casting - Assert(y.d_value < Integer(1).multiplyByPow2(32)); + CheckArgument(y.d_value < Integer(1).multiplyByPow2(32), y); uint32_t amount = y.d_value.toUnsignedInt(); Integer rest = d_value.divByPow2(amount); @@ -310,7 +316,7 @@ public: if(sign_bit == Integer(0)) { return BitVector(d_size, rest); } - Integer res = rest.oneExtend(d_size - amount, amount); + Integer res = rest.oneExtend(d_size - amount, amount); return BitVector(d_size, res); } @@ -358,17 +364,15 @@ public: inline BitVector::BitVector(const std::string& num, unsigned base) { - AlwaysAssert( base == 2 || base == 16 ); + CheckArgument(base == 2 || base == 16, base); if( base == 2 ) { d_size = num.size(); - } else if( base == 16 ) { - d_size = num.size() * 4; } else { - Unreachable("Unsupported base in BitVector(std::string&, unsigned int)."); + d_size = num.size() * 4; } - d_value = Integer(num,base); + d_value = Integer(num, base); }/* BitVector::BitVector() */ diff --git a/src/util/cardinality.h b/src/util/cardinality.h index 81a291006..17368c157 100644 --- a/src/util/cardinality.h +++ b/src/util/cardinality.h @@ -26,7 +26,7 @@ #include <utility> #include "util/integer.h" -#include "util/Assert.h" +#include "util/exception.h" namespace CVC4 { @@ -118,7 +118,6 @@ public: CheckArgument(card >= 0, card, "Cardinality must be a nonnegative integer, not %ld.", card); d_card += 1; - Assert(isFinite()); } /** @@ -130,14 +129,12 @@ public: "Cardinality must be a nonnegative integer, not %s.", card.toString().c_str()); d_card += 1; - Assert(isFinite()); } /** * Construct an infinite cardinality equal to the given Beth number. */ Cardinality(CardinalityBeth beth) : d_card(-beth.getNumber() - 1) { - Assert(!isFinite()); } /** diff --git a/src/util/datatype.cpp b/src/util/datatype.cpp index ec8c8e166..ee9c4e406 100644 --- a/src/util/datatype.cpp +++ b/src/util/datatype.cpp @@ -28,6 +28,7 @@ #include "expr/node.h" #include "util/recursion_breaker.h" #include "util/matcher.h" +#include "util/Assert.h" using namespace std; @@ -67,11 +68,11 @@ const Datatype& Datatype::datatypeOf(Expr item) { size_t Datatype::indexOf(Expr item) { ExprManagerScope ems(item); - AssertArgument(item.getType().isConstructor() || - item.getType().isTester() || - item.getType().isSelector(), - item, - "arg must be a datatype constructor, selector, or tester"); + CheckArgument(item.getType().isConstructor() || + item.getType().isTester() || + item.getType().isSelector(), + item, + "arg must be a datatype constructor, selector, or tester"); TNode n = Node::fromExpr(item); if( item.getKind()==kind::APPLY_TYPE_ASCRIPTION ){ return indexOf( item[0] ); @@ -87,29 +88,27 @@ void Datatype::resolve(ExprManager* em, const std::vector<Type>& replacements, const std::vector< SortConstructorType >& paramTypes, const std::vector< DatatypeType >& paramReplacements) - throw(AssertionException, DatatypeResolutionException) { + throw(IllegalArgumentException, DatatypeResolutionException) { - AssertArgument(em != NULL, "cannot resolve a Datatype with a NULL expression manager"); - CheckArgument(!d_resolved, "cannot resolve a Datatype twice"); - AssertArgument(resolutions.find(d_name) != resolutions.end(), + CheckArgument(em != NULL, em, "cannot resolve a Datatype with a NULL expression manager"); + CheckArgument(!d_resolved, this, "cannot resolve a Datatype twice"); + CheckArgument(resolutions.find(d_name) != resolutions.end(), resolutions, "Datatype::resolve(): resolutions doesn't contain me!"); - AssertArgument(placeholders.size() == replacements.size(), placeholders, + CheckArgument(placeholders.size() == replacements.size(), placeholders, "placeholders and replacements must be the same size"); - AssertArgument(paramTypes.size() == paramReplacements.size(), paramTypes, + CheckArgument(paramTypes.size() == paramReplacements.size(), paramTypes, "paramTypes and paramReplacements must be the same size"); CheckArgument(getNumConstructors() > 0, *this, "cannot resolve a Datatype that has no constructors"); DatatypeType self = (*resolutions.find(d_name)).second; - AssertArgument(&self.getDatatype() == this, "Datatype::resolve(): resolutions doesn't contain me!"); + CheckArgument(&self.getDatatype() == this, resolutions, "Datatype::resolve(): resolutions doesn't contain me!"); d_resolved = true; size_t index = 0; for(iterator i = begin(), i_end = end(); i != i_end; ++i) { (*i).resolve(em, self, resolutions, placeholders, replacements, paramTypes, paramReplacements); - Assert((*i).isResolved()); Node::fromExpr((*i).d_constructor).setAttribute(DatatypeIndexAttr(), index); Node::fromExpr((*i).d_tester).setAttribute(DatatypeIndexAttr(), index++); } d_self = self; - Assert(index == getNumConstructors()); } void Datatype::addConstructor(const DatatypeConstructor& c) { @@ -118,7 +117,7 @@ void Datatype::addConstructor(const DatatypeConstructor& c) { d_constructors.push_back(c); } -Cardinality Datatype::getCardinality() const throw(AssertionException) { +Cardinality Datatype::getCardinality() const throw(IllegalArgumentException) { CheckArgument(isResolved(), this, "this datatype is not yet resolved"); RecursionBreaker<const Datatype*, DatatypeHashFunction> breaker(__PRETTY_FUNCTION__, this); if(breaker.isRecursion()) { @@ -131,7 +130,7 @@ Cardinality Datatype::getCardinality() const throw(AssertionException) { return c; } -bool Datatype::isFinite() const throw(AssertionException) { +bool Datatype::isFinite() const throw(IllegalArgumentException) { CheckArgument(isResolved(), this, "this datatype is not yet resolved"); // we're using some internals, so we have to set up this library context @@ -157,7 +156,7 @@ bool Datatype::isFinite() const throw(AssertionException) { return true; } -bool Datatype::isWellFounded() const throw(AssertionException) { +bool Datatype::isWellFounded() const throw(IllegalArgumentException) { CheckArgument(isResolved(), this, "this datatype is not yet resolved"); // we're using some internals, so we have to set up this library context @@ -191,7 +190,7 @@ bool Datatype::isWellFounded() const throw(AssertionException) { return false; } -Expr Datatype::mkGroundTerm( Type t ) const throw(AssertionException) { +Expr Datatype::mkGroundTerm( Type t ) const throw(IllegalArgumentException) { CheckArgument(isResolved(), this, "this datatype is not yet resolved"); // we're using some internals, so we have to set up this library context @@ -274,16 +273,16 @@ Expr Datatype::mkGroundTerm( Type t ) const throw(AssertionException) { } } -DatatypeType Datatype::getDatatypeType() const throw(AssertionException) { +DatatypeType Datatype::getDatatypeType() const throw(IllegalArgumentException) { CheckArgument(isResolved(), *this, "Datatype must be resolved to get its DatatypeType"); - Assert(!d_self.isNull() && !DatatypeType(d_self).isParametric()); + CheckArgument(!d_self.isNull() && !DatatypeType(d_self).isParametric(), this); return DatatypeType(d_self); } DatatypeType Datatype::getDatatypeType(const std::vector<Type>& params) - const throw(AssertionException) { + const throw(IllegalArgumentException) { CheckArgument(isResolved(), *this, "Datatype must be resolved to get its DatatypeType"); - Assert(!d_self.isNull() && DatatypeType(d_self).isParametric()); + CheckArgument(!d_self.isNull() && DatatypeType(d_self).isParametric(), this); return DatatypeType(d_self).instantiate(params); } @@ -394,9 +393,9 @@ void DatatypeConstructor::resolve(ExprManager* em, DatatypeType self, const std::vector<Type>& replacements, const std::vector< SortConstructorType >& paramTypes, const std::vector< DatatypeType >& paramReplacements) - throw(AssertionException, DatatypeResolutionException) { + throw(IllegalArgumentException, DatatypeResolutionException) { - AssertArgument(em != NULL, "cannot resolve a Datatype with a NULL expression manager"); + CheckArgument(em != NULL, em, "cannot resolve a Datatype with a NULL expression manager"); CheckArgument(!isResolved(), "cannot resolve a Datatype constructor twice; " "perhaps the same constructor was added twice, " @@ -577,7 +576,7 @@ Expr DatatypeConstructor::getTester() const { return d_tester; } -Cardinality DatatypeConstructor::getCardinality() const throw(AssertionException) { +Cardinality DatatypeConstructor::getCardinality() const throw(IllegalArgumentException) { CheckArgument(isResolved(), this, "this datatype constructor is not yet resolved"); Cardinality c = 1; @@ -589,7 +588,7 @@ Cardinality DatatypeConstructor::getCardinality() const throw(AssertionException return c; } -bool DatatypeConstructor::isFinite() const throw(AssertionException) { +bool DatatypeConstructor::isFinite() const throw(IllegalArgumentException) { CheckArgument(isResolved(), this, "this datatype constructor is not yet resolved"); // we're using some internals, so we have to set up this library context @@ -615,7 +614,7 @@ bool DatatypeConstructor::isFinite() const throw(AssertionException) { return true; } -bool DatatypeConstructor::isWellFounded() const throw(AssertionException) { +bool DatatypeConstructor::isWellFounded() const throw(IllegalArgumentException) { CheckArgument(isResolved(), this, "this datatype constructor is not yet resolved"); // we're using some internals, so we have to set up this library context @@ -659,7 +658,7 @@ bool DatatypeConstructor::isWellFounded() const throw(AssertionException) { return true; } -Expr DatatypeConstructor::mkGroundTerm( Type t ) const throw(AssertionException) { +Expr DatatypeConstructor::mkGroundTerm( Type t ) const throw(IllegalArgumentException) { CheckArgument(isResolved(), this, "this datatype constructor is not yet resolved"); // we're using some internals, so we have to set up this library context @@ -684,7 +683,7 @@ Expr DatatypeConstructor::mkGroundTerm( Type t ) const throw(AssertionException) groundTerms.push_back(getConstructor()); // for each selector, get a ground term - Assert( t.isDatatype() ); + CheckArgument( t.isDatatype(), t ); std::vector< Type > instTypes; std::vector< Type > paramTypes; if( DatatypeType(t).isParametric() ){ diff --git a/src/util/datatype.h b/src/util/datatype.h index 9853ba417..86bd1cfe3 100644 --- a/src/util/datatype.h +++ b/src/util/datatype.h @@ -35,7 +35,6 @@ namespace CVC4 { #include "expr/expr.h" #include "expr/type.h" -#include "util/Assert.h" #include "util/output.h" #include "util/hash.h" #include "util/exception.h" @@ -155,7 +154,7 @@ private: const std::vector<Type>& replacements, const std::vector< SortConstructorType >& paramTypes, const std::vector< DatatypeType >& paramReplacements) - throw(AssertionException, DatatypeResolutionException); + throw(IllegalArgumentException, DatatypeResolutionException); friend class Datatype; /** Helper function for resolving parametric datatypes. @@ -260,28 +259,28 @@ public: * Return the cardinality of this constructor (the product of the * cardinalities of its arguments). */ - Cardinality getCardinality() const throw(AssertionException); + Cardinality getCardinality() const throw(IllegalArgumentException); /** * Return true iff this constructor is finite (it is nullary or * each of its argument types are finite). This function can * only be called for resolved constructors. */ - bool isFinite() const throw(AssertionException); + bool isFinite() const throw(IllegalArgumentException); /** * Return true iff this constructor is well-founded (there exist * ground terms). The constructor must be resolved or an * exception is thrown. */ - bool isWellFounded() const throw(AssertionException); + bool isWellFounded() const throw(IllegalArgumentException); /** * Construct and return a ground term of this constructor. The * constructor must be both resolved and well-founded, or else an * exception is thrown. */ - Expr mkGroundTerm( Type t ) const throw(AssertionException); + Expr mkGroundTerm( Type t ) const throw(IllegalArgumentException); /** * Returns true iff this Datatype constructor has already been @@ -441,7 +440,7 @@ private: const std::vector<Type>& replacements, const std::vector< SortConstructorType >& paramTypes, const std::vector< DatatypeType >& paramReplacements) - throw(AssertionException, DatatypeResolutionException); + throw(IllegalArgumentException, DatatypeResolutionException); friend class ExprManager;// for access to resolve() public: @@ -484,7 +483,7 @@ public: * cardinalities of its constructors). The Datatype must be * resolved. */ - Cardinality getCardinality() const throw(AssertionException); + Cardinality getCardinality() const throw(IllegalArgumentException); /** * Return true iff this Datatype is finite (all constructors are @@ -492,32 +491,32 @@ public: * datatype is not well-founded, this function returns false. The * Datatype must be resolved or an exception is thrown. */ - bool isFinite() const throw(AssertionException); + bool isFinite() const throw(IllegalArgumentException); /** * Return true iff this datatype is well-founded (there exist ground * terms). The Datatype must be resolved or an exception is thrown. */ - bool isWellFounded() const throw(AssertionException); + bool isWellFounded() const throw(IllegalArgumentException); /** * Construct and return a ground term of this Datatype. The * Datatype must be both resolved and well-founded, or else an * exception is thrown. */ - Expr mkGroundTerm( Type t ) const throw(AssertionException); + Expr mkGroundTerm( Type t ) const throw(IllegalArgumentException); /** * Get the DatatypeType associated to this Datatype. Can only be * called post-resolution. */ - DatatypeType getDatatypeType() const throw(AssertionException); + DatatypeType getDatatypeType() const throw(IllegalArgumentException); /** * Get the DatatypeType associated to this (parameterized) Datatype. Can only be * called post-resolution. */ - DatatypeType getDatatypeType(const std::vector<Type>& params) const throw(AssertionException); + DatatypeType getDatatypeType(const std::vector<Type>& params) const throw(IllegalArgumentException); /** * Return true iff the two Datatypes are the same. diff --git a/src/util/exception.cpp b/src/util/exception.cpp new file mode 100644 index 000000000..d31f52fe7 --- /dev/null +++ b/src/util/exception.cpp @@ -0,0 +1,102 @@ +/********************* */ +/*! \file exception.cpp + ** \verbatim + ** Original author: mdeters + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** 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 CVC4's exception base class and some associated utilities + ** + ** CVC4's exception base class and some associated utilities. + **/ + +#include "util/exception.h" +#include <string> +#include <cstdio> +#include <cstdlib> +#include <cstdarg> + +using namespace std; +using namespace CVC4; + +void IllegalArgumentException::construct(const char* header, const char* extra, + const char* function, const char* fmt, + va_list args) { + // try building the exception msg with a smallish buffer first, + // then with a larger one if sprintf tells us to. + int n = 512; + char* buf; + + for(;;) { + buf = new char[n]; + + int size; + if(extra == NULL) { + size = snprintf(buf, n, "%s\n%s\n", + header, function); + } else { + size = snprintf(buf, n, "%s\n%s\n\n %s\n", + header, function, extra); + } + + if(size < n) { + va_list args_copy; + va_copy(args_copy, args); + size += vsnprintf(buf + size, n - size, fmt, args_copy); + va_end(args_copy); + + if(size < n) { + break; + } + } + + if(size >= n) { + // try again with a buffer that's large enough + n = size + 1; + delete [] buf; + } + } + + setMessage(string(buf)); + + delete [] buf; +} + +void IllegalArgumentException::construct(const char* header, const char* extra, + const char* function) { + // try building the exception msg with a smallish buffer first, + // then with a larger one if sprintf tells us to. + int n = 256; + char* buf; + + for(;;) { + buf = new char[n]; + + int size; + if(extra == NULL) { + size = snprintf(buf, n, "%s.\n%s\n", + header, function); + } else { + size = snprintf(buf, n, "%s.\n%s\n\n %s\n", + header, function, extra); + } + + if(size < n) { + break; + } else { + // try again with a buffer that's large enough + n = size + 1; + delete [] buf; + } + } + + setMessage(string(buf)); + + delete [] buf; +} diff --git a/src/util/exception.h b/src/util/exception.h index fe01eba36..89e42b6d1 100644 --- a/src/util/exception.h +++ b/src/util/exception.h @@ -11,7 +11,7 @@ ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** - ** \brief CVC4's exception base class and some associated utilities. + ** \brief CVC4's exception base class and some associated utilities ** ** CVC4's exception base class and some associated utilities. **/ @@ -25,6 +25,8 @@ #include <string> #include <sstream> #include <exception> +#include <cstdlib> +#include <cstdarg> namespace CVC4 { @@ -75,6 +77,51 @@ public: };/* class Exception */ +class CVC4_PUBLIC IllegalArgumentException : public Exception { +protected: + IllegalArgumentException() : Exception() {} + + void construct(const char* header, const char* extra, + const char* function, const char* fmt, ...) { + va_list args; + va_start(args, fmt); + construct(header, extra, function, fmt, args); + va_end(args); + } + + void construct(const char* header, const char* extra, + const char* function, const char* fmt, va_list args); + + void construct(const char* header, const char* extra, + const char* function); + +public: + IllegalArgumentException(const char* condStr, const char* argDesc, + const char* function, const char* fmt, ...) : + Exception() { + va_list args; + va_start(args, fmt); + construct("Illegal argument detected", + ( std::string("`") + argDesc + "' is a bad argument" + + (*condStr == '\0' ? std::string() : + ( std::string("; expected ") + + condStr + " to hold" )) ).c_str(), + function, fmt, args); + va_end(args); + } + + IllegalArgumentException(const char* condStr, const char* argDesc, + const char* function) : + Exception() { + construct("Illegal argument detected", + ( std::string("`") + argDesc + "' is a bad argument" + + (*condStr == '\0' ? std::string() : + ( std::string("; expected ") + + condStr + " to hold" )) ).c_str(), + function); + } +};/* class IllegalArgumentException */ + inline std::ostream& operator<<(std::ostream& os, const Exception& e) throw() CVC4_PUBLIC; inline std::ostream& operator<<(std::ostream& os, const Exception& e) throw() { e.toStream(os); @@ -83,4 +130,42 @@ inline std::ostream& operator<<(std::ostream& os, const Exception& e) throw() { }/* CVC4 namespace */ +#if defined(__BUILDING_CVC4LIB) || defined(__BUILDING_CVC4LIB_UNIT_TEST) +# include "util/Assert.h" +#endif /* __BUILDING_CVC4LIB || __BUILDING_CVC4LIB_UNIT_TEST */ + +namespace CVC4 { + +#ifndef CheckArgument +template <class T> inline void CheckArgument(bool cond, const T& arg, const char* fmt, ...) CVC4_PUBLIC; +template <class T> inline void CheckArgument(bool cond, const T& arg, const char* fmt, ...) { + if(EXPECT_FALSE( !cond )) { \ + throw ::CVC4::IllegalArgumentException("", "", ""); \ + } \ +} +template <class T> inline void CheckArgument(bool cond, const T& arg) CVC4_PUBLIC; +template <class T> inline void CheckArgument(bool cond, const T& arg) { + if(EXPECT_FALSE( !cond )) { \ + throw ::CVC4::IllegalArgumentException("", "", ""); \ + } \ +} +#endif /* CheckArgument */ + +#ifndef DebugCheckArgument +template <class T> inline void DebugCheckArgument(bool cond, const T& arg, const char* fmt, ...) CVC4_PUBLIC; +template <class T> inline void DebugCheckArgument(bool cond, const T& arg, const char* fmt, ...) { + if(EXPECT_FALSE( !cond )) { \ + throw ::CVC4::IllegalArgumentException("", "", ""); \ + } \ +} +template <class T> inline void DebugCheckArgument(bool cond, const T& arg) CVC4_PUBLIC; +template <class T> inline void DebugCheckArgument(bool cond, const T& arg) { + if(EXPECT_FALSE( !cond )) { \ + throw ::CVC4::IllegalArgumentException("", "", ""); \ + } \ +} +#endif /* DebugCheckArgument */ + +}/* CVC4 namespace */ + #endif /* __CVC4__EXCEPTION_H */ diff --git a/src/util/integer_cln_imp.h b/src/util/integer_cln_imp.h index 7fd6a2694..5dfcae6d2 100644 --- a/src/util/integer_cln_imp.h +++ b/src/util/integer_cln_imp.h @@ -31,7 +31,7 @@ #include <cln/integer_io.h> #include <limits> -#include "util/Assert.h" +#include "util/exception.h" namespace CVC4 { @@ -232,7 +232,7 @@ public: } Integer oneExtend(uint32_t size, uint32_t amount) const { - Assert((*this) < Integer(1).multiplyByPow2(size)); + DebugCheckArgument((*this) < Integer(1).multiplyByPow2(size), size); cln::cl_byte range(amount, size); cln::cl_I allones = (cln::cl_I(1) << (size + amount))- 1; // 2^size - 1 Integer temp(allones); @@ -291,7 +291,7 @@ public: * If y divides *this, then exactQuotient returns (this/y) */ Integer exactQuotient(const Integer& y) const { - Assert(y.divides(*this)); + DebugCheckArgument(y.divides(*this), y); return Integer( cln::exquo(d_value, y.d_value) ); } @@ -316,7 +316,7 @@ public: }else if(exp == 0){ return Integer( 1 ); }else{ - Unimplemented(); + throw Exception("Negative exponent in Integer::pow()"); } } @@ -367,8 +367,7 @@ public: fprinthexadecimal(ss,d_value); break; default: - Unhandled(); - break; + throw Exception("Unhandled base in Integer::toString()"); } std::string output = ss.str(); for( unsigned i = 0; i <= output.length(); ++i){ @@ -382,7 +381,6 @@ public: int sgn() const { cln::cl_I sgn = cln::signum(d_value); - Assert(sgn == 0 || sgn == -1 || sgn == 1); return cln::cl_I_to_int(sgn); } @@ -402,19 +400,19 @@ public: long getLong() const { // ensure there isn't overflow - AlwaysAssert(d_value <= std::numeric_limits<long>::max(), - "Overflow detected in Integer::getLong()"); - AlwaysAssert(d_value >= std::numeric_limits<long>::min(), - "Overflow detected in Integer::getLong()"); + CheckArgument(d_value <= std::numeric_limits<long>::max(), this, + "Overflow detected in Integer::getLong()"); + CheckArgument(d_value >= std::numeric_limits<long>::min(), this, + "Overflow detected in Integer::getLong()"); return cln::cl_I_to_long(d_value); } unsigned long getUnsignedLong() const { // ensure there isn't overflow - AlwaysAssert(d_value <= std::numeric_limits<unsigned long>::max(), - "Overflow detected in Integer::getUnsignedLong()"); - AlwaysAssert(d_value >= std::numeric_limits<unsigned long>::min(), - "Overflow detected in Integer::getUnsignedLong()"); + CheckArgument(d_value <= std::numeric_limits<unsigned long>::max(), this, + "Overflow detected in Integer::getUnsignedLong()"); + CheckArgument(d_value >= std::numeric_limits<unsigned long>::min(), this, + "Overflow detected in Integer::getUnsignedLong()"); return cln::cl_I_to_ulong(d_value); } diff --git a/src/util/integer_gmp_imp.h b/src/util/integer_gmp_imp.h index 5b6468a9e..66428ec41 100644 --- a/src/util/integer_gmp_imp.h +++ b/src/util/integer_gmp_imp.h @@ -25,8 +25,8 @@ #include <string> #include <iostream> -#include "util/Assert.h" #include "util/gmp_util.h" +#include "util/exception.h" namespace CVC4 { @@ -178,7 +178,7 @@ public: */ Integer oneExtend(uint32_t size, uint32_t amount) const { // check that the size is accurate - Assert ((*this) < Integer(1).multiplyByPow2(size)); + DebugCheckArgument((*this) < Integer(1).multiplyByPow2(size), size); mpz_class res = d_value; for (unsigned i = size; i < size + amount; ++i) { @@ -251,7 +251,7 @@ public: * If y divides *this, then exactQuotient returns (this/y) */ Integer exactQuotient(const Integer& y) const { - Assert(y.divides(*this)); + DebugCheckArgument(y.divides(*this), y); mpz_class q; mpz_divexact(q.get_mpz_t(), d_value.get_mpz_t(), y.d_value.get_mpz_t()); return Integer( q ); @@ -346,15 +346,15 @@ public: long getLong() const { long si = d_value.get_si(); // ensure there wasn't overflow - AlwaysAssert(mpz_cmp_si(d_value.get_mpz_t(), si) == 0, + CheckArgument(mpz_cmp_si(d_value.get_mpz_t(), si) == 0, this, "Overflow detected in Integer::getLong()"); return si; } unsigned long getUnsignedLong() const { unsigned long ui = d_value.get_ui(); // ensure there wasn't overflow - AlwaysAssert(mpz_cmp_ui(d_value.get_mpz_t(), ui) == 0, - "Overflow detected in Integer::getUnsignedLong()"); + CheckArgument(mpz_cmp_ui(d_value.get_mpz_t(), ui) == 0, this, + "Overflow detected in Integer::getUnsignedLong()"); return ui; } diff --git a/src/util/predicate.h b/src/util/predicate.h index 18e0b8b70..ba050bd43 100644 --- a/src/util/predicate.h +++ b/src/util/predicate.h @@ -23,7 +23,7 @@ #ifndef __CVC4__PREDICATE_H #define __CVC4__PREDICATE_H -#include "util/Assert.h" +#include "util/exception.h" namespace CVC4 { diff --git a/src/util/rational_cln_imp.h b/src/util/rational_cln_imp.h index 182e813cd..575f09ef5 100644 --- a/src/util/rational_cln_imp.h +++ b/src/util/rational_cln_imp.h @@ -25,6 +25,7 @@ #include <gmp.h> #include <string> #include <sstream> +#include <cassert> #include <cln/rational.h> #include <cln/input.h> #include <cln/io.h> @@ -32,7 +33,7 @@ #include <cln/rational_io.h> #include <cln/number_io.h> -#include "util/Assert.h" +#include "util/exception.h" #include "util/integer.h" namespace CVC4 { @@ -213,7 +214,7 @@ public: }else if(cln::minusp(d_value)){ return -1; }else{ - Assert(cln::plusp(d_value)); + assert(cln::plusp(d_value)); return 1; } } diff --git a/src/util/rational_gmp_imp.h b/src/util/rational_gmp_imp.h index b86dc32f2..383f0fb2b 100644 --- a/src/util/rational_gmp_imp.h +++ b/src/util/rational_gmp_imp.h @@ -26,6 +26,7 @@ #include <string> #include "util/integer.h" +#include "util/exception.h" namespace CVC4 { diff --git a/src/util/result.h b/src/util/result.h index f0cf3f20e..0894007bc 100644 --- a/src/util/result.h +++ b/src/util/result.h @@ -24,16 +24,10 @@ #include <iostream> #include <string> -#include "util/Assert.h" +#include "util/exception.h" namespace CVC4 { -// TODO: either templatize Result on its Kind (Sat/Validity) or subclass. -// TODO: INVALID/SAT provide models, etc?---perhaps just by linking back -// into the SmtEngine that produced the Result? -// TODO: make unconstructible except by SmtEngine? That would ensure that -// any Result in the system is bona fide. - class Result; std::ostream& operator<<(std::ostream& out, const Result& r) CVC4_PUBLIC; @@ -137,9 +131,9 @@ public: return d_which == TYPE_NONE; } enum UnknownExplanation whyUnknown() const { - AlwaysAssert( isUnknown(), - "This result is not unknown, so the reason for " - "being unknown cannot be inquired of it" ); + CheckArgument( isUnknown(), this, + "This result is not unknown, so the reason for " + "being unknown cannot be inquired of it" ); return d_unknownExplanation; } diff --git a/src/util/sexpr.h b/src/util/sexpr.h index 4feffc18f..345a6c132 100644 --- a/src/util/sexpr.h +++ b/src/util/sexpr.h @@ -28,7 +28,7 @@ #include "util/integer.h" #include "util/rational.h" -#include "util/Assert.h" +#include "util/exception.h" namespace CVC4 { @@ -182,7 +182,7 @@ inline bool SExpr::isKeyword() const { } inline std::string SExpr::getValue() const { - AlwaysAssert( isAtom() ); + CheckArgument( isAtom(), this ); switch(d_sexprType) { case SEXPR_INTEGER: return d_integerValue.toString(); @@ -198,24 +198,24 @@ inline std::string SExpr::getValue() const { case SEXPR_STRING: case SEXPR_KEYWORD: return d_stringValue; - default: - Unhandled(d_sexprType); + case SEXPR_NOT_ATOM: + return std::string(); } - return d_stringValue; + return std::string(); } inline const CVC4::Integer& SExpr::getIntegerValue() const { - AlwaysAssert( isInteger() ); + CheckArgument( isInteger(), this ); return d_integerValue; } inline const CVC4::Rational& SExpr::getRationalValue() const { - AlwaysAssert( isRational() ); + CheckArgument( isRational(), this ); return d_rationalValue; } inline const std::vector<SExpr>& SExpr::getChildren() const { - AlwaysAssert( !isAtom() ); + CheckArgument( !isAtom(), this ); return d_children; } diff --git a/src/util/statistics_registry.cpp b/src/util/statistics_registry.cpp index f2a698a48..48e1355ec 100644 --- a/src/util/statistics_registry.cpp +++ b/src/util/statistics_registry.cpp @@ -50,36 +50,38 @@ StatisticsRegistry* StatisticsRegistry::current() { return stats::getStatisticsRegistry(smt::currentSmtEngine()); } -void StatisticsRegistry::registerStat(Stat* s) throw(AssertionException) { +void StatisticsRegistry::registerStat(Stat* s) throw(CVC4::IllegalArgumentException) { #ifdef CVC4_STATISTICS_ON StatSet& stats = current()->d_stats; - AlwaysAssert(stats.find(s) == stats.end(), - "Statistic `%s' was already registered with this registry.", s->getName().c_str()); + CheckArgument(stats.find(s) == stats.end(), s, + "Statistic `%s' was already registered with this registry.", + s->getName().c_str()); stats.insert(s); #endif /* CVC4_STATISTICS_ON */ }/* StatisticsRegistry::registerStat() */ -void StatisticsRegistry::unregisterStat(Stat* s) throw(AssertionException) { +void StatisticsRegistry::unregisterStat(Stat* s) throw(CVC4::IllegalArgumentException) { #ifdef CVC4_STATISTICS_ON StatSet& stats = current()->d_stats; - AlwaysAssert(stats.find(s) != stats.end(), - "Statistic `%s' was not registered with this registry.", s->getName().c_str()); + CheckArgument(stats.find(s) != stats.end(), s, + "Statistic `%s' was not registered with this registry.", + s->getName().c_str()); stats.erase(s); #endif /* CVC4_STATISTICS_ON */ }/* StatisticsRegistry::unregisterStat() */ #endif /* ! __BUILDING_STATISTICS_FOR_EXPORT */ -void StatisticsRegistry::registerStat_(Stat* s) throw(AssertionException) { +void StatisticsRegistry::registerStat_(Stat* s) throw(CVC4::IllegalArgumentException) { #ifdef CVC4_STATISTICS_ON - AlwaysAssert(d_stats.find(s) == d_stats.end()); + CheckArgument(d_stats.find(s) == d_stats.end(), s); d_stats.insert(s); #endif /* CVC4_STATISTICS_ON */ }/* StatisticsRegistry::registerStat_() */ -void StatisticsRegistry::unregisterStat_(Stat* s) throw(AssertionException) { +void StatisticsRegistry::unregisterStat_(Stat* s) throw(CVC4::IllegalArgumentException) { #ifdef CVC4_STATISTICS_ON - AlwaysAssert(d_stats.find(s) != d_stats.end()); + CheckArgument(d_stats.find(s) != d_stats.end(), s); d_stats.erase(s); #endif /* CVC4_STATISTICS_ON */ }/* StatisticsRegistry::unregisterStat_() */ @@ -98,7 +100,7 @@ void StatisticsRegistry::flushInformation(std::ostream &out) const { void TimerStat::start() { if(__CVC4_USE_STATISTICS) { - AlwaysAssert(!d_running); + CheckArgument(!d_running, *this, "timer already running"); clock_gettime(CLOCK_MONOTONIC, &d_start); d_running = true; } @@ -106,7 +108,7 @@ void TimerStat::start() { void TimerStat::stop() { if(__CVC4_USE_STATISTICS) { - AlwaysAssert(d_running); + CheckArgument(d_running, *this, "timer not running"); ::timespec end; clock_gettime(CLOCK_MONOTONIC, &end); d_data += end - d_start; diff --git a/src/util/statistics_registry.h b/src/util/statistics_registry.h index 870a88d66..99168353f 100644 --- a/src/util/statistics_registry.h +++ b/src/util/statistics_registry.h @@ -30,8 +30,7 @@ #include <ctime> #include <vector> #include <stdint.h> - -#include "util/Assert.h" +#include <cassert> namespace CVC4 { @@ -69,10 +68,11 @@ public: * will throw an assertion exception if the given name contains the * statistic delimiter string. */ - Stat(const std::string& name) throw(CVC4::AssertionException) : + Stat(const std::string& name) throw(CVC4::IllegalArgumentException) : d_name(name) { if(__CVC4_USE_STATISTICS) { - AlwaysAssert(d_name.find(", ") == std::string::npos); + CheckArgument(d_name.find(", ") == std::string::npos, name, + "Statistics names cannot include a comma (',')"); } } @@ -270,11 +270,7 @@ public: /** Get the value of the referenced data cell. */ const T& getData() const { - if(__CVC4_USE_STATISTICS) { - return *d_data; - } else { - Unreachable(); - } + return *d_data; } };/* class ReferenceStat<T> */ @@ -316,11 +312,7 @@ public: /** Get the underlying data value. */ const T& getData() const { - if(__CVC4_USE_STATISTICS) { - return d_data; - } else { - Unreachable(); - } + return d_data; } };/* class BackedStat<T> */ @@ -362,11 +354,7 @@ public: /** Get the data of the underlying (wrapped) statistic. */ const T& getData() const { - if(__CVC4_USE_STATISTICS) { - return d_stat.getData(); - } else { - Unreachable(); - } + return d_stat.getData(); } SExpr getValue() const { @@ -569,11 +557,14 @@ public: StatisticsRegistry() {} /** Construct a statistics registry */ - StatisticsRegistry(const std::string& name) throw(CVC4::AssertionException) : + StatisticsRegistry(const std::string& name) + throw(CVC4::IllegalArgumentException) : Stat(name) { d_prefix = name; if(__CVC4_USE_STATISTICS) { - AlwaysAssert(d_name.find(s_regDelim) == std::string::npos); + CheckArgument(d_name.find(s_regDelim) == std::string::npos, name, + "StatisticsRegistry names cannot contain the string \"%s\"", + s_regDelim.c_str()); } } @@ -608,17 +599,17 @@ public: #if (defined(__BUILDING_CVC4LIB) || defined(__BUILDING_CVC4LIB_UNIT_TEST)) && !defined(__BUILDING_STATISTICS_FOR_EXPORT) /** Register a new statistic, making it active. */ - static void registerStat(Stat* s) throw(AssertionException); + static void registerStat(Stat* s) throw(CVC4::IllegalArgumentException); /** Unregister an active statistic, making it inactive. */ - static void unregisterStat(Stat* s) throw(AssertionException); + static void unregisterStat(Stat* s) throw(CVC4::IllegalArgumentException); #endif /* (__BUILDING_CVC4LIB || __BUILDING_CVC4LIB) && ! __BUILDING_STATISTICS_FOR_EXPORT */ /** Register a new statistic */ - void registerStat_(Stat* s) throw(AssertionException); + void registerStat_(Stat* s) throw(CVC4::IllegalArgumentException); /** Unregister a new statistic */ - void unregisterStat_(Stat* s) throw(AssertionException); + void unregisterStat_(Stat* s) throw(CVC4::IllegalArgumentException); };/* class StatisticsRegistry */ @@ -630,11 +621,11 @@ public: inline timespec& operator+=(timespec& a, const timespec& b) { // assumes a.tv_nsec and b.tv_nsec are in range const long nsec_per_sec = 1000000000L; // one thousand million - Assert(a.tv_nsec >= 0 && a.tv_nsec < nsec_per_sec); - Assert(b.tv_nsec >= 0 && b.tv_nsec < nsec_per_sec); + CheckArgument(a.tv_nsec >= 0 && a.tv_nsec < nsec_per_sec, a); + CheckArgument(b.tv_nsec >= 0 && b.tv_nsec < nsec_per_sec, b); a.tv_sec += b.tv_sec; long nsec = a.tv_nsec + b.tv_nsec; - Assert(nsec >= 0); + assert(nsec >= 0); if(nsec < 0) { nsec += nsec_per_sec; --a.tv_sec; @@ -643,7 +634,7 @@ inline timespec& operator+=(timespec& a, const timespec& b) { nsec -= nsec_per_sec; ++a.tv_sec; } - Assert(nsec >= 0 && nsec < nsec_per_sec); + assert(nsec >= 0 && nsec < nsec_per_sec); a.tv_nsec = nsec; return a; } @@ -652,8 +643,8 @@ inline timespec& operator+=(timespec& a, const timespec& b) { inline timespec& operator-=(timespec& a, const timespec& b) { // assumes a.tv_nsec and b.tv_nsec are in range const long nsec_per_sec = 1000000000L; // one thousand million - Assert(a.tv_nsec >= 0 && a.tv_nsec < nsec_per_sec); - Assert(b.tv_nsec >= 0 && b.tv_nsec < nsec_per_sec); + CheckArgument(a.tv_nsec >= 0 && a.tv_nsec < nsec_per_sec, a); + CheckArgument(b.tv_nsec >= 0 && b.tv_nsec < nsec_per_sec, b); a.tv_sec -= b.tv_sec; long nsec = a.tv_nsec - b.tv_nsec; if(nsec < 0) { @@ -664,7 +655,7 @@ inline timespec& operator-=(timespec& a, const timespec& b) { nsec -= nsec_per_sec; ++a.tv_sec; } - Assert(nsec >= 0 && nsec < nsec_per_sec); + assert(nsec >= 0 && nsec < nsec_per_sec); a.tv_nsec = nsec; return a; } @@ -855,9 +846,9 @@ public: RegisterStatistic(StatisticsRegistry* reg, Stat* stat) : d_reg(reg), d_stat(stat) { - Assert(d_reg != NULL, - "You need to specify a statistics registry" - "on which to set the statistic"); + CheckArgument(reg != NULL, reg, + "You need to specify a statistics registry" + "on which to set the statistic"); d_reg->registerStat_(d_stat); } diff --git a/src/util/subrange_bound.h b/src/util/subrange_bound.h index 5de17106d..ffb2a1eaf 100644 --- a/src/util/subrange_bound.h +++ b/src/util/subrange_bound.h @@ -23,7 +23,7 @@ #define __CVC4__SUBRANGE_BOUND_H #include "util/integer.h" -#include "util/Assert.h" +#include "util/exception.h" #include <limits> @@ -222,7 +222,7 @@ public: * precondition: joinIsBounded(a,b) is true */ static SubrangeBounds join(const SubrangeBounds& a, const SubrangeBounds& b){ - Assert(joinIsBounded(a,b)); + DebugCheckArgument(joinIsBounded(a,b), a); SubrangeBound newLower = SubrangeBound::min(a.lower, b.lower); SubrangeBound newUpper = SubrangeBound::max(a.upper, b.upper); return SubrangeBounds(newLower, newUpper); |