diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-04-28 08:07:54 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-04-28 08:07:54 -0500 |
commit | 8ea1603f55d940e56ab3cbee8177f06200228aaa (patch) | |
tree | a263e0beea29d39de303eddb94511a1387295bd2 /src | |
parent | 30c0e8689a1e5f1ae160cde17d8124c86ead1568 (diff) |
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.
Diffstat (limited to 'src')
-rw-r--r-- | src/theory/strings/theory_strings.cpp | 19 | ||||
-rw-r--r-- | src/theory/strings/theory_strings_utils.cpp | 5 |
2 files changed, 22 insertions, 2 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; } } 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) |