diff options
| author | Tim King <taking@google.com> | 2015-12-24 05:38:43 -0500 |
|---|---|---|
| committer | Tim King <taking@google.com> | 2015-12-24 05:38:43 -0500 |
| commit | a39ad6584c1d61e22e72b53c3838f4f675ed2e19 (patch) | |
| tree | ed40cb371c41ac285ca2bf41a82254a36134e132 | |
| parent | 87b0fe9ce10d1e5e9ed5a3e7db77f46bf3f68922 (diff) | |
Miscellaneous fixes
- Splitting the two instances of CheckArgument. The template version is now always defined in base/exception.h and is available in a cvc4_public header. This version has lost its variadic version (due to swig not supporting va_list's). The CPP macro version has been renamed PrettyCheckArgument. (Taking suggestions for a better name.) This is now only defined in base/cvc4_assert.h. Only use this in cvc4_private headers and in .cpp files that can use cvc4_private headers. To use a variadic version of CheckArguments, outside of this scope, you need to duplicate this macro locally. See cvc3_compat.cpp for an example.
- Making fitsSignedInt() and fitsUnsignedInt() work more robustly for CLN on 32 bit systems.
- Refactoring ArrayStoreAll to avoid potential problems with circular header inclusions.
- Changing some headers to use iosfwd when possible.
76 files changed, 1522 insertions, 1070 deletions
diff --git a/src/base/cvc4_assert.h b/src/base/cvc4_assert.h index 6dca5c81d..6b47de8cc 100644 --- a/src/base/cvc4_assert.h +++ b/src/base/cvc4_assert.h @@ -282,11 +282,15 @@ void debugAssertionFailed(const AssertionException& thisException, const char* l #define InternalError(msg...) \ throw ::CVC4::InternalErrorException(__PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg) #define IllegalArgument(arg, msg...) \ - throw ::CVC4::IllegalArgumentException("", #arg, __PRETTY_FUNCTION__, ## msg) -#define CheckArgument(cond, arg, msg...) \ + throw ::CVC4::IllegalArgumentException("", #arg, __PRETTY_FUNCTION__, \ + ::CVC4::IllegalArgumentException::formatVariadic(msg).c_str()); +// This cannot use check argument directly as this forces +// CheckArgument to use a va_list. This is unsupported in Swig. +#define PrettyCheckArgument(cond, arg, msg...) \ do { \ if(__builtin_expect( ( ! (cond) ), false )) { \ - throw ::CVC4::IllegalArgumentException(#cond, #arg, __PRETTY_FUNCTION__, ## msg); \ + throw ::CVC4::IllegalArgumentException(#cond, #arg, __PRETTY_FUNCTION__, \ + ::CVC4::IllegalArgumentException::formatVariadic(msg).c_str()); \ } \ } while(0) #define AlwaysAssertArgument(cond, arg, msg...) \ diff --git a/src/base/exception.cpp b/src/base/exception.cpp index d8eee50bc..87bdfcfa5 100644 --- a/src/base/exception.cpp +++ b/src/base/exception.cpp @@ -15,6 +15,7 @@ **/ #include "base/exception.h" + #include <string> #include <cstdio> #include <cstdlib> @@ -24,12 +25,58 @@ using namespace std; -#warning "TODO: Remove the second definition of CheckArgument and DebugCheckArgument." - namespace CVC4 { + +char* IllegalArgumentException::s_header = "Illegal argument detected"; + +std::string IllegalArgumentException::formatVariadic() { + return std::string(); +} + +std::string IllegalArgumentException::formatVariadic(const char* format, ...) { + va_list args; + va_start(args, format); + + int n = 512; + char* buf = NULL; + + for (int i = 0; i < 2; ++i){ + Assert(n > 0); + if(buf != NULL){ + delete [] buf; + } + buf = new char[n]; + + va_list args_copy; + va_copy(args_copy, args); + int size = vsnprintf(buf, n, format, args); + va_end(args_copy); + + if(size >= n){ + buf[n-1] = '\0'; + n = size + 1; + } else { + break; + } + } + // buf is not NULL is an invariant. + // buf is also 0 terminated. + Assert(buf != NULL); + std::string result(buf); + delete [] buf; + va_end(args); + return result; +} + +std::string IllegalArgumentException::format_extra(const char* condStr, const char* argDesc){ + return ( std::string("`") + argDesc + "' is a bad argument" + + (*condStr == '\0' ? std::string() : + ( std::string("; expected ") + + condStr + " to hold" )) ); +} + void IllegalArgumentException::construct(const char* header, const char* extra, - const char* function, const char* fmt, - va_list args) { + const char* function, const char* tail) { // try building the exception msg with a smallish buffer first, // then with a larger one if sprintf tells us to. int n = 512; @@ -40,25 +87,17 @@ void IllegalArgumentException::construct(const char* header, const char* extra, int size; if(extra == NULL) { - size = snprintf(buf, n, "%s\n%s\n", - header, function); + size = snprintf(buf, n, "%s\n%s\n%s", + header, function, tail); } else { - size = snprintf(buf, n, "%s\n%s\n\n %s\n", - header, function, extra); + size = snprintf(buf, n, "%s\n%s\n\n %s\n%s", + header, function, extra, tail); } 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) { + break; + } else { + // size >= n // try again with a buffer that's large enough n = size + 1; delete [] buf; diff --git a/src/base/exception.h b/src/base/exception.h index 78bb160cc..84872b9b1 100644 --- a/src/base/exception.h +++ b/src/base/exception.h @@ -19,13 +19,13 @@ #ifndef __CVC4__EXCEPTION_H #define __CVC4__EXCEPTION_H -#include <iostream> -#include <string> +#include <cstdarg> +#include <cstdlib> +#include <exception> +#include <iosfwd> #include <sstream> #include <stdexcept> -#include <exception> -#include <cstdlib> -#include <cstdarg> +#include <string> namespace CVC4 { @@ -81,44 +81,37 @@ 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); + const char* function, const char* tail); void construct(const char* header, const char* extra, const char* function); + static std::string format_extra(const char* condStr, const char* argDesc); + + static char* s_header; + public: + IllegalArgumentException(const char* condStr, const char* argDesc, - const char* function, const char* fmt, ...) : + const char* function, const char* tail) : 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); + construct(s_header, format_extra(condStr, argDesc).c_str(), function, tail); } 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); + construct(s_header, format_extra(condStr, argDesc).c_str(), function); } + + /** + * This is a convenience function for building usages that are variadic. + * + * Having IllegalArgumentException itself be variadic is problematic for + * making sure calls to IllegalArgumentException clean up memory. + */ + static std::string formatVariadic(); + static std::string formatVariadic(const char* format, ...); };/* class IllegalArgumentException */ inline std::ostream& operator<<(std::ostream& os, const Exception& e) throw() CVC4_PUBLIC; @@ -127,43 +120,22 @@ inline std::ostream& operator<<(std::ostream& os, const Exception& e) throw() { return os; } -}/* CVC4 namespace */ - -#if (defined(__BUILDING_CVC4LIB) || defined(__BUILDING_CVC4LIB_UNIT_TEST)) && !defined(__BUILDING_STATISTICS_FOR_EXPORT) -# include "base/cvc4_assert.h" -#endif /* (__BUILDING_CVC4LIB || __BUILDING_CVC4LIB_UNIT_TEST) && !__BUILDING_STATISTICS_FOR_EXPORT */ - -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, ...) { +template <class T> inline void CheckArgument(bool cond, const T& arg, + const char* tail) CVC4_PUBLIC; +template <class T> inline void CheckArgument(bool cond, const T& arg, + const char* tail) { if(__builtin_expect( ( !cond ), false )) { \ 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) + CVC4_PUBLIC; template <class T> inline void CheckArgument(bool cond, const T& arg) { if(__builtin_expect( ( !cond ), false )) { \ 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(__builtin_expect( ( !cond ), false )) { \ - 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(__builtin_expect( ( !cond ), false )) { \ - throw ::CVC4::IllegalArgumentException("", "", ""); \ - } \ -} -#endif /* DebugCheckArgument */ }/* CVC4 namespace */ diff --git a/src/bindings/java_stream_adapters.h b/src/bindings/java_stream_adapters.h index b4a311ad0..c198b95aa 100644 --- a/src/bindings/java_stream_adapters.h +++ b/src/bindings/java_stream_adapters.h @@ -33,7 +33,7 @@ #include <sstream> #include <set> #include <cassert> -#include <iostream> +#include <iosfwd> #include <string> #include <jni.h> diff --git a/src/compat/cvc3_compat.cpp b/src/compat/cvc3_compat.cpp index d44bae7ee..3fa790f3e 100644 --- a/src/compat/cvc3_compat.cpp +++ b/src/compat/cvc3_compat.cpp @@ -18,11 +18,12 @@ #include <algorithm> #include <cassert> -#include <iostream> +#include <iosfwd> #include <iterator> #include <sstream> #include <string> +#include "base/exception.h" #include "base/output.h" #include "expr/kind.h" #include "expr/predicate.h" @@ -43,6 +44,16 @@ using namespace std; +// Matches base/cvc4_assert.h's PrettyCheckArgument. +// base/cvc4_assert.h cannot be directly included. +#define CompatCheckArgument(cond, arg, msg...) \ + do { \ + if(__builtin_expect( ( ! (cond) ), false )) { \ + throw ::CVC4::IllegalArgumentException(#cond, #arg, __PRETTY_FUNCTION__, \ + ::CVC4::IllegalArgumentException::formatVariadic(msg).c_str()); \ + } \ + } while(0) + #define Unimplemented(str) throw Exception(str) namespace CVC3 { @@ -474,12 +485,12 @@ std::string Expr::getUid() const { } std::string Expr::getString() const { - CVC4::CheckArgument(getKind() == CVC4::kind::CONST_STRING, *this, "CVC3::Expr::getString(): not a string Expr: `%s'", toString().c_str()); + CompatCheckArgument(getKind() == CVC4::kind::CONST_STRING, *this, "CVC3::Expr::getString(): not a string Expr: `%s'", toString().c_str()); return getConst<CVC4::String>().toString(); } std::vector<Expr> Expr::getVars() const { - CVC4::CheckArgument(isClosure(), *this, "CVC3::Expr::getVars(): not a closure Expr: `%s'", toString().c_str()); + CompatCheckArgument(isClosure(), *this, "CVC3::Expr::getVars(): not a closure Expr: `%s'", toString().c_str()); const vector<CVC4::Expr>& kids = (*this)[0].getChildren(); vector<Expr> v; for(vector<CVC4::Expr>::const_iterator i = kids.begin(); i != kids.end(); ++i) { @@ -497,7 +508,7 @@ int Expr::getBoundIndex() const { } Expr Expr::getBody() const { - CVC4::CheckArgument(isClosure(), *this, "CVC3::Expr::getBody(): not a closure Expr: `%s'", toString().c_str()); + CompatCheckArgument(isClosure(), *this, "CVC3::Expr::getBody(): not a closure Expr: `%s'", toString().c_str()); return (*this)[1]; } @@ -546,7 +557,7 @@ bool Expr::isSkolem() const { } const Rational& Expr::getRational() const { - CVC4::CheckArgument(isRational(), *this, "CVC3::Expr::getRational(): not a rational Expr: `%s'", toString().c_str()); + CompatCheckArgument(isRational(), *this, "CVC3::Expr::getRational(): not a rational Expr: `%s'", toString().c_str()); return getConst<CVC4::Rational>(); } @@ -573,7 +584,8 @@ Expr Expr::getExpr() const { } std::vector< std::vector<Expr> > Expr::getTriggers() const { - CVC4::CheckArgument(isClosure(), *this, "getTriggers() called on non-closure expr"); + CompatCheckArgument(isClosure(), *this, + "getTriggers() called on non-closure expr"); if(getNumChildren() < 3) { // no triggers for this quantifier return vector< vector<Expr> >(); @@ -756,37 +768,37 @@ CLFlag& CLFlag::operator=(const CLFlag& f) { } CLFlag& CLFlag::operator=(bool b) { - CVC4::CheckArgument(d_tp == CLFLAG_BOOL, this); + CompatCheckArgument(d_tp == CLFLAG_BOOL, this); d_data.b = b; return *this; } CLFlag& CLFlag::operator=(int i) { - CVC4::CheckArgument(d_tp == CLFLAG_INT, this); + CompatCheckArgument(d_tp == CLFLAG_INT, this); d_data.i = i; return *this; } CLFlag& CLFlag::operator=(const std::string& s) { - CVC4::CheckArgument(d_tp == CLFLAG_STRING, this); + CompatCheckArgument(d_tp == CLFLAG_STRING, this); *d_data.s = s; return *this; } CLFlag& CLFlag::operator=(const char* s) { - CVC4::CheckArgument(d_tp == CLFLAG_STRING, this); + CompatCheckArgument(d_tp == CLFLAG_STRING, this); *d_data.s = s; return *this; } CLFlag& CLFlag::operator=(const std::pair<string, bool>& p) { - CVC4::CheckArgument(d_tp == CLFLAG_STRVEC, this); + CompatCheckArgument(d_tp == CLFLAG_STRVEC, this); d_data.sv->push_back(p); return *this; } CLFlag& CLFlag::operator=(const std::vector<std::pair<string, bool> >& sv) { - CVC4::CheckArgument(d_tp == CLFLAG_STRVEC, this); + CompatCheckArgument(d_tp == CLFLAG_STRVEC, this); *d_data.sv = sv; return *this; } @@ -804,22 +816,22 @@ bool CLFlag::display() const { } const bool& CLFlag::getBool() const { - CVC4::CheckArgument(d_tp == CLFLAG_BOOL, this); + CompatCheckArgument(d_tp == CLFLAG_BOOL, this); return d_data.b; } const int& CLFlag::getInt() const { - CVC4::CheckArgument(d_tp == CLFLAG_INT, this); + CompatCheckArgument(d_tp == CLFLAG_INT, this); return d_data.i; } const std::string& CLFlag::getString() const { - CVC4::CheckArgument(d_tp == CLFLAG_STRING, this); + CompatCheckArgument(d_tp == CLFLAG_STRING, this); return *d_data.s; } const std::vector<std::pair<string, bool> >& CLFlag::getStrVec() const { - CVC4::CheckArgument(d_tp == CLFLAG_STRVEC, this); + CompatCheckArgument(d_tp == CLFLAG_STRVEC, this); return *d_data.sv; } @@ -842,7 +854,7 @@ size_t CLFlags::countFlags(const std::string& name, const CLFlag& CLFlags::getFlag(const std::string& name) const { FlagMap::const_iterator i = d_map.find(name); - CVC4::CheckArgument(i != d_map.end(), name, "No command-line flag by that name, or not supported."); + CompatCheckArgument(i != d_map.end(), name, "No command-line flag by that name, or not supported."); return (*i).second; } @@ -852,8 +864,8 @@ const CLFlag& CLFlags::operator[](const std::string& name) const { void CLFlags::setFlag(const std::string& name, const CLFlag& f) { FlagMap::iterator i = d_map.find(name); - CVC4::CheckArgument(i != d_map.end(), name, "No command-line flag by that name, or not supported."); - CVC4::CheckArgument((*i).second.getType() == f.getType(), f, + CompatCheckArgument(i != d_map.end(), name, "No command-line flag by that name, or not supported."); + CompatCheckArgument((*i).second.getType() == f.getType(), f, "Command-line flag `%s' has type %s, but caller tried to set to a %s.", name.c_str(), toString((*i).second.getType()).c_str(), @@ -863,38 +875,38 @@ void CLFlags::setFlag(const std::string& name, const CLFlag& f) { void CLFlags::setFlag(const std::string& name, bool b) { FlagMap::iterator i = d_map.find(name); - CVC4::CheckArgument(i != d_map.end(), name, "No command-line flag by that name, or not supported."); + CompatCheckArgument(i != d_map.end(), name, "No command-line flag by that name, or not supported."); (*i).second = b; } void CLFlags::setFlag(const std::string& name, int i) { FlagMap::iterator it = d_map.find(name); - CVC4::CheckArgument(it != d_map.end(), name, "No command-line flag by that name, or not supported."); + CompatCheckArgument(it != d_map.end(), name, "No command-line flag by that name, or not supported."); (*it).second = i; } void CLFlags::setFlag(const std::string& name, const std::string& s) { FlagMap::iterator i = d_map.find(name); - CVC4::CheckArgument(i != d_map.end(), name, "No command-line flag by that name, or not supported."); + CompatCheckArgument(i != d_map.end(), name, "No command-line flag by that name, or not supported."); (*i).second = s; } void CLFlags::setFlag(const std::string& name, const char* s) { FlagMap::iterator i = d_map.find(name); - CVC4::CheckArgument(i != d_map.end(), name, "No command-line flag by that name, or not supported."); + CompatCheckArgument(i != d_map.end(), name, "No command-line flag by that name, or not supported."); (*i).second = s; } void CLFlags::setFlag(const std::string& name, const std::pair<string, bool>& p) { FlagMap::iterator i = d_map.find(name); - CVC4::CheckArgument(i != d_map.end(), name, "No command-line flag by that name, or not supported."); + CompatCheckArgument(i != d_map.end(), name, "No command-line flag by that name, or not supported."); (*i).second = p; } void CLFlags::setFlag(const std::string& name, const std::vector<std::pair<string, bool> >& sv) { FlagMap::iterator i = d_map.find(name); - CVC4::CheckArgument(i != d_map.end(), name, "No command-line flag by that name, or not supported."); + CompatCheckArgument(i != d_map.end(), name, "No command-line flag by that name, or not supported."); (*i).second = sv; } @@ -1233,8 +1245,8 @@ Type ValidityChecker::intType() { Type ValidityChecker::subrangeType(const Expr& l, const Expr& r) { bool noLowerBound = l.getType().isString() && l.getConst<CVC4::String>() == "_NEGINF"; bool noUpperBound = r.getType().isString() && r.getConst<CVC4::String>() == "_POSINF"; - CVC4::CheckArgument(noLowerBound || (l.getKind() == CVC4::kind::CONST_RATIONAL && l.getConst<Rational>().isIntegral()), l); - CVC4::CheckArgument(noUpperBound || (r.getKind() == CVC4::kind::CONST_RATIONAL && r.getConst<Rational>().isIntegral()), r); + CompatCheckArgument(noLowerBound || (l.getKind() == CVC4::kind::CONST_RATIONAL && l.getConst<Rational>().isIntegral()), l); + CompatCheckArgument(noUpperBound || (r.getKind() == CVC4::kind::CONST_RATIONAL && r.getConst<Rational>().isIntegral()), r); CVC4::SubrangeBound bl = noLowerBound ? CVC4::SubrangeBound() : CVC4::SubrangeBound(l.getConst<Rational>().getNumerator()); CVC4::SubrangeBound br = noUpperBound ? CVC4::SubrangeBound() : CVC4::SubrangeBound(r.getConst<Rational>().getNumerator()); return d_em->mkSubrangeType(CVC4::SubrangeBounds(bl, br)); @@ -1298,7 +1310,7 @@ Type ValidityChecker::recordType(const std::string& field0, const Type& type0, Type ValidityChecker::recordType(const std::vector<std::string>& fields, const std::vector<Type>& types) { - CVC4::CheckArgument(fields.size() == types.size() && fields.size() > 0, + CompatCheckArgument(fields.size() == types.size() && fields.size() > 0, "invalid vector length(s) in recordType()"); std::vector< std::pair<std::string, CVC4::Type> > fieldSpecs; for(unsigned i = 0; i < fields.size(); ++i) { @@ -1311,7 +1323,9 @@ Type ValidityChecker::dataType(const std::string& name, const std::string& constructor, const std::vector<std::string>& selectors, const std::vector<Expr>& types) { - CVC4::CheckArgument(selectors.size() == types.size(), types, "expected selectors and types vectors to be of equal length"); + CompatCheckArgument(selectors.size() == types.size(), types, + "expected selectors and types vectors to be of equal" + "length"); vector<string> cv; vector< vector<string> > sv; vector< vector<Expr> > tv; @@ -1325,8 +1339,12 @@ Type ValidityChecker::dataType(const std::string& name, const std::vector<std::string>& constructors, const std::vector<std::vector<std::string> >& selectors, const std::vector<std::vector<Expr> >& types) { - CVC4::CheckArgument(constructors.size() == selectors.size(), selectors, "expected constructors and selectors vectors to be of equal length"); - CVC4::CheckArgument(constructors.size() == types.size(), types, "expected constructors and types vectors to be of equal length"); + CompatCheckArgument(constructors.size() == selectors.size(), selectors, + "Expected constructors and selectors vectors to be of " + "equal length."); + CompatCheckArgument(constructors.size() == types.size(), types, + "Expected constructors and types vectors to be of equal " + "length."); vector<string> nv; vector< vector<string> > cv; vector< vector< vector<string> > > sv; @@ -1347,22 +1365,36 @@ void ValidityChecker::dataType(const std::vector<std::string>& names, const std::vector<std::vector<std::vector<Expr> > >& types, std::vector<Type>& returnTypes) { - CVC4::CheckArgument(names.size() == constructors.size(), constructors, "expected names and constructors vectors to be of equal length"); - CVC4::CheckArgument(names.size() == selectors.size(), selectors, "expected names and selectors vectors to be of equal length"); - CVC4::CheckArgument(names.size() == types.size(), types, "expected names and types vectors to be of equal length"); + CompatCheckArgument(names.size() == constructors.size(), constructors, + "Expected names and constructors vectors to be of equal " + "length."); + CompatCheckArgument(names.size() == selectors.size(), selectors, + "Expected names and selectors vectors to be of equal " + "length."); + CompatCheckArgument(names.size() == types.size(), types, + "Expected names and types vectors to be of equal " + "length."); vector<CVC4::Datatype> dv; // Set up the datatype specifications. for(unsigned i = 0; i < names.size(); ++i) { CVC4::Datatype dt(names[i], false); - CVC4::CheckArgument(constructors[i].size() == selectors[i].size(), "expected sub-vectors in constructors and selectors vectors to match in size"); - CVC4::CheckArgument(constructors[i].size() == types[i].size(), "expected sub-vectors in constructors and types vectors to match in size"); + CompatCheckArgument(constructors[i].size() == selectors[i].size(), + "Expected sub-vectors in constructors and selectors " + "vectors to match in size."); + CompatCheckArgument(constructors[i].size() == types[i].size(), + "Expected sub-vectors in constructors and types " + "vectors to match in size."); for(unsigned j = 0; j < constructors[i].size(); ++j) { CVC4::DatatypeConstructor ctor(constructors[i][j]); - CVC4::CheckArgument(selectors[i][j].size() == types[i][j].size(), types, "expected sub-vectors in selectors and types vectors to match in size"); + CompatCheckArgument(selectors[i][j].size() == types[i][j].size(), types, + "Expected sub-vectors in selectors and types vectors " + "to match in size."); for(unsigned k = 0; k < selectors[i][j].size(); ++k) { if(types[i][j][k].getType().isString()) { - ctor.addArg(selectors[i][j][k], CVC4::DatatypeUnresolvedType(types[i][j][k].getConst<CVC4::String>().toString())); + CVC4::DatatypeUnresolvedType unresolvedName = + types[i][j][k].getConst<CVC4::String>().toString(); + ctor.addArg(selectors[i][j][k], unresolvedName); } else { ctor.addArg(selectors[i][j][k], exprToType(types[i][j][k])); } @@ -1388,10 +1420,17 @@ void ValidityChecker::dataType(const std::vector<std::string>& names, } for(CVC4::Datatype::const_iterator j = dt.begin(); j != dt.end(); ++j) { // For each constructor, register its name and its selectors names. - CVC4::CheckArgument(d_constructors.find((*j).getName()) == d_constructors.end(), constructors, "cannot have two constructors with the same name in a ValidityChecker"); + CompatCheckArgument( + d_constructors.find((*j).getName()) == d_constructors.end(), + constructors, + "Cannot have two constructors with the same name in a " + "ValidityChecker."); d_constructors[(*j).getName()] = &dt; for(CVC4::DatatypeConstructor::const_iterator k = (*j).begin(); k != (*j).end(); ++k) { - CVC4::CheckArgument(d_selectors.find((*k).getName()) == d_selectors.end(), selectors, "cannot have two selectors with the same name in a ValidityChecker"); + CompatCheckArgument( + d_selectors.find((*k).getName()) == d_selectors.end(), selectors, + "Cannot have two selectors with the same name in a " + "ValidityChecker."); d_selectors[(*k).getName()] = make_pair(&dt, (*j).getName()); } } @@ -1407,7 +1446,8 @@ Type ValidityChecker::arrayType(const Type& typeIndex, const Type& typeData) { } Type ValidityChecker::bitvecType(int n) { - CVC4::CheckArgument(n >= 0, n, "cannot construct a bitvector type of negative size"); + CompatCheckArgument(n >= 0, n, + "Cannot construct a bitvector type of negative size."); return d_em->mkBitVectorType(n); } @@ -1444,7 +1484,7 @@ Expr ValidityChecker::varExpr(const std::string& name, const Type& type) { Expr ValidityChecker::varExpr(const std::string& name, const Type& type, const Expr& def) { - CVC4::CheckArgument(def.getType() == type, def, "expected types to match"); + CompatCheckArgument(def.getType() == type, def, "expected types to match"); d_parserContext->defineVar(name, def); return def; } @@ -1595,7 +1635,7 @@ Expr ValidityChecker::andExpr(const Expr& left, const Expr& right) { Expr ValidityChecker::andExpr(const std::vector<Expr>& children) { // AND must have at least 2 children - CVC4::CheckArgument(children.size() > 0, children); + CompatCheckArgument(children.size() > 0, children); return (children.size() == 1) ? children[0] : Expr(d_em->mkExpr(CVC4::kind::AND, *reinterpret_cast<const vector<CVC4::Expr>*>(&children))); } @@ -1605,7 +1645,7 @@ Expr ValidityChecker::orExpr(const Expr& left, const Expr& right) { Expr ValidityChecker::orExpr(const std::vector<Expr>& children) { // OR must have at least 2 children - CVC4::CheckArgument(children.size() > 0, children); + CompatCheckArgument(children.size() > 0, children); return (children.size() == 1) ? children[0] : Expr(d_em->mkExpr(CVC4::kind::OR, *reinterpret_cast<const vector<CVC4::Expr>*>(&children))); } @@ -1627,7 +1667,7 @@ Expr ValidityChecker::iteExpr(const Expr& ifpart, const Expr& thenpart, } Expr ValidityChecker::distinctExpr(const std::vector<Expr>& children) { - CVC4::CheckArgument(children.size() > 1, children, "it makes no sense to create a `distinct' expression with only one child"); + CompatCheckArgument(children.size() > 1, children, "it makes no sense to create a `distinct' expression with only one child"); const vector<CVC4::Expr>& v = *reinterpret_cast<const vector<CVC4::Expr>*>(&children); return d_em->mkExpr(CVC4::kind::DISTINCT, v); @@ -1639,7 +1679,7 @@ Op ValidityChecker::createOp(const std::string& name, const Type& type) { Op ValidityChecker::createOp(const std::string& name, const Type& type, const Expr& def) { - CVC4::CheckArgument(def.getType() == type, type, + CompatCheckArgument(def.getType() == type, type, "Type mismatch in ValidityChecker::createOp(): `%s' defined to an " "expression of type %s but ascribed as type %s", name.c_str(), def.getType().toString().c_str(), type.toString().c_str()); @@ -1689,7 +1729,7 @@ Expr ValidityChecker::ratExpr(const std::string& n, int base) { if(n.find(".") == string::npos) { return d_em->mkConst(Rational(n, base)); } else { - CVC4::CheckArgument(base == 10, base, "unsupported base for decimal parsing"); + CompatCheckArgument(base == 10, base, "unsupported base for decimal parsing"); return d_em->mkConst(Rational::fromDecimal(n)); } } @@ -1704,7 +1744,7 @@ Expr ValidityChecker::plusExpr(const Expr& left, const Expr& right) { Expr ValidityChecker::plusExpr(const std::vector<Expr>& children) { // PLUS must have at least 2 children - CVC4::CheckArgument(children.size() > 0, children); + CompatCheckArgument(children.size() > 0, children); return (children.size() == 1) ? children[0] : Expr(d_em->mkExpr(CVC4::kind::PLUS, *reinterpret_cast<const vector<CVC4::Expr>*>(&children))); } @@ -1806,10 +1846,11 @@ Expr ValidityChecker::newBVConstExpr(const std::vector<bool>& bits) { Expr ValidityChecker::newBVConstExpr(const Rational& r, int len) { // implementation based on CVC3's TheoryBitvector::newBVConstExpr() - CVC4::CheckArgument(r.getDenominator() == 1, r, "ValidityChecker::newBVConstExpr: " - "not an integer: `%s'", r.toString().c_str()); - CVC4::CheckArgument(len > 0, len, "ValidityChecker::newBVConstExpr: " - "len = %d", len); + CompatCheckArgument(r.getDenominator() == 1, r, + "ValidityChecker::newBVConstExpr: " + "not an integer: `%s'", r.toString().c_str()); + CompatCheckArgument(len > 0, len, "ValidityChecker::newBVConstExpr: " + "len = %d", len); string s(r.toString(2)); size_t strsize = s.size(); @@ -1831,8 +1872,8 @@ Expr ValidityChecker::newBVConstExpr(const Rational& r, int len) { } Expr ValidityChecker::newConcatExpr(const Expr& t1, const Expr& t2) { - CVC4::CheckArgument(t1.getType().isBitVector(), t1, "can only concat a bitvector, not a `%s'", t1.getType().toString().c_str()); - CVC4::CheckArgument(t2.getType().isBitVector(), t2, "can only concat a bitvector, not a `%s'", t2.getType().toString().c_str()); + CompatCheckArgument(t1.getType().isBitVector(), t1, "can only concat a bitvector, not a `%s'", t1.getType().toString().c_str()); + CompatCheckArgument(t2.getType().isBitVector(), t2, "can only concat a bitvector, not a `%s'", t2.getType().toString().c_str()); return d_em->mkExpr(CVC4::kind::BITVECTOR_CONCAT, t1, t2); } @@ -1843,29 +1884,43 @@ Expr ValidityChecker::newConcatExpr(const std::vector<Expr>& kids) { } Expr ValidityChecker::newBVExtractExpr(const Expr& e, int hi, int low) { - CVC4::CheckArgument(e.getType().isBitVector(), e, "can only bvextract from a bitvector, not a `%s'", e.getType().toString().c_str()); - CVC4::CheckArgument(hi >= low, hi, "extraction [%d:%d] is bad; possibly inverted?", hi, low); - CVC4::CheckArgument(low >= 0, low, "extraction [%d:%d] is bad (negative)", hi, low); - CVC4::CheckArgument(CVC4::BitVectorType(e.getType()).getSize() > unsigned(hi), hi, "bitvector is of size %u, extraction [%d:%d] is off-the-end", CVC4::BitVectorType(e.getType()).getSize(), hi, low); + CompatCheckArgument(e.getType().isBitVector(), e, + "can only bvextract from a bitvector, not a `%s'", + e.getType().toString().c_str()); + CompatCheckArgument(hi >= low, hi, + "extraction [%d:%d] is bad; possibly inverted?", hi, low); + CompatCheckArgument(low >= 0, low, + "extraction [%d:%d] is bad (negative)", hi, low); + CompatCheckArgument(CVC4::BitVectorType(e.getType()).getSize() > unsigned(hi), + hi, + "bitvector is of size %u, extraction [%d:%d] is off-the-end", + CVC4::BitVectorType(e.getType()).getSize(), hi, low); return d_em->mkExpr(CVC4::kind::BITVECTOR_EXTRACT, - d_em->mkConst(CVC4::BitVectorExtract(hi, low)), e); + d_em->mkConst(CVC4::BitVectorExtract(hi, low)), e); } Expr ValidityChecker::newBVNegExpr(const Expr& t1) { // CVC3's BVNEG => SMT-LIBv2 bvnot - CVC4::CheckArgument(t1.getType().isBitVector(), t1, "can only bvneg a bitvector, not a `%s'", t1.getType().toString().c_str()); + CompatCheckArgument(t1.getType().isBitVector(), t1, + "can only bvneg a bitvector, not a `%s'", + t1.getType().toString().c_str()); return d_em->mkExpr(CVC4::kind::BITVECTOR_NOT, t1); } Expr ValidityChecker::newBVAndExpr(const Expr& t1, const Expr& t2) { - CVC4::CheckArgument(t1.getType().isBitVector(), t1, "can only bvand a bitvector, not a `%s'", t1.getType().toString().c_str()); - CVC4::CheckArgument(t2.getType().isBitVector(), t2, "can only bvand a bitvector, not a `%s'", t2.getType().toString().c_str()); + CompatCheckArgument(t1.getType().isBitVector(), t1, + "can only bvand a bitvector, not a `%s'", + t1.getType().toString().c_str()); + CompatCheckArgument(t2.getType().isBitVector(), t2, + "can only bvand a bitvector, not a `%s'", + t2.getType().toString().c_str()); return d_em->mkExpr(CVC4::kind::BITVECTOR_AND, t1, t2); } Expr ValidityChecker::newBVAndExpr(const std::vector<Expr>& kids) { // BITVECTOR_AND is not N-ary in CVC4 - CVC4::CheckArgument(kids.size() > 1, kids, "BITVECTOR_AND must have at least 2 children"); + CompatCheckArgument(kids.size() > 1, kids, + "BITVECTOR_AND must have at least 2 children"); std::vector<Expr>::const_reverse_iterator i = kids.rbegin(); Expr e = *i++; while(i != kids.rend()) { @@ -1875,14 +1930,19 @@ Expr ValidityChecker::newBVAndExpr(const std::vector<Expr>& kids) { } Expr ValidityChecker::newBVOrExpr(const Expr& t1, const Expr& t2) { - CVC4::CheckArgument(t1.getType().isBitVector(), t1, "can only bvor a bitvector, not a `%s'", t1.getType().toString().c_str()); - CVC4::CheckArgument(t2.getType().isBitVector(), t2, "can only bvor a bitvector, not a `%s'", t2.getType().toString().c_str()); + CompatCheckArgument(t1.getType().isBitVector(), t1, + "can only bvor a bitvector, not a `%s'", + t1.getType().toString().c_str()); + CompatCheckArgument(t2.getType().isBitVector(), t2, + "can only bvor a bitvector, not a `%s'", + t2.getType().toString().c_str()); return d_em->mkExpr(CVC4::kind::BITVECTOR_OR, t1, t2); } Expr ValidityChecker::newBVOrExpr(const std::vector<Expr>& kids) { // BITVECTOR_OR is not N-ary in CVC4 - CVC4::CheckArgument(kids.size() > 1, kids, "BITVECTOR_OR must have at least 2 children"); + CompatCheckArgument(kids.size() > 1, kids, + "BITVECTOR_OR must have at least 2 children"); std::vector<Expr>::const_reverse_iterator i = kids.rbegin(); Expr e = *i++; while(i != kids.rend()) { @@ -1892,14 +1952,19 @@ Expr ValidityChecker::newBVOrExpr(const std::vector<Expr>& kids) { } Expr ValidityChecker::newBVXorExpr(const Expr& t1, const Expr& t2) { - CVC4::CheckArgument(t1.getType().isBitVector(), t1, "can only bvxor a bitvector, not a `%s'", t1.getType().toString().c_str()); - CVC4::CheckArgument(t2.getType().isBitVector(), t2, "can only bvxor a bitvector, not a `%s'", t2.getType().toString().c_str()); + CompatCheckArgument(t1.getType().isBitVector(), t1, + "can only bvxor a bitvector, not a `%s'", + t1.getType().toString().c_str()); + CompatCheckArgument(t2.getType().isBitVector(), t2, + "can only bvxor a bitvector, not a `%s'", + t2.getType().toString().c_str()); return d_em->mkExpr(CVC4::kind::BITVECTOR_XOR, t1, t2); } Expr ValidityChecker::newBVXorExpr(const std::vector<Expr>& kids) { // BITVECTOR_XOR is not N-ary in CVC4 - CVC4::CheckArgument(kids.size() > 1, kids, "BITVECTOR_XOR must have at least 2 children"); + CompatCheckArgument(kids.size() > 1, kids, + "BITVECTOR_XOR must have at least 2 children"); std::vector<Expr>::const_reverse_iterator i = kids.rbegin(); Expr e = *i++; while(i != kids.rend()) { @@ -1909,14 +1974,19 @@ Expr ValidityChecker::newBVXorExpr(const std::vector<Expr>& kids) { } Expr ValidityChecker::newBVXnorExpr(const Expr& t1, const Expr& t2) { - CVC4::CheckArgument(t1.getType().isBitVector(), t1, "can only bvxnor a bitvector, not a `%s'", t1.getType().toString().c_str()); - CVC4::CheckArgument(t2.getType().isBitVector(), t2, "can only bvxnor a bitvector, not a `%s'", t2.getType().toString().c_str()); + CompatCheckArgument(t1.getType().isBitVector(), t1, + "can only bvxnor a bitvector, not a `%s'", + t1.getType().toString().c_str()); + CompatCheckArgument(t2.getType().isBitVector(), t2, + "can only bvxnor a bitvector, not a `%s'", + t2.getType().toString().c_str()); return d_em->mkExpr(CVC4::kind::BITVECTOR_XNOR, t1, t2); } Expr ValidityChecker::newBVXnorExpr(const std::vector<Expr>& kids) { // BITVECTOR_XNOR is not N-ary in CVC4 - CVC4::CheckArgument(kids.size() > 1, kids, "BITVECTOR_XNOR must have at least 2 children"); + CompatCheckArgument(kids.size() > 1, kids, + "BITVECTOR_XNOR must have at least 2 children"); std::vector<Expr>::const_reverse_iterator i = kids.rbegin(); Expr e = *i++; while(i != kids.rend()) { @@ -1926,73 +1996,81 @@ Expr ValidityChecker::newBVXnorExpr(const std::vector<Expr>& kids) { } Expr ValidityChecker::newBVNandExpr(const Expr& t1, const Expr& t2) { - CVC4::CheckArgument(t1.getType().isBitVector(), t1, "can only bvnand a bitvector, not a `%s'", t1.getType().toString().c_str()); - CVC4::CheckArgument(t2.getType().isBitVector(), t2, "can only bvnand a bitvector, not a `%s'", t2.getType().toString().c_str()); + CompatCheckArgument(t1.getType().isBitVector(), t1, + "can only bvnand a bitvector, not a `%s'", + t1.getType().toString().c_str()); + CompatCheckArgument(t2.getType().isBitVector(), t2, + "can only bvnand a bitvector, not a `%s'", + t2.getType().toString().c_str()); return d_em->mkExpr(CVC4::kind::BITVECTOR_NAND, t1, t2); } Expr ValidityChecker::newBVNorExpr(const Expr& t1, const Expr& t2) { - CVC4::CheckArgument(t1.getType().isBitVector(), t1, "can only bvnor a bitvector, not a `%s'", t1.getType().toString().c_str()); - CVC4::CheckArgument(t2.getType().isBitVector(), t2, "can only bvnor a bitvector, not a `%s'", t2.getType().toString().c_str()); + CompatCheckArgument(t1.getType().isBitVector(), t1, + "can only bvnor a bitvector, not a `%s'", + t1.getType().toString().c_str()); + CompatCheckArgument(t2.getType().isBitVector(), t2, + "can only bvnor a bitvector, not a `%s'", + t2.getType().toString().c_str()); return d_em->mkExpr(CVC4::kind::BITVECTOR_NOR, t1, t2); } Expr ValidityChecker::newBVCompExpr(const Expr& t1, const Expr& t2) { - CVC4::CheckArgument(t1.getType().isBitVector(), t1, "can only bvcomp a bitvector, not a `%s'", t1.getType().toString().c_str()); - CVC4::CheckArgument(t2.getType().isBitVector(), t2, "can only bvcomp a bitvector, not a `%s'", t2.getType().toString().c_str()); + CompatCheckArgument(t1.getType().isBitVector(), t1, "can only bvcomp a bitvector, not a `%s'", t1.getType().toString().c_str()); + CompatCheckArgument(t2.getType().isBitVector(), t2, "can only bvcomp a bitvector, not a `%s'", t2.getType().toString().c_str()); return d_em->mkExpr(CVC4::kind::BITVECTOR_COMP, t1, t2); } Expr ValidityChecker::newBVLTExpr(const Expr& t1, const Expr& t2) { - CVC4::CheckArgument(t1.getType().isBitVector(), t1, "can only bvlt a bitvector, not a `%s'", t1.getType().toString().c_str()); - CVC4::CheckArgument(t2.getType().isBitVector(), t2, "can only bvlt a bitvector, not a `%s'", t2.getType().toString().c_str()); + CompatCheckArgument(t1.getType().isBitVector(), t1, "can only bvlt a bitvector, not a `%s'", t1.getType().toString().c_str()); + CompatCheckArgument(t2.getType().isBitVector(), t2, "can only bvlt a bitvector, not a `%s'", t2.getType().toString().c_str()); return d_em->mkExpr(CVC4::kind::BITVECTOR_ULT, t1, t2); } Expr ValidityChecker::newBVLEExpr(const Expr& t1, const Expr& t2) { - CVC4::CheckArgument(t1.getType().isBitVector(), t1, "can only bvle a bitvector, not a `%s'", t1.getType().toString().c_str()); - CVC4::CheckArgument(t2.getType().isBitVector(), t2, "can only bvle a bitvector, not a `%s'", t2.getType().toString().c_str()); + CompatCheckArgument(t1.getType().isBitVector(), t1, "can only bvle a bitvector, not a `%s'", t1.getType().toString().c_str()); + CompatCheckArgument(t2.getType().isBitVector(), t2, "can only bvle a bitvector, not a `%s'", t2.getType().toString().c_str()); return d_em->mkExpr(CVC4::kind::BITVECTOR_ULE, t1, t2); } Expr ValidityChecker::newBVSLTExpr(const Expr& t1, const Expr& t2) { - CVC4::CheckArgument(t1.getType().isBitVector(), t1, "can only bvslt a bitvector, not a `%s'", t1.getType().toString().c_str()); - CVC4::CheckArgument(t2.getType().isBitVector(), t2, "can only bvslt a bitvector, not a `%s'", t2.getType().toString().c_str()); + CompatCheckArgument(t1.getType().isBitVector(), t1, "can only bvslt a bitvector, not a `%s'", t1.getType().toString().c_str()); + CompatCheckArgument(t2.getType().isBitVector(), t2, "can only bvslt a bitvector, not a `%s'", t2.getType().toString().c_str()); return d_em->mkExpr(CVC4::kind::BITVECTOR_SLT, t1, t2); } Expr ValidityChecker::newBVSLEExpr(const Expr& t1, const Expr& t2) { - CVC4::CheckArgument(t1.getType().isBitVector(), t1, "can only bvsle a bitvector, not a `%s'", t1.getType().toString().c_str()); - CVC4::CheckArgument(t2.getType().isBitVector(), t2, "can only bvsle a bitvector, not a `%s'", t2.getType().toString().c_str()); + CompatCheckArgument(t1.getType().isBitVector(), t1, "can only bvsle a bitvector, not a `%s'", t1.getType().toString().c_str()); + CompatCheckArgument(t2.getType().isBitVector(), t2, "can only bvsle a bitvector, not a `%s'", t2.getType().toString().c_str()); return d_em->mkExpr(CVC4::kind::BITVECTOR_SLE, t1, t2); } Expr ValidityChecker::newSXExpr(const Expr& t1, int len) { - CVC4::CheckArgument(t1.getType().isBitVector(), t1, "can only sx a bitvector, not a `%s'", t1.getType().toString().c_str()); - CVC4::CheckArgument(len >= 0, len, "must sx by a positive integer"); - CVC4::CheckArgument(unsigned(len) >= CVC4::BitVectorType(t1.getType()).getSize(), len, "cannot sx by something smaller than the bitvector (%d < %u)", len, CVC4::BitVectorType(t1.getType()).getSize()); + CompatCheckArgument(t1.getType().isBitVector(), t1, "can only sx a bitvector, not a `%s'", t1.getType().toString().c_str()); + CompatCheckArgument(len >= 0, len, "must sx by a positive integer"); + CompatCheckArgument(unsigned(len) >= CVC4::BitVectorType(t1.getType()).getSize(), len, "cannot sx by something smaller than the bitvector (%d < %u)", len, CVC4::BitVectorType(t1.getType()).getSize()); return d_em->mkExpr(CVC4::kind::BITVECTOR_SIGN_EXTEND, d_em->mkConst(CVC4::BitVectorSignExtend(len)), t1); } Expr ValidityChecker::newBVUminusExpr(const Expr& t1) { // CVC3's BVUMINUS => SMT-LIBv2 bvneg - CVC4::CheckArgument(t1.getType().isBitVector(), t1, "can only bvuminus a bitvector, not a `%s'", t1.getType().toString().c_str()); + CompatCheckArgument(t1.getType().isBitVector(), t1, "can only bvuminus a bitvector, not a `%s'", t1.getType().toString().c_str()); return d_em->mkExpr(CVC4::kind::BITVECTOR_NEG, t1); } Expr ValidityChecker::newBVSubExpr(const Expr& t1, const Expr& t2) { - CVC4::CheckArgument(t1.getType().isBitVector(), t1, "can only bvsub a bitvector, not a `%s'", t1.getType().toString().c_str()); - CVC4::CheckArgument(t2.getType().isBitVector(), t2, "can only bvsub by a bitvector, not a `%s'", t2.getType().toString().c_str()); + CompatCheckArgument(t1.getType().isBitVector(), t1, "can only bvsub a bitvector, not a `%s'", t1.getType().toString().c_str()); + CompatCheckArgument(t2.getType().isBitVector(), t2, "can only bvsub by a bitvector, not a `%s'", t2.getType().toString().c_str()); return d_em->mkExpr(CVC4::kind::BITVECTOR_SUB, t1, t2); } // Copied from CVC3's bitvector theory: makes bitvector expression "e" // into "len" bits, by zero-padding, or extracting least-significant bits. Expr ValidityChecker::bvpad(int len, const Expr& e) { - CVC4::CheckArgument(len >= 0, len, + CompatCheckArgument(len >= 0, len, "padding length must be a non-negative integer, not %d", len); - CVC4::CheckArgument(e.getType().isBitVector(), e, + CompatCheckArgument(e.getType().isBitVector(), e, "input to bitvector operation must be a bitvector"); unsigned size = CVC4::BitVectorType(e.getType()).getSize(); @@ -2011,89 +2089,89 @@ Expr ValidityChecker::bvpad(int len, const Expr& e) { Expr ValidityChecker::newBVPlusExpr(int numbits, const std::vector<Expr>& kids) { // BITVECTOR_PLUS is not N-ary in CVC4 - CVC4::CheckArgument(kids.size() > 1, kids, "BITVECTOR_PLUS must have at least 2 children"); + CompatCheckArgument(kids.size() > 1, kids, "BITVECTOR_PLUS must have at least 2 children"); std::vector<Expr>::const_reverse_iterator i = kids.rbegin(); Expr e = *i++; while(i != kids.rend()) { e = d_em->mkExpr(CVC4::kind::BITVECTOR_PLUS, bvpad(numbits, *i++), e); } unsigned size = CVC4::BitVectorType(e.getType()).getSize(); - CVC4::CheckArgument(unsigned(numbits) == size, numbits, + CompatCheckArgument(unsigned(numbits) == size, numbits, "argument must match computed size of bitvector sum: " "passed size == %u, computed size == %u", numbits, size); return e; } Expr ValidityChecker::newBVPlusExpr(int numbits, const Expr& t1, const Expr& t2) { - CVC4::CheckArgument(t1.getType().isBitVector(), t1, "can only bvplus a bitvector, not a `%s'", t1.getType().toString().c_str()); - CVC4::CheckArgument(t2.getType().isBitVector(), t2, "can only bvplus a bitvector, not a `%s'", t2.getType().toString().c_str()); + CompatCheckArgument(t1.getType().isBitVector(), t1, "can only bvplus a bitvector, not a `%s'", t1.getType().toString().c_str()); + CompatCheckArgument(t2.getType().isBitVector(), t2, "can only bvplus a bitvector, not a `%s'", t2.getType().toString().c_str()); Expr e = d_em->mkExpr(CVC4::kind::BITVECTOR_PLUS, bvpad(numbits, t1), bvpad(numbits, t2)); unsigned size = CVC4::BitVectorType(e.getType()).getSize(); - CVC4::CheckArgument(unsigned(numbits) == size, numbits, + CompatCheckArgument(unsigned(numbits) == size, numbits, "argument must match computed size of bitvector sum: " "passed size == %u, computed size == %u", numbits, size); return e; } Expr ValidityChecker::newBVMultExpr(int numbits, const Expr& t1, const Expr& t2) { - CVC4::CheckArgument(t1.getType().isBitVector(), t1, "can only bvmult a bitvector, not a `%s'", t1.getType().toString().c_str()); - CVC4::CheckArgument(t2.getType().isBitVector(), t2, "can only bvmult by a bitvector, not a `%s'", t2.getType().toString().c_str()); + CompatCheckArgument(t1.getType().isBitVector(), t1, "can only bvmult a bitvector, not a `%s'", t1.getType().toString().c_str()); + CompatCheckArgument(t2.getType().isBitVector(), t2, "can only bvmult by a bitvector, not a `%s'", t2.getType().toString().c_str()); Expr e = d_em->mkExpr(CVC4::kind::BITVECTOR_MULT, bvpad(numbits, t1), bvpad(numbits, t2)); unsigned size = CVC4::BitVectorType(e.getType()).getSize(); - CVC4::CheckArgument(unsigned(numbits) == size, numbits, + CompatCheckArgument(unsigned(numbits) == size, numbits, "argument must match computed size of bitvector product: " "passed size == %u, computed size == %u", numbits, size); return e; } Expr ValidityChecker::newBVUDivExpr(const Expr& t1, const Expr& t2) { - CVC4::CheckArgument(t1.getType().isBitVector(), t1, "can only bvudiv a bitvector, not a `%s'", t1.getType().toString().c_str()); - CVC4::CheckArgument(t2.getType().isBitVector(), t2, "can only bvudiv by a bitvector, not a `%s'", t2.getType().toString().c_str()); + CompatCheckArgument(t1.getType().isBitVector(), t1, "can only bvudiv a bitvector, not a `%s'", t1.getType().toString().c_str()); + CompatCheckArgument(t2.getType().isBitVector(), t2, "can only bvudiv by a bitvector, not a `%s'", t2.getType().toString().c_str()); return d_em->mkExpr(CVC4::kind::BITVECTOR_UDIV, t1, t2); } Expr ValidityChecker::newBVURemExpr(const Expr& t1, const Expr& t2) { - CVC4::CheckArgument(t1.getType().isBitVector(), t1, "can only bvurem a bitvector, not a `%s'", t1.getType().toString().c_str()); - CVC4::CheckArgument(t2.getType().isBitVector(), t2, "can only bvurem by a bitvector, not a `%s'", t2.getType().toString().c_str()); + CompatCheckArgument(t1.getType().isBitVector(), t1, "can only bvurem a bitvector, not a `%s'", t1.getType().toString().c_str()); + CompatCheckArgument(t2.getType().isBitVector(), t2, "can only bvurem by a bitvector, not a `%s'", t2.getType().toString().c_str()); return d_em->mkExpr(CVC4::kind::BITVECTOR_UREM, t1, t2); } Expr ValidityChecker::newBVSDivExpr(const Expr& t1, const Expr& t2) { - CVC4::CheckArgument(t1.getType().isBitVector(), t1, "can only bvsdiv a bitvector, not a `%s'", t1.getType().toString().c_str()); - CVC4::CheckArgument(t2.getType().isBitVector(), t2, "can only bvsdiv by a bitvector, not a `%s'", t2.getType().toString().c_str()); + CompatCheckArgument(t1.getType().isBitVector(), t1, "can only bvsdiv a bitvector, not a `%s'", t1.getType().toString().c_str()); + CompatCheckArgument(t2.getType().isBitVector(), t2, "can only bvsdiv by a bitvector, not a `%s'", t2.getType().toString().c_str()); return d_em->mkExpr(CVC4::kind::BITVECTOR_SDIV, t1, t2); } Expr ValidityChecker::newBVSRemExpr(const Expr& t1, const Expr& t2) { - CVC4::CheckArgument(t1.getType().isBitVector(), t1, "can only bvsrem a bitvector, not a `%s'", t1.getType().toString().c_str()); - CVC4::CheckArgument(t2.getType().isBitVector(), t2, "can only bvsrem by a bitvector, not a `%s'", t2.getType().toString().c_str()); + CompatCheckArgument(t1.getType().isBitVector(), t1, "can only bvsrem a bitvector, not a `%s'", t1.getType().toString().c_str()); + CompatCheckArgument(t2.getType().isBitVector(), t2, "can only bvsrem by a bitvector, not a `%s'", t2.getType().toString().c_str()); return d_em->mkExpr(CVC4::kind::BITVECTOR_SREM, t1, t2); } Expr ValidityChecker::newBVSModExpr(const Expr& t1, const Expr& t2) { - CVC4::CheckArgument(t1.getType().isBitVector(), t1, "can only bvsmod a bitvector, not a `%s'", t1.getType().toString().c_str()); - CVC4::CheckArgument(t2.getType().isBitVector(), t2, "can only bvsmod by a bitvector, not a `%s'", t2.getType().toString().c_str()); + CompatCheckArgument(t1.getType().isBitVector(), t1, "can only bvsmod a bitvector, not a `%s'", t1.getType().toString().c_str()); + CompatCheckArgument(t2.getType().isBitVector(), t2, "can only bvsmod by a bitvector, not a `%s'", t2.getType().toString().c_str()); return d_em->mkExpr(CVC4::kind::BITVECTOR_SMOD, t1, t2); } Expr ValidityChecker::newFixedLeftShiftExpr(const Expr& t1, int r) { - CVC4::CheckArgument(t1.getType().isBitVector(), t1, "can only left-shift a bitvector, not a `%s'", t1.getType().toString().c_str()); - CVC4::CheckArgument(r >= 0, r, "left shift amount must be >= 0 (you passed %d)", r); + CompatCheckArgument(t1.getType().isBitVector(), t1, "can only left-shift a bitvector, not a `%s'", t1.getType().toString().c_str()); + CompatCheckArgument(r >= 0, r, "left shift amount must be >= 0 (you passed %d)", r); // Defined in: // http://www.cs.nyu.edu/acsys/cvc3/doc/user_doc.html#user_doc_pres_lang_expr_bit return d_em->mkExpr(CVC4::kind::BITVECTOR_CONCAT, t1, d_em->mkConst(CVC4::BitVector(r))); } Expr ValidityChecker::newFixedConstWidthLeftShiftExpr(const Expr& t1, int r) { - CVC4::CheckArgument(t1.getType().isBitVector(), t1, "can only right-shift a bitvector, not a `%s'", t1.getType().toString().c_str()); - CVC4::CheckArgument(r >= 0, r, "const-width left shift amount must be >= 0 (you passed %d)", r); + CompatCheckArgument(t1.getType().isBitVector(), t1, "can only right-shift a bitvector, not a `%s'", t1.getType().toString().c_str()); + CompatCheckArgument(r >= 0, r, "const-width left shift amount must be >= 0 (you passed %d)", r); // just turn it into a BVSHL return d_em->mkExpr(CVC4::kind::BITVECTOR_SHL, t1, d_em->mkConst(CVC4::BitVector(CVC4::BitVectorType(t1.getType()).getSize(), unsigned(r)))); } Expr ValidityChecker::newFixedRightShiftExpr(const Expr& t1, int r) { - CVC4::CheckArgument(t1.getType().isBitVector(), t1, "can only right-shift a bitvector, not a `%s'", t1.getType().toString().c_str()); - CVC4::CheckArgument(r >= 0, r, "right shift amount must be >= 0 (you passed %d)", r); + CompatCheckArgument(t1.getType().isBitVector(), t1, "can only right-shift a bitvector, not a `%s'", t1.getType().toString().c_str()); + CompatCheckArgument(r >= 0, r, "right shift amount must be >= 0 (you passed %d)", r); // Defined in: // http://www.cs.nyu.edu/acsys/cvc3/doc/user_doc.html#user_doc_pres_lang_expr_bit // Should be equivalent to a BVLSHR; just turn it into that. @@ -2101,20 +2179,20 @@ Expr ValidityChecker::newFixedRightShiftExpr(const Expr& t1, int r) { } Expr ValidityChecker::newBVSHL(const Expr& t1, const Expr& t2) { - CVC4::CheckArgument(t1.getType().isBitVector(), t1, "can only right-shift a bitvector, not a `%s'", t1.getType().toString().c_str()); - CVC4::CheckArgument(t2.getType().isBitVector(), t2, "can only right-shift by a bitvector, not a `%s'", t2.getType().toString().c_str()); + CompatCheckArgument(t1.getType().isBitVector(), t1, "can only right-shift a bitvector, not a `%s'", t1.getType().toString().c_str()); + CompatCheckArgument(t2.getType().isBitVector(), t2, "can only right-shift by a bitvector, not a `%s'", t2.getType().toString().c_str()); return d_em->mkExpr(CVC4::kind::BITVECTOR_SHL, t1, t2); } Expr ValidityChecker::newBVLSHR(const Expr& t1, const Expr& t2) { - CVC4::CheckArgument(t1.getType().isBitVector(), t1, "can only right-shift a bitvector, not a `%s'", t1.getType().toString().c_str()); - CVC4::CheckArgument(t2.getType().isBitVector(), t2, "can only right-shift by a bitvector, not a `%s'", t2.getType().toString().c_str()); + CompatCheckArgument(t1.getType().isBitVector(), t1, "can only right-shift a bitvector, not a `%s'", t1.getType().toString().c_str()); + CompatCheckArgument(t2.getType().isBitVector(), t2, "can only right-shift by a bitvector, not a `%s'", t2.getType().toString().c_str()); return d_em->mkExpr(CVC4::kind::BITVECTOR_LSHR, t1, t2); } Expr ValidityChecker::newBVASHR(const Expr& t1, const Expr& t2) { - CVC4::CheckArgument(t1.getType().isBitVector(), t1, "can only right-shift a bitvector, not a `%s'", t1.getType().toString().c_str()); - CVC4::CheckArgument(t2.getType().isBitVector(), t2, "can only right-shift by a bitvector, not a `%s'", t2.getType().toString().c_str()); + CompatCheckArgument(t1.getType().isBitVector(), t1, "can only right-shift a bitvector, not a `%s'", t1.getType().toString().c_str()); + CompatCheckArgument(t2.getType().isBitVector(), t2, "can only right-shift by a bitvector, not a `%s'", t2.getType().toString().c_str()); return d_em->mkExpr(CVC4::kind::BITVECTOR_ASHR, t1, t2); } @@ -2129,30 +2207,30 @@ Expr ValidityChecker::tupleExpr(const std::vector<Expr>& exprs) { } Expr ValidityChecker::tupleSelectExpr(const Expr& tuple, int index) { - CVC4::CheckArgument(index >= 0 && index < tuple.getNumChildren(), + CompatCheckArgument(index >= 0 && index < tuple.getNumChildren(), "invalid index in tuple select"); return d_em->mkExpr(d_em->mkConst(CVC4::TupleSelect(index)), tuple); } Expr ValidityChecker::tupleUpdateExpr(const Expr& tuple, int index, const Expr& newValue) { - CVC4::CheckArgument(index >= 0 && index < tuple.getNumChildren(), + CompatCheckArgument(index >= 0 && index < tuple.getNumChildren(), "invalid index in tuple update"); return d_em->mkExpr(d_em->mkConst(CVC4::TupleUpdate(index)), tuple, newValue); } Expr ValidityChecker::datatypeConsExpr(const std::string& constructor, const std::vector<Expr>& args) { ConstructorMap::const_iterator i = d_constructors.find(constructor); - CVC4::CheckArgument(i != d_constructors.end(), constructor, "no such constructor"); + CompatCheckArgument(i != d_constructors.end(), constructor, "no such constructor"); const CVC4::Datatype& dt = *(*i).second; const CVC4::DatatypeConstructor& ctor = dt[constructor]; - CVC4::CheckArgument(ctor.getNumArgs() == args.size(), args, "arity mismatch in constructor application"); + CompatCheckArgument(ctor.getNumArgs() == args.size(), args, "arity mismatch in constructor application"); return d_em->mkExpr(CVC4::kind::APPLY_CONSTRUCTOR, ctor.getConstructor(), vector<CVC4::Expr>(args.begin(), args.end())); } Expr ValidityChecker::datatypeSelExpr(const std::string& selector, const Expr& arg) { SelectorMap::const_iterator i = d_selectors.find(selector); - CVC4::CheckArgument(i != d_selectors.end(), selector, "no such selector"); + CompatCheckArgument(i != d_selectors.end(), selector, "no such selector"); const CVC4::Datatype& dt = *(*i).second.first; string constructor = (*i).second.second; const CVC4::DatatypeConstructor& ctor = dt[constructor]; @@ -2161,7 +2239,7 @@ Expr ValidityChecker::datatypeSelExpr(const std::string& selector, const Expr& a Expr ValidityChecker::datatypeTestExpr(const std::string& constructor, const Expr& arg) { ConstructorMap::const_iterator i = d_constructors.find(constructor); - CVC4::CheckArgument(i != d_constructors.end(), constructor, "no such constructor"); + CompatCheckArgument(i != d_constructors.end(), constructor, "no such constructor"); const CVC4::Datatype& dt = *(*i).second; const CVC4::DatatypeConstructor& ctor = dt[constructor]; return d_em->mkExpr(CVC4::kind::APPLY_TESTER, ctor.getTester(), arg); @@ -2314,7 +2392,7 @@ void ValidityChecker::returnFromCheck() { } void ValidityChecker::getUserAssumptions(std::vector<Expr>& assumptions) { - CVC4::CheckArgument(assumptions.empty(), assumptions, "assumptions arg must be empty"); + CompatCheckArgument(assumptions.empty(), assumptions, "assumptions arg must be empty"); vector<CVC4::Expr> v = d_smt->getAssertions(); assumptions.swap(*reinterpret_cast<vector<Expr>*>(&v)); } @@ -2349,7 +2427,7 @@ QueryResult ValidityChecker::tryModelGeneration() { } FormulaValue ValidityChecker::value(const Expr& e) { - CVC4::CheckArgument(e.getType() == d_em->booleanType(), e, "argument must be a formula"); + CompatCheckArgument(e.getType() == d_em->booleanType(), e, "argument must be a formula"); try { return d_smt->getValue(e).getConst<bool>() ? TRUE_VAL : FALSE_VAL; } catch(CVC4::Exception& e) { @@ -2367,7 +2445,7 @@ Expr ValidityChecker::getValue(const Expr& e) { } bool ValidityChecker::inconsistent(std::vector<Expr>& assumptions) { - CVC4::CheckArgument(assumptions.empty(), assumptions, "assumptions vector should be empty on entry"); + CompatCheckArgument(assumptions.empty(), assumptions, "assumptions vector should be empty on entry"); if(d_smt->checkSat() == CVC4::Result::UNSAT) { // supposed to be a minimal set, but CVC4 doesn't support that d_smt->getAssertions().swap(*reinterpret_cast<std::vector<CVC4::Expr>*>(&assumptions)); @@ -2427,9 +2505,9 @@ void ValidityChecker::pop() { } void ValidityChecker::popto(int stackLevel) { - CVC4::CheckArgument(stackLevel >= 0, stackLevel, + CompatCheckArgument(stackLevel >= 0, stackLevel, "Cannot pop to a negative stack level %d", stackLevel); - CVC4::CheckArgument(unsigned(stackLevel) <= d_stackLevel, stackLevel, + CompatCheckArgument(unsigned(stackLevel) <= d_stackLevel, stackLevel, "Cannot pop to a stack level higher than the current one! " "At stack level %u, user requested stack level %d", d_stackLevel, stackLevel); @@ -2451,9 +2529,9 @@ void ValidityChecker::popScope() { } void ValidityChecker::poptoScope(int scopeLevel) { - CVC4::CheckArgument(scopeLevel >= 0, scopeLevel, + CompatCheckArgument(scopeLevel >= 0, scopeLevel, "Cannot pop to a negative scope level %d", scopeLevel); - CVC4::CheckArgument(unsigned(scopeLevel) <= d_parserContext->scopeLevel(), + CompatCheckArgument(unsigned(scopeLevel) <= d_parserContext->scopeLevel(), scopeLevel, "Cannot pop to a scope level higher than the current one! " "At scope level %u, user requested scope level %d", diff --git a/src/cvc4.i b/src/cvc4.i index ad042d398..6ee0c7572 100644 --- a/src/cvc4.i +++ b/src/cvc4.i @@ -40,13 +40,13 @@ namespace std { namespace CVC4 {} using namespace CVC4; -#include <iostream> -#include <vector> +#include <cassert> +#include <ext/hash_map> +#include <iosfwd> #include <set> #include <string> -#include <ext/hash_map> #include <typeinfo> -#include <cassert> +#include <vector> #include "base/exception.h" #include "base/modal_exception.h" diff --git a/src/expr/array_store_all.cpp b/src/expr/array_store_all.cpp index 62c8ec978..d9d0a5f8d 100644 --- a/src/expr/array_store_all.cpp +++ b/src/expr/array_store_all.cpp @@ -20,12 +20,85 @@ #include <iostream> +#include "base/cvc4_assert.h" +#include "expr/expr.h" +#include "expr/type.h" + using namespace std; namespace CVC4 { +ArrayStoreAll::ArrayStoreAll(const ArrayStoreAll& other) + : d_type(new ArrayType(other.getType())) + , d_expr(new Expr(other.getExpr())) {} + +ArrayStoreAll::~ArrayStoreAll() throw() { + delete d_expr; + delete d_type; +} + +ArrayStoreAll& ArrayStoreAll::operator=(const ArrayStoreAll& other){ + (*d_type) = other.getType(); + (*d_expr) = other.getExpr(); +} + +ArrayStoreAll::ArrayStoreAll(const ArrayType& type, const Expr& expr) + throw(IllegalArgumentException) + : d_type(new ArrayType(type)) + , d_expr(new Expr(expr)) +{ + // this check is stronger than the assertion check in the expr manager that ArrayTypes are actually array types + // because this check is done in production builds too + PrettyCheckArgument( + type.isArray(), + type, + "array store-all constants can only be created for array types, not `%s'", + type.toString().c_str()); + + PrettyCheckArgument( + expr.getType().isComparableTo(type.getConstituentType()), + expr, + "expr type `%s' does not match constituent type of array type `%s'", + expr.getType().toString().c_str(), + type.toString().c_str()); + + PrettyCheckArgument( + expr.isConst(), + expr, + "ArrayStoreAll requires a constant expression"); +} + + +const ArrayType& ArrayStoreAll::getType() const throw() { + return *d_type; +} + +const Expr& ArrayStoreAll::getExpr() const throw() { + return *d_expr; +} + +bool ArrayStoreAll::operator==(const ArrayStoreAll& asa) const throw() { + return getType() == asa.getType() && getExpr() == asa.getExpr(); +} + + +bool ArrayStoreAll::operator<(const ArrayStoreAll& asa) const throw() { + return (getType() < asa.getType()) || + (getType() == asa.getType() && getExpr() < asa.getExpr()); +} + +bool ArrayStoreAll::operator<=(const ArrayStoreAll& asa) const throw() { + return (getType() < asa.getType()) || + (getType() == asa.getType() && getExpr() <= asa.getExpr()); +} + std::ostream& operator<<(std::ostream& out, const ArrayStoreAll& asa) { return out << "__array_store_all__(" << asa.getType() << ", " << asa.getExpr() << ')'; } +size_t ArrayStoreAllHashFunction::operator()(const ArrayStoreAll& asa) const { + return TypeHashFunction()(asa.getType()) * ExprHashFunction()(asa.getExpr()); +} + + }/* CVC4 namespace */ diff --git a/src/expr/array_store_all.h b/src/expr/array_store_all.h index b1d624266..293b785a9 100644 --- a/src/expr/array_store_all.h +++ b/src/expr/array_store_all.h @@ -20,61 +20,43 @@ #pragma once +#include <iosfwd> + +#include "base/exception.h" + namespace CVC4 { // messy; Expr needs ArrayStoreAll (because it's the payload of a // CONSTANT-kinded expression), and ArrayStoreAll needs Expr. - class CVC4_PUBLIC ArrayStoreAll; + class Expr; + class ArrayType; }/* CVC4 namespace */ -#include "expr/expr.h" -#include "expr/type.h" -#include <iostream> namespace CVC4 { class CVC4_PUBLIC ArrayStoreAll { - const ArrayType d_type; - const Expr d_expr; - public: + ArrayStoreAll(const ArrayStoreAll& other); - ArrayStoreAll(ArrayType type, Expr expr) throw(IllegalArgumentException) : - d_type(type), - d_expr(expr) { + ArrayStoreAll& operator=(const ArrayStoreAll& other); - // this check is stronger than the assertion check in the expr manager that ArrayTypes are actually array types - // because this check is done in production builds too - CheckArgument(type.isArray(), type, "array store-all constants can only be created for array types, not `%s'", type.toString().c_str()); + ArrayStoreAll(const ArrayType& type, const Expr& expr) + throw(IllegalArgumentException); - CheckArgument(expr.getType().isComparableTo(type.getConstituentType()), expr, "expr type `%s' does not match constituent type of array type `%s'", expr.getType().toString().c_str(), type.toString().c_str()); - CheckArgument(expr.isConst(), expr, "ArrayStoreAll requires a constant expression"); - } + ~ArrayStoreAll() throw(); - ~ArrayStoreAll() throw() { - } + const ArrayType& getType() const throw(); - ArrayType getType() const throw() { - return d_type; - } - Expr getExpr() const throw() { - return d_expr; - } + const Expr& getExpr() const throw(); + + bool operator==(const ArrayStoreAll& asa) const throw(); - bool operator==(const ArrayStoreAll& asa) const throw() { - return d_type == asa.d_type && d_expr == asa.d_expr; - } bool operator!=(const ArrayStoreAll& asa) const throw() { return !(*this == asa); } - bool operator<(const ArrayStoreAll& asa) const throw() { - return d_type < asa.d_type || - (d_type == asa.d_type && d_expr < asa.d_expr); - } - bool operator<=(const ArrayStoreAll& asa) const throw() { - return d_type < asa.d_type || - (d_type == asa.d_type && d_expr <= asa.d_expr); - } + bool operator<(const ArrayStoreAll& asa) const throw(); + bool operator<=(const ArrayStoreAll& asa) const throw(); bool operator>(const ArrayStoreAll& asa) const throw() { return !(*this <= asa); } @@ -82,6 +64,9 @@ public: return !(*this < asa); } +private: + ArrayType* d_type; + Expr* d_expr; };/* class ArrayStoreAll */ std::ostream& operator<<(std::ostream& out, const ArrayStoreAll& asa) CVC4_PUBLIC; @@ -90,9 +75,7 @@ std::ostream& operator<<(std::ostream& out, const ArrayStoreAll& asa) CVC4_PUBLI * Hash function for the ArrayStoreAll constants. */ struct CVC4_PUBLIC ArrayStoreAllHashFunction { - inline size_t operator()(const ArrayStoreAll& asa) const { - return TypeHashFunction()(asa.getType()) * ExprHashFunction()(asa.getExpr()); - } + size_t operator()(const ArrayStoreAll& asa) const; };/* struct ArrayStoreAllHashFunction */ }/* CVC4 namespace */ diff --git a/src/expr/datatype.cpp b/src/expr/datatype.cpp index 4ebc5071f..b9870afb4 100644 --- a/src/expr/datatype.cpp +++ b/src/expr/datatype.cpp @@ -67,7 +67,7 @@ const Datatype& Datatype::datatypeOf(Expr item) { size_t Datatype::indexOf(Expr item) { ExprManagerScope ems(item); - CheckArgument(item.getType().isConstructor() || + PrettyCheckArgument(item.getType().isConstructor() || item.getType().isTester() || item.getType().isSelector(), item, @@ -83,7 +83,7 @@ size_t Datatype::indexOf(Expr item) { size_t Datatype::cindexOf(Expr item) { ExprManagerScope ems(item); - CheckArgument(item.getType().isSelector(), + PrettyCheckArgument(item.getType().isSelector(), item, "arg must be a datatype selector"); TNode n = Node::fromExpr(item); @@ -103,17 +103,17 @@ void Datatype::resolve(ExprManager* em, const std::vector< DatatypeType >& paramReplacements) throw(IllegalArgumentException, DatatypeResolutionException) { - 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, + PrettyCheckArgument(em != NULL, em, "cannot resolve a Datatype with a NULL expression manager"); + PrettyCheckArgument(!d_resolved, this, "cannot resolve a Datatype twice"); + PrettyCheckArgument(resolutions.find(d_name) != resolutions.end(), resolutions, "Datatype::resolve(): resolutions doesn't contain me!"); - CheckArgument(placeholders.size() == replacements.size(), placeholders, + PrettyCheckArgument(placeholders.size() == replacements.size(), placeholders, "placeholders and replacements must be the same size"); - CheckArgument(paramTypes.size() == paramReplacements.size(), paramTypes, + PrettyCheckArgument(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"); + PrettyCheckArgument(getNumConstructors() > 0, *this, "cannot resolve a Datatype that has no constructors"); DatatypeType self = (*resolutions.find(d_name)).second; - CheckArgument(&self.getDatatype() == this, resolutions, "Datatype::resolve(): resolutions doesn't contain me!"); + PrettyCheckArgument(&self.getDatatype() == this, resolutions, "Datatype::resolve(): resolutions doesn't contain me!"); d_resolved = true; size_t index = 0; for(std::vector<DatatypeConstructor>::iterator i = d_constructors.begin(), i_end = d_constructors.end(); i != i_end; ++i) { @@ -136,14 +136,14 @@ void Datatype::resolve(ExprManager* em, } void Datatype::addConstructor(const DatatypeConstructor& c) { - CheckArgument(!d_resolved, this, + PrettyCheckArgument(!d_resolved, this, "cannot add a constructor to a finalized Datatype"); d_constructors.push_back(c); } void Datatype::setSygus( Type st, Expr bvl, bool allow_const, bool allow_all ){ - CheckArgument(!d_resolved, this, + PrettyCheckArgument(!d_resolved, this, "cannot set sygus type to a finalized Datatype"); d_sygus_type = st; d_sygus_bvl = bvl; @@ -153,14 +153,14 @@ void Datatype::setSygus( Type st, Expr bvl, bool allow_const, bool allow_all ){ Cardinality Datatype::getCardinality() const throw(IllegalArgumentException) { - CheckArgument(isResolved(), this, "this datatype is not yet resolved"); + PrettyCheckArgument(isResolved(), this, "this datatype is not yet resolved"); std::vector< Type > processing; computeCardinality( processing ); return d_card; } Cardinality Datatype::computeCardinality( std::vector< Type >& processing ) const throw(IllegalArgumentException){ - CheckArgument(isResolved(), this, "this datatype is not yet resolved"); + PrettyCheckArgument(isResolved(), this, "this datatype is not yet resolved"); if( std::find( processing.begin(), processing.end(), d_self )!=processing.end() ){ d_card = Cardinality::INTEGERS; }else{ @@ -176,7 +176,7 @@ Cardinality Datatype::computeCardinality( std::vector< Type >& processing ) cons } bool Datatype::isRecursiveSingleton() const throw(IllegalArgumentException) { - CheckArgument(isResolved(), this, "this datatype is not yet resolved"); + PrettyCheckArgument(isResolved(), this, "this datatype is not yet resolved"); if( d_card_rec_singleton==0 ){ Assert( d_card_u_assume.empty() ); std::vector< Type > processing; @@ -251,7 +251,8 @@ bool Datatype::computeCardinalityRecSingleton( std::vector< Type >& processing, } bool Datatype::isFinite() const throw(IllegalArgumentException) { - CheckArgument(isResolved(), this, "this datatype is not yet resolved"); + PrettyCheckArgument(isResolved(), this, "this datatype is not yet resolved"); + // we're using some internals, so we have to set up this library context ExprManagerScope ems(d_self); TypeNode self = TypeNode::fromType(d_self); @@ -272,7 +273,7 @@ bool Datatype::isFinite() const throw(IllegalArgumentException) { } bool Datatype::isUFinite() const throw(IllegalArgumentException) { - CheckArgument(isResolved(), this, "this datatype is not yet resolved"); + PrettyCheckArgument(isResolved(), this, "this datatype is not yet resolved"); // we're using some internals, so we have to set up this library context ExprManagerScope ems(d_self); TypeNode self = TypeNode::fromType(d_self); @@ -293,7 +294,7 @@ bool Datatype::isUFinite() const throw(IllegalArgumentException) { } bool Datatype::isWellFounded() const throw(IllegalArgumentException) { - CheckArgument(isResolved(), this, "this datatype is not yet resolved"); + PrettyCheckArgument(isResolved(), this, "this datatype is not yet resolved"); if( d_well_founded==0 ){ // we're using some internals, so we have to set up this library context ExprManagerScope ems(d_self); @@ -308,7 +309,7 @@ bool Datatype::isWellFounded() const throw(IllegalArgumentException) { } bool Datatype::computeWellFounded( std::vector< Type >& processing ) const throw(IllegalArgumentException) { - CheckArgument(isResolved(), this, "this datatype is not yet resolved"); + PrettyCheckArgument(isResolved(), this, "this datatype is not yet resolved"); if( std::find( processing.begin(), processing.end(), d_self )!=processing.end() ){ return d_isCo; }else{ @@ -328,7 +329,7 @@ bool Datatype::computeWellFounded( std::vector< Type >& processing ) const throw } Expr Datatype::mkGroundTerm( Type t ) const throw(IllegalArgumentException) { - CheckArgument(isResolved(), this, "this datatype is not yet resolved"); + PrettyCheckArgument(isResolved(), this, "this datatype is not yet resolved"); ExprManagerScope ems(d_self); @@ -348,7 +349,7 @@ Expr Datatype::mkGroundTerm( Type t ) const throw(IllegalArgumentException) { if( groundTerm.isNull() ){ if( !d_isCo ){ // if we get all the way here, we aren't well-founded - CheckArgument(false, *this, "datatype is not well-founded, cannot construct a ground term!"); + IllegalArgument(*this, "datatype is not well-founded, cannot construct a ground term!"); }else{ return groundTerm; } @@ -404,15 +405,15 @@ Expr Datatype::computeGroundTerm( Type t, std::vector< Type >& processing ) cons } DatatypeType Datatype::getDatatypeType() const throw(IllegalArgumentException) { - CheckArgument(isResolved(), *this, "Datatype must be resolved to get its DatatypeType"); - CheckArgument(!d_self.isNull(), *this); + PrettyCheckArgument(isResolved(), *this, "Datatype must be resolved to get its DatatypeType"); + PrettyCheckArgument(!d_self.isNull(), *this); return DatatypeType(d_self); } DatatypeType Datatype::getDatatypeType(const std::vector<Type>& params) const throw(IllegalArgumentException) { - CheckArgument(isResolved(), *this, "Datatype must be resolved to get its DatatypeType"); - CheckArgument(!d_self.isNull() && DatatypeType(d_self).isParametric(), this); + PrettyCheckArgument(isResolved(), *this, "Datatype must be resolved to get its DatatypeType"); + PrettyCheckArgument(!d_self.isNull() && DatatypeType(d_self).isParametric(), this); return DatatypeType(d_self).instantiate(params); } @@ -491,7 +492,7 @@ bool Datatype::operator==(const Datatype& other) const throw() { } const DatatypeConstructor& Datatype::operator[](size_t index) const { - CheckArgument(index < getNumConstructors(), index, "index out of bounds"); + PrettyCheckArgument(index < getNumConstructors(), index, "index out of bounds"); return d_constructors[index]; } @@ -501,7 +502,7 @@ const DatatypeConstructor& Datatype::operator[](std::string name) const { return *i; } } - CheckArgument(false, name, "No such constructor `%s' of datatype `%s'", name.c_str(), d_name.c_str()); + IllegalArgument(name, "No such constructor `%s' of datatype `%s'", name.c_str(), d_name.c_str()); } Expr Datatype::getConstructor(std::string name) const { @@ -540,8 +541,8 @@ void DatatypeConstructor::resolve(ExprManager* em, DatatypeType self, const std::vector< DatatypeType >& paramReplacements, size_t cindex) throw(IllegalArgumentException, DatatypeResolutionException) { - CheckArgument(em != NULL, em, "cannot resolve a Datatype with a NULL expression manager"); - CheckArgument(!isResolved(), + PrettyCheckArgument(em != NULL, em, "cannot resolve a Datatype with a NULL expression manager"); + PrettyCheckArgument(!isResolved(), "cannot resolve a Datatype constructor twice; " "perhaps the same constructor was added twice, " "or to two datatypes?"); @@ -640,7 +641,7 @@ DatatypeConstructor::DatatypeConstructor(std::string name) : d_name(name + '\0' + "is_" + name), // default tester name is "is_FOO" d_tester(), d_args() { - CheckArgument(name != "", name, "cannot construct a datatype constructor without a name"); + PrettyCheckArgument(name != "", name, "cannot construct a datatype constructor without a name"); } DatatypeConstructor::DatatypeConstructor(std::string name, std::string tester) : @@ -651,8 +652,8 @@ DatatypeConstructor::DatatypeConstructor(std::string name, std::string tester) : d_name(name + '\0' + tester), d_tester(), d_args() { - CheckArgument(name != "", name, "cannot construct a datatype constructor without a name"); - CheckArgument(!tester.empty(), tester, "cannot construct a datatype constructor without a tester"); + PrettyCheckArgument(name != "", name, "cannot construct a datatype constructor without a name"); + PrettyCheckArgument(!tester.empty(), tester, "cannot construct a datatype constructor without a tester"); } void DatatypeConstructor::setSygus( Expr op, Expr let_body, std::vector< Expr >& let_args, unsigned num_let_input_args ){ @@ -668,8 +669,8 @@ void DatatypeConstructor::addArg(std::string selectorName, Type selectorType) { // we're going to be a constant stuffed inside a node. So we stow // the selector type away inside a var until resolution (when we can // create the proper selector type) - CheckArgument(!isResolved(), this, "cannot modify a finalized Datatype constructor"); - CheckArgument(!selectorType.isNull(), selectorType, "cannot add a null selector type"); + PrettyCheckArgument(!isResolved(), this, "cannot modify a finalized Datatype constructor"); + PrettyCheckArgument(!selectorType.isNull(), selectorType, "cannot add a null selector type"); // we're using some internals, so we have to set up this library context ExprManagerScope ems(selectorType); @@ -684,8 +685,8 @@ void DatatypeConstructor::addArg(std::string selectorName, DatatypeUnresolvedTyp // we're going to be a constant stuffed inside a node. So we stow // the selector type away after a NUL in the name string until // resolution (when we can create the proper selector type) - CheckArgument(!isResolved(), this, "cannot modify a finalized Datatype constructor"); - CheckArgument(selectorType.getName() != "", selectorType, "cannot add a null selector type"); + PrettyCheckArgument(!isResolved(), this, "cannot modify a finalized Datatype constructor"); + PrettyCheckArgument(selectorType.getName() != "", selectorType, "cannot add a null selector type"); d_args.push_back(DatatypeConstructorArg(selectorName + '\0' + selectorType.getName(), Expr())); } @@ -695,7 +696,7 @@ void DatatypeConstructor::addArg(std::string selectorName, DatatypeSelfType) { // the name string with a NUL to indicate that we have a // self-selecting selector until resolution (when we can create the // proper selector type) - CheckArgument(!isResolved(), this, "cannot modify a finalized Datatype constructor"); + PrettyCheckArgument(!isResolved(), this, "cannot modify a finalized Datatype constructor"); d_args.push_back(DatatypeConstructorArg(selectorName + '\0', Expr())); } @@ -708,15 +709,15 @@ std::string DatatypeConstructor::getTesterName() const throw() { } Expr DatatypeConstructor::getConstructor() const { - CheckArgument(isResolved(), this, "this datatype constructor is not yet resolved"); + PrettyCheckArgument(isResolved(), this, "this datatype constructor is not yet resolved"); return d_constructor; } Type DatatypeConstructor::getSpecializedConstructorType(Type returnType) const { - CheckArgument(isResolved(), this, "this datatype constructor is not yet resolved"); + PrettyCheckArgument(isResolved(), this, "this datatype constructor is not yet resolved"); ExprManagerScope ems(d_constructor); const Datatype& dt = Datatype::datatypeOf(d_constructor); - CheckArgument(dt.isParametric(), this, "this datatype constructor is not parametric"); + PrettyCheckArgument(dt.isParametric(), this, "this datatype constructor is not parametric"); DatatypeType dtt = dt.getDatatypeType(); Matcher m(dtt); m.doMatching( TypeNode::fromType(dtt), TypeNode::fromType(returnType) ); @@ -727,42 +728,42 @@ Type DatatypeConstructor::getSpecializedConstructorType(Type returnType) const { } Expr DatatypeConstructor::getTester() const { - CheckArgument(isResolved(), this, "this datatype constructor is not yet resolved"); + PrettyCheckArgument(isResolved(), this, "this datatype constructor is not yet resolved"); return d_tester; } Expr DatatypeConstructor::getSygusOp() const { - CheckArgument(isResolved(), this, "this datatype constructor is not yet resolved"); + PrettyCheckArgument(isResolved(), this, "this datatype constructor is not yet resolved"); return d_sygus_op; } Expr DatatypeConstructor::getSygusLetBody() const { - CheckArgument(isResolved(), this, "this datatype constructor is not yet resolved"); + PrettyCheckArgument(isResolved(), this, "this datatype constructor is not yet resolved"); return d_sygus_let_body; } unsigned DatatypeConstructor::getNumSygusLetArgs() const { - CheckArgument(isResolved(), this, "this datatype constructor is not yet resolved"); + PrettyCheckArgument(isResolved(), this, "this datatype constructor is not yet resolved"); return d_sygus_let_args.size(); } Expr DatatypeConstructor::getSygusLetArg( unsigned i ) const { - CheckArgument(isResolved(), this, "this datatype constructor is not yet resolved"); + PrettyCheckArgument(isResolved(), this, "this datatype constructor is not yet resolved"); return d_sygus_let_args[i]; } unsigned DatatypeConstructor::getNumSygusLetInputArgs() const { - CheckArgument(isResolved(), this, "this datatype constructor is not yet resolved"); + PrettyCheckArgument(isResolved(), this, "this datatype constructor is not yet resolved"); return d_sygus_num_let_input_args; } bool DatatypeConstructor::isSygusIdFunc() const { - CheckArgument(isResolved(), this, "this datatype constructor is not yet resolved"); + PrettyCheckArgument(isResolved(), this, "this datatype constructor is not yet resolved"); return d_sygus_let_args.size()==1 && d_sygus_let_args[0]==d_sygus_let_body; } Cardinality DatatypeConstructor::getCardinality() const throw(IllegalArgumentException) { - CheckArgument(isResolved(), this, "this datatype constructor is not yet resolved"); + PrettyCheckArgument(isResolved(), this, "this datatype constructor is not yet resolved"); Cardinality c = 1; @@ -803,7 +804,8 @@ bool DatatypeConstructor::computeWellFounded( std::vector< Type >& processing ) bool DatatypeConstructor::isFinite() const throw(IllegalArgumentException) { - CheckArgument(isResolved(), this, "this datatype constructor is not yet resolved"); + PrettyCheckArgument(isResolved(), this, "this datatype constructor is not yet resolved"); + // we're using some internals, so we have to set up this library context ExprManagerScope ems(d_constructor); TNode self = Node::fromExpr(d_constructor); @@ -822,8 +824,9 @@ bool DatatypeConstructor::isFinite() const throw(IllegalArgumentException) { self.setAttribute(DatatypeFiniteAttr(), true); return true; } + bool DatatypeConstructor::isUFinite() const throw(IllegalArgumentException) { - CheckArgument(isResolved(), this, "this datatype constructor is not yet resolved"); + PrettyCheckArgument(isResolved(), this, "this datatype constructor is not yet resolved"); // we're using some internals, so we have to set up this library context ExprManagerScope ems(d_constructor); TNode self = Node::fromExpr(d_constructor); @@ -899,7 +902,7 @@ Expr DatatypeConstructor::computeGroundTerm( Type t, std::vector< Type >& proces const DatatypeConstructorArg& DatatypeConstructor::operator[](size_t index) const { - CheckArgument(index < getNumArgs(), index, "index out of bounds"); + PrettyCheckArgument(index < getNumArgs(), index, "index out of bounds"); return d_args[index]; } @@ -909,7 +912,7 @@ const DatatypeConstructorArg& DatatypeConstructor::operator[](std::string name) return *i; } } - CheckArgument(false, name, "No such arg `%s' of constructor `%s'", name.c_str(), d_name.c_str()); + IllegalArgument(name, "No such arg `%s' of constructor `%s'", name.c_str(), d_name.c_str()); } Expr DatatypeConstructor::getSelector(std::string name) const { @@ -938,7 +941,7 @@ DatatypeConstructorArg::DatatypeConstructorArg(std::string name, Expr selector) d_name(name), d_selector(selector), d_resolved(false) { - CheckArgument(name != "", name, "cannot construct a datatype constructor arg without a name"); + PrettyCheckArgument(name != "", name, "cannot construct a datatype constructor arg without a name"); } std::string DatatypeConstructorArg::getName() const throw() { @@ -951,12 +954,12 @@ std::string DatatypeConstructorArg::getName() const throw() { } Expr DatatypeConstructorArg::getSelector() const { - CheckArgument(isResolved(), this, "cannot get a selector for an unresolved datatype constructor"); + PrettyCheckArgument(isResolved(), this, "cannot get a selector for an unresolved datatype constructor"); return d_selector; } Expr DatatypeConstructorArg::getConstructor() const { - CheckArgument(isResolved(), this, + PrettyCheckArgument(isResolved(), this, "cannot get a associated constructor for argument of an unresolved datatype constructor"); return d_constructor; } diff --git a/src/expr/datatype.h b/src/expr/datatype.h index 1ea9fd6be..5f80c54f7 100644 --- a/src/expr/datatype.h +++ b/src/expr/datatype.h @@ -798,13 +798,16 @@ inline size_t Datatype::getNumParameters() const throw() { } inline Type Datatype::getParameter( unsigned int i ) const { - CheckArgument(isParametric(), this, "cannot get type parameter of a non-parametric datatype"); - CheckArgument(i < d_params.size(), i, "type parameter index out of range for datatype"); + CheckArgument(isParametric(), this, + "Cannot get type parameter of a non-parametric datatype."); + CheckArgument(i < d_params.size(), i, + "Type parameter index out of range for datatype."); return d_params[i]; } inline std::vector<Type> Datatype::getParameters() const { - CheckArgument(isParametric(), this, "cannot get type parameters of a non-parametric datatype"); + CheckArgument(isParametric(), this, + "Cannot get type parameters of a non-parametric datatype."); return d_params; } diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp index e7088a395..59f423e3c 100644 --- a/src/expr/expr_manager_template.cpp +++ b/src/expr/expr_manager_template.cpp @@ -29,7 +29,7 @@ ${includes} // compiler directs the user to the template file instead of the // generated one. We don't want the user to modify the generated one, // since it'll get overwritten on a later build. -#line 32 "${template}" +#line 33 "${template}" #ifdef CVC4_STATISTICS_ON #define INC_STAT(kind) \ @@ -164,16 +164,18 @@ RoundingModeType ExprManager::roundingModeType() const { Expr ExprManager::mkExpr(Kind kind, Expr child1) { const kind::MetaKind mk = kind::metaKindOf(kind); const unsigned n = 1 - (mk == kind::metakind::PARAMETERIZED ? 1 : 0); - CheckArgument(mk == kind::metakind::PARAMETERIZED || - mk == kind::metakind::OPERATOR, kind, - "Only operator-style expressions are made with mkExpr(); " - "to make variables and constants, see mkVar(), mkBoundVar(), " - "and mkConst()."); - CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind, - "Exprs with kind %s must have at least %u children and " - "at most %u children (the one under construction has %u)", - kind::kindToString(kind).c_str(), - minArity(kind), maxArity(kind), n); + PrettyCheckArgument( + mk == kind::metakind::PARAMETERIZED || + mk == kind::metakind::OPERATOR, kind, + "Only operator-style expressions are made with mkExpr(); " + "to make variables and constants, see mkVar(), mkBoundVar(), " + "and mkConst()."); + PrettyCheckArgument( + n >= minArity(kind) && n <= maxArity(kind), kind, + "Exprs with kind %s must have at least %u children and " + "at most %u children (the one under construction has %u)", + kind::kindToString(kind).c_str(), + minArity(kind), maxArity(kind), n); NodeManagerScope nms(d_nodeManager); try { INC_STAT(kind); @@ -186,16 +188,18 @@ Expr ExprManager::mkExpr(Kind kind, Expr child1) { Expr ExprManager::mkExpr(Kind kind, Expr child1, Expr child2) { const kind::MetaKind mk = kind::metaKindOf(kind); const unsigned n = 2 - (mk == kind::metakind::PARAMETERIZED ? 1 : 0); - CheckArgument(mk == kind::metakind::PARAMETERIZED || - mk == kind::metakind::OPERATOR, kind, - "Only operator-style expressions are made with mkExpr(); " - "to make variables and constants, see mkVar(), mkBoundVar(), " - "and mkConst()."); - CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind, - "Exprs with kind %s must have at least %u children and " - "at most %u children (the one under construction has %u)", - kind::kindToString(kind).c_str(), - minArity(kind), maxArity(kind), n); + PrettyCheckArgument( + mk == kind::metakind::PARAMETERIZED || + mk == kind::metakind::OPERATOR, kind, + "Only operator-style expressions are made with mkExpr(); " + "to make variables and constants, see mkVar(), mkBoundVar(), " + "and mkConst()."); + PrettyCheckArgument( + n >= minArity(kind) && n <= maxArity(kind), kind, + "Exprs with kind %s must have at least %u children and " + "at most %u children (the one under construction has %u)", + kind::kindToString(kind).c_str(), + minArity(kind), maxArity(kind), n); NodeManagerScope nms(d_nodeManager); try { INC_STAT(kind); @@ -210,16 +214,18 @@ Expr ExprManager::mkExpr(Kind kind, Expr child1, Expr child2) { Expr ExprManager::mkExpr(Kind kind, Expr child1, Expr child2, Expr child3) { const kind::MetaKind mk = kind::metaKindOf(kind); const unsigned n = 3 - (mk == kind::metakind::PARAMETERIZED ? 1 : 0); - CheckArgument(mk == kind::metakind::PARAMETERIZED || - mk == kind::metakind::OPERATOR, kind, - "Only operator-style expressions are made with mkExpr(); " - "to make variables and constants, see mkVar(), mkBoundVar(), " - "and mkConst()."); - CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind, - "Exprs with kind %s must have at least %u children and " - "at most %u children (the one under construction has %u)", - kind::kindToString(kind).c_str(), - minArity(kind), maxArity(kind), n); + PrettyCheckArgument( + mk == kind::metakind::PARAMETERIZED || + mk == kind::metakind::OPERATOR, kind, + "Only operator-style expressions are made with mkExpr(); " + "to make variables and constants, see mkVar(), mkBoundVar(), " + "and mkConst()."); + PrettyCheckArgument( + n >= minArity(kind) && n <= maxArity(kind), kind, + "Exprs with kind %s must have at least %u children and " + "at most %u children (the one under construction has %u)", + kind::kindToString(kind).c_str(), + minArity(kind), maxArity(kind), n); NodeManagerScope nms(d_nodeManager); try { INC_STAT(kind); @@ -236,16 +242,18 @@ Expr ExprManager::mkExpr(Kind kind, Expr child1, Expr child2, Expr child3, Expr child4) { const kind::MetaKind mk = kind::metaKindOf(kind); const unsigned n = 4 - (mk == kind::metakind::PARAMETERIZED ? 1 : 0); - CheckArgument(mk == kind::metakind::PARAMETERIZED || - mk == kind::metakind::OPERATOR, kind, - "Only operator-style expressions are made with mkExpr(); " - "to make variables and constants, see mkVar(), mkBoundVar(), " - "and mkConst()."); - CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind, - "Exprs with kind %s must have at least %u children and " - "at most %u children (the one under construction has %u)", - kind::kindToString(kind).c_str(), - minArity(kind), maxArity(kind), n); + PrettyCheckArgument( + mk == kind::metakind::PARAMETERIZED || + mk == kind::metakind::OPERATOR, kind, + "Only operator-style expressions are made with mkExpr(); " + "to make variables and constants, see mkVar(), mkBoundVar(), " + "and mkConst()."); + PrettyCheckArgument( + n >= minArity(kind) && n <= maxArity(kind), kind, + "Exprs with kind %s must have at least %u children and " + "at most %u children (the one under construction has %u)", + kind::kindToString(kind).c_str(), + minArity(kind), maxArity(kind), n); NodeManagerScope nms(d_nodeManager); try { INC_STAT(kind); @@ -263,16 +271,18 @@ Expr ExprManager::mkExpr(Kind kind, Expr child1, Expr child2, Expr child3, Expr child4, Expr child5) { const kind::MetaKind mk = kind::metaKindOf(kind); const unsigned n = 5 - (mk == kind::metakind::PARAMETERIZED ? 1 : 0); - CheckArgument(mk == kind::metakind::PARAMETERIZED || - mk == kind::metakind::OPERATOR, kind, - "Only operator-style expressions are made with mkExpr(); " - "to make variables and constants, see mkVar(), mkBoundVar(), " - "and mkConst()."); - CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind, - "Exprs with kind %s must have at least %u children and " - "at most %u children (the one under construction has %u)", - kind::kindToString(kind).c_str(), - minArity(kind), maxArity(kind), n); + PrettyCheckArgument( + mk == kind::metakind::PARAMETERIZED || + mk == kind::metakind::OPERATOR, kind, + "Only operator-style expressions are made with mkExpr(); " + "to make variables and constants, see mkVar(), mkBoundVar(), " + "and mkConst()."); + PrettyCheckArgument( + n >= minArity(kind) && n <= maxArity(kind), kind, + "Exprs with kind %s must have at least %u children and " + "at most %u children (the one under construction has %u)", + kind::kindToString(kind).c_str(), + minArity(kind), maxArity(kind), n); NodeManagerScope nms(d_nodeManager); try { INC_STAT(kind); @@ -290,16 +300,18 @@ Expr ExprManager::mkExpr(Kind kind, Expr child1, Expr child2, Expr child3, Expr ExprManager::mkExpr(Kind kind, const std::vector<Expr>& children) { const kind::MetaKind mk = kind::metaKindOf(kind); const unsigned n = children.size() - (mk == kind::metakind::PARAMETERIZED ? 1 : 0); - CheckArgument(mk == kind::metakind::PARAMETERIZED || - mk == kind::metakind::OPERATOR, kind, - "Only operator-style expressions are made with mkExpr(); " - "to make variables and constants, see mkVar(), mkBoundVar(), " - "and mkConst()."); - CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind, - "Exprs with kind %s must have at least %u children and " - "at most %u children (the one under construction has %u)", - kind::kindToString(kind).c_str(), - minArity(kind), maxArity(kind), n); + PrettyCheckArgument( + mk == kind::metakind::PARAMETERIZED || + mk == kind::metakind::OPERATOR, kind, + "Only operator-style expressions are made with mkExpr(); " + "to make variables and constants, see mkVar(), mkBoundVar(), " + "and mkConst()."); + PrettyCheckArgument( + n >= minArity(kind) && n <= maxArity(kind), kind, + "Exprs with kind %s must have at least %u children and " + "at most %u children (the one under construction has %u)", + kind::kindToString(kind).c_str(), + minArity(kind), maxArity(kind), n); NodeManagerScope nms(d_nodeManager); @@ -321,17 +333,20 @@ Expr ExprManager::mkExpr(Kind kind, const std::vector<Expr>& children) { Expr ExprManager::mkExpr(Kind kind, Expr child1, const std::vector<Expr>& otherChildren) { const kind::MetaKind mk = kind::metaKindOf(kind); - const unsigned n = otherChildren.size() - (mk == kind::metakind::PARAMETERIZED ? 1 : 0) + 1; - CheckArgument(mk == kind::metakind::PARAMETERIZED || - mk == kind::metakind::OPERATOR, kind, - "Only operator-style expressions are made with mkExpr(); " - "to make variables and constants, see mkVar(), mkBoundVar(), " - "and mkConst()."); - CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind, - "Exprs with kind %s must have at least %u children and " - "at most %u children (the one under construction has %u)", - kind::kindToString(kind).c_str(), - minArity(kind), maxArity(kind), n); + const unsigned n = + otherChildren.size() - (mk == kind::metakind::PARAMETERIZED ? 1 : 0) + 1; + PrettyCheckArgument( + mk == kind::metakind::PARAMETERIZED || + mk == kind::metakind::OPERATOR, kind, + "Only operator-style expressions are made with mkExpr(); " + "to make variables and constants, see mkVar(), mkBoundVar(), " + "and mkConst()."); + PrettyCheckArgument( + n >= minArity(kind) && n <= maxArity(kind), kind, + "Exprs with kind %s must have at least %u children and " + "at most %u children (the one under construction has %u)", + kind::kindToString(kind).c_str(), + minArity(kind), maxArity(kind), n); NodeManagerScope nms(d_nodeManager); @@ -355,13 +370,16 @@ Expr ExprManager::mkExpr(Kind kind, Expr child1, Expr ExprManager::mkExpr(Expr opExpr) { const unsigned n = 0; Kind kind = NodeManager::operatorToKind(opExpr.getNode()); - CheckArgument(opExpr.getKind() == kind::BUILTIN || kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED, opExpr, - "This Expr constructor is for parameterized kinds only"); - CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind, - "Exprs with kind %s must have at least %u children and " - "at most %u children (the one under construction has %u)", - kind::kindToString(kind).c_str(), - minArity(kind), maxArity(kind), n); + PrettyCheckArgument( + opExpr.getKind() == kind::BUILTIN || + kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED, opExpr, + "This Expr constructor is for parameterized kinds only"); + PrettyCheckArgument( + n >= minArity(kind) && n <= maxArity(kind), kind, + "Exprs with kind %s must have at least %u children and " + "at most %u children (the one under construction has %u)", + kind::kindToString(kind).c_str(), + minArity(kind), maxArity(kind), n); NodeManagerScope nms(d_nodeManager); try { INC_STAT(kind); @@ -374,13 +392,16 @@ Expr ExprManager::mkExpr(Expr opExpr) { Expr ExprManager::mkExpr(Expr opExpr, Expr child1) { const unsigned n = 1; Kind kind = NodeManager::operatorToKind(opExpr.getNode()); - CheckArgument(opExpr.getKind() == kind::BUILTIN || kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED, opExpr, - "This Expr constructor is for parameterized kinds only"); - CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind, - "Exprs with kind %s must have at least %u children and " - "at most %u children (the one under construction has %u)", - kind::kindToString(kind).c_str(), - minArity(kind), maxArity(kind), n); + PrettyCheckArgument( + (opExpr.getKind() == kind::BUILTIN || + kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED), opExpr, + "This Expr constructor is for parameterized kinds only"); + PrettyCheckArgument( + n >= minArity(kind) && n <= maxArity(kind), kind, + "Exprs with kind %s must have at least %u children and " + "at most %u children (the one under construction has %u)", + kind::kindToString(kind).c_str(), + minArity(kind), maxArity(kind), n); NodeManagerScope nms(d_nodeManager); try { INC_STAT(kind); @@ -393,13 +414,16 @@ Expr ExprManager::mkExpr(Expr opExpr, Expr child1) { Expr ExprManager::mkExpr(Expr opExpr, Expr child1, Expr child2) { const unsigned n = 2; Kind kind = NodeManager::operatorToKind(opExpr.getNode()); - CheckArgument(opExpr.getKind() == kind::BUILTIN || kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED, opExpr, - "This Expr constructor is for parameterized kinds only"); - CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind, - "Exprs with kind %s must have at least %u children and " - "at most %u children (the one under construction has %u)", - kind::kindToString(kind).c_str(), - minArity(kind), maxArity(kind), n); + PrettyCheckArgument( + (opExpr.getKind() == kind::BUILTIN || + kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED), opExpr, + "This Expr constructor is for parameterized kinds only"); + PrettyCheckArgument( + n >= minArity(kind) && n <= maxArity(kind), kind, + "Exprs with kind %s must have at least %u children and " + "at most %u children (the one under construction has %u)", + kind::kindToString(kind).c_str(), + minArity(kind), maxArity(kind), n); NodeManagerScope nms(d_nodeManager); try { INC_STAT(kind); @@ -414,9 +438,11 @@ Expr ExprManager::mkExpr(Expr opExpr, Expr child1, Expr child2) { Expr ExprManager::mkExpr(Expr opExpr, Expr child1, Expr child2, Expr child3) { const unsigned n = 3; Kind kind = NodeManager::operatorToKind(opExpr.getNode()); - CheckArgument(opExpr.getKind() == kind::BUILTIN || kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED, opExpr, + PrettyCheckArgument( + (opExpr.getKind() == kind::BUILTIN || + kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED), opExpr, "This Expr constructor is for parameterized kinds only"); - CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind, + PrettyCheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind, "Exprs with kind %s must have at least %u children and " "at most %u children (the one under construction has %u)", kind::kindToString(kind).c_str(), @@ -437,13 +463,18 @@ Expr ExprManager::mkExpr(Expr opExpr, Expr child1, Expr child2, Expr child3, Expr child4) { const unsigned n = 4; Kind kind = NodeManager::operatorToKind(opExpr.getNode()); - CheckArgument(opExpr.getKind() == kind::BUILTIN || kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED, opExpr, - "This Expr constructor is for parameterized kinds only"); - CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind, - "Exprs with kind %s must have at least %u children and " - "at most %u children (the one under construction has %u)", - kind::kindToString(kind).c_str(), - minArity(kind), maxArity(kind), n); + PrettyCheckArgument( + (opExpr.getKind() == kind::BUILTIN || + kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED), opExpr, + "This Expr constructor is for parameterized kinds only"); + + PrettyCheckArgument( + n >= minArity(kind) && n <= maxArity(kind), kind, + "Exprs with kind %s must have at least %u children and " + "at most %u children (the one under construction has %u)", + kind::kindToString(kind).c_str(), + minArity(kind), maxArity(kind), n); + NodeManagerScope nms(d_nodeManager); try { INC_STAT(kind); @@ -461,13 +492,16 @@ Expr ExprManager::mkExpr(Expr opExpr, Expr child1, Expr child2, Expr child3, Expr child4, Expr child5) { const unsigned n = 5; Kind kind = NodeManager::operatorToKind(opExpr.getNode()); - CheckArgument(opExpr.getKind() == kind::BUILTIN || kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED, opExpr, - "This Expr constructor is for parameterized kinds only"); - CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind, - "Exprs with kind %s must have at least %u children and " - "at most %u children (the one under construction has %u)", - kind::kindToString(kind).c_str(), - minArity(kind), maxArity(kind), n); + PrettyCheckArgument( + (opExpr.getKind() == kind::BUILTIN || + kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED), opExpr, + "This Expr constructor is for parameterized kinds only"); + PrettyCheckArgument( + n >= minArity(kind) && n <= maxArity(kind), kind, + "Exprs with kind %s must have at least %u children and " + "at most %u children (the one under construction has %u)", + kind::kindToString(kind).c_str(), + minArity(kind), maxArity(kind), n); NodeManagerScope nms(d_nodeManager); try { INC_STAT(kind); @@ -485,13 +519,16 @@ Expr ExprManager::mkExpr(Expr opExpr, Expr child1, Expr child2, Expr child3, Expr ExprManager::mkExpr(Expr opExpr, const std::vector<Expr>& children) { const unsigned n = children.size(); Kind kind = NodeManager::operatorToKind(opExpr.getNode()); - CheckArgument(opExpr.getKind() == kind::BUILTIN || kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED, opExpr, - "This Expr constructor is for parameterized kinds only"); - CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind, - "Exprs with kind %s must have at least %u children and " - "at most %u children (the one under construction has %u)", - kind::kindToString(kind).c_str(), - minArity(kind), maxArity(kind), n); + PrettyCheckArgument( + (opExpr.getKind() == kind::BUILTIN || + kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED), opExpr, + "This Expr constructor is for parameterized kinds only"); + PrettyCheckArgument( + n >= minArity(kind) && n <= maxArity(kind), kind, + "Exprs with kind %s must have at least %u children and " + "at most %u children (the one under construction has %u)", + kind::kindToString(kind).c_str(), + minArity(kind), maxArity(kind), n); NodeManagerScope nms(d_nodeManager); @@ -652,11 +689,12 @@ ExprManager::mkMutualDatatypeTypes(const std::vector<Datatype>& datatypes, } Type type(d_nodeManager, typeNode); DatatypeType dtt(type); - CheckArgument(nameResolutions.find((*i).getName()) == nameResolutions.end(), - datatypes, - "cannot construct two datatypes at the same time " - "with the same name `%s'", - (*i).getName().c_str()); + PrettyCheckArgument( + nameResolutions.find((*i).getName()) == nameResolutions.end(), + datatypes, + "cannot construct two datatypes at the same time " + "with the same name `%s'", + (*i).getName().c_str()); nameResolutions.insert(std::make_pair((*i).getName(), dtt)); dtts.push_back(dtt); } @@ -687,10 +725,11 @@ ExprManager::mkMutualDatatypeTypes(const std::vector<Datatype>& datatypes, } std::map<std::string, DatatypeType>::const_iterator resolver = nameResolutions.find(name); - CheckArgument(resolver != nameResolutions.end(), - unresolvedTypes, - "cannot resolve type `%s'; it's not among " - "the datatypes being defined", name.c_str()); + PrettyCheckArgument( + resolver != nameResolutions.end(), + unresolvedTypes, + "cannot resolve type `%s'; it's not among " + "the datatypes being defined", name.c_str()); // We will instruct the Datatype to substitute "*i" (the // unresolved SortType used as a placeholder in complex types) // with "(*resolver).second" (the DatatypeType we created in the @@ -902,9 +941,10 @@ Expr ExprManager::mkBoundVar(Type type) { Expr ExprManager::mkAssociative(Kind kind, const std::vector<Expr>& children) { - CheckArgument( kind::isAssociative(kind), kind, - "Illegal kind in mkAssociative: %s", - kind::kindToString(kind).c_str()); + PrettyCheckArgument( + kind::isAssociative(kind), kind, + "Illegal kind in mkAssociative: %s", + kind::kindToString(kind).c_str()); NodeManagerScope nms(d_nodeManager); const unsigned int max = maxArity(kind); diff --git a/src/expr/expr_template.cpp b/src/expr/expr_template.cpp index dbd7c049b..dfbe179be 100644 --- a/src/expr/expr_template.cpp +++ b/src/expr/expr_template.cpp @@ -13,18 +13,18 @@ ** ** Public-facing expression interface, implementation. **/ +#include "expr/expr.h" + +#include <iterator> +#include <utility> +#include <vector> #include "base/cvc4_assert.h" -#include "expr/expr.h" #include "expr/node.h" #include "expr/expr_manager_scope.h" #include "expr/variable_type_map.h" #include "expr/node_manager_attributes.h" -#include <vector> -#include <iterator> -#include <utility> - ${includes} // This is a hack, but an important one: if there's an error, the @@ -326,15 +326,16 @@ bool Expr::hasOperator() const { Expr Expr::getOperator() const { ExprManagerScope ems(*this); Assert(d_node != NULL, "Unexpected NULL expression pointer!"); - CheckArgument(d_node->hasOperator(), *this, - "Expr::getOperator() called on an Expr with no operator"); + PrettyCheckArgument(d_node->hasOperator(), *this, + "Expr::getOperator() called on an Expr with no operator"); return Expr(d_exprManager, new Node(d_node->getOperator())); } Type Expr::getType(bool check) const throw (TypeCheckingException) { ExprManagerScope ems(*this); Assert(d_node != NULL, "Unexpected NULL expression pointer!"); - CheckArgument(!d_node->isNull(), this, "Can't get type of null expression!"); + PrettyCheckArgument(!d_node->isNull(), this, + "Can't get type of null expression!"); return d_exprManager->getType(*this, check); } @@ -509,40 +510,40 @@ Expr Expr::notExpr() const { Expr Expr::andExpr(const Expr& e) const { Assert(d_exprManager != NULL, "Don't have an expression manager for this expression!"); - CheckArgument(d_exprManager == e.d_exprManager, e, - "Different expression managers!"); + PrettyCheckArgument(d_exprManager == e.d_exprManager, e, + "Different expression managers!"); return d_exprManager->mkExpr(AND, *this, e); } Expr Expr::orExpr(const Expr& e) const { Assert(d_exprManager != NULL, "Don't have an expression manager for this expression!"); - CheckArgument(d_exprManager == e.d_exprManager, e, - "Different expression managers!"); + PrettyCheckArgument(d_exprManager == e.d_exprManager, e, + "Different expression managers!"); return d_exprManager->mkExpr(OR, *this, e); } Expr Expr::xorExpr(const Expr& e) const { Assert(d_exprManager != NULL, "Don't have an expression manager for this expression!"); - CheckArgument(d_exprManager == e.d_exprManager, e, - "Different expression managers!"); + PrettyCheckArgument(d_exprManager == e.d_exprManager, e, + "Different expression managers!"); return d_exprManager->mkExpr(XOR, *this, e); } Expr Expr::iffExpr(const Expr& e) const { Assert(d_exprManager != NULL, "Don't have an expression manager for this expression!"); - CheckArgument(d_exprManager == e.d_exprManager, e, - "Different expression managers!"); + PrettyCheckArgument(d_exprManager == e.d_exprManager, e, + "Different expression managers!"); return d_exprManager->mkExpr(IFF, *this, e); } Expr Expr::impExpr(const Expr& e) const { Assert(d_exprManager != NULL, "Don't have an expression manager for this expression!"); - CheckArgument(d_exprManager == e.d_exprManager, e, - "Different expression managers!"); + PrettyCheckArgument(d_exprManager == e.d_exprManager, e, + "Different expression managers!"); return d_exprManager->mkExpr(IMPLIES, *this, e); } @@ -550,10 +551,10 @@ Expr Expr::iteExpr(const Expr& then_e, const Expr& else_e) const { Assert(d_exprManager != NULL, "Don't have an expression manager for this expression!"); - CheckArgument(d_exprManager == then_e.d_exprManager, then_e, - "Different expression managers!"); - CheckArgument(d_exprManager == else_e.d_exprManager, else_e, - "Different expression managers!"); + PrettyCheckArgument(d_exprManager == then_e.d_exprManager, then_e, + "Different expression managers!"); + PrettyCheckArgument(d_exprManager == else_e.d_exprManager, else_e, + "Different expression managers!"); return d_exprManager->mkExpr(ITE, *this, then_e, else_e); } diff --git a/src/expr/kind_map.h b/src/expr/kind_map.h index d3ed43e1c..02e9728f0 100644 --- a/src/expr/kind_map.h +++ b/src/expr/kind_map.h @@ -23,6 +23,7 @@ #include <stdint.h> #include <iterator> +#include "base/cvc4_assert.h" #include "expr/kind.h" namespace CVC4 { diff --git a/src/expr/kind_template.h b/src/expr/kind_template.h index c2ccb6b5e..799d1ac33 100644 --- a/src/expr/kind_template.h +++ b/src/expr/kind_template.h @@ -19,7 +19,7 @@ #ifndef __CVC4__KIND_H #define __CVC4__KIND_H -#include <iostream> +#include <iosfwd> #include <sstream> #include "base/exception.h" diff --git a/src/expr/matcher.h b/src/expr/matcher.h index 92b1ce109..8cb092a64 100644 --- a/src/expr/matcher.h +++ b/src/expr/matcher.h @@ -19,7 +19,7 @@ #ifndef __CVC4__MATCHER_H #define __CVC4__MATCHER_H -#include <iostream> +#include <iosfwd> #include <string> #include <vector> #include <map> diff --git a/src/expr/mkexpr b/src/expr/mkexpr index 068063c05..4717b611d 100755 --- a/src/expr/mkexpr +++ b/src/expr/mkexpr @@ -239,7 +239,7 @@ template <> $2 const & Expr::getConst< $2 >() const; #line $lineno \"$kf\" template <> $2 const & Expr::getConst() const { #line $lineno \"$kf\" - CheckArgument(getKind() == ::CVC4::kind::$1, *this, \"Improper kind for getConst<$2>()\"); + PrettyCheckArgument(getKind() == ::CVC4::kind::$1, *this, \"Improper kind for getConst<$2>()\"); #line $lineno \"$kf\" return d_node->getConst< $2 >(); } diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp index 17524a3c0..c9e6866d4 100644 --- a/src/expr/node_manager.cpp +++ b/src/expr/node_manager.cpp @@ -393,8 +393,8 @@ TypeNode NodeManager::mkConstructorType(const DatatypeConstructor& constructor, sorts.push_back(sort); } Debug("datatypes") << "ctor range: " << range << endl; - CheckArgument(!range.isFunctionLike(), range, - "cannot create higher-order function types"); + PrettyCheckArgument(!range.isFunctionLike(), range, + "cannot create higher-order function types"); sorts.push_back(range); return mkTypeNode(kind::CONSTRUCTOR_TYPE, sorts); } diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index 390af8967..870408939 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -1098,7 +1098,8 @@ inline TypeNode NodeManager::mkArrayType(TypeNode indexType, "cannot index arrays by a function-like type"); CheckArgument(!constituentType.isFunctionLike(), constituentType, "cannot store function-like types in arrays"); - Debug("arrays") << "making array type " << indexType << " " << constituentType << std::endl; + Debug("arrays") << "making array type " << indexType << " " + << constituentType << std::endl; return mkTypeNode(kind::ARRAY_TYPE, indexType, constituentType); } diff --git a/src/expr/predicate.cpp b/src/expr/predicate.cpp index a4dd29592..5ccc3484a 100644 --- a/src/expr/predicate.cpp +++ b/src/expr/predicate.cpp @@ -34,9 +34,11 @@ Predicate::Predicate(const Expr& e) throw(IllegalArgumentException) : d_predicate(new Expr(e)) , d_witness(new Expr()) { - CheckArgument(! e.isNull(), e, "Predicate cannot be null"); - CheckArgument(e.getType().isPredicate(), e, "Expression given is not predicate"); - CheckArgument(FunctionType(e.getType()).getArgTypes().size() == 1, e, "Expression given is not predicate of a single argument"); + PrettyCheckArgument(! e.isNull(), e, "Predicate cannot be null"); + PrettyCheckArgument(e.getType().isPredicate(), e, + "Expression given is not predicate"); + PrettyCheckArgument(FunctionType(e.getType()).getArgTypes().size() == 1, e, + "Expression given is not predicate of a single argument"); } Predicate::Predicate(const Expr& e, const Expr& w) @@ -44,9 +46,11 @@ Predicate::Predicate(const Expr& e, const Expr& w) : d_predicate(new Expr(e)) , d_witness(new Expr(w)) { - CheckArgument(! e.isNull(), e, "Predicate cannot be null"); - CheckArgument(e.getType().isPredicate(), e, "Expression given is not predicate"); - CheckArgument(FunctionType(e.getType()).getArgTypes().size() == 1, e, "Expression given is not predicate of a single argument"); + PrettyCheckArgument(! e.isNull(), e, "Predicate cannot be null"); + PrettyCheckArgument(e.getType().isPredicate(), e, + "Expression given is not predicate"); + PrettyCheckArgument(FunctionType(e.getType()).getArgTypes().size() == 1, e, + "Expression given is not predicate of a single argument"); } Predicate::~Predicate() { diff --git a/src/expr/record.cpp b/src/expr/record.cpp index 2dee03dbf..ec5ef96f1 100644 --- a/src/expr/record.cpp +++ b/src/expr/record.cpp @@ -68,8 +68,9 @@ bool Record::contains(const std::string& name) const { size_t Record::getIndex(std::string name) const { FieldVector::const_iterator i = find(*d_fields, name); - CheckArgument(i != d_fields->end(), name, - "requested field `%s' does not exist in record", name.c_str()); + PrettyCheckArgument(i != d_fields->end(), name, + "requested field `%s' does not exist in record", + name.c_str()); return i - d_fields->begin(); } @@ -115,7 +116,8 @@ std::ostream& operator<<(std::ostream& out, const RecordUpdate& t) { const std::pair<std::string, Type>& Record::operator[](size_t index) const { - CheckArgument(index < d_fields->size(), index, "index out of bounds for record type"); + PrettyCheckArgument(index < d_fields->size(), index, + "index out of bounds for record type"); return (*d_fields)[index]; } diff --git a/src/expr/result.cpp b/src/expr/result.cpp index 95e382b98..aeb62b0c3 100644 --- a/src/expr/result.cpp +++ b/src/expr/result.cpp @@ -29,6 +29,62 @@ using namespace std; namespace CVC4 { +Result::Result() + : d_sat(SAT_UNKNOWN) + , d_validity(VALIDITY_UNKNOWN) + , d_which(TYPE_NONE) + , d_unknownExplanation(UNKNOWN_REASON) + , d_inputName("") +{ } + + +Result::Result(enum Sat s, std::string inputName) + : d_sat(s) + , d_validity(VALIDITY_UNKNOWN) + , d_which(TYPE_SAT) + , d_unknownExplanation(UNKNOWN_REASON) + , d_inputName(inputName) +{ + PrettyCheckArgument(s != SAT_UNKNOWN, + "Must provide a reason for satisfiability being unknown"); +} + +Result::Result(enum Validity v, std::string inputName) + : d_sat(SAT_UNKNOWN) + , d_validity(v) + , d_which(TYPE_VALIDITY) + , d_unknownExplanation(UNKNOWN_REASON) + , d_inputName(inputName) +{ + PrettyCheckArgument(v != VALIDITY_UNKNOWN, + "Must provide a reason for validity being unknown"); +} + + +Result::Result(enum Sat s, enum UnknownExplanation unknownExplanation, + std::string inputName) + : d_sat(s) + , d_validity(VALIDITY_UNKNOWN) + , d_which(TYPE_SAT) + , d_unknownExplanation(unknownExplanation) + , d_inputName(inputName) +{ + PrettyCheckArgument(s == SAT_UNKNOWN, + "improper use of unknown-result constructor"); +} + +Result::Result(enum Validity v, enum UnknownExplanation unknownExplanation, + std::string inputName) + : d_sat(SAT_UNKNOWN) + , d_validity(v) + , d_which(TYPE_VALIDITY) + , d_unknownExplanation(unknownExplanation) + , d_inputName(inputName) +{ + PrettyCheckArgument(v == VALIDITY_UNKNOWN, + "improper use of unknown-result constructor"); +} + Result::Result(const std::string& instr, std::string inputName) : d_sat(SAT_UNKNOWN), d_validity(VALIDITY_UNKNOWN), @@ -78,6 +134,13 @@ Result::Result(const std::string& instr, std::string inputName) : } } +Result::UnknownExplanation Result::whyUnknown() const { + PrettyCheckArgument( isUnknown(), this, + "This result is not unknown, so the reason for " + "being unknown cannot be inquired of it" ); + return d_unknownExplanation; +} + bool Result::operator==(const Result& r) const throw() { if(d_which != r.d_which) { return false; diff --git a/src/expr/result.h b/src/expr/result.h index 74697eba6..8069f7ef9 100644 --- a/src/expr/result.h +++ b/src/expr/result.h @@ -75,49 +75,20 @@ private: std::string d_inputName; public: - Result() : - d_sat(SAT_UNKNOWN), - d_validity(VALIDITY_UNKNOWN), - d_which(TYPE_NONE), - d_unknownExplanation(UNKNOWN_REASON), - d_inputName("") { - } - Result(enum Sat s, std::string inputName = "") : - d_sat(s), - d_validity(VALIDITY_UNKNOWN), - d_which(TYPE_SAT), - d_unknownExplanation(UNKNOWN_REASON), - d_inputName(inputName) { - CheckArgument(s != SAT_UNKNOWN, - "Must provide a reason for satisfiability being unknown"); - } - Result(enum Validity v, std::string inputName = "") : - d_sat(SAT_UNKNOWN), - d_validity(v), - d_which(TYPE_VALIDITY), - d_unknownExplanation(UNKNOWN_REASON), - d_inputName(inputName) { - CheckArgument(v != VALIDITY_UNKNOWN, - "Must provide a reason for validity being unknown"); - } - Result(enum Sat s, enum UnknownExplanation unknownExplanation, std::string inputName = "") : - d_sat(s), - d_validity(VALIDITY_UNKNOWN), - d_which(TYPE_SAT), - d_unknownExplanation(unknownExplanation), - d_inputName(inputName) { - CheckArgument(s == SAT_UNKNOWN, - "improper use of unknown-result constructor"); - } - Result(enum Validity v, enum UnknownExplanation unknownExplanation, std::string inputName = "") : - d_sat(SAT_UNKNOWN), - d_validity(v), - d_which(TYPE_VALIDITY), - d_unknownExplanation(unknownExplanation), - d_inputName(inputName) { - CheckArgument(v == VALIDITY_UNKNOWN, - "improper use of unknown-result constructor"); - } + + Result(); + + Result(enum Sat s, std::string inputName = ""); + + Result(enum Validity v, std::string inputName = ""); + + Result(enum Sat s, + enum UnknownExplanation unknownExplanation, + std::string inputName = ""); + + Result(enum Validity v, enum UnknownExplanation unknownExplanation, + std::string inputName = ""); + Result(const std::string& s, std::string inputName = ""); Result(const Result& r, std::string inputName) { @@ -128,24 +99,24 @@ public: enum Sat isSat() const { return d_which == TYPE_SAT ? d_sat : SAT_UNKNOWN; } + enum Validity isValid() const { return d_which == TYPE_VALIDITY ? d_validity : VALIDITY_UNKNOWN; } + bool isUnknown() const { return isSat() == SAT_UNKNOWN && isValid() == VALIDITY_UNKNOWN; } + Type getType() const { return d_which; } + bool isNull() const { return d_which == TYPE_NONE; } - enum UnknownExplanation whyUnknown() const { - CheckArgument( isUnknown(), this, - "This result is not unknown, so the reason for " - "being unknown cannot be inquired of it" ); - return d_unknownExplanation; - } + + enum UnknownExplanation whyUnknown() const; bool operator==(const Result& r) const throw(); inline bool operator!=(const Result& r) const throw(); diff --git a/src/expr/sexpr.cpp b/src/expr/sexpr.cpp index 0c0828616..69741859f 100644 --- a/src/expr/sexpr.cpp +++ b/src/expr/sexpr.cpp @@ -311,7 +311,7 @@ bool SExpr::languageQuotesKeywords(OutputLanguage language) { std::string SExpr::getValue() const { - CheckArgument( isAtom(), this ); + PrettyCheckArgument( isAtom(), this ); switch(d_sexprType) { case SEXPR_INTEGER: return d_integerValue.toString(); @@ -335,17 +335,17 @@ std::string SExpr::getValue() const { } const CVC4::Integer& SExpr::getIntegerValue() const { - CheckArgument( isInteger(), this ); + PrettyCheckArgument( isInteger(), this ); return d_integerValue; } const CVC4::Rational& SExpr::getRationalValue() const { - CheckArgument( isRational(), this ); + PrettyCheckArgument( isRational(), this ); return d_rationalValue; } const std::vector<SExpr>& SExpr::getChildren() const { - CheckArgument( !isAtom(), this ); + PrettyCheckArgument( !isAtom(), this ); Assert( d_children != NULL ); return *d_children; } diff --git a/src/expr/statistics_registry.cpp b/src/expr/statistics_registry.cpp index c1db992c5..bf36236f7 100644 --- a/src/expr/statistics_registry.cpp +++ b/src/expr/statistics_registry.cpp @@ -17,6 +17,7 @@ #include "expr/statistics_registry.h" +#include "base/cvc4_assert.h" #include "expr/expr_manager.h" #include "lib/clock_gettime.h" #include "smt/smt_engine.h" @@ -36,6 +37,19 @@ namespace CVC4 { +/** Construct a statistics registry */ +StatisticsRegistry::StatisticsRegistry(const std::string& name) + throw(CVC4::IllegalArgumentException) : + Stat(name) { + + d_prefix = name; + if(__CVC4_USE_STATISTICS) { + PrettyCheckArgument(d_name.find(s_regDelim) == std::string::npos, name, + "StatisticsRegistry names cannot contain the string \"%s\"", + s_regDelim.c_str()); + } +} + namespace stats { // This is a friend of SmtEngine, just to reach in and get it. @@ -60,9 +74,9 @@ StatisticsRegistry* StatisticsRegistry::current() { void StatisticsRegistry::registerStat(Stat* s) throw(CVC4::IllegalArgumentException) { #ifdef CVC4_STATISTICS_ON StatSet& stats = current()->d_stats; - CheckArgument(stats.find(s) == stats.end(), s, - "Statistic `%s' was already registered with this registry.", - s->getName().c_str()); + PrettyCheckArgument(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() */ @@ -70,7 +84,7 @@ void StatisticsRegistry::registerStat(Stat* s) throw(CVC4::IllegalArgumentExcept void StatisticsRegistry::unregisterStat(Stat* s) throw(CVC4::IllegalArgumentException) { #ifdef CVC4_STATISTICS_ON StatSet& stats = current()->d_stats; - CheckArgument(stats.find(s) != stats.end(), s, + PrettyCheckArgument(stats.find(s) != stats.end(), s, "Statistic `%s' was not registered with this registry.", s->getName().c_str()); stats.erase(s); @@ -81,14 +95,14 @@ void StatisticsRegistry::unregisterStat(Stat* s) throw(CVC4::IllegalArgumentExce void StatisticsRegistry::registerStat_(Stat* s) throw(CVC4::IllegalArgumentException) { #ifdef CVC4_STATISTICS_ON - CheckArgument(d_stats.find(s) == d_stats.end(), s); + PrettyCheckArgument(d_stats.find(s) == d_stats.end(), s); d_stats.insert(s); #endif /* CVC4_STATISTICS_ON */ }/* StatisticsRegistry::registerStat_() */ void StatisticsRegistry::unregisterStat_(Stat* s) throw(CVC4::IllegalArgumentException) { #ifdef CVC4_STATISTICS_ON - CheckArgument(d_stats.find(s) != d_stats.end(), s); + PrettyCheckArgument(d_stats.find(s) != d_stats.end(), s); d_stats.erase(s); #endif /* CVC4_STATISTICS_ON */ }/* StatisticsRegistry::unregisterStat_() */ @@ -107,7 +121,7 @@ void StatisticsRegistry::flushInformation(std::ostream &out) const { void TimerStat::start() { if(__CVC4_USE_STATISTICS) { - CheckArgument(!d_running, *this, "timer already running"); + PrettyCheckArgument(!d_running, *this, "timer already running"); clock_gettime(CLOCK_MONOTONIC, &d_start); d_running = true; } @@ -115,7 +129,7 @@ void TimerStat::start() { void TimerStat::stop() { if(__CVC4_USE_STATISTICS) { - CheckArgument(d_running, *this, "timer not running"); + PrettyCheckArgument(d_running, *this, "timer not running"); ::timespec end; clock_gettime(CLOCK_MONOTONIC, &end); d_data += end - d_start; diff --git a/src/expr/statistics_registry.h b/src/expr/statistics_registry.h index 89efe4021..4793f1301 100644 --- a/src/expr/statistics_registry.h +++ b/src/expr/statistics_registry.h @@ -607,15 +607,7 @@ public: /** Construct a statistics registry */ StatisticsRegistry(const std::string& name) - throw(CVC4::IllegalArgumentException) : - Stat(name) { - d_prefix = name; - if(__CVC4_USE_STATISTICS) { - CheckArgument(d_name.find(s_regDelim) == std::string::npos, name, - "StatisticsRegistry names cannot contain the string \"%s\"", - s_regDelim.c_str()); - } - } + throw(CVC4::IllegalArgumentException); /** * Set the name of this statistic registry, used as prefix during diff --git a/src/expr/symbol_table.cpp b/src/expr/symbol_table.cpp index 3d53f2e44..c0a80b7ce 100644 --- a/src/expr/symbol_table.cpp +++ b/src/expr/symbol_table.cpp @@ -17,17 +17,18 @@ **/ #include "expr/symbol_table.h" -#include "expr/expr.h" -#include "expr/type.h" -#include "expr/expr_manager_scope.h" + +#include <string> +#include <utility> + #include "context/cdhashmap.h" #include "context/cdhashset.h" #include "context/context.h" +#include "expr/expr.h" +#include "expr/expr_manager_scope.h" +#include "expr/type.h" -#include <string> -#include <utility> -using namespace CVC4; using namespace CVC4::context; using namespace std; @@ -49,7 +50,7 @@ SymbolTable::~SymbolTable() { void SymbolTable::bind(const std::string& name, Expr obj, bool levelZero) throw() { - CheckArgument(!obj.isNull(), obj, "cannot bind to a null Expr"); + PrettyCheckArgument(!obj.isNull(), obj, "cannot bind to a null Expr"); ExprManagerScope ems(obj); if(levelZero) d_exprMap->insertAtContextLevelZero(name, obj); else d_exprMap->insert(name, obj); @@ -57,7 +58,7 @@ void SymbolTable::bind(const std::string& name, Expr obj, void SymbolTable::bindDefinedFunction(const std::string& name, Expr obj, bool levelZero) throw() { - CheckArgument(!obj.isNull(), obj, "cannot bind to a null Expr"); + PrettyCheckArgument(!obj.isNull(), obj, "cannot bind to a null Expr"); ExprManagerScope ems(obj); if(levelZero){ d_exprMap->insertAtContextLevelZero(name, obj); @@ -121,7 +122,7 @@ bool SymbolTable::isBoundType(const std::string& name) const throw() { Type SymbolTable::lookupType(const std::string& name) const throw() { pair<vector<Type>, Type> p = (*d_typeMap->find(name)).second; - CheckArgument(p.first.size() == 0, name, + PrettyCheckArgument(p.first.size() == 0, name, "type constructor arity is wrong: " "`%s' requires %u parameters but was provided 0", name.c_str(), p.first.size()); @@ -131,12 +132,12 @@ Type SymbolTable::lookupType(const std::string& name) const throw() { Type SymbolTable::lookupType(const std::string& name, const std::vector<Type>& params) const throw() { pair<vector<Type>, Type> p = (*d_typeMap->find(name)).second; - CheckArgument(p.first.size() == params.size(), params, + PrettyCheckArgument(p.first.size() == params.size(), params, "type constructor arity is wrong: " "`%s' requires %u parameters but was provided %u", name.c_str(), p.first.size(), params.size()); if(p.first.size() == 0) { - CheckArgument(p.second.isSort(), name); + PrettyCheckArgument(p.second.isSort(), name.c_str()); return p.second; } if(p.second.isSortConstructor()) { @@ -161,7 +162,7 @@ Type SymbolTable::lookupType(const std::string& name, return instantiation; } else if(p.second.isDatatype()) { - CheckArgument(DatatypeType(p.second).isParametric(), name, "expected parametric datatype"); + PrettyCheckArgument(DatatypeType(p.second).isParametric(), name, "expected parametric datatype"); return DatatypeType(p.second).instantiate(params); } else { if(Debug.isOn("sort")) { diff --git a/src/expr/type.cpp b/src/expr/type.cpp index 327be72eb..99d04d658 100644 --- a/src/expr/type.cpp +++ b/src/expr/type.cpp @@ -92,8 +92,8 @@ Type Type::getBaseType() const { } Type& Type::operator=(const Type& t) { - CheckArgument(d_typeNode != NULL, this, "Unexpected NULL typenode pointer!"); - CheckArgument(t.d_typeNode != NULL, t, "Unexpected NULL typenode pointer!"); + PrettyCheckArgument(d_typeNode != NULL, this, "Unexpected NULL typenode pointer!"); + PrettyCheckArgument(t.d_typeNode != NULL, t, "Unexpected NULL typenode pointer!"); if(this != &t) { if(d_nodeManager == t.d_nodeManager) { @@ -354,7 +354,7 @@ vector<Type> FunctionType::getArgTypes() const { Type FunctionType::getRangeType() const { NodeManagerScope nms(d_nodeManager); - CheckArgument(isNull() || isFunction(), this); + PrettyCheckArgument(isNull() || isFunction(), this); return makeType(d_typeNode->getRangeType()); } @@ -430,112 +430,112 @@ SortType SortConstructorType::instantiate(const std::vector<Type>& params) const BooleanType::BooleanType(const Type& t) throw(IllegalArgumentException) : Type(t) { - CheckArgument(isNull() || isBoolean(), this); + PrettyCheckArgument(isNull() || isBoolean(), this); } IntegerType::IntegerType(const Type& t) throw(IllegalArgumentException) : Type(t) { - CheckArgument(isNull() || isInteger(), this); + PrettyCheckArgument(isNull() || isInteger(), this); } RealType::RealType(const Type& t) throw(IllegalArgumentException) : Type(t) { - CheckArgument(isNull() || isReal(), this); + PrettyCheckArgument(isNull() || isReal(), this); } StringType::StringType(const Type& t) throw(IllegalArgumentException) : Type(t) { - CheckArgument(isNull() || isString(), this); + PrettyCheckArgument(isNull() || isString(), this); } RoundingModeType::RoundingModeType(const Type& t) throw(IllegalArgumentException) : Type(t) { - CheckArgument(isNull() || isRoundingMode(), this); + PrettyCheckArgument(isNull() || isRoundingMode(), this); } BitVectorType::BitVectorType(const Type& t) throw(IllegalArgumentException) : Type(t) { - CheckArgument(isNull() || isBitVector(), this); + PrettyCheckArgument(isNull() || isBitVector(), this); } FloatingPointType::FloatingPointType(const Type& t) throw(IllegalArgumentException) : Type(t) { - CheckArgument(isNull() || isFloatingPoint(), this); + PrettyCheckArgument(isNull() || isFloatingPoint(), this); } DatatypeType::DatatypeType(const Type& t) throw(IllegalArgumentException) : Type(t) { - CheckArgument(isNull() || isDatatype(), this); + PrettyCheckArgument(isNull() || isDatatype(), this); } ConstructorType::ConstructorType(const Type& t) throw(IllegalArgumentException) : Type(t) { - CheckArgument(isNull() || isConstructor(), this); + PrettyCheckArgument(isNull() || isConstructor(), this); } SelectorType::SelectorType(const Type& t) throw(IllegalArgumentException) : Type(t) { - CheckArgument(isNull() || isSelector(), this); + PrettyCheckArgument(isNull() || isSelector(), this); } -TesterType::TesterType(const Type& t) throw(IllegalArgumentException) : - Type(t) { - CheckArgument(isNull() || isTester(), this); +TesterType::TesterType(const Type& t) throw(IllegalArgumentException) + : Type(t) { + PrettyCheckArgument(isNull() || isTester(), this); } -FunctionType::FunctionType(const Type& t) throw(IllegalArgumentException) : - Type(t) { - CheckArgument(isNull() || isFunction(), this); +FunctionType::FunctionType(const Type& t) throw(IllegalArgumentException) + : Type(t) { + PrettyCheckArgument(isNull() || isFunction(), this); } -TupleType::TupleType(const Type& t) throw(IllegalArgumentException) : - Type(t) { - CheckArgument(isNull() || isTuple(), this); +TupleType::TupleType(const Type& t) throw(IllegalArgumentException) + : Type(t) { + PrettyCheckArgument(isNull() || isTuple(), this); } -RecordType::RecordType(const Type& t) throw(IllegalArgumentException) : - Type(t) { - CheckArgument(isNull() || isRecord(), this); +RecordType::RecordType(const Type& t) throw(IllegalArgumentException) + : Type(t) { + PrettyCheckArgument(isNull() || isRecord(), this); } -SExprType::SExprType(const Type& t) throw(IllegalArgumentException) : - Type(t) { - CheckArgument(isNull() || isSExpr(), this); +SExprType::SExprType(const Type& t) throw(IllegalArgumentException) + : Type(t) { + PrettyCheckArgument(isNull() || isSExpr(), this); } -ArrayType::ArrayType(const Type& t) throw(IllegalArgumentException) : - Type(t) { - CheckArgument(isNull() || isArray(), this); +ArrayType::ArrayType(const Type& t) throw(IllegalArgumentException) + : Type(t) { + PrettyCheckArgument(isNull() || isArray(), this); } -SetType::SetType(const Type& t) throw(IllegalArgumentException) : - Type(t) { - CheckArgument(isNull() || isSet(), this); +SetType::SetType(const Type& t) throw(IllegalArgumentException) + : Type(t) { + PrettyCheckArgument(isNull() || isSet(), this); } -SortType::SortType(const Type& t) throw(IllegalArgumentException) : - Type(t) { - CheckArgument(isNull() || isSort(), this); +SortType::SortType(const Type& t) throw(IllegalArgumentException) + : Type(t) { + PrettyCheckArgument(isNull() || isSort(), this); } SortConstructorType::SortConstructorType(const Type& t) - throw(IllegalArgumentException) : - Type(t) { - CheckArgument(isNull() || isSortConstructor(), this); + throw(IllegalArgumentException) + : Type(t) { + PrettyCheckArgument(isNull() || isSortConstructor(), this); } /* - not in release 1.0 PredicateSubtype::PredicateSubtype(const Type& t) throw(IllegalArgumentException) : Type(t) { - CheckArgument(isNull() || isPredicateSubtype(), this); + PrettyCheckArgument(isNull() || isPredicateSubtype(), this); } */ SubrangeType::SubrangeType(const Type& t) throw(IllegalArgumentException) : Type(t) { - CheckArgument(isNull() || isSubrange(), this); + PrettyCheckArgument(isNull() || isSubrange(), this); } unsigned BitVectorType::getSize() const { @@ -585,7 +585,7 @@ std::vector<Type> ConstructorType::getArgTypes() const { const Datatype& DatatypeType::getDatatype() const { NodeManagerScope nms(d_nodeManager); if( d_typeNode->isParametricDatatype() ) { - CheckArgument( (*d_typeNode)[0].getKind() == kind::DATATYPE_TYPE, this); + PrettyCheckArgument( (*d_typeNode)[0].getKind() == kind::DATATYPE_TYPE, this); const Datatype& dt = (*d_typeNode)[0].getConst<Datatype>(); return dt; } else { diff --git a/src/expr/uninterpreted_constant.cpp b/src/expr/uninterpreted_constant.cpp index d41ab1045..97bc3ae4b 100644 --- a/src/expr/uninterpreted_constant.cpp +++ b/src/expr/uninterpreted_constant.cpp @@ -20,10 +20,20 @@ #include <sstream> #include <string> +#include "base/cvc4_assert.h" + using namespace std; namespace CVC4 { +UninterpretedConstant::UninterpretedConstant(Type type, Integer index) throw(IllegalArgumentException) + : d_type(type) + , d_index(index) +{ + //PrettyCheckArgument(type.isSort(), type, "uninterpreted constants can only be created for uninterpreted sorts, not `%s'", type.toString().c_str()); + PrettyCheckArgument(index >= 0, index, "index >= 0 required for uninterpreted constant index, not `%s'", index.toString().c_str()); +} + std::ostream& operator<<(std::ostream& out, const UninterpretedConstant& uc) { stringstream ss; ss << uc.getType(); diff --git a/src/expr/uninterpreted_constant.h b/src/expr/uninterpreted_constant.h index 13a80a19d..5b2293df6 100644 --- a/src/expr/uninterpreted_constant.h +++ b/src/expr/uninterpreted_constant.h @@ -18,26 +18,18 @@ #pragma once +#include <iosfwd> + #include "expr/type.h" -#include <iostream> namespace CVC4 { class CVC4_PUBLIC UninterpretedConstant { - const Type d_type; - const Integer d_index; - public: - UninterpretedConstant(Type type, Integer index) throw(IllegalArgumentException) : - d_type(type), - d_index(index) { - //CheckArgument(type.isSort(), type, "uninterpreted constants can only be created for uninterpreted sorts, not `%s'", type.toString().c_str()); - CheckArgument(index >= 0, index, "index >= 0 required for uninterpreted constant index, not `%s'", index.toString().c_str()); - } + UninterpretedConstant(Type type, Integer index) throw(IllegalArgumentException); - ~UninterpretedConstant() throw() { - } + ~UninterpretedConstant() throw() { } Type getType() const throw() { return d_type; @@ -68,6 +60,9 @@ public: return !(*this < uc); } +private: + const Type d_type; + const Integer d_index; };/* class UninterpretedConstant */ std::ostream& operator<<(std::ostream& out, const UninterpretedConstant& uc) CVC4_PUBLIC; diff --git a/src/main/command_executor.h b/src/main/command_executor.h index 49d18a153..8ef1a6a5f 100644 --- a/src/main/command_executor.h +++ b/src/main/command_executor.h @@ -15,7 +15,7 @@ #ifndef __CVC4__MAIN__COMMAND_EXECUTOR_H #define __CVC4__MAIN__COMMAND_EXECUTOR_H -#include <iostream> +#include <iosfwd> #include <string> #include "expr/expr_manager.h" diff --git a/src/main/command_executor_portfolio.h b/src/main/command_executor_portfolio.h index b3532cea4..ee2b270fb 100644 --- a/src/main/command_executor_portfolio.h +++ b/src/main/command_executor_portfolio.h @@ -21,10 +21,10 @@ #include "main/command_executor.h" #include "main/portfolio_util.h" -#include <vector> -#include <string> -#include <iostream> +#include <iosfwd> #include <sstream> +#include <string> +#include <vector> namespace CVC4 { diff --git a/src/main/interactive_shell.h b/src/main/interactive_shell.h index 1b1031776..844fddf45 100644 --- a/src/main/interactive_shell.h +++ b/src/main/interactive_shell.h @@ -15,7 +15,7 @@ #ifndef __CVC4__INTERACTIVE_SHELL_H #define __CVC4__INTERACTIVE_SHELL_H -#include <iostream> +#include <iosfwd> #include <string> #include "options/language.h" diff --git a/src/options/base_options b/src/options/base_options index 588220817..edbef801d 100644 --- a/src/options/base_options +++ b/src/options/base_options @@ -81,9 +81,9 @@ module BASE "options/base_options.h" Base option binary_name std::string -option in std::istream* :default &std::cin :include <iostream> -option out std::ostream* :default &std::cout :include <iostream> -option err std::ostream* :default &std::cerr :include <iostream> +option in std::istream* :default &std::cin :include <iosfwd> +option out std::ostream* :default &std::cout :include <iosfwd> +option err std::ostream* :default &std::cerr :include <iosfwd> common-option inputLanguage input-language -L --lang=LANG InputLanguage :handler CVC4::options::stringToInputLanguage :include "options/language.h" :default language::input::LANG_AUTO :read-write force input language (default is "auto"; see --lang help) diff --git a/src/options/boolean_term_conversion_mode.cpp b/src/options/boolean_term_conversion_mode.cpp index efeb3ab16..d1466ae14 100644 --- a/src/options/boolean_term_conversion_mode.cpp +++ b/src/options/boolean_term_conversion_mode.cpp @@ -18,7 +18,6 @@ #include <iostream> - namespace CVC4 { std::ostream& operator<<(std::ostream& out, theory::booleans::BooleanTermConversionMode mode) { diff --git a/src/options/boolean_term_conversion_mode.h b/src/options/boolean_term_conversion_mode.h index 5671dea13..65cc7a8a5 100644 --- a/src/options/boolean_term_conversion_mode.h +++ b/src/options/boolean_term_conversion_mode.h @@ -20,7 +20,7 @@ #ifndef __CVC4__THEORY__BOOLEANS__BOOLEAN_TERM_CONVERSION_MODE_H #define __CVC4__THEORY__BOOLEANS__BOOLEAN_TERM_CONVERSION_MODE_H -#include <iostream> +#include <iosfwd> namespace CVC4 { namespace theory { diff --git a/src/options/bv_bitblast_mode.cpp b/src/options/bv_bitblast_mode.cpp index 9576134f6..99ceb41ee 100644 --- a/src/options/bv_bitblast_mode.cpp +++ b/src/options/bv_bitblast_mode.cpp @@ -16,6 +16,8 @@ #include "options/bv_bitblast_mode.h" +#include <iostream> + namespace CVC4 { std::ostream& operator<<(std::ostream& out, theory::bv::BitblastMode mode) { diff --git a/src/options/bv_bitblast_mode.h b/src/options/bv_bitblast_mode.h index 89ecdc381..08a6e4077 100644 --- a/src/options/bv_bitblast_mode.h +++ b/src/options/bv_bitblast_mode.h @@ -19,7 +19,7 @@ #ifndef __CVC4__THEORY__BV__BITBLAST_MODE_H #define __CVC4__THEORY__BV__BITBLAST_MODE_H -#include <iostream> +#include <iosfwd> namespace CVC4 { namespace theory { diff --git a/src/options/options_handler_interface.cpp b/src/options/options_handler_interface.cpp index d803fced0..bce3643aa 100644 --- a/src/options/options_handler_interface.cpp +++ b/src/options/options_handler_interface.cpp @@ -44,313 +44,313 @@ static const char* s_third_argument_warning = // theory/arith/options_handlers.h ArithUnateLemmaMode stringToArithUnateLemmaMode(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException) { - CheckArgument(handler != NULL, handler, s_third_argument_warning); + PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning); return handler->stringToArithUnateLemmaMode(option, optarg); } ArithPropagationMode stringToArithPropagationMode(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException) { - CheckArgument(handler != NULL, handler, s_third_argument_warning); + PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning); return handler->stringToArithPropagationMode(option, optarg); } ErrorSelectionRule stringToErrorSelectionRule(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException) { - CheckArgument(handler != NULL, handler, s_third_argument_warning); + PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning); return handler->stringToErrorSelectionRule(option, optarg); } // theory/quantifiers/options_handlers.h theory::quantifiers::InstWhenMode stringToInstWhenMode(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException) { - CheckArgument(handler != NULL, handler, s_third_argument_warning); + PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning); return handler->stringToInstWhenMode(option, optarg); } void checkInstWhenMode(std::string option, theory::quantifiers::InstWhenMode mode, OptionsHandler* handler) throw(OptionException) { - CheckArgument(handler != NULL, handler, s_third_argument_warning); + PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning); handler->checkInstWhenMode(option, mode); } theory::quantifiers::LiteralMatchMode stringToLiteralMatchMode(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException) { - CheckArgument(handler != NULL, handler, s_third_argument_warning); + PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning); return handler->stringToLiteralMatchMode(option, optarg); } void checkLiteralMatchMode(std::string option, theory::quantifiers::LiteralMatchMode mode, OptionsHandler* handler) throw(OptionException) { - CheckArgument(handler != NULL, handler, s_third_argument_warning); + PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning); handler->checkLiteralMatchMode(option, mode); } theory::quantifiers::MbqiMode stringToMbqiMode(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException) { - CheckArgument(handler != NULL, handler, s_third_argument_warning); + PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning); return handler->stringToMbqiMode(option, optarg); } void checkMbqiMode(std::string option, theory::quantifiers::MbqiMode mode, OptionsHandler* handler) throw(OptionException) { - CheckArgument(handler != NULL, handler, s_third_argument_warning); + PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning); handler->checkMbqiMode(option, mode); } theory::quantifiers::QcfWhenMode stringToQcfWhenMode(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException) { - CheckArgument(handler != NULL, handler, s_third_argument_warning); + PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning); return handler->stringToQcfWhenMode(option, optarg); } theory::quantifiers::QcfMode stringToQcfMode(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException) { - CheckArgument(handler != NULL, handler, s_third_argument_warning); + PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning); return handler->stringToQcfMode(option, optarg); } theory::quantifiers::UserPatMode stringToUserPatMode(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException) { - CheckArgument(handler != NULL, handler, s_third_argument_warning); + PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning); return handler->stringToUserPatMode(option, optarg); } theory::quantifiers::TriggerSelMode stringToTriggerSelMode(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException) { - CheckArgument(handler != NULL, handler, s_third_argument_warning); + PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning); return handler->stringToTriggerSelMode(option, optarg); } theory::quantifiers::PrenexQuantMode stringToPrenexQuantMode(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException) { - CheckArgument(handler != NULL, handler, s_third_argument_warning); + PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning); return handler->stringToPrenexQuantMode(option, optarg); } theory::quantifiers::CegqiFairMode stringToCegqiFairMode(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException) { - CheckArgument(handler != NULL, handler, s_third_argument_warning); + PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning); return handler->stringToCegqiFairMode(option, optarg); } theory::quantifiers::TermDbMode stringToTermDbMode(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException) { - CheckArgument(handler != NULL, handler, s_third_argument_warning); + PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning); return handler-> stringToTermDbMode(option, optarg); } theory::quantifiers::IteLiftQuantMode stringToIteLiftQuantMode(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException) { - CheckArgument(handler != NULL, handler, s_third_argument_warning); + PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning); return handler->stringToIteLiftQuantMode(option, optarg); } theory::quantifiers::SygusInvTemplMode stringToSygusInvTemplMode(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException) { - CheckArgument(handler != NULL, handler, s_third_argument_warning); + PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning); return handler->stringToSygusInvTemplMode(option, optarg); } theory::quantifiers::MacrosQuantMode stringToMacrosQuantMode(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException) { - CheckArgument(handler != NULL, handler, s_third_argument_warning); + PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning); return handler->stringToMacrosQuantMode(option, optarg); } // theory/bv/options_handlers.h void abcEnabledBuild(std::string option, bool value, OptionsHandler* handler) throw(OptionException) { - CheckArgument(handler != NULL, handler, s_third_argument_warning); + PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning); handler->abcEnabledBuild(option, value); } void abcEnabledBuild(std::string option, std::string value, OptionsHandler* handler) throw(OptionException) { - CheckArgument(handler != NULL, handler, s_third_argument_warning); + PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning); handler->abcEnabledBuild(option, value); } theory::bv::BitblastMode stringToBitblastMode(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException) { - CheckArgument(handler != NULL, handler, s_third_argument_warning); + PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning); return handler->stringToBitblastMode(option, optarg); } theory::bv::BvSlicerMode stringToBvSlicerMode(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException) { - CheckArgument(handler != NULL, handler, s_third_argument_warning); + PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning); return handler->stringToBvSlicerMode(option, optarg); } void setBitblastAig(std::string option, bool arg, OptionsHandler* handler) throw(OptionException) { - CheckArgument(handler != NULL, handler, s_third_argument_warning); + PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning); handler->setBitblastAig(option, arg); } // theory/booleans/options_handlers.h theory::booleans::BooleanTermConversionMode stringToBooleanTermConversionMode(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException) { - CheckArgument(handler != NULL, handler, s_third_argument_warning); + PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning); return handler->stringToBooleanTermConversionMode( option, optarg); } // theory/uf/options_handlers.h theory::uf::UfssMode stringToUfssMode(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException) { - CheckArgument(handler != NULL, handler, s_third_argument_warning); + PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning); return handler->stringToUfssMode(option, optarg); } // theory/options_handlers.h theory::TheoryOfMode stringToTheoryOfMode(std::string option, std::string optarg, OptionsHandler* handler) { - CheckArgument(handler != NULL, handler, s_third_argument_warning); + PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning); return handler->stringToTheoryOfMode(option, optarg); } void useTheory(std::string option, std::string optarg, OptionsHandler* handler) { - CheckArgument(handler != NULL, handler, s_third_argument_warning); + PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning); return handler->useTheory(option, optarg); } // printer/options_handlers.h ModelFormatMode stringToModelFormatMode(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException) { - CheckArgument(handler != NULL, handler, s_third_argument_warning); + PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning); return handler->stringToModelFormatMode(option, optarg); } InstFormatMode stringToInstFormatMode(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException) { - CheckArgument(handler != NULL, handler, s_third_argument_warning); + PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning); return handler->stringToInstFormatMode(option, optarg); } // decision/options_handlers.h decision::DecisionMode stringToDecisionMode(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException) { - CheckArgument(handler != NULL, handler, s_third_argument_warning); + PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning); return handler->stringToDecisionMode(option, optarg); } decision::DecisionWeightInternal stringToDecisionWeightInternal(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException) { - CheckArgument(handler != NULL, handler, s_third_argument_warning); + PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning); return handler->stringToDecisionWeightInternal(option, optarg); } /* options/base_options_handlers.h */ void setVerbosity(std::string option, int value, OptionsHandler* handler) throw(OptionException) { - CheckArgument(handler != NULL, handler, s_third_argument_warning); + PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning); handler->setVerbosity(option, value); } void increaseVerbosity(std::string option, OptionsHandler* handler) { - CheckArgument(handler != NULL, handler, s_third_argument_warning); + PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning); handler->increaseVerbosity(option); } void decreaseVerbosity(std::string option, OptionsHandler* handler) { - CheckArgument(handler != NULL, handler, s_third_argument_warning); + PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning); handler->decreaseVerbosity(option); } OutputLanguage stringToOutputLanguage(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException) { - CheckArgument(handler != NULL, handler, s_third_argument_warning); + PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning); return handler->stringToOutputLanguage(option, optarg); } InputLanguage stringToInputLanguage(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException) { - CheckArgument(handler != NULL, handler, s_third_argument_warning); + PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning); return handler->stringToInputLanguage(option, optarg); } void addTraceTag(std::string option, std::string optarg, OptionsHandler* handler) { - CheckArgument(handler != NULL, handler, s_third_argument_warning); + PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning); handler->addTraceTag(option, optarg); } void addDebugTag(std::string option, std::string optarg, OptionsHandler* handler) { - CheckArgument(handler != NULL, handler, s_third_argument_warning); + PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning); handler->addDebugTag(option, optarg); } void setPrintSuccess(std::string option, bool value, OptionsHandler* handler) { - CheckArgument(handler != NULL, handler, s_third_argument_warning); + PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning); handler->setPrintSuccess(option, value); } /* main/options_handlers.h */ void showConfiguration(std::string option, OptionsHandler* handler) { - CheckArgument(handler != NULL, handler, s_third_argument_warning); + PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning); handler->showConfiguration(option); } void showDebugTags(std::string option, OptionsHandler* handler) { - CheckArgument(handler != NULL, handler, s_third_argument_warning); + PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning); handler->showDebugTags(option); } void showTraceTags(std::string option, OptionsHandler* handler) { - CheckArgument(handler != NULL, handler, s_third_argument_warning); + PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning); handler->showTraceTags(option); } void threadN(std::string option, OptionsHandler* handler){ - CheckArgument(handler != NULL, handler, s_third_argument_warning); + PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning); handler->threadN(option); } /* expr/options_handlers.h */ void setDefaultExprDepth(std::string option, int depth, OptionsHandler* handler){ - CheckArgument(handler != NULL, handler, s_third_argument_warning); + PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning); handler->setDefaultExprDepth(option, depth); } void setDefaultDagThresh(std::string option, int dag, OptionsHandler* handler){ - CheckArgument(handler != NULL, handler, s_third_argument_warning); + PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning); handler->setDefaultDagThresh(option, dag); } void setPrintExprTypes(std::string option, OptionsHandler* handler) { - CheckArgument(handler != NULL, handler, s_third_argument_warning); + PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning); handler->setPrintExprTypes(option); } /* smt/options_handlers.h */ void dumpMode(std::string option, std::string optarg, OptionsHandler* handler) { - CheckArgument(handler != NULL, handler, s_third_argument_warning); + PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning); handler->dumpMode(option, optarg); } LogicInfo* stringToLogicInfo(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException){ - CheckArgument(handler != NULL, handler, s_third_argument_warning); + PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning); return handler->stringToLogicInfo(option, optarg); } SimplificationMode stringToSimplificationMode(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException){ - CheckArgument(handler != NULL, handler, s_third_argument_warning); + PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning); return handler->stringToSimplificationMode(option, optarg); } // ensure we haven't started search yet void beforeSearch(std::string option, bool value, OptionsHandler* handler) throw(ModalException){ - CheckArgument(handler != NULL, handler, s_third_argument_warning); + PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning); handler->beforeSearch(option, value); } void setProduceAssertions(std::string option, bool value, OptionsHandler* handler) throw() { - CheckArgument(handler != NULL, handler, s_third_argument_warning); + PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning); handler->setProduceAssertions(option, value); } // ensure we are a proof-enabled build of CVC4 void proofEnabledBuild(std::string option, bool value, OptionsHandler* handler) throw(OptionException) { - CheckArgument(handler != NULL, handler, s_third_argument_warning); + PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning); handler->proofEnabledBuild(option, value); } void dumpToFile(std::string option, std::string optarg, OptionsHandler* handler) { - CheckArgument(handler != NULL, handler, s_third_argument_warning); + PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning); handler->dumpToFile(option, optarg); } void setRegularOutputChannel(std::string option, std::string optarg, OptionsHandler* handler) { - CheckArgument(handler != NULL, handler, s_third_argument_warning); + PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning); handler->setRegularOutputChannel(option, optarg); } void setDiagnosticOutputChannel(std::string option, std::string optarg, OptionsHandler* handler) { - CheckArgument(handler != NULL, handler, s_third_argument_warning); + PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning); handler->setDiagnosticOutputChannel(option, optarg); } std::string checkReplayFilename(std::string option, std::string optarg, OptionsHandler* handler) { - CheckArgument(handler != NULL, handler, s_third_argument_warning); + PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning); return handler->checkReplayFilename(option, optarg); } std::ostream* checkReplayLogFilename(std::string option, std::string optarg, OptionsHandler* handler) { - CheckArgument(handler != NULL, handler, s_third_argument_warning); + PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning); return handler->checkReplayLogFilename(option, optarg); } // ensure we are a stats-enabled build of CVC4 void statsEnabledBuild(std::string option, bool value, OptionsHandler* handler) throw(OptionException) { - CheckArgument(handler != NULL, handler, s_third_argument_warning); + PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning); return handler->statsEnabledBuild(option, value); } unsigned long tlimitHandler(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException) { - CheckArgument(handler != NULL, handler, s_third_argument_warning); + PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning); return handler->tlimitHandler(option, optarg); } unsigned long tlimitPerHandler(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException) { - CheckArgument(handler != NULL, handler, s_third_argument_warning); + PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning); return handler-> tlimitPerHandler(option, optarg); } unsigned long rlimitHandler(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException) { - CheckArgument(handler != NULL, handler, s_third_argument_warning); + PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning); return handler->rlimitHandler(option, optarg); } unsigned long rlimitPerHandler(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException) { - CheckArgument(handler != NULL, handler, s_third_argument_warning); + PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning); return handler->rlimitPerHandler(option, optarg); } diff --git a/src/options/simplification_mode.cpp b/src/options/simplification_mode.cpp index 08f961c15..ab7851ef9 100644 --- a/src/options/simplification_mode.cpp +++ b/src/options/simplification_mode.cpp @@ -17,6 +17,8 @@ #include "options/simplification_mode.h" +#include <iostream> + namespace CVC4 { std::ostream& operator<<(std::ostream& out, SimplificationMode mode) { diff --git a/src/options/simplification_mode.h b/src/options/simplification_mode.h index b0b78d318..dd02ada5c 100644 --- a/src/options/simplification_mode.h +++ b/src/options/simplification_mode.h @@ -20,7 +20,7 @@ #ifndef __CVC4__SMT__SIMPLIFICATION_MODE_H #define __CVC4__SMT__SIMPLIFICATION_MODE_H -#include <iostream> +#include <iosfwd> namespace CVC4 { diff --git a/src/proof/cnf_proof.h b/src/proof/cnf_proof.h index c1d245716..d3e59ef93 100644 --- a/src/proof/cnf_proof.h +++ b/src/proof/cnf_proof.h @@ -16,16 +16,17 @@ ** **/ +#include "cvc4_private.h" + #ifndef __CVC4__CNF_PROOF_H #define __CVC4__CNF_PROOF_H -#include "cvc4_private.h" -#include "util/proof.h" -#include "proof/sat_proof.h" - -#include <ext/hash_set> #include <ext/hash_map> -#include <iostream> +#include <ext/hash_set> +#include <iosfwd> + +#include "proof/sat_proof.h" +#include "util/proof.h" namespace CVC4 { namespace prop { diff --git a/src/proof/proof_manager.h b/src/proof/proof_manager.h index 4bab86745..6864eca3d 100644 --- a/src/proof/proof_manager.h +++ b/src/proof/proof_manager.h @@ -19,13 +19,14 @@ #ifndef __CVC4__PROOF_MANAGER_H #define __CVC4__PROOF_MANAGER_H -#include <iostream> +#include <iosfwd> #include <map> -#include "proof/proof.h" -#include "util/proof.h" + #include "expr/node.h" +#include "proof/proof.h" #include "theory/logic_info.h" #include "theory/substitutions.h" +#include "util/proof.h" namespace CVC4 { diff --git a/src/proof/sat_proof.h b/src/proof/sat_proof.h index a9793e784..52319431c 100644 --- a/src/proof/sat_proof.h +++ b/src/proof/sat_proof.h @@ -19,13 +19,15 @@ #ifndef __CVC4__SAT__PROOF_H #define __CVC4__SAT__PROOF_H -#include <iostream> #include <stdint.h> -#include <vector> -#include <set> + #include <ext/hash_map> #include <ext/hash_set> +#include <iosfwd> +#include <set> #include <sstream> +#include <vector> + #include "expr/expr.h" #include "proof/proof_manager.h" diff --git a/src/proof/theory_proof.h b/src/proof/theory_proof.h index d69ec5db9..375ec8205 100644 --- a/src/proof/theory_proof.h +++ b/src/proof/theory_proof.h @@ -16,15 +16,16 @@ ** **/ +#include "cvc4_private.h" #ifndef __CVC4__THEORY_PROOF_H #define __CVC4__THEORY_PROOF_H -#include "cvc4_private.h" -#include "util/proof.h" -#include "expr/expr.h" #include <ext/hash_set> -#include <iostream> +#include <iosfwd> + +#include "expr/expr.h" +#include "util/proof.h" namespace CVC4 { diff --git a/src/proof/unsat_core.h b/src/proof/unsat_core.h index 644f56509..8e92fe3d1 100644 --- a/src/proof/unsat_core.h +++ b/src/proof/unsat_core.h @@ -20,8 +20,9 @@ #ifndef __CVC4__UNSAT_CORE_H #define __CVC4__UNSAT_CORE_H -#include <iostream> +#include <iosfwd> #include <vector> + #include "expr/expr.h" namespace CVC4 { diff --git a/src/prop/minisat/core/Solver.h b/src/prop/minisat/core/Solver.h index 3ed828f7c..3be6b1b22 100644 --- a/src/prop/minisat/core/Solver.h +++ b/src/prop/minisat/core/Solver.h @@ -23,7 +23,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include "cvc4_private.h" -#include <iostream> +#include <iosfwd> #include "base/output.h" #include "context/context.h" diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 1bd2b059b..000cc167f 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -4001,18 +4001,20 @@ bool SmtEngine::addToAssignment(const Expr& ex) throw() { Expr e = d_private->substituteAbstractValues(Node::fromExpr(ex)).toExpr(); Type type = e.getType(options::typeChecking()); // must be Boolean - CheckArgument( type.isBoolean(), e, - "expected Boolean-typed variable or function application " - "in addToAssignment()" ); + PrettyCheckArgument( + type.isBoolean(), e, + "expected Boolean-typed variable or function application " + "in addToAssignment()" ); Node n = e.getNode(); // must be an APPLY of a zero-ary defined function, or a variable - CheckArgument( ( ( n.getKind() == kind::APPLY && - ( d_definedFunctions->find(n.getOperator()) != - d_definedFunctions->end() ) && - n.getNumChildren() == 0 ) || - n.isVar() ), e, - "expected variable or defined-function application " - "in addToAssignment(),\ngot %s", e.toString().c_str() ); + PrettyCheckArgument( + ( ( n.getKind() == kind::APPLY && + ( d_definedFunctions->find(n.getOperator()) != + d_definedFunctions->end() ) && + n.getNumChildren() == 0 ) || + n.isVar() ), e, + "expected variable or defined-function application " + "in addToAssignment(),\ngot %s", e.toString().c_str() ); if(!options::produceAssignments()) { return false; } diff --git a/src/smt_util/command.cpp b/src/smt_util/command.cpp index 464a2e0aa..ae4e1f1f0 100644 --- a/src/smt_util/command.cpp +++ b/src/smt_util/command.cpp @@ -23,6 +23,7 @@ #include <utility> #include <vector> +#include "base/cvc4_assert.h" #include "base/output.h" #include "expr/node.h" #include "expr/sexpr.h" @@ -939,7 +940,8 @@ GetValueCommand::GetValueCommand(Expr term) throw() : GetValueCommand::GetValueCommand(const std::vector<Expr>& terms) throw() : d_terms(terms) { - CheckArgument(terms.size() >= 1, terms, "cannot get-value of an empty set of terms"); + PrettyCheckArgument(terms.size() >= 1, terms, + "cannot get-value of an empty set of terms"); } const std::vector<Expr>& GetValueCommand::getTerms() const throw() { diff --git a/src/smt_util/command.h b/src/smt_util/command.h index b35fb7a7f..17d65beb2 100644 --- a/src/smt_util/command.h +++ b/src/smt_util/command.h @@ -22,11 +22,11 @@ #ifndef __CVC4__COMMAND_H #define __CVC4__COMMAND_H -#include <iostream> +#include <iosfwd> +#include <map> #include <sstream> #include <string> #include <vector> -#include <map> #include "expr/datatype.h" #include "expr/expr.h" diff --git a/src/smt_util/model.h b/src/smt_util/model.h index 98794a53d..33a9312a6 100644 --- a/src/smt_util/model.h +++ b/src/smt_util/model.h @@ -17,7 +17,7 @@ #ifndef __CVC4__MODEL_H #define __CVC4__MODEL_H -#include <iostream> +#include <iosfwd> #include <vector> #include "expr/expr.h" diff --git a/src/theory/arith/cut_log.h b/src/theory/arith/cut_log.h index bbed13418..f4d392995 100644 --- a/src/theory/arith/cut_log.h +++ b/src/theory/arith/cut_log.h @@ -234,7 +234,7 @@ std::ostream& operator<<(std::ostream& os, const NodeLog& nl); class ApproximateSimplex; class TreeLog { private: - ApproximateSimplex* d_generator; + ApproximateSimplex* d_generator CVC4_UNUSED; int next_exec_ord; typedef std::map<int, NodeLog> ToNodeMap; diff --git a/src/theory/arith/delta_rational.h b/src/theory/arith/delta_rational.h index 5f67847d8..39d5a9d64 100644 --- a/src/theory/arith/delta_rational.h +++ b/src/theory/arith/delta_rational.h @@ -22,6 +22,7 @@ #include <ostream> #include "base/exception.h" +#include "base/cvc4_assert.h" #include "util/integer.h" #include "util/rational.h" diff --git a/src/theory/logic_info.cpp b/src/theory/logic_info.cpp index 15600fefc..02eeefcaf 100644 --- a/src/theory/logic_info.cpp +++ b/src/theory/logic_info.cpp @@ -78,8 +78,167 @@ LogicInfo::LogicInfo(const char* logicString) throw(IllegalArgumentException) : lock(); } +/** Is sharing enabled for this logic? */ +bool LogicInfo::isSharingEnabled() const { + PrettyCheckArgument(d_locked, *this, + "This LogicInfo isn't locked yet, and cannot be queried"); + return d_sharingTheories > 1; +} + + +/** Is the given theory module active in this logic? */ +bool LogicInfo::isTheoryEnabled(theory::TheoryId theory) const { + PrettyCheckArgument(d_locked, *this, + "This LogicInfo isn't locked yet, and cannot be queried"); + return d_theories[theory]; +} + +/** Is this a quantified logic? */ +bool LogicInfo::isQuantified() const { + PrettyCheckArgument(d_locked, *this, + "This LogicInfo isn't locked yet, and cannot be queried"); + return isTheoryEnabled(theory::THEORY_QUANTIFIERS); +} + +/** Is this the all-inclusive logic? */ +bool LogicInfo::hasEverything() const { + PrettyCheckArgument(d_locked, *this, + "This LogicInfo isn't locked yet, and cannot be queried"); + LogicInfo everything; + everything.lock(); + return *this == everything; +} + +/** Is this the all-exclusive logic? (Here, that means propositional logic) */ +bool LogicInfo::hasNothing() const { + PrettyCheckArgument(d_locked, *this, + "This LogicInfo isn't locked yet, and cannot be queried"); + LogicInfo nothing(""); + nothing.lock(); + return *this == nothing; +} + +bool LogicInfo::isPure(theory::TheoryId theory) const { + PrettyCheckArgument(d_locked, *this, + "This LogicInfo isn't locked yet, and cannot be queried"); + // the third and fourth conjucts are really just to rule out the misleading + // case where you ask isPure(THEORY_BOOL) and get true even in e.g. QF_LIA + return isTheoryEnabled(theory) && !isSharingEnabled() && + ( !isTrueTheory(theory) || d_sharingTheories == 1 ) && + ( isTrueTheory(theory) || d_sharingTheories == 0 ); +} + +bool LogicInfo::areIntegersUsed() const { + PrettyCheckArgument(d_locked, *this, + "This LogicInfo isn't locked yet, and cannot be queried"); + PrettyCheckArgument( + isTheoryEnabled(theory::THEORY_ARITH), *this, + "Arithmetic not used in this LogicInfo; cannot ask whether integers are used"); + return d_integers; +} + +bool LogicInfo::areRealsUsed() const { + PrettyCheckArgument(d_locked, *this, + "This LogicInfo isn't locked yet, and cannot be queried"); + PrettyCheckArgument( + isTheoryEnabled(theory::THEORY_ARITH), *this, + "Arithmetic not used in this LogicInfo; cannot ask whether reals are used"); + return d_reals; +} + +bool LogicInfo::isLinear() const { + PrettyCheckArgument(d_locked, *this, + "This LogicInfo isn't locked yet, and cannot be queried"); + PrettyCheckArgument( + isTheoryEnabled(theory::THEORY_ARITH), *this, + "Arithmetic not used in this LogicInfo; cannot ask whether it's linear"); + return d_linear || d_differenceLogic; +} + +bool LogicInfo::isDifferenceLogic() const { + PrettyCheckArgument(d_locked, *this, + "This LogicInfo isn't locked yet, and cannot be queried"); + PrettyCheckArgument( + isTheoryEnabled(theory::THEORY_ARITH), *this, + "Arithmetic not used in this LogicInfo; cannot ask whether it's difference logic"); + return d_differenceLogic; +} + +bool LogicInfo::hasCardinalityConstraints() const { + PrettyCheckArgument(d_locked, *this, + "This LogicInfo isn't locked yet, and cannot be queried"); + return d_cardinalityConstraints; +} + + +bool LogicInfo::operator==(const LogicInfo& other) const { + PrettyCheckArgument(isLocked() && other.isLocked(), *this, + "This LogicInfo isn't locked yet, and cannot be queried"); + for(theory::TheoryId id = theory::THEORY_FIRST; id < theory::THEORY_LAST; ++id) { + if(d_theories[id] != other.d_theories[id]) { + return false; + } + } + + PrettyCheckArgument(d_sharingTheories == other.d_sharingTheories, *this, + "LogicInfo internal inconsistency"); + if(isTheoryEnabled(theory::THEORY_ARITH)) { + return + d_integers == other.d_integers && + d_reals == other.d_reals && + d_linear == other.d_linear && + d_differenceLogic == other.d_differenceLogic; + } else { + return true; + } +} + +bool LogicInfo::operator<=(const LogicInfo& other) const { + PrettyCheckArgument(isLocked() && other.isLocked(), *this, + "This LogicInfo isn't locked yet, and cannot be queried"); + for(theory::TheoryId id = theory::THEORY_FIRST; id < theory::THEORY_LAST; ++id) { + if(d_theories[id] && !other.d_theories[id]) { + return false; + } + } + PrettyCheckArgument(d_sharingTheories <= other.d_sharingTheories, *this, + "LogicInfo internal inconsistency"); + if(isTheoryEnabled(theory::THEORY_ARITH) && other.isTheoryEnabled(theory::THEORY_ARITH)) { + return + (!d_integers || other.d_integers) && + (!d_reals || other.d_reals) && + (d_linear || !other.d_linear) && + (d_differenceLogic || !other.d_differenceLogic); + } else { + return true; + } +} + +bool LogicInfo::operator>=(const LogicInfo& other) const { + PrettyCheckArgument(isLocked() && other.isLocked(), *this, + "This LogicInfo isn't locked yet, and cannot be queried"); + for(theory::TheoryId id = theory::THEORY_FIRST; id < theory::THEORY_LAST; ++id) { + if(!d_theories[id] && other.d_theories[id]) { + return false; + } + } + PrettyCheckArgument(d_sharingTheories >= other.d_sharingTheories, *this, + "LogicInfo internal inconsistency"); + if(isTheoryEnabled(theory::THEORY_ARITH) && other.isTheoryEnabled(theory::THEORY_ARITH)) { + return + (d_integers || !other.d_integers) && + (d_reals || !other.d_reals) && + (!d_linear || other.d_linear) && + (!d_differenceLogic || other.d_differenceLogic); + } else { + return true; + } +} + std::string LogicInfo::getLogicString() const { - CheckArgument(d_locked, *this, "This LogicInfo isn't locked yet, and cannot be queried"); + PrettyCheckArgument( + d_locked, *this, + "This LogicInfo isn't locked yet, and cannot be queried"); if(d_logicString == "") { LogicInfo qf_all_supported; qf_all_supported.disableQuantifiers(); @@ -156,7 +315,8 @@ std::string LogicInfo::getLogicString() const { } void LogicInfo::setLogicString(std::string logicString) throw(IllegalArgumentException) { - CheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified"); + PrettyCheckArgument(!d_locked, *this, + "This LogicInfo is locked, and cannot be modified"); for(TheoryId id = THEORY_FIRST; id < THEORY_LAST; ++id) { d_theories[id] = false;// ensure it's cleared } @@ -299,17 +459,17 @@ void LogicInfo::setLogicString(std::string logicString) throw(IllegalArgumentExc } void LogicInfo::enableEverything() { - CheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified"); + PrettyCheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified"); *this = LogicInfo(); } void LogicInfo::disableEverything() { - CheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified"); + PrettyCheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified"); *this = LogicInfo(""); } void LogicInfo::enableTheory(theory::TheoryId theory) { - CheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified"); + PrettyCheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified"); if(!d_theories[theory]) { if(isTrueTheory(theory)) { ++d_sharingTheories; @@ -320,7 +480,7 @@ void LogicInfo::enableTheory(theory::TheoryId theory) { } void LogicInfo::disableTheory(theory::TheoryId theory) { - CheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified"); + PrettyCheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified"); if(d_theories[theory]) { if(isTrueTheory(theory)) { Assert(d_sharingTheories > 0); @@ -336,14 +496,14 @@ void LogicInfo::disableTheory(theory::TheoryId theory) { } void LogicInfo::enableIntegers() { - CheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified"); + PrettyCheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified"); d_logicString = ""; enableTheory(THEORY_ARITH); d_integers = true; } void LogicInfo::disableIntegers() { - CheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified"); + PrettyCheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified"); d_logicString = ""; d_integers = false; if(!d_reals) { @@ -352,14 +512,14 @@ void LogicInfo::disableIntegers() { } void LogicInfo::enableReals() { - CheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified"); + PrettyCheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified"); d_logicString = ""; enableTheory(THEORY_ARITH); d_reals = true; } void LogicInfo::disableReals() { - CheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified"); + PrettyCheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified"); d_logicString = ""; d_reals = false; if(!d_integers) { @@ -368,21 +528,21 @@ void LogicInfo::disableReals() { } void LogicInfo::arithOnlyDifference() { - CheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified"); + PrettyCheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified"); d_logicString = ""; d_linear = true; d_differenceLogic = true; } void LogicInfo::arithOnlyLinear() { - CheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified"); + PrettyCheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified"); d_logicString = ""; d_linear = true; d_differenceLogic = false; } void LogicInfo::arithNonLinear() { - CheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified"); + PrettyCheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified"); d_logicString = ""; d_linear = false; d_differenceLogic = false; diff --git a/src/theory/logic_info.h b/src/theory/logic_info.h index 9cecc88b7..54b735114 100644 --- a/src/theory/logic_info.h +++ b/src/theory/logic_info.h @@ -104,84 +104,43 @@ public: std::string getLogicString() const; /** Is sharing enabled for this logic? */ - bool isSharingEnabled() const { - CheckArgument(d_locked, *this, "This LogicInfo isn't locked yet, and cannot be queried"); - return d_sharingTheories > 1; - } + bool isSharingEnabled() const; /** Is the given theory module active in this logic? */ - bool isTheoryEnabled(theory::TheoryId theory) const { - CheckArgument(d_locked, *this, "This LogicInfo isn't locked yet, and cannot be queried"); - return d_theories[theory]; - } + bool isTheoryEnabled(theory::TheoryId theory) const; /** Is this a quantified logic? */ - bool isQuantified() const { - CheckArgument(d_locked, *this, "This LogicInfo isn't locked yet, and cannot be queried"); - return isTheoryEnabled(theory::THEORY_QUANTIFIERS); - } + bool isQuantified() const; /** Is this the all-inclusive logic? */ - bool hasEverything() const { - CheckArgument(d_locked, *this, "This LogicInfo isn't locked yet, and cannot be queried"); - LogicInfo everything; - everything.lock(); - return *this == everything; - } + bool hasEverything() const; /** Is this the all-exclusive logic? (Here, that means propositional logic) */ - bool hasNothing() const { - CheckArgument(d_locked, *this, "This LogicInfo isn't locked yet, and cannot be queried"); - LogicInfo nothing(""); - nothing.lock(); - return *this == nothing; - } + bool hasNothing() const; /** * Is this a pure logic (only one "true" background theory). Quantifiers * can exist in such logics though; to test for quantifier-free purity, * use "isPure(theory) && !isQuantified()". */ - bool isPure(theory::TheoryId theory) const { - CheckArgument(d_locked, *this, "This LogicInfo isn't locked yet, and cannot be queried"); - // the third and fourth conjucts are really just to rule out the misleading - // case where you ask isPure(THEORY_BOOL) and get true even in e.g. QF_LIA - return isTheoryEnabled(theory) && !isSharingEnabled() && - ( !isTrueTheory(theory) || d_sharingTheories == 1 ) && - ( isTrueTheory(theory) || d_sharingTheories == 0 ); - } + bool isPure(theory::TheoryId theory) const; // these are for arithmetic /** Are integers in this logic? */ - bool areIntegersUsed() const { - CheckArgument(d_locked, *this, "This LogicInfo isn't locked yet, and cannot be queried"); - CheckArgument(isTheoryEnabled(theory::THEORY_ARITH), *this, "Arithmetic not used in this LogicInfo; cannot ask whether integers are used"); - return d_integers; - } + bool areIntegersUsed() const; + /** Are reals in this logic? */ - bool areRealsUsed() const { - CheckArgument(d_locked, *this, "This LogicInfo isn't locked yet, and cannot be queried"); - CheckArgument(isTheoryEnabled(theory::THEORY_ARITH), *this, "Arithmetic not used in this LogicInfo; cannot ask whether reals are used"); - return d_reals; - } + bool areRealsUsed() const; + /** Does this logic only linear arithmetic? */ - bool isLinear() const { - CheckArgument(d_locked, *this, "This LogicInfo isn't locked yet, and cannot be queried"); - CheckArgument(isTheoryEnabled(theory::THEORY_ARITH), *this, "Arithmetic not used in this LogicInfo; cannot ask whether it's linear"); - return d_linear || d_differenceLogic; - } + bool isLinear() const; + /** Does this logic only permit difference reasoning? (implies linear) */ - bool isDifferenceLogic() const { - CheckArgument(d_locked, *this, "This LogicInfo isn't locked yet, and cannot be queried"); - CheckArgument(isTheoryEnabled(theory::THEORY_ARITH), *this, "Arithmetic not used in this LogicInfo; cannot ask whether it's difference logic"); - return d_differenceLogic; - } + bool isDifferenceLogic() const; + /** Does this logic allow cardinality constraints? */ - bool hasCardinalityConstraints() const { - CheckArgument(d_locked, *this, "This LogicInfo isn't locked yet, and cannot be queried"); - return d_cardinalityConstraints; - } + bool hasCardinalityConstraints() const; // MUTATORS @@ -258,74 +217,27 @@ public: // COMPARISON /** Are these two LogicInfos equal? */ - bool operator==(const LogicInfo& other) const { - CheckArgument(isLocked() && other.isLocked(), *this, "This LogicInfo isn't locked yet, and cannot be queried"); - for(theory::TheoryId id = theory::THEORY_FIRST; id < theory::THEORY_LAST; ++id) { - if(d_theories[id] != other.d_theories[id]) { - return false; - } - } - CheckArgument(d_sharingTheories == other.d_sharingTheories, *this, "LogicInfo internal inconsistency"); - if(isTheoryEnabled(theory::THEORY_ARITH)) { - return - d_integers == other.d_integers && - d_reals == other.d_reals && - d_linear == other.d_linear && - d_differenceLogic == other.d_differenceLogic; - } else { - return true; - } - } + bool operator==(const LogicInfo& other) const; + /** Are these two LogicInfos disequal? */ bool operator!=(const LogicInfo& other) const { return !(*this == other); } + /** Is this LogicInfo "greater than" (does it contain everything and more) the other? */ bool operator>(const LogicInfo& other) const { return *this >= other && *this != other; } + /** Is this LogicInfo "less than" (does it contain strictly less) the other? */ bool operator<(const LogicInfo& other) const { return *this <= other && *this != other; } /** Is this LogicInfo "less than or equal" the other? */ - bool operator<=(const LogicInfo& other) const { - CheckArgument(isLocked() && other.isLocked(), *this, "This LogicInfo isn't locked yet, and cannot be queried"); - for(theory::TheoryId id = theory::THEORY_FIRST; id < theory::THEORY_LAST; ++id) { - if(d_theories[id] && !other.d_theories[id]) { - return false; - } - } - CheckArgument(d_sharingTheories <= other.d_sharingTheories, *this, "LogicInfo internal inconsistency"); - if(isTheoryEnabled(theory::THEORY_ARITH) && other.isTheoryEnabled(theory::THEORY_ARITH)) { - return - (!d_integers || other.d_integers) && - (!d_reals || other.d_reals) && - (d_linear || !other.d_linear) && - (d_differenceLogic || !other.d_differenceLogic); - } else { - return true; - } - } + bool operator<=(const LogicInfo& other) const; + /** Is this LogicInfo "greater than or equal" the other? */ - bool operator>=(const LogicInfo& other) const { - CheckArgument(isLocked() && other.isLocked(), *this, "This LogicInfo isn't locked yet, and cannot be queried"); - for(theory::TheoryId id = theory::THEORY_FIRST; id < theory::THEORY_LAST; ++id) { - if(!d_theories[id] && other.d_theories[id]) { - return false; - } - } - CheckArgument(d_sharingTheories >= other.d_sharingTheories, *this, "LogicInfo internal inconsistency"); - if(isTheoryEnabled(theory::THEORY_ARITH) && other.isTheoryEnabled(theory::THEORY_ARITH)) { - return - (d_integers || !other.d_integers) && - (d_reals || !other.d_reals) && - (!d_linear || other.d_linear) && - (!d_differenceLogic || other.d_differenceLogic); - } else { - return true; - } - } + bool operator>=(const LogicInfo& other) const; /** Are two LogicInfos comparable? That is, is one of <= or > true? */ bool isComparableTo(const LogicInfo& other) const { diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp index 798576ec3..b92d72ef4 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.cpp +++ b/src/theory/quantifiers/quantifiers_rewriter.cpp @@ -1817,11 +1817,9 @@ void QuantifiersRewriter::computePurifyExpand( Node body, std::vector< Node >& c std::map< int, std::vector< Node > > disj; std::map< int, std::vector< Node > > fvs; for( unsigned i=0; i<body.getNumChildren(); i++ ){ - int pid = getPurifyIdLit( body[i] ); - + int pid CVC4_UNUSED = getPurifyIdLit( body[i] ); } //mark as an attribute //Node attr = NodeManager::currentNM()->mkNode( INST_ATTRIBUTE, body ); - } } diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp index a39d74bb0..fb5fb0f0c 100644 --- a/src/theory/theory_model.cpp +++ b/src/theory/theory_model.cpp @@ -22,10 +22,11 @@ #include "theory/uf/theory_uf_model.h" using namespace std; -using namespace CVC4; using namespace CVC4::kind; using namespace CVC4::context; -using namespace CVC4::theory; + +namespace CVC4 { +namespace theory { TheoryModel::TheoryModel(context::Context* c, std::string name, bool enableFuncModels) : d_substitutions(c, false), d_modelBuilt(c, false), d_enableFuncModels(enableFuncModels) @@ -963,3 +964,6 @@ void TheoryEngineModelBuilder::processBuildModel(TheoryModel* m, bool fullModel) } } } + +} /* namespace CVC4::theory */ +} /* namespace CVC4 */ diff --git a/src/util/Makefile.am b/src/util/Makefile.am index 914d6e7d2..55f1a14da 100644 --- a/src/util/Makefile.am +++ b/src/util/Makefile.am @@ -45,6 +45,7 @@ libutil_la_SOURCES = \ regexp.h \ smt2_quote_string.cpp \ smt2_quote_string.h \ + subrange_bound.cpp \ subrange_bound.h \ tuple.h \ unsafe_interrupt_exception.h \ diff --git a/src/util/abstract_value.cpp b/src/util/abstract_value.cpp index e401661eb..c9dc0251d 100644 --- a/src/util/abstract_value.cpp +++ b/src/util/abstract_value.cpp @@ -15,10 +15,13 @@ **/ #include "util/abstract_value.h" + #include <iostream> #include <sstream> #include <string> +#include "base/cvc4_assert.h" + using namespace std; namespace CVC4 { @@ -29,7 +32,7 @@ std::ostream& operator<<(std::ostream& out, const AbstractValue& val) { AbstractValue::AbstractValue(Integer index) throw(IllegalArgumentException) : d_index(index) { - CheckArgument(index >= 1, index, "index >= 1 required for abstract value, not `%s'", index.toString().c_str()); + PrettyCheckArgument(index >= 1, index, "index >= 1 required for abstract value, not `%s'", index.toString().c_str()); } }/* CVC4 namespace */ diff --git a/src/util/abstract_value.h b/src/util/abstract_value.h index d597edc8b..f02df2e66 100644 --- a/src/util/abstract_value.h +++ b/src/util/abstract_value.h @@ -18,7 +18,7 @@ #pragma once -#include <iostream> +#include <iosfwd> #include "util/integer.h" diff --git a/src/util/bin_heap.h b/src/util/bin_heap.h index d057bcf84..ed6192cf7 100644 --- a/src/util/bin_heap.h +++ b/src/util/bin_heap.h @@ -26,6 +26,7 @@ #include <limits> #include <functional> +#include "base/cvc4_assert.h" #include "base/exception.h" namespace CVC4 { diff --git a/src/util/bitvector.h b/src/util/bitvector.h index 762753795..041cae38e 100644 --- a/src/util/bitvector.h +++ b/src/util/bitvector.h @@ -20,7 +20,7 @@ #ifndef __CVC4__BITVECTOR_H #define __CVC4__BITVECTOR_H -#include <iostream> +#include <iosfwd> #include "base/exception.h" #include "util/integer.h" @@ -28,34 +28,13 @@ namespace CVC4 { class CVC4_PUBLIC BitVector { - -private: - - /* - Class invariants: - * no overflows: 2^d_size < d_value - * no negative numbers: d_value >= 0 - */ - unsigned d_size; - Integer d_value; - - Integer toSignedInt() const { - // returns Integer corresponding to two's complement interpretation of bv - unsigned size = d_size; - Integer sign_bit = d_value.extractBitRange(1,size-1); - Integer val = d_value.extractBitRange(size-1, 0); - Integer res = Integer(-1) * sign_bit.multiplyByPow2(size - 1) + val; - return res; - } - - public: BitVector(unsigned size, const Integer& val): d_size(size), d_value(val.modByPow2(size)) {} - + BitVector(unsigned size = 0) : d_size(size), d_value(0) {} @@ -63,7 +42,7 @@ public: : d_size(size), d_value(z) { d_value = d_value.modByPow2(size); } - + BitVector(unsigned size, unsigned long int z) : d_size(size), d_value(z) { d_value = d_value.modByPow2(size); @@ -71,7 +50,7 @@ public: BitVector(unsigned size, const BitVector& q) : d_size(size), d_value(q.d_value) {} - + BitVector(const std::string& num, unsigned base = 2); ~BitVector() {} @@ -79,7 +58,7 @@ public: Integer toInteger() const { return d_value; } - + BitVector& operator =(const BitVector& x) { if(this == &x) return *this; @@ -89,12 +68,12 @@ public: } bool operator ==(const BitVector& y) const { - if (d_size != y.d_size) return false; + if (d_size != y.d_size) return false; return d_value == y.d_value; } bool operator !=(const BitVector& y) const { - if (d_size != y.d_size) return true; + if (d_size != y.d_size) return true; return d_value != y.d_value; } @@ -113,24 +92,24 @@ public: // xor BitVector operator ^(const BitVector& y) const { CheckArgument(d_size == y.d_size, y); - return BitVector(d_size, d_value.bitwiseXor(y.d_value)); + return BitVector(d_size, d_value.bitwiseXor(y.d_value)); } - + // or BitVector operator |(const BitVector& y) const { CheckArgument(d_size == y.d_size, y); - return BitVector(d_size, d_value.bitwiseOr(y.d_value)); + return BitVector(d_size, d_value.bitwiseOr(y.d_value)); } - + // and BitVector operator &(const BitVector& y) const { CheckArgument(d_size == y.d_size, y); - return BitVector(d_size, d_value.bitwiseAnd(y.d_value)); + return BitVector(d_size, d_value.bitwiseAnd(y.d_value)); } // not BitVector operator ~() const { - return BitVector(d_size, d_value.bitwiseNot()); + return BitVector(d_size, d_value.bitwiseNot()); } /* @@ -139,7 +118,7 @@ public: bool operator <(const BitVector& y) const { - return d_value < y.d_value; + return d_value < y.d_value; } bool operator >(const BitVector& y) const { @@ -147,14 +126,14 @@ public: } bool operator <=(const BitVector& y) const { - return d_value <= y.d_value; + return d_value <= y.d_value; } - + bool operator >=(const BitVector& y) const { return d_value >= y.d_value ; } - + BitVector operator +(const BitVector& y) const { CheckArgument(d_size == y.d_size, y); Integer sum = d_value + y.d_value; @@ -165,12 +144,12 @@ public: 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)); + BitVector one(d_size, Integer(1)); return *this + ~y + one; } BitVector operator -() const { - BitVector one(d_size, Integer(1)); + BitVector one(d_size, Integer(1)); return ~(*this) + one; } @@ -183,16 +162,16 @@ public: BitVector setBit(uint32_t i) const { CheckArgument(i < d_size, i); Integer res = d_value.setBit(i); - return BitVector(d_size, res); + return BitVector(d_size, res); } bool isBitSet(uint32_t i) const { - CheckArgument(i < d_size, i); - return d_value.isBitSet(i); + CheckArgument(i < d_size, i); + return d_value.isBitSet(i); } - - /** - * Total division function that returns 0 when the denominator is 0. + + /** + * Total division function that returns 0 when the denominator is 0. */ BitVector unsignedDivTotal (const BitVector& y) const { @@ -203,11 +182,11 @@ public: } CheckArgument(d_value >= 0, this); CheckArgument(y.d_value > 0, y); - return BitVector(d_size, d_value.floorDivideQuotient(y.d_value)); + return BitVector(d_size, d_value.floorDivideQuotient(y.d_value)); } - - /** - * Total division function that returns 0 when the denominator is 0. + + /** + * Total division function that returns 0 when the denominator is 0. */ BitVector unsignedRemTotal(const BitVector& y) const { CheckArgument(d_size == y.d_size, y); @@ -216,25 +195,25 @@ public: } CheckArgument(d_value >= 0, this); CheckArgument(y.d_value > 0, y); - return BitVector(d_size, d_value.floorDivideRemainder(y.d_value)); + return BitVector(d_size, d_value.floorDivideRemainder(y.d_value)); } - - + + bool signedLessThan(const BitVector& y) const { 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(); - - return a < b; + Integer b = y.toSignedInt(); + + return a < b; } bool unsignedLessThan(const BitVector& y) const { CheckArgument(d_size == y.d_size, y); CheckArgument(d_value >= 0, this); CheckArgument(y.d_value >= 0, y); - return d_value < y.d_value; + return d_value < y.d_value; } bool signedLessThanEq(const BitVector& y) const { @@ -242,100 +221,98 @@ public: CheckArgument(d_value >= 0, this); CheckArgument(y.d_value >= 0, y); Integer a = (*this).toSignedInt(); - Integer b = y.toSignedInt(); - - return a <= b; + Integer b = y.toSignedInt(); + + return a <= b; } bool unsignedLessThanEq(const BitVector& y) const { CheckArgument(d_size == y.d_size, this); CheckArgument(d_value >= 0, this); CheckArgument(y.d_value >= 0, y); - return d_value <= y.d_value; + return d_value <= y.d_value; } - + /* Extend operations */ - BitVector zeroExtend(unsigned amount) const { - return BitVector(d_size + amount, d_value); + return BitVector(d_size + amount, d_value); } BitVector signExtend(unsigned amount) const { Integer sign_bit = d_value.extractBitRange(1, d_size -1); if(sign_bit == Integer(0)) { - return BitVector(d_size + amount, d_value); + return BitVector(d_size + amount, d_value); } else { Integer val = d_value.oneExtend(d_size, amount); return BitVector(d_size+ amount, val); } } - + /* Shifts on BitVectors */ - BitVector leftShift(const BitVector& y) const { if (y.d_value > Integer(d_size)) { - return BitVector(d_size, Integer(0)); + return BitVector(d_size, Integer(0)); } if (y.d_value == 0) { - return *this; + return *this; } // making sure we don't lose information casting CheckArgument(y.d_value < Integer(1).multiplyByPow2(32), y); - uint32_t amount = y.d_value.toUnsignedInt(); + uint32_t amount = y.d_value.toUnsignedInt(); Integer res = d_value.multiplyByPow2(amount); return BitVector(d_size, res); } BitVector logicalRightShift(const BitVector& y) const { if(y.d_value > Integer(d_size)) { - return BitVector(d_size, Integer(0)); + return BitVector(d_size, Integer(0)); } // making sure we don't lose information casting CheckArgument(y.d_value < Integer(1).multiplyByPow2(32), y); - uint32_t amount = y.d_value.toUnsignedInt(); - Integer res = d_value.divByPow2(amount); + uint32_t amount = y.d_value.toUnsignedInt(); + Integer res = d_value.divByPow2(amount); return BitVector(d_size, res); } BitVector arithRightShift(const BitVector& y) const { - Integer sign_bit = d_value.extractBitRange(1, d_size - 1); + Integer sign_bit = d_value.extractBitRange(1, d_size - 1); if(y.d_value > Integer(d_size)) { if(sign_bit == Integer(0)) { - return BitVector(d_size, Integer(0)); + return BitVector(d_size, Integer(0)); } else { - return BitVector(d_size, Integer(d_size).multiplyByPow2(d_size) -1 ); + return BitVector(d_size, Integer(d_size).multiplyByPow2(d_size) -1 ); } } - + if (y.d_value == 0) { - return *this; + return *this; } // making sure we don't lose information casting CheckArgument(y.d_value < Integer(1).multiplyByPow2(32), y); - + uint32_t amount = y.d_value.toUnsignedInt(); Integer rest = d_value.divByPow2(amount); - + if(sign_bit == Integer(0)) { - return BitVector(d_size, rest); + return BitVector(d_size, rest); } Integer res = rest.oneExtend(d_size - amount, amount); return BitVector(d_size, res); } - + /* Convenience functions */ - + size_t hash() const { return d_value.hash() + d_size; } @@ -367,9 +344,26 @@ public: @return k if the integer is equal to 2^{k-1} and zero otherwise */ unsigned isPow2() { - return d_value.isPow2(); + return d_value.isPow2(); } +private: + /* + Class invariants: + * no overflows: 2^d_size < d_value + * no negative numbers: d_value >= 0 + */ + unsigned d_size; + Integer d_value; + + Integer toSignedInt() const { + // returns Integer corresponding to two's complement interpretation of bv + unsigned size = d_size; + Integer sign_bit = d_value.extractBitRange(1,size-1); + Integer val = d_value.extractBitRange(size-1, 0); + Integer res = Integer(-1) * sign_bit.multiplyByPow2(size - 1) + val; + return res; + } };/* class BitVector */ @@ -428,7 +422,7 @@ struct CVC4_PUBLIC BitVectorExtractHashFunction { /** - * The structure representing the extraction of one Boolean bit. + * The structure representing the extraction of one Boolean bit. */ struct CVC4_PUBLIC BitVectorBitOf { /** The index of the bit */ @@ -437,7 +431,7 @@ struct CVC4_PUBLIC BitVectorBitOf { : bitIndex(i) {} bool operator == (const BitVectorBitOf& other) const { - return bitIndex == other.bitIndex; + return bitIndex == other.bitIndex; } };/* struct BitVectorBitOf */ diff --git a/src/util/cardinality.cpp b/src/util/cardinality.cpp index dfee0aae2..07e094a38 100644 --- a/src/util/cardinality.cpp +++ b/src/util/cardinality.cpp @@ -16,6 +16,9 @@ #include "util/cardinality.h" +#include "base/cvc4_assert.h" + + namespace CVC4 { const Integer Cardinality::s_unknownCard(0); @@ -27,6 +30,45 @@ const Cardinality Cardinality::INTEGERS(CardinalityBeth(0)); const Cardinality Cardinality::REALS(CardinalityBeth(1)); const Cardinality Cardinality::UNKNOWN_CARD((CardinalityUnknown())); +CardinalityBeth::CardinalityBeth(const Integer& beth) + : d_index(beth) +{ + PrettyCheckArgument(beth >= 0, beth, + "Beth index must be a nonnegative integer, not %s.", + beth.toString().c_str()); +} + +Cardinality::Cardinality(long card) + : d_card(card) +{ + PrettyCheckArgument(card >= 0, card, + "Cardinality must be a nonnegative integer, not %ld.", + card); + d_card += 1; +} + +Cardinality::Cardinality(const Integer& card) + : d_card(card) +{ + PrettyCheckArgument(card >= 0, card, + "Cardinality must be a nonnegative integer, not %s.", + card.toString().c_str()); + d_card += 1; +} + + +Integer Cardinality::getFiniteCardinality() const throw(IllegalArgumentException) { + PrettyCheckArgument(isFinite(), *this, "This cardinality is not finite."); + PrettyCheckArgument(!isLargeFinite(), *this, "This cardinality is finite, but too large to represent."); + return d_card - 1; +} + +Integer Cardinality::getBethNumber() const throw(IllegalArgumentException) { + PrettyCheckArgument(!isFinite() && !isUnknown(), *this, + "This cardinality is not infinite (or is unknown)."); + return -d_card - 1; +} + Cardinality& Cardinality::operator+=(const Cardinality& c) throw() { if(isUnknown()) { return *this; diff --git a/src/util/cardinality.h b/src/util/cardinality.h index 1cb4454e0..8b0d85980 100644 --- a/src/util/cardinality.h +++ b/src/util/cardinality.h @@ -36,11 +36,7 @@ class CVC4_PUBLIC CardinalityBeth { Integer d_index; public: - CardinalityBeth(const Integer& beth) : d_index(beth) { - CheckArgument(beth >= 0, beth, - "Beth index must be a nonnegative integer, not %s.", - beth.toString().c_str()); - } + CardinalityBeth(const Integer& beth); const Integer& getNumber() const throw() { return d_index; @@ -112,22 +108,13 @@ public: * "unsigned" argument to enforce the restriction, we mask some * errors that automatically convert, like "Cardinality(-1)". */ - Cardinality(long card) : d_card(card) { - CheckArgument(card >= 0, card, - "Cardinality must be a nonnegative integer, not %ld.", card); - d_card += 1; - } + Cardinality(long card); /** * Construct a finite cardinality equal to the integer argument. * The argument must be nonnegative. */ - Cardinality(const Integer& card) : d_card(card) { - CheckArgument(card >= 0, card, - "Cardinality must be a nonnegative integer, not %s.", - card.toString().c_str()); - d_card += 1; - } + Cardinality(const Integer& card); /** * Construct an infinite cardinality equal to the given Beth number. @@ -187,22 +174,14 @@ public: * cardinality. (If this cardinality is infinite, this function * throws an IllegalArgumentException.) */ - Integer getFiniteCardinality() const throw(IllegalArgumentException) { - CheckArgument(isFinite(), *this, "This cardinality is not finite."); - CheckArgument(!isLargeFinite(), *this, "This cardinality is finite, but too large to represent."); - return d_card - 1; - } + Integer getFiniteCardinality() const throw(IllegalArgumentException); /** * In the case that this cardinality is infinite, return its Beth * number. (If this cardinality is finite, this function throws an * IllegalArgumentException.) */ - Integer getBethNumber() const throw(IllegalArgumentException) { - CheckArgument(!isFinite() && !isUnknown(), *this, - "This cardinality is not infinite (or is unknown)."); - return -d_card - 1; - } + Integer getBethNumber() const throw(IllegalArgumentException); /** Assigning addition of this cardinality with another. */ Cardinality& operator+=(const Cardinality& c) throw(); diff --git a/src/util/divisible.cpp b/src/util/divisible.cpp index 4a8b7a2e7..85824a77f 100644 --- a/src/util/divisible.cpp +++ b/src/util/divisible.cpp @@ -17,6 +17,7 @@ #include "util/divisible.h" +#include "base/cvc4_assert.h" #include "base/exception.h" using namespace std; @@ -24,7 +25,7 @@ using namespace std; namespace CVC4 { Divisible::Divisible(const Integer& n) : k(n) { - CheckArgument(n > 0, n, "Divisible predicate must be constructed over positive N"); + PrettyCheckArgument(n > 0, n, "Divisible predicate must be constructed over positive N"); } }/* CVC4 namespace */ diff --git a/src/util/divisible.h b/src/util/divisible.h index 5f62def02..56178e604 100644 --- a/src/util/divisible.h +++ b/src/util/divisible.h @@ -20,7 +20,7 @@ #ifndef __CVC4__DIVISIBLE_H #define __CVC4__DIVISIBLE_H -#include <iostream> +#include <iosfwd> #include "base/exception.h" #include "util/integer.h" diff --git a/src/util/floatingpoint.cpp b/src/util/floatingpoint.cpp index d3bb1967a..d1164133a 100644 --- a/src/util/floatingpoint.cpp +++ b/src/util/floatingpoint.cpp @@ -19,20 +19,20 @@ namespace CVC4 { - FloatingPointSize::FloatingPointSize (unsigned _e, unsigned _s) : e(_e), s(_s) - { - CheckArgument(validExponentSize(_e),_e,"Invalid exponent size : %d",_e); - CheckArgument(validSignificandSize(_s),_s,"Invalid significand size : %d",_s); - } +FloatingPointSize::FloatingPointSize (unsigned _e, unsigned _s) : e(_e), s(_s) +{ + PrettyCheckArgument(validExponentSize(_e),_e,"Invalid exponent size : %d",_e); + PrettyCheckArgument(validSignificandSize(_s),_s,"Invalid significand size : %d",_s); +} - FloatingPointSize::FloatingPointSize (const FloatingPointSize &old) : e(old.e), s(old.s) - { - CheckArgument(validExponentSize(e),e,"Invalid exponent size : %d",e); - CheckArgument(validSignificandSize(s),s,"Invalid significand size : %d",s); - } +FloatingPointSize::FloatingPointSize (const FloatingPointSize &old) : e(old.e), s(old.s) +{ + PrettyCheckArgument(validExponentSize(e),e,"Invalid exponent size : %d",e); + PrettyCheckArgument(validSignificandSize(s),s,"Invalid significand size : %d",s); +} - void FloatingPointLiteral::unfinished (void) const { - Unimplemented("Floating-point literals not yet implemented."); - } +void FloatingPointLiteral::unfinished (void) const { + Unimplemented("Floating-point literals not yet implemented."); +} }/* CVC4 namespace */ diff --git a/src/util/integer_cln_imp.cpp b/src/util/integer_cln_imp.cpp index 1cb4349eb..27a4b7d06 100644 --- a/src/util/integer_cln_imp.cpp +++ b/src/util/integer_cln_imp.cpp @@ -26,8 +26,34 @@ # error "This source should only ever be built if CVC4_CLN_IMP is on !" #endif /* CVC4_CLN_IMP */ +#include "base/cvc4_assert.h" + using namespace std; -using namespace CVC4; + +namespace CVC4 { + +signed int Integer::s_fastSignedIntMin = -(1<<29); +signed int Integer::s_fastSignedIntMax = (1<<29)-1; +signed long Integer::s_slowSignedIntMin = (signed long) std::numeric_limits<signed int>::min(); +signed long Integer::s_slowSignedIntMax = (signed long) std::numeric_limits<signed int>::max(); + +unsigned int Integer::s_fastUnsignedIntMax = (1<<29)-1; +unsigned long Integer::s_slowUnsignedIntMax = (unsigned long) std::numeric_limits<unsigned int>::max(); + +Integer Integer::oneExtend(uint32_t size, uint32_t amount) const { + 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); + + return Integer(cln::deposit_field(allones, d_value, range)); +} + + +Integer Integer::exactQuotient(const Integer& y) const { + DebugCheckArgument(y.divides(*this), y); + return Integer( cln::exquo(d_value, y.d_value) ); +} void Integer::parseInt(const std::string& s, unsigned base) throw(std::invalid_argument) { @@ -78,14 +104,21 @@ void Integer::readInt(const cln::cl_read_flags& flags, const std::string& s, uns } bool Integer::fitsSignedInt() const { + // http://www.ginac.de/CLN/cln.html#Conversions // TODO improve performance - return d_value <= std::numeric_limits<signed int>::max() && - d_value >= std::numeric_limits<signed int>::min(); + Assert(s_slowSignedIntMin <= s_fastSignedIntMin); + Assert(s_fastSignedIntMin <= s_fastSignedIntMax); + Assert(s_fastSignedIntMax <= s_slowSignedIntMax); + + return (d_value <= s_fastSignedIntMax || d_value <= s_slowSignedIntMax) && + (d_value >= s_fastSignedIntMin || d_value >= s_slowSignedIntMax); } bool Integer::fitsUnsignedInt() const { // TODO improve performance - return sgn() >= 0 && d_value <= std::numeric_limits<unsigned int>::max(); + Assert(s_fastUnsignedIntMax <= s_slowUnsignedIntMax); + return sgn() >= 0 && + (d_value <= s_fastUnsignedIntMax || d_value <= s_slowUnsignedIntMax); } signed int Integer::getSignedInt() const { @@ -99,3 +132,5 @@ unsigned int Integer::getUnsignedInt() const { CheckArgument(fitsUnsignedInt(), this, "Overflow detected in Integer::getUnsignedInt()"); return cln::cl_I_to_uint(d_value); } + +} /* namespace CVC4 */ diff --git a/src/util/integer_cln_imp.h b/src/util/integer_cln_imp.h index 6df8d3b8e..9e5e6c2ae 100644 --- a/src/util/integer_cln_imp.h +++ b/src/util/integer_cln_imp.h @@ -20,14 +20,13 @@ #ifndef __CVC4__INTEGER_H #define __CVC4__INTEGER_H -#include <string> -#include <sstream> -#include <iostream> - -#include <cln/integer.h> #include <cln/input.h> +#include <cln/integer.h> #include <cln/integer_io.h> +#include <iostream> #include <limits> +#include <sstream> +#include <string> #include "base/exception.h" @@ -57,6 +56,17 @@ private: void parseInt(const std::string& s, unsigned base) throw(std::invalid_argument); + + // These constants are to help with CLN conversion in 32 bit. + // See http://www.ginac.de/CLN/cln.html#Conversions + static signed int s_fastSignedIntMax; /* 2^29 - 1 */ + static signed int s_fastSignedIntMin; /* -2^29 */ + static unsigned int s_fastUnsignedIntMax; /* 2^29 - 1 */ + + static signed long s_slowSignedIntMax; /* std::numeric_limits<signed int>::max() */ + static signed long s_slowSignedIntMin; /* std::numeric_limits<signed int>::min() */ + static unsigned long s_slowUnsignedIntMax; /* std::numeric_limits<unsigned int>::max() */ + public: /** Constructs a rational with the value 0. */ @@ -186,14 +196,7 @@ public: return Integer(cln::logior(d_value, mask)); } - Integer oneExtend(uint32_t size, uint32_t amount) const { - 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); - - return Integer(cln::deposit_field(allones, d_value, range)); - } + Integer oneExtend(uint32_t size, uint32_t amount) const; uint32_t toUnsignedInt() const { return cln::cl_I_to_uint(d_value); @@ -300,10 +303,7 @@ public: /** * If y divides *this, then exactQuotient returns (this/y) */ - Integer exactQuotient(const Integer& y) const { - DebugCheckArgument(y.divides(*this), y); - return Integer( cln::exquo(d_value, y.d_value) ); - } + Integer exactQuotient(const Integer& y) const; Integer modByPow2(uint32_t exp) const { cln::cl_byte range(exp, 0); diff --git a/src/util/integer_gmp_imp.cpp b/src/util/integer_gmp_imp.cpp index bde759219..df1bd297a 100644 --- a/src/util/integer_gmp_imp.cpp +++ b/src/util/integer_gmp_imp.cpp @@ -21,16 +21,18 @@ #include <string> #include "cvc4autoconfig.h" + +#include "base/cvc4_assert.h" #include "util/rational.h" #ifndef CVC4_GMP_IMP # error "This source should only ever be built if CVC4_GMP_IMP is on !" #endif /* CVC4_GMP_IMP */ -using namespace std; -using namespace CVC4; +using namespace std; +namespace CVC4 { Integer::Integer(const char* s, unsigned base) : d_value(s, base) @@ -52,10 +54,11 @@ bool Integer::fitsUnsignedInt() const { signed int Integer::getSignedInt() const { // ensure there isn't overflow CheckArgument(d_value <= std::numeric_limits<int>::max(), this, - "Overflow detected in Integer::getSignedInt()"); + "Overflow detected in Integer::getSignedInt()."); CheckArgument(d_value >= std::numeric_limits<int>::min(), this, - "Overflow detected in Integer::getSignedInt()"); - CheckArgument(fitsSignedInt(), this, "Overflow detected in Integer::getSignedInt()"); + "Overflow detected in Integer::getSignedInt()."); + CheckArgument(fitsSignedInt(), this, + "Overflow detected in Integer::getSignedInt()."); return (signed int) d_value.get_si(); } @@ -65,6 +68,28 @@ unsigned int Integer::getUnsignedInt() const { "Overflow detected in Integer::getUnsignedInt()"); CheckArgument(d_value >= std::numeric_limits<unsigned int>::min(), this, "Overflow detected in Integer::getUnsignedInt()"); - CheckArgument(fitsSignedInt(), this, "Overflow detected in Integer::getUnsignedInt()"); + CheckArgument(fitsSignedInt(), this, + "Overflow detected in Integer::getUnsignedInt()"); return (unsigned int) d_value.get_ui(); } + +Integer Integer::oneExtend(uint32_t size, uint32_t amount) const { + // check that the size is accurate + DebugCheckArgument((*this) < Integer(1).multiplyByPow2(size), size); + mpz_class res = d_value; + + for (unsigned i = size; i < size + amount; ++i) { + mpz_setbit(res.get_mpz_t(), i); + } + + return Integer(res); +} + +Integer Integer::exactQuotient(const Integer& y) const { + 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 ); +} + +} /* namespace CVC4 */ diff --git a/src/util/integer_gmp_imp.h b/src/util/integer_gmp_imp.h index 0d3122cd8..9cae16222 100644 --- a/src/util/integer_gmp_imp.h +++ b/src/util/integer_gmp_imp.h @@ -21,7 +21,7 @@ #define __CVC4__INTEGER_H #include <string> -#include <iostream> +#include <iosfwd> #include <limits> #include "base/exception.h" @@ -190,17 +190,7 @@ public: * Returns the integer with the binary representation of size bits * extended with amount 1's */ - Integer oneExtend(uint32_t size, uint32_t amount) const { - // check that the size is accurate - DebugCheckArgument((*this) < Integer(1).multiplyByPow2(size), size); - mpz_class res = d_value; - - for (unsigned i = size; i < size + amount; ++i) { - mpz_setbit(res.get_mpz_t(), i); - } - - return Integer(res); - } + Integer oneExtend(uint32_t size, uint32_t amount) const; uint32_t toUnsignedInt() const { return mpz_get_ui(d_value.get_mpz_t()); @@ -319,12 +309,7 @@ public: /** * If y divides *this, then exactQuotient returns (this/y) */ - Integer exactQuotient(const Integer& y) const { - 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 ); - } + Integer exactQuotient(const Integer& y) const; /** * Returns y mod 2^exp @@ -430,14 +415,15 @@ public: long si = d_value.get_si(); // ensure there wasn't overflow CheckArgument(mpz_cmp_si(d_value.get_mpz_t(), si) == 0, this, - "Overflow detected in Integer::getLong()"); + "Overflow detected in Integer::getLong()."); return si; } + unsigned long getUnsignedLong() const { unsigned long ui = d_value.get_ui(); // ensure there wasn't overflow CheckArgument(mpz_cmp_ui(d_value.get_mpz_t(), ui) == 0, this, - "Overflow detected in Integer::getUnsignedLong()"); + "Overflow detected in Integer::getUnsignedLong()."); return ui; } diff --git a/src/util/proof.h b/src/util/proof.h index be1e2a8e2..22d9f97d5 100644 --- a/src/util/proof.h +++ b/src/util/proof.h @@ -20,7 +20,7 @@ #ifndef __CVC4__PROOF_H #define __CVC4__PROOF_H -#include <iostream> +#include <iosfwd> namespace CVC4 { diff --git a/src/util/rational_cln_imp.cpp b/src/util/rational_cln_imp.cpp index 5044aff18..608b33f2b 100644 --- a/src/util/rational_cln_imp.cpp +++ b/src/util/rational_cln_imp.cpp @@ -24,8 +24,11 @@ # error "This source should only ever be built if CVC4_CLN_IMP is on !" #endif /* CVC4_CLN_IMP */ +#include "base/cvc4_assert.h" + using namespace std; -using namespace CVC4; + +namespace CVC4 { /* Computes a rational given a decimal string. The rational * version of <code>xxx.yyy</code> is <code>xxxyyy/(10^3)</code>. @@ -48,7 +51,7 @@ Rational Rational::fromDecimal(const std::string& dec) { } } -std::ostream& CVC4::operator<<(std::ostream& os, const Rational& q){ +std::ostream& operator<<(std::ostream& os, const Rational& q){ return os << q.toString(); } @@ -105,3 +108,5 @@ RationalFromDoubleException::RationalFromDoubleException(double d) throw() ss << ")"; setMessage(ss.str()); } + +} /* namespace CVC4 */ diff --git a/src/util/rational_gmp_imp.cpp b/src/util/rational_gmp_imp.cpp index f0f7d46eb..63fb8e05c 100644 --- a/src/util/rational_gmp_imp.cpp +++ b/src/util/rational_gmp_imp.cpp @@ -21,15 +21,18 @@ #include "cvc4autoconfig.h" -#ifndef CVC4_GMP_IMP +#ifndef CVC4_GMP_IMP // Make sure this comes after cvc4autoconfig.h # error "This source should only ever be built if CVC4_GMP_IMP is on !" #endif /* CVC4_GMP_IMP */ -std::ostream& CVC4::operator<<(std::ostream& os, const Rational& q){ +#include "base/cvc4_assert.h" + +namespace CVC4 { + +std::ostream& operator<<(std::ostream& os, const Rational& q){ return os << q.toString(); } -namespace CVC4 { /* Computes a rational given a decimal string. The rational * version of <code>xxx.yyy</code> is <code>xxxyyy/(10^3)</code>. diff --git a/src/util/subrange_bound.cpp b/src/util/subrange_bound.cpp new file mode 100644 index 000000000..5d66b75ad --- /dev/null +++ b/src/util/subrange_bound.cpp @@ -0,0 +1,63 @@ +/********************* */ +/*! \file subrange_bound.cpp + ** \verbatim + ** Original author: Tim King + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 project. + ** Copyright (c) 2015 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Representation of subrange bounds + ** + ** Simple class to represent a subrange bound, either infinite + ** (no bound) or finite (an arbitrary precision integer). + **/ + +#include "util/subrange_bound.h" + +#include <limits> + +#include "base/cvc4_assert.h" +#include "base/exception.h" +#include "util/integer.h" + +namespace CVC4 { + +std::ostream& operator<<(std::ostream& out, const SubrangeBounds& bounds) +throw() { + out << bounds.lower << ".." << bounds.upper; + + return out; +} + +/** Get the finite SubrangeBound, failing an assertion if infinite. */ +const Integer& SubrangeBound::getBound() const throw(IllegalArgumentException) { + PrettyCheckArgument(!d_nobound, this, "SubrangeBound is infinite"); + return d_bound; +} + +SubrangeBounds::SubrangeBounds(const SubrangeBound& l, + const SubrangeBound& u) + : lower(l) + , upper(u) +{ + PrettyCheckArgument(!l.hasBound() || !u.hasBound() || + l.getBound() <= u.getBound(), + l, "Bad subrange bounds specified"); +} + +bool SubrangeBounds::joinIsBounded(const SubrangeBounds& a, const SubrangeBounds& b){ + return (a.lower.hasBound() && b.lower.hasBound()) || + (a.upper.hasBound() && b.upper.hasBound()); +} + +SubrangeBounds SubrangeBounds::join(const SubrangeBounds& a, const SubrangeBounds& 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); +} + +} /* namespace CVC4 */ diff --git a/src/util/subrange_bound.h b/src/util/subrange_bound.h index 6cff7133c..d5b50bf4c 100644 --- a/src/util/subrange_bound.h +++ b/src/util/subrange_bound.h @@ -34,9 +34,6 @@ namespace CVC4 { * has a lower bound of -5 and an infinite upper bound. */ class CVC4_PUBLIC SubrangeBound { - bool d_nobound; - Integer d_bound; - public: /** Construct an infinite SubrangeBound. */ @@ -55,10 +52,7 @@ public: } /** Get the finite SubrangeBound, failing an assertion if infinite. */ - const Integer& getBound() const throw(IllegalArgumentException) { - CheckArgument(!d_nobound, this, "SubrangeBound is infinite"); - return d_bound; - } + const Integer& getBound() const throw(IllegalArgumentException); /** Returns true iff this is a finite SubrangeBound. */ bool hasBound() const throw() { @@ -145,6 +139,9 @@ public: } } +private: + bool d_nobound; + Integer d_bound; };/* class SubrangeBound */ class CVC4_PUBLIC SubrangeBounds { @@ -153,13 +150,7 @@ public: SubrangeBound lower; SubrangeBound upper; - SubrangeBounds(const SubrangeBound& l, const SubrangeBound& u) : - lower(l), - upper(u) { - CheckArgument(!l.hasBound() || !u.hasBound() || - l.getBound() <= u.getBound(), - l, "Bad subrange bounds specified"); - } + SubrangeBounds(const SubrangeBound& l, const SubrangeBound& u); bool operator==(const SubrangeBounds& bounds) const { return lower == bounds.lower && upper == bounds.upper; @@ -210,21 +201,13 @@ public: /** * Returns true if the join of two subranges is not (- infinity, + infinity). */ - static bool joinIsBounded(const SubrangeBounds& a, const SubrangeBounds& b){ - return (a.lower.hasBound() && b.lower.hasBound()) || - (a.upper.hasBound() && b.upper.hasBound()); - } + static bool joinIsBounded(const SubrangeBounds& a, const SubrangeBounds& b); /** * Returns the join of two subranges, a and b. * precondition: joinIsBounded(a,b) is true */ - static SubrangeBounds join(const SubrangeBounds& a, const SubrangeBounds& 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); - } + static SubrangeBounds join(const SubrangeBounds& a, const SubrangeBounds& b); };/* class SubrangeBounds */ @@ -252,15 +235,8 @@ operator<<(std::ostream& out, const SubrangeBound& bound) throw() { return out; } -inline std::ostream& -operator<<(std::ostream& out, const SubrangeBounds& bounds) throw() CVC4_PUBLIC; - -inline std::ostream& -operator<<(std::ostream& out, const SubrangeBounds& bounds) throw() { - out << bounds.lower << ".." << bounds.upper; - - return out; -} +std::ostream& operator<<(std::ostream& out, const SubrangeBounds& bounds) +throw() CVC4_PUBLIC; }/* CVC4 namespace */ diff --git a/test/unit/expr/attribute_black.h b/test/unit/expr/attribute_black.h index 5f9a7ebce..d162171d6 100644 --- a/test/unit/expr/attribute_black.h +++ b/test/unit/expr/attribute_black.h @@ -145,7 +145,7 @@ public: } class Foo { - int blah; + int blah CVC4_UNUSED; public: Foo(int b) : blah(b) {} }; |