From 8ea1603f55d940e56ab3cbee8177f06200228aaa Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Tue, 28 Apr 2020 08:07:54 -0500
Subject: [PATCH] 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.
---
 src/theory/strings/theory_strings.cpp         | 19 +++++++++++++++++++
 src/theory/strings/theory_strings_utils.cpp   |  5 +++--
 test/regress/CMakeLists.txt                   |  1 +
 .../regress2/strings/cmi-split-cm-fail.smt2   | 12 ++++++++++++
 4 files changed, 35 insertions(+), 2 deletions(-)
 create mode 100644 test/regress/regress2/strings/cmi-split-cm-fail.smt2

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;
       }
     }
diff --git a/src/theory/strings/theory_strings_utils.cpp b/src/theory/strings/theory_strings_utils.cpp
index b2a62cc62..b64a0df01 100644
--- a/src/theory/strings/theory_strings_utils.cpp
+++ b/src/theory/strings/theory_strings_utils.cpp
@@ -36,8 +36,9 @@ uint32_t getAlphabetCardinality()
     Assert(128 <= String::num_codes());
     return 128;
   }
-  Assert(256 <= String::num_codes());
-  return 256;
+  // 3*16^4 = 196608 values in the SMT-LIB standard for Unicode strings
+  Assert(196608 <= String::num_codes());
+  return 196608;
 }
 
 Node mkAnd(const std::vector<Node>& a)
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 935a4694f..656bb5880 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -2050,6 +2050,7 @@ set(regress_2_tests
   regress2/quantifiers/sygus-inst-ufbv-sdlx-fixpoint-5.smt2
   regress2/quantifiers/syn874-1.smt2
   regress2/simplify.javafe.ast.ArrayInit.35_without_quantification2.smt2
+  regress2/strings/cmi-split-cm-fail.smt2
   regress2/strings/cmu-dis-0707-3.smt2
   regress2/strings/cmu-disagree-0707-dd.smt2
   regress2/strings/cmu-prereg-fmf.smt2
diff --git a/test/regress/regress2/strings/cmi-split-cm-fail.smt2 b/test/regress/regress2/strings/cmi-split-cm-fail.smt2
new file mode 100644
index 000000000..e2ae94a27
--- /dev/null
+++ b/test/regress/regress2/strings/cmi-split-cm-fail.smt2
@@ -0,0 +1,12 @@
+; COMMAND-LINE: --strings-exp --rewrite-divk
+; EXPECT: sat
+(set-info :smt-lib-version 2.6)
+(set-logic QF_SLIA)
+(set-info :status sat)
+
+(declare-fun s () String)
+
+(assert (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (not (not (not (= (ite (not (= (str.at s 0) (str.at s 1))) 1 0) 0)))) (not (= (ite (not (= (str.at s 3) (str.at s 5))) 1 0) 0))) (not (not (= (ite (not (= (str.at s 2) (str.at s 6))) 1 0) 0)))) (not (not (= (ite (not (= (str.at s 1) (str.at s 7))) 1 0) 0)))) (not (= (ite (not (= (str.at s 2) (str.at s 5))) 1 0) 0))) (not (not (= (ite (not (= (str.at s 1) (str.at s 6))) 1 0) 0)))) (not (= (ite (not (= (str.at s 1) (str.at s 5))) 1 0) 0))) (not (= (ite (not (= (str.at s 1) (str.at s 4))) 1 0) 0))) (not (= (ite (not (= (str.at s 4) (str.at s 7))) 1 0) 0))) (not (= (ite (not (= (str.at s 4) (str.at s 6))) 1 0) 0))) (not (= (ite (<= (str.len s) 8) 1 0) 0))) (not (= (ite (= (str.len s) 8) 1 0) 0))) (not (not (= (ite (not (= (str.at s 6) (str.at s 7))) 1 0) 0)))) (not (= (ite (<= (str.len s) 8) 1 0) 0))) (not (= (ite (= (str.len s) 8) 1 0) 0))) (not (not (= (ite (<= (str.len s) 7) 1 0) 0)))) (not (not (= (ite (= (str.len s) 7) 1 0) 0)))) (not (not (= (ite (<= (str.len s) 6) 1 0) 0)))) (not (not (= (ite (= (str.len s) 6) 1 0) 0)))) (not (not (= (ite (not (= (str.at s 4) (str.at s 5))) 1 0) 0)))) (not (= (ite (not (= (str.at s 5) (str.at s 7))) 1 0) 0))) (not (= (ite (not (= (str.at s 5) (str.at s 6))) 1 0) 0))) (not (= (ite (<= (str.len s) 8) 1 0) 0))) (not (= (ite (= (str.len s) 8) 1 0) 0))) (not (not (= (ite (not (= (str.at s 6) (str.at s 7))) 1 0) 0)))) (not (= (ite (<= (str.len s) 8) 1 0) 0))) (not (= (ite (= (str.len s) 8) 1 0) 0))) (not (not (= (ite (<= (str.len s) 7) 1 0) 0)))) (not (not (= (ite (= (str.len s) 7) 1 0) 0)))) (not (not (= (ite (<= (str.len s) 6) 1 0) 0)))) (not (not (= (ite (= (str.len s) 6) 1 0) 0)))) (not (not (= (ite (<= (str.len s) 5) 1 0) 0)))) (not (not (= (ite (= (str.len s) 5) 1 0) 0)))) (not (not (= (ite (<= (str.len s) 4) 1 0) 0)))) (not (not (= (ite (= (str.len s) 4) 1 0) 0)))) (not (not (= (ite (not (= (str.at s 1) (str.at s 3))) 1 0) 0)))) (not (= (ite (not (= (str.at s 4) (str.at s 6))) 1 0) 0))) (not (not (= (ite (not (= (str.at s 3) (str.at s 7))) 1 0) 0)))) (not (= (ite (<= (str.len s) 8) 1 0) 0))) (not (= (ite (= (str.len s) 8) 1 0) 0))) (not (not (= (ite (<= (str.len s) 7) 1 0) 0)))) (not (not (= (ite (= (str.len s) 7) 1 0) 0)))) (not (not (= (ite (not (= (str.at s 4) (str.at s 5))) 1 0) 0)))) (not (not (= (ite (not (= (str.at s 3) (str.at s 6))) 1 0) 0)))) (not (= (ite (not (= (str.at s 3) (str.at s 5))) 1 0) 0))) (not (= (ite (not (= (str.at s 3) (str.at s 4))) 1 0) 0))) (not (= (ite (not (= (str.at s 4) (str.at s 7))) 1 0) 0))) (not (= (ite (not (= (str.at s 4) (str.at s 6))) 1 0) 0))) (not (= (ite (<= (str.len s) 8) 1 0) 0))) (not (= (ite (= (str.len s) 8) 1 0) 0))) (not (not (= (ite (not (= (str.at s 6) (str.at s 7))) 1 0) 0)))) (not (= (ite (<= (str.len s) 8) 1 0) 0))) (not (= (ite (= (str.len s) 8) 1 0) 0))) (not (not (= (ite (<= (str.len s) 7) 1 0) 0)))) (not (not (= (ite (= (str.len s) 7) 1 0) 0)))) (not (not (= (ite (<= (str.len s) 6) 1 0) 0)))) (not (not (= (ite (= (str.len s) 6) 1 0) 0)))) (not (not (= (ite (not (= (str.at s 4) (str.at s 5))) 1 0) 0)))) (not (= (ite (not (= (str.at s 5) (str.at s 7))) 1 0) 0))) (not (= (ite (not (= (str.at s 5) (str.at s 6))) 1 0) 0))) (not (= (ite (<= (str.len s) 8) 1 0) 0))) (not (= (ite (= (str.len s) 8) 1 0) 0))) (not (not (= (ite (not (= (str.at s 6) (str.at s 7))) 1 0) 0)))) (not (= (ite (<= (str.len s) 8) 1 0) 0))) (not (= (ite (= (str.len s) 8) 1 0) 0))) (not (not (= (ite (<= (str.len s) 7) 1 0) 0)))) (not (not (= (ite (= (str.len s) 7) 1 0) 0)))) (not (not (= (ite (<= (str.len s) 6) 1 0) 0)))) (not (not (= (ite (= (str.len s) 6) 1 0) 0)))) (not (not (= (ite (<= (str.len s) 5) 1 0) 0)))) (not (not (= (ite (= (str.len s) 5) 1 0) 0)))) (not (not (= (ite (<= (str.len s) 4) 1 0) 0)))) (not (not (= (ite (= (str.len s) 4) 1 0) 0)))) (not (not (= (ite (<= (str.len s) 3) 1 0) 0)))) (not (not (= (ite (= (str.len s) 3) 1 0) 0)))) (not (not (= (ite (not (= (str.at s 1) (str.at s 2))) 1 0) 0)))) (not (= (ite (<= (str.len s) 8) 1 0) 0))) (not (= (ite (= (str.len s) 8) 1 0) 0))) (not (not (= (ite (not (= (str.at s 4) (str.at s 5))) 1 0) 0)))) (not (not (= (ite (not (= (str.at s 3) (str.at s 6))) 1 0) 0)))) (not (not (= (ite (not (= (str.at s 2) (str.at s 7))) 1 0) 0)))) (not (= (ite (not (= (str.at s 3) (str.at s 5))) 1 0) 0))) (not (not (= (ite (not (= (str.at s 2) (str.at s 6))) 1 0) 0)))) (not (= (ite (not (= (str.at s 2) (str.at s 5))) 1 0) 0))) (not (= (ite (not (= (str.at s 2) (str.at s 4))) 1 0) 0))) (not (= (ite (not (= (str.at s 4) (str.at s 7))) 1 0) 0))) (not (= (ite (not (= (str.at s 4) (str.at s 6))) 1 0) 0))) (not (= (ite (<= (str.len s) 8) 1 0) 0))) (not (= (ite (= (str.len s) 8) 1 0) 0))) (not (not (= (ite (not (= (str.at s 6) (str.at s 7))) 1 0) 0)))) (not (= (ite (<= (str.len s) 8) 1 0) 0))) (not (= (ite (= (str.len s) 8) 1 0) 0))) (not (not (= (ite (<= (str.len s) 7) 1 0) 0)))) (not (not (= (ite (= (str.len s) 7) 1 0) 0)))) (not (not (= (ite (<= (str.len s) 6) 1 0) 0)))) (not (not (= (ite (= (str.len s) 6) 1 0) 0)))) (not (not (= (ite (not (= (str.at s 4) (str.at s 5))) 1 0) 0)))) (not (= (ite (not (= (str.at s 5) (str.at s 7))) 1 0) 0))) (not (= (ite (not (= (str.at s 5) (str.at s 6))) 1 0) 0))) (not (= (ite (<= (str.len s) 8) 1 0) 0))) (not (= (ite (= (str.len s) 8) 1 0) 0))) (not (not (= (ite (not (= (str.at s 6) (str.at s 7))) 1 0) 0)))) (not (= (ite (<= (str.len s) 8) 1 0) 0))) (not (= (ite (= (str.len s) 8) 1 0) 0))) (not (not (= (ite (<= (str.len s) 7) 1 0) 0)))) (not (not (= (ite (= (str.len s) 7) 1 0) 0)))) (not (not (= (ite (<= (str.len s) 6) 1 0) 0)))) (not (not (= (ite (= (str.len s) 6) 1 0) 0)))) (not (not (= (ite (<= (str.len s) 5) 1 0) 0)))) (not (not (= (ite (= (str.len s) 5) 1 0) 0)))) (not (not (= (ite (<= (str.len s) 4) 1 0) 0)))) (not (not (= (ite (= (str.len s) 4) 1 0) 0)))) (not (not (= (ite (not (= (str.at s 2) (str.at s 3))) 1 0) 0)))) (not (= (ite (not (= (str.at s 4) (str.at s 6))) 1 0) 0))) (not (not (= (ite (not (= (str.at s 3) (str.at s 7))) 1 0) 0)))) (not (= (ite (<= (str.len s) 8) 1 0) 0))) (not (= (ite (= (str.len s) 8) 1 0) 0))) (not (not (= (ite (<= (str.len s) 7) 1 0) 0)))) (not (not (= (ite (= (str.len s) 7) 1 0) 0)))) (not (not (= (ite (not (= (str.at s 4) (str.at s 5))) 1 0) 0)))) (not (not (= (ite (not (= (str.at s 3) (str.at s 6))) 1 0) 0)))) (not (= (ite (not (= (str.at s 3) (str.at s 5))) 1 0) 0))) (not (= (ite (not (= (str.at s 3) (str.at s 4))) 1 0) 0))) (not (= (ite (not (= (str.at s 4) (str.at s 7))) 1 0) 0))) (not (= (ite (not (= (str.at s 4) (str.at s 6))) 1 0) 0))) (not (= (ite (<= (str.len s) 8) 1 0) 0))) (not (= (ite (= (str.len s) 8) 1 0) 0))) (not (not (= (ite (not (= (str.at s 6) (str.at s 7))) 1 0) 0)))) (not (= (ite (<= (str.len s) 8) 1 0) 0))) (not (= (ite (= (str.len s) 8) 1 0) 0))) (not (not (= (ite (<= (str.len s) 7) 1 0) 0)))) (not (not (= (ite (= (str.len s) 7) 1 0) 0)))) (not (not (= (ite (<= (str.len s) 6) 1 0) 0)))) (not (not (= (ite (= (str.len s) 6) 1 0) 0)))) (not (not (= (ite (not (= (str.at s 4) (str.at s 5))) 1 0) 0)))) (not (= (ite (not (= (str.at s 5) (str.at s 7))) 1 0) 0))) (not (= (ite (not (= (str.at s 5) (str.at s 6))) 1 0) 0))) (not (= (ite (<= (str.len s) 8) 1 0) 0))) (not (= (ite (= (str.len s) 8) 1 0) 0))) (not (not (= (ite (not (= (str.at s 6) (str.at s 7))) 1 0) 0)))) (not (= (ite (<= (str.len s) 8) 1 0) 0))) (not (= (ite (= (str.len s) 8) 1 0) 0))) (not (not (= (ite (<= (str.len s) 7) 1 0) 0)))) (not (not (= (ite (= (str.len s) 7) 1 0) 0)))) (not (not (= (ite (<= (str.len s) 6) 1 0) 0)))) (not (not (= (ite (= (str.len s) 6) 1 0) 0)))) (not (not (= (ite (<= (str.len s) 5) 1 0) 0)))) (not (not (= (ite (= (str.len s) 5) 1 0) 0)))) (not (not (= (ite (<= (str.len s) 4) 1 0) 0)))) (not (not (= (ite (= (str.len s) 4) 1 0) 0)))) (not (not (= (ite (<= (str.len s) 3) 1 0) 0)))) (not (not (= (ite (= (str.len s) 3) 1 0) 0)))) (not (not (= (ite (<= (str.len s) 2) 1 0) 0)))) (not (not (= (ite (= (str.len s) 2) 1 0) 0)))) (not (not (= (ite (<= (str.len s) 1) 1 0) 0)))) (not (not (= (ite (= (str.len s) 1) 1 0) 0)))) (not (not (= (ite (<= (str.len s) 0) 1 0) 0)))) (not (not (= (ite (= (str.len s) 0) 1 0) 0)))))
+
+(check-sat)
+(exit)
-- 
2.30.2