Update cardinality in strings to unicode standard (#4402)

This updates the default cardinality in strings to match the Unicode standard, 196608.

This avoids a check-model failure from 25 benchmarks in SMT-LIB, which were related to a split due to insufficient constants being required during collectModelInfo.

This also makes a few places throw an AlwaysAssert(false) that otherwise would lead to incorrect models. These regardless should never throw, but it would be better to have an assertion failure.

1 files changed, 19 insertions, 0 deletions

diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index 9e14d6a3f..5b7c38361 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -264,6 +264,9 @@ bool TheoryStrings::collectModelInfo(TheoryModel* m)
   // assert the (relevant) portion of the equality engine to the model
   if (!m->assertEqualityEngine(&d_equalityEngine, &termSet))
   {
+    Unreachable()
+        << "TheoryStrings::collectModelInfo: failed to assert equality engine"
+        << std::endl;
     return false;
   }
 
@@ -423,6 +426,8 @@ bool TheoryStrings::collectModelInfoType(
       uint32_t currLen =
           lts_values[i].getConst<Rational>().getNumerator().toUnsignedInt();
       std::unique_ptr<SEnumLen> sel;
+      Trace("strings-model") << "Cardinality of alphabet is "
+                             << utils::getAlphabetCardinality() << std::endl;
       if (tn.isString())
       {
         sel.reset(new StringEnumLen(
@@ -474,7 +479,10 @@ bool TheoryStrings::collectModelInfoType(
                 Node spl = nm->mkNode(OR, sl, sl.negate());
                 ++(d_statistics.d_lemmasCmiSplit);
                 d_out->lemma(spl);
+                Trace("strings-lemma")
+                    << "Strings::CollectModelInfoSplit: " << spl << std::endl;
               }
+              // we added a lemma, so can return here
               return false;
             }
             c = sel->getCurrent();
@@ -491,6 +499,11 @@ bool TheoryStrings::collectModelInfoType(
         processed[eqc] = c;
         if (!m->assertEquality(eqc, c, true))
         {
+          // this should never happen due to the model soundness argument
+          // for strings
+          Unreachable()
+              << "TheoryStrings::collectModelInfoType: Inconsistent equality"
+              << std::endl;
           return false;
         }
       }
@@ -534,6 +547,12 @@ bool TheoryStrings::collectModelInfoType(
       processed[nodes[i]] = cc;
       if (!m->assertEquality(nodes[i], cc, true))
       {
+        // this should never happen due to the model soundness argument
+        // for strings
+
+        Unreachable() << "TheoryStrings::collectModelInfoType: "
+                         "Inconsistent equality (unprocessed eqc)"
+                      << std::endl;
         return false;
       }
     }