Use assertions instead of (Pretty)CheckArgument in util. (#9066)

This is in preparation for getting rid of IllegalArgumentException.
This exception was originally used for guards in the old API and is now
obsolete.

src/util/cardinality.cpp

@@ -36,36 +36,32 @@ const Cardinality Cardinality::REALS(CardinalityBeth(1));
 const Cardinality Cardinality::UNKNOWN_CARD((CardinalityUnknown()));
 
 CardinalityBeth::CardinalityBeth(const Integer& beth) : d_index(beth) {
-  PrettyCheckArgument(beth >= 0, beth,
-                      "Beth index must be a nonnegative integer, not %s.",
-                      beth.toString().c_str());
+  Assert(beth >= 0) << "Beth index must be a nonnegative integer, not "
+                    << beth.toString().c_str();
 }
 
 Cardinality::Cardinality(long card) : d_card(card) {
-  PrettyCheckArgument(card >= 0, card,
-                      "Cardinality must be a nonnegative integer, not %ld.",
-                      card);
+  Assert(card >= 0) << "Cardinality must be a nonnegative integer, not "
+                    << card;
   d_card += 1;
 }
 
 Cardinality::Cardinality(const Integer& card) : d_card(card) {
-  PrettyCheckArgument(card >= 0, card,
-                      "Cardinality must be a nonnegative integer, not %s.",
-                      card.toString().c_str());
+  Assert(card >= 0) << "Cardinality must be a nonnegative integer, not "
+                    << card.toString().c_str();
   d_card += 1;
 }
 
 Integer Cardinality::getFiniteCardinality() const {
-  PrettyCheckArgument(isFinite(), *this, "This cardinality is not finite.");
-  PrettyCheckArgument(
-      !isLargeFinite(), *this,
-      "This cardinality is finite, but too large to represent.");
+  Assert(isFinite()) << "This cardinality is not finite.";
+  Assert(!isLargeFinite())
+      << "This cardinality is finite, but too large to represent.";
   return d_card - 1;
 }
 
 Integer Cardinality::getBethNumber() const {
-  PrettyCheckArgument(!isFinite() && !isUnknown(), *this,
-                      "This cardinality is not infinite (or is unknown).");
+  Assert(!isFinite() && !isUnknown())
+      << "This cardinality is not infinite (or is unknown).";
   return -d_card - 1;
 }
 

src/util/divisible.cpp

@@ -23,7 +23,7 @@ using namespace std;
 namespace cvc5::internal {
 
 Divisible::Divisible(const Integer& n) : k(n) {
-  PrettyCheckArgument(n > 0, n, "Divisible predicate must be constructed over positive N");
+  Assert(n > 0) << "Divisible predicate must be constructed over positive N";
 }
 
 }  // namespace cvc5::internal

src/util/result.cpp

@@ -35,8 +35,8 @@ Result::Result()
 Result::Result(Status s, std::string inputName)
     : d_status(s), d_unknownExplanation(UNKNOWN_REASON), d_inputName(inputName)
 {
-  PrettyCheckArgument(s != UNKNOWN,
-                      "Must provide a reason for satisfiability being unknown");
+  Assert(s != UNKNOWN)
+      << "Must provide a reason for satisfiability being unknown";
 }
 
 Result::Result(Status s,
@@ -46,8 +46,7 @@ Result::Result(Status s,
       d_unknownExplanation(unknownExplanation),
       d_inputName(inputName)
 {
-  PrettyCheckArgument(s == UNKNOWN,
-                      "improper use of unknown-result constructor");
+  Assert(s == UNKNOWN) << "improper use of unknown-result constructor";
 }
 
 Result::Result(const std::string& instr, std::string inputName)
@@ -105,9 +104,8 @@ Result::Result(const std::string& instr, std::string inputName)
 
 UnknownExplanation Result::getUnknownExplanation() const
 {
-  PrettyCheckArgument(isUnknown(), this,
-                      "This result is not unknown, so the reason for "
-                      "being unknown cannot be inquired of it");
+  Assert(isUnknown()) << "This result is not unknown, so the reason for "
+                         "being unknown cannot be inquired of it";
   return d_unknownExplanation;
 }
 

src/util/uninterpreted_sort_value.cpp

@@ -35,15 +35,12 @@ UninterpretedSortValue::UninterpretedSortValue(const TypeNode& type,
                                                const Integer& index)
     : d_type(new TypeNode(type)), d_index(index)
 {
-  PrettyCheckArgument(type.isUninterpretedSort(),
-                      type,
-                      "uninterpreted constants can only be created for "
-                      "uninterpreted sorts, not `%s'",
-                      type.toString().c_str());
-  PrettyCheckArgument(index >= 0,
-                      index,
-                      "index >= 0 required for abstract value, not `%s'",
-                      index.toString().c_str());
+  Assert(type.isUninterpretedSort())
+      << "uninterpreted constants can only be created for "
+         "uninterpreted sorts, not `"
+      << type.toString().c_str() << "'";
+  Assert(index >= 0) << "index >= 0 required for abstract value, not `"
+                     << index.toString().c_str() << "'";
 }
 
 UninterpretedSortValue::UninterpretedSortValue(

test/unit/util/cardinality_black.cpp

@@ -37,10 +37,10 @@ TEST_F(TestUtilBlackCardinality, cardinalities)
   Cardinality two(2);
 
   Cardinality invalid(0);
-  ASSERT_THROW(invalid = Cardinality(-1), IllegalArgumentException);
-  ASSERT_THROW(invalid = Cardinality(-2), IllegalArgumentException);
-  ASSERT_THROW(invalid = Cardinality(Integer("-3983982192391747295721957")),
-               IllegalArgumentException);
+  ASSERT_DEATH(invalid = Cardinality(-1), "card >= 0");
+  ASSERT_DEATH(invalid = Cardinality(-2), "card >= 0");
+  ASSERT_DEATH(invalid = Cardinality(Integer("-3983982192391747295721957")),
+               "card >= 0");
   invalid = one;             // test assignment
   invalid = Cardinality(5);  // test assignment to temporary
 
@@ -125,16 +125,16 @@ TEST_F(TestUtilBlackCardinality, cardinalities)
   ASSERT_EQ(two.getFiniteCardinality(), 2);
   ASSERT_EQ(copy.getFiniteCardinality(), 1);
   ASSERT_EQ(invalid.getFiniteCardinality(), 5);
-  ASSERT_THROW(big.getFiniteCardinality(), IllegalArgumentException);
-  ASSERT_THROW(i.getFiniteCardinality(), IllegalArgumentException);
-  ASSERT_THROW(r.getFiniteCardinality(), IllegalArgumentException);
+  ASSERT_DEATH(big.getFiniteCardinality(), "!isLargeFinite\\(\\)");
+  ASSERT_DEATH(i.getFiniteCardinality(), "getFiniteCardinality\\(\\)");
+  ASSERT_DEATH(r.getFiniteCardinality(), "isFinite\\(\\)");
 
-  ASSERT_THROW(zero.getBethNumber(), IllegalArgumentException);
-  ASSERT_THROW(one.getBethNumber(), IllegalArgumentException);
-  ASSERT_THROW(two.getBethNumber(), IllegalArgumentException);
-  ASSERT_THROW(copy.getBethNumber(), IllegalArgumentException);
-  ASSERT_THROW(invalid.getBethNumber(), IllegalArgumentException);
-  ASSERT_THROW(big.getBethNumber(), IllegalArgumentException);
+  ASSERT_DEATH(zero.getBethNumber(), "!isFinite\\(\\) && !isUnknown\\(\\)");
+  ASSERT_DEATH(one.getBethNumber(), "!isFinite\\(\\) && !isUnknown\\(\\)");
+  ASSERT_DEATH(two.getBethNumber(), "!isFinite\\(\\) && !isUnknown\\(\\)");
+  ASSERT_DEATH(copy.getBethNumber(), "!isFinite\\(\\) && !isUnknown\\(\\)");
+  ASSERT_DEATH(invalid.getBethNumber(), "!isFinite\\(\\) && !isUnknown\\(\\)");
+  ASSERT_DEATH(big.getBethNumber(), "!isFinite\\(\\) && !isUnknown\\(\\)");
   ASSERT_TRUE(i.getBethNumber() == 0);
   ASSERT_TRUE(r.getBethNumber() == 1);
 
@@ -218,7 +218,7 @@ TEST_F(TestUtilBlackCardinality, cardinalities)
   ASSERT_EQ(x.compare(y), Cardinality::LESS);
   ASSERT_EQ(y.compare(z), Cardinality::LESS);
 
-  ASSERT_THROW(big.getBethNumber(), IllegalArgumentException);
+  ASSERT_DEATH(big.getBethNumber(), "!isFinite\\(\\) && !isUnknown\\(\\)");
   ASSERT_EQ(x.getBethNumber(), 0);
   ASSERT_EQ(y.getBethNumber(), 1);
   ASSERT_EQ(z.getBethNumber(), 2);