Changes assertion (about maximum set cardinality) to an exception. (#4907)

Changes the assertion that checks for the maximum cardinality of set models to an exception, following #4374.
Also cleans up the code around it: previously, the Rational was checked against LONG_MAX, converted to std::uint32_t and then stored into an unsigned. Now we use std::uint32_t all the way.
Fixes #4374.

diff --git a/src/theory/sets/cardinality_extension.cpp b/src/theory/sets/cardinality_extension.cpp
index 1c12c71e42b1ef22f2705a2793c7bd5f8e38ba5c..4aa866d27d50fc7c9281e45aa1ddd07cb4456bb7 100644 (file)
--- a/src/theory/sets/cardinality_extension.cpp
+++ b/src/theory/sets/cardinality_extension.cpp
@@ -997,9 +997,14 @@ void CardinalityExtension::mkModelValueElementsFor(
       Node v = val.getModelValue(it->second);
       Trace("sets-model") << "Cardinality of " << eqc << " is " << v
                           << std::endl;
-      Assert(v.getConst<Rational>() <= LONG_MAX)
-          << "Exceeded LONG_MAX in sets model";
-      unsigned vu = v.getConst<Rational>().getNumerator().toUnsignedInt();
+      if (v.getConst<Rational>() > UINT32_MAX)
+      {
+        std::stringstream ss;
+        ss << "The model for " << eqc << " was computed to have cardinality "
+           << v << ". We only allow sets up to cardinality " << UINT32_MAX;
+        throw LogicException(ss.str());
+      }
+      std::uint32_t vu = v.getConst<Rational>().getNumerator().toUnsignedInt();
       Assert(els.size() <= vu);
       NodeManager* nm = NodeManager::currentNM();
       if (elementType.isInterpretedFinite())

diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index b23765313cf497ed7c716962081d8631da9cc118..c78e8dc2aaec04f3a1bfc36f13d48eac7312c652 100644 (file)
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -312,7 +312,7 @@ bool TheoryStrings::collectModelInfoType(
   std::map< Node, Node > processed;
   //step 1 : get all values for known lengths
   std::vector< Node > lts_values;
-  std::map<unsigned, Node> values_used;
+  std::map<std::size_t, Node> values_used;
   std::vector<Node> len_splits;
   for( unsigned i=0; i<col.size(); i++ ) {
     Trace("strings-model") << "Checking length for {";
@@ -339,15 +339,16 @@ bool TheoryStrings::collectModelInfoType(
     else
     {
       // must throw logic exception if we cannot construct the string
-      if (len_value.getConst<Rational>() > Rational(String::maxSize()))
+      if (len_value.getConst<Rational>() > String::maxSize())
       {
         std::stringstream ss;
-        ss << "Cannot generate model with string whose length exceeds UINT32_MAX";
+        ss << "The model was computed to have strings of length " << len_value
+           << ". We only allow strings up to length " << String::maxSize();
         throw LogicException(ss.str());
       }
-      unsigned lvalue =
+      std::size_t lvalue =
           len_value.getConst<Rational>().getNumerator().toUnsignedInt();
-      std::map<unsigned, Node>::iterator itvu = values_used.find(lvalue);
+      auto itvu = values_used.find(lvalue);
       if (itvu == values_used.end())
       {
         values_used[lvalue] = lts[i];
@@ -417,7 +418,7 @@ bool TheoryStrings::collectModelInfoType(
     if( !pure_eq.empty() ){
       if( lts_values[i].isNull() ){
         // start with length two (other lengths have special precendence)
-        unsigned lvalue = 2;
+        std::size_t lvalue = 2;
         while( values_used.find( lvalue )!=values_used.end() ){
           lvalue++;
         }

diff --git a/test/regress/regress0/strings/large-model.smt2 b/test/regress/regress0/strings/large-model.smt2
index 74b781c82932992ba2dc05c55864377c315a8f4a..f3aa7f8f25903406c53b13acf7db922c4be4f0c3 100644 (file)
--- a/test/regress/regress0/strings/large-model.smt2
+++ b/test/regress/regress0/strings/large-model.smt2
@@ -1,5 +1,6 @@
 ; COMMAND-LINE: --lang=smt2.6 --check-models
-; EXPECT: (error "Cannot generate model with string whose length exceeds UINT32_MAX")
+; SCRUBBER: sed -E 's/of length [0-9]+/of length LENGTH/'
+; EXPECT: (error "The model was computed to have strings of length LENGTH. We only allow strings up to length 4294967295")
 ; EXIT: 1
 (set-logic SLIA)
 (declare-fun x () String)