From: Tim King <taking@cs.nyu.edu>
Date: Wed, 4 Oct 2017 16:26:28 +0000 (-0700)
Subject: Removing the throw specifier from ArrayStoreAll constructor. (#1182)
X-Git-Tag: cvc5-1.0.0~5580
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=f2bd626d6337ca4df70c0bf541d7d9bec4ef5be5;p=cvc5.git

Removing the throw specifier from ArrayStoreAll constructor. (#1182)

Addresses CIDS: 1457252 and 1379620.

Miscellaneous cleanup to ArrayStoreAll.
---

diff --git a/src/expr/array_store_all.cpp b/src/expr/array_store_all.cpp
index 4bad04f79..ff026057c 100644
--- a/src/expr/array_store_all.cpp
+++ b/src/expr/array_store_all.cpp
@@ -28,9 +28,8 @@ using namespace std;
 
 namespace CVC4 {
 
-ArrayStoreAll::ArrayStoreAll(const ArrayType& type,
-                             const Expr& expr) throw(IllegalArgumentException)
-    : d_type(NULL), d_expr(NULL) {
+ArrayStoreAll::ArrayStoreAll(const ArrayType& type, const Expr& expr)
+    : d_type(), d_expr() {
   // this check is stronger than the assertion check in the expr manager that
   // ArrayTypes are actually array types
   // because this check is done in production builds too
@@ -50,18 +49,15 @@ ArrayStoreAll::ArrayStoreAll(const ArrayType& type,
   // Delay allocation until the checks above have been performed. If these fail,
   // the memory for d_type and d_expr should not leak. The alternative is catch,
   // delete and re-throw.
-  d_type = new ArrayType(type);
-  d_expr = new Expr(expr);
+  d_type.reset(new ArrayType(type));
+  d_expr.reset(new Expr(expr));
 }
 
 ArrayStoreAll::ArrayStoreAll(const ArrayStoreAll& other)
     : d_type(new ArrayType(other.getType())),
       d_expr(new Expr(other.getExpr())) {}
 
-ArrayStoreAll::~ArrayStoreAll() throw() {
-  delete d_expr;
-  delete d_type;
-}
+ArrayStoreAll::~ArrayStoreAll() throw() {}
 
 ArrayStoreAll& ArrayStoreAll::operator=(const ArrayStoreAll& other) {
   (*d_type) = other.getType();
@@ -77,6 +73,10 @@ bool ArrayStoreAll::operator==(const ArrayStoreAll& asa) const throw() {
   return getType() == asa.getType() && getExpr() == asa.getExpr();
 }
 
+bool ArrayStoreAll::operator!=(const ArrayStoreAll& asa) const throw() {
+  return !(*this == asa);
+}
+
 bool ArrayStoreAll::operator<(const ArrayStoreAll& asa) const throw() {
   return (getType() < asa.getType()) ||
          (getType() == asa.getType() && getExpr() < asa.getExpr());
@@ -87,6 +87,14 @@ bool ArrayStoreAll::operator<=(const ArrayStoreAll& asa) const throw() {
          (getType() == asa.getType() && getExpr() <= asa.getExpr());
 }
 
+bool ArrayStoreAll::operator>(const ArrayStoreAll& asa) const throw() {
+  return !(*this <= asa);
+}
+
+bool ArrayStoreAll::operator>=(const ArrayStoreAll& asa) const throw() {
+  return !(*this < asa);
+}
+
 std::ostream& operator<<(std::ostream& out, const ArrayStoreAll& asa) {
   return out << "__array_store_all__(" << asa.getType() << ", " << asa.getExpr()
              << ')';
@@ -96,4 +104,4 @@ size_t ArrayStoreAllHashFunction::operator()(const ArrayStoreAll& asa) const {
   return TypeHashFunction()(asa.getType()) * ExprHashFunction()(asa.getExpr());
 }
 
-} /* CVC4 namespace */
+}  // namespace CVC4
diff --git a/src/expr/array_store_all.h b/src/expr/array_store_all.h
index c8474dfa1..308794f48 100644
--- a/src/expr/array_store_all.h
+++ b/src/expr/array_store_all.h
@@ -18,64 +18,58 @@
 
 #include "cvc4_public.h"
 
-#pragma once
+#ifndef __CVC4__ARRAY_STORE_ALL_H
+#define __CVC4__ARRAY_STORE_ALL_H
 
 #include <iosfwd>
-
-#include "base/exception.h"
+#include <memory>
 
 namespace CVC4 {
-  // messy; Expr needs ArrayStoreAll (because it's the payload of a
-  // CONSTANT-kinded expression), and ArrayStoreAll needs Expr.
-  class Expr;
-  class ArrayType;
-}/* CVC4 namespace */
-
+// messy; Expr needs ArrayStoreAll (because it's the payload of a
+// CONSTANT-kinded expression), and ArrayStoreAll needs Expr.
+class Expr;
+class ArrayType;
+}  // namespace CVC4
 
 namespace CVC4 {
 
 class CVC4_PUBLIC ArrayStoreAll {
-public:
-  ArrayStoreAll(const ArrayStoreAll& other);
+ public:
+  /**
+   * @throws IllegalArgumentException if `type` is not an array or if `expr` is
+   * not a constant of type `type`.
+   */
+  ArrayStoreAll(const ArrayType& type, const Expr& expr);
+  ~ArrayStoreAll() throw();
 
+  ArrayStoreAll(const ArrayStoreAll& other);
   ArrayStoreAll& operator=(const ArrayStoreAll& other);
 
-  ArrayStoreAll(const ArrayType& type, const Expr& expr)
-      throw(IllegalArgumentException);
-
-  ~ArrayStoreAll() throw();
-
   const ArrayType& getType() const throw();
-
   const Expr& getExpr() const throw();
 
   bool operator==(const ArrayStoreAll& asa) const throw();
-
-  bool operator!=(const ArrayStoreAll& asa) const throw() {
-    return !(*this == asa);
-  }
-
+  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() {
-    return !(*this <= asa);
-  }
-  bool operator>=(const ArrayStoreAll& asa) const throw() {
-    return !(*this < asa);
-  }
+  bool operator>(const ArrayStoreAll& asa) const throw();
+  bool operator>=(const ArrayStoreAll& asa) const throw();
 
-private:
-  ArrayType* d_type;
-  Expr* d_expr;
-};/* class ArrayStoreAll */
+ private:
+  std::unique_ptr<ArrayType> d_type;
+  std::unique_ptr<Expr> d_expr;
+}; /* class ArrayStoreAll */
 
-std::ostream& operator<<(std::ostream& out, const ArrayStoreAll& asa) CVC4_PUBLIC;
+std::ostream& operator<<(std::ostream& out,
+                         const ArrayStoreAll& asa) CVC4_PUBLIC;
 
 /**
  * Hash function for the ArrayStoreAll constants.
  */
 struct CVC4_PUBLIC ArrayStoreAllHashFunction {
   size_t operator()(const ArrayStoreAll& asa) const;
-};/* struct ArrayStoreAllHashFunction */
+}; /* struct ArrayStoreAllHashFunction */
+
+}  // namespace CVC4
 
-}/* CVC4 namespace */
+#endif /* __CVC4__ARRAY_STORE_ALL_H */