diff options
85 files changed, 1125 insertions, 786 deletions
diff --git a/Makefile.am b/Makefile.am index 267e10bc2..fb3e979d9 100644 --- a/Makefile.am +++ b/Makefile.am @@ -107,6 +107,8 @@ EXTRA_DIST = \ doc/cvc4.1_template.in \ doc/cvc4.5.in \ doc/libcvc4.3_template.in \ + doc/SmtEngine.3cvc4_template.in \ + doc/options.3cvc4_template.in \ doc/libcvc4parser.3.in \ doc/libcvc4compat.3.in man_MANS = \ @@ -114,6 +116,8 @@ man_MANS = \ doc/pcvc4.1 \ doc/cvc4.5 \ doc/libcvc4.3 \ + doc/SmtEngine.3cvc4 \ + doc/options.3cvc4 \ doc/libcvc4parser.3 \ doc/libcvc4compat.3 diff --git a/configure.ac b/configure.ac index dc62970f1..40dd6df2c 100644 --- a/configure.ac +++ b/configure.ac @@ -1136,6 +1136,8 @@ CVC4_CONFIG_FILE_ONLY_IF_CHANGED([src/util/tls.h]) CVC4_CONFIG_FILE_ONLY_IF_CHANGED([doc/cvc4.1_template]) CVC4_CONFIG_FILE_ONLY_IF_CHANGED([doc/cvc4.5]) CVC4_CONFIG_FILE_ONLY_IF_CHANGED([doc/libcvc4.3_template]) +CVC4_CONFIG_FILE_ONLY_IF_CHANGED([doc/SmtEngine.3cvc4_template]) +CVC4_CONFIG_FILE_ONLY_IF_CHANGED([doc/options.3cvc4_template]) CVC4_CONFIG_FILE_ONLY_IF_CHANGED([doc/libcvc4parser.3]) CVC4_CONFIG_FILE_ONLY_IF_CHANGED([doc/libcvc4compat.3]) diff --git a/doc/SmtEngine.3cvc4_template.in b/doc/SmtEngine.3cvc4_template.in new file mode 100644 index 000000000..99b0451f6 --- /dev/null +++ b/doc/SmtEngine.3cvc4_template.in @@ -0,0 +1,51 @@ +.\" Process this file with +.\" groff -man -Tascii SmtEngine.3cvc4 +.\" +.TH SMTENGINE 3cvc4 "@MAN_DATE@" "CVC4 release @VERSION@" "CVC4 Library Interfaces" +.SH NAME +SmtEngine \- the primary interface to CVC4's theorem-proving capabilities +.SH DESCRIPTION +.B SmtEngine +is the main entry point into the CVC4 theorem prover API. + +.SH SMTENGINE OPTIONS + +The SmtEngine is in charge of setting and getting information and options. +Numerous options are available via the +.I SmtEngine::setOption() +call. +.I SmtEngine::setOption() +and +.I SmtEngine::getOption() +use the following option keys. + +.RS +.TP 10 +.I "COMMON OPTIONS" +${common_manpage_smt_documentation} + +${remaining_manpage_smt_documentation} +.PD +.RE + +.SH VERSION +This manual page refers to +.B CVC4 +version @VERSION@. +.SH BUGS +A Bugzilla for the CVC4 project is maintained at +.BR http://church.cims.nyu.edu/bugzilla3/ . +.SH AUTHORS +.B CVC4 +is developed by a team of researchers at New York University +and the University of Iowa. +See the AUTHORS file in the distribution for a full list of +contributors. +.SH "SEE ALSO" +.BR libcvc4 (3), +.BR libcvc4parser (3), +.BR libcvc4compat (3) + +Additionally, the CVC4 wiki contains useful information about the +design and internals of CVC4. It is maintained at +.BR http://church.cims.nyu.edu/wiki/ . diff --git a/doc/cvc4.1_template.in b/doc/cvc4.1_template.in index ad8226261..5a5f90214 100644 --- a/doc/cvc4.1_template.in +++ b/doc/cvc4.1_template.in @@ -115,7 +115,7 @@ This manual page refers to version @VERSION@. .SH BUGS A Bugzilla for the CVC4 project is maintained at -.BR http://goedel.cs.nyu.edu/bugzilla3/ . +.BR http://church.cims.nyu.edu/bugzilla3/ . .SH AUTHORS .B CVC4 is developed by a team of researchers at New York University @@ -129,4 +129,4 @@ contributors. Additionally, the CVC4 wiki contains useful information about the design and internals of CVC4. It is maintained at -.BR http://goedel.cs.nyu.edu/wiki/ . +.BR http://church.cims.nyu.edu/wiki/ . diff --git a/doc/cvc4.5.in b/doc/cvc4.5.in index d862eec8a..ab4e8806c 100644 --- a/doc/cvc4.5.in +++ b/doc/cvc4.5.in @@ -18,4 +18,4 @@ to background theories of interest. Additionally, the CVC4 wiki contains useful information about the design and internals of CVC4. It is maintained at -.BR http://goedel.cs.nyu.edu/wiki/ . +.BR http://church.cims.nyu.edu/wiki/ . diff --git a/doc/libcvc4.3_template.in b/doc/libcvc4.3_template.in index 5483099c3..2ff96eb5a 100644 --- a/doc/libcvc4.3_template.in +++ b/doc/libcvc4.3_template.in @@ -55,21 +55,6 @@ is used to build up expressions and types, and the .I SmtEngine is used primarily to make assertions, check satisfiability/validity, and extract models and proofs. -The SmtEngine is also in charge of setting and getting information and options. -.I SmtEngine::setOption() -and -.I SmtEngine::getOption() -use the following option keys. - -.RS -.TP 10 -.I "COMMON OPTIONS" -${common_manpage_smt_documentation} - -${remaining_manpage_smt_documentation} -.PD -.RE - .SH "SEE ALSO" .BR cvc4 (1), .BR libcvc4parser (3), diff --git a/doc/libcvc4compat.3.in b/doc/libcvc4compat.3.in index e429fc815..3722557b0 100644 --- a/doc/libcvc4compat.3.in +++ b/doc/libcvc4compat.3.in @@ -12,4 +12,4 @@ libcvc4compat \- a CVC3 compatibility library interface for the CVC4 theorem pro Additionally, the CVC4 wiki contains useful information about the design and internals of CVC4. It is maintained at -.BR http://goedel.cs.nyu.edu/wiki/ . +.BR http://church.cims.nyu.edu/wiki/ . diff --git a/doc/libcvc4parser.3.in b/doc/libcvc4parser.3.in index fa17d6d18..67ec74326 100644 --- a/doc/libcvc4parser.3.in +++ b/doc/libcvc4parser.3.in @@ -12,4 +12,4 @@ libcvc4parser \- a parser library interface for the CVC4 theorem prover Additionally, the CVC4 wiki contains useful information about the design and internals of CVC4. It is maintained at -.BR http://goedel.cs.nyu.edu/wiki/ . +.BR http://church.cims.nyu.edu/wiki/ . diff --git a/doc/options.3cvc4_template.in b/doc/options.3cvc4_template.in new file mode 100644 index 000000000..8ee39b761 --- /dev/null +++ b/doc/options.3cvc4_template.in @@ -0,0 +1,39 @@ +.\" Process this file with +.\" groff -man -Tascii options.3cvc4 +.\" +.TH OPTIONS 3cvc4 "@MAN_DATE@" "CVC4 release @VERSION@" "CVC4 Internals Documentation" +.SH NAME +options \- the options infrastructure + +.SH AVAILABLE INTERNAL OPTIONS + +.RS +.TP 10 +.I "COMMON OPTIONS" +${common_manpage_internals_documentation} + +${remaining_manpage_internals_documentation} +.PD +.RE + +.SH VERSION +This manual page refers to +.B CVC4 +version @VERSION@. +.SH BUGS +A Bugzilla for the CVC4 project is maintained at +.BR http://church.cims.nyu.edu/bugzilla3/ . +.SH AUTHORS +.B CVC4 +is developed by a team of researchers at New York University +and the University of Iowa. +See the AUTHORS file in the distribution for a full list of +contributors. +.SH "SEE ALSO" +.BR libcvc4 (3), +.BR libcvc4parser (3), +.BR libcvc4compat (3) + +Additionally, the CVC4 wiki contains useful information about the +design and internals of CVC4. It is maintained at +.BR http://church.cims.nyu.edu/wiki/ . diff --git a/src/compat/cvc3_compat.cpp b/src/compat/cvc3_compat.cpp index b7c7013d2..95417845f 100644 --- a/src/compat/cvc3_compat.cpp +++ b/src/compat/cvc3_compat.cpp @@ -40,9 +40,12 @@ #include <sstream> #include <algorithm> #include <iterator> +#include <cassert> using namespace std; +#define Unimplemented(str) throw Exception(str) + namespace CVC3 { // Connects ExprManagers to ValidityCheckers. Needed to clean up the @@ -60,13 +63,13 @@ static bool typeHasExpr(const Type& t) { static Expr typeToExpr(const Type& t) { std::hash_map<Type, Expr, CVC4::TypeHashFunction>::const_iterator i = s_typeToExpr.find(t); - AlwaysAssert(i != s_typeToExpr.end()); + assert(i != s_typeToExpr.end()); return (*i).second; } static Type exprToType(const Expr& e) { std::hash_map<Expr, Type, CVC4::ExprHashFunction>::const_iterator i = s_exprToType.find(e); - AlwaysAssert(i != s_exprToType.end()); + assert(i != s_exprToType.end()); return (*i).second; } @@ -145,7 +148,7 @@ bool operator==(const Cardinality& c, CVC3CardinalityKind d) { return c.isUnknown(); } - Unhandled(d); + throw Exception("internal error: CVC3 cardinality kind unhandled"); } bool operator==(CVC3CardinalityKind d, const Cardinality& c) { @@ -431,7 +434,7 @@ Expr Expr::getExpr() const { } std::vector< std::vector<Expr> > Expr::getTriggers() const { - CheckArgument(isClosure(), *this, __PRETTY_FUNCTION__, "getTriggers() called on non-closure expr"); + CVC4::CheckArgument(isClosure(), *this, "getTriggers() called on non-closure expr"); if(getNumChildren() < 3) { // no triggers for this quantifier return vector< vector<Expr> >(); @@ -589,37 +592,37 @@ CLFlag& CLFlag::operator=(const CLFlag& f) { } CLFlag& CLFlag::operator=(bool b) { - CheckArgument(d_tp == CLFLAG_BOOL, this); + CVC4::CheckArgument(d_tp == CLFLAG_BOOL, this); d_data.b = b; return *this; } CLFlag& CLFlag::operator=(int i) { - CheckArgument(d_tp == CLFLAG_INT, this); + CVC4::CheckArgument(d_tp == CLFLAG_INT, this); d_data.i = i; return *this; } CLFlag& CLFlag::operator=(const std::string& s) { - CheckArgument(d_tp == CLFLAG_STRING, this); + CVC4::CheckArgument(d_tp == CLFLAG_STRING, this); *d_data.s = s; return *this; } CLFlag& CLFlag::operator=(const char* s) { - CheckArgument(d_tp == CLFLAG_STRING, this); + CVC4::CheckArgument(d_tp == CLFLAG_STRING, this); *d_data.s = s; return *this; } CLFlag& CLFlag::operator=(const std::pair<string, bool>& p) { - CheckArgument(d_tp == CLFLAG_STRVEC, this); + CVC4::CheckArgument(d_tp == CLFLAG_STRVEC, this); d_data.sv->push_back(p); return *this; } CLFlag& CLFlag::operator=(const std::vector<std::pair<string, bool> >& sv) { - CheckArgument(d_tp == CLFLAG_STRVEC, this); + CVC4::CheckArgument(d_tp == CLFLAG_STRVEC, this); *d_data.sv = sv; return *this; } @@ -637,22 +640,22 @@ bool CLFlag::display() const { } const bool& CLFlag::getBool() const { - CheckArgument(d_tp == CLFLAG_BOOL, this); + CVC4::CheckArgument(d_tp == CLFLAG_BOOL, this); return d_data.b; } const int& CLFlag::getInt() const { - CheckArgument(d_tp == CLFLAG_INT, this); + CVC4::CheckArgument(d_tp == CLFLAG_INT, this); return d_data.i; } const std::string& CLFlag::getString() const { - CheckArgument(d_tp == CLFLAG_STRING, this); + CVC4::CheckArgument(d_tp == CLFLAG_STRING, this); return *d_data.s; } const std::vector<std::pair<string, bool> >& CLFlag::getStrVec() const { - CheckArgument(d_tp == CLFLAG_STRVEC, this); + CVC4::CheckArgument(d_tp == CLFLAG_STRVEC, this); return *d_data.sv; } @@ -675,7 +678,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); - CheckArgument(i != d_map.end(), name, "No command-line flag by that name, or not supported."); + CVC4::CheckArgument(i != d_map.end(), name, "No command-line flag by that name, or not supported."); return (*i).second; } @@ -685,49 +688,49 @@ 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); - CheckArgument(i != d_map.end(), name, "No command-line flag by that name, or not supported."); - CheckArgument((*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(), - toString(f.getType()).c_str()); + 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, + "Command-line flag `%s' has type %s, but caller tried to set to a %s.", + name.c_str(), + toString((*i).second.getType()).c_str(), + toString(f.getType()).c_str()); (*i).second = f; } void CLFlags::setFlag(const std::string& name, bool b) { FlagMap::iterator i = d_map.find(name); - CheckArgument(i != d_map.end(), name, "No command-line flag by that name, or not supported."); + CVC4::CheckArgument(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); - CheckArgument(it != d_map.end(), name, "No command-line flag by that name, or not supported."); + CVC4::CheckArgument(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); - CheckArgument(i != d_map.end(), name, "No command-line flag by that name, or not supported."); + CVC4::CheckArgument(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); - CheckArgument(i != d_map.end(), name, "No command-line flag by that name, or not supported."); + CVC4::CheckArgument(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); - CheckArgument(i != d_map.end(), name, "No command-line flag by that name, or not supported."); + CVC4::CheckArgument(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); - CheckArgument(i != d_map.end(), name, "No command-line flag by that name, or not supported."); + CVC4::CheckArgument(i != d_map.end(), name, "No command-line flag by that name, or not supported."); (*i).second = sv; } @@ -1063,8 +1066,8 @@ Type ValidityChecker::intType() { Type ValidityChecker::subrangeType(const Expr& l, const Expr& r) { bool noLowerBound = l.getType().isString() && l.getConst<string>() == "_NEGINF"; bool noUpperBound = r.getType().isString() && r.getConst<string>() == "_POSINF"; - CheckArgument(noLowerBound || (l.getKind() == CVC4::kind::CONST_RATIONAL && l.getConst<Rational>().isIntegral()), l); - CheckArgument(noUpperBound || (r.getKind() == CVC4::kind::CONST_RATIONAL && r.getConst<Rational>().isIntegral()), r); + 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); 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)); @@ -1123,7 +1126,7 @@ Type ValidityChecker::dataType(const std::string& name, const std::string& constructor, const std::vector<std::string>& selectors, const std::vector<Expr>& types) { - CheckArgument(selectors.size() == types.size(), types, "expected selectors and types vectors to be of equal length"); + CVC4::CheckArgument(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; @@ -1137,8 +1140,8 @@ 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) { - CheckArgument(constructors.size() == selectors.size(), selectors, "expected constructors and selectors vectors to be of equal length"); - CheckArgument(constructors.size() == types.size(), types, "expected constructors and types vectors to be of equal length"); + 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"); vector<string> nv; vector< vector<string> > cv; vector< vector< vector<string> > > sv; @@ -1149,7 +1152,7 @@ Type ValidityChecker::dataType(const std::string& name, tv.push_back(types); vector<Type> dtts; dataType(nv, cv, sv, tv, dtts); - AlwaysAssert(dtts.size() == 1); + assert(dtts.size() == 1); return dtts[0]; } @@ -1159,19 +1162,19 @@ void ValidityChecker::dataType(const std::vector<std::string>& names, const std::vector<std::vector<std::vector<Expr> > >& types, std::vector<Type>& returnTypes) { - CheckArgument(names.size() == constructors.size(), constructors, "expected names and constructors vectors to be of equal length"); - CheckArgument(names.size() == selectors.size(), selectors, "expected names and selectors vectors to be of equal length"); - CheckArgument(names.size() == types.size(), types, "expected names and types vectors to be of equal length"); + 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"); vector<CVC4::Datatype> dv; // Set up the datatype specifications. for(unsigned i = 0; i < names.size(); ++i) { CVC4::Datatype dt(names[i]); - CheckArgument(constructors[i].size() == selectors[i].size(), "expected sub-vectors in constructors and selectors vectors to match in size"); - CheckArgument(constructors[i].size() == types[i].size(), "expected sub-vectors in constructors and types vectors to match in size"); + 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"); for(unsigned j = 0; j < constructors[i].size(); ++j) { CVC4::DatatypeConstructor ctor(constructors[i][j]); - CheckArgument(selectors[i][j].size() == types[i][j].size(), types, "expected sub-vectors in selectors and types vectors to match in size"); + CVC4::CheckArgument(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<string>())); @@ -1200,10 +1203,10 @@ 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. - CheckArgument(d_constructors.find((*j).getName()) == d_constructors.end(), constructors, "cannot have two constructors with the same name in a ValidityChecker"); + CVC4::CheckArgument(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) { - CheckArgument(d_selectors.find((*k).getName()) == d_selectors.end(), selectors, "cannot have two selectors with the same name in a ValidityChecker"); + CVC4::CheckArgument(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()); } } @@ -1219,7 +1222,7 @@ Type ValidityChecker::arrayType(const Type& typeIndex, const Type& typeData) { } Type ValidityChecker::bitvecType(int n) { - CheckArgument(n >= 0, n, "cannot construct a bitvector type of negative size"); + CVC4::CheckArgument(n >= 0, n, "cannot construct a bitvector type of negative size"); return d_em->mkBitVectorType(n); } @@ -1255,7 +1258,7 @@ Expr ValidityChecker::varExpr(const std::string& name, const Type& type) { Expr ValidityChecker::varExpr(const std::string& name, const Type& type, const Expr& def) { - FatalAssert(def.getType() == type, "expected types to match"); + CVC4::CheckArgument(def.getType() == type, def, "expected types to match"); d_parserContext->defineVar(name, def); } @@ -1281,7 +1284,7 @@ Type ValidityChecker::getBaseType(const Type& t) { if(type.isReal()) { return d_em->realType(); } - Assert(!type.isInteger());// should be handled by Real + assert(!type.isInteger());// should be handled by Real if(type.isBoolean()) { return d_em->booleanType(); } @@ -1418,7 +1421,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 - CheckArgument(children.size() > 0, children); + CVC4::CheckArgument(children.size() > 0, children); return (children.size() == 1) ? children[0] : Expr(d_em->mkExpr(CVC4::kind::AND, *reinterpret_cast<const vector<CVC4::Expr>*>(&children))); } @@ -1428,7 +1431,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 - CheckArgument(children.size() > 0, children); + CVC4::CheckArgument(children.size() > 0, children); return (children.size() == 1) ? children[0] : Expr(d_em->mkExpr(CVC4::kind::OR, *reinterpret_cast<const vector<CVC4::Expr>*>(&children))); } @@ -1450,7 +1453,7 @@ Expr ValidityChecker::iteExpr(const Expr& ifpart, const Expr& thenpart, } Expr ValidityChecker::distinctExpr(const std::vector<Expr>& children) { - CheckArgument(children.size() > 1, children, "it makes no sense to create a `distinct' expression with only one child"); + CVC4::CheckArgument(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); @@ -1462,7 +1465,7 @@ Op ValidityChecker::createOp(const std::string& name, const Type& type) { Op ValidityChecker::createOp(const std::string& name, const Type& type, const Expr& def) { - CheckArgument(def.getType() == type, type, + CVC4::CheckArgument(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()); @@ -1512,7 +1515,7 @@ Expr ValidityChecker::ratExpr(const std::string& n, int base) { if(n.find(".") == string::npos) { return d_em->mkConst(Rational(n, base)); } else { - CheckArgument(base == 10, base, "unsupported base for decimal parsing"); + CVC4::CheckArgument(base == 10, base, "unsupported base for decimal parsing"); return d_em->mkConst(Rational::fromDecimal(n)); } } @@ -1527,7 +1530,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 - CheckArgument(children.size() > 0, children); + CVC4::CheckArgument(children.size() > 0, children); return (children.size() == 1) ? children[0] : Expr(d_em->mkExpr(CVC4::kind::PLUS, *reinterpret_cast<const vector<CVC4::Expr>*>(&children))); } @@ -1618,9 +1621,9 @@ Expr ValidityChecker::newBVConstExpr(const std::vector<bool>& bits) { Expr ValidityChecker::newBVConstExpr(const Rational& r, int len) { // implementation based on CVC3's TheoryBitvector::newBVConstExpr() - CheckArgument(r.getDenominator() == 1, r, "ValidityChecker::newBVConstExpr: " + CVC4::CheckArgument(r.getDenominator() == 1, r, "ValidityChecker::newBVConstExpr: " "not an integer: `%s'", r.toString().c_str()); - CheckArgument(len > 0, len, "ValidityChecker::newBVConstExpr: " + CVC4::CheckArgument(len > 0, len, "ValidityChecker::newBVConstExpr: " "len = %d", len); string s(r.toString(2)); @@ -1643,8 +1646,8 @@ Expr ValidityChecker::newBVConstExpr(const Rational& r, int len) { } Expr ValidityChecker::newConcatExpr(const Expr& t1, const Expr& t2) { - CheckArgument(t1.getType().isBitVector(), t1, "can only concat a bitvector, not a `%s'", t1.getType().toString().c_str()); - CheckArgument(t2.getType().isBitVector(), t2, "can only concat a bitvector, not a `%s'", t2.getType().toString().c_str()); + 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()); return d_em->mkExpr(CVC4::kind::BITVECTOR_CONCAT, t1, t2); } @@ -1655,29 +1658,29 @@ Expr ValidityChecker::newConcatExpr(const std::vector<Expr>& kids) { } Expr ValidityChecker::newBVExtractExpr(const Expr& e, int hi, int low) { - CheckArgument(e.getType().isBitVector(), e, "can only bvextract from a bitvector, not a `%s'", e.getType().toString().c_str()); - CheckArgument(hi >= low, hi, "extraction [%d:%d] is bad; possibly inverted?", hi, low); - CheckArgument(low >= 0, low, "extraction [%d:%d] is bad (negative)", hi, low); - 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); + 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); return d_em->mkExpr(CVC4::kind::BITVECTOR_EXTRACT, d_em->mkConst(CVC4::BitVectorExtract(hi, low)), e); } Expr ValidityChecker::newBVNegExpr(const Expr& t1) { // CVC3's BVNEG => SMT-LIBv2 bvnot - CheckArgument(t1.getType().isBitVector(), t1, "can only bvneg a bitvector, not a `%s'", t1.getType().toString().c_str()); + CVC4::CheckArgument(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) { - CheckArgument(t1.getType().isBitVector(), t1, "can only bvand a bitvector, not a `%s'", t1.getType().toString().c_str()); - CheckArgument(t2.getType().isBitVector(), t2, "can only bvand a bitvector, not a `%s'", t2.getType().toString().c_str()); + 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()); 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 - CheckArgument(kids.size() > 1, kids, "BITVECTOR_AND must have at least 2 children"); + CVC4::CheckArgument(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()) { @@ -1687,14 +1690,14 @@ Expr ValidityChecker::newBVAndExpr(const std::vector<Expr>& kids) { } Expr ValidityChecker::newBVOrExpr(const Expr& t1, const Expr& t2) { - CheckArgument(t1.getType().isBitVector(), t1, "can only bvor a bitvector, not a `%s'", t1.getType().toString().c_str()); - CheckArgument(t2.getType().isBitVector(), t2, "can only bvor a bitvector, not a `%s'", t2.getType().toString().c_str()); + 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()); 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 - CheckArgument(kids.size() > 1, kids, "BITVECTOR_OR must have at least 2 children"); + CVC4::CheckArgument(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()) { @@ -1704,14 +1707,14 @@ Expr ValidityChecker::newBVOrExpr(const std::vector<Expr>& kids) { } Expr ValidityChecker::newBVXorExpr(const Expr& t1, const Expr& t2) { - CheckArgument(t1.getType().isBitVector(), t1, "can only bvxor a bitvector, not a `%s'", t1.getType().toString().c_str()); - CheckArgument(t2.getType().isBitVector(), t2, "can only bvxor a bitvector, not a `%s'", t2.getType().toString().c_str()); + 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()); 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 - CheckArgument(kids.size() > 1, kids, "BITVECTOR_XOR must have at least 2 children"); + CVC4::CheckArgument(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()) { @@ -1721,14 +1724,14 @@ Expr ValidityChecker::newBVXorExpr(const std::vector<Expr>& kids) { } Expr ValidityChecker::newBVXnorExpr(const Expr& t1, const Expr& t2) { - CheckArgument(t1.getType().isBitVector(), t1, "can only bvxnor a bitvector, not a `%s'", t1.getType().toString().c_str()); - CheckArgument(t2.getType().isBitVector(), t2, "can only bvxnor a bitvector, not a `%s'", t2.getType().toString().c_str()); + 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()); 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 - CheckArgument(kids.size() > 1, kids, "BITVECTOR_XNOR must have at least 2 children"); + CVC4::CheckArgument(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()) { @@ -1738,73 +1741,73 @@ Expr ValidityChecker::newBVXnorExpr(const std::vector<Expr>& kids) { } Expr ValidityChecker::newBVNandExpr(const Expr& t1, const Expr& t2) { - CheckArgument(t1.getType().isBitVector(), t1, "can only bvnand a bitvector, not a `%s'", t1.getType().toString().c_str()); - CheckArgument(t2.getType().isBitVector(), t2, "can only bvnand a bitvector, not a `%s'", t2.getType().toString().c_str()); + 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()); return d_em->mkExpr(CVC4::kind::BITVECTOR_NAND, t1, t2); } Expr ValidityChecker::newBVNorExpr(const Expr& t1, const Expr& t2) { - CheckArgument(t1.getType().isBitVector(), t1, "can only bvnor a bitvector, not a `%s'", t1.getType().toString().c_str()); - CheckArgument(t2.getType().isBitVector(), t2, "can only bvnor a bitvector, not a `%s'", t2.getType().toString().c_str()); + 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()); return d_em->mkExpr(CVC4::kind::BITVECTOR_NOR, t1, t2); } Expr ValidityChecker::newBVCompExpr(const Expr& t1, const Expr& t2) { - CheckArgument(t1.getType().isBitVector(), t1, "can only bvcomp a bitvector, not a `%s'", t1.getType().toString().c_str()); - CheckArgument(t2.getType().isBitVector(), t2, "can only bvcomp a bitvector, not a `%s'", t2.getType().toString().c_str()); + 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()); return d_em->mkExpr(CVC4::kind::BITVECTOR_COMP, t1, t2); } Expr ValidityChecker::newBVLTExpr(const Expr& t1, const Expr& t2) { - CheckArgument(t1.getType().isBitVector(), t1, "can only bvlt a bitvector, not a `%s'", t1.getType().toString().c_str()); - CheckArgument(t2.getType().isBitVector(), t2, "can only bvlt a bitvector, not a `%s'", t2.getType().toString().c_str()); + 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()); return d_em->mkExpr(CVC4::kind::BITVECTOR_ULT, t1, t2); } Expr ValidityChecker::newBVLEExpr(const Expr& t1, const Expr& t2) { - CheckArgument(t1.getType().isBitVector(), t1, "can only bvle a bitvector, not a `%s'", t1.getType().toString().c_str()); - CheckArgument(t2.getType().isBitVector(), t2, "can only bvle a bitvector, not a `%s'", t2.getType().toString().c_str()); + 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()); return d_em->mkExpr(CVC4::kind::BITVECTOR_ULE, t1, t2); } Expr ValidityChecker::newBVSLTExpr(const Expr& t1, const Expr& t2) { - CheckArgument(t1.getType().isBitVector(), t1, "can only bvslt a bitvector, not a `%s'", t1.getType().toString().c_str()); - CheckArgument(t2.getType().isBitVector(), t2, "can only bvslt a bitvector, not a `%s'", t2.getType().toString().c_str()); + 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()); return d_em->mkExpr(CVC4::kind::BITVECTOR_SLT, t1, t2); } Expr ValidityChecker::newBVSLEExpr(const Expr& t1, const Expr& t2) { - CheckArgument(t1.getType().isBitVector(), t1, "can only bvsle a bitvector, not a `%s'", t1.getType().toString().c_str()); - CheckArgument(t2.getType().isBitVector(), t2, "can only bvsle a bitvector, not a `%s'", t2.getType().toString().c_str()); + 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()); return d_em->mkExpr(CVC4::kind::BITVECTOR_SLE, t1, t2); } Expr ValidityChecker::newSXExpr(const Expr& t1, int len) { - CheckArgument(t1.getType().isBitVector(), t1, "can only sx a bitvector, not a `%s'", t1.getType().toString().c_str()); - CheckArgument(len >= 0, len, "must sx by a positive integer"); - 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()); + 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()); 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 - CheckArgument(t1.getType().isBitVector(), t1, "can only bvuminus a bitvector, not a `%s'", t1.getType().toString().c_str()); + CVC4::CheckArgument(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) { - CheckArgument(t1.getType().isBitVector(), t1, "can only bvsub a bitvector, not a `%s'", t1.getType().toString().c_str()); - CheckArgument(t2.getType().isBitVector(), t2, "can only bvsub by a bitvector, not a `%s'", t2.getType().toString().c_str()); + 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()); 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) { - CheckArgument(len >= 0, len, + CVC4::CheckArgument(len >= 0, len, "padding length must be a non-negative integer, not %d", len); - CheckArgument(e.getType().isBitVector(), e, + CVC4::CheckArgument(e.getType().isBitVector(), e, "input to bitvector operation must be a bitvector"); unsigned size = CVC4::BitVectorType(e.getType()).getSize(); @@ -1823,89 +1826,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 - CheckArgument(kids.size() > 1, kids, "BITVECTOR_PLUS must have at least 2 children"); + CVC4::CheckArgument(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(); - CheckArgument(unsigned(numbits) == size, numbits, + CVC4::CheckArgument(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) { - CheckArgument(t1.getType().isBitVector(), t1, "can only bvplus a bitvector, not a `%s'", t1.getType().toString().c_str()); - CheckArgument(t2.getType().isBitVector(), t2, "can only bvplus a bitvector, not a `%s'", t2.getType().toString().c_str()); + 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()); Expr e = d_em->mkExpr(CVC4::kind::BITVECTOR_PLUS, bvpad(numbits, t1), bvpad(numbits, t2)); unsigned size = CVC4::BitVectorType(e.getType()).getSize(); - CheckArgument(unsigned(numbits) == size, numbits, + CVC4::CheckArgument(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) { - CheckArgument(t1.getType().isBitVector(), t1, "can only bvmult a bitvector, not a `%s'", t1.getType().toString().c_str()); - CheckArgument(t2.getType().isBitVector(), t2, "can only bvmult by a bitvector, not a `%s'", t2.getType().toString().c_str()); + 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()); Expr e = d_em->mkExpr(CVC4::kind::BITVECTOR_MULT, bvpad(numbits, t1), bvpad(numbits, t2)); unsigned size = CVC4::BitVectorType(e.getType()).getSize(); - CheckArgument(unsigned(numbits) == size, numbits, + CVC4::CheckArgument(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) { - CheckArgument(t1.getType().isBitVector(), t1, "can only bvudiv a bitvector, not a `%s'", t1.getType().toString().c_str()); - CheckArgument(t2.getType().isBitVector(), t2, "can only bvudiv by a bitvector, not a `%s'", t2.getType().toString().c_str()); + 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()); return d_em->mkExpr(CVC4::kind::BITVECTOR_UDIV, t1, t2); } Expr ValidityChecker::newBVURemExpr(const Expr& t1, const Expr& t2) { - CheckArgument(t1.getType().isBitVector(), t1, "can only bvurem a bitvector, not a `%s'", t1.getType().toString().c_str()); - CheckArgument(t2.getType().isBitVector(), t2, "can only bvurem by a bitvector, not a `%s'", t2.getType().toString().c_str()); + 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()); return d_em->mkExpr(CVC4::kind::BITVECTOR_UREM, t1, t2); } Expr ValidityChecker::newBVSDivExpr(const Expr& t1, const Expr& t2) { - CheckArgument(t1.getType().isBitVector(), t1, "can only bvsdiv a bitvector, not a `%s'", t1.getType().toString().c_str()); - CheckArgument(t2.getType().isBitVector(), t2, "can only bvsdiv by a bitvector, not a `%s'", t2.getType().toString().c_str()); + 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()); return d_em->mkExpr(CVC4::kind::BITVECTOR_SDIV, t1, t2); } Expr ValidityChecker::newBVSRemExpr(const Expr& t1, const Expr& t2) { - CheckArgument(t1.getType().isBitVector(), t1, "can only bvsrem a bitvector, not a `%s'", t1.getType().toString().c_str()); - CheckArgument(t2.getType().isBitVector(), t2, "can only bvsrem by a bitvector, not a `%s'", t2.getType().toString().c_str()); + 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()); return d_em->mkExpr(CVC4::kind::BITVECTOR_SREM, t1, t2); } Expr ValidityChecker::newBVSModExpr(const Expr& t1, const Expr& t2) { - CheckArgument(t1.getType().isBitVector(), t1, "can only bvsmod a bitvector, not a `%s'", t1.getType().toString().c_str()); - CheckArgument(t2.getType().isBitVector(), t2, "can only bvsmod by a bitvector, not a `%s'", t2.getType().toString().c_str()); + 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()); return d_em->mkExpr(CVC4::kind::BITVECTOR_SMOD, t1, t2); } Expr ValidityChecker::newFixedLeftShiftExpr(const Expr& t1, int r) { - CheckArgument(t1.getType().isBitVector(), t1, "can only left-shift a bitvector, not a `%s'", t1.getType().toString().c_str()); - CheckArgument(r >= 0, r, "left shift amount must be >= 0 (you passed %d)", 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); // 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) { - CheckArgument(t1.getType().isBitVector(), t1, "can only right-shift a bitvector, not a `%s'", t1.getType().toString().c_str()); - CheckArgument(r >= 0, r, "const-width left shift amount must be >= 0 (you passed %d)", 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); // 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) { - CheckArgument(t1.getType().isBitVector(), t1, "can only right-shift a bitvector, not a `%s'", t1.getType().toString().c_str()); - CheckArgument(r >= 0, r, "right shift amount must be >= 0 (you passed %d)", 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); // 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. @@ -1913,20 +1916,20 @@ Expr ValidityChecker::newFixedRightShiftExpr(const Expr& t1, int r) { } Expr ValidityChecker::newBVSHL(const Expr& t1, const Expr& t2) { - CheckArgument(t1.getType().isBitVector(), t1, "can only right-shift a bitvector, not a `%s'", t1.getType().toString().c_str()); - CheckArgument(t2.getType().isBitVector(), t2, "can only right-shift by a bitvector, not a `%s'", t2.getType().toString().c_str()); + 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()); return d_em->mkExpr(CVC4::kind::BITVECTOR_SHL, t1, t2); } Expr ValidityChecker::newBVLSHR(const Expr& t1, const Expr& t2) { - CheckArgument(t1.getType().isBitVector(), t1, "can only right-shift a bitvector, not a `%s'", t1.getType().toString().c_str()); - CheckArgument(t2.getType().isBitVector(), t2, "can only right-shift by a bitvector, not a `%s'", t2.getType().toString().c_str()); + 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()); return d_em->mkExpr(CVC4::kind::BITVECTOR_LSHR, t1, t2); } Expr ValidityChecker::newBVASHR(const Expr& t1, const Expr& t2) { - CheckArgument(t1.getType().isBitVector(), t1, "can only right-shift a bitvector, not a `%s'", t1.getType().toString().c_str()); - CheckArgument(t2.getType().isBitVector(), t2, "can only right-shift by a bitvector, not a `%s'", t2.getType().toString().c_str()); + 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()); return d_em->mkExpr(CVC4::kind::BITVECTOR_ASHR, t1, t2); } @@ -1951,16 +1954,16 @@ Expr ValidityChecker::tupleUpdateExpr(const Expr& tuple, int index, Expr ValidityChecker::datatypeConsExpr(const std::string& constructor, const std::vector<Expr>& args) { ConstructorMap::const_iterator i = d_constructors.find(constructor); - AlwaysAssert(i != d_constructors.end(), "no such constructor"); + CVC4::CheckArgument(i != d_constructors.end(), constructor, "no such constructor"); const CVC4::Datatype& dt = *(*i).second; const CVC4::DatatypeConstructor& ctor = dt[constructor]; - AlwaysAssert(ctor.getNumArgs() == args.size(), "arity mismatch in constructor application"); + CVC4::CheckArgument(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); - AlwaysAssert(i != d_selectors.end(), "no such selector"); + CVC4::CheckArgument(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]; @@ -1969,7 +1972,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); - AlwaysAssert(i != d_constructors.end(), "no such constructor"); + CVC4::CheckArgument(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); @@ -2122,7 +2125,7 @@ void ValidityChecker::returnFromCheck() { } void ValidityChecker::getUserAssumptions(std::vector<Expr>& assumptions) { - CheckArgument(assumptions.empty(), assumptions, "assumptions arg must be empty"); + CVC4::CheckArgument(assumptions.empty(), assumptions, "assumptions arg must be empty"); vector<CVC4::Expr> v = d_smt->getAssertions(); assumptions.swap(*reinterpret_cast<vector<Expr>*>(&v)); } @@ -2157,7 +2160,7 @@ QueryResult ValidityChecker::tryModelGeneration() { } FormulaValue ValidityChecker::value(const Expr& e) { - CheckArgument(e.getType() == d_em->booleanType(), e, "argument must be a formula"); + CVC4::CheckArgument(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) { @@ -2175,7 +2178,7 @@ Expr ValidityChecker::getValue(const Expr& e) { } bool ValidityChecker::inconsistent(std::vector<Expr>& assumptions) { - CheckArgument(assumptions.empty(), assumptions, "assumptions vector should be empty on entry"); + CVC4::CheckArgument(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)); @@ -2235,12 +2238,12 @@ void ValidityChecker::pop() { } void ValidityChecker::popto(int stackLevel) { - CheckArgument(stackLevel >= 0, stackLevel, - "Cannot pop to a negative stack level %d", stackLevel); - CheckArgument(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); + CVC4::CheckArgument(stackLevel >= 0, stackLevel, + "Cannot pop to a negative stack level %d", stackLevel); + CVC4::CheckArgument(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); while(unsigned(stackLevel) < d_stackLevel) { pop(); } @@ -2259,13 +2262,13 @@ void ValidityChecker::popScope() { } void ValidityChecker::poptoScope(int scopeLevel) { - CheckArgument(scopeLevel >= 0, scopeLevel, - "Cannot pop to a negative scope level %d", scopeLevel); - CheckArgument(unsigned(scopeLevel) <= d_parserContext->getDeclarationLevel(), - scopeLevel, - "Cannot pop to a scope level higher than the current one! " - "At scope level %u, user requested scope level %d", - d_parserContext->getDeclarationLevel(), scopeLevel); + CVC4::CheckArgument(scopeLevel >= 0, scopeLevel, + "Cannot pop to a negative scope level %d", scopeLevel); + CVC4::CheckArgument(unsigned(scopeLevel) <= d_parserContext->getDeclarationLevel(), + scopeLevel, + "Cannot pop to a scope level higher than the current one! " + "At scope level %u, user requested scope level %d", + d_parserContext->getDeclarationLevel(), scopeLevel); while(unsigned(scopeLevel) < d_parserContext->getDeclarationLevel()) { popScope(); } diff --git a/src/compat/cvc3_compat.h b/src/compat/cvc3_compat.h index 31d914b58..911e967ca 100644 --- a/src/compat/cvc3_compat.h +++ b/src/compat/cvc3_compat.h @@ -68,16 +68,6 @@ #include <map> #include <utility> -// some #defines that CVC3 exported to userspace :( -#ifdef CVC4_DEBUG -# define DebugAssert(cond, str) Assert((cond), "CVC3-style assertion failed: %s", std::string(str).c_str()); -# define IF_DEBUG(x) x -#else -# define DebugAssert(...) -# define IF_DEBUG(x) -#endif -#define FatalAssert(cond, str) AlwaysAssert((cond), "CVC3-style assertion failed: %s", std::string(str).c_str()); - //class CInterface; namespace CVC3 { diff --git a/src/expr/kind_template.h b/src/expr/kind_template.h index fc7d838a1..2857dc5d8 100644 --- a/src/expr/kind_template.h +++ b/src/expr/kind_template.h @@ -24,7 +24,7 @@ #include <iostream> #include <sstream> -#include "util/Assert.h" +#include "util/exception.h" namespace CVC4 { namespace kind { @@ -100,6 +100,7 @@ struct KindHashFunction { */ enum TypeConstant { ${type_constant_list} +#line 104 "${template}" LAST_TYPE };/* enum TypeConstant */ @@ -115,6 +116,7 @@ struct TypeConstantHashFunction { inline std::ostream& operator<<(std::ostream& out, TypeConstant typeConstant) { switch(typeConstant) { ${type_constant_descriptions} +#line 120 "${template}" default: out << "UNKNOWN_TYPE_CONSTANT"; break; @@ -126,8 +128,9 @@ namespace theory { enum TheoryId { ${theory_enum} +#line 132 "${template}" THEORY_LAST -}; +};/* enum TheoryId */ const TheoryId THEORY_FIRST = static_cast<TheoryId>(0); const TheoryId THEORY_SAT_SOLVER = THEORY_LAST; @@ -139,6 +142,7 @@ inline TheoryId& operator ++ (TheoryId& id) { inline std::ostream& operator<<(std::ostream& out, TheoryId theoryId) { switch(theoryId) { ${theory_descriptions} +#line 146 "${template}" default: out << "UNKNOWN_THEORY"; break; @@ -148,23 +152,28 @@ ${theory_descriptions} inline TheoryId kindToTheoryId(::CVC4::Kind k) { switch(k) { + case kind::UNDEFINED_KIND: + case kind::NULL_EXPR: + break; ${kind_to_theory_id} - default: - Unhandled(k); +#line 160 "${template}" + case kind::LAST_KIND: + break; } + throw IllegalArgumentException("", "k", __PRETTY_FUNCTION__, "bad kind"); } inline TheoryId typeConstantToTheoryId(::CVC4::TypeConstant typeConstant) { switch(typeConstant) { ${type_constant_to_theory_id} - default: - Unhandled(typeConstant); +#line 170 "${template}" + case LAST_TYPE: + break; } + throw IllegalArgumentException("", "k", __PRETTY_FUNCTION__, "bad type constant"); } -}/* theory namespace */ - - +}/* CVC4::theory namespace */ }/* CVC4 namespace */ #endif /* __CVC4__KIND_H */ diff --git a/src/expr/symbol_table.cpp b/src/expr/symbol_table.cpp index e3bd898ef..71745f649 100644 --- a/src/expr/symbol_table.cpp +++ b/src/expr/symbol_table.cpp @@ -50,7 +50,7 @@ SymbolTable::~SymbolTable() { } void SymbolTable::bind(const std::string& name, Expr obj, - bool levelZero) throw(AssertionException) { + bool levelZero) throw() { CheckArgument(!obj.isNull(), obj, "cannot bind to a null Expr"); ExprManagerScope ems(obj); if(levelZero) d_exprMap->insertAtContextLevelZero(name, obj); @@ -58,7 +58,7 @@ void SymbolTable::bind(const std::string& name, Expr obj, } void SymbolTable::bindDefinedFunction(const std::string& name, Expr obj, - bool levelZero) throw(AssertionException) { + bool levelZero) throw() { CheckArgument(!obj.isNull(), obj, "cannot bind to a null Expr"); ExprManagerScope ems(obj); if(levelZero){ @@ -84,7 +84,7 @@ bool SymbolTable::isBoundDefinedFunction(Expr func) const throw() { return d_functions->contains(func); } -Expr SymbolTable::lookup(const std::string& name) const throw(AssertionException) { +Expr SymbolTable::lookup(const std::string& name) const throw() { return (*d_exprMap->find(name)).second; } @@ -121,7 +121,7 @@ bool SymbolTable::isBoundType(const std::string& name) const throw() { return d_typeMap->find(name) != d_typeMap->end(); } -Type SymbolTable::lookupType(const std::string& name) const throw(AssertionException) { +Type SymbolTable::lookupType(const std::string& name) const throw() { pair<vector<Type>, Type> p = (*d_typeMap->find(name)).second; Assert(p.first.size() == 0, "type constructor arity is wrong: " @@ -131,7 +131,7 @@ Type SymbolTable::lookupType(const std::string& name) const throw(AssertionExcep } Type SymbolTable::lookupType(const std::string& name, - const std::vector<Type>& params) const throw(AssertionException) { + const std::vector<Type>& params) const throw() { pair<vector<Type>, Type> p = (*d_typeMap->find(name)).second; Assert(p.first.size() == params.size(), "type constructor arity is wrong: " diff --git a/src/expr/symbol_table.h b/src/expr/symbol_table.h index 3f24d10f8..6db335ded 100644 --- a/src/expr/symbol_table.h +++ b/src/expr/symbol_table.h @@ -79,7 +79,7 @@ public: * @param obj the expression to bind to <code>name</code> * @param levelZero set if the binding must be done at level 0 */ - void bind(const std::string& name, Expr obj, bool levelZero = false) throw(AssertionException); + void bind(const std::string& name, Expr obj, bool levelZero = false) throw(); /** * Bind a function body to a name in the current scope. If @@ -93,7 +93,7 @@ public: * @param obj the expression to bind to <code>name</code> * @param levelZero set if the binding must be done at level 0 */ - void bindDefinedFunction(const std::string& name, Expr obj, bool levelZero = false) throw(AssertionException); + void bindDefinedFunction(const std::string& name, Expr obj, bool levelZero = false) throw(); /** * Bind a type to a name in the current scope. If <code>name</code> @@ -159,7 +159,7 @@ public: * @param name the identifier to lookup * @returns the expression bound to <code>name</code> in the current scope. */ - Expr lookup(const std::string& name) const throw(AssertionException); + Expr lookup(const std::string& name) const throw(); /** * Lookup a bound type. @@ -167,7 +167,7 @@ public: * @param name the type identifier to lookup * @returns the type bound to <code>name</code> in the current scope. */ - Type lookupType(const std::string& name) const throw(AssertionException); + Type lookupType(const std::string& name) const throw(); /** * Lookup a bound parameterized type. @@ -178,7 +178,7 @@ public: * the current scope. */ Type lookupType(const std::string& name, - const std::vector<Type>& params) const throw(AssertionException); + const std::vector<Type>& params) const throw(); /** * Lookup the arity of a bound parameterized type. diff --git a/src/expr/type.cpp b/src/expr/type.cpp index 5a00a538c..c94094b2b 100644 --- a/src/expr/type.cpp +++ b/src/expr/type.cpp @@ -23,7 +23,7 @@ #include "expr/node_manager.h" #include "expr/type.h" #include "expr/type_node.h" -#include "util/Assert.h" +#include "util/exception.h" using namespace std; @@ -88,8 +88,8 @@ bool Type::isComparableTo(Type t) const { } Type& Type::operator=(const Type& t) { - Assert(d_typeNode != NULL, "Unexpected NULL typenode pointer!"); - Assert(t.d_typeNode != NULL, "Unexpected NULL typenode pointer!"); + CheckArgument(d_typeNode != NULL, this, "Unexpected NULL typenode pointer!"); + CheckArgument(t.d_typeNode != NULL, t, "Unexpected NULL typenode pointer!"); if(this != &t) { if(d_nodeManager == t.d_nodeManager) { @@ -202,9 +202,9 @@ bool Type::isBoolean() const { } /** Cast to a Boolean type */ -Type::operator BooleanType() const throw(AssertionException) { +Type::operator BooleanType() const throw(IllegalArgumentException) { NodeManagerScope nms(d_nodeManager); - Assert(isNull() || isBoolean()); + CheckArgument(isNull() || isBoolean(), this); return BooleanType(*this); } @@ -215,9 +215,9 @@ bool Type::isInteger() const { } /** Cast to a integer type */ -Type::operator IntegerType() const throw(AssertionException) { +Type::operator IntegerType() const throw(IllegalArgumentException) { NodeManagerScope nms(d_nodeManager); - Assert(isNull() || isInteger()); + CheckArgument(isNull() || isInteger(), this); return IntegerType(*this); } @@ -228,9 +228,9 @@ bool Type::isReal() const { } /** Cast to a real type */ -Type::operator RealType() const throw(AssertionException) { +Type::operator RealType() const throw(IllegalArgumentException) { NodeManagerScope nms(d_nodeManager); - Assert(isNull() || isReal()); + CheckArgument(isNull() || isReal(), this); return RealType(*this); } @@ -241,9 +241,9 @@ bool Type::isString() const { } /** Cast to a string type */ -Type::operator StringType() const throw(AssertionException) { +Type::operator StringType() const throw(IllegalArgumentException) { NodeManagerScope nms(d_nodeManager); - Assert(isNull() || isString()); + CheckArgument(isNull() || isString(), this); return StringType(*this); } @@ -254,16 +254,16 @@ bool Type::isBitVector() const { } /** Cast to a bit-vector type */ -Type::operator BitVectorType() const throw(AssertionException) { +Type::operator BitVectorType() const throw(IllegalArgumentException) { NodeManagerScope nms(d_nodeManager); - Assert(isNull() || isBitVector()); + CheckArgument(isNull() || isBitVector(), this); return BitVectorType(*this); } /** Cast to a Constructor type */ -Type::operator DatatypeType() const throw(AssertionException) { +Type::operator DatatypeType() const throw(IllegalArgumentException) { NodeManagerScope nms(d_nodeManager); - Assert(isNull() || isDatatype()); + CheckArgument(isNull() || isDatatype(), this); return DatatypeType(*this); } @@ -274,9 +274,9 @@ bool Type::isDatatype() const { } /** Cast to a Constructor type */ -Type::operator ConstructorType() const throw(AssertionException) { +Type::operator ConstructorType() const throw(IllegalArgumentException) { NodeManagerScope nms(d_nodeManager); - Assert(isNull() || isConstructor()); + CheckArgument(isNull() || isConstructor(), this); return ConstructorType(*this); } @@ -287,9 +287,9 @@ bool Type::isConstructor() const { } /** Cast to a Selector type */ -Type::operator SelectorType() const throw(AssertionException) { +Type::operator SelectorType() const throw(IllegalArgumentException) { NodeManagerScope nms(d_nodeManager); - Assert(isNull() || isSelector()); + CheckArgument(isNull() || isSelector(), this); return SelectorType(*this); } @@ -300,9 +300,9 @@ bool Type::isSelector() const { } /** Cast to a Tester type */ -Type::operator TesterType() const throw(AssertionException) { +Type::operator TesterType() const throw(IllegalArgumentException) { NodeManagerScope nms(d_nodeManager); - Assert(isNull() || isTester()); + CheckArgument(isNull() || isTester(), this); return TesterType(*this); } @@ -328,9 +328,9 @@ bool Type::isPredicate() const { } /** Cast to a function type */ -Type::operator FunctionType() const throw(AssertionException) { +Type::operator FunctionType() const throw(IllegalArgumentException) { NodeManagerScope nms(d_nodeManager); - Assert(isNull() || isFunction()); + CheckArgument(isNull() || isFunction(), this); return FunctionType(*this); } @@ -341,9 +341,9 @@ bool Type::isTuple() const { } /** Cast to a tuple type */ -Type::operator TupleType() const throw(AssertionException) { +Type::operator TupleType() const throw(IllegalArgumentException) { NodeManagerScope nms(d_nodeManager); - Assert(isNull() || isTuple()); + CheckArgument(isNull() || isTuple(), this); return TupleType(*this); } @@ -354,9 +354,9 @@ bool Type::isSExpr() const { } /** Cast to a symbolic expression type */ -Type::operator SExprType() const throw(AssertionException) { +Type::operator SExprType() const throw(IllegalArgumentException) { NodeManagerScope nms(d_nodeManager); - Assert(isNull() || isSExpr()); + CheckArgument(isNull() || isSExpr(), this); return SExprType(*this); } @@ -367,7 +367,7 @@ bool Type::isArray() const { } /** Cast to an array type */ -Type::operator ArrayType() const throw(AssertionException) { +Type::operator ArrayType() const throw(IllegalArgumentException) { NodeManagerScope nms(d_nodeManager); return ArrayType(*this); } @@ -379,9 +379,9 @@ bool Type::isSort() const { } /** Cast to a sort type */ -Type::operator SortType() const throw(AssertionException) { +Type::operator SortType() const throw(IllegalArgumentException) { NodeManagerScope nms(d_nodeManager); - Assert(isNull() || isSort()); + CheckArgument(isNull() || isSort(), this); return SortType(*this); } @@ -392,9 +392,9 @@ bool Type::isSortConstructor() const { } /** Cast to a sort constructor type */ -Type::operator SortConstructorType() const throw(AssertionException) { +Type::operator SortConstructorType() const throw(IllegalArgumentException) { NodeManagerScope nms(d_nodeManager); - Assert(isNull() || isSortConstructor()); + CheckArgument(isNull() || isSortConstructor(), this); return SortConstructorType(*this); } @@ -405,9 +405,9 @@ bool Type::isPredicateSubtype() const { } /** Cast to a predicate subtype */ -Type::operator PredicateSubtype() const throw(AssertionException) { +Type::operator PredicateSubtype() const throw(IllegalArgumentException) { NodeManagerScope nms(d_nodeManager); - Assert(isNull() || isPredicateSubtype()); + CheckArgument(isNull() || isPredicateSubtype(), this); return PredicateSubtype(*this); } @@ -418,9 +418,9 @@ bool Type::isSubrange() const { } /** Cast to a predicate subtype */ -Type::operator SubrangeType() const throw(AssertionException) { +Type::operator SubrangeType() const throw(IllegalArgumentException) { NodeManagerScope nms(d_nodeManager); - Assert(isNull() || isSubrange()); + CheckArgument(isNull() || isSubrange(), this); return SubrangeType(*this); } @@ -438,7 +438,7 @@ vector<Type> FunctionType::getArgTypes() const { Type FunctionType::getRangeType() const { NodeManagerScope nms(d_nodeManager); - Assert(isNull() || isFunction()); + CheckArgument(isNull() || isFunction(), this); return makeType(d_typeNode->getRangeType()); } @@ -503,92 +503,92 @@ SortType SortConstructorType::instantiate(const std::vector<Type>& params) const return SortType(makeType(d_nodeManager->mkSort(*d_typeNode, paramsNodes))); } -BooleanType::BooleanType(const Type& t) throw(AssertionException) : +BooleanType::BooleanType(const Type& t) throw(IllegalArgumentException) : Type(t) { - Assert(isNull() || isBoolean()); + CheckArgument(isNull() || isBoolean(), this); } -IntegerType::IntegerType(const Type& t) throw(AssertionException) : +IntegerType::IntegerType(const Type& t) throw(IllegalArgumentException) : Type(t) { - Assert(isNull() || isInteger()); + CheckArgument(isNull() || isInteger(), this); } -RealType::RealType(const Type& t) throw(AssertionException) : +RealType::RealType(const Type& t) throw(IllegalArgumentException) : Type(t) { - Assert(isNull() || isReal()); + CheckArgument(isNull() || isReal(), this); } -StringType::StringType(const Type& t) throw(AssertionException) : +StringType::StringType(const Type& t) throw(IllegalArgumentException) : Type(t) { - Assert(isNull() || isString()); + CheckArgument(isNull() || isString(), this); } -BitVectorType::BitVectorType(const Type& t) throw(AssertionException) : +BitVectorType::BitVectorType(const Type& t) throw(IllegalArgumentException) : Type(t) { - Assert(isNull() || isBitVector()); + CheckArgument(isNull() || isBitVector(), this); } -DatatypeType::DatatypeType(const Type& t) throw(AssertionException) : +DatatypeType::DatatypeType(const Type& t) throw(IllegalArgumentException) : Type(t) { - Assert(isNull() || isDatatype()); + CheckArgument(isNull() || isDatatype(), this); } -ConstructorType::ConstructorType(const Type& t) throw(AssertionException) : +ConstructorType::ConstructorType(const Type& t) throw(IllegalArgumentException) : Type(t) { - Assert(isNull() || isConstructor()); + CheckArgument(isNull() || isConstructor(), this); } -SelectorType::SelectorType(const Type& t) throw(AssertionException) : +SelectorType::SelectorType(const Type& t) throw(IllegalArgumentException) : Type(t) { - Assert(isNull() || isSelector()); + CheckArgument(isNull() || isSelector(), this); } -TesterType::TesterType(const Type& t) throw(AssertionException) : +TesterType::TesterType(const Type& t) throw(IllegalArgumentException) : Type(t) { - Assert(isNull() || isTester()); + CheckArgument(isNull() || isTester(), this); } -FunctionType::FunctionType(const Type& t) throw(AssertionException) : +FunctionType::FunctionType(const Type& t) throw(IllegalArgumentException) : Type(t) { - Assert(isNull() || isFunction()); + CheckArgument(isNull() || isFunction(), this); } -TupleType::TupleType(const Type& t) throw(AssertionException) : +TupleType::TupleType(const Type& t) throw(IllegalArgumentException) : Type(t) { - Assert(isNull() || isTuple()); + CheckArgument(isNull() || isTuple(), this); } -SExprType::SExprType(const Type& t) throw(AssertionException) : +SExprType::SExprType(const Type& t) throw(IllegalArgumentException) : Type(t) { - Assert(isNull() || isSExpr()); + CheckArgument(isNull() || isSExpr(), this); } -ArrayType::ArrayType(const Type& t) throw(AssertionException) : +ArrayType::ArrayType(const Type& t) throw(IllegalArgumentException) : Type(t) { - Assert(isNull() || isArray()); + CheckArgument(isNull() || isArray(), this); } -SortType::SortType(const Type& t) throw(AssertionException) : +SortType::SortType(const Type& t) throw(IllegalArgumentException) : Type(t) { - Assert(isNull() || isSort()); + CheckArgument(isNull() || isSort(), this); } SortConstructorType::SortConstructorType(const Type& t) - throw(AssertionException) : + throw(IllegalArgumentException) : Type(t) { - Assert(isNull() || isSortConstructor()); + CheckArgument(isNull() || isSortConstructor(), this); } PredicateSubtype::PredicateSubtype(const Type& t) - throw(AssertionException) : + throw(IllegalArgumentException) : Type(t) { - Assert(isNull() || isPredicateSubtype()); + CheckArgument(isNull() || isPredicateSubtype(), this); } SubrangeType::SubrangeType(const Type& t) - throw(AssertionException) : + throw(IllegalArgumentException) : Type(t) { - Assert(isNull() || isSubrange()); + CheckArgument(isNull() || isSubrange(), this); } unsigned BitVectorType::getSize() const { @@ -625,7 +625,7 @@ std::vector<Type> ConstructorType::getArgTypes() const { const Datatype& DatatypeType::getDatatype() const { if( d_typeNode->isParametricDatatype() ) { - Assert( (*d_typeNode)[0].getKind() == kind::DATATYPE_TYPE ); + CheckArgument( (*d_typeNode)[0].getKind() == kind::DATATYPE_TYPE, this); const Datatype& dt = (*d_typeNode)[0].getConst<Datatype>(); return dt; } else { diff --git a/src/expr/type.h b/src/expr/type.h index caaf256f5..39d50fd31 100644 --- a/src/expr/type.h +++ b/src/expr/type.h @@ -26,7 +26,6 @@ #include <limits.h> #include <stdint.h> -#include "util/Assert.h" #include "util/cardinality.h" #include "util/subrange_bound.h" @@ -64,7 +63,7 @@ class PredicateSubtype; class SubrangeType; class Type; -/** Strategy for hashing Types */ +/** Hash function for Types */ struct CVC4_PUBLIC TypeHashFunction { /** Return a hash code for type t */ size_t operator()(const CVC4::Type& t) const; @@ -238,7 +237,7 @@ public: * Cast this type to a Boolean type * @return the BooleanType */ - operator BooleanType() const throw(AssertionException); + operator BooleanType() const throw(IllegalArgumentException); /** * Is this the integer type? @@ -250,7 +249,7 @@ public: * Cast this type to a integer type * @return the IntegerType */ - operator IntegerType() const throw(AssertionException); + operator IntegerType() const throw(IllegalArgumentException); /** * Is this the real type? @@ -262,7 +261,7 @@ public: * Cast this type to a real type * @return the RealType */ - operator RealType() const throw(AssertionException); + operator RealType() const throw(IllegalArgumentException); /** * Is this the string type? @@ -274,7 +273,7 @@ public: * Cast this type to a string type * @return the StringType */ - operator StringType() const throw(AssertionException); + operator StringType() const throw(IllegalArgumentException); /** * Is this the bit-vector type? @@ -286,7 +285,7 @@ public: * Cast this type to a bit-vector type * @return the BitVectorType */ - operator BitVectorType() const throw(AssertionException); + operator BitVectorType() const throw(IllegalArgumentException); /** * Is this a function type? @@ -305,7 +304,7 @@ public: * Cast this type to a function type * @return the FunctionType */ - operator FunctionType() const throw(AssertionException); + operator FunctionType() const throw(IllegalArgumentException); /** * Is this a tuple type? @@ -317,7 +316,7 @@ public: * Cast this type to a tuple type * @return the TupleType */ - operator TupleType() const throw(AssertionException); + operator TupleType() const throw(IllegalArgumentException); /** * Is this a symbolic expression type? @@ -329,7 +328,7 @@ public: * Cast this type to a symbolic expression type * @return the SExprType */ - operator SExprType() const throw(AssertionException); + operator SExprType() const throw(IllegalArgumentException); /** * Is this an array type? @@ -341,7 +340,7 @@ public: * Cast this type to an array type * @return the ArrayType */ - operator ArrayType() const throw(AssertionException); + operator ArrayType() const throw(IllegalArgumentException); /** * Is this a datatype type? @@ -353,7 +352,7 @@ public: * Cast this type to a datatype type * @return the DatatypeType */ - operator DatatypeType() const throw(AssertionException); + operator DatatypeType() const throw(IllegalArgumentException); /** * Is this a constructor type? @@ -365,7 +364,7 @@ public: * Cast this type to a constructor type * @return the ConstructorType */ - operator ConstructorType() const throw(AssertionException); + operator ConstructorType() const throw(IllegalArgumentException); /** * Is this a selector type? @@ -377,7 +376,7 @@ public: * Cast this type to a selector type * @return the SelectorType */ - operator SelectorType() const throw(AssertionException); + operator SelectorType() const throw(IllegalArgumentException); /** * Is this a tester type? @@ -389,7 +388,7 @@ public: * Cast this type to a tester type * @return the TesterType */ - operator TesterType() const throw(AssertionException); + operator TesterType() const throw(IllegalArgumentException); /** * Is this a sort kind? @@ -401,7 +400,7 @@ public: * Cast this type to a sort type * @return the sort type */ - operator SortType() const throw(AssertionException); + operator SortType() const throw(IllegalArgumentException); /** * Is this a sort constructor kind? @@ -413,7 +412,7 @@ public: * Cast this type to a sort constructor type * @return the sort constructor type */ - operator SortConstructorType() const throw(AssertionException); + operator SortConstructorType() const throw(IllegalArgumentException); /** * Is this a predicate subtype? @@ -425,7 +424,7 @@ public: * Cast this type to a predicate subtype * @return the predicate subtype */ - operator PredicateSubtype() const throw(AssertionException); + operator PredicateSubtype() const throw(IllegalArgumentException); /** * Is this an integer subrange type? @@ -437,7 +436,7 @@ public: * Cast this type to an integer subrange type * @return the integer subrange type */ - operator SubrangeType() const throw(AssertionException); + operator SubrangeType() const throw(IllegalArgumentException); /** * Outputs a string representation of this type to the stream. @@ -459,7 +458,7 @@ class CVC4_PUBLIC BooleanType : public Type { public: /** Construct from the base type */ - BooleanType(const Type& type = Type()) throw(AssertionException); + BooleanType(const Type& type = Type()) throw(IllegalArgumentException); };/* class BooleanType */ /** @@ -470,7 +469,7 @@ class CVC4_PUBLIC IntegerType : public Type { public: /** Construct from the base type */ - IntegerType(const Type& type = Type()) throw(AssertionException); + IntegerType(const Type& type = Type()) throw(IllegalArgumentException); };/* class IntegerType */ /** @@ -481,7 +480,7 @@ class CVC4_PUBLIC RealType : public Type { public: /** Construct from the base type */ - RealType(const Type& type = Type()) throw(AssertionException); + RealType(const Type& type = Type()) throw(IllegalArgumentException); };/* class RealType */ /** @@ -492,7 +491,7 @@ class CVC4_PUBLIC StringType : public Type { public: /** Construct from the base type */ - StringType(const Type& type) throw(AssertionException); + StringType(const Type& type) throw(IllegalArgumentException); };/* class StringType */ /** @@ -503,7 +502,7 @@ class CVC4_PUBLIC FunctionType : public Type { public: /** Construct from the base type */ - FunctionType(const Type& type = Type()) throw(AssertionException); + FunctionType(const Type& type = Type()) throw(IllegalArgumentException); /** Get the argument types */ std::vector<Type> getArgTypes() const; @@ -520,7 +519,7 @@ class CVC4_PUBLIC TupleType : public Type { public: /** Construct from the base type */ - TupleType(const Type& type = Type()) throw(AssertionException); + TupleType(const Type& type = Type()) throw(IllegalArgumentException); /** Get the constituent types */ std::vector<Type> getTypes() const; @@ -534,7 +533,7 @@ class CVC4_PUBLIC SExprType : public Type { public: /** Construct from the base type */ - SExprType(const Type& type = Type()) throw(AssertionException); + SExprType(const Type& type = Type()) throw(IllegalArgumentException); /** Get the constituent types */ std::vector<Type> getTypes() const; @@ -548,7 +547,7 @@ class CVC4_PUBLIC ArrayType : public Type { public: /** Construct from the base type */ - ArrayType(const Type& type = Type()) throw(AssertionException); + ArrayType(const Type& type = Type()) throw(IllegalArgumentException); /** Get the index type */ Type getIndexType() const; @@ -565,7 +564,7 @@ class CVC4_PUBLIC SortType : public Type { public: /** Construct from the base type */ - SortType(const Type& type = Type()) throw(AssertionException); + SortType(const Type& type = Type()) throw(IllegalArgumentException); /** Get the name of the sort */ std::string getName() const; @@ -586,7 +585,7 @@ class CVC4_PUBLIC SortConstructorType : public Type { public: /** Construct from the base type */ - SortConstructorType(const Type& type = Type()) throw(AssertionException); + SortConstructorType(const Type& type = Type()) throw(IllegalArgumentException); /** Get the name of the sort constructor */ std::string getName() const; @@ -607,7 +606,7 @@ class CVC4_PUBLIC PredicateSubtype : public Type { public: /** Construct from the base type */ - PredicateSubtype(const Type& type = Type()) throw(AssertionException); + PredicateSubtype(const Type& type = Type()) throw(IllegalArgumentException); /** Get the LAMBDA defining this predicate subtype */ Expr getPredicate() const; @@ -625,7 +624,7 @@ class CVC4_PUBLIC SubrangeType : public Type { public: /** Construct from the base type */ - SubrangeType(const Type& type = Type()) throw(AssertionException); + SubrangeType(const Type& type = Type()) throw(IllegalArgumentException); /** Get the bounds defining this integer subrange */ SubrangeBounds getSubrangeBounds() const; @@ -640,7 +639,7 @@ class CVC4_PUBLIC BitVectorType : public Type { public: /** Construct from the base type */ - BitVectorType(const Type& type = Type()) throw(AssertionException); + BitVectorType(const Type& type = Type()) throw(IllegalArgumentException); /** * Returns the size of the bit-vector type. @@ -659,7 +658,7 @@ class CVC4_PUBLIC DatatypeType : public Type { public: /** Construct from the base type */ - DatatypeType(const Type& type = Type()) throw(AssertionException); + DatatypeType(const Type& type = Type()) throw(IllegalArgumentException); /** Get the underlying datatype */ const Datatype& getDatatype() const; @@ -705,7 +704,7 @@ class CVC4_PUBLIC ConstructorType : public Type { public: /** Construct from the base type */ - ConstructorType(const Type& type = Type()) throw(AssertionException); + ConstructorType(const Type& type = Type()) throw(IllegalArgumentException); /** Get the range type */ DatatypeType getRangeType() const; @@ -727,7 +726,7 @@ class CVC4_PUBLIC SelectorType : public Type { public: /** Construct from the base type */ - SelectorType(const Type& type = Type()) throw(AssertionException); + SelectorType(const Type& type = Type()) throw(IllegalArgumentException); /** Get the domain type for this selector (the datatype type) */ DatatypeType getDomain() const; @@ -745,7 +744,7 @@ class CVC4_PUBLIC TesterType : public Type { public: /** Construct from the base type */ - TesterType(const Type& type = Type()) throw(AssertionException); + TesterType(const Type& type = Type()) throw(IllegalArgumentException); /** Get the type that this tester tests (the datatype type) */ DatatypeType getDomain() const; diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp index a3086d96c..3eba7ff6a 100644 --- a/src/main/driver_unified.cpp +++ b/src/main/driver_unified.cpp @@ -33,7 +33,6 @@ #include "parser/parser_exception.h" #include "expr/expr_manager.h" #include "expr/command.h" -#include "util/Assert.h" #include "util/configuration.h" #include "options/options.h" #include "main/command_executor.h" diff --git a/src/main/interactive_shell.cpp b/src/main/interactive_shell.cpp index 719c8f61d..4f75779af 100644 --- a/src/main/interactive_shell.cpp +++ b/src/main/interactive_shell.cpp @@ -37,6 +37,7 @@ #include "util/language.h" #include <string.h> +#include <cassert> #if HAVE_LIBREADLINE # include <readline/readline.h> @@ -121,7 +122,9 @@ InteractiveShell::InteractiveShell(ExprManager& exprManager, commandsEnd = tptp_commands + sizeof(tptp_commands) / sizeof(*tptp_commands); break; default: - Unhandled(lang); + std::stringstream ss; + ss << "internal error: unhandled language " << lang; + throw Exception(ss.str()); } d_usingReadline = true; int err = ::read_history(d_historyFilename.c_str()); @@ -195,12 +198,12 @@ Command* InteractiveShell::readCommand() { while(true) { Debug("interactive") << "Input now '" << input << line << "'" << endl << flush; - Assert( !(d_in.fail() && !d_in.eof()) || line.empty() ); + assert( !(d_in.fail() && !d_in.eof()) || line.empty() ); /* Check for failure. */ if(d_in.fail() && !d_in.eof()) { /* This should only happen if the input line was empty. */ - Assert( line.empty() ); + assert( line.empty() ); d_in.clear(); } @@ -229,7 +232,7 @@ Command* InteractiveShell::readCommand() { if(!d_usingReadline) { /* Extract the newline delimiter from the stream too */ int c CVC4_UNUSED = d_in.get(); - Assert( c == '\n' ); + assert( c == '\n' ); Debug("interactive") << "Next char is '" << (char)c << "'" << endl << flush; } diff --git a/src/main/main.cpp b/src/main/main.cpp index 73936526f..e3196bb4e 100644 --- a/src/main/main.cpp +++ b/src/main/main.cpp @@ -33,7 +33,6 @@ #include "expr/expr_manager.h" #include "smt/smt_engine.h" #include "expr/command.h" -#include "util/Assert.h" #include "util/configuration.h" #include "main/options.h" #include "theory/uf/options.h" diff --git a/src/main/util.cpp b/src/main/util.cpp index 523486f80..90e960673 100644 --- a/src/main/util.cpp +++ b/src/main/util.cpp @@ -25,10 +25,10 @@ #include <sys/resource.h> #include <unistd.h> -#include "util/Assert.h" #include "util/exception.h" #include "options/options.h" #include "util/statistics.h" +#include "util/tls.h" #include "smt/smt_engine.h" #include "cvc4autoconfig.h" @@ -39,6 +39,11 @@ using CVC4::Exception; using namespace std; namespace CVC4 { + +#ifdef CVC4_DEBUG + extern CVC4_THREADLOCAL(const char*) s_debugLastException; +#endif /* CVC4_DEBUG */ + namespace main { size_t cvc4StackSize; diff --git a/src/options/Makefile.am b/src/options/Makefile.am index 1eb3fdac4..d4d5b2861 100644 --- a/src/options/Makefile.am +++ b/src/options/Makefile.am @@ -177,6 +177,8 @@ options-stamp: options_holder_template.h options_template.cpp ../smt/smt_options @srcdir@/../smt/smt_options_template.cpp @builddir@/../smt/smt_options.cpp \ @top_builddir@/doc/cvc4.1_template @top_builddir@/doc/cvc4.1 \ @top_builddir@/doc/libcvc4.3_template @top_builddir@/doc/libcvc4.3 \ + @top_builddir@/doc/SmtEngine.3cvc4_template @top_builddir@/doc/SmtEngine.3cvc4 \ + @top_builddir@/doc/options.3cvc4_template @top_builddir@/doc/options.3cvc4 \ -t \ @srcdir@/base_options_template.h @srcdir@/base_options_template.cpp \ $(foreach o,$(OPTIONS_FILES),"$(srcdir)/$(o)" "$(patsubst %/,%,$(dir $(o)))") \ diff --git a/src/options/mkoptions b/src/options/mkoptions index f023686ad..8e098cb95 100755 --- a/src/options/mkoptions +++ b/src/options/mkoptions @@ -72,11 +72,14 @@ common_manpage_documentation= remaining_manpage_documentation= common_manpage_smt_documentation= remaining_manpage_smt_documentation= +common_manpage_internals_documentation= +remaining_manpage_internals_documentation= seen_module=false seen_endmodule=false expect_doc=false expect_doc_alternate=false +seen_doc=false n_long=256 internal= @@ -137,6 +140,10 @@ function module { .TP .I \"`echo "$module_name" | tr a-z A-Z` OPTIONS\" " + remaining_manpage_internals_documentation="${remaining_manpage_internals_documentation} +.TP +.I \"`echo "$module_name" | tr a-z A-Z` OPTIONS\" +" } function endmodule { @@ -203,6 +210,7 @@ function handle_option { expect_doc=true fi expect_doc_alternate=false + seen_doc=false # scan ahead to see where the type is type_pos=2 @@ -923,6 +931,7 @@ function doc { # doc text... check_module_seen expect_doc=false + seen_doc=true if [ -z "$short_option" -a -z "$long_option" ]; then if [ -n "$short_option_alternate" -o -n "$long_option_alternate" ]; then @@ -935,10 +944,6 @@ function doc { fi fi - if [ "$category" = UNDOCUMENTED ]; then - return - fi - the_opt= if [ "$long_option" ]; then the_opt="--$long_option" @@ -951,9 +956,6 @@ function doc { fi elif [ "$short_option" ]; then the_opt="-$short_option" - elif [ -z "$smtname" ]; then - # nothing to document - return fi if ! $options_already_documented; then @@ -998,7 +1000,7 @@ function doc { common_manpage_documentation="${common_manpage_documentation} .IP \"$the_opt\" $mandoc" - else + elif [ "$category" != UNDOCUMENTED ]; then remaining_documentation="${remaining_documentation}\\n\" #line $lineno \"$kf\" \"$(echo "$doc_line" | sed 's,'\'',\\'\'',g;s,",\\",g')" @@ -1008,7 +1010,7 @@ $mandoc" fi fi - if [ "$smtname" ]; then + if [ "$smtname" -a "$category" != UNDOCUMENTED ]; then if [ "$category" = COMMON ]; then common_manpage_smt_documentation="${common_manpage_smt_documentation} .TP @@ -1021,8 +1023,30 @@ $mandoc" ($type) $mansmtdoc" fi fi + if [ "$internal" != - ]; then + if [ -z "$default_value" ]; then + typedefault="($type)" + else + typedefault="($type, default = $default_value)" + fi + if [ "$category" = COMMON ]; then + common_manpage_internals_documentation="${common_manpage_internals_documentation} +.TP +.B \"$internal\" +$typedefault +.br +$mansmtdoc" + else + remaining_manpage_internals_documentation="${remaining_manpage_internals_documentation} +.TP +.B \"$internal\" +$typedefault +.br +$mansmtdoc" + fi + fi else - if [ "$the_opt" ]; then + if [ "$the_opt" -a "$category" != UNDOCUMENTED ]; then if [ "$category" = COMMON ]; then common_manpage_documentation="${common_manpage_documentation} $@" @@ -1032,12 +1056,24 @@ $@" fi fi - if [ "$smtname" ]; then + if [ "$smtname" -a "$category" != UNDOCUMENTED ]; then + if [ "$category" = COMMON ]; then common_manpage_smt_documentation="${common_manpage_smt_documentation} $@" - else + else remaining_manpage_smt_documentation="${remaining_manpage_smt_documentation} $@" + fi + fi + + if [ "$internal" != - ]; then + if [ "$category" = COMMON ]; then + common_manpage_internals_documentation="${common_manpage_internals_documentation} +$@" + else + remaining_manpage_internals_documentation="${remaining_manpage_internals_documentation} +$@" + fi fi fi } @@ -1147,6 +1183,29 @@ function check_doc { echo "$kf:$lineno: warning: SMT option $smtname is lacking documentation" >&2 fi expect_doc=false + elif ! $seen_doc; then + if [ -n "$internal" -a "$internal" != - ]; then + if [ -z "$default_value" ]; then + typedefault="($type)" + else + typedefault="($type, default = $default_value)" + fi + if [ "$category" = COMMON ]; then + common_manpage_internals_documentation="${common_manpage_internals_documentation} +.TP +.B \"$internal\" +$typedefault +.br +[undocumented]" + else + remaining_manpage_internals_documentation="${remaining_manpage_internals_documentation} +.TP +.B \"$internal\" +$typedefault +.br +[undocumented]" + fi + fi fi if $expect_doc_alternate; then @@ -1280,7 +1339,7 @@ EOF fi } -total=$(($#/2+19*${#templates[@]})) +total=$(($#/2+21*${#templates[@]})) count=0 while [ $# -gt 0 ]; do kf="$1"; shift @@ -1383,6 +1442,8 @@ for var in \ remaining_manpage_documentation \ common_manpage_smt_documentation \ remaining_manpage_smt_documentation \ + common_manpage_internals_documentation \ + remaining_manpage_internals_documentation \ ; do let ++count progress "$output" $count $total diff --git a/src/parser/antlr_input.cpp b/src/parser/antlr_input.cpp index ea593e7da..0dc833ee5 100644 --- a/src/parser/antlr_input.cpp +++ b/src/parser/antlr_input.cpp @@ -36,7 +36,6 @@ #include "parser/smt2/smt2_input.h" #include "parser/tptp/tptp_input.h" #include "util/output.h" -#include "util/Assert.h" using namespace std; using namespace CVC4; @@ -51,7 +50,7 @@ AntlrInputStream::AntlrInputStream(std::string name, bool fileIsTemporary) : InputStream(name,fileIsTemporary), d_input(input) { - AlwaysAssert( input != NULL ); + assert( input != NULL ); } AntlrInputStream::~AntlrInputStream() { @@ -65,7 +64,7 @@ pANTLR3_INPUT_STREAM AntlrInputStream::getAntlr3InputStream() const { AntlrInputStream* AntlrInputStream::newFileInputStream(const std::string& name, bool useMmap) - throw (InputStreamException, AssertionException) { + throw (InputStreamException) { pANTLR3_INPUT_STREAM input = NULL; if( useMmap ) { input = MemoryMappedInputBufferNew(name); @@ -87,7 +86,7 @@ AntlrInputStream* AntlrInputStream::newStreamInputStream(std::istream& input, const std::string& name, bool lineBuffered) - throw (InputStreamException, AssertionException) { + throw (InputStreamException) { pANTLR3_INPUT_STREAM inputStream = NULL; @@ -162,10 +161,10 @@ AntlrInputStream::newStreamInputStream(std::istream& input, AntlrInputStream* AntlrInputStream::newStringInputStream(const std::string& input, const std::string& name) - throw (InputStreamException, AssertionException) { + throw (InputStreamException) { char* inputStr = strdup(input.c_str()); char* nameStr = strdup(name.c_str()); - AlwaysAssert( inputStr!=NULL && nameStr!=NULL ); + assert( inputStr!=NULL && nameStr!=NULL ); #ifdef CVC4_ANTLR3_OLD_INPUT_STREAM pANTLR3_INPUT_STREAM inputStream = antlr3NewAsciiStringInPlaceStream((pANTLR3_UINT8) inputStr, @@ -207,7 +206,9 @@ AntlrInput* AntlrInput::newInput(InputLanguage lang, AntlrInputStream& inputStre break; default: - Unhandled(lang); + std::stringstream ss; + ss << "internal error: unhandled language " << lang << " in AntlrInput::newInput"; + throw ParserException(ss.str()); } return input; @@ -261,11 +262,11 @@ pANTLR3_COMMON_TOKEN_STREAM AntlrInput::getTokenStream() { void AntlrInput::lexerError(pANTLR3_BASE_RECOGNIZER recognizer) { pANTLR3_LEXER lexer = (pANTLR3_LEXER)(recognizer->super); - AlwaysAssert(lexer!=NULL); + assert(lexer!=NULL); Parser *parser = (Parser*)(lexer->super); - AlwaysAssert(parser!=NULL); + assert(parser!=NULL); AntlrInput *input = (AntlrInput*) parser->getInput(); - AlwaysAssert(input!=NULL); + assert(input!=NULL); /* Call the error display routine *if* there's not already a * parse error pending. If a parser error is pending, this @@ -280,7 +281,7 @@ void AntlrInput::warning(const std::string& message) { } void AntlrInput::parseError(const std::string& message) - throw (ParserException, AssertionException) { + throw (ParserException) { Debug("parser") << "Throwing exception: " << getInputStream()->getName() << ":" << d_lexer->getLine(d_lexer) << "." diff --git a/src/parser/antlr_input.h b/src/parser/antlr_input.h index 2d468a7d6..613390ca1 100644 --- a/src/parser/antlr_input.h +++ b/src/parser/antlr_input.h @@ -27,12 +27,12 @@ #include <stdexcept> #include <string> #include <vector> +#include <cassert> #include "parser/bounded_token_buffer.h" #include "parser/parser_exception.h" #include "parser/input.h" -#include "util/Assert.h" #include "util/bitvector.h" #include "util/integer.h" #include "util/rational.h" @@ -73,13 +73,13 @@ public: */ static AntlrInputStream* newFileInputStream(const std::string& name, bool useMmap = false) - throw (InputStreamException, AssertionException); + throw (InputStreamException); /** Create an input from an istream. */ static AntlrInputStream* newStreamInputStream(std::istream& input, const std::string& name, bool lineBuffered = false) - throw (InputStreamException, AssertionException); + throw (InputStreamException); /** Create a string input. * @@ -88,7 +88,7 @@ public: */ static AntlrInputStream* newStringInputStream(const std::string& input, const std::string& name) - throw (InputStreamException, AssertionException); + throw (InputStreamException); };/* class AntlrInputStream */ class Parser; @@ -212,7 +212,7 @@ protected: * Throws a <code>ParserException</code> with the given message. */ void parseError(const std::string& msg) - throw (ParserException, AssertionException); + throw (ParserException); /** Set the ANTLR3 lexer for this input. */ void setAntlr3Lexer(pANTLR3_LEXER pLexer); @@ -255,7 +255,7 @@ inline std::string AntlrInput::tokenTextSubstr(pANTLR3_COMMON_TOKEN token, ANTLR3_MARKER start = token->getStartIndex(token); // Its the last character of the token (not the one just after) ANTLR3_MARKER end = token->getStopIndex(token); - Assert( start < end ); + assert( start < end ); if( index > (size_t) end - start ) { std::stringstream ss; ss << "Out-of-bounds substring index: " << index; diff --git a/src/parser/antlr_input_imports.cpp b/src/parser/antlr_input_imports.cpp index d714c4975..9c92846bb 100644 --- a/src/parser/antlr_input_imports.cpp +++ b/src/parser/antlr_input_imports.cpp @@ -57,7 +57,6 @@ #include "parser/antlr_input.h" #include "parser/parser.h" #include "parser/parser_exception.h" -#include "util/Assert.h" using namespace std; @@ -92,11 +91,11 @@ void AntlrInput::reportError(pANTLR3_BASE_RECOGNIZER recognizer) { // Dig the CVC4 objects out of the ANTLR3 mess pANTLR3_PARSER antlr3Parser = (pANTLR3_PARSER)(recognizer->super); - AlwaysAssert(antlr3Parser!=NULL); + assert(antlr3Parser!=NULL); Parser *parser = (Parser*)(antlr3Parser->super); - AlwaysAssert(parser!=NULL); + assert(parser!=NULL); AntlrInput *input = (AntlrInput*) parser->getInput() ; - AlwaysAssert(input!=NULL); + assert(input!=NULL); // Signal we are in error recovery now recognizer->state->errorRecovery = ANTLR3_TRUE; @@ -235,7 +234,7 @@ void AntlrInput::reportError(pANTLR3_BASE_RECOGNIZER recognizer) { } } } else { - Unreachable("Parse error with empty set of expected tokens."); + assert(false);//("Parse error with empty set of expected tokens."); } } break; @@ -257,7 +256,7 @@ void AntlrInput::reportError(pANTLR3_BASE_RECOGNIZER recognizer) { // then we are just going to report what we know about the // token. // - Unhandled("Unexpected exception in parser."); + assert(false);//("Unexpected exception in parser."); break; } diff --git a/src/parser/antlr_line_buffered_input.cpp b/src/parser/antlr_line_buffered_input.cpp index b42562f72..0facbddaf 100644 --- a/src/parser/antlr_line_buffered_input.cpp +++ b/src/parser/antlr_line_buffered_input.cpp @@ -20,9 +20,9 @@ #include <antlr3.h> #include <iostream> #include <string> +#include <cassert> #include "util/output.h" -#include "util/Assert.h" namespace CVC4 { namespace parser { @@ -242,7 +242,7 @@ myLA(pANTLR3_INT_STREAM is, ANTLR3_INT32 la) { in.getline((((char*)input->data) + input->sizeBuf), 1024); } input->sizeBuf += strlen(((char*)input->data) + input->sizeBuf); - Assert(*(((char*)input->data) + input->sizeBuf) == '\0'); + assert(*(((char*)input->data) + input->sizeBuf) == '\0'); Debug("pipe") << "SIZEBUF now " << input->sizeBuf << std::endl; *(((char*)input->data) + input->sizeBuf) = '\n'; ++input->sizeBuf; diff --git a/src/parser/bounded_token_buffer.cpp b/src/parser/bounded_token_buffer.cpp index d63d3afe0..7edbf7b7f 100644 --- a/src/parser/bounded_token_buffer.cpp +++ b/src/parser/bounded_token_buffer.cpp @@ -56,7 +56,7 @@ #include <antlr3tokenstream.h> #include "parser/bounded_token_buffer.h" -#include "util/Assert.h" +#include <cassert> namespace CVC4 { namespace parser { @@ -142,7 +142,7 @@ BoundedTokenBufferSourceNew(ANTLR3_UINT32 k, pANTLR3_TOKEN_SOURCE source) pANTLR3_COMMON_TOKEN_STREAM stream; - AlwaysAssert( k > 0 ); + assert( k > 0 ); /* Memory for the interface structure */ @@ -235,7 +235,7 @@ static pANTLR3_COMMON_TOKEN tokLT(pANTLR3_TOKEN_STREAM ts, ANTLR3_INT32 k) { buffer = (pBOUNDED_TOKEN_BUFFER) cts->super; /* k must be in the range [-buffer->k..buffer->k] */ - AlwaysAssert( k <= (ANTLR3_INT32)buffer->k + assert( k <= (ANTLR3_INT32)buffer->k && -k <= (ANTLR3_INT32)buffer->k ); if(k == 0) { @@ -244,7 +244,7 @@ static pANTLR3_COMMON_TOKEN tokLT(pANTLR3_TOKEN_STREAM ts, ANTLR3_INT32 k) { /* Initialize the buffer on our first call. */ if( EXPECT_FALSE(buffer->empty == ANTLR3_TRUE) ) { - AlwaysAssert( buffer->tokenBuffer != NULL ); + assert( buffer->tokenBuffer != NULL ); buffer->tokenBuffer[ 0 ] = nextToken(buffer); buffer->maxIndex = 0; buffer->currentIndex = 0; @@ -257,7 +257,7 @@ static pANTLR3_COMMON_TOKEN tokLT(pANTLR3_TOKEN_STREAM ts, ANTLR3_INT32 k) { kIndex = buffer->currentIndex + k - 1; } else { /* Can't look behind more tokens than we've consumed. */ - AlwaysAssert( -k <= (ANTLR3_INT32)buffer->currentIndex ); + assert( -k <= (ANTLR3_INT32)buffer->currentIndex ); /* look-behind token k is at offset -k */ kIndex = buffer->currentIndex + k; } @@ -289,7 +289,8 @@ dbgTokLT (pANTLR3_TOKEN_STREAM ts, ANTLR3_INT32 k) static pANTLR3_COMMON_TOKEN get (pANTLR3_TOKEN_STREAM ts, ANTLR3_UINT32 i) { - Unreachable(); + assert(false);// unimplemented + return NULL; } static pANTLR3_TOKEN_SOURCE @@ -308,19 +309,22 @@ setTokenSource ( pANTLR3_TOKEN_STREAM ts, static pANTLR3_STRING toString (pANTLR3_TOKEN_STREAM ts) { - Unimplemented("toString(ts)"); + assert(false);// unimplemented + return NULL; } static pANTLR3_STRING toStringSS(pANTLR3_TOKEN_STREAM ts, ANTLR3_UINT32 start, ANTLR3_UINT32 stop) { - Unimplemented("toStringSS(ts, %u, %u)", start, stop); + assert(false);// unimplemented + return NULL; } static pANTLR3_STRING toStringTT (pANTLR3_TOKEN_STREAM ts, pANTLR3_COMMON_TOKEN start, pANTLR3_COMMON_TOKEN stop) { - Unimplemented("toStringTT(ts, %u, %u)", start, stop); + assert(false);// unimplemented + return NULL; } /** Move the input pointer to the next incoming token. The stream @@ -379,7 +383,8 @@ _LA (pANTLR3_INT_STREAM is, ANTLR3_INT32 i) static ANTLR3_UINT32 dbgLA (pANTLR3_INT_STREAM is, ANTLR3_INT32 i) { - Unreachable(); + assert(false); + return 0; } static ANTLR3_MARKER @@ -394,7 +399,8 @@ mark (pANTLR3_INT_STREAM is) static ANTLR3_MARKER dbgMark (pANTLR3_INT_STREAM is) { - Unreachable(); + assert(false); + return 0; } static void @@ -406,7 +412,8 @@ release (pANTLR3_INT_STREAM is, ANTLR3_MARKER mark) static ANTLR3_UINT32 size (pANTLR3_INT_STREAM is) { - Unreachable(); + assert(false); + return 0; } static ANTLR3_MARKER @@ -426,12 +433,12 @@ tindex (pANTLR3_INT_STREAM is) static void dbgRewindLast (pANTLR3_INT_STREAM is) { - Unreachable(); + assert(false); } static void rewindLast (pANTLR3_INT_STREAM is) { - Unreachable(); + assert(false); } static void rewindStream (pANTLR3_INT_STREAM is, ANTLR3_MARKER marker) @@ -441,7 +448,7 @@ rewindStream (pANTLR3_INT_STREAM is, ANTLR3_MARKER marker) static void dbgRewindStream (pANTLR3_INT_STREAM is, ANTLR3_MARKER marker) { - Unreachable(); + assert(false); } static void @@ -458,7 +465,7 @@ seek (pANTLR3_INT_STREAM is, ANTLR3_MARKER index) static void dbgSeek (pANTLR3_INT_STREAM is, ANTLR3_MARKER index) { - Unreachable(); + assert(false); } static pANTLR3_COMMON_TOKEN nextToken(pBOUNDED_TOKEN_BUFFER buffer) { diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g index 4577b504c..b496aa91c 100644 --- a/src/parser/cvc/Cvc.g +++ b/src/parser/cvc/Cvc.g @@ -288,7 +288,9 @@ int getOperatorPrecedence(int type) { case IN_TOK: return 33; default: - Unhandled(CvcParserTokenNames[type]); + std::stringstream ss; + ss << "internal error: no entry in precedence table for operator " << CvcParserTokenNames[type]; + throw ParserException(ss.str()); } }/* getOperatorPrecedence() */ @@ -318,16 +320,18 @@ Kind getOperatorKind(int type, bool& negate) { case INTDIV_TOK: return kind::INTS_DIVISION; case MOD_TOK: return kind::INTS_MODULUS; case DIV_TOK: return kind::DIVISION; - case EXP_TOK: Unhandled(CvcParserTokenNames[type]); + case EXP_TOK: break; // bvBinop case CONCAT_TOK: return kind::BITVECTOR_CONCAT; case BAR: return kind::BITVECTOR_OR; case BVAND_TOK: return kind::BITVECTOR_AND; - - default: - Unhandled(CvcParserTokenNames[type]); } + + std::stringstream ss; + ss << "internal error: no entry in operator-kind table for operator " << CvcParserTokenNames[type]; + throw ParserException(ss.str()); + }/* getOperatorKind() */ unsigned findPivot(const std::vector<unsigned>& operators, @@ -355,10 +359,10 @@ Expr createPrecedenceTree(Parser* parser, ExprManager* em, const std::vector<CVC4::Expr>& expressions, const std::vector<unsigned>& operators, unsigned startIndex, unsigned stopIndex) { - Assert(expressions.size() == operators.size() + 1); - Assert(startIndex < expressions.size()); - Assert(stopIndex < expressions.size()); - Assert(startIndex <= stopIndex); + assert(expressions.size() == operators.size() + 1); + assert(startIndex < expressions.size()); + assert(stopIndex < expressions.size()); + assert(startIndex <= stopIndex); if(stopIndex == startIndex) { return expressions[startIndex]; @@ -450,6 +454,7 @@ Expr addNots(ExprManager* em, size_t n, Expr e) { @parser::includes { #include <stdint.h> +#include <cassert> #include "expr/command.h" #include "parser/parser.h" #include "util/subrange_bound.h" @@ -1016,7 +1021,7 @@ type[CVC4::Type& t, /* a type, possibly a function */ : restrictedTypePossiblyFunctionLHS[t,check,lhs] { if(lhs) { - Assert(t.isTuple()); + assert(t.isTuple()); args = TupleType(t).getTypes(); } else { args.push_back(t); @@ -1430,7 +1435,7 @@ arrayStore[CVC4::Expr& f] } : ( LBRACKET formula[f2] { dims.push_back(f2); } RBRACKET )+ ASSIGN_TOK uminusTerm[f3] - { Assert(dims.size() >= 1); + { assert(dims.size() >= 1); // these loops are a bit complicated; they're only used for the // multidimensional ...WITH [a][b] :=... syntax for(unsigned i = 0; i < dims.size() - 1; ++i) { @@ -1630,7 +1635,7 @@ postfixTerm[CVC4::Expr& f] } else if(t.isTester()) { f = MK_EXPR(CVC4::kind::APPLY_TESTER, args); } else { - Unhandled(t); + PARSER_STATE->parseError("internal error: unhandled function application kind"); } } @@ -1864,18 +1869,18 @@ simpleTerm[CVC4::Expr& f] | INTEGER_LITERAL { f = MK_CONST(AntlrInput::tokenToInteger($INTEGER_LITERAL)); } /* bitvector literals */ | HEX_LITERAL - { Assert( AntlrInput::tokenText($HEX_LITERAL).find("0hex") == 0 ); + { assert( AntlrInput::tokenText($HEX_LITERAL).find("0hex") == 0 ); std::string hexString = AntlrInput::tokenTextSubstr($HEX_LITERAL, 4); f = MK_CONST( BitVector(hexString, 16) ); } | BINARY_LITERAL - { Assert( AntlrInput::tokenText($BINARY_LITERAL).find("0bin") == 0 ); + { assert( AntlrInput::tokenText($BINARY_LITERAL).find("0bin") == 0 ); std::string binString = AntlrInput::tokenTextSubstr($BINARY_LITERAL, 4); f = MK_CONST( BitVector(binString, 2) ); } /* record literals */ | PARENHASH recordEntry[name,e] { names.push_back(name); args.push_back(e); } ( COMMA recordEntry[name,e] { names.push_back(name); args.push_back(e); } )* HASHPAREN { std::vector< std::pair<std::string, Type> > typeIds; - Assert(names.size() == args.size()); + assert(names.size() == args.size()); for(unsigned i = 0; i < names.size(); ++i) { typeIds.push_back(std::make_pair(names[i], args[i].getType())); } diff --git a/src/parser/cvc/cvc_input.cpp b/src/parser/cvc/cvc_input.cpp index d91a13bee..26ee4a693 100644 --- a/src/parser/cvc/cvc_input.cpp +++ b/src/parser/cvc/cvc_input.cpp @@ -32,7 +32,7 @@ namespace parser { CvcInput::CvcInput(AntlrInputStream& inputStream) : AntlrInput(inputStream,6) { pANTLR3_INPUT_STREAM input = inputStream.getAntlr3InputStream(); - AlwaysAssert( input != NULL ); + assert( input != NULL ); d_pCvcLexer = CvcLexerNew(input); if( d_pCvcLexer == NULL ) { @@ -42,7 +42,7 @@ CvcInput::CvcInput(AntlrInputStream& inputStream) : setAntlr3Lexer( d_pCvcLexer->pLexer ); pANTLR3_COMMON_TOKEN_STREAM tokenStream = getTokenStream(); - AlwaysAssert( tokenStream != NULL ); + assert( tokenStream != NULL ); d_pCvcParser = CvcParserNew(tokenStream); if( d_pCvcParser == NULL ) { @@ -59,12 +59,12 @@ CvcInput::~CvcInput() { } Command* CvcInput::parseCommand() - throw (ParserException, TypeCheckingException, AssertionException) { + throw (ParserException, TypeCheckingException) { return d_pCvcParser->parseCommand(d_pCvcParser); } Expr CvcInput::parseExpr() - throw (ParserException, TypeCheckingException, AssertionException) { + throw (ParserException, TypeCheckingException) { return d_pCvcParser->parseExpr(d_pCvcParser); } diff --git a/src/parser/cvc/cvc_input.h b/src/parser/cvc/cvc_input.h index 9a1f24fde..94e1bfc60 100644 --- a/src/parser/cvc/cvc_input.h +++ b/src/parser/cvc/cvc_input.h @@ -66,7 +66,7 @@ protected: * @throws ParserException if an error is encountered during parsing. */ Command* parseCommand() - throw(ParserException, TypeCheckingException, AssertionException); + throw(ParserException, TypeCheckingException); /** Parse an expression from the input. Returns a null <code>Expr</code> * if there is no expression there to parse. @@ -74,7 +74,7 @@ protected: * @throws ParserException if an error is encountered during parsing. */ Expr parseExpr() - throw(ParserException, TypeCheckingException, AssertionException); + throw(ParserException, TypeCheckingException); private: diff --git a/src/parser/input.cpp b/src/parser/input.cpp index 76aa47812..12c674a61 100644 --- a/src/parser/input.cpp +++ b/src/parser/input.cpp @@ -24,7 +24,6 @@ #include "expr/type.h" #include "parser/antlr_input.h" #include "util/output.h" -#include "util/Assert.h" using namespace std; using namespace CVC4; @@ -57,7 +56,7 @@ InputStream *Input::getInputStream() { Input* Input::newFileInput(InputLanguage lang, const std::string& filename, bool useMmap) - throw (InputStreamException, AssertionException) { + throw (InputStreamException) { AntlrInputStream *inputStream = AntlrInputStream::newFileInputStream(filename, useMmap); return AntlrInput::newInput(lang, *inputStream); @@ -67,7 +66,7 @@ Input* Input::newStreamInput(InputLanguage lang, std::istream& input, const std::string& name, bool lineBuffered) - throw (InputStreamException, AssertionException) { + throw (InputStreamException) { AntlrInputStream *inputStream = AntlrInputStream::newStreamInputStream(input, name, lineBuffered); return AntlrInput::newInput(lang, *inputStream); @@ -76,7 +75,7 @@ Input* Input::newStreamInput(InputLanguage lang, Input* Input::newStringInput(InputLanguage lang, const std::string& str, const std::string& name) - throw (InputStreamException, AssertionException) { + throw (InputStreamException) { AntlrInputStream *inputStream = AntlrInputStream::newStringInputStream(str, name); return AntlrInput::newInput(lang, *inputStream); } diff --git a/src/parser/input.h b/src/parser/input.h index d47ca4d12..6f30724d1 100644 --- a/src/parser/input.h +++ b/src/parser/input.h @@ -29,7 +29,6 @@ #include "expr/expr.h" #include "expr/expr_manager.h" #include "parser/parser_exception.h" -#include "util/Assert.h" #include "util/language.h" namespace CVC4 { @@ -111,7 +110,7 @@ public: static Input* newFileInput(InputLanguage lang, const std::string& filename, bool useMmap = false) - throw (InputStreamException, AssertionException); + throw (InputStreamException); /** Create an input for the given stream. * @@ -126,7 +125,7 @@ public: std::istream& input, const std::string& name, bool lineBuffered = false) - throw (InputStreamException, AssertionException); + throw (InputStreamException); /** Create an input for the given string * @@ -137,7 +136,7 @@ public: static Input* newStringInput(InputLanguage lang, const std::string& input, const std::string& name) - throw (InputStreamException, AssertionException); + throw (InputStreamException); /** Destructor. Frees the input stream and closes the input. */ @@ -172,7 +171,7 @@ protected: * @throws ParserException if an error is encountered during parsing. */ virtual Command* parseCommand() - throw (ParserException, TypeCheckingException, AssertionException) = 0; + throw (ParserException, TypeCheckingException) = 0; /** * Issue a warning to the user, with source file, line, and column info. @@ -183,7 +182,7 @@ protected: * Throws a <code>ParserException</code> with the given message. */ virtual void parseError(const std::string& msg) - throw (ParserException, AssertionException) = 0; + throw (ParserException) = 0; /** Parse an expression from the input by invoking the * implementation-specific parsing method. Returns a null @@ -192,7 +191,7 @@ protected: * @throws ParserException if an error is encountered during parsing. */ virtual Expr parseExpr() - throw (ParserException, TypeCheckingException, AssertionException) = 0; + throw (ParserException, TypeCheckingException) = 0; /** Set the Parser object for this input. */ virtual void setParser(Parser& parser) = 0; diff --git a/src/parser/memory_mapped_input_buffer.cpp b/src/parser/memory_mapped_input_buffer.cpp index f0b7a9d2c..8f8f07099 100644 --- a/src/parser/memory_mapped_input_buffer.cpp +++ b/src/parser/memory_mapped_input_buffer.cpp @@ -26,7 +26,6 @@ #include <antlr3input.h> #include "parser/memory_mapped_input_buffer.h" -#include "util/Assert.h" #include "util/exception.h" namespace CVC4 { diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp index 2a64d122d..7b58ba4f9 100644 --- a/src/parser/parser.cpp +++ b/src/parser/parser.cpp @@ -20,6 +20,7 @@ #include <fstream> #include <iterator> #include <stdint.h> +#include <cassert> #include "parser/input.h" #include "parser/parser.h" @@ -30,7 +31,6 @@ #include "expr/type.h" #include "util/output.h" #include "options/options.h" -#include "util/Assert.h" using namespace std; using namespace CVC4::kind; @@ -53,16 +53,15 @@ Parser::Parser(ExprManager* exprManager, Input* input, bool strictMode, bool par Expr Parser::getSymbol(const std::string& name, SymbolType type) { checkDeclaration(name, CHECK_DECLARED, type); - Assert( isDeclared(name, type) ); + assert( isDeclared(name, type) ); - switch( type ) { - - case SYM_VARIABLE: // Functions share var namespace + if(type == SYM_VARIABLE) { + // Functions share var namespace return d_symtab->lookup(name); - - default: - Unhandled(type); } + + assert(false);//Unhandled(type); + return Expr(); } @@ -77,14 +76,14 @@ Expr Parser::getFunction(const std::string& name) { Type Parser::getType(const std::string& var_name, SymbolType type) { checkDeclaration(var_name, CHECK_DECLARED, type); - Assert( isDeclared(var_name, type) ); + assert( isDeclared(var_name, type) ); Type t = getSymbol(var_name, type).getType(); return t; } Type Parser::getSort(const std::string& name) { checkDeclaration(name, CHECK_DECLARED, SYM_SORT); - Assert( isDeclared(name, SYM_SORT) ); + assert( isDeclared(name, SYM_SORT) ); Type t = d_symtab->lookupType(name); return t; } @@ -92,14 +91,14 @@ Type Parser::getSort(const std::string& name) { Type Parser::getSort(const std::string& name, const std::vector<Type>& params) { checkDeclaration(name, CHECK_DECLARED, SYM_SORT); - Assert( isDeclared(name, SYM_SORT) ); + assert( isDeclared(name, SYM_SORT) ); Type t = d_symtab->lookupType(name, params); return t; } size_t Parser::getArity(const std::string& sort_name){ checkDeclaration(sort_name, CHECK_DECLARED, SYM_SORT); - Assert( isDeclared(sort_name, SYM_SORT) ); + assert( isDeclared(sort_name, SYM_SORT) ); return d_symtab->lookupArity(sort_name); } @@ -187,20 +186,20 @@ Parser::defineVar(const std::string& name, const Expr& val, bool levelZero) { Debug("parser") << "defineVar( " << name << " := " << val << " , " << levelZero << ")" << std::endl;; d_symtab->bind(name, val, levelZero); - Assert( isDeclared(name) ); + assert( isDeclared(name) ); } void Parser::defineFunction(const std::string& name, const Expr& val, bool levelZero) { d_symtab->bindDefinedFunction(name, val, levelZero); - Assert( isDeclared(name) ); + assert( isDeclared(name) ); } void Parser::defineType(const std::string& name, const Type& type) { d_symtab->bindType(name, type); - Assert( isDeclared(name, SYM_SORT) ); + assert( isDeclared(name, SYM_SORT) ); } void @@ -208,7 +207,7 @@ Parser::defineType(const std::string& name, const std::vector<Type>& params, const Type& type) { d_symtab->bindType(name, params, type); - Assert( isDeclared(name, SYM_SORT) ); + assert( isDeclared(name, SYM_SORT) ); } void @@ -283,7 +282,7 @@ Parser::mkMutualDatatypeTypes(const std::vector<Datatype>& datatypes) { std::vector<DatatypeType> types = d_exprManager->mkMutualDatatypeTypes(datatypes, d_unresolved); - Assert(datatypes.size() == types.size()); + assert(datatypes.size() == types.size()); for(unsigned i = 0; i < datatypes.size(); ++i) { DatatypeType t = types[i]; @@ -379,9 +378,9 @@ bool Parser::isDeclared(const std::string& name, SymbolType type) { return d_symtab->isBound(name); case SYM_SORT: return d_symtab->isBoundType(name); - default: - Unhandled(type); } + assert(false);//Unhandled(type); + return false; } void Parser::checkDeclaration(const std::string& varName, @@ -411,7 +410,7 @@ void Parser::checkDeclaration(const std::string& varName, break; default: - Unhandled(check); + assert(false);//Unhandled(check); } } diff --git a/src/parser/parser.h b/src/parser/parser.h index 7efc4d78c..deeff5a62 100644 --- a/src/parser/parser.h +++ b/src/parser/parser.h @@ -24,6 +24,7 @@ #include <string> #include <set> #include <list> +#include <cassert> #include "parser/input.h" #include "parser/parser_exception.h" diff --git a/src/parser/parser_builder.cpp b/src/parser/parser_builder.cpp index 73c31f578..f48d1e309 100644 --- a/src/parser/parser_builder.cpp +++ b/src/parser/parser_builder.cpp @@ -61,29 +61,27 @@ void ParserBuilder::init(ExprManager* exprManager, } Parser* ParserBuilder::build() - throw (InputStreamException, AssertionException) { + throw (InputStreamException) { Input* input = NULL; switch( d_inputType ) { case FILE_INPUT: input = Input::newFileInput(d_lang, d_filename, d_mmap); break; case LINE_BUFFERED_STREAM_INPUT: - AlwaysAssert( d_streamInput != NULL, - "Uninitialized stream input in ParserBuilder::build()" ); + assert( d_streamInput != NULL ); input = Input::newStreamInput(d_lang, *d_streamInput, d_filename, true); break; case STREAM_INPUT: - AlwaysAssert( d_streamInput != NULL, - "Uninitialized stream input in ParserBuilder::build()" ); + assert( d_streamInput != NULL ); input = Input::newStreamInput(d_lang, *d_streamInput, d_filename); break; case STRING_INPUT: input = Input::newStringInput(d_lang, d_stringInput, d_filename); break; - default: - Unreachable(); } + assert(input != NULL); + Parser* parser = NULL; switch(d_lang) { case language::input::LANG_SMTLIB_V1: diff --git a/src/parser/parser_builder.h b/src/parser/parser_builder.h index 095769ab5..4952f310d 100644 --- a/src/parser/parser_builder.h +++ b/src/parser/parser_builder.h @@ -91,7 +91,7 @@ public: const Options& options); /** Build the parser, using the current settings. */ - Parser *build() throw (InputStreamException, AssertionException); + Parser *build() throw (InputStreamException); /** Should semantic checks be enabled in the parser? (Default: yes) */ ParserBuilder& withChecks(bool flag = true); diff --git a/src/parser/smt1/Smt1.g b/src/parser/smt1/Smt1.g index b228fb9ec..e093037eb 100644 --- a/src/parser/smt1/Smt1.g +++ b/src/parser/smt1/Smt1.g @@ -241,7 +241,7 @@ annotatedFormula[CVC4::Expr& expr] { if((kind == CVC4::kind::AND || kind == CVC4::kind::OR) && args.size() == 1) { /* Unary AND/OR can be replaced with the argument. It just so happens expr should already by the only argument. */ - Assert( expr == args[0] ); + assert( expr == args[0] ); } else if( CVC4::kind::isAssociative(kind) && args.size() > EXPR_MANAGER->maxArity(kind) ) { /* Special treatment for associative operators with lots of children */ @@ -474,7 +474,7 @@ functionDeclaration[CVC4::Command*& smt_command] { sorts.push_back(t); } sortList[sorts] RPAREN_TOK { if( sorts.size() == 1 ) { - Assert( t == sorts[0] ); + assert( t == sorts[0] ); } else { t = EXPR_MANAGER->mkFunctionType(sorts); } @@ -566,8 +566,8 @@ annotation[CVC4::Command*& smt_command] : attribute[key] ( USER_VALUE { std::string value = AntlrInput::tokenText($USER_VALUE); - Assert(*value.begin() == '{'); - Assert(*value.rbegin() == '}'); + assert(*value.begin() == '{'); + assert(*value.rbegin() == '}'); // trim whitespace value.erase(value.begin(), value.begin() + 1); value.erase(value.begin(), std::find_if(value.begin(), value.end(), std::not1(std::ptr_fun<int, int>(std::isspace)))); diff --git a/src/parser/smt1/smt1.cpp b/src/parser/smt1/smt1.cpp index c91743226..9074cc20a 100644 --- a/src/parser/smt1/smt1.cpp +++ b/src/parser/smt1/smt1.cpp @@ -117,9 +117,10 @@ void Smt1::addTheory(Theory theory) { } case THEORY_BITVECTOR_ARRAYS_EX: { - Unimplemented("Cannot yet handle SMT-LIBv1 bitvector arrays (i.e., the BitVector_ArraysEx theory)"); - //addOperator(kind::SELECT); - //addOperator(kind::STORE); + // We don't define the "Array" symbol in this case; + // the parser creates the Array[m:n] types on the fly. + addOperator(kind::SELECT); + addOperator(kind::STORE); break; } @@ -134,7 +135,6 @@ void Smt1::addTheory(Theory theory) { case THEORY_INT_ARRAYS: case THEORY_INT_ARRAYS_EX: { defineType("Array", getExprManager()->mkArrayType(getExprManager()->integerType(), getExprManager()->integerType())); - addOperator(kind::SELECT); addOperator(kind::STORE); break; @@ -167,7 +167,9 @@ void Smt1::addTheory(Theory theory) { break; default: - Unhandled(theory); + std::stringstream ss; + ss << "internal error: unsupported theory " << theory; + throw ParserException(ss.str()); } } @@ -229,8 +231,8 @@ void Smt1::setLogic(const std::string& name) { addTheory(THEORY_BITVECTORS); break; - case QF_ABV: - addTheory(THEORY_ARRAYS_EX); + case QF_ABV:// nonstandard logic + addTheory(THEORY_BITVECTOR_ARRAYS_EX); addTheory(THEORY_BITVECTORS); break; @@ -241,18 +243,18 @@ void Smt1::setLogic(const std::string& name) { case QF_AUFBV: addOperator(kind::APPLY_UF); - addTheory(THEORY_ARRAYS_EX); + addTheory(THEORY_BITVECTOR_ARRAYS_EX); addTheory(THEORY_BITVECTORS); break; - case QF_AUFBVLIA: + case QF_AUFBVLIA:// nonstandard logic addOperator(kind::APPLY_UF); addTheory(THEORY_ARRAYS_EX); addTheory(THEORY_BITVECTORS); addTheory(THEORY_INTS); break; - case QF_AUFBVLRA: + case QF_AUFBVLRA:// nonstandard logic addOperator(kind::APPLY_UF); addTheory(THEORY_ARRAYS_EX); addTheory(THEORY_BITVECTORS); @@ -260,22 +262,22 @@ void Smt1::setLogic(const std::string& name) { break; case QF_AUFLIA: - addTheory(THEORY_INT_ARRAYS_EX); + addTheory(THEORY_INT_ARRAYS_EX);// nonstandard logic addOperator(kind::APPLY_UF); addTheory(THEORY_INTS); break; - case QF_AUFLIRA: + case QF_AUFLIRA:// nonstandard logic addTheory(THEORY_INT_INT_REAL_ARRAY_ARRAYS_EX); addOperator(kind::APPLY_UF); addTheory(THEORY_INTS); addTheory(THEORY_REALS); break; - case ALL_SUPPORTED: + case ALL_SUPPORTED:// nonstandard logic addTheory(THEORY_QUANTIFIERS); /* fall through */ - case QF_ALL_SUPPORTED: + case QF_ALL_SUPPORTED:// nonstandard logic addTheory(THEORY_ARRAYS_EX); addOperator(kind::APPLY_UF); addTheory(THEORY_INTS); diff --git a/src/parser/smt1/smt1_input.cpp b/src/parser/smt1/smt1_input.cpp index 4987cd793..aae990311 100644 --- a/src/parser/smt1/smt1_input.cpp +++ b/src/parser/smt1/smt1_input.cpp @@ -33,7 +33,7 @@ namespace parser { Smt1Input::Smt1Input(AntlrInputStream& inputStream) : AntlrInput(inputStream, 2) { pANTLR3_INPUT_STREAM input = inputStream.getAntlr3InputStream(); - AlwaysAssert( input != NULL ); + assert( input != NULL ); d_pSmt1Lexer = Smt1LexerNew(input); if( d_pSmt1Lexer == NULL ) { @@ -43,7 +43,7 @@ Smt1Input::Smt1Input(AntlrInputStream& inputStream) : setAntlr3Lexer( d_pSmt1Lexer->pLexer ); pANTLR3_COMMON_TOKEN_STREAM tokenStream = getTokenStream(); - AlwaysAssert( tokenStream != NULL ); + assert( tokenStream != NULL ); d_pSmt1Parser = Smt1ParserNew(tokenStream); if( d_pSmt1Parser == NULL ) { @@ -60,12 +60,12 @@ Smt1Input::~Smt1Input() { } Command* Smt1Input::parseCommand() - throw (ParserException, TypeCheckingException, AssertionException) { + throw (ParserException, TypeCheckingException) { return d_pSmt1Parser->parseCommand(d_pSmt1Parser); } Expr Smt1Input::parseExpr() - throw (ParserException, TypeCheckingException, AssertionException) { + throw (ParserException, TypeCheckingException) { return d_pSmt1Parser->parseExpr(d_pSmt1Parser); } diff --git a/src/parser/smt1/smt1_input.h b/src/parser/smt1/smt1_input.h index 77d6f4b50..0f8a962ba 100644 --- a/src/parser/smt1/smt1_input.h +++ b/src/parser/smt1/smt1_input.h @@ -69,7 +69,7 @@ protected: * @throws ParserException if an error is encountered during parsing. */ Command* parseCommand() - throw(ParserException, TypeCheckingException, AssertionException); + throw(ParserException, TypeCheckingException); /** * Parse an expression from the input. Returns a null @@ -78,7 +78,7 @@ protected: * @throws ParserException if an error is encountered during parsing. */ Expr parseExpr() - throw(ParserException, TypeCheckingException, AssertionException); + throw(ParserException, TypeCheckingException); private: diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index fb97d5d1e..1b778f87a 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -587,7 +587,7 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2] args.size() == 1) { /* Unary AND/OR can be replaced with the argument. It just so happens expr should already by the only argument. */ - Assert( expr == args[0] ); + assert( expr == args[0] ); } else if( CVC4::kind::isAssociative(kind) && args.size() > EXPR_MANAGER->maxArity(kind) ) { /* Special treatment for associative operators with lots of children */ @@ -778,12 +778,12 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2] } | HEX_LITERAL - { Assert( AntlrInput::tokenText($HEX_LITERAL).find("#x") == 0 ); + { assert( AntlrInput::tokenText($HEX_LITERAL).find("#x") == 0 ); std::string hexString = AntlrInput::tokenTextSubstr($HEX_LITERAL, 2); expr = MK_CONST( BitVector(hexString, 16) ); } | BINARY_LITERAL - { Assert( AntlrInput::tokenText($BINARY_LITERAL).find("#b") == 0 ); + { assert( AntlrInput::tokenText($BINARY_LITERAL).find("#b") == 0 ); std::string binString = AntlrInput::tokenTextSubstr($BINARY_LITERAL, 2); expr = MK_CONST( BitVector(binString, 2) ); } @@ -1055,7 +1055,9 @@ sortSymbol[CVC4::Type& t, CVC4::parser::DeclarationCheck check] } t = EXPR_MANAGER->mkBitVectorType(numerals.front()); } else { - Unhandled(name); + std::stringstream ss; + ss << "unknown indexed symbol `" << name << "'"; + PARSER_STATE->parseError(ss.str()); } } | LPAREN_TOK symbol[name,CHECK_NONE,SYM_SORT] sortList[args] RPAREN_TOK diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index ca7697810..45caf94a8 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -88,7 +88,9 @@ void Smt2::addTheory(Theory theory) { break; default: - Unhandled(theory); + std::stringstream ss; + ss << "internal error: unsupported theory " << theory; + throw ParserException(ss.str()); } } diff --git a/src/parser/smt2/smt2_input.cpp b/src/parser/smt2/smt2_input.cpp index 8f43b0acf..dd90598bb 100644 --- a/src/parser/smt2/smt2_input.cpp +++ b/src/parser/smt2/smt2_input.cpp @@ -34,7 +34,7 @@ namespace parser { Smt2Input::Smt2Input(AntlrInputStream& inputStream) : AntlrInput(inputStream, 2) { pANTLR3_INPUT_STREAM input = inputStream.getAntlr3InputStream(); - AlwaysAssert( input != NULL ); + assert( input != NULL ); d_pSmt2Lexer = Smt2LexerNew(input); if( d_pSmt2Lexer == NULL ) { @@ -44,7 +44,7 @@ Smt2Input::Smt2Input(AntlrInputStream& inputStream) : setAntlr3Lexer( d_pSmt2Lexer->pLexer ); pANTLR3_COMMON_TOKEN_STREAM tokenStream = getTokenStream(); - AlwaysAssert( tokenStream != NULL ); + assert( tokenStream != NULL ); d_pSmt2Parser = Smt2ParserNew(tokenStream); if( d_pSmt2Parser == NULL ) { @@ -61,12 +61,12 @@ Smt2Input::~Smt2Input() { } Command* Smt2Input::parseCommand() - throw (ParserException, TypeCheckingException, AssertionException) { + throw (ParserException, TypeCheckingException) { return d_pSmt2Parser->parseCommand(d_pSmt2Parser); } Expr Smt2Input::parseExpr() - throw (ParserException, TypeCheckingException, AssertionException) { + throw (ParserException, TypeCheckingException) { return d_pSmt2Parser->parseExpr(d_pSmt2Parser); } diff --git a/src/parser/smt2/smt2_input.h b/src/parser/smt2/smt2_input.h index 05a62c30d..2e36b218e 100644 --- a/src/parser/smt2/smt2_input.h +++ b/src/parser/smt2/smt2_input.h @@ -78,7 +78,7 @@ protected: * @throws ParserException if an error is encountered during parsing. */ Command* parseCommand() - throw(ParserException, TypeCheckingException, AssertionException); + throw(ParserException, TypeCheckingException); /** * Parse an expression from the input. Returns a null @@ -87,7 +87,7 @@ protected: * @throws ParserException if an error is encountered during parsing. */ Expr parseExpr() - throw(ParserException, TypeCheckingException, AssertionException); + throw(ParserException, TypeCheckingException); };/* class Smt2Input */ diff --git a/src/parser/tptp/tptp.cpp b/src/parser/tptp/tptp.cpp index 134498eea..7df2b0210 100644 --- a/src/parser/tptp/tptp.cpp +++ b/src/parser/tptp/tptp.cpp @@ -83,7 +83,9 @@ void Tptp::addTheory(Theory theory) { break; default: - Unhandled(theory); + std::stringstream ss; + ss << "internal error: Tptp::addTheory(): unhandled theory " << theory; + throw ParserException(ss.str()); } } diff --git a/src/parser/tptp/tptp.h b/src/parser/tptp/tptp.h index 9d75a1d37..6d35cac61 100644 --- a/src/parser/tptp/tptp.h +++ b/src/parser/tptp/tptp.h @@ -24,6 +24,7 @@ #include "parser/parser.h" #include "expr/command.h" #include <ext/hash_set> +#include <cassert> namespace CVC4 { @@ -52,9 +53,9 @@ class Tptp : public Parser { public: bool cnf; //in a cnf formula - void addFreeVar(Expr var){Assert(cnf); d_freeVar.push_back(var); }; + void addFreeVar(Expr var){assert(cnf); d_freeVar.push_back(var); }; std::vector< Expr > getFreeVar(){ - Assert(cnf); + assert(cnf); std::vector< Expr > r; r.swap(d_freeVar); return r; @@ -212,22 +213,19 @@ inline Command* Tptp::makeCommand(FormulaRole fr, Expr & expr){ case FR_PLAIN: // it's a usual assert return new AssertCommand(expr); - break; case FR_CONJECTURE: // something to prove return new AssertCommand(getExprManager()->mkExpr(kind::NOT,expr)); - break; case FR_UNKNOWN: case FR_FI_DOMAIN: case FR_FI_FUNCTORS: case FR_FI_PREDICATES: case FR_TYPE: return new EmptyCommand("Untreated role"); - break; - default: - Unreachable("fr",fr); - }; -}; + } + assert(false);// unreachable + return NULL; +} namespace tptp { /** diff --git a/src/parser/tptp/tptp_input.cpp b/src/parser/tptp/tptp_input.cpp index 689f13a8b..8d41a5b68 100644 --- a/src/parser/tptp/tptp_input.cpp +++ b/src/parser/tptp/tptp_input.cpp @@ -34,7 +34,7 @@ namespace parser { TptpInput::TptpInput(AntlrInputStream& inputStream) : AntlrInput(inputStream, 1) { pANTLR3_INPUT_STREAM input = inputStream.getAntlr3InputStream(); - AlwaysAssert( input != NULL ); + assert( input != NULL ); d_pTptpLexer = TptpLexerNew(input); if( d_pTptpLexer == NULL ) { @@ -44,7 +44,7 @@ TptpInput::TptpInput(AntlrInputStream& inputStream) : setAntlr3Lexer( d_pTptpLexer->pLexer ); pANTLR3_COMMON_TOKEN_STREAM tokenStream = getTokenStream(); - AlwaysAssert( tokenStream != NULL ); + assert( tokenStream != NULL ); d_pTptpParser = TptpParserNew(tokenStream); if( d_pTptpParser == NULL ) { @@ -61,12 +61,12 @@ TptpInput::~TptpInput() { } Command* TptpInput::parseCommand() - throw (ParserException, TypeCheckingException, AssertionException) { + throw (ParserException, TypeCheckingException) { return d_pTptpParser->parseCommand(d_pTptpParser); } Expr TptpInput::parseExpr() - throw (ParserException, TypeCheckingException, AssertionException) { + throw (ParserException, TypeCheckingException) { return d_pTptpParser->parseExpr(d_pTptpParser); } diff --git a/src/parser/tptp/tptp_input.h b/src/parser/tptp/tptp_input.h index 7977117d0..32d3efad1 100644 --- a/src/parser/tptp/tptp_input.h +++ b/src/parser/tptp/tptp_input.h @@ -78,7 +78,7 @@ protected: * @throws ParserException if an error is encountered during parsing. */ Command* parseCommand() - throw(ParserException, TypeCheckingException, AssertionException); + throw(ParserException, TypeCheckingException); /** * Parse an expression from the input. Returns a null @@ -87,7 +87,7 @@ protected: * @throws ParserException if an error is encountered during parsing. */ Expr parseExpr() - throw(ParserException, TypeCheckingException, AssertionException); + throw(ParserException, TypeCheckingException); };/* class TptpInput */ diff --git a/src/printer/dagification_visitor.cpp b/src/printer/dagification_visitor.cpp index 98d6a26bb..53b471906 100644 --- a/src/printer/dagification_visitor.cpp +++ b/src/printer/dagification_visitor.cpp @@ -39,7 +39,7 @@ DagificationVisitor::DagificationVisitor(unsigned threshold, std::string letVarP d_substNodes() { // 0 doesn't make sense - CheckArgument(threshold > 0, threshold); + AlwaysAssertArgument(threshold > 0, threshold); } DagificationVisitor::~DagificationVisitor() { diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp index c5345c5a7..9fb825e47 100644 --- a/src/prop/cnf_stream.cpp +++ b/src/prop/cnf_stream.cpp @@ -134,12 +134,12 @@ void TseitinCnfStream::ensureLiteral(TNode n) { return; } - CheckArgument(n.getType().isBoolean(), n, - "CnfStream::ensureLiteral() requires a node of Boolean type.\n" - "got node: %s\n" - "its type: %s\n", - n.toString().c_str(), - n.getType().toString().c_str()); + AlwaysAssertArgument(n.getType().isBoolean(), n, + "CnfStream::ensureLiteral() requires a node of Boolean type.\n" + "got node: %s\n" + "its type: %s\n", + n.toString().c_str(), + n.getType().toString().c_str()); bool negated CVC4_UNUSED = false; SatLiteral lit; diff --git a/src/smt/options b/src/smt/options index 24c8b5e43..f82867b68 100644 --- a/src/smt/options +++ b/src/smt/options @@ -81,4 +81,7 @@ option lemmaInputChannel LemmaInputChannel* :default NULL :include "util/lemma_i option lemmaOutputChannel LemmaOutputChannel* :default NULL :include "util/lemma_output_channel.h" The output channel to receive notfication events for new lemmas +option optionWithOnlyAlternate /--optionWithOnlyAlternate bool + option with only an alternate + endmodule diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 2db746c0a..b968da2e0 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -250,7 +250,7 @@ class SmtEnginePrivate : public NodeManagerListener { * to be in that type. */ void constrainSubtypes(TNode n, std::vector<Node>& assertions) - throw(AssertionException); + throw(); /** * Perform non-clausal simplification of a Node. This involves @@ -259,7 +259,7 @@ class SmtEnginePrivate : public NodeManagerListener { * * Returns false if the formula simplifies to "false" */ - bool simplifyAssertions() throw(TypeCheckingException, AssertionException); + bool simplifyAssertions() throw(TypeCheckingException); public: @@ -344,13 +344,13 @@ public: * even be simplified. */ void addFormula(TNode n) - throw(TypeCheckingException, AssertionException); + throw(TypeCheckingException); /** * Expand definitions in n. */ Node expandDefinitions(TNode n, hash_map<Node, Node, NodeHashFunction>& cache) - throw(TypeCheckingException, AssertionException); + throw(TypeCheckingException); };/* class SmtEnginePrivate */ @@ -358,7 +358,7 @@ public: using namespace CVC4::smt; -SmtEngine::SmtEngine(ExprManager* em) throw(AssertionException) : +SmtEngine::SmtEngine(ExprManager* em) throw() : d_context(em->getContext()), d_userLevels(), d_userContext(new UserContext()), @@ -571,7 +571,7 @@ void SmtEngine::setLogic(const std::string& s) throw(ModalException) { // tempt people in the code to use the (potentially unlocked) // version that's passed in, leading to assert-fails in certain // uses of the CVC4 library. -void SmtEngine::setLogicInternal() throw(AssertionException) { +void SmtEngine::setLogicInternal() throw() { Assert(!d_fullyInited, "setting logic in SmtEngine but the engine has already finished initializing for this run"); d_logic.lock(); @@ -926,7 +926,7 @@ void SmtEngine::defineFunction(Expr func, } Node SmtEnginePrivate::expandDefinitions(TNode n, hash_map<Node, Node, NodeHashFunction>& cache) - throw(TypeCheckingException, AssertionException) { + throw(TypeCheckingException) { if(n.getKind() != kind::APPLY && n.getNumChildren() == 0) { // don't bother putting in the cache @@ -1315,7 +1315,7 @@ void SmtEnginePrivate::unconstrainedSimp() { void SmtEnginePrivate::constrainSubtypes(TNode top, std::vector<Node>& assertions) - throw(AssertionException) { + throw() { Trace("constrainSubtypes") << "constrainSubtypes(): looking at " << top << endl; @@ -1373,7 +1373,7 @@ void SmtEnginePrivate::constrainSubtypes(TNode top, std::vector<Node>& assertion // returns false if simpflication led to "false" bool SmtEnginePrivate::simplifyAssertions() - throw(TypeCheckingException, AssertionException) { + throw(TypeCheckingException) { Assert(d_smt.d_pendingPops == 0); try { @@ -1660,7 +1660,7 @@ void SmtEnginePrivate::processAssertions() { } void SmtEnginePrivate::addFormula(TNode n) - throw(TypeCheckingException, AssertionException) { + throw(TypeCheckingException) { Trace("smt") << "SmtEnginePrivate::addFormula(" << n << ")" << endl; @@ -1865,7 +1865,7 @@ Expr SmtEngine::expandDefinitions(const Expr& e) throw(TypeCheckingException) { } Expr SmtEngine::getValue(const Expr& e) - throw(ModalException, AssertionException) { + throw(ModalException) { Assert(e.getExprManager() == d_exprManager); SmtScope smts(this); @@ -1906,7 +1906,7 @@ Expr SmtEngine::getValue(const Expr& e) return Expr(d_exprManager, new Node(resultNode)); } -bool SmtEngine::addToAssignment(const Expr& e) throw(AssertionException) { +bool SmtEngine::addToAssignment(const Expr& e) throw() { SmtScope smts(this); finalOptionsAreSet(); doPendingPops(); @@ -1935,7 +1935,7 @@ bool SmtEngine::addToAssignment(const Expr& e) throw(AssertionException) { return true; } -CVC4::SExpr SmtEngine::getAssignment() throw(ModalException, AssertionException) { +CVC4::SExpr SmtEngine::getAssignment() throw(ModalException) { Trace("smt") << "SMT getAssignment()" << endl; SmtScope smts(this); finalOptionsAreSet(); @@ -2014,7 +2014,7 @@ void SmtEngine::addToModelCommand(Command* c) { } } -Model* SmtEngine::getModel() throw(ModalException, AssertionException) { +Model* SmtEngine::getModel() throw(ModalException) { Trace("smt") << "SMT getModel()" << endl; SmtScope smts(this); @@ -2040,7 +2040,7 @@ Model* SmtEngine::getModel() throw(ModalException, AssertionException) { return d_theoryEngine->getModel(); } -void SmtEngine::checkModel() throw(InternalErrorException) { +void SmtEngine::checkModel() { // --check-model implies --interactive, which enables the assertion list, // so we should be ok. Assert(d_assertionList != NULL, "don't have an assertion list to check in SmtEngine::checkModel()"); @@ -2157,7 +2157,7 @@ void SmtEngine::checkModel() throw(InternalErrorException) { Notice() << "SmtEngine::checkModel(): all assertions checked out OK !" << endl; } -Proof* SmtEngine::getProof() throw(ModalException, AssertionException) { +Proof* SmtEngine::getProof() throw(ModalException) { Trace("smt") << "SMT getProof()" << endl; SmtScope smts(this); finalOptionsAreSet(); @@ -2185,7 +2185,7 @@ Proof* SmtEngine::getProof() throw(ModalException, AssertionException) { } vector<Expr> SmtEngine::getAssertions() - throw(ModalException, AssertionException) { + throw(ModalException) { SmtScope smts(this); finalOptionsAreSet(); if(Dump.isOn("benchmark")) { diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index 0214cddd3..e906863ad 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -219,7 +219,7 @@ class CVC4_PUBLIC SmtEngine { * Check that a generated Model (via getModel()) actually satisfies * all user assertions. */ - void checkModel() throw(InternalErrorException); + void checkModel(); /** * This is something of an "init" procedure, but is idempotent; call @@ -275,7 +275,7 @@ class CVC4_PUBLIC SmtEngine { * Internally handle the setting of a logic. This function should always * be called when d_logic is updated. */ - void setLogicInternal() throw(AssertionException); + void setLogicInternal() throw(); friend class ::CVC4::smt::SmtEnginePrivate; friend class ::CVC4::smt::SmtScope; @@ -300,7 +300,7 @@ public: /** * Construct an SmtEngine with the given expression manager. */ - SmtEngine(ExprManager* em) throw(AssertionException); + SmtEngine(ExprManager* em) throw(); /** * Destruct the SMT engine. @@ -394,7 +394,7 @@ public: * by a SAT or INVALID query). Only permitted if the SmtEngine is * set to operate interactively and produce-models is on. */ - Expr getValue(const Expr& e) throw(ModalException, AssertionException); + Expr getValue(const Expr& e) throw(ModalException); /** * Add a function to the set of expressions whose value is to be @@ -405,34 +405,34 @@ public: * this function returns true if the expression was added and false * if this request was ignored. */ - bool addToAssignment(const Expr& e) throw(AssertionException); + bool addToAssignment(const Expr& e) throw(); /** * Get the assignment (only if immediately preceded by a SAT or * INVALID query). Only permitted if the SmtEngine is set to * operate interactively and produce-assignments is on. */ - CVC4::SExpr getAssignment() throw(ModalException, AssertionException); + CVC4::SExpr getAssignment() throw(ModalException); /** * Get the model (only if immediately preceded by a SAT * or INVALID query). Only permitted if CVC4 was built with model * support and produce-models is on. */ - Model* getModel() throw(ModalException, AssertionException); + Model* getModel() throw(ModalException); /** * Get the last proof (only if immediately preceded by an UNSAT * or VALID query). Only permitted if CVC4 was built with proof * support and produce-proofs is on. */ - Proof* getProof() throw(ModalException, AssertionException); + Proof* getProof() throw(ModalException); /** * Get the current set of assertions. Only permitted if the * SmtEngine is set to operate interactively. */ - std::vector<Expr> getAssertions() throw(ModalException, AssertionException); + std::vector<Expr> getAssertions() throw(ModalException); /** * Push a user-level context. diff --git a/src/theory/logic_info.cpp b/src/theory/logic_info.cpp index 9660986cf..c4ae81927 100644 --- a/src/theory/logic_info.cpp +++ b/src/theory/logic_info.cpp @@ -76,7 +76,7 @@ LogicInfo::LogicInfo(const char* logicString) throw(IllegalArgumentException) : } std::string LogicInfo::getLogicString() const { - Assert(d_locked, "This LogicInfo isn't locked yet, and cannot be queried"); + CheckArgument(d_locked, *this, "This LogicInfo isn't locked yet, and cannot be queried"); if(d_logicString == "") { size_t seen = 0; // make sure we support all the active theories @@ -129,7 +129,7 @@ std::string LogicInfo::getLogicString() const { } void LogicInfo::setLogicString(std::string logicString) throw(IllegalArgumentException) { - Assert(!d_locked, "This LogicInfo is locked, and cannot be modified"); + CheckArgument(!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 } @@ -244,17 +244,17 @@ void LogicInfo::setLogicString(std::string logicString) throw(IllegalArgumentExc } void LogicInfo::enableEverything() { - Assert(!d_locked, "This LogicInfo is locked, and cannot be modified"); + CheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified"); *this = LogicInfo(); } void LogicInfo::disableEverything() { - Assert(!d_locked, "This LogicInfo is locked, and cannot be modified"); + CheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified"); *this = LogicInfo(""); } void LogicInfo::enableTheory(theory::TheoryId theory) { - Assert(!d_locked, "This LogicInfo is locked, and cannot be modified"); + CheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified"); if(!d_theories[theory]) { if(isTrueTheory(theory)) { ++d_sharingTheories; @@ -265,7 +265,7 @@ void LogicInfo::enableTheory(theory::TheoryId theory) { } void LogicInfo::disableTheory(theory::TheoryId theory) { - Assert(!d_locked, "This LogicInfo is locked, and cannot be modified"); + CheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified"); if(d_theories[theory]) { if(isTrueTheory(theory)) { Assert(d_sharingTheories > 0); @@ -281,14 +281,14 @@ void LogicInfo::disableTheory(theory::TheoryId theory) { } void LogicInfo::enableIntegers() { - Assert(!d_locked, "This LogicInfo is locked, and cannot be modified"); + CheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified"); d_logicString = ""; enableTheory(THEORY_ARITH); d_integers = true; } void LogicInfo::disableIntegers() { - Assert(!d_locked, "This LogicInfo is locked, and cannot be modified"); + CheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified"); d_logicString = ""; d_integers = false; if(!d_reals) { @@ -297,14 +297,14 @@ void LogicInfo::disableIntegers() { } void LogicInfo::enableReals() { - Assert(!d_locked, "This LogicInfo is locked, and cannot be modified"); + CheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified"); d_logicString = ""; enableTheory(THEORY_ARITH); d_reals = true; } void LogicInfo::disableReals() { - Assert(!d_locked, "This LogicInfo is locked, and cannot be modified"); + CheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified"); d_logicString = ""; d_reals = false; if(!d_integers) { @@ -313,21 +313,21 @@ void LogicInfo::disableReals() { } void LogicInfo::arithOnlyDifference() { - Assert(!d_locked, "This LogicInfo is locked, and cannot be modified"); + CheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified"); d_logicString = ""; d_linear = true; d_differenceLogic = true; } void LogicInfo::arithOnlyLinear() { - Assert(!d_locked, "This LogicInfo is locked, and cannot be modified"); + CheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified"); d_logicString = ""; d_linear = true; d_differenceLogic = false; } void LogicInfo::arithNonLinear() { - Assert(!d_locked, "This LogicInfo is locked, and cannot be modified"); + CheckArgument(!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 36b71e931..8cd326039 100644 --- a/src/theory/logic_info.h +++ b/src/theory/logic_info.h @@ -105,25 +105,25 @@ public: /** Is sharing enabled for this logic? */ bool isSharingEnabled() const { - Assert(d_locked, "This LogicInfo isn't locked yet, and cannot be queried"); + CheckArgument(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 isTheoryEnabled(theory::TheoryId theory) const { - Assert(d_locked, "This LogicInfo isn't locked yet, and cannot be queried"); + CheckArgument(d_locked, *this, "This LogicInfo isn't locked yet, and cannot be queried"); return d_theories[theory]; } /** Is this a quantified logic? */ bool isQuantified() const { - Assert(d_locked, "This LogicInfo isn't locked yet, and cannot be queried"); + CheckArgument(d_locked, *this, "This LogicInfo isn't locked yet, and cannot be queried"); return isTheoryEnabled(theory::THEORY_QUANTIFIERS) || isTheoryEnabled(theory::THEORY_REWRITERULES); } /** Is this the all-inclusive logic? */ bool hasEverything() const { - Assert(d_locked, "This LogicInfo isn't locked yet, and cannot be queried"); + CheckArgument(d_locked, *this, "This LogicInfo isn't locked yet, and cannot be queried"); LogicInfo everything; everything.lock(); return *this == everything; @@ -131,7 +131,7 @@ public: /** Is this the all-exclusive logic? (Here, that means propositional logic) */ bool hasNothing() const { - Assert(d_locked, "This LogicInfo isn't locked yet, and cannot be queried"); + CheckArgument(d_locked, *this, "This LogicInfo isn't locked yet, and cannot be queried"); LogicInfo nothing(""); nothing.lock(); return *this == nothing; @@ -143,7 +143,7 @@ public: * use "isPure(theory) && !isQuantified()". */ bool isPure(theory::TheoryId theory) const { - Assert(d_locked, "This LogicInfo isn't locked yet, and cannot be queried"); + 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() && @@ -155,22 +155,22 @@ public: /** Are integers in this logic? */ bool areIntegersUsed() const { - Assert(d_locked, "This LogicInfo isn't locked yet, and cannot be queried"); + CheckArgument(d_locked, *this, "This LogicInfo isn't locked yet, and cannot be queried"); return d_integers; } /** Are reals in this logic? */ bool areRealsUsed() const { - Assert(d_locked, "This LogicInfo isn't locked yet, and cannot be queried"); + CheckArgument(d_locked, *this, "This LogicInfo isn't locked yet, and cannot be queried"); return d_reals; } /** Does this logic only linear arithmetic? */ bool isLinear() const { - Assert(d_locked, "This LogicInfo isn't locked yet, and cannot be queried"); + CheckArgument(d_locked, *this, "This LogicInfo isn't locked yet, and cannot be queried"); return d_linear || d_differenceLogic; } /** Does this logic only permit difference reasoning? (implies linear) */ bool isDifferenceLogic() const { - Assert(d_locked, "This LogicInfo isn't locked yet, and cannot be queried"); + CheckArgument(d_locked, *this, "This LogicInfo isn't locked yet, and cannot be queried"); return d_differenceLogic; } @@ -252,13 +252,13 @@ public: /** Are these two LogicInfos equal? */ bool operator==(const LogicInfo& other) const { - Assert(isLocked() && other.isLocked(), "This LogicInfo isn't locked yet, and cannot be queried"); + 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; } } - Assert(d_sharingTheories == other.d_sharingTheories, "LogicInfo internal inconsistency"); + CheckArgument(d_sharingTheories == other.d_sharingTheories, *this, "LogicInfo internal inconsistency"); if(isTheoryEnabled(theory::THEORY_ARITH)) { return d_integers == other.d_integers && @@ -283,13 +283,13 @@ public: } /** Is this LogicInfo "less than or equal" the other? */ bool operator<=(const LogicInfo& other) const { - Assert(isLocked() && other.isLocked(), "This LogicInfo isn't locked yet, and cannot be queried"); + 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; } } - Assert(d_sharingTheories <= other.d_sharingTheories, "LogicInfo internal inconsistency"); + 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) && @@ -302,13 +302,13 @@ public: } /** Is this LogicInfo "greater than or equal" the other? */ bool operator>=(const LogicInfo& other) const { - Assert(isLocked() && other.isLocked(), "This LogicInfo isn't locked yet, and cannot be queried"); + 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; } } - Assert(d_sharingTheories >= other.d_sharingTheories, "LogicInfo internal inconsistency"); + 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) && diff --git a/src/util/Assert.cpp b/src/util/Assert.cpp index 11745ad26..e299bef1d 100644 --- a/src/util/Assert.cpp +++ b/src/util/Assert.cpp @@ -27,7 +27,7 @@ using namespace std; namespace CVC4 { #ifdef CVC4_DEBUG -CVC4_THREADLOCAL_PUBLIC(const char*) s_debugLastException = NULL; +CVC4_THREADLOCAL(const char*) s_debugLastException = NULL; #endif /* CVC4_DEBUG */ void AssertionException::construct(const char* header, const char* extra, diff --git a/src/util/Assert.h b/src/util/Assert.h index 3334de4a0..4a6fe4d3a 100644 --- a/src/util/Assert.h +++ b/src/util/Assert.h @@ -16,7 +16,7 @@ ** Assertion utility classes, functions, exceptions, and macros. **/ -#include "cvc4_public.h" +#include "cvc4_private.h" #ifndef __CVC4__ASSERT_H #define __CVC4__ASSERT_H @@ -36,7 +36,7 @@ namespace CVC4 { -class CVC4_PUBLIC AssertionException : public Exception { +class AssertionException : public Exception { protected: void construct(const char* header, const char* extra, const char* function, const char* file, @@ -75,7 +75,7 @@ public: } };/* class AssertionException */ -class CVC4_PUBLIC UnreachableCodeException : public AssertionException { +class UnreachableCodeException : public AssertionException { protected: UnreachableCodeException() : AssertionException() {} @@ -97,7 +97,7 @@ public: } };/* class UnreachableCodeException */ -class CVC4_PUBLIC UnhandledCaseException : public UnreachableCodeException { +class UnhandledCaseException : public UnreachableCodeException { protected: UnhandledCaseException() : UnreachableCodeException() {} @@ -129,7 +129,7 @@ public: } };/* class UnhandledCaseException */ -class CVC4_PUBLIC UnimplementedOperationException : public AssertionException { +class UnimplementedOperationException : public AssertionException { protected: UnimplementedOperationException() : AssertionException() {} @@ -151,14 +151,14 @@ public: } };/* class UnimplementedOperationException */ -class CVC4_PUBLIC IllegalArgumentException : public AssertionException { +class AssertArgumentException : public AssertionException { protected: - IllegalArgumentException() : AssertionException() {} + AssertArgumentException() : AssertionException() {} public: - IllegalArgumentException(const char* argDesc, const char* function, - const char* file, unsigned line, - const char* fmt, ...) : + AssertArgumentException(const char* argDesc, const char* function, + const char* file, unsigned line, + const char* fmt, ...) : AssertionException() { va_list args; va_start(args, fmt); @@ -168,17 +168,17 @@ public: va_end(args); } - IllegalArgumentException(const char* argDesc, const char* function, - const char* file, unsigned line) : + AssertArgumentException(const char* argDesc, const char* function, + const char* file, unsigned line) : AssertionException() { construct("Illegal argument detected", ( std::string("`") + argDesc + "' is a bad argument" ).c_str(), function, file, line); } - IllegalArgumentException(const char* condStr, const char* argDesc, - const char* function, const char* file, - unsigned line, const char* fmt, ...) : + AssertArgumentException(const char* condStr, const char* argDesc, + const char* function, const char* file, + unsigned line, const char* fmt, ...) : AssertionException() { va_list args; va_start(args, fmt); @@ -189,18 +189,18 @@ public: va_end(args); } - IllegalArgumentException(const char* condStr, const char* argDesc, - const char* function, const char* file, - unsigned line) : + AssertArgumentException(const char* condStr, const char* argDesc, + const char* function, const char* file, + unsigned line) : AssertionException() { construct("Illegal argument detected", ( std::string("`") + argDesc + "' is a bad argument; expected " + condStr + " to hold" ).c_str(), function, file, line); } -};/* class IllegalArgumentException */ +};/* class AssertArgumentException */ -class CVC4_PUBLIC InternalErrorException : public AssertionException { +class InternalErrorException : public AssertionException { protected: InternalErrorException() : AssertionException() {} @@ -235,7 +235,7 @@ public: #ifdef CVC4_DEBUG -extern CVC4_THREADLOCAL_PUBLIC(const char*) s_debugLastException; +extern CVC4_THREADLOCAL(const char*) s_debugLastException; /** * Special assertion failure handling in debug mode; in non-debug @@ -247,8 +247,7 @@ extern CVC4_THREADLOCAL_PUBLIC(const char*) s_debugLastException; * debug builds only; in debug builds, it handles all assertion * failures (even those that exist in non-debug builds). */ -void debugAssertionFailed(const AssertionException& thisException, - const char* lastException) CVC4_PUBLIC; +void debugAssertionFailed(const AssertionException& thisException, const char* lastException); // If we're currently handling an exception, print a warning instead; // otherwise std::terminate() is called by the runtime and we lose @@ -283,22 +282,28 @@ void debugAssertionFailed(const AssertionException& thisException, #define InternalError(msg...) \ throw ::CVC4::InternalErrorException(__PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg) #define IllegalArgument(arg, msg...) \ - throw ::CVC4::IllegalArgumentException(#arg, __PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg) + throw ::CVC4::IllegalArgumentException("", #arg, __PRETTY_FUNCTION__, ## msg) #define CheckArgument(cond, arg, msg...) \ - AlwaysAssertArgument(cond, arg, ## msg) + do { \ + if(EXPECT_FALSE( ! (cond) )) { \ + throw ::CVC4::IllegalArgumentException(#cond, #arg, __PRETTY_FUNCTION__, ## msg); \ + } \ + } while(0) #define AlwaysAssertArgument(cond, arg, msg...) \ do { \ if(EXPECT_FALSE( ! (cond) )) { \ - throw ::CVC4::IllegalArgumentException(#cond, #arg, __PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg); \ + throw ::CVC4::AssertArgumentException(#cond, #arg, __PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg); \ } \ } while(0) #ifdef CVC4_ASSERTIONS # define Assert(cond, msg...) AlwaysAssert(cond, ## msg) # define AssertArgument(cond, arg, msg...) AlwaysAssertArgument(cond, arg, ## msg) +# define DebugCheckArgument(cond, arg, msg...) CheckArgument(cond, arg, ## msg) #else /* ! CVC4_ASSERTIONS */ # define Assert(cond, msg...) /*EXPECT_TRUE( cond )*/ # define AssertArgument(cond, arg, msg...) /*EXPECT_TRUE( cond )*/ +# define DebugCheckArgument(cond, arg, msg...) /*EXPECT_TRUE( cond )*/ #endif /* CVC4_ASSERTIONS */ }/* CVC4 namespace */ diff --git a/src/util/Makefile.am b/src/util/Makefile.am index 7d9a055fd..fcbadf490 100644 --- a/src/util/Makefile.am +++ b/src/util/Makefile.am @@ -27,6 +27,7 @@ libutil_la_SOURCES = \ Makefile.in \ debug.h \ exception.h \ + exception.cpp \ hash.h \ bool.h \ proof.h \ diff --git a/src/util/ascription_type.h b/src/util/ascription_type.h index 579746332..4421d6ca7 100644 --- a/src/util/ascription_type.h +++ b/src/util/ascription_type.h @@ -46,7 +46,7 @@ public: };/* class AscriptionType */ /** - * A hash strategy for type ascription operators. + * A hash function for type ascription operators. */ struct CVC4_PUBLIC AscriptionTypeHashFunction { inline size_t operator()(const AscriptionType& at) const { diff --git a/src/util/bitvector.h b/src/util/bitvector.h index 185bb55d9..a3d4f1b60 100644 --- a/src/util/bitvector.h +++ b/src/util/bitvector.h @@ -23,7 +23,7 @@ #define __CVC4__BITVECTOR_H #include <iostream> -#include "util/Assert.h" +#include "util/exception.h" #include "util/integer.h" namespace CVC4 { @@ -99,8 +99,8 @@ public: return d_value != y.d_value; } - BitVector equals(const BitVector& y) const { - Assert(d_size == y.d_size); + BitVector equals(const BitVector& y) const { + CheckArgument(d_size == y.d_size, y); return d_value == y.d_value; } @@ -118,19 +118,19 @@ public: // xor BitVector operator ^(const BitVector& y) const { - Assert (d_size == y.d_size); + CheckArgument(d_size == y.d_size, y); return BitVector(d_size, d_value.bitwiseXor(y.d_value)); } // or BitVector operator |(const BitVector& y) const { - Assert (d_size == y.d_size); + CheckArgument(d_size == y.d_size, y); return BitVector(d_size, d_value.bitwiseOr(y.d_value)); } // and BitVector operator &(const BitVector& y) const { - Assert (d_size == y.d_size); + CheckArgument(d_size == y.d_size, y); return BitVector(d_size, d_value.bitwiseAnd(y.d_value)); } @@ -162,13 +162,13 @@ public: BitVector operator +(const BitVector& y) const { - Assert (d_size == y.d_size); + CheckArgument(d_size == y.d_size, y); Integer sum = d_value + y.d_value; return BitVector(d_size, sum); } BitVector operator -(const BitVector& y) const { - Assert (d_size == y.d_size); + CheckArgument(d_size == y.d_size, y); // to maintain the invariant that we are only adding BitVectors of the // same size BitVector one(d_size, Integer(1)); @@ -181,35 +181,38 @@ public: } BitVector operator *(const BitVector& y) const { - Assert (d_size == y.d_size); + CheckArgument(d_size == y.d_size, y); Integer prod = d_value * y.d_value; return BitVector(d_size, prod); } BitVector unsignedDiv (const BitVector& y) const { - Assert (d_size == y.d_size); + CheckArgument(d_size == y.d_size, y); // TODO: decide whether we really want these semantics if (y.d_value == 0) { return BitVector(d_size, Integer(0)); } - Assert (d_value >= 0 && y.d_value > 0); + CheckArgument(d_value >= 0, this); + CheckArgument(y.d_value > 0, y); return BitVector(d_size, d_value.floorDivideQuotient(y.d_value)); } BitVector unsignedRem(const BitVector& y) const { - Assert (d_size == y.d_size); + CheckArgument(d_size == y.d_size, y); // TODO: decide whether we really want these semantics if (y.d_value == 0) { return BitVector(d_size, Integer(0)); } - Assert (d_value >= 0 && y.d_value > 0); + CheckArgument(d_value >= 0, this); + CheckArgument(y.d_value > 0, y); return BitVector(d_size, d_value.floorDivideRemainder(y.d_value)); } bool signedLessThan(const BitVector& y) const { - Assert(d_size == y.d_size); - Assert(d_value >= 0 && y.d_value >= 0); + CheckArgument(d_size == y.d_size, y); + CheckArgument(d_value >= 0, this); + CheckArgument(y.d_value >= 0, y); Integer a = (*this).toSignedInt(); Integer b = y.toSignedInt(); @@ -217,14 +220,16 @@ public: } bool unsignedLessThan(const BitVector& y) const { - Assert(d_size == y.d_size); - Assert(d_value >= 0 && y.d_value >= 0); + CheckArgument(d_size == y.d_size, y); + CheckArgument(d_value >= 0, this); + CheckArgument(y.d_value >= 0, y); return d_value < y.d_value; } bool signedLessThanEq(const BitVector& y) const { - Assert(d_size == y.d_size); - Assert(d_value >= 0 && y.d_value >= 0); + CheckArgument(d_size == y.d_size, y); + CheckArgument(d_value >= 0, this); + CheckArgument(y.d_value >= 0, y); Integer a = (*this).toSignedInt(); Integer b = y.toSignedInt(); @@ -232,8 +237,9 @@ public: } bool unsignedLessThanEq(const BitVector& y) const { - Assert(d_size == y.d_size); - Assert(d_value >= 0 && y.d_value >= 0); + CheckArgument(d_size == y.d_size, this); + CheckArgument(d_value >= 0, this); + CheckArgument(y.d_value >= 0, y); return d_value <= y.d_value; } @@ -269,7 +275,7 @@ public: } // making sure we don't lose information casting - Assert(y.d_value < Integer(1).multiplyByPow2(32)); + CheckArgument(y.d_value < Integer(1).multiplyByPow2(32), y); uint32_t amount = y.d_value.toUnsignedInt(); Integer res = d_value.multiplyByPow2(amount); return BitVector(d_size, res); @@ -281,7 +287,7 @@ public: } // making sure we don't lose information casting - Assert(y.d_value < Integer(1).multiplyByPow2(32)); + CheckArgument(y.d_value < Integer(1).multiplyByPow2(32), y); uint32_t amount = y.d_value.toUnsignedInt(); Integer res = d_value.divByPow2(amount); return BitVector(d_size, res); @@ -302,7 +308,7 @@ public: } // making sure we don't lose information casting - Assert(y.d_value < Integer(1).multiplyByPow2(32)); + CheckArgument(y.d_value < Integer(1).multiplyByPow2(32), y); uint32_t amount = y.d_value.toUnsignedInt(); Integer rest = d_value.divByPow2(amount); @@ -310,7 +316,7 @@ public: if(sign_bit == Integer(0)) { return BitVector(d_size, rest); } - Integer res = rest.oneExtend(d_size - amount, amount); + Integer res = rest.oneExtend(d_size - amount, amount); return BitVector(d_size, res); } @@ -358,17 +364,15 @@ public: inline BitVector::BitVector(const std::string& num, unsigned base) { - AlwaysAssert( base == 2 || base == 16 ); + CheckArgument(base == 2 || base == 16, base); if( base == 2 ) { d_size = num.size(); - } else if( base == 16 ) { - d_size = num.size() * 4; } else { - Unreachable("Unsupported base in BitVector(std::string&, unsigned int)."); + d_size = num.size() * 4; } - d_value = Integer(num,base); + d_value = Integer(num, base); }/* BitVector::BitVector() */ diff --git a/src/util/cardinality.h b/src/util/cardinality.h index 81a291006..17368c157 100644 --- a/src/util/cardinality.h +++ b/src/util/cardinality.h @@ -26,7 +26,7 @@ #include <utility> #include "util/integer.h" -#include "util/Assert.h" +#include "util/exception.h" namespace CVC4 { @@ -118,7 +118,6 @@ public: CheckArgument(card >= 0, card, "Cardinality must be a nonnegative integer, not %ld.", card); d_card += 1; - Assert(isFinite()); } /** @@ -130,14 +129,12 @@ public: "Cardinality must be a nonnegative integer, not %s.", card.toString().c_str()); d_card += 1; - Assert(isFinite()); } /** * Construct an infinite cardinality equal to the given Beth number. */ Cardinality(CardinalityBeth beth) : d_card(-beth.getNumber() - 1) { - Assert(!isFinite()); } /** diff --git a/src/util/datatype.cpp b/src/util/datatype.cpp index ec8c8e166..ee9c4e406 100644 --- a/src/util/datatype.cpp +++ b/src/util/datatype.cpp @@ -28,6 +28,7 @@ #include "expr/node.h" #include "util/recursion_breaker.h" #include "util/matcher.h" +#include "util/Assert.h" using namespace std; @@ -67,11 +68,11 @@ const Datatype& Datatype::datatypeOf(Expr item) { size_t Datatype::indexOf(Expr item) { ExprManagerScope ems(item); - AssertArgument(item.getType().isConstructor() || - item.getType().isTester() || - item.getType().isSelector(), - item, - "arg must be a datatype constructor, selector, or tester"); + CheckArgument(item.getType().isConstructor() || + item.getType().isTester() || + item.getType().isSelector(), + item, + "arg must be a datatype constructor, selector, or tester"); TNode n = Node::fromExpr(item); if( item.getKind()==kind::APPLY_TYPE_ASCRIPTION ){ return indexOf( item[0] ); @@ -87,29 +88,27 @@ void Datatype::resolve(ExprManager* em, const std::vector<Type>& replacements, const std::vector< SortConstructorType >& paramTypes, const std::vector< DatatypeType >& paramReplacements) - throw(AssertionException, DatatypeResolutionException) { + throw(IllegalArgumentException, DatatypeResolutionException) { - AssertArgument(em != NULL, "cannot resolve a Datatype with a NULL expression manager"); - CheckArgument(!d_resolved, "cannot resolve a Datatype twice"); - AssertArgument(resolutions.find(d_name) != resolutions.end(), + CheckArgument(em != NULL, em, "cannot resolve a Datatype with a NULL expression manager"); + CheckArgument(!d_resolved, this, "cannot resolve a Datatype twice"); + CheckArgument(resolutions.find(d_name) != resolutions.end(), resolutions, "Datatype::resolve(): resolutions doesn't contain me!"); - AssertArgument(placeholders.size() == replacements.size(), placeholders, + CheckArgument(placeholders.size() == replacements.size(), placeholders, "placeholders and replacements must be the same size"); - AssertArgument(paramTypes.size() == paramReplacements.size(), paramTypes, + CheckArgument(paramTypes.size() == paramReplacements.size(), paramTypes, "paramTypes and paramReplacements must be the same size"); CheckArgument(getNumConstructors() > 0, *this, "cannot resolve a Datatype that has no constructors"); DatatypeType self = (*resolutions.find(d_name)).second; - AssertArgument(&self.getDatatype() == this, "Datatype::resolve(): resolutions doesn't contain me!"); + CheckArgument(&self.getDatatype() == this, resolutions, "Datatype::resolve(): resolutions doesn't contain me!"); d_resolved = true; size_t index = 0; for(iterator i = begin(), i_end = end(); i != i_end; ++i) { (*i).resolve(em, self, resolutions, placeholders, replacements, paramTypes, paramReplacements); - Assert((*i).isResolved()); Node::fromExpr((*i).d_constructor).setAttribute(DatatypeIndexAttr(), index); Node::fromExpr((*i).d_tester).setAttribute(DatatypeIndexAttr(), index++); } d_self = self; - Assert(index == getNumConstructors()); } void Datatype::addConstructor(const DatatypeConstructor& c) { @@ -118,7 +117,7 @@ void Datatype::addConstructor(const DatatypeConstructor& c) { d_constructors.push_back(c); } -Cardinality Datatype::getCardinality() const throw(AssertionException) { +Cardinality Datatype::getCardinality() const throw(IllegalArgumentException) { CheckArgument(isResolved(), this, "this datatype is not yet resolved"); RecursionBreaker<const Datatype*, DatatypeHashFunction> breaker(__PRETTY_FUNCTION__, this); if(breaker.isRecursion()) { @@ -131,7 +130,7 @@ Cardinality Datatype::getCardinality() const throw(AssertionException) { return c; } -bool Datatype::isFinite() const throw(AssertionException) { +bool Datatype::isFinite() const throw(IllegalArgumentException) { CheckArgument(isResolved(), this, "this datatype is not yet resolved"); // we're using some internals, so we have to set up this library context @@ -157,7 +156,7 @@ bool Datatype::isFinite() const throw(AssertionException) { return true; } -bool Datatype::isWellFounded() const throw(AssertionException) { +bool Datatype::isWellFounded() const throw(IllegalArgumentException) { CheckArgument(isResolved(), this, "this datatype is not yet resolved"); // we're using some internals, so we have to set up this library context @@ -191,7 +190,7 @@ bool Datatype::isWellFounded() const throw(AssertionException) { return false; } -Expr Datatype::mkGroundTerm( Type t ) const throw(AssertionException) { +Expr Datatype::mkGroundTerm( Type t ) const throw(IllegalArgumentException) { CheckArgument(isResolved(), this, "this datatype is not yet resolved"); // we're using some internals, so we have to set up this library context @@ -274,16 +273,16 @@ Expr Datatype::mkGroundTerm( Type t ) const throw(AssertionException) { } } -DatatypeType Datatype::getDatatypeType() const throw(AssertionException) { +DatatypeType Datatype::getDatatypeType() const throw(IllegalArgumentException) { CheckArgument(isResolved(), *this, "Datatype must be resolved to get its DatatypeType"); - Assert(!d_self.isNull() && !DatatypeType(d_self).isParametric()); + CheckArgument(!d_self.isNull() && !DatatypeType(d_self).isParametric(), this); return DatatypeType(d_self); } DatatypeType Datatype::getDatatypeType(const std::vector<Type>& params) - const throw(AssertionException) { + const throw(IllegalArgumentException) { CheckArgument(isResolved(), *this, "Datatype must be resolved to get its DatatypeType"); - Assert(!d_self.isNull() && DatatypeType(d_self).isParametric()); + CheckArgument(!d_self.isNull() && DatatypeType(d_self).isParametric(), this); return DatatypeType(d_self).instantiate(params); } @@ -394,9 +393,9 @@ void DatatypeConstructor::resolve(ExprManager* em, DatatypeType self, const std::vector<Type>& replacements, const std::vector< SortConstructorType >& paramTypes, const std::vector< DatatypeType >& paramReplacements) - throw(AssertionException, DatatypeResolutionException) { + throw(IllegalArgumentException, DatatypeResolutionException) { - AssertArgument(em != NULL, "cannot resolve a Datatype with a NULL expression manager"); + CheckArgument(em != NULL, em, "cannot resolve a Datatype with a NULL expression manager"); CheckArgument(!isResolved(), "cannot resolve a Datatype constructor twice; " "perhaps the same constructor was added twice, " @@ -577,7 +576,7 @@ Expr DatatypeConstructor::getTester() const { return d_tester; } -Cardinality DatatypeConstructor::getCardinality() const throw(AssertionException) { +Cardinality DatatypeConstructor::getCardinality() const throw(IllegalArgumentException) { CheckArgument(isResolved(), this, "this datatype constructor is not yet resolved"); Cardinality c = 1; @@ -589,7 +588,7 @@ Cardinality DatatypeConstructor::getCardinality() const throw(AssertionException return c; } -bool DatatypeConstructor::isFinite() const throw(AssertionException) { +bool DatatypeConstructor::isFinite() const throw(IllegalArgumentException) { CheckArgument(isResolved(), this, "this datatype constructor is not yet resolved"); // we're using some internals, so we have to set up this library context @@ -615,7 +614,7 @@ bool DatatypeConstructor::isFinite() const throw(AssertionException) { return true; } -bool DatatypeConstructor::isWellFounded() const throw(AssertionException) { +bool DatatypeConstructor::isWellFounded() const throw(IllegalArgumentException) { CheckArgument(isResolved(), this, "this datatype constructor is not yet resolved"); // we're using some internals, so we have to set up this library context @@ -659,7 +658,7 @@ bool DatatypeConstructor::isWellFounded() const throw(AssertionException) { return true; } -Expr DatatypeConstructor::mkGroundTerm( Type t ) const throw(AssertionException) { +Expr DatatypeConstructor::mkGroundTerm( Type t ) const throw(IllegalArgumentException) { CheckArgument(isResolved(), this, "this datatype constructor is not yet resolved"); // we're using some internals, so we have to set up this library context @@ -684,7 +683,7 @@ Expr DatatypeConstructor::mkGroundTerm( Type t ) const throw(AssertionException) groundTerms.push_back(getConstructor()); // for each selector, get a ground term - Assert( t.isDatatype() ); + CheckArgument( t.isDatatype(), t ); std::vector< Type > instTypes; std::vector< Type > paramTypes; if( DatatypeType(t).isParametric() ){ diff --git a/src/util/datatype.h b/src/util/datatype.h index 9853ba417..86bd1cfe3 100644 --- a/src/util/datatype.h +++ b/src/util/datatype.h @@ -35,7 +35,6 @@ namespace CVC4 { #include "expr/expr.h" #include "expr/type.h" -#include "util/Assert.h" #include "util/output.h" #include "util/hash.h" #include "util/exception.h" @@ -155,7 +154,7 @@ private: const std::vector<Type>& replacements, const std::vector< SortConstructorType >& paramTypes, const std::vector< DatatypeType >& paramReplacements) - throw(AssertionException, DatatypeResolutionException); + throw(IllegalArgumentException, DatatypeResolutionException); friend class Datatype; /** Helper function for resolving parametric datatypes. @@ -260,28 +259,28 @@ public: * Return the cardinality of this constructor (the product of the * cardinalities of its arguments). */ - Cardinality getCardinality() const throw(AssertionException); + Cardinality getCardinality() const throw(IllegalArgumentException); /** * Return true iff this constructor is finite (it is nullary or * each of its argument types are finite). This function can * only be called for resolved constructors. */ - bool isFinite() const throw(AssertionException); + bool isFinite() const throw(IllegalArgumentException); /** * Return true iff this constructor is well-founded (there exist * ground terms). The constructor must be resolved or an * exception is thrown. */ - bool isWellFounded() const throw(AssertionException); + bool isWellFounded() const throw(IllegalArgumentException); /** * Construct and return a ground term of this constructor. The * constructor must be both resolved and well-founded, or else an * exception is thrown. */ - Expr mkGroundTerm( Type t ) const throw(AssertionException); + Expr mkGroundTerm( Type t ) const throw(IllegalArgumentException); /** * Returns true iff this Datatype constructor has already been @@ -441,7 +440,7 @@ private: const std::vector<Type>& replacements, const std::vector< SortConstructorType >& paramTypes, const std::vector< DatatypeType >& paramReplacements) - throw(AssertionException, DatatypeResolutionException); + throw(IllegalArgumentException, DatatypeResolutionException); friend class ExprManager;// for access to resolve() public: @@ -484,7 +483,7 @@ public: * cardinalities of its constructors). The Datatype must be * resolved. */ - Cardinality getCardinality() const throw(AssertionException); + Cardinality getCardinality() const throw(IllegalArgumentException); /** * Return true iff this Datatype is finite (all constructors are @@ -492,32 +491,32 @@ public: * datatype is not well-founded, this function returns false. The * Datatype must be resolved or an exception is thrown. */ - bool isFinite() const throw(AssertionException); + bool isFinite() const throw(IllegalArgumentException); /** * Return true iff this datatype is well-founded (there exist ground * terms). The Datatype must be resolved or an exception is thrown. */ - bool isWellFounded() const throw(AssertionException); + bool isWellFounded() const throw(IllegalArgumentException); /** * Construct and return a ground term of this Datatype. The * Datatype must be both resolved and well-founded, or else an * exception is thrown. */ - Expr mkGroundTerm( Type t ) const throw(AssertionException); + Expr mkGroundTerm( Type t ) const throw(IllegalArgumentException); /** * Get the DatatypeType associated to this Datatype. Can only be * called post-resolution. */ - DatatypeType getDatatypeType() const throw(AssertionException); + DatatypeType getDatatypeType() const throw(IllegalArgumentException); /** * Get the DatatypeType associated to this (parameterized) Datatype. Can only be * called post-resolution. */ - DatatypeType getDatatypeType(const std::vector<Type>& params) const throw(AssertionException); + DatatypeType getDatatypeType(const std::vector<Type>& params) const throw(IllegalArgumentException); /** * Return true iff the two Datatypes are the same. diff --git a/src/util/exception.cpp b/src/util/exception.cpp new file mode 100644 index 000000000..d31f52fe7 --- /dev/null +++ b/src/util/exception.cpp @@ -0,0 +1,102 @@ +/********************* */ +/*! \file exception.cpp + ** \verbatim + ** Original author: mdeters + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009-2012 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief CVC4's exception base class and some associated utilities + ** + ** CVC4's exception base class and some associated utilities. + **/ + +#include "util/exception.h" +#include <string> +#include <cstdio> +#include <cstdlib> +#include <cstdarg> + +using namespace std; +using namespace CVC4; + +void IllegalArgumentException::construct(const char* header, const char* extra, + const char* function, const char* fmt, + va_list args) { + // try building the exception msg with a smallish buffer first, + // then with a larger one if sprintf tells us to. + int n = 512; + char* buf; + + for(;;) { + buf = new char[n]; + + int size; + if(extra == NULL) { + size = snprintf(buf, n, "%s\n%s\n", + header, function); + } else { + size = snprintf(buf, n, "%s\n%s\n\n %s\n", + header, function, extra); + } + + if(size < n) { + va_list args_copy; + va_copy(args_copy, args); + size += vsnprintf(buf + size, n - size, fmt, args_copy); + va_end(args_copy); + + if(size < n) { + break; + } + } + + if(size >= n) { + // try again with a buffer that's large enough + n = size + 1; + delete [] buf; + } + } + + setMessage(string(buf)); + + delete [] buf; +} + +void IllegalArgumentException::construct(const char* header, const char* extra, + const char* function) { + // try building the exception msg with a smallish buffer first, + // then with a larger one if sprintf tells us to. + int n = 256; + char* buf; + + for(;;) { + buf = new char[n]; + + int size; + if(extra == NULL) { + size = snprintf(buf, n, "%s.\n%s\n", + header, function); + } else { + size = snprintf(buf, n, "%s.\n%s\n\n %s\n", + header, function, extra); + } + + if(size < n) { + break; + } else { + // try again with a buffer that's large enough + n = size + 1; + delete [] buf; + } + } + + setMessage(string(buf)); + + delete [] buf; +} diff --git a/src/util/exception.h b/src/util/exception.h index fe01eba36..89e42b6d1 100644 --- a/src/util/exception.h +++ b/src/util/exception.h @@ -11,7 +11,7 @@ ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** - ** \brief CVC4's exception base class and some associated utilities. + ** \brief CVC4's exception base class and some associated utilities ** ** CVC4's exception base class and some associated utilities. **/ @@ -25,6 +25,8 @@ #include <string> #include <sstream> #include <exception> +#include <cstdlib> +#include <cstdarg> namespace CVC4 { @@ -75,6 +77,51 @@ public: };/* class Exception */ +class CVC4_PUBLIC IllegalArgumentException : public Exception { +protected: + IllegalArgumentException() : Exception() {} + + void construct(const char* header, const char* extra, + const char* function, const char* fmt, ...) { + va_list args; + va_start(args, fmt); + construct(header, extra, function, fmt, args); + va_end(args); + } + + void construct(const char* header, const char* extra, + const char* function, const char* fmt, va_list args); + + void construct(const char* header, const char* extra, + const char* function); + +public: + IllegalArgumentException(const char* condStr, const char* argDesc, + const char* function, const char* fmt, ...) : + Exception() { + va_list args; + va_start(args, fmt); + construct("Illegal argument detected", + ( std::string("`") + argDesc + "' is a bad argument" + + (*condStr == '\0' ? std::string() : + ( std::string("; expected ") + + condStr + " to hold" )) ).c_str(), + function, fmt, args); + va_end(args); + } + + IllegalArgumentException(const char* condStr, const char* argDesc, + const char* function) : + Exception() { + construct("Illegal argument detected", + ( std::string("`") + argDesc + "' is a bad argument" + + (*condStr == '\0' ? std::string() : + ( std::string("; expected ") + + condStr + " to hold" )) ).c_str(), + function); + } +};/* class IllegalArgumentException */ + inline std::ostream& operator<<(std::ostream& os, const Exception& e) throw() CVC4_PUBLIC; inline std::ostream& operator<<(std::ostream& os, const Exception& e) throw() { e.toStream(os); @@ -83,4 +130,42 @@ inline std::ostream& operator<<(std::ostream& os, const Exception& e) throw() { }/* CVC4 namespace */ +#if defined(__BUILDING_CVC4LIB) || defined(__BUILDING_CVC4LIB_UNIT_TEST) +# include "util/Assert.h" +#endif /* __BUILDING_CVC4LIB || __BUILDING_CVC4LIB_UNIT_TEST */ + +namespace CVC4 { + +#ifndef CheckArgument +template <class T> inline void CheckArgument(bool cond, const T& arg, const char* fmt, ...) CVC4_PUBLIC; +template <class T> inline void CheckArgument(bool cond, const T& arg, const char* fmt, ...) { + if(EXPECT_FALSE( !cond )) { \ + throw ::CVC4::IllegalArgumentException("", "", ""); \ + } \ +} +template <class T> inline void CheckArgument(bool cond, const T& arg) CVC4_PUBLIC; +template <class T> inline void CheckArgument(bool cond, const T& arg) { + if(EXPECT_FALSE( !cond )) { \ + throw ::CVC4::IllegalArgumentException("", "", ""); \ + } \ +} +#endif /* CheckArgument */ + +#ifndef DebugCheckArgument +template <class T> inline void DebugCheckArgument(bool cond, const T& arg, const char* fmt, ...) CVC4_PUBLIC; +template <class T> inline void DebugCheckArgument(bool cond, const T& arg, const char* fmt, ...) { + if(EXPECT_FALSE( !cond )) { \ + throw ::CVC4::IllegalArgumentException("", "", ""); \ + } \ +} +template <class T> inline void DebugCheckArgument(bool cond, const T& arg) CVC4_PUBLIC; +template <class T> inline void DebugCheckArgument(bool cond, const T& arg) { + if(EXPECT_FALSE( !cond )) { \ + throw ::CVC4::IllegalArgumentException("", "", ""); \ + } \ +} +#endif /* DebugCheckArgument */ + +}/* CVC4 namespace */ + #endif /* __CVC4__EXCEPTION_H */ diff --git a/src/util/integer_cln_imp.h b/src/util/integer_cln_imp.h index 7fd6a2694..5dfcae6d2 100644 --- a/src/util/integer_cln_imp.h +++ b/src/util/integer_cln_imp.h @@ -31,7 +31,7 @@ #include <cln/integer_io.h> #include <limits> -#include "util/Assert.h" +#include "util/exception.h" namespace CVC4 { @@ -232,7 +232,7 @@ public: } Integer oneExtend(uint32_t size, uint32_t amount) const { - Assert((*this) < Integer(1).multiplyByPow2(size)); + DebugCheckArgument((*this) < Integer(1).multiplyByPow2(size), size); cln::cl_byte range(amount, size); cln::cl_I allones = (cln::cl_I(1) << (size + amount))- 1; // 2^size - 1 Integer temp(allones); @@ -291,7 +291,7 @@ public: * If y divides *this, then exactQuotient returns (this/y) */ Integer exactQuotient(const Integer& y) const { - Assert(y.divides(*this)); + DebugCheckArgument(y.divides(*this), y); return Integer( cln::exquo(d_value, y.d_value) ); } @@ -316,7 +316,7 @@ public: }else if(exp == 0){ return Integer( 1 ); }else{ - Unimplemented(); + throw Exception("Negative exponent in Integer::pow()"); } } @@ -367,8 +367,7 @@ public: fprinthexadecimal(ss,d_value); break; default: - Unhandled(); - break; + throw Exception("Unhandled base in Integer::toString()"); } std::string output = ss.str(); for( unsigned i = 0; i <= output.length(); ++i){ @@ -382,7 +381,6 @@ public: int sgn() const { cln::cl_I sgn = cln::signum(d_value); - Assert(sgn == 0 || sgn == -1 || sgn == 1); return cln::cl_I_to_int(sgn); } @@ -402,19 +400,19 @@ public: long getLong() const { // ensure there isn't overflow - AlwaysAssert(d_value <= std::numeric_limits<long>::max(), - "Overflow detected in Integer::getLong()"); - AlwaysAssert(d_value >= std::numeric_limits<long>::min(), - "Overflow detected in Integer::getLong()"); + CheckArgument(d_value <= std::numeric_limits<long>::max(), this, + "Overflow detected in Integer::getLong()"); + CheckArgument(d_value >= std::numeric_limits<long>::min(), this, + "Overflow detected in Integer::getLong()"); return cln::cl_I_to_long(d_value); } unsigned long getUnsignedLong() const { // ensure there isn't overflow - AlwaysAssert(d_value <= std::numeric_limits<unsigned long>::max(), - "Overflow detected in Integer::getUnsignedLong()"); - AlwaysAssert(d_value >= std::numeric_limits<unsigned long>::min(), - "Overflow detected in Integer::getUnsignedLong()"); + CheckArgument(d_value <= std::numeric_limits<unsigned long>::max(), this, + "Overflow detected in Integer::getUnsignedLong()"); + CheckArgument(d_value >= std::numeric_limits<unsigned long>::min(), this, + "Overflow detected in Integer::getUnsignedLong()"); return cln::cl_I_to_ulong(d_value); } diff --git a/src/util/integer_gmp_imp.h b/src/util/integer_gmp_imp.h index 5b6468a9e..66428ec41 100644 --- a/src/util/integer_gmp_imp.h +++ b/src/util/integer_gmp_imp.h @@ -25,8 +25,8 @@ #include <string> #include <iostream> -#include "util/Assert.h" #include "util/gmp_util.h" +#include "util/exception.h" namespace CVC4 { @@ -178,7 +178,7 @@ public: */ Integer oneExtend(uint32_t size, uint32_t amount) const { // check that the size is accurate - Assert ((*this) < Integer(1).multiplyByPow2(size)); + DebugCheckArgument((*this) < Integer(1).multiplyByPow2(size), size); mpz_class res = d_value; for (unsigned i = size; i < size + amount; ++i) { @@ -251,7 +251,7 @@ public: * If y divides *this, then exactQuotient returns (this/y) */ Integer exactQuotient(const Integer& y) const { - Assert(y.divides(*this)); + DebugCheckArgument(y.divides(*this), y); mpz_class q; mpz_divexact(q.get_mpz_t(), d_value.get_mpz_t(), y.d_value.get_mpz_t()); return Integer( q ); @@ -346,15 +346,15 @@ public: long getLong() const { long si = d_value.get_si(); // ensure there wasn't overflow - AlwaysAssert(mpz_cmp_si(d_value.get_mpz_t(), si) == 0, + CheckArgument(mpz_cmp_si(d_value.get_mpz_t(), si) == 0, this, "Overflow detected in Integer::getLong()"); return si; } unsigned long getUnsignedLong() const { unsigned long ui = d_value.get_ui(); // ensure there wasn't overflow - AlwaysAssert(mpz_cmp_ui(d_value.get_mpz_t(), ui) == 0, - "Overflow detected in Integer::getUnsignedLong()"); + CheckArgument(mpz_cmp_ui(d_value.get_mpz_t(), ui) == 0, this, + "Overflow detected in Integer::getUnsignedLong()"); return ui; } diff --git a/src/util/predicate.h b/src/util/predicate.h index 18e0b8b70..ba050bd43 100644 --- a/src/util/predicate.h +++ b/src/util/predicate.h @@ -23,7 +23,7 @@ #ifndef __CVC4__PREDICATE_H #define __CVC4__PREDICATE_H -#include "util/Assert.h" +#include "util/exception.h" namespace CVC4 { diff --git a/src/util/rational_cln_imp.h b/src/util/rational_cln_imp.h index 182e813cd..575f09ef5 100644 --- a/src/util/rational_cln_imp.h +++ b/src/util/rational_cln_imp.h @@ -25,6 +25,7 @@ #include <gmp.h> #include <string> #include <sstream> +#include <cassert> #include <cln/rational.h> #include <cln/input.h> #include <cln/io.h> @@ -32,7 +33,7 @@ #include <cln/rational_io.h> #include <cln/number_io.h> -#include "util/Assert.h" +#include "util/exception.h" #include "util/integer.h" namespace CVC4 { @@ -213,7 +214,7 @@ public: }else if(cln::minusp(d_value)){ return -1; }else{ - Assert(cln::plusp(d_value)); + assert(cln::plusp(d_value)); return 1; } } diff --git a/src/util/rational_gmp_imp.h b/src/util/rational_gmp_imp.h index b86dc32f2..383f0fb2b 100644 --- a/src/util/rational_gmp_imp.h +++ b/src/util/rational_gmp_imp.h @@ -26,6 +26,7 @@ #include <string> #include "util/integer.h" +#include "util/exception.h" namespace CVC4 { diff --git a/src/util/result.h b/src/util/result.h index f0cf3f20e..0894007bc 100644 --- a/src/util/result.h +++ b/src/util/result.h @@ -24,16 +24,10 @@ #include <iostream> #include <string> -#include "util/Assert.h" +#include "util/exception.h" namespace CVC4 { -// TODO: either templatize Result on its Kind (Sat/Validity) or subclass. -// TODO: INVALID/SAT provide models, etc?---perhaps just by linking back -// into the SmtEngine that produced the Result? -// TODO: make unconstructible except by SmtEngine? That would ensure that -// any Result in the system is bona fide. - class Result; std::ostream& operator<<(std::ostream& out, const Result& r) CVC4_PUBLIC; @@ -137,9 +131,9 @@ public: return d_which == TYPE_NONE; } enum UnknownExplanation whyUnknown() const { - AlwaysAssert( isUnknown(), - "This result is not unknown, so the reason for " - "being unknown cannot be inquired of it" ); + CheckArgument( isUnknown(), this, + "This result is not unknown, so the reason for " + "being unknown cannot be inquired of it" ); return d_unknownExplanation; } diff --git a/src/util/sexpr.h b/src/util/sexpr.h index 4feffc18f..345a6c132 100644 --- a/src/util/sexpr.h +++ b/src/util/sexpr.h @@ -28,7 +28,7 @@ #include "util/integer.h" #include "util/rational.h" -#include "util/Assert.h" +#include "util/exception.h" namespace CVC4 { @@ -182,7 +182,7 @@ inline bool SExpr::isKeyword() const { } inline std::string SExpr::getValue() const { - AlwaysAssert( isAtom() ); + CheckArgument( isAtom(), this ); switch(d_sexprType) { case SEXPR_INTEGER: return d_integerValue.toString(); @@ -198,24 +198,24 @@ inline std::string SExpr::getValue() const { case SEXPR_STRING: case SEXPR_KEYWORD: return d_stringValue; - default: - Unhandled(d_sexprType); + case SEXPR_NOT_ATOM: + return std::string(); } - return d_stringValue; + return std::string(); } inline const CVC4::Integer& SExpr::getIntegerValue() const { - AlwaysAssert( isInteger() ); + CheckArgument( isInteger(), this ); return d_integerValue; } inline const CVC4::Rational& SExpr::getRationalValue() const { - AlwaysAssert( isRational() ); + CheckArgument( isRational(), this ); return d_rationalValue; } inline const std::vector<SExpr>& SExpr::getChildren() const { - AlwaysAssert( !isAtom() ); + CheckArgument( !isAtom(), this ); return d_children; } diff --git a/src/util/statistics_registry.cpp b/src/util/statistics_registry.cpp index f2a698a48..48e1355ec 100644 --- a/src/util/statistics_registry.cpp +++ b/src/util/statistics_registry.cpp @@ -50,36 +50,38 @@ StatisticsRegistry* StatisticsRegistry::current() { return stats::getStatisticsRegistry(smt::currentSmtEngine()); } -void StatisticsRegistry::registerStat(Stat* s) throw(AssertionException) { +void StatisticsRegistry::registerStat(Stat* s) throw(CVC4::IllegalArgumentException) { #ifdef CVC4_STATISTICS_ON StatSet& stats = current()->d_stats; - AlwaysAssert(stats.find(s) == stats.end(), - "Statistic `%s' was already registered with this registry.", s->getName().c_str()); + CheckArgument(stats.find(s) == stats.end(), s, + "Statistic `%s' was already registered with this registry.", + s->getName().c_str()); stats.insert(s); #endif /* CVC4_STATISTICS_ON */ }/* StatisticsRegistry::registerStat() */ -void StatisticsRegistry::unregisterStat(Stat* s) throw(AssertionException) { +void StatisticsRegistry::unregisterStat(Stat* s) throw(CVC4::IllegalArgumentException) { #ifdef CVC4_STATISTICS_ON StatSet& stats = current()->d_stats; - AlwaysAssert(stats.find(s) != stats.end(), - "Statistic `%s' was not registered with this registry.", s->getName().c_str()); + CheckArgument(stats.find(s) != stats.end(), s, + "Statistic `%s' was not registered with this registry.", + s->getName().c_str()); stats.erase(s); #endif /* CVC4_STATISTICS_ON */ }/* StatisticsRegistry::unregisterStat() */ #endif /* ! __BUILDING_STATISTICS_FOR_EXPORT */ -void StatisticsRegistry::registerStat_(Stat* s) throw(AssertionException) { +void StatisticsRegistry::registerStat_(Stat* s) throw(CVC4::IllegalArgumentException) { #ifdef CVC4_STATISTICS_ON - AlwaysAssert(d_stats.find(s) == d_stats.end()); + CheckArgument(d_stats.find(s) == d_stats.end(), s); d_stats.insert(s); #endif /* CVC4_STATISTICS_ON */ }/* StatisticsRegistry::registerStat_() */ -void StatisticsRegistry::unregisterStat_(Stat* s) throw(AssertionException) { +void StatisticsRegistry::unregisterStat_(Stat* s) throw(CVC4::IllegalArgumentException) { #ifdef CVC4_STATISTICS_ON - AlwaysAssert(d_stats.find(s) != d_stats.end()); + CheckArgument(d_stats.find(s) != d_stats.end(), s); d_stats.erase(s); #endif /* CVC4_STATISTICS_ON */ }/* StatisticsRegistry::unregisterStat_() */ @@ -98,7 +100,7 @@ void StatisticsRegistry::flushInformation(std::ostream &out) const { void TimerStat::start() { if(__CVC4_USE_STATISTICS) { - AlwaysAssert(!d_running); + CheckArgument(!d_running, *this, "timer already running"); clock_gettime(CLOCK_MONOTONIC, &d_start); d_running = true; } @@ -106,7 +108,7 @@ void TimerStat::start() { void TimerStat::stop() { if(__CVC4_USE_STATISTICS) { - AlwaysAssert(d_running); + CheckArgument(d_running, *this, "timer not running"); ::timespec end; clock_gettime(CLOCK_MONOTONIC, &end); d_data += end - d_start; diff --git a/src/util/statistics_registry.h b/src/util/statistics_registry.h index 870a88d66..99168353f 100644 --- a/src/util/statistics_registry.h +++ b/src/util/statistics_registry.h @@ -30,8 +30,7 @@ #include <ctime> #include <vector> #include <stdint.h> - -#include "util/Assert.h" +#include <cassert> namespace CVC4 { @@ -69,10 +68,11 @@ public: * will throw an assertion exception if the given name contains the * statistic delimiter string. */ - Stat(const std::string& name) throw(CVC4::AssertionException) : + Stat(const std::string& name) throw(CVC4::IllegalArgumentException) : d_name(name) { if(__CVC4_USE_STATISTICS) { - AlwaysAssert(d_name.find(", ") == std::string::npos); + CheckArgument(d_name.find(", ") == std::string::npos, name, + "Statistics names cannot include a comma (',')"); } } @@ -270,11 +270,7 @@ public: /** Get the value of the referenced data cell. */ const T& getData() const { - if(__CVC4_USE_STATISTICS) { - return *d_data; - } else { - Unreachable(); - } + return *d_data; } };/* class ReferenceStat<T> */ @@ -316,11 +312,7 @@ public: /** Get the underlying data value. */ const T& getData() const { - if(__CVC4_USE_STATISTICS) { - return d_data; - } else { - Unreachable(); - } + return d_data; } };/* class BackedStat<T> */ @@ -362,11 +354,7 @@ public: /** Get the data of the underlying (wrapped) statistic. */ const T& getData() const { - if(__CVC4_USE_STATISTICS) { - return d_stat.getData(); - } else { - Unreachable(); - } + return d_stat.getData(); } SExpr getValue() const { @@ -569,11 +557,14 @@ public: StatisticsRegistry() {} /** Construct a statistics registry */ - StatisticsRegistry(const std::string& name) throw(CVC4::AssertionException) : + StatisticsRegistry(const std::string& name) + throw(CVC4::IllegalArgumentException) : Stat(name) { d_prefix = name; if(__CVC4_USE_STATISTICS) { - AlwaysAssert(d_name.find(s_regDelim) == std::string::npos); + CheckArgument(d_name.find(s_regDelim) == std::string::npos, name, + "StatisticsRegistry names cannot contain the string \"%s\"", + s_regDelim.c_str()); } } @@ -608,17 +599,17 @@ public: #if (defined(__BUILDING_CVC4LIB) || defined(__BUILDING_CVC4LIB_UNIT_TEST)) && !defined(__BUILDING_STATISTICS_FOR_EXPORT) /** Register a new statistic, making it active. */ - static void registerStat(Stat* s) throw(AssertionException); + static void registerStat(Stat* s) throw(CVC4::IllegalArgumentException); /** Unregister an active statistic, making it inactive. */ - static void unregisterStat(Stat* s) throw(AssertionException); + static void unregisterStat(Stat* s) throw(CVC4::IllegalArgumentException); #endif /* (__BUILDING_CVC4LIB || __BUILDING_CVC4LIB) && ! __BUILDING_STATISTICS_FOR_EXPORT */ /** Register a new statistic */ - void registerStat_(Stat* s) throw(AssertionException); + void registerStat_(Stat* s) throw(CVC4::IllegalArgumentException); /** Unregister a new statistic */ - void unregisterStat_(Stat* s) throw(AssertionException); + void unregisterStat_(Stat* s) throw(CVC4::IllegalArgumentException); };/* class StatisticsRegistry */ @@ -630,11 +621,11 @@ public: inline timespec& operator+=(timespec& a, const timespec& b) { // assumes a.tv_nsec and b.tv_nsec are in range const long nsec_per_sec = 1000000000L; // one thousand million - Assert(a.tv_nsec >= 0 && a.tv_nsec < nsec_per_sec); - Assert(b.tv_nsec >= 0 && b.tv_nsec < nsec_per_sec); + CheckArgument(a.tv_nsec >= 0 && a.tv_nsec < nsec_per_sec, a); + CheckArgument(b.tv_nsec >= 0 && b.tv_nsec < nsec_per_sec, b); a.tv_sec += b.tv_sec; long nsec = a.tv_nsec + b.tv_nsec; - Assert(nsec >= 0); + assert(nsec >= 0); if(nsec < 0) { nsec += nsec_per_sec; --a.tv_sec; @@ -643,7 +634,7 @@ inline timespec& operator+=(timespec& a, const timespec& b) { nsec -= nsec_per_sec; ++a.tv_sec; } - Assert(nsec >= 0 && nsec < nsec_per_sec); + assert(nsec >= 0 && nsec < nsec_per_sec); a.tv_nsec = nsec; return a; } @@ -652,8 +643,8 @@ inline timespec& operator+=(timespec& a, const timespec& b) { inline timespec& operator-=(timespec& a, const timespec& b) { // assumes a.tv_nsec and b.tv_nsec are in range const long nsec_per_sec = 1000000000L; // one thousand million - Assert(a.tv_nsec >= 0 && a.tv_nsec < nsec_per_sec); - Assert(b.tv_nsec >= 0 && b.tv_nsec < nsec_per_sec); + CheckArgument(a.tv_nsec >= 0 && a.tv_nsec < nsec_per_sec, a); + CheckArgument(b.tv_nsec >= 0 && b.tv_nsec < nsec_per_sec, b); a.tv_sec -= b.tv_sec; long nsec = a.tv_nsec - b.tv_nsec; if(nsec < 0) { @@ -664,7 +655,7 @@ inline timespec& operator-=(timespec& a, const timespec& b) { nsec -= nsec_per_sec; ++a.tv_sec; } - Assert(nsec >= 0 && nsec < nsec_per_sec); + assert(nsec >= 0 && nsec < nsec_per_sec); a.tv_nsec = nsec; return a; } @@ -855,9 +846,9 @@ public: RegisterStatistic(StatisticsRegistry* reg, Stat* stat) : d_reg(reg), d_stat(stat) { - Assert(d_reg != NULL, - "You need to specify a statistics registry" - "on which to set the statistic"); + CheckArgument(reg != NULL, reg, + "You need to specify a statistics registry" + "on which to set the statistic"); d_reg->registerStat_(d_stat); } diff --git a/src/util/subrange_bound.h b/src/util/subrange_bound.h index 5de17106d..ffb2a1eaf 100644 --- a/src/util/subrange_bound.h +++ b/src/util/subrange_bound.h @@ -23,7 +23,7 @@ #define __CVC4__SUBRANGE_BOUND_H #include "util/integer.h" -#include "util/Assert.h" +#include "util/exception.h" #include <limits> @@ -222,7 +222,7 @@ public: * precondition: joinIsBounded(a,b) is true */ static SubrangeBounds join(const SubrangeBounds& a, const SubrangeBounds& b){ - Assert(joinIsBounded(a,b)); + DebugCheckArgument(joinIsBounded(a,b), a); SubrangeBound newLower = SubrangeBound::min(a.lower, b.lower); SubrangeBound newUpper = SubrangeBound::max(a.upper, b.upper); return SubrangeBounds(newLower, newUpper); diff --git a/test/system/ouroborous.cpp b/test/system/ouroborous.cpp index ac864d16b..daa7a9aae 100644 --- a/test/system/ouroborous.cpp +++ b/test/system/ouroborous.cpp @@ -72,8 +72,8 @@ string translate(string in, InputLanguage inlang, OutputLanguage outlang) { Expr e = psr->nextExpression(); stringstream ss; ss << Expr::setlanguage(outlang) << Expr::setdepth(-1) << e; - AlwaysAssert(psr->nextExpression().isNull(), "next expr should be null"); - AlwaysAssert(psr->done(), "parser should be done"); + assert(psr->nextExpression().isNull());// next expr should be null + assert(psr->done());// parser should be done string s = ss.str(); cout << "got this:" << endl << s << endl @@ -81,7 +81,7 @@ string translate(string in, InputLanguage inlang, OutputLanguage outlang) { psr->setInput(Input::newStringInput(toInputLanguage(outlang), s, "internal-buffer")); Expr f = psr->nextExpression(); - AlwaysAssert(e == f); + assert(e == f); cout << "got same expressions " << e.getId() << " and " << f.getId() << endl << "==============================================" << endl; @@ -103,7 +103,7 @@ void runTestString(std::string instr, InputLanguage instrlang = input::LANG_SMTL string out = translate(cvc, input::LANG_CVC4, output::LANG_SMTLIB_V2); cout << "back to SMT2 : " << out << endl << endl; - AlwaysAssert(out == smt2, "differences in output"); + assert(out == smt2);// differences in output } @@ -121,7 +121,7 @@ int runTest() { delete c; } - AlwaysAssert(psr->done(), "parser should be done"); + assert(psr->done());// parser should be done cout << Expr::setdepth(-1); diff --git a/test/unit/expr/expr_manager_public.h b/test/unit/expr/expr_manager_public.h index e709648c9..e0ebe9640 100644 --- a/test/unit/expr/expr_manager_public.h +++ b/test/unit/expr/expr_manager_public.h @@ -23,7 +23,6 @@ #include "expr/expr_manager.h" #include "expr/expr.h" -#include "util/Assert.h" #include "util/exception.h" using namespace CVC4; @@ -120,12 +119,12 @@ public: void testMkAssociativeTooFew() { std::vector<Expr> vars = mkVars(d_exprManager->booleanType(), 1); - TS_ASSERT_THROWS( d_exprManager->mkAssociative(AND,vars), AssertionException); + TS_ASSERT_THROWS( d_exprManager->mkAssociative(AND,vars), IllegalArgumentException); } void testMkAssociativeBadKind() { std::vector<Expr> vars = mkVars(d_exprManager->integerType(), 10); - TS_ASSERT_THROWS( d_exprManager->mkAssociative(TUPLE,vars), AssertionException); + TS_ASSERT_THROWS( d_exprManager->mkAssociative(TUPLE,vars), IllegalArgumentException); } }; diff --git a/test/unit/expr/expr_public.h b/test/unit/expr/expr_public.h index 279d4bebe..0d7608cac 100644 --- a/test/unit/expr/expr_public.h +++ b/test/unit/expr/expr_public.h @@ -23,7 +23,6 @@ #include "expr/expr_manager.h" #include "expr/expr.h" -#include "util/Assert.h" #include "util/exception.h" using namespace CVC4; diff --git a/test/unit/expr/kind_map_black.h b/test/unit/expr/kind_map_black.h index e5bcdd298..b994bd3af 100644 --- a/test/unit/expr/kind_map_black.h +++ b/test/unit/expr/kind_map_black.h @@ -102,7 +102,7 @@ public: TS_ASSERT(!(AND ^ AND ^ AND).isEmpty()); #ifdef CVC4_ASSERTIONS - TS_ASSERT_THROWS(~LAST_KIND, IllegalArgumentException); + TS_ASSERT_THROWS(~LAST_KIND, AssertArgumentException); #endif /* CVC4_ASSERTIONS */ } diff --git a/test/unit/expr/node_black.h b/test/unit/expr/node_black.h index 1518efadf..1a5f5ecfa 100644 --- a/test/unit/expr/node_black.h +++ b/test/unit/expr/node_black.h @@ -427,8 +427,8 @@ public: TS_ASSERT( f == fa.getOperator() ); #ifdef CVC4_ASSERTIONS - TS_ASSERT_THROWS( f.getOperator(), AssertionException ); - TS_ASSERT_THROWS( a.getOperator(), AssertionException ); + TS_ASSERT_THROWS( f.getOperator(), IllegalArgumentException ); + TS_ASSERT_THROWS( a.getOperator(), IllegalArgumentException ); #endif /* CVC4_ASSERTIONS */ } diff --git a/test/unit/expr/type_cardinality_public.h b/test/unit/expr/type_cardinality_public.h index 7ba212dd5..78a872aea 100644 --- a/test/unit/expr/type_cardinality_public.h +++ b/test/unit/expr/type_cardinality_public.h @@ -26,7 +26,6 @@ #include "expr/type.h" #include "expr/expr_manager.h" #include "util/cardinality.h" -#include "util/Assert.h" using namespace CVC4; using namespace CVC4::kind; diff --git a/test/unit/theory/logic_info_white.h b/test/unit/theory/logic_info_white.h index a2f61f5d2..c091eab71 100644 --- a/test/unit/theory/logic_info_white.h +++ b/test/unit/theory/logic_info_white.h @@ -450,31 +450,29 @@ public: LogicInfo info; TS_ASSERT( !info.isLocked() ); -#ifdef CVC4_ASSERTIONS - TS_ASSERT_THROWS( info.getLogicString(), CVC4::AssertionException ); - TS_ASSERT_THROWS( info.isTheoryEnabled( THEORY_BUILTIN ), CVC4::AssertionException ); - TS_ASSERT_THROWS( info.isTheoryEnabled( THEORY_BOOL ), CVC4::AssertionException ); - TS_ASSERT_THROWS( info.isTheoryEnabled( THEORY_UF ), CVC4::AssertionException ); - TS_ASSERT_THROWS( info.isTheoryEnabled( THEORY_ARITH ), CVC4::AssertionException ); - TS_ASSERT_THROWS( info.isTheoryEnabled( THEORY_ARRAY ), CVC4::AssertionException ); - TS_ASSERT_THROWS( info.isTheoryEnabled( THEORY_BV ), CVC4::AssertionException ); - TS_ASSERT_THROWS( info.isTheoryEnabled( THEORY_DATATYPES ), CVC4::AssertionException ); - TS_ASSERT_THROWS( info.isTheoryEnabled( THEORY_QUANTIFIERS ), CVC4::AssertionException ); - TS_ASSERT_THROWS( info.isTheoryEnabled( THEORY_REWRITERULES ), CVC4::AssertionException ); - TS_ASSERT_THROWS( ! info.isPure( THEORY_BUILTIN ), CVC4::AssertionException ); - TS_ASSERT_THROWS( ! info.isPure( THEORY_BOOL ), CVC4::AssertionException ); - TS_ASSERT_THROWS( ! info.isPure( THEORY_UF ), CVC4::AssertionException ); - TS_ASSERT_THROWS( ! info.isPure( THEORY_ARITH ), CVC4::AssertionException ); - TS_ASSERT_THROWS( ! info.isPure( THEORY_ARRAY ), CVC4::AssertionException ); - TS_ASSERT_THROWS( ! info.isPure( THEORY_BV ), CVC4::AssertionException ); - TS_ASSERT_THROWS( ! info.isPure( THEORY_DATATYPES ), CVC4::AssertionException ); - TS_ASSERT_THROWS( ! info.isPure( THEORY_QUANTIFIERS ), CVC4::AssertionException ); - TS_ASSERT_THROWS( ! info.isPure( THEORY_REWRITERULES ), CVC4::AssertionException ); - TS_ASSERT_THROWS( info.isQuantified(), CVC4::AssertionException ); - TS_ASSERT_THROWS( info.areIntegersUsed(), CVC4::AssertionException ); - TS_ASSERT_THROWS( info.areRealsUsed(), CVC4::AssertionException ); - TS_ASSERT_THROWS( ! info.isLinear(), CVC4::AssertionException ); -#endif /* CVC4_ASSERTIONS */ + TS_ASSERT_THROWS( info.getLogicString(), CVC4::IllegalArgumentException ); + TS_ASSERT_THROWS( info.isTheoryEnabled( THEORY_BUILTIN ), CVC4::IllegalArgumentException ); + TS_ASSERT_THROWS( info.isTheoryEnabled( THEORY_BOOL ), CVC4::IllegalArgumentException ); + TS_ASSERT_THROWS( info.isTheoryEnabled( THEORY_UF ), CVC4::IllegalArgumentException ); + TS_ASSERT_THROWS( info.isTheoryEnabled( THEORY_ARITH ), CVC4::IllegalArgumentException ); + TS_ASSERT_THROWS( info.isTheoryEnabled( THEORY_ARRAY ), CVC4::IllegalArgumentException ); + TS_ASSERT_THROWS( info.isTheoryEnabled( THEORY_BV ), CVC4::IllegalArgumentException ); + TS_ASSERT_THROWS( info.isTheoryEnabled( THEORY_DATATYPES ), CVC4::IllegalArgumentException ); + TS_ASSERT_THROWS( info.isTheoryEnabled( THEORY_QUANTIFIERS ), CVC4::IllegalArgumentException ); + TS_ASSERT_THROWS( info.isTheoryEnabled( THEORY_REWRITERULES ), CVC4::IllegalArgumentException ); + TS_ASSERT_THROWS( ! info.isPure( THEORY_BUILTIN ), CVC4::IllegalArgumentException ); + TS_ASSERT_THROWS( ! info.isPure( THEORY_BOOL ), CVC4::IllegalArgumentException ); + TS_ASSERT_THROWS( ! info.isPure( THEORY_UF ), CVC4::IllegalArgumentException ); + TS_ASSERT_THROWS( ! info.isPure( THEORY_ARITH ), CVC4::IllegalArgumentException ); + TS_ASSERT_THROWS( ! info.isPure( THEORY_ARRAY ), CVC4::IllegalArgumentException ); + TS_ASSERT_THROWS( ! info.isPure( THEORY_BV ), CVC4::IllegalArgumentException ); + TS_ASSERT_THROWS( ! info.isPure( THEORY_DATATYPES ), CVC4::IllegalArgumentException ); + TS_ASSERT_THROWS( ! info.isPure( THEORY_QUANTIFIERS ), CVC4::IllegalArgumentException ); + TS_ASSERT_THROWS( ! info.isPure( THEORY_REWRITERULES ), CVC4::IllegalArgumentException ); + TS_ASSERT_THROWS( info.isQuantified(), CVC4::IllegalArgumentException ); + TS_ASSERT_THROWS( info.areIntegersUsed(), CVC4::IllegalArgumentException ); + TS_ASSERT_THROWS( info.areRealsUsed(), CVC4::IllegalArgumentException ); + TS_ASSERT_THROWS( ! info.isLinear(), CVC4::IllegalArgumentException ); info.lock(); TS_ASSERT( info.isLocked() ); @@ -503,17 +501,15 @@ public: TS_ASSERT( info.areRealsUsed() ); TS_ASSERT( ! info.isLinear() ); -#ifdef CVC4_ASSERTIONS - TS_ASSERT_THROWS( info.arithOnlyLinear(), CVC4::AssertionException ); - TS_ASSERT_THROWS( info.disableIntegers(), CVC4::AssertionException ); - TS_ASSERT_THROWS( info.disableQuantifiers(), CVC4::AssertionException ); - TS_ASSERT_THROWS( info.disableTheory(THEORY_BV), CVC4::AssertionException ); - TS_ASSERT_THROWS( info.disableTheory(THEORY_DATATYPES), CVC4::AssertionException ); - TS_ASSERT_THROWS( info.enableIntegers(), CVC4::AssertionException ); - TS_ASSERT_THROWS( info.disableReals(), CVC4::AssertionException ); - TS_ASSERT_THROWS( info.disableTheory(THEORY_ARITH), CVC4::AssertionException ); - TS_ASSERT_THROWS( info.disableTheory(THEORY_UF), CVC4::AssertionException ); -#endif /* CVC4_ASSERTIONS */ + TS_ASSERT_THROWS( info.arithOnlyLinear(), CVC4::IllegalArgumentException ); + TS_ASSERT_THROWS( info.disableIntegers(), CVC4::IllegalArgumentException ); + TS_ASSERT_THROWS( info.disableQuantifiers(), CVC4::IllegalArgumentException ); + TS_ASSERT_THROWS( info.disableTheory(THEORY_BV), CVC4::IllegalArgumentException ); + TS_ASSERT_THROWS( info.disableTheory(THEORY_DATATYPES), CVC4::IllegalArgumentException ); + TS_ASSERT_THROWS( info.enableIntegers(), CVC4::IllegalArgumentException ); + TS_ASSERT_THROWS( info.disableReals(), CVC4::IllegalArgumentException ); + TS_ASSERT_THROWS( info.disableTheory(THEORY_ARITH), CVC4::IllegalArgumentException ); + TS_ASSERT_THROWS( info.disableTheory(THEORY_UF), CVC4::IllegalArgumentException ); info = info.getUnlockedCopy(); TS_ASSERT( !info.isLocked() ); diff --git a/test/unit/util/assert_white.h b/test/unit/util/assert_white.h index 6d88f89bd..54c77b165 100644 --- a/test/unit/util/assert_white.h +++ b/test/unit/util/assert_white.h @@ -32,7 +32,7 @@ public: void testAssert() { #ifdef CVC4_ASSERTIONS TS_ASSERT_THROWS( Assert(false), AssertionException ); - TS_ASSERT_THROWS( AssertArgument(false, "x"), IllegalArgumentException ); + TS_ASSERT_THROWS( AssertArgument(false, "x"), AssertArgumentException ); #else /* CVC4_ASSERTIONS */ TS_ASSERT_THROWS_NOTHING( Assert(false) ); TS_ASSERT_THROWS_NOTHING( AssertArgument(false, "x") ); @@ -46,7 +46,7 @@ public: TS_ASSERT_THROWS( IllegalArgument("x"), IllegalArgumentException ); TS_ASSERT_THROWS( CheckArgument(false, "x"), IllegalArgumentException ); TS_ASSERT_THROWS( AlwaysAssertArgument(false, "x"), - IllegalArgumentException ); + AssertArgumentException ); TS_ASSERT_THROWS_NOTHING( AssertArgument(true, "x") ); TS_ASSERT_THROWS_NOTHING( AssertArgument(true, "x") ); } diff --git a/test/unit/util/boolean_simplification_black.h b/test/unit/util/boolean_simplification_black.h index 8f2d0d97f..e333e7205 100644 --- a/test/unit/util/boolean_simplification_black.h +++ b/test/unit/util/boolean_simplification_black.h @@ -135,7 +135,7 @@ public: #ifdef CVC4_ASSERTIONS in = Node(); - TS_ASSERT_THROWS( BooleanSimplification::negate(in), IllegalArgumentException ); + TS_ASSERT_THROWS( BooleanSimplification::negate(in), AssertArgumentException ); #endif /* CVC4_ASSERTIONS */ } @@ -170,7 +170,7 @@ public: #ifdef CVC4_ASSERTIONS in = d_nm->mkNode(kind::AND, a, b); - TS_ASSERT_THROWS( BooleanSimplification::simplifyClause(in), IllegalArgumentException ); + TS_ASSERT_THROWS( BooleanSimplification::simplifyClause(in), AssertArgumentException ); #endif /* CVC4_ASSERTIONS */ } @@ -195,7 +195,7 @@ public: #ifdef CVC4_ASSERTIONS in = d_nm->mkNode(kind::OR, a, b); - TS_ASSERT_THROWS( BooleanSimplification::simplifyHornClause(in), IllegalArgumentException ); + TS_ASSERT_THROWS( BooleanSimplification::simplifyHornClause(in), AssertArgumentException ); #endif /* CVC4_ASSERTIONS */ } @@ -216,7 +216,7 @@ public: #ifdef CVC4_ASSERTIONS in = d_nm->mkNode(kind::OR, a, b); - TS_ASSERT_THROWS( BooleanSimplification::simplifyConflict(in), IllegalArgumentException ); + TS_ASSERT_THROWS( BooleanSimplification::simplifyConflict(in), AssertArgumentException ); #endif /* CVC4_ASSERTIONS */ } |