New C++ API: Add missing catch blocks for std::invalid_argument. (#2772)

diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp
index dbbb4b535fd5eed6bc4b756a0279462d7a09b305..d9a395d156dd07fd11b505b4368b177eec9e4be4 100644 (file)
--- a/src/api/cvc4cpp.cpp
+++ b/src/api/cvc4cpp.cpp
@@ -1037,7 +1037,7 @@ Term Term::notTerm() const
   {
     return d_expr->notExpr();
   }
-  catch (TypeCheckingException& e)
+  catch (const CVC4::TypeCheckingException& e)
   {
     throw CVC4ApiException(e.getMessage());
   }
@@ -1049,7 +1049,7 @@ Term Term::andTerm(const Term& t) const
   {
     return d_expr->andExpr(*t.d_expr);
   }
-  catch (TypeCheckingException& e)
+  catch (const CVC4::TypeCheckingException& e)
   {
     throw CVC4ApiException(e.getMessage());
   }
@@ -1061,7 +1061,7 @@ Term Term::orTerm(const Term& t) const
   {
     return d_expr->orExpr(*t.d_expr);
   }
-  catch (TypeCheckingException& e)
+  catch (const CVC4::TypeCheckingException& e)
   {
     throw CVC4ApiException(e.getMessage());
   }
@@ -1073,7 +1073,7 @@ Term Term::xorTerm(const Term& t) const
   {
     return d_expr->xorExpr(*t.d_expr);
   }
-  catch (TypeCheckingException& e)
+  catch (const CVC4::TypeCheckingException& e)
   {
     throw CVC4ApiException(e.getMessage());
   }
@@ -1085,7 +1085,7 @@ Term Term::eqTerm(const Term& t) const
   {
     return d_expr->eqExpr(*t.d_expr);
   }
-  catch (TypeCheckingException& e)
+  catch (const CVC4::TypeCheckingException& e)
   {
     throw CVC4ApiException(e.getMessage());
   }
@@ -1097,7 +1097,7 @@ Term Term::impTerm(const Term& t) const
   {
     return d_expr->impExpr(*t.d_expr);
   }
-  catch (TypeCheckingException& e)
+  catch (const CVC4::TypeCheckingException& e)
   {
     throw CVC4ApiException(e.getMessage());
   }
@@ -1109,7 +1109,7 @@ Term Term::iteTerm(const Term& then_t, const Term& else_t) const
   {
     return d_expr->iteExpr(*then_t.d_expr, *else_t.d_expr);
   }
-  catch (TypeCheckingException& e)
+  catch (const CVC4::TypeCheckingException& e)
   {
     throw CVC4ApiException(e.getMessage());
   }
@@ -1926,7 +1926,17 @@ Term Solver::mkBoolean(bool val) const { return d_exprMgr->mkConst<bool>(val); }
 
 Term Solver::mkPi() const
 {
-  return d_exprMgr->mkNullaryOperator(d_exprMgr->realType(), CVC4::kind::PI);
+  try
+  {
+    Term res =
+        d_exprMgr->mkNullaryOperator(d_exprMgr->realType(), CVC4::kind::PI);
+    (void)res.d_expr->getType(true); /* kick off type checking */
+    return res;
+  }
+  catch (const CVC4::TypeCheckingException& e)
+  {
+    throw CVC4ApiException(e.getMessage());
+  }
 }
 
 template <typename T>
@@ -1938,7 +1948,7 @@ Term Solver::mkConstHelper(T t) const
     (void)res.d_expr->getType(true); /* kick off type checking */
     return res;
   }
-  catch (CVC4::TypeCheckingException& e)
+  catch (const CVC4::TypeCheckingException& e)
   {
     throw CVC4ApiException(e.getMessage());
   }
@@ -1947,19 +1957,19 @@ Term Solver::mkConstHelper(T t) const
 /* Split out to avoid nested API calls (problematic with API tracing). */
 Term Solver::mkRealFromStrHelper(std::string s) const
 {
+  /* CLN and GMP handle this case differently, CLN interprets it as 0, GMP
+   * throws an std::invalid_argument exception. For consistency, we treat it
+   * as invalid. */
+  CVC4_API_ARG_CHECK_EXPECTED(s != ".", s)
+      << "a string representing an integer, real or rational value.";
   try
   {
-    /* CLN and GMP handle this case differently, CLN interprets it as 0, GMP
-     * throws an std::invalid_argument exception. For consistency, we treat it
-     * as invalid. */
-    CVC4_API_ARG_CHECK_EXPECTED(s != ".", s)
-        << "a string representing an integer, real or rational value.";
     CVC4::Rational r = s.find('/') != std::string::npos
                            ? CVC4::Rational(s)
                            : CVC4::Rational::fromDecimal(s);
     return mkConstHelper<CVC4::Rational>(r);
   }
-  catch (std::invalid_argument& e)
+  catch (const std::invalid_argument& e)
   {
     throw CVC4ApiException(e.what());
   }
@@ -1978,42 +1988,98 @@ Term Solver::mkReal(const std::string& s) const
 
 Term Solver::mkReal(int32_t val) const
 {
-  return mkConstHelper<CVC4::Rational>(CVC4::Rational(val));
+  try
+  {
+    return mkConstHelper<CVC4::Rational>(CVC4::Rational(val));
+  }
+  catch (const std::invalid_argument& e)
+  {
+    throw CVC4ApiException(e.what());
+  }
 }
 
 Term Solver::mkReal(int64_t val) const
 {
-  return mkConstHelper<CVC4::Rational>(CVC4::Rational(val));
+  try
+  {
+    return mkConstHelper<CVC4::Rational>(CVC4::Rational(val));
+  }
+  catch (const std::invalid_argument& e)
+  {
+    throw CVC4ApiException(e.what());
+  }
 }
 
 Term Solver::mkReal(uint32_t val) const
 {
-  return mkConstHelper<CVC4::Rational>(CVC4::Rational(val));
+  try
+  {
+    return mkConstHelper<CVC4::Rational>(CVC4::Rational(val));
+  }
+  catch (const std::invalid_argument& e)
+  {
+    throw CVC4ApiException(e.what());
+  }
 }
 
 Term Solver::mkReal(uint64_t val) const
 {
-  return mkConstHelper<CVC4::Rational>(CVC4::Rational(val));
+  try
+  {
+    return mkConstHelper<CVC4::Rational>(CVC4::Rational(val));
+  }
+  catch (const std::invalid_argument& e)
+  {
+    throw CVC4ApiException(e.what());
+  }
 }
 
 Term Solver::mkReal(int32_t num, int32_t den) const
 {
-  return mkConstHelper<CVC4::Rational>(CVC4::Rational(num, den));
+  try
+  {
+    return mkConstHelper<CVC4::Rational>(CVC4::Rational(num, den));
+  }
+  catch (const std::invalid_argument& e)
+  {
+    throw CVC4ApiException(e.what());
+  }
 }
 
 Term Solver::mkReal(int64_t num, int64_t den) const
 {
-  return mkConstHelper<CVC4::Rational>(CVC4::Rational(num, den));
+  try
+  {
+    return mkConstHelper<CVC4::Rational>(CVC4::Rational(num, den));
+  }
+  catch (const std::invalid_argument& e)
+  {
+    throw CVC4ApiException(e.what());
+  }
 }
 
 Term Solver::mkReal(uint32_t num, uint32_t den) const
 {
-  return mkConstHelper<CVC4::Rational>(CVC4::Rational(num, den));
+  try
+  {
+    return mkConstHelper<CVC4::Rational>(CVC4::Rational(num, den));
+  }
+  catch (const std::invalid_argument& e)
+  {
+    throw CVC4ApiException(e.what());
+  }
 }
 
 Term Solver::mkReal(uint64_t num, uint64_t den) const
 {
-  return mkConstHelper<CVC4::Rational>(CVC4::Rational(num, den));
+  try
+  {
+    return mkConstHelper<CVC4::Rational>(CVC4::Rational(num, den));
+  }
+  catch (const std::invalid_argument& e)
+  {
+    throw CVC4ApiException(e.what());
+  }
 }
 
 Term Solver::mkRegexpEmpty() const
@@ -2025,7 +2091,7 @@ Term Solver::mkRegexpEmpty() const
     (void)res.d_expr->getType(true); /* kick off type checking */
     return res;
   }
-  catch (TypeCheckingException& e)
+  catch (const CVC4::TypeCheckingException& e)
   {
     throw CVC4ApiException(e.getMessage());
   }
@@ -2040,7 +2106,7 @@ Term Solver::mkRegexpSigma() const
     (void)res.d_expr->getType(true); /* kick off type checking */
     return res;
   }
-  catch (TypeCheckingException& e)
+  catch (const CVC4::TypeCheckingException& e)
   {
     throw CVC4ApiException(e.getMessage());
   }
@@ -2062,7 +2128,7 @@ Term Solver::mkSepNil(Sort sort) const
     (void)res.d_expr->getType(true); /* kick off type checking */
     return res;
   }
-  catch (TypeCheckingException& e)
+  catch (const CVC4::TypeCheckingException& e)
   {
     throw CVC4ApiException(e.getMessage());
   }
@@ -2099,7 +2165,7 @@ Term Solver::mkUniverseSet(Sort sort) const
     // (void)res.d_expr->getType(true); /* kick off type checking */
     return res;
   }
-  catch (TypeCheckingException& e)
+  catch (const CVC4::TypeCheckingException& e)
   {
     throw CVC4ApiException(e.getMessage());
   }
@@ -2109,7 +2175,14 @@ Term Solver::mkUniverseSet(Sort sort) const
 Term Solver::mkBVFromIntHelper(uint32_t size, uint64_t val) const
 {
   CVC4_API_ARG_CHECK_EXPECTED(size > 0, size) << "a bit-width > 0";
-  return mkConstHelper<CVC4::BitVector>(CVC4::BitVector(size, val));
+  try
+  {
+    return mkConstHelper<CVC4::BitVector>(CVC4::BitVector(size, val));
+  }
+  catch (const std::invalid_argument& e)
+  {
+    throw CVC4ApiException(e.what());
+  }
 }
 
 Term Solver::mkBitVector(uint32_t size, uint64_t val) const
@@ -2120,14 +2193,14 @@ Term Solver::mkBitVector(uint32_t size, uint64_t val) const
 /* Split out to avoid nested API calls (problematic with API tracing). */
 Term Solver::mkBVFromStrHelper(std::string s, uint32_t base) const
 {
+  CVC4_API_ARG_CHECK_EXPECTED(!s.empty(), s) << "a non-empty string";
+  CVC4_API_ARG_CHECK_EXPECTED(base == 2 || base == 10 || base == 16, s)
+      << "base 2, 10, or 16";
   try
   {
-    CVC4_API_ARG_CHECK_EXPECTED(!s.empty(), s) << "a non-empty string";
-    CVC4_API_ARG_CHECK_EXPECTED(base == 2 || base == 10 || base == 16, s)
-        << "base 2, 10, or 16";
     return mkConstHelper<CVC4::BitVector>(CVC4::BitVector(s, base));
   }
-  catch (std::invalid_argument& e)
+  catch (const std::invalid_argument& e)
   {
     throw CVC4ApiException(e.what());
   }
@@ -2137,19 +2210,18 @@ Term Solver::mkBVFromStrHelper(uint32_t size,
                                std::string s,
                                uint32_t base) const
 {
+  CVC4_API_ARG_CHECK_EXPECTED(!s.empty(), s) << "a non-empty string";
+  CVC4_API_ARG_CHECK_EXPECTED(base == 2 || base == 10 || base == 16, s)
+      << "base 2, 10, or 16";
   try
   {
-    CVC4_API_ARG_CHECK_EXPECTED(!s.empty(), s) << "a non-empty string";
-    CVC4_API_ARG_CHECK_EXPECTED(base == 2 || base == 10 || base == 16, s)
-        << "base 2, 10, or 16";
-
     Integer val(s, base);
     CVC4_API_CHECK(val.modByPow2(size) == val)
         << "Overflow in bitvector construction (specified bitvector size "
         << size << " too small to hold value " << s << ")";
     return mkConstHelper<CVC4::BitVector>(CVC4::BitVector(size, val));
   }
-  catch (std::invalid_argument& e)
+  catch (const std::invalid_argument& e)
   {
     throw CVC4ApiException(e.what());
   }
@@ -2219,14 +2291,7 @@ Term Solver::mkNegZero(uint32_t exp, uint32_t sig) const
 
 Term Solver::mkConst(RoundingMode rm) const
 {
-  try
-  {
-    return mkConstHelper<CVC4::RoundingMode>(s_rmodes.at(rm));
-  }
-  catch (std::invalid_argument& e)
-  {
-    throw CVC4ApiException(e.what());
-  }
+  return mkConstHelper<CVC4::RoundingMode>(s_rmodes.at(rm));
 }
 
 Term Solver::mkConst(Kind kind, Sort arg) const
@@ -2249,7 +2314,7 @@ Term Solver::mkConst(Kind kind, Sort arg) const
       return res;
     }
   }
-  catch (TypeCheckingException& e)
+  catch (const CVC4::TypeCheckingException& e)
   {
     throw CVC4ApiException(e.getMessage());
   }
@@ -2286,11 +2351,11 @@ Term Solver::mkConstFromStrHelper(Kind kind, std::string s) const
       // do not call getType(), for abstract values, type can not be computed
       // until it is substituted away
     }
-    catch (std::invalid_argument& e)
+    catch (const std::invalid_argument& e)
     {
       throw CVC4ApiException(e.what());
     }
-    catch (TypeCheckingException& e)
+    catch (const CVC4::TypeCheckingException& e)
     {
       throw CVC4ApiException(e.getMessage());
     }
@@ -2348,12 +2413,23 @@ Term Solver::mkConstFromIntHelper(Kind kind, T a) const
       // do not call getType(), for abstract values, type can not be computed
       // until it is substituted away
     }
-    catch (TypeCheckingException& e)
+    catch (const std::invalid_argument& e)
+    {
+      throw CVC4ApiException(e.what());
+    }
+    catch (const CVC4::TypeCheckingException& e)
     {
       throw CVC4ApiException(e.getMessage());
     }
   }
-  return mkConstHelper<CVC4::Rational>(CVC4::Rational(a));
+  try
+  {
+    return mkConstHelper<CVC4::Rational>(CVC4::Rational(a));
+  }
+  catch (const std::invalid_argument& e)
+  {
+    throw CVC4ApiException(e.what());
+  }
 }
 
 Term Solver::mkConst(Kind kind, int32_t arg) const
@@ -2385,28 +2461,56 @@ Term Solver::mkConst(Kind kind, uint32_t arg1, uint32_t arg2) const
   {
     return mkBVFromIntHelper(arg1, arg2);
   }
-  return mkConstHelper<CVC4::Rational>(CVC4::Rational(arg1, arg2));
+  try
+  {
+    return mkConstHelper<CVC4::Rational>(CVC4::Rational(arg1, arg2));
+  }
+  catch (const std::invalid_argument& e)
+  {
+    throw CVC4ApiException(e.what());
+  }
 }
 
 Term Solver::mkConst(Kind kind, int32_t arg1, int32_t arg2) const
 {
   CVC4_API_KIND_CHECK_EXPECTED(kind == CONST_RATIONAL, kind)
       << "CONST_RATIONAL";
-  return mkConstHelper<CVC4::Rational>(CVC4::Rational(arg1, arg2));
+  try
+  {
+    return mkConstHelper<CVC4::Rational>(CVC4::Rational(arg1, arg2));
+  }
+  catch (const std::invalid_argument& e)
+  {
+    throw CVC4ApiException(e.what());
+  }
 }
 
 Term Solver::mkConst(Kind kind, int64_t arg1, int64_t arg2) const
 {
   CVC4_API_KIND_CHECK_EXPECTED(kind == CONST_RATIONAL, kind)
       << "CONST_RATIONAL";
-  return mkConstHelper<CVC4::Rational>(CVC4::Rational(arg1, arg2));
+  try
+  {
+    return mkConstHelper<CVC4::Rational>(CVC4::Rational(arg1, arg2));
+  }
+  catch (const std::invalid_argument& e)
+  {
+    throw CVC4ApiException(e.what());
+  }
 }
 
 Term Solver::mkConst(Kind kind, uint64_t arg1, uint64_t arg2) const
 {
   CVC4_API_KIND_CHECK_EXPECTED(kind == CONST_RATIONAL, kind)
       << "CONST_RATIONAL";
-  return mkConstHelper<CVC4::Rational>(CVC4::Rational(arg1, arg2));
+  try
+  {
+    return mkConstHelper<CVC4::Rational>(CVC4::Rational(arg1, arg2));
+  }
+  catch (const std::invalid_argument& e)
+  {
+    throw CVC4ApiException(e.what());
+  }
 }
 
 Term Solver::mkConst(Kind kind, uint32_t arg1, uint64_t arg2) const
@@ -2447,7 +2551,7 @@ Term Solver::mkVar(const std::string& symbol, Sort sort) const
     (void)res.d_expr->getType(true); /* kick off type checking */
     return res;
   }
-  catch (TypeCheckingException& e)
+  catch (const CVC4::TypeCheckingException& e)
   {
     throw CVC4ApiException(e.getMessage());
   }
@@ -2462,7 +2566,7 @@ Term Solver::mkVar(Sort sort) const
     (void)res.d_expr->getType(true); /* kick off type checking */
     return res;
   }
-  catch (TypeCheckingException& e)
+  catch (const CVC4::TypeCheckingException& e)
   {
     throw CVC4ApiException(e.getMessage());
   }
@@ -2477,7 +2581,7 @@ Term Solver::mkBoundVar(const std::string& symbol, Sort sort) const
     (void)res.d_expr->getType(true); /* kick off type checking */
     return res;
   }
-  catch (TypeCheckingException& e)
+  catch (const CVC4::TypeCheckingException& e)
   {
     throw CVC4ApiException(e.getMessage());
   }
@@ -2492,7 +2596,7 @@ Term Solver::mkBoundVar(Sort sort) const
     (void)res.d_expr->getType(true); /* kick off type checking */
     return res;
   }
-  catch (TypeCheckingException& e)
+  catch (const CVC4::TypeCheckingException& e)
   {
     throw CVC4ApiException(e.getMessage());
   }
@@ -2570,7 +2674,7 @@ Term Solver::mkTerm(Kind kind) const
     (void)res.d_expr->getType(true); /* kick off type checking */
     return res;
   }
-  catch (TypeCheckingException& e)
+  catch (const CVC4::TypeCheckingException& e)
   {
     throw CVC4ApiException(e.getMessage());
   }
@@ -2585,7 +2689,7 @@ Term Solver::mkTerm(Kind kind, Sort sort) const
     (void)res.d_expr->getType(true); /* kick off type checking */
     return res;
   }
-  catch (TypeCheckingException& e)
+  catch (const CVC4::TypeCheckingException& e)
   {
     throw CVC4ApiException(e.getMessage());
   }
@@ -2601,7 +2705,7 @@ Term Solver::mkTerm(Kind kind, Term child) const
     (void)res.d_expr->getType(true); /* kick off type checking */
     return res;
   }
-  catch (TypeCheckingException& e)
+  catch (const CVC4::TypeCheckingException& e)
   {
     throw CVC4ApiException(e.getMessage());
   }
@@ -2619,7 +2723,7 @@ Term Solver::mkTerm(Kind kind, Term child1, Term child2) const
     (void)res.d_expr->getType(true); /* kick off type checking */
     return res;
   }
-  catch (TypeCheckingException& e)
+  catch (const CVC4::TypeCheckingException& e)
   {
     throw CVC4ApiException(e.getMessage());
   }
@@ -2641,7 +2745,7 @@ Term Solver::mkTerm(Kind kind, Term child1, Term child2, Term child3) const
     (void)res.d_expr->getType(true); /* kick off type checking */
     return res;
   }
-  catch (TypeCheckingException& e)
+  catch (const CVC4::TypeCheckingException& e)
   {
     throw CVC4ApiException(e.getMessage());
   }
@@ -2666,7 +2770,7 @@ Term Solver::mkTerm(Kind kind, const std::vector<Term>& children) const
     (void)res.d_expr->getType(true); /* kick off type checking */
     return res;
   }
-  catch (TypeCheckingException& e)
+  catch (const CVC4::TypeCheckingException& e)
   {
     throw CVC4ApiException(e.getMessage());
   }
@@ -2682,7 +2786,7 @@ Term Solver::mkTerm(OpTerm opTerm, Term child) const
     (void)res.d_expr->getType(true); /* kick off type checking */
     return res;
   }
-  catch (TypeCheckingException& e)
+  catch (const CVC4::TypeCheckingException& e)
   {
     throw CVC4ApiException(e.getMessage());
   }
@@ -2700,7 +2804,7 @@ Term Solver::mkTerm(OpTerm opTerm, Term child1, Term child2) const
     (void)res.d_expr->getType(true); /* kick off type checking */
     return res;
   }
-  catch (TypeCheckingException& e)
+  catch (const CVC4::TypeCheckingException& e)
   {
     throw CVC4ApiException(e.getMessage());
   }
@@ -2719,7 +2823,7 @@ Term Solver::mkTerm(OpTerm opTerm, Term child1, Term child2, Term child3) const
     (void)res.d_expr->getType(true); /* kick off type checking */
     return res;
   }
-  catch (TypeCheckingException& e)
+  catch (const CVC4::TypeCheckingException& e)
   {
     throw CVC4ApiException(e.getMessage());
   }
@@ -2741,7 +2845,7 @@ Term Solver::mkTerm(OpTerm opTerm, const std::vector<Term>& children) const
     (void)res.d_expr->getType(true); /* kick off type checking */
     return res;
   }
-  catch (TypeCheckingException& e)
+  catch (const CVC4::TypeCheckingException& e)
   {
     throw CVC4ApiException(e.getMessage());
   }