Removing miscellaneous throw specifiers. (#1474)

4 files changed, 35 insertions, 29 deletions

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 */