namespace CVC4 {
class CVC4_PUBLIC Exception : public std::exception {
-protected:
+ protected:
std::string d_msg;
-public:
+ public:
// Constructors
- Exception() throw() : d_msg("Unknown exception") {}
- Exception(const std::string& msg) throw() : d_msg(msg) {}
- Exception(const char* msg) throw() : d_msg(msg) {}
+ Exception() : d_msg("Unknown exception") {}
+ Exception(const std::string& msg) : d_msg(msg) {}
+ Exception(const char* msg) : d_msg(msg) {}
// Destructor
- virtual ~Exception() throw() {}
+ virtual ~Exception() {}
// NON-VIRTUAL METHOD for setting and printing the error message
- void setMessage(const std::string& msg) throw() { d_msg = msg; }
- std::string getMessage() const throw() { return d_msg; }
+ void setMessage(const std::string& msg) { d_msg = msg; }
+ std::string getMessage() const { return d_msg; }
// overridden from base class std::exception
- virtual const char* what() const throw() { return d_msg.c_str(); }
+ const char* what() const noexcept override { return d_msg.c_str(); }
/**
* Get this exception as a string. Note that
* toString(), there is no stream, so the parameters are default
* and you'll get exprs and types printed using the AST language.
*/
- std::string toString() const throw() {
+ std::string toString() const
+ {
std::stringstream ss;
toStream(ss);
return ss.str();
* a derived class, it's recommended that this method print the
* type of exception before the actual message.
*/
- virtual void toStream(std::ostream& os) const throw() { os << d_msg; }
+ virtual void toStream(std::ostream& os) const { os << d_msg; }
};/* class Exception */
static std::string formatVariadic(const char* format, ...);
};/* 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() {
+inline std::ostream& operator<<(std::ostream& os,
+ const Exception& e) CVC4_PUBLIC;
+inline std::ostream& operator<<(std::ostream& os, const Exception& e)
+{
e.toStream(os);
return os;
}
#include "base/exception.h"
%}
-%ignore CVC4::operator<<(std::ostream&, const Exception&) throw();
-%ignore CVC4::Exception::Exception(const char*) throw();
+%ignore CVC4::operator<<(std::ostream&, const Exception&);
+%ignore CVC4::Exception::Exception(const char*);
%typemap(javabase) CVC4::Exception "java.lang.RuntimeException";
%rename(CVC4IllegalArgumentException) CVC4::IllegalArgumentException;
* An exception that is thrown when a datatype resolution fails.
*/
class CVC4_PUBLIC DatatypeResolutionException : public Exception {
-public:
+ public:
inline DatatypeResolutionException(std::string msg);
};/* class DatatypeResolutionException */
}
}
-TypeCheckingException::TypeCheckingException(const TypeCheckingException& t) throw() :
- Exception(t.d_msg), d_expr(new Expr(t.getExpression())) {
+TypeCheckingException::TypeCheckingException(const TypeCheckingException& t)
+ : Exception(t.d_msg), d_expr(new Expr(t.getExpression()))
+{
}
-TypeCheckingException::TypeCheckingException(const Expr& expr, std::string message) throw() :
- Exception(message), d_expr(new Expr(expr)) {
+TypeCheckingException::TypeCheckingException(const Expr& expr,
+ std::string message)
+ : Exception(message), d_expr(new Expr(expr))
+{
}
-TypeCheckingException::TypeCheckingException(ExprManager* em,
- const TypeCheckingExceptionPrivate* exc) throw() :
- Exception(exc->getMessage()), d_expr(new Expr(em, new Node(exc->getNode()))) {
+TypeCheckingException::TypeCheckingException(
+ ExprManager* em, const TypeCheckingExceptionPrivate* exc)
+ : Exception(exc->getMessage()),
+ d_expr(new Expr(em, new Node(exc->getNode())))
+{
}
-TypeCheckingException::~TypeCheckingException() throw() {
- delete d_expr;
-}
+TypeCheckingException::~TypeCheckingException() { delete d_expr; }
-void TypeCheckingException::toStream(std::ostream& os) const throw() {
+void TypeCheckingException::toStream(std::ostream& os) const
+{
os << "Error during type checking: " << d_msg << endl
<< "The ill-typed expression: " << *d_expr;
}
-Expr TypeCheckingException::getExpression() const throw() {
- return *d_expr;
-}
+Expr TypeCheckingException::getExpression() const { return *d_expr; }
Expr::Expr() :
d_node(new Node),
* Exception thrown in the case of type-checking errors.
*/
class CVC4_PUBLIC TypeCheckingException : public Exception {
-
+ private:
friend class SmtEngine;
friend class smt::SmtEnginePrivate;
-private:
-
/** The expression responsible for the error */
Expr* d_expr;
-protected:
-
- TypeCheckingException() throw() : Exception() {}
+ protected:
+ TypeCheckingException() : Exception() {}
TypeCheckingException(ExprManager* em,
- const TypeCheckingExceptionPrivate* exc) throw();
+ const TypeCheckingExceptionPrivate* exc);
-public:
-
- TypeCheckingException(const Expr& expr, std::string message) throw();
+ public:
+ TypeCheckingException(const Expr& expr, std::string message);
/** Copy constructor */
- TypeCheckingException(const TypeCheckingException& t) throw();
+ TypeCheckingException(const TypeCheckingException& t);
/** Destructor */
- ~TypeCheckingException() throw();
+ ~TypeCheckingException() override;
/**
* Get the Expr that caused the type-checking to fail.
*
* @return the expr
*/
- Expr getExpression() const throw();
+ Expr getExpression() const;
/**
* Returns the message corresponding to the type-checking failure.
* We prefer toStream() to toString() because that keeps the expr-depth
* and expr-language settings present in the stream.
*/
- void toStream(std::ostream& out) const throw();
+ void toStream(std::ostream& out) const override;
friend class ExprManager;
};/* class TypeCheckingException */
* Exception thrown in case of failure to export
*/
class CVC4_PUBLIC ExportUnsupportedException : public Exception {
-public:
- ExportUnsupportedException() throw():
- Exception("export unsupported") {
- }
- ExportUnsupportedException(const char* msg) throw():
- Exception(msg) {
- }
+ public:
+ ExportUnsupportedException() : Exception("export unsupported") {}
+ ExportUnsupportedException(const char* msg) : Exception(msg) {}
};/* class DatatypeExportUnsupportedException */
std::ostream& operator<<(std::ostream& out,
namespace CVC4 {
TypeCheckingExceptionPrivate::TypeCheckingExceptionPrivate(TNode node,
- std::string message) throw() :
- Exception(message),
- d_node(new Node(node)) {
+ std::string message)
+ : Exception(message), d_node(new Node(node))
+{
#ifdef CVC4_DEBUG
LastExceptionBuffer* current = LastExceptionBuffer::getCurrent();
if(current != NULL){
#endif /* CVC4_DEBUG */
}
-TypeCheckingExceptionPrivate::~TypeCheckingExceptionPrivate() throw () {
- delete d_node;
-}
+TypeCheckingExceptionPrivate::~TypeCheckingExceptionPrivate() { delete d_node; }
-void TypeCheckingExceptionPrivate::toStream(std::ostream& os) const throw() {
+void TypeCheckingExceptionPrivate::toStream(std::ostream& os) const
+{
os << "Error during type checking: " << d_msg << std::endl << *d_node << endl << "The ill-typed expression: " << *d_node;
}
-NodeTemplate<true> TypeCheckingExceptionPrivate::getNode() const throw() {
+NodeTemplate<true> TypeCheckingExceptionPrivate::getNode() const
+{
return *d_node;
}
-UnknownTypeException::UnknownTypeException(TNode n) throw() :
- TypeCheckingExceptionPrivate(n, "this expression contains an element of unknown type (such as an abstract value);"
- " its type cannot be computed until it is substituted away") {
+UnknownTypeException::UnknownTypeException(TNode n)
+ : TypeCheckingExceptionPrivate(
+ n,
+ "this expression contains an element of unknown type (such as an "
+ "abstract value);"
+ " its type cannot be computed until it is substituted away")
+{
}
/** Is this node constant? (and has that been computed yet?) */
* thrown by node.getType().
*/
class TypeCheckingExceptionPrivate : public Exception {
-
-private:
-
+ private:
/** The node responsible for the failure */
NodeTemplate<true>* d_node;
-public:
-
+ public:
/**
* Construct the exception with the problematic node and the message
* @param node the problematic node
* @param message the message explaining the failure
*/
- TypeCheckingExceptionPrivate(NodeTemplate<false> node, std::string message) throw();
+ TypeCheckingExceptionPrivate(NodeTemplate<false> node, std::string message);
/** Destructor */
- ~TypeCheckingExceptionPrivate() throw ();
+ ~TypeCheckingExceptionPrivate() override;
/**
* Get the Node that caused the type-checking to fail.
* @return the node
*/
- NodeTemplate<true> getNode() const throw();
+ NodeTemplate<true> getNode() const;
/**
* Returns the message corresponding to the type-checking failure.
* We prefer toStream() to toString() because that keeps the expr-depth
* and expr-language settings present in the stream.
*/
- void toStream(std::ostream& out) const throw();
+ void toStream(std::ostream& out) const override;
};/* class TypeCheckingExceptionPrivate */
class UnknownTypeException : public TypeCheckingExceptionPrivate {
-public:
-
- UnknownTypeException(NodeTemplate<false> node) throw();
-
+ public:
+ UnknownTypeException(NodeTemplate<false> node);
};/* class UnknownTypeException */
/**
* class, below) should be used instead.
*/
class CVC4_PUBLIC OptionException : public CVC4::Exception {
-public:
- OptionException(const std::string& s) throw() :
- CVC4::Exception("Error in option parsing: " + s) {
+ public:
+ OptionException(const std::string& s)
+ : CVC4::Exception("Error in option parsing: " + s)
+ {
}
};/* class OptionException */
* unrecognized or unsupported option key.
*/
class CVC4_PUBLIC UnrecognizedOptionException : public CVC4::OptionException {
-public:
+ public:
UnrecognizedOptionException() :
CVC4::OptionException("Unrecognized informational or option key or setting") {
}
namespace parser {
class CVC4_PUBLIC ParserException : public Exception {
-public:
+ public:
// Constructors
- ParserException() throw() :
- d_filename(),
- d_line(0),
- d_column(0) {
- }
+ ParserException() : d_filename(), d_line(0), d_column(0) {}
- ParserException(const std::string& msg) throw() :
- Exception(msg),
- d_filename(),
- d_line(0),
- d_column(0) {
+ ParserException(const std::string& msg)
+ : Exception(msg), d_filename(), d_line(0), d_column(0)
+ {
}
- ParserException(const char* msg) throw() :
- Exception(msg),
- d_filename(),
- d_line(0),
- d_column(0) {
+ ParserException(const char* msg)
+ : Exception(msg), d_filename(), d_line(0), d_column(0)
+ {
}
- ParserException(const std::string& msg, const std::string& filename,
- unsigned long line, unsigned long column) throw() :
- Exception(msg),
- d_filename(filename),
- d_line(line),
- d_column(column) {
+ ParserException(const std::string& msg,
+ const std::string& filename,
+ unsigned long line,
+ unsigned long column)
+ : Exception(msg), d_filename(filename), d_line(line), d_column(column)
+ {
}
// Destructor
- virtual ~ParserException() throw() {}
+ ~ParserException() override {}
- virtual void toStream(std::ostream& os) const throw() {
+ void toStream(std::ostream& os) const override
+ {
if( d_line > 0 ) {
os << "Parse Error: " << d_filename << ":" << d_line << "."
<< d_column << ": " << d_msg;
}
}
- std::string getFilename() const throw() {
- return d_filename;
- }
+ std::string getFilename() const { return d_filename; }
- int getLine() const throw() {
- return d_line;
- }
+ int getLine() const { return d_line; }
- int getColumn() const throw() {
- return d_column;
- }
+ int getColumn() const { return d_column; }
-protected:
+ protected:
std::string d_filename;
unsigned long d_line;
unsigned long d_column;
};/* class ParserException */
class CVC4_PUBLIC ParserEndOfFileException : public ParserException {
-public:
-
+ public:
// Constructors same as ParserException's
- ParserEndOfFileException() throw() :
- ParserException() {
- }
+ ParserEndOfFileException() : ParserException() {}
- ParserEndOfFileException(const std::string& msg) throw() :
- ParserException(msg) {
- }
+ ParserEndOfFileException(const std::string& msg) : ParserException(msg) {}
- ParserEndOfFileException(const char* msg) throw() :
- ParserException(msg) {
- }
+ ParserEndOfFileException(const char* msg) : ParserException(msg) {}
- ParserEndOfFileException(const std::string& msg, const std::string& filename,
- unsigned long line, unsigned long column) throw() :
- ParserException(msg, filename, line, column) {
+ ParserEndOfFileException(const std::string& msg,
+ const std::string& filename,
+ unsigned long line,
+ unsigned long column)
+ : ParserException(msg, filename, line, column)
+ {
}
};/* class ParserEndOfFileException */
namespace CVC4 {
class CVC4_PUBLIC LogicException : public CVC4::Exception {
-public:
+ public:
LogicException() :
Exception("Feature used while operating in "
"incorrect state") {
}
}
-
-DeltaRationalException::DeltaRationalException(const char* op, const DeltaRational& a, const DeltaRational& b) throw (){
- std::stringstream ss;
- ss << "Operation [" << op << "] between DeltaRational values ";
- ss << a << " and " << b << " is not a DeltaRational.";
- setMessage(ss.str());
+DeltaRationalException::DeltaRationalException(const char* op,
+ const DeltaRational& a,
+ const DeltaRational& b)
+{
+ std::stringstream ss;
+ ss << "Operation [" << op << "] between DeltaRational values ";
+ ss << a << " and " << b << " is not a DeltaRational.";
+ setMessage(ss.str());
}
-DeltaRationalException::~DeltaRationalException() throw () { }
-
+DeltaRationalException::~DeltaRationalException() {}
Integer DeltaRational::euclidianDivideQuotient(const DeltaRational& y) const throw(DeltaRationalException){
if(isIntegral() && y.isIntegral()){
class DeltaRational;
class DeltaRationalException : public Exception {
-public:
- DeltaRationalException(const char* op, const DeltaRational& a, const DeltaRational& b) throw ();
- virtual ~DeltaRationalException() throw ();
+ public:
+ DeltaRationalException(const char* op,
+ const DeltaRational& a,
+ const DeltaRational& b);
+ ~DeltaRationalException() override;
};
d_congruenceManager.setMasterEqualityEngine(eq);
}
-TheoryArithPrivate::ModelException::ModelException(TNode n, const char* msg) throw (){
+TheoryArithPrivate::ModelException::ModelException(TNode n, const char* msg)
+{
stringstream ss;
ss << "Cannot construct a model for " << n << " as " << endl << msg;
setMessage(ss.str());
}
-TheoryArithPrivate::ModelException::~ModelException() throw (){ }
-
+TheoryArithPrivate::ModelException::~ModelException() {}
TheoryArithPrivate::Statistics::Statistics()
: d_statAssertUpperConflicts("theory::arith::AssertUpperConflicts", 0)
bool replayLog(ApproximateSimplex* approx);
class ModelException : public Exception {
- public:
- ModelException(TNode n, const char* msg) throw ();
- virtual ~ModelException() throw ();
+ public:
+ ModelException(TNode n, const char* msg);
+ ~ModelException() override;
};
/**
class NoMoreValuesException : public Exception {
public:
- NoMoreValuesException(TypeNode n) throw() :
- Exception("No more values for type `" + n.toString() + "'") {
+ NoMoreValuesException(TypeNode n)
+ : Exception("No more values for type `" + n.toString() + "'")
+ {
}
};/* class NoMoreValuesException */
}catch(cln::floating_point_overflow_exception& fpoe){
return Maybe<Rational>();
}
- Unreachable();
}
} /* namespace CVC4 */
/**
* Constructs a Rational from a C string in a given base (defaults to 10).
+ *
* Throws std::invalid_argument if the string is not a valid rational.
* For more information about what is a valid rational string,
* see GMP's documentation for mpq_set_str().
projects / cvc5.git / commitdiff