Removing miscellaneous throw specifiers. (#1474)

diff --git a/src/cvc4.i b/src/cvc4.i
index 58dceb6b17541bc90df516d9816ca3239143a8e9..2f7205b19e5393fee302fcc45b297335c5449ad5 100644 (file)
--- 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 a60f2c3657b3ca5da28d6b0ed39526cf33dafc4b..aae8024908952f12e881350d9ebdd0eb5312f378 100644 (file)
--- 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 70fecb871f5aa55469c7386ac0e97b61f569fc86..210ab4d5c2a1cc50a143d0a7fe6c8aadc4f7cc1a 100644 (file)
--- 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 ff026057cb84f7cab4f65b226f3a16165e85cb0d..65d16d9cc7622c7a81c36da69306202d38d00110 100644 (file)
--- 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 308794f4891fe86d711ed7f7d1215e5eae64109e..6b265d7405147e1d59dee8b5ce0d046a1364fedd 100644 (file)
--- 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 d6249d6fd4a9ae70b4e168080734444ccece198e..bc4205217b8a6e582762ba865d15d10cae342544 100644 (file)
--- 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 a12c68791e316e9cff94bec6587a3f4ff0d96ed7..35a3b6a6e60e94189c1c00dae31d1c7c7a053a1a 100644 (file)
--- 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 0b17731141c92fc181c878fb7ef672e0339e6dfb..d9345a5f52462ed1ab8abd7d6ce1bfde5fd83064 100644 (file)
--- 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 8a5d0971e2b971d1f535ac396d2aff44e5d61d26..0a5139c59ac3976a6a217ed052b625e3fe894b18 100644 (file)
--- 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 5ed9a36fde5a59de9b4f53bd6a95aecdba61d5b1..4f80f24efaf396d5e0f8889720b7a5a1e3113623 100644 (file)
--- 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 43c880a7fe1119c8939e22c1f60f85ea1a5ea040..de6b47aa588d8e761fa28cf508e3341c1cd0c8a5 100644 (file)
--- 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 40f96a47cccc0abf6ddc4538eb1d5d3f3ed15ebb..13ae93dc3d4b111bc121b379c4da7b597c4a8380 100644 (file)
--- 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 2d350c9d95bda21048a24c85d11745b16c120ca1..4a6764b0e2102ef2a583daeaa19139401e0c7818 100644 (file)
--- 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 af2ac6442f7309ddb937e2ac31f84f380b995b90..f141111b19dc2554748c35bd3ce3431ebb7d2be8 100644 (file)
--- 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 0e49e99cb7f9f0d81177e85f824f5826e68fd156..c03aa0d18d85132c443a4db81531a054a8ca1da1 100644 (file)
--- 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 */