Removing miscellaneous throw specifiers. (#1474)

15 files changed, 80 insertions, 82 deletions

diff --git a/src/cvc4.i b/src/cvc4.i
index 58dceb6b1..2f7205b19 100644
--- a/src/cvc4.i
+++ b/src/cvc4.i
@@ -3,6 +3,7 @@
 #if SWIG_VERSION < 0x030000
 %define final %enddef
 %define override %enddef
+%define noexcept %enddef
 #endif
 
 %import "bindings/swig.h"
diff --git a/src/decision/justification_heuristic.cpp b/src/decision/justification_heuristic.cpp
index a60f2c365..aae802490 100644
--- a/src/decision/justification_heuristic.cpp
+++ b/src/decision/justification_heuristic.cpp
@@ -55,7 +55,8 @@ JustificationHeuristic::JustificationHeuristic(CVC4::DecisionEngine* de,
   Trace("decision") << "Justification heuristic enabled" << std::endl;
 }
 
-JustificationHeuristic::~JustificationHeuristic() throw() {
+JustificationHeuristic::~JustificationHeuristic()
+{
   smtStatisticsRegistry()->unregisterStat(&d_helfulness);
   smtStatisticsRegistry()->unregisterStat(&d_giveup);
   smtStatisticsRegistry()->unregisterStat(&d_timestat);
diff --git a/src/decision/justification_heuristic.h b/src/decision/justification_heuristic.h
index 70fecb871..210ab4d5c 100644
--- a/src/decision/justification_heuristic.h
+++ b/src/decision/justification_heuristic.h
@@ -115,7 +115,7 @@ public:
                          context::UserContext *uc,
                          context::Context *c);
 
-  ~JustificationHeuristic() throw();
+  ~JustificationHeuristic();
 
   prop::SatLiteral getNext(bool &stopSearch);
 
diff --git a/src/expr/array_store_all.cpp b/src/expr/array_store_all.cpp
index ff026057c..65d16d9cc 100644
--- a/src/expr/array_store_all.cpp
+++ b/src/expr/array_store_all.cpp
@@ -65,33 +65,39 @@ ArrayStoreAll& ArrayStoreAll::operator=(const ArrayStoreAll& other) {
   return *this;
 }
 
-const ArrayType& ArrayStoreAll::getType() const throw() { return *d_type; }
+const ArrayType& ArrayStoreAll::getType() const { return *d_type; }
 
-const Expr& ArrayStoreAll::getExpr() const throw() { return *d_expr; }
+const Expr& ArrayStoreAll::getExpr() const { return *d_expr; }
 
-bool ArrayStoreAll::operator==(const ArrayStoreAll& asa) const throw() {
+bool ArrayStoreAll::operator==(const ArrayStoreAll& asa) const
+{
   return getType() == asa.getType() && getExpr() == asa.getExpr();
 }
 
-bool ArrayStoreAll::operator!=(const ArrayStoreAll& asa) const throw() {
+bool ArrayStoreAll::operator!=(const ArrayStoreAll& asa) const
+{
   return !(*this == asa);
 }
 
-bool ArrayStoreAll::operator<(const ArrayStoreAll& asa) const throw() {
+bool ArrayStoreAll::operator<(const ArrayStoreAll& asa) const
+{
   return (getType() < asa.getType()) ||
          (getType() == asa.getType() && getExpr() < asa.getExpr());
 }
 
-bool ArrayStoreAll::operator<=(const ArrayStoreAll& asa) const throw() {
+bool ArrayStoreAll::operator<=(const ArrayStoreAll& asa) const
+{
   return (getType() < asa.getType()) ||
          (getType() == asa.getType() && getExpr() <= asa.getExpr());
 }
 
-bool ArrayStoreAll::operator>(const ArrayStoreAll& asa) const throw() {
+bool ArrayStoreAll::operator>(const ArrayStoreAll& asa) const
+{
   return !(*this <= asa);
 }
 
-bool ArrayStoreAll::operator>=(const ArrayStoreAll& asa) const throw() {
+bool ArrayStoreAll::operator>=(const ArrayStoreAll& asa) const
+{
   return !(*this < asa);
 }
 
diff --git a/src/expr/array_store_all.h b/src/expr/array_store_all.h
index 308794f48..6b265d740 100644
--- a/src/expr/array_store_all.h
+++ b/src/expr/array_store_all.h
@@ -40,20 +40,20 @@ class CVC4_PUBLIC ArrayStoreAll {
    * not a constant of type `type`.
    */
   ArrayStoreAll(const ArrayType& type, const Expr& expr);
-  ~ArrayStoreAll() throw();
+  ~ArrayStoreAll();
 
   ArrayStoreAll(const ArrayStoreAll& other);
   ArrayStoreAll& operator=(const ArrayStoreAll& other);
 
-  const ArrayType& getType() const throw();
-  const Expr& getExpr() const throw();
+  const ArrayType& getType() const;
+  const Expr& getExpr() const;
 
-  bool operator==(const ArrayStoreAll& asa) const throw();
-  bool operator!=(const ArrayStoreAll& asa) const throw();
-  bool operator<(const ArrayStoreAll& asa) const throw();
-  bool operator<=(const ArrayStoreAll& asa) const throw();
-  bool operator>(const ArrayStoreAll& asa) const throw();
-  bool operator>=(const ArrayStoreAll& asa) const throw();
+  bool operator==(const ArrayStoreAll& asa) const;
+  bool operator!=(const ArrayStoreAll& asa) const;
+  bool operator<(const ArrayStoreAll& asa) const;
+  bool operator<=(const ArrayStoreAll& asa) const;
+  bool operator>(const ArrayStoreAll& asa) const;
+  bool operator>=(const ArrayStoreAll& asa) const;
 
  private:
   std::unique_ptr<ArrayType> d_type;
diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp
index d6249d6fd..bc4205217 100644
--- a/src/expr/expr_manager_template.cpp
+++ b/src/expr/expr_manager_template.cpp
@@ -93,7 +93,8 @@ ExprManager::ExprManager(const Options& options) :
 #endif
 }
 
-ExprManager::~ExprManager() throw() {
+ExprManager::~ExprManager()
+{
   NodeManagerScope nms(d_nodeManager);
 
   try {
@@ -128,7 +129,8 @@ const Options& ExprManager::getOptions() const {
   return d_nodeManager->getOptions();
 }
 
-ResourceManager* ExprManager::getResourceManager() throw() {
+ResourceManager* ExprManager::getResourceManager()
+{
   return d_nodeManager->getResourceManager();
 }
 
diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h
index a12c68791..35a3b6a6e 100644
--- a/src/expr/expr_manager_template.h
+++ b/src/expr/expr_manager_template.h
@@ -109,13 +109,13 @@ public:
    * any expression references that used to be managed by this expression
    * manager and are left-over are bad.
    */
-  ~ExprManager() throw();
+  ~ExprManager();
 
   /** Get this expr manager's options */
   const Options& getOptions() const;
 
   /** Get this expr manager's resource manager */
-  ResourceManager* getResourceManager() throw();
+  ResourceManager* getResourceManager();
 
   /** Get the type for booleans */
   BooleanType booleanType() const;
@@ -436,27 +436,6 @@ public:
   SortConstructorType mkSortConstructor(const std::string& name,
                                         size_t arity) const;
 
-  /**
-   * Make a predicate subtype type defined by the given LAMBDA
-   * expression.  A TypeCheckingException can be thrown if lambda is
-   * not a LAMBDA, or is ill-typed, or if CVC4 fails at proving that
-   * the resulting predicate subtype is inhabited.
-   */
-  // not in release 1.0
-  //Type mkPredicateSubtype(Expr lambda)
-  //  throw(TypeCheckingException);
-
-  /**
-   * Make a predicate subtype type defined by the given LAMBDA
-   * expression and whose non-emptiness is witnessed by the given
-   * witness.  A TypeCheckingException can be thrown if lambda is not
-   * a LAMBDA, or is ill-typed, or if the witness is not a witness or
-   * ill-typed.
-   */
-  // not in release 1.0
-  //Type mkPredicateSubtype(Expr lambda, Expr witness)
-  //  throw(TypeCheckingException);
-
   /** Get the type of an expression */
   Type getType(Expr e, bool check = false)
     throw(TypeCheckingException);
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index 0b1773114..d9345a5f5 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -391,10 +391,11 @@ public:
   }
 
   /** Get this node manager's resource manager */
-  ResourceManager* getResourceManager() throw() { return d_resourceManager; }
+  ResourceManager* getResourceManager() { return d_resourceManager; }
 
   /** Get this node manager's statistics registry */
-  StatisticsRegistry* getStatisticsRegistry() const throw() {
+  StatisticsRegistry* getStatisticsRegistry() const
+  {
     return d_statisticsRegistry;
   }
 
diff --git a/src/main/main.h b/src/main/main.h
index 8a5d0971e..0a5139c59 100644
--- a/src/main/main.h
+++ b/src/main/main.h
@@ -56,12 +56,13 @@ extern bool segvSpin;
 /** A pointer to the options in play */
 extern CVC4_THREAD_LOCAL Options* pOptions;
 
-/** Initialize the driver.  Sets signal handlers for SIGINT and SIGSEGV. */
-void cvc4_init() throw(Exception);
+/** Initialize the driver.  Sets signal handlers for SIGINT and SIGSEGV.
+ * This can throw a CVC4::Exception.
+ */
+void cvc4_init();
 
 /** Shutdown the driver. Frees memory for the signal handlers. */
-void cvc4_shutdown() throw();
-
+void cvc4_shutdown() noexcept;
 
 }/* CVC4::main namespace */
 }/* CVC4 namespace */
diff --git a/src/main/portfolio_util.h b/src/main/portfolio_util.h
index 5ed9a36fd..4f80f24ef 100644
--- a/src/main/portfolio_util.h
+++ b/src/main/portfolio_util.h
@@ -47,7 +47,7 @@ public:
     cnt(0)
   {}
 
-  ~PortfolioLemmaOutputChannel() throw() { }
+  ~PortfolioLemmaOutputChannel() {}
 
   void notifyNewLemma(Expr lemma);
 };/* class PortfolioLemmaOutputChannel */
@@ -65,7 +65,7 @@ public:
                              VarMap& to,
                                VarMap& from);
 
-  ~PortfolioLemmaInputChannel() throw() { }
+  ~PortfolioLemmaInputChannel() {}
 
   bool hasNewLemma();
   Expr getNewLemma();
diff --git a/src/main/util.cpp b/src/main/util.cpp
index 43c880a7f..de6b47aa5 100644
--- a/src/main/util.cpp
+++ b/src/main/util.cpp
@@ -261,7 +261,8 @@ void cvc4terminate() {
 }
 
 /** Initialize the driver.  Sets signal handlers for SIGINT and SIGSEGV. */
-void cvc4_init() throw(Exception) {
+void cvc4_init()
+{
 #ifdef CVC4_DEBUG
   LastExceptionBuffer::setCurrent(new LastExceptionBuffer());
 #endif
diff --git a/src/smt_util/boolean_simplification.cpp b/src/smt_util/boolean_simplification.cpp
index 40f96a47c..13ae93dc3 100644
--- a/src/smt_util/boolean_simplification.cpp
+++ b/src/smt_util/boolean_simplification.cpp
@@ -18,10 +18,9 @@
 
 namespace CVC4 {
 
-bool
-BooleanSimplification::push_back_associative_commute_recursive
-    (Node n, std::vector<Node>& buffer, Kind k, Kind notK, bool negateNode)
-    throw(AssertionException) {
+bool BooleanSimplification::push_back_associative_commute_recursive(
+    Node n, std::vector<Node>& buffer, Kind k, Kind notK, bool negateNode)
+{
   Node::iterator i = n.begin(), end = n.end();
   for(; i != end; ++i){
     Node child = *i;
diff --git a/src/smt_util/boolean_simplification.h b/src/smt_util/boolean_simplification.h
index 2d350c9d9..4a6764b0e 100644
--- a/src/smt_util/boolean_simplification.h
+++ b/src/smt_util/boolean_simplification.h
@@ -38,12 +38,11 @@ class BooleanSimplification {
   BooleanSimplification() CVC4_UNDEFINED;
   BooleanSimplification(const BooleanSimplification&) CVC4_UNDEFINED;
 
-  static bool push_back_associative_commute_recursive
-    (Node n, std::vector<Node>& buffer, Kind k, Kind notK, bool negateNode)
-    throw(AssertionException) CVC4_WARN_UNUSED_RESULT;
-
-public:
+  static bool push_back_associative_commute_recursive(
+      Node n, std::vector<Node>& buffer, Kind k, Kind notK, bool negateNode)
+      CVC4_WARN_UNUSED_RESULT;
 
+ public:
   /**
    * The threshold for removing duplicates.  (See removeDuplicates().)
    */
@@ -55,7 +54,7 @@ public:
    * function is a no-op.
    */
   static void removeDuplicates(std::vector<Node>& buffer)
-      throw(AssertionException) {
+  {
     if(buffer.size() < DUPLICATE_REMOVAL_THRESHOLD) {
       std::sort(buffer.begin(), buffer.end());
       std::vector<Node>::iterator new_end =
@@ -70,7 +69,8 @@ public:
    * push_back_associative_commute()), removes duplicates, and returns
    * the resulting Node.
    */
-  static Node simplifyConflict(Node andNode) throw(AssertionException) {
+  static Node simplifyConflict(Node andNode)
+  {
     AssertArgument(!andNode.isNull(), andNode);
     AssertArgument(andNode.getKind() == kind::AND, andNode);
 
@@ -94,7 +94,8 @@ public:
    * push_back_associative_commute()), removes duplicates, and returns
    * the resulting Node.
    */
-  static Node simplifyClause(Node orNode) throw(AssertionException) {
+  static Node simplifyClause(Node orNode)
+  {
     AssertArgument(!orNode.isNull(), orNode);
     AssertArgument(orNode.getKind() == kind::OR, orNode);
 
@@ -120,7 +121,8 @@ public:
    * The input doesn't actually have to be Horn, it seems, but that's
    * the common case(?), hence the name.
    */
-  static Node simplifyHornClause(Node implication) throw(AssertionException) {
+  static Node simplifyHornClause(Node implication)
+  {
     AssertArgument(implication.getKind() == kind::IMPLIES, implication);
 
     TNode left = implication[0];
@@ -151,10 +153,12 @@ public:
    * this if e.g. you're simplifying the (OR...) in (NOT (OR...)),
    * intending to make the result an AND.
    */
-  static inline void
-  push_back_associative_commute(Node n, std::vector<Node>& buffer,
-                                Kind k, Kind notK, bool negateChildren = false)
-      throw(AssertionException) {
+  static inline void push_back_associative_commute(Node n,
+                                                   std::vector<Node>& buffer,
+                                                   Kind k,
+                                                   Kind notK,
+                                                   bool negateChildren = false)
+  {
     AssertArgument(buffer.empty(), buffer);
     AssertArgument(!n.isNull(), n);
     AssertArgument(k != kind::UNDEFINED_KIND && k != kind::NULL_EXPR, k);
@@ -177,7 +181,8 @@ public:
    *
    * @param n the node to negate (cannot be the null node)
    */
-  static Node negate(TNode n) throw(AssertionException) {
+  static Node negate(TNode n)
+  {
     AssertArgument(!n.isNull(), n);
 
     bool polarity = true;
@@ -202,7 +207,8 @@ public:
    *
    * @param e the Expr to negate (cannot be the null Expr)
    */
-  static Expr negate(Expr e) throw(AssertionException) {
+  static Expr negate(Expr e)
+  {
     ExprManagerScope ems(e);
     return negate(Node::fromExpr(e)).toExpr();
   }
@@ -211,7 +217,8 @@ public:
    * Simplify an OR, AND, or IMPLIES.  This function is the identity
    * for all other kinds.
    */
-  inline static Node simplify(TNode n) throw(AssertionException) {
+  inline static Node simplify(TNode n)
+  {
     switch(n.getKind()) {
     case kind::AND:
       return simplifyConflict(n);
diff --git a/src/smt_util/lemma_input_channel.h b/src/smt_util/lemma_input_channel.h
index af2ac6442..f141111b1 100644
--- a/src/smt_util/lemma_input_channel.h
+++ b/src/smt_util/lemma_input_channel.h
@@ -26,10 +26,10 @@ namespace CVC4 {
 
 class CVC4_PUBLIC LemmaInputChannel {
 public:
-  virtual ~LemmaInputChannel() throw() { }
+ virtual ~LemmaInputChannel() {}
 
-  virtual bool hasNewLemma() = 0;
-  virtual Expr getNewLemma() = 0;
+ virtual bool hasNewLemma() = 0;
+ virtual Expr getNewLemma() = 0;
 
 };/* class LemmaOutputChannel */
 
diff --git a/src/smt_util/lemma_output_channel.h b/src/smt_util/lemma_output_channel.h
index 0e49e99cb..c03aa0d18 100644
--- a/src/smt_util/lemma_output_channel.h
+++ b/src/smt_util/lemma_output_channel.h
@@ -32,13 +32,13 @@ namespace CVC4 {
  */
 class CVC4_PUBLIC LemmaOutputChannel {
 public:
-  virtual ~LemmaOutputChannel() throw() { }
+ virtual ~LemmaOutputChannel() {}
 
-  /**
-   * Notifies this output channel that there's a new lemma.
-   * The lemma may or may not be in CNF.
-   */
-  virtual void notifyNewLemma(Expr lemma) = 0;
+ /**
+  * Notifies this output channel that there's a new lemma.
+  * The lemma may or may not be in CNF.
+  */
+ virtual void notifyNewLemma(Expr lemma) = 0;
 };/* class LemmaOutputChannel */
 
 }/* CVC4 namespace */