From 256d4093ab6ac3b792c6f1f11131124d1ae6b069 Mon Sep 17 00:00:00 2001
From: Tim King <taking@cs.nyu.edu>
Date: Thu, 4 Jan 2018 13:09:39 -0800
Subject: Removing miscellaneous throw specifiers. (#1474)

---
 src/smt_util/boolean_simplification.h | 39 +++++++++++++++++++++--------------
 1 file changed, 23 insertions(+), 16 deletions(-)

(limited to 'src/smt_util/boolean_simplification.h')

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);
-- 
cgit v1.2.3