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.

diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index 9e14d6a3f2c1a945a6ec89fbaed4f5a31cee6bae..5b7c383613d6ab680f42de0c3dcdaea5d632008b 100644 (file)
--- 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 b2a62cc62dfba5f2827eb922778d66307f19c99c..b64a0df0122c0b9453a435bd79e9bc2b02fbd062 100644 (file)
--- 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 935a4694ff5bf86f0f29b636b8f10e01ba0049f7..656bb5880ad4534a0a46edc1f3e21dfe5dc3c204 100644 (file)
--- 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 (file)
index 0000000..e2ae94a
--- /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)