diff options
Diffstat (limited to 'src/theory/strings/theory_strings.cpp')
| -rw-r--r-- | src/theory/strings/theory_strings.cpp | 21 |
1 files changed, 16 insertions, 5 deletions
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 1d853a754..c777a0976 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -175,11 +175,7 @@ TheoryStrings::TheoryStrings(context::Context* c, d_true = NodeManager::currentNM()->mkConst( true ); d_false = NodeManager::currentNM()->mkConst( false ); - d_card_size = 256; - if (options::stdPrintASCII()) - { - d_card_size = 128; - } + d_card_size = TheoryStringsRewriter::getAlphabetCardinality(); } TheoryStrings::~TheoryStrings() { @@ -741,6 +737,21 @@ void TheoryStrings::preRegisterTerm(TNode n) { throw LogicException(ss.str()); } if( tn.isString() ) { + // all characters of constants should fall in the alphabet + if (n.isConst()) + { + std::vector<unsigned> vec = n.getConst<String>().getVec(); + for (unsigned u : vec) + { + if (u >= d_card_size) + { + std::stringstream ss; + ss << "Characters in string \"" << n + << "\" are outside of the given alphabet."; + throw LogicException(ss.str()); + } + } + } // if finite model finding is enabled, // then we minimize the length of this term if it is a variable // but not an internally generated Skolem, or a term that does |