diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-06-19 16:48:10 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-06-19 16:48:10 -0500 |
commit | 22780596b561dff9b0eb5b0620252280a678944e (patch) | |
tree | 796c7a3a270f0509f36762ba88e938c644d9dfd4 /test | |
parent | e0633c091c37b79f9e3a2517cf95113c788db083 (diff) |
Convert more uses of strings to words (#4584)
Towards theory of sequences.
This PR also adds support for sequences in default sygus grammars.
Also removes an interface for mkEmptyWord which doesn't have an equivalent for sequences.
Diffstat (limited to 'test')
-rw-r--r-- | test/unit/theory/theory_strings_word_white.h | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/test/unit/theory/theory_strings_word_white.h b/test/unit/theory/theory_strings_word_white.h index bc6279cb8..2e29d50b8 100644 --- a/test/unit/theory/theory_strings_word_white.h +++ b/test/unit/theory/theory_strings_word_white.h @@ -63,7 +63,8 @@ class TheoryStringsWordWhite : public CxxTest::TestSuite Node cac = d_nm->mkConst(String("cac")); Node abca = d_nm->mkConst(String("abca")); - TS_ASSERT(Word::mkEmptyWord(kind::CONST_STRING) == empty); + TypeNode stringType = d_nm->stringType(); + TS_ASSERT(Word::mkEmptyWord(stringType) == empty); std::vector<Node> vec; vec.push_back(abc); |